diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy
index 93804f156c..5054ec5a40 100644
--- a/lib/Corres_UL.thy
+++ b/lib/Corres_UL.thy
@@ -481,6 +481,18 @@ lemma corres_if3:
                                     (if G then a else b) (if G' then c else d)"
   by simp
 
+lemma corres_if_strong:
+  "\<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; R s; R' s'\<rbrakk> \<Longrightarrow> G = G';
+    \<lbrakk>G; G'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' a c;
+    \<lbrakk>\<not> G; \<not> G'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r Q Q' b d \<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r
+         (R and (if G then P else Q)) (R' and (if G' then P' else Q'))
+         (if G then a else b) (if G' then c else d)"
+  by (fastforce simp: corres_underlying_def)
+
+lemmas corres_if_strong' =
+  corres_if_strong[where R=R and P=R and Q=R for R,
+                   where R'=R' and P'=R' and Q'=R' for R', simplified]
 
 text \<open>Some equivalences about liftM and other useful simps\<close>
 
@@ -740,6 +752,11 @@ lemma corres_assert_assume:
   by (auto simp: bind_def assert_def fail_def return_def
                  corres_underlying_def)
 
+lemma corres_assert_assume_l:
+  "corres_underlying sr nf nf' rrel P Q (f ()) g
+  \<Longrightarrow> corres_underlying sr nf nf' rrel (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
+  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
+
 lemma corres_assert_gen_asm_cross:
   "\<lbrakk> \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; Q' s'\<rbrakk> \<Longrightarrow> A;
      A \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy
index b92de195f0..0054e44ace 100644
--- a/lib/ExtraCorres.thy
+++ b/lib/ExtraCorres.thy
@@ -5,7 +5,7 @@
  *)
 
 theory ExtraCorres
-imports Corres_UL
+imports Corres_UL DetWPLib
 begin
 
 (* FIXME: the S in this rule is mainly to make the induction work, we don't actually need it in
@@ -181,12 +181,17 @@ qed
 
 text \<open>Some results concerning the interaction of abstract and concrete states\<close>
 
+definition ex_abs_underlying :: "('a \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
+  "ex_abs_underlying sr P s' \<equiv> \<exists>s. (s,s') \<in> sr \<and> P s"
+
+lemma ex_absI[intro!]:
+  "(s, s') \<in> sr \<Longrightarrow> P s \<Longrightarrow> ex_abs_underlying sr P s'"
+  by (auto simp add: ex_abs_underlying_def)
+
 lemma corres_u_nofail:
-  "corres_underlying S nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow>
-  no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> S \<and> P s \<and> P' s') g"
-  apply (clarsimp simp add: corres_underlying_def no_fail_def)
-  apply fastforce
-  done
+  "\<lbrakk>corres_underlying S nf True r P P' f g; nf \<Longrightarrow> no_fail P f\<rbrakk>
+   \<Longrightarrow> no_fail (P' and ex_abs_underlying S P) g"
+  by (fastforce simp: corres_underlying_def ex_abs_underlying_def no_fail_def)
 
 lemma wp_from_corres_u:
   "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
@@ -204,7 +209,7 @@ lemma wp_from_corres_u_unit:
 lemma corres_nofail:
   "corres_underlying state_relation nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow>
   no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> P' s') g"
-  by (rule corres_u_nofail)
+  by (fastforce intro: no_fail_pre corres_u_nofail simp: ex_abs_underlying_def)
 
 lemma wp_from_corres_unit:
   "\<lbrakk> corres_underlying state_relation nf nf' r G G' f f';
@@ -213,13 +218,6 @@ lemma wp_from_corres_unit:
   f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> state_relation \<and> Q s \<and> Q' s'\<rbrace>"
   by (auto intro!: wp_from_corres_u_unit)
 
-definition ex_abs_underlying :: "('a \<times> 'b) set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'b \<Rightarrow> bool" where
-  "ex_abs_underlying sr P s' \<equiv> \<exists>s. (s,s') \<in> sr \<and> P s"
-
-lemma ex_absI[intro!]:
-  "(s, s') \<in> sr \<Longrightarrow> P s \<Longrightarrow> ex_abs_underlying sr P s'"
-  by (auto simp add: ex_abs_underlying_def)
-
 lemma corres_underlying_split_ex_abs:
   assumes ac: "corres_underlying srel nf nf' r' G G' a c"
   assumes bd: "\<forall>rv rv'. r' rv rv' \<longrightarrow>
@@ -251,6 +249,100 @@ lemma hoare_from_abs_inv:
   using assms
   by (fastforce intro: hoare_from_abs[where R=\<top> and S=\<top> and R'=\<top> and Q="\<lambda>_. P" , simplified])
 
+lemma corres_from_valid:
+  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying srel P) f'"
+  assumes
+    "\<And>s. \<lbrace>\<lambda>s'. P s \<and> P' s' \<and> (s, s') \<in> srel\<rbrace>
+          f' \<lbrace>\<lambda>rv' t'. \<exists>(rv, t) \<in> fst (f s). (t, t') \<in> srel \<and> rrel rv rv'\<rbrace>"
+  shows "corres_underlying srel nf nf' rrel P P' f f'"
+  using assms
+  by (fastforce simp: corres_underlying_def valid_def no_fail_def)
+
+lemma corres_from_valid_det:
+  assumes det: "det_wp P f"
+  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying srel P) f'"
+  assumes valid:
+    "\<And>s rv t.
+      \<lbrakk>fst (f s) = {(rv, t)}; P s\<rbrakk>
+      \<Longrightarrow> \<lbrace>\<lambda>s'. P' s' \<and> (s, s') \<in> srel\<rbrace> f' \<lbrace>\<lambda>rv' t'. (t, t') \<in> srel \<and> rrel rv rv'\<rbrace>"
+  shows "corres_underlying srel nf nf' rrel P P' f f'"
+  apply (clarsimp simp: corres_underlying_def)
+  apply (intro conjI)
+   apply (insert det)
+   apply (clarsimp simp: det_wp_def)
+   apply (force dest: use_valid[OF _ valid])
+  apply (fastforce dest: nf' simp: no_fail_def ex_abs_underlying_def)
+  done
+
+lemma corres_noop_ex_abs:
+  assumes P: "\<And>s. P s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> f \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> r x rv\<rbrace>"
+  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying sr P) f"
+  shows "corres_underlying sr nf nf' r P P' (return x) f"
+  apply (simp add: corres_underlying_def return_def)
+  apply clarsimp
+  apply (frule P)
+  apply (insert nf')
+  apply (fastforce simp: valid_def no_fail_def ex_abs_underlying_def)
+  done
+
+lemma corres_symb_exec_r_conj_ex_abs:
+  assumes z: "\<And>rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)"
+  assumes y: "\<lbrace>Q'\<rbrace> m \<lbrace>R'\<rbrace>"
+  assumes x: "\<And>s. Q s \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> m \<lbrace>\<lambda>rv s'. (s, s') \<in> sr\<rbrace>"
+  assumes nf: "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying sr Q) m"
+  shows      "corres_underlying sr nf nf' r Q (P' and Q') x (m >>= (\<lambda>rv. y rv))"
+proof -
+  have P: "corres_underlying sr nf nf' dc Q P' (return undefined) m"
+    apply (rule corres_noop_ex_abs)
+     apply (simp add: x)
+    apply (erule nf)
+    done
+  show ?thesis
+    apply (rule corres_guard_imp)
+      apply (subst return_bind[symmetric], rule corres_split[OF P])
+        apply (rule z)
+       apply wp
+      apply (rule y)
+     apply simp+
+    done
+qed
+
+lemmas corres_symb_exec_r_conj_ex_abs_forwards =
+  corres_symb_exec_r_conj_ex_abs[where P'=P' and Q'=P' for P', simplified]
+
+lemma gets_the_corres_ex_abs':
+ "\<lbrakk>no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\<rbrakk> \<Longrightarrow>
+   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
+   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))"
+  by (fastforce simp: gets_the_def no_ofail_def corres_underlying_def split_def exec_gets
+                      assert_opt_def fail_def return_def ex_abs_underlying_def)
+
+lemmas gets_the_corres_ex_abs = gets_the_corres_ex_abs'[THEN iffD2]
+
+lemma gets_the_corres':
+ "\<lbrakk>no_ofail P a; no_ofail P' b\<rbrakk> \<Longrightarrow>
+   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
+   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))"
+  apply (erule gets_the_corres_ex_abs')
+  apply (fastforce intro: no_ofail_pre_imp)
+  done
+
+lemmas gets_the_corres = gets_the_corres'[THEN iffD2]
+
+lemma gets_the_corres_relation:
+ "\<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f');
+   P s; P' s'; (s, s') \<in> sr\<rbrakk>
+  \<Longrightarrow> r (the (f s)) (the (f' s'))"
+  apply (rule_tac P=P and a=f and b=f' and P'=P'
+               in gets_the_corres_ex_abs'[THEN iffD1, rule_format];
+         fastforce?)
+  apply (rule no_ofail_gets_the_eq[THEN iffD2])
+  apply (fastforce intro: corres_u_nofail)
+  done
+
+
+\<comment> \<open>Some @{term corres_underlying} rules for @{term whileLoop}\<close>
+
 lemma in_whileLoop_corres:
   assumes body_corres:
     "\<And>r r'. rrel r r' \<Longrightarrow>
@@ -422,6 +514,10 @@ lemma ifM_corres:
      apply (wpsimp wp: abs_valid conc_valid hoare_vcg_if_lift2)+
   done
 
+lemmas ifM_corres' =
+  ifM_corres[where A=A and B=A and C=A for A, simplified,
+             where A'=A' and B'=A' and C'=A' for A', simplified]
+
 lemma orM_corres:
   "\<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) R R' b b';
     \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R' s\<rbrace>\<rbrakk>
@@ -432,6 +528,9 @@ lemma orM_corres:
         apply (wpsimp | fastforce)+
   done
 
+lemmas orM_corres' =
+  orM_corres[where A=A and B=A for A, simplified, where A'=A' and B'=A' for A', simplified]
+
 lemma andM_corres:
   "\<lbrakk>corres_underlying srel nf nf' (=) A A' a a'; corres_underlying srel nf nf' (=) Q Q' b b';
     \<lbrace>B\<rbrace> a \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>; \<lbrace>B'\<rbrace> a' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>\<rbrakk>
@@ -451,4 +550,8 @@ lemma notM_corres:
       apply wpsimp+
   done
 
+lemma ifM_to_top_of_bind:
+  "((ifM test true false) >>= z) = ifM test (true >>= z) (false >>= z)"
+  by (force simp: ifM_def bind_def split: if_splits)
+
 end
diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy
new file mode 100644
index 0000000000..e8bae311db
--- /dev/null
+++ b/lib/Heap_List.thy
@@ -0,0 +1,479 @@
+(*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Singly-linked lists on heaps or projections from heaps, as predicate and as recursive function.
+   Loosely after ~~/src/HOL/Hoare/Pointer_Examples.thy *)
+
+theory Heap_List
+imports Main "HOL-Library.Prefix_Order" ListLibLemmas
+begin
+
+(* Given a heap projection that returns the next-pointer for an object at address x,
+   given a start pointer x, and an end pointer y, determine if the given list
+   is the path of addresses visited when following the next-pointers from x to y *)
+primrec heap_path :: "('a \<rightharpoonup> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> 'a option \<Rightarrow> bool" where
+  "heap_path hp x [] y     = (x = y)"
+| "heap_path hp x (a#as) y = (x = Some a \<and> heap_path hp (hp a) as y)"
+
+(* When a path ends in None, it is a singly-linked list *)
+abbreviation heap_ls :: "('a \<rightharpoonup> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> bool" where
+  "heap_ls hp x xs \<equiv> heap_path hp x xs None"
+
+(* Walk a linked list of next pointers, recording which it visited.
+   Terminates artificially at loops, and otherwise because the address domain is finite *)
+function heap_walk :: "('a::finite \<rightharpoonup> 'a) \<Rightarrow> 'a option \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+  "heap_walk hp None xs = xs"
+| "heap_walk hp (Some x) xs = (if x \<in> set xs then xs else heap_walk hp (hp x) (xs@[x]))"
+  by pat_completeness auto
+
+lemma card_set_UNIV:
+  fixes xs :: "'a::finite list"
+  assumes "x \<notin> set xs"
+  shows "card (set xs) < card(UNIV::'a set)"
+proof -
+  have "finite (UNIV::'a set)" by simp
+  moreover
+  from assms have "set xs \<subset> UNIV" by blast
+  ultimately
+  show ?thesis by (rule psubset_card_mono)
+qed
+
+termination heap_walk
+  by (relation "measure (\<lambda>(_, _, xs). card(UNIV :: 'a set) - card (set xs))";
+      simp add: card_set_UNIV diff_less_mono2)
+
+lemma heap_path_append[simp]:
+  "heap_path hp start (xs @ ys) end = (\<exists>x. heap_path hp start xs x \<and> heap_path hp x ys end)"
+  by (induct xs arbitrary: start; simp)
+
+lemma heap_path_None[simp]:
+  "heap_path hp None xs end = (xs = [] \<and> end = None)"
+  by (cases xs, auto)
+
+lemma heap_ls_unique:
+  "\<lbrakk> heap_ls hp x xs; heap_ls hp x ys \<rbrakk> \<Longrightarrow> xs = ys"
+  by (induct xs arbitrary: ys x; simp) (case_tac ys; clarsimp)
+
+lemma heap_ls_hd_not_in_tl:
+  "heap_ls hp (hp x) xs \<Longrightarrow> x \<notin> set xs"
+proof
+  assume "x \<in> set xs"
+  then obtain ys zs where xs: "xs = ys @ x # zs"  by (auto simp: in_set_conv_decomp)
+  moreover assume "heap_ls hp (hp x) xs"
+  moreover from this xs have "heap_ls hp (hp x) zs" by clarsimp
+  ultimately show False by (fastforce dest: heap_ls_unique)
+qed
+
+lemma heap_ls_distinct:
+  "heap_ls hp x xs \<Longrightarrow> distinct xs"
+  by (induct xs arbitrary: x; clarsimp simp: heap_ls_hd_not_in_tl)
+
+lemma heap_ls_is_walk':
+  "\<lbrakk> heap_ls hp x xs; set xs \<inter> set ys = {} \<rbrakk> \<Longrightarrow> heap_walk hp x ys = ys @ xs"
+  by (frule heap_ls_distinct) (induct xs arbitrary: x ys; clarsimp)
+
+lemma heap_ls_is_walk:
+  "heap_ls hp x xs \<Longrightarrow> heap_walk hp x [] = xs"
+  using heap_ls_is_walk' by fastforce
+
+lemma heap_path_end_unique:
+  "heap_path hp x xs y \<Longrightarrow> heap_path hp x xs y' \<Longrightarrow> y = y'"
+  by (induct xs arbitrary: x; clarsimp)
+
+lemma heap_path_head:
+  "heap_path hp x xs y \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> x = Some (hd xs)"
+  by (induct xs arbitrary: x; clarsimp)
+
+lemma heap_path_non_nil_lookup_next:
+  "heap_path hp x (xs@z#ys) y \<Longrightarrow> hp z = (case ys of [] \<Rightarrow> y | _ \<Rightarrow> Some (hd ys))"
+  by (cases ys; fastforce)
+
+lemma heap_path_prefix:
+  "heap_path hp st ls ed \<Longrightarrow> \<forall>xs\<le>ls. heap_path hp st xs (if xs = [] then st else hp (last xs))"
+  apply clarsimp
+  apply (erule Prefix_Order.prefixE)
+  by (metis append_butlast_last_id heap_path_append heap_path_non_nil_lookup_next list.case(1))
+
+lemma heap_path_butlast:
+  "heap_path hp st ls ed \<Longrightarrow> ls \<noteq> [] \<Longrightarrow> heap_path hp st (butlast ls) (Some (last ls))"
+  by (induct ls rule: rev_induct; simp)
+
+lemma in_list_decompose_takeWhile:
+  "x \<in> set xs \<Longrightarrow>
+   xs = (takeWhile ((\<noteq>) x) xs) @ x # (drop (length (takeWhile ((\<noteq>) x) xs) + 1) xs)"
+  by (induct xs arbitrary: x; clarsimp)
+
+lemma takeWhile_neq_hd_eq_Nil[simp]:
+  "takeWhile ((\<noteq>) (hd xs)) xs = Nil"
+  by (metis (full_types) hd_Cons_tl takeWhile.simps(1) takeWhile.simps(2))
+
+lemma heap_not_in_dom[simp]:
+  "ptr \<notin> dom hp \<Longrightarrow> hp(ptr := None) = hp"
+  by (auto simp: dom_def)
+
+lemma heap_path_takeWhile_lookup_next:
+  "\<lbrakk> heap_path hp st rs ed; r \<in> set rs \<rbrakk>
+   \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) r) rs) (Some r)"
+  apply (drule heap_path_prefix)
+  apply (subgoal_tac "takeWhile ((\<noteq>) r) rs @ [r] \<le> rs", fastforce)
+  by (fastforce dest!: in_list_decompose_takeWhile intro: Prefix_Order.prefixI)
+
+lemma heap_path_heap_upd_not_in:
+  "\<lbrakk>heap_path hp st rs ed; r \<notin> set rs\<rbrakk> \<Longrightarrow> heap_path (hp(r:= x)) st rs ed"
+  by (induct rs arbitrary: st; clarsimp)
+
+lemma heap_path_last_update:
+  "\<lbrakk>heap_path hp st xs end; xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> heap_path (hp(last xs := new)) st xs new"
+  by (induct xs arbitrary: st rule: rev_induct; simp add: heap_path_heap_upd_not_in)
+
+lemma heap_walk_lb:
+  "heap_walk hp x xs \<ge> xs"
+  apply (induct xs rule: heap_walk.induct; clarsimp)
+  by (metis Prefix_Order.prefixE Prefix_Order.prefixI append_assoc)
+
+lemma heal_walk_Some_nonempty':
+  "heap_walk hp (Some x) [] > []"
+  by (fastforce intro: heap_walk_lb less_le_trans[where y="[x]"])
+
+lemma heal_walk_Some_nonempty:
+  "heap_walk hp (Some x) [] \<noteq> []"
+  by (metis less_list_def heal_walk_Some_nonempty')
+
+lemma heap_walk_Nil_None:
+  "heap_walk hp st [] = [] \<Longrightarrow> st = None"
+   by (case_tac st; simp only: heal_walk_Some_nonempty)
+
+lemma heap_path_last_end:
+  "heap_path hp st xs end \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> hp (last xs) = end"
+  by (induct xs rule: rev_induct; clarsimp)
+
+lemmas heap_ls_last_None = heap_path_last_end[where ?end=None]
+
+(* sym_heap *)
+
+definition sym_heap where
+  "sym_heap hp hp' \<equiv> \<forall>p p'. hp p = Some p' \<longleftrightarrow> hp' p' = Some p"
+
+lemma sym_heapD1:
+  "sym_heap hp hp' \<Longrightarrow> hp p = Some p' \<Longrightarrow> hp' p' = Some p"
+  by (clarsimp simp: sym_heap_def)
+
+lemma sym_heapD2:
+  "sym_heap hp hp' \<Longrightarrow> hp' p' = Some p \<Longrightarrow> hp p = Some p'"
+  by (clarsimp simp: sym_heap_def)
+
+lemma sym_heap_symmetric:
+  "sym_heap hp hp' \<longleftrightarrow> sym_heap hp' hp"
+  unfolding sym_heap_def by blast
+
+lemma sym_heap_None:
+  "\<lbrakk>sym_heap hp hp'; hp p = None\<rbrakk> \<Longrightarrow> \<forall>p'. hp' p' \<noteq> Some p" unfolding sym_heap_def by force
+
+lemma sym_heap_remove_only:
+  "\<lbrakk>sym_heap hp hp'; hp' y = Some x\<rbrakk> \<Longrightarrow> sym_heap (hp(x := None)) (hp'(y := None))"
+  apply (clarsimp simp: sym_heap_def)
+  apply (metis option.inject)
+  done
+
+lemma sym_heap_remove_only':
+  "\<lbrakk>sym_heap hp hp'; hp y = Some x\<rbrakk> \<Longrightarrow> sym_heap (hp(y := None)) (hp'(x := None))"
+  apply (clarsimp simp: sym_heap_def)
+  apply (metis option.inject)
+  done
+
+lemma sym_heap_remove_middle_from_chain:
+  "\<lbrakk>sym_heap hp hp'; before \<noteq> middle; middle \<noteq> after;
+    hp before = Some middle; hp middle = Some after\<rbrakk>
+   \<Longrightarrow> sym_heap (hp(before := Some after, middle := None))
+                (hp'(after := Some before, middle := None))"
+  apply (clarsimp simp: sym_heap_def)
+  apply (metis option.simps(1))
+  done
+
+lemma sym_heap_connect:
+  "\<lbrakk>sym_heap hp hp'; hp a = None; hp' b = None \<rbrakk> \<Longrightarrow> sym_heap (hp(a \<mapsto> b)) (hp'(b \<mapsto> a))"
+  by (force simp: sym_heap_def)
+
+lemma sym_heap_insert_into_middle_of_chain:
+  "\<lbrakk>sym_heap hp hp'; hp before = Some after; hp middle = None; hp' middle = None\<rbrakk>
+   \<Longrightarrow> sym_heap (hp(before \<mapsto> middle, middle \<mapsto> after)) (hp'(after \<mapsto> middle, middle \<mapsto> before))"
+  apply (clarsimp simp: sym_heap_def)
+  apply (metis option.simps)
+  done
+
+lemma sym_heap_path_reverse:
+  "sym_heap hp hp' \<Longrightarrow>
+      heap_path hp (Some p) (p#ps) (Some p')
+          \<longleftrightarrow> heap_path hp' (Some p') (p'#(rev ps)) (Some p)"
+  unfolding sym_heap_def by (induct ps arbitrary: p p' rule: rev_induct; force)
+
+lemma sym_heap_ls_rev_Cons:
+  "\<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) (p#ps)\<rbrakk>
+  \<Longrightarrow> heap_path hp' (Some (last (p#ps))) (rev ps) (Some p)"
+  supply rev.simps[simp del]
+  apply (induct ps arbitrary: p rule: rev_induct; simp add: rev.simps)
+  by (auto dest!: sym_heap_path_reverse[THEN iffD1])
+
+lemma sym_heap_ls_rev:
+  "\<lbrakk>sym_heap hp hp'; heap_ls hp (Some p) ps\<rbrakk>
+  \<Longrightarrow> heap_path hp' (Some (last ps)) (butlast (rev ps)) (Some p)
+      \<and> hp (last ps) = None"
+  apply (induct ps arbitrary: p rule: rev_induct, simp)
+  apply (frule heap_path_head; clarsimp)
+  by (auto dest!: sym_heap_path_reverse[THEN iffD1])
+
+lemma heap_path_sym_heap_non_nil_lookup_prev:
+  "\<lbrakk>heap_ls hp x (xs @ z # ys); sym_heap hp hp'; xs \<noteq> []\<rbrakk> \<Longrightarrow> hp' z = (Some (last xs))"
+  supply heap_path_append[simp del]
+  apply (cut_tac xs="butlast xs" and z="last xs" and ys="z # ys"
+              in heap_path_non_nil_lookup_next[where hp=hp and x=x and y=None])
+   apply (frule append_butlast_last_id)
+   apply (metis append_eq_Cons_conv append_eq_append_conv2)
+  apply (fastforce dest: sym_heapD1)
+  done
+
+lemma heap_ls_no_loops:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs\<rbrakk> \<Longrightarrow> hp p \<noteq> Some p"
+  apply (frule heap_ls_distinct)
+  apply (fastforce dest: split_list heap_path_non_nil_lookup_next split: list.splits)
+  done
+
+lemma heap_ls_prev_no_loops:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; sym_heap hp hp'\<rbrakk> \<Longrightarrow> hp' p \<noteq> Some p"
+  by (fastforce dest: heap_ls_no_loops sym_heapD2)
+
+(* more on heap_path : next/prev in path *)
+
+lemma heap_path_extend:
+  "heap_path hp st (ls @ [p]) (hp p) \<longleftrightarrow> heap_path hp st ls (Some p)"
+  by (induct ls rule: rev_induct; simp)
+
+lemma heap_path_prefix_heap_ls:
+  "\<lbrakk>heap_ls hp st xs; heap_path hp st ys ed\<rbrakk> \<Longrightarrow> ys \<le> xs"
+  apply (induct xs arbitrary: ys st, simp)
+  apply (case_tac ys; clarsimp)
+  done
+
+lemma distinct_decompose2:
+  "\<lbrakk>distinct xs; xs = ys @ x # y # zs\<rbrakk>
+   \<Longrightarrow> x \<noteq> y \<and> x \<notin> set ys \<and> y \<notin> set ys \<and> x \<notin> set zs \<and> y \<notin> set zs"
+  by (simp add: in_set_conv_decomp)
+
+lemma heap_path_distinct_next_cases: (* the other direction needs sym_heap *)
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; p \<in> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> ed = Some p \<or> ed = Some np \<or> np \<in> set xs"
+  apply (cases ed; simp)
+   apply (frule in_list_decompose_takeWhile)
+   apply (subgoal_tac "heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)")
+   apply (drule heap_path_non_nil_lookup_next)
+   apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs"; simp)
+   apply (metis in_set_dropD list.set_intros(1))
+  apply simp
+  apply (frule in_list_decompose_takeWhile)
+  apply (subgoal_tac "heap_path hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs) ed")
+  apply (frule heap_path_non_nil_lookup_next)
+  apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs", simp)
+  apply (simp split: if_split_asm)
+  apply (drule (1) distinct_decompose2)
+  apply clarsimp
+  by (metis in_set_dropD list.set_intros(1)) simp
+
+lemma heap_ls_next_in_list:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> np \<in> set xs"
+   apply (subgoal_tac "distinct xs")
+   by (fastforce dest!: heap_path_distinct_next_cases) (erule heap_ls_distinct)
+
+lemma heap_path_distinct_sym_prev_cases:
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow> st = Some np \<or> p \<in> set xs"
+  apply (cases st; simp)
+  apply (rename_tac stp)
+  apply (case_tac "stp = np"; simp)
+  apply (cases xs; simp del: heap_path.simps)
+  apply (frule heap_path_head, simp)
+  apply (cases ed, clarsimp)
+   apply (frule sym_heap_ls_rev_Cons, fastforce)
+   apply (drule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def)
+   apply simp
+  apply (simp del: heap_path.simps)
+  apply (frule (1) sym_heap_path_reverse[where hp'=hp', THEN iffD1])
+  apply simp
+  apply (frule heap_path_distinct_next_cases[where hp=hp']; simp add: sym_heap_def)
+  apply fastforce
+  done
+
+lemma heap_ls_prev_cases:
+  "\<lbrakk>heap_ls hp st xs; np \<in> set xs; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow> st = Some np \<or> p \<in> set xs"
+   apply (subgoal_tac "distinct xs")
+   by (fastforce dest!: heap_path_distinct_sym_prev_cases) (erule heap_ls_distinct)
+
+lemma heap_ls_prev_not_in:
+  "\<lbrakk>heap_ls hp st xs; np \<notin> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> p \<notin> set xs"
+  by (meson heap_ls_next_in_list)
+
+lemma heap_path_distinct_prev_not_in:
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; np \<notin> set xs; hp p = Some np; ed \<noteq> Some np; ed \<noteq> Some p\<rbrakk>
+  \<Longrightarrow> p \<notin> set xs"
+  using heap_path_distinct_next_cases
+  by fastforce
+
+lemma heap_path_distinct_next_not_in:
+  "\<lbrakk>heap_path hp st xs ed; distinct xs; p \<notin> set xs; hp p = Some np;
+    sym_heap hp hp'; st \<noteq> Some np\<rbrakk>
+  \<Longrightarrow> np \<notin> set xs"
+  by (fastforce dest!: heap_path_distinct_sym_prev_cases[simplified])
+
+lemma heap_ls_next_not_in:
+  "\<lbrakk>heap_ls hp st xs; p \<notin> set xs; hp p = Some np; sym_heap hp hp'; st \<noteq> Some np\<rbrakk>
+  \<Longrightarrow> np \<notin> set xs"
+  by (fastforce dest!: heap_ls_prev_cases[simplified])
+
+lemma sym_heap_prev_None_is_start:
+  "\<lbrakk>heap_ls hp st xs; sym_heap hp hp'; p \<in> set xs; hp' p = None\<rbrakk>
+   \<Longrightarrow> Some p = st"
+  using split_list_last heap_path_sym_heap_non_nil_lookup_prev
+  by fastforce
+
+lemma not_last_next_not_None:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> last xs\<rbrakk> \<Longrightarrow> hp p \<noteq> None"
+  by (fastforce intro: heap_path_head dest: split_list)
+
+lemma not_head_prev_not_None:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; p \<noteq> hd xs; sym_heap hp hp'\<rbrakk>
+   \<Longrightarrow> hp' p \<noteq> None"
+  using sym_heap_prev_None_is_start heap_path_head
+  by fastforce
+
+(* more on heap_path *)
+
+lemma heap_ls_next_takeWhile_append:
+  "\<lbrakk>heap_ls hp st xs; p \<in> set xs; hp p = Some np\<rbrakk>
+  \<Longrightarrow> takeWhile ((\<noteq>) np) xs = (takeWhile ((\<noteq>) p) xs) @ [p]"
+  apply (frule heap_ls_distinct)
+  apply (frule in_list_decompose_takeWhile)
+  apply (subgoal_tac "heap_ls hp st (takeWhile ((\<noteq>) p) xs @ p # drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs)")
+   prefer 2 apply simp
+  apply (drule heap_path_non_nil_lookup_next)
+  apply (case_tac "drop (length (takeWhile ((\<noteq>) p) xs) + 1) xs"; simp)
+  apply (subgoal_tac "np \<in> set xs")
+   prefer 2 apply (erule (2) heap_ls_next_in_list)
+  apply (frule in_list_decompose_takeWhile[where x=np])
+  apply (drule (1) distinct_inj_middle[where x=np and xa="takeWhile ((\<noteq>) np) xs" and ya="takeWhile ((\<noteq>) p) xs @ [p]"])
+   apply simp+
+  done
+
+(* RT FIXME: Move *)
+lemma takeWhile_neq_notin_same:
+  "x \<notin> set xs \<Longrightarrow> takeWhile ((\<noteq>) x) xs = xs"
+  using takeWhile_eq_all_conv by blast
+
+lemma heap_path_extend_takeWhile:
+  "\<lbrakk>heap_ls hp st xs; heap_path hp st (takeWhile ((\<noteq>) p) xs) (Some p); hp p = Some np\<rbrakk>
+  \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) np) xs) (Some np)"
+  apply (case_tac "p \<in> set xs")
+  apply (subst heap_ls_next_takeWhile_append[where p=p and np=np and hp=hp]; simp)
+  apply (drule takeWhile_neq_notin_same, simp)
+  apply (drule (1) heap_path_end_unique, simp)
+  done
+
+lemma heap_ls_next_takeWhile_append_sym:
+  "\<lbrakk>heap_ls hp st xs; np \<in> set xs; st \<noteq> Some np; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow>takeWhile ((\<noteq>) np) xs = (takeWhile ((\<noteq>) p) xs) @ [p]"
+  apply (frule (3) heap_ls_prev_cases, simp)
+  apply (fastforce elim!: heap_ls_next_takeWhile_append)
+  done
+
+lemma heap_path_curtail_takeWhile:
+  "\<lbrakk>heap_ls hp st xs; heap_path hp st (takeWhile ((\<noteq>) np) xs) (Some np);
+    st \<noteq> Some np; hp p = Some np; sym_heap hp hp'\<rbrakk>
+  \<Longrightarrow> heap_path hp st (takeWhile ((\<noteq>) p) xs) (Some p)"
+  apply (case_tac "np \<in> set xs")
+   apply (drule (4) heap_ls_next_takeWhile_append_sym)
+   apply simp
+  apply (drule takeWhile_neq_notin_same, simp)
+  apply (drule (1) heap_path_end_unique, simp)
+  done
+
+(* more on heap_path : end *)
+
+
+\<comment> \<open>Lemmas relating an update to the list to an update to the heap\<close>
+
+lemma heap_ls_prepend:
+  "\<lbrakk>heap_ls hp st xs; new \<notin> set xs; xs \<noteq> []\<rbrakk>
+   \<Longrightarrow> heap_ls (hp(new := Some (hd xs))) (Some new) (new # xs)"
+  apply simp
+  apply (erule heap_path_heap_upd_not_in[rotated])
+  apply (frule (1) heap_path_head)
+  apply fastforce
+  done
+
+lemma heap_ls_append:
+  "\<lbrakk>heap_ls hp st xs; xs \<noteq> []; new \<notin> set xs\<rbrakk>
+   \<Longrightarrow> heap_ls (hp(last xs := Some new, new := None)) st (xs @ [new])"
+  apply (frule heap_ls_distinct)
+  apply simp
+  apply (rule heap_path_heap_upd_not_in)
+   apply (fastforce simp: heap_path_last_update)
+  apply assumption
+  done
+
+lemma heap_ls_list_insert_before:
+  "\<lbrakk>heap_ls hp st (xs @ ys); new \<notin> set (xs @ ys); xs \<noteq> []; ys \<noteq> []\<rbrakk>
+   \<Longrightarrow> heap_ls (hp(last xs := Some new, new := Some (hd ys))) st
+               (list_insert_before (xs @ ys) (hd ys) new)"
+  apply (frule heap_ls_distinct)
+  apply (subst list_insert_before_distinct; fastforce?)
+  apply simp
+  apply (rule conjI)
+   \<comment> \<open>the path until new\<close>
+   apply (fastforce intro: heap_path_heap_upd_not_in heap_path_last_update)
+  \<comment> \<open>the path from hd ys\<close>
+  apply (metis disjoint_iff_not_equal heap_path_head heap_path_heap_upd_not_in last_in_set)
+  done
+
+lemma heap_ls_remove_singleton:
+  "heap_ls hp st [x] \<Longrightarrow> heap_ls (hp(x := None)) None []"
+  by simp
+
+lemma heap_ls_remove_head_not_singleton:
+  "\<lbrakk>heap_ls hp st xs; tl xs \<noteq> []\<rbrakk>
+   \<Longrightarrow> heap_ls (hp(hd xs := None)) (Some (hd (tl xs))) (tl xs)"
+  apply (frule heap_ls_distinct)
+  apply (cases xs; simp)
+  apply clarsimp
+  apply (frule heap_path_head)
+   apply fastforce
+  apply (fastforce elim!: heap_path_heap_upd_not_in)
+  done
+
+lemma heap_ls_remove_last_not_singleton:
+  "\<lbrakk>heap_ls hp st xs; butlast xs \<noteq> []\<rbrakk>
+   \<Longrightarrow> heap_ls (hp((last (butlast xs)) := None)) st (butlast xs)"
+  apply (frule heap_ls_distinct)
+  apply (frule distinct_butlast)
+  apply (fastforce dest: heap_path_last_update heap_path_butlast)
+  done
+
+lemma heap_ls_remove_middle:
+  "\<lbrakk>heap_ls hp st (xs @ a # ys); xs \<noteq> []; ys \<noteq> []\<rbrakk>
+   \<Longrightarrow> heap_ls (hp(last xs := Some (hd ys), a := None)) st (xs @ ys)"
+  apply (frule heap_ls_distinct)
+  apply simp
+  apply (rule_tac x="Some (hd ys)" in exI)
+  apply (rule conjI)
+   apply (fastforce intro: heap_path_heap_upd_not_in heap_path_last_update)
+  apply (rule heap_path_heap_upd_not_in)
+   apply (rule heap_path_heap_upd_not_in)
+    using heap_path_head apply fastforce
+   apply force
+  apply fastforce
+  done
+
+end
\ No newline at end of file
diff --git a/lib/Lib.thy b/lib/Lib.thy
index 69c29df3f7a..1374020d11 100644
--- a/lib/Lib.thy
+++ b/lib/Lib.thy
@@ -2558,6 +2558,10 @@ lemma ranD:
   "v \<in> ran f \<Longrightarrow> \<exists>x. f x = Some v"
   by (auto simp: ran_def)
 
+lemma fun_upd_swap:
+  "a \<noteq> c \<Longrightarrow>  hp(c := d, a := b) = hp(a := b, c := d)"
+  by fastforce
+
 text \<open>Prevent clarsimp and others from creating Some from not None by folding this and unfolding
   again when safe.\<close>
 
diff --git a/lib/ListLibLemmas.thy b/lib/ListLibLemmas.thy
index bdb72d61f8..fdb3ba42cf 100644
--- a/lib/ListLibLemmas.thy
+++ b/lib/ListLibLemmas.thy
@@ -371,6 +371,32 @@ lemma list_insert_after_after:
   apply fastforce
   done
 
+lemma list_insert_before_not_found:
+  "a \<notin> set ls \<Longrightarrow> list_insert_before ls a new = ls"
+  by (induct ls; fastforce)
+
+lemma list_insert_before_nonempty:
+  "ls \<noteq> [] \<Longrightarrow> list_insert_before ls a new \<noteq> []"
+  by (induct ls; clarsimp)
+
+lemma list_insert_before_head:
+  "xs \<noteq> [] \<Longrightarrow> list_insert_before xs (hd xs) new = new # xs"
+   by (induct xs; fastforce)
+
+lemma last_of_list_insert_before:
+  "xs \<noteq> [] \<Longrightarrow> last (list_insert_before xs a new) = last xs"
+  by (induct xs; clarsimp simp: list_insert_before_nonempty)
+
+lemma list_insert_before_distinct:
+  "\<lbrakk>distinct (xs @ ys); ys \<noteq> []\<rbrakk> \<Longrightarrow> list_insert_before (xs @ ys) (hd ys) new = xs @ new # ys"
+  by (induct xs; fastforce simp add: list_insert_before_head)
+
+lemma set_list_insert_before:
+  "\<lbrakk>new \<notin> set ls; before \<in> set ls\<rbrakk> \<Longrightarrow> set (list_insert_before ls before new) = set ls \<union> {new}"
+  apply (induct ls; clarsimp)
+  apply fastforce
+  done
+
 lemma list_remove_removed:
   "set (list_remove list x) = (set list) - {x}"
   apply (induct list,simp+)
diff --git a/lib/List_Lib.thy b/lib/List_Lib.thy
index 936f86e6e6..e6471707cb 100644
--- a/lib/List_Lib.thy
+++ b/lib/List_Lib.thy
@@ -26,6 +26,12 @@ primrec list_insert_after :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Righta
   "list_insert_after (x # xs) a b = (if x = a then x # b # xs
                                      else x # list_insert_after xs a b)"
 
+\<comment> \<open>Inserts the value new immediately before the first occurence of a (if any) in the list\<close>
+primrec list_insert_before :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a list" where
+  "list_insert_before [] a new = []" |
+  "list_insert_before (x # xs) a new = (if x = a then new # x # xs
+                                        else x # list_insert_before xs a new)"
+
 primrec list_remove :: "'a list \<Rightarrow> 'a \<Rightarrow> 'a list" where
   "list_remove [] a = []" |
   "list_remove (x # xs) a = (if x = a then (list_remove xs a)
diff --git a/lib/MonadicRewrite.thy b/lib/MonadicRewrite.thy
index 3058fd921b..e4fbed6481 100644
--- a/lib/MonadicRewrite.thy
+++ b/lib/MonadicRewrite.thy
@@ -10,7 +10,7 @@
 theory MonadicRewrite
 imports
   Monads.Nondet_VCG
-  Corres_UL
+  ExtraCorres
   Monads.Nondet_Empty_Fail
   Rules_Tac
 begin
@@ -81,6 +81,10 @@ lemma monadic_rewrite_pre_imp_eq:
   "\<lbrakk> \<And>s. P s \<Longrightarrow> f s = g s \<rbrakk> \<Longrightarrow> monadic_rewrite F E P f g"
   by (simp add: monadic_rewrite_def)
 
+lemma monadic_rewrite_guard_arg_cong:
+  "(\<And>s. P s \<Longrightarrow> x = y) \<Longrightarrow> monadic_rewrite F E P (f x) (f y)"
+  by (clarsimp simp: monadic_rewrite_def)
+
 lemma monadic_rewrite_exists:
   "(\<And>v. monadic_rewrite F E (Q v) m m')
    \<Longrightarrow> monadic_rewrite F E ((\<lambda>s. \<forall>v. P v s \<longrightarrow> Q v s) and (\<lambda>s. \<exists>v. P v s)) m m'"
@@ -693,7 +697,7 @@ lemma monadic_rewrite_refine_validE_R:
   by (simp add: validE_R_def validE_def monadic_rewrite_refine_valid)
 
 lemma monadic_rewrite_is_valid:
-  "\<lbrakk> monadic_rewrite False False P' f f'; \<lbrace>P\<rbrace> do x <- f; g x od \<lbrace>Q\<rbrace> \<rbrakk>
+  "\<lbrakk> monadic_rewrite False E P' f f'; \<lbrace>P\<rbrace> do x <- f; g x od \<lbrace>Q\<rbrace> \<rbrakk>
    \<Longrightarrow> \<lbrace>P and P'\<rbrace> do x <- f'; g x od \<lbrace>Q\<rbrace>"
   by (fastforce simp: monadic_rewrite_def valid_def bind_def)
 
@@ -740,6 +744,13 @@ lemma monadic_rewrite_corres_r_generic:
    \<Longrightarrow> corres_underlying R nf nf' r P (P' and Q) a c"
   by (fastforce simp: corres_underlying_def monadic_rewrite_def)
 
+lemma monadic_rewrite_corres_r_generic_ex_abs:
+  "\<lbrakk> monadic_rewrite F E (\<lambda>s'. Q s' \<and> ex_abs_underlying sr P s') c' c;
+     corres_underlying sr nf nf'' r P P' a c';
+     F \<longrightarrow> nf''; nf' \<longrightarrow> nf'' \<rbrakk>
+   \<Longrightarrow> corres_underlying sr nf nf' r P (P' and Q) a c"
+  by (fastforce simp: corres_underlying_def monadic_rewrite_def)
+
 lemma monadic_rewrite_corres_r:
   "\<lbrakk> monadic_rewrite False True Q c c';
      corres_underlying R nf nf' r P P' a c' \<rbrakk>
diff --git a/lib/Monads/nondet/Nondet_No_Fail.thy b/lib/Monads/nondet/Nondet_No_Fail.thy
index 8bf7c5fd0b..6e30a191c2 100644
--- a/lib/Monads/nondet/Nondet_No_Fail.thy
+++ b/lib/Monads/nondet/Nondet_No_Fail.thy
@@ -130,7 +130,7 @@ lemma no_fail_returnOK[simp, wp]:
   by (simp add: returnOk_def)
 
 lemma no_fail_bind[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 >>= (\<lambda>rv. g rv))"
+  "\<lbrakk> \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>; no_fail P f \<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= (\<lambda>rv. g rv))"
   unfolding no_fail_def bind_def
   using post_by_hoare by fastforce
 
diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy
index f1b2d6960c..278d25a24f 100644
--- a/lib/Monads/reader_option/Reader_Option_VCG.thy
+++ b/lib/Monads/reader_option/Reader_Option_VCG.thy
@@ -59,6 +59,10 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric]
 
 
 (* WP rules for ovalid. *)
+lemma ovalid_post_taut[wp]:
+  "\<lblot>P\<rblot> f \<lblot>\<top>\<top>\<rblot>"
+  by (simp add: ovalid_def)
+
 lemma ovalid_inv[wp]:
   "ovalid P f (\<lambda>_. P)"
   by (simp add: ovalid_def)
@@ -247,7 +251,7 @@ lemma no_ofail_ogets[wp]:
   by simp
 
 lemma no_ofail_obind[wp]:
-  "\<lbrakk> \<And>r. no_ofail (P r) (g r); no_ofail Q f; ovalid Q f P \<rbrakk> \<Longrightarrow> no_ofail Q (obind f g)"
+  "\<lbrakk> \<And>r. no_ofail (R r) (g r); \<lblot>Q\<rblot> f \<lblot>R\<rblot>; no_ofail P f \<rbrakk> \<Longrightarrow> no_ofail (P and Q) (f |>> g)"
   by (auto simp: no_ofail_def obind_def ovalid_def)
 
 lemma no_ofail_K_bind[wp]:
@@ -275,6 +279,11 @@ lemma no_ofail_oassert_opt[simp, wp]:
   "no_ofail (\<lambda>_. P \<noteq> None) (oassert_opt P)"
   by (simp add: no_ofail_def oassert_opt_def split: option.splits)
 
+lemma no_ofail_if[wp]:
+  "\<lbrakk> P \<Longrightarrow> no_ofail Q f; \<not> P \<Longrightarrow> no_ofail R g \<rbrakk>
+   \<Longrightarrow> no_ofail (if P then Q else R) (if P then f else g)"
+  by simp
+
 lemma no_ofail_owhen[wp]:
   "(P \<Longrightarrow> no_ofail Q f) \<Longrightarrow> no_ofail (if P then Q else \<top>) (owhen P f)"
   by (simp add: no_ofail_def owhen_def)
@@ -287,11 +296,14 @@ lemma no_ofail_oassert[simp, wp]:
   "no_ofail (\<lambda>_. P) (oassert P)"
   by (simp add: oassert_def no_ofail_def)
 
-lemma no_ofail_gets_the:
-  "no_ofail P f \<Longrightarrow> no_fail P (gets_the (f :: ('s, 'a) lookup))"
-  by (fastforce simp: no_ofail_def no_fail_def gets_the_def gets_def
-                      get_def assert_opt_def bind_def return_def fail_def
-               split: option.split)
+lemma no_ofail_gets_the_eq:
+  "no_ofail P f \<longleftrightarrow> no_fail P (gets_the (f :: ('s, 'a) lookup))"
+  by (auto simp: no_ofail_def no_fail_def gets_the_def gets_def
+                 get_def assert_opt_def bind_def return_def fail_def
+         split: option.split)
+
+lemmas no_ofail_gets_the =
+  no_ofail_gets_the_eq[THEN iffD1]
 
 lemma no_ofail_is_triple[wp_trip]:
   "no_ofail P f = triple_judgement P f (\<lambda>s f. f s \<noteq> None)"
@@ -348,7 +360,7 @@ lemma ovalidNF_pre_imp:
   by (simp add: ovalidNF_def)
 
 lemma no_ofail_pre_imp:
-  "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; no_ofail P f \<rbrakk> \<Longrightarrow> no_ofail P' f"
+  "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f"
   by (simp add: no_ofail_def)
 
 lemma ovalid_post_imp:
diff --git a/proof/crefine/lib/AutoCorres_C.thy b/proof/crefine/lib/AutoCorres_C.thy
index 6b3f6b7abf..1b189f0a66 100644
--- a/proof/crefine/lib/AutoCorres_C.thy
+++ b/proof/crefine/lib/AutoCorres_C.thy
@@ -934,10 +934,10 @@ lemma terminates_spec_no_fail:
       using normal by auto
     show ?thesis
       apply (clarsimp simp: ac AC_call_L1_def L2_call_L1_def)
-      apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select
-                wp_del: select_f_wp)
-      apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce)
-      apply (wpsimp wp: nf_pre)+
+      apply (wpsimp wp_del: select_f_wp)
+            apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce)
+           apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select)+
+      apply (fastforce simp: nf_pre)
       done
   qed
 
diff --git a/proof/infoflow/refine/ADT_IF_Refine_C.thy b/proof/infoflow/refine/ADT_IF_Refine_C.thy
index ec9dff489c..60d409bff2 100644
--- a/proof/infoflow/refine/ADT_IF_Refine_C.thy
+++ b/proof/infoflow/refine/ADT_IF_Refine_C.thy
@@ -193,23 +193,20 @@ lemma handleInterrupt_no_fail:
 
 lemma handleEvent_Interrupt_no_fail: "no_fail (invs' and ex_abs einvs) (handleEvent Interrupt)"
   apply (simp add: handleEvent_def)
-  apply (rule no_fail_pre)
    apply wp
-    apply (rule handleInterrupt_no_fail)
-   apply (simp add: crunch_simps)
-   apply (rule_tac Q="\<lambda>r s. ex_abs (einvs) s \<and> invs' s \<and>
-                            (\<forall>irq. r = Some irq
-                                   \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)"
-                in hoare_strengthen_post)
-    apply (rule hoare_vcg_conj_lift)
-     apply (rule corres_ex_abs_lift)
-      apply (rule dmo_getActiveIRQ_corres)
-     apply wp
-     apply simp
-    apply wp
-     apply simp
-    apply (rule doMachineOp_getActiveIRQ_IRQ_active)
-   apply clarsimp
+     apply (rule handleInterrupt_no_fail)
+    apply (simp add: crunch_simps)
+    apply (rule_tac Q="\<lambda>r s. ex_abs (einvs) s \<and> invs' s \<and>
+                             (\<forall>irq. r = Some irq
+                                    \<longrightarrow> intStateIRQTable (ksInterruptState s) irq \<noteq> irqstate.IRQInactive)"
+                 in hoare_strengthen_post)
+     apply (rule hoare_vcg_conj_lift)
+      apply (rule corres_ex_abs_lift)
+       apply (rule dmo_getActiveIRQ_corres)
+      apply wpsimp
+     apply (wpsimp wp: doMachineOp_getActiveIRQ_IRQ_active)
+    apply clarsimp
+   apply wpsimp
   apply (clarsimp simp: invs'_def valid_state'_def)
   done
 
diff --git a/proof/invariant-abstract/ARM/Machine_AI.thy b/proof/invariant-abstract/ARM/Machine_AI.thy
index ab2f402f20..9077037067 100644
--- a/proof/invariant-abstract/ARM/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM/Machine_AI.thy
@@ -271,8 +271,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]:
 lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
   "no_fail \<top> (invalidateCacheRange_RAM s e p)"
   apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def)
-  apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp)
-   apply (auto intro: hoare_post_taut)
+  apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb)
   done
 
 lemma no_fail_branchFlushRange[simp, wp]:
diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
index 5a172f2603..b98d74625b 100644
--- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
+++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy
@@ -280,8 +280,7 @@ lemma no_fail_invalidateCacheRange_I[simp, wp]:
 lemma no_fail_invalidateCacheRange_RAM[simp, wp]:
   "no_fail \<top> (invalidateCacheRange_RAM s e p)"
   apply (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def)
-  apply (rule no_fail_pre, wp no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb, simp)
-   apply (auto intro: hoare_post_taut)
+  apply (wpsimp wp: no_fail_invalidateL2Range no_fail_invalidateByVA no_fail_dsb)
   done
 
 lemma no_fail_branchFlushRange[simp, wp]:
diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy
index ec6dffbdf6..e31be58437 100644
--- a/proof/refine/AARCH64/Schedule_R.thy
+++ b/proof/refine/AARCH64/Schedule_R.thy
@@ -1575,11 +1575,6 @@ lemma corres_assert_ret:
   apply (simp add: assert_def return_def fail_def)
   done
 
-lemma corres_assert_assume_l:
-  "corres dc P Q (f ()) g
-  \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
-  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
-
 lemma corres_assert_assume_r:
   "corres dc P Q f (g ())
   \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"
diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy
index 2ae604d46e..d495a8db2d 100644
--- a/proof/refine/AARCH64/TcbAcc_R.thy
+++ b/proof/refine/AARCH64/TcbAcc_R.thy
@@ -1599,9 +1599,8 @@ lemma no_fail_asUser [wp]:
   "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
   apply (simp add: asUser_def split_def)
   apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
   done
 
 lemma asUser_setRegister_corres:
diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy
index 1eeb7b4351..8b3d92fa3e 100644
--- a/proof/refine/ARM/Schedule_R.thy
+++ b/proof/refine/ARM/Schedule_R.thy
@@ -1454,11 +1454,6 @@ lemma corres_assert_ret:
   apply (simp add: assert_def return_def fail_def)
   done
 
-lemma corres_assert_assume_l:
-  "corres dc P Q (f ()) g
-  \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
-  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
-
 lemma corres_assert_assume_r:
   "corres dc P Q f (g ())
   \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"
diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy
index b697dafd55..f040d40a8e 100644
--- a/proof/refine/ARM/TcbAcc_R.thy
+++ b/proof/refine/ARM/TcbAcc_R.thy
@@ -1534,9 +1534,8 @@ lemma no_fail_asUser [wp]:
   "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
   apply (simp add: asUser_def split_def)
   apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
   done
 
 lemma asUser_setRegister_corres:
diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy
index 6ca57825eb..07f0317cbc 100644
--- a/proof/refine/ARM/Tcb_R.thy
+++ b/proof/refine/ARM/Tcb_R.thy
@@ -341,9 +341,7 @@ lemma invokeTCB_WriteRegisters_corres:
          apply (rule asUser_corres)
          apply (simp add: zipWithM_mapM getRestartPC_def setNextPC_def)
          apply (rule corres_Id, simp+)
-         apply (rule no_fail_pre, wp no_fail_mapM)
-            apply clarsimp
-            apply (wp no_fail_setRegister | simp)+
+         apply (wpsimp wp: no_fail_mapM no_fail_setRegister)+
         apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
           apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]])
             apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]])
diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy
index 0b6d59bdc9..b4edbdf7f4 100644
--- a/proof/refine/ARM_HYP/Schedule_R.thy
+++ b/proof/refine/ARM_HYP/Schedule_R.thy
@@ -1550,11 +1550,6 @@ lemma corres_assert_ret:
   apply (simp add: assert_def return_def fail_def)
   done
 
-lemma corres_assert_assume_l:
-  "corres dc P Q (f ()) g
-  \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
-  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
-
 lemma corres_assert_assume_r:
   "corres dc P Q f (g ())
   \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"
diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy
index 409f3d5673..cecb49920c 100644
--- a/proof/refine/ARM_HYP/TcbAcc_R.thy
+++ b/proof/refine/ARM_HYP/TcbAcc_R.thy
@@ -1581,9 +1581,8 @@ lemma no_fail_asUser [wp]:
   "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
   apply (simp add: asUser_def split_def)
   apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
   done
 
 lemma asUser_setRegister_corres:
diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy
index 8524d6bdd5..2637f53166 100644
--- a/proof/refine/RISCV64/Schedule_R.thy
+++ b/proof/refine/RISCV64/Schedule_R.thy
@@ -1419,11 +1419,6 @@ lemma corres_assert_ret:
   apply (simp add: assert_def return_def fail_def)
   done
 
-lemma corres_assert_assume_l:
-  "corres dc P Q (f ()) g
-  \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
-  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
-
 lemma corres_assert_assume_r:
   "corres dc P Q f (g ())
   \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"
diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy
index 708fdaedcc..2cee7bc860 100644
--- a/proof/refine/RISCV64/TcbAcc_R.thy
+++ b/proof/refine/RISCV64/TcbAcc_R.thy
@@ -1568,9 +1568,8 @@ lemma no_fail_asUser [wp]:
   "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
   apply (simp add: asUser_def split_def)
   apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
   done
 
 lemma asUser_setRegister_corres:
diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy
index c4f071c007..4c9e2ac531 100644
--- a/proof/refine/RISCV64/Tcb_R.thy
+++ b/proof/refine/RISCV64/Tcb_R.thy
@@ -329,8 +329,8 @@ lemma invokeTCB_WriteRegisters_corres:
            apply (clarsimp simp: mask_def user_vtop_def
                            cong: if_cong)
           apply simp
-         apply (rule no_fail_pre, wp no_fail_mapM)
-            apply (clarsimp, (wp no_fail_setRegister | simp)+)
+         apply (wpsimp wp: no_fail_mapM no_fail_setRegister)
+        apply simp
         apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
           apply (rule corres_split_nor[OF corres_when[OF refl restart_corres]])
             apply (rule corres_split_nor[OF corres_when[OF refl rescheduleRequired_corres]])
diff --git a/proof/refine/X64/IpcCancel_R.thy b/proof/refine/X64/IpcCancel_R.thy
index 1c0bde4875..d18d63fc87 100644
--- a/proof/refine/X64/IpcCancel_R.thy
+++ b/proof/refine/X64/IpcCancel_R.thy
@@ -1448,10 +1448,7 @@ lemma no_fail_nativeThreadUsingFPU[wp]:
   "no_fail (\<top> and \<top>) (X64.nativeThreadUsingFPU thread)"
   supply Collect_const[simp del]
   apply (simp only: X64.nativeThreadUsingFPU_def)
-  apply (rule no_fail_bind)
-    apply (simp add: Arch.no_fail_machine_op_lift)
-   apply simp
-  apply wp
+  apply (wpsimp wp: Arch.no_fail_machine_op_lift)
   done
 
 lemma (in delete_one) prepareThreadDelete_corres:
diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy
index c1827abcf3..3aa19c9a3f 100644
--- a/proof/refine/X64/Schedule_R.thy
+++ b/proof/refine/X64/Schedule_R.thy
@@ -1418,11 +1418,6 @@ lemma corres_assert_ret:
   apply (simp add: assert_def return_def fail_def)
   done
 
-lemma corres_assert_assume_l:
-  "corres dc P Q (f ()) g
-  \<Longrightarrow> corres dc (P and (\<lambda>s. P')) Q (assert P' >>= f) g"
-  by (force simp: corres_underlying_def assert_def return_def bind_def fail_def)
-
 lemma corres_assert_assume_r:
   "corres dc P Q f (g ())
   \<Longrightarrow> corres dc P (Q and (\<lambda>s. Q')) f (assert Q' >>= g)"
diff --git a/proof/refine/X64/TcbAcc_R.thy b/proof/refine/X64/TcbAcc_R.thy
index d4a9418bee..a93e6af8f7 100644
--- a/proof/refine/X64/TcbAcc_R.thy
+++ b/proof/refine/X64/TcbAcc_R.thy
@@ -1561,9 +1561,8 @@ lemma no_fail_asUser [wp]:
   "no_fail \<top> f \<Longrightarrow> no_fail (tcb_at' t) (asUser t f)"
   apply (simp add: asUser_def split_def)
   apply wp
-   apply (simp add: no_fail_def)
-   apply (wp hoare_drop_imps)
-  apply simp
+    apply (simp add: no_fail_def)
+    apply (wpsimp wp: hoare_drop_imps no_fail_threadGet)+
   done
 
 lemma asUser_setRegister_corres:
diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy
index 5d33d79026..f90c895e5b 100644
--- a/proof/refine/X64/Tcb_R.thy
+++ b/proof/refine/X64/Tcb_R.thy
@@ -344,7 +344,7 @@ lemma invokeTCB_WriteRegisters_corres:
                                  mask_def user_vtop_def
                            cong: if_cong)
           apply simp
-         apply (rule no_fail_pre, wp no_fail_mapM)
+         apply (wpsimp wp: no_fail_mapM no_fail_setRegister)
             apply (clarsimp simp: sanitiseOrFlags_def sanitiseAndFlags_def)
             apply ((safe)[1], (wp no_fail_setRegister | simp)+)
         apply (rule corres_split_nor[OF asUser_postModifyRegisters_corres[simplified]])
diff --git a/tools/autocorres/tests/examples/FactorialTest.thy b/tools/autocorres/tests/examples/FactorialTest.thy
index de0314c599..0cad8e4130 100644
--- a/tools/autocorres/tests/examples/FactorialTest.thy
+++ b/tools/autocorres/tests/examples/FactorialTest.thy
@@ -47,7 +47,7 @@ proof (induct n arbitrary: m rule: less_induct)
 
    show "no_ofail (\<lambda>_. unat x < m) (factorial' m x)"
      apply (subst factorial'.simps)
-     apply (wp induct_asm ovalid_post_triv)
+     apply (wpsimp wp: induct_asm ovalid_post_triv)
      apply unat_arith
     done
 qed