# HG changeset patch
# User huffman
# Date 1244571128 25200
# Node ID 16068eb224c0b0ebb8ed77be9e52d4071b4b419f
# Parent  8abf99ab669cafe540629a83ce53b75b0f7d3330# Parent  feec2711da4e1969e82bed0ab7f7684448f714d4
merged

diff -r 8abf99ab669c -r 16068eb224c0 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -750,7 +750,7 @@
   using convex_Inter[unfolded Ball_def mem_def] by auto
 
 lemma bounded_convex_hull: assumes "bounded s" shows "bounded(convex hull s)"
-proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def by auto
+proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_iff by auto
   show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
     unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
     unfolding subset_eq mem_cball dist_norm using B by auto qed
@@ -2018,7 +2018,7 @@
       case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm)
 	using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
     next guess a using UNIV_witness[where 'a = 'n] ..
-      obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_def by auto
+      obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_iff by auto
       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)
 	unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def])
       case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
diff -r 8abf99ab669c -r 16068eb224c0 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
+++ b/src/HOL/Library/Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -1783,6 +1783,36 @@
   then show ?thesis using Kp by blast
 qed
 
+lemma smult_conv_scaleR: "c *s x = scaleR c x"
+  unfolding vector_scalar_mult_def vector_scaleR_def by simp
+
+lemma linear_conv_bounded_linear:
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
+  shows "linear f \<longleftrightarrow> bounded_linear f"
+proof
+  assume "linear f"
+  show "bounded_linear f"
+  proof
+    fix x y show "f (x + y) = f x + f y"
+      using `linear f` unfolding linear_def by simp
+  next
+    fix r x show "f (scaleR r x) = scaleR r (f x)"
+      using `linear f` unfolding linear_def
+      by (simp add: smult_conv_scaleR)
+  next
+    have "\<exists>B. \<forall>x. norm (f x) \<le> B * norm x"
+      using `linear f` by (rule linear_bounded)
+    thus "\<exists>K. \<forall>x. norm (f x) \<le> norm x * K"
+      by (simp add: mult_commute)
+  qed
+next
+  assume "bounded_linear f"
+  then interpret f: bounded_linear f .
+  show "linear f"
+    unfolding linear_def smult_conv_scaleR
+    by (simp add: f.add f.scaleR)
+qed
+
 subsection{* Bilinear functions. *}
 
 definition "bilinear f \<longleftrightarrow> (\<forall>x. linear(\<lambda>y. f x y)) \<and> (\<forall>y. linear(\<lambda>x. f x y))"
@@ -1886,6 +1916,41 @@
   with Kp show ?thesis by blast
 qed
 
+lemma bilinear_conv_bounded_bilinear:
+  fixes h :: "real ^ _ \<Rightarrow> real ^ _ \<Rightarrow> real ^ _"
+  shows "bilinear h \<longleftrightarrow> bounded_bilinear h"
+proof
+  assume "bilinear h"
+  show "bounded_bilinear h"
+  proof
+    fix x y z show "h (x + y) z = h x z + h y z"
+      using `bilinear h` unfolding bilinear_def linear_def by simp
+  next
+    fix x y z show "h x (y + z) = h x y + h x z"
+      using `bilinear h` unfolding bilinear_def linear_def by simp
+  next
+    fix r x y show "h (scaleR r x) y = scaleR r (h x y)"
+      using `bilinear h` unfolding bilinear_def linear_def
+      by (simp add: smult_conv_scaleR)
+  next
+    fix r x y show "h x (scaleR r y) = scaleR r (h x y)"
+      using `bilinear h` unfolding bilinear_def linear_def
+      by (simp add: smult_conv_scaleR)
+  next
+    have "\<exists>B. \<forall>x y. norm (h x y) \<le> B * norm x * norm y"
+      using `bilinear h` by (rule bilinear_bounded)
+    thus "\<exists>K. \<forall>x y. norm (h x y) \<le> norm x * norm y * K"
+      by (simp add: mult_ac)
+  qed
+next
+  assume "bounded_bilinear h"
+  then interpret h: bounded_bilinear h .
+  show "bilinear h"
+    unfolding bilinear_def linear_conv_bounded_linear
+    using h.bounded_linear_left h.bounded_linear_right
+    by simp
+qed
+
 subsection{* Adjoints. *}
 
 definition "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
diff -r 8abf99ab669c -r 16068eb224c0 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 09 19:41:27 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Tue Jun 09 11:12:08 2009 -0700
@@ -969,8 +969,8 @@
   "at_infinity = Abs_net (range (\<lambda>r. {x. r \<le> norm x}))"
 
 definition
-  indirection :: "real ^'n::finite \<Rightarrow> real ^'n \<Rightarrow> (real ^'n) net" (infixr "indirection" 70) where
-  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = c*s v}"
+  indirection :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> 'a net" (infixr "indirection" 70) where
+  "a indirection v = (at a) within {b. \<exists>c\<ge>0. b - a = scaleR c v}"
 
 text{* Prove That They are all nets. *}
 
@@ -1130,7 +1130,7 @@
   unfolding Lim_at LIM_def by (simp only: zero_less_dist_iff)
 
 lemma Lim_at_infinity:
-  "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x::real^'n::finite. norm x >= b \<longrightarrow> dist (f x) l < e)"
+  "(f ---> l) at_infinity \<longleftrightarrow> (\<forall>e>0. \<exists>b. \<forall>x. norm x >= b \<longrightarrow> dist (f x) l < e)"
   by (auto simp add: tendsto_iff eventually_at_infinity)
 
 lemma Lim_sequentially:
@@ -1141,10 +1141,8 @@
 lemma Lim_sequentially_iff_LIMSEQ: "(S ---> l) sequentially \<longleftrightarrow> S ----> l"
   unfolding Lim_sequentially LIMSEQ_def ..
 
-lemma Lim_eventually:
-  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
-  shows "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
-  unfolding tendsto_iff by (auto elim: eventually_rev_mono)
+lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
+  by (rule topological_tendstoI, auto elim: eventually_rev_mono)
 
 text{* The expected monotonicity property. *}
 
@@ -1172,31 +1170,32 @@
 text{* Interrelations between restricted and unrestricted limits. *}
 
 lemma Lim_at_within: "(f ---> l) net ==> (f ---> l)(net within S)"
+  (* FIXME: rename *)
   unfolding tendsto_def Limits.eventually_within
   apply (clarify, drule spec, drule (1) mp, drule (1) mp)
   by (auto elim!: eventually_elim1)
 
 lemma Lim_within_open:
-  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
   assumes"a \<in> S" "open S"
   shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?lhs
-  { fix e::real assume "e>0"
-    have "eventually (\<lambda>x. dist (f x) l < e) (at a within S)"
-      using `?lhs` `e>0` by (rule tendstoD)
-    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> dist (f x) l < e) (at a)"
+  { fix A assume "open A" "l \<in> A"
+    with `?lhs` have "eventually (\<lambda>x. f x \<in> A) (at a within S)"
+      by (rule topological_tendstoD)
+    hence "eventually (\<lambda>x. x \<in> S \<longrightarrow> f x \<in> A) (at a)"
       unfolding Limits.eventually_within .
-    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"
+    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"
       unfolding eventually_at_topological by fast
-    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"
+    hence "open (T \<inter> S)" "a \<in> T \<inter> S" "\<forall>x\<in>(T \<inter> S). x \<noteq> a \<longrightarrow> f x \<in> A"
       using assms by auto
-    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> dist (f x) l < e)"
+    hence "\<exists>T. open T \<and> a \<in> T \<and> (\<forall>x\<in>T. x \<noteq> a \<longrightarrow> f x \<in> A)"
       by fast
-    hence "eventually (\<lambda>x. dist (f x) l < e) (at a)"
+    hence "eventually (\<lambda>x. f x \<in> A) (at a)"
       unfolding eventually_at_topological .
   }
-  thus ?rhs by (rule tendstoI)
+  thus ?rhs by (rule topological_tendstoI)
 next
   assume ?rhs
   thus ?lhs by (rule Lim_at_within)
@@ -1242,25 +1241,12 @@
 lemma Lim_linear: fixes f :: "('a \<Rightarrow> real^'n::finite)" and h :: "(real^'n \<Rightarrow> real^'m::finite)"
   assumes "(f ---> l) net" "linear h"
   shows "((\<lambda>x. h (f x)) ---> h l) net"
-proof -
-  obtain b where b: "b>0" "\<forall>x. norm (h x) \<le> b * norm x"
-    using assms(2) using linear_bounded_pos[of h] by auto
-  { fix e::real assume "e >0"
-    hence "e/b > 0" using `b>0` by (metis divide_pos_pos)
-    with `(f ---> l) net` have "eventually (\<lambda>x. dist (f x) l < e/b) net"
-      by (rule tendstoD)
-    then have "eventually (\<lambda>x. dist (h (f x)) (h l) < e) net"
-      apply (rule eventually_rev_mono [rule_format])
-      apply (simp add: dist_norm linear_sub [OF `linear h`, symmetric])
-      apply (rule le_less_trans [OF b(2) [rule_format]])
-      apply (simp add: pos_less_divide_eq `0 < b` mult_commute)
-      done
-  }
-  thus ?thesis unfolding tendsto_iff by simp
-qed
+using `linear h` `(f ---> l) net`
+unfolding linear_conv_bounded_linear
+by (rule bounded_linear.tendsto)
 
 lemma Lim_const: "((\<lambda>x. a) ---> a) net"
-  unfolding tendsto_def by simp
+  by (rule tendsto_const)
 
 lemma Lim_cmul:
   fixes f :: "'a \<Rightarrow> real ^ 'n::finite"
@@ -1274,34 +1260,16 @@
 lemma Lim_neg:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
-  apply (simp add: Lim dist_norm  group_simps)
-  apply (subst minus_diff_eq[symmetric])
-  unfolding norm_minus_cancel by simp
+  by (rule tendsto_minus)
 
 lemma Lim_add: fixes f :: "'a \<Rightarrow> 'b::real_normed_vector" shows
  "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) + g(x)) ---> l + m) net"
-proof-
-  assume as:"(f ---> l) net" "(g ---> m) net"
-  { fix e::real
-    assume "e>0"
-    hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
-            "eventually (\<lambda>x. dist (g x) m < e/2) net" using as
-      by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
-    hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
-      apply (elim eventually_rev_mp)
-      apply (rule always_eventually, clarify)
-      apply (rule le_less_trans [OF dist_triangle_add])
-      apply simp
-      done
-  }
-  thus ?thesis unfolding tendsto_iff by simp
-qed
+  by (rule tendsto_add)
 
 lemma Lim_sub:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "(f ---> l) net \<Longrightarrow> (g ---> m) net \<Longrightarrow> ((\<lambda>x. f(x) - g(x)) ---> l - m) net"
-  unfolding diff_minus
-  by (simp add: Lim_add Lim_neg)
+  by (rule tendsto_diff)
 
 lemma Lim_null:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
@@ -1347,7 +1315,7 @@
   fixes g :: "'a \<Rightarrow> 'c::real_normed_vector"
   assumes "eventually (\<lambda>n. norm(f n) <= norm(g n)) net"  "(g ---> 0) net"
   shows "(f ---> 0) net"
-proof(simp add: tendsto_iff, rule+)
+proof (rule tendstoI)
   fix e::real assume "e>0"
   { fix x
     assume "norm (f x) \<le> norm (g x)" "dist (g x) 0 < e"
@@ -1361,24 +1329,43 @@
 text{* Deducing things about the limit from the elements. *}
 
 lemma Lim_in_closed_set:
-  fixes l :: "'a::metric_space" (* FIXME: generalize to topological_space *)
-  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net"  "\<not>(trivial_limit net)" "(f ---> l) net"
+  assumes "closed S" "eventually (\<lambda>x. f(x) \<in> S) net" "\<not>(trivial_limit net)" "(f ---> l) net"
   shows "l \<in> S"
 proof (rule ccontr)
   assume "l \<notin> S"
-  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
-  hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
-  have "eventually (\<lambda>x. dist (f x) l < e) net"
-    using assms(4) `e>0` by (rule tendstoD)
-  with assms(2) have "eventually (\<lambda>x. f x \<in> S \<and> dist (f x) l < e) net"
-    by (rule eventually_conjI)
-  then obtain x where "f x \<in> S" "dist (f x) l < e"
-    using assms(3) eventually_happens by auto
-  with * show "False" by (simp add: dist_commute)
+  with `closed S` have "open (- S)" "l \<in> - S"
+    by (simp_all add: open_Compl)
+  with assms(4) have "eventually (\<lambda>x. f x \<in> - S) net"
+    by (rule topological_tendstoD)
+  with assms(2) have "eventually (\<lambda>x. False) net"
+    by (rule eventually_elim2) simp
+  with assms(3) show "False"
+    by (simp add: eventually_False)
 qed
 
 text{* Need to prove closed(cball(x,e)) before deducing this as a corollary. *}
 
+lemma Lim_dist_ubound:
+  assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. dist a (f x) <= e) net"
+  shows "dist a l <= e"
+proof (rule ccontr)
+  assume "\<not> dist a l \<le> e"
+  then have "0 < dist a l - e" by simp
+  with assms(2) have "eventually (\<lambda>x. dist (f x) l < dist a l - e) net"
+    by (rule tendstoD)
+  with assms(3) have "eventually (\<lambda>x. dist a (f x) \<le> e \<and> dist (f x) l < dist a l - e) net"
+    by (rule eventually_conjI)
+  then obtain w where "dist a (f w) \<le> e" "dist (f w) l < dist a l - e"
+    using assms(1) eventually_happens by auto
+  hence "dist a (f w) + dist (f w) l < e + (dist a l - e)"
+    by (rule add_le_less_mono)
+  hence "dist a (f w) + dist (f w) l < dist a l"
+    by simp
+  also have "\<dots> \<le> dist a (f w) + dist (f w) l"
+    by (rule dist_triangle)
+  finally show False by simp
+qed
+
 lemma Lim_norm_ubound:
   fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   assumes "\<not>(trivial_limit net)" "(f ---> l) net" "eventually (\<lambda>x. norm(f x) <= e) net"
@@ -1453,76 +1440,15 @@
   shows "~(trivial_limit net) \<Longrightarrow> (f ---> l) net ==> Lim net f = l"
   unfolding Lim_def using Lim_unique[of net f] by auto
 
-text{* Limit under bilinear function (surprisingly tedious, but important) *}
-
-lemma norm_bound_lemma:
-  "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"
-proof-
-  assume e: "0 < e"
-  have th1: "(2 * norm x + 2 * norm y + 2) > 0" using norm_ge_zero[of x] norm_ge_zero[of y] by norm
-  hence th0: "0 < e / (2 * norm x + 2 * norm y + 2)"  using `e>0` using divide_pos_pos by auto
-  moreover
-  { fix x' y'
-    assume h: "norm (x' - x) < 1" "norm (x' - x) < e / (2 * norm x + 2 * norm y + 2)"
-      "norm (y' - y) < 1" "norm (y' - y) < e / (2 * norm x + 2 * norm y + 2)"
-    have th: "\<And>a b (c::real). a \<ge> 0 \<Longrightarrow> c \<ge> 0 \<Longrightarrow> a + (b + c) < e ==> b < e " by arith
-    from h have thx: "norm (x' - x) * norm y < e / 2"
-      using th0 th1 apply (simp add: field_simps)
-      apply (rule th) defer defer apply assumption
-      by (simp_all add: norm_ge_zero zero_le_mult_iff)
-
-    have "norm x' - norm x < 1" apply(rule le_less_trans)
-      using h(1) using norm_triangle_ineq2[of x' x] by auto
-    hence *:"norm x' < 1 + norm x"  by auto
-
-    have thy: "norm (y' - y) * norm x' < e / (2 * norm x + 2 * norm y + 2) * (1 + norm x)"
-      using mult_strict_mono'[OF h(4) * norm_ge_zero norm_ge_zero] by auto
-    also have "\<dots> \<le> e/2" apply simp unfolding divide_le_eq
-      using th1 th0 `e>0` by auto
-
-    finally have "norm x' * norm (y' - y) + norm (x' - x) * norm y < e"
-      using thx and e by (simp add: field_simps)  }
-  ultimately show ?thesis apply(rule_tac x="min 1 (e / 2 / (norm x + norm y + 1))" in exI) by auto
-qed
+text{* Limit under bilinear function *}
 
 lemma Lim_bilinear:
   fixes net :: "'a net" and h:: "real ^'m::finite \<Rightarrow> real ^'n::finite \<Rightarrow> real ^'p::finite"
   assumes "(f ---> l) net" and "(g ---> m) net" and "bilinear h"
   shows "((\<lambda>x. h (f x) (g x)) ---> (h l m)) net"
-proof -
-  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
-  { fix e::real assume "e>0"
-    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`
-      using norm_bound_lemma[of "e / B" l m] using divide_pos_pos by auto
-
-    have *:"\<And>x y. h (f x) (g x) - h l m = h (f x) (g x - m) + h (f x - l) m"
-      unfolding bilinear_rsub[OF assms(3)]
-      unfolding bilinear_lsub[OF assms(3)] by auto
-
-    have "eventually (\<lambda>x. dist (f x) l < d) net"
-      using assms(1) `d>0` by (rule tendstoD)
-    moreover
-    have "eventually (\<lambda>x. dist (g x) m < d) net"
-      using assms(2) `d>0` by (rule tendstoD)
-    ultimately
-    have "eventually (\<lambda>x. dist (f x) l < d \<and> dist (g x) m < d) net"
-      by (rule eventually_conjI)
-    moreover
-    { fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
-      hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
-	using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm  by auto
-      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"
-	using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]]
-	using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto
-      also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
-      finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
-    }
-    ultimately have "eventually (\<lambda>x. dist (h (f x) (g x)) (h l m) < e) net"
-      by (auto elim: eventually_rev_mono)
-  }
-  thus "((\<lambda>x. h (f x) (g x)) ---> h l m) net"
-    unfolding tendsto_iff by simp
-qed
+using `bilinear h` `(f ---> l) net` `(g ---> m) net`
+unfolding bilinear_conv_bounded_bilinear
+by (rule bounded_bilinear.tendsto)
 
 text{* These are special for limits out of the same vector space. *}
 
@@ -1535,31 +1461,41 @@
 
 lemma Lim_at_zero:
   fixes a :: "'a::real_normed_vector"
-  fixes l :: "'b::metric_space" (* FIXME: generalize to topological_space *)
+  fixes l :: "'b::topological_space"
   shows "(f ---> l) (at a) \<longleftrightarrow> ((\<lambda>x. f(a + x)) ---> l) (at 0)" (is "?lhs = ?rhs")
 proof
   assume "?lhs"
-  { fix e::real assume "e>0"
-    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
-    { fix x::"'a" assume "0 < dist x 0 \<and> dist x 0 < d"
-      hence "dist (f (a + x)) l < e" using d
-      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
+  { fix S assume "open S" "l \<in> S"
+    with `?lhs` have "eventually (\<lambda>x. f x \<in> S) (at a)"
+      by (rule topological_tendstoD)
+    then obtain d where d: "d>0" "\<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S"
+      unfolding Limits.eventually_at by fast
+    { fix x::"'a" assume "x \<noteq> 0 \<and> dist x 0 < d"
+      hence "f (a + x) \<in> S" using d
+      apply(erule_tac x="x+a" in allE)
+      by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
     }
-    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
+    hence "\<exists>d>0. \<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
+      using d(1) by auto
+    hence "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
+      unfolding Limits.eventually_at .
   }
-  thus "?rhs" unfolding Lim_at by auto
+  thus "?rhs" by (rule topological_tendstoI)
 next
   assume "?rhs"
-  { fix e::real assume "e>0"
-    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"
-      unfolding Lim_at by auto
-    { fix x::"'a" assume "0 < dist x a \<and> dist x a < d"
-      hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
+  { fix S assume "open S" "l \<in> S"
+    with `?rhs` have "eventually (\<lambda>x. f (a + x) \<in> S) (at 0)"
+      by (rule topological_tendstoD)
+    then obtain d where d: "d>0" "\<forall>x. x \<noteq> 0 \<and> dist x 0 < d \<longrightarrow> f (a + x) \<in> S"
+      unfolding Limits.eventually_at by fast
+    { fix x::"'a" assume "x \<noteq> a \<and> dist x a < d"
+      hence "f x \<in> S" using d apply(erule_tac x="x-a" in allE)
 	by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
     }
-    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
+    hence "\<exists>d>0. \<forall>x. x \<noteq> a \<and> dist x a < d \<longrightarrow> f x \<in> S" using d(1) by auto
+    hence "eventually (\<lambda>x. f x \<in> S) (at a)" unfolding Limits.eventually_at .
   }
-  thus "?lhs" unfolding Lim_at by auto
+  thus "?lhs" by (rule topological_tendstoI)
 qed
 
 text{* It's also sometimes useful to extract the limit point from the net.  *}
@@ -1615,10 +1551,9 @@
 qed
 
 lemma Lim_transform_eventually:
-  fixes l :: "'a::metric_space" (* FIXME: generalize to t2_space *)
-  shows "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
-  unfolding tendsto_iff
-  apply (clarify, drule spec, drule (1) mp)
+  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f ---> l) net ==> (g ---> l) net"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
   apply (erule (1) eventually_elim2, simp)
   done
 
@@ -1743,17 +1678,19 @@
   by (metis trans_le_add1 )
 
 lemma seq_offset_neg:
-  fixes l :: "'a::metric_space" (* TODO: generalize *)
-  shows "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
-  apply (simp add: Lim_sequentially)
+  "(f ---> l) sequentially ==> ((\<lambda>i. f(i - k)) ---> l) sequentially"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
+  apply (simp only: eventually_sequentially)
   apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k")
   apply metis
   by arith
 
 lemma seq_offset_rev:
-  fixes l :: "'a::metric_space" (* TODO: generalize *)
-  shows "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
-  apply (simp add: Lim_sequentially)
+  "((\<lambda>i. f(i + k)) ---> l) sequentially ==> (f ---> l) sequentially"
+  apply (rule topological_tendstoI)
+  apply (drule (2) topological_tendstoD)
+  apply (simp only: eventually_sequentially)
   apply (subgoal_tac "\<And>N k (n::nat). N + k <= n ==> N <= n - k \<and> (n - k) + k = n")
   by metis arith
 
@@ -1770,7 +1707,7 @@
 text{* More properties of closed balls. *}
 
 lemma closed_cball: "closed (cball x e)"
-unfolding cball_def closed_def Compl_eq_Diff_UNIV [symmetric]
+unfolding cball_def closed_def
 unfolding Collect_neg_eq [symmetric] not_le
 apply (clarsimp simp add: open_dist, rename_tac y)
 apply (rule_tac x="dist x y - e" in exI, clarsimp)
@@ -1802,7 +1739,6 @@
 
 lemma islimpt_ball:
   fixes x y :: "'a::{real_normed_vector,perfect_space}"
-    (* FIXME: generalize to metric_space *)
   shows "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
 proof
   assume "?lhs"
@@ -1810,7 +1746,7 @@
     hence *:"ball x e = {}" using ball_eq_empty[of x e] by auto
     have False using `?lhs` unfolding * using islimpt_EMPTY[of y] by auto
   }
-  hence "e > 0" by (metis dlo_simps(3))
+  hence "e > 0" by (metis not_less)
   moreover
   have "y \<in> cball x e" using closed_cball[of x e] islimpt_subset[of y "ball x e" "cball x e"] ball_subset_cball[of x e] `?lhs` unfolding closed_limpt by auto
   ultimately show "?rhs" by auto
@@ -1869,12 +1805,56 @@
   thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto
 qed
 
+lemma closure_ball_lemma:
+  fixes x y :: "'a::real_normed_vector"
+  assumes "x \<noteq> y" shows "y islimpt ball x (dist x y)"
+proof (rule islimptI)
+  fix T assume "y \<in> T" "open T"
+  then obtain r where "0 < r" "\<forall>z. dist z y < r \<longrightarrow> z \<in> T"
+    unfolding open_dist by fast
+  (* choose point between x and y, within distance r of y. *)
+  def k \<equiv> "min 1 (r / (2 * dist x y))"
+  def z \<equiv> "y + scaleR k (x - y)"
+  have z_def2: "z = x + scaleR (1 - k) (y - x)"
+    unfolding z_def by (simp add: algebra_simps)
+  have "dist z y < r"
+    unfolding z_def k_def using `0 < r`
+    by (simp add: dist_norm norm_scaleR min_def)
+  hence "z \<in> T" using `\<forall>z. dist z y < r \<longrightarrow> z \<in> T` by simp
+  have "dist x z < dist x y"
+    unfolding z_def2 dist_norm
+    apply (simp add: norm_scaleR norm_minus_commute)
+    apply (simp only: dist_norm [symmetric])
+    apply (subgoal_tac "\<bar>1 - k\<bar> * dist x y < 1 * dist x y", simp)
+    apply (rule mult_strict_right_mono)
+    apply (simp add: k_def divide_pos_pos zero_less_dist_iff `0 < r` `x \<noteq> y`)
+    apply (simp add: zero_less_dist_iff `x \<noteq> y`)
+    done
+  hence "z \<in> ball x (dist x y)" by simp
+  have "z \<noteq> y"
+    unfolding z_def k_def using `x \<noteq> y` `0 < r`
+    by (simp add: min_def)
+  show "\<exists>z\<in>ball x (dist x y). z \<in> T \<and> z \<noteq> y"
+    using `z \<in> ball x (dist x y)` `z \<in> T` `z \<noteq> y`
+    by fast
+qed
+
 lemma closure_ball:
-  fixes x y :: "'a::{real_normed_vector,perfect_space}"
-    (* FIXME: generalize to metric_space *)
-  shows "0 < e ==> (closure(ball x e) = cball x e)"
-  apply (simp add: closure_def islimpt_ball expand_set_eq)
-  by arith
+  fixes x :: "'a::real_normed_vector"
+  shows "0 < e \<Longrightarrow> closure (ball x e) = cball x e"
+apply (rule equalityI)
+apply (rule closure_minimal)
+apply (rule ball_subset_cball)
+apply (rule closed_cball)
+apply (rule subsetI, rename_tac y)
+apply (simp add: le_less [where 'a=real])
+apply (erule disjE)
+apply (rule subsetD [OF closure_subset], simp)
+apply (simp add: closure_def)
+apply clarify
+apply (rule closure_ball_lemma)
+apply (simp add: zero_less_dist_iff)
+done
 
 lemma interior_cball:
   fixes x :: "real ^ _" (* FIXME: generalize *)
@@ -1962,24 +1942,30 @@
 text{* For points in the interior, localization of limits makes no difference.   *}
 
 lemma eventually_within_interior:
-  fixes x :: "'a::metric_space"
   assumes "x \<in> interior S"
   shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
 proof-
-  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
-  { 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
-    hence "?rhs" unfolding eventually_at using e by (auto simp add: dist_commute intro!: add exI[of _ "min e d"])
+  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
+    unfolding interior_def by fast
+  { assume "?lhs"
+    then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
+      unfolding Limits.eventually_within Limits.eventually_at_topological
+      by auto
+    with T have "open (A \<inter> T)" "x \<in> A \<inter> T" "\<forall>y\<in>(A \<inter> T). y \<noteq> x \<longrightarrow> P y"
+      by auto
+    then have "?rhs"
+      unfolding Limits.eventually_at_topological by auto
   } moreover
-  { assume "?rhs" hence "?lhs" unfolding eventually_within eventually_at by auto
+  { assume "?rhs" hence "?lhs"
+      unfolding Limits.eventually_within
+      by (auto elim: eventually_elim1)
   } ultimately
-  show "?thesis" by auto
+  show "?thesis" ..
 qed
 
 lemma lim_within_interior:
-  fixes x :: "'a::metric_space"
-  fixes l :: "'b::metric_space" (* TODO: generalize *)
-  shows "x \<in> interior S  ==> ((f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x))"
-  by (simp add: tendsto_iff eventually_within_interior)
+  "x \<in> interior S \<Longrightarrow> (f ---> l) (at x within S) \<longleftrightarrow> (f ---> l) (at x)"
+  unfolding tendsto_def by (simp add: eventually_within_interior)
 
 lemma netlimit_within_interior:
   fixes x :: "'a::{perfect_space, real_normed_vector}"
@@ -1996,8 +1982,21 @@
 
   (* FIXME: This has to be unified with BSEQ!! *)
 definition
-  bounded :: "'a::real_normed_vector set \<Rightarrow> bool" where
-  "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x <= a)"
+  bounded :: "'a::metric_space set \<Rightarrow> bool" where
+  "bounded S \<longleftrightarrow> (\<exists>x e. \<forall>y\<in>S. dist x y \<le> e)"
+
+lemma bounded_any_center: "bounded S \<longleftrightarrow> (\<exists>e. \<forall>y\<in>S. dist a y \<le> e)"
+unfolding bounded_def
+apply safe
+apply (rule_tac x="dist a x + e" in exI, clarify)
+apply (drule (1) bspec)
+apply (erule order_trans [OF dist_triangle add_left_mono])
+apply auto
+done
+
+lemma bounded_iff: "bounded S \<longleftrightarrow> (\<exists>a. \<forall>x\<in>S. norm x \<le> a)"
+unfolding bounded_any_center [where a=0]
+by (simp add: dist_norm)
 
 lemma bounded_empty[simp]: "bounded {}" by (simp add: bounded_def)
 lemma bounded_subset: "bounded T \<Longrightarrow> S \<subseteq> T ==> bounded S"
@@ -2008,16 +2007,17 @@
 
 lemma bounded_closure[intro]: assumes "bounded S" shows "bounded(closure S)"
 proof-
-  from assms obtain a where a:"\<forall>x\<in>S. norm x \<le> a" unfolding bounded_def by auto
-  { fix x assume "x\<in>closure S"
-    then obtain xa where xa:"\<forall>n. xa n \<in> S"  "(xa ---> x) sequentially" unfolding closure_sequential by auto
-    have "\<forall>n. xa n \<in> S \<longrightarrow> norm (xa n) \<le> a" using a by simp
-    hence "eventually (\<lambda>n. norm (xa n) \<le> a) sequentially"
-      by (rule eventually_mono, simp add: xa(1))
-    have "norm x \<le> a"
-      apply (rule Lim_norm_ubound[of sequentially xa x a])
+  from assms obtain x and a where a: "\<forall>y\<in>S. dist x y \<le> a" unfolding bounded_def by auto
+  { fix y assume "y \<in> closure S"
+    then obtain f where f: "\<forall>n. f n \<in> S"  "(f ---> y) sequentially"
+      unfolding closure_sequential by auto
+    have "\<forall>n. f n \<in> S \<longrightarrow> dist x (f n) \<le> a" using a by simp
+    hence "eventually (\<lambda>n. dist x (f n) \<le> a) sequentially"
+      by (rule eventually_mono, simp add: f(1))
+    have "dist x y \<le> a"
+      apply (rule Lim_dist_ubound [of sequentially f])
       apply (rule trivial_limit_sequentially)
-      apply (rule xa(2))
+      apply (rule f(2))
       apply fact
       done
   }
@@ -2026,11 +2026,9 @@
 
 lemma bounded_cball[simp,intro]: "bounded (cball x e)"
   apply (simp add: bounded_def)
-  apply (rule exI[where x="norm x + e"])
-  apply (clarsimp simp add: Ball_def dist_norm, rename_tac y)
-  apply (subgoal_tac "norm y - norm x \<le> e", simp)
-  apply (rule order_trans [OF norm_triangle_ineq2])
-  apply (simp add: norm_minus_commute)
+  apply (rule_tac x=x in exI)
+  apply (rule_tac x=e in exI)
+  apply auto
   done
 
 lemma bounded_ball[simp,intro]: "bounded(ball x e)"
@@ -2038,22 +2036,31 @@
 
 lemma finite_imp_bounded[intro]: assumes "finite S" shows "bounded S"
 proof-
-  { fix x F assume as:"bounded F"
-    then obtain a where "\<forall>x\<in>F. norm x \<le> a" unfolding bounded_def by auto
-    hence "bounded (insert x F)" unfolding bounded_def by(auto intro!: add exI[of _ "max a (norm x)"])
+  { fix a F assume as:"bounded F"
+    then obtain x e where "\<forall>y\<in>F. dist x y \<le> e" unfolding bounded_def by auto
+    hence "\<forall>y\<in>(insert a F). dist x y \<le> max e (dist x a)" by auto
+    hence "bounded (insert a F)" unfolding bounded_def by (intro exI)
   }
   thus ?thesis using finite_induct[of S bounded]  using bounded_empty assms by auto
 qed
 
 lemma bounded_Un[simp]: "bounded (S \<union> T) \<longleftrightarrow> bounded S \<and> bounded T"
   apply (auto simp add: bounded_def)
-  by (rule_tac x="max a aa" in exI, auto)
+  apply (rename_tac x y r s)
+  apply (rule_tac x=x in exI)
+  apply (rule_tac x="max r (dist x y + s)" in exI)
+  apply (rule ballI, rename_tac z, safe)
+  apply (drule (1) bspec, simp)
+  apply (drule (1) bspec)
+  apply (rule min_max.le_supI2)
+  apply (erule order_trans [OF dist_triangle add_left_mono])
+  done
 
 lemma bounded_Union[intro]: "finite F \<Longrightarrow> (\<forall>S\<in>F. bounded S) \<Longrightarrow> bounded(\<Union>F)"
   by (induct rule: finite_induct[of F], auto)
 
 lemma bounded_pos: "bounded S \<longleftrightarrow> (\<exists>b>0. \<forall>x\<in> S. norm x <= b)"
-  apply (simp add: bounded_def)
+  apply (simp add: bounded_iff)
   apply (subgoal_tac "\<And>x (y::real). 0 < 1 + abs y \<and> (x <= y \<longrightarrow> x <= 1 + abs y)")
   by metis arith
 
@@ -2067,13 +2074,16 @@
 lemma bounded_insert[intro]:"bounded(insert x S) \<longleftrightarrow> bounded S"
   by (metis Diff_cancel Un_empty_right Un_insert_right bounded_Un bounded_subset finite.emptyI finite_imp_bounded infinite_remove subset_insertI)
 
-lemma bot_bounded_UNIV[simp, intro]: "~(bounded (UNIV:: (real^'n::finite) set))"
+lemma not_bounded_UNIV[simp, intro]:
+  "\<not> bounded (UNIV :: 'a::{real_normed_vector, perfect_space} set)"
 proof(auto simp add: bounded_pos not_le)
+  obtain x :: 'a where "x \<noteq> 0"
+    using perfect_choose_dist [OF zero_less_one] by fast
   fix b::real  assume b: "b >0"
   have b1: "b +1 \<ge> 0" using b by simp
-  then obtain x:: "real^'n" where "norm x = b + 1" using vector_choose_size[of "b+1"] by blast
-  hence "norm x > b" using b by simp
-  then show "\<exists>(x::real^'n). b < norm x"  by blast
+  with `x \<noteq> 0` have "b < norm (scaleR (b + 1) (sgn x))"
+    by (simp add: norm_scaleR norm_sgn)
+  then show "\<exists>x::'a. b < norm x" ..
 qed
 
 lemma bounded_linear_image:
@@ -2098,7 +2108,9 @@
   apply (rule bounded_linear_image, assumption)
   by (rule linear_compose_cmul, rule linear_id[unfolded id_def])
 
-lemma bounded_translation: assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
+lemma bounded_translation:
+  fixes S :: "'a::real_normed_vector set"
+  assumes "bounded S" shows "bounded ((\<lambda>x. a + x) ` S)"
 proof-
   from assms obtain b where b:"b>0" "\<forall>x\<in>S. norm x \<le> b" unfolding bounded_pos by auto
   { fix x assume "x\<in>S"
@@ -2114,7 +2126,7 @@
 lemma bounded_vec1:
   fixes S :: "real set"
   shows "bounded(vec1 ` S) \<longleftrightarrow>  (\<exists>a. \<forall>x\<in>S. abs x <= a)"
-  by (simp add: bounded_def forall_vec1 norm_vec1 vec1_in_image_vec1)
+  by (simp add: bounded_iff forall_vec1 norm_vec1 vec1_in_image_vec1)
 
 lemma bounded_has_rsup: assumes "bounded(vec1 ` S)" "S \<noteq> {}"
   shows "\<forall>x\<in>S. x <= rsup S" and "\<forall>b. (\<forall>x\<in>S. x <= b) \<longrightarrow> rsup S <= b"
@@ -2208,6 +2220,30 @@
    (\<forall>f. (\<forall>n::nat. f n \<in> S) \<longrightarrow>
        (\<exists>l\<in>S. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f o r) ---> l) sequentially))"
 
+text {*
+  A metric space (or topological vector space) is said to have the
+  Heine-Borel property if every closed and bounded subset is compact.
+*}
+
+class heine_borel =
+  assumes bounded_imp_convergent_subsequence:
+    "bounded s \<Longrightarrow> \<forall>n::nat. f n \<in> s
+      \<Longrightarrow> \<exists>l r. (\<forall>m n. m < n --> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially"
+
+lemma bounded_closed_imp_compact:
+  fixes s::"'a::heine_borel set"
+  assumes "bounded s" and "closed s" shows "compact s"
+proof (unfold compact_def, clarify)
+  fix f :: "nat \<Rightarrow> 'a" assume f: "\<forall>n. f n \<in> s"
+  obtain l r where r: "\<forall>m n. m < n \<longrightarrow> r m < r n" and l: "((f \<circ> r) ---> l) sequentially"
+    using bounded_imp_convergent_subsequence [OF `bounded s` `\<forall>n. f n \<in> s`] by auto
+  from f have fr: "\<forall>n. (f \<circ> r) n \<in> s" by simp
+  have "l \<in> s" using `closed s` fr l
+    unfolding closed_sequential_limits by blast
+  show "\<exists>l\<in>s. \<exists>r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially"
+    using `l \<in> s` r l by blast
+qed
+
 lemma monotone_bigger: fixes r::"nat\<Rightarrow>nat"
   assumes "\<forall>m n::nat. m < n --> r m < r n"
   shows "n \<le> r n"
@@ -2219,6 +2255,12 @@
   ultimately show "Suc n \<le> r (Suc n)" by auto
 qed
 
+lemma eventually_subsequence:
+  assumes r: "\<forall>m n. m < n \<longrightarrow> r m < r n"
+  shows "eventually P sequentially \<Longrightarrow> eventually (\<lambda>n. P (r n)) sequentially"
+unfolding eventually_sequentially
+by (metis monotone_bigger [OF r] le_trans)
+
 lemma lim_subsequence:
   fixes l :: "'a::metric_space" (* TODO: generalize *)
   shows "\<forall>m n. m < n \<longrightarrow> r m < r n \<Longrightarrow> (s ---> l) sequentially \<Longrightarrow> ((s o r) ---> l) sequentially"
@@ -2264,87 +2306,97 @@
   unfolding abs_minus_cancel by(rule_tac x="-l" in exI)auto
 
 lemma compact_real_lemma:
- assumes "\<forall>n::nat. abs(s n) \<le> b"
-  shows "\<exists>l r. (\<forall>m n::nat. m < n --> r m < r n) \<and>
-           (\<forall>e>0::real. \<exists>N. \<forall>n\<ge>N. (abs(s (r n) - l) < e))"
+  assumes "\<forall>n::nat. abs(s n) \<le> b"
+  shows "\<exists>(l::real) r. (\<forall>m n::nat. m < n --> r m < r n) \<and> ((s \<circ> r) ---> l) sequentially"
 proof-
   obtain r where r:"\<forall>m n::nat. m < n \<longrightarrow> r m < r n"
     "(\<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))"
     using seq_monosub[of s] by (auto simp add: subseq_def monoseq_def)
-  thus ?thesis using convergent_bounded_monotone[of "s o r" b] and assms by auto
-qed
+  thus ?thesis using convergent_bounded_monotone[of "s o r" b] and assms
+    unfolding tendsto_iff dist_norm eventually_sequentially by auto
+qed
+
+instance real :: heine_borel
+proof
+  fix s :: "real set" and f :: "nat \<Rightarrow> real"
+  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+  then obtain b where b: "\<forall>n. abs (f n) \<le> b"
+    unfolding bounded_iff by auto
+  obtain l :: real and r :: "nat \<Rightarrow> nat" where
+    r: "\<forall>m n. m < n \<longrightarrow> r m < r n" and l: "((f \<circ> r) ---> l) sequentially"
+    using compact_real_lemma [OF b] by auto
+  thus "\<exists>l r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially"
+    by auto
+qed
+
+lemma bounded_component: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)"
+unfolding bounded_def
+apply clarify
+apply (rule_tac x="x $ i" in exI)
+apply (rule_tac x="e" in exI)
+apply clarify
+apply (rule order_trans [OF dist_nth_le], simp)
+done
 
 lemma compact_lemma:
-  assumes "bounded s" and "\<forall>n. (x::nat \<Rightarrow>real^'a::finite) n \<in> s"
+  fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n::finite"
+  assumes "bounded s" and "\<forall>n. f n \<in> s"
   shows "\<forall>d.
-        \<exists>l::(real^'a::finite). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
-        (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
-proof-
-  obtain b where b:"\<forall>x\<in>s. norm x \<le> b" using assms(1)[unfolded bounded_def] by auto
-  { { fix i::'a
-      { fix n::nat
-	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 }
-      hence "\<forall>n. \<bar>x n $ i\<bar> \<le> b" by auto
-    } note b' = this
-
-    fix d::"'a set" have "finite d" by simp
-    hence "\<exists>l::(real^'a). \<exists> r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
-        (\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>d. \<bar>x (r n) $ i - l $ i\<bar> < e)"
-    proof(induct d) case empty thus ?case by auto
-    next case (insert k d)
-	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"
-	  using insert(3) by auto
-	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"
-	  using b'[of k] and compact_real_lemma[of "\<lambda>i. ((x \<circ> r1) i)$k" b] by auto
-	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
-	moreover
-	def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::real^'a"
-	{ fix e::real assume "e>0"
-	  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
-	  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
-	  { fix n assume n:"n\<ge> N1 + N2"
-	    fix i assume i:"i\<in>(insert k d)"
-	    hence "\<bar>x (r n) $ i - l $ i\<bar> < e"
-	      using N2[THEN spec[where x="n"]] and n
- 	      using N1[THEN spec[where x="r2 n"]] and n
-	      using monotone_bigger[OF r] and i
-	      unfolding l_def and r_def
-	      using monotone_bigger[OF r2, of n] by auto  }
-	  hence "\<exists>N. \<forall>n\<ge>N. \<forall>i\<in>(insert k d). \<bar>x (r n) $ i - l $ i\<bar> < e" by blast	}
-	ultimately show ?case by auto
-    qed  }
-  thus ?thesis by auto
-qed
-
-lemma bounded_closed_imp_compact: fixes s::"(real^'a::finite) set"
-  assumes "bounded s" and "closed s"
-  shows "compact s"
-proof-
-  let ?d = "UNIV::'a set"
-  { fix f assume as:"\<forall>n::nat. f n \<in> s"
-    obtain l::"real^'a" and r where r:"\<forall>n m::nat. m < n \<longrightarrow> r m < r n"
-      and lr:"\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>i\<in>?d. \<bar>f (r n) $ i - l $ i\<bar> < e"
-      using compact_lemma[OF assms(1) as, THEN spec[where x="?d"]] by auto
+        \<exists>l r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
+        (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
+proof
+  fix d::"'n set" have "finite d" by simp
+  thus "\<exists>l::'a ^ 'n. \<exists>r. (\<forall>n m::nat. m < n --> r m < r n) \<and>
+      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
+  proof(induct d) case empty thus ?case by auto
+  next case (insert k d)
+    have s': "bounded ((\<lambda>x. x $ k) ` s)" using `bounded s` by (rule bounded_component)
+    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"
+      using insert(3) by auto
+    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` s" using `\<forall>n. f n \<in> s` by simp
+    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"
+      using bounded_imp_convergent_subsequence[OF s' f'] unfolding o_def by auto
+    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
+    moreover
+    def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
     { fix e::real assume "e>0"
-      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
-      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
-      { fix n assume n:"n\<ge>N"
-	hence "finite ?d"  "?d \<noteq> {}" by auto
-	moreover
-	{ fix i assume i:"i \<in> ?d"
-	  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]]
-	    by auto  }
-	ultimately have "(\<Sum>i \<in> ?d. \<bar>((f \<circ> r) n - l) $ i\<bar>)
-	  < (\<Sum>i \<in> ?d. e / real_of_nat (card ?d))"
-	  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
-	hence "(\<Sum>i \<in> ?d. \<bar>((f \<circ> r) n - l) $ i\<bar>) < e" unfolding setsum_constant by auto
-	hence "dist ((f \<circ> r) n) l < e" unfolding dist_norm using norm_le_l1[of "(f \<circ> r) n - l"] by auto  }
-      hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> r) n) l < e" by auto  }
-    hence *:"((f \<circ> r) ---> l) sequentially" unfolding Lim_sequentially by auto
-    moreover have "l\<in>s"
-      using assms(2)[unfolded closed_sequential_limits, THEN spec[where x="f \<circ> r"], THEN spec[where x=l]] and * and as by auto
-    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  }
-  thus ?thesis unfolding compact_def by auto
+      from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" by blast
+      from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" by (rule tendstoD)
+      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
+        by (rule eventually_subsequence)
+      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially"
+        using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
+    }
+    ultimately show ?case by auto
+  qed
+qed
+
+instance "^" :: (heine_borel, finite) heine_borel
+proof
+  fix s :: "('a ^ 'b) set" and f :: "nat \<Rightarrow> 'a ^ 'b"
+  assume s: "bounded s" and f: "\<forall>n. f n \<in> s"
+  then obtain l r where r: "\<forall>n m::nat. m < n --> r m < r n"
+    and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially"
+    using compact_lemma [OF s f] by blast
+  let ?d = "UNIV::'b set"
+  { fix e::real assume "e>0"
+    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
+    with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially"
+      by simp
+    moreover
+    { fix n assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))"
+      have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))"
+        unfolding dist_vector_def using zero_le_dist by (rule setL2_le_setsum)
+      also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))"
+        by (rule setsum_strict_mono) (simp_all add: n)
+      finally have "dist (f (r n)) l < e" by simp
+    }
+    ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially"
+      by (rule eventually_elim1)
+  }
+  hence *:"((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp
+  with r show "\<exists>l r. (\<forall>m n. m < n \<longrightarrow> r m < r n) \<and> ((f \<circ> r) ---> l) sequentially" by auto
 qed
 
 subsection{* Completeness. *}
@@ -2353,7 +2405,9 @@
   "Cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
 unfolding Cauchy_def by blast
 
-definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> Cauchy f
+definition
+  complete :: "'a::metric_space set \<Rightarrow> bool" where
+  "complete s \<longleftrightarrow> (\<forall>f. (\<forall>n. f n \<in> s) \<and> Cauchy f
                       --> (\<exists>l \<in> s. (f ---> l) sequentially))"
 
 lemma cauchy: "Cauchy s \<longleftrightarrow> (\<forall>e>0.\<exists> N::nat. \<forall>n\<ge>N. dist(s n)(s N) < e)" (is "?lhs = ?rhs")
@@ -2394,16 +2448,13 @@
 proof-
   from assms obtain N::nat where "\<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (s m) (s n) < 1" unfolding cauchy_def apply(erule_tac x= 1 in allE) by auto
   hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
-  { fix n::nat assume "n\<ge>N"
-    hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
-      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)
-  }
-  hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
   moreover
   have "bounded (s ` {0..N})" using finite_imp_bounded[of "s ` {1..N}"] by auto
-  then obtain a where a:"\<forall>x\<in>s ` {0..N}. norm x \<le> a" unfolding bounded_def by auto
-  ultimately show "?thesis" unfolding bounded_def
-    apply(rule_tac x="max a (norm (s N) + 1)" in exI) apply auto
+  then obtain a where a:"\<forall>x\<in>s ` {0..N}. dist (s N) x \<le> a"
+    unfolding bounded_any_center [where a="s N"] by auto
+  ultimately show "?thesis"
+    unfolding bounded_any_center [where a="s N"]
+    apply(rule_tac x="max a 1" in exI) apply auto
     apply(erule_tac x=n in allE) apply(erule_tac x=n in ballE) by auto
 qed
 
@@ -2432,24 +2483,48 @@
   thus ?thesis unfolding complete_def by auto
 qed
 
-lemma complete_univ:
- "complete UNIV"
+instance heine_borel < complete_space
+proof
+  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
+  hence "bounded (range f)" unfolding image_def
+    using cauchy_imp_bounded [of f] by auto
+  hence "compact (closure (range f))"
+    using bounded_closed_imp_compact [of "closure (range f)"] by auto
+  hence "complete (closure (range f))"
+    using compact_imp_complete by auto
+  moreover have "\<forall>n. f n \<in> closure (range f)"
+    using closure_subset [of "range f"] by auto
+  ultimately have "\<exists>l\<in>closure (range f). (f ---> l) sequentially"
+    using `Cauchy f` unfolding complete_def by auto
+  then show "convergent f"
+    unfolding convergent_def LIMSEQ_conv_tendsto [symmetric] by auto
+qed
+
+lemma complete_univ: "complete (UNIV :: 'a::complete_space set)"
 proof(simp add: complete_def, rule, rule)
-  fix f::"nat \<Rightarrow> real^'n::finite" assume "Cauchy f"
-  hence "bounded (f`UNIV)" using cauchy_imp_bounded[of f] unfolding image_def by auto
-  hence "compact (closure (f`UNIV))"  using bounded_closed_imp_compact[of "closure (range f)"] by auto
-  hence "complete (closure (range f))" using compact_imp_complete by auto
-  thus "\<exists>l. (f ---> l) sequentially" unfolding complete_def[of "closure (range f)"] using `Cauchy f` unfolding closure_def  by auto
-qed
-
-lemma complete_eq_closed: "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
+  fix f :: "nat \<Rightarrow> 'a" assume "Cauchy f"
+  hence "convergent f" by (rule Cauchy_convergent)
+  hence "\<exists>l. f ----> l" unfolding convergent_def .  
+  thus "\<exists>l. (f ---> l) sequentially" unfolding LIMSEQ_conv_tendsto .
+qed
+
+lemma complete_imp_closed: assumes "complete s" shows "closed s"
+proof -
+  { fix x assume "x islimpt s"
+    then obtain f where f: "\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially"
+      unfolding islimpt_sequential by auto
+    then obtain l where l: "l\<in>s" "(f ---> l) sequentially"
+      using `complete s`[unfolded complete_def] using convergent_imp_cauchy[of f x] by auto
+    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto
+  }
+  thus "closed s" unfolding closed_limpt by auto
+qed
+
+lemma complete_eq_closed:
+  fixes s :: "'a::complete_space set"
+  shows "complete s \<longleftrightarrow> closed s" (is "?lhs = ?rhs")
 proof
-  assume ?lhs
-  { fix x assume "x islimpt s"
-    then obtain f where f:"\<forall>n. f n \<in> s - {x}" "(f ---> x) sequentially" unfolding islimpt_sequential by auto
-    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
-    hence "x \<in> s"  using Lim_unique[of sequentially f l x] trivial_limit_sequentially f(2) by auto  }
-  thus ?rhs unfolding closed_limpt by auto
+  assume ?lhs thus ?rhs by (rule complete_imp_closed)
 next
   assume ?rhs
   { fix f assume as:"\<forall>n::nat. f n \<in> s" "Cauchy f"
@@ -2459,8 +2534,7 @@
 qed
 
 lemma convergent_eq_cauchy:
-  fixes s :: "nat \<Rightarrow> real ^ 'n::finite"
-    (* FIXME: generalize to complete metric spaces *)
+  fixes s :: "nat \<Rightarrow> 'a::complete_space"
   shows "(\<exists>l. (s ---> l) sequentially) \<longleftrightarrow> Cauchy s" (is "?lhs = ?rhs")
 proof
   assume ?lhs then obtain l where "(s ---> l) sequentially" by auto
@@ -2470,9 +2544,9 @@
 qed
 
 lemma convergent_imp_bounded:
-  fixes s :: "nat \<Rightarrow> real ^ 'n::finite" (* FIXME: generalize *)
+  fixes s :: "nat \<Rightarrow> 'a::metric_space"
   shows "(s ---> l) sequentially ==> bounded (s ` (UNIV::(nat set)))"
-  using convergent_eq_cauchy[of s]
+  using convergent_imp_cauchy[of s]
   using cauchy_imp_bounded[of s]
   unfolding image_def
   by auto
@@ -2603,28 +2677,31 @@
 
 subsection{* Complete the chain of compactness variants. *}
 
-primrec helper_2::"(real \<Rightarrow> 'a::real_normed_vector) \<Rightarrow> nat \<Rightarrow> 'a" where
+primrec helper_2::"(real \<Rightarrow> 'a::metric_space) \<Rightarrow> nat \<Rightarrow> 'a" where
   "helper_2 beyond 0 = beyond 0" |
-  "helper_2 beyond (Suc n) = beyond (norm (helper_2 beyond n) + 1 )"
-
-lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::real_normed_vector set"
+  "helper_2 beyond (Suc n) = beyond (dist arbitrary (helper_2 beyond n) + 1 )"
+
+lemma bolzano_weierstrass_imp_bounded: fixes s::"'a::metric_space set"
   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
   shows "bounded s"
 proof(rule ccontr)
   assume "\<not> bounded s"
-  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> norm (beyond a) \<le> a"
-    unfolding bounded_def apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> norm x \<le> a"] by auto
-  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. norm (beyond a) > a" unfolding linorder_not_le by auto
+  then obtain beyond where "\<forall>a. beyond a \<in>s \<and> \<not> dist arbitrary (beyond a) \<le> a"
+    unfolding bounded_any_center [where a=arbitrary]
+    apply simp using choice[of "\<lambda>a x. x\<in>s \<and> \<not> dist arbitrary x \<le> a"] by auto
+  hence beyond:"\<And>a. beyond a \<in>s" "\<And>a. dist arbitrary (beyond a) > a"
+    unfolding linorder_not_le by auto
   def x \<equiv> "helper_2 beyond"
 
   { fix m n ::nat assume "m<n"
-    hence "norm (x m) + 1 < norm (x n)"
+    hence "dist arbitrary (x m) + 1 < dist arbitrary (x n)"
     proof(induct n)
       case 0 thus ?case by auto
     next
       case (Suc n)
-      have *:"norm (x n) + 1 < norm (x (Suc n))" unfolding x_def and helper_2.simps
-	using beyond(2)[of "norm (helper_2 beyond n) + 1"] by auto
+      have *:"dist arbitrary (x n) + 1 < dist arbitrary (x (Suc n))"
+        unfolding x_def and helper_2.simps
+	using beyond(2)[of "dist arbitrary (helper_2 beyond n) + 1"] by auto
       thus ?case proof(cases "m < n")
 	case True thus ?thesis using Suc and * by auto
       next
@@ -2636,12 +2713,12 @@
     have "1 < dist (x m) (x n)"
     proof(cases "m<n")
       case True
-      hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
-      thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_norm using norm_triangle_sub[of "x n" "x m"] by auto
+      hence "1 < dist arbitrary (x n) - dist arbitrary (x m)" using *[of m n] by auto
+      thus ?thesis using dist_triangle [of arbitrary "x n" "x m"] by arith
     next
       case False hence "n<m" using `m\<noteq>n` by auto
-      hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
-      thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_norm using norm_triangle_sub[of "x m" "x n"] by auto
+      hence "1 < dist arbitrary (x m) - dist arbitrary (x n)" using *[of n m] by auto
+      thus ?thesis using dist_triangle2 [of arbitrary "x m" "x n"] by arith
     qed  } note ** = this
   { fix a b assume "x a = x b" "a \<noteq> b"
     hence False using **[of a b] by auto  }
@@ -2712,13 +2789,13 @@
       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
       thus "l\<in>s" using sequence_unique_limpt[of x l l'] using as cas by auto
     qed  }
-  thus ?thesis unfolding closed_sequential_limits by auto (* FIXME: simp_depth_limit exceeded *)
+  thus ?thesis unfolding closed_sequential_limits by fast
 qed
 
 text{* Hence express everything as an equivalence.   *}
 
 lemma compact_eq_heine_borel:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   shows "compact s \<longleftrightarrow>
            (\<forall>f. (\<forall>t \<in> f. open t) \<and> s \<subseteq> (\<Union> f)
                --> (\<exists>f'. f' \<subseteq> f \<and> finite f' \<and> s \<subseteq> (\<Union> f')))" (is "?lhs = ?rhs")
@@ -2732,7 +2809,7 @@
 qed
 
 lemma compact_eq_bolzano_weierstrass:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   shows "compact s \<longleftrightarrow> (\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t))" (is "?lhs = ?rhs")
 proof
   assume ?lhs thus ?rhs unfolding compact_eq_heine_borel using heine_borel_imp_bolzano_weierstrass[of s] by auto
@@ -2741,7 +2818,7 @@
 qed
 
 lemma compact_eq_bounded_closed:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   shows "compact s \<longleftrightarrow> bounded s \<and> closed s"  (is "?lhs = ?rhs")
 proof
   assume ?lhs thus ?rhs unfolding compact_eq_bolzano_weierstrass using bolzano_weierstrass_imp_bounded bolzano_weierstrass_imp_closed by auto
@@ -2750,16 +2827,30 @@
 qed
 
 lemma compact_imp_bounded:
-  fixes s :: "(real^ _) set"
+  fixes s :: "'a::metric_space set"
   shows "compact s ==> bounded s"
-  unfolding compact_eq_bounded_closed
-  by simp
+proof -
+  assume "compact s"
+  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')"
+    by (rule compact_imp_heine_borel)
+  hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
+    using heine_borel_imp_bolzano_weierstrass[of s] by auto
+  thus "bounded s"
+    by (rule bolzano_weierstrass_imp_bounded)
+qed
 
 lemma compact_imp_closed:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::metric_space set"
   shows "compact s ==> closed s"
-  unfolding compact_eq_bounded_closed
-  by simp
+proof -
+  assume "compact s"
+  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')"
+    by (rule compact_imp_heine_borel)
+  hence "\<forall>t. infinite t \<and> t \<subseteq> s \<longrightarrow> (\<exists>x \<in> s. x islimpt t)"
+    using heine_borel_imp_bolzano_weierstrass[of s] by auto
+  thus "closed s"
+    by (rule bolzano_weierstrass_imp_closed)
+qed
 
 text{* In particular, some common special cases. *}
 
@@ -2768,9 +2859,11 @@
   unfolding compact_def
   by simp
 
+(* TODO: can any of the next 3 lemmas be generalized to metric spaces? *)
+
   (* FIXME : Rename *)
 lemma compact_union[intro]:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::heine_borel set"
   shows "compact s \<Longrightarrow> compact t ==> compact (s \<union> t)"
   unfolding compact_eq_bounded_closed
   using bounded_Un[of s t]
@@ -2778,7 +2871,7 @@
   by simp
 
 lemma compact_inter[intro]:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::heine_borel set"
   shows "compact s \<Longrightarrow> compact t ==> compact (s \<inter> t)"
   unfolding compact_eq_bounded_closed
   using bounded_Int[of s t]
@@ -2786,7 +2879,7 @@
   by simp
 
 lemma compact_inter_closed[intro]:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::heine_borel set"
   shows "compact s \<Longrightarrow> closed t ==> compact (s \<inter> t)"
   unfolding compact_eq_bounded_closed
   using closed_Int[of s t]
@@ -2794,7 +2887,7 @@
   by blast
 
 lemma closed_inter_compact[intro]:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::heine_borel set"
   shows "closed s \<Longrightarrow> compact t ==> compact (s \<inter> t)"
 proof-
   assume "closed s" "compact t"
@@ -2805,25 +2898,6 @@
     by auto
 qed
 
-lemma finite_imp_closed:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
-  shows "finite s ==> closed s"
-proof-
-  assume "finite s" hence "\<not>( \<exists>t. t \<subseteq> s \<and> infinite t)" using finite_subset by auto
-  thus ?thesis using bolzano_weierstrass_imp_closed[of s] by auto
-qed
-
-lemma finite_imp_compact:
-  fixes s :: "(real ^ _) set"
-  shows "finite s ==> compact s"
-  unfolding compact_eq_bounded_closed
-  using finite_imp_closed finite_imp_bounded
-  by blast
-
-lemma compact_sing [simp]: "compact {a}"
-  unfolding compact_def o_def
-  by (auto simp add: tendsto_const)
-
 lemma closed_sing [simp]:
   fixes a :: "'a::metric_space"
   shows "closed {a}"
@@ -2833,27 +2907,49 @@
   apply (simp add: dist_nz dist_commute)
   done
 
+lemma finite_imp_closed:
+  fixes s :: "'a::metric_space set"
+  shows "finite s ==> closed s"
+proof (induct set: finite)
+  case empty show "closed {}" by simp
+next
+  case (insert x F)
+  hence "closed ({x} \<union> F)" by (simp only: closed_Un closed_sing)
+  thus "closed (insert x F)" by simp
+qed
+
+lemma finite_imp_compact:
+  fixes s :: "'a::heine_borel set"
+  shows "finite s ==> compact s"
+  unfolding compact_eq_bounded_closed
+  using finite_imp_closed finite_imp_bounded
+  by blast
+
+lemma compact_sing [simp]: "compact {a}"
+  unfolding compact_def o_def
+  by (auto simp add: tendsto_const)
+
 lemma compact_cball[simp]:
-  fixes x :: "real ^ _"
+  fixes x :: "'a::heine_borel"
   shows "compact(cball x e)"
   using compact_eq_bounded_closed bounded_cball closed_cball
   by blast
 
 lemma compact_frontier_bounded[intro]:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   shows "bounded s ==> compact(frontier s)"
   unfolding frontier_def
   using compact_eq_bounded_closed
   by blast
 
 lemma compact_frontier[intro]:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   shows "compact s ==> compact (frontier s)"
   using compact_eq_bounded_closed compact_frontier_bounded
   by blast
 
 lemma frontier_subset_compact:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   shows "compact s ==> frontier s \<subseteq> s"
   using frontier_subset_closed compact_eq_bounded_closed
   by blast
@@ -2867,7 +2963,7 @@
 text{* Finite intersection property. I could make it an equivalence in fact. *}
 
 lemma compact_imp_fip:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::heine_borel set"
   assumes "compact s"  "\<forall>t \<in> f. closed t"
         "\<forall>f'. finite f' \<and> f' \<subseteq> f --> (s \<inter> (\<Inter> f') \<noteq> {})"
   shows "s \<inter> (\<Inter> f) \<noteq> {}"
@@ -2886,7 +2982,7 @@
 lemma bounded_closed_nest:
   assumes "\<forall>n. closed(s n)" "\<forall>n. (s n \<noteq> {})"
   "(\<forall>m n. m \<le> n --> s n \<subseteq> s m)"  "bounded(s 0)"
-  shows "\<exists> a::real^'a::finite. \<forall>n::nat. a \<in> s(n)"
+  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s(n)"
 proof-
   from assms(2) obtain x where x:"\<forall>n::nat. x n \<in> s n" using choice[of "\<lambda>n x. x\<in> s n"] by auto
   from assms(4,1) have *:"compact (s 0)" using bounded_closed_imp_compact[of "s 0"] by auto
@@ -2918,7 +3014,7 @@
           "\<forall>n. (s n \<noteq> {})"
           "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
           "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y \<in> (s n). dist x y < e"
-  shows "\<exists>a::real^'a::finite. \<forall>n::nat. a \<in> s n"
+  shows "\<exists>a::'a::heine_borel. \<forall>n::nat. a \<in> s n"
 proof-
   have "\<forall>n. \<exists> x. x\<in>s n" using assms(2) by auto
   hence "\<exists>t. \<forall>n. t n \<in> s n" using choice[of "\<lambda> n x. x \<in> s n"] by auto
@@ -2951,7 +3047,7 @@
           "\<forall>n. s n \<noteq> {}"
           "\<forall>m n. m \<le> n --> s n \<subseteq> s m"
           "\<forall>e>0. \<exists>n. \<forall>x \<in> (s n). \<forall> y\<in>(s n). dist x y < e"
-  shows "\<exists>a::real^'a::finite. \<Inter> {t. (\<exists>n::nat. t = s n)} = {a}"
+  shows "\<exists>a::'a::heine_borel. \<Inter> {t. (\<exists>n::nat. t = s n)} = {a}"
 proof-
   obtain a where a:"\<forall>n. a \<in> s n" using decreasing_closed_nest[of s] using assms by auto
   { fix b assume b:"b \<in> \<Inter>{t. \<exists>n. t = s n}"
@@ -2966,7 +3062,7 @@
 
 text{* Cauchy-type criteria for uniform convergence. *}
 
-lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> real^'a::finite" shows
+lemma uniformly_convergent_eq_cauchy: fixes s::"nat \<Rightarrow> 'b \<Rightarrow> 'a::heine_borel" shows
  "(\<exists>l. \<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e) \<longleftrightarrow>
   (\<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")
 proof(rule)
@@ -3000,7 +3096,7 @@
 qed
 
 lemma uniformly_cauchy_imp_uniformly_convergent:
-  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> real ^ 'n::finite"
+  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> 'b::heine_borel"
   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"
           "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
   shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
@@ -3390,13 +3486,13 @@
   unfolding dist_norm minus_diff_minus norm_minus_cancel ..
 
 lemma uniformly_continuous_on_neg:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
+  fixes f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   shows "uniformly_continuous_on s f
          ==> uniformly_continuous_on s (\<lambda>x. -(f x))"
   unfolding uniformly_continuous_on_def dist_minus .
 
 lemma uniformly_continuous_on_add:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
   assumes "uniformly_continuous_on s f" "uniformly_continuous_on s g"
   shows "uniformly_continuous_on s (\<lambda>x. f x + g x)"
 proof-
@@ -3409,7 +3505,7 @@
 qed
 
 lemma uniformly_continuous_on_sub:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> real ^ _" (* FIXME: generalize *)
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" (* FIXME: generalize 'a *)
   shows "uniformly_continuous_on s f \<Longrightarrow> uniformly_continuous_on s g
            ==> uniformly_continuous_on s  (\<lambda>x. f x - g x)"
   unfolding ab_diff_minus
@@ -3907,11 +4003,18 @@
   thus ?thesis unfolding Lim_at by auto
 qed
 
+lemma bounded_linear_continuous_at:
+  assumes "bounded_linear f"  shows "continuous (at a) f"
+  unfolding continuous_at using assms
+  apply (rule bounded_linear.tendsto)
+  apply (rule Lim_at_id [unfolded id_def])
+  done
+
 lemma linear_continuous_at:
   fixes f :: "real ^ _ \<Rightarrow> real ^ _"
   assumes "linear f"  shows "continuous (at a) f"
-  unfolding continuous_at Lim_at_zero[of f "f a" a] using linear_lim_0[OF assms]
-  unfolding Lim_null[of "\<lambda>x. f (a + x)"] unfolding linear_sub[OF assms, THEN sym] by auto
+  using assms unfolding linear_conv_bounded_linear
+  by (rule bounded_linear_continuous_at)
 
 lemma linear_continuous_within:
   fixes f :: "real ^ _ \<Rightarrow> real ^ _"
@@ -4202,14 +4305,15 @@
 subsection{* Preservation properties for pasted sets.                                  *}
 
 lemma bounded_pastecart:
+  fixes s :: "('a::real_normed_vector ^ _) set" (* FIXME: generalize to metric_space *)
   assumes "bounded s" "bounded t"
   shows "bounded { pastecart x y | x y . (x \<in> s \<and> y \<in> t)}"
 proof-
-  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
+  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
   { fix x y assume "x\<in>s" "y\<in>t"
     hence "norm x \<le> a" "norm y \<le> b" using ab by auto
     hence "norm (pastecart x y) \<le> a + b" using norm_pastecart[of x y] by auto }
-  thus ?thesis unfolding bounded_def by auto
+  thus ?thesis unfolding bounded_iff by auto
 qed
 
 lemma closed_pastecart:
@@ -4241,24 +4345,25 @@
 
 text{* Hence some useful properties follow quite easily.                         *}
 
+lemma compact_scaleR_image:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "compact s"  shows "compact ((\<lambda>x. scaleR c x) ` s)"
+proof-
+  let ?f = "\<lambda>x. scaleR c x"
+  have *:"bounded_linear ?f" by (rule scaleR.bounded_linear_right)
+  show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
+    using bounded_linear_continuous_at[OF *] assms by auto
+qed
+
 lemma compact_scaling:
   fixes s :: "(real ^ _) set"
   assumes "compact s"  shows "compact ((\<lambda>x. c *s x) ` s)"
-proof-
-  let ?f = "\<lambda>x. c *s x"
-  have *:"linear ?f" unfolding linear_def vector_smult_assoc vector_add_ldistrib real_mult_commute by auto
-  show ?thesis using compact_continuous_image[of s ?f] continuous_at_imp_continuous_on[of s ?f]
-    using linear_continuous_at[OF *] assms by auto
-qed
+  using assms unfolding smult_conv_scaleR by (rule compact_scaleR_image)
 
 lemma compact_negations:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  shows "compact ((\<lambda>x. -x) ` s)"
-proof-
-  have "(\<lambda>x. - x) ` s = (\<lambda>x. (- 1) *s x) ` s"
-    unfolding vector_sneg_minus1 ..
-  thus ?thesis using compact_scaling[OF assms, of "-1"] by auto
-qed
+  using compact_scaleR_image [OF assms, of "- 1"] by auto
 
 lemma compact_sums:
   fixes s t :: "(real ^ _) set"
@@ -4317,6 +4422,7 @@
 text{* We can state this in terms of diameter of a set.                          *}
 
 definition "diameter s = (if s = {} then 0::real else rsup {norm(x - y) | x y. x \<in> s \<and> y \<in> s})"
+  (* TODO: generalize to class metric_space *)
 
 lemma diameter_bounded:
   assumes "bounded s"
@@ -4324,7 +4430,7 @@
         "\<forall>d>0. d < diameter s --> (\<exists>x\<in>s. \<exists>y\<in>s. norm(x - y) > d)"
 proof-
   let ?D = "{norm (x - y) |x y. x \<in> s \<and> y \<in> s}"
-  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_def] by auto
+  obtain a where a:"\<forall>x\<in>s. norm x \<le> a" using assms[unfolded bounded_iff] by auto
   { fix x y assume "x \<in> s" "y \<in> s"
     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)  }
   note * = this
@@ -4365,9 +4471,9 @@
 
 text{* Related results with closure as the conclusion.                           *}
 
-lemma closed_scaling:
-  fixes s :: "(real ^ _) set"
-  assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
+lemma closed_scaleR_image:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "closed s" shows "closed ((\<lambda>x. scaleR c x) ` s)"
 proof(cases "s={}")
   case True thus ?thesis by auto
 next
@@ -4378,29 +4484,39 @@
     case True thus ?thesis apply auto unfolding * using closed_sing by auto
   next
     case False
-    { fix x l assume as:"\<forall>n::nat. x n \<in> op *s c ` s"  "(x ---> l) sequentially"
-      { 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) }
+    { fix x l assume as:"\<forall>n::nat. x n \<in> scaleR c ` s"  "(x ---> l) sequentially"
+      { fix n::nat have "scaleR (1 / c) (x n) \<in> s"
+          using as(1)[THEN spec[where x=n]]
+          using `c\<noteq>0` by (auto simp add: vector_smult_assoc)
+      }
       moreover
       { fix e::real assume "e>0"
 	hence "0 < e *\<bar>c\<bar>"  using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
-	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
-	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
+	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
+	hence "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
+          unfolding dist_norm unfolding scaleR_right_diff_distrib[THEN sym] norm_scaleR
 	  using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto  }
-      hence "((\<lambda>n. (1 / c) *s x n) ---> (1 / c) *s l) sequentially" unfolding Lim_sequentially by auto
-      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"]]
-	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  }
-    thus ?thesis unfolding closed_sequential_limits by auto
+      hence "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially" unfolding Lim_sequentially by auto
+      ultimately have "l \<in> scaleR c ` s"
+        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"]]
+	unfolding image_iff using `c\<noteq>0` apply(rule_tac x="scaleR (1 / c) l" in bexI) by auto  }
+    thus ?thesis unfolding closed_sequential_limits by fast
   qed
 qed
 
+lemma closed_scaling:
+  fixes s :: "(real ^ _) set"
+  assumes "closed s" shows "closed ((\<lambda>x. c *s x) ` s)"
+  using assms unfolding smult_conv_scaleR by (rule closed_scaleR_image)
+
 lemma closed_negations:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes s :: "'a::real_normed_vector set"
   assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
-  using closed_scaling[OF assms, of "- 1"]
-  unfolding vector_sneg_minus1 by auto
+  using closed_scaleR_image[OF assms, of "- 1"] by simp
 
 lemma compact_closed_sums:
-  fixes s :: "(real ^ _) set"
+  fixes s :: "'a::real_normed_vector set"
   assumes "compact s"  "closed t"  shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
 proof-
   let ?S = "{x + y |x y. x \<in> s \<and> y \<in> t}"
@@ -4416,11 +4532,11 @@
       using f(3) by auto
     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
   }
-  thus ?thesis unfolding closed_sequential_limits by auto
+  thus ?thesis unfolding closed_sequential_limits by fast
 qed
 
 lemma closed_compact_sums:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::real_normed_vector set"
   assumes "closed s"  "compact t"
   shows "closed {x + y | x y. x \<in> s \<and> y \<in> t}"
 proof-
@@ -4430,7 +4546,7 @@
 qed
 
 lemma compact_closed_differences:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::real_normed_vector set"
   assumes "compact s"  "closed t"
   shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
 proof-
@@ -4440,7 +4556,7 @@
 qed
 
 lemma closed_compact_differences:
-  fixes s t :: "(real ^ _) set"
+  fixes s t :: "'a::real_normed_vector set"
   assumes "closed s" "compact t"
   shows "closed {x - y | x y. x \<in> s \<and> y \<in> t}"
 proof-
@@ -4450,7 +4566,7 @@
 qed
 
 lemma closed_translation:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes a :: "'a::real_normed_vector"
   assumes "closed s"  shows "closed ((\<lambda>x. a + x) ` s)"
 proof-
   have "{a + y |y. y \<in> s} = (op + a ` s)" by auto
@@ -4458,21 +4574,26 @@
 qed
 
 lemma translation_UNIV:
- "range (\<lambda>x::real^'a. a + x) = UNIV"
+  fixes a :: "'a::ab_group_add" shows "range (\<lambda>x. a + x) = UNIV"
   apply (auto simp add: image_iff) apply(rule_tac x="x - a" in exI) by auto
 
-lemma translation_diff: "(\<lambda>x::real^'a. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)" by auto
+lemma translation_diff:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)"
+  by auto
 
 lemma closure_translation:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes a :: "'a::real_normed_vector"
   shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
 proof-
-  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"  apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
-  show ?thesis unfolding closure_interior translation_diff translation_UNIV using interior_translation[of a "UNIV - s"] unfolding * by auto
+  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"
+    apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
+  show ?thesis unfolding closure_interior translation_diff translation_UNIV
+    using interior_translation[of a "UNIV - s"] unfolding * by auto
 qed
 
 lemma frontier_translation:
-  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  fixes a :: "'a::real_normed_vector"
   shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
   unfolding frontier_def translation_diff interior_translation closure_translation by auto
 
@@ -4769,7 +4890,7 @@
       have "\<bar>x$i\<bar> \<le> \<bar>a$i\<bar> + \<bar>b$i\<bar>" using x[THEN spec[where x=i]] by auto  }
     hence "(\<Sum>i\<in>UNIV. \<bar>x $ i\<bar>) \<le> ?b" by(rule setsum_mono)
     hence "norm x \<le> ?b" using norm_le_l1[of x] by auto  }
-  thus ?thesis unfolding interval and bounded_def by auto
+  thus ?thesis unfolding interval and bounded_iff by auto
 qed
 
 lemma bounded_interval: fixes a :: "real^'n::finite" shows
@@ -5194,7 +5315,7 @@
   assumes "bounded {s n| n::nat. True}"  "\<forall>n. dest_vec1(s n) \<le> dest_vec1(s(Suc n))"
   shows "\<exists>l. (s ---> l) sequentially"
 proof-
-  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
+  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
   { fix m::nat
     have "\<And> n. n\<ge>m \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)"
       apply(induct_tac n) apply simp using assms(2) apply(erule_tac x="na" in allE) by(auto simp add: not_less_eq_eq)  }
@@ -5384,6 +5505,7 @@
 qed
 
 lemma complete_isometric_image:
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _"
   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"
   shows "complete(f ` s)"
 proof-
@@ -5577,7 +5699,7 @@
 qed
 
 lemma complete_subspace:
-  "subspace s ==> complete s"
+  fixes s :: "(real ^ _) set" shows "subspace s ==> complete s"
   using complete_eq_closed closed_subspace
   by auto