author himmelma Thu, 28 May 2009 09:46:43 +0200 changeset 31275 1ba01cdd9a9a parent 31272 703183ff0926 child 31276 f6427bc40421
Changed prioriy of vector_scalar_mult
```--- 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```