squash lib/monads/trace: suggestions from PR review

Signed-off-by: Corey Lewis <[email protected]>

lib/Monads/trace/Trace_Empty_Fail.thy

@@ -21,8 +21,9 @@ definition empty_fail :: "('s,'a) tmonad \<Rightarrow> bool" where
   "empty_fail m \<equiv> \<forall>s. mres (m s) = {} \<longrightarrow> Failed \<in> snd ` (m s)"
 
 text \<open>Useful in forcing otherwise unknown executions to have the @{const empty_fail} property.\<close>
-\<comment> \<open>definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" where
-  "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)"\<close>
+definition mk_ef ::
+  "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set" where
+  "mk_ef S \<equiv> if mres S = {} then S \<union> {([], Failed)} else S"
 
 
 subsection \<open>WPC setup\<close>
@@ -66,7 +67,7 @@ subsection \<open>Wellformed monads\<close>
 
 (*
   Collect generic empty_fail lemmas here:
-   - naming convention is emtpy_fail_NAME.
+   - naming convention is empty_fail_NAME.
    - add lemmas with assumptions to [empty_fail_cond] set
    - add lemmas without assumption to [empty_fail_term] set
 *)
@@ -195,9 +196,9 @@ lemma empty_fail_assert_opt[empty_fail_term]:
   "empty_fail (assert_opt x)"
   by (simp add: assert_opt_def empty_fail_term split: option.splits)
 
-\<comment> \<open>lemma empty_fail_mk_ef[empty_fail_term]:
+lemma empty_fail_mk_ef[empty_fail_term]:
   "empty_fail (mk_ef o m)"
-  by (simp add: empty_fail_def mk_ef_def)\<close>
+  by (simp add: empty_fail_def mk_ef_def)
 
 lemma empty_fail_gets_the[empty_fail_term]:
   "empty_fail (gets_the f)"

lib/Monads/trace/Trace_Monad.thy

@@ -727,16 +727,16 @@ section "Combinators that have conditions with side effects"
 definition notM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
   "notM m = do c \<leftarrow> m; return (\<not> c) od"
 
-definition
-  whileM :: "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, unit) tmonad" where
+definition whileM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, unit) tmonad" where
   "whileM C B \<equiv> do
     c \<leftarrow> C;
     whileLoop (\<lambda>c s. c) (\<lambda>_. do B; C od) c;
     return ()
   od"
 
-definition
-  ifM :: "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow>
+definition ifM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow> ('s, 'a) tmonad \<Rightarrow>
           ('s, 'a) tmonad" where
   "ifM test t f = do
     c \<leftarrow> test;
@@ -751,12 +751,12 @@ definition ifME ::
     if c then t else f
    odE"
 
-definition
-  whenM :: "('s, bool) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
+definition whenM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" where
   "whenM t m = ifM t m (return ())"
 
-definition
-  orM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
+definition orM ::
+  "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
   "orM a b = ifM a (return True) b"
 
 definition

lib/Monads/trace/Trace_Monad_Equations.thy

@@ -47,7 +47,7 @@ lemma throwError_bind:
 
 lemma bind_bindE_assoc:
   "((f >>= g) >>=E h)
-    = f >>= (\<lambda>rv. g rv >>=E h)"
+   = f >>= (\<lambda>rv. g rv >>=E h)"
   by (simp add: bindE_def bind_assoc)
 
 lemma returnOk_bind:
@@ -67,7 +67,7 @@ lemma cart_singleton_image:
 
 lemma liftE_bindE_handle:
   "((liftE f >>=E (\<lambda>x. g x)) <handle> h)
-      = f >>= (\<lambda>x. g x <handle> h)"
+   = f >>= (\<lambda>x. g x <handle> h)"
   by (simp add: liftE_bindE handleE_def handleE'_def
                 bind_assoc)
 
@@ -89,7 +89,7 @@ lemma liftE_bindE_assoc:
 
 lemma unlessE_throw_catch_If:
   "catch (unlessE P (throwError e) >>=E f) g
-      = (if P then catch (f ()) g else g e)"
+   = (if P then catch (f ()) g else g e)"
   by (simp add: unlessE_def catch_throwError split: if_split)
 
 lemma whenE_bindE_throwError_to_if:
@@ -125,13 +125,13 @@ lemma all_rv_choice_fn_eq_pred:
 
 lemma all_rv_choice_fn_eq:
   "\<lbrakk> \<And>rv. \<exists>fn. f rv = g fn \<rbrakk>
-    \<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))"
+   \<Longrightarrow> \<exists>fn. f = (\<lambda>rv. g (fn rv))"
   using all_rv_choice_fn_eq_pred[where f=f and g=g and P=\<top>]
   by (simp add: fun_eq_iff)
 
 lemma gets_the_eq_bind:
   "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
-     \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')"
+   \<Longrightarrow> \<exists>fn. (f >>= g) = gets_the (fn o fn')"
   apply (clarsimp dest!: all_rv_choice_fn_eq)
   apply (rule_tac x="\<lambda>s. case (fn s) of None \<Rightarrow> None | Some v \<Rightarrow> fna v s" in exI)
   apply (simp add: gets_the_def bind_assoc exec_gets
@@ -141,7 +141,7 @@ lemma gets_the_eq_bind:
 
 lemma gets_the_eq_bindE:
   "\<lbrakk> \<exists>fn. f = gets_the (fn o fn'); \<And>rv. \<exists>fn. g rv = gets_the (fn o fn') \<rbrakk>
-     \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')"
+   \<Longrightarrow> \<exists>fn. (f >>=E g) = gets_the (fn o fn')"
   apply (simp add: bindE_def)
   apply (erule gets_the_eq_bind)
   apply (simp add: lift_def gets_the_returns split: sum.split)
@@ -167,9 +167,9 @@ lemma ex_const_function:
 
 lemma gets_the_condsE:
   "(\<exists>fn. whenE P f = gets_the (fn o fn'))
-            = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))"
+   = (P \<longrightarrow> (\<exists>fn. f = gets_the (fn o fn')))"
   "(\<exists>fn. unlessE P g = gets_the (fn o fn'))
-            = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))"
+   = (\<not> P \<longrightarrow> (\<exists>fn. g = gets_the (fn o fn')))"
   by (simp add: whenE_def unlessE_def gets_the_returns ex_const_function
          split: if_split)+
 
@@ -183,7 +183,7 @@ lemma liftME_return:
 
 lemma fold_bindE_into_list_case:
   "(doE v \<leftarrow> f; case_list (g v) (h v) x odE)
-      = (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)"
+   = (case_list (doE v \<leftarrow> f; g v odE) (\<lambda>x xs. doE v \<leftarrow> f; h v x xs odE) x)"
   by (simp split: list.split)
 
 lemma whenE_liftE:
@@ -230,23 +230,22 @@ lemma modify_id_return:
  "modify id = return ()"
   by (simp add: simpler_modify_def return_def)
 
-
 lemma liftE_bind_return_bindE_returnOk:
   "liftE (v >>= (\<lambda>rv. return (f rv)))
-     = (liftE v >>=E (\<lambda>rv. returnOk (f rv)))"
+   = (liftE v >>=E (\<lambda>rv. returnOk (f rv)))"
   by (simp add: liftE_bindE, simp add: liftE_def returnOk_def)
 
 lemma bind_eqI:
   "g = g' \<Longrightarrow> f >>= g = f >>= g'" by simp
 
 lemma unlessE_throwError_returnOk:
   "(if P then returnOk v else throwError x)
-    = (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))"
+   = (unlessE P (throwError x) >>=E (\<lambda>_. returnOk v))"
   by (cases P, simp_all add: unlessE_def)
 
 lemma gets_the_bind_eq:
   "\<lbrakk> f s = Some x; g x s = h s \<rbrakk>
-    \<Longrightarrow> (gets_the f >>= g) s = h s"
+   \<Longrightarrow> (gets_the f >>= g) s = h s"
   by (simp add: gets_the_def bind_assoc exec_gets assert_opt_def)
 
 lemma zipWithM_x_modify:
@@ -261,7 +260,7 @@ lemma zipWithM_x_modify:
 
 lemma assert2:
   "(do v1 \<leftarrow> assert P; v2 \<leftarrow> assert Q; c od)
-     = (do v \<leftarrow> assert (P \<and> Q); c od)"
+   = (do v \<leftarrow> assert (P \<and> Q); c od)"
   by (simp add: assert_def split: if_split)
 
 lemma assert_opt_def2:
@@ -270,20 +269,20 @@ lemma assert_opt_def2:
 
 lemma gets_assert:
   "(do v1 \<leftarrow> assert v; v2 \<leftarrow> gets f; c v1 v2 od)
-     = (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)"
+   = (do v2 \<leftarrow> gets f; v1 \<leftarrow> assert v; c v1 v2 od)"
   by (simp add: simpler_gets_def return_def assert_def fail_def bind_def
          split: if_split)
 
 lemma modify_assert:
   "(do v2 \<leftarrow> modify f; v1 \<leftarrow> assert v; c v1 od)
-    = (do v1 \<leftarrow> assert v; v2 \<leftarrow> modify f; c v1 od)"
+   = (do v1 \<leftarrow> assert v; v2 \<leftarrow> modify f; c v1 od)"
   by (simp add: simpler_modify_def return_def assert_def fail_def bind_def
          split: if_split)
 
 lemma gets_fold_into_modify:
   "do x \<leftarrow> gets f; modify (g x) od = modify (\<lambda>s. g (f s) s)"
   "do x \<leftarrow> gets f; _ \<leftarrow> modify (g x); h od
-     = do modify (\<lambda>s. g (f s) s); h od"
+   = do modify (\<lambda>s. g (f s) s); h od"
   by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets
                     exec_get exec_put)