File Lambda.ML

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

- Proposition of Renaming Sanity (plus auxiliary lemma)
- Proof of _[_:=_] = _<_:=_> when substitution is enabled
- plus a host of useful lemmas linking the notions of capturing and free 
  variables in a term under substitution

*)


(* Proposition of Renaming Sanity and lemmas *)

Goal "y:(Capt x e) --> x:FV(e)"; 
by(induct_tac "e" 1);
by(Auto_tac);
qed "aux_renaming_lemma_1";
Addsimps [aux_renaming_lemma_1];


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 "renaming_sanity_2";


Goal "((x~:FV(e')) & ((Capt x e) Int FV(e')) = {}) --> (x~:FV(e[x:=e']))";
by(induct_tac "e" 1);
by(Auto_tac);
qed "renaming_sanity_3";


(* the more user-friendly version of the above *)
Goal "[|x~:FV(e'); ((Capt x e) Int FV(e')) = {}|] ==> x~:FV(e[x:=e'])";
by(rtac (renaming_sanity_3 RS mp) 1);
by(Fast_tac 1);
qed "renaming_sanity_3";


Goal "(y~:FV(e)) --> (e[x:=Var y][y:=Var x] = e)";
by(induct_tac "e" 1);
by(Auto_tac);
qed "renaming_sanity_4";


Addsimps[renaming_sanity_1, renaming_sanity_2];


(* Some useful Capt / FV / substitution - type lemmas *)

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


Goal "[|A-{x} <= B-{x}; y:A; x~=y|] ==> y:B";
by(Blast_tac 1);
qed "subset_lemma_2";


Goal "y~:FV(e) --> Capt y e = {}";
by(induct_tac "e" 1);
by(ALLGOALS Full_simp_tac);
by(Fast_tac 1);
qed "Capt_FV_lemma_1";


Goal "y~:BV(e) --> y~:Capt x e";
by(induct_tac "e" 1);
by(Auto_tac);
qed "Capt_BV_lemma_1";


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


Goal "x:FV(e[y:=e']) ==> x:FV(e') | x:FV(e)";
by(rtac mp 1);
by(atac 2);
by(induct_tac "e" 1);
by(Auto_tac);
qed "FV_subst_lemma_1";


Goal "x:FV(e) --> x~=y --> x:FV(e[y:=e'])";
by(induct_tac "e" 1);
by(Auto_tac);
qed "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 "FV_subst_lemma_3";


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(Auto_tac);
qed "FV_subst_lemma_4";


Goal "A --> B --> C ==> ~C --> ~A | ~B";
by(Blast_tac 1);
qed "special_contrapositive";


Goal "x~:FV(e[y:=e']) ==> x~:FV(e) | x=y";
by(cut_facts_tac [(FV_subst_lemma_2 RS special_contrapositive)] 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(Auto_tac);
qed "FV_subst_lemma_6";


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


Goal "x:BV(e[y:=e']) ==> x:BV(e) | x:BV(e')";
by(rtac mp 1);
by(atac 2);
by(thin_tac "x:BV(e[y:=e'])" 1);
by(induct_tac "e" 1);
by(Auto_tac);
qed "BV_subst_lemma_1";


Goal "x~:FV(e) & x~:FV(e') --> x~:FV(e[y:=e'])";
by(induct_tac "e" 1);
by(Asm_simp_tac 1);
by(Asm_simp_tac 1);
by(strip_tac 1);
by(Simp_tac 1);
by(resolve_tac [conjI] 1);
by(resolve_tac [conjI] 2);
by(ALLGOALS strip_tac);
by(Auto_tac);
qed "FV_lemma_1";


Goal "[|y~:FV(e); y~=z|] ==> y~:FV(e[x:=Var z])";
by(rtac (FV_lemma_1 RS mp) 1);
by(Asm_simp_tac 1);
qed "FV_var_subst_lemma_1";


Goal "y~:BV(e) ==> y~:BV(e[x:=Var z])";
by(rtac mp 1);
by(atac 2);
by(thin_tac "y~:BV(e)" 1);
by(induct_tac "e" 1);
by(Auto_tac);
qed "BV_var_subst_lemma_1";


(* Induction principles for the (parallel-) beta side condition *)


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 "(Capt x (e1 $ e2) Un A) Int B = {} ==> (Capt x e1 Un A) Int B = {} & (Capt x e2 Un A) Int B = {}";
by(Auto_tac);
qed "Capt_induct_2";


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


Goal "[|y~=x; (Capt x (Abs y e) Un A) Int B = {} |] ==> (Capt x e Un A) Int B = {}";
by(dtac not_sym 1);
by(Asm_full_simp_tac 1);
by(case_tac "x:FV(e)" 1);
by(ALLGOALS Asm_full_simp_tac);
by(Fast_tac 1);
by(asm_simp_tac (simpset() addsimps[Capt_FV_lemma_1]) 1);
qed "Capt_induct_4";


Goal "[|Capt x (Abs y (e1 $ e2)) Int A = {}; y~=x|] ==> Capt x (Abs y e1) Int A = {} & Capt x (Abs y e2) Int A = {}";
by(Auto_tac);
qed "Capt_induct_5";


Goal "[|Capt x (Abs y (Abs z e)) Int A = {}; y~=x; z~=x |] ==> Capt x (Abs y e) Int A = {}";
by(Auto_tac);
qed "Capt_induct_6";


(* Proof of "sharp" = "normal" substitution under suitable conditions *)


Goal "(Capt x e1) Int FV(e2) = {} ==> e1[x:=e2] = e1<x:=e2>";
by(rtac mp 1);
by(atac 2);
by(induct_tac "e1" 1);
by(ALLGOALS strip_tac);
by(ALLGOALS Simp_tac);
by(dtac Capt_induct_1 1);
by(Fast_tac 1);
by(rtac conjI 1);
by(ALLGOALS strip_tac);
by(ALLGOALS (fatac Capt_induct_3 1));
by(ALLGOALS (mp_tac));
by(atac 1);
by(dtac not_sym 1);
by(case_tac "x:FV(lterm)" 1);
by(Auto_tac);
qed "subst_equivalence";