File Alpha.ML

(*  Title:      Alpha.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:	11th July, 2000

- Proof of alpha-symmetry
- Proof of Lemma D

*)

val sq_alpha_E1 = sq_alpha.mk_cases "((Abs x e),y) ->sA (Abs y (e[x:=Var y]))";
val sq_alpha_E2 = sq_alpha.mk_cases "(e,y) ->sA e'";
val alpha_E = alpha.mk_cases "e ->A e'";
val rev_alpha_E = rev_alpha.mk_cases "e A<- e'";

AddSEs[sq_alpha_E1,sq_alpha_E2,alpha_E,rev_alpha_E];
AddSIs i_alpha.intrs;
Addsimps i_alpha.intrs;
AddSIs alpha.intrs;
Addsimps alpha.intrs;
AddSIs rev_alpha.intrs;
Addsimps rev_alpha.intrs;


(* Lemma showing symmetry of alpha-equivalence *)
Goal "(e1 =A= e2) ==> (e2 =A= e1)";
by(etac rtrancl_induct 1);
by(Simp_tac 1);
by(Full_simp_tac 1);
by(etac disjE 1);
by(ALLGOALS (rotate_tac 2));
by(ALLGOALS (rtac rtrancl_trans));
by(atac 2);
by(atac 3);
by(dtac rev_alpha.rev 1);
by(etac rev_alpha_E 2);
by(ALLGOALS (rotate_tac 2));
by(dres_inst_tac [("A","alpha")] UnI2 1);
by(dres_inst_tac [("B","rev_alpha")] UnI1 2);
by(distinct_subgoals_tac);
by(etac r_into_rtrancl 1);
qed "alphaeq_sym";


Goal "[|x~=y; y~:Capt x e|] ==> x~:FV(e[x:=Var y])";
by(rtac renaming_sanity_3 1);
by(Auto_tac);
qed "aux_symmetry_lemma_1";


Goal "x~=y & y~:FV(e) & y~:(Capt x e) --> x~:(Capt y (e[x:=Var y]))";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Simp_tac 1);
by(Asm_full_simp_tac 1);
by(Full_simp_tac 1);
by(Asm_full_simp_tac 1);
by(Auto_tac);
by(rotate_tac 2 1);
by(etac swap 1);
by(Auto_tac);
qed "aux_symmetry_lemma_2";


Goal "(((Abs x e),y) ->sA (Abs y (e[x:=Var y]))) ==> ((Abs y (e[x:=Var y])),x) ->sA (Abs x ((e[x:=Var y])[y:=Var x]))";
by(etac sq_alpha_E1 1);
by(rtac sq_alpha.alpha 1);
by(Fast_tac 1);
by(Auto_tac);
by(datac aux_symmetry_lemma_1 1 1);
by(Fast_tac 1);
by(asm_full_simp_tac (simpset() addsimps[aux_symmetry_lemma_2]) 1);
qed "local_alpha_symmetry_1";


Goal "((Abs x e),y) ->sA (Abs y (e[x:=Var y])) ==> e = ((e[x:=Var y])[y:=Var x])";
by(etac sq_alpha_E1 1);
by(asm_full_simp_tac (simpset() addsimps[renaming_sanity_4]) 1);
qed "renaming4_enabled";


Goal "((Abs x e),y) ->sA (Abs y (e[x:=Var y])) ==> ((Abs y (e[x:=Var y])),x) ->sA (Abs x e)";
by(ftac renaming4_enabled 1);
by(dtac local_alpha_symmetry_1 1);
by(Asm_full_simp_tac 1);
qed "local_alpha_symmetry_2";


Goal "[|x~=y; y~:FV(e); y~:(Capt x e)|] ==> ((Abs y (e[x:=Var y])),x) ->sA (Abs x e)"; 
by(rtac local_alpha_symmetry_2 1); 
by(rtac sq_alpha.alpha 1); 
by(Auto_tac); 
qed "local_alpha_symmetry_3"; 


(* Symmetry of squiggly alpha *)
Goal "((e,y) ->sA e') ==> EX x. ((e',x) ->sA e)"; 
by(etac sq_alpha_E2 1); 
by(Asm_full_simp_tac 1); 
by(datac local_alpha_symmetry_3 2 1); 
by(eresolve_tac [exI] 1); 
qed "squiggly_alpha_symmetric";


(* Symmetry of indexed alpha *)
Goal "((e,y) ->iA e') ==> (EX x. ((e',x) ->iA e))";
by(etac i_alpha.induct 1);
by(dtac squiggly_alpha_symmetric 1);
by(ALLGOALS (etac exE));
by(ALLGOALS (rtac exI));
by(etac i_alpha.index 1);
by(ALLGOALS (rotate_tac 1));
by(dtac i_alpha.aappL 1);
by(dtac i_alpha.aappR 2);
by(dtac i_alpha.aabs 3);
by(ALLGOALS atac);
qed "index_alpha_symmetric";


(* Symmetry of the 'proper' alpha rewrite relation *)
Goal "(e ->A e') ==> (e' ->A e)";
by(etac alpha_E 1);
by(dtac index_alpha_symmetric 1);
by(etac exE 1);
by(etac alpha.strip 1);
qed "alpha_symmetric";


(* LEMMA D *)
Goal "(e =A= e') ==> (e' ->>A e)";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(Full_simp_tac 1);
by(etac disjE 1);
by(dtac alpha_symmetric 1);
by(etac rev_alpha_E 2);
by(distinct_subgoals_tac);
by(eatac rtrancl_into_rtrancl2 1 1);
qed "Lemma_D";