use order topology for extended reals

--- a/src/HOL/Library/Extended_Nat.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -6,7 +6,7 @@
 header {* Extended natural numbers (i.e. with infinity) *}
 
 theory Extended_Nat
-imports Main
+imports "~~/src/HOL/Main"
 begin
 
 class infinity =

--- a/src/HOL/Library/Extended_Real.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -8,9 +8,32 @@
 header {* Extended real number line *}
 
 theory Extended_Real
-imports Complex_Main Extended_Nat
+imports "~~/src/HOL/Complex_Main" Extended_Nat
 begin
 
+lemma LIMSEQ_SUP:
+  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
+  assumes "incseq X"
+  shows "X ----> (SUP i. X i)"
+  using `incseq X`
+  by (intro increasing_tendsto)
+     (auto simp: SUP_upper less_SUP_iff incseq_def eventually_sequentially intro: less_le_trans)
+
+lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
+  by (cases P) (simp_all add: eventually_False)
+
+lemma (in complete_lattice) Inf_le_Sup:
+  assumes "A \<noteq> {}" shows "Inf A \<le> Sup A"
+proof -
+  from `A \<noteq> {}` obtain x where "x \<in> A" by auto
+  then show ?thesis
+    by (metis Sup_upper2 Inf_lower)
+qed
+
+lemma (in complete_lattice) INF_le_SUP:
+  "A \<noteq> {} \<Longrightarrow> INFI A f \<le> SUPR A f"
+  unfolding INF_def SUP_def by (rule Inf_le_Sup) auto
+
 text {*
 
 For more lemmas about the extended real numbers go to
@@ -18,6 +41,26 @@
 
 *}
 
+lemma (in complete_lattice) Sup_eqI:
+  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
+  assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
+  shows "Sup A = x"
+  by (metis antisym Sup_least Sup_upper assms)
+
+lemma (in complete_lattice) Inf_eqI:
+  assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
+  assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
+  shows "Inf A = x"
+  by (metis antisym Inf_greatest Inf_lower assms)
+
+lemma (in complete_lattice) SUP_eqI:
+  "(\<And>i. i \<in> A \<Longrightarrow> f i \<le> x) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> (SUP i:A. f i) = x"
+  unfolding SUP_def by (rule Sup_eqI) auto
+
+lemma (in complete_lattice) INF_eqI:
+  "(\<And>i. i \<in> A \<Longrightarrow> x \<le> f i) \<Longrightarrow> (\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<ge> y) \<Longrightarrow> x \<ge> y) \<Longrightarrow> (INF i:A. f i) = x"
+  unfolding INF_def by (rule Inf_eqI) auto
+
 lemma (in complete_lattice) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
 proof
   assume "{x..} = UNIV"
@@ -1353,22 +1396,6 @@
   unfolding Sup_ereal_def
   by (auto intro!: Least_equality)
 
-lemma ereal_SUPI:
-  fixes x :: ereal
-  assumes "!!i. i : A ==> f i <= x"
-  assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
-  shows "(SUP i:A. f i) = x"
-  unfolding SUP_def Sup_ereal_def
-  using assms by (auto intro!: Least_equality)
-
-lemma ereal_INFI:
-  fixes x :: ereal
-  assumes "!!i. i : A ==> f i >= x"
-  assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
-  shows "(INF i:A. f i) = x"
-  unfolding INF_def Inf_ereal_def
-  using assms by (auto intro!: Greatest_equality)
-
 lemma Sup_ereal_close:
   fixes e :: ereal
   assumes "0 < e" and S: "\<bar>Sup S\<bar> \<noteq> \<infinity>" "S \<noteq> {}"
@@ -1476,6 +1503,17 @@
     using assms by (metis SUP_least SUP_upper2)
 qed
 
+lemma INFI_eq:
+  assumes "\<forall>i\<in>A. \<exists>j\<in>B. f i \<ge> g j"
+  assumes "\<forall>j\<in>B. \<exists>i\<in>A. g j \<ge> f i"
+  shows "(INF i:A. f i) = (INF j:B. g j)"
+proof (intro antisym)
+  show "(INF i:A. f i) \<le> (INF j:B. g j)"
+    using assms by (metis INF_greatest INF_lower2)
+  show "(INF i:B. g i) \<le> (INF j:A. f j)"
+    using assms by (metis INF_greatest INF_lower2)
+qed
+
 lemma SUP_ereal_le_addI:
   fixes f :: "'i \<Rightarrow> ereal"
   assumes "\<And>i. f i + y \<le> z" and "y \<noteq> -\<infinity>"
@@ -1491,7 +1529,7 @@
   fixes f g :: "nat \<Rightarrow> ereal"
   assumes "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) = SUPR UNIV f + SUPR UNIV g"
-proof (rule ereal_SUPI)
+proof (rule SUP_eqI)
   fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
   have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
     unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
@@ -1531,7 +1569,7 @@
 lemma SUPR_ereal_cmult:
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
   shows "(SUP i. c * f i) = c * SUPR UNIV f"
-proof (rule ereal_SUPI)
+proof (rule SUP_eqI)
   fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
   then show "c * f i \<le> c * SUPR UNIV f"
     using `0 \<le> c` by (rule ereal_mult_left_mono)
@@ -1598,7 +1636,7 @@
   qed
   from choice[OF this] guess f .. note f = this
   have "SUPR UNIV f = Sup A"
-  proof (rule ereal_SUPI)
+  proof (rule SUP_eqI)
     fix i show "f i \<le> Sup A" using f
       by (auto intro!: complete_lattice_class.Sup_upper)
   next
@@ -1801,18 +1839,84 @@
 
 subsubsection "Topological space"
 
-instantiation ereal :: topological_space
+instantiation ereal :: linorder_topology
 begin
 
-definition "open A \<longleftrightarrow> open (ereal -` A)
-       \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A))
-       \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+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_def by auto
+  unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+  case (Int A B)
+  moreover then obtain x z where "\<infinity> \<in> A \<Longrightarrow> {ereal x <..} \<subseteq> A" "\<infinity> \<in> B \<Longrightarrow> {ereal z <..} \<subseteq> B"
+      by auto
+  ultimately show ?case
+    by (intro exI[of _ "max x z"]) fastforce
+next
+  { fix x have "x \<noteq> \<infinity> \<Longrightarrow> \<exists>t. x \<le> ereal t" by (cases x) auto }
+  moreover case (Basis S)
+  ultimately show ?case
+    by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
 
 lemma open_MInfty: "open A \<Longrightarrow> -\<infinity> \<in> A \<Longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A)"
-  unfolding open_ereal_def by auto
+  unfolding open_ereal_generated
+proof (induct rule: generate_topology.induct)
+  case (Int A B)
+  moreover then obtain x z where "-\<infinity> \<in> A \<Longrightarrow> {..< ereal x} \<subseteq> A" "-\<infinity> \<in> B \<Longrightarrow> {..< ereal z} \<subseteq> B"
+      by auto
+  ultimately show ?case
+    by (intro exI[of _ "min x z"]) fastforce
+next
+  { fix x have "x \<noteq> - \<infinity> \<Longrightarrow> \<exists>t. ereal t \<le> x" by (cases x) auto }
+  moreover case (Basis S)
+  ultimately show ?case
+    by (auto split: ereal.split)
+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
+  { 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 case (Basis S)
+  ultimately show ?case
+    by (auto split: ereal.split)
+qed (fastforce simp add: vimage_Union)+
+
+lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
+  unfolding open_generated_order[where 'a=real]
+proof (induct rule: generate_topology.induct)
+  case (Basis S)
+  moreover { fix x have "ereal ` {..< x} = { -\<infinity> <..< ereal x }" by auto (case_tac xa, auto) }
+  moreover { fix x have "ereal ` {x <..} = { ereal x <..< \<infinity> }" by auto (case_tac xa, auto) }
+  ultimately show ?case
+     by auto
+qed (auto simp add: image_Union image_Int)
+
+lemma open_ereal_def: "open A \<longleftrightarrow> open (ereal -` A) \<and> (\<infinity> \<in> A \<longrightarrow> (\<exists>x. {ereal x <..} \<subseteq> A)) \<and> (-\<infinity> \<in> A \<longrightarrow> (\<exists>x. {..<ereal x} \<subseteq> A))"
+  (is "open A \<longleftrightarrow> ?rhs")
+proof
+  assume "open A" then show ?rhs
+    using open_PInfty open_MInfty open_ereal_vimage by auto
+next
+  assume "?rhs"
+  then obtain x y where A: "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..< ereal y} \<subseteq> A"
+    by auto
+  have *: "A = ereal ` (ereal -` A) \<union> (if \<infinity> \<in> A then {ereal x<..} else {}) \<union> (if -\<infinity> \<in> A then {..< ereal y} else {})"
+    using A(2,3) by auto
+  from open_ereal[OF A(1)] show "open A"
+    by (subst *) (auto simp: open_Un)
+qed
 
 lemma open_PInfty2: assumes "open A" "\<infinity> \<in> A" obtains x where "{ereal x<..} \<subseteq> A"
   using open_PInfty[OF assms] by auto
@@ -1821,85 +1925,17 @@
   using open_MInfty[OF assms] by auto
 
 lemma ereal_openE: assumes "open A" obtains x y where
-  "open (ereal -` A)"
-  "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A"
-  "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
+  "open (ereal -` A)" "\<infinity> \<in> A \<Longrightarrow> {ereal x<..} \<subseteq> A" "-\<infinity> \<in> A \<Longrightarrow> {..<ereal y} \<subseteq> A"
   using assms open_ereal_def by auto
 
-instance
-proof
-  let ?U = "UNIV::ereal set"
-  show "open ?U" unfolding open_ereal_def
-    by (auto intro!: exI[of _ 0])
-next
-  fix S T::"ereal set" assume "open S" and "open T"
-  from `open S`[THEN ereal_openE] guess xS yS .
-  moreover from `open T`[THEN ereal_openE] guess xT yT .
-  ultimately have
-    "open (ereal -` (S \<inter> T))"
-    "\<infinity> \<in> S \<inter> T \<Longrightarrow> {ereal (max xS xT) <..} \<subseteq> S \<inter> T"
-    "-\<infinity> \<in> S \<inter> T \<Longrightarrow> {..< ereal (min yS yT)} \<subseteq> S \<inter> T"
-    by auto
-  then show "open (S Int T)" unfolding open_ereal_def by blast
-next
-  fix K :: "ereal set set" assume "\<forall>S\<in>K. open S"
-  then have *: "\<forall>S. \<exists>x y. S \<in> K \<longrightarrow> open (ereal -` S) \<and>
-    (\<infinity> \<in> S \<longrightarrow> {ereal x <..} \<subseteq> S) \<and> (-\<infinity> \<in> S \<longrightarrow> {..< ereal y} \<subseteq> S)"
-    by (auto simp: open_ereal_def)
-  then show "open (Union K)" unfolding open_ereal_def
-  proof (intro conjI impI)
-    show "open (ereal -` \<Union>K)"
-      using *[THEN choice] by (auto simp: vimage_Union)
-  qed ((metis UnionE Union_upper subset_trans *)+)
-qed
-end
-
-lemma open_ereal: "open S \<Longrightarrow> open (ereal ` S)"
-  by (auto simp: inj_vimage_image_eq open_ereal_def)
-
-lemma open_ereal_vimage: "open S \<Longrightarrow> open (ereal -` S)"
-  unfolding open_ereal_def by auto
-
-lemma open_ereal_lessThan[intro, simp]: "open {..< a :: ereal}"
-proof -
-  have "\<And>x. ereal -` {..<ereal x} = {..< x}"
-    "ereal -` {..< \<infinity>} = UNIV" "ereal -` {..< -\<infinity>} = {}" by auto
-  then show ?thesis by (cases a) (auto simp: open_ereal_def)
-qed
-
-lemma open_ereal_greaterThan[intro, simp]:
-  "open {a :: ereal <..}"
-proof -
-  have "\<And>x. ereal -` {ereal x<..} = {x<..}"
-    "ereal -` {\<infinity><..} = {}" "ereal -` {-\<infinity><..} = UNIV" by auto
-  then show ?thesis by (cases a) (auto simp: open_ereal_def)
-qed
-
-lemma ereal_open_greaterThanLessThan[intro, simp]: "open {a::ereal <..< b}"
-  unfolding greaterThanLessThan_def by auto
-
-lemma closed_ereal_atLeast[simp, intro]: "closed {a :: ereal ..}"
-proof -
-  have "- {a ..} = {..< a}" by auto
-  then show "closed {a ..}"
-    unfolding closed_def using open_ereal_lessThan by auto
-qed
-
-lemma closed_ereal_atMost[simp, intro]: "closed {.. b :: ereal}"
-proof -
-  have "- {.. b} = {b <..}" by auto
-  then show "closed {.. b}"
-    unfolding closed_def using open_ereal_greaterThan by auto
-qed
-
-lemma closed_ereal_atLeastAtMost[simp, intro]:
-  shows "closed {a :: ereal .. b}"
-  unfolding atLeastAtMost_def by auto
-
-lemma closed_ereal_singleton:
-  "closed {a :: ereal}"
-by (metis atLeastAtMost_singleton closed_ereal_atLeastAtMost)
-
+lemmas open_ereal_lessThan = open_lessThan[where 'a=ereal]
+lemmas open_ereal_greaterThan = open_greaterThan[where 'a=ereal]
+lemmas ereal_open_greaterThanLessThan = open_greaterThanLessThan[where 'a=ereal]
+lemmas closed_ereal_atLeast = closed_atLeast[where 'a=ereal]
+lemmas closed_ereal_atMost = closed_atMost[where 'a=ereal]
+lemmas closed_ereal_atLeastAtMost = closed_atLeastAtMost[where 'a=ereal]
+lemmas closed_ereal_singleton = closed_singleton[where 'a=ereal]
+  
 lemma ereal_open_cont_interval:
   fixes S :: "ereal set"
   assumes "open S" "x \<in> S" "\<bar>x\<bar> \<noteq> \<infinity>"
@@ -1928,28 +1964,6 @@
   show thesis by auto
 qed
 
-instance ereal :: t2_space
-proof
-  fix x y :: ereal assume "x ~= y"
-  let "?P x (y::ereal)" = "EX U V. open U & open V & x : U & y : V & U Int V = {}"
-
-  { fix x y :: ereal assume "x < y"
-    from ereal_dense[OF this] obtain z where z: "x < z" "z < y" by auto
-    have "?P x y"
-      apply (rule exI[of _ "{..<z}"])
-      apply (rule exI[of _ "{z<..}"])
-      using z by auto }
-  note * = this
-
-  from `x ~= y`
-  show "EX U V. open U & open V & x : U & y : V & U Int V = {}"
-  proof (cases rule: linorder_cases)
-    assume "x = y" with `x ~= y` show ?thesis by simp
-  next assume "x < y" from *[OF this] show ?thesis by auto
-  next assume "y < x" from *[OF this] show ?thesis by auto
-  qed
-qed
-
 subsubsection {* Convergent sequences *}
 
 lemma lim_ereal[simp]:
@@ -1979,152 +1993,72 @@
     by (rule eventually_mono)
 qed
 
-lemma Lim_PInfty: "f ----> \<infinity> <-> (ALL B. EX N. ALL n>=N. f n >= ereal B)" (is "?l = ?r")
-proof
-  assume ?r
-  show ?l
-    apply(rule topological_tendstoI)
-    unfolding eventually_sequentially
-  proof-
-    fix S :: "ereal set" assume "open S" "\<infinity> : S"
-    from open_PInfty[OF this] guess B .. note B=this
-    from `?r`[rule_format,of "B+1"] guess N .. note N=this
-    show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
-    proof safe case goal1
-      have "ereal B < ereal (B + 1)" by auto
-      also have "... <= f n" using goal1 N by auto
-      finally show ?case using B by fastforce
-    qed
-  qed
+lemma tendsto_PInfty: "(f ---> \<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. ereal r < f x) F)"
+  unfolding tendsto_def
+proof safe
+  fix S :: "ereal set" assume "open S" "\<infinity> \<in> S"
+  from open_PInfty[OF this] guess B .. note B = this
+  moreover
+  assume "\<forall>r::real. eventually (\<lambda>z. r < f z) F"
+  then have "eventually (\<lambda>z. f z \<in> {B <..}) F" by auto
+  ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
 next
-  assume ?l
-  show ?r
-  proof fix B::real have "open {ereal B<..}" "\<infinity> : {ereal B<..}" by auto
-    from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
-    guess N .. note N=this
-    show "EX N. ALL n>=N. ereal B <= f n" apply(rule_tac x=N in exI) using N by auto
-  qed
+  fix x assume "\<forall>S. open S \<longrightarrow> \<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+  from this[rule_format, of "{ereal x <..}"]
+  show "eventually (\<lambda>y. ereal x < f y) F" by auto
 qed
 
-
-lemma Lim_MInfty: "f ----> (-\<infinity>) <-> (ALL B. EX N. ALL n>=N. f n <= ereal B)" (is "?l = ?r")
-proof
-  assume ?r
-  show ?l
-    apply(rule topological_tendstoI)
-    unfolding eventually_sequentially
-  proof-
-    fix S :: "ereal set"
-    assume "open S" "(-\<infinity>) : S"
-    from open_MInfty[OF this] guess B .. note B=this
-    from `?r`[rule_format,of "B-(1::real)"] guess N .. note N=this
-    show "EX N. ALL n>=N. f n : S" apply(rule_tac x=N in exI)
-    proof safe case goal1
-      have "ereal (B - 1) >= f n" using goal1 N by auto
-      also have "... < ereal B" by auto
-      finally show ?case using B by fastforce
-    qed
-  qed
-next assume ?l show ?r
-  proof fix B::real have "open {..<ereal B}" "(-\<infinity>) : {..<ereal B}" by auto
-    from topological_tendstoD[OF `?l` this,unfolded eventually_sequentially]
-    guess N .. note N=this
-    show "EX N. ALL n>=N. ereal B >= f n" apply(rule_tac x=N in exI) using N by auto
-  qed
+lemma tendsto_MInfty: "(f ---> -\<infinity>) F \<longleftrightarrow> (\<forall>r. eventually (\<lambda>x. f x < ereal r) F)"
+  unfolding tendsto_def
+proof safe
+  fix S :: "ereal set" assume "open S" "-\<infinity> \<in> S"
+  from open_MInfty[OF this] guess B .. note B = this
+  moreover
+  assume "\<forall>r::real. eventually (\<lambda>z. f z < r) F"
+  then have "eventually (\<lambda>z. f z \<in> {..< B}) F" by auto
+  ultimately show "eventually (\<lambda>z. f z \<in> S) F" by (auto elim!: eventually_elim1)
+next
+  fix x assume "\<forall>S. open S \<longrightarrow> -\<infinity> \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F"
+  from this[rule_format, of "{..< ereal x}"]
+  show "eventually (\<lambda>y. f y < ereal x) F" by auto
 qed
 
-
-lemma Lim_bounded_PInfty: assumes lim:"f ----> l" and "!!n. f n <= ereal B" shows "l ~= \<infinity>"
-proof(rule ccontr,unfold not_not) let ?B = "B + 1" assume as:"l=\<infinity>"
-  from lim[unfolded this Lim_PInfty,rule_format,of "?B"]
-  guess N .. note N=this[rule_format,OF le_refl]
-  hence "ereal ?B <= ereal B" using assms(2)[of N] by(rule order_trans)
-  hence "ereal ?B < ereal ?B" apply (rule le_less_trans) by auto
-  thus False by auto
-qed
+lemma Lim_PInfty: "f ----> \<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. f n \<ge> ereal B)"
+  unfolding tendsto_PInfty eventually_sequentially
+proof safe
+  fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. ereal r \<le> f n"
+  from this[rule_format, of "r+1"] guess N ..
+  moreover have "ereal r < ereal (r + 1)" by auto
+  ultimately show "\<exists>N. \<forall>n\<ge>N. ereal r < f n"
+    by (blast intro: less_le_trans)
+qed (blast intro: less_imp_le)
 
+lemma Lim_MInfty: "f ----> -\<infinity> \<longleftrightarrow> (\<forall>B. \<exists>N. \<forall>n\<ge>N. ereal B \<ge> f n)"
+  unfolding tendsto_MInfty eventually_sequentially
+proof safe
+  fix r assume "\<forall>r. \<exists>N. \<forall>n\<ge>N. f n \<le> ereal r"
+  from this[rule_format, of "r - 1"] guess N ..
+  moreover have "ereal (r - 1) < ereal r" by auto
+  ultimately show "\<exists>N. \<forall>n\<ge>N. f n < ereal r"
+    by (blast intro: le_less_trans)
+qed (blast intro: less_imp_le)
 
-lemma Lim_bounded_MInfty: assumes lim:"f ----> l" and "!!n. f n >= ereal B" shows "l ~= (-\<infinity>)"
-proof(rule ccontr,unfold not_not) let ?B = "B - 1" assume as:"l=(-\<infinity>)"
-  from lim[unfolded this Lim_MInfty,rule_format,of "?B"]
-  guess N .. note N=this[rule_format,OF le_refl]
-  hence "ereal B <= ereal ?B" using assms(2)[of N] order_trans[of "ereal B" "f N" "ereal(B - 1)"] by blast
-  thus False by auto
-qed
+lemma Lim_bounded_PInfty: "f ----> l \<Longrightarrow> (\<And>n. f n \<le> ereal B) \<Longrightarrow> l \<noteq> \<infinity>"
+  using LIMSEQ_le_const2[of f l "ereal B"] by auto
 
+lemma Lim_bounded_MInfty: "f ----> l \<Longrightarrow> (\<And>n. ereal B \<le> f n) \<Longrightarrow> l \<noteq> -\<infinity>"
+  using LIMSEQ_le_const[of f l "ereal B"] by auto
 
 lemma tendsto_explicit:
   "f ----> f0 <-> (ALL S. open S --> f0 : S --> (EX N. ALL n>=N. f n : S))"
   unfolding tendsto_def eventually_sequentially by auto
 
-
-lemma tendsto_obtains_N:
-  assumes "f ----> f0"
-  assumes "open S" "f0 : S"
-  obtains N where "ALL n>=N. f n : S"
-  using tendsto_explicit[of f f0] assms by auto
-
-
-lemma tail_same_limit:
-  fixes X Y N
-  assumes "X ----> L" "ALL n>=N. X n = Y n"
-  shows "Y ----> L"
-proof-
-{ fix S assume "open S" and "L:S"
-  then obtain N1 where "ALL n>=N1. X n : S"
-     using assms unfolding tendsto_def eventually_sequentially by auto
-  hence "ALL n>=max N N1. Y n : S" using assms by auto
-  hence "EX N. ALL n>=N. Y n : S" apply(rule_tac x="max N N1" in exI) by auto
-}
-thus ?thesis using tendsto_explicit by auto
-qed
-
-
 lemma Lim_bounded_PInfty2:
-assumes lim:"f ----> l" and "ALL n>=N. f n <= ereal B"
-shows "l ~= \<infinity>"
-proof-
-  def g == "(%n. if n>=N then f n else ereal B)"
-  hence "g ----> l" using tail_same_limit[of f l N g] lim by auto
-  moreover have "!!n. g n <= ereal B" using g_def assms by auto
-  ultimately show ?thesis using  Lim_bounded_PInfty by auto
-qed
+  "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
+  using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
 
-lemma Lim_bounded_ereal:
-  assumes lim:"f ----> (l :: ereal)"
-  and "ALL n>=M. f n <= C"
-  shows "l<=C"
-proof-
-{ assume "l=(-\<infinity>)" hence ?thesis by auto }
-moreover
-{ assume "~(l=(-\<infinity>))"
-  { assume "C=\<infinity>" hence ?thesis by auto }
-  moreover
-  { assume "C=(-\<infinity>)" hence "ALL n>=M. f n = (-\<infinity>)" using assms by auto
-    hence "l=(-\<infinity>)" using assms
-       tendsto_unique[OF trivial_limit_sequentially] tail_same_limit[of "\<lambda>n. -\<infinity>" "-\<infinity>" M f, OF tendsto_const] by auto
-    hence ?thesis by auto }
-  moreover
-  { assume "EX B. C = ereal B"
-    then obtain B where B_def: "C=ereal B" by auto
-    hence "~(l=\<infinity>)" using Lim_bounded_PInfty2 assms by auto
-    then obtain m where m_def: "ereal m=l" using `~(l=(-\<infinity>))` by (cases l) auto
-    then obtain N where N_def: "ALL n>=N. f n : {ereal(m - 1) <..< ereal(m+1)}"
-       apply (subst tendsto_obtains_N[of f l "{ereal(m - 1) <..< ereal(m+1)}"]) using assms by auto
-    { fix n assume "n>=N"
-      hence "EX r. ereal r = f n" using N_def by (cases "f n") auto
-    } then obtain g where g_def: "ALL n>=N. ereal (g n) = f n" by metis
-    hence "(%n. ereal (g n)) ----> l" using tail_same_limit[of f l N] assms by auto
-    hence *: "(%n. g n) ----> m" using m_def by auto
-    { fix n assume "n>=max N M"
-      hence "ereal (g n) <= ereal B" using assms g_def B_def by auto
-      hence "g n <= B" by auto
-    } hence "EX N. ALL n>=N. g n <= B" by blast
-    hence "m<=B" using * LIMSEQ_le_const2[of g m B] by auto
-    hence ?thesis using m_def B_def by auto
-  } ultimately have ?thesis by (cases C) auto
-} ultimately show ?thesis by blast
-qed
+lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
+  by (intro LIMSEQ_le_const2) auto
 
 lemma real_of_ereal_mult[simp]:
   fixes a b :: ereal shows "real (a * b) = real a * real b"
@@ -2204,349 +2138,6 @@
 lemma ereal_mult_m1[simp]: "x * ereal (-1) = -x"
   by (cases x) auto
 
-lemma ereal_LimI_finite:
-  fixes x :: ereal
-  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
-  assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
-  shows "u ----> x"
-proof (rule topological_tendstoI, unfold eventually_sequentially)
-  obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
-  fix S assume "open S" "x : S"
-  then have "open (ereal -` S)" unfolding open_ereal_def by auto
-  with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
-    unfolding open_real_def rx_def by auto
-  then obtain n where
-    upper: "!!N. n <= N ==> u N < x + ereal r" and
-    lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
-  show "EX N. ALL n>=N. u n : S"
-  proof (safe intro!: exI[of _ n])
-    fix N assume "n <= N"
-    from upper[OF this] lower[OF this] assms `0 < r`
-    have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
-    then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
-    hence "rx < ra + r" and "ra < rx + r"
-       using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
-    hence "dist (real (u N)) rx < r"
-      using rx_def ra_def
-      by (auto simp: dist_real_def abs_diff_less_iff field_simps)
-    from dist[OF this] show "u N : S" using `u N  ~: {\<infinity>, -\<infinity>}`
-      by (auto simp: ereal_real split: split_if_asm)
-  qed
-qed
-
-lemma ereal_LimI_finite_iff:
-  fixes x :: ereal
-  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
-  shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
-  (is "?lhs <-> ?rhs")
-proof
-  assume lim: "u ----> x"
-  { fix r assume "(r::ereal)>0"
-    then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
-       apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
-       using lim ereal_between[of x r] assms `r>0` by auto
-    hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
-      using ereal_minus_less[of r x] by (cases r) auto
-  } then show "?rhs" by auto
-next
-  assume ?rhs then show "u ----> x"
-    using ereal_LimI_finite[of x] assms by auto
-qed
-
-
-subsubsection {* @{text Liminf} and @{text Limsup} *}
-
-definition
-  "Liminf net f = (GREATEST l. \<forall>y<l. eventually (\<lambda>x. y < f x) net)"
-
-definition
-  "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
-
-lemma Liminf_Sup:
-  fixes f :: "'a => 'b::complete_linorder"
-  shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
-  by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
-
-lemma Limsup_Inf:
-  fixes f :: "'a => 'b::complete_linorder"
-  shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
-  by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
-
-lemma ereal_SupI:
-  fixes x :: ereal
-  assumes "\<And>y. y \<in> A \<Longrightarrow> y \<le> x"
-  assumes "\<And>y. (\<And>z. z \<in> A \<Longrightarrow> z \<le> y) \<Longrightarrow> x \<le> y"
-  shows "Sup A = x"
-  unfolding Sup_ereal_def
-  using assms by (auto intro!: Least_equality)
-
-lemma ereal_InfI:
-  fixes x :: ereal
-  assumes "\<And>i. i \<in> A \<Longrightarrow> x \<le> i"
-  assumes "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> i) \<Longrightarrow> y \<le> x"
-  shows "Inf A = x"
-  unfolding Inf_ereal_def
-  using assms by (auto intro!: Greatest_equality)
-
-lemma Limsup_const:
-  fixes c :: "'a::complete_linorder"
-  assumes ntriv: "\<not> trivial_limit net"
-  shows "Limsup net (\<lambda>x. c) = c"
-  unfolding Limsup_Inf
-proof (safe intro!: antisym complete_lattice_class.Inf_greatest complete_lattice_class.Inf_lower)
-  fix x assume *: "\<forall>y>x. eventually (\<lambda>_. c < y) net"
-  show "c \<le> x"
-  proof (rule ccontr)
-    assume "\<not> c \<le> x" then have "x < c" by auto
-    then show False using ntriv * by (auto simp: trivial_limit_def)
-  qed
-qed auto
-
-lemma Liminf_const:
-  fixes c :: "'a::complete_linorder"
-  assumes ntriv: "\<not> trivial_limit net"
-  shows "Liminf net (\<lambda>x. c) = c"
-  unfolding Liminf_Sup
-proof (safe intro!: antisym complete_lattice_class.Sup_least complete_lattice_class.Sup_upper)
-  fix x assume *: "\<forall>y<x. eventually (\<lambda>_. y < c) net"
-  show "x \<le> c"
-  proof (rule ccontr)
-    assume "\<not> x \<le> c" then have "c < x" by auto
-    then show False using ntriv * by (auto simp: trivial_limit_def)
-  qed
-qed auto
-
-definition (in order) mono_set:
-  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
-
-lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
-lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
-lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
-lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
-
-lemma (in complete_linorder) mono_set_iff:
-  fixes S :: "'a set"
-  defines "a \<equiv> Inf S"
-  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
-proof
-  assume "mono_set S"
-  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
-  show ?c
-  proof cases
-    assume "a \<in> S"
-    show ?c
-      using mono[OF _ `a \<in> S`]
-      by (auto intro: Inf_lower simp: a_def)
-  next
-    assume "a \<notin> S"
-    have "S = {a <..}"
-    proof safe
-      fix x assume "x \<in> S"
-      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
-      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
-    next
-      fix x assume "a < x"
-      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
-      with mono[of y x] show "x \<in> S" by auto
-    qed
-    then show ?c ..
-  qed
-qed auto
-
-lemma lim_imp_Liminf:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes ntriv: "\<not> trivial_limit net"
-  assumes lim: "(f ---> f0) net"
-  shows "Liminf net f = f0"
-  unfolding Liminf_Sup
-proof (safe intro!: ereal_SupI)
-  fix y assume *: "\<forall>y'<y. eventually (\<lambda>x. y' < f x) net"
-  show "y \<le> f0"
-  proof (rule ereal_le_ereal)
-    fix B assume "B < y"
-    { assume "f0 < B"
-      then have "eventually (\<lambda>x. f x < B \<and> B < f x) net"
-         using topological_tendstoD[OF lim, of "{..<B}"] *[rule_format, OF `B < y`]
-         by (auto intro: eventually_conj)
-      also have "(\<lambda>x. f x < B \<and> B < f x) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
-      finally have False using ntriv[unfolded trivial_limit_def] by auto
-    } then show "B \<le> f0" by (metis linorder_le_less_linear)
-  qed
-next
-  fix y assume *: "\<forall>z. z \<in> {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net} \<longrightarrow> z \<le> y"
-  show "f0 \<le> y"
-  proof (safe intro!: *[rule_format])
-    fix y assume "y < f0" then show "eventually (\<lambda>x. y < f x) net"
-      using lim[THEN topological_tendstoD, of "{y <..}"] by auto
-  qed
-qed
-
-lemma ereal_Liminf_le_Limsup:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes ntriv: "\<not> trivial_limit net"
-  shows "Liminf net f \<le> Limsup net f"
-  unfolding Limsup_Inf Liminf_Sup
-proof (safe intro!: complete_lattice_class.Inf_greatest  complete_lattice_class.Sup_least)
-  fix u v assume *: "\<forall>y<u. eventually (\<lambda>x. y < f x) net" "\<forall>y>v. eventually (\<lambda>x. f x < y) net"
-  show "u \<le> v"
-  proof (rule ccontr)
-    assume "\<not> u \<le> v"
-    then obtain t where "t < u" "v < t"
-      using ereal_dense[of v u] by (auto simp: not_le)
-    then have "eventually (\<lambda>x. t < f x \<and> f x < t) net"
-      using * by (auto intro: eventually_conj)
-    also have "(\<lambda>x. t < f x \<and> f x < t) = (\<lambda>x. False)" by (auto simp: fun_eq_iff)
-    finally show False using ntriv by (auto simp: trivial_limit_def)
-  qed
-qed
-
-lemma Liminf_mono:
-  fixes f g :: "'a => ereal"
-  assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
-  shows "Liminf net f \<le> Liminf net g"
-  unfolding Liminf_Sup
-proof (safe intro!: Sup_mono bexI)
-  fix a y assume "\<forall>y<a. eventually (\<lambda>x. y < f x) net" and "y < a"
-  then have "eventually (\<lambda>x. y < f x) net" by auto
-  then show "eventually (\<lambda>x. y < g x) net"
-    by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
-qed simp
-
-lemma Liminf_eq:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "eventually (\<lambda>x. f x = g x) net"
-  shows "Liminf net f = Liminf net g"
-  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
-
-lemma Liminf_mono_all:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "\<And>x. f x \<le> g x"
-  shows "Liminf net f \<le> Liminf net g"
-  using assms by (intro Liminf_mono always_eventually) auto
-
-lemma Limsup_mono:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes ev: "eventually (\<lambda>x. f x \<le> g x) net"
-  shows "Limsup net f \<le> Limsup net g"
-  unfolding Limsup_Inf
-proof (safe intro!: Inf_mono bexI)
-  fix a y assume "\<forall>y>a. eventually (\<lambda>x. g x < y) net" and "a < y"
-  then have "eventually (\<lambda>x. g x < y) net" by auto
-  then show "eventually (\<lambda>x. f x < y) net"
-    by (rule eventually_rev_mp) (rule eventually_mono[OF _ ev], auto)
-qed simp
-
-lemma Limsup_mono_all:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "\<And>x. f x \<le> g x"
-  shows "Limsup net f \<le> Limsup net g"
-  using assms by (intro Limsup_mono always_eventually) auto
-
-lemma Limsup_eq:
-  fixes f g :: "'a \<Rightarrow> ereal"
-  assumes "eventually (\<lambda>x. f x = g x) net"
-  shows "Limsup net f = Limsup net g"
-  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
-
-abbreviation "liminf \<equiv> Liminf sequentially"
-
-abbreviation "limsup \<equiv> Limsup sequentially"
-
-lemma liminf_SUPR_INFI:
-  fixes f :: "nat \<Rightarrow> ereal"
-  shows "liminf f = (SUP n. INF m:{n..}. f m)"
-  unfolding Liminf_Sup eventually_sequentially
-proof (safe intro!: antisym complete_lattice_class.Sup_least)
-  fix x assume *: "\<forall>y<x. \<exists>N. \<forall>n\<ge>N. y < f n" show "x \<le> (SUP n. INF m:{n..}. f m)"
-  proof (rule ereal_le_ereal)
-    fix y assume "y < x"
-    with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
-    then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
-    also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro SUP_upper) auto
-    finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
-  qed
-next
-  show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
-  proof (unfold SUP_def, safe intro!: Sup_mono bexI)
-    fix y n assume "y < INFI {n..} f"
-    from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
-  qed (rule order_refl)
-qed
-
-lemma tail_same_limsup:
-  fixes X Y :: "nat => ereal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
-  shows "limsup X = limsup Y"
-  using Limsup_eq[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma tail_same_liminf:
-  fixes X Y :: "nat => ereal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n = Y n"
-  shows "liminf X = liminf Y"
-  using Liminf_eq[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma liminf_mono:
-  fixes X Y :: "nat \<Rightarrow> ereal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
-  shows "liminf X \<le> liminf Y"
-  using Liminf_mono[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma limsup_mono:
-  fixes X Y :: "nat => ereal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
-  shows "limsup X \<le> limsup Y"
-  using Limsup_mono[of X Y sequentially] eventually_sequentially assms by auto
-
-lemma
-  fixes X :: "nat \<Rightarrow> ereal"
-  shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
-    and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
-  unfolding incseq_def decseq_def by auto
-
-lemma liminf_bounded:
-  fixes X Y :: "nat \<Rightarrow> ereal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> C \<le> X n"
-  shows "C \<le> liminf X"
-  using liminf_mono[of N "\<lambda>n. C" X] assms Liminf_const[of sequentially C] by simp
-
-lemma limsup_bounded:
-  fixes X Y :: "nat => ereal"
-  assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= C"
-  shows "limsup X \<le> C"
-  using limsup_mono[of N X "\<lambda>n. C"] assms Limsup_const[of sequentially C] by simp
-
-lemma liminf_bounded_iff:
-  fixes x :: "nat \<Rightarrow> ereal"
-  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
-proof safe
-  fix B assume "B < C" "C \<le> liminf x"
-  then have "B < liminf x" by auto
-  then obtain N where "B < (INF m:{N..}. x m)"
-    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
-  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
-next
-  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
-  { fix B assume "B<C"
-    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
-    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
-    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
-    finally have "B \<le> liminf x" .
-  } then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
-qed
-
-lemma liminf_subseq_mono:
-  fixes X :: "nat \<Rightarrow> ereal"
-  assumes "subseq r"
-  shows "liminf X \<le> liminf (X \<circ> r) "
-proof-
-  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
-  proof (safe intro!: INF_mono)
-    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
-      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
-  qed
-  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
-qed
-
 lemma ereal_real': assumes "\<bar>x\<bar> \<noteq> \<infinity>" shows "ereal (real x) = x"
   using assms by auto
 
@@ -2618,6 +2209,333 @@
   "[| (a::ereal) <= x; c <= x |] ==> max a c <= x"
   by (metis sup_ereal_def sup_least)
 
+
+lemma ereal_LimI_finite:
+  fixes x :: ereal
+  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+  assumes "!!r. 0 < r ==> EX N. ALL n>=N. u n < x + r & x < u n + r"
+  shows "u ----> x"
+proof (rule topological_tendstoI, unfold eventually_sequentially)
+  obtain rx where rx_def: "x=ereal rx" using assms by (cases x) auto
+  fix S assume "open S" "x : S"
+  then have "open (ereal -` S)" unfolding open_ereal_def by auto
+  with `x \<in> S` obtain r where "0 < r" and dist: "!!y. dist y rx < r ==> ereal y \<in> S"
+    unfolding open_real_def rx_def by auto
+  then obtain n where
+    upper: "!!N. n <= N ==> u N < x + ereal r" and
+    lower: "!!N. n <= N ==> x < u N + ereal r" using assms(2)[of "ereal r"] by auto
+  show "EX N. ALL n>=N. u n : S"
+  proof (safe intro!: exI[of _ n])
+    fix N assume "n <= N"
+    from upper[OF this] lower[OF this] assms `0 < r`
+    have "u N ~: {\<infinity>,(-\<infinity>)}" by auto
+    then obtain ra where ra_def: "(u N) = ereal ra" by (cases "u N") auto
+    hence "rx < ra + r" and "ra < rx + r"
+       using rx_def assms `0 < r` lower[OF `n <= N`] upper[OF `n <= N`] by auto
+    hence "dist (real (u N)) rx < r"
+      using rx_def ra_def
+      by (auto simp: dist_real_def abs_diff_less_iff field_simps)
+    from dist[OF this] show "u N : S" using `u N  ~: {\<infinity>, -\<infinity>}`
+      by (auto simp: ereal_real split: split_if_asm)
+  qed
+qed
+
+lemma tendsto_obtains_N:
+  assumes "f ----> f0"
+  assumes "open S" "f0 : S"
+  obtains N where "ALL n>=N. f n : S"
+  using tendsto_explicit[of f f0] assms by auto
+
+lemma ereal_LimI_finite_iff:
+  fixes x :: ereal
+  assumes "\<bar>x\<bar> \<noteq> \<infinity>"
+  shows "u ----> x <-> (ALL r. 0 < r --> (EX N. ALL n>=N. u n < x + r & x < u n + r))"
+  (is "?lhs <-> ?rhs")
+proof
+  assume lim: "u ----> x"
+  { fix r assume "(r::ereal)>0"
+    then obtain N where N_def: "ALL n>=N. u n : {x - r <..< x + r}"
+       apply (subst tendsto_obtains_N[of u x "{x - r <..< x + r}"])
+       using lim ereal_between[of x r] assms `r>0` by auto
+    hence "EX N. ALL n>=N. u n < x + r & x < u n + r"
+      using ereal_minus_less[of r x] by (cases r) auto
+  } then show "?rhs" by auto
+next
+  assume ?rhs then show "u ----> x"
+    using ereal_LimI_finite[of x] assms by auto
+qed
+
+
+subsubsection {* @{text Liminf} and @{text Limsup} *}
+
+definition
+  "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
+
+definition
+  "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
+
+abbreviation "liminf \<equiv> Liminf sequentially"
+
+abbreviation "limsup \<equiv> Limsup sequentially"
+
+lemma Liminf_eqI:
+  "(\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> x) \<Longrightarrow>  
+    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y) \<Longrightarrow> x \<le> y) \<Longrightarrow> Liminf F f = x"
+  unfolding Liminf_def by (auto intro!: SUP_eqI)
+
+lemma Limsup_eqI:
+  "(\<And>P. eventually P F \<Longrightarrow> x \<le> SUPR (Collect P) f) \<Longrightarrow>  
+    (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
+  unfolding Limsup_def by (auto intro!: INF_eqI)
+
+lemma liminf_SUPR_INFI:
+  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+  shows "liminf f = (SUP n. INF m:{n..}. f m)"
+  unfolding Liminf_def eventually_sequentially
+  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
+
+lemma limsup_INFI_SUPR:
+  fixes f :: "nat \<Rightarrow> 'a :: complete_lattice"
+  shows "limsup f = (INF n. SUP m:{n..}. f m)"
+  unfolding Limsup_def eventually_sequentially
+  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
+
+lemma Limsup_const: 
+  assumes ntriv: "\<not> trivial_limit F"
+  shows "Limsup F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+  have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
+    using ntriv by (intro SUP_const) (auto simp: eventually_False *)
+  then show ?thesis
+    unfolding Limsup_def using eventually_True
+    by (subst INF_cong[where D="\<lambda>x. c"])
+       (auto intro!: INF_const simp del: eventually_True)
+qed
+
+lemma Liminf_const:
+  assumes ntriv: "\<not> trivial_limit F"
+  shows "Liminf F (\<lambda>x. c) = (c::'a::complete_lattice)"
+proof -
+  have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
+  have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
+    using ntriv by (intro INF_const) (auto simp: eventually_False *)
+  then show ?thesis
+    unfolding Liminf_def using eventually_True
+    by (subst SUP_cong[where D="\<lambda>x. c"])
+       (auto intro!: SUP_const simp del: eventually_True)
+qed
+
+lemma Liminf_mono:
+  fixes f g :: "'a => 'b :: complete_lattice"
+  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+  shows "Liminf F f \<le> Liminf F g"
+  unfolding Liminf_def
+proof (safe intro!: SUP_mono)
+  fix P assume "eventually P F"
+  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
+  then show "\<exists>Q\<in>{P. eventually P F}. INFI (Collect P) f \<le> INFI (Collect Q) g"
+    by (intro bexI[of _ ?Q]) (auto intro!: INF_mono)
+qed
+
+lemma Liminf_eq:
+  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+  assumes "eventually (\<lambda>x. f x = g x) F"
+  shows "Liminf F f = Liminf F g"
+  by (intro antisym Liminf_mono eventually_mono[OF _ assms]) auto
+
+lemma Limsup_mono:
+  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+  assumes ev: "eventually (\<lambda>x. f x \<le> g x) F"
+  shows "Limsup F f \<le> Limsup F g"
+  unfolding Limsup_def
+proof (safe intro!: INF_mono)
+  fix P assume "eventually P F"
+  with ev have "eventually (\<lambda>x. f x \<le> g x \<and> P x) F" (is "eventually ?Q F") by (rule eventually_conj)
+  then show "\<exists>Q\<in>{P. eventually P F}. SUPR (Collect Q) f \<le> SUPR (Collect P) g"
+    by (intro bexI[of _ ?Q]) (auto intro!: SUP_mono)
+qed
+
+lemma Limsup_eq:
+  fixes f g :: "'a \<Rightarrow> 'b :: complete_lattice"
+  assumes "eventually (\<lambda>x. f x = g x) net"
+  shows "Limsup net f = Limsup net g"
+  by (intro antisym Limsup_mono eventually_mono[OF _ assms]) auto
+
+lemma Liminf_le_Limsup:
+  fixes f :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes ntriv: "\<not> trivial_limit F"
+  shows "Liminf F f \<le> Limsup F f"
+  unfolding Limsup_def Liminf_def
+  apply (rule complete_lattice_class.SUP_least)
+  apply (rule complete_lattice_class.INF_greatest)
+proof safe
+  fix P Q assume "eventually P F" "eventually Q F"
+  then have "eventually (\<lambda>x. P x \<and> Q x) F" (is "eventually ?C F") by (rule eventually_conj)
+  then have not_False: "(\<lambda>x. P x \<and> Q x) \<noteq> (\<lambda>x. False)"
+    using ntriv by (auto simp add: eventually_False)
+  have "INFI (Collect P) f \<le> INFI (Collect ?C) f"
+    by (rule INF_mono) auto
+  also have "\<dots> \<le> SUPR (Collect ?C) f"
+    using not_False by (intro INF_le_SUP) auto
+  also have "\<dots> \<le> SUPR (Collect Q) f"
+    by (rule SUP_mono) auto
+  finally show "INFI (Collect P) f \<le> SUPR (Collect Q) f" .
+qed
+
+lemma
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows ereal_incseq_uminus[simp]: "incseq (\<lambda>i. - X i) = decseq X"
+    and ereal_decseq_uminus[simp]: "decseq (\<lambda>i. - X i) = incseq X"
+  unfolding incseq_def decseq_def by auto
+
+lemma Liminf_bounded:
+  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes le: "eventually (\<lambda>n. C \<le> X n) F"
+  shows "C \<le> Liminf F X"
+  using Liminf_mono[OF le] Liminf_const[OF ntriv, of C] by simp
+
+lemma Limsup_bounded:
+  fixes X Y :: "'a \<Rightarrow> 'b::complete_lattice"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes le: "eventually (\<lambda>n. X n \<le> C) F"
+  shows "Limsup F X \<le> C"
+  using Limsup_mono[OF le] Limsup_const[OF ntriv, of C] by simp
+
+lemma liminf_bounded_iff:
+  fixes x :: "nat \<Rightarrow> ereal"
+  shows "C \<le> liminf x \<longleftrightarrow> (\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n)" (is "?lhs <-> ?rhs")
+proof safe
+  fix B assume "B < C" "C \<le> liminf x"
+  then have "B < liminf x" by auto
+  then obtain N where "B < (INF m:{N..}. x m)"
+    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
+  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
+next
+  assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
+  { fix B assume "B<C"
+    then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
+    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
+    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
+    finally have "B \<le> liminf x" .
+  } then show "?lhs"
+    by (metis * leD Liminf_bounded[OF sequentially_bot] linorder_le_less_linear eventually_sequentially)
+qed
+
+lemma liminf_subseq_mono:
+  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+  assumes "subseq r"
+  shows "liminf X \<le> liminf (X \<circ> r) "
+proof-
+  have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
+  proof (safe intro!: INF_mono)
+    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
+      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+  qed
+  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
+qed
+
+lemma limsup_subseq_mono:
+  fixes X :: "nat \<Rightarrow> 'a :: complete_linorder"
+  assumes "subseq r"
+  shows "limsup (X \<circ> r) \<le> limsup X"
+proof-
+  have "\<And>n. (SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)"
+  proof (safe intro!: SUP_mono)
+    fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
+      using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
+  qed
+  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
+qed
+
+lemma lim_imp_Liminf:
+  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Liminf F f = f0"
+proof (rule Liminf_eqI)
+  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+  show "f0 \<le> y"
+  proof (rule ereal_le_ereal)
+    fix B
+    assume "B < f0"
+    have "B \<le> INFI {x. B < f x} f"
+      by (rule INF_greatest) simp
+    also have "INFI {x. B < f x} f \<le> y"
+      using lim[THEN topological_tendstoD, of "{B <..}"] `B < f0` * by auto
+    finally show "B \<le> y" .
+  qed
+next
+  fix P assume P: "eventually P F"
+  then have "eventually (\<lambda>x. INFI (Collect P) f \<le> f x) F"
+    by eventually_elim (auto intro!: INF_lower)
+  then show "INFI (Collect P) f \<le> f0"
+    by (rule tendsto_le[OF ntriv lim tendsto_const])
+qed
+
+lemma lim_imp_Limsup:
+  fixes f :: "'a \<Rightarrow> ereal" (* generalize to inner dense, complete_linorder, order_topology *)
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Limsup F f = f0"
+proof (rule Limsup_eqI)
+  fix y assume *: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+  show "y \<le> f0"
+  proof (rule ereal_ge_ereal, safe)
+    fix B
+    assume "f0 < B"
+    have "y \<le> SUPR {x. f x < B} f"
+      using lim[THEN topological_tendstoD, of "{..< B}"] `f0 < B` * by auto
+    also have "SUPR {x. f x < B} f \<le> B"
+      by (rule SUP_least) simp
+    finally show "y \<le> B" .
+  qed
+next
+  fix P assume P: "eventually P F"
+  then have "eventually (\<lambda>x. f x \<le> SUPR (Collect P) f) F"
+    by eventually_elim (auto intro!: SUP_upper)
+  then show "f0 \<le> SUPR (Collect P) f"
+    by (rule tendsto_le[OF ntriv tendsto_const lim])
+qed
+
+definition (in order) mono_set:
+  "mono_set S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
+
+lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
+lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
+lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
+lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto
+
+lemma (in complete_linorder) mono_set_iff:
+  fixes S :: "'a set"
+  defines "a \<equiv> Inf S"
+  shows "mono_set S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
+proof
+  assume "mono_set S"
+  then have mono: "\<And>x y. x \<le> y \<Longrightarrow> x \<in> S \<Longrightarrow> y \<in> S" by (auto simp: mono_set)
+  show ?c
+  proof cases
+    assume "a \<in> S"
+    show ?c
+      using mono[OF _ `a \<in> S`]
+      by (auto intro: Inf_lower simp: a_def)
+  next
+    assume "a \<notin> S"
+    have "S = {a <..}"
+    proof safe
+      fix x assume "x \<in> S"
+      then have "a \<le> x" unfolding a_def by (rule Inf_lower)
+      then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
+    next
+      fix x assume "a < x"
+      then obtain y where "y < x" "y \<in> S" unfolding a_def Inf_less_iff ..
+      with mono[of y x] show "x \<in> S" by auto
+    qed
+    then show ?c ..
+  qed
+qed auto
+
 subsubsection {* Tests for code generator *}
 
 (* A small list of simple arithmetic expressions *)

--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -288,16 +288,9 @@
   assumes lim:"f ----> (l :: ereal)"
     and ge: "ALL n>=N. f n >= C"
   shows "l>=C"
-proof -
-  def g == "(%i. -(f i))"
-  { fix n
-    assume "n>=N"
-    then have "g n <= -C" using assms ereal_minus_le_minus g_def by auto }
-  then have "ALL n>=N. g n <= -C" by auto
-  moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto
-  ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto
-  then show ?thesis using ereal_minus_le_minus by auto
-qed
+  using ge
+  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+     (auto simp: eventually_sequentially)
 
 lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
 proof
@@ -326,54 +319,69 @@
   fixes f :: "'a => ereal"
   shows "Liminf net f =
     Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
-  unfolding Liminf_Sup
-proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
-  fix l S
-  assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
-  then have "S = UNIV \<or> S = {Inf S <..}"
-    using ereal_open_mono_set[of S] by auto
-  then show "eventually (\<lambda>x. f x \<in> S) net"
-  proof
-    assume S: "S = {Inf S<..}"
-    then have "Inf S < l" using `l \<in> S` by auto
-    then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
-    then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
-  qed auto
+    (is "_ = Sup ?A")
+proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
+  fix P assume P: "eventually P net"
+  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
+  { fix x assume "P x"
+    then have "INFI (Collect P) f \<le> f x"
+      by (intro complete_lattice_class.INF_lower) simp
+    with S have "f x \<in> S"
+      by (simp add: mono_set) }
+  with P show "eventually (\<lambda>x. f x \<in> S) net"
+    by (auto elim: eventually_elim1)
 next
-  fix l y
-  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
-  have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
-    using `y < l` by (intro S[rule_format]) auto
-  then show "eventually (\<lambda>x. y < f x) net" by auto
+  fix y l
+  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
+  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
+  show "l \<le> y"
+  proof (rule ereal_le_ereal)
+    fix B assume "B < l"
+    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
+      by (intro S[rule_format]) auto
+    then have "INFI {x. B < f x} f \<le> y"
+      using P by auto
+    moreover have "B \<le> INFI {x. B < f x} f"
+      by (intro INF_greatest) auto
+    ultimately show "B \<le> y"
+      by simp
+  qed
 qed
 
 lemma ereal_Limsup_Inf_monoset:
   fixes f :: "'a => ereal"
   shows "Limsup net f =
     Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
-  unfolding Limsup_Inf
-proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
-  fix l S
-  assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
-  then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
-  then have "S = UNIV \<or> S = {..< Sup S}"
-    unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
-  then show "eventually (\<lambda>x. f x \<in> S) net"
-  proof
-    assume S: "S = {..< Sup S}"
-    then have "l < Sup S" using `l \<in> S` by auto
-    then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
-    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
-  qed auto
+    (is "_ = Inf ?A")
+proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
+  fix P assume P: "eventually P net"
+  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
+  { fix x assume "P x"
+    then have "f x \<le> SUPR (Collect P) f"
+      by (intro complete_lattice_class.SUP_upper) simp
+    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
+    have "f x \<in> S"
+      by (simp add: inj_image_mem_iff) }
+  with P show "eventually (\<lambda>x. f x \<in> S) net"
+    by (auto elim: eventually_elim1)
 next
-  fix l y
-  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
-  have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
-    using `l < y` by (intro S[rule_format]) auto
-  then show "eventually (\<lambda>x. f x < y) net" by auto
+  fix y l
+  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
+  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
+  show "y \<le> l"
+  proof (rule ereal_ge_ereal, safe)
+    fix B assume "l < B"
+    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
+      by (intro S[rule_format]) auto
+    then have "y \<le> SUPR {x. f x < B} f"
+      using P by auto
+    moreover have "SUPR {x. f x < B} f \<le> B"
+      by (intro SUP_least) auto
+    ultimately show "y \<le> B"
+      by simp
+  qed
 qed
 
-
 lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
   using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
 
@@ -434,21 +442,16 @@
   shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
 proof (intro lim_imp_Liminf iffI assms)
   assume rhs: "Liminf net f = \<infinity>"
-  { fix S :: "ereal set"
-    assume "open S & \<infinity> : S"
-    then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
-    moreover
-    have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
-      using rhs
-      unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
-      by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)
-    ultimately
-    have "eventually (%x. f x : S) net"
-      apply (subst eventually_mono)
-      apply auto
-      done
-  }
-  then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
+  show "(f ---> \<infinity>) net"
+    unfolding tendsto_PInfty
+  proof
+    fix r :: real
+    have "ereal r < top" unfolding top_ereal_def by simp
+    with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
+      unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
+    then show "eventually (\<lambda>x. ereal r < f x) net"
+      by (auto elim!: eventually_elim1 dest: less_INF_D)
+  qed
 qed
 
 lemma Limsup_MInfty:
@@ -474,12 +477,12 @@
   show "(f ---> f0) net"
   proof (rule topological_tendstoI)
     fix S
-    assume "open S""f0 \<in> S"
+    assume "open S" "f0 \<in> S"
     then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
       using ereal_open_cont_interval2[of S f0] real lim by auto
     then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
-      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
-      by (auto intro!: eventually_conj)
+      unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
+      by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
     with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
       by (rule_tac eventually_mono) auto
   qed
@@ -518,7 +521,7 @@
   assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
     and "X ----> x" "Y ----> y"
   shows "x <= y"
-  by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
+  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
 
 lemma incseq_le_ereal:
   fixes X :: "nat \<Rightarrow> ereal"
@@ -577,114 +580,24 @@
   by (metis abs_less_iff assms leI le_max_iff_disj
     less_eq_real_def less_le_not_le less_minus_iff minus_minus)
 
-lemma bounded_increasing_convergent2:
-  fixes f::"nat => real"
-  assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m"
-  shows "EX l. (f ---> l) sequentially"
-proof -
-  def N == "max (abs (f 0)) (abs B)"
-  { fix n
-    have "abs (f n) <= N"
-      unfolding N_def
-      apply (subst bounded_abs)
-      using assms apply auto
-      done }
-  then have "bounded {f n| n::nat. True}"
-    unfolding bounded_real by auto
-  then show ?thesis
-    apply (rule Topology_Euclidean_Space.bounded_increasing_convergent)
-    using assms apply auto
-    done
-qed
-
 lemma lim_ereal_increasing:
-  assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
-  obtains l where "f ----> (l::ereal)"
-proof (cases "f = (\<lambda>x. - \<infinity>)")
-  case True
-  then show thesis
-    using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
-next
-  case False
-  then obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
-  have "ALL n>=N. f n >= f N" using assms by auto
-  then have minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
-  def Y == "(%n. (if n>=N then f n else f N))"
-  then have incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
-  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
-  show thesis
-  proof (cases "EX B. ALL n. f n < ereal B")
-    case False
-    then show thesis
-      apply -
-      apply (rule that[of \<infinity>])
-      unfolding Lim_PInfty not_ex not_all
-      apply safe
-      apply (erule_tac x=B in allE, safe)
-      apply (rule_tac x=x in exI, safe)
-      apply (rule order_trans[OF _ assms[rule_format]])
-      apply auto
-      done
-  next
-    case True
-    then guess B ..
-    then have "ALL n. Y n < ereal B" using Y_def by auto
-    note B = this[rule_format]
-    { fix n
-      have "Y n < \<infinity>"
-        using B[of n]
-        apply (subst less_le_trans)
-        apply auto
-        done
-      then have "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
-    }
-    then have *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
-    { fix n
-      have "real (Y n) < B"
-      proof -
-        case goal1
-        then show ?case
-          using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer
-          unfolding ereal_less using * by auto
-      qed
-    }
-    then have B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
-    have "EX l. (%n. real (Y n)) ----> l"
-      apply (rule bounded_increasing_convergent2)
-    proof safe
-      show "\<And>n. real (Y n) <= B" using B' by auto
-      fix n m :: nat
-      assume "n<=m"
-      then have "ereal (real (Y n)) <= ereal (real (Y m))"
-        using incy[rule_format,of n m] apply(subst ereal_real)+
-        using *[rule_format, of n] *[rule_format, of m] by auto
-      then show "real (Y n) <= real (Y m)" by auto
-    qed
-    then guess l .. note l=this
-    have "Y ----> ereal l"
-      using l
-      apply -
-      apply (subst(asm) lim_ereal[THEN sym])
-      unfolding ereal_real
-      using * apply auto
-      done
-    then show thesis
-      apply -
-      apply (rule that[of "ereal l"])
-      apply (subst tail_same_limit[of Y _ N])
-      using Y_def apply auto
-      done
-  qed
+  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
+  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
+proof
+  show "f ----> (SUP n. f n)"
+    using assms
+    by (intro increasing_tendsto)
+       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
 qed
 
 lemma lim_ereal_decreasing:
-  assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
-  obtains l where "f ----> (l::ereal)"
-proof -
-  from lim_ereal_increasing[of "\<lambda>x. - f x"] assms
-  obtain l where "(\<lambda>x. - f x) ----> l" by auto
-  from ereal_lim_mult[OF this, of "- 1"] show thesis
-    by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)
+  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
+  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
+proof
+  show "f ----> (INF n. f n)"
+    using assms
+    by (intro decreasing_tendsto)
+       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
 qed
 
 lemma compact_ereal:
@@ -711,37 +624,17 @@
   by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
 
 lemma SUP_Lim_ereal:
-  fixes X :: "nat \<Rightarrow> ereal"
-  assumes "incseq X" "X ----> l"
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  assumes inc: "incseq X" and l: "X ----> l"
   shows "(SUP n. X n) = l"
-proof (rule ereal_SUPI)
-  fix n from assms show "X n \<le> l"
-    by (intro incseq_le_ereal) (simp add: incseq_def)
-next
-  fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
-  with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"] show "l \<le> y" by auto
-qed
-
-lemma LIMSEQ_ereal_SUPR:
-  fixes X :: "nat \<Rightarrow> ereal"
-  assumes "incseq X"
-  shows "X ----> (SUP n. X n)"
-proof (rule lim_ereal_increasing)
-  fix n m :: nat
-  assume "m \<le> n"
-  then show "X m \<le> X n" using `incseq X` by (simp add: incseq_def)
-next
-  fix l
-  assume "X ----> l"
-  with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp
-qed
+  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
 
 lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
   using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
   by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
 
 lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
-  using LIMSEQ_ereal_SUPR[of "\<lambda>i. - X i"]
+  using LIMSEQ_SUP[of "\<lambda>i. - X i"]
   by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
 
 lemma SUP_eq_LIMSEQ:
@@ -755,165 +648,66 @@
     from SUP_Lim_ereal[OF inc this]
     show "(SUP n. ereal (f n)) = ereal x" . }
   { assume "(SUP n. ereal (f n)) = ereal x"
-    with LIMSEQ_ereal_SUPR[OF inc]
+    with LIMSEQ_SUP[OF inc]
     show "f ----> x" by auto }
 qed
 
 lemma Liminf_within:
-  fixes f :: "'a::metric_space => ereal"
-  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
-proof -
-  let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
-  { fix T
-    assume T_def: "open T & mono_set T & ?l:T"
-    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
-    proof -
-      { assume "T=UNIV" then have ?thesis by (simp add: gt_ex) }
-      moreover
-      { assume "~(T=UNIV)"
-        then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto
-        then have "B<?l" using T_def by auto
-        then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
-          unfolding less_SUP_iff by auto
-        { fix y assume "y:S & 0 < dist y x & dist y x < d"
-          then have "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
-          then have "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
-        } then have ?thesis apply(rule_tac x="d" in exI) using d_def by auto
-      }
-      ultimately show ?thesis by auto
-    qed
-  }
-  moreover
-  { fix z
-    assume a: "ALL T. open T --> mono_set T --> z : T -->
-       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
-    { fix B
-      assume "B<z"
-      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
-         using a[rule_format, of "{B<..}"] mono_greaterThan by auto
-      { fix y
-        assume "y:(S Int ball x d - {x})"
-        then have "y:S & 0 < dist y x & dist y x < d"
-          unfolding ball_def
-          apply (simp add: dist_commute)
-          apply (metis dist_eq_0_iff less_le zero_le_dist)
-          done
-        then have "B <= f y" using d_def by auto
-      }
-      then have "B <= INFI (S Int ball x d - {x}) f"
-        apply (subst INF_greatest)
-        apply auto
-        done
-      also have "...<=?l"
-        apply (subst SUP_upper)
-        using d_def apply auto
-        done
-      finally have "B<=?l" by auto
-    }
-    then have "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
-  }
-  ultimately show ?thesis
-    unfolding ereal_Liminf_Sup_monoset eventually_within
-    apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"])
-    apply auto
-    done
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
+  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
+  unfolding Liminf_def eventually_within
+proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
+  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+    by (auto simp: zero_less_dist_iff dist_commute)
+  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
+    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
+next
+  fix d :: real assume "0 < d"
+  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
+    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
 qed
 
 lemma Limsup_within:
-  fixes f :: "'a::metric_space => ereal"
-  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
-proof -
-  let ?l = "(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
-  { fix T
-    assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
-    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
-    proof -
-      { assume "T = UNIV"
-        then have ?thesis by (simp add: gt_ex) }
-      moreover
-      { assume "T \<noteq> UNIV"
-        then have "~(uminus ` T = UNIV)"
-          by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)
-        then have "uminus ` T = {Inf (uminus ` T)<..}"
-          using T_def ereal_open_mono_set[of "uminus ` T"] ereal_open_uminus[of T] by auto
-        then obtain B where "T={..<B}"
-          unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]
-          unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp
-        then have "?l<B" using T_def by auto
-        then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
-          unfolding INF_less_iff by auto
-        { fix y
-          assume "y:S & 0 < dist y x & dist y x < d"
-          then have "y:(S Int ball x d - {x})"
-            unfolding ball_def by (auto simp add: dist_commute)
-          then have "f y:T"
-            using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
-        }
-        then have ?thesis
-          apply (rule_tac x="d" in exI)
-          using d_def apply auto
-          done
-      }
-      ultimately show ?thesis by auto
-    qed
-  }
-  moreover
-  { fix z
-    assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
-       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
-    { fix B
-      assume "z<B"
-      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
-         using a[rule_format, of "{..<B}"] by auto
-      { fix y
-        assume "y:(S Int ball x d - {x})"
-        then have "y:S & 0 < dist y x & dist y x < d"
-          unfolding ball_def
-          apply (simp add: dist_commute)
-          apply (metis dist_eq_0_iff less_le zero_le_dist)
-          done
-        then have "f y <= B" using d_def by auto
-      }
-      then have "SUPR (S Int ball x d - {x}) f <= B"
-        apply (subst SUP_least)
-        apply auto
-        done
-      moreover
-      have "?l<=SUPR (S Int ball x d - {x}) f"
-        apply (subst INF_lower)
-        using d_def apply auto
-        done
-      ultimately have "?l<=B" by auto
-    } then have "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
-  }
-  ultimately show ?thesis
-    unfolding ereal_Limsup_Inf_monoset eventually_within
-    apply (subst ereal_InfI)
-    apply auto
-    done
+  fixes f :: "'a::metric_space => 'b::complete_lattice"
+  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
+  unfolding Limsup_def eventually_within
+proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
+  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
+  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
+    by (auto simp: zero_less_dist_iff dist_commute)
+  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
+    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
+next
+  fix d :: real assume "0 < d"
+  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
+    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
+    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
+       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
 qed
 
-
 lemma Liminf_within_UNIV:
-  fixes f :: "'a::metric_space => ereal"
+  fixes f :: "'a::metric_space => _"
   shows "Liminf (at x) f = Liminf (at x within UNIV) f"
   by simp (* TODO: delete *)
 
 
 lemma Liminf_at:
-  fixes f :: "'a::metric_space => ereal"
+  fixes f :: "'a::metric_space => _"
   shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
   using Liminf_within[of x UNIV f] by simp
 
 
 lemma Limsup_within_UNIV:
-  fixes f :: "'a::metric_space => ereal"
+  fixes f :: "'a::metric_space => _"
   shows "Limsup (at x) f = Limsup (at x within UNIV) f"
   by simp (* TODO: delete *)
 
 
 lemma Limsup_at:
-  fixes f :: "'a::metric_space => ereal"
+  fixes f :: "'a::metric_space => _"
   shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
   using Limsup_within[of x UNIV f] by simp
 
@@ -1295,7 +1089,7 @@
 proof -
   have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
     using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
-  from LIMSEQ_ereal_SUPR[OF this]
+  from LIMSEQ_SUP[OF this]
   show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
 qed
 

--- a/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory Discrete_Topology
-imports Multivariate_Analysis
+imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
 begin
 
 text {* Copy of discrete types with discrete topology. This space is polish. *}

--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -297,7 +297,7 @@
     qed
   next
     fix x show "(SUP i. ?g i x) = max 0 (u x)"
-    proof (rule ereal_SUPI)
+    proof (rule SUP_eqI)
       fix i show "?g i x \<le> max 0 (u x)" unfolding max_def f_def
         by (cases "u x") (auto simp: field_simps real_natfloor_le natfloor_neg
                                      mult_nonpos_nonneg mult_nonneg_nonneg)
@@ -2147,7 +2147,7 @@
     assume neq_0: "(\<integral>\<^isup>+ x. max 0 (ereal (2 * w x)) \<partial>M) \<noteq> 0" (is "?wx \<noteq> 0")
     have "0 = limsup (\<lambda>n. 0 :: ereal)" by (simp add: Limsup_const)
     also have "\<dots> \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)"
-      by (intro limsup_mono positive_integral_positive)
+      by (simp add: Limsup_mono  positive_integral_positive)
     finally have pos: "0 \<le> limsup (\<lambda>n. \<integral>\<^isup>+ x. ereal \<bar>u n x - u' x\<bar> \<partial>M)" .
     have "?wx = (\<integral>\<^isup>+ x. liminf (\<lambda>n. max 0 (ereal (?diff n x))) \<partial>M)"
       using u'
@@ -2178,11 +2178,11 @@
   qed
 
   have "liminf ?f \<le> limsup ?f"
-    by (intro ereal_Liminf_le_Limsup trivial_limit_sequentially)
+    by (intro Liminf_le_Limsup trivial_limit_sequentially)
   moreover
   { have "0 = liminf (\<lambda>n. 0 :: ereal)" by (simp add: Liminf_const)
     also have "\<dots> \<le> liminf ?f"
-      by (intro liminf_mono positive_integral_positive)
+      by (simp add: Liminf_mono positive_integral_positive)
     finally have "0 \<le> liminf ?f" . }
   ultimately have liminf_limsup_eq: "liminf ?f = ereal 0" "limsup ?f = ereal 0"
     using `limsup ?f = 0` by auto

--- a/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -698,7 +698,7 @@
   have "integral\<^isup>P lebesgue f = ereal (integral UNIV f')"
   proof (rule tendsto_unique[OF trivial_limit_sequentially])
     have "(\<lambda>i. integral\<^isup>S lebesgue (u i)) ----> (SUP i. integral\<^isup>P lebesgue (u i))"
-      unfolding u_eq by (intro LIMSEQ_ereal_SUPR incseq_positive_integral u)
+      unfolding u_eq by (intro LIMSEQ_SUP incseq_positive_integral u)
     also note positive_integral_monotone_convergence_SUP
       [OF u(2)  borel_measurable_simple_function[OF u(1)] u(5), symmetric]
     finally show "(\<lambda>k. integral\<^isup>S lebesgue (u k)) ----> integral\<^isup>P lebesgue f"

--- a/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -50,7 +50,7 @@
   then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: ereal)"
     by (auto simp: setsum_cases)
   moreover have "(SUP n. if i < n then f i else 0) = (f i :: ereal)"
-  proof (rule ereal_SUPI)
+  proof (rule SUP_eqI)
     fix y :: ereal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y"
     from this[of "Suc i"] show "f i \<le> y" by auto
   qed (insert assms, simp)
@@ -523,7 +523,7 @@
 lemma SUP_emeasure_incseq:
   assumes A: "range A \<subseteq> sets M" "incseq A"
   shows "(SUP n. emeasure M (A n)) = emeasure M (\<Union>i. A i)"
-  using LIMSEQ_ereal_SUPR[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
+  using LIMSEQ_SUP[OF incseq_emeasure, OF A] Lim_emeasure_incseq[OF A]
   by (simp add: LIMSEQ_unique)
 
 lemma decseq_emeasure:
@@ -1570,7 +1570,7 @@
       have "incseq (\<lambda>i. ?M (F i))"
         using `incseq F` unfolding incseq_def by (auto simp: card_mono dest: finite_subset)
       then have "(\<lambda>i. ?M (F i)) ----> (SUP n. ?M (F n))"
-        by (rule LIMSEQ_ereal_SUPR)
+        by (rule LIMSEQ_SUP)
 
       moreover have "(SUP n. ?M (F n)) = \<infinity>"
       proof (rule SUP_PInfty)

--- a/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:27 2013 +0100
+++ b/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:30 2013 +0100
@@ -16,7 +16,7 @@
   assumes f_nonneg: "\<And>i. 0 \<le> f i"
   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
   shows "x = (SUP i : A. f i)"
-proof (subst eq_commute, rule ereal_SUPI)
+proof (subst eq_commute, rule SUP_eqI)
   show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
 next
   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
@@ -45,7 +45,7 @@
   assumes f_nonneg: "\<And>i. 0 \<le> f i"
   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
   shows "x = (INF i : A. f i)"
-proof (subst eq_commute, rule ereal_INFI)
+proof (subst eq_commute, rule INF_eqI)
   show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
 next
   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
@@ -79,7 +79,7 @@
   from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
   ultimately
   have "(INF i : A. f i) = x + e" using `e > 0`
-    by (intro ereal_INFI)
+    by (intro INF_eqI)
       (force, metis add.comm_neutral add_left_mono ereal_less(1)
         linorder_not_le not_less_iff_gr_or_eq)
   thus False using assms by auto
@@ -97,7 +97,7 @@
   from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
   ultimately
   have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
-    by (intro ereal_SUPI)
+    by (intro SUP_eqI)
        (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
         metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
   thus False using assms by auto
@@ -290,7 +290,7 @@
       have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
         by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
       ultimately show ?thesis by simp
-    qed (auto intro!: ereal_INFI)
+    qed (auto intro!: INF_eqI)
     note `?inner A` `?outer A` }
   note closed_in_D = this
   from `B \<in> sets borel`
@@ -299,8 +299,8 @@
   then show "?inner B" "?outer B"
   proof (induct B rule: sigma_sets_induct_disjoint)
     case empty
-    { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
-    { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
+    { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
+    { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
   next
     case (basic B)
     { case 1 from basic closed_in_D show ?case by auto }