--- 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 \<inter> T = T" )
apply auto
apply (frule closedin_closed_Int[of T S])
- by simp
+ apply simp
+ done
lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> 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 \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
@@ -709,7 +711,8 @@
lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 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 \<le> 0 ==> ball x e = {}" by simp
@@ -770,17 +773,21 @@
defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^isub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
-proof safe
- fix x assume "x \<in> M"
- obtain e where e: "e > 0" "ball x e \<subseteq> M"
- using openE[OF `open M` `x \<in> M`] by auto
- moreover then obtain a b where ab: "x \<in> box a b"
- "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" "box a b \<subseteq> ball x e"
- using rational_boxes[OF e(1)] by metis
- ultimately show "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))"
- by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
- (auto simp: euclidean_representation I_def a'_def b'_def)
-qed (auto simp: I_def)
+proof -
+ {
+ fix x assume "x \<in> M"
+ obtain e where e: "e > 0" "ball x e \<subseteq> M"
+ using openE[OF `open M` `x \<in> M`] by auto
+ moreover then obtain a b where ab: "x \<in> box a b"
+ "\<forall>i \<in> Basis. a \<bullet> i \<in> \<rat>" "\<forall>i\<in>Basis. b \<bullet> i \<in> \<rat>" "box a b \<subseteq> ball x e"
+ using rational_boxes[OF e(1)] by metis
+ ultimately have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))"
+ by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> 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 " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
unfolding connected_def openin_open closedin_closed
- apply (subst exists_diff) by blast
+ apply (subst exists_diff)
+ apply blast
+ done
hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
- (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis
+ (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
+ apply (simp add: closed_def)
+ apply metis
+ done
have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
(is "_ \<longleftrightarrow> \<not> (\<exists>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]: "\<not> x islimpt {}"
unfolding islimpt_def by auto
@@ -1199,15 +1212,13 @@
subsection {* Filters and the ``eventually true'' quantifier *}
-definition
- indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
- (infixr "indirection" 70) where
- "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
+definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
+ (infixr "indirection" 70)
+ where "a indirection v = at a within {b. \<exists>c\<ge>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) \<longleftrightarrow> \<not> a islimpt S"
+lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
proof
assume "trivial_limit (at a within S)"
thus "\<not> a islimpt S"
@@ -1335,7 +1346,7 @@
lemma eventually_within_interior:
assumes "x \<in> interior S"
shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
-proof-
+proof -
from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
{ assume "?lhs"
then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> 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 "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
shows "dist a l <= e"
-proof-
+proof -
have "dist a l \<in> {..e}"
proof (rule Lim_in_closed_set)
show "closed {..e}" by simp
@@ -1495,7 +1507,7 @@
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
shows "norm(l) <= e"
-proof-
+proof -
have "norm l \<in> {..e}"
proof (rule Lim_in_closed_set)
show "closed {..e}" by simp
@@ -1510,7 +1522,7 @@
fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
assumes "\<not> (trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. e <= norm(f x)) net"
shows "e \<le> norm l"
-proof-
+proof -
have "norm l \<in> {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 "((\<lambda>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 \<Rightarrow> 'a" where
- "netlimit F \<equiv> Lim F (\<lambda>x. x)"
+abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a"
+ where "netlimit F \<equiv> Lim F (\<lambda>x. x)"
lemma netlimit_within:
"\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
@@ -1565,7 +1577,7 @@
fixes x :: "'a::{t2_space,perfect_space}"
assumes "x \<in> 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\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
- and fl: "(f ---> l) (at a)"
+ assumes ab: "a\<noteq>b"
+ and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> 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 \<in> 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 \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> 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 \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>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 \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
shows "Inf S \<in> closure S"
- unfolding closure_approachable
-proof safe
+proof -
have *: "\<forall>x\<in>S. Inf S \<le> 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 \<in> S" "x < Inf S + e"
- by (subst (asm) cInf_less_iff[of _ B]) auto
- with * show "\<exists>x\<in>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 \<in> S" "x < Inf S + e"
+ by (subst (asm) cInf_less_iff[of _ B]) auto
+ with * have "\<exists>x\<in>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 \<in> A})"
@@ -1755,29 +1774,30 @@
lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
by (simp add: infdist_def)
-lemma infdist_nonneg:
- shows "0 \<le> infdist x A"
- using assms by (auto simp add: infdist_def intro: cInf_greatest)
+lemma infdist_nonneg: "0 \<le> infdist x A"
+ by (auto simp add: infdist_def intro: cInf_greatest)
lemma infdist_le:
assumes "a \<in> A"
- assumes "d = dist x a"
+ and "d = dist x a"
shows "infdist x A \<le> d"
using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
lemma infdist_zero[simp]:
- assumes "a \<in> A" shows "infdist a A = 0"
+ assumes "a \<in> A"
+ shows "infdist a A = 0"
proof -
from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 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 \<le> infdist y A + dist x y"
+lemma infdist_triangle: "infdist x A \<le> 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 \<noteq> {}" then obtain a where "a \<in> A" by auto
+ assume "A \<noteq> {}"
+ then obtain a where "a \<in> A" by auto
have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
proof (rule cInf_greatest)
from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
@@ -1815,10 +1835,13 @@
proof (rule ccontr)
assume "infdist x A \<noteq> 0"
with infdist_nonneg[of x A] have "infdist x A > 0" by auto
- hence "ball x (infdist x A) \<inter> closure A = {}" apply auto
- by (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
+ hence "ball x (infdist x A) \<inter> closure A = {}"
+ apply auto
+ apply (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
eucl_less_not_refl euclidean_trans(2) infdist_le)
- hence "x \<notin> closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
+ done
+ hence "x \<notin> closure A"
+ by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
thus False using `x \<in> closure A` by simp
qed
next
@@ -1880,7 +1903,8 @@
apply (simp only: eventually_sequentially)
apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
apply metis
- by arith
+ apply arith
+ done
lemma seq_offset_rev:
"((\<lambda>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 \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. cball x e \<subseteq> S)"
-proof-
- { fix x and e::real assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
+proof -
+ {
+ fix x and e::real
+ assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
hence "\<exists>d>0. cball x d \<subseteq> S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
- } moreover
- { fix x and e::real assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
- hence "\<exists>d>0. ball x d \<subseteq> 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\<in>S" "e>0" "cball x e \<subseteq> S"
+ hence "\<exists>d>0. ball x d \<subseteq> 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 ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
@@ -1933,7 +1967,10 @@
}
hence "e > 0" by (metis not_less)
moreover
- have "y \<in> 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 \<in> 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 \<Longrightarrow> 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\<ge>0")
+proof (cases "e\<ge>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 \<in> cball x e"
@@ -2066,15 +2103,18 @@
hence "y \<in> 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 \<in> 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 \<noteq> y` by auto
- hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
+ hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
+ using d as(1)[unfolded subset_eq] by blast
have "y - x \<noteq> 0" using `x \<noteq> 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 "\<dots> = (dist y x) + d/2"using ** by (auto simp add: distrib_right dist_norm)
finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
- qed }
+ qed
+ }
hence "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> 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 = {}) \<longleftrightarrow> 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 \<Rightarrow> bool" where
- "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
+definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
+ where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
unfolding bounded_def subset_eq by auto
lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> 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 \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> 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 "\<forall>x\<in>s. abs (x::real) \<le> 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: "\<forall>y\<in>S. dist x y \<le> a" unfolding bounded_def by auto
- { fix y assume "y \<in> closure S"
+lemma bounded_closure[intro]:
+ assumes "bounded S"
+ shows "bounded (closure S)"
+proof -
+ from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a"
+ unfolding bounded_def by auto
+ {
+ fix y
+ assume "y \<in> closure S"
then obtain f where f: "\<forall>n. f n \<in> S" "(f ---> y) sequentially"
unfolding closure_sequential by auto
have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
@@ -2205,10 +2256,10 @@
done
lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
- by (induct rule: finite_induct[of F], auto)
+ by (induct rule: finite_induct[of F]) auto
lemma bounded_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. bounded (B x) \<Longrightarrow> bounded (\<Union>x\<in>A. B x)"
- by (induct set: finite, auto)
+ by (induct set: finite) auto
lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"
proof -
@@ -2218,12 +2269,14 @@
qed
lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
- by (induct set: finite, simp_all)
+ by (induct set: finite) simp_all
lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
apply (simp add: bounded_iff)
apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
- by metis arith
+ apply metis
+ apply arith
+ done
lemma Bseq_eq_bounded: "Bseq f \<longleftrightarrow> 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]:
"\<not> 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" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
- from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x" using bounded_linear.pos_bounded by (auto simp add: mult_ac)
- { fix x assume "x\<in>S"
+proof -
+ from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b"
+ unfolding bounded_pos by auto
+ from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x"
+ using bounded_linear.pos_bounded by (auto simp add: mult_ac)
+ {
+ fix x assume "x\<in>S"
hence "norm x \<le> b" using b by auto
- hence "norm (f x) \<le> 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) \<le> 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 ((\<lambda>x. a + x) ` S)"
+ assumes "bounded S"
+ shows "bounded ((\<lambda>x. a + x) ` S)"
proof-
- from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
- { fix x assume "x\<in>S"
- hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto
+ from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b"
+ unfolding bounded_pos by auto
+ {
+ fix x
+ assume "x\<in>S"
+ hence "norm (a + x) \<le> 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 \<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
+ apply simp
+ done
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
+ 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
thus "x \<ge> Inf S" using `x\<in>S`
by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
next
@@ -2353,24 +2423,40 @@
shows "\<exists>x \<in> s. x islimpt t"
proof(rule ccontr)
assume "\<not> (\<exists>x \<in> s. x islimpt t)"
- then obtain f where f:"\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)" unfolding islimpt_def
+ then obtain f where f:"\<forall>x\<in>s. x \<in> f x \<and> open (f x) \<and> (\<forall>y\<in>t. y \<in> f x \<longrightarrow> y = x)"
+ unfolding islimpt_def
using bchoice[of s "\<lambda> x T. x \<in> T \<and> open T \<and> (\<forall>y\<in>t. y \<in> T \<longrightarrow> y = x)"] by auto
obtain g where g:"g\<subseteq>{t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
- using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]] using f by auto
+ using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
+ using f by auto
from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa" by auto
- { fix x y assume "x\<in>t" "y\<in>t" "f x = f y"
- hence "x \<in> f x" "y \<in> f x \<longrightarrow> y = x" using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
- hence "x = y" using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>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\<in>t" "y\<in>t" "f x = f y"
+ hence "x \<in> f x" "y \<in> f x \<longrightarrow> y = x"
+ using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
+ hence "x = y"
+ using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>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\<in>t" "f x \<notin> g"
+ {
+ fix x
+ assume "x\<in>t" "f x \<notin> g"
from g(3) assms(3) `x\<in>t` obtain h where "h\<in>g" and "x\<in>h" by auto
- then obtain y where "y\<in>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\<in>t` and `x\<in>h`[unfolded `h = f y`] by auto
- hence False using `f x \<notin> g` `h\<in>g` unfolding `h = f y` by auto }
+ then obtain y where "y\<in>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\<in>t` and `x\<in>h`[unfolded `h = f y`] by auto
+ hence False
+ using `f x \<notin> g` `h\<in>g` unfolding `h = f y` by auto
+ }
hence "f ` t \<subseteq> 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 \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
- { fix n i
+ {
+ fix n i
have "infinite (A (Suc n) \<inter> range f - f`{.. i})"
using l A by auto
then have "\<exists>x. x \<in> A (Suc n) \<inter> range f - f`{.. i}"
@@ -2391,7 +2478,8 @@
then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
by (auto simp: not_le)
then have "i < s n i" "f (s n i) \<in> A (Suc n)"
- unfolding s_def by (auto intro: someI2_ex) }
+ unfolding s_def by (auto intro: someI2_ex)
+ }
note s = this
def r \<equiv> "nat_rec (s 0 0) s"
have "subseq r"
@@ -2402,9 +2490,13 @@
fix S assume "open S" "l \<in> S"
with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
moreover
- { fix i assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
- by (cases i) (simp_all add: r_def s) }
- then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
+ {
+ fix i
+ assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
+ by (cases i) (simp_all add: r_def s)
+ }
+ then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially"
+ by (auto simp: eventually_sequentially)
ultimately show "eventually (\<lambda>i. f (r i) \<in> 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 \<Longrightarrow> \<not> 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 \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> 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 "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
shows "closed s"
-proof-
- { fix x l assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
+proof -
+ {
+ fix x l
+ assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
hence "l \<in> s"
- proof(cases "\<forall>n. x n \<noteq> l")
- case False thus "l\<in>s" using as(1) by auto
+ proof (cases "\<forall>n. x n \<noteq> l")
+ case False
+ thus "l\<in>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'\<in>s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto
- thus "l\<in>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'\<in>s" "l' islimpt (range x)"
+ using assms[THEN spec[where x="range x"]] as(1) by auto
+ thus "l\<in>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" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)" using assms by auto
+ have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)"
+ using assms by auto
then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
- by (elim compactE_image)
+ by (rule compactE_image)
from `finite D` have "bounded (\<Union>x\<in>D. ball x 1)"
by (simp add: bounded_UN)
thus "bounded U" using `U \<subseteq> (\<Union>x\<in>D. ball x 1)`
@@ -2557,10 +2658,12 @@
lemma compact_union [intro]:
assumes "compact s" "compact t" shows " compact (s \<union> t)"
proof (rule compactI)
- fix f assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
+ fix f
+ assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
- moreover from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
+ moreover
+ from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
by (auto intro!: exI[of _ "s' \<union> t'"])
@@ -2596,8 +2699,7 @@
thus ?thesis by simp
qed
-lemma finite_imp_compact:
- shows "finite s \<Longrightarrow> compact s"
+lemma finite_imp_compact: "finite s \<Longrightarrow> 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: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
+ fix A
+ assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) ----> x"
using `seq_compact U` by (fastforce simp: seq_compact_def subset_eq)
show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>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 \<noteq> {}" by auto
@@ -2882,17 +2986,21 @@
assumes "compact U" shows "seq_compact U"
unfolding seq_compact_def
proof safe
- fix X :: "nat \<Rightarrow> 'a" assume "\<forall>n. X n \<in> U"
+ fix X :: "nat \<Rightarrow> 'a"
+ assume "\<forall>n. X n \<in> U"
then have "eventually (\<lambda>x. x \<in> U) (filtermap X sequentially)"
by (auto simp: eventually_filtermap)
- moreover have "filtermap X sequentially \<noteq> bot"
+ moreover
+ have "filtermap X sequentially \<noteq> bot"
by (simp add: trivial_limit_def eventually_filtermap)
- ultimately obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
+ ultimately
+ obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
using `compact U` by (auto simp: compact_filter)
from countable_basis_at_decseq[of x] guess A . note A = this
def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> X j \<in> A (Suc n)"
- { fix n i
+ {
+ fix n i
have "\<exists>a. i < a \<and> X a \<in> A (Suc n)"
proof (rule ccontr)
assume "\<not> (\<exists>a>i. X a \<in> A (Suc n))"
@@ -2907,7 +3015,8 @@
by (simp add: eventually_False)
qed
then have "i < s n i" "X (s n i) \<in> A (Suc n)"
- unfolding s_def by (auto intro: someI2_ex) }
+ unfolding s_def by (auto intro: someI2_ex)
+ }
note s = this
def r \<equiv> "nat_rec (s 0 0) s"
have "subseq r"
@@ -2915,12 +3024,18 @@
moreover
have "(\<lambda>n. X (r n)) ----> x"
proof (rule topological_tendstoI)
- fix S assume "open S" "x \<in> S"
+ fix S
+ assume "open S" "x \<in> S"
with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
moreover
- { fix i assume "Suc 0 \<le> i" then have "X (r i) \<in> A i"
- by (cases i) (simp_all add: r_def s) }
- then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
+ {
+ fix i
+ assume "Suc 0 \<le> i"
+ then have "X (r i) \<in> A i"
+ by (cases i) (simp_all add: r_def s)
+ }
+ then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially"
+ by (auto simp: eventually_sequentially)
ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
by eventually_elim auto
qed
@@ -2975,7 +3090,9 @@
assumes "\<forall>t. infinite t \<and> countable t \<and> t \<subseteq> s --> (\<exists>x\<in>s. \<forall>U. x\<in>U \<and> open U \<longrightarrow> infinite (U \<inter> t))"
shows "seq_compact s"
proof -
- { fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+ {
+ fix f :: "nat \<Rightarrow> 'a"
+ assume f: "\<forall>n. f n \<in> s"
have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
proof (cases "finite (range f)")
case True
@@ -3031,37 +3148,59 @@
lemma cauchy_def:
"Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
-unfolding Cauchy_def by metis
-
-fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
+ unfolding Cauchy_def by metis
+
+fun helper_1 :: "('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
"helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (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 "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
-proof(rule, rule, rule ccontr)
- fix e::real assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
+proof (rule, rule, rule ccontr)
+ fix e::real
+ assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
def x \<equiv> "helper_1 s e"
- { fix n
+ {
+ fix n
have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
- proof(induct_tac rule:nat_less_induct)
- fix n def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
- assume as:"\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
- have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)" using assm apply simp apply(erule_tac x="x ` {0 ..< n}" in allE) using as by auto
- then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)" unfolding subset_eq by auto
- have "Q (x n)" unfolding x_def and helper_1.simps[of s e n]
- apply(rule someI2[where a=z]) unfolding x_def[symmetric] and Q_def using z by auto
- thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto
- qed }
- hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
- then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially" using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
- from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
- then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> r) n) < e" unfolding cauchy_def using `e>0` by auto
+ proof (induct n rule: nat_less_induct)
+ fix n
+ def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
+ assume as: "\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
+ have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
+ using assm
+ apply simp
+ apply (erule_tac x="x ` {0 ..< n}" in allE)
+ using as
+ apply auto
+ done
+ then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
+ unfolding subset_eq by auto
+ have "Q (x n)"
+ unfolding x_def and helper_1.simps[of s e n]
+ apply (rule someI2[where a=z])
+ unfolding x_def[symmetric] and Q_def
+ using z
+ apply auto
+ done
+ thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
+ unfolding Q_def by auto
+ qed
+ }
+ hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)"
+ by blast+
+ then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
+ using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
+ from this(3) have "Cauchy (x \<circ> r)"
+ using LIMSEQ_imp_Cauchy by auto
+ then obtain N::nat where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist ((x \<circ> r) m) ((x \<circ> 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 \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> 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 \<longleftrightarrow> bounded s \<and> 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 "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
proof safe
- fix d :: "'a set" assume d: "d \<subseteq> Basis"
+ fix d :: "'a set"
+ assume d: "d \<subseteq> Basis"
with finite_Basis have "finite d" by (blast intro: finite_subset)
from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
- (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
- proof(induct d) case empty thus ?case unfolding subseq_def by auto
- next case (insert k d) have k[intro]:"k\<in>Basis" using insert by auto
+ (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+ proof (induct d)
+ case empty
+ thus ?case unfolding subseq_def by auto
+ next
+ case (insert k d)
+ have k[intro]:"k\<in>Basis" using insert by auto
have s': "bounded ((\<lambda>x. x \<bullet> 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 \<equiv> "(\<Sum>i\<in>Basis. (if i = k then l2 else l1\<bullet>i) *\<^sub>R i)::'a"
- { fix e::real assume "e>0"
- from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially" by blast
- from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially" by (rule tendstoD)
+ {
+ fix e::real
+ assume "e>0"
+ from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
+ by blast
+ from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially"
+ by (rule tendstoD)
from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
by (rule eventually_subseq)
have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
@@ -3226,47 +3381,58 @@
then obtain l::'a and r where r: "subseq r"
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> 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 (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))) sequentially"
by simp
moreover
- { fix n assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
+ {
+ fix n
+ assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> 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 "\<dots> < (\<Sum>i\<in>(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 (\<lambda>n. dist (f (r n)) l < e) sequentially"
by (rule eventually_elim1)
}
- hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
- with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
+ hence *: "((f \<circ> r) ---> l) sequentially"
+ unfolding o_def tendsto_iff by simp
+ with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
+ by auto
qed
lemma bounded_fst: "bounded s \<Longrightarrow> 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 \<Longrightarrow> 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 \<Rightarrow> bool" where
- "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
-
-lemma compact_imp_complete: assumes "compact s" shows "complete s"
-proof-
- { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
+definition complete :: "'a::metric_space set \<Rightarrow> bool"
+ where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
+
+lemma compact_imp_complete:
+ assumes "compact s"
+ shows "complete s"
+proof -
+ {
+ fix f
+ assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> 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:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> 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:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
- { fix n::nat assume n:"n \<ge> max N M"
+ {
+ fix e::real
+ assume "e>0"
+ from as(2) obtain N where N:"\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> 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:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
+ {
+ fix n::nat
+ assume n:"n \<ge> max N M"
have "dist ((f \<circ> r) n) l < e/2" using n M by auto
moreover have "r n \<ge> N" using lr'[of n] n by auto
hence "dist (f n) ((f \<circ> 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 "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast }
- hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>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 "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
+ }
+ hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>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 "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
+ from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1"
+ unfolding cauchy_def
+ apply (erule_tac x= 1 in allE)
+ apply auto
+ done
hence N:"\<forall>n. N \<le> n \<longrightarrow> 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:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> 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:"\<forall>n::nat. f n \<in> s" "Cauchy f"
- then obtain l where "(f ---> l) sequentially" using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
- hence "\<exists>l\<in>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:"\<forall>n::nat. f n \<in> s" "Cauchy f"
+ then obtain l where "(f ---> l) sequentially"
+ using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
+ hence "\<exists>l\<in>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 "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
- "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)" "bounded(s 0)"
+ "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)" "bounded(s 0)"
shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
-proof-
- from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n" using choice[of "\<lambda>n x. x\<in> 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:"\<forall>n::nat. x n \<in> s n"
+ using choice[of "\<lambda>n x. x\<in> 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\<in>s 0" "subseq r" "((x \<circ> 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:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto
+ with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e"
+ unfolding LIMSEQ_def by auto
hence "dist ((x \<circ> r) (max N n)) l < e" by auto
moreover
have "r (max N n) \<ge> n" using lr(2) using seq_suble[of r "max N n"] by auto
hence "(x \<circ> r) (max N n) \<in> 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 "\<exists>y\<in>s n. dist y l < e" by auto
}
hence "l \<in> s n" using closed_approachable[of "s n" l] assms(1) by blast