move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
authorhoelzl
Tue Nov 05 09:45:02 2013 +0100 (2013-11-05)
changeset 54263c4159fe6fa46
parent 54262 326fd7103cb4
child 54264 27501a51d847
move Lubs from HOL to HOL-Library (replaced by conditionally complete lattices)
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Hahn_Banach/Bounds.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Library/Glbs.thy
src/HOL/Library/Lubs_Glbs.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Limits.thy
src/HOL/Lubs.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Integration.thy
src/HOL/Multivariate_Analysis/Operator_Norm.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/NSA.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/ex/Dedekind_Real.thy
     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:00 2013 +0100
     1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 09:45:02 2013 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Conditionally-complete Lattices *}
     1.5  
     1.6  theory Conditionally_Complete_Lattices
     1.7 -imports Main Lubs
     1.8 +imports Main
     1.9  begin
    1.10  
    1.11  lemma (in linorder) Sup_fin_eq_Max: "finite X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Sup_fin X = Max X"
    1.12 @@ -28,6 +28,12 @@
    1.13  lemma bdd_belowI[intro]: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> x) \<Longrightarrow> bdd_below A"
    1.14    by (auto simp: bdd_below_def)
    1.15  
    1.16 +lemma bdd_aboveI2: "(\<And>x. x \<in> A \<Longrightarrow> f x \<le> M) \<Longrightarrow> bdd_above (f`A)"
    1.17 +  by force
    1.18 +
    1.19 +lemma bdd_belowI2: "(\<And>x. x \<in> A \<Longrightarrow> m \<le> f x) \<Longrightarrow> bdd_below (f`A)"
    1.20 +  by force
    1.21 +
    1.22  lemma bdd_above_empty [simp, intro]: "bdd_above {}"
    1.23    unfolding bdd_above_def by auto
    1.24  
    1.25 @@ -298,6 +304,12 @@
    1.26  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)"
    1.27    by (metis cSUP_least cSUP_upper assms order_trans)
    1.28  
    1.29 +lemma less_cINF_D: "bdd_below (f`A) \<Longrightarrow> y < (INF i:A. f i) \<Longrightarrow> i \<in> A \<Longrightarrow> y < f i"
    1.30 +  by (metis cINF_lower less_le_trans)
    1.31 +
    1.32 +lemma cSUP_lessD: "bdd_above (f`A) \<Longrightarrow> (SUP i:A. f i) < y \<Longrightarrow> i \<in> A \<Longrightarrow> f i < y"
    1.33 +  by (metis cSUP_upper le_less_trans)
    1.34 +
    1.35  lemma cINF_insert: "A \<noteq> {} \<Longrightarrow> bdd_below (f ` A) \<Longrightarrow> INFI (insert a A) f = inf (f a) (INFI A f)"
    1.36    by (metis INF_def cInf_insert assms empty_is_image image_insert)
    1.37  
    1.38 @@ -347,11 +359,6 @@
    1.39  instance complete_lattice \<subseteq> conditionally_complete_lattice
    1.40    by default (auto intro: Sup_upper Sup_least Inf_lower Inf_greatest)
    1.41  
    1.42 -lemma isLub_cSup: 
    1.43 -  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
    1.44 -  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
    1.45 -            intro!: setgeI cSup_upper cSup_least)
    1.46 -
    1.47  lemma cSup_eq:
    1.48    fixes a :: "'a :: {conditionally_complete_lattice, no_bot}"
    1.49    assumes upper: "\<And>x. x \<in> X \<Longrightarrow> x \<le> a"
    1.50 @@ -370,12 +377,6 @@
    1.51    assume "X = {}" with gt_ex[of a] least show ?thesis by (auto simp: less_le_not_le)
    1.52  qed (intro cInf_eq_non_empty assms)
    1.53  
    1.54 -lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
    1.55 -  by (metis cSup_least setle_def)
    1.56 -
    1.57 -lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
    1.58 -  by (metis cInf_greatest setge_def)
    1.59 -
    1.60  class conditionally_complete_linorder = conditionally_complete_lattice + linorder
    1.61  begin
    1.62  
    1.63 @@ -386,6 +387,12 @@
    1.64  lemma cInf_less_iff: "X \<noteq> {} \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X < y \<longleftrightarrow> (\<exists>x\<in>X. x < y)"
    1.65    by (rule iffI) (metis cInf_greatest not_less, metis cInf_lower le_less_trans)
    1.66  
    1.67 +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)"
    1.68 +  unfolding INF_def using cInf_less_iff[of "f`A"] by auto
    1.69 +
    1.70 +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)"
    1.71 +  unfolding SUP_def using less_cSup_iff[of "f`A"] by auto
    1.72 +
    1.73  lemma less_cSupE:
    1.74    assumes "y < Sup X" "X \<noteq> {}" obtains x where "x \<in> X" "y < x"
    1.75    by (metis cSup_least assms not_le that)
    1.76 @@ -437,27 +444,6 @@
    1.77  lemma cInf_eq_Min: "finite (X::'a::conditionally_complete_linorder set) \<Longrightarrow> X \<noteq> {} \<Longrightarrow> Inf X = Min X"
    1.78    using cInf_eq_Inf_fin[of X] Inf_fin_eq_Min[of X] by simp
    1.79  
    1.80 -lemma cSup_bounds:
    1.81 -  fixes S :: "'a :: conditionally_complete_lattice set"
    1.82 -  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
    1.83 -  shows "a \<le> Sup S \<and> Sup S \<le> b"
    1.84 -proof-
    1.85 -  from isLub_cSup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
    1.86 -  hence b: "Sup S \<le> b" using u 
    1.87 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
    1.88 -  from Se obtain y where y: "y \<in> S" by blast
    1.89 -  from lub l have "a \<le> Sup S"
    1.90 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
    1.91 -       (metis le_iff_sup le_sup_iff y)
    1.92 -  with b show ?thesis by blast
    1.93 -qed
    1.94 -
    1.95 -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"
    1.96 -  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
    1.97 -
    1.98 -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"
    1.99 -  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
   1.100 -
   1.101  lemma cSup_lessThan[simp]: "Sup {..<x::'a::{conditionally_complete_linorder, no_bot, dense_linorder}} = x"
   1.102    by (auto intro!: cSup_eq_non_empty intro: dense_le)
   1.103  
     2.1 --- a/src/HOL/Hahn_Banach/Bounds.thy	Tue Nov 05 09:45:00 2013 +0100
     2.2 +++ b/src/HOL/Hahn_Banach/Bounds.thy	Tue Nov 05 09:45:02 2013 +0100
     2.3 @@ -57,25 +57,7 @@
     2.4    finally show ?thesis .
     2.5  qed
     2.6  
     2.7 -lemma lub_compat: "lub A x = isLub UNIV A x"
     2.8 -proof -
     2.9 -  have "isUb UNIV A = (\<lambda>x. A *<= x \<and> x \<in> UNIV)"
    2.10 -    by (rule ext) (simp only: isUb_def)
    2.11 -  then show ?thesis
    2.12 -    by (simp only: lub_def isLub_def leastP_def setge_def setle_def) blast
    2.13 -qed
    2.14 -
    2.15 -lemma real_complete:
    2.16 -  fixes A :: "real set"
    2.17 -  assumes nonempty: "\<exists>a. a \<in> A"
    2.18 -    and ex_upper: "\<exists>y. \<forall>a \<in> A. a \<le> y"
    2.19 -  shows "\<exists>x. lub A x"
    2.20 -proof -
    2.21 -  from ex_upper have "\<exists>y. isUb UNIV A y"
    2.22 -    unfolding isUb_def setle_def by blast
    2.23 -  with nonempty have "\<exists>x. isLub UNIV A x"
    2.24 -    by (rule reals_complete)
    2.25 -  then show ?thesis by (simp only: lub_compat)
    2.26 -qed
    2.27 +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"
    2.28 +  by (intro exI[of _ "Sup A"]) (auto intro!: cSup_upper cSup_least simp: lub_def)
    2.29  
    2.30  end
     3.1 --- a/src/HOL/Library/ContNotDenum.thy	Tue Nov 05 09:45:00 2013 +0100
     3.2 +++ b/src/HOL/Library/ContNotDenum.thy	Tue Nov 05 09:45:02 2013 +0100
     3.3 @@ -131,17 +131,15 @@
     3.4  
     3.5    -- "A denotes the set of all left-most points of all the intervals ..."
     3.6    moreover obtain A where Adef: "A = ?g ` \<nat>" by simp
     3.7 -  ultimately have "\<exists>x. x\<in>A"
     3.8 +  ultimately have "A \<noteq> {}"
     3.9    proof -
    3.10      have "(0::nat) \<in> \<nat>" by simp
    3.11 -    moreover have "?g 0 = ?g 0" by simp
    3.12 -    ultimately have "?g 0 \<in> ?g ` \<nat>" by (rule  rev_image_eqI)
    3.13 -    with Adef have "?g 0 \<in> A" by simp
    3.14 -    thus ?thesis ..
    3.15 +    with Adef show ?thesis
    3.16 +      by blast
    3.17    qed
    3.18  
    3.19    -- "Now show that A is bounded above ..."
    3.20 -  moreover have "\<exists>y. isUb (UNIV::real set) A y"
    3.21 +  moreover have "bdd_above A"
    3.22    proof -
    3.23      {
    3.24        fix n
    3.25 @@ -177,18 +175,11 @@
    3.26        obtain a and b where "f 0 = closed_int a b" and alb: "a \<le> b" by blast
    3.27      ultimately have "\<forall>n. ?g n \<in> closed_int a b" by auto
    3.28      with alb have "\<forall>n. ?g n \<le> b" using closed_int_most by blast
    3.29 -    with Adef have "\<forall>y\<in>A. y\<le>b" by auto
    3.30 -    hence "A *<= b" by (unfold setle_def)
    3.31 -    moreover have "b \<in> (UNIV::real set)" by simp
    3.32 -    ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
    3.33 -    hence "isUb (UNIV::real set) A b" by (unfold isUb_def)
    3.34 -    thus ?thesis by auto
    3.35 +    with Adef show "bdd_above A" by auto
    3.36    qed
    3.37 -  -- "by the Axiom Of Completeness, A has a least upper bound ..."
    3.38 -  ultimately have "\<exists>t. isLub UNIV A t" by (rule reals_complete)
    3.39  
    3.40    -- "denote this least upper bound as t ..."
    3.41 -  then obtain t where tdef: "isLub UNIV A t" ..
    3.42 +  def tdef: t == "Sup A"
    3.43  
    3.44    -- "and finally show that this least upper bound is in all the intervals..."
    3.45    have "\<forall>n. t \<in> f n"
    3.46 @@ -229,82 +220,76 @@
    3.47          with Adef have "(?g n) \<in> A" by auto
    3.48          ultimately show ?thesis by simp
    3.49        qed 
    3.50 -      with tdef show "a \<le> t" by (rule isLubD2)
    3.51 +      with `bdd_above A` show "a \<le> t"
    3.52 +        unfolding tdef by (intro cSup_upper)
    3.53      qed
    3.54      moreover have "t \<le> b"
    3.55 -    proof -
    3.56 -      have "isUb UNIV A b"
    3.57 -      proof -
    3.58 -        {
    3.59 -          from alb int have
    3.60 -            ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
    3.61 -          
    3.62 -          have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
    3.63 -          proof (rule allI, induct_tac m)
    3.64 -            show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
    3.65 -          next
    3.66 -            fix m n
    3.67 -            assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
    3.68 -            {
    3.69 -              fix p
    3.70 -              from pp have "f (p + n) \<subseteq> f p" by simp
    3.71 -              moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
    3.72 -              hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
    3.73 -              ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
    3.74 -            }
    3.75 -            thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
    3.76 -          qed 
    3.77 -          have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
    3.78 -          proof ((rule allI)+, rule impI)
    3.79 -            fix \<alpha>::nat and \<beta>::nat
    3.80 -            assume "\<beta> \<le> \<alpha>"
    3.81 -            hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
    3.82 -            then obtain k where "\<alpha> = \<beta> + k" ..
    3.83 -            moreover
    3.84 -            from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
    3.85 -            ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
    3.86 -          qed 
    3.87 -          
    3.88 -          fix m   
    3.89 +      unfolding tdef
    3.90 +    proof (rule cSup_least)
    3.91 +      {
    3.92 +        from alb int have
    3.93 +          ain: "b\<in>f n \<and> (\<forall>x\<in>f n. x \<le> b)" using closed_int_most by blast
    3.94 +        
    3.95 +        have subsetd: "\<forall>m. \<forall>n. f (n + m) \<subseteq> f n"
    3.96 +        proof (rule allI, induct_tac m)
    3.97 +          show "\<forall>n. f (n + 0) \<subseteq> f n" by simp
    3.98 +        next
    3.99 +          fix m n
   3.100 +          assume pp: "\<forall>p. f (p + n) \<subseteq> f p"
   3.101            {
   3.102 -            assume "m \<ge> n"
   3.103 -            with subsetm have "f m \<subseteq> f n" by simp
   3.104 -            with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   3.105 -            moreover
   3.106 -            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   3.107 -            ultimately have "?g m \<le> b" by auto
   3.108 +            fix p
   3.109 +            from pp have "f (p + n) \<subseteq> f p" by simp
   3.110 +            moreover from subset have "f (Suc (p + n)) \<subseteq> f (p + n)" by auto
   3.111 +            hence "f (p + (Suc n)) \<subseteq> f (p + n)" by simp
   3.112 +            ultimately have "f (p + (Suc n)) \<subseteq> f p" by simp
   3.113            }
   3.114 +          thus "\<forall>p. f (p + Suc n) \<subseteq> f p" ..
   3.115 +        qed 
   3.116 +        have subsetm: "\<forall>\<alpha> \<beta>. \<alpha> \<ge> \<beta> \<longrightarrow> (f \<alpha>) \<subseteq> (f \<beta>)"
   3.117 +        proof ((rule allI)+, rule impI)
   3.118 +          fix \<alpha>::nat and \<beta>::nat
   3.119 +          assume "\<beta> \<le> \<alpha>"
   3.120 +          hence "\<exists>k. \<alpha> = \<beta> + k" by (simp only: le_iff_add)
   3.121 +          then obtain k where "\<alpha> = \<beta> + k" ..
   3.122 +          moreover
   3.123 +          from subsetd have "f (\<beta> + k) \<subseteq> f \<beta>" by simp
   3.124 +          ultimately show "f \<alpha> \<subseteq> f \<beta>" by auto
   3.125 +        qed 
   3.126 +        
   3.127 +        fix m   
   3.128 +        {
   3.129 +          assume "m \<ge> n"
   3.130 +          with subsetm have "f m \<subseteq> f n" by simp
   3.131 +          with ain have "\<forall>x\<in>f m. x \<le> b" by auto
   3.132            moreover
   3.133 -          {
   3.134 -            assume "\<not>(m \<ge> n)"
   3.135 -            hence "m < n" by simp
   3.136 -            with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   3.137 -            from closed obtain ma and mb where
   3.138 -              "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   3.139 -            hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   3.140 -            from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   3.141 -            moreover have "(?g m) = ma"
   3.142 -            proof -
   3.143 -              from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   3.144 -              moreover from one have
   3.145 -                "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   3.146 -                by (rule closed_int_least)
   3.147 -              with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   3.148 -              ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   3.149 -              thus "?g m = ma" by auto
   3.150 -            qed
   3.151 -            ultimately have "?g m \<le> b" by simp
   3.152 -          } 
   3.153 -          ultimately have "?g m \<le> b" by (rule case_split)
   3.154 +          from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" by simp
   3.155 +          ultimately have "?g m \<le> b" by auto
   3.156          }
   3.157 -        with Adef have "\<forall>y\<in>A. y\<le>b" by auto
   3.158 -        hence "A *<= b" by (unfold setle_def)
   3.159 -        moreover have "b \<in> (UNIV::real set)" by simp
   3.160 -        ultimately have "A *<= b \<and> b \<in> (UNIV::real set)" by simp
   3.161 -        thus "isUb (UNIV::real set) A b" by (unfold isUb_def)
   3.162 -      qed
   3.163 -      with tdef show "t \<le> b" by (rule isLub_le_isUb)
   3.164 -    qed
   3.165 +        moreover
   3.166 +        {
   3.167 +          assume "\<not>(m \<ge> n)"
   3.168 +          hence "m < n" by simp
   3.169 +          with subsetm have sub: "(f n) \<subseteq> (f m)" by simp
   3.170 +          from closed obtain ma and mb where
   3.171 +            "f m = closed_int ma mb \<and> ma \<le> mb" by blast
   3.172 +          hence one: "ma \<le> mb" and fm: "f m = closed_int ma mb" by auto 
   3.173 +          from one alb sub fm int have "ma \<le> b" using closed_subset by blast
   3.174 +          moreover have "(?g m) = ma"
   3.175 +          proof -
   3.176 +            from gdef have "?g m \<in> f m \<and> (\<forall>x\<in>f m. ?g m \<le> x)" ..
   3.177 +            moreover from one have
   3.178 +              "ma \<in> closed_int ma mb \<and> (\<forall>x\<in>closed_int ma mb. ma \<le> x)"
   3.179 +              by (rule closed_int_least)
   3.180 +            with fm have "ma\<in>f m \<and> (\<forall>x\<in>f m. ma \<le> x)" by simp
   3.181 +            ultimately have "ma \<le> ?g m \<and> ?g m \<le> ma" by auto
   3.182 +            thus "?g m = ma" by auto
   3.183 +          qed
   3.184 +          ultimately have "?g m \<le> b" by simp
   3.185 +        } 
   3.186 +        ultimately have "?g m \<le> b" by (rule case_split)
   3.187 +      }
   3.188 +      with Adef show "\<And>y. y \<in> A \<Longrightarrow> y \<le> b" by auto
   3.189 +    qed fact
   3.190      ultimately have "t \<in> closed_int a b" by (rule closed_mem)
   3.191      with int show "t \<in> f n" by simp
   3.192    qed
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 05 09:45:00 2013 +0100
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Tue Nov 05 09:45:02 2013 +0100
     4.3 @@ -451,7 +451,7 @@
     4.4  
     4.5  definition
     4.6    dist_fps_def: "dist (a::'a fps) b =
     4.7 -    (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ The (leastP (\<lambda>n. a$n \<noteq> b$n))) else 0)"
     4.8 +    (if (\<exists>n. a$n \<noteq> b$n) then inverse (2 ^ (LEAST n. a$n \<noteq> b$n)) else 0)"
     4.9  
    4.10  lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
    4.11    by (simp add: dist_fps_def)
    4.12 @@ -467,34 +467,6 @@
    4.13  
    4.14  end
    4.15  
    4.16 -lemma fps_nonzero_least_unique:
    4.17 -  assumes a0: "a \<noteq> 0"
    4.18 -  shows "\<exists>!n. leastP (\<lambda>n. a$n \<noteq> 0) n"
    4.19 -proof -
    4.20 -  from fps_nonzero_nth_minimal [of a] a0
    4.21 -  obtain n where "a$n \<noteq> 0" "\<forall>m < n. a$m = 0" by blast
    4.22 -  then have ln: "leastP (\<lambda>n. a$n \<noteq> 0) n"
    4.23 -    by (auto simp add: leastP_def setge_def not_le [symmetric])
    4.24 -  moreover
    4.25 -  {
    4.26 -    fix m
    4.27 -    assume "leastP (\<lambda>n. a $ n \<noteq> 0) m"
    4.28 -    then have "m = n" using ln
    4.29 -      apply (auto simp add: leastP_def setge_def)
    4.30 -      apply (erule allE[where x=n])
    4.31 -      apply (erule allE[where x=m])
    4.32 -      apply simp
    4.33 -      done
    4.34 -  }
    4.35 -  ultimately show ?thesis by blast
    4.36 -qed
    4.37 -
    4.38 -lemma fps_eq_least_unique:
    4.39 -  assumes "(a::('a::ab_group_add) fps) \<noteq> b"
    4.40 -  shows "\<exists>! n. leastP (\<lambda>n. a$n \<noteq> b$n) n"
    4.41 -  using fps_nonzero_least_unique[of "a - b"] assms
    4.42 -  by auto
    4.43 -
    4.44  instantiation fps :: (comm_ring_1) metric_space
    4.45  begin
    4.46  
    4.47 @@ -540,31 +512,15 @@
    4.48    moreover
    4.49    {
    4.50      assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
    4.51 -    let ?P = "\<lambda>a b n. a$n \<noteq> b$n"
    4.52 -    from fps_eq_least_unique[OF ab] fps_eq_least_unique[OF ac]
    4.53 -      fps_eq_least_unique[OF bc]
    4.54 -    obtain nab nac nbc where nab: "leastP (?P a b) nab"
    4.55 -      and nac: "leastP (?P a c) nac"
    4.56 -      and nbc: "leastP (?P b c) nbc" by blast
    4.57 -    from nab have nab': "\<And>m. m < nab \<Longrightarrow> a$m = b$m" "a$nab \<noteq> b$nab"
    4.58 -      by (auto simp add: leastP_def setge_def)
    4.59 -    from nac have nac': "\<And>m. m < nac \<Longrightarrow> a$m = c$m" "a$nac \<noteq> c$nac"
    4.60 -      by (auto simp add: leastP_def setge_def)
    4.61 -    from nbc have nbc': "\<And>m. m < nbc \<Longrightarrow> b$m = c$m" "b$nbc \<noteq> c$nbc"
    4.62 -      by (auto simp add: leastP_def setge_def)
    4.63 -
    4.64 -    have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
    4.65 -      by (simp add: fps_eq_iff)
    4.66 -    from ab ac bc nab nac nbc
    4.67 -    have dab: "dist a b = inverse (2 ^ nab)"
    4.68 -      and dac: "dist a c = inverse (2 ^ nac)"
    4.69 -      and dbc: "dist b c = inverse (2 ^ nbc)"
    4.70 -      unfolding th0
    4.71 -      apply (simp_all add: dist_fps_def)
    4.72 -      apply (erule the1_equality[OF fps_eq_least_unique[OF ab]])
    4.73 -      apply (erule the1_equality[OF fps_eq_least_unique[OF ac]])
    4.74 -      apply (erule the1_equality[OF fps_eq_least_unique[OF bc]])
    4.75 -      done
    4.76 +    def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n"
    4.77 +    then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m"
    4.78 +      by (auto dest: not_less_Least)
    4.79 +
    4.80 +    from ab ac bc
    4.81 +    have dab: "dist a b = inverse (2 ^ n a b)"
    4.82 +      and dac: "dist a c = inverse (2 ^ n a c)"
    4.83 +      and dbc: "dist b c = inverse (2 ^ n b c)"
    4.84 +      by (simp_all add: dist_fps_def n_def fps_eq_iff)
    4.85      from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0"
    4.86        unfolding th by simp_all
    4.87      from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0"
    4.88 @@ -575,11 +531,13 @@
    4.89        assume h: "dist a b > dist a c + dist b c"
    4.90        then have gt: "dist a b > dist a c" "dist a b > dist b c"
    4.91          using pos by auto
    4.92 -      from gt have gtn: "nab < nbc" "nab < nac"
    4.93 +      from gt have gtn: "n a b < n b c" "n a b < n a c"
    4.94          unfolding dab dbc dac by (auto simp add: th1)
    4.95 -      from nac'(1)[OF gtn(2)] nbc'(1)[OF gtn(1)]
    4.96 -      have "a $ nab = b $ nab" by simp
    4.97 -      with nab'(2) have False  by simp
    4.98 +      from n'[OF gtn(2)] n'(1)[OF gtn(1)]
    4.99 +      have "a $ n a b = b $ n a b" by simp
   4.100 +      moreover have "a $ n a b \<noteq> b $ n a b"
   4.101 +         unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff)
   4.102 +      ultimately have False by contradiction
   4.103      }
   4.104      then have "dist a b \<le> dist a c + dist b c"
   4.105        by (auto simp add: not_le[symmetric])
   4.106 @@ -649,17 +607,12 @@
   4.107        moreover
   4.108        {
   4.109          assume neq: "?s n \<noteq> a"
   4.110 -        from fps_eq_least_unique[OF neq]
   4.111 -        obtain k where k: "leastP (\<lambda>i. ?s n $ i \<noteq> a$i) k" by blast
   4.112 -        have th0: "\<And>(a::'a fps) b. a \<noteq> b \<longleftrightarrow> (\<exists>n. a$n \<noteq> b$n)"
   4.113 -          by (simp add: fps_eq_iff)
   4.114 +        def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i"
   4.115          from neq have dth: "dist (?s n) a = (1/2)^k"
   4.116 -          unfolding th0 dist_fps_def
   4.117 -          unfolding the1_equality[OF fps_eq_least_unique[OF neq], OF k]
   4.118 -          by (auto simp add: inverse_eq_divide power_divide)
   4.119 -
   4.120 -        from k have kn: "k > n"
   4.121 -          by (simp add: leastP_def setge_def fps_sum_rep_nth split:split_if_asm)
   4.122 +          by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff)
   4.123 +
   4.124 +        from neq have kn: "k > n"
   4.125 +          by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex)
   4.126          then have "dist (?s n) a < (1/2)^n" unfolding dth
   4.127            by (auto intro: power_strict_decreasing)
   4.128          also have "\<dots> <= (1/2)^n0" using nn0
   4.129 @@ -3797,20 +3750,14 @@
   4.130    assumes "dist f g < inverse (2 ^ i)"
   4.131      and"j \<le> i"
   4.132    shows "f $ j = g $ j"
   4.133 -proof (cases "f = g")
   4.134 -  case False
   4.135 -  hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
   4.136 -  with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
   4.137 +proof (rule ccontr)
   4.138 +  assume "f $ j \<noteq> g $ j"
   4.139 +  then have "\<exists>n. f $ n \<noteq> g $ n" by auto
   4.140 +  with assms have "i < (LEAST n. f $ n \<noteq> g $ n)"
   4.141      by (simp add: split_if_asm dist_fps_def)
   4.142 -  moreover
   4.143 -  from fps_eq_least_unique[OF `f \<noteq> g`]
   4.144 -  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
   4.145 -  moreover from n have "\<And>m. m < n \<Longrightarrow> f$m = g$m" "f$n \<noteq> g$n"
   4.146 -    by (auto simp add: leastP_def setge_def)
   4.147 -  ultimately show ?thesis using `j \<le> i` by simp
   4.148 -next
   4.149 -  case True
   4.150 -  then show ?thesis by simp
   4.151 +  also have "\<dots> \<le> j"
   4.152 +    using `f $ j \<noteq> g $ j` by (auto intro: Least_le)
   4.153 +  finally show False using `j \<le> i` by simp
   4.154  qed
   4.155  
   4.156  lemma nth_equal_imp_dist_less:
   4.157 @@ -3819,18 +3766,13 @@
   4.158  proof (cases "f = g")
   4.159    case False
   4.160    hence "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff)
   4.161 -  with assms have "dist f g = inverse (2 ^ (The (leastP (\<lambda>n. f $ n \<noteq> g $ n))))"
   4.162 +  with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))"
   4.163      by (simp add: split_if_asm dist_fps_def)
   4.164    moreover
   4.165 -  from fps_eq_least_unique[OF `f \<noteq> g`]
   4.166 -  obtain n where "leastP (\<lambda>n. f$n \<noteq> g$n) n" "The (leastP (\<lambda>n. f $ n \<noteq> g $ n)) = n" by blast
   4.167 -  with assms have "i < The (leastP (\<lambda>n. f $ n \<noteq> g $ n))"
   4.168 -    by (metis (full_types) leastPD1 not_le)
   4.169 +  from assms `\<exists>n. f $ n \<noteq> g $ n` have "i < (LEAST n. f $ n \<noteq> g $ n)"
   4.170 +    by (metis (mono_tags) LeastI not_less)
   4.171    ultimately show ?thesis by simp
   4.172 -next
   4.173 -  case True
   4.174 -  then show ?thesis by simp
   4.175 -qed
   4.176 +qed simp
   4.177  
   4.178  lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)"
   4.179    using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast
     5.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 05 09:45:00 2013 +0100
     5.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Nov 05 09:45:02 2013 +0100
     5.3 @@ -156,28 +156,11 @@
     5.4  text{* An alternative useful formulation of completeness of the reals *}
     5.5  lemma real_sup_exists: assumes ex: "\<exists>x. P x" and bz: "\<exists>z. \<forall>x. P x \<longrightarrow> x < z"
     5.6    shows "\<exists>(s::real). \<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < s"
     5.7 -proof-
     5.8 -  from ex bz obtain x Y where x: "P x" and Y: "\<And>x. P x \<Longrightarrow> x < Y"  by blast
     5.9 -  from ex have thx:"\<exists>x. x \<in> Collect P" by blast
    5.10 -  from bz have thY: "\<exists>Y. isUb UNIV (Collect P) Y"
    5.11 -    by(auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def order_le_less)
    5.12 -  from reals_complete[OF thx thY] obtain L where L: "isLub UNIV (Collect P) L"
    5.13 -    by blast
    5.14 -  from Y[OF x] have xY: "x < Y" .
    5.15 -  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)
    5.16 -  from Y have Y': "\<forall>x. P x \<longrightarrow> x \<le> Y"
    5.17 -    apply (clarsimp, atomize (full)) by auto
    5.18 -  from L Y' have "L \<le> Y" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    5.19 -  {fix y
    5.20 -    {fix z assume z: "P z" "y < z"
    5.21 -      from L' z have "y < L" by auto }
    5.22 -    moreover
    5.23 -    {assume yL: "y < L" "\<forall>z. P z \<longrightarrow> \<not> y < z"
    5.24 -      hence nox: "\<forall>z. P z \<longrightarrow> y \<ge> z" by auto
    5.25 -      from nox L have "y \<ge> L" by (auto simp add: isUb_def isLub_def setge_def setle_def leastP_def Ball_def)
    5.26 -      with yL(1) have False  by arith}
    5.27 -    ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
    5.28 -  thus ?thesis by blast
    5.29 +proof
    5.30 +  from bz have "bdd_above (Collect P)"
    5.31 +    by (force intro: less_imp_le)
    5.32 +  then show "\<forall>y. (\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < Sup (Collect P)"
    5.33 +    using ex bz by (subst less_cSup_iff) auto
    5.34  qed
    5.35  
    5.36  subsection {* Fundamental theorem of algebra *}
     6.1 --- a/src/HOL/Library/Glbs.thy	Tue Nov 05 09:45:00 2013 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,79 +0,0 @@
     6.4 -(* Author: Amine Chaieb, University of Cambridge *)
     6.5 -
     6.6 -header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
     6.7 -
     6.8 -theory Glbs
     6.9 -imports Lubs
    6.10 -begin
    6.11 -
    6.12 -definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
    6.13 -  where "greatestP P x = (P x \<and> Collect P *<=  x)"
    6.14 -
    6.15 -definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    6.16 -  where "isLb R S x = (x <=* S \<and> x: R)"
    6.17 -
    6.18 -definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    6.19 -  where "isGlb R S x = greatestP (isLb R S) x"
    6.20 -
    6.21 -definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
    6.22 -  where "lbs R S = Collect (isLb R S)"
    6.23 -
    6.24 -
    6.25 -subsection {* Rules about the Operators @{term greatestP}, @{term isLb}
    6.26 -  and @{term isGlb} *}
    6.27 -
    6.28 -lemma leastPD1: "greatestP P x \<Longrightarrow> P x"
    6.29 -  by (simp add: greatestP_def)
    6.30 -
    6.31 -lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
    6.32 -  by (simp add: greatestP_def)
    6.33 -
    6.34 -lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
    6.35 -  by (blast dest!: greatestPD2 setleD)
    6.36 -
    6.37 -lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
    6.38 -  by (simp add: isGlb_def isLb_def greatestP_def)
    6.39 -
    6.40 -lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
    6.41 -  by (simp add: isGlb_def isLb_def greatestP_def)
    6.42 -
    6.43 -lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
    6.44 -  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
    6.45 -
    6.46 -lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
    6.47 -  by (blast dest!: isGlbD1 setgeD)
    6.48 -
    6.49 -lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
    6.50 -  by (simp add: isGlb_def)
    6.51 -
    6.52 -lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
    6.53 -  by (simp add: isGlb_def)
    6.54 -
    6.55 -lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
    6.56 -  by (simp add: isGlb_def greatestP_def)
    6.57 -
    6.58 -lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
    6.59 -  by (simp add: isLb_def setge_def)
    6.60 -
    6.61 -lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
    6.62 -  by (simp add: isLb_def)
    6.63 -
    6.64 -lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
    6.65 -  by (simp add: isLb_def)
    6.66 -
    6.67 -lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
    6.68 -  by (simp add: isLb_def)
    6.69 -
    6.70 -lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
    6.71 -  unfolding isGlb_def by (blast intro!: greatestPD3)
    6.72 -
    6.73 -lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
    6.74 -  unfolding lbs_def isGlb_def by (rule greatestPD2)
    6.75 -
    6.76 -lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
    6.77 -  apply (frule isGlb_isLb)
    6.78 -  apply (frule_tac x = y in isGlb_isLb)
    6.79 -  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
    6.80 -  done
    6.81 -
    6.82 -end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Library/Lubs_Glbs.thy	Tue Nov 05 09:45:02 2013 +0100
     7.3 @@ -0,0 +1,245 @@
     7.4 +(*  Title:      HOL/Library/Lubs_Glbs.thy
     7.5 +    Author:     Jacques D. Fleuriot, University of Cambridge
     7.6 +    Author:     Amine Chaieb, University of Cambridge *)
     7.7 +
     7.8 +header {* Definitions of Least Upper Bounds and Greatest Lower Bounds *}
     7.9 +
    7.10 +theory Lubs_Glbs
    7.11 +imports Complex_Main
    7.12 +begin
    7.13 +
    7.14 +text {* Thanks to suggestions by James Margetson *}
    7.15 +
    7.16 +definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
    7.17 +  where "S *<= x = (ALL y: S. y \<le> x)"
    7.18 +
    7.19 +definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
    7.20 +  where "x <=* S = (ALL y: S. x \<le> y)"
    7.21 +
    7.22 +
    7.23 +subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
    7.24 +
    7.25 +lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
    7.26 +  by (simp add: setle_def)
    7.27 +
    7.28 +lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
    7.29 +  by (simp add: setle_def)
    7.30 +
    7.31 +lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
    7.32 +  by (simp add: setge_def)
    7.33 +
    7.34 +lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
    7.35 +  by (simp add: setge_def)
    7.36 +
    7.37 +
    7.38 +definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
    7.39 +  where "leastP P x = (P x \<and> x <=* Collect P)"
    7.40 +
    7.41 +definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    7.42 +  where "isUb R S x = (S *<= x \<and> x: R)"
    7.43 +
    7.44 +definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
    7.45 +  where "isLub R S x = leastP (isUb R S) x"
    7.46 +
    7.47 +definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
    7.48 +  where "ubs R S = Collect (isUb R S)"
    7.49 +
    7.50 +
    7.51 +subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
    7.52 +
    7.53 +lemma leastPD1: "leastP P x \<Longrightarrow> P x"
    7.54 +  by (simp add: leastP_def)
    7.55 +
    7.56 +lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
    7.57 +  by (simp add: leastP_def)
    7.58 +
    7.59 +lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
    7.60 +  by (blast dest!: leastPD2 setgeD)
    7.61 +
    7.62 +lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
    7.63 +  by (simp add: isLub_def isUb_def leastP_def)
    7.64 +
    7.65 +lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
    7.66 +  by (simp add: isLub_def isUb_def leastP_def)
    7.67 +
    7.68 +lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
    7.69 +  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
    7.70 +
    7.71 +lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
    7.72 +  by (blast dest!: isLubD1 setleD)
    7.73 +
    7.74 +lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
    7.75 +  by (simp add: isLub_def)
    7.76 +
    7.77 +lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
    7.78 +  by (simp add: isLub_def)
    7.79 +
    7.80 +lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
    7.81 +  by (simp add: isLub_def leastP_def)
    7.82 +
    7.83 +lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
    7.84 +  by (simp add: isUb_def setle_def)
    7.85 +
    7.86 +lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
    7.87 +  by (simp add: isUb_def)
    7.88 +
    7.89 +lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
    7.90 +  by (simp add: isUb_def)
    7.91 +
    7.92 +lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
    7.93 +  by (simp add: isUb_def)
    7.94 +
    7.95 +lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
    7.96 +  unfolding isLub_def by (blast intro!: leastPD3)
    7.97 +
    7.98 +lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
    7.99 +  unfolding ubs_def isLub_def by (rule leastPD2)
   7.100 +
   7.101 +lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
   7.102 +  apply (frule isLub_isUb)
   7.103 +  apply (frule_tac x = y in isLub_isUb)
   7.104 +  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
   7.105 +  done
   7.106 +
   7.107 +lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
   7.108 +  by (simp add: isUbI setleI)
   7.109 +
   7.110 +
   7.111 +definition greatestP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
   7.112 +  where "greatestP P x = (P x \<and> Collect P *<=  x)"
   7.113 +
   7.114 +definition isLb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
   7.115 +  where "isLb R S x = (x <=* S \<and> x: R)"
   7.116 +
   7.117 +definition isGlb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
   7.118 +  where "isGlb R S x = greatestP (isLb R S) x"
   7.119 +
   7.120 +definition lbs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
   7.121 +  where "lbs R S = Collect (isLb R S)"
   7.122 +
   7.123 +
   7.124 +subsection {* Rules about the Operators @{term greatestP}, @{term isLb} and @{term isGlb} *}
   7.125 +
   7.126 +lemma greatestPD1: "greatestP P x \<Longrightarrow> P x"
   7.127 +  by (simp add: greatestP_def)
   7.128 +
   7.129 +lemma greatestPD2: "greatestP P x \<Longrightarrow> Collect P *<= x"
   7.130 +  by (simp add: greatestP_def)
   7.131 +
   7.132 +lemma greatestPD3: "greatestP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<ge> y"
   7.133 +  by (blast dest!: greatestPD2 setleD)
   7.134 +
   7.135 +lemma isGlbD1: "isGlb R S x \<Longrightarrow> x <=* S"
   7.136 +  by (simp add: isGlb_def isLb_def greatestP_def)
   7.137 +
   7.138 +lemma isGlbD1a: "isGlb R S x \<Longrightarrow> x: R"
   7.139 +  by (simp add: isGlb_def isLb_def greatestP_def)
   7.140 +
   7.141 +lemma isGlb_isLb: "isGlb R S x \<Longrightarrow> isLb R S x"
   7.142 +  unfolding isLb_def by (blast dest: isGlbD1 isGlbD1a)
   7.143 +
   7.144 +lemma isGlbD2: "isGlb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
   7.145 +  by (blast dest!: isGlbD1 setgeD)
   7.146 +
   7.147 +lemma isGlbD3: "isGlb R S x \<Longrightarrow> greatestP (isLb R S) x"
   7.148 +  by (simp add: isGlb_def)
   7.149 +
   7.150 +lemma isGlbI1: "greatestP (isLb R S) x \<Longrightarrow> isGlb R S x"
   7.151 +  by (simp add: isGlb_def)
   7.152 +
   7.153 +lemma isGlbI2: "isLb R S x \<Longrightarrow> Collect (isLb R S) *<= x \<Longrightarrow> isGlb R S x"
   7.154 +  by (simp add: isGlb_def greatestP_def)
   7.155 +
   7.156 +lemma isLbD: "isLb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<ge> x"
   7.157 +  by (simp add: isLb_def setge_def)
   7.158 +
   7.159 +lemma isLbD2: "isLb R S x \<Longrightarrow> x <=* S "
   7.160 +  by (simp add: isLb_def)
   7.161 +
   7.162 +lemma isLbD2a: "isLb R S x \<Longrightarrow> x: R"
   7.163 +  by (simp add: isLb_def)
   7.164 +
   7.165 +lemma isLbI: "x <=* S \<Longrightarrow> x: R \<Longrightarrow> isLb R S x"
   7.166 +  by (simp add: isLb_def)
   7.167 +
   7.168 +lemma isGlb_le_isLb: "isGlb R S x \<Longrightarrow> isLb R S y \<Longrightarrow> x \<ge> y"
   7.169 +  unfolding isGlb_def by (blast intro!: greatestPD3)
   7.170 +
   7.171 +lemma isGlb_ubs: "isGlb R S x \<Longrightarrow> lbs R S *<= x"
   7.172 +  unfolding lbs_def isGlb_def by (rule greatestPD2)
   7.173 +
   7.174 +lemma isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::'a::linorder)"
   7.175 +  apply (frule isGlb_isLb)
   7.176 +  apply (frule_tac x = y in isGlb_isLb)
   7.177 +  apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   7.178 +  done
   7.179 +
   7.180 +lemma bdd_above_setle: "bdd_above A \<longleftrightarrow> (\<exists>a. A *<= a)"
   7.181 +  by (auto simp: bdd_above_def setle_def)
   7.182 +
   7.183 +lemma bdd_below_setge: "bdd_below A \<longleftrightarrow> (\<exists>a. a <=* A)"
   7.184 +  by (auto simp: bdd_below_def setge_def)
   7.185 +
   7.186 +lemma isLub_cSup: 
   7.187 +  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   7.188 +  by  (auto simp add: isLub_def setle_def leastP_def isUb_def
   7.189 +            intro!: setgeI cSup_upper cSup_least)
   7.190 +
   7.191 +lemma isGlb_cInf: 
   7.192 +  "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
   7.193 +  by  (auto simp add: isGlb_def setge_def greatestP_def isLb_def
   7.194 +            intro!: setleI cInf_lower cInf_greatest)
   7.195 +
   7.196 +lemma cSup_le: "(S::'a::conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   7.197 +  by (metis cSup_least setle_def)
   7.198 +
   7.199 +lemma cInf_ge: "(S::'a :: conditionally_complete_lattice set) \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   7.200 +  by (metis cInf_greatest setge_def)
   7.201 +
   7.202 +lemma cSup_bounds:
   7.203 +  fixes S :: "'a :: conditionally_complete_lattice set"
   7.204 +  shows "S \<noteq> {} \<Longrightarrow> a <=* S \<Longrightarrow> S *<= b \<Longrightarrow> a \<le> Sup S \<and> Sup S \<le> b"
   7.205 +  using cSup_least[of S b] cSup_upper2[of _ S a]
   7.206 +  by (auto simp: bdd_above_setle setge_def setle_def)
   7.207 +
   7.208 +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"
   7.209 +  by (rule cSup_eq) (auto simp: not_le[symmetric] setle_def)
   7.210 +
   7.211 +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"
   7.212 +  by (rule cInf_eq) (auto simp: not_le[symmetric] setge_def)
   7.213 +
   7.214 +text{* Use completeness of reals (supremum property) to show that any bounded sequence has a least upper bound*}
   7.215 +
   7.216 +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"
   7.217 +  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
   7.218 +
   7.219 +lemma Bseq_isUb: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
   7.220 +  by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
   7.221 +
   7.222 +lemma Bseq_isLub: "\<And>X :: nat \<Rightarrow> real. Bseq X \<Longrightarrow> \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
   7.223 +  by (blast intro: reals_complete Bseq_isUb)
   7.224 +
   7.225 +lemma isLub_mono_imp_LIMSEQ:
   7.226 +  fixes X :: "nat \<Rightarrow> real"
   7.227 +  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
   7.228 +  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
   7.229 +  shows "X ----> u"
   7.230 +proof -
   7.231 +  have "X ----> (SUP i. X i)"
   7.232 +    using u[THEN isLubD1] X
   7.233 +    by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
   7.234 +  also have "(SUP i. X i) = u"
   7.235 +    using isLub_cSup[of "range X"] u[THEN isLubD1]
   7.236 +    by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
   7.237 +  finally show ?thesis .
   7.238 +qed
   7.239 +
   7.240 +lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
   7.241 +
   7.242 +lemma real_le_inf_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. b <=* s \<Longrightarrow> Inf s \<le> Inf (t::real set)"
   7.243 +  by (rule cInf_superset_mono) (auto simp: bdd_below_setge)
   7.244 +
   7.245 +lemma real_ge_sup_subset: "t \<noteq> {} \<Longrightarrow> t \<subseteq> s \<Longrightarrow> \<exists>b. s *<= b \<Longrightarrow> Sup s \<ge> Sup (t::real set)"
   7.246 +  by (rule cSup_subset_mono) (auto simp: bdd_above_setle)
   7.247 +
   7.248 +end
     8.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Nov 05 09:45:00 2013 +0100
     8.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Nov 05 09:45:02 2013 +0100
     8.3 @@ -756,7 +756,8 @@
     8.4  declare Inf_Set_fold[folded Inf'_def, code]
     8.5  
     8.6  lemma INFI_Set_fold [code]:
     8.7 -  "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
     8.8 +  fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
     8.9 +  shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
    8.10  proof -
    8.11    have "comp_fun_commute ((inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
    8.12      by default (auto simp add: fun_eq_iff ac_simps)
    8.13 @@ -796,7 +797,8 @@
    8.14  declare Sup_Set_fold[folded Sup'_def, code]
    8.15  
    8.16  lemma SUPR_Set_fold [code]:
    8.17 -  "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
    8.18 +  fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
    8.19 +  shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
    8.20  proof -
    8.21    have "comp_fun_commute ((sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a) \<circ> f)" 
    8.22      by default (auto simp add: fun_eq_iff ac_simps)
     9.1 --- a/src/HOL/Limits.thy	Tue Nov 05 09:45:00 2013 +0100
     9.2 +++ b/src/HOL/Limits.thy	Tue Nov 05 09:45:02 2013 +0100
     9.3 @@ -138,6 +138,18 @@
     9.4  lemma BseqI: "[| 0 < K; \<forall>n. norm (X n) \<le> K |] ==> Bseq X"
     9.5  by (auto simp add: Bseq_def)
     9.6  
     9.7 +lemma Bseq_bdd_above: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_above (range X)"
     9.8 +proof (elim BseqE, intro bdd_aboveI2)
     9.9 +  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "X n \<le> K"
    9.10 +    by (auto elim!: allE[of _ n])
    9.11 +qed
    9.12 +
    9.13 +lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
    9.14 +proof (elim BseqE, intro bdd_belowI2)
    9.15 +  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
    9.16 +    by (auto elim!: allE[of _ n])
    9.17 +qed
    9.18 +
    9.19  lemma lemma_NBseq_def:
    9.20    "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    9.21  proof safe
    9.22 @@ -210,18 +222,6 @@
    9.23  
    9.24  subsubsection{*Upper Bounds and Lubs of Bounded Sequences*}
    9.25  
    9.26 -lemma Bseq_isUb:
    9.27 -  "!!(X::nat=>real). Bseq X ==> \<exists>U. isUb (UNIV::real set) {x. \<exists>n. X n = x} U"
    9.28 -by (auto intro: isUbI setleI simp add: Bseq_def abs_le_iff)
    9.29 -
    9.30 -text{* Use completeness of reals (supremum property)
    9.31 -   to show that any bounded sequence has a least upper bound*}
    9.32 -
    9.33 -lemma Bseq_isLub:
    9.34 -  "!!(X::nat=>real). Bseq X ==>
    9.35 -   \<exists>U. isLub (UNIV::real set) {x. \<exists>n. X n = x} U"
    9.36 -by (blast intro: reals_complete Bseq_isUb)
    9.37 -
    9.38  lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
    9.39    by (simp add: Bseq_def)
    9.40  
    9.41 @@ -1358,40 +1358,29 @@
    9.42  
    9.43  text {* A monotone sequence converges to its least upper bound. *}
    9.44  
    9.45 -lemma isLub_mono_imp_LIMSEQ:
    9.46 -  fixes X :: "nat \<Rightarrow> real"
    9.47 -  assumes u: "isLub UNIV {x. \<exists>n. X n = x} u" (* FIXME: use 'range X' *)
    9.48 -  assumes X: "\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n"
    9.49 -  shows "X ----> u"
    9.50 -proof (rule LIMSEQ_I)
    9.51 -  have 1: "\<forall>n. X n \<le> u"
    9.52 -    using isLubD2 [OF u] by auto
    9.53 -  have "\<forall>y. (\<forall>n. X n \<le> y) \<longrightarrow> u \<le> y"
    9.54 -    using isLub_le_isUb [OF u] by (auto simp add: isUb_def setle_def)
    9.55 -  hence 2: "\<forall>y<u. \<exists>n. y < X n"
    9.56 -    by (metis not_le)
    9.57 -  fix r :: real assume "0 < r"
    9.58 -  hence "u - r < u" by simp
    9.59 -  hence "\<exists>m. u - r < X m" using 2 by simp
    9.60 -  then obtain m where "u - r < X m" ..
    9.61 -  with X have "\<forall>n\<ge>m. u - r < X n"
    9.62 -    by (fast intro: less_le_trans)
    9.63 -  hence "\<exists>m. \<forall>n\<ge>m. u - r < X n" ..
    9.64 -  thus "\<exists>m. \<forall>n\<ge>m. norm (X n - u) < r"
    9.65 -    using 1 by (simp add: diff_less_eq add_commute)
    9.66 -qed
    9.67 +lemma LIMSEQ_incseq_SUP:
    9.68 +  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
    9.69 +  assumes u: "bdd_above (range X)"
    9.70 +  assumes X: "incseq X"
    9.71 +  shows "X ----> (SUP i. X i)"
    9.72 +  by (rule order_tendstoI)
    9.73 +     (auto simp: eventually_sequentially u less_cSUP_iff intro: X[THEN incseqD] less_le_trans cSUP_lessD[OF u])
    9.74  
    9.75 -text{*A standard proof of the theorem for monotone increasing sequence*}
    9.76 -
    9.77 -lemma Bseq_mono_convergent:
    9.78 -   "Bseq X \<Longrightarrow> \<forall>m. \<forall>n \<ge> m. X m \<le> X n \<Longrightarrow> convergent (X::nat=>real)"
    9.79 -  by (metis Bseq_isLub isLub_mono_imp_LIMSEQ convergentI)
    9.80 +lemma LIMSEQ_decseq_INF:
    9.81 +  fixes X :: "nat \<Rightarrow> 'a::{conditionally_complete_linorder, linorder_topology}"
    9.82 +  assumes u: "bdd_below (range X)"
    9.83 +  assumes X: "decseq X"
    9.84 +  shows "X ----> (INF i. X i)"
    9.85 +  by (rule order_tendstoI)
    9.86 +     (auto simp: eventually_sequentially u cINF_less_iff intro: X[THEN decseqD] le_less_trans less_cINF_D[OF u])
    9.87  
    9.88  text{*Main monotonicity theorem*}
    9.89  
    9.90  lemma Bseq_monoseq_convergent: "Bseq X \<Longrightarrow> monoseq X \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
    9.91 -  by (metis monoseq_iff incseq_def decseq_eq_incseq convergent_minus_iff Bseq_minus_iff
    9.92 -            Bseq_mono_convergent)
    9.93 +  by (auto simp: monoseq_iff convergent_def intro: LIMSEQ_decseq_INF LIMSEQ_incseq_SUP dest: Bseq_bdd_above Bseq_bdd_below)
    9.94 +
    9.95 +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)"
    9.96 +  by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
    9.97  
    9.98  lemma Cauchy_iff:
    9.99    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
    10.1 --- a/src/HOL/Lubs.thy	Tue Nov 05 09:45:00 2013 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,103 +0,0 @@
    10.4 -(*  Title:      HOL/Lubs.thy
    10.5 -    Author:     Jacques D. Fleuriot, University of Cambridge
    10.6 -*)
    10.7 -
    10.8 -header {* Definitions of Upper Bounds and Least Upper Bounds *}
    10.9 -
   10.10 -theory Lubs
   10.11 -imports Main
   10.12 -begin
   10.13 -
   10.14 -text {* Thanks to suggestions by James Margetson *}
   10.15 -
   10.16 -definition setle :: "'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"  (infixl "*<=" 70)
   10.17 -  where "S *<= x = (ALL y: S. y \<le> x)"
   10.18 -
   10.19 -definition setge :: "'a::ord \<Rightarrow> 'a set \<Rightarrow> bool"  (infixl "<=*" 70)
   10.20 -  where "x <=* S = (ALL y: S. x \<le> y)"
   10.21 -
   10.22 -definition leastP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a::ord \<Rightarrow> bool"
   10.23 -  where "leastP P x = (P x \<and> x <=* Collect P)"
   10.24 -
   10.25 -definition isUb :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
   10.26 -  where "isUb R S x = (S *<= x \<and> x: R)"
   10.27 -
   10.28 -definition isLub :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a::ord \<Rightarrow> bool"
   10.29 -  where "isLub R S x = leastP (isUb R S) x"
   10.30 -
   10.31 -definition ubs :: "'a set \<Rightarrow> 'a::ord set \<Rightarrow> 'a set"
   10.32 -  where "ubs R S = Collect (isUb R S)"
   10.33 -
   10.34 -
   10.35 -subsection {* Rules for the Relations @{text "*<="} and @{text "<=*"} *}
   10.36 -
   10.37 -lemma setleI: "ALL y: S. y \<le> x \<Longrightarrow> S *<= x"
   10.38 -  by (simp add: setle_def)
   10.39 -
   10.40 -lemma setleD: "S *<= x \<Longrightarrow> y: S \<Longrightarrow> y \<le> x"
   10.41 -  by (simp add: setle_def)
   10.42 -
   10.43 -lemma setgeI: "ALL y: S. x \<le> y \<Longrightarrow> x <=* S"
   10.44 -  by (simp add: setge_def)
   10.45 -
   10.46 -lemma setgeD: "x <=* S \<Longrightarrow> y: S \<Longrightarrow> x \<le> y"
   10.47 -  by (simp add: setge_def)
   10.48 -
   10.49 -
   10.50 -subsection {* Rules about the Operators @{term leastP}, @{term ub} and @{term lub} *}
   10.51 -
   10.52 -lemma leastPD1: "leastP P x \<Longrightarrow> P x"
   10.53 -  by (simp add: leastP_def)
   10.54 -
   10.55 -lemma leastPD2: "leastP P x \<Longrightarrow> x <=* Collect P"
   10.56 -  by (simp add: leastP_def)
   10.57 -
   10.58 -lemma leastPD3: "leastP P x \<Longrightarrow> y: Collect P \<Longrightarrow> x \<le> y"
   10.59 -  by (blast dest!: leastPD2 setgeD)
   10.60 -
   10.61 -lemma isLubD1: "isLub R S x \<Longrightarrow> S *<= x"
   10.62 -  by (simp add: isLub_def isUb_def leastP_def)
   10.63 -
   10.64 -lemma isLubD1a: "isLub R S x \<Longrightarrow> x: R"
   10.65 -  by (simp add: isLub_def isUb_def leastP_def)
   10.66 -
   10.67 -lemma isLub_isUb: "isLub R S x \<Longrightarrow> isUb R S x"
   10.68 -  unfolding isUb_def by (blast dest: isLubD1 isLubD1a)
   10.69 -
   10.70 -lemma isLubD2: "isLub R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
   10.71 -  by (blast dest!: isLubD1 setleD)
   10.72 -
   10.73 -lemma isLubD3: "isLub R S x \<Longrightarrow> leastP (isUb R S) x"
   10.74 -  by (simp add: isLub_def)
   10.75 -
   10.76 -lemma isLubI1: "leastP(isUb R S) x \<Longrightarrow> isLub R S x"
   10.77 -  by (simp add: isLub_def)
   10.78 -
   10.79 -lemma isLubI2: "isUb R S x \<Longrightarrow> x <=* Collect (isUb R S) \<Longrightarrow> isLub R S x"
   10.80 -  by (simp add: isLub_def leastP_def)
   10.81 -
   10.82 -lemma isUbD: "isUb R S x \<Longrightarrow> y : S \<Longrightarrow> y \<le> x"
   10.83 -  by (simp add: isUb_def setle_def)
   10.84 -
   10.85 -lemma isUbD2: "isUb R S x \<Longrightarrow> S *<= x"
   10.86 -  by (simp add: isUb_def)
   10.87 -
   10.88 -lemma isUbD2a: "isUb R S x \<Longrightarrow> x: R"
   10.89 -  by (simp add: isUb_def)
   10.90 -
   10.91 -lemma isUbI: "S *<= x \<Longrightarrow> x: R \<Longrightarrow> isUb R S x"
   10.92 -  by (simp add: isUb_def)
   10.93 -
   10.94 -lemma isLub_le_isUb: "isLub R S x \<Longrightarrow> isUb R S y \<Longrightarrow> x \<le> y"
   10.95 -  unfolding isLub_def by (blast intro!: leastPD3)
   10.96 -
   10.97 -lemma isLub_ubs: "isLub R S x \<Longrightarrow> x <=* ubs R S"
   10.98 -  unfolding ubs_def isLub_def by (rule leastPD2)
   10.99 -
  10.100 -lemma isLub_unique: "[| isLub R S x; isLub R S y |] ==> x = (y::'a::linorder)"
  10.101 -  apply (frule isLub_isUb)
  10.102 -  apply (frule_tac x = y in isLub_isUb)
  10.103 -  apply (blast intro!: order_antisym dest!: isLub_le_isUb)
  10.104 -  done
  10.105 -
  10.106 -end
    11.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Nov 05 09:45:00 2013 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue Nov 05 09:45:02 2013 +0100
    11.3 @@ -4506,38 +4506,30 @@
    11.4      apply (erule_tac x="x - y" in ballE)
    11.5      apply (auto simp add: inner_diff)
    11.6      done
    11.7 -  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
    11.8 +  def k \<equiv> "SUP x:t. a \<bullet> x"
    11.9    show ?thesis
   11.10      apply (rule_tac x="-a" in exI)
   11.11      apply (rule_tac x="-(k + b / 2)" in exI)
   11.12 -    apply rule
   11.13 -    apply rule
   11.14 -    defer
   11.15 -    apply rule
   11.16 +    apply (intro conjI ballI)
   11.17      unfolding inner_minus_left and neg_less_iff_less
   11.18    proof -
   11.19 -    from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
   11.20 -      apply (erule_tac x=y in ballE)
   11.21 -      apply (rule setleI)
   11.22 -      using `y \<in> s`
   11.23 -      apply auto
   11.24 -      done
   11.25 -    then have k: "isLub UNIV ((\<lambda>x. inner a x) ` t) k"
   11.26 +    fix x assume "x \<in> t"
   11.27 +    then have "inner a x - b / 2 < k"
   11.28        unfolding k_def
   11.29 -      apply (rule_tac isLub_cSup)
   11.30 -      using assms(5)
   11.31 -      apply auto
   11.32 -      done
   11.33 -    fix x
   11.34 -    assume "x \<in> t"
   11.35 -    then show "inner a x < (k + b / 2)"
   11.36 -      using `0<b` and isLubD2[OF k, of "inner a x"] by auto
   11.37 +    proof (subst less_cSUP_iff)
   11.38 +      show "t \<noteq> {}" by fact
   11.39 +      show "bdd_above (op \<bullet> a ` t)"
   11.40 +        using ab[rule_format, of y] `y \<in> s`
   11.41 +        by (intro bdd_aboveI2[where M="inner a y - b"]) (auto simp: field_simps intro: less_imp_le)
   11.42 +    qed (auto intro!: bexI[of _ x] `0<b`)
   11.43 +    then show "inner a x < k + b / 2"
   11.44 +      by auto
   11.45    next
   11.46      fix x
   11.47      assume "x \<in> s"
   11.48      then have "k \<le> inner a x - b"
   11.49        unfolding k_def
   11.50 -      apply (rule_tac cSup_least)
   11.51 +      apply (rule_tac cSUP_least)
   11.52        using assms(5)
   11.53        using ab[THEN bspec[where x=x]]
   11.54        apply auto
   11.55 @@ -4626,20 +4618,14 @@
   11.56    from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
   11.57    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"
   11.58      using assms(3-5) by auto
   11.59 -  then have "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
   11.60 +  then have *: "\<And>x y. x \<in> t \<Longrightarrow> y \<in> s \<Longrightarrow> inner a y \<le> inner a x"
   11.61      by (force simp add: inner_diff)
   11.62 -  then show ?thesis
   11.63 -    apply (rule_tac x=a in exI)
   11.64 -    apply (rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI)
   11.65 +  then have bdd: "bdd_above ((op \<bullet> a)`s)"
   11.66 +    using `t \<noteq> {}` by (auto intro: bdd_aboveI2[OF *])
   11.67 +  show ?thesis
   11.68      using `a\<noteq>0`
   11.69 -    apply auto
   11.70 -    apply (rule isLub_cSup[THEN isLubD2])
   11.71 -    prefer 4
   11.72 -    apply (rule cSup_least)
   11.73 -    using assms(3-5)
   11.74 -    apply (auto simp add: setle_def)
   11.75 -    apply metis
   11.76 -    done
   11.77 +    by (intro exI[of _ a] exI[of _ "SUP x:s. a \<bullet> x"])
   11.78 +       (auto intro!: cSUP_upper bdd cSUP_least `a \<noteq> 0` `s \<noteq> {}` *)
   11.79  qed
   11.80  
   11.81  
    12.1 --- a/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 05 09:45:00 2013 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Integration.thy	Tue Nov 05 09:45:02 2013 +0100
    12.3 @@ -28,10 +28,10 @@
    12.4  proof -
    12.5    have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e"
    12.6      by arith
    12.7 -  then show ?thesis
    12.8 -    using S b cSup_bounds[of S "l - e" "l+e"]
    12.9 -    unfolding th
   12.10 -    by (auto simp add: setge_def setle_def)
   12.11 +  have "bdd_above S"
   12.12 +    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
   12.13 +  with S b show ?thesis
   12.14 +    unfolding th by (auto intro!: cSup_upper2 cSup_least)
   12.15  qed
   12.16  
   12.17  lemma cInf_asclose: (* TODO: is this really needed? *)
   12.18 @@ -70,39 +70,6 @@
   12.19    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists>x\<in>S. a \<ge> x)"
   12.20    by (metis cInf_eq_Min Min_le_iff)
   12.21  
   12.22 -lemma Inf: (* rename *)
   12.23 -  fixes S :: "real set"
   12.24 -  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. b <=* S) \<Longrightarrow> isGlb UNIV S (Inf S)"
   12.25 -  by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def
   12.26 -    intro: cInf_lower cInf_greatest)
   12.27 -
   12.28 -lemma real_le_inf_subset:
   12.29 -  assumes "t \<noteq> {}"
   12.30 -    and "t \<subseteq> s"
   12.31 -    and "\<exists>b. b <=* s"
   12.32 -  shows "Inf s \<le> Inf (t::real set)"
   12.33 -  apply (rule isGlb_le_isLb)
   12.34 -  apply (rule Inf[OF assms(1)])
   12.35 -  apply (insert assms)
   12.36 -  apply (erule exE)
   12.37 -  apply (rule_tac x = b in exI)
   12.38 -  apply (auto simp: isLb_def setge_def intro!: cInf_lower cInf_greatest)
   12.39 -  done
   12.40 -
   12.41 -lemma real_ge_sup_subset:
   12.42 -  fixes t :: "real set"
   12.43 -  assumes "t \<noteq> {}"
   12.44 -    and "t \<subseteq> s"
   12.45 -    and "\<exists>b. s *<= b"
   12.46 -  shows "Sup s \<ge> Sup t"
   12.47 -  apply (rule isLub_le_isUb)
   12.48 -  apply (rule isLub_cSup[OF assms(1)])
   12.49 -  apply (insert assms)
   12.50 -  apply (erule exE)
   12.51 -  apply (rule_tac x = b in exI)
   12.52 -  apply (auto simp: isUb_def setle_def intro!: cSup_upper cSup_least)
   12.53 -  done
   12.54 -
   12.55  (*declare not_less[simp] not_le[simp]*)
   12.56  
   12.57  lemmas scaleR_simps = scaleR_zero_left scaleR_minus_left scaleR_left_diff_distrib
   12.58 @@ -486,24 +453,24 @@
   12.59  subsection {* Bounds on intervals where they exist. *}
   12.60  
   12.61  definition interval_upperbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
   12.62 -  where "interval_upperbound s = (\<Sum>i\<in>Basis. Sup {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
   12.63 +  where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
   12.64  
   12.65  definition interval_lowerbound :: "('a::ordered_euclidean_space) set \<Rightarrow> 'a"
   12.66 -  where "interval_lowerbound s = (\<Sum>i\<in>Basis. Inf {a. \<exists>x\<in>s. x\<bullet>i = a} *\<^sub>R i)"
   12.67 +  where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
   12.68  
   12.69  lemma interval_upperbound[simp]:
   12.70    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   12.71      interval_upperbound {a..b} = (b::'a::ordered_euclidean_space)"
   12.72    unfolding interval_upperbound_def euclidean_representation_setsum
   12.73 -  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setle_def
   12.74 -      intro!: cSup_unique)
   12.75 +  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] SUP_def
   12.76 +           intro!: cSup_eq)
   12.77  
   12.78  lemma interval_lowerbound[simp]:
   12.79    "\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
   12.80      interval_lowerbound {a..b} = (a::'a::ordered_euclidean_space)"
   12.81    unfolding interval_lowerbound_def euclidean_representation_setsum
   12.82 -  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] setge_def
   12.83 -      intro!: cInf_unique)
   12.84 +  by (auto simp del: ex_simps simp add: Bex_def ex_simps[symmetric] eucl_le[where 'a='a] INF_def
   12.85 +           intro!: cInf_eq)
   12.86  
   12.87  lemmas interval_bounds = interval_upperbound interval_lowerbound
   12.88  
   12.89 @@ -6627,7 +6594,7 @@
   12.90  lemma interval_bound_sing[simp]:
   12.91    "interval_upperbound {a} = a"
   12.92    "interval_lowerbound {a} = a"
   12.93 -  unfolding interval_upperbound_def interval_lowerbound_def
   12.94 +  unfolding interval_upperbound_def interval_lowerbound_def SUP_def INF_def
   12.95    by (auto simp: euclidean_representation)
   12.96  
   12.97  lemma additive_tagged_division_1:
   12.98 @@ -11236,37 +11203,26 @@
   12.99  lemma bounded_variation_absolutely_integrable_interval:
  12.100    fixes f :: "'n::ordered_euclidean_space \<Rightarrow> 'm::ordered_euclidean_space"
  12.101    assumes "f integrable_on {a..b}"
  12.102 -    and "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
  12.103 +    and *: "\<forall>d. d division_of {a..b} \<longrightarrow> setsum (\<lambda>k. norm(integral k f)) d \<le> B"
  12.104    shows "f absolutely_integrable_on {a..b}"
  12.105  proof -
  12.106 -  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of {a..b} }"
  12.107 -  def i \<equiv> "Sup ?S"
  12.108 -  have i: "isLub UNIV ?S i"
  12.109 -    unfolding i_def
  12.110 -    apply (rule isLub_cSup)
  12.111 -    apply (rule elementary_interval)
  12.112 -    defer
  12.113 -    apply (rule_tac x=B in exI)
  12.114 -    apply (rule setleI)
  12.115 -    using assms(2)
  12.116 -    apply auto
  12.117 -    done
  12.118 +  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of {a..b}}"
  12.119 +  have D_1: "?D \<noteq> {}"
  12.120 +    by (rule elementary_interval[of a b]) auto
  12.121 +  have D_2: "bdd_above (?f`?D)"
  12.122 +    by (metis * mem_Collect_eq bdd_aboveI2)
  12.123 +  note D = D_1 D_2
  12.124 +  let ?S = "SUP x:?D. ?f x"
  12.125    show ?thesis
  12.126      apply rule
  12.127      apply (rule assms)
  12.128      apply rule
  12.129 -    apply (subst has_integral[of _ i])
  12.130 +    apply (subst has_integral[of _ ?S])
  12.131    proof safe
  12.132      case goal1
  12.133 -    then have "i - e / 2 \<notin> Collect (isUb UNIV (setsum (\<lambda>k. norm (integral k f)) `
  12.134 -      {d. d division_of {a..b}}))"
  12.135 -      using isLub_ubs[OF i,rule_format]
  12.136 -      unfolding setge_def ubs_def
  12.137 -      by auto
  12.138 -    then have "\<exists>y. y division_of {a..b} \<and> i - e / 2 < (\<Sum>k\<in>y. norm (integral k f))"
  12.139 -      unfolding mem_Collect_eq isUb_def setle_def
  12.140 -      by (simp add: not_le)
  12.141 -    then guess d .. note d=conjunctD2[OF this]
  12.142 +    then have "?S - e / 2 < ?S" by simp
  12.143 +    then obtain d where d: "d division_of {a..b}" "?S - e / 2 < (\<Sum>k\<in>d. norm (integral k f))"
  12.144 +      unfolding less_cSUP_iff[OF D] by auto
  12.145      note d' = division_ofD[OF this(1)]
  12.146  
  12.147      have "\<forall>x. \<exists>e>0. \<forall>i\<in>d. x \<notin> i \<longrightarrow> ball x e \<inter> i = {}"
  12.148 @@ -11451,21 +11407,17 @@
  12.149          done
  12.150        note snd_p = division_ofD[OF division_of_tagged_division[OF p(1)]]
  12.151  
  12.152 -      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> i - e / 2 < sni \<and> sni' \<le> i \<and>
  12.153 -        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - i) < e"
  12.154 +      have *: "\<And>sni sni' sf sf'. abs (sf' - sni') < e / 2 \<longrightarrow> ?S - e / 2 < sni \<and> sni' \<le> ?S \<and>
  12.155 +        sni \<le> sni' \<and> sf' = sf \<longrightarrow> abs (sf - ?S) < e"
  12.156          by arith
  12.157 -      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - i) < e"
  12.158 +      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R norm (f x)) - ?S) < e"
  12.159          unfolding real_norm_def
  12.160          apply (rule *[rule_format,OF **])
  12.161          apply safe
  12.162          apply(rule d(2))
  12.163        proof -
  12.164 -        case goal1
  12.165 -        show ?case unfolding sum_p'
  12.166 -          apply (rule isLubD2[OF i])
  12.167 -          using division_of_tagged_division[OF p'']
  12.168 -          apply auto
  12.169 -          done
  12.170 +        case goal1 show ?case
  12.171 +          by (auto simp: sum_p' division_of_tagged_division[OF p''] D intro!: cSUP_upper)
  12.172        next
  12.173          case goal2
  12.174          have *: "{k \<inter> l | k l. k \<in> d \<and> l \<in> snd ` p} =
  12.175 @@ -11756,18 +11708,13 @@
  12.176      and "\<forall>d. d division_of (\<Union>d) \<longrightarrow> setsum (\<lambda>k. norm (integral k f)) d \<le> B"
  12.177    shows "f absolutely_integrable_on UNIV"
  12.178  proof (rule absolutely_integrable_onI, fact, rule)
  12.179 -  let ?S = "(\<lambda>d. setsum (\<lambda>k. norm(integral k f)) d) ` {d. d division_of  (\<Union>d)}"
  12.180 -  def i \<equiv> "Sup ?S"
  12.181 -  have i: "isLub UNIV ?S i"
  12.182 -    unfolding i_def
  12.183 -    apply (rule isLub_cSup)
  12.184 -    apply (rule elementary_interval)
  12.185 -    defer
  12.186 -    apply (rule_tac x=B in exI)
  12.187 -    apply (rule setleI)
  12.188 -    using assms(2)
  12.189 -    apply auto
  12.190 -    done
  12.191 +  let ?f = "\<lambda>d. \<Sum>k\<in>d. norm (integral k f)" and ?D = "{d. d division_of  (\<Union>d)}"
  12.192 +  have D_1: "?D \<noteq> {}"
  12.193 +    by (rule elementary_interval) auto
  12.194 +  have D_2: "bdd_above (?f`?D)"
  12.195 +    by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
  12.196 +  note D = D_1 D_2
  12.197 +  let ?S = "SUP d:?D. ?f d"
  12.198    have f_int: "\<And>a b. f absolutely_integrable_on {a..b}"
  12.199      apply (rule bounded_variation_absolutely_integrable_interval[where B=B])
  12.200      apply (rule integrable_on_subinterval[OF assms(1)])
  12.201 @@ -11776,7 +11723,7 @@
  12.202      apply (rule assms(2)[rule_format])
  12.203      apply auto
  12.204      done
  12.205 -  show "((\<lambda>x. norm (f x)) has_integral i) UNIV"
  12.206 +  show "((\<lambda>x. norm (f x)) has_integral ?S) UNIV"
  12.207      apply (subst has_integral_alt')
  12.208      apply safe
  12.209    proof -
  12.210 @@ -11785,16 +11732,11 @@
  12.211        using f_int[of a b] by auto
  12.212    next
  12.213      case goal2
  12.214 -    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> i - e"
  12.215 +    have "\<exists>y\<in>setsum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union>d}. \<not> y \<le> ?S - e"
  12.216      proof (rule ccontr)
  12.217        assume "\<not> ?thesis"
  12.218 -      then have "i \<le> i - e"
  12.219 -        apply -
  12.220 -        apply (rule isLub_le_isUb[OF i])
  12.221 -        apply (rule isUbI)
  12.222 -        unfolding setle_def
  12.223 -        apply auto
  12.224 -        done
  12.225 +      then have "?S \<le> ?S - e"
  12.226 +        by (intro cSUP_least[OF D(1)]) auto
  12.227        then show False
  12.228          using goal2 by auto
  12.229      qed
  12.230 @@ -11811,9 +11753,9 @@
  12.231      proof -
  12.232        fix a b :: 'n
  12.233        assume ab: "ball 0 (K + 1) \<subseteq> {a..b}"
  12.234 -      have *: "\<forall>s s1. i - e < s1 \<and> s1 \<le> s \<and> s < i + e \<longrightarrow> abs (s - i) < e"
  12.235 +      have *: "\<forall>s s1. ?S - e < s1 \<and> s1 \<le> s \<and> s < ?S + e \<longrightarrow> abs (s - ?S) < e"
  12.236          by arith
  12.237 -      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - i) < e"
  12.238 +      show "norm (integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) - ?S) < e"
  12.239          unfolding real_norm_def
  12.240          apply (rule *[rule_format])
  12.241          apply safe
  12.242 @@ -11865,10 +11807,10 @@
  12.243          from henstock_lemma[OF f(1) `e/2>0`] guess d2 . note d2=this
  12.244          from fine_division_exists[OF gauge_inter[OF d1(1) d2(1)], of a b] guess p .
  12.245          note p=this(1) conjunctD2[OF this(2)[unfolded fine_inter]]
  12.246 -        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> i \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
  12.247 -          abs (sf' - di) < e / 2 \<longrightarrow> di < i + e"
  12.248 +        have *: "\<And>sf sf' si di. sf' = sf \<longrightarrow> si \<le> ?S \<longrightarrow> abs (sf - si) < e / 2 \<longrightarrow>
  12.249 +          abs (sf' - di) < e / 2 \<longrightarrow> di < ?S + e"
  12.250            by arith
  12.251 -        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < i + e"
  12.252 +        show "integral {a..b} (\<lambda>x. if x \<in> UNIV then norm (f x) else 0) < ?S + e"
  12.253            apply (subst if_P)
  12.254            apply rule
  12.255          proof (rule *[rule_format])
  12.256 @@ -11891,18 +11833,12 @@
  12.257              apply (subst abs_of_nonneg)
  12.258              apply auto
  12.259              done
  12.260 -          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> i"
  12.261 +          show "(\<Sum>(x, k)\<in>p. norm (integral k f)) \<le> ?S"
  12.262 +            using partial_division_of_tagged_division[of p "{a..b}"] p(1)
  12.263              apply (subst setsum_over_tagged_division_lemma[OF p(1)])
  12.264 -            defer
  12.265 -            apply (rule isLubD2[OF i])
  12.266 -            unfolding image_iff
  12.267 -            apply (rule_tac x="snd ` p" in bexI)
  12.268 -            unfolding mem_Collect_eq
  12.269 -            defer
  12.270 -            apply (rule partial_division_of_tagged_division[of _ "{a..b}"])
  12.271 -            using p(1)
  12.272 -            unfolding tagged_division_of_def
  12.273 -            apply auto
  12.274 +            apply (simp add: integral_null)
  12.275 +            apply (intro cSUP_upper2[OF D(2), of "snd ` p"])
  12.276 +            apply (auto simp: tagged_partial_division_of_def)
  12.277              done
  12.278          qed
  12.279        qed
  12.280 @@ -12378,11 +12314,22 @@
  12.281  lemma dominated_convergence:
  12.282    fixes f :: "nat \<Rightarrow> 'n::ordered_euclidean_space \<Rightarrow> real"
  12.283    assumes "\<And>k. (f k) integrable_on s" "h integrable_on s"
  12.284 -    and "\<And>k. \<forall>x \<in> s. norm(f k x) \<le> (h x)"
  12.285 +    and "\<And>k. \<forall>x \<in> s. norm (f k x) \<le> h x"
  12.286      and "\<forall>x \<in> s. ((\<lambda>k. f k x) ---> g x) sequentially"
  12.287    shows "g integrable_on s"
  12.288      and "((\<lambda>k. integral s (f k)) ---> integral s g) sequentially"
  12.289  proof -
  12.290 +  have bdd_below[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_below {f n x |n. P n}"
  12.291 +  proof (safe intro!: bdd_belowI)
  12.292 +    fix n x show "x \<in> s \<Longrightarrow> - h x \<le> f n x"
  12.293 +      using assms(3)[rule_format, of x n] by simp
  12.294 +  qed
  12.295 +  have bdd_above[simp]: "\<And>x P. x \<in> s \<Longrightarrow> bdd_above {f n x |n. P n}"
  12.296 +  proof (safe intro!: bdd_aboveI)
  12.297 +    fix n x show "x \<in> s \<Longrightarrow> f n x \<le> h x"
  12.298 +      using assms(3)[rule_format, of x n] by simp
  12.299 +  qed
  12.300 +
  12.301    have "\<And>m. (\<lambda>x. Inf {f j x |j. m \<le> j}) integrable_on s \<and>
  12.302      ((\<lambda>k. integral s (\<lambda>x. Inf {f j x |j. j \<in> {m..m + k}})) --->
  12.303      integral s (\<lambda>x. Inf {f j x |j. m \<le> j}))sequentially"
  12.304 @@ -12422,66 +12369,32 @@
  12.305      fix x
  12.306      assume x: "x \<in> s"
  12.307      show "Inf {f j x |j. j \<in> {m..m + Suc k}} \<le> Inf {f j x |j. j \<in> {m..m + k}}"
  12.308 -      apply (rule cInf_ge)
  12.309 -      unfolding setge_def
  12.310 -      defer
  12.311 -      apply rule
  12.312 -      apply (subst cInf_finite_le_iff)
  12.313 -      prefer 3
  12.314 -      apply (rule_tac x=xa in bexI)
  12.315 -      apply auto
  12.316 -      done
  12.317 -    let ?S = "{f j x| j.  m \<le> j}"
  12.318 -    def i \<equiv> "Inf ?S"
  12.319 -    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
  12.320 +      by (rule cInf_superset_mono) auto
  12.321 +    let ?S = "{f j x| j. m \<le> j}"
  12.322 +    show "((\<lambda>k. Inf {f j x |j. j \<in> {m..m + k}}) ---> Inf ?S) sequentially"
  12.323      proof (rule LIMSEQ_I)
  12.324        case goal1
  12.325        note r = this
  12.326 -      have i: "isGlb UNIV ?S i"
  12.327 -        unfolding i_def
  12.328 -        apply (rule Inf)
  12.329 -        defer
  12.330 -        apply (rule_tac x="- h x - 1" in exI)
  12.331 -        unfolding setge_def
  12.332 -      proof safe
  12.333 -        case goal1
  12.334 -        then show ?case using assms(3)[rule_format,OF x, of j] by auto
  12.335 -      qed auto
  12.336 -
  12.337 -      have "\<exists>y\<in>?S. \<not> y \<ge> i + r"
  12.338 -      proof(rule ccontr)
  12.339 -        assume "\<not> ?thesis"
  12.340 -        then have "i \<ge> i + r"
  12.341 -          apply -
  12.342 -          apply (rule isGlb_le_isLb[OF i])
  12.343 -          apply (rule isLbI)
  12.344 -          unfolding setge_def
  12.345 -          apply fastforce+
  12.346 -          done
  12.347 -        then show False using r by auto
  12.348 -      qed
  12.349 -      then guess y .. note y=this[unfolded not_le]
  12.350 -      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
  12.351 +
  12.352 +      have "\<exists>y\<in>?S. y < Inf ?S + r"
  12.353 +        by (subst cInf_less_iff[symmetric]) (auto simp: `x\<in>s` r)
  12.354 +      then obtain N where N: "f N x < Inf ?S + r" "m \<le> N"
  12.355 +        by blast
  12.356  
  12.357        show ?case
  12.358          apply (rule_tac x=N in exI)
  12.359        proof safe
  12.360          case goal1
  12.361 -        have *: "\<And>y ix. y < i + r \<longrightarrow> i \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - i) < r"
  12.362 +        have *: "\<And>y ix. y < Inf ?S + r \<longrightarrow> Inf ?S \<le> ix \<longrightarrow> ix \<le> y \<longrightarrow> abs(ix - Inf ?S) < r"
  12.363            by arith
  12.364          show ?case
  12.365            unfolding real_norm_def
  12.366 -            apply (rule *[rule_format,OF y(2)])
  12.367 -            unfolding i_def
  12.368 -            apply (rule real_le_inf_subset)
  12.369 -            prefer 3
  12.370 -            apply (rule,rule isGlbD1[OF i])
  12.371 -            prefer 3
  12.372 -            apply (subst cInf_finite_le_iff)
  12.373 -            prefer 3
  12.374 -            apply (rule_tac x=y in bexI)
  12.375 +            apply (rule *[rule_format, OF N(1)])
  12.376 +            apply (rule cInf_superset_mono, auto simp: `x\<in>s`) []
  12.377 +            apply (rule cInf_lower)
  12.378              using N goal1
  12.379 -            apply auto
  12.380 +            apply auto []
  12.381 +            apply simp
  12.382              done
  12.383        qed
  12.384      qed
  12.385 @@ -12525,65 +12438,27 @@
  12.386      fix x
  12.387      assume x: "x\<in>s"
  12.388      show "Sup {f j x |j. j \<in> {m..m + Suc k}} \<ge> Sup {f j x |j. j \<in> {m..m + k}}"
  12.389 -      apply (rule cSup_le)
  12.390 -      unfolding setle_def
  12.391 -      defer
  12.392 -      apply rule
  12.393 -      apply (subst cSup_finite_ge_iff)
  12.394 -      prefer 3
  12.395 -      apply (rule_tac x=y in bexI)
  12.396 -      apply auto
  12.397 -      done
  12.398 -    let ?S = "{f j x| j.  m \<le> j}"
  12.399 -    def i \<equiv> "Sup ?S"
  12.400 -    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> i) sequentially"
  12.401 +      by (rule cSup_subset_mono) auto
  12.402 +    let ?S = "{f j x| j. m \<le> j}"
  12.403 +    show "((\<lambda>k. Sup {f j x |j. j \<in> {m..m + k}}) ---> Sup ?S) sequentially"
  12.404      proof (rule LIMSEQ_I)
  12.405        case goal1 note r=this
  12.406 -      have i: "isLub UNIV ?S i"
  12.407 -        unfolding i_def
  12.408 -        apply (rule isLub_cSup)
  12.409 -        defer
  12.410 -        apply (rule_tac x="h x" in exI)
  12.411 -        unfolding setle_def
  12.412 -      proof safe
  12.413 -        case goal1
  12.414 -        then show ?case
  12.415 -          using assms(3)[rule_format,OF x, of j] by auto
  12.416 -      qed auto
  12.417 -
  12.418 -      have "\<exists>y\<in>?S. \<not> y \<le> i - r"
  12.419 -      proof (rule ccontr)
  12.420 -        assume "\<not> ?thesis"
  12.421 -        then have "i \<le> i - r"
  12.422 -          apply -
  12.423 -          apply (rule isLub_le_isUb[OF i])
  12.424 -          apply (rule isUbI)
  12.425 -          unfolding setle_def
  12.426 -          apply fastforce+
  12.427 -          done
  12.428 -        then show False
  12.429 -          using r by auto
  12.430 -      qed
  12.431 -      then guess y .. note y=this[unfolded not_le]
  12.432 -      from this(1)[unfolded mem_Collect_eq] guess N .. note N=conjunctD2[OF this]
  12.433 +      have "\<exists>y\<in>?S. Sup ?S - r < y"
  12.434 +        by (subst less_cSup_iff[symmetric]) (auto simp: r `x\<in>s`)
  12.435 +      then obtain N where N: "Sup ?S - r < f N x" "m \<le> N"
  12.436 +        by blast
  12.437  
  12.438        show ?case
  12.439          apply (rule_tac x=N in exI)
  12.440        proof safe
  12.441          case goal1
  12.442 -        have *: "\<And>y ix. i - r < y \<longrightarrow> ix \<le> i \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - i) < r"
  12.443 +        have *: "\<And>y ix. Sup ?S - r < y \<longrightarrow> ix \<le> Sup ?S \<longrightarrow> y \<le> ix \<longrightarrow> abs(ix - Sup ?S) < r"
  12.444            by arith
  12.445          show ?case
  12.446 -          unfolding real_norm_def
  12.447 -          apply (rule *[rule_format,OF y(2)])
  12.448 -          unfolding i_def
  12.449 -          apply (rule real_ge_sup_subset)
  12.450 -          prefer 3
  12.451 -          apply (rule, rule isLubD1[OF i])
  12.452 -          prefer 3
  12.453 -          apply (subst cSup_finite_ge_iff)
  12.454 -          prefer 3
  12.455 -          apply (rule_tac x = y in bexI)
  12.456 +          apply simp
  12.457 +          apply (rule *[rule_format, OF N(1)])
  12.458 +          apply (rule cSup_subset_mono, auto simp: `x\<in>s`) []
  12.459 +          apply (subst cSup_upper)
  12.460            using N goal1
  12.461            apply auto
  12.462            done
  12.463 @@ -12616,17 +12491,7 @@
  12.464  
  12.465      have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
  12.466      show "Inf {f j x |j. k \<le> j} \<le> Inf {f j x |j. Suc k \<le> j}"
  12.467 -      apply -
  12.468 -      apply (rule real_le_inf_subset)
  12.469 -      prefer 3
  12.470 -      unfolding setge_def
  12.471 -      apply (rule_tac x="- h x" in exI)
  12.472 -      apply safe
  12.473 -      apply (rule *)
  12.474 -      using assms(3)[rule_format,OF x]
  12.475 -      unfolding real_norm_def abs_le_iff
  12.476 -      apply auto
  12.477 -      done
  12.478 +      by (intro cInf_superset_mono) (auto simp: `x\<in>s`)
  12.479  
  12.480      show "(\<lambda>k::nat. Inf {f j x |j. k \<le> j}) ----> g x"
  12.481      proof (rule LIMSEQ_I)
  12.482 @@ -12674,16 +12539,7 @@
  12.483      assume x: "x \<in> s"
  12.484  
  12.485      show "Sup {f j x |j. k \<le> j} \<ge> Sup {f j x |j. Suc k \<le> j}"
  12.486 -      apply -
  12.487 -      apply (rule real_ge_sup_subset)
  12.488 -      prefer 3
  12.489 -      unfolding setle_def
  12.490 -      apply (rule_tac x="h x" in exI)
  12.491 -      apply safe
  12.492 -      using assms(3)[rule_format,OF x]
  12.493 -      unfolding real_norm_def abs_le_iff
  12.494 -      apply auto
  12.495 -      done
  12.496 +      by (rule cSup_subset_mono) (auto simp: `x\<in>s`)
  12.497      show "((\<lambda>k. Sup {f j x |j. k \<le> j}) ---> g x) sequentially"
  12.498      proof (rule LIMSEQ_I)
  12.499        case goal1
  12.500 @@ -12712,41 +12568,18 @@
  12.501      from LIMSEQ_D [OF inc2(2) goal1] guess N1 .. note N1=this[unfolded real_norm_def]
  12.502      from LIMSEQ_D [OF dec2(2) goal1] guess N2 .. note N2=this[unfolded real_norm_def]
  12.503      show ?case
  12.504 -      apply (rule_tac x="N1+N2" in exI, safe)
  12.505 -    proof -
  12.506 +    proof (rule_tac x="N1+N2" in exI, safe)
  12.507        fix n
  12.508        assume n: "n \<ge> N1 + N2"
  12.509        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"
  12.510          by arith
  12.511        show "norm (integral s (f n) - integral s g) < r"
  12.512          unfolding real_norm_def
  12.513 -        apply (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
  12.514 -      proof -
  12.515 +      proof (rule *[rule_format,OF N1[rule_format] N2[rule_format], of n n])
  12.516          show "integral s (\<lambda>x. Inf {f j x |j. n \<le> j}) \<le> integral s (f n)"
  12.517 -        proof (rule integral_le[OF dec1(1) assms(1)], safe)
  12.518 -          fix x
  12.519 -          assume x: "x \<in> s"
  12.520 -          have *: "\<And>x y::real. x \<ge> - y \<Longrightarrow> - x \<le> y" by auto
  12.521 -          show "Inf {f j x |j. n \<le> j} \<le> f n x"
  12.522 -            apply (intro cInf_lower bdd_belowI)
  12.523 -            apply auto []
  12.524 -            apply (rule *)
  12.525 -            using assms(3)[rule_format,OF x]
  12.526 -            unfolding real_norm_def abs_le_iff
  12.527 -            apply auto
  12.528 -            done
  12.529 -        qed
  12.530 +          by (rule integral_le[OF dec1(1) assms(1)]) (auto intro!: cInf_lower)
  12.531          show "integral s (f n) \<le> integral s (\<lambda>x. Sup {f j x |j. n \<le> j})"
  12.532 -        proof (rule integral_le[OF assms(1) inc1(1)], safe)
  12.533 -          fix x
  12.534 -          assume x: "x \<in> s"
  12.535 -          show "f n x \<le> Sup {f j x |j. n \<le> j}"
  12.536 -            apply (rule cSup_upper)
  12.537 -            using assms(3)[rule_format,OF x]
  12.538 -            unfolding real_norm_def abs_le_iff
  12.539 -            apply auto
  12.540 -            done
  12.541 -        qed
  12.542 +          by (rule integral_le[OF assms(1) inc1(1)]) (auto intro!: cSup_upper)
  12.543        qed (insert n, auto)
  12.544      qed
  12.545    qed
    13.1 --- a/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Nov 05 09:45:00 2013 +0100
    13.2 +++ b/src/HOL/Multivariate_Analysis/Operator_Norm.thy	Tue Nov 05 09:45:02 2013 +0100
    13.3 @@ -8,7 +8,7 @@
    13.4  imports Linear_Algebra
    13.5  begin
    13.6  
    13.7 -definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
    13.8 +definition "onorm f = (SUP x:{x. norm x = 1}. norm (f x))"
    13.9  
   13.10  lemma norm_bound_generalize:
   13.11    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   13.12 @@ -67,25 +67,22 @@
   13.13    shows "norm (f x) \<le> onorm f * norm x"
   13.14      and "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
   13.15  proof -
   13.16 -  let ?S = "{norm (f x) |x. norm x = 1}"
   13.17 +  let ?S = "(\<lambda>x. norm (f x))`{x. norm x = 1}"
   13.18    have "norm (f (SOME i. i \<in> Basis)) \<in> ?S"
   13.19      by (auto intro!: exI[of _ "SOME i. i \<in> Basis"] norm_Basis SOME_Basis)
   13.20    then have Se: "?S \<noteq> {}"
   13.21      by auto
   13.22 -  from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
   13.23 -    unfolding norm_bound_generalize[OF lf, symmetric]
   13.24 -    by (auto simp add: setle_def)
   13.25 -  from isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
   13.26 -  show "norm (f x) \<le> onorm f * norm x"
   13.27 +  from linear_bounded[OF lf] have b: "bdd_above ?S"
   13.28 +    unfolding norm_bound_generalize[OF lf, symmetric] by auto
   13.29 +  then show "norm (f x) \<le> onorm f * norm x"
   13.30      apply -
   13.31      apply (rule spec[where x = x])
   13.32      unfolding norm_bound_generalize[OF lf, symmetric]
   13.33 -    apply (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
   13.34 +    apply (auto simp: onorm_def intro!: cSUP_upper)
   13.35      done
   13.36    show "\<forall>x. norm (f x) \<le> b * norm x \<Longrightarrow> onorm f \<le> b"
   13.37 -    using isLub_cSup[OF Se b, unfolded onorm_def[symmetric]]
   13.38      unfolding norm_bound_generalize[OF lf, symmetric]
   13.39 -    by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)
   13.40 +    using Se by (auto simp: onorm_def intro!: cSUP_least b)
   13.41  qed
   13.42  
   13.43  lemma onorm_pos_le:
   13.44 @@ -107,18 +104,8 @@
   13.45    apply arith
   13.46    done
   13.47  
   13.48 -lemma onorm_const:
   13.49 -  "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
   13.50 -proof -
   13.51 -  let ?f = "\<lambda>x::'a. y::'b"
   13.52 -  have th: "{norm (?f x)| x. norm x = 1} = {norm y}"
   13.53 -    by (auto simp: SOME_Basis intro!: exI[of _ "SOME i. i \<in> Basis"])
   13.54 -  show ?thesis
   13.55 -    unfolding onorm_def th
   13.56 -    apply (rule cSup_unique)
   13.57 -    apply (simp_all  add: setle_def)
   13.58 -    done
   13.59 -qed
   13.60 +lemma onorm_const: "onorm (\<lambda>x::'a::euclidean_space. y::'b::euclidean_space) = norm y"
   13.61 +  using SOME_Basis by (auto simp add: onorm_def intro!: cSUP_const norm_Basis)
   13.62  
   13.63  lemma onorm_pos_lt:
   13.64    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:45:00 2013 +0100
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 05 09:45:02 2013 +0100
    14.3 @@ -10,7 +10,6 @@
    14.4  imports
    14.5    Complex_Main
    14.6    "~~/src/HOL/Library/Countable_Set"
    14.7 -  "~~/src/HOL/Library/Glbs"
    14.8    "~~/src/HOL/Library/FuncSet"
    14.9    Linear_Algebra
   14.10    Norm_Arith
   14.11 @@ -28,8 +27,6 @@
   14.12  lemma lim_subseq: "subseq r \<Longrightarrow> s ----> l \<Longrightarrow> (s \<circ> r) ----> l"
   14.13    by (rule LIMSEQ_subseq_LIMSEQ)
   14.14  
   14.15 -lemmas real_isGlb_unique = isGlb_unique[where 'a=real]
   14.16 -
   14.17  lemma countable_PiE:
   14.18    "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
   14.19    by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
   14.20 @@ -1555,7 +1552,7 @@
   14.21        fix y
   14.22        assume "y \<in> {x<..} \<inter> I"
   14.23        with False bnd have "Inf (f ` ({x<..} \<inter> I)) \<le> f y"
   14.24 -        by (auto intro: cInf_lower)
   14.25 +        by (auto intro!: cInf_lower bdd_belowI2)
   14.26        with a have "a < f y"
   14.27          by (blast intro: less_le_trans)
   14.28      }
    15.1 --- a/src/HOL/NSA/NSA.thy	Tue Nov 05 09:45:00 2013 +0100
    15.2 +++ b/src/HOL/NSA/NSA.thy	Tue Nov 05 09:45:02 2013 +0100
    15.3 @@ -6,7 +6,7 @@
    15.4  header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
    15.5  
    15.6  theory NSA
    15.7 -imports HyperDef
    15.8 +imports HyperDef "~~/src/HOL/Library/Lubs_Glbs"
    15.9  begin
   15.10  
   15.11  definition
    16.1 --- a/src/HOL/Real.thy	Tue Nov 05 09:45:00 2013 +0100
    16.2 +++ b/src/HOL/Real.thy	Tue Nov 05 09:45:02 2013 +0100
    16.3 @@ -970,13 +970,6 @@
    16.4  qed
    16.5  end
    16.6  
    16.7 -text {*
    16.8 -  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"}:
    16.9 -*}
   16.10 -
   16.11 -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"
   16.12 -  by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro!: cSup_upper)
   16.13 -
   16.14  
   16.15  subsection {* Hiding implementation details *}
   16.16  
    17.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Nov 05 09:45:00 2013 +0100
    17.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Tue Nov 05 09:45:02 2013 +0100
    17.3 @@ -1425,9 +1425,6 @@
    17.4    @{term "{r::real. \<exists>N. \<forall>n\<ge>N. r < X n}"}
    17.5  *}
    17.6  
    17.7 -lemma isUb_UNIV_I: "(\<And>y. y \<in> S \<Longrightarrow> y \<le> u) \<Longrightarrow> isUb UNIV S u"
    17.8 -by (simp add: isUbI setleI)
    17.9 -
   17.10  lemma increasing_LIMSEQ:
   17.11    fixes f :: "nat \<Rightarrow> real"
   17.12    assumes inc: "\<And>n. f n \<le> f (Suc n)"
   17.13 @@ -1454,40 +1451,33 @@
   17.14    then have mem_S: "\<And>N x. \<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S" by auto
   17.15  
   17.16    { fix N x assume N: "\<forall>n\<ge>N. X n < x"
   17.17 -  have "isUb UNIV S x"
   17.18 -  proof (rule isUb_UNIV_I)
   17.19    fix y::real assume "y \<in> S"
   17.20    hence "\<exists>M. \<forall>n\<ge>M. y < X n"
   17.21      by (simp add: S_def)
   17.22    then obtain M where "\<forall>n\<ge>M. y < X n" ..
   17.23    hence "y < X (max M N)" by simp
   17.24    also have "\<dots> < x" using N by simp
   17.25 -  finally show "y \<le> x"
   17.26 -    by (rule order_less_imp_le)
   17.27 -  qed }
   17.28 +  finally have "y \<le> x"
   17.29 +    by (rule order_less_imp_le) }
   17.30    note bound_isUb = this 
   17.31  
   17.32 -  have "\<exists>u. isLub UNIV S u"
   17.33 -  proof (rule reals_complete)
   17.34    obtain N where "\<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < 1"
   17.35      using X[THEN metric_CauchyD, OF zero_less_one] by auto
   17.36    hence N: "\<forall>n\<ge>N. dist (X n) (X N) < 1" by simp
   17.37 -  show "\<exists>x. x \<in> S"
   17.38 -  proof
   17.39 +  have [simp]: "S \<noteq> {}"
   17.40 +  proof (intro exI ex_in_conv[THEN iffD1])
   17.41      from N have "\<forall>n\<ge>N. X N - 1 < X n"
   17.42        by (simp add: abs_diff_less_iff dist_real_def)
   17.43      thus "X N - 1 \<in> S" by (rule mem_S)
   17.44    qed
   17.45 -  show "\<exists>u. isUb UNIV S u"
   17.46 +  have [simp]: "bdd_above S"
   17.47    proof
   17.48      from N have "\<forall>n\<ge>N. X n < X N + 1"
   17.49        by (simp add: abs_diff_less_iff dist_real_def)
   17.50 -    thus "isUb UNIV S (X N + 1)"
   17.51 +    thus "\<And>s. s \<in> S \<Longrightarrow>  s \<le> X N + 1"
   17.52        by (rule bound_isUb)
   17.53    qed
   17.54 -  qed
   17.55 -  then obtain x where x: "isLub UNIV S x" ..
   17.56 -  have "X ----> x"
   17.57 +  have "X ----> Sup S"
   17.58    proof (rule metric_LIMSEQ_I)
   17.59    fix r::real assume "0 < r"
   17.60    hence r: "0 < r/2" by simp
   17.61 @@ -1499,17 +1489,18 @@
   17.62  
   17.63    from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
   17.64    hence "X N - r/2 \<in> S" by (rule mem_S)
   17.65 -  hence 1: "X N - r/2 \<le> x" using x isLub_isUb isUbD by fast
   17.66 +  hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
   17.67  
   17.68    from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
   17.69 -  hence "isUb UNIV S (X N + r/2)" by (rule bound_isUb)
   17.70 -  hence 2: "x \<le> X N + r/2" using x isLub_le_isUb by fast
   17.71 +  from bound_isUb[OF this]
   17.72 +  have 2: "Sup S \<le> X N + r/2"
   17.73 +    by (intro cSup_least) simp_all
   17.74  
   17.75 -  show "\<exists>N. \<forall>n\<ge>N. dist (X n) x < r"
   17.76 +  show "\<exists>N. \<forall>n\<ge>N. dist (X n) (Sup S) < r"
   17.77    proof (intro exI allI impI)
   17.78      fix n assume n: "N \<le> n"
   17.79      from N n have "X n < X N + r/2" and "X N - r/2 < X n" by simp+
   17.80 -    thus "dist (X n) x < r" using 1 2
   17.81 +    thus "dist (X n) (Sup S) < r" using 1 2
   17.82        by (simp add: abs_diff_less_iff dist_real_def)
   17.83    qed
   17.84    qed
    18.1 --- a/src/HOL/ex/Dedekind_Real.thy	Tue Nov 05 09:45:00 2013 +0100
    18.2 +++ b/src/HOL/ex/Dedekind_Real.thy	Tue Nov 05 09:45:02 2013 +0100
    18.3 @@ -1506,7 +1506,6 @@
    18.4  instance real :: linorder
    18.5    by (intro_classes, rule real_le_linear)
    18.6  
    18.7 -
    18.8  lemma real_le_eq_diff: "(x \<le> y) = (x-y \<le> (0::real))"
    18.9  apply (cases x, cases y) 
   18.10  apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus
   18.11 @@ -1657,7 +1656,6 @@
   18.12  lemma real_less_all_real2: "~ 0 < y ==> \<forall>x. y < real_of_preal x"
   18.13  by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1])
   18.14  
   18.15 -
   18.16  subsection {* Completeness of Positive Reals *}
   18.17  
   18.18  text {*
   18.19 @@ -1759,107 +1757,23 @@
   18.20  qed
   18.21  
   18.22  text {*
   18.23 -  \medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc.
   18.24 -*}
   18.25 -
   18.26 -lemma posreals_complete:
   18.27 -  assumes positive_S: "\<forall>x \<in> S. 0 < x"
   18.28 -    and not_empty_S: "\<exists>x. x \<in> S"
   18.29 -    and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u"
   18.30 -  shows "\<exists>t. isLub (UNIV::real set) S t"
   18.31 -proof
   18.32 -  let ?pS = "{w. real_of_preal w \<in> S}"
   18.33 -
   18.34 -  obtain u where "isUb UNIV S u" using upper_bound_Ex ..
   18.35 -  hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def)
   18.36 -
   18.37 -  obtain x where x_in_S: "x \<in> S" using not_empty_S ..
   18.38 -  hence x_gt_zero: "0 < x" using positive_S by simp
   18.39 -  have  "x \<le> u" using sup and x_in_S ..
   18.40 -  hence "0 < u" using x_gt_zero by arith
   18.41 -
   18.42 -  then obtain pu where u_is_pu: "u = real_of_preal pu"
   18.43 -    by (auto simp add: real_gt_zero_preal_Ex)
   18.44 -
   18.45 -  have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu"
   18.46 -  proof
   18.47 -    fix pa
   18.48 -    assume "pa \<in> ?pS"
   18.49 -    then obtain a where a: "a \<in> S" "a = real_of_preal pa"
   18.50 -      by simp
   18.51 -    then have "a \<le> u" using sup by simp
   18.52 -    with a show "pa \<le> pu"
   18.53 -      using sup and u_is_pu by (simp add: real_of_preal_le_iff)
   18.54 -  qed
   18.55 -
   18.56 -  have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)"
   18.57 -  proof
   18.58 -    fix y
   18.59 -    assume y_in_S: "y \<in> S"
   18.60 -    hence "0 < y" using positive_S by simp
   18.61 -    then obtain py where y_is_py: "y = real_of_preal py"
   18.62 -      by (auto simp add: real_gt_zero_preal_Ex)
   18.63 -    hence py_in_pS: "py \<in> ?pS" using y_in_S by simp
   18.64 -    with pS_less_pu have "py \<le> psup ?pS"
   18.65 -      by (rule preal_psup_le)
   18.66 -    thus "y \<le> real_of_preal (psup ?pS)"
   18.67 -      using y_is_py by (simp add: real_of_preal_le_iff)
   18.68 -  qed
   18.69 -
   18.70 -  moreover {
   18.71 -    fix x
   18.72 -    assume x_ub_S: "\<forall>y\<in>S. y \<le> x"
   18.73 -    have "real_of_preal (psup ?pS) \<le> x"
   18.74 -    proof -
   18.75 -      obtain "s" where s_in_S: "s \<in> S" using not_empty_S ..
   18.76 -      hence s_pos: "0 < s" using positive_S by simp
   18.77 -
   18.78 -      hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex)
   18.79 -      then obtain "ps" where s_is_ps: "s = real_of_preal ps" ..
   18.80 -      hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp
   18.81 -
   18.82 -      from x_ub_S have "s \<le> x" using s_in_S ..
   18.83 -      hence "0 < x" using s_pos by simp
   18.84 -      hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex)
   18.85 -      then obtain "px" where x_is_px: "x = real_of_preal px" ..
   18.86 -
   18.87 -      have "\<forall>pe \<in> ?pS. pe \<le> px"
   18.88 -      proof
   18.89 -        fix pe
   18.90 -        assume "pe \<in> ?pS"
   18.91 -        hence "real_of_preal pe \<in> S" by simp
   18.92 -        hence "real_of_preal pe \<le> x" using x_ub_S by simp
   18.93 -        thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff)
   18.94 -      qed
   18.95 -
   18.96 -      moreover have "?pS \<noteq> {}" using ps_in_pS by auto
   18.97 -      ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub)
   18.98 -      thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff)
   18.99 -    qed
  18.100 -  }
  18.101 -  ultimately show "isLub UNIV S (real_of_preal (psup ?pS))"
  18.102 -    by (simp add: isLub_def leastP_def isUb_def setle_def setge_def)
  18.103 -qed
  18.104 -
  18.105 -text {*
  18.106 -  \medskip reals Completeness (again!)
  18.107 +  \medskip Completeness
  18.108  *}
  18.109  
  18.110  lemma reals_complete:
  18.111 +  fixes S :: "real set"
  18.112    assumes notempty_S: "\<exists>X. X \<in> S"
  18.113 -    and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y"
  18.114 -  shows "\<exists>t. isLub (UNIV :: real set) S t"
  18.115 +    and exists_Ub: "bdd_above S"
  18.116 +  shows "\<exists>x. (\<forall>s\<in>S. s \<le> x) \<and> (\<forall>y. (\<forall>s\<in>S. s \<le> y) \<longrightarrow> x \<le> y)"
  18.117  proof -
  18.118    obtain X where X_in_S: "X \<in> S" using notempty_S ..
  18.119 -  obtain Y where Y_isUb: "isUb (UNIV::real set) S Y"
  18.120 -    using exists_Ub ..
  18.121 +  obtain Y where Y_isUb: "\<forall>s\<in>S. s \<le> Y"
  18.122 +    using exists_Ub by (auto simp: bdd_above_def)
  18.123    let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (-X) + 1} \<inter> {x. 0 < x}"
  18.124  
  18.125    {
  18.126      fix x
  18.127 -    assume "isUb (UNIV::real set) S x"
  18.128 -    hence S_le_x: "\<forall> y \<in> S. y <= x"
  18.129 -      by (simp add: isUb_def setle_def)
  18.130 +    assume S_le_x: "\<forall>s\<in>S. s \<le> x"
  18.131      {
  18.132        fix s
  18.133        assume "s \<in> {z. \<exists>x\<in>S. z = x + - X + 1}"
  18.134 @@ -1868,86 +1782,74 @@
  18.135        then have "x1 \<le> x" using S_le_x by simp
  18.136        with x1 have "s \<le> x + - X + 1" by arith
  18.137      }
  18.138 -    then have "isUb (UNIV::real set) ?SHIFT (x + (-X) + 1)"
  18.139 -      by (auto simp add: isUb_def setle_def)
  18.140 +    then have "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
  18.141 +      by auto
  18.142    } note S_Ub_is_SHIFT_Ub = this
  18.143  
  18.144 -  hence "isUb UNIV ?SHIFT (Y + (-X) + 1)" using Y_isUb by simp
  18.145 -  hence "\<exists>Z. isUb UNIV ?SHIFT Z" ..
  18.146 +  have *: "\<forall>s\<in>?SHIFT. s \<le> Y + (-X) + 1" using Y_isUb by (rule S_Ub_is_SHIFT_Ub)
  18.147 +  have "\<forall>s\<in>?SHIFT. s < Y + (-X) + 2"
  18.148 +  proof
  18.149 +    fix s assume "s\<in>?SHIFT"
  18.150 +    with * have "s \<le> Y + (-X) + 1" by simp
  18.151 +    also have "\<dots> < Y + (-X) + 2" by simp
  18.152 +    finally show "s < Y + (-X) + 2" .
  18.153 +  qed
  18.154    moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto
  18.155    moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT"
  18.156      using X_in_S and Y_isUb by auto
  18.157 -  ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t"
  18.158 -    using posreals_complete [of ?SHIFT] by blast
  18.159 +  ultimately obtain t where t_is_Lub: "\<forall>y. (\<exists>x\<in>?SHIFT. y < x) = (y < t)"
  18.160 +    using posreal_complete [of ?SHIFT] unfolding bdd_above_def by blast
  18.161  
  18.162    show ?thesis
  18.163    proof
  18.164 -    show "isLub UNIV S (t + X + (-1))"
  18.165 -    proof (rule isLubI2)
  18.166 -      {
  18.167 -        fix x
  18.168 -        assume "isUb (UNIV::real set) S x"
  18.169 -        hence "isUb (UNIV::real set) (?SHIFT) (x + (-X) + 1)"
  18.170 -          using S_Ub_is_SHIFT_Ub by simp
  18.171 -        hence "t \<le> (x + (-X) + 1)"
  18.172 -          using t_is_Lub by (simp add: isLub_le_isUb)
  18.173 -        hence "t + X + -1 \<le> x" by arith
  18.174 -      }
  18.175 -      then show "(t + X + -1) <=* Collect (isUb UNIV S)"
  18.176 -        by (simp add: setgeI)
  18.177 +    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)"
  18.178 +    proof safe
  18.179 +      fix x
  18.180 +      assume "\<forall>s\<in>S. s \<le> x"
  18.181 +      hence "\<forall>s\<in>?SHIFT. s \<le> x + (-X) + 1"
  18.182 +        using S_Ub_is_SHIFT_Ub by simp
  18.183 +      then have "\<not> x + (-X) + 1 < t"
  18.184 +        by (subst t_is_Lub[rule_format, symmetric]) (simp add: not_less)
  18.185 +      thus "t + X + -1 \<le> x" by arith
  18.186      next
  18.187 -      show "isUb UNIV S (t + X + -1)"
  18.188 -      proof -
  18.189 -        {
  18.190 -          fix y
  18.191 -          assume y_in_S: "y \<in> S"
  18.192 -          have "y \<le> t + X + -1"
  18.193 -          proof -
  18.194 -            obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
  18.195 -            hence "\<exists> x \<in> S. u = x + - X + 1" by simp
  18.196 -            then obtain "x" where x_and_u: "u = x + - X + 1" ..
  18.197 -            have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2)
  18.198 +      fix y
  18.199 +      assume y_in_S: "y \<in> S"
  18.200 +      obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty ..
  18.201 +      hence "\<exists> x \<in> S. u = x + - X + 1" by simp
  18.202 +      then obtain "x" where x_and_u: "u = x + - X + 1" ..
  18.203 +      have u_le_t: "u \<le> t"
  18.204 +      proof (rule dense_le)
  18.205 +        fix x assume "x < u" then have "x < t"
  18.206 +          using u_in_shift t_is_Lub by auto
  18.207 +        then show "x \<le> t"  by simp
  18.208 +      qed
  18.209  
  18.210 -            show ?thesis
  18.211 -            proof cases
  18.212 -              assume "y \<le> x"
  18.213 -              moreover have "x = u + X + - 1" using x_and_u by arith
  18.214 -              moreover have "u + X + - 1  \<le> t + X + -1" using u_le_t by arith
  18.215 -              ultimately show "y  \<le> t + X + -1" by arith
  18.216 -            next
  18.217 -              assume "~(y \<le> x)"
  18.218 -              hence x_less_y: "x < y" by arith
  18.219 +      show "y \<le> t + X + -1"
  18.220 +      proof cases
  18.221 +        assume "y \<le> x"
  18.222 +        moreover have "x = u + X + - 1" using x_and_u by arith
  18.223 +        moreover have "u + X + - 1  \<le> t + X + -1" using u_le_t by arith
  18.224 +        ultimately show "y  \<le> t + X + -1" by arith
  18.225 +      next
  18.226 +        assume "~(y \<le> x)"
  18.227 +        hence x_less_y: "x < y" by arith
  18.228  
  18.229 -              have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
  18.230 -              hence "0 < x + (-X) + 1" by simp
  18.231 -              hence "0 < y + (-X) + 1" using x_less_y by arith
  18.232 -              hence "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
  18.233 -              hence "y + (-X) + 1 \<le> t" using t_is_Lub  by (simp add: isLubD2)
  18.234 -              thus ?thesis by simp
  18.235 -            qed
  18.236 -          qed
  18.237 -        }
  18.238 -        then show ?thesis by (simp add: isUb_def setle_def)
  18.239 +        have "x + (-X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp
  18.240 +        hence "0 < x + (-X) + 1" by simp
  18.241 +        hence "0 < y + (-X) + 1" using x_less_y by arith
  18.242 +        hence *: "y + (-X) + 1 \<in> ?SHIFT" using y_in_S by simp
  18.243 +        have "y + (-X) + 1 \<le> t"
  18.244 +        proof (rule dense_le)
  18.245 +          fix x assume "x < y + (-X) + 1" then have "x < t"
  18.246 +            using * t_is_Lub by auto
  18.247 +          then show "x \<le> t"  by simp
  18.248 +        qed
  18.249 +        thus ?thesis by simp
  18.250        qed
  18.251      qed
  18.252    qed
  18.253  qed
  18.254  
  18.255 -text{*A version of the same theorem without all those predicates!*}
  18.256 -lemma reals_complete2:
  18.257 -  fixes S :: "(real set)"
  18.258 -  assumes "\<exists>y. y\<in>S" and "\<exists>(x::real). \<forall>y\<in>S. y \<le> x"
  18.259 -  shows "\<exists>x. (\<forall>y\<in>S. y \<le> x) & 
  18.260 -               (\<forall>z. ((\<forall>y\<in>S. y \<le> z) --> x \<le> z))"
  18.261 -proof -
  18.262 -  have "\<exists>x. isLub UNIV S x" 
  18.263 -    by (rule reals_complete)
  18.264 -       (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def assms)
  18.265 -  thus ?thesis
  18.266 -    by (metis UNIV_I isLub_isUb isLub_le_isUb isUbD isUb_def setleI)
  18.267 -qed
  18.268 -
  18.269 -
  18.270  subsection {* The Archimedean Property of the Reals *}
  18.271  
  18.272  theorem reals_Archimedean:
  18.273 @@ -1969,34 +1871,30 @@
  18.274        by (rule mult_right_mono)
  18.275      thus "x * of_nat (Suc n) \<le> 1" by (simp del: of_nat_Suc)
  18.276    qed
  18.277 -  hence "{z. \<exists>n. z = x * (of_nat (Suc n))} *<= 1"
  18.278 -    by (simp add: setle_def del: of_nat_Suc, safe, rule spec)
  18.279 -  hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} 1"
  18.280 -    by (simp add: isUbI)
  18.281 -  hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (of_nat (Suc n))} Y" ..
  18.282 -  moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
  18.283 -  ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t"
  18.284 -    by (simp add: reals_complete)
  18.285 -  then obtain "t" where
  18.286 -    t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * of_nat (Suc n)} t" ..
  18.287 +  hence 2: "bdd_above {z. \<exists>n. z = x * (of_nat (Suc n))}"
  18.288 +    by (auto intro!: bdd_aboveI[of _ 1])
  18.289 +  have 1: "\<exists>X. X \<in> {z. \<exists>n. z = x* (of_nat (Suc n))}" by auto
  18.290 +  obtain t where
  18.291 +    upper: "\<And>z. z \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> z \<le> t" and
  18.292 +    least: "\<And>y. (\<And>a. a \<in> {z. \<exists>n. z = x * of_nat (Suc n)} \<Longrightarrow> a \<le> y) \<Longrightarrow> t \<le> y"
  18.293 +    using reals_complete[OF 1 2] by auto
  18.294 +
  18.295  
  18.296 -  have "\<forall>n::nat. x * of_nat n \<le> t + - x"
  18.297 -  proof
  18.298 -    fix n
  18.299 -    from t_is_Lub have "x * of_nat (Suc n) \<le> t"
  18.300 -      by (simp add: isLubD2)
  18.301 -    hence  "x * (of_nat n) + x \<le> t"
  18.302 -      by (simp add: distrib_left)
  18.303 -    thus  "x * (of_nat n) \<le> t + - x" by arith
  18.304 +  have "t \<le> t + - x"
  18.305 +  proof (rule least)
  18.306 +    fix a assume a: "a \<in> {z. \<exists>n. z = x * (of_nat (Suc n))}"
  18.307 +    have "\<forall>n::nat. x * of_nat n \<le> t + - x"
  18.308 +    proof
  18.309 +      fix n
  18.310 +      have "x * of_nat (Suc n) \<le> t"
  18.311 +        by (simp add: upper)
  18.312 +      hence  "x * (of_nat n) + x \<le> t"
  18.313 +        by (simp add: distrib_left)
  18.314 +      thus  "x * (of_nat n) \<le> t + - x" by arith
  18.315 +    qed    hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
  18.316 +    with a show "a \<le> t + - x"
  18.317 +      by auto
  18.318    qed
  18.319 -
  18.320 -  hence "\<forall>m. x * of_nat (Suc m) \<le> t + - x" by (simp del: of_nat_Suc)
  18.321 -  hence "{z. \<exists>n. z = x * (of_nat (Suc n))}  *<= (t + - x)"
  18.322 -    by (auto simp add: setle_def)
  18.323 -  hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (of_nat (Suc n))} (t + (-x))"
  18.324 -    by (simp add: isUbI)
  18.325 -  hence "t \<le> t + - x"
  18.326 -    using t_is_Lub by (simp add: isLub_le_isUb)
  18.327    thus False using x_pos by arith
  18.328  qed
  18.329