--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Mon Jan 14 14:46:12 2019 +0100
@@ -900,10 +900,6 @@
"(\<And>x. x \<in> space M =simp=> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N M v"
by (auto intro: nn_integral_cong simp: simp_implies_def)
-lemma nn_integral_cong_strong:
- "M = N \<Longrightarrow> (\<And>x. x \<in> space M \<Longrightarrow> u x = v x) \<Longrightarrow> integral\<^sup>N M u = integral\<^sup>N N v"
- by (auto intro: nn_integral_cong)
-
lemma incseq_nn_integral:
assumes "incseq f" shows "incseq (\<lambda>i. integral\<^sup>N M (f i))"
proof -
--- a/src/HOL/Groups_Big.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Groups_Big.thy Mon Jan 14 14:46:12 2019 +0100
@@ -147,7 +147,7 @@
using g_h unfolding \<open>A = B\<close>
by (induct B rule: infinite_finite_induct) auto
-lemma cong_strong [cong]:
+lemma cong_simp [cong]:
"\<lbrakk> A = B; \<And>x. x \<in> B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
by (rule cong) (simp_all add: simp_implies_def)
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Mon Jan 14 14:46:12 2019 +0100
@@ -534,9 +534,9 @@
COEND
\<lbrace>\<acute>x=n\<rbrace>"
apply oghoare
-apply (simp_all cong del: sum.cong_strong)
+apply (simp_all cong del: sum.cong_simp)
apply (tactic \<open>ALLGOALS (clarify_tac \<^context>)\<close>)
-apply (simp_all cong del: sum.cong_strong)
+apply (simp_all cong del: sum.cong_simp)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
--- a/src/HOL/Library/FSet.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Library/FSet.thy Mon Jan 14 14:46:12 2019 +0100
@@ -755,7 +755,7 @@
lemmas cong[fundef_cong] = set.cong[Transfer.transferred]
-lemma cong_strong[cong]:
+lemma cong_simp[cong]:
"\<lbrakk> A = B; \<And>x. x |\<in>| B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F g A = F h B"
unfolding simp_implies_def by (auto cong: cong)
--- a/src/HOL/Number_Theory/Gauss.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy Mon Jan 14 14:46:12 2019 +0100
@@ -339,7 +339,7 @@
theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[prod id A = prod id F * prod id D](mod p)"
- by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_strong)
+ by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_simp)
then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
@@ -364,7 +364,7 @@
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
by (rule cong_trans) (simp add: a ac_simps)
then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
- by (rule cong_trans) (simp add: aux cong del: prod.cong_strong)
+ by (rule cong_trans) (simp add: aux cong del: prod.cong_simp)
with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (metis cong_mult_lcancel)
then show ?thesis
--- a/src/HOL/Probability/Information.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Probability/Information.thy Mon Jan 14 14:46:12 2019 +0100
@@ -1913,7 +1913,7 @@
also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
(auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
- cong del: sum.cong_strong intro!: sum.mono_neutral_left measure_nonneg)
+ cong del: sum.cong_simp intro!: sum.mono_neutral_left measure_nonneg)
finally have "\<H>(\<lambda>x. (X x, Y x)) = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))" .
then show ?thesis
unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
--- a/src/HOL/Transcendental.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Transcendental.thy Mon Jan 14 14:46:12 2019 +0100
@@ -6088,7 +6088,7 @@
also have "\<dots> = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
by (simp add: sum.Sigma)
also have "\<dots> = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
- by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
also have "\<dots> = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
by (simp add: sum.Sigma)
also have "\<dots> = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
@@ -6110,7 +6110,7 @@
apply (rule_tac x="x + Suc j" in image_eqI, auto)
done
then show ?thesis
- by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_simp)
qed
then show ?thesis
by (simp add: polyfun_diff [OF assms] sum_distrib_right)