File WeakABComm.ML

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

*)

val alpha0_E = alpha0.mk_cases "s ->A0 t";
val par_beta_E5 = par_beta.mk_cases "(Var x) $ e -|>B e'";
val i_alpha_E1 = i_alpha.mk_cases "(Abs x e,y) ->iA e3";


Goal "[|e -|>B e'; y~:FV(e); y~:BV(e); x~=y|] ==> (Abs x e',y) ->>iA Abs y (e'[x:=Var y])";
by(rtac rt_ialpha_base 1);
by(ftac par_beta_FV_lemma 1);
by(dtac par_beta_BV_lemma 1);
by(rtac i_alpha.index 1);
by(etac sq_alpha.alpha 1);
by(cut_inst_tac [("x","x"),("e","e'")] capt_in_bound_var 1);
by(Blast_tac 1);
qed "lemmaA_aux_1";


Goal "[|e -|>B e'; y~:FV(e); y~:BV(e)|] ==> e[x:=Var y] -|>B e'[x:=Var y]";
by(rtac par_beta_subst 1);
by(Simp_tac 1);
by(atac 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(ftac par_beta_BV_lemma 2);
by(cut_inst_tac [("x","x"),("e","e'")] capt_in_bound_var 2);
by(Auto_tac);
qed "lemmaA_aux_2";


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


Goal "[|Capt x e' Int A = {}; e -|>B e'; y~:FV(e); y~:BV(e); x~=y|] ==> Capt y (e'[x:=Var y]) Int A = {}";
by(etac Capt_subst_var_lemma_1 1);
by(dtac par_beta_FV_lemma 1);
by(dtac par_beta_BV_lemma 2);
by(ALLGOALS Fast_tac);
qed "lemmaA_aux_3";


Goal "(s,y) ->iA t ==> x~=y --> Capt x t <= Capt x s Un {y}";
by(etac i_alpha.induct 1);
by(dtac ialpha_FV_lemma 4);
by(ALLGOALS Full_simp_tac);
by(Fast_tac 3);
by(Fast_tac 2);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 3);
by(Fast_tac 2);
by(etac sq_alpha_E2 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(dtac FV_subst_lemma_1 3);
by(Asm_full_simp_tac 3);
by(dtac FV_subst_lemma_1 2);
by(etac disjE 2);
by(Asm_full_simp_tac 2);
by(cut_inst_tac [("x","xa"),("e","e"),("e'","Var y")] renaming_sanity_3 2);
by(Asm_simp_tac 2);
by(Asm_simp_tac 2);
by(Blast_tac 2);
by(rotate_tac ~1 2);
by(dtac (Capt_FV_lemma_1 RS mp) 2);
by(Blast_tac 2);
by(cut_inst_tac [("y","x"),("x","xa"),("e","e"),("e'","Var y")] subcase2_lemma_1 1);
by(Auto_tac);
qed "i_alpha_Capt_lemma_1";


Goal "(s,y) ->>iA t ==> x~=y --> Capt x t <= Capt x s Un {y}";
by(etac rt_ialpha.induct 1);
by(Fast_tac 1);
by(strip_tac 1);
by(mp_tac 1);
by(dres_inst_tac [("x","x"),("y","y")] i_alpha_Capt_lemma_1 1);
by(Fast_tac 1);
qed "rt_ialpha_Capt_lemma_1";


Goal "(Abs x s,y) ->iA Abs x t ==> (s,y) ->iA t";
by(etac i_alpha_E1 1);
by(etac sq_alpha_E2 1);
by(Auto_tac);
qed "ialpha_abs_elim";


val i_alpha_E2 = i_alpha.mk_cases "(e,y) ->iA Abs x e'";


Goal "(e,y) ->iA Abs x e' ==> x~=y --> (EX e''. e = Abs x e'')";
by(etac i_alpha_E2 1);
by(ALLGOALS strip_tac);
by(etac sq_alpha_E2 1);
by(Asm_full_simp_tac 1);
by(rtac exI 1);
by(Fast_tac 1);
qed "rt_ialpha_abs_elim_aux";


Goal "(s,y) ->>iA t ==> (ALL s' t'. s = Abs x s' & t = Abs x t' --> x~=y --> (s',y) ->>iA t')";
by(etac rt_ialpha.induct 1);
by(ALLGOALS strip_tac);
by(etac conjE 1);
by(Asm_full_simp_tac 1);
by(rtac rt_ialpha.refl 1);
by(Asm_full_simp_tac 1);
by(ftac rt_ialpha_abs_elim_aux 1);
by(mp_tac 1);
by(etac exE 1);
by(Asm_full_simp_tac 1);
by(dtac ialpha_abs_elim 1);
by(eatac rt_ialpha.trans 1 1);
qed "rt_ialpha_abs_elim";


(* User-friendly version of the above generation lemma for ->>iA *)
Goal "(Abs x s,y) ->>iA (Abs x t) ==> x~=y --> (s,y) ->>iA t";
by(cut_inst_tac [("s","Abs x s"),("t","Abs x t"),("x","x"),("y","y")] rt_ialpha_abs_elim 1);
by(atac 1);
by(Fast_tac 1);
qed "rt_ialpha_abs_elim";


(* Substitutivity lemma on ->sA *)

Goal "(s,y) ->sA t ==> Capt x s Int FV(u) = {} --> Capt x t Int FV(u) = {} --> x~=y --> (s[x:=u],y) ->sA t[x:=u]";
by(strip_tac 1);
by(etac sq_alpha_E2 1);
by(Auto_tac);
by(etac sq_alpha.alpha 6);
by(Fast_tac 6);
by(etac sq_alpha.alpha 5);
by(Fast_tac 5);
by(cut_inst_tac [("x","x"),("e","e"),("e'","Var y")] renaming_sanity_3 2);
by(Asm_simp_tac 2);
by(Simp_tac 2 THEN Fast_tac 2);
by(rotate_tac ~1 2);
by(ftac (renaming_sanity_2 RS mp) 2);
by(Asm_full_simp_tac 2);
by(etac sq_alpha.alpha 2);
by(Fast_tac 2);
by(rotate_tac ~3 3);
by(ftac not_sym 3);
by(case_tac "x:FV(e)" 3);
by(Asm_full_simp_tac 4);
by(etac sq_alpha.alpha 4);
by(Fast_tac 4);
by(Asm_full_simp_tac 3);
by(rotate_tac 4 3);
by(dres_inst_tac [("y2","xa"),("e'2","Var y")] (FV_subst_lemma_2 RS mp RS mp) 3);
by(atac 3);
by(Asm_full_simp_tac 3);
by(Fast_tac 3);
by(case_tac "x=xa" 2);
by(Asm_full_simp_tac 2);
by(cut_inst_tac [("x","xa"),("e","e"),("e'","Var y")] renaming_sanity_3 2);
by(Asm_simp_tac 2);
by(Simp_tac 2 THEN Fast_tac 2);
by(Asm_simp_tac 2);
by(etac sq_alpha.alpha 2);
by(Fast_tac 2);
by(case_tac "x:FV(e)" 2);
by(Asm_full_simp_tac 2);
by(Fast_tac 2);
by(cut_inst_tac [("x1","x"),("e1","e"),("e'1","Var y"),("y1","xa")] (FV_lemma_1 RS mp) 2);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 2);
by(etac sq_alpha.alpha 2);
by(Fast_tac 2);
by(stac Substitution_Lemma_4 1);
by(atac 1);
by(atac 1);
by(atac 1);
by(etac sq_alpha.alpha 1);
by(Asm_simp_tac 1);
by(rtac conjI 1);
by(rtac (FV_lemma_1 RS mp) 1);
by(Asm_simp_tac 1);
by(stac (subcase2_lemma_1 RS sym) 1);
by(REPEAT (atac 1));
qed "sq_alpha_substitutivity";


(* Substitutivity lemma on ->iA *)
Goal "(s,y) ->iA t ==> Capt x s Int FV(u) = {} --> Capt x t Int FV(u) = {} --> x~=y --> (s[x:=u],y) ->iA t[x:=u]";
by(etac i_alpha.induct 1);
by(ALLGOALS strip_tac);
by(REPEAT (dtac Capt_induct_1 2));
by(REPEAT (dtac Capt_induct_1 3));
by(case_tac "xa=x" 4);
by(Asm_simp_tac 4);
by(rotate_tac ~1 4);
by(fatac Capt_induct_3 1 4);
by(rotate_tac ~3 4);
by(fatac Capt_induct_3 1 4);
by(ALLGOALS Asm_full_simp_tac);
by(datac (sq_alpha_substitutivity RS mp RS mp RS mp) 3 1);
by(Fast_tac 1);
qed "i_alpha_substitutivity";


Goal "[|A Int B = {}; C <= (A Un {x}); x~:B|] ==> C Int B = {}";
by(Blast_tac 1);
qed "subset_lemma_3";


(* Substitutivity lemma on ->>iA *)
Goal "(s,y) ->>iA t ==> x~=y --> y~:FV(u) --> Capt x s Int FV(u) = {} --> Capt x t Int FV(u) = {} --> (s[x:=u],y) ->>iA t[x:=u]";
by(etac rt_ialpha.induct 1);
by(ALLGOALS strip_tac);
by(rtac rt_ialpha.refl 1);
by(fatac (rt_ialpha_Capt_lemma_1 RS mp) 1 1);
by(fatac subset_lemma_3 2 1);
by(Asm_full_simp_tac 1);
by(etac rt_ialpha.trans 1);
by(eatac (i_alpha_substitutivity RS mp RS mp RS mp) 3 1);
qed "rt_ialpha_substitutivity";


(* Second substitutivity lemma on squiggly alpha *)
Goal "[|(s,y) ->>iA t; x~=y|] ==> (e[x:=s],y) ->>iA e[x:=t]";
by(case_tac "x:FV(e)" 1);
by(Asm_simp_tac 2);
by(rtac rt_ialpha.refl 2);
by(induct_tac "e" 1);
by(Asm_simp_tac 1);
by(ALLGOALS strip_tac);
by(rtac rt_ialpha.refl 1);
by(Simp_tac 1);
by(eatac (rt_ialpha_doubleApp RS mp) 1 1);
by(case_tac "x = var" 1);
by(Asm_simp_tac 1);
by(rtac rt_ialpha.refl 1);
by(rotate_tac ~1 1);
by(ftac not_sym 1);
by(dtac rt_ialpha_FV_lemma 1);
by(Asm_simp_tac 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(etac rt_ialpha_abs 1);
by(rtac rt_ialpha.refl 1);
qed "rt_ialpha_easy_substitutivity";


(* Key sublemma of Lemma A *)
Goal "(s,y) ->iA0 t ==> ALL t'. s -|>B t' --> (EX s'. t -|>B s' & (t',y) ->>iA s')";
(* Set up the induction over the use of the alpha-0 rule *)
by(etac i_alpha0.induct 1);
by(rotate_tac 1 1);
by(rtac mp 1);
by(atac 2);
by(thin_tac "y~:(FV(s) Un BV(s))" 1);
by(etac i_alpha.induct 1);
by(ALLGOALS strip_tac);
(* Case 1 *)
by(etac sq_alpha_E2 1);
by(Asm_full_simp_tac 1);
by(etac par_beta_E2 1);
by(Asm_simp_tac 1);
by(ftac par_beta_BV_lemma 1);
by(ftac par_beta_FV_lemma 1);
by(etac conjE 1);
by(fatac lemmaA_aux_1 3 1);
by(datac lemmaA_aux_2 2 1);
by(dres_inst_tac [("x","ya")] par_beta.abs 1);
by(rtac exI 1);
by(eatac conjI 1 1);
(* Case 2 *)
by(etac par_beta_E2 3);
by(dtac FV_Un_BV_induct_1 3);
by(mp_tac 3);
by(etac allE 3);
by(mp_tac 3);
by(etac exE 3);
by(etac conjE 3);
by(rotate_tac 4 3);
by(dres_inst_tac [("x","x")] par_beta.abs 3);
by(dres_inst_tac [("x","x")] rt_ialpha_abs 3); 
by(rtac exI 3);
by(Asm_simp_tac 3);
by(Fast_tac 3);
(* The application subgoals are symmetric but must be dealt with separately *)
by(case_tac "sa" 1);
(* Subcase sa = variable *)
by(Asm_full_simp_tac 1);
by(etac par_beta_E5 1);
by(etac par_beta_E1 1);
by(cut_inst_tac [("e","Var var")] par_beta_refl 1);
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(Asm_simp_tac 1);
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.app 1 1);
by(etac rt_ialpha_appL 1);
(* Subcase sa = application *)
by(etac par_beta_E3 1);
by(Asm_full_simp_tac 2);
by(Asm_full_simp_tac 1);
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.app 1 1);
by(Asm_simp_tac 1);
by(etac rt_ialpha_appL 1);
(* Subcase sa = abstraction *)
by(Asm_full_simp_tac 1);
(* Straightforward subsubcase - no beta reduct *)
by(etac par_beta_E4 1);
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.app 1 1);
by(Asm_simp_tac 1);
by(etac rt_ialpha_appL 1);
(* Bitch subsubcase where we have a beta-reduct - splits further *) 
by(etac i_alpha_E1 1);
(* Subsubsubcase where the alpha-reduct is outermost *)
by(etac sq_alpha_E2 1);
by(Asm_full_simp_tac 1);
by(dres_inst_tac [("x","x")] par_beta.abs 1);
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(etac par_beta_E2A 1);
by(rotate_tac ~1 1);
by(fatac lemmaA_aux_2 2 1);
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.beta 1 1);
by(eatac lemmaA_aux_3 3 1);
by(fatac not_sym 1 1);
by(stac Substitution_Lemma_3 1);
by(atac 1);
by(dtac par_beta_FV_lemma 1);
by(datac subset_lemma_1 2 1);
by(dtac par_beta_BV_lemma 1);
by(datac subset_lemma_1 2 1);
by(rtac rt_ialpha.refl 1);
(* Subsubsubcase where the alpha-reduct is not outermost *)
by(dres_inst_tac [("x","var")] par_beta.abs 1);
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(Asm_full_simp_tac 1);
by(rotate_tac ~5 1);
by(etac par_beta_E2 1);
by(Asm_full_simp_tac 1);
by(ftac not_sym 1);
by(datac (rt_ialpha_abs_elim RS mp) 1 1);
by(fatac (rt_ialpha_Capt_lemma_1 RS mp) 1 1);
by(ftac par_beta_FV_lemma 1);
by(rotate_tac ~1 1);
by(fatac subset_lemma_1 1 1);
by(fatac subset_lemma_3 2 1);
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.beta 2 1);
by(eatac (rt_ialpha_substitutivity RS mp RS mp RS mp RS mp) 4 1);
(* Second application case *)
by(Asm_full_simp_tac 1);
by(etac par_beta_E3 1);
(* Straightforward case - no beta reduct *)
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.app 1 1);
by(Asm_simp_tac 1);
by(etac rt_ialpha_appR 1);
(* Tricky case - beta reduct exists *)
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(Asm_simp_tac 1);
by(case_tac "x=ya" 1);
by(Asm_full_simp_tac 1);
by(rtac exI 1);
by(rtac conjI 1);
by(eatac par_beta.beta 1 1);
by(ftac (rt_ialpha_FV_lemma) 1);
by(Asm_full_simp_tac 1);
by(eatac rt_ialpha_easy_substitutivity 1 1);
qed "key_to_WeakABComm";


val alpha0_E = alpha0.mk_cases "s ->A0 t";


(* Adaptation of previous lemma, using ordinary ->>A and ->A0 *)

Goal "[|s ->A0 t;  s -|>B t'|] ==> (EX s'. t -|>B s' & t' ->>A s')";
by(etac alpha0_E 1);
by(dtac key_to_WeakABComm 1);
by(etac allE 1);
by(mp_tac 1);
by(etac exE 1);
by(etac conjE 1);
by(rtac exI 1);
by(etac conjI 1);
by(etac rt_ialpha_in_alpha 1);
qed "real_key_to_WeakABComm";


(* WEAK ALPHA/PARBETA COMMUTATIVITY *)
Goal "[|s ->>A0 t; s -|>B t'|] ==> (EX s'. t -|>B s' & t' ->>A s')";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(etac exE 1);
by(etac conjE 1);
by(datac real_key_to_WeakABComm 1 1);
by(etac exE 1);
by(etac conjE 1);
by(rtac exI 1);
by(etac conjI 1);
by(eatac rtrancl_trans 1 1);
qed "WeakABComm";