# HG changeset patch
# User huffman
# Date 1243646587 25200
# Node ID 80667d5bee32a39b61a360ed9b30293b7fb50d5f
# Parent  fc09ec06b89b956bf59657797fb57ed7ab7b75b1
generalize topological notions to class metric_space; add class perfect_space

diff -r fc09ec06b89b -r 80667d5bee32 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Fri May 29 15:32:33 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Fri May 29 18:23:07 2009 -0700
@@ -615,7 +615,7 @@
 
 subsection {* One rather trivial consequence. *}
 
-lemma connected_UNIV: "connected UNIV"
+lemma connected_UNIV: "connected (UNIV :: (real ^ _) set)"
   by(simp add: convex_connected convex_UNIV)
 
 subsection {* Convex functions into the reals. *}
@@ -763,10 +763,10 @@
   thus "dist x (u *s y + v *s z) \<le> e" using real_convex_bound_le[OF yz uv] by auto 
 qed
 
-lemma connected_ball: "connected(ball x e)"
+lemma connected_ball: "connected(ball (x::real^_) e)" (* FIXME: generalize *)
   using convex_connected convex_ball by auto
 
-lemma connected_cball: "connected(cball x e)"
+lemma connected_cball: "connected(cball (x::real^_) e)" (* FIXME: generalize *)
   using convex_connected convex_cball by auto
 
 subsection {* Convex hull. *}
@@ -2186,7 +2186,9 @@
   ultimately show "u *s x + v *s y \<in> s" apply- apply(rule assms[unfolded is_interval_def, rule_format, OF as(1,2)])
     using as(3-) dimindex_ge_1 apply- by(auto simp add: vector_component) qed
 
-lemma is_interval_connected: "is_interval s \<Longrightarrow> connected s"
+lemma is_interval_connected:
+  fixes s :: "(real ^ _) set"
+  shows "is_interval s \<Longrightarrow> connected s"
   using is_interval_convex convex_connected by auto
 
 lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
diff -r fc09ec06b89b -r 80667d5bee32 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 15:32:33 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri May 29 18:23:07 2009 -0700
@@ -195,7 +195,7 @@
 
 subsection{* The universal Euclidean versions are what we use most of the time *}
 definition
-  "open" :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
+  "open" :: "'a::metric_space set \<Rightarrow> bool" where
   "open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
 definition "closed S \<longleftrightarrow> open(UNIV - S)"
 definition "euclidean = topology open"
@@ -288,17 +288,26 @@
 subsection{* Open and closed balls. *}
 
 definition
-  ball :: "real ^ 'n::finite \<Rightarrow> real \<Rightarrow> (real^'n) set" where
+  ball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
   "ball x e = {y. dist x y < e}"
 
 definition
-  cball :: "real ^ 'n::finite \<Rightarrow> real \<Rightarrow> (real^'n) set" where
+  cball :: "'a::metric_space \<Rightarrow> real \<Rightarrow> 'a set" where
   "cball x e = {y. dist x y \<le> e}"
 
 lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
 lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
-lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_norm)
-lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_norm)
+
+lemma mem_ball_0 [simp]:
+  fixes x :: "'a::real_normed_vector"
+  shows "x \<in> ball 0 e \<longleftrightarrow> norm x < e"
+  by (simp add: dist_norm)
+
+lemma mem_cball_0 [simp]:
+  fixes x :: "'a::real_normed_vector"
+  shows "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e"
+  by (simp add: dist_norm)
+
 lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e"  by simp
 lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
 lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
@@ -494,8 +503,9 @@
 
 subsection{* Limit points *}
 
-definition islimpt:: "real ^'n::finite \<Rightarrow> (real^'n) set \<Rightarrow> bool" (infixr "islimpt" 60) where
-  islimpt_def: "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
+definition
+  islimpt:: "'a::metric_space \<Rightarrow> 'a set \<Rightarrow> bool" (infixr "islimpt" 60) where
+  "x islimpt S \<longleftrightarrow> (\<forall>T. x\<in>T \<longrightarrow> open T \<longrightarrow> (\<exists>y\<in>S. y\<in>T \<and> y\<noteq>x))"
 
   (* FIXME: Sure this form is OK????*)
 lemma islimptE: assumes "x islimpt S" and "x \<in> T" and "open T"
@@ -519,17 +529,44 @@
   using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   by metis (* FIXME: VERY slow! *)
 
-lemma islimpt_UNIV[simp, intro]: "(x:: real ^'n::finite) islimpt UNIV"
-proof-
+axclass perfect_space \<subseteq> metric_space
+  islimpt_UNIV [simp, intro]: "x islimpt UNIV"
+
+lemma perfect_choose_dist:
+  fixes x :: "'a::perfect_space"
+  shows "0 < r \<Longrightarrow> \<exists>a. a \<noteq> x \<and> dist a x < r"
+using islimpt_UNIV [of x]
+by (simp add: islimpt_approachable)
+
+instance real :: perfect_space
+apply default
+apply (rule islimpt_approachable [THEN iffD2])
+apply (clarify, rule_tac x="x + e/2" in bexI)
+apply (auto simp add: dist_norm)
+done
+  
+instance "^" :: (perfect_space, finite) perfect_space
+proof
+  fix x :: "'a ^ 'b"
   {
-    fix e::real assume ep: "e>0"
-    from vector_choose_size[of "e/2"] ep have "\<exists>(c:: real ^'n). norm c = e/2" by auto
-    then obtain c ::"real^'n" where c: "norm c = e/2" by blast
-    let ?x = "x + c"
-    have "?x \<noteq> x" using c ep by (auto simp add: norm_eq_0_imp)
-    moreover have "dist ?x x < e" using c ep apply simp by norm
-    ultimately have "\<exists>x'. x' \<noteq> x\<and> dist x' x < e" by blast}
-  then show ?thesis unfolding islimpt_approachable by blast
+    fix e :: real assume "0 < e"
+    def a \<equiv> "x $ arbitrary"
+    have "a islimpt UNIV" by (rule islimpt_UNIV)
+    with `0 < e` obtain b where "b \<noteq> a" and "dist b a < e"
+      unfolding islimpt_approachable by auto
+    def y \<equiv> "Cart_lambda ((Cart_nth x)(arbitrary := b))"
+    from `b \<noteq> a` have "y \<noteq> x"
+      unfolding a_def y_def by (simp add: Cart_eq)
+    from `dist b a < e` have "dist y x < e"
+      unfolding dist_vector_def a_def y_def
+      apply simp
+      apply (rule le_less_trans [OF setL2_le_setsum [OF zero_le_dist]])
+      apply (subst setsum_diff1' [where a=arbitrary], simp, simp, simp)
+      done
+    from `y \<noteq> x` and `dist y x < e`
+    have "\<exists>y\<in>UNIV. y \<noteq> x \<and> dist y x < e" by auto
+  }
+  then show "x islimpt UNIV" unfolding islimpt_approachable by blast
 qed
 
 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
@@ -562,7 +599,7 @@
 qed
 
 lemma finite_set_avoid:
-  fixes a :: "real ^ 'n::finite"
+  fixes a :: "'a::metric_space"
   assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
 proof(induct rule: finite_induct[OF fS])
   case 1 thus ?case apply auto by ferrack
@@ -594,7 +631,7 @@
   done
 
 lemma discrete_imp_closed:
-  assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. norm(y - x) < e \<longrightarrow> y = x"
+  assumes e: "0 < e" and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
   shows "closed S"
 proof-
   {fix x assume C: "\<forall>e>0. \<exists>x'\<in>S. x' \<noteq> x \<and> dist x' x < e"
@@ -603,8 +640,7 @@
     let ?m = "min (e/2) (dist x y) "
     from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
     from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
-    have th: "norm (z - y) < e" using z y
-      unfolding dist_norm [symmetric]
+    have th: "dist z y < e" using z y
       by (intro dist_triangle_lt [where z=x], simp)
     from d[rule_format, OF y(1) z(1) th] y z
     have False by (auto simp add: dist_commute)}
@@ -644,23 +680,28 @@
   apply (metis Int_lower1 Int_lower2 subset_interior)
   by (metis Int_mono interior_subset open_inter open_interior open_subset_interior)
 
-lemma interior_limit_point[intro]: assumes x: "x \<in> interior S" shows "x islimpt S"
+lemma interior_limit_point [intro]:
+  fixes x :: "'a::perfect_space"
+  assumes x: "x \<in> interior S" shows "x islimpt S"
 proof-
   from x obtain e where e: "e>0" "\<forall>x'. dist x x' < e \<longrightarrow> x' \<in> S"
     unfolding mem_interior subset_eq Ball_def mem_ball by blast
-  {fix d::real assume d: "d>0"
-    let ?m = "min d e / 2"
-    have mde2: "?m \<ge> 0" using e(1) d(1) by arith
-    from vector_choose_dist[OF mde2, of x]
-    obtain y where y: "dist x y = ?m" by blast
-    have th: "dist x y < e" "dist x y < d" unfolding y using e(1) d(1) by arith+
+  {
+    fix d::real assume d: "d>0"
+    let ?m = "min d e"
+    have mde2: "0 < ?m" using e(1) d(1) by simp
+    from perfect_choose_dist [OF mde2, of x]
+    obtain y where "y \<noteq> x" and "dist y x < ?m" by blast
+    then have "dist y x < e" "dist y x < d" by simp_all
+    from `dist y x < e` e(2) have "y \<in> S" by (simp add: dist_commute)
     have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d"
-      apply (rule bexI[where x=y])
-      using e th y by (auto simp add: dist_commute)}
+      using `y \<in> S` `y \<noteq> x` `dist y x < d` by fast
+  }
   then show ?thesis unfolding islimpt_approachable by blast
 qed
 
 lemma interior_closed_Un_empty_interior:
+  fixes S T :: "(real ^ 'n::finite) set" (* FIXME: generalize to perfect_space *)
   assumes cS: "closed S" and iT: "interior T = {}"
   shows "interior(S \<union> T) = interior S"
 proof-
@@ -690,7 +731,7 @@
 	  done
 	then have "\<exists>z. z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" by blast
 	then have "\<exists>x' \<in>S. x'\<noteq>y \<and> dist x' y < d" using e by auto}
-      then have "y\<in>S" by (metis islimpt_approachable cS closed_limpt) }
+      then have "y\<in>S" by (metis islimpt_approachable [where 'a="real^'n"] cS closed_limpt[where 'a="real^'n"]) }
     then have "x \<in> interior S" unfolding mem_interior using e(1) by blast}
   hence "interior (S\<union>T) \<subseteq> interior S" unfolding mem_interior Ball_def subset_eq by blast
   ultimately show ?thesis by blast
@@ -766,7 +807,7 @@
     with * have "closure S \<subseteq> t"
       unfolding closure_def
       using closed_limpt[of t]
-      by blast
+      by auto
   }
   ultimately show ?thesis
     using hull_unique[of S, of "closure S", of closed]
@@ -1286,7 +1327,7 @@
   ultimately show ?rhs apply (rule_tac x="(\<lambda>n::nat. f (inverse (real n + 1)))" in exI) by auto
 next
   assume ?rhs
-  then obtain f::"nat\<Rightarrow>real^'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto
+  then obtain f::"nat\<Rightarrow>'a"  where f:"(\<forall>n. f n \<in> S - {x})" "(\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f n) x < e)" unfolding Lim_sequentially by auto
   { fix e::real assume "e>0"
     then obtain N where "dist (f N) x < e" using f(2) by auto
     moreover have "f N\<in>S" "f N \<noteq> x" using f(1) by auto
@@ -1773,9 +1814,11 @@
 
 text{* More properties of closed balls. *}
 
-lemma closed_cball: "closed(cball x e)"
+lemma closed_cball:
+  fixes x :: "'a::real_normed_vector" (* FIXME: generalize to metric_space *)
+  shows "closed (cball x e)"
 proof-
-  { fix xa::"nat\<Rightarrow>real^'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
+  { fix xa::"nat\<Rightarrow>'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
     from as(2) have "((\<lambda>n. x - xa n) ---> x - l) sequentially" using Lim_sub[of "\<lambda>n. x" x sequentially xa l] Lim_const[of x sequentially] by auto
     moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_norm by auto
     ultimately have "dist x l \<le> e"
@@ -1800,10 +1843,16 @@
   by (metis open_contains_cball subset_eq order_less_imp_le centre_in_cball mem_def)
 
 lemma mem_interior_cball: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. cball x e \<subseteq> S)"
-  apply (simp add: interior_def)
-  by (metis open_contains_cball subset_trans ball_subset_cball centre_in_ball open_ball)
-
-lemma islimpt_ball: "y islimpt ball x e \<longleftrightarrow> 0 < e \<and> y \<in> cball x e" (is "?lhs = ?rhs")
+  apply (simp add: interior_def, safe)
+  apply (force simp add: open_contains_cball)
+  apply (rule_tac x="ball x e" in exI)
+  apply (simp add: open_ball centre_in_ball subset_trans [OF ball_subset_cball])
+  done
+
+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"
   { assume "e \<le> 0"
@@ -1826,38 +1875,41 @@
       next
 	case False
 
-	have "dist x (y - (d / (2 * dist y x)) *s (y - x))
-	      = norm (x - y + (d / (2 * norm (y - x))) *s (y - x))"
+	have "dist x (y - (d / (2 * dist y x)) *\<^sub>R (y - x))
+	      = norm (x - y + (d / (2 * norm (y - x))) *\<^sub>R (y - x))"
 	  unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] by auto
 	also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
-	  using vector_sadd_rdistrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
-	  unfolding vector_smult_lneg vector_smult_lid
-	  by (auto simp add: norm_minus_commute)
+	  using scaleR_left_distrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
+	  unfolding scaleR_minus_left scaleR_one
+	  by (auto simp add: norm_minus_commute norm_scaleR)
 	also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
 	  unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
 	  unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
 	also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
-	finally have "y - (d / (2 * dist y x)) *s (y - x) \<in> ball x e" using `d>0` by auto
+	finally have "y - (d / (2 * dist y x)) *\<^sub>R (y - x) \<in> ball x e" using `d>0` by auto
 
 	moreover
 
-	have "(d / (2*dist y x)) *s (y - x) \<noteq> 0"
-	  using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding vector_mul_eq_0 by (auto simp add: dist_commute)
+	have "(d / (2*dist y x)) *\<^sub>R (y - x) \<noteq> 0"
+	  using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding scaleR_eq_0_iff by (auto simp add: dist_commute)
 	moreover
-	have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_mul
+	have "dist (y - (d / (2 * dist y x)) *\<^sub>R (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_scaleR
 	  using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
 	  unfolding dist_norm by auto
-	ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by (rule_tac  x="y - (d / (2*dist y x)) *s (y - x)" in bexI) auto
+	ultimately show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by (rule_tac  x="y - (d / (2*dist y x)) *\<^sub>R (y - x)" in bexI) auto
       qed
     next
       case False hence "d > dist x y" by auto
       show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
       proof(cases "x=y")
 	case True
-	obtain z where **:"dist y z = (min e d) / 2" using vector_choose_dist[of "(min e d) / 2" y]
+	obtain z where **: "z \<noteq> y" "dist z y < min e d"
+          using perfect_choose_dist[of "min e d" y]
 	  using `d > 0` `e>0` by auto
 	show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
-	  apply(rule_tac x=z in bexI) unfolding `x=y` dist_commute dist_nz using **  `d > 0` `e>0` by auto
+          unfolding `x = y`
+          using `z \<noteq> y` **
+          by (rule_tac x=z in bexI, auto simp add: dist_commute)
       next
 	case False thus "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
 	  using `d>0` `d > dist x y` `?rhs` by(rule_tac x=x in bexI, auto)
@@ -1866,11 +1918,16 @@
   thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto
 qed
 
-lemma closure_ball: "0 < e ==> (closure(ball x e) = cball x e)"
+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
 
-lemma interior_cball: "interior(cball x e) = ball x e"
+lemma interior_cball:
+  fixes x :: "real ^ _" (* FIXME: generalize *)
+  shows "interior(cball x e) = ball x e"
 proof(cases "e\<ge>0")
   case False note cs = this
   from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover
@@ -1916,12 +1973,16 @@
   ultimately show ?thesis using interior_unique[of "ball x e" "cball x e"] using open_ball[of x e] by auto
 qed
 
-lemma frontier_ball: "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
+lemma frontier_ball:
+  fixes a :: "real ^ _" (* FIXME: generalize *)
+  shows "0 < e ==> frontier(ball a e) = {x. dist a x = e}"
   apply (simp add: frontier_def closure_ball interior_open open_ball order_less_imp_le)
   apply (simp add: expand_set_eq)
   by arith
 
-lemma frontier_cball: "frontier(cball a e) = {x. dist a x = e}"
+lemma frontier_cball:
+  fixes a :: "real ^ _" (* FIXME: generalize *)
+  shows "frontier(cball a e) = {x. dist a x = e}"
   apply (simp add: frontier_def interior_cball closed_cball closure_closed order_less_imp_le)
   apply (simp add: expand_set_eq)
   by arith
@@ -1931,7 +1992,9 @@
   by (metis zero_le_dist dist_self order_less_le_trans)
 lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
 
-lemma cball_eq_sing: "(cball x e = {x}) \<longleftrightarrow> e = 0"
+lemma cball_eq_sing:
+  fixes x :: "real ^ _" (* FIXME: generalize *)
+  shows "(cball x e = {x}) \<longleftrightarrow> e = 0"
 proof-
   { assume as:"\<forall>xa. (dist x xa \<le> e) = (xa = x)"
     hence "e \<ge> 0" apply (erule_tac x=x in allE) by auto
@@ -1941,7 +2004,9 @@
   thus ?thesis unfolding expand_set_eq mem_cball by (auto simp add: dist_nz)
 qed
 
-lemma cball_sing:  "e = 0 ==> cball x e = {x}" by (simp add: cball_eq_sing)
+lemma cball_sing:
+  fixes x :: "real ^ _" (* FIXME: generalize *)
+  shows "e = 0 ==> cball x e = {x}" by (simp add: cball_eq_sing)
 
 text{* For points in the interior, localization of limits makes no difference.   *}
 
@@ -2650,6 +2715,7 @@
 qed
 
 lemma bolzano_weierstrass_imp_closed:
+  fixes s :: "(real ^ 'n::finite) set"
   assumes "\<forall>t. infinite t \<and> t \<subseteq> s --> (\<exists>x \<in> s. x islimpt t)"
   shows "closed s"
 proof-
@@ -2746,7 +2812,8 @@
 qed
 
 lemma finite_imp_closed:
- "finite s ==> closed s"
+  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
@@ -2764,7 +2831,8 @@
   by blast
 
 lemma closed_sing[simp]:
- "closed {a}"
+  fixes a :: "real ^ _" (* FIXME: generalize *)
+  shows "closed {a}"
   using compact_eq_bounded_closed compact_sing[of a]
   by blast
 
@@ -2790,7 +2858,8 @@
   by blast
 
 lemma open_delete:
- "open s ==> open(s - {x})"
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  shows "open s ==> open(s - {x})"
   using open_diff[of s "{x}"] closed_sing
   by blast
 
@@ -3516,11 +3585,13 @@
 qed
 
 lemma continuous_open_preimage_univ:
- "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _" (* FIXME: generalize *)
+  shows "\<forall>x. continuous (at x) f \<Longrightarrow> open s \<Longrightarrow> open {x. f x \<in> s}"
   using continuous_open_preimage[of UNIV f s] open_UNIV continuous_at_imp_continuous_on by auto
 
 lemma continuous_closed_preimage_univ:
- "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
+  fixes f :: "real ^ _ \<Rightarrow> real ^ _" (* FIXME: generalize *)
+  shows "(\<forall>x. continuous (at x) f) \<Longrightarrow> closed s ==> closed {x. f x \<in> s}"
   using continuous_closed_preimage[of UNIV f s] closed_UNIV continuous_at_imp_continuous_on by auto
 
 text{* Equality of continuous functions on closure and related results.          *}
@@ -3614,6 +3685,7 @@
 text{* Some arithmetical combinations (more to prove).                           *}
 
 lemma open_scaling[intro]:
+  fixes s :: "(real ^ _) set"
   assumes "c \<noteq> 0"  "open s"
   shows "open((\<lambda>x. c *s x) ` s)"
 proof-
@@ -3631,9 +3703,11 @@
 qed
 
 lemma open_negations:
- "open s ==> open ((\<lambda> x. -x) ` s)" unfolding pth_3 by auto
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  shows "open s ==> open ((\<lambda> x. -x) ` s)" unfolding pth_3 by auto
 
 lemma open_translation:
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
   assumes "open s"  shows "open((\<lambda>x. a + x) ` s)"
 proof-
   { fix x have "continuous (at x) (\<lambda>x. x - a)" using continuous_sub[of "at x" "\<lambda>x. x" "\<lambda>x. a"] continuous_at_id[of x] continuous_const[of "at x" a] by auto  }
@@ -3642,6 +3716,7 @@
 qed
 
 lemma open_affinity:
+  fixes s :: "(real ^ _) set"
   assumes "open s"  "c \<noteq> 0"
   shows "open ((\<lambda>x. a + c *s x) ` s)"
 proof-
@@ -3650,7 +3725,9 @@
   thus ?thesis using assms open_translation[of "op *s c ` s" a] unfolding * by auto
 qed
 
-lemma interior_translation: "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
+lemma interior_translation:
+  fixes s :: "'a::real_normed_vector set"
+  shows "interior ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (interior s)"
 proof (rule set_ext, rule)
   fix x assume "x \<in> interior (op + a ` s)"
   then obtain e where "e>0" and e:"ball x e \<subseteq> op + a ` s" unfolding mem_interior by auto
@@ -3833,16 +3910,19 @@
 
 
 lemma open_vec1:
+  fixes s :: "real set" shows
  "open(vec1 ` s) \<longleftrightarrow>
         (\<forall>x \<in> s. \<exists>e>0. \<forall>x'. abs(x' - x) < e --> x' \<in> s)" (is "?lhs = ?rhs")
   unfolding open_def apply simp unfolding forall_vec1 dist_vec1 vec1_in_image_vec1 by simp
 
 lemma islimpt_approachable_vec1:
+  fixes s :: "real set" shows
  "(vec1 x) islimpt (vec1 ` s) \<longleftrightarrow>
          (\<forall>e>0.  \<exists>x'\<in> s. x' \<noteq> x \<and> abs(x' - x) < e)"
   by (auto simp add: islimpt_approachable dist_vec1 vec1_eq)
 
 lemma closed_vec1:
+  fixes s :: "real set" shows
  "closed (vec1 ` s) \<longleftrightarrow>
         (\<forall>x. (\<forall>e>0.  \<exists>x' \<in> s. x' \<noteq> x \<and> abs(x' - x) < e)
             --> x \<in> s)"
@@ -3952,6 +4032,7 @@
 text{* For *minimal* distance, we only need closure, not compactness.            *}
 
 lemma distance_attains_inf:
+  fixes a :: "real ^ _" (* FIXME: generalize *)
   assumes "closed s"  "s \<noteq> {}"
   shows "\<exists>x \<in> s. \<forall>y \<in> s. dist a x \<le> dist a y"
 proof-
@@ -4087,6 +4168,7 @@
 qed
 
 lemma closed_pastecart:
+  fixes s :: "(real ^ 'a::finite) set" (* FIXME: generalize *)
   assumes "closed s"  "closed t"
   shows "closed {pastecart x y | x y . x \<in> s \<and> y \<in> t}"
 proof-
@@ -4229,6 +4311,7 @@
 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)"
 proof(cases "s={}")
   case True thus ?thesis by auto
@@ -4256,6 +4339,7 @@
 qed
 
 lemma closed_negations:
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
   assumes "closed s"  shows "closed ((\<lambda>x. -x) ` s)"
   using closed_scaling[OF assms, of "-1"] unfolding  pth_3 by auto
 
@@ -4306,6 +4390,7 @@
 qed
 
 lemma closed_translation:
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
   assumes "closed s"  shows "closed ((\<lambda>x. a + x) ` s)"
 proof-
   have "{a + y |y. y \<in> s} = (op + a ` s)" by auto
@@ -4319,20 +4404,23 @@
 lemma translation_diff: "(\<lambda>x::real^'a. a + x) ` (s - t) = ((\<lambda>x. a + x) ` s) - ((\<lambda>x. a + x) ` t)" by auto
 
 lemma closure_translation:
- "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  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
 qed
 
 lemma frontier_translation:
- "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  shows "frontier((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (frontier s)"
   unfolding frontier_def translation_diff interior_translation closure_translation by auto
 
 subsection{* Separation between points and sets.                                       *}
 
 lemma separate_point_closed:
- "closed s \<Longrightarrow> a \<notin> s  ==> (\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x)"
+  fixes s :: "(real ^ _) set" (* FIXME: generalize *)
+  shows "closed s \<Longrightarrow> a \<notin> s  ==> (\<exists>d>0. \<forall>x\<in>s. d \<le> dist a x)"
 proof(cases "s = {}")
   case True
   thus ?thesis by(auto intro!: exI[where x=1])
@@ -4733,11 +4821,13 @@
   using bounded_subset_closed_interval_symmetric[of s] by auto
 
 lemma frontier_closed_interval:
- "frontier {a .. b} = {a .. b} - {a<..<b}"
+  fixes a b :: "real ^ _"
+  shows "frontier {a .. b} = {a .. b} - {a<..<b}"
   unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] ..
 
 lemma frontier_open_interval:
- "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
+  fixes a b :: "real ^ _"
+  shows "frontier {a<..<b} = (if {a<..<b} = {} then {} else {a .. b} - {a<..<b})"
 proof(cases "{a<..<b} = {}")
   case True thus ?thesis using frontier_empty by auto
 next
@@ -4899,10 +4989,10 @@
   thus ?thesis unfolding closed_closedin[THEN sym] and * by auto
 qed
 
-lemma closed_halfspace_ge: "closed {x. a \<bullet> x \<ge> b}"
+lemma closed_halfspace_ge: "closed {x::real^_. a \<bullet> x \<ge> b}"
   using closed_halfspace_le[of "-a" "-b"] unfolding dot_lneg by auto
 
-lemma closed_hyperplane: "closed {x. a \<bullet> x = b}"
+lemma closed_hyperplane: "closed {x::real^_. a \<bullet> x = b}"
 proof-
   have "{x. a \<bullet> x = b} = {x. a \<bullet> x \<ge> b} \<inter> {x. a \<bullet> x \<le> b}" by auto
   thus ?thesis using closed_halfspace_le[of a b] and closed_halfspace_ge[of b a] using closed_Int by auto
@@ -4918,13 +5008,13 @@
 
 text{* Openness of halfspaces.                                                   *}
 
-lemma open_halfspace_lt: "open {x. a \<bullet> x < b}"
+lemma open_halfspace_lt: "open {x::real^_. a \<bullet> x < b}"
 proof-
   have "UNIV - {x. b \<le> a \<bullet> x} = {x. a \<bullet> x < b}" by auto
   thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
 qed
 
-lemma open_halfspace_gt: "open {x. a \<bullet> x > b}"
+lemma open_halfspace_gt: "open {x::real^_. a \<bullet> x > b}"
 proof-
   have "UNIV - {x. b \<ge> a \<bullet> x} = {x. a \<bullet> x > b}" by auto
   thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
@@ -5288,6 +5378,7 @@
 qed
 
 lemma closed_injective_image_subspace:
+  fixes s :: "(real ^ _) set"
   assumes "subspace s" "linear f" "\<forall>x\<in>s. f x = 0 --> x = 0" "closed s"
   shows "closed(f ` s)"
 proof-
@@ -5412,7 +5503,8 @@
   by auto
 
 lemma dim_closure:
- "dim(closure s) = dim s" (is "?dc = ?d")
+  fixes s :: "(real ^ _) set"
+  shows "dim(closure s) = dim s" (is "?dc = ?d")
 proof-
   have "?dc \<le> ?d" using closure_minimal[OF span_inc, of s]
     using closed_subspace[OF subspace_span, of s]