src/HOL/Library/ListVector.thy
 author nipkow Wed Feb 27 18:01:10 2008 +0100 (2008-02-27) changeset 26166 dbeab703a28d child 27109 779e73b02cca permissions -rw-r--r--
Renamed ListSpace to ListVector
     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 instance list :: ("{zero,plus}")plus

    33 list_add_def : "op + \<equiv> zipwith0 (op +)" ..

    34

    35 instance list :: ("{zero,uminus}")uminus

    36 list_uminus_def: "uminus \<equiv> map uminus" ..

    37

    38 instance list :: ("{zero,minus}")minus

    39 list_diff_def: "op - \<equiv> zipwith0 (op -)" ..

    40

    41 lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"

    42 by(induct ys) simp_all

    43

    44

    45 lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"

    46 by (induct xs) (auto simp:list_add_def)

    47

    48 lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"

    49 by (induct xs) (auto simp:list_add_def)

    50

    51 lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"

    52 by(auto simp:list_add_def)

    53

    54 lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"

    55 by (induct xs) (auto simp:list_diff_def list_uminus_def)

    56

    57 lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"

    58 by (induct xs) (auto simp:list_diff_def)

    59

    60 lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"

    61 by (induct xs) (auto simp:list_diff_def)

    62

    63 lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"

    64 by (induct xs) (auto simp:list_uminus_def)

    65

    66 lemma self_list_diff:

    67   "xs - xs = replicate (length(xs::'a::group_add list)) 0"

    68 by(induct xs) simp_all

    69

    70 lemma list_add_assoc: fixes xs :: "'a::monoid_add list"

    71 shows "(xs+ys)+zs = xs+(ys+zs)"

    72 apply(induct xs arbitrary: ys zs)

    73  apply simp

    74 apply(case_tac ys)

    75  apply(simp)

    76 apply(simp)

    77 apply(case_tac zs)

    78  apply(simp)

    79 apply(simp add:add_assoc)

    80 done

    81

    82 subsection "Inner product"

    83

    84 definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where

    85 "\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"

    86

    87 lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"

    88 by(simp add:iprod_def)

    89

    90 lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"

    91 by(simp add:iprod_def)

    92

    93 lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"

    94 by(simp add:iprod_def)

    95

    96 lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"

    97 apply(induct cs arbitrary:xs)

    98  apply simp

    99 apply(case_tac xs) apply simp

   100 apply auto

   101 done

   102

   103 lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"

   104 by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)

   105

   106 lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"

   107 apply(induct xs arbitrary: ys zs)

   108 apply (simp add: o_def split_def)

   109 apply(case_tac ys)

   110 apply simp

   111 apply(case_tac zs)

   112 apply (simp)

   113 apply(simp add:left_distrib)

   114 done

   115

   116 lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"

   117 apply(induct xs arbitrary: ys zs)

   118 apply (simp add: o_def split_def)

   119 apply(case_tac ys)

   120 apply simp

   121 apply(case_tac zs)

   122 apply (simp)

   123 apply(simp add:left_diff_distrib)

   124 done

   125

   126 lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"

   127 apply(induct xs arbitrary: ys)

   128 apply simp

   129 apply(case_tac ys)

   130 apply (simp)

   131 apply (simp add:right_distrib mult_assoc)

   132 done

   133

   134 end