src/HOL/Library/ListVector.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 69064 5840724b1d71
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (*  Author: Tobias Nipkow, 2007 *)
     2 
     3 section \<open>Lists as vectors\<close>
     4 
     5 theory ListVector
     6 imports Main
     7 begin
     8 
     9 text\<open>\noindent
    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.\<close>
    12 
    13 text\<open>Multiplication with a scalar:\<close>
    14 
    15 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
    16 where "x *\<^sub>s xs \<equiv> map ((*) x) xs"
    17 
    18 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
    19 by (induct xs) simp_all
    20 
    21 subsection \<open>\<open>+\<close> and \<open>-\<close>\<close>
    22 
    23 fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    24 where
    25 "zipwith0 f [] [] = []" |
    26 "zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
    27 "zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
    28 "zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
    29 
    30 instantiation list :: ("{zero, plus}") plus
    31 begin
    32 
    33 definition
    34   list_add_def: "(+) = zipwith0 (+)"
    35 
    36 instance ..
    37 
    38 end
    39 
    40 instantiation list :: ("{zero, uminus}") uminus
    41 begin
    42 
    43 definition
    44   list_uminus_def: "uminus = map uminus"
    45 
    46 instance ..
    47 
    48 end
    49 
    50 instantiation list :: ("{zero,minus}") minus
    51 begin
    52 
    53 definition
    54   list_diff_def: "(-) = zipwith0 (-)"
    55 
    56 instance ..
    57 
    58 end
    59 
    60 lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
    61 by(induct ys) simp_all
    62 
    63 lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
    64 by (induct xs) (auto simp:list_add_def)
    65 
    66 lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
    67 by (induct xs) (auto simp:list_add_def)
    68 
    69 lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
    70 by(auto simp:list_add_def)
    71 
    72 lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
    73 by (induct xs) (auto simp:list_diff_def list_uminus_def)
    74 
    75 lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
    76 by (induct xs) (auto simp:list_diff_def)
    77 
    78 lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
    79 by (induct xs) (auto simp:list_diff_def)
    80 
    81 lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
    82 by (induct xs) (auto simp:list_uminus_def)
    83 
    84 lemma self_list_diff:
    85   "xs - xs = replicate (length(xs::'a::group_add list)) 0"
    86 by(induct xs) simp_all
    87 
    88 lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
    89 shows "(xs+ys)+zs = xs+(ys+zs)"
    90 apply(induct xs arbitrary: ys zs)
    91  apply simp
    92 apply(case_tac ys)
    93  apply(simp)
    94 apply(simp)
    95 apply(case_tac zs)
    96  apply(simp)
    97 apply(simp add: add.assoc)
    98 done
    99 
   100 subsection "Inner product"
   101 
   102 definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
   103 "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
   104 
   105 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
   106 by(simp add: iprod_def)
   107 
   108 lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
   109 by(simp add: iprod_def)
   110 
   111 lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
   112 by(simp add: iprod_def)
   113 
   114 lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
   115 apply(induct cs arbitrary:xs)
   116  apply simp
   117 apply(case_tac xs) apply simp
   118 apply auto
   119 done
   120 
   121 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
   122 by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)
   123 
   124 lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
   125 apply(induct xs arbitrary: ys zs)
   126 apply (simp add: o_def split_def)
   127 apply(case_tac ys)
   128 apply simp
   129 apply(case_tac zs)
   130 apply (simp)
   131 apply(simp add: distrib_right)
   132 done
   133 
   134 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
   135 apply(induct xs arbitrary: ys zs)
   136 apply (simp add: o_def split_def)
   137 apply(case_tac ys)
   138 apply simp
   139 apply(case_tac zs)
   140 apply (simp)
   141 apply(simp add: left_diff_distrib)
   142 done
   143 
   144 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
   145 apply(induct xs arbitrary: ys)
   146 apply simp
   147 apply(case_tac ys)
   148 apply (simp)
   149 apply (simp add: distrib_left mult.assoc)
   150 done
   151 
   152 end