author huffman Sat, 21 Feb 2009 09:55:32 -0800 changeset 30039 7208c88df507 parent 30038 4a1fa865c57a child 30040 e2cd1acda1ab
fix real_vector, real_algebra instances
```--- a/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 09:17:33 2009 -0800
+++ b/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 09:55:32 2009 -0800
@@ -84,7 +84,13 @@
instance by (intro_classes)
end

-text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
+instantiation "^" :: (scaleR, type) scaleR
+begin
+definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x\$i)))"
+instance ..
+end
+
+text{* Also the scalar-vector multiplication. *}

definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
where "c *s x = (\<chi> i. c * (x\$i))"
@@ -118,6 +124,7 @@
@{thm vector_minus_def}, @{thm vector_uminus_def},
@{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
+              @{thm vector_scaleR_def},
@{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]
fun vector_arith_tac ths =
simp_tac ss1
@@ -166,9 +173,18 @@
shows "(- x)\$i = - (x\$i)"
using i by vector

+lemma vector_scaleR_component:
+  fixes x :: "'a::scaleR ^ 'n"
+  assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
+  shows "(scaleR r x)\$i = scaleR r (x\$i)"
+  using i by vector
+
lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector

-lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component cond_component
+lemmas vector_component =
+  vector_smult_component vector_minus_component vector_uminus_component
+  vector_scaleR_component cond_component

subsection {* Some frequently useful arithmetic lemmas over vectors. *}

@@ -199,6 +215,9 @@
apply (intro_classes)
by (vector Cart_eq)

+instance "^" :: (real_vector, type) real_vector
+  by default (vector scaleR_left_distrib scaleR_right_distrib)+
+
instance "^" :: (semigroup_mult,type) semigroup_mult
apply (intro_classes) by (vector mult_assoc)

@@ -242,6 +261,18 @@
instance "^" :: (ring,type) ring by (intro_classes)
instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
+
+instance "^" :: (ring_1,type) ring_1 ..
+
+instance "^" :: (real_algebra,type) real_algebra
+  apply intro_classes
+  apply (simp_all add: vector_scaleR_def ring_simps)
+  apply vector
+  apply vector
+  done
+
+instance "^" :: (real_algebra_1,type) real_algebra_1 ..
+
lemma of_nat_index:
"i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n"
apply (induct n)
@@ -290,8 +321,7 @@
qed

instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
-  (* FIXME!!! Why does the axclass package complain here !!*)
-(* instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes *)
+instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes

lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
by (vector mult_assoc)
@@ -936,45 +966,6 @@
using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
by simp

-instantiation "^" :: ("{scaleR, one, times}",type) scaleR
-begin
-
-definition vector_scaleR_def: "(scaleR :: real \<Rightarrow> 'a ^'b \<Rightarrow> 'a ^'b) \<equiv> (\<lambda> c x . (scaleR c 1) *s x)"
-instance ..
-end
-
-instantiation "^" :: ("ring_1",type) ring_1
-begin
-instance by intro_classes
-end
-
-instantiation "^" :: (real_algebra_1,type) real_vector
-begin
-
-instance
-  apply intro_classes
-  done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra
-begin
-
-instance
-  apply intro_classes
-  apply (simp_all add: vector_scaleR_def ring_simps)
-  apply vector
-  apply vector
-  done
-end
-
-instantiation "^" :: (real_algebra_1,type) real_algebra_1
-begin
-
-instance ..
-end
-
lemma setsum_vmul:
fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
assumes fS: "finite S"
@@ -5168,4 +5159,4 @@