File MarkedLambda.ML

(*  Title:      MarkedLambda.ML
    Author:     James Brotherston / Rene Vestergaard
    Revised:    19th March, 2001

*)

(* Proposition of Renaming Sanity and lemmas *)

Goal "y:Capt x e --> x:FV(e)";
by(induct_tac "e" 1);
by(Auto_tac);
qed_spec_mp "FV_Capt_1";


Goal "x~:FV(e) --> Capt x e = {}";
by(induct_tac "e" 1);
by(ALLGOALS Full_simp_tac);
by(ALLGOALS Fast_tac);
qed_spec_mp "FV_Capt_2";


Goal "e[x:=Var x] = e";
by(induct_tac "e" 1);
by(Auto_tac);
qed "renaming_sanity_1";


Goal "x~:FV(e) --> (e[x:=e'] = e)";
by(induct_tac "e" 1);
by(Auto_tac);
qed_spec_mp "renaming_sanity_2";


Goal "(Capt x e) <= BV(e)";
by(induct_tac "e" 1);
by(Auto_tac);
qed "Capt_in_BV";


Addsimps[renaming_sanity_1, renaming_sanity_2, FV_Capt_1];
Goal "x ~: FV e' & Capt x e Int FV e' = {} --> x ~: FV (e[x:=e'])";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(SELECT_GOAL Auto_tac 1);
by(SELECT_GOAL Auto_tac 1);
by(SELECT_GOAL Auto_tac 1);
by(Asm_full_simp_tac 1);
by(Clarify_tac 1);
by(Force_tac 1);
qed_spec_mp "renaming_sanity_3";


Goal "Capt y (e1 $ e2) Int A = {} ==> Capt y e1 Int A = {} & Capt y e2 Int A = {}";
by(Auto_tac);
qed "Capt_induct_1";


Goal "[|y~=x; Capt x (Abs y e) Int A = {}|] ==> Capt x e Int A = {}";
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(e)" 1);
by(dtac not_sym 1);
by(ALLGOALS Asm_full_simp_tac);
by(Fast_tac 1);
by(dtac FV_Capt_2 1);
by(Fast_tac 1);
qed "Capt_induct_2";


Goal "Capt y (<Abs var e1> @ e2 ) Int A = {} ==> Capt y e2 Int A = {} & (var~=y --> Capt y e1 Int A = {} & (y:FV(e1) --> var~:A))";
by(Auto_tac);
qed "Capt_induct_3";


Goal "[|(Capt y (Abs z e)) Int FV(e') = {}; z~=y|] ==> z~:FV(e') | y~:FV(e)";
by(Auto_tac);
qed "Capt_Int_FV_lemma_1";


Goal "[|A <= B; x~:B|] ==> x~:A";
by(Blast_tac 1);
qed "subset_lemma_1";


Goal "x:FV(e[y:=e']) --> x:FV(e) | x:FV(e')";
by(induct_tac "e" 1);
by(Auto_tac);
qed_spec_mp "FV_subst_lemma_1";


Goal "x:FV(e) --> x~=y --> x:FV(e[y:=e'])";
by(induct_tac "e" 1);
by(Auto_tac);
qed_spec_mp "FV_subst_lemma_2";


Goal "x:FV(e') ==> x:FV(e) --> x:FV(e[y:=e'])";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Auto_tac);
qed_spec_mp "FV_subst_lemma_3";


Goal "[|x~:FV(e); x~:FV(e')|] ==> x~:FV(e[y:=e'])";
by(cut_inst_tac [("e1","e"),("y1","y"),("x1","x"),("e'1","e'")] (FV_subst_lemma_1 RS impI) 1);
by(atac 1);
by(Fast_tac 1);
qed_spec_mp "FV_subst_lemma_4";


Goal "x~:FV(e[y:=e']) ==> x~:FV(e) | x=y";
by(cut_inst_tac [("e2","e"),("e'2","e'")] (FV_subst_lemma_2 RS impI RS impI) 1);
by(atac 1 THEN atac 1);
by(Fast_tac 1);
qed "FV_subst_lemma_5";


Goal "x:FV(e') ==> (Capt y e) Int FV(e') = {} --> y:FV(e) --> x:FV(e[y:=e'])";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1 THEN Fast_tac 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(case_tac "var=y" 1);
by(SELECT_GOAL Auto_tac 1);
by(ftac not_sym 1);
by(asm_full_simp_tac (simpset() delsimps[subst_Red]) 1);
by(etac disjE 1);
by(ALLGOALS (asm_full_simp_tac (simpset() delsimps[FV_Red])));
by(Force_tac 1);
by(Force_tac 1);
qed_spec_mp "FV_subst_lemma_6";


Goal "x:FV(e1) --> y:FV(e2) --> y:FV(e1[x:=e2]) | e1[x:=e2] = e1";
by(induct_tac "e1" 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
by(SELECT_GOAL Auto_tac 1);
by(SELECT_GOAL Auto_tac 1);
by(Auto_tac);
qed_spec_mp "FV_subst_lemma_7";


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 "x:BV(e[y:=e']) --> x:BV(e) | x:BV(e')";
by(induct_tac "e" 1);
by(Auto_tac);
qed_spec_mp "BV_subst_lemma_1";





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 1 1 THEN Fast_tac 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1 THEN datac FV_subst_lemma_3 1 1 THEN Fast_tac 1);
by(datac FV_subst_lemma_2 1 1 THEN Fast_tac 1);
by(datac FV_subst_lemma_2 1 1 THEN Fast_tac 1);
by(ALLGOALS (case_tac "x=y"));
by(rotate_tac ~1 2 THEN datac FV_subst_lemma_2 1 2 THEN Fast_tac 2);
by(rotate_tac ~1 3 THEN datac FV_subst_lemma_2 1 3 THEN Fast_tac 3);
by(ALLGOALS (Asm_full_simp_tac));
by(ALLGOALS (datac FV_subst_lemma_3 1));
by(ALLGOALS Fast_tac);
qed "Capt_in_capt_subst_1";


Goal "y:FV(e) -->(Capt y e) Int FV(e') = {} --> Capt x e' <= Capt x (e[y:=e'])";
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_2 1 1);
by(mp_tac 1);
by(rtac conjI 1);
by(rtac conjI 2);
by(Fast_tac 2);
by(ALLGOALS strip_tac);
by(Asm_simp_tac 1);
by(rtac conjI 1 THEN strip_tac 1);
by(Fast_tac 1);
by(rtac conjI 1 THEN strip_tac 1);
by(etac conjE 1 THEN etac FV_Capt_2 1);
by(strip_tac 1 THEN dtac FV_Capt_2 1);
by(Fast_tac 1);
by(datac Capt_Int_FV_lemma_1 1 1);
by(etac disjE 1 THEN REPEAT_DETERM (Fast_tac 1));
by(dtac Capt_induct_3 1 THEN etac conjE 1);
by(case_tac "var=y" 1);
by(ALLGOALS (asm_full_simp_tac (simpset() delsimps[Capt_Red])));
by(SELECT_GOAL Auto_tac 1);
by(case_tac "x=var" 1);
by(Asm_full_simp_tac 1);
by(case_tac "var:FV(e')" 1);
by(dtac FV_Capt_2 2 THEN Fast_tac 2);
by(Fast_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(ALLGOALS (etac disjE));
by(Asm_full_simp_tac 2 THEN Fast_tac 2);
by(Fast_tac 2);
by(Asm_full_simp_tac 2 THEN Fast_tac 2);
by(case_tac "y:FV(mlterm2)" 1);
by(Asm_full_simp_tac 1 THEN Fast_tac 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(Fast_tac 1);
by(rotate_tac ~1 1 THEN dtac FV_Capt_2 1);
by(Fast_tac 1);
qed_spec_mp "Capt_in_capt_subst_2";


Goal "[|(Capt x (Abs y e)) Int FV(e2) = {}; x~=y|] ==> (Abs y e)[x:=e2] = Abs y (e[x:=e2])";
by(case_tac "x:FV(e)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(Fast_tac 1);
by(Fast_tac 1);
qed "Capt_subst_enabling";


Goal "[|(Capt x (<Abs y e1> @ e2)) Int FV(e) = {}; x~=y|] ==> (<Abs y e1> @ e2)[x:=e] = <Abs y (e1[x:=e])> @ e2[x:=e]";
by(case_tac "x:FV(e1)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(Fast_tac 1);
by(Fast_tac 1);
qed "Capt_subst_enabling_2";


Goal "Capt x ((<Abs z e1> @ e2)[y:=e3]) Int A = {} ==> Capt x (e2[y:=e3]) Int A = {}";
by(Auto_tac); 
qed "Capt_subst_redex_1";


(* Substitution Lemma - Formulation 1 *)

Goal "[|Capt x e3 Int FV(e2) = {}; y~:FV(e2); y~=x|] ==> Capt y(e1) Int FV(e3) = {} --> Capt x e1 Int FV(e2) = {} --> Capt x (e1[y:=e3]) Int FV(e2) = {} --> e1[x:=e2][y:=e3[x:=e2]] = e1[y:=e3][x:=e2]";
by(induct_tac "e1" 1);
by(ALLGOALS strip_tac);
by(Asm_simp_tac 1);
by(full_simp_tac (simpset() delsimps[Capt_App]) 1);
by(REPEAT_DETERM (dtac Capt_induct_1 1));
by(Fast_tac 1);
by(case_tac "y=var" 1);
by(Asm_simp_tac 1);
by(ftac not_sym 1);
by(rotate_tac ~2 1);
by(ftac not_sym 1);
by(fatac Capt_induct_2 1 1);
by(case_tac "x=var" 1);
by(Asm_simp_tac 1);
by(strip_tac 1);
by(case_tac "y:FV(mlterm)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(ftac not_sym 1);
by(rotate_tac ~1 1);
by(fatac Capt_induct_2 1 1);
by(fatac Capt_subst_enabling 1 1);
by(rotate_tac 9 1);
by(fatac Capt_subst_enabling 1 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs,subst_Abs]) 1);
by(rotate_tac 6 1);
by(ftac Capt_induct_2 1);
by(rotate_tac ~4 1);
by(atac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(case_tac "x:FV(mlterm[y:=e3])" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(dtac FV_subst_lemma_1 1);
by(etac disjE 1);
by(contr_tac 2);
by(case_tac "y:FV(mlterm)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(mlterm)" 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(case_tac "y:FV(mlterm)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(mlterm[y:=e3])" 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(Asm_full_simp_tac 1);
by(case_tac "var:FV(e3)" 1);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(e3)" 1);
by(rotate_tac ~1 2);
by(Asm_full_simp_tac 2);
by(Asm_full_simp_tac 1);
by(dtac FV_subst_lemma_7 1);
by(rotate_tac ~1 1);
by(atac 1);
by(etac disjE 1);
by(contr_tac 1);
by(Asm_simp_tac 1);
(* Redex case *)
by(ftac Capt_subst_redex_1 1);
by(ftac Capt_induct_3 1);
by(rotate_tac 6 1 THEN ftac Capt_induct_3 1);
by(REPEAT_DETERM (etac conjE 1));
by(REPEAT_DETERM (mp_tac 1));
by(ftac not_sym 1);
by(case_tac "var=y" 1);
by(Asm_simp_tac 1);
by(mp_tac 1 THEN etac conjE 1);
by(case_tac "var=x" 1);
by(Asm_simp_tac 1);
by(strip_tac 1);
by(case_tac "y:FV(mlterm1)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(mp_tac 1 THEN etac conjE 1);
by(rotate_tac ~6 1 THEN ftac not_sym 1);
by(rotate_tac 3 1 THEN ftac not_sym 1);
by(stac Capt_subst_enabling_2 1);
by(atac 1 THEN atac 1);
by(case_tac "y:FV(mlterm1)" 1);
by(Asm_simp_tac 2);
by(mp_tac 1);
by(stac Capt_subst_enabling_2 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(atac 1);
by(stac Capt_subst_enabling_2 1);
by(atac 1 THEN atac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red]) 1);
by(rtac conjI 1 THEN ALLGOALS strip_tac);
by(defer_tac 1);
by(case_tac "x:FV(mlterm1)" 1);
by(mp_tac 1);
by(dtac FV_subst_lemma_1 1);
by(Fast_tac 1);
by(case_tac "x:FV(mlterm1[y:=e3])" 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1 THEN dtac FV_subst_lemma_1 1);
by(Fast_tac 1);
by(case_tac "x:FV(e3)" 1);
by(rotate_tac ~1 2 THEN Asm_full_simp_tac 2);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1 THEN dres_inst_tac [("y","y"),("e","mlterm1")] FV_subst_lemma_6 1);
by(Fast_tac 1);
by(atac 1);
by(contr_tac 1);
by(case_tac "x:FV(mlterm1[y:=e3])" 1);
by(rotate_tac ~1 2 THEN dtac FV_Capt_2 2);
by(Asm_full_simp_tac 2);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
qed_spec_mp "Substitution_Lemma_1";


(* Substitution Lemma - Formulation 2 *)

Goal "[|Capt x e3 Int FV(e2) = {}; y~=x|] ==> Capt y(e1) Int FV(e3) = {} --> Capt y e1 Int FV(e3[x:=e2]) = {} --> Capt x (e1[y:=e3]) Int FV(e2) = {} --> x~:FV(e1) --> e1[y:=e3[x:=e2]] = e1[y:=e3][x:=e2]";
by(induct_tac "e1" 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(full_simp_tac (simpset() delsimps[Capt_App]) 1);
by(REPEAT_DETERM (dtac Capt_induct_1 1));
by(Fast_tac 1);
by(case_tac "y=var" 1);
by(case_tac "x:FV(mlterm)" 1);
by(Asm_simp_tac 2);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(ftac not_sym 1);
by(rotate_tac ~2 1);
by(ftac not_sym 1);
by(fatac Capt_induct_2 1 1);
by(rotate_tac ~2 1);
by(ftac Capt_induct_2 1);
by(rotate_tac ~3 1);
by(atac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs,subst_Abs]) 1);
by(case_tac "x=var" 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(strip_tac 1);
by(case_tac "y:FV(mlterm)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(rotate_tac ~1 1);
by(ftac not_sym 1);
by(fatac Capt_subst_enabling 1 1);
by(rotate_tac 10 1);
by(fatac Capt_subst_enabling 1 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(rotate_tac 6 1);
by(fatac Capt_induct_2 1 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(strip_tac 1);
by(case_tac "x:FV(mlterm[y:=e3])" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(rotate_tac ~4 1);
by(Fast_tac 1);
(* Redex case *)
by(ftac not_sym 1);
by(ftac Capt_induct_3 1);
by(rotate_tac 5 1 THEN ftac Capt_induct_3 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red,subst_Red]) 1);
by(case_tac "var=y" 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1 THEN ftac not_sym 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Red,subst_Red]) 1);
by(case_tac "var=x" 1);
by(case_tac "x:FV(e3)" 1);
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1 THEN ftac not_sym 1);
by(stac Capt_subst_enabling_2 1);
by(atac 1 THEN atac 1);
by(case_tac "var:FV(e3)" 1);
by(Asm_full_simp_tac 1);
by(case_tac "var:FV(e3[x:=e2])" 1);
by(Asm_full_simp_tac 1);
by(case_tac "var:FV(e2)" 1);
by(ALLGOALS (asm_full_simp_tac (simpset() delsimps[Capt_Red])));
by(rotate_tac 4 1 THEN dtac Capt_induct_3 1);
by(Asm_full_simp_tac 1);
by(rotate_tac 4 1 THEN dtac Capt_induct_3 1);
by(Asm_full_simp_tac 1);
qed_spec_mp "Substitution_Lemma_2";