lib: update for trace refactor

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
seL4 · Aug 14, 2023 · 64e0efd · 64e0efd
1 parent 0f126da
commit 64e0efd
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 9 deletions.
diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy
@@ -7,7 +7,8 @@
 theory Crunch_Instances_Trace
 imports
   Crunch
-  Monads.Trace_VCG
+  Monads.Trace_No_Fail
+  Monads.Trace_RG
 begin
 
 lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE

diff --git a/lib/concurrency/Atomicity_Lib.thy b/lib/concurrency/Atomicity_Lib.thy
@@ -5,8 +5,9 @@
  *)
 theory Atomicity_Lib
 
-imports "Prefix_Refinement"
-
+imports
+  Prefix_Refinement
+  Monads.Trace_Det
 begin
 
 text \<open>This library introduces a number of proofs about the question of
@@ -186,7 +187,7 @@ lemma repeat_n_nothing:
 lemma repeat_nothing:
   "repeat (\<lambda>_. {}) = return ()"
   by (simp add: repeat_def bind_def select_def repeat_n_nothing
-                Sigma_def if_fun_lift UN_If_distrib return_def
+                Sigma_def if_distribR UN_If_distrib return_def
            cong del: image_cong_simp)
 
 lemma detrace_env_steps:

diff --git a/lib/concurrency/Prefix_Refinement.thy b/lib/concurrency/Prefix_Refinement.thy
@@ -7,8 +7,6 @@ theory Prefix_Refinement
 
 imports
   Triv_Refinement
-  "Monads.Trace_Lemmas"
-
 begin
 
 section \<open>Definition of prefix fragment refinement.\<close>
@@ -1242,7 +1240,7 @@ lemma prefix_refinement_repeat:
       apply simp
       apply (rule prefix_refinement_repeat_n, assumption+)
       apply (rule validI_weaken_pre, assumption, simp)
-     apply (wp select_wp)
+     apply wp
     apply wp
    apply clarsimp
   apply clarsimp

diff --git a/lib/concurrency/Triv_Refinement.thy b/lib/concurrency/Triv_Refinement.thy
@@ -6,8 +6,8 @@
 theory Triv_Refinement
 
 imports
-  "Monads.Trace_VCG"
-  "Monads.Strengthen"
+  "Monads.Trace_RG"
+  "Monads.Trace_Strengthen_Setup"
 
 begin