diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy
index 6675f35f295..691b929717d 100644
--- a/lib/Monads/Fun_Pred_Syntax.thy
+++ b/lib/Monads/Fun_Pred_Syntax.thy
@@ -173,6 +173,17 @@ lemmas pred_neg_bot_eq[simp] =
    entirely in the future *)
 
 
+subsection "Simplification Rules for Lifted And/Or"
+
+lemma bipred_disj_op_eq[simp]:
+  "reflp R \<Longrightarrow> ((=) or R) = R"
+  "reflp R \<Longrightarrow> (R or (=)) = R"
+  by (auto simp: reflp_def)
+
+lemma bipred_le_true[simp]: "R \<le> \<top>\<top>"
+  by clarsimp
+
+
 section \<open>Examples\<close>
 
 experiment
diff --git a/lib/Monads/Monad_Lib.thy b/lib/Monads/Monad_Lib.thy
index 9147968b1c0..d1dc62120a5 100644
--- a/lib/Monads/Monad_Lib.thy
+++ b/lib/Monads/Monad_Lib.thy
@@ -69,4 +69,8 @@ lemma sum_all_ex[simp]:
   "(\<forall>a. x \<noteq> Inr a) = (\<exists>a. x = Inl a)"
   by (metis Inr_not_Inl sum.exhaust)+
 
+lemma context_disjE:
+  "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; \<lbrakk>\<not>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
+  by auto
+
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy
index 02dd0b2a3cf..472ec988afe 100644
--- a/lib/Monads/trace/Trace_Empty_Fail.thy
+++ b/lib/Monads/trace/Trace_Empty_Fail.thy
@@ -14,14 +14,16 @@ begin
 section \<open>Monads that are wellformed w.r.t. failure\<close>
 
 text \<open>
-  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)"
+  Usually, well-formed monads constructed from the primitives in Trace_Monad will have the following
+  property: if they return an empty set of completed results, there exists a trace corresponding to
+  a failed result.\<close>
+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>
-definition mk_ef :: "'a set \<times> bool \<Rightarrow> 'a set \<times> bool" where
-  "mk_ef S \<equiv> (fst S, fst S = {} \<or> snd S)"
+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>
@@ -36,34 +38,36 @@ wpc_setup "\<lambda>m. empty_fail m" wpc_helper_empty_fail_final
 subsection \<open>@{const empty_fail} intro/dest rules\<close>
 
 lemma empty_failI:
-  "(\<And>s. fst (m s) = {} \<Longrightarrow> snd (m s)) \<Longrightarrow> empty_fail m"
+  "(\<And>s. mres (m s) = {} \<Longrightarrow> Failed \<in> snd ` (m s)) \<Longrightarrow> empty_fail m"
   by (simp add: empty_fail_def)
 
 lemma empty_failD:
-  "\<lbrakk> empty_fail m; fst (m s) = {} \<rbrakk> \<Longrightarrow> snd (m s)"
+  "\<lbrakk> empty_fail m; mres (m s) = {} \<rbrakk> \<Longrightarrow> Failed \<in> snd ` (m s)"
   by (simp add: empty_fail_def)
 
 lemma empty_fail_not_snd:
-  "\<lbrakk> \<not> snd (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> fst (m s)"
+  "\<lbrakk> Failed \<notin> snd ` (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> mres (m s)"
   by (fastforce simp: empty_fail_def)
 
 lemmas empty_failD2 = empty_fail_not_snd[rotated]
 
 lemma empty_failD3:
-  "\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}"
+  "\<lbrakk> empty_fail f; Failed \<notin> snd ` (f s) \<rbrakk> \<Longrightarrow> mres (f s) \<noteq> {}"
   by (drule(1) empty_failD2, clarsimp)
 
 lemma empty_fail_bindD1:
   "empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
   unfolding empty_fail_def bind_def
-  by (fastforce simp: split_def image_image)
+  apply clarsimp
+  apply (drule_tac x=s in spec)
+  by (force simp: split_def mres_def vimage_def split: tmres.splits)
 
 
 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
 *)
@@ -91,32 +95,53 @@ lemma empty_fail_If_applied[empty_fail_cond]:
 
 lemma empty_fail_put[empty_fail_term]:
   "empty_fail (put f)"
-  by (simp add: put_def empty_fail_def)
+  by (simp add: put_def empty_fail_def mres_def vimage_def)
 
 lemma empty_fail_modify[empty_fail_term]:
   "empty_fail (modify f)"
-  by (simp add: empty_fail_def simpler_modify_def)
+  by (simp add: empty_fail_def simpler_modify_def mres_def vimage_def)
 
 lemma empty_fail_gets[empty_fail_term]:
   "empty_fail (gets f)"
-  by (simp add: empty_fail_def simpler_gets_def)
+  by (simp add: empty_fail_def simpler_gets_def mres_def vimage_def)
 
 lemma empty_fail_select[empty_fail_cond]:
   "S \<noteq> {} \<Longrightarrow> empty_fail (select S)"
-  by (simp add: empty_fail_def select_def)
-
-lemma empty_fail_select_f[empty_fail_cond]:
-  assumes ef: "fst S = {} \<Longrightarrow> snd S"
-  shows "empty_fail (select_f S)"
-  by (fastforce simp add: empty_fail_def select_f_def intro: ef)
+  by (simp add: empty_fail_def select_def mres_def image_def)
+
+lemma mres_bind_empty:
+  "mres ((f >>= g) s) = {}
+   \<Longrightarrow> mres (f s) = {} \<or> (\<forall>res\<in>mres (f s). mres (g (fst res) (snd res)) = {})"
+  apply clarsimp
+  apply (clarsimp simp: mres_def split_def vimage_def bind_def)
+  apply (rename_tac rv s' trace)
+  apply (drule_tac x=rv in spec, drule_tac x=s' in spec)
+  apply (clarsimp simp: image_def)
+  apply fastforce
+  done
+
+lemma bind_FailedI1:
+  "Failed \<in> snd ` f s \<Longrightarrow> Failed \<in> snd ` (f >>= g) s"
+  by (force simp: bind_def vimage_def)
+
+lemma bind_FailedI2:
+  "\<lbrakk>\<forall>res\<in>mres (f s). Failed \<in> snd ` (g (fst res) (snd res)); mres (f s) \<noteq> {}\<rbrakk>
+   \<Longrightarrow> Failed \<in> snd ` (f >>= g) s"
+  by (force simp: bind_def mres_def image_def split_def)
 
 lemma empty_fail_bind[empty_fail_cond]:
   "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)"
-  by (fastforce simp: bind_def empty_fail_def split_def)
+  unfolding empty_fail_def
+  apply clarsimp
+  apply (drule mres_bind_empty)
+  apply (erule context_disjE)
+   apply (fastforce intro: bind_FailedI1)
+  apply (fastforce intro!: bind_FailedI2)
+  done
 
 lemma empty_fail_return[empty_fail_term]:
   "empty_fail (return x)"
-  by (simp add: empty_fail_def return_def)
+  by (simp add: empty_fail_def return_def mres_def vimage_def)
 
 lemma empty_fail_returnOk[empty_fail_term]:
   "empty_fail (returnOk v)"
@@ -191,7 +216,7 @@ lemma empty_fail_assertE[empty_fail_term]:
 
 lemma empty_fail_get[empty_fail_term]:
   "empty_fail get"
-  by (simp add: empty_fail_def get_def)
+  by (simp add: empty_fail_def get_def mres_def vimage_def)
 
 lemma empty_fail_catch[empty_fail_cond]:
   "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)"
@@ -203,7 +228,7 @@ lemma empty_fail_guard[empty_fail_term]:
 
 lemma empty_fail_spec[empty_fail_term]:
   "empty_fail (state_select F)"
-  by (clarsimp simp: state_select_def empty_fail_def)
+  by (clarsimp simp: state_select_def empty_fail_def default_elem_def mres_def image_def)
 
 lemma empty_fail_when[empty_fail_cond]:
   "(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
@@ -321,7 +346,7 @@ subsection \<open>Equations and legacy names\<close>
 
 lemma empty_fail_select_eq[simp]:
   "empty_fail (select V) = (V \<noteq> {})"
-  by (clarsimp simp: select_def empty_fail_def)
+  by (clarsimp simp: select_def empty_fail_def mres_def image_def)
 
 lemma empty_fail_liftM_eq[simp]:
   "empty_fail (liftM f m) = empty_fail m"
@@ -330,7 +355,7 @@ lemma empty_fail_liftM_eq[simp]:
 
 lemma empty_fail_liftE_eq[simp]:
   "empty_fail (liftE f) = empty_fail f"
-  by (fastforce simp: liftE_def empty_fail_def bind_def)
+  by (auto simp: liftE_def empty_fail_bindD1)
 
 lemma liftME_empty_fail_eq[simp]:
   "empty_fail (liftME f m) = empty_fail m"
diff --git a/lib/Monads/trace/Trace_In_Monad.thy b/lib/Monads/trace/Trace_In_Monad.thy
index 24769154c79..0078c66c445 100644
--- a/lib/Monads/trace/Trace_In_Monad.thy
+++ b/lib/Monads/trace/Trace_In_Monad.thy
@@ -55,8 +55,8 @@ lemma inl_whenE:
   by (auto simp add: in_whenE)
 
 lemma inr_in_unlessE_throwError[termination_simp]:
-  "(Inr (), s') \<in> fst (unlessE P (throwError E) s) = (P \<and> s'=s)"
-  by (simp add: unlessE_def returnOk_def throwError_def return_def)
+  "(Inr (), s') \<in> mres (unlessE P (throwError E) s) = (P \<and> s'=s)"
+  by (simp add: unlessE_def returnOk_def throwError_def in_return)
 
 lemma in_fail:
   "r \<in> mres (fail s) = False"
@@ -90,6 +90,18 @@ lemma in_when:
   "(v, s') \<in> mres (when P f s) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not>P \<longrightarrow> v = () \<and> s' = s))"
   by (simp add: when_def in_return)
 
+lemma in_unless:
+  "(v, s') \<in> mres (unless P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))"
+  by (simp add: unless_def in_when)
+
+lemma in_unlessE:
+  "(v, s') \<in> mres (unlessE P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))"
+  by (simp add: unlessE_def in_returnOk)
+
+lemma inl_unlessE:
+  "((Inl x, s') \<in> mres (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> mres (f s))"
+  by (auto simp add: in_unlessE)
+
 lemma in_modify:
   "(v, s') \<in> mres (modify f s) = (s'=f s \<and> v = ())"
   by (auto simp add: modify_def bind_def get_def put_def mres_def)
@@ -118,8 +130,8 @@ lemma in_bindE:
 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:
diff --git a/lib/Monads/trace/Trace_Lemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy
index f6e7706f3cb..557c2a855de 100644
--- a/lib/Monads/trace/Trace_Lemmas.thy
+++ b/lib/Monads/trace/Trace_Lemmas.thy
@@ -31,15 +31,15 @@ lemma bind_apply_cong':
 lemmas bind_apply_cong = bind_apply_cong'[rule_format, fundef_cong]
 
 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)
+  "\<lbrakk> f = f'; \<And>v s s'. (v, s') \<in> mres (f' s) \<Longrightarrow> g v s' = g' v s' \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
+  by (auto intro!: bind_apply_cong)
 
 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'"
+  "\<lbrakk> M = M' ; \<And>v s s'. (Inr v, s') \<in> mres (M' s) \<Longrightarrow> N v s' = N' v s' \<rbrakk> \<Longrightarrow> bindE M N = bindE M' N'"
   by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_cong)
 
 lemma bindE_apply_cong[fundef_cong]:
-  "\<lbrakk> f s = f' s'; \<And>rv st. (Inr rv, st) \<in> fst (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
+  "\<lbrakk> f s = f' s'; \<And>rv st. (Inr rv, st) \<in> mres (f' s') \<Longrightarrow> g rv st = g' rv st \<rbrakk>
   \<Longrightarrow> (f >>=E g) s = (f' >>=E g') s'"
   by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_apply_cong)
 
@@ -63,11 +63,12 @@ lemma unlessE_apply_cong[fundef_cong]:
   "\<lbrakk> C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> unlessE C m s = unlessE C' m' s'"
   by (simp add: unlessE_def)
 
+
 subsection \<open>Simplifying Monads\<close>
 
 lemma nested_bind[simp]:
   "do x <- do y <- f; return (g y) od; h x od = do y <- f; h (g y) od"
-  by (clarsimp simp: bind_def Let_def split_def return_def)
+  by (fastforce simp: bind_def return_def split: tmres.splits)
 
 lemma bind_dummy_ret_val:
   "do y \<leftarrow> a; b od = do a; b od"
diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy
index 37f7a70eab9..7ddffb245c2 100644
--- a/lib/Monads/trace/Trace_Monad.thy
+++ b/lib/Monads/trace/Trace_Monad.thy
@@ -47,21 +47,22 @@ text \<open>
 type_synonym ('s, 'a) tmonad = "'s \<Rightarrow> ((tmid \<times> 's) list \<times> ('s, 'a) tmres) set"
 
 text \<open>
-  Print the type @{typ "('s,'a) nondet_monad"} instead of its unwieldy expansion.
+  Print the type @{typ "('s,'a) tmonad"} instead of its unwieldy expansion.
   Needs an AST translation in code, because it needs to check that the state variable
-  @{typ 's} occurs twice. This comparison is not guaranteed to always work as expected
+  @{typ 's} occurs three times. This comparison is not guaranteed to always work as expected
   (AST instances might have different decoration), but it does seem to work here.\<close>
 print_ast_translation \<open>
   let
-    fun monad_tr _ [t1, Ast.Appl [Ast.Constant @{type_syntax prod},
-                          Ast.Appl [Ast.Constant @{type_syntax set},
-                            Ast.Appl [Ast.Constant @{type_syntax prod}, t2, t3]],
-                          Ast.Constant @{type_syntax bool}]] =
-      if t3 = t1
-      then Ast.Appl [Ast.Constant @{type_syntax "nondet_monad"}, t1, t2]
+    fun tmonad_tr _ [t1, Ast.Appl [Ast.Constant @{type_syntax set},
+                          Ast.Appl [Ast.Constant @{type_syntax prod},
+                            Ast.Appl [Ast.Constant @{type_syntax list},
+                              Ast.Appl [Ast.Constant @{type_syntax prod},
+                                Ast.Constant @{type_syntax tmid}, t2]],
+                            Ast.Appl [Ast.Constant @{type_syntax tmres}, t3, t4]]]] =
+      if t1 = t2 andalso t1 = t3
+      then Ast.Appl [Ast.Constant @{type_syntax "tmonad"}, t1, t4]
       else raise Match
-  in [(@{type_syntax "fun"}, monad_tr)] end
-\<close>
+  in [(@{type_syntax "fun"}, tmonad_tr)] end\<close>
 
 text \<open>Returns monad results, ignoring failures and traces.\<close>
 definition mres :: "((tmid \<times> 's) list \<times> ('s, 'a) tmres) set \<Rightarrow> ('a \<times> 's) set" where
@@ -141,11 +142,16 @@ text \<open>
   FIXME: The @{text select_f} function was left out here until we figure
   out what variant we actually need.\<close>
 
-text \<open>@{text select_state} takes a relationship between
-  states, and outputs nondeterministically a state
-  related to the input state.\<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))"
+definition
+  "default_elem dflt A \<equiv> if A = {} then {dflt} else A"
+
+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) tmonad" where
+  "state_select r \<equiv>
+     \<lambda>s. (Pair [] ` default_elem Failed (Result ` (\<lambda>x. ((), x)) ` {s'. (s, s') \<in> r}))"
 
 subsection "Failure"
 
@@ -212,7 +218,7 @@ 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>
 definition
-  gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) nondet_monad" where
+  gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) tmonad" where
   "gets_map f p \<equiv> gets f >>= (\<lambda>m. assert_opt (m p))"
 
 
@@ -520,8 +526,8 @@ text \<open>The same for the exception monad:\<close>
 definition liftME :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'e+'a) tmonad \<Rightarrow> ('s,'e+'b) tmonad" where
   "liftME f m \<equiv> doE x \<leftarrow> m; returnOk (f x) odE"
 
-text \<open> Execute @{term f} for @{term "Some x"}, otherwise do nothing. \<close>
-definition maybeM :: "('a \<Rightarrow> ('s, unit) nondet_monad) \<Rightarrow> 'a option \<Rightarrow> ('s, unit) nondet_monad" where
+text \<open>Execute @{term f} for @{term "Some x"}, otherwise do nothing.\<close>
+definition maybeM :: "('a \<Rightarrow> ('s, unit) tmonad) \<Rightarrow> 'a option \<Rightarrow> ('s, unit) tmonad" where
   "maybeM f y \<equiv> case y of Some x \<Rightarrow> f x | None \<Rightarrow> return ()"
 
 text \<open>Run a sequence of monads from left to right, ignoring return values.\<close>
@@ -589,10 +595,8 @@ primrec filterM :: "('a \<Rightarrow> ('s, bool) tmonad) \<Rightarrow> 'a list \
      return (if b then (x # ys) else ys)
    od"
 
-text \<open>
-  @{text select_state} takes a relationship between states, and outputs
-  nondeterministically a state related to the input state.\<close>
-definition state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) tmonad" where
+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};
@@ -600,6 +604,11 @@ definition state_select :: "('s \<times> 's) set \<Rightarrow> ('s, unit) tmonad
     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 default_elem_def
+                    intro!: eq_reflection)
+  apply fastforce
+  done
 
 
 section "Catching and Handling Exceptions"
@@ -715,45 +724,46 @@ notation (output)
 
 section "Combinators that have conditions with side effects"
 
-definition notM :: "('s, bool) nondet_monad \<Rightarrow> ('s, bool) nondet_monad" where
+definition notM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" 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) 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) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow> ('s, 'a) nondet_monad \<Rightarrow>
-          ('s, 'a) nondet_monad" where
+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;
     if c then t else f
    od"
 
 definition ifME ::
-  "('a, 'b + bool) nondet_monad \<Rightarrow> ('a, 'b + 'c) nondet_monad \<Rightarrow> ('a, 'b + 'c) nondet_monad
-   \<Rightarrow> ('a, 'b + 'c) nondet_monad" where
+  "('a, 'b + bool) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad \<Rightarrow> ('a, 'b + 'c) tmonad
+   \<Rightarrow> ('a, 'b + 'c) tmonad" where
   "ifME test t f = doE
     c \<leftarrow> test;
     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) tmonad \<Rightarrow> ('s, unit) tmonad \<Rightarrow> ('s, unit) tmonad" 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) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" 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
+  andM :: "('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad \<Rightarrow> ('s, bool) tmonad" where
   "andM a b = ifM a b (return False)"
 
+
 subsection "Await command"
 
 text \<open>@{term "Await c f"} blocks the execution until @{term "c"} is true,
diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy
index 265b8c73c88..2e0815222df 100644
--- a/lib/Monads/trace/Trace_Monad_Equations.thy
+++ b/lib/Monads/trace/Trace_Monad_Equations.thy
@@ -29,11 +29,7 @@ lemma exec_modify:
 
 lemma bind_return_eq:
   "(a >>= return) = (b >>= return) \<Longrightarrow> a = b"
-  apply (clarsimp simp:bind_def)
-  apply (rule ext)
-  apply (drule_tac x= x in fun_cong)
-  apply (auto simp:return_def split_def)
-  done
+  by clarsimp
 
 lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl]
 
@@ -51,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:
@@ -71,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)
 
@@ -93,13 +89,13 @@ 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:
   "whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)"
   unfolding whenE_def bindE_def
-  by (auto simp: Nondet_Monad.lift_def throwError_def returnOk_def)
+  by (auto simp: lift_def throwError_def returnOk_def)
 
 lemma alternative_liftE_returnOk:
   "(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)"
@@ -129,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
@@ -145,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)
@@ -171,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)+
 
@@ -187,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:
@@ -216,7 +212,7 @@ lemma maybe_fail_bind_fail:
 
 lemma select_singleton[simp]:
   "select {x} = return x"
-  by (fastforce simp add: fun_eq_iff select_def return_def)
+  by (simp add: select_def return_def)
 
 lemma return_modify:
   "return () = modify id"
@@ -234,10 +230,9 @@ 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:
@@ -245,12 +240,12 @@ lemma bind_eqI:
 
 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:
@@ -265,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:
@@ -274,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)
 
@@ -332,7 +327,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: Nondet_Monad.lift_def throwError_def split: sum.splits)
+  apply (clarsimp simp: 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"
@@ -354,36 +349,24 @@ lemma if_to_top_of_bindE:
   "(bindE (If P x y) z) = If P (bindE x z) (bindE y z)"
   by (simp split: if_split)
 
-lemma modify_id:
-  "modify id = return ()"
-  by (simp add: modify_def get_def bind_def put_def return_def)
-
 lemma modify_modify:
   "(do x \<leftarrow> modify f; modify (g x) od) = modify (g () o f)"
   by (simp add: bind_def simpler_modify_def)
 
-lemmas modify_modify_bind = arg_cong2[where f=bind,
-  OF modify_modify refl, simplified bind_assoc]
-
-lemma select_single:
-  "select {x} = return x"
-  by (simp add: select_def return_def)
+lemmas modify_modify_bind =
+  arg_cong2[where f=bind, OF modify_modify refl, simplified bind_assoc]
 
 lemma put_then_get[unfolded K_bind_def]:
   "do put s; get od = do put s; return s od"
   by (simp add: put_def bind_def get_def return_def)
 
-lemmas put_then_get_then
-    = put_then_get[THEN bind_then_eq, simplified bind_assoc return_bind]
+lemmas put_then_get_then =
+    put_then_get[THEN bind_then_eq, simplified bind_assoc return_bind]
 
 lemma select_empty_bind[simp]:
   "select {} >>= f = select {}"
   by (simp add: select_def bind_def)
 
-lemma fail_bind[simp]:
-  "fail >>= f = fail"
-  by (simp add: bind_def fail_def)
-
 
 subsection \<open>Alternative env_steps with repeat\<close>
 
diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy
index 27b5d9d34df..80f4ab5f7a7 100644
--- a/lib/Monads/trace/Trace_More_VCG.thy
+++ b/lib/Monads/trace/Trace_More_VCG.thy
@@ -11,11 +11,12 @@
 theory Trace_More_VCG
   imports
     Trace_VCG
+    Trace_In_Monad
 begin
 
 lemma hoare_take_disjunct:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace>
-    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>"
   by (erule hoare_strengthen_post, simp)
 
 lemma hoare_post_add:
@@ -44,10 +45,6 @@ lemma hoare_name_pre_stateE:
   "\<lbrakk>\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>"
   by (clarsimp simp: validE_def2)
 
-lemma valid_prove_more: (* FIXME: duplicate *)
-  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
-  by (rule hoare_post_add)
-
 lemma hoare_vcg_if_lift:
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P \<longrightarrow> X rv s) \<and> (\<not>P \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
    \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P then X rv s else Y rv s\<rbrace>"
@@ -97,12 +94,12 @@ lemmas hoare_lift_Pf_pre_conj' = hoare_lift_Pf2_pre_conj[where Q=P and P=P for P
 
 lemma hoare_if_r_and:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace>
-  = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>"
+   = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_convert_imp:
-  "\<lbrakk> \<lbrace>\<lambda>s. \<not> P s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk> \<Longrightarrow>
-    \<lbrace>\<lambda>s. P s \<longrightarrow> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> S rv s\<rbrace>"
+  "\<lbrakk> \<lbrace>\<lambda>s. \<not> P s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<longrightarrow> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> S rv s\<rbrace>"
   apply (simp only: imp_conv_disj)
   apply (erule(1) hoare_vcg_disj_lift)
   done
@@ -115,8 +112,8 @@ lemma hoare_vcg_ex_lift_R:
   done
 
 lemma hoare_case_option_wpR:
-  "\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk> \<Longrightarrow>
-  \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-"
+  "\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk>
+   \<Longrightarrow> \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-"
   by (cases v) auto
 
 lemma hoare_vcg_conj_liftE_R:
@@ -129,12 +126,6 @@ lemma K_valid[wp]:
   "\<lbrace>K P\<rbrace> f \<lbrace>\<lambda>_. K P\<rbrace>"
   by (simp add: valid_def)
 
-lemma hoare_vcg_exI:
-  "\<lbrace>P\<rbrace> f \<lbrace>Q x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
-  apply (simp add: valid_def split_def)
-  apply blast
-  done
-
 lemma hoare_exI_tuple:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>(rv,rv') s. Q x rv rv' s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>(rv,rv') s. \<exists>x. Q x rv rv' s\<rbrace>"
   by (fastforce simp: valid_def)
@@ -182,7 +173,7 @@ lemma gets_inv [simp]:
 
 lemma select_inv:
   "\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>"
-  by (simp add: select_def valid_def)
+  by wpsimp
 
 lemmas return_inv = hoare_return_drop_var
 
@@ -223,9 +214,10 @@ lemma list_cases_weak_wp:
   assumes "\<And>x xs. \<lbrace>P_B\<rbrace> b x xs \<lbrace>Q\<rbrace>"
   shows
   "\<lbrace>P_A and P_B\<rbrace>
-    case ts of
-      [] \<Rightarrow> a
-    | x#xs \<Rightarrow> b x xs \<lbrace>Q\<rbrace>"
+   case ts of
+       [] \<Rightarrow> a
+     | x#xs \<Rightarrow> b x xs
+   \<lbrace>Q\<rbrace>"
   apply (cases ts)
   apply (simp, rule hoare_weaken_pre, rule assms, simp)+
   done
@@ -234,18 +226,18 @@ lemmas hoare_FalseE_R = hoare_FalseE[where E="\<top>\<top>", folded validE_R_def
 
 lemma hoare_vcg_if_lift2:
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>"
 
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>"
   by (auto simp: valid_def split_def)
 
 lemma hoare_vcg_if_lift_ER: (* Required because of lack of rv in lifting rules *)
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then X rv s else Y rv s\<rbrace>, -"
 
   "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P' rv \<longrightarrow> X rv s) \<and> (\<not> P' rv \<longrightarrow> Y rv s)\<rbrace>, - \<Longrightarrow>
-  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
+   \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv. if P' rv then X rv else Y rv\<rbrace>, -"
   by (auto simp: valid_def validE_R_def validE_def split_def)
 
 lemma hoare_vcg_imp_liftE:
@@ -303,7 +295,7 @@ lemma set_shrink_proof:
   assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
   shows
   "\<lbrace>\<lambda>s. \<forall>S'. S' \<subseteq> S s \<longrightarrow> P S'\<rbrace>
-     f
+   f
    \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
   apply (clarsimp simp: valid_def)
   apply (drule spec, erule mp)
@@ -331,7 +323,7 @@ lemma shrinks_proof:
   by (metis use_valid w z)
 
 lemma use_validE_R:
-  "\<lbrakk> (Inr r, s') \<in> fst (f s); \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; P s \<rbrakk> \<Longrightarrow> Q r s'"
+  "\<lbrakk> (Inr r, s') \<in> mres (f s); \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; P s \<rbrakk> \<Longrightarrow> Q r s'"
   unfolding validE_R_def validE_def
   by (frule(2) use_valid, simp)
 
@@ -345,8 +337,6 @@ lemma valid_preservation_ex:
   apply simp
   done
 
-lemmas valid_prove_more' = valid_prove_more[where Q="\<lambda>rv. Q" for Q]
-
 lemma whenE_inv:
   assumes a: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
   shows "\<lbrace>P\<rbrace> whenE Q f \<lbrace>\<lambda>_. P\<rbrace>"
@@ -358,9 +348,12 @@ lemma whenE_throwError_wp:
 
 lemma ifM_throwError_returnOk:
   "\<lbrace>Q\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> P s\<rbrace> \<Longrightarrow> \<lbrace>Q\<rbrace> ifM test (throwError e) (returnOk ()) \<lbrace>\<lambda>_. P\<rbrace>, -"
-  by (fastforce simp: ifM_def returnOk_def throwError_def return_def validE_R_def valid_def
-                      validE_def bind_def
-               split: if_splits)
+  unfolding ifM_def
+  apply (fold liftE_bindE)
+  apply wpsimp
+   apply assumption
+  apply simp
+  done
 
 lemma ifME_liftE:
   "ifME (liftE test) a b = ifM test a b"
@@ -368,14 +361,10 @@ lemma ifME_liftE:
 
 lemma gets_the_inv: "\<lbrace>P\<rbrace> gets_the V \<lbrace>\<lambda>rv. P\<rbrace>" by wpsimp
 
-lemma select_f_inv:
-  "\<lbrace>P\<rbrace> select_f S \<lbrace>\<lambda>_. P\<rbrace>"
-  by (simp add: select_f_def valid_def)
-
 lemmas state_unchanged = in_inv_by_hoareD [THEN sym]
 
 lemma validI:
-  assumes rl: "\<And>s r s'. \<lbrakk> P s; (r, s') \<in> fst (S s) \<rbrakk> \<Longrightarrow> Q r s'"
+  assumes rl: "\<And>s r s'. \<lbrakk> P s; (r, s') \<in> mres (S s) \<rbrakk> \<Longrightarrow> Q r s'"
   shows "\<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>"
   unfolding valid_def using rl by safe
 
@@ -386,23 +375,13 @@ lemma opt_return_pres_lift:
 
 lemma valid_return_unit:
   "\<lbrace>P\<rbrace> f >>= (\<lambda>_. return ()) \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>"
-  apply (rule validI)
-  apply (fastforce simp: valid_def return_def bind_def split_def)
-  done
-
-lemma static_imp_wp:
-  "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>"
-  by (cases P, simp_all add: valid_def)
-
-lemma static_imp_wpE :
-  "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
-  by (cases P, simp_all)
+  by (auto simp: valid_def in_bind in_return Ball_def)
 
-lemma static_imp_conj_wp:
+lemma hoare_weak_lift_imp_conj:
   "\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk>
-    \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>"
+   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>"
   apply (rule hoare_vcg_conj_lift)
-   apply (rule static_imp_wp)
+   apply (rule hoare_weak_lift_imp)
    apply assumption+
   done
 
@@ -415,10 +394,6 @@ lemma hoare_validE_R_conj:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, -"
   by (simp add: valid_def validE_def validE_R_def Let_def split_def split: sum.splits)
 
-lemma hoare_vcg_const_imp_lift_R:
-  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. F \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. F \<longrightarrow> Q rv s\<rbrace>,-"
-  by (cases F, simp_all)
-
 lemma hoare_vcg_disj_lift_R:
   assumes x: "\<lbrace>P\<rbrace>  f \<lbrace>Q\<rbrace>,-"
   assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
@@ -429,9 +404,10 @@ lemma hoare_vcg_disj_lift_R:
 lemmas throwError_validE_R = throwError_wp [where E="\<top>\<top>", folded validE_R_def]
 
 lemma valid_case_option_post_wp:
-  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>rv. Q x\<rbrace>) \<Longrightarrow>
-    \<lbrace>\<lambda>s. case ep of Some x \<Rightarrow> P x s | _ \<Rightarrow> True\<rbrace>
-       f \<lbrace>\<lambda>rv s. case ep of Some x \<Rightarrow> Q x s | _ \<Rightarrow> True\<rbrace>"
+  "\<lbrakk>\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>\<lambda>rv. Q x\<rbrace>\<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. case ep of Some x \<Rightarrow> P x s | _ \<Rightarrow> True\<rbrace>
+   f
+   \<lbrace>\<lambda>rv s. case ep of Some x \<Rightarrow> Q x s | _ \<Rightarrow> True\<rbrace>"
   by (cases ep, simp_all add: hoare_vcg_prop)
 
 lemma P_bool_lift:
@@ -454,7 +430,7 @@ lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda
   by (wp, simp)
 
 lemma post_by_hoare2:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; (r, s') \<in> fst (f s); P s \<rbrakk> \<Longrightarrow> Q r s'"
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; (r, s') \<in> mres (f s); P s \<rbrakk> \<Longrightarrow> Q r s'"
   by (rule post_by_hoare, assumption+)
 
 lemma hoare_Ball_helper:
@@ -511,19 +487,19 @@ lemma hoare_ex_pre: (* safe, unlike hoare_vcg_ex_lift *)
   by (fastforce simp: valid_def)
 
 lemma hoare_ex_pre_conj:
-  "(\<And>x. \<lbrace>\<lambda>s. P x s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>)
-  \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
+  "\<lbrakk>\<And>x. \<lbrace>\<lambda>s. P x s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. (\<exists>x. P x s) \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_conj_lift_inv:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. P' s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv. I\<rbrace>;
-   \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
+    \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
    \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I s\<rbrace>"
    by (fastforce simp: valid_def)
 
-lemma hoare_in_monad_post :
+lemma hoare_in_monad_post:
   assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
-  shows      "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> fst (f s)\<rbrace>"
+  shows      "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> mres (f s)\<rbrace>"
   apply (clarsimp simp: valid_def)
   apply (subgoal_tac "s = b", simp)
   apply (simp add: state_unchanged [OF x])
@@ -544,7 +520,7 @@ lemma validE_R_sp:
 
 lemma valid_set_take_helper:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace>
-    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>"
   apply (erule hoare_strengthen_post)
   apply (clarsimp dest!: in_set_takeD)
   done
@@ -576,29 +552,13 @@ lemma wp_split_const_if_R:
   shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-"
   by (case_tac G, simp_all add: x y)
 
-lemma wp_throw_const_imp:
-  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
-  shows      "\<lbrace>\<lambda>s. G \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. G \<longrightarrow> Q rv s\<rbrace>"
-  by (case_tac G, simp_all add: x hoare_vcg_prop)
-
-lemma wp_throw_const_impE:
-  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
-  shows      "\<lbrace>\<lambda>s. G \<longrightarrow> P s\<rbrace> f \<lbrace>\<lambda>rv s. G \<longrightarrow> Q rv s\<rbrace>,\<lbrace>\<lambda>rv s. G \<longrightarrow> E rv s\<rbrace>"
-  apply (case_tac G, simp_all add: x)
-  apply wp
-  done
-
-lemma hoare_const_imp_R:
-  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
-  by (cases P, simp_all)
-
 lemma hoare_vcg_imp_lift_R:
   "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -"
   by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)
 
 lemma hoare_disj_division:
   "\<lbrakk> P \<or> Q; P \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>; Q \<Longrightarrow> \<lbrace>T\<rbrace> f \<lbrace>S\<rbrace> \<rbrakk>
-     \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"
+   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)\<rbrace> f \<lbrace>S\<rbrace>"
   apply safe
    apply (rule hoare_pre_imp)
     prefer 2
@@ -615,8 +575,8 @@ lemma hoare_grab_asm:
   by (cases G, simp+)
 
 lemma hoare_grab_asm2:
-  "(P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>)
-  \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>"
+  "\<lbrakk>P' \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> P' \<and> R s\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_grab_exs:
@@ -631,8 +591,8 @@ lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s
   by (rule hoare_pre, wp, simp)
 
 lemma hoare_vcg_conj_lift_R:
-  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>,- \<rbrakk> \<Longrightarrow>
-     \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> S rv s\<rbrace>,-"
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>,- \<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> R s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> S rv s\<rbrace>,-"
   apply (simp add: validE_R_def validE_def)
   apply (drule(1) hoare_vcg_conj_lift)
   apply (erule hoare_strengthen_post)
@@ -649,12 +609,12 @@ lemma hoare_walk_assmsE:
   done
 
 lemma univ_wp:
-  "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
+  "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> mres (f s). Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
   by (simp add: valid_def)
 
 lemma univ_get_wp:
   assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>"
-  shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
+  shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> mres (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
   apply (rule hoare_pre_imp [OF _ univ_wp])
   apply clarsimp
   apply (drule bspec, assumption, simp)
@@ -662,16 +622,11 @@ lemma univ_get_wp:
   apply (simp add: state_unchanged [OF x])
   done
 
-lemma result_in_set_wp :
+lemma other_hoare_in_monad_post:
   assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>"
-  shows      "\<lbrace>\<lambda>s. True\<rbrace> fn \<lbrace>\<lambda>v s'. (v, s') \<in> fst (fn s')\<rbrace>"
-  by (rule hoare_pre_imp [OF _ univ_get_wp], simp_all add: x split_def) clarsimp
-
-lemma other_result_in_set_wp:
-  assumes x: "\<And>P. \<lbrace>P\<rbrace> fn \<lbrace>\<lambda>rv. P\<rbrace>"
-  shows "\<lbrace>\<lambda>s. \<forall>(v, s) \<in> fst (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> fst (fn s')\<rbrace>"
+  shows "\<lbrace>\<lambda>s. \<forall>(v, s) \<in> mres (fn s). F v = v\<rbrace> fn \<lbrace>\<lambda>v s'. (F v, s') \<in> mres (fn s')\<rbrace>"
   proof -
-  have P: "\<And>v s. (F v = v) \<and> (v, s) \<in> fst (fn s) \<Longrightarrow> (F v, s) \<in> fst (fn s)"
+  have P: "\<And>v s. (F v = v) \<and> (v, s) \<in> mres (fn s) \<Longrightarrow> (F v, s) \<in> mres (fn s)"
     by simp
   show ?thesis
   apply (rule hoare_post_imp [OF P], assumption)
@@ -679,7 +634,7 @@ lemma other_result_in_set_wp:
   defer
    apply (rule hoare_vcg_conj_lift)
     apply (rule univ_get_wp [OF x])
-   apply (rule result_in_set_wp [OF x])
+   apply (rule hoare_in_monad_post [OF x])
   apply clarsimp
   apply (drule bspec, assumption, simp)
   done
@@ -687,7 +642,7 @@ lemma other_result_in_set_wp:
 
 lemma weak_if_wp:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
-  \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
+   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>"
   by (auto simp add: valid_def split_def)
 
 lemma weak_if_wp':
@@ -696,12 +651,12 @@ lemma weak_if_wp':
   by (auto simp add: valid_def split_def)
 
 lemma bindE_split_recursive_asm:
-  assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> fst (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. B x s \<and> s = s'\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
+  assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> mres (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. B x s \<and> s = s'\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
   shows      "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
-  apply (clarsimp simp: validE_def valid_def bindE_def bind_def lift_def)
+  apply (clarsimp simp: validE_def valid_def bindE_def in_bind lift_def)
   apply (erule allE, erule(1) impE)
   apply (drule(1) bspec, simp)
-  apply (case_tac a, simp_all add: throwError_def return_def)
+  apply (case_tac x, simp_all add: in_throwError)
   apply (drule x)
   apply (clarsimp simp: validE_def valid_def)
   apply (drule(1) bspec, simp)
@@ -713,7 +668,7 @@ lemma validE_R_abstract_rv:
 
 lemma validE_cases_valid:
   "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace>
-      \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   apply (simp add: validE_def)
   apply (erule hoare_strengthen_post)
   apply (simp split: sum.split_asm)
@@ -738,12 +693,10 @@ lemma hoare_gen_asm_conj:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp: valid_def)
 
-
 lemma hoare_add_K:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I\<rbrace>"
   by (fastforce simp: valid_def)
 
-
 lemma valid_rv_lift:
   "\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>"
   by (fastforce simp: valid_def)
@@ -754,20 +707,19 @@ lemma valid_imp_ex:
 
 lemma valid_rv_split:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> Q' s\<rbrace>\<rbrakk>
-  \<Longrightarrow>
-  \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>"
   by (fastforce simp: valid_def)
 
 lemma hoare_rv_split:
   "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk>
-  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
   apply (clarsimp simp: valid_def)
   apply (case_tac a, fastforce+)
   done
 
-lemma combine_validE: "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>;
-         \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk> \<Longrightarrow>
-         \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>"
+lemma combine_validE:
+  "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk>
+   \<Longrightarrow> \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>"
   apply (clarsimp simp: validE_def valid_def split: sum.splits)
   apply (erule allE, erule (1) impE)+
   apply (drule (1) bspec)+
@@ -819,9 +771,9 @@ lemma hoare_name_pre_state2:
   by (auto simp: valid_def intro: hoare_name_pre_state)
 
 lemma returnOk_E': "\<lbrace>P\<rbrace> returnOk r -,\<lbrace>E\<rbrace>"
-  by (clarsimp simp: returnOk_def validE_E_def validE_def valid_def return_def)
+  by wpsimp
 
 lemma throwError_R': "\<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>,-"
-  by (clarsimp simp:throwError_def validE_R_def validE_def valid_def return_def)
+  by wpsimp
 
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_No_Fail.thy b/lib/Monads/trace/Trace_No_Fail.thy
index 4265dd0793d..3630aa911a7 100644
--- a/lib/Monads/trace/Trace_No_Fail.thy
+++ b/lib/Monads/trace/Trace_No_Fail.thy
@@ -144,13 +144,14 @@ lemma no_fail_assume_pre:
   "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f"
   by (simp add: no_fail_def)
 
-lemma no_fail_liftM_eq[simp]:
+\<comment> \<open>lemma no_fail_liftM_eq[simp]:
   "no_fail P (liftM f m) = no_fail P m"
-  by (auto simp: liftM_def no_fail_def bind_def return_def)
+  by (auto simp: liftM_def no_fail_def bind_def return_def)\<close>
 
 lemma no_fail_liftM[wp]:
   "no_fail P m \<Longrightarrow> no_fail P (liftM f m)"
-  by simp
+  unfolding liftM_def
+  by wpsimp
 
 lemma no_fail_pre_and:
   "no_fail P f \<Longrightarrow> no_fail (P and Q) f"
diff --git a/lib/Monads/trace/Trace_No_Throw.thy b/lib/Monads/trace/Trace_No_Throw.thy
index 90d667b718d..f5174f1ecd7 100644
--- a/lib/Monads/trace/Trace_No_Throw.thy
+++ b/lib/Monads/trace/Trace_No_Throw.thy
@@ -27,10 +27,12 @@ definition no_return :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b + 'c) tmo
 
 (* Alternative definition of no_throw; easier to work with than unfolding validE. *)
 lemma no_throw_def':
-  "no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> fst (A s). (\<exists>x. r = Inr x)))"
+  "no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> mres (A s). (\<exists>x. r = Inr x)))"
   by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)
 
 
+subsection \<open>no_throw rules\<close>
+
 lemma no_throw_returnOk[simp]:
   "no_throw P (returnOk a)"
   unfolding no_throw_def
@@ -53,12 +55,14 @@ lemma no_throw_bindE_simple:
 lemma no_throw_handleE_simple:
   "\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)"
   by (fastforce simp: no_throw_def' handleE_def handleE'_def validE_def valid_def bind_def return_def
-                split: sum.splits)
+                      mres_def image_def
+                split: sum.splits tmres.splits)
 
 lemma no_throw_handle2:
   "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)"
-  by (fastforce simp: no_throw_def' handleE'_def validE_def valid_def bind_def return_def
-                split: sum.splits)
+  by (fastforce simp: no_throw_def' handleE'_def validE_def valid_def bind_def return_def mres_def
+                      image_def
+                split: sum.splits tmres.splits)
 
 lemma no_throw_handle:
   "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle> B)"
@@ -92,7 +96,7 @@ lemma condition_nothrow:
   by (clarsimp simp: condition_def no_throw_def validE_def2)
 
 lemma no_throw_Inr:
-  "\<lbrakk> x \<in> fst (A s); no_throw P A; P s \<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y"
+  "\<lbrakk> x \<in> mres (A s); no_throw P A; P s \<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y"
   by (fastforce simp: no_throw_def' split: sum.splits)
 
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index fb844d0f181..f4d3164cca6 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -69,7 +69,7 @@ abbreviation(input)
   "\<bottom>\<bottom>\<bottom> \<equiv> \<lambda>_ _ _. False"
 
 text \<open>
-  Test whether the enironment steps in @{text tr} satisfy the rely condition @{text R},
+  Test whether the environment steps in @{text tr} satisfy the rely condition @{text R},
   assuming that @{text s0s} was the initial state before the first step in the trace.\<close>
 definition rely_cond :: "'s rg_pred \<Rightarrow> 's \<Rightarrow> (tmid \<times> 's) list \<Rightarrow> bool" where
   "rely_cond R s0s tr = (\<forall>(ident, s0, s) \<in> trace_steps (rev tr) s0s. ident = Env \<longrightarrow> R s0 s)"
diff --git a/lib/Monads/trace/Trace_Sat.thy b/lib/Monads/trace/Trace_Sat.thy
index 20d68e584df..213303f21a2 100644
--- a/lib/Monads/trace/Trace_Sat.thy
+++ b/lib/Monads/trace/Trace_Sat.thy
@@ -29,7 +29,7 @@ definition ex_exs_validE ::
 text \<open>
   Seen as predicate transformer, @{const exs_valid} is the so-called conjugate wp in the literature,
   i.e. with
-  @{term "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"} and
+  @{term "wp f Q \<equiv> \<lambda>s. mres (f s) \<subseteq> {(rv,s). Q rv s}"} and
   @{term "cwp f Q \<equiv> not (wp f (not Q))"}, we get
   @{prop "valid P f Q = (\<forall>s. P s \<longrightarrow> wp f Q s)"} and
   @{prop "exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"}.
@@ -39,7 +39,7 @@ experiment
 begin
 
 definition
-  "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"
+  "wp f Q \<equiv> \<lambda>s. mres (f s) \<subseteq> {(rv,s). Q rv s}"
 
 definition
   "cwp f Q \<equiv> not (wp f (not Q))"
@@ -100,11 +100,11 @@ lemma exs_valid_return[wp]:
 
 lemma exs_valid_select[wp]:
   "\<lbrace>\<lambda>s. \<exists>r \<in> S. Q r s\<rbrace> select S \<exists>\<lbrace>Q\<rbrace>"
-  by (clarsimp simp: exs_valid_def select_def)
+  by (auto simp: exs_valid_def select_def mres_def image_def)
 
 lemma exs_valid_alt[wp]:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> g \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P or P'\<rbrace> f \<sqinter> g \<exists>\<lbrace>Q\<rbrace>"
-  by (fastforce simp: exs_valid_def alternative_def)
+  by (fastforce simp: exs_valid_def alternative_def mres_def image_def)
 
 lemma exs_valid_get[wp]:
   "\<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace> Q \<rbrace>"
@@ -129,7 +129,7 @@ lemma exs_valid_assert[wp]:
   by (wpsimp | rule conjI)+
 
 lemma exs_valid_state_assert[wp]:
-    "\<lbrace> \<lambda>s. Q () s \<and> G s \<rbrace> state_assert G \<exists>\<lbrace> Q \<rbrace>"
+  "\<lbrace>\<lambda>s. Q () s \<and> G s\<rbrace> state_assert G \<exists>\<lbrace>Q\<rbrace>"
   unfolding state_assert_def
   by wp
 
@@ -145,7 +145,7 @@ lemma gets_exs_valid:
 
 lemma exs_valid_assert_opt[wp]:
   "\<lbrace>\<lambda>s. \<exists>x. G = Some x \<and> Q x s\<rbrace> assert_opt G \<exists>\<lbrace>Q\<rbrace>"
-  by (clarsimp simp: assert_opt_def exs_valid_def get_def assert_def bind_def' return_def)
+  by (clarsimp simp: assert_opt_def exs_valid_def return_def mres_def)
 
 lemma gets_the_exs_valid[wp]:
   "\<lbrace>\<lambda>s. \<exists>x. h s = Some x \<and> Q x s\<rbrace> gets_the h \<exists>\<lbrace>Q\<rbrace>"
diff --git a/lib/Monads/trace/Trace_Strengthen_Setup.thy b/lib/Monads/trace/Trace_Strengthen_Setup.thy
index c4b652fa001..4980330968f 100644
--- a/lib/Monads/trace/Trace_Strengthen_Setup.thy
+++ b/lib/Monads/trace/Trace_Strengthen_Setup.thy
@@ -42,33 +42,29 @@ lemma strengthen_validI[strg]:
   by (cases F, auto elim: validI_strengthen_post)
 
 lemma wpfix_strengthen_hoare:
-  "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
-    \<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s))
-    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>)"
+  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>
+   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>)"
   by (cases F, auto elim: hoare_chain)
 
 lemma wpfix_strengthen_validE_R_cong:
-  "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
-    \<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s))
-    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -)"
+  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (Q' r s)\<rbrakk>
+   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -) (\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, -)"
   by (cases F, auto elim: hoare_chainE simp: validE_R_def)
 
 lemma wpfix_strengthen_validE_cong:
-  "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
-    \<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (Q r s) (R r s))
-    \<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s))
-    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)"
+  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (Q r s) (R r s);
+    \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
+   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>T\<rbrace>)"
   by (cases F, auto elim: hoare_chainE)
 
 lemma wpfix_strengthen_validE_E_cong:
-  "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
-    \<Longrightarrow> (\<And>r s. st F (\<longrightarrow>) (S r s) (T r s))
-    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>)"
+  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s); \<And>r s. st F (\<longrightarrow>) (S r s) (T r s)\<rbrakk>
+   \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace> f -, \<lbrace>S\<rbrace>) (\<lbrace>P'\<rbrace> f -, \<lbrace>T\<rbrace>)"
   by (cases F, auto elim: hoare_chainE simp: validE_E_def)
 
 lemma wpfix_no_fail_cong:
-  "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s))
-    \<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)"
+  "\<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (P' s)\<rbrakk>
+   \<Longrightarrow> st F (\<longrightarrow>) (no_fail P f) (no_fail P' f)"
   by (cases F, auto elim: no_fail_pre)
 
 lemmas nondet_wpfix_strgs =
diff --git a/lib/Monads/trace/Trace_Total.thy b/lib/Monads/trace/Trace_Total.thy
index 7c89f267f21..1c08d8460c0 100644
--- a/lib/Monads/trace/Trace_Total.thy
+++ b/lib/Monads/trace/Trace_Total.thy
@@ -52,13 +52,15 @@ subsection \<open>Basic @{const validNF} theorems\<close>
 lemma validNF_make_schematic_post:
   "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>!) \<Longrightarrow>
    \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>!"
-  by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)
+  by (fastforce simp: valid_def validNF_def no_fail_def mres_def image_def
+               split: prod.splits)
 
 lemma validE_NF_make_schematic_post:
   "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>!) \<Longrightarrow>
    \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
         \<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>!"
-  by (auto simp add: validE_NF_def validE_def valid_def no_fail_def split: prod.splits sum.splits)
+  by (fastforce simp: validE_NF_def validE_def valid_def no_fail_def mres_def image_def
+               split: prod.splits sum.splits)
 
 lemma validNF_conjD1:
   "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv s. Q rv s \<and> Q' rv s \<rbrace>! \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
@@ -84,7 +86,7 @@ lemma validNF_no_fail:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
   by (erule validNFE)
 
-lemma snd_validNF:
+lemma validNF_not_failed:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Failed \<notin> snd ` (f s)"
   by (clarsimp simp: validNF_def no_fail_def)
 
@@ -344,6 +346,6 @@ lemma validE_NF_condition[wp]:
 
 lemma hoare_assume_preNF:
   "(\<And>s. P s \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>!"
-  by (metis validNF_alt_def)
+  by (simp add: validNF_alt_def)
 
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
index f950d1b6e24..dd0a2f57a89 100644
--- a/lib/Monads/trace/Trace_VCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -139,17 +139,6 @@ wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>,-" wpc_helper_v
 wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m -,\<lbrace>E\<rbrace>" wpc_helper_validR_R
 
 
-subsection "Simplification Rules for Lifted And/Or"
-
-lemma bipred_disj_op_eq[simp]:
-  "reflp R \<Longrightarrow> ((=) or R) = R"
-  apply (rule ext, rule ext)
-  apply (auto simp: reflp_def)
-  done
-
-lemma bipred_le_true[simp]: "R \<le> \<top>\<top>"
-  by clarsimp
-
 subsection "Hoare Logic Rules"
 
 lemma bind_wp[wp_split]:
@@ -180,7 +169,7 @@ lemma seq_ext':
 
 lemma seq_ext:
   "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>"
-  by (fastforce simp: valid_def bind_def)
+  by (rule bind_wp)
 
 lemma seqE':
   "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
@@ -320,7 +309,7 @@ lemma use_valid:
 lemmas post_by_hoare = use_valid[rotated]
 
 lemma use_valid_inv:
-  assumes step: "(r, s') \<in> fst (f s)"
+  assumes step: "(r, s') \<in> mres (f s)"
   assumes pres: "\<And>N. \<lbrace>\<lambda>s. N (P s) \<and> E s\<rbrace> f \<lbrace>\<lambda>rv s. N (P s)\<rbrace>"
   shows "E s \<Longrightarrow> P s = P s'"
   using use_valid[where f=f, OF step pres[where N="\<lambda>p. p = P s"]] by simp
@@ -418,7 +407,7 @@ lemma hoare_case_option_wp2:
 (* Might be useful for forward reasoning, when P is known. *)
 lemma hoare_when_cases:
   "\<lbrakk>\<And>s. \<lbrakk>\<not>B; P s\<rbrakk> \<Longrightarrow> Q s; B \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> when B f \<lbrace>\<lambda>_. Q\<rbrace>"
-  by (cases B; simp add: valid_def return_def)
+  by (cases B; simp add: valid_def return_def mres_def)
 
 lemma hoare_vcg_prop:
   "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>"
@@ -624,6 +613,14 @@ lemma hoare_weak_lift_imp:
   "\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> P' s\<rbrace> f \<lbrace>\<lambda>rv s. P \<longrightarrow> Q rv s\<rbrace>"
   by (auto simp add: valid_def split_def)
 
+lemma hoare_weak_lift_impE:
+  "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,\<lbrace>\<lambda>rv s. P \<longrightarrow> E rv s\<rbrace>"
+  by (cases P; simp add: validE_def hoare_vcg_prop)
+
+lemma hoare_weak_lift_imp_R:
+  "\<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace>,- \<Longrightarrow> \<lbrace>\<lambda>s. P \<longrightarrow> Q s\<rbrace> m \<lbrace>\<lambda>rv s. P \<longrightarrow> R rv s\<rbrace>,-"
+  by (cases P, simp_all)
+
 lemmas hoare_vcg_weaken_imp = hoare_weaken_imp  (* FIXME lib: eliminate *)
 
 lemma hoare_vcg_ex_lift:
@@ -724,7 +721,7 @@ lemma return_wp:
 
 lemma get_wp:
   "\<lbrace>\<lambda>s. P s s\<rbrace> get \<lbrace>P\<rbrace>"
-  by(simp add: valid_def split_def get_def)
+  by (simp add: valid_def get_def mres_def)
 
 lemma gets_wp:
   "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>"
@@ -835,12 +832,9 @@ lemma select_wp:
   by (simp add: select_def valid_def mres_def image_def)
 
 lemma state_select_wp:
-  "\<lbrace> \<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t \<rbrace> state_select f \<lbrace>P\<rbrace>"
-  apply (clarsimp simp: state_select_def assert_def)
-  apply (rule hoare_weaken_pre)
-   apply (wp put_wp select_wp hoare_vcg_if_split return_wp fail_wp get_wp)
-  apply simp
-  done
+  "\<lbrace>\<lambda>s. \<forall>t. (s, t) \<in> f \<longrightarrow> P () t\<rbrace> state_select f \<lbrace>P\<rbrace>"
+  unfolding state_select_def2
+  by (wpsimp wp: put_wp select_wp return_wp get_wp assert_wp)
 
 lemma condition_wp:
   "\<lbrakk> \<lbrace>Q\<rbrace> A \<lbrace>P\<rbrace>;  \<lbrace>R\<rbrace> B \<lbrace>P\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>"
@@ -875,18 +869,18 @@ lemma unlessE_wp:
 lemma maybeM_wp:
   "(\<And>x. y = Some x \<Longrightarrow> \<lbrace>P x\<rbrace> m x \<lbrace>Q\<rbrace>) \<Longrightarrow>
    \<lbrace>\<lambda>s. (\<forall>x. y = Some x \<longrightarrow> P x s) \<and> (y = None \<longrightarrow> Q () s)\<rbrace> maybeM m y \<lbrace>Q\<rbrace>"
-  unfolding maybeM_def by (cases y; simp add: bind_def return_def valid_def)
+  unfolding maybeM_def by (wpsimp wp: return_wp) auto
 
 lemma notM_wp:
   "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>c. Q (\<not> c)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> notM m \<lbrace>Q\<rbrace>"
-  unfolding notM_def by (fastforce simp: bind_def return_def valid_def)
+  unfolding notM_def by (wpsimp wp: return_wp)
 
 lemma ifM_wp:
   assumes [wp]: "\<lbrace>Q\<rbrace> f \<lbrace>S\<rbrace>" "\<lbrace>R\<rbrace> g \<lbrace>S\<rbrace>"
   assumes [wp]: "\<lbrace>A\<rbrace> P \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>" "\<lbrace>B\<rbrace> P \<lbrace>\<lambda>c s. \<not>c \<longrightarrow> R s\<rbrace>"
   shows "\<lbrace>A and B\<rbrace> ifM P f g \<lbrace>S\<rbrace>"
-  unfolding ifM_def using assms
-  by (fastforce simp: bind_def valid_def split: if_splits)
+  unfolding ifM_def
+  by (wpsimp wp: hoare_vcg_if_split hoare_vcg_conj_lift)
 
 lemma andM_wp:
   assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"