generalize dist function to class real_normed_vector
authorhuffman
Thu May 28 13:41:41 2009 -0700 (2009-05-28)
changeset 312850a3f9ee4117c
parent 31280 8ef7ba78bf26
child 31286 424874813840
generalize dist function to class real_normed_vector
src/HOL/Library/Convex_Euclidean_Space.thy
src/HOL/Library/Euclidean_Space.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 15:54:20 2009 +0200
     1.2 +++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
     1.3 @@ -609,7 +609,7 @@
     1.4  	apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this
     1.5  
     1.6      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.7 -      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_sym)+
     1.8 +      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
     1.9        using * apply(simp add: dist_def)
    1.10        using as(1,2)[unfolded open_def] apply simp
    1.11        using as(1,2)[unfolded open_def] apply simp
    1.12 @@ -1357,7 +1357,9 @@
    1.13  
    1.14  subsection {* Extremal points of a simplex are some vertices. *}
    1.15  
    1.16 -lemma dist_increases_online: assumes "d \<noteq> 0"
    1.17 +lemma dist_increases_online:
    1.18 +  fixes a b d :: "real ^ 'n::finite"
    1.19 +  assumes "d \<noteq> 0"
    1.20    shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
    1.21  proof(cases "a \<bullet> d - b \<bullet> d > 0")
    1.22    case True hence "0 < d \<bullet> d + (a \<bullet> d * 2 - b \<bullet> d * 2)" 
    1.23 @@ -1409,7 +1411,7 @@
    1.24   	proof(erule_tac disjE)
    1.25  	  assume "dist a y < dist a (y + w *s (x - b))"
    1.26  	  hence "norm (y - a) < norm ((u + w) *s x + (v - w) *s b - a)"
    1.27 -	    unfolding dist_sym[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
    1.28 +	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
    1.29  	  moreover have "(u + w) *s x + (v - w) *s b \<in> convex hull insert x s"
    1.30  	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
    1.31  	    apply(rule_tac x="u + w" in exI) apply rule defer 
    1.32 @@ -1418,7 +1420,7 @@
    1.33  	next
    1.34  	  assume "dist a y < dist a (y - w *s (x - b))"
    1.35  	  hence "norm (y - a) < norm ((u - w) *s x + (v + w) *s b - a)"
    1.36 -	    unfolding dist_sym[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
    1.37 +	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
    1.38  	  moreover have "(u - w) *s x + (v + w) *s b \<in> convex hull insert x s"
    1.39  	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
    1.40  	    apply(rule_tac x="u - w" in exI) apply rule defer 
    1.41 @@ -1437,7 +1439,7 @@
    1.42    have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
    1.43    then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
    1.44      using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
    1.45 -    unfolding dist_sym[of a] unfolding dist_def by auto
    1.46 +    unfolding dist_commute[of a] unfolding dist_def by auto
    1.47    thus ?thesis proof(cases "x\<in>s")
    1.48      case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
    1.49        using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
    1.50 @@ -1513,6 +1515,7 @@
    1.51    qed(rule divide_pos_pos, auto) qed
    1.52  
    1.53  lemma closer_point_lemma:
    1.54 +  fixes x y z :: "real ^ 'n::finite"
    1.55    assumes "(y - x) \<bullet> (z - x) > 0"
    1.56    shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *s (z - x)) y < dist x y"
    1.57  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.58 @@ -1526,7 +1529,7 @@
    1.59  proof(rule ccontr) assume "\<not> (a - x) \<bullet> (y - x) \<le> 0"
    1.60    then obtain u where u:"u>0" "u\<le>1" "dist (x + u *s (y - x)) a < dist x a" using closer_point_lemma[of a x y] by auto
    1.61    let ?z = "(1 - u) *s x + u *s y" have "?z \<in> s" using mem_convex[OF assms(1,3,4), of u] using u by auto
    1.62 -  thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_sym field_simps) qed
    1.63 +  thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_commute field_simps) qed
    1.64  
    1.65  lemma any_closest_point_unique:
    1.66    assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
    1.67 @@ -1592,7 +1595,7 @@
    1.68        using assms(1)[unfolded convex_alt] and y and `x\<in>s` and `y\<in>s` by auto
    1.69      assume "\<not> (y - z) \<bullet> y \<le> (y - z) \<bullet> x" then obtain v where
    1.70        "v>0" "v\<le>1" "dist (y + v *s (x - y)) z < dist y z" using closer_point_lemma[of z y x] by auto
    1.71 -    thus False using *[THEN spec[where x=v]] by(auto simp add: dist_sym field_simps)
    1.72 +    thus False using *[THEN spec[where x=v]] by(auto simp add: dist_commute field_simps)
    1.73    qed auto
    1.74  qed
    1.75  
    1.76 @@ -1613,7 +1616,7 @@
    1.77        then obtain u where "u>0" "u\<le>1" "dist (y + u *s (x - y)) z < dist y z" by auto
    1.78        thus False using y[THEN bspec[where x="y + u *s (x - y)"]]
    1.79  	using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
    1.80 -	using `x\<in>s` `y\<in>s` by (auto simp add: dist_sym field_simps) qed
    1.81 +	using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute field_simps) qed
    1.82      moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
    1.83      hence "0 < (y - z) \<bullet> (y - z)" unfolding norm_pow_2 by simp
    1.84      ultimately show "(y - z) \<bullet> z + (norm (y - z))\<twosuperior> / 2 < (y - z) \<bullet> x"
    1.85 @@ -2092,7 +2095,7 @@
    1.86      unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
    1.87      fix y assume "dist (u *s x) y < 1 - u"
    1.88      hence "inverse (1 - u) *s (y - u *s x) \<in> s"
    1.89 -      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_sym dist_def
    1.90 +      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_def
    1.91        unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_mul      
    1.92        apply (rule mult_left_le_imp_le[of "1 - u"])
    1.93        unfolding class_semiring.mul_a using `u<1` by auto
    1.94 @@ -2420,8 +2423,8 @@
    1.95    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.96      using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by(auto simp add:field_simps)
    1.97  next case False fix y assume "y\<in>cball x e" 
    1.98 -  hence "dist x y < 0" using False unfolding mem_cball not_le by auto
    1.99 -  thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using dist_pos_le[of x y] by auto qed
   1.100 +  hence "dist x y < 0" using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
   1.101 +  thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using zero_le_dist[of x y] by auto qed
   1.102  
   1.103  subsection {* Hence a convex function on an open set is continuous. *}
   1.104  
   1.105 @@ -2498,7 +2501,7 @@
   1.106  lemma midpoint_eq_endpoint:
   1.107    "midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
   1.108    "midpoint a b = b \<longleftrightarrow> a = b"
   1.109 -  unfolding dist_eq_0[THEN sym] dist_midpoint by auto
   1.110 +  unfolding dist_eq_0_iff[where 'a="real^'n", THEN sym] dist_midpoint by auto
   1.111  
   1.112  lemma convex_contains_segment:
   1.113    "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
   1.114 @@ -2544,7 +2547,7 @@
   1.115  lemma between:"between (a,b) (x::real^'n::finite) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
   1.116  proof(cases "a = b")
   1.117    case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
   1.118 -    by(auto simp add:segment_refl dist_sym) next
   1.119 +    by(auto simp add:segment_refl dist_commute) next
   1.120    case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto 
   1.121    have *:"\<And>u. a - ((1 - u) *s a + u *s b) = u *s (a - b)" by auto
   1.122    show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq
     2.1 --- a/src/HOL/Library/Euclidean_Space.thy	Thu May 28 15:54:20 2009 +0200
     2.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
     2.3 @@ -620,12 +620,6 @@
     2.4  lemma norm_real: "norm(x::real ^ 1) = abs(x$1)"
     2.5    by (simp add: norm_vector_1)
     2.6  
     2.7 -text{* Metric *}
     2.8 -
     2.9 -text {* FIXME: generalize to arbitrary @{text real_normed_vector} types *}
    2.10 -definition dist:: "real ^ 'n::finite \<Rightarrow> real ^ 'n \<Rightarrow> real" where
    2.11 -  "dist x y = norm (x - y)"
    2.12 -
    2.13  lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))"
    2.14    by (auto simp add: norm_real dist_def)
    2.15  
    2.16 @@ -959,38 +953,38 @@
    2.17  
    2.18  text{* Hence more metric properties. *}
    2.19  
    2.20 -lemma dist_refl[simp]: "dist x x = 0" by norm
    2.21 -
    2.22 -lemma dist_sym: "dist x y = dist y x"by norm
    2.23 -
    2.24 -lemma dist_pos_le[simp]: "0 <= dist x y" by norm
    2.25 -
    2.26 -lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm
    2.27 -
    2.28 -lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm
    2.29 -
    2.30 -lemma dist_eq_0[simp]: "dist x y = 0 \<longleftrightarrow> x = y" by norm
    2.31 -
    2.32 -lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by norm
    2.33 -lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by norm
    2.34 -
    2.35 -lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e" by norm
    2.36 -
    2.37 -lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e" by norm
    2.38 -
    2.39 -lemma dist_triangle_half_l: "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 ==> dist x1 x2 < e" by norm
    2.40 -
    2.41 -lemma dist_triangle_half_r: "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 ==> dist x1 x2 < e" by norm
    2.42 +lemma dist_triangle_alt: "dist y z <= dist x y + dist x z"
    2.43 +using dist_triangle [of y z x] by (simp add: dist_commute)
    2.44 +
    2.45 +lemma dist_triangle2: "dist x y \<le> dist x z + dist y z"
    2.46 +using dist_triangle [of x y z] by (simp add: dist_commute)
    2.47 +
    2.48 +lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by (simp add: zero_less_dist_iff)
    2.49 +lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by (simp add: zero_less_dist_iff)
    2.50 +
    2.51 +lemma dist_triangle_le: "dist x z + dist y z <= e \<Longrightarrow> dist x y <= e"
    2.52 +by (rule order_trans [OF dist_triangle2])
    2.53 +
    2.54 +lemma dist_triangle_lt: "dist x z + dist y z < e ==> dist x y < e"
    2.55 +by (rule le_less_trans [OF dist_triangle2])
    2.56 +
    2.57 +lemma dist_triangle_half_l:
    2.58 +  "dist x1 y < e / 2 \<Longrightarrow> dist x2 y < e / 2 \<Longrightarrow> dist x1 x2 < e"
    2.59 +by (rule dist_triangle_lt [where z=y], simp)
    2.60 +
    2.61 +lemma dist_triangle_half_r:
    2.62 +  "dist y x1 < e / 2 \<Longrightarrow> dist y x2 < e / 2 \<Longrightarrow> dist x1 x2 < e"
    2.63 +by (rule dist_triangle_half_l, simp_all add: dist_commute)
    2.64  
    2.65  lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'"
    2.66 -  by norm
    2.67 +unfolding dist_def by (rule norm_diff_triangle_ineq)
    2.68  
    2.69  lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y"
    2.70    unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul ..
    2.71  
    2.72 -lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm
    2.73 -
    2.74 -lemma dist_le_0[simp]: "dist x y <= 0 \<longleftrightarrow> x = y" by norm
    2.75 +lemma dist_triangle_add_half:
    2.76 +  " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 \<Longrightarrow> dist(x + y) (x' + y') < e"
    2.77 +by (rule le_less_trans [OF dist_triangle_add], simp)
    2.78  
    2.79  lemma setsum_component [simp]:
    2.80    fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n"
     3.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 15:54:20 2009 +0200
     3.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
     3.3 @@ -194,7 +194,9 @@
     3.4    by (simp add: subtopology_superset)
     3.5  
     3.6  subsection{* The universal Euclidean versions are what we use most of the time *}
     3.7 -definition "open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
     3.8 +definition
     3.9 +  "open" :: "(real ^ 'n::finite) set \<Rightarrow> bool" where
    3.10 +  "open S \<longleftrightarrow> (\<forall>x \<in> S. \<exists>e >0. \<forall>x'. dist x' x < e \<longrightarrow> x' \<in> S)"
    3.11  definition "closed S \<longleftrightarrow> open(UNIV - S)"
    3.12  definition "euclidean = topology open"
    3.13  
    3.14 @@ -285,8 +287,13 @@
    3.15  
    3.16  subsection{* Open and closed balls. *}
    3.17  
    3.18 -definition "ball x e = {y. dist x y < e}"
    3.19 -definition "cball x e = {y. dist x y \<le> e}"
    3.20 +definition
    3.21 +  ball :: "real ^ 'n::finite \<Rightarrow> real \<Rightarrow> (real^'n) set" where
    3.22 +  "ball x e = {y. dist x y < e}"
    3.23 +
    3.24 +definition
    3.25 +  cball :: "real ^ 'n::finite \<Rightarrow> real \<Rightarrow> (real^'n) set" where
    3.26 +  "cball x e = {y. dist x y \<le> e}"
    3.27  
    3.28  lemma mem_ball[simp]: "y \<in> ball x e \<longleftrightarrow> dist x y < e" by (simp add: ball_def)
    3.29  lemma mem_cball[simp]: "y \<in> cball x e \<longleftrightarrow> dist x y \<le> e" by (simp add: cball_def)
    3.30 @@ -312,7 +319,7 @@
    3.31  
    3.32  lemma open_ball[intro, simp]: "open (ball x e)"
    3.33    unfolding open_def ball_def Collect_def Ball_def mem_def
    3.34 -  unfolding dist_sym
    3.35 +  unfolding dist_commute
    3.36    apply clarify
    3.37    apply (rule_tac x="e - dist xa x" in exI)
    3.38    using dist_triangle_alt[where z=x]
    3.39 @@ -322,9 +329,9 @@
    3.40    apply (erule_tac x="xa" in allE)
    3.41    by arith
    3.42  
    3.43 -lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_refl)
    3.44 +lemma centre_in_ball[simp]: "x \<in> ball x e \<longleftrightarrow> e > 0" by (metis mem_ball dist_self)
    3.45  lemma open_contains_ball: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. ball x e \<subseteq> S)"
    3.46 -  unfolding open_def subset_eq mem_ball Ball_def dist_sym ..
    3.47 +  unfolding open_def subset_eq mem_ball Ball_def dist_commute ..
    3.48  
    3.49  lemma open_contains_ball_eq: "open S \<Longrightarrow> \<forall>x. x\<in>S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
    3.50    by (metis open_contains_ball subset_eq centre_in_ball)
    3.51 @@ -332,7 +339,7 @@
    3.52  lemma ball_eq_empty[simp]: "ball x e = {} \<longleftrightarrow> e \<le> 0"
    3.53    unfolding mem_ball expand_set_eq
    3.54    apply (simp add: not_less)
    3.55 -  by (metis dist_pos_le order_trans dist_refl)
    3.56 +  by (metis zero_le_dist order_trans dist_self)
    3.57  
    3.58  lemma ball_empty[intro]: "e \<le> 0 ==> ball x e = {}" by simp
    3.59  
    3.60 @@ -380,14 +387,14 @@
    3.61      { fix x assume "x\<in>S"
    3.62        hence "x \<in> \<Union>{B. \<exists>x\<in>S. B = ball x (d x)}"
    3.63  	apply simp apply(rule_tac x="ball x(d x)" in exI) apply auto
    3.64 -	unfolding dist_refl using d[of x] by auto
    3.65 +        by (rule d [THEN conjunct1])
    3.66        hence "x\<in> ?T \<inter> U" using SU and `x\<in>S` by auto  }
    3.67      moreover
    3.68      { fix y assume "y\<in>?T"
    3.69        then obtain B where "y\<in>B" "B\<in>{B. \<exists>x\<in>S. B = ball x (d x)}" by auto
    3.70        then obtain x where "x\<in>S" and x:"y \<in> ball x (d x)" by auto
    3.71        assume "y\<in>U"
    3.72 -      hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_sym) }
    3.73 +      hence "y\<in>S" using d[OF `x\<in>S`] and x by(auto simp add: dist_commute) }
    3.74      ultimately have "S = ?T \<inter> U" by blast
    3.75      with oT have ?lhs unfolding openin_subtopology open_openin[symmetric] by blast}
    3.76    ultimately show ?thesis by blast
    3.77 @@ -472,8 +479,8 @@
    3.78    let ?V = "ball y (dist x y / 2)"
    3.79    have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
    3.80                 ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
    3.81 -  have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym]
    3.82 -    by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1)
    3.83 +  have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_commute]
    3.84 +    by (auto simp add: expand_set_eq less_divide_eq_number_of1)
    3.85    then show ?thesis by blast
    3.86  qed
    3.87  
    3.88 @@ -500,14 +507,17 @@
    3.89    unfolding islimpt_def
    3.90    apply auto
    3.91    apply(erule_tac x="ball x e" in allE)
    3.92 -  apply (auto simp add: dist_refl)
    3.93 -  apply(rule_tac x=y in bexI) apply (auto simp add: dist_sym)
    3.94 -  by (metis open_def dist_sym open_ball centre_in_ball mem_ball)
    3.95 +  apply auto
    3.96 +  apply(rule_tac x=y in bexI)
    3.97 +  apply (auto simp add: dist_commute)
    3.98 +  apply (simp add: open_def, drule (1) bspec)
    3.99 +  apply (clarify, drule spec, drule (1) mp, auto)
   3.100 +  done
   3.101  
   3.102  lemma islimpt_approachable_le: "x islimpt S \<longleftrightarrow> (\<forall>e>0. \<exists>x'\<in> S. x' \<noteq> x \<and> dist x' x <= e)"
   3.103    unfolding islimpt_approachable
   3.104    using approachable_lt_le[where f="\<lambda>x'. dist x' x" and P="\<lambda>x'. \<not> (x'\<in>S \<and> x'\<noteq>x)"]
   3.105 -  by metis
   3.106 +  by metis (* FIXME: VERY slow! *)
   3.107  
   3.108  lemma islimpt_UNIV[simp, intro]: "(x:: real ^'n::finite) islimpt UNIV"
   3.109  proof-
   3.110 @@ -546,7 +556,7 @@
   3.111  	by (rule th') auto
   3.112        have th2: "\<bar>dist x x'\<bar> \<ge> \<bar>(x' - x)$i\<bar>" using  component_le_norm[of "x'-x" i]
   3.113  	apply (simp add: dist_def) by norm
   3.114 -      from th[OF th1 th2] x'(3) have False by (simp add: dist_sym dist_pos_le) }
   3.115 +      from th[OF th1 th2] x'(3) have False by (simp add: dist_commute) }
   3.116    then show ?thesis unfolding closed_limpt islimpt_approachable
   3.117      unfolding not_le[symmetric] by blast
   3.118  qed
   3.119 @@ -569,7 +579,7 @@
   3.120  
   3.121  lemma islimpt_finite: assumes fS: "finite S" shows "\<not> a islimpt S"
   3.122    unfolding islimpt_approachable
   3.123 -  using finite_set_avoid[OF fS, of a] by (metis dist_sym  not_le)
   3.124 +  using finite_set_avoid[OF fS, of a] by (metis dist_commute  not_le)
   3.125  
   3.126  lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
   3.127    apply (rule iffI)
   3.128 @@ -591,9 +601,11 @@
   3.129      let ?m = "min (e/2) (dist x y) "
   3.130      from e2 y(2) have mp: "?m > 0" by (simp add: dist_nz[THEN sym])
   3.131      from C[rule_format, OF mp] obtain z where z: "z \<in> S" "z\<noteq>x" "dist z x < ?m" by blast
   3.132 -    have th: "norm (z - y) < e" using z y by norm
   3.133 +    have th: "norm (z - y) < e" using z y
   3.134 +      unfolding dist_def [symmetric]
   3.135 +      by (intro dist_triangle_lt [where z=x], simp)
   3.136      from d[rule_format, OF y(1) z(1) th] y z
   3.137 -    have False by (auto simp add: dist_sym)}
   3.138 +    have False by (auto simp add: dist_commute)}
   3.139    then show ?thesis by (metis islimpt_approachable closed_limpt)
   3.140  qed
   3.141  
   3.142 @@ -642,7 +654,7 @@
   3.143      have th: "dist x y < e" "dist x y < d" unfolding y using e(1) d(1) by arith+
   3.144      have "\<exists>x'\<in>S. x'\<noteq> x \<and> dist x' x < d"
   3.145        apply (rule bexI[where x=y])
   3.146 -      using e th y by (auto simp add: dist_sym)}
   3.147 +      using e th y by (auto simp add: dist_commute)}
   3.148    then show ?thesis unfolding islimpt_approachable by blast
   3.149  qed
   3.150  
   3.151 @@ -657,17 +669,16 @@
   3.152      {fix y assume y: "y \<in> ball x e"
   3.153        {fix d::real assume d: "d > 0"
   3.154  	let ?k = "min d (e - dist x y)"
   3.155 -	have kp: "?k > 0" using d e(1) y[unfolded mem_ball] by norm
   3.156 +	have kp: "?k > 0" using d e(1) y[unfolded mem_ball] by simp
   3.157  	have "?k/2 \<ge> 0" using kp by simp
   3.158  	then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist)
   3.159  	from iT[unfolded expand_set_eq mem_interior]
   3.160  	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: less_divide_eq_number_of1)
   3.161  	then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq)
   3.162  	have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp
   3.163 -	  using w e(1) d apply (auto simp only: dist_sym)
   3.164 +	  using w e(1) d apply (auto simp only: dist_commute)
   3.165  	  apply (auto simp add: min_def cong del: if_weak_cong)
   3.166  	  apply (cases "d \<le> e - dist x y", auto simp add: ring_simps cong del: if_weak_cong)
   3.167 -	  apply norm
   3.168  	  apply (cases "d \<le> e - dist x y", auto simp add: ring_simps not_le not_less cong del: if_weak_cong)
   3.169  	  apply norm
   3.170  	  apply norm
   3.171 @@ -877,9 +888,9 @@
   3.172      assume "e > 0"
   3.173      let ?rhse = "(\<exists>x\<in>S. dist a x < e) \<and> (\<exists>x. x \<notin> S \<and> dist a x < e)"
   3.174      { assume "a\<in>S"
   3.175 -      have "\<exists>x\<in>S. dist a x < e" using dist_refl[of a] `e>0` `a\<in>S` by(rule_tac x=a in bexI) auto
   3.176 +      have "\<exists>x\<in>S. dist a x < e" using `e>0` `a\<in>S` by(rule_tac x=a in bexI) auto
   3.177        moreover have "\<exists>x. x \<notin> S \<and> dist a x < e" using `?lhs` `a\<in>S`
   3.178 -	unfolding frontier_closures closure_def islimpt_def using dist_refl[of a] `e>0`
   3.179 +	unfolding frontier_closures closure_def islimpt_def using `e>0`
   3.180  	by (auto, erule_tac x="ball a e" in allE, auto)
   3.181        ultimately have ?rhse by auto
   3.182      }
   3.183 @@ -887,8 +898,8 @@
   3.184      { assume "a\<notin>S"
   3.185        hence ?rhse using `?lhs`
   3.186  	unfolding frontier_closures closure_def islimpt_def
   3.187 -	using open_ball[of a e] dist_refl[of a] `e > 0`
   3.188 -	by (auto, erule_tac x = "ball a e" in allE, auto)
   3.189 +	using open_ball[of a e] `e > 0`
   3.190 +	by (auto, erule_tac x = "ball a e" in allE, auto) (* FIXME: VERY slow! *)
   3.191      }
   3.192      ultimately have ?rhse by auto
   3.193    }
   3.194 @@ -957,7 +968,10 @@
   3.195  
   3.196  subsection{* Common nets and The "within" modifier for nets. *}
   3.197  
   3.198 -definition "at a = mknet(\<lambda>x y. 0 < dist x a \<and> dist x a <= dist y a)"
   3.199 +definition
   3.200 +  at :: "real ^ 'n::finite \<Rightarrow> (real ^ 'n) net" where
   3.201 +  "at a = mknet(\<lambda>x y. 0 < dist x a \<and> dist x a <= dist y a)"
   3.202 +
   3.203  definition "at_infinity = mknet(\<lambda>x y. norm x \<ge> norm y)"
   3.204  definition "sequentially = mknet(\<lambda>(m::nat) n. m >= n)"
   3.205  
   3.206 @@ -982,7 +996,7 @@
   3.207  
   3.208  lemma at: "\<And>x y. netord (at a) x y \<longleftrightarrow> 0 < dist x a \<and> dist x a <= dist y a"
   3.209    apply (net at_def)
   3.210 -  by (metis dist_sym real_le_linear real_le_trans)
   3.211 +  by (metis dist_commute real_le_linear real_le_trans)
   3.212  
   3.213  lemma at_infinity:
   3.214   "\<And>x y. netord at_infinity x y \<longleftrightarrow> norm x >= norm y"
   3.215 @@ -1029,7 +1043,8 @@
   3.216      then have "\<not> a islimpt S"
   3.217        using bc
   3.218        unfolding within at dist_nz islimpt_approachable_le
   3.219 -      by(auto simp add: dist_triangle dist_sym dist_eq_0[THEN sym]) }
   3.220 +      by (auto simp add: dist_triangle dist_commute dist_eq_0_iff [symmetric]
   3.221 +               simp del: dist_eq_0_iff) }
   3.222    moreover
   3.223    {assume "\<not> a islimpt S"
   3.224      then obtain e where e: "e > 0" "\<forall>x' \<in> S. x' \<noteq> a \<longrightarrow> dist x' a > e"
   3.225 @@ -1038,7 +1053,7 @@
   3.226      from b e(1) have "a \<noteq> b" by (simp add: dist_nz)
   3.227      moreover have "\<forall>x. \<not> ((0 < dist x a \<and> dist x a \<le> dist a a) \<and> x \<in> S) \<and>
   3.228                   \<not> ((0 < dist x a \<and> dist x a \<le> dist b a) \<and> x \<in> S)"
   3.229 -      using e(2) b by (auto simp add: dist_refl dist_sym)
   3.230 +      using e(2) b by (auto simp add: dist_commute)
   3.231      ultimately have "trivial_limit (at a within S)"  unfolding trivial_limit_def within at
   3.232        by blast}
   3.233    ultimately show ?thesis unfolding trivial_limit_def by blast
   3.234 @@ -1091,7 +1106,7 @@
   3.235      hence "\<forall>x\<in>S. 0 < dist x a \<and> dist x a \<le> (d/2) \<longrightarrow> P x" using order_less_imp_le by auto
   3.236    }
   3.237    thus ?thesis unfolding eventually_within_le using approachable_lt_le
   3.238 -    by (auto, rule_tac x="d/2" in exI, auto)
   3.239 +    apply auto  by (rule_tac x="d/2" in exI, auto)
   3.240  qed
   3.241  
   3.242  lemma eventually_at: "eventually P (at a) \<longleftrightarrow> (\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> P x)"
   3.243 @@ -1185,11 +1200,11 @@
   3.244    by (auto simp add: tendsto_def eventually_sequentially)
   3.245  
   3.246  lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f ---> l) net"
   3.247 -  by (auto simp add: eventually_def Lim dist_refl)
   3.248 +  by (auto simp add: eventually_def Lim)
   3.249  
   3.250  text{* The expected monotonicity property. *}
   3.251  
   3.252 -lemma Lim_within_empty:  "(f ---> l) (at x within {})"
   3.253 +lemma Lim_within_empty: "(f ---> l) (at x within {})"
   3.254    by (simp add: Lim_within_le)
   3.255  
   3.256  lemma Lim_within_subset: "(f ---> l) (at a within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (at a within T)"
   3.257 @@ -1291,7 +1306,7 @@
   3.258      { fix x
   3.259        have "netord net x y \<longrightarrow> dist (h (f x)) (h l) < e"
   3.260  	using y(2) b unfolding dist_def	using linear_sub[of h "f x" l] `linear h`
   3.261 -	apply auto by (metis b(1) b(2) dist_def dist_sym less_le_not_le linorder_not_le mult_imp_div_pos_le real_mult_commute xt1(7))
   3.262 +	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! *)
   3.263      }
   3.264      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
   3.265        by(rule_tac x="y" in exI) auto
   3.266 @@ -1300,7 +1315,7 @@
   3.267  qed
   3.268  
   3.269  lemma Lim_const: "((\<lambda>x. a) ---> a) net"
   3.270 -  by (auto simp add: Lim dist_refl trivial_limit_def)
   3.271 +  by (auto simp add: Lim trivial_limit_def)
   3.272  
   3.273  lemma Lim_cmul: "(f ---> l) net ==> ((\<lambda>x. c *s f x) ---> c *s l) net"
   3.274    apply (rule Lim_linear[where f = f])
   3.275 @@ -1359,7 +1374,7 @@
   3.276    { fix x
   3.277      assume "norm (f x) \<le> g x" "dist (vec1 (g x)) 0 < e"
   3.278      hence "dist (f x) 0 < e"  unfolding vec_def using dist_vec1[of "g x" "0"]
   3.279 -      by (vector dist_def norm_vec1 dist_refl real_vector_norm_def dot_def vec1_def)
   3.280 +      by (vector dist_def norm_vec1 real_vector_norm_def dot_def vec1_def)
   3.281    }
   3.282    thus "eventually (\<lambda>x. dist (f x) 0 < e) net"
   3.283      using eventually_and[of "\<lambda>x. norm(f x) <= g x" "\<lambda>x. dist (vec1 (g x)) 0 < e" net]
   3.284 @@ -1404,7 +1419,7 @@
   3.285      hence *:"\<forall>x. dist l x < e \<longrightarrow> x \<notin> S" by auto
   3.286      obtain y where "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> dist (f x) l < e)"
   3.287        using assms(3,4) `e>0` unfolding tendsto_def eventually_def by blast
   3.288 -    hence "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> f x \<notin> S)"  using * by (auto simp add: dist_sym)
   3.289 +    hence "(\<exists>x. netord net x y) \<and> (\<forall>x. netord net x y \<longrightarrow> f x \<notin> S)"  using * by (auto simp add: dist_commute)
   3.290      hence False using assms(2,3)
   3.291        using eventually_and[of "(\<lambda>x. f x \<in> S)" "(\<lambda>x. f x \<notin> S)"] not_eventually[of "(\<lambda>x. f x \<in> S \<and> f x \<notin> S)" net]
   3.292        unfolding eventually_def by blast
   3.293 @@ -1546,7 +1561,7 @@
   3.294      with `?lhs` obtain d where d:"d>0" "\<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" unfolding Lim_at by auto
   3.295      { fix x::"real^'a" assume "0 < dist x 0 \<and> dist x 0 < d"
   3.296        hence "dist (f (a + x)) l < e" using d
   3.297 -      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_def dist_sym)
   3.298 +      apply(erule_tac x="x+a" in allE) by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
   3.299      }
   3.300      hence "\<exists>d>0. \<forall>x. 0 < dist x 0 \<and> dist x 0 < d \<longrightarrow> dist (f (a + x)) l < e" using d(1) by auto
   3.301    }
   3.302 @@ -1558,7 +1573,7 @@
   3.303        unfolding Lim_at by auto
   3.304      { fix x::"real^'a" assume "0 < dist x a \<and> dist x a < d"
   3.305        hence "dist (f x) l < e" using d apply(erule_tac x="x-a" in allE)
   3.306 -	by(auto simp add: comm_monoid_add.mult_commute dist_def dist_sym)
   3.307 +	by(auto simp add: comm_monoid_add.mult_commute dist_def dist_commute)
   3.308      }
   3.309      hence "\<exists>d>0. \<forall>x. 0 < dist x a \<and> dist x a < d \<longrightarrow> dist (f x) l < e" using d(1) by auto
   3.310    }
   3.311 @@ -1575,14 +1590,16 @@
   3.312    { fix x assume "x \<noteq> a"
   3.313      then obtain y where y:"dist y a \<le> dist a a \<and> 0 < dist y a \<and> y \<in> S \<or> dist y a \<le> dist x a \<and> 0 < dist y a \<and> y \<in> S" using assms unfolding trivial_limit_def within at by blast
   3.314      assume "\<forall>y. \<not> netord (at a within S) y x"
   3.315 -    hence "x = a" using y unfolding within at by (auto simp add: dist_refl dist_nz)
   3.316 +    hence "x = a" using y unfolding within at by (auto simp add: dist_nz)
   3.317    }
   3.318    moreover
   3.319 -  have "\<forall>y. \<not> netord (at a within S) y a"  using assms unfolding trivial_limit_def within at by (auto simp add: dist_refl)
   3.320 +  have "\<forall>y. \<not> netord (at a within S) y a"  using assms unfolding trivial_limit_def within at by auto
   3.321    ultimately show ?thesis unfolding netlimit_def using some_equality[of "\<lambda>x. \<forall>y. \<not> netord (at a within S) y x"] by blast
   3.322  qed
   3.323  
   3.324 -lemma netlimit_at: "netlimit(at a) = a"
   3.325 +lemma netlimit_at:
   3.326 +  fixes a :: "real ^ 'n::finite"
   3.327 +  shows "netlimit(at a) = a"
   3.328    apply (subst within_UNIV[symmetric])
   3.329    using netlimit_within[of a UNIV]
   3.330    by (simp add: trivial_limit_at within_UNIV)
   3.331 @@ -1600,6 +1617,7 @@
   3.332    using Lim_eventually[of "\<lambda>x. f x - g x" 0 net] Lim_transform[of f g net l] by auto
   3.333  
   3.334  lemma Lim_transform_within:
   3.335 +  fixes x :: "real ^ 'n::finite"
   3.336    assumes "0 < d" "(\<forall>x'\<in>S. 0 < dist x' x \<and> dist x' x < d \<longrightarrow> f x' = g x')"
   3.337            "(f ---> l) (at x within S)"
   3.338    shows   "(g ---> l) (at x within S)"
   3.339 @@ -1623,7 +1641,7 @@
   3.340    shows "(g ---> l) (at a within S)"
   3.341  proof-
   3.342    have "\<forall>x'\<in>S. 0 < dist x' a \<and> dist x' a < dist a b \<longrightarrow> f x' = g x'" using assms(2)
   3.343 -    apply auto apply(erule_tac x=x' in ballE) by (auto simp add: dist_sym dist_refl)
   3.344 +    apply auto apply(erule_tac x=x' in ballE) by (auto simp add: dist_commute)
   3.345    thus ?thesis using Lim_transform_within[of "dist a b" S a f g l] using assms(1,3) unfolding dist_nz by auto
   3.346  qed
   3.347  
   3.348 @@ -1644,7 +1662,7 @@
   3.349  proof-
   3.350    from assms(1,2) obtain e::real where "e>0" and e:"ball a e \<subseteq> S" unfolding open_contains_ball by auto
   3.351    hence "\<forall>x'. 0 < dist x' a \<and> dist x' a < e \<longrightarrow> f x' = g x'" using assms(3)
   3.352 -    unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_refl dist_sym)
   3.353 +    unfolding ball_def subset_eq apply auto apply(erule_tac x=x' in allE) apply(erule_tac x=x' in ballE) by(auto simp add: dist_commute)
   3.354    thus ?thesis using Lim_transform_at[of e a f g l] `e>0` assms(4) by auto
   3.355  qed
   3.356  
   3.357 @@ -1683,7 +1701,7 @@
   3.358  
   3.359  lemma closure_approachable: "x \<in> closure S \<longleftrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e)"
   3.360    apply (auto simp add: closure_def islimpt_approachable)
   3.361 -  by (metis dist_refl)
   3.362 +  by (metis dist_self)
   3.363  
   3.364  lemma closed_approachable: "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
   3.365    by (metis closure_closed closure_approachable)
   3.366 @@ -1765,7 +1783,7 @@
   3.367      proof(cases "d \<le> dist x y")
   3.368        case True thus "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
   3.369        proof(cases "x=y")
   3.370 -	case True hence False using `d \<le> dist x y` `d>0` dist_refl[of x] by auto
   3.371 +	case True hence False using `d \<le> dist x y` `d>0` by auto
   3.372  	thus "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d" by auto
   3.373        next
   3.374  	case False
   3.375 @@ -1776,7 +1794,7 @@
   3.376  	also have "\<dots> = \<bar>- 1 + d / (2 * norm (x - y))\<bar> * norm (x - y)"
   3.377  	  using vector_sadd_rdistrib[of "- 1" "d / (2 * norm (y - x))", THEN sym, of "y - x"]
   3.378  	  unfolding vector_smult_lneg vector_smult_lid
   3.379 -	  by (auto simp add: dist_sym[unfolded dist_def] norm_mul)
   3.380 +	  by (auto simp add: dist_commute[unfolded dist_def] norm_mul)
   3.381  	also have "\<dots> = \<bar>- norm (x - y) + d / 2\<bar>"
   3.382  	  unfolding abs_mult_pos[of "norm (x - y)", OF norm_ge_zero[of "x - y"]]
   3.383  	  unfolding real_add_mult_distrib using `x\<noteq>y`[unfolded dist_nz, unfolded dist_def] by auto
   3.384 @@ -1786,10 +1804,10 @@
   3.385  	moreover
   3.386  
   3.387  	have "(d / (2*dist y x)) *s (y - x) \<noteq> 0"
   3.388 -	  using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding vector_mul_eq_0 by (auto simp add: dist_sym dist_refl)
   3.389 +	  using `x\<noteq>y`[unfolded dist_nz] `d>0` unfolding vector_mul_eq_0 by (auto simp add: dist_commute)
   3.390  	moreover
   3.391  	have "dist (y - (d / (2 * dist y x)) *s (y - x)) y < d" unfolding dist_def apply simp unfolding norm_minus_cancel norm_mul
   3.392 -	  using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_sym[of x y]
   3.393 +	  using `d>0` `x\<noteq>y`[unfolded dist_nz] dist_commute[of x y]
   3.394  	  unfolding dist_def by auto
   3.395  	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
   3.396        qed
   3.397 @@ -1799,12 +1817,12 @@
   3.398        proof(cases "x=y")
   3.399  	case True
   3.400  	obtain z where **:"dist y z = (min e d) / 2" using vector_choose_dist[of "(min e d) / 2" y]
   3.401 -	  using `d > 0` `e>0` by (auto simp add: dist_refl)
   3.402 +	  using `d > 0` `e>0` by auto
   3.403  	show "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
   3.404 -	  apply(rule_tac x=z in bexI) unfolding `x=y` dist_sym dist_refl dist_nz using **  `d > 0` `e>0` by auto
   3.405 +	  apply(rule_tac x=z in bexI) unfolding `x=y` dist_commute dist_nz using **  `d > 0` `e>0` by auto
   3.406        next
   3.407  	case False thus "\<exists>x'\<in>ball x e. x' \<noteq> y \<and> dist x' y < d"
   3.408 -	  using `d>0` `d > dist x y` `?rhs` by(rule_tac x=x in bexI, auto simp add: dist_refl)
   3.409 +	  using `d>0` `d > dist x y` `?rhs` by(rule_tac x=x in bexI, auto)
   3.410        qed
   3.411      qed  }
   3.412    thus "?lhs" unfolding mem_cball islimpt_approachable mem_ball by auto
   3.413 @@ -1819,7 +1837,7 @@
   3.414    case False note cs = this
   3.415    from cs have "ball x e = {}" using ball_empty[of e x] by auto moreover
   3.416    { fix y assume "y \<in> cball x e"
   3.417 -    hence False unfolding mem_cball using dist_nz[of x y] cs by (auto simp add: dist_refl)  }
   3.418 +    hence False unfolding mem_cball using dist_nz[of x y] cs by auto  }
   3.419    hence "cball x e = {}" by auto
   3.420    hence "interior (cball x e) = {}" using interior_empty by auto
   3.421    ultimately show ?thesis by blast
   3.422 @@ -1831,12 +1849,12 @@
   3.423  
   3.424      then obtain xa where xa:"dist y xa = d / 2" using vector_choose_dist[of "d/2" y] by auto
   3.425      hence xa_y:"xa \<noteq> y" using dist_nz[of y xa] using `d>0` by auto
   3.426 -    have "xa\<in>S" using d[THEN spec[where x=xa]] using xa apply(auto simp add: dist_sym) unfolding dist_nz[THEN sym] using xa_y by auto
   3.427 +    have "xa\<in>S" using d[THEN spec[where x=xa]] using xa apply(auto simp add: dist_commute) unfolding dist_nz[THEN sym] using xa_y by auto
   3.428      hence xa_cball:"xa \<in> cball x e" using as(1) by auto
   3.429  
   3.430      hence "y \<in> ball x e" proof(cases "x = y")
   3.431        case True
   3.432 -      hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] by (auto simp add: dist_sym)
   3.433 +      hence "e>0" using xa_y[unfolded dist_nz] xa_cball[unfolded mem_cball] by (auto simp add: dist_commute)
   3.434        thus "y \<in> ball x e" using `x = y ` by simp
   3.435      next
   3.436        case False
   3.437 @@ -1853,7 +1871,7 @@
   3.438  	by (auto simp add: vector_sadd_rdistrib vector_smult_lid ring_simps vector_sadd_rdistrib vector_ssub_ldistrib)
   3.439        also have "\<dots> = \<bar>1 + d / (2 * norm (y - x))\<bar> * norm (y - x)" using ** by auto
   3.440        also have "\<dots> = (dist y x) + d/2"using ** by (auto simp add: left_distrib dist_def)
   3.441 -      finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_sym)
   3.442 +      finally have "e \<ge> dist x y +d/2" using *[unfolded mem_cball] by (auto simp add: dist_commute)
   3.443        thus "y \<in> ball x e" unfolding mem_ball using `d>0` by auto
   3.444      qed  }
   3.445    hence "\<forall>S \<subseteq> cball x e. open S \<longrightarrow> S \<subseteq> ball x e" by auto
   3.446 @@ -1872,17 +1890,17 @@
   3.447  
   3.448  lemma cball_eq_empty: "(cball x e = {}) \<longleftrightarrow> e < 0"
   3.449    apply (simp add: expand_set_eq not_le)
   3.450 -  by (metis dist_pos_le dist_refl order_less_le_trans)
   3.451 +  by (metis zero_le_dist dist_self order_less_le_trans)
   3.452  lemma cball_empty: "e < 0 ==> cball x e = {}" by (simp add: cball_eq_empty)
   3.453  
   3.454  lemma cball_eq_sing: "(cball x e = {x}) \<longleftrightarrow> e = 0"
   3.455  proof-
   3.456    { assume as:"\<forall>xa. (dist x xa \<le> e) = (xa = x)"
   3.457 -    hence "e \<ge> 0" apply (erule_tac x=x in allE) by (auto simp add: dist_pos_le dist_refl)
   3.458 +    hence "e \<ge> 0" apply (erule_tac x=x in allE) by auto
   3.459      then obtain y where y:"dist x y = e" using vector_choose_dist[of e] by auto
   3.460 -    hence "e = 0" using as apply(erule_tac x=y in allE) by (auto simp add: dist_pos_le dist_refl)
   3.461 +    hence "e = 0" using as apply(erule_tac x=y in allE) by auto
   3.462    }
   3.463 -  thus ?thesis unfolding expand_set_eq mem_cball by (auto simp add: dist_refl dist_nz dist_le_0)
   3.464 +  thus ?thesis unfolding expand_set_eq mem_cball by (auto simp add: dist_nz)
   3.465  qed
   3.466  
   3.467  lemma cball_sing:  "e = 0 ==> cball x e = {x}" by (simp add: cball_eq_sing)
   3.468 @@ -1894,7 +1912,7 @@
   3.469  proof-
   3.470    from assms obtain e where e:"e>0" "\<forall>y. dist x y < e \<longrightarrow> y \<in> S" unfolding mem_interior ball_def subset_eq by auto
   3.471    { assume "?lhs" then obtain d where "d>0" "\<forall>xa\<in>S. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa" unfolding eventually_within by auto
   3.472 -    hence "?rhs" unfolding eventually_at using e by (auto simp add: dist_sym intro!: add exI[of _ "min e d"])
   3.473 +    hence "?rhs" unfolding eventually_at using e by (auto simp add: dist_commute intro!: add exI[of _ "min e d"])
   3.474    } moreover
   3.475    { assume "?rhs" hence "?lhs" unfolding eventually_within eventually_at by auto
   3.476    } ultimately
   3.477 @@ -2252,7 +2270,9 @@
   3.478  
   3.479    (* FIXME: Unify this with Cauchy from SEQ!!!!!*)
   3.480  
   3.481 -definition cauchy_def:"cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
   3.482 +definition
   3.483 +  cauchy :: "(nat \<Rightarrow> real ^ 'n::finite) \<Rightarrow> bool" where
   3.484 +  "cauchy s \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m n. m \<ge> N \<and> n \<ge> N --> dist(s m)(s n) < e)"
   3.485  
   3.486  definition complete_def:"complete s \<longleftrightarrow> (\<forall>f::(nat=>real^'a::finite). (\<forall>n. f n \<in> s) \<and> cauchy f
   3.487                        --> (\<exists>l \<in> s. (f ---> l) sequentially))"
   3.488 @@ -2297,7 +2317,7 @@
   3.489    hence N:"\<forall>n. N \<le> n \<longrightarrow> dist (s N) (s n) < 1" by auto
   3.490    { fix n::nat assume "n\<ge>N"
   3.491      hence "norm (s n) \<le> norm (s N) + 1" using N apply(erule_tac x=n in allE) unfolding dist_def
   3.492 -      using norm_triangle_sub[of "s N" "s n"] by (auto, metis dist_def dist_sym le_add_right_mono norm_triangle_sub real_less_def)
   3.493 +      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)
   3.494    }
   3.495    hence "\<forall>n\<ge>N. norm (s n) \<le> norm (s N) + 1" by auto
   3.496    moreover
   3.497 @@ -2327,7 +2347,7 @@
   3.498  	have "dist ((f \<circ> r) n) l < e/2" using n M by auto
   3.499  	moreover have "r n \<ge> N" using lr'[of n] n by auto
   3.500  	hence "dist (f n) ((f \<circ> r) n) < e / 2" using N using n by auto
   3.501 -	ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_sym)  }
   3.502 +	ultimately have "dist (f n) l < e" using dist_triangle_half_r[of "f (r n)" "f n" e l] by (auto simp add: dist_commute)  }
   3.503        hence "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast  }
   3.504      hence "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s` unfolding Lim_sequentially by auto  }
   3.505    thus ?thesis unfolding complete_def by auto
   3.506 @@ -2443,7 +2463,7 @@
   3.507    then obtain y where y:"y \<in> ball x (inverse (real (r (N1 + N2) + 1)))" "y \<notin> b" by auto
   3.508  
   3.509    have "dist x l < e/2" using N1 unfolding x_def o_def by auto
   3.510 -  hence "dist y l < e" using y N2' using dist_triangle[of y l x]by (auto simp add:dist_sym)
   3.511 +  hence "dist y l < e" using y N2' using dist_triangle[of y l x]by (auto simp add:dist_commute)
   3.512  
   3.513    thus False using e and `y\<notin>b` by auto
   3.514  qed
   3.515 @@ -2533,14 +2553,14 @@
   3.516      proof(cases "m<n")
   3.517        case True
   3.518        hence "1 < norm (x n) - norm (x m)" using *[of m n] by auto
   3.519 -      thus ?thesis unfolding dist_sym[of "x m" "x n"] unfolding dist_def using norm_triangle_sub[of "x n" "x m"] by auto
   3.520 +      thus ?thesis unfolding dist_commute[of "x m" "x n"] unfolding dist_def using norm_triangle_sub[of "x n" "x m"] by auto
   3.521      next
   3.522        case False hence "n<m" using `m\<noteq>n` by auto
   3.523        hence "1 < norm (x m) - norm (x n)" using *[of n m] by auto
   3.524 -      thus ?thesis unfolding dist_sym[of "x n" "x m"] unfolding dist_def using norm_triangle_sub[of "x m" "x n"] by auto
   3.525 +      thus ?thesis unfolding dist_commute[of "x n" "x m"] unfolding dist_def using norm_triangle_sub[of "x m" "x n"] by auto
   3.526      qed  } note ** = this
   3.527    { fix a b assume "x a = x b" "a \<noteq> b"
   3.528 -    hence False using **[of a b] unfolding dist_eq_0[THEN sym] by auto  }
   3.529 +    hence False using **[of a b] by auto  }
   3.530    hence "inj x" unfolding inj_on_def by auto
   3.531    moreover
   3.532    { fix n::nat
   3.533 @@ -2583,7 +2603,7 @@
   3.534    then obtain N::nat where N:"\<forall>n\<ge>N. dist (f n) l < e / 2"
   3.535      using assms(2)[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
   3.536    def d \<equiv> "Min (insert (e/2) ((\<lambda>n. if dist (f n) l' = 0 then e/2 else dist (f n) l') ` {0 .. N}))"
   3.537 -  have "d>0" using `e>0` unfolding d_def e_def using dist_pos_le[of _ l', unfolded order_le_less] by auto
   3.538 +  have "d>0" using `e>0` unfolding d_def e_def using zero_le_dist[of _ l', unfolded order_le_less] by auto
   3.539    obtain k where k:"f k \<noteq> l'"  "dist (f k) l' < d" using `d>0` and assms(3)[unfolded islimpt_approachable, THEN spec[where x="d"]] by auto
   3.540    have "k\<ge>N" using k(1)[unfolded dist_nz] using k(2)[unfolded d_def]
   3.541      by force
   3.542 @@ -2829,9 +2849,9 @@
   3.543      { fix e::real assume "e>0"
   3.544        hence "dist a b < e" using assms(4 )using b using a by blast
   3.545      }
   3.546 -    hence "dist a b = 0" by (metis dist_eq_0 dist_nz real_less_def)
   3.547 +    hence "dist a b = 0" by (metis dist_eq_0_iff dist_nz real_less_def)
   3.548    }
   3.549 -  with a have "\<Inter>{t. \<exists>n. t = s n} = {a}"  unfolding dist_eq_0 by auto
   3.550 +  with a have "\<Inter>{t. \<exists>n. t = s n} = {a}"  by auto
   3.551    thus ?thesis by auto
   3.552  qed
   3.553  
   3.554 @@ -2865,12 +2885,13 @@
   3.555  	using l[THEN spec[where x=x], unfolded Lim_sequentially] using `e>0` by(auto elim!: allE[where x="e/2"])
   3.556        fix n::nat assume "n\<ge>N"
   3.557        hence "dist(s n x)(l x) < e"  using `P x`and N[THEN spec[where x=n], THEN spec[where x="N+M"], THEN spec[where x=x]]
   3.558 -	using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"] by (auto simp add: dist_sym)  }
   3.559 +	using M[THEN spec[where x="N+M"]] and dist_triangle_half_l[of "s n x" "s (N+M) x" e "l x"] by (auto simp add: dist_commute)  }
   3.560      hence "\<exists>N. \<forall>n x. N \<le> n \<and> P x \<longrightarrow> dist(s n x)(l x) < e" by auto }
   3.561    thus ?lhs by auto
   3.562  qed
   3.563  
   3.564  lemma uniformly_cauchy_imp_uniformly_convergent:
   3.565 +  fixes s :: "nat \<Rightarrow> 'a \<Rightarrow> real ^ 'n::finite"
   3.566    assumes "\<forall>e>0.\<exists>N. \<forall>m (n::nat) x. N \<le> m \<and> N \<le> n \<and> P x --> dist(s m x)(s n x) < e"
   3.567            "\<forall>x. P x --> (\<forall>e>0. \<exists>N. \<forall>n. N \<le> n --> dist(s n x)(l x) < e)"
   3.568    shows "\<forall>e>0. \<exists>N. \<forall>n x. N \<le> n \<and> P x --> dist(s n x)(l x) < e"
   3.569 @@ -2937,32 +2958,37 @@
   3.570        using `?lhs`[unfolded continuous_within Lim_within] by auto
   3.571      { fix y assume "y\<in>f ` (ball x d \<inter> s)"
   3.572        hence "y \<in> ball (f x) e" using d(2) unfolding dist_nz[THEN sym]
   3.573 -	apply (auto simp add: dist_sym mem_ball) apply(erule_tac x=xa in ballE) apply auto unfolding dist_refl using `e>0` by auto
   3.574 +	apply (auto simp add: dist_commute mem_ball) apply(erule_tac x=xa in ballE) apply auto using `e>0` by auto
   3.575      }
   3.576 -    hence "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e" using `d>0` unfolding subset_eq ball_def by (auto simp add: dist_sym)  }
   3.577 +    hence "\<exists>d>0. f ` (ball x d \<inter> s) \<subseteq> ball (f x) e" using `d>0` unfolding subset_eq ball_def by (auto simp add: dist_commute)  }
   3.578    thus ?rhs by auto
   3.579  next
   3.580    assume ?rhs thus ?lhs unfolding continuous_within Lim_within ball_def subset_eq
   3.581 -    apply (auto simp add: dist_sym) apply(erule_tac x=e in allE) by auto
   3.582 +    apply (auto simp add: dist_commute) apply(erule_tac x=e in allE) by auto
   3.583  qed
   3.584  
   3.585  lemma continuous_at_ball: fixes f::"real^'a::finite \<Rightarrow> real^'a"
   3.586    shows "continuous (at x) f \<longleftrightarrow> (\<forall>e>0. \<exists>d>0. f ` (ball x d) \<subseteq> ball (f x) e)" (is "?lhs = ?rhs")
   3.587  proof
   3.588    assume ?lhs thus ?rhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
   3.589 -    apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x=xa in allE) apply (auto simp add: dist_refl dist_sym dist_nz)
   3.590 -    unfolding dist_nz[THEN sym] by (auto simp add: dist_refl)
   3.591 +    apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x=xa in allE) apply (auto simp add: dist_commute dist_nz)
   3.592 +    unfolding dist_nz[THEN sym] by auto
   3.593  next
   3.594    assume ?rhs thus ?lhs unfolding continuous_at Lim_at subset_eq Ball_def Bex_def image_iff mem_ball
   3.595 -    apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x="f xa" in allE) by (auto simp add: dist_refl dist_sym dist_nz)
   3.596 +    apply auto apply(erule_tac x=e in allE) apply auto apply(rule_tac x=d in exI) apply auto apply(erule_tac x="f xa" in allE) by (auto simp add: dist_commute dist_nz)
   3.597  qed
   3.598  
   3.599  text{* For setwise continuity, just start from the epsilon-delta definitions. *}
   3.600  
   3.601 -definition "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d::real>0. \<forall>x' \<in> s. dist x' x < d --> dist (f x') (f x) < e)"
   3.602 -
   3.603 -
   3.604 -definition "uniformly_continuous_on s f \<longleftrightarrow>
   3.605 +definition
   3.606 +  continuous_on :: "(real ^ 'n::finite) set \<Rightarrow> (real ^ 'n \<Rightarrow> real ^ 'm::finite) \<Rightarrow> bool" where
   3.607 +  "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d::real>0. \<forall>x' \<in> s. dist x' x < d --> dist (f x') (f x) < e)"
   3.608 +
   3.609 +
   3.610 +definition
   3.611 +  uniformly_continuous_on ::
   3.612 +    "(real ^ 'n::finite) set \<Rightarrow> (real ^ 'n \<Rightarrow> real ^ 'm::finite) \<Rightarrow> bool" where
   3.613 +  "uniformly_continuous_on s f \<longleftrightarrow>
   3.614          (\<forall>e>0. \<exists>d>0. \<forall>x\<in>s. \<forall> x'\<in>s. dist x' x < d
   3.615                             --> dist (f x') (f x) < e)"
   3.616  
   3.617 @@ -2985,7 +3011,7 @@
   3.618    { fix x' assume "\<not> 0 < dist x' x"
   3.619      hence "x=x'"
   3.620        using dist_nz[of x' x] by auto
   3.621 -    hence "dist (f x') (f x) < e" using dist_refl[of "f x'"] `e>0` by auto
   3.622 +    hence "dist (f x') (f x) < e" using `e>0` by auto
   3.623    }
   3.624    thus "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using d by auto
   3.625  qed
   3.626 @@ -2999,8 +3025,8 @@
   3.627      assume "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e"
   3.628      then obtain d where "d>0" and d:"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" by auto
   3.629      { fix x' assume as:"x'\<in>s" "dist x' x < d"
   3.630 -      hence "dist (f x') (f x) < e" using dist_refl[of "f x'"] `e>0` d `x'\<in>s` dist_eq_0[of x' x] dist_pos_le[of x' x] as(2) by (metis dist_eq_0 dist_nz) }
   3.631 -    hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `d>0` by (auto simp add: dist_refl)
   3.632 +      hence "dist (f x') (f x) < e" using `e>0` d `x'\<in>s` dist_eq_0_iff[of x' x] zero_le_dist[of x' x] as(2) by (metis dist_eq_0_iff dist_nz) }
   3.633 +    hence "\<exists>d>0. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `d>0` by auto
   3.634    }
   3.635    thus ?lhs using `?rhs` unfolding continuous_on_def continuous_within Lim_within by auto
   3.636  next
   3.637 @@ -3051,7 +3077,7 @@
   3.638      hence "\<exists>N. \<forall>n\<ge>N. dist ((f \<circ> x) n) (f a) < e"
   3.639        apply(rule_tac  x=N in exI) using N d  apply auto using x(1)
   3.640        apply(erule_tac x=n in allE) apply(erule_tac x=n in allE)
   3.641 -      apply(erule_tac x="x n" in ballE)  apply auto unfolding dist_nz[THEN sym] apply auto unfolding dist_refl using `e>0` by auto
   3.642 +      apply(erule_tac x="x n" in ballE)  apply auto unfolding dist_nz[THEN sym] apply auto using `e>0` by auto
   3.643    }
   3.644    thus ?rhs unfolding continuous_within unfolding Lim_sequentially by simp
   3.645  next
   3.646 @@ -3106,7 +3132,7 @@
   3.647        { fix n assume "n\<ge>N"
   3.648  	hence "norm (f (x n) - f (y n) - 0) < e"
   3.649  	  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
   3.650 -	  unfolding dist_sym and dist_def by simp  }
   3.651 +	  unfolding dist_commute and dist_def by simp  }
   3.652        hence "\<exists>N. \<forall>n\<ge>N. norm (f (x n) - f (y n) - 0) < e"  by auto  }
   3.653      hence "((\<lambda>n. f(x n) - f(y n)) ---> 0) sequentially" unfolding Lim_sequentially and dist_def by auto  }
   3.654    thus ?rhs by auto
   3.655 @@ -3116,7 +3142,7 @@
   3.656      then obtain e where "e>0" "\<forall>d>0. \<exists>x\<in>s. \<exists>x'\<in>s. dist x' x < d \<and> \<not> dist (f x') (f x) < e" unfolding uniformly_continuous_on_def by auto
   3.657      then obtain fa where fa:"\<forall>x.  0 < x \<longrightarrow> fst (fa x) \<in> s \<and> snd (fa x) \<in> s \<and> dist (fst (fa x)) (snd (fa x)) < x \<and> \<not> dist (f (fst (fa x))) (f (snd (fa x))) < e"
   3.658        using choice[of "\<lambda>d x. d>0 \<longrightarrow> fst x \<in> s \<and> snd x \<in> s \<and> dist (snd x) (fst x) < d \<and> \<not> dist (f (snd x)) (f (fst x)) < e"] unfolding Bex_def
   3.659 -      by (auto simp add: dist_sym)
   3.660 +      by (auto simp add: dist_commute)
   3.661      def x \<equiv> "\<lambda>n::nat. fst (fa (inverse (real n + 1)))"
   3.662      def y \<equiv> "\<lambda>n::nat. snd (fa (inverse (real n + 1)))"
   3.663      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"
   3.664 @@ -3145,7 +3171,7 @@
   3.665    { fix e::real assume "e>0"
   3.666      then obtain d' where d':"d'>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(4) unfolding continuous_within Lim_within by auto
   3.667      { fix x' assume "x'\<in>s" "0 < dist x' x" "dist x' x < (min d d')"
   3.668 -      hence "dist (f x') (g x) < e" using assms(2,3) apply(erule_tac x=x in ballE) unfolding dist_refl using d' by auto  }
   3.669 +      hence "dist (f x') (g x) < e" using assms(2,3) apply(erule_tac x=x in ballE) using d' by auto  }
   3.670      hence "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
   3.671      hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto  }
   3.672    hence "(f ---> g x) (at x within s)" unfolding Lim_within using assms(1) by auto
   3.673 @@ -3160,7 +3186,7 @@
   3.674    { fix e::real assume "e>0"
   3.675      then obtain d' where d':"d'>0" "\<forall>xa. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < e" using assms(3) unfolding continuous_at Lim_at by auto
   3.676      { fix x' assume "0 < dist x' x" "dist x' x < (min d d')"
   3.677 -      hence "dist (f x') (g x) < e" using assms(2) apply(erule_tac x=x in allE) unfolding dist_refl using d' by auto
   3.678 +      hence "dist (f x') (g x) < e" using assms(2) apply(erule_tac x=x in allE) using d' by auto
   3.679      }
   3.680      hence "\<forall>xa. 0 < dist xa x \<and> dist xa x < (min d d') \<longrightarrow> dist (f xa) (g x) < e" by blast
   3.681      hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (g x) < e" using `d>0` `d'>0` by(rule_tac x="min d d'" in exI)auto
   3.682 @@ -3287,8 +3313,8 @@
   3.683      with assms(2)[unfolded continuous_within Lim_within] obtain d  where "d>0" and d:"\<forall>xa\<in>f ` s. 0 < dist xa (f x) \<and> dist xa (f x) < d \<longrightarrow> dist (g xa) (g (f x)) < e" by auto
   3.684      from assms(1)[unfolded continuous_within Lim_within] obtain d' where "d'>0" and d':"\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d' \<longrightarrow> dist (f xa) (f x) < d" using `d>0` by auto
   3.685      { fix y assume as:"y\<in>s"  "0 < dist y x"  "dist y x < d'"
   3.686 -      hence "dist (f y) (f x) < d" using d'[THEN bspec[where x=y]] by (auto simp add:dist_sym)
   3.687 -      hence "dist (g (f y)) (g (f x)) < e" using as(1) d[THEN bspec[where x="f y"]] unfolding dist_nz[THEN sym] using `e>0` by (auto simp add: dist_refl)   }
   3.688 +      hence "dist (f y) (f x) < d" using d'[THEN bspec[where x=y]] by (auto simp add:dist_commute)
   3.689 +      hence "dist (g (f y)) (g (f x)) < e" using as(1) d[THEN bspec[where x="f y"]] unfolding dist_nz[THEN sym] using `e>0` by auto   }
   3.690      hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (g (f xa)) (g (f x)) < e" using `d'>0` by auto  }
   3.691    thus ?thesis unfolding continuous_within Lim_within by auto
   3.692  qed
   3.693 @@ -3332,7 +3358,7 @@
   3.694      moreover
   3.695      { fix x' assume "x'\<in>ball x d" hence "f x' \<in> t"
   3.696  	using e[unfolded subset_eq Ball_def mem_ball, THEN spec[where x="f x'"]]    d[THEN spec[where x=x']]
   3.697 -	unfolding mem_ball apply (auto simp add: dist_sym)
   3.698 +	unfolding mem_ball apply (auto simp add: dist_commute)
   3.699  	unfolding dist_nz[THEN sym] using as(2) by auto  }
   3.700      hence "\<forall>x'\<in>ball x d. f x' \<in> t" by auto
   3.701      ultimately have "\<exists>s. open s \<and> x \<in> s \<and> (\<forall>x'\<in>s. f x' \<in> t)"
   3.702 @@ -3346,7 +3372,7 @@
   3.703      then obtain d where "d>0" and d:"ball x d \<subseteq> s" unfolding open_contains_ball by auto
   3.704      { fix y assume "0 < dist y x \<and> dist y x < d"
   3.705        hence "dist (f y) (f x) < e" using d[unfolded subset_eq Ball_def mem_ball, THEN spec[where x=y]]
   3.706 -	using s(3)[THEN bspec[where x=y], unfolded mem_ball] by (auto simp add: dist_sym)  }
   3.707 +	using s(3)[THEN bspec[where x=y], unfolded mem_ball] by (auto simp add: dist_commute)  }
   3.708      hence "\<exists>d>0. \<forall>xa. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `d>0` by auto  }
   3.709    thus ?lhs unfolding continuous_at Lim_at by auto
   3.710  qed
   3.711 @@ -3363,7 +3389,7 @@
   3.712      { fix x assume as':"x\<in>{x \<in> s. f x \<in> t}"
   3.713        then obtain e where e: "e>0" "\<forall>x'\<in>f ` s. dist x' (f x) < e \<longrightarrow> x' \<in> t" using as[unfolded openin_euclidean_subtopology_iff, THEN conjunct2, THEN bspec[where x="f x"]] by auto
   3.714        from this(1) obtain d where d: "d>0" "\<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" using `?lhs`[unfolded continuous_on Lim_within, THEN bspec[where x=x]] using as' by auto
   3.715 -      have "\<exists>e>0. \<forall>x'\<in>s. dist x' x < e \<longrightarrow> x' \<in> {x \<in> s. f x \<in> t}" using d e unfolding dist_nz[THEN sym] by (rule_tac x=d in exI, auto simp add: dist_refl)  }
   3.716 +      have "\<exists>e>0. \<forall>x'\<in>s. dist x' x < e \<longrightarrow> x' \<in> {x \<in> s. f x \<in> t}" using d e unfolding dist_nz[THEN sym] by (rule_tac x=d in exI, auto)  }
   3.717      ultimately have "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" unfolding openin_euclidean_subtopology_iff by auto  }
   3.718    thus ?rhs unfolding continuous_on Lim_within using openin by auto
   3.719  next
   3.720 @@ -3371,12 +3397,12 @@
   3.721    { fix e::real and x assume "x\<in>s" "e>0"
   3.722      { fix xa x' assume "dist (f xa) (f x) < e" "xa \<in> s" "x' \<in> s" "dist (f xa) (f x') < e - dist (f xa) (f x)"
   3.723        hence "dist (f x') (f x) < e" using dist_triangle[of "f x'" "f x" "f xa"]
   3.724 -	by (auto simp add: dist_sym)  }
   3.725 +	by (auto simp add: dist_commute)  }
   3.726      hence "ball (f x) e \<inter> f ` s \<subseteq> f ` s \<and> (\<forall>xa\<in>ball (f x) e \<inter> f ` s. \<exists>ea>0. \<forall>x'\<in>f ` s. dist x' xa < ea \<longrightarrow> x' \<in> ball (f x) e \<inter> f ` s)" apply auto
   3.727 -      apply(rule_tac x="e - dist (f xa) (f x)" in exI) using `e>0` by (auto simp add: dist_sym)
   3.728 +      apply(rule_tac x="e - dist (f xa) (f x)" in exI) using `e>0` by (auto simp add: dist_commute)
   3.729      hence "\<forall>xa\<in>{xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}. \<exists>ea>0. \<forall>x'\<in>s. dist x' xa < ea \<longrightarrow> x' \<in> {xa \<in> s. f xa \<in> ball (f x) e \<inter> f ` s}"
   3.730        using `?rhs`[unfolded openin_euclidean_subtopology_iff, THEN spec[where x="ball (f x) e \<inter> f ` s"]] by auto
   3.731 -    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" apply(erule_tac x=x in ballE) apply auto unfolding dist_refl using `e>0` `x\<in>s` by (auto simp add: dist_sym)  }
   3.732 +    hence "\<exists>d>0. \<forall>xa\<in>s. 0 < dist xa x \<and> dist xa x < d \<longrightarrow> dist (f xa) (f x) < e" apply(erule_tac x=x in ballE) apply auto using `e>0` `x\<in>s` by (auto simp add: dist_commute)  }
   3.733    thus ?lhs unfolding continuous_on Lim_within by auto
   3.734  qed
   3.735  
   3.736 @@ -3504,7 +3530,7 @@
   3.737      using assms(1)[unfolded continuous_within Lim_within, THEN spec[where x="dist (f x) a"]] assms(3)[unfolded dist_nz] by auto
   3.738    { fix y assume " y\<in>s"  "dist x y < d"
   3.739      hence "f y \<noteq> a" using d[THEN bspec[where x=y]] assms(3)[unfolded dist_nz]
   3.740 -      apply auto unfolding dist_nz[THEN sym] by (auto simp add: dist_sym) }
   3.741 +      apply auto unfolding dist_nz[THEN sym] by (auto simp add: dist_commute) }
   3.742    thus ?thesis using `d>0` by auto
   3.743  qed
   3.744  
   3.745 @@ -3656,13 +3682,13 @@
   3.746        obtain z where "z\<in>s" and z:"ball x ea \<subseteq> ball z (d z (e / 2))" using ea[THEN bspec[where x=x]] and `x\<in>s` by auto
   3.747        hence "x\<in>ball z (d z (e / 2))" using `ea>0` unfolding subset_eq by auto
   3.748        hence "dist (f z) (f x) < e / 2" using d[THEN spec[where x="e/2"]] and `e>0` and `x\<in>s` and `z\<in>s`
   3.749 -	by (auto  simp add: dist_sym)
   3.750 +	by (auto  simp add: dist_commute)
   3.751        moreover have "y\<in>ball z (d z (e / 2))" using as and `ea>0` and z[unfolded subset_eq]
   3.752 -	by (auto simp add: dist_sym)
   3.753 +	by (auto simp add: dist_commute)
   3.754        hence "dist (f z) (f y) < e / 2" using d[THEN spec[where x="e/2"]] and `e>0` and `y\<in>s` and `z\<in>s`
   3.755 -	by (auto  simp add: dist_sym)
   3.756 +	by (auto  simp add: dist_commute)
   3.757        ultimately have "dist (f y) (f x) < e" using dist_triangle_half_r[of "f z" "f x" e "f y"]
   3.758 -	by (auto simp add: dist_sym)  }
   3.759 +	by (auto simp add: dist_commute)  }
   3.760      then have "\<exists>d>0. \<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e" using `ea>0` by auto  }
   3.761    thus ?thesis unfolding uniformly_continuous_on_def by auto
   3.762  qed
   3.763 @@ -3788,7 +3814,7 @@
   3.764  
   3.765  lemma continuous_on_vec1_range:
   3.766   " 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))"
   3.767 -  unfolding continuous_on_def apply (simp del: dist_sym) unfolding dist_vec1 unfolding dist_def ..
   3.768 +  unfolding continuous_on_def apply (simp del: dist_commute) unfolding dist_vec1 unfolding dist_def ..
   3.769  
   3.770  lemma continuous_at_vec1_norm:
   3.771   "\<forall>x. continuous (at x) (vec1 o norm)"
   3.772 @@ -3875,7 +3901,7 @@
   3.773      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 }
   3.774    thus ?thesis using assms
   3.775      using continuous_attains_sup[of s "\<lambda>x. dist a x"]
   3.776 -    unfolding continuous_on_vec1_range by (auto simp add: dist_sym)
   3.777 +    unfolding continuous_on_vec1_range by (auto simp add: dist_commute)
   3.778  qed
   3.779  
   3.780  text{* For *minimal* distance, we only need closure, not compactness.            *}
   3.781 @@ -3886,7 +3912,7 @@
   3.782  proof-
   3.783    from assms(2) obtain b where "b\<in>s" by auto
   3.784    let ?B = "cball a (dist b a) \<inter> s"
   3.785 -  have "b \<in> ?B" using `b\<in>s` by (simp add: dist_sym)
   3.786 +  have "b \<in> ?B" using `b\<in>s` by (simp add: dist_commute)
   3.787    hence "?B \<noteq> {}" by auto
   3.788    moreover
   3.789    { fix x assume "x\<in>?B"
   3.790 @@ -3896,7 +3922,7 @@
   3.791  	using real_abs_sub_norm[of "x' - a" "x - a"]  by auto  }
   3.792      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 }
   3.793    hence "continuous_on (cball a (dist b a) \<inter> s) (vec1 \<circ> dist a)" unfolding continuous_on_vec1_range
   3.794 -    by (auto  simp add: dist_sym)
   3.795 +    by (auto  simp add: dist_commute)
   3.796    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
   3.797    ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y" using continuous_attains_inf[of ?B "dist a"] by fastsimp
   3.798    thus ?thesis by fastsimp
   3.799 @@ -4273,8 +4299,8 @@
   3.800      using separate_point_closed[OF compact_closed_differences[OF assms(1,2)], of 0] by auto
   3.801    { fix x y assume "x\<in>s" "y\<in>t"
   3.802      hence "x - y \<in> {x - y |x y. x \<in> s \<and> y \<in> t}" by auto
   3.803 -    hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_sym
   3.804 -      by (auto  simp add: dist_sym)
   3.805 +    hence "d \<le> dist (x - y) 0" using d[THEN bspec[where x="x - y"]] using dist_commute
   3.806 +      by (auto  simp add: dist_commute)
   3.807      hence "d \<le> dist x y" unfolding dist_def by auto  }
   3.808    thus ?thesis using `d>0` by auto
   3.809  qed
   3.810 @@ -4286,7 +4312,7 @@
   3.811    have *:"t \<inter> s = {}" using assms(3) by auto
   3.812    show ?thesis using separate_compact_closed[OF assms(2,1) *]
   3.813      apply auto apply(rule_tac x=d in exI) apply auto apply (erule_tac x=y in ballE)
   3.814 -    by (auto simp add: dist_sym)
   3.815 +    by (auto simp add: dist_commute)
   3.816  qed
   3.817  
   3.818  (* A cute way of denoting open and closed intervals using overloading.       *)
   3.819 @@ -4789,7 +4815,7 @@
   3.820  	pos_less_divide_eq[OF False[unfolded vec_0 zero_less_norm_iff[of a, THEN sym]]] and real_mult_commute by auto
   3.821        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  }
   3.822      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  }
   3.823 -  thus ?thesis using assms unfolding Lim apply (auto simp add: dist_sym)
   3.824 +  thus ?thesis using assms unfolding Lim apply (auto simp add: dist_commute)
   3.825      unfolding dist_vec1 by auto
   3.826  qed
   3.827  
   3.828 @@ -5094,19 +5120,19 @@
   3.829    show ?th unfolding homeomorphic_minimal
   3.830      apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
   3.831      apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
   3.832 -    apply (auto simp add: dist_sym) unfolding dist_def and vector_smult_assoc using assms apply auto
   3.833 +    apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
   3.834      unfolding norm_minus_cancel and norm_mul
   3.835      using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
   3.836 -    apply (auto simp add: dist_sym)
   3.837 +    apply (auto simp add: dist_commute)
   3.838      using pos_less_divide_eq[OF *(1), THEN sym] unfolding real_mult_commute[of _ "\<bar>e / d\<bar>"]
   3.839      using pos_less_divide_eq[OF *(2), THEN sym] unfolding real_mult_commute[of _ "\<bar>d / e\<bar>"]
   3.840 -    by (auto simp add: dist_sym)
   3.841 +    by (auto simp add: dist_commute)
   3.842  next
   3.843    have *:"\<bar>e / d\<bar> > 0" "\<bar>d / e\<bar> >0" using assms using divide_pos_pos by auto
   3.844    show ?cth unfolding homeomorphic_minimal
   3.845      apply(rule_tac x="\<lambda>x. b + (e/d) *s (x - a)" in exI)
   3.846      apply(rule_tac x="\<lambda>x. a + (d/e) *s (x - b)" in exI)
   3.847 -    apply (auto simp add: dist_sym) unfolding dist_def and vector_smult_assoc using assms apply auto
   3.848 +    apply (auto simp add: dist_commute) unfolding dist_def and vector_smult_assoc using assms apply auto
   3.849      unfolding norm_minus_cancel and norm_mul
   3.850      using continuous_on_add[OF continuous_on_const continuous_on_cmul[OF continuous_on_sub[OF continuous_on_id continuous_on_const]]]
   3.851      apply auto
   3.852 @@ -5479,7 +5505,7 @@
   3.853        also have "\<dots> = (c ^ m) * (d * (1 - c ^ k) + (1 - c) * c ^ k * d)"
   3.854  	unfolding power_add by (auto simp add: ring_simps)
   3.855        also have "\<dots> \<le> (c ^ m) * d * (1 - c ^ Suc k)"
   3.856 -	using c by (auto simp add: ring_simps dist_pos_le)
   3.857 +	using c by (auto simp add: ring_simps)
   3.858        finally show ?case by auto
   3.859      qed
   3.860    } note cf_z2 = this
   3.861 @@ -5487,10 +5513,10 @@
   3.862      hence "\<exists>N. \<forall>m n. N \<le> m \<and> N \<le> n \<longrightarrow> dist (z m) (z n) < e"
   3.863      proof(cases "d = 0")
   3.864        case True
   3.865 -      hence "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def by (auto simp add: pos_prod_le[OF `1 - c > 0`] dist_le_0)
   3.866 +      hence "\<And>n. z n = z0" using cf_z2[of 0] and c unfolding z_def by (auto simp add: pos_prod_le[OF `1 - c > 0`])
   3.867        thus ?thesis using `e>0` by auto
   3.868      next
   3.869 -      case False hence "d>0" unfolding d_def using dist_pos_le[of "z 0" "z 1"]
   3.870 +      case False hence "d>0" unfolding d_def using zero_le_dist[of "z 0" "z 1"]
   3.871  	by (metis False d_def real_less_def)
   3.872        hence "0 < e * (1 - c) / d" using `e>0` and `1-c>0`
   3.873  	using divide_pos_pos[of "e * (1 - c)" d] and mult_pos_pos[of e "1 - c"] by auto
   3.874 @@ -5505,7 +5531,7 @@
   3.875  
   3.876  	have "dist (z m) (z n) \<le> c ^ n * d * (1 - c ^ (m - n)) / (1 - c)"
   3.877  	  using cf_z2[of n "m - n"] and `m>n` unfolding pos_le_divide_eq[OF `1-c>0`]
   3.878 -	  by (auto simp add: real_mult_commute dist_sym)
   3.879 +	  by (auto simp add: real_mult_commute dist_commute)
   3.880  	also have "\<dots> \<le> c ^ N * d * (1 - c ^ (m - n)) / (1 - c)"
   3.881  	  using mult_right_mono[OF * order_less_imp_le[OF **]]
   3.882  	  unfolding real_mult_assoc by auto
   3.883 @@ -5520,7 +5546,7 @@
   3.884  	proof(cases "n = m")
   3.885  	  case True thus ?thesis using `e>0` by auto
   3.886  	next
   3.887 -	  case False thus ?thesis using as and *[of n m] *[of m n] unfolding nat_neq_iff by (auto simp add: dist_sym)
   3.888 +	  case False thus ?thesis using as and *[of n m] *[of m n] unfolding nat_neq_iff by (auto simp add: dist_commute)
   3.889  	qed }
   3.890        thus ?thesis by auto
   3.891      qed
   3.892 @@ -5530,15 +5556,15 @@
   3.893  
   3.894    def e \<equiv> "dist (f x) x"
   3.895    have "e = 0" proof(rule ccontr)
   3.896 -    assume "e \<noteq> 0" hence "e>0" unfolding e_def using dist_pos_le[of "f x" x]
   3.897 -      by (metis dist_eq_0 dist_nz dist_sym e_def)
   3.898 +    assume "e \<noteq> 0" hence "e>0" unfolding e_def using zero_le_dist[of "f x" x]
   3.899 +      by (metis dist_eq_0_iff dist_nz e_def)
   3.900      then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
   3.901        using x[unfolded Lim_sequentially, THEN spec[where x="e/2"]] by auto
   3.902      hence N':"dist (z N) x < e / 2" by auto
   3.903  
   3.904      have *:"c * dist (z N) x \<le> dist (z N) x" unfolding mult_le_cancel_right2
   3.905 -      using dist_pos_le[of "z N" x] and c
   3.906 -      by (metis dist_eq_0 dist_nz dist_sym order_less_asym real_less_def)
   3.907 +      using zero_le_dist[of "z N" x] and c
   3.908 +      by (metis dist_eq_0_iff dist_nz order_less_asym real_less_def)
   3.909      have "dist (f (z N)) (f x) \<le> c * dist (z N) x" using lipschitz[THEN bspec[where x="z N"], THEN bspec[where x=x]]
   3.910        using z_in_s[of N] `x\<in>s` using c by auto
   3.911      also have "\<dots> < e / 2" using N' and c using * by auto
   3.912 @@ -5546,14 +5572,14 @@
   3.913        using N[THEN spec[where x="Suc N"]] and dist_triangle_half_r[of "z (Suc N)" "f x" e x]
   3.914        unfolding e_def by auto
   3.915    qed
   3.916 -  hence "f x = x" unfolding e_def and dist_eq_0 by auto
   3.917 +  hence "f x = x" unfolding e_def by auto
   3.918    moreover
   3.919    { fix y assume "f y = y" "y\<in>s"
   3.920      hence "dist x y \<le> c * dist x y" using lipschitz[THEN bspec[where x=x], THEN bspec[where x=y]]
   3.921        using `x\<in>s` and `f x = x` by auto
   3.922      hence "dist x y = 0" unfolding mult_le_cancel_right1
   3.923 -      using c and dist_pos_le[of x y] by auto
   3.924 -    hence "y = x" unfolding dist_eq_0 by auto
   3.925 +      using c and zero_le_dist[of x y] by auto
   3.926 +    hence "y = x" by auto
   3.927    }
   3.928    ultimately show ?thesis unfolding Bex1_def using `x\<in>s` by blast+
   3.929  qed
   3.930 @@ -5623,7 +5649,7 @@
   3.931      unfolding o_def and h_def a_def b_def  by auto
   3.932  
   3.933    { fix n::nat
   3.934 -    have *:"\<And>fx fy x 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
   3.935 +    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
   3.936      { fix x y ::"real^'a"
   3.937        have "dist (-x) (-y) = dist x y" unfolding dist_def
   3.938  	using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
   3.939 @@ -5637,7 +5663,7 @@
   3.940  	apply(erule_tac x="Na+Nb+n" in allE) apply simp
   3.941  	using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)"
   3.942            "-b"  "- f (r (Na + Nb + n)) y"]
   3.943 -	unfolding ** unfolding group_simps(12) by (auto simp add: dist_sym)
   3.944 +	unfolding ** unfolding group_simps(12) by (auto simp add: dist_commute)
   3.945        moreover
   3.946        have "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) \<ge> dist a b - dist (f n x) (f n y)"
   3.947  	using distf[of n "r (Na+Nb+n)", OF _ `x\<in>s` `y\<in>s`]
     4.1 --- a/src/HOL/RealVector.thy	Thu May 28 15:54:20 2009 +0200
     4.2 +++ b/src/HOL/RealVector.thy	Thu May 28 13:41:41 2009 -0700
     4.3 @@ -169,6 +169,11 @@
     4.4  lemmas scaleR_cancel_left = real_vector.scale_cancel_left
     4.5  lemmas scaleR_cancel_right = real_vector.scale_cancel_right
     4.6  
     4.7 +lemma scaleR_minus1_left [simp]:
     4.8 +  fixes x :: "'a::real_vector"
     4.9 +  shows "scaleR (-1) x = - x"
    4.10 +  using scaleR_minus_left [of 1 x] by simp
    4.11 +
    4.12  class real_algebra = real_vector + ring +
    4.13    assumes mult_scaleR_left [simp]: "scaleR a x * y = scaleR a (x * y)"
    4.14    and mult_scaleR_right [simp]: "x * scaleR a y = scaleR a (x * y)"
    4.15 @@ -633,6 +638,44 @@
    4.16  by (induct n) (simp_all add: norm_mult)
    4.17  
    4.18  
    4.19 +subsection {* Distance function *}
    4.20 +
    4.21 +(* TODO: There should be a metric_space class for this,
    4.22 +which should be a superclass of real_normed_vector. *)
    4.23 +
    4.24 +definition
    4.25 +  dist :: "'a::real_normed_vector \<Rightarrow> 'a \<Rightarrow> real"
    4.26 +where
    4.27 +  "dist x y = norm (x - y)"
    4.28 +
    4.29 +lemma zero_le_dist [simp]: "0 \<le> dist x y"
    4.30 +unfolding dist_def by (rule norm_ge_zero)
    4.31 +
    4.32 +lemma dist_eq_0_iff [simp]: "dist x y = 0 \<longleftrightarrow> x = y"
    4.33 +unfolding dist_def by simp
    4.34 +
    4.35 +lemma dist_self [simp]: "dist x x = 0"
    4.36 +unfolding dist_def by simp
    4.37 +
    4.38 +lemma zero_less_dist_iff: "0 < dist x y \<longleftrightarrow> x \<noteq> y"
    4.39 +by (simp add: less_le)
    4.40 +
    4.41 +lemma dist_not_less_zero [simp]: "\<not> dist x y < 0"
    4.42 +by (simp add: not_less)
    4.43 +
    4.44 +lemma dist_le_zero_iff [simp]: "dist x y \<le> 0 \<longleftrightarrow> x = y"
    4.45 +by (simp add: le_less)
    4.46 +
    4.47 +lemma dist_commute: "dist x y = dist y x"
    4.48 +unfolding dist_def by (rule norm_minus_commute)
    4.49 +
    4.50 +lemma dist_triangle: "dist x z \<le> dist x y + dist y z"
    4.51 +unfolding dist_def
    4.52 +apply (rule ord_eq_le_trans [OF _ norm_triangle_ineq])
    4.53 +apply (simp add: diff_minus)
    4.54 +done
    4.55 +
    4.56 +
    4.57  subsection {* Sign function *}
    4.58  
    4.59  lemma norm_sgn: