merged
authorhuffman
Tue Jun 09 11:12:08 2009 -0700 (2009-06-09)
changeset 3153816068eb224c0
parent 31524 8abf99ab669c
parent 31537 feec2711da4e
child 31539 dc2662edd381
child 31558 e7a282113145
merged
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
     1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
     1.3 @@ -750,7 +750,7 @@
     1.4    using convex_Inter[unfolded Ball_def mem_def] by auto
     1.5  
     1.6  lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)"
     1.7 -proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def by auto
     1.8 +proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
     1.9    show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
    1.10      unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
    1.11      unfolding subset_eq mem_cball dist_norm using B by auto qed
    1.12 @@ -2018,7 +2018,7 @@
    1.13        case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm)
    1.14  	using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
    1.15      next guess a using UNIV_witness[where 'a = 'n] ..
    1.16 -      obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_def by auto
    1.17 +      obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
    1.18        hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis a" in ballE) defer apply(erule_tac x="basis a" in ballE)
    1.19  	unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def])
    1.20        case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
     2.3 @@ -1783,6 +1783,36 @@
     2.4    then show ?thesis using Kp by blast
     2.5  qed
     2.6  
     2.7 +lemma smult_conv_scaleR: "c *s x = scaleR c x"
     2.8 +  unfolding vector_scalar_mult_def vector_scaleR_def by simp
     2.9 +
    2.10 +lemma linear_conv_bounded_linear:
    2.11 +  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
    2.12 +  shows "linear f \<longleftrightarrow> bounded_linear f"
    2.13 +proof
    2.14 +  assume "linear f"
    2.15 +  show "bounded_linear f"
    2.16 +  proof
    2.17 +    fix x y show "f (x + y) = f x + f y"
    2.18 +      using `linear f` unfolding linear_def by simp
    2.19 +  next
    2.20 +    fix r x show "f (scaleR r x) = scaleR r (f x)"
    2.21 +      using `linear f` unfolding linear_def
    2.22 +      by (simp add: smult_conv_scaleR)
    2.23 +  next
    2.24 +    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
    2.25 +      using `linear f` by (rule linear_bounded)
    2.26 +    thus "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
    2.27 +      by (simp add: mult_commute)
    2.28 +  qed
    2.29 +next
    2.30 +  assume "bounded_linear f"
    2.31 +  then interpret f: bounded_linear f .
    2.32 +  show "linear f"
    2.33 +    unfolding linear_def smult_conv_scaleR
    2.34 +    by (simp add: f.add f.scaleR)
    2.35 +qed
    2.36 +
    2.37  subsection{* Bilinear functions. *}
    2.38  
    2.39  definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
    2.40 @@ -1886,6 +1916,41 @@
    2.41    with Kp show ?thesis by blast
    2.42  qed
    2.43  
    2.44 +lemma bilinear_conv_bounded_bilinear:
    2.45 +  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
    2.46 +  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
    2.47 +proof
    2.48 +  assume "bilinear h"
    2.49 +  show "bounded_bilinear h"
    2.50 +  proof
    2.51 +    fix x y z show "h (x + y) z = h x z + h y z"
    2.52 +      using `bilinear h` unfolding bilinear_def linear_def by simp
    2.53 +  next
    2.54 +    fix x y z show "h x (y + z) = h x y + h x z"
    2.55 +      using `bilinear h` unfolding bilinear_def linear_def by simp
    2.56 +  next
    2.57 +    fix r x y show "h (scaleR r x) y = scaleR r (h x y)"
    2.58 +      using `bilinear h` unfolding bilinear_def linear_def
    2.59 +      by (simp add: smult_conv_scaleR)
    2.60 +  next
    2.61 +    fix r x y show "h x (scaleR r y) = scaleR r (h x y)"
    2.62 +      using `bilinear h` unfolding bilinear_def linear_def
    2.63 +      by (simp add: smult_conv_scaleR)
    2.64 +  next
    2.65 +    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
    2.66 +      using `bilinear h` by (rule bilinear_bounded)
    2.67 +    thus "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
    2.68 +      by (simp add: mult_ac)
    2.69 +  qed
    2.70 +next
    2.71 +  assume "bounded_bilinear h"
    2.72 +  then interpret h: bounded_bilinear h .
    2.73 +  show "bilinear h"
    2.74 +    unfolding bilinear_def linear_conv_bounded_linear
    2.75 +    using h.bounded_linear_left h.bounded_linear_right
    2.76 +    by simp
    2.77 +qed
    2.78 +
    2.79  subsection{* Adjoints. *}
    2.80  
    2.81  definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
     3.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
     3.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
     3.3 @@ -969,8 +969,8 @@
     3.4    "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
     3.5  
     3.6  definition
     3.7 -  indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
     3.8 -  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
     3.9 +  indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
    3.10 +  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
    3.11  
    3.12  text{* Prove That They are all nets. *}
    3.13  
    3.14 @@ -1130,7 +1130,7 @@
    3.15    unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
    3.16  
    3.17  lemma Lim_at_infinity:
    3.18 -  "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
    3.19 +  "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
    3.20    by (auto simp add: tendsto_iff eventually_at_infinity)
    3.21  
    3.22  lemma Lim_sequentially:
    3.23 @@ -1141,10 +1141,8 @@
    3.24  lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
    3.25    unfolding Lim_sequentially LIMSEQ_def ..
    3.26  
    3.27 -lemma Lim_eventually:
    3.28 -  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
    3.29 -  shows "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    3.30 -  unfolding tendsto_iff by (auto elim: eventually_rev_mono)
    3.31 +lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
    3.32 +  by (rule topological_tendstoI, auto elim: eventually_rev_mono)
    3.33  
    3.34  text{* The expected monotonicity property. *}
    3.35  
    3.36 @@ -1172,31 +1170,32 @@
    3.37  text{* Interrelations between restricted and unrestricted limits. *}
    3.38  
    3.39  lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
    3.40 +  (* FIXME: rename *)
    3.41    unfolding tendsto_def Limits.eventually_within
    3.42    apply (clarify, drule spec, drule (1) mp, drule (1) mp)
    3.43    by (auto elim!: eventually_elim1)
    3.44  
    3.45  lemma Lim_within_open:
    3.46 -  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
    3.47 +  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
    3.48    assumes"a \<in> S" "open S"
    3.49    shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
    3.50  proof
    3.51    assume ?lhs
    3.52 -  { fix e::real assume "e>0"
    3.53 -    have "eventually (\<lambda>x. dist (f x) l < e) (at a within S)"
    3.54 -      using `?lhs` `e>0` by (rule tendstoD)
    3.55 -    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
    3.56 +  { fix A assume "open A" "l \<in> A"
    3.57 +    with `?lhs` have "eventually (\<lambda>x. f x \<in> A) (at a within S)"
    3.58 +      by (rule topological_tendstoD)
    3.59 +    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x \<in> A) (at a)"
    3.60        unfolding Limits.eventually_within .
    3.61 -    then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> dist (f x) l < e"
    3.62 +    then obtain T where "open T" "a \<in> T" "\<forall>x\<in>T. x \<noteq> a \<longrightarrow> x \<in> S \<longrightarrow> f x \<in> A"
    3.63        unfolding eventually_at_topological by fast
    3.64 -    hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> dist (f x) l < e"
    3.65 +    hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> f x \<in> A"
    3.66        using assms by auto
    3.67 -    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
    3.68 +    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> f x \<in> A)"
    3.69        by fast
    3.70 -    hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
    3.71 +    hence "eventually (\<lambda>x. f x \<in> A) (at a)"
    3.72        unfolding eventually_at_topological .
    3.73    }
    3.74 -  thus ?rhs by (rule tendstoI)
    3.75 +  thus ?rhs by (rule topological_tendstoI)
    3.76  next
    3.77    assume ?rhs
    3.78    thus ?lhs by (rule Lim_at_within)
    3.79 @@ -1242,25 +1241,12 @@
    3.80  lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
    3.81    assumes "(f ---> l) net" "linear h"
    3.82    shows "((\<lambda>x. h (f x)) ---> h l) net"
    3.83 -proof -
    3.84 -  obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x"
    3.85 -    using assms(2) using linear_bounded_pos[of h] by auto
    3.86 -  { fix e::real assume "e >0"
    3.87 -    hence "e/b > 0" using `b>0` by (metis divide_pos_pos)
    3.88 -    with `(f ---> l) net` have "eventually (\<lambda>x. dist (f x) l < e/b) net"
    3.89 -      by (rule tendstoD)
    3.90 -    then have "eventually (\<lambda>x. dist (h (f x)) (h l) < e) net"
    3.91 -      apply (rule eventually_rev_mono [rule_format])
    3.92 -      apply (simp add: dist_norm linear_sub [OF `linear h`, symmetric])
    3.93 -      apply (rule le_less_trans [OF b(2) [rule_format]])
    3.94 -      apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
    3.95 -      done
    3.96 -  }
    3.97 -  thus ?thesis unfolding tendsto_iff by simp
    3.98 -qed
    3.99 +using `linear h` `(f ---> l) net`
   3.100 +unfolding linear_conv_bounded_linear
   3.101 +by (rule bounded_linear.tendsto)
   3.102  
   3.103  lemma Lim_const: "((\<lambda>x. a) ---> a) net"
   3.104 -  unfolding tendsto_def by simp
   3.105 +  by (rule tendsto_const)
   3.106  
   3.107  lemma Lim_cmul:
   3.108    fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
   3.109 @@ -1274,34 +1260,16 @@
   3.110  lemma Lim_neg:
   3.111    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   3.112    shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
   3.113 -  apply (simp add: Lim dist_norm  group_simps)
   3.114 -  apply (subst minus_diff_eq[symmetric])
   3.115 -  unfolding norm_minus_cancel by simp
   3.116 +  by (rule tendsto_minus)
   3.117  
   3.118  lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
   3.119   "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
   3.120 -proof-
   3.121 -  assume as:"(f ---> l) net" "(g ---> m) net"
   3.122 -  { fix e::real
   3.123 -    assume "e>0"
   3.124 -    hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
   3.125 -            "eventually (\<lambda>x. dist (g x) m < e/2) net" using as
   3.126 -      by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
   3.127 -    hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
   3.128 -      apply (elim eventually_rev_mp)
   3.129 -      apply (rule always_eventually, clarify)
   3.130 -      apply (rule le_less_trans [OF dist_triangle_add])
   3.131 -      apply simp
   3.132 -      done
   3.133 -  }
   3.134 -  thus ?thesis unfolding tendsto_iff by simp
   3.135 -qed
   3.136 +  by (rule tendsto_add)
   3.137  
   3.138  lemma Lim_sub:
   3.139    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   3.140    shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
   3.141 -  unfolding diff_minus
   3.142 -  by (simp add: Lim_add Lim_neg)
   3.143 +  by (rule tendsto_diff)
   3.144  
   3.145  lemma Lim_null:
   3.146    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   3.147 @@ -1347,7 +1315,7 @@
   3.148    fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   3.149    assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   3.150    shows "(f ---> 0) net"
   3.151 -proof(simp add: tendsto_iff, rule+)
   3.152 +proof (rule tendstoI)
   3.153    fix e::real assume "e>0"
   3.154    { fix x
   3.155      assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
   3.156 @@ -1361,24 +1329,43 @@
   3.157  text{* Deducing things about the limit from the elements. *}
   3.158  
   3.159  lemma Lim_in_closed_set:
   3.160 -  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
   3.161 -  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net"  "\<not>(trivial_limit net)" "(f ---> l) net"
   3.162 +  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
   3.163    shows "l \<in> S"
   3.164  proof (rule ccontr)
   3.165    assume "l \<notin> S"
   3.166 -  obtain e where e:"e>0" "ball l e \<subseteq> UNIV - S" using assms(1) `l \<notin> S` unfolding closed_def open_contains_ball Compl_eq_Diff_UNIV by auto
   3.167 -  hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
   3.168 -  have "eventually (\<lambda>x. dist (f x) l < e) net"
   3.169 -    using assms(4) `e>0` by (rule tendstoD)
   3.170 -  with assms(2) have "eventually (\<lambda>x. f x \<in> S \<and> dist (f x) l < e) net"
   3.171 -    by (rule eventually_conjI)
   3.172 -  then obtain x where "f x \<in> S" "dist (f x) l < e"
   3.173 -    using assms(3) eventually_happens by auto
   3.174 -  with * show "False" by (simp add: dist_commute)
   3.175 +  with `closed S` have "open (- S)" "l \<in> - S"
   3.176 +    by (simp_all add: open_Compl)
   3.177 +  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) net"
   3.178 +    by (rule topological_tendstoD)
   3.179 +  with assms(2) have "eventually (\<lambda>x. False) net"
   3.180 +    by (rule eventually_elim2) simp
   3.181 +  with assms(3) show "False"
   3.182 +    by (simp add: eventually_False)
   3.183  qed
   3.184  
   3.185  text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
   3.186  
   3.187 +lemma Lim_dist_ubound:
   3.188 +  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
   3.189 +  shows "dist a l <= e"
   3.190 +proof (rule ccontr)
   3.191 +  assume "\<not> dist a l \<le> e"
   3.192 +  then have "0 < dist a l - e" by simp
   3.193 +  with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
   3.194 +    by (rule tendstoD)
   3.195 +  with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
   3.196 +    by (rule eventually_conjI)
   3.197 +  then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
   3.198 +    using assms(1) eventually_happens by auto
   3.199 +  hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
   3.200 +    by (rule add_le_less_mono)
   3.201 +  hence "dist a (f w) + dist (f w) l < dist a l"
   3.202 +    by simp
   3.203 +  also have "\<dots> \<le> dist a (f w) + dist (f w) l"
   3.204 +    by (rule dist_triangle)
   3.205 +  finally show False by simp
   3.206 +qed
   3.207 +
   3.208  lemma Lim_norm_ubound:
   3.209    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   3.210    assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
   3.211 @@ -1453,76 +1440,15 @@
   3.212    shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
   3.213    unfolding Lim_def using Lim_unique[of net f] by auto
   3.214  
   3.215 -text{* Limit under bilinear function (surprisingly tedious, but important) *}
   3.216 -
   3.217 -lemma norm_bound_lemma:
   3.218 -  "0 < e \<Longrightarrow> \<exists>d>0. \<forall>(x'::real^'b::finite) y'::real^'a::finite. norm(x' - (x::real^'b)) < d \<and> norm(y' - y) < d \<longrightarrow> norm(x') * norm(y' - y) + norm(x' - x) * norm(y) < e"
   3.219 -proof-
   3.220 -  assume e: "0 < e"
   3.221 -  have th1: "(2 * norm x + 2 * norm y + 2) > 0" using norm_ge_zero[of x] norm_ge_zero[of y] by norm
   3.222 -  hence th0: "0 < e / (2 * norm x + 2 * norm y + 2)"  using `e>0` using divide_pos_pos by auto
   3.223 -  moreover
   3.224 -  { fix x' y'
   3.225 -    assume h: "norm (x' - x) < 1" "norm (x' - x) < e / (2 * norm x + 2 * norm y + 2)"
   3.226 -      "norm (y' - y) < 1" "norm (y' - y) < e / (2 * norm x + 2 * norm y + 2)"
   3.227 -    have th: "\<And>a b (c::real). a \<ge> 0 \<Longrightarrow> c \<ge> 0 \<Longrightarrow> a + (b + c) < e ==> b < e " by arith
   3.228 -    from h have thx: "norm (x' - x) * norm y < e / 2"
   3.229 -      using th0 th1 apply (simp add: field_simps)
   3.230 -      apply (rule th) defer defer apply assumption
   3.231 -      by (simp_all add: norm_ge_zero zero_le_mult_iff)
   3.232 -
   3.233 -    have "norm x' - norm x < 1" apply(rule le_less_trans)
   3.234 -      using h(1) using norm_triangle_ineq2[of x' x] by auto
   3.235 -    hence *:"norm x' < 1 + norm x"  by auto
   3.236 -
   3.237 -    have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
   3.238 -      using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
   3.239 -    also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
   3.240 -      using th1 th0 `e>0` by auto
   3.241 -
   3.242 -    finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
   3.243 -      using thx and e by (simp add: field_simps)  }
   3.244 -  ultimately show ?thesis apply(rule_tac x="min 1 (e / 2 / (norm x + norm y + 1))" in exI) by auto
   3.245 -qed
   3.246 +text{* Limit under bilinear function *}
   3.247  
   3.248  lemma Lim_bilinear:
   3.249    fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
   3.250    assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
   3.251    shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
   3.252 -proof -
   3.253 -  obtain B where "B>0" and B:"\<forall>x y. norm (h x y) \<le> B * norm x * norm y" using bilinear_bounded_pos[OF assms(3)] by auto
   3.254 -  { fix e::real assume "e>0"
   3.255 -    obtain d where "d>0" and d:"\<forall>x' y'. norm (x' - l) < d \<and> norm (y' - m) < d \<longrightarrow> norm x' * norm (y' - m) + norm (x' - l) * norm m < e / B" using `B>0` `e>0`
   3.256 -      using norm_bound_lemma[of "e / B" l m] using divide_pos_pos by auto
   3.257 -
   3.258 -    have *:"\<And>x y. h (f x) (g x) - h l m = h (f x) (g x - m) + h (f x - l) m"
   3.259 -      unfolding bilinear_rsub[OF assms(3)]
   3.260 -      unfolding bilinear_lsub[OF assms(3)] by auto
   3.261 -
   3.262 -    have "eventually (\<lambda>x. dist (f x) l < d) net"
   3.263 -      using assms(1) `d>0` by (rule tendstoD)
   3.264 -    moreover
   3.265 -    have "eventually (\<lambda>x. dist (g x) m < d) net"
   3.266 -      using assms(2) `d>0` by (rule tendstoD)
   3.267 -    ultimately
   3.268 -    have "eventually (\<lambda>x. dist (f x) l < d \<and> dist (g x) m < d) net"
   3.269 -      by (rule eventually_conjI)
   3.270 -    moreover
   3.271 -    { fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
   3.272 -      hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
   3.273 -	using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm  by auto
   3.274 -      have "norm (h (f x) (g x - m)) + norm (h (f x - l) m) \<le> B * norm (f x) * norm (g x - m) + B * norm (f x - l) * norm m"
   3.275 -	using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]]
   3.276 -	using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto
   3.277 -      also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
   3.278 -      finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
   3.279 -    }
   3.280 -    ultimately have "eventually (\<lambda>x. dist (h (f x) (g x)) (h l m) < e) net"
   3.281 -      by (auto elim: eventually_rev_mono)
   3.282 -  }
   3.283 -  thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
   3.284 -    unfolding tendsto_iff by simp
   3.285 -qed
   3.286 +using `bilinear h` `(f ---> l) net` `(g ---> m) net`
   3.287 +unfolding bilinear_conv_bounded_bilinear
   3.288 +by (rule bounded_bilinear.tendsto)
   3.289  
   3.290  text{* These are special for limits out of the same vector space. *}
   3.291  
   3.292 @@ -1535,31 +1461,41 @@
   3.293  
   3.294  lemma Lim_at_zero:
   3.295    fixes a :: "'a::real_normed_vector"
   3.296 -  fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
   3.297 +  fixes l :: "'b::topological_space"
   3.298    shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
   3.299  proof
   3.300    assume "?lhs"
   3.301 -  { fix e::real assume "e>0"
   3.302 -    with `?lhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" unfolding Lim_at by auto
   3.303 -    { fix x::"'a" assume "0 < dist x 0 \<and> dist x 0 < d"
   3.304 -      hence "dist (f (a + x)) l < e" using d
   3.305 -      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
   3.306 +  { fix S assume "open S" "l \<in> S"
   3.307 +    with `?lhs` have "eventually (\<lambda>x. f x \<in> S) (at a)"
   3.308 +      by (rule topological_tendstoD)
   3.309 +    then obtain d where d: "d>0" "\<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S"
   3.310 +      unfolding Limits.eventually_at by fast
   3.311 +    { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
   3.312 +      hence "f (a + x) \<in> S" using d
   3.313 +      apply(erule_tac x="x+a" in allE)
   3.314 +      by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
   3.315      }
   3.316 -    hence "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e" using d(1) by auto
   3.317 +    hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
   3.318 +      using d(1) by auto
   3.319 +    hence "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
   3.320 +      unfolding Limits.eventually_at .
   3.321    }
   3.322 -  thus "?rhs" unfolding Lim_at by auto
   3.323 +  thus "?rhs" by (rule topological_tendstoI)
   3.324  next
   3.325    assume "?rhs"
   3.326 -  { fix e::real assume "e>0"
   3.327 -    with `?rhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e"
   3.328 -      unfolding Lim_at by auto
   3.329 -    { fix x::"'a" assume "0 < dist x a \<and> dist x a < d"
   3.330 -      hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
   3.331 +  { fix S assume "open S" "l \<in> S"
   3.332 +    with `?rhs` have "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
   3.333 +      by (rule topological_tendstoD)
   3.334 +    then obtain d where d: "d>0" "\<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
   3.335 +      unfolding Limits.eventually_at by fast
   3.336 +    { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
   3.337 +      hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
   3.338  	by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
   3.339      }
   3.340 -    hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using d(1) by auto
   3.341 +    hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
   3.342 +    hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
   3.343    }
   3.344 -  thus "?lhs" unfolding Lim_at by auto
   3.345 +  thus "?lhs" by (rule topological_tendstoI)
   3.346  qed
   3.347  
   3.348  text{* It's also sometimes useful to extract the limit point from the net.  *}
   3.349 @@ -1615,10 +1551,9 @@
   3.350  qed
   3.351  
   3.352  lemma Lim_transform_eventually:
   3.353 -  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
   3.354 -  shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   3.355 -  unfolding tendsto_iff
   3.356 -  apply (clarify, drule spec, drule (1) mp)
   3.357 +  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
   3.358 +  apply (rule topological_tendstoI)
   3.359 +  apply (drule (2) topological_tendstoD)
   3.360    apply (erule (1) eventually_elim2, simp)
   3.361    done
   3.362  
   3.363 @@ -1743,17 +1678,19 @@
   3.364    by (metis trans_le_add1 )
   3.365  
   3.366  lemma seq_offset_neg:
   3.367 -  fixes l :: "'a::metric_space" (* TODO: generalize *)
   3.368 -  shows "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   3.369 -  apply (simp add: Lim_sequentially)
   3.370 +  "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
   3.371 +  apply (rule topological_tendstoI)
   3.372 +  apply (drule (2) topological_tendstoD)
   3.373 +  apply (simp only: eventually_sequentially)
   3.374    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
   3.375    apply metis
   3.376    by arith
   3.377  
   3.378  lemma seq_offset_rev:
   3.379 -  fixes l :: "'a::metric_space" (* TODO: generalize *)
   3.380 -  shows "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   3.381 -  apply (simp add: Lim_sequentially)
   3.382 +  "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
   3.383 +  apply (rule topological_tendstoI)
   3.384 +  apply (drule (2) topological_tendstoD)
   3.385 +  apply (simp only: eventually_sequentially)
   3.386    apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
   3.387    by metis arith
   3.388  
   3.389 @@ -1770,7 +1707,7 @@
   3.390  text{* More properties of closed balls. *}
   3.391  
   3.392  lemma closed_cball: "closed (cball x e)"
   3.393 -unfolding cball_def closed_def Compl_eq_Diff_UNIV [symmetric]
   3.394 +unfolding cball_def closed_def
   3.395  unfolding Collect_neg_eq [symmetric] not_le
   3.396  apply (clarsimp simp add: open_dist, rename_tac y)
   3.397  apply (rule_tac x="dist x y - e" in exI, clarsimp)
   3.398 @@ -1802,7 +1739,6 @@
   3.399  
   3.400  lemma islimpt_ball:
   3.401    fixes x y :: "'a::{real_normed_vector,perfect_space}"
   3.402 -    (* FIXME: generalize to metric_space *)
   3.403    shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
   3.404  proof
   3.405    assume "?lhs"
   3.406 @@ -1810,7 +1746,7 @@
   3.407      hence *:"ball x e = {}" using ball_eq_empty[of x e] by auto
   3.408      have False using `?lhs` unfolding * using islimpt_EMPTY[of y] by auto
   3.409    }
   3.410 -  hence "e > 0" by (metis dlo_simps(3))
   3.411 +  hence "e > 0" by (metis not_less)
   3.412    moreover
   3.413    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
   3.414    ultimately show "?rhs" by auto
   3.415 @@ -1869,12 +1805,56 @@
   3.416    thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto
   3.417  qed
   3.418  
   3.419 +lemma closure_ball_lemma:
   3.420 +  fixes x y :: "'a::real_normed_vector"
   3.421 +  assumes "x \<noteq> y" shows "y islimpt ball x (dist x y)"
   3.422 +proof (rule islimptI)
   3.423 +  fix T assume "y \<in> T" "open T"
   3.424 +  then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
   3.425 +    unfolding open_dist by fast
   3.426 +  (* choose point between x and y, within distance r of y. *)
   3.427 +  def k \<equiv> "min 1 (r / (2 * dist x y))"
   3.428 +  def z \<equiv> "y + scaleR k (x - y)"
   3.429 +  have z_def2: "z = x + scaleR (1 - k) (y - x)"
   3.430 +    unfolding z_def by (simp add: algebra_simps)
   3.431 +  have "dist z y < r"
   3.432 +    unfolding z_def k_def using `0 < r`
   3.433 +    by (simp add: dist_norm norm_scaleR min_def)
   3.434 +  hence "z \<in> T" using `\<forall>z. dist z y < r \<longrightarrow> z \<in> T` by simp
   3.435 +  have "dist x z < dist x y"
   3.436 +    unfolding z_def2 dist_norm
   3.437 +    apply (simp add: norm_scaleR norm_minus_commute)
   3.438 +    apply (simp only: dist_norm [symmetric])
   3.439 +    apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
   3.440 +    apply (rule mult_strict_right_mono)
   3.441 +    apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \<noteq> y`)
   3.442 +    apply (simp add: zero_less_dist_iff `x \<noteq> y`)
   3.443 +    done
   3.444 +  hence "z \<in> ball x (dist x y)" by simp
   3.445 +  have "z \<noteq> y"
   3.446 +    unfolding z_def k_def using `x \<noteq> y` `0 < r`
   3.447 +    by (simp add: min_def)
   3.448 +  show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
   3.449 +    using `z \<in> ball x (dist x y)` `z \<in> T` `z \<noteq> y`
   3.450 +    by fast
   3.451 +qed
   3.452 +
   3.453  lemma closure_ball:
   3.454 -  fixes x y :: "'a::{real_normed_vector,perfect_space}"
   3.455 -    (* FIXME: generalize to metric_space *)
   3.456 -  shows "0 < e ==> (closure(ball x e) = cball x e)"
   3.457 -  apply (simp add: closure_def islimpt_ball expand_set_eq)
   3.458 -  by arith
   3.459 +  fixes x :: "'a::real_normed_vector"
   3.460 +  shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
   3.461 +apply (rule equalityI)
   3.462 +apply (rule closure_minimal)
   3.463 +apply (rule ball_subset_cball)
   3.464 +apply (rule closed_cball)
   3.465 +apply (rule subsetI, rename_tac y)
   3.466 +apply (simp add: le_less [where 'a=real])
   3.467 +apply (erule disjE)
   3.468 +apply (rule subsetD [OF closure_subset], simp)
   3.469 +apply (simp add: closure_def)
   3.470 +apply clarify
   3.471 +apply (rule closure_ball_lemma)
   3.472 +apply (simp add: zero_less_dist_iff)
   3.473 +done
   3.474  
   3.475  lemma interior_cball:
   3.476    fixes x :: "real ^ _" (* FIXME: generalize *)
   3.477 @@ -1962,24 +1942,30 @@
   3.478  text{* For points in the interior, localization of limits makes no difference.   *}
   3.479  
   3.480  lemma eventually_within_interior:
   3.481 -  fixes x :: "'a::metric_space"
   3.482    assumes "x \<in> interior S"
   3.483    shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
   3.484  proof-
   3.485 -  from assms obtain e where e:"e>0" "\<forall>y. dist x y < e \<longrightarrow> y \<in> S" unfolding mem_interior ball_def subset_eq by auto
   3.486 -  { assume "?lhs" then obtain d where "d>0" "\<forall>xa\<in>S. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa" unfolding eventually_within by auto
   3.487 -    hence "?rhs" unfolding eventually_at using e by (auto simp add: dist_commute intro!: add exI[of _ "min e d"])
   3.488 +  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
   3.489 +    unfolding interior_def by fast
   3.490 +  { assume "?lhs"
   3.491 +    then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
   3.492 +      unfolding Limits.eventually_within Limits.eventually_at_topological
   3.493 +      by auto
   3.494 +    with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
   3.495 +      by auto
   3.496 +    then have "?rhs"
   3.497 +      unfolding Limits.eventually_at_topological by auto
   3.498    } moreover
   3.499 -  { assume "?rhs" hence "?lhs" unfolding eventually_within eventually_at by auto
   3.500 +  { assume "?rhs" hence "?lhs"
   3.501 +      unfolding Limits.eventually_within
   3.502 +      by (auto elim: eventually_elim1)
   3.503    } ultimately
   3.504 -  show "?thesis" by auto
   3.505 +  show "?thesis" ..
   3.506  qed
   3.507  
   3.508  lemma lim_within_interior:
   3.509 -  fixes x :: "'a::metric_space"
   3.510 -  fixes l :: "'b::metric_space" (* TODO: generalize *)
   3.511 -  shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
   3.512 -  by (simp add: tendsto_iff eventually_within_interior)
   3.513 +  "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
   3.514 +  unfolding tendsto_def by (simp add: eventually_within_interior)
   3.515  
   3.516  lemma netlimit_within_interior:
   3.517    fixes x :: "'a::{perfect_space, real_normed_vector}"
   3.518 @@ -1996,8 +1982,21 @@
   3.519  
   3.520    (* FIXME: This has to be unified with BSEQ!! *)
   3.521  definition
   3.522 -  bounded :: "'a::real_normed_vector set \<Rightarrow> bool" where
   3.523 -  "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x <= a)"
   3.524 +  bounded :: "'a::metric_space set \<Rightarrow> bool" where
   3.525 +  "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
   3.526 +
   3.527 +lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
   3.528 +unfolding bounded_def
   3.529 +apply safe
   3.530 +apply (rule_tac x="dist a x + e" in exI, clarify)
   3.531 +apply (drule (1) bspec)
   3.532 +apply (erule order_trans [OF dist_triangle add_left_mono])
   3.533 +apply auto
   3.534 +done
   3.535 +
   3.536 +lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
   3.537 +unfolding bounded_any_center [where a=0]
   3.538 +by (simp add: dist_norm)
   3.539  
   3.540  lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
   3.541  lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
   3.542 @@ -2008,16 +2007,17 @@
   3.543  
   3.544  lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)"
   3.545  proof-
   3.546 -  from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto
   3.547 -  { fix x assume "x\<in>closure S"
   3.548 -    then obtain xa where xa:"\<forall>n. xa n \<in> S"  "(xa ---> x) sequentially" unfolding closure_sequential by auto
   3.549 -    have "\<forall>n. xa n \<in> S \<longrightarrow> norm (xa n) \<le> a" using a by simp
   3.550 -    hence "eventually (\<lambda>n. norm (xa n) \<le> a) sequentially"
   3.551 -      by (rule eventually_mono, simp add: xa(1))
   3.552 -    have "norm x \<le> a"
   3.553 -      apply (rule Lim_norm_ubound[of sequentially xa x a])
   3.554 +  from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" unfolding bounded_def by auto
   3.555 +  { fix y assume "y \<in> closure S"
   3.556 +    then obtain f where f: "\<forall>n. f n \<in> S"  "(f ---> y) sequentially"
   3.557 +      unfolding closure_sequential by auto
   3.558 +    have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
   3.559 +    hence "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
   3.560 +      by (rule eventually_mono, simp add: f(1))
   3.561 +    have "dist x y \<le> a"
   3.562 +      apply (rule Lim_dist_ubound [of sequentially f])
   3.563        apply (rule trivial_limit_sequentially)
   3.564 -      apply (rule xa(2))
   3.565 +      apply (rule f(2))
   3.566        apply fact
   3.567        done
   3.568    }
   3.569 @@ -2026,11 +2026,9 @@
   3.570  
   3.571  lemma bounded_cball[simp,intro]: "bounded (cball x e)"
   3.572    apply (simp add: bounded_def)
   3.573 -  apply (rule exI[where x="norm x + e"])
   3.574 -  apply (clarsimp simp add: Ball_def dist_norm, rename_tac y)
   3.575 -  apply (subgoal_tac "norm y - norm x \<le> e", simp)
   3.576 -  apply (rule order_trans [OF norm_triangle_ineq2])
   3.577 -  apply (simp add: norm_minus_commute)
   3.578 +  apply (rule_tac x=x in exI)
   3.579 +  apply (rule_tac x=e in exI)
   3.580 +  apply auto
   3.581    done
   3.582  
   3.583  lemma bounded_ball[simp,intro]: "bounded(ball x e)"
   3.584 @@ -2038,22 +2036,31 @@
   3.585  
   3.586  lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
   3.587  proof-
   3.588 -  { fix x F assume as:"bounded F"
   3.589 -    then obtain a where "\<forall>x\<in>F. norm x \<le> a" unfolding bounded_def by auto
   3.590 -    hence "bounded (insert x F)" unfolding bounded_def by(auto intro!: add exI[of _ "max a (norm x)"])
   3.591 +  { fix a F assume as:"bounded F"
   3.592 +    then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
   3.593 +    hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
   3.594 +    hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
   3.595    }
   3.596    thus ?thesis using finite_induct[of S bounded]  using bounded_empty assms by auto
   3.597  qed
   3.598  
   3.599  lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
   3.600    apply (auto simp add: bounded_def)
   3.601 -  by (rule_tac x="max a aa" in exI, auto)
   3.602 +  apply (rename_tac x y r s)
   3.603 +  apply (rule_tac x=x in exI)
   3.604 +  apply (rule_tac x="max r (dist x y + s)" in exI)
   3.605 +  apply (rule ballI, rename_tac z, safe)
   3.606 +  apply (drule (1) bspec, simp)
   3.607 +  apply (drule (1) bspec)
   3.608 +  apply (rule min_max.le_supI2)
   3.609 +  apply (erule order_trans [OF dist_triangle add_left_mono])
   3.610 +  done
   3.611  
   3.612  lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
   3.613    by (induct rule: finite_induct[of F], auto)
   3.614  
   3.615  lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
   3.616 -  apply (simp add: bounded_def)
   3.617 +  apply (simp add: bounded_iff)
   3.618    apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
   3.619    by metis arith
   3.620  
   3.621 @@ -2067,13 +2074,16 @@
   3.622  lemma bounded_insert[intro]:"bounded(insert x S) \<longleftrightarrow> bounded S"
   3.623    by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI)
   3.624  
   3.625 -lemma bot_bounded_UNIV[simp, intro]: "~(bounded (UNIV:: (real^'n::finite) set))"
   3.626 +lemma not_bounded_UNIV[simp, intro]:
   3.627 +  "\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
   3.628  proof(auto simp add: bounded_pos not_le)
   3.629 +  obtain x :: 'a where "x \<noteq> 0"
   3.630 +    using perfect_choose_dist [OF zero_less_one] by fast
   3.631    fix b::real  assume b: "b >0"
   3.632    have b1: "b +1 \<ge> 0" using b by simp
   3.633 -  then obtain x:: "real^'n" where "norm x = b + 1" using vector_choose_size[of "b+1"] by blast
   3.634 -  hence "norm x > b" using b by simp
   3.635 -  then show "\<exists>(x::real^'n). b < norm x"  by blast
   3.636 +  with `x \<noteq> 0` have "b < norm (scaleR (b + 1) (sgn x))"
   3.637 +    by (simp add: norm_scaleR norm_sgn)
   3.638 +  then show "\<exists>x::'a. b < norm x" ..
   3.639  qed
   3.640  
   3.641  lemma bounded_linear_image:
   3.642 @@ -2098,7 +2108,9 @@
   3.643    apply (rule bounded_linear_image, assumption)
   3.644    by (rule linear_compose_cmul, rule linear_id[unfolded id_def])
   3.645  
   3.646 -lemma bounded_translation: assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
   3.647 +lemma bounded_translation:
   3.648 +  fixes S :: "'a::real_normed_vector set"
   3.649 +  assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
   3.650  proof-
   3.651    from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
   3.652    { fix x assume "x\<in>S"
   3.653 @@ -2114,7 +2126,7 @@
   3.654  lemma bounded_vec1:
   3.655    fixes S :: "real set"
   3.656    shows "bounded(vec1 ` S) \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
   3.657 -  by (simp add: bounded_def forall_vec1 norm_vec1 vec1_in_image_vec1)
   3.658 +  by (simp add: bounded_iff forall_vec1 norm_vec1 vec1_in_image_vec1)
   3.659  
   3.660  lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \<noteq> {}"
   3.661    shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
   3.662 @@ -2208,6 +2220,30 @@
   3.663     (\<forall>f. (\<forall>n::nat. f n \<in> S) \<longrightarrow>
   3.664         (\<exists>l\<in>S. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f o r) ---> l) sequentially))"
   3.665  
   3.666 +text {*
   3.667 +  A metric space (or topological vector space) is said to have the
   3.668 +  Heine-Borel property if every closed and bounded subset is compact.
   3.669 +*}
   3.670 +
   3.671 +class heine_borel =
   3.672 +  assumes bounded_imp_convergent_subsequence:
   3.673 +    "bounded s \<Longrightarrow> \<forall>n::nat. f n \<in> s
   3.674 +      \<Longrightarrow> \<exists>l r. (\<forall>m n. m < n --> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially"
   3.675 +
   3.676 +lemma bounded_closed_imp_compact:
   3.677 +  fixes s::"'a::heine_borel set"
   3.678 +  assumes "bounded s" and "closed s" shows "compact s"
   3.679 +proof (unfold compact_def, clarify)
   3.680 +  fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
   3.681 +  obtain l r where r: "\<forall>m n. m < n \<longrightarrow> r m < r n" and l: "((f \<circ> r) ---> l) sequentially"
   3.682 +    using bounded_imp_convergent_subsequence [OF `bounded s` `\<forall>n. f n \<in> s`] by auto
   3.683 +  from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp
   3.684 +  have "l \<in> s" using `closed s` fr l
   3.685 +    unfolding closed_sequential_limits by blast
   3.686 +  show "\<exists>l\<in>s. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially"
   3.687 +    using `l \<in> s` r l by blast
   3.688 +qed
   3.689 +
   3.690  lemma monotone_bigger: fixes r::"nat\<Rightarrow>nat"
   3.691    assumes "\<forall>m n::nat. m < n --> r m < r n"
   3.692    shows "n \<le> r n"
   3.693 @@ -2219,6 +2255,12 @@
   3.694    ultimately show "Suc n \<le> r (Suc n)" by auto
   3.695  qed
   3.696  
   3.697 +lemma eventually_subsequence:
   3.698 +  assumes r: "\<forall>m n. m < n \<longrightarrow> r m < r n"
   3.699 +  shows "eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
   3.700 +unfolding eventually_sequentially
   3.701 +by (metis monotone_bigger [OF r] le_trans)
   3.702 +
   3.703  lemma lim_subsequence:
   3.704    fixes l :: "'a::metric_space" (* TODO: generalize *)
   3.705    shows "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
   3.706 @@ -2264,87 +2306,97 @@
   3.707    unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto
   3.708  
   3.709  lemma compact_real_lemma:
   3.710 - assumes "\<forall>n::nat. abs(s n) \<le> b"
   3.711 -  shows "\<exists>l r. (\<forall>m n::nat. m < n --> r m < r n) \<and>
   3.712 -           (\<forall>e>0::real. \<exists>N. \<forall>n\<ge>N. (abs(s (r n) - l) < e))"
   3.713 +  assumes "\<forall>n::nat. abs(s n) \<le> b"
   3.714 +  shows "\<exists>(l::real) r. (\<forall>m n::nat. m < n --> r m < r n) \<and> ((s \<circ> r) ---> l) sequentially"
   3.715  proof-
   3.716    obtain r where r:"\<forall>m n::nat. m < n \<longrightarrow> r m < r n"
   3.717      "(\<forall>m n. m \<le> n \<longrightarrow> s (r m) \<le> s (r n)) \<or> (\<forall>m n. m \<le> n \<longrightarrow> s (r n) \<le> s (r m))"
   3.718      using seq_monosub[of s] by (auto simp add: subseq_def monoseq_def)
   3.719 -  thus ?thesis using convergent_bounded_monotone[of "s o r" b] and assms by auto
   3.720 -qed
   3.721 +  thus ?thesis using convergent_bounded_monotone[of "s o r" b] and assms
   3.722 +    unfolding tendsto_iff dist_norm eventually_sequentially by auto
   3.723 +qed
   3.724 +
   3.725 +instance real :: heine_borel
   3.726 +proof
   3.727 +  fix s :: "real set" and f :: "nat \<Rightarrow> real"
   3.728 +  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
   3.729 +  then obtain b where b: "\<forall>n. abs (f n) \<le> b"
   3.730 +    unfolding bounded_iff by auto
   3.731 +  obtain l :: real and r :: "nat \<Rightarrow> nat" where
   3.732 +    r: "\<forall>m n. m < n \<longrightarrow> r m < r n" and l: "((f \<circ> r) ---> l) sequentially"
   3.733 +    using compact_real_lemma [OF b] by auto
   3.734 +  thus "\<exists>l r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially"
   3.735 +    by auto
   3.736 +qed
   3.737 +
   3.738 +lemma bounded_component: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
   3.739 +unfolding bounded_def
   3.740 +apply clarify
   3.741 +apply (rule_tac x="x $ i" in exI)
   3.742 +apply (rule_tac x="e" in exI)
   3.743 +apply clarify
   3.744 +apply (rule order_trans [OF dist_nth_le], simp)
   3.745 +done
   3.746  
   3.747  lemma compact_lemma:
   3.748 -  assumes "bounded s" and "\<forall>n. (x::nat \<Rightarrow>real^'a::finite) n \<in> s"
   3.749 +  fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n::finite"
   3.750 +  assumes "bounded s" and "\<forall>n. f n \<in> s"
   3.751    shows "\<forall>d.
   3.752 -        \<exists>l::(real^'a::finite). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
   3.753 -        (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
   3.754 -proof-
   3.755 -  obtain b where b:"\<forall>x\<in>s. norm x \<le> b" using assms(1)[unfolded bounded_def] by auto
   3.756 -  { { fix i::'a
   3.757 -      { fix n::nat
   3.758 -	have "\<bar>x n $ i\<bar> \<le> b" using b[THEN bspec[where x="x n"]] and component_le_norm[of "x n" i] and assms(2)[THEN spec[where x=n]] by auto }
   3.759 -      hence "\<forall>n. \<bar>x n $ i\<bar> \<le> b" by auto
   3.760 -    } note b' = this
   3.761 -
   3.762 -    fix d::"'a set" have "finite d" by simp
   3.763 -    hence "\<exists>l::(real^'a). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
   3.764 -        (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
   3.765 -    proof(induct d) case empty thus ?case by auto
   3.766 -    next case (insert k d)
   3.767 -	obtain l1::"real^'a" and r1 where r1:"\<forall>n m::nat. m < n \<longrightarrow> r1 m < r1 n" and lr1:"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r1 n) $ i - l1 $ i\<bar> < e"
   3.768 -	  using insert(3) by auto
   3.769 -	obtain l2 r2 where r2:"\<forall>m n::nat. m < n \<longrightarrow> r2 m < r2 n" and lr2:"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>(x \<circ> r1) (r2 n) $ k - l2\<bar> < e"
   3.770 -	  using b'[of k] and compact_real_lemma[of "\<lambda>i. ((x \<circ> r1) i)$k" b] by auto
   3.771 -	def r \<equiv> "r1 \<circ> r2" have r:"\<forall>m n. m < n \<longrightarrow> r m < r n" unfolding r_def o_def using r1 and r2 by auto
   3.772 -	moreover
   3.773 -	def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::real^'a"
   3.774 -	{ fix e::real assume "e>0"
   3.775 -	  from lr1 obtain N1 where N1:"\<forall>n\<ge>N1. \<forall>i\<in>d. \<bar>x (r1 n) $ i - l1 $ i\<bar> < e" using `e>0` by blast
   3.776 -	  from lr2 obtain N2 where N2:"\<forall>n\<ge>N2. \<bar>(x \<circ> r1) (r2 n) $ k - l2\<bar> < e" using `e>0` by blast
   3.777 -	  { fix n assume n:"n\<ge> N1 + N2"
   3.778 -	    fix i assume i:"i\<in>(insert k d)"
   3.779 -	    hence "\<bar>x (r n) $ i - l $ i\<bar> < e"
   3.780 -	      using N2[THEN spec[where x="n"]] and n
   3.781 - 	      using N1[THEN spec[where x="r2 n"]] and n
   3.782 -	      using monotone_bigger[OF r] and i
   3.783 -	      unfolding l_def and r_def
   3.784 -	      using monotone_bigger[OF r2, of n] by auto  }
   3.785 -	  hence "\<exists>N. \<forall>n\<ge>N. \<forall>i\<in>(insert k d). \<bar>x (r n) $ i - l $ i\<bar> < e" by blast	}
   3.786 -	ultimately show ?case by auto
   3.787 -    qed  }
   3.788 -  thus ?thesis by auto
   3.789 -qed
   3.790 -
   3.791 -lemma bounded_closed_imp_compact: fixes s::"(real^'a::finite) set"
   3.792 -  assumes "bounded s" and "closed s"
   3.793 -  shows "compact s"
   3.794 -proof-
   3.795 -  let ?d = "UNIV::'a set"
   3.796 -  { fix f assume as:"\<forall>n::nat. f n \<in> s"
   3.797 -    obtain l::"real^'a" and r where r:"\<forall>n m::nat. m < n \<longrightarrow> r m < r n"
   3.798 -      and lr:"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>?d. \<bar>f (r n) $ i - l $ i\<bar> < e"
   3.799 -      using compact_lemma[OF assms(1) as, THEN spec[where x="?d"]] by auto
   3.800 +        \<exists>l r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
   3.801 +        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
   3.802 +proof
   3.803 +  fix d::"'n set" have "finite d" by simp
   3.804 +  thus "\<exists>l::'a ^ 'n. \<exists>r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
   3.805 +      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
   3.806 +  proof(induct d) case empty thus ?case by auto
   3.807 +  next case (insert k d)
   3.808 +    have s': "bounded ((\<lambda>x. x $ k) ` s)" using `bounded s` by (rule bounded_component)
   3.809 +    obtain l1::"'a^'n" and r1 where r1:"\<forall>n m::nat. m < n \<longrightarrow> r1 m < r1 n" and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
   3.810 +      using insert(3) by auto
   3.811 +    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` s" using `\<forall>n. f n \<in> s` by simp
   3.812 +    obtain l2 r2 where r2:"\<forall>m n::nat. m < n \<longrightarrow> r2 m < r2 n" and lr2:"((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially"
   3.813 +      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
   3.814 +    def r \<equiv> "r1 \<circ> r2" have r:"\<forall>m n. m < n \<longrightarrow> r m < r n" unfolding r_def o_def using r1 and r2 by auto
   3.815 +    moreover
   3.816 +    def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
   3.817      { fix e::real assume "e>0"
   3.818 -      hence "0 < e / (real_of_nat (card ?d))" using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
   3.819 -      then obtain N::nat where N:"\<forall>n\<ge>N. \<forall>i\<in>?d. \<bar>f (r n) $ i - l $ i\<bar> < e / (real_of_nat (card ?d))" using lr[THEN spec[where x="e / (real_of_nat (card ?d))"]] by blast
   3.820 -      { fix n assume n:"n\<ge>N"
   3.821 -	hence "finite ?d"  "?d \<noteq> {}" by auto
   3.822 -	moreover
   3.823 -	{ fix i assume i:"i \<in> ?d"
   3.824 -	  hence "\<bar>((f \<circ> r) n - l) $ i\<bar> < e / real_of_nat (card ?d)" using `n\<ge>N` using N[THEN spec[where x=n]]
   3.825 -	    by auto  }
   3.826 -	ultimately have "(\<Sum>i \<in> ?d. \<bar>((f \<circ> r) n - l) $ i\<bar>)
   3.827 -	  < (\<Sum>i \<in> ?d. e / real_of_nat (card ?d))"
   3.828 -	  using setsum_strict_mono[of "?d" "\<lambda>i. \<bar>((f \<circ> r) n - l) $ i\<bar>" "\<lambda>i. e / (real_of_nat (card ?d))"] by auto
   3.829 -	hence "(\<Sum>i \<in> ?d. \<bar>((f \<circ> r) n - l) $ i\<bar>) < e" unfolding setsum_constant by auto
   3.830 -	hence "dist ((f \<circ> r) n) l < e" unfolding dist_norm using norm_le_l1[of "(f \<circ> r) n - l"] by auto  }
   3.831 -      hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> r) n) l < e" by auto  }
   3.832 -    hence *:"((f \<circ> r) ---> l) sequentially" unfolding Lim_sequentially by auto
   3.833 -    moreover have "l\<in>s"
   3.834 -      using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="f \<circ> r"], THEN spec[where x=l]] and * and as by auto
   3.835 -    ultimately have "\<exists>l\<in>s. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially" using r by auto  }
   3.836 -  thus ?thesis unfolding compact_def by auto
   3.837 +      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" by blast
   3.838 +      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" by (rule tendstoD)
   3.839 +      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
   3.840 +        by (rule eventually_subsequence)
   3.841 +      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially"
   3.842 +        using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
   3.843 +    }
   3.844 +    ultimately show ?case by auto
   3.845 +  qed
   3.846 +qed
   3.847 +
   3.848 +instance "^" :: (heine_borel, finite) heine_borel
   3.849 +proof
   3.850 +  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
   3.851 +  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
   3.852 +  then obtain l r where r: "\<forall>n m::nat. m < n --> r m < r n"
   3.853 +    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
   3.854 +    using compact_lemma [OF s f] by blast
   3.855 +  let ?d = "UNIV::'b set"
   3.856 +  { fix e::real assume "e>0"
   3.857 +    hence "0 < e / (real_of_nat (card ?d))"
   3.858 +      using zero_less_card_finite using divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto
   3.859 +    with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially"
   3.860 +      by simp
   3.861 +    moreover
   3.862 +    { fix n assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
   3.863 +      have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
   3.864 +        unfolding dist_vector_def using zero_le_dist by (rule setL2_le_setsum)
   3.865 +      also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
   3.866 +        by (rule setsum_strict_mono) (simp_all add: n)
   3.867 +      finally have "dist (f (r n)) l < e" by simp
   3.868 +    }
   3.869 +    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
   3.870 +      by (rule eventually_elim1)
   3.871 +  }
   3.872 +  hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
   3.873 +  with r show "\<exists>l r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially" by auto
   3.874  qed
   3.875  
   3.876  subsection{* Completeness. *}
   3.877 @@ -2353,7 +2405,9 @@
   3.878    "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
   3.879  unfolding Cauchy_def by blast
   3.880  
   3.881 -definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> Cauchy f
   3.882 +definition
   3.883 +  complete :: "'a::metric_space set \<Rightarrow> bool" where
   3.884 +  "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f
   3.885                        --> (\<exists>l \<in> s. (f ---> l) sequentially))"
   3.886  
   3.887  lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
   3.888 @@ -2394,16 +2448,13 @@
   3.889  proof-
   3.890    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
   3.891    hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
   3.892 -  { fix n::nat assume "n\<ge>N"
   3.893 -    hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
   3.894 -      using norm_triangle_sub[of "s N" "s n"] by (auto, metis norm_minus_commute le_add_right_mono norm_triangle_sub real_less_def)
   3.895 -  }
   3.896 -  hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
   3.897    moreover
   3.898    have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto
   3.899 -  then obtain a where a:"\<forall>x\<in>s ` {0..N}. norm x \<le> a" unfolding bounded_def by auto
   3.900 -  ultimately show "?thesis" unfolding bounded_def
   3.901 -    apply(rule_tac x="max a (norm (s N) + 1)" in exI) apply auto
   3.902 +  then obtain a where a:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> a"
   3.903 +    unfolding bounded_any_center [where a="s N"] by auto
   3.904 +  ultimately show "?thesis"
   3.905 +    unfolding bounded_any_center [where a="s N"]
   3.906 +    apply(rule_tac x="max a 1" in exI) apply auto
   3.907      apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
   3.908  qed
   3.909  
   3.910 @@ -2432,24 +2483,48 @@
   3.911    thus ?thesis unfolding complete_def by auto
   3.912  qed
   3.913  
   3.914 -lemma complete_univ:
   3.915 - "complete UNIV"
   3.916 +instance heine_borel < complete_space
   3.917 +proof
   3.918 +  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
   3.919 +  hence "bounded (range f)" unfolding image_def
   3.920 +    using cauchy_imp_bounded [of f] by auto
   3.921 +  hence "compact (closure (range f))"
   3.922 +    using bounded_closed_imp_compact [of "closure (range f)"] by auto
   3.923 +  hence "complete (closure (range f))"
   3.924 +    using compact_imp_complete by auto
   3.925 +  moreover have "\<forall>n. f n \<in> closure (range f)"
   3.926 +    using closure_subset [of "range f"] by auto
   3.927 +  ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
   3.928 +    using `Cauchy f` unfolding complete_def by auto
   3.929 +  then show "convergent f"
   3.930 +    unfolding convergent_def LIMSEQ_conv_tendsto [symmetric] by auto
   3.931 +qed
   3.932 +
   3.933 +lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
   3.934  proof(simp add: complete_def, rule, rule)
   3.935 -  fix f::"nat \<Rightarrow> real^'n::finite" assume "Cauchy f"
   3.936 -  hence "bounded (f`UNIV)" using cauchy_imp_bounded[of f] unfolding image_def by auto
   3.937 -  hence "compact (closure (f`UNIV))"  using bounded_closed_imp_compact[of "closure (range f)"] by auto
   3.938 -  hence "complete (closure (range f))" using compact_imp_complete by auto
   3.939 -  thus "\<exists>l. (f ---> l) sequentially" unfolding complete_def[of "closure (range f)"] using `Cauchy f` unfolding closure_def  by auto
   3.940 -qed
   3.941 -
   3.942 -lemma complete_eq_closed: "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
   3.943 +  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
   3.944 +  hence "convergent f" by (rule Cauchy_convergent)
   3.945 +  hence "\<exists>l. f ----> l" unfolding convergent_def .  
   3.946 +  thus "\<exists>l. (f ---> l) sequentially" unfolding LIMSEQ_conv_tendsto .
   3.947 +qed
   3.948 +
   3.949 +lemma complete_imp_closed: assumes "complete s" shows "closed s"
   3.950 +proof -
   3.951 +  { fix x assume "x islimpt s"
   3.952 +    then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
   3.953 +      unfolding islimpt_sequential by auto
   3.954 +    then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
   3.955 +      using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
   3.956 +    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
   3.957 +  }
   3.958 +  thus "closed s" unfolding closed_limpt by auto
   3.959 +qed
   3.960 +
   3.961 +lemma complete_eq_closed:
   3.962 +  fixes s :: "'a::complete_space set"
   3.963 +  shows "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
   3.964  proof
   3.965 -  assume ?lhs
   3.966 -  { fix x assume "x islimpt s"
   3.967 -    then obtain f where f:"\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially" unfolding islimpt_sequential by auto
   3.968 -    then obtain l where l: "l\<in>s" "(f ---> l) sequentially" using `?lhs`[unfolded complete_def]  using convergent_imp_cauchy[of f x] by auto
   3.969 -    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto  }
   3.970 -  thus ?rhs unfolding closed_limpt by auto
   3.971 +  assume ?lhs thus ?rhs by (rule complete_imp_closed)
   3.972  next
   3.973    assume ?rhs
   3.974    { fix f assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
   3.975 @@ -2459,8 +2534,7 @@
   3.976  qed
   3.977  
   3.978  lemma convergent_eq_cauchy:
   3.979 -  fixes s :: "nat \<Rightarrow> real ^ 'n::finite"
   3.980 -    (* FIXME: generalize to complete metric spaces *)
   3.981 +  fixes s :: "nat \<Rightarrow> 'a::complete_space"
   3.982    shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
   3.983  proof
   3.984    assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
   3.985 @@ -2470,9 +2544,9 @@
   3.986  qed
   3.987  
   3.988  lemma convergent_imp_bounded:
   3.989 -  fixes s :: "nat \<Rightarrow> real ^ 'n::finite" (* FIXME: generalize *)
   3.990 +  fixes s :: "nat \<Rightarrow> 'a::metric_space"
   3.991    shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
   3.992 -  using convergent_eq_cauchy[of s]
   3.993 +  using convergent_imp_cauchy[of s]
   3.994    using cauchy_imp_bounded[of s]
   3.995    unfolding image_def
   3.996    by auto
   3.997 @@ -2603,28 +2677,31 @@
   3.998  
   3.999  subsection{* Complete the chain of compactness variants. *}
  3.1000  
  3.1001 -primrec helper_2::"(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> nat \<Rightarrow> 'a" where
  3.1002 +primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
  3.1003    "helper_2 beyond 0 = beyond 0" |
  3.1004 -  "helper_2 beyond (Suc n) = beyond (norm (helper_2 beyond n) + 1 )"
  3.1005 -
  3.1006 -lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::real_normed_vector set"
  3.1007 +  "helper_2 beyond (Suc n) = beyond (dist arbitrary (helper_2 beyond n) + 1 )"
  3.1008 +
  3.1009 +lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
  3.1010    assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
  3.1011    shows "bounded s"
  3.1012  proof(rule ccontr)
  3.1013    assume "\<not> bounded s"
  3.1014 -  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> norm (beyond a) \<le> a"
  3.1015 -    unfolding bounded_def apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> norm x \<le> a"] by auto
  3.1016 -  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. norm (beyond a) > a" unfolding linorder_not_le by auto
  3.1017 +  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist arbitrary (beyond a) \<le> a"
  3.1018 +    unfolding bounded_any_center [where a=arbitrary]
  3.1019 +    apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist arbitrary x \<le> a"] by auto
  3.1020 +  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist arbitrary (beyond a) > a"
  3.1021 +    unfolding linorder_not_le by auto
  3.1022    def x \<equiv> "helper_2 beyond"
  3.1023  
  3.1024    { fix m n ::nat assume "m<n"
  3.1025 -    hence "norm (x m) + 1 < norm (x n)"
  3.1026 +    hence "dist arbitrary (x m) + 1 < dist arbitrary (x n)"
  3.1027      proof(induct n)
  3.1028        case 0 thus ?case by auto
  3.1029      next
  3.1030        case (Suc n)
  3.1031 -      have *:"norm (x n) + 1 < norm (x (Suc n))" unfolding x_def and helper_2.simps
  3.1032 -	using beyond(2)[of "norm (helper_2 beyond n) + 1"] by auto
  3.1033 +      have *:"dist arbitrary (x n) + 1 < dist arbitrary (x (Suc n))"
  3.1034 +        unfolding x_def and helper_2.simps
  3.1035 +	using beyond(2)[of "dist arbitrary (helper_2 beyond n) + 1"] by auto
  3.1036        thus ?case proof(cases "m < n")
  3.1037  	case True thus ?thesis using Suc and * by auto
  3.1038        next
  3.1039 @@ -2636,12 +2713,12 @@
  3.1040      have "1 < dist (x m) (x n)"
  3.1041      proof(cases "m<n")
  3.1042        case True
  3.1043 -      hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
  3.1044 -      thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_norm using norm_triangle_sub[of "x n" "x m"] by auto
  3.1045 +      hence "1 < dist arbitrary (x n) - dist arbitrary (x m)" using *[of m n] by auto
  3.1046 +      thus ?thesis using dist_triangle [of arbitrary "x n" "x m"] by arith
  3.1047      next
  3.1048        case False hence "n<m" using `m\<noteq>n` by auto
  3.1049 -      hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
  3.1050 -      thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_norm using norm_triangle_sub[of "x m" "x n"] by auto
  3.1051 +      hence "1 < dist arbitrary (x m) - dist arbitrary (x n)" using *[of n m] by auto
  3.1052 +      thus ?thesis using dist_triangle2 [of arbitrary "x m" "x n"] by arith
  3.1053      qed  } note ** = this
  3.1054    { fix a b assume "x a = x b" "a \<noteq> b"
  3.1055      hence False using **[of a b] by auto  }
  3.1056 @@ -2712,13 +2789,13 @@
  3.1057        then obtain l' where "l'\<in>s" "l' islimpt {y. \<exists>n. y = x n}" using assms[THEN spec[where x="{y. \<exists>n. y = x n}"]] as(1) by auto
  3.1058        thus "l\<in>s" using sequence_unique_limpt[of x l l'] using as cas by auto
  3.1059      qed  }
  3.1060 -  thus ?thesis unfolding closed_sequential_limits by auto (* FIXME: simp_depth_limit exceeded *)
  3.1061 +  thus ?thesis unfolding closed_sequential_limits by fast
  3.1062  qed
  3.1063  
  3.1064  text{* Hence express everything as an equivalence.   *}
  3.1065  
  3.1066  lemma compact_eq_heine_borel:
  3.1067 -  fixes s :: "(real ^ _) set"
  3.1068 +  fixes s :: "'a::heine_borel set"
  3.1069    shows "compact s \<longleftrightarrow>
  3.1070             (\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f)
  3.1071                 --> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f')))" (is "?lhs = ?rhs")
  3.1072 @@ -2732,7 +2809,7 @@
  3.1073  qed
  3.1074  
  3.1075  lemma compact_eq_bolzano_weierstrass:
  3.1076 -  fixes s :: "(real ^ _) set"
  3.1077 +  fixes s :: "'a::heine_borel set"
  3.1078    shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
  3.1079  proof
  3.1080    assume ?lhs thus ?rhs unfolding compact_eq_heine_borel using heine_borel_imp_bolzano_weierstrass[of s] by auto
  3.1081 @@ -2741,7 +2818,7 @@
  3.1082  qed
  3.1083  
  3.1084  lemma compact_eq_bounded_closed:
  3.1085 -  fixes s :: "(real ^ _) set"
  3.1086 +  fixes s :: "'a::heine_borel set"
  3.1087    shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
  3.1088  proof
  3.1089    assume ?lhs thus ?rhs unfolding compact_eq_bolzano_weierstrass using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed by auto
  3.1090 @@ -2750,16 +2827,30 @@
  3.1091  qed
  3.1092  
  3.1093  lemma compact_imp_bounded:
  3.1094 -  fixes s :: "(real^ _) set"
  3.1095 +  fixes s :: "'a::metric_space set"
  3.1096    shows "compact s ==> bounded s"
  3.1097 -  unfolding compact_eq_bounded_closed
  3.1098 -  by simp
  3.1099 +proof -
  3.1100 +  assume "compact s"
  3.1101 +  hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
  3.1102 +    by (rule compact_imp_heine_borel)
  3.1103 +  hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
  3.1104 +    using heine_borel_imp_bolzano_weierstrass[of s] by auto
  3.1105 +  thus "bounded s"
  3.1106 +    by (rule bolzano_weierstrass_imp_bounded)
  3.1107 +qed
  3.1108  
  3.1109  lemma compact_imp_closed:
  3.1110 -  fixes s :: "(real ^ _) set"
  3.1111 +  fixes s :: "'a::metric_space set"
  3.1112    shows "compact s ==> closed s"
  3.1113 -  unfolding compact_eq_bounded_closed
  3.1114 -  by simp
  3.1115 +proof -
  3.1116 +  assume "compact s"
  3.1117 +  hence "\<forall>f. (\<forall>t\<in>f. open t) \<and> s \<subseteq> \<Union>f \<longrightarrow> (\<exists>f'\<subseteq>f. finite f' \<and> s \<subseteq> \<Union>f')"
  3.1118 +    by (rule compact_imp_heine_borel)
  3.1119 +  hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
  3.1120 +    using heine_borel_imp_bolzano_weierstrass[of s] by auto
  3.1121 +  thus "closed s"
  3.1122 +    by (rule bolzano_weierstrass_imp_closed)
  3.1123 +qed
  3.1124  
  3.1125  text{* In particular, some common special cases. *}
  3.1126  
  3.1127 @@ -2768,9 +2859,11 @@
  3.1128    unfolding compact_def
  3.1129    by simp
  3.1130  
  3.1131 +(* TODO: can any of the next 3 lemmas be generalized to metric spaces? *)
  3.1132 +
  3.1133    (* FIXME : Rename *)
  3.1134  lemma compact_union[intro]:
  3.1135 -  fixes s t :: "(real ^ _) set"
  3.1136 +  fixes s t :: "'a::heine_borel set"
  3.1137    shows "compact s \<Longrightarrow> compact t ==> compact (s \<union> t)"
  3.1138    unfolding compact_eq_bounded_closed
  3.1139    using bounded_Un[of s t]
  3.1140 @@ -2778,7 +2871,7 @@
  3.1141    by simp
  3.1142  
  3.1143  lemma compact_inter[intro]:
  3.1144 -  fixes s t :: "(real ^ _) set"
  3.1145 +  fixes s t :: "'a::heine_borel set"
  3.1146    shows "compact s \<Longrightarrow> compact t ==> compact (s \<inter> t)"
  3.1147    unfolding compact_eq_bounded_closed
  3.1148    using bounded_Int[of s t]
  3.1149 @@ -2786,7 +2879,7 @@
  3.1150    by simp
  3.1151  
  3.1152  lemma compact_inter_closed[intro]:
  3.1153 -  fixes s t :: "(real ^ _) set"
  3.1154 +  fixes s t :: "'a::heine_borel set"
  3.1155    shows "compact s \<Longrightarrow> closed t ==> compact (s \<inter> t)"
  3.1156    unfolding compact_eq_bounded_closed
  3.1157    using closed_Int[of s t]
  3.1158 @@ -2794,7 +2887,7 @@
  3.1159    by blast
  3.1160  
  3.1161  lemma closed_inter_compact[intro]:
  3.1162 -  fixes s t :: "(real ^ _) set"
  3.1163 +  fixes s t :: "'a::heine_borel set"
  3.1164    shows "closed s \<Longrightarrow> compact t ==> compact (s \<inter> t)"
  3.1165  proof-
  3.1166    assume "closed s" "compact t"
  3.1167 @@ -2805,25 +2898,6 @@
  3.1168      by auto
  3.1169  qed
  3.1170  
  3.1171 -lemma finite_imp_closed:
  3.1172 -  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
  3.1173 -  shows "finite s ==> closed s"
  3.1174 -proof-
  3.1175 -  assume "finite s" hence "\<not>( \<exists>t. t \<subseteq> s \<and> infinite t)" using finite_subset by auto
  3.1176 -  thus ?thesis using bolzano_weierstrass_imp_closed[of s] by auto
  3.1177 -qed
  3.1178 -
  3.1179 -lemma finite_imp_compact:
  3.1180 -  fixes s :: "(real ^ _) set"
  3.1181 -  shows "finite s ==> compact s"
  3.1182 -  unfolding compact_eq_bounded_closed
  3.1183 -  using finite_imp_closed finite_imp_bounded
  3.1184 -  by blast
  3.1185 -
  3.1186 -lemma compact_sing [simp]: "compact {a}"
  3.1187 -  unfolding compact_def o_def
  3.1188 -  by (auto simp add: tendsto_const)
  3.1189 -
  3.1190  lemma closed_sing [simp]:
  3.1191    fixes a :: "'a::metric_space"
  3.1192    shows "closed {a}"
  3.1193 @@ -2833,27 +2907,49 @@
  3.1194    apply (simp add: dist_nz dist_commute)
  3.1195    done
  3.1196  
  3.1197 +lemma finite_imp_closed:
  3.1198 +  fixes s :: "'a::metric_space set"
  3.1199 +  shows "finite s ==> closed s"
  3.1200 +proof (induct set: finite)
  3.1201 +  case empty show "closed {}" by simp
  3.1202 +next
  3.1203 +  case (insert x F)
  3.1204 +  hence "closed ({x} \<union> F)" by (simp only: closed_Un closed_sing)
  3.1205 +  thus "closed (insert x F)" by simp
  3.1206 +qed
  3.1207 +
  3.1208 +lemma finite_imp_compact:
  3.1209 +  fixes s :: "'a::heine_borel set"
  3.1210 +  shows "finite s ==> compact s"
  3.1211 +  unfolding compact_eq_bounded_closed
  3.1212 +  using finite_imp_closed finite_imp_bounded
  3.1213 +  by blast
  3.1214 +
  3.1215 +lemma compact_sing [simp]: "compact {a}"
  3.1216 +  unfolding compact_def o_def
  3.1217 +  by (auto simp add: tendsto_const)
  3.1218 +
  3.1219  lemma compact_cball[simp]:
  3.1220 -  fixes x :: "real ^ _"
  3.1221 +  fixes x :: "'a::heine_borel"
  3.1222    shows "compact(cball x e)"
  3.1223    using compact_eq_bounded_closed bounded_cball closed_cball
  3.1224    by blast
  3.1225  
  3.1226  lemma compact_frontier_bounded[intro]:
  3.1227 -  fixes s :: "(real ^ _) set"
  3.1228 +  fixes s :: "'a::heine_borel set"
  3.1229    shows "bounded s ==> compact(frontier s)"
  3.1230    unfolding frontier_def
  3.1231    using compact_eq_bounded_closed
  3.1232    by blast
  3.1233  
  3.1234  lemma compact_frontier[intro]:
  3.1235 -  fixes s :: "(real ^ _) set"
  3.1236 +  fixes s :: "'a::heine_borel set"
  3.1237    shows "compact s ==> compact (frontier s)"
  3.1238    using compact_eq_bounded_closed compact_frontier_bounded
  3.1239    by blast
  3.1240  
  3.1241  lemma frontier_subset_compact:
  3.1242 -  fixes s :: "(real ^ _) set"
  3.1243 +  fixes s :: "'a::heine_borel set"
  3.1244    shows "compact s ==> frontier s \<subseteq> s"
  3.1245    using frontier_subset_closed compact_eq_bounded_closed
  3.1246    by blast
  3.1247 @@ -2867,7 +2963,7 @@
  3.1248  text{* Finite intersection property. I could make it an equivalence in fact. *}
  3.1249  
  3.1250  lemma compact_imp_fip:
  3.1251 -  fixes s :: "(real ^ _) set"
  3.1252 +  fixes s :: "'a::heine_borel set"
  3.1253    assumes "compact s"  "\<forall>t \<in> f. closed t"
  3.1254          "\<forall>f'. finite f' \<and> f' \<subseteq> f --> (s \<inter> (\<Inter> f') \<noteq> {})"
  3.1255    shows "s \<inter> (\<Inter> f) \<noteq> {}"
  3.1256 @@ -2886,7 +2982,7 @@
  3.1257  lemma bounded_closed_nest:
  3.1258    assumes "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
  3.1259    "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"  "bounded(s 0)"
  3.1260 -  shows "\<exists> a::real^'a::finite. \<forall>n::nat. a \<in> s(n)"
  3.1261 +  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
  3.1262  proof-
  3.1263    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
  3.1264    from assms(4,1) have *:"compact (s 0)" using bounded_closed_imp_compact[of "s 0"] by auto
  3.1265 @@ -2918,7 +3014,7 @@
  3.1266            "\<forall>n. (s n \<noteq> {})"
  3.1267            "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
  3.1268            "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
  3.1269 -  shows "\<exists>a::real^'a::finite. \<forall>n::nat. a \<in> s n"
  3.1270 +  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s n"
  3.1271  proof-
  3.1272    have "\<forall>n. \<exists> x. x\<in>s n" using assms(2) by auto
  3.1273    hence "\<exists>t. \<forall>n. t n \<in> s n" using choice[of "\<lambda> n x. x \<in> s n"] by auto
  3.1274 @@ -2951,7 +3047,7 @@
  3.1275            "\<forall>n. s n \<noteq> {}"
  3.1276            "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
  3.1277            "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y\<in>(s n). dist x y < e"
  3.1278 -  shows "\<exists>a::real^'a::finite. \<Inter> {t. (\<exists>n::nat. t = s n)} = {a}"
  3.1279 +  shows "\<exists>a::'a::heine_borel. \<Inter> {t. (\<exists>n::nat. t = s n)} = {a}"
  3.1280  proof-
  3.1281    obtain a where a:"\<forall>n. a \<in> s n" using decreasing_closed_nest[of s] using assms by auto
  3.1282    { fix b assume b:"b \<in> \<Inter>{t. \<exists>n. t = s n}"
  3.1283 @@ -2966,7 +3062,7 @@
  3.1284  
  3.1285  text{* Cauchy-type criteria for uniform convergence. *}
  3.1286  
  3.1287 -lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> real^'a::finite" shows
  3.1288 +lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::heine_borel" shows
  3.1289   "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
  3.1290    (\<forall>e>0. \<exists>N. \<forall>m n x. N \<le> m \<and> N \<le> n \<and> P x  --> dist (s m x) (s n x) < e)" (is "?lhs = ?rhs")
  3.1291  proof(rule)
  3.1292 @@ -3000,7 +3096,7 @@
  3.1293  qed
  3.1294  
  3.1295  lemma uniformly_cauchy_imp_uniformly_convergent:
  3.1296 -  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> real ^ 'n::finite"
  3.1297 +  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::heine_borel"
  3.1298    assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
  3.1299            "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
  3.1300    shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
  3.1301 @@ -3390,13 +3486,13 @@
  3.1302    unfolding dist_norm minus_diff_minus norm_minus_cancel ..
  3.1303  
  3.1304  lemma uniformly_continuous_on_neg:
  3.1305 -  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
  3.1306 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
  3.1307    shows "uniformly_continuous_on s f
  3.1308           ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
  3.1309    unfolding uniformly_continuous_on_def dist_minus .
  3.1310  
  3.1311  lemma uniformly_continuous_on_add:
  3.1312 -  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
  3.1313 +  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
  3.1314    assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
  3.1315    shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
  3.1316  proof-
  3.1317 @@ -3409,7 +3505,7 @@
  3.1318  qed
  3.1319  
  3.1320  lemma uniformly_continuous_on_sub:
  3.1321 -  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
  3.1322 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
  3.1323    shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
  3.1324             ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
  3.1325    unfolding ab_diff_minus
  3.1326 @@ -3907,11 +4003,18 @@
  3.1327    thus ?thesis unfolding Lim_at by auto
  3.1328  qed
  3.1329  
  3.1330 +lemma bounded_linear_continuous_at:
  3.1331 +  assumes "bounded_linear f"  shows "continuous (at a) f"
  3.1332 +  unfolding continuous_at using assms
  3.1333 +  apply (rule bounded_linear.tendsto)
  3.1334 +  apply (rule Lim_at_id [unfolded id_def])
  3.1335 +  done
  3.1336 +
  3.1337  lemma linear_continuous_at:
  3.1338    fixes f :: "real ^ _ \<Rightarrow> real ^ _"
  3.1339    assumes "linear f"  shows "continuous (at a) f"
  3.1340 -  unfolding continuous_at Lim_at_zero[of f "f a" a] using linear_lim_0[OF assms]
  3.1341 -  unfolding Lim_null[of "\<lambda>x. f (a + x)"] unfolding linear_sub[OF assms, THEN sym] by auto
  3.1342 +  using assms unfolding linear_conv_bounded_linear
  3.1343 +  by (rule bounded_linear_continuous_at)
  3.1344  
  3.1345  lemma linear_continuous_within:
  3.1346    fixes f :: "real ^ _ \<Rightarrow> real ^ _"
  3.1347 @@ -4202,14 +4305,15 @@
  3.1348  subsection{* Preservation properties for pasted sets.                                  *}
  3.1349  
  3.1350  lemma bounded_pastecart:
  3.1351 +  fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
  3.1352    assumes "bounded s" "bounded t"
  3.1353    shows "bounded { pastecart x y | x y . (x \<in> s \<and> y \<in> t)}"
  3.1354  proof-
  3.1355 -  obtain a b where ab:"\<forall>x\<in>s. norm x \<le> a" "\<forall>x\<in>t. norm x \<le> b" using assms[unfolded bounded_def] by auto
  3.1356 +  obtain a b where ab:"\<forall>x\<in>s. norm x \<le> a" "\<forall>x\<in>t. norm x \<le> b" using assms[unfolded bounded_iff] by auto
  3.1357    { fix x y assume "x\<in>s" "y\<in>t"
  3.1358      hence "norm x \<le> a" "norm y \<le> b" using ab by auto
  3.1359      hence "norm (pastecart x y) \<le> a + b" using norm_pastecart[of x y] by auto }
  3.1360 -  thus ?thesis unfolding bounded_def by auto
  3.1361 +  thus ?thesis unfolding bounded_iff by auto
  3.1362  qed
  3.1363  
  3.1364  lemma closed_pastecart:
  3.1365 @@ -4241,24 +4345,25 @@
  3.1366  
  3.1367  text{* Hence some useful properties follow quite easily.                         *}
  3.1368  
  3.1369 +lemma compact_scaleR_image:
  3.1370 +  fixes s :: "'a::real_normed_vector set"
  3.1371 +  assumes "compact s"  shows "compact ((\<lambda>x. scaleR c x) ` s)"
  3.1372 +proof-
  3.1373 +  let ?f = "\<lambda>x. scaleR c x"
  3.1374 +  have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
  3.1375 +  show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
  3.1376 +    using bounded_linear_continuous_at[OF *] assms by auto
  3.1377 +qed
  3.1378 +
  3.1379  lemma compact_scaling:
  3.1380    fixes s :: "(real ^ _) set"
  3.1381    assumes "compact s"  shows "compact ((\<lambda>x. c *s x) ` s)"
  3.1382 -proof-
  3.1383 -  let ?f = "\<lambda>x. c *s x"
  3.1384 -  have *:"linear ?f" unfolding linear_def vector_smult_assoc vector_add_ldistrib real_mult_commute by auto
  3.1385 -  show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
  3.1386 -    using linear_continuous_at[OF *] assms by auto
  3.1387 -qed
  3.1388 +  using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)
  3.1389  
  3.1390  lemma compact_negations:
  3.1391 -  fixes s :: "(real ^ _) set"
  3.1392 +  fixes s :: "'a::real_normed_vector set"
  3.1393    assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
  3.1394 -proof-
  3.1395 -  have "(\<lambda>x. - x) ` s = (\<lambda>x. (- 1) *s x) ` s"
  3.1396 -    unfolding vector_sneg_minus1 ..
  3.1397 -  thus ?thesis using compact_scaling[OF assms, of "-1"] by auto
  3.1398 -qed
  3.1399 +  using compact_scaleR_image [OF assms, of "- 1"] by auto
  3.1400  
  3.1401  lemma compact_sums:
  3.1402    fixes s t :: "(real ^ _) set"
  3.1403 @@ -4317,6 +4422,7 @@
  3.1404  text{* We can state this in terms of diameter of a set.                          *}
  3.1405  
  3.1406  definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
  3.1407 +  (* TODO: generalize to class metric_space *)
  3.1408  
  3.1409  lemma diameter_bounded:
  3.1410    assumes "bounded s"
  3.1411 @@ -4324,7 +4430,7 @@
  3.1412          "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
  3.1413  proof-
  3.1414    let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
  3.1415 -  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_def] by auto
  3.1416 +  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
  3.1417    { fix x y assume "x \<in> s" "y \<in> s"
  3.1418      hence "norm (x - y) \<le> 2 * a" using norm_triangle_ineq[of x "-y", unfolded norm_minus_cancel] a[THEN bspec[where x=x]] a[THEN bspec[where x=y]] by (auto simp add: ring_simps)  }
  3.1419    note * = this
  3.1420 @@ -4365,9 +4471,9 @@
  3.1421  
  3.1422  text{* Related results with closure as the conclusion.                           *}
  3.1423  
  3.1424 -lemma closed_scaling:
  3.1425 -  fixes s :: "(real ^ _) set"
  3.1426 -  assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
  3.1427 +lemma closed_scaleR_image:
  3.1428 +  fixes s :: "'a::real_normed_vector set"
  3.1429 +  assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
  3.1430  proof(cases "s={}")
  3.1431    case True thus ?thesis by auto
  3.1432  next
  3.1433 @@ -4378,29 +4484,39 @@
  3.1434      case True thus ?thesis apply auto unfolding * using closed_sing by auto
  3.1435    next
  3.1436      case False
  3.1437 -    { fix x l assume as:"\<forall>n::nat. x n \<in> op *s c ` s"  "(x ---> l) sequentially"
  3.1438 -      { fix n::nat have "(1 / c) *s x n \<in> s" using as(1)[THEN spec[where x=n]] using `c\<noteq>0` by (auto simp add: vector_smult_assoc) }
  3.1439 +    { fix x l assume as:"\<forall>n::nat. x n \<in> scaleR c ` s"  "(x ---> l) sequentially"
  3.1440 +      { fix n::nat have "scaleR (1 / c) (x n) \<in> s"
  3.1441 +          using as(1)[THEN spec[where x=n]]
  3.1442 +          using `c\<noteq>0` by (auto simp add: vector_smult_assoc)
  3.1443 +      }
  3.1444        moreover
  3.1445        { fix e::real assume "e>0"
  3.1446  	hence "0 < e *\<bar>c\<bar>"  using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
  3.1447 -	then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>" using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
  3.1448 -	hence "\<exists>N. \<forall>n\<ge>N. dist ((1 / c) *s x n) ((1 / c) *s l) < e" unfolding dist_norm unfolding vector_ssub_ldistrib[THEN sym] norm_mul
  3.1449 +	then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
  3.1450 +          using as(2)[unfolded Lim_sequentially, THEN spec[where x="e * abs c"]] by auto
  3.1451 +	hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
  3.1452 +          unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] norm_scaleR
  3.1453  	  using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto  }
  3.1454 -      hence "((\<lambda>n. (1 / c) *s x n) ---> (1 / c) *s l) sequentially" unfolding Lim_sequentially by auto
  3.1455 -      ultimately have "l \<in> op *s c ` s"  using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. (1/c) *s x n"], THEN spec[where x="(1/c) *s l"]]
  3.1456 -	unfolding image_iff using `c\<noteq>0` apply(rule_tac x="(1 / c) *s l" in bexI) apply auto unfolding vector_smult_assoc  by auto  }
  3.1457 -    thus ?thesis unfolding closed_sequential_limits by auto
  3.1458 +      hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto
  3.1459 +      ultimately have "l \<in> scaleR c ` s"
  3.1460 +        using assms[unfolded closed_sequential_limits, THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"], THEN spec[where x="scaleR (1/c) l"]]
  3.1461 +	unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto  }
  3.1462 +    thus ?thesis unfolding closed_sequential_limits by fast
  3.1463    qed
  3.1464  qed
  3.1465  
  3.1466 +lemma closed_scaling:
  3.1467 +  fixes s :: "(real ^ _) set"
  3.1468 +  assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
  3.1469 +  using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
  3.1470 +
  3.1471  lemma closed_negations:
  3.1472 -  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
  3.1473 +  fixes s :: "'a::real_normed_vector set"
  3.1474    assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
  3.1475 -  using closed_scaling[OF assms, of "- 1"]
  3.1476 -  unfolding vector_sneg_minus1 by auto
  3.1477 +  using closed_scaleR_image[OF assms, of "- 1"] by simp
  3.1478  
  3.1479  lemma compact_closed_sums:
  3.1480 -  fixes s :: "(real ^ _) set"
  3.1481 +  fixes s :: "'a::real_normed_vector set"
  3.1482    assumes "compact s"  "closed t"  shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
  3.1483  proof-
  3.1484    let ?S = "{x + y |x y. x \<in> s \<and> y \<in> t}"
  3.1485 @@ -4416,11 +4532,11 @@
  3.1486        using f(3) by auto
  3.1487      hence "l \<in> ?S" using `l' \<in> s` apply auto apply(rule_tac x=l' in exI) apply(rule_tac x="l - l'" in exI) by auto
  3.1488    }
  3.1489 -  thus ?thesis unfolding closed_sequential_limits by auto
  3.1490 +  thus ?thesis unfolding closed_sequential_limits by fast
  3.1491  qed
  3.1492  
  3.1493  lemma closed_compact_sums:
  3.1494 -  fixes s t :: "(real ^ _) set"
  3.1495 +  fixes s t :: "'a::real_normed_vector set"
  3.1496    assumes "closed s"  "compact t"
  3.1497    shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
  3.1498  proof-
  3.1499 @@ -4430,7 +4546,7 @@
  3.1500  qed
  3.1501  
  3.1502  lemma compact_closed_differences:
  3.1503 -  fixes s t :: "(real ^ _) set"
  3.1504 +  fixes s t :: "'a::real_normed_vector set"
  3.1505    assumes "compact s"  "closed t"
  3.1506    shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
  3.1507  proof-
  3.1508 @@ -4440,7 +4556,7 @@
  3.1509  qed
  3.1510  
  3.1511  lemma closed_compact_differences:
  3.1512 -  fixes s t :: "(real ^ _) set"
  3.1513 +  fixes s t :: "'a::real_normed_vector set"
  3.1514    assumes "closed s" "compact t"
  3.1515    shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
  3.1516  proof-
  3.1517 @@ -4450,7 +4566,7 @@
  3.1518  qed
  3.1519  
  3.1520  lemma closed_translation:
  3.1521 -  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
  3.1522 +  fixes a :: "'a::real_normed_vector"
  3.1523    assumes "closed s"  shows "closed ((\<lambda>x. a + x) ` s)"
  3.1524  proof-
  3.1525    have "{a + y |y. y \<in> s} = (op + a ` s)" by auto
  3.1526 @@ -4458,21 +4574,26 @@
  3.1527  qed
  3.1528  
  3.1529  lemma translation_UNIV:
  3.1530 - "range (\<lambda>x::real^'a. a + x) = UNIV"
  3.1531 +  fixes a :: "'a::ab_group_add" shows "range (\<lambda>x. a + x) = UNIV"
  3.1532    apply (auto simp add: image_iff) apply(rule_tac x="x - a" in exI) by auto
  3.1533  
  3.1534 -lemma translation_diff: "(\<lambda>x::real^'a. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)" by auto
  3.1535 +lemma translation_diff:
  3.1536 +  fixes a :: "'a::ab_group_add"
  3.1537 +  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
  3.1538 +  by auto
  3.1539  
  3.1540  lemma closure_translation:
  3.1541 -  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
  3.1542 +  fixes a :: "'a::real_normed_vector"
  3.1543    shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
  3.1544  proof-
  3.1545 -  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"  apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
  3.1546 -  show ?thesis unfolding closure_interior translation_diff translation_UNIV using interior_translation[of a "UNIV - s"] unfolding * by auto
  3.1547 +  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"
  3.1548 +    apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
  3.1549 +  show ?thesis unfolding closure_interior translation_diff translation_UNIV
  3.1550 +    using interior_translation[of a "UNIV - s"] unfolding * by auto
  3.1551  qed
  3.1552  
  3.1553  lemma frontier_translation:
  3.1554 -  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
  3.1555 +  fixes a :: "'a::real_normed_vector"
  3.1556    shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
  3.1557    unfolding frontier_def translation_diff interior_translation closure_translation by auto
  3.1558  
  3.1559 @@ -4769,7 +4890,7 @@
  3.1560        have "\<bar>x$i\<bar> \<le> \<bar>a$i\<bar> + \<bar>b$i\<bar>" using x[THEN spec[where x=i]] by auto  }
  3.1561      hence "(\<Sum>i\<in>UNIV. \<bar>x $ i\<bar>) \<le> ?b" by(rule setsum_mono)
  3.1562      hence "norm x \<le> ?b" using norm_le_l1[of x] by auto  }
  3.1563 -  thus ?thesis unfolding interval and bounded_def by auto
  3.1564 +  thus ?thesis unfolding interval and bounded_iff by auto
  3.1565  qed
  3.1566  
  3.1567  lemma bounded_interval: fixes a :: "real^'n::finite" shows
  3.1568 @@ -5194,7 +5315,7 @@
  3.1569    assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
  3.1570    shows "\<exists>l. (s ---> l) sequentially"
  3.1571  proof-
  3.1572 -  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_def abs_dest_vec1] by auto
  3.1573 +  obtain a where a:"\<forall>n. \<bar>dest_vec1 (s n)\<bar> \<le>  a" using assms(1)[unfolded bounded_iff abs_dest_vec1] by auto
  3.1574    { fix m::nat
  3.1575      have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
  3.1576        apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
  3.1577 @@ -5384,6 +5505,7 @@
  3.1578  qed
  3.1579  
  3.1580  lemma complete_isometric_image:
  3.1581 +  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
  3.1582    assumes "0 < e" and s:"subspace s" and f:"linear f" and normf:"\<forall>x\<in>s. norm(f x) \<ge> e * norm(x)" and cs:"complete s"
  3.1583    shows "complete(f ` s)"
  3.1584  proof-
  3.1585 @@ -5577,7 +5699,7 @@
  3.1586  qed
  3.1587  
  3.1588  lemma complete_subspace:
  3.1589 -  "subspace s ==> complete s"
  3.1590 +  fixes s :: "(real ^ _) set" shows "subspace s ==> complete s"
  3.1591    using complete_eq_closed closed_subspace
  3.1592    by auto
  3.1593