File ParBeta.ML

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

- Properties of the parallel beta relation. including substitutivity

*)

val par_beta_E1 = par_beta.mk_cases "Var x -|>B e'";
val par_beta_E2 = par_beta.mk_cases "Abs x e -|>B e'";
val par_beta_E2A = par_beta.mk_cases "Abs x e -|>B Abs x e'";
val par_beta_E3 = par_beta.mk_cases "e1 $ e2 -|>B e'";
val par_beta_E4 = par_beta.mk_cases "(Abs x e) $ e' -|>B e''";

Addsimps par_beta.intrs;
AddSIs par_beta.intrs;
AddSEs [par_beta_E1,par_beta_E2,par_beta_E3,par_beta_E4];

Goal "e -|>B e";
by(induct_tac "e" 1);
by(ALLGOALS Asm_simp_tac);
qed "par_beta_refl";
Addsimps [par_beta_refl];


Goal "ALL t'. t -|>B t' --> FV(t') <= FV(t)";
by(induct_tac "t" 1);
by(ALLGOALS strip_tac);
by(Fast_tac 1); 
by(etac par_beta_E2 2);
by(Asm_simp_tac 2); 
by(Fast_tac 2); 
by(etac par_beta_E3 1); 
by(ALLGOALS Asm_full_simp_tac); 
by(Fast_tac 1);
by(dtac par_beta.abs 1); 
by(REPEAT_DETERM (etac allE 1)); 
by(REPEAT_DETERM (mp_tac 1)); 
by(Auto_tac); 
by(ALLGOALS (ftac FV_subst_lemma_1)); 
by(ALLGOALS (etac disjE)); 
by(Fast_tac 1);
by(Fast_tac 2); 
by(ALLGOALS (rotate_tac 3));
by(ALLGOALS (datac subset_lemma_1 1));
by(datac renaming_sanity_3 1 2);
by(contr_tac 2);
by(eatac subset_lemma_2 1 1);
by(rotate_tac ~2 1);
by(Auto_tac);
by(datac renaming_sanity_3 1 1);
by(contr_tac 1);
qed "par_beta_FV_lemma";


Goal "t -|>B t' ==> FV(t') <= FV(t)";
by(asm_full_simp_tac (simpset() addsimps[par_beta_FV_lemma]) 1);
qed "par_beta_FV_lemma";


Goal "ALL t'. t -|>B t' --> BV(t') <= BV(t)";
by(induct_tac "t" 1);
by(ALLGOALS strip_tac);
by(Fast_tac 1); 
by(etac par_beta_E2 2); 
by(Asm_simp_tac 2); 
by(Fast_tac 2); 
by(etac par_beta_E3 1); 
by(ALLGOALS Asm_full_simp_tac); 
by(Fast_tac 1);
by(dtac par_beta.abs 1); 
by(REPEAT_DETERM (etac allE 1)); 
by(REPEAT_DETERM (mp_tac 1)); 
by(Auto_tac); 
by(dtac BV_subst_lemma_1 1); 
by(etac disjE 1); 
by(Fast_tac 1);
by(Fast_tac 1); 
qed"par_beta_BV_lemma";


Goal "t -|>B t' ==> BV(t') <= BV(t)";
by(asm_full_simp_tac (simpset() addsimps[par_beta_BV_lemma]) 1);
qed "par_beta_BV_lemma";


Goal "x~=y | x:FV(e') ==> Capt x e <= Capt x (e[y:=e'])";
by(induct_tac "e" 1);
by(Simp_tac 1);
by(Simp_tac 1);
by(Fast_tac 1);
by(Asm_simp_tac 1);
by(REPEAT ((rtac conjI 1) THEN (strip_tac 1)));
by(Fast_tac 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(rtac conjI 3);
by(rtac conjI 4);
by(ALLGOALS strip_tac);
by(TRYALL Fast_tac);
by(Auto_tac);
by(case_tac "x = y" 2);
by(thin_tac "y:FV(e')" 3);
by(distinct_subgoals_tac);
by(rotate_tac ~1 1);
by(datac (FV_subst_lemma_2 RS mp RS mp) 1 1);
by(Fast_tac 1);
by(case_tac "y:FV(lterm)" 1);
by(rotate_tac ~1 2);
by(Asm_full_simp_tac 2);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1);
by(datac (FV_subst_lemma_3 RS mp) 1 1);
by(Fast_tac 1);
qed "Capt_in_capt_subst_1";


Goal "[|(Capt x (e[y:=e1])) Int A = {}; (Capt x (Abs y s)) Int B = {}; FV(e) <= FV(s); A <= B |] ==> (Capt x (Abs y e)) Int A = {}";
by(case_tac "x=y" 1);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(e)" 1);
by(Asm_simp_tac 2);
by(rotate_tac ~2 1);
by(ftac disjI1 1);
by(dtac Capt_in_capt_subst_1 1);
by(Asm_simp_tac 1);
by(datac subsetD 1 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
qed "key_induction_1";


Goal "[|(Capt y e) Int FV(e') = {}; y:FV(e)|] ==> Capt x e' <= Capt x (e[y:=e'])";
by(rtac mp 1);
by(atac 2);
by(rtac mp 1);
by(rotate_tac 1 2);
by(atac 2);
by(thin_tac "y:FV(e)" 1);
by(thin_tac "Capt y e Int FV(e') = {}" 1);
by(induct_tac "e" 1);
by(Simp_tac 1);
by(Simp_tac 1);
by(Blast_tac 1);
by(strip_tac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(etac conjE 1);
by(dtac not_sym 1);
by(fatac Capt_induct_3 1 1);
by(mp_tac 1);
by(rtac conjI 1);
by(rtac conjI 2);
by(Fast_tac 2);
by(ALLGOALS strip_tac);
by(ALLGOALS Simp_tac);
by(ALLGOALS (rtac conjI));
by(rtac conjI 4);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(Fast_tac 1);
by(asm_simp_tac (simpset() addsimps[Capt_FV_lemma_1]) 1);
by(rotate_tac ~1 1);
by(dtac (Capt_FV_lemma_1 RS mp) 1);
by(Fast_tac 1);
by(ALLGOALS (dtac Capt_Int_FV_lemma_1));
by(ALLGOALS Fast_tac);
qed "Capt_in_capt_subst_2";


Goal "[|(Capt x (e[y:=e'])) Int A = {}; (Capt y e) Int FV(e') = {}; y:FV(e)|] ==> (Capt x e') Int A = {}";
by(rotate_tac 1 1);
by(datac Capt_in_capt_subst_2 1 1);
by(Fast_tac 1);
qed "key_induction_2";


Goal "[|A Int FV(e) = {}; A Int FV(e') = {}|] ==> A Int FV(e[x:=e']) = {}";
by(Auto_tac);
by(dtac FV_subst_lemma_1 1);
by(Blast_tac 1);
qed "Int_subst_lemma_1";


Goal "[|(Capt y e) Int FV(e1) = {}; (Capt y (e[x:=e1])) Int FV(e2) = {}|] ==> (Capt y e) Int FV(e1[x:=e2]) = {}";
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(rotate_tac ~1 1);
by(case_tac "y=x" 1);
by(dtac disjI2 1);
by(dtac Capt_in_capt_subst_1 1);
by(etac Int_subst_lemma_1 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(ftac disjI1 1);
by(dtac Capt_in_capt_subst_1 1);
by(etac Int_subst_lemma_1 1);
by(Fast_tac 1);
qed "subcase1_lemma_1";


Goal "(Capt x e) Int FV(e1) = {} --> (Capt x e) Int FV(e1[x:=e2]) = {} --> e[x:=e1][x:=e2] = e[x:=e1[x:=e2]]";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Simp_tac 1);
by(REPEAT_DETERM (dtac Capt_induct_1 1));
by(Asm_full_simp_tac 1);
by(case_tac "var=x" 1);
by(Asm_simp_tac 1);
by(case_tac "x:FV(lterm)" 1);
by(Asm_simp_tac 2);
by(ftac not_sym 1);
by(fatac Capt_subst_enabling 1 1);
by(rotate_tac 2 1);
by(fatac Capt_subst_enabling 1 1);
by(fatac Capt_induct_3 1 1);
by(rotate_tac 2 1);
by(fatac Capt_induct_3 1 1);
by(REPEAT (mp_tac 1));
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs,subst_Abs]) 1);
by(auto_tac ((claset(),simpset() delsimps[Capt_Abs])));
by(fatac Capt_Int_FV_lemma_1 1 1);
by(case_tac "var:FV(e1)" 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~6 1);
by(fatac Capt_Int_FV_lemma_1 1 1);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(rotate_tac ~1 1);
by(dtac (FV_subst_lemma_4 RS mp) 1);
by(rotate_tac 5 1);
by(mp_tac 1);
by(Auto_tac);
qed "subcase1_lemma_2";


Goal "[|y~:FV(e'); y~=x|] ==> Capt y e = Capt y(e[x:=e'])";
by(induct_tac "e" 1);
by(dtac (Capt_FV_lemma_1 RS mp) 1);
by(Asm_full_simp_tac 1);
by(Asm_simp_tac 1);
by(Asm_simp_tac 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(etac conjE 1);
by(dtac FV_subst_lemma_1 1);
by(Fast_tac 1);
by(dtac FV_subst_lemma_5 1);
by(Fast_tac 1);
qed "subcase2_lemma_1";


Goal "[|(Capt y e) Int FV(e1) = {}; (Capt x (e[y:=e1])) Int FV(e2) = {}; x~=y; y:FV(e)|] ==> (Capt y e) Int FV(e1[x:=e2]) = {}";
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(fatac (Capt_subst_distribute RS mp RS mp) 3 1);
by(etac Int_subst_lemma_1 1);
by(Auto_tac);
qed "subcase2_lemma_2";


Goal "[|(Capt x (Abs xa s'a)) Int FV(t') = {}; xa:FV(t'); x~=xa|] ==> x~:FV(s'a)";
by(Auto_tac);
qed "subcase3_lemma_1";


(* Substitutivity of parallel-beta *)

Goal "ALL x s' t t'. t -|>B t' --> s -|>B s' --> ((Capt x s) Int FV(t) ={}) --> ((Capt x s') Int FV(t') = {}) --> s[x:=t] -|>B s'[x:=t']";
by(induct_tac "s" 1);
by(ALLGOALS strip_tac);
(* Case s = variable *)
by(etac par_beta_E1 1);
by(Asm_simp_tac 1);
by(defer_tac 1);
(* Case s = abstraction *)
by(etac par_beta_E2 1);
by(case_tac "var = x" 1);
by(Asm_full_simp_tac 1);
by(fatac Capt_induct_3 1 1);
by(REPEAT_DETERM (etac allE 1));
by(REPEAT_DETERM (mp_tac 1));
by(rotate_tac 2 1);
by(ftac Capt_induct_3 1);
by(Asm_full_simp_tac 1);
by(mp_tac 1);
by(Asm_simp_tac 1);
by(rtac conjI 1);
by(strip_tac 1);
by(rotate_tac 5 1);
by(dtac par_beta_FV_lemma 1);
by(Blast_tac 1);
by(strip_tac 1);
by(case_tac "x:FV(lterm)" 1);
by(Asm_full_simp_tac 2);
by(dtac Capt_Int_FV_lemma_1 1);
by(Fast_tac 1);
by(Fast_tac 1);
(* Case s = application *)
by(dtac Capt_induct_1 1);
by(etac conjE 1);
by(etac par_beta_E3 1);
(* Easy subcase s' = application *)
by((REPEAT_DETERM (etac allE 1)) THEN (REPEAT_DETERM (mp_tac 1)));
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
(* Bitch subcase s' = substitution *)
by(rotate_tac ~5 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(ftac par_beta.abs 1);
by(REPEAT_DETERM (etac allE 1));
by(rotate_tac 5 1);
by(REPEAT_DETERM (mp_tac 1));
by(ftac par_beta_FV_lemma 1);
by(rotate_tac 5 1);
by(ftac par_beta_FV_lemma 1);
by(fatac key_induction_1 3 1);
by(mp_tac 1);
(* Split into sub-subcases *)
by(rtac conjI 1);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(etac conjE 1);
by(case_tac "xa=x" 3);
by(thin_tac "xa:FV(t)" 3);
by(ALLGOALS (asm_full_simp_tac (simpset() delsimps[Capt_Abs])));
by(distinct_subgoals_tac);
by(defer_tac 1);
(* Sub-subcase xa = x *)
by(fatac subcase1_lemma_1 1 1);
by(stac (subcase1_lemma_2 RS mp RS mp) 1);
by(REPEAT_DETERM (atac 1));
by(case_tac "x:FV(s'a)" 1);
by(datac key_induction_2 2 1);
by(mp_tac 1);
by(eatac par_beta.beta 2 1);
by(cut_inst_tac [("e","lterm2[x:=t]")] par_beta_refl 1);
by(dtac par_beta.beta 1);
by(rotate_tac ~1 1);
by(atac 1);
by(rotate_tac ~2 1);
by(dtac (Capt_FV_lemma_1 RS mp) 1);
by(rotate_tac ~1 1);
by(Fast_tac 1);
by(Asm_full_simp_tac 1);
by(defer_tac 1);
(* Sub-subcase xa ~= x & xa~:FV(t') *)
by(fatac subset_lemma_1 1 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(case_tac "xa:FV(s'a)" 1); 
by(ftac not_sym 1);
by(fatac subcase2_lemma_2 3 1);
by(cut_inst_tac [("y","xa"),("e","s'a"),("e'","t'")] subcase2_lemma_1 1);
by(atac 1);
by(fatac not_sym 1 1);
by(fatac key_induction_2 2 1);
by(rotate_tac 12 1);
by(fatac Capt_induct_3 1 1);
by(stac (Substitution_Lemma_1 RS mp RS mp RS mp RS sym) 1);
by(REPEAT_DETERM (atac 1));
by(Asm_full_simp_tac 1);
by(etac par_beta_E2A 1);
by(rotate_tac ~1 1);
by(dtac par_beta.beta 1);
by(rotate_tac ~8 1);
by(REPEAT_DETERM (atac 1));
by(etac par_beta_E2A 1);
by(rotate_tac ~1 1);
by(cut_inst_tac [("e","lterm2[x:=t]")] par_beta_refl 1);
by(cut_inst_tac [("e","s'a"),("e'","t'"),("x","xa")] FV_lemma_1 1);
by(dtac par_beta.beta 1);
by(rotate_tac ~2 1);
by(atac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(rotate_tac ~1 1);
by(ftac (Capt_FV_lemma_1 RS mp) 1);
by(rotate_tac ~1 1);
by(Fast_tac 1);
by(Asm_full_simp_tac 1);
(* Subcase xa:FV(t); splits into xa:FV(t') and xa~:FV(t') *)
(* xa ~:FV(t') is exactly like the previous case *)
by(case_tac "xa~:FV(t')" 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(case_tac "xa:FV(s'a)" 1); 
by(ftac not_sym 1);
by(fatac subcase2_lemma_2 3 1);
by(cut_inst_tac [("y","xa"),("e","s'a"),("e'","t'")] subcase2_lemma_1 1);
by(atac 1);
by(fatac not_sym 1 1);
by(fatac key_induction_2 2 1);
by(rotate_tac 12 1);
by(fatac Capt_induct_3 1 1);
by(stac (Substitution_Lemma_1 RS mp RS mp RS mp RS sym) 1);
by(REPEAT_DETERM (atac 1));
by(Asm_full_simp_tac 1);
by(etac par_beta_E2A 1);
by(rotate_tac ~1 1);
by(dtac par_beta.beta 1);
by(rotate_tac ~8 1);
by(REPEAT_DETERM (atac 1));
by(etac par_beta_E2A 1);
by(rotate_tac ~1 1);
by(cut_inst_tac [("e","lterm2[x:=t]")] par_beta_refl 1);
by(cut_inst_tac [("e","s'a"),("e'","t'"),("x","xa")] FV_lemma_1 1);
by(dtac par_beta.beta 1);
by(rotate_tac ~2 1);
by(atac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(rotate_tac ~1 1);
by(ftac (Capt_FV_lemma_1 RS mp) 1);
by(rotate_tac ~1 1);
by(Fast_tac 1);
by(Asm_full_simp_tac 1);
(* Only one "proper" subcase remaining: xa:FV(t'); xa~=x *)
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(rotate_tac ~4 1);
by(ftac not_sym 1);
by(fatac subcase3_lemma_1 2 1);
by(case_tac "xa:FV(s'a)" 1);
by(fatac key_induction_2 2 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(fatac subcase2_lemma_2 3 1);
by(dtac par_beta.beta 1);
by(rotate_tac 5 1);
by(atac 1);
by(atac 1);
(* substitution lemma for this subcase now required in subgoal 1 *)
by(dtac par_beta.beta 2);
by(cut_inst_tac [("e","lterm2[x:=t]")] par_beta_refl 2);
by(rotate_tac ~1 2);
by(atac 2);
by(rotate_tac ~1 2);
by(ftac (Capt_FV_lemma_1 RS mp) 2);
by(rotate_tac ~1 2);
by(Fast_tac 2);
by(Asm_full_simp_tac 2);
by(stac (Substitution_Lemma_2 RS mp RS mp RS mp RS mp RS sym) 1);
by(REPEAT_DETERM (atac 1));
qed "par_beta_subst";


(* More user-friendly version of par-beta substitutivity *)
Goal "[|t -|>B t'; s -|>B s'; (Capt x s) Int FV(t) ={}; (Capt x s') Int FV(t') = {}|] ==> s[x:=t] -|>B s'[x:=t']";
by(asm_full_simp_tac (simpset() addsimps[par_beta_subst]) 1);
qed "par_beta_subst";