# HG changeset patch # User haftmann # Date 1551769221 0 # Node ID 62e47f06d22c02a0afbf3e555f50bf2f929e4857 # Parent b58a575d211e51acbc1e6066fd5400962c4212b2 avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default diff -r b58a575d211e -r 62e47f06d22c NEWS --- 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, diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Binary_Product_Measure.thy --- 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)]: diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Borel_Space.thy --- 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) \ 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 "(\x. SUP i. (F ^^ i) bot x) \ borel_measurable M" by measurable also have "(\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 "(\x. INF i. (F ^^ i) top x) \ borel_measurable M" by measurable also have "(\x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)" - by auto + by (auto simp add: image_comp) also have "\ = gfp F" by (rule inf_continuous_gfp[symmetric]) fact finally show ?thesis . diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Bounded_Continuous_Function.thy --- 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 diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Lebesgue_Integral_Substitution.thy --- 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 "... = \\<^sup>+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x \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 diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Measurable.thy --- 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 "(\x. SUP i. (F ^^ i) bot x) \ measurable M (count_space UNIV)" by measurable also have "(\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 "(\x. INF i. (F ^^ i) top x) \ measurable M (count_space UNIV)" by measurable also have "(\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 "(\x. SUP i. (F ^^ i) bot s x) \ measurable M (count_space UNIV)" by measurable also have "(\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 "(\x. INF i. (F ^^ i) top s x) \ measurable M (count_space UNIV)" by measurable also have "(\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 diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Measure_Space.thy --- 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 \ I. k (B a) = (SUP x\I. k (B x))} = {a \ B ` I. k a = (SUP x\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 \ {} \ (\m. m \ M \ f m \ Pow \) \ (SUP m\M. sigma \ (f m)) = sigma \ (\m\M. f m)" - using Sup_sigma[of "f`M" \] by auto + using Sup_sigma[of "f`M" \] by (auto simp: image_comp) lemma sets_vimage_Sup_eq: assumes *: "M \ {}" "f \ X \ Y" "\m. m \ M \ space m = Y" diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy --- 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 _ "\i x. ennreal (f i x)"]) auto + by (intro exI [of _ "\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 \ borel_measurable M" obtains f where "\i. simple_function M (f i)" "incseq f" "\i x. f i x < top" "\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: "\i. simple_function M (U i)" "incseq U" "\i x. U i x < top" and sup: "\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: "\x i. x \ space M \ 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 \Counting space\ @@ -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 diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Ordered_Euclidean_Space.thy --- 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 \ Basis \ (INF x\X. f x) \ i = (INF x\X. f x \ i)" and inner_Basis_SUP_left: "i \ Basis \ (SUP x\X. f x) \ i = (SUP x\X. f x \ 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 \ Basis \ \x\ \ i = \x \ i\" by (auto simp: eucl_abs) diff -r b58a575d211e -r 62e47f06d22c src/HOL/Analysis/Tagged_Division.thy --- 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 \ B)" by simp have "(\i\Basis. (SUP x\A \ B. x \ (i, 0)) *\<^sub>R i) = (\i\Basis. (SUP x\A. x \ 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 \ B)" by simp have "(\i\Basis. (SUP x\A \ B. x \ (0, i)) *\<^sub>R i) = (\i\Basis. (SUP x\B. x \ 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 \ B)" by simp have "(\i\Basis. (INF x\A \ B. x \ (i, 0)) *\<^sub>R i) = (\i\Basis. (INF x\A. x \ 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 \ B)" by simp have "(\i\Basis. (INF x\A \ B. x \ (0, i)) *\<^sub>R i) = (\i\Basis. (INF x\B. x \ 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 diff -r b58a575d211e -r 62e47f06d22c src/HOL/Complete_Lattices.thy --- 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]: " \(g ` f ` A) = \((g \ f) ` A)" +lemma INF_image: "\ (g ` f ` A) = \ ((g \ f) ` A)" by (simp add: image_comp) lemma INF_identity_eq [simp]: "(\x\A. x) = \A" @@ -70,7 +70,7 @@ context Sup begin -lemma SUP_image [simp]: "\(g ` f ` A) = \((g \ f) ` A)" +lemma SUP_image: "\ (g ` f ` A) = \ ((g \ f) ` A)" by(fact Inf.INF_image) lemma SUP_identity_eq [simp]: "(\x\A. x) = \A" @@ -677,10 +677,10 @@ end lemma INF_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)" - using Inf_apply [of "f ` A"] by (simp add: comp_def) + by (simp add: image_comp) lemma SUP_apply [simp]: "(\y\A. f y) x = (\y\A. f y x)" - using Sup_apply [of "f ` A"] by (simp add: comp_def) + by (simp add: image_comp) subsection \Complete lattice on unary and binary predicates\ diff -r b58a575d211e -r 62e47f06d22c src/HOL/Hilbert_Choice.thy --- 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 "(\x\{f ` A |f. \Y\A. f Y \ Y}. \a\x. g a) \ (\x\A. \a\x. g a)" - by (auto intro!: SUP_least INF_greatest) + by (auto intro!: SUP_least INF_greatest simp add: image_comp) next show "(\x\A. \a\x. g a) \ (\x\{f ` A |f. \Y\A. f Y \ Y}. \a\x. g a)" proof (cases "{} \ A") @@ -1103,10 +1103,10 @@ begin lemma sup_INF: "a \ (\b\B. f b) = (\b\B. a \ f b)" - by (simp add: sup_Inf) + by (simp add: sup_Inf image_comp) lemma inf_SUP: "a \ (\b\B. f b) = (\b\B. a \ f b)" - by (simp add: inf_Sup) + by (simp add: inf_Sup image_comp) lemma Inf_sup: "\B \ a = (\b\B. b \ 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 .. diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Extended_Nat.thy --- 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 \ sup_continuous (\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 \Traditional theorem names\ diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Extended_Nonnegative_Real.thy --- 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 :: "_ \ _ \ 'a::complete_lattice" assumes M: "\i. i \ I \ sup_continuous (M i)" shows "sup_continuous (SUP i\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 :: "_ \ _ \ 'a::complete_lattice" @@ -1410,7 +1410,7 @@ shows "(INF i. f i + c) = (INF i. f i) + c" using continuous_at_Inf_mono[of "\x. x + c" "f`UNIV"] using continuous_add[of "at_right (Inf (range f))", of "\x. x" "\x. c"] - by (auto simp: mono_def) + by (auto simp: mono_def image_comp) lemma INF_ennreal_const_add: fixes f g :: "nat \ ennreal" @@ -1609,9 +1609,9 @@ obtain M :: "nat \ ennreal" where "incseq M" and M: "range M \ g ` I" and eq: "(SUP i \ I. g i) = (SUP i. M i)" by auto have "f (SUP i \ I. g i) = (SUP i \ range M. f i)" - unfolding eq sup_continuousD[OF f \mono M\] by simp + unfolding eq sup_continuousD[OF f \mono M\] by (simp add: image_comp) also have "\ \ (SUP i \ 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 \ I. g i) \ (SUP i \ I. f (g i))" . qed diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Extended_Real.thy --- 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 \ '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 \ '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: "\SUP a\A. ereal (f a)\ \ \ \ ereal (SUP a\A. f a) = (SUP a\A. ereal (f a))" - using ereal_Sup[of "f`A"] by auto + by (simp add: ereal_Sup image_comp) lemma ereal_Inf: assumes *: "\INF a\A. ereal a\ \ \" @@ -2183,7 +2183,7 @@ qed lemma ereal_INF: "\INF a\A. ereal (f a)\ \ \ \ ereal (INF a\A. f a) = (INF a\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 \ ereal" shows "(SUP x\S. uminus (f x)) = - (INF x\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 \ ereal" shows "(INF x\S. - f x) = - (SUP x\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 \ ereal" @@ -2297,7 +2297,8 @@ case False then show ?thesis by (subst continuous_at_Sup_mono[where f="\x. x + c"]) - (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \I \ {}\ \c \ -\\) + (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \I \ {}\ + \c \ -\\ 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="\x. x + c"]) - (auto simp: mono_def add_mono \I \ {}\ \c \ -\\ continuous_at_imp_continuous_at_within continuous_at) + (auto simp: mono_def add_mono \I \ {}\ \c \ -\\ 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="\x. c * x"]) - (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \I \ {}\ + (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \I \ {}\ image_comp intro!: ereal_mult_left_mono c) qed @@ -2626,7 +2628,8 @@ lemma ereal_of_enat_SUP: "A \ {} \ ereal_of_enat (SUP a\A. f a) = (SUP a \ 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>\ereal\" diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Liminf_Limsup.thy --- 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 \ {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\{P. eventually P F}. Inf (g ` Collect P)) = + Sup (f ` (\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 \ {P. eventually P F}. f (Inf (g ` Collect P)))" + by (simp add: Liminf_def image_comp) also have "\ = (SUP P \ {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 \ {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\{P. eventually P F}. Sup (g ` Collect P)) = + Inf (f ` (\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 \ {P. eventually P F}. f (Sup (g ` Collect P)))" + by (simp add: Limsup_def image_comp) also have "\ = (INF P \ {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 \eventually P F\ F show False by auto qed - have "f (Limsup F g) = (SUP P \ {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\{P. eventually P F}. Sup (g ` Collect P)) = + Sup (f ` (\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 \ {P. eventually P F}. f (Sup (g ` Collect P)))" + by (simp add: Limsup_def image_comp) also have "\ = (SUP P \ {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 \ {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\{P. eventually P F}. Inf (g ` Collect P)) = + Inf (f ` (\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 \ {P. eventually P F}. f (Inf (g ` Collect P)))" + by (simp add: Liminf_def image_comp) also have "\ = (INF P \ {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 \ Liminf F (\x. g (f x))" diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Option_ord.thy --- 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 (\x\A. f x) = (\x\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 \ {} \ Some (\x\A. f x) = (\x\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: "\(Sup ` A) \ \(Inf ` {f ` A |f. \Y\A. f Y \ Y})" for A :: "('a::complete_distrib_lattice option) set set" diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Order_Continuity.thy --- 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 (\f. f x)" and sup_continuous_fun: "(\s. sup_continuous (\x. P x s)) \ sup_continuous P" and sup_continuous_If: "sup_continuous F \ sup_continuous G \ sup_continuous (\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 (\f. f x)" and inf_continuous_fun: "(\s. inf_continuous (\x. P x s)) \ inf_continuous P" and inf_continuous_If: "inf_continuous F \ inf_continuous G \ inf_continuous (\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 \ inf_continuous g \ inf_continuous (\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 "\ = F (cclfp F)" unfolding cclfp_def by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono) diff -r b58a575d211e -r 62e47f06d22c src/HOL/Library/Product_Order.thy --- 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\A. fst x)" - unfolding Sup_prod_def by simp - -lemma snd_Sup: "snd (Sup A) = (SUP x\A. snd x)" - unfolding Sup_prod_def by simp +lemma fst_Inf: "fst (Inf A) = (INF x\A. fst x)" + by (simp add: Inf_prod_def) -lemma fst_Inf: "fst (Inf A) = (INF x\A. fst x)" - unfolding Inf_prod_def by simp +lemma fst_INF: "fst (INF x\A. f x) = (INF x\A. fst (f x))" + by (simp add: fst_Inf image_image) -lemma snd_Inf: "snd (Inf A) = (INF x\A. snd x)" - unfolding Inf_prod_def by simp +lemma fst_Sup: "fst (Sup A) = (SUP x\A. fst x)" + by (simp add: Sup_prod_def) lemma fst_SUP: "fst (SUP x\A. f x) = (SUP x\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\A. snd x)" + by (simp add: Inf_prod_def) + +lemma snd_INF: "snd (INF x\A. f x) = (INF x\A. snd (f x))" + by (simp add: snd_Inf image_image) + +lemma snd_Sup: "snd (Sup A) = (SUP x\A. snd x)" + by (simp add: Sup_prod_def) lemma snd_SUP: "snd (SUP x\A. f x) = (SUP x\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\A. f x) = (INF x\A. fst (f x))" - using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def) - -lemma snd_INF: "snd (INF x\A. f x) = (INF x\A. snd (f x))" - using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def) +lemma INF_Pair: "(INF x\A. (f x, g x)) = (INF x\A. f x, INF x\A. g x)" + by (simp add: Inf_prod_def image_image) lemma SUP_Pair: "(SUP x\A. (f x, g x)) = (SUP x\A. f x, SUP x\A. g x)" - unfolding Sup_prod_def by (simp add: comp_def) - -lemma INF_Pair: "(INF x\A. (f x, g x)) = (INF x\A. f x, INF x\A. g x)" - unfolding Inf_prod_def by (simp add: comp_def) + by (simp add: Sup_prod_def image_image) text \Alternative formulations for set infima and suprema over the product @@ -221,11 +221,11 @@ lemma INF_prod_alt_def: "Inf (f ` A) = (Inf ((fst \ f) ` A), Inf ((snd \ 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 \ f) ` A), Sup((snd \ f) ` A))" - unfolding Sup_prod_def by simp + by (simp add: Sup_prod_def image_image) subsection \Complete distributive lattices\ @@ -236,7 +236,7 @@ proof fix A::"('a\'b) set set" show "Inf (Sup ` A) \ Sup (Inf ` {f ` A |f. \Y\A. f Y \ 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 \Bekic's Theorem\ diff -r b58a575d211e -r 62e47f06d22c src/HOL/Predicate.thy --- 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 (\