Renamed ListSpace to ListVector
authornipkow
Wed Feb 27 18:01:10 2008 +0100 (2008-02-27)
changeset 26166dbeab703a28d
parent 26165 3c0c69a65943
child 26167 ccc9007a7164
Renamed ListSpace to ListVector
src/HOL/Library/ListSpace.thy
src/HOL/Library/ListVector.thy
     1.1 --- a/src/HOL/Library/ListSpace.thy	Wed Feb 27 16:41:36 2008 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,134 +0,0 @@
     1.4 -(*  ID:         $Id$
     1.5 -    Author:     Tobias Nipkow, 2007
     1.6 -*)
     1.7 -
     1.8 -header "Lists as vectors"
     1.9 -
    1.10 -theory ListSpace
    1.11 -imports Main
    1.12 -begin
    1.13 -
    1.14 -text{* \noindent
    1.15 -A vector-space like structure of lists and arithmetic operations on them.
    1.16 -Is only a vector space if restricted to lists of the same length. *}
    1.17 -
    1.18 -text{* Multiplication with a scalar: *}
    1.19 -
    1.20 -abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
    1.21 -where "x *\<^sub>s xs \<equiv> map (op * x) xs"
    1.22 -
    1.23 -lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
    1.24 -by (induct xs) simp_all
    1.25 -
    1.26 -subsection {* @{text"+"} and @{text"-"} *}
    1.27 -
    1.28 -fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    1.29 -where
    1.30 -"zipwith0 f [] [] = []" |
    1.31 -"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
    1.32 -"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
    1.33 -"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
    1.34 -
    1.35 -instance list :: ("{zero,plus}")plus
    1.36 -list_add_def : "op + \<equiv> zipwith0 (op +)" ..
    1.37 -
    1.38 -instance list :: ("{zero,uminus}")uminus
    1.39 -list_uminus_def: "uminus \<equiv> map uminus" ..
    1.40 -
    1.41 -instance list :: ("{zero,minus}")minus
    1.42 -list_diff_def: "op - \<equiv> zipwith0 (op -)" ..
    1.43 -
    1.44 -lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
    1.45 -by(induct ys) simp_all
    1.46 -
    1.47 -
    1.48 -lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
    1.49 -by (induct xs) (auto simp:list_add_def)
    1.50 -
    1.51 -lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
    1.52 -by (induct xs) (auto simp:list_add_def)
    1.53 -
    1.54 -lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
    1.55 -by(auto simp:list_add_def)
    1.56 -
    1.57 -lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
    1.58 -by (induct xs) (auto simp:list_diff_def list_uminus_def)
    1.59 -
    1.60 -lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
    1.61 -by (induct xs) (auto simp:list_diff_def)
    1.62 -
    1.63 -lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
    1.64 -by (induct xs) (auto simp:list_diff_def)
    1.65 -
    1.66 -lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
    1.67 -by (induct xs) (auto simp:list_uminus_def)
    1.68 -
    1.69 -lemma self_list_diff:
    1.70 -  "xs - xs = replicate (length(xs::'a::group_add list)) 0"
    1.71 -by(induct xs) simp_all
    1.72 -
    1.73 -lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
    1.74 -shows "(xs+ys)+zs = xs+(ys+zs)"
    1.75 -apply(induct xs arbitrary: ys zs)
    1.76 - apply simp
    1.77 -apply(case_tac ys)
    1.78 - apply(simp)
    1.79 -apply(simp)
    1.80 -apply(case_tac zs)
    1.81 - apply(simp)
    1.82 -apply(simp add:add_assoc)
    1.83 -done
    1.84 -
    1.85 -subsection "Inner product"
    1.86 -
    1.87 -definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
    1.88 -"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
    1.89 -
    1.90 -lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
    1.91 -by(simp add:iprod_def)
    1.92 -
    1.93 -lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
    1.94 -by(simp add:iprod_def)
    1.95 -
    1.96 -lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
    1.97 -by(simp add:iprod_def)
    1.98 -
    1.99 -lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
   1.100 -apply(induct cs arbitrary:xs)
   1.101 - apply simp
   1.102 -apply(case_tac xs) apply simp
   1.103 -apply auto
   1.104 -done
   1.105 -
   1.106 -lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
   1.107 -by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
   1.108 -
   1.109 -lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
   1.110 -apply(induct xs arbitrary: ys zs)
   1.111 -apply (simp add: o_def split_def)
   1.112 -apply(case_tac ys)
   1.113 -apply simp
   1.114 -apply(case_tac zs)
   1.115 -apply (simp)
   1.116 -apply(simp add:left_distrib)
   1.117 -done
   1.118 -
   1.119 -lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
   1.120 -apply(induct xs arbitrary: ys zs)
   1.121 -apply (simp add: o_def split_def)
   1.122 -apply(case_tac ys)
   1.123 -apply simp
   1.124 -apply(case_tac zs)
   1.125 -apply (simp)
   1.126 -apply(simp add:left_diff_distrib)
   1.127 -done
   1.128 -
   1.129 -lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
   1.130 -apply(induct xs arbitrary: ys)
   1.131 -apply simp
   1.132 -apply(case_tac ys)
   1.133 -apply (simp)
   1.134 -apply (simp add:right_distrib mult_assoc)
   1.135 -done
   1.136 -
   1.137 -end
   1.138 \ No newline at end of file
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/ListVector.thy	Wed Feb 27 18:01:10 2008 +0100
     2.3 @@ -0,0 +1,134 @@
     2.4 +(*  ID:         $Id$
     2.5 +    Author:     Tobias Nipkow, 2007
     2.6 +*)
     2.7 +
     2.8 +header "Lists as vectors"
     2.9 +
    2.10 +theory ListVector
    2.11 +imports Main
    2.12 +begin
    2.13 +
    2.14 +text{* \noindent
    2.15 +A vector-space like structure of lists and arithmetic operations on them.
    2.16 +Is only a vector space if restricted to lists of the same length. *}
    2.17 +
    2.18 +text{* Multiplication with a scalar: *}
    2.19 +
    2.20 +abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70)
    2.21 +where "x *\<^sub>s xs \<equiv> map (op * x) xs"
    2.22 +
    2.23 +lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs"
    2.24 +by (induct xs) simp_all
    2.25 +
    2.26 +subsection {* @{text"+"} and @{text"-"} *}
    2.27 +
    2.28 +fun zipwith0 :: "('a::zero \<Rightarrow> 'b::zero \<Rightarrow> 'c) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'c list"
    2.29 +where
    2.30 +"zipwith0 f [] [] = []" |
    2.31 +"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |
    2.32 +"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |
    2.33 +"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"
    2.34 +
    2.35 +instance list :: ("{zero,plus}")plus
    2.36 +list_add_def : "op + \<equiv> zipwith0 (op +)" ..
    2.37 +
    2.38 +instance list :: ("{zero,uminus}")uminus
    2.39 +list_uminus_def: "uminus \<equiv> map uminus" ..
    2.40 +
    2.41 +instance list :: ("{zero,minus}")minus
    2.42 +list_diff_def: "op - \<equiv> zipwith0 (op -)" ..
    2.43 +
    2.44 +lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
    2.45 +by(induct ys) simp_all
    2.46 +
    2.47 +
    2.48 +lemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"
    2.49 +by (induct xs) (auto simp:list_add_def)
    2.50 +
    2.51 +lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"
    2.52 +by (induct xs) (auto simp:list_add_def)
    2.53 +
    2.54 +lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"
    2.55 +by(auto simp:list_add_def)
    2.56 +
    2.57 +lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"
    2.58 +by (induct xs) (auto simp:list_diff_def list_uminus_def)
    2.59 +
    2.60 +lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"
    2.61 +by (induct xs) (auto simp:list_diff_def)
    2.62 +
    2.63 +lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"
    2.64 +by (induct xs) (auto simp:list_diff_def)
    2.65 +
    2.66 +lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"
    2.67 +by (induct xs) (auto simp:list_uminus_def)
    2.68 +
    2.69 +lemma self_list_diff:
    2.70 +  "xs - xs = replicate (length(xs::'a::group_add list)) 0"
    2.71 +by(induct xs) simp_all
    2.72 +
    2.73 +lemma list_add_assoc: fixes xs :: "'a::monoid_add list"
    2.74 +shows "(xs+ys)+zs = xs+(ys+zs)"
    2.75 +apply(induct xs arbitrary: ys zs)
    2.76 + apply simp
    2.77 +apply(case_tac ys)
    2.78 + apply(simp)
    2.79 +apply(simp)
    2.80 +apply(case_tac zs)
    2.81 + apply(simp)
    2.82 +apply(simp add:add_assoc)
    2.83 +done
    2.84 +
    2.85 +subsection "Inner product"
    2.86 +
    2.87 +definition iprod :: "'a::ring list \<Rightarrow> 'a list \<Rightarrow> 'a" ("\<langle>_,_\<rangle>") where
    2.88 +"\<langle>xs,ys\<rangle> = (\<Sum>(x,y) \<leftarrow> zip xs ys. x*y)"
    2.89 +
    2.90 +lemma iprod_Nil[simp]: "\<langle>[],ys\<rangle> = 0"
    2.91 +by(simp add:iprod_def)
    2.92 +
    2.93 +lemma iprod_Nil2[simp]: "\<langle>xs,[]\<rangle> = 0"
    2.94 +by(simp add:iprod_def)
    2.95 +
    2.96 +lemma iprod_Cons[simp]: "\<langle>x#xs,y#ys\<rangle> = x*y + \<langle>xs,ys\<rangle>"
    2.97 +by(simp add:iprod_def)
    2.98 +
    2.99 +lemma iprod0_if_coeffs0: "\<forall>c\<in>set cs. c = 0 \<Longrightarrow> \<langle>cs,xs\<rangle> = 0"
   2.100 +apply(induct cs arbitrary:xs)
   2.101 + apply simp
   2.102 +apply(case_tac xs) apply simp
   2.103 +apply auto
   2.104 +done
   2.105 +
   2.106 +lemma iprod_uminus[simp]: "\<langle>-xs,ys\<rangle> = -\<langle>xs,ys\<rangle>"
   2.107 +by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)
   2.108 +
   2.109 +lemma iprod_left_add_distrib: "\<langle>xs + ys,zs\<rangle> = \<langle>xs,zs\<rangle> + \<langle>ys,zs\<rangle>"
   2.110 +apply(induct xs arbitrary: ys zs)
   2.111 +apply (simp add: o_def split_def)
   2.112 +apply(case_tac ys)
   2.113 +apply simp
   2.114 +apply(case_tac zs)
   2.115 +apply (simp)
   2.116 +apply(simp add:left_distrib)
   2.117 +done
   2.118 +
   2.119 +lemma iprod_left_diff_distrib: "\<langle>xs - ys, zs\<rangle> = \<langle>xs,zs\<rangle> - \<langle>ys,zs\<rangle>"
   2.120 +apply(induct xs arbitrary: ys zs)
   2.121 +apply (simp add: o_def split_def)
   2.122 +apply(case_tac ys)
   2.123 +apply simp
   2.124 +apply(case_tac zs)
   2.125 +apply (simp)
   2.126 +apply(simp add:left_diff_distrib)
   2.127 +done
   2.128 +
   2.129 +lemma iprod_assoc: "\<langle>x *\<^sub>s xs, ys\<rangle> = x * \<langle>xs,ys\<rangle>"
   2.130 +apply(induct xs arbitrary: ys)
   2.131 +apply simp
   2.132 +apply(case_tac ys)
   2.133 +apply (simp)
   2.134 +apply (simp add:right_distrib mult_assoc)
   2.135 +done
   2.136 +
   2.137 +end
   2.138 \ No newline at end of file