--- a/NEWS Sun Dec 30 16:56:31 2018 +0100
+++ b/NEWS Sun Dec 30 17:44:33 2018 +0100
@@ -84,7 +84,8 @@
INCOMPATIBILITY.
* Strong congruence rules (with =simp=> in the premises) for constant f
-are now uniformly called f_cong_strong.
+are now uniformly called f_cong_simp, in accordance with congruence
+rules produced for mappers by the datatype package. INCOMPATIBILITY.
* Sledgehammer: The URL for SystemOnTPTP, which is used by remote
provers, has been updated.
--- a/src/HOL/Analysis/Bochner_Integration.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/Bochner_Integration.thy Sun Dec 30 17:44:33 2018 +0100
@@ -524,7 +524,7 @@
assumes "M = N" "\<And>x. x \<in> space N \<Longrightarrow> f x = g x" "x = y"
shows "has_bochner_integral M f x \<longleftrightarrow> has_bochner_integral N g y"
unfolding has_bochner_integral.simps assms(1,3)
- using assms(2) by (simp cong: measurable_cong_strong nn_integral_cong_strong)
+ using assms(2) by (simp cong: measurable_cong_simp nn_integral_cong_simp)
lemma%unimportant has_bochner_integral_cong_AE:
"f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> (AE x in M. f x = g x) \<Longrightarrow>
--- a/src/HOL/Analysis/Caratheodory.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy Sun Dec 30 17:44:33 2018 +0100
@@ -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: SUP_cong_strong)
+ by (auto simp add: f_def cong del: SUP_cong_simp)
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 Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy Sun Dec 30 17:44:33 2018 +0100
@@ -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 L2_set_cong_strong:
+lemma L2_set_cong_simp:
"\<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/Lebesgue_Measure.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Sun Dec 30 17:44:33 2018 +0100
@@ -407,7 +407,7 @@
lemma measurable_lebesgue_cong:
assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
- by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
+ by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
text%unimportant \<open>Measurability of continuous functions\<close>
--- a/src/HOL/Analysis/Measure_Space.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Sun Dec 30 17:44:33 2018 +0100
@@ -1143,7 +1143,7 @@
"(\<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)"
by auto
-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)"
+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)"
by (auto simp: simp_implies_def)
lemma AE_all_countable:
@@ -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: SUP_cong_strong)
+ using A by (auto cong del: SUP_cong_simp)
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 Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Dec 30 17:44:33 2018 +0100
@@ -2058,7 +2058,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: SUP_cong_strong)
+ unfolding nn_integral_def_finite by (simp cong del: SUP_cong_simp)
qed
lemma nn_integral_count_space_indicator:
--- a/src/HOL/Analysis/Sigma_Algebra.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Sun Dec 30 17:44:33 2018 +0100
@@ -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: SUP_cong_strong)
+ by (simp add: range_binary_eq cong del: SUP_cong_simp)
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)"
- by (simp add: range_binary_eq cong del: INF_cong_strong)
+ by (simp add: range_binary_eq cong del: INF_cong_simp)
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: SUP_cong_strong)
+ by (simp add: range_binaryset_eq cong del: SUP_cong_simp)
subsubsection \<open>Closed CDI\<close>
@@ -1802,7 +1802,7 @@
unfolding measurable_def using assms
by (simp cong: vimage_inter_cong Pi_cong add: simp_implies_def)
-lemma measurable_cong_strong:
+lemma measurable_cong_simp:
"M = N \<Longrightarrow> M' = N' \<Longrightarrow> (\<And>w. w \<in> space M \<Longrightarrow> f w = g w) \<Longrightarrow>
f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
by (metis measurable_cong)
--- a/src/HOL/Complete_Lattices.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Complete_Lattices.thy Sun Dec 30 17:44:33 2018 +0100
@@ -61,7 +61,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 INF_cong_strong [cong]:
+lemma INF_cong_simp [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)
@@ -82,9 +82,9 @@
lemma SUP_cong: "A = B \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
by (fact Inf.INF_cong)
-lemma SUP_cong_strong [cong]:
+lemma SUP_cong_simp [cong]:
"A = B \<Longrightarrow> (\<And>x. x \<in> B =simp=> C x = D x) \<Longrightarrow> \<Squnion>(C ` A) = \<Squnion>(D ` B)"
-by (fact Inf.INF_cong_strong)
+by (fact Inf.INF_cong_simp)
end
@@ -179,19 +179,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: INF_cong_strong)
+ by (simp cong del: INF_cong_simp)
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: SUP_cong_strong)
+ by (simp cong del: SUP_cong_simp)
lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
- by (simp cong del: INF_cong_strong)
+ by (simp cong del: INF_cong_simp)
lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
- by (simp cong del: SUP_cong_strong)
+ by (simp cong del: SUP_cong_simp)
lemma Inf_UNIV [simp]: "\<Sqinter>UNIV = \<bottom>"
by (auto intro!: antisym Inf_lower)
@@ -437,11 +437,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: INF_cong_strong)
+ by (auto intro: antisym cong del: INF_cong_simp)
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: SUP_cong_strong)
+ by (auto intro: antisym cong del: SUP_cong_simp)
end
--- a/src/HOL/Data_Structures/Braun_Tree.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Data_Structures/Braun_Tree.thy Sun Dec 30 17:44:33 2018 +0100
@@ -252,7 +252,7 @@
by (simp add: insert_ident Icc_eq_insert_lb_nat nat_in_image braun_indices1)
thus ?case using Node.IH even_odd_decomp[OF _ _ 3]
by(simp add: card_image inj_on_def card_braun_indices Let_def 1 2 inj_image_eq_iff image_comp
- cong: image_cong_strong)
+ cong: image_cong_simp)
qed
lemma braun_iff_braun_indices: "braun t \<longleftrightarrow> braun_indices t = {1..size t}"
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Dec 30 17:44:33 2018 +0100
@@ -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: INF_cong_strong SUP_cong_strong)
+apply (auto cong del: INF_cong_simp SUP_cong_simp)
apply force
apply (rule While)
apply force
--- a/src/HOL/Library/Complete_Partial_Order2.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Library/Complete_Partial_Order2.thy Sun Dec 30 17:44:33 2018 +0100
@@ -188,7 +188,7 @@
proof(cases "Y = {}")
case True
then show ?thesis
- by (simp add: image_constant_conv cong del: SUP_cong_strong)
+ by (simp add: image_constant_conv cong del: SUP_cong_simp)
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: SUP_cong_strong)
+by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
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.SUP_cong_strong)
+ by (auto simp add: image_constant_conv cong del: c.SUP_cong_simp)
next
case False
let ?Y = "Y \<inter> {x. \<not> x \<le> bound}"
--- a/src/HOL/Probability/Giry_Monad.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Sun Dec 30 17:44:33 2018 +0100
@@ -1763,7 +1763,7 @@
qed
qed
-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"
+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"
by (auto simp: simp_implies_def intro!: bind_cong)
lemma sets_bind_measurable:
--- a/src/HOL/ROOT Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/ROOT Sun Dec 30 17:44:33 2018 +0100
@@ -65,7 +65,6 @@
"HOL-Library"
"HOL-Computational_Algebra"
theories
- L2_Norm
Analysis
document_files
"root.tex"
--- a/src/HOL/Set.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Set.thy Sun Dec 30 17:44:33 2018 +0100
@@ -426,7 +426,7 @@
(\<forall>x\<in>A. P x) \<longleftrightarrow> (\<forall>x\<in>B. Q x)"
by (simp add: Ball_def)
-lemma ball_cong_strong [cong]:
+lemma ball_cong_simp [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)
@@ -436,7 +436,7 @@
(\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
by (simp add: Bex_def cong: conj_cong)
-lemma bex_cong_strong [cong]:
+lemma bex_cong_simp [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)
@@ -939,7 +939,7 @@
lemma image_cong: "\<lbrakk> M = N; \<And>x. x \<in> N \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> f ` M = g ` N"
by (simp add: image_def)
-lemma image_cong_strong: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
+lemma image_cong_simp: "\<lbrakk> M = N; \<And>x. x \<in> N =simp=> f x = g x\<rbrakk> \<Longrightarrow> f ` M = g ` N"
by (simp add: image_def simp_implies_def)
lemma image_Int_subset: "f ` (A \<inter> B) \<subseteq> f ` A \<inter> f ` B"
--- a/src/HOL/Topological_Spaces.thy Sun Dec 30 16:56:31 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Sun Dec 30 17:44:33 2018 +0100
@@ -1882,7 +1882,7 @@
unfolding continuous_on_def
by (intro ball_cong filterlim_cong) (auto simp: eventually_at_filter)
-lemma continuous_on_cong_strong:
+lemma continuous_on_cong_simp:
"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)