File FreshAlphaConf.ML

(*  Title:      FreshAlphaConf.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:    2nd August, 2000

- Proof of fresh-naming alpha confluence
*)

val ialpha1_E1 = i_alpha1.mk_cases "(Var x,y) ->iA1 e";
val ialpha1_E2 = i_alpha1.mk_cases "(Abs x e,y) ->iA1 e'";
val ialpha1_E3 = i_alpha1.mk_cases "(e1 $ e2,y) ->iA1 e'";
val ialpha1_E4 = i_alpha1.mk_cases "(Abs x e,y) ->iA1 e[x:=Var y]";


Goal "y~:(BV(Abs x e) Un FV(Abs x e)) ==> y~:(BV(e) Un FV(e))";
by(Auto_tac);
qed "BV_Un_FV_induct_1";


Goal "y~:(BV(e1 $ e2) Un FV(e1 $ e2)) ==> y~:(BV(e1) Un FV(e1)) & y~:(BV(e2) Un FV(e2))";
by(Auto_tac);
qed "BV_Un_FV_induct_2";


Goal "y~:(BV(e) Un FV(e)) --> (e,y) ->iA1 e";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Full_simp_tac 1);
by(Fast_tac 1);
by(dtac BV_Un_FV_induct_2 1);
by(Fast_tac 1);
by(ftac BV_Un_FV_induct_1 1);
by(mp_tac 1);
by(Full_simp_tac 1);
by(Fast_tac 1);
qed "FAC_proposition_1";


Goal "(e,y) ->iA1 e' ==> y~:(BV(e) Un FV(e))";
by(etac i_alpha1.induct 1);
by(Auto_tac);
qed "FAC_proposition_2";


(* Lemma 3, which involves another horrendous case-split *)
Goal "(e1,z1) ->iA1 e2 ==> ALL e3. (e1,z2) ->iA1 e3 --> z1~=z2 --> (EX e4. (e2,z2) ->iA1 e4 & (e3,z1) ->iA1 e4)";
by(etac i_alpha1.induct 1);
by(ALLGOALS strip_tac);
(* Var rule case *)
by(etac ialpha1_E1 1);
by(Asm_simp_tac 1);
by(Fast_tac 1);
by(defer_tac 1);
(* Abs rule case; splits into two subcases, one of which is trivial *)
by(etac ialpha1_E2 1);
by(Fast_tac 2);
by(rotate_tac 3 1);
by(ftac not_sym 1);
by(rotate_tac ~1 1);
by(fatac (ialpha1_var_subst RS mp RS mp) 1 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("x","z2")] i_alpha1.abs 1);
by(atac 1);
by(Asm_simp_tac 1);
by(rtac exI 1);
by(rtac conjI 1);
by(atac 2);
by(rtac i_alpha1.contr 1);
by(Asm_simp_tac 1);
by(ftac ialpha1_FV_lemma 1);
by(dtac ialpha1_BV_lemma 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
(* AppL rule case; two subcases, one of which is trivial *)
by(etac ialpha1_E3 1);
by(Fast_tac 1);
by(Asm_simp_tac 1);
by(ftac ialpha1_FV_lemma 1);
by(ftac ialpha1_BV_lemma 1);
by(rotate_tac 4 1);
by(ftac ialpha1_FV_lemma 1);
by(ftac ialpha1_BV_lemma 1);
by(rtac exI 1);
by(rtac conjI 1);
by(etac i_alpha1.appR 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(etac i_alpha1.appL 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("x","y")] subset_lemma_1 1);
by(Fast_tac 1);
by(atac 1);
(* AppR rule case; symmetric to the previous case *)
by(etac ialpha1_E3 1);
by(Fast_tac 2);
by(Asm_simp_tac 1);
by(ftac ialpha1_FV_lemma 1);
by(ftac ialpha1_BV_lemma 1);
by(rotate_tac 4 1);
by(ftac ialpha1_FV_lemma 1);
by(ftac ialpha1_BV_lemma 1);
by(rtac exI 1);
by(rtac conjI 1);
by(etac i_alpha1.appL 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(etac i_alpha1.appR 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("x","y")] subset_lemma_1 1);
by(Fast_tac 1);
by(atac 1);
(* Contr rule case; two subcases, one of which is the same as the Abs case *)
by(etac ialpha1_E2 1);
by(defer_tac 1);
by(Asm_full_simp_tac 1);
by(REPEAT (etac conjE 1));
by(rotate_tac 3 1);
by(ftac not_sym 1);
by(rotate_tac ~1 1);
by(fatac (ialpha1_var_subst RS mp RS mp) 1 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("x","y")] i_alpha1.abs 1);
by(atac 1);
by(rtac exI 1);
by(etac conjI 1);
by(rtac i_alpha1.contr 1);
by(Asm_simp_tac 1);
by(ftac ialpha1_FV_lemma 1);
by(dtac ialpha1_BV_lemma 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
(* Subcase involving a second use of Contr *)
by(Asm_full_simp_tac 1);
by(REPEAT (etac conjE 1));
by(ftac not_sym 1);
by(rtac exI 1);
by(rtac conjI 1);
by(dres_inst_tac [("z","y"),("x","x")] BV_var_subst_lemma_1 1);
by(dres_inst_tac [("z","y"),("x","x")] FV_var_subst_lemma_1 1);
by(atac 1);
by(rtac i_alpha1.contr 1);
by(Force_tac 1);
by(stac Substitution_Lemma_3 1);
by(Fast_tac 2);
by(atac 2);
by(Simp_tac 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(Fast_tac 1);
by(rtac (FAC_proposition_1 RS mp) 1);
by(case_tac "y:FV(e)" 1);
by(Asm_full_simp_tac 1);
by(rotate_tac 6 1);
by(dres_inst_tac [("z","z2"),("x","x")] BV_var_subst_lemma_1 1);
by(dres_inst_tac [("z","z2"),("x","x")] FV_var_subst_lemma_1 1);
by(atac 1);
by(Force_tac 1);
qed "FAC_lemma_3";

(* User-friendly formulation of the above *)
Goal "[|(e1,z1) ->iA1 e2; (e1,z2) ->iA1 e3; z1~=z2|] ==> EX e4. (e2,z2) ->iA1 e4 & (e3,z1) ->iA1 e4";
by(dtac FAC_lemma_3 1);
by(Blast_tac 1);
qed "FAC_lemma_3";


(* Lemma 4 *)
Goal "(e1,y) ->iA e2 ==> z~:(FV(e1) Un BV(e1) Un {y}) --> (EX e3. (e1,z) ->iA1 e3 & (e2,z) ->iA1 e3)";
by(etac i_alpha.induct 1);
by(ALLGOALS strip_tac);
by(Auto_tac);
by(rtac exI 1);
by(rtac conjI 1);
by(rtac i_alpha1.contr 2);
by(rotate_tac 4 2);
by(dres_inst_tac [("x","x"),("z","y")] BV_var_subst_lemma_1 2);
by(dres_inst_tac [("x","x"),("z","y")] FV_var_subst_lemma_1 2);
by(atac 2);
by(Asm_simp_tac 2);
by(stac (Substitution_Lemma_1 RS mp RS mp RS mp RS sym) 1);
by(Asm_simp_tac 7);
by(rtac i_alpha1.contr 7);
by(ALLGOALS Asm_full_simp_tac);
by(fatac not_sym 1 1);
by(Fast_tac 1);
by(dtac (Capt_BV_lemma_1 RS mp) 1);
by(Fast_tac 1);
by(dres_inst_tac [("x","x"),("z","y")] BV_var_subst_lemma_1 1);
by(dtac (Capt_BV_lemma_1 RS mp) 1);
by(Fast_tac 1);
qed "FAC_lemma_4"; 


(* User-friendly version of the above *)
Goal "[|(e1,y) ->iA e2; z~:(FV(e1) Un BV(e1) Un {y})|] ==> EX e3. (e1,z) ->iA1 e3 & (e2,z) ->iA1 e3";
by(dtac FAC_lemma_4 1);
by(Fast_tac 1);
qed "FAC_lemma_4";


(* Lemma 6 *)
Goal "(e1,zs) ->>iA1 e2 ==> ALL e3. (e1,z) ->iA1 e3 --> ~(z mem zs) --> (EX e4. (e2,z) ->iA1 e4 & (e3,zs) ->>iA1 e4)";
by(etac cl_ialpha1.induct 1);
by(ALLGOALS strip_tac);
by(Blast_tac 1);
by(dtac (list_theory_1 RS mp) 1);
by(etac conjE 1);
by(etac allE 1);
by(REPEAT (mp_tac 1));
by(etac exE 1);
by(etac conjE 1);
by(datac FAC_lemma_3 2 1);
by(Blast_tac 1);
qed "FAC_lemma_6";


(* User-friendly version of the above *)
Goal "[|(e1,zs) ->>iA1 e2; (e1,z) ->iA1 e3; ~(z mem zs)|] ==> EX e4. (e2,z) ->iA1 e4 & (e3,zs) ->>iA1 e4";
by(dtac FAC_lemma_6 1);
by(Blast_tac 1);
qed "FAC_lemma_6";


Goal "[|(ALL z. z mem (zs) --> ~ z mem xs & z ~: BV e1 & z ~: FV e1); zs=y#ys|] ==> ALL z. z mem ys --> ~ z mem xs & z ~: BV e1 & z ~: FV e1";
by(Asm_full_simp_tac 1);
qed "list_induct_aux";


Goal "[|uniqlist(zs); zs=y#ys|] ==> uniqlist(ys) & ~(y mem ys)";
by(Auto_tac);
qed "uniqlist_induct_1";


(* Lemma 5 *)
Goal "(e1,xs) ->>ciA e2 ==> ALL zs. length(zs) = length(xs) --> uniqlist(zs) --> (ALL z.(z mem zs --> ~(z mem xs) & z~:(BV(e1) Un FV(e1)))) --> (EX e3. (e1,zs) ->>iA1 e3 & (e2,rev zs) ->>iA1 e3)";
by(etac cl_ialpha.induct 1);
by(ALLGOALS strip_tac);
(* Reflexive case *)
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
(* Inductive case; first extract induction hypothesis *)
by(dtac list_theory_2 1);
by(asm_full_simp_tac (simpset() addsimps[length_Suc_conv]) 1);
by(REPEAT_DETERM (etac exE 1));
by(REPEAT_DETERM (etac conjE 1));
by(etac allE 1);
by(mp_tac 1);
by(fatac list_induct_aux 1 1);
by(datac uniqlist_induct_1 1 1);
by(etac conjE 1);
by(REPEAT_DETERM (mp_tac 1));
by(ftac list_theory_4 1);
by(etac allE 1); 
by(etac allE 1);
by(REPEAT_DETERM (mp_tac 1));
by(REPEAT_DETERM (etac exE 1));
by(REPEAT_DETERM (etac conjE 1));
(* Apply Lemma 4, showing y is a suitable fresh variable *)
by(ftac cl_ialpha_FV_lemma 1);
by(dtac cl_ialpha_BV_lemma 1);
by(REPEAT_DETERM (dtac (list_theory_3 RS mp) 1));
by(dtac not_sym 1);
by(Asm_full_simp_tac 1);
by(dtac FAC_lemma_4 1);
by(Asm_full_simp_tac 1);
by(etac conjI 1);
by(etac conjI 1);
by(Fast_tac 1);
by(etac exE 1);
by(etac conjE 1);
(* Apply Lemma 6 *)
by(datac FAC_lemma_6 1 1);
by(rtac (list_theory_5 RS mp) 1);
by(Asm_simp_tac 1);
by(etac exE 1);
by(etac conjE 1);
by(rtac exI 1);
by(rtac conjI 1);
by(eatac cl_ialpha1.trans 1 1);
by(eatac cl_ialpha1_trans2 1 1);
qed "FAC_lemma_5";


(* User-friendly version of Lemma 5 *)
Goal "[|(e1,xs) ->>ciA e2; uniqlist(zs); length(zs) = length(xs); ALL z.(z mem zs --> ~(z mem xs) & z~:(BV(e1) Un FV(e1)))|] ==> (EX e3. (e1,zs) ->>iA1 e3 & (e2,rev zs) ->>iA1 e3)";
by(dtac FAC_lemma_5 1);
by(Auto_tac);
qed "FAC_lemma_5";


(* Lemma 7 *)
Goal "e1 ->>A e2 ==> EX e3. e1 ->>A0 e3 & e2 ->>A0 e3";
by(dtac rt_alpha_to_rt_ialpha 1);
by(etac exE 1);
by(cut_inst_tac [("n","length(xs)"),("e","e1"),("ys","xs")] exists_suitable_list 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(datac FAC_lemma_5 2 1);
by(etac exE 2);
by(etac conjE 2);
by(dtac rt_ialpha1_to_rt_ialpha0 2);
by(dtac rt_ialpha1_to_rt_ialpha0 2);
by(Fast_tac 2);
by(strip_tac 1);
by(etac allE 1);
by(mp_tac 1);
by(rtac conjI 1);
by(Fast_tac 2);
by(rtac (list_theory_5 RS mp) 1);
by(Fast_tac 1);
qed "FAC_lemma_7";


Goal "[|x =A= y; y =A= z|] ==> x =A= z";
by(rtac rtrancl_trans 1);
by(Auto_tac);
qed "alphaeq_trans";


Goal "e ->>A e' ==> e =A= e'";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(rotate_tac 1 1);
by(dres_inst_tac [("B","rev_alpha")] UnI1 1);
by(rotate_tac ~1 1);
by(dtac r_into_rtrancl 1);
by(datac alphaeq_trans 2 1);
qed "rt_alpha_in_alphaeq";


(* FRESH-NAMING ALPHA CONFLUENCE *)
Goal "[|e ->>A e1; e ->>A e2|] ==> EX e3. e1 ->>A0 e3 & e2 ->>A0 e3";
by(rtac FAC_lemma_7 1);
by(REPEAT_DETERM (dtac rt_alpha_in_alphaeq 1));
by(rtac Lemma_D 1);
by(dtac alphaeq_sym 1);
by(rotate_tac 1 1);
by(rtac alphaeq_sym 1);
by(eatac alphaeq_trans 1 1);
qed "FreshAlphaConf";