author huffman Sat Feb 21 09:55:32 2009 -0800 (2009-02-21) changeset 30039 7208c88df507 parent 30038 4a1fa865c57a child 30040 e2cd1acda1ab
fix real_vector, real_algebra instances
```     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 09:17:33 2009 -0800
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 09:55:32 2009 -0800
1.3 @@ -84,7 +84,13 @@
1.4  instance by (intro_classes)
1.5  end
1.6
1.7 -text{* Also the scalar-vector multiplication. FIXME: We should unify this with the scalar multiplication in @{text real_vector} *}
1.8 +instantiation "^" :: (scaleR, type) scaleR
1.9 +begin
1.10 +definition vector_scaleR_def: "scaleR = (\<lambda> r x.  (\<chi> i. scaleR r (x\$i)))"
1.11 +instance ..
1.12 +end
1.13 +
1.14 +text{* Also the scalar-vector multiplication. *}
1.15
1.16  definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'n" (infixr "*s" 75)
1.17    where "c *s x = (\<chi> i. c * (x\$i))"
1.18 @@ -118,6 +124,7 @@
1.20                @{thm vector_minus_def}, @{thm vector_uminus_def},
1.21                @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def},
1.22 +              @{thm vector_scaleR_def},
1.23                @{thm Cart_lambda_beta'}, @{thm vector_scalar_mult_def}]
1.24   fun vector_arith_tac ths =
1.25     simp_tac ss1
1.26 @@ -166,9 +173,18 @@
1.27    shows "(- x)\$i = - (x\$i)"
1.28    using i by vector
1.29
1.30 +lemma vector_scaleR_component:
1.31 +  fixes x :: "'a::scaleR ^ 'n"
1.32 +  assumes i: "i \<in> {1 .. dimindex(UNIV :: 'n set)}"
1.33 +  shows "(scaleR r x)\$i = scaleR r (x\$i)"
1.34 +  using i by vector
1.35 +
1.36  lemma cond_component: "(if b then x else y)\$i = (if b then x\$i else y\$i)" by vector
1.37
1.38 -lemmas vector_component = vec_component vector_add_component vector_mult_component vector_smult_component vector_minus_component vector_uminus_component cond_component
1.39 +lemmas vector_component =
1.41 +  vector_smult_component vector_minus_component vector_uminus_component
1.42 +  vector_scaleR_component cond_component
1.43
1.44  subsection {* Some frequently useful arithmetic lemmas over vectors. *}
1.45
1.46 @@ -199,6 +215,9 @@
1.47    apply (intro_classes)
1.48    by (vector Cart_eq)
1.49
1.50 +instance "^" :: (real_vector, type) real_vector
1.51 +  by default (vector scaleR_left_distrib scaleR_right_distrib)+
1.52 +
1.53  instance "^" :: (semigroup_mult,type) semigroup_mult
1.54    apply (intro_classes) by (vector mult_assoc)
1.55
1.56 @@ -242,6 +261,18 @@
1.57  instance "^" :: (ring,type) ring by (intro_classes)
1.58  instance "^" :: (semiring_1_cancel,type) semiring_1_cancel by (intro_classes)
1.59  instance "^" :: (comm_semiring_1,type) comm_semiring_1 by (intro_classes)
1.60 +
1.61 +instance "^" :: (ring_1,type) ring_1 ..
1.62 +
1.63 +instance "^" :: (real_algebra,type) real_algebra
1.64 +  apply intro_classes
1.65 +  apply (simp_all add: vector_scaleR_def ring_simps)
1.66 +  apply vector
1.67 +  apply vector
1.68 +  done
1.69 +
1.70 +instance "^" :: (real_algebra_1,type) real_algebra_1 ..
1.71 +
1.72  lemma of_nat_index:
1.73    "i\<in>{1 .. dimindex (UNIV :: 'n set)} \<Longrightarrow> (of_nat n :: 'a::semiring_1 ^'n)\$i = of_nat n"
1.74    apply (induct n)
1.75 @@ -290,8 +321,7 @@
1.76  qed
1.77
1.78  instance "^" :: (comm_ring_1,type) comm_ring_1 by intro_classes
1.79 -  (* FIXME!!! Why does the axclass package complain here !!*)
1.80 -(* instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes *)
1.81 +instance "^" :: (ring_char_0,type) ring_char_0 by intro_classes
1.82
1.83  lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
1.84    by (vector mult_assoc)
1.85 @@ -936,45 +966,6 @@
1.86    using real_setsum_norm_le[OF fS K] setsum_constant[symmetric]
1.87    by simp
1.88
1.89 -instantiation "^" :: ("{scaleR, one, times}",type) scaleR
1.90 -begin
1.91 -
1.92 -definition vector_scaleR_def: "(scaleR :: real \<Rightarrow> 'a ^'b \<Rightarrow> 'a ^'b) \<equiv> (\<lambda> c x . (scaleR c 1) *s x)"
1.93 -instance ..
1.94 -end
1.95 -
1.96 -instantiation "^" :: ("ring_1",type) ring_1
1.97 -begin
1.98 -instance by intro_classes
1.99 -end
1.100 -
1.101 -instantiation "^" :: (real_algebra_1,type) real_vector
1.102 -begin
1.103 -
1.104 -instance
1.105 -  apply intro_classes
1.106 -  apply (simp_all  add: vector_scaleR_def)
1.108 -  done
1.109 -end
1.110 -
1.111 -instantiation "^" :: (real_algebra_1,type) real_algebra
1.112 -begin
1.113 -
1.114 -instance
1.115 -  apply intro_classes
1.116 -  apply (simp_all add: vector_scaleR_def ring_simps)
1.117 -  apply vector
1.118 -  apply vector
1.119 -  done
1.120 -end
1.121 -
1.122 -instantiation "^" :: (real_algebra_1,type) real_algebra_1
1.123 -begin
1.124 -
1.125 -instance ..
1.126 -end
1.127 -
1.128  lemma setsum_vmul:
1.129    fixes f :: "'a \<Rightarrow> 'b::{real_normed_vector,semiring, mult_zero}"
1.130    assumes fS: "finite S"
1.131 @@ -5168,4 +5159,4 @@