More Nondet Monad improvements

lib/Monads/nondet/Nondet_Det.thy

@@ -59,6 +59,10 @@ lemma bind_detI[simp, intro!]:
   apply clarsimp
   done
 
+lemma det_modify[iff]:
+  "det (modify f)"
+  by (simp add: modify_def)
+
 lemma the_run_stateI:
   "fst (M s) = {s'} \<Longrightarrow> the_run_state M s = s'"
   by (simp add: the_run_state_def)

lib/Monads/nondet/Nondet_Empty_Fail.thy

@@ -63,7 +63,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
 *)

lib/Monads/nondet/Nondet_In_Monad.thy

@@ -38,9 +38,13 @@ lemma in_bindE_L:
   by (simp add: bindE_def bind_def)
      (force simp: return_def throwError_def lift_def split_def split: sum.splits if_split_asm)
 
+lemma in_return:
+  "(r, s') \<in> fst (return v s) = (r = v \<and> s' = s)"
+  by (simp add: return_def)
+
 lemma in_liftE:
   "((v, s') \<in> fst (liftE f s)) = (\<exists>v'. v = Inr v' \<and> (v', s') \<in> fst (f s))"
-  by (force simp add: liftE_def bind_def return_def split_def)
+  by (force simp: liftE_def in_bind in_return)
 
 lemma in_whenE:
   "((v, s') \<in> fst (whenE P f s)) = ((P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (\<not>P \<longrightarrow> v = Inr () \<and> s' = s))"
@@ -58,10 +62,6 @@ lemma in_fail:
   "r \<in> fst (fail s) = False"
   by (simp add: fail_def)
 
-lemma in_return:
-  "(r, s') \<in> fst (return v s) = (r = v \<and> s' = s)"
-  by (simp add: return_def)
-
 lemma in_assert:
   "(r, s') \<in> fst (assert P s) = (P \<and> s' = s)"
   by (simp add: assert_def return_def fail_def)
@@ -90,6 +90,18 @@ lemma in_when:
   "(v, s') \<in> fst (when P f s) = ((P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (\<not>P \<longrightarrow> v = () \<and> s' = s))"
   by (simp add: when_def in_return)
 
+lemma in_unless:
+  "(v, s') \<in> fst (unless P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))"
+  by (simp add: unless_def in_when)
+
+lemma in_unlessE:
+  "(v, s') \<in> fst (unlessE P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))"
+  by (simp add: unlessE_def in_returnOk)
+
+lemma inl_unlessE:
+  "((Inl x, s') \<in> fst (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> fst (f s))"
+  by (auto simp add: in_unlessE)
+
 lemma in_modify:
   "(v, s') \<in> fst (modify f s) = (s'=f s \<and> v = ())"
   by (simp add: modify_def bind_def get_def put_def)
@@ -112,12 +124,11 @@ lemma in_bindE:
     (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inr rv', s'') \<in> fst (f s)))"
   by (force simp: bindE_def bind_def lift_def throwError_def return_def  split: sum.splits)
 
-(* FIXME lib: remove unlessE_whenE + unless_when here and replace with in_unless lemmas *)
 lemmas in_monad = inl_whenE in_whenE in_liftE in_bind in_bindE_L
                   in_bindE_R in_returnOk in_throwError in_fail
                   in_assertE in_assert in_return in_assert_opt
-                  in_get in_gets in_put in_when unlessE_whenE
-                  unless_when in_modify gets_the_in_monad
+                  in_get in_gets in_put in_when inl_unlessE in_unlessE
+                  in_unless in_modify gets_the_in_monad
                   in_alternative in_liftM
 
 lemma bind_det_exec:

lib/Monads/nondet/Nondet_Lemmas.thy

@@ -6,7 +6,7 @@
  *)
 
 theory Nondet_Lemmas
-imports Nondet_Monad
+  imports Nondet_Monad
 begin
 
 section \<open>General Lemmas Regarding the Nondeterministic State Monad\<close>
@@ -15,12 +15,12 @@ subsection \<open>Congruence Rules for the Function Package\<close>
 
 lemma bind_cong[fundef_cong]:
   "\<lbrakk> f = f'; \<And>v s s'. (v, s') \<in> fst (f' s) \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
-  by (auto simp: bind_def Let_def split_def intro: rev_image_eqI)
+  by (auto simp: bind_def split_def)
 
 lemma bind_apply_cong [fundef_cong]:
   "\<lbrakk> f s = f' s'; \<And>rv st. (rv, st) \<in> fst (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
    \<Longrightarrow> (f >>= g) s = (f' >>= g') s'"
-  by (auto simp: bind_def split_def intro: SUP_cong [OF refl] intro: rev_image_eqI)
+  by (auto simp: bind_def split_def)
 
 lemma bindE_cong[fundef_cong]:
   "\<lbrakk> M = M' ; \<And>v s s'. (Inr v, s') \<in> fst (M' s) \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'"

lib/Monads/nondet/Nondet_Monad.thy

@@ -110,16 +110,18 @@ definition alternative ::
   "('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad" (infixl "\<sqinter>" 20) where
   "f \<sqinter> g \<equiv> \<lambda>s. (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s))"
 
-text \<open>A variant of @{text select} that takes a pair. The first component
-  is a set as in normal @{text select}, the second component indicates
-  whether the execution failed. This is useful to lift monads between
-  different state spaces.\<close>
+text \<open>
+  A variant of @{text select} that takes a pair. The first component is a set
+  as in normal @{text select}, the second component indicates whether the
+  execution failed. This is useful to lift monads between different state
+  spaces.\<close>
 definition select_f :: "'a set \<times> bool  \<Rightarrow> ('s,'a) nondet_monad" where
   "select_f S \<equiv> \<lambda>s. (fst S \<times> {s}, snd S)"
 
-text \<open>@{text select_state} takes a relationship between
-  states, and outputs nondeterministically a state
-  related to the input state.\<close>
+text \<open>
+  @{text state_select} takes a relationship between states, and outputs
+  nondeterministically a state related to the input state. Fails if no such
+  state exists.\<close>
 definition state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) nondet_monad" where
   "state_select r \<equiv> \<lambda>s. ((\<lambda>x. ((), x)) ` {s'. (s, s') \<in> r}, \<not> (\<exists>s'. (s, s') \<in> r))"
 
@@ -184,7 +186,6 @@ text \<open>
 definition gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) nondet_monad" where
   "gets_the f \<equiv> gets f >>= assert_opt"
 
-
 text \<open>
   Get a map (such as a heap) from the current state and apply an argument to the map.
   Fail if the map returns @{const None}, otherwise return the value.\<close>
@@ -499,6 +500,21 @@ primrec filterM :: "('a \<Rightarrow> ('s, bool) nondet_monad) \<Rightarrow> 'a
      return (if b then (x # ys) else ys)
    od"
 
+text \<open>An alternative definition of @{term state_select}\<close>
+lemma state_select_def2:
+  "state_select r \<equiv> (do
+    s \<leftarrow> get;
+    S \<leftarrow> return {s'. (s, s') \<in> r};
+    assert (S \<noteq> {});
+    s' \<leftarrow> select S;
+    put s'
+  od)"
+  apply (clarsimp simp add: state_select_def get_def return_def assert_def fail_def select_def
+                            put_def bind_def fun_eq_iff
+                    intro!: eq_reflection)
+  apply fastforce
+  done
+
 
 section "Catching and Handling Exceptions"
 
@@ -609,16 +625,16 @@ section "Combinators that have conditions with side effects"
 definition notM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
   "notM m = do c \<leftarrow> m; return (\<not> c) od"
 
-definition
-  whileM :: "('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
+definition whileM ::
+  "('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" 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) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow>
+definition ifM ::
+  "('s, bool) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow>
           ('s, 'a) nondet_monad" where
   "ifM test t f = do
     c \<leftarrow> test;
@@ -633,16 +649,16 @@ definition ifME ::
     if c then t else f
    odE"
 
-definition
-  whenM :: "('s, bool) nondet_monad \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
+definition whenM ::
+  "('s, bool) nondet_monad \<Rightarrow> ('s, unit) nondet_monad \<Rightarrow> ('s, unit) nondet_monad" where
   "whenM t m = ifM t m (return ())"
 
-definition
-  orM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
+definition orM ::
+  "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
   "orM a b = ifM a (return True) b"
 
-definition
-  andM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
+definition andM ::
+  "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
   "andM a b = ifM a b (return False)"
 
 end