lib/concurrency: update for changed prefix_refinement rules

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

lib/concurrency/Atomicity_Lib.thy

@@ -31,7 +31,7 @@ lemmas prefix_refinement_env_steps_Await =
 
 lemma pfx_refn_interferences:
   "env_stable AR R sr iosr (\<lambda>_. True)
-   \<Longrightarrow> prefix_refinement sr iosr iosr \<top>\<top> AR R \<top>\<top> \<top>\<top> interferences interferences"
+   \<Longrightarrow> prefix_refinement sr iosr iosr dc AR R \<top>\<top> \<top>\<top> interferences interferences"
   apply (rule prefix_refinement_repeat)
     apply (erule prefix_refinement_interference)
    apply wp+
@@ -64,14 +64,12 @@ lemma repeat_pre_triv_refinement[simplified]:
   apply (simp add: repeat_def select_early)
   apply (rule triv_refinement_select_concrete_All; clarsimp)
   apply (rule_tac x="Suc x" in triv_refinement_select_abstract_x; simp)
-  apply (rule triv_refinement_refl)
   done
 
 lemma repeat_none_triv_refinement:
   "triv_refinement (repeat f) (return ())"
   apply (simp add: repeat_def)
   apply (rule_tac x="0" in triv_refinement_select_abstract_x; simp)
-  apply (rule triv_refinement_refl)
   done
 
 lemmas repeat_triv_refinement_consume_1 =
@@ -466,7 +464,6 @@ lemma rel_tr_refinement_bind_right_general:
   apply (simp add: rely_cond_append list_all2_same reflpD[where R=sr] rel_prod_sel)
   done
 
-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]
 
@@ -810,7 +807,7 @@ lemma adjust_tr_relation_equivp:
   done
 
 lemma prefix_refinement_i_modify_split:
-  "\<lbrakk>adjust_tr_relation tr_r sr; \<forall>s t. isr s t \<longrightarrow> P s \<longrightarrow> Q t \<longrightarrow> intsr (f s) (g t);
+  "\<lbrakk>adjust_tr_relation tr_r sr; \<And>s t. \<lbrakk>isr s t; P s; Q t\<rbrakk> \<Longrightarrow> intsr (f s) (g t);
     \<forall>s. tr_r s (g s); \<forall>s t. R s t \<longrightarrow> R (g s) (g t); not_env_steps_first b;
     prefix_refinement sr intsr osr rvr' AR R P' Q' d (do x \<leftarrow> interferences; b od)\<rbrakk>
    \<Longrightarrow> prefix_refinement sr isr osr rvr' AR R (\<lambda>s0 s. P s \<and> P' s0 (f s)) (\<lambda>s0 s. Q s \<and> Q' s0 (g s))

lib/concurrency/examples/Peterson_Atomicity.thy

@@ -373,9 +373,9 @@ lemmas prefix_refinement_interference_peterson_cs1 =
   prefix_refinement_interference[OF env_stable_peterson_sr_cs1]
 
 lemmas prefix_refinement_bind_2left_2right
-  = prefix_refinement_bind[where a="bind a a'" and c="bind c c'" for a a' c c', simplified bind_assoc]
+  = prefix_refinement_bind[where a="Trace_Monad.bind a a'" and c="Trace_Monad.bind c c'" for a a' c c', simplified bind_assoc]
 lemmas rel_tr_refinement_bind_left_general_2left_2right
-  = rel_tr_refinement_bind_left_general[where f="bind f f'" and g="bind g g'" for f f' g g',
+  = rel_tr_refinement_bind_left_general[where f="Trace_Monad.bind f f'" and g="Trace_Monad.bind g g'" for f f' g g',
                                         simplified bind_assoc]
 
 lemma peterson_rel_imp_invs:
@@ -393,7 +393,7 @@ lemma peterson_rel_set_label:
   by (simp add: peterson_rel_def set_label_def)
 
 lemma acquire_lock_refinement:
-  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
+  "prefix_refinement peterson_sr peterson_sr peterson_sr dc
      (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
      \<top>\<top> \<top>\<top>
      (acquire_lock ident) (acquire_lock ident)"
@@ -429,12 +429,12 @@ lemma peterson_sr_ab_label:
   by (simp add: peterson_sr_def)
 
 lemma critical_section_refinement:
-  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
+  "prefix_refinement peterson_sr peterson_sr peterson_sr dc
      (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
      (\<lambda>_ s. invs s \<and> ab_label s ident = Critical) \<top>\<top>
      abs_critical_section critical_section"
   apply (simp add: abs_critical_section_def critical_section_def)
-  apply (rule prefix_refinement_weaken_pre)
+  apply pfx_refn_pre
     apply (rule prefix_refinement_interferences_split)
     apply (rule prefix_refinement_bind_sr)
        apply (rule prefix_refinement_interference_peterson)
@@ -457,20 +457,20 @@ lemma critical_section_refinement:
       apply (rule prefix_refinement_bind_sr)
          apply (rule prefix_refinement_interference_peterson)
         apply (rule prefix_refinement_bind[where intsr=peterson_sr_cs1])
-           apply (rule pfx_refn_modifyT)
+           apply (rule prefix_refinement_modifyT)
            apply (clarsimp simp add: peterson_sr_def peterson_sr_cs1_def)
           apply (rule prefix_refinement_bind_sr)
              apply (rule cs_refine)
             apply (rule prefix_refinement_interference_peterson)
 
-           apply (wpsimp wp: validI_triv[OF cs_closed])+
+           apply (wpsimp wp: cs_closed)+
   apply (subst peterson_rel_imp_label[symmetric], assumption, simp)
   apply (drule peterson_rel_imp_invs, simp)
   apply (simp add: peterson_sr_ab_label)
   done
 
 lemma release_lock_refinement:
-  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
+  "prefix_refinement peterson_sr peterson_sr peterson_sr dc
      (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
      \<top>\<top> \<top>\<top>
      (release_lock ident) (release_lock ident)"
@@ -532,7 +532,7 @@ lemma acquire_lock_prefix_closed[simp]:
            simp: cs_closed acquire_lock_def)
 
 theorem peterson_proc_refinement:
-  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
+  "prefix_refinement peterson_sr peterson_sr peterson_sr dc
      (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
      (\<lambda>_ s. invs s \<and> ab_label s ident = Exited)
      (\<lambda>_ s. invs s \<and> ab_label s ident = Exited)
@@ -545,7 +545,7 @@ theorem peterson_proc_refinement:
       apply (rule prefix_refinement_bind_sr)
          apply (rule critical_section_refinement)
         apply (rule release_lock_refinement)
-       apply (wpsimp wp: validI_triv acquire_lock_wp
+       apply (wpsimp wp: acquire_lock_wp
                      simp: pred_conj_def)+
   done
 
@@ -597,18 +597,17 @@ lemma peterson_proc_mutual_excl_helper:
    peterson_proc ident
    \<lbrace>peterson_rel3 ident\<rbrace>,
    \<lbrace>\<lambda>rv s0 s. peterson_rel3 ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>"
-  apply (rule prefix_refinement_validI')
+  apply (rule prefix_refinement_validI)
         apply (rule peterson_proc_refinement)
        apply (rule abs_peterson_proc_mutual_excl)
-      apply (clarsimp simp: peterson_sr_peterson_rel3 peterson_sr_ab_label)
-     apply (clarsimp simp: peterson_sr_peterson_rel3)
-    apply clarsimp
-    apply (rule_tac x=t0 in exI)
-    apply (rule_tac x="t \<lparr>cs1_v := cs1_v t0\<rparr>" in exI)
-    apply (clarsimp simp: peterson_rel_def peterson_sr_def)
-   apply clarsimp
-   apply (rule_tac x="t \<lparr>cs1_v := cs1_v s0\<rparr>" in exI)
-   apply (clarsimp simp: peterson_rel_def peterson_sr_def invs_def invs_defs)
+      apply clarsimp
+      apply (rule_tac x=t0 in exI)
+      apply (rule_tac x="t \<lparr>cs1_v := cs1_v t0\<rparr>" in exI)
+      apply (clarsimp simp: peterson_rel_def peterson_sr_def)
+     apply (rule_tac x="t \<lparr>cs1_v := cs1_v s0\<rparr>" in exI)
+     apply (clarsimp simp: peterson_rel_def peterson_sr_def invs_def invs_defs)
+    apply (clarsimp simp: peterson_sr_peterson_rel3)
+   apply (clarsimp simp: peterson_sr_peterson_rel3 peterson_sr_ab_label)
   apply clarsimp
   done
 
@@ -687,7 +686,7 @@ lemma abs_peterson_proc_prefix_closed[simp]:
            simp: cs_closed abs_peterson_proc_def acquire_lock_def release_lock_def)
 
 lemma peterson_repeat_refinement:
-  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
+  "prefix_refinement peterson_sr peterson_sr peterson_sr dc
      (peterson_rel (other_ident ident)) (peterson_rel (other_ident ident))
      (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited)
      (\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited)
@@ -707,11 +706,11 @@ lemma peterson_repeat_refinement:
        apply (rule peterson_proc_refinement[THEN prefix_refinement_weaken_pre])
         apply simp+
       apply (rule prefix_refinement_interference_peterson)
-     apply (wpsimp wp: validI_triv)+
+     apply wpsimp+
   done
 
 theorem peterson_proc_system_refinement:
-  "prefix_refinement peterson_sr peterson_sr peterson_sr \<top>\<top>
+  "prefix_refinement peterson_sr peterson_sr peterson_sr dc
      (\<lambda>s0 s. s0 = s) (\<lambda>t0 t. t0 = t)
      (\<lambda>s0 s. s0 = s \<and> invs s \<and> ab_label s = (\<lambda>_. Exited))
      (\<lambda>t0 t. t0 = t \<and> invs t \<and> ab_label t = (\<lambda>_. Exited))
@@ -761,12 +760,12 @@ theorem peterson_proc_system_mutual_excl:
    peterson_proc_system
    \<lbrace>\<lambda>s0 s. invs s0 \<longrightarrow> invs s\<rbrace>,
    \<lbrace>\<lambda>rv s0 s. invs s\<rbrace>"
-  apply (rule prefix_refinement_validI')
+  apply (rule prefix_refinement_validI)
         apply (rule peterson_proc_system_refinement)
        apply (rule abs_peterson_proc_system_mutual_excl)
-      apply clarsimp
-     apply (clarsimp simp: peterson_sr_invs_sym )
-    apply (fastforce simp: peterson_rel_def peterson_sr_def)
+      apply (fastforce simp: peterson_rel_def peterson_sr_def)
+     apply clarsimp
+    apply (clarsimp simp: peterson_sr_invs_sym )
    apply clarsimp
   apply (fastforce simp: peterson_sr_def)
   done

lib/concurrency/examples/Plus2_Prefix.thy

@@ -117,9 +117,9 @@ abbreviation (input)
      prefix_refinement (\<lambda>s t. t = mainv s) (\<lambda>s t. t = mainv s) (\<lambda>s t. t = mainv s) rvr AR R P Q"
 
 theorem pfx_refn_plus2_x:
-  "p_refn (\<top>\<top>) AR R (=) (\<top>\<top>) (plus2_x tid) plus2"
+  "p_refn dc AR R (=) (\<top>\<top>) (plus2_x tid) plus2"
   apply (simp add: plus2_x_def plus2_def)
-  apply (rule prefix_refinement_weaken_pre)
+  apply pfx_refn_pre
     apply (rule pfx_refn_bind prefix_refinement_interference
                 prefix_refinement_env_steps pfx_refn_modifyT env_stable
            | wpsimp)+
@@ -140,17 +140,17 @@ theorem plus2_parallel:
    parallel plus2 plus2
    \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = 4\<rbrace>"
   apply (rule_tac sr="\<lambda>s t. t = mainv s" in prefix_refinement_validI)
-      apply (rule prefix_refinement_parallel_triv;
-             ((rule par_tr_fin_plus2_x prefix_closed_plus2)?))
-       apply (rule pfx_refn_plus2_x[where tid=1])
-      apply (rule pfx_refn_plus2_x[where tid=2])
+        apply (rule prefix_refinement_parallel_triv;
+               ((rule par_tr_fin_plus2_x prefix_closed_plus2 twp_post_taut)+)?)
+         apply (rule pfx_refn_plus2_x[where tid=1])
+        apply (rule pfx_refn_plus2_x[where tid=2])
+       apply (rule plus2_x_parallel)
+      apply clarsimp
+      apply (clarsimp simp: plus2_xstate.splits)
+      apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y])
+      apply simp
      apply clarsimp
-     apply (rule rg_strengthen_post)
-      apply (rule plus2_x_parallel[simplified])
-     apply clarsimp
-    apply (clarsimp simp: plus2_xstate.splits)
-    apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y])
-    apply simp
+    apply clarsimp
    apply clarsimp
   apply (intro prefix_closed_parallel prefix_closed_plus2)
   done
@@ -215,16 +215,16 @@ lemma bipred_disj_top_eq:
   by auto
 
 lemma fold_parallel_pfx_refn_induct:
-  "\<lbrakk>list_all2 (prefix_refinement sr sr sr (\<lambda>_ _. True) (\<top>\<top>) (\<top>\<top>) P Q) xs ys;
-    prefix_refinement sr sr sr (\<lambda>_ _. True) (\<top>\<top>) (\<top>\<top>) P Q x y;
+  "\<lbrakk>list_all2 (prefix_refinement sr sr sr dc (\<top>\<top>) (\<top>\<top>) P Q) xs ys;
+    prefix_refinement sr sr sr dc (\<top>\<top>) (\<top>\<top>) P Q x y;
     \<forall>x \<in> set (x # xs). par_tr_fin_principle x;
     \<forall>y \<in> set (y # ys). prefix_closed y\<rbrakk>
-   \<Longrightarrow> prefix_refinement sr sr sr (\<lambda>_ _. True) (\<top>\<top>) (\<top>\<top>) P Q
+   \<Longrightarrow> prefix_refinement sr sr sr dc(\<top>\<top>) (\<top>\<top>) P Q
          (fold parallel (rev xs) x) (fold parallel (rev ys) y)"
   apply (induct rule: list_all2_induct; simp)
   apply (rule prefix_refinement_parallel_triv[simplified bipred_disj_top_eq]; simp?)
    apply (clarsimp simp: fold_parallel_par_tr_fin_principle
-                         fold_parallel_prefix_closed)+
+                         fold_parallel_prefix_closed rg_TrueI)+
   done
 
 lemmas fold_parallel_pfx_refn =
@@ -236,22 +236,23 @@ theorem plus2_n_parallel:
    fold parallel (replicate (n - 1) plus2) plus2
    \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ s0 s. s = n * 2\<rbrace>"
   apply (rule_tac sr="\<lambda>s t. t = mainv s" in prefix_refinement_validI)
-      apply (rule prefix_refinement_weaken_rely,
-             rule_tac xs="map plus2_x [1 ..< n]" in fold_parallel_pfx_refn)
-           apply (clarsimp simp: list_all2_conv_all_nth)
-           apply (rule pfx_refn_plus2_x)
-          apply (rule pfx_refn_plus2_x[where tid=0])
-         apply (simp add: par_tr_fin_plus2_x)
-        apply (simp add: prefix_closed_plus2)
-       apply (simp add: le_fun_def)
-      apply (simp add: le_fun_def)
-     apply simp
-     apply (rule rg_strengthen_post, rule plus2_x_n_parallel[simplified], simp)
+        apply (rule prefix_refinement_weaken_rely,
+               rule_tac xs="map plus2_x [1 ..< n]" in fold_parallel_pfx_refn)
+             apply (clarsimp simp: list_all2_conv_all_nth)
+             apply (rule pfx_refn_plus2_x)
+            apply (rule pfx_refn_plus2_x[where tid=0])
+           apply (simp add: par_tr_fin_plus2_x)
+          apply (simp add: prefix_closed_plus2)
+         apply (simp add: le_fun_def)
+        apply (simp add: le_fun_def)
+       apply (rule plus2_x_n_parallel, simp)
+      apply clarsimp
+      apply (clarsimp simp: plus2_xstate.splits exI[where x="\<lambda>_. 0"])
      apply clarsimp
-    apply (clarsimp simp: plus2_xstate.splits exI[where x="\<lambda>_. 0"])
+     apply (rule exI, strengthen refl)
+     apply (clarsimp simp: plus2_rel_def plus2_inv_def)
+    apply clarsimp
    apply clarsimp
-   apply (rule exI, strengthen refl)
-   apply (clarsimp simp: plus2_rel_def plus2_inv_def)
   apply (rule fold_parallel_prefix_closed)
   apply (simp add: prefix_closed_plus2)
   done