src/HOL/Library/ListVector.thy
 author wenzelm Mon Dec 28 17:43:30 2015 +0100 (2015-12-28) changeset 61952 546958347e05 parent 61585 a9599d3d7610 child 63882 018998c00003 permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 (*  Author: Tobias Nipkow, 2007 *)

     2

     3 section \<open>Lists as vectors\<close>

     4

     5 theory ListVector

     6 imports List 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 (op * 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: "op + = zipwith0 (op +)"

    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: "op - = zipwith0 (op -)"

    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_listsum_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