# HG changeset patch # User wenzelm # Date 1373643798 -7200 # Node ID 8a7b59a81088450cdd5794fcff0d1230ca6b4ef0 # Parent fee0db8cf60dbe9a886dacbcc86988d30e1faa2f tuned proofs; diff -r fee0db8cf60d -r 8a7b59a81088 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jul 12 16:19:43 2013 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Jul 12 17:43:18 2013 +0200 @@ -585,7 +585,8 @@ apply (subgoal_tac "S \ T = T" ) apply auto apply (frule closedin_closed_Int[of T S]) - by simp + apply simp + done lemma closed_subset: "S \ T \ closed S \ closedin (subtopology euclidean T) S" by (auto simp add: closedin_closed) @@ -693,7 +694,8 @@ apply atomize apply (erule_tac x="y" in allE) apply (erule_tac x="xa" in allE) - by arith + apply arith + done lemma open_contains_ball: "open S \ (\x\S. \e>0. ball x e \ S)" unfolding open_dist subset_eq mem_ball Ball_def dist_commute .. @@ -709,7 +711,8 @@ lemma ball_eq_empty[simp]: "ball x e = {} \ e \ 0" unfolding mem_ball set_eq_iff apply (simp add: not_less) - by (metis zero_le_dist order_trans dist_self) + apply (metis zero_le_dist order_trans dist_self) + done lemma ball_empty[intro]: "e \ 0 ==> ball x e = {}" by simp @@ -770,17 +773,21 @@ defines "b' \ \f :: 'a \ real \ real. (\(i::'a)\Basis. snd (f i) *\<^sub>R i)" defines "I \ {f\Basis \\<^isub>E \ \ \. box (a' f) (b' f) \ M}" shows "M = (\f\I. box (a' f) (b' f))" -proof safe - fix x assume "x \ M" - obtain e where e: "e > 0" "ball x e \ M" - using openE[OF `open M` `x \ M`] by auto - moreover then obtain a b where ab: "x \ box a b" - "\i \ Basis. a \ i \ \" "\i\Basis. b \ i \ \" "box a b \ ball x e" - using rational_boxes[OF e(1)] by metis - ultimately show "x \ (\f\I. box (a' f) (b' f))" - by (intro UN_I[of "\i\Basis. (a \ i, b \ i)"]) - (auto simp: euclidean_representation I_def a'_def b'_def) -qed (auto simp: I_def) +proof - + { + fix x assume "x \ M" + obtain e where e: "e > 0" "ball x e \ M" + using openE[OF `open M` `x \ M`] by auto + moreover then obtain a b where ab: "x \ box a b" + "\i \ Basis. a \ i \ \" "\i\Basis. b \ i \ \" "box a b \ ball x e" + using rational_boxes[OF e(1)] by metis + ultimately have "x \ (\f\I. box (a' f) (b' f))" + by (intro UN_I[of "\i\Basis. (a \ i, b \ i)"]) + (auto simp: euclidean_representation I_def a'_def b'_def) + } + then show ?thesis by (auto simp: I_def) +qed + subsection{* Connectedness *} @@ -812,9 +819,14 @@ proof- have " \ connected S \ (\e1 e2. open e1 \ open (- e2) \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})" unfolding connected_def openin_open closedin_closed - apply (subst exists_diff) by blast + apply (subst exists_diff) + apply blast + done hence th0: "connected S \ \ (\e2 e1. closed e2 \ open e1 \ S \ e1 \ (- e2) \ e1 \ (- e2) \ S = {} \ e1 \ S \ {} \ (- e2) \ S \ {})" - (is " _ \ \ (\e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis + (is " _ \ \ (\e2 e1. ?P e2 e1)") + apply (simp add: closed_def) + apply metis + done have th1: "?rhs \ \ (\t' t. closed t'\t = S\t' \ t\{} \ t\S \ (\t'. open t' \ t = S \ t'))" (is "_ \ \ (\t' t. ?Q t' t)") @@ -827,8 +839,8 @@ then show ?thesis unfolding th0 th1 by simp qed -lemma connected_empty[simp, intro]: "connected {}" - by (simp add: connected_def) +lemma connected_empty[simp, intro]: "connected {}" (* FIXME duplicate? *) + by simp subsection{* Limit points *} @@ -887,7 +899,8 @@ unfolding closed_def apply (subst open_subopen) apply (simp add: islimpt_def subset_eq) - by (metis ComplE ComplI) + apply (metis ComplE ComplI) + done lemma islimpt_EMPTY[simp]: "\ x islimpt {}" unfolding islimpt_def by auto @@ -1199,15 +1212,13 @@ subsection {* Filters and the ``eventually true'' quantifier *} -definition - indirection :: "'a::real_normed_vector \ 'a \ 'a filter" - (infixr "indirection" 70) where - "a indirection v = at a within {b. \c\0. b - a = scaleR c v}" +definition indirection :: "'a::real_normed_vector \ 'a \ 'a filter" + (infixr "indirection" 70) + where "a indirection v = at a within {b. \c\0. b - a = scaleR c v}" text {* Identify Trivial limits, where we can't approach arbitrarily closely. *} -lemma trivial_limit_within: - shows "trivial_limit (at a within S) \ \ a islimpt S" +lemma trivial_limit_within: "trivial_limit (at a within S) \ \ a islimpt S" proof assume "trivial_limit (at a within S)" thus "\ a islimpt S" @@ -1335,7 +1346,7 @@ lemma eventually_within_interior: assumes "x \ interior S" shows "eventually P (at x within S) \ eventually P (at x)" (is "?lhs = ?rhs") -proof- +proof - from assms obtain T where T: "open T" "x \ T" "T \ S" .. { assume "?lhs" then obtain A where "open A" "x \ A" "\y\A. y \ x \ y \ S \ P y" @@ -1345,11 +1356,12 @@ by auto then have "?rhs" unfolding eventually_at_topological by auto - } moreover + } + moreover { assume "?rhs" hence "?lhs" by (auto elim: eventually_elim1 simp: eventually_at_filter) - } ultimately - show "?thesis" .. + } + ultimately show "?thesis" .. qed lemma at_within_interior: @@ -1480,7 +1492,7 @@ lemma Lim_dist_ubound: assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. dist a (f x) <= e) net" shows "dist a l <= e" -proof- +proof - have "dist a l \ {..e}" proof (rule Lim_in_closed_set) show "closed {..e}" by simp @@ -1495,7 +1507,7 @@ fixes f :: "'a \ 'b::real_normed_vector" assumes "\(trivial_limit net)" "(f ---> l) net" "eventually (\x. norm(f x) <= e) net" shows "norm(l) <= e" -proof- +proof - have "norm l \ {..e}" proof (rule Lim_in_closed_set) show "closed {..e}" by simp @@ -1510,7 +1522,7 @@ fixes f :: "'a \ 'b::real_normed_vector" assumes "\ (trivial_limit net)" "(f ---> l) net" "eventually (\x. e <= norm(f x)) net" shows "e \ norm l" -proof- +proof - have "norm l \ {e..}" proof (rule Lim_in_closed_set) show "closed {e..}" by simp @@ -1526,8 +1538,8 @@ lemma Lim_bilinear: assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h" shows "((\x. h (f x) (g x)) ---> (h l m)) net" -using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net` -by (rule bounded_bilinear.tendsto) + using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net` + by (rule bounded_bilinear.tendsto) text{* These are special for limits out of the same vector space. *} @@ -1545,8 +1557,8 @@ text{* It's also sometimes useful to extract the limit point from the filter. *} -abbreviation netlimit :: "'a::t2_space filter \ 'a" where - "netlimit F \ Lim F (\x. x)" +abbreviation netlimit :: "'a::t2_space filter \ 'a" + where "netlimit F \ Lim F (\x. x)" lemma netlimit_within: "\ trivial_limit (at a within S) \ netlimit (at a within S) = a" @@ -1565,7 +1577,7 @@ fixes x :: "'a::{t2_space,perfect_space}" assumes "x \ interior S" shows "netlimit (at x within S) = x" -using assms by (metis at_within_interior netlimit_at) + using assms by (metis at_within_interior netlimit_at) text{* Transformation of limit. *} @@ -1619,11 +1631,11 @@ lemma Lim_transform_away_at: fixes a b :: "'a::t1_space" - assumes ab: "a\b" and fg: "\x. x \ a \ x \ b \ f x = g x" - and fl: "(f ---> l) (at a)" + assumes ab: "a\b" + and fg: "\x. x \ a \ x \ b \ f x = g x" + and fl: "(f ---> l) (at a)" shows "(g ---> l) (at a)" - using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl - by simp + using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp text{* Alternatively, within an open set. *} @@ -1665,28 +1677,32 @@ assume "?lhs" moreover { assume "l \ S" hence "?rhs" using tendsto_const[of l sequentially] by auto - } moreover + } + moreover { assume "l islimpt S" hence "?rhs" unfolding islimpt_sequential by auto - } ultimately - show "?rhs" unfolding closure_def by auto + } + ultimately show "?rhs" + unfolding closure_def by auto next assume "?rhs" - thus "?lhs" unfolding closure_def unfolding islimpt_sequential by auto + thus "?lhs" unfolding closure_def islimpt_sequential by auto qed lemma closed_sequential_limits: fixes S :: "'a::first_countable_topology set" shows "closed S \ (\x l. (\n. x n \ S) \ (x ---> l) sequentially \ l \ S)" unfolding closed_limpt - using closure_sequential [where 'a='a] closure_closed [where 'a='a] closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a] + using closure_sequential [where 'a='a] closure_closed [where 'a='a] + closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a] by metis lemma closure_approachable: fixes S :: "'a::metric_space set" shows "x \ closure S \ (\e>0. \y\S. dist y x < e)" apply (auto simp add: closure_def islimpt_approachable) - by (metis dist_self) + apply (metis dist_self) + done lemma closed_approachable: fixes S :: "'a::metric_space set" @@ -1697,17 +1713,18 @@ fixes S :: "real set" assumes "S \ {}" "\x\S. B \ x" shows "Inf S \ closure S" - unfolding closure_approachable -proof safe +proof - have *: "\x\S. Inf S \ x" using cInf_lower_EX[of _ S] assms by metis - - fix e :: real assume "0 < e" - then have "Inf S < Inf S + e" by simp - with assms obtain x where "x \ S" "x < Inf S + e" - by (subst (asm) cInf_less_iff[of _ B]) auto - with * show "\x\S. dist x (Inf S) < e" - by (intro bexI[of _ x]) (auto simp add: dist_real_def) + { + fix e :: real assume "0 < e" + then have "Inf S < Inf S + e" by simp + with assms obtain x where "x \ S" "x < Inf S + e" + by (subst (asm) cInf_less_iff[of _ B]) auto + with * have "\x\S. dist x (Inf S) < e" + by (intro bexI[of _ x]) (auto simp add: dist_real_def) + } + then show ?thesis unfolding closure_approachable by auto qed lemma closed_contains_Inf: @@ -1731,7 +1748,8 @@ then have "y : (S Int ball x e - {x})" unfolding ball_def by (simp add: dist_commute) then have "S Int ball x e - {x} ~= {}" by blast - } then have "?rhs" by auto + } + then have "?rhs" by auto } moreover { assume "?rhs" @@ -1748,6 +1766,7 @@ ultimately show ?thesis by auto qed + subsection {* Infimum Distance *} definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \ A})" @@ -1755,29 +1774,30 @@ lemma infdist_notempty: "A \ {} \ infdist x A = Inf {dist x a|a. a \ A}" by (simp add: infdist_def) -lemma infdist_nonneg: - shows "0 \ infdist x A" - using assms by (auto simp add: infdist_def intro: cInf_greatest) +lemma infdist_nonneg: "0 \ infdist x A" + by (auto simp add: infdist_def intro: cInf_greatest) lemma infdist_le: assumes "a \ A" - assumes "d = dist x a" + and "d = dist x a" shows "infdist x A \ d" using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def) lemma infdist_zero[simp]: - assumes "a \ A" shows "infdist a A = 0" + assumes "a \ A" + shows "infdist a A = 0" proof - from infdist_le[OF assms, of "dist a a"] have "infdist a A \ 0" by auto with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto qed -lemma infdist_triangle: - shows "infdist x A \ infdist y A + dist x y" +lemma infdist_triangle: "infdist x A \ infdist y A + dist x y" proof cases - assume "A = {}" thus ?thesis by (simp add: infdist_def) + assume "A = {}" + thus ?thesis by (simp add: infdist_def) next - assume "A \ {}" then obtain a where "a \ A" by auto + assume "A \ {}" + then obtain a where "a \ A" by auto have "infdist x A \ Inf {dist x y + dist y a |a. a \ A}" proof (rule cInf_greatest) from `A \ {}` show "{dist x y + dist y a |a. a \ A} \ {}" by simp @@ -1815,10 +1835,13 @@ proof (rule ccontr) assume "infdist x A \ 0" with infdist_nonneg[of x A] have "infdist x A > 0" by auto - hence "ball x (infdist x A) \ closure A = {}" apply auto - by (metis `0 < infdist x A` `x \ closure A` closure_approachable dist_commute + hence "ball x (infdist x A) \ closure A = {}" + apply auto + apply (metis `0 < infdist x A` `x \ closure A` closure_approachable dist_commute eucl_less_not_refl euclidean_trans(2) infdist_le) - hence "x \ closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal) + done + hence "x \ closure A" + by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal) thus False using `x \ closure A` by simp qed next @@ -1880,7 +1903,8 @@ apply (simp only: eventually_sequentially) apply (subgoal_tac "\N k (n::nat). N + k <= n ==> N <= n - k") apply metis - by arith + apply arith + done lemma seq_offset_rev: "((\i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially" @@ -1892,24 +1916,34 @@ subsection {* More properties of closed balls *} lemma closed_cball: "closed (cball x e)" -unfolding cball_def closed_def -unfolding Collect_neg_eq [symmetric] not_le -apply (clarsimp simp add: open_dist, rename_tac y) -apply (rule_tac x="dist x y - e" in exI, clarsimp) -apply (rename_tac x') -apply (cut_tac x=x and y=x' and z=y in dist_triangle) -apply simp -done + unfolding cball_def closed_def + unfolding Collect_neg_eq [symmetric] not_le + apply (clarsimp simp add: open_dist, rename_tac y) + apply (rule_tac x="dist x y - e" in exI, clarsimp) + apply (rename_tac x') + apply (cut_tac x=x and y=x' and z=y in dist_triangle) + apply simp + done lemma open_contains_cball: "open S \ (\x\S. \e>0. cball x e \ S)" -proof- - { fix x and e::real assume "x\S" "e>0" "ball x e \ S" +proof - + { + fix x and e::real + assume "x\S" "e>0" "ball x e \ S" hence "\d>0. cball x d \ S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto) - } moreover - { fix x and e::real assume "x\S" "e>0" "cball x e \ S" - hence "\d>0. ball x d \ S" unfolding subset_eq apply(rule_tac x="e/2" in exI) by auto - } ultimately - show ?thesis unfolding open_contains_ball by auto + } + moreover + { + fix x and e::real + assume "x\S" "e>0" "cball x e \ S" + hence "\d>0. ball x d \ S" + unfolding subset_eq + apply(rule_tac x="e/2" in exI) + apply auto + done + } + ultimately show ?thesis + unfolding open_contains_ball by auto qed lemma open_contains_cball_eq: "open S ==> (\x. x \ S \ (\e>0. cball x e \ S))" @@ -1933,7 +1967,10 @@ } hence "e > 0" by (metis not_less) moreover - have "y \ cball x e" using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] ball_subset_cball[of x e] `?lhs` unfolding closed_limpt by auto + have "y \ cball x e" + using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] + ball_subset_cball[of x e] `?lhs` + unfolding closed_limpt by auto ultimately show "?rhs" by auto next assume "?rhs" hence "e>0" by auto @@ -2027,25 +2064,25 @@ lemma closure_ball: fixes x :: "'a::real_normed_vector" shows "0 < e \ closure (ball x e) = cball x e" -apply (rule equalityI) -apply (rule closure_minimal) -apply (rule ball_subset_cball) -apply (rule closed_cball) -apply (rule subsetI, rename_tac y) -apply (simp add: le_less [where 'a=real]) -apply (erule disjE) -apply (rule subsetD [OF closure_subset], simp) -apply (simp add: closure_def) -apply clarify -apply (rule closure_ball_lemma) -apply (simp add: zero_less_dist_iff) -done + apply (rule equalityI) + apply (rule closure_minimal) + apply (rule ball_subset_cball) + apply (rule closed_cball) + apply (rule subsetI, rename_tac y) + apply (simp add: le_less [where 'a=real]) + apply (erule disjE) + apply (rule subsetD [OF closure_subset], simp) + apply (simp add: closure_def) + apply clarify + apply (rule closure_ball_lemma) + apply (simp add: zero_less_dist_iff) + done (* In a trivial vector space, this fails for e = 0. *) lemma interior_cball: fixes x :: "'a::{real_normed_vector, perfect_space}" shows "interior (cball x e) = ball x e" -proof(cases "e\0") +proof (cases "e\0") case False note cs = this from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover { fix y assume "y \ cball x e" @@ -2066,15 +2103,18 @@ hence "y \ ball x e" proof(cases "x = y") case True - hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] by (auto simp add: dist_commute) + hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] + by (auto simp add: dist_commute) thus "y \ ball x e" using `x = y ` by simp next case False have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d" unfolding dist_norm using `d>0` norm_ge_zero[of "y - x"] `x \ y` by auto - hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \ cball x e" using d as(1)[unfolded subset_eq] by blast + hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \ cball x e" + using d as(1)[unfolded subset_eq] by blast have "y - x \ 0" using `x \ y` by auto - hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[THEN sym] + hence **:"d / (2 * norm (y - x)) > 0" + unfolding zero_less_norm_iff[THEN sym] using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) x = norm (y + (d / (2 * norm (y - x))) *\<^sub>R y - (d / (2 * norm (y - x))) *\<^sub>R x - x)" @@ -2086,9 +2126,11 @@ also have "\ = (dist y x) + d/2"using ** by (auto simp add: distrib_right dist_norm) finally have "e \ dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute) thus "y \ ball x e" unfolding mem_ball using `d>0` by auto - qed } + qed + } hence "\S \ cball x e. open S \ S \ ball x e" by auto - ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto + ultimately show ?thesis + using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto qed lemma frontier_ball: @@ -2096,19 +2138,24 @@ shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}" apply (simp add: frontier_def closure_ball interior_open order_less_imp_le) apply (simp add: set_eq_iff) - by arith + apply arith + done lemma frontier_cball: fixes a :: "'a::{real_normed_vector, perfect_space}" shows "frontier(cball a e) = {x. dist a x = e}" apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le) apply (simp add: set_eq_iff) - by arith + apply arith + done lemma cball_eq_empty: "(cball x e = {}) \ e < 0" apply (simp add: set_eq_iff not_le) - by (metis zero_le_dist dist_self order_less_le_trans) -lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty) + apply (metis zero_le_dist dist_self order_less_le_trans) + done + +lemma cball_empty: "e < 0 ==> cball x e = {}" + by (simp add: cball_eq_empty) lemma cball_eq_sing: fixes x :: "'a::{metric_space,perfect_space}" @@ -2130,25 +2177,24 @@ subsection {* Boundedness *} (* FIXME: This has to be unified with BSEQ!! *) -definition (in metric_space) - bounded :: "'a set \ bool" where - "bounded S \ (\x e. \y\S. dist x y \ e)" +definition (in metric_space) bounded :: "'a set \ bool" + where "bounded S \ (\x e. \y\S. dist x y \ e)" lemma bounded_subset_cball: "bounded S \ (\e x. S \ cball x e)" unfolding bounded_def subset_eq by auto lemma bounded_any_center: "bounded S \ (\e. \y\S. dist a y \ e)" -unfolding bounded_def -apply safe -apply (rule_tac x="dist a x + e" in exI, clarify) -apply (drule (1) bspec) -apply (erule order_trans [OF dist_triangle add_left_mono]) -apply auto -done + unfolding bounded_def + apply safe + apply (rule_tac x="dist a x + e" in exI, clarify) + apply (drule (1) bspec) + apply (erule order_trans [OF dist_triangle add_left_mono]) + apply auto + done lemma bounded_iff: "bounded S \ (\a. \x\S. norm x \ a)" -unfolding bounded_any_center [where a=0] -by (simp add: dist_norm) + unfolding bounded_any_center [where a=0] + by (simp add: dist_norm) lemma bounded_realI: assumes "\x\s. abs (x::real) \ B" shows "bounded s" unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI) @@ -2163,10 +2209,15 @@ lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)" by (metis bounded_subset interior_subset) -lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)" -proof- - from assms obtain x and a where a: "\y\S. dist x y \ a" unfolding bounded_def by auto - { fix y assume "y \ closure S" +lemma bounded_closure[intro]: + assumes "bounded S" + shows "bounded (closure S)" +proof - + from assms obtain x and a where a: "\y\S. dist x y \ a" + unfolding bounded_def by auto + { + fix y + assume "y \ closure S" then obtain f where f: "\n. f n \ S" "(f ---> y) sequentially" unfolding closure_sequential by auto have "\n. f n \ S \ dist x (f n) \ a" using a by simp @@ -2205,10 +2256,10 @@ done lemma bounded_Union[intro]: "finite F \ (\S\F. bounded S) \ bounded(\F)" - by (induct rule: finite_induct[of F], auto) + by (induct rule: finite_induct[of F]) auto lemma bounded_UN [intro]: "finite A \ \x\A. bounded (B x) \ bounded (\x\A. B x)" - by (induct set: finite, auto) + by (induct set: finite) auto lemma bounded_insert [simp]: "bounded (insert x S) \ bounded S" proof - @@ -2218,12 +2269,14 @@ qed lemma finite_imp_bounded [intro]: "finite S \ bounded S" - by (induct set: finite, simp_all) + by (induct set: finite) simp_all lemma bounded_pos: "bounded S \ (\b>0. \x\ S. norm x <= b)" apply (simp add: bounded_iff) apply (subgoal_tac "\x (y::real). 0 < 1 + abs y \ (x <= y \ x <= 1 + abs y)") - by metis arith + apply metis + apply arith + done lemma Bseq_eq_bounded: "Bseq f \ bounded (range f::_::real_normed_vector set)" unfolding Bseq_def bounded_pos by auto @@ -2232,8 +2285,7 @@ by (metis Int_lower1 Int_lower2 bounded_subset) lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)" -apply (metis Diff_subset bounded_subset) -done + by (metis Diff_subset bounded_subset) lemma not_bounded_UNIV[simp, intro]: "\ bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)" @@ -2250,16 +2302,24 @@ lemma bounded_linear_image: assumes "bounded S" "bounded_linear f" shows "bounded(f ` S)" -proof- - from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto - from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac) - { fix x assume "x\S" +proof - + from assms(1) obtain b where b:"b>0" "\x\S. norm x \ b" + unfolding bounded_pos by auto + from assms(2) obtain B where B:"B>0" "\x. norm (f x) \ B * norm x" + using bounded_linear.pos_bounded by (auto simp add: mult_ac) + { + fix x assume "x\S" hence "norm x \ b" using b by auto - hence "norm (f x) \ B * b" using B(2) apply(erule_tac x=x in allE) - by (metis B(1) B(2) order_trans mult_le_cancel_left_pos) + hence "norm (f x) \ B * b" using B(2) + apply (erule_tac x=x in allE) + apply (metis B(1) B(2) order_trans mult_le_cancel_left_pos) + done } - thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI) - using b B mult_pos_pos [of b B] by (auto simp add: mult_commute) + thus ?thesis unfolding bounded_pos + apply (rule_tac x="b*B" in exI) + using b B mult_pos_pos [of b B] + apply (auto simp add: mult_commute) + done qed lemma bounded_scaling: @@ -2271,13 +2331,20 @@ lemma bounded_translation: fixes S :: "'a::real_normed_vector set" - assumes "bounded S" shows "bounded ((\x. a + x) ` S)" + assumes "bounded S" + shows "bounded ((\x. a + x) ` S)" proof- - from assms obtain b where b:"b>0" "\x\S. norm x \ b" unfolding bounded_pos by auto - { fix x assume "x\S" - hence "norm (a + x) \ b + norm a" using norm_triangle_ineq[of a x] b by auto + from assms obtain b where b:"b>0" "\x\S. norm x \ b" + unfolding bounded_pos by auto + { + fix x + assume "x\S" + hence "norm (a + x) \ b + norm a" + using norm_triangle_ineq[of a x] b by auto } - thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"] + thus ?thesis + unfolding bounded_pos + using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"] by (auto intro!: exI[of _ "b + norm a"]) qed @@ -2315,15 +2382,18 @@ 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 + apply simp + done 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 + fix x + assume "x\S" + from assms(1) obtain a where a:"\x\S. \x\ \ a" + unfolding bounded_real by auto thus "x \ Inf S" using `x\S` by (metis cInf_lower_EX abs_le_D2 minus_le_iff) next @@ -2353,24 +2423,40 @@ shows "\x \ s. x islimpt t" proof(rule ccontr) assume "\ (\x \ s. x islimpt t)" - then obtain f where f:"\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" unfolding islimpt_def + then obtain f where f:"\x\s. x \ f x \ open (f x) \ (\y\t. y \ f x \ y = x)" + unfolding islimpt_def using bchoice[of s "\ x T. x \ T \ open T \ (\y\t. y \ T \ y = x)"] by auto obtain g where g:"g\{t. \x. x \ s \ t = f x}" "finite g" "s \ \g" - using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \x. x\s \ t = f x}"]] using f by auto + using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \x. x\s \ t = f x}"]] + using f by auto from g(1,3) have g':"\x\g. \xa \ s. x = f xa" by auto - { fix x y assume "x\t" "y\t" "f x = f y" - hence "x \ f x" "y \ f x \ y = x" using f[THEN bspec[where x=x]] and `t\s` by auto - hence "x = y" using `f x = f y` and f[THEN bspec[where x=y]] and `y\t` and `t\s` by auto } - hence "inj_on f t" unfolding inj_on_def by simp - hence "infinite (f ` t)" using assms(2) using finite_imageD by auto + { + fix x y + assume "x\t" "y\t" "f x = f y" + hence "x \ f x" "y \ f x \ y = x" + using f[THEN bspec[where x=x]] and `t\s` by auto + hence "x = y" + using `f x = f y` and f[THEN bspec[where x=y]] and `y\t` and `t\s` by auto + } + hence "inj_on f t" + unfolding inj_on_def by simp + hence "infinite (f ` t)" + using assms(2) using finite_imageD by auto moreover - { fix x assume "x\t" "f x \ g" + { + fix x + assume "x\t" "f x \ g" from g(3) assms(3) `x\t` obtain h where "h\g" and "x\h" by auto - then obtain y where "y\s" "h = f y" using g'[THEN bspec[where x=h]] by auto - hence "y = x" using f[THEN bspec[where x=y]] and `x\t` and `x\h`[unfolded `h = f y`] by auto - hence False using `f x \ g` `h\g` unfolding `h = f y` by auto } + then obtain y where "y\s" "h = f y" + using g'[THEN bspec[where x=h]] by auto + hence "y = x" + using f[THEN bspec[where x=y]] and `x\t` and `x\h`[unfolded `h = f y`] by auto + hence False + using `f x \ g` `h\g` unfolding `h = f y` by auto + } hence "f ` t \ g" by auto - ultimately show False using g(2) using finite_subset by auto + ultimately show False + using g(2) using finite_subset by auto qed lemma acc_point_range_imp_convergent_subsequence: @@ -2381,7 +2467,8 @@ from countable_basis_at_decseq[of l] guess A . note A = this def s \ "\n i. SOME j. i < j \ f j \ A (Suc n)" - { fix n i + { + fix n i have "infinite (A (Suc n) \ range f - f`{.. i})" using l A by auto then have "\x. x \ A (Suc n) \ range f - f`{.. i}" @@ -2391,7 +2478,8 @@ then have "\a. i < a \ f a \ A (Suc n)" by (auto simp: not_le) then have "i < s n i" "f (s n i) \ A (Suc n)" - unfolding s_def by (auto intro: someI2_ex) } + unfolding s_def by (auto intro: someI2_ex) + } note s = this def r \ "nat_rec (s 0 0) s" have "subseq r" @@ -2402,9 +2490,13 @@ fix S assume "open S" "l \ S" with A(3) have "eventually (\i. A i \ S) sequentially" by auto moreover - { fix i assume "Suc 0 \ i" then have "f (r i) \ A i" - by (cases i) (simp_all add: r_def s) } - then have "eventually (\i. f (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) + { + fix i + assume "Suc 0 \ i" then have "f (r i) \ A i" + by (cases i) (simp_all add: r_def s) + } + then have "eventually (\i. f (r i) \ A i) sequentially" + by (auto simp: eventually_sequentially) ultimately show "eventually (\i. f (r i) \ S) sequentially" by eventually_elim auto qed @@ -2429,11 +2521,11 @@ lemma closure_insert: fixes x :: "'a::t1_space" shows "closure (insert x s) = insert x (closure s)" -apply (rule closure_unique) -apply (rule insert_mono [OF closure_subset]) -apply (rule closed_insert [OF closed_closure]) -apply (simp add: closure_minimal) -done + apply (rule closure_unique) + apply (rule insert_mono [OF closure_subset]) + apply (rule closed_insert [OF closed_closure]) + apply (simp add: closure_minimal) + done lemma islimpt_insert: fixes x :: "'a::t1_space" @@ -2466,12 +2558,12 @@ lemma islimpt_finite: fixes x :: "'a::t1_space" shows "finite s \ \ x islimpt s" -by (induct set: finite, simp_all add: islimpt_insert) + by (induct set: finite) (simp_all add: islimpt_insert) lemma islimpt_union_finite: fixes x :: "'a::t1_space" shows "finite s \ x islimpt (s \ t) \ x islimpt t" -by (simp add: islimpt_Un islimpt_finite) + by (simp add: islimpt_Un islimpt_finite) lemma islimpt_eq_acc_point: fixes l :: "'a :: t1_space" @@ -2526,26 +2618,35 @@ fixes s :: "'a::{first_countable_topology, t2_space} set" assumes "\t. infinite t \ t \ s --> (\x \ s. x islimpt t)" shows "closed s" -proof- - { fix x l assume as: "\n::nat. x n \ s" "(x ---> l) sequentially" +proof - + { + fix x l + assume as: "\n::nat. x n \ s" "(x ---> l) sequentially" hence "l \ s" - proof(cases "\n. x n \ l") - case False thus "l\s" using as(1) by auto + proof (cases "\n. x n \ l") + case False + thus "l\s" using as(1) by auto next case True note cas = this - with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto - then obtain l' where "l'\s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto - thus "l\s" using sequence_unique_limpt[of x l l'] using as cas by auto - qed } + with as(2) have "infinite (range x)" + using sequence_infinite_lemma[of x l] by auto + then obtain l' where "l'\s" "l' islimpt (range x)" + using assms[THEN spec[where x="range x"]] as(1) by auto + thus "l\s" using sequence_unique_limpt[of x l l'] + using as cas by auto + qed + } thus ?thesis unfolding closed_sequential_limits by fast qed lemma compact_imp_bounded: - assumes "compact U" shows "bounded U" + assumes "compact U" + shows "bounded U" proof - - have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)" using assms by auto + have "compact U" "\x\U. open (ball x 1)" "U \ (\x\U. ball x 1)" + using assms by auto then obtain D where D: "D \ U" "finite D" "U \ (\x\D. ball x 1)" - by (elim compactE_image) + by (rule compactE_image) from `finite D` have "bounded (\x\D. ball x 1)" by (simp add: bounded_UN) thus "bounded U" using `U \ (\x\D. ball x 1)` @@ -2557,10 +2658,12 @@ lemma compact_union [intro]: assumes "compact s" "compact t" shows " compact (s \ t)" proof (rule compactI) - fix f assume *: "Ball f open" "s \ t \ \f" + fix f + assume *: "Ball f open" "s \ t \ \f" from * `compact s` obtain s' where "s' \ f \ finite s' \ s \ \s'" unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis - moreover from * `compact t` obtain t' where "t' \ f \ finite t' \ t \ \t'" + moreover + from * `compact t` obtain t' where "t' \ f \ finite t' \ t \ \t'" unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis ultimately show "\f'\f. finite f' \ s \ t \ \f'" by (auto intro!: exI[of _ "s' \ t'"]) @@ -2596,8 +2699,7 @@ thus ?thesis by simp qed -lemma finite_imp_compact: - shows "finite s \ compact s" +lemma finite_imp_compact: "finite s \ compact s" by (induct set: finite) simp_all lemma open_delete: @@ -2841,12 +2943,14 @@ assumes "seq_compact U" shows "countably_compact U" proof (safe intro!: countably_compactI) - fix A assume A: "\a\A. open a" "U \ \A" "countable A" + fix A + assume A: "\a\A. open a" "U \ \A" "countable A" have subseq: "\X. range X \ U \ \r x. x \ U \ subseq r \ (X \ r) ----> x" using `seq_compact U` by (fastforce simp: seq_compact_def subset_eq) show "\T\A. finite T \ U \ \T" proof cases - assume "finite A" with A show ?thesis by auto + assume "finite A" + with A show ?thesis by auto next assume "infinite A" then have "A \ {}" by auto @@ -2882,17 +2986,21 @@ assumes "compact U" shows "seq_compact U" unfolding seq_compact_def proof safe - fix X :: "nat \ 'a" assume "\n. X n \ U" + fix X :: "nat \ 'a" + assume "\n. X n \ U" then have "eventually (\x. x \ U) (filtermap X sequentially)" by (auto simp: eventually_filtermap) - moreover have "filtermap X sequentially \ bot" + moreover + have "filtermap X sequentially \ bot" by (simp add: trivial_limit_def eventually_filtermap) - ultimately obtain x where "x \ U" and x: "inf (nhds x) (filtermap X sequentially) \ bot" (is "?F \ _") + ultimately + obtain x where "x \ U" and x: "inf (nhds x) (filtermap X sequentially) \ bot" (is "?F \ _") using `compact U` by (auto simp: compact_filter) from countable_basis_at_decseq[of x] guess A . note A = this def s \ "\n i. SOME j. i < j \ X j \ A (Suc n)" - { fix n i + { + fix n i have "\a. i < a \ X a \ A (Suc n)" proof (rule ccontr) assume "\ (\a>i. X a \ A (Suc n))" @@ -2907,7 +3015,8 @@ by (simp add: eventually_False) qed then have "i < s n i" "X (s n i) \ A (Suc n)" - unfolding s_def by (auto intro: someI2_ex) } + unfolding s_def by (auto intro: someI2_ex) + } note s = this def r \ "nat_rec (s 0 0) s" have "subseq r" @@ -2915,12 +3024,18 @@ moreover have "(\n. X (r n)) ----> x" proof (rule topological_tendstoI) - fix S assume "open S" "x \ S" + fix S + assume "open S" "x \ S" with A(3) have "eventually (\i. A i \ S) sequentially" by auto moreover - { fix i assume "Suc 0 \ i" then have "X (r i) \ A i" - by (cases i) (simp_all add: r_def s) } - then have "eventually (\i. X (r i) \ A i) sequentially" by (auto simp: eventually_sequentially) + { + fix i + assume "Suc 0 \ i" + then have "X (r i) \ A i" + by (cases i) (simp_all add: r_def s) + } + then have "eventually (\i. X (r i) \ A i) sequentially" + by (auto simp: eventually_sequentially) ultimately show "eventually (\i. X (r i) \ S) sequentially" by eventually_elim auto qed @@ -2975,7 +3090,9 @@ assumes "\t. infinite t \ countable t \ t \ s --> (\x\s. \U. x\U \ open U \ infinite (U \ t))" shows "seq_compact s" proof - - { fix f :: "nat \ 'a" assume f: "\n. f n \ s" + { + fix f :: "nat \ 'a" + assume f: "\n. f n \ s" have "\l\s. \r. subseq r \ ((f \ r) ---> l) sequentially" proof (cases "finite (range f)") case True @@ -3031,37 +3148,59 @@ lemma cauchy_def: "Cauchy s \ (\e>0. \N. \m n. m \ N \ n \ N --> dist(s m)(s n) < e)" -unfolding Cauchy_def by metis - -fun helper_1::"('a::metric_space set) \ real \ nat \ 'a" where + unfolding Cauchy_def by metis + +fun helper_1 :: "('a::metric_space set) \ real \ nat \ 'a" where "helper_1 s e n = (SOME y::'a. y \ s \ (\m (dist (helper_1 s e m) y < e)))" declare helper_1.simps[simp del] lemma seq_compact_imp_totally_bounded: assumes "seq_compact s" shows "\e>0. \k. finite k \ k \ s \ s \ (\((\x. ball x e) ` k))" -proof(rule, rule, rule ccontr) - fix e::real assume "e>0" and assm:"\ (\k. finite k \ k \ s \ s \ \((\x. ball x e) ` k))" +proof (rule, rule, rule ccontr) + fix e::real + assume "e>0" and assm:"\ (\k. finite k \ k \ s \ s \ \((\x. ball x e) ` k))" def x \ "helper_1 s e" - { fix n + { + fix n have "x n \ s \ (\m dist (x m) (x n) < e)" - proof(induct_tac rule:nat_less_induct) - fix n def Q \ "(\y. y \ s \ (\m dist (x m) y < e))" - assume as:"\m s \ (\ma dist (x ma) (x m) < e)" - have "\ s \ (\x\x ` {0..s" "z \ (\x\x ` {0.. s \ (\m dist (x m) (x n) < e)" unfolding Q_def by auto - qed } - hence "\n::nat. x n \ s" and x:"\n. \m < n. \ (dist (x m) (x n) < e)" by blast+ - then obtain l r where "l\s" and r:"subseq r" and "((x \ r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto - from this(3) have "Cauchy (x \ r)" using LIMSEQ_imp_Cauchy by auto - then obtain N::nat where N:"\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" unfolding cauchy_def using `e>0` by auto + proof (induct n rule: nat_less_induct) + fix n + def Q \ "(\y. y \ s \ (\m dist (x m) y < e))" + assume as: "\m s \ (\ma dist (x ma) (x m) < e)" + have "\ s \ (\x\x ` {0..s" "z \ (\x\x ` {0.. s \ (\m dist (x m) (x n) < e)" + unfolding Q_def by auto + qed + } + hence "\n::nat. x n \ s" and x:"\n. \m < n. \ (dist (x m) (x n) < e)" + by blast+ + then obtain l r where "l\s" and r:"subseq r" and "((x \ r) ---> l) sequentially" + using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto + from this(3) have "Cauchy (x \ r)" + using LIMSEQ_imp_Cauchy by auto + then obtain N::nat where N:"\m n. N \ m \ N \ n \ dist ((x \ r) m) ((x \ r) n) < e" + unfolding cauchy_def using `e>0` by auto show False using N[THEN spec[where x=N], THEN spec[where x="N+1"]] using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]] - using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto + using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] + by auto qed subsubsection{* Heine-Borel theorem *} @@ -3115,9 +3254,11 @@ fixes s :: "'a::metric_space set" shows "compact s \ (\t. infinite t \ t \ s --> (\x \ s. x islimpt t))" (is "?lhs = ?rhs") proof - assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto + assume ?lhs + thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto next - assume ?rhs thus ?lhs + assume ?rhs + thus ?lhs unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact) qed @@ -3153,11 +3294,16 @@ fixes s :: "'a::heine_borel set" shows "compact s \ bounded s \ closed s" (is "?lhs = ?rhs") proof - assume ?lhs thus ?rhs - using compact_imp_closed compact_imp_bounded by blast + assume ?lhs + thus ?rhs + using compact_imp_closed compact_imp_bounded + by blast next - assume ?rhs thus ?lhs - using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto + assume ?rhs + thus ?lhs + using bounded_closed_imp_seq_compact[of s] + unfolding compact_eq_seq_compact_metric + by auto qed (* TODO: is this lemma necessary? *) @@ -3186,12 +3332,17 @@ shows "\d\Basis. \l::'a. \ r. subseq r \ (\e>0. eventually (\n. \i\d. dist (f (r n) \ i) (l \ i) < e) sequentially)" proof safe - fix d :: "'a set" assume d: "d \ Basis" + fix d :: "'a set" + assume d: "d \ Basis" with finite_Basis have "finite d" by (blast intro: finite_subset) from this d show "\l::'a. \r. subseq r \ - (\e>0. eventually (\n. \i\d. dist (f (r n) \ i) (l \ i) < e) sequentially)" - proof(induct d) case empty thus ?case unfolding subseq_def by auto - next case (insert k d) have k[intro]:"k\Basis" using insert by auto + (\e>0. eventually (\n. \i\d. dist (f (r n) \ i) (l \ i) < e) sequentially)" + proof (induct d) + case empty + thus ?case unfolding subseq_def by auto + next + case (insert k d) + have k[intro]:"k\Basis" using insert by auto have s': "bounded ((\x. x \ k) ` range f)" using `bounded (range f)` by (auto intro!: bounded_linear_image bounded_linear_inner_left) obtain l1::"'a" and r1 where r1:"subseq r1" and @@ -3206,9 +3357,13 @@ using r1 and r2 unfolding r_def o_def subseq_def by auto moreover def l \ "(\i\Basis. (if i = k then l2 else l1\i) *\<^sub>R i)::'a" - { fix e::real assume "e>0" - from lr1 `e>0` have N1:"eventually (\n. \i\d. dist (f (r1 n) \ i) (l1 \ i) < e) sequentially" by blast - from lr2 `e>0` have N2:"eventually (\n. dist (f (r1 (r2 n)) \ k) l2 < e) sequentially" by (rule tendstoD) + { + fix e::real + assume "e>0" + from lr1 `e>0` have N1:"eventually (\n. \i\d. dist (f (r1 n) \ i) (l1 \ i) < e) sequentially" + by blast + from lr2 `e>0` have N2:"eventually (\n. dist (f (r1 (r2 n)) \ k) l2 < e) sequentially" + by (rule tendstoD) from r2 N1 have N1': "eventually (\n. \i\d. dist (f (r1 (r2 n)) \ i) (l1 \ i) < e) sequentially" by (rule eventually_subseq) have "eventually (\n. \i\(insert k d). dist (f (r n) \ i) (l \ i) < e) sequentially" @@ -3226,47 +3381,58 @@ then obtain l::'a and r where r: "subseq r" and l: "\e>0. eventually (\n. \i\Basis. dist (f (r n) \ i) (l \ i) < e) sequentially" using compact_lemma [OF f] by blast - { fix e::real assume "e>0" - hence "0 < e / real_of_nat DIM('a)" by (auto intro!: divide_pos_pos DIM_positive) + { + fix e::real + assume "e>0" + hence "0 < e / real_of_nat DIM('a)" + by (auto intro!: divide_pos_pos DIM_positive) with l have "eventually (\n. \i\Basis. dist (f (r n) \ i) (l \ i) < e / (real_of_nat DIM('a))) sequentially" by simp moreover - { fix n assume n: "\i\Basis. dist (f (r n) \ i) (l \ i) < e / (real_of_nat DIM('a))" + { + fix n + assume n: "\i\Basis. dist (f (r n) \ i) (l \ i) < e / (real_of_nat DIM('a))" have "dist (f (r n)) l \ (\i\Basis. dist (f (r n) \ i) (l \ i))" - apply(subst euclidean_dist_l2) using zero_le_dist by (rule setL2_le_setsum) + apply (subst euclidean_dist_l2) + using zero_le_dist + by (rule setL2_le_setsum) also have "\ < (\i\(Basis::'a set). e / (real_of_nat DIM('a)))" - apply(rule setsum_strict_mono) using n by auto + apply (rule setsum_strict_mono) + using n + by auto finally have "dist (f (r n)) l < e" by auto } ultimately have "eventually (\n. dist (f (r n)) l < e) sequentially" by (rule eventually_elim1) } - hence *:"((f \ r) ---> l) sequentially" unfolding o_def tendsto_iff by simp - with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" by auto + hence *: "((f \ r) ---> l) sequentially" + unfolding o_def tendsto_iff by simp + with r show "\l r. subseq r \ ((f \ r) ---> l) sequentially" + by auto qed lemma bounded_fst: "bounded s \ bounded (fst ` s)" -unfolding bounded_def -apply clarify -apply (rule_tac x="a" in exI) -apply (rule_tac x="e" in exI) -apply clarsimp -apply (drule (1) bspec) -apply (simp add: dist_Pair_Pair) -apply (erule order_trans [OF real_sqrt_sum_squares_ge1]) -done + unfolding bounded_def + apply clarify + apply (rule_tac x="a" in exI) + apply (rule_tac x="e" in exI) + apply clarsimp + apply (drule (1) bspec) + apply (simp add: dist_Pair_Pair) + apply (erule order_trans [OF real_sqrt_sum_squares_ge1]) + done lemma bounded_snd: "bounded s \ bounded (snd ` s)" -unfolding bounded_def -apply clarify -apply (rule_tac x="b" in exI) -apply (rule_tac x="e" in exI) -apply clarsimp -apply (drule (1) bspec) -apply (simp add: dist_Pair_Pair) -apply (erule order_trans [OF real_sqrt_sum_squares_ge2]) -done + unfolding bounded_def + apply clarify + apply (rule_tac x="b" in exI) + apply (rule_tac x="e" in exI) + apply clarsimp + apply (drule (1) bspec) + apply (simp add: dist_Pair_Pair) + apply (erule order_trans [OF real_sqrt_sum_squares_ge2]) + done instance prod :: (heine_borel, heine_borel) heine_borel proof @@ -3293,27 +3459,45 @@ subsubsection{* Completeness *} -definition complete :: "'a::metric_space set \ bool" where - "complete s \ (\f. (\n. f n \ s) \ Cauchy f \ (\l\s. f ----> l))" - -lemma compact_imp_complete: assumes "compact s" shows "complete s" -proof- - { fix f assume as: "(\n::nat. f n \ s)" "Cauchy f" +definition complete :: "'a::metric_space set \ bool" + where "complete s \ (\f. (\n. f n \ s) \ Cauchy f \ (\l\s. f ----> l))" + +lemma compact_imp_complete: + assumes "compact s" + shows "complete s" +proof - + { + fix f + assume as: "(\n::nat. f n \ s)" "Cauchy f" from as(1) obtain l r where lr: "l\s" "subseq r" "(f \ r) ----> l" using assms unfolding compact_def by blast note lr' = seq_suble [OF lr(2)] - { fix e::real assume "e>0" - from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" unfolding cauchy_def using `e>0` apply (erule_tac x="e/2" in allE) by auto - from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" using `e>0` by auto - { fix n::nat assume n:"n \ max N M" + { + fix e::real + assume "e>0" + from as(2) obtain N where N:"\m n. N \ m \ N \ n \ dist (f m) (f n) < e/2" + unfolding cauchy_def + using `e>0` apply (erule_tac x="e/2" in allE) + apply auto + done + from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] + obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" using `e>0` by auto + { + fix n::nat + assume n:"n \ max N M" have "dist ((f \ r) n) l < e/2" using n M by auto moreover have "r n \ N" using lr'[of n] n by auto hence "dist (f n) ((f \ r) n) < e / 2" using N using n by auto - ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) } - hence "\N. \n\N. dist (f n) l < e" by blast } - hence "\l\s. (f ---> l) sequentially" using `l\s` unfolding LIMSEQ_def by auto } + ultimately have "dist (f n) l < e" + using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute) + } + hence "\N. \n\N. dist (f n) l < e" by blast + } + hence "\l\s. (f ---> l) sequentially" using `l\s` + unfolding LIMSEQ_def by auto + } thus ?thesis unfolding complete_def by auto qed @@ -3436,16 +3620,25 @@ lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)" proof- - from assms obtain N::nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto + from assms obtain N::nat where "\m n. N \ m \ N \ n \ dist (s m) (s n) < 1" + unfolding cauchy_def + apply (erule_tac x= 1 in allE) + apply auto + done hence N:"\n. N \ n \ dist (s N) (s n) < 1" by auto moreover - have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto + have "bounded (s ` {0..N})" + using finite_imp_bounded[of "s ` {1..N}"] by auto then obtain a where a:"\x\s ` {0..N}. dist (s N) x \ a" unfolding bounded_any_center [where a="s N"] by auto ultimately show "?thesis" unfolding bounded_any_center [where a="s N"] - apply(rule_tac x="max a 1" in exI) apply auto - apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto + apply (rule_tac x="max a 1" in exI) + apply auto + apply (erule_tac x=y in allE) + apply (erule_tac x=y in ballE) + apply auto + done qed instance heine_borel < complete_space @@ -3493,9 +3686,15 @@ assume ?lhs thus ?rhs by (rule complete_imp_closed) next assume ?rhs - { fix f assume as:"\n::nat. f n \ s" "Cauchy f" - then obtain l where "(f ---> l) sequentially" using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto - hence "\l\s. (f ---> l) sequentially" using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]] using as(1) by auto } + { + fix f + assume as:"\n::nat. f n \ s" "Cauchy f" + then obtain l where "(f ---> l) sequentially" + using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto + hence "\l\s. (f ---> l) sequentially" + using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]] + using as(1) by auto + } thus ?lhs unfolding complete_def by auto qed @@ -3538,25 +3737,35 @@ lemma bounded_closed_nest: assumes "\n. closed(s n)" "\n. (s n \ {})" - "(\m n. m \ n --> s n \ s m)" "bounded(s 0)" + "(\m n. m \ n --> s n \ s m)" "bounded(s 0)" shows "\a::'a::heine_borel. \n::nat. a \ s(n)" -proof- - from assms(2) obtain x where x:"\n::nat. x n \ s n" using choice[of "\n x. x\ s n"] by auto - from assms(4,1) have *:"seq_compact (s 0)" using bounded_closed_imp_seq_compact[of "s 0"] by auto +proof - + from assms(2) obtain x where x:"\n::nat. x n \ s n" + using choice[of "\n x. x\ s n"] by auto + from assms(4,1) have *:"seq_compact (s 0)" + using bounded_closed_imp_seq_compact[of "s 0"] by auto then obtain l r where lr:"l\s 0" "subseq r" "((x \ r) ---> l) sequentially" - unfolding seq_compact_def apply(erule_tac x=x in allE) using x using assms(3) by blast + unfolding seq_compact_def + apply (erule_tac x=x in allE) + using x using assms(3) + apply blast + done { fix n::nat { fix e::real assume "e>0" - with lr(3) obtain N where N:"\m\N. dist ((x \ r) m) l < e" unfolding LIMSEQ_def by auto + with lr(3) obtain N where N:"\m\N. dist ((x \ r) m) l < e" + unfolding LIMSEQ_def by auto hence "dist ((x \ r) (max N n)) l < e" by auto moreover have "r (max N n) \ n" using lr(2) using seq_suble[of r "max N n"] by auto hence "(x \ r) (max N n) \ s n" - using x apply(erule_tac x=n in allE) - using x apply(erule_tac x="r (max N n)" in allE) - using assms(3) apply(erule_tac x=n in allE) apply(erule_tac x="r (max N n)" in allE) by auto + using x apply (erule_tac x=n in allE) + using x apply (erule_tac x="r (max N n)" in allE) + using assms(3) apply (erule_tac x=n in allE) + apply (erule_tac x="r (max N n)" in allE) + apply auto + done ultimately have "\y\s n. dist y l < e" by auto } hence "l \ s n" using closed_approachable[of "s n" l] assms(1) by blast