# Theory ListSum

Up to index of Isabelle/HOL/Tame

theory ListSum
imports ListAux
begin

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

theory ListSum
imports ListAux
begin

primrec
"ListSum [] f = 0"
"ListSum (l#ls) f = f l + ListSum ls f"

syntax "_ListSum" :: "idt => 'b list => ('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)"

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))"

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"

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. ∑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 = {}"
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)

"(∑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`

`  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`