diff -r 8ef7ba78bf26 -r 0a3f9ee4117c src/HOL/Library/Convex_Euclidean_Space.thy
--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 15:54:20 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Thu May 28 13:41:41 2009 -0700
@@ -609,7 +609,7 @@
 	apply auto unfolding zero_less_divide_iff using n by simp  }  note * = this
 
     have "\<exists>x\<ge>0. x \<le> 1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e1 \<and> (1 - x) *s x1 + x *s x2 \<notin> e2"
-      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_sym)+
+      apply(rule connected_real_lemma) apply (simp add: `x1\<in>e1` `x2\<in>e2` dist_commute)+
       using * apply(simp add: dist_def)
       using as(1,2)[unfolded open_def] apply simp
       using as(1,2)[unfolded open_def] apply simp
@@ -1357,7 +1357,9 @@
 
 subsection {* Extremal points of a simplex are some vertices. *}
 
-lemma dist_increases_online: assumes "d \<noteq> 0"
+lemma dist_increases_online:
+  fixes a b d :: "real ^ 'n::finite"
+  assumes "d \<noteq> 0"
   shows "dist a (b + d) > dist a b \<or> dist a (b - d) > dist a b"
 proof(cases "a \<bullet> d - b \<bullet> d > 0")
   case True hence "0 < d \<bullet> d + (a \<bullet> d * 2 - b \<bullet> d * 2)" 
@@ -1409,7 +1411,7 @@
  	proof(erule_tac disjE)
 	  assume "dist a y < dist a (y + w *s (x - b))"
 	  hence "norm (y - a) < norm ((u + w) *s x + (v - w) *s b - a)"
-	    unfolding dist_sym[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
+	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
 	  moreover have "(u + w) *s x + (v - w) *s b \<in> convex hull insert x s"
 	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
 	    apply(rule_tac x="u + w" in exI) apply rule defer 
@@ -1418,7 +1420,7 @@
 	next
 	  assume "dist a y < dist a (y - w *s (x - b))"
 	  hence "norm (y - a) < norm ((u - w) *s x + (v + w) *s b - a)"
-	    unfolding dist_sym[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
+	    unfolding dist_commute[of a] unfolding dist_def obt(5) by (simp add: ring_simps)
 	  moreover have "(u - w) *s x + (v + w) *s b \<in> convex hull insert x s"
 	    unfolding convex_hull_insert[OF `s\<noteq>{}`] and mem_Collect_eq
 	    apply(rule_tac x="u - w" in exI) apply rule defer 
@@ -1437,7 +1439,7 @@
   have "convex hull s \<noteq> {}" using hull_subset[of s convex] and assms(2) by auto
   then obtain x where x:"x\<in>convex hull s" "\<forall>y\<in>convex hull s. norm (y - a) \<le> norm (x - a)"
     using distance_attains_sup[OF finite_imp_compact_convex_hull[OF assms(1)], of a]
-    unfolding dist_sym[of a] unfolding dist_def by auto
+    unfolding dist_commute[of a] unfolding dist_def by auto
   thus ?thesis proof(cases "x\<in>s")
     case False then obtain y where "y\<in>convex hull s" "norm (x - a) < norm (y - a)"
       using simplex_furthest_lt[OF assms(1), THEN bspec[where x=x]] and x(1) by auto
@@ -1513,6 +1515,7 @@
   qed(rule divide_pos_pos, auto) qed
 
 lemma closer_point_lemma:
+  fixes x y z :: "real ^ 'n::finite"
   assumes "(y - x) \<bullet> (z - x) > 0"
   shows "\<exists>u>0. u \<le> 1 \<and> dist (x + u *s (z - x)) y < dist x y"
 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)"
@@ -1526,7 +1529,7 @@
 proof(rule ccontr) assume "\<not> (a - x) \<bullet> (y - x) \<le> 0"
   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
   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
-  thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_sym field_simps) qed
+  thus False using assms(5)[THEN bspec[where x="?z"]] and u(3) by (auto simp add: dist_commute field_simps) qed
 
 lemma any_closest_point_unique:
   assumes "convex s" "closed s" "x \<in> s" "y \<in> s"
@@ -1592,7 +1595,7 @@
       using assms(1)[unfolded convex_alt] and y and `x\<in>s` and `y\<in>s` by auto
     assume "\<not> (y - z) \<bullet> y \<le> (y - z) \<bullet> x" then obtain v where
       "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
-    thus False using *[THEN spec[where x=v]] by(auto simp add: dist_sym field_simps)
+    thus False using *[THEN spec[where x=v]] by(auto simp add: dist_commute field_simps)
   qed auto
 qed
 
@@ -1613,7 +1616,7 @@
       then obtain u where "u>0" "u\<le>1" "dist (y + u *s (x - y)) z < dist y z" by auto
       thus False using y[THEN bspec[where x="y + u *s (x - y)"]]
 	using assms(1)[unfolded convex_alt, THEN bspec[where x=y]]
-	using `x\<in>s` `y\<in>s` by (auto simp add: dist_sym field_simps) qed
+	using `x\<in>s` `y\<in>s` by (auto simp add: dist_commute field_simps) qed
     moreover have "0 < norm (y - z) ^ 2" using `y\<in>s` `z\<notin>s` by auto
     hence "0 < (y - z) \<bullet> (y - z)" unfolding norm_pow_2 by simp
     ultimately show "(y - z) \<bullet> z + (norm (y - z))\<twosuperior> / 2 < (y - z) \<bullet> x"
@@ -2092,7 +2095,7 @@
     unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
     fix y assume "dist (u *s x) y < 1 - u"
     hence "inverse (1 - u) *s (y - u *s x) \<in> s"
-      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_sym dist_def
+      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_def
       unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_mul      
       apply (rule mult_left_le_imp_le[of "1 - u"])
       unfolding class_semiring.mul_a using `u<1` by auto
@@ -2420,8 +2423,8 @@
   thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using assms(1)[unfolded convex_on_def,rule_format, OF y z, of "1/2" "1/2"]
     using assms(2)[rule_format,OF y] assms(2)[rule_format,OF z] by(auto simp add:field_simps)
 next case False fix y assume "y\<in>cball x e" 
-  hence "dist x y < 0" using False unfolding mem_cball not_le by auto
-  thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using dist_pos_le[of x y] by auto qed
+  hence "dist x y < 0" using False unfolding mem_cball not_le by (auto simp del: dist_not_less_zero)
+  thus "\<bar>f y\<bar> \<le> b + 2 * \<bar>f x\<bar>" using zero_le_dist[of x y] by auto qed
 
 subsection {* Hence a convex function on an open set is continuous. *}
 
@@ -2498,7 +2501,7 @@
 lemma midpoint_eq_endpoint:
   "midpoint a b = a \<longleftrightarrow> a = (b::real^'n::finite)"
   "midpoint a b = b \<longleftrightarrow> a = b"
-  unfolding dist_eq_0[THEN sym] dist_midpoint by auto
+  unfolding dist_eq_0_iff[where 'a="real^'n", THEN sym] dist_midpoint by auto
 
 lemma convex_contains_segment:
   "convex s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. closed_segment a b \<subseteq> s)"
@@ -2544,7 +2547,7 @@
 lemma between:"between (a,b) (x::real^'n::finite) \<longleftrightarrow> dist a b = (dist a x) + (dist x b)"
 proof(cases "a = b")
   case True thus ?thesis unfolding between_def split_conv mem_def[of x, symmetric]
-    by(auto simp add:segment_refl dist_sym) next
+    by(auto simp add:segment_refl dist_commute) next
   case False hence Fal:"norm (a - b) \<noteq> 0" and Fal2: "norm (a - b) > 0" by auto 
   have *:"\<And>u. a - ((1 - u) *s a + u *s b) = u *s (a - b)" by auto
   show ?thesis unfolding between_def split_conv mem_def[of x, symmetric] closed_segment_def mem_Collect_eq