diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy
index 3618371ae..94a6a6cc0 100644
--- a/lib/clib/CCorresLemmas.thy
+++ b/lib/clib/CCorresLemmas.thy
@@ -630,6 +630,13 @@ lemma ccorres_liftE:
   by (fastforce split: xstate.splits
                 simp: liftE_def ccorres_underlying_def bind_def' return_def unif_rrel_def)
 
+lemma ccorres_liftE':
+  fixes \<Gamma>
+  assumes cc: "ccorresG sr \<Gamma> (r \<circ> Inr) xf P P' hs a c"
+  shows   "ccorresG sr \<Gamma> r xf P P' hs (liftE a) c"
+  using cc
+  by (auto intro!: ccorres_liftE cong: ccorres_context_cong)
+
 lemma ccorres_if_bind:
   "ccorres_underlying sr Gamm r xf arrel axf G G' hs (if a then (b >>= f) else (c >>= f)) d
   \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf G G' hs ((if a then b else c) >>= f) d"
@@ -871,9 +878,9 @@ proof -
   qed
   thus ?thesis using lxs j pn
     apply (auto simp: init_xs_def word_less_nat_alt neq_Nil_conv unat_word_ariths unat_of_nat push_mods
-                simp del: unsigned_of_nat
                 elim!: ccorres_guard_imp2
-                dest!: spec[where x=Nil])
+                dest!: spec[where x=Nil]
+                cong: ccorres_all_cong)
     done
 qed
 
@@ -1151,4 +1158,23 @@ qed
 
 lemmas ccorres_While' = ccorres_While[where C'=UNIV, simplified]
 
+
+\<comment> \<open>simp rules for rewriting common patterns in the return relations\<close>
+lemma ccorres_dc_o_simp[simp]:
+  "ccorres_underlying srel \<Gamma> (dc \<circ> f) xf ar axf P Q hs m c
+   = ccorres_underlying srel \<Gamma> dc xf ar axf P Q hs m c"
+  "ccorres_underlying srel \<Gamma> r xf (dc \<circ> f) axf P Q hs m c
+   = ccorres_underlying srel \<Gamma> r xf dc axf P Q hs m c"
+  by (simp cong: ccorres_all_cong)+
+
+lemma ccorres_inl_rrel_inl_rrel[simp]:
+  "ccorres_underlying srel \<Gamma> r xf (inl_rrel (inl_rrel ar)) axf P Q hs m c
+   = ccorres_underlying srel \<Gamma> r xf (inl_rrel ar) axf P Q hs m c"
+  by (simp add: inl_rrel_inl_rrel cong: ccorres_all_cong)+
+
+lemma ccorres_inr_rrel_Inr[simp]:
+  "ccorres_underlying srel \<Gamma> (inr_rrel r \<circ> Inr) xf ar axf P Q hs m c
+   = ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c"
+  by (simp cong: ccorres_context_cong)+
+
 end
diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
index a8ab1afb8..20d5c09fc 100644
--- a/lib/clib/Corres_UL_C.thy
+++ b/lib/clib/Corres_UL_C.thy
@@ -1719,4 +1719,110 @@ lemma ccorres_grab_asm:
    ccorres_underlying sr G rr xf ar ax (P and K Q) P' hs f g"
   by (fastforce simp: ccorres_underlying_def)
 
+
+\<comment> \<open> An experimental cong rule for rewriting everywhere reasonable, with full context.
+    Can cause problems when there are schematic variables or when one of the return relations
+    takes a pair as a parameter. \<close>
+lemma ccorres_context_cong_helper':
+  assumes c: "ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c"
+  assumes "\<And>s. P s = P' s"
+  \<comment> \<open>Don't use membership equality when rewriting Q, as the LHS can be simplified into something
+     that is unable to unify with the RHS.
+  assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> s' \<in> Q = (s' \<in> Q')"\<close>
+  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q = Q'"
+  assumes "hs = hs'"
+  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk> \<Longrightarrow> a s = a' s"
+  assumes "\<And>s s' s''. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk>  \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'"
+  assumes "\<And>s s' t'.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
+             xf t' = xf' t'"
+  assumes "\<And>x s t s' t'.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s);
+               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
+             r x (xf' t') = r' x (xf' t')"
+  assumes "\<And>s s' t' n.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> size hs'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
+             axf t' = axf' t'"
+  assumes "\<And>x s t s' t' n.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> size hs';
+               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
+             ar x (axf' t') = ar' x (axf' t')"
+  shows   "ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'"
+  using c
+  apply -
+  apply (rule ccorresI')
+  apply (erule (1) ccorresE)
+      apply (force simp: assms)
+     apply (force simp: assms)
+    apply (force simp: assms)
+   apply (clarsimp simp: assms)
+   apply (erule exec_handlers_semantic_equivD2)
+   apply (force simp: assms)
+  apply (fastforce simp: unif_rrel_def assms)
+  done
+
+lemma ccorres_context_cong_helper:
+  assumes "\<And>s. P s = P' s"
+  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q = Q'"
+  assumes "hs = hs'"
+  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk> \<Longrightarrow> a s = a' s"
+  assumes "\<And>s s' s''. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk>  \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'"
+  assumes "\<And>s s' t'.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
+             xf t' = xf' t'"
+  assumes "\<And>x s t s' t'.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s);
+               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
+             r x (xf' t') = r' x (xf' t')"
+  assumes "\<And>s s' t' n.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> size hs'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
+             axf t' = axf' t'"
+  assumes "\<And>x s t s' t' n.
+             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> size hs';
+               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
+             ar x (axf' t') = ar' x (axf' t')"
+  shows   "ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c
+           = ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'"
+  using assms
+  apply -
+  apply rule
+   apply (erule ccorres_context_cong_helper'; assumption)
+  apply (erule ccorres_context_cong_helper')
+  by (fastforce simp: semantic_equiv_sym exec_handlers_semantic_equiv[where a=c and b=c'])+
+
+lemmas ccorres_context_cong = ccorres_context_cong_helper[OF _ _ _ _ semantic_equivI]
+
+\<comment> \<open> Only rewrite guards, the handler stack and function bodies, with context.
+    This is often more useful, as we generally want the return relations and extraction
+    functions to be stable while working with a ccorres_underlying statement. \<close>
+lemma ccorres_context_weak_cong:
+  assumes "\<And>s. P s = P' s"
+  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q = Q'"
+  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk> \<Longrightarrow> a s = a' s"
+  assumes "\<And>s s' s''. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk>  \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> s'' = \<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> s''"
+  shows   "ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c
+           = ccorres_underlying sr \<Gamma> r xf ar axf P' Q' hs a' c'"
+  by (clarsimp simp: assms cong: ccorres_context_cong)
+
+\<comment> \<open> Even more restrictive: only rewrite the abstract monad. \<close>
+lemma ccorres_abstract_cong:
+  "\<lbrakk> \<And>s s'. \<lbrakk> (s, s') \<in> sr; P s ; s' \<in> P' \<rbrakk> \<Longrightarrow> a s = b s \<rbrakk> \<Longrightarrow>
+   ccorres_underlying sr G r xf ar axf P P' hs a c
+   = ccorres_underlying sr G r xf ar axf P P' hs b c"
+  by (clarsimp cong: ccorres_context_weak_cong)
+
+\<comment> \<open> Rewrite almost everywhere, without context. This should behave the same as with normal
+    term rewriting with no cong rule, except it will not rewrite the state relation or function
+    environment. \<close>
+lemma ccorres_all_cong:
+  "\<lbrakk> r=r'; xf=xf'; ar=ar'; axf=axf'; P=P'; Q=Q'; hs=hs'; m=m'; c=c' \<rbrakk> \<Longrightarrow>
+   ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c
+   = ccorres_underlying srel \<Gamma> r' xf' ar' axf' P' Q' hs' m' c'"
+  by (simp cong: ccorres_context_cong)
+
+\<comment> \<open> Only rewrite guards, the handler stack and function bodies, without context.
+    We make this the default behaviour, so that the the return relations and extraction
+    functions are stable under simplification. \<close>
+lemmas ccorres_weak_cong = ccorres_all_cong[OF refl refl refl refl, cong]
+
 end