prefer naming convention from datatype package for strong congruence rules
authorhaftmann
Sun Dec 30 10:34:56 2018 +0000 (8 months ago)
changeset 6954627dae626822b
parent 69545 4aed40ecfb43
child 69552 b85f4c5cb588
prefer naming convention from datatype package for strong congruence rules
NEWS
src/HOL/Analysis/Bochner_Integration.thy
src/HOL/Analysis/Caratheodory.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Lebesgue_Measure.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/Data_Structures/Braun_Tree.thy
src/HOL/Hoare_Parallel/RG_Examples.thy
src/HOL/Library/Complete_Partial_Order2.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Set.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/NEWS	Sun Dec 30 10:34:56 2018 +0000
     1.2 +++ b/NEWS	Sun Dec 30 10:34:56 2018 +0000
     1.3 @@ -84,7 +84,8 @@
     1.4  INCOMPATIBILITY.
     1.5  
     1.6  * Strong congruence rules (with =simp=> in the premises) for constant f
     1.7 -are now uniformly called f_cong_strong. 
     1.8 +are now uniformly called f_cong_simp, in accordance with congruence
     1.9 +rules produced for mappers by the datatype package. INCOMPATIBILITY.
    1.10  
    1.11  * Sledgehammer: The URL for SystemOnTPTP, which is used by remote
    1.12  provers, has been updated.
     2.1 --- a/src/HOL/Analysis/Bochner_Integration.thy	Sun Dec 30 10:34:56 2018 +0000
     2.2 +++ b/src/HOL/Analysis/Bochner_Integration.thy	Sun Dec 30 10:34:56 2018 +0000
     2.3 @@ -524,7 +524,7 @@
     2.4    assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
     2.5    shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
     2.6    unfolding has_bochner_integral.simps assms(1,3)
     2.7 -  using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
     2.8 +  using assms(2) by (simp cong: measurable_cong_simp nn_integral_cong_simp)
     2.9  
    2.10  lemma%unimportant has_bochner_integral_cong_AE:
    2.11    "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
     3.1 --- a/src/HOL/Analysis/Caratheodory.thy	Sun Dec 30 10:34:56 2018 +0000
     3.2 +++ b/src/HOL/Analysis/Caratheodory.thy	Sun Dec 30 10:34:56 2018 +0000
     3.3 @@ -737,7 +737,7 @@
     3.4            using f C Ai unfolding bij_betw_def by auto
     3.5          then have "\<Union>range f = A i"
     3.6            using f C Ai unfolding bij_betw_def
     3.7 -            by (auto simp add: f_def cong del: SUP_cong_strong)
     3.8 +            by (auto simp add: f_def cong del: SUP_cong_simp)
     3.9          moreover
    3.10          { have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
    3.11              using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
     4.1 --- a/src/HOL/Analysis/L2_Norm.thy	Sun Dec 30 10:34:56 2018 +0000
     4.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Sun Dec 30 10:34:56 2018 +0000
     4.3 @@ -14,7 +14,7 @@
     4.4    "\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
     4.5    unfolding L2_set_def by simp
     4.6  
     4.7 -lemma L2_set_cong_strong:
     4.8 +lemma L2_set_cong_simp:
     4.9    "\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
    4.10    unfolding L2_set_def simp_implies_def by simp
    4.11  
     5.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Dec 30 10:34:56 2018 +0000
     5.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Dec 30 10:34:56 2018 +0000
     5.3 @@ -407,7 +407,7 @@
     5.4  lemma measurable_lebesgue_cong:
     5.5    assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
     5.6    shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
     5.7 -  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
     5.8 +  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
     5.9  
    5.10  text%unimportant \<open>Measurability of continuous functions\<close>
    5.11  
     6.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Dec 30 10:34:56 2018 +0000
     6.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Sun Dec 30 10:34:56 2018 +0000
     6.3 @@ -1143,7 +1143,7 @@
     6.4    "(\<And>x. x \<in> space M \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in M. Q x)"
     6.5    by auto
     6.6  
     6.7 -lemma AE_cong_strong: "M = N \<Longrightarrow> (\<And>x. x \<in> space N =simp=> P x = Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in N. Q x)"
     6.8 +lemma AE_cong_simp: "M = N \<Longrightarrow> (\<And>x. x \<in> space N =simp=> P x = Q x) \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> (AE x in N. Q x)"
     6.9    by (auto simp: simp_implies_def)
    6.10  
    6.11  lemma AE_all_countable:
    6.12 @@ -2589,7 +2589,7 @@
    6.13        using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
    6.14    next
    6.15      show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
    6.16 -      using A by (auto cong del: SUP_cong_strong)
    6.17 +      using A by (auto cong del: SUP_cong_simp)
    6.18    next
    6.19      fix i
    6.20      have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
     7.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Dec 30 10:34:56 2018 +0000
     7.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Dec 30 10:34:56 2018 +0000
     7.3 @@ -2058,7 +2058,7 @@
     7.4        by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
     7.5    qed
     7.6    then show ?thesis
     7.7 -    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_strong)
     7.8 +    unfolding nn_integral_def_finite by (simp cong del: SUP_cong_simp)
     7.9  qed
    7.10  
    7.11  lemma nn_integral_count_space_indicator:
     8.1 --- a/src/HOL/Analysis/Sigma_Algebra.thy	Sun Dec 30 10:34:56 2018 +0000
     8.2 +++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Dec 30 10:34:56 2018 +0000
     8.3 @@ -436,10 +436,10 @@
     8.4    by (auto simp add: binary_def)
     8.5  
     8.6  lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
     8.7 -  by (simp add: range_binary_eq cong del: SUP_cong_strong)
     8.8 +  by (simp add: range_binary_eq cong del: SUP_cong_simp)
     8.9  
    8.10  lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
    8.11 -  by (simp add: range_binary_eq cong del: INF_cong_strong)
    8.12 +  by (simp add: range_binary_eq cong del: INF_cong_simp)
    8.13  
    8.14  lemma sigma_algebra_iff2:
    8.15       "sigma_algebra \<Omega> M \<longleftrightarrow>
    8.16 @@ -943,7 +943,7 @@
    8.17    done
    8.18  
    8.19  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
    8.20 -  by (simp add: range_binaryset_eq cong del: SUP_cong_strong)
    8.21 +  by (simp add: range_binaryset_eq cong del: SUP_cong_simp)
    8.22  
    8.23  subsubsection \<open>Closed CDI\<close>
    8.24  
    8.25 @@ -1802,7 +1802,7 @@
    8.26    unfolding measurable_def using assms
    8.27    by (simp cong: vimage_inter_cong Pi_cong add: simp_implies_def)
    8.28  
    8.29 -lemma measurable_cong_strong:
    8.30 +lemma measurable_cong_simp:
    8.31    "M = N \<Longrightarrow> M' = N' \<Longrightarrow> (\<And>w. w \<in> space M \<Longrightarrow> f w = g w) \<Longrightarrow>
    8.32      f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
    8.33    by (metis measurable_cong)
     9.1 --- a/src/HOL/Complete_Lattices.thy	Sun Dec 30 10:34:56 2018 +0000
     9.2 +++ b/src/HOL/Complete_Lattices.thy	Sun Dec 30 10:34:56 2018 +0000
     9.3 @@ -61,7 +61,7 @@
     9.4  lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
     9.5    by (simp add: image_def)
     9.6  
     9.7 -lemma INF_cong_strong [cong]:
     9.8 +lemma INF_cong_simp [cong]:
     9.9    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
    9.10    unfolding simp_implies_def by (fact INF_cong)
    9.11  
    9.12 @@ -82,9 +82,9 @@
    9.13  lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
    9.14  by (fact Inf.INF_cong)
    9.15  
    9.16 -lemma SUP_cong_strong [cong]:
    9.17 +lemma SUP_cong_simp [cong]:
    9.18    "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
    9.19 -by (fact Inf.INF_cong_strong)
    9.20 +by (fact Inf.INF_cong_simp)
    9.21  
    9.22  end
    9.23  
    9.24 @@ -179,19 +179,19 @@
    9.25    by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
    9.26  
    9.27  lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
    9.28 -  by (simp cong del: INF_cong_strong)
    9.29 +  by (simp cong del: INF_cong_simp)
    9.30  
    9.31  lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
    9.32    by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
    9.33  
    9.34  lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
    9.35 -  by (simp cong del: SUP_cong_strong)
    9.36 +  by (simp cong del: SUP_cong_simp)
    9.37  
    9.38  lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
    9.39 -  by (simp cong del: INF_cong_strong)
    9.40 +  by (simp cong del: INF_cong_simp)
    9.41  
    9.42  lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
    9.43 -  by (simp cong del: SUP_cong_strong)
    9.44 +  by (simp cong del: SUP_cong_simp)
    9.45  
    9.46  lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
    9.47    by (auto intro!: antisym Inf_lower)
    9.48 @@ -437,11 +437,11 @@
    9.49  
    9.50  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)"
    9.51    using INF_eq_const [of I f c] INF_lower [of _ I f]
    9.52 -  by (auto intro: antisym cong del: INF_cong_strong)
    9.53 +  by (auto intro: antisym cong del: INF_cong_simp)
    9.54  
    9.55  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)"
    9.56    using SUP_eq_const [of I f c] SUP_upper [of _ I f]
    9.57 -  by (auto intro: antisym cong del: SUP_cong_strong)
    9.58 +  by (auto intro: antisym cong del: SUP_cong_simp)
    9.59  
    9.60  end
    9.61  
    10.1 --- a/src/HOL/Data_Structures/Braun_Tree.thy	Sun Dec 30 10:34:56 2018 +0000
    10.2 +++ b/src/HOL/Data_Structures/Braun_Tree.thy	Sun Dec 30 10:34:56 2018 +0000
    10.3 @@ -252,7 +252,7 @@
    10.4      by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1)
    10.5    thus ?case using Node.IH even_odd_decomp[OF _ _ 3]
    10.6      by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp
    10.7 -           cong: image_cong_strong)
    10.8 +           cong: image_cong_simp)
    10.9  qed
   10.10  
   10.11  lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}"
    11.1 --- a/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Dec 30 10:34:56 2018 +0000
    11.2 +++ b/src/HOL/Hoare_Parallel/RG_Examples.thy	Sun Dec 30 10:34:56 2018 +0000
    11.3 @@ -321,7 +321,7 @@
    11.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>
    11.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>]"
    11.6  apply (rule Parallel)
    11.7 -apply (auto cong del: INF_cong_strong SUP_cong_strong)
    11.8 +apply (auto cong del: INF_cong_simp SUP_cong_simp)
    11.9  apply force
   11.10  apply (rule While)
   11.11      apply force
    12.1 --- a/src/HOL/Library/Complete_Partial_Order2.thy	Sun Dec 30 10:34:56 2018 +0000
    12.2 +++ b/src/HOL/Library/Complete_Partial_Order2.thy	Sun Dec 30 10:34:56 2018 +0000
    12.3 @@ -188,7 +188,7 @@
    12.4  proof(cases "Y = {}")
    12.5    case True
    12.6    then show ?thesis
    12.7 -    by (simp add: image_constant_conv cong del: SUP_cong_strong)
    12.8 +    by (simp add: image_constant_conv cong del: SUP_cong_simp)
    12.9  next
   12.10    case False
   12.11    have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f ` Y)"
   12.12 @@ -518,7 +518,7 @@
   12.13  context ccpo begin
   12.14  
   12.15  lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
   12.16 -by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_strong)
   12.17 +by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
   12.18  
   12.19  lemma mcont_const [cont_intro, simp]:
   12.20    "mcont luba orda Sup (\<le>) (\<lambda>x. c)"
   12.21 @@ -695,7 +695,7 @@
   12.22      hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
   12.23      moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
   12.24      ultimately show ?thesis using True Y
   12.25 -      by (auto simp add: image_constant_conv cong del: c.SUP_cong_strong)
   12.26 +      by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
   12.27    next
   12.28      case False
   12.29      let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
    13.1 --- a/src/HOL/Probability/Giry_Monad.thy	Sun Dec 30 10:34:56 2018 +0000
    13.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Sun Dec 30 10:34:56 2018 +0000
    13.3 @@ -1763,7 +1763,7 @@
    13.4    qed
    13.5  qed
    13.6  
    13.7 -lemma bind_cong_strong: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
    13.8 +lemma bind_cong_simp: "M = N \<Longrightarrow> (\<And>x. x\<in>space M =simp=> f x = g x) \<Longrightarrow> bind M f = bind N g"
    13.9    by (auto simp: simp_implies_def intro!: bind_cong)
   13.10  
   13.11  lemma sets_bind_measurable:
    14.1 --- a/src/HOL/Set.thy	Sun Dec 30 10:34:56 2018 +0000
    14.2 +++ b/src/HOL/Set.thy	Sun Dec 30 10:34:56 2018 +0000
    14.3 @@ -426,7 +426,7 @@
    14.4      (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
    14.5  by (simp add: Ball_def)
    14.6  
    14.7 -lemma ball_cong_strong [cong]:
    14.8 +lemma ball_cong_simp [cong]:
    14.9    "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
   14.10      (\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
   14.11  by (simp add: simp_implies_def Ball_def)
   14.12 @@ -436,7 +436,7 @@
   14.13      (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
   14.14  by (simp add: Bex_def cong: conj_cong)
   14.15  
   14.16 -lemma bex_cong_strong [cong]:
   14.17 +lemma bex_cong_simp [cong]:
   14.18    "\<lbrakk> A = B;  \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
   14.19      (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
   14.20  by (simp add: simp_implies_def Bex_def cong: conj_cong)
   14.21 @@ -939,7 +939,7 @@
   14.22  lemma image_cong: "\<lbrakk> M = N;  \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
   14.23  by (simp add: image_def)
   14.24  
   14.25 -lemma image_cong_strong: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
   14.26 +lemma image_cong_simp: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
   14.27  by (simp add: image_def simp_implies_def)
   14.28  
   14.29  lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
    15.1 --- a/src/HOL/Topological_Spaces.thy	Sun Dec 30 10:34:56 2018 +0000
    15.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Dec 30 10:34:56 2018 +0000
    15.3 @@ -1882,7 +1882,7 @@
    15.4    unfolding continuous_on_def
    15.5    by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
    15.6  
    15.7 -lemma continuous_on_cong_strong:
    15.8 +lemma continuous_on_cong_simp:
    15.9    "s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
   15.10    unfolding simp_implies_def by (rule continuous_on_cong)
   15.11