File Member.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 "(''W'') :- exists ''X'' (exists ''L'' (spec(varT ''W'' == funT ''pair'' [varT ''X'',varT ''L'']) sand assert(isNat(varT ''X'') && isList(varT ''L'')) sand spec(relT ''In'' [varT ''X'', funT ''elems'' [varT ''L'']]))) prefsto(empty) ?x";
by (trans_inst_tac [("pid","''Member''"),("V","''W''"),("y","''Y''")] intro_recursion2);
by (asm_full_simp_tac (simpset () addsimps []) 1);
by (optac [1,1,2,2]);
by (trans_inst_tac [("B","((pex ''H'' (pex ''T''  (varT ''L'' == funT ''cons'' [varT ''H'', varT ''T'']))) || varT ''L'' == funT ''emptyl'' [])")] introduce_spec);
by (res_inst_tac [("x","natV y")] exI 1);
by (res_inst_tac [("x","listV ys")] exI 1);
by (Simp_tac 1); 
by (optac [1]);
by (transtac lift_por);
by (transtac por_commute);
by (close);
by (transtac right_distribute_pand_over_por);
by (optac [1]);
by (transtac pand_to_sand);
by (close);
by (optac [1,2]);
by (trans_inst_tac [("Q", "pfalse")] equiv_spec);
by (close);
by (optac [2,1]);
by (transtac lift_exists);
by (optac [1]);
by (transtac lift_exists);
by (close);
by (close);
by (optac [2]);
by (transtac expand_scope_exists);
by (optac [1]);
by (transtac expand_scope_exists);
by (optac [1]);
by (transtac pand_to_sand);
by (optac [2]);
by (trans_inst_tac [("Q", "varT ''X'' == varT ''H'' || relT ''In'' [varT ''X'',funT ''elems'' [varT ''T'']]")] equiv_spec); 
by (transtac lift_por);
by (optac [2]);
by (trans_inst_tac [("B", "isNat (varT ''X'') && isList (varT ''T'')")] introduce_assumpt);
by (trans_inst_tac [("B", "funT ''pair'' [varT ''X'', varT ''T''] << varT ''W''")] introduce_assumpt);
by (trans_inst_tac [("V", "funT ''pair'' [varT ''X'', varT ''T'']"),("pid","''Member''")] use_environment);
by (simp_tac (simpset() addsimps [dom_def]) 1);
by (rtac sand_right_cmono 1);
by (rtac exists_one_point_pair 1);
by (REPEAT close);
qed "member_refine";