1 (* Author: Tobias Nipkow, 2007 *) |
1 (* Author: Tobias Nipkow, 2007 *) |
2 |
2 |
3 section {* Lists as vectors *} |
3 section \<open>Lists as vectors\<close> |
4 |
4 |
5 theory ListVector |
5 theory ListVector |
6 imports List Main |
6 imports List Main |
7 begin |
7 begin |
8 |
8 |
9 text{* \noindent |
9 text\<open>\noindent |
10 A vector-space like structure of lists and arithmetic operations on them. |
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. *} |
11 Is only a vector space if restricted to lists of the same length.\<close> |
12 |
12 |
13 text{* Multiplication with a scalar: *} |
13 text\<open>Multiplication with a scalar:\<close> |
14 |
14 |
15 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70) |
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" |
16 where "x *\<^sub>s xs \<equiv> map (op * x) xs" |
17 |
17 |
18 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs" |
18 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs" |
19 by (induct xs) simp_all |
19 by (induct xs) simp_all |
20 |
20 |
21 subsection {* @{text"+"} and @{text"-"} *} |
21 subsection \<open>@{text"+"} and @{text"-"}\<close> |
22 |
22 |
23 fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
23 fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list" |
24 where |
24 where |
25 "zipwith0 f [] [] = []" | |
25 "zipwith0 f [] [] = []" | |
26 "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" | |
26 "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" | |