File Variables.ML

(*  Title:      Variables.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:	3rd August, 2000

- Proof of existence of fresh variables w.r.t any finite variable set

*)


Goal "finite(A::nat set) ==> EX m. (ALL x:A .x<=m)";
by(etac finite_induct 1);
by(Fast_tac 1);
by(etac exE 1);
by(case_tac "x<=m" 1);
by(Blast_tac 1);
by(Asm_full_simp_tac 1);
by(rtac exI 1);
by(rtac conjI 1);
by(Fast_tac 1);
by(Auto_tac);
qed "exists_max_in_finite_set";


Goal "(ALL x:A. x<=m) ==> ALL x:A. x < Suc m";
by(Auto_tac);
qed "exists_sup_in_finite_set_1";


Goal "finite(A::nat set) ==> EX n. ALL x:A. x < n";
by(dtac exists_max_in_finite_set 1);
by(etac exE 1);
by(dtac exists_sup_in_finite_set_1 1);
by(Auto_tac);
qed "exists_sup_in_finite_set_2";


Goal "finite(A::nat set) ==> EX y. y~:A";
by(dtac exists_sup_in_finite_set_2 1);
by(Blast_tac 1);
qed "finite_implies_exists_freshvar";


Goal "finite(A::var set) ==> finite(deX `` A)";
by(etac finite_induct 1);
by(Simp_tac 1);
by(Auto_tac);
qed "finite_var_to_nat";


Goal "X(deX y) = y";
by(induct_tac "y" 1);
by(Auto_tac);
qed "X_lemma_1";


Goal "y:A ==> X y: X``A";
by(Auto_tac);
qed "X_set_mono";


Goal "y:A ==> deX y: deX``A";
by(Auto_tac);
qed "deX_set_mono";


Goal "(X``(deX``A)) = A";
by(Auto_tac);
by(asm_simp_tac (simpset() addsimps[X_lemma_1]) 1);
by(dtac deX_set_mono 1);
by(dtac X_set_mono 1);
by(asm_full_simp_tac (simpset() addsimps[X_lemma_1]) 1);
qed "X_set_lemma_1";


Goal "y~:(deX `` A) ==> (X y)~:(X``(deX``A))";
by(Blast_tac 1);
qed "nat_to_var_mono_1";


Goal "finite(A::var set) ==> EX y. y~:A";
by(dtac finite_var_to_nat 1);
by(dtac finite_implies_exists_freshvar 1);
by(etac exE 1);
by(dtac nat_to_var_mono_1 1);
by(asm_full_simp_tac (simpset() addsimps[X_set_lemma_1]) 1);
by(Auto_tac);
qed "finite_implies_ex_freshvar";