squash: move in_omonad to Reader_Option_Monad.thy

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Feb 29, 2024 · 8610075 · 8610075
1 parent ce911d2
commit 8610075
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 4 deletions.
diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy
@@ -130,8 +130,6 @@ lemmas omonad_simps [simp] =
   gets_the_throwError gets_the_assert gets_the_Some
   gets_the_oapply_comp
 
-lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq in_opt_pred Let_def
-
 
 section "Relation between option monad loops and non-deterministic monad loops."
 

diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy
@@ -482,6 +482,8 @@ lemma obindK_is_opt_map:
   "f \<bind> (\<lambda>x. K $ g x) = f |> g"
   by (simp add: obind_def opt_map_def)
 
+lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq in_opt_pred Let_def
+
 
 section \<open>"While" loops over option monad.\<close>
 

diff --git a/lib/Monads/trace/Trace_Reader_Option.thy b/lib/Monads/trace/Trace_Reader_Option.thy
@@ -130,8 +130,6 @@ lemmas omonad_simps [simp] =
   gets_the_throwError gets_the_assert gets_the_Some
   gets_the_oapply_comp
 
-lemmas in_omonad = bind_eq_Some_conv in_obind_eq in_opt_map_eq in_opt_pred Let_def
-
 
 section "Relation between option monad loops and trace monad loops."