New theory SupInf of the supremum and infimum operators for sets of reals.
authorpaulson
Tue Oct 27 12:59:57 2009 +0000 (2009-10-27)
changeset 332693b7e2dbbd684
parent 33083 1fad3160d873
child 33270 320a1d67b9ae
New theory SupInf of the supremum and infimum operators for sets of reals.
NEWS
src/HOL/Complex_Main.thy
src/HOL/IsaMakefile
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/SupInf.thy
     1.1 --- a/NEWS	Fri Oct 23 14:33:07 2009 +0200
     1.2 +++ b/NEWS	Tue Oct 27 12:59:57 2009 +0000
     1.3 @@ -62,6 +62,8 @@
     1.4  of finite and infinite sets. It is shown that they form a complete
     1.5  lattice.
     1.6  
     1.7 +* New theory SupInf of the supremum and infimum operators for sets of reals.
     1.8 +
     1.9  * Split off prime number ingredients from theory GCD
    1.10  to theory Number_Theory/Primes;
    1.11  
     2.1 --- a/src/HOL/Complex_Main.thy	Fri Oct 23 14:33:07 2009 +0200
     2.2 +++ b/src/HOL/Complex_Main.thy	Tue Oct 27 12:59:57 2009 +0000
     2.3 @@ -4,6 +4,7 @@
     2.4  imports
     2.5    Main
     2.6    Real
     2.7 +  SupInf
     2.8    Complex
     2.9    Log
    2.10    Ln
     3.1 --- a/src/HOL/IsaMakefile	Fri Oct 23 14:33:07 2009 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Tue Oct 27 12:59:57 2009 +0000
     3.3 @@ -307,6 +307,7 @@
     3.4    RealVector.thy \
     3.5    SEQ.thy \
     3.6    Series.thy \
     3.7 +  SupInf.thy \
     3.8    Taylor.thy \
     3.9    Transcendental.thy \
    3.10    Tools/float_syntax.ML \
     4.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
     4.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
     4.3 @@ -1133,7 +1133,7 @@
     4.4      hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
     4.5        apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
     4.6        apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto  }
     4.7 -  thus ?thesis unfolding convex_def cone_def by blast
     4.8 +  thus ?thesis unfolding convex_def cone_def by auto
     4.9  qed
    4.10  
    4.11  lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
    4.12 @@ -1742,17 +1742,16 @@
    4.13      using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
    4.14      using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast)
    4.15    hence ab:"\<forall>x\<in>s. \<forall>y\<in>t. b + inner a y < inner a x" apply- apply(rule,rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
    4.16 -  def k \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
    4.17 +  def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
    4.18    show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI)
    4.19      apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
    4.20      from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
    4.21        apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
    4.22 -    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
    4.23 +    hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
    4.24      fix x assume "x\<in>t" thus "inner a x < (k + b / 2)" using `0<b` and isLubD2[OF k, of "inner a x"] by auto
    4.25    next
    4.26      fix x assume "x\<in>s" 
    4.27 -    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
    4.28 -      unfolding setle_def
    4.29 +    hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
    4.30        using ab[THEN bspec[where x=x]] by auto
    4.31      thus "k + b / 2 < inner a x" using `0 < b` by auto
    4.32    qed
    4.33 @@ -1794,11 +1793,20 @@
    4.34    assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
    4.35    shows "\<exists>a b. a \<noteq> 0 \<and> (\<forall>x\<in>s. inner a x \<le> b) \<and> (\<forall>x\<in>t. inner a x \<ge> b)"
    4.36  proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
    4.37 -  obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x"  using assms(3-5) by auto 
    4.38 -  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x" apply- apply(rule, rule) apply(erule_tac x="x - y" in ballE) by (auto simp add: inner_diff)
    4.39 -  thus ?thesis apply(rule_tac x=a in exI, rule_tac x="rsup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
    4.40 -    apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def
    4.41 -    prefer 4 using assms(3-5) by blast+ qed
    4.42 +  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" 
    4.43 +    using assms(3-5) by auto 
    4.44 +  hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
    4.45 +    by (force simp add: inner_diff)
    4.46 +  thus ?thesis
    4.47 +    apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
    4.48 +    apply auto
    4.49 +    apply (rule Sup[THEN isLubD2]) 
    4.50 +    prefer 4
    4.51 +    apply (rule Sup_least) 
    4.52 +     using assms(3-5) apply (auto simp add: setle_def)
    4.53 +    apply (metis COMBC_def Collect_def Collect_mem_eq) 
    4.54 +    done
    4.55 +qed
    4.56  
    4.57  subsection {* More convexity generalities. *}
    4.58  
    4.59 @@ -2571,12 +2579,17 @@
    4.60      thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm 
    4.61        by(auto simp add: vector_component_simps) qed
    4.62    hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
    4.63 -    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
    4.64 -  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed
    4.65 -
    4.66 -subsection {* Line segments, starlike sets etc.                                         *)
    4.67 -(* Use the same overloading tricks as for intervals, so that                 *)
    4.68 -(* segment[a,b] is closed and segment(a,b) is open relative to affine hull. *}
    4.69 +    apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
    4.70 +    apply force
    4.71 +    done
    4.72 +  thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball]
    4.73 +    using `d>0` by auto 
    4.74 +qed
    4.75 +
    4.76 +subsection {* Line segments, Starlike Sets, etc.*}
    4.77 +
    4.78 +(* Use the same overloading tricks as for intervals, so that 
    4.79 +   segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
    4.80  
    4.81  definition
    4.82    midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
     5.1 --- a/src/HOL/Library/Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
     5.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
     5.3 @@ -2297,242 +2297,9 @@
     5.4    ultimately show ?thesis by metis
     5.5  qed
     5.6  
     5.7 -(* Supremum and infimum of real sets *)
     5.8 -
     5.9 -
    5.10 -definition rsup:: "real set \<Rightarrow> real" where
    5.11 -  "rsup S = (SOME a. isLub UNIV S a)"
    5.12 -
    5.13 -lemma rsup_alt: "rsup S = (SOME a. (\<forall>x \<in> S. x \<le> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<le> b) \<longrightarrow> a \<le> b))"  by (auto simp  add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def)
    5.14 -
    5.15 -lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>b. S *<= b"
    5.16 -  shows "isLub UNIV S (rsup S)"
    5.17 -using Se b
    5.18 -unfolding rsup_def
    5.19 -apply clarify
    5.20 -apply (rule someI_ex)
    5.21 -apply (rule reals_complete)
    5.22 -by (auto simp add: isUb_def setle_def)
    5.23 -
    5.24 -lemma rsup_le: assumes Se: "S \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> b"
    5.25 -proof-
    5.26 -  from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def)
    5.27 -  from rsup[OF Se] Sb have "isLub UNIV S (rsup S)"  by blast
    5.28 -  then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def)
    5.29 -qed
    5.30 -
    5.31 -lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.32 -  shows "rsup S = Max S"
    5.33 -using fS Se
    5.34 -proof-
    5.35 -  let ?m = "Max S"
    5.36 -  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
    5.37 -  with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def)
    5.38 -  from Max_in[OF fS Se] lub have mrS: "?m \<le> rsup S"
    5.39 -    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
    5.40 -  moreover
    5.41 -  have "rsup S \<le> ?m" using Sm lub
    5.42 -    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
    5.43 -  ultimately  show ?thesis by arith
    5.44 -qed
    5.45 -
    5.46 -lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.47 -  shows "rsup S \<in> S"
    5.48 -  using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
    5.49 -
    5.50 -lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.51 -  shows "isUb S S (rsup S)"
    5.52 -  using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS]
    5.53 -  unfolding isUb_def setle_def by metis
    5.54 -
    5.55 -lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.56 -  shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
    5.57 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    5.58 -
    5.59 -lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.60 -  shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
    5.61 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    5.62 -
    5.63 -lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.64 -  shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
    5.65 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    5.66 -
    5.67 -lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
    5.68 -  shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
    5.69 -using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
    5.70 -
    5.71 -lemma rsup_unique: assumes b: "S *<= b" and S: "\<forall>b' < b. \<exists>x \<in> S. b' < x"
    5.72 -  shows "rsup S = b"
    5.73 -using b S
    5.74 -unfolding setle_def rsup_alt
    5.75 -apply -
    5.76 -apply (rule some_equality)
    5.77 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
    5.78 -done
    5.79 -
    5.80 -lemma rsup_le_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> rsup T"
    5.81 -  apply (rule rsup_le)
    5.82 -  apply simp
    5.83 -  using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def)
    5.84 -
    5.85 -lemma isUb_def': "isUb R S = (\<lambda>x. S *<= x \<and> x \<in> R)"
    5.86 -  apply (rule ext)
    5.87 -  by (metis isUb_def)
    5.88 -
    5.89 -lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def)
    5.90 -lemma rsup_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
    5.91 -  shows "a \<le> rsup S \<and> rsup S \<le> b"
    5.92 -proof-
    5.93 -  from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
    5.94 -  hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
    5.95 -  from Se obtain y where y: "y \<in> S" by blast
    5.96 -  from lub l have "a \<le> rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
    5.97 -    apply (erule ballE[where x=y])
    5.98 -    apply (erule ballE[where x=y])
    5.99 -    apply arith
   5.100 -    using y apply auto
   5.101 -    done
   5.102 -  with b show ?thesis by blast
   5.103 -qed
   5.104 -
   5.105 -lemma rsup_abs_le: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> a"
   5.106 -  unfolding abs_le_interval_iff  using rsup_bounds[of S "-a" a]
   5.107 -  by (auto simp add: setge_def setle_def)
   5.108 -
   5.109 -lemma rsup_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rsup S - l\<bar> \<le> e"
   5.110 -proof-
   5.111 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
   5.112 -  show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th
   5.113 -    by  (auto simp add: setge_def setle_def)
   5.114 -qed
   5.115 -
   5.116 -definition rinf:: "real set \<Rightarrow> real" where
   5.117 -  "rinf S = (SOME a. isGlb UNIV S a)"
   5.118 -
   5.119 -lemma rinf_alt: "rinf S = (SOME a. (\<forall>x \<in> S. x \<ge> a) \<and> (\<forall>b. (\<forall>x \<in> S. x \<ge> b) \<longrightarrow> a \<ge> b))"  by (auto simp  add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def)
   5.120 -
   5.121 -lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
   5.122 -  shows "\<exists>(t::real). isGlb UNIV S t"
   5.123 -proof-
   5.124 -  let ?M = "uminus ` S"
   5.125 -  from lb have th: "\<exists>y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def)
   5.126 -    by (rule_tac x="-y" in exI, auto)
   5.127 -  from Se have Me: "\<exists>x. x \<in> ?M" by blast
   5.128 -  from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast
   5.129 -  have "isGlb UNIV S (- t)" using t
   5.130 -    apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def)
   5.131 -    apply (erule_tac x="-y" in allE)
   5.132 -    apply auto
   5.133 -    done
   5.134 -  then show ?thesis by metis
   5.135 -qed
   5.136 -
   5.137 -lemma rinf: assumes Se: "S \<noteq> {}" and b: "\<exists>b. b <=* S"
   5.138 -  shows "isGlb UNIV S (rinf S)"
   5.139 -using Se b
   5.140 -unfolding rinf_def
   5.141 -apply clarify
   5.142 -apply (rule someI_ex)
   5.143 -apply (rule reals_complete_Glb)
   5.144 -apply (auto simp add: isLb_def setle_def setge_def)
   5.145 -done
   5.146 -
   5.147 -lemma rinf_ge: assumes Se: "S \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> b"
   5.148 -proof-
   5.149 -  from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def)
   5.150 -  from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)"  by blast
   5.151 -  then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def)
   5.152 -qed
   5.153 -
   5.154 -lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.155 -  shows "rinf S = Min S"
   5.156 -using fS Se
   5.157 -proof-
   5.158 -  let ?m = "Min S"
   5.159 -  from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?m" by metis
   5.160 -  with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def)
   5.161 -  from Min_in[OF fS Se] glb have mrS: "?m \<ge> rinf S"
   5.162 -    by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
   5.163 -  moreover
   5.164 -  have "rinf S \<ge> ?m" using Sm glb
   5.165 -    by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def)
   5.166 -  ultimately  show ?thesis by arith
   5.167 -qed
   5.168 -
   5.169 -lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.170 -  shows "rinf S \<in> S"
   5.171 -  using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
   5.172 -
   5.173 -lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.174 -  shows "isLb S S (rinf S)"
   5.175 -  using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS]
   5.176 -  unfolding isLb_def setge_def by metis
   5.177 -
   5.178 -lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.179 -  shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   5.180 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   5.181 -
   5.182 -lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.183 -  shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   5.184 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   5.185 -
   5.186 -lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.187 -  shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   5.188 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   5.189 -
   5.190 -lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
   5.191 -  shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   5.192 -using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
   5.193 -
   5.194 -lemma rinf_unique: assumes b: "b <=* S" and S: "\<forall>b' > b. \<exists>x \<in> S. b' > x"
   5.195 -  shows "rinf S = b"
   5.196 -using b S
   5.197 -unfolding setge_def rinf_alt
   5.198 -apply -
   5.199 -apply (rule some_equality)
   5.200 -apply (metis  linorder_not_le order_eq_iff[symmetric])+
   5.201 -done
   5.202 -
   5.203 -lemma rinf_ge_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> rinf S >= rinf T"
   5.204 -  apply (rule rinf_ge)
   5.205 -  apply simp
   5.206 -  using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def)
   5.207 -
   5.208 -lemma isLb_def': "isLb R S = (\<lambda>x. x <=* S \<and> x \<in> R)"
   5.209 -  apply (rule ext)
   5.210 -  by (metis isLb_def)
   5.211 -
   5.212 -lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   5.213 -  shows "a \<le> rinf S \<and> rinf S \<le> b"
   5.214 -proof-
   5.215 -  from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
   5.216 -  hence b: "a \<le> rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
   5.217 -  from Se obtain y where y: "y \<in> S" by blast
   5.218 -  from lub u have "b \<ge> rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
   5.219 -    apply (erule ballE[where x=y])
   5.220 -    apply (erule ballE[where x=y])
   5.221 -    apply arith
   5.222 -    using y apply auto
   5.223 -    done
   5.224 -  with b show ?thesis by blast
   5.225 -qed
   5.226 -
   5.227 -lemma rinf_abs_ge: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> a"
   5.228 -  unfolding abs_le_interval_iff  using rinf_bounds[of S "-a" a]
   5.229 -  by (auto simp add: setge_def setle_def)
   5.230 -
   5.231 -lemma rinf_asclose: assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>rinf S - l\<bar> \<le> e"
   5.232 -proof-
   5.233 -  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
   5.234 -  show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th
   5.235 -    by  (auto simp add: setge_def setle_def)
   5.236 -qed
   5.237 -
   5.238 -
   5.239 -
   5.240  subsection{* Operator norm. *}
   5.241  
   5.242 -definition "onorm f = rsup {norm (f x)| x. norm x = 1}"
   5.243 +definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
   5.244  
   5.245  lemma norm_bound_generalize:
   5.246    fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
   5.247 @@ -2578,7 +2345,7 @@
   5.248      have Se: "?S \<noteq> {}" using  norm_basis by auto
   5.249      from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
   5.250        unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
   5.251 -    {from rsup[OF Se b, unfolded onorm_def[symmetric]]
   5.252 +    {from Sup[OF Se b, unfolded onorm_def[symmetric]]
   5.253        show "norm (f x) <= onorm f * norm x"
   5.254          apply -
   5.255          apply (rule spec[where x = x])
   5.256 @@ -2586,7 +2353,7 @@
   5.257          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   5.258      {
   5.259        show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
   5.260 -        using rsup[OF Se b, unfolded onorm_def[symmetric]]
   5.261 +        using Sup[OF Se b, unfolded onorm_def[symmetric]]
   5.262          unfolding norm_bound_generalize[OF lf, symmetric]
   5.263          by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
   5.264    }
   5.265 @@ -2612,7 +2379,7 @@
   5.266      by(auto intro: vector_choose_size set_ext)
   5.267    show ?thesis
   5.268      unfolding onorm_def th
   5.269 -    apply (rule rsup_unique) by (simp_all  add: setle_def)
   5.270 +    apply (rule Sup_unique) by (simp_all  add: setle_def)
   5.271  qed
   5.272  
   5.273  lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
   5.274 @@ -3055,31 +2822,6 @@
   5.275  qed
   5.276  
   5.277  (* ------------------------------------------------------------------------- *)
   5.278 -(* Relate max and min to sup and inf.                                        *)
   5.279 -(* ------------------------------------------------------------------------- *)
   5.280 -
   5.281 -lemma real_max_rsup: "max x y = rsup {x,y}"
   5.282 -proof-
   5.283 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   5.284 -  from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
   5.285 -  moreover
   5.286 -  have "max x y \<le> rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"]
   5.287 -    by (simp add: linorder_linear)
   5.288 -  ultimately show ?thesis by arith
   5.289 -qed
   5.290 -
   5.291 -lemma real_min_rinf: "min x y = rinf {x,y}"
   5.292 -proof-
   5.293 -  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   5.294 -  from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
   5.295 -    by (simp add: linorder_linear)
   5.296 -  moreover
   5.297 -  have "min x y \<le> rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"]
   5.298 -    by simp
   5.299 -  ultimately show ?thesis by arith
   5.300 -qed
   5.301 -
   5.302 -(* ------------------------------------------------------------------------- *)
   5.303  (* Geometric progression.                                                    *)
   5.304  (* ------------------------------------------------------------------------- *)
   5.305  
   5.306 @@ -5048,7 +4790,7 @@
   5.307  
   5.308  (* Infinity norm.                                                            *)
   5.309  
   5.310 -definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
   5.311 +definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
   5.312  
   5.313  lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
   5.314    by auto
   5.315 @@ -5065,7 +4807,7 @@
   5.316  
   5.317  lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
   5.318    unfolding infnorm_def
   5.319 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   5.320 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   5.321    unfolding infnorm_set_image
   5.322    by auto
   5.323  
   5.324 @@ -5076,13 +4818,13 @@
   5.325    have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
   5.326    show ?thesis
   5.327    unfolding infnorm_def
   5.328 -  unfolding rsup_finite_le_iff[ OF infnorm_set_lemma]
   5.329 +  unfolding Sup_finite_le_iff[ OF infnorm_set_lemma]
   5.330    apply (subst diff_le_eq[symmetric])
   5.331 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   5.332 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   5.333    unfolding infnorm_set_image bex_simps
   5.334    apply (subst th)
   5.335    unfolding th1
   5.336 -  unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
   5.337 +  unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
   5.338  
   5.339    unfolding infnorm_set_image ball_simps bex_simps
   5.340    apply simp
   5.341 @@ -5094,7 +4836,7 @@
   5.342  proof-
   5.343    have "infnorm x <= 0 \<longleftrightarrow> x = 0"
   5.344      unfolding infnorm_def
   5.345 -    unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
   5.346 +    unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   5.347      unfolding infnorm_set_image ball_simps
   5.348      by vector
   5.349    then show ?thesis using infnorm_pos_le[of x] by simp
   5.350 @@ -5105,7 +4847,7 @@
   5.351  
   5.352  lemma infnorm_neg: "infnorm (- x) = infnorm x"
   5.353    unfolding infnorm_def
   5.354 -  apply (rule cong[of "rsup" "rsup"])
   5.355 +  apply (rule cong[of "Sup" "Sup"])
   5.356    apply blast
   5.357    apply (rule set_ext)
   5.358    apply auto
   5.359 @@ -5140,14 +4882,15 @@
   5.360      apply (rule finite_imageI) unfolding Collect_def mem_def by simp
   5.361    have S0: "?S \<noteq> {}" by blast
   5.362    have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
   5.363 -  from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]
   5.364 -  show ?thesis unfolding infnorm_def isUb_def setle_def
   5.365 -    unfolding infnorm_set_image ball_simps by auto
   5.366 +  from Sup_finite_in[OF fS S0] 
   5.367 +  show ?thesis unfolding infnorm_def infnorm_set_image 
   5.368 +    by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty 
   5.369 +              rangeI real_le_refl)
   5.370  qed
   5.371  
   5.372  lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
   5.373    apply (subst infnorm_def)
   5.374 -  unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
   5.375 +  unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
   5.376    unfolding infnorm_set_image ball_simps
   5.377    apply (simp add: abs_mult)
   5.378    apply (rule allI)
   5.379 @@ -5180,7 +4923,7 @@
   5.380  (* Prove that it differs only up to a bound from Euclidean norm.             *)
   5.381  
   5.382  lemma infnorm_le_norm: "infnorm x \<le> norm x"
   5.383 -  unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]
   5.384 +  unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
   5.385    unfolding infnorm_set_image  ball_simps
   5.386    by (metis component_le_norm)
   5.387  lemma card_enum: "card {1 .. n} = n" by auto
   5.388 @@ -5200,7 +4943,7 @@
   5.389      apply (rule setsum_bounded)
   5.390      apply (rule power_mono)
   5.391      unfolding abs_of_nonneg[OF infnorm_pos_le]
   5.392 -    unfolding infnorm_def  rsup_finite_ge_iff[OF infnorm_set_lemma]
   5.393 +    unfolding infnorm_def  Sup_finite_ge_iff[OF infnorm_set_lemma]
   5.394      unfolding infnorm_set_image bex_simps
   5.395      apply blast
   5.396      by (rule abs_ge_zero)
     6.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Oct 23 14:33:07 2009 +0200
     6.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Oct 27 12:59:57 2009 +0000
     6.3 @@ -2100,59 +2100,54 @@
     6.4    shows "bounded S \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
     6.5    by (simp add: bounded_iff)
     6.6  
     6.7 -lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
     6.8 -  shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
     6.9 +lemma bounded_has_Sup:
    6.10 +  fixes S :: "real set"
    6.11 +  assumes "bounded S" "S \<noteq> {}"
    6.12 +  shows "\<forall>x\<in>S. x <= Sup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> Sup S <= b"
    6.13 +proof
    6.14 +  fix x assume "x\<in>S"
    6.15 +  thus "x \<le> Sup S"
    6.16 +    by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
    6.17 +next
    6.18 +  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
    6.19 +    by (metis SupInf.Sup_least)
    6.20 +qed
    6.21 +
    6.22 +lemma Sup_insert:
    6.23 +  fixes S :: "real set"
    6.24 +  shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))" 
    6.25 +by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal) 
    6.26 +
    6.27 +lemma Sup_insert_finite:
    6.28 +  fixes S :: "real set"
    6.29 +  shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
    6.30 +  apply (rule Sup_insert)
    6.31 +  apply (rule finite_imp_bounded)
    6.32 +  by simp
    6.33 +
    6.34 +lemma bounded_has_Inf:
    6.35 +  fixes S :: "real set"
    6.36 +  assumes "bounded S"  "S \<noteq> {}"
    6.37 +  shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
    6.38  proof
    6.39    fix x assume "x\<in>S"
    6.40    from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
    6.41 -  hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
    6.42 -  thus "x \<le> rsup S" using rsup[OF `S\<noteq>{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\<in>S` by auto
    6.43 -next
    6.44 -  show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> b" using assms
    6.45 -  using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def]
    6.46 -  apply (auto simp add: bounded_real)
    6.47 -  by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def)
    6.48 -qed
    6.49 -
    6.50 -lemma rsup_insert: assumes "bounded S"
    6.51 -  shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))"
    6.52 -proof(cases "S={}")
    6.53 -  case True thus ?thesis using rsup_finite_in[of "{x}"] by auto
    6.54 +  thus "x \<ge> Inf S" using `x\<in>S`
    6.55 +    by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
    6.56  next
    6.57 -  let ?S = "insert x S"
    6.58 -  case False
    6.59 -  hence *:"\<forall>x\<in>S. x \<le> rsup S" using bounded_has_rsup(1)[of S] using assms by auto
    6.60 -  hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto
    6.61 -  hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto
    6.62 -  moreover
    6.63 -  have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto
    6.64 -  { fix y assume as:"isUb UNIV (insert x S) y"
    6.65 -    hence "max x (rsup S) \<le> y" unfolding isUb_def using rsup_le[OF `S\<noteq>{}`]
    6.66 -      unfolding setle_def by auto  }
    6.67 -  hence "max x (rsup S) <=* isUb UNIV (insert x S)" unfolding setge_def Ball_def mem_def by auto
    6.68 -  hence "isLub UNIV ?S (max x (rsup S))" using ** isLubI2[of UNIV ?S "max x (rsup S)"] unfolding Collect_def by auto
    6.69 -  ultimately show ?thesis using real_isLub_unique[of UNIV ?S] using `S\<noteq>{}` by auto
    6.70 -qed
    6.71 -
    6.72 -lemma sup_insert_finite: "finite S \<Longrightarrow> rsup(insert x S) = (if S = {} then x else max x (rsup S))"
    6.73 -  apply (rule rsup_insert)
    6.74 -  apply (rule finite_imp_bounded)
    6.75 -  by simp
    6.76 -
    6.77 -lemma bounded_has_rinf:
    6.78 -  assumes "bounded S"  "S \<noteq> {}"
    6.79 -  shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
    6.80 -proof
    6.81 -  fix x assume "x\<in>S"
    6.82 -  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
    6.83 -  hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
    6.84 -  thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
    6.85 -next
    6.86 -  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> b" using assms
    6.87 -  using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def]
    6.88 -  apply (auto simp add: bounded_real)
    6.89 -  by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def)
    6.90 -qed
    6.91 +  show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
    6.92 +    by (metis SupInf.Inf_greatest)
    6.93 +qed
    6.94 +
    6.95 +lemma Inf_insert:
    6.96 +  fixes S :: "real set"
    6.97 +  shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))" 
    6.98 +by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal) 
    6.99 +lemma Inf_insert_finite:
   6.100 +  fixes S :: "real set"
   6.101 +  shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
   6.102 +  by (rule Inf_insert, rule finite_imp_bounded, simp)
   6.103 +
   6.104  
   6.105  (* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
   6.106  lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
   6.107 @@ -2161,29 +2156,6 @@
   6.108    apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
   6.109    done
   6.110  
   6.111 -lemma rinf_insert: assumes "bounded S"
   6.112 -  shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs")
   6.113 -proof(cases "S={}")
   6.114 -  case True thus ?thesis using rinf_finite_in[of "{x}"] by auto
   6.115 -next
   6.116 -  let ?S = "insert x S"
   6.117 -  case False
   6.118 -  hence *:"\<forall>x\<in>S. x \<ge> rinf S" using bounded_has_rinf(1)[of S] using assms by auto
   6.119 -  hence "min x (rinf S) <=* insert x S" unfolding setge_def by auto
   6.120 -  hence "isGlb UNIV ?S (rinf ?S)" using rinf[of ?S] by auto
   6.121 -  moreover
   6.122 -  have **:"isLb UNIV ?S (min x (rinf S))" unfolding isLb_def setge_def using * by auto
   6.123 -  { fix y assume as:"isLb UNIV (insert x S) y"
   6.124 -    hence "min x (rinf S) \<ge> y" unfolding isLb_def using rinf_ge[OF `S\<noteq>{}`]
   6.125 -      unfolding setge_def by auto  }
   6.126 -  hence "isLb UNIV (insert x S) *<= min x (rinf S)" unfolding setle_def Ball_def mem_def by auto
   6.127 -  hence "isGlb UNIV ?S (min x (rinf S))" using ** isGlbI2[of UNIV ?S "min x (rinf S)"] unfolding Collect_def by auto
   6.128 -  ultimately show ?thesis using real_isGlb_unique[of UNIV ?S] using `S\<noteq>{}` by auto
   6.129 -qed
   6.130 -
   6.131 -lemma inf_insert_finite: "finite S ==> rinf(insert x S) = (if S = {} then x else min x (rinf S))"
   6.132 -  by (rule rinf_insert, rule finite_imp_bounded, simp)
   6.133 -
   6.134  subsection{* Compactness (the definition is the one based on convegent subsequences). *}
   6.135  
   6.136  definition
   6.137 @@ -4120,30 +4092,35 @@
   6.138    shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
   6.139  proof-
   6.140    from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
   6.141 -  { fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> rsup s - x' < e"
   6.142 -    have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto
   6.143 -    moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
   6.144 -    ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto  }
   6.145 -  thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]]
   6.146 -    apply(rule_tac x="rsup s" in bexI) by auto
   6.147 -qed
   6.148 +  { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s"  "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e"
   6.149 +    have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
   6.150 +    moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
   6.151 +    ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto  }
   6.152 +  thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
   6.153 +    apply(rule_tac x="Sup s" in bexI) by auto
   6.154 +qed
   6.155 +
   6.156 +lemma Inf:
   6.157 +  fixes S :: "real set"
   6.158 +  shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
   6.159 +by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def) 
   6.160  
   6.161  lemma compact_attains_inf:
   6.162    fixes s :: "real set"
   6.163    assumes "compact s" "s \<noteq> {}"  shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
   6.164  proof-
   6.165    from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
   6.166 -  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s"  "rinf s \<notin> s"  "0 < e"
   6.167 -      "\<forall>x'\<in>s. x' = rinf s \<or> \<not> abs (x' - rinf s) < e"
   6.168 -    have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto
   6.169 +  { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s"  "Inf s \<notin> s"  "0 < e"
   6.170 +      "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
   6.171 +    have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
   6.172      moreover
   6.173      { fix x assume "x \<in> s"
   6.174 -      hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto
   6.175 -      have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
   6.176 -    hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto
   6.177 -    ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto  }
   6.178 -  thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]]
   6.179 -    apply(rule_tac x="rinf s" in bexI) by auto
   6.180 +      hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
   6.181 +      have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
   6.182 +    hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
   6.183 +    ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto  }
   6.184 +  thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
   6.185 +    apply(rule_tac x="Inf s" in bexI) by auto
   6.186  qed
   6.187  
   6.188  lemma continuous_attains_sup:
   6.189 @@ -4413,7 +4390,7 @@
   6.190  
   6.191  text{* We can state this in terms of diameter of a set.                          *}
   6.192  
   6.193 -definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
   6.194 +definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
   6.195    (* TODO: generalize to class metric_space *)
   6.196  
   6.197  lemma diameter_bounded:
   6.198 @@ -4427,12 +4404,22 @@
   6.199      hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
   6.200    note * = this
   6.201    { fix x y assume "x\<in>s" "y\<in>s"  hence "s \<noteq> {}" by auto
   6.202 -    have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
   6.203 +    have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
   6.204 +      apply auto    (*FIXME: something horrible has happened here!*)
   6.205 +      apply atomize
   6.206 +      apply safe
   6.207 +      apply metis +
   6.208 +      done
   6.209      have "norm(x - y) \<le> diameter s" unfolding diameter_def using `s\<noteq>{}` *[OF `x\<in>s` `y\<in>s`] `x\<in>s` `y\<in>s` isLubD1[OF lub] unfolding setle_def by auto  }
   6.210    moreover
   6.211    { fix d::real assume "d>0" "d < diameter s"
   6.212      hence "s\<noteq>{}" unfolding diameter_def by auto
   6.213 -    hence lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] unfolding setle_def by auto
   6.214 +    hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def 
   6.215 +      apply auto    (*FIXME: something horrible has happened here!*)
   6.216 +      apply atomize
   6.217 +      apply safe
   6.218 +      apply metis +
   6.219 +      done
   6.220      have "\<exists>d' \<in> ?D. d' > d"
   6.221      proof(rule ccontr)
   6.222        assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
   6.223 @@ -4448,6 +4435,7 @@
   6.224  lemma diameter_bounded_bound:
   6.225   "bounded s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s ==> norm(x - y) \<le> diameter s"
   6.226    using diameter_bounded by blast
   6.227 +atp_minimize [atp=remote_vampire] Collect_def Max_ge add_increasing2 add_le_cancel_left diameter_def_raw equation_minus_iff finite finite_imageI norm_imp_pos_and_ge rangeI
   6.228  
   6.229  lemma diameter_compact_attained:
   6.230    fixes s :: "'a::real_normed_vector set"
   6.231 @@ -4456,8 +4444,8 @@
   6.232  proof-
   6.233    have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
   6.234    then obtain x y where xys:"x\<in>s" "y\<in>s" and xy:"\<forall>u\<in>s. \<forall>v\<in>s. norm (u - v) \<le> norm (x - y)" using compact_sup_maxdistance[OF assms] by auto
   6.235 -  hence "diameter s \<le> norm (x - y)" using rsup_le[of "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}" "norm (x - y)"]
   6.236 -    unfolding setle_def and diameter_def by auto
   6.237 +  hence "diameter s \<le> norm (x - y)" 
   6.238 +    by (force simp add: diameter_def intro!: Sup_least) 
   6.239    thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto
   6.240  qed
   6.241  
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/SupInf.thy	Tue Oct 27 12:59:57 2009 +0000
     7.3 @@ -0,0 +1,467 @@
     7.4 +(*  Author: Amine Chaieb and L C Paulson, University of Cambridge *)
     7.5 +
     7.6 +header {*Sup and Inf Operators on Sets of Reals.*}
     7.7 +
     7.8 +theory SupInf
     7.9 +imports RComplete
    7.10 +begin
    7.11 +
    7.12 +lemma minus_max_eq_min:
    7.13 +  fixes x :: "'a::{lordered_ab_group_add, linorder}"
    7.14 +  shows "- (max x y) = min (-x) (-y)"
    7.15 +by (metis le_imp_neg_le linorder_linear min_max.inf_absorb2 min_max.le_iff_inf min_max.le_iff_sup min_max.sup_absorb1)
    7.16 +
    7.17 +lemma minus_min_eq_max:
    7.18 +  fixes x :: "'a::{lordered_ab_group_add, linorder}"
    7.19 +  shows "- (min x y) = max (-x) (-y)"
    7.20 +by (metis minus_max_eq_min minus_minus)
    7.21 +
    7.22 +lemma minus_Max_eq_Min [simp]:
    7.23 +  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
    7.24 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
    7.25 +proof (induct S rule: finite_ne_induct)
    7.26 +  case (singleton x)
    7.27 +  thus ?case by simp
    7.28 +next
    7.29 +  case (insert x S)
    7.30 +  thus ?case by (simp add: minus_max_eq_min) 
    7.31 +qed
    7.32 +
    7.33 +lemma minus_Min_eq_Max [simp]:
    7.34 +  fixes S :: "'a::{lordered_ab_group_add, linorder} set"
    7.35 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
    7.36 +proof (induct S rule: finite_ne_induct)
    7.37 +  case (singleton x)
    7.38 +  thus ?case by simp
    7.39 +next
    7.40 +  case (insert x S)
    7.41 +  thus ?case by (simp add: minus_min_eq_max) 
    7.42 +qed
    7.43 +
    7.44 +instantiation real :: Sup 
    7.45 +begin
    7.46 +definition
    7.47 +  Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
    7.48 +
    7.49 +instance ..
    7.50 +end
    7.51 +
    7.52 +instantiation real :: Inf 
    7.53 +begin
    7.54 +definition
    7.55 +  Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
    7.56 +
    7.57 +instance ..
    7.58 +end
    7.59 +
    7.60 +subsection{*Supremum of a set of reals*}
    7.61 +
    7.62 +lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
    7.63 +  fixes x :: real
    7.64 +  assumes x: "x \<in> X"
    7.65 +      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
    7.66 +  shows "x \<le> Sup X"
    7.67 +proof (auto simp add: Sup_real_def) 
    7.68 +  from reals_complete2
    7.69 +  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
    7.70 +    by (blast intro: x z)
    7.71 +  hence "x \<le> s"
    7.72 +    by (blast intro: x z)
    7.73 +  also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
    7.74 +    by (fast intro: Least_equality [symmetric])  
    7.75 +  finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
    7.76 +qed
    7.77 +
    7.78 +lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
    7.79 +  fixes z :: real
    7.80 +  assumes x: "X \<noteq> {}"
    7.81 +      and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
    7.82 +  shows "Sup X \<le> z"
    7.83 +proof (auto simp add: Sup_real_def) 
    7.84 +  from reals_complete2 x
    7.85 +  obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
    7.86 +    by (blast intro: z)
    7.87 +  hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
    7.88 +    by (best intro: Least_equality)  
    7.89 +  also with s z have "... \<le> z"
    7.90 +    by blast
    7.91 +  finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
    7.92 +qed
    7.93 +
    7.94 +lemma Sup_singleton [simp]: "Sup {x::real} = x"
    7.95 +  by (force intro: Least_equality simp add: Sup_real_def)
    7.96 + 
    7.97 +lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
    7.98 +  fixes z :: real
    7.99 +  assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   7.100 +  shows  "Sup X = z"
   7.101 +  by (force intro: Least_equality X z simp add: Sup_real_def)
   7.102 + 
   7.103 +lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
   7.104 +  fixes x :: real
   7.105 +  shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
   7.106 +  by (metis Sup_upper real_le_trans)
   7.107 +
   7.108 +lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
   7.109 +  fixes z :: real
   7.110 +  shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
   7.111 +  by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
   7.112 +
   7.113 +lemma Sup_eq:
   7.114 +  fixes a :: real
   7.115 +  shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
   7.116 +        \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
   7.117 +  by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
   7.118 +        insert_not_empty real_le_anti_sym)
   7.119 +
   7.120 +lemma Sup_le:
   7.121 +  fixes S :: "real set"
   7.122 +  shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
   7.123 +by (metis SupInf.Sup_least setle_def)
   7.124 +
   7.125 +lemma Sup_upper_EX: 
   7.126 +  fixes x :: real
   7.127 +  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow>  x \<le> Sup X"
   7.128 +  by blast
   7.129 +
   7.130 +lemma Sup_insert_nonempty: 
   7.131 +  fixes x :: real
   7.132 +  assumes x: "x \<in> X"
   7.133 +      and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   7.134 +  shows "Sup (insert a X) = max a (Sup X)"
   7.135 +proof (cases "Sup X \<le> a")
   7.136 +  case True
   7.137 +  thus ?thesis
   7.138 +    apply (simp add: max_def) 
   7.139 +    apply (rule Sup_eq_maximum)
   7.140 +    apply (metis insertCI)
   7.141 +    apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)     
   7.142 +    done
   7.143 +next
   7.144 +  case False
   7.145 +  hence 1:"a < Sup X" by simp
   7.146 +  have "Sup X \<le> Sup (insert a X)"
   7.147 +    apply (rule Sup_least)
   7.148 +    apply (metis empty_psubset_nonempty psubset_eq x)
   7.149 +    apply (rule Sup_upper_EX) 
   7.150 +    apply blast
   7.151 +    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
   7.152 +    done
   7.153 +  moreover 
   7.154 +  have "Sup (insert a X) \<le> Sup X"
   7.155 +    apply (rule Sup_least)
   7.156 +    apply blast
   7.157 +    apply (metis False Sup_upper insertE real_le_linear z) 
   7.158 +    done
   7.159 +  ultimately have "Sup (insert a X) = Sup X"
   7.160 +    by (blast intro:  antisym )
   7.161 +  thus ?thesis
   7.162 +    by (metis 1 min_max.le_iff_sup real_less_def)
   7.163 +qed
   7.164 +
   7.165 +lemma Sup_insert_if: 
   7.166 +  fixes X :: "real set"
   7.167 +  assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
   7.168 +  shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
   7.169 +by auto (metis Sup_insert_nonempty z) 
   7.170 +
   7.171 +lemma Sup: 
   7.172 +  fixes S :: "real set"
   7.173 +  shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
   7.174 +by  (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI) 
   7.175 +
   7.176 +lemma Sup_finite_Max: 
   7.177 +  fixes S :: "real set"
   7.178 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.179 +  shows "Sup S = Max S"
   7.180 +using fS Se
   7.181 +proof-
   7.182 +  let ?m = "Max S"
   7.183 +  from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
   7.184 +  with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
   7.185 +  from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
   7.186 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   7.187 +  moreover
   7.188 +  have "Sup S \<le> ?m" using Sm lub
   7.189 +    by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
   7.190 +  ultimately  show ?thesis by arith
   7.191 +qed
   7.192 +
   7.193 +lemma Sup_finite_in:
   7.194 +  fixes S :: "real set"
   7.195 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.196 +  shows "Sup S \<in> S"
   7.197 +  using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
   7.198 +
   7.199 +lemma Sup_finite_ge_iff: 
   7.200 +  fixes S :: "real set"
   7.201 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.202 +  shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
   7.203 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
   7.204 +
   7.205 +lemma Sup_finite_le_iff: 
   7.206 +  fixes S :: "real set"
   7.207 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.208 +  shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
   7.209 +by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans) 
   7.210 +
   7.211 +lemma Sup_finite_gt_iff: 
   7.212 +  fixes S :: "real set"
   7.213 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.214 +  shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
   7.215 +by (metis Se Sup_finite_le_iff fS linorder_not_less)
   7.216 +
   7.217 +lemma Sup_finite_lt_iff: 
   7.218 +  fixes S :: "real set"
   7.219 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.220 +  shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
   7.221 +by (metis Se Sup_finite_ge_iff fS linorder_not_less)
   7.222 +
   7.223 +lemma Sup_unique:
   7.224 +  fixes S :: "real set"
   7.225 +  shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
   7.226 +unfolding setle_def
   7.227 +apply (rule Sup_eq, auto) 
   7.228 +apply (metis linorder_not_less) 
   7.229 +done
   7.230 +
   7.231 +lemma Sup_abs_le:
   7.232 +  fixes S :: "real set"
   7.233 +  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
   7.234 +by (auto simp add: abs_le_interval_iff) (metis Sup_upper2) 
   7.235 +
   7.236 +lemma Sup_bounds:
   7.237 +  fixes S :: "real set"
   7.238 +  assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
   7.239 +  shows "a \<le> Sup S \<and> Sup S \<le> b"
   7.240 +proof-
   7.241 +  from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
   7.242 +  hence b: "Sup S \<le> b" using u 
   7.243 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) 
   7.244 +  from Se obtain y where y: "y \<in> S" by blast
   7.245 +  from lub l have "a \<le> Sup S"
   7.246 +    by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
   7.247 +       (metis le_iff_sup le_sup_iff y)
   7.248 +  with b show ?thesis by blast
   7.249 +qed
   7.250 +
   7.251 +lemma Sup_asclose: 
   7.252 +  fixes S :: "real set"
   7.253 +  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
   7.254 +proof-
   7.255 +  have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
   7.256 +  thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
   7.257 +    by  (auto simp add: setge_def setle_def)
   7.258 +qed
   7.259 +
   7.260 +
   7.261 +subsection{*Infimum of a set of reals*}
   7.262 +
   7.263 +lemma Inf_lower [intro]: 
   7.264 +  fixes z :: real
   7.265 +  assumes x: "x \<in> X"
   7.266 +      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   7.267 +  shows "Inf X \<le> x"
   7.268 +proof -
   7.269 +  have "-x \<le> Sup (uminus ` X)"
   7.270 +    by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
   7.271 +  thus ?thesis 
   7.272 +    by (auto simp add: Inf_real_def)
   7.273 +qed
   7.274 +
   7.275 +lemma Inf_greatest [intro]: 
   7.276 +  fixes z :: real
   7.277 +  assumes x: "X \<noteq> {}"
   7.278 +      and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
   7.279 +  shows "z \<le> Inf X"
   7.280 +proof -
   7.281 +  have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
   7.282 +  hence "z \<le> - Sup (uminus ` X)"
   7.283 +    by simp
   7.284 +  thus ?thesis 
   7.285 +    by (auto simp add: Inf_real_def)
   7.286 +qed
   7.287 +
   7.288 +lemma Inf_singleton [simp]: "Inf {x::real} = x"
   7.289 +  by (simp add: Inf_real_def) 
   7.290 + 
   7.291 +lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
   7.292 +  fixes z :: real
   7.293 +  assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   7.294 +  shows  "Inf X = z"
   7.295 +proof -
   7.296 +  have "Sup (uminus ` X) = -z" using x z
   7.297 +    by (force intro: Sup_eq_maximum x z)
   7.298 +  thus ?thesis
   7.299 +    by (simp add: Inf_real_def) 
   7.300 +qed
   7.301 + 
   7.302 +lemma Inf_lower2:
   7.303 +  fixes x :: real
   7.304 +  shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
   7.305 +  by (metis Inf_lower real_le_trans)
   7.306 +
   7.307 +lemma Inf_real_iff:
   7.308 +  fixes z :: real
   7.309 +  shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
   7.310 +  by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear 
   7.311 +            order_less_le_trans)
   7.312 +
   7.313 +lemma Inf_eq:
   7.314 +  fixes a :: real
   7.315 +  shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
   7.316 +  by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
   7.317 +        insert_absorb insert_not_empty real_le_anti_sym)
   7.318 +
   7.319 +lemma Inf_ge: 
   7.320 +  fixes S :: "real set"
   7.321 +  shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
   7.322 +by (metis SupInf.Inf_greatest setge_def)
   7.323 +
   7.324 +lemma Inf_lower_EX: 
   7.325 +  fixes x :: real
   7.326 +  shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
   7.327 +  by blast
   7.328 +
   7.329 +lemma Inf_insert_nonempty: 
   7.330 +  fixes x :: real
   7.331 +  assumes x: "x \<in> X"
   7.332 +      and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   7.333 +  shows "Inf (insert a X) = min a (Inf X)"
   7.334 +proof (cases "a \<le> Inf X")
   7.335 +  case True
   7.336 +  thus ?thesis
   7.337 +    by (simp add: min_def)
   7.338 +       (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z) 
   7.339 +next
   7.340 +  case False
   7.341 +  hence 1:"Inf X < a" by simp
   7.342 +  have "Inf (insert a X) \<le> Inf X"
   7.343 +    apply (rule Inf_greatest)
   7.344 +    apply (metis empty_psubset_nonempty psubset_eq x)
   7.345 +    apply (rule Inf_lower_EX) 
   7.346 +    apply (blast intro: elim:) 
   7.347 +    apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
   7.348 +    done
   7.349 +  moreover 
   7.350 +  have "Inf X \<le> Inf (insert a X)"
   7.351 +    apply (rule Inf_greatest)
   7.352 +    apply blast
   7.353 +    apply (metis False Inf_lower insertE real_le_linear z) 
   7.354 +    done
   7.355 +  ultimately have "Inf (insert a X) = Inf X"
   7.356 +    by (blast intro:  antisym )
   7.357 +  thus ?thesis
   7.358 +    by (metis False min_max.inf_absorb2 real_le_linear)
   7.359 +qed
   7.360 +
   7.361 +lemma Inf_insert_if: 
   7.362 +  fixes X :: "real set"
   7.363 +  assumes z:  "!!x. x \<in> X \<Longrightarrow> z \<le> x"
   7.364 +  shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
   7.365 +by auto (metis Inf_insert_nonempty z) 
   7.366 +
   7.367 +text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
   7.368 +lemma Inf_binary:
   7.369 +  "Inf{a, b::real} = min a b"
   7.370 +  by (subst Inf_insert_nonempty, auto)
   7.371 +
   7.372 +lemma Inf_greater:
   7.373 +  fixes z :: real
   7.374 +  shows "X \<noteq> {} \<Longrightarrow>  Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
   7.375 +  by (metis Inf_real_iff mem_def not_leE)
   7.376 +
   7.377 +lemma Inf_close:
   7.378 +  fixes e :: real
   7.379 +  shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
   7.380 +  by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
   7.381 +
   7.382 +lemma Inf_finite_Min:
   7.383 +  fixes S :: "real set"
   7.384 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
   7.385 +by (simp add: Inf_real_def Sup_finite_Max image_image) 
   7.386 +
   7.387 +lemma Inf_finite_in: 
   7.388 +  fixes S :: "real set"
   7.389 +  assumes fS: "finite S" and Se: "S \<noteq> {}"
   7.390 +  shows "Inf S \<in> S"
   7.391 +  using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
   7.392 +
   7.393 +lemma Inf_finite_ge_iff: 
   7.394 +  fixes S :: "real set"
   7.395 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
   7.396 +by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
   7.397 +
   7.398 +lemma Inf_finite_le_iff:
   7.399 +  fixes S :: "real set"
   7.400 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   7.401 +by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
   7.402 +          real_le_anti_sym real_le_linear)
   7.403 +
   7.404 +lemma Inf_finite_gt_iff: 
   7.405 +  fixes S :: "real set"
   7.406 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
   7.407 +by (metis Inf_finite_le_iff linorder_not_less)
   7.408 +
   7.409 +lemma Inf_finite_lt_iff: 
   7.410 +  fixes S :: "real set"
   7.411 +  shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
   7.412 +by (metis Inf_finite_ge_iff linorder_not_less)
   7.413 +
   7.414 +lemma Inf_unique:
   7.415 +  fixes S :: "real set"
   7.416 +  shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
   7.417 +unfolding setge_def
   7.418 +apply (rule Inf_eq, auto) 
   7.419 +apply (metis less_le_not_le linorder_not_less) 
   7.420 +done
   7.421 +
   7.422 +lemma Inf_abs_ge:
   7.423 +  fixes S :: "real set"
   7.424 +  shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
   7.425 +by (simp add: Inf_real_def) (rule Sup_abs_le, auto) 
   7.426 +
   7.427 +lemma Inf_asclose:
   7.428 +  fixes S :: "real set"
   7.429 +  assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
   7.430 +proof -
   7.431 +  have "\<bar>- Sup (uminus ` S) - l\<bar> =  \<bar>Sup (uminus ` S) - (-l)\<bar>"
   7.432 +    by auto
   7.433 +  also have "... \<le> e" 
   7.434 +    apply (rule Sup_asclose) 
   7.435 +    apply (auto simp add: S)
   7.436 +    apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def) 
   7.437 +    done
   7.438 +  finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   7.439 +  thus ?thesis
   7.440 +    by (simp add: Inf_real_def)
   7.441 +qed
   7.442 +
   7.443 +subsection{*Relate max and min to sup and inf.*}
   7.444 +
   7.445 +lemma real_max_Sup:
   7.446 +  fixes x :: real
   7.447 +  shows "max x y = Sup {x,y}"
   7.448 +proof-
   7.449 +  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   7.450 +  from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
   7.451 +  moreover
   7.452 +  have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
   7.453 +    by (simp add: linorder_linear)
   7.454 +  ultimately show ?thesis by arith
   7.455 +qed
   7.456 +
   7.457 +lemma real_min_Inf: 
   7.458 +  fixes x :: real
   7.459 +  shows "min x y = Inf {x,y}"
   7.460 +proof-
   7.461 +  have f: "finite {x, y}" "{x,y} \<noteq> {}"  by simp_all
   7.462 +  from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
   7.463 +    by (simp add: linorder_linear)
   7.464 +  moreover
   7.465 +  have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
   7.466 +    by simp
   7.467 +  ultimately show ?thesis by arith
   7.468 +qed
   7.469 +
   7.470 +end