# HG changeset patch
# User wenzelm
# Date 1362499656 -3600
# Node ID ef494f2288cf780327b7319fcefb1e0e9e4af4e2
# Parent  dd1dd470690b683acb058d3c45b350666979bd5a# Parent  45579fbe5a242400fb880ce7da4d0fb21c111f64
merged

diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Complete_Lattices.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -589,6 +589,14 @@
 
 end
 
+instance complete_linorder \<subseteq> complete_distrib_lattice
+  apply default
+  apply (safe intro!: INF_eqI[symmetric] sup_mono complete_lattice_class.Inf_lower
+                      SUP_eqI[symmetric] inf_mono complete_lattice_class.Sup_upper)
+  apply (auto simp: not_less[symmetric]
+                    Inf_less_iff less_Sup_iff le_max_iff_disj sup_max min_le_iff_disj inf_min)
+  done
+
 subsection {* Complete lattice on @{typ bool} *}
 
 instantiation bool :: complete_lattice
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Library/Extended.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Extended.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -0,0 +1,201 @@
+(*  Author:     Tobias Nipkow, TU München
+
+A theory of types extended with a greatest and a least element.
+Oriented towards numeric types, hence "\<infinity>" and "-\<infinity>".
+*)
+
+theory Extended
+imports Main
+begin
+
+datatype 'a extended = Fin 'a | Pinf ("\<infinity>") | Minf ("-\<infinity>")
+
+lemmas extended_cases2 = extended.exhaust[case_product extended.exhaust]
+lemmas extended_cases3 = extended.exhaust[case_product extended_cases2]
+
+instantiation extended :: (order)order
+begin
+
+fun less_eq_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
+"Fin x \<le> Fin y = (x \<le> y)" |
+"_     \<le> Pinf  = True" |
+"Minf  \<le> _     = True" |
+"(_::'a extended) \<le> _     = False"
+
+lemma less_eq_extended_cases:
+  "x \<le> y = (case x of Fin x \<Rightarrow> (case y of Fin y \<Rightarrow> x \<le> y | Pinf \<Rightarrow> True | Minf \<Rightarrow> False)
+            | Pinf \<Rightarrow> y=Pinf | Minf \<Rightarrow> True)"
+by(induct x y rule: less_eq_extended.induct)(auto split: extended.split)
+
+definition less_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> bool" where
+"((x::'a extended) < y) = (x \<le> y & \<not> x \<ge> y)"
+
+instance
+proof
+  case goal1 show ?case by(rule less_extended_def)
+next
+  case goal2 show ?case by(cases x) auto
+next
+  case goal3 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
+next
+  case goal4 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
+qed
+
+end
+
+instance extended :: (linorder)linorder
+proof
+  case goal1 thus ?case by(auto simp: less_eq_extended_cases split:extended.splits)
+qed
+
+lemma Minf_le[simp]: "Minf \<le> y"
+by(cases y) auto
+lemma le_Pinf[simp]: "x \<le> Pinf"
+by(cases x) auto
+lemma le_Minf[simp]: "x \<le> Minf \<longleftrightarrow> x = Minf"
+by(cases x) auto
+lemma Pinf_le[simp]: "Pinf \<le> x \<longleftrightarrow> x = Pinf"
+by(cases x) auto
+
+lemma less_extended_simps[simp]:
+  "Fin x < Fin y = (x < y)"
+  "Fin x < Pinf  = True"
+  "Fin x < Minf  = False"
+  "Pinf < h      = False"
+  "Minf < Fin x  = True"
+  "Minf < Pinf   = True"
+  "l    < Minf   = False"
+by (auto simp add: less_extended_def)
+
+lemma min_extended_simps[simp]:
+  "min (Fin x) (Fin y) = Fin(min x y)"
+  "min xx      Pinf    = xx"
+  "min xx      Minf    = Minf"
+  "min Pinf    yy      = yy"
+  "min Minf    yy      = Minf"
+by (auto simp add: min_def)
+
+lemma max_extended_simps[simp]:
+  "max (Fin x) (Fin y) = Fin(max x y)"
+  "max xx      Pinf    = Pinf"
+  "max xx      Minf    = xx"
+  "max Pinf    yy      = Pinf"
+  "max Minf    yy      = yy"
+by (auto simp add: max_def)
+
+
+instantiation extended :: (plus)plus
+begin
+
+text {* The following definition of of addition is totalized
+to make it asociative and commutative. Normally the sum of plus and minus infinity is undefined. *}
+
+fun plus_extended where
+"Fin x + Fin y = Fin(x+y)" |
+"Fin x + Pinf  = Pinf" |
+"Pinf  + Fin x = Pinf" |
+"Pinf  + Pinf  = Pinf" |
+"Minf  + Fin y = Minf" |
+"Fin x + Minf  = Minf" |
+"Minf  + Minf  = Minf" |
+"Minf  + Pinf  = Pinf" |
+"Pinf  + Minf  = Pinf"
+
+instance ..
+
+end
+
+
+instance extended :: (ab_semigroup_add)ab_semigroup_add
+proof
+  fix a b c :: "'a extended"
+  show "a + b = b + a"
+    by (induct a b rule: plus_extended.induct) (simp_all add: ac_simps)
+  show "a + b + c = a + (b + c)"
+    by (cases rule: extended_cases3[of a b c]) (simp_all add: ac_simps)
+qed
+
+instance extended :: (ordered_ab_semigroup_add)ordered_ab_semigroup_add
+proof
+  fix a b c :: "'a extended"
+  assume "a \<le> b" then show "c + a \<le> c + b"
+    by (cases rule: extended_cases3[of a b c]) (auto simp: add_left_mono)
+qed
+
+instantiation extended :: (comm_monoid_add)comm_monoid_add
+begin
+
+definition "0 = Fin 0"
+
+instance
+proof
+  fix x :: "'a extended" show "0 + x = x" unfolding zero_extended_def by(cases x)auto
+qed
+
+end
+
+instantiation extended :: (uminus)uminus
+begin
+
+fun uminus_extended where
+"- (Fin x) = Fin (- x)" |
+"- Pinf    = Minf" |
+"- Minf    = Pinf"
+
+instance ..
+
+end
+
+
+instantiation extended :: (ab_group_add)minus
+begin
+definition "x - y = x + -(y::'a extended)"
+instance ..
+end
+
+lemma minus_extended_simps[simp]:
+  "Fin x - Fin y = Fin(x - y)"
+  "Fin x - Pinf  = Minf"
+  "Fin x - Minf  = Pinf"
+  "Pinf  - Fin y = Pinf"
+  "Pinf  - Minf  = Pinf"
+  "Minf  - Fin y = Minf"
+  "Minf  - Pinf  = Minf"
+  "Minf  - Minf  = Pinf"
+  "Pinf  - Pinf  = Pinf"
+by (simp_all add: minus_extended_def)
+
+instantiation extended :: (lattice)bounded_lattice
+begin
+
+definition "bot = Minf"
+definition "top = Pinf"
+
+fun inf_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
+"inf_extended (Fin i) (Fin j) = Fin (inf i j)" |
+"inf_extended a Minf = Minf" |
+"inf_extended Minf a = Minf" |
+"inf_extended Pinf a = a" |
+"inf_extended a Pinf = a"
+
+fun sup_extended :: "'a extended \<Rightarrow> 'a extended \<Rightarrow> 'a extended" where
+"sup_extended (Fin i) (Fin j) = Fin (sup i j)" |
+"sup_extended a Pinf = Pinf" |
+"sup_extended Pinf a = Pinf" |
+"sup_extended Minf a = a" |
+"sup_extended a Minf = a"
+
+instance
+proof
+  fix x y z ::"'a extended"
+  show "inf x y \<le> x" "inf x y \<le> y" "\<lbrakk>x \<le> y; x \<le> z\<rbrakk> \<Longrightarrow> x \<le> inf y z"
+    "x \<le> sup x y" "y \<le> sup x y" "\<lbrakk>y \<le> x; z \<le> x\<rbrakk> \<Longrightarrow> sup y z \<le> x" "bot \<le> x" "x \<le> top"
+    apply (atomize (full))
+    apply (cases rule: extended_cases3[of x y z])
+    apply (auto simp: bot_extended_def top_extended_def)
+    done
+qed
+end
+
+end
+
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -8,7 +8,7 @@
 header {* Extended real number line *}
 
 theory Extended_Real
-imports Complex_Main Extended_Nat
+imports Complex_Main Extended_Nat Liminf_Limsup
 begin
 
 text {*
@@ -18,26 +18,6 @@
 
 *}
 
-lemma SUPR_pair:
-  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
-  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
-
-lemma INFI_pair:
-  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
-  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
-
-lemma le_Sup_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
-  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
-  unfolding le_SUP_iff
-  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
-
-lemma Inf_le_iff_less:
-  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
-  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
-  unfolding INF_le_iff
-  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
-
 subsection {* Definition and basic properties *}
 
 datatype ereal = ereal real | PInfty | MInfty
@@ -151,10 +131,11 @@
 
 subsubsection "Addition"
 
-instantiation ereal :: comm_monoid_add
+instantiation ereal :: "{one, comm_monoid_add}"
 begin
 
 definition "0 = ereal 0"
+definition "1 = ereal 1"
 
 function plus_ereal where
 "ereal r + ereal p = ereal (r + p)" |
@@ -193,6 +174,8 @@
 qed
 end
 
+instance ereal :: numeral ..
+
 lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
   unfolding real_of_ereal_def zero_ereal_def by simp
 
@@ -494,9 +477,7 @@
 instantiation ereal :: "{comm_monoid_mult, sgn}"
 begin
 
-definition "1 = ereal 1"
-
-function sgn_ereal where
+function sgn_ereal :: "ereal \<Rightarrow> ereal" where
   "sgn (ereal r) = ereal (sgn r)"
 | "sgn (\<infinity>::ereal) = 1"
 | "sgn (-\<infinity>::ereal) = -1"
@@ -681,8 +662,6 @@
   using assms
   by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
 
-instance ereal :: numeral ..
-
 lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
   apply (induct w rule: num_induct)
   apply (simp only: numeral_One one_ereal_def)
@@ -1718,6 +1697,31 @@
   show thesis by auto
 qed
 
+instance ereal :: perfect_space
+proof (default, rule)
+  fix a :: ereal assume a: "open {a}"
+  show False
+  proof (cases a)
+    case MInf
+    then obtain y where "{..<ereal y} \<le> {a}" using a open_MInfty2[of "{a}"] by auto
+    then have "ereal (y - 1) \<in> {a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
+    then show False using `a = -\<infinity>` by auto
+  next
+    case PInf
+    then obtain y where "{ereal y<..} \<le> {a}" using a open_PInfty2[of "{a}"] by auto
+    then have "ereal (y + 1) \<in> {a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
+    then show False using `a = \<infinity>` by auto
+  next
+    case (real r)
+    then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
+    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
+    then obtain b where b_def: "a<b \<and> b<a+e"
+      using fin ereal_between dense[of a "a+e"] by auto
+    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
+    then show False using b_def e by auto
+  qed
+qed
+
 subsubsection {* Convergent sequences *}
 
 lemma lim_ereal[simp]:
@@ -1806,9 +1810,16 @@
   "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: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
+lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
   by (intro LIMSEQ_le_const2) auto
 
+lemma Lim_bounded2_ereal:
+  assumes lim:"f ----> (l :: 'a::linorder_topology)" and ge: "ALL n>=N. f n >= C"
+  shows "l>=C"
+  using ge
+  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+     (auto simp: eventually_sequentially)
+
 lemma real_of_ereal_mult[simp]:
   fixes a b :: ereal shows "real (a * b) = real a * real b"
   by (cases rule: ereal2_cases[of a b]) auto
@@ -1981,123 +1992,15 @@
     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 ereal_Limsup_uminus:
+  fixes f :: "'a => ereal"
+  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
+  unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
 
-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 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")
+  unfolding le_Liminf_iff eventually_sequentially ..
 
 lemma
   fixes X :: "nat \<Rightarrow> ereal"
@@ -2105,220 +2008,6 @@
     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 le_Liminf_iff:
-  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
-  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
-proof -
-  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
-    then have "eventually (\<lambda>x. y < X x) F"
-      by (auto elim!: eventually_elim1 dest: less_INF_D) }
-  moreover
-  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
-    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
-    proof cases
-      assume "\<exists>z. y < z \<and> z < C"
-      then guess z ..
-      moreover then have "z \<le> INFI {x. z < X x} X"
-        by (auto intro!: INF_greatest)
-      ultimately show ?thesis
-        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
-    next
-      assume "\<not> (\<exists>z. y < z \<and> z < C)"
-      then have "C \<le> INFI {x. y < X x} X"
-        by (intro INF_greatest) auto
-      with `y < C` show ?thesis
-        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
-    qed }
-  ultimately show ?thesis
-    unfolding Liminf_def le_SUP_iff by auto
-qed
-
-lemma lim_imp_Liminf:
-  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes lim: "(f ---> f0) F"
-  shows "Liminf F f = f0"
-proof (intro Liminf_eqI)
-  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])
-next
-  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
-  show "f0 \<le> y"
-  proof cases
-    assume "\<exists>z. y < z \<and> z < f0"
-    then guess z ..
-    moreover have "z \<le> INFI {x. z < f x} f"
-      by (rule INF_greatest) simp
-    ultimately show ?thesis
-      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
-  next
-    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
-    show ?thesis
-    proof (rule classical)
-      assume "\<not> f0 \<le> y"
-      then have "eventually (\<lambda>x. y < f x) F"
-        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
-      then have "eventually (\<lambda>x. f0 \<le> f x) F"
-        using discrete by (auto elim!: eventually_elim1)
-      then have "INFI {x. f0 \<le> f x} f \<le> y"
-        by (rule upper)
-      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
-        by (intro INF_greatest) simp
-      ultimately show "f0 \<le> y" by simp
-    qed
-  qed
-qed
-
-lemma lim_imp_Limsup:
-  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
-  assumes ntriv: "\<not> trivial_limit F"
-  assumes lim: "(f ---> f0) F"
-  shows "Limsup F f = f0"
-proof (intro Limsup_eqI)
-  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])
-next
-  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
-  show "y \<le> f0"
-  proof cases
-    assume "\<exists>z. f0 < z \<and> z < y"
-    then guess z ..
-    moreover have "SUPR {x. f x < z} f \<le> z"
-      by (rule SUP_least) simp
-    ultimately show ?thesis
-      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
-  next
-    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
-    show ?thesis
-    proof (rule classical)
-      assume "\<not> y \<le> f0"
-      then have "eventually (\<lambda>x. f x < y) F"
-        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
-      then have "eventually (\<lambda>x. f x \<le> f0) F"
-        using discrete by (auto elim!: eventually_elim1 simp: not_less)
-      then have "y \<le> SUPR {x. f x \<le> f0} f"
-        by (rule lower)
-      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
-        by (intro SUP_least) simp
-      ultimately show "y \<le> f0" by simp
-    qed
-  qed
-qed
-
-lemma Liminf_eq_Limsup:
-  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
-  assumes ntriv: "\<not> trivial_limit F"
-    and lim: "Liminf F f = f0" "Limsup F f = f0"
-  shows "(f ---> f0) F"
-proof (rule order_tendstoI)
-  fix a assume "f0 < a"
-  with assms have "Limsup F f < a" by simp
-  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
-    unfolding Limsup_def INF_less_iff by auto
-  then show "eventually (\<lambda>x. f x < a) F"
-    by (auto elim!: eventually_elim1 dest: SUP_lessD)
-next
-  fix a assume "a < f0"
-  with assms have "a < Liminf F f" by simp
-  then obtain P where "eventually P F" "a < INFI (Collect P) f"
-    unfolding Liminf_def less_SUP_iff by auto
-  then show "eventually (\<lambda>x. a < f x) F"
-    by (auto elim!: eventually_elim1 dest: less_INF_D)
-qed
-
-lemma tendsto_iff_Liminf_eq_Limsup:
-  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
-  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
-  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
-
-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")
-  unfolding le_Liminf_iff eventually_sequentially ..
-
-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
-
-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 *)
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Library/Glbs.thy
--- a/src/HOL/Library/Glbs.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Library/Glbs.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -70,4 +70,10 @@
 lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
   unfolding lbs_def isGlb_def by (rule greatestPD2)
 
+lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
+  apply (frule isGlb_isLb)
+  apply (frule_tac x = y in isGlb_isLb)
+  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
+  done
+
 end
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Library/Library.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -17,7 +17,7 @@
   Diagonal_Subsequence
   Dlist
   Eval_Witness
-  Extended_Nat
+  Extended Extended_Nat Extended_Real
   FinFun
   Float
   Formal_Power_Series
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Library/Liminf_Limsup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -0,0 +1,320 @@
+(*  Title:      HOL/Library/Liminf_Limsup.thy
+    Author:     Johannes Hölzl, TU München
+*)
+
+header {* Liminf and Limsup on complete lattices *}
+
+theory Liminf_Limsup
+imports "~~/src/HOL/Complex_Main"
+begin
+
+lemma le_Sup_iff_less:
+  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+  unfolding le_SUP_iff
+  by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
+
+lemma Inf_le_iff_less:
+  fixes x :: "'a :: {complete_linorder, inner_dense_linorder}"
+  shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+  unfolding INF_le_iff
+  by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
+
+lemma SUPR_pair:
+  "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
+  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
+
+lemma INFI_pair:
+  "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
+  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
+
+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 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 le_Liminf_iff:
+  fixes X :: "_ \<Rightarrow> _ :: complete_linorder"
+  shows "C \<le> Liminf F X \<longleftrightarrow> (\<forall>y<C. eventually (\<lambda>x. y < X x) F)"
+proof -
+  { fix y P assume "eventually P F" "y < INFI (Collect P) X"
+    then have "eventually (\<lambda>x. y < X x) F"
+      by (auto elim!: eventually_elim1 dest: less_INF_D) }
+  moreover
+  { fix y P assume "y < C" and y: "\<forall>y<C. eventually (\<lambda>x. y < X x) F"
+    have "\<exists>P. eventually P F \<and> y < INFI (Collect P) X"
+    proof cases
+      assume "\<exists>z. y < z \<and> z < C"
+      then guess z ..
+      moreover then have "z \<le> INFI {x. z < X x} X"
+        by (auto intro!: INF_greatest)
+      ultimately show ?thesis
+        using y by (intro exI[of _ "\<lambda>x. z < X x"]) auto
+    next
+      assume "\<not> (\<exists>z. y < z \<and> z < C)"
+      then have "C \<le> INFI {x. y < X x} X"
+        by (intro INF_greatest) auto
+      with `y < C` show ?thesis
+        using y by (intro exI[of _ "\<lambda>x. y < X x"]) auto
+    qed }
+  ultimately show ?thesis
+    unfolding Liminf_def le_SUP_iff by auto
+qed
+
+lemma lim_imp_Liminf:
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Liminf F f = f0"
+proof (intro Liminf_eqI)
+  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])
+next
+  fix y assume upper: "\<And>P. eventually P F \<Longrightarrow> INFI (Collect P) f \<le> y"
+  show "f0 \<le> y"
+  proof cases
+    assume "\<exists>z. y < z \<and> z < f0"
+    then guess z ..
+    moreover have "z \<le> INFI {x. z < f x} f"
+      by (rule INF_greatest) simp
+    ultimately show ?thesis
+      using lim[THEN topological_tendstoD, THEN upper, of "{z <..}"] by auto
+  next
+    assume discrete: "\<not> (\<exists>z. y < z \<and> z < f0)"
+    show ?thesis
+    proof (rule classical)
+      assume "\<not> f0 \<le> y"
+      then have "eventually (\<lambda>x. y < f x) F"
+        using lim[THEN topological_tendstoD, of "{y <..}"] by auto
+      then have "eventually (\<lambda>x. f0 \<le> f x) F"
+        using discrete by (auto elim!: eventually_elim1)
+      then have "INFI {x. f0 \<le> f x} f \<le> y"
+        by (rule upper)
+      moreover have "f0 \<le> INFI {x. f0 \<le> f x} f"
+        by (intro INF_greatest) simp
+      ultimately show "f0 \<le> y" by simp
+    qed
+  qed
+qed
+
+lemma lim_imp_Limsup:
+  fixes f :: "'a \<Rightarrow> _ :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+  assumes lim: "(f ---> f0) F"
+  shows "Limsup F f = f0"
+proof (intro Limsup_eqI)
+  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])
+next
+  fix y assume lower: "\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f"
+  show "y \<le> f0"
+  proof cases
+    assume "\<exists>z. f0 < z \<and> z < y"
+    then guess z ..
+    moreover have "SUPR {x. f x < z} f \<le> z"
+      by (rule SUP_least) simp
+    ultimately show ?thesis
+      using lim[THEN topological_tendstoD, THEN lower, of "{..< z}"] by auto
+  next
+    assume discrete: "\<not> (\<exists>z. f0 < z \<and> z < y)"
+    show ?thesis
+    proof (rule classical)
+      assume "\<not> y \<le> f0"
+      then have "eventually (\<lambda>x. f x < y) F"
+        using lim[THEN topological_tendstoD, of "{..< y}"] by auto
+      then have "eventually (\<lambda>x. f x \<le> f0) F"
+        using discrete by (auto elim!: eventually_elim1 simp: not_less)
+      then have "y \<le> SUPR {x. f x \<le> f0} f"
+        by (rule lower)
+      moreover have "SUPR {x. f x \<le> f0} f \<le> f0"
+        by (intro SUP_least) simp
+      ultimately show "y \<le> f0" by simp
+    qed
+  qed
+qed
+
+lemma Liminf_eq_Limsup:
+  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  assumes ntriv: "\<not> trivial_limit F"
+    and lim: "Liminf F f = f0" "Limsup F f = f0"
+  shows "(f ---> f0) F"
+proof (rule order_tendstoI)
+  fix a assume "f0 < a"
+  with assms have "Limsup F f < a" by simp
+  then obtain P where "eventually P F" "SUPR (Collect P) f < a"
+    unfolding Limsup_def INF_less_iff by auto
+  then show "eventually (\<lambda>x. f x < a) F"
+    by (auto elim!: eventually_elim1 dest: SUP_lessD)
+next
+  fix a assume "a < f0"
+  with assms have "a < Liminf F f" by simp
+  then obtain P where "eventually P F" "a < INFI (Collect P) f"
+    unfolding Liminf_def less_SUP_iff by auto
+  then show "eventually (\<lambda>x. a < f x) F"
+    by (auto elim!: eventually_elim1 dest: less_INF_D)
+qed
+
+lemma tendsto_iff_Liminf_eq_Limsup:
+  fixes f0 :: "'a :: {complete_linorder, linorder_topology}"
+  shows "\<not> trivial_limit F \<Longrightarrow> (f ---> f0) F \<longleftrightarrow> (Liminf F f = f0 \<and> Limsup F f = f0)"
+  by (metis Liminf_eq_Limsup lim_imp_Limsup lim_imp_Liminf)
+
+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
+
+end
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -11,6 +11,114 @@
   imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"
 begin
 
+lemma convergent_limsup_cl:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  shows "convergent X \<Longrightarrow> limsup X = lim X"
+  by (auto simp: convergent_def limI lim_imp_Limsup)
+
+lemma lim_increasing_cl:
+  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_decreasing_cl:
+  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_complete_linorder:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
+proof -
+  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
+    using seq_monosub[of X] unfolding comp_def by auto
+  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
+    by (auto simp add: monoseq_def)
+  then obtain l where "(X\<circ>r) ----> l"
+     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] by auto
+  then show ?thesis using `subseq r` by auto
+qed
+
+lemma compact_UNIV: "compact (UNIV :: 'a::{complete_linorder, linorder_topology, second_countable_topology} set)"
+  using compact_complete_linorder
+  by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
+
+lemma compact_eq_closed:
+  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
+  shows "compact S \<longleftrightarrow> closed S"
+  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto
+
+lemma closed_contains_Sup_cl:
+  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
+  assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S"
+proof -
+  from compact_eq_closed[of S] compact_attains_sup[of S] assms
+  obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
+  moreover then have "Sup S = s"
+    by (auto intro!: Sup_eqI)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma closed_contains_Inf_cl:
+  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
+  assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S"
+proof -
+  from compact_eq_closed[of S] compact_attains_inf[of S] assms
+  obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
+  moreover then have "Inf S = s"
+    by (auto intro!: Inf_eqI)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma ereal_dense3: 
+  fixes x y :: ereal shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
+proof (cases x y rule: ereal2_cases, simp_all)
+  fix r q :: real assume "r < q"
+  from Rats_dense_in_real[OF this]
+  show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
+    by (fastforce simp: Rats_def)
+next
+  fix r :: real show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
+    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
+    by (auto simp: Rats_def)
+qed
+
+instance ereal :: second_countable_topology
+proof (default, intro exI conjI)
+  let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
+  show "countable ?B" by (auto intro: countable_rat)
+  show "open = generate_topology ?B"
+  proof (intro ext iffI)
+    fix S :: "ereal set" assume "open S"
+    then show "generate_topology ?B S"
+      unfolding open_generated_order
+    proof induct
+      case (Basis b)
+      then obtain e where "b = {..< e} \<or> b = {e <..}" by auto
+      moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}"
+        by (auto dest: ereal_dense3
+                 simp del: ex_simps
+                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
+      ultimately show ?case
+        by (auto intro: generate_topology.intros)
+    qed (auto intro: generate_topology.intros)
+  next
+    fix S assume "generate_topology ?B S" then show "open S" by induct auto
+  qed
+qed
+
 lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
   unfolding continuous_on_topological open_ereal_def by auto
 
@@ -22,35 +130,13 @@
 
 lemma ereal_open_uminus:
   fixes S :: "ereal set"
-  assumes "open S"
-  shows "open (uminus ` S)"
-  unfolding open_ereal_def
-proof (intro conjI impI)
-  obtain x y where
-    S: "open (ereal -` S)" "\<infinity> \<in> S \<Longrightarrow> {ereal x<..} \<subseteq> S" "-\<infinity> \<in> S \<Longrightarrow> {..< ereal y} \<subseteq> S"
-    using `open S` unfolding open_ereal_def by auto
-  have "ereal -` uminus ` S = uminus ` (ereal -` S)"
-  proof safe
-    fix x y
-    assume "ereal x = - y" "y \<in> S"
-    then show "x \<in> uminus ` ereal -` S" by (cases y) auto
-  next
-    fix x
-    assume "ereal x \<in> S"
-    then show "- x \<in> ereal -` uminus ` S"
-      by (auto intro: image_eqI[of _ _ "ereal x"])
-  qed
-  then show "open (ereal -` uminus ` S)"
-    using S by (auto intro: open_negations)
-  { assume "\<infinity> \<in> uminus ` S"
-    then have "-\<infinity> \<in> S" by (metis image_iff ereal_uminus_uminus)
-    then have "uminus ` {..<ereal y} \<subseteq> uminus ` S" using S by (intro image_mono) auto
-    then show "\<exists>x. {ereal x<..} \<subseteq> uminus ` S" using ereal_uminus_lessThan by auto }
-  { assume "-\<infinity> \<in> uminus ` S"
-    then have "\<infinity> : S" by (metis image_iff ereal_uminus_uminus)
-    then have "uminus ` {ereal x<..} <= uminus ` S" using S by (intro image_mono) auto
-    then show "\<exists>y. {..<ereal y} <= uminus ` S" using ereal_uminus_greaterThan by auto }
-qed
+  assumes "open S" shows "open (uminus ` S)"
+  using `open S`[unfolded open_generated_order]
+proof induct
+  have "range uminus = (UNIV :: ereal set)"
+    by (auto simp: image_iff ereal_uminus_eq_reorder)
+  then show "open (range uminus :: ereal set)" by simp
+qed (auto simp add: image_Union image_Int)
 
 lemma ereal_uminus_complement:
   fixes S :: "ereal set"
@@ -61,83 +147,7 @@
   fixes S :: "ereal set"
   assumes "closed S"
   shows "closed (uminus ` S)"
-  using assms unfolding closed_def
-  using ereal_open_uminus[of "- S"] ereal_uminus_complement by auto
-
-instance ereal :: perfect_space
-proof (default, rule)
-  fix a :: ereal assume a: "open {a}"
-  show False
-  proof (cases a)
-    case MInf
-    then obtain y where "{..<ereal y} <= {a}" using a open_MInfty2[of "{a}"] by auto
-    then have "ereal(y - 1):{a}" apply (subst subsetD[of "{..<ereal y}"]) by auto
-    then show False using `a=(-\<infinity>)` by auto
-  next
-    case PInf
-    then obtain y where "{ereal y<..} <= {a}" using a open_PInfty2[of "{a}"] by auto
-    then have "ereal(y+1):{a}" apply (subst subsetD[of "{ereal y<..}"]) by auto
-    then show False using `a=\<infinity>` by auto
-  next
-    case (real r) then have fin: "\<bar>a\<bar> \<noteq> \<infinity>" by simp
-    from ereal_open_cont_interval[OF a singletonI this] guess e . note e = this
-    then obtain b where b_def: "a<b & b<a+e"
-      using fin ereal_between dense[of a "a+e"] by auto
-    then have "b: {a-e <..< a+e}" using fin ereal_between[of a e] e by auto
-    then show False using b_def e by auto
-  qed
-qed
-
-lemma ereal_closed_contains_Inf:
-  fixes S :: "ereal set"
-  assumes "closed S" "S ~= {}"
-  shows "Inf S : S"
-proof (rule ccontr)
-  assume "Inf S \<notin> S"
-  then have a: "open (-S)" "Inf S:(- S)" using assms by auto
-  show False
-  proof (cases "Inf S")
-    case MInf
-    then have "(-\<infinity>) : - S" using a by auto
-    then obtain y where "{..<ereal y} <= (-S)" using a open_MInfty2[of "- S"] by auto
-    then have "ereal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff
-      complete_lattice_class.Inf_greatest double_complement set_rev_mp)
-    then show False using MInf by auto
-  next
-    case PInf
-    then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
-    then show False using `Inf S ~: S` by (simp add: top_ereal_def)
-  next
-    case (real r)
-    then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
-    from ereal_open_cont_interval[OF a this] guess e . note e = this
-    { fix x
-      assume "x:S" then have "x>=Inf S" by (rule complete_lattice_class.Inf_lower)
-      then have *: "x>Inf S-e" using e by (metis fin ereal_between(1) order_less_le_trans)
-      { assume "x<Inf S+e"
-        then have "x:{Inf S-e <..< Inf S+e}" using * by auto
-        then have False using e `x:S` by auto
-      } then have "x>=Inf S+e" by (metis linorder_le_less_linear)
-    }
-    then have "Inf S + e <= Inf S" by (metis le_Inf_iff)
-    then show False using real e by (cases e) auto
-  qed
-qed
-
-lemma ereal_closed_contains_Sup:
-  fixes S :: "ereal set"
-  assumes "closed S" "S ~= {}"
-  shows "Sup S : S"
-proof -
-  have "closed (uminus ` S)"
-    by (metis assms(1) ereal_closed_uminus)
-  then have "Inf (uminus ` S) : uminus ` S"
-    using assms ereal_closed_contains_Inf[of "uminus ` S"] by auto
-  then have "- Sup S : uminus ` S"
-    using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)
-  then show ?thesis
-    by (metis imageI ereal_uminus_uminus ereal_minus_minus_image)
-qed
+  using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus)
 
 lemma ereal_open_closed_aux:
   fixes S :: "ereal set"
@@ -146,7 +156,7 @@
   shows "S = {}"
 proof (rule ccontr)
   assume "S ~= {}"
-  then have *: "(Inf S):S" by (metis assms(2) ereal_closed_contains_Inf)
+  then have *: "(Inf S):S" by (metis assms(2) closed_contains_Inf_cl)
   { assume "Inf S=(-\<infinity>)"
     then have False using * assms(3) by auto }
   moreover
@@ -284,14 +294,6 @@
     ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
   by (auto simp add: algebra_simps)
 
-lemma Lim_bounded2_ereal:
-  assumes lim:"f ----> (l :: ereal)"
-    and ge: "ALL n>=N. f n >= C"
-  shows "l>=C"
-  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
   assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
@@ -303,113 +305,9 @@
   then show "x = -\<infinity>" by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
 qed
 
-lemma ereal_open_mono_set:
-  fixes S :: "ereal set"
-  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
-  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
-    ereal_open_closed mono_set_iff open_ereal_greaterThan)
-
-lemma ereal_closed_mono_set:
-  fixes S :: "ereal set"
-  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
-  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
-    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
-
-lemma ereal_Liminf_Sup_monoset:
-  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}"
-    (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 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 dense_le)
-    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}"
-    (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 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 dense_ge)
-    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
 
-lemma ereal_Limsup_uminus:
-  fixes f :: "'a => ereal"
-  shows "Limsup net (\<lambda>x. - (f x)) = -(Liminf net f)"
-proof -
-  { fix P l
-    have "(\<exists>x. (l::ereal) = -x \<and> P x) \<longleftrightarrow> P (-l)"
-      by (auto intro!: exI[of _ "-l"]) }
-  note Ex_cancel = this
-  { fix P :: "ereal set \<Rightarrow> bool"
-    have "(\<forall>S. P S) \<longleftrightarrow> (\<forall>S. P (uminus`S))"
-      apply auto
-      apply (erule_tac x="uminus`S" in allE)
-      apply (auto simp: image_image)
-      done }
-  note add_uminus_image = this
-  { fix x S
-    have "(x::ereal) \<in> uminus`S \<longleftrightarrow> -x\<in>S"
-      by (auto intro!: image_eqI[of _ _ "-x"]) }
-  note remove_uminus_image = this
-  show ?thesis
-    unfolding ereal_Limsup_Inf_monoset ereal_Liminf_Sup_monoset
-    unfolding ereal_Inf_uminus_image_eq[symmetric] image_Collect Ex_cancel
-    by (subst add_uminus_image) (simp add: open_uminus_iff remove_uminus_image)
-qed
-
 lemma ereal_Liminf_uminus:
   fixes f :: "'a => ereal"
   shows "Liminf net (\<lambda>x. - (f x)) = -(Limsup net f)"
@@ -423,219 +321,78 @@
     ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
   by (auto simp: ereal_uminus_reorder)
 
-lemma lim_imp_Limsup:
-  fixes f :: "'a => ereal"
-  assumes "\<not> trivial_limit net"
-    and lim: "(f ---> f0) net"
-  shows "Limsup net f = f0"
-  using ereal_Lim_uminus[of f f0] lim_imp_Liminf[of net "(%x. -(f x))" "-f0"]
-     ereal_Liminf_uminus[of net f] assms by simp
-
-lemma convergent_ereal_limsup:
-  fixes X :: "nat \<Rightarrow> ereal"
-  shows "convergent X \<Longrightarrow> limsup X = lim X"
-  by (auto simp: convergent_def limI lim_imp_Limsup)
-
 lemma Liminf_PInfty:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "\<not> trivial_limit net"
   shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
-proof (intro lim_imp_Liminf iffI assms)
-  assume rhs: "Liminf net f = \<infinity>"
-  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
+  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto
 
 lemma Limsup_MInfty:
   fixes f :: "'a \<Rightarrow> ereal"
   assumes "\<not> trivial_limit net"
   shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
-  using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
-        ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
-
-lemma ereal_Liminf_eq_Limsup:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes ntriv: "\<not> trivial_limit net"
-    and lim: "Liminf net f = f0" "Limsup net f = f0"
-  shows "(f ---> f0) net"
-proof (cases f0)
-  case PInf
-  then show ?thesis using Liminf_PInfty[OF ntriv] lim by auto
-next
-  case MInf
-  then show ?thesis using Limsup_MInfty[OF ntriv] lim by auto
-next
-  case (real r)
-  show "(f ---> f0) net"
-  proof (rule topological_tendstoI)
-    fix 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_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
-qed
-
-lemma ereal_Liminf_eq_Limsup_iff:
-  fixes f :: "'a \<Rightarrow> ereal"
-  assumes "\<not> trivial_limit net"
-  shows "(f ---> f0) net \<longleftrightarrow> Liminf net f = f0 \<and> Limsup net f = f0"
-  by (metis assms ereal_Liminf_eq_Limsup lim_imp_Liminf lim_imp_Limsup)
+  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto
 
 lemma convergent_ereal:
-  fixes X :: "nat \<Rightarrow> ereal"
+  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   shows "convergent X \<longleftrightarrow> limsup X = liminf X"
-  using ereal_Liminf_eq_Limsup_iff[of sequentially]
+  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   by (auto simp: convergent_def)
 
-lemma limsup_INFI_SUPR:
-  fixes f :: "nat \<Rightarrow> ereal"
-  shows "limsup f = (INF n. SUP m:{n..}. f m)"
-  using ereal_Limsup_uminus[of sequentially "\<lambda>x. - f x"]
-  by (simp add: liminf_SUPR_INFI ereal_INFI_uminus ereal_SUPR_uminus)
-
 lemma liminf_PInfty:
-  fixes X :: "nat => ereal"
-  shows "X ----> \<infinity> <-> liminf X = \<infinity>"
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
   by (metis Liminf_PInfty trivial_limit_sequentially)
 
 lemma limsup_MInfty:
-  fixes X :: "nat => ereal"
-  shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)"
+  fixes X :: "nat \<Rightarrow> ereal"
+  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   by (metis Limsup_MInfty trivial_limit_sequentially)
 
 lemma ereal_lim_mono:
-  fixes X Y :: "nat => ereal"
+  fixes X Y :: "nat => 'a::linorder_topology"
   assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
     and "X ----> x" "Y ----> y"
   shows "x <= y"
   using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
 
 lemma incseq_le_ereal:
-  fixes X :: "nat \<Rightarrow> ereal"
+  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
   assumes inc: "incseq X" and lim: "X ----> L"
   shows "X N \<le> L"
   using inc by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
 
 lemma decseq_ge_ereal:
   assumes dec: "decseq X"
-    and lim: "X ----> (L::ereal)"
+    and lim: "X ----> (L::'a::linorder_topology)"
   shows "X N >= L"
   using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
 
-lemma liminf_bounded_open:
-  fixes x :: "nat \<Rightarrow> ereal"
-  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
-  (is "_ \<longleftrightarrow> ?P x0")
-proof
-  assume "?P x0"
-  then show "x0 \<le> liminf x"
-    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
-    by (intro complete_lattice_class.Sup_upper) auto
-next
-  assume "x0 \<le> liminf x"
-  { fix S :: "ereal set"
-    assume om: "open S & mono_set S & x0:S"
-    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
-    moreover
-    { assume "~(S=UNIV)"
-      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
-      then have "B<x0" using om by auto
-      then have "EX N. ALL n>=N. x n : S"
-        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
-    }
-    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
-  }
-  then show "?P x0" by auto
-qed
-
-lemma limsup_subseq_mono:
-  fixes X :: "nat \<Rightarrow> ereal"
-  assumes "subseq r"
-  shows "limsup (X \<circ> r) \<le> limsup X"
-proof -
-  have "(\<lambda>n. - X n) \<circ> r = (\<lambda>n. - (X \<circ> r) n)" by (simp add: fun_eq_iff)
-  then have "- limsup X \<le> - limsup (X \<circ> r)"
-     using liminf_subseq_mono[of r "(%n. - X n)"]
-       ereal_Liminf_uminus[of sequentially X]
-       ereal_Liminf_uminus[of sequentially "X o r"] assms by auto
-  then show ?thesis by auto
-qed
-
 lemma bounded_abs:
   assumes "(a::real)<=x" "x<=b"
   shows "abs x <= max (abs a) (abs b)"
   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 lim_ereal_increasing:
-  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 \<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:
-  fixes X :: "nat \<Rightarrow> ereal"
-  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
-proof -
-  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
-    using seq_monosub[of X] unfolding comp_def by auto
-  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
-    by (auto simp add: monoseq_def)
-  then obtain l where "(X\<circ>r) ----> l"
-     using lim_ereal_increasing[of "X \<circ> r"] lim_ereal_decreasing[of "X \<circ> r"] by auto
-  then show ?thesis using `subseq r` by auto
-qed
-
 lemma ereal_Sup_lim:
-  assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
+  assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})"
   shows "a \<le> Sup s"
   by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
 
 lemma ereal_Inf_lim:
-  assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
+  assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})"
   shows "Inf s \<le> a"
   by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
 
 lemma SUP_Lim_ereal:
   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
-  assumes inc: "incseq X" and l: "X ----> l"
-  shows "(SUP n. X n) = l"
+  assumes inc: "incseq X" and l: "X ----> l" shows "(SUP n. X n) = l"
   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_SUP[of "\<lambda>i. - X i"]
-  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
+lemma INF_Lim_ereal:
+  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
+  assumes dec: "decseq X" and l: "X ----> l" shows "(INF n. X n) = l"
+  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l] by simp
 
 lemma SUP_eq_LIMSEQ:
   assumes "mono f"
@@ -652,127 +409,6 @@
     show "f ----> x" by auto }
 qed
 
-lemma Liminf_within:
-  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 => '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 => _"
-  shows "Liminf (at x) f = Liminf (at x within UNIV) f"
-  by simp (* TODO: delete *)
-
-
-lemma Liminf_at:
-  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 => _"
-  shows "Limsup (at x) f = Limsup (at x within UNIV) f"
-  by simp (* TODO: delete *)
-
-
-lemma Limsup_at:
-  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
-
-lemma Lim_within_constant:
-  assumes "ALL y:S. f y = C"
-  shows "(f ---> C) (at x within S)"
-  unfolding tendsto_def Limits.eventually_within eventually_at_topological
-  using assms by simp (metis open_UNIV UNIV_I)
-
-lemma Liminf_within_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> ereal"
-  assumes "ALL y:S. f y = C"
-    and "~trivial_limit (at x within S)"
-  shows "Liminf (at x within S) f = C"
-  by (metis Lim_within_constant assms lim_imp_Liminf)
-
-lemma Limsup_within_constant:
-  fixes f :: "'a::topological_space \<Rightarrow> ereal"
-  assumes "ALL y:S. f y = C"
-    and "~trivial_limit (at x within S)"
-  shows "Limsup (at x within S) f = C"
-  by (metis Lim_within_constant assms lim_imp_Limsup)
-
-lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
-  unfolding islimpt_def by blast
-
-
-lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
-  unfolding closure_def using islimpt_punctured by blast
-
-
-lemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))"
-  using islimpt_in_closure by (metis trivial_limit_within)
-
-
-lemma not_trivial_limit_within_ball:
-  "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"
-  (is "?lhs = ?rhs")
-proof -
-  { assume "?lhs"
-    { fix e :: real
-      assume "e>0"
-      then obtain y where "y:(S-{x}) & dist y x < e"
-        using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
-        by auto
-      then have "y : (S Int ball x e - {x})"
-        unfolding ball_def by (simp add: dist_commute)
-      then have "S Int ball x e - {x} ~= {}" by blast
-    } then have "?rhs" by auto
-  }
-  moreover
-  { assume "?rhs"
-    { fix e :: real
-      assume "e>0"
-      then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
-      then have "y:(S-{x}) & dist y x < e"
-        unfolding ball_def by (simp add: dist_commute)
-      then have "EX y:(S-{x}). dist y x < e" by auto
-    }
-    then have "?lhs"
-      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
-  }
-  ultimately show ?thesis by auto
-qed
-
 lemma liminf_ereal_cminus:
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "c \<noteq> -\<infinity>"
@@ -794,43 +430,6 @@
 
 subsubsection {* Continuity *}
 
-lemma continuous_imp_tendsto:
-  assumes "continuous (at x0) f"
-    and "x ----> x0"
-  shows "(f o x) ----> (f x0)"
-proof -
-  { fix S
-    assume "open S & (f x0):S"
-    then obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"
-       using assms continuous_at_open by metis
-    then have "(EX N. ALL n>=N. x n : T)"
-      using assms tendsto_explicit T_def by auto
-    then have "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto
-  }
-  then show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto
-qed
-
-
-lemma continuous_at_sequentially2:
-  fixes f :: "'a::metric_space => 'b:: topological_space"
-  shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"
-proof -
-  { assume "~(continuous (at x0) f)"
-    then obtain T where
-      T_def: "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"
-      using continuous_at_open[of x0 f] by metis
-    def X == "{x'. f x' ~: T}"
-    then have "x0 islimpt X"
-      unfolding islimpt_def using T_def by auto
-    then obtain x where x_def: "(ALL n. x n : X) & x ----> x0"
-      using islimpt_sequential[of x0 X] by auto
-    then have "~(f o x) ----> (f x0)"
-      unfolding tendsto_explicit using X_def T_def by auto
-    then have "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto
-  }
-  then show ?thesis using continuous_imp_tendsto by auto
-qed
-
 lemma continuous_at_of_ereal:
   fixes x0 :: ereal
   assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
@@ -916,35 +515,6 @@
   unfolding continuous_at_open using assms t1_space by auto
 
 
-lemma closure_contains_Inf:
-  fixes S :: "real set"
-  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
-  shows "Inf S : closure S"
-proof -
-  have *: "ALL x:S. Inf S <= x"
-    using Inf_lower_EX[of _ S] assms by metis
-  { fix e
-    assume "e>(0 :: real)"
-    then obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto
-    moreover then have "x > Inf S - e" using * by auto
-    ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
-    then have "EX x:S. abs (x - Inf S) < e" using x_def by auto
-  }
-  then show ?thesis
-    apply (subst closure_approachable)
-    unfolding dist_norm apply auto
-    done
-qed
-
-
-lemma closed_contains_Inf:
-  fixes S :: "real set"
-  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
-    and "closed S"
-  shows "Inf S : S"
-  by (metis closure_contains_Inf closure_closed assms)
-
-
 lemma mono_closed_real:
   fixes S :: "real set"
   assumes mono: "ALL y z. y:S & y<=z --> z:S"
@@ -1317,4 +887,205 @@
   then show "\<forall>i. f i = 0" by auto
 qed simp
 
+lemma Liminf_within:
+  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 => '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_at:
+  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_at:
+  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
+
+lemma min_Liminf_at:
+  fixes f :: "'a::metric_space => 'b::complete_linorder"
+  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
+  unfolding inf_min[symmetric] Liminf_at
+  apply (subst inf_commute)
+  apply (subst SUP_inf)
+  apply (intro SUP_cong[OF refl])
+  apply (cut_tac A="ball x b - {x}" and B="{x}" and M=f in INF_union)
+  apply (simp add: INF_def del: inf_ereal_def)
+  done
+
+subsection {* monoset *}
+
+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 ereal_open_mono_set:
+  fixes S :: "ereal set"
+  shows "(open S \<and> mono_set S) \<longleftrightarrow> (S = UNIV \<or> S = {Inf S <..})"
+  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
+    ereal_open_closed mono_set_iff open_ereal_greaterThan)
+
+lemma ereal_closed_mono_set:
+  fixes S :: "ereal set"
+  shows "(closed S \<and> mono_set S) \<longleftrightarrow> (S = {} \<or> S = {Inf S ..})"
+  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
+    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)
+
+lemma ereal_Liminf_Sup_monoset:
+  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}"
+    (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 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 dense_le)
+    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}"
+    (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 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 dense_ge)
+    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 liminf_bounded_open:
+  fixes x :: "nat \<Rightarrow> ereal"
+  shows "x0 \<le> liminf x \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> x0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. x n \<in> S))"
+  (is "_ \<longleftrightarrow> ?P x0")
+proof
+  assume "?P x0"
+  then show "x0 \<le> liminf x"
+    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
+    by (intro complete_lattice_class.Sup_upper) auto
+next
+  assume "x0 \<le> liminf x"
+  { fix S :: "ereal set"
+    assume om: "open S & mono_set S & x0:S"
+    { assume "S = UNIV" then have "EX N. (ALL n>=N. x n : S)" by auto }
+    moreover
+    { assume "~(S=UNIV)"
+      then obtain B where B_def: "S = {B<..}" using om ereal_open_mono_set by auto
+      then have "B<x0" using om by auto
+      then have "EX N. ALL n>=N. x n : S"
+        unfolding B_def using `x0 \<le> liminf x` liminf_bounded_iff by auto
+    }
+    ultimately have "EX N. (ALL n>=N. x n : S)" by auto
+  }
+  then show "?P x0" by auto
+qed
+
 end
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -48,6 +48,11 @@
     and "\<And>r x. f (r *\<^sub>R x) = r *\<^sub>R f x" "\<And>x. norm (f x) \<le> norm x * K"
   shows "bounded_linear f"
   unfolding bounded_linear_def additive_def bounded_linear_axioms_def using assms by auto
+
+lemma Inf: (* rename *)
+  fixes S :: "real set"
+  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
+by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
  
 lemma real_le_inf_subset:
   assumes "t \<noteq> {}" "t \<subseteq> s" "\<exists>b. b <=* s"
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -28,12 +28,7 @@
 lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s o r) ----> l"
   by (rule LIMSEQ_subseq_LIMSEQ)
 
-(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
-lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
-  apply (frule isGlb_isLb)
-  apply (frule_tac x = y in isGlb_isLb)
-  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
-  done
+lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
 
 lemma countable_PiE: 
   "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
@@ -45,9 +40,10 @@
 begin
 
 definition "topological_basis B =
-  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
-
-lemma "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x))"
+  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x)))"
+
+lemma topological_basis:
+  "topological_basis B = (\<forall>x. open x \<longleftrightarrow> (\<exists>B'. B' \<subseteq> B \<and> \<Union>B' = x))"
   unfolding topological_basis_def
   apply safe
      apply fastforce
@@ -105,6 +101,19 @@
   using assms
   by (simp add: topological_basis_def)
 
+lemma topological_basis_imp_subbasis:
+  assumes B: "topological_basis B" shows "open = generate_topology B"
+proof (intro ext iffI)
+  fix S :: "'a set" assume "open S"
+  with B obtain B' where "B' \<subseteq> B" "S = \<Union>B'"
+    unfolding topological_basis_def by blast
+  then show "generate_topology B S"
+    by (auto intro: generate_topology.intros dest: topological_basis_open)
+next
+  fix S :: "'a set" assume "generate_topology B S" then show "open S"
+    by induct (auto dest: topological_basis_open[OF B])
+qed
+
 lemma basis_dense:
   fixes B::"'a set set" and f::"'a set \<Rightarrow> 'a"
   assumes "topological_basis B"
@@ -236,6 +245,70 @@
   qed
 qed
 
+
+lemma countable_basis:
+  obtains A :: "nat \<Rightarrow> 'a::first_countable_topology set" where
+    "\<And>i. open (A i)" "\<And>i. x \<in> A i"
+    "\<And>F. (\<forall>n. F n \<in> A n) \<Longrightarrow> F ----> x"
+proof atomize_elim
+  from countable_basis_at_decseq[of x] guess A . note A = this
+  { fix F S assume "\<forall>n. F n \<in> A n" "open S" "x \<in> S"
+    with A(3)[of S] have "eventually (\<lambda>n. F n \<in> S) sequentially"
+      by (auto elim: eventually_elim1 simp: subset_eq) }
+  with A show "\<exists>A. (\<forall>i. open (A i)) \<and> (\<forall>i. x \<in> A i) \<and> (\<forall>F. (\<forall>n. F n \<in> A n) \<longrightarrow> F ----> x)"
+    by (intro exI[of _ A]) (auto simp: tendsto_def)
+qed
+
+lemma sequentially_imp_eventually_nhds_within:
+  fixes a :: "'a::first_countable_topology"
+  assumes "\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially"
+  shows "eventually P (nhds a within s)"
+proof (rule ccontr)
+  from countable_basis[of a] guess A . note A = this
+  assume "\<not> eventually P (nhds a within s)"
+  with A have P: "\<exists>F. \<forall>n. F n \<in> s \<and> F n \<in> A n \<and> \<not> P (F n)"
+    unfolding Limits.eventually_within eventually_nhds by (intro choice) fastforce
+  then guess F ..
+  hence F0: "\<forall>n. F n \<in> s" and F2: "\<forall>n. F n \<in> A n" and F3: "\<forall>n. \<not> P (F n)"
+    by fast+
+  with A have "F ----> a" by auto
+  hence "eventually (\<lambda>n. P (F n)) sequentially"
+    using assms F0 by simp
+  thus "False" by (simp add: F3)
+qed
+
+lemma eventually_nhds_within_iff_sequentially:
+  fixes a :: "'a::first_countable_topology"
+  shows "eventually P (nhds a within s) \<longleftrightarrow> 
+    (\<forall>f. (\<forall>n. f n \<in> s) \<and> f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
+proof (safe intro!: sequentially_imp_eventually_nhds_within)
+  assume "eventually P (nhds a within s)" 
+  then obtain S where "open S" "a \<in> S" "\<forall>x\<in>S. x \<in> s \<longrightarrow> P x"
+    by (auto simp: Limits.eventually_within eventually_nhds)
+  moreover fix f assume "\<forall>n. f n \<in> s" "f ----> a"
+  ultimately show "eventually (\<lambda>n. P (f n)) sequentially"
+    by (auto dest!: topological_tendstoD elim: eventually_elim1)
+qed
+
+lemma eventually_nhds_iff_sequentially:
+  fixes a :: "'a::first_countable_topology"
+  shows "eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f ----> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
+  using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
+
+lemma not_eventually_sequentiallyD:
+  assumes P: "\<not> eventually P sequentially"
+  shows "\<exists>r. subseq r \<and> (\<forall>n. \<not> P (r n))"
+proof -
+  from P have "\<forall>n. \<exists>m\<ge>n. \<not> P m"
+    unfolding eventually_sequentially by (simp add: not_less)
+  then obtain r where "\<And>n. r n \<ge> n" "\<And>n. \<not> P (r n)"
+    by (auto simp: choice_iff)
+  then show ?thesis
+    by (auto intro!: exI[of _ "\<lambda>n. r (((Suc \<circ> r) ^^ Suc n) 0)"]
+             simp: less_eq_Suc_le subseq_Suc_iff)
+qed
+
+
 instance prod :: (first_countable_topology, first_countable_topology) first_countable_topology
 proof
   fix x :: "'a \<times> 'b"
@@ -274,11 +347,56 @@
 qed
 
 class second_countable_topology = topological_space +
-  assumes ex_countable_basis:
-    "\<exists>B::'a::topological_space set set. countable B \<and> topological_basis B"
-
-sublocale second_countable_topology < countable_basis "SOME B. countable B \<and> topological_basis B"
-  using someI_ex[OF ex_countable_basis] by unfold_locales safe
+  assumes ex_countable_subbasis: "\<exists>B::'a::topological_space set set. countable B \<and> open = generate_topology B"
+begin
+
+lemma ex_countable_basis: "\<exists>B::'a set set. countable B \<and> topological_basis B"
+proof -
+  from ex_countable_subbasis obtain B where B: "countable B" "open = generate_topology B" by blast
+  let ?B = "Inter ` {b. finite b \<and> b \<subseteq> B }"
+
+  show ?thesis
+  proof (intro exI conjI)
+    show "countable ?B"
+      by (intro countable_image countable_Collect_finite_subset B)
+    { fix S assume "open S"
+      then have "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. (\<Union>b\<in>B'. \<Inter>b) = S"
+        unfolding B
+      proof induct
+        case UNIV show ?case by (intro exI[of _ "{{}}"]) simp
+      next
+        case (Int a b)
+        then obtain x y where x: "a = UNION x Inter" "\<And>i. i \<in> x \<Longrightarrow> finite i \<and> i \<subseteq> B"
+          and y: "b = UNION y Inter" "\<And>i. i \<in> y \<Longrightarrow> finite i \<and> i \<subseteq> B"
+          by blast
+        show ?case
+          unfolding x y Int_UN_distrib2
+          by (intro exI[of _ "{i \<union> j| i j.  i \<in> x \<and> j \<in> y}"]) (auto dest: x(2) y(2))
+      next
+        case (UN K)
+        then have "\<forall>k\<in>K. \<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = k" by auto
+        then guess k unfolding bchoice_iff ..
+        then show "\<exists>B'\<subseteq>{b. finite b \<and> b \<subseteq> B}. UNION B' Inter = \<Union>K"
+          by (intro exI[of _ "UNION K k"]) auto
+      next
+        case (Basis S) then show ?case
+          by (intro exI[of _ "{{S}}"]) auto
+      qed
+      then have "(\<exists>B'\<subseteq>Inter ` {b. finite b \<and> b \<subseteq> B}. \<Union>B' = S)"
+        unfolding subset_image_iff by blast }
+    then show "topological_basis ?B"
+      unfolding topological_space_class.topological_basis_def
+      by (safe intro!: topological_space_class.open_Inter) 
+         (simp_all add: B generate_topology.Basis subset_eq)
+  qed
+qed
+
+end
+
+sublocale second_countable_topology <
+  countable_basis "SOME B. countable B \<and> topological_basis B"
+  using someI_ex[OF ex_countable_basis]
+  by unfold_locales safe
 
 instance prod :: (second_countable_topology, second_countable_topology) second_countable_topology
 proof
@@ -287,8 +405,9 @@
   moreover
   obtain B :: "'b set set" where "countable B" "topological_basis B"
     using ex_countable_basis by auto
-  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> topological_basis B"
-    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod)
+  ultimately show "\<exists>B::('a \<times> 'b) set set. countable B \<and> open = generate_topology B"
+    by (auto intro!: exI[of _ "(\<lambda>(a, b). a \<times> b) ` (A \<times> B)"] topological_basis_prod
+      topological_basis_imp_subbasis)
 qed
 
 instance second_countable_topology \<subseteq> first_countable_topology
@@ -837,6 +956,9 @@
 lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
   unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
 
+lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
+  unfolding islimpt_def by blast
+
 text {* A perfect space has no isolated points. *}
 
 lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV"
@@ -1120,6 +1242,10 @@
 qed
 
 
+lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
+  unfolding closure_def using islimpt_punctured by blast
+
+
 subsection {* Frontier (aka boundary) *}
 
 definition "frontier S = closure S - interior S"
@@ -1209,6 +1335,9 @@
   apply (drule_tac x=UNIV in spec, simp)
   done
 
+lemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))"
+  using islimpt_in_closure by (metis trivial_limit_within)
+
 text {* Some property holds "sufficiently close" to the limit point. *}
 
 lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
@@ -1698,6 +1827,62 @@
   shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
   by (metis closure_closed closure_approachable)
 
+lemma closure_contains_Inf:
+  fixes S :: "real set"
+  assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
+  shows "Inf S \<in> closure S"
+  unfolding closure_approachable
+proof safe
+  have *: "\<forall>x\<in>S. Inf S \<le> x"
+    using Inf_lower_EX[of _ S] assms by metis
+
+  fix e :: real assume "0 < e"
+  then obtain x where x: "x \<in> S" "x < Inf S + e"
+    using Inf_close `S \<noteq> {}` by auto
+  moreover then have "x > Inf S - e" using * by auto
+  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
+  then show "\<exists>x\<in>S. dist x (Inf S) < e"
+    using x by (auto simp: dist_norm)
+qed
+
+lemma closed_contains_Inf:
+  fixes S :: "real set"
+  assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
+    and "closed S"
+  shows "Inf S \<in> S"
+  by (metis closure_contains_Inf closure_closed assms)
+
+
+lemma not_trivial_limit_within_ball:
+  "(\<not> trivial_limit (at x within S)) = (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
+  (is "?lhs = ?rhs")
+proof -
+  { assume "?lhs"
+    { fix e :: real
+      assume "e>0"
+      then obtain y where "y:(S-{x}) & dist y x < e"
+        using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
+        by auto
+      then have "y : (S Int ball x e - {x})"
+        unfolding ball_def by (simp add: dist_commute)
+      then have "S Int ball x e - {x} ~= {}" by blast
+    } then have "?rhs" by auto
+  }
+  moreover
+  { assume "?rhs"
+    { fix e :: real
+      assume "e>0"
+      then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
+      then have "y:(S-{x}) & dist y x < e"
+        unfolding ball_def by (simp add: dist_commute)
+      then have "EX y:(S-{x}). dist y x < e" by auto
+    }
+    then have "?lhs"
+      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
+  }
+  ultimately show ?thesis by auto
+qed
+
 subsection {* Infimum Distance *}
 
 definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
@@ -3715,6 +3900,7 @@
   using assms unfolding continuous_at continuous_within
   by (rule Lim_at_within)
 
+
 text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
 
 lemma continuous_within_eps_delta:
@@ -3982,6 +4168,15 @@
 lemma continuous_const: "continuous F (\<lambda>x. c)"
   unfolding continuous_def by (rule tendsto_const)
 
+lemma continuous_fst: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. fst (f x))"
+  unfolding continuous_def by (rule tendsto_fst)
+
+lemma continuous_snd: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. snd (f x))"
+  unfolding continuous_def by (rule tendsto_snd)
+
+lemma continuous_Pair: "continuous F f \<Longrightarrow> continuous F g \<Longrightarrow> continuous F (\<lambda>x. (f x, g x))"
+  unfolding continuous_def by (rule tendsto_Pair)
+
 lemma continuous_dist:
   assumes "continuous F f" and "continuous F g"
   shows "continuous F (\<lambda>x. dist (f x) (g x))"
@@ -4258,6 +4453,20 @@
 unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
 unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
 
+lemma continuous_imp_tendsto:
+  assumes "continuous (at x0) f" and "x ----> x0"
+  shows "(f \<circ> x) ----> (f x0)"
+proof (rule topological_tendstoI)
+  fix S
+  assume "open S" "f x0 \<in> S"
+  then obtain T where T_def: "open T" "x0 \<in> T" "\<forall>x\<in>T. f x \<in> S"
+     using assms continuous_at_open by metis
+  then have "eventually (\<lambda>n. x n \<in> T) sequentially"
+    using assms T_def by (auto simp: tendsto_def)
+  then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
+    using T_def by (auto elim!: eventually_elim1)
+qed
+
 lemma continuous_on_open:
   shows "continuous_on s f \<longleftrightarrow>
         (\<forall>t. openin (subtopology euclidean (f ` s)) t
@@ -4851,62 +5060,61 @@
   shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
   unfolding continuous_on_iff dist_norm by simp
 
-text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
-
 lemma compact_attains_sup:
-  fixes s :: "real set"
-  assumes "compact s"  "s \<noteq> {}"
-  shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
-proof-
-  from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
-  { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e"
-    have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
-    moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
-    ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto  }
-  thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
-    apply(rule_tac x="Sup s" in bexI) by auto
-qed
-
-lemma Inf:
-  fixes S :: "real set"
-  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
-by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
+  fixes S :: "'a::linorder_topology set"
+  assumes "compact S" "S \<noteq> {}"
+  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
+proof (rule classical)
+  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
+  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
+    by (metis not_le)
+  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
+    by auto
+  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
+    by (erule compactE_image)
+  with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
+    by (auto intro!: Max_in)
+  with C have "S \<subseteq> {..< Max (t`C)}"
+    by (auto intro: less_le_trans simp: subset_eq)
+  with t Max `C \<subseteq> S` show ?thesis
+    by fastforce
+qed
 
 lemma compact_attains_inf:
-  fixes s :: "real set"
-  assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
-proof-
-  from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
-  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s"  "Inf s \<notin> s"  "0 < e"
-      "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
-    have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
-    moreover
-    { fix x assume "x \<in> s"
-      hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
-      have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
-    hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
-    ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto  }
-  thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
-    apply(rule_tac x="Inf s" in bexI) by auto
+  fixes S :: "'a::linorder_topology set"
+  assumes "compact S" "S \<noteq> {}"
+  shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t"
+proof (rule classical)
+  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
+  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
+    by (metis not_le)
+  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
+    by auto
+  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
+    by (erule compactE_image)
+  with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
+    by (auto intro!: Min_in)
+  with C have "S \<subseteq> {Min (t`C) <..}"
+    by (auto intro: le_less_trans simp: subset_eq)
+  with t Min `C \<subseteq> S` show ?thesis
+    by fastforce
 qed
 
 lemma continuous_attains_sup:
-  fixes f :: "'a::topological_space \<Rightarrow> real"
-  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
-        ==> (\<exists>x \<in> s. \<forall>y \<in> s.  f y \<le> f x)"
-  using compact_attains_sup[of "f ` s"]
-  using compact_continuous_image[of s f] by auto
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
+  using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
 
 lemma continuous_attains_inf:
-  fixes f :: "'a::topological_space \<Rightarrow> real"
-  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f
-        \<Longrightarrow> (\<exists>x \<in> s. \<forall>y \<in> s. f x \<le> f y)"
-  using compact_attains_inf[of "f ` s"]
-  using compact_continuous_image[of s f] by auto
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
+  using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
+
+text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
 
 lemma distance_attains_sup:
   assumes "compact s" "s \<noteq> {}"
-  shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a y \<le> dist a x"
+  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
 proof (rule continuous_attains_sup [OF assms])
   { fix x assume "x\<in>s"
     have "(dist a ---> dist a x) (at x within s)"
@@ -4921,34 +5129,17 @@
 lemma distance_attains_inf:
   fixes a :: "'a::heine_borel"
   assumes "closed s"  "s \<noteq> {}"
-  shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a x \<le> dist a y"
+  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a x \<le> dist a y"
 proof-
-  from assms(2) obtain b where "b\<in>s" by auto
-  let ?B = "cball a (dist b a) \<inter> s"
-  have "b \<in> ?B" using `b\<in>s` by (simp add: dist_commute)
-  hence "?B \<noteq> {}" by auto
-  moreover
-  { fix x assume "x\<in>?B"
-    fix e::real assume "e>0"
-    { fix x' assume "x'\<in>?B" and as:"dist x' x < e"
-      from as have "\<bar>dist a x' - dist a x\<bar> < e"
-        unfolding abs_less_iff minus_diff_eq
-        using dist_triangle2 [of a x' x]
-        using dist_triangle [of a x x']
-        by arith
-    }
-    hence "\<exists>d>0. \<forall>x'\<in>?B. dist x' x < d \<longrightarrow> \<bar>dist a x' - dist a x\<bar> < e"
-      using `e>0` by auto
-  }
-  hence "continuous_on (cball a (dist b a) \<inter> s) (dist a)"
-    unfolding continuous_on Lim_within dist_norm real_norm_def
-    by fast
+  from assms(2) obtain b where "b \<in> s" by auto
+  let ?B = "s \<inter> cball a (dist b a)"
+  have "?B \<noteq> {}" using `b \<in> s` by (auto simp add: dist_commute)
+  moreover have "continuous_on ?B (dist a)"
+    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_at_id continuous_const)
   moreover have "compact ?B"
-    using compact_cball[of a "dist b a"]
-    unfolding compact_eq_bounded_closed
-    using bounded_Int and closed_Int and assms(1) by auto
-  ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y"
-    using continuous_attains_inf[of ?B "dist a"] by fastforce
+    by (intro closed_inter_compact `closed s` compact_cball)
+  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
+    by (metis continuous_attains_inf)
   thus ?thesis by fastforce
 qed
 
@@ -4985,11 +5176,43 @@
 apply (simp add: o_def)
 done
 
-text {* Generalize to @{class topological_space} *}
 lemma compact_Times: 
-  fixes s :: "'a::metric_space set" and t :: "'b::metric_space set"
-  shows "compact s \<Longrightarrow> compact t \<Longrightarrow> compact (s \<times> t)"
-  unfolding compact_eq_seq_compact_metric by (rule seq_compact_Times)
+  assumes "compact s" "compact t"
+  shows "compact (s \<times> t)"
+proof (rule compactI)
+  fix C assume C: "\<forall>t\<in>C. open t" "s \<times> t \<subseteq> \<Union>C"
+  have "\<forall>x\<in>s. \<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
+  proof
+    fix x assume "x \<in> s"
+    have "\<forall>y\<in>t. \<exists>a b c. c \<in> C \<and> open a \<and> open b \<and> x \<in> a \<and> y \<in> b \<and> a \<times> b \<subseteq> c" (is "\<forall>y\<in>t. ?P y")
+    proof 
+      fix y assume "y \<in> t"
+      with `x \<in> s` C obtain c where "c \<in> C" "(x, y) \<in> c" "open c" by auto
+      then show "?P y" by (auto elim!: open_prod_elim)
+    qed
+    then obtain a b c where b: "\<And>y. y \<in> t \<Longrightarrow> open (b y)"
+      and c: "\<And>y. y \<in> t \<Longrightarrow> c y \<in> C \<and> open (a y) \<and> open (b y) \<and> x \<in> a y \<and> y \<in> b y \<and> a y \<times> b y \<subseteq> c y"
+      by metis
+    then have "\<forall>y\<in>t. open (b y)" "t \<subseteq> (\<Union>y\<in>t. b y)" by auto
+    from compactE_image[OF `compact t` this] obtain D where "D \<subseteq> t" "finite D" "t \<subseteq> (\<Union>y\<in>D. b y)"
+      by auto
+    moreover with c have "(\<Inter>y\<in>D. a y) \<times> t \<subseteq> (\<Union>y\<in>D. c y)"
+      by (fastforce simp: subset_eq)
+    ultimately show "\<exists>a. open a \<and> x \<in> a \<and> (\<exists>d\<subseteq>C. finite d \<and> a \<times> t \<subseteq> \<Union>d)"
+      using c by (intro exI[of _ "c`D"] exI[of _ "\<Inter>a`D"] conjI) (auto intro!: open_INT)
+  qed
+  then obtain a d where a: "\<forall>x\<in>s. open (a x)" "s \<subseteq> (\<Union>x\<in>s. a x)"
+    and d: "\<And>x. x \<in> s \<Longrightarrow> d x \<subseteq> C \<and> finite (d x) \<and> a x \<times> t \<subseteq> \<Union>d x"
+    unfolding subset_eq UN_iff by metis
+  moreover from compactE_image[OF `compact s` a] obtain e where e: "e \<subseteq> s" "finite e"
+    and s: "s \<subseteq> (\<Union>x\<in>e. a x)" by auto
+  moreover
+  { from s have "s \<times> t \<subseteq> (\<Union>x\<in>e. a x \<times> t)" by auto
+    also have "\<dots> \<subseteq> (\<Union>x\<in>e. \<Union>d x)" using d `e \<subseteq> s` by (intro UN_mono) auto
+    finally have "s \<times> t \<subseteq> (\<Union>x\<in>e. \<Union>d x)" . }
+  ultimately show "\<exists>C'\<subseteq>C. finite C' \<and> s \<times> t \<subseteq> \<Union>C'"
+    by (intro exI[of _ "(\<Union>x\<in>e. d x)"]) (auto simp add: subset_eq)
+qed
 
 text{* Hence some useful properties follow quite easily. *}
 
@@ -5266,50 +5489,23 @@
 
 lemma separate_compact_closed:
   fixes s t :: "'a::heine_borel set"
-  assumes "compact s" and "closed t" and "s \<inter> t = {}"
+  assumes "compact s" and t: "closed t" "s \<inter> t = {}"
   shows "\<exists>d>0. \<forall>x\<in>s. \<forall>y\<in>t. d \<le> dist x y"
-proof - (* FIXME: long proof *)
-  let ?T = "\<Union>x\<in>s. { ball x (d / 2) | d. 0 < d \<and> (\<forall>y\<in>t. d \<le> dist x y) }"
-  note `compact s`
-  moreover have "\<forall>t\<in>?T. open t" by auto
-  moreover have "s \<subseteq> \<Union>?T"
-    apply auto
-    apply (rule rev_bexI, assumption)
-    apply (subgoal_tac "x \<notin> t")
-    apply (drule separate_point_closed [OF `closed t`])
-    apply clarify
-    apply (rule_tac x="ball x (d / 2)" in exI)
-    apply simp
-    apply fast
-    apply (cut_tac assms(3))
-    apply auto
-    done
-  ultimately obtain U where "U \<subseteq> ?T" and "finite U" and "s \<subseteq> \<Union>U"
-    by (rule compactE)
-  from `finite U` and `U \<subseteq> ?T` have "\<exists>d>0. \<forall>x\<in>\<Union>U. \<forall>y\<in>t. d \<le> dist x y"
-    apply (induct set: finite)
-    apply simp
-    apply (rule exI)
-    apply (rule zero_less_one)
-    apply clarsimp
-    apply (rename_tac y e)
-    apply (rule_tac x="min d (e / 2)" in exI)
-    apply simp
-    apply (subst ball_Un)
-    apply (rule conjI)
-    apply (intro ballI, rename_tac z)
-    apply (rule min_max.le_infI2)
-    apply (simp only: mem_ball)
-    apply (drule (1) bspec)
-    apply (cut_tac x=y and y=x and z=z in dist_triangle, arith)
-    apply simp
-    apply (intro ballI)
-    apply (rule min_max.le_infI1)
-    apply simp
-    done
-  with `s \<subseteq> \<Union>U` show ?thesis
-    by fast
-qed
+proof cases
+  assume "s \<noteq> {} \<and> t \<noteq> {}"
+  then have "s \<noteq> {}" "t \<noteq> {}" by auto
+  let ?inf = "\<lambda>x. infdist x t"
+  have "continuous_on s ?inf"
+    by (auto intro!: continuous_at_imp_continuous_on continuous_infdist continuous_at_id)
+  then obtain x where x: "x \<in> s" "\<forall>y\<in>s. ?inf x \<le> ?inf y"
+    using continuous_attains_inf[OF `compact s` `s \<noteq> {}`] by auto
+  then have "0 < ?inf x"
+    using t `t \<noteq> {}` in_closed_iff_infdist_zero by (auto simp: less_le infdist_nonneg)
+  moreover have "\<forall>x'\<in>s. \<forall>y\<in>t. ?inf x \<le> dist x' y"
+    using x by (auto intro: order_trans infdist_le)
+  ultimately show ?thesis
+    by auto
+qed (auto intro!: exI[of _ 1])
 
 lemma separate_closed_compact:
   fixes s t :: "'a::heine_borel set"
@@ -5711,9 +5907,6 @@
   then have b: "\<And>f. (\<Sum>i\<in>Basis. snd (f i) *\<^sub>R i) = b f" by simp
   def B \<equiv> "(\<lambda>f. box (a f) (b f)) ` (Basis \<rightarrow>\<^isub>E (\<rat> \<times> \<rat>))"
 
-  have "countable B" unfolding B_def 
-    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
-  moreover
   have "Ball B open" by (simp add: B_def open_box)
   moreover have "(\<forall>A. open A \<longrightarrow> (\<exists>B'\<subseteq>B. \<Union>B' = A))"
   proof safe
@@ -5725,7 +5918,12 @@
       done
   qed
   ultimately
-  show "\<exists>B::'a set set. countable B \<and> topological_basis B" unfolding topological_basis_def by blast
+  have "topological_basis B" unfolding topological_basis_def by blast
+  moreover
+  have "countable B" unfolding B_def 
+    by (intro countable_image countable_PiE finite_Basis countable_SIGMA countable_rat)
+  ultimately show "\<exists>B::'a set set. countable B \<and> open = generate_topology B"
+    by (blast intro: topological_basis_imp_subbasis)
 qed
 
 instance euclidean_space \<subseteq> polish_space ..
@@ -6543,129 +6741,37 @@
   fixes s :: "'a::metric_space set"
   assumes s:"compact s" "s \<noteq> {}" and gs:"(g ` s) \<subseteq> s"
       and dist:"\<forall>x\<in>s. \<forall>y\<in>s. x \<noteq> y \<longrightarrow> dist (g x) (g y) < dist x y"
-  shows "\<exists>! x\<in>s. g x = x"
-proof(cases "\<exists>x\<in>s. g x \<noteq> x")
-  obtain x where "x\<in>s" using s(2) by auto
-  case False hence g:"\<forall>x\<in>s. g x = x" by auto
-  { fix y assume "y\<in>s"
-    hence "x = y" using `x\<in>s` and dist[THEN bspec[where x=x], THEN bspec[where x=y]]
-      unfolding g[THEN bspec[where x=x], OF `x\<in>s`]
-      unfolding g[THEN bspec[where x=y], OF `y\<in>s`] by auto  }
-  thus ?thesis using `x\<in>s` and g by blast+
-next
-  case True
-  then obtain x where [simp]:"x\<in>s" and "g x \<noteq> x" by auto
-  { fix x y assume "x \<in> s" "y \<in> s"
-    hence "dist (g x) (g y) \<le> dist x y"
-      using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
-  def y \<equiv> "g x"
-  have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
-  def f \<equiv> "\<lambda>n. g ^^ n"
-  have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
-  have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
-  { fix n::nat and z assume "z\<in>s"
-    have "f n z \<in> s" unfolding f_def
-    proof(induct n)
-      case 0 thus ?case using `z\<in>s` by simp
-    next
-      case (Suc n) thus ?case using gs[unfolded image_subset_iff] by auto
-    qed } note fs = this
-  { fix m n ::nat assume "m\<le>n"
-    fix w z assume "w\<in>s" "z\<in>s"
-    have "dist (f n w) (f n z) \<le> dist (f m w) (f m z)" using `m\<le>n`
-    proof(induct n)
-      case 0 thus ?case by auto
-    next
-      case (Suc n)
-      thus ?case proof(cases "m\<le>n")
-        case True thus ?thesis using Suc(1)
-          using dist'[OF fs fs, OF `w\<in>s` `z\<in>s`, of n n] by auto
-      next
-        case False hence mn:"m = Suc n" using Suc(2) by simp
-        show ?thesis unfolding mn  by auto
-      qed
-    qed } note distf = this
-
-  def h \<equiv> "\<lambda>n. (f n x, f n y)"
-  let ?s2 = "s \<times> s"
-  obtain l r where "l\<in>?s2" and r:"subseq r" and lr:"((h \<circ> r) ---> l) sequentially"
-    using compact_Times [OF s(1) s(1), unfolded compact_def, THEN spec[where x=h]] unfolding  h_def
-    using fs[OF `x\<in>s`] and fs[OF `y\<in>s`] by blast
-  def a \<equiv> "fst l" def b \<equiv> "snd l"
-  have lab:"l = (a, b)" unfolding a_def b_def by simp
-  have [simp]:"a\<in>s" "b\<in>s" unfolding a_def b_def using `l\<in>?s2` by auto
-
-  have lima:"((fst \<circ> (h \<circ> r)) ---> a) sequentially"
-   and limb:"((snd \<circ> (h \<circ> r)) ---> b) sequentially"
-    using lr
-    unfolding o_def a_def b_def by (rule tendsto_intros)+
-
-  { fix n::nat
-    have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (\<bar>dist fx fy - dist a b\<bar> < dist a b - dist x y)" by auto
-
-    { assume as:"dist a b > dist (f n x) (f n y)"
-      then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
-        and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
-        using lima limb unfolding h_def LIMSEQ_def by (fastforce simp del: less_divide_eq_numeral1)
-      hence "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> < dist a b - dist (f n x) (f n y)"
-        apply -
-        apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
-        apply (drule_tac x="Na+Nb+n" in spec, drule mp, simp)
-        apply (drule (1) add_strict_mono, simp only: real_sum_of_halves)
-        apply (erule le_less_trans [rotated])
-        apply (erule thin_rl)
-        apply (rule abs_leI)
-        apply (simp add: diff_le_iff add_assoc)
-        apply (rule order_trans [OF dist_triangle add_left_mono])
-        apply (subst add_commute, rule dist_triangle2)
-        apply (simp add: diff_le_iff add_assoc)
-        apply (rule order_trans [OF dist_triangle3 add_left_mono])
-        apply (subst add_commute, rule dist_triangle)
-        done
-      moreover
-      have "\<bar>dist (f (r (Na + Nb + n)) x) (f (r (Na + Nb + n)) y) - dist a b\<bar> \<ge> dist a b - dist (f n x) (f n y)"
-        using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
-        using seq_suble[OF r, of "Na+Nb+n"]
-        using *[of "f (r (Na + Nb + n)) x" "f (r (Na + Nb + n)) y" "f n x" "f n y"] by auto
-      ultimately have False by simp
-    }
-    hence "dist a b \<le> dist (f n x) (f n y)" by(rule ccontr)auto }
-  note ab_fn = this
-
-  have [simp]:"a = b" proof(rule ccontr)
-    def e \<equiv> "dist a b - dist (g a) (g b)"
-    assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce
-    hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2"
-      using lima limb unfolding LIMSEQ_def
-      apply (auto elim!: allE[where x="e/2"]) apply(rename_tac N N', rule_tac x="r (max N N')" in exI) unfolding h_def by fastforce
-    then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto
-    have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a"
-      using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto
-    moreover have "dist (f (Suc n) y) (g b) \<le> dist (f n y) b"
-      using dist[THEN bspec[where x="f n y"], THEN bspec[where x="b"]] and fs by auto
-    ultimately have "dist (f (Suc n) x) (g a) + dist (f (Suc n) y) (g b) < e" using n by auto
-    thus False unfolding e_def using ab_fn[of "Suc n"]
-      using dist_triangle2 [of "f (Suc n) y" "g a" "g b"]
-      using dist_triangle2 [of "f (Suc n) x" "f (Suc n) y" "g a"]
-      by auto
+  shows "\<exists>!x\<in>s. g x = x"
+proof -
+  let ?D = "(\<lambda>x. (x, x)) ` s"
+  have D: "compact ?D" "?D \<noteq> {}"
+    by (rule compact_continuous_image)
+       (auto intro!: s continuous_Pair continuous_within_id simp: continuous_on_eq_continuous_within)
+
+  have "\<And>x y e. x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> 0 < e \<Longrightarrow> dist y x < e \<Longrightarrow> dist (g y) (g x) < e"
+    using dist by fastforce
+  then have "continuous_on s g"
+    unfolding continuous_on_iff by auto
+  then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
+    unfolding continuous_on_eq_continuous_within
+    by (intro continuous_dist ballI continuous_within_compose)
+       (auto intro!:  continuous_fst continuous_snd continuous_within_id simp: image_image)
+
+  obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
+    using continuous_attains_inf[OF D cont] by auto
+
+  have "g a = a"
+  proof (rule ccontr)
+    assume "g a \<noteq> a"
+    with `a \<in> s` gs have "dist (g (g a)) (g a) < dist (g a) a"
+      by (intro dist[rule_format]) auto
+    moreover have "dist (g a) a \<le> dist (g (g a)) (g a)"
+      using `a \<in> s` gs by (intro le) auto
+    ultimately show False by auto
   qed
-
-  have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto
-  { fix x y assume "x\<in>s" "y\<in>s" moreover
-    fix e::real assume "e>0" ultimately
-    have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastforce }
-  hence "continuous_on s g" unfolding continuous_on_iff by auto
-
-  hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially
-    apply (rule allE[where x="\<lambda>n. (fst \<circ> h \<circ> r) n"]) apply (erule ballE[where x=a])
-    using lima unfolding h_def o_def using fs[OF `x\<in>s`] by (auto simp add: y_def)
-  hence "g a = a" using tendsto_unique[OF trivial_limit_sequentially limb, of "g a"]
-    unfolding `a=b` and o_assoc by auto
-  moreover
-  { fix x assume "x\<in>s" "g x = x" "x\<noteq>a"
-    hence "False" using dist[THEN bspec[where x=a], THEN bspec[where x=x]]
-      using `g a = a` and `a\<in>s` by auto  }
-  ultimately show "\<exists>!x\<in>s. g x = x" using `a\<in>s` by blast
+  moreover have "\<And>x. x \<in> s \<Longrightarrow> g x = x \<Longrightarrow> x = a"
+    using dist[THEN bspec[where x=a]] `g a = a` and `a\<in>s` by auto
+  ultimately show "\<exists>!x\<in>s. g x = x" using `a \<in> s` by blast
 qed
 
 declare tendsto_const [intro] (* FIXME: move *)
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -1133,7 +1133,7 @@
   shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
 proof -
   have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
-    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
+    by (simp add: lim_def convergent_def convergent_limsup_cl)
   then show ?thesis
     by simp
 qed
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Discrete_Topology.thy
--- a/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -50,15 +50,13 @@
 
 instance discrete :: (countable) second_countable_topology
 proof
-  let ?B = "(range (\<lambda>n::nat. {from_nat n::'a discrete}))"
-  have "topological_basis ?B"
-  proof (intro topological_basisI)
-    fix x::"'a discrete" and O' assume "open O'" "x \<in> O'"
-    thus "\<exists>B'\<in>range (\<lambda>n. {from_nat n}). x \<in> B' \<and> B' \<subseteq> O'"
-      by (auto intro: exI[where x="to_nat x"])
-  qed (simp add: open_discrete_def)
+  let ?B = "range (\<lambda>n::'a discrete. {n})"
+  have "\<And>S. generate_topology ?B (\<Union>x\<in>S. {x})"
+    by (intro generate_topology_Union) (auto intro: generate_topology.intros)
+  then have "open = generate_topology ?B"
+    by (auto intro!: ext simp: open_discrete_def)
   moreover have "countable ?B" by simp
-  ultimately show "\<exists>B::'a discrete set set. countable B \<and> topological_basis B" by blast
+  ultimately show "\<exists>B::'a discrete set set. countable B \<and> open = generate_topology B" by blast
 qed
 
 instance discrete :: (countable) polish_space ..
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -605,7 +605,7 @@
   shows "open x"
   using finmap_topological_basis assms by (auto simp: topological_basis_def)
 
-instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap)
+instance proof qed (blast intro: finmap_topological_basis countable_basis_finmap topological_basis_imp_subbasis)
 
 end
 
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Infinite_Product_Measure.thy
--- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -303,7 +303,7 @@
       with `(\<Inter>i. A i) = {}` show False by auto
     qed
     ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
-      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
+      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (A i)"] by simp
   qed fact+
   then guess \<mu> .. note \<mu> = this
   show ?thesis
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -2190,7 +2190,7 @@
     using diff positive_integral_positive[of M]
     by (subst integral_eq_positive_integral[of _ M]) (auto simp: ereal_real integrable_def)
   then show ?lim_diff
-    using ereal_Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
+    using Liminf_eq_Limsup[OF trivial_limit_sequentially liminf_limsup_eq]
     by simp
 
   show ?lim
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -385,7 +385,7 @@
     finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
   ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
     by simp
-  with LIMSEQ_ereal_INFI[OF decseq_fA]
+  with LIMSEQ_INF[OF decseq_fA]
   show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
 qed
 
@@ -565,7 +565,7 @@
 lemma Lim_emeasure_decseq:
   assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
   shows "(\<lambda>i. emeasure M (A i)) ----> emeasure M (\<Inter>i. A i)"
-  using LIMSEQ_ereal_INFI[OF decseq_emeasure, OF A]
+  using LIMSEQ_INF[OF decseq_emeasure, OF A]
   using INF_emeasure_decseq[OF A fin] by simp
 
 lemma emeasure_subadditive:
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Probability/Projective_Limit.thy
--- a/src/HOL/Probability/Projective_Limit.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -515,7 +515,7 @@
       thus False using Z by simp
     qed
     ultimately show "(\<lambda>i. \<mu>G (Z i)) ----> 0"
-      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (Z i)"] by simp
+      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (Z i)"] by simp
   qed
   then guess \<mu> .. note \<mu> = this
   def f \<equiv> "finmap_of J B"
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Mar 05 17:07:36 2013 +0100
@@ -766,11 +766,10 @@
 fun effective_term_order ctxt atp =
   let val ord = Config.get ctxt term_order in
     if ord = smartN then
-      if atp = spassN then
-        {is_lpo = false, gen_weights = true, gen_prec = true, gen_simp = false}
-      else
-        {is_lpo = false, gen_weights = false, gen_prec = false,
+      let val is_spass = (atp = spassN orelse atp = spass_polyN) in
+        {is_lpo = false, gen_weights = is_spass, gen_prec = is_spass,
          gen_simp = false}
+      end
     else
       let val is_lpo = String.isSubstring lpoN ord in
         {is_lpo = is_lpo,
diff -r 45579fbe5a24 -r ef494f2288cf src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Tue Mar 05 11:37:01 2013 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Tue Mar 05 17:07:36 2013 +0100
@@ -535,7 +535,7 @@
   val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
   val cterms = map (Thm.cterm_of @{theory}) terms
   val start = Timing.start ()
-  val thm = sat.rawsat_thm @{context} cterms
+  val _ = sat.rawsat_thm @{context} cterms
 in
   (Timing.result start, ! sat.counter)
 end;