From 8610075a9035b827bfcce18f13362406fd965968 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Thu, 29 Feb 2024 21:11:42 +1100 Subject: [PATCH] squash: move in_omonad to Reader_Option_Monad.thy Signed-off-by: Corey Lewis --- lib/Monads/nondet/Nondet_Reader_Option.thy | 2 -- lib/Monads/reader_option/Reader_Option_Monad.thy | 2 ++ lib/Monads/trace/Trace_Reader_Option.thy | 2 -- 3 files changed, 2 insertions(+), 4 deletions(-) diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy index 72a4f22b88..918884bcd1 100644 --- 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 index c8ee9a15f6..686dd1d626 100644 --- 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 \ (\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 \"While" loops over option monad.\ diff --git a/lib/Monads/trace/Trace_Reader_Option.thy b/lib/Monads/trace/Trace_Reader_Option.thy index 33a0325ed8..27f59281d0 100644 --- 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."