diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy
index 837b0c8c250..f1b2d6960ca 100644
--- a/lib/Monads/reader_option/Reader_Option_VCG.thy
+++ b/lib/Monads/reader_option/Reader_Option_VCG.thy
@@ -116,8 +116,8 @@ lemma owhile_ovalid[wp]:
    \<Longrightarrow> ovalid (I a) (owhile_inv C B a I M) Q"
   unfolding owhile_inv_def owhile_def ovalid_def
   apply clarify
-  apply (frule_tac I = "\<lambda>a. I a s" in option_while_rule)
-  apply auto
+  apply (frule (1) option_while_rule[where I = "\<lambda>a. I a s" for s])
+   apply auto
   done
 
 definition ovalid_property where "ovalid_property P x = (\<lambda>s f. (\<forall>r. Some r = x s f \<longrightarrow> P r s))"
@@ -187,7 +187,7 @@ lemma owhile_NF[wp]:
    \<Longrightarrow> ovalidNF (I a) (owhile_inv C B a I M) Q"
   unfolding owhile_inv_def ovalidNF_def ovalid_def
   apply clarify
-  apply (rule_tac I = I and M = "measure (\<lambda>r. M r s)" in owhile_rule)
+  apply (rule owhile_rule[where I = I and M = "measure (\<lambda>r. M r s)" and s = s for s])
        apply fastforce
       apply fastforce
      apply fastforce
diff --git a/lib/Monads/trace/Trace_Det.thy b/lib/Monads/trace/Trace_Det.thy
index 4b17f18dbfa..54c7f031518 100644
--- a/lib/Monads/trace/Trace_Det.thy
+++ b/lib/Monads/trace/Trace_Det.thy
@@ -55,10 +55,8 @@ lemma det_UN:
 lemma bind_detI[simp, intro!]:
   "\<lbrakk> det f; \<forall>x. det (g x) \<rbrakk> \<Longrightarrow> det (f >>= g)"
   unfolding bind_def det_def
-  apply clarsimp
-  apply (erule_tac x=s in allE)
-  apply clarsimp
-  done
+  apply (erule all_reg[rotated])
+  by clarsimp
 
 lemma det_modify[iff]:
   "det (modify f)"
diff --git a/lib/Monads/trace/Trace_Empty_Fail.thy b/lib/Monads/trace/Trace_Empty_Fail.thy
index 472ec988afe..cfc2fcf51b1 100644
--- a/lib/Monads/trace/Trace_Empty_Fail.thy
+++ b/lib/Monads/trace/Trace_Empty_Fail.thy
@@ -58,8 +58,7 @@ lemma empty_failD3:
 lemma empty_fail_bindD1:
   "empty_fail (a >>= b) \<Longrightarrow> empty_fail a"
   unfolding empty_fail_def bind_def
-  apply clarsimp
-  apply (drule_tac x=s in spec)
+  apply (erule all_reg[rotated])
   by (force simp: split_def mres_def vimage_def split: tmres.splits)
 
 
@@ -112,10 +111,7 @@ lemma empty_fail_select[empty_fail_cond]:
 lemma mres_bind_empty:
   "mres ((f >>= g) s) = {}
    \<Longrightarrow> mres (f s) = {} \<or> (\<forall>res\<in>mres (f s). mres (g (fst res) (snd res)) = {})"
-  apply clarsimp
-  apply (clarsimp simp: mres_def split_def vimage_def bind_def)
-  apply (rename_tac rv s' trace)
-  apply (drule_tac x=rv in spec, drule_tac x=s' in spec)
+  apply (clarsimp simp: bind_def mres_def split_def)
   apply (clarsimp simp: image_def)
   apply fastforce
   done
diff --git a/lib/Monads/trace/Trace_Lemmas.thy b/lib/Monads/trace/Trace_Lemmas.thy
index 557c2a855de..eb504156f80 100644
--- a/lib/Monads/trace/Trace_Lemmas.thy
+++ b/lib/Monads/trace/Trace_Lemmas.thy
@@ -204,8 +204,8 @@ lemma liftE_liftM:
 lemma liftME_liftM:
   "liftME f = liftM (case_sum Inl (Inr \<circ> f))"
   unfolding liftME_def liftM_def bindE_def returnOk_def lift_def
-  apply (rule ext, rename_tac x)
-  apply (rule_tac f="bind x" in arg_cong)
+  apply (rule ext)
+  apply (rule arg_cong[where f="bind m" for m])
   apply (fastforce simp: throwError_def split: sum.splits)
   done
 
diff --git a/lib/Monads/trace/Trace_Monad.thy b/lib/Monads/trace/Trace_Monad.thy
index f0d093b77ec..45241d87468 100644
--- a/lib/Monads/trace/Trace_Monad.thy
+++ b/lib/Monads/trace/Trace_Monad.thy
@@ -806,6 +806,7 @@ lemma parallel_def2:
    apply (rule exI, rule conjI, assumption)+
    apply (simp add: list_all2_conv_all_nth list_eq_iff_nth_eq split_def prod_eq_iff)
    apply clarsimp
+  apply (rename_tac ys zs)
   apply (rule_tac x="map (((\<noteq>) Env) o fst) ys" in exI)
   apply (simp add: zip_map1 o_def split_def)
   apply (strengthen subst[where P="\<lambda>xs. (xs, v) \<in> S" for v S, mk_strg I _ E])
diff --git a/lib/Monads/trace/Trace_Monad_Equations.thy b/lib/Monads/trace/Trace_Monad_Equations.thy
index 00156438b89..50e76715dc5 100644
--- a/lib/Monads/trace/Trace_Monad_Equations.thy
+++ b/lib/Monads/trace/Trace_Monad_Equations.thy
@@ -117,35 +117,22 @@ lemma gets_the_returns:
   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>
+  "\<lbrakk> f = gets_the (fn_f o fn'); \<And>rv. g rv = gets_the (fn_g rv 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 clarsimp
+  apply (rule exI[where x="\<lambda>s. case (fn_f s) of None \<Rightarrow> None | Some v \<Rightarrow> fn_g v s"])
   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>
+  "\<lbrakk> f = gets_the (fn_f o fn'); \<And>rv. g rv = gets_the (fn_g rv 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)
+  unfolding bindE_def
+  apply (erule gets_the_eq_bind[where fn_g="\<lambda>rv s. case rv of Inl e \<Rightarrow> Some (Inl e) | Inr v \<Rightarrow> fn_g v s"])
   apply (simp add: lift_def gets_the_returns split: sum.split)
-  apply fastforce
   done
 
 lemma gets_the_fail:
@@ -531,7 +518,7 @@ lemma put_trace_mapM_x:
 
 lemma rev_surj:
   "surj rev"
-  by (rule_tac f=rev in surjI, simp)
+  by (rule surjI[where f=rev], simp)
 
 lemma select_image:
   "select (f ` S) = do x \<leftarrow> select S; return (f x) od"
diff --git a/lib/Monads/trace/Trace_More_VCG.thy b/lib/Monads/trace/Trace_More_VCG.thy
index 927bb042728..8ae996e52fb 100644
--- a/lib/Monads/trace/Trace_More_VCG.thy
+++ b/lib/Monads/trace/Trace_More_VCG.thy
@@ -137,8 +137,8 @@ lemma hoare_split_bind_case_sum:
              "\<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)
+  apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]])
+  apply (wpsimp wp: x split: sum.splits)
   done
 
 lemma hoare_split_bind_case_sumE:
@@ -147,8 +147,8 @@ lemma hoare_split_bind_case_sumE:
   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])
+  apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]])
+  apply (wpsimp wp: x[unfolded validE_def] split: sum.splits)
   done
 
 lemma assertE_sp:
@@ -256,12 +256,11 @@ lemma doesn't_grow_proof:
   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 (erule le_less_trans[rotated])
+  apply (rule card_mono[OF y])
   apply clarsimp
   apply (rule ccontr)
-  apply (subgoal_tac "x \<notin> S b", simp)
-  apply (erule use_valid [OF _ x])
+  apply (drule (2) use_valid[OF _ x, OF _ conjI])
   apply simp
   done
 
@@ -297,13 +296,12 @@ lemma shrinks_proof:
   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 (erule less_le_trans[rotated])
+  apply (rule psubset_card_mono[OF y])
   apply (rule psubsetI)
    apply clarsimp
    apply (rule ccontr)
-   apply (subgoal_tac "x \<notin> S b", simp)
-   apply (erule use_valid [OF _ x])
+   apply (drule (2) use_valid[OF _ x, OF _ conjI])
    apply simp
   by (metis use_valid w z)
 
@@ -393,13 +391,12 @@ lemma P_bool_lift:
   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 back_subst[where P=P], assumption)
   apply (rule iffI)
-   apply (rule classical)
-   apply (drule (1) use_valid [OF _ f])
-   apply simp
-  apply (erule (1) use_valid [OF _ t])
+   apply (erule (1) use_valid [OF _ t])
+  apply (rule classical)
+  apply (drule (1) use_valid [OF _ f])
+  apply simp
   done
 
 lemmas fail_inv = hoare_fail_any[where Q="\<lambda>_. P" and P=P for P]
@@ -416,11 +413,10 @@ lemma hoare_Ball_helper:
   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)
+  apply (drule bspec, erule back_subst[where P="\<lambda>A. x\<in>A" for x])
+   apply (erule post_by_hoare[OF y, rotated])
+   apply (rule refl)
+  apply (erule (1) post_by_hoare[OF x])
   done
 
 lemma handy_prop_divs:
@@ -479,14 +475,14 @@ 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> mres (f s)\<rbrace>"
   apply (clarsimp simp: valid_def)
-  apply (subgoal_tac "s = b", simp)
-  apply (simp add: state_unchanged [OF x])
+  apply (rule back_subst[where P="\<lambda>s. x\<in>mres (f s)" for x], assumption)
+  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 (cases xs, simp_all)
   apply wp
   done
 
@@ -522,13 +518,13 @@ 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)
+  by (cases 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)
+  by (cases G, simp_all add: x y)
 
 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>
@@ -589,11 +585,12 @@ lemma univ_wp:
 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> mres (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>"
-  apply (rule hoare_pre_imp [OF _ univ_wp])
+  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])
+  apply (drule mp)
+   apply (simp add: state_unchanged[OF x])
+  apply simp
   done
 
 lemma other_hoare_in_monad_post:
@@ -630,10 +627,10 @@ lemma bindE_split_recursive_asm:
   apply (clarsimp simp: validE_def valid_def bindE_def in_bind lift_def)
   apply (erule allE, erule(1) impE)
   apply (drule(1) bspec, simp)
-  apply (case_tac x, simp_all add: in_throwError)
+  apply (clarsimp simp: in_throwError split: sum.splits)
   apply (drule x)
   apply (clarsimp simp: validE_def valid_def)
-  apply (drule(1) bspec, simp)
+  apply (drule(1) bspec, simp split: sum.splits)
   done
 
 lemma validE_R_abstract_rv:
@@ -687,9 +684,8 @@ lemma valid_rv_split:
 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
+  apply (clarsimp simp: valid_def split_def)
+  by (metis (full_types) fst_eqD snd_conv)
 
 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>
@@ -718,23 +714,19 @@ lemma validE_pre_satisfies_post:
 
 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)
+  by (fastforce simp: Ball_def validE_R_def validE_def valid_def split: sum.splits)
 
 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)
+  by (fastforce simp: Ball_def validE_E_def validE_def valid_def split: sum.splits)
 
 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)
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
 
 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)
+  by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)
 
 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>"
diff --git a/lib/Monads/trace/Trace_RG.thy b/lib/Monads/trace/Trace_RG.thy
index 3dec5f51b0a..ce39dc9af02 100644
--- a/lib/Monads/trace/Trace_RG.thy
+++ b/lib/Monads/trace/Trace_RG.thy
@@ -272,8 +272,8 @@ proof (induct n arbitrary: res)
   case 0 then show ?case by auto
 next
   case (Suc n)
-  have drop_1: "\<And>tr res. (tr, res) \<in> f s \<Longrightarrow> \<exists>res'. (drop 1 tr, res') \<in> f s"
-    by (case_tac tr; fastforce dest: prefix_closedD[rotated] intro: Suc)
+  have drop_1: "(tr, res) \<in> f s \<Longrightarrow> \<exists>res'. (drop 1 tr, res') \<in> f s" for tr res
+    by (cases tr; fastforce dest: prefix_closedD[rotated] intro: Suc)
   show ?case
     using Suc.hyps[OF Suc.prems]
     by (metis drop_1[simplified] drop_drop add_0 add_Suc)
@@ -291,7 +291,8 @@ lemma parallel_prefix_closed[wp_split]:
   "\<lbrakk>prefix_closed f; prefix_closed g\<rbrakk>
    \<Longrightarrow> prefix_closed (parallel f g)"
   apply (subst prefix_closed_def, clarsimp simp: parallel_def)
-  apply (case_tac f_steps; clarsimp)
+  apply (subst (asm) zip.zip_Cons)
+  apply (clarsimp split: list.splits)
   apply (drule(1) prefix_closedD)+
   apply fastforce
   done
@@ -338,7 +339,7 @@ lemma guar_cond_drop_Suc:
   "\<lbrakk>guar_cond R s0 (drop (Suc n) xs);
     fst (xs ! n) \<noteq> Env \<longrightarrow> R (last_st_tr (drop (Suc n) xs) s0) (snd (xs ! n))\<rbrakk>
    \<Longrightarrow> guar_cond R s0 (drop n xs)"
-  by (case_tac "n < length xs"; simp add: guar_cond_drop_Suc_eq)
+  by (cases "n < length xs"; simp add: guar_cond_drop_Suc_eq)
 
 lemma rely_cond_Cons_eq:
   "rely_cond R s0 (x # xs)
@@ -427,8 +428,9 @@ proof -
                       hd_drop_conv_nth hd_append)
      apply (fastforce simp: split_def intro!: nth_equalityI)
     apply clarsimp
-    apply (erule_tac x=n in meta_allE)+
     apply (drule meta_mp, erule rely_cond_is_drop, simp)
+    apply clarsimp
+    apply (erule meta_allE, drule meta_mp, assumption)+
     apply (subst(asm) rely_cond_drop_Suc_eq[where xs="map f xs" for f xs], simp)
     apply (clarsimp simp: last_st_tr_drop_map_zip_hd if_split[where P="\<lambda>x. x = Env"]
                           split_def)
@@ -493,7 +495,7 @@ lemma put_trace_res:
    \<Longrightarrow> \<exists>n. tr = drop n xs \<and> n \<le> length xs
          \<and> res = (case n of 0 \<Rightarrow> Result ((), s) | _ \<Rightarrow> Incomplete)"
   apply (clarsimp simp: put_trace_eq_drop)
-  apply (case_tac n; auto intro: exI[where x=0])
+  apply (auto simp: gr0_conv_Suc intro: exI[where x=0])
   done
 
 lemma put_trace_twp[wp]:
diff --git a/lib/Monads/trace/Trace_VCG.thy b/lib/Monads/trace/Trace_VCG.thy
index f3fca936c09..a879ef0912e 100644
--- a/lib/Monads/trace/Trace_VCG.thy
+++ b/lib/Monads/trace/Trace_VCG.thy
@@ -1016,7 +1016,7 @@ lemmas liftME_E_E_wp[wp_split] = validE_validE_E [OF liftME_wp, simplified, OF v
 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)
+  by (cases 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>"
diff --git a/lib/Monads/wp/WPFix.thy b/lib/Monads/wp/WPFix.thy
index 1428c8fae7e..619d43a0b90 100644
--- a/lib/Monads/wp/WPFix.thy
+++ b/lib/Monads/wp/WPFix.thy
@@ -242,11 +242,13 @@ lemma demo2:
     \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inl 8) | Some y \<Rightarrow> R (Inr y)))
     \<and> (\<forall>x. I x \<longrightarrow> (case x of None \<Rightarrow> R (Inr 9) | Some y \<Rightarrow> R (Inl (y - 1))))"
   apply (intro exI conjI[rotated] allI)
+    apply (rename_tac x)
     apply (case_tac x; simp)
      apply wpfix
      apply (rule P)
     apply wpfix
     apply (rule P)
+   apply (rename_tac x)
    apply (case_tac x; simp)
     apply wpfix
     apply (rule P)
diff --git a/lib/Monads/wp/WPI.thy b/lib/Monads/wp/WPI.thy
index 3b67c283ed5..9e772719d9d 100644
--- a/lib/Monads/wp/WPI.thy
+++ b/lib/Monads/wp/WPI.thy
@@ -116,6 +116,7 @@ private lemma
   (atomic f (\<lambda>s. A' s \<and> Pres' s) (\<lambda>r s. A r s \<and> Pres r s) B Q' \<Longrightarrow> trip Ts) \<Longrightarrow> trip Ts"
   apply (erule meta_mp)
   apply (clarsimp simp: valid_def atomic_def)
+  apply (rename_tac P s r s')
   apply (drule_tac x=P in spec)
   apply (drule_tac x=P in meta_spec)
   apply (drule_tac x=s in spec)+