ereal: tuned proofs concerning continuity and suprema
authorhoelzl
Tue Jan 27 16:12:40 2015 +0100 (2015-01-27)
changeset 594522538b2c51769
parent 59451 86be42bb5174
child 59453 4736ff5a41d8
ereal: tuned proofs concerning continuity and suprema
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Lebesgue_Integral_Substitution.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Regularity.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jan 26 14:40:13 2015 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Jan 27 16:12:40 2015 +0100
     1.3 @@ -102,15 +102,25 @@
     1.4  lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
     1.5    by (rule bdd_belowI[of _ bot]) simp
     1.6  
     1.7 -lemma bdd_above_uminus[simp]:
     1.8 -  fixes X :: "'a::ordered_ab_group_add set"
     1.9 -  shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
    1.10 -  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    1.11 +lemma bdd_above_image_mono: "mono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_above (f`A)"
    1.12 +  by (auto simp: bdd_above_def mono_def)
    1.13 +
    1.14 +lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)"
    1.15 +  by (auto simp: bdd_below_def mono_def)
    1.16 +  
    1.17 +lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)"
    1.18 +  by (auto simp: bdd_above_def bdd_below_def antimono_def)
    1.19  
    1.20 -lemma bdd_below_uminus[simp]:
    1.21 +lemma bdd_below_image_antimono: "antimono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below (f`A)"
    1.22 +  by (auto simp: bdd_above_def bdd_below_def antimono_def)
    1.23 +
    1.24 +lemma
    1.25    fixes X :: "'a::ordered_ab_group_add set"
    1.26 -  shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
    1.27 -  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
    1.28 +  shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
    1.29 +    and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
    1.30 +  using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"]
    1.31 +  using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"]
    1.32 +  by (auto simp: antimono_def image_image)
    1.33  
    1.34  context lattice
    1.35  begin
     2.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Jan 26 14:40:13 2015 +0100
     2.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Jan 27 16:12:40 2015 +0100
     2.3 @@ -568,6 +568,9 @@
     2.4  lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
     2.5    by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
     2.6  
     2.7 +lemma ereal_less_uminus_reorder: "a < - b \<longleftrightarrow> b < - (a::ereal)"
     2.8 +  by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
     2.9 +
    2.10  lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::ereal)"
    2.11    by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)
    2.12  
    2.13 @@ -1605,39 +1608,142 @@
    2.14    show "\<exists>a b::ereal. a \<noteq> b"
    2.15      using zero_neq_one by blast
    2.16  qed
    2.17 +subsubsection "Topological space"
    2.18 +
    2.19 +instantiation ereal :: linear_continuum_topology
    2.20 +begin
    2.21 +
    2.22 +definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
    2.23 +  open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
    2.24 +
    2.25 +instance
    2.26 +  by default (simp add: open_ereal_generated)
    2.27 +
    2.28 +end
    2.29 +
    2.30 +lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
    2.31 +  apply (rule tendsto_compose[where g=ereal])
    2.32 +  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
    2.33 +  apply (rule_tac x="case a of MInfty \<Rightarrow> UNIV | ereal x \<Rightarrow> {x <..} | PInfty \<Rightarrow> {}" in exI)
    2.34 +  apply (auto split: ereal.split) []
    2.35 +  apply (rule_tac x="case a of MInfty \<Rightarrow> {} | ereal x \<Rightarrow> {..< x} | PInfty \<Rightarrow> UNIV" in exI)
    2.36 +  apply (auto split: ereal.split) []
    2.37 +  done
    2.38 +
    2.39 +lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
    2.40 +  apply (rule tendsto_compose[where g=uminus])
    2.41 +  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
    2.42 +  apply (rule_tac x="{..< -a}" in exI)
    2.43 +  apply (auto split: ereal.split simp: ereal_less_uminus_reorder) []
    2.44 +  apply (rule_tac x="{- a <..}" in exI)
    2.45 +  apply (auto split: ereal.split simp: ereal_uminus_reorder) []
    2.46 +  done
    2.47 +
    2.48 +lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
    2.49 +  using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
    2.50 +  by auto
    2.51 +
    2.52 +lemma ereal_divide_less_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a / c < b \<longleftrightarrow> a < b * c"
    2.53 +  by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
    2.54 +
    2.55 +lemma ereal_less_divide_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
    2.56 +  by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
    2.57 +
    2.58 +lemma tendsto_cmult_ereal[tendsto_intros, simp, intro]:
    2.59 +  assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
    2.60 +proof -
    2.61 +  { fix c :: ereal assume "0 < c" "c < \<infinity>"
    2.62 +    then have "((\<lambda>x. c * f x::ereal) ---> c * x) F"
    2.63 +      apply (intro tendsto_compose[OF _ f])
    2.64 +      apply (auto intro!: order_tendstoI simp: eventually_at_topological)
    2.65 +      apply (rule_tac x="{a/c <..}" in exI)
    2.66 +      apply (auto split: ereal.split simp: ereal_divide_less_iff mult.commute) []
    2.67 +      apply (rule_tac x="{..< a/c}" in exI)
    2.68 +      apply (auto split: ereal.split simp: ereal_less_divide_iff mult.commute) []
    2.69 +      done }
    2.70 +  note * = this
    2.71 +
    2.72 +  have "((0 < c \<and> c < \<infinity>) \<or> (-\<infinity> < c \<and> c < 0) \<or> c = 0)"
    2.73 +    using c by (cases c) auto
    2.74 +  then show ?thesis
    2.75 +  proof (elim disjE conjE)
    2.76 +    assume "- \<infinity> < c" "c < 0"
    2.77 +    then have "0 < - c" "- c < \<infinity>"
    2.78 +      by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
    2.79 +    then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
    2.80 +      by (rule *)
    2.81 +    from tendsto_uminus_ereal[OF this] show ?thesis 
    2.82 +      by simp
    2.83 +  qed (auto intro!: *)
    2.84 +qed
    2.85 +
    2.86 +lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]:
    2.87 +  assumes "x \<noteq> 0" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
    2.88 +proof cases
    2.89 +  assume "\<bar>c\<bar> = \<infinity>"
    2.90 +  show ?thesis
    2.91 +  proof (rule filterlim_cong[THEN iffD1, OF refl refl _ tendsto_const])
    2.92 +    have "0 < x \<or> x < 0"
    2.93 +      using `x \<noteq> 0` by (auto simp add: neq_iff)
    2.94 +    then show "eventually (\<lambda>x'. c * x = c * f x') F"
    2.95 +    proof
    2.96 +      assume "0 < x" from order_tendstoD(1)[OF f this] show ?thesis
    2.97 +        by eventually_elim (insert `0<x` `\<bar>c\<bar> = \<infinity>`, auto)
    2.98 +    next
    2.99 +      assume "x < 0" from order_tendstoD(2)[OF f this] show ?thesis
   2.100 +        by eventually_elim (insert `x<0` `\<bar>c\<bar> = \<infinity>`, auto)
   2.101 +    qed
   2.102 +  qed
   2.103 +qed (rule tendsto_cmult_ereal[OF _ f])
   2.104 +
   2.105 +lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]:
   2.106 +  assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
   2.107 +  apply (intro tendsto_compose[OF _ f])
   2.108 +  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
   2.109 +  apply (rule_tac x="{a - y <..}" in exI)
   2.110 +  apply (auto split: ereal.split simp: ereal_minus_less_iff c) []
   2.111 +  apply (rule_tac x="{..< a - y}" in exI)
   2.112 +  apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
   2.113 +  done
   2.114 +
   2.115 +lemma tendsto_add_left_ereal[tendsto_intros, simp, intro]:
   2.116 +  assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
   2.117 +  apply (intro tendsto_compose[OF _ f])
   2.118 +  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
   2.119 +  apply (rule_tac x="{a - y <..}" in exI)
   2.120 +  apply (insert c, auto split: ereal.split simp: ereal_minus_less_iff) []
   2.121 +  apply (rule_tac x="{..< a - y}" in exI)
   2.122 +  apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
   2.123 +  done
   2.124 +
   2.125 +lemma continuous_at_ereal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ereal (f x))"
   2.126 +  unfolding continuous_def by auto
   2.127 +
   2.128 +lemma continuous_on_ereal[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. ereal (f x))"
   2.129 +  unfolding continuous_on_def by auto
   2.130  
   2.131  lemma ereal_Sup:
   2.132    assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
   2.133    shows "ereal (Sup A) = (SUP a:A. ereal a)"
   2.134 -proof (rule antisym)
   2.135 +proof (rule continuous_at_Sup_mono)
   2.136    obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
   2.137      using * by (force simp: bot_ereal_def)
   2.138 -  then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r"
   2.139 -    by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
   2.140 -
   2.141 -  show "ereal (Sup A) \<le> (SUP a:A. ereal a)"
   2.142 -    using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`])
   2.143 -  show "(SUP a:A. ereal a) \<le> ereal (Sup A)"
   2.144 -    using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI)
   2.145 -qed
   2.146 +  then show "bdd_above A" "A \<noteq> {}"
   2.147 +    by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
   2.148 +qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
   2.149  
   2.150  lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
   2.151    using ereal_Sup[of "f`A"] by auto
   2.152 -  
   2.153 +
   2.154  lemma ereal_Inf:
   2.155    assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
   2.156    shows "ereal (Inf A) = (INF a:A. ereal a)"
   2.157 -proof (rule antisym)
   2.158 +proof (rule continuous_at_Inf_mono)
   2.159    obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
   2.160      using * by (force simp: top_ereal_def)
   2.161 -  then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a"
   2.162 -    by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
   2.163 -
   2.164 -  show "(INF a:A. ereal a) \<le> ereal (Inf A)"
   2.165 -    using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`])
   2.166 -  show "ereal (Inf A) \<le> (INF a:A. ereal a)"
   2.167 -    using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI)
   2.168 -qed
   2.169 +  then show "bdd_below A" "A \<noteq> {}"
   2.170 +    by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
   2.171 +qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
   2.172  
   2.173  lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
   2.174    using ereal_Inf[of "f`A"] by auto
   2.175 @@ -1660,9 +1766,15 @@
   2.176  
   2.177  lemma ereal_INF_uminus_eq:
   2.178    fixes f :: "'a \<Rightarrow> ereal"
   2.179 -  shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
   2.180 +  shows "(INF x:S. - f x) = - (SUP x:S. f x)"
   2.181    using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
   2.182  
   2.183 +lemma ereal_SUP_uminus:
   2.184 +  fixes f :: "'a \<Rightarrow> ereal"
   2.185 +  shows "(SUP i : R. - f i) = - (INF i : R. f i)"
   2.186 +  using ereal_Sup_uminus_image_eq[of "f`R"]
   2.187 +  by (simp add: image_image)
   2.188 +
   2.189  lemma ereal_SUP_not_infty:
   2.190    fixes f :: "_ \<Rightarrow> ereal"
   2.191    shows "A \<noteq> {} \<Longrightarrow> l \<noteq> -\<infinity> \<Longrightarrow> u \<noteq> \<infinity> \<Longrightarrow> \<forall>a\<in>A. l \<le> f a \<and> f a \<le> u \<Longrightarrow> \<bar>SUPREMUM A f\<bar> \<noteq> \<infinity>"
   2.192 @@ -1675,17 +1787,6 @@
   2.193    using INF_lower2[of _ A f u] INF_greatest[of A l f]
   2.194    by (cases "INFIMUM A f") auto
   2.195  
   2.196 -lemma ereal_SUP_uminus:
   2.197 -  fixes f :: "'a \<Rightarrow> ereal"
   2.198 -  shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
   2.199 -  using ereal_Sup_uminus_image_eq[of "f`R"]
   2.200 -  by (simp add: image_image)
   2.201 -
   2.202 -lemma ereal_INF_uminus:
   2.203 -  fixes f :: "'a \<Rightarrow> ereal"
   2.204 -  shows "(INF i : R. - f i) = - (SUP i : R. f i)"
   2.205 -  using ereal_SUP_uminus [of _ "\<lambda>x. - f x"] by simp
   2.206 -
   2.207  lemma ereal_image_uminus_shift:
   2.208    fixes X Y :: "ereal set"
   2.209    shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
   2.210 @@ -1697,12 +1798,6 @@
   2.211      by (simp add: image_image)
   2.212  qed (simp add: image_image)
   2.213  
   2.214 -lemma Inf_ereal_iff:
   2.215 -  fixes z :: ereal
   2.216 -  shows "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x < y) \<longleftrightarrow> Inf X < y"
   2.217 -  by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower
   2.218 -      less_le_not_le linear order_less_le_trans)
   2.219 -
   2.220  lemma Sup_eq_MInfty:
   2.221    fixes S :: "ereal set"
   2.222    shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
   2.223 @@ -1742,101 +1837,108 @@
   2.224  qed
   2.225  
   2.226  lemma SUP_PInfty:
   2.227 -  fixes f :: "'a \<Rightarrow> ereal"
   2.228 -  assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
   2.229 -  shows "(SUP i:A. f i) = \<infinity>"
   2.230 -  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
   2.231 -  apply simp
   2.232 -proof safe
   2.233 -  fix x :: ereal
   2.234 -  assume "x \<noteq> \<infinity>"
   2.235 -  show "\<exists>i\<in>A. x < f i"
   2.236 -  proof (cases x)
   2.237 -    case PInf
   2.238 -    with `x \<noteq> \<infinity>` show ?thesis
   2.239 -      by simp
   2.240 -  next
   2.241 -    case MInf
   2.242 -    with assms[of "0"] show ?thesis
   2.243 -      by force
   2.244 -  next
   2.245 -    case (real r)
   2.246 -    with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
   2.247 -      by auto
   2.248 -    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
   2.249 -      using assms ..
   2.250 -    ultimately show ?thesis
   2.251 -      by (auto intro!: bexI[of _ i])
   2.252 -  qed
   2.253 -qed
   2.254 +  "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i:A. f i :: ereal) = \<infinity>"
   2.255 +  unfolding top_ereal_def[symmetric] SUP_eq_top_iff
   2.256 +  by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
   2.257  
   2.258  lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
   2.259    by (rule SUP_PInfty) auto
   2.260  
   2.261 -lemma Inf_less:
   2.262 -  fixes x :: ereal
   2.263 -  assumes "(INF i:A. f i) < x"
   2.264 -  shows "\<exists>i. i \<in> A \<and> f i \<le> x"
   2.265 -proof (rule ccontr)
   2.266 -  assume "\<not> ?thesis"
   2.267 -  then have "\<forall>i\<in>A. f i > x"
   2.268 -    by auto
   2.269 -  then have "(INF i:A. f i) \<ge> x"
   2.270 -    by (subst INF_greatest) auto
   2.271 -  then show False
   2.272 -    using assms by auto
   2.273 +lemma SUP_ereal_add_left:
   2.274 +  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
   2.275 +  shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
   2.276 +proof cases
   2.277 +  assume "(SUP i:I. f i) = - \<infinity>"
   2.278 +  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
   2.279 +    unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto
   2.280 +  ultimately show ?thesis
   2.281 +    by (cases c) (auto simp: `I \<noteq> {}`)
   2.282 +next
   2.283 +  assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
   2.284 +    unfolding Sup_image_eq[symmetric]
   2.285 +    by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
   2.286 +       (auto simp: continuous_at_within continuous_at mono_def ereal_add_mono `I \<noteq> {}` `c \<noteq> -\<infinity>`)
   2.287 +qed
   2.288 +
   2.289 +lemma SUP_ereal_add_right:
   2.290 +  fixes c :: ereal
   2.291 +  shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)"
   2.292 +  using SUP_ereal_add_left[of I c f] by (simp add: add.commute)
   2.293 +
   2.294 +lemma SUP_ereal_minus_right:
   2.295 +  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
   2.296 +  shows "(SUP i:I. c - f i :: ereal) = c - (INF i:I. f i)"
   2.297 +  using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
   2.298 +  by (simp add: ereal_SUP_uminus minus_ereal_def)
   2.299 +
   2.300 +lemma SUP_ereal_minus_left:
   2.301 +  assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
   2.302 +  shows "(SUP i:I. f i - c:: ereal) = (SUP i:I. f i) - c"
   2.303 +  using SUP_ereal_add_left[OF `I \<noteq> {}`, of "-c" f] by (simp add: `c \<noteq> \<infinity>` minus_ereal_def)
   2.304 +
   2.305 +lemma INF_ereal_minus_right:
   2.306 +  assumes "I \<noteq> {}" and "\<bar>c\<bar> \<noteq> \<infinity>"
   2.307 +  shows "(INF i:I. c - f i) = c - (SUP i:I. f i::ereal)"
   2.308 +proof -
   2.309 +  { fix b have "(-c) + b = - (c - b)"
   2.310 +      using `\<bar>c\<bar> \<noteq> \<infinity>` by (cases c b rule: ereal2_cases) auto }
   2.311 +  note * = this
   2.312 +  show ?thesis
   2.313 +    using SUP_ereal_add_right[OF `I \<noteq> {}`, of "-c" f] `\<bar>c\<bar> \<noteq> \<infinity>`
   2.314 +    by (auto simp add: * ereal_SUP_uminus_eq)
   2.315  qed
   2.316  
   2.317  lemma SUP_ereal_le_addI:
   2.318    fixes f :: "'i \<Rightarrow> ereal"
   2.319 -  assumes "\<And>i. f i + y \<le> z"
   2.320 -    and "y \<noteq> -\<infinity>"
   2.321 +  assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
   2.322    shows "SUPREMUM UNIV f + y \<le> z"
   2.323 -proof (cases y)
   2.324 -  case (real r)
   2.325 -  then have "\<And>i. f i \<le> z - y"
   2.326 -    using assms by (simp add: ereal_le_minus_iff)
   2.327 -  then have "SUPREMUM UNIV f \<le> z - y"
   2.328 -    by (rule SUP_least)
   2.329 -  then show ?thesis
   2.330 -    using real by (simp add: ereal_le_minus_iff)
   2.331 -qed (insert assms, auto)
   2.332 +  unfolding SUP_ereal_add_left[OF UNIV_not_empty `y \<noteq> -\<infinity>`, symmetric]
   2.333 +  by (rule SUP_least assms)+
   2.334 +
   2.335 +lemma SUP_combine:
   2.336 +  fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
   2.337 +  assumes mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> f a c \<le> f b d"
   2.338 +  shows "(SUP i:UNIV. SUP j:UNIV. f i j) = (SUP i. f i i)"
   2.339 +proof (rule antisym)
   2.340 +  show "(SUP i j. f i j) \<le> (SUP i. f i i)"
   2.341 +    by (rule SUP_least SUP_upper2[where i="sup i j" for i j] UNIV_I mono sup_ge1 sup_ge2)+
   2.342 +  show "(SUP i. f i i) \<le> (SUP i j. f i j)"
   2.343 +    by (rule SUP_least SUP_upper2 UNIV_I mono order_refl)+
   2.344 +qed
   2.345  
   2.346  lemma SUP_ereal_add:
   2.347    fixes f g :: "nat \<Rightarrow> ereal"
   2.348 -  assumes "incseq f"
   2.349 -    and "incseq g"
   2.350 +  assumes inc: "incseq f" "incseq g"
   2.351      and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
   2.352    shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
   2.353 -proof (rule SUP_eqI)
   2.354 -  fix y
   2.355 -  assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
   2.356 -  have f: "SUPREMUM UNIV f \<noteq> -\<infinity>"
   2.357 -    using pos
   2.358 -    unfolding SUP_def Sup_eq_MInfty
   2.359 -    by (auto dest: image_eqD)
   2.360 -  {
   2.361 -    fix j
   2.362 -    {
   2.363 -      fix i
   2.364 -      have "f i + g j \<le> f i + g (max i j)"
   2.365 -        using `incseq g`[THEN incseqD]
   2.366 -        by (rule add_left_mono) auto
   2.367 -      also have "\<dots> \<le> f (max i j) + g (max i j)"
   2.368 -        using `incseq f`[THEN incseqD]
   2.369 -        by (rule add_right_mono) auto
   2.370 -      also have "\<dots> \<le> y" using * by auto
   2.371 -      finally have "f i + g j \<le> y" .
   2.372 -    }
   2.373 -    then have "SUPREMUM UNIV f + g j \<le> y"
   2.374 -      using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
   2.375 -    then have "g j + SUPREMUM UNIV f \<le> y" by (simp add: ac_simps)
   2.376 -  }
   2.377 -  then have "SUPREMUM UNIV g + SUPREMUM UNIV f \<le> y"
   2.378 -    using f by (rule SUP_ereal_le_addI)
   2.379 -  then show "SUPREMUM UNIV f + SUPREMUM UNIV g \<le> y"
   2.380 -    by (simp add: ac_simps)
   2.381 -qed (auto intro!: add_mono SUP_upper)
   2.382 +  apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
   2.383 +  apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
   2.384 +  apply (subst (2) add.commute)
   2.385 +  apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)])
   2.386 +  apply (subst (2) add.commute)
   2.387 +  apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
   2.388 +  done
   2.389 +
   2.390 +lemma INF_ereal_add:
   2.391 +  fixes f :: "nat \<Rightarrow> ereal"
   2.392 +  assumes "decseq f" "decseq g"
   2.393 +    and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   2.394 +  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
   2.395 +proof -
   2.396 +  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
   2.397 +    using assms unfolding INF_less_iff by auto
   2.398 +  { fix a b :: ereal assume "a \<noteq> \<infinity>" "b \<noteq> \<infinity>"
   2.399 +    then have "- ((- a) + (- b)) = a + b"
   2.400 +      by (cases a b rule: ereal2_cases) auto }
   2.401 +  note * = this
   2.402 +  have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   2.403 +    by (simp add: fin *)
   2.404 +  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
   2.405 +    unfolding ereal_INF_uminus_eq
   2.406 +    using assms INF_less
   2.407 +    by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
   2.408 +  finally show ?thesis .
   2.409 +qed
   2.410  
   2.411  lemma SUP_ereal_add_pos:
   2.412    fixes f g :: "nat \<Rightarrow> ereal"
   2.413 @@ -1863,313 +1965,85 @@
   2.414    then show ?thesis by simp
   2.415  qed
   2.416  
   2.417 -lemma SUP_ereal_cmult:
   2.418 -  fixes f :: "nat \<Rightarrow> ereal"
   2.419 -  assumes "\<And>i. 0 \<le> f i"
   2.420 -    and "0 \<le> c"
   2.421 -  shows "(SUP i. c * f i) = c * SUPREMUM UNIV f"
   2.422 -proof (rule SUP_eqI)
   2.423 -  fix i
   2.424 -  have "f i \<le> SUPREMUM UNIV f"
   2.425 -    by (rule SUP_upper) auto
   2.426 -  then show "c * f i \<le> c * SUPREMUM UNIV f"
   2.427 -    using `0 \<le> c` by (rule ereal_mult_left_mono)
   2.428 -next
   2.429 -  fix y
   2.430 -  assume "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
   2.431 -  then have *: "\<And>i. c * f i \<le> y" by simp
   2.432 -  show "c * SUPREMUM UNIV f \<le> y"
   2.433 -  proof (cases "0 < c \<and> c \<noteq> \<infinity>")
   2.434 -    case True
   2.435 -    with * have "SUPREMUM UNIV f \<le> y / c"
   2.436 -      by (intro SUP_least) (auto simp: ereal_le_divide_pos)
   2.437 -    with True show ?thesis
   2.438 -      by (auto simp: ereal_le_divide_pos)
   2.439 -  next
   2.440 -    case False
   2.441 -    {
   2.442 -      assume "c = \<infinity>"
   2.443 -      have ?thesis
   2.444 -      proof (cases "\<forall>i. f i = 0")
   2.445 -        case True
   2.446 -        then have "range f = {0}"
   2.447 -          by auto
   2.448 -        with True show "c * SUPREMUM UNIV f \<le> y"
   2.449 -          using * by auto
   2.450 -      next
   2.451 -        case False
   2.452 -        then obtain i where "f i \<noteq> 0"
   2.453 -          by auto
   2.454 -        with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis
   2.455 -          by (auto split: split_if_asm)
   2.456 -      qed
   2.457 -    }
   2.458 -    moreover note False
   2.459 -    ultimately show ?thesis
   2.460 -      using * `0 \<le> c` by auto
   2.461 -  qed
   2.462 -qed
   2.463 -
   2.464 -lemma SUP_ereal_mult_right:
   2.465 +lemma SUP_ereal_mult_left:
   2.466    fixes f :: "'a \<Rightarrow> ereal"
   2.467    assumes "I \<noteq> {}"
   2.468 -  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   2.469 -    and "0 \<le> c"
   2.470 +  assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
   2.471    shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
   2.472 -proof (rule SUP_eqI)
   2.473 -  fix i assume "i \<in> I"
   2.474 -  then have "f i \<le> SUPREMUM I f"
   2.475 -    by (rule SUP_upper)
   2.476 -  then show "c * f i \<le> c * SUPREMUM I f"
   2.477 -    using `0 \<le> c` by (rule ereal_mult_left_mono)
   2.478 +proof cases
   2.479 +  assume "(SUP i:I. f i) = 0"
   2.480 +  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
   2.481 +    by (metis SUP_upper f antisym)
   2.482 +  ultimately show ?thesis
   2.483 +    by simp
   2.484  next
   2.485 -  fix y assume *: "\<And>i. i \<in> I \<Longrightarrow> c * f i \<le> y"
   2.486 -  { assume "c = \<infinity>" have "c * SUPREMUM I f \<le> y"
   2.487 -    proof cases
   2.488 -      assume "\<forall>i\<in>I. f i = 0"
   2.489 -      then show ?thesis
   2.490 -        using * `c = \<infinity>` by (auto simp: SUP_constant bot_ereal_def)
   2.491 -    next
   2.492 -      assume "\<not> (\<forall>i\<in>I. f i = 0)"
   2.493 -      then obtain i where "f i \<noteq> 0" "i \<in> I"
   2.494 -        by auto
   2.495 -      with *[of i] `c = \<infinity>` `i \<in> I \<Longrightarrow> 0 \<le> f i` show ?thesis
   2.496 -        by (auto split: split_if_asm)
   2.497 -    qed }
   2.498 -  moreover
   2.499 -  { assume "c \<noteq> 0" "c \<noteq> \<infinity>"
   2.500 -    moreover with `0 \<le> c` * have "SUPREMUM I f \<le> y / c"
   2.501 -      by (intro SUP_least) (auto simp: ereal_le_divide_pos)
   2.502 -    ultimately have "c * SUPREMUM I f \<le> y"
   2.503 -      using `0 \<le> c` * by (auto simp: ereal_le_divide_pos) }
   2.504 -  moreover { assume "c = 0" with * `I \<noteq> {}` have "c * SUPREMUM I f \<le> y" by auto }
   2.505 -  ultimately show "c * SUPREMUM I f \<le> y"
   2.506 -    by blast
   2.507 +  assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
   2.508 +    unfolding SUP_def
   2.509 +    by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
   2.510 +       (auto simp: mono_def continuous_at continuous_at_within `I \<noteq> {}`
   2.511 +             intro!: ereal_mult_left_mono c)
   2.512  qed
   2.513  
   2.514 -lemma SUP_ereal_add_left:
   2.515 -  fixes f :: "'a \<Rightarrow> ereal"
   2.516 -  assumes "I \<noteq> {}"
   2.517 -  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
   2.518 -    and "0 \<le> c"
   2.519 -  shows "(SUP i:I. f i + c) = SUPREMUM I f + c"
   2.520 -proof (intro SUP_eqI)
   2.521 -  fix B assume *: "\<And>i. i \<in> I \<Longrightarrow> f i + c \<le> B"
   2.522 -  show "SUPREMUM I f + c \<le> B"
   2.523 -  proof cases
   2.524 -    assume "c = \<infinity>" with `I \<noteq> {}` * show ?thesis
   2.525 -      by auto
   2.526 -  next
   2.527 -    assume "c \<noteq> \<infinity>"
   2.528 -    with `0 \<le> c` have [simp]: "\<bar>c\<bar> \<noteq> \<infinity>"
   2.529 -      by simp
   2.530 -    have "SUPREMUM I f \<le> B - c"
   2.531 -      by (simp add: SUP_le_iff ereal_le_minus *)
   2.532 -    then show ?thesis
   2.533 -      by (simp add: ereal_le_minus)
   2.534 -  qed
   2.535 -qed (auto intro: ereal_add_mono SUP_upper)
   2.536 -
   2.537 -lemma SUP_ereal_add_right:
   2.538 -  fixes c :: ereal
   2.539 -  shows "I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i) \<Longrightarrow> 0 \<le> c \<Longrightarrow> (SUP i:I. c + f i) = c + SUPREMUM I f"
   2.540 -  using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
   2.541 +lemma countable_approach: 
   2.542 +  fixes x :: ereal
   2.543 +  assumes "x \<noteq> -\<infinity>"
   2.544 +  shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
   2.545 +proof (cases x)
   2.546 +  case (real r)
   2.547 +  moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0"
   2.548 +    by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
   2.549 +  ultimately show ?thesis
   2.550 +    by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
   2.551 +next 
   2.552 +  case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis
   2.553 +    by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty)
   2.554 +qed (simp add: assms)
   2.555  
   2.556  lemma Sup_countable_SUP:
   2.557    assumes "A \<noteq> {}"
   2.558 -  shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
   2.559 -proof (cases "Sup A")
   2.560 -  case (real r)
   2.561 -  have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
   2.562 -  proof
   2.563 -    fix n :: nat
   2.564 -    have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
   2.565 -      using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
   2.566 -    then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
   2.567 -    then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
   2.568 -      by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
   2.569 -  qed
   2.570 -  from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
   2.571 -    where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
   2.572 -  have "SUPREMUM UNIV f = Sup A"
   2.573 -  proof (rule SUP_eqI)
   2.574 -    fix i
   2.575 -    show "f i \<le> Sup A"
   2.576 -      using f by (auto intro!: complete_lattice_class.Sup_upper)
   2.577 -  next
   2.578 -    fix y
   2.579 -    assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
   2.580 -    show "Sup A \<le> y"
   2.581 -    proof (rule ereal_le_epsilon, intro allI impI)
   2.582 -      fix e :: ereal
   2.583 -      assume "0 < e"
   2.584 -      show "Sup A \<le> y + e"
   2.585 -      proof (cases e)
   2.586 -        case (real r)
   2.587 -        then have "0 < r"
   2.588 -          using `0 < e` by auto
   2.589 -        then obtain n :: nat where *: "1 / real n < r" "0 < n"
   2.590 -          using ex_inverse_of_nat_less
   2.591 -          by (auto simp: real_eq_of_nat inverse_eq_divide)
   2.592 -        have "Sup A \<le> f n + 1 / ereal (real n)"
   2.593 -          using f[THEN spec, of n]
   2.594 -          by auto
   2.595 -        also have "1 / ereal (real n) \<le> e"
   2.596 -          using real *
   2.597 -          by (auto simp: one_ereal_def )
   2.598 -        with bound have "f n + 1 / ereal (real n) \<le> y + e"
   2.599 -          by (rule add_mono) simp
   2.600 -        finally show "Sup A \<le> y + e" .
   2.601 -      qed (insert `0 < e`, auto)
   2.602 -    qed
   2.603 -  qed
   2.604 -  with f show ?thesis
   2.605 -    by (auto intro!: exI[of _ f])
   2.606 -next
   2.607 -  case PInf
   2.608 -  from `A \<noteq> {}` obtain x where "x \<in> A"
   2.609 -    by auto
   2.610 -  show ?thesis
   2.611 -  proof (cases "\<infinity> \<in> A")
   2.612 -    case True
   2.613 -    then have "\<infinity> \<le> Sup A"
   2.614 -      by (intro complete_lattice_class.Sup_upper)
   2.615 -    with True show ?thesis
   2.616 -      by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
   2.617 -  next
   2.618 -    case False
   2.619 -    have "\<exists>x\<in>A. 0 \<le> x"
   2.620 -      by (metis Infty_neq_0(2) PInf complete_lattice_class.Sup_least ereal_infty_less_eq2(1) linorder_linear)
   2.621 -    then obtain x where "x \<in> A" and "0 \<le> x"
   2.622 -      by auto
   2.623 -    have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
   2.624 -    proof (rule ccontr)
   2.625 -      assume "\<not> ?thesis"
   2.626 -      then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
   2.627 -        by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
   2.628 -      then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
   2.629 -        by (cases x) auto
   2.630 -    qed
   2.631 -    from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
   2.632 -      where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
   2.633 -    have "SUPREMUM UNIV f = \<infinity>"
   2.634 -    proof (rule SUP_PInfty)
   2.635 -      fix n :: nat
   2.636 -      show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
   2.637 -        using f[THEN spec, of n] `0 \<le> x`
   2.638 -        by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
   2.639 -    qed
   2.640 -    then show ?thesis
   2.641 -      using f PInf by (auto intro!: exI[of _ f])
   2.642 -  qed
   2.643 -next
   2.644 -  case MInf
   2.645 +  shows "\<exists>f::nat \<Rightarrow> ereal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
   2.646 +proof cases
   2.647 +  assume "Sup A = -\<infinity>"
   2.648    with `A \<noteq> {}` have "A = {-\<infinity>}"
   2.649      by (auto simp: Sup_eq_MInfty)
   2.650    then show ?thesis
   2.651 -    using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
   2.652 +    by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
   2.653 +next
   2.654 +  assume "Sup A \<noteq> -\<infinity>"
   2.655 +  then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l ----> Sup A"
   2.656 +    by (auto dest: countable_approach)
   2.657 +
   2.658 +  have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
   2.659 +  proof (rule dependent_nat_choice)
   2.660 +    show "\<exists>x. x \<in> A \<and> l 0 \<le> x"
   2.661 +      using l[of 0] by (auto simp: less_Sup_iff)
   2.662 +  next
   2.663 +    fix x n assume "x \<in> A \<and> l n \<le> x"
   2.664 +    moreover from l[of "Suc n"] obtain y where "y \<in> A" "l (Suc n) < y"
   2.665 +      by (auto simp: less_Sup_iff)
   2.666 +    ultimately show "\<exists>y. (y \<in> A \<and> l (Suc n) \<le> y) \<and> x \<le> y"
   2.667 +      by (auto intro!: exI[of _ "max x y"] split: split_max)
   2.668 +  qed
   2.669 +  then guess f .. note f = this
   2.670 +  then have "range f \<subseteq> A" "incseq f"
   2.671 +    by (auto simp: incseq_Suc_iff)
   2.672 +  moreover
   2.673 +  have "(SUP i. f i) = Sup A"
   2.674 +  proof (rule tendsto_unique)
   2.675 +    show "f ----> (SUP i. f i)"
   2.676 +      by (rule LIMSEQ_SUP `incseq f`)+
   2.677 +    show "f ----> Sup A"
   2.678 +      using l f
   2.679 +      by (intro tendsto_sandwich[OF _ _ l_Sup tendsto_const])
   2.680 +         (auto simp: Sup_upper)
   2.681 +  qed simp
   2.682 +  ultimately show ?thesis
   2.683 +    by auto
   2.684  qed
   2.685  
   2.686  lemma SUP_countable_SUP:
   2.687    "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
   2.688 -  using Sup_countable_SUP [of "g`A"]
   2.689 -  by auto
   2.690 -
   2.691 -lemma Sup_ereal_cadd:
   2.692 -  fixes A :: "ereal set"
   2.693 -  assumes "A \<noteq> {}"
   2.694 -    and "a \<noteq> -\<infinity>"
   2.695 -  shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
   2.696 -proof (rule antisym)
   2.697 -  have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
   2.698 -    by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
   2.699 -  then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
   2.700 -  show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
   2.701 -  proof (cases a)
   2.702 -    case PInf with `A \<noteq> {}`
   2.703 -    show ?thesis
   2.704 -      by (auto simp: image_constant max.absorb1)
   2.705 -  next
   2.706 -    case (real r)
   2.707 -    then have **: "op + (- a) ` op + a ` A = A"
   2.708 -      by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
   2.709 -    from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis
   2.710 -      unfolding **
   2.711 -      by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
   2.712 -  qed (insert `a \<noteq> -\<infinity>`, auto)
   2.713 -qed
   2.714 -
   2.715 -lemma Sup_ereal_cminus:
   2.716 -  fixes A :: "ereal set"
   2.717 -  assumes "A \<noteq> {}"
   2.718 -    and "a \<noteq> -\<infinity>"
   2.719 -  shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
   2.720 -  using Sup_ereal_cadd [of "uminus ` A" a] assms
   2.721 -  unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
   2.722 -
   2.723 -lemma SUP_ereal_cminus:
   2.724 -  fixes f :: "'i \<Rightarrow> ereal"
   2.725 -  fixes A
   2.726 -  assumes "A \<noteq> {}"
   2.727 -    and "a \<noteq> -\<infinity>"
   2.728 -  shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
   2.729 -  using Sup_ereal_cminus[of "f`A" a] assms
   2.730 -  unfolding SUP_def INF_def image_image by auto
   2.731 -
   2.732 -lemma Inf_ereal_cminus:
   2.733 -  fixes A :: "ereal set"
   2.734 -  assumes "A \<noteq> {}"
   2.735 -    and "\<bar>a\<bar> \<noteq> \<infinity>"
   2.736 -  shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
   2.737 -proof -
   2.738 -  {
   2.739 -    fix x
   2.740 -    have "-a - -x = -(a - x)"
   2.741 -      using assms by (cases x) auto
   2.742 -  } note * = this
   2.743 -  then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
   2.744 -    by (auto simp: image_image)
   2.745 -  with * show ?thesis
   2.746 -    using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
   2.747 -    by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
   2.748 -qed
   2.749 -
   2.750 -lemma INF_ereal_cminus:
   2.751 -  fixes a :: ereal
   2.752 -  assumes "A \<noteq> {}"
   2.753 -    and "\<bar>a\<bar> \<noteq> \<infinity>"
   2.754 -  shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
   2.755 -  using Inf_ereal_cminus[of "f`A" a] assms
   2.756 -  unfolding SUP_def INF_def image_image
   2.757 -  by auto
   2.758 -
   2.759 -lemma uminus_ereal_add_uminus_uminus:
   2.760 -  fixes a b :: ereal
   2.761 -  shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
   2.762 -  by (cases rule: ereal2_cases[of a b]) auto
   2.763 -
   2.764 -lemma INF_ereal_add:
   2.765 -  fixes f :: "nat \<Rightarrow> ereal"
   2.766 -  assumes "decseq f" "decseq g"
   2.767 -    and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   2.768 -  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
   2.769 -proof -
   2.770 -  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
   2.771 -    using assms unfolding INF_less_iff by auto
   2.772 -  {
   2.773 -    fix i
   2.774 -    from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
   2.775 -      by (rule uminus_ereal_add_uminus_uminus)
   2.776 -  }
   2.777 -  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   2.778 -    by simp
   2.779 -  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
   2.780 -    unfolding ereal_INF_uminus
   2.781 -    using assms INF_less
   2.782 -    by (subst SUP_ereal_add)
   2.783 -       (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
   2.784 -  finally show ?thesis .
   2.785 -qed
   2.786 +  using Sup_countable_SUP [of "g`A"] by auto
   2.787  
   2.788  subsection "Relation to @{typ enat}"
   2.789  
   2.790 @@ -2225,19 +2099,6 @@
   2.791  
   2.792  subsection "Limits on @{typ ereal}"
   2.793  
   2.794 -subsubsection "Topological space"
   2.795 -
   2.796 -instantiation ereal :: linear_continuum_topology
   2.797 -begin
   2.798 -
   2.799 -definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
   2.800 -  open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
   2.801 -
   2.802 -instance
   2.803 -  by default (simp add: open_ereal_generated)
   2.804 -
   2.805 -end
   2.806 -
   2.807  lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
   2.808    unfolding open_ereal_generated
   2.809  proof (induct rule: generate_topology.induct)
   2.810 @@ -2279,23 +2140,7 @@
   2.811  qed (fastforce simp add: vimage_Union)+
   2.812  
   2.813  lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
   2.814 -  unfolding open_ereal_generated
   2.815 -proof (induct rule: generate_topology.induct)
   2.816 -  case (Int A B)
   2.817 -  then show ?case
   2.818 -    by auto
   2.819 -next
   2.820 -  case (Basis S)
   2.821 -  {
   2.822 -    fix x have
   2.823 -      "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
   2.824 -      "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
   2.825 -      by (induct x) auto
   2.826 -  }
   2.827 -  moreover note Basis
   2.828 -  ultimately show ?case
   2.829 -    by (auto split: ereal.split)
   2.830 -qed (fastforce simp add: vimage_Union)+
   2.831 +  by (intro open_vimage continuous_intros)
   2.832  
   2.833  lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
   2.834    unfolding open_generated_order[where 'a=real]
   2.835 @@ -2422,23 +2267,6 @@
   2.836  
   2.837  subsubsection {* Convergent sequences *}
   2.838  
   2.839 -lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
   2.840 -  (is "?l = ?r")
   2.841 -proof (intro iffI topological_tendstoI)
   2.842 -  fix S
   2.843 -  assume "?l" and "open S" and "x \<in> S"
   2.844 -  then show "eventually (\<lambda>x. f x \<in> S) net"
   2.845 -    using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
   2.846 -    by (simp add: inj_image_mem_iff)
   2.847 -next
   2.848 -  fix S
   2.849 -  assume "?r" and "open S" and "ereal x \<in> S"
   2.850 -  show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
   2.851 -    using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
   2.852 -    using `ereal x \<in> S`
   2.853 -    by auto
   2.854 -qed
   2.855 -
   2.856  lemma lim_real_of_ereal[simp]:
   2.857    assumes lim: "(f ---> ereal x) net"
   2.858    shows "((\<lambda>x. real (f x)) ---> x) net"
   2.859 @@ -2454,6 +2282,9 @@
   2.860      by (rule eventually_mono)
   2.861  qed
   2.862  
   2.863 +lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
   2.864 +  by (auto dest!: lim_real_of_ereal)
   2.865 +
   2.866  lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
   2.867  proof -
   2.868    {
   2.869 @@ -2763,7 +2594,7 @@
   2.870  lemma ereal_Limsup_uminus:
   2.871    fixes f :: "'a \<Rightarrow> ereal"
   2.872    shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
   2.873 -  unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
   2.874 +  unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus_eq ..
   2.875  
   2.876  lemma liminf_bounded_iff:
   2.877    fixes x :: "nat \<Rightarrow> ereal"
     3.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Jan 26 14:40:13 2015 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Jan 27 16:12:40 2015 +0100
     3.3 @@ -250,71 +250,22 @@
     3.4      and t: "\<bar>t\<bar> \<noteq> \<infinity>"
     3.5    shows "open ((\<lambda>x. m * x + t) ` S)"
     3.6  proof -
     3.7 -  obtain r where r[simp]: "m = ereal r"
     3.8 -    using m by (cases m) auto
     3.9 -  obtain p where p[simp]: "t = ereal p"
    3.10 -    using t by auto
    3.11 -  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
    3.12 -    using m by auto
    3.13 -  from `open S` [THEN ereal_openE]
    3.14 -  obtain l u where T:
    3.15 -      "open (ereal -` S)"
    3.16 -      "\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S"
    3.17 -      "- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S"
    3.18 -    by blast
    3.19 -  let ?f = "(\<lambda>x. m * x + t)"
    3.20 -  show ?thesis
    3.21 -    unfolding open_ereal_def
    3.22 -  proof (intro conjI impI exI subsetI)
    3.23 -    have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
    3.24 -    proof safe
    3.25 -      fix x y
    3.26 -      assume "ereal y = m * x + t" "x \<in> S"
    3.27 -      then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
    3.28 -        using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
    3.29 -    qed force
    3.30 -    then show "open (ereal -` ?f ` S)"
    3.31 -      using open_affinity[OF T(1) `r \<noteq> 0`]
    3.32 -      by (auto simp: ac_simps)
    3.33 -  next
    3.34 -    assume "\<infinity> \<in> ?f`S"
    3.35 -    with `0 < r` have "\<infinity> \<in> S"
    3.36 -      by auto
    3.37 -    fix x
    3.38 -    assume "x \<in> {ereal (r * l + p)<..}"
    3.39 -    then have [simp]: "ereal (r * l + p) < x"
    3.40 -      by auto
    3.41 -    show "x \<in> ?f`S"
    3.42 -    proof (rule image_eqI)
    3.43 -      show "x = m * ((x - t) / m) + t"
    3.44 -        using m t
    3.45 -        by (cases rule: ereal3_cases[of m x t]) auto
    3.46 -      have "ereal l < (x - t) / m"
    3.47 -        using m t
    3.48 -        by (simp add: ereal_less_divide_pos ereal_less_minus)
    3.49 -      then show "(x - t) / m \<in> S"
    3.50 -        using T(2)[OF `\<infinity> \<in> S`] by auto
    3.51 -    qed
    3.52 -  next
    3.53 -    assume "-\<infinity> \<in> ?f ` S"
    3.54 -    with `0 < r` have "-\<infinity> \<in> S"
    3.55 -      by auto
    3.56 -    fix x assume "x \<in> {..<ereal (r * u + p)}"
    3.57 -    then have [simp]: "x < ereal (r * u + p)"
    3.58 -      by auto
    3.59 -    show "x \<in> ?f`S"
    3.60 -    proof (rule image_eqI)
    3.61 -      show "x = m * ((x - t) / m) + t"
    3.62 -        using m t
    3.63 -        by (cases rule: ereal3_cases[of m x t]) auto
    3.64 -      have "(x - t)/m < ereal u"
    3.65 -        using m t
    3.66 -        by (simp add: ereal_divide_less_pos ereal_minus_less)
    3.67 -      then show "(x - t)/m \<in> S"
    3.68 -        using T(3)[OF `-\<infinity> \<in> S`]
    3.69 -        by auto
    3.70 -    qed
    3.71 -  qed
    3.72 +  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
    3.73 +    using m t
    3.74 +    apply (intro open_vimage `open S`)
    3.75 +    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
    3.76 +                 tendsto_ident_at tendsto_add_left_ereal)
    3.77 +    apply auto
    3.78 +    done
    3.79 +  also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
    3.80 +    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
    3.81 +                       simp del: uminus_ereal.simps)
    3.82 +  also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
    3.83 +    using m t
    3.84 +    by (simp add: set_eq_iff image_iff)
    3.85 +       (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
    3.86 +              ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
    3.87 +  finally show ?thesis .
    3.88  qed
    3.89  
    3.90  lemma ereal_open_affinity:
    3.91 @@ -340,45 +291,6 @@
    3.92      unfolding image_image by simp
    3.93  qed
    3.94  
    3.95 -lemma ereal_lim_mult:
    3.96 -  fixes X :: "'a \<Rightarrow> ereal"
    3.97 -  assumes lim: "(X ---> L) net"
    3.98 -    and a: "\<bar>a\<bar> \<noteq> \<infinity>"
    3.99 -  shows "((\<lambda>i. a * X i) ---> a * L) net"
   3.100 -proof cases
   3.101 -  assume "a \<noteq> 0"
   3.102 -  show ?thesis
   3.103 -  proof (rule topological_tendstoI)
   3.104 -    fix S
   3.105 -    assume "open S" and "a * L \<in> S"
   3.106 -    have "a * L / a = L"
   3.107 -      using `a \<noteq> 0` a
   3.108 -      by (cases rule: ereal2_cases[of a L]) auto
   3.109 -    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
   3.110 -      using `a * L \<in> S`
   3.111 -      by (force simp: image_iff)
   3.112 -    moreover have "open ((\<lambda>x. x / a) ` S)"
   3.113 -      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
   3.114 -      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
   3.115 -    note * = lim[THEN topological_tendstoD, OF this L]
   3.116 -    {
   3.117 -      fix x
   3.118 -      from a `a \<noteq> 0` have "a * (x / a) = x"
   3.119 -        by (cases rule: ereal2_cases[of a x]) auto
   3.120 -    }
   3.121 -    note this[simp]
   3.122 -    show "eventually (\<lambda>x. a * X x \<in> S) net"
   3.123 -      by (rule eventually_mono[OF _ *]) auto
   3.124 -  qed
   3.125 -qed auto
   3.126 -
   3.127 -lemma ereal_lim_uminus:
   3.128 -  fixes X :: "'a \<Rightarrow> ereal"
   3.129 -  shows "((\<lambda>i. - X i) ---> - L) net \<longleftrightarrow> (X ---> L) net"
   3.130 -  using ereal_lim_mult[of X L net "ereal (-1)"]
   3.131 -    ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
   3.132 -  by (auto simp add: algebra_simps)
   3.133 -
   3.134  lemma ereal_open_atLeast:
   3.135    fixes x :: ereal
   3.136    shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
   3.137 @@ -409,14 +321,6 @@
   3.138    shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
   3.139    using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
   3.140  
   3.141 -lemma ereal_Lim_uminus:
   3.142 -  fixes f :: "'a \<Rightarrow> ereal"
   3.143 -  shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
   3.144 -  using
   3.145 -    ereal_lim_mult[of f f0 net "- 1"]
   3.146 -    ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
   3.147 -  by (auto simp: ereal_uminus_reorder)
   3.148 -
   3.149  lemma Liminf_PInfty:
   3.150    fixes f :: "'a \<Rightarrow> ereal"
   3.151    assumes "\<not> trivial_limit net"
   3.152 @@ -559,9 +463,9 @@
   3.153    case (real r)
   3.154    then show ?thesis
   3.155      unfolding liminf_SUP_INF limsup_INF_SUP
   3.156 -    apply (subst INF_ereal_cminus)
   3.157 +    apply (subst INF_ereal_minus_right)
   3.158      apply auto
   3.159 -    apply (subst SUP_ereal_cminus)
   3.160 +    apply (subst SUP_ereal_minus_right)
   3.161      apply auto
   3.162      done
   3.163  qed (insert `c \<noteq> -\<infinity>`, simp)
   3.164 @@ -889,7 +793,7 @@
   3.165    shows "(\<Sum>i. a * f i) = a * suminf f"
   3.166    by (auto simp: setsum_ereal_right_distrib[symmetric] assms
   3.167         ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
   3.168 -       intro!: SUP_ereal_cmult)
   3.169 +       intro!: SUP_ereal_mult_left)
   3.170  
   3.171  lemma suminf_PInfty:
   3.172    fixes f :: "nat \<Rightarrow> ereal"
     4.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Mon Jan 26 14:40:13 2015 +0100
     4.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Jan 27 16:12:40 2015 +0100
     4.3 @@ -641,7 +641,7 @@
     4.4        finally show "?f i \<le> ?g i" .
     4.5      qed
     4.6      show "?g ----> 0"
     4.7 -      using ereal_lim_mult[OF f_s, of "ereal K"] by simp
     4.8 +      using tendsto_cmult_ereal[OF _ f_s, of "ereal K"] by simp
     4.9    qed
    4.10  
    4.11    assume "(\<lambda>i. simple_bochner_integral M (s i)) ----> x"
     5.1 --- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Mon Jan 26 14:40:13 2015 +0100
     5.2 +++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Tue Jan 27 16:12:40 2015 +0100
     5.3 @@ -566,7 +566,7 @@
     5.4           (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
     5.5                 intro!: ereal_mult_right_mono)
     5.6      also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
     5.7 -      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
     5.8 +      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_mult_left)
     5.9           (auto split: split_indicator simp: derivg_nonneg mult_ac)
    5.10      finally show ?case by simp
    5.11    qed
     6.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Jan 26 14:40:13 2015 +0100
     6.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Jan 27 16:12:40 2015 +0100
     6.3 @@ -944,11 +944,11 @@
     6.4    next
     6.5      show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
     6.6        using measure_conv u_range B_u unfolding simple_integral_def
     6.7 -      by (auto intro!: setsum.cong SUP_ereal_cmult [symmetric])
     6.8 +      by (auto intro!: setsum.cong SUP_ereal_mult_left [symmetric])
     6.9    qed
    6.10    moreover
    6.11    have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
    6.12 -    apply (subst SUP_ereal_cmult [symmetric])
    6.13 +    apply (subst SUP_ereal_mult_left [symmetric])
    6.14    proof (safe intro!: SUP_mono bexI)
    6.15      fix i
    6.16      have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
    6.17 @@ -1115,7 +1115,7 @@
    6.18            by auto }
    6.19        then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
    6.20          using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
    6.21 -        by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
    6.22 +        by (subst SUP_ereal_mult_left [symmetric, OF _ u(6) `0 \<le> a`])
    6.23             (auto intro!: SUP_ereal_add
    6.24                   simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) }
    6.25      then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
    6.26 @@ -1127,8 +1127,10 @@
    6.27    finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
    6.28      unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
    6.29      unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
    6.30 -    apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
    6.31 -    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
    6.32 +    apply (subst SUP_ereal_mult_left [symmetric, OF _ pos(1) `0 \<le> a`])
    6.33 +    apply simp
    6.34 +    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf])
    6.35 +    .
    6.36    then show ?thesis by (simp add: nn_integral_max_0)
    6.37  qed
    6.38  
    6.39 @@ -2120,7 +2122,7 @@
    6.40  next
    6.41    case (seq U)
    6.42    from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
    6.43 -    by eventually_elim (simp add: SUP_ereal_cmult seq)
    6.44 +    by eventually_elim (simp add: SUP_ereal_mult_left seq)
    6.45    from seq f show ?case
    6.46      apply (simp add: nn_integral_monotone_convergence_SUP)
    6.47      apply (subst nn_integral_cong_AE[OF eq])
     7.1 --- a/src/HOL/Probability/Regularity.thy	Mon Jan 26 14:40:13 2015 +0100
     7.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Jan 27 16:12:40 2015 +0100
     7.3 @@ -312,7 +312,7 @@
     7.4      case 2
     7.5      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
     7.6      also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
     7.7 -      unfolding inner by (subst INF_ereal_cminus) force+
     7.8 +      unfolding inner by (subst INF_ereal_minus_right) force+
     7.9      also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
    7.10        by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
    7.11      also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
    7.12 @@ -331,7 +331,7 @@
    7.13      case 1
    7.14      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    7.15      also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
    7.16 -      unfolding outer by (subst SUP_ereal_cminus) auto
    7.17 +      unfolding outer by (subst SUP_ereal_minus_right) auto
    7.18      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
    7.19        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
    7.20      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
     8.1 --- a/src/HOL/Topological_Spaces.thy	Mon Jan 26 14:40:13 2015 +0100
     8.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Jan 27 16:12:40 2015 +0100
     8.3 @@ -2789,6 +2789,154 @@
     8.4      using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
     8.5  qed
     8.6  
     8.7 +lemma continuous_at_Sup_mono:
     8.8 +  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
     8.9 +  assumes "mono f"
    8.10 +  assumes cont: "continuous (at_left (Sup S)) f"
    8.11 +  assumes S: "S \<noteq> {}" "bdd_above S"
    8.12 +  shows "f (Sup S) = (SUP s:S. f s)"
    8.13 +proof (rule antisym)
    8.14 +  have f: "(f ---> f (Sup S)) (at_left (Sup S))"
    8.15 +    using cont unfolding continuous_within .
    8.16 +
    8.17 +  show "f (Sup S) \<le> (SUP s:S. f s)"
    8.18 +  proof cases
    8.19 +    assume "Sup S \<in> S" then show ?thesis
    8.20 +      by (rule cSUP_upper) (auto intro: bdd_above_image_mono S `mono f`)
    8.21 +  next
    8.22 +    assume "Sup S \<notin> S"
    8.23 +    from `S \<noteq> {}` obtain s where "s \<in> S"
    8.24 +      by auto
    8.25 +    with `Sup S \<notin> S` S have "s < Sup S"
    8.26 +      unfolding less_le by (blast intro: cSup_upper)
    8.27 +    show ?thesis
    8.28 +    proof (rule ccontr)
    8.29 +      assume "\<not> ?thesis"
    8.30 +      with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "b < Sup S"
    8.31 +        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s:S. f s) < f y"
    8.32 +        by (auto simp: not_le eventually_at_left[OF `s < Sup S`])
    8.33 +      with `S \<noteq> {}` obtain c where "c \<in> S" "b < c"
    8.34 +        using less_cSupD[of S b] by auto
    8.35 +      with `Sup S \<notin> S` S have "c < Sup S"
    8.36 +        unfolding less_le by (blast intro: cSup_upper)
    8.37 +      from *[OF `b < c` `c < Sup S`] cSUP_upper[OF `c \<in> S` bdd_above_image_mono[of f]]
    8.38 +      show False
    8.39 +        by (auto simp: assms)
    8.40 +    qed
    8.41 +  qed
    8.42 +qed (intro cSUP_least `mono f`[THEN monoD] cSup_upper S)
    8.43 +
    8.44 +lemma continuous_at_Sup_antimono:
    8.45 +  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
    8.46 +  assumes "antimono f"
    8.47 +  assumes cont: "continuous (at_left (Sup S)) f"
    8.48 +  assumes S: "S \<noteq> {}" "bdd_above S"
    8.49 +  shows "f (Sup S) = (INF s:S. f s)"
    8.50 +proof (rule antisym)
    8.51 +  have f: "(f ---> f (Sup S)) (at_left (Sup S))"
    8.52 +    using cont unfolding continuous_within .
    8.53 +
    8.54 +  show "(INF s:S. f s) \<le> f (Sup S)"
    8.55 +  proof cases
    8.56 +    assume "Sup S \<in> S" then show ?thesis
    8.57 +      by (intro cINF_lower) (auto intro: bdd_below_image_antimono S `antimono f`)
    8.58 +  next
    8.59 +    assume "Sup S \<notin> S"
    8.60 +    from `S \<noteq> {}` obtain s where "s \<in> S"
    8.61 +      by auto
    8.62 +    with `Sup S \<notin> S` S have "s < Sup S"
    8.63 +      unfolding less_le by (blast intro: cSup_upper)
    8.64 +    show ?thesis
    8.65 +    proof (rule ccontr)
    8.66 +      assume "\<not> ?thesis"
    8.67 +      with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "b < Sup S"
    8.68 +        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s:S. f s)"
    8.69 +        by (auto simp: not_le eventually_at_left[OF `s < Sup S`])
    8.70 +      with `S \<noteq> {}` obtain c where "c \<in> S" "b < c"
    8.71 +        using less_cSupD[of S b] by auto
    8.72 +      with `Sup S \<notin> S` S have "c < Sup S"
    8.73 +        unfolding less_le by (blast intro: cSup_upper)
    8.74 +      from *[OF `b < c` `c < Sup S`] cINF_lower[OF bdd_below_image_antimono, of f S c] `c \<in> S`
    8.75 +      show False
    8.76 +        by (auto simp: assms)
    8.77 +    qed
    8.78 +  qed
    8.79 +qed (intro cINF_greatest `antimono f`[THEN antimonoD] cSup_upper S)
    8.80 +
    8.81 +lemma continuous_at_Inf_mono:
    8.82 +  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
    8.83 +  assumes "mono f"
    8.84 +  assumes cont: "continuous (at_right (Inf S)) f"
    8.85 +  assumes S: "S \<noteq> {}" "bdd_below S"
    8.86 +  shows "f (Inf S) = (INF s:S. f s)"
    8.87 +proof (rule antisym)
    8.88 +  have f: "(f ---> f (Inf S)) (at_right (Inf S))"
    8.89 +    using cont unfolding continuous_within .
    8.90 +
    8.91 +  show "(INF s:S. f s) \<le> f (Inf S)"
    8.92 +  proof cases
    8.93 +    assume "Inf S \<in> S" then show ?thesis
    8.94 +      by (rule cINF_lower[rotated]) (auto intro: bdd_below_image_mono S `mono f`)
    8.95 +  next
    8.96 +    assume "Inf S \<notin> S"
    8.97 +    from `S \<noteq> {}` obtain s where "s \<in> S"
    8.98 +      by auto
    8.99 +    with `Inf S \<notin> S` S have "Inf S < s"
   8.100 +      unfolding less_le by (blast intro: cInf_lower)
   8.101 +    show ?thesis
   8.102 +    proof (rule ccontr)
   8.103 +      assume "\<not> ?thesis"
   8.104 +      with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "Inf S < b"
   8.105 +        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s:S. f s)"
   8.106 +        by (auto simp: not_le eventually_at_right[OF `Inf S < s`])
   8.107 +      with `S \<noteq> {}` obtain c where "c \<in> S" "c < b"
   8.108 +        using cInf_lessD[of S b] by auto
   8.109 +      with `Inf S \<notin> S` S have "Inf S < c"
   8.110 +        unfolding less_le by (blast intro: cInf_lower)
   8.111 +      from *[OF `Inf S < c` `c < b`] cINF_lower[OF bdd_below_image_mono[of f] `c \<in> S`]
   8.112 +      show False
   8.113 +        by (auto simp: assms)
   8.114 +    qed
   8.115 +  qed
   8.116 +qed (intro cINF_greatest `mono f`[THEN monoD] cInf_lower `bdd_below S` `S \<noteq> {}`)
   8.117 +
   8.118 +lemma continuous_at_Inf_antimono:
   8.119 +  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
   8.120 +  assumes "antimono f"
   8.121 +  assumes cont: "continuous (at_right (Inf S)) f"
   8.122 +  assumes S: "S \<noteq> {}" "bdd_below S"
   8.123 +  shows "f (Inf S) = (SUP s:S. f s)"
   8.124 +proof (rule antisym)
   8.125 +  have f: "(f ---> f (Inf S)) (at_right (Inf S))"
   8.126 +    using cont unfolding continuous_within .
   8.127 +
   8.128 +  show "f (Inf S) \<le> (SUP s:S. f s)"
   8.129 +  proof cases
   8.130 +    assume "Inf S \<in> S" then show ?thesis
   8.131 +      by (rule cSUP_upper) (auto intro: bdd_above_image_antimono S `antimono f`)
   8.132 +  next
   8.133 +    assume "Inf S \<notin> S"
   8.134 +    from `S \<noteq> {}` obtain s where "s \<in> S"
   8.135 +      by auto
   8.136 +    with `Inf S \<notin> S` S have "Inf S < s"
   8.137 +      unfolding less_le by (blast intro: cInf_lower)
   8.138 +    show ?thesis
   8.139 +    proof (rule ccontr)
   8.140 +      assume "\<not> ?thesis"
   8.141 +      with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "Inf S < b"
   8.142 +        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s:S. f s) < f y"
   8.143 +        by (auto simp: not_le eventually_at_right[OF `Inf S < s`])
   8.144 +      with `S \<noteq> {}` obtain c where "c \<in> S" "c < b"
   8.145 +        using cInf_lessD[of S b] by auto
   8.146 +      with `Inf S \<notin> S` S have "Inf S < c"
   8.147 +        unfolding less_le by (blast intro: cInf_lower)
   8.148 +      from *[OF `Inf S < c` `c < b`] cSUP_upper[OF `c \<in> S` bdd_above_image_antimono[of f]]
   8.149 +      show False
   8.150 +        by (auto simp: assms)
   8.151 +    qed
   8.152 +  qed
   8.153 +qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
   8.154 +
   8.155  subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
   8.156  
   8.157  context begin interpretation lifting_syntax .