From ae6b0764a452d4db9f5e5d62f6a14ea4165859c8 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Mon, 14 Aug 2023 17:33:28 +1000
Subject: [PATCH] lib: update for trace monad refactor

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/Crunch_Instances_Trace.thy        | 3 ++-
 lib/concurrency/Atomicity_Lib.thy     | 7 ++++---
 lib/concurrency/Prefix_Refinement.thy | 4 +---
 lib/concurrency/Triv_Refinement.thy   | 4 ++--
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy
index e7966c63b8..bf8acb44b1 100644
--- 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
index 728dbdac88..8f50ac0e02 100644
--- 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
index 774d3360f6..20f0e5bf9b 100644
--- 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
index caefd59834..b31995381f 100644
--- 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