more simp rules

--- a/src/HOL/Data_Structures/Sorting.thy	Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/Data_Structures/Sorting.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -205,7 +205,8 @@
 lemma length_msort: "length(msort xs) = length xs"
 proof (induction xs rule: msort.induct)
   case (1 xs)
-  thus ?case by (auto simp: msort.simps[of xs] length_merge)
+  show ?case
+    by (auto simp: msort.simps [of xs] 1 length_merge)
 qed
 text \<open>Why structured proof?
    To have the name "xs" to specialize msort.simps with xs

--- a/src/HOL/Data_Structures/Trie_Fun.thy	Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/Data_Structures/Trie_Fun.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -67,12 +67,11 @@
   case 1 thus ?case by (force split: option.splits)
 next
   case 2
-  thus ?case
-    apply (auto simp add: image_iff split!: if_splits option.splits)
-       apply blast
-      apply (metis insertE insertI2 insert_Diff_single option.inject)
-     apply blast
-    by (metis insertE insertI2 insert_Diff_single option.inject)
+  show ?case
+    apply (auto simp add: image_iff 2 split!: if_splits option.splits)
+     apply (metis DiffI empty_iff insert_iff option.inject)
+     apply (metis DiffI empty_iff insert_iff option.inject)
+    done
 qed
 
 interpretation S: Set

--- a/src/HOL/HOL.thy	Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/HOL.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -941,6 +941,36 @@
 
 lemma eta_contract_eq: "(\<lambda>s. f s) = f" ..
 
+lemma subst_all:
+  \<open>(\<And>x. x = a \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close>
+proof (rule equal_intr_rule)
+  assume *: \<open>\<And>x. x = a \<Longrightarrow> PROP P x\<close>
+  show \<open>PROP P a\<close>
+    by (rule *) (rule refl)
+next
+  fix x
+  assume \<open>PROP P a\<close> and \<open>x = a\<close>
+  from \<open>x = a\<close> have \<open>x \<equiv> a\<close>
+    by (rule eq_reflection)
+  with \<open>PROP P a\<close> show \<open>PROP P x\<close>
+    by simp
+qed
+
+lemma subst_all':
+  \<open>(\<And>x. a = x \<Longrightarrow> PROP P x) \<equiv> PROP P a\<close>
+proof (rule equal_intr_rule)
+  assume *: \<open>\<And>x. a = x \<Longrightarrow> PROP P x\<close>
+  show \<open>PROP P a\<close>
+    by (rule *) (rule refl)
+next
+  fix x
+  assume \<open>PROP P a\<close> and \<open>a = x\<close>
+  from \<open>a = x\<close> have \<open>a \<equiv> x\<close>
+    by (rule eq_reflection)
+  with \<open>PROP P a\<close> show \<open>PROP P x\<close>
+    by simp
+qed
+
 lemma simp_thms:
   shows not_not: "(\<not> \<not> P) = P"
   and Not_eq_iff: "((\<not> P) = (\<not> Q)) = (P = Q)"
@@ -1372,6 +1402,8 @@
   ex_simps
   all_simps
   simp_thms
+  subst_all
+  subst_all'
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = if_split

--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -91,8 +91,8 @@
 lemma nat_le_dec: "\<And>n::nat. m < n \<or> \<not> (m < n)"
   apply (induct m)
   apply (case_tac n)
-  apply (case_tac [3] n)
-  apply (simp del: simp_thms, iprover?)+
+    apply (case_tac [3] n)
+  apply (simp del: simp_thms subst_all subst_all', iprover?)+
   done
 
 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"

--- a/src/HOL/Transcendental.thy	Wed Jun 03 11:44:21 2020 +0200
+++ b/src/HOL/Transcendental.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -688,7 +688,7 @@
     qed
     then have "\<And>p q.
        \<lbrakk>p < n; q < n - Suc 0\<rbrakk> \<Longrightarrow> norm ((z + h) ^ q * z ^ (n - 2 - q)) \<le> K ^ (n - 2)"
-      by simp
+      by (simp del: subst_all')
     then
     show "norm (\<Sum>p<n - Suc 0. \<Sum>q<n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q)) \<le>
         of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2))"