fix real_vector, real_algebra instances
authorhuffman
Sat Feb 21 09:55:32 2009 -0800 (2009-02-21)
changeset 300397208c88df507
parent 30038 4a1fa865c57a
child 30040 e2cd1acda1ab
fix real_vector, real_algebra instances
src/HOL/Library/Euclidean_Space.thy
     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.19               [@{thm vector_add_def}, @{thm vector_mult_def},  
    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.40 +  vec_component vector_add_component vector_mult_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.107 -  apply (simp_all add: vector_sadd_rdistrib vector_add_ldistrib vector_smult_lid vector_smult_assoc scaleR_left_distrib mult_commute)
   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 @@
   1.132  apply (simp add: norm_eq_0)
   1.133  done
   1.134  
   1.135 -end
   1.136 \ No newline at end of file
   1.137 +end