avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
authorhaftmann
Tue Mar 05 07:00:21 2019 +0000 (3 months ago ago)
changeset 7004262e47f06d22c
parent 70041 b58a575d211e
child 70046 c28da0820b8b
avoid context-sensitive simp rules whose context-free form (image_comp) is not simp by default
NEWS
src/HOL/Analysis/Binary_Product_Measure.thy
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Bounded_Continuous_Function.thy
src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
src/HOL/Analysis/Measurable.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Tagged_Division.thy
src/HOL/Complete_Lattices.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Library/Extended_Nat.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/Order_Continuity.thy
src/HOL/Library/Product_Order.thy
src/HOL/Predicate.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Helly_Selection.thy
src/HOL/Probability/SPMF.thy
     1.1 --- a/NEWS	Sun Mar 03 20:27:42 2019 +0100
     1.2 +++ b/NEWS	Tue Mar 05 07:00:21 2019 +0000
     1.3 @@ -135,6 +135,9 @@
     1.4  are not used by default any longer.  INCOMPATIBILITY; consider using
     1.5  declare image_cong_simp [cong del] in extreme situations.
     1.6  
     1.7 +* INF_image and SUP_image are no default simp rules any longer.
     1.8 +INCOMPATIBILITY, prefer image_comp as simp rule if needed.
     1.9 +
    1.10  * Simplified syntax setup for big operators under image. In rare
    1.11  situations, type conversions are not inserted implicitly any longer
    1.12  and need to be given explicitly. Auxiliary abbreviations INFIMUM,
     2.1 --- a/src/HOL/Analysis/Binary_Product_Measure.thy	Sun Mar 03 20:27:42 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Binary_Product_Measure.thy	Tue Mar 05 07:00:21 2019 +0000
     2.3 @@ -558,7 +558,7 @@
     2.4    from this measurable_emeasure_Pair[OF set] show ?case
     2.5      by (rule measurable_cong[THEN iffD1])
     2.6  qed (simp_all add: nn_integral_add nn_integral_cmult measurable_compose_Pair1
     2.7 -                   nn_integral_monotone_convergence_SUP incseq_def le_fun_def
     2.8 +                   nn_integral_monotone_convergence_SUP incseq_def le_fun_def image_comp
     2.9                cong: measurable_cong)
    2.10  
    2.11  lemma (in sigma_finite_measure) nn_integral_fst:
    2.12 @@ -572,7 +572,7 @@
    2.13      by (simp cong: nn_integral_cong)
    2.14  qed (simp_all add: emeasure_pair_measure nn_integral_cmult nn_integral_add
    2.15                     nn_integral_monotone_convergence_SUP measurable_compose_Pair1
    2.16 -                   borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def
    2.17 +                   borel_measurable_nn_integral_fst nn_integral_mono incseq_def le_fun_def image_comp
    2.18                cong: nn_integral_cong)
    2.19  
    2.20  lemma (in sigma_finite_measure) borel_measurable_nn_integral[measurable (raw)]:
     3.1 --- a/src/HOL/Analysis/Borel_Space.thy	Sun Mar 03 20:27:42 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Tue Mar 05 07:00:21 2019 +0000
     3.3 @@ -228,7 +228,7 @@
     3.4  proof -
     3.5    have "Inf (uminus ` S) \<in> closure (uminus ` S)"
     3.6        using assms by (intro closure_contains_Inf) auto
     3.7 -  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def)
     3.8 +  also have "Inf (uminus ` S) = -Sup S" by (simp add: Inf_real_def image_comp)
     3.9    also have "closure (uminus ` S) = uminus ` closure S"
    3.10        by (rule sym, intro closure_injective_linear_image) (auto intro: linearI)
    3.11    finally show ?thesis by auto
    3.12 @@ -876,7 +876,7 @@
    3.13    then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> borel_measurable M"
    3.14      by measurable
    3.15    also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = (SUP i. (F ^^ i) bot)"
    3.16 -    by auto
    3.17 +    by (auto simp add: image_comp)
    3.18    also have "(SUP i. (F ^^ i) bot) = lfp F"
    3.19      by (rule sup_continuous_lfp[symmetric]) fact
    3.20    finally show ?thesis .
    3.21 @@ -893,7 +893,7 @@
    3.22    then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> borel_measurable M"
    3.23      by measurable
    3.24    also have "(\<lambda>x. INF i. (F ^^ i) top x) = (INF i. (F ^^ i) top)"
    3.25 -    by auto
    3.26 +    by (auto simp add: image_comp)
    3.27    also have "\<dots> = gfp F"
    3.28      by (rule inf_continuous_gfp[symmetric]) fact
    3.29    finally show ?thesis .
     4.1 --- a/src/HOL/Analysis/Bounded_Continuous_Function.thy	Sun Mar 03 20:27:42 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy	Tue Mar 05 07:00:21 2019 +0000
     4.3 @@ -272,7 +272,7 @@
     4.4      apply transfer
     4.5      by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
     4.6        (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
     4.7 -        simp: bounded_norm_comp bcontfun_def)
     4.8 +        simp: bounded_norm_comp bcontfun_def image_comp)
     4.9  qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
    4.10  
    4.11  end
     5.1 --- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Sun Mar 03 20:27:42 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue Mar 05 07:00:21 2019 +0000
     5.3 @@ -274,7 +274,7 @@
     5.4      also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ennreal (g' x) * indicator {a..b} x \<partial>lborel"
     5.5        by (subst mult.assoc, subst mult.commute, subst SUP_mult_left_ennreal)
     5.6           (auto split: split_indicator simp: derivg_nonneg mult_ac)
     5.7 -    finally show ?case by simp
     5.8 +    finally show ?case by (simp add: image_comp)
     5.9    qed
    5.10  qed
    5.11  
     6.1 --- a/src/HOL/Analysis/Measurable.thy	Sun Mar 03 20:27:42 2019 +0100
     6.2 +++ b/src/HOL/Analysis/Measurable.thy	Tue Mar 05 07:00:21 2019 +0000
     6.3 @@ -432,7 +432,7 @@
     6.4    then have "(\<lambda>x. SUP i. (F ^^ i) bot x) \<in> measurable M (count_space UNIV)"
     6.5      by measurable
     6.6    also have "(\<lambda>x. SUP i. (F ^^ i) bot x) = lfp F"
     6.7 -    by (subst sup_continuous_lfp) (auto intro: F)
     6.8 +    by (subst sup_continuous_lfp) (auto intro: F simp: image_comp)
     6.9    finally show ?thesis .
    6.10  qed
    6.11  
    6.12 @@ -455,7 +455,7 @@
    6.13    then have "(\<lambda>x. INF i. (F ^^ i) top x) \<in> measurable M (count_space UNIV)"
    6.14      by measurable
    6.15    also have "(\<lambda>x. INF i. (F ^^ i) top x) = gfp F"
    6.16 -    by (subst inf_continuous_gfp) (auto intro: F)
    6.17 +    by (subst inf_continuous_gfp) (auto intro: F simp: image_comp)
    6.18    finally show ?thesis .
    6.19  qed
    6.20  
    6.21 @@ -478,7 +478,7 @@
    6.22    then have "(\<lambda>x. SUP i. (F ^^ i) bot s x) \<in> measurable M (count_space UNIV)"
    6.23      by measurable
    6.24    also have "(\<lambda>x. SUP i. (F ^^ i) bot s x) = lfp F s"
    6.25 -    by (subst sup_continuous_lfp) (auto simp: F)
    6.26 +    by (subst sup_continuous_lfp) (auto simp: F simp: image_comp)
    6.27    finally show ?thesis .
    6.28  qed
    6.29  
    6.30 @@ -494,7 +494,7 @@
    6.31    then have "(\<lambda>x. INF i. (F ^^ i) top s x) \<in> measurable M (count_space UNIV)"
    6.32      by measurable
    6.33    also have "(\<lambda>x. INF i. (F ^^ i) top s x) = gfp F s"
    6.34 -    by (subst inf_continuous_gfp) (auto simp: F)
    6.35 +    by (subst inf_continuous_gfp) (auto simp: F simp: image_comp)
    6.36    finally show ?thesis .
    6.37  qed
    6.38  
     7.1 --- a/src/HOL/Analysis/Measure_Space.thy	Sun Mar 03 20:27:42 2019 +0100
     7.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Tue Mar 05 07:00:21 2019 +0000
     7.3 @@ -3571,7 +3571,7 @@
     7.4    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))}"
     7.5      by auto
     7.6    ultimately show ?thesis
     7.7 -    using assms by (auto simp: Sup_lexord_def Let_def)
     7.8 +    using assms by (auto simp: Sup_lexord_def Let_def image_comp)
     7.9  qed
    7.10  
    7.11  lemma sets_SUP_cong:
    7.12 @@ -3674,7 +3674,7 @@
    7.13  
    7.14  lemma SUP_sigma_sigma:
    7.15    "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)"
    7.16 -  using Sup_sigma[of "f`M" \<Omega>] by auto
    7.17 +  using Sup_sigma[of "f`M" \<Omega>] by (auto simp: image_comp)
    7.18  
    7.19  lemma sets_vimage_Sup_eq:
    7.20    assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
     8.1 --- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Sun Mar 03 20:27:42 2019 +0100
     8.2 +++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy	Tue Mar 05 07:00:21 2019 +0000
     8.3 @@ -386,7 +386,7 @@
     8.4          by (simp add: real)
     8.5      qed }
     8.6    ultimately show ?thesis
     8.7 -    by (intro exI[of _ "\<lambda>i x. ennreal (f i x)"]) auto
     8.8 +    by (intro exI [of _ "\<lambda>i x. ennreal (f i x)"]) (auto simp add: image_comp)
     8.9  qed
    8.10  
    8.11  lemma borel_measurable_implies_simple_function_sequence':
    8.12 @@ -394,7 +394,8 @@
    8.13    assumes u: "u \<in> borel_measurable M"
    8.14    obtains f where
    8.15      "\<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"
    8.16 -  using borel_measurable_implies_simple_function_sequence[OF u] by (auto simp: fun_eq_iff) blast
    8.17 +  using borel_measurable_implies_simple_function_sequence [OF u]
    8.18 +  by (metis SUP_apply)
    8.19  
    8.20  lemma%important simple_function_induct
    8.21      [consumes 1, case_names cong set mult add, induct set: simple_function]:
    8.22 @@ -481,7 +482,7 @@
    8.23  proof%unimportant (induct rule: borel_measurable_implies_simple_function_sequence')
    8.24    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"
    8.25    have u_eq: "u = (SUP i. U i)"
    8.26 -    using u sup by auto
    8.27 +    using u by (auto simp add: image_comp sup)
    8.28  
    8.29    have not_inf: "\<And>x i. x \<in> space M \<Longrightarrow> U i x < top"
    8.30      using U by (auto simp: image_iff eq_commute)
    8.31 @@ -1538,7 +1539,7 @@
    8.32      using N by auto
    8.33    from f show ?thesis
    8.34      apply induct
    8.35 -    apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N)
    8.36 +    apply (simp_all add: nn_integral_add nn_integral_cmult nn_integral_monotone_convergence_SUP N image_comp)
    8.37      apply (auto intro!: nn_integral_cong cong: nn_integral_cong simp: N(2)[symmetric])
    8.38      done
    8.39  qed
    8.40 @@ -1667,7 +1668,7 @@
    8.41      by (subst nn_integral_cong[OF eq])
    8.42         (auto simp add: emeasure_distr intro!: nn_integral_indicator[symmetric] measurable_sets)
    8.43  qed (simp_all add: measurable_compose[OF T] T nn_integral_cmult nn_integral_add
    8.44 -                   nn_integral_monotone_convergence_SUP le_fun_def incseq_def)
    8.45 +                   nn_integral_monotone_convergence_SUP le_fun_def incseq_def image_comp)
    8.46  
    8.47  subsubsection%unimportant \<open>Counting space\<close>
    8.48  
    8.49 @@ -2198,7 +2199,7 @@
    8.50    have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
    8.51      by eventually_elim (simp add: SUP_mult_left_ennreal seq)
    8.52    from seq f show ?case
    8.53 -    apply (simp add: nn_integral_monotone_convergence_SUP)
    8.54 +    apply (simp add: nn_integral_monotone_convergence_SUP image_comp)
    8.55      apply (subst nn_integral_cong_AE[OF eq])
    8.56      apply (subst nn_integral_monotone_convergence_SUP_AE)
    8.57      apply (auto simp: incseq_def le_fun_def intro!: mult_left_mono)
    8.58 @@ -2500,7 +2501,7 @@
    8.59  next
    8.60    case (seq U)
    8.61    thus ?case
    8.62 -    by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal)
    8.63 +    by(simp add: nn_integral_monotone_convergence_SUP SUP_mult_left_ennreal image_comp)
    8.64  qed simp
    8.65  
    8.66  end
     9.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Sun Mar 03 20:27:42 2019 +0100
     9.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Mar 05 07:00:21 2019 +0000
     9.3 @@ -53,7 +53,7 @@
     9.4  
     9.5  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)"
     9.6    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)"
     9.7 -  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
     9.8 +  using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: image_comp)
     9.9  
    9.10  lemma abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
    9.11    by (auto simp: eucl_abs)
    10.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Sun Mar 03 20:27:42 2019 +0100
    10.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Mar 05 07:00:21 2019 +0000
    10.3 @@ -170,10 +170,10 @@
    10.4  proof-
    10.5    from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
    10.6    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)"
    10.7 -      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
    10.8 +      by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
    10.9    moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   10.10    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)"
   10.11 -      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   10.12 +      by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp inner_Pair_0)
   10.13    ultimately show ?thesis unfolding interval_upperbound_def
   10.14        by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
   10.15  qed
   10.16 @@ -184,10 +184,10 @@
   10.17  proof-
   10.18    from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
   10.19    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)"
   10.20 -      by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
   10.21 +      by (subst (2) fst_image_times') (simp del: fst_image_times add: image_comp inner_Pair_0)
   10.22    moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
   10.23    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)"
   10.24 -      by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
   10.25 +      by (subst (2) snd_image_times') (simp del: snd_image_times add: image_comp inner_Pair_0)
   10.26    ultimately show ?thesis unfolding interval_lowerbound_def
   10.27        by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
   10.28  qed
    11.1 --- a/src/HOL/Complete_Lattices.thy	Sun Mar 03 20:27:42 2019 +0100
    11.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Mar 05 07:00:21 2019 +0000
    11.3 @@ -49,7 +49,7 @@
    11.4  context Inf
    11.5  begin
    11.6  
    11.7 -lemma INF_image [simp]: " \<Sqinter>(g ` f ` A) = \<Sqinter>((g \<circ> f) ` A)"
    11.8 +lemma INF_image: "\<Sqinter> (g ` f ` A) = \<Sqinter> ((g \<circ> f) ` A)"
    11.9    by (simp add: image_comp)
   11.10  
   11.11  lemma INF_identity_eq [simp]: "(\<Sqinter>x\<in>A. x) = \<Sqinter>A"
   11.12 @@ -70,7 +70,7 @@
   11.13  context Sup
   11.14  begin
   11.15  
   11.16 -lemma SUP_image [simp]: "\<Squnion>(g ` f ` A) = \<Squnion>((g \<circ> f) ` A)"
   11.17 +lemma SUP_image: "\<Squnion> (g ` f ` A) = \<Squnion> ((g \<circ> f) ` A)"
   11.18  by(fact Inf.INF_image)
   11.19  
   11.20  lemma SUP_identity_eq [simp]: "(\<Squnion>x\<in>A. x) = \<Squnion>A"
   11.21 @@ -677,10 +677,10 @@
   11.22  end
   11.23  
   11.24  lemma INF_apply [simp]: "(\<Sqinter>y\<in>A. f y) x = (\<Sqinter>y\<in>A. f y x)"
   11.25 -  using Inf_apply [of "f ` A"] by (simp add: comp_def)
   11.26 +  by (simp add: image_comp)
   11.27  
   11.28  lemma SUP_apply [simp]: "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   11.29 -  using Sup_apply [of "f ` A"] by (simp add: comp_def)
   11.30 +  by (simp add: image_comp)
   11.31  
   11.32  subsection \<open>Complete lattice on unary and binary predicates\<close>
   11.33  
    12.1 --- a/src/HOL/Hilbert_Choice.thy	Sun Mar 03 20:27:42 2019 +0100
    12.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Mar 05 07:00:21 2019 +0000
    12.3 @@ -1025,7 +1025,7 @@
    12.4      for f and B
    12.5      using that by (auto intro: SUP_upper2 INF_lower2)
    12.6    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)"
    12.7 -    by (auto intro!: SUP_least INF_greatest)
    12.8 +    by (auto intro!: SUP_least INF_greatest simp add: image_comp)
    12.9  next
   12.10    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)"
   12.11    proof (cases "{} \<in> A")
   12.12 @@ -1103,10 +1103,10 @@
   12.13  begin
   12.14  
   12.15  lemma sup_INF: "a \<squnion> (\<Sqinter>b\<in>B. f b) = (\<Sqinter>b\<in>B. a \<squnion> f b)"
   12.16 -  by (simp add: sup_Inf)
   12.17 +  by (simp add: sup_Inf image_comp)
   12.18  
   12.19  lemma inf_SUP: "a \<sqinter> (\<Squnion>b\<in>B. f b) = (\<Squnion>b\<in>B. a \<sqinter> f b)"
   12.20 -  by (simp add: inf_Sup)
   12.21 +  by (simp add: inf_Sup image_comp)
   12.22  
   12.23  lemma Inf_sup: "\<Sqinter>B \<squnion> a = (\<Sqinter>b\<in>B. b \<squnion> a)"
   12.24    by (simp add: sup_Inf sup_commute)
   12.25 @@ -1175,7 +1175,7 @@
   12.26  
   12.27  instantiation "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice
   12.28  begin
   12.29 -instance by standard (simp add: le_fun_def INF_SUP_set)
   12.30 +instance by standard (simp add: le_fun_def INF_SUP_set image_comp)
   12.31  end
   12.32  
   12.33  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
    13.1 --- a/src/HOL/Library/Extended_Nat.thy	Sun Mar 03 20:27:42 2019 +0100
    13.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Mar 05 07:00:21 2019 +0000
    13.3 @@ -678,7 +678,8 @@
    13.4    by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)
    13.5  
    13.6  lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))"
    13.7 -  using  eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def)
    13.8 +  using eSuc_Sup [of "_ ` UNIV"] by (auto simp: sup_continuous_def image_comp)
    13.9 +
   13.10  
   13.11  subsection \<open>Traditional theorem names\<close>
   13.12  
    14.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Mar 03 20:27:42 2019 +0100
    14.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Tue Mar 05 07:00:21 2019 +0000
    14.3 @@ -109,7 +109,7 @@
    14.4    fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
    14.5    assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
    14.6    shows  "sup_continuous (SUP i\<in>I. M i)"
    14.7 -  unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
    14.8 +  unfolding sup_continuous_def by (auto simp add: sup_continuousD [OF M] image_comp intro: SUP_commute)
    14.9  
   14.10  lemma sup_continuous_apply_SUP[order_continuous_intros]:
   14.11    fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
   14.12 @@ -1410,7 +1410,7 @@
   14.13    shows "(INF i. f i + c) = (INF i. f i) + c"
   14.14    using continuous_at_Inf_mono[of "\<lambda>x. x + c" "f`UNIV"]
   14.15    using continuous_add[of "at_right (Inf (range f))", of "\<lambda>x. x" "\<lambda>x. c"]
   14.16 -  by (auto simp: mono_def)
   14.17 +  by (auto simp: mono_def image_comp)
   14.18  
   14.19  lemma INF_ennreal_const_add:
   14.20    fixes f g :: "nat \<Rightarrow> ennreal"
   14.21 @@ -1609,9 +1609,9 @@
   14.22    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)"
   14.23      by auto
   14.24    have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
   14.25 -    unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
   14.26 +    unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by (simp add: image_comp)
   14.27    also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
   14.28 -    by (insert M, drule SUP_subset_mono) auto
   14.29 +    by (insert M, drule SUP_subset_mono) (auto simp add: image_comp)
   14.30    finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
   14.31  qed
   14.32  
    15.1 --- a/src/HOL/Library/Extended_Real.thy	Sun Mar 03 20:27:42 2019 +0100
    15.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 05 07:00:21 2019 +0000
    15.3 @@ -41,7 +41,7 @@
    15.4    unfolding sup_continuous_def
    15.5  proof safe
    15.6    fix M :: "nat \<Rightarrow> 'a" assume "incseq M" then show "f (SUP i. M i) = (SUP i. f (M i))"
    15.7 -    using continuous_at_Sup_mono[OF assms, of "range M"] by simp
    15.8 +    using continuous_at_Sup_mono [OF assms, of "range M"] by (simp add: image_comp)
    15.9  qed
   15.10  
   15.11  lemma sup_continuous_at_left:
   15.12 @@ -80,7 +80,7 @@
   15.13    unfolding inf_continuous_def
   15.14  proof safe
   15.15    fix M :: "nat \<Rightarrow> 'a" assume "decseq M" then show "f (INF i. M i) = (INF i. f (M i))"
   15.16 -    using continuous_at_Inf_mono[OF assms, of "range M"] by simp
   15.17 +    using continuous_at_Inf_mono [OF assms, of "range M"] by (simp add: image_comp)
   15.18  qed
   15.19  
   15.20  lemma inf_continuous_at_right:
   15.21 @@ -2158,7 +2158,7 @@
   15.22  qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
   15.23  
   15.24  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))"
   15.25 -  using ereal_Sup[of "f`A"] by auto
   15.26 +  by (simp add: ereal_Sup image_comp)
   15.27  
   15.28  lemma ereal_Inf:
   15.29    assumes *: "\<bar>INF a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
   15.30 @@ -2183,7 +2183,7 @@
   15.31  qed
   15.32  
   15.33  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))"
   15.34 -  using ereal_Inf[of "f`A"] by auto
   15.35 +  by (simp add: ereal_Inf image_comp)
   15.36  
   15.37  lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
   15.38    by (auto intro!: SUP_eqI
   15.39 @@ -2193,7 +2193,7 @@
   15.40  lemma ereal_SUP_uminus_eq:
   15.41    fixes f :: "'a \<Rightarrow> ereal"
   15.42    shows "(SUP x\<in>S. uminus (f x)) = - (INF x\<in>S. f x)"
   15.43 -  using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
   15.44 +  using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: image_comp)
   15.45  
   15.46  lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
   15.47    by (auto intro!: inj_onI)
   15.48 @@ -2204,7 +2204,7 @@
   15.49  lemma ereal_INF_uminus_eq:
   15.50    fixes f :: "'a \<Rightarrow> ereal"
   15.51    shows "(INF x\<in>S. - f x) = - (SUP x\<in>S. f x)"
   15.52 -  using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
   15.53 +  using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: image_comp)
   15.54  
   15.55  lemma ereal_SUP_uminus:
   15.56    fixes f :: "'a \<Rightarrow> ereal"
   15.57 @@ -2297,7 +2297,8 @@
   15.58    case False
   15.59    then show ?thesis
   15.60      by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
   15.61 -       (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close>)
   15.62 +      (auto simp: continuous_at_imp_continuous_at_within continuous_at mono_def add_mono \<open>I \<noteq> {}\<close>
   15.63 +      \<open>c \<noteq> -\<infinity>\<close> image_comp)
   15.64  qed
   15.65  
   15.66  lemma SUP_ereal_add_right:
   15.67 @@ -2370,7 +2371,8 @@
   15.68      unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
   15.69    then show ?thesis
   15.70      by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
   15.71 -       (auto simp: mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within continuous_at)
   15.72 +       (auto simp: mono_def add_mono \<open>I \<noteq> {}\<close> \<open>c \<noteq> -\<infinity>\<close> continuous_at_imp_continuous_at_within
   15.73 +        continuous_at image_comp)
   15.74  qed
   15.75  
   15.76  lemma INF_ereal_add_right:
   15.77 @@ -2464,7 +2466,7 @@
   15.78    case False
   15.79    then show ?thesis
   15.80      by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
   15.81 -       (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close>
   15.82 +       (auto simp: mono_def continuous_at continuous_at_imp_continuous_at_within \<open>I \<noteq> {}\<close> image_comp
   15.83               intro!: ereal_mult_left_mono c)
   15.84  qed
   15.85  
   15.86 @@ -2626,7 +2628,8 @@
   15.87  
   15.88  lemma ereal_of_enat_SUP:
   15.89    "A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a\<in>A. f a) = (SUP a \<in> A. ereal_of_enat (f a))"
   15.90 -  using ereal_of_enat_Sup[of "f`A"] by auto
   15.91 +  by (simp add: ereal_of_enat_Sup image_comp)
   15.92 +
   15.93  
   15.94  subsection "Limits on \<^typ>\<open>ereal\<close>"
   15.95  
    16.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Sun Mar 03 20:27:42 2019 +0100
    16.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 05 07:00:21 2019 +0000
    16.3 @@ -435,14 +435,16 @@
    16.4      qed }
    16.5    note * = this
    16.6  
    16.7 -  have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
    16.8 -    unfolding Liminf_def
    16.9 -    by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
   16.10 -       (auto intro: eventually_True)
   16.11 +  have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
   16.12 +    Sup (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
   16.13 +    using am continuous_on_imp_continuous_within [OF c]
   16.14 +    by (rule continuous_at_Sup_mono) (auto intro: eventually_True)
   16.15 +  then have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
   16.16 +    by (simp add: Liminf_def image_comp)
   16.17    also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
   16.18      using * continuous_at_Inf_mono [OF am continuous_on_imp_continuous_within [OF c]]
   16.19      by auto 
   16.20 -  finally show ?thesis by (auto simp: Liminf_def)
   16.21 +  finally show ?thesis by (auto simp: Liminf_def image_comp)
   16.22  qed
   16.23  
   16.24  lemma Limsup_compose_continuous_mono:
   16.25 @@ -460,14 +462,16 @@
   16.26      qed }
   16.27    note * = this
   16.28  
   16.29 -  have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
   16.30 -    unfolding Limsup_def
   16.31 -    by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
   16.32 -       (auto intro: eventually_True)
   16.33 +  have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
   16.34 +    Inf (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
   16.35 +    using am continuous_on_imp_continuous_within [OF c]
   16.36 +    by (rule continuous_at_Inf_mono) (auto intro: eventually_True)
   16.37 +  then have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
   16.38 +    by (simp add: Limsup_def image_comp)
   16.39    also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
   16.40      using * continuous_at_Sup_mono [OF am continuous_on_imp_continuous_within [OF c]]
   16.41      by auto
   16.42 -  finally show ?thesis by (auto simp: Limsup_def)
   16.43 +  finally show ?thesis by (auto simp: Limsup_def image_comp)
   16.44  qed
   16.45  
   16.46  lemma Liminf_compose_continuous_antimono:
   16.47 @@ -484,15 +488,18 @@
   16.48      with \<open>eventually P F\<close> F show False
   16.49        by auto
   16.50    qed
   16.51 -  have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
   16.52 -    unfolding Limsup_def
   16.53 -    by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   16.54 -       (auto intro: eventually_True)
   16.55 +
   16.56 +  have "f (INF P\<in>{P. eventually P F}. Sup (g ` Collect P)) =
   16.57 +    Sup (f ` (\<lambda>P. Sup (g ` Collect P)) ` {P. eventually P F})"
   16.58 +    using am continuous_on_imp_continuous_within [OF c]
   16.59 +    by (rule continuous_at_Inf_antimono) (auto intro: eventually_True)
   16.60 +  then have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
   16.61 +    by (simp add: Limsup_def image_comp)
   16.62    also have "\<dots> = (SUP P \<in> {P. eventually P F}. Inf (f ` (g ` Collect P)))"
   16.63      using * continuous_at_Sup_antimono [OF am continuous_on_imp_continuous_within [OF c]]
   16.64      by auto
   16.65    finally show ?thesis
   16.66 -    by (auto simp: Liminf_def)
   16.67 +    by (auto simp: Liminf_def image_comp)
   16.68  qed
   16.69  
   16.70  lemma Limsup_compose_continuous_antimono:
   16.71 @@ -510,15 +517,17 @@
   16.72      qed }
   16.73    note * = this
   16.74  
   16.75 -  have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
   16.76 -    unfolding Liminf_def
   16.77 -    by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
   16.78 -       (auto intro: eventually_True)
   16.79 +  have "f (SUP P\<in>{P. eventually P F}. Inf (g ` Collect P)) =
   16.80 +    Inf (f ` (\<lambda>P. Inf (g ` Collect P)) ` {P. eventually P F})"
   16.81 +    using am continuous_on_imp_continuous_within [OF c]
   16.82 +    by (rule continuous_at_Sup_antimono) (auto intro: eventually_True)
   16.83 +  then have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
   16.84 +    by (simp add: Liminf_def image_comp)
   16.85    also have "\<dots> = (INF P \<in> {P. eventually P F}. Sup (f ` (g ` Collect P)))"
   16.86      using * continuous_at_Inf_antimono [OF am continuous_on_imp_continuous_within [OF c]]
   16.87      by auto
   16.88    finally show ?thesis
   16.89 -    by (auto simp: Limsup_def)
   16.90 +    by (auto simp: Limsup_def image_comp)
   16.91  qed
   16.92  
   16.93  lemma Liminf_filtermap_le: "Liminf (filtermap f F) g \<le> Liminf F (\<lambda>x. g (f x))"
    17.1 --- a/src/HOL/Library/Option_ord.thy	Sun Mar 03 20:27:42 2019 +0100
    17.2 +++ b/src/HOL/Library/Option_ord.thy	Tue Mar 05 07:00:21 2019 +0000
    17.3 @@ -277,11 +277,11 @@
    17.4  
    17.5  lemma Some_INF:
    17.6    "Some (\<Sqinter>x\<in>A. f x) = (\<Sqinter>x\<in>A. Some (f x))"
    17.7 -  using Some_Inf [of "f ` A"] by (simp add: comp_def)
    17.8 +  by (simp add: Some_Inf image_comp)
    17.9  
   17.10  lemma Some_SUP:
   17.11    "A \<noteq> {} \<Longrightarrow> Some (\<Squnion>x\<in>A. f x) = (\<Squnion>x\<in>A. Some (f x))"
   17.12 -  using Some_Sup [of "f ` A"] by (simp add: comp_def)
   17.13 +  by (simp add: Some_Sup image_comp)
   17.14  
   17.15  lemma option_Inf_Sup: "\<Sqinter>(Sup ` A) \<le> \<Squnion>(Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   17.16    for A :: "('a::complete_distrib_lattice option) set set"
    18.1 --- a/src/HOL/Library/Order_Continuity.thy	Sun Mar 03 20:27:42 2019 +0100
    18.2 +++ b/src/HOL/Library/Order_Continuity.thy	Tue Mar 05 07:00:21 2019 +0000
    18.3 @@ -68,7 +68,7 @@
    18.4      and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
    18.5      and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
    18.6      and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
    18.7 -  by (auto simp: sup_continuous_def)
    18.8 +  by (auto simp: sup_continuous_def image_comp)
    18.9  
   18.10  lemma sup_continuous_compose:
   18.11    assumes f: "sup_continuous f" and g: "sup_continuous g"
   18.12 @@ -242,7 +242,7 @@
   18.13      and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
   18.14      and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
   18.15      and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
   18.16 -  by (auto simp: inf_continuous_def)
   18.17 +  by (auto simp: inf_continuous_def image_comp)
   18.18  
   18.19  lemma inf_continuous_inf[order_continuous_intros]:
   18.20    "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
   18.21 @@ -412,7 +412,8 @@
   18.22    assumes "sup_continuous F" shows "cclfp F = F (cclfp F)"
   18.23  proof -
   18.24    have "cclfp F = (SUP i. F ((F ^^ i) bot))"
   18.25 -    unfolding cclfp_def by (subst UNIV_nat_eq) auto
   18.26 +    unfolding cclfp_def
   18.27 +    by (subst UNIV_nat_eq) (simp add: image_comp)
   18.28    also have "\<dots> = F (cclfp F)"
   18.29      unfolding cclfp_def
   18.30      by (intro sup_continuousD[symmetric] assms mono_funpow sup_continuous_mono)
    19.1 --- a/src/HOL/Library/Product_Order.thy	Sun Mar 03 20:27:42 2019 +0100
    19.2 +++ b/src/HOL/Library/Product_Order.thy	Tue Mar 05 07:00:21 2019 +0000
    19.3 @@ -185,35 +185,35 @@
    19.4    by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
    19.5      INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
    19.6  
    19.7 -lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)"
    19.8 -  unfolding Sup_prod_def by simp
    19.9 -
   19.10 -lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)"
   19.11 -  unfolding Sup_prod_def by simp
   19.12 +lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)"
   19.13 +  by (simp add: Inf_prod_def)
   19.14  
   19.15 -lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)"
   19.16 -  unfolding Inf_prod_def by simp
   19.17 +lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))"
   19.18 +  by (simp add: fst_Inf image_image)
   19.19  
   19.20 -lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)"
   19.21 -  unfolding Inf_prod_def by simp
   19.22 +lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)"
   19.23 +  by (simp add: Sup_prod_def)
   19.24  
   19.25  lemma fst_SUP: "fst (SUP x\<in>A. f x) = (SUP x\<in>A. fst (f x))"
   19.26 -  using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
   19.27 +  by (simp add: fst_Sup image_image)
   19.28 +
   19.29 +lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)"
   19.30 +  by (simp add: Inf_prod_def)
   19.31 +
   19.32 +lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))"
   19.33 +  by (simp add: snd_Inf image_image)
   19.34 +
   19.35 +lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)"
   19.36 +  by (simp add: Sup_prod_def)
   19.37  
   19.38  lemma snd_SUP: "snd (SUP x\<in>A. f x) = (SUP x\<in>A. snd (f x))"
   19.39 -  using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
   19.40 +  by (simp add: snd_Sup image_image)
   19.41  
   19.42 -lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))"
   19.43 -  using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
   19.44 -
   19.45 -lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))"
   19.46 -  using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
   19.47 +lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)"
   19.48 +  by (simp add: Inf_prod_def image_image)
   19.49  
   19.50  lemma SUP_Pair: "(SUP x\<in>A. (f x, g x)) = (SUP x\<in>A. f x, SUP x\<in>A. g x)"
   19.51 -  unfolding Sup_prod_def by (simp add: comp_def)
   19.52 -
   19.53 -lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)"
   19.54 -  unfolding Inf_prod_def by (simp add: comp_def)
   19.55 +  by (simp add: Sup_prod_def image_image)
   19.56  
   19.57  
   19.58  text \<open>Alternative formulations for set infima and suprema over the product
   19.59 @@ -221,11 +221,11 @@
   19.60  
   19.61  lemma INF_prod_alt_def:
   19.62    "Inf (f ` A) = (Inf ((fst \<circ> f) ` A), Inf ((snd \<circ> f) ` A))"
   19.63 -  unfolding Inf_prod_def by simp
   19.64 +  by (simp add: Inf_prod_def image_image)
   19.65  
   19.66  lemma SUP_prod_alt_def:
   19.67    "Sup (f ` A) = (Sup ((fst \<circ> f) ` A), Sup((snd \<circ> f) ` A))"
   19.68 -  unfolding Sup_prod_def by simp
   19.69 +  by (simp add: Sup_prod_def image_image)
   19.70  
   19.71  
   19.72  subsection \<open>Complete distributive lattices\<close>
   19.73 @@ -236,7 +236,7 @@
   19.74  proof
   19.75    fix A::"('a\<times>'b) set set"
   19.76    show "Inf (Sup ` A) \<le> Sup (Inf ` {f ` A |f. \<forall>Y\<in>A. f Y \<in> Y})"
   19.77 -    by (simp add: Sup_prod_def Inf_prod_def INF_SUP_set)
   19.78 +    by (simp add: Inf_prod_def Sup_prod_def INF_SUP_set image_image)
   19.79  qed
   19.80  
   19.81  subsection \<open>Bekic's Theorem\<close>
    20.1 --- a/src/HOL/Predicate.thy	Sun Mar 03 20:27:42 2019 +0100
    20.2 +++ b/src/HOL/Predicate.thy	Tue Mar 05 07:00:21 2019 +0000
    20.3 @@ -78,11 +78,11 @@
    20.4  
    20.5  lemma eval_INF [simp]:
    20.6    "eval (\<Sqinter>(f ` A)) = \<Sqinter>((eval \<circ> f) ` A)"
    20.7 -  by simp
    20.8 +  by (simp add: image_comp)
    20.9  
   20.10  lemma eval_SUP [simp]:
   20.11    "eval (\<Squnion>(f ` A)) = \<Squnion>((eval \<circ> f) ` A)"
   20.12 -  by simp
   20.13 +  by (simp add: image_comp)
   20.14  
   20.15  instantiation pred :: (type) complete_boolean_algebra
   20.16  begin
   20.17 @@ -400,7 +400,7 @@
   20.18  
   20.19  lemma eval_map [simp]:
   20.20    "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
   20.21 -  by (auto simp add: map_def comp_def)
   20.22 +  by (simp add: map_def comp_def image_comp)
   20.23  
   20.24  functor map: map
   20.25    by (rule ext, rule pred_eqI, auto)+
    21.1 --- a/src/HOL/Probability/Giry_Monad.thy	Sun Mar 03 20:27:42 2019 +0100
    21.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Tue Mar 05 07:00:21 2019 +0000
    21.3 @@ -880,7 +880,7 @@
    21.4    also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
    21.5      using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
    21.6                   (simp_all add: M cong: measurable_cong_sets)
    21.7 -  finally show ?case by (simp add: ac_simps)
    21.8 +  finally show ?case by (simp add: ac_simps image_comp)
    21.9  qed
   21.10  
   21.11  lemma measurable_join1:
    22.1 --- a/src/HOL/Probability/Helly_Selection.thy	Sun Mar 03 20:27:42 2019 +0100
    22.2 +++ b/src/HOL/Probability/Helly_Selection.thy	Tue Mar 05 07:00:21 2019 +0000
    22.3 @@ -88,7 +88,7 @@
    22.4  
    22.5    define F where "F x = Inf {lim (?f n) |n. x < r n}" for x
    22.6    have F_eq: "ereal (F x) = (INF n\<in>{n. x < r n}. ereal (lim (?f n)))" for x
    22.7 -    unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image)
    22.8 +    unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image image_comp)
    22.9    have mono_F: "mono F"
   22.10      using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
   22.11    moreover have "\<And>x. continuous (at_right x) F"
    23.1 --- a/src/HOL/Probability/SPMF.thy	Sun Mar 03 20:27:42 2019 +0100
    23.2 +++ b/src/HOL/Probability/SPMF.thy	Tue Mar 05 07:00:21 2019 +0000
    23.3 @@ -45,7 +45,7 @@
    23.4  
    23.5  lemma ennreal_SUP:
    23.6    "\<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))"
    23.7 -using ennreal_Sup[of "f ` A"] by auto
    23.8 +using ennreal_Sup[of "f ` A"] by (auto simp add: image_comp)
    23.9  
   23.10  lemma ennreal_lt_0: "x < 0 \<Longrightarrow> ennreal x = 0"
   23.11  by(simp add: ennreal_eq_0_iff)
   23.12 @@ -1589,7 +1589,7 @@
   23.13        using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
   23.14      also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf p f) i))"
   23.15        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)
   23.16 -    also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
   23.17 +    also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y image_comp)
   23.18      finally show "spmf ?lhs i = spmf ?rhs i" by simp
   23.19    qed
   23.20  qed simp
   23.21 @@ -1620,14 +1620,14 @@
   23.22        using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
   23.23  
   23.24      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)"
   23.25 -      by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
   23.26 +      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)
   23.27      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))"
   23.28        unfolding nn_integral_measure_spmf' using Y chain''
   23.29        by(rule nn_integral_monotone_convergence_SUP_countable) simp
   23.30      also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
   23.31        by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult)
   23.32      also have "\<dots> = ennreal (spmf ?rhs i)" using chain'''
   23.33 -      by(auto simp add: ennreal_spmf_lub_spmf Y)
   23.34 +      by(auto simp add: ennreal_spmf_lub_spmf Y image_comp)
   23.35      finally show "spmf ?lhs i = spmf ?rhs i" by simp
   23.36    qed
   23.37  qed simp