# Theory ListVector

Up to index of Isabelle/HOL/LinearQuantifierElim

theory ListVector
imports Main
(*  Author: Tobias Nipkow, 2007 *)header {* Lists as vectors *}theory ListVectorimports List Mainbegintext{* \noindentA vector-space like structure of lists and arithmetic operations on them.Is only a vector space if restricted to lists of the same length. *}text{* Multiplication with a scalar: *}abbreviation scale :: "('a::times) => 'a list => 'a list" (infix "*⇩s" 70)where "x *⇩s xs ≡ map (op * x) xs"lemma scale1[simp]: "(1::'a::monoid_mult) *⇩s xs = xs"by (induct xs) simp_allsubsection {* @{text"+"} and @{text"-"} *}fun zipwith0 :: "('a::zero => 'b::zero => 'c) => 'a list => 'b list => 'c list"where"zipwith0 f [] [] = []" |"zipwith0 f (x#xs) (y#ys) = f x y # zipwith0 f xs ys" |"zipwith0 f (x#xs) [] = f x 0 # zipwith0 f xs []" |"zipwith0 f [] (y#ys) = f 0 y # zipwith0 f [] ys"instantiation list :: ("{zero, plus}") plusbegindefinition  list_add_def: "op + = zipwith0 (op +)"instance ..endinstantiation list :: ("{zero, uminus}") uminusbegindefinition  list_uminus_def: "uminus = map uminus"instance ..endinstantiation list :: ("{zero,minus}") minusbegindefinition  list_diff_def: "op - = zipwith0 (op -)"instance ..endlemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"by(induct ys) simp_alllemma list_add_Nil[simp]: "[] + xs = (xs::'a::monoid_add list)"by (induct xs) (auto simp:list_add_def)lemma list_add_Nil2[simp]: "xs + [] = (xs::'a::monoid_add list)"by (induct xs) (auto simp:list_add_def)lemma list_add_Cons[simp]: "(x#xs) + (y#ys) = (x+y)#(xs+ys)"by(auto simp:list_add_def)lemma list_diff_Nil[simp]: "[] - xs = -(xs::'a::group_add list)"by (induct xs) (auto simp:list_diff_def list_uminus_def)lemma list_diff_Nil2[simp]: "xs - [] = (xs::'a::group_add list)"by (induct xs) (auto simp:list_diff_def)lemma list_diff_Cons_Cons[simp]: "(x#xs) - (y#ys) = (x-y)#(xs-ys)"by (induct xs) (auto simp:list_diff_def)lemma list_uminus_Cons[simp]: "-(x#xs) = (-x)#(-xs)"by (induct xs) (auto simp:list_uminus_def)lemma self_list_diff:  "xs - xs = replicate (length(xs::'a::group_add list)) 0"by(induct xs) simp_alllemma list_add_assoc: fixes xs :: "'a::monoid_add list"shows "(xs+ys)+zs = xs+(ys+zs)"apply(induct xs arbitrary: ys zs) apply simpapply(case_tac ys) apply(simp)apply(simp)apply(case_tac zs) apply(simp)apply(simp add: add_assoc)donesubsection "Inner product"definition iprod :: "'a::ring list => 'a list => 'a" ("⟨_,_⟩") where"⟨xs,ys⟩ = (∑(x,y) \<leftarrow> zip xs ys. x*y)"lemma iprod_Nil[simp]: "⟨[],ys⟩ = 0"by(simp add: iprod_def)lemma iprod_Nil2[simp]: "⟨xs,[]⟩ = 0"by(simp add: iprod_def)lemma iprod_Cons[simp]: "⟨x#xs,y#ys⟩ = x*y + ⟨xs,ys⟩"by(simp add: iprod_def)lemma iprod0_if_coeffs0: "∀c∈set cs. c = 0 ==> ⟨cs,xs⟩ = 0"apply(induct cs arbitrary:xs) apply simpapply(case_tac xs) apply simpapply autodonelemma iprod_uminus[simp]: "⟨-xs,ys⟩ = -⟨xs,ys⟩"by(simp add: iprod_def uminus_listsum_map o_def split_def map_zip_map list_uminus_def)lemma iprod_left_add_distrib: "⟨xs + ys,zs⟩ = ⟨xs,zs⟩ + ⟨ys,zs⟩"apply(induct xs arbitrary: ys zs)apply (simp add: o_def split_def)apply(case_tac ys)apply simpapply(case_tac zs)apply (simp)apply(simp add: distrib_right)donelemma iprod_left_diff_distrib: "⟨xs - ys, zs⟩ = ⟨xs,zs⟩ - ⟨ys,zs⟩"apply(induct xs arbitrary: ys zs)apply (simp add: o_def split_def)apply(case_tac ys)apply simpapply(case_tac zs)apply (simp)apply(simp add: left_diff_distrib)donelemma iprod_assoc: "⟨x *⇩s xs, ys⟩ = x * ⟨xs,ys⟩"apply(induct xs arbitrary: ys)apply simpapply(case_tac ys)apply (simp)apply (simp add: distrib_left mult_assoc)doneend