--- a/NEWS Sun Oct 21 08:19:06 2018 +0200
+++ b/NEWS Sun Oct 21 09:39:09 2018 +0200
@@ -43,6 +43,9 @@
and prod_mset.swap, similarly to sum.swap and prod.swap.
INCOMPATIBILITY.
+* Strong congruence rules (with =simp=> in the premises) for constant f
+are now uniformly called f_cong_strong.
+
* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
provers, has been updated.
--- a/src/HOL/Analysis/Caratheodory.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Analysis/Caratheodory.thy Sun Oct 21 09:39:09 2018 +0200
@@ -737,7 +737,7 @@
using f C Ai unfolding bij_betw_def by auto
then have "\<Union>range f = A i"
using f C Ai unfolding bij_betw_def
- by (auto simp add: f_def cong del: strong_SUP_cong)
+ by (auto simp add: f_def cong del: SUP_cong_strong)
moreover
{ have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)"
using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def)
--- a/src/HOL/Analysis/L2_Norm.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Analysis/L2_Norm.thy Sun Oct 21 09:39:09 2018 +0200
@@ -14,7 +14,7 @@
"\<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
unfolding L2_set_def by simp
-lemma strong_L2_set_cong:
+lemma L2_set_cong_strong:
"\<lbrakk>A = B; \<And>x. x \<in> B =simp=> f x = g x\<rbrakk> \<Longrightarrow> L2_set f A = L2_set g B"
unfolding L2_set_def simp_implies_def by simp
--- a/src/HOL/Analysis/Measure_Space.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Oct 21 09:39:09 2018 +0200
@@ -2589,7 +2589,7 @@
using E \<Omega> by (subst (1 2) emeasure_restrict_space) (auto simp: sets_eq sets_eq[THEN sets_eq_imp_space_eq])
next
show "range (from_nat_into A) \<subseteq> E" "(\<Union>i. from_nat_into A i) = \<Omega>"
- using A by (auto cong del: strong_SUP_cong)
+ using A by (auto cong del: SUP_cong_strong)
next
fix i
have "emeasure (restrict_space M \<Omega>) (from_nat_into A i) = emeasure M (from_nat_into A i)"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Oct 21 09:39:09 2018 +0200
@@ -2055,7 +2055,7 @@
by (subst s_eq) (auto simp: image_subset_iff le_fun_def split: split_indicator split_indicator_asm)
qed
then show ?thesis
- unfolding nn_integral_def_finite by (simp cong del: strong_SUP_cong)
+ unfolding nn_integral_def_finite by (simp cong del: SUP_cong_strong)
qed
lemma nn_integral_count_space_indicator:
--- a/src/HOL/Analysis/Sigma_Algebra.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Sun Oct 21 09:39:09 2018 +0200
@@ -436,10 +436,10 @@
by (auto simp add: binary_def)
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)"
- by (simp add: range_binary_eq cong del: strong_SUP_cong)
+ by (simp add: range_binary_eq cong del: SUP_cong_strong)
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
- by (simp add: range_binary_eq cong del: strong_INF_cong)
+ by (simp add: range_binary_eq cong del: INF_cong_strong)
lemma sigma_algebra_iff2:
"sigma_algebra \<Omega> M \<longleftrightarrow>
@@ -943,7 +943,7 @@
done
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
- by (simp add: range_binaryset_eq cong del: strong_SUP_cong)
+ by (simp add: range_binaryset_eq cong del: SUP_cong_strong)
subsubsection \<open>Closed CDI\<close>
--- a/src/HOL/Complete_Lattices.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Complete_Lattices.thy Sun Oct 21 09:39:09 2018 +0200
@@ -73,7 +73,7 @@
lemma INF_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
by (simp add: image_def)
-lemma strong_INF_cong [cong]:
+lemma INF_cong_strong [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Sqinter>(C ` A) = \<Sqinter>(D ` B)"
unfolding simp_implies_def by (fact INF_cong)
@@ -83,20 +83,20 @@
begin
lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
- by (simp add: image_comp)
+by(fact Inf.INF_image)
lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
- by simp
+by(fact Inf.INF_identity_eq)
lemma SUP_id_eq [simp]: "\<Squnion>(id ` A) = \<Squnion>A"
- by (simp add: id_def)
+by(fact Inf.INF_id_eq)
lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
- by (simp add: image_def)
+by (fact Inf.INF_cong)
-lemma strong_SUP_cong [cong]:
+lemma SUP_cong_strong [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
- unfolding simp_implies_def by (fact SUP_cong)
+by (fact Inf.INF_cong_strong)
end
@@ -191,19 +191,19 @@
by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
lemma INF_insert [simp]: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> \<Sqinter>(f ` A)"
- by (simp cong del: strong_INF_cong)
+ by (simp cong del: INF_cong_strong)
lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
lemma SUP_insert [simp]: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> \<Squnion>(f ` A)"
- by (simp cong del: strong_SUP_cong)
+ by (simp cong del: SUP_cong_strong)
lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
- by (simp cong del: strong_INF_cong)
+ by (simp cong del: INF_cong_strong)
lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
- by (simp cong del: strong_SUP_cong)
+ by (simp cong del: SUP_cong_strong)
lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
by (auto intro!: antisym Inf_lower)
@@ -449,11 +449,11 @@
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)"
using INF_eq_const [of I f c] INF_lower [of _ I f]
- by (auto intro: antisym cong del: strong_INF_cong)
+ by (auto intro: antisym cong del: INF_cong_strong)
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)"
using SUP_eq_const [of I f c] SUP_upper [of _ I f]
- by (auto intro: antisym cong del: strong_SUP_cong)
+ by (auto intro: antisym cong del: SUP_cong_strong)
end
--- a/src/HOL/Groups_Big.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Groups_Big.thy Sun Oct 21 09:39:09 2018 +0200
@@ -147,10 +147,9 @@
using g_h unfolding \<open>A = B\<close>
by (induct B rule: infinite_finite_induct) auto
-lemma strong_cong [cong]:
- assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
- shows "F (\<lambda>x. g x) A = F (\<lambda>x. h x) B"
- by (rule cong) (use assms in \<open>simp_all add: simp_implies_def\<close>)
+lemma cong_strong [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)
lemma reindex_cong:
assumes "inj_on l B"
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Oct 21 09:39:09 2018 +0200
@@ -534,9 +534,9 @@
COEND
\<lbrace>\<acute>x=n\<rbrace>"
apply oghoare
-apply (simp_all cong del: sum.strong_cong)
+apply (simp_all cong del: sum.cong_strong)
apply (tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
-apply (simp_all cong del: sum.strong_cong)
+apply (simp_all cong del: sum.cong_strong)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Oct 21 09:39:09 2018 +0200
@@ -321,7 +321,7 @@
\<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>
(\<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>]"
apply (rule Parallel)
-apply (auto cong del: strong_INF_cong strong_SUP_cong)
+apply (auto cong del: INF_cong_strong SUP_cong_strong)
apply force
apply (rule While)
apply force
--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Oct 21 09:39:09 2018 +0200
@@ -188,7 +188,7 @@
proof(cases "Y = {}")
case True
then show ?thesis
- by (simp add: image_constant_conv cong del: strong_SUP_cong)
+ by (simp add: image_constant_conv cong del: SUP_cong_strong)
next
case False
have chain1: "\<And>f. f \<in> Z \<Longrightarrow> Complete_Partial_Order.chain (\<le>) (f ` Y)"
@@ -518,7 +518,7 @@
context ccpo begin
lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
-by (rule contI) (simp add: image_constant_conv cong del: strong_SUP_cong)
+by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_strong)
lemma mcont_const [cont_intro, simp]:
"mcont luba orda Sup (\<le>) (\<lambda>x. c)"
@@ -695,7 +695,7 @@
hence "\<Squnion>Y \<le> bound" using chain by(auto intro: ccpo_Sup_least)
moreover have "Y \<inter> {x. \<not> x \<le> bound} = {}" using True by auto
ultimately show ?thesis using True Y
- by (auto simp add: image_constant_conv cong del: c.strong_SUP_cong)
+ by (auto simp add: image_constant_conv cong del: c.SUP_cong_strong)
next
case False
let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
--- a/src/HOL/Library/FSet.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Library/FSet.thy Sun Oct 21 09:39:09 2018 +0200
@@ -755,10 +755,9 @@
lemmas cong[fundef_cong] = set.cong[Transfer.transferred]
-lemma strong_cong[cong]:
- assumes "A = B" "\<And>x. x |\<in>| B =simp=> g x = h x"
- shows "F g A = F h B"
-using assms unfolding simp_implies_def by (auto cong: cong)
+lemma cong_strong[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)
end
--- a/src/HOL/Library/Groups_Big_Fun.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Library/Groups_Big_Fun.thy Sun Oct 21 09:39:09 2018 +0200
@@ -62,16 +62,11 @@
"\<not> finite {a. g a \<noteq> \<^bold>1} \<Longrightarrow> G g = \<^bold>1"
by (simp add: expand_set)
-lemma cong:
+lemma cong [cong]:
assumes "\<And>a. g a = h a"
shows "G g = G h"
using assms by (simp add: expand_set)
-lemma strong_cong [cong]:
- assumes "\<And>a. g a = h a"
- shows "G (\<lambda>a. g a) = G (\<lambda>a. h a)"
- using assms by (fact cong)
-
lemma not_neutral_obtains_not_neutral:
assumes "G g \<noteq> \<^bold>1"
obtains a where "g a \<noteq> \<^bold>1"
@@ -202,7 +197,7 @@
have "(\<lambda>b. if a = b then g b else \<^bold>1) = (\<lambda>b. if b = a then g b else \<^bold>1)"
by (simp add: fun_eq_iff)
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)"
- by (simp cong del: strong_cong)
+ by (simp cong del: cong)
then show ?thesis by simp
qed
--- a/src/HOL/Number_Theory/Gauss.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy Sun Oct 21 09:39:09 2018 +0200
@@ -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.strong_cong)
+ by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_strong)
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.strong_cong)
+ by (rule cong_trans) (simp add: aux cong del: prod.cong_strong)
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 Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Probability/Information.thy Sun Oct 21 09:39:09 2018 +0200
@@ -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.strong_cong intro!: sum.mono_neutral_left measure_nonneg)
+ cong del: sum.cong_strong 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/Set.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Set.thy Sun Oct 21 09:39:09 2018 +0200
@@ -422,24 +422,24 @@
text \<open>Congruence rules\<close>
lemma ball_cong:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+ "\<lbrakk> A = B; \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
(\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
- by (simp add: Ball_def)
-
-lemma strong_ball_cong [cong]:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+by (simp add: Ball_def)
+
+lemma ball_cong_strong [cong]:
+ "\<lbrakk> A = B; \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
(\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
- by (simp add: simp_implies_def Ball_def)
+by (simp add: simp_implies_def Ball_def)
lemma bex_cong:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+ "\<lbrakk> A = B; \<And>x. x \<in> B \<Longrightarrow> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
(\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
- by (simp add: Bex_def cong: conj_cong)
-
-lemma strong_bex_cong [cong]:
- "A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x) \<Longrightarrow>
+by (simp add: Bex_def cong: conj_cong)
+
+lemma bex_cong_strong [cong]:
+ "\<lbrakk> A = B; \<And>x. x \<in> B =simp=> P x \<longleftrightarrow> Q x \<rbrakk> \<Longrightarrow>
(\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
- by (simp add: simp_implies_def Bex_def cong: conj_cong)
+by (simp add: simp_implies_def Bex_def cong: conj_cong)
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)"
by auto
--- a/src/HOL/Topological_Spaces.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy Sun Oct 21 09:39:09 2018 +0200
@@ -1882,7 +1882,7 @@
unfolding continuous_on_def
by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
-lemma continuous_on_strong_cong:
+lemma continuous_on_cong_strong:
"s = t \<Longrightarrow> (\<And>x. x \<in> t =simp=> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
unfolding simp_implies_def by (rule continuous_on_cong)
--- a/src/HOL/Transcendental.thy Sun Oct 21 08:19:06 2018 +0200
+++ b/src/HOL/Transcendental.thy Sun Oct 21 09:39:09 2018 +0200
@@ -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.strong_cong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
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.strong_cong)
+ by (auto simp: sum.reindex_bij_betw [OF h, symmetric] intro: sum.cong_strong)
qed
then show ?thesis
by (simp add: polyfun_diff [OF assms] sum_distrib_right)