File Execs.ML

Addsimps [refsto_exec,refeq_exec];  

Goal "id : {(C :: Ctx). ! p q. p refsto q \<longrightarrow> C(p) refsto C(q)}";
by (asm_full_simp_tac (simpset() addsimps [id_def]) 1);
qed "id_in_MCtx";

(*goal Execs.thy "exec p c : Exec2";
by (simp_tac (simpset() addsimps [Exec2_def]) 1);
by (induct_tac "c" 1);
by (simp_tac (simpset() addsimps [dom_def,Exec2_def]) 10); 
*)


goal Execs.thy "dom(exec p (assert A)) = {s. s <= bnds(A)}";
by (simp_tac (simpset() addsimps [dom_def]) 1);
qed "dom_assume";


goal Execs.thy "dom(exec p (c1 pand c2)) = dom(exec p c1) Int dom(exec p c2)";
by (simp_tac (simpset() addsimps [dom_PInt]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "dom_pand";



goal Execs.thy "dom(exec p (assert A)) = Pow {b. {b} : dom(exec p (assert A))}";
by (simp_tac (simpset() addsimps [dom_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "assume_property1";


val prems = goal Execs.thy "[| dom(exec p c1) = Pow {b . {b}: dom(exec p c1)}; dom(exec p c2) = Pow {b . {b}: dom(exec p c2)} |] ==> dom(exec p (c1 pand c2)) = Pow {b . {b}: dom(exec p (c1 pand c2))}";
by (cut_facts_tac prems 1);
by (simp_tac (simpset() addsimps []) 1);
by (eresolve_tac [ssubst] 1);
by (eresolve_tac [ssubst] 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "pand_property1";


(*
goal Execs.thy "! s: dom(exec p c). the ((exec p c)(s)) <= s";
by (induct_tac "c" 1);
by (simp_tac (simpset() addsimps [dom_def]) 2);
by (simp_tac (simpset() addsimps [dom_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps [dom_PInt]) 1);
by (resolve_tac [ballI] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsimps [PInt_def]) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps [dom_PUn]) 1);
by (resolve_tac [ballI] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [conjunct2] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (dresolve_tac [conjunct1] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsimps [PUn_def]) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "exec_property2";
*)


goal Execs.thy "dom(exec p (exists v c)) = {s. (unbind v s):dom(exec p c)}";
by (asm_full_simp_tac (simpset() addsimps [ex_def,dom_def,unbind_def]) 1);
qed "dom_exists";


goal Execs.thy "dom(exec p (Cmd.all v c)) = {s. (unbind v s):dom(exec p c)}";
by (simp_tac (simpset() addsimps [unbind_def,forall_def,dom_def]) 1);
qed "dom_all";


goal Execs.thy "dom(exec p abort) = {{}}";
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
qed "dom_abort";

goal Execs.thy "! s: dom(exec p c). the ((exec p c)(s)) <= s";
by (induct_tac "c" 1);
by (simp_tac (simpset() addsimps [dom_def]) 2);
by (simp_tac (simpset() addsimps [dom_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps [dom_PInt]) 1);
by (resolve_tac [ballI] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsimps [PInt_def]) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps [dom_PUn]) 1);
by (resolve_tac [ballI] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [conjunct2] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (dresolve_tac [conjunct1] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsimps [PUn_def]) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps []) 2);
by (asm_full_simp_tac (simpset() addsimps [ex_def,dom_def,unbind_def]) 2);
by (resolve_tac [allI] 2);
by (resolve_tac [impI] 2);
by (resolve_tac [subsetI] 2);
by (asm_full_simp_tac (simpset() addsimps []) 2);
by (asm_full_simp_tac (simpset() addsimps [forall_def,dom_def]) 2);
by (blast_tac (claset() addIs [] addEs []) 2);
by (asm_full_simp_tac (simpset() addsimps []) 2);
by (resolve_tac [ballI] 2);
by (Rewrite_subgoal_tac [dom_abort] 2);
by (asm_full_simp_tac (simpset() addsimps []) 2);
by (simp_tac (simpset() addsimps []) 1);
by (simp_tac (simpset() addsimps [dom_partcomp]) 1);
by (simp_tac (simpset() addsimps [partcomp_def]) 1);
by (strip_tac 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (dresolve_tac [bspec] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (cut_inst_tac [("x","(pexec (p(list := None)) (the (p list)) rterm)")] Rep_Exec 1);
by (asm_full_simp_tac (simpset() addsimps [Exec_def,dom_def]) 1);
qed "exec_property2";


Goal "((exec p c){}) = Some {}";
by (cut_inst_tac [("p","p"),("c","c")] exec_property2 1);
by (dres_inst_tac [("x","{}")] bspec 1);
by (cut_inst_tac [("p","p"),("c","c")] exec_property1 1);
by (eresolve_tac [ssubst] 1);
by (Blast_tac 1);
by (cut_inst_tac [("f", "exec p c"), ("a","{}")] some_the_equiv 1);
by (eresolve_tac [ssubst] 2);
by (Blast_tac 2);
by (cut_inst_tac [("p","p"),("c","c")] exec_property1 1);
by (eresolve_tac [ssubst] 1);
by (Blast_tac 1);
qed "exec_empty";