# HG changeset patch
# User huffman
# Date 1243555202 25200
# Node ID 847f00f435d43dc2e4e7cff5cd4f732ce66d236e
# Parent  67dff9c5b2bdd2b671aff15c548dbefe2b0dc365
move dist operation to new metric_space class

diff -r 67dff9c5b2bd -r 847f00f435d4 src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 17:00:02 2009 -0700
@@ -118,7 +118,7 @@
 
 lemma dist_triangle_eq:"dist x z = dist x y + dist y z \<longleftrightarrow> norm (x - y) *s (y - z) = norm (y - z) *s (x - y)"
 proof- have *:"x - y + (y - z) = x - z" by auto
-  show ?thesis unfolding dist_def norm_triangle_eq[of "x - y" "y - z", unfolded *] 
+  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *] 
     by(auto simp add:norm_minus_commute) qed
 
 lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto 
@@ -601,7 +601,7 @@
 
     have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e2"
       apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
-      using * apply(simp add: dist_def)
+      using * apply(simp add: dist_norm)
       using as(1,2)[unfolded open_def] apply simp
       using as(1,2)[unfolded open_def] apply simp
       using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
@@ -675,14 +675,14 @@
     using assms(2)[unfolded convex_on_def, THEN bspec[where x=x], THEN bspec[where x=y], THEN spec[where x="1-u"]] by auto
   moreover
   have *:"x - ((1 - u) *s x + u *s y) = u *s (x - y)" by (simp add: vector_ssub_ldistrib vector_sub_rdistrib)
-  have "(1 - u) *s x + u *s y \<in> ball x e" unfolding mem_ball dist_def unfolding * and norm_mul and abs_of_pos[OF `0<u`] unfolding dist_def[THEN sym]
+  have "(1 - u) *s x + u *s y \<in> ball x e" unfolding mem_ball dist_norm unfolding * and norm_mul and abs_of_pos[OF `0<u`] unfolding dist_norm[THEN sym]
     using u unfolding pos_less_divide_eq[OF xy] by auto
   hence "f x \<le> f ((1 - u) *s x + u *s y)" using assms(4) by auto
   ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
 qed
 
 lemma convex_distance: "convex_on s (\<lambda>x. dist a x)"
-proof(auto simp add: convex_on_def dist_def)
+proof(auto simp add: convex_on_def dist_norm)
   fix x y assume "x\<in>s" "y\<in>s"
   fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
   have "a = u *s a + v *s a" unfolding vector_sadd_rdistrib[THEN sym] and `u+v=1` by simp
@@ -782,7 +782,7 @@
 proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def 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_def using B by auto qed
+    unfolding subset_eq mem_cball dist_norm using B by auto qed
 
 lemma finite_imp_bounded_convex_hull:
   "finite s \<Longrightarrow> bounded(convex hull s)"
@@ -1222,10 +1222,10 @@
     show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`]
       using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto
   next  fix y assume "y \<in> cball a (Min i)"
-    hence y:"norm (a - y) \<le> Min i" unfolding dist_def[THEN sym] by auto
+    hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto
     { fix x assume "x\<in>t"
       hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
-      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_def by auto
+      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
       moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
       ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto }
     moreover
@@ -1355,18 +1355,18 @@
 proof(cases "a \<bullet> d - b \<bullet> d > 0")
   case True hence "0 < d \<bullet> d + (a \<bullet> d * 2 - b \<bullet> d * 2)" 
     apply(rule_tac add_pos_pos) using assms by auto
-  thus ?thesis apply(rule_tac disjI2) unfolding dist_def and real_vector_norm_def and real_sqrt_less_iff
+  thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
     by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
 next
   case False hence "0 < d \<bullet> d + (b \<bullet> d * 2 - a \<bullet> d * 2)" 
     apply(rule_tac add_pos_nonneg) using assms by auto
-  thus ?thesis apply(rule_tac disjI1) unfolding dist_def and real_vector_norm_def and real_sqrt_less_iff
+  thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
     by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
 qed
 
 lemma norm_increases_online:
  "(d::real^'n::finite) \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
-  using dist_increases_online[of d a 0] unfolding dist_def by auto
+  using dist_increases_online[of d a 0] unfolding dist_norm by auto
 
 lemma simplex_furthest_lt:
   fixes s::"(real^'n::finite) set" assumes "finite s"
@@ -1402,7 +1402,7 @@
  	proof(erule_tac disjE)
 	  assume "dist a y < dist a (y + w *s (x - b))"
 	  hence "norm (y - a) < norm ((u + w) *s x + (v - w) *s b - a)"
-	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
+	    unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: ring_simps)
 	  moreover have "(u + w) *s x + (v - w) *s b \<in> convex hull insert x s"
 	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
 	    apply(rule_tac x="u + w" in exI) apply rule defer 
@@ -1411,7 +1411,7 @@
 	next
 	  assume "dist a y < dist a (y - w *s (x - b))"
 	  hence "norm (y - a) < norm ((u - w) *s x + (v + w) *s b - a)"
-	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
+	    unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: ring_simps)
 	  moreover have "(u - w) *s x + (v + w) *s b \<in> convex hull insert x s"
 	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
 	    apply(rule_tac x="u - w" in exI) apply rule defer 
@@ -1430,7 +1430,7 @@
   have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
   then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
     using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
-    unfolding dist_commute[of a] unfolding dist_def by auto
+    unfolding dist_commute[of a] unfolding dist_norm by auto
   thus ?thesis proof(cases "x\<in>s")
     case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
@@ -1469,7 +1469,8 @@
 
 subsection {* Closest point of a convex set is unique, with a continuous projection. *}
 
-definition 
+definition
+  closest_point :: "(real ^ 'n::finite) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
  "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
 
 lemma closest_point_exists:
@@ -1512,7 +1513,7 @@
 proof- obtain u where "u>0" and u:"\<forall>v>0. v \<le> u \<longrightarrow> norm (v *s (z - x) - (y - x)) < norm (y - x)"
     using closer_points_lemma[OF assms] by auto
   show ?thesis apply(rule_tac x="min u 1" in exI) using u[THEN spec[where x="min u 1"]] and `u>0`
-    unfolding dist_def by(auto simp add: norm_minus_commute field_simps) qed
+    unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed
 
 lemma any_closest_point_dot:
   assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
@@ -1555,7 +1556,7 @@
        "(y - closest_point s y) \<bullet> (closest_point s x - closest_point s y) \<le> 0"
     apply(rule_tac[!] any_closest_point_dot[OF assms(1-2)])
     using closest_point_exists[OF assms(2-3)] by auto
-  thus ?thesis unfolding dist_def and norm_le
+  thus ?thesis unfolding dist_norm and norm_le
     using dot_pos_le[of "(x - closest_point s x) - (y - closest_point s y)"]
     by (auto simp add: dot_sym dot_ladd dot_radd) qed
 
@@ -1686,9 +1687,9 @@
        using hull_subset[of c convex] unfolding subset_eq and dot_rmult
        apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
        by(auto simp add: dot_sym elim!: ballE) 
-    thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_def by auto
+    thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
   qed(insert closed_halfspace_ge, auto)
-  then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_def by auto
+  then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
   thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: dot_sym) qed
 
 lemma separating_hyperplane_sets:
@@ -1719,7 +1720,7 @@
     fix z assume "z \<in> ball ((1 - u) *s x + u *s y) (min d e)"
     hence "(1- u) *s (z - u *s (y - x)) + u *s (z + (1 - u) *s (y - x)) \<in> s"
       apply(rule_tac assms[unfolded convex_alt, rule_format])
-      using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_def by(auto simp add: ring_simps)
+      using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_norm by(auto simp add: ring_simps)
     thus "z \<in> s" using u by (auto simp add: ring_simps) qed(insert u ed(3-4), auto) qed
 
 lemma convex_hull_eq_empty: "convex hull s = {} \<longleftrightarrow> s = {}"
@@ -1934,7 +1935,7 @@
     fix e  assume "0 < e" and as:"(u + e / 2 / norm x) *s x \<in> s"
     hence "u + e / 2 / norm x > u" using`norm x > 0` by(auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
     thus False using u_max[OF _ as] by auto
-  qed(insert `y\<in>s`, auto simp add: dist_def obt(3))
+  qed(insert `y\<in>s`, auto simp add: dist_norm obt(3))
   thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption)
     apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
 
@@ -2004,7 +2005,7 @@
 
   { fix x assume as:"x \<in> cball (0::real^'n) 1"
     have "norm x *s surf (pi x) \<in> s" proof(cases "x=0 \<or> norm x = 1") 
-      case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_def)
+      case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_norm)
       thus ?thesis apply(rule_tac assms(3)[rule_format, THEN DiffD1])
 	apply(rule_tac fs[unfolded subset_eq, rule_format])
 	unfolding surf(5)[THEN sym] by auto
@@ -2027,7 +2028,7 @@
       moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *s surf (pi x))" 
 	unfolding pi(2)[OF *] surf(4)[rule_format, OF pix] ..
       moreover have "surf (pi x) \<in> frontier s" using surf(5) pix by auto
-      hence "dist 0 (inverse (norm (surf (pi x))) *s x) \<le> 1" unfolding dist_def
+      hence "dist 0 (inverse (norm (surf (pi x))) *s x) \<le> 1" unfolding dist_norm
 	using ** and * using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
 	using False `x\<in>s` by(auto simp add:field_simps)
       ultimately show ?thesis unfolding image_iff apply(rule_tac x="inverse (norm (surf(pi x))) *s x" in bexI)
@@ -2040,15 +2041,15 @@
     prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof-
     fix x::"real^'n" assume as:"x \<in> cball 0 1"
     thus "continuous (at x) (\<lambda>x. norm x *s surf (pi x))" proof(cases "x=0")
-      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm[THEN spec])
+      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
       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_def by (auto simp add: norm_basis[unfolded One_nat_def])
+	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)
 	apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
-	unfolding norm_0 vector_smult_lzero dist_def diff_0_right norm_mul abs_norm_cancel proof-
+	unfolding norm_0 vector_smult_lzero dist_norm diff_0_right norm_mul abs_norm_cancel proof-
 	fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0<e"
 	hence "surf (pi x) \<in> frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto
 	hence "norm (surf (pi x)) \<le> B" using B fs by auto
@@ -2086,7 +2087,7 @@
     unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
     fix y assume "dist (u *s x) y < 1 - u"
     hence "inverse (1 - u) *s (y - u *s x) \<in> s"
-      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_def
+      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
       unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_mul      
       apply (rule mult_left_le_imp_le[of "1 - u"])
       unfolding class_semiring.mul_a using `u<1` by auto
@@ -2102,7 +2103,7 @@
   let ?d = "inverse d" and ?n = "0::real^'n"
   have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *s (x - a)) ` s"
     apply(rule, rule_tac x="d *s x + a" in image_eqI) defer
-    apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_def
+    apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_norm
     by(auto simp add: mult_right_le_one_le)
   hence "(\<lambda>x. inverse d *s (x - a)) ` s homeomorphic cball ?n 1"
     using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *s -a + ?d *s x) ` s", OF convex_affinity compact_affinity]
@@ -2368,10 +2369,10 @@
     show "\<bar>f y - f x\<bar> < e" proof(cases "y=x")
       case False def t \<equiv> "k / norm (y - x)"
       have "2 < t" "0<t" unfolding t_def using as False and `k>0` by(auto simp add:field_simps)
-      have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def
+      have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
 	apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute) 
       { def w \<equiv> "x + t *s (y - x)"
-	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def 
+	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm 
 	  unfolding t_def using `k>0` by(auto simp add: norm_mul simp del: vector_ssub_ldistrib) 
 	have "(1 / t) *s x + - x + ((t - 1) / t) *s x = (1 / t - 1 + (t - 1) / t) *s x" by auto 
 	also have "\<dots> = 0"  using `t>0` by(auto simp add:field_simps simp del:vector_sadd_rdistrib)
@@ -2384,7 +2385,7 @@
 	  using `0<t` `2<t` and `x\<in>s` `w\<in>s` by(auto simp add:field_simps) }
       moreover 
       { def w \<equiv> "x - t *s (y - x)"
-	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def 
+	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm 
 	  unfolding t_def using `k>0` by(auto simp add: norm_mul simp del: vector_ssub_ldistrib) 
 	have "(1 / (1 + t)) *s x + (t / (1 + t)) *s x = (1 / (1 + t) + t / (1 + t)) *s x" by auto
 	also have "\<dots>=x" using `t>0` by (auto simp add:field_simps simp del:vector_sadd_rdistrib)
@@ -2409,7 +2410,7 @@
   apply(rule) proof(cases "0 \<le> e") case True
   fix y assume y:"y\<in>cball x e" def z \<equiv> "2 *s x - y"
   have *:"x - (2 *s x - y) = y - x" by vector
-  have z:"z\<in>cball x e" using y unfolding z_def mem_cball dist_def * by(auto simp add: norm_minus_commute)
+  have z:"z\<in>cball x e" using y unfolding z_def mem_cball dist_norm * by(auto simp add: norm_minus_commute)
   have "(1 / 2) *s y + (1 / 2) *s z = x" unfolding z_def by auto
   thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
     using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by(auto simp add:field_simps)
@@ -2438,7 +2439,7 @@
     fix z assume z:"z\<in>{x - ?d..x + ?d}"
     have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
       by (metis card_enum field_simps d_def not_one_le_zero of_nat_le_iff real_eq_of_nat real_of_nat_1)
-    show "dist x z \<le> e" unfolding dist_def e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
+    show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
       using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed
   hence k:"\<forall>y\<in>{x - ?d..x + ?d}. f y \<le> k" unfolding c(2) apply(rule_tac convex_on_convex_hull_bound) apply assumption
     unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
@@ -2448,8 +2449,8 @@
   hence "\<forall>y\<in>cball x d. abs (f y) \<le> k + 2 * abs (f x)" apply(rule_tac convex_bounds_lemma) apply assumption proof
     fix y assume y:"y\<in>cball x d"
     { fix i::'n have "x $ i - d \<le> y $ i"  "y $ i \<le> x $ i + d" 
-	using order_trans[OF component_le_norm y[unfolded mem_cball dist_def], of i] by(auto simp add: vector_component)  }
-    thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_def 
+	using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component)  }
+    thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm 
       by(auto simp add: vector_component_simps) qed
   hence "continuous_on (ball x d) (vec1 \<circ> f)" apply(rule_tac convex_on_bounded_continuous)
     apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
@@ -2484,10 +2485,10 @@
 proof-
   have *: "\<And>x y::real^'n::finite. 2 *s x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
   have **:"\<And>x y::real^'n::finite. 2 *s x =   y \<Longrightarrow> norm x = (norm y) / 2" by auto
-  show ?t1 unfolding midpoint_def dist_def apply (rule **) by(auto,vector)
-  show ?t2 unfolding midpoint_def dist_def apply (rule *)  by(auto,vector)
-  show ?t3 unfolding midpoint_def dist_def apply (rule *)  by(auto,vector)
-  show ?t4 unfolding midpoint_def dist_def apply (rule **) by(auto,vector) qed
+  show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
+  show ?t2 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
+  show ?t3 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
+  show ?t4 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) qed
 
 lemma midpoint_eq_endpoint:
   "midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
@@ -2550,14 +2551,14 @@
 	unfolding norm_minus_commute[of x a] * norm_mul Cart_eq using as(2,3)
 	by(auto simp add: vector_component_simps field_simps)
     next assume as:"dist a b = dist a x + dist x b"
-      have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_def] norm_ge_zero by auto 
+      have "norm (a - x) / norm (a - b) \<le> 1" unfolding divide_le_eq_1_pos[OF Fal2] unfolding as[unfolded dist_norm] norm_ge_zero by auto 
       thus "\<exists>u. x = (1 - u) *s a + u *s b \<and> 0 \<le> u \<and> u \<le> 1" apply(rule_tac x="dist a x / dist a b" in exI)
-	unfolding dist_def Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
+	unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
 	  fix i::'n have "((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i =
 	    ((norm (a - b) - norm (a - x)) * (a $ i) + norm (a - x) * (b $ i)) / norm (a - b)"
 	    using Fal by(auto simp add:vector_component_simps field_simps)
 	  also have "\<dots> = x$i" apply(rule divide_eq_imp[OF Fal])
-	    unfolding as[unfolded dist_def] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
+	    unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
 	    by(auto simp add:field_simps vector_component_simps)
 	  finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i" by auto
 	qed(insert Fal2, auto) qed qed
@@ -2566,7 +2567,7 @@
   "between (a,b) (midpoint a b)" (is ?t1) 
   "between (b,a) (midpoint a b)" (is ?t2)
 proof- have *:"\<And>x y z. x = (1/2::real) *s z \<Longrightarrow> y = (1/2) *s z \<Longrightarrow> norm z = norm x + norm y" by auto
-  show ?t1 ?t2 unfolding between midpoint_def dist_def apply(rule_tac[!] *)
+  show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
     by(auto simp add:field_simps Cart_eq vector_component_simps) qed
 
 lemma between_mem_convex_hull:
@@ -2584,10 +2585,10 @@
     fix y assume as:"dist (x - e *s (x - c)) y < e * d"
     have *:"y = (1 - (1 - e)) *s ((1 / e) *s y - ((1 - e) / e) *s x) + (1 - e) *s x" using `e>0` by auto
     have "dist c ((1 / e) *s y - ((1 - e) / e) *s x) = abs(1/e) * norm (e *s c - y + (1 - e) *s x)"
-      unfolding dist_def unfolding norm_mul[THEN sym] apply(rule norm_eqI) using `e>0`
+      unfolding dist_norm unfolding norm_mul[THEN sym] apply(rule norm_eqI) using `e>0`
       by(auto simp add:vector_component_simps Cart_eq field_simps) 
     also have "\<dots> = abs(1/e) * norm (x - e *s (x - c) - y)" by(auto intro!:norm_eqI)
-    also have "\<dots> < d" using as[unfolded dist_def] and `e>0`
+    also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
       by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
     finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format])
       apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto
@@ -2608,12 +2609,12 @@
 	using `e\<le>1` `e>0` `d>0` by(auto intro!:mult_pos_pos divide_pos_pos)
       then obtain y where "y\<in>s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
 	using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
-      thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_def using pos_less_divide_eq[OF *] by auto qed qed
+      thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] by auto qed qed
   then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
   def z \<equiv> "c + ((1 - e) / e) *s (x - y)"
   have *:"x - e *s (x - c) = y - e *s (y - z)" unfolding z_def using `e>0` by auto
   have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
-    unfolding interior_open[OF open_ball] mem_ball z_def dist_def using y and assms(4,5)
+    unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
     by(auto simp del:vector_ssub_ldistrib simp add:field_simps norm_minus_commute) 
   thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
     using assms(1,4-5) `y\<in>s` by auto qed
@@ -2656,10 +2657,10 @@
   fix x::"real^'n" and e assume "0<e" and as:"\<forall>xa. dist x xa < e \<longrightarrow> (\<forall>x. 0 \<le> xa $ x) \<and> setsum (op $ xa) UNIV \<le> 1"
   show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
     fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *s basis i"]] and `e>0`
-      unfolding dist_def by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
+      unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
   next guess a using UNIV_witness[where 'a='n] ..
     have **:"dist x (x + (e / 2) *s basis a) < e" using  `e>0` and norm_basis[of a]
-      unfolding dist_def by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
+      unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
     have "\<And>i. (x + (e / 2) *s basis a) $ i = x$i + (if i = a then e/2 else 0)" by(auto simp add:vector_component_simps)
     hence *:"setsum (op $ (x + (e / 2) *s basis a)) UNIV = setsum (\<lambda>i. x$i + (if a = i then e/2 else 0)) UNIV" by(rule_tac setsum_cong, auto) 
     have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *s basis a)) UNIV" unfolding * setsum_addf
@@ -2677,11 +2678,11 @@
     fix y assume y:"dist x y < min (Min (op $ x ` UNIV)) ?d"
     have "setsum (op $ y) UNIV \<le> setsum (\<lambda>i. x$i + ?d) UNIV" proof(rule setsum_mono)
       fix i::'n have "abs (y$i - x$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
-	using y[unfolded min_less_iff_conj dist_def, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
+	using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
       thus "y $ i \<le> x $ i + ?d" by auto qed
     also have "\<dots> \<le> 1" unfolding setsum_addf setsum_constant card_enum real_eq_of_nat using dimindex_ge_1 by(auto simp add: Suc_le_eq)
     finally show "(\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" apply- proof(rule,rule)
-      fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_def, THEN conjunct1]
+      fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
 	using Min_gr_iff[of "op $ x ` dimset x"] dimindex_ge_1 by auto
       thus "0 \<le> y$i" using component_le_norm[of "x - y" i] and as(1)[rule_format, of i] by(auto simp add: vector_component_simps)
     qed auto qed auto qed
@@ -3225,7 +3226,7 @@
     unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_mul by(auto intro!: ***) 
   have "continuous_on (UNIV - {0}) (vec1 \<circ> (\<lambda>x::real^'n. 1 / norm x))" unfolding o_def continuous_on_eq_continuous_within
     apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
-    apply(rule continuous_at_vec1_norm[unfolded o_def,THEN spec]) by auto
+    apply(rule continuous_at_vec1_norm[unfolded o_def]) by auto
   thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
     by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
 
@@ -3234,4 +3235,4 @@
  
 (** In continuous_at_vec1_norm : Use \<And> instead of \<forall>. **)
 
-end
\ No newline at end of file
+end
diff -r 67dff9c5b2bd -r 847f00f435d4 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy	Thu May 28 17:00:02 2009 -0700
@@ -509,6 +509,9 @@
 definition vector_sgn_def:
   "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
 
+definition dist_vector_def:
+  "dist (x::'a^'b) y = norm (x - y)"
+
 instance proof
   fix a :: real and x y :: "'a ^ 'b"
   show "0 \<le> norm x"
@@ -527,6 +530,8 @@
     by (simp add: norm_scaleR setL2_right_distrib)
   show "sgn x = scaleR (inverse (norm x)) x"
     by (rule vector_sgn_def)
+  show "dist x y = norm (x - y)"
+    by (rule dist_vector_def)
 qed
 
 end
@@ -621,7 +626,7 @@
   by (simp add: norm_vector_1)
 
 lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
-  by (auto simp add: norm_real dist_def)
+  by (auto simp add: norm_real dist_norm)
 
 subsection {* A connectedness or intermediate value lemma with several applications. *}
 
@@ -953,37 +958,52 @@
 
 text{* Hence more metric properties. *}
 
-lemma dist_triangle_alt: "dist y z <= dist x y + dist x z"
+lemma dist_triangle_alt:
+  fixes x y z :: "'a::metric_space"
+  shows "dist y z <= dist x y + dist x z"
 using dist_triangle [of y z x] by (simp add: dist_commute)
 
-lemma dist_triangle2: "dist x y \<le> dist x z + dist y z"
-using dist_triangle [of x y z] by (simp add: dist_commute)
-
-lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by (simp add: zero_less_dist_iff)
-lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by (simp add: zero_less_dist_iff)
-
-lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
+lemma dist_pos_lt:
+  fixes x y :: "'a::metric_space"
+  shows "x \<noteq> y ==> 0 < dist x y"
+by (simp add: zero_less_dist_iff)
+
+lemma dist_nz:
+  fixes x y :: "'a::metric_space"
+  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
+by (simp add: zero_less_dist_iff)
+
+lemma dist_triangle_le:
+  fixes x y z :: "'a::metric_space"
+  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
 by (rule order_trans [OF dist_triangle2])
 
-lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e"
+lemma dist_triangle_lt:
+  fixes x y z :: "'a::metric_space"
+  shows "dist x z + dist y z < e ==> dist x y < e"
 by (rule le_less_trans [OF dist_triangle2])
 
 lemma dist_triangle_half_l:
-  "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
+  fixes x1 x2 y :: "'a::metric_space"
+  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
 by (rule dist_triangle_lt [where z=y], simp)
 
 lemma dist_triangle_half_r:
-  "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
+  fixes x1 x2 y :: "'a::metric_space"
+  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
 by (rule dist_triangle_half_l, simp_all add: dist_commute)
 
-lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'"
-unfolding dist_def by (rule norm_diff_triangle_ineq)
+lemma dist_triangle_add:
+  fixes x y x' y' :: "'a::real_normed_vector"
+  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
+unfolding dist_norm by (rule norm_diff_triangle_ineq)
 
 lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
-  unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul ..
+  unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
 
 lemma dist_triangle_add_half:
-  " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
+  fixes x x' y y' :: "'a::real_normed_vector"
+  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
 by (rule le_less_trans [OF dist_triangle_add], simp)
 
 lemma setsum_component [simp]:
@@ -1222,7 +1242,7 @@
 proof-
   from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"
     by blast
-  then have "dist x (x - c) = e" by (simp add: dist_def)
+  then have "dist x (x - c) = e" by (simp add: dist_norm)
   then show ?thesis by blast
 qed
 
@@ -2546,7 +2566,7 @@
 qed
 
 lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
-  by (metis dist_def fstcart_sub[symmetric] norm_fstcart)
+  by (metis dist_vector_def fstcart_sub[symmetric] norm_fstcart)
 
 lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
 proof-
@@ -2561,7 +2581,7 @@
 qed
 
 lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
-  by (metis dist_def sndcart_sub[symmetric] norm_sndcart)
+  by (metis dist_vector_def sndcart_sub[symmetric] norm_sndcart)
 
 lemma dot_pastecart: "(pastecart (x1::'a::{times,comm_monoid_add}^'n::finite) (x2::'a::{times,comm_monoid_add}^'m::finite)) \<bullet> (pastecart y1 y2) =  x1 \<bullet> y1 + x2 \<bullet> y2"
   by (simp add: dot_def setsum_UNIV_sum pastecart_def)
@@ -3901,7 +3921,7 @@
 qed
 
 lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
-  by (metis set_eq_subset span_mono span_span span_inc)
+  by (metis set_eq_subset span_mono span_span span_inc) (* FIXME: slow *)
 
 (* ------------------------------------------------------------------------- *)
 (* Low-dimensional subset is in a hyperplane (weak orthogonal complement).   *)
diff -r 67dff9c5b2bd -r 847f00f435d4 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Inner_Product.thy	Thu May 28 17:00:02 2009 -0700
@@ -10,7 +10,7 @@
 
 subsection {* Real inner product spaces *}
 
-class real_inner = real_vector + sgn_div_norm +
+class real_inner = real_vector + sgn_div_norm + dist_norm +
   fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
   assumes inner_commute: "inner x y = inner y x"
   and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
diff -r 67dff9c5b2bd -r 847f00f435d4 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 17:00:02 2009 -0700
@@ -297,8 +297,8 @@
 
 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_def)
-lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_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 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)
@@ -555,13 +555,15 @@
 	apply (simp only: vector_component)
 	by (rule th') auto
       have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)$i\<bar>" using  component_le_norm[of "x'-x" i]
-	apply (simp add: dist_def) by norm
+	apply (simp add: dist_norm) by norm
       from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
   then show ?thesis unfolding closed_limpt islimpt_approachable
     unfolding not_le[symmetric] by blast
 qed
 
-lemma finite_set_avoid: assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
+lemma finite_set_avoid:
+  fixes a :: "real ^ 'n::finite"
+  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
 next
@@ -602,7 +604,7 @@
     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_def [symmetric]
+      unfolding dist_norm [symmetric]
       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)}
@@ -1305,8 +1307,8 @@
     then obtain y where y: "\<exists>x. netord net x y" "\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e/b" by auto
     { fix x
       have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
-	using y(2) b unfolding dist_def	using linear_sub[of h "f x" l] `linear h`
-	apply auto by (metis b(1) b(2) dist_def dist_commute less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
+	using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h`
+	apply auto by (metis b(1) b(2) dist_vector_def dist_commute less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7)) (* FIXME: VERY slow! *)
     }
     hence " (\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (h (f x)) (h l) < e))" using y
       by(rule_tac x="y" in exI) auto
@@ -1325,7 +1327,7 @@
   done
 
 lemma Lim_neg: "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
-  apply (simp add: Lim dist_def  group_simps)
+  apply (simp add: Lim dist_norm  group_simps)
   apply (subst minus_diff_eq[symmetric])
   unfolding norm_minus_cancel by simp
 
@@ -1362,9 +1364,9 @@
   unfolding diff_minus
   by (simp add: Lim_add Lim_neg)
 
-lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_def)
+lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
 lemma Lim_null_norm: "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
-  by (simp add: Lim dist_def norm_vec1)
+  by (simp add: Lim dist_norm norm_vec1)
 
 lemma Lim_null_comparison:
   assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
@@ -1374,7 +1376,7 @@
   { fix x
     assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
     hence "dist (f x) 0 < e"  unfolding vec_def using dist_vec1[of "g x" "0"]
-      by (vector dist_def norm_vec1 real_vector_norm_def dot_def vec1_def)
+      by (vector dist_norm norm_vec1 real_vector_norm_def dot_def vec1_def)
   }
   thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
     using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
@@ -1384,7 +1386,7 @@
 
 lemma Lim_component: "(f ---> l) net
                       ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
-  apply (simp add: Lim dist_def vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
+  apply (simp add: Lim dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
   apply (auto simp del: vector_minus_component)
   apply (erule_tac x=e in allE)
   apply clarify
@@ -1475,7 +1477,7 @@
   { assume "norm (l - l') > 0"
     hence "norm (l - l') = 0" using *[of "(norm (l - l')) /2"] using norm_ge_zero[of "l - l'"] by simp
   }
-  hence "l = l'" using norm_ge_zero[of "l - l'"] unfolding le_less and dist_nz[of l l', unfolded dist_def, THEN sym] by auto
+  hence "l = l'" using norm_ge_zero[of "l - l'"] unfolding le_less and dist_nz[of l l', unfolded dist_norm, THEN sym] by auto
   thus ?thesis using assms using Lim_sub[of f l net f l'] by simp
 qed
 
@@ -1534,12 +1536,12 @@
 
     { 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_def  by auto
+	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_def and * using norm_triangle_lt by auto
+      finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
     }
     moreover
     obtain c where "(\<exists>x. netord net x c) \<and> (\<forall>x. netord net x c \<longrightarrow> dist (f x) l < d \<and> dist (g x) m < d)"
@@ -1561,7 +1563,7 @@
     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::"real^'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_def dist_commute)
+      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
   }
@@ -1573,7 +1575,7 @@
       unfolding Lim_at by auto
     { fix x::"real^'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)
-	by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
+	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
   }
@@ -1730,7 +1732,7 @@
       using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
       by (metis dlo_simps(4) le_imp_inverse_le linorder_not_less real_of_nat_gt_zero_cancel_iff real_of_nat_less_iff xt1(7))
   }
-  thus ?thesis unfolding Lim_sequentially dist_def apply simp unfolding norm_vec1 by auto
+  thus ?thesis unfolding Lim_sequentially dist_norm apply simp unfolding norm_vec1 by auto
 qed
 
 text{* More properties of closed balls. *}
@@ -1739,9 +1741,9 @@
 proof-
   { fix xa::"nat\<Rightarrow>real^'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_def 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"
-      unfolding dist_def
+      unfolding dist_norm
       using Lim_norm_ubound[of sequentially _ "x - l" e] using trivial_limit_sequentially by auto
   }
   thus ?thesis unfolding closed_sequential_limits by auto
@@ -1790,15 +1792,15 @@
 
 	have "dist x (y - (d / (2 * dist y x)) *s (y - x))
 	      = norm (x - y + (d / (2 * norm (y - x))) *s (y - x))"
-	  unfolding mem_cball mem_ball dist_def diff_diff_eq2 diff_add_eq[THEN sym] by auto
+	  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: dist_commute[unfolded dist_def] norm_mul)
+	  by (auto simp add: norm_minus_commute)
 	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_def] 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_def)
+	  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
 
 	moreover
@@ -1806,9 +1808,9 @@
 	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)
 	moreover
-	have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_def apply simp unfolding norm_minus_cancel norm_mul
+	have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_mul
 	  using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
-	  unfolding dist_def by auto
+	  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
       qed
     next
@@ -1858,7 +1860,7 @@
       thus "y \<in> ball x e" using `x = y ` by simp
     next
       case False
-      have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_def
+      have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_norm
 	using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by auto
       hence *:"y + (d / 2 / dist y x) *s (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
       have "y - x \<noteq> 0" using `x \<noteq> y` by auto
@@ -1866,11 +1868,11 @@
 	using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
 
       have "dist (y + (d / 2 / dist y x) *s (y - x)) x = norm (y + (d / (2 * norm (y - x))) *s y - (d / (2 * norm (y - x))) *s x - x)"
-	by (auto simp add: dist_def vector_ssub_ldistrib add_diff_eq)
+	by (auto simp add: dist_norm vector_ssub_ldistrib add_diff_eq)
       also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *s (y - x))"
 	by (auto simp add: vector_sadd_rdistrib vector_smult_lid ring_simps vector_sadd_rdistrib vector_ssub_ldistrib)
       also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)" using ** by auto
-      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_def)
+      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
       finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
       thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
     qed  }
@@ -2257,7 +2259,7 @@
 	  < (\<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_def using norm_le_l1[of "(f \<circ> r) n - l"] 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"
@@ -2316,8 +2318,8 @@
   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_def
-      using norm_triangle_sub[of "s N" "s n"] by (auto, metis dist_def dist_commute le_add_right_mono norm_triangle_sub real_less_def)
+    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 dist_vector_def dist_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
@@ -2553,11 +2555,11 @@
     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_def using norm_triangle_sub[of "x n" "x m"] 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
     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_def using norm_triangle_sub[of "x m" "x n"] 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
     qed  } note ** = this
   { fix a b assume "x a = x b" "a \<noteq> b"
     hence False using **[of a b] by auto  }
@@ -3128,13 +3130,13 @@
     { fix e::real assume "e>0"
       then obtain d where "d>0" and d:"\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
 	using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
-      obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_def] and `d>0` by auto
+      obtain N where N:"\<forall>n\<ge>N. norm (x n - y n - 0) < d" using xy[unfolded Lim_sequentially dist_norm] and `d>0` by auto
       { fix n assume "n\<ge>N"
 	hence "norm (f (x n) - f (y n) - 0) < e"
 	  using N[THEN spec[where x=n]] using d[THEN bspec[where x="x n"], THEN bspec[where x="y n"]] using x and y
-	  unfolding dist_commute and dist_def by simp  }
+	  unfolding dist_commute and dist_norm by simp  }
       hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e"  by auto  }
-    hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_def by auto  }
+    hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto  }
   thus ?rhs by auto
 next
   assume ?rhs
@@ -3147,7 +3149,7 @@
     def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
     have xyn:"\<forall>n. x n \<in> s \<and> y n \<in> s" and xy0:"\<forall>n. dist (x n) (y n) < inverse (real n + 1)" and fxy:"\<forall>n. \<not> dist (f (x n)) (f (y n)) < e"
       unfolding x_def and y_def using fa by auto
-    have *:"\<And>x y. dist (x - y) 0 = dist x y" unfolding dist_def by auto
+    have *:"\<And>x (y::real^_). dist (x - y) 0 = dist x y" unfolding dist_norm by auto
     { fix e::real assume "e>0"
       then obtain N::nat where "N \<noteq> 0" and N:"0 < inverse (real N) \<and> inverse (real N) < e" unfolding real_arch_inv[of e]   by auto
       { fix n::nat assume "n\<ge>N"
@@ -3517,7 +3519,7 @@
   have *:"f ` s \<subseteq> cball 0 b" using assms(2)[unfolded mem_cball_0[THEN sym]] by auto
   show ?thesis
     using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
-    unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_def)
+    unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_norm)
 qed
 
 text{* Making a continuous function avoid some value in a neighbourhood.         *}
@@ -3580,10 +3582,10 @@
     have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
     moreover
     { fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
-      hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
+      hence "norm ((1 / c) *s y - x) < e" unfolding dist_norm
 	using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
 	  assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
-      hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"]  e[THEN spec[where x="(1 / c) *s y"]]  assms(1) unfolding dist_def vector_smult_assoc by auto  }
+      hence "y \<in> op *s c ` s" using rev_image_eqI[of "(1 / c) *s y" s y "op *s c"]  e[THEN spec[where x="(1 / c) *s y"]]  assms(1) unfolding dist_norm vector_smult_assoc by auto  }
     ultimately have "\<exists>e>0. \<forall>x'. dist x' (c *s x) < e \<longrightarrow> x' \<in> op *s c ` s" apply(rule_tac x="e * abs c" in exI) by auto  }
   thus ?thesis unfolding open_def by auto
 qed
@@ -3612,14 +3614,14 @@
 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
-  hence "ball (x - a) e \<subseteq> s" unfolding subset_eq Ball_def mem_ball dist_def apply auto apply(erule_tac x="a + xa" in allE) unfolding ab_group_add_class.diff_diff_eq[THEN sym] by auto
+  hence "ball (x - a) e \<subseteq> s" unfolding subset_eq Ball_def mem_ball dist_norm apply auto apply(erule_tac x="a + xa" in allE) unfolding ab_group_add_class.diff_diff_eq[THEN sym] by auto
   thus "x \<in> op + a ` interior s" unfolding image_iff apply(rule_tac x="x - a" in bexI) unfolding mem_interior using `e > 0` by auto
 next
   fix x assume "x \<in> op + a ` interior s"
   then obtain y e where "e>0" and e:"ball y e \<subseteq> s" and y:"x = a + y" unfolding image_iff Bex_def mem_interior by auto
   { fix z have *:"a + y - z = y + a - z" by auto
     assume "z\<in>ball x e"
-    hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_def y ab_group_add_class.diff_diff_eq2 * by auto
+    hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y ab_group_add_class.diff_diff_eq2 * by auto
     hence "z \<in> op + a ` s" unfolding image_iff by(auto intro!: bexI[where x="z - a"])  }
   hence "ball x e \<subseteq> op + a ` s" unfolding subset_eq by auto
   thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
@@ -3732,8 +3734,8 @@
     { fix y assume "y\<in>s" "dist y x < d"
       hence "dist (f n y) (f n x) < e / 3" using d[THEN bspec[where x=y]] by auto
       hence "norm (f n y - g x) < 2 * e / 3" using norm_triangle_lt[of "f n y - f n x" "f n x - g x" "2*e/3"]
-	using n(1)[THEN bspec[where x=x], OF `x\<in>s`] unfolding dist_def unfolding ab_group_add_class.ab_diff_minus by auto
-      hence "dist (g y) (g x) < e" unfolding dist_def using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
+	using n(1)[THEN bspec[where x=x], OF `x\<in>s`] unfolding dist_norm unfolding ab_group_add_class.ab_diff_minus by auto
+      hence "dist (g y) (g x) < e" unfolding dist_norm using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
 	unfolding norm_minus_cancel[of "f n y - g y", THEN sym] using norm_triangle_lt[of "f n y - g x" "g y - f n y" e] by (auto simp add: uminus_add_conv_diff)  }
     hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e" using `d>0` by auto  }
   thus ?thesis unfolding continuous_on_def by auto
@@ -3750,7 +3752,7 @@
       hence "B * norm x < e" using `B>0` using mult_strict_right_mono[of "norm x" " e / B" B] unfolding real_mult_commute by auto
       hence "norm (f x) < e" using B[THEN spec[where x=x]] `B>0` using order_le_less_trans[of "norm (f x)" "B * norm x" e] by auto   }
     moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto
-    ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_def by auto  }
+    ultimately have "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f x) 0 < e" unfolding dist_norm by auto  }
   thus ?thesis unfolding Lim_at by auto
 qed
 
@@ -3808,13 +3810,13 @@
 lemma continuous_at_vec1_range:
  "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
         \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
-  unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_def apply auto
+  unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
   apply(erule_tac x=e in allE) apply auto apply (rule_tac x=d in exI) apply auto apply (erule_tac x=x' in allE) apply auto
   apply(erule_tac x=e in allE) by auto
 
 lemma continuous_on_vec1_range:
  " continuous_on s (vec1 o f) \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
-  unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_def ..
+  unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm ..
 
 lemma continuous_at_vec1_norm:
  "continuous (at x) (vec1 o norm)"
@@ -3828,7 +3830,7 @@
   shows "continuous (at (a::real^'a::finite)) (\<lambda> x. vec1(x$i))"
 proof-
   { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
-    hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_def by auto  }
+    hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto  }
   thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
 qed
 
@@ -3837,12 +3839,12 @@
 proof-
   { fix e::real and x xa assume "x\<in>s" "e>0" "xa\<in>s" "0 < norm (xa - x) \<and> norm (xa - x) < e"
     hence "\<bar>xa $ i - x $ i\<bar> < e" using component_le_norm[of "xa - x" i] by auto  }
-  thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_def by auto
+  thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_norm by auto
 qed
 
 lemma continuous_at_vec1_infnorm:
  "continuous (at x) (vec1 o infnorm)"
-  unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_def
+  unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_norm
   apply auto apply (rule_tac x=e in exI) apply auto
   using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
 
@@ -3898,7 +3900,7 @@
     { fix x' assume "x'\<in>s" and as:"norm (x' - x) < e"
       hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
 	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
-    hence "\<exists>d>0. \<forall>x'\<in>s. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_def by auto }
+    hence "\<exists>d>0. \<forall>x'\<in>s. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_norm by auto }
   thus ?thesis using assms
     using continuous_attains_sup[of s "\<lambda>x. dist a x"]
     unfolding continuous_on_vec1_range by (auto simp add: dist_commute)
@@ -3920,7 +3922,7 @@
     { fix x' assume "x'\<in>?B" and as:"norm (x' - x) < e"
       hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
 	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
-    hence "\<exists>d>0. \<forall>x'\<in>?B. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_def by auto }
+    hence "\<exists>d>0. \<forall>x'\<in>?B. norm (x' - x) < d \<longrightarrow> \<bar>dist x' a - dist x a\<bar> < e" using `e>0` unfolding dist_norm by auto }
   hence "continuous_on (cball a (dist b a) \<inter> s) (vec1 \<circ> dist a)" unfolding continuous_on_vec1_range
     by (auto  simp add: dist_commute)
   moreover have "compact ?B" using compact_cball[of a "dist b a"] unfolding compact_eq_bounded_closed using bounded_Int and closed_Int and assms(1) by auto
@@ -4120,7 +4122,7 @@
   have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
   then obtain x where x:"x\<in>{x - y |x y. x \<in> s \<and> y \<in> s}"  "\<forall>y\<in>{x - y |x y. x \<in> s \<and> y \<in> s}. norm y \<le> norm x"
     using compact_differences[OF assms(1) assms(1)]
-    using distance_attains_sup[unfolded dist_def, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
+    using distance_attains_sup[unfolded dist_norm, of "{x - y | x y . x\<in>s \<and> y\<in>s}" 0] by(auto simp add: norm_minus_cancel)
   from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
   thus ?thesis using x(2)[unfolded `x = a - b`] by blast
 qed
@@ -4193,7 +4195,7 @@
       { 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_def unfolding vector_ssub_ldistrib[THEN sym] norm_mul
+	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
 	  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"]]
@@ -4301,7 +4303,7 @@
     hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
     hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
       by (auto  simp add: dist_commute)
-    hence "d \<le> dist x y" unfolding dist_def by auto  }
+    hence "d \<le> dist x y" unfolding dist_norm by auto  }
   thus ?thesis using `d>0` by auto
 qed
 
@@ -4504,7 +4506,7 @@
     { fix x' assume as:"dist x' x < ?d"
       { fix i
 	have "\<bar>x'$i - x $ i\<bar> < d i"
-	  using norm_bound_component_lt[OF as[unfolded dist_def], of i]
+	  using norm_bound_component_lt[OF as[unfolded dist_norm], of i]
 	  unfolding vector_minus_component and Min_gr_iff[OF **] by auto
 	hence "a $ i < x' $ i" "x' $ i < b $ i" using d[THEN spec[where x=i]] by auto  }
       hence "a < x' \<and> x' < b" unfolding vector_less_def by auto  }
@@ -4518,13 +4520,13 @@
   { fix x i assume as:"\<forall>e>0. \<exists>x'\<in>{a..b}. x' \<noteq> x \<and> dist x' x < e"(* and xab:"a$i > x$i \<or> b$i < x$i"*)
     { assume xa:"a$i > x$i"
       with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < a$i - x$i" by(erule_tac x="a$i - x$i" in allE)auto
-      hence False unfolding mem_interval and dist_def
+      hence False unfolding mem_interval and dist_norm
 	using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xa by(auto elim!: allE[where x=i])
     } hence "a$i \<le> x$i" by(rule ccontr)auto
     moreover
     { assume xb:"b$i < x$i"
       with as obtain y where y:"y\<in>{a..b}" "y \<noteq> x" "dist y x < x$i - b$i" by(erule_tac x="x$i - b$i" in allE)auto
-      hence False unfolding mem_interval and dist_def
+      hence False unfolding mem_interval and dist_norm
 	using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xb by(auto elim!: allE[where x=i])
     } hence "x$i \<le> b$i" by(rule ccontr)auto
     ultimately
@@ -4543,7 +4545,7 @@
     { fix i
       have "dist (x - (e / 2) *s basis i) x < e"
 	   "dist (x + (e / 2) *s basis i) x < e"
-	unfolding dist_def apply auto
+	unfolding dist_norm apply auto
 	unfolding norm_minus_cancel and norm_mul using norm_basis[of i] and `e>0` by auto
       hence "a $ i \<le> (x - (e / 2) *s basis i) $ i"
                     "(x + (e / 2) *s basis i) $ i \<le> b $ i"
@@ -4761,7 +4763,7 @@
     fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. x $ i \<le> b $ i}. x' \<noteq> x \<and> dist x' x < e"
     { assume "x$i > b$i"
       then obtain y where "y $ i \<le> b $ i"  "y \<noteq> x"  "dist y x < x$i - b$i" using x[THEN spec[where x="x$i - b$i"]] by auto
-      hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto   }
+      hence False using component_le_norm[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
     hence "x$i \<le> b$i" by(rule ccontr)auto  }
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
@@ -4773,7 +4775,7 @@
     fix x::"real^'n" assume x:"\<forall>e>0. \<exists>x'\<in>{x. \<forall>i. a $ i \<le> x $ i}. x' \<noteq> x \<and> dist x' x < e"
     { assume "a$i > x$i"
       then obtain y where "a $ i \<le> y $ i"  "y \<noteq> x"  "dist y x < a$i - x$i" using x[THEN spec[where x="a$i - x$i"]] by auto
-      hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto   }
+      hence False using component_le_norm[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
     hence "a$i \<le> x$i" by(rule ccontr)auto  }
   thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
 qed
@@ -4810,7 +4812,7 @@
     then obtain x y where x:"netord net x y" and y:"\<forall>x. netord net x y \<longrightarrow> dist l (f x) < e / norm a" apply(erule_tac x="e / norm a" in allE) apply auto using False using norm_ge_zero[of a] apply auto
       using divide_pos_pos[of e "norm a"] by auto
     { fix z assume "netord net z y" hence "dist l (f z) < e / norm a" using y by blast
-      hence "norm a * norm (l - f z) < e" unfolding dist_def and
+      hence "norm a * norm (l - f z) < e" unfolding dist_norm and
 	pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto
       hence "\<bar>a \<bullet> l - a \<bullet> f z\<bar> < e" using order_le_less_trans[OF norm_cauchy_schwarz_abs[of a "l - f z"], of e] unfolding dot_rsub[symmetric] by auto  }
     hence "\<exists>y. (\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> \<bar>a \<bullet> l - a \<bullet> f x\<bar> < e)" using x by auto  }
@@ -4980,7 +4982,7 @@
   hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
   then obtain l where "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<bar>dest_vec1 (s n) - l\<bar> < e" using convergent_bounded_monotone[OF a] by auto
   thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
-    unfolding dist_def unfolding abs_dest_vec1 and dest_vec1_sub by auto
+    unfolding dist_norm unfolding abs_dest_vec1 and dest_vec1_sub by auto
 qed
 
 subsection{* Basic homeomorphism definitions.                                          *}
@@ -5119,7 +5121,7 @@
   show ?th unfolding homeomorphic_minimal
     apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
     apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
-    apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
+    apply (auto simp add: dist_commute) unfolding dist_norm and vector_smult_assoc using assms apply auto
     unfolding norm_minus_cancel and norm_mul
     using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
     apply (auto simp add: dist_commute)
@@ -5131,7 +5133,7 @@
   show ?cth unfolding homeomorphic_minimal
     apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
     apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
-    apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
+    apply (auto simp add: dist_commute) unfolding dist_norm and vector_smult_assoc using assms apply auto
     unfolding norm_minus_cancel and norm_mul
     using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
     apply auto
@@ -5148,7 +5150,7 @@
 proof-
   { fix d::real assume "d>0"
     then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
-      using cf[unfolded cauchy o_def dist_def, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
+      using cf[unfolded cauchy o_def dist_norm, THEN spec[where x="e*d"]] and e and mult_pos_pos[of e d] by auto
     { fix n assume "n\<ge>N"
       hence "norm (f (x n - x N)) < e * d" using N[THEN spec[where x=n]] unfolding linear_sub[OF f, THEN sym] by auto
       moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
@@ -5157,7 +5159,7 @@
       ultimately have "norm (x n - x N) < d" using `e>0`
 	using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto   }
     hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
-  thus ?thesis unfolding cauchy and dist_def by auto
+  thus ?thesis unfolding cauchy and dist_norm by auto
 qed
 
 lemma complete_isometric_image:
@@ -5178,7 +5180,10 @@
   thus ?thesis unfolding complete_def by auto
 qed
 
-lemma dist_0_norm:"dist 0 x = norm x" unfolding dist_def by(auto simp add: norm_minus_cancel)
+lemma dist_0_norm:
+  fixes x :: "'a::real_normed_vector"
+  shows "dist 0 x = norm x"
+unfolding dist_norm by simp
 
 lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
   assumes s:"closed s"  "subspace s"  and f:"linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
@@ -5197,7 +5202,7 @@
   let ?S' = "{x::real^'m. x\<in>s \<and> norm x = norm a}"
   let ?S'' = "{x::real^'m. norm x = norm a}"
 
-  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_def by (auto simp add: norm_minus_cancel)
+  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by (auto simp add: norm_minus_cancel)
   hence "compact ?S''" using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
   moreover have "?S' = s \<inter> ?S''" by auto
   ultimately have "compact ?S'" using closed_inter_compact[of s ?S''] using s(1) by auto
@@ -5652,9 +5657,9 @@
     unfolding o_def and h_def a_def b_def  by auto
 
   { fix n::nat
-    have *:"\<And>fx fy (x::real^_) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_def by norm
+    have *:"\<And>fx fy (x::real^_) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
     { fix x y ::"real^'a"
-      have "dist (-x) (-y) = dist x y" unfolding dist_def
+      have "dist (-x) (-y) = dist x y" unfolding dist_norm
 	using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
 
     { assume as:"dist a b > dist (f n x) (f n y)"
diff -r 67dff9c5b2bd -r 847f00f435d4 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu May 28 14:36:21 2009 -0700
+++ b/src/HOL/RealVector.thy	Thu May 28 17:00:02 2009 -0700
@@ -416,6 +416,45 @@
   by (rule Reals_cases) auto
 
 
+subsection {* Metric spaces *}
+
+class dist =
+  fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
+
+class metric_space = dist +
+  assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
+  assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
+begin
+
+lemma dist_self [simp]: "dist x x = 0"
+by simp
+
+lemma zero_le_dist [simp]: "0 \<le> dist x y"
+using dist_triangle2 [of x x y] by simp
+
+lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
+by (simp add: less_le)
+
+lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
+by (simp add: not_less)
+
+lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
+by (simp add: le_less)
+
+lemma dist_commute: "dist x y = dist y x"
+proof (rule order_antisym)
+  show "dist x y \<le> dist y x"
+    using dist_triangle2 [of x y x] by simp
+  show "dist y x \<le> dist x y"
+    using dist_triangle2 [of y x y] by simp
+qed
+
+lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
+using dist_triangle2 [of x z y] by (simp add: dist_commute)
+
+end
+
+
 subsection {* Real normed vector spaces *}
 
 class norm =
@@ -424,7 +463,10 @@
 class sgn_div_norm = scaleR + norm + sgn +
   assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
 
-class real_normed_vector = real_vector + sgn_div_norm +
+class dist_norm = dist + norm + minus +
+  assumes dist_norm: "dist x y = norm (x - y)"
+
+class real_normed_vector = real_vector + sgn_div_norm + dist_norm +
   assumes norm_ge_zero [simp]: "0 \<le> norm x"
   and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
@@ -458,8 +500,12 @@
 definition
   real_norm_def [simp]: "norm r = \<bar>r\<bar>"
 
+definition
+  dist_real_def: "dist x y = \<bar>x - y\<bar>"
+
 instance
 apply (intro_classes, unfold real_norm_def real_scaleR_def)
+apply (rule dist_real_def)
 apply (simp add: real_sgn_def)
 apply (rule abs_ge_zero)
 apply (rule abs_eq_0)
@@ -637,43 +683,17 @@
   shows "norm (x ^ n) = norm x ^ n"
 by (induct n) (simp_all add: norm_mult)
 
-
-subsection {* Distance function *}
-
-(* TODO: There should be a metric_space class for this,
-which should be a superclass of real_normed_vector. *)
-
-definition
-  dist :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real"
-where
-  "dist x y = norm (x - y)"
-
-lemma zero_le_dist [simp]: "0 \<le> dist x y"
-unfolding dist_def by (rule norm_ge_zero)
-
-lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
-unfolding dist_def by simp
+text {* Every normed vector space is a metric space. *}
 
-lemma dist_self [simp]: "dist x x = 0"
-unfolding dist_def by simp
-
-lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
-by (simp add: less_le)
-
-lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
-by (simp add: not_less)
-
-lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
-by (simp add: le_less)
-
-lemma dist_commute: "dist x y = dist y x"
-unfolding dist_def by (rule norm_minus_commute)
-
-lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
-unfolding dist_def
-apply (rule ord_eq_le_trans [OF _ norm_triangle_ineq])
-apply (simp add: diff_minus)
-done
+instance real_normed_vector < metric_space
+proof
+  fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y"
+    unfolding dist_norm by simp
+next
+  fix x y z :: 'a show "dist x y \<le> dist x z + dist y z"
+    unfolding dist_norm
+    using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
+qed
 
 
 subsection {* Sign function *}