File AlphaZero.ML

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

- Properties of indexed alpha, alpha0, and alpha1, including equivalence of
  ->>iA0 and ->>iA1

*)

AddSIs i_alpha1.intrs;
AddSIs cl_ialpha1.intrs;
AddSIs cl_ialpha.intrs;


Goal "(s,y) ->iA t ==> (s,y) ->>iA t";
by(rtac rt_ialpha.trans 1);
by(atac 2);
by(rtac rt_ialpha.refl 1);
qed "rt_ialpha_base";


Goal "(s,y) ->>iA t ==> s ->>A t";
by(etac rt_ialpha.induct 1);
by(Simp_tac 1);
by(dtac alpha.strip 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rt_ialpha_in_alpha";


Goal "(s,y) ->>iA t ==> (Abs x s,y) ->>iA Abs x t";
by(etac rt_ialpha.induct 1);
by(rtac rt_ialpha.refl 1);
by(dres_inst_tac [("x","x")] i_alpha.aabs 1);
by(eatac rt_ialpha.trans 1 1);
qed "rt_ialpha_abs";


Goal "(s,y) ->>iA t ==> (s $ u,y) ->>iA (t $ u)";
by(etac rt_ialpha.induct 1);
by(rtac rt_ialpha.refl 1);
by(dres_inst_tac [("u","u")] i_alpha.aappL 1);
by(eatac rt_ialpha.trans 1 1);
qed "rt_ialpha_appL";


Goal "(s,y) ->>iA t ==> (u $ s,y) ->>iA (u $ t)";
by(etac rt_ialpha.induct 1);
by(rtac rt_ialpha.refl 1);
by(dres_inst_tac [("u","u")] i_alpha.aappR 1);
by(eatac rt_ialpha.trans 1 1);
qed "rt_ialpha_appR";


Goal "(t,y) ->>iA u ==> ALL s. (s,y) ->>iA t --> (s,y) ->>iA u";
by(etac rt_ialpha.induct 1);
by(ALLGOALS strip_tac);
by(atac 1);
by(etac allE 1);
by(mp_tac 1);
by(rotate_tac ~1 1);
by(eatac rt_ialpha.trans 1 1);
qed "rt_ialpha_bigtrans";


Goal "[|(s,y) ->>iA t; (t,y) ->>iA u|] ==> (s,y) ->>iA u";
by(rotate_tac ~1 1);
by(dtac rt_ialpha_bigtrans 1);
by(etac allE 1);
by(Fast_tac 1);
qed "rt_ialpha_bigtrans";


Goal "(s1,y) ->>iA t1 ==> (s2,y) ->>iA t2 --> (s1 $ s2,y) ->>iA (t1 $ t2)";
by(etac rt_ialpha.induct 1);
by(ALLGOALS strip_tac);
by(etac rt_ialpha_appR 1);
by(mp_tac 1);
by(dtac rt_ialpha_base 1);
by(etac rt_ialpha_bigtrans 1);
by(etac rt_ialpha_appL 1);
qed "rt_ialpha_doubleApp";


Goal "(s,y) ->iA t ==> FV(t) = FV(s)";
by(etac i_alpha.induct 1);
by(Auto_tac);
by(dtac FV_subst_lemma_1 1);
by(etac disjE 1);
by(atac 2);
by(Asm_full_simp_tac 1);
by(cut_inst_tac [("x","x"),("e","e"),("e'","Var y")] renaming_sanity_3 1);
by(Asm_simp_tac 1);
by(contr_tac 2);
by(Auto_tac);
by(eatac (FV_subst_lemma_2 RS mp RS mp) 1 1);
qed "ialpha_FV_lemma";


Goal "(s,y) ->>iA t ==> FV(s) = FV(t)";
by(etac rt_ialpha.induct 1);
by(Simp_tac 1);
by(dtac ialpha_FV_lemma 1);
by(Asm_full_simp_tac 1);
qed "rt_ialpha_FV_lemma";


Goal "Capt x e Int FV(e') = {} --> BV(e[x:=e']) = (if x:FV(e) then BV(e) Un BV(e') else BV(e))";
by(induct_tac "e" 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(dtac Capt_induct_1 1);
by(Auto_tac);
qed "BV_subst_lemma_2";


Goal "(s,y) ->iA t ==> BV(t) <= BV(s) Un {y}";
by(etac i_alpha.induct 1);
by(ALLGOALS Full_simp_tac);
by(Fast_tac 4);
by(Fast_tac 3);
by(Fast_tac 2);
by(etac sq_alpha_E2 1);
by(Asm_simp_tac 1);
by(stac (BV_subst_lemma_2 RS mp) 1);
by(Auto_tac);
qed "i_alpha_BV_lemma_1";


Goal "(s,y) ->iA1 t ==> (s,y) ->>iA t";
by(etac i_alpha1.induct 1);
by(rtac rt_ialpha.refl 1);
by(etac rt_ialpha_appR 4);
by(etac rt_ialpha_appL 3);
by(etac rt_ialpha_abs 2);
by(rtac rt_ialpha_base 1);
by(Auto_tac);
by(rtac sq_alpha.alpha 1);
by(fatac not_sym 1 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(Fast_tac 1);
qed "ialpha1_in_rt_ialpha";


Goal "(s,y) ->iA1 t ==> FV(s) = FV(t)";
by(dtac ialpha1_in_rt_ialpha 1);
by(etac rt_ialpha_FV_lemma 1);
qed "ialpha1_FV_lemma";


Goal "(s,y) ->iA1 t ==> BV(t) <= BV(s) Un {y}";
by(etac i_alpha1.induct 1);
by(Auto_tac);
by(cut_inst_tac [("x1","x"),("e1","e"),("e'1","Var y")] (BV_subst_lemma_2 RS mp) 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(Simp_tac 1);
by(Fast_tac 1);
by(case_tac "x:FV(e)" 1);
by(ALLGOALS Asm_full_simp_tac);
qed "ialpha1_BV_lemma";


Goal "(s,ys) ->>ciA t ==> FV(s) = FV(t)";
by(etac cl_ialpha.induct 1); 
by(Simp_tac 1);
by(dtac ialpha_FV_lemma 1);
by(Asm_simp_tac 1);
qed "cl_ialpha_FV_lemma";


Goal "(s,ys) ->>ciA t ==> BV(t) <= BV(s) Un set(ys)";
by(etac cl_ialpha.induct 1);
by(Fast_tac 1);
by(dtac i_alpha_BV_lemma_1 1);
by(Asm_full_simp_tac 1);
by(Blast_tac 1);
qed "cl_ialpha_BV_lemma";


(* Lemma showing equivalence of two transitivity notions on ->>iA1 *)
Goal "(t,ys) ->>iA1 u ==> ALL s y. (s,y) ->iA1 t --> (s,ys@[y]) ->>iA1 u";
by(etac cl_ialpha1.induct 1);
by(ALLGOALS strip_tac);
by(Asm_full_simp_tac 1);
by(Fast_tac 1);
by(etac allE 1);
by(etac allE 1);
by(mp_tac 1);
by(rotate_tac ~1 1);
by(datac cl_ialpha1.trans 1 1);
by(Auto_tac);
qed "cl_ialpha1_trans2";

(* User-friendly version of the above *)
Goal "[|(s,y) ->iA1 t; (t,ys) ->>iA1 u|] ==> (s,ys@[y]) ->>iA1 u";
by(dtac cl_ialpha1_trans2 1);
by(Auto_tac);
qed "cl_ialpha1_trans2";


(* Lemmas showing equivalence of our notions of alpha *)

val ialpha0_E1 = i_alpha0.mk_cases "(e,y) ->iA0 e'";
val ialpha0_E2 = i_alpha0.mk_cases "(Abs x e,y) ->iA0 Abs x e'";

Goal "(e1,y) ->iA1 e2 ==> e1~=e2 --> (e1,y) ->iA0 e2";
by(etac i_alpha1.induct 1);
by(Fast_tac 1);
by(ALLGOALS strip_tac);
by(rtac i_alpha0.ialpha0 1);
by(ALLGOALS Asm_full_simp_tac);
by(Fast_tac 2);
by(rtac i_alpha.index 1);
by(REPEAT_DETERM (etac conjE 1));
by(etac sq_alpha.alpha 1);
by(dtac (Capt_BV_lemma_1 RS mp) 1);
by(Fast_tac 1);
by(ALLGOALS (etac ialpha0_E1));
by(rtac i_alpha0.ialpha0 1);
by(etac i_alpha.aabs 1);
by(Force_tac 1);
by(rtac i_alpha0.ialpha0 1);
by(etac i_alpha.aappL 1);
by(Force_tac 1);
by(rtac i_alpha0.ialpha0 1);
by(etac i_alpha.aappR 1);
by(Force_tac 1);
qed "ialpha1_to_ialpha0";


Goal "(e,xs) ->>iA1 e' ==> e ->>A0 e'";
by(etac cl_ialpha1.induct 1);
by(rtac rtrancl_refl 1);
by(case_tac "e2=e3" 1);
by(Fast_tac 1);
by(datac (ialpha1_to_ialpha0 RS mp) 1 1);
by(dtac alpha0.strip 1);
by(eatac rtrancl_into_rtrancl 1 1);
qed "rt_ialpha1_to_rt_ialpha0";


Goal "e ->>A e' ==> EX xs. (e,xs) ->>ciA e'";
by(etac rtrancl_induct 1);
by(Fast_tac 1);
by(etac exE 1);
by(etac alpha_E 1);
by(datac cl_ialpha.trans 1 1);
by(Fast_tac 1);
qed "rt_alpha_to_rt_ialpha";


(* Variable-substitutivity on ->iA1 *)
Goal "(e,z) ->iA1 e' ==> y~=z --> y~:Capt x e --> (e[x:=Var y],z) ->iA1 e'[x:=Var y]";
by(etac i_alpha1.induct 1);
by(ALLGOALS strip_tac);
by(Asm_simp_tac 1);
by(Fast_tac 1);
by(Asm_full_simp_tac 4);
by(etac i_alpha1.appR 4);
by(Asm_full_simp_tac 3);
by(etac i_alpha1.appL 3);
by(REPEAT (etac conjE 4));
by(dres_inst_tac [("z","y"),("x","x")] BV_var_subst_lemma_1 4);
by(ftac not_sym 4);
by(datac FV_var_subst_lemma_1 1 4);
by(Fast_tac 4);
by(REPEAT (etac conjE 3));
by(dres_inst_tac [("z","y"),("x","x")] BV_var_subst_lemma_1 3);
by(ftac not_sym 3);
by(datac FV_var_subst_lemma_1 1 3);
by(Fast_tac 3);
by(case_tac "x=xa" 2);
by(Asm_full_simp_tac 2);
by(eatac i_alpha1.abs 1 2);
by(Asm_full_simp_tac 2);
by(Auto_tac);
by(case_tac "x:FV(e)" 4);
by(Asm_full_simp_tac 5);
by(rotate_tac ~1 4);
by(Asm_full_simp_tac 4);
by(stac Substitution_Lemma_4 1);
by(atac 1);
by(atac 1);
by(Asm_simp_tac 1);
by(rtac i_alpha1.contr 1);
by(dres_inst_tac [("z","y"),("x","x")] BV_var_subst_lemma_1 1);
by(dres_inst_tac [("z","y"),("x","x")] FV_var_subst_lemma_1 1);
by(atac 1);
by(Force_tac 1);
by(cut_inst_tac [("x","x"),("e","e"),("e'","Var ya")] renaming_sanity_3 1);
by(Asm_simp_tac 1);
by(fatac not_sym 1 1);
by(cut_inst_tac [("x","x"),("e","e")] capt_in_bound_var 1);
by(Asm_simp_tac 1);
by(Fast_tac 1);
by(Asm_simp_tac 1);
by(rtac i_alpha1.contr 1);
by(Force_tac 1);
by(case_tac "x=y" 1);
by(Asm_simp_tac 1);
by(rtac i_alpha1.contr 1);
by(Asm_simp_tac 1);
by(case_tac "x:FV(e)" 1);
by(Asm_full_simp_tac 1);
by(rotate_tac ~1 1);
by(dres_inst_tac [("z","ya"),("x","y")] FV_var_subst_lemma_1 1);
by(fatac not_sym 1 1);
by(Asm_simp_tac 1);
by(rtac i_alpha1.contr 1);
by(Asm_simp_tac 1);
qed "ialpha1_var_subst";