File Included.ML

Addsimps [elems_def,In_def,apply_cons,emptyl_def,apply_pair,dom_pair,elems_dom,cons_dom,emptyl_dom,listof_def,natof_def,setof_def];

Addsimps [substp_equal];
Addsimps [substp_refsto_point];
use "windowtac3.ML";

Addsimps [neq_Nil_conv];

Delsimps [refsto_assume_def,refeq_assume_def];
Delsimps [refsto_pcmd_def,refeq_pcmd_def];

Goal "entails A (B <=> C) ==> env p ass A ||- spec(B => D) [=] spec(C => D)";
by (rtac equiv_spec 1);
by (Asm_full_simp_tac 1);
qed "equiv_implication_spec";

Goal "entails (isNat(varT ''X'') && isNat(varT ''H'') && isList(varT ''T'')) ((relT ''In'' [varT ''X'', funT ''elems'' [funT ''cons'' [varT ''H'',varT ''T'']]]) <=> ((varT ''X'' == varT ''H'') || (relT ''In'' [varT ''X'', funT ''elems'' [varT ''T'']])))";
by (Simp_tac 1);
by (Auto_tac);
qed "In_simp";

Goal "entails P ((A && (B || C)) <=> ((A && B) || (A && C)))";
by (Auto_tac);
qed "distrib_land_over_lor";

Goal "entails P (((A || B) => C ) <=> ((A => C) && (B => C)))";
by (Auto_tac);
qed "gregs_rule"; 

Goal "(''W'') :- exists ''U'' (exists ''V'' (spec(varT ''W'' == funT ''pair'' [varT ''U'', varT ''V'']) sand (assert(isList(varT ''U'')) sand assert(isList(varT ''V''))) sand spec(pall ''X'' ((isNat(varT ''X'') && relT ''In'' [varT ''X'', funT ''elems'' [varT ''U'']]) => relT ''In'' [varT ''X'', funT ''elems'' [varT ''V'']])))) prefsto(p) ?x";
by (trans_inst_tac [("pid","Included"),("V","''W''"),("y","''Y''")] intro_recursion);
by (asm_full_simp_tac (simpset () addsimps [pcmd_apply]) 1);
by (optac [1]);
by (optac [1]);
by (optac [2]);
by (optac [1]);
by (optac [2]);
by (trans_inst_tac [("B","((pex ''H'' (pex ''T'' (varT ''U'' == funT ''cons'' [varT ''H'', varT ''T'']))) || varT ''U'' == funT ''emptyl'' [])")] introduce_assumpt);
by (res_inst_tac [("x","natV y")] exI 1);
by (res_inst_tac [("x","listV ys")] exI 1);
by (Simp_tac 1);
by (transtac combine_assert);
by (close); 
by (transtac combine_assert);
by (close);
by (optac [2]);
by (trans_inst_tac [("B","varT ''U'' == funT ''emptyl'' [] || (pex ''H'' (pex ''T'' (varT ''U'' == funT ''cons'' [varT ''H'', varT ''T''])))")] introduce_spec);
by (optac [1]);
by (transtac lift_por);
by (close);
by (transtac right_distribute_pand_over_por);
by (optac [2]);
by (optac [1]);
by (transtac lift_exists);
by (optac [1]);
by (transtac lift_exists);
by (close);
by (close);
by (transtac expand_scope_exists);
by (close);
by (optac [1]);
by (transtac pand_to_sand);
by (optac [2]);
by (trans_inst_tac [("Q","ptrue")] equiv_spec);
by (close);
by (close);
by (optac [2]);
by (optac [1]);
by (transtac expand_scope_exists);
by (optac [1]);
by (transtac pand_to_sand);
by (optac [2]);
by (trans_inst_tac [("Q","pall ''X'' ((isNat (varT ''X'') && (relT ''In'' [varT ''X'', funT ''elems'' [funT ''cons'' [varT ''H'', varT ''T'']]])) => relT ''In'' [varT ''X'', funT ''elems'' [varT ''V'']])")] equiv_spec);
by (trans_inst_tac [("B","isNat(varT ''H'')")] introduce_assumpt);
by (trans_inst_tac [("B","isList(varT ''T'')")] introduce_assumpt);
by (optac [2]);
by (optac [2]);
by (transtac lift_forall);
by (optac [1]);
by (trans_inst_tac [("C","isNat (varT ''X'') && ((varT ''X'' == varT ''H'') || (relT ''In'' [varT ''X'', funT ''elems'' [varT ''T'']]))")] equiv_implication_spec);
by (transtac equiv_implication_spec);
by (rtac distrib_land_over_lor 1);
by (transtac equiv_spec);
by (rtac gregs_rule 1);
by (transtac lift_pand);
by (close);


by (transtac forall_distrib); 
by (transtac pand_to_sand);

by (optac [2]);
by (transtac lift_forall);
by (trans_inst_tac [("B","isList(varT ''V'')")] introduce_assumpt);
by (trans_inst_tac [("B","isList(varT ''T'')")] introduce_assumpt);
by (transtac sand_assoc);

by (trans_inst_tac [("B","funT ''pair'' [varT ''T'', varT ''V''] << varT ''W''")] introduce_assumpt);
by(Simp_tac 1);
by (trans_inst_tac [("V", "funT ''pair'' [varT ''T'', varT ''V'']")] forall_assumpt_refine);
by (rtac sand_right_cmono 1);
by (rtac exists_one_point_pair 1);
by (close);
by (optac [1]);
by (transtac forall_one_point);
by (Simp_tac 1);
by (REPEAT remove_assumpts_and_close);
qed "included";

Goal "env p ||- spec(P) pand spec(ptrue) [=] spec(P)";
by (simp_tac (simpset() addsimps [refeq_cmd_def,refeq_exec,PInt_def,dom_def]) 1);
by (rtac ext 1);
by (Auto_tac);
qed "spec_pand_true";