seL4 · corlewis · Aug 9, 2023 · Jul 7, 2023 · Jul 7, 2023 · Jul 7, 2023
diff --git a/lib/BCorres_UL.thy b/lib/BCorres_UL.thy
@@ -6,7 +6,7 @@
 
 theory BCorres_UL
 imports
-  Monads.NonDetMonadVCG
+  Monads.Nondet_VCG
   Crunch_Instances_NonDet
 begin
 

diff --git a/lib/Bisim_UL.thy b/lib/Bisim_UL.thy
@@ -8,9 +8,9 @@
 
 theory Bisim_UL
 imports
-  Monads.NonDetMonadVCG
+  Monads.Nondet_VCG
   Corres_UL
-  Monads.Empty_Fail
+  Monads.Nondet_Empty_Fail
 begin
 
 (* This still looks a bit wrong to me, although it is more or less what I want \<emdash> we want to be

diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
@@ -1284,7 +1284,7 @@ lemma corres_underlying_assert_assert:
 lemma corres_underlying_stateAssert_stateAssert:
   assumes "\<And>s s'. \<lbrakk> (s,s') \<in> rf_sr; P s; P' s' \<rbrakk> \<Longrightarrow> Q' s' = Q s"
   shows "corres_underlying rf_sr nf False dc P P' (stateAssert Q []) (stateAssert Q' [])"
-  by (auto simp: stateAssert_def get_def NonDetMonad.bind_def corres_underlying_def
+  by (auto simp: stateAssert_def get_def Nondet_Monad.bind_def corres_underlying_def
                  assert_def return_def fail_def assms)
 
 (* We can ignore a stateAssert in the middle of a computation even if we don't ignore abstract
@@ -1294,7 +1294,7 @@ lemma corres_stateAssert_no_fail:
      corres_underlying S False nf' r P Q (do v \<leftarrow> g; h v od) f \<rbrakk> \<Longrightarrow>
    corres_underlying S False nf' r P Q (do v \<leftarrow> g; _ \<leftarrow> stateAssert X []; h v od) f"
   apply (simp add: corres_underlying_def stateAssert_def get_def assert_def return_def no_fail_def fail_def cong: if_cong)
-  apply (clarsimp simp: split_def NonDetMonad.bind_def split: if_splits)
+  apply (clarsimp simp: split_def Nondet_Monad.bind_def split: if_splits)
   apply (erule allE, erule (1) impE)
   apply (drule (1) bspec, clarsimp)+
   done

diff --git a/lib/Crunch_Instances_NonDet.thy b/lib/Crunch_Instances_NonDet.thy
@@ -8,8 +8,8 @@ theory Crunch_Instances_NonDet
 imports
   Crunch
   Monads.WPEx
-  Monads.Empty_Fail
-  Monads.No_Fail
+  Monads.Nondet_Empty_Fail
+  Monads.Nondet_No_Fail
 begin
 
 lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE

diff --git a/lib/Crunch_Instances_Trace.thy b/lib/Crunch_Instances_Trace.thy
@@ -7,7 +7,7 @@
 theory Crunch_Instances_Trace
 imports
   Crunch
-  Monads.TraceMonadVCG
+  Monads.Trace_VCG
 begin
 
 lemmas [crunch_param_rules] = Let_def return_bind returnOk_bindE

diff --git a/lib/CutMon.thy b/lib/CutMon.thy
@@ -10,8 +10,8 @@
 
 theory CutMon
   imports
-    Monads.Empty_Fail
-    Monads.NonDetMonadVCG
+    Monads.Nondet_Empty_Fail
+    Monads.Nondet_VCG
 begin
 
 definition

diff --git a/lib/EVTutorial/EquivValidTutorial.thy b/lib/EVTutorial/EquivValidTutorial.thy
@@ -55,7 +55,7 @@ In this sense, EquivValid statements could be thought of as \<^emph>\<open>relat
 
 text \<open> This tutorial will introduce some syntactic sugar to emphasise the similarity
 between Hoare triples and EquivValid statements.
-(Here, \<open>\<top>\<top>\<close> is an alias provided by Monads.NonDetMonad for the trivial binary predicate,
+(Here, \<open>\<top>\<top>\<close> is an alias provided by Monads.Nondet\_Monad for the trivial binary predicate,
 which always returns \<open>True\<close>; similarly, there is also \<open>\<bottom>\<bottom>\<close> for \<open>False\<close>.) \<close>
 
 abbreviation

diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy
@@ -13,15 +13,15 @@ theory HaskellLib_H
 imports
   Lib
   More_Numeral_Type
-  Monads.NonDetMonadVCG
-  Monads.OptionMonad
+  Monads.Nondet_VCG
+  Monads.Reader_Option_Monad
 begin
 
 abbreviation (input) "flip \<equiv> swp"
 
 abbreviation(input) bind_drop :: "('a, 'c) nondet_monad \<Rightarrow> ('a, 'b) nondet_monad
                       \<Rightarrow> ('a, 'b) nondet_monad" (infixl ">>'_" 60)
-  where "bind_drop \<equiv> (\<lambda>x y. NonDetMonad.bind x (K_bind y))"
+  where "bind_drop \<equiv> (\<lambda>x y. Nondet_Monad.bind x (K_bind y))"
 
 lemma bind_drop_test:
   "foldr bind_drop x (return ()) = sequence_x x"

diff --git a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy
@@ -6,7 +6,7 @@
 
 theory Hoare_Sep_Tactics
 imports
-  Monads.NonDetMonadVCG
+  Monads.Nondet_VCG
   Sep_Algebra.Sep_Algebra_L4v
 begin
 

diff --git a/lib/Injection_Handler.thy b/lib/Injection_Handler.thy
@@ -7,7 +7,7 @@
 (* Definition of injection_handler and supporting lemmas. *)
 
 theory Injection_Handler
-  imports Monads.NonDetMonadVCG
+  imports Monads.Nondet_VCG
 begin
 
 definition injection_handler ::

diff --git a/lib/Insulin.thy b/lib/Insulin.thy
@@ -34,11 +34,11 @@
  *
  * Another example (l4v libraries):
  *   > desugar_term "\<lbrace> P and Q \<rbrace> f \<lbrace> \<lambda>r _. r \<in> {0..<5} \<rbrace>!" "\<lbrace>"
- *   NonDetMonad_Total.validNF (P and Q) f (\<lambda>r _. r \<in> {0\<Colon>'b..<5\<Colon>'b})
+ *   Nondet_Total.validNF (P and Q) f (\<lambda>r _. r \<in> {0\<Colon>'b..<5\<Colon>'b})
  *
  * Desugar multiple operators:
  *   > desugar_term "\<lbrace> P and Q \<rbrace> f \<lbrace> \<lambda>r _. r \<in> {0..<5} \<rbrace>!" "\<lbrace>" "and" ".."
- *   NonDetMonad.validNF (Lib.pred_conj P Q) f
+ *   Nondet_Monad.validNF (Lib.pred_conj P Q) f
  *     (\<lambda>r _. r \<in> Set_Interval.ord_class.atLeastLessThan (0\<Colon>'b) (5\<Colon>'b))
  *
  *

diff --git a/lib/Monad_Commute.thy b/lib/Monad_Commute.thy
@@ -9,7 +9,7 @@
 
 theory Monad_Commute
   imports
-    Monads.Monad_Equations
+    Monads.Nondet_Monad_Equations
     Monad_Lists (* for mapM_x *)
 begin
 

diff --git a/lib/Monad_Lists.thy b/lib/Monad_Lists.thy
@@ -10,10 +10,10 @@
 
 theory Monad_Lists
   imports
-    Monads.In_Monad
-    Monads.Det
-    Monads.Empty_Fail
-    Monads.No_Fail
+    Monads.Nondet_In_Monad
+    Monads.Nondet_Det
+    Monads.Nondet_Empty_Fail
+    Monads.Nondet_No_Fail
 begin
 
 lemma mapME_Cons:

diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy
@@ -9,9 +9,9 @@
 
 theory MonadicRewrite
 imports
-  Monads.NonDetMonadVCG
+  Monads.Nondet_VCG
   Corres_UL
-  Monads.Empty_Fail
+  Monads.Nondet_Empty_Fail
   Rules_Tac
 begin
 

diff --git a/lib/Monads/Less_Monad_Syntax.thy b/lib/Monads/Less_Monad_Syntax.thy
@@ -12,7 +12,7 @@ begin
 no_syntax
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
 
-(* remove input version of >>= from Monad_Syntax, avoid clash with NonDetMonad *)
+(* remove input version of >>= from Monad_Syntax, avoid clash with Nondet_Monad *)
 no_notation
   Monad_Syntax.bind (infixl ">>=" 54)
 

diff --git a/lib/Monads/Monad_Lib.thy b/lib/Monads/Monad_Lib.thy
@@ -5,7 +5,7 @@
  *)
 
 (* This theory collects the minimum constant definitions and lemmas for the monad definition
-   theories (NonDetMonad, TraceMonad etc). Only things that are necessary for these and needed
+   theories (Nondet_Monad, Trace_Monad etc). Only things that are necessary for these and needed
    by more than one of them should go in here. *)
 
 theory Monad_Lib

diff --git a/lib/Monads/README.md b/lib/Monads/README.md
@@ -33,7 +33,7 @@ The directory [`wp/`](./wp/) contains proof methods to reason about these monads
 in weakest-precondition style.
 
 [l4v]: https://github.com/seL4/l4v/
-[nondet]: ./NonDetMonad.thy
-[option]: ./OptionMonad.thy
-[trace]: ./TraceMonad.thy
+[nondet]: ./nondet/Nondet_Monad.thy
+[option]: ./reader_option/Reader_Option_Monad.thy
+[trace]: ./trace/Trace_Monad.thy
 [AutoCorres]: ../../tools/autocorres/
diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT
@@ -16,35 +16,38 @@ session Monads (lib) = HOL +
 
   directories
     wp
+    nondet
+    reader_option
+    trace
 
   theories
-    WhileLoopRules
-    TraceMonad
-    OptionMonadND
-    OptionMonadWP
-    Strengthen_Demo
-    TraceMonadLemmas
+    WPBang
+    WPFix
+    Eisbach_WP
+    WPI
+    WPC
+    WP_Pre
+    WP
     Datatype_Schematic
-    WhileLoopRulesCompleteness
+    Nondet_Monad
+    Nondet_Lemmas
+    Nondet_VCG
+    Nondet_More_VCG
+    Nondet_In_Monad
+    Nondet_Sat
+    Nondet_Det
+    Nondet_No_Fail
+    Nondet_No_Throw
+    Nondet_Empty_Fail
+    Nondet_Monad_Equations
+    Nondet_While_Loop_Rules
+    Nondet_While_Loop_Rules_Completeness
+    Reader_Option_Monad
+    Reader_Option_ND
+    Reader_Option_VCG
+    Trace_Monad
+    Trace_Lemmas
+    Trace_VCG
     Strengthen
-    Strengthen_Setup
-    OptionMonad
-    TraceMonadVCG
-    In_Monad
-    NonDetMonadVCG
-    NonDetMonad_Sat
-    More_NonDetMonadVCG
-    NonDetMonad
-    NonDetMonadLemmas
-    Det
-    No_Fail
-    No_Throw
-    Empty_Fail
-    Monad_Equations
-    "wp/WPBang"
-    "wp/WPFix"
-    "wp/Eisbach_WP"
-    "wp/WPI"
-    "wp/WPC"
-    "wp/WP_Pre"
-    "wp/WP"
+    Nondet_Strengthen_Setup
+    Strengthen_Demo
diff --git a/lib/Monads/Det.thy → lib/Monads/nondet/Nondet_Det.thy b/lib/Monads/Det.thy → lib/Monads/nondet/Nondet_Det.thy
@@ -5,9 +5,9 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-theory Det
+theory Nondet_Det
   imports
-    NonDetMonad
+    Nondet_Monad
 begin
 
 subsection "Determinism"

diff --git a/lib/Monads/Empty_Fail.thy → lib/Monads/nondet/Nondet_Empty_Fail.thy b/lib/Monads/Empty_Fail.thy → lib/Monads/nondet/Nondet_Empty_Fail.thy
@@ -5,16 +5,16 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-theory Empty_Fail
+theory Nondet_Empty_Fail
   imports
-    NonDetMonad
+    Nondet_Monad
     WPSimp
 begin
 
 section \<open>Monads that are wellformed w.r.t. failure\<close>
 
 text \<open>
-  Usually, well-formed monads constructed from the primitives in NonDetMonad will have the following
+  Usually, well-formed monads constructed from the primitives in Nondet_Monad will have the following
   property: if they return an empty set of results, they will have the failure flag set.\<close>
 definition empty_fail :: "('s,'a) nondet_monad \<Rightarrow> bool" where
   "empty_fail m \<equiv> \<forall>s. fst (m s) = {} \<longrightarrow> snd (m s)"

diff --git a/lib/Monads/In_Monad.thy → lib/Monads/nondet/Nondet_In_Monad.thy b/lib/Monads/In_Monad.thy → lib/Monads/nondet/Nondet_In_Monad.thy
@@ -5,8 +5,8 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-theory In_Monad
-  imports NonDetMonadLemmas
+theory Nondet_In_Monad
+  imports Nondet_Lemmas
 begin
 
 section \<open>Reasoning directly about states\<close>

diff --git a/lib/Monads/NonDetMonadLemmas.thy → lib/Monads/nondet/Nondet_Lemmas.thy b/lib/Monads/NonDetMonadLemmas.thy → lib/Monads/nondet/Nondet_Lemmas.thy
@@ -5,8 +5,8 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-theory NonDetMonadLemmas
-imports NonDetMonad
+theory Nondet_Lemmas
+imports Nondet_Monad
 begin
 
 section \<open>General Lemmas Regarding the Nondeterministic State Monad\<close>

diff --git a/lib/Monads/NonDetMonad.thy → lib/Monads/nondet/Nondet_Monad.thy b/lib/Monads/NonDetMonad.thy → lib/Monads/nondet/Nondet_Monad.thy
@@ -11,7 +11,7 @@
 
 chapter "Nondeterministic State Monad with Failure"
 
-theory NonDetMonad
+theory Nondet_Monad
   imports
     Fun_Pred_Syntax
     Monad_Lib

diff --git a/lib/Monads/MonadEq.thy → lib/Monads/nondet/Nondet_MonadEq.thy b/lib/Monads/MonadEq.thy → lib/Monads/nondet/Nondet_MonadEq.thy
@@ -19,10 +19,10 @@
  *
  * are added to the "monad_eq" set.
  *)
-theory MonadEq
+theory Nondet_MonadEq
   imports
-    In_Monad
-    NonDetMonadVCG
+    Nondet_In_Monad
+    Nondet_VCG
 begin
 
 (* Setup "monad_eq" attributes. *)

diff --git a/lib/Monads/MonadEq_Lemmas.thy → lib/Monads/nondet/Nondet_MonadEq_Lemmas.thy b/lib/Monads/MonadEq_Lemmas.thy → lib/Monads/nondet/Nondet_MonadEq_Lemmas.thy
@@ -11,10 +11,10 @@
 
    If you are planning to use the monad_eq method, this is the theory you should import.
 
-   See MonadEq.thy for definition and description of the method. *)
+   See Nondet_MonadEq.thy for definition and description of the method. *)
 
-theory MonadEq_Lemmas
-  imports MonadEq
+theory Nondet_MonadEq_Lemmas
+  imports Nondet_MonadEq
 begin
 
 lemma snd_return[monad_eq]:

diff --git a/lib/Monads/Monad_Equations.thy → lib/Monads/nondet/Nondet_Monad_Equations.thy b/lib/Monads/Monad_Equations.thy → lib/Monads/nondet/Nondet_Monad_Equations.thy
@@ -8,11 +8,11 @@
 (* Equations between monads. Conclusions of the form "f = g" where f and g are monads.
    Should not be Hoare triples (those go into a different theory). *)
 
-theory Monad_Equations
+theory Nondet_Monad_Equations
   imports
-    Empty_Fail
-    No_Fail
-    MonadEq_Lemmas
+    Nondet_Empty_Fail
+    Nondet_No_Fail
+    Nondet_MonadEq_Lemmas
 begin
 
 lemmas assertE_assert = assertE_liftE
@@ -146,7 +146,7 @@ lemma unlessE_throw_catch_If:
 lemma whenE_bindE_throwError_to_if:
   "whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)"
   unfolding whenE_def bindE_def
-  by (auto simp: NonDetMonad.lift_def throwError_def returnOk_def)
+  by (auto simp: Nondet_Monad.lift_def throwError_def returnOk_def)
 
 lemma alternative_liftE_returnOk:
   "(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)"
@@ -431,7 +431,7 @@ lemma liftE_fail[simp]: "liftE fail = fail"
 
 lemma catch_bind_distrib:
   "do _ <- m <catch> h; f od = (doE m; liftE f odE <catch> (\<lambda>x. do h x; f od))"
-  by (force simp: catch_def bindE_def bind_assoc liftE_def NonDetMonad.lift_def bind_def
+  by (force simp: catch_def bindE_def bind_assoc liftE_def Nondet_Monad.lift_def bind_def
                   split_def return_def throwError_def
             split: sum.splits)
 
@@ -451,7 +451,7 @@ lemma catch_is_if:
    od"
   apply (simp add: bindE_def catch_def bind_assoc cong: if_cong)
   apply (rule bind_cong, rule refl)
-  apply (clarsimp simp: NonDetMonad.lift_def throwError_def split: sum.splits)
+  apply (clarsimp simp: Nondet_Monad.lift_def throwError_def split: sum.splits)
   done
 
 lemma liftE_K_bind: "liftE ((K_bind (\<lambda>s. A s)) x) = K_bind (liftE (\<lambda>s. A s)) x"