From f6da36521d9e8734f642cccb31248c511fb7b089 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Thu, 22 Feb 2024 10:22:41 +1100
Subject: [PATCH] lib+spec+proof+tools: update for reader_option refactor

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 lib/NonDetMonadLemmaBucket.thy              | 2 +-
 lib/clib/Corres_UL_C.thy                    | 2 +-
 proof/sep-capDL/Lookups_D.thy               | 2 +-
 spec/design/m-skel/AARCH64/MachineTypes.thy | 3 +--
 spec/design/m-skel/ARM/MachineTypes.thy     | 3 +--
 spec/design/m-skel/ARM_HYP/MachineTypes.thy | 3 +--
 spec/design/m-skel/RISCV64/MachineTypes.thy | 3 +--
 spec/design/m-skel/X64/MachineTypes.thy     | 3 +--
 tools/autocorres/NonDetMonadEx.thy          | 4 ++--
 tools/autocorres/TypeStrengthen.thy         | 1 -
 10 files changed, 10 insertions(+), 16 deletions(-)

diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy
index 7d0272dda8..bcc1e310c1 100644
--- a/lib/NonDetMonadLemmaBucket.thy
+++ b/lib/NonDetMonadLemmaBucket.thy
@@ -19,7 +19,7 @@ imports
   Injection_Handler
   Monads.Nondet_While_Loop_Rules_Completeness
   "Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 lemma distinct_tuple_helper:
diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
index d6630dc80f..7580326cf6 100644
--- a/lib/clib/Corres_UL_C.thy
+++ b/lib/clib/Corres_UL_C.thy
@@ -14,7 +14,7 @@ imports
   CParser.LemmaBucket_C
   Lib.LemmaBucket
   SIMPL_Lemmas
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 declare word_neq_0_conv [simp del]
diff --git a/proof/sep-capDL/Lookups_D.thy b/proof/sep-capDL/Lookups_D.thy
index 0fca39865a..1396177f23 100644
--- a/proof/sep-capDL/Lookups_D.thy
+++ b/proof/sep-capDL/Lookups_D.thy
@@ -7,7 +7,7 @@
 theory Lookups_D
 imports
   "DSpec.Syscall_D"
-  "Monads.Reader_Option_ND"
+  "Monads.Nondet_Reader_Option"
 begin
 
 type_synonym 'a lookup = "cdl_state \<Rightarrow> 'a option"
diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy
index 98c96196f3..7e750b414c 100644
--- a/spec/design/m-skel/AARCH64/MachineTypes.thy
+++ b/spec/design/m-skel/AARCH64/MachineTypes.thy
@@ -9,8 +9,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin
diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy
index 6455feb8a4..28613511b3 100644
--- a/spec/design/m-skel/ARM/MachineTypes.thy
+++ b/spec/design/m-skel/ARM/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Setup_Locale
   Platform
 begin
diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy
index 7e895ec27b..50d1b6a192 100644
--- a/spec/design/m-skel/ARM_HYP/MachineTypes.thy
+++ b/spec/design/m-skel/ARM_HYP/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Setup_Locale
   Platform
 begin
diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy
index 234e80542c..01ba79fbc3 100644
--- a/spec/design/m-skel/RISCV64/MachineTypes.thy
+++ b/spec/design/m-skel/RISCV64/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin
diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy
index e8465d4e15..54bb5a930b 100644
--- a/spec/design/m-skel/X64/MachineTypes.thy
+++ b/spec/design/m-skel/X64/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin
diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy
index 3b54035cad..3f836354cb 100644
--- a/tools/autocorres/NonDetMonadEx.thy
+++ b/tools/autocorres/NonDetMonadEx.thy
@@ -16,7 +16,7 @@ imports
   "Monads.Nondet_More_VCG"
   "Monads.Nondet_No_Throw"
   "Monads.Nondet_No_Fail"
-  "Monads.Reader_Option_ND"
+  "Monads.Nondet_Reader_Option"
 begin
 
 (*
@@ -276,7 +276,7 @@ lemma whileLoop_to_fold:
            (\<lambda>r. return (Q r))
            i s) = return (if P i \<le> x then fold (\<lambda>i r. (Q r)) [unat (P i) ..< unat x] i else i) s"
     (is "?LHS s = return (?RHS x) s")
-  apply (subst Reader_Option_ND.gets_the_return [symmetric])
+  apply (subst gets_the_return [symmetric])
   apply (subst gets_the_whileLoop)
   apply (rule gets_the_to_return)
   apply (subst owhile_to_fold)
diff --git a/tools/autocorres/TypeStrengthen.thy b/tools/autocorres/TypeStrengthen.thy
index bdebf9aff5..5106ca596c 100644
--- a/tools/autocorres/TypeStrengthen.thy
+++ b/tools/autocorres/TypeStrengthen.thy
@@ -14,7 +14,6 @@
 theory TypeStrengthen
 imports
   L2Defs
-  "Monads.Reader_Option_ND"
   ExecConcrete
 begin