Up to index of Isabelle/HOL/residual-beta-theory
theory Variables = Main(* 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