--- a/src/HOL/Library/Euclidean_Space.thy Wed May 27 21:46:50 2009 -0700
+++ b/src/HOL/Library/Euclidean_Space.thy Thu May 28 09:46:43 2009 +0200
@@ -109,10 +109,10 @@
text{* Also the scalar-vector multiplication. *}
-definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
+definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70)
where "c *s x = (\<chi> i. c * (x$i))"
-text{* Constant Vectors *}
+text{* Constant Vectors *}
definition "vec x = (\<chi> i. x)"
--- a/src/HOL/Library/Topology_Euclidean_Space.thy Wed May 27 21:46:50 2009 -0700
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Thu May 28 09:46:43 2009 +0200
@@ -4601,8 +4601,8 @@
def f == "\<lambda>n::nat. x + (inverse (real n + 1)) *s (?c - x)"
{ fix n assume fn:"f n < b \<longrightarrow> a < f n \<longrightarrow> f n = x" and xc:"x \<noteq> ?c"
have *:"0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1" unfolding inverse_le_1_iff by auto
- have "inverse (real n + 1) *s (1 / 2) *s (a + b) + (1 - inverse (real n + 1)) *s x =
- x + inverse (real n + 1) *s ((1 / 2) *s (a + b) - x)" by (auto simp add: vector_ssub_ldistrib vector_add_ldistrib field_simps vector_sadd_rdistrib[THEN sym])
+ have "(inverse (real n + 1)) *s ((1 / 2) *s (a + b)) + (1 - inverse (real n + 1)) *s x =
+ x + (inverse (real n + 1)) *s ((1 / 2 *s (a + b)) - x)" by (auto simp add: vector_ssub_ldistrib vector_add_ldistrib field_simps vector_sadd_rdistrib[THEN sym])
hence "f n < b" and "a < f n" using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *] unfolding f_def by auto
hence False using fn unfolding f_def using xc by(auto simp add: vector_mul_lcancel vector_ssub_ldistrib) }
moreover