src/HOL/Library/ListVector.thy
author wenzelm
Wed, 08 Mar 2017 10:50:59 +0100
changeset 65151 a7394aa4d21c
parent 63882 018998c00003
child 66453 cc19f7ca2ed6
permissions -rw-r--r--
tuned proofs;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
30663
0b6aff7451b2 Main is (Complex_Main) base entry point in library theories
haftmann
parents: 27487
diff changeset
     1
(*  Author: Tobias Nipkow, 2007 *)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
     2
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     3
section \<open>Lists as vectors\<close>
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
     4
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
     5
theory ListVector
30663
0b6aff7451b2 Main is (Complex_Main) base entry point in library theories
haftmann
parents: 27487
diff changeset
     6
imports List Main
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
     7
begin
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
     8
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     9
text\<open>\noindent
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    10
A vector-space like structure of lists and arithmetic operations on them.
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    11
Is only a vector space if restricted to lists of the same length.\<close>
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    12
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
    13
text\<open>Multiplication with a scalar:\<close>
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    14
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    15
abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    16
where "x *\<^sub>s xs \<equiv> map (op * x) xs"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    17
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    18
lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    19
by (induct xs) simp_all
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    20
61585
a9599d3d7610 isabelle update_cartouches -c -t;
wenzelm
parents: 60500
diff changeset
    21
subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    22
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    23
fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    24
where
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    25
"zipwith0 f [] [] = []" |
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    26
"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    27
"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    28
"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    29
27109
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    30
instantiation list :: ("{zero, plus}") plus
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    31
begin
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    32
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    33
definition
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    34
  list_add_def: "op + = zipwith0 (op +)"
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    35
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    36
instance ..
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    37
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    38
end
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    39
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    40
instantiation list :: ("{zero, uminus}") uminus
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    41
begin
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    42
27109
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    43
definition
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    44
  list_uminus_def: "uminus = map uminus"
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    45
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    46
instance ..
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    47
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    48
end
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    49
27109
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    50
instantiation list :: ("{zero,minus}") minus
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    51
begin
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    52
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    53
definition
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    54
  list_diff_def: "op - = zipwith0 (op -)"
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    55
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    56
instance ..
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    57
779e73b02cca more instantiation
haftmann
parents: 26166
diff changeset
    58
end
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    59
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    60
lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    61
by(induct ys) simp_all
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    62
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    63
lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    64
by (induct xs) (auto simp:list_add_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    65
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    66
lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    67
by (induct xs) (auto simp:list_add_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    68
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    69
lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    70
by(auto simp:list_add_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    71
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    72
lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    73
by (induct xs) (auto simp:list_diff_def list_uminus_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    74
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    75
lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    76
by (induct xs) (auto simp:list_diff_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    77
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    78
lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    79
by (induct xs) (auto simp:list_diff_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    80
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    81
lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    82
by (induct xs) (auto simp:list_uminus_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    83
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    84
lemma self_list_diff:
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    85
  "xs - xs = replicate (length(xs::'a::group_add list)) 0"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    86
by(induct xs) simp_all
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    87
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    88
lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    89
shows "(xs+ys)+zs = xs+(ys+zs)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    90
apply(induct xs arbitrary: ys zs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    91
 apply simp
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    92
apply(case_tac ys)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    93
 apply(simp)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    94
apply(simp)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    95
apply(case_tac zs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    96
 apply(simp)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 49962
diff changeset
    97
apply(simp add: add.assoc)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    98
done
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
    99
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   100
subsection "Inner product"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   101
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   102
definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   103
"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   104
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   105
lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
49961
webertj
parents: 30663
diff changeset
   106
by(simp add: iprod_def)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   107
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   108
lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
49961
webertj
parents: 30663
diff changeset
   109
by(simp add: iprod_def)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   110
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   111
lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
49961
webertj
parents: 30663
diff changeset
   112
by(simp add: iprod_def)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   113
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   114
lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   115
apply(induct cs arbitrary:xs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   116
 apply simp
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   117
apply(case_tac xs) apply simp
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   118
apply auto
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   119
done
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   120
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   121
lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
63882
018998c00003 renamed listsum -> sum_list, listprod ~> prod_list
nipkow
parents: 61585
diff changeset
   122
by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   123
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   124
lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   125
apply(induct xs arbitrary: ys zs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   126
apply (simp add: o_def split_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   127
apply(case_tac ys)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   128
apply simp
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   129
apply(case_tac zs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   130
apply (simp)
49962
a8cc904a6820 Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents: 49961
diff changeset
   131
apply(simp add: distrib_right)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   132
done
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   133
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   134
lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   135
apply(induct xs arbitrary: ys zs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   136
apply (simp add: o_def split_def)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   137
apply(case_tac ys)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   138
apply simp
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   139
apply(case_tac zs)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   140
apply (simp)
49961
webertj
parents: 30663
diff changeset
   141
apply(simp add: left_diff_distrib)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   142
done
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   143
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   144
lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   145
apply(induct xs arbitrary: ys)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   146
apply simp
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   147
apply(case_tac ys)
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   148
apply (simp)
57512
cc97b347b301 reduced name variants for assoc and commute on plus and mult
haftmann
parents: 49962
diff changeset
   149
apply (simp add: distrib_left mult.assoc)
26166
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   150
done
dbeab703a28d Renamed ListSpace to ListVector
nipkow
parents:
diff changeset
   151
49961
webertj
parents: 30663
diff changeset
   152
end