File RefCmd.ML

Addsimps [refeq_cmd_def,refsto_cmd_def];
Addsimps [refsto_exec,refeq_exec];
Addsimps [refsto_pcmd_def,refeq_pcmd_def, refsto_pexec, refeq_pexec];
Addsimps [bnds_land,bnds_lor,bnds_lnot,bnds_equiv];

section "PRELIMINARY DEFINITIONS";

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

section "PARAMETERISED REFINEMENT RELATIONS PROPERTIES";

Goal "S prefeq(p) T ==> S prefsto(p) T";
by (Asm_full_simp_tac 1);
qed "prefeqD1";


Goal "[| S prefsto(p) T; T prefsto(p) U |] ==> S prefsto(p) U";
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
by (Blast_tac 1);
qed "prefsto_trans";

Goal "[| S prefeq(p) T; T prefeq(p) U |] ==> S prefeq(p) U";
by (asm_full_simp_tac (simpset() addsimps [dom_def]) 1);
qed "prefeq_trans";

Goal "S prefsto(p) S";
by (Simp_tac 1);
qed "prefsto_refl";

Goal "S prefeq(p) S";
by (Simp_tac 1);
qed "prefeq_refl";

Goal "S prefeq(p) T ==> T prefeq(p) S";
by (Asm_full_simp_tac 1);
qed "prefeq_symm";


section "REFINEMENT RELATION PROPERTIES";


val prems = goal RefCmd.thy "[| S [=](p) T; T [=](p) U |] ==> S [=](p) U";
by (cut_facts_tac prems 1);
by (Rewrite_subgoal_tac [refeq_cmd_def] 1);
by (Rewrite_subgoal_tac [refeq_exec] 1);
by (resolve_tac [trans] 1);
by (Asm_simp_tac 1);
by (Asm_simp_tac 1);
qed "refeq_trans";



val prems = goal RefCmd.thy "S [=](p) T ==> T [=](p) S";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "refeq_symm";


goal RefCmd.thy "S [=](p) S";
by (simp_tac (simpset() addsimps []) 1);
qed "refeq_refl";


Goal "[| S [=(p) T; T [=(p) U |] ==> S [=(p) U ";
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (rtac conjI 1);
by (res_inst_tac [("B","dom (exec p T)")] subset_trans 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (rtac ballI 1);
by (res_inst_tac [("s", "exec p T s")] trans 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (cut_inst_tac [("A","dom (exec p S)"), ("B","dom (exec p T)"),("c","s")] subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "refsto_trans";


goal RefCmd.thy "S [=(p) S";
by (simp_tac (simpset() addsimps []) 1);
qed "refsto_refl";


Goal "[| env p ||- c1 [= c2; env p ||- c2 [= c1|] ==> env p ||- c1 [=] c2";
by (Asm_full_simp_tac 1);
by (rtac expand_partial_fun_eq 1);
by (Auto_tac);
qed "refsto_antisymm";


val prems = goal RefCmd.thy "[| S [=](p) T|] ==> S [=(p) T";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "refeqD1";


val prems = goal RefCmd.thy "[| S [=](p) T|] ==> T [=(p) S";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "refeqD2";


Goal "(env p ||- c1 [= c2 & env p ||- c2 [= c1) = (env p ||- c1 [=] c2)";
by (rtac iffI 1);
by (rtac refsto_antisymm 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
by (rtac refeqD1 1);
by (Asm_full_simp_tac 1);
by (rtac refeqD2 1);
by (Asm_full_simp_tac 1);
qed "refeq_simp";

(*
Goal "(S [=](p) T) = (! b. exec p S {b} = exec p T {b})";
by (rtac (sym RS trans) 1);
by (rtac refeq_simp 1);
by (asm_full_simp_tac (simpset() addsimps [refines_pointwise]) 1);
by (rtac iffI 1);
by (strip_tac 1);
by (cut_inst_tac [("P","{b}:dom (exec p S)")] excluded_middle 1);
by (dresolve_tac [disjE] 1);
by (assume_tac 3);
by (dresolve_tac [conjunct2] 2);
by (dresolve_tac [conjunct1] 2);
by (dres_inst_tac [("x","{b}")] bspec 2);
by (Asm_full_simp_tac 2);
by (Asm_full_simp_tac 2);
by (cut_inst_tac [("P","{b}:dom (exec p T)")] excluded_middle 1);
by (dresolve_tac [disjE] 1);
by (Asm_full_simp_tac 3);
by (dresolve_tac [conjunct2] 2);
by (dresolve_tac [conjunct2] 2);
by (dresolve_tac [conjunct2] 2);
by (dres_inst_tac [("x","{b}")] bspec 2);
by (Asm_full_simp_tac 2);
by (Asm_full_simp_tac 2);
by (cut_inst_tac [("f","exec p S"),("s","{b}")] apply_None 1);
by (assume_tac 1);
by (cut_inst_tac [("f","exec p T"),("s","{b}")] apply_None 1);
by (assume_tac 1);
by (Asm_full_simp_tac 1);
by (Auto_tac);
by (Asm_full_simp_tac 1);
by (rtac conjI 1);
by (strip_tac 1);

by (Asm_full_simp_tac 1);
*)

section "ALGEBRA RULES";

Goal "env p ||- fail sand S [=] fail";
by (simp_tac (simpset() addsimps [partcomp_def,dom_def,exec_empty]) 1);
qed "fail_sand";

Goal "env p ||- abort sand S [=] abort";
by (simp_tac (simpset() addsimps [partcomp_def,dom_def,exec_empty]) 1);
by (rtac ext 1);
by (Auto_tac);
by (simp_tac (simpset() addsimps [exec_empty]) 1);
qed "abort_sand";

Goal "env p ||- spec(ptrue) sand S [=] S";
by (simp_tac (simpset() addsimps [partcomp_def,dom_def,exec_empty,bnds_def]) 1);
qed "skip_sand";

goal RefCmd.thy "(S pand T) [=](p) (T pand S)";
by (simp_tac (simpset() addsimps [PInt_commute]) 1);
qed "pand_commute";


goal RefCmd.thy "(S por T) [=](p) (T por S)";
by (simp_tac (simpset() addsimps [PUn_commute]) 1);
qed "por_commute";


goal RefCmd.thy "(S pand (T pand U)) [=](p) ((S pand T) pand U)";
by (simp_tac (simpset() addsimps [PInt_assoc]) 1);
qed "pand_assoc";



goal RefCmd.thy "(S por (T por U)) [=](p) ((S por T) por U)";
by (simp_tac (simpset() addsimps [PUn_assoc]) 1);
qed "por_assoc";




goal RefCmd.thy "(S pand (T por U)) [=](p) ((S pand T) por (S pand U))";
by (simp_tac (simpset() addsimps [distrib_PInt_PUn]) 1);
qed "distribute_pand_over_por";



goal RefCmd.thy "(S por (T pand U)) [=](p) ((S por T) pand (S por U))";
by (simp_tac (simpset() addsimps [distrib_PUn_PInt]) 1);
qed "distribute_por_over_pand";

goal RefCmd.thy "(S sand (T por U)) [=](p) ((S sand T) por (S sand U))";
by (simp_tac (simpset() addsimps [PUn_def,partcomp_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [dom_def]) 1);
qed "left_distrib_sand_over_por";



goal RefCmd.thy "(S sand (T pand U)) [=](p) ((S sand T) pand (S sand U))";
by (simp_tac (simpset() addsimps [PInt_def,partcomp_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps []) 1);
qed "left_distrib_sand_over_pand";

goal RefCmd.thy "(S por T) pand U [=](p) (S pand U) por (T pand U)";
by (simp_tac (simpset() addsimps [PInt_def,PUn_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "right_distribute_pand_over_por";

goal RefCmd.thy "((S sand T) sand U) [=](p) (S sand (T sand U))";
by (simp_tac (simpset() addsimps [partcomp_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps []) 1);
qed "sand_assoc";

(*
Goal "(S [=](p) T) = (! b. exec p S {b} = exec p T {b})"; 
Goal "Cmd.all V (S pand T) [=](p) (Cmd.all V S) pand (Cmd.all V S)";
by (Auto_tac);
by (simp_tac (simpset() addsimps [forall_def,PInt_def,dom_def,unbind_def]) 1);
by (Auto_tac);
*)

section "MONOTONICITY RULES";


val prems = goal RefCmd.thy "[| c1 [=(p) c2; c3 [=(p) c4 |] ==> c1 pand c3 [=(p) c2 pand c4";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [refsto_exec]) 1);
by (resolve_tac [conjI] 1);
by (resolve_tac [Int_mono] 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (strip_tac 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 (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (dresolve_tac [bspec] 1);
by (rotate_tac 4 1);
by (assume_tac 1);
by (dresolve_tac [bspec] 1);
by (rotate_tac 2 1);
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [PInt_def]) 1);
by (rtac conjI 1);
by (rtac subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (rtac subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "pand_mono";




val prems = goal RefCmd.thy "[| c1 [=(p) c2; c3 [=(p) c4 |] ==> c1 por c3 [=(p) c2 por c4";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [refsto_exec]) 1);
by (resolve_tac [conjI] 1);
by (rtac Int_mono 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 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 (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 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 (asm_full_simp_tac (simpset() addsimps [PUn_def]) 1);
by (rtac conjI 1);
by (res_inst_tac [("c","s"),("A","dom (exec p c1)"), ("B","dom (exec p c2)")]  subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (res_inst_tac [("c","s"),("A","dom (exec p c3)"), ("B","dom (exec p c4)")]  subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed "por_mono";

val prems = goal RefCmd.thy "[| c1 [=(p) c2; c3 [=(p) c4 |] ==> c1 sand c3 [=(p) c2 sand c4";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [refsto_exec]) 1);
by (resolve_tac [conjI] 1);
by (simp_tac (simpset() addsimps [dom_partcomp]) 1);
by (resolve_tac [subsetI] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (resolve_tac [conjI] 1);
by (res_inst_tac [("c","x"),("A","dom (exec p c1)"), ("B","dom (exec p c2)")]  subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 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 (eresolve_tac [subst] 1);
by (res_inst_tac [("c","the (exec p c1 x)"),("A","dom (exec p c3)"), ("B","dom (exec p c4)")]  subsetD 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (resolve_tac [ballI] 1);
by (asm_full_simp_tac (simpset() addsimps [dom_partcomp]) 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 1);
by (forward_tac [conjunct1] 1);
by (dresolve_tac [conjunct2] 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 (asm_full_simp_tac (simpset() addsimps [partcomp_def,dom_def]) 1);
qed "sand_mono";

Goal "S [=(p) T ==> S pand U [=(p) T pand U";
by (resolve_tac [pand_mono] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (resolve_tac [refsto_refl] 1);

qed "pand_left_mono";

Goal "S [=(p) T ==> U pand S [=(p) U pand T";
by (resolve_tac [pand_mono] 1);
by (resolve_tac [refsto_refl] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "pand_right_mono";

Goal "S [=(p) T ==> S por U [=(p) T por U";
by (resolve_tac [por_mono] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (resolve_tac [refsto_refl] 1);
qed "por_left_mono";

Goal "S [=(p) T ==> U por S [=(p) U por T";
by (resolve_tac [por_mono] 1);
by (resolve_tac [refsto_refl] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "por_right_mono";

Goal "S [=(p) T ==> S sand U [=(p) T sand U";
by (resolve_tac [sand_mono] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (resolve_tac [refsto_refl] 1);
qed "sand_left_mono";

Goal "S [=(p) T ==> U sand S [=(p) U sand T";
by (resolve_tac [sand_mono] 1);
by (resolve_tac [refsto_refl] 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
qed "sand_right_mono";

Goal "[| S [=](p) T; U [=](p) V |] ==> S sand U [=](p) T sand V";
by (Asm_full_simp_tac 1);
qed "sand_refeq_mono";

Goal "[| S [=](p) T; U [=](p) V |] ==> S pand U [=](p) T pand V";
by (Asm_full_simp_tac 1);
qed "pand_refeq_mono";

Goal "[| S [=](p) T; U [=](p) V |] ==> S por U [=](p) T por V";
by (Asm_full_simp_tac 1);
qed "por_refeq_mono";

Goal "[| S [=](p) T|] ==> exists V S [=](p) exists V T";
by (Asm_full_simp_tac 1);
qed "exists_refeq_mono";

section "PREDICATE LIFTING RULES";

goal RefCmd.thy "(spec(P) pand spec(Q)) [=](p) (spec(P && Q))";
by (simp_tac (simpset() addsimps [PInt_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "lift_pand";

goal RefCmd.thy "(spec(P) por spec(Q)) [=](p) (spec(P || Q))";
by (simp_tac (simpset() addsimps [PUn_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "lift_por";

goal RefCmd.thy "(exists v (spec P)) [=](p) spec(pex v P)";
by (simp_tac (simpset() addsimps [ex_def,dom_def,unbind_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "lift_exists";

goal RefCmd.thy "(Cmd.all v (spec P)) [=](p) spec(pall v P)";
by (simp_tac (simpset() addsimps [forall_def,bnds_def,unbind_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "lift_forall";

section "ASSUMPTION RULES";

goal RefCmd.thy "assert(A) sand assert(B) [=](p) assert(A && B)";
by (simp_tac (simpset() addsimps [partcomp_def,dom_def]) 1);
by (resolve_tac [ext] 1);
by (Rewrite_subgoal_tac [if_Some_point] 1);
by (simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "combine_assert";


goal RefCmd.thy "(assert(A) sand S) [=(p) S";
by (Rewrite_subgoal_tac [refsto_cmd_def] 1);
by (Rewrite_subgoal_tac [refsto_exec] 1);
by (resolve_tac [conjI] 1);
by (simp_tac (simpset() addsimps []) 1);
by (Rewrite_subgoal_tac [dom_partcomp] 1);
by (simp_tac (simpset() addsimps [dom_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (asm_full_simp_tac (simpset() addsimps [dom_partcomp,dom_def,partcomp_def]) 1);
qed "remove_assert";


Goal "|[P => Q]| ==> assert(P) [=(p) assert(Q)";
by (asm_full_simp_tac (simpset() addsimps [dom_def,bnds_def,everywhere_def]) 1);
by (resolve_tac [conjI] 1);
by (blast_tac (claset() addIs [] addEs []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "weaken_assert";


Goal "spec(P) [=](p) spec(P) sand assert(P)";
by (simp_tac (simpset() addsimps [refeq_exec,partcomp_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset () addsimps [dom_def,bnds_def]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "establish_assert";

val prems = Goal "|[A]| ==> S [=](p) assert(A) sand S";
by (asm_full_simp_tac (simpset() addsimps [refeq_exec,dom_def,everywhere_def,partcomp_def,bnds_def]) 1);
qed "introduce_assert";

val prems = goal RefCmd.thy "|[ A => (P <=> Q) ]| ==> assert(A) sand spec(P) [=](p) assert(A) sand spec(Q)";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [refeq_exec,dom_def,everywhere_def,partcomp_def,bnds_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps []) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "equivalent_under_assert";

val prems = goal RefCmd.thy "|[ P => A ]| ==> spec(P) [=](p) spec(P) sand assert(A)";
by (cut_facts_tac prems 1);
by (asm_full_simp_tac (simpset() addsimps [refeq_exec,dom_def,everywhere_def,partcomp_def,bnds_def]) 1);
by (resolve_tac [ext] 1);
by (simp_tac (simpset() addsimps [if_Some_point]) 1);
by (blast_tac (claset() addIs [] addEs []) 1);
qed "assert_after_spec";





section "SPECIFICATION RULES";


Goal "|[ P <=>  Q ]| ==> spec(P) [=](p) spec(Q)";
by (asm_full_simp_tac(simpset() addsimps [equiv_def,everywhere_def,bnds_def]) 1);
qed "equivalent_spec";