(*  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
lemma
ListSum ls1 f1 == natListSum ls1 f1
lemma
ListSum ls1 f1 == intListSum ls1 f1
lemma
∑v∈V 0 = 0
lemma ListSum_compl1:
ListSum [x∈xs . ¬ P x] f + ListSum (filter P xs) f = ListSum xs f
lemma ListSum_compl2:
ListSum (filter P xs) f + ListSum [x∈xs . ¬ P x] f = ListSum xs f
lemmas ListSum_compl:
ListSum [x∈xs . ¬ P x] f + ListSum (filter P xs) f = ListSum xs f
ListSum (filter P xs) f + ListSum [x∈xs . ¬ P x] f = ListSum xs f
lemmas ListSum_compl:
ListSum [x∈xs . ¬ P x] f + ListSum (filter P xs) f = ListSum xs f
ListSum (filter P xs) f + ListSum [x∈xs . ¬ P x] f = ListSum xs f
lemma ListSum_conv_setsum:
distinct xs ==> ListSum xs f = setsum f (set xs)
lemma listsum_cong:
[| xs = ys; !!y. y ∈ set ys ==> f y = g y |] ==> ListSum xs f = ListSum ys g
lemma strong_listsum_cong:
[| xs = ys; !!y. y ∈ set ys =simp=> f y = g y |] ==> ListSum xs f = ListSum ys g
lemma ListSum_eq:
(!!v. v ∈ set V ==> f v = g v) ==> ListSum V f = ListSum V g
lemma ListSum_set_eq:
[| distinct B; distinct C; set B = set C |] ==> ListSum B f = ListSum C f
lemma ListSum_disj_union:
[| distinct A; distinct B; distinct C; set C = set A ∪ set B; set A ∩ set B = {} |] ==> ListSum C f = ListSum A f + ListSum B f
lemma separating_insert1:
separating (insert a V) F ==> separating V F
lemma separating_insert2:
[| separating (insert a V) F; a ∉ V; v ∈ V |] ==> F a ∩ F v = {}
lemma setsum_disj_Union:
[| finite V; !!f. finite (F f); separating V F |] ==> (∑v∈V. setsum w (F v)) = setsum w (UN v:V. F v)
lemma listsum_const:
∑x∈xs k = |xs| * k
lemma ListSum_add:
ListSum V f + ListSum V g = ∑x∈V f x + g x
lemma ListSum_le:
(!!v. v ∈ set V ==> f v ≤ g v) ==> ListSum V f ≤ ListSum V g
lemma ListSum1_bound:
a ∈ set F ==> d a ≤ ListSum F d
lemma ListSum2_bound:
[| a ∈ set F; b ∈ set F; a ≠ b |] ==> d a + d b ≤ ListSum F d