# HG changeset patch
# User haftmann
# Date 1593691858 0
# Node ID bad75618fb8277c6073e641b11ec53ded49343df
# Parent  ace45a11a45ed97dfb656340e0488d3fc006cd2e
extraction of equations x = t from premises beneath meta-all

diff -r ace45a11a45e -r bad75618fb82 CONTRIBUTORS
--- a/CONTRIBUTORS	Thu Jul 02 08:49:04 2020 +0000
+++ b/CONTRIBUTORS	Thu Jul 02 12:10:58 2020 +0000
@@ -20,6 +20,10 @@
 * May 2020: Florian Haftmann
   Generic algebraically founded bit operations NOT, AND, OR, XOR.
 
+* June 2020: Florian Haftmann
+  Simproc defined_all for more aggressive substitution with variables
+  from assumptions.
+
 
 Contributions to Isabelle2020
 -----------------------------
diff -r ace45a11a45e -r bad75618fb82 NEWS
--- a/NEWS	Thu Jul 02 08:49:04 2020 +0000
+++ b/NEWS	Thu Jul 02 12:10:58 2020 +0000
@@ -77,10 +77,10 @@
 * Session HOL-Word: Theory Z2 is not used any longer.
 Minor INCOMPATIBILITY.
 
-* Rewrite rule subst_all performs
+* Simproc defined_all and rewrite rule subst_all perform
 more aggressive substitution with variables from assumptions.
 INCOMPATIBILITY, use something like
-"supply subst_all [simp del]"
+"supply subst_all [simp del] [[simproc del: defined_all]]"
 to leave fragile proofs unaffected.
 
 
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Auth/Guard/P1.thy
--- a/src/HOL/Auth/Guard/P1.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Auth/Guard/P1.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -282,6 +282,7 @@
 
 lemma insertion_resilience: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L
 \<longrightarrow> ins (L,Suc i,M) \<notin> valid A n B"
+supply [[simproc del: defined_all]]
 apply (induct i)
 (* i = 0 *)
 apply clarify
@@ -481,6 +482,7 @@
 
 lemma pro_imp_Guard [rule_format]: "[| evs \<in> p1; B \<notin> bad; A \<notin> bad |] ==>
 pro B ofr A r I (cons M L) J C \<in> set evs \<longrightarrow> Guard ofr {priK A} (spies evs)"
+supply [[simproc del: defined_all]]
 apply (erule p1.induct) (* +3 subgoals *)
 (* Nil *)
 apply simp
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Auth/Guard/P2.thy
--- a/src/HOL/Auth/Guard/P2.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Auth/Guard/P2.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -193,6 +193,7 @@
 
 lemma insertion_resilience: "\<forall>L. L \<in> valid A n B \<longrightarrow> Suc i < len L
 \<longrightarrow> ins (L,Suc i,M) \<notin> valid A n B"
+supply [[simproc del: defined_all]]
 apply (induct i)
 (* i = 0 *)
 apply clarify
@@ -393,6 +394,7 @@
 
 lemma pro_imp_Guard [rule_format]: "[| evs \<in> p2; B \<notin> bad; A \<notin> bad |] ==>
 pro B ofr A r I (cons M L) J C \<in> set evs \<longrightarrow> Guard ofr {priK A} (spies evs)"
+supply [[simproc del: defined_all]]
 apply (erule p2.induct) (* +3 subgoals *)
 (* Nil *)
 apply simp
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -981,7 +981,8 @@
     from fvar obtain upd w
       where upd: "upd = snd (fst (fvar statDeclC stat fn a s2))" and
               v: "v=(w,upd)"
-      by (cases "fvar statDeclC stat fn a s2") simp
+      by (cases "fvar statDeclC stat fn a s2")
+        (simp, use surjective_pairing in blast)
     {
       fix j val fix s::state
       assume "normal s3"
@@ -1025,7 +1026,8 @@
     from avar obtain upd w
       where upd: "upd = snd (fst (avar G i a s2))" and
               v: "v=(w,upd)"
-      by (cases "avar G i a s2") simp
+      by (cases "avar G i a s2")
+        (simp, use surjective_pairing in blast)
     {
       fix j val fix s::state
       assume "normal s2'"
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Data_Structures/AVL_Bal_Set.thy
--- a/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Data_Structures/AVL_Bal_Set.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -139,7 +139,6 @@
    avl t' \<and> height t = height t' + (if decr t t' then 1 else 0)"
 apply(induction t arbitrary: t' a rule: split_max_induct)
  apply(auto simp: max_absorb1 max_absorb2 height_1_iff split!: splits prod.splits)
-apply(fastforce)+
 done
 
 lemma avl_delete: "avl t \<Longrightarrow>
diff -r ace45a11a45e -r bad75618fb82 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/HOL.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -1234,8 +1234,6 @@
 simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close>
 simproc_setup defined_all("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
 
-declare [[simproc del: defined_all]]
-
 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
 
 simproc_setup neq ("x = y") = \<open>fn _ =>
diff -r ace45a11a45e -r bad75618fb82 src/HOL/HOLCF/IOA/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/Abstraction.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/HOLCF/IOA/Abstraction.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -296,7 +296,6 @@
   apply (simp add: nil_is_Conc)
   text \<open>cons case\<close>
   apply (pair aa)
-  apply auto
   done
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/HOLCF/IOA/TLS.thy
--- a/src/HOL/HOLCF/IOA/TLS.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/HOLCF/IOA/TLS.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -153,9 +153,7 @@
   apply (pair ex)
   apply (Seq_case x2)
   apply (simp add: unlift_def)
-  apply fast
   apply (simp add: unlift_def)
-  apply fast
   apply (simp add: unlift_def)
   apply (pair a)
   apply (Seq_case_simp s)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointer_Examples.thy
--- a/src/HOL/Hoare/Pointer_Examples.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Hoare/Pointer_Examples.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -31,7 +31,6 @@
   \<^cancel>\<open>apply clarsimp\<close>
   \<^cancel>\<open>apply(rename_tac ps')\<close>
   \<^cancel>\<open>apply(fastforce intro:notin_List_update[THEN iffD2])\<close>
-  apply fastforce
   done
 
 text\<open>And now with ghost variables \<^term>\<open>ps\<close> and \<^term>\<open>qs\<close>. Even
@@ -48,7 +47,6 @@
   {List next q (rev Ps @ Qs)}"
 apply vcg_simp
  apply fastforce
-apply fastforce
 done
 
 text "A longer readable version:"
@@ -104,7 +102,6 @@
 apply vcg_simp
   apply clarsimp
  apply clarsimp
-apply clarsimp
 done
 
 
@@ -461,7 +458,6 @@
 apply (simp only:distPath_def)
 apply vcg_simp
   apply clarsimp
-  apply clarsimp
  apply (case_tac "(q = Null)")
   apply (fastforce intro: Path_is_List)
  apply clarsimp
@@ -499,7 +495,6 @@
   {islist next p \<and> map elem (rev(list next p)) = Xs}"
 apply vcg_simp
  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
-apply fastforce
 done
 
 
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointer_ExamplesAbort.thy
--- a/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Hoare/Pointer_ExamplesAbort.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -23,7 +23,6 @@
 apply vcg_simp
   apply fastforce
  apply(fastforce intro:notin_List_update[THEN iffD2])
-apply fastforce
 done
 
 end
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare/Pointers0.thy
--- a/src/HOL/Hoare/Pointers0.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Hoare/Pointers0.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -198,7 +198,6 @@
   \<^cancel>\<open>apply simp\<close>
   \<^cancel>\<open>apply(rule_tac x = "p#qs" in exI)\<close>
   \<^cancel>\<open>apply simp\<close>
-  apply fastforce
   done
 
 
@@ -254,7 +253,6 @@
 apply vcg_simp
   apply clarsimp
  apply clarsimp
-apply clarsimp
 done
 
 
@@ -427,7 +425,6 @@
   {islist next p \<and> map elem (rev(list next p)) = Xs}"
 apply vcg_simp
  apply (clarsimp simp: subset_insert_iff neq_Nil_conv fun_upd_apply new_notin)
-apply fastforce
 done
 
 
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare_Parallel/RG_Hoare.thy
--- a/src/HOL/Hoare_Parallel/RG_Hoare.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Hoare_Parallel/RG_Hoare.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -174,6 +174,7 @@
   "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x
    \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m
    \<longrightarrow> x!i -e\<rightarrow> x!Suc i"
+  supply [[simproc del: defined_all]]
 apply(induct x,simp)
 apply clarify
 apply(erule cptn.cases,simp)
@@ -185,7 +186,7 @@
  apply(subgoal_tac "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> ctran)")
   apply force
  apply clarify
- apply(erule_tac x="Suc ia" in allE,simp)
+   apply(erule_tac x="Suc ia" in allE,simp)
 apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (J j) \<notin> ctran" for H J in allE,simp)
 done
 
@@ -232,6 +233,7 @@
   (\<forall>i. (Suc i)<length x \<longrightarrow>
           (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow>
   (\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> fst(x!j)=fst(x!k)"
+  supply [[simproc del: defined_all]]
 apply(induct x)
  apply clarify
  apply(force elim:cptn.cases)
@@ -326,6 +328,7 @@
   " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar;
   stable pre rely; stable post rely\<rbrakk>
   \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]"
+  supply [[simproc del: defined_all]]
 apply(unfold com_validity_def)
 apply clarify
 apply(simp add:comm_def)
@@ -595,6 +598,7 @@
   "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow>
   (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow>
   (\<exists>xs\<in> cp (Some P) s. x=map (lift Q) xs)"
+  supply [[simproc del: defined_all]]
 apply(erule cptn_mod.induct)
 apply(unfold cp_def)
 apply safe
@@ -625,6 +629,7 @@
   (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow>
   (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i
    \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)"
+  supply [[simproc del: defined_all]]
 apply(erule cptn.induct)
 apply(unfold cp_def)
 apply safe
@@ -879,6 +884,7 @@
   "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar;
    stable pre rely;  stable post rely; x \<in> cptn_mod \<rbrakk>
   \<Longrightarrow>  \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)"
+  supply [[simproc del: defined_all]]
 apply(erule cptn_mod.induct)
 apply safe
 apply (simp_all del:last.simps)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Hoare_Parallel/RG_Tran.thy
--- a/src/HOL/Hoare_Parallel/RG_Tran.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -176,6 +176,7 @@
 lemma cptn_onlyif_cptn_mod_aux [rule_format]:
   "\<forall>s Q t xs.((Some a, s), Q, t) \<in> ctran \<longrightarrow> (Q, t) # xs \<in> cptn_mod 
   \<longrightarrow> (Some a, s) # (Q, t) # xs \<in> cptn_mod"
+  supply [[simproc del: defined_all]]
 apply(induct a)
 apply simp_all
 \<comment> \<open>basic\<close>
@@ -718,6 +719,7 @@
   (\<exists>clist. (length clist = length xs) \<and> 
   (xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist) \<and> 
   (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))"
+  supply [[simproc del: defined_all]]
 apply(induct ys)
  apply(clarify)
  apply(rule_tac x="map (\<lambda>i. []) [0..<length xs]" in exI)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Library/Quantified_Premise_Simproc.thy
--- a/src/HOL/Library/Quantified_Premise_Simproc.thy	Thu Jul 02 08:49:04 2020 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Author: Florian Haftmann, TU München *)
-
-theory Quantified_Premise_Simproc
-  imports Main
-begin
-
-declare [[simproc add: defined_all]]
-
-end
diff -r ace45a11a45e -r bad75618fb82 src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -410,6 +410,7 @@
   \<longrightarrow>
 sttp_of (compTpInitLvars jmb lvars (ST, pre @ replicate (length lvars) Err))
     = (ST, pre @ map (Fun.comp OK snd) lvars)"
+  supply [[simproc del: defined_all]]
   apply (induct lvars)
    apply simp
 
diff -r ace45a11a45e -r bad75618fb82 src/HOL/MicroJava/J/WellForm.thy
--- a/src/HOL/MicroJava/J/WellForm.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/MicroJava/J/WellForm.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -532,7 +532,6 @@
 apply (erule_tac x = "Da" in allE)
 apply (clarsimp)
  apply (simp add: map_of_map)
- apply (clarify)
  apply (subst method_rec, assumption+)
  apply (simp add: map_add_def map_of_map split: option.split)
 done
@@ -552,7 +551,6 @@
 apply (erule_tac x = "Da" in allE)
 apply (clarsimp)
  apply (simp add: map_of_map)
- apply (clarify)
  apply (subst method_rec, assumption+)
  apply (simp add: map_add_def map_of_map split: option.split)
 done
@@ -599,7 +597,6 @@
 apply (simp (no_asm_use) only: map_add_Some_iff)
 apply (erule disjE)
 apply (simp (no_asm_use) add: map_of_map) apply blast
-apply blast
 apply (rule trans [symmetric], rule sym, assumption)
 apply (rule_tac x=vn in fun_cong)
 apply (rule trans, rule field_rec, assumption+)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Nominal/Examples/Class1.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -2936,7 +2936,9 @@
 apply(subgoal_tac "y\<sharp>[aa].Ma")
 apply(drule sym)
 apply(simp_all add: abs_fresh)
-done
+apply (metis abs_fresh(5))
+done
+ 
 
 lemma fin_rest_elims:
   shows "fin (Cut <a>.M (x).N) y \<Longrightarrow> False"
@@ -2958,7 +2960,7 @@
 lemma not_fin_subst1:
   assumes a: "\<not>(fin M x)" 
   shows "\<not>(fin (M{c:=(y).P}) x)"
-using a
+using a [[simproc del: defined_all]]
 apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
 apply(auto)
 apply(drule fin_elims, simp)
@@ -3043,7 +3045,7 @@
 lemma not_fin_subst2:
   assumes a: "\<not>(fin M x)" 
   shows "\<not>(fin (M{y:=<c>.P}) x)"
-using a
+using a [[simproc del: defined_all]]
 apply(nominal_induct M avoiding: x c y P rule: trm.strong_induct)
 apply(auto)
 apply(erule fin.cases, simp_all add: trm.inject)
@@ -3157,7 +3159,6 @@
 apply(drule fin_elims, simp)
 apply(drule fin_elims, simp)
 apply(rule fin.intros)
-apply(auto)[1]
 apply(rule subst_fresh)
 apply(simp)
 apply(drule fin_elims, simp)
@@ -3195,7 +3196,7 @@
 lemma fin_substn_nrename:
   assumes a: "fin M x" "x\<noteq>y" "x\<sharp>P"
   shows "M[x\<turnstile>n>y]{y:=<c>.P} = Cut <c>.P (x).(M{y:=<c>.P})"
-using a
+using a [[simproc del: defined_all]]
 apply(nominal_induct M avoiding: x y c P rule: trm.strong_induct)
 apply(drule fin_Ax_elim)
 apply(simp)
@@ -3440,7 +3441,6 @@
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substn)
 apply(simp add: fic.intros abs_fresh)
@@ -3471,7 +3471,6 @@
 apply(drule fic_elims, simp)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(drule fic_elims, simp)
-apply(erule conjE)+
 apply(drule freshc_after_substc)
 apply(simp)
 apply(simp add: fic.intros abs_fresh)
@@ -3501,7 +3500,6 @@
 apply(drule fic_elims, simp)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substc)
 apply(simp)
@@ -3514,7 +3512,6 @@
 apply(drule fic_elims, simp)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substc)
 apply(simp)
@@ -3528,7 +3525,6 @@
 apply(drule fic_elims, simp)
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substc)
 apply(simp)
@@ -3546,7 +3542,6 @@
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
 apply(rule fic.intros)
-apply(auto)[1]
 apply(rule subst_fresh)
 apply(simp)
 apply(drule fic_elims, simp)
@@ -3590,7 +3585,6 @@
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
 apply(rule fic.intros)
-apply(auto)[1]
 apply(rule subst_fresh)
 apply(simp)
 apply(drule fic_elims, simp)
@@ -3683,7 +3677,6 @@
 apply(simp)
 apply(drule fic_ImpR_elim)
 apply(simp add: abs_fresh fresh_atm)
-apply(auto)[1]
 apply(generate_fresh "coname")
 apply(fresh_fun_simp)
 apply(simp add: trm.inject alpha fresh_atm calc_atm abs_fresh fresh_prod)
@@ -4715,7 +4708,7 @@
 lemma a_redu_NotL_elim:
   assumes a: "NotL <a>.M x \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = NotL <a>.M' x \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4736,7 +4729,7 @@
 lemma a_redu_NotR_elim:
   assumes a: "NotR (x).M a \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = NotR (x).M' a \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4757,7 +4750,7 @@
 lemma a_redu_AndR_elim:
   assumes a: "AndR <a>.M <b>.N c\<longrightarrow>\<^sub>a R"
   shows "(\<exists>M'. R = AndR <a>.M' <b>.N c \<and> M\<longrightarrow>\<^sub>aM') \<or> (\<exists>N'. R = AndR <a>.M <b>.N' c \<and> N\<longrightarrow>\<^sub>aN')"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4846,7 +4839,7 @@
 lemma a_redu_AndL1_elim:
   assumes a: "AndL1 (x).M y \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = AndL1 (x).M' y \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4867,7 +4860,7 @@
 lemma a_redu_AndL2_elim:
   assumes a: "AndL2 (x).M y \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = AndL2 (x).M' y \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4888,7 +4881,7 @@
 lemma a_redu_OrL_elim:
   assumes a: "OrL (x).M (y).N z\<longrightarrow>\<^sub>a R"
   shows "(\<exists>M'. R = OrL (x).M' (y).N z \<and> M\<longrightarrow>\<^sub>aM') \<or> (\<exists>N'. R = OrL (x).M (y).N' z \<and> N\<longrightarrow>\<^sub>aN')"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4977,7 +4970,7 @@
 lemma a_redu_OrR1_elim:
   assumes a: "OrR1 <a>.M b \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = OrR1 <a>.M' b \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -4998,7 +4991,7 @@
 lemma a_redu_OrR2_elim:
   assumes a: "OrR2 <a>.M b \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = OrR2 <a>.M' b \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -5019,7 +5012,7 @@
 lemma a_redu_ImpL_elim:
   assumes a: "ImpL <a>.M (y).N z\<longrightarrow>\<^sub>a R"
   shows "(\<exists>M'. R = ImpL <a>.M' (y).N z \<and> M\<longrightarrow>\<^sub>aM') \<or> (\<exists>N'. R = ImpL <a>.M (y).N' z \<and> N\<longrightarrow>\<^sub>aN')"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -5108,7 +5101,7 @@
 lemma a_redu_ImpR_elim:
   assumes a: "ImpR (x).<a>.M b \<longrightarrow>\<^sub>a R"
   shows "\<exists>M'. R = ImpR (x).<a>.M' b \<and> M\<longrightarrow>\<^sub>aM'"
-using a
+using a [[simproc del: defined_all]]
 apply(erule_tac a_redu.cases, simp_all add: trm.inject)
 apply(erule_tac l_redu.cases, simp_all add: trm.inject)
 apply(erule_tac c_redu.cases, simp_all add: trm.inject)
@@ -5454,7 +5447,6 @@
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(drule fin_elims, simp)
 apply(drule fin_elims, simp)
-apply(auto)[1]
 apply(drule freshn_after_substc)
 apply(simp add: fin.intros)
 apply(subgoal_tac "\<exists>c'::coname. c'\<sharp>(trm1{coname3:=(x).P},P,coname1,trm2{coname3:=(x).P},coname2)")
@@ -5466,12 +5458,10 @@
 apply(rule exists_fresh'(2)[OF fs_coname1])
 apply(drule fin_elims, simp)
 apply(drule fin_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshn_after_substc)
 apply(simp add: fin.intros abs_fresh)
 apply(drule fin_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshn_after_substc)
 apply(simp add: fin.intros abs_fresh)
@@ -5578,7 +5568,6 @@
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(drule freshc_after_substn)
 apply(simp add: fic.intros)
 apply(subgoal_tac "\<exists>x'::name. x'\<sharp>(trm{x:=<b>.P},P)")
@@ -5612,12 +5601,10 @@
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substn)
 apply(simp add: fic.intros abs_fresh)
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substn)
 apply(simp add: fic.intros abs_fresh)
@@ -5630,7 +5617,6 @@
 apply(rule exists_fresh'(1)[OF fs_name1])
 apply(drule fic_elims, simp)
 apply(drule fic_elims, simp)
-apply(auto)[1]
 apply(simp add: abs_fresh fresh_atm)
 apply(drule freshc_after_substn)
 apply(simp add: fic.intros abs_fresh)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Nominal/Examples/Class3.thy
--- a/src/HOL/Nominal/Examples/Class3.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Nominal/Examples/Class3.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -297,7 +297,7 @@
   assumes a: "R[a\<turnstile>c>b] = AndR <c>.M <d>.N e" "c\<sharp>(a,b,d,e,N,R)" "d\<sharp>(a,b,c,e,M,R)" "e\<sharp>a"
   shows "(\<exists>M' N'. R = AndR <c>.M' <d>.N' e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M') \<or>
          (\<exists>M' N'. R = AndR <c>.M' <d>.N' a \<and> b=e \<and> M'[a\<turnstile>c>b] = M \<and> N'[a\<turnstile>c>b] = N \<and> c\<sharp>N' \<and> d\<sharp>M')"
-using a
+using a [[simproc del: defined_all]]
 apply(nominal_induct R avoiding: a b c d e M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: trm.inject alpha)[1]
 apply(auto split: if_splits simp add: trm.inject alpha)[1]
@@ -1487,7 +1487,7 @@
   assumes a: "R[x\<turnstile>n>y] = OrL (v).M (w).N u" "v\<sharp>(R,N,u,x,y)" "w\<sharp>(R,M,u,x,y)" "x\<noteq>y" 
   shows "(\<exists>M' N'. (R = OrL (v).M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or> 
          (\<exists>M' N'. (R = OrL (v).M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N)"
-using a
+using a [[simproc del: defined_all]]
 apply(nominal_induct R avoiding: y x u v w M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(name1,v)]\<bullet>trm1" in exI)
@@ -1550,7 +1550,7 @@
   assumes a: "R[x\<turnstile>n>y] = ImpL <c>.M (w).N u" "c\<sharp>(R,N)" "w\<sharp>(R,M,u,x,y)" "x\<noteq>y" 
   shows "(\<exists>M' N'. (R = ImpL <c>.M' (w).N' u) \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N) \<or> 
          (\<exists>M' N'. (R = ImpL <c>.M' (w).N' x) \<and> y=u \<and> M'[x\<turnstile>n>y] = M \<and> N'[x\<turnstile>n>y] = N)"
-using a
+using a [[simproc del: defined_all]]
 apply(nominal_induct R avoiding: y x u c w M N rule: trm.strong_induct)
 apply(auto split: if_splits simp add: fresh_prod fresh_atm abs_fresh alpha trm.inject)
 apply(rule_tac x="[(coname,c)]\<bullet>trm1" in exI)
@@ -2367,7 +2367,7 @@
   and     a3: "(x):N \<in> (\<parallel>(B)\<parallel>)"
   and     a4: "SNa N"
   shows   "SNa (Cut <a>.M (x).N)"
-using a1 a2 a3 a4
+using a1 a2 a3 a4 [[simproc del: defined_all]]
 apply(induct B M N arbitrary: a x rule: my_wf_induct_triple''[OF wf_measure_triple])
 apply(rule SNaI)
 apply(drule Cut_a_redu_elim)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -368,6 +368,7 @@
    "(\<exists>r'. r \<rightarrow>\<^sub>\<beta> r' \<and> s = r' \<degree>\<degree> rs) \<or>
     (\<exists>rs'. rs [\<rightarrow>\<^sub>\<beta>]\<^sub>1 rs' \<and> s = r \<degree>\<degree> rs') \<or>
     (\<exists>t u us. x \<sharp> r \<longrightarrow> r = (Lam [x].t) \<and> rs = u # us \<and> s = t[x::=u] \<degree>\<degree> us)"
+    supply [[simproc del: defined_all]]
     apply (nominal_induct u \<equiv> "r \<degree>\<degree> rs" s avoiding: x r rs rule: beta.strong_induct)
     apply (simp add: App_eq_foldl_conv)
     apply (split if_split_asm)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Probability/Random_Permutations.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -51,7 +51,7 @@
 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> 
      fold_random_permutation f x A = 
        pmf_of_set A \<bind> (\<lambda>a. fold_random_permutation f (f a x) (A - {a}))"
-by (force, simp_all)
+  by simp_all fastforce
 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,A). card A)")
   fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b and y :: 'a
   assume A: "finite A" "A \<noteq> {}" "y \<in> set_pmf (pmf_of_set A)"
@@ -126,7 +126,7 @@
 | "finite A \<Longrightarrow> A \<noteq> {} \<Longrightarrow> 
      fold_bind_random_permutation f g x A = 
        pmf_of_set A \<bind> (\<lambda>a. fold_bind_random_permutation f g (f a x) (A - {a}))"
-by (force, simp_all)
+  by simp_all fastforce
 termination proof (relation "Wellfounded.measure (\<lambda>(_,_,_,A). card A)")
   fix A :: "'a set" and f :: "'a \<Rightarrow> 'b \<Rightarrow> 'b" and x :: 'b 
     and y :: 'a and g :: "'b \<Rightarrow> 'c pmf"
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -58,6 +58,7 @@
   by (erule L.induct) iprover+
 
 lemma lemma2': "R a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
+  supply [[simproc del: defined_all]]
   apply (induct set: R)
   apply (erule L.cases)
   apply simp+
@@ -69,17 +70,19 @@
   done
 
 lemma lemma2: "R a vs ws \<Longrightarrow> good vs \<Longrightarrow> good ws"
+  supply [[simproc del: defined_all]]
   apply (induct set: R)
   apply iprover
   apply (erule good.cases)
   apply simp_all
   apply (rule good0)
   apply (erule lemma2')
-  apply assumption
+   apply assumption
   apply (erule good1)
   done
 
 lemma lemma3': "T a vs ws \<Longrightarrow> L as vs \<Longrightarrow> L (a # as) ws"
+  supply [[simproc del: defined_all]]
   apply (induct set: T)
   apply (erule L.cases)
   apply simp_all
@@ -93,6 +96,7 @@
   done
 
 lemma lemma3: "T a ws zs \<Longrightarrow> good ws \<Longrightarrow> good zs"
+  supply [[simproc del: defined_all]]
   apply (induct set: T)
   apply (erule good.cases)
   apply simp_all
@@ -107,6 +111,7 @@
   done
 
 lemma lemma4: "R a ws zs \<Longrightarrow> ws \<noteq> [] \<Longrightarrow> T a ws zs"
+  supply [[simproc del: defined_all]]
   apply (induct set: R)
   apply iprover
   apply (case_tac vs)
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -62,8 +62,8 @@
 theorem lemma2: "\<And>p. is_path r p 0 j k \<Longrightarrow> r j k = T"
   unfolding is_path_def
   apply (simp cong add: conj_cong add: split_paired_all)
-  apply (case_tac "aa")
-  apply simp+
+  apply (case_tac a)
+  apply simp_all
   done
 
 theorem is_path'_conc: "is_path' r j xs i \<Longrightarrow> is_path' r i ys k \<Longrightarrow>
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Lambda/LambdaType.thy
--- a/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -120,13 +120,19 @@
   apply simp
   done
 
-lemma types_snocE: "e \<tturnstile> ts @ [t] : Ts \<Longrightarrow>
-  (\<And>Us U. Ts = Us @ [U] \<Longrightarrow> e \<tturnstile> ts : Us \<Longrightarrow> e \<turnstile> t : U \<Longrightarrow> P) \<Longrightarrow> P"
-  apply (cases Ts rule: rev_exhaust2)
-  apply simp
-  apply (case_tac "ts @ [t]")
-  apply (simp add: types_snoc_eq)+
-  done
+lemma types_snocE:
+  assumes \<open>e \<tturnstile> ts @ [t] : Ts\<close>
+  obtains Us and U where \<open>Ts = Us @ [U]\<close> \<open>e \<tturnstile> ts : Us\<close> \<open>e \<turnstile> t : U\<close>
+proof (cases Ts rule: rev_exhaust2)
+  case Nil
+  with assms show ?thesis
+    by (cases "ts @ [t]") simp_all
+next
+  case (snoc Us U)
+  with assms have "e \<tturnstile> ts @ [t] : Us @ [U]" by simp
+  then have "e \<tturnstile> ts : Us" "e \<turnstile> t : U" by (simp_all add: types_snoc_eq)
+  with snoc show ?thesis by (rule that)
+qed
 
 
 subsection \<open>n-ary function types\<close>
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -261,7 +261,7 @@
 declare NF.induct [ind_realizer]
 declare rtranclp.induct [ind_realizer irrelevant]
 declare rtyping.induct [ind_realizer]
-lemmas [extraction_expand] = conj_assoc listall_cons_eq
+lemmas [extraction_expand] = conj_assoc listall_cons_eq subst_all equal_allI
 
 extract type_NF
 
diff -r ace45a11a45e -r bad75618fb82 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/ROOT	Thu Jul 02 12:10:58 2020 +0000
@@ -73,7 +73,6 @@
     OptionalSugar
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
-    Quantified_Premise_Simproc
     (*legacy tools*)
     Old_Datatype
     Old_Recdef
diff -r ace45a11a45e -r bad75618fb82 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Thu Jul 02 08:49:04 2020 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Thu Jul 02 12:10:58 2020 +0000
@@ -823,7 +823,6 @@
   apply clarsimp
   apply (drule bthrs)
   apply (simp (no_asm_use) add: Let_def split: prod.split_asm if_split_asm)
-  apply clarify
   apply (erule allE, erule impE, erule exI)
   apply (case_tac k)
    apply clarsimp