# HG changeset patch
# User hoelzl
# Date 1383641102 -3600
# Node ID c4159fe6fa46dda3bf3e09960e04d476f7f1c0f9
# Parent  326fd7103cb4d169d38e2c4c6ab09bf040eae4dc
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)

diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -7,7 +7,7 @@
 header {* Conditionally-complete Lattices *}
 
 theory Conditionally_Complete_Lattices
-imports Main Lubs
+imports Main
 begin
 
 lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
@@ -28,6 +28,12 @@
 lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
   by (auto simp: bdd_below_def)
 
+lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)"
+  by force
+
+lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)"
+  by force
+
 lemma bdd_above_empty [simp, intro]: "bdd_above {}"
   unfolding bdd_above_def by auto
 
@@ -298,6 +304,12 @@
 lemma cSUP_le_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f ` A) \<Longrightarrow> SUPR A f \<le> u \<longleftrightarrow> (\<forall>x\<in>A. f x \<le> u)"
   by (metis cSUP_least cSUP_upper assms order_trans)
 
+lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
+  by (metis cINF_lower less_le_trans)
+
+lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
+  by (metis cSUP_upper le_less_trans)
+
 lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
   by (metis INF_def cInf_insert assms empty_is_image image_insert)
 
@@ -347,11 +359,6 @@
 instance complete_lattice \<subseteq> conditionally_complete_lattice
   by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
 
-lemma isLub_cSup: 
-  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
-  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
-            intro!: setgeI cSup_upper cSup_least)
-
 lemma cSup_eq:
   fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
   assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
@@ -370,12 +377,6 @@
   assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
 qed (intro cInf_eq_non_empty assms)
 
-lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
-  by (metis cSup_least setle_def)
-
-lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
-  by (metis cInf_greatest setge_def)
-
 class conditionally_complete_linorder = conditionally_complete_lattice + linorder
 begin
 
@@ -386,6 +387,12 @@
 lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
   by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
 
+lemma cINF_less_iff: "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
+  unfolding INF_def using cInf_less_iff[of "f`A"] by auto
+
+lemma less_cSUP_iff: "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
+  unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
+
 lemma less_cSupE:
   assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
   by (metis cSup_least assms not_le that)
@@ -437,27 +444,6 @@
 lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
   using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
 
-lemma cSup_bounds:
-  fixes S :: "'a :: conditionally_complete_lattice set"
-  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
-  shows "a \<le> Sup S \<and> Sup S \<le> b"
-proof-
-  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
-  hence b: "Sup S \<le> b" using u 
-    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
-  from Se obtain y where y: "y \<in> S" by blast
-  from lub l have "a \<le> Sup S"
-    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
-       (metis le_iff_sup le_sup_iff y)
-  with b show ?thesis by blast
-qed
-
-lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
-  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
-
-lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
-  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
-
 lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
   by (auto intro!: cSup_eq_non_empty intro: dense_le)
 
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Hahn_Banach/Bounds.thy
--- a/src/HOL/Hahn_Banach/Bounds.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Hahn_Banach/Bounds.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -57,25 +57,7 @@
   finally show ?thesis .
 qed
 
-lemma lub_compat: "lub A x = isLub UNIV A x"
-proof -
-  have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
-    by (rule ext) (simp only: isUb_def)
-  then show ?thesis
-    by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
-qed
-
-lemma real_complete:
-  fixes A :: "real set"
-  assumes nonempty: "\<exists>a. a \<in> A"
-    and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
-  shows "\<exists>x. lub A x"
-proof -
-  from ex_upper have "\<exists>y. isUb UNIV A y"
-    unfolding isUb_def setle_def by blast
-  with nonempty have "\<exists>x. isLub UNIV A x"
-    by (rule reals_complete)
-  then show ?thesis by (simp only: lub_compat)
-qed
+lemma real_complete: "\<exists>a::real. a \<in> A \<Longrightarrow> \<exists>y. \<forall>a \<in> A. a \<le> y \<Longrightarrow> \<exists>x. lub A x"
+  by (intro exI[of _ "Sup A"]) (auto intro!: cSup_upper cSup_least simp: lub_def)
 
 end
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -131,17 +131,15 @@
 
   -- "A denotes the set of all left-most points of all the intervals ..."
   moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
-  ultimately have "\<exists>x. x\<in>A"
+  ultimately have "A \<noteq> {}"
   proof -
     have "(0::nat) \<in> \<nat>" by simp
-    moreover have "?g 0 = ?g 0" by simp
-    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
-    with Adef have "?g 0 \<in> A" by simp
-    thus ?thesis ..
+    with Adef show ?thesis
+      by blast
   qed
 
   -- "Now show that A is bounded above ..."
-  moreover have "\<exists>y. isUb (UNIV::real set) A y"
+  moreover have "bdd_above A"
   proof -
     {
       fix n
@@ -177,18 +175,11 @@
       obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
     ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
     with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
-    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
-    hence "A *<= b" by (unfold setle_def)
-    moreover have "b \<in> (UNIV::real set)" by simp
-    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
-    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
-    thus ?thesis by auto
+    with Adef show "bdd_above A" by auto
   qed
-  -- "by the Axiom Of Completeness, A has a least upper bound ..."
-  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
 
   -- "denote this least upper bound as t ..."
-  then obtain t where tdef: "isLub UNIV A t" ..
+  def tdef: t == "Sup A"
 
   -- "and finally show that this least upper bound is in all the intervals..."
   have "\<forall>n. t \<in> f n"
@@ -229,82 +220,76 @@
         with Adef have "(?g n) \<in> A" by auto
         ultimately show ?thesis by simp
       qed 
-      with tdef show "a \<le> t" by (rule isLubD2)
+      with `bdd_above A` show "a \<le> t"
+        unfolding tdef by (intro cSup_upper)
     qed
     moreover have "t \<le> b"
-    proof -
-      have "isUb UNIV A b"
-      proof -
+      unfolding tdef
+    proof (rule cSup_least)
+      {
+        from alb int have
+          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
+        
+        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
+        proof (rule allI, induct_tac m)
+          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
+        next
+          fix m n
+          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
+          {
+            fix p
+            from pp have "f (p + n) \<subseteq> f p" by simp
+            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
+            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
+            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
+          }
+          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
+        qed 
+        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
+        proof ((rule allI)+, rule impI)
+          fix \<alpha>::nat and \<beta>::nat
+          assume "\<beta> \<le> \<alpha>"
+          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
+          then obtain k where "\<alpha> = \<beta> + k" ..
+          moreover
+          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
+          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
+        qed 
+        
+        fix m   
         {
-          from alb int have
-            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
-          
-          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
-          proof (rule allI, induct_tac m)
-            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
-          next
-            fix m n
-            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
-            {
-              fix p
-              from pp have "f (p + n) \<subseteq> f p" by simp
-              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
-              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
-              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
-            }
-            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
-          qed 
-          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
-          proof ((rule allI)+, rule impI)
-            fix \<alpha>::nat and \<beta>::nat
-            assume "\<beta> \<le> \<alpha>"
-            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
-            then obtain k where "\<alpha> = \<beta> + k" ..
-            moreover
-            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
-            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
-          qed 
-          
-          fix m   
-          {
-            assume "m \<ge> n"
-            with subsetm have "f m \<subseteq> f n" by simp
-            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
-            moreover
-            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
-            ultimately have "?g m \<le> b" by auto
-          }
+          assume "m \<ge> n"
+          with subsetm have "f m \<subseteq> f n" by simp
+          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
           moreover
-          {
-            assume "\<not>(m \<ge> n)"
-            hence "m < n" by simp
-            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
-            from closed obtain ma and mb where
-              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
-            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
-            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
-            moreover have "(?g m) = ma"
-            proof -
-              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
-              moreover from one have
-                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
-                by (rule closed_int_least)
-              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
-              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
-              thus "?g m = ma" by auto
-            qed
-            ultimately have "?g m \<le> b" by simp
-          } 
-          ultimately have "?g m \<le> b" by (rule case_split)
+          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
+          ultimately have "?g m \<le> b" by auto
         }
-        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
-        hence "A *<= b" by (unfold setle_def)
-        moreover have "b \<in> (UNIV::real set)" by simp
-        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
-        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
-      qed
-      with tdef show "t \<le> b" by (rule isLub_le_isUb)
-    qed
+        moreover
+        {
+          assume "\<not>(m \<ge> n)"
+          hence "m < n" by simp
+          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
+          from closed obtain ma and mb where
+            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
+          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
+          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
+          moreover have "(?g m) = ma"
+          proof -
+            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
+            moreover from one have
+              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
+              by (rule closed_int_least)
+            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
+            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
+            thus "?g m = ma" by auto
+          qed
+          ultimately have "?g m \<le> b" by simp
+        } 
+        ultimately have "?g m \<le> b" by (rule case_split)
+      }
+      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
+    qed fact
     ultimately have "t \<in> closed_int a b" by (rule closed_mem)
     with int show "t \<in> f n" by simp
   qed
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -451,7 +451,7 @@
 
 definition
   dist_fps_def: "dist (a::'a fps) b =
-    (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
+    (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
 
 lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
   by (simp add: dist_fps_def)
@@ -467,34 +467,6 @@
 
 end
 
-lemma fps_nonzero_least_unique:
-  assumes a0: "a \<noteq> 0"
-  shows "\<exists>!n. leastP (\<lambda>n. a$n \<noteq> 0) n"
-proof -
-  from fps_nonzero_nth_minimal [of a] a0
-  obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast
-  then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n"
-    by (auto simp add: leastP_def setge_def not_le [symmetric])
-  moreover
-  {
-    fix m
-    assume "leastP (\<lambda>n. a $ n \<noteq> 0) m"
-    then have "m = n" using ln
-      apply (auto simp add: leastP_def setge_def)
-      apply (erule allE[where x=n])
-      apply (erule allE[where x=m])
-      apply simp
-      done
-  }
-  ultimately show ?thesis by blast
-qed
-
-lemma fps_eq_least_unique:
-  assumes "(a::('a::ab_group_add) fps) \<noteq> b"
-  shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
-  using fps_nonzero_least_unique[of "a - b"] assms
-  by auto
-
 instantiation fps :: (comm_ring_1) metric_space
 begin
 
@@ -540,31 +512,15 @@
   moreover
   {
     assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
-    let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
-    from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac]
-      fps_eq_least_unique[OF bc]
-    obtain nab nac nbc where nab: "leastP (?P a b) nab"
-      and nac: "leastP (?P a c) nac"
-      and nbc: "leastP (?P b c) nbc" by blast
-    from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab"
-      by (auto simp add: leastP_def setge_def)
-    from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac"
-      by (auto simp add: leastP_def setge_def)
-    from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc"
-      by (auto simp add: leastP_def setge_def)
-
-    have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
-      by (simp add: fps_eq_iff)
-    from ab ac bc nab nac nbc
-    have dab: "dist a b = inverse (2 ^ nab)"
-      and dac: "dist a c = inverse (2 ^ nac)"
-      and dbc: "dist b c = inverse (2 ^ nbc)"
-      unfolding th0
-      apply (simp_all add: dist_fps_def)
-      apply (erule the1_equality[OF fps_eq_least_unique[OF ab]])
-      apply (erule the1_equality[OF fps_eq_least_unique[OF ac]])
-      apply (erule the1_equality[OF fps_eq_least_unique[OF bc]])
-      done
+    def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n"
+    then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m"
+      by (auto dest: not_less_Least)
+
+    from ab ac bc
+    have dab: "dist a b = inverse (2 ^ n a b)"
+      and dac: "dist a c = inverse (2 ^ n a c)"
+      and dbc: "dist b c = inverse (2 ^ n b c)"
+      by (simp_all add: dist_fps_def n_def fps_eq_iff)
     from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
       unfolding th by simp_all
     from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0"
@@ -575,11 +531,13 @@
       assume h: "dist a b > dist a c + dist b c"
       then have gt: "dist a b > dist a c" "dist a b > dist b c"
         using pos by auto
-      from gt have gtn: "nab < nbc" "nab < nac"
+      from gt have gtn: "n a b < n b c" "n a b < n a c"
         unfolding dab dbc dac by (auto simp add: th1)
-      from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)]
-      have "a $ nab = b $ nab" by simp
-      with nab'(2) have False  by simp
+      from n'[OF gtn(2)] n'(1)[OF gtn(1)]
+      have "a $ n a b = b $ n a b" by simp
+      moreover have "a $ n a b \<noteq> b $ n a b"
+         unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff)
+      ultimately have False by contradiction
     }
     then have "dist a b \<le> dist a c + dist b c"
       by (auto simp add: not_le[symmetric])
@@ -649,17 +607,12 @@
       moreover
       {
         assume neq: "?s n \<noteq> a"
-        from fps_eq_least_unique[OF neq]
-        obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast
-        have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
-          by (simp add: fps_eq_iff)
+        def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i"
         from neq have dth: "dist (?s n) a = (1/2)^k"
-          unfolding th0 dist_fps_def
-          unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k]
-          by (auto simp add: inverse_eq_divide power_divide)
-
-        from k have kn: "k > n"
-          by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
+          by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
+
+        from neq have kn: "k > n"
+          by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
         then have "dist (?s n) a < (1/2)^n" unfolding dth
           by (auto intro: power_strict_decreasing)
         also have "\<dots> <= (1/2)^n0" using nn0
@@ -3797,20 +3750,14 @@
   assumes "dist f g < inverse (2 ^ i)"
     and"j \<le> i"
   shows "f $ j = g $ j"
-proof (cases "f = g")
-  case False
-  hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
-  with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
+proof (rule ccontr)
+  assume "f $ j \<noteq> g $ j"
+  then have "\<exists>n. f $ n \<noteq> g $ n" by auto
+  with assms have "i < (LEAST n. f $ n \<noteq> g $ n)"
     by (simp add: split_if_asm dist_fps_def)
-  moreover
-  from fps_eq_least_unique[OF `f \<noteq> g`]
-  obtain n where n: "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
-  moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
-    by (auto simp add: leastP_def setge_def)
-  ultimately show ?thesis using `j \<le> i` by simp
-next
-  case True
-  then show ?thesis by simp
+  also have "\<dots> \<le> j"
+    using `f $ j \<noteq> g $ j` by (auto intro: Least_le)
+  finally show False using `j \<le> i` by simp
 qed
 
 lemma nth_equal_imp_dist_less:
@@ -3819,18 +3766,13 @@
 proof (cases "f = g")
   case False
   hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
-  with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
+  with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))"
     by (simp add: split_if_asm dist_fps_def)
   moreover
-  from fps_eq_least_unique[OF `f \<noteq> g`]
-  obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
-  with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
-    by (metis (full_types) leastPD1 not_le)
+  from assms `\<exists>n. f $ n \<noteq> g $ n` have "i < (LEAST n. f $ n \<noteq> g $ n)"
+    by (metis (mono_tags) LeastI not_less)
   ultimately show ?thesis by simp
-next
-  case True
-  then show ?thesis by simp
-qed
+qed simp
 
 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
   using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Library/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -156,28 +156,11 @@
 text{* An alternative useful formulation of completeness of the reals *}
 lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
   shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
-proof-
-  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
-  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
-  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
-    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
-  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
-    by blast
-  from Y[OF x] have xY: "x < Y" .
-  from L have L': "\<forall>x. P x \<longrightarrow> x \<le> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
-  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
-    apply (clarsimp, atomize (full)) by auto
-  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
-  {fix y
-    {fix z assume z: "P z" "y < z"
-      from L' z have "y < L" by auto }
-    moreover
-    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
-      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
-      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
-      with yL(1) have False  by arith}
-    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
-  thus ?thesis by blast
+proof
+  from bz have "bdd_above (Collect P)"
+    by (force intro: less_imp_le)
+  then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
+    using ex bz by (subst less_cSup_iff) auto
 qed
 
 subsection {* Fundamental theorem of algebra *}
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Library/Glbs.thy
--- a/src/HOL/Library/Glbs.thy	Tue Nov 05 09:45:00 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-(* Author: Amine Chaieb, University of Cambridge *)
-
-header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
-
-theory Glbs
-imports Lubs
-begin
-
-definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
-  where "greatestP P x = (P x \<and> Collect P *<=  x)"
-
-definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
-  where "isLb R S x = (x <=* S \<and> x: R)"
-
-definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
-  where "isGlb R S x = greatestP (isLb R S) x"
-
-definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
-  where "lbs R S = Collect (isLb R S)"
-
-
-subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
-  and @{term isGlb} *}
-
-lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
-  by (simp add: greatestP_def)
-
-lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
-  by (simp add: greatestP_def)
-
-lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
-  by (blast dest!: greatestPD2 setleD)
-
-lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
-  by (simp add: isGlb_def isLb_def greatestP_def)
-
-lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
-  by (simp add: isGlb_def isLb_def greatestP_def)
-
-lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
-  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
-
-lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
-  by (blast dest!: isGlbD1 setgeD)
-
-lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
-  by (simp add: isGlb_def)
-
-lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
-  by (simp add: isGlb_def)
-
-lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
-  by (simp add: isGlb_def greatestP_def)
-
-lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
-  by (simp add: isLb_def setge_def)
-
-lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
-  by (simp add: isLb_def)
-
-lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
-  by (simp add: isLb_def)
-
-lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
-  by (simp add: isLb_def)
-
-lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
-  unfolding isGlb_def by (blast intro!: greatestPD3)
-
-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 326fd7103cb4 -r c4159fe6fa46 src/HOL/Library/Lubs_Glbs.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Lubs_Glbs.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -0,0 +1,245 @@
+(*  Title:      HOL/Library/Lubs_Glbs.thy
+    Author:     Jacques D. Fleuriot, University of Cambridge
+    Author:     Amine Chaieb, University of Cambridge *)
+
+header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
+
+theory Lubs_Glbs
+imports Complex_Main
+begin
+
+text {* Thanks to suggestions by James Margetson *}
+
+definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
+  where "S *<= x = (ALL y: S. y \<le> x)"
+
+definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
+  where "x <=* S = (ALL y: S. x \<le> y)"
+
+
+subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
+
+lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
+  by (simp add: setle_def)
+
+lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
+  by (simp add: setle_def)
+
+lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
+  by (simp add: setge_def)
+
+lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
+  by (simp add: setge_def)
+
+
+definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "leastP P x = (P x \<and> x <=* Collect P)"
+
+definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "isUb R S x = (S *<= x \<and> x: R)"
+
+definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "isLub R S x = leastP (isUb R S) x"
+
+definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
+  where "ubs R S = Collect (isUb R S)"
+
+
+subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
+
+lemma leastPD1: "leastP P x \<Longrightarrow> P x"
+  by (simp add: leastP_def)
+
+lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
+  by (simp add: leastP_def)
+
+lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
+  by (blast dest!: leastPD2 setgeD)
+
+lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
+  by (simp add: isLub_def isUb_def leastP_def)
+
+lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
+  by (simp add: isLub_def isUb_def leastP_def)
+
+lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
+  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
+
+lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
+  by (blast dest!: isLubD1 setleD)
+
+lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
+  by (simp add: isLub_def)
+
+lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
+  by (simp add: isLub_def)
+
+lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
+  by (simp add: isLub_def leastP_def)
+
+lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
+  by (simp add: isUb_def setle_def)
+
+lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
+  by (simp add: isUb_def)
+
+lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
+  by (simp add: isUb_def)
+
+lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
+  by (simp add: isUb_def)
+
+lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
+  unfolding isLub_def by (blast intro!: leastPD3)
+
+lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
+  unfolding ubs_def isLub_def by (rule leastPD2)
+
+lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
+  apply (frule isLub_isUb)
+  apply (frule_tac x = y in isLub_isUb)
+  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
+  done
+
+lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
+  by (simp add: isUbI setleI)
+
+
+definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "greatestP P x = (P x \<and> Collect P *<=  x)"
+
+definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "isLb R S x = (x <=* S \<and> x: R)"
+
+definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
+  where "isGlb R S x = greatestP (isLb R S) x"
+
+definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
+  where "lbs R S = Collect (isLb R S)"
+
+
+subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *}
+
+lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
+  by (simp add: greatestP_def)
+
+lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
+  by (simp add: greatestP_def)
+
+lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
+  by (blast dest!: greatestPD2 setleD)
+
+lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
+  by (simp add: isGlb_def isLb_def greatestP_def)
+
+lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
+  by (simp add: isGlb_def isLb_def greatestP_def)
+
+lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
+  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
+
+lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
+  by (blast dest!: isGlbD1 setgeD)
+
+lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
+  by (simp add: isGlb_def)
+
+lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
+  by (simp add: isGlb_def)
+
+lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
+  by (simp add: isGlb_def greatestP_def)
+
+lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
+  by (simp add: isLb_def setge_def)
+
+lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
+  by (simp add: isLb_def)
+
+lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
+  by (simp add: isLb_def)
+
+lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
+  by (simp add: isLb_def)
+
+lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
+  unfolding isGlb_def by (blast intro!: greatestPD3)
+
+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
+
+lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)"
+  by (auto simp: bdd_above_def setle_def)
+
+lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)"
+  by (auto simp: bdd_below_def setge_def)
+
+lemma isLub_cSup: 
+  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
+  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
+            intro!: setgeI cSup_upper cSup_least)
+
+lemma isGlb_cInf: 
+  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
+  by  (auto simp add: isGlb_def setge_def greatestP_def isLb_def
+            intro!: setleI cInf_lower cInf_greatest)
+
+lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+  by (metis cSup_least setle_def)
+
+lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+  by (metis cInf_greatest setge_def)
+
+lemma cSup_bounds:
+  fixes S :: "'a :: conditionally_complete_lattice set"
+  shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b"
+  using cSup_least[of S b] cSup_upper2[of _ S a]
+  by (auto simp: bdd_above_setle setge_def setle_def)
+
+lemma cSup_unique: "(S::'a :: {conditionally_complete_linorder, no_bot} set) *<= b \<Longrightarrow> (\<forall>b'<b. \<exists>x\<in>S. b' < x) \<Longrightarrow> Sup S = b"
+  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
+
+lemma cInf_unique: "b <=* (S::'a :: {conditionally_complete_linorder, no_top} set) \<Longrightarrow> (\<forall>b'>b. \<exists>x\<in>S. b' > x) \<Longrightarrow> Inf S = b"
+  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
+
+text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*}
+
+lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
+  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
+
+lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
+  by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
+
+lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
+  by (blast intro: reals_complete Bseq_isUb)
+
+lemma isLub_mono_imp_LIMSEQ:
+  fixes X :: "nat \<Rightarrow> real"
+  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
+  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
+  shows "X ----> u"
+proof -
+  have "X ----> (SUP i. X i)"
+    using u[THEN isLubD1] X
+    by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
+  also have "(SUP i. X i) = u"
+    using isLub_cSup[of "range X"] u[THEN isLubD1]
+    by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
+  finally show ?thesis .
+qed
+
+lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
+
+lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)"
+  by (rule cInf_superset_mono) (auto simp: bdd_below_setge)
+
+lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)"
+  by (rule cSup_subset_mono) (auto simp: bdd_above_setle)
+
+end
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Library/RBT_Set.thy
--- a/src/HOL/Library/RBT_Set.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Library/RBT_Set.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -756,7 +756,8 @@
 declare Inf_Set_fold[folded Inf'_def, code]
 
 lemma INFI_Set_fold [code]:
-  "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
+  fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
+  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
 proof -
   have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
     by default (auto simp add: fun_eq_iff ac_simps)
@@ -796,7 +797,8 @@
 declare Sup_Set_fold[folded Sup'_def, code]
 
 lemma SUPR_Set_fold [code]:
-  "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
+  fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
+  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
 proof -
   have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
     by default (auto simp add: fun_eq_iff ac_simps)
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Limits.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -138,6 +138,18 @@
 lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
 by (auto simp add: Bseq_def)
 
+lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)"
+proof (elim BseqE, intro bdd_aboveI2)
+  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K"
+    by (auto elim!: allE[of _ n])
+qed
+
+lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
+proof (elim BseqE, intro bdd_belowI2)
+  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
+    by (auto elim!: allE[of _ n])
+qed
+
 lemma lemma_NBseq_def:
   "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
 proof safe
@@ -210,18 +222,6 @@
 
 subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
 
-lemma Bseq_isUb:
-  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
-
-text{* Use completeness of reals (supremum property)
-   to show that any bounded sequence has a least upper bound*}
-
-lemma Bseq_isLub:
-  "!!(X::nat=>real). Bseq X ==>
-   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
-by (blast intro: reals_complete Bseq_isUb)
-
 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   by (simp add: Bseq_def)
 
@@ -1358,40 +1358,29 @@
 
 text {* A monotone sequence converges to its least upper bound. *}
 
-lemma isLub_mono_imp_LIMSEQ:
-  fixes X :: "nat \<Rightarrow> real"
-  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
-  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
-  shows "X ----> u"
-proof (rule LIMSEQ_I)
-  have 1: "\<forall>n. X n \<le> u"
-    using isLubD2 [OF u] by auto
-  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
-    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
-  hence 2: "\<forall>y<u. \<exists>n. y < X n"
-    by (metis not_le)
-  fix r :: real assume "0 < r"
-  hence "u - r < u" by simp
-  hence "\<exists>m. u - r < X m" using 2 by simp
-  then obtain m where "u - r < X m" ..
-  with X have "\<forall>n\<ge>m. u - r < X n"
-    by (fast intro: less_le_trans)
-  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
-  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
-    using 1 by (simp add: diff_less_eq add_commute)
-qed
+lemma LIMSEQ_incseq_SUP:
+  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
+  assumes u: "bdd_above (range X)"
+  assumes X: "incseq X"
+  shows "X ----> (SUP i. X i)"
+  by (rule order_tendstoI)
+     (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
 
-text{*A standard proof of the theorem for monotone increasing sequence*}
-
-lemma Bseq_mono_convergent:
-   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
-  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
+lemma LIMSEQ_decseq_INF:
+  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
+  assumes u: "bdd_below (range X)"
+  assumes X: "decseq X"
+  shows "X ----> (INF i. X i)"
+  by (rule order_tendstoI)
+     (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
 
 text{*Main monotonicity theorem*}
 
 lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
-  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
-            Bseq_mono_convergent)
+  by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
+
+lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
+  by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
 
 lemma Cauchy_iff:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Lubs.thy
--- a/src/HOL/Lubs.thy	Tue Nov 05 09:45:00 2013 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,103 +0,0 @@
-(*  Title:      HOL/Lubs.thy
-    Author:     Jacques D. Fleuriot, University of Cambridge
-*)
-
-header {* Definitions of Upper Bounds and Least Upper Bounds *}
-
-theory Lubs
-imports Main
-begin
-
-text {* Thanks to suggestions by James Margetson *}
-
-definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
-  where "S *<= x = (ALL y: S. y \<le> x)"
-
-definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
-  where "x <=* S = (ALL y: S. x \<le> y)"
-
-definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
-  where "leastP P x = (P x \<and> x <=* Collect P)"
-
-definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
-  where "isUb R S x = (S *<= x \<and> x: R)"
-
-definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
-  where "isLub R S x = leastP (isUb R S) x"
-
-definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
-  where "ubs R S = Collect (isUb R S)"
-
-
-subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
-
-lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
-  by (simp add: setle_def)
-
-lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
-  by (simp add: setle_def)
-
-lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
-  by (simp add: setge_def)
-
-lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
-  by (simp add: setge_def)
-
-
-subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
-
-lemma leastPD1: "leastP P x \<Longrightarrow> P x"
-  by (simp add: leastP_def)
-
-lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
-  by (simp add: leastP_def)
-
-lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
-  by (blast dest!: leastPD2 setgeD)
-
-lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
-  by (simp add: isLub_def isUb_def leastP_def)
-
-lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
-  by (simp add: isLub_def isUb_def leastP_def)
-
-lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
-  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
-
-lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
-  by (blast dest!: isLubD1 setleD)
-
-lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
-  by (simp add: isLub_def)
-
-lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
-  by (simp add: isLub_def)
-
-lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
-  by (simp add: isLub_def leastP_def)
-
-lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
-  by (simp add: isUb_def setle_def)
-
-lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
-  by (simp add: isUb_def)
-
-lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
-  by (simp add: isUb_def)
-
-lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
-  by (simp add: isUb_def)
-
-lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
-  unfolding isLub_def by (blast intro!: leastPD3)
-
-lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
-  unfolding ubs_def isLub_def by (rule leastPD2)
-
-lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
-  apply (frule isLub_isUb)
-  apply (frule_tac x = y in isLub_isUb)
-  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
-  done
-
-end
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -4506,38 +4506,30 @@
     apply (erule_tac x="x - y" in ballE)
     apply (auto simp add: inner_diff)
     done
-  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
+  def k \<equiv> "SUP x:t. a \<bullet> x"
   show ?thesis
     apply (rule_tac x="-a" in exI)
     apply (rule_tac x="-(k + b / 2)" in exI)
-    apply rule
-    apply rule
-    defer
-    apply rule
+    apply (intro conjI ballI)
     unfolding inner_minus_left and neg_less_iff_less
   proof -
-    from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
-      apply (erule_tac x=y in ballE)
-      apply (rule setleI)
-      using `y \<in> s`
-      apply auto
-      done
-    then have k: "isLub UNIV ((\<lambda>x. inner a x) ` t) k"
+    fix x assume "x \<in> t"
+    then have "inner a x - b / 2 < k"
       unfolding k_def
-      apply (rule_tac isLub_cSup)
-      using assms(5)
-      apply auto
-      done
-    fix x
-    assume "x \<in> t"
-    then show "inner a x < (k + b / 2)"
-      using `0<b` and isLubD2[OF k, of "inner a x"] by auto
+    proof (subst less_cSUP_iff)
+      show "t \<noteq> {}" by fact
+      show "bdd_above (op \<bullet> a ` t)"
+        using ab[rule_format, of y] `y \<in> s`
+        by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
+    qed (auto intro!: bexI[of _ x] `0<b`)
+    then show "inner a x < k + b / 2"
+      by auto
   next
     fix x
     assume "x \<in> s"
     then have "k \<le> inner a x - b"
       unfolding k_def
-      apply (rule_tac cSup_least)
+      apply (rule_tac cSUP_least)
       using assms(5)
       using ab[THEN bspec[where x=x]]
       apply auto
@@ -4626,20 +4618,14 @@
   from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
   obtain a where "a \<noteq> 0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"
     using assms(3-5) by auto
-  then have "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
+  then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
     by (force simp add: inner_diff)
-  then show ?thesis
-    apply (rule_tac x=a in exI)
-    apply (rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI)
+  then have bdd: "bdd_above ((op \<bullet> a)`s)"
+    using `t \<noteq> {}` by (auto intro: bdd_aboveI2[OF *])
+  show ?thesis
     using `a\<noteq>0`
-    apply auto
-    apply (rule isLub_cSup[THEN isLubD2])
-    prefer 4
-    apply (rule cSup_least)
-    using assms(3-5)
-    apply (auto simp add: setle_def)
-    apply metis
-    done
+    by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"])
+       (auto intro!: cSUP_upper bdd cSUP_least `a \<noteq> 0` `s \<noteq> {}` *)
 qed
 
 
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -28,10 +28,10 @@
 proof -
   have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
     by arith
-  then show ?thesis
-    using S b cSup_bounds[of S "l - e" "l+e"]
-    unfolding th
-    by (auto simp add: setge_def setle_def)
+  have "bdd_above S"
+    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
+  with S b show ?thesis
+    unfolding th by (auto intro!: cSup_upper2 cSup_least)
 qed
 
 lemma cInf_asclose: (* TODO: is this really needed? *)
@@ -70,39 +70,6 @@
   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
   by (metis cInf_eq_Min Min_le_iff)
 
-lemma Inf: (* rename *)
-  fixes S :: "real set"
-  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
-  by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def
-    intro: cInf_lower cInf_greatest)
-
-lemma real_le_inf_subset:
-  assumes "t \<noteq> {}"
-    and "t \<subseteq> s"
-    and "\<exists>b. b <=* s"
-  shows "Inf s \<le> Inf (t::real set)"
-  apply (rule isGlb_le_isLb)
-  apply (rule Inf[OF assms(1)])
-  apply (insert assms)
-  apply (erule exE)
-  apply (rule_tac x = b in exI)
-  apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
-  done
-
-lemma real_ge_sup_subset:
-  fixes t :: "real set"
-  assumes "t \<noteq> {}"
-    and "t \<subseteq> s"
-    and "\<exists>b. s *<= b"
-  shows "Sup s \<ge> Sup t"
-  apply (rule isLub_le_isUb)
-  apply (rule isLub_cSup[OF assms(1)])
-  apply (insert assms)
-  apply (erule exE)
-  apply (rule_tac x = b in exI)
-  apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
-  done
-
 (*declare not_less[simp] not_le[simp]*)
 
 lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
@@ -486,24 +453,24 @@
 subsection {* Bounds on intervals where they exist. *}
 
 definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
-  where "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
+  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
 
 definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
-  where "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
+  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
 
 lemma interval_upperbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
     interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
   unfolding interval_upperbound_def euclidean_representation_setsum
-  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
-      intro!: cSup_unique)
+  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] SUP_def
+           intro!: cSup_eq)
 
 lemma interval_lowerbound[simp]:
   "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
     interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
   unfolding interval_lowerbound_def euclidean_representation_setsum
-  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
-      intro!: cInf_unique)
+  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] INF_def
+           intro!: cInf_eq)
 
 lemmas interval_bounds = interval_upperbound interval_lowerbound
 
@@ -6627,7 +6594,7 @@
 lemma interval_bound_sing[simp]:
   "interval_upperbound {a} = a"
   "interval_lowerbound {a} = a"
-  unfolding interval_upperbound_def interval_lowerbound_def
+  unfolding interval_upperbound_def interval_lowerbound_def SUP_def INF_def
   by (auto simp: euclidean_representation)
 
 lemma additive_tagged_division_1:
@@ -11236,37 +11203,26 @@
 lemma bounded_variation_absolutely_integrable_interval:
   fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
   assumes "f integrable_on {a..b}"
-    and "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
+    and *: "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
   shows "f absolutely_integrable_on {a..b}"
 proof -
-  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }"
-  def i \<equiv> "Sup ?S"
-  have i: "isLub UNIV ?S i"
-    unfolding i_def
-    apply (rule isLub_cSup)
-    apply (rule elementary_interval)
-    defer
-    apply (rule_tac x=B in exI)
-    apply (rule setleI)
-    using assms(2)
-    apply auto
-    done
+  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of {a..b}}"
+  have D_1: "?D \<noteq> {}"
+    by (rule elementary_interval[of a b]) auto
+  have D_2: "bdd_above (?f`?D)"
+    by (metis * mem_Collect_eq bdd_aboveI2)
+  note D = D_1 D_2
+  let ?S = "SUP x:?D. ?f x"
   show ?thesis
     apply rule
     apply (rule assms)
     apply rule
-    apply (subst has_integral[of _ i])
+    apply (subst has_integral[of _ ?S])
   proof safe
     case goal1
-    then have "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
-      {d. d division_of {a..b}}))"
-      using isLub_ubs[OF i,rule_format]
-      unfolding setge_def ubs_def
-      by auto
-    then have "\<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
-      unfolding mem_Collect_eq isUb_def setle_def
-      by (simp add: not_le)
-    then guess d .. note d=conjunctD2[OF this]
+    then have "?S - e / 2 < ?S" by simp
+    then obtain d where d: "d division_of {a..b}" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
+      unfolding less_cSUP_iff[OF D] by auto
     note d' = division_ofD[OF this(1)]
 
     have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
@@ -11451,21 +11407,17 @@
         done
       note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
 
-      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
-        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - i) < e"
+      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
+        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
         by arith
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e"
+      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
         unfolding real_norm_def
         apply (rule *[rule_format,OF **])
         apply safe
         apply(rule d(2))
       proof -
-        case goal1
-        show ?case unfolding sum_p'
-          apply (rule isLubD2[OF i])
-          using division_of_tagged_division[OF p'']
-          apply auto
-          done
+        case goal1 show ?case
+          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
       next
         case goal2
         have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
@@ -11756,18 +11708,13 @@
     and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
   shows "f absolutely_integrable_on UNIV"
 proof (rule absolutely_integrable_onI, fact, rule)
-  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of  (\<Union>d)}"
-  def i \<equiv> "Sup ?S"
-  have i: "isLub UNIV ?S i"
-    unfolding i_def
-    apply (rule isLub_cSup)
-    apply (rule elementary_interval)
-    defer
-    apply (rule_tac x=B in exI)
-    apply (rule setleI)
-    using assms(2)
-    apply auto
-    done
+  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
+  have D_1: "?D \<noteq> {}"
+    by (rule elementary_interval) auto
+  have D_2: "bdd_above (?f`?D)"
+    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
+  note D = D_1 D_2
+  let ?S = "SUP d:?D. ?f d"
   have f_int: "\<And>a b. f absolutely_integrable_on {a..b}"
     apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
     apply (rule integrable_on_subinterval[OF assms(1)])
@@ -11776,7 +11723,7 @@
     apply (rule assms(2)[rule_format])
     apply auto
     done
-  show "((\<lambda>x. norm (f x)) has_integral i) UNIV"
+  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
     apply (subst has_integral_alt')
     apply safe
   proof -
@@ -11785,16 +11732,11 @@
       using f_int[of a b] by auto
   next
     case goal2
-    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
+    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
     proof (rule ccontr)
       assume "\<not> ?thesis"
-      then have "i \<le> i - e"
-        apply -
-        apply (rule isLub_le_isUb[OF i])
-        apply (rule isUbI)
-        unfolding setle_def
-        apply auto
-        done
+      then have "?S \<le> ?S - e"
+        by (intro cSUP_least[OF D(1)]) auto
       then show False
         using goal2 by auto
     qed
@@ -11811,9 +11753,9 @@
     proof -
       fix a b :: 'n
       assume ab: "ball 0 (K + 1) \<subseteq> {a..b}"
-      have *: "\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs (s - i) < e"
+      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
         by arith
-      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
+      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
         unfolding real_norm_def
         apply (rule *[rule_format])
         apply safe
@@ -11865,10 +11807,10 @@
         from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
         from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
         note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
-        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
-          abs (sf' - di) < e / 2 \<longrightarrow> di < i + e"
+        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
+          abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
           by arith
-        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e"
+        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
           apply (subst if_P)
           apply rule
         proof (rule *[rule_format])
@@ -11891,18 +11833,12 @@
             apply (subst abs_of_nonneg)
             apply auto
             done
-          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
+          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
+            using partial_division_of_tagged_division[of p "{a..b}"] p(1)
             apply (subst setsum_over_tagged_division_lemma[OF p(1)])
-            defer
-            apply (rule isLubD2[OF i])
-            unfolding image_iff
-            apply (rule_tac x="snd ` p" in bexI)
-            unfolding mem_Collect_eq
-            defer
-            apply (rule partial_division_of_tagged_division[of _ "{a..b}"])
-            using p(1)
-            unfolding tagged_division_of_def
-            apply auto
+            apply (simp add: integral_null)
+            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
+            apply (auto simp: tagged_partial_division_of_def)
             done
         qed
       qed
@@ -12378,11 +12314,22 @@
 lemma dominated_convergence:
   fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
   assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
-    and "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
+    and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
     and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
   shows "g integrable_on s"
     and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
 proof -
+  have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
+  proof (safe intro!: bdd_belowI)
+    fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
+      using assms(3)[rule_format, of x n] by simp
+  qed
+  have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
+  proof (safe intro!: bdd_aboveI)
+    fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
+      using assms(3)[rule_format, of x n] by simp
+  qed
+
   have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
     ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
     integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
@@ -12422,66 +12369,32 @@
     fix x
     assume x: "x \<in> s"
     show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
-      apply (rule cInf_ge)
-      unfolding setge_def
-      defer
-      apply rule
-      apply (subst cInf_finite_le_iff)
-      prefer 3
-      apply (rule_tac x=xa in bexI)
-      apply auto
-      done
-    let ?S = "{f j x| j.  m \<le> j}"
-    def i \<equiv> "Inf ?S"
-    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
+      by (rule cInf_superset_mono) auto
+    let ?S = "{f j x| j. m \<le> j}"
+    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
     proof (rule LIMSEQ_I)
       case goal1
       note r = this
-      have i: "isGlb UNIV ?S i"
-        unfolding i_def
-        apply (rule Inf)
-        defer
-        apply (rule_tac x="- h x - 1" in exI)
-        unfolding setge_def
-      proof safe
-        case goal1
-        then show ?case using assms(3)[rule_format,OF x, of j] by auto
-      qed auto
-
-      have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
-      proof(rule ccontr)
-        assume "\<not> ?thesis"
-        then have "i \<ge> i + r"
-          apply -
-          apply (rule isGlb_le_isLb[OF i])
-          apply (rule isLbI)
-          unfolding setge_def
-          apply fastforce+
-          done
-        then show False using r by auto
-      qed
-      then guess y .. note y=this[unfolded not_le]
-      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
+
+      have "\<exists>y\<in>?S. y < Inf ?S + r"
+        by (subst cInf_less_iff[symmetric]) (auto simp: `x\<in>s` r)
+      then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
+        by blast
 
       show ?case
         apply (rule_tac x=N in exI)
       proof safe
         case goal1
-        have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
+        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
           by arith
         show ?case
           unfolding real_norm_def
-            apply (rule *[rule_format,OF y(2)])
-            unfolding i_def
-            apply (rule real_le_inf_subset)
-            prefer 3
-            apply (rule,rule isGlbD1[OF i])
-            prefer 3
-            apply (subst cInf_finite_le_iff)
-            prefer 3
-            apply (rule_tac x=y in bexI)
+            apply (rule *[rule_format, OF N(1)])
+            apply (rule cInf_superset_mono, auto simp: `x\<in>s`) []
+            apply (rule cInf_lower)
             using N goal1
-            apply auto
+            apply auto []
+            apply simp
             done
       qed
     qed
@@ -12525,65 +12438,27 @@
     fix x
     assume x: "x\<in>s"
     show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
-      apply (rule cSup_le)
-      unfolding setle_def
-      defer
-      apply rule
-      apply (subst cSup_finite_ge_iff)
-      prefer 3
-      apply (rule_tac x=y in bexI)
-      apply auto
-      done
-    let ?S = "{f j x| j.  m \<le> j}"
-    def i \<equiv> "Sup ?S"
-    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
+      by (rule cSup_subset_mono) auto
+    let ?S = "{f j x| j. m \<le> j}"
+    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
     proof (rule LIMSEQ_I)
       case goal1 note r=this
-      have i: "isLub UNIV ?S i"
-        unfolding i_def
-        apply (rule isLub_cSup)
-        defer
-        apply (rule_tac x="h x" in exI)
-        unfolding setle_def
-      proof safe
-        case goal1
-        then show ?case
-          using assms(3)[rule_format,OF x, of j] by auto
-      qed auto
-
-      have "\<exists>y\<in>?S. \<not> y \<le> i - r"
-      proof (rule ccontr)
-        assume "\<not> ?thesis"
-        then have "i \<le> i - r"
-          apply -
-          apply (rule isLub_le_isUb[OF i])
-          apply (rule isUbI)
-          unfolding setle_def
-          apply fastforce+
-          done
-        then show False
-          using r by auto
-      qed
-      then guess y .. note y=this[unfolded not_le]
-      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
+      have "\<exists>y\<in>?S. Sup ?S - r < y"
+        by (subst less_cSup_iff[symmetric]) (auto simp: r `x\<in>s`)
+      then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
+        by blast
 
       show ?case
         apply (rule_tac x=N in exI)
       proof safe
         case goal1
-        have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
+        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
           by arith
         show ?case
-          unfolding real_norm_def
-          apply (rule *[rule_format,OF y(2)])
-          unfolding i_def
-          apply (rule real_ge_sup_subset)
-          prefer 3
-          apply (rule, rule isLubD1[OF i])
-          prefer 3
-          apply (subst cSup_finite_ge_iff)
-          prefer 3
-          apply (rule_tac x = y in bexI)
+          apply simp
+          apply (rule *[rule_format, OF N(1)])
+          apply (rule cSup_subset_mono, auto simp: `x\<in>s`) []
+          apply (subst cSup_upper)
           using N goal1
           apply auto
           done
@@ -12616,17 +12491,7 @@
 
     have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
     show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
-      apply -
-      apply (rule real_le_inf_subset)
-      prefer 3
-      unfolding setge_def
-      apply (rule_tac x="- h x" in exI)
-      apply safe
-      apply (rule *)
-      using assms(3)[rule_format,OF x]
-      unfolding real_norm_def abs_le_iff
-      apply auto
-      done
+      by (intro cInf_superset_mono) (auto simp: `x\<in>s`)
 
     show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
     proof (rule LIMSEQ_I)
@@ -12674,16 +12539,7 @@
     assume x: "x \<in> s"
 
     show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
-      apply -
-      apply (rule real_ge_sup_subset)
-      prefer 3
-      unfolding setle_def
-      apply (rule_tac x="h x" in exI)
-      apply safe
-      using assms(3)[rule_format,OF x]
-      unfolding real_norm_def abs_le_iff
-      apply auto
-      done
+      by (rule cSup_subset_mono) (auto simp: `x\<in>s`)
     show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
     proof (rule LIMSEQ_I)
       case goal1
@@ -12712,41 +12568,18 @@
     from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
     from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
     show ?case
-      apply (rule_tac x="N1+N2" in exI, safe)
-    proof -
+    proof (rule_tac x="N1+N2" in exI, safe)
       fix n
       assume n: "n \<ge> N1 + N2"
       have *: "\<And>i0 i i1 g. \<bar>i0 - g\<bar> < r \<longrightarrow> \<bar>i1 - g\<bar> < r \<longrightarrow> i0 \<le> i \<longrightarrow> i \<le> i1 \<longrightarrow> \<bar>i - g\<bar> < r"
         by arith
       show "norm (integral s (f n) - integral s g) < r"
         unfolding real_norm_def
-        apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
-      proof -
+      proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
         show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
-        proof (rule integral_le[OF dec1(1) assms(1)], safe)
-          fix x
-          assume x: "x \<in> s"
-          have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
-          show "Inf {f j x |j. n \<le> j} \<le> f n x"
-            apply (intro cInf_lower bdd_belowI)
-            apply auto []
-            apply (rule *)
-            using assms(3)[rule_format,OF x]
-            unfolding real_norm_def abs_le_iff
-            apply auto
-            done
-        qed
+          by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
         show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
-        proof (rule integral_le[OF assms(1) inc1(1)], safe)
-          fix x
-          assume x: "x \<in> s"
-          show "f n x \<le> Sup {f j x |j. n \<le> j}"
-            apply (rule cSup_upper)
-            using assms(3)[rule_format,OF x]
-            unfolding real_norm_def abs_le_iff
-            apply auto
-            done
-        qed
+          by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
       qed (insert n, auto)
     qed
   qed
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Multivariate_Analysis/Operator_Norm.thy
--- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -8,7 +8,7 @@
 imports Linear_Algebra
 begin
 
-definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
+definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"
 
 lemma norm_bound_generalize:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -67,25 +67,22 @@
   shows "norm (f x) \<le> onorm f * norm x"
     and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
 proof -
-  let ?S = "{norm (f x) |x. norm x = 1}"
+  let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
   have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
     by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
   then have Se: "?S \<noteq> {}"
     by auto
-  from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
-    unfolding norm_bound_generalize[OF lf, symmetric]
-    by (auto simp add: setle_def)
-  from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
-  show "norm (f x) \<le> onorm f * norm x"
+  from linear_bounded[OF lf] have b: "bdd_above ?S"
+    unfolding norm_bound_generalize[OF lf, symmetric] by auto
+  then show "norm (f x) \<le> onorm f * norm x"
     apply -
     apply (rule spec[where x = x])
     unfolding norm_bound_generalize[OF lf, symmetric]
-    apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
+    apply (auto simp: onorm_def intro!: cSUP_upper)
     done
   show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
-    using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
     unfolding norm_bound_generalize[OF lf, symmetric]
-    by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
+    using Se by (auto simp: onorm_def intro!: cSUP_least b)
 qed
 
 lemma onorm_pos_le:
@@ -107,18 +104,8 @@
   apply arith
   done
 
-lemma onorm_const:
-  "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
-proof -
-  let ?f = "\<lambda>x::'a. y::'b"
-  have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
-    by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
-  show ?thesis
-    unfolding onorm_def th
-    apply (rule cSup_unique)
-    apply (simp_all  add: setle_def)
-    done
-qed
+lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
+  using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)
 
 lemma onorm_pos_lt:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -10,7 +10,6 @@
 imports
   Complex_Main
   "~~/src/HOL/Library/Countable_Set"
-  "~~/src/HOL/Library/Glbs"
   "~~/src/HOL/Library/FuncSet"
   Linear_Algebra
   Norm_Arith
@@ -28,8 +27,6 @@
 lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
   by (rule LIMSEQ_subseq_LIMSEQ)
 
-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)"
   by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
@@ -1555,7 +1552,7 @@
       fix y
       assume "y \<in> {x<..} \<inter> I"
       with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
-        by (auto intro: cInf_lower)
+        by (auto intro!: cInf_lower bdd_belowI2)
       with a have "a < f y"
         by (blast intro: less_le_trans)
     }
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/NSA/NSA.thy
--- a/src/HOL/NSA/NSA.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/NSA/NSA.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -6,7 +6,7 @@
 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
 theory NSA
-imports HyperDef
+imports HyperDef "~~/src/HOL/Library/Lubs_Glbs"
 begin
 
 definition
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Real.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -970,13 +970,6 @@
 qed
 end
 
-text {*
-  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
-*}
-
-lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t"
-  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
-
 
 subsection {* Hiding implementation details *}
 
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -1425,9 +1425,6 @@
   @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
 *}
 
-lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
-by (simp add: isUbI setleI)
-
 lemma increasing_LIMSEQ:
   fixes f :: "nat \<Rightarrow> real"
   assumes inc: "\<And>n. f n \<le> f (Suc n)"
@@ -1454,40 +1451,33 @@
   then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
 
   { fix N x assume N: "\<forall>n\<ge>N. X n < x"
-  have "isUb UNIV S x"
-  proof (rule isUb_UNIV_I)
   fix y::real assume "y \<in> S"
   hence "\<exists>M. \<forall>n\<ge>M. y < X n"
     by (simp add: S_def)
   then obtain M where "\<forall>n\<ge>M. y < X n" ..
   hence "y < X (max M N)" by simp
   also have "\<dots> < x" using N by simp
-  finally show "y \<le> x"
-    by (rule order_less_imp_le)
-  qed }
+  finally have "y \<le> x"
+    by (rule order_less_imp_le) }
   note bound_isUb = this 
 
-  have "\<exists>u. isLub UNIV S u"
-  proof (rule reals_complete)
   obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
     using X[THEN metric_CauchyD, OF zero_less_one] by auto
   hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp
-  show "\<exists>x. x \<in> S"
-  proof
+  have [simp]: "S \<noteq> {}"
+  proof (intro exI ex_in_conv[THEN iffD1])
     from N have "\<forall>n\<ge>N. X N - 1 < X n"
       by (simp add: abs_diff_less_iff dist_real_def)
     thus "X N - 1 \<in> S" by (rule mem_S)
   qed
-  show "\<exists>u. isUb UNIV S u"
+  have [simp]: "bdd_above S"
   proof
     from N have "\<forall>n\<ge>N. X n < X N + 1"
       by (simp add: abs_diff_less_iff dist_real_def)
-    thus "isUb UNIV S (X N + 1)"
+    thus "\<And>s. s \<in> S \<Longrightarrow>  s \<le> X N + 1"
       by (rule bound_isUb)
   qed
-  qed
-  then obtain x where x: "isLub UNIV S x" ..
-  have "X ----> x"
+  have "X ----> Sup S"
   proof (rule metric_LIMSEQ_I)
   fix r::real assume "0 < r"
   hence r: "0 < r/2" by simp
@@ -1499,17 +1489,18 @@
 
   from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
   hence "X N - r/2 \<in> S" by (rule mem_S)
-  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
+  hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
 
   from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
-  hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
-  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
+  from bound_isUb[OF this]
+  have 2: "Sup S \<le> X N + r/2"
+    by (intro cSup_least) simp_all
 
-  show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r"
+  show "\<exists>N. \<forall>n\<ge>N. dist (X n) (Sup S) < r"
   proof (intro exI allI impI)
     fix n assume n: "N \<le> n"
     from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
-    thus "dist (X n) x < r" using 1 2
+    thus "dist (X n) (Sup S) < r" using 1 2
       by (simp add: abs_diff_less_iff dist_real_def)
   qed
   qed
diff -r 326fd7103cb4 -r c4159fe6fa46 src/HOL/ex/Dedekind_Real.thy
--- a/src/HOL/ex/Dedekind_Real.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/ex/Dedekind_Real.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -1506,7 +1506,6 @@
 instance real :: linorder
   by (intro_classes, rule real_le_linear)
 
-
 lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
 apply (cases x, cases y) 
 apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
@@ -1657,7 +1656,6 @@
 lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
 by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
 
-
 subsection {* Completeness of Positive Reals *}
 
 text {*
@@ -1759,107 +1757,23 @@
 qed
 
 text {*
-  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
-*}
-
-lemma posreals_complete:
-  assumes positive_S: "\<forall>x \<in> S. 0 < x"
-    and not_empty_S: "\<exists>x. x \<in> S"
-    and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u"
-  shows "\<exists>t. isLub (UNIV::real set) S t"
-proof
-  let ?pS = "{w. real_of_preal w \<in> S}"
-
-  obtain u where "isUb UNIV S u" using upper_bound_Ex ..
-  hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def)
-
-  obtain x where x_in_S: "x \<in> S" using not_empty_S ..
-  hence x_gt_zero: "0 < x" using positive_S by simp
-  have  "x \<le> u" using sup and x_in_S ..
-  hence "0 < u" using x_gt_zero by arith
-
-  then obtain pu where u_is_pu: "u = real_of_preal pu"
-    by (auto simp add: real_gt_zero_preal_Ex)
-
-  have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu"
-  proof
-    fix pa
-    assume "pa \<in> ?pS"
-    then obtain a where a: "a \<in> S" "a = real_of_preal pa"
-      by simp
-    then have "a \<le> u" using sup by simp
-    with a show "pa \<le> pu"
-      using sup and u_is_pu by (simp add: real_of_preal_le_iff)
-  qed
-
-  have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)"
-  proof
-    fix y
-    assume y_in_S: "y \<in> S"
-    hence "0 < y" using positive_S by simp
-    then obtain py where y_is_py: "y = real_of_preal py"
-      by (auto simp add: real_gt_zero_preal_Ex)
-    hence py_in_pS: "py \<in> ?pS" using y_in_S by simp
-    with pS_less_pu have "py \<le> psup ?pS"
-      by (rule preal_psup_le)
-    thus "y \<le> real_of_preal (psup ?pS)"
-      using y_is_py by (simp add: real_of_preal_le_iff)
-  qed
-
-  moreover {
-    fix x
-    assume x_ub_S: "\<forall>y\<in>S. y \<le> x"
-    have "real_of_preal (psup ?pS) \<le> x"
-    proof -
-      obtain "s" where s_in_S: "s \<in> S" using not_empty_S ..
-      hence s_pos: "0 < s" using positive_S by simp
-
-      hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex)
-      then obtain "ps" where s_is_ps: "s = real_of_preal ps" ..
-      hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp
-
-      from x_ub_S have "s \<le> x" using s_in_S ..
-      hence "0 < x" using s_pos by simp
-      hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex)
-      then obtain "px" where x_is_px: "x = real_of_preal px" ..
-
-      have "\<forall>pe \<in> ?pS. pe \<le> px"
-      proof
-        fix pe
-        assume "pe \<in> ?pS"
-        hence "real_of_preal pe \<in> S" by simp
-        hence "real_of_preal pe \<le> x" using x_ub_S by simp
-        thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff)
-      qed
-
-      moreover have "?pS \<noteq> {}" using ps_in_pS by auto
-      ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub)
-      thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff)
-    qed
-  }
-  ultimately show "isLub UNIV S (real_of_preal (psup ?pS))"
-    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
-qed
-
-text {*
-  \medskip reals Completeness (again!)
+  \medskip Completeness
 *}
 
 lemma reals_complete:
+  fixes S :: "real set"
   assumes notempty_S: "\<exists>X. X \<in> S"
-    and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
-  shows "\<exists>t. isLub (UNIV :: real set) S t"
+    and exists_Ub: "bdd_above S"
+  shows "\<exists>x. (\<forall>s\<in>S. s \<le> x) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> x \<le> y)"
 proof -
   obtain X where X_in_S: "X \<in> S" using notempty_S ..
-  obtain Y where Y_isUb: "isUb (UNIV::real set) S Y"
-    using exists_Ub ..
+  obtain Y where Y_isUb: "\<forall>s\<in>S. s \<le> Y"
+    using exists_Ub by (auto simp: bdd_above_def)
   let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}"
 
   {
     fix x
-    assume "isUb (UNIV::real set) S x"
-    hence S_le_x: "\<forall> y \<in> S. y <= x"
-      by (simp add: isUb_def setle_def)
+    assume S_le_x: "\<forall>s\<in>S. s \<le> x"
     {
       fix s
       assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
@@ -1868,86 +1782,74 @@
       then have "x1 \<le> x" using S_le_x by simp
       with x1 have "s \<le> x + - X + 1" by arith
     }
-    then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
-      by (auto simp add: isUb_def setle_def)
+    then have "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
+      by auto
   } note S_Ub_is_SHIFT_Ub = this
 
-  hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp
-  hence "\<exists>Z. isUb UNIV ?SHIFT Z" ..
+  have *: "\<forall>s\<in>?SHIFT. s \<le> Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub)
+  have "\<forall>s\<in>?SHIFT. s < Y + (-X) + 2"
+  proof
+    fix s assume "s\<in>?SHIFT"
+    with * have "s \<le> Y + (-X) + 1" by simp
+    also have "\<dots> < Y + (-X) + 2" by simp
+    finally show "s < Y + (-X) + 2" .
+  qed
   moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto
   moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT"
     using X_in_S and Y_isUb by auto
-  ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t"
-    using posreals_complete [of ?SHIFT] by blast
+  ultimately obtain t where t_is_Lub: "\<forall>y. (\<exists>x\<in>?SHIFT. y < x) = (y < t)"
+    using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast
 
   show ?thesis
   proof
-    show "isLub UNIV S (t + X + (-1))"
-    proof (rule isLubI2)
-      {
-        fix x
-        assume "isUb (UNIV::real set) S x"
-        hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)"
-          using S_Ub_is_SHIFT_Ub by simp
-        hence "t \<le> (x + (-X) + 1)"
-          using t_is_Lub by (simp add: isLub_le_isUb)
-        hence "t + X + -1 \<le> x" by arith
-      }
-      then show "(t + X + -1) <=* Collect (isUb UNIV S)"
-        by (simp add: setgeI)
+    show "(\<forall>s\<in>S. s \<le> (t + X + (-1))) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> (t + X + (-1)) \<le> y)"
+    proof safe
+      fix x
+      assume "\<forall>s\<in>S. s \<le> x"
+      hence "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
+        using S_Ub_is_SHIFT_Ub by simp
+      then have "\<not> x + (-X) + 1 < t"
+        by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less)
+      thus "t + X + -1 \<le> x" by arith
     next
-      show "isUb UNIV S (t + X + -1)"
-      proof -
-        {
-          fix y
-          assume y_in_S: "y \<in> S"
-          have "y \<le> t + X + -1"
-          proof -
-            obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
-            hence "\<exists> x \<in> S. u = x + - X + 1" by simp
-            then obtain "x" where x_and_u: "u = x + - X + 1" ..
-            have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2)
+      fix y
+      assume y_in_S: "y \<in> S"
+      obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
+      hence "\<exists> x \<in> S. u = x + - X + 1" by simp
+      then obtain "x" where x_and_u: "u = x + - X + 1" ..
+      have u_le_t: "u \<le> t"
+      proof (rule dense_le)
+        fix x assume "x < u" then have "x < t"
+          using u_in_shift t_is_Lub by auto
+        then show "x \<le> t"  by simp
+      qed
 
-            show ?thesis
-            proof cases
-              assume "y \<le> x"
-              moreover have "x = u + X + - 1" using x_and_u by arith
-              moreover have "u + X + - 1  \<le> t + X + -1" using u_le_t by arith
-              ultimately show "y  \<le> t + X + -1" by arith
-            next
-              assume "~(y \<le> x)"
-              hence x_less_y: "x < y" by arith
+      show "y \<le> t + X + -1"
+      proof cases
+        assume "y \<le> x"
+        moreover have "x = u + X + - 1" using x_and_u by arith
+        moreover have "u + X + - 1  \<le> t + X + -1" using u_le_t by arith
+        ultimately show "y  \<le> t + X + -1" by arith
+      next
+        assume "~(y \<le> x)"
+        hence x_less_y: "x < y" by arith
 
-              have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
-              hence "0 < x + (-X) + 1" by simp
-              hence "0 < y + (-X) + 1" using x_less_y by arith
-              hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
-              hence "y + (-X) + 1 \<le> t" using t_is_Lub  by (simp add: isLubD2)
-              thus ?thesis by simp
-            qed
-          qed
-        }
-        then show ?thesis by (simp add: isUb_def setle_def)
+        have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
+        hence "0 < x + (-X) + 1" by simp
+        hence "0 < y + (-X) + 1" using x_less_y by arith
+        hence *: "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
+        have "y + (-X) + 1 \<le> t"
+        proof (rule dense_le)
+          fix x assume "x < y + (-X) + 1" then have "x < t"
+            using * t_is_Lub by auto
+          then show "x \<le> t"  by simp
+        qed
+        thus ?thesis by simp
       qed
     qed
   qed
 qed
 
-text{*A version of the same theorem without all those predicates!*}
-lemma reals_complete2:
-  fixes S :: "(real set)"
-  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
-  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
-               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
-proof -
-  have "\<exists>x. isLub UNIV S x" 
-    by (rule reals_complete)
-       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
-  thus ?thesis
-    by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
-qed
-
-
 subsection {* The Archimedean Property of the Reals *}
 
 theorem reals_Archimedean:
@@ -1969,34 +1871,30 @@
       by (rule mult_right_mono)
     thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc)
   qed
-  hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1"
-    by (simp add: setle_def del: of_nat_Suc, safe, rule spec)
-  hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1"
-    by (simp add: isUbI)
-  hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" ..
-  moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
-  ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t"
-    by (simp add: reals_complete)
-  then obtain "t" where
-    t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" ..
+  hence 2: "bdd_above {z. \<exists>n. z = x * (of_nat (Suc n))}"
+    by (auto intro!: bdd_aboveI[of _ 1])
+  have 1: "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
+  obtain t where
+    upper: "\<And>z. z \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> z \<le> t" and
+    least: "\<And>y. (\<And>a. a \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> a \<le> y) \<Longrightarrow> t \<le> y"
+    using reals_complete[OF 1 2] by auto
 
-  have "\<forall>n::nat. x * of_nat n \<le> t + - x"
-  proof
-    fix n
-    from t_is_Lub have "x * of_nat (Suc n) \<le> t"
-      by (simp add: isLubD2)
-    hence  "x * (of_nat n) + x \<le> t"
-      by (simp add: distrib_left)
-    thus  "x * (of_nat n) \<le> t + - x" by arith
+
+  have "t \<le> t + - x"
+  proof (rule least)
+    fix a assume a: "a \<in> {z. \<exists>n. z = x * (of_nat (Suc n))}"
+    have "\<forall>n::nat. x * of_nat n \<le> t + - x"
+    proof
+      fix n
+      have "x * of_nat (Suc n) \<le> t"
+        by (simp add: upper)
+      hence  "x * (of_nat n) + x \<le> t"
+        by (simp add: distrib_left)
+      thus  "x * (of_nat n) \<le> t + - x" by arith
+    qed    hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
+    with a show "a \<le> t + - x"
+      by auto
   qed
-
-  hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
-  hence "{z. \<exists>n. z = x * (of_nat (Suc n))}  *<= (t + - x)"
-    by (auto simp add: setle_def)
-  hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))"
-    by (simp add: isUbI)
-  hence "t \<le> t + - x"
-    using t_is_Lub by (simp add: isLub_le_isUb)
   thus False using x_pos by arith
 qed