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 "∑⇘x∈xs⇙ f" == "CONST ListSum xs (λx. f)" 

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

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

lemma ListSum_compl2: 
  "(∑⇘x ∈  [x←xs. P x]⇙ f x) + (∑⇘x ∈  [x←xs. ¬ 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 ∈ V⇙ f v) = (∑⇘v ∈ V⇙ g 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 ∈ A⇙ f a) + (∑⇘a ∈ B⇙ (f a::nat))"
by (simp add: ListSum_conv_sum sum.union_disjoint)


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

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

lemma ListSum_le: 
  "(⋀v. v ∈ set V ⟹ f v ≤ g v) ⟹ (∑⇘v ∈ V⇙ f v) ≤ (∑⇘v ∈ V⇙ (g v::nat))"
proof (induct V)
  case Nil then show ?case by simp
next
  case (Cons v V) then have "(∑⇘v ∈ V⇙ f v) ≤ (∑⇘v ∈ V⇙ g 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 ∈ F⇙ d f)"
by (induct F) auto

end