Theory ListSum

(*  ID:         $Id: ListSum.thy,v 1.2 2006/01/11 19:40:45 nipkow Exp $
    Author:     Gertrud Bauer, Tobias Nipkow
*)

header "Summation Over Lists"

theory ListSum
imports ListAux
begin

consts ListSum :: "'b list => ('b => 'a::comm_monoid_add) => 'a::comm_monoid_add" 
primrec 
 "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)"    ("∑_∈_ _")
translations "∑x∈xs f" == "ListSum xs (λx. f)" 

(* implementation on natural numbers *)
(* 1. nat list sum *)
consts natListSum :: "'b list => ('b => nat) => nat" 
primrec 
 "natListSum [] f = 0"
 "natListSum (l#ls) f = f l + natListSum ls f"

(* implementation on integers *)
(* 2. int list sum *)
consts intListSum :: "'b list => ('b => int) => int" 
primrec 
 "intListSum [] f = 0"
 "intListSum (l#ls) f = f l + intListSum ls f"



lemma [THEN eq_reflection, code unfold]: "((ListSum ls f)::nat) = natListSum ls f"
 by (induct ls) simp_all

lemma [THEN eq_reflection, code unfold]: "((ListSum ls f)::int) = intListSum ls f"
 by (induct ls) simp_all



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_setsum:
 "distinct xs ==> ListSum xs f =  setsum 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_set_eq: 
 "!!C. distinct B ==> distinct C ==> set B = set C ==>
  ∑a ∈ B f a = ∑a ∈ C (f a::nat)"
  by (simp add: ListSum_conv_setsum)

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_setsum setsum_Un_disjoint)


constdefs separating :: "'a set => ('a => 'b set) => bool"
  "separating V F ≡ 
   (∀v1 ∈ V. ∀v2 ∈ V. v1 ≠ v2 -->  F v1 ∩ F v2 = {})"


lemma separating_insert1: 
  "separating (insert a V) F ==> separating V F"
  by (simp add: separating_def)

lemma separating_insert2:
  "separating (insert a V) F ==> a ∉ V ==>  v ∈ V ==> 
  F a ∩ F v = {}"
  by (auto simp add: separating_def)

lemma setsum_disj_Union: 
 "finite V ==> 
  (!!f. finite (F f)) ==> 
  separating V F ==> 
  (∑v∈V. ∑f∈(F v). (w f::nat)) = (∑f∈(\<Union>v∈V. F v). w f)"
proof (induct  rule: finite_induct)
  case empty then show ?case by simp
next
  case (insert a V) 
  then have s: "separating (insert a V) F" by simp
  then have "separating V F" by (rule_tac separating_insert1)
  with insert
  have IH: "(∑v∈V. ∑f∈(F v). w f) = (∑f∈(\<Union>v∈V. F v). w f)" 
    by simp

  moreover have prems: "finite V" "a ∉ V" "!!f. finite (F f)" .

  moreover from s have "!!v. a ∉ V ==> v ∈ V ==> F a ∩ F v = {}"
   by (simp add: separating_insert2)
  with prems have "(F a) ∩ (\<Union>v∈V. F v) = {}" by auto 

  ultimately show ?case by (simp add: setsum_Un_disjoint)
qed


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

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 arith
qed

lemma ListSum1_bound:
 "a ∈ set F ==> (d a::nat)  ≤ ∑f ∈ F d f"
by (induct F) auto

lemma ListSum2_bound:
  "a ∈ set F ==> b ∈ set F ==> a ≠ b ==> d a + d b ≤ ∑f ∈ F (d f::nat)"
proof (induct F)
  case Nil then show ?case by simp
next
  case (Cons f F)
  then have "a = f ∨ a ∈ set F"  "b = f ∨ b ∈ set F" by simp_all
  then show ?case
  proof (elim disjE)
    assume "a = f"  "b = f" with Cons have False by simp
    then show ?thesis by simp
  next
    assume "a = f"  "b ∈ set F"
    with Cons show ?thesis by (simp add: ListSum1_bound)
  next
    assume "a ∈ set F" "b = f"
    with Cons show ?thesis by (simp add: ListSum1_bound)
  next
    assume "a ∈ set F" "b ∈ set F"
    with Cons have "d a + d b ≤ ∑f ∈ F d f" by simp
    then show ?thesis by simp arith
  qed
qed

end