File ExistsBCF.ML

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

- Proof that any term can be alpha0-reduced to a BCF

*)


Goal "(s,ys) ->>iA1 t ==> FV(s) = FV(t)";
by(etac cl_ialpha1.induct 1);
by(Simp_tac 1);
by(dtac ialpha1_FV_lemma 1);
by(Asm_full_simp_tac 1);
qed "cl_ialpha1_FV_lemma";


Goal "(s,ys) ->>iA1 t ==> BV(t) <= BV(s) Un set(ys)";
by(etac cl_ialpha1.induct 1);
by(Fast_tac 1);
by(dtac ialpha1_BV_lemma 1);
by(Force_tac 1);
qed "cl_ialpha1_BV_lemma";


Goal "(e,xs) ->>iA1 e' ==> x~:set(xs) --> (Abs x e,xs) ->>iA1 Abs x e'";
by(etac cl_ialpha1.induct 1);
by(Fast_tac 1);
by(strip_tac 1);
by(Asm_full_simp_tac 1);
by(etac conjE 1);
by(datac i_alpha1.abs 1 1);
by(eatac cl_ialpha1.trans 1 1);
qed "cl_ialpha1_abs";


Goal "(e,xs) ->>iA1 e' ==> y~:set(xs) --> y~:BV(e) --> (e[x:=Var y],xs) ->>iA1 e'[x:=Var y]";
by(etac cl_ialpha1.induct 1);
by(Fast_tac 1);
by(strip_tac 1);
by(Asm_full_simp_tac 1);
by(etac conjE 1);
by(datac (ialpha1_var_subst RS mp RS mp) 1 1);
by(dtac cl_ialpha1_BV_lemma 1);
by(rtac (Capt_BV_lemma_1 RS mp) 1);
by(Fast_tac 1);
by(eatac cl_ialpha1.trans 1 1);
qed "cl_ialpha1_var_subst";


Goal "BV(e[x:=Var y]) = BV(e)";
by(induct_tac "e" 1);
by(Auto_tac);
qed "BV_var_subst";
Addsimps[BV_var_subst];


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


Goal "x~=y ==> FV(e[x:=Var y]) <= FV(e) Un {y}";
by(induct_tac "e" 1);
by(Auto_tac);
qed "FV_var_subst";


Goal "[|(ALL z. z mem zs --> z ~: FV(Abs x e1) & z~:BV(Abs x e1)); zs=y#ys|] ==> ALL z. z mem ys --> z ~: BV e1 & z ~: FV e1";
by(strip_tac 1);
by(Asm_full_simp_tac 1);
by(eres_inst_tac [("x","z")] allE 1);
by(case_tac "y=z" 1);
by(Auto_tac);
qed "EBCF_aux_1";


Goal "ALL m xs. length xs = n + m --> (EX ys zs. xs = ys @ zs & length(ys) = n & length(zs) = m)";
by(induct_tac "n" 1); 
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(strip_tac 1);
by(asm_full_simp_tac (simpset() addsimps[length_Suc_conv]) 1);
by(REPEAT_DETERM (etac exE 1));
by(etac conjE 1);
by(REPEAT_DETERM (etac allE 1));
by(mp_tac 1);
by(REPEAT_DETERM (etac exE 1));
by(REPEAT_DETERM (etac conjE 1));
by(res_inst_tac [("x","y#ysa")] exI 1);
by(res_inst_tac [("x","zs")] exI 1);
by(rtac conjI 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1);
by(atac 2);
by(res_inst_tac [("x","y")] exI 1);
by(res_inst_tac [("x","ysa")] exI 1);
by(Asm_simp_tac 1);
qed "EBCF_aux_2";


Goal "length xs = n + m ==> (EX ys zs. xs = ys @ zs & length(ys) = n & length(zs) = m)";
by(asm_full_simp_tac (simpset() addsimps[EBCF_aux_2]) 1);
qed "EBCF_aux_3";


Goal "ALL x. x mem ys@zs --> P x ==> (ALL x. x mem ys --> P x) & (ALL x. x mem zs --> P x)";
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
qed "EBCF_aux_4";


Goal "uniqlist(ys@zs) --> uniqlist(ys) & uniqlist(zs)";
by(induct_tac "ys" 1);
by(Asm_full_simp_tac 1);
by(strip_tac 1);
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
qed "uniqlist_property_1";


Goal "uniqlist(ys@zs) --> set(ys) Int set(zs) = {}";
by(induct_tac "ys" 1);
by(Simp_tac 1);
by(strip_tac 1);
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
by(Fast_tac 1);
qed "uniqlist_property_2";


Goal "(ALL x. x mem ys --> x~:FV(e1) & x~:FV(e2) & P x) --> FV(e1) Int set(ys) = {} & FV(e2) Int set(ys) = {}";
by(induct_tac "ys" 1);
by(Simp_tac 1);
by(strip_tac 1);
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
by(Auto_tac);
qed "EBCF_aux_5";


Goal "ALL x. x mem y#ys --> P x ==> (ALL x. x mem ys --> P x) & P y";
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
qed "all_list_induct_1";


Goal "(e1,xs) ->>iA1 e1' ==> ALL e2. (ALL x. x mem xs --> x~:(BV(e2) Un FV(e2))) --> (e1 $ e2,xs) ->>iA1 (e1' $ e2)";
by(etac cl_ialpha1.induct 1);
by(ALLGOALS strip_tac);
by(rtac cl_ialpha1.refl 1);
by(dtac all_list_induct_1 1);
by(etac conjE 1);
by(etac allE 1);
by(mp_tac 1);
by(datac i_alpha1.appL 1 1);
by(eatac cl_ialpha1.trans 1 1);
qed "cl_ialpha1_appL";


Goal "[|(e1,xs) ->>iA1 e1'; ALL x. x mem xs --> x~:(BV(e2) Un FV(e2))|] ==> (e1 $ e2,xs) ->>iA1 (e1' $ e2)";
by(asm_full_simp_tac (simpset() addsimps[cl_ialpha1_appL]) 1);
qed "cl_ialpha1_appL";


Goal "(e1,xs) ->>iA1 e1' ==> ALL e2. (ALL x. x mem xs --> x~:(BV(e2) Un FV(e2))) --> (e2 $ e1,xs) ->>iA1 (e2 $ e1')";
by(etac cl_ialpha1.induct 1);
by(ALLGOALS strip_tac);
by(rtac cl_ialpha1.refl 1);
by(dtac all_list_induct_1 1);
by(etac conjE 1);
by(etac allE 1);
by(mp_tac 1);
by(datac i_alpha1.appR 1 1);
by(eatac cl_ialpha1.trans 1 1);
qed "cl_ialpha1_appR";


Goal "[|(e1,xs) ->>iA1 e1'; ALL x. x mem xs --> x~:(BV(e2) Un FV(e2))|] ==> (e2 $ e1,xs) ->>iA1 (e2 $ e1')";
by(asm_full_simp_tac (simpset() addsimps[cl_ialpha1_appR]) 1);
qed "cl_ialpha1_appR";


Goal "(e2,ys) ->>iA1 e3 ==> ALL e1 xs. (e1,xs) ->>iA1 e2 --> (e1,ys@xs) ->>iA1 e3";
by(etac cl_ialpha1.induct 1);
by(ALLGOALS strip_tac);
by(Simp_tac 1);
by(REPEAT_DETERM (etac allE 1));
by(mp_tac 1);
by(Simp_tac 1);
by(eatac cl_ialpha1.trans 1 1);
qed "cl_ialpha1_bigtrans";


Goal "[|(e1,xs) ->>iA1 e2; (e2,ys) ->>iA1 e3|] ==> (e1,ys@xs) ->>iA1 e3";
by(asm_full_simp_tac (simpset() addsimps[cl_ialpha1_bigtrans]) 1);
qed "cl_ialpha1_bigtrans";


Goal "[|(e1,xs) ->>iA1 e1'; ALL x. x mem xs --> x~:(BV(e2) Un FV(e2)); (e2,ys) ->>iA1 e2'; ALL y. y mem ys --> y~:(BV(e1') Un FV(e1'))|] ==> (e1 $ e2, ys@xs) ->>iA1 (e1' $ e2')";
by(datac cl_ialpha1_appL 1 1);
by(rotate_tac 1 1);
by(datac cl_ialpha1_appR 1 1);
by(eatac cl_ialpha1_bigtrans 1 1);
qed "cl_ialpha1_doubleApp";


(* Key to existence of alpha0-rewrite sequence to a BCF *)
Goalw [BCF] "ALL xs. lambdas(e1) = length(xs) --> uniqlist(xs) --> (ALL x. x mem xs --> x~:FV(e1) Un BV(e1)) --> (EX e2. (e1,rev xs) ->>iA1 e2 & BCF(e2) & BV(e2) = set(xs))";
by(induct_tac "e1" 1);
by(ALLGOALS strip_tac);
(* Variable case *)
by(res_inst_tac [("x","Var var")] exI 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(defer_tac 1);
(* Abstraction case; first extract induction hypothesis *)
by(dtac sym 1);
by(asm_full_simp_tac (simpset() addsimps[length_Suc_conv] delsimps[FV_Abs,BV_Abs]) 1);
by(REPEAT_DETERM (etac exE 1));
by(etac conjE 1);
by(fatac EBCF_aux_1 1 1);
by(rotate_tac ~2 1);
by(dtac sym 1);
by(rotate_tac 1 1);
by(etac allE 1);
by(mp_tac 1);
by(ftac list_theory_4 1);
by(etac allE 1);
by(mp_tac 1);
by(Asm_full_simp_tac 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
(* Now apply contraction rule *)
by(res_inst_tac [("x","Abs y (e2[var:=Var y])")] exI 1);
by(rtac conjI 1);
by(dtac (list_theory_3 RS mp) 1);
by(dres_inst_tac [("x2","var")] (cl_ialpha1_var_subst RS mp RS mp) 1);
by(Asm_simp_tac 1);
by(atac 1);
by(dres_inst_tac [("x","y")] cl_ialpha1_abs 1);
by(Asm_full_simp_tac 1);
by(rtac cl_ialpha1_trans2 1);
by(atac 2);
by(rtac i_alpha1.contr 1);
by(Asm_full_simp_tac 1);
(* ... and show that the resulting term is a BCF *)
by(ftac cl_ialpha1_BV_lemma 1);
by(ftac cl_ialpha1_FV_lemma 1);
by(Asm_full_simp_tac 1);
by(rtac conjI 1);
by(etac (UB_var_subst RS mp) 1);
by(rtac conjI 1);
by(datac (list_theory_3 RS mp) 1 1);
by(cut_inst_tac [("x","var"),("y","y"),("e","e2")] FV_var_subst 1);
by(fatac not_sym 1 1);
by(Fast_tac 1);
(* Application case; first extract dual induction hypotheses *)
by(Asm_full_simp_tac 1);
by(dtac sym 1);
by(dtac EBCF_aux_3 1);
by(REPEAT_DETERM (etac exE 1));
by(REPEAT_DETERM (etac conjE 1));
by(rotate_tac ~2 1);
by(dtac sym 1);
by(dtac sym 1);
by(etac allE 1);
by(mp_tac 1);
by(etac allE 1);
by(mp_tac 1);
by(Asm_full_simp_tac 1);
by(ftac (uniqlist_property_1 RS mp) 1);
by(etac conjE 1);
by(REPEAT_DETERM (mp_tac 1));
by(dtac EBCF_aux_4 1);
by(etac conjE 1);
by(Auto_tac);
(* Split into two subgoals *)
by(res_inst_tac [("x","e2 $ e2a")] exI 1);
by(rtac conjI 1);
by(defer_tac 1);
(* Show that the given reduct is a BCF *)
by(dtac (uniqlist_property_2 RS mp) 1);
by(dtac cl_ialpha1_FV_lemma 1);
by(dtac cl_ialpha1_FV_lemma 1);
by(dtac (EBCF_aux_5 RS mp) 1);
by(dtac (EBCF_aux_5 RS mp) 1);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
(* and finally show that the given alpha0 transition is valid *)
by(ftac cl_ialpha1_FV_lemma 1);
by(etac cl_ialpha1_doubleApp 1);
by(atac 2);
by(ALLGOALS strip_tac);
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
by(dtac (uniqlist_property_2 RS mp) 1);
by(asm_full_simp_tac (simpset() addsimps[set_mem_eq]) 1);
by(Fast_tac 1);
qed "key_to_BCF_existence";


(* EXISTENCE OF BCF VIA ALPHA0-REWRITE SEQUENCE *)
Goal "EX e2. e1 ->>A0 e2 & BCF(e2)";
by(cut_inst_tac [("e1.0","e1")] key_to_BCF_existence 1);
by(cut_inst_tac [("n","lambdas(e1)"),("e","e1"),("ys","[]")] exists_suitable_list 1);
by(etac exE 1);
by(REPEAT_DETERM (etac conjE 1));
by(dtac sym 1);
by(etac allE 1);
by(mp_tac 1);
by(Asm_full_simp_tac 1);
by(etac exE 1);
by(res_inst_tac [("x","e2")] exI 1);
by(etac conjE 1);
by(dtac rt_ialpha1_to_rt_ialpha0 1);
by(Fast_tac 1);
qed "ExistsBCF";