lib/concurrency: update for changed lemma names

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

lib/concurrency/Atomicity_Lib.thy

@@ -438,8 +438,7 @@ lemma not_env_steps_first_interference:
   apply (clarsimp simp: not_env_steps_first_def)
   done
 
-lemmas not_env_steps_first_simple
-    = no_trace_all[THEN not_env_steps_first_no_trace]
+lemmas not_env_steps_first_simple = no_trace_terminal[THEN not_env_steps_first_no_trace]
 
 lemma not_env_steps_first_repeat_n:
   "not_env_steps_first f \<Longrightarrow> not_env_steps_first (repeat_n n f)"
@@ -753,8 +752,6 @@ lemma shuttle_gets_env_step[simplified K_bind_def]:
   apply (clarsimp simp: rely_cond_def reflpD)
   done
 
-lemmas prefix_closed_interference[simp] = interference_twp[THEN validI_prefix_closed]
-
 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)

lib/concurrency/Prefix_Refinement.thy

@@ -543,7 +543,7 @@ lemma is_matching_fragment_validI_disj:
   apply (erule(2) validI_triv_refinement)
   done
 
-lemma rely_prefix_closed:
+lemma prefix_closed_rely:
   "prefix_closed f \<Longrightarrow> prefix_closed (rely f R s0)"
   apply (subst prefix_closed_def, clarsimp simp: rely_def rely_cond_Cons_eq)
   apply (erule(1) prefix_closedD)
@@ -593,7 +593,7 @@ theorem prefix_refinement_parallel:
   apply (subst is_matching_fragment_def, clarsimp)
   apply (frule(1) is_matching_fragment_validI_disj[where g=a and G=Ga], blast)
   apply (frule(1) is_matching_fragment_validI_disj[where g=c and G=Gc], blast)
-  apply (intro conjI parallel_prefix_closed rely_prefix_closed rely_self_closed,
+  apply (intro conjI prefix_closed_parallel prefix_closed_rely rely_self_closed,
     simp_all add: is_matching_fragment_prefix_closed)
      apply (rule self_closed_parallel_fragment,
         (assumption | erule par_tr_fin_principle_triv_refinement[rotated])+)
@@ -772,7 +772,7 @@ lemma env_closed_mbind:
   apply (fastforce elim: image_eqI[rotated])
   done
 
-lemma mbind_prefix_closed:
+lemma prefix_closed_mbind:
   "prefix_closed f
     \<Longrightarrow> \<forall>tr x s' s. (tr, Result (x, s')) \<in> f s \<longrightarrow> prefix_closed (g (last_st_tr tr s0) x)
    \<Longrightarrow> prefix_closed (mbind f g s0)"
@@ -800,7 +800,7 @@ lemma is_matching_fragment_mbind:
         (mbind f_a f_b s0)"
   apply (subst is_matching_fragment_def, clarsimp)
   apply (strengthen env_closed_mbind[where ctr''=ctr', mk_strg I E]
-                    mbind_prefix_closed
+                    prefix_closed_mbind
                     self_closed_mbind[where ctr'="ctr'", mk_strg I E])
   apply (simp add: conj_comms if_bool_eq_conj mres_def split del: if_split)
   apply (intro conjI allI impI; clarsimp?;
@@ -1346,10 +1346,10 @@ lemma prefix_refinement_modify:
 
 lemmas pfx_refn_modifyT = prefix_refinement_modify[where P="\<top>" and Q="\<top>"]
 
-lemmas prefix_refinement_get_pre
-    = prefix_refinement_bind[OF prefix_refinement_get _
-        valid_validI_wp[OF _ get_sp] valid_validI_wp[OF _ get_sp],
-    simplified pred_conj_def no_trace_all, simplified]
+lemmas prefix_refinement_get_pre =
+  prefix_refinement_bind[OF prefix_refinement_get _ valid_validI_wp[OF _ get_sp]
+                            valid_validI_wp[OF _ get_sp],
+                         simplified pred_conj_def, simplified]
 
 lemma prefix_refinement_gets:
   "\<forall>s t. iosr s t \<and> P s \<and> Q t \<longrightarrow> rvr (f s) (f' t)
@@ -1477,7 +1477,7 @@ lemma is_matching_fragment_add_rely:
     \<Longrightarrow> AR' \<le> AR
     \<Longrightarrow> is_matching_fragment sr osr r ctr cres s0 AR' s (rely f AR' s0)"
   apply (frule is_matching_fragment_Nil)
-  apply (clarsimp simp: is_matching_fragment_def rely_prefix_closed
+  apply (clarsimp simp: is_matching_fragment_def prefix_closed_rely
                         rely_self_closed)
   apply (intro conjI)
     apply (erule rely_env_closed)

lib/concurrency/examples/Peterson_Atomicity.thy

@@ -813,7 +813,7 @@ theorem peterson_proc_system_refinement:
 
 lemma peterson_proc_system_prefix_closed[simp]:
   "prefix_closed (peterson_proc_system)"
-  by (auto intro!: prefix_closed_bind parallel_prefix_closed
+  by (auto intro!: prefix_closed_bind prefix_closed_parallel
              simp: cs_closed peterson_proc_system_def)
 
 theorem peterson_proc_system_mutual_excl:

lib/concurrency/examples/Plus2_Prefix.thy

@@ -147,7 +147,7 @@ theorem plus2_parallel:
     apply (strengthen exI[where x="f(1 := x, 2 := y)" for f x y])
     apply simp
    apply clarsimp
-  apply (intro parallel_prefix_closed prefix_closed_plus2)
+  apply (intro prefix_closed_parallel prefix_closed_plus2)
   done
 
 section \<open>Generalising\<close>
@@ -202,7 +202,7 @@ lemma fold_parallel_par_tr_fin_principle[where xs="rev xs" for xs, simplified]:
 lemma fold_parallel_prefix_closed[where xs="rev xs" for xs, simplified]:
   "\<forall>x \<in> insert x (set xs). prefix_closed x
     \<Longrightarrow> prefix_closed (fold parallel (rev xs) x)"
-  by (induct xs, simp_all add: parallel_prefix_closed)
+  by (induct xs, simp_all add: prefix_closed_parallel)
 
 lemma bipred_disj_top_eq:
   "(Rel or (\<lambda>_ _. True)) = (\<lambda>_ _. True)"