Quelle  ListVector.thy

(*  Author: Tobias Nipkow, 2007 *)

section ‹Lists as vectors›

theory ListVector
  imports Main
begin

text‹\noindent
 A 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 ((*) x) xs"

lemma scale1[simp]: "(1::'a::monoid_mult) *🪙s xs = xs"
  by (induct xs) simp_all

subsection ‹‹+› and ‹-›\<close>

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}") plus
begin

definition
  list_add_def: "(+) = zipwith0 (+)"

instance ..

end

instantiation list :: ("{zero, uminus}") uminus
begin

definition
  list_uminus_def: "uminus = map uminus"

instance ..

end

instantiation list :: ("{zero,minus}") minus
begin

definition
  list_diff_def: "(-) = zipwith0 (-)"

instance ..

end

lemma zipwith0_Nil[simp]: "zipwith0 f [] ys = map (f 0) ys"
  by(induct ys) simp_all

lemma 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_all

lemma list_add_assoc: 
  fixes xs :: "'a::monoid_add list"
  shows "(xs+ys)+zs = xs+(ys+zs)"
proof (induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys zs)
  show ?case
    by (cases ys; cases zs; simp add: add.assoc Cons)
qed

subsection "Inner product"

definition iprod :: "'a::ring list ==> 'a list ==> 'a" (‹(‹open_block notation=‹mixfix iprod›\›\⟨_,_⟩)›)
  where "⟨xs,ys⟩ = (∑(x,y) ← 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"
proof (induct cs arbitrary: xs)
  case Nil
  then show ?case by simp
next
  case (Cons a cs xs)
  then show ?case
    by (cases xs; fastforce)
qed

lemma iprod_uminus[simp]: "⟨-xs,ys⟩ = -⟨xs,ys⟩"
  by(simp add: iprod_def uminus_sum_list_map o_def split_def map_zip_map list_uminus_def)

lemma iprod_left_add_distrib: "⟨xs + ys,zs⟩ = ⟨xs,zs⟩ + ⟨ys,zs⟩"
proof (induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys zs)
  show ?case
    by (cases ys; cases zs; simp add: distrib_right Cons)
qed

lemma iprod_left_diff_distrib: "⟨xs - ys, zs⟩ = ⟨xs,zs⟩ - ⟨ys,zs⟩"
proof (induct xs arbitrary: ys zs)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys zs)
  show ?case
    by (cases ys; cases zs; simp add: left_diff_distrib Cons)
qed

lemma iprod_assoc: "⟨x *🪙s xs, ys⟩ = x * ⟨xs,ys⟩"
proof (induct xs arbitrary: ys)
  case Nil
  then show ?case by simp
next
  case (Cons a xs ys)
  show ?case
    by (cases ys; simp add: distrib_left mult.assoc Cons)
qed

end