New theory SupInf of the supremum and infimum operators for sets of reals.
--- a/NEWS Fri Oct 23 14:33:07 2009 +0200
+++ b/NEWS Tue Oct 27 12:59:57 2009 +0000
@@ -62,6 +62,8 @@
of finite and infinite sets. It is shown that they form a complete
lattice.
+* New theory SupInf of the supremum and infimum operators for sets of reals.
+
* Split off prime number ingredients from theory GCD
to theory Number_Theory/Primes;
--- a/src/HOL/Complex_Main.thy Fri Oct 23 14:33:07 2009 +0200
+++ b/src/HOL/Complex_Main.thy Tue Oct 27 12:59:57 2009 +0000
@@ -4,6 +4,7 @@
imports
Main
Real
+ SupInf
Complex
Log
Ln
--- a/src/HOL/IsaMakefile Fri Oct 23 14:33:07 2009 +0200
+++ b/src/HOL/IsaMakefile Tue Oct 27 12:59:57 2009 +0000
@@ -307,6 +307,7 @@
RealVector.thy \
SEQ.thy \
Series.thy \
+ SupInf.thy \
Taylor.thy \
Transcendental.thy \
Tools/float_syntax.ML \
--- a/src/HOL/Library/Convex_Euclidean_Space.thy Fri Oct 23 14:33:07 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy Tue Oct 27 12:59:57 2009 +0000
@@ -1133,7 +1133,7 @@
hence "x + y \<in> s" using `?lhs`[unfolded convex_def, THEN conjunct1]
apply(erule_tac x="2*\<^sub>R x" in ballE) apply(erule_tac x="2*\<^sub>R y" in ballE)
apply(erule_tac x="1/2" in allE) apply simp apply(erule_tac x="1/2" in allE) by auto }
- thus ?thesis unfolding convex_def cone_def by blast
+ thus ?thesis unfolding convex_def cone_def by auto
qed
lemma affine_dependent_biggerset: fixes s::"(real^'n::finite) set"
@@ -1742,17 +1742,16 @@
using separating_hyperplane_closed_point[OF convex_differences[OF assms(1,3)], of 0]
using closed_compact_differences[OF assms(2,4)] using assms(6) by(auto, blast)
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)
- def k \<equiv> "rsup ((\<lambda>x. inner a x) ` t)"
+ def k \<equiv> "Sup ((\<lambda>x. inner a x) ` t)"
show ?thesis apply(rule_tac x="-a" in exI, rule_tac x="-(k + b / 2)" in exI)
apply(rule,rule) defer apply(rule) unfolding inner_minus_left and neg_less_iff_less proof-
from ab have "((\<lambda>x. inner a x) ` t) *<= (inner a y - b)"
apply(erule_tac x=y in ballE) apply(rule setleI) using `y\<in>s` by auto
- hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto
+ hence k:"isLub UNIV ((\<lambda>x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto
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
next
fix x assume "x\<in>s"
- hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5)
- unfolding setle_def
+ hence "k \<le> inner a x - b" unfolding k_def apply(rule_tac Sup_least) using assms(5)
using ab[THEN bspec[where x=x]] by auto
thus "k + b / 2 < inner a x" using `0 < b` by auto
qed
@@ -1794,11 +1793,20 @@
assumes "convex s" "convex (t::(real^'n::finite) set)" "s \<noteq> {}" "t \<noteq> {}" "s \<inter> t = {}"
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)"
proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]]
- obtain a where "a\<noteq>0" "\<forall>x\<in>{x - y |x y. x \<in> t \<and> y \<in> s}. 0 \<le> inner a x" using assms(3-5) by auto
- 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)
- 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`
- apply(rule) apply(rule,rule) apply(rule rsup[THEN isLubD2]) prefer 4 apply(rule,rule rsup_le) unfolding setle_def
- prefer 4 using assms(3-5) by blast+ qed
+ 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
+ hence "\<forall>x\<in>t. \<forall>y\<in>s. inner a y \<le> inner a x"
+ by (force simp add: inner_diff)
+ thus ?thesis
+ apply(rule_tac x=a in exI, rule_tac x="Sup ((\<lambda>x. inner a x) ` s)" in exI) using `a\<noteq>0`
+ apply auto
+ apply (rule Sup[THEN isLubD2])
+ prefer 4
+ apply (rule Sup_least)
+ using assms(3-5) apply (auto simp add: setle_def)
+ apply (metis COMBC_def Collect_def Collect_mem_eq)
+ done
+qed
subsection {* More convexity generalities. *}
@@ -2571,12 +2579,17 @@
thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm
by(auto simp add: vector_component_simps) qed
hence "continuous_on (ball x d) f" apply(rule_tac convex_on_bounded_continuous)
- apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
- thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball] using `d>0` by auto qed
-
-subsection {* Line segments, starlike sets etc. *)
-(* Use the same overloading tricks as for intervals, so that *)
-(* segment[a,b] is closed and segment(a,b) is open relative to affine hull. *}
+ apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball)
+ apply force
+ done
+ thus "continuous (at x) f" unfolding continuous_on_eq_continuous_at[OF open_ball]
+ using `d>0` by auto
+qed
+
+subsection {* Line segments, Starlike Sets, etc.*}
+
+(* Use the same overloading tricks as for intervals, so that
+ segment[a,b] is closed and segment(a,b) is open relative to affine hull. *)
definition
midpoint :: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
--- a/src/HOL/Library/Euclidean_Space.thy Fri Oct 23 14:33:07 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy Tue Oct 27 12:59:57 2009 +0000
@@ -2297,242 +2297,9 @@
ultimately show ?thesis by metis
qed
-(* Supremum and infimum of real sets *)
-
-
-definition rsup:: "real set \<Rightarrow> real" where
- "rsup S = (SOME a. isLub UNIV S a)"
-
-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)
-
-lemma rsup: assumes Se: "S \<noteq> {}" and b: "\<exists>b. S *<= b"
- shows "isLub UNIV S (rsup S)"
-using Se b
-unfolding rsup_def
-apply clarify
-apply (rule someI_ex)
-apply (rule reals_complete)
-by (auto simp add: isUb_def setle_def)
-
-lemma rsup_le: assumes Se: "S \<noteq> {}" and Sb: "S *<= b" shows "rsup S \<le> b"
-proof-
- from Sb have bu: "isUb UNIV S b" by (simp add: isUb_def setle_def)
- from rsup[OF Se] Sb have "isLub UNIV S (rsup S)" by blast
- then show ?thesis using bu by (auto simp add: isLub_def leastP_def setle_def setge_def)
-qed
-
-lemma rsup_finite_Max: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "rsup S = Max S"
-using fS Se
-proof-
- let ?m = "Max S"
- from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
- with rsup[OF Se] have lub: "isLub UNIV S (rsup S)" by (metis setle_def)
- from Max_in[OF fS Se] lub have mrS: "?m \<le> rsup S"
- by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
- moreover
- have "rsup S \<le> ?m" using Sm lub
- by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
- ultimately show ?thesis by arith
-qed
-
-lemma rsup_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "rsup S \<in> S"
- using rsup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
-
-lemma rsup_finite_Ub: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "isUb S S (rsup S)"
- using rsup_finite_Max[OF fS Se] rsup_finite_in[OF fS Se] Max_ge[OF fS]
- unfolding isUb_def setle_def by metis
-
-lemma rsup_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<le> rsup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<ge> rsup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a < rsup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a > rsup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
-using rsup_finite_Ub[OF fS Se] by (auto simp add: isUb_def setle_def)
-
-lemma rsup_unique: assumes b: "S *<= b" and S: "\<forall>b' < b. \<exists>x \<in> S. b' < x"
- shows "rsup S = b"
-using b S
-unfolding setle_def rsup_alt
-apply -
-apply (rule some_equality)
-apply (metis linorder_not_le order_eq_iff[symmetric])+
-done
-
-lemma rsup_le_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. T *<= b) \<Longrightarrow> rsup S \<le> rsup T"
- apply (rule rsup_le)
- apply simp
- using rsup[of T] by (auto simp add: isLub_def leastP_def setge_def setle_def isUb_def)
-
-lemma isUb_def': "isUb R S = (\<lambda>x. S *<= x \<and> x \<in> R)"
- apply (rule ext)
- by (metis isUb_def)
-
-lemma UNIV_trivial: "UNIV x" using UNIV_I[of x] by (metis mem_def)
-lemma rsup_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
- shows "a \<le> rsup S \<and> rsup S \<le> b"
-proof-
- from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast
- hence b: "rsup S \<le> b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
- from Se obtain y where y: "y \<in> S" by blast
- from lub l have "a \<le> rsup S" apply (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def')
- apply (erule ballE[where x=y])
- apply (erule ballE[where x=y])
- apply arith
- using y apply auto
- done
- with b show ?thesis by blast
-qed
-
-lemma rsup_abs_le: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rsup S\<bar> \<le> a"
- unfolding abs_le_interval_iff using rsup_bounds[of S "-a" a]
- by (auto simp add: setge_def setle_def)
-
-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"
-proof-
- have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
- show ?thesis using S b rsup_bounds[of S "l - e" "l+e"] unfolding th
- by (auto simp add: setge_def setle_def)
-qed
-
-definition rinf:: "real set \<Rightarrow> real" where
- "rinf S = (SOME a. isGlb UNIV S a)"
-
-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)
-
-lemma reals_complete_Glb: assumes Se: "\<exists>x. x \<in> S" and lb: "\<exists> y. isLb UNIV S y"
- shows "\<exists>(t::real). isGlb UNIV S t"
-proof-
- let ?M = "uminus ` S"
- from lb have th: "\<exists>y. isUb UNIV ?M y" apply (auto simp add: isUb_def isLb_def setle_def setge_def)
- by (rule_tac x="-y" in exI, auto)
- from Se have Me: "\<exists>x. x \<in> ?M" by blast
- from reals_complete[OF Me th] obtain t where t: "isLub UNIV ?M t" by blast
- have "isGlb UNIV S (- t)" using t
- apply (auto simp add: isLub_def isGlb_def leastP_def greatestP_def setle_def setge_def isUb_def isLb_def)
- apply (erule_tac x="-y" in allE)
- apply auto
- done
- then show ?thesis by metis
-qed
-
-lemma rinf: assumes Se: "S \<noteq> {}" and b: "\<exists>b. b <=* S"
- shows "isGlb UNIV S (rinf S)"
-using Se b
-unfolding rinf_def
-apply clarify
-apply (rule someI_ex)
-apply (rule reals_complete_Glb)
-apply (auto simp add: isLb_def setle_def setge_def)
-done
-
-lemma rinf_ge: assumes Se: "S \<noteq> {}" and Sb: "b <=* S" shows "rinf S \<ge> b"
-proof-
- from Sb have bu: "isLb UNIV S b" by (simp add: isLb_def setge_def)
- from rinf[OF Se] Sb have "isGlb UNIV S (rinf S)" by blast
- then show ?thesis using bu by (auto simp add: isGlb_def greatestP_def setle_def setge_def)
-qed
-
-lemma rinf_finite_Min: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "rinf S = Min S"
-using fS Se
-proof-
- let ?m = "Min S"
- from Min_le[OF fS] have Sm: "\<forall> x\<in> S. x \<ge> ?m" by metis
- with rinf[OF Se] have glb: "isGlb UNIV S (rinf S)" by (metis setge_def)
- from Min_in[OF fS Se] glb have mrS: "?m \<ge> rinf S"
- by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def)
- moreover
- have "rinf S \<ge> ?m" using Sm glb
- by (auto simp add: isGlb_def greatestP_def isLb_def setle_def setge_def)
- ultimately show ?thesis by arith
-qed
-
-lemma rinf_finite_in: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "rinf S \<in> S"
- using rinf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
-
-lemma rinf_finite_Lb: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "isLb S S (rinf S)"
- using rinf_finite_Min[OF fS Se] rinf_finite_in[OF fS Se] Min_le[OF fS]
- unfolding isLb_def setge_def by metis
-
-lemma rinf_finite_ge_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<le> rinf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_finite_le_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a \<ge> rinf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_finite_gt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a < rinf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_finite_lt_iff: assumes fS: "finite S" and Se: "S \<noteq> {}"
- shows "a > rinf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
-using rinf_finite_Lb[OF fS Se] by (auto simp add: isLb_def setge_def)
-
-lemma rinf_unique: assumes b: "b <=* S" and S: "\<forall>b' > b. \<exists>x \<in> S. b' > x"
- shows "rinf S = b"
-using b S
-unfolding setge_def rinf_alt
-apply -
-apply (rule some_equality)
-apply (metis linorder_not_le order_eq_iff[symmetric])+
-done
-
-lemma rinf_ge_subset: "S\<noteq>{} \<Longrightarrow> S \<subseteq> T \<Longrightarrow> (\<exists>b. b <=* T) \<Longrightarrow> rinf S >= rinf T"
- apply (rule rinf_ge)
- apply simp
- using rinf[of T] by (auto simp add: isGlb_def greatestP_def setge_def setle_def isLb_def)
-
-lemma isLb_def': "isLb R S = (\<lambda>x. x <=* S \<and> x \<in> R)"
- apply (rule ext)
- by (metis isLb_def)
-
-lemma rinf_bounds: assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
- shows "a \<le> rinf S \<and> rinf S \<le> b"
-proof-
- from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast
- hence b: "a \<le> rinf S" using l by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
- from Se obtain y where y: "y \<in> S" by blast
- from lub u have "b \<ge> rinf S" apply (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def')
- apply (erule ballE[where x=y])
- apply (erule ballE[where x=y])
- apply arith
- using y apply auto
- done
- with b show ?thesis by blast
-qed
-
-lemma rinf_abs_ge: "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>rinf S\<bar> \<le> a"
- unfolding abs_le_interval_iff using rinf_bounds[of S "-a" a]
- by (auto simp add: setge_def setle_def)
-
-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"
-proof-
- have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
- show ?thesis using S b rinf_bounds[of S "l - e" "l+e"] unfolding th
- by (auto simp add: setge_def setle_def)
-qed
-
-
-
subsection{* Operator norm. *}
-definition "onorm f = rsup {norm (f x)| x. norm x = 1}"
+definition "onorm f = Sup {norm (f x)| x. norm x = 1}"
lemma norm_bound_generalize:
fixes f:: "real ^'n::finite \<Rightarrow> real^'m::finite"
@@ -2578,7 +2345,7 @@
have Se: "?S \<noteq> {}" using norm_basis by auto
from linear_bounded[OF lf] have b: "\<exists> b. ?S *<= b"
unfolding norm_bound_generalize[OF lf, symmetric] by (auto simp add: setle_def)
- {from rsup[OF Se b, unfolded onorm_def[symmetric]]
+ {from Sup[OF Se b, unfolded onorm_def[symmetric]]
show "norm (f x) <= onorm f * norm x"
apply -
apply (rule spec[where x = x])
@@ -2586,7 +2353,7 @@
by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
{
show "\<forall>x. norm (f x) <= b * norm x \<Longrightarrow> onorm f <= b"
- using rsup[OF Se b, unfolded onorm_def[symmetric]]
+ using Sup[OF Se b, unfolded onorm_def[symmetric]]
unfolding norm_bound_generalize[OF lf, symmetric]
by (auto simp add: isLub_def isUb_def leastP_def setge_def setle_def)}
}
@@ -2612,7 +2379,7 @@
by(auto intro: vector_choose_size set_ext)
show ?thesis
unfolding onorm_def th
- apply (rule rsup_unique) by (simp_all add: setle_def)
+ apply (rule Sup_unique) by (simp_all add: setle_def)
qed
lemma onorm_pos_lt: assumes lf: "linear (f::real ^ 'n::finite \<Rightarrow> real ^'m::finite)"
@@ -3055,31 +2822,6 @@
qed
(* ------------------------------------------------------------------------- *)
-(* Relate max and min to sup and inf. *)
-(* ------------------------------------------------------------------------- *)
-
-lemma real_max_rsup: "max x y = rsup {x,y}"
-proof-
- have f: "finite {x, y}" "{x,y} \<noteq> {}" by simp_all
- from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \<le> max x y" by simp
- moreover
- have "max x y \<le> rsup {x,y}" using rsup_finite_ge_iff[OF f, of "max x y"]
- by (simp add: linorder_linear)
- ultimately show ?thesis by arith
-qed
-
-lemma real_min_rinf: "min x y = rinf {x,y}"
-proof-
- have f: "finite {x, y}" "{x,y} \<noteq> {}" by simp_all
- from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \<le> min x y"
- by (simp add: linorder_linear)
- moreover
- have "min x y \<le> rinf {x,y}" using rinf_finite_ge_iff[OF f, of "min x y"]
- by simp
- ultimately show ?thesis by arith
-qed
-
-(* ------------------------------------------------------------------------- *)
(* Geometric progression. *)
(* ------------------------------------------------------------------------- *)
@@ -5048,7 +4790,7 @@
(* Infinity norm. *)
-definition "infnorm (x::real^'n::finite) = rsup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
+definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\<in> (UNIV :: 'n set)}"
lemma numseg_dimindex_nonempty: "\<exists>i. i \<in> (UNIV :: 'n set)"
by auto
@@ -5065,7 +4807,7 @@
lemma infnorm_pos_le: "0 \<le> infnorm (x::real^'n::finite)"
unfolding infnorm_def
- unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
+ unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
unfolding infnorm_set_image
by auto
@@ -5076,13 +4818,13 @@
have th2: "\<And>x (y::real). abs(x + y) - abs(x) <= abs(y)" by arith
show ?thesis
unfolding infnorm_def
- unfolding rsup_finite_le_iff[ OF infnorm_set_lemma]
+ unfolding Sup_finite_le_iff[ OF infnorm_set_lemma]
apply (subst diff_le_eq[symmetric])
- unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
+ unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
unfolding infnorm_set_image bex_simps
apply (subst th)
unfolding th1
- unfolding rsup_finite_ge_iff[ OF infnorm_set_lemma]
+ unfolding Sup_finite_ge_iff[ OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps bex_simps
apply simp
@@ -5094,7 +4836,7 @@
proof-
have "infnorm x <= 0 \<longleftrightarrow> x = 0"
unfolding infnorm_def
- unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
+ unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps
by vector
then show ?thesis using infnorm_pos_le[of x] by simp
@@ -5105,7 +4847,7 @@
lemma infnorm_neg: "infnorm (- x) = infnorm x"
unfolding infnorm_def
- apply (rule cong[of "rsup" "rsup"])
+ apply (rule cong[of "Sup" "Sup"])
apply blast
apply (rule set_ext)
apply auto
@@ -5140,14 +4882,15 @@
apply (rule finite_imageI) unfolding Collect_def mem_def by simp
have S0: "?S \<noteq> {}" by blast
have th1: "\<And>S f. f ` S = { f i| i. i \<in> S}" by blast
- from rsup_finite_in[OF fS S0] rsup_finite_Ub[OF fS S0]
- show ?thesis unfolding infnorm_def isUb_def setle_def
- unfolding infnorm_set_image ball_simps by auto
+ from Sup_finite_in[OF fS S0]
+ show ?thesis unfolding infnorm_def infnorm_set_image
+ by (metis Sup_finite_ge_iff finite finite_imageI UNIV_not_empty image_is_empty
+ rangeI real_le_refl)
qed
lemma infnorm_mul_lemma: "infnorm(a *s x) <= \<bar>a\<bar> * infnorm x"
apply (subst infnorm_def)
- unfolding rsup_finite_le_iff[OF infnorm_set_lemma]
+ unfolding Sup_finite_le_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps
apply (simp add: abs_mult)
apply (rule allI)
@@ -5180,7 +4923,7 @@
(* Prove that it differs only up to a bound from Euclidean norm. *)
lemma infnorm_le_norm: "infnorm x \<le> norm x"
- unfolding infnorm_def rsup_finite_le_iff[OF infnorm_set_lemma]
+ unfolding infnorm_def Sup_finite_le_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image ball_simps
by (metis component_le_norm)
lemma card_enum: "card {1 .. n} = n" by auto
@@ -5200,7 +4943,7 @@
apply (rule setsum_bounded)
apply (rule power_mono)
unfolding abs_of_nonneg[OF infnorm_pos_le]
- unfolding infnorm_def rsup_finite_ge_iff[OF infnorm_set_lemma]
+ unfolding infnorm_def Sup_finite_ge_iff[OF infnorm_set_lemma]
unfolding infnorm_set_image bex_simps
apply blast
by (rule abs_ge_zero)
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Oct 23 14:33:07 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Tue Oct 27 12:59:57 2009 +0000
@@ -2100,59 +2100,54 @@
shows "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. abs x <= a)"
by (simp add: bounded_iff)
-lemma bounded_has_rsup: assumes "bounded S" "S \<noteq> {}"
- shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
+lemma bounded_has_Sup:
+ fixes S :: "real set"
+ assumes "bounded S" "S \<noteq> {}"
+ shows "\<forall>x\<in>S. x <= Sup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> Sup S <= b"
+proof
+ fix x assume "x\<in>S"
+ thus "x \<le> Sup S"
+ by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real)
+next
+ show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> Sup S \<le> b" using assms
+ by (metis SupInf.Sup_least)
+qed
+
+lemma Sup_insert:
+ fixes S :: "real set"
+ shows "bounded S ==> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
+by auto (metis Int_absorb Sup_insert_nonempty assms bounded_has_Sup(1) disjoint_iff_not_equal)
+
+lemma Sup_insert_finite:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
+ apply (rule Sup_insert)
+ apply (rule finite_imp_bounded)
+ by simp
+
+lemma bounded_has_Inf:
+ fixes S :: "real set"
+ assumes "bounded S" "S \<noteq> {}"
+ shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
proof
fix x assume "x\<in>S"
from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
- hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def)
- 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
-next
- show "\<forall>b. (\<forall>x\<in>S. x \<le> b) \<longrightarrow> rsup S \<le> b" using assms
- using rsup[of S, unfolded isLub_def isUb_def leastP_def setle_def setge_def]
- apply (auto simp add: bounded_real)
- by (auto simp add: isLub_def isUb_def leastP_def setle_def setge_def)
-qed
-
-lemma rsup_insert: assumes "bounded S"
- shows "rsup(insert x S) = (if S = {} then x else max x (rsup S))"
-proof(cases "S={}")
- case True thus ?thesis using rsup_finite_in[of "{x}"] by auto
+ thus "x \<ge> Inf S" using `x\<in>S`
+ by (metis Inf_lower_EX abs_le_D2 minus_le_iff)
next
- let ?S = "insert x S"
- case False
- hence *:"\<forall>x\<in>S. x \<le> rsup S" using bounded_has_rsup(1)[of S] using assms by auto
- hence "insert x S *<= max x (rsup S)" unfolding setle_def by auto
- hence "isLub UNIV ?S (rsup ?S)" using rsup[of ?S] by auto
- moreover
- have **:"isUb UNIV ?S (max x (rsup S))" unfolding isUb_def setle_def using * by auto
- { fix y assume as:"isUb UNIV (insert x S) y"
- hence "max x (rsup S) \<le> y" unfolding isUb_def using rsup_le[OF `S\<noteq>{}`]
- unfolding setle_def by auto }
- hence "max x (rsup S) <=* isUb UNIV (insert x S)" unfolding setge_def Ball_def mem_def by auto
- hence "isLub UNIV ?S (max x (rsup S))" using ** isLubI2[of UNIV ?S "max x (rsup S)"] unfolding Collect_def by auto
- ultimately show ?thesis using real_isLub_unique[of UNIV ?S] using `S\<noteq>{}` by auto
-qed
-
-lemma sup_insert_finite: "finite S \<Longrightarrow> rsup(insert x S) = (if S = {} then x else max x (rsup S))"
- apply (rule rsup_insert)
- apply (rule finite_imp_bounded)
- by simp
-
-lemma bounded_has_rinf:
- assumes "bounded S" "S \<noteq> {}"
- shows "\<forall>x\<in>S. x >= rinf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S >= b"
-proof
- fix x assume "x\<in>S"
- from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
- hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto
- thus "x \<ge> rinf S" using rinf[OF `S\<noteq>{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\<in>S` by auto
-next
- show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> rinf S \<ge> b" using assms
- using rinf[of S, unfolded isGlb_def isLb_def greatestP_def setle_def setge_def]
- apply (auto simp add: bounded_real)
- by (auto simp add: isGlb_def isLb_def greatestP_def setle_def setge_def)
-qed
+ show "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S \<ge> b" using assms
+ by (metis SupInf.Inf_greatest)
+qed
+
+lemma Inf_insert:
+ fixes S :: "real set"
+ shows "bounded S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
+by auto (metis Int_absorb Inf_insert_nonempty bounded_has_Inf(1) disjoint_iff_not_equal)
+lemma Inf_insert_finite:
+ fixes S :: "real set"
+ shows "finite S ==> Inf(insert x S) = (if S = {} then x else min x (Inf S))"
+ by (rule Inf_insert, rule finite_imp_bounded, simp)
+
(* TODO: Move this to RComplete.thy -- would need to include Glb into RComplete *)
lemma real_isGlb_unique: "[| isGlb R S x; isGlb R S y |] ==> x = (y::real)"
@@ -2161,29 +2156,6 @@
apply (blast intro!: order_antisym dest!: isGlb_le_isLb)
done
-lemma rinf_insert: assumes "bounded S"
- shows "rinf(insert x S) = (if S = {} then x else min x (rinf S))" (is "?lhs = ?rhs")
-proof(cases "S={}")
- case True thus ?thesis using rinf_finite_in[of "{x}"] by auto
-next
- let ?S = "insert x S"
- case False
- hence *:"\<forall>x\<in>S. x \<ge> rinf S" using bounded_has_rinf(1)[of S] using assms by auto
- hence "min x (rinf S) <=* insert x S" unfolding setge_def by auto
- hence "isGlb UNIV ?S (rinf ?S)" using rinf[of ?S] by auto
- moreover
- have **:"isLb UNIV ?S (min x (rinf S))" unfolding isLb_def setge_def using * by auto
- { fix y assume as:"isLb UNIV (insert x S) y"
- hence "min x (rinf S) \<ge> y" unfolding isLb_def using rinf_ge[OF `S\<noteq>{}`]
- unfolding setge_def by auto }
- hence "isLb UNIV (insert x S) *<= min x (rinf S)" unfolding setle_def Ball_def mem_def by auto
- hence "isGlb UNIV ?S (min x (rinf S))" using ** isGlbI2[of UNIV ?S "min x (rinf S)"] unfolding Collect_def by auto
- ultimately show ?thesis using real_isGlb_unique[of UNIV ?S] using `S\<noteq>{}` by auto
-qed
-
-lemma inf_insert_finite: "finite S ==> rinf(insert x S) = (if S = {} then x else min x (rinf S))"
- by (rule rinf_insert, rule finite_imp_bounded, simp)
-
subsection{* Compactness (the definition is the one based on convegent subsequences). *}
definition
@@ -4120,30 +4092,35 @@
shows "\<exists>x \<in> s. \<forall>y \<in> s. y \<le> x"
proof-
from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
- { fix e::real assume as: "\<forall>x\<in>s. x \<le> rsup s" "rsup s \<notin> s" "0 < e" "\<forall>x'\<in>s. x' = rsup s \<or> \<not> rsup s - x' < e"
- have "isLub UNIV s (rsup s)" using rsup[OF assms(2)] unfolding setle_def using as(1) by auto
- moreover have "isUb UNIV s (rsup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
- ultimately have False using isLub_le_isUb[of UNIV s "rsup s" "rsup s - e"] using `e>0` by auto }
- thus ?thesis using bounded_has_rsup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rsup s"]]
- apply(rule_tac x="rsup s" in bexI) by auto
-qed
+ { fix e::real assume as: "\<forall>x\<in>s. x \<le> Sup s" "Sup s \<notin> s" "0 < e" "\<forall>x'\<in>s. x' = Sup s \<or> \<not> Sup s - x' < e"
+ have "isLub UNIV s (Sup s)" using Sup[OF assms(2)] unfolding setle_def using as(1) by auto
+ moreover have "isUb UNIV s (Sup s - e)" unfolding isUb_def unfolding setle_def using as(4,2) by auto
+ ultimately have False using isLub_le_isUb[of UNIV s "Sup s" "Sup s - e"] using `e>0` by auto }
+ thus ?thesis using bounded_has_Sup(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Sup s"]]
+ apply(rule_tac x="Sup s" in bexI) by auto
+qed
+
+lemma Inf:
+ fixes S :: "real set"
+ shows "S \<noteq> {} ==> (\<exists>b. b <=* S) ==> isGlb UNIV S (Inf S)"
+by (auto simp add: isLb_def setle_def setge_def isGlb_def greatestP_def)
lemma compact_attains_inf:
fixes s :: "real set"
assumes "compact s" "s \<noteq> {}" shows "\<exists>x \<in> s. \<forall>y \<in> s. x \<le> y"
proof-
from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto
- { fix e::real assume as: "\<forall>x\<in>s. x \<ge> rinf s" "rinf s \<notin> s" "0 < e"
- "\<forall>x'\<in>s. x' = rinf s \<or> \<not> abs (x' - rinf s) < e"
- have "isGlb UNIV s (rinf s)" using rinf[OF assms(2)] unfolding setge_def using as(1) by auto
+ { fix e::real assume as: "\<forall>x\<in>s. x \<ge> Inf s" "Inf s \<notin> s" "0 < e"
+ "\<forall>x'\<in>s. x' = Inf s \<or> \<not> abs (x' - Inf s) < e"
+ have "isGlb UNIV s (Inf s)" using Inf[OF assms(2)] unfolding setge_def using as(1) by auto
moreover
{ fix x assume "x \<in> s"
- hence *:"abs (x - rinf s) = x - rinf s" using as(1)[THEN bspec[where x=x]] by auto
- have "rinf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
- hence "isLb UNIV s (rinf s + e)" unfolding isLb_def and setge_def by auto
- ultimately have False using isGlb_le_isLb[of UNIV s "rinf s" "rinf s + e"] using `e>0` by auto }
- thus ?thesis using bounded_has_rinf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="rinf s"]]
- apply(rule_tac x="rinf s" in bexI) by auto
+ hence *:"abs (x - Inf s) = x - Inf s" using as(1)[THEN bspec[where x=x]] by auto
+ have "Inf s + e \<le> x" using as(4)[THEN bspec[where x=x]] using as(2) `x\<in>s` unfolding * by auto }
+ hence "isLb UNIV s (Inf s + e)" unfolding isLb_def and setge_def by auto
+ ultimately have False using isGlb_le_isLb[of UNIV s "Inf s" "Inf s + e"] using `e>0` by auto }
+ thus ?thesis using bounded_has_Inf(1)[OF a(1) assms(2)] using a(2)[unfolded closed_real, THEN spec[where x="Inf s"]]
+ apply(rule_tac x="Inf s" in bexI) by auto
qed
lemma continuous_attains_sup:
@@ -4413,7 +4390,7 @@
text{* We can state this in terms of diameter of a set. *}
-definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
+definition "diameter s = (if s = {} then 0::real else Sup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
(* TODO: generalize to class metric_space *)
lemma diameter_bounded:
@@ -4427,12 +4404,22 @@
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) }
note * = this
{ fix x y assume "x\<in>s" "y\<in>s" hence "s \<noteq> {}" by auto
- have lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] using `s\<noteq>{}` unfolding setle_def by auto
+ have lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] using `s\<noteq>{}` unfolding setle_def
+ apply auto (*FIXME: something horrible has happened here!*)
+ apply atomize
+ apply safe
+ apply metis +
+ done
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 }
moreover
{ fix d::real assume "d>0" "d < diameter s"
hence "s\<noteq>{}" unfolding diameter_def by auto
- hence lub:"isLub UNIV ?D (rsup ?D)" using * rsup[of ?D] unfolding setle_def by auto
+ hence lub:"isLub UNIV ?D (Sup ?D)" using * Sup[of ?D] unfolding setle_def
+ apply auto (*FIXME: something horrible has happened here!*)
+ apply atomize
+ apply safe
+ apply metis +
+ done
have "\<exists>d' \<in> ?D. d' > d"
proof(rule ccontr)
assume "\<not> (\<exists>d'\<in>{norm (x - y) |x y. x \<in> s \<and> y \<in> s}. d < d')"
@@ -4448,6 +4435,7 @@
lemma diameter_bounded_bound:
"bounded s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s ==> norm(x - y) \<le> diameter s"
using diameter_bounded by blast
+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
lemma diameter_compact_attained:
fixes s :: "'a::real_normed_vector set"
@@ -4456,8 +4444,8 @@
proof-
have b:"bounded s" using assms(1) by (rule compact_imp_bounded)
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
- 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)"]
- unfolding setle_def and diameter_def by auto
+ hence "diameter s \<le> norm (x - y)"
+ by (force simp add: diameter_def intro!: Sup_least)
thus ?thesis using diameter_bounded(1)[OF b, THEN bspec[where x=x], THEN bspec[where x=y], OF xys] and xys by auto
qed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SupInf.thy Tue Oct 27 12:59:57 2009 +0000
@@ -0,0 +1,467 @@
+(* Author: Amine Chaieb and L C Paulson, University of Cambridge *)
+
+header {*Sup and Inf Operators on Sets of Reals.*}
+
+theory SupInf
+imports RComplete
+begin
+
+lemma minus_max_eq_min:
+ fixes x :: "'a::{lordered_ab_group_add, linorder}"
+ shows "- (max x y) = min (-x) (-y)"
+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)
+
+lemma minus_min_eq_max:
+ fixes x :: "'a::{lordered_ab_group_add, linorder}"
+ shows "- (min x y) = max (-x) (-y)"
+by (metis minus_max_eq_min minus_minus)
+
+lemma minus_Max_eq_Min [simp]:
+ fixes S :: "'a::{lordered_ab_group_add, linorder} set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Max S) = Min (uminus ` S)"
+proof (induct S rule: finite_ne_induct)
+ case (singleton x)
+ thus ?case by simp
+next
+ case (insert x S)
+ thus ?case by (simp add: minus_max_eq_min)
+qed
+
+lemma minus_Min_eq_Max [simp]:
+ fixes S :: "'a::{lordered_ab_group_add, linorder} set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> - (Min S) = Max (uminus ` S)"
+proof (induct S rule: finite_ne_induct)
+ case (singleton x)
+ thus ?case by simp
+next
+ case (insert x S)
+ thus ?case by (simp add: minus_min_eq_max)
+qed
+
+instantiation real :: Sup
+begin
+definition
+ Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
+
+instance ..
+end
+
+instantiation real :: Inf
+begin
+definition
+ Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
+
+instance ..
+end
+
+subsection{*Supremum of a set of reals*}
+
+lemma Sup_upper [intro]: (*REAL_SUP_UBOUND in HOL4*)
+ fixes x :: real
+ assumes x: "x \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "x \<le> Sup X"
+proof (auto simp add: Sup_real_def)
+ from reals_complete2
+ obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+ by (blast intro: x z)
+ hence "x \<le> s"
+ by (blast intro: x z)
+ also with s have "... = (LEAST z. \<forall>x\<in>X. x \<le> z)"
+ by (fast intro: Least_equality [symmetric])
+ finally show "x \<le> (LEAST z. \<forall>x\<in>X. x \<le> z)" .
+qed
+
+lemma Sup_least [intro]: (*REAL_IMP_SUP_LE in HOL4*)
+ fixes z :: real
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup X \<le> z"
+proof (auto simp add: Sup_real_def)
+ from reals_complete2 x
+ obtain s where s: "(\<forall>y\<in>X. y \<le> s) & (\<forall>z. ((\<forall>y\<in>X. y \<le> z) --> s \<le> z))"
+ by (blast intro: z)
+ hence "(LEAST z. \<forall>x\<in>X. x \<le> z) = s"
+ by (best intro: Least_equality)
+ also with s z have "... \<le> z"
+ by blast
+ finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
+qed
+
+lemma Sup_singleton [simp]: "Sup {x::real} = x"
+ by (force intro: Least_equality simp add: Sup_real_def)
+
+lemma Sup_eq_maximum: (*REAL_SUP_MAX in HOL4*)
+ fixes z :: real
+ assumes X: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup X = z"
+ by (force intro: Least_equality X z simp add: Sup_real_def)
+
+lemma Sup_upper2: (*REAL_IMP_LE_SUP in HOL4*)
+ fixes x :: real
+ shows "x \<in> X \<Longrightarrow> y \<le> x \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> y \<le> Sup X"
+ by (metis Sup_upper real_le_trans)
+
+lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
+ fixes z :: real
+ shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
+ by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
+
+lemma Sup_eq:
+ fixes a :: real
+ shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a)
+ \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
+ by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
+ insert_not_empty real_le_anti_sym)
+
+lemma Sup_le:
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> S *<= b \<Longrightarrow> Sup S \<le> b"
+by (metis SupInf.Sup_least setle_def)
+
+lemma Sup_upper_EX:
+ fixes x :: real
+ shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> x \<le> z \<Longrightarrow> x \<le> Sup X"
+ by blast
+
+lemma Sup_insert_nonempty:
+ fixes x :: real
+ assumes x: "x \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup (insert a X) = max a (Sup X)"
+proof (cases "Sup X \<le> a")
+ case True
+ thus ?thesis
+ apply (simp add: max_def)
+ apply (rule Sup_eq_maximum)
+ apply (metis insertCI)
+ apply (metis Sup_upper insertE le_iff_sup real_le_linear real_le_trans sup_absorb1 z)
+ done
+next
+ case False
+ hence 1:"a < Sup X" by simp
+ have "Sup X \<le> Sup (insert a X)"
+ apply (rule Sup_least)
+ apply (metis empty_psubset_nonempty psubset_eq x)
+ apply (rule Sup_upper_EX)
+ apply blast
+ apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+ done
+ moreover
+ have "Sup (insert a X) \<le> Sup X"
+ apply (rule Sup_least)
+ apply blast
+ apply (metis False Sup_upper insertE real_le_linear z)
+ done
+ ultimately have "Sup (insert a X) = Sup X"
+ by (blast intro: antisym )
+ thus ?thesis
+ by (metis 1 min_max.le_iff_sup real_less_def)
+qed
+
+lemma Sup_insert_if:
+ fixes X :: "real set"
+ assumes z: "!!x. x \<in> X \<Longrightarrow> x \<le> z"
+ shows "Sup (insert a X) = (if X={} then a else max a (Sup X))"
+by auto (metis Sup_insert_nonempty z)
+
+lemma Sup:
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> (\<exists>b. S *<= b) \<Longrightarrow> isLub UNIV S (Sup S)"
+by (auto simp add: isLub_def setle_def leastP_def isUb_def intro!: setgeI)
+
+lemma Sup_finite_Max:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "Sup S = Max S"
+using fS Se
+proof-
+ let ?m = "Max S"
+ from Max_ge[OF fS] have Sm: "\<forall> x\<in> S. x \<le> ?m" by metis
+ with Sup[OF Se] have lub: "isLub UNIV S (Sup S)" by (metis setle_def)
+ from Max_in[OF fS Se] lub have mrS: "?m \<le> Sup S"
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ moreover
+ have "Sup S \<le> ?m" using Sm lub
+ by (auto simp add: isLub_def leastP_def isUb_def setle_def setge_def)
+ ultimately show ?thesis by arith
+qed
+
+lemma Sup_finite_in:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "Sup S \<in> S"
+ using Sup_finite_Max[OF fS Se] Max_in[OF fS Se] by metis
+
+lemma Sup_finite_ge_iff:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "a \<le> Sup S \<longleftrightarrow> (\<exists> x \<in> S. a \<le> x)"
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS linorder_not_le less_le_trans)
+
+lemma Sup_finite_le_iff:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "a \<ge> Sup S \<longleftrightarrow> (\<forall> x \<in> S. a \<ge> x)"
+by (metis Max_ge Se Sup_finite_Max Sup_finite_in fS le_iff_sup real_le_trans)
+
+lemma Sup_finite_gt_iff:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "a < Sup S \<longleftrightarrow> (\<exists> x \<in> S. a < x)"
+by (metis Se Sup_finite_le_iff fS linorder_not_less)
+
+lemma Sup_finite_lt_iff:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "a > Sup S \<longleftrightarrow> (\<forall> x \<in> S. a > x)"
+by (metis Se Sup_finite_ge_iff fS linorder_not_less)
+
+lemma Sup_unique:
+ fixes S :: "real set"
+ shows "S *<= b \<Longrightarrow> (\<forall>b' < b. \<exists>x \<in> S. b' < x) \<Longrightarrow> Sup S = b"
+unfolding setle_def
+apply (rule Sup_eq, auto)
+apply (metis linorder_not_less)
+done
+
+lemma Sup_abs_le:
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
+by (auto simp add: abs_le_interval_iff) (metis Sup_upper2)
+
+lemma Sup_bounds:
+ fixes S :: "real set"
+ assumes Se: "S \<noteq> {}" and l: "a <=* S" and u: "S *<= b"
+ shows "a \<le> Sup S \<and> Sup S \<le> b"
+proof-
+ from Sup[OF Se] u have lub: "isLub UNIV S (Sup S)" by blast
+ hence b: "Sup S \<le> b" using u
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ from Se obtain y where y: "y \<in> S" by blast
+ from lub l have "a \<le> Sup S"
+ by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def)
+ (metis le_iff_sup le_sup_iff y)
+ with b show ?thesis by blast
+qed
+
+lemma Sup_asclose:
+ fixes S :: "real set"
+ assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Sup S - l\<bar> \<le> e"
+proof-
+ have th: "\<And>(x::real) l e. \<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" by arith
+ thus ?thesis using S b Sup_bounds[of S "l - e" "l+e"] unfolding th
+ by (auto simp add: setge_def setle_def)
+qed
+
+
+subsection{*Infimum of a set of reals*}
+
+lemma Inf_lower [intro]:
+ fixes z :: real
+ assumes x: "x \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf X \<le> x"
+proof -
+ have "-x \<le> Sup (uminus ` X)"
+ by (rule Sup_upper [where z = "-z"]) (auto simp add: image_iff x z)
+ thus ?thesis
+ by (auto simp add: Inf_real_def)
+qed
+
+lemma Inf_greatest [intro]:
+ fixes z :: real
+ assumes x: "X \<noteq> {}"
+ and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "z \<le> Inf X"
+proof -
+ have "Sup (uminus ` X) \<le> -z" using x z by (force intro: Sup_least)
+ hence "z \<le> - Sup (uminus ` X)"
+ by simp
+ thus ?thesis
+ by (auto simp add: Inf_real_def)
+qed
+
+lemma Inf_singleton [simp]: "Inf {x::real} = x"
+ by (simp add: Inf_real_def)
+
+lemma Inf_eq_minimum: (*REAL_INF_MIN in HOL4*)
+ fixes z :: real
+ assumes x: "z \<in> X" and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf X = z"
+proof -
+ have "Sup (uminus ` X) = -z" using x z
+ by (force intro: Sup_eq_maximum x z)
+ thus ?thesis
+ by (simp add: Inf_real_def)
+qed
+
+lemma Inf_lower2:
+ fixes x :: real
+ shows "x \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> Inf X \<le> y"
+ by (metis Inf_lower real_le_trans)
+
+lemma Inf_real_iff:
+ fixes z :: real
+ shows "X \<noteq> {} \<Longrightarrow> (!!x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> (\<exists>x\<in>X. x<y) \<longleftrightarrow> Inf X < y"
+ by (metis Inf_greatest Inf_lower less_le_not_le real_le_linear
+ order_less_le_trans)
+
+lemma Inf_eq:
+ fixes a :: real
+ 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"
+ by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
+ insert_absorb insert_not_empty real_le_anti_sym)
+
+lemma Inf_ge:
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> b <=* S \<Longrightarrow> Inf S \<ge> b"
+by (metis SupInf.Inf_greatest setge_def)
+
+lemma Inf_lower_EX:
+ fixes x :: real
+ shows "x \<in> X \<Longrightarrow> \<exists>z. \<forall>x. x \<in> X \<longrightarrow> z \<le> x \<Longrightarrow> Inf X \<le> x"
+ by blast
+
+lemma Inf_insert_nonempty:
+ fixes x :: real
+ assumes x: "x \<in> X"
+ and z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf (insert a X) = min a (Inf X)"
+proof (cases "a \<le> Inf X")
+ case True
+ thus ?thesis
+ by (simp add: min_def)
+ (blast intro: Inf_eq_minimum Inf_lower real_le_refl real_le_trans z)
+next
+ case False
+ hence 1:"Inf X < a" by simp
+ have "Inf (insert a X) \<le> Inf X"
+ apply (rule Inf_greatest)
+ apply (metis empty_psubset_nonempty psubset_eq x)
+ apply (rule Inf_lower_EX)
+ apply (blast intro: elim:)
+ apply (metis insert_iff real_le_linear real_le_refl real_le_trans z)
+ done
+ moreover
+ have "Inf X \<le> Inf (insert a X)"
+ apply (rule Inf_greatest)
+ apply blast
+ apply (metis False Inf_lower insertE real_le_linear z)
+ done
+ ultimately have "Inf (insert a X) = Inf X"
+ by (blast intro: antisym )
+ thus ?thesis
+ by (metis False min_max.inf_absorb2 real_le_linear)
+qed
+
+lemma Inf_insert_if:
+ fixes X :: "real set"
+ assumes z: "!!x. x \<in> X \<Longrightarrow> z \<le> x"
+ shows "Inf (insert a X) = (if X={} then a else min a (Inf X))"
+by auto (metis Inf_insert_nonempty z)
+
+text{*We could prove the analogous result for the supremum, and also generalise it to the union operator.*}
+lemma Inf_binary:
+ "Inf{a, b::real} = min a b"
+ by (subst Inf_insert_nonempty, auto)
+
+lemma Inf_greater:
+ fixes z :: real
+ shows "X \<noteq> {} \<Longrightarrow> Inf X < z \<Longrightarrow> \<exists>x \<in> X. x < z"
+ by (metis Inf_real_iff mem_def not_leE)
+
+lemma Inf_close:
+ fixes e :: real
+ shows "X \<noteq> {} \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>x \<in> X. x < Inf X + e"
+ by (metis add_strict_increasing comm_monoid_add.mult_commute Inf_greater linorder_not_le pos_add_strict)
+
+lemma Inf_finite_Min:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> Inf S = Min S"
+by (simp add: Inf_real_def Sup_finite_Max image_image)
+
+lemma Inf_finite_in:
+ fixes S :: "real set"
+ assumes fS: "finite S" and Se: "S \<noteq> {}"
+ shows "Inf S \<in> S"
+ using Inf_finite_Min[OF fS Se] Min_in[OF fS Se] by metis
+
+lemma Inf_finite_ge_iff:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<le> Inf S \<longleftrightarrow> (\<forall> x \<in> S. a \<le> x)"
+by (metis Inf_finite_Min Inf_finite_in Min_le real_le_trans)
+
+lemma Inf_finite_le_iff:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
+by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
+ real_le_anti_sym real_le_linear)
+
+lemma Inf_finite_gt_iff:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a < Inf S \<longleftrightarrow> (\<forall> x \<in> S. a < x)"
+by (metis Inf_finite_le_iff linorder_not_less)
+
+lemma Inf_finite_lt_iff:
+ fixes S :: "real set"
+ shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a > Inf S \<longleftrightarrow> (\<exists> x \<in> S. a > x)"
+by (metis Inf_finite_ge_iff linorder_not_less)
+
+lemma Inf_unique:
+ fixes S :: "real set"
+ shows "b <=* S \<Longrightarrow> (\<forall>b' > b. \<exists>x \<in> S. b' > x) \<Longrightarrow> Inf S = b"
+unfolding setge_def
+apply (rule Inf_eq, auto)
+apply (metis less_le_not_le linorder_not_less)
+done
+
+lemma Inf_abs_ge:
+ fixes S :: "real set"
+ shows "S \<noteq> {} \<Longrightarrow> (\<forall>x\<in>S. \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Inf S\<bar> \<le> a"
+by (simp add: Inf_real_def) (rule Sup_abs_le, auto)
+
+lemma Inf_asclose:
+ fixes S :: "real set"
+ assumes S:"S \<noteq> {}" and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e" shows "\<bar>Inf S - l\<bar> \<le> e"
+proof -
+ have "\<bar>- Sup (uminus ` S) - l\<bar> = \<bar>Sup (uminus ` S) - (-l)\<bar>"
+ by auto
+ also have "... \<le> e"
+ apply (rule Sup_asclose)
+ apply (auto simp add: S)
+ apply (metis abs_minus_add_cancel b comm_monoid_add.mult_commute real_diff_def)
+ done
+ finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
+ thus ?thesis
+ by (simp add: Inf_real_def)
+qed
+
+subsection{*Relate max and min to sup and inf.*}
+
+lemma real_max_Sup:
+ fixes x :: real
+ shows "max x y = Sup {x,y}"
+proof-
+ have f: "finite {x, y}" "{x,y} \<noteq> {}" by simp_all
+ from Sup_finite_le_iff[OF f, of "max x y"] have "Sup {x,y} \<le> max x y" by simp
+ moreover
+ have "max x y \<le> Sup {x,y}" using Sup_finite_ge_iff[OF f, of "max x y"]
+ by (simp add: linorder_linear)
+ ultimately show ?thesis by arith
+qed
+
+lemma real_min_Inf:
+ fixes x :: real
+ shows "min x y = Inf {x,y}"
+proof-
+ have f: "finite {x, y}" "{x,y} \<noteq> {}" by simp_all
+ from Inf_finite_le_iff[OF f, of "min x y"] have "Inf {x,y} \<le> min x y"
+ by (simp add: linorder_linear)
+ moreover
+ have "min x y \<le> Inf {x,y}" using Inf_finite_ge_iff[OF f, of "min x y"]
+ by simp
+ ultimately show ?thesis by arith
+qed
+
+end