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";


Goal "[| 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 (auto_tac (claset(), simpset() addsimps [PInt_def,dom_def]));
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 "dom (exec p (spec P)) = UNIV";
by (auto_tac (claset(), simpset() addsimps [dom_def]));
qed "dom_spec";


Goal "dom (exec p (assert A)) = {s. s <= bnds(A)}";
by (auto_tac (claset(), simpset() addsimps [dom_def]));
qed "dom_assert";

Goal "dom (exec p (c1 pand c2)) = dom (exec p c1) Int dom (exec p c2)";
by (Simp_tac 1);
by (Blast_tac 1);
qed "dom_pand";

Goal "dom (exec p (c1 por c2)) = dom (exec p c1) Int dom (exec p c2)";
by (Simp_tac 1);
by (Blast_tac 1);
qed "dom_por";

Goal "dom (exec p fail) = UNIV";
by (auto_tac (claset(), simpset() addsimps [dom_def]));
qed "dom_fail";

Goal "[| x <= {y. P(y)}; x <= {y. Q(y)} |] ==> x <= {y. P(y) & Q(y)}";
by (Auto_tac);
qed "Collect_subset_conj";
 
(*
Goal "dom (exec p c) = Pow {b. {b} : dom (exec p c)}";
by (induct_tac "c" 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_pand,dom_por,dom_exists,dom_all,dom_abort,dom_spec]) 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_assert]) 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_pand,dom_por,dom_exists,dom_all,dom_abort,dom_spec]) 1);
by (etac ssubst 1);
by (etac ssubst 1);
by (Simp_tac 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_pand,dom_por,dom_exists,dom_all,dom_abort,dom_spec]) 1);
by (etac ssubst 1);
by (etac ssubst 1);
by (Simp_tac 1);
by (Blast_tac 1);
by (defer_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_pand,dom_por,dom_exists,dom_all,dom_abort,dom_spec]) 1);
by (etac ssubst 1);
by (simp_tac (simpset() addsimps [unbind_def,Pow_def]) 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_pand,dom_por,dom_exists,dom_all,dom_abort,dom_spec]) 1);
by (etac ssubst 1);
by (simp_tac (simpset() addsimps [unbind_def,Pow_def]) 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_fail]) 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_abort]) 1);
by (Blast_tac 1);
by (Simp_tac 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);
by (asm_full_simp_tac (simpset() addsimps [dom_partcomp]) 1);
by (rtac equalityI 1);
*)



goal Execs.thy "! s: dom(exec p c). the ((exec p c)(s)) <= s";
by (induct_tac "c" 1);
by (auto_tac (claset(), simpset() addsimps [PInt_def,PUn_def,dom_def,ex_def,forall_def,unbind_def,partcomp_def]));
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);
by (Auto_tac);
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 (rtac (exec_property1 RS 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 (rtac (exec_property1 RS ssubst) 1);
by (Auto_tac);
qed "exec_empty";

(*
Goal "! s: dom(exec p c). (exec p c)(s) = Some {b. b:s & ((exec p c)({b}) = Some {b})}";
by (induct_tac "c" 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_spec]) 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_assert]) 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
by (asm_full_simp_tac (HOL_basic_ss addsimps [dom_pand,PInt_def]) 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (rtac ballI 1);
by (rtac trans 1);
by (rtac PInt_def 1);

*)