haftmann@30663: (*  Author: Tobias Nipkow, 2007 *)
nipkow@26166: 
haftmann@30663: header {* Lists as vectors *}
nipkow@26166: 
nipkow@26166: theory ListVector
haftmann@30663: imports List Main
nipkow@26166: begin
nipkow@26166: 
nipkow@26166: text{* \noindent
nipkow@26166: A vector-space like structure of lists and arithmetic operations on them.
nipkow@26166: Is only a vector space if restricted to lists of the same length. *}
nipkow@26166: 
nipkow@26166: text{* Multiplication with a scalar: *}
nipkow@26166: 
nipkow@26166: abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
nipkow@26166: where "x *\<^sub>s xs \<equiv> map (op * x) xs"
nipkow@26166: 
nipkow@26166: lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
nipkow@26166: by (induct xs) simp_all
nipkow@26166: 
nipkow@26166: subsection {* @{text"+"} and @{text"-"} *}
nipkow@26166: 
nipkow@26166: fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
nipkow@26166: where
nipkow@26166: "zipwith0 f [] [] = []" |
nipkow@26166: "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
nipkow@26166: "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
nipkow@26166: "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
nipkow@26166: 
haftmann@27109: instantiation list :: ("{zero, plus}") plus
haftmann@27109: begin
haftmann@27109: 
haftmann@27109: definition
haftmann@27109:   list_add_def: "op + = zipwith0 (op +)"
haftmann@27109: 
haftmann@27109: instance ..
haftmann@27109: 
haftmann@27109: end
haftmann@27109: 
haftmann@27109: instantiation list :: ("{zero, uminus}") uminus
haftmann@27109: begin
nipkow@26166: 
haftmann@27109: definition
haftmann@27109:   list_uminus_def: "uminus = map uminus"
haftmann@27109: 
haftmann@27109: instance ..
haftmann@27109: 
haftmann@27109: end
nipkow@26166: 
haftmann@27109: instantiation list :: ("{zero,minus}") minus
haftmann@27109: begin
haftmann@27109: 
haftmann@27109: definition
haftmann@27109:   list_diff_def: "op - = zipwith0 (op -)"
haftmann@27109: 
haftmann@27109: instance ..
haftmann@27109: 
haftmann@27109: end
nipkow@26166: 
nipkow@26166: lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
nipkow@26166: by(induct ys) simp_all
nipkow@26166: 
nipkow@26166: lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
nipkow@26166: by (induct xs) (auto simp:list_add_def)
nipkow@26166: 
nipkow@26166: lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
nipkow@26166: by (induct xs) (auto simp:list_add_def)
nipkow@26166: 
nipkow@26166: lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
nipkow@26166: by(auto simp:list_add_def)
nipkow@26166: 
nipkow@26166: lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
nipkow@26166: by (induct xs) (auto simp:list_diff_def list_uminus_def)
nipkow@26166: 
nipkow@26166: lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
nipkow@26166: by (induct xs) (auto simp:list_diff_def)
nipkow@26166: 
nipkow@26166: lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
nipkow@26166: by (induct xs) (auto simp:list_diff_def)
nipkow@26166: 
nipkow@26166: lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
nipkow@26166: by (induct xs) (auto simp:list_uminus_def)
nipkow@26166: 
nipkow@26166: lemma self_list_diff:
nipkow@26166:   "xs - xs = replicate (length(xs::'a::group_add list)) 0"
nipkow@26166: by(induct xs) simp_all
nipkow@26166: 
nipkow@26166: lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
nipkow@26166: shows "(xs+ys)+zs = xs+(ys+zs)"
nipkow@26166: apply(induct xs arbitrary: ys zs)
nipkow@26166:  apply simp
nipkow@26166: apply(case_tac ys)
nipkow@26166:  apply(simp)
nipkow@26166: apply(simp)
nipkow@26166: apply(case_tac zs)
nipkow@26166:  apply(simp)
haftmann@57512: apply(simp add: add.assoc)
nipkow@26166: done
nipkow@26166: 
nipkow@26166: subsection "Inner product"
nipkow@26166: 
nipkow@26166: definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
nipkow@26166: "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
nipkow@26166: 
nipkow@26166: lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
webertj@49961: by(simp add: iprod_def)
nipkow@26166: 
nipkow@26166: lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
webertj@49961: by(simp add: iprod_def)
nipkow@26166: 
nipkow@26166: lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
webertj@49961: by(simp add: iprod_def)
nipkow@26166: 
nipkow@26166: lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
nipkow@26166: apply(induct cs arbitrary:xs)
nipkow@26166:  apply simp
nipkow@26166: apply(case_tac xs) apply simp
nipkow@26166: apply auto
nipkow@26166: done
nipkow@26166: 
nipkow@26166: lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
nipkow@26166: by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
nipkow@26166: 
nipkow@26166: lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
nipkow@26166: apply(induct xs arbitrary: ys zs)
nipkow@26166: apply (simp add: o_def split_def)
nipkow@26166: apply(case_tac ys)
nipkow@26166: apply simp
nipkow@26166: apply(case_tac zs)
nipkow@26166: apply (simp)
webertj@49962: apply(simp add: distrib_right)
nipkow@26166: done
nipkow@26166: 
nipkow@26166: lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
nipkow@26166: apply(induct xs arbitrary: ys zs)
nipkow@26166: apply (simp add: o_def split_def)
nipkow@26166: apply(case_tac ys)
nipkow@26166: apply simp
nipkow@26166: apply(case_tac zs)
nipkow@26166: apply (simp)
webertj@49961: apply(simp add: left_diff_distrib)
nipkow@26166: done
nipkow@26166: 
nipkow@26166: lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
nipkow@26166: apply(induct xs arbitrary: ys)
nipkow@26166: apply simp
nipkow@26166: apply(case_tac ys)
nipkow@26166: apply (simp)
haftmann@57512: apply (simp add: distrib_left mult.assoc)
nipkow@26166: done
nipkow@26166: 
webertj@49961: end