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