Theory ListSum

(*  Author:     Gertrud Bauer, Tobias Nipkow
*)

section "Summation Over Lists"

theory ListSum
imports ListAux
begin

primrec ListSum :: "'b list  ('b  'a::comm_monoid_add)  'a::comm_monoid_add"  where
  "ListSum [] f = 0"
| "ListSum (l#ls) f = f l + ListSum ls f"

syntax "_ListSum" :: "idt  'b list  ('a::comm_monoid_add)  
  ('a::comm_monoid_add)"    ("∑⇘__ _" [0, 0, 10] 10)
translations "∑⇘xxsf" == "CONST ListSum xs (λx. f)" 

lemma [simp]: "(∑⇘v  V0) = (0::nat)" by (induct V) simp_all

lemma ListSum_compl1: 
  "(∑⇘x  [xxs. ¬ P x]f x) + (∑⇘x  [xxs. P x]f x) = (∑⇘x  xs(f x::nat))" 
 by (induct xs) simp_all

lemma ListSum_compl2: 
  "(∑⇘x   [xxs. P x]f x) + (∑⇘x   [xxs. ¬ P x]f x) = (∑⇘x  xs(f x::nat))" 
 by (induct xs) simp_all

lemmas ListSum_compl = ListSum_compl1 ListSum_compl2


lemma ListSum_conv_sum:
 "distinct xs  ListSum xs f =  sum f (set xs)"
by(induct xs) simp_all


lemma listsum_cong:
 " xs = ys; y. y  set ys  f y = g y 
   ListSum xs f = ListSum ys g"
apply simp
apply(erule thin_rl)
by (induct ys) simp_all


lemma strong_listsum_cong[cong]:
 " xs = ys; y. y  set ys =simp=> f y = g y 
   ListSum xs f = ListSum ys g"
by(auto simp:simp_implies_def intro!:listsum_cong)


lemma ListSum_eq [trans]: 
  "(v. v  set V  f v = g v)  (∑⇘v  Vf v) = (∑⇘v  Vg v)" 
by(auto intro!:listsum_cong)


lemma ListSum_disj_union: 
  "distinct A  distinct B  distinct C  
  set C = set A  set B   
  set A  set B = {} 
  (∑⇘a  C(f a)) = (∑⇘a  Af a) + (∑⇘a  B(f a::nat))"
by (simp add: ListSum_conv_sum sum.union_disjoint)


lemma listsum_const[simp]: 
  "(∑⇘x  xsk) = length xs * k"
by (induct xs) (simp_all add: ring_distribs)

lemma ListSum_add: 
  "(∑⇘x  Vf x) + (∑⇘x  Vg x) = (∑⇘x  V(f x + (g x::nat)))" 
  by (induct V) auto

lemma ListSum_le: 
  "(v. v  set V  f v  g v)  (∑⇘v  Vf v)  (∑⇘v  V(g v::nat))"
proof (induct V)
  case Nil then show ?case by simp
next
  case (Cons v V) then have "(∑⇘v  Vf v)  (∑⇘v  Vg v)" by simp
  moreover from Cons have "f v  g v" by simp
  ultimately show ?case by simp
qed

lemma ListSum1_bound:
 "a  set F  (d a::nat) (∑⇘f  Fd f)"
by (induct F) auto

end