# HG changeset patch # User nipkow # Date 1547473572 -3600 # Node ID bc758f4f09e56f01a3f4b8909144168a0ce14842 # Parent e61b0b819d288bb01c7df55fad9935dd715cc6b4 uniform naming diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- 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 @@ "(\x. x \ space M =simp=> u x = v x) \ 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 \ (\x. x \ space M \ u x = v x) \ 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 (\i. integral\<^sup>N M (f i))" proof - diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Groups_Big.thy --- 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 \A = B\ by (induct B rule: infinite_finite_induct) auto -lemma cong_strong [cong]: +lemma cong_simp [cong]: "\ A = B; \x. x \ B =simp=> g x = h x \ \ F (\x. g x) A = F (\x. h x) B" by (rule cong) (simp_all add: simp_implies_def) diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Hoare_Parallel/OG_Examples.thy --- 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 \\x=n\" apply oghoare -apply (simp_all cong del: sum.cong_strong) +apply (simp_all cong del: sum.cong_simp) apply (tactic \ALLGOALS (clarify_tac \<^context>)\) -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) diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Library/FSet.thy --- 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]: "\ A = B; \x. x |\| B =simp=> g x = h x \ \ F g A = F h B" unfolding simp_implies_def by (auto cong: cong) diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Number_Theory/Gauss.thy --- 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 diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Probability/Information.thy --- 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 "\ = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\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 "\(\x. (X x, Y x)) = entropy b (count_space (Y ` space M) \\<^sub>M count_space (X ` space M)) (\x. (Y x, X x))" . then show ?thesis unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp diff -r e61b0b819d28 -r bc758f4f09e5 src/HOL/Transcendental.thy --- 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 "\ = (\(i,j) \ (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))" by (simp add: sum.Sigma) also have "\ = (\(j,i) \ (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 "\ = (\ji=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))" by (simp add: sum.Sigma) also have "\ = (x - y) * (\ji=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)