diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy
new file mode 100644
index 000000000..02dd0b2a3
--- /dev/null
+++ b/lib/Monads/trace/Trace_Empty_Fail.thy
@@ -0,0 +1,343 @@
+(*
+ * Copyright 2023, Proofcraft Pty Ltd
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+theory Trace_Empty_Fail
+  imports
+    Trace_Monad
+    WPSimp
+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)"
+
+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)"
+
+
+subsection \<open>WPC setup\<close>
+
+lemma wpc_helper_empty_fail_final:
+  "empty_fail f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (empty_fail f)"
+  by (clarsimp simp: wpc_helper_def)
+
+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"
+  by (simp add: empty_fail_def)
+
+lemma empty_failD:
+  "\<lbrakk> empty_fail m; fst (m s) = {} \<rbrakk> \<Longrightarrow> 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)"
+  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> {}"
+  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)
+
+
+subsection \<open>Wellformed monads\<close>
+
+(*
+  Collect generic empty_fail lemmas here:
+   - naming convention is emtpy_fail_NAME.
+   - add lemmas with assumptions to [empty_fail_cond] set
+   - add lemmas without assumption to [empty_fail_term] set
+*)
+
+named_theorems empty_fail_term
+named_theorems empty_fail_cond
+
+lemma empty_fail_K_bind[empty_fail_cond]:
+  "empty_fail f \<Longrightarrow> empty_fail (K_bind f x)"
+  by simp
+
+lemma empty_fail_fun_app[empty_fail_cond]:
+  "empty_fail (f x) \<Longrightarrow> empty_fail (f $ x)"
+  by simp
+
+(* empty_fail as such does not need context, but empty_fail_select_f does, so we need to build
+   up context in other rules *)
+lemma empty_fail_If[empty_fail_cond]:
+  "\<lbrakk> P \<Longrightarrow> empty_fail f; \<not>P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)"
+  by (simp split: if_split)
+
+lemma empty_fail_If_applied[empty_fail_cond]:
+  "\<lbrakk> P \<Longrightarrow> empty_fail (f x); \<not>P \<Longrightarrow> empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail ((if P then f else g) x)"
+  by simp
+
+lemma empty_fail_put[empty_fail_term]:
+  "empty_fail (put f)"
+  by (simp add: put_def empty_fail_def)
+
+lemma empty_fail_modify[empty_fail_term]:
+  "empty_fail (modify f)"
+  by (simp add: empty_fail_def simpler_modify_def)
+
+lemma empty_fail_gets[empty_fail_term]:
+  "empty_fail (gets f)"
+  by (simp add: empty_fail_def simpler_gets_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)
+
+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)
+
+lemma empty_fail_return[empty_fail_term]:
+  "empty_fail (return x)"
+  by (simp add: empty_fail_def return_def)
+
+lemma empty_fail_returnOk[empty_fail_term]:
+  "empty_fail (returnOk v)"
+  by (fastforce simp: returnOk_def empty_fail_term)
+
+lemma empty_fail_throwError[empty_fail_term]:
+  "empty_fail (throwError v)"
+  by (fastforce simp: throwError_def empty_fail_term)
+
+lemma empty_fail_lift[empty_fail_cond]:
+  "\<lbrakk> \<And>x. empty_fail (f x) \<rbrakk> \<Longrightarrow> empty_fail (lift f x)"
+  unfolding lift_def
+  by (auto simp: empty_fail_term split: sum.split)
+
+lemma empty_fail_liftE[empty_fail_cond]:
+  "empty_fail f \<Longrightarrow> empty_fail (liftE f)"
+  by (simp add: liftE_def empty_fail_cond empty_fail_term)
+
+lemma empty_fail_bindE[empty_fail_cond]:
+  "\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)"
+  by (simp add: bindE_def empty_fail_cond)
+
+lemma empty_fail_mapM[empty_fail_cond]:
+  assumes m: "\<And>x. x \<in> set xs \<Longrightarrow> empty_fail (m x)"
+  shows "empty_fail (mapM m xs)"
+using m
+proof (induct xs)
+  case Nil
+  thus ?case by (simp add: mapM_def sequence_def empty_fail_term)
+next
+  case Cons
+  have P: "\<And>m x xs. mapM m (x # xs) = (do y \<leftarrow> m x; ys \<leftarrow> (mapM m xs); return (y # ys) od)"
+    by (simp add: mapM_def sequence_def Let_def)
+  from Cons
+  show ?case by (simp add: P m empty_fail_cond empty_fail_term)
+qed
+
+lemma empty_fail_fail[empty_fail_term]:
+  "empty_fail fail"
+  by (simp add: fail_def empty_fail_def)
+
+lemma empty_fail_assert[empty_fail_term]:
+  "empty_fail (assert P)"
+  unfolding assert_def by (simp add: empty_fail_term)
+
+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)
+
+lemma empty_fail_mk_ef[empty_fail_term]:
+  "empty_fail (mk_ef o m)"
+  by (simp add: empty_fail_def mk_ef_def)
+
+lemma empty_fail_gets_the[empty_fail_term]:
+  "empty_fail (gets_the f)"
+  unfolding gets_the_def
+  by (simp add: empty_fail_cond empty_fail_term)
+
+lemma empty_fail_gets_map[empty_fail_term]:
+  "empty_fail (gets_map f p)"
+  unfolding gets_map_def
+  by (simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_whenEs[empty_fail_cond]:
+  "(P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)"
+  "(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f)"
+  by (auto simp add: whenE_def unlessE_def empty_fail_term)
+
+lemma empty_fail_assertE[empty_fail_term]:
+  "empty_fail (assertE P)"
+  by (simp add: assertE_def empty_fail_term)
+
+lemma empty_fail_get[empty_fail_term]:
+  "empty_fail get"
+  by (simp add: empty_fail_def get_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)"
+  by (simp add: catch_def empty_fail_cond empty_fail_term split: sum.split)
+
+lemma empty_fail_guard[empty_fail_term]:
+  "empty_fail (state_assert G)"
+  by (clarsimp simp: state_assert_def empty_fail_cond empty_fail_term)
+
+lemma empty_fail_spec[empty_fail_term]:
+  "empty_fail (state_select F)"
+  by (clarsimp simp: state_select_def empty_fail_def)
+
+lemma empty_fail_when[empty_fail_cond]:
+  "(P \<Longrightarrow> empty_fail x) \<Longrightarrow> empty_fail (when P x)"
+  unfolding when_def
+  by (simp add: empty_fail_term)
+
+lemma empty_fail_unless[empty_fail_cond]:
+  "(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unless P f)"
+  unfolding unless_def
+  by (simp add: empty_fail_cond)
+
+lemma empty_fail_liftM[empty_fail_cond]:
+  "empty_fail m \<Longrightarrow> empty_fail (liftM f m)"
+  unfolding liftM_def
+  by (fastforce simp: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_liftME[empty_fail_cond]:
+  "empty_fail m \<Longrightarrow> empty_fail (liftME f m)"
+  unfolding liftME_def
+  by (simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_handleE[empty_fail_cond]:
+  "\<lbrakk> empty_fail L; \<And>r. empty_fail (R r) \<rbrakk> \<Longrightarrow> empty_fail (L <handle> R)"
+  by (clarsimp simp: handleE_def handleE'_def empty_fail_term empty_fail_cond split: sum.splits)
+
+lemma empty_fail_handle'[empty_fail_cond]:
+  "\<lbrakk>empty_fail f; \<And>e. empty_fail (handler e)\<rbrakk> \<Longrightarrow> empty_fail (f <handle2> handler)"
+  unfolding handleE'_def
+  by (fastforce simp: empty_fail_term empty_fail_cond split: sum.splits)
+
+lemma empty_fail_sequence[empty_fail_cond]:
+  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence ms)"
+  unfolding sequence_def
+  by (induct ms; simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_sequence_x[empty_fail_cond]:
+  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequence_x ms)"
+  unfolding sequence_x_def
+  by (induct ms; simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_sequenceE[empty_fail_cond]:
+  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE ms)"
+  unfolding sequenceE_def
+  by (induct ms; simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_sequenceE_x[empty_fail_cond]:
+  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (sequenceE_x ms)"
+  unfolding sequenceE_x_def
+  by (induct ms; simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_mapM_x[empty_fail_cond]:
+  "(\<And>m. m \<in> f ` set ms \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapM_x f ms)"
+  unfolding mapM_x_def
+  by (fastforce intro: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_mapME[empty_fail_cond]:
+  "(\<And>m. m \<in> f ` set xs \<Longrightarrow> empty_fail m) \<Longrightarrow> empty_fail (mapME f xs)"
+  unfolding mapME_def
+  by (fastforce intro: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_mapME_x[empty_fail_cond]:
+  "(\<And>m'. m' \<in> f ` set xs \<Longrightarrow> empty_fail m') \<Longrightarrow> empty_fail (mapME_x f xs)"
+  unfolding mapME_x_def
+  by (fastforce intro: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_filterM[empty_fail_cond]:
+  "(\<And>m. m \<in> set ms \<Longrightarrow> empty_fail (P m)) \<Longrightarrow> empty_fail (filterM P ms)"
+  by (induct ms; simp add: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_zipWithM_x[empty_fail_cond]:
+  "(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM_x f xs ys)"
+  unfolding zipWithM_x_def zipWith_def
+  by (fastforce intro: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_zipWithM[empty_fail_cond]:
+  "(\<And>x y. empty_fail (f x y)) \<Longrightarrow> empty_fail (zipWithM f xs ys)"
+  unfolding zipWithM_def zipWith_def
+  by (fastforce intro: empty_fail_term empty_fail_cond)
+
+lemma empty_fail_maybeM[empty_fail_cond]:
+  "\<forall>x. empty_fail (f x) \<Longrightarrow> empty_fail (maybeM f t)"
+  unfolding maybeM_def
+  by (fastforce intro: empty_fail_term split: option.splits)
+
+lemma empty_fail_ifM[empty_fail_cond]:
+  "\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifM P a b)"
+  by (simp add: ifM_def empty_fail_cond)
+
+lemma empty_fail_ifME[empty_fail_cond]:
+  "\<lbrakk> empty_fail P; empty_fail a; empty_fail b \<rbrakk> \<Longrightarrow> empty_fail (ifME P a b)"
+  by (simp add: ifME_def empty_fail_cond)
+
+lemma empty_fail_whenM[empty_fail_cond]:
+  "\<lbrakk> empty_fail P; empty_fail f \<rbrakk> \<Longrightarrow> empty_fail (whenM P f)"
+  by (simp add: whenM_def empty_fail_term empty_fail_cond)
+
+lemma empty_fail_andM[empty_fail_cond]:
+  "\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (andM A B)"
+  by (simp add: andM_def empty_fail_term empty_fail_cond)
+
+lemma empty_fail_orM[empty_fail_cond]:
+  "\<lbrakk> empty_fail A; empty_fail B \<rbrakk> \<Longrightarrow> empty_fail (orM A B)"
+  by (simp add: orM_def empty_fail_term empty_fail_cond)
+
+lemma empty_fail_notM[empty_fail_cond]:
+  "empty_fail A \<Longrightarrow> empty_fail (notM A)"
+  by (simp add: notM_def empty_fail_term empty_fail_cond)
+
+(* not everything [simp] by default, because side conditions can slow down simp a lot *)
+lemmas empty_fail[wp, intro!] = empty_fail_term empty_fail_cond
+lemmas [simp] = empty_fail_term
+
+
+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)
+
+lemma empty_fail_liftM_eq[simp]:
+  "empty_fail (liftM f m) = empty_fail m"
+  unfolding liftM_def
+  by (fastforce dest: empty_fail_bindD1)
+
+lemma empty_fail_liftE_eq[simp]:
+  "empty_fail (liftE f) = empty_fail f"
+  by (fastforce simp: liftE_def empty_fail_def bind_def)
+
+lemma liftME_empty_fail_eq[simp]:
+  "empty_fail (liftME f m) = empty_fail m"
+  unfolding liftME_def
+  by (fastforce dest: empty_fail_bindD1 simp: bindE_def)
+
+(* legacy name binding *)
+lemmas empty_fail_error_bits = empty_fail_returnOk empty_fail_throwError empty_fail_liftE_eq
+
+end
diff --git a/lib/Monads/trace/Trace_In_Monad.thy b/lib/Monads/trace/Trace_In_Monad.thy
index 073d4096b..24769154c 100644
--- a/lib/Monads/trace/Trace_In_Monad.thy
+++ b/lib/Monads/trace/Trace_In_Monad.thy
@@ -54,6 +54,10 @@ lemma inl_whenE:
   "((Inl x, s') \<in> mres (whenE P f s)) = (P \<and> (Inl x, s') \<in> mres (f s))"
   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)
+
 lemma in_fail:
   "r \<in> mres (fail s) = False"
   by (simp add: fail_def mres_def)
diff --git a/lib/Monads/trace/Trace_Lemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy
index 9ce793eea..f6e7706f3 100644
--- a/lib/Monads/trace/Trace_Lemmas.thy
+++ b/lib/Monads/trace/Trace_Lemmas.thy
@@ -30,17 +30,169 @@ 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)
+
+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'"
+  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>
+  \<Longrightarrow> (f >>=E g) s = (f' >>=E g') s'"
+  by (auto simp: bindE_def lift_def split: sum.splits intro!: bind_apply_cong)
+
+lemma K_bind_apply_cong[fundef_cong]:
+  "\<lbrakk> f st = f' st' \<rbrakk> \<Longrightarrow> K_bind f arg st = K_bind f' arg' st'"
+  by simp
+
+lemma when_apply_cong[fundef_cong]:
+  "\<lbrakk> C = C'; s = s'; C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> when C m s = when C' m' s'"
+  by (simp add: when_def)
+
+lemma unless_apply_cong[fundef_cong]:
+  "\<lbrakk> C = C'; s = s'; \<not> C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> unless C m s = unless C' m' s'"
+  by (simp add: when_def unless_def)
+
+lemma whenE_apply_cong[fundef_cong]:
+  "\<lbrakk> C = C'; s = s'; C' \<Longrightarrow> m s' = m' s' \<rbrakk> \<Longrightarrow> whenE C m s = whenE C' m' s'"
+  by (simp add: whenE_def)
+
+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)
+
+lemma bind_dummy_ret_val:
+  "do y \<leftarrow> a; b od = do a; b od"
+  by simp
+
 lemma fail_update[iff]:
   "fail (f s) = fail s"
   by (simp add: fail_def)
 
+lemma fail_bind[simp]:
+  "fail >>= f = fail"
+  by (simp add: bind_def fail_def)
+
+lemma fail_bindE[simp]:
+  "fail >>=E f = fail"
+  by (simp add: bindE_def bind_def fail_def)
+
+lemma assert_A_False[simp]:
+  "assert False = fail"
+  by (simp add: assert_def)
+
 lemma assert_A_True[simp]:
   "assert True = return ()"
   by (simp add: assert_def)
 
+lemma assert_False[simp]:
+  "assert False >>= f = fail"
+  by simp
+
+lemma assert_True[simp]:
+  "assert True >>= f = f ()"
+  by simp
+
+lemma assertE_False[simp]:
+  "assertE False >>=E f = fail"
+  by (simp add: assertE_def)
+
+lemma assertE_True[simp]:
+  "assertE True >>=E f = f ()"
+  by (simp add: assertE_def)
+
+lemma when_False_bind[simp]:
+  "when False g >>= f = f ()"
+  by (rule ext) (simp add: when_def bind_def return_def)
+
+lemma when_True_bind[simp]:
+  "when True g >>= f = g >>= f"
+  by (simp add: when_def bind_def return_def)
+
+lemma whenE_False_bind[simp]:
+  "whenE False g >>=E f = f ()"
+  by (simp add: whenE_def bindE_def returnOk_def lift_def)
+
+lemma whenE_True_bind[simp]:
+  "whenE True g >>=E f = g >>=E f"
+  by (simp add: whenE_def bindE_def returnOk_def lift_def)
+
+lemma when_True[simp]:
+  "when True X = X"
+  by (clarsimp simp: when_def)
+
+lemma when_False[simp]:
+  "when False X = return ()"
+  by (clarsimp simp: when_def)
+
+lemma unless_False[simp]:
+  "unless False X = X"
+  by (clarsimp simp: unless_def)
+
+lemma unlessE_False[simp]:
+  "unlessE False f = f"
+  unfolding unlessE_def by fastforce
+
+lemma unless_True[simp]:
+  "unless True X = return ()"
+  by (clarsimp simp: unless_def)
+
+lemma unlessE_True[simp]:
+  "unlessE True f = returnOk ()"
+  unfolding unlessE_def by fastforce
+
+lemma unlessE_whenE:
+  "unlessE P = whenE (\<not>P)"
+  by (rule ext) (simp add: unlessE_def whenE_def)
+
+lemma unless_when:
+  "unless P = when (\<not>P)"
+  by (rule ext) (simp add: unless_def when_def)
+
+lemma gets_to_return[simp]:
+  "gets (\<lambda>s. v) = return v"
+  by (clarsimp simp: gets_def put_def get_def bind_def return_def)
+
+lemma assert_opt_Some:
+  "assert_opt (Some x) = return x"
+  by (simp add: assert_opt_def)
+
+lemma assertE_liftE:
+  "assertE P = liftE (assert P)"
+  by (simp add: assertE_def assert_def liftE_def returnOk_def)
+
+lemma liftE_handleE'[simp]:
+  "(liftE a <handle2> b) = liftE a"
+  by (clarsimp simp: liftE_def handleE'_def)
+
+lemma liftE_handleE[simp]:
+  "(liftE a <handle> b) = liftE a"
+  unfolding handleE_def by simp
+
+lemma alternative_bind:
+  "((a \<sqinter> b) >>= c) = ((a >>= c) \<sqinter> (b >>= c))"
+  by (fastforce simp add: alternative_def bind_def split_def)
+
+lemma alternative_refl:
+  "(a \<sqinter> a) = a"
+  by (simp add: alternative_def)
+
+lemma alternative_com:
+  "(f \<sqinter> g) = (g \<sqinter> f)"
+  by (auto simp: alternative_def)
+
+lemma liftE_alternative:
+  "liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)"
+  by (simp add: liftE_def alternative_bind)
+
 
 subsection \<open>Lifting and Alternative Basic Definitions\<close>
 
@@ -65,7 +217,7 @@ lemma liftM_id[simp]:
   by (auto simp: liftM_def)
 
 lemma liftM_bind:
-  "liftM t f >>= g = (f >>= (\<lambda>x. g (t x)))"
+  "liftM t f >>= g = f >>= (\<lambda>x. g (t x))"
   by (simp add: liftM_def bind_assoc)
 
 lemma gets_bind_ign:
@@ -86,4 +238,33 @@ lemma bind_eqI:
   "\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'"
   by (auto simp: bind_def split_def)
 
+lemma condition_split:
+  "P (condition C a b s) \<longleftrightarrow> (C s \<longrightarrow> P (a s)) \<and> (\<not>C s \<longrightarrow> P (b s))"
+  by (clarsimp simp: condition_def)
+
+lemma condition_split_asm:
+  "P (condition C a b s) \<longleftrightarrow> (\<not>(C s \<and> \<not> P (a s) \<or> \<not>C s \<and> \<not>P (b s)))"
+  by (clarsimp simp: condition_def)
+
+lemmas condition_splits = condition_split condition_split_asm
+
+lemma condition_true_triv[simp]:
+  "condition (\<lambda>_. True) A B = A"
+  by (fastforce split: condition_splits)
+
+lemma condition_false_triv[simp]:
+  "condition (\<lambda>_. False) A B = B"
+  by (fastforce split: condition_splits)
+
+lemma condition_true:
+  "P s \<Longrightarrow> condition P A B s = A s"
+  by (clarsimp simp: condition_def)
+
+lemma condition_false:
+  "\<not> P s \<Longrightarrow> condition P A B s = B s"
+  by (clarsimp simp: condition_def)
+
+lemmas arg_cong_bind = arg_cong2[where f=bind]
+lemmas arg_cong_bind1 = arg_cong_bind[OF refl ext]
+
 end
diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy
index 8ddf802f4..37f7a70ea 100644
--- a/lib/Monads/trace/Trace_Monad.thy
+++ b/lib/Monads/trace/Trace_Monad.thy
@@ -46,6 +46,23 @@ text \<open>
   pair of result and state when the computation did not fail.\<close>
 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.
+  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
+  (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]
+      else raise Match
+  in [(@{type_syntax "fun"}, monad_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
   "mres r = Result -` (snd ` r)"
@@ -124,6 +141,12 @@ 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))"
+
 subsection "Failure"
 
 text \<open>
@@ -185,6 +208,13 @@ text \<open>
 definition gets_the :: "('s \<Rightarrow> 'a option) \<Rightarrow> ('s, 'a) tmonad" 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>
+definition
+  gets_map :: "('s \<Rightarrow> 'a \<Rightarrow> 'b option) \<Rightarrow> 'a \<Rightarrow> ('s, 'b) nondet_monad" where
+  "gets_map f p \<equiv> gets f >>= (\<lambda>m. assert_opt (m p))"
+
 
 subsection \<open>The Monad Laws\<close>
 
@@ -490,6 +520,10 @@ 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
+  "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>
 definition sequence_x :: "('s, 'a) tmonad list \<Rightarrow> ('s, unit) tmonad" where
   "sequence_x xs \<equiv> foldr (\<lambda>x y. x >>= (\<lambda>_. y)) xs (return ())"
@@ -678,6 +712,48 @@ definition whileLoopE ::
 notation (output)
   whileLoopE  ("(whileLoopE (_)//  (_))" [1000, 1000] 1000)
 
+
+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
+  "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
+  "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
+  "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
+  "whenM t m = ifM t m (return ())"
+
+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
+  "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 ee0730def..265b8c73c 100644
--- a/lib/Monads/trace/Trace_Monad_Equations.thy
+++ b/lib/Monads/trace/Trace_Monad_Equations.thy
@@ -10,11 +10,350 @@
 
 theory Trace_Monad_Equations
   imports
-    Trace_Lemmas
+    Trace_No_Fail
 begin
 
+lemmas assertE_assert = assertE_liftE
+
+lemma assert_def2:
+  "assert v = assert_opt (if v then Some () else None)"
+  by (cases v; simp add: assert_def assert_opt_def)
+
+lemma return_returnOk:
+  "return (Inr x) = returnOk x"
+  unfolding returnOk_def by simp
+
+lemma exec_modify:
+  "(modify f >>= g) s = g () (f s)"
+  by (simp add: bind_def simpler_modify_def)
+
+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
+
 lemmas bind_then_eq = arg_cong2[where f=bind, OF _ refl]
 
+lemma bindE_bind_linearise:
+  "((f >>=E g) >>= h) =
+   (f >>= case_sum (h o Inl) (\<lambda>rv. g rv >>= h))"
+  apply (simp add: bindE_def bind_assoc)
+  apply (rule ext, rule bind_apply_cong, rule refl)
+  apply (simp add: lift_def throwError_def split: sum.split)
+  done
+
+lemma throwError_bind:
+  "(throwError e >>= f) = (f (Inl e))"
+  by (simp add: throwError_def)
+
+lemma bind_bindE_assoc:
+  "((f >>= g) >>=E h)
+    = f >>= (\<lambda>rv. g rv >>=E h)"
+  by (simp add: bindE_def bind_assoc)
+
+lemma returnOk_bind:
+  "returnOk v >>= f = (f (Inr v))"
+  by (simp add: returnOk_def)
+
+lemma liftE_bind:
+  "(liftE m >>= m') = (m >>= (\<lambda>rv. m' (Inr rv)))"
+  by (simp add: liftE_def)
+
+lemma catch_throwError: "catch (throwError ft) g = g ft"
+  by (simp add: catch_def throwError_bind)
+
+lemma cart_singleton_image:
+  "S \<times> {s} = (\<lambda>v. (v, s)) ` S"
+  by auto
+
+lemma liftE_bindE_handle:
+  "((liftE f >>=E (\<lambda>x. g x)) <handle> h)
+      = f >>= (\<lambda>x. g x <handle> h)"
+  by (simp add: liftE_bindE handleE_def handleE'_def
+                bind_assoc)
+
+lemma catch_liftE:
+  "catch (liftE g) h = g"
+  by (simp add: catch_def liftE_def)
+
+lemma catch_liftE_bindE:
+  "catch (liftE g >>=E (\<lambda>x. f x)) h = g >>= (\<lambda>x. catch (f x) h)"
+  by (simp add: liftE_bindE catch_def bind_assoc)
+
+lemma returnOk_catch_bind:
+  "catch (returnOk v) h >>= g = g v"
+  by (simp add: returnOk_liftE catch_liftE)
+
+lemma liftE_bindE_assoc:
+  "(liftE f >>=E g) >>= h = f >>= (\<lambda>x. g x >>= h)"
+  by (simp add: liftE_bindE bind_assoc)
+
+lemma unlessE_throw_catch_If:
+  "catch (unlessE P (throwError e) >>=E f) g
+      = (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)
+
+lemma alternative_liftE_returnOk:
+  "(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)"
+  by (simp add: liftE_def alternative_def returnOk_def bind_def return_def)
+
+lemma gets_the_return:
+  "(return x = gets_the f) = (\<forall>s. f s = Some x)"
+  apply (subst fun_eq_iff)
+  apply (simp add: return_def gets_the_def exec_gets
+                   assert_opt_def fail_def
+            split: option.split)
+  apply auto
+  done
+
+lemma gets_the_returns:
+  "(return x = gets_the f) = (\<forall>s. f s = Some x)"
+  "(returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x))"
+  "(throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))"
+  by (simp_all add: returnOk_def throwError_def
+                    gets_the_return)
+
+lemma all_rv_choice_fn_eq_pred:
+  "\<lbrakk> \<And>rv. P rv \<Longrightarrow> \<exists>fn. f rv = g fn \<rbrakk> \<Longrightarrow> \<exists>fn. \<forall>rv. P rv \<longrightarrow> f rv = g (fn rv)"
+  apply (rule_tac x="\<lambda>rv. SOME h. f rv = g h" in exI)
+  apply (clarsimp split: if_split)
+  by (meson someI_ex)
+
+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))"
+  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')"
+  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
+                   assert_opt_def fun_eq_iff
+            split: option.split)
+  done
+
+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')"
+  apply (simp add: bindE_def)
+  apply (erule gets_the_eq_bind)
+  apply (simp add: lift_def gets_the_returns split: sum.split)
+  apply fastforce
+  done
+
+lemma gets_the_fail:
+  "(fail = gets_the f) = (\<forall>s. f s = None)"
+  by (simp add: gets_the_def exec_gets assert_opt_def
+                fail_def return_def fun_eq_iff
+         split: option.split)
+
+lemma gets_the_asserts:
+  "(fail = gets_the f) = (\<forall>s. f s = None)"
+  "(assert P = gets_the g) = (\<forall>s. g s = (if P then Some () else None))"
+  "(assertE P = gets_the h) = (\<forall>s. h s = (if P then Some (Inr ()) else None))"
+  by (simp add: assert_def assertE_def gets_the_fail gets_the_returns
+         split: if_split)+
+
+lemma ex_const_function:
+  "\<exists>f. \<forall>s. f (f' s) = v"
+  by force
+
+lemma gets_the_condsE:
+  "(\<exists>fn. whenE P 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')))"
+  by (simp add: whenE_def unlessE_def gets_the_returns ex_const_function
+         split: if_split)+
+
+lemma let_into_return:
+  "(let f = x in m f) = (do f \<leftarrow> return x; m f od)"
+  by simp
+
+lemma liftME_return:
+  "liftME f (returnOk v) = returnOk (f v)"
+  by (simp add: liftME_def)
+
+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)"
+  by (simp split: list.split)
+
+lemma whenE_liftE:
+  "whenE P (liftE f) = liftE (when P f)"
+  by (simp add: whenE_def when_def returnOk_liftE)
+
+lemma whenE_whenE_body:
+  "whenE P (throwError f) >>=E (\<lambda>_. whenE Q (throwError f) >>=E r) = whenE (P \<or> Q) (throwError f) >>=E r"
+  apply (cases P)
+   apply (simp add: whenE_def)
+  apply simp
+  done
+
+lemma whenE_whenE_same:
+  "whenE P (throwError f) >>=E (\<lambda>_. whenE P (throwError g) >>=E r) = whenE P (throwError f) >>=E r"
+  apply (cases P)
+   apply (simp add: whenE_def)
+  apply simp
+  done
+
+lemma maybe_fail_bind_fail:
+  "unless P fail >>= (\<lambda>_. fail) = fail"
+  "when P fail >>= (\<lambda>_. fail) = fail"
+  by (clarsimp simp: bind_def fail_def return_def
+                     unless_def when_def)+
+
+lemma select_singleton[simp]:
+  "select {x} = return x"
+  by (fastforce simp add: fun_eq_iff select_def return_def)
+
+lemma return_modify:
+  "return () = modify id"
+  by (simp add: return_def simpler_modify_def)
+
+lemma liftE_liftM_liftME:
+  "liftE (liftM f m) = liftME f (liftE m)"
+  by (simp add: liftE_liftM liftME_liftM liftM_def)
+
+lemma bind_return_unit:
+  "f = (f >>= (\<lambda>x. return ()))"
+  by simp
+
+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)))"
+  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))"
+  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"
+  by (simp add: gets_the_def bind_assoc exec_gets assert_opt_def)
+
+lemma zipWithM_x_modify:
+  "zipWithM_x (\<lambda>a b. modify (f a b)) as bs
+   = modify (\<lambda>s. foldl (\<lambda>s (a, b). f a b s) s (zip as bs))"
+  apply (simp add: zipWithM_x_def zipWith_def sequence_x_def)
+  apply (induct ("zip as bs"))
+   apply (simp add: simpler_modify_def return_def)
+  apply (rule ext)
+  apply (simp add: simpler_modify_def bind_def split_def)
+  done
+
+lemma assert2:
+  "(do v1 \<leftarrow> assert P; v2 \<leftarrow> assert Q; c od)
+     = (do v \<leftarrow> assert (P \<and> Q); c od)"
+  by (simp add: assert_def split: if_split)
+
+lemma assert_opt_def2:
+  "assert_opt v = (do assert (v \<noteq> None); return (the v) od)"
+  by (simp add: assert_opt_def split: option.split)
+
+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)"
+  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)"
+  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"
+  by (simp_all add: fun_eq_iff modify_def bind_assoc exec_gets
+                    exec_get exec_put)
+
+lemma bind_assoc2:
+  "(do x \<leftarrow> a; _ \<leftarrow> b; c x od) = (do x \<leftarrow> (do x' \<leftarrow> a; _ \<leftarrow> b; return x' od); c x od)"
+  by (simp add: bind_assoc)
+
+lemma bind_assoc_return_reverse:
+  "do x \<leftarrow> f;
+      _ \<leftarrow> g x;
+      h x
+   od =
+   do x \<leftarrow> do x \<leftarrow> f;
+              _ \<leftarrow> g x;
+              return x
+           od;
+      h x
+   od"
+  by (simp only: bind_assoc return_bind)
+
+lemma if_bind:
+  "(if P then (a >>= (\<lambda>_. b)) else return ()) =
+   (if P then a else return ()) >>= (\<lambda>_. if P then b else return ())"
+  by (cases P; simp)
+
+lemma bind_liftE_distrib: "(liftE (A >>= (\<lambda>x. B x))) = (liftE A >>=E (\<lambda>x. liftE (\<lambda>s. B x s)))"
+  by (clarsimp simp: liftE_def bindE_def lift_def bind_assoc)
+
+lemma if_catch_distrib:
+  "((if P then f else g) <catch> h) = (if P then f <catch> h else g <catch> h)"
+  by (simp split: if_split)
+
+lemma will_throw_and_catch:
+  "f = throwError e \<Longrightarrow> (f <catch> (\<lambda>_. g)) = g"
+  by (simp add: catch_def throwError_def)
+
+lemma catch_is_if:
+  "(doE x <- f; g x odE <catch> h) =
+   do
+     rv <- f;
+     if sum.isl rv then h (projl rv) else g (projr rv) <catch> h
+   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)
+  done
+
+lemma liftE_K_bind: "liftE ((K_bind (\<lambda>s. A s)) x) = K_bind (liftE (\<lambda>s. A s)) x"
+  by clarsimp
+
+lemma monad_eq_split_tail:
+  "\<lbrakk>f = g; a s = b s\<rbrakk> \<Longrightarrow> (a >>= f) s = ((b >>= g) s)"
+  by (simp add:bind_def)
+
+lemma assert_opt_If:
+  "assert_opt v = If (v = None) fail (return (the v))"
+  by (simp add: assert_opt_def split: option.split)
+
+lemma if_to_top_of_bind:
+  "(bind (If P x y) z) = If P (bind x z) (bind y z)"
+  by (simp split: if_split)
+
+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)
diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy
index 9a12ec1ee..27b5d9d34 100644
--- a/lib/Monads/trace/Trace_More_VCG.thy
+++ b/lib/Monads/trace/Trace_More_VCG.thy
@@ -13,8 +13,815 @@ theory Trace_More_VCG
     Trace_VCG
 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>"
+  by (erule hoare_strengthen_post, simp)
+
+lemma hoare_post_add:
+  "\<lbrace>P\<rbrace> S \<lbrace>\<lambda>r s. R r s \<and> Q r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>"
+  by (erule hoare_strengthen_post, simp)
+
+lemma hoare_post_addE:
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. R s \<and> Q s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. Q s\<rbrace>, \<lbrace>T\<rbrace>"
+  by (erule hoare_post_impErr'; simp)
+
+lemma hoare_pre_add:
+  "(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>)"
+  apply (subst iff_conv_conj_imp)
+  by(intro conjI impI; rule hoare_weaken_pre, assumption, clarsimp)
+
+lemma hoare_pre_addE:
+  "(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>)"
+  apply (subst iff_conv_conj_imp)
+  by(intro conjI impI; rule hoare_weaken_preE, assumption, clarsimp)
+
+lemma hoare_name_pre_state:
+  "\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+  by (clarsimp simp: valid_def)
+
+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>"
+
+  "\<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. if P then X rv else Y rv\<rbrace>"
+  by (auto simp: valid_def split_def)
+
+lemma hoare_vcg_if_lift_strong:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>P\<rbrace>; \<lbrace>\<lambda>s. \<not> P' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>R'\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. if P' s then Q' s else R' s\<rbrace> f \<lbrace>\<lambda>rv s. if P rv s then Q rv s else R rv s\<rbrace>"
+
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>P\<rbrace>; \<lbrace>\<lambda>s. \<not> P' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace> Q\<rbrace>; \<lbrace>R'\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. if P' s then Q' s else R' s\<rbrace> f \<lbrace>\<lambda>rv s. (if P rv s then Q rv else R rv) s\<rbrace>"
+  by (wpsimp wp: hoare_vcg_imp_lift' | assumption | fastforce)+
+
+lemma hoare_vcg_imp_lift_pre_add:
+  "\<lbrakk> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. R rv s\<rbrace>; f \<lbrace>\<lambda>s. \<not> Q s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace>"
+  apply (rule hoare_weaken_pre)
+   apply (rule hoare_vcg_imp_lift')
+    apply fastforce
+   apply fastforce
+  apply (clarsimp simp: pred_conj_def valid_def)
+  done
+
 lemma hoare_pre_tautI:
   "\<lbrakk> \<lbrace>A and P\<rbrace> a \<lbrace>B\<rbrace>; \<lbrace>A and not P\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace>"
   by (fastforce simp: valid_def split_def pred_conj_def pred_neg_def)
 
+lemma hoare_lift_Pf_pre_conj:
+  assumes P: "\<And>x. \<lbrace>\<lambda>s. Q x s\<rbrace> m \<lbrace>P x\<rbrace>"
+  assumes f: "\<And>P. \<lbrace>\<lambda>s. P (g s) \<and> R s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
+  shows "\<lbrace>\<lambda>s. Q (g s) s \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. P (f s) rv s\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (rule use_valid [OF _ P], simp)
+  apply (rule use_valid [OF _ f], simp, simp)
+  done
+
+lemmas hoare_lift_Pf4 = hoare_lift_Pf_pre_conj[where R=\<top>, simplified]
+lemmas hoare_lift_Pf3 = hoare_lift_Pf4[where f=f and g=f for f]
+lemmas hoare_lift_Pf2 = hoare_lift_Pf3[where P="\<lambda>f _. P f" for P]
+lemmas hoare_lift_Pf = hoare_lift_Pf2[where Q=P and P=P for P]
+
+lemmas hoare_lift_Pf3_pre_conj = hoare_lift_Pf_pre_conj[where f=f and g=f for f]
+lemmas hoare_lift_Pf2_pre_conj = hoare_lift_Pf3_pre_conj[where P="\<lambda>f _. P f" for P]
+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>"
+  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>"
+  apply (simp only: imp_conv_disj)
+  apply (erule(1) hoare_vcg_disj_lift)
+  done
+
+lemma hoare_vcg_ex_lift_R:
+  "\<lbrakk> \<And>v. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>v. P v s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>v. Q v rv s\<rbrace>,-"
+  apply (simp add: validE_R_def validE_def)
+  apply (rule hoare_strengthen_post, erule hoare_vcg_ex_lift)
+  apply (auto split: sum.split)
+  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>,-"
+  by (cases v) auto
+
+lemma hoare_vcg_conj_liftE_R:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>,-; \<lbrace>Q\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> Q' rv s\<rbrace>, -"
+  apply (simp add: validE_R_def validE_def valid_def split: sum.splits)
+  apply blast
+  done
+
+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)
+
+lemma hoare_ex_all:
+  "(\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>"
+  apply (rule iffI)
+   apply (fastforce simp: valid_def)+
+  done
+
+lemma hoare_imp_eq_substR:
+  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<longrightarrow> Q x s\<rbrace>,-"
+  by (fastforce simp add: valid_def validE_R_def validE_def split: sum.splits)
+
+lemma hoare_split_bind_case_sum:
+  assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>"
+             "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>"
+  assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
+  shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>"
+  apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]])
+  apply (case_tac x, simp_all add: x)
+  done
+
+lemma hoare_split_bind_case_sumE:
+  assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+             "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
+  shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (unfold validE_def)
+  apply (rule hoare_seq_ext [OF _ y[unfolded validE_def]])
+  apply (case_tac x, simp_all add: x [unfolded validE_def])
+  done
+
+lemma assertE_sp:
+  "\<lbrace>P\<rbrace> assertE Q \<lbrace>\<lambda>rv s. Q \<and> P s\<rbrace>,\<lbrace>E\<rbrace>"
+  by (clarsimp simp: assertE_def) wp
+
+lemma throwErrorE_E [wp]:
+  "\<lbrace>Q e\<rbrace> throwError e -, \<lbrace>Q\<rbrace>"
+  by (simp add: validE_E_def) wp
+
+lemma gets_inv [simp]:
+  "\<lbrace> P \<rbrace> gets f \<lbrace> \<lambda>r. P \<rbrace>"
+  by (simp add: gets_def, wp)
+
+lemma select_inv:
+  "\<lbrace> P \<rbrace> select S \<lbrace> \<lambda>r. P \<rbrace>"
+  by (simp add: select_def valid_def)
+
+lemmas return_inv = hoare_return_drop_var
+
+lemma assert_inv: "\<lbrace>P\<rbrace> assert Q \<lbrace>\<lambda>r. P\<rbrace>"
+  unfolding assert_def
+  by (cases Q) simp+
+
+lemma assert_opt_inv: "\<lbrace>P\<rbrace> assert_opt Q \<lbrace>\<lambda>r. P\<rbrace>"
+  unfolding assert_opt_def
+  by (cases Q) simp+
+
+lemma case_options_weak_wp:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>x. \<lbrace>P'\<rbrace> g x \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> case opt of None \<Rightarrow> f | Some x \<Rightarrow> g x \<lbrace>Q\<rbrace>"
+  apply (cases opt)
+   apply (clarsimp elim!: hoare_weaken_pre)
+  apply (rule hoare_weaken_pre [where Q=P'])
+   apply simp+
+  done
+
+lemma case_option_wp_None_return:
+  assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>"
+  shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk>
+         \<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace>
+             (case opt of None \<Rightarrow> return () | Some x \<Rightarrow> f x)
+             \<lbrace>\<lambda>_. Q\<rbrace>"
+  by (cases opt; wpsimp)
+
+lemma case_option_wp_None_returnOk:
+  assumes [wp]: "\<And>x. \<lbrace>P' x\<rbrace> f x \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
+  shows "\<lbrakk>\<And>x s. (Q and P x) s \<Longrightarrow> P' x s \<rbrakk>
+         \<Longrightarrow> \<lbrace>Q and (\<lambda>s. opt \<noteq> None \<longrightarrow> P (the opt) s)\<rbrace>
+             (case opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> f x)
+             \<lbrace>\<lambda>_. Q\<rbrace>,\<lbrace>E\<rbrace>"
+  by (cases opt; wpsimp)
+
+lemma list_cases_weak_wp:
+  assumes "\<lbrace>P_A\<rbrace> a \<lbrace>Q\<rbrace>"
+  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>"
+  apply (cases ts)
+  apply (simp, rule hoare_weaken_pre, rule assms, simp)+
+  done
+
+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. (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>"
+  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. (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>, -"
+  by (auto simp: valid_def validE_R_def validE_def split_def)
+
+lemma hoare_vcg_imp_liftE:
+  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, \<lbrace>A\<rbrace>; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>A\<rbrace> \<rbrakk>
+   \<Longrightarrow> \<lbrace>\<lambda>s. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, \<lbrace>A\<rbrace>"
+  apply (simp only: imp_conv_disj)
+  apply (clarsimp simp: validE_def valid_def split_def sum.case_eq_if)
+  done
+
+lemma hoare_list_all_lift:
+  "(\<And>r. r \<in> set xs \<Longrightarrow> \<lbrace>Q r\<rbrace> f \<lbrace>\<lambda>rv. Q r\<rbrace>)
+   \<Longrightarrow> \<lbrace>\<lambda>s. list_all (\<lambda>r. Q r s) xs\<rbrace> f \<lbrace>\<lambda>rv s. list_all (\<lambda>r. Q r s) xs\<rbrace>"
+  apply (induct xs; simp)
+  apply wpsimp
+  apply (rule hoare_vcg_conj_lift; simp)
+  done
+
+lemma undefined_valid: "\<lbrace>\<bottom>\<rbrace> undefined \<lbrace>Q\<rbrace>"
+  by (rule hoare_pre_cont)
+
+lemma assertE_wp:
+  "\<lbrace>\<lambda>s. F \<longrightarrow> Q () s\<rbrace> assertE F \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (rule hoare_pre)
+   apply (unfold assertE_def)
+   apply wp
+  apply simp
+  done
+
+lemma doesn't_grow_proof:
+  assumes y: "\<And>s. finite (S s)"
+  assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. card (S s) < n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (subgoal_tac "S b \<subseteq> S s")
+   apply (drule card_mono [OF y], simp)
+  apply clarsimp
+  apply (rule ccontr)
+  apply (subgoal_tac "x \<notin> S b", simp)
+  apply (erule use_valid [OF _ x])
+  apply simp
+  done
+
+lemma hoare_vcg_propE_R:
+  "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>, -"
+  by (simp add: validE_R_def validE_def valid_def split_def split: sum.split)
+
+lemma set_preserved_proof:
+  assumes y: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<in> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<in> S s\<rbrace>"
+  assumes x: "\<And>x. \<lbrace>\<lambda>s. Q s \<and> x \<notin> S s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. Q s \<and> P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  by (metis (mono_tags, lifting) equalityI post_by_hoare subsetI x y)
+
+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
+   \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (drule spec, erule mp)
+  apply (clarsimp simp: subset_iff)
+  apply (rule ccontr)
+  apply (drule(1) use_valid [OF _ x])
+  apply simp
+  done
+
+lemma shrinks_proof:
+  assumes y: "\<And>s. finite (S s)"
+  assumes x: "\<And>x. \<lbrace>\<lambda>s. x \<notin> S s \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
+  assumes z: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. x \<notin> S s\<rbrace>"
+  assumes w: "\<And>s. P s \<Longrightarrow> x \<in> S s"
+  shows      "\<lbrace>\<lambda>s. card (S s) \<le> n \<and> P s\<rbrace> f \<lbrace>\<lambda>rv s. card (S s) < n\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (subgoal_tac "S b \<subset> S s")
+   apply (drule psubset_card_mono [OF y], simp)
+  apply (rule psubsetI)
+   apply clarsimp
+   apply (rule ccontr)
+   apply (subgoal_tac "x \<notin> S b", simp)
+   apply (erule use_valid [OF _ x])
+   apply simp
+  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'"
+  unfolding validE_R_def validE_def
+  by (frule(2) use_valid, simp)
+
+lemma valid_preservation_ex:
+  assumes x: "\<And>x P. \<lbrace>\<lambda>s. P (f s x :: 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s x)\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. P (f s :: 'a \<Rightarrow> 'b)\<rbrace> m \<lbrace>\<lambda>rv s. P (f s)\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (erule subst[rotated, where P=P])
+  apply (rule ext)
+  apply (erule use_valid [OF _ x])
+  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>"
+  by (wpsimp wp: a)
+
+lemma whenE_throwError_wp:
+  "\<lbrace>\<lambda>s. \<not> P \<longrightarrow> Q s\<rbrace> whenE P (throwError e) \<lbrace>\<lambda>_. Q\<rbrace>, \<lbrace>\<top>\<top>\<rbrace>"
+  by wpsimp
+
+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)
+
+lemma ifME_liftE:
+  "ifME (liftE test) a b = ifM test a b"
+  by (simp add: ifME_def ifM_def liftE_bindE)
+
+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'"
+  shows "\<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>"
+  unfolding valid_def using rl by safe
+
+lemma opt_return_pres_lift:
+  assumes x: "\<And>v. \<lbrace>P\<rbrace> f v \<lbrace>\<lambda>rv. P\<rbrace>"
+  shows      "\<lbrace>P\<rbrace> case x of None \<Rightarrow> return () | Some v \<Rightarrow> f v \<lbrace>\<lambda>rv. P\<rbrace>"
+  by (wpsimp wp: x)
+
+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)
+
+lemma static_imp_conj_wp:
+  "\<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>"
+  apply (rule hoare_vcg_conj_lift)
+   apply (rule static_imp_wp)
+   apply assumption+
+  done
+
+lemma hoare_eq_P:
+  assumes "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
+  shows "\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>"
+  by (rule assms)
+
+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>,-"
+  shows      "\<lbrace>\<lambda>s. P s \<or> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<or> Q' rv s\<rbrace>,-"
+  using assms
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
+
+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>"
+  by (cases ep, simp_all add: hoare_vcg_prop)
+
+lemma P_bool_lift:
+  assumes t: "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>"
+  assumes f: "\<lbrace>\<lambda>s. \<not>Q s\<rbrace> f \<lbrace>\<lambda>r s. \<not>Q s\<rbrace>"
+  shows "\<lbrace>\<lambda>s. P (Q s)\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (subgoal_tac "Q b = Q s")
+   apply simp
+  apply (rule iffI)
+   apply (rule classical)
+   apply (drule (1) use_valid [OF _ f])
+   apply simp
+  apply (erule (1) use_valid [OF _ t])
+  done
+
+lemmas fail_inv = hoare_fail_any[where Q="\<lambda>_. P" and P=P for P]
+
+lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda>s. f s = rv)\<rbrace>"
+  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'"
+  by (rule post_by_hoare, assumption+)
+
+lemma hoare_Ball_helper:
+  assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>"
+  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
+  shows "\<lbrace>\<lambda>s. \<forall>x \<in> S s. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S s. Q x rv s\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (subgoal_tac "S b = S s")
+   apply (erule post_by_hoare2 [OF x])
+   apply (clarsimp simp: Ball_def)
+  apply (erule_tac P1="\<lambda>x. x = S s" in post_by_hoare2 [OF y])
+  apply (rule refl)
+  done
+
+lemma handy_prop_divs:
+  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (Q s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s)\<rbrace>"
+             "\<And>P. \<lbrace>\<lambda>s. P (R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (R' rv s)\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. P (Q s \<and> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<and> R' rv s)\<rbrace>"
+             "\<lbrace>\<lambda>s. P (Q s \<or> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<or> R' rv s)\<rbrace>"
+   apply (clarsimp simp: valid_def
+                  elim!: subst[rotated, where P=P])
+   apply (rule use_valid [OF _ x(1)], assumption)
+   apply (rule use_valid [OF _ x(2)], assumption)
+   apply simp
+  apply (clarsimp simp: valid_def
+                 elim!: subst[rotated, where P=P])
+  apply (rule use_valid [OF _ x(1)], assumption)
+  apply (rule use_valid [OF _ x(2)], assumption)
+  apply simp
+  done
+
+lemma hoare_as_subst:
+  "\<lbrakk> \<And>P. \<lbrace>\<lambda>s. P (fn s)\<rbrace> f \<lbrace>\<lambda>rv s. P (fn s)\<rbrace>;
+     \<And>v :: 'a. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. P (fn s) s\<rbrace> f \<lbrace>\<lambda>rv s. Q (fn s) rv s\<rbrace>"
+  by (rule hoare_lift_Pf3)
+
+lemmas hoare_vcg_ball_lift = hoare_vcg_const_Ball_lift
+
+lemma hoare_set_preserved:
+  assumes x: "\<And>x. \<lbrace>fn' x\<rbrace> m \<lbrace>\<lambda>rv. fn x\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace>"
+  apply (induct xs)
+   apply simp
+   apply wp
+  apply simp
+  apply (rule hoare_vcg_conj_lift)
+   apply (rule x)
+  apply assumption
+  done
+
+lemma hoare_ex_pre: (* safe, unlike hoare_vcg_ex_lift *)
+  "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>"
+  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>"
+  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>
+   \<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 :
+  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>"
+  apply (clarsimp simp: valid_def)
+  apply (subgoal_tac "s = b", simp)
+  apply (simp add: state_unchanged [OF x])
+  done
+
+lemma list_case_throw_validE_R:
+  "\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow>
+   \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>,-"
+  apply (case_tac xs, simp_all)
+  apply wp
+  done
+
+lemma validE_R_sp:
+  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
+  assumes y: "\<And>x. \<lbrace>Q x\<rbrace> g x \<lbrace>R\<rbrace>,-"
+  shows "\<lbrace>P\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>R\<rbrace>,-"
+  by (rule hoare_pre, wp x y, simp)
+
+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>"
+  apply (erule hoare_strengthen_post)
+  apply (clarsimp dest!: in_set_takeD)
+  done
+
+lemma whenE_throwError_sp:
+  "\<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, -"
+  apply (simp add: whenE_def validE_R_def)
+  apply (intro conjI impI; wp)
+  done
+
+lemma weaker_hoare_ifE:
+  assumes x: "\<lbrace>P \<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  assumes y: "\<lbrace>P'\<rbrace> b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  shows      "\<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (rule hoare_vcg_precond_impE)
+   apply (wp x y)
+  apply simp
+  done
+
+lemma wp_split_const_if:
+  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>"
+  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_split_const_if_R:
+  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
+  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
+  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>"
+  apply safe
+   apply (rule hoare_pre_imp)
+    prefer 2
+    apply simp
+   apply simp
+  apply (rule hoare_pre_imp)
+   prefer 2
+   apply simp
+  apply simp
+  done
+
+lemma hoare_grab_asm:
+  "\<lbrakk> G \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. G \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>"
+  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>"
+  by (fastforce simp: valid_def)
+
+lemma hoare_grab_exs:
+  assumes x: "\<And>x. P x \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
+  shows      "\<lbrace>\<lambda>s. \<exists>x. P x \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>"
+  apply (clarsimp simp: valid_def)
+  apply (erule(2) use_valid [OF _ x])
+  done
+
+lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s. P\<rbrace>"
+  unfolding validE_E_def
+  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>,-"
+  apply (simp add: validE_R_def validE_def)
+  apply (drule(1) hoare_vcg_conj_lift)
+  apply (erule hoare_strengthen_post)
+  apply (clarsimp split: sum.splits)
+  done
+
+lemma hoare_walk_assmsE:
+  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" and y: "\<And>s. P s \<Longrightarrow> Q s" and z: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. Q\<rbrace>"
+  shows      "\<lbrace>P\<rbrace> doE x \<leftarrow> f; g odE \<lbrace>\<lambda>rv. Q\<rbrace>"
+  apply (wp z)
+   apply (simp add: validE_def)
+   apply (rule hoare_strengthen_post [OF x])
+   apply (auto simp: y split: sum.splits)
+  done
+
+lemma univ_wp:
+  "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> fst (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>"
+  apply (rule hoare_pre_imp [OF _ univ_wp])
+  apply clarsimp
+  apply (drule bspec, assumption, simp)
+  apply (subgoal_tac "s = b", simp)
+  apply (simp add: state_unchanged [OF x])
+  done
+
+lemma result_in_set_wp :
+  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>"
+  proof -
+  have P: "\<And>v s. (F v = v) \<and> (v, s) \<in> fst (fn s) \<Longrightarrow> (F v, s) \<in> fst (fn s)"
+    by simp
+  show ?thesis
+  apply (rule hoare_post_imp [OF P], assumption)
+  apply (rule hoare_pre_imp)
+  defer
+   apply (rule hoare_vcg_conj_lift)
+    apply (rule univ_get_wp [OF x])
+   apply (rule result_in_set_wp [OF x])
+  apply clarsimp
+  apply (drule bspec, assumption, simp)
+  done
+  qed
+
+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>"
+  by (auto simp add: valid_def split_def)
+
+lemma weak_if_wp':
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q r and Q' r\<rbrace> \<Longrightarrow>
+   \<lbrace>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 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>"
+  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 (erule allE, erule(1) impE)
+  apply (drule(1) bspec, simp)
+  apply (case_tac a, simp_all add: throwError_def return_def)
+  apply (drule x)
+  apply (clarsimp simp: validE_def valid_def)
+  apply (drule(1) bspec, simp)
+  done
+
+lemma validE_R_abstract_rv:
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
+  by (erule hoare_post_imp_R, simp)
+
+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>"
+  apply (simp add: validE_def)
+  apply (erule hoare_strengthen_post)
+  apply (simp split: sum.split_asm)
+  done
+
+lemma liftM_pre:
+  assumes rl: "\<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace> \<lambda>_ _. False \<rbrace>"
+  shows "\<lbrace>\<lambda>s. \<not> P s \<rbrace> liftM f a \<lbrace> \<lambda>_ _. False \<rbrace>"
+  unfolding liftM_def
+  apply (rule seq)
+  apply (rule rl)
+  apply wp
+  apply simp
+  done
+
+lemma hoare_gen_asm':
+  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace>"
+  apply (auto intro: hoare_assume_pre)
+  done
+
+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)
+
+lemma valid_imp_ex:
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. rv \<longrightarrow> Q rv s x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>x. Q rv s x)\<rbrace>"
+  by (fastforce simp: valid_def)
+
+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>"
+  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>"
+  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>"
+  apply (clarsimp simp: validE_def valid_def split: sum.splits)
+  apply (erule allE, erule (1) impE)+
+  apply (drule (1) bspec)+
+  apply clarsimp
+  done
+
+lemma valid_case_prod:
+  "\<lbrakk> \<And>x y. valid (P x y) (f x y) Q \<rbrakk> \<Longrightarrow> valid (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q"
+  by (simp add: split_def)
+
+lemma validE_case_prod:
+  "\<lbrakk> \<And>x y. validE (P x y) (f x y) Q E \<rbrakk> \<Longrightarrow> validE (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q E"
+  by (simp add: split_def)
+
+lemma valid_pre_satisfies_post:
+  "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>"
+  by (clarsimp simp: valid_def)
+
+lemma validE_pre_satisfies_post:
+  "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s'; \<And>s r' s'. P s \<Longrightarrow> R r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>"
+  by (clarsimp simp: validE_def2 split: sum.splits)
+
+lemma hoare_validE_R_conjI:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - ; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, - \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -"
+  apply (clarsimp simp: Ball_def validE_R_def validE_def valid_def)
+  by (case_tac a; fastforce)
+
+lemma hoare_validE_E_conjI:
+  "\<lbrakk> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> ; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace> \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
+  apply (clarsimp simp: Ball_def validE_E_def validE_def valid_def)
+  by (case_tac a; fastforce)
+
+lemma validE_R_post_conjD1:
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def valid_def)
+  by (case_tac a; fastforce)
+
+lemma validE_R_post_conjD2:
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def valid_def)
+  by (case_tac a; fastforce)
+
+lemma throw_opt_wp[wp]:
+  "\<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  unfolding throw_opt_def by wpsimp auto
+
+lemma hoare_name_pre_state2:
+  "(\<And>s. \<lbrace>P and ((=) s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+  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)
+
+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)
+
 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 dd47142aa..4265dd079 100644
--- a/lib/Monads/trace/Trace_No_Fail.thy
+++ b/lib/Monads/trace/Trace_No_Fail.thy
@@ -42,6 +42,11 @@ subsection \<open>Bundles\<close>
 
 bundle no_pre = hoare_pre [wp_pre del] no_fail_pre [wp_pre del]
 
+bundle classic_wp_pre =
+  hoare_pre [wp_pre del]
+  all_classic_wp_combs[wp_comb del]
+  all_classic_wp_combs[wp_comb]
+
 
 subsection \<open>Lemmas\<close>
 
@@ -135,8 +140,91 @@ lemma no_fail_bind[wp]:
   apply (fastforce simp: image_def)
   done
 
+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]:
+  "no_fail P (liftM f m) = no_fail P m"
+  by (auto simp: liftM_def no_fail_def bind_def return_def)
+
+lemma no_fail_liftM[wp]:
+  "no_fail P m \<Longrightarrow> no_fail P (liftM f m)"
+  by simp
+
+lemma no_fail_pre_and:
+  "no_fail P f \<Longrightarrow> no_fail (P and Q) f"
+  by (erule no_fail_pre) simp
+
+lemma no_fail_spec:
+  "\<lbrakk> \<And>s. no_fail (((=) s) and P) f \<rbrakk> \<Longrightarrow> no_fail P f"
+  by (simp add: no_fail_def)
+
+lemma no_fail_assertE[wp]:
+  "no_fail (\<lambda>_. P) (assertE P)"
+  by (simp add: assertE_def split: if_split)
+
+lemma no_fail_spec_pre:
+  "\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f"
+  by (erule no_fail_pre, simp)
+
+lemma no_fail_whenE[wp]:
+  "\<lbrakk> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. G \<longrightarrow> P s) (whenE G f)"
+  by (simp add: whenE_def split: if_split)
+
+lemma no_fail_unlessE[wp]:
+  "\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)"
+  by (simp add: unlessE_def split: if_split)
+
+lemma no_fail_throwError[wp]:
+  "no_fail \<top> (throwError e)"
+  by (simp add: throwError_def)
+
+lemma no_fail_liftE[wp]:
+  "no_fail P f \<Longrightarrow> no_fail P (liftE f)"
+  unfolding liftE_def by wpsimp
+
+lemma no_fail_gets_the[wp]:
+  "no_fail (\<lambda>s. f s \<noteq> None) (gets_the f)"
+  unfolding gets_the_def
+  by wpsimp
+
+lemma no_fail_lift:
+  "(\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not>isl x \<longrightarrow> P s) (lift f x)"
+  unfolding lift_def
+  by (wpsimp wp: no_fail_throwError split: sum.splits | assumption)+
+
+lemma validE_R_valid_eq:
+  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace>"
+  unfolding validE_R_def validE_def valid_def
+  by (fastforce split: sum.splits prod.split)
+
+lemma no_fail_bindE[wp]:
+  "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<rbrakk>
+     \<Longrightarrow> no_fail (P and Q) (f >>=E g)"
+  unfolding bindE_def
+  by (wpsimp wp: no_fail_lift simp: validE_R_valid_eq | assumption)+
+
+lemma no_fail_False[simp]:
+  "no_fail (\<lambda>_. False) X"
+  by (clarsimp simp: no_fail_def)
+
+lemma no_fail_gets_map[wp]:
+  "no_fail (\<lambda>s. f s p \<noteq> None) (gets_map f p)"
+  unfolding gets_map_def by wpsimp
+
 lemma no_fail_or:
   "\<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a"
   by (clarsimp simp: no_fail_def)
 
+lemma no_fail_state_assert[wp]:
+  "no_fail P (state_assert P)"
+  unfolding state_assert_def
+  by wpsimp
+
+lemma no_fail_condition:
+  "\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)"
+  unfolding condition_def no_fail_def
+  by clarsimp
+
 end
diff --git a/lib/Monads/trace/Trace_No_Throw.thy b/lib/Monads/trace/Trace_No_Throw.thy
index c98ac9659..90d667b71 100644
--- a/lib/Monads/trace/Trace_No_Throw.thy
+++ b/lib/Monads/trace/Trace_No_Throw.thy
@@ -25,4 +25,74 @@ definition no_throw :: "('s \<Rightarrow> bool) \<Rightarrow> ('s, 'e + 'a) tmon
 definition no_return :: "('a \<Rightarrow> bool) \<Rightarrow> ('a, 'b + 'c) tmonad \<Rightarrow> bool" where
   "no_return P A \<equiv> \<lbrace> P \<rbrace> A \<lbrace>\<lambda>_ _. False\<rbrace>,\<lbrace>\<lambda>_ _. True \<rbrace>"
 
+(* 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)))"
+  by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)
+
+
+lemma no_throw_returnOk[simp]:
+  "no_throw P (returnOk a)"
+  unfolding no_throw_def
+  by wp
+
+lemma no_throw_liftE[simp]:
+  "no_throw P (liftE x)"
+  by (wpsimp simp: liftE_def no_throw_def validE_def)
+
+lemma no_throw_bindE:
+  "\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk>
+   \<Longrightarrow> no_throw A (X >>=E Y)"
+  unfolding no_throw_def
+  using hoare_validE_cases seqE by blast
+
+lemma no_throw_bindE_simple:
+  "\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)"
+  using hoareE_TrueI no_throw_bindE by blast
+
+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)
+
+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)
+
+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)"
+  unfolding handleE_def
+  by (rule no_throw_handle2)
+
+lemma no_throw_fail[simp]:
+  "no_throw P fail"
+  by (clarsimp simp: no_throw_def)
+
+lemma handleE'_nothrow_lhs:
+  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle2> R)"
+  unfolding no_throw_def
+  using handleE'_wp[rotated] by fastforce
+
+lemma handleE'_nothrow_rhs:
+  "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)"
+  unfolding no_throw_def
+  by (metis hoareE_TrueI no_throw_def no_throw_handle2)
+
+lemma handleE_nothrow_lhs:
+  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle> R)"
+  by (metis handleE'_nothrow_lhs handleE_def)
+
+lemma handleE_nothrow_rhs:
+  "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)"
+  by (metis no_throw_handleE_simple)
+
+lemma condition_nothrow:
+  "\<lbrakk> no_throw \<top> L; no_throw \<top> R \<rbrakk> \<Longrightarrow> no_throw \<top> (condition C L R)"
+  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"
+  by (fastforce simp: no_throw_def' split: sum.splits)
+
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_Sat.thy b/lib/Monads/trace/Trace_Sat.thy
index 2f40ec7b7..20d68e584 100644
--- a/lib/Monads/trace/Trace_Sat.thy
+++ b/lib/Monads/trace/Trace_Sat.thy
@@ -26,6 +26,30 @@ definition ex_exs_validE ::
   ("\<lbrace>_\<rbrace> _ \<exists>\<lbrace>_\<rbrace>, \<lbrace>_\<rbrace>") where
   "\<lbrace>P\<rbrace> f \<exists>\<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<equiv> \<lbrace>P\<rbrace> f  \<exists>\<lbrace>\<lambda>rv. case rv of Inl e \<Rightarrow> E e | Inr v \<Rightarrow> Q v\<rbrace>"
 
+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 "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)"}.
+
+  See also "Predicate Calculus and Program Semantics" by E. W. Dijkstra and C. S. Scholten.\<close>
+experiment
+begin
+
+definition
+  "wp f Q \<equiv> \<lambda>s. fst (f s) \<subseteq> {(rv,s). Q rv s}"
+
+definition
+  "cwp f Q \<equiv> not (wp f (not Q))"
+
+lemma
+  "exs_valid P f Q = (\<forall>s. P s \<longrightarrow> cwp f Q s)"
+  unfolding exs_valid_def cwp_def wp_def by auto
+
+end
+
 
 subsection \<open>Set up for @{method wp}\<close>
 
@@ -76,9 +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>"
-  apply (clarsimp simp: exs_valid_def select_def mres_def)
-  apply (auto simp add: image_def)
-  done
+  by (clarsimp simp: exs_valid_def select_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)
 
 lemma exs_valid_get[wp]:
   "\<lbrace>\<lambda>s. Q s s\<rbrace> get \<exists>\<lbrace> Q \<rbrace>"
@@ -97,10 +123,15 @@ lemma exs_valid_fail[wp]:
   unfolding fail_def exs_valid_def
   by simp
 
+lemma exs_valid_assert[wp]:
+  "\<lbrace>\<lambda>s. Q () s \<and> G\<rbrace> assert G \<exists>\<lbrace>Q\<rbrace>"
+  unfolding assert_def
+  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>"
-  by (clarsimp simp: state_assert_def exs_valid_def get_def
-           assert_def bind_def2 return_def mres_def)
+  unfolding state_assert_def
+  by wp
 
 lemmas exs_valid_guard = exs_valid_state_assert
 
@@ -108,4 +139,16 @@ lemma exs_valid_condition[wp]:
   "\<lbrakk> \<lbrace>P\<rbrace> l \<exists>\<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> r \<exists>\<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (C s \<and> P s) \<or> (\<not> C s \<and> P' s)\<rbrace> condition C l r \<exists>\<lbrace>Q\<rbrace>"
   by (clarsimp simp: condition_def exs_valid_def split: sum.splits)
 
+lemma gets_exs_valid:
+  "\<lbrace>(=) s\<rbrace> gets f \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
+  by (rule exs_valid_gets)
+
+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)
+
+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>"
+  by (wpsimp simp: gets_the_def)
+
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_Strengthen_Setup.thy b/lib/Monads/trace/Trace_Strengthen_Setup.thy
index 024d370f8..c4b652fa0 100644
--- a/lib/Monads/trace/Trace_Strengthen_Setup.thy
+++ b/lib/Monads/trace/Trace_Strengthen_Setup.thy
@@ -41,6 +41,46 @@ lemma strengthen_validI[strg]:
    \<Longrightarrow> st F (\<longrightarrow>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q\<rbrace>) (\<lbrace>P\<rbrace>,\<lbrace>G\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>Q'\<rbrace>)"
   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>)"
+  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>, -)"
+  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>)"
+  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>)"
+  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)"
+  by (cases F, auto elim: no_fail_pre)
+
+lemmas nondet_wpfix_strgs =
+    wpfix_strengthen_validE_R_cong
+    wpfix_strengthen_validE_E_cong
+    wpfix_strengthen_validE_cong
+    wpfix_strengthen_hoare
+    wpfix_no_fail_cong
+
 end
 
+lemmas nondet_wpfix_strgs[wp_fix_strgs]
+    = strengthen_implementation.nondet_wpfix_strgs
+
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_Total.thy b/lib/Monads/trace/Trace_Total.thy
index 97c804807..7c89f267f 100644
--- a/lib/Monads/trace/Trace_Total.thy
+++ b/lib/Monads/trace/Trace_Total.thy
@@ -49,17 +49,40 @@ wpc_setup "\<lambda>m. \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>!" wpc_helper_va
 
 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)
+
+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)
+
+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>!"
+  by (fastforce simp: validNF_def valid_def no_fail_def)
+
+lemma validNF_conjD2:
+  "\<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 (fastforce simp: validNF_def valid_def no_fail_def)
+
 lemma validNF[intro?]: (* FIXME lib: should be validNFI *)
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!"
   by (clarsimp simp: validNF_def)
 
+lemma validNFE:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; \<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
+  by (clarsimp simp: validNF_def)
+
 lemma validNF_valid:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
-  by (clarsimp simp: validNF_def)
+  by (erule validNFE)
 
 lemma validNF_no_fail:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
-  by (clarsimp simp: validNF_def)
+  by (erule validNFE)
 
 lemma snd_validNF:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>!; P s \<rbrakk> \<Longrightarrow> Failed \<notin> snd ` (f s)"
@@ -163,60 +186,45 @@ subsection "validNF compound rules"
 
 lemma validNF_state_assert[wp]:
   "\<lbrace> \<lambda>s. P () s \<and> G s  \<rbrace> state_assert G \<lbrace> P \<rbrace>!"
-  apply (rule validNF)
-  apply wpsimp
-  apply (clarsimp simp: no_fail_def state_assert_def
-              bind_def2 assert_def return_def get_def)
-  done
+  by (rule validNF; wpsimp)
 
 lemma validNF_modify[wp]:
   "\<lbrace> \<lambda>s. P () (f s) \<rbrace> modify f \<lbrace> P \<rbrace>!"
-  apply (clarsimp simp: modify_def)
-  apply wp
-  done
+  by (rule validNF; wpsimp)
 
 lemma validNF_gets[wp]:
   "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>!"
-  apply (clarsimp simp: gets_def)
-  apply wp
-  done
+  by (rule validNF; wpsimp)
 
 lemma validNF_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>!"
-  apply rule
-   apply (drule validNF_valid)+
-   apply (erule (1) condition_wp)
-  apply (drule validNF_no_fail)+
-  apply (clarsimp simp: no_fail_def condition_def)
-  done
+  by (erule validNFE)+
+     (rule validNF; wpsimp wp: no_fail_condition)
 
 lemma validNF_assert[wp]:
-    "\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
-  apply (rule validNF)
-   apply (clarsimp simp: valid_def in_return)
-  apply (clarsimp simp: no_fail_def return_def)
-  done
+  "\<lbrace> (\<lambda>s. P) and (R ()) \<rbrace> assert P \<lbrace> R \<rbrace>!"
+  by (rule validNF; wpsimp)
 
 lemma validNF_false_pre:
   "\<lbrace> \<lambda>_. False \<rbrace> P \<lbrace> Q \<rbrace>!"
-  by (clarsimp simp: validNF_def no_fail_def)
+  by (rule validNF; wpsimp)
 
 lemma validNF_chain:
    "\<lbrakk>\<lbrace>P'\<rbrace> a \<lbrace>R'\<rbrace>!; \<And>s. P s \<Longrightarrow> P' s; \<And>r s. R' r s \<Longrightarrow> R r s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>!"
   by (fastforce simp: validNF_def valid_def no_fail_def Ball_def)
 
 lemma validNF_case_prod[wp]:
-  "\<lbrakk> \<And>x y. validNF (P x y) (B x y) Q \<rbrakk> \<Longrightarrow> validNF (case_prod P v) (case_prod (\<lambda>x y. B x y) v) Q"
+  "\<lbrakk>\<And>x y. \<lbrace>P x y\<rbrace> B x y \<lbrace>Q\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>case v of (x, y) \<Rightarrow> P x y\<rbrace> case v of (x, y) \<Rightarrow> B x y \<lbrace>Q\<rbrace>!"
   by (metis prod.exhaust split_conv)
 
 lemma validE_NF_case_prod[wp]:
-    "\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
-          \<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
-  apply (clarsimp simp: validE_NF_alt_def)
-  apply (erule validNF_case_prod)
-  done
+  "\<lbrakk> \<And>a b. \<lbrace>P a b\<rbrace> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow>
+   \<lbrace>case x of (a, b) \<Rightarrow> P a b\<rbrace> case x of (a, b) \<Rightarrow> f a b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!"
+  unfolding validE_NF_alt_def
+  by (erule validNF_case_prod)
 
-lemma no_fail_is_validNF_True: "no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)"
+lemma no_fail_is_validNF_True:
+  "no_fail P s = (\<lbrace> P \<rbrace> s \<lbrace> \<lambda>_ _. True \<rbrace>!)"
   by (clarsimp simp: no_fail_def validNF_def valid_def)
 
 
@@ -226,13 +234,17 @@ lemma validE_NF[intro?]:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!"
   by (clarsimp simp: validE_NF_def)
 
+lemma validE_NFE:
+  "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>!; \<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R"
+  by (clarsimp simp: validE_NF_def)
+
 lemma validE_NF_valid:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>"
-  by (clarsimp simp: validE_NF_def)
+  by (rule validE_NFE)
 
 lemma validE_NF_no_fail:
   "\<lbrakk> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>! \<rbrakk> \<Longrightarrow> no_fail P f"
-  by (clarsimp simp: validE_NF_def)
+  by (rule validE_NFE)
 
 lemma validE_NF_weaken_pre[wp_pre]:
   "\<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>!"
@@ -263,21 +275,13 @@ lemma validE_NF_chain:
 
 lemma validE_NF_bind_wp[wp]:
   "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>!"
-  apply (unfold validE_NF_alt_def bindE_def)
-  apply (rule validNF_bind [rotated])
-   apply assumption
-  apply (clarsimp simp: lift_def throwError_def split: sum.splits)
-    apply wpsimp
-  done
+  by (blast intro: validE_NF hoare_vcg_seqE no_fail_pre no_fail_bindE validE_validE_R validE_weaken
+            elim!: validE_NFE)
 
 lemma validNF_catch[wp]:
   "\<lbrakk>\<And>x. \<lbrace>E x\<rbrace> handler x \<lbrace>Q\<rbrace>!; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>!\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f <catch> (\<lambda>x. handler x) \<lbrace>Q\<rbrace>!"
-  apply (unfold validE_NF_alt_def catch_def)
-  apply (rule validNF_bind [rotated])
-   apply assumption
-  apply (clarsimp simp: lift_def throwError_def split: sum.splits)
-  apply wp
-  done
+  unfolding validE_NF_alt_def catch_def lift_def throwError_def
+  by (clarsimp simp: validNF_return split: sum.splits elim!: validNF_bind[rotated])
 
 lemma validNF_throwError[wp]:
   "\<lbrace>E e\<rbrace> throwError e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
@@ -285,15 +289,15 @@ lemma validNF_throwError[wp]:
 
 lemma validNF_returnOk[wp]:
   "\<lbrace>P e\<rbrace> returnOk e \<lbrace>P\<rbrace>, \<lbrace>E\<rbrace>!"
- by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp
+  by (clarsimp simp: validE_NF_alt_def returnOk_def) wpsimp
 
 lemma validNF_whenE[wp]:
   "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>!"
-  unfolding whenE_def by clarsimp wp
+  unfolding whenE_def by wpsimp
 
 lemma validNF_nobindE[wp]:
   "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>r s. B s\<rbrace>,\<lbrace>E\<rbrace>! \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>!"
-  by clarsimp wp
+  by wpsimp
 
 text \<open>
   Set up triple rules for @{term validE_NF} so that we can use @{method wp} combinator rules.\<close>
@@ -336,11 +340,10 @@ lemma validE_NF_handleE[wp]:
 lemma validE_NF_condition[wp]:
   "\<lbrakk> \<lbrace> Q \<rbrace> A \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!; \<lbrace> R \<rbrace> B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!\<rbrakk> \<Longrightarrow>
    \<lbrace>\<lambda>s. if C s then Q s else R s\<rbrace> condition C A B \<lbrace>P\<rbrace>,\<lbrace> E \<rbrace>!"
-  apply rule
-   apply (drule validE_NF_valid)+
-   apply wp
-  apply (drule validE_NF_no_fail)+
-  apply (clarsimp simp: no_fail_def condition_def)
-  done
+  by (erule validE_NFE)+ (wpsimp wp: no_fail_condition validE_NF)
+
+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)
 
 end
\ No newline at end of file
diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
index c20265ebd..f950d1b6e 100644
--- a/lib/Monads/trace/Trace_VCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -71,6 +71,18 @@ definition validE_E :: (* FIXME lib: this should be an abbreviation *)
   "('s \<Rightarrow> bool) \<Rightarrow>  ('s, 'e + 'a) tmonad \<Rightarrow> ('e \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" ("\<lbrace>_\<rbrace>/ _ /-, \<lbrace>_\<rbrace>") where
   "\<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace> \<equiv> validE P f (\<lambda>x y. True) Q"
 
+(* These lemmas are useful to apply to rules to convert valid rules into a format suitable for wp. *)
+lemma valid_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 split: prod.splits)
+
+lemma validE_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_def valid_def split: prod.splits sum.splits)
+
 
 section \<open>Lemmas\<close>
 
@@ -166,7 +178,9 @@ lemma seq_ext':
    \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>"
   by (metis bind_wp)
 
-lemmas seq_ext = bind_wp[rotated]
+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)
 
 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>
@@ -305,6 +319,12 @@ lemma use_valid:
 
 lemmas post_by_hoare = use_valid[rotated]
 
+lemma use_valid_inv:
+  assumes step: "(r, s') \<in> fst (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
+
 lemma use_validE_norm:
   "\<lbrakk> (Inr r', s') \<in> mres (B s); \<lbrace>P\<rbrace> B \<lbrace>Q\<rbrace>,\<lbrace> E \<rbrace>; P s \<rbrakk> \<Longrightarrow> Q r' s'"
   unfolding validE_def valid_def by force
@@ -328,6 +348,22 @@ lemma hoare_gen_asm:
   "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and K P\<rbrace> f \<lbrace>Q\<rbrace>"
   by (fastforce simp add: valid_def)
 
+lemmas hoare_gen_asm_single = hoare_gen_asm[where P'="\<top>", simplified pred_conj_def simp_thms]
+
+lemma hoare_gen_asm_lk:
+  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>K P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
+  by (fastforce simp add: valid_def)
+
+\<comment> \<open>Useful for forward reasoning, when P is known.
+    The first version allows weakening the precondition.\<close>
+lemma hoare_gen_asm_spec':
+  "\<lbrakk> \<And>s. P s \<Longrightarrow> S \<and> R s; S \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+  by (fastforce simp: valid_def)
+
+lemma hoare_gen_asm_spec:
+  "\<lbrakk> \<And>s. P s \<Longrightarrow> S; S \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
+  by (rule hoare_gen_asm_spec'[where S=S and R=P]) simp
+
 lemma hoare_conjI:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>"
   unfolding valid_def by blast
@@ -374,10 +410,24 @@ lemma hoare_case_option_wp:
   \<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_case_option_wp2:
+  "\<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 s. case v of None \<Rightarrow> Q rv s | Some x \<Rightarrow> Q' x rv s\<rbrace>"
+  by (cases v) auto
+
+(* 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)
+
 lemma hoare_vcg_prop:
   "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. P\<rbrace>"
   by (simp add: valid_def)
 
+lemma validE_eq_valid:
+  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>,\<lbrace>\<lambda>rv. Q\<rbrace> = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q\<rbrace>"
+  by (simp add: validE_def)
+
 
 subsection \<open>@{const valid} and @{const validE}, @{const validE_R}, @{const validE_E}\<close>
 
@@ -489,7 +539,7 @@ lemma hoare_seq_ext_nobindE:
   "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> doE f; g odE \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
   by (erule seqE) (clarsimp simp: validE_def)
 
-lemmas hoare_seq_ext_skip' = hoare_seq_ext[where Q'=Q and Q=Q for Q]
+lemmas hoare_seq_ext_skip' = hoare_seq_ext[where B=C and C=C for C]
 
 lemma hoare_chain:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<And>s. R s \<Longrightarrow> P s; \<And>rv s. Q rv s \<Longrightarrow> S rv s \<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>S\<rbrace>"
@@ -507,6 +557,9 @@ lemma hoare_vcg_conj_lift:
   unfolding valid_def
   by fastforce
 
+\<comment> \<open>A variant which works nicely with subgoals that do not contain schematics\<close>
+lemmas hoare_vcg_conj_lift_pre_fix = hoare_vcg_conj_lift[where P=R and P'=R for R, simplified]
+
 lemma hoare_vcg_conj_liftE1:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E\<rbrace>"
   unfolding valid_def validE_R_def validE_def
@@ -535,6 +588,30 @@ lemma hoare_vcg_all_lift_R:
   "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>, -"
   by (rule hoare_vcg_const_Ball_lift_R[where S=UNIV, simplified])
 
+lemma hoare_vcg_imp_lift:
+  "\<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 (simp only: imp_conv_disj) (rule hoare_vcg_disj_lift)
+
+lemma hoare_vcg_imp_lift':
+  "\<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. \<not> P' s \<longrightarrow> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
+  by (wpsimp wp: hoare_vcg_imp_lift)
+
+lemma hoare_vcg_imp_conj_lift[wp_comb]:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> Q' rv s\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
+  by (auto simp: valid_def)
+
+lemmas hoare_vcg_imp_conj_lift'[wp_unsafe] = hoare_vcg_imp_conj_lift[where Q'''="\<top>\<top>", simplified]
+
+lemma hoare_absorb_imp:
+  "\<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> R rv s\<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
+  by (erule hoare_post_imp[rotated], blast)
+
+lemma hoare_weaken_imp:
+  "\<lbrakk> \<And>rv s. Q rv s \<Longrightarrow> Q' rv s ;  \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> R rv s\<rbrace> \<rbrakk>
+    \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<longrightarrow> R rv s\<rbrace>"
+  by (clarsimp simp: valid_def split_def)
+
 lemma hoare_vcg_const_imp_lift:
   "\<lbrakk> P \<Longrightarrow> \<lbrace>Q\<rbrace> m \<lbrace>R\<rbrace> \<rbrakk> \<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: hoare_vcg_prop)
@@ -547,6 +624,8 @@ 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)
 
+lemmas hoare_vcg_weaken_imp = hoare_weaken_imp  (* FIXME lib: eliminate *)
+
 lemma hoare_vcg_ex_lift:
   "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>"
   by (clarsimp simp: valid_def, blast)
@@ -555,6 +634,17 @@ lemma hoare_vcg_ex_lift_R1:
   "(\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>, -"
   by (fastforce simp: valid_def validE_R_def validE_def split: sum.splits)
 
+lemma hoare_liftP_ext:
+  assumes "\<And>P x. m \<lbrace>\<lambda>s. P (f s x)\<rbrace>"
+  shows "m \<lbrace>\<lambda>s. P (f s)\<rbrace>"
+  unfolding valid_def
+  apply clarsimp
+  apply (erule subst[rotated, where P=P])
+  apply (rule ext)
+  apply (drule use_valid, rule assms, rule refl)
+  apply simp
+  done
+
 (* for instantiations *)
 lemma hoare_triv:    "\<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>f\<lbrace>Q\<rbrace>" .
 lemma hoare_trivE:   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" .
@@ -575,11 +665,48 @@ lemma hoare_vcg_R_conj:
   unfolding validE_R_def validE_def
   by (rule hoare_post_imp[OF _ hoare_vcg_conj_lift]; simp split: sum.splits)
 
+lemma hoare_lift_Pf_E_R:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m \<lbrace>\<lambda>_. P x\<rbrace>, -; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>, - \<rbrakk> \<Longrightarrow>
+   \<lbrace>\<lambda>s. P (f s) s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>, -"
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
+
+lemma hoare_lift_Pf_E_E:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> m -, \<lbrace>\<lambda>_. P x\<rbrace>; \<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s)\<rbrace> \<rbrakk> \<Longrightarrow>
+  \<lbrace>\<lambda>s. P (f s) s\<rbrace> m -, \<lbrace>\<lambda>_ s. P (f s) s\<rbrace>"
+  by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_const_Ball_lift_E_E:
+ "(\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P x\<rbrace> f -,\<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x \<in> S. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x \<in> S. Q x rv s\<rbrace>"
+  unfolding validE_E_def validE_def valid_def
+  by (fastforce split: sum.splits)
+
+lemma hoare_vcg_all_liftE_E:
+  "(\<And>x. \<lbrace>P x\<rbrace> f -, \<lbrace>Q x\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<forall>x. Q x rv s\<rbrace>"
+  by (rule hoare_vcg_const_Ball_lift_E_E[where S=UNIV, simplified])
+
+lemma hoare_vcg_imp_liftE_E:
+  "\<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. \<not> P' s \<longrightarrow> Q' s\<rbrace> f -, \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>"
+  by (auto simp add: valid_def validE_E_def validE_def split_def split: sum.splits)
+
+lemma hoare_vcg_ex_liftE:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. Q x rv s\<rbrace>,\<lbrace>E\<rbrace>"
+  by (fastforce simp: validE_def valid_def split: sum.splits)
+
+lemma hoare_vcg_ex_liftE_E:
+  "\<lbrakk> \<And>x. \<lbrace>P x\<rbrace> f -,\<lbrace>E x\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f -,\<lbrace>\<lambda>rv s. \<exists>x. E x rv s\<rbrace>"
+  by (fastforce simp: validE_E_def validE_def valid_def split: sum.splits)
+
 lemma hoare_post_imp_R:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
   unfolding validE_R_def
   by (erule hoare_post_impErr)
 
+lemma hoare_post_imp_E:
+  "\<lbrakk> \<lbrace>P\<rbrace> f -,\<lbrace>Q'\<rbrace>; \<And>rv s. Q' rv s \<Longrightarrow> Q rv s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>"
+  unfolding validE_E_def
+  by (rule hoare_post_impErr)
+
 lemma hoare_post_comb_imp_conj:
   "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>"
   by (wpsimp wp: hoare_vcg_conj_lift)
@@ -596,8 +723,8 @@ lemma return_wp:
   by(simp add: valid_def return_def mres_def)
 
 lemma get_wp:
-  "\<lbrace>\<lambda>s. Q s s\<rbrace> get \<lbrace>Q\<rbrace>"
-  by (simp add: get_def valid_def mres_def)
+  "\<lbrace>\<lambda>s. P s s\<rbrace> get \<lbrace>P\<rbrace>"
+  by(simp add: valid_def split_def get_def)
 
 lemma gets_wp:
   "\<lbrace>\<lambda>s. P (f s) s\<rbrace> gets f \<lbrace>P\<rbrace>"
@@ -740,10 +867,53 @@ lemma whenE_wp:
   "(P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then Q else R ()\<rbrace> whenE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>"
   unfolding whenE_def by clarsimp (wp returnOk_wp)
 
+lemma unlessE_wp:
+  "(\<not> P \<Longrightarrow> \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>if P then R () else Q\<rbrace> unlessE P f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>"
+  unfolding unlessE_def
+  by (wpsimp wp: returnOk_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)
+
+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)
+
+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)
+
+lemma andM_wp:
+  assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"
+  assumes [wp]: "\<lbrace>P\<rbrace> A \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>" "\<lbrace>P'\<rbrace> A \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> Q False s\<rbrace>"
+  shows "\<lbrace>P and P'\<rbrace> andM A B \<lbrace>Q\<rbrace>"
+  unfolding andM_def by (wp ifM_wp return_wp)
+
+lemma orM_wp:
+  assumes [wp]: "\<lbrace>Q'\<rbrace> B \<lbrace>Q\<rbrace>"
+  assumes [wp]: "\<lbrace>P\<rbrace> A \<lbrace>\<lambda>c s. c \<longrightarrow> Q True s\<rbrace>" "\<lbrace>P'\<rbrace> A \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> Q' s\<rbrace>"
+  shows "\<lbrace>P and P'\<rbrace> orM A B \<lbrace>Q\<rbrace>"
+  unfolding orM_def by (wp ifM_wp return_wp)
+
+lemma whenM_wp:
+  assumes [wp]: "\<lbrace>Q\<rbrace> f \<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> S () s\<rbrace>"
+  shows "\<lbrace>A and B\<rbrace> whenM P f \<lbrace>S\<rbrace>"
+  unfolding whenM_def by (wp ifM_wp return_wp)
+
 lemma hoare_K_bind[wp_split]:
   "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>"
   by simp
 
+lemma validE_K_bind[wp_split]:
+  "\<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>, \<lbrace> E \<rbrace> \<Longrightarrow> \<lbrace> P \<rbrace> K_bind x f \<lbrace> Q \<rbrace>, \<lbrace> E \<rbrace>"
+  by simp
+
 lemma hoare_fun_app_wp:
   "\<lbrace>P\<rbrace> f' x \<lbrace>Q'\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f' $ x \<lbrace>Q'\<rbrace>"
   "\<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
@@ -771,6 +941,31 @@ lemma case_option_wpE:
 
 lemmas liftME_E_E_wp[wp_split] = validE_validE_E [OF liftME_wp, simplified, OF validE_E_validE]
 
+lemma assert_opt_wp:
+  "\<lbrace>\<lambda>s. x \<noteq> None \<longrightarrow> Q (the x) s\<rbrace> assert_opt x \<lbrace>Q\<rbrace>"
+  unfolding assert_opt_def
+  by (case_tac x; wpsimp wp: fail_wp return_wp)
+
+lemma gets_the_wp:
+  "\<lbrace>\<lambda>s. (f s \<noteq> None) \<longrightarrow> Q (the (f s)) s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
+  unfolding gets_the_def
+  by (wp seq_ext gets_wp assert_opt_wp)
+
+lemma gets_the_wp': (* FIXME: should prefer this one in [wp] *)
+  "\<lbrace>\<lambda>s. \<forall>rv. f s = Some rv \<longrightarrow> Q rv s\<rbrace> gets_the f \<lbrace>Q\<rbrace>"
+  unfolding gets_the_def
+  by (wpsimp wp: seq_ext gets_wp assert_opt_wp)
+
+lemma gets_map_wp:
+  "\<lbrace>\<lambda>s. f s p \<noteq> None \<longrightarrow> Q (the (f s p)) s\<rbrace> gets_map f p \<lbrace>Q\<rbrace>"
+  unfolding gets_map_def
+  by (wpsimp wp: seq_ext gets_wp assert_opt_wp)
+
+lemma gets_map_wp':
+  "\<lbrace>\<lambda>s. \<forall>rv. f s p = Some rv \<longrightarrow> Q rv s\<rbrace> gets_map f p \<lbrace>Q\<rbrace>"
+  unfolding gets_map_def
+  by (wpsimp wp: seq_ext gets_wp assert_opt_wp)
+
 (* FIXME: make wp *)
 lemma whenE_throwError_wp:
   "\<lbrace>\<lambda>s. \<not>Q \<longrightarrow> P s\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv. P\<rbrace>, -"
@@ -864,6 +1059,9 @@ lemmas [wp] = hoare_vcg_prop
               failE_wp
               assert_wp
               state_assert_wp
+              assert_opt_wp
+              gets_the_wp
+              gets_map_wp'
               liftE_wp
               alternative_wp
               alternativeE_R_wp
@@ -873,6 +1071,7 @@ lemmas [wp] = hoare_vcg_prop
               state_select_wp
               condition_wp
               conditionE_wp
+              maybeM_wp notM_wp ifM_wp andM_wp orM_wp whenM_wp
 
 lemmas [wp_trip] = valid_is_triple validE_is_triple validE_E_is_triple validE_R_is_triple
 
@@ -965,8 +1164,20 @@ lemmas hoare_wp_pred_conj_elims =
   hoare_elim_pred_conjE2 hoare_elim_pred_conjE_R
 
 
+subsection \<open>Bundles\<close>
+
+bundle no_pre = hoare_pre [wp_pre del]
+
+bundle classic_wp_pre = hoare_pre [wp_pre del]
+    all_classic_wp_combs[wp_comb del] all_classic_wp_combs[wp_comb]
+
+
 text \<open>Miscellaneous lemmas on hoare triples\<close>
 
+lemma hoare_pre_cases:
+  "\<lbrakk> \<lbrace>\<lambda>s. R s \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. \<not>R s \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace>"
+  unfolding valid_def by fastforce
+
 lemma hoare_vcg_mp:
   "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<longrightarrow> Q' r s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>"
   by (auto simp: valid_def split_def)
@@ -988,6 +1199,12 @@ lemma hoare_list_case:
    \<lbrace>case xs of [] \<Rightarrow> P1 | y#ys \<Rightarrow> P2 y ys\<rbrace> f (case xs of [] \<Rightarrow> f1 | y#ys \<Rightarrow> f2 y ys) \<lbrace>Q\<rbrace>"
   by (cases xs; simp)
 
+lemmas whenE_wps[wp_split] =
+  whenE_wp whenE_wp[THEN validE_validE_R] whenE_wp[THEN validE_validE_E]
+
+lemmas unlessE_wps[wp_split] =
+  unlessE_wp unlessE_wp[THEN validE_validE_R] unlessE_wp[THEN validE_validE_E]
+
 lemma hoare_use_eq:
   assumes "\<And>P. \<lbrace>\<lambda>s. P (f s)\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
   assumes "\<And>f. \<lbrace>\<lambda>s. P f s\<rbrace> m \<lbrace>\<lambda>_ s. Q f s\<rbrace>"
@@ -1043,12 +1260,58 @@ lemma hoare_drop_impE_E:
 
 lemmas hoare_drop_imps = hoare_drop_imp hoare_drop_impE_R hoare_drop_impE_E
 
+(*This is unsafe, but can be very useful when supplied as a comb rule.*)
+lemma hoare_drop_imp_conj[wp_unsafe]:
+  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q'' rv s) \<and> Q''' rv s\<rbrace> \<rbrakk> \<Longrightarrow>
+   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>rv s. (Q rv s \<longrightarrow> Q' rv s \<and> Q'' rv s) \<and> Q''' rv s\<rbrace>"
+  by (auto simp: valid_def)
+
+lemmas hoare_drop_imp_conj'[wp_unsafe] = hoare_drop_imp_conj[where Q'''="\<top>\<top>", simplified]
+
 lemmas bindE_E_wp[wp_split] = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
 
 lemma True_E_E[wp]:
   "\<lbrace>\<top>\<rbrace> f -,\<lbrace>\<top>\<top>\<rbrace>"
   by (auto simp: validE_E_def validE_def valid_def split: sum.splits)
 
+lemma hoare_vcg_set_pred_lift:
+  assumes "\<And>P x. m \<lbrace> \<lambda>s. P (f x s) \<rbrace>"
+  shows "m \<lbrace> \<lambda>s. P {x. f x s} \<rbrace>"
+  using assms[where P="\<lambda>x . x"] assms[where P=Not] use_valid
+  by (fastforce simp: valid_def elim!: subst[rotated, where P=P])
+
+lemma hoare_vcg_set_pred_lift_mono:
+  assumes f: "\<And>x. m \<lbrace> f x \<rbrace>"
+  assumes mono: "\<And>A B. A \<subseteq> B \<Longrightarrow> P A \<Longrightarrow> P B"
+  shows "m \<lbrace> \<lambda>s. P {x. f x s} \<rbrace>"
+  by (fastforce simp: valid_def elim!: mono[rotated] dest: use_valid[OF _ f])
+
+text \<open>If a function contains an @{term assert}, or equivalent, then it might be
+      possible to strengthen the precondition of an already-proven hoare triple
+      @{text pos}, by additionally proving a side condition @{text neg}, that
+      violating some condition causes failure. The stronger hoare triple produced
+      by this theorem allows the precondition to assume that the condition is
+      satisfied.\<close>
+lemma hoare_strengthen_pre_via_assert_forward:
+  assumes pos: "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
+  assumes rel: "\<And>s. S s \<longrightarrow> P s \<or> N s"
+  assumes neg: "\<lbrace> N \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
+  shows "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
+  apply (rule hoare_weaken_pre)
+   apply (rule hoare_strengthen_post)
+    apply (rule hoare_vcg_disj_lift[OF pos neg])
+   by (auto simp: rel)
+
+text \<open>Like @{thm hoare_strengthen_pre_via_assert_forward}, strengthen a precondition
+      by proving a side condition that the negation of that condition would cause
+      failure. This version is intended for backward reasoning. Apply it to a goal to
+      obtain a stronger precondition after proving the side condition.\<close>
+lemma hoare_strengthen_pre_via_assert_backward:
+  assumes neg: "\<lbrace> Not \<circ> E \<rbrace> f \<lbrace> \<bottom>\<bottom> \<rbrace>"
+  assumes pos: "\<lbrace> P and E \<rbrace> f \<lbrace> Q \<rbrace>"
+  shows "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
+  by (rule hoare_strengthen_pre_via_assert_forward[OF pos _ neg], simp)
+
 
 subsection \<open>Strongest postcondition rules\<close>
 
@@ -1080,4 +1343,44 @@ lemma hoare_returnOk_sp:
   "\<lbrace>P\<rbrace> returnOk x \<lbrace>\<lambda>rv s. rv = x \<and> P s\<rbrace>, \<lbrace>Q\<rbrace>"
   by (simp add: valid_def validE_def returnOk_def return_def mres_def)
 
+\<comment> \<open>For forward reasoning in Hoare proofs, these lemmas allow us to step over the
+    left-hand-side of monadic bind, while keeping the same precondition.\<close>
+
+named_theorems forward_inv_step_rules
+
+lemmas hoare_forward_inv_step_nobind[forward_inv_step_rules] =
+  hoare_seq_ext_nobind[where B=A and A=A for A, rotated]
+
+lemmas hoare_seq_ext_skip[forward_inv_step_rules] =
+  hoare_seq_ext[where B="\<lambda>_. A" and A=A for A, rotated]
+
+lemmas hoare_forward_inv_step_nobindE_valid[forward_inv_step_rules] =
+  hoare_seq_ext_nobindE[where B=A and A=A and E="\<lambda>_. C" and C="\<lambda>_. C" for A C,
+                        simplified validE_eq_valid, rotated]
+
+lemmas hoare_forward_inv_step_valid[forward_inv_step_rules] =
+  hoare_vcg_seqE[where B="\<lambda>_. A" and A=A and E="\<lambda>_. C" and C="\<lambda>_. C" for A C,
+                 simplified validE_eq_valid, rotated]
+
+lemmas hoare_forward_inv_step_nobindE[forward_inv_step_rules] =
+  hoare_seq_ext_nobindE[where B=A and A=A for A, rotated]
+
+lemmas hoare_seq_ext_skipE[forward_inv_step_rules] =
+  hoare_vcg_seqE[where B="\<lambda>_. A" and A=A for A, rotated]
+
+lemmas hoare_forward_inv_step_nobindE_validE_E[forward_inv_step_rules] =
+  hoare_forward_inv_step_nobindE[where C="\<top>\<top>", simplified validE_E_def[symmetric]]
+
+lemmas hoare_forward_inv_step_validE_E[forward_inv_step_rules] =
+  hoare_seq_ext_skipE[where C="\<top>\<top>", simplified validE_E_def[symmetric]]
+
+lemmas hoare_forward_inv_step_nobindE_validE_R[forward_inv_step_rules] =
+  hoare_forward_inv_step_nobindE[where E="\<top>\<top>", simplified validE_R_def[symmetric]]
+
+lemmas hoare_forward_inv_step_validE_R[forward_inv_step_rules] =
+  hoare_seq_ext_skipE[where E="\<top>\<top>", simplified validE_R_def[symmetric]]
+
+method forward_inv_step uses wp simp =
+  rule forward_inv_step_rules, solves \<open>wpsimp wp: wp simp: simp\<close>
+
 end