src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 52624 8a7b59a81088
parent 52141 eff000cab70f
child 52625 b74bf6c0e5a1
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 12 16:19:43 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Jul 12 17:43:18 2013 +0200
     1.3 @@ -585,7 +585,8 @@
     1.4    apply (subgoal_tac "S \<inter> T = T" )
     1.5    apply auto
     1.6    apply (frule closedin_closed_Int[of T S])
     1.7 -  by simp
     1.8 +  apply simp
     1.9 +  done
    1.10  
    1.11  lemma closed_subset: "S \<subseteq> T \<Longrightarrow> closed S \<Longrightarrow> closedin (subtopology euclidean T) S"
    1.12    by (auto simp add: closedin_closed)
    1.13 @@ -693,7 +694,8 @@
    1.14    apply atomize
    1.15    apply (erule_tac x="y" in allE)
    1.16    apply (erule_tac x="xa" in allE)
    1.17 -  by arith
    1.18 +  apply arith
    1.19 +  done
    1.20  
    1.21  lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
    1.22    unfolding open_dist subset_eq mem_ball Ball_def dist_commute ..
    1.23 @@ -709,7 +711,8 @@
    1.24  lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
    1.25    unfolding mem_ball set_eq_iff
    1.26    apply (simp add: not_less)
    1.27 -  by (metis zero_le_dist order_trans dist_self)
    1.28 +  apply (metis zero_le_dist order_trans dist_self)
    1.29 +  done
    1.30  
    1.31  lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
    1.32  
    1.33 @@ -770,17 +773,21 @@
    1.34    defines "b' \<equiv> \<lambda>f :: 'a \<Rightarrow> real \<times> real. (\<Sum>(i::'a)\<in>Basis. snd (f i) *\<^sub>R i)"
    1.35    defines "I \<equiv> {f\<in>Basis \<rightarrow>\<^isub>E \<rat> \<times> \<rat>. box (a' f) (b' f) \<subseteq> M}"
    1.36    shows "M = (\<Union>f\<in>I. box (a' f) (b' f))"
    1.37 -proof safe
    1.38 -  fix x assume "x \<in> M"
    1.39 -  obtain e where e: "e > 0" "ball x e \<subseteq> M"
    1.40 -    using openE[OF `open M` `x \<in> M`] by auto
    1.41 -  moreover then obtain a b where ab: "x \<in> box a b"
    1.42 -    "\<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"
    1.43 -    using rational_boxes[OF e(1)] by metis
    1.44 -  ultimately show "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))"
    1.45 -     by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
    1.46 -        (auto simp: euclidean_representation I_def a'_def b'_def)
    1.47 -qed (auto simp: I_def)
    1.48 +proof -
    1.49 +  {
    1.50 +    fix x assume "x \<in> M"
    1.51 +    obtain e where e: "e > 0" "ball x e \<subseteq> M"
    1.52 +      using openE[OF `open M` `x \<in> M`] by auto
    1.53 +    moreover then obtain a b where ab: "x \<in> box a b"
    1.54 +      "\<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"
    1.55 +      using rational_boxes[OF e(1)] by metis
    1.56 +    ultimately have "x \<in> (\<Union>f\<in>I. box (a' f) (b' f))"
    1.57 +       by (intro UN_I[of "\<lambda>i\<in>Basis. (a \<bullet> i, b \<bullet> i)"])
    1.58 +          (auto simp: euclidean_representation I_def a'_def b'_def)
    1.59 +  }
    1.60 +  then show ?thesis by (auto simp: I_def)
    1.61 +qed
    1.62 +
    1.63  
    1.64  subsection{* Connectedness *}
    1.65  
    1.66 @@ -812,9 +819,14 @@
    1.67  proof-
    1.68    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> {})"
    1.69      unfolding connected_def openin_open closedin_closed
    1.70 -    apply (subst exists_diff) by blast
    1.71 +    apply (subst exists_diff)
    1.72 +    apply blast
    1.73 +    done
    1.74    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> {})"
    1.75 -    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis
    1.76 +    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)")
    1.77 +    apply (simp add: closed_def)
    1.78 +    apply metis
    1.79 +    done
    1.80  
    1.81    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'))"
    1.82      (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
    1.83 @@ -827,8 +839,8 @@
    1.84    then show ?thesis unfolding th0 th1 by simp
    1.85  qed
    1.86  
    1.87 -lemma connected_empty[simp, intro]: "connected {}"
    1.88 -  by (simp add: connected_def)
    1.89 +lemma connected_empty[simp, intro]: "connected {}"  (* FIXME duplicate? *)
    1.90 +  by simp
    1.91  
    1.92  
    1.93  subsection{* Limit points *}
    1.94 @@ -887,7 +899,8 @@
    1.95    unfolding closed_def
    1.96    apply (subst open_subopen)
    1.97    apply (simp add: islimpt_def subset_eq)
    1.98 -  by (metis ComplE ComplI)
    1.99 +  apply (metis ComplE ComplI)
   1.100 +  done
   1.101  
   1.102  lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
   1.103    unfolding islimpt_def by auto
   1.104 @@ -1199,15 +1212,13 @@
   1.105  
   1.106  subsection {* Filters and the ``eventually true'' quantifier *}
   1.107  
   1.108 -definition
   1.109 -  indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
   1.110 -    (infixr "indirection" 70) where
   1.111 -  "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
   1.112 +definition indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a filter"
   1.113 +    (infixr "indirection" 70)
   1.114 +  where "a indirection v = at a within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
   1.115  
   1.116  text {* Identify Trivial limits, where we can't approach arbitrarily closely. *}
   1.117  
   1.118 -lemma trivial_limit_within:
   1.119 -  shows "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
   1.120 +lemma trivial_limit_within: "trivial_limit (at a within S) \<longleftrightarrow> \<not> a islimpt S"
   1.121  proof
   1.122    assume "trivial_limit (at a within S)"
   1.123    thus "\<not> a islimpt S"
   1.124 @@ -1335,7 +1346,7 @@
   1.125  lemma eventually_within_interior:
   1.126    assumes "x \<in> interior S"
   1.127    shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
   1.128 -proof-
   1.129 +proof -
   1.130    from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
   1.131    { assume "?lhs"
   1.132      then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   1.133 @@ -1345,11 +1356,12 @@
   1.134        by auto
   1.135      then have "?rhs"
   1.136        unfolding eventually_at_topological by auto
   1.137 -  } moreover
   1.138 +  }
   1.139 +  moreover
   1.140    { assume "?rhs" hence "?lhs"
   1.141        by (auto elim: eventually_elim1 simp: eventually_at_filter)
   1.142 -  } ultimately
   1.143 -  show "?thesis" ..
   1.144 +  }
   1.145 +  ultimately show "?thesis" ..
   1.146  qed
   1.147  
   1.148  lemma at_within_interior:
   1.149 @@ -1480,7 +1492,7 @@
   1.150  lemma Lim_dist_ubound:
   1.151    assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
   1.152    shows "dist a l <= e"
   1.153 -proof-
   1.154 +proof -
   1.155    have "dist a l \<in> {..e}"
   1.156    proof (rule Lim_in_closed_set)
   1.157      show "closed {..e}" by simp
   1.158 @@ -1495,7 +1507,7 @@
   1.159    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.160    assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
   1.161    shows "norm(l) <= e"
   1.162 -proof-
   1.163 +proof -
   1.164    have "norm l \<in> {..e}"
   1.165    proof (rule Lim_in_closed_set)
   1.166      show "closed {..e}" by simp
   1.167 @@ -1510,7 +1522,7 @@
   1.168    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.169    assumes "\<not> (trivial_limit net)"  "(f ---> l) net"  "eventually (\<lambda>x. e <= norm(f x)) net"
   1.170    shows "e \<le> norm l"
   1.171 -proof-
   1.172 +proof -
   1.173    have "norm l \<in> {e..}"
   1.174    proof (rule Lim_in_closed_set)
   1.175      show "closed {e..}" by simp
   1.176 @@ -1526,8 +1538,8 @@
   1.177  lemma Lim_bilinear:
   1.178    assumes "(f ---> l) net" and "(g ---> m) net" and "bounded_bilinear h"
   1.179    shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
   1.180 -using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
   1.181 -by (rule bounded_bilinear.tendsto)
   1.182 +  using `bounded_bilinear h` `(f ---> l) net` `(g ---> m) net`
   1.183 +  by (rule bounded_bilinear.tendsto)
   1.184  
   1.185  text{* These are special for limits out of the same vector space. *}
   1.186  
   1.187 @@ -1545,8 +1557,8 @@
   1.188  
   1.189  text{* It's also sometimes useful to extract the limit point from the filter. *}
   1.190  
   1.191 -abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a" where
   1.192 -  "netlimit F \<equiv> Lim F (\<lambda>x. x)"
   1.193 +abbreviation netlimit :: "'a::t2_space filter \<Rightarrow> 'a"
   1.194 +  where "netlimit F \<equiv> Lim F (\<lambda>x. x)"
   1.195  
   1.196  lemma netlimit_within:
   1.197    "\<not> trivial_limit (at a within S) \<Longrightarrow> netlimit (at a within S) = a"
   1.198 @@ -1565,7 +1577,7 @@
   1.199    fixes x :: "'a::{t2_space,perfect_space}"
   1.200    assumes "x \<in> interior S"
   1.201    shows "netlimit (at x within S) = x"
   1.202 -using assms by (metis at_within_interior netlimit_at)
   1.203 +  using assms by (metis at_within_interior netlimit_at)
   1.204  
   1.205  text{* Transformation of limit. *}
   1.206  
   1.207 @@ -1619,11 +1631,11 @@
   1.208  
   1.209  lemma Lim_transform_away_at:
   1.210    fixes a b :: "'a::t1_space"
   1.211 -  assumes ab: "a\<noteq>b" and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   1.212 -  and fl: "(f ---> l) (at a)"
   1.213 +  assumes ab: "a\<noteq>b"
   1.214 +    and fg: "\<forall>x. x \<noteq> a \<and> x \<noteq> b \<longrightarrow> f x = g x"
   1.215 +    and fl: "(f ---> l) (at a)"
   1.216    shows "(g ---> l) (at a)"
   1.217 -  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl
   1.218 -  by simp
   1.219 +  using Lim_transform_away_within[OF ab, of UNIV f g l] fg fl by simp
   1.220  
   1.221  text{* Alternatively, within an open set. *}
   1.222  
   1.223 @@ -1665,28 +1677,32 @@
   1.224    assume "?lhs" moreover
   1.225    { assume "l \<in> S"
   1.226      hence "?rhs" using tendsto_const[of l sequentially] by auto
   1.227 -  } moreover
   1.228 +  }
   1.229 +  moreover
   1.230    { assume "l islimpt S"
   1.231      hence "?rhs" unfolding islimpt_sequential by auto
   1.232 -  } ultimately
   1.233 -  show "?rhs" unfolding closure_def by auto
   1.234 +  }
   1.235 +  ultimately show "?rhs"
   1.236 +    unfolding closure_def by auto
   1.237  next
   1.238    assume "?rhs"
   1.239 -  thus "?lhs" unfolding closure_def unfolding islimpt_sequential by auto
   1.240 +  thus "?lhs" unfolding closure_def islimpt_sequential by auto
   1.241  qed
   1.242  
   1.243  lemma closed_sequential_limits:
   1.244    fixes S :: "'a::first_countable_topology set"
   1.245    shows "closed S \<longleftrightarrow> (\<forall>x l. (\<forall>n. x n \<in> S) \<and> (x ---> l) sequentially \<longrightarrow> l \<in> S)"
   1.246    unfolding closed_limpt
   1.247 -  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]
   1.248 +  using closure_sequential [where 'a='a] closure_closed [where 'a='a]
   1.249 +    closed_limpt [where 'a='a] islimpt_sequential [where 'a='a] mem_delete [where 'a='a]
   1.250    by metis
   1.251  
   1.252  lemma closure_approachable:
   1.253    fixes S :: "'a::metric_space set"
   1.254    shows "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
   1.255    apply (auto simp add: closure_def islimpt_approachable)
   1.256 -  by (metis dist_self)
   1.257 +  apply (metis dist_self)
   1.258 +  done
   1.259  
   1.260  lemma closed_approachable:
   1.261    fixes S :: "'a::metric_space set"
   1.262 @@ -1697,17 +1713,18 @@
   1.263    fixes S :: "real set"
   1.264    assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
   1.265    shows "Inf S \<in> closure S"
   1.266 -  unfolding closure_approachable
   1.267 -proof safe
   1.268 +proof -
   1.269    have *: "\<forall>x\<in>S. Inf S \<le> x"
   1.270      using cInf_lower_EX[of _ S] assms by metis
   1.271 -
   1.272 -  fix e :: real assume "0 < e"
   1.273 -  then have "Inf S < Inf S + e" by simp
   1.274 -  with assms obtain x where "x \<in> S" "x < Inf S + e"
   1.275 -    by (subst (asm) cInf_less_iff[of _ B]) auto
   1.276 -  with * show "\<exists>x\<in>S. dist x (Inf S) < e"
   1.277 -    by (intro bexI[of _ x]) (auto simp add: dist_real_def)
   1.278 +  {
   1.279 +    fix e :: real assume "0 < e"
   1.280 +    then have "Inf S < Inf S + e" by simp
   1.281 +    with assms obtain x where "x \<in> S" "x < Inf S + e"
   1.282 +      by (subst (asm) cInf_less_iff[of _ B]) auto
   1.283 +    with * have "\<exists>x\<in>S. dist x (Inf S) < e"
   1.284 +      by (intro bexI[of _ x]) (auto simp add: dist_real_def)
   1.285 +  }
   1.286 +  then show ?thesis unfolding closure_approachable by auto
   1.287  qed
   1.288  
   1.289  lemma closed_contains_Inf:
   1.290 @@ -1731,7 +1748,8 @@
   1.291        then have "y : (S Int ball x e - {x})"
   1.292          unfolding ball_def by (simp add: dist_commute)
   1.293        then have "S Int ball x e - {x} ~= {}" by blast
   1.294 -    } then have "?rhs" by auto
   1.295 +    }
   1.296 +    then have "?rhs" by auto
   1.297    }
   1.298    moreover
   1.299    { assume "?rhs"
   1.300 @@ -1748,6 +1766,7 @@
   1.301    ultimately show ?thesis by auto
   1.302  qed
   1.303  
   1.304 +
   1.305  subsection {* Infimum Distance *}
   1.306  
   1.307  definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
   1.308 @@ -1755,29 +1774,30 @@
   1.309  lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = Inf {dist x a|a. a \<in> A}"
   1.310    by (simp add: infdist_def)
   1.311  
   1.312 -lemma infdist_nonneg:
   1.313 -  shows "0 \<le> infdist x A"
   1.314 -  using assms by (auto simp add: infdist_def intro: cInf_greatest)
   1.315 +lemma infdist_nonneg: "0 \<le> infdist x A"
   1.316 +  by (auto simp add: infdist_def intro: cInf_greatest)
   1.317  
   1.318  lemma infdist_le:
   1.319    assumes "a \<in> A"
   1.320 -  assumes "d = dist x a"
   1.321 +    and "d = dist x a"
   1.322    shows "infdist x A \<le> d"
   1.323    using assms by (auto intro!: cInf_lower[where z=0] simp add: infdist_def)
   1.324  
   1.325  lemma infdist_zero[simp]:
   1.326 -  assumes "a \<in> A" shows "infdist a A = 0"
   1.327 +  assumes "a \<in> A"
   1.328 +  shows "infdist a A = 0"
   1.329  proof -
   1.330    from infdist_le[OF assms, of "dist a a"] have "infdist a A \<le> 0" by auto
   1.331    with infdist_nonneg[of a A] assms show "infdist a A = 0" by auto
   1.332  qed
   1.333  
   1.334 -lemma infdist_triangle:
   1.335 -  shows "infdist x A \<le> infdist y A + dist x y"
   1.336 +lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
   1.337  proof cases
   1.338 -  assume "A = {}" thus ?thesis by (simp add: infdist_def)
   1.339 +  assume "A = {}"
   1.340 +  thus ?thesis by (simp add: infdist_def)
   1.341  next
   1.342 -  assume "A \<noteq> {}" then obtain a where "a \<in> A" by auto
   1.343 +  assume "A \<noteq> {}"
   1.344 +  then obtain a where "a \<in> A" by auto
   1.345    have "infdist x A \<le> Inf {dist x y + dist y a |a. a \<in> A}"
   1.346    proof (rule cInf_greatest)
   1.347      from `A \<noteq> {}` show "{dist x y + dist y a |a. a \<in> A} \<noteq> {}" by simp
   1.348 @@ -1815,10 +1835,13 @@
   1.349    proof (rule ccontr)
   1.350      assume "infdist x A \<noteq> 0"
   1.351      with infdist_nonneg[of x A] have "infdist x A > 0" by auto
   1.352 -    hence "ball x (infdist x A) \<inter> closure A = {}" apply auto
   1.353 -      by (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
   1.354 +    hence "ball x (infdist x A) \<inter> closure A = {}"
   1.355 +      apply auto
   1.356 +      apply (metis `0 < infdist x A` `x \<in> closure A` closure_approachable dist_commute
   1.357          eucl_less_not_refl euclidean_trans(2) infdist_le)
   1.358 -    hence "x \<notin> closure A" by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
   1.359 +      done
   1.360 +    hence "x \<notin> closure A"
   1.361 +      by (metis `0 < infdist x A` centre_in_ball disjoint_iff_not_equal)
   1.362      thus False using `x \<in> closure A` by simp
   1.363    qed
   1.364  next
   1.365 @@ -1880,7 +1903,8 @@
   1.366    apply (simp only: eventually_sequentially)
   1.367    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
   1.368    apply metis
   1.369 -  by arith
   1.370 +  apply arith
   1.371 +  done
   1.372  
   1.373  lemma seq_offset_rev:
   1.374    "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   1.375 @@ -1892,24 +1916,34 @@
   1.376  subsection {* More properties of closed balls *}
   1.377  
   1.378  lemma closed_cball: "closed (cball x e)"
   1.379 -unfolding cball_def closed_def
   1.380 -unfolding Collect_neg_eq [symmetric] not_le
   1.381 -apply (clarsimp simp add: open_dist, rename_tac y)
   1.382 -apply (rule_tac x="dist x y - e" in exI, clarsimp)
   1.383 -apply (rename_tac x')
   1.384 -apply (cut_tac x=x and y=x' and z=y in dist_triangle)
   1.385 -apply simp
   1.386 -done
   1.387 +  unfolding cball_def closed_def
   1.388 +  unfolding Collect_neg_eq [symmetric] not_le
   1.389 +  apply (clarsimp simp add: open_dist, rename_tac y)
   1.390 +  apply (rule_tac x="dist x y - e" in exI, clarsimp)
   1.391 +  apply (rename_tac x')
   1.392 +  apply (cut_tac x=x and y=x' and z=y in dist_triangle)
   1.393 +  apply simp
   1.394 +  done
   1.395  
   1.396  lemma open_contains_cball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0.  cball x e \<subseteq> S)"
   1.397 -proof-
   1.398 -  { fix x and e::real assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
   1.399 +proof -
   1.400 +  {
   1.401 +    fix x and e::real
   1.402 +    assume "x\<in>S" "e>0" "ball x e \<subseteq> S"
   1.403      hence "\<exists>d>0. cball x d \<subseteq> S" unfolding subset_eq by (rule_tac x="e/2" in exI, auto)
   1.404 -  } moreover
   1.405 -  { fix x and e::real assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
   1.406 -    hence "\<exists>d>0. ball x d \<subseteq> S" unfolding subset_eq apply(rule_tac x="e/2" in exI) by auto
   1.407 -  } ultimately
   1.408 -  show ?thesis unfolding open_contains_ball by auto
   1.409 +  }
   1.410 +  moreover
   1.411 +  {
   1.412 +    fix x and e::real
   1.413 +    assume "x\<in>S" "e>0" "cball x e \<subseteq> S"
   1.414 +    hence "\<exists>d>0. ball x d \<subseteq> S"
   1.415 +      unfolding subset_eq
   1.416 +      apply(rule_tac x="e/2" in exI)
   1.417 +      apply auto
   1.418 +      done
   1.419 +  }
   1.420 +  ultimately show ?thesis
   1.421 +    unfolding open_contains_ball by auto
   1.422  qed
   1.423  
   1.424  lemma open_contains_cball_eq: "open S ==> (\<forall>x. x \<in> S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S))"
   1.425 @@ -1933,7 +1967,10 @@
   1.426    }
   1.427    hence "e > 0" by (metis not_less)
   1.428    moreover
   1.429 -  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
   1.430 +  have "y \<in> cball x e"
   1.431 +    using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"]
   1.432 +      ball_subset_cball[of x e] `?lhs`
   1.433 +    unfolding closed_limpt by auto
   1.434    ultimately show "?rhs" by auto
   1.435  next
   1.436    assume "?rhs" hence "e>0"  by auto
   1.437 @@ -2027,25 +2064,25 @@
   1.438  lemma closure_ball:
   1.439    fixes x :: "'a::real_normed_vector"
   1.440    shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
   1.441 -apply (rule equalityI)
   1.442 -apply (rule closure_minimal)
   1.443 -apply (rule ball_subset_cball)
   1.444 -apply (rule closed_cball)
   1.445 -apply (rule subsetI, rename_tac y)
   1.446 -apply (simp add: le_less [where 'a=real])
   1.447 -apply (erule disjE)
   1.448 -apply (rule subsetD [OF closure_subset], simp)
   1.449 -apply (simp add: closure_def)
   1.450 -apply clarify
   1.451 -apply (rule closure_ball_lemma)
   1.452 -apply (simp add: zero_less_dist_iff)
   1.453 -done
   1.454 +  apply (rule equalityI)
   1.455 +  apply (rule closure_minimal)
   1.456 +  apply (rule ball_subset_cball)
   1.457 +  apply (rule closed_cball)
   1.458 +  apply (rule subsetI, rename_tac y)
   1.459 +  apply (simp add: le_less [where 'a=real])
   1.460 +  apply (erule disjE)
   1.461 +  apply (rule subsetD [OF closure_subset], simp)
   1.462 +  apply (simp add: closure_def)
   1.463 +  apply clarify
   1.464 +  apply (rule closure_ball_lemma)
   1.465 +  apply (simp add: zero_less_dist_iff)
   1.466 +  done
   1.467  
   1.468  (* In a trivial vector space, this fails for e = 0. *)
   1.469  lemma interior_cball:
   1.470    fixes x :: "'a::{real_normed_vector, perfect_space}"
   1.471    shows "interior (cball x e) = ball x e"
   1.472 -proof(cases "e\<ge>0")
   1.473 +proof (cases "e\<ge>0")
   1.474    case False note cs = this
   1.475    from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover
   1.476    { fix y assume "y \<in> cball x e"
   1.477 @@ -2066,15 +2103,18 @@
   1.478  
   1.479      hence "y \<in> ball x e" proof(cases "x = y")
   1.480        case True
   1.481 -      hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] by (auto simp add: dist_commute)
   1.482 +      hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball]
   1.483 +        by (auto simp add: dist_commute)
   1.484        thus "y \<in> ball x e" using `x = y ` by simp
   1.485      next
   1.486        case False
   1.487        have "dist (y + (d / 2 / dist y x) *\<^sub>R (y - x)) y < d" unfolding dist_norm
   1.488          using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by auto
   1.489 -      hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
   1.490 +      hence *:"y + (d / 2 / dist y x) *\<^sub>R (y - x) \<in> cball x e"
   1.491 +        using d as(1)[unfolded subset_eq] by blast
   1.492        have "y - x \<noteq> 0" using `x \<noteq> y` by auto
   1.493 -      hence **:"d / (2 * norm (y - x)) > 0" unfolding zero_less_norm_iff[THEN sym]
   1.494 +      hence **:"d / (2 * norm (y - x)) > 0"
   1.495 +        unfolding zero_less_norm_iff[THEN sym]
   1.496          using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
   1.497  
   1.498        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)"
   1.499 @@ -2086,9 +2126,11 @@
   1.500        also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: distrib_right dist_norm)
   1.501        finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
   1.502        thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
   1.503 -    qed  }
   1.504 +    qed
   1.505 +  }
   1.506    hence "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e" by auto
   1.507 -  ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto
   1.508 +  ultimately show ?thesis
   1.509 +    using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto
   1.510  qed
   1.511  
   1.512  lemma frontier_ball:
   1.513 @@ -2096,19 +2138,24 @@
   1.514    shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
   1.515    apply (simp add: frontier_def closure_ball interior_open order_less_imp_le)
   1.516    apply (simp add: set_eq_iff)
   1.517 -  by arith
   1.518 +  apply arith
   1.519 +  done
   1.520  
   1.521  lemma frontier_cball:
   1.522    fixes a :: "'a::{real_normed_vector, perfect_space}"
   1.523    shows "frontier(cball a e) = {x. dist a x = e}"
   1.524    apply (simp add: frontier_def interior_cball closed_cball order_less_imp_le)
   1.525    apply (simp add: set_eq_iff)
   1.526 -  by arith
   1.527 +  apply arith
   1.528 +  done
   1.529  
   1.530  lemma cball_eq_empty: "(cball x e = {}) \<longleftrightarrow> e < 0"
   1.531    apply (simp add: set_eq_iff not_le)
   1.532 -  by (metis zero_le_dist dist_self order_less_le_trans)
   1.533 -lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
   1.534 +  apply (metis zero_le_dist dist_self order_less_le_trans)
   1.535 +  done
   1.536 +
   1.537 +lemma cball_empty: "e < 0 ==> cball x e = {}"
   1.538 +  by (simp add: cball_eq_empty)
   1.539  
   1.540  lemma cball_eq_sing:
   1.541    fixes x :: "'a::{metric_space,perfect_space}"
   1.542 @@ -2130,25 +2177,24 @@
   1.543  subsection {* Boundedness *}
   1.544  
   1.545    (* FIXME: This has to be unified with BSEQ!! *)
   1.546 -definition (in metric_space)
   1.547 -  bounded :: "'a set \<Rightarrow> bool" where
   1.548 -  "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
   1.549 +definition (in metric_space) bounded :: "'a set \<Rightarrow> bool"
   1.550 +  where "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
   1.551  
   1.552  lemma bounded_subset_cball: "bounded S \<longleftrightarrow> (\<exists>e x. S \<subseteq> cball x e)"
   1.553    unfolding bounded_def subset_eq by auto
   1.554  
   1.555  lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
   1.556 -unfolding bounded_def
   1.557 -apply safe
   1.558 -apply (rule_tac x="dist a x + e" in exI, clarify)
   1.559 -apply (drule (1) bspec)
   1.560 -apply (erule order_trans [OF dist_triangle add_left_mono])
   1.561 -apply auto
   1.562 -done
   1.563 +  unfolding bounded_def
   1.564 +  apply safe
   1.565 +  apply (rule_tac x="dist a x + e" in exI, clarify)
   1.566 +  apply (drule (1) bspec)
   1.567 +  apply (erule order_trans [OF dist_triangle add_left_mono])
   1.568 +  apply auto
   1.569 +  done
   1.570  
   1.571  lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
   1.572 -unfolding bounded_any_center [where a=0]
   1.573 -by (simp add: dist_norm)
   1.574 +  unfolding bounded_any_center [where a=0]
   1.575 +  by (simp add: dist_norm)
   1.576  
   1.577  lemma bounded_realI: assumes "\<forall>x\<in>s. abs (x::real) \<le> B" shows "bounded s"
   1.578    unfolding bounded_def dist_real_def apply(rule_tac x=0 in exI)
   1.579 @@ -2163,10 +2209,15 @@
   1.580  lemma bounded_interior[intro]: "bounded S ==> bounded(interior S)"
   1.581    by (metis bounded_subset interior_subset)
   1.582  
   1.583 -lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)"
   1.584 -proof-
   1.585 -  from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" unfolding bounded_def by auto
   1.586 -  { fix y assume "y \<in> closure S"
   1.587 +lemma bounded_closure[intro]:
   1.588 +  assumes "bounded S"
   1.589 +  shows "bounded (closure S)"
   1.590 +proof -
   1.591 +  from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a"
   1.592 +    unfolding bounded_def by auto
   1.593 +  {
   1.594 +    fix y
   1.595 +    assume "y \<in> closure S"
   1.596      then obtain f where f: "\<forall>n. f n \<in> S"  "(f ---> y) sequentially"
   1.597        unfolding closure_sequential by auto
   1.598      have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
   1.599 @@ -2205,10 +2256,10 @@
   1.600    done
   1.601  
   1.602  lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
   1.603 -  by (induct rule: finite_induct[of F], auto)
   1.604 +  by (induct rule: finite_induct[of F]) auto
   1.605  
   1.606  lemma bounded_UN [intro]: "finite A \<Longrightarrow> \<forall>x\<in>A. bounded (B x) \<Longrightarrow> bounded (\<Union>x\<in>A. B x)"
   1.607 -  by (induct set: finite, auto)
   1.608 +  by (induct set: finite) auto
   1.609  
   1.610  lemma bounded_insert [simp]: "bounded (insert x S) \<longleftrightarrow> bounded S"
   1.611  proof -
   1.612 @@ -2218,12 +2269,14 @@
   1.613  qed
   1.614  
   1.615  lemma finite_imp_bounded [intro]: "finite S \<Longrightarrow> bounded S"
   1.616 -  by (induct set: finite, simp_all)
   1.617 +  by (induct set: finite) simp_all
   1.618  
   1.619  lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
   1.620    apply (simp add: bounded_iff)
   1.621    apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
   1.622 -  by metis arith
   1.623 +  apply metis
   1.624 +  apply arith
   1.625 +  done
   1.626  
   1.627  lemma Bseq_eq_bounded: "Bseq f \<longleftrightarrow> bounded (range f::_::real_normed_vector set)"
   1.628    unfolding Bseq_def bounded_pos by auto
   1.629 @@ -2232,8 +2285,7 @@
   1.630    by (metis Int_lower1 Int_lower2 bounded_subset)
   1.631  
   1.632  lemma bounded_diff[intro]: "bounded S ==> bounded (S - T)"
   1.633 -apply (metis Diff_subset bounded_subset)
   1.634 -done
   1.635 +  by (metis Diff_subset bounded_subset)
   1.636  
   1.637  lemma not_bounded_UNIV[simp, intro]:
   1.638    "\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
   1.639 @@ -2250,16 +2302,24 @@
   1.640  lemma bounded_linear_image:
   1.641    assumes "bounded S" "bounded_linear f"
   1.642    shows "bounded(f ` S)"
   1.643 -proof-
   1.644 -  from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
   1.645 -  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)
   1.646 -  { fix x assume "x\<in>S"
   1.647 +proof -
   1.648 +  from assms(1) obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b"
   1.649 +    unfolding bounded_pos by auto
   1.650 +  from assms(2) obtain B where B:"B>0" "\<forall>x. norm (f x) \<le> B * norm x"
   1.651 +    using bounded_linear.pos_bounded by (auto simp add: mult_ac)
   1.652 +  {
   1.653 +    fix x assume "x\<in>S"
   1.654      hence "norm x \<le> b" using b by auto
   1.655 -    hence "norm (f x) \<le> B * b" using B(2) apply(erule_tac x=x in allE)
   1.656 -      by (metis B(1) B(2) order_trans mult_le_cancel_left_pos)
   1.657 +    hence "norm (f x) \<le> B * b" using B(2)
   1.658 +      apply (erule_tac x=x in allE)
   1.659 +      apply (metis B(1) B(2) order_trans mult_le_cancel_left_pos)
   1.660 +      done
   1.661    }
   1.662 -  thus ?thesis unfolding bounded_pos apply(rule_tac x="b*B" in exI)
   1.663 -    using b B mult_pos_pos [of b B] by (auto simp add: mult_commute)
   1.664 +  thus ?thesis unfolding bounded_pos
   1.665 +    apply (rule_tac x="b*B" in exI)
   1.666 +    using b B mult_pos_pos [of b B]
   1.667 +    apply (auto simp add: mult_commute)
   1.668 +    done
   1.669  qed
   1.670  
   1.671  lemma bounded_scaling:
   1.672 @@ -2271,13 +2331,20 @@
   1.673  
   1.674  lemma bounded_translation:
   1.675    fixes S :: "'a::real_normed_vector set"
   1.676 -  assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
   1.677 +  assumes "bounded S"
   1.678 +  shows "bounded ((\<lambda>x. a + x) ` S)"
   1.679  proof-
   1.680 -  from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
   1.681 -  { fix x assume "x\<in>S"
   1.682 -    hence "norm (a + x) \<le> b + norm a" using norm_triangle_ineq[of a x] b by auto
   1.683 +  from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b"
   1.684 +    unfolding bounded_pos by auto
   1.685 +  {
   1.686 +    fix x
   1.687 +    assume "x\<in>S"
   1.688 +    hence "norm (a + x) \<le> b + norm a"
   1.689 +      using norm_triangle_ineq[of a x] b by auto
   1.690    }
   1.691 -  thus ?thesis unfolding bounded_pos using norm_ge_zero[of a] b(1) using add_strict_increasing[of b 0 "norm a"]
   1.692 +  thus ?thesis
   1.693 +    unfolding bounded_pos
   1.694 +    using norm_ge_zero[of a] b(1) and add_strict_increasing[of b 0 "norm a"]
   1.695      by (auto intro!: exI[of _ "b + norm a"])
   1.696  qed
   1.697  
   1.698 @@ -2315,15 +2382,18 @@
   1.699    shows "finite S \<Longrightarrow> Sup(insert x S) = (if S = {} then x else max x (Sup S))"
   1.700    apply (rule Sup_insert)
   1.701    apply (rule finite_imp_bounded)
   1.702 -  by simp
   1.703 +  apply simp
   1.704 +  done
   1.705  
   1.706  lemma bounded_has_Inf:
   1.707    fixes S :: "real set"
   1.708    assumes "bounded S"  "S \<noteq> {}"
   1.709    shows "\<forall>x\<in>S. x >= Inf S" and "\<forall>b. (\<forall>x\<in>S. x >= b) \<longrightarrow> Inf S >= b"
   1.710  proof
   1.711 -  fix x assume "x\<in>S"
   1.712 -  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a" unfolding bounded_real by auto
   1.713 +  fix x
   1.714 +  assume "x\<in>S"
   1.715 +  from assms(1) obtain a where a:"\<forall>x\<in>S. \<bar>x\<bar> \<le> a"
   1.716 +    unfolding bounded_real by auto
   1.717    thus "x \<ge> Inf S" using `x\<in>S`
   1.718      by (metis cInf_lower_EX abs_le_D2 minus_le_iff)
   1.719  next
   1.720 @@ -2353,24 +2423,40 @@
   1.721    shows "\<exists>x \<in> s. x islimpt t"
   1.722  proof(rule ccontr)
   1.723    assume "\<not> (\<exists>x \<in> s. x islimpt t)"
   1.724 -  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
   1.725 +  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)"
   1.726 +    unfolding islimpt_def
   1.727      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
   1.728    obtain g where g:"g\<subseteq>{t. \<exists>x. x \<in> s \<and> t = f x}" "finite g" "s \<subseteq> \<Union>g"
   1.729 -    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
   1.730 +    using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="{t. \<exists>x. x\<in>s \<and> t = f x}"]]
   1.731 +    using f by auto
   1.732    from g(1,3) have g':"\<forall>x\<in>g. \<exists>xa \<in> s. x = f xa" by auto
   1.733 -  { fix x y assume "x\<in>t" "y\<in>t" "f x = f y"
   1.734 -    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
   1.735 -    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  }
   1.736 -  hence "inj_on f t" unfolding inj_on_def by simp
   1.737 -  hence "infinite (f ` t)" using assms(2) using finite_imageD by auto
   1.738 +  {
   1.739 +    fix x y
   1.740 +    assume "x\<in>t" "y\<in>t" "f x = f y"
   1.741 +    hence "x \<in> f x"  "y \<in> f x \<longrightarrow> y = x"
   1.742 +      using f[THEN bspec[where x=x]] and `t\<subseteq>s` by auto
   1.743 +    hence "x = y"
   1.744 +      using `f x = f y` and f[THEN bspec[where x=y]] and `y\<in>t` and `t\<subseteq>s` by auto
   1.745 +  }
   1.746 +  hence "inj_on f t"
   1.747 +    unfolding inj_on_def by simp
   1.748 +  hence "infinite (f ` t)"
   1.749 +    using assms(2) using finite_imageD by auto
   1.750    moreover
   1.751 -  { fix x assume "x\<in>t" "f x \<notin> g"
   1.752 +  {
   1.753 +    fix x
   1.754 +    assume "x\<in>t" "f x \<notin> g"
   1.755      from g(3) assms(3) `x\<in>t` obtain h where "h\<in>g" and "x\<in>h" by auto
   1.756 -    then obtain y where "y\<in>s" "h = f y" using g'[THEN bspec[where x=h]] by auto
   1.757 -    hence "y = x" using f[THEN bspec[where x=y]] and `x\<in>t` and `x\<in>h`[unfolded `h = f y`] by auto
   1.758 -    hence False using `f x \<notin> g` `h\<in>g` unfolding `h = f y` by auto  }
   1.759 +    then obtain y where "y\<in>s" "h = f y"
   1.760 +      using g'[THEN bspec[where x=h]] by auto
   1.761 +    hence "y = x"
   1.762 +      using f[THEN bspec[where x=y]] and `x\<in>t` and `x\<in>h`[unfolded `h = f y`] by auto
   1.763 +    hence False
   1.764 +      using `f x \<notin> g` `h\<in>g` unfolding `h = f y` by auto
   1.765 +  }
   1.766    hence "f ` t \<subseteq> g" by auto
   1.767 -  ultimately show False using g(2) using finite_subset by auto
   1.768 +  ultimately show False
   1.769 +    using g(2) using finite_subset by auto
   1.770  qed
   1.771  
   1.772  lemma acc_point_range_imp_convergent_subsequence:
   1.773 @@ -2381,7 +2467,8 @@
   1.774    from countable_basis_at_decseq[of l] guess A . note A = this
   1.775  
   1.776    def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> f j \<in> A (Suc n)"
   1.777 -  { fix n i
   1.778 +  {
   1.779 +    fix n i
   1.780      have "infinite (A (Suc n) \<inter> range f - f`{.. i})"
   1.781        using l A by auto
   1.782      then have "\<exists>x. x \<in> A (Suc n) \<inter> range f - f`{.. i}"
   1.783 @@ -2391,7 +2478,8 @@
   1.784      then have "\<exists>a. i < a \<and> f a \<in> A (Suc n)"
   1.785        by (auto simp: not_le)
   1.786      then have "i < s n i" "f (s n i) \<in> A (Suc n)"
   1.787 -      unfolding s_def by (auto intro: someI2_ex) }
   1.788 +      unfolding s_def by (auto intro: someI2_ex)
   1.789 +  }
   1.790    note s = this
   1.791    def r \<equiv> "nat_rec (s 0 0) s"
   1.792    have "subseq r"
   1.793 @@ -2402,9 +2490,13 @@
   1.794      fix S assume "open S" "l \<in> S"
   1.795      with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
   1.796      moreover
   1.797 -    { fix i assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
   1.798 -        by (cases i) (simp_all add: r_def s) }
   1.799 -    then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
   1.800 +    {
   1.801 +      fix i
   1.802 +      assume "Suc 0 \<le> i" then have "f (r i) \<in> A i"
   1.803 +        by (cases i) (simp_all add: r_def s)
   1.804 +    }
   1.805 +    then have "eventually (\<lambda>i. f (r i) \<in> A i) sequentially"
   1.806 +      by (auto simp: eventually_sequentially)
   1.807      ultimately show "eventually (\<lambda>i. f (r i) \<in> S) sequentially"
   1.808        by eventually_elim auto
   1.809    qed
   1.810 @@ -2429,11 +2521,11 @@
   1.811  lemma closure_insert:
   1.812    fixes x :: "'a::t1_space"
   1.813    shows "closure (insert x s) = insert x (closure s)"
   1.814 -apply (rule closure_unique)
   1.815 -apply (rule insert_mono [OF closure_subset])
   1.816 -apply (rule closed_insert [OF closed_closure])
   1.817 -apply (simp add: closure_minimal)
   1.818 -done
   1.819 +  apply (rule closure_unique)
   1.820 +  apply (rule insert_mono [OF closure_subset])
   1.821 +  apply (rule closed_insert [OF closed_closure])
   1.822 +  apply (simp add: closure_minimal)
   1.823 +  done
   1.824  
   1.825  lemma islimpt_insert:
   1.826    fixes x :: "'a::t1_space"
   1.827 @@ -2466,12 +2558,12 @@
   1.828  lemma islimpt_finite:
   1.829    fixes x :: "'a::t1_space"
   1.830    shows "finite s \<Longrightarrow> \<not> x islimpt s"
   1.831 -by (induct set: finite, simp_all add: islimpt_insert)
   1.832 +  by (induct set: finite) (simp_all add: islimpt_insert)
   1.833  
   1.834  lemma islimpt_union_finite:
   1.835    fixes x :: "'a::t1_space"
   1.836    shows "finite s \<Longrightarrow> x islimpt (s \<union> t) \<longleftrightarrow> x islimpt t"
   1.837 -by (simp add: islimpt_Un islimpt_finite)
   1.838 +  by (simp add: islimpt_Un islimpt_finite)
   1.839  
   1.840  lemma islimpt_eq_acc_point:
   1.841    fixes l :: "'a :: t1_space"
   1.842 @@ -2526,26 +2618,35 @@
   1.843    fixes s :: "'a::{first_countable_topology, t2_space} set"
   1.844    assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
   1.845    shows "closed s"
   1.846 -proof-
   1.847 -  { fix x l assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
   1.848 +proof -
   1.849 +  {
   1.850 +    fix x l
   1.851 +    assume as: "\<forall>n::nat. x n \<in> s" "(x ---> l) sequentially"
   1.852      hence "l \<in> s"
   1.853 -    proof(cases "\<forall>n. x n \<noteq> l")
   1.854 -      case False thus "l\<in>s" using as(1) by auto
   1.855 +    proof (cases "\<forall>n. x n \<noteq> l")
   1.856 +      case False
   1.857 +      thus "l\<in>s" using as(1) by auto
   1.858      next
   1.859        case True note cas = this
   1.860 -      with as(2) have "infinite (range x)" using sequence_infinite_lemma[of x l] by auto
   1.861 -      then obtain l' where "l'\<in>s" "l' islimpt (range x)" using assms[THEN spec[where x="range x"]] as(1) by auto
   1.862 -      thus "l\<in>s" using sequence_unique_limpt[of x l l'] using as cas by auto
   1.863 -    qed  }
   1.864 +      with as(2) have "infinite (range x)"
   1.865 +        using sequence_infinite_lemma[of x l] by auto
   1.866 +      then obtain l' where "l'\<in>s" "l' islimpt (range x)"
   1.867 +        using assms[THEN spec[where x="range x"]] as(1) by auto
   1.868 +      thus "l\<in>s" using sequence_unique_limpt[of x l l']
   1.869 +        using as cas by auto
   1.870 +    qed
   1.871 +  }
   1.872    thus ?thesis unfolding closed_sequential_limits by fast
   1.873  qed
   1.874  
   1.875  lemma compact_imp_bounded:
   1.876 -  assumes "compact U" shows "bounded U"
   1.877 +  assumes "compact U"
   1.878 +  shows "bounded U"
   1.879  proof -
   1.880 -  have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)" using assms by auto
   1.881 +  have "compact U" "\<forall>x\<in>U. open (ball x 1)" "U \<subseteq> (\<Union>x\<in>U. ball x 1)"
   1.882 +    using assms by auto
   1.883    then obtain D where D: "D \<subseteq> U" "finite D" "U \<subseteq> (\<Union>x\<in>D. ball x 1)"
   1.884 -    by (elim compactE_image)
   1.885 +    by (rule compactE_image)
   1.886    from `finite D` have "bounded (\<Union>x\<in>D. ball x 1)"
   1.887      by (simp add: bounded_UN)
   1.888    thus "bounded U" using `U \<subseteq> (\<Union>x\<in>D. ball x 1)` 
   1.889 @@ -2557,10 +2658,12 @@
   1.890  lemma compact_union [intro]:
   1.891    assumes "compact s" "compact t" shows " compact (s \<union> t)"
   1.892  proof (rule compactI)
   1.893 -  fix f assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
   1.894 +  fix f
   1.895 +  assume *: "Ball f open" "s \<union> t \<subseteq> \<Union>f"
   1.896    from * `compact s` obtain s' where "s' \<subseteq> f \<and> finite s' \<and> s \<subseteq> \<Union>s'"
   1.897      unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
   1.898 -  moreover from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
   1.899 +  moreover
   1.900 +  from * `compact t` obtain t' where "t' \<subseteq> f \<and> finite t' \<and> t \<subseteq> \<Union>t'"
   1.901      unfolding compact_eq_heine_borel by (auto elim!: allE[of _ f]) metis
   1.902    ultimately show "\<exists>f'\<subseteq>f. finite f' \<and> s \<union> t \<subseteq> \<Union>f'"
   1.903      by (auto intro!: exI[of _ "s' \<union> t'"])
   1.904 @@ -2596,8 +2699,7 @@
   1.905    thus ?thesis by simp
   1.906  qed
   1.907  
   1.908 -lemma finite_imp_compact:
   1.909 -  shows "finite s \<Longrightarrow> compact s"
   1.910 +lemma finite_imp_compact: "finite s \<Longrightarrow> compact s"
   1.911    by (induct set: finite) simp_all
   1.912  
   1.913  lemma open_delete:
   1.914 @@ -2841,12 +2943,14 @@
   1.915    assumes "seq_compact U"
   1.916    shows "countably_compact U"
   1.917  proof (safe intro!: countably_compactI)
   1.918 -  fix A assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
   1.919 +  fix A
   1.920 +  assume A: "\<forall>a\<in>A. open a" "U \<subseteq> \<Union>A" "countable A"
   1.921    have subseq: "\<And>X. range X \<subseteq> U \<Longrightarrow> \<exists>r x. x \<in> U \<and> subseq r \<and> (X \<circ> r) ----> x"
   1.922      using `seq_compact U` by (fastforce simp: seq_compact_def subset_eq)
   1.923    show "\<exists>T\<subseteq>A. finite T \<and> U \<subseteq> \<Union>T"
   1.924    proof cases
   1.925 -    assume "finite A" with A show ?thesis by auto
   1.926 +    assume "finite A"
   1.927 +    with A show ?thesis by auto
   1.928    next
   1.929      assume "infinite A"
   1.930      then have "A \<noteq> {}" by auto
   1.931 @@ -2882,17 +2986,21 @@
   1.932    assumes "compact U" shows "seq_compact U"
   1.933    unfolding seq_compact_def
   1.934  proof safe
   1.935 -  fix X :: "nat \<Rightarrow> 'a" assume "\<forall>n. X n \<in> U"
   1.936 +  fix X :: "nat \<Rightarrow> 'a"
   1.937 +  assume "\<forall>n. X n \<in> U"
   1.938    then have "eventually (\<lambda>x. x \<in> U) (filtermap X sequentially)"
   1.939      by (auto simp: eventually_filtermap)
   1.940 -  moreover have "filtermap X sequentially \<noteq> bot"
   1.941 +  moreover
   1.942 +  have "filtermap X sequentially \<noteq> bot"
   1.943      by (simp add: trivial_limit_def eventually_filtermap)
   1.944 -  ultimately obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
   1.945 +  ultimately
   1.946 +  obtain x where "x \<in> U" and x: "inf (nhds x) (filtermap X sequentially) \<noteq> bot" (is "?F \<noteq> _")
   1.947      using `compact U` by (auto simp: compact_filter)
   1.948  
   1.949    from countable_basis_at_decseq[of x] guess A . note A = this
   1.950    def s \<equiv> "\<lambda>n i. SOME j. i < j \<and> X j \<in> A (Suc n)"
   1.951 -  { fix n i
   1.952 +  {
   1.953 +    fix n i
   1.954      have "\<exists>a. i < a \<and> X a \<in> A (Suc n)"
   1.955      proof (rule ccontr)
   1.956        assume "\<not> (\<exists>a>i. X a \<in> A (Suc n))"
   1.957 @@ -2907,7 +3015,8 @@
   1.958          by (simp add: eventually_False)
   1.959      qed
   1.960      then have "i < s n i" "X (s n i) \<in> A (Suc n)"
   1.961 -      unfolding s_def by (auto intro: someI2_ex) }
   1.962 +      unfolding s_def by (auto intro: someI2_ex)
   1.963 +  }
   1.964    note s = this
   1.965    def r \<equiv> "nat_rec (s 0 0) s"
   1.966    have "subseq r"
   1.967 @@ -2915,12 +3024,18 @@
   1.968    moreover
   1.969    have "(\<lambda>n. X (r n)) ----> x"
   1.970    proof (rule topological_tendstoI)
   1.971 -    fix S assume "open S" "x \<in> S"
   1.972 +    fix S
   1.973 +    assume "open S" "x \<in> S"
   1.974      with A(3) have "eventually (\<lambda>i. A i \<subseteq> S) sequentially" by auto
   1.975      moreover
   1.976 -    { fix i assume "Suc 0 \<le> i" then have "X (r i) \<in> A i"
   1.977 -        by (cases i) (simp_all add: r_def s) }
   1.978 -    then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially" by (auto simp: eventually_sequentially)
   1.979 +    {
   1.980 +      fix i
   1.981 +      assume "Suc 0 \<le> i"
   1.982 +      then have "X (r i) \<in> A i"
   1.983 +        by (cases i) (simp_all add: r_def s)
   1.984 +    }
   1.985 +    then have "eventually (\<lambda>i. X (r i) \<in> A i) sequentially"
   1.986 +      by (auto simp: eventually_sequentially)
   1.987      ultimately show "eventually (\<lambda>i. X (r i) \<in> S) sequentially"
   1.988        by eventually_elim auto
   1.989    qed
   1.990 @@ -2975,7 +3090,9 @@
   1.991    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))"
   1.992    shows "seq_compact s"
   1.993  proof -
   1.994 -  { fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
   1.995 +  {
   1.996 +    fix f :: "nat \<Rightarrow> 'a"
   1.997 +    assume f: "\<forall>n. f n \<in> s"
   1.998      have "\<exists>l\<in>s. \<exists>r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
   1.999      proof (cases "finite (range f)")
  1.1000        case True
  1.1001 @@ -3031,37 +3148,59 @@
  1.1002  
  1.1003  lemma cauchy_def:
  1.1004    "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
  1.1005 -unfolding Cauchy_def by metis
  1.1006 -
  1.1007 -fun helper_1::"('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
  1.1008 +  unfolding Cauchy_def by metis
  1.1009 +
  1.1010 +fun helper_1 :: "('a::metric_space set) \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> 'a" where
  1.1011    "helper_1 s e n = (SOME y::'a. y \<in> s \<and> (\<forall>m<n. \<not> (dist (helper_1 s e m) y < e)))"
  1.1012  declare helper_1.simps[simp del]
  1.1013  
  1.1014  lemma seq_compact_imp_totally_bounded:
  1.1015    assumes "seq_compact s"
  1.1016    shows "\<forall>e>0. \<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> (\<Union>((\<lambda>x. ball x e) ` k))"
  1.1017 -proof(rule, rule, rule ccontr)
  1.1018 -  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))"
  1.1019 +proof (rule, rule, rule ccontr)
  1.1020 +  fix e::real
  1.1021 +  assume "e>0" and assm:"\<not> (\<exists>k. finite k \<and> k \<subseteq> s \<and> s \<subseteq> \<Union>((\<lambda>x. ball x e) ` k))"
  1.1022    def x \<equiv> "helper_1 s e"
  1.1023 -  { fix n
  1.1024 +  {
  1.1025 +    fix n
  1.1026      have "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
  1.1027 -    proof(induct_tac rule:nat_less_induct)
  1.1028 -      fix n  def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
  1.1029 -      assume as:"\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
  1.1030 -      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
  1.1031 -      then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)" unfolding subset_eq by auto
  1.1032 -      have "Q (x n)" unfolding x_def and helper_1.simps[of s e n]
  1.1033 -        apply(rule someI2[where a=z]) unfolding x_def[symmetric] and Q_def using z by auto
  1.1034 -      thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)" unfolding Q_def by auto
  1.1035 -    qed }
  1.1036 -  hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)" by blast+
  1.1037 -  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
  1.1038 -  from this(3) have "Cauchy (x \<circ> r)" using LIMSEQ_imp_Cauchy by auto
  1.1039 -  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
  1.1040 +    proof (induct n rule: nat_less_induct)
  1.1041 +      fix n
  1.1042 +      def Q \<equiv> "(\<lambda>y. y \<in> s \<and> (\<forall>m<n. \<not> dist (x m) y < e))"
  1.1043 +      assume as: "\<forall>m<n. x m \<in> s \<and> (\<forall>ma<m. \<not> dist (x ma) (x m) < e)"
  1.1044 +      have "\<not> s \<subseteq> (\<Union>x\<in>x ` {0..<n}. ball x e)"
  1.1045 +        using assm
  1.1046 +        apply simp
  1.1047 +        apply (erule_tac x="x ` {0 ..< n}" in allE)
  1.1048 +        using as
  1.1049 +        apply auto
  1.1050 +        done
  1.1051 +      then obtain z where z:"z\<in>s" "z \<notin> (\<Union>x\<in>x ` {0..<n}. ball x e)"
  1.1052 +        unfolding subset_eq by auto
  1.1053 +      have "Q (x n)"
  1.1054 +        unfolding x_def and helper_1.simps[of s e n]
  1.1055 +        apply (rule someI2[where a=z])
  1.1056 +        unfolding x_def[symmetric] and Q_def
  1.1057 +        using z
  1.1058 +        apply auto
  1.1059 +        done
  1.1060 +      thus "x n \<in> s \<and> (\<forall>m<n. \<not> dist (x m) (x n) < e)"
  1.1061 +        unfolding Q_def by auto
  1.1062 +    qed
  1.1063 +  }
  1.1064 +  hence "\<forall>n::nat. x n \<in> s" and x:"\<forall>n. \<forall>m < n. \<not> (dist (x m) (x n) < e)"
  1.1065 +    by blast+
  1.1066 +  then obtain l r where "l\<in>s" and r:"subseq r" and "((x \<circ> r) ---> l) sequentially"
  1.1067 +    using assms(1)[unfolded seq_compact_def, THEN spec[where x=x]] by auto
  1.1068 +  from this(3) have "Cauchy (x \<circ> r)"
  1.1069 +    using LIMSEQ_imp_Cauchy by auto
  1.1070 +  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"
  1.1071 +    unfolding cauchy_def using `e>0` by auto
  1.1072    show False
  1.1073      using N[THEN spec[where x=N], THEN spec[where x="N+1"]]
  1.1074      using r[unfolded subseq_def, THEN spec[where x=N], THEN spec[where x="N+1"]]
  1.1075 -    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]] by auto
  1.1076 +    using x[THEN spec[where x="r (N+1)"], THEN spec[where x="r (N)"]]
  1.1077 +    by auto
  1.1078  qed
  1.1079  
  1.1080  subsubsection{* Heine-Borel theorem *}
  1.1081 @@ -3115,9 +3254,11 @@
  1.1082    fixes s :: "'a::metric_space set"
  1.1083    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
  1.1084  proof
  1.1085 -  assume ?lhs thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
  1.1086 +  assume ?lhs
  1.1087 +  thus ?rhs using heine_borel_imp_bolzano_weierstrass[of s] by auto
  1.1088  next
  1.1089 -  assume ?rhs thus ?lhs
  1.1090 +  assume ?rhs
  1.1091 +  thus ?lhs
  1.1092      unfolding compact_eq_seq_compact_metric by (rule bolzano_weierstrass_imp_seq_compact)
  1.1093  qed
  1.1094  
  1.1095 @@ -3153,11 +3294,16 @@
  1.1096    fixes s :: "'a::heine_borel set"
  1.1097    shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
  1.1098  proof
  1.1099 -  assume ?lhs thus ?rhs
  1.1100 -    using compact_imp_closed compact_imp_bounded by blast
  1.1101 +  assume ?lhs
  1.1102 +  thus ?rhs
  1.1103 +    using compact_imp_closed compact_imp_bounded
  1.1104 +    by blast
  1.1105  next
  1.1106 -  assume ?rhs thus ?lhs
  1.1107 -    using bounded_closed_imp_seq_compact[of s] unfolding compact_eq_seq_compact_metric by auto
  1.1108 +  assume ?rhs
  1.1109 +  thus ?lhs
  1.1110 +    using bounded_closed_imp_seq_compact[of s]
  1.1111 +    unfolding compact_eq_seq_compact_metric
  1.1112 +    by auto
  1.1113  qed
  1.1114  
  1.1115  (* TODO: is this lemma necessary? *)
  1.1116 @@ -3186,12 +3332,17 @@
  1.1117    shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r. subseq r \<and>
  1.1118          (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
  1.1119  proof safe
  1.1120 -  fix d :: "'a set" assume d: "d \<subseteq> Basis" 
  1.1121 +  fix d :: "'a set"
  1.1122 +  assume d: "d \<subseteq> Basis" 
  1.1123    with finite_Basis have "finite d" by (blast intro: finite_subset)
  1.1124    from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
  1.1125 -      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
  1.1126 -  proof(induct d) case empty thus ?case unfolding subseq_def by auto
  1.1127 -  next case (insert k d) have k[intro]:"k\<in>Basis" using insert by auto
  1.1128 +    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
  1.1129 +  proof (induct d)
  1.1130 +    case empty
  1.1131 +    thus ?case unfolding subseq_def by auto
  1.1132 +  next
  1.1133 +    case (insert k d)
  1.1134 +    have k[intro]:"k\<in>Basis" using insert by auto
  1.1135      have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)" using `bounded (range f)`
  1.1136        by (auto intro!: bounded_linear_image bounded_linear_inner_left)
  1.1137      obtain l1::"'a" and r1 where r1:"subseq r1" and
  1.1138 @@ -3206,9 +3357,13 @@
  1.1139        using r1 and r2 unfolding r_def o_def subseq_def by auto
  1.1140      moreover
  1.1141      def l \<equiv> "(\<Sum>i\<in>Basis. (if i = k then l2 else l1\<bullet>i) *\<^sub>R i)::'a"
  1.1142 -    { fix e::real assume "e>0"
  1.1143 -      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
  1.1144 -      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially" by (rule tendstoD)
  1.1145 +    {
  1.1146 +      fix e::real
  1.1147 +      assume "e>0"
  1.1148 +      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
  1.1149 +        by blast
  1.1150 +      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially"
  1.1151 +        by (rule tendstoD)
  1.1152        from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
  1.1153          by (rule eventually_subseq)
  1.1154        have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
  1.1155 @@ -3226,47 +3381,58 @@
  1.1156    then obtain l::'a and r where r: "subseq r"
  1.1157      and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
  1.1158      using compact_lemma [OF f] by blast
  1.1159 -  { fix e::real assume "e>0"
  1.1160 -    hence "0 < e / real_of_nat DIM('a)" by (auto intro!: divide_pos_pos DIM_positive)
  1.1161 +  {
  1.1162 +    fix e::real
  1.1163 +    assume "e>0"
  1.1164 +    hence "0 < e / real_of_nat DIM('a)"
  1.1165 +      by (auto intro!: divide_pos_pos DIM_positive)
  1.1166      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"
  1.1167        by simp
  1.1168      moreover
  1.1169 -    { fix n assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
  1.1170 +    {
  1.1171 +      fix n
  1.1172 +      assume n: "\<forall>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i) < e / (real_of_nat DIM('a))"
  1.1173        have "dist (f (r n)) l \<le> (\<Sum>i\<in>Basis. dist (f (r n) \<bullet> i) (l \<bullet> i))"
  1.1174 -        apply(subst euclidean_dist_l2) using zero_le_dist by (rule setL2_le_setsum)
  1.1175 +        apply (subst euclidean_dist_l2)
  1.1176 +        using zero_le_dist
  1.1177 +        by (rule setL2_le_setsum)
  1.1178        also have "\<dots> < (\<Sum>i\<in>(Basis::'a set). e / (real_of_nat DIM('a)))"
  1.1179 -        apply(rule setsum_strict_mono) using n by auto
  1.1180 +        apply (rule setsum_strict_mono)
  1.1181 +        using n
  1.1182 +        by auto
  1.1183        finally have "dist (f (r n)) l < e" 
  1.1184          by auto
  1.1185      }
  1.1186      ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
  1.1187        by (rule eventually_elim1)
  1.1188    }
  1.1189 -  hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
  1.1190 -  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto
  1.1191 +  hence *: "((f \<circ> r) ---> l) sequentially"
  1.1192 +    unfolding o_def tendsto_iff by simp
  1.1193 +  with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially"
  1.1194 +    by auto
  1.1195  qed
  1.1196  
  1.1197  lemma bounded_fst: "bounded s \<Longrightarrow> bounded (fst ` s)"
  1.1198 -unfolding bounded_def
  1.1199 -apply clarify
  1.1200 -apply (rule_tac x="a" in exI)
  1.1201 -apply (rule_tac x="e" in exI)
  1.1202 -apply clarsimp
  1.1203 -apply (drule (1) bspec)
  1.1204 -apply (simp add: dist_Pair_Pair)
  1.1205 -apply (erule order_trans [OF real_sqrt_sum_squares_ge1])
  1.1206 -done
  1.1207 +  unfolding bounded_def
  1.1208 +  apply clarify
  1.1209 +  apply (rule_tac x="a" in exI)
  1.1210 +  apply (rule_tac x="e" in exI)
  1.1211 +  apply clarsimp
  1.1212 +  apply (drule (1) bspec)
  1.1213 +  apply (simp add: dist_Pair_Pair)
  1.1214 +  apply (erule order_trans [OF real_sqrt_sum_squares_ge1])
  1.1215 +  done
  1.1216  
  1.1217  lemma bounded_snd: "bounded s \<Longrightarrow> bounded (snd ` s)"
  1.1218 -unfolding bounded_def
  1.1219 -apply clarify
  1.1220 -apply (rule_tac x="b" in exI)
  1.1221 -apply (rule_tac x="e" in exI)
  1.1222 -apply clarsimp
  1.1223 -apply (drule (1) bspec)
  1.1224 -apply (simp add: dist_Pair_Pair)
  1.1225 -apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
  1.1226 -done
  1.1227 +  unfolding bounded_def
  1.1228 +  apply clarify
  1.1229 +  apply (rule_tac x="b" in exI)
  1.1230 +  apply (rule_tac x="e" in exI)
  1.1231 +  apply clarsimp
  1.1232 +  apply (drule (1) bspec)
  1.1233 +  apply (simp add: dist_Pair_Pair)
  1.1234 +  apply (erule order_trans [OF real_sqrt_sum_squares_ge2])
  1.1235 +  done
  1.1236  
  1.1237  instance prod :: (heine_borel, heine_borel) heine_borel
  1.1238  proof
  1.1239 @@ -3293,27 +3459,45 @@
  1.1240  
  1.1241  subsubsection{* Completeness *}
  1.1242  
  1.1243 -definition complete :: "'a::metric_space set \<Rightarrow> bool" where
  1.1244 -  "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
  1.1245 -
  1.1246 -lemma compact_imp_complete: assumes "compact s" shows "complete s"
  1.1247 -proof-
  1.1248 -  { fix f assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
  1.1249 +definition complete :: "'a::metric_space set \<Rightarrow> bool"
  1.1250 +  where "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f \<longrightarrow> (\<exists>l\<in>s. f ----> l))"
  1.1251 +
  1.1252 +lemma compact_imp_complete:
  1.1253 +  assumes "compact s"
  1.1254 +  shows "complete s"
  1.1255 +proof -
  1.1256 +  {
  1.1257 +    fix f
  1.1258 +    assume as: "(\<forall>n::nat. f n \<in> s)" "Cauchy f"
  1.1259      from as(1) obtain l r where lr: "l\<in>s" "subseq r" "(f \<circ> r) ----> l"
  1.1260        using assms unfolding compact_def by blast
  1.1261  
  1.1262      note lr' = seq_suble [OF lr(2)]
  1.1263  
  1.1264 -    { fix e::real assume "e>0"
  1.1265 -      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
  1.1266 -      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
  1.1267 -      { fix n::nat assume n:"n \<ge> max N M"
  1.1268 +    {
  1.1269 +      fix e::real
  1.1270 +      assume "e>0"
  1.1271 +      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"
  1.1272 +        unfolding cauchy_def
  1.1273 +        using `e>0` apply (erule_tac x="e/2" in allE)
  1.1274 +        apply auto
  1.1275 +        done
  1.1276 +      from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]]
  1.1277 +      obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2" using `e>0` by auto
  1.1278 +      {
  1.1279 +        fix n::nat
  1.1280 +        assume n:"n \<ge> max N M"
  1.1281          have "dist ((f \<circ> r) n) l < e/2" using n M by auto
  1.1282          moreover have "r n \<ge> N" using lr'[of n] n by auto
  1.1283          hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
  1.1284 -        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)  }
  1.1285 -      hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast  }
  1.1286 -    hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding LIMSEQ_def by auto  }
  1.1287 +        ultimately have "dist (f n) l < e"
  1.1288 +          using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute)
  1.1289 +      }
  1.1290 +      hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
  1.1291 +    }
  1.1292 +    hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s`
  1.1293 +      unfolding LIMSEQ_def by auto
  1.1294 +  }
  1.1295    thus ?thesis unfolding complete_def by auto
  1.1296  qed
  1.1297  
  1.1298 @@ -3436,16 +3620,25 @@
  1.1299  
  1.1300  lemma cauchy_imp_bounded: assumes "Cauchy s" shows "bounded (range s)"
  1.1301  proof-
  1.1302 -  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
  1.1303 +  from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1"
  1.1304 +    unfolding cauchy_def
  1.1305 +    apply (erule_tac x= 1 in allE)
  1.1306 +    apply auto
  1.1307 +    done
  1.1308    hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
  1.1309    moreover
  1.1310 -  have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto
  1.1311 +  have "bounded (s ` {0..N})"
  1.1312 +    using finite_imp_bounded[of "s ` {1..N}"] by auto
  1.1313    then obtain a where a:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> a"
  1.1314      unfolding bounded_any_center [where a="s N"] by auto
  1.1315    ultimately show "?thesis"
  1.1316      unfolding bounded_any_center [where a="s N"]
  1.1317 -    apply(rule_tac x="max a 1" in exI) apply auto
  1.1318 -    apply(erule_tac x=y in allE) apply(erule_tac x=y in ballE) by auto
  1.1319 +    apply (rule_tac x="max a 1" in exI)
  1.1320 +    apply auto
  1.1321 +    apply (erule_tac x=y in allE)
  1.1322 +    apply (erule_tac x=y in ballE)
  1.1323 +    apply auto
  1.1324 +    done
  1.1325  qed
  1.1326  
  1.1327  instance heine_borel < complete_space
  1.1328 @@ -3493,9 +3686,15 @@
  1.1329    assume ?lhs thus ?rhs by (rule complete_imp_closed)
  1.1330  next
  1.1331    assume ?rhs
  1.1332 -  { fix f assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
  1.1333 -    then obtain l where "(f ---> l) sequentially" using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
  1.1334 -    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  }
  1.1335 +  {
  1.1336 +    fix f
  1.1337 +    assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
  1.1338 +    then obtain l where "(f ---> l) sequentially"
  1.1339 +      using complete_univ[unfolded complete_def, THEN spec[where x=f]] by auto
  1.1340 +    hence "\<exists>l\<in>s. (f ---> l) sequentially"
  1.1341 +      using `?rhs`[unfolded closed_sequential_limits, THEN spec[where x=f], THEN spec[where x=l]]
  1.1342 +      using as(1) by auto
  1.1343 +  }
  1.1344    thus ?lhs unfolding complete_def by auto
  1.1345  qed
  1.1346  
  1.1347 @@ -3538,25 +3737,35 @@
  1.1348  
  1.1349  lemma bounded_closed_nest:
  1.1350    assumes "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
  1.1351 -  "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"  "bounded(s 0)"
  1.1352 +    "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"  "bounded(s 0)"
  1.1353    shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
  1.1354 -proof-
  1.1355 -  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
  1.1356 -  from assms(4,1) have *:"seq_compact (s 0)" using bounded_closed_imp_seq_compact[of "s 0"] by auto
  1.1357 +proof -
  1.1358 +  from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n"
  1.1359 +    using choice[of "\<lambda>n x. x\<in> s n"] by auto
  1.1360 +  from assms(4,1) have *:"seq_compact (s 0)"
  1.1361 +    using bounded_closed_imp_seq_compact[of "s 0"] by auto
  1.1362  
  1.1363    then obtain l r where lr:"l\<in>s 0" "subseq r" "((x \<circ> r) ---> l) sequentially"
  1.1364 -    unfolding seq_compact_def apply(erule_tac x=x in allE)  using x using assms(3) by blast
  1.1365 +    unfolding seq_compact_def
  1.1366 +    apply (erule_tac x=x in allE)
  1.1367 +    using x using assms(3)
  1.1368 +    apply blast
  1.1369 +    done
  1.1370  
  1.1371    { fix n::nat
  1.1372      { fix e::real assume "e>0"
  1.1373 -      with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e" unfolding LIMSEQ_def by auto
  1.1374 +      with lr(3) obtain N where N:"\<forall>m\<ge>N. dist ((x \<circ> r) m) l < e"
  1.1375 +        unfolding LIMSEQ_def by auto
  1.1376        hence "dist ((x \<circ> r) (max N n)) l < e" by auto
  1.1377        moreover
  1.1378        have "r (max N n) \<ge> n" using lr(2) using seq_suble[of r "max N n"] by auto
  1.1379        hence "(x \<circ> r) (max N n) \<in> s n"
  1.1380 -        using x apply(erule_tac x=n in allE)
  1.1381 -        using x apply(erule_tac x="r (max N n)" in allE)
  1.1382 -        using assms(3) apply(erule_tac x=n in allE) apply(erule_tac x="r (max N n)" in allE) by auto
  1.1383 +        using x apply (erule_tac x=n in allE)
  1.1384 +        using x apply (erule_tac x="r (max N n)" in allE)
  1.1385 +        using assms(3) apply (erule_tac x=n in allE)
  1.1386 +        apply (erule_tac x="r (max N n)" in allE)
  1.1387 +        apply auto
  1.1388 +        done
  1.1389        ultimately have "\<exists>y\<in>s n. dist y l < e" by auto
  1.1390      }
  1.1391      hence "l \<in> s n" using closed_approachable[of "s n" l] assms(1) by blast