26166

1 
(* ID: $Id$


2 
Author: Tobias Nipkow, 2007


3 
*)


4 


5 
header "Lists as vectors"


6 


7 
theory ListVector

27487

8 
imports Plain "~~/src/HOL/List"

26166

9 
begin


10 


11 
text{* \noindent


12 
A vectorspace like structure of lists and arithmetic operations on them.


13 
Is only a vector space if restricted to lists of the same length. *}


14 


15 
text{* Multiplication with a scalar: *}


16 


17 
abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)


18 
where "x *\<^sub>s xs \<equiv> map (op * x) xs"


19 


20 
lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"


21 
by (induct xs) simp_all


22 


23 
subsection {* @{text"+"} and @{text""} *}


24 


25 
fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"


26 
where


27 
"zipwith0 f [] [] = []" 


28 
"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" 


29 
"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" 


30 
"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"


31 

27109

32 
instantiation list :: ("{zero, plus}") plus


33 
begin


34 


35 
definition


36 
list_add_def: "op + = zipwith0 (op +)"


37 


38 
instance ..


39 


40 
end


41 


42 
instantiation list :: ("{zero, uminus}") uminus


43 
begin

26166

44 

27109

45 
definition


46 
list_uminus_def: "uminus = map uminus"


47 


48 
instance ..


49 


50 
end

26166

51 

27109

52 
instantiation list :: ("{zero,minus}") minus


53 
begin


54 


55 
definition


56 
list_diff_def: "op  = zipwith0 (op )"


57 


58 
instance ..


59 


60 
end

26166

61 


62 
lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"


63 
by(induct ys) simp_all


64 


65 
lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"


66 
by (induct xs) (auto simp:list_add_def)


67 


68 
lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"


69 
by (induct xs) (auto simp:list_add_def)


70 


71 
lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"


72 
by(auto simp:list_add_def)


73 


74 
lemma list_diff_Nil[simp]: "[]  xs = (xs::'a::group_add list)"


75 
by (induct xs) (auto simp:list_diff_def list_uminus_def)


76 


77 
lemma list_diff_Nil2[simp]: "xs  [] = (xs::'a::group_add list)"


78 
by (induct xs) (auto simp:list_diff_def)


79 


80 
lemma list_diff_Cons_Cons[simp]: "(x#xs)  (y#ys) = (xy)#(xsys)"


81 
by (induct xs) (auto simp:list_diff_def)


82 


83 
lemma list_uminus_Cons[simp]: "(x#xs) = (x)#(xs)"


84 
by (induct xs) (auto simp:list_uminus_def)


85 


86 
lemma self_list_diff:


87 
"xs  xs = replicate (length(xs::'a::group_add list)) 0"


88 
by(induct xs) simp_all


89 


90 
lemma list_add_assoc: fixes xs :: "'a::monoid_add list"


91 
shows "(xs+ys)+zs = xs+(ys+zs)"


92 
apply(induct xs arbitrary: ys zs)


93 
apply simp


94 
apply(case_tac ys)


95 
apply(simp)


96 
apply(simp)


97 
apply(case_tac zs)


98 
apply(simp)


99 
apply(simp add:add_assoc)


100 
done


101 


102 
subsection "Inner product"


103 


104 
definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where


105 
"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"


106 


107 
lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"


108 
by(simp add:iprod_def)


109 


110 
lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"


111 
by(simp add:iprod_def)


112 


113 
lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"


114 
by(simp add:iprod_def)


115 


116 
lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"


117 
apply(induct cs arbitrary:xs)


118 
apply simp


119 
apply(case_tac xs) apply simp


120 
apply auto


121 
done


122 


123 
lemma iprod_uminus[simp]: "\<langle>xs,ys\<rangle> = \<langle>xs,ys\<rangle>"


124 
by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)


125 


126 
lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"


127 
apply(induct xs arbitrary: ys zs)


128 
apply (simp add: o_def split_def)


129 
apply(case_tac ys)


130 
apply simp


131 
apply(case_tac zs)


132 
apply (simp)


133 
apply(simp add:left_distrib)


134 
done


135 


136 
lemma iprod_left_diff_distrib: "\<langle>xs  ys, zs\<rangle> = \<langle>xs,zs\<rangle>  \<langle>ys,zs\<rangle>"


137 
apply(induct xs arbitrary: ys zs)


138 
apply (simp add: o_def split_def)


139 
apply(case_tac ys)


140 
apply simp


141 
apply(case_tac zs)


142 
apply (simp)


143 
apply(simp add:left_diff_distrib)


144 
done


145 


146 
lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"


147 
apply(induct xs arbitrary: ys)


148 
apply simp


149 
apply(case_tac ys)


150 
apply (simp)


151 
apply (simp add:right_distrib mult_assoc)


152 
done


153 


154 
end 