--- 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.
--- 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;
--- 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
--- 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
--- 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)"
--- 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))"