header "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\<leftarrow>xs. ¬ P x]⇙ f x) + (∑⇘x ∈ [x\<leftarrow>xs. P x]⇙ f x) = (∑⇘x ∈ xs⇙ (f x::nat))"
by (induct xs) simp_all
lemma ListSum_compl2:
"(∑⇘x ∈ [x\<leftarrow>xs. P x]⇙ f x) + (∑⇘x ∈ [x\<leftarrow>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_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)
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