move dist operation to new metric_space class
authorhuffman
Thu May 28 17:00:02 2009 -0700 (2009-05-28)
changeset 31289847f00f435d4
parent 31288 67dff9c5b2bd
child 31290 f41c023d90bc
move dist operation to new metric_space class
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Topology_Euclidean_Space.thy
src/HOL/RealVector.thy
     1.1 --- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 14:36:21 2009 -0700
     1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 17:00:02 2009 -0700
     1.3 @@ -118,7 +118,7 @@
     1.4  
     1.5  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)"
     1.6  proof- have *:"x - y + (y - z) = x - z" by auto
     1.7 -  show ?thesis unfolding dist_def norm_triangle_eq[of "x - y" "y - z", unfolded *] 
     1.8 +  show ?thesis unfolding dist_norm norm_triangle_eq[of "x - y" "y - z", unfolded *] 
     1.9      by(auto simp add:norm_minus_commute) qed
    1.10  
    1.11  lemma norm_eqI:"x = y \<Longrightarrow> norm x = norm y" by auto 
    1.12 @@ -601,7 +601,7 @@
    1.13  
    1.14      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"
    1.15        apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
    1.16 -      using * apply(simp add: dist_def)
    1.17 +      using * apply(simp add: dist_norm)
    1.18        using as(1,2)[unfolded open_def] apply simp
    1.19        using as(1,2)[unfolded open_def] apply simp
    1.20        using assms[unfolded convex_alt, THEN bspec[where x=x1], THEN bspec[where x=x2]] using x1 x2
    1.21 @@ -675,14 +675,14 @@
    1.22      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
    1.23    moreover
    1.24    have *:"x - ((1 - u) *s x + u *s y) = u *s (x - y)" by (simp add: vector_ssub_ldistrib vector_sub_rdistrib)
    1.25 -  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]
    1.26 +  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]
    1.27      using u unfolding pos_less_divide_eq[OF xy] by auto
    1.28    hence "f x \<le> f ((1 - u) *s x + u *s y)" using assms(4) by auto
    1.29    ultimately show False using mult_strict_left_mono[OF y `u>0`] unfolding left_diff_distrib by auto
    1.30  qed
    1.31  
    1.32  lemma convex_distance: "convex_on s (\<lambda>x. dist a x)"
    1.33 -proof(auto simp add: convex_on_def dist_def)
    1.34 +proof(auto simp add: convex_on_def dist_norm)
    1.35    fix x y assume "x\<in>s" "y\<in>s"
    1.36    fix u v ::real assume "0 \<le> u" "0 \<le> v" "u + v = 1"
    1.37    have "a = u *s a + v *s a" unfolding vector_sadd_rdistrib[THEN sym] and `u+v=1` by simp
    1.38 @@ -782,7 +782,7 @@
    1.39  proof- from assms obtain B where B:"\<forall>x\<in>s. norm x \<le> B" unfolding bounded_def by auto
    1.40    show ?thesis apply(rule bounded_subset[OF bounded_cball, of _ 0 B])
    1.41      unfolding subset_hull[unfolded mem_def, of convex, OF convex_cball]
    1.42 -    unfolding subset_eq mem_cball dist_def using B by auto qed
    1.43 +    unfolding subset_eq mem_cball dist_norm using B by auto qed
    1.44  
    1.45  lemma finite_imp_bounded_convex_hull:
    1.46    "finite s \<Longrightarrow> bounded(convex hull s)"
    1.47 @@ -1222,10 +1222,10 @@
    1.48      show "0 < Min i" unfolding i_def and Min_gr_iff[OF finite_imageI[OF obt(1)] `b \` t\<noteq>{}`]
    1.49        using b apply simp apply rule apply(erule_tac x=x in ballE) using `t\<subseteq>s` by auto
    1.50    next  fix y assume "y \<in> cball a (Min i)"
    1.51 -    hence y:"norm (a - y) \<le> Min i" unfolding dist_def[THEN sym] by auto
    1.52 +    hence y:"norm (a - y) \<le> Min i" unfolding dist_norm[THEN sym] by auto
    1.53      { fix x assume "x\<in>t"
    1.54        hence "Min i \<le> b x" unfolding i_def apply(rule_tac Min_le) using obt(1) by auto
    1.55 -      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_def by auto
    1.56 +      hence "x + (y - a) \<in> cball x (b x)" using y unfolding mem_cball dist_norm by auto
    1.57        moreover from `x\<in>t` have "x\<in>s" using obt(2) by auto
    1.58        ultimately have "x + (y - a) \<in> s" using y and b[THEN bspec[where x=x]] unfolding subset_eq by auto }
    1.59      moreover
    1.60 @@ -1355,18 +1355,18 @@
    1.61  proof(cases "a \<bullet> d - b \<bullet> d > 0")
    1.62    case True hence "0 < d \<bullet> d + (a \<bullet> d * 2 - b \<bullet> d * 2)" 
    1.63      apply(rule_tac add_pos_pos) using assms by auto
    1.64 -  thus ?thesis apply(rule_tac disjI2) unfolding dist_def and real_vector_norm_def and real_sqrt_less_iff
    1.65 +  thus ?thesis apply(rule_tac disjI2) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
    1.66      by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
    1.67  next
    1.68    case False hence "0 < d \<bullet> d + (b \<bullet> d * 2 - a \<bullet> d * 2)" 
    1.69      apply(rule_tac add_pos_nonneg) using assms by auto
    1.70 -  thus ?thesis apply(rule_tac disjI1) unfolding dist_def and real_vector_norm_def and real_sqrt_less_iff
    1.71 +  thus ?thesis apply(rule_tac disjI1) unfolding dist_norm and real_vector_norm_def and real_sqrt_less_iff
    1.72      by(simp add: dot_rsub dot_radd dot_lsub dot_ladd dot_sym field_simps)
    1.73  qed
    1.74  
    1.75  lemma norm_increases_online:
    1.76   "(d::real^'n::finite) \<noteq> 0 \<Longrightarrow> norm(a + d) > norm a \<or> norm(a - d) > norm a"
    1.77 -  using dist_increases_online[of d a 0] unfolding dist_def by auto
    1.78 +  using dist_increases_online[of d a 0] unfolding dist_norm by auto
    1.79  
    1.80  lemma simplex_furthest_lt:
    1.81    fixes s::"(real^'n::finite) set" assumes "finite s"
    1.82 @@ -1402,7 +1402,7 @@
    1.83   	proof(erule_tac disjE)
    1.84  	  assume "dist a y < dist a (y + w *s (x - b))"
    1.85  	  hence "norm (y - a) < norm ((u + w) *s x + (v - w) *s b - a)"
    1.86 -	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
    1.87 +	    unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: ring_simps)
    1.88  	  moreover have "(u + w) *s x + (v - w) *s b \<in> convex hull insert x s"
    1.89  	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
    1.90  	    apply(rule_tac x="u + w" in exI) apply rule defer 
    1.91 @@ -1411,7 +1411,7 @@
    1.92  	next
    1.93  	  assume "dist a y < dist a (y - w *s (x - b))"
    1.94  	  hence "norm (y - a) < norm ((u - w) *s x + (v + w) *s b - a)"
    1.95 -	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
    1.96 +	    unfolding dist_commute[of a] unfolding dist_norm obt(5) by (simp add: ring_simps)
    1.97  	  moreover have "(u - w) *s x + (v + w) *s b \<in> convex hull insert x s"
    1.98  	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
    1.99  	    apply(rule_tac x="u - w" in exI) apply rule defer 
   1.100 @@ -1430,7 +1430,7 @@
   1.101    have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
   1.102    then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
   1.103      using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
   1.104 -    unfolding dist_commute[of a] unfolding dist_def by auto
   1.105 +    unfolding dist_commute[of a] unfolding dist_norm by auto
   1.106    thus ?thesis proof(cases "x\<in>s")
   1.107      case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
   1.108        using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
   1.109 @@ -1469,7 +1469,8 @@
   1.110  
   1.111  subsection {* Closest point of a convex set is unique, with a continuous projection. *}
   1.112  
   1.113 -definition 
   1.114 +definition
   1.115 +  closest_point :: "(real ^ 'n::finite) set \<Rightarrow> real ^ 'n \<Rightarrow> real ^ 'n" where
   1.116   "closest_point s a = (SOME x. x \<in> s \<and> (\<forall>y\<in>s. dist a x \<le> dist a y))"
   1.117  
   1.118  lemma closest_point_exists:
   1.119 @@ -1512,7 +1513,7 @@
   1.120  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)"
   1.121      using closer_points_lemma[OF assms] by auto
   1.122    show ?thesis apply(rule_tac x="min u 1" in exI) using u[THEN spec[where x="min u 1"]] and `u>0`
   1.123 -    unfolding dist_def by(auto simp add: norm_minus_commute field_simps) qed
   1.124 +    unfolding dist_norm by(auto simp add: norm_minus_commute field_simps) qed
   1.125  
   1.126  lemma any_closest_point_dot:
   1.127    assumes "convex s" "closed s" "x \<in> s" "y \<in> s" "\<forall>z\<in>s. dist a x \<le> dist a z"
   1.128 @@ -1555,7 +1556,7 @@
   1.129         "(y - closest_point s y) \<bullet> (closest_point s x - closest_point s y) \<le> 0"
   1.130      apply(rule_tac[!] any_closest_point_dot[OF assms(1-2)])
   1.131      using closest_point_exists[OF assms(2-3)] by auto
   1.132 -  thus ?thesis unfolding dist_def and norm_le
   1.133 +  thus ?thesis unfolding dist_norm and norm_le
   1.134      using dot_pos_le[of "(x - closest_point s x) - (y - closest_point s y)"]
   1.135      by (auto simp add: dot_sym dot_ladd dot_radd) qed
   1.136  
   1.137 @@ -1686,9 +1687,9 @@
   1.138         using hull_subset[of c convex] unfolding subset_eq and dot_rmult
   1.139         apply- apply rule defer apply rule apply(rule mult_nonneg_nonneg)
   1.140         by(auto simp add: dot_sym elim!: ballE) 
   1.141 -    thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_def by auto
   1.142 +    thus "frontier (cball 0 1) \<inter> \<Inter>f \<noteq> {}" unfolding c(1) frontier_cball dist_norm by auto
   1.143    qed(insert closed_halfspace_ge, auto)
   1.144 -  then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_def by auto
   1.145 +  then obtain x where "norm x = 1" "\<forall>y\<in>s. x\<in>?k y" unfolding frontier_cball dist_norm by auto
   1.146    thus ?thesis apply(rule_tac x=x in exI) by(auto simp add: dot_sym) qed
   1.147  
   1.148  lemma separating_hyperplane_sets:
   1.149 @@ -1719,7 +1720,7 @@
   1.150      fix z assume "z \<in> ball ((1 - u) *s x + u *s y) (min d e)"
   1.151      hence "(1- u) *s (z - u *s (y - x)) + u *s (z + (1 - u) *s (y - x)) \<in> s"
   1.152        apply(rule_tac assms[unfolded convex_alt, rule_format])
   1.153 -      using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_def by(auto simp add: ring_simps)
   1.154 +      using ed(1,2) and u unfolding subset_eq mem_ball Ball_def dist_norm by(auto simp add: ring_simps)
   1.155      thus "z \<in> s" using u by (auto simp add: ring_simps) qed(insert u ed(3-4), auto) qed
   1.156  
   1.157  lemma convex_hull_eq_empty: "convex hull s = {} \<longleftrightarrow> s = {}"
   1.158 @@ -1934,7 +1935,7 @@
   1.159      fix e  assume "0 < e" and as:"(u + e / 2 / norm x) *s x \<in> s"
   1.160      hence "u + e / 2 / norm x > u" using`norm x > 0` by(auto simp del:zero_less_norm_iff intro!: divide_pos_pos)
   1.161      thus False using u_max[OF _ as] by auto
   1.162 -  qed(insert `y\<in>s`, auto simp add: dist_def obt(3))
   1.163 +  qed(insert `y\<in>s`, auto simp add: dist_norm obt(3))
   1.164    thus ?thesis apply(rule_tac that[of u]) apply(rule obt(1), assumption)
   1.165      apply(rule,rule,rule ccontr) apply(rule u_max) by auto qed
   1.166  
   1.167 @@ -2004,7 +2005,7 @@
   1.168  
   1.169    { fix x assume as:"x \<in> cball (0::real^'n) 1"
   1.170      have "norm x *s surf (pi x) \<in> s" proof(cases "x=0 \<or> norm x = 1") 
   1.171 -      case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_def)
   1.172 +      case False hence "pi x \<in> sphere" "norm x < 1" using pi(1)[of x] as by(auto simp add: dist_norm)
   1.173        thus ?thesis apply(rule_tac assms(3)[rule_format, THEN DiffD1])
   1.174  	apply(rule_tac fs[unfolded subset_eq, rule_format])
   1.175  	unfolding surf(5)[THEN sym] by auto
   1.176 @@ -2027,7 +2028,7 @@
   1.177        moreover have "pi x = pi ((inverse (norm (surf (pi x))) * norm x) *s surf (pi x))" 
   1.178  	unfolding pi(2)[OF *] surf(4)[rule_format, OF pix] ..
   1.179        moreover have "surf (pi x) \<in> frontier s" using surf(5) pix by auto
   1.180 -      hence "dist 0 (inverse (norm (surf (pi x))) *s x) \<le> 1" unfolding dist_def
   1.181 +      hence "dist 0 (inverse (norm (surf (pi x))) *s x) \<le> 1" unfolding dist_norm
   1.182  	using ** and * using front_smul[THEN bspec[where x="surf (pi x)"], THEN spec[where x="norm x * ?a"]]
   1.183  	using False `x\<in>s` by(auto simp add:field_simps)
   1.184        ultimately show ?thesis unfolding image_iff apply(rule_tac x="inverse (norm (surf(pi x))) *s x" in bexI)
   1.185 @@ -2040,15 +2041,15 @@
   1.186      prefer 4 apply(rule continuous_at_imp_continuous_on, rule) apply(rule_tac [3] hom2) proof-
   1.187      fix x::"real^'n" assume as:"x \<in> cball 0 1"
   1.188      thus "continuous (at x) (\<lambda>x. norm x *s surf (pi x))" proof(cases "x=0")
   1.189 -      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm[THEN spec])
   1.190 +      case False thus ?thesis apply(rule_tac continuous_mul, rule_tac continuous_at_vec1_norm)
   1.191  	using cont_surfpi unfolding continuous_on_eq_continuous_at[OF open_delete[OF open_UNIV]] o_def by auto
   1.192      next guess a using UNIV_witness[where 'a = 'n] ..
   1.193        obtain B where B:"\<forall>x\<in>s. norm x \<le> B" using compact_imp_bounded[OF assms(1)] unfolding bounded_def by auto
   1.194        hence "B > 0" using assms(2) unfolding subset_eq apply(erule_tac x="basis a" in ballE) defer apply(erule_tac x="basis a" in ballE)
   1.195 -	unfolding Ball_def mem_cball dist_def by (auto simp add: norm_basis[unfolded One_nat_def])
   1.196 +	unfolding Ball_def mem_cball dist_norm by (auto simp add: norm_basis[unfolded One_nat_def])
   1.197        case True show ?thesis unfolding True continuous_at Lim_at apply(rule,rule) apply(rule_tac x="e / B" in exI)
   1.198  	apply(rule) apply(rule divide_pos_pos) prefer 3 apply(rule,rule,erule conjE)
   1.199 -	unfolding norm_0 vector_smult_lzero dist_def diff_0_right norm_mul abs_norm_cancel proof-
   1.200 +	unfolding norm_0 vector_smult_lzero dist_norm diff_0_right norm_mul abs_norm_cancel proof-
   1.201  	fix e and x::"real^'n" assume as:"norm x < e / B" "0 < norm x" "0<e"
   1.202  	hence "surf (pi x) \<in> frontier s" using pi(1)[of x] unfolding surf(5)[THEN sym] by auto
   1.203  	hence "norm (surf (pi x)) \<le> B" using B fs by auto
   1.204 @@ -2086,7 +2087,7 @@
   1.205      unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
   1.206      fix y assume "dist (u *s x) y < 1 - u"
   1.207      hence "inverse (1 - u) *s (y - u *s x) \<in> s"
   1.208 -      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_def
   1.209 +      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
   1.210        unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_mul      
   1.211        apply (rule mult_left_le_imp_le[of "1 - u"])
   1.212        unfolding class_semiring.mul_a using `u<1` by auto
   1.213 @@ -2102,7 +2103,7 @@
   1.214    let ?d = "inverse d" and ?n = "0::real^'n"
   1.215    have "cball ?n 1 \<subseteq> (\<lambda>x. inverse d *s (x - a)) ` s"
   1.216      apply(rule, rule_tac x="d *s x + a" in image_eqI) defer
   1.217 -    apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_def
   1.218 +    apply(rule d[unfolded subset_eq, rule_format]) using `d>0` unfolding mem_cball dist_norm
   1.219      by(auto simp add: mult_right_le_one_le)
   1.220    hence "(\<lambda>x. inverse d *s (x - a)) ` s homeomorphic cball ?n 1"
   1.221      using homeomorphic_convex_compact_lemma[of "(\<lambda>x. ?d *s -a + ?d *s x) ` s", OF convex_affinity compact_affinity]
   1.222 @@ -2368,10 +2369,10 @@
   1.223      show "\<bar>f y - f x\<bar> < e" proof(cases "y=x")
   1.224        case False def t \<equiv> "k / norm (y - x)"
   1.225        have "2 < t" "0<t" unfolding t_def using as False and `k>0` by(auto simp add:field_simps)
   1.226 -      have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def
   1.227 +      have "y\<in>s" apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm
   1.228  	apply(rule order_trans[of _ "2 * norm (x - y)"]) using as by(auto simp add: field_simps norm_minus_commute) 
   1.229        { def w \<equiv> "x + t *s (y - x)"
   1.230 -	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def 
   1.231 +	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm 
   1.232  	  unfolding t_def using `k>0` by(auto simp add: norm_mul simp del: vector_ssub_ldistrib) 
   1.233  	have "(1 / t) *s x + - x + ((t - 1) / t) *s x = (1 / t - 1 + (t - 1) / t) *s x" by auto 
   1.234  	also have "\<dots> = 0"  using `t>0` by(auto simp add:field_simps simp del:vector_sadd_rdistrib)
   1.235 @@ -2384,7 +2385,7 @@
   1.236  	  using `0<t` `2<t` and `x\<in>s` `w\<in>s` by(auto simp add:field_simps) }
   1.237        moreover 
   1.238        { def w \<equiv> "x - t *s (y - x)"
   1.239 -	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_def 
   1.240 +	have "w\<in>s" unfolding w_def apply(rule k[unfolded subset_eq,rule_format]) unfolding mem_cball dist_norm 
   1.241  	  unfolding t_def using `k>0` by(auto simp add: norm_mul simp del: vector_ssub_ldistrib) 
   1.242  	have "(1 / (1 + t)) *s x + (t / (1 + t)) *s x = (1 / (1 + t) + t / (1 + t)) *s x" by auto
   1.243  	also have "\<dots>=x" using `t>0` by (auto simp add:field_simps simp del:vector_sadd_rdistrib)
   1.244 @@ -2409,7 +2410,7 @@
   1.245    apply(rule) proof(cases "0 \<le> e") case True
   1.246    fix y assume y:"y\<in>cball x e" def z \<equiv> "2 *s x - y"
   1.247    have *:"x - (2 *s x - y) = y - x" by vector
   1.248 -  have z:"z\<in>cball x e" using y unfolding z_def mem_cball dist_def * by(auto simp add: norm_minus_commute)
   1.249 +  have z:"z\<in>cball x e" using y unfolding z_def mem_cball dist_norm * by(auto simp add: norm_minus_commute)
   1.250    have "(1 / 2) *s y + (1 / 2) *s z = x" unfolding z_def by auto
   1.251    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"]
   1.252      using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by(auto simp add:field_simps)
   1.253 @@ -2438,7 +2439,7 @@
   1.254      fix z assume z:"z\<in>{x - ?d..x + ?d}"
   1.255      have e:"e = setsum (\<lambda>i. d) (UNIV::'n set)" unfolding setsum_constant d_def using dimge1
   1.256        by (metis card_enum field_simps d_def not_one_le_zero of_nat_le_iff real_eq_of_nat real_of_nat_1)
   1.257 -    show "dist x z \<le> e" unfolding dist_def e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
   1.258 +    show "dist x z \<le> e" unfolding dist_norm e apply(rule_tac order_trans[OF norm_le_l1], rule setsum_mono)
   1.259        using z[unfolded mem_interval] apply(erule_tac x=i in allE) by(auto simp add:field_simps vector_component_simps) qed
   1.260    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
   1.261      unfolding k_def apply(rule, rule Max_ge) using c(1) by auto
   1.262 @@ -2448,8 +2449,8 @@
   1.263    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
   1.264      fix y assume y:"y\<in>cball x d"
   1.265      { fix i::'n have "x $ i - d \<le> y $ i"  "y $ i \<le> x $ i + d" 
   1.266 -	using order_trans[OF component_le_norm y[unfolded mem_cball dist_def], of i] by(auto simp add: vector_component)  }
   1.267 -    thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_def 
   1.268 +	using order_trans[OF component_le_norm y[unfolded mem_cball dist_norm], of i] by(auto simp add: vector_component)  }
   1.269 +    thus "f y \<le> k" apply(rule_tac k[rule_format]) unfolding mem_cball mem_interval dist_norm 
   1.270        by(auto simp add: vector_component_simps) qed
   1.271    hence "continuous_on (ball x d) (vec1 \<circ> f)" apply(rule_tac convex_on_bounded_continuous)
   1.272      apply(rule open_ball, rule convex_on_subset[OF conv], rule ball_subset_cball) by auto
   1.273 @@ -2484,10 +2485,10 @@
   1.274  proof-
   1.275    have *: "\<And>x y::real^'n::finite. 2 *s x = - y \<Longrightarrow> norm x = (norm y) / 2" unfolding equation_minus_iff by auto
   1.276    have **:"\<And>x y::real^'n::finite. 2 *s x =   y \<Longrightarrow> norm x = (norm y) / 2" by auto
   1.277 -  show ?t1 unfolding midpoint_def dist_def apply (rule **) by(auto,vector)
   1.278 -  show ?t2 unfolding midpoint_def dist_def apply (rule *)  by(auto,vector)
   1.279 -  show ?t3 unfolding midpoint_def dist_def apply (rule *)  by(auto,vector)
   1.280 -  show ?t4 unfolding midpoint_def dist_def apply (rule **) by(auto,vector) qed
   1.281 +  show ?t1 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector)
   1.282 +  show ?t2 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
   1.283 +  show ?t3 unfolding midpoint_def dist_norm apply (rule *)  by(auto,vector)
   1.284 +  show ?t4 unfolding midpoint_def dist_norm apply (rule **) by(auto,vector) qed
   1.285  
   1.286  lemma midpoint_eq_endpoint:
   1.287    "midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
   1.288 @@ -2550,14 +2551,14 @@
   1.289  	unfolding norm_minus_commute[of x a] * norm_mul Cart_eq using as(2,3)
   1.290  	by(auto simp add: vector_component_simps field_simps)
   1.291      next assume as:"dist a b = dist a x + dist x b"
   1.292 -      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 
   1.293 +      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 
   1.294        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)
   1.295 -	unfolding dist_def Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
   1.296 +	unfolding dist_norm Cart_eq apply- apply rule defer apply(rule, rule divide_nonneg_pos) prefer 4 proof rule
   1.297  	  fix i::'n have "((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i =
   1.298  	    ((norm (a - b) - norm (a - x)) * (a $ i) + norm (a - x) * (b $ i)) / norm (a - b)"
   1.299  	    using Fal by(auto simp add:vector_component_simps field_simps)
   1.300  	  also have "\<dots> = x$i" apply(rule divide_eq_imp[OF Fal])
   1.301 -	    unfolding as[unfolded dist_def] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
   1.302 +	    unfolding as[unfolded dist_norm] using as[unfolded dist_triangle_eq Cart_eq,rule_format, of i]
   1.303  	    by(auto simp add:field_simps vector_component_simps)
   1.304  	  finally show "x $ i = ((1 - norm (a - x) / norm (a - b)) *s a + (norm (a - x) / norm (a - b)) *s b) $ i" by auto
   1.305  	qed(insert Fal2, auto) qed qed
   1.306 @@ -2566,7 +2567,7 @@
   1.307    "between (a,b) (midpoint a b)" (is ?t1) 
   1.308    "between (b,a) (midpoint a b)" (is ?t2)
   1.309  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
   1.310 -  show ?t1 ?t2 unfolding between midpoint_def dist_def apply(rule_tac[!] *)
   1.311 +  show ?t1 ?t2 unfolding between midpoint_def dist_norm apply(rule_tac[!] *)
   1.312      by(auto simp add:field_simps Cart_eq vector_component_simps) qed
   1.313  
   1.314  lemma between_mem_convex_hull:
   1.315 @@ -2584,10 +2585,10 @@
   1.316      fix y assume as:"dist (x - e *s (x - c)) y < e * d"
   1.317      have *:"y = (1 - (1 - e)) *s ((1 / e) *s y - ((1 - e) / e) *s x) + (1 - e) *s x" using `e>0` by auto
   1.318      have "dist c ((1 / e) *s y - ((1 - e) / e) *s x) = abs(1/e) * norm (e *s c - y + (1 - e) *s x)"
   1.319 -      unfolding dist_def unfolding norm_mul[THEN sym] apply(rule norm_eqI) using `e>0`
   1.320 +      unfolding dist_norm unfolding norm_mul[THEN sym] apply(rule norm_eqI) using `e>0`
   1.321        by(auto simp add:vector_component_simps Cart_eq field_simps) 
   1.322      also have "\<dots> = abs(1/e) * norm (x - e *s (x - c) - y)" by(auto intro!:norm_eqI)
   1.323 -    also have "\<dots> < d" using as[unfolded dist_def] and `e>0`
   1.324 +    also have "\<dots> < d" using as[unfolded dist_norm] and `e>0`
   1.325        by(auto simp add:pos_divide_less_eq[OF `e>0`] real_mult_commute)
   1.326      finally show "y \<in> s" apply(subst *) apply(rule assms(1)[unfolded convex_alt,rule_format])
   1.327        apply(rule d[unfolded subset_eq,rule_format]) unfolding mem_ball using assms(3-5) by auto
   1.328 @@ -2608,12 +2609,12 @@
   1.329  	using `e\<le>1` `e>0` `d>0` by(auto intro!:mult_pos_pos divide_pos_pos)
   1.330        then obtain y where "y\<in>s" "y \<noteq> x" "dist y x < e * d / (1 - e)"
   1.331  	using x[unfolded islimpt_approachable,THEN spec[where x="e*d / (1 - e)"]] by auto
   1.332 -      thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_def using pos_less_divide_eq[OF *] by auto qed qed
   1.333 +      thus ?thesis apply(rule_tac x=y in bexI) unfolding dist_norm using pos_less_divide_eq[OF *] by auto qed qed
   1.334    then obtain y where "y\<in>s" and y:"norm (y - x) * (1 - e) < e * d" by auto
   1.335    def z \<equiv> "c + ((1 - e) / e) *s (x - y)"
   1.336    have *:"x - e *s (x - c) = y - e *s (y - z)" unfolding z_def using `e>0` by auto
   1.337    have "z\<in>interior s" apply(rule subset_interior[OF d,unfolded subset_eq,rule_format])
   1.338 -    unfolding interior_open[OF open_ball] mem_ball z_def dist_def using y and assms(4,5)
   1.339 +    unfolding interior_open[OF open_ball] mem_ball z_def dist_norm using y and assms(4,5)
   1.340      by(auto simp del:vector_ssub_ldistrib simp add:field_simps norm_minus_commute) 
   1.341    thus ?thesis unfolding * apply - apply(rule mem_interior_convex_shrink) 
   1.342      using assms(1,4-5) `y\<in>s` by auto qed
   1.343 @@ -2656,10 +2657,10 @@
   1.344    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"
   1.345    show "(\<forall>xa. 0 < x $ xa) \<and> setsum (op $ x) UNIV < 1" apply(rule,rule) proof-
   1.346      fix i::'n show "0 < x $ i" using as[THEN spec[where x="x - (e / 2) *s basis i"]] and `e>0`
   1.347 -      unfolding dist_def by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
   1.348 +      unfolding dist_norm by(auto simp add: norm_basis vector_component_simps basis_component elim:allE[where x=i])
   1.349    next guess a using UNIV_witness[where 'a='n] ..
   1.350      have **:"dist x (x + (e / 2) *s basis a) < e" using  `e>0` and norm_basis[of a]
   1.351 -      unfolding dist_def by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
   1.352 +      unfolding dist_norm by(auto simp add: vector_component_simps basis_component intro!: mult_strict_left_mono_comm)
   1.353      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)
   1.354      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) 
   1.355      have "setsum (op $ x) UNIV < setsum (op $ (x + (e / 2) *s basis a)) UNIV" unfolding * setsum_addf
   1.356 @@ -2677,11 +2678,11 @@
   1.357      fix y assume y:"dist x y < min (Min (op $ x ` UNIV)) ?d"
   1.358      have "setsum (op $ y) UNIV \<le> setsum (\<lambda>i. x$i + ?d) UNIV" proof(rule setsum_mono)
   1.359        fix i::'n have "abs (y$i - x$i) < ?d" apply(rule le_less_trans) using component_le_norm[of "y - x" i]
   1.360 -	using y[unfolded min_less_iff_conj dist_def, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
   1.361 +	using y[unfolded min_less_iff_conj dist_norm, THEN conjunct2] by(auto simp add:vector_component_simps norm_minus_commute)
   1.362        thus "y $ i \<le> x $ i + ?d" by auto qed
   1.363      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)
   1.364      finally show "(\<forall>i. 0 \<le> y $ i) \<and> setsum (op $ y) UNIV \<le> 1" apply- proof(rule,rule)
   1.365 -      fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_def, THEN conjunct1]
   1.366 +      fix i::'n have "norm (x - y) < x$i" using y[unfolded min_less_iff_conj dist_norm, THEN conjunct1]
   1.367  	using Min_gr_iff[of "op $ x ` dimset x"] dimindex_ge_1 by auto
   1.368        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)
   1.369      qed auto qed auto qed
   1.370 @@ -3225,7 +3226,7 @@
   1.371      unfolding image_iff apply(rule_tac x=x in bexI) unfolding mem_Collect_eq norm_mul by(auto intro!: ***) 
   1.372    have "continuous_on (UNIV - {0}) (vec1 \<circ> (\<lambda>x::real^'n. 1 / norm x))" unfolding o_def continuous_on_eq_continuous_within
   1.373      apply(rule, rule continuous_at_within_inv[unfolded o_def inverse_eq_divide]) apply(rule continuous_at_within)
   1.374 -    apply(rule continuous_at_vec1_norm[unfolded o_def,THEN spec]) by auto
   1.375 +    apply(rule continuous_at_vec1_norm[unfolded o_def]) by auto
   1.376    thus ?thesis unfolding * ** using path_connected_punctured_universe[OF assms]
   1.377      by(auto intro!: path_connected_continuous_image continuous_on_intros continuous_on_mul) qed
   1.378  
   1.379 @@ -3234,4 +3235,4 @@
   1.380   
   1.381  (** In continuous_at_vec1_norm : Use \<And> instead of \<forall>. **)
   1.382  
   1.383 -end
   1.384 \ No newline at end of file
   1.385 +end
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu May 28 14:36:21 2009 -0700
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu May 28 17:00:02 2009 -0700
     2.3 @@ -509,6 +509,9 @@
     2.4  definition vector_sgn_def:
     2.5    "sgn (x::'a^'b) = scaleR (inverse (norm x)) x"
     2.6  
     2.7 +definition dist_vector_def:
     2.8 +  "dist (x::'a^'b) y = norm (x - y)"
     2.9 +
    2.10  instance proof
    2.11    fix a :: real and x y :: "'a ^ 'b"
    2.12    show "0 \<le> norm x"
    2.13 @@ -527,6 +530,8 @@
    2.14      by (simp add: norm_scaleR setL2_right_distrib)
    2.15    show "sgn x = scaleR (inverse (norm x)) x"
    2.16      by (rule vector_sgn_def)
    2.17 +  show "dist x y = norm (x - y)"
    2.18 +    by (rule dist_vector_def)
    2.19  qed
    2.20  
    2.21  end
    2.22 @@ -621,7 +626,7 @@
    2.23    by (simp add: norm_vector_1)
    2.24  
    2.25  lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
    2.26 -  by (auto simp add: norm_real dist_def)
    2.27 +  by (auto simp add: norm_real dist_norm)
    2.28  
    2.29  subsection {* A connectedness or intermediate value lemma with several applications. *}
    2.30  
    2.31 @@ -953,37 +958,52 @@
    2.32  
    2.33  text{* Hence more metric properties. *}
    2.34  
    2.35 -lemma dist_triangle_alt: "dist y z <= dist x y + dist x z"
    2.36 +lemma dist_triangle_alt:
    2.37 +  fixes x y z :: "'a::metric_space"
    2.38 +  shows "dist y z <= dist x y + dist x z"
    2.39  using dist_triangle [of y z x] by (simp add: dist_commute)
    2.40  
    2.41 -lemma dist_triangle2: "dist x y \<le> dist x z + dist y z"
    2.42 -using dist_triangle [of x y z] by (simp add: dist_commute)
    2.43 -
    2.44 -lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by (simp add: zero_less_dist_iff)
    2.45 -lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by (simp add: zero_less_dist_iff)
    2.46 -
    2.47 -lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    2.48 +lemma dist_pos_lt:
    2.49 +  fixes x y :: "'a::metric_space"
    2.50 +  shows "x \<noteq> y ==> 0 < dist x y"
    2.51 +by (simp add: zero_less_dist_iff)
    2.52 +
    2.53 +lemma dist_nz:
    2.54 +  fixes x y :: "'a::metric_space"
    2.55 +  shows "x \<noteq> y \<longleftrightarrow> 0 < dist x y"
    2.56 +by (simp add: zero_less_dist_iff)
    2.57 +
    2.58 +lemma dist_triangle_le:
    2.59 +  fixes x y z :: "'a::metric_space"
    2.60 +  shows "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    2.61  by (rule order_trans [OF dist_triangle2])
    2.62  
    2.63 -lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e"
    2.64 +lemma dist_triangle_lt:
    2.65 +  fixes x y z :: "'a::metric_space"
    2.66 +  shows "dist x z + dist y z < e ==> dist x y < e"
    2.67  by (rule le_less_trans [OF dist_triangle2])
    2.68  
    2.69  lemma dist_triangle_half_l:
    2.70 -  "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    2.71 +  fixes x1 x2 y :: "'a::metric_space"
    2.72 +  shows "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    2.73  by (rule dist_triangle_lt [where z=y], simp)
    2.74  
    2.75  lemma dist_triangle_half_r:
    2.76 -  "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    2.77 +  fixes x1 x2 y :: "'a::metric_space"
    2.78 +  shows "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    2.79  by (rule dist_triangle_half_l, simp_all add: dist_commute)
    2.80  
    2.81 -lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'"
    2.82 -unfolding dist_def by (rule norm_diff_triangle_ineq)
    2.83 +lemma dist_triangle_add:
    2.84 +  fixes x y x' y' :: "'a::real_normed_vector"
    2.85 +  shows "dist (x + y) (x' + y') <= dist x x' + dist y y'"
    2.86 +unfolding dist_norm by (rule norm_diff_triangle_ineq)
    2.87  
    2.88  lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
    2.89 -  unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul ..
    2.90 +  unfolding dist_norm vector_ssub_ldistrib[symmetric] norm_mul ..
    2.91  
    2.92  lemma dist_triangle_add_half:
    2.93 -  " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
    2.94 +  fixes x x' y y' :: "'a::real_normed_vector"
    2.95 +  shows "dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
    2.96  by (rule le_less_trans [OF dist_triangle_add], simp)
    2.97  
    2.98  lemma setsum_component [simp]:
    2.99 @@ -1222,7 +1242,7 @@
   2.100  proof-
   2.101    from vector_choose_size[OF e] obtain c:: "real ^'n"  where "norm c = e"
   2.102      by blast
   2.103 -  then have "dist x (x - c) = e" by (simp add: dist_def)
   2.104 +  then have "dist x (x - c) = e" by (simp add: dist_norm)
   2.105    then show ?thesis by blast
   2.106  qed
   2.107  
   2.108 @@ -2546,7 +2566,7 @@
   2.109  qed
   2.110  
   2.111  lemma dist_fstcart: "dist(fstcart (x::real^_)) (fstcart y) <= dist x y"
   2.112 -  by (metis dist_def fstcart_sub[symmetric] norm_fstcart)
   2.113 +  by (metis dist_vector_def fstcart_sub[symmetric] norm_fstcart)
   2.114  
   2.115  lemma norm_sndcart: "norm(sndcart x) <= norm (x::real ^('n::finite + 'm::finite))"
   2.116  proof-
   2.117 @@ -2561,7 +2581,7 @@
   2.118  qed
   2.119  
   2.120  lemma dist_sndcart: "dist(sndcart (x::real^_)) (sndcart y) <= dist x y"
   2.121 -  by (metis dist_def sndcart_sub[symmetric] norm_sndcart)
   2.122 +  by (metis dist_vector_def sndcart_sub[symmetric] norm_sndcart)
   2.123  
   2.124  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"
   2.125    by (simp add: dot_def setsum_UNIV_sum pastecart_def)
   2.126 @@ -3901,7 +3921,7 @@
   2.127  qed
   2.128  
   2.129  lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
   2.130 -  by (metis set_eq_subset span_mono span_span span_inc)
   2.131 +  by (metis set_eq_subset span_mono span_span span_inc) (* FIXME: slow *)
   2.132  
   2.133  (* ------------------------------------------------------------------------- *)
   2.134  (* Low-dimensional subset is in a hyperplane (weak orthogonal complement).   *)
     3.1 --- a/src/HOL/Library/Inner_Product.thy	Thu May 28 14:36:21 2009 -0700
     3.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu May 28 17:00:02 2009 -0700
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  subsection {* Real inner product spaces *}
     3.6  
     3.7 -class real_inner = real_vector + sgn_div_norm +
     3.8 +class real_inner = real_vector + sgn_div_norm + dist_norm +
     3.9    fixes inner :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    3.10    assumes inner_commute: "inner x y = inner y x"
    3.11    and inner_left_distrib: "inner (x + y) z = inner x z + inner y z"
     4.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 14:36:21 2009 -0700
     4.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 17:00:02 2009 -0700
     4.3 @@ -297,8 +297,8 @@
     4.4  
     4.5  lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
     4.6  lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
     4.7 -lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_def)
     4.8 -lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_def)
     4.9 +lemma mem_ball_0[simp]: "x \<in> ball 0 e \<longleftrightarrow> norm x < e" by (simp add: dist_norm)
    4.10 +lemma mem_cball_0[simp]: "x \<in> cball 0 e \<longleftrightarrow> norm x \<le> e" by (simp add: dist_norm)
    4.11  lemma centre_in_cball[simp]: "x \<in> cball x e \<longleftrightarrow> 0\<le> e"  by simp
    4.12  lemma ball_subset_cball[simp,intro]: "ball x e \<subseteq> cball x e" by (simp add: subset_eq)
    4.13  lemma subset_ball[intro]: "d <= e ==> ball x d \<subseteq> ball x e" by (simp add: subset_eq)
    4.14 @@ -555,13 +555,15 @@
    4.15  	apply (simp only: vector_component)
    4.16  	by (rule th') auto
    4.17        have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)$i\<bar>" using  component_le_norm[of "x'-x" i]
    4.18 -	apply (simp add: dist_def) by norm
    4.19 +	apply (simp add: dist_norm) by norm
    4.20        from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
    4.21    then show ?thesis unfolding closed_limpt islimpt_approachable
    4.22      unfolding not_le[symmetric] by blast
    4.23  qed
    4.24  
    4.25 -lemma finite_set_avoid: assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
    4.26 +lemma finite_set_avoid:
    4.27 +  fixes a :: "real ^ 'n::finite"
    4.28 +  assumes fS: "finite S" shows  "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d <= dist a x"
    4.29  proof(induct rule: finite_induct[OF fS])
    4.30    case 1 thus ?case apply auto by ferrack
    4.31  next
    4.32 @@ -602,7 +604,7 @@
    4.33      from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
    4.34      from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
    4.35      have th: "norm (z - y) < e" using z y
    4.36 -      unfolding dist_def [symmetric]
    4.37 +      unfolding dist_norm [symmetric]
    4.38        by (intro dist_triangle_lt [where z=x], simp)
    4.39      from d[rule_format, OF y(1) z(1) th] y z
    4.40      have False by (auto simp add: dist_commute)}
    4.41 @@ -1305,8 +1307,8 @@
    4.42      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
    4.43      { fix x
    4.44        have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
    4.45 -	using y(2) b unfolding dist_def	using linear_sub[of h "f x" l] `linear h`
    4.46 -	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! *)
    4.47 +	using y(2) b unfolding dist_norm using linear_sub[of h "f x" l] `linear h`
    4.48 +	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! *)
    4.49      }
    4.50      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
    4.51        by(rule_tac x="y" in exI) auto
    4.52 @@ -1325,7 +1327,7 @@
    4.53    done
    4.54  
    4.55  lemma Lim_neg: "(f ---> l) net ==> ((\<lambda>x. -(f x)) ---> -l) net"
    4.56 -  apply (simp add: Lim dist_def  group_simps)
    4.57 +  apply (simp add: Lim dist_norm  group_simps)
    4.58    apply (subst minus_diff_eq[symmetric])
    4.59    unfolding norm_minus_cancel by simp
    4.60  
    4.61 @@ -1362,9 +1364,9 @@
    4.62    unfolding diff_minus
    4.63    by (simp add: Lim_add Lim_neg)
    4.64  
    4.65 -lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_def)
    4.66 +lemma Lim_null: "(f ---> l) net \<longleftrightarrow> ((\<lambda>x. f(x) - l) ---> 0) net" by (simp add: Lim dist_norm)
    4.67  lemma Lim_null_norm: "(f ---> 0) net \<longleftrightarrow> ((\<lambda>x. vec1(norm(f x))) ---> 0) net"
    4.68 -  by (simp add: Lim dist_def norm_vec1)
    4.69 +  by (simp add: Lim dist_norm norm_vec1)
    4.70  
    4.71  lemma Lim_null_comparison:
    4.72    assumes "eventually (\<lambda>x. norm(f x) <= g x) net" "((\<lambda>x. vec1(g x)) ---> 0) net"
    4.73 @@ -1374,7 +1376,7 @@
    4.74    { fix x
    4.75      assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
    4.76      hence "dist (f x) 0 < e"  unfolding vec_def using dist_vec1[of "g x" "0"]
    4.77 -      by (vector dist_def norm_vec1 real_vector_norm_def dot_def vec1_def)
    4.78 +      by (vector dist_norm norm_vec1 real_vector_norm_def dot_def vec1_def)
    4.79    }
    4.80    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
    4.81      using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
    4.82 @@ -1384,7 +1386,7 @@
    4.83  
    4.84  lemma Lim_component: "(f ---> l) net
    4.85                        ==> ((\<lambda>a. vec1((f a :: real ^'n::finite)$i)) ---> vec1(l$i)) net"
    4.86 -  apply (simp add: Lim dist_def vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
    4.87 +  apply (simp add: Lim dist_norm vec1_sub[symmetric] norm_vec1  vector_minus_component[symmetric] del: vector_minus_component)
    4.88    apply (auto simp del: vector_minus_component)
    4.89    apply (erule_tac x=e in allE)
    4.90    apply clarify
    4.91 @@ -1475,7 +1477,7 @@
    4.92    { assume "norm (l - l') > 0"
    4.93      hence "norm (l - l') = 0" using *[of "(norm (l - l')) /2"] using norm_ge_zero[of "l - l'"] by simp
    4.94    }
    4.95 -  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
    4.96 +  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
    4.97    thus ?thesis using assms using Lim_sub[of f l net f l'] by simp
    4.98  qed
    4.99  
   4.100 @@ -1534,12 +1536,12 @@
   4.101  
   4.102      { fix x assume "dist (f x) l < d \<and> dist (g x) m < d"
   4.103        hence **:"norm (f x) * norm (g x - m) + norm (f x - l) * norm m < e / B"
   4.104 -	using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_def  by auto
   4.105 +	using d[THEN spec[where x="f x"], THEN spec[where x="g x"]] unfolding dist_norm  by auto
   4.106        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"
   4.107  	using B[THEN spec[where x="f x"], THEN spec[where x="g x - m"]]
   4.108  	using B[THEN spec[where x="f x - l"], THEN spec[where x="m"]] by auto
   4.109        also have "\<dots> < e" using ** and `B>0` by(auto simp add: field_simps)
   4.110 -      finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_def and * using norm_triangle_lt by auto
   4.111 +      finally have "dist (h (f x) (g x)) (h l m) < e" unfolding dist_norm and * using norm_triangle_lt by auto
   4.112      }
   4.113      moreover
   4.114      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)"
   4.115 @@ -1561,7 +1563,7 @@
   4.116      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
   4.117      { fix x::"real^'a" assume "0 < dist x 0 \<and> dist x 0 < d"
   4.118        hence "dist (f (a + x)) l < e" using d
   4.119 -      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
   4.120 +      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
   4.121      }
   4.122      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
   4.123    }
   4.124 @@ -1573,7 +1575,7 @@
   4.125        unfolding Lim_at by auto
   4.126      { fix x::"real^'a" assume "0 < dist x a \<and> dist x a < d"
   4.127        hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
   4.128 -	by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
   4.129 +	by(auto simp add: comm_monoid_add.mult_commute dist_norm dist_commute)
   4.130      }
   4.131      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
   4.132    }
   4.133 @@ -1730,7 +1732,7 @@
   4.134        using real_arch_inv[of e] apply auto apply(rule_tac x=n in exI)
   4.135        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))
   4.136    }
   4.137 -  thus ?thesis unfolding Lim_sequentially dist_def apply simp unfolding norm_vec1 by auto
   4.138 +  thus ?thesis unfolding Lim_sequentially dist_norm apply simp unfolding norm_vec1 by auto
   4.139  qed
   4.140  
   4.141  text{* More properties of closed balls. *}
   4.142 @@ -1739,9 +1741,9 @@
   4.143  proof-
   4.144    { fix xa::"nat\<Rightarrow>real^'a" and l assume as: "\<forall>n. dist x (xa n) \<le> e" "(xa ---> l) sequentially"
   4.145      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
   4.146 -    moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_def by auto
   4.147 +    moreover from as(1) have "eventually (\<lambda>n. norm (x - xa n) \<le> e) sequentially" unfolding eventually_sequentially dist_norm by auto
   4.148      ultimately have "dist x l \<le> e"
   4.149 -      unfolding dist_def
   4.150 +      unfolding dist_norm
   4.151        using Lim_norm_ubound[of sequentially _ "x - l" e] using trivial_limit_sequentially by auto
   4.152    }
   4.153    thus ?thesis unfolding closed_sequential_limits by auto
   4.154 @@ -1790,15 +1792,15 @@
   4.155  
   4.156  	have "dist x (y - (d / (2 * dist y x)) *s (y - x))
   4.157  	      = norm (x - y + (d / (2 * norm (y - x))) *s (y - x))"
   4.158 -	  unfolding mem_cball mem_ball dist_def diff_diff_eq2 diff_add_eq[THEN sym] by auto
   4.159 +	  unfolding mem_cball mem_ball dist_norm diff_diff_eq2 diff_add_eq[THEN sym] by auto
   4.160  	also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
   4.161  	  using vector_sadd_rdistrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
   4.162  	  unfolding vector_smult_lneg vector_smult_lid
   4.163 -	  by (auto simp add: dist_commute[unfolded dist_def] norm_mul)
   4.164 +	  by (auto simp add: norm_minus_commute)
   4.165  	also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
   4.166  	  unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
   4.167 -	  unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_def] by auto
   4.168 -	also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_def)
   4.169 +	  unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_norm] by auto
   4.170 +	also have "\<dots> \<le> e - d/2" using `d \<le> dist x y` and `d>0` and `?rhs` by(auto simp add: dist_norm)
   4.171  	finally have "y - (d / (2 * dist y x)) *s (y - x) \<in> ball x e" using `d>0` by auto
   4.172  
   4.173  	moreover
   4.174 @@ -1806,9 +1808,9 @@
   4.175  	have "(d / (2*dist y x)) *s (y - x) \<noteq> 0"
   4.176  	  using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding vector_mul_eq_0 by (auto simp add: dist_commute)
   4.177  	moreover
   4.178 -	have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_def apply simp unfolding norm_minus_cancel norm_mul
   4.179 +	have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_norm apply simp unfolding norm_minus_cancel norm_mul
   4.180  	  using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
   4.181 -	  unfolding dist_def by auto
   4.182 +	  unfolding dist_norm by auto
   4.183  	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
   4.184        qed
   4.185      next
   4.186 @@ -1858,7 +1860,7 @@
   4.187        thus "y \<in> ball x e" using `x = y ` by simp
   4.188      next
   4.189        case False
   4.190 -      have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_def
   4.191 +      have "dist (y + (d / 2 / dist y x) *s (y - x)) y < d" unfolding dist_norm
   4.192  	using `d>0` norm_ge_zero[of "y - x"] `x \<noteq> y` by auto
   4.193        hence *:"y + (d / 2 / dist y x) *s (y - x) \<in> cball x e" using d as(1)[unfolded subset_eq] by blast
   4.194        have "y - x \<noteq> 0" using `x \<noteq> y` by auto
   4.195 @@ -1866,11 +1868,11 @@
   4.196  	using `d>0` divide_pos_pos[of d "2*norm (y - x)"] by auto
   4.197  
   4.198        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)"
   4.199 -	by (auto simp add: dist_def vector_ssub_ldistrib add_diff_eq)
   4.200 +	by (auto simp add: dist_norm vector_ssub_ldistrib add_diff_eq)
   4.201        also have "\<dots> = norm ((1 + d / (2 * norm (y - x))) *s (y - x))"
   4.202  	by (auto simp add: vector_sadd_rdistrib vector_smult_lid ring_simps vector_sadd_rdistrib vector_ssub_ldistrib)
   4.203        also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)" using ** by auto
   4.204 -      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_def)
   4.205 +      also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_norm)
   4.206        finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
   4.207        thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
   4.208      qed  }
   4.209 @@ -2257,7 +2259,7 @@
   4.210  	  < (\<Sum>i \<in> ?d. e / real_of_nat (card ?d))"
   4.211  	  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
   4.212  	hence "(\<Sum>i \<in> ?d. \<bar>((f \<circ> r) n - l) $ i\<bar>) < e" unfolding setsum_constant by auto
   4.213 -	hence "dist ((f \<circ> r) n) l < e" unfolding dist_def using norm_le_l1[of "(f \<circ> r) n - l"] by auto  }
   4.214 +	hence "dist ((f \<circ> r) n) l < e" unfolding dist_norm using norm_le_l1[of "(f \<circ> r) n - l"] by auto  }
   4.215        hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> r) n) l < e" by auto  }
   4.216      hence *:"((f \<circ> r) ---> l) sequentially" unfolding Lim_sequentially by auto
   4.217      moreover have "l\<in>s"
   4.218 @@ -2316,8 +2318,8 @@
   4.219    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
   4.220    hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
   4.221    { fix n::nat assume "n\<ge>N"
   4.222 -    hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_def
   4.223 -      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)
   4.224 +    hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_norm
   4.225 +      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)
   4.226    }
   4.227    hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
   4.228    moreover
   4.229 @@ -2553,11 +2555,11 @@
   4.230      proof(cases "m<n")
   4.231        case True
   4.232        hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
   4.233 -      thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_def using norm_triangle_sub[of "x n" "x m"] by auto
   4.234 +      thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_norm using norm_triangle_sub[of "x n" "x m"] by auto
   4.235      next
   4.236        case False hence "n<m" using `m\<noteq>n` by auto
   4.237        hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
   4.238 -      thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_def using norm_triangle_sub[of "x m" "x n"] by auto
   4.239 +      thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_norm using norm_triangle_sub[of "x m" "x n"] by auto
   4.240      qed  } note ** = this
   4.241    { fix a b assume "x a = x b" "a \<noteq> b"
   4.242      hence False using **[of a b] by auto  }
   4.243 @@ -3128,13 +3130,13 @@
   4.244      { fix e::real assume "e>0"
   4.245        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"
   4.246  	using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
   4.247 -      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
   4.248 +      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
   4.249        { fix n assume "n\<ge>N"
   4.250  	hence "norm (f (x n) - f (y n) - 0) < e"
   4.251  	  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
   4.252 -	  unfolding dist_commute and dist_def by simp  }
   4.253 +	  unfolding dist_commute and dist_norm by simp  }
   4.254        hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e"  by auto  }
   4.255 -    hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_def by auto  }
   4.256 +    hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_norm by auto  }
   4.257    thus ?rhs by auto
   4.258  next
   4.259    assume ?rhs
   4.260 @@ -3147,7 +3149,7 @@
   4.261      def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
   4.262      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"
   4.263        unfolding x_def and y_def using fa by auto
   4.264 -    have *:"\<And>x y. dist (x - y) 0 = dist x y" unfolding dist_def by auto
   4.265 +    have *:"\<And>x (y::real^_). dist (x - y) 0 = dist x y" unfolding dist_norm by auto
   4.266      { fix e::real assume "e>0"
   4.267        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
   4.268        { fix n::nat assume "n\<ge>N"
   4.269 @@ -3517,7 +3519,7 @@
   4.270    have *:"f ` s \<subseteq> cball 0 b" using assms(2)[unfolded mem_cball_0[THEN sym]] by auto
   4.271    show ?thesis
   4.272      using image_closure_subset[OF assms(1) closed_cball[of 0 b] *] assms(3)
   4.273 -    unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_def)
   4.274 +    unfolding subset_eq apply(erule_tac x="f x" in ballE) by (auto simp add: dist_norm)
   4.275  qed
   4.276  
   4.277  text{* Making a continuous function avoid some value in a neighbourhood.         *}
   4.278 @@ -3580,10 +3582,10 @@
   4.279      have "e * abs c > 0" using assms(1)[unfolded zero_less_abs_iff[THEN sym]] using real_mult_order[OF `e>0`] by auto
   4.280      moreover
   4.281      { fix y assume "dist y (c *s x) < e * \<bar>c\<bar>"
   4.282 -      hence "norm ((1 / c) *s y - x) < e" unfolding dist_def
   4.283 +      hence "norm ((1 / c) *s y - x) < e" unfolding dist_norm
   4.284  	using norm_mul[of c "(1 / c) *s y - x", unfolded vector_ssub_ldistrib, unfolded vector_smult_assoc] assms(1)
   4.285  	  assms(1)[unfolded zero_less_abs_iff[THEN sym]] by (simp del:zero_less_abs_iff)
   4.286 -      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  }
   4.287 +      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  }
   4.288      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  }
   4.289    thus ?thesis unfolding open_def by auto
   4.290  qed
   4.291 @@ -3612,14 +3614,14 @@
   4.292  proof (rule set_ext, rule)
   4.293    fix x assume "x \<in> interior (op + a ` s)"
   4.294    then obtain e where "e>0" and e:"ball x e \<subseteq> op + a ` s" unfolding mem_interior by auto
   4.295 -  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
   4.296 +  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
   4.297    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
   4.298  next
   4.299    fix x assume "x \<in> op + a ` interior s"
   4.300    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
   4.301    { fix z have *:"a + y - z = y + a - z" by auto
   4.302      assume "z\<in>ball x e"
   4.303 -    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
   4.304 +    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
   4.305      hence "z \<in> op + a ` s" unfolding image_iff by(auto intro!: bexI[where x="z - a"])  }
   4.306    hence "ball x e \<subseteq> op + a ` s" unfolding subset_eq by auto
   4.307    thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
   4.308 @@ -3732,8 +3734,8 @@
   4.309      { fix y assume "y\<in>s" "dist y x < d"
   4.310        hence "dist (f n y) (f n x) < e / 3" using d[THEN bspec[where x=y]] by auto
   4.311        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"]
   4.312 -	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
   4.313 -      hence "dist (g y) (g x) < e" unfolding dist_def using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
   4.314 +	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
   4.315 +      hence "dist (g y) (g x) < e" unfolding dist_norm using n(1)[THEN bspec[where x=y], OF `y\<in>s`]
   4.316  	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)  }
   4.317      hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (g x') (g x) < e" using `d>0` by auto  }
   4.318    thus ?thesis unfolding continuous_on_def by auto
   4.319 @@ -3750,7 +3752,7 @@
   4.320        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
   4.321        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   }
   4.322      moreover have "e / B > 0" using `e>0` `B>0` divide_pos_pos by auto
   4.323 -    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  }
   4.324 +    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  }
   4.325    thus ?thesis unfolding Lim_at by auto
   4.326  qed
   4.327  
   4.328 @@ -3808,13 +3810,13 @@
   4.329  lemma continuous_at_vec1_range:
   4.330   "continuous (at x) (vec1 o f) \<longleftrightarrow> (\<forall>e>0. \<exists>d>0.
   4.331          \<forall>x'. norm(x' - x) < d --> abs(f x' - f x) < e)"
   4.332 -  unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_def apply auto
   4.333 +  unfolding continuous_at unfolding Lim_at apply simp unfolding dist_vec1 unfolding dist_nz[THEN sym] unfolding dist_norm apply auto
   4.334    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
   4.335    apply(erule_tac x=e in allE) by auto
   4.336  
   4.337  lemma continuous_on_vec1_range:
   4.338   " 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))"
   4.339 -  unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_def ..
   4.340 +  unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_norm ..
   4.341  
   4.342  lemma continuous_at_vec1_norm:
   4.343   "continuous (at x) (vec1 o norm)"
   4.344 @@ -3828,7 +3830,7 @@
   4.345    shows "continuous (at (a::real^'a::finite)) (\<lambda> x. vec1(x$i))"
   4.346  proof-
   4.347    { fix e::real and x assume "0 < dist x a" "dist x a < e" "e>0"
   4.348 -    hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_def by auto  }
   4.349 +    hence "\<bar>x $ i - a $ i\<bar> < e" using component_le_norm[of "x - a" i] unfolding dist_norm by auto  }
   4.350    thus ?thesis unfolding continuous_at tendsto_def eventually_at dist_vec1 by auto
   4.351  qed
   4.352  
   4.353 @@ -3837,12 +3839,12 @@
   4.354  proof-
   4.355    { fix e::real and x xa assume "x\<in>s" "e>0" "xa\<in>s" "0 < norm (xa - x) \<and> norm (xa - x) < e"
   4.356      hence "\<bar>xa $ i - x $ i\<bar> < e" using component_le_norm[of "xa - x" i] by auto  }
   4.357 -  thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_def by auto
   4.358 +  thus ?thesis unfolding continuous_on Lim_within dist_vec1 unfolding dist_norm by auto
   4.359  qed
   4.360  
   4.361  lemma continuous_at_vec1_infnorm:
   4.362   "continuous (at x) (vec1 o infnorm)"
   4.363 -  unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_def
   4.364 +  unfolding continuous_at Lim_at o_def unfolding dist_vec1 unfolding dist_norm
   4.365    apply auto apply (rule_tac x=e in exI) apply auto
   4.366    using order_trans[OF real_abs_sub_infnorm infnorm_le_norm, of _ x] by (metis xt1(7))
   4.367  
   4.368 @@ -3898,7 +3900,7 @@
   4.369      { fix x' assume "x'\<in>s" and as:"norm (x' - x) < e"
   4.370        hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
   4.371  	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
   4.372 -    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 }
   4.373 +    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 }
   4.374    thus ?thesis using assms
   4.375      using continuous_attains_sup[of s "\<lambda>x. dist a x"]
   4.376      unfolding continuous_on_vec1_range by (auto simp add: dist_commute)
   4.377 @@ -3920,7 +3922,7 @@
   4.378      { fix x' assume "x'\<in>?B" and as:"norm (x' - x) < e"
   4.379        hence "\<bar>norm (x' - a) - norm (x - a)\<bar> < e"
   4.380  	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
   4.381 -    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 }
   4.382 +    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 }
   4.383    hence "continuous_on (cball a (dist b a) \<inter> s) (vec1 \<circ> dist a)" unfolding continuous_on_vec1_range
   4.384      by (auto  simp add: dist_commute)
   4.385    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
   4.386 @@ -4120,7 +4122,7 @@
   4.387    have "{x - y | x y . x\<in>s \<and> y\<in>s} \<noteq> {}" using `s \<noteq> {}` by auto
   4.388    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"
   4.389      using compact_differences[OF assms(1) assms(1)]
   4.390 -    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)
   4.391 +    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)
   4.392    from x(1) obtain a b where "a\<in>s" "b\<in>s" "x = a - b" by auto
   4.393    thus ?thesis using x(2)[unfolded `x = a - b`] by blast
   4.394  qed
   4.395 @@ -4193,7 +4195,7 @@
   4.396        { fix e::real assume "e>0"
   4.397  	hence "0 < e *\<bar>c\<bar>"  using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
   4.398  	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
   4.399 -	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
   4.400 +	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
   4.401  	  using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto  }
   4.402        hence "((\<lambda>n. (1 / c) *s x n) ---> (1 / c) *s l) sequentially" unfolding Lim_sequentially by auto
   4.403        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"]]
   4.404 @@ -4301,7 +4303,7 @@
   4.405      hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
   4.406      hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
   4.407        by (auto  simp add: dist_commute)
   4.408 -    hence "d \<le> dist x y" unfolding dist_def by auto  }
   4.409 +    hence "d \<le> dist x y" unfolding dist_norm by auto  }
   4.410    thus ?thesis using `d>0` by auto
   4.411  qed
   4.412  
   4.413 @@ -4504,7 +4506,7 @@
   4.414      { fix x' assume as:"dist x' x < ?d"
   4.415        { fix i
   4.416  	have "\<bar>x'$i - x $ i\<bar> < d i"
   4.417 -	  using norm_bound_component_lt[OF as[unfolded dist_def], of i]
   4.418 +	  using norm_bound_component_lt[OF as[unfolded dist_norm], of i]
   4.419  	  unfolding vector_minus_component and Min_gr_iff[OF **] by auto
   4.420  	hence "a $ i < x' $ i" "x' $ i < b $ i" using d[THEN spec[where x=i]] by auto  }
   4.421        hence "a < x' \<and> x' < b" unfolding vector_less_def by auto  }
   4.422 @@ -4518,13 +4520,13 @@
   4.423    { 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"*)
   4.424      { assume xa:"a$i > x$i"
   4.425        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
   4.426 -      hence False unfolding mem_interval and dist_def
   4.427 +      hence False unfolding mem_interval and dist_norm
   4.428  	using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xa by(auto elim!: allE[where x=i])
   4.429      } hence "a$i \<le> x$i" by(rule ccontr)auto
   4.430      moreover
   4.431      { assume xb:"b$i < x$i"
   4.432        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
   4.433 -      hence False unfolding mem_interval and dist_def
   4.434 +      hence False unfolding mem_interval and dist_norm
   4.435  	using component_le_norm[of "y-x" i, unfolded vector_minus_component] and xb by(auto elim!: allE[where x=i])
   4.436      } hence "x$i \<le> b$i" by(rule ccontr)auto
   4.437      ultimately
   4.438 @@ -4543,7 +4545,7 @@
   4.439      { fix i
   4.440        have "dist (x - (e / 2) *s basis i) x < e"
   4.441  	   "dist (x + (e / 2) *s basis i) x < e"
   4.442 -	unfolding dist_def apply auto
   4.443 +	unfolding dist_norm apply auto
   4.444  	unfolding norm_minus_cancel and norm_mul using norm_basis[of i] and `e>0` by auto
   4.445        hence "a $ i \<le> (x - (e / 2) *s basis i) $ i"
   4.446                      "(x + (e / 2) *s basis i) $ i \<le> b $ i"
   4.447 @@ -4761,7 +4763,7 @@
   4.448      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"
   4.449      { assume "x$i > b$i"
   4.450        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
   4.451 -      hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto   }
   4.452 +      hence False using component_le_norm[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
   4.453      hence "x$i \<le> b$i" by(rule ccontr)auto  }
   4.454    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
   4.455  qed
   4.456 @@ -4773,7 +4775,7 @@
   4.457      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"
   4.458      { assume "a$i > x$i"
   4.459        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
   4.460 -      hence False using component_le_norm[of "y - x" i] unfolding dist_def and vector_minus_component by auto   }
   4.461 +      hence False using component_le_norm[of "y - x" i] unfolding dist_norm and vector_minus_component by auto   }
   4.462      hence "a$i \<le> x$i" by(rule ccontr)auto  }
   4.463    thus ?thesis unfolding closed_limpt unfolding islimpt_approachable by blast
   4.464  qed
   4.465 @@ -4810,7 +4812,7 @@
   4.466      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
   4.467        using divide_pos_pos[of e "norm a"] by auto
   4.468      { fix z assume "netord net z y" hence "dist l (f z) < e / norm a" using y by blast
   4.469 -      hence "norm a * norm (l - f z) < e" unfolding dist_def and
   4.470 +      hence "norm a * norm (l - f z) < e" unfolding dist_norm and
   4.471  	pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto
   4.472        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  }
   4.473      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  }
   4.474 @@ -4980,7 +4982,7 @@
   4.475    hence "\<forall>m n. m \<le> n \<longrightarrow> dest_vec1 (s m) \<le> dest_vec1 (s n)" by auto
   4.476    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
   4.477    thus ?thesis unfolding Lim_sequentially apply(rule_tac x="vec1 l" in exI)
   4.478 -    unfolding dist_def unfolding abs_dest_vec1 and dest_vec1_sub by auto
   4.479 +    unfolding dist_norm unfolding abs_dest_vec1 and dest_vec1_sub by auto
   4.480  qed
   4.481  
   4.482  subsection{* Basic homeomorphism definitions.                                          *}
   4.483 @@ -5119,7 +5121,7 @@
   4.484    show ?th unfolding homeomorphic_minimal
   4.485      apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
   4.486      apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
   4.487 -    apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
   4.488 +    apply (auto simp add: dist_commute) unfolding dist_norm and vector_smult_assoc using assms apply auto
   4.489      unfolding norm_minus_cancel and norm_mul
   4.490      using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
   4.491      apply (auto simp add: dist_commute)
   4.492 @@ -5131,7 +5133,7 @@
   4.493    show ?cth unfolding homeomorphic_minimal
   4.494      apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
   4.495      apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
   4.496 -    apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
   4.497 +    apply (auto simp add: dist_commute) unfolding dist_norm and vector_smult_assoc using assms apply auto
   4.498      unfolding norm_minus_cancel and norm_mul
   4.499      using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
   4.500      apply auto
   4.501 @@ -5148,7 +5150,7 @@
   4.502  proof-
   4.503    { fix d::real assume "d>0"
   4.504      then obtain N where N:"\<forall>n\<ge>N. norm (f (x n) - f (x N)) < e * d"
   4.505 -      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
   4.506 +      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
   4.507      { fix n assume "n\<ge>N"
   4.508        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
   4.509        moreover have "e * norm (x n - x N) \<le> norm (f (x n - x N))"
   4.510 @@ -5157,7 +5159,7 @@
   4.511        ultimately have "norm (x n - x N) < d" using `e>0`
   4.512  	using mult_left_less_imp_less[of e "norm (x n - x N)" d] by auto   }
   4.513      hence "\<exists>N. \<forall>n\<ge>N. norm (x n - x N) < d" by auto }
   4.514 -  thus ?thesis unfolding cauchy and dist_def by auto
   4.515 +  thus ?thesis unfolding cauchy and dist_norm by auto
   4.516  qed
   4.517  
   4.518  lemma complete_isometric_image:
   4.519 @@ -5178,7 +5180,10 @@
   4.520    thus ?thesis unfolding complete_def by auto
   4.521  qed
   4.522  
   4.523 -lemma dist_0_norm:"dist 0 x = norm x" unfolding dist_def by(auto simp add: norm_minus_cancel)
   4.524 +lemma dist_0_norm:
   4.525 +  fixes x :: "'a::real_normed_vector"
   4.526 +  shows "dist 0 x = norm x"
   4.527 +unfolding dist_norm by simp
   4.528  
   4.529  lemma injective_imp_isometric: fixes f::"real^'m::finite \<Rightarrow> real^'n::finite"
   4.530    assumes s:"closed s"  "subspace s"  and f:"linear f" "\<forall>x\<in>s. (f x = 0) \<longrightarrow> (x = 0)"
   4.531 @@ -5197,7 +5202,7 @@
   4.532    let ?S' = "{x::real^'m. x\<in>s \<and> norm x = norm a}"
   4.533    let ?S'' = "{x::real^'m. norm x = norm a}"
   4.534  
   4.535 -  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_def by (auto simp add: norm_minus_cancel)
   4.536 +  have "?S'' = frontier(cball 0 (norm a))" unfolding frontier_cball and dist_norm by (auto simp add: norm_minus_cancel)
   4.537    hence "compact ?S''" using compact_frontier[OF compact_cball, of 0 "norm a"] by auto
   4.538    moreover have "?S' = s \<inter> ?S''" by auto
   4.539    ultimately have "compact ?S'" using closed_inter_compact[of s ?S''] using s(1) by auto
   4.540 @@ -5652,9 +5657,9 @@
   4.541      unfolding o_def and h_def a_def b_def  by auto
   4.542  
   4.543    { fix n::nat
   4.544 -    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
   4.545 +    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
   4.546      { fix x y ::"real^'a"
   4.547 -      have "dist (-x) (-y) = dist x y" unfolding dist_def
   4.548 +      have "dist (-x) (-y) = dist x y" unfolding dist_norm
   4.549  	using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
   4.550  
   4.551      { assume as:"dist a b > dist (f n x) (f n y)"
     5.1 --- a/src/HOL/RealVector.thy	Thu May 28 14:36:21 2009 -0700
     5.2 +++ b/src/HOL/RealVector.thy	Thu May 28 17:00:02 2009 -0700
     5.3 @@ -416,6 +416,45 @@
     5.4    by (rule Reals_cases) auto
     5.5  
     5.6  
     5.7 +subsection {* Metric spaces *}
     5.8 +
     5.9 +class dist =
    5.10 +  fixes dist :: "'a \<Rightarrow> 'a \<Rightarrow> real"
    5.11 +
    5.12 +class metric_space = dist +
    5.13 +  assumes dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    5.14 +  assumes dist_triangle2: "dist x y \<le> dist x z + dist y z"
    5.15 +begin
    5.16 +
    5.17 +lemma dist_self [simp]: "dist x x = 0"
    5.18 +by simp
    5.19 +
    5.20 +lemma zero_le_dist [simp]: "0 \<le> dist x y"
    5.21 +using dist_triangle2 [of x x y] by simp
    5.22 +
    5.23 +lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
    5.24 +by (simp add: less_le)
    5.25 +
    5.26 +lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
    5.27 +by (simp add: not_less)
    5.28 +
    5.29 +lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
    5.30 +by (simp add: le_less)
    5.31 +
    5.32 +lemma dist_commute: "dist x y = dist y x"
    5.33 +proof (rule order_antisym)
    5.34 +  show "dist x y \<le> dist y x"
    5.35 +    using dist_triangle2 [of x y x] by simp
    5.36 +  show "dist y x \<le> dist x y"
    5.37 +    using dist_triangle2 [of y x y] by simp
    5.38 +qed
    5.39 +
    5.40 +lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
    5.41 +using dist_triangle2 [of x z y] by (simp add: dist_commute)
    5.42 +
    5.43 +end
    5.44 +
    5.45 +
    5.46  subsection {* Real normed vector spaces *}
    5.47  
    5.48  class norm =
    5.49 @@ -424,7 +463,10 @@
    5.50  class sgn_div_norm = scaleR + norm + sgn +
    5.51    assumes sgn_div_norm: "sgn x = x /\<^sub>R norm x"
    5.52  
    5.53 -class real_normed_vector = real_vector + sgn_div_norm +
    5.54 +class dist_norm = dist + norm + minus +
    5.55 +  assumes dist_norm: "dist x y = norm (x - y)"
    5.56 +
    5.57 +class real_normed_vector = real_vector + sgn_div_norm + dist_norm +
    5.58    assumes norm_ge_zero [simp]: "0 \<le> norm x"
    5.59    and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    5.60    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    5.61 @@ -458,8 +500,12 @@
    5.62  definition
    5.63    real_norm_def [simp]: "norm r = \<bar>r\<bar>"
    5.64  
    5.65 +definition
    5.66 +  dist_real_def: "dist x y = \<bar>x - y\<bar>"
    5.67 +
    5.68  instance
    5.69  apply (intro_classes, unfold real_norm_def real_scaleR_def)
    5.70 +apply (rule dist_real_def)
    5.71  apply (simp add: real_sgn_def)
    5.72  apply (rule abs_ge_zero)
    5.73  apply (rule abs_eq_0)
    5.74 @@ -637,43 +683,17 @@
    5.75    shows "norm (x ^ n) = norm x ^ n"
    5.76  by (induct n) (simp_all add: norm_mult)
    5.77  
    5.78 -
    5.79 -subsection {* Distance function *}
    5.80 -
    5.81 -(* TODO: There should be a metric_space class for this,
    5.82 -which should be a superclass of real_normed_vector. *)
    5.83 -
    5.84 -definition
    5.85 -  dist :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real"
    5.86 -where
    5.87 -  "dist x y = norm (x - y)"
    5.88 -
    5.89 -lemma zero_le_dist [simp]: "0 \<le> dist x y"
    5.90 -unfolding dist_def by (rule norm_ge_zero)
    5.91 -
    5.92 -lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    5.93 -unfolding dist_def by simp
    5.94 +text {* Every normed vector space is a metric space. *}
    5.95  
    5.96 -lemma dist_self [simp]: "dist x x = 0"
    5.97 -unfolding dist_def by simp
    5.98 -
    5.99 -lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
   5.100 -by (simp add: less_le)
   5.101 -
   5.102 -lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
   5.103 -by (simp add: not_less)
   5.104 -
   5.105 -lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
   5.106 -by (simp add: le_less)
   5.107 -
   5.108 -lemma dist_commute: "dist x y = dist y x"
   5.109 -unfolding dist_def by (rule norm_minus_commute)
   5.110 -
   5.111 -lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
   5.112 -unfolding dist_def
   5.113 -apply (rule ord_eq_le_trans [OF _ norm_triangle_ineq])
   5.114 -apply (simp add: diff_minus)
   5.115 -done
   5.116 +instance real_normed_vector < metric_space
   5.117 +proof
   5.118 +  fix x y :: 'a show "dist x y = 0 \<longleftrightarrow> x = y"
   5.119 +    unfolding dist_norm by simp
   5.120 +next
   5.121 +  fix x y z :: 'a show "dist x y \<le> dist x z + dist y z"
   5.122 +    unfolding dist_norm
   5.123 +    using norm_triangle_ineq4 [of "x - z" "y - z"] by simp
   5.124 +qed
   5.125  
   5.126  
   5.127  subsection {* Sign function *}