# HG changeset patch
# User haftmann
# Date 1592560007 0
# Node ID ee2c7f0dd1bef01a79acbaa19c4bd8eec41edf96
# Parent  4320875eb8a12c77337f384e8e919a297674a95b
prefer single name

diff -r 4320875eb8a1 -r ee2c7f0dd1be NEWS
--- a/NEWS	Thu Jun 18 09:07:54 2020 +0000
+++ b/NEWS	Fri Jun 19 09:46:47 2020 +0000
@@ -64,15 +64,21 @@
 "bintrunc" and "max_word" are now mere input abbreviations.
 Minor INCOMPATIBILITY.
 
+* Rewrite rule subst_all performs
+more aggressive substitution with variables from assumptions.
+INCOMPATIBILITY, use something like
+"supply subst_all [simp del]"
+to leave fragile proofs unaffected.
+
 
 *** FOL ***
 
 * Added the "at most 1" quantifier, Uniq, as in HOL.
 
-* Simproc defined_all and rewrite rules subst_all and subst_all' perform
+* Simproc defined_all and rewrite rule subst_all perform
 more aggressive substitution with variables from assumptions.
 INCOMPATIBILITY, use something like
-"supply subst_all [simp] subst_all' [simp] [[simproc del: defined_all]]"
+"supply subst_all [simp del] [[simproc del: defined_all]]"
 to leave fragile proofs unaffected.
 
 
diff -r 4320875eb8a1 -r ee2c7f0dd1be src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/FOL/FOL.thy	Fri Jun 19 09:46:47 2020 +0000
@@ -345,7 +345,7 @@
 (*intuitionistic simprules only*)
 val IFOL_ss =
   put_simpset FOL_basic_ss \<^context>
-  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all subst_all'}
+  addsimps @{thms meta_simps IFOL_simps int_ex_simps int_all_simps subst_all}
   addsimprocs [\<^simproc>\<open>defined_All\<close>, \<^simproc>\<open>defined_Ex\<close>]
   |> Simplifier.add_cong @{thm imp_cong}
   |> simpset_of;
diff -r 4320875eb8a1 -r ee2c7f0dd1be src/FOL/IFOL.thy
--- a/src/FOL/IFOL.thy	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/FOL/IFOL.thy	Fri Jun 19 09:46:47 2020 +0000
@@ -829,32 +829,34 @@
 
 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
+proof -
+  show \<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
+  show \<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
 qed
 
 
diff -r 4320875eb8a1 -r ee2c7f0dd1be src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/HOL/HOL.thy	Fri Jun 19 09:46:47 2020 +0000
@@ -943,32 +943,34 @@
 
 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
+proof -
+  show \<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
+  show \<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
 qed
 
 lemma simp_thms:
@@ -1403,7 +1405,6 @@
   all_simps
   simp_thms
   subst_all
-  subst_all'
 
 lemmas [cong] = imp_cong simp_implies_cong
 lemmas [split] = if_split
diff -r 4320875eb8a1 -r ee2c7f0dd1be src/HOL/Proofs/Lambda/NormalForm.thy
--- a/src/HOL/Proofs/Lambda/NormalForm.thy	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy	Fri Jun 19 09:46:47 2020 +0000
@@ -92,7 +92,7 @@
   apply (induct m)
   apply (case_tac n)
     apply (case_tac [3] n)
-  apply (simp del: simp_thms subst_all subst_all', iprover?)+
+  apply (simp del: simp_thms subst_all, iprover?)+
   done
 
 lemma App_NF_D: assumes NF: "NF (Var n \<degree>\<degree> ts)"
diff -r 4320875eb8a1 -r ee2c7f0dd1be src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Jun 18 09:07:54 2020 +0000
+++ b/src/HOL/Transcendental.thy	Fri Jun 19 09:46:47 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 del: subst_all')
+      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))"