# HG changeset patch # User paulson # Date 1256648397 0 # Node ID 3b7e2dbbd68458744b7f22b048cdb5e3418e23e5 # Parent 1fad3160d873412c09582184472b3229dbfd7182 New theory SupInf of the supremum and infimum operators for sets of reals. diff -r 1fad3160d873 -r 3b7e2dbbd684 NEWS --- 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; diff -r 1fad3160d873 -r 3b7e2dbbd684 src/HOL/Complex_Main.thy --- 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 diff -r 1fad3160d873 -r 3b7e2dbbd684 src/HOL/IsaMakefile --- 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 \ diff -r 1fad3160d873 -r 3b7e2dbbd684 src/HOL/Library/Convex_Euclidean_Space.thy --- 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 \ 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:"\x\s. \y\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 \ "rsup ((\x. inner a x) ` t)" + def k \ "Sup ((\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 "((\x. inner a x) ` t) *<= (inner a y - b)" apply(erule_tac x=y in ballE) apply(rule setleI) using `y\s` by auto - hence k:"isLub UNIV ((\x. inner a x) ` t) k" unfolding k_def apply(rule_tac rsup) using assms(5) by auto + hence k:"isLub UNIV ((\x. inner a x) ` t) k" unfolding k_def apply(rule_tac Sup) using assms(5) by auto fix x assume "x\t" thus "inner a x < (k + b / 2)" using `0s" - hence "k \ inner a x - b" unfolding k_def apply(rule_tac rsup_le) using assms(5) - unfolding setle_def + hence "k \ 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 \ {}" "t \ {}" "s \ t = {}" shows "\a b. a \ 0 \ (\x\s. inner a x \ b) \ (\x\t. inner a x \ b)" proof- from separating_hyperplane_set_0[OF convex_differences[OF assms(2,1)]] - obtain a where "a\0" "\x\{x - y |x y. x \ t \ y \ s}. 0 \ inner a x" using assms(3-5) by auto - hence "\x\t. \y\s. inner a y \ 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 ((\x. inner a x) ` s)" in exI) using `a\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\0" "\x\{x - y |x y. x \ t \ y \ s}. 0 \ inner a x" + using assms(3-5) by auto + hence "\x\t. \y\s. inner a y \ inner a x" + by (force simp add: inner_diff) + thus ?thesis + apply(rule_tac x=a in exI, rule_tac x="Sup ((\x. inner a x) ` s)" in exI) using `a\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 \ 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 \ real ^ 'n \ real ^ 'n" where diff -r 1fad3160d873 -r 3b7e2dbbd684 src/HOL/Library/Euclidean_Space.thy --- 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 \ real" where - "rsup S = (SOME a. isLub UNIV S a)" - -lemma rsup_alt: "rsup S = (SOME a. (\x \ S. x \ a) \ (\b. (\x \ S. x \ b) \ a \ b))" by (auto simp add: isLub_def rsup_def leastP_def isUb_def setle_def setge_def) - -lemma rsup: assumes Se: "S \ {}" and b: "\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 \ {}" and Sb: "S *<= b" shows "rsup S \ 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 \ {}" - shows "rsup S = Max S" -using fS Se -proof- - let ?m = "Max S" - from Max_ge[OF fS] have Sm: "\ x\ S. x \ ?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 \ rsup S" - by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def) - moreover - have "rsup S \ ?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 \ {}" - shows "rsup S \ 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 \ {}" - 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 \ {}" - shows "a \ rsup S \ (\ x \ S. a \ 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 \ {}" - shows "a \ rsup S \ (\ x \ S. a \ 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 \ {}" - shows "a < rsup S \ (\ x \ 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 \ {}" - shows "a > rsup S \ (\ x \ 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: "\b' < b. \x \ 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\{} \ S \ T \ (\b. T *<= b) \ rsup S \ 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 = (\x. S *<= x \ x \ 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 \ {}" and l: "a <=* S" and u: "S *<= b" - shows "a \ rsup S \ rsup S \ b" -proof- - from rsup[OF Se] u have lub: "isLub UNIV S (rsup S)" by blast - hence b: "rsup S \ b" using u by (auto simp add: isLub_def leastP_def setle_def setge_def isUb_def') - from Se obtain y where y: "y \ S" by blast - from lub l have "a \ 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 \ {} \ (\x\S. \x\ \ a) \ \rsup S\ \ 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 \ {}" and b: "\x\S. \x - l\ \ e" shows "\rsup S - l\ \ e" -proof- - have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ 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 \ real" where - "rinf S = (SOME a. isGlb UNIV S a)" - -lemma rinf_alt: "rinf S = (SOME a. (\x \ S. x \ a) \ (\b. (\x \ S. x \ b) \ a \ b))" by (auto simp add: isGlb_def rinf_def greatestP_def isLb_def setle_def setge_def) - -lemma reals_complete_Glb: assumes Se: "\x. x \ S" and lb: "\ y. isLb UNIV S y" - shows "\(t::real). isGlb UNIV S t" -proof- - let ?M = "uminus ` S" - from lb have th: "\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: "\x. x \ ?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 \ {}" and b: "\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 \ {}" and Sb: "b <=* S" shows "rinf S \ 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 \ {}" - shows "rinf S = Min S" -using fS Se -proof- - let ?m = "Min S" - from Min_le[OF fS] have Sm: "\ x\ S. x \ ?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 \ rinf S" - by (auto simp add: isGlb_def greatestP_def setle_def setge_def isLb_def) - moreover - have "rinf S \ ?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 \ {}" - shows "rinf S \ 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 \ {}" - 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 \ {}" - shows "a \ rinf S \ (\ x \ S. a \ 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 \ {}" - shows "a \ rinf S \ (\ x \ S. a \ 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 \ {}" - shows "a < rinf S \ (\ x \ 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 \ {}" - shows "a > rinf S \ (\ x \ 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: "\b' > b. \x \ 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\{} \ S \ T \ (\b. b <=* T) \ 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 = (\x. x <=* S \ x \ R)" - apply (rule ext) - by (metis isLb_def) - -lemma rinf_bounds: assumes Se: "S \ {}" and l: "a <=* S" and u: "S *<= b" - shows "a \ rinf S \ rinf S \ b" -proof- - from rinf[OF Se] l have lub: "isGlb UNIV S (rinf S)" by blast - hence b: "a \ 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 \ S" by blast - from lub u have "b \ 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 \ {} \ (\x\S. \x\ \ a) \ \rinf S\ \ 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 \ {}" and b: "\x\S. \x - l\ \ e" shows "\rinf S - l\ \ e" -proof- - have th: "\(x::real) l e. \x - l\ \ e \ l - e \ x \ x \ 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 \ real^'m::finite" @@ -2578,7 +2345,7 @@ have Se: "?S \ {}" using norm_basis by auto from linear_bounded[OF lf] have b: "\ 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 "\x. norm (f x) <= b * norm x \ 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 \ 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} \ {}" by simp_all - from rsup_finite_le_iff[OF f, of "max x y"] have "rsup {x,y} \ max x y" by simp - moreover - have "max x y \ 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} \ {}" by simp_all - from rinf_finite_le_iff[OF f, of "min x y"] have "rinf {x,y} \ min x y" - by (simp add: linorder_linear) - moreover - have "min x y \ 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\ (UNIV :: 'n set)}" +definition "infnorm (x::real^'n::finite) = Sup {abs(x$i) |i. i\ (UNIV :: 'n set)}" lemma numseg_dimindex_nonempty: "\i. i \ (UNIV :: 'n set)" by auto @@ -5065,7 +4807,7 @@ lemma infnorm_pos_le: "0 \ 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: "\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 \ 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 \ {}" by blast have th1: "\S f. f ` S = { f i| i. i \ 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) <= \a\ * 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 \ 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) diff -r 1fad3160d873 -r 3b7e2dbbd684 src/HOL/Library/Topology_Euclidean_Space.thy --- 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 \ (\a. \x\S. abs x <= a)" by (simp add: bounded_iff) -lemma bounded_has_rsup: assumes "bounded S" "S \ {}" - shows "\x\S. x <= rsup S" and "\b. (\x\S. x <= b) \ rsup S <= b" +lemma bounded_has_Sup: + fixes S :: "real set" + assumes "bounded S" "S \ {}" + shows "\x\S. x <= Sup S" and "\b. (\x\S. x <= b) \ Sup S <= b" +proof + fix x assume "x\S" + thus "x \ Sup S" + by (metis SupInf.Sup_upper abs_le_D1 assms(1) bounded_real) +next + show "\b. (\x\S. x \ b) \ Sup S \ 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 \ 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 \ {}" + shows "\x\S. x >= Inf S" and "\b. (\x\S. x >= b) \ Inf S >= b" proof fix x assume "x\S" from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto - hence *:"S *<= a" using setleI[of S a] by (metis abs_le_interval_iff mem_def) - thus "x \ rsup S" using rsup[OF `S\{}`] using assms(1)[unfolded bounded_real] using isLubD2[of UNIV S "rsup S" x] using `x\S` by auto -next - show "\b. (\x\S. x \ b) \ rsup S \ 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 \ Inf S" using `x\S` + by (metis Inf_lower_EX abs_le_D2 minus_le_iff) next - let ?S = "insert x S" - case False - hence *:"\x\S. x \ 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) \ y" unfolding isUb_def using rsup_le[OF `S\{}`] - 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\{}` by auto -qed - -lemma sup_insert_finite: "finite S \ 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 \ {}" - shows "\x\S. x >= rinf S" and "\b. (\x\S. x >= b) \ rinf S >= b" -proof - fix x assume "x\S" - from assms(1) obtain a where a:"\x\S. \x\ \ a" unfolding bounded_real by auto - hence *:"- a <=* S" using setgeI[of S "-a"] unfolding abs_le_interval_iff by auto - thus "x \ rinf S" using rinf[OF `S\{}`] using isGlbD2[of UNIV S "rinf S" x] using `x\S` by auto -next - show "\b. (\x\S. x >= b) \ rinf S \ 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 "\b. (\x\S. x >= b) \ Inf S \ 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 *:"\x\S. x \ 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) \ y" unfolding isLb_def using rinf_ge[OF `S\{}`] - 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\{}` 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 "\x \ s. \y \ s. y \ x" proof- from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto - { fix e::real assume as: "\x\s. x \ rsup s" "rsup s \ s" "0 < e" "\x'\s. x' = rsup s \ \ 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: "\x\s. x \ Sup s" "Sup s \ s" "0 < e" "\x'\s. x' = Sup s \ \ 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 \ {} ==> (\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 \ {}" shows "\x \ s. \y \ s. x \ y" proof- from assms(1) have a:"bounded s" "closed s" unfolding compact_eq_bounded_closed by auto - { fix e::real assume as: "\x\s. x \ rinf s" "rinf s \ s" "0 < e" - "\x'\