File SubstLemmas.ML

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

- Substitution Lemmas (plus auxiliaries)
*)


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(stac subst_equivalence 1);
by(dtac not_sym 1);
by(datac Capt_induct_3 2 1);
by(stac subst_equivalence 1);
by(atac 1);
by(rtac mp 1);
by(atac 2);
by(rotate_tac 2 1);
by(rtac mp 1);
by(atac 2);
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(ALLGOALS (ftac not_sym));
by(Asm_full_simp_tac 1);
by(datac Capt_induct_5 1 1);
by(Auto_tac);
qed "Capt_subst_enabling";


(* 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_3 1 1);
by(case_tac "x=var" 1);
by(Asm_simp_tac 1);
by(strip_tac 1);
by(case_tac "y:FV(lterm)" 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_3 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_3 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(lterm[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 1);
by(case_tac "y:FV(lterm)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(lterm)" 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(case_tac "y:FV(lterm)" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(lterm[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_4 RS mp RS mp) 1);
by(rotate_tac ~1 1);
by(atac 1);
by(etac disjE 1);
by(contr_tac 1);
by(Asm_simp_tac 1);
qed "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(lterm)" 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_3 1 1);
by(rotate_tac ~2 1);
by(ftac Capt_induct_3 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(lterm)" 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_3 1 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(strip_tac 1);
by(case_tac "x:FV(lterm[y:=e3])" 1);
by(Asm_simp_tac 2);
by(Asm_full_simp_tac 1);
by(rotate_tac ~4 1);
by(Fast_tac 1);
qed "Substitution_Lemma_2";


Goal "(A Un B) Int C = {} ==> A Int C = {} & B Int C = {}";
by(Blast_tac 1);
qed "disjoint_monotinicity";


Goal "[|x:FV(e'); x~=y|] ==> (Capt y e) Int FV(e') = {} --> y:FV(e) --> Capt x (e[y:=e']) = Capt x e Un Capt x e' Un Capt y e";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(Asm_full_simp_tac 1);
by(dtac disjoint_monotinicity 1);
by(Asm_full_simp_tac 1);
by(etac disjE 1);
by(case_tac "y:FV(lterm2)" 1);
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
by(ftac (Capt_FV_lemma_1 RS mp) 1);
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
by(case_tac "y:FV(lterm1)" 1);
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
by(ftac (Capt_FV_lemma_1 RS mp) 1);
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
by(asm_full_simp_tac (simpset() delsimps[Capt_Abs]) 1);
by(etac conjE 1);
by(fatac Capt_Int_FV_lemma_1 1 1);
by(rotate_tac ~2 1);
by(ftac not_sym 1);
by(rotate_tac ~1 1);
by(fatac Capt_induct_3 1 1);
by(mp_tac 1);
by(rtac conjI 1);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(contr_tac 2);
by(Fast_tac 2);
by(etac conjE 1);
by(Asm_simp_tac 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(rtac conjI 2);
by(ALLGOALS strip_tac);
by(rotate_tac ~2 2);
by(dtac (Capt_FV_lemma_1 RS mp) 2);
by(Asm_simp_tac 2);
by(thin_tac "x:FV(lterm)" 1);
by(thin_tac "x~:FV(lterm)" 2);
by(distinct_subgoals_tac);
by(case_tac "x=var" 1);
by(Asm_full_simp_tac 1);
by(etac conjI 1);
by(dtac FV_subst_lemma_6 1);
by(Fast_tac 1);
qed "Capt_subst_distribute";


(* Substitution Lemma - Formulation 3 *)

Goal "[|Capt x e Int A = {}; y~:FV(e); y~:BV(e); x~=y|] ==> Capt y (e[x:=Var y]) Int A = {}";
by(case_tac "x:FV(e)" 1);
by(dtac (Capt_FV_lemma_1 RS mp) 2);
by(Asm_simp_tac 2);
by(stac (Capt_subst_distribute RS mp RS mp) 1);
by(Simp_tac 1);
by(fatac not_sym 1 1);
by(atac 2);
by(dtac (Capt_BV_lemma_1 RS mp) 1);
by((Simp_tac 1) THEN (Fast_tac 1));
by(dtac (Capt_FV_lemma_1 RS mp) 1);
by(Asm_simp_tac 1);
qed "Capt_subst_var_lemma_1";


(* Substitution Lemma - Formulation 3 *)

Goal "[|Capt x e Int FV(e') = {}; y~:FV(e); y~:BV(e)|] ==> e[x:=Var y][y:=e'] = e[x:=e']";
by(case_tac "x=y" 1);
by(Asm_full_simp_tac 1);
by(stac (Substitution_Lemma_2 RS mp RS mp RS mp RS mp RS sym) 1);
by(ALLGOALS Asm_simp_tac);
by(dres_inst_tac [("x1","x")] (Capt_BV_lemma_1 RS mp) 1);
by(Fast_tac 1);
by(etac Capt_subst_var_lemma_1 1);
by(ALLGOALS atac);
qed "Substitution_Lemma_3";


(* Substitution Lemma - Formulation 4 *)

Goal "[|y~=z; x~=z; x~:FV(e')|] ==> e[x:=Var y][z:=e'] = e[z:=e'][x:=Var y]";
by(induct_tac "e" 1);
by(Asm_simp_tac 1);
by(Asm_simp_tac 1);
by(case_tac "var=x" 1);
by(Asm_simp_tac 1);
by(case_tac "var=z" 1);
by(Asm_simp_tac 1);
by(Asm_simp_tac 1);
qed "Substitution_Lemma_4";