|
1 (* ID: $Id$ |
|
2 Author: Tobias Nipkow, 2007 |
|
3 *) |
|
4 |
|
5 header "Lists as vectors" |
|
6 |
|
7 theory ListSpace |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 text{* \noindent |
|
12 A vector-space 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 |
|
32 instance list :: ("{zero,plus}")plus |
|
33 list_add_def : "op + \<equiv> zipwith0 (op +)" .. |
|
34 |
|
35 instance list :: ("{zero,uminus}")uminus |
|
36 list_uminus_def: "uminus \<equiv> map uminus" .. |
|
37 |
|
38 instance list :: ("{zero,minus}")minus |
|
39 list_diff_def: "op - \<equiv> zipwith0 (op -)" .. |
|
40 |
|
41 lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys" |
|
42 by(induct ys) simp_all |
|
43 |
|
44 |
|
45 lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)" |
|
46 by (induct xs) (auto simp:list_add_def) |
|
47 |
|
48 lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)" |
|
49 by (induct xs) (auto simp:list_add_def) |
|
50 |
|
51 lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)" |
|
52 by(auto simp:list_add_def) |
|
53 |
|
54 lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)" |
|
55 by (induct xs) (auto simp:list_diff_def list_uminus_def) |
|
56 |
|
57 lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)" |
|
58 by (induct xs) (auto simp:list_diff_def) |
|
59 |
|
60 lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)" |
|
61 by (induct xs) (auto simp:list_diff_def) |
|
62 |
|
63 lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)" |
|
64 by (induct xs) (auto simp:list_uminus_def) |
|
65 |
|
66 lemma self_list_diff: |
|
67 "xs - xs = replicate (length(xs::'a::group_add list)) 0" |
|
68 by(induct xs) simp_all |
|
69 |
|
70 lemma list_add_assoc: fixes xs :: "'a::monoid_add list" |
|
71 shows "(xs+ys)+zs = xs+(ys+zs)" |
|
72 apply(induct xs arbitrary: ys zs) |
|
73 apply simp |
|
74 apply(case_tac ys) |
|
75 apply(simp) |
|
76 apply(simp) |
|
77 apply(case_tac zs) |
|
78 apply(simp) |
|
79 apply(simp add:add_assoc) |
|
80 done |
|
81 |
|
82 subsection "Inner product" |
|
83 |
|
84 definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where |
|
85 "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)" |
|
86 |
|
87 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0" |
|
88 by(simp add:iprod_def) |
|
89 |
|
90 lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0" |
|
91 by(simp add:iprod_def) |
|
92 |
|
93 lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>" |
|
94 by(simp add:iprod_def) |
|
95 |
|
96 lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0" |
|
97 apply(induct cs arbitrary:xs) |
|
98 apply simp |
|
99 apply(case_tac xs) apply simp |
|
100 apply auto |
|
101 done |
|
102 |
|
103 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>" |
|
104 by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def) |
|
105 |
|
106 lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>" |
|
107 apply(induct xs arbitrary: ys zs) |
|
108 apply (simp add: o_def split_def) |
|
109 apply(case_tac ys) |
|
110 apply simp |
|
111 apply(case_tac zs) |
|
112 apply (simp) |
|
113 apply(simp add:left_distrib) |
|
114 done |
|
115 |
|
116 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>" |
|
117 apply(induct xs arbitrary: ys zs) |
|
118 apply (simp add: o_def split_def) |
|
119 apply(case_tac ys) |
|
120 apply simp |
|
121 apply(case_tac zs) |
|
122 apply (simp) |
|
123 apply(simp add:left_diff_distrib) |
|
124 done |
|
125 |
|
126 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>" |
|
127 apply(induct xs arbitrary: ys) |
|
128 apply simp |
|
129 apply(case_tac ys) |
|
130 apply (simp) |
|
131 apply (simp add:right_distrib mult_assoc) |
|
132 done |
|
133 |
|
134 end |