diff --git a/tools/autocorres/CCorresE.thy b/tools/autocorres/CCorresE.thy
index 198ffa0a2..918f7a885 100644
--- a/tools/autocorres/CCorresE.thy
+++ b/tools/autocorres/CCorresE.thy
@@ -269,7 +269,7 @@ lemma ccorresE_termination':
   apply clarsimp
   apply (erule allE, erule (1) impE)
   apply (clarsimp split: sum.splits xstate.splits)
-  apply (erule (1) my_BallE)
+  apply (drule (1) bspec)
   apply clarsimp
   apply (erule allE, erule impE, rule refl)
   apply clarsimp
@@ -313,7 +313,7 @@ lemma ccorresE_While:
        apply (insert ccorresE_exec_Normal [OF body_refines])[1]
        apply clarsimp
        apply atomize
-       apply (erule allE2, erule (1) impE)
+       apply (erule allE, erule allE, erule (1) impE)
        apply (frule snd_whileLoopE_first_step, force simp: cond_match)
        apply clarsimp
        apply (erule impE)
@@ -329,7 +329,7 @@ lemma ccorresE_While:
       apply (insert ccorresE_exec_Abrupt [OF body_refines])[1]
       apply clarsimp
       apply atomize
-      apply (erule allE2, erule (1) impE)
+      apply (erule allE, erule allE, erule (1) impE)
       apply (frule snd_whileLoopE_first_step, force simp: cond_match)
       apply clarsimp
       apply (subst whileLoopE_unroll)
@@ -414,13 +414,10 @@ lemma ccorresE_symb_exec_l:
   apply (clarsimp simp: ccorresE_def validE_def valid_def exs_valid_def)
   apply (erule allE, erule impE, assumption)+
   apply (clarsimp)
-  apply (erule (1) my_BallE)
-  apply clarsimp
-  apply (erule_tac x=aa and y=s in allE2)
+  apply (drule (1) bspec)
   apply clarsimp
   apply (monad_eq simp: Bex_def Ball_def split: xstate.splits)
-  apply fastforce
-  done
+  by fastforce
 
 lemma ccorresE_no_fail_term:
   " \<lbrakk> ccorresE st ct \<Gamma> G G' A B; no_fail G A; s \<in> G'; G (st s); ct \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> B \<down> Normal s"
diff --git a/tools/autocorres/CorresXF.thy b/tools/autocorres/CorresXF.thy
index 0099910b1..c203cf080 100644
--- a/tools/autocorres/CorresXF.thy
+++ b/tools/autocorres/CorresXF.thy
@@ -51,12 +51,12 @@ lemma corresXF_simple_corresXF:
    apply clarsimp
    apply (erule allE, erule impE, force)
    apply (clarsimp split: sum.splits cong del: unit.case_cong)
-   apply (erule (1) my_BallE)
+   apply (drule (1) bspec)
    apply clarsimp
   apply clarsimp
   apply (erule_tac x=s in allE)
   apply (clarsimp split: sum.splits cong del: unit.case_cong)
-  apply (erule (1) my_BallE)
+  apply (drule (1) bspec)
   apply clarsimp
   done
 
@@ -144,23 +144,12 @@ lemma corresXF_exec_normal:
   "\<lbrakk> corresXF st ret ex P A B; (Inr r', s') \<in> fst (B s); \<not> snd (A (st s)); P s \<rbrakk>
       \<Longrightarrow> (Inr (ret r' s'), st s') \<in> fst (A (st s))"
   using corresXF_simple_exec
-  apply (clarsimp simp: corresXF_def)
-  apply (clarsimp split: sum.splits)
-  apply (erule_tac x=s in allE)
-  apply clarsimp
-  apply (erule (1) my_BallE)
-  apply clarsimp
-  done
+  by (fastforce simp: corresXF_def)
 
 lemma corresXF_exec_except:
   "\<lbrakk> corresXF st ret ex P A B; (Inl r', s') \<in> fst (B s); \<not> snd (A (st s)); P s \<rbrakk>
       \<Longrightarrow> (Inl (ex r' s'), st s') \<in> fst (A (st s))"
-  apply (clarsimp simp: corresXF_def)
-  apply (erule allE, erule impE, force)
-  apply (clarsimp)
-  apply (erule (1) my_BallE)
-  apply (clarsimp split: sum.splits)
-  done
+  by (fastforce simp: corresXF_def)
 
 lemma corresXF_exec_fail:
   "\<lbrakk> corresXF st ret ex P A B; snd (B s); P s \<rbrakk>
@@ -256,11 +245,9 @@ lemma corresXF_join:
   apply (subst (asm) corresXF_simple_corresXF[symmetric])+
   apply (subst corresXF_simple_corresXF[symmetric])
   apply (unfold bindE_def)
-  apply (erule corresXF_simple_join [where P'="\<lambda>a b s. (case b of Inl r \<Rightarrow> a = Inl (E r s) | Inr r \<Rightarrow> a = Inr (V r s) \<and> P' (theRight a) r s)"])
+  apply (erule corresXF_simple_join [where P'="\<lambda>a b s. (case b of Inl r \<Rightarrow> a = Inl (E r s) | Inr r \<Rightarrow> a = Inr (V r s) \<and> P' (projr a) r s)"])
     apply (simp add: corresXF_simple_def split: sum.splits unit.splits)
-    apply (clarsimp simp: NonDetMonad.lift_def
-      throwError_def return_def split: sum.splits
-      cong del: unit.case_cong)
+    apply (clarsimp simp: NonDetMonad.lift_def throwError_def return_def)
     apply fastforce
    apply (fastforce simp: NonDetMonad.validE_def split: sum.splits cong del: unit.case_cong)
   apply simp
@@ -272,11 +259,9 @@ lemma corresXF_except:
   apply (subst (asm) corresXF_simple_corresXF[symmetric])+
   apply (subst corresXF_simple_corresXF[symmetric])
   apply (unfold handleE'_def)
-  apply (erule corresXF_simple_join [where P'="\<lambda>a b s. (case b of Inr r \<Rightarrow> a = Inr (V r s) | Inl r \<Rightarrow> a = Inl (E r s) \<and> P' (theLeft a) r s)"])
+  apply (erule corresXF_simple_join [where P'="\<lambda>a b s. (case b of Inr r \<Rightarrow> a = Inr (V r s) | Inl r \<Rightarrow> a = Inl (E r s) \<and> P' (projl a) r s)"])
     apply (simp add: corresXF_simple_def split: sum.splits unit.splits)
-    apply (clarsimp simp: NonDetMonad.lift_def throwError_def
-      return_def split: sum.splits unit.splits cong del:
-      unit.case_cong)
+    apply (clarsimp simp: NonDetMonad.lift_def throwError_def return_def)
     apply fastforce
    apply (clarsimp simp: NonDetMonad.validE_def split: sum.splits cong del: unit.case_cong)
   apply simp
@@ -315,19 +300,16 @@ lemma corresXF_simple_loop_terminates:
    apply (clarsimp simp: cond_match)
   apply atomize
   apply clarsimp
-  apply (erule allE2)
-  apply (erule impE)
+  apply (erule allE, erule allE, erule impE)
    apply (erule conjI)
    apply (clarsimp simp: cond_match)
   apply clarsimp
   apply (rule whileLoop_terminates.intros(2))
    apply (clarsimp simp: cond_match)
   apply (clarsimp split: sum.splits)
-  apply (erule (1) my_BallE)
+  apply (drule (1) bspec)
   apply clarsimp
-  apply (erule (1) my_BallE)
-  apply clarsimp
-  apply (erule_tac x=a and y=b in allE2)
+  apply (drule (1) bspec)
   apply clarsimp
   apply (frule use_valid [OF _ pred_inv])
     apply (clarsimp simp: no_fail_def)
@@ -579,13 +561,13 @@ lemma corresXF_while:
   apply (rule corresXF_simple_weaken_pre)
    apply (rule corresXF_simple_while [where
       P ="\<lambda>x s. (case x of Inl _ \<Rightarrow> True| Inr v \<Rightarrow>  P v s)"
-                  and P'="\<lambda>x s. P' (theRight x) s"])
+                  and P'="\<lambda>x s. P' (projr x) s"])
        apply (insert body_corres)[1]
        apply (subst (asm) corresXF_simple_corresXF[symmetric])
        apply atomize
-       apply (erule_tac x="theRight x" in allE)
-       apply (clarsimp simp: corresXF_simple_def NonDetMonad.lift_def
-      throwError_def return_def split: sum.splits)
+       apply (erule_tac x="projr x" in allE)
+       apply (clarsimp simp: corresXF_simple_def NonDetMonad.lift_def throwError_def return_def
+                       split: sum.splits)
       apply (clarsimp simp: cond_match split: sum.splits)
      apply (clarsimp simp: lift_def split: sum.splits)
      apply (cut_tac  pred_inv [unfolded validE_def, simplified lift_def])
@@ -671,7 +653,7 @@ proof -
         apply (erule impE)
          apply (erule contrapos_nn)
          apply (erule new_body_fails_more)
-        apply (erule (1) my_BallE)
+        apply (drule (1) bspec)
         apply clarsimp
         apply (monad_eq simp: cond_match guardE_def split_def  split: sum.splits)
        apply (drule snd_whileLoopE_first_step)
@@ -708,9 +690,9 @@ lemma ccorresE_corresXF_merge:
   apply clarsimp
   apply (erule allE, erule impE, fastforce)
   apply (case_tac t; clarsimp)
-   apply (erule (1) my_BallE)
+   apply (drule (1) bspec)
    apply (clarsimp split: sum.splits)
-  apply (erule (1) my_BallE)
+  apply (drule (1) bspec)
   apply (clarsimp split: sum.splits)
   apply (drule no_throw_Inr, assumption)
    apply simp
@@ -816,8 +798,7 @@ lemma corresXF_spec:
     \<Longrightarrow>  corresXF st ret ex P (specE A) (specE A')"
   apply (monad_eq simp: corresXF_def specE_def spec_def Ball_def split: sum.splits)
   apply (frule_tac y=s' in surjD)
-  apply (clarsimp simp: image_def set_eq_UNIV)
-  apply metis
+  apply blast
   done
 
 lemma corresXF_throw:
diff --git a/tools/autocorres/ExceptionRewrite.thy b/tools/autocorres/ExceptionRewrite.thy
index 3ff8f0671..b40ae9952 100644
--- a/tools/autocorres/ExceptionRewrite.thy
+++ b/tools/autocorres/ExceptionRewrite.thy
@@ -75,10 +75,10 @@ lemma no_return_bindE:
     apply (erule disjE)
      apply clarsimp
     apply clarsimp
-    apply (erule (1) my_BallE)
+    apply (drule (1) bspec)
     apply clarsimp
    apply clarsimp
-   apply (erule (1) my_BallE)
+   apply (drule (1) bspec)
    apply (clarsimp split: sum.splits)
   apply (clarsimp simp: snd_bindE no_return_def validE_def valid_def)
   apply (erule_tac x=x in allE)
@@ -344,13 +344,17 @@ lemma L1_catch_cond_seq:
   apply (rule L1_catch_single_cond)
   done
 
+lemma unit_not_Inr:
+  "(a \<noteq> Inr ()) = (a = Inl ())"
+  by (cases a; clarsimp)
+
 (* This exciting lemma lets up break up a L1_catch into two parts in
  * the exciting circumstance that "E" never returns. *)
 lemma L1_catch_seq_cond_noreturn_ex:
   "\<lbrakk> no_return \<top> E \<rbrakk> \<Longrightarrow> (L1_catch (L1_seq (L1_condition c A B) C) E) = (L1_seq (L1_catch (L1_condition c A B) E) (L1_catch C E))"
   apply (clarsimp simp: L1_defs)
-  apply (monad_eq simp: no_return_def valid_def validE_def Ball_def
-      Bex_def unit_Inl_or_Inr split:sum.splits)
+  apply (monad_eq simp: no_return_def valid_def validE_def Ball_def Bex_def unit_not_Inr
+                  split: sum.splits)
   apply (safe, (metis Inr_not_Inl)+)
   done
 
diff --git a/tools/autocorres/ExecConcrete.thy b/tools/autocorres/ExecConcrete.thy
index 141de6e91..5e5e41785 100644
--- a/tools/autocorres/ExecConcrete.thy
+++ b/tools/autocorres/ExecConcrete.thy
@@ -179,8 +179,8 @@ lemma corresXF_simple_exec_concrete:
 lemma corresXF_exec_concrete_self:
     "corresXF st (\<lambda>r s. r) (\<lambda>r s. r) P (exec_concrete st M) M"
   apply (subst corresXF_simple_corresXF [symmetric])
-  apply clarsimp
-  apply (rule corresXF_simple_exec_concrete)
+  apply (simp add: surjective_sum[where f=id, simplified])
+  apply (rule corresXF_simple_exec_concrete)+
   done
 
 lemma corresXF_exec_concrete [intro?]:
@@ -307,7 +307,7 @@ lemma corresXF_simple_exec_abstract:
 lemma corresXF_exec_abstract_self:
     "corresXF st (\<lambda>r s. r) (\<lambda>r s. r) P M (exec_abstract st M)"
   apply (subst corresXF_simple_corresXF [symmetric])
-  apply clarsimp
+  apply (simp add: surjective_sum[where f=id, simplified])
   apply (rule corresXF_simple_exec_abstract)
   done
 
diff --git a/tools/autocorres/HeapLift.thy b/tools/autocorres/HeapLift.thy
index 1555dc70f..a8a5c46ad 100644
--- a/tools/autocorres/HeapLift.thy
+++ b/tools/autocorres/HeapLift.thy
@@ -157,9 +157,8 @@ definition "abs_spec st P (A :: ('a \<times> 'a) set) (C :: ('c \<times> 'c) set
 lemma L2Tcorres_spec [heap_abs]:
   "\<lbrakk> abs_spec st P A C \<rbrakk>
      \<Longrightarrow> L2Tcorres st (L2_seq (L2_guard P) (\<lambda>_. (L2_spec A))) (L2_spec C)"
-  apply (monad_eq simp: corresXF_def L2Tcorres_def L2_defs image_def set_eq_UNIV
-             split_def Ball_def state_select_def abs_spec_def split: sum.splits)
-  done
+  by (monad_eq simp: corresXF_def L2Tcorres_def L2_defs image_def split_def Ball_def
+                     state_select_def abs_spec_def)
 
 lemma abs_spec_constant [heap_abs]:
   "abs_spec st \<top> {(a, b). C} {(a, b). C}"
@@ -1368,7 +1367,7 @@ lemma heap_abs_expr_c_guard_array [heap_abs]:
    apply (subst (asm) (2) set_array_addrs)
    apply force
   apply clarsimp
-  apply (erule (1) my_BallE)
+  apply (drule (1) bspec)
   apply (drule (1) valid_typ_heap_c_guard)
   apply simp
   done
diff --git a/tools/autocorres/L2Defs.thy b/tools/autocorres/L2Defs.thy
index aa6f5b01f..25b00ef91 100644
--- a/tools/autocorres/L2Defs.thy
+++ b/tools/autocorres/L2Defs.thy
@@ -174,8 +174,7 @@ lemma L2corres_spec:
   apply (clarsimp simp: L2corres_def L2_defs L1_spec_def corresXF_def
                         liftE_def spec_alt_def return_def bind_def select_def)
   apply (clarsimp simp: image_def)
-  apply (subst (asm) set_eq_UNIV)
-  apply metis
+  apply (smt (verit) UNIV_I mem_Collect_eq)
   done
 
 lemma L2corres_seq:
@@ -280,7 +279,7 @@ lemma corresXF_E:
   apply clarsimp
   apply (erule allE, erule impE, fastforce)
   apply clarsimp
-  apply (erule (1) my_BallE)
+  apply (drule (1) bspec)
   apply (clarsimp split: sum.splits)
   done
 
@@ -506,9 +505,7 @@ lemma L2_gets_bind: "\<lbrakk> \<And>s s'. V s = V s' \<rbrakk> \<Longrightarrow
   apply (rule ext)
   apply (clarsimp simp: L2_seq_def L2_gets_def gets_def get_def return_def bindE_def)
   apply (clarsimp simp: liftE_def2 bind_def lift_def)
-  apply atomize
-  apply (erule_tac x=x and y=undefined in allE2)
-  apply simp
+  apply metis
   done
 
 (* TODO: remove internal var if it is not user-visible *)
diff --git a/tools/autocorres/MonadMono.thy b/tools/autocorres/MonadMono.thy
index e2406f864..be9e698a6 100644
--- a/tools/autocorres/MonadMono.thy
+++ b/tools/autocorres/MonadMono.thy
@@ -12,7 +12,8 @@
 theory MonadMono
 imports
   NonDetMonadEx
-  "Monads.OptionMonadWP"
+  Monads.WhileLoopRulesCompleteness
+  Monads.OptionMonadWP
 begin
 
 (*
@@ -284,15 +285,11 @@ definition "option_monad_mono f \<equiv>
 lemma option_monad_mono_eq:
   "(\<And>m. f m = gets_the (f' m)) \<Longrightarrow> monad_mono f = option_monad_mono f'"
   apply (clarsimp simp: monad_mono_def option_monad_mono_def gets_the_def
-    gets_def get_def assert_opt_def return_def fail_def bind_def' split: option.splits)
-  apply (rule iff_allI iff_impI)+
-  apply (rule_tac t = "\<forall>r. f' x s = Some r \<longrightarrow> (\<exists>r'. f' y s = Some r') \<and> (\<forall>r'. f' y s = Some r' \<longrightarrow> r = r')"
-              and s = "\<forall>r. f' x s = Some r \<longrightarrow> f' y s = Some r" in subst)
-   apply (force intro: iff_allI iff_impI)
-  apply (rule iffI)
-   apply (metis (no_types) option.exhaust)
-  apply force
-  done
+                        gets_def get_def assert_opt_def return_def fail_def bind_def'
+                  split: option.splits)
+  apply (intro iff_allI iffI impI allI)
+   apply (metis option.collapse)
+  by fastforce
 
 lemma measure_ocall_ovalid [wp]:
     "\<lbrakk> \<forall> m. ovalid P (x m) Q; option_monad_mono x \<rbrakk> \<Longrightarrow> ovalid P (measure_ocall x) Q"
diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy
index 486fabefd..7a6a62067 100644
--- a/tools/autocorres/NonDetMonadEx.thy
+++ b/tools/autocorres/NonDetMonadEx.thy
@@ -11,7 +11,11 @@
 theory NonDetMonadEx
 imports
   "Word_Lib.WordSetup"
-  "Lib.NonDetMonadLemmaBucket"
+  "Monads.NonDetMonadVCG"
+  "Lib.Monad_Equations"
+  "Lib.More_NonDetMonadVCG"
+  "Monads.No_Throw"
+  "Monads.No_Fail"
   "Monads.OptionMonadND"
 begin
 
diff --git a/tools/autocorres/TypeStrengthen.thy b/tools/autocorres/TypeStrengthen.thy
index 54bba785b..314d370de 100644
--- a/tools/autocorres/TypeStrengthen.thy
+++ b/tools/autocorres/TypeStrengthen.thy
@@ -101,6 +101,9 @@ lemma TS_return_L2_condition:
     "L2_condition (\<lambda>_. c) (TS_return A) (TS_return B) = TS_return (if c then A else B)"
   by (monad_eq simp: L2_defs TS_return_def)
 
+lemma split_distrib: "case_prod (\<lambda>a b. T (f a b)) = (\<lambda>x. T (case_prod (\<lambda>a b. f a b) x))"
+  by (clarsimp simp: split_def)
+
 lemmas [ts_rule pure] =
   TS_return_L2_gets
   TS_return_L2_seq
diff --git a/tools/autocorres/WordAbstract.thy b/tools/autocorres/WordAbstract.thy
index d23fe0f36..e2ebd0f0c 100644
--- a/tools/autocorres/WordAbstract.thy
+++ b/tools/autocorres/WordAbstract.thy
@@ -322,8 +322,9 @@ lemma sint_shiftl_nonneg:
   apply (drule (1) int_shiftl_lt_2p_bits[rotated])
   apply (clarsimp simp: min_def split: if_split_asm)
   apply (rule conjI; clarsimp)
-   apply (smt (z3) decr_length_less_iff diff_Suc_Suc diff_is_0_eq diff_le_mono diff_le_self
-                   diff_zero le_def less_handy_casesE nat_less_le order_refl)
+   apply (smt (verit) One_nat_def bot_nat_0.extremum_uniqueI diff_Suc_eq_diff_pred
+                      le_diff_iff le_diff_iff' len_gt_0 len_of_finite_1_def less_eq_Suc_le
+                      nat_le_Suc_less_imp)
   using less_eq_decr_length_iff nat_le_linear by blast
 
 lemma abstract_val_signed_shiftl_signed:
diff --git a/tools/autocorres/tests/examples/Memcpy.thy b/tools/autocorres/tests/examples/Memcpy.thy
index 894d2fc92..720c482e1 100644
--- a/tools/autocorres/tests/examples/Memcpy.thy
+++ b/tools/autocorres/tests/examples/Memcpy.thy
@@ -182,8 +182,7 @@ lemma memcpy_word:
      apply clarsimp
     apply (clarsimp simp: h_val_def)[1]
     apply (rule arg_cong[where f=from_bytes])
-    apply (subst numeral_eqs(3))+
-    apply simp
+    apply (simp add: numeral_nat)
     apply (rule_tac x=0 in allE, assumption, erule impE, unat_arith)
     apply (rule_tac x=1 in allE, assumption, erule impE, unat_arith)
     apply (rule_tac x=2 in allE, assumption, erule impE, unat_arith)
@@ -383,7 +382,8 @@ lemma update_bytes_postpend: "length bs = x + 1 \<Longrightarrow>
   apply (clarsimp simp:ptr_add_def)
   apply (subst heap_update_list_concat_fold_hrs_mem)
    apply clarsimp+
-  by (metis append_eq_conv_conj append_self_conv hd_drop_conv_nth2 lessI take_hd_drop)
+  apply (metis append.right_neutral append_eq_conv_conj lessI take_Suc_conv_app_nth)
+  done
 
 lemma h_val_not_id_general:
   fixes y :: "'a::mem_type ptr"
@@ -600,8 +600,7 @@ lemma memcpy_wp':
       apply clarsimp
       apply (rule update_bytes_eq)
         apply (subgoal_tac "min (unat i) (unat (i + 1)) = unat i")
-         apply clarsimp
-        apply clarsimp
+         apply presburger
         apply unat_arith
        apply (clarsimp simp:ptr_add_def)
       apply clarsimp