src/HOL/Library/ListVector.thy
author haftmann
Tue Jun 10 15:31:01 2008 +0200 (2008-06-10)
changeset 27109 779e73b02cca
parent 26166 dbeab703a28d
child 27368 9f90ac19e32b
permissions -rw-r--r--
more instantiation
nipkow@26166
     1
(*  ID:         $Id$
nipkow@26166
     2
    Author:     Tobias Nipkow, 2007
nipkow@26166
     3
*)
nipkow@26166
     4
nipkow@26166
     5
header "Lists as vectors"
nipkow@26166
     6
nipkow@26166
     7
theory ListVector
nipkow@26166
     8
imports Main
nipkow@26166
     9
begin
nipkow@26166
    10
nipkow@26166
    11
text{* \noindent
nipkow@26166
    12
A vector-space like structure of lists and arithmetic operations on them.
nipkow@26166
    13
Is only a vector space if restricted to lists of the same length. *}
nipkow@26166
    14
nipkow@26166
    15
text{* Multiplication with a scalar: *}
nipkow@26166
    16
nipkow@26166
    17
abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
nipkow@26166
    18
where "x *\<^sub>s xs \<equiv> map (op * x) xs"
nipkow@26166
    19
nipkow@26166
    20
lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
nipkow@26166
    21
by (induct xs) simp_all
nipkow@26166
    22
nipkow@26166
    23
subsection {* @{text"+"} and @{text"-"} *}
nipkow@26166
    24
nipkow@26166
    25
fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
nipkow@26166
    26
where
nipkow@26166
    27
"zipwith0 f [] [] = []" |
nipkow@26166
    28
"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
nipkow@26166
    29
"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
nipkow@26166
    30
"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
nipkow@26166
    31
haftmann@27109
    32
instantiation list :: ("{zero, plus}") plus
haftmann@27109
    33
begin
haftmann@27109
    34
haftmann@27109
    35
definition
haftmann@27109
    36
  list_add_def: "op + = zipwith0 (op +)"
haftmann@27109
    37
haftmann@27109
    38
instance ..
haftmann@27109
    39
haftmann@27109
    40
end
haftmann@27109
    41
haftmann@27109
    42
instantiation list :: ("{zero, uminus}") uminus
haftmann@27109
    43
begin
nipkow@26166
    44
haftmann@27109
    45
definition
haftmann@27109
    46
  list_uminus_def: "uminus = map uminus"
haftmann@27109
    47
haftmann@27109
    48
instance ..
haftmann@27109
    49
haftmann@27109
    50
end
nipkow@26166
    51
haftmann@27109
    52
instantiation list :: ("{zero,minus}") minus
haftmann@27109
    53
begin
haftmann@27109
    54
haftmann@27109
    55
definition
haftmann@27109
    56
  list_diff_def: "op - = zipwith0 (op -)"
haftmann@27109
    57
haftmann@27109
    58
instance ..
haftmann@27109
    59
haftmann@27109
    60
end
nipkow@26166
    61
nipkow@26166
    62
lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
nipkow@26166
    63
by(induct ys) simp_all
nipkow@26166
    64
nipkow@26166
    65
lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
nipkow@26166
    66
by (induct xs) (auto simp:list_add_def)
nipkow@26166
    67
nipkow@26166
    68
lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
nipkow@26166
    69
by (induct xs) (auto simp:list_add_def)
nipkow@26166
    70
nipkow@26166
    71
lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
nipkow@26166
    72
by(auto simp:list_add_def)
nipkow@26166
    73
nipkow@26166
    74
lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
nipkow@26166
    75
by (induct xs) (auto simp:list_diff_def list_uminus_def)
nipkow@26166
    76
nipkow@26166
    77
lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
nipkow@26166
    78
by (induct xs) (auto simp:list_diff_def)
nipkow@26166
    79
nipkow@26166
    80
lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
nipkow@26166
    81
by (induct xs) (auto simp:list_diff_def)
nipkow@26166
    82
nipkow@26166
    83
lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
nipkow@26166
    84
by (induct xs) (auto simp:list_uminus_def)
nipkow@26166
    85
nipkow@26166
    86
lemma self_list_diff:
nipkow@26166
    87
  "xs - xs = replicate (length(xs::'a::group_add list)) 0"
nipkow@26166
    88
by(induct xs) simp_all
nipkow@26166
    89
nipkow@26166
    90
lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
nipkow@26166
    91
shows "(xs+ys)+zs = xs+(ys+zs)"
nipkow@26166
    92
apply(induct xs arbitrary: ys zs)
nipkow@26166
    93
 apply simp
nipkow@26166
    94
apply(case_tac ys)
nipkow@26166
    95
 apply(simp)
nipkow@26166
    96
apply(simp)
nipkow@26166
    97
apply(case_tac zs)
nipkow@26166
    98
 apply(simp)
nipkow@26166
    99
apply(simp add:add_assoc)
nipkow@26166
   100
done
nipkow@26166
   101
nipkow@26166
   102
subsection "Inner product"
nipkow@26166
   103
nipkow@26166
   104
definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
nipkow@26166
   105
"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
nipkow@26166
   106
nipkow@26166
   107
lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
nipkow@26166
   108
by(simp add:iprod_def)
nipkow@26166
   109
nipkow@26166
   110
lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
nipkow@26166
   111
by(simp add:iprod_def)
nipkow@26166
   112
nipkow@26166
   113
lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
nipkow@26166
   114
by(simp add:iprod_def)
nipkow@26166
   115
nipkow@26166
   116
lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
nipkow@26166
   117
apply(induct cs arbitrary:xs)
nipkow@26166
   118
 apply simp
nipkow@26166
   119
apply(case_tac xs) apply simp
nipkow@26166
   120
apply auto
nipkow@26166
   121
done
nipkow@26166
   122
nipkow@26166
   123
lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
nipkow@26166
   124
by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
nipkow@26166
   125
nipkow@26166
   126
lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
nipkow@26166
   127
apply(induct xs arbitrary: ys zs)
nipkow@26166
   128
apply (simp add: o_def split_def)
nipkow@26166
   129
apply(case_tac ys)
nipkow@26166
   130
apply simp
nipkow@26166
   131
apply(case_tac zs)
nipkow@26166
   132
apply (simp)
nipkow@26166
   133
apply(simp add:left_distrib)
nipkow@26166
   134
done
nipkow@26166
   135
nipkow@26166
   136
lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
nipkow@26166
   137
apply(induct xs arbitrary: ys zs)
nipkow@26166
   138
apply (simp add: o_def split_def)
nipkow@26166
   139
apply(case_tac ys)
nipkow@26166
   140
apply simp
nipkow@26166
   141
apply(case_tac zs)
nipkow@26166
   142
apply (simp)
nipkow@26166
   143
apply(simp add:left_diff_distrib)
nipkow@26166
   144
done
nipkow@26166
   145
nipkow@26166
   146
lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
nipkow@26166
   147
apply(induct xs arbitrary: ys)
nipkow@26166
   148
apply simp
nipkow@26166
   149
apply(case_tac ys)
nipkow@26166
   150
apply (simp)
nipkow@26166
   151
apply (simp add:right_distrib mult_assoc)
nipkow@26166
   152
done
nipkow@26166
   153
nipkow@26166
   154
end