File RefAssume.ML

section "PRELIMINARY DEFINITIONS";
(*
Addsimps [refsto_exec,refsto_cmd_def];
Delsimps [dom_def];

Goal "(env p ||- c1 [= c2) = (! b. {b}:dom(exec p c1) --> {b} : dom (exec p c2) & (exec p c1)({b}) = (exec p c2)({b}))";
by (rtac iffI 1);
by (asm_full_simp_tac (simpset () addsimps [dom_def]) 1);
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
by (cut_inst_tac [("p","p"),("c","c1")] exec_property1 1);
by (cut_inst_tac [("p","p"),("c","c2")] exec_property1 1);
by (eresolve_tac [ssubst] 1);
by (eresolve_tac [ssubst] 1);
by (resolve_tac [Pow_mono] 1);
by (resolve_tac [subsetI] 1);
by (Asm_full_simp_tac 1);
by (rtac ballI 1);
by (cut_inst_tac [("p","p"),("c","c1")] exec_property3 1);
by (cut_inst_tac [("p","p"),("c","c2")] exec_property3 1);
by (rotate_tac 1 1);
by (dresolve_tac [bspec] 1);
by (Asm_full_simp_tac 1);
by (dres_inst_tac [("x","s")] bspec 1);
by (eresolve_tac [ssubst] 2);
by (eresolve_tac [ssubst] 2);
by (Asm_full_simp_tac 2);
by (cut_inst_tac [("p","p"),("c","c1")] exec_property1 1);
by (cut_inst_tac [("p","p"),("c","c2")] exec_property1 1);
by (rotate_tac 3 1);
by (dresolve_tac [subst] 1);
by (rotate_tac 1 1);
by (assume_tac 1);
by (eresolve_tac [ssubst] 1);
by (Asm_full_simp_tac  1);
by (resolve_tac [subsetI] 1);
by (Asm_full_simp_tac  1);
by (dresolve_tac [subsetD] 1);
by (Asm_full_simp_tac  1);
by (Asm_full_simp_tac  1);
by (cut_inst_tac [("p","p"),("c","c1")] exec_property1 1);
by (rotate_tac 2 1);
by (dresolve_tac [subst] 1);
by (assume_tac 1);
by (Auto_tac);
by (dresolve_tac [subsetD] 1);
by (rotate_tac 2 1);
by (assume_tac 1);
by (Asm_full_simp_tac  1);
by (dres_inst_tac [("x","x")] spec 1);
by (dresolve_tac [mp] 1);
by (Asm_full_simp_tac  1);
by (Asm_full_simp_tac  1);
by (cut_inst_tac [("p","p"),("c","c1")] exec_property1 1);
by (rotate_tac 2 1);
by (dresolve_tac [subst] 1);
by (assume_tac 1);
by (Auto_tac);
by (dresolve_tac [subsetD] 1);
by (rotate_tac 2 1);
by (assume_tac 1);
by (Asm_full_simp_tac  1);
qed "refines_pointwise";
*)


Delsimps [refsto_exec,refsto_cmd_def];
Addsimps [refeq_assume_def,refsto_assume_def,bnds_def];


Goal "(env p ass A ||- c1 [= c2) = (! b. (evalp A b) & {b} : dom (exec p c1) --> (exec p c1)({b}) = (exec p c2)({b}))";
by (Asm_full_simp_tac  1);
by (rtac trans 1);
by (rtac refines_pointwise 1);
by (asm_full_simp_tac (simpset () addsimps [refsto_exec,refsto_cmd_def,dom_def,partcomp_def]) 1);
by (rtac iffI 1);
by (Asm_full_simp_tac 2);
by (rtac allI 1);
by (Asm_full_simp_tac 1);
qed "refsto_point_property";

section "Refinement relation properties";

Addsimps [entails_def];

Goal "[| env p ass A ||- S [=] T; env p ass A ||- T [=] U|] ==> env p ass A ||- S [=] U";
by (Asm_full_simp_tac 1);
qed "crefeq_trans";


Goal "[| env p ass A ||- S [= T; env p ass A ||- T [= U|] ==> env p ass A ||- S [= U";
by (Asm_full_simp_tac 1);
by (rtac refsto_trans 1);
by (Blast_tac 1);
by (Blast_tac 1);
qed "crefsto_trans";

Addsimps [refsto_exec,refsto_cmd_def];

Goal "env p ass A ||- c [= c";
by (Simp_tac 1);
qed "crefsto_reflex";

Addsimps [refeq_exec,refeq_cmd_def];

Goal "env p ass A ||- c [=] c";
by (Simp_tac 1);
qed "crefeq_reflex";

Goal "env p ass A ||- S [=] T ==> env p ass A ||- T [=] S";
by (Asm_full_simp_tac 1);
qed "crefeq_symm";

Goal "env p ass A ||- c1 [=] c2 ==> env p ass A ||- c1 [= c2";
by (Asm_full_simp_tac 1);
qed "crefeqD1";


Goal "env p ass A ||- c1 [=] c2 ==> env p ass A ||- c2 [= c1";
by (Asm_full_simp_tac 1);
qed "crefeqD2";


section "MONOTONICITY RULES";

Addsimps [PInt_def,dom_def];
Delsimps [entails_def];

Addsimps [refsto_point_property];
Delsimps [refsto_assume_def];
Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- c1 pand c3 [= c2 pand c3";
by (Auto_tac);
qed "pand_left_cmono";

Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- c3 pand c1 [= c3 pand c2";
by (Auto_tac);
qed "pand_right_cmono";

Addsimps [PUn_def];

Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- c3 por c1 [= c3 por c2";
by (Auto_tac);
qed "por_right_cmono";


Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- c1 por c3 [= c2 por c3";
by (Auto_tac);
qed "por_left_cmono";

Goal "[| env p ass A ||- S [= T; env p ass A ||- U [= V |] ==> env p ass A ||- S pand U [= T pand V";
by (Auto_tac);
qed "pand_cmono";


Delsimps [dom_def,PInt_def,PUn_def,partcomp_def];
Addsimps [dom_partcomp];
Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- c3 sand c1 [= c3 sand c2";
by (Asm_full_simp_tac 1);
by (strip_tac 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (cut_inst_tac [("c","c3"),("p","p")] exec_property2 1);
by (rotate_tac 4 1);
by (dres_inst_tac [("x","{b}")] bspec 1);
by (Asm_full_simp_tac 1);
by (dresolve_tac [single_subs_cases] 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (asm_full_simp_tac (simpset() addsimps [partcomp_def,dom_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [partcomp_def,dom_def,exec_empty]) 1);
qed "sand_right_cmono";


Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- c1 sand c3 [= c2 sand c3";
by (Asm_full_simp_tac 1);
by (strip_tac 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (cut_inst_tac [("c","c2"),("p","p")] exec_property2 1);
by (rotate_tac 4 1);
by (dres_inst_tac [("x","{b}")] bspec 1);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (dresolve_tac [single_subs_cases] 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (asm_full_simp_tac (simpset() addsimps [partcomp_def,dom_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [partcomp_def,dom_def,exec_empty]) 1);
qed "sand_left_cmono";

section "ASSUMPTION RULES";

Addsimps [dom_def,partcomp_def];

Delsimps [refsto_exec,refsto_cmd_def];

Goal "env p ass A && B ||- S [= T ==> env p ass A ||- assert B sand S [= assert B sand T";
by (Asm_full_simp_tac 1);
qed "assume_in_context";

Addsimps [entails_def];

Goal "entails A (B => C) ==> env p ass A ||- assert(B) [= assert(C)";
by (Auto_tac);
qed "weaken_assumpt";

Goal "entails A B ==> env p ass A ||- c [= assert(B) sand c";
by (Auto_tac);
qed "introduce_assumpt";




Addsimps [partcomp_def,dom_def];

Goal "env p ass B && A ||- c1 [= c2 ==> env p ass B ||- spec A sand c1 [= spec A sand c2";
by (Asm_full_simp_tac 1);
by (strip_tac 1);
by (cut_inst_tac [("P", "evalp A b")] excluded_middle 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (dres_inst_tac [("x","b")] spec 2); 
by (dresolve_tac [mp] 2);
by (Asm_full_simp_tac 2);
by (forw_inst_tac [("A","evalp A"), ("b","b")] single_int_collect 2);
by (forward_tac [subst] 2);
by (assume_tac 2);
by (eresolve_tac [ssubst] 2);
by (Blast_tac 2);
by (forw_inst_tac [("A","evalp A"), ("b","b")] not_single_int_collect 1);
by (eresolve_tac [ssubst] 1);
by (simp_tac (simpset() addsimps [exec_empty]) 1);
by (forw_inst_tac [("A","evalp A"), ("b","b")] single_int_collect 1);
by (Auto_tac);
qed "spec_in_cont";

Delsimps [refsto_exec,refeq_exec,refsto_cmd_def,refeq_cmd_def,partcomp_def,dom_def];
(*
Goal "entails A (P <=> Q) ==> env p ass A ||- spec(P) [=] spec(Q)";
by (Auto_tac);
qed "equiv_spec2";
*)
Addsimps [dom_def,partcomp_def];

Goal "env p ||- S [= T ==> env p ass ptrue ||- S [= T";
by (asm_full_simp_tac (simpset() addsimps [everywhere_def,refsto_exec,refsto_cmd_def]) 1);
qed "refsto_to_crefsto";

Delsimps [refsto_exec,refsto_cmd_def];
Addsimps [dom_def];

Goal "env p ass ptrue ||- S [= T ==> env p ||- S [= T";
by (asm_full_simp_tac (simpset () addsimps [refines_pointwise,dom_def]) 1);
qed "crefsto_to_refsto";

Addsimps [refeq_assume_def,refsto_assume_def,refeq_cmd_def,refeq_exec];
Delsimps [dom_def];




Delsimps [refeq_cmd_def,refeq_exec,refsto_exec,refsto_cmd_def,refsto_point_property];
Goal "[| env p ass A ||- c1 [= c2; env p ass A ||- c2 [= c1|] ==> env p ass A ||- c1 [=] c2";
by (Asm_full_simp_tac 1);
by (rtac refsto_antisymm 1);
by (Auto_tac);
qed "crefsto_antisymm";

Goal "(env p ass A ||- c1 [= c2 & env p ass A ||- c2 [= c1) = (env p ass A ||- c1 [=] c2)";
by (rtac iffI 1);
by (rtac crefsto_antisymm 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
by (rtac crefeqD1 1);
by (Asm_full_simp_tac 1);
by (rtac crefeqD2 1);
by (Asm_full_simp_tac 1);
qed "crefeq_simp";

Delsimps [refeq_assume_def,refsto_assume_def];

Goal "(env p ass A ||- c1 [=] c2) = (! b. evalp A b --> exec p c1 {b} = exec p c2 {b})";
by (rtac (sym RS trans) 1);
by (rtac crefeq_simp 1);
by (asm_full_simp_tac (simpset() addsimps [refsto_point_property]) 1);
by (rtac iffI 1);
by (strip_tac 1);
by (cut_inst_tac [("P","{b}:dom (exec p c1)")] excluded_middle 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (dresolve_tac [conjunct1] 2);
by (dres_inst_tac [("x","b")] spec 2);
by (Asm_full_simp_tac 2);
by (cut_inst_tac [("P","{b}:dom (exec p c2)")] excluded_middle 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (dresolve_tac [conjunct2] 2);
by (dres_inst_tac [("x","b")] spec 2);
by (Asm_full_simp_tac 2);
by (cut_inst_tac [("f","exec p c1"),("s","{b}")] apply_None 1);
by (assume_tac 1);
by (cut_inst_tac [("f","exec p c2"),("s","{b}")] apply_None 1);
by (assume_tac 1);
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
by (strip_tac 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "refeq_point_property";


Delsimps [refsto_assume_def];
Addsimps [refsto_point_property,refeq_point_property];
Goal "entails A (P <=> Q) ==> env p ass A ||- spec(P) [=] spec(Q)";
by (Auto_tac);
qed "equiv_spec";

Addsimps [refsto_point_property];

Delsimps [refsto_cmd_def,refsto_assume_def];
Delsimps [dom_def];
Addsimps [entails_def];
Goal "entails A B ==> env p ass A ||- c [=] spec(B) pand c";
by (asm_full_simp_tac (simpset() addsimps [dom_def,PInt_def]) 1);
by (Asm_full_simp_tac 1);
by (strip_tac 1);
by (cut_inst_tac [("p","p"),("c","c")] exec_property2 1);
by (dres_inst_tac [("x","{b}")] bspec 1);
by (asm_full_simp_tac (simpset() addsimps [dom_def,PInt_def]) 1);
by (dresolve_tac [single_subs_cases] 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (cut_inst_tac [("f", "exec p c"), ("a","{b}"),("b","{b}")] some_the_equiv 1);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (Asm_full_simp_tac  1);
by (dres_inst_tac [("x","b")]  spec 1);
by (dresolve_tac [mp] 1);
by (assume_tac 1);
by (dres_inst_tac [("A","evalp B"), ("b","b")] single_int_collect 1);
by (Asm_full_simp_tac 1);
by (cut_inst_tac [("f", "exec p c"), ("a","{b}"),("b","{}")] some_the_equiv 1);
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (Asm_full_simp_tac  1);
qed "introduce_spec";




Addsimps [if_eq_Some_simp];

Goal "env p ||- c1 [= c2 ==> env p ass A ||- c1 [= c2";
by (asm_full_simp_tac (simpset() addsimps [refines_pointwise]) 1);
qed "assume_context_intro";

Goal "env p ass A ||- c1 [= c2 ==> env p ||- spec(A) sand c1 [= spec(A) sand c2";
by (asm_full_simp_tac (simpset() addsimps [dom_def,refines_pointwise]) 1);
by (strip_tac 1);
by (cut_inst_tac [("P", "evalp A b")] excluded_middle 1); 
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (cut_inst_tac [("A", "evalp A"), ("b","b")] not_single_int_collect 1);
by (Asm_full_simp_tac 1);
by (cut_inst_tac [("A", "evalp A"), ("b","b")] single_int_collect 2);
by (Asm_full_simp_tac 2);
by (forward_tac [subst] 1);
by (rotate_tac 1 1);
by (assume_tac 1);
by (eresolve_tac [ssubst] 1);
by (asm_full_simp_tac (simpset() addsimps [exec_empty]) 1);
by (forward_tac [subst] 1);
by (rotate_tac 1 1);
by (assume_tac 1);
by (eresolve_tac [ssubst] 1);
by (rtac conjI 1);
by (Blast_tac 2);
by (dres_inst_tac [("x","b")] spec 1);
by (dresolve_tac [mp] 1);
by (Asm_full_simp_tac 1);
by (eresolve_tac [subst] 1);
by (Asm_full_simp_tac 1);
qed "spec_in_cont2";

Delsimps [refsto_point_property];
Addsimps [refsto_assume_def];

Goal "env p ass A ||- c1 [= c2 ==> env p ||- assert(A) sand c1 [= assert(A) sand c2";
by (Asm_full_simp_tac 1);
qed "assume_in_context2";


(*
Goal "env p ass A ||- c1 [= c2 ==> env p ass A ||- exists V c1 [= exists V c2";
by (Asm_full_simp_tac 1);
by (strip_tac 1);
by (asm_full_simp_tac (simpset() addsimps [ex_def,dom_def]) 1);
by (rtac conjI 1);
by (strip_tac 1);
by (asm_full_simp_tac (simpset() addsimps [unbind_def]) 1);
by (Auto_tac);
by (strip_tac 2);
*)




(*
Addsimps [ex_def,unbind_def];
Goal "[| env p ass A ||- c1 [= c2|] ==> env p ass A ||- exists v c1 [= exists v c2";
by (Auto_tac);
*)





(*

Goal "env p ||- S [= T ==> env p ass A ||- S [= T";
by (asm_full_simp_tac (simpset() addsimps [refsto_point_def,entails_def]) 1);
qed "refsto_implies_crefsto";





*)