uniform naming of strong congruence rules
authornipkow
Sun Oct 21 09:39:09 2018 +0200 (13 months ago ago)
changeset 6916474f1b0f10b2b
parent 69163 6c9453ec2191
child 69165 c360f3b603f8
uniform naming of strong congruence rules
NEWS
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Analysis/Sigma_Algebra.thy
src/HOL/Complete_Lattices.thy
src/HOL/Groups_Big.thy
src/HOL/Hoare_Parallel/OG_Examples.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Number_Theory/Gauss.thy
src/HOL/Probability/Information.thy
src/HOL/Set.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/NEWS	Sun Oct 21 08:19:06 2018 +0200
     1.2 +++ b/NEWS	Sun Oct 21 09:39:09 2018 +0200
     1.3 @@ -43,6 +43,9 @@
     1.4  and prod_mset.swap, similarly to sum.swap and prod.swap.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Strong congruence rules (with =simp=> in the premises) for constant f
     1.8 +are now uniformly called f_cong_strong. 
     1.9 +
    1.10  * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
    1.11  provers, has been updated.
    1.12  
     2.1 --- a/src/HOL/Analysis/Caratheodory.thy	Sun Oct 21 08:19:06 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Sun Oct 21 09:39:09 2018 +0200
     2.3 @@ -737,7 +737,7 @@
     2.4            using f C Ai unfolding bij_betw_def by auto
     2.5          then have "\<Union>range f = A i"
     2.6            using f C Ai unfolding bij_betw_def
     2.7 -            by (auto simp add: f_def cong del: strong_SUP_cong)
     2.8 +            by (auto simp add: f_def cong del: SUP_cong_strong)
     2.9          moreover
    2.10          { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
    2.11              using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
     3.1 --- a/src/HOL/Analysis/L2_Norm.thy	Sun Oct 21 08:19:06 2018 +0200
     3.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Sun Oct 21 09:39:09 2018 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
     3.5    unfolding L2_set_def by simp
     3.6  
     3.7 -lemma strong_L2_set_cong:
     3.8 +lemma L2_set_cong_strong:
     3.9    "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
    3.10    unfolding L2_set_def simp_implies_def by simp
    3.11  
     4.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Oct 21 08:19:06 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Sun Oct 21 09:39:09 2018 +0200
     4.3 @@ -2589,7 +2589,7 @@
     4.4        using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
     4.5    next
     4.6      show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
     4.7 -      using A by (auto cong del: strong_SUP_cong)
     4.8 +      using A by (auto cong del: SUP_cong_strong)
     4.9    next
    4.10      fix i
    4.11      have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
     5.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Oct 21 08:19:06 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Oct 21 09:39:09 2018 +0200
     5.3 @@ -2055,7 +2055,7 @@
     5.4        by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
     5.5    qed
     5.6    then show ?thesis
     5.7 -    unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong)
     5.8 +    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_strong)
     5.9  qed
    5.10  
    5.11  lemma nn_integral_count_space_indicator:
     6.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Sun Oct 21 08:19:06 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Oct 21 09:39:09 2018 +0200
     6.3 @@ -436,10 +436,10 @@
     6.4    by (auto simp add: binary_def)
     6.5  
     6.6  lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
     6.7 -  by (simp add: range_binary_eq cong del: strong_SUP_cong)
     6.8 +  by (simp add: range_binary_eq cong del: SUP_cong_strong)
     6.9  
    6.10  lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
    6.11 -  by (simp add: range_binary_eq cong del: strong_INF_cong)
    6.12 +  by (simp add: range_binary_eq cong del: INF_cong_strong)
    6.13  
    6.14  lemma sigma_algebra_iff2:
    6.15       "sigma_algebra \<Omega> M \<longleftrightarrow>
    6.16 @@ -943,7 +943,7 @@
    6.17    done
    6.18  
    6.19  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
    6.20 -  by (simp add: range_binaryset_eq cong del: strong_SUP_cong)
    6.21 +  by (simp add: range_binaryset_eq cong del: SUP_cong_strong)
    6.22  
    6.23  subsubsection \<open>Closed CDI\<close>
    6.24  
     7.1 --- a/src/HOL/Complete_Lattices.thy	Sun Oct 21 08:19:06 2018 +0200
     7.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Oct 21 09:39:09 2018 +0200
     7.3 @@ -73,7 +73,7 @@
     7.4  lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
     7.5    by (simp add: image_def)
     7.6  
     7.7 -lemma strong_INF_cong [cong]:
     7.8 +lemma INF_cong_strong [cong]:
     7.9    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
    7.10    unfolding simp_implies_def by (fact INF_cong)
    7.11  
    7.12 @@ -83,20 +83,20 @@
    7.13  begin
    7.14  
    7.15  lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
    7.16 -  by (simp add: image_comp)
    7.17 +by(fact Inf.INF_image)
    7.18  
    7.19  lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
    7.20 -  by simp
    7.21 +by(fact Inf.INF_identity_eq)
    7.22  
    7.23  lemma SUP_id_eq [simp]: "\<Squnion>(id ` A) = \<Squnion>A"
    7.24 -  by (simp add: id_def)
    7.25 +by(fact Inf.INF_id_eq)
    7.26  
    7.27  lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
    7.28 -  by (simp add: image_def)
    7.29 +by (fact Inf.INF_cong)
    7.30  
    7.31 -lemma strong_SUP_cong [cong]:
    7.32 +lemma SUP_cong_strong [cong]:
    7.33    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
    7.34 -  unfolding simp_implies_def by (fact SUP_cong)
    7.35 +by (fact Inf.INF_cong_strong)
    7.36  
    7.37  end
    7.38  
    7.39 @@ -191,19 +191,19 @@
    7.40    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    7.41  
    7.42  lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
    7.43 -  by (simp cong del: strong_INF_cong)
    7.44 +  by (simp cong del: INF_cong_strong)
    7.45  
    7.46  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    7.47    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    7.48  
    7.49  lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
    7.50 -  by (simp cong del: strong_SUP_cong)
    7.51 +  by (simp cong del: SUP_cong_strong)
    7.52  
    7.53  lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
    7.54 -  by (simp cong del: strong_INF_cong)
    7.55 +  by (simp cong del: INF_cong_strong)
    7.56  
    7.57  lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
    7.58 -  by (simp cong del: strong_SUP_cong)
    7.59 +  by (simp cong del: SUP_cong_strong)
    7.60  
    7.61  lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
    7.62    by (auto intro!: antisym Inf_lower)
    7.63 @@ -449,11 +449,11 @@
    7.64  
    7.65  lemma INF_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f i \<le> c) \<Longrightarrow> \<Sqinter>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    7.66    using INF_eq_const [of I f c] INF_lower [of _ I f]
    7.67 -  by (auto intro: antisym cong del: strong_INF_cong)
    7.68 +  by (auto intro: antisym cong del: INF_cong_strong)
    7.69  
    7.70  lemma SUP_eq_iff: "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> c \<le> f i) \<Longrightarrow> \<Squnion>(f ` I) = c \<longleftrightarrow> (\<forall>i\<in>I. f i = c)"
    7.71    using SUP_eq_const [of I f c] SUP_upper [of _ I f]
    7.72 -  by (auto intro: antisym cong del: strong_SUP_cong)
    7.73 +  by (auto intro: antisym cong del: SUP_cong_strong)
    7.74  
    7.75  end
    7.76  
     8.1 --- a/src/HOL/Groups_Big.thy	Sun Oct 21 08:19:06 2018 +0200
     8.2 +++ b/src/HOL/Groups_Big.thy	Sun Oct 21 09:39:09 2018 +0200
     8.3 @@ -147,10 +147,9 @@
     8.4    using g_h unfolding \<open>A = B\<close>
     8.5    by (induct B rule: infinite_finite_induct) auto
     8.6  
     8.7 -lemma strong_cong [cong]:
     8.8 -  assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
     8.9 -  shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
    8.10 -  by (rule cong) (use assms in \<open>simp_all add: simp_implies_def\<close>)
    8.11 +lemma cong_strong [cong]:
    8.12 +  "\<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"
    8.13 +by (rule cong) (simp_all add: simp_implies_def)
    8.14  
    8.15  lemma reindex_cong:
    8.16    assumes "inj_on l B"
     9.1 --- a/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Oct 21 08:19:06 2018 +0200
     9.2 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy	Sun Oct 21 09:39:09 2018 +0200
     9.3 @@ -534,9 +534,9 @@
     9.4   COEND
     9.5   \<lbrace>\<acute>x=n\<rbrace>"
     9.6  apply oghoare
     9.7 -apply (simp_all cong del: sum.strong_cong)
     9.8 +apply (simp_all cong del: sum.cong_strong)
     9.9  apply (tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
    9.10 -apply (simp_all cong del: sum.strong_cong)
    9.11 +apply (simp_all cong del: sum.cong_strong)
    9.12     apply(erule (1) Example2_lemma2)
    9.13    apply(erule (1) Example2_lemma2)
    9.14   apply(erule (1) Example2_lemma2)
    10.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Oct 21 08:19:06 2018 +0200
    10.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Oct 21 09:39:09 2018 +0200
    10.3 @@ -321,7 +321,7 @@
    10.4        \<lbrace>\<forall>i<n. (\<acute>X!i) mod n=i \<and> (\<forall>j<\<acute>X!i. j mod n=i \<longrightarrow> \<not>P(B!j)) \<and>
    10.5          (\<acute>Y!i<m \<longrightarrow> P(B!(\<acute>Y!i)) \<and> \<acute>Y!i\<le> m+i) \<and> (\<exists>j<n. \<acute>Y!j \<le> \<acute>X!i)\<rbrace>]"
    10.6  apply (rule Parallel)
    10.7 -apply (auto cong del: strong_INF_cong strong_SUP_cong)
    10.8 +apply (auto cong del: INF_cong_strong SUP_cong_strong)
    10.9  apply force
   10.10  apply (rule While)
   10.11      apply force
    11.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Oct 21 08:19:06 2018 +0200
    11.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Oct 21 09:39:09 2018 +0200
    11.3 @@ -188,7 +188,7 @@
    11.4  proof(cases "Y = {}")
    11.5    case True
    11.6    then show ?thesis
    11.7 -    by (simp add: image_constant_conv cong del: strong_SUP_cong)
    11.8 +    by (simp add: image_constant_conv cong del: SUP_cong_strong)
    11.9  next
   11.10    case False
   11.11    have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f ` Y)"
   11.12 @@ -518,7 +518,7 @@
   11.13  context ccpo begin
   11.14  
   11.15  lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
   11.16 -by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong)
   11.17 +by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_strong)
   11.18  
   11.19  lemma mcont_const [cont_intro, simp]:
   11.20    "mcont luba orda Sup (\<le>) (\<lambda>x. c)"
   11.21 @@ -695,7 +695,7 @@
   11.22      hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
   11.23      moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
   11.24      ultimately show ?thesis using True Y
   11.25 -      by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong)
   11.26 +      by (auto simp add: image_constant_conv cong del: c.SUP_cong_strong)
   11.27    next
   11.28      case False
   11.29      let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
    12.1 --- a/src/HOL/Library/FSet.thy	Sun Oct 21 08:19:06 2018 +0200
    12.2 +++ b/src/HOL/Library/FSet.thy	Sun Oct 21 09:39:09 2018 +0200
    12.3 @@ -755,10 +755,9 @@
    12.4  
    12.5  lemmas cong[fundef_cong] = set.cong[Transfer.transferred]
    12.6  
    12.7 -lemma strong_cong[cong]:
    12.8 -  assumes "A = B" "\<And>x. x |\<in>| B =simp=> g x = h x"
    12.9 -  shows "F g A = F h B"
   12.10 -using assms unfolding simp_implies_def by (auto cong: cong)
   12.11 +lemma cong_strong[cong]:
   12.12 +  "\<lbrakk> A = B;  \<And>x. x |\<in>| B =simp=> g x = h x \<rbrakk> \<Longrightarrow> F g A = F h B"
   12.13 +unfolding simp_implies_def by (auto cong: cong)
   12.14  
   12.15  end
   12.16  
    13.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 21 08:19:06 2018 +0200
    13.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Oct 21 09:39:09 2018 +0200
    13.3 @@ -62,16 +62,11 @@
    13.4    "\<not> finite {a. g a \<noteq> \<^bold>1} \<Longrightarrow> G g = \<^bold>1"
    13.5    by (simp add: expand_set)
    13.6  
    13.7 -lemma cong:
    13.8 +lemma cong [cong]:
    13.9    assumes "\<And>a. g a = h a"
   13.10    shows "G g = G h"
   13.11    using assms by (simp add: expand_set)
   13.12  
   13.13 -lemma strong_cong [cong]:
   13.14 -  assumes "\<And>a. g a = h a"
   13.15 -  shows "G (\<lambda>a. g a) = G (\<lambda>a. h a)"
   13.16 -  using assms by (fact cong)
   13.17 -
   13.18  lemma not_neutral_obtains_not_neutral:
   13.19    assumes "G g \<noteq> \<^bold>1"
   13.20    obtains a where "g a \<noteq> \<^bold>1"
   13.21 @@ -202,7 +197,7 @@
   13.22    have "(\<lambda>b. if a = b then g b else \<^bold>1) = (\<lambda>b. if b = a then g b else \<^bold>1)"
   13.23      by (simp add: fun_eq_iff)
   13.24    then have "G (\<lambda>b. if a = b then g b else \<^bold>1) = G (\<lambda>b. if b = a then g b else \<^bold>1)"
   13.25 -    by (simp cong del: strong_cong)
   13.26 +    by (simp cong del: cong)
   13.27    then show ?thesis by simp
   13.28  qed
   13.29  
    14.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Oct 21 08:19:06 2018 +0200
    14.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Oct 21 09:39:09 2018 +0200
    14.3 @@ -339,7 +339,7 @@
    14.4  theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
    14.5  proof -
    14.6    have "[prod id A = prod id F * prod id D](mod p)"
    14.7 -    by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.strong_cong)
    14.8 +    by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_strong)
    14.9    then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
   14.10      by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
   14.11    then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
   14.12 @@ -364,7 +364,7 @@
   14.13        (-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
   14.14      by (rule cong_trans) (simp add: a ac_simps)
   14.15    then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
   14.16 -    by (rule cong_trans) (simp add: aux cong del: prod.strong_cong)
   14.17 +    by (rule cong_trans) (simp add: aux cong del: prod.cong_strong)
   14.18    with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
   14.19      by (metis cong_mult_lcancel)
   14.20    then show ?thesis
    15.1 --- a/src/HOL/Probability/Information.thy	Sun Oct 21 08:19:06 2018 +0200
    15.2 +++ b/src/HOL/Probability/Information.thy	Sun Oct 21 09:39:09 2018 +0200
    15.3 @@ -1913,7 +1913,7 @@
    15.4    also have "\<dots> = entropy b (count_space (Y ` space M) \<Otimes>\<^sub>M count_space (X ` space M)) (\<lambda>x. (Y x, X x))"
    15.5      by (subst entropy_distr[OF simple_distributed_joint[OF YX]])
    15.6         (auto simp: pair_measure_count_space sigma_finite_measure_count_space_finite lebesgue_integral_count_space_finite
    15.7 -             cong del: sum.strong_cong  intro!: sum.mono_neutral_left measure_nonneg)
    15.8 +             cong del: sum.cong_strong intro!: sum.mono_neutral_left measure_nonneg)
    15.9    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))" .
   15.10    then show ?thesis
   15.11      unfolding conditional_entropy_eq_entropy_simple[OF Y X] by simp
    16.1 --- a/src/HOL/Set.thy	Sun Oct 21 08:19:06 2018 +0200
    16.2 +++ b/src/HOL/Set.thy	Sun Oct 21 09:39:09 2018 +0200
    16.3 @@ -422,24 +422,24 @@
    16.4  text \<open>Congruence rules\<close>
    16.5  
    16.6  lemma ball_cong:
    16.7 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow>
    16.8 +  "\<lbrakk> A = B;  \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
    16.9      (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
   16.10 -  by (simp add: Ball_def)
   16.11 -
   16.12 -lemma strong_ball_cong [cong]:
   16.13 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x) \<Longrightarrow>
   16.14 +by (simp add: Ball_def)
   16.15 +
   16.16 +lemma ball_cong_strong [cong]:
   16.17 +  "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
   16.18      (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
   16.19 -  by (simp add: simp_implies_def Ball_def)
   16.20 +by (simp add: simp_implies_def Ball_def)
   16.21  
   16.22  lemma bex_cong:
   16.23 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow>
   16.24 +  "\<lbrakk> A = B;  \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
   16.25      (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
   16.26 -  by (simp add: Bex_def cong: conj_cong)
   16.27 -
   16.28 -lemma strong_bex_cong [cong]:
   16.29 -  "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x) \<Longrightarrow>
   16.30 +by (simp add: Bex_def cong: conj_cong)
   16.31 +
   16.32 +lemma bex_cong_strong [cong]:
   16.33 +  "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
   16.34      (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
   16.35 -  by (simp add: simp_implies_def Bex_def cong: conj_cong)
   16.36 +by (simp add: simp_implies_def Bex_def cong: conj_cong)
   16.37  
   16.38  lemma bex1_def: "(\<exists>!x\<in>X. P x) \<longleftrightarrow> (\<exists>x\<in>X. P x) \<and> (\<forall>x\<in>X. \<forall>y\<in>X. P x \<longrightarrow> P y \<longrightarrow> x = y)"
   16.39    by auto
    17.1 --- a/src/HOL/Topological_Spaces.thy	Sun Oct 21 08:19:06 2018 +0200
    17.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Oct 21 09:39:09 2018 +0200
    17.3 @@ -1882,7 +1882,7 @@
    17.4    unfolding continuous_on_def
    17.5    by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
    17.6  
    17.7 -lemma continuous_on_strong_cong:
    17.8 +lemma continuous_on_cong_strong:
    17.9    "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
   17.10    unfolding simp_implies_def by (rule continuous_on_cong)
   17.11  
    18.1 --- a/src/HOL/Transcendental.thy	Sun Oct 21 08:19:06 2018 +0200
    18.2 +++ b/src/HOL/Transcendental.thy	Sun Oct 21 09:39:09 2018 +0200
    18.3 @@ -6088,7 +6088,7 @@
    18.4    also have "\<dots> = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
    18.5      by (simp add: sum.Sigma)
    18.6    also have "\<dots> = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
    18.7 -    by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.strong_cong)
    18.8 +    by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
    18.9    also have "\<dots> = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
   18.10      by (simp add: sum.Sigma)
   18.11    also have "\<dots> = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
   18.12 @@ -6110,7 +6110,7 @@
   18.13        apply (rule_tac x="x + Suc j" in image_eqI, auto)
   18.14        done
   18.15      then show ?thesis
   18.16 -      by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.strong_cong)
   18.17 +      by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
   18.18    qed
   18.19    then show ?thesis
   18.20      by (simp add: polyfun_diff [OF assms] sum_distrib_right)