src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 50087 635d73673b5e parent 49962 a8cc904a6820 child 50094 84ddcf5364b4
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 15 14:04:23 2012 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Nov 15 10:49:58 2012 +0100
1.3 @@ -7,9 +7,210 @@
1.4  header {* Elementary topology in Euclidean space. *}
1.6  theory Topology_Euclidean_Space
1.7 -imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
1.8 +imports
1.9 +  SEQ
1.10 +  "~~/src/HOL/Library/Diagonal_Subsequence"
1.11 +  "~~/src/HOL/Library/Countable"
1.12 +  Linear_Algebra
1.13 +  "~~/src/HOL/Library/Glbs"
1.14 +  Norm_Arith
1.15 +begin
1.16 +
1.17 +subsection {* Topological Basis *}
1.18 +
1.19 +context topological_space
1.20 +begin
1.21 +
1.22 +definition "topological_basis B =
1.23 +  ((\<forall>b\<in>B. open b) \<and> (\<forall>x. open x \<longrightarrow> (\<exists>B'. B' \<subseteq> B \<and> Union B' = x)))"
1.24 +
1.25 +lemma topological_basis_iff:
1.26 +  assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
1.27 +  shows "topological_basis B \<longleftrightarrow> (\<forall>O'. open O' \<longrightarrow> (\<forall>x\<in>O'. \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'))"
1.28 +    (is "_ \<longleftrightarrow> ?rhs")
1.29 +proof safe
1.30 +  fix O' and x::'a
1.31 +  assume H: "topological_basis B" "open O'" "x \<in> O'"
1.32 +  hence "(\<exists>B'\<subseteq>B. \<Union>B' = O')" by (simp add: topological_basis_def)
1.33 +  then obtain B' where "B' \<subseteq> B" "O' = \<Union>B'" by auto
1.34 +  thus "\<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'" using H by auto
1.35 +next
1.36 +  assume H: ?rhs
1.37 +  show "topological_basis B" using assms unfolding topological_basis_def
1.38 +  proof safe
1.39 +    fix O'::"'a set" assume "open O'"
1.40 +    with H obtain f where "\<forall>x\<in>O'. f x \<in> B \<and> x \<in> f x \<and> f x \<subseteq> O'"
1.41 +      by (force intro: bchoice simp: Bex_def)
1.42 +    thus "\<exists>B'\<subseteq>B. \<Union>B' = O'"
1.43 +      by (auto intro: exI[where x="{f x |x. x \<in> O'}"])
1.44 +  qed
1.45 +qed
1.46 +
1.47 +lemma topological_basisI:
1.48 +  assumes "\<And>B'. B' \<in> B \<Longrightarrow> open B'"
1.49 +  assumes "\<And>O' x. open O' \<Longrightarrow> x \<in> O' \<Longrightarrow> \<exists>B'\<in>B. x \<in> B' \<and> B' \<subseteq> O'"
1.50 +  shows "topological_basis B"
1.51 +  using assms by (subst topological_basis_iff) auto
1.52 +
1.53 +lemma topological_basisE:
1.54 +  fixes O'
1.55 +  assumes "topological_basis B"
1.56 +  assumes "open O'"
1.57 +  assumes "x \<in> O'"
1.58 +  obtains B' where "B' \<in> B" "x \<in> B'" "B' \<subseteq> O'"
1.59 +proof atomize_elim
1.60 +  from assms have "\<And>B'. B'\<in>B \<Longrightarrow> open B'" by (simp add: topological_basis_def)
1.61 +  with topological_basis_iff assms
1.62 +  show  "\<exists>B'. B' \<in> B \<and> x \<in> B' \<and> B' \<subseteq> O'" using assms by (simp add: Bex_def)
1.63 +qed
1.64 +
1.65 +end
1.66 +
1.67 +subsection {* Enumerable Basis *}
1.68 +
1.69 +class enumerable_basis = topological_space +
1.70 +  assumes ex_enum_basis: "\<exists>f::nat \<Rightarrow> 'a set. topological_basis (range f)"
1.71  begin
1.73 +definition enum_basis'::"nat \<Rightarrow> 'a set"
1.74 +  where "enum_basis' = Eps (topological_basis o range)"
1.75 +
1.76 +lemma enumerable_basis': "topological_basis (range enum_basis')"
1.77 +  using ex_enum_basis
1.78 +  unfolding enum_basis'_def o_def
1.79 +  by (rule someI_ex)
1.80 +
1.81 +lemmas enumerable_basisE' = topological_basisE[OF enumerable_basis']
1.82 +
1.83 +text {* Extend enumeration of basis, such that it is closed under (finite) Union *}
1.84 +
1.85 +definition enum_basis::"nat \<Rightarrow> 'a set"
1.86 +  where "enum_basis n = \<Union>(set (map enum_basis' (from_nat n)))"
1.87 +
1.88 +lemma
1.89 +  open_enum_basis:
1.90 +  assumes "B \<in> range enum_basis"
1.91 +  shows "open B"
1.92 +  using assms enumerable_basis'
1.93 +  by (force simp add: topological_basis_def enum_basis_def)
1.94 +
1.95 +lemma enumerable_basis: "topological_basis (range enum_basis)"
1.96 +proof (rule topological_basisI[OF open_enum_basis])
1.97 +  fix O' x assume "open O'" "x \<in> O'"
1.98 +  from topological_basisE[OF enumerable_basis' this] guess B' . note B' = this
1.99 +  moreover then obtain n where "B' = enum_basis' n" by auto
1.100 +  moreover hence "B' = enum_basis (to_nat [n])" by (auto simp: enum_basis_def)
1.101 +  ultimately show "\<exists>B'\<in>range enum_basis. x \<in> B' \<and> B' \<subseteq> O'" by blast
1.102 +qed
1.104 +lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
1.106 +lemma open_enumerable_basis_ex:
1.107 +  assumes "open X"
1.108 +  shows "\<exists>N. X = (\<Union>n\<in>N. enum_basis n)"
1.109 +proof -
1.110 +  from enumerable_basis assms obtain B' where "B' \<subseteq> range enum_basis" "X = Union B'"
1.111 +    unfolding topological_basis_def by blast
1.112 +  hence "Union B' = (\<Union>n\<in>{n. enum_basis n \<in> B'}. enum_basis n)" by auto
1.113 +  with `X = Union B'` show ?thesis by blast
1.114 +qed
1.116 +lemma open_enumerable_basisE:
1.117 +  assumes "open X"
1.118 +  obtains N where "X = (\<Union>n\<in>N. enum_basis n)"
1.119 +  using assms open_enumerable_basis_ex by (atomize_elim) simp
1.121 +lemma countable_dense_set:
1.122 +  shows "\<exists>x::nat \<Rightarrow> _. \<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
1.123 +proof -
1.124 +  def x \<equiv> "\<lambda>n. (SOME x::'a. x \<in> enum_basis n)"
1.125 +  have x: "\<And>n. enum_basis n \<noteq> ({}::'a set) \<Longrightarrow> x n \<in> enum_basis n" unfolding x_def
1.126 +    by (rule someI_ex) auto
1.127 +  have "\<forall>y. open y \<longrightarrow> y \<noteq> {} \<longrightarrow> (\<exists>n. x n \<in> y)"
1.128 +  proof (intro allI impI)
1.129 +    fix y::"'a set" assume "open y" "y \<noteq> {}"
1.130 +    from open_enumerable_basisE[OF `open y`] guess N . note N = this
1.131 +    obtain n where n: "n \<in> N" "enum_basis n \<noteq> ({}::'a set)"
1.132 +    proof (atomize_elim, rule ccontr, clarsimp)
1.133 +      assume "\<forall>n. n \<in> N \<longrightarrow> enum_basis n = ({}::'a set)"
1.134 +      hence "(\<Union>n\<in>N. enum_basis n) = (\<Union>n\<in>N. {}::'a set)"
1.135 +        by (intro UN_cong) auto
1.136 +      hence "y = {}" unfolding N by simp
1.137 +      with `y \<noteq> {}` show False by auto
1.138 +    qed
1.139 +    with x N n have "x n \<in> y" by auto
1.140 +    thus "\<exists>n. x n \<in> y" ..
1.141 +  qed
1.142 +  thus ?thesis by blast
1.143 +qed
1.145 +lemma countable_dense_setE:
1.146 +  obtains x :: "nat \<Rightarrow> _"
1.147 +  where "\<And>y. open y \<Longrightarrow> y \<noteq> {} \<Longrightarrow> \<exists>n. x n \<in> y"
1.148 +  using countable_dense_set by blast
1.150 +text {* Construction of an Increasing Sequence Approximating Open Sets *}
1.152 +lemma empty_basisI[intro]: "{} \<in> range enum_basis"
1.153 +proof
1.154 +  show "{} = enum_basis (to_nat ([]::nat list))" by (simp add: enum_basis_def)
1.155 +qed rule
1.157 +lemma union_basisI[intro]:
1.158 +  assumes "A \<in> range enum_basis" "B \<in> range enum_basis"
1.159 +  shows "A \<union> B \<in> range enum_basis"
1.160 +proof -
1.161 +  from assms obtain a b where "A \<union> B = enum_basis a \<union> enum_basis b" by auto
1.162 +  also have "\<dots> = enum_basis (to_nat (from_nat a @ from_nat b::nat list))"
1.163 +    by (simp add: enum_basis_def)
1.164 +  finally show ?thesis by simp
1.165 +qed
1.167 +lemma open_imp_Union_of_incseq:
1.168 +  assumes "open X"
1.169 +  shows "\<exists>S. incseq S \<and> (\<Union>j. S j) = X \<and> range S \<subseteq> range enum_basis"
1.170 +proof -
1.171 +  from open_enumerable_basis_ex[OF `open X`] obtain N where N: "X = (\<Union>n\<in>N. enum_basis n)" by auto
1.172 +  hence X: "X = (\<Union>n. if n \<in> N then enum_basis n else {})" by (auto split: split_if_asm)
1.173 +  def S \<equiv> "nat_rec (if 0 \<in> N then enum_basis 0 else {})
1.174 +    (\<lambda>n S. if (Suc n) \<in> N then S \<union> enum_basis (Suc n) else S)"
1.175 +  have S_simps[simp]:
1.176 +    "S 0 = (if 0 \<in> N then enum_basis 0 else {})"
1.177 +    "\<And>n. S (Suc n) = (if (Suc n) \<in> N then S n \<union> enum_basis (Suc n) else S n)"
1.178 +    by (simp_all add: S_def)
1.179 +  have "incseq S" by (rule incseq_SucI) auto
1.180 +  moreover
1.181 +  have "(\<Union>j. S j) = X" unfolding N
1.182 +  proof safe
1.183 +    fix x n assume "n \<in> N" "x \<in> enum_basis n"
1.184 +    hence "x \<in> S n" by (cases n) auto
1.185 +    thus "x \<in> (\<Union>j. S j)" by auto
1.186 +  next
1.187 +    fix x j
1.188 +    assume "x \<in> S j"
1.189 +    thus "x \<in> UNION N enum_basis" by (induct j) (auto split: split_if_asm)
1.190 +  qed
1.191 +  moreover have "range S \<subseteq> range enum_basis"
1.192 +  proof safe
1.193 +    fix j show "S j \<in> range enum_basis" by (induct j) auto
1.194 +  qed
1.195 +  ultimately show ?thesis by auto
1.196 +qed
1.198 +lemma open_incseqE:
1.199 +  assumes "open X"
1.200 +  obtains S where "incseq S" "(\<Union>j. S j) = X" "range S \<subseteq> range enum_basis"
1.201 +  using open_imp_Union_of_incseq assms by atomize_elim
1.203 +end
1.205 +subsection {* Polish spaces *}
1.207 +text {* Textbooks define Polish spaces as completely metrizable.
1.208 +  We assume the topology to be complete for a given metric. *}
1.210 +class polish_space = complete_space + enumerable_basis
1.212  subsection {* General notion of a topology as a value *}
1.214  definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"
1.215 @@ -377,6 +578,86 @@
1.217  lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
1.219 +lemma rational_boxes:
1.220 +  fixes x :: "'a\<Colon>ordered_euclidean_space"
1.221 +  assumes "0 < e"
1.222 +  shows "\<exists>a b. (\<forall>i. a \$\$ i \<in> \<rat>) \<and> (\<forall>i. b \$\$ i \<in> \<rat>) \<and> x \<in> {a <..< b} \<and> {a <..< b} \<subseteq> ball x e"
1.223 +proof -
1.224 +  def e' \<equiv> "e / (2 * sqrt (real (DIM ('a))))"
1.225 +  then have e: "0 < e'" using assms by (auto intro!: divide_pos_pos)
1.226 +  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> y < x \$\$ i \<and> x \$\$ i - y < e'" (is "\<forall>i. ?th i")
1.227 +  proof
1.228 +    fix i from Rats_dense_in_real[of "x \$\$ i - e'" "x \$\$ i"] e
1.229 +    show "?th i" by auto
1.230 +  qed
1.231 +  from choice[OF this] guess a .. note a = this
1.232 +  have "\<forall>i. \<exists>y. y \<in> \<rat> \<and> x \$\$ i < y \<and> y - x \$\$ i < e'" (is "\<forall>i. ?th i")
1.233 +  proof
1.234 +    fix i from Rats_dense_in_real[of "x \$\$ i" "x \$\$ i + e'"] e
1.235 +    show "?th i" by auto
1.236 +  qed
1.237 +  from choice[OF this] guess b .. note b = this
1.238 +  { fix y :: 'a assume *: "Chi a < y" "y < Chi b"
1.239 +    have "dist x y = sqrt (\<Sum>i<DIM('a). (dist (x \$\$ i) (y \$\$ i))\<twosuperior>)"
1.240 +      unfolding setL2_def[symmetric] by (rule euclidean_dist_l2)
1.241 +    also have "\<dots> < sqrt (\<Sum>i<DIM('a). e^2 / real (DIM('a)))"
1.242 +    proof (rule real_sqrt_less_mono, rule setsum_strict_mono)
1.243 +      fix i assume i: "i \<in> {..<DIM('a)}"
1.244 +      have "a i < y\$\$i \<and> y\$\$i < b i" using * i eucl_less[where 'a='a] by auto
1.245 +      moreover have "a i < x\$\$i" "x\$\$i - a i < e'" using a by auto
1.246 +      moreover have "x\$\$i < b i" "b i - x\$\$i < e'" using b by auto
1.247 +      ultimately have "\<bar>x\$\$i - y\$\$i\<bar> < 2 * e'" by auto
1.248 +      then have "dist (x \$\$ i) (y \$\$ i) < e/sqrt (real (DIM('a)))"
1.249 +        unfolding e'_def by (auto simp: dist_real_def)
1.250 +      then have "(dist (x \$\$ i) (y \$\$ i))\<twosuperior> < (e/sqrt (real (DIM('a))))\<twosuperior>"
1.251 +        by (rule power_strict_mono) auto
1.252 +      then show "(dist (x \$\$ i) (y \$\$ i))\<twosuperior> < e\<twosuperior> / real DIM('a)"
1.253 +        by (simp add: power_divide)
1.254 +    qed auto
1.255 +    also have "\<dots> = e" using `0 < e` by (simp add: real_eq_of_nat DIM_positive)
1.256 +    finally have "dist x y < e" . }
1.257 +  with a b show ?thesis
1.258 +    apply (rule_tac exI[of _ "Chi a"])
1.259 +    apply (rule_tac exI[of _ "Chi b"])
1.260 +    using eucl_less[where 'a='a] by auto
1.261 +qed
1.263 +lemma ex_rat_list:
1.264 +  fixes x :: "'a\<Colon>ordered_euclidean_space"
1.265 +  assumes "\<And> i. x \$\$ i \<in> \<rat>"
1.266 +  shows "\<exists> r. length r = DIM('a) \<and> (\<forall> i < DIM('a). of_rat (r ! i) = x \$\$ i)"
1.267 +proof -
1.268 +  have "\<forall>i. \<exists>r. x \$\$ i = of_rat r" using assms unfolding Rats_def by blast
1.269 +  from choice[OF this] guess r ..
1.270 +  then show ?thesis by (auto intro!: exI[of _ "map r [0 ..< DIM('a)]"])
1.271 +qed
1.273 +lemma open_UNION:
1.274 +  fixes M :: "'a\<Colon>ordered_euclidean_space set"
1.275 +  assumes "open M"
1.276 +  shows "M = UNION {(a, b) | a b. {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)} \<subseteq> M}
1.277 +                   (\<lambda> (a, b). {Chi (of_rat \<circ> op ! a) <..< Chi (of_rat \<circ> op ! b)})"
1.278 +    (is "M = UNION ?idx ?box")
1.279 +proof safe
1.280 +  fix x assume "x \<in> M"
1.281 +  obtain e where e: "e > 0" "ball x e \<subseteq> M"
1.282 +    using openE[OF assms `x \<in> M`] by auto
1.283 +  then obtain a b where ab: "x \<in> {a <..< b}" "\<And>i. a \$\$ i \<in> \<rat>" "\<And>i. b \$\$ i \<in> \<rat>" "{a <..< b} \<subseteq> ball x e"
1.284 +    using rational_boxes[OF e(1)] by blast
1.285 +  then obtain p q where pq: "length p = DIM ('a)"
1.286 +                            "length q = DIM ('a)"
1.287 +                            "\<forall> i < DIM ('a). of_rat (p ! i) = a \$\$ i \<and> of_rat (q ! i) = b \$\$ i"
1.288 +    using ex_rat_list[OF ab(2)] ex_rat_list[OF ab(3)] by blast
1.289 +  hence p: "Chi (of_rat \<circ> op ! p) = a"
1.290 +    using euclidean_eq[of "Chi (of_rat \<circ> op ! p)" a]
1.291 +    unfolding o_def by auto
1.292 +  from pq have q: "Chi (of_rat \<circ> op ! q) = b"
1.293 +    using euclidean_eq[of "Chi (of_rat \<circ> op ! q)" b]
1.294 +    unfolding o_def by auto
1.295 +  have "x \<in> ?box (p, q)"
1.296 +    using p q ab by auto
1.297 +  thus "x \<in> UNION ?idx ?box" using ab e p q exI[of _ p] exI[of _ q] by auto
1.298 +qed auto
1.300  subsection{* Connectedness *}
1.302 @@ -803,7 +1084,6 @@
1.303    using frontier_complement frontier_subset_eq[of "- S"]
1.304    unfolding open_closed by auto
1.307  subsection {* Filters and the ``eventually true'' quantifier *}
1.309  definition
1.310 @@ -1361,6 +1641,121 @@
1.311    shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
1.312    by (metis closure_closed closure_approachable)
1.314 +subsection {* Infimum Distance *}
1.316 +definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
1.318 +lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
1.319 +  by (simp add: infdist_def)
1.321 +lemma infdist_nonneg:
1.322 +  shows "0 \<le> infdist x A"
1.323 +  using assms by (auto simp add: infdist_def)
1.325 +lemma infdist_le:
1.326 +  assumes "a \<in> A"
1.327 +  assumes "d = dist x a"
1.328 +  shows "infdist x A \<le> d"
1.329 +  using assms by (auto intro!: SupInf.Inf_lower[where z=0] simp add: infdist_def)
1.331 +lemma infdist_zero[simp]:
1.332 +  assumes "a \<in> A" shows "infdist a A = 0"
1.333 +proof -
1.334 +  from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0" by auto
1.335 +  with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto
1.336 +qed
1.338 +lemma infdist_triangle:
1.339 +  shows "infdist x A \<le> infdist y A + dist x y"
1.340 +proof cases
1.341 +  assume "A = {}" thus ?thesis by (simp add: infdist_def)
1.342 +next
1.343 +  assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
1.344 +  have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
1.345 +  proof
1.346 +    from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
1.347 +    fix d assume "d \<in> {dist x y + dist y a |a. a \<in> A}"
1.348 +    then obtain a where d: "d = dist x y + dist y a" "a \<in> A" by auto
1.349 +    show "infdist x A \<le> d"
1.350 +      unfolding infdist_notempty[OF `A \<noteq> {}`]
1.351 +    proof (rule Inf_lower2)
1.352 +      show "dist x a \<in> {dist x a |a. a \<in> A}" using `a \<in> A` by auto
1.353 +      show "dist x a \<le> d" unfolding d by (rule dist_triangle)
1.354 +      fix d assume "d \<in> {dist x a |a. a \<in> A}"
1.355 +      then obtain a where "a \<in> A" "d = dist x a" by auto
1.356 +      thus "infdist x A \<le> d" by (rule infdist_le)
1.357 +    qed
1.358 +  qed
1.359 +  also have "\<dots> = dist x y + infdist y A"
1.360 +  proof (rule Inf_eq, safe)
1.361 +    fix a assume "a \<in> A"
1.362 +    thus "dist x y + infdist y A \<le> dist x y + dist y a" by (auto intro: infdist_le)
1.363 +  next
1.364 +    fix i assume inf: "\<And>d. d \<in> {dist x y + dist y a |a. a \<in> A} \<Longrightarrow> i \<le> d"
1.365 +    hence "i - dist x y \<le> infdist y A" unfolding infdist_notempty[OF `A \<noteq> {}`] using `a \<in> A`
1.366 +      by (intro Inf_greatest) (auto simp: field_simps)
1.367 +    thus "i \<le> dist x y + infdist y A" by simp
1.368 +  qed
1.369 +  finally show ?thesis by simp
1.370 +qed
1.372 +lemma
1.373 +  in_closure_iff_infdist_zero:
1.374 +  assumes "A \<noteq> {}"
1.375 +  shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
1.376 +proof
1.377 +  assume "x \<in> closure A"
1.378 +  show "infdist x A = 0"
1.379 +  proof (rule ccontr)
1.380 +    assume "infdist x A \<noteq> 0"
1.381 +    with infdist_nonneg[of x A] have "infdist x A > 0" by auto
1.382 +    hence "ball x (infdist x A) \<inter> closure A = {}" apply auto
1.383 +      by (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
1.384 +        eucl_less_not_refl euclidean_trans(2) infdist_le)
1.385 +    hence "x \<notin> closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
1.386 +    thus False using `x \<in> closure A` by simp
1.387 +  qed
1.388 +next
1.389 +  assume x: "infdist x A = 0"
1.390 +  then obtain a where "a \<in> A" by atomize_elim (metis all_not_in_conv assms)
1.391 +  show "x \<in> closure A" unfolding closure_approachable
1.392 +  proof (safe, rule ccontr)
1.393 +    fix e::real assume "0 < e"
1.394 +    assume "\<not> (\<exists>y\<in>A. dist y x < e)"
1.395 +    hence "infdist x A \<ge> e" using `a \<in> A`
1.396 +      unfolding infdist_def
1.397 +      by (force intro: Inf_greatest simp: dist_commute)
1.398 +    with x `0 < e` show False by auto
1.399 +  qed
1.400 +qed
1.402 +lemma
1.403 +  in_closed_iff_infdist_zero:
1.404 +  assumes "closed A" "A \<noteq> {}"
1.405 +  shows "x \<in> A \<longleftrightarrow> infdist x A = 0"
1.406 +proof -
1.407 +  have "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
1.408 +    by (rule in_closure_iff_infdist_zero) fact
1.409 +  with assms show ?thesis by simp
1.410 +qed
1.412 +lemma tendsto_infdist [tendsto_intros]:
1.413 +  assumes f: "(f ---> l) F"
1.414 +  shows "((\<lambda>x. infdist (f x) A) ---> infdist l A) F"
1.415 +proof (rule tendstoI)
1.416 +  fix e ::real assume "0 < e"
1.417 +  from tendstoD[OF f this]
1.418 +  show "eventually (\<lambda>x. dist (infdist (f x) A) (infdist l A) < e) F"
1.419 +  proof (eventually_elim)
1.420 +    fix x
1.421 +    from infdist_triangle[of l A "f x"] infdist_triangle[of "f x" A l]
1.422 +    have "dist (infdist (f x) A) (infdist l A) \<le> dist (f x) l"
1.423 +      by (simp add: dist_commute dist_real_def)
1.424 +    also assume "dist (f x) l < e"
1.425 +    finally show "dist (infdist (f x) A) (infdist l A) < e" .
1.426 +  qed
1.427 +qed
1.429  text{* Some other lemmas about sequences. *}
1.431  lemma sequentially_offset:
1.432 @@ -2696,6 +3091,157 @@
1.433    assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
1.434  qed
1.436 +lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
1.437 +  by metis
1.439 +lemma nat_approx_posE:
1.440 +  fixes e::real
1.441 +  assumes "0 < e"
1.442 +  obtains n::nat where "1 / (Suc n) < e"
1.443 +proof atomize_elim
1.444 +  have " 1 / real (Suc (nat (ceiling (1/e)))) < 1 / (ceiling (1/e))"
1.445 +    by (rule divide_strict_left_mono) (auto intro!: mult_pos_pos simp: `0 < e`)
1.446 +  also have "1 / (ceiling (1/e)) \<le> 1 / (1/e)"
1.447 +    by (rule divide_left_mono) (auto intro!: divide_pos_pos simp: `0 < e`)
1.448 +  also have "\<dots> = e" by simp
1.449 +  finally show  "\<exists>n. 1 / real (Suc n) < e" ..
1.450 +qed
1.452 +lemma compact_eq_totally_bounded:
1.453 +  shows "compact s \<longleftrightarrow> complete s \<and> (\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k)))"
1.454 +proof (safe intro!: compact_imp_complete)
1.455 +  fix e::real
1.456 +  def f \<equiv> "(\<lambda>x::'a. ball x e) ` UNIV"
1.457 +  assume "0 < e" "compact s"
1.458 +  hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
1.459 +    by (simp add: compact_eq_heine_borel)
1.460 +  moreover
1.461 +  have d0: "\<And>x::'a. dist x x < e" using `0 < e` by simp
1.462 +  hence "(\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f" by (auto simp: f_def intro!: d0)
1.463 +  ultimately have "(\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')" ..
1.464 +  then guess K .. note K = this
1.465 +  have "\<forall>K'\<in>K. \<exists>k. K' = ball k e" using K by (auto simp: f_def)
1.466 +  then obtain k where "\<And>K'. K' \<in> K \<Longrightarrow> K' = ball (k K') e" unfolding bchoice_iff by blast
1.467 +  thus "\<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k" using K
1.468 +    by (intro exI[where x="k ` K"]) (auto simp: f_def)
1.469 +next
1.470 +  assume assms: "complete s" "\<forall>e>0. \<exists>k. finite k \<and> s \<subseteq> \<Union>(\<lambda>x. ball x e) ` k"
1.471 +  show "compact s"
1.472 +  proof cases
1.473 +    assume "s = {}" thus "compact s" by (simp add: compact_def)
1.474 +  next
1.475 +    assume "s \<noteq> {}"
1.476 +    show ?thesis
1.477 +      unfolding compact_def
1.478 +    proof safe
1.479 +      fix f::"nat \<Rightarrow> _" assume "\<forall>n. f n \<in> s" hence f: "\<And>n. f n \<in> s" by simp
1.480 +      from assms have "\<forall>e. \<exists>k. e>0 \<longrightarrow> finite k \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))" by simp
1.481 +      then obtain K where
1.482 +        K: "\<And>e. e > 0 \<Longrightarrow> finite (K e) \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
1.483 +        unfolding choice_iff by blast
1.484 +      {
1.485 +        fix e::real and f' have f': "\<And>n::nat. (f o f') n \<in> s" using f by auto
1.486 +        assume "e > 0"
1.487 +        from K[OF this] have K: "finite (K e)" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
1.488 +          by simp_all
1.489 +        have "\<exists>k\<in>(K e). \<exists>r. subseq r \<and> (\<forall>i. (f o f' o r) i \<in> ball k e)"
1.490 +        proof (rule ccontr)
1.491 +          from K have "finite (K e)" "K e \<noteq> {}" "s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` (K e)))"
1.492 +            using `s \<noteq> {}`
1.493 +            by auto
1.494 +          moreover
1.495 +          assume "\<not> (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f \<circ> f' o r) i \<in> ball k e))"
1.496 +          hence "\<And>r k. k \<in> K e \<Longrightarrow> subseq r \<Longrightarrow> (\<exists>i. (f o f' o r) i \<notin> ball k e)" by simp
1.497 +          ultimately
1.498 +          show False using f'
1.499 +          proof (induct arbitrary: s f f' rule: finite_ne_induct)
1.500 +            case (singleton x)
1.501 +            have "\<exists>i. (f \<circ> f' o id) i \<notin> ball x e" by (rule singleton) (auto simp: subseq_def)
1.502 +            thus ?case using singleton by (auto simp: ball_def)
1.503 +          next
1.504 +            case (insert x A)
1.505 +            show ?case
1.506 +            proof cases
1.507 +              have inf_ms: "infinite ((f o f') -` s)" using insert by (simp add: vimage_def)
1.508 +              have "infinite ((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A)))"
1.509 +                using insert by (intro infinite_super[OF _ inf_ms]) auto
1.510 +              also have "((f o f') -` \<Union>((\<lambda>x. ball x e) ` (insert x A))) =
1.511 +                {m. (f o f') m \<in> ball x e} \<union> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by auto
1.512 +              finally have "infinite \<dots>" .
1.513 +              moreover assume "finite {m. (f o f') m \<in> ball x e}"
1.514 +              ultimately have inf: "infinite {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}" by blast
1.515 +              hence "A \<noteq> {}" by auto then obtain k where "k \<in> A" by auto
1.516 +              def r \<equiv> "enumerate {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
1.517 +              have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
1.518 +                using enumerate_mono[OF _ inf] by (simp add: r_def)
1.519 +              hence "subseq r" by (simp add: subseq_def)
1.520 +              have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> \<Union>((\<lambda>x. ball x e) ` A)}"
1.521 +                using enumerate_in_set[OF inf] by (simp add: r_def)
1.522 +              show False
1.523 +              proof (rule insert)
1.524 +                show "\<Union>(\<lambda>x. ball x e) ` A \<subseteq> \<Union>(\<lambda>x. ball x e) ` A" by simp
1.525 +                fix k s assume "k \<in> A" "subseq s"
1.526 +                thus "\<exists>i. (f o f' o r o s) i \<notin> ball k e" using `subseq r`
1.527 +                  by (subst (2) o_assoc[symmetric]) (intro insert(6) subseq_o, simp_all)
1.528 +              next
1.529 +                fix n show "(f \<circ> f' o r) n \<in> \<Union>(\<lambda>x. ball x e) ` A" using r_in_set by auto
1.530 +              qed
1.531 +            next
1.532 +              assume inf: "infinite {m. (f o f') m \<in> ball x e}"
1.533 +              def r \<equiv> "enumerate {m. (f o f') m \<in> ball x e}"
1.534 +              have r_mono: "\<And>n m. n < m \<Longrightarrow> r n < r m"
1.535 +                using enumerate_mono[OF _ inf] by (simp add: r_def)
1.536 +              hence "subseq r" by (simp add: subseq_def)
1.537 +              from insert(6)[OF insertI1 this] obtain i where "(f o f') (r i) \<notin> ball x e" by auto
1.538 +              moreover
1.539 +              have r_in_set: "\<And>n. r n \<in> {m. (f o f') m \<in> ball x e}"
1.540 +                using enumerate_in_set[OF inf] by (simp add: r_def)
1.541 +              hence "(f o f') (r i) \<in> ball x e" by simp
1.542 +              ultimately show False by simp
1.543 +            qed
1.544 +          qed
1.545 +        qed
1.546 +      }
1.547 +      hence ex: "\<forall>f'. \<forall>e > 0. (\<exists>k\<in>K e. \<exists>r. subseq r \<and> (\<forall>i. (f o f' \<circ> r) i \<in> ball k e))" by simp
1.548 +      let ?e = "\<lambda>n. 1 / real (Suc n)"
1.549 +      let ?P = "\<lambda>n s. \<exists>k\<in>K (?e n). (\<forall>i. (f o s) i \<in> ball k (?e n))"
1.550 +      interpret subseqs ?P using ex by unfold_locales force
1.551 +      from `complete s` have limI: "\<And>f. (\<And>n. f n \<in> s) \<Longrightarrow> Cauchy f \<Longrightarrow> (\<exists>l\<in>s. f ----> l)"
1.552 +        by (simp add: complete_def)
1.553 +      have "\<exists>l\<in>s. (f o diagseq) ----> l"
1.554 +      proof (intro limI metric_CauchyI)
1.555 +        fix e::real assume "0 < e" hence "0 < e / 2" by auto
1.556 +        from nat_approx_posE[OF this] guess n . note n = this
1.557 +        show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) n) < e"
1.558 +        proof (rule exI[where x="Suc n"], safe)
1.559 +          fix m mm assume "Suc n \<le> m" "Suc n \<le> mm"
1.560 +          let ?e = "1 / real (Suc n)"
1.561 +          from reducer_reduces[of n] obtain k where
1.562 +            "k\<in>K ?e"  "\<And>i. (f o seqseq (Suc n)) i \<in> ball k ?e"
1.563 +            unfolding seqseq_reducer by auto
1.564 +          moreover
1.565 +          note diagseq_sub[OF `Suc n \<le> m`] diagseq_sub[OF `Suc n \<le> mm`]
1.566 +          ultimately have "{(f o diagseq) m, (f o diagseq) mm} \<subseteq> ball k ?e" by auto
1.567 +          also have "\<dots> \<subseteq> ball k (e / 2)" using n by (intro subset_ball) simp
1.568 +          finally
1.569 +          have "dist k ((f \<circ> diagseq) m) + dist k ((f \<circ> diagseq) mm) < e / 2 + e /2"
1.570 +            by (intro add_strict_mono) auto
1.571 +          hence "dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k < e"
1.572 +            by (simp add: dist_commute)
1.573 +          moreover have "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) \<le>
1.574 +            dist ((f \<circ> diagseq) m) k + dist ((f \<circ> diagseq) mm) k"
1.575 +            by (rule dist_triangle2)
1.576 +          ultimately show "dist ((f \<circ> diagseq) m) ((f \<circ> diagseq) mm) < e"
1.577 +            by simp
1.578 +        qed
1.579 +      next
1.580 +        fix n show "(f o diagseq) n \<in> s" using f by simp
1.581 +      qed
1.582 +      thus "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l" using subseq_diagseq by auto
1.583 +    qed
1.584 +  qed
1.585 +qed
1.587  lemma compact_eq_bounded_closed:
1.588    fixes s :: "'a::heine_borel set"
1.589    shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
1.590 @@ -2738,9 +3284,6 @@
1.591    unfolding compact_def
1.592    by simp
1.594 -lemma subseq_o: "subseq r \<Longrightarrow> subseq s \<Longrightarrow> subseq (r \<circ> s)"
1.595 -  unfolding subseq_def by simp (* TODO: move somewhere else *)
1.597  lemma compact_union [intro]:
1.598    assumes "compact s" and "compact t"
1.599    shows "compact (s \<union> t)"
1.600 @@ -2771,6 +3314,13 @@
1.601    qed
1.602  qed
1.604 +lemma compact_Union [intro]: "finite S \<Longrightarrow> (\<And>T. T \<in> S \<Longrightarrow> compact T) \<Longrightarrow> compact (\<Union>S)"
1.605 +  by (induct set: finite) auto
1.607 +lemma compact_UN [intro]:
1.608 +  "finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
1.609 +  unfolding SUP_def by (rule compact_Union) auto
1.611  lemma compact_inter_closed [intro]:
1.612    assumes "compact s" and "closed t"
1.613    shows "compact (s \<inter> t)"
1.614 @@ -3294,6 +3844,11 @@
1.615    shows "continuous F (\<lambda>x. dist (f x) (g x))"
1.616    using assms unfolding continuous_def by (rule tendsto_dist)
1.618 +lemma continuous_infdist:
1.619 +  assumes "continuous F f"
1.620 +  shows "continuous F (\<lambda>x. infdist (f x) A)"
1.621 +  using assms unfolding continuous_def by (rule tendsto_infdist)
1.623  lemma continuous_norm:
1.624    shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. norm (f x))"
1.625    unfolding continuous_def by (rule tendsto_norm)
1.626 @@ -4886,6 +5441,39 @@
1.627    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
1.628  qed
1.630 +instance ordered_euclidean_space \<subseteq> enumerable_basis
1.631 +proof
1.632 +  def to_cube \<equiv> "\<lambda>(a, b). {Chi (real_of_rat \<circ> op ! a)<..<Chi (real_of_rat \<circ> op ! b)}::'a set"
1.633 +  def enum \<equiv> "\<lambda>n. (to_cube (from_nat n)::'a set)"
1.634 +  have "Ball (range enum) open" unfolding enum_def
1.635 +  proof safe
1.636 +    fix n show "open (to_cube (from_nat n))"
1.637 +      by (cases "from_nat n::rat list \<times> rat list")
1.638 +         (simp add: open_interval to_cube_def)
1.639 +  qed
1.640 +  moreover have "(\<forall>x. open x \<longrightarrow> (\<exists>B'\<subseteq>range enum. \<Union>B' = x))"
1.641 +  proof safe
1.642 +    fix x::"'a set" assume "open x"
1.643 +    def lists \<equiv> "{(a, b) |a b. to_cube (a, b) \<subseteq> x}"
1.644 +    from open_UNION[OF `open x`]
1.645 +    have "\<Union>(to_cube ` lists) = x" unfolding lists_def to_cube_def
1.646 +     by simp
1.647 +    moreover have "to_cube ` lists \<subseteq> range enum"
1.648 +    proof
1.649 +      fix x assume "x \<in> to_cube ` lists"
1.650 +      then obtain l where "l \<in> lists" "x = to_cube l" by auto
1.651 +      hence "x = enum (to_nat l)" by (simp add: to_cube_def enum_def)
1.652 +      thus "x \<in> range enum" by simp
1.653 +    qed
1.654 +    ultimately
1.655 +    show "\<exists>B'\<subseteq>range enum. \<Union>B' = x" by blast
1.656 +  qed
1.657 +  ultimately
1.658 +  show "\<exists>f::nat\<Rightarrow>'a set. topological_basis (range f)" unfolding topological_basis_def by blast
1.659 +qed
1.661 +instance ordered_euclidean_space \<subseteq> polish_space ..
1.663  text {* Intervals in general, including infinite and mixtures of open and closed. *}
1.665  definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>