lib/concurrency: update for changed RG rules

Signed-off-by: Corey Lewis <[email protected]>

lib/Crunch_Instances_Trace.thy

@@ -8,7 +8,7 @@ theory Crunch_Instances_Trace
 imports
   Crunch
   Monads.Trace_No_Fail
-  Monads.Trace_RG
+  Monads.Trace_More_RG
 begin
 
 lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE

lib/concurrency/Atomicity_Lib.thy

@@ -36,10 +36,7 @@ lemma pfx_refn_interferences:
     \<Longrightarrow> prefix_refinement sr iosr iosr (\<top>\<top>) (\<top>\<top>) (\<top>\<top>) AR R interferences interferences"
   apply (rule prefix_refinement_repeat)
     apply (erule prefix_refinement_interference)
-   apply wp
-   apply simp
-  apply wp
-  apply simp
+   apply wp+
   done
 
 lemma repeat_n_validI:
@@ -59,7 +56,7 @@ lemma repeat_validI:
 lemma interferences_twp[wp]:
   "\<lbrace>\<lambda>s0 s. (\<forall>s'. R\<^sup>*\<^sup>* s s' \<longrightarrow> Q () s' s') \<and> G s0 s \<and> reflp G \<and> Q () s0 s\<rbrace>,\<lbrace>R\<rbrace> interferences \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   (is "\<lbrace>?P\<rbrace>,\<lbrace>R\<rbrace> ?f \<lbrace>G\<rbrace>,\<lbrace>?Q\<rbrace>")
-  apply (rule validI_strengthen_post, rule repeat_validI)
+  apply (rule rg_strengthen_post, rule repeat_validI)
    apply wp
    apply (clarsimp simp: reflpD[where R=G])
    apply (metis rtranclp_trans)
@@ -506,7 +503,7 @@ lemma rel_tr_refinement_bind_right_general:
         split del: if_split)
   done
 
-lemmas validI_triv' = validI_weaken_pre[OF validI_triv, simplified]
+lemmas validI_triv' = rg_weaken_pre[OF validI_triv, simplified]
 lemmas rel_tr_refinement_bind_right
     = rel_tr_refinement_bind_right_general[where C'=False, simplified]
 
@@ -529,8 +526,7 @@ lemma rel_tr_refinement_comm_repeat_n[simplified K_bind_def]:
    apply (rule rel_tr_refinement_bind_right_general[rule_format])
      apply (metis equivpE)
     apply assumption
-   apply (rule validI_weaken_pre, wp repeat_n_validI)
-   apply simp
+   apply (wpsimp wp: repeat_n_validI)
   apply (drule_tac h="\<lambda>x. do f; return x od"
       in rel_tr_refinement_bind_left_general[rotated 2])
     apply (metis equivpE)
@@ -551,7 +547,7 @@ lemma rel_tr_refinement_comm_repeat[simplified K_bind_def]:
   apply (rule rel_tr_refinement_bind_right_general[rule_format])
     apply (metis equivpE)
    apply (erule(1) rel_tr_refinement_comm_repeat_n, simp+)
-  apply (rule validI_weaken_pre, wp, simp)
+  apply wpsimp
   done
 
 lemma rel_tr_refinement_rev_comm_repeat_n[simplified K_bind_def]:
@@ -574,8 +570,7 @@ lemma rel_tr_refinement_rev_comm_repeat_n[simplified K_bind_def]:
    apply (rule rel_tr_refinement_bind_right_general[rule_format])
      apply (metis equivpE)
     apply assumption
-   apply (rule validI_weaken_pre, wp repeat_n_validI)
-   apply simp
+   apply (wpsimp wp: repeat_n_validI)
   apply (drule_tac h="\<lambda>x. do f; return x od"
       in rel_tr_refinement_bind_left_general[rotated 2])
     apply (metis equivpE)
@@ -596,7 +591,7 @@ lemma rel_tr_refinement_rev_comm_repeat[simplified K_bind_def]:
   apply (rule rel_tr_refinement_bind_right_general[rule_format])
     apply (metis equivpE)
    apply (erule(1) rel_tr_refinement_rev_comm_repeat_n, simp+)
-  apply (rule validI_weaken_pre, wp, simp)
+  apply wpsimp
   done
 
 lemma alternative_distrib_lhs_bind:
@@ -755,8 +750,7 @@ lemma shuttle_gets_env_step[simplified K_bind_def]:
 lemma env_step_twp[wp]:
   "\<lbrace>\<lambda>s0 s. (\<forall>s'. R s0 s' \<longrightarrow> Q () s' s')\<rbrace>,\<lbrace>R\<rbrace> env_step \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>"
   apply (simp add: env_step_def)
-  apply (rule validI_weaken_pre)
-   apply (wp put_trace_elem_twp)
+  apply (wp put_trace_elem_twp)
   apply (clarsimp simp: rely_cond_def drop_Cons' guar_cond_def)
   done
 
@@ -775,7 +769,7 @@ lemma shuttle_modify_interferences[simplified K_bind_def]:
      apply assumption
     apply (rule shuttle_modify_interference, (simp add: r_into_rtranclp)+)
    apply (simp add: not_env_steps_first_interference)
-  apply (rule validI_weaken_pre, wp, simp)
+  apply wpsimp
   done
 
 lemmas shuttle_modify_interferences_flat
@@ -798,8 +792,7 @@ lemma rshuttle_modify_interferences[simplified K_bind_def]:
      apply assumption
     apply (rule rshuttle_modify_interference, (simp add: r_into_rtranclp)+)
    apply (simp add: not_env_steps_first_interference)
-  apply (rule validI_weaken_pre, wp)
-  apply simp
+  apply wpsimp
   done
 
 lemma shuttle_gets_interference[simplified K_bind_def]:
@@ -819,9 +812,9 @@ lemma shuttle_gets_interference[simplified K_bind_def]:
        apply (metis equivpE)
       apply simp
      apply simp
-    apply (rule validI_weaken_pre, wp)
+    apply wpsimp
     apply (clarsimp simp: r_into_rtranclp)
-   apply (simp add: commit_step_def, rule validI_weaken_pre, wp put_trace_elem_twp)
+   apply (simp add: commit_step_def, wp put_trace_elem_twp)
    apply (simp add: drop_Cons' guar_cond_def)
   apply (rule shuttle_gets_commit_step[THEN
     rel_tr_refinement_bind_left_general[rotated -1], simplified bind_assoc return_bind])
@@ -844,8 +837,7 @@ lemma shuttle_gets_interferences[simplified K_bind_def]:
     apply simp
    apply (rule rel_tr_refinement_comm_repeat, assumption)
      apply (rule shuttle_gets_interference; simp)
-     apply simp
-    apply (rule validI_weaken_pre, wp, simp)
+    apply simp
    apply wpsimp
   apply (simp add: bind_assoc)
   apply (rule rel_tr_refinement_refl)

lib/concurrency/Prefix_Refinement.thy

@@ -995,7 +995,7 @@ theorem prefix_refinement_validI:
   apply (case_tac tr; clarsimp simp: list_all2_Cons2 matching_tr_def)
   done
 
-lemmas prefix_refinement_validI' = prefix_refinement_validI[OF _ validI_strengthen_guar, OF _ validI_strengthen_post]
+lemmas prefix_refinement_validI' = prefix_refinement_validI[OF _ rg_strengthen_guar, OF _ rg_strengthen_post]
 
 section \<open>Building blocks.\<close>
 text \<open>
@@ -1239,7 +1239,7 @@ lemma prefix_refinement_repeat:
        apply simp
       apply simp
       apply (rule prefix_refinement_repeat_n, assumption+)
-      apply (rule validI_weaken_pre, assumption, simp)
+      apply (rule rg_weaken_pre, assumption, simp)
      apply wp
     apply wp
    apply clarsimp

lib/concurrency/Triv_Refinement.thy

@@ -6,7 +6,7 @@
 theory Triv_Refinement
 
 imports
-  "Monads.Trace_RG"
+  "Monads.Trace_More_RG"
   "Monads.Trace_Strengthen_Setup"
 
 begin

lib/concurrency/examples/Peterson_Atomicity.thy

@@ -258,9 +258,9 @@ lemma cs2_wp_apply_peterson[wp]:
   \<lbrace> peterson_rel ident \<rbrace>,
   \<lbrace> Q \<rbrace>"
   apply (rule validI_name_pre[OF cs_closed], clarsimp simp del: imp_disjL)
-  apply (rule validI_weaken_pre)
+  apply (rule rg_weaken_pre)
    apply (rule validI_well_behaved[OF cs_closed])
-     apply (rule validI_strengthen_post)
+     apply (rule rg_strengthen_post)
       apply (rule_tac s=s and ?s0.0=s0
          and lockf="\<lambda>s. critical (ab_label s ident)"
          and I="invs" in cs_wp)
@@ -284,8 +284,7 @@ lemma release_lock_mutual_excl:
    \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
                \<and> ab_label s ident = Exited \<rbrace>"
   apply (simp add: release_lock_def)
-  apply (rule validI_weaken_pre)
-   apply wpsimp+
+  apply wpsimp
   apply (strengthen peterson_rel_imp_assume_invs | simp)+
   apply (cases ident)
   apply (safe, simp_all)
@@ -303,8 +302,7 @@ lemma abs_critical_section_mutual_excl:
    \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
                \<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>"
   apply (simp add: abs_critical_section_def)
-  apply (rule validI_weaken_pre)
-   apply wpsimp+
+  apply wpsimp
   apply (strengthen peterson_rel_imp_assume_invs | simp)+
   apply (cases ident)
   apply (safe, simp_all)
@@ -321,8 +319,7 @@ lemma acquire_lock_mutual_excl:
    \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> invs s0
                \<and> ab_label s ident = Critical \<and> csI (cs2_v s) \<rbrace>"
   apply (simp add: acquire_lock_def)
-  apply (rule validI_weaken_pre)
-   apply (wpsimp wp: Await_sync_twp)+
+  apply (wpsimp wp: Await_sync_twp)
   apply (strengthen peterson_rel_imp_assume_invs | simp)+
   apply (cases ident)
   apply (safe, simp_all)
@@ -340,9 +337,8 @@ theorem abs_peterson_proc_mutual_excl:
    \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
                \<and> ab_label s ident = Exited \<rbrace>"
   apply (simp add: abs_peterson_proc_def bind_assoc)
-  apply (rule validI_weaken_pre)
-   apply (wpsimp wp: release_lock_mutual_excl acquire_lock_mutual_excl
-                     abs_critical_section_mutual_excl)+
+  apply (wpsimp wp: release_lock_mutual_excl acquire_lock_mutual_excl
+                    abs_critical_section_mutual_excl)
   done
 
 definition
@@ -562,8 +558,7 @@ lemma acquire_lock_wp:
    \<lbrace> \<top>\<top> \<rbrace>,
    \<lbrace> \<lambda>rv s0 s. invs s \<and> ab_label s ident = Critical \<rbrace>"
   apply (simp add: acquire_lock_def)
-  apply (rule validI_weaken_pre)
-   apply (wpsimp wp: Await_sync_twp)+
+  apply (wpsimp wp: Await_sync_twp)
   apply (subst (asm) peterson_rel_imp_label, assumption+)
   apply (drule(1) peterson_rel_imp_invs)
   apply (drule(1) peterson_rel_trans)
@@ -630,7 +625,7 @@ lemma peterson_rel_helpers:
   by (clarsimp simp: peterson_rel_def peterson_rel2_def peterson_rel3_def)
 
 lemma peterson_rel_peterson_rel2:
-  "peterson_rel ident s0 s \<longrightarrow> peterson_rel2 ident s0 s"
+  "peterson_rel ident s0 s \<Longrightarrow> peterson_rel2 ident s0 s"
   by (clarsimp simp: peterson_rel_def peterson_rel2_def)
 
 lemma peterson_sr_peterson_rel3:
@@ -679,9 +674,8 @@ lemma peterson_proc_mutual_excl_helper':
                \<and> ab_label s ident = Exited \<rbrace>"
   apply (simp add: peterson_proc_def acquire_lock_def release_lock_def
                    critical_section_def)
-  apply (rule validI_weaken_pre)
-   apply (wp Await_sync_twp | simp add: split_def
-          | rule validI_strengthen_guar[OF _ allI[OF allI[OF peterson_rel_peterson_rel2]]])+
+  apply (wp Await_sync_twp | simp add: split_def
+         | rule rg_strengthen_guar[OF _ peterson_rel_peterson_rel2])+
   apply (clarsimp simp: imp_conjL)
   apply (strengthen peterson_rel_imp_assume_invs | simp)+
   apply (cases ident)
@@ -699,7 +693,7 @@ lemma peterson_proc_mutual_excl:
    \<lbrace> peterson_rel ident \<rbrace>,
    \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
                \<and> ab_label s ident = Exited \<rbrace>"
-  apply (rule validI_strengthen_guar, rule validI_strengthen_post, rule validI_guar_post_conj_lift)
+  apply (rule rg_strengthen_guar, rule rg_strengthen_post, rule validI_guar_post_conj_lift)
      apply (rule peterson_proc_mutual_excl_helper)
     apply (rule peterson_proc_mutual_excl_helper')
    apply (clarsimp simp: peterson_rel_helpers)+
@@ -716,7 +710,7 @@ lemma validI_repeat_interference:
   apply (rule bind_twp)
    apply simp
    apply (rule interference_twp)
-  apply (rule validI_strengthen_post)
+  apply (rule rg_strengthen_post)
    apply (rule repeat_validI, assumption)
   apply simp
   done
@@ -727,7 +721,7 @@ lemma abs_peterson_proc_system_mutual_excl:
      abs_peterson_proc_system
    \<lbrace> \<lambda>s0 s. invs s0 \<longrightarrow> invs s \<rbrace>,
    \<lbrace> \<lambda>rv s0 s. invs s \<rbrace>"
-  apply (rule validI_weaken_pre, rule validI_strengthen_post)
+  apply (rule rg_weaken_pre, rule rg_strengthen_post)
     apply (unfold abs_peterson_proc_system_def)
     apply (rule rg_validI[where Qf="\<lambda>_ _. invs" and Qg="\<lambda>_ _. invs"])
            apply (rule validI_repeat_interference[OF abs_peterson_proc_mutual_excl])
@@ -761,9 +755,9 @@ lemma peterson_repeat_refinement:
   apply (rule prefix_refinement_weaken_pre)
     apply (rule prefix_refinement_bind_sr)
        apply (rule prefix_refinement_repeat[rotated])
-         apply (rule abs_peterson_proc_mutual_excl[THEN validI_strengthen_guar])
+         apply (rule abs_peterson_proc_mutual_excl[THEN rg_strengthen_guar])
          apply simp
-        apply (rule peterson_proc_mutual_excl[THEN validI_strengthen_guar, THEN validI_weaken_pre])
+        apply (rule peterson_proc_mutual_excl[THEN rg_strengthen_guar, THEN rg_weaken_pre])
          apply simp+
        apply (rule peterson_proc_refinement[THEN prefix_refinement_weaken_pre])
         apply simp+
@@ -793,19 +787,19 @@ theorem peterson_proc_system_refinement:
         apply (rule eq_refl, rule bipred_disj_op_eq, simp)
        apply (clarsimp intro!: par_tr_fin_bind par_tr_fin_interference)
       apply (clarsimp intro!: par_tr_fin_bind par_tr_fin_interference)
-     apply (rule validI_weaken_pre, rule validI_weaken_rely)
+     apply (rule rg_weaken_pre, rule rg_weaken_rely)
        apply (rule validI_repeat_interference; simp)
         apply (rule peterson_proc_mutual_excl)
        apply (simp+)[3]
-    apply (rule validI_weaken_pre, rule validI_weaken_rely)
+    apply (rule rg_weaken_pre, rule rg_weaken_rely)
       apply (rule validI_repeat_interference; simp)
        apply (rule peterson_proc_mutual_excl)
       apply (simp+)[3]
-  apply (rule validI_weaken_pre, rule validI_weaken_rely)
+  apply (rule rg_weaken_pre, rule rg_weaken_rely)
      apply (rule validI_repeat_interference; simp)
       apply (rule abs_peterson_proc_mutual_excl)
      apply (simp+)[3]
-  apply (rule validI_weaken_pre, rule validI_weaken_rely)
+  apply (rule rg_weaken_pre, rule rg_weaken_rely)
     apply (rule validI_repeat_interference; simp)
      apply (rule abs_peterson_proc_mutual_excl)
     apply (simp+)[3]

lib/concurrency/examples/Plus2_Prefix.thy

@@ -79,17 +79,15 @@ theorem plus2_x_property:
   "\<lbrace>\<lambda>s0 s. plus2_inv tids s \<and> threadv s tid = 0 \<and> s = s0 \<and> tid \<in> tids \<and> finite tids\<rbrace>,\<lbrace>plus2_rel tids {tid}\<rbrace>
     plus2_x tid \<lbrace>plus2_rel tids (- {tid})\<rbrace>,\<lbrace>\<lambda>_ _ s. plus2_inv tids s \<and> threadv s tid = 2\<rbrace>"
   apply (simp add: plus2_x_def)
-  apply (rule validI_weaken_pre)
-   apply wp
-  apply clarsimp
+  apply wpsimp
   apply (clarsimp simp: plus2_rel_def point_update_def)
   done
 
 corollary plus2_x_parallel:
   "\<lbrace>\<lambda>s0 s. mainv s = 0 \<and> (\<forall>tid \<in> {1, 2}. threadv s tid = 0) \<and> s = s0\<rbrace>,\<lbrace>\<lambda>a b. a = b\<rbrace>
     parallel (plus2_x 1) (plus2_x 2) \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. mainv s = 4\<rbrace>"
-  apply (rule validI_weaken_pre)
-   apply (rule validI_strengthen_post)
+  apply (rule rg_weaken_pre)
+   apply (rule rg_strengthen_post)
     apply ((rule rg_validI plus2_x_property[where tids="{1, 2}"])+; simp add: plus2_rel_def le_fun_def)
    apply (clarsimp simp: plus2_inv_def)
   apply (clarsimp simp add: plus2_inv_def)
@@ -114,10 +112,8 @@ theorem pfx_refn_plus2_x:
   apply (simp add: plus2_x_def plus2_def)
   apply (rule prefix_refinement_weaken_pre)
     apply (rule pfx_refn_bind prefix_refinement_interference
-         prefix_refinement_env_steps allI
-         pfx_refn_modifyT env_stable
-       | simp
-       | wp)+
+                prefix_refinement_env_steps pfx_refn_modifyT env_stable
+           | wpsimp)+
   done
 
 lemma par_tr_fin_plus2_x:
@@ -127,8 +123,7 @@ lemma par_tr_fin_plus2_x:
 lemma prefix_closed_plus2:
   "prefix_closed plus2"
   apply (simp add: plus2_def)
-  apply (rule validI_prefix_closed_T, rule validI_weaken_pre, wp)
-  apply simp
+  apply (rule validI_prefix_closed_T, wpsimp)
   done
 
 theorem plus2_parallel:
@@ -140,7 +135,7 @@ theorem plus2_parallel:
        apply (rule pfx_refn_plus2_x[where tid=1])
       apply (rule pfx_refn_plus2_x[where tid=2])
      apply clarsimp
-     apply (rule validI_strengthen_post)
+     apply (rule rg_strengthen_post)
       apply (rule plus2_x_parallel[simplified])
      apply clarsimp
     apply (clarsimp simp: plus2_xstate.splits)
@@ -164,10 +159,10 @@ lemma plus2_x_n_parallel_induct:
   apply (case_tac n)
    apply (simp only: lessThan_Suc)
    apply simp
-   apply (rule validI_weaken_pre, rule plus2_x_property)
+   apply (wp plus2_x_property)
    apply clarsimp
   apply (clarsimp split del: if_split)
-  apply (rule validI_weaken_pre, rule validI_strengthen_post,
+  apply (rule rg_weaken_pre, rule rg_strengthen_post,
     rule rg_validI, rule plus2_x_property[where tids="{..< N}"],
     assumption, (clarsimp simp: plus2_rel_def)+)
    apply (auto dest: less_Suc_eq[THEN iffD1])[1]
@@ -178,8 +173,8 @@ theorem plus2_x_n_parallel:
   "n > 0 \<Longrightarrow>
   \<lbrace>\<lambda>s0 s. mainv s = 0 \<and> (\<forall>i < n. threadv s i = 0) \<and> s = s0\<rbrace>,\<lbrace>plus2_rel {..< n} {..< n}\<rbrace>
     fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ _ s. mainv s = (n * 2)\<rbrace>"
-  apply (rule validI_weaken_pre, rule validI_strengthen_post,
-      rule validI_strengthen_guar, erule plus2_x_n_parallel_induct)
+  apply (rule rg_weaken_pre, rule rg_strengthen_post,
+      rule rg_strengthen_guar, erule plus2_x_n_parallel_induct)
      apply simp
     apply simp
    apply (clarsimp simp: plus2_inv_def)
@@ -240,7 +235,7 @@ theorem plus2_n_parallel:
        apply (simp add: le_fun_def)
       apply (simp add: le_fun_def)
      apply simp
-     apply (rule validI_strengthen_post, rule plus2_x_n_parallel[simplified], simp)
+     apply (rule rg_strengthen_post, rule plus2_x_n_parallel[simplified], simp)
      apply clarsimp
     apply (clarsimp simp: plus2_xstate.splits exI[where x="\<lambda>_. 0"])
    apply clarsimp