# HG changeset patch
# User hoelzl
# Date 1422371560 -3600
# Node ID 2538b2c51769f9e40c424644233f8f8c5cb6eac3
# Parent  86be42bb5174e0c00de98329419d4678dd55fed7
ereal: tuned proofs concerning continuity and suprema

diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -102,15 +102,25 @@
 lemma (in order_bot) bdd_above_bot[simp, intro!]: "bdd_below A"
   by (rule bdd_belowI[of _ bot]) simp
 
-lemma bdd_above_uminus[simp]:
-  fixes X :: "'a::ordered_ab_group_add set"
-  shows "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
-  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
+lemma bdd_above_image_mono: "mono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_above (f`A)"
+  by (auto simp: bdd_above_def mono_def)
+
+lemma bdd_below_image_mono: "mono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_below (f`A)"
+  by (auto simp: bdd_below_def mono_def)
+  
+lemma bdd_above_image_antimono: "antimono f \<Longrightarrow> bdd_below A \<Longrightarrow> bdd_above (f`A)"
+  by (auto simp: bdd_above_def bdd_below_def antimono_def)
 
-lemma bdd_below_uminus[simp]:
+lemma bdd_below_image_antimono: "antimono f \<Longrightarrow> bdd_above A \<Longrightarrow> bdd_below (f`A)"
+  by (auto simp: bdd_above_def bdd_below_def antimono_def)
+
+lemma
   fixes X :: "'a::ordered_ab_group_add set"
-  shows"bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
-  by (auto simp: bdd_above_def bdd_below_def intro: le_imp_neg_le) (metis le_imp_neg_le minus_minus)
+  shows bdd_above_uminus[simp]: "bdd_above (uminus ` X) \<longleftrightarrow> bdd_below X"
+    and bdd_below_uminus[simp]: "bdd_below (uminus ` X) \<longleftrightarrow> bdd_above X"
+  using bdd_above_image_antimono[of uminus X] bdd_below_image_antimono[of uminus "uminus`X"]
+  using bdd_below_image_antimono[of uminus X] bdd_above_image_antimono[of uminus "uminus`X"]
+  by (auto simp: antimono_def image_image)
 
 context lattice
 begin
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -568,6 +568,9 @@
 lemma ereal_uminus_less_reorder: "- a < b \<longleftrightarrow> -b < (a::ereal)"
   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
 
+lemma ereal_less_uminus_reorder: "a < - b \<longleftrightarrow> b < - (a::ereal)"
+  by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_less_minus)
+
 lemma ereal_uminus_le_reorder: "- a \<le> b \<longleftrightarrow> -b \<le> (a::ereal)"
   by (subst (3) ereal_uminus_uminus[symmetric]) (simp only: ereal_minus_le_minus)
 
@@ -1605,39 +1608,142 @@
   show "\<exists>a b::ereal. a \<noteq> b"
     using zero_neq_one by blast
 qed
+subsubsection "Topological space"
+
+instantiation ereal :: linear_continuum_topology
+begin
+
+definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
+  open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
+
+instance
+  by default (simp add: open_ereal_generated)
+
+end
+
+lemma tendsto_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. ereal (f x)) ---> ereal x) F"
+  apply (rule tendsto_compose[where g=ereal])
+  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+  apply (rule_tac x="case a of MInfty \<Rightarrow> UNIV | ereal x \<Rightarrow> {x <..} | PInfty \<Rightarrow> {}" in exI)
+  apply (auto split: ereal.split) []
+  apply (rule_tac x="case a of MInfty \<Rightarrow> {} | ereal x \<Rightarrow> {..< x} | PInfty \<Rightarrow> UNIV" in exI)
+  apply (auto split: ereal.split) []
+  done
+
+lemma tendsto_uminus_ereal[tendsto_intros, simp, intro]: "(f ---> x) F \<Longrightarrow> ((\<lambda>x. - f x::ereal) ---> - x) F"
+  apply (rule tendsto_compose[where g=uminus])
+  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+  apply (rule_tac x="{..< -a}" in exI)
+  apply (auto split: ereal.split simp: ereal_less_uminus_reorder) []
+  apply (rule_tac x="{- a <..}" in exI)
+  apply (auto split: ereal.split simp: ereal_uminus_reorder) []
+  done
+
+lemma ereal_Lim_uminus: "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x::ereal) ---> - f0) net"
+  using tendsto_uminus_ereal[of f f0 net] tendsto_uminus_ereal[of "\<lambda>x. - f x" "- f0" net]
+  by auto
+
+lemma ereal_divide_less_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a / c < b \<longleftrightarrow> a < b * c"
+  by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
+
+lemma ereal_less_divide_iff: "0 < (c::ereal) \<Longrightarrow> c < \<infinity> \<Longrightarrow> a < b / c \<longleftrightarrow> a * c < b"
+  by (cases a b c rule: ereal3_cases) (auto simp: field_simps)
+
+lemma tendsto_cmult_ereal[tendsto_intros, simp, intro]:
+  assumes c: "\<bar>c\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+proof -
+  { fix c :: ereal assume "0 < c" "c < \<infinity>"
+    then have "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+      apply (intro tendsto_compose[OF _ f])
+      apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+      apply (rule_tac x="{a/c <..}" in exI)
+      apply (auto split: ereal.split simp: ereal_divide_less_iff mult.commute) []
+      apply (rule_tac x="{..< a/c}" in exI)
+      apply (auto split: ereal.split simp: ereal_less_divide_iff mult.commute) []
+      done }
+  note * = this
+
+  have "((0 < c \<and> c < \<infinity>) \<or> (-\<infinity> < c \<and> c < 0) \<or> c = 0)"
+    using c by (cases c) auto
+  then show ?thesis
+  proof (elim disjE conjE)
+    assume "- \<infinity> < c" "c < 0"
+    then have "0 < - c" "- c < \<infinity>"
+      by (auto simp: ereal_uminus_reorder ereal_less_uminus_reorder[of 0])
+    then have "((\<lambda>x. (- c) * f x) ---> (- c) * x) F"
+      by (rule *)
+    from tendsto_uminus_ereal[OF this] show ?thesis 
+      by simp
+  qed (auto intro!: *)
+qed
+
+lemma tendsto_cmult_ereal_not_0[tendsto_intros, simp, intro]:
+  assumes "x \<noteq> 0" and f: "(f ---> x) F" shows "((\<lambda>x. c * f x::ereal) ---> c * x) F"
+proof cases
+  assume "\<bar>c\<bar> = \<infinity>"
+  show ?thesis
+  proof (rule filterlim_cong[THEN iffD1, OF refl refl _ tendsto_const])
+    have "0 < x \<or> x < 0"
+      using `x \<noteq> 0` by (auto simp add: neq_iff)
+    then show "eventually (\<lambda>x'. c * x = c * f x') F"
+    proof
+      assume "0 < x" from order_tendstoD(1)[OF f this] show ?thesis
+        by eventually_elim (insert `0<x` `\<bar>c\<bar> = \<infinity>`, auto)
+    next
+      assume "x < 0" from order_tendstoD(2)[OF f this] show ?thesis
+        by eventually_elim (insert `x<0` `\<bar>c\<bar> = \<infinity>`, auto)
+    qed
+  qed
+qed (rule tendsto_cmult_ereal[OF _ f])
+
+lemma tendsto_cadd_ereal[tendsto_intros, simp, intro]:
+  assumes c: "y \<noteq> - \<infinity>" "x \<noteq> - \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
+  apply (intro tendsto_compose[OF _ f])
+  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+  apply (rule_tac x="{a - y <..}" in exI)
+  apply (auto split: ereal.split simp: ereal_minus_less_iff c) []
+  apply (rule_tac x="{..< a - y}" in exI)
+  apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
+  done
+
+lemma tendsto_add_left_ereal[tendsto_intros, simp, intro]:
+  assumes c: "\<bar>y\<bar> \<noteq> \<infinity>" and f: "(f ---> x) F" shows "((\<lambda>x. f x + y::ereal) ---> x + y) F"
+  apply (intro tendsto_compose[OF _ f])
+  apply (auto intro!: order_tendstoI simp: eventually_at_topological)
+  apply (rule_tac x="{a - y <..}" in exI)
+  apply (insert c, auto split: ereal.split simp: ereal_minus_less_iff) []
+  apply (rule_tac x="{..< a - y}" in exI)
+  apply (auto split: ereal.split simp: ereal_less_minus_iff c) []
+  done
+
+lemma continuous_at_ereal[continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. ereal (f x))"
+  unfolding continuous_def by auto
+
+lemma continuous_on_ereal[continuous_intros]: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. ereal (f x))"
+  unfolding continuous_on_def by auto
 
 lemma ereal_Sup:
   assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
   shows "ereal (Sup A) = (SUP a:A. ereal a)"
-proof (rule antisym)
+proof (rule continuous_at_Sup_mono)
   obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
     using * by (force simp: bot_ereal_def)
-  then have upper: "\<And>a. a \<in> A \<Longrightarrow> a \<le> r"
-    by (auto intro!: SUP_upper simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
-
-  show "ereal (Sup A) \<le> (SUP a:A. ereal a)"
-    using upper by (simp add: r[symmetric] cSup_least[OF `A \<noteq> {}`])
-  show "(SUP a:A. ereal a) \<le> ereal (Sup A)"
-    using upper `A \<noteq> {}` by (intro SUP_least) (auto intro!: cSup_upper bdd_aboveI)
-qed
+  then show "bdd_above A" "A \<noteq> {}"
+    by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
 
 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))"
   using ereal_Sup[of "f`A"] by auto
-  
+
 lemma ereal_Inf:
   assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
   shows "ereal (Inf A) = (INF a:A. ereal a)"
-proof (rule antisym)
+proof (rule continuous_at_Inf_mono)
   obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
     using * by (force simp: top_ereal_def)
-  then have lower: "\<And>a. a \<in> A \<Longrightarrow> r \<le> a"
-    by (auto intro!: INF_lower simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
-
-  show "(INF a:A. ereal a) \<le> ereal (Inf A)"
-    using lower by (simp add: r[symmetric] cInf_greatest[OF `A \<noteq> {}`])
-  show "ereal (Inf A) \<le> (INF a:A. ereal a)"
-    using lower `A \<noteq> {}` by (intro INF_greatest) (auto intro!: cInf_lower bdd_belowI)
-qed
+  then show "bdd_below A" "A \<noteq> {}"
+    by (auto intro!: INF_lower bdd_belowI[of _ r] simp add: ereal_less_eq(3)[symmetric] simp del: ereal_less_eq)
+qed (auto simp: mono_def continuous_at_within continuous_at_ereal)
 
 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))"
   using ereal_Inf[of "f`A"] by auto
@@ -1660,9 +1766,15 @@
 
 lemma ereal_INF_uminus_eq:
   fixes f :: "'a \<Rightarrow> ereal"
-  shows "(INF x:S. uminus (f x)) = - (SUP x:S. f x)"
+  shows "(INF x:S. - f x) = - (SUP x:S. f x)"
   using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
 
+lemma ereal_SUP_uminus:
+  fixes f :: "'a \<Rightarrow> ereal"
+  shows "(SUP i : R. - f i) = - (INF i : R. f i)"
+  using ereal_Sup_uminus_image_eq[of "f`R"]
+  by (simp add: image_image)
+
 lemma ereal_SUP_not_infty:
   fixes f :: "_ \<Rightarrow> ereal"
   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>"
@@ -1675,17 +1787,6 @@
   using INF_lower2[of _ A f u] INF_greatest[of A l f]
   by (cases "INFIMUM A f") auto
 
-lemma ereal_SUP_uminus:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
-  using ereal_Sup_uminus_image_eq[of "f`R"]
-  by (simp add: image_image)
-
-lemma ereal_INF_uminus:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "(INF i : R. - f i) = - (SUP i : R. f i)"
-  using ereal_SUP_uminus [of _ "\<lambda>x. - f x"] by simp
-
 lemma ereal_image_uminus_shift:
   fixes X Y :: "ereal set"
   shows "uminus ` X = Y \<longleftrightarrow> X = uminus ` Y"
@@ -1697,12 +1798,6 @@
     by (simp add: image_image)
 qed (simp add: image_image)
 
-lemma Inf_ereal_iff:
-  fixes z :: ereal
-  shows "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x < y) \<longleftrightarrow> Inf X < y"
-  by (metis complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower
-      less_le_not_le linear order_less_le_trans)
-
 lemma Sup_eq_MInfty:
   fixes S :: "ereal set"
   shows "Sup S = -\<infinity> \<longleftrightarrow> S = {} \<or> S = {-\<infinity>}"
@@ -1742,101 +1837,108 @@
 qed
 
 lemma SUP_PInfty:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
-  shows "(SUP i:A. f i) = \<infinity>"
-  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
-  apply simp
-proof safe
-  fix x :: ereal
-  assume "x \<noteq> \<infinity>"
-  show "\<exists>i\<in>A. x < f i"
-  proof (cases x)
-    case PInf
-    with `x \<noteq> \<infinity>` show ?thesis
-      by simp
-  next
-    case MInf
-    with assms[of "0"] show ?thesis
-      by force
-  next
-    case (real r)
-    with less_PInf_Ex_of_nat[of x] obtain n :: nat where "x < ereal (real n)"
-      by auto
-    moreover obtain i where "i \<in> A" "ereal (real n) \<le> f i"
-      using assms ..
-    ultimately show ?thesis
-      by (auto intro!: bexI[of _ i])
-  qed
-qed
+  "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i:A. f i :: ereal) = \<infinity>"
+  unfolding top_ereal_def[symmetric] SUP_eq_top_iff
+  by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
 
 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
   by (rule SUP_PInfty) auto
 
-lemma Inf_less:
-  fixes x :: ereal
-  assumes "(INF i:A. f i) < x"
-  shows "\<exists>i. i \<in> A \<and> f i \<le> x"
-proof (rule ccontr)
-  assume "\<not> ?thesis"
-  then have "\<forall>i\<in>A. f i > x"
-    by auto
-  then have "(INF i:A. f i) \<ge> x"
-    by (subst INF_greatest) auto
-  then show False
-    using assms by auto
+lemma SUP_ereal_add_left:
+  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
+  shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
+proof cases
+  assume "(SUP i:I. f i) = - \<infinity>"
+  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
+    unfolding Sup_eq_MInfty Sup_image_eq[symmetric] by auto
+  ultimately show ?thesis
+    by (cases c) (auto simp: `I \<noteq> {}`)
+next
+  assume "(SUP i:I. f i) \<noteq> - \<infinity>" then show ?thesis
+    unfolding Sup_image_eq[symmetric]
+    by (subst continuous_at_Sup_mono[where f="\<lambda>x. x + c"])
+       (auto simp: continuous_at_within continuous_at mono_def ereal_add_mono `I \<noteq> {}` `c \<noteq> -\<infinity>`)
+qed
+
+lemma SUP_ereal_add_right:
+  fixes c :: ereal
+  shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)"
+  using SUP_ereal_add_left[of I c f] by (simp add: add.commute)
+
+lemma SUP_ereal_minus_right:
+  assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
+  shows "(SUP i:I. c - f i :: ereal) = c - (INF i:I. f i)"
+  using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
+  by (simp add: ereal_SUP_uminus minus_ereal_def)
+
+lemma SUP_ereal_minus_left:
+  assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
+  shows "(SUP i:I. f i - c:: ereal) = (SUP i:I. f i) - c"
+  using SUP_ereal_add_left[OF `I \<noteq> {}`, of "-c" f] by (simp add: `c \<noteq> \<infinity>` minus_ereal_def)
+
+lemma INF_ereal_minus_right:
+  assumes "I \<noteq> {}" and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "(INF i:I. c - f i) = c - (SUP i:I. f i::ereal)"
+proof -
+  { fix b have "(-c) + b = - (c - b)"
+      using `\<bar>c\<bar> \<noteq> \<infinity>` by (cases c b rule: ereal2_cases) auto }
+  note * = this
+  show ?thesis
+    using SUP_ereal_add_right[OF `I \<noteq> {}`, of "-c" f] `\<bar>c\<bar> \<noteq> \<infinity>`
+    by (auto simp add: * ereal_SUP_uminus_eq)
 qed
 
 lemma SUP_ereal_le_addI:
   fixes f :: "'i \<Rightarrow> ereal"
-  assumes "\<And>i. f i + y \<le> z"
-    and "y \<noteq> -\<infinity>"
+  assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
   shows "SUPREMUM UNIV f + y \<le> z"
-proof (cases y)
-  case (real r)
-  then have "\<And>i. f i \<le> z - y"
-    using assms by (simp add: ereal_le_minus_iff)
-  then have "SUPREMUM UNIV f \<le> z - y"
-    by (rule SUP_least)
-  then show ?thesis
-    using real by (simp add: ereal_le_minus_iff)
-qed (insert assms, auto)
+  unfolding SUP_ereal_add_left[OF UNIV_not_empty `y \<noteq> -\<infinity>`, symmetric]
+  by (rule SUP_least assms)+
+
+lemma SUP_combine:
+  fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
+  assumes mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> f a c \<le> f b d"
+  shows "(SUP i:UNIV. SUP j:UNIV. f i j) = (SUP i. f i i)"
+proof (rule antisym)
+  show "(SUP i j. f i j) \<le> (SUP i. f i i)"
+    by (rule SUP_least SUP_upper2[where i="sup i j" for i j] UNIV_I mono sup_ge1 sup_ge2)+
+  show "(SUP i. f i i) \<le> (SUP i j. f i j)"
+    by (rule SUP_least SUP_upper2 UNIV_I mono order_refl)+
+qed
 
 lemma SUP_ereal_add:
   fixes f g :: "nat \<Rightarrow> ereal"
-  assumes "incseq f"
-    and "incseq g"
+  assumes inc: "incseq f" "incseq g"
     and pos: "\<And>i. f i \<noteq> -\<infinity>" "\<And>i. g i \<noteq> -\<infinity>"
   shows "(SUP i. f i + g i) = SUPREMUM UNIV f + SUPREMUM UNIV g"
-proof (rule SUP_eqI)
-  fix y
-  assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
-  have f: "SUPREMUM UNIV f \<noteq> -\<infinity>"
-    using pos
-    unfolding SUP_def Sup_eq_MInfty
-    by (auto dest: image_eqD)
-  {
-    fix j
-    {
-      fix i
-      have "f i + g j \<le> f i + g (max i j)"
-        using `incseq g`[THEN incseqD]
-        by (rule add_left_mono) auto
-      also have "\<dots> \<le> f (max i j) + g (max i j)"
-        using `incseq f`[THEN incseqD]
-        by (rule add_right_mono) auto
-      also have "\<dots> \<le> y" using * by auto
-      finally have "f i + g j \<le> y" .
-    }
-    then have "SUPREMUM UNIV f + g j \<le> y"
-      using assms(4)[of j] by (intro SUP_ereal_le_addI) auto
-    then have "g j + SUPREMUM UNIV f \<le> y" by (simp add: ac_simps)
-  }
-  then have "SUPREMUM UNIV g + SUPREMUM UNIV f \<le> y"
-    using f by (rule SUP_ereal_le_addI)
-  then show "SUPREMUM UNIV f + SUPREMUM UNIV g \<le> y"
-    by (simp add: ac_simps)
-qed (auto intro!: add_mono SUP_upper)
+  apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty])
+  apply (metis SUP_upper UNIV_I assms(4) ereal_infty_less_eq(2))
+  apply (subst (2) add.commute)
+  apply (subst SUP_ereal_add_left[symmetric, OF UNIV_not_empty assms(3)])
+  apply (subst (2) add.commute)
+  apply (rule SUP_combine[symmetric] ereal_add_mono inc[THEN monoD] | assumption)+
+  done
+
+lemma INF_ereal_add:
+  fixes f :: "nat \<Rightarrow> ereal"
+  assumes "decseq f" "decseq g"
+    and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
+  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
+proof -
+  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
+    using assms unfolding INF_less_iff by auto
+  { fix a b :: ereal assume "a \<noteq> \<infinity>" "b \<noteq> \<infinity>"
+    then have "- ((- a) + (- b)) = a + b"
+      by (cases a b rule: ereal2_cases) auto }
+  note * = this
+  have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
+    by (simp add: fin *)
+  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
+    unfolding ereal_INF_uminus_eq
+    using assms INF_less
+    by (subst SUP_ereal_add) (auto simp: ereal_SUP_uminus fin *)
+  finally show ?thesis .
+qed
 
 lemma SUP_ereal_add_pos:
   fixes f g :: "nat \<Rightarrow> ereal"
@@ -1863,313 +1965,85 @@
   then show ?thesis by simp
 qed
 
-lemma SUP_ereal_cmult:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "\<And>i. 0 \<le> f i"
-    and "0 \<le> c"
-  shows "(SUP i. c * f i) = c * SUPREMUM UNIV f"
-proof (rule SUP_eqI)
-  fix i
-  have "f i \<le> SUPREMUM UNIV f"
-    by (rule SUP_upper) auto
-  then show "c * f i \<le> c * SUPREMUM UNIV f"
-    using `0 \<le> c` by (rule ereal_mult_left_mono)
-next
-  fix y
-  assume "\<And>i. i \<in> UNIV \<Longrightarrow> c * f i \<le> y"
-  then have *: "\<And>i. c * f i \<le> y" by simp
-  show "c * SUPREMUM UNIV f \<le> y"
-  proof (cases "0 < c \<and> c \<noteq> \<infinity>")
-    case True
-    with * have "SUPREMUM UNIV f \<le> y / c"
-      by (intro SUP_least) (auto simp: ereal_le_divide_pos)
-    with True show ?thesis
-      by (auto simp: ereal_le_divide_pos)
-  next
-    case False
-    {
-      assume "c = \<infinity>"
-      have ?thesis
-      proof (cases "\<forall>i. f i = 0")
-        case True
-        then have "range f = {0}"
-          by auto
-        with True show "c * SUPREMUM UNIV f \<le> y"
-          using * by auto
-      next
-        case False
-        then obtain i where "f i \<noteq> 0"
-          by auto
-        with *[of i] `c = \<infinity>` `0 \<le> f i` show ?thesis
-          by (auto split: split_if_asm)
-      qed
-    }
-    moreover note False
-    ultimately show ?thesis
-      using * `0 \<le> c` by auto
-  qed
-qed
-
-lemma SUP_ereal_mult_right:
+lemma SUP_ereal_mult_left:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "I \<noteq> {}"
-  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
-    and "0 \<le> c"
+  assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
   shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
-proof (rule SUP_eqI)
-  fix i assume "i \<in> I"
-  then have "f i \<le> SUPREMUM I f"
-    by (rule SUP_upper)
-  then show "c * f i \<le> c * SUPREMUM I f"
-    using `0 \<le> c` by (rule ereal_mult_left_mono)
+proof cases
+  assume "(SUP i:I. f i) = 0"
+  moreover then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
+    by (metis SUP_upper f antisym)
+  ultimately show ?thesis
+    by simp
 next
-  fix y assume *: "\<And>i. i \<in> I \<Longrightarrow> c * f i \<le> y"
-  { assume "c = \<infinity>" have "c * SUPREMUM I f \<le> y"
-    proof cases
-      assume "\<forall>i\<in>I. f i = 0"
-      then show ?thesis
-        using * `c = \<infinity>` by (auto simp: SUP_constant bot_ereal_def)
-    next
-      assume "\<not> (\<forall>i\<in>I. f i = 0)"
-      then obtain i where "f i \<noteq> 0" "i \<in> I"
-        by auto
-      with *[of i] `c = \<infinity>` `i \<in> I \<Longrightarrow> 0 \<le> f i` show ?thesis
-        by (auto split: split_if_asm)
-    qed }
-  moreover
-  { assume "c \<noteq> 0" "c \<noteq> \<infinity>"
-    moreover with `0 \<le> c` * have "SUPREMUM I f \<le> y / c"
-      by (intro SUP_least) (auto simp: ereal_le_divide_pos)
-    ultimately have "c * SUPREMUM I f \<le> y"
-      using `0 \<le> c` * by (auto simp: ereal_le_divide_pos) }
-  moreover { assume "c = 0" with * `I \<noteq> {}` have "c * SUPREMUM I f \<le> y" by auto }
-  ultimately show "c * SUPREMUM I f \<le> y"
-    by blast
+  assume "(SUP i:I. f i) \<noteq> 0" then show ?thesis
+    unfolding SUP_def
+    by (subst continuous_at_Sup_mono[where f="\<lambda>x. c * x"])
+       (auto simp: mono_def continuous_at continuous_at_within `I \<noteq> {}`
+             intro!: ereal_mult_left_mono c)
 qed
 
-lemma SUP_ereal_add_left:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "I \<noteq> {}"
-  assumes "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i"
-    and "0 \<le> c"
-  shows "(SUP i:I. f i + c) = SUPREMUM I f + c"
-proof (intro SUP_eqI)
-  fix B assume *: "\<And>i. i \<in> I \<Longrightarrow> f i + c \<le> B"
-  show "SUPREMUM I f + c \<le> B"
-  proof cases
-    assume "c = \<infinity>" with `I \<noteq> {}` * show ?thesis
-      by auto
-  next
-    assume "c \<noteq> \<infinity>"
-    with `0 \<le> c` have [simp]: "\<bar>c\<bar> \<noteq> \<infinity>"
-      by simp
-    have "SUPREMUM I f \<le> B - c"
-      by (simp add: SUP_le_iff ereal_le_minus *)
-    then show ?thesis
-      by (simp add: ereal_le_minus)
-  qed
-qed (auto intro: ereal_add_mono SUP_upper)
-
-lemma SUP_ereal_add_right:
-  fixes c :: ereal
-  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"
-  using SUP_ereal_add_left[of I f c] by (simp add: add_ac)
+lemma countable_approach: 
+  fixes x :: ereal
+  assumes "x \<noteq> -\<infinity>"
+  shows "\<exists>f. incseq f \<and> (\<forall>i::nat. f i < x) \<and> (f ----> x)"
+proof (cases x)
+  case (real r)
+  moreover have "(\<lambda>n. r - inverse (real (Suc n))) ----> r - 0"
+    by (intro tendsto_intros LIMSEQ_inverse_real_of_nat)
+  ultimately show ?thesis
+    by (intro exI[of _ "\<lambda>n. x - inverse (Suc n)"]) (auto simp: incseq_def)
+next 
+  case PInf with LIMSEQ_SUP[of "\<lambda>n::nat. ereal (real n)"] show ?thesis
+    by (intro exI[of _ "\<lambda>n. ereal (real n)"]) (auto simp: incseq_def SUP_nat_Infty)
+qed (simp add: assms)
 
 lemma Sup_countable_SUP:
   assumes "A \<noteq> {}"
-  shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPREMUM UNIV f"
-proof (cases "Sup A")
-  case (real r)
-  have "\<forall>n::nat. \<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
-  proof
-    fix n :: nat
-    have "\<exists>x\<in>A. Sup A - 1 / ereal (real n) < x"
-      using assms real by (intro Sup_ereal_close) (auto simp: one_ereal_def)
-    then obtain x where "x \<in> A" "Sup A - 1 / ereal (real n) < x" ..
-    then show "\<exists>x. x \<in> A \<and> Sup A < x + 1 / ereal (real n)"
-      by (auto intro!: exI[of _ x] simp: ereal_minus_less_iff)
-  qed
-  from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
-    where f: "\<forall>x. f x \<in> A \<and> Sup A < f x + 1 / ereal (real x)" ..
-  have "SUPREMUM UNIV f = Sup A"
-  proof (rule SUP_eqI)
-    fix i
-    show "f i \<le> Sup A"
-      using f by (auto intro!: complete_lattice_class.Sup_upper)
-  next
-    fix y
-    assume bound: "\<And>i. i \<in> UNIV \<Longrightarrow> f i \<le> y"
-    show "Sup A \<le> y"
-    proof (rule ereal_le_epsilon, intro allI impI)
-      fix e :: ereal
-      assume "0 < e"
-      show "Sup A \<le> y + e"
-      proof (cases e)
-        case (real r)
-        then have "0 < r"
-          using `0 < e` by auto
-        then obtain n :: nat where *: "1 / real n < r" "0 < n"
-          using ex_inverse_of_nat_less
-          by (auto simp: real_eq_of_nat inverse_eq_divide)
-        have "Sup A \<le> f n + 1 / ereal (real n)"
-          using f[THEN spec, of n]
-          by auto
-        also have "1 / ereal (real n) \<le> e"
-          using real *
-          by (auto simp: one_ereal_def )
-        with bound have "f n + 1 / ereal (real n) \<le> y + e"
-          by (rule add_mono) simp
-        finally show "Sup A \<le> y + e" .
-      qed (insert `0 < e`, auto)
-    qed
-  qed
-  with f show ?thesis
-    by (auto intro!: exI[of _ f])
-next
-  case PInf
-  from `A \<noteq> {}` obtain x where "x \<in> A"
-    by auto
-  show ?thesis
-  proof (cases "\<infinity> \<in> A")
-    case True
-    then have "\<infinity> \<le> Sup A"
-      by (intro complete_lattice_class.Sup_upper)
-    with True show ?thesis
-      by (auto intro!: exI[of _ "\<lambda>x. \<infinity>"])
-  next
-    case False
-    have "\<exists>x\<in>A. 0 \<le> x"
-      by (metis Infty_neq_0(2) PInf complete_lattice_class.Sup_least ereal_infty_less_eq2(1) linorder_linear)
-    then obtain x where "x \<in> A" and "0 \<le> x"
-      by auto
-    have "\<forall>n::nat. \<exists>f. f \<in> A \<and> x + ereal (real n) \<le> f"
-    proof (rule ccontr)
-      assume "\<not> ?thesis"
-      then have "\<exists>n::nat. Sup A \<le> x + ereal (real n)"
-        by (simp add: Sup_le_iff not_le less_imp_le Ball_def) (metis less_imp_le)
-      then show False using `x \<in> A` `\<infinity> \<notin> A` PInf
-        by (cases x) auto
-    qed
-    from choice[OF this] obtain f :: "nat \<Rightarrow> ereal"
-      where f: "\<forall>z. f z \<in> A \<and> x + ereal (real z) \<le> f z" ..
-    have "SUPREMUM UNIV f = \<infinity>"
-    proof (rule SUP_PInfty)
-      fix n :: nat
-      show "\<exists>i\<in>UNIV. ereal (real n) \<le> f i"
-        using f[THEN spec, of n] `0 \<le> x`
-        by (cases rule: ereal2_cases[of "f n" x]) (auto intro!: exI[of _ n])
-    qed
-    then show ?thesis
-      using f PInf by (auto intro!: exI[of _ f])
-  qed
-next
-  case MInf
+  shows "\<exists>f::nat \<Rightarrow> ereal. incseq f \<and> range f \<subseteq> A \<and> Sup A = (SUP i. f i)"
+proof cases
+  assume "Sup A = -\<infinity>"
   with `A \<noteq> {}` have "A = {-\<infinity>}"
     by (auto simp: Sup_eq_MInfty)
   then show ?thesis
-    using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
+    by (auto intro!: exI[of _ "\<lambda>_. -\<infinity>"] simp: bot_ereal_def)
+next
+  assume "Sup A \<noteq> -\<infinity>"
+  then obtain l where "incseq l" and l: "\<And>i::nat. l i < Sup A" and l_Sup: "l ----> Sup A"
+    by (auto dest: countable_approach)
+
+  have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
+  proof (rule dependent_nat_choice)
+    show "\<exists>x. x \<in> A \<and> l 0 \<le> x"
+      using l[of 0] by (auto simp: less_Sup_iff)
+  next
+    fix x n assume "x \<in> A \<and> l n \<le> x"
+    moreover from l[of "Suc n"] obtain y where "y \<in> A" "l (Suc n) < y"
+      by (auto simp: less_Sup_iff)
+    ultimately show "\<exists>y. (y \<in> A \<and> l (Suc n) \<le> y) \<and> x \<le> y"
+      by (auto intro!: exI[of _ "max x y"] split: split_max)
+  qed
+  then guess f .. note f = this
+  then have "range f \<subseteq> A" "incseq f"
+    by (auto simp: incseq_Suc_iff)
+  moreover
+  have "(SUP i. f i) = Sup A"
+  proof (rule tendsto_unique)
+    show "f ----> (SUP i. f i)"
+      by (rule LIMSEQ_SUP `incseq f`)+
+    show "f ----> Sup A"
+      using l f
+      by (intro tendsto_sandwich[OF _ _ l_Sup tendsto_const])
+         (auto simp: Sup_upper)
+  qed simp
+  ultimately show ?thesis
+    by auto
 qed
 
 lemma SUP_countable_SUP:
   "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPREMUM A g = SUPREMUM UNIV f"
-  using Sup_countable_SUP [of "g`A"]
-  by auto
-
-lemma Sup_ereal_cadd:
-  fixes A :: "ereal set"
-  assumes "A \<noteq> {}"
-    and "a \<noteq> -\<infinity>"
-  shows "Sup ((\<lambda>x. a + x) ` A) = a + Sup A"
-proof (rule antisym)
-  have *: "\<And>a::ereal. \<And>A. Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A"
-    by (auto intro!: add_mono complete_lattice_class.SUP_least complete_lattice_class.Sup_upper)
-  then show "Sup ((\<lambda>x. a + x) ` A) \<le> a + Sup A" .
-  show "a + Sup A \<le> Sup ((\<lambda>x. a + x) ` A)"
-  proof (cases a)
-    case PInf with `A \<noteq> {}`
-    show ?thesis
-      by (auto simp: image_constant max.absorb1)
-  next
-    case (real r)
-    then have **: "op + (- a) ` op + a ` A = A"
-      by (auto simp: image_iff ac_simps zero_ereal_def[symmetric])
-    from *[of "-a" "(\<lambda>x. a + x) ` A"] real show ?thesis
-      unfolding **
-      by (cases rule: ereal2_cases[of "Sup A" "Sup (op + a ` A)"]) auto
-  qed (insert `a \<noteq> -\<infinity>`, auto)
-qed
-
-lemma Sup_ereal_cminus:
-  fixes A :: "ereal set"
-  assumes "A \<noteq> {}"
-    and "a \<noteq> -\<infinity>"
-  shows "Sup ((\<lambda>x. a - x) ` A) = a - Inf A"
-  using Sup_ereal_cadd [of "uminus ` A" a] assms
-  unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
-
-lemma SUP_ereal_cminus:
-  fixes f :: "'i \<Rightarrow> ereal"
-  fixes A
-  assumes "A \<noteq> {}"
-    and "a \<noteq> -\<infinity>"
-  shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
-  using Sup_ereal_cminus[of "f`A" a] assms
-  unfolding SUP_def INF_def image_image by auto
-
-lemma Inf_ereal_cminus:
-  fixes A :: "ereal set"
-  assumes "A \<noteq> {}"
-    and "\<bar>a\<bar> \<noteq> \<infinity>"
-  shows "Inf ((\<lambda>x. a - x) ` A) = a - Sup A"
-proof -
-  {
-    fix x
-    have "-a - -x = -(a - x)"
-      using assms by (cases x) auto
-  } note * = this
-  then have "(\<lambda>x. -a - x)`uminus`A = uminus ` (\<lambda>x. a - x) ` A"
-    by (auto simp: image_image)
-  with * show ?thesis
-    using Sup_ereal_cminus [of "uminus ` A" "- a"] assms
-    by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
-qed
-
-lemma INF_ereal_cminus:
-  fixes a :: ereal
-  assumes "A \<noteq> {}"
-    and "\<bar>a\<bar> \<noteq> \<infinity>"
-  shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
-  using Inf_ereal_cminus[of "f`A" a] assms
-  unfolding SUP_def INF_def image_image
-  by auto
-
-lemma uminus_ereal_add_uminus_uminus:
-  fixes a b :: ereal
-  shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
-  by (cases rule: ereal2_cases[of a b]) auto
-
-lemma INF_ereal_add:
-  fixes f :: "nat \<Rightarrow> ereal"
-  assumes "decseq f" "decseq g"
-    and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
-  shows "(INF i. f i + g i) = INFIMUM UNIV f + INFIMUM UNIV g"
-proof -
-  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
-    using assms unfolding INF_less_iff by auto
-  {
-    fix i
-    from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
-      by (rule uminus_ereal_add_uminus_uminus)
-  }
-  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
-    by simp
-  also have "\<dots> = INFIMUM UNIV f + INFIMUM UNIV g"
-    unfolding ereal_INF_uminus
-    using assms INF_less
-    by (subst SUP_ereal_add)
-       (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
-  finally show ?thesis .
-qed
+  using Sup_countable_SUP [of "g`A"] by auto
 
 subsection "Relation to @{typ enat}"
 
@@ -2225,19 +2099,6 @@
 
 subsection "Limits on @{typ ereal}"
 
-subsubsection "Topological space"
-
-instantiation ereal :: linear_continuum_topology
-begin
-
-definition "open_ereal" :: "ereal set \<Rightarrow> bool" where
-  open_ereal_generated: "open_ereal = generate_topology (range lessThan \<union> range greaterThan)"
-
-instance
-  by default (simp add: open_ereal_generated)
-
-end
-
 lemma open_PInfty: "open A \<Longrightarrow> \<infinity> \<in> A \<Longrightarrow> (\<exists>x. {ereal x<..} \<subseteq> A)"
   unfolding open_ereal_generated
 proof (induct rule: generate_topology.induct)
@@ -2279,23 +2140,7 @@
 qed (fastforce simp add: vimage_Union)+
 
 lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
-  unfolding open_ereal_generated
-proof (induct rule: generate_topology.induct)
-  case (Int A B)
-  then show ?case
-    by auto
-next
-  case (Basis S)
-  {
-    fix x have
-      "ereal -` {..<x} = (case x of PInfty \<Rightarrow> UNIV | MInfty \<Rightarrow> {} | ereal r \<Rightarrow> {..<r})"
-      "ereal -` {x<..} = (case x of PInfty \<Rightarrow> {} | MInfty \<Rightarrow> UNIV | ereal r \<Rightarrow> {r<..})"
-      by (induct x) auto
-  }
-  moreover note Basis
-  ultimately show ?case
-    by (auto split: ereal.split)
-qed (fastforce simp add: vimage_Union)+
+  by (intro open_vimage continuous_intros)
 
 lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
   unfolding open_generated_order[where 'a=real]
@@ -2422,23 +2267,6 @@
 
 subsubsection {* Convergent sequences *}
 
-lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
-  (is "?l = ?r")
-proof (intro iffI topological_tendstoI)
-  fix S
-  assume "?l" and "open S" and "x \<in> S"
-  then show "eventually (\<lambda>x. f x \<in> S) net"
-    using `?l`[THEN topological_tendstoD, OF open_ereal, OF `open S`]
-    by (simp add: inj_image_mem_iff)
-next
-  fix S
-  assume "?r" and "open S" and "ereal x \<in> S"
-  show "eventually (\<lambda>x. ereal (f x) \<in> S) net"
-    using `?r`[THEN topological_tendstoD, OF open_ereal_vimage, OF `open S`]
-    using `ereal x \<in> S`
-    by auto
-qed
-
 lemma lim_real_of_ereal[simp]:
   assumes lim: "(f ---> ereal x) net"
   shows "((\<lambda>x. real (f x)) ---> x) net"
@@ -2454,6 +2282,9 @@
     by (rule eventually_mono)
 qed
 
+lemma lim_ereal[simp]: "((\<lambda>n. ereal (f n)) ---> ereal x) net \<longleftrightarrow> (f ---> x) net"
+  by (auto dest!: lim_real_of_ereal)
+
 lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
 proof -
   {
@@ -2763,7 +2594,7 @@
 lemma ereal_Limsup_uminus:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
-  unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
+  unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus_eq ..
 
 lemma liminf_bounded_iff:
   fixes x :: "nat \<Rightarrow> ereal"
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -250,71 +250,22 @@
     and t: "\<bar>t\<bar> \<noteq> \<infinity>"
   shows "open ((\<lambda>x. m * x + t) ` S)"
 proof -
-  obtain r where r[simp]: "m = ereal r"
-    using m by (cases m) auto
-  obtain p where p[simp]: "t = ereal p"
-    using t by auto
-  have "r \<noteq> 0" "0 < r" and m': "m \<noteq> \<infinity>" "m \<noteq> -\<infinity>" "m \<noteq> 0"
-    using m by auto
-  from `open S` [THEN ereal_openE]
-  obtain l u where T:
-      "open (ereal -` S)"
-      "\<infinity> \<in> S \<Longrightarrow> {ereal l<..} \<subseteq> S"
-      "- \<infinity> \<in> S \<Longrightarrow> {..<ereal u} \<subseteq> S"
-    by blast
-  let ?f = "(\<lambda>x. m * x + t)"
-  show ?thesis
-    unfolding open_ereal_def
-  proof (intro conjI impI exI subsetI)
-    have "ereal -` ?f ` S = (\<lambda>x. r * x + p) ` (ereal -` S)"
-    proof safe
-      fix x y
-      assume "ereal y = m * x + t" "x \<in> S"
-      then show "y \<in> (\<lambda>x. r * x + p) ` ereal -` S"
-        using `r \<noteq> 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
-    qed force
-    then show "open (ereal -` ?f ` S)"
-      using open_affinity[OF T(1) `r \<noteq> 0`]
-      by (auto simp: ac_simps)
-  next
-    assume "\<infinity> \<in> ?f`S"
-    with `0 < r` have "\<infinity> \<in> S"
-      by auto
-    fix x
-    assume "x \<in> {ereal (r * l + p)<..}"
-    then have [simp]: "ereal (r * l + p) < x"
-      by auto
-    show "x \<in> ?f`S"
-    proof (rule image_eqI)
-      show "x = m * ((x - t) / m) + t"
-        using m t
-        by (cases rule: ereal3_cases[of m x t]) auto
-      have "ereal l < (x - t) / m"
-        using m t
-        by (simp add: ereal_less_divide_pos ereal_less_minus)
-      then show "(x - t) / m \<in> S"
-        using T(2)[OF `\<infinity> \<in> S`] by auto
-    qed
-  next
-    assume "-\<infinity> \<in> ?f ` S"
-    with `0 < r` have "-\<infinity> \<in> S"
-      by auto
-    fix x assume "x \<in> {..<ereal (r * u + p)}"
-    then have [simp]: "x < ereal (r * u + p)"
-      by auto
-    show "x \<in> ?f`S"
-    proof (rule image_eqI)
-      show "x = m * ((x - t) / m) + t"
-        using m t
-        by (cases rule: ereal3_cases[of m x t]) auto
-      have "(x - t)/m < ereal u"
-        using m t
-        by (simp add: ereal_divide_less_pos ereal_minus_less)
-      then show "(x - t)/m \<in> S"
-        using T(3)[OF `-\<infinity> \<in> S`]
-        by auto
-    qed
-  qed
+  have "open ((\<lambda>x. inverse m * (x + -t)) -` S)"
+    using m t
+    apply (intro open_vimage `open S`)
+    apply (intro continuous_at_imp_continuous_on ballI tendsto_cmult_ereal continuous_at[THEN iffD2]
+                 tendsto_ident_at tendsto_add_left_ereal)
+    apply auto
+    done
+  also have "(\<lambda>x. inverse m * (x + -t)) -` S = (\<lambda>x. (x - t) / m) -` S"
+    using m t by (auto simp: divide_ereal_def mult.commute uminus_ereal.simps[symmetric] minus_ereal_def
+                       simp del: uminus_ereal.simps)
+  also have "(\<lambda>x. (x - t) / m) -` S = (\<lambda>x. m * x + t) ` S"
+    using m t
+    by (simp add: set_eq_iff image_iff)
+       (metis abs_ereal_less0 abs_ereal_uminus ereal_divide_eq ereal_eq_minus ereal_minus(7,8)
+              ereal_minus_less_minus ereal_mult_eq_PInfty ereal_uminus_uminus ereal_zero_mult)
+  finally show ?thesis .
 qed
 
 lemma ereal_open_affinity:
@@ -340,45 +291,6 @@
     unfolding image_image by simp
 qed
 
-lemma ereal_lim_mult:
-  fixes X :: "'a \<Rightarrow> ereal"
-  assumes lim: "(X ---> L) net"
-    and a: "\<bar>a\<bar> \<noteq> \<infinity>"
-  shows "((\<lambda>i. a * X i) ---> a * L) net"
-proof cases
-  assume "a \<noteq> 0"
-  show ?thesis
-  proof (rule topological_tendstoI)
-    fix S
-    assume "open S" and "a * L \<in> S"
-    have "a * L / a = L"
-      using `a \<noteq> 0` a
-      by (cases rule: ereal2_cases[of a L]) auto
-    then have L: "L \<in> ((\<lambda>x. x / a) ` S)"
-      using `a * L \<in> S`
-      by (force simp: image_iff)
-    moreover have "open ((\<lambda>x. x / a) ` S)"
-      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a \<noteq> 0` a
-      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
-    note * = lim[THEN topological_tendstoD, OF this L]
-    {
-      fix x
-      from a `a \<noteq> 0` have "a * (x / a) = x"
-        by (cases rule: ereal2_cases[of a x]) auto
-    }
-    note this[simp]
-    show "eventually (\<lambda>x. a * X x \<in> S) net"
-      by (rule eventually_mono[OF _ *]) auto
-  qed
-qed auto
-
-lemma ereal_lim_uminus:
-  fixes X :: "'a \<Rightarrow> ereal"
-  shows "((\<lambda>i. - X i) ---> - L) net \<longleftrightarrow> (X ---> L) net"
-  using ereal_lim_mult[of X L net "ereal (-1)"]
-    ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
-  by (auto simp add: algebra_simps)
-
 lemma ereal_open_atLeast:
   fixes x :: ereal
   shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
@@ -409,14 +321,6 @@
   shows "Liminf net (\<lambda>x. - (f x)) = - Limsup net f"
   using ereal_Limsup_uminus[of _ "(\<lambda>x. - (f x))"] by auto
 
-lemma ereal_Lim_uminus:
-  fixes f :: "'a \<Rightarrow> ereal"
-  shows "(f ---> f0) net \<longleftrightarrow> ((\<lambda>x. - f x) ---> - f0) net"
-  using
-    ereal_lim_mult[of f f0 net "- 1"]
-    ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
-  by (auto simp: ereal_uminus_reorder)
-
 lemma Liminf_PInfty:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "\<not> trivial_limit net"
@@ -559,9 +463,9 @@
   case (real r)
   then show ?thesis
     unfolding liminf_SUP_INF limsup_INF_SUP
-    apply (subst INF_ereal_cminus)
+    apply (subst INF_ereal_minus_right)
     apply auto
-    apply (subst SUP_ereal_cminus)
+    apply (subst SUP_ereal_minus_right)
     apply auto
     done
 qed (insert `c \<noteq> -\<infinity>`, simp)
@@ -889,7 +793,7 @@
   shows "(\<Sum>i. a * f i) = a * suminf f"
   by (auto simp: setsum_ereal_right_distrib[symmetric] assms
        ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
-       intro!: SUP_ereal_cmult)
+       intro!: SUP_ereal_mult_left)
 
 lemma suminf_PInfty:
   fixes f :: "nat \<Rightarrow> ereal"
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Probability/Bochner_Integration.thy
--- a/src/HOL/Probability/Bochner_Integration.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -641,7 +641,7 @@
       finally show "?f i \<le> ?g i" .
     qed
     show "?g ----> 0"
-      using ereal_lim_mult[OF f_s, of "ereal K"] by simp
+      using tendsto_cmult_ereal[OF _ f_s, of "ereal K"] by simp
   qed
 
   assume "(\<lambda>i. simple_bochner_integral M (s i)) ----> x"
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Probability/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Lebesgue_Integral_Substitution.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -566,7 +566,7 @@
          (auto simp: incseq_def le_fun_def derivg_nonneg Mf' split: split_indicator
                intro!: ereal_mult_right_mono)
     also from sup have "... = \<integral>\<^sup>+x. (SUP i. F i (g x)) * ereal (g' x) * indicator {a..b} x \<partial>lborel"
-      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_cmult)
+      by (subst mult.assoc, subst mult.commute, subst SUP_ereal_mult_left)
          (auto split: split_indicator simp: derivg_nonneg mult_ac)
     finally show ?case by simp
   qed
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -944,11 +944,11 @@
   next
     show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
       using measure_conv u_range B_u unfolding simple_integral_def
-      by (auto intro!: setsum.cong SUP_ereal_cmult [symmetric])
+      by (auto intro!: setsum.cong SUP_ereal_mult_left [symmetric])
   qed
   moreover
   have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
-    apply (subst SUP_ereal_cmult [symmetric])
+    apply (subst SUP_ereal_mult_left [symmetric])
   proof (safe intro!: SUP_mono bexI)
     fix i
     have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
@@ -1115,7 +1115,7 @@
           by auto }
       then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
         using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
-        by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
+        by (subst SUP_ereal_mult_left [symmetric, OF _ u(6) `0 \<le> a`])
            (auto intro!: SUP_ereal_add
                  simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono) }
     then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
@@ -1127,8 +1127,10 @@
   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)"
     unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
     unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
-    apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
-    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
+    apply (subst SUP_ereal_mult_left [symmetric, OF _ pos(1) `0 \<le> a`])
+    apply simp
+    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf])
+    .
   then show ?thesis by (simp add: nn_integral_max_0)
 qed
 
@@ -2120,7 +2122,7 @@
 next
   case (seq U)
   from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
-    by eventually_elim (simp add: SUP_ereal_cmult seq)
+    by eventually_elim (simp add: SUP_ereal_mult_left seq)
   from seq f show ?case
     apply (simp add: nn_integral_monotone_convergence_SUP)
     apply (subst nn_integral_cong_AE[OF eq])
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Probability/Regularity.thy
--- a/src/HOL/Probability/Regularity.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Probability/Regularity.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -312,7 +312,7 @@
     case 2
     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
     also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
-      unfolding inner by (subst INF_ereal_cminus) force+
+      unfolding inner by (subst INF_ereal_minus_right) force+
     also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
       by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
     also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
@@ -331,7 +331,7 @@
     case 1
     have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
     also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
-      unfolding outer by (subst SUP_ereal_cminus) auto
+      unfolding outer by (subst SUP_ereal_minus_right) auto
     also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
       by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
     also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
diff -r 86be42bb5174 -r 2538b2c51769 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon Jan 26 14:40:13 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue Jan 27 16:12:40 2015 +0100
@@ -2789,6 +2789,154 @@
     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)
 qed
 
+lemma continuous_at_Sup_mono:
+  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+  assumes "mono f"
+  assumes cont: "continuous (at_left (Sup S)) f"
+  assumes S: "S \<noteq> {}" "bdd_above S"
+  shows "f (Sup S) = (SUP s:S. f s)"
+proof (rule antisym)
+  have f: "(f ---> f (Sup S)) (at_left (Sup S))"
+    using cont unfolding continuous_within .
+
+  show "f (Sup S) \<le> (SUP s:S. f s)"
+  proof cases
+    assume "Sup S \<in> S" then show ?thesis
+      by (rule cSUP_upper) (auto intro: bdd_above_image_mono S `mono f`)
+  next
+    assume "Sup S \<notin> S"
+    from `S \<noteq> {}` obtain s where "s \<in> S"
+      by auto
+    with `Sup S \<notin> S` S have "s < Sup S"
+      unfolding less_le by (blast intro: cSup_upper)
+    show ?thesis
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "b < Sup S"
+        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s:S. f s) < f y"
+        by (auto simp: not_le eventually_at_left[OF `s < Sup S`])
+      with `S \<noteq> {}` obtain c where "c \<in> S" "b < c"
+        using less_cSupD[of S b] by auto
+      with `Sup S \<notin> S` S have "c < Sup S"
+        unfolding less_le by (blast intro: cSup_upper)
+      from *[OF `b < c` `c < Sup S`] cSUP_upper[OF `c \<in> S` bdd_above_image_mono[of f]]
+      show False
+        by (auto simp: assms)
+    qed
+  qed
+qed (intro cSUP_least `mono f`[THEN monoD] cSup_upper S)
+
+lemma continuous_at_Sup_antimono:
+  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+  assumes "antimono f"
+  assumes cont: "continuous (at_left (Sup S)) f"
+  assumes S: "S \<noteq> {}" "bdd_above S"
+  shows "f (Sup S) = (INF s:S. f s)"
+proof (rule antisym)
+  have f: "(f ---> f (Sup S)) (at_left (Sup S))"
+    using cont unfolding continuous_within .
+
+  show "(INF s:S. f s) \<le> f (Sup S)"
+  proof cases
+    assume "Sup S \<in> S" then show ?thesis
+      by (intro cINF_lower) (auto intro: bdd_below_image_antimono S `antimono f`)
+  next
+    assume "Sup S \<notin> S"
+    from `S \<noteq> {}` obtain s where "s \<in> S"
+      by auto
+    with `Sup S \<notin> S` S have "s < Sup S"
+      unfolding less_le by (blast intro: cSup_upper)
+    show ?thesis
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "b < Sup S"
+        and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s:S. f s)"
+        by (auto simp: not_le eventually_at_left[OF `s < Sup S`])
+      with `S \<noteq> {}` obtain c where "c \<in> S" "b < c"
+        using less_cSupD[of S b] by auto
+      with `Sup S \<notin> S` S have "c < Sup S"
+        unfolding less_le by (blast intro: cSup_upper)
+      from *[OF `b < c` `c < Sup S`] cINF_lower[OF bdd_below_image_antimono, of f S c] `c \<in> S`
+      show False
+        by (auto simp: assms)
+    qed
+  qed
+qed (intro cINF_greatest `antimono f`[THEN antimonoD] cSup_upper S)
+
+lemma continuous_at_Inf_mono:
+  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+  assumes "mono f"
+  assumes cont: "continuous (at_right (Inf S)) f"
+  assumes S: "S \<noteq> {}" "bdd_below S"
+  shows "f (Inf S) = (INF s:S. f s)"
+proof (rule antisym)
+  have f: "(f ---> f (Inf S)) (at_right (Inf S))"
+    using cont unfolding continuous_within .
+
+  show "(INF s:S. f s) \<le> f (Inf S)"
+  proof cases
+    assume "Inf S \<in> S" then show ?thesis
+      by (rule cINF_lower[rotated]) (auto intro: bdd_below_image_mono S `mono f`)
+  next
+    assume "Inf S \<notin> S"
+    from `S \<noteq> {}` obtain s where "s \<in> S"
+      by auto
+    with `Inf S \<notin> S` S have "Inf S < s"
+      unfolding less_le by (blast intro: cInf_lower)
+    show ?thesis
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "Inf S < b"
+        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s:S. f s)"
+        by (auto simp: not_le eventually_at_right[OF `Inf S < s`])
+      with `S \<noteq> {}` obtain c where "c \<in> S" "c < b"
+        using cInf_lessD[of S b] by auto
+      with `Inf S \<notin> S` S have "Inf S < c"
+        unfolding less_le by (blast intro: cInf_lower)
+      from *[OF `Inf S < c` `c < b`] cINF_lower[OF bdd_below_image_mono[of f] `c \<in> S`]
+      show False
+        by (auto simp: assms)
+    qed
+  qed
+qed (intro cINF_greatest `mono f`[THEN monoD] cInf_lower `bdd_below S` `S \<noteq> {}`)
+
+lemma continuous_at_Inf_antimono:
+  fixes f :: "'a :: {linorder_topology, conditionally_complete_linorder} \<Rightarrow> 'b :: {linorder_topology, conditionally_complete_linorder}"
+  assumes "antimono f"
+  assumes cont: "continuous (at_right (Inf S)) f"
+  assumes S: "S \<noteq> {}" "bdd_below S"
+  shows "f (Inf S) = (SUP s:S. f s)"
+proof (rule antisym)
+  have f: "(f ---> f (Inf S)) (at_right (Inf S))"
+    using cont unfolding continuous_within .
+
+  show "f (Inf S) \<le> (SUP s:S. f s)"
+  proof cases
+    assume "Inf S \<in> S" then show ?thesis
+      by (rule cSUP_upper) (auto intro: bdd_above_image_antimono S `antimono f`)
+  next
+    assume "Inf S \<notin> S"
+    from `S \<noteq> {}` obtain s where "s \<in> S"
+      by auto
+    with `Inf S \<notin> S` S have "Inf S < s"
+      unfolding less_le by (blast intro: cInf_lower)
+    show ?thesis
+    proof (rule ccontr)
+      assume "\<not> ?thesis"
+      with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "Inf S < b"
+        and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s:S. f s) < f y"
+        by (auto simp: not_le eventually_at_right[OF `Inf S < s`])
+      with `S \<noteq> {}` obtain c where "c \<in> S" "c < b"
+        using cInf_lessD[of S b] by auto
+      with `Inf S \<notin> S` S have "Inf S < c"
+        unfolding less_le by (blast intro: cInf_lower)
+      from *[OF `Inf S < c` `c < b`] cSUP_upper[OF `c \<in> S` bdd_above_image_antimono[of f]]
+      show False
+        by (auto simp: assms)
+    qed
+  qed
+qed (intro cSUP_least `antimono f`[THEN antimonoD] cInf_lower S)
+
 subsection {* Setup @{typ "'a filter"} for lifting and transfer *}
 
 context begin interpretation lifting_syntax .