avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
--- a/NEWS Sun Mar 03 20:27:42 2019 +0100
+++ b/NEWS Tue Mar 05 07:00:21 2019 +0000
@@ -135,6 +135,9 @@
are not used by default any longer. INCOMPATIBILITY; consider using
declare image_cong_simp [cong del] in extreme situations.
+* INF_image and SUP_image are no default simp rules any longer.
+INCOMPATIBILITY, prefer image_comp as simp rule if needed.
+
* Simplified syntax setup for big operators under image. In rare
situations, type conversions are not inserted implicitly any longer
and need to be given explicitly. Auxiliary abbreviations INFIMUM,
--- a/src/HOL/Analysis/Binary_Product_Measure.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Tue Mar 05 07:00:21 2019 +0000
@@ -558,7 +558,7 @@
from this measurable_emeasure_Pair[OF set] show ?case
by (rule measurable_cong[THEN iffD1])
qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1
- nn_integral_monotone_convergence_SUP incseq_def le_fun_def
+ nn_integral_monotone_convergence_SUP incseq_def le_fun_def image_comp
cong: measurable_cong)
lemma (in sigma_finite_measure) nn_integral_fst:
@@ -572,7 +572,7 @@
by (simp cong: nn_integral_cong)
qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add
nn_integral_monotone_convergence_SUP measurable_compose_Pair1
- borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def
+ borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def image_comp
cong: nn_integral_cong)
lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
--- a/src/HOL/Analysis/Borel_Space.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Tue Mar 05 07:00:21 2019 +0000
@@ -228,7 +228,7 @@
proof -
have "Inf (uminus ` S) \<in> closure (uminus ` S)"
using assms by (intro closure_contains_Inf) auto
- also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
+ also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def image_comp)
also have "closure (uminus ` S) = uminus ` closure S"
by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
finally show ?thesis by auto
@@ -876,7 +876,7 @@
then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> borel_measurable M"
by measurable
also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
- by auto
+ by (auto simp add: image_comp)
also have "(SUP i. (F ^^ i) bot) = lfp F"
by (rule sup_continuous_lfp[symmetric]) fact
finally show ?thesis .
@@ -893,7 +893,7 @@
then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> borel_measurable M"
by measurable
also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
- by auto
+ by (auto simp add: image_comp)
also have "\<dots> = gfp F"
by (rule inf_continuous_gfp[symmetric]) fact
finally show ?thesis .
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Tue Mar 05 07:00:21 2019 +0000
@@ -272,7 +272,7 @@
apply transfer
by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
(auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
- simp: bounded_norm_comp bcontfun_def)
+ simp: bounded_norm_comp bcontfun_def image_comp)
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
end
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy Tue Mar 05 07:00:21 2019 +0000
@@ -274,7 +274,7 @@
also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal)
(auto split: split_indicator simp: derivg_nonneg mult_ac)
- finally show ?case by simp
+ finally show ?case by (simp add: image_comp)
qed
qed
--- a/src/HOL/Analysis/Measurable.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Measurable.thy Tue Mar 05 07:00:21 2019 +0000
@@ -432,7 +432,7 @@
then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
by measurable
also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
- by (subst sup_continuous_lfp) (auto intro: F)
+ by (subst sup_continuous_lfp) (auto intro: F simp: image_comp)
finally show ?thesis .
qed
@@ -455,7 +455,7 @@
then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
by measurable
also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
- by (subst inf_continuous_gfp) (auto intro: F)
+ by (subst inf_continuous_gfp) (auto intro: F simp: image_comp)
finally show ?thesis .
qed
@@ -478,7 +478,7 @@
then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
by measurable
also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
- by (subst sup_continuous_lfp) (auto simp: F)
+ by (subst sup_continuous_lfp) (auto simp: F simp: image_comp)
finally show ?thesis .
qed
@@ -494,7 +494,7 @@
then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
by measurable
also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
- by (subst inf_continuous_gfp) (auto simp: F)
+ by (subst inf_continuous_gfp) (auto simp: F simp: image_comp)
finally show ?thesis .
qed
--- a/src/HOL/Analysis/Measure_Space.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Tue Mar 05 07:00:21 2019 +0000
@@ -3571,7 +3571,7 @@
moreover have "B ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} = {a \<in> B ` I. k a = (SUP x\<in>I. k (B x))}"
by auto
ultimately show ?thesis
- using assms by (auto simp: Sup_lexord_def Let_def)
+ using assms by (auto simp: Sup_lexord_def Let_def image_comp)
qed
lemma sets_SUP_cong:
@@ -3674,7 +3674,7 @@
lemma SUP_sigma_sigma:
"M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
- using Sup_sigma[of "f`M" \<Omega>] by auto
+ using Sup_sigma[of "f`M" \<Omega>] by (auto simp: image_comp)
lemma sets_vimage_Sup_eq:
assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Tue Mar 05 07:00:21 2019 +0000
@@ -386,7 +386,7 @@
by (simp add: real)
qed }
ultimately show ?thesis
- by (intro exI[of _ "\<lambda>i x. ennreal (f i x)"]) auto
+ by (intro exI [of _ "\<lambda>i x. ennreal (f i x)"]) (auto simp add: image_comp)
qed
lemma borel_measurable_implies_simple_function_sequence':
@@ -394,7 +394,8 @@
assumes u: "u \<in> borel_measurable M"
obtains f where
"\<And>i. simple_function M (f i)" "incseq f" "\<And>i x. f i x < top" "\<And>x. (SUP i. f i x) = u x"
- using borel_measurable_implies_simple_function_sequence[OF u] by (auto simp: fun_eq_iff) blast
+ using borel_measurable_implies_simple_function_sequence [OF u]
+ by (metis SUP_apply)
lemma%important simple_function_induct
[consumes 1, case_names cong set mult add, induct set: simple_function]:
@@ -481,7 +482,7 @@
proof%unimportant (induct rule: borel_measurable_implies_simple_function_sequence')
fix U assume U: "\<And>i. simple_function M (U i)" "incseq U" "\<And>i x. U i x < top" and sup: "\<And>x. (SUP i. U i x) = u x"
have u_eq: "u = (SUP i. U i)"
- using u sup by auto
+ using u by (auto simp add: image_comp sup)
have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top"
using U by (auto simp: image_iff eq_commute)
@@ -1538,7 +1539,7 @@
using N by auto
from f show ?thesis
apply induct
- apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N)
+ apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N image_comp)
apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric])
done
qed
@@ -1667,7 +1668,7 @@
by (subst nn_integral_cong[OF eq])
(auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
- nn_integral_monotone_convergence_SUP le_fun_def incseq_def)
+ nn_integral_monotone_convergence_SUP le_fun_def incseq_def image_comp)
subsubsection%unimportant \<open>Counting space\<close>
@@ -2198,7 +2199,7 @@
have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
by eventually_elim (simp add: SUP_mult_left_ennreal seq)
from seq f show ?case
- apply (simp add: nn_integral_monotone_convergence_SUP)
+ apply (simp add: nn_integral_monotone_convergence_SUP image_comp)
apply (subst nn_integral_cong_AE[OF eq])
apply (subst nn_integral_monotone_convergence_SUP_AE)
apply (auto simp: incseq_def le_fun_def intro!: mult_left_mono)
@@ -2500,7 +2501,7 @@
next
case (seq U)
thus ?case
- by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal)
+ by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal image_comp)
qed simp
end
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue Mar 05 07:00:21 2019 +0000
@@ -53,7 +53,7 @@
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)"
- using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
+ using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp)
lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
by (auto simp: eucl_abs)
--- a/src/HOL/Analysis/Tagged_Division.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Tue Mar 05 07:00:21 2019 +0000
@@ -170,10 +170,10 @@
proof-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>A. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
+ by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>B. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
+ by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp inner_Pair_0)
ultimately show ?thesis unfolding interval_upperbound_def
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
@@ -184,10 +184,10 @@
proof-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>A. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
+ by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>B. x \<bullet> i) *\<^sub>R i)"
- by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
+ by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp inner_Pair_0)
ultimately show ?thesis unfolding interval_lowerbound_def
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
qed
--- a/src/HOL/Complete_Lattices.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Mar 05 07:00:21 2019 +0000
@@ -49,7 +49,7 @@
context Inf
begin
-lemma INF_image [simp]: " \<Sqinter>(g ` f ` A) = \<Sqinter>((g \<circ> f) ` A)"
+lemma INF_image: "\<Sqinter> (g ` f ` A) = \<Sqinter> ((g \<circ> f) ` A)"
by (simp add: image_comp)
lemma INF_identity_eq [simp]: "(\<Sqinter>x\<in>A. x) = \<Sqinter>A"
@@ -70,7 +70,7 @@
context Sup
begin
-lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
+lemma SUP_image: "\<Squnion> (g ` f ` A) = \<Squnion> ((g \<circ> f) ` A)"
by(fact Inf.INF_image)
lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
@@ -677,10 +677,10 @@
end
lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
- using Inf_apply [of "f ` A"] by (simp add: comp_def)
+ by (simp add: image_comp)
lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
- using Sup_apply [of "f ` A"] by (simp add: comp_def)
+ by (simp add: image_comp)
subsection \<open>Complete lattice on unary and binary predicates\<close>
--- a/src/HOL/Hilbert_Choice.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Hilbert_Choice.thy Tue Mar 05 07:00:21 2019 +0000
@@ -1025,7 +1025,7 @@
for f and B
using that by (auto intro: SUP_upper2 INF_lower2)
then show "(\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a) \<le> (\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a)"
- by (auto intro!: SUP_least INF_greatest)
+ by (auto intro!: SUP_least INF_greatest simp add: image_comp)
next
show "(\<Sqinter>x\<in>A. \<Squnion>a\<in>x. g a) \<le> (\<Squnion>x\<in>{f ` A |f. \<forall>Y\<in>A. f Y \<in> Y}. \<Sqinter>a\<in>x. g a)"
proof (cases "{} \<in> A")
@@ -1103,10 +1103,10 @@
begin
lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
- by (simp add: sup_Inf)
+ by (simp add: sup_Inf image_comp)
lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
- by (simp add: inf_Sup)
+ by (simp add: inf_Sup image_comp)
lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
by (simp add: sup_Inf sup_commute)
@@ -1175,7 +1175,7 @@
instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
begin
-instance by standard (simp add: le_fun_def INF_SUP_set)
+instance by standard (simp add: le_fun_def INF_SUP_set image_comp)
end
instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
--- a/src/HOL/Library/Extended_Nat.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Tue Mar 05 07:00:21 2019 +0000
@@ -678,7 +678,8 @@
by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)
lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))"
- using eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def)
+ using eSuc_Sup [of "_ ` UNIV"] by (auto simp: sup_continuous_def image_comp)
+
subsection \<open>Traditional theorem names\<close>
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Mar 05 07:00:21 2019 +0000
@@ -109,7 +109,7 @@
fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
shows "sup_continuous (SUP i\<in>I. M i)"
- unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
+ unfolding sup_continuous_def by (auto simp add: sup_continuousD [OF M] image_comp intro: SUP_commute)
lemma sup_continuous_apply_SUP[order_continuous_intros]:
fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
@@ -1410,7 +1410,7 @@
shows "(INF i. f i + c) = (INF i. f i) + c"
using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
- by (auto simp: mono_def)
+ by (auto simp: mono_def image_comp)
lemma INF_ennreal_const_add:
fixes f g :: "nat \<Rightarrow> ennreal"
@@ -1609,9 +1609,9 @@
obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i \<in> I. g i) = (SUP i. M i)"
by auto
have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
- unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
+ unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by (simp add: image_comp)
also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
- by (insert M, drule SUP_subset_mono) auto
+ by (insert M, drule SUP_subset_mono) (auto simp add: image_comp)
finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
qed
--- a/src/HOL/Library/Extended_Real.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Mar 05 07:00:21 2019 +0000
@@ -41,7 +41,7 @@
unfolding sup_continuous_def
proof safe
fix M :: "nat \<Rightarrow> 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))"
- using continuous_at_Sup_mono[OF assms, of "range M"] by simp
+ using continuous_at_Sup_mono [OF assms, of "range M"] by (simp add: image_comp)
qed
lemma sup_continuous_at_left:
@@ -80,7 +80,7 @@
unfolding inf_continuous_def
proof safe
fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
- using continuous_at_Inf_mono[OF assms, of "range M"] by simp
+ using continuous_at_Inf_mono [OF assms, of "range M"] by (simp add: image_comp)
qed
lemma inf_continuous_at_right:
@@ -2158,7 +2158,7 @@
qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
lemma ereal_SUP: "\<bar>SUP a\<in>A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a\<in>A. f a) = (SUP a\<in>A. ereal (f a))"
- using ereal_Sup[of "f`A"] by auto
+ by (simp add: ereal_Sup image_comp)
lemma ereal_Inf:
assumes *: "\<bar>INF a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
@@ -2183,7 +2183,7 @@
qed
lemma ereal_INF: "\<bar>INF a\<in>A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a\<in>A. f a) = (INF a\<in>A. ereal (f a))"
- using ereal_Inf[of "f`A"] by auto
+ by (simp add: ereal_Inf image_comp)
lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
by (auto intro!: SUP_eqI
@@ -2193,7 +2193,7 @@
lemma ereal_SUP_uminus_eq:
fixes f :: "'a \<Rightarrow> ereal"
shows "(SUP x\<in>S. uminus (f x)) = - (INF x\<in>S. f x)"
- using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+ using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: image_comp)
lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
by (auto intro!: inj_onI)
@@ -2204,7 +2204,7 @@
lemma ereal_INF_uminus_eq:
fixes f :: "'a \<Rightarrow> ereal"
shows "(INF x\<in>S. - f x) = - (SUP x\<in>S. f x)"
- using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
+ using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: image_comp)
lemma ereal_SUP_uminus:
fixes f :: "'a \<Rightarrow> ereal"
@@ -2297,7 +2297,8 @@
case False
then show ?thesis
by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
- (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
+ (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \<open>I \<noteq> {}\<close>
+ \<open>c \<noteq> -\<infinity>\<close> image_comp)
qed
lemma SUP_ereal_add_right:
@@ -2370,7 +2371,8 @@
unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
then show ?thesis
by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
- (auto simp: mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at)
+ (auto simp: mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within
+ continuous_at image_comp)
qed
lemma INF_ereal_add_right:
@@ -2464,7 +2466,7 @@
case False
then show ?thesis
by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
- (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
+ (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close> image_comp
intro!: ereal_mult_left_mono c)
qed
@@ -2626,7 +2628,8 @@
lemma ereal_of_enat_SUP:
"A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a\<in>A. f a) = (SUP a \<in> A. ereal_of_enat (f a))"
- using ereal_of_enat_Sup[of "f`A"] by auto
+ by (simp add: ereal_of_enat_Sup image_comp)
+
subsection "Limits on \<^typ>\<open>ereal\<close>"
--- a/src/HOL/Library/Liminf_Limsup.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Mar 05 07:00:21 2019 +0000
@@ -435,14 +435,16 @@
qed }
note * = this
- have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
- unfolding Liminf_def
- by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
- (auto intro: eventually_True)
+ have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
+ Sup (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
+ using am continuous_on_imp_continuous_within [OF c]
+ by (rule continuous_at_Sup_mono) (auto intro: eventually_True)
+ then have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
+ by (simp add: Liminf_def image_comp)
also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
using * continuous_at_Inf_mono [OF am continuous_on_imp_continuous_within [OF c]]
by auto
- finally show ?thesis by (auto simp: Liminf_def)
+ finally show ?thesis by (auto simp: Liminf_def image_comp)
qed
lemma Limsup_compose_continuous_mono:
@@ -460,14 +462,16 @@
qed }
note * = this
- have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
- unfolding Limsup_def
- by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
- (auto intro: eventually_True)
+ have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
+ Inf (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
+ using am continuous_on_imp_continuous_within [OF c]
+ by (rule continuous_at_Inf_mono) (auto intro: eventually_True)
+ then have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
+ by (simp add: Limsup_def image_comp)
also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
using * continuous_at_Sup_mono [OF am continuous_on_imp_continuous_within [OF c]]
by auto
- finally show ?thesis by (auto simp: Limsup_def)
+ finally show ?thesis by (auto simp: Limsup_def image_comp)
qed
lemma Liminf_compose_continuous_antimono:
@@ -484,15 +488,18 @@
with \<open>eventually P F\<close> F show False
by auto
qed
- have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
- unfolding Limsup_def
- by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
- (auto intro: eventually_True)
+
+ have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
+ Sup (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
+ using am continuous_on_imp_continuous_within [OF c]
+ by (rule continuous_at_Inf_antimono) (auto intro: eventually_True)
+ then have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
+ by (simp add: Limsup_def image_comp)
also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
using * continuous_at_Sup_antimono [OF am continuous_on_imp_continuous_within [OF c]]
by auto
finally show ?thesis
- by (auto simp: Liminf_def)
+ by (auto simp: Liminf_def image_comp)
qed
lemma Limsup_compose_continuous_antimono:
@@ -510,15 +517,17 @@
qed }
note * = this
- have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
- unfolding Liminf_def
- by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
- (auto intro: eventually_True)
+ have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
+ Inf (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
+ using am continuous_on_imp_continuous_within [OF c]
+ by (rule continuous_at_Sup_antimono) (auto intro: eventually_True)
+ then have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
+ by (simp add: Liminf_def image_comp)
also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
using * continuous_at_Inf_antimono [OF am continuous_on_imp_continuous_within [OF c]]
by auto
finally show ?thesis
- by (auto simp: Limsup_def)
+ by (auto simp: Limsup_def image_comp)
qed
lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
--- a/src/HOL/Library/Option_ord.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Option_ord.thy Tue Mar 05 07:00:21 2019 +0000
@@ -277,11 +277,11 @@
lemma Some_INF:
"Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
- using Some_Inf [of "f ` A"] by (simp add: comp_def)
+ by (simp add: Some_Inf image_comp)
lemma Some_SUP:
"A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
- using Some_Sup [of "f ` A"] by (simp add: comp_def)
+ by (simp add: Some_Sup image_comp)
lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
for A :: "('a::complete_distrib_lattice option) set set"
--- a/src/HOL/Library/Order_Continuity.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Order_Continuity.thy Tue Mar 05 07:00:21 2019 +0000
@@ -68,7 +68,7 @@
and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
- by (auto simp: sup_continuous_def)
+ by (auto simp: sup_continuous_def image_comp)
lemma sup_continuous_compose:
assumes f: "sup_continuous f" and g: "sup_continuous g"
@@ -242,7 +242,7 @@
and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
- by (auto simp: inf_continuous_def)
+ by (auto simp: inf_continuous_def image_comp)
lemma inf_continuous_inf[order_continuous_intros]:
"inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
@@ -412,7 +412,8 @@
assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
proof -
have "cclfp F = (SUP i. F ((F ^^ i) bot))"
- unfolding cclfp_def by (subst UNIV_nat_eq) auto
+ unfolding cclfp_def
+ by (subst UNIV_nat_eq) (simp add: image_comp)
also have "\<dots> = F (cclfp F)"
unfolding cclfp_def
by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono)
--- a/src/HOL/Library/Product_Order.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Library/Product_Order.thy Tue Mar 05 07:00:21 2019 +0000
@@ -185,35 +185,35 @@
by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
-lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)"
- unfolding Sup_prod_def by simp
-
-lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)"
- unfolding Sup_prod_def by simp
+lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)"
+ by (simp add: Inf_prod_def)
-lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)"
- unfolding Inf_prod_def by simp
+lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))"
+ by (simp add: fst_Inf image_image)
-lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)"
- unfolding Inf_prod_def by simp
+lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)"
+ by (simp add: Sup_prod_def)
lemma fst_SUP: "fst (SUP x\<in>A. f x) = (SUP x\<in>A. fst (f x))"
- using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
+ by (simp add: fst_Sup image_image)
+
+lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)"
+ by (simp add: Inf_prod_def)
+
+lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))"
+ by (simp add: snd_Inf image_image)
+
+lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)"
+ by (simp add: Sup_prod_def)
lemma snd_SUP: "snd (SUP x\<in>A. f x) = (SUP x\<in>A. snd (f x))"
- using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
+ by (simp add: snd_Sup image_image)
-lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))"
- using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
-
-lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))"
- using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
+lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)"
+ by (simp add: Inf_prod_def image_image)
lemma SUP_Pair: "(SUP x\<in>A. (f x, g x)) = (SUP x\<in>A. f x, SUP x\<in>A. g x)"
- unfolding Sup_prod_def by (simp add: comp_def)
-
-lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)"
- unfolding Inf_prod_def by (simp add: comp_def)
+ by (simp add: Sup_prod_def image_image)
text \<open>Alternative formulations for set infima and suprema over the product
@@ -221,11 +221,11 @@
lemma INF_prod_alt_def:
"Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))"
- unfolding Inf_prod_def by simp
+ by (simp add: Inf_prod_def image_image)
lemma SUP_prod_alt_def:
"Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))"
- unfolding Sup_prod_def by simp
+ by (simp add: Sup_prod_def image_image)
subsection \<open>Complete distributive lattices\<close>
@@ -236,7 +236,7 @@
proof
fix A::"('a\<times>'b) set set"
show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
- by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
+ by (simp add: Inf_prod_def Sup_prod_def INF_SUP_set image_image)
qed
subsection \<open>Bekic's Theorem\<close>
--- a/src/HOL/Predicate.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Predicate.thy Tue Mar 05 07:00:21 2019 +0000
@@ -78,11 +78,11 @@
lemma eval_INF [simp]:
"eval (\<Sqinter>(f ` A)) = \<Sqinter>((eval \<circ> f) ` A)"
- by simp
+ by (simp add: image_comp)
lemma eval_SUP [simp]:
"eval (\<Squnion>(f ` A)) = \<Squnion>((eval \<circ> f) ` A)"
- by simp
+ by (simp add: image_comp)
instantiation pred :: (type) complete_boolean_algebra
begin
@@ -400,7 +400,7 @@
lemma eval_map [simp]:
"eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
- by (auto simp add: map_def comp_def)
+ by (simp add: map_def comp_def image_comp)
functor map: map
by (rule ext, rule pred_eqI, auto)+
--- a/src/HOL/Probability/Giry_Monad.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Tue Mar 05 07:00:21 2019 +0000
@@ -880,7 +880,7 @@
also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
(simp_all add: M cong: measurable_cong_sets)
- finally show ?case by (simp add: ac_simps)
+ finally show ?case by (simp add: ac_simps image_comp)
qed
lemma measurable_join1:
--- a/src/HOL/Probability/Helly_Selection.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Probability/Helly_Selection.thy Tue Mar 05 07:00:21 2019 +0000
@@ -88,7 +88,7 @@
define F where "F x = Inf {lim (?f n) |n. x < r n}" for x
have F_eq: "ereal (F x) = (INF n\<in>{n. x < r n}. ereal (lim (?f n)))" for x
- unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image)
+ unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image image_comp)
have mono_F: "mono F"
using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
moreover have "\<And>x. continuous (at_right x) F"
--- a/src/HOL/Probability/SPMF.thy Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Probability/SPMF.thy Tue Mar 05 07:00:21 2019 +0000
@@ -45,7 +45,7 @@
lemma ennreal_SUP:
"\<lbrakk> (SUP a\<in>A. ennreal (f a)) \<noteq> \<top>; A \<noteq> {} \<rbrakk> \<Longrightarrow> ennreal (SUP a\<in>A. f a) = (SUP a\<in>A. ennreal (f a))"
-using ennreal_Sup[of "f ` A"] by auto
+using ennreal_Sup[of "f ` A"] by (auto simp add: image_comp)
lemma ennreal_lt_0: "x < 0 \<Longrightarrow> ennreal x = 0"
by(simp add: ennreal_eq_0_iff)
@@ -1589,7 +1589,7 @@
using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf p f) i))"
by(auto simp add: ennreal_spmf_bind nn_integral_measure_spmf nn_integral_count_space_indicator set_lub_spmf[OF chain] in_set_spmf_iff_spmf ennreal_mult intro!: arg_cong [of _ _ Sup] image_cong nn_integral_cong split: split_indicator)
- also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
+ also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y image_comp)
finally show "spmf ?lhs i = spmf ?rhs i" by simp
qed
qed simp
@@ -1620,14 +1620,14 @@
using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p\<in>Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
- by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
+ by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult image_comp)
also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
unfolding nn_integral_measure_spmf' using Y chain''
by(rule nn_integral_monotone_convergence_SUP_countable) simp
also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult)
also have "\<dots> = ennreal (spmf ?rhs i)" using chain'''
- by(auto simp add: ennreal_spmf_lub_spmf Y)
+ by(auto simp add: ennreal_spmf_lub_spmf Y image_comp)
finally show "spmf ?lhs i = spmf ?rhs i" by simp
qed
qed simp