src/HOL/Library/ListVector.thy
 author nipkow Tue Sep 22 14:31:22 2015 +0200 (2015-09-22) changeset 61225 1a690dce8cfc parent 60500 903bb1495239 child 61585 a9599d3d7610 permissions -rw-r--r--
tuned references
1 (*  Author: Tobias Nipkow, 2007 *)
3 section \<open>Lists as vectors\<close>
5 theory ListVector
6 imports List Main
7 begin
9 text\<open>\noindent
10 A vector-space like structure of lists and arithmetic operations on them.
11 Is only a vector space if restricted to lists of the same length.\<close>
13 text\<open>Multiplication with a scalar:\<close>
15 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
16 where "x *\<^sub>s xs \<equiv> map (op * x) xs"
18 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
19 by (induct xs) simp_all
21 subsection \<open>@{text"+"} and @{text"-"}\<close>
23 fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
24 where
25 "zipwith0 f [] [] = []" |
26 "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
27 "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
28 "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
30 instantiation list :: ("{zero, plus}") plus
31 begin
33 definition
34   list_add_def: "op + = zipwith0 (op +)"
36 instance ..
38 end
40 instantiation list :: ("{zero, uminus}") uminus
41 begin
43 definition
44   list_uminus_def: "uminus = map uminus"
46 instance ..
48 end
50 instantiation list :: ("{zero,minus}") minus
51 begin
53 definition
54   list_diff_def: "op - = zipwith0 (op -)"
56 instance ..
58 end
60 lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
61 by(induct ys) simp_all
64 by (induct xs) (auto simp:list_add_def)
67 by (induct xs) (auto simp:list_add_def)
69 lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
72 lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
73 by (induct xs) (auto simp:list_diff_def list_uminus_def)
75 lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
76 by (induct xs) (auto simp:list_diff_def)
78 lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
79 by (induct xs) (auto simp:list_diff_def)
81 lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
82 by (induct xs) (auto simp:list_uminus_def)
84 lemma self_list_diff:
85   "xs - xs = replicate (length(xs::'a::group_add list)) 0"
86 by(induct xs) simp_all
89 shows "(xs+ys)+zs = xs+(ys+zs)"
90 apply(induct xs arbitrary: ys zs)
91  apply simp
92 apply(case_tac ys)
93  apply(simp)
94 apply(simp)
95 apply(case_tac zs)
96  apply(simp)
98 done
100 subsection "Inner product"
102 definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
103 "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
105 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
108 lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
111 lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
114 lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
115 apply(induct cs arbitrary:xs)
116  apply simp
117 apply(case_tac xs) apply simp
118 apply auto
119 done
121 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
122 by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
124 lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
125 apply(induct xs arbitrary: ys zs)
126 apply (simp add: o_def split_def)
127 apply(case_tac ys)
128 apply simp
129 apply(case_tac zs)
130 apply (simp)
132 done
134 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
135 apply(induct xs arbitrary: ys zs)
136 apply (simp add: o_def split_def)
137 apply(case_tac ys)
138 apply simp
139 apply(case_tac zs)
140 apply (simp)