File VarList.ML

(*  Title:      VarList.thy
    Author:     James Brotherston / Rene Vestergaard
    Revised:    30th August, 2000

- Useful lemmas about existence of lists of fresh variable, plus auxiliaries

*)


Goal "~(z mem x#xs) --> x~=z & ~z mem xs";
by(Auto_tac);
qed "list_theory_1";


Goal "(ALL z. z mem zs --> ~(z mem x#xs) & Q z) ==> (ALL z. z mem zs --> ~(z mem xs) & Q z) & (ALL z. z mem zs --> x~=z)";
by(rtac conjI 1);
by(ALLGOALS strip_tac); 
by(ALLGOALS (etac allE));
by(ALLGOALS mp_tac);
by(ALLGOALS (etac conjE));
by(ALLGOALS (dtac (list_theory_1 RS mp)));
by(ALLGOALS Fast_tac);
qed "list_theory_2";


Goal "~(y mem ys) --> y~:set(ys)";
by(induct_tac "ys" 1);
by(Asm_full_simp_tac 1);
by(Auto_tac);
qed "list_theory_3";


Goal "zs = y#ys ==> y mem zs";
by(Auto_tac);
qed "list_theory_4";


Goal "y~:(set ys) --> ~(y mem ys)";
by(induct_tac "ys" 1);
by(Auto_tac);
qed "list_theory_5";



(* Show existence of suitable list of variables for use in Lemma 5 *)

Goal "length(zs) = x --> finite (FV(e) Un BV(e) Un set(ys) Un set(zs))";
by(induct_tac "e" 1);
by(Auto_tac);
qed "finite_var_lemma_1";


Goal "length(zs) = x ==> EX z. z~:FV(e) Un BV(e) Un set(ys) Un set(zs)";
by(ftac (finite_var_lemma_1 RS mp) 1);
by(etac (finite_var_lemma_1 RS mp RS finite_implies_ex_freshvar) 1);
qed "exists_suitable_z";


Goal "z mem zs --> z:(set zs)";
by(induct_tac "zs" 1);
by(Auto_tac);
qed "mem_impl_set";


Goal "z:(set zs) --> z mem zs";
by(induct_tac "zs" 1);
by(Auto_tac);
qed "set_impl_mem";


Goal "EX zs. length(zs) = n & uniqlist(zs) & (ALL z. (z mem zs) --> z~:FV(e) Un BV(e) Un set(ys))";
by(induct_tac "n" 1);
by(Asm_full_simp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(asm_full_simp_tac (simpset() addsimps[length_Suc_conv]) 1);
by(cut_inst_tac [("e","e"),("ys","ys"),("zs","zs")] exists_suitable_z 1);
by(atac 1);
by(etac exE 1);
by(res_inst_tac [("x","z#zs")] exI 1);
by(rtac conjI 1);
by(res_inst_tac [("x","z")] exI 1);
by(res_inst_tac [("x","zs")] exI 1);
by(rtac conjI 1);
by(Simp_tac 1);
by(atac 1);
by(rtac conjI 1);
by(strip_tac 2);
by(dtac (mem_impl_set RS mp) 2);
by(Auto_tac);
by(rotate_tac ~2 1);
by(dtac (list_theory_5 RS mp) 1);
by(contr_tac 1);
by(ALLGOALS (dtac (set_impl_mem RS mp)));
by(ALLGOALS (etac allE));
by(ALLGOALS (mp_tac));
by(Auto_tac);
qed "exists_suitable_list";