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.5  
     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.72  
    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.103 +
   1.104 +lemmas enumerable_basisE = topological_basisE[OF enumerable_basis]
   1.105 +
   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.115 +
   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.120 +
   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.144 +
   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.149 +
   1.150 +text {* Construction of an Increasing Sequence Approximating Open Sets *}
   1.151 +
   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.156 +
   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.166 +
   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.197 +
   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.202 +
   1.203 +end
   1.204 +
   1.205 +subsection {* Polish spaces *}
   1.206 +
   1.207 +text {* Textbooks define Polish spaces as completely metrizable.
   1.208 +  We assume the topology to be complete for a given metric. *}
   1.209 +
   1.210 +class polish_space = complete_space + enumerable_basis
   1.211 +
   1.212  subsection {* General notion of a topology as a value *}
   1.213  
   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.216  
   1.217  lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
   1.218  
   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.262 +
   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.272 +
   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.299  
   1.300  subsection{* Connectedness *}
   1.301  
   1.302 @@ -803,7 +1084,6 @@
   1.303    using frontier_complement frontier_subset_eq[of "- S"]
   1.304    unfolding open_closed by auto
   1.305  
   1.306 -
   1.307  subsection {* Filters and the ``eventually true'' quantifier *}
   1.308  
   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.313  
   1.314 +subsection {* Infimum Distance *}
   1.315 +
   1.316 +definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
   1.317 +
   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.320 +
   1.321 +lemma infdist_nonneg:
   1.322 +  shows "0 \<le> infdist x A"
   1.323 +  using assms by (auto simp add: infdist_def)
   1.324 +
   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.330 +
   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.337 +
   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.371 +
   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.401 +
   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.411 +
   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.428 +
   1.429  text{* Some other lemmas about sequences. *}
   1.430  
   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.435  
   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.438 +
   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.451 +
   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.586 +
   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.593  
   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.596 -
   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.603  
   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.606 +
   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.610 +
   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.617  
   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.622 +
   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.629  
   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.660 +
   1.661 +instance ordered_euclidean_space \<subseteq> polish_space ..
   1.662 +
   1.663  text {* Intervals in general, including infinite and mixtures of open and closed. *}
   1.664  
   1.665  definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>