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