Theory Variables

Up to index of Isabelle/HOL/residual-beta-theory

theory Variables = Main
files [Variables.ML]:
(*  Title:      Variables.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    3rd August, 2000

- Definition of an infinite set of named variables as an isomorphic copy of nat
*)

Variables = Main +

datatype var = X nat

consts  deX :: var => nat

primrec deX "deX (X n) = n"

end

theorem exists_max_in_finite_set:

  finite A ==> EX m. ALL x:A. x <= m

theorem exists_sup_in_finite_set_1:

  ALL x:A. x <= m ==> ALL x:A. x < Suc m

theorem exists_sup_in_finite_set_2:

  finite A ==> EX n. ALL x:A. x < n

theorem finite_implies_exists_freshvar:

  finite A ==> EX y. y ~: A

theorem finite_var_to_nat:

  finite A ==> finite (deX `` A)

theorem X_lemma_1:

  X (deX y) = y

theorem X_set_mono:

  y : A ==> X y : X `` A

theorem deX_set_mono:

  y : A ==> deX y : deX `` A

theorem X_set_lemma_1:

  X `` deX `` A = A

theorem nat_to_var_mono_1:

  y ~: deX `` A ==> X y ~: X `` deX `` A

theorem finite_implies_ex_freshvar:

  finite A ==> EX y. y ~: A