# Theory Groups_List

```(* Author: Tobias Nipkow, TU Muenchen *)

section ‹Sum and product over lists›

theory Groups_List
imports List
begin

locale monoid_list = monoid
begin

definition F :: "'a list ⇒ 'a"
where
eq_foldr [code]: "F xs = foldr f xs ❙1"

lemma Nil [simp]:
"F [] = ❙1"

lemma Cons [simp]:
"F (x # xs) = x ❙* F xs"

lemma append [simp]:
"F (xs @ ys) = F xs ❙* F ys"
by (induct xs) (simp_all add: assoc)

end

locale comm_monoid_list = comm_monoid + monoid_list
begin

lemma rev [simp]:
"F (rev xs) = F xs"
by (simp add: eq_foldr foldr_fold  fold_rev fun_eq_iff assoc left_commute)

end

locale comm_monoid_list_set = list: comm_monoid_list + set: comm_monoid_set
begin

lemma distinct_set_conv_list:
"distinct xs ⟹ set.F g (set xs) = list.F (map g xs)"
by (induct xs) simp_all

lemma set_conv_list [code]:
"set.F g (set xs) = list.F (map g (remdups xs))"

lemma list_conv_set_nth:
"list.F xs = set.F (λi. xs ! i) {0..<length xs}"
proof -
have "xs = map (λi. xs ! i) [0..<length xs]"
also have "list.F … = set.F (λi. xs ! i) {0..<length xs}"
by (subst distinct_set_conv_list [symmetric]) auto
finally show ?thesis .
qed

end

subsection ‹List summation›

begin

sublocale sum_list: monoid_list plus 0
defines
sum_list = sum_list.F ..

end

begin

sublocale sum_list: comm_monoid_list plus 0
rewrites
"monoid_list.F plus 0 = sum_list"
proof -
show "comm_monoid_list plus 0" ..
then interpret sum_list: comm_monoid_list plus 0 .
from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
qed

sublocale sum: comm_monoid_list_set plus 0
rewrites
"monoid_list.F plus 0 = sum_list"
and "comm_monoid_set.F plus 0 = sum"
proof -
show "comm_monoid_list_set plus 0" ..
then interpret sum: comm_monoid_list_set plus 0 .
from sum_list_def show "monoid_list.F plus 0 = sum_list" by simp
from sum_def show "comm_monoid_set.F plus 0 = sum" by (auto intro: sym)
qed

end

text ‹Some syntactic sugar for summing a function over a list:›
syntax (ASCII)
"_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
syntax
"_sum_list" :: "pttrn => 'a list => 'b => 'b"    ("(3∑_←_. _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
"∑x←xs. b" == "CONST sum_list (CONST map (λx. b) xs)"

context
includes lifting_syntax
begin

lemma sum_list_transfer [transfer_rule]:
"(list_all2 A ===> A) sum_list sum_list"
if [transfer_rule]: "A 0 0" "(A ===> A ===> A) (+) (+)"
unfolding sum_list.eq_foldr [abs_def]
by transfer_prover

end

text ‹TODO duplicates›
lemmas sum_list_simps = sum_list.Nil sum_list.Cons
lemmas sum_list_append = sum_list.append
lemmas sum_list_rev = sum_list.rev

"fold plus xs = plus (sum_list (rev xs))"
proof
fix x
have "fold plus xs x = sum_list (rev xs @ [x])"
also have "… = sum_list (rev xs) + x"
by simp
finally show "fold plus xs x = sum_list (rev xs) + x"
.
qed

"x ∈ set xs ⟹ sum_list (map f xs) = f x + sum_list (map f (remove1 x xs))"
by (induct xs) (auto simp add: ac_simps)

"size_list f xs = sum_list (map f xs) + size xs"
by (induct xs) auto

"length (concat xss) = sum_list (map length xss)"
by (induct xss) simp_all

"length (product_lists xss) = foldr (*) (map length xss) 1"
proof (induct xss)
case (Cons xs xss) then show ?case by (induct xs) (auto simp: length_concat o_def)
qed simp

assumes "⋀x. x ∈ set xs ⟹ ¬ P x ⟹ f x = 0"
shows "sum_list (map f (filter P xs)) = sum_list (map f xs)"
using assms by (induct xs) auto

lemma sum_list_filter_le_nat:
fixes f :: "'a ⇒ nat"
shows "sum_list (map f (filter P xs)) ≤ sum_list (map f xs)"
by(induction xs; simp)

"distinct xs ⟹ sum_list xs = Sum (set xs)"
by (induct xs) simp_all

lemma sum_list_upt[simp]:
"m ≤ n ⟹ sum_list [m..<n] = ∑ {m..<n}"

begin

lemma sum_list_nonneg: "(⋀x. x ∈ set xs ⟹ 0 ≤ x) ⟹ 0 ≤ sum_list xs"
by (induction xs) auto

lemma sum_list_nonpos: "(⋀x. x ∈ set xs ⟹ x ≤ 0) ⟹ sum_list xs ≤ 0"
by (induction xs) (auto simp: add_nonpos_nonpos)

lemma sum_list_nonneg_eq_0_iff:
"(⋀x. x ∈ set xs ⟹ 0 ≤ x) ⟹ sum_list xs = 0 ⟷ (∀x∈ set xs. x = 0)"

end

begin

lemma sum_list_eq_0_iff [simp]:
"sum_list ns = 0 ⟷ (∀n ∈ set ns. n = 0)"

lemma member_le_sum_list:
"x ∈ set xs ⟹ x ≤ sum_list xs"

lemma elem_le_sum_list:
"k < size ns ⟹ ns ! k ≤ sum_list (ns)"
by (rule member_le_sum_list) simp

end

lemma (in ordered_cancel_comm_monoid_diff) sum_list_update:
"k < size xs ⟹ sum_list (xs[k := x]) = sum_list xs + x - xs ! k"
apply(induction xs arbitrary:k)
apply (auto simp: add_ac split: nat.split)
apply(drule elem_le_sum_list)

"(∑x←xs. r) = of_nat (length xs) * r"
by (induct xs) (simp_all add: distrib_right)

"(∑x←xs. 0) = 0"
by (induct xs) (simp_all add: distrib_right)

text‹For non-Abelian groups ‹xs› needs to be reversed on one side:›
"- sum_list (map f xs) = sum_list (map (uminus ∘ f) xs)"
by (induct xs) simp_all

"(∑x←xs. f x + g x) = sum_list (map f xs) + sum_list (map g xs)"
by (induct xs) (simp_all add: algebra_simps)

"(∑x←xs. f x - g x) = sum_list (map f xs) - sum_list (map g xs)"
by (induct xs) (simp_all add: algebra_simps)

lemma (in semiring_0) sum_list_const_mult:
"(∑x←xs. c * f x) = c * (∑x←xs. f x)"
by (induct xs) (simp_all add: algebra_simps)

lemma (in semiring_0) sum_list_mult_const:
"(∑x←xs. f x * c) = (∑x←xs. f x) * c"
by (induct xs) (simp_all add: algebra_simps)

"¦sum_list xs¦ ≤ sum_list (map abs xs)"
by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])

lemma sum_list_mono:
shows "(⋀x. x ∈ set xs ⟹ f x ≤ g x) ⟹ (∑x←xs. f x) ≤ (∑x←xs. g x)"

lemma sum_list_strict_mono:
shows "⟦ xs ≠ [];  ⋀x. x ∈ set xs ⟹ f x < g x ⟧
⟹ sum_list (map f xs) < sum_list (map g xs)"
proof (induction xs)
case Nil thus ?case by simp
next
case C: (Cons _ xs)
show ?case
proof (cases xs)
case Nil thus ?thesis using C.prems by simp
next
qed
qed

text ‹A much more general version of this monotonicity lemma
can be formulated with multisets and the multiset order›

lemma sum_list_mono2: fixes xs :: "'a ::ordered_comm_monoid_add list"
shows "⟦ length xs = length ys; ⋀i. i < length xs ⟶ xs!i ≤ ys!i ⟧
⟹ sum_list xs ≤ sum_list ys"
apply(induction xs ys rule: list_induct2)
by(auto simp: nth_Cons' less_Suc_eq_0_disj imp_ex add_mono)

"distinct xs ⟹ sum_list (map f xs) = sum f (set xs)"
by (induct xs) simp_all

"sum_list (map f [m..<n]) = sum f (set [m..<n])"

"sum_list (map f [k..l]) = sum f (set [k..l])"

text ‹General equivalence between \<^const>‹sum_list› and \<^const>‹sum››
"sum_list xs = (∑ i = 0 ..< length xs. xs ! i)"
using interv_sum_list_conv_sum_set_nat [of "(!) xs" 0 "length xs"] by (simp add: map_nth)

lemma sum_list_map_eq_sum_count:
"sum_list (map f xs) = sum (λx. count_list xs x * f x) (set xs)"
proof(induction xs)
case (Cons x xs)
show ?case (is "?l = ?r")
proof cases
assume "x ∈ set xs"
have "?l = f x + (∑x∈set xs. count_list xs x * f x)" by (simp add: Cons.IH)
also have "set xs = insert x (set xs - {x})" using ‹x ∈ set xs›by blast
also have "f x + (∑x∈insert x (set xs - {x}). count_list xs x * f x) = ?r"
finally show ?thesis .
next
assume "x ∉ set xs"
hence "⋀xa. xa ∈ set xs ⟹ x ≠ xa" by blast
thus ?thesis by (simp add: Cons.IH ‹x ∉ set xs›)
qed
qed simp

lemma sum_list_map_eq_sum_count2:
assumes "set xs ⊆ X" "finite X"
shows "sum_list (map f xs) = sum (λx. count_list xs x * f x) X"
proof-
let ?F = "λx. count_list xs x * f x"
have "sum ?F X = sum ?F (set xs ∪ (X - set xs))"
using Un_absorb1[OF assms(1)] by(simp)
also have "… = sum ?F (set xs)"
using assms(2)
by(simp add: sum.union_disjoint[OF _ _ Diff_disjoint] del: Un_Diff_cancel)
qed

lemma sum_list_replicate: "sum_list (replicate n c) = of_nat n * c"

lemma sum_list_nonneg:
"(⋀x. x ∈ set xs ⟹ (x :: 'a :: ordered_comm_monoid_add) ≥ 0) ⟹ sum_list xs ≥ 0"
by (induction xs) simp_all

lemma sum_list_Suc:
"sum_list (map (λx. Suc(f x)) xs) = sum_list (map f xs) + length xs"
by(induction xs; simp)

"sum_list (map f (filter P xs)) = sum_list (map (λx. if P x then f x else 0) xs)"
by (induction xs) simp_all

text ‹Summation of a strictly ascending sequence with length ‹n›
can be upper-bounded by summation over ‹{0..<n}›.›

lemma sorted_wrt_less_sum_mono_lowerbound:
fixes f :: "nat ⇒ ('b::ordered_comm_monoid_add)"
assumes mono: "⋀x y. x≤y ⟹ f x ≤ f y"
shows "sorted_wrt (<) ns ⟹
(∑i∈{0..<length ns}. f i) ≤ (∑i←ns. f i)"
proof (induction ns rule: rev_induct)
case Nil
then show ?case by simp
next
case (snoc n ns)
have "sum f {0..<length (ns @ [n])}
= sum f {0..<length ns} + f (length ns)"
by simp
also have "sum f {0..<length ns} ≤ sum_list (map f ns)"
using snoc by (auto simp: sorted_wrt_append)
also have "length ns ≤ n"
using sorted_wrt_less_idx[OF snoc.prems(1), of "length ns"] by auto
finally have "sum f {0..<length (ns @ [n])} ≤ sum_list (map f ns) + f n"
thus ?case by simp
qed

subsection ‹Horner sums›

context comm_semiring_0
begin

definition horner_sum :: ‹('b ⇒ 'a) ⇒ 'a ⇒ 'b list ⇒ 'a›
where horner_sum_foldr: ‹horner_sum f a xs = foldr (λx b. f x + a * b) xs 0›

lemma horner_sum_simps [simp]:
‹horner_sum f a [] = 0›
‹horner_sum f a (x # xs) = f x + a * horner_sum f a xs›

lemma horner_sum_eq_sum_funpow:
‹horner_sum f a xs = (∑n = 0..<length xs. ((*) a ^^ n) (f (xs ! n)))›
proof (induction xs)
case Nil
then show ?case
by simp
next
case (Cons x xs)
then show ?case
by (simp add: sum.atLeast0_lessThan_Suc_shift sum_distrib_left del: sum.op_ivl_Suc)
qed

end

context
includes lifting_syntax
begin

lemma horner_sum_transfer [transfer_rule]:
‹((B ===> A) ===> A ===> list_all2 B ===> A) horner_sum horner_sum›
if [transfer_rule]: ‹A 0 0›
and [transfer_rule]: ‹(A ===> A ===> A) (+) (+)›
and [transfer_rule]: ‹(A ===> A ===> A) (*) (*)›
by (unfold horner_sum_foldr) transfer_prover

end

context comm_semiring_1
begin

lemma horner_sum_eq_sum:
‹horner_sum f a xs = (∑n = 0..<length xs. f (xs ! n) * a ^ n)›
proof -
have ‹(*) a ^^ n = (*) (a ^ n)› for n
by (induction n) (simp_all add: ac_simps)
then show ?thesis
qed

lemma horner_sum_append:
‹horner_sum f a (xs @ ys) = horner_sum f a xs + a ^ length xs * horner_sum f a ys›
using sum.atLeastLessThan_shift_bounds [of _ 0 ‹length xs› ‹length ys›]
atLeastLessThan_add_Un [of 0 ‹length xs› ‹length ys›]

end

context linordered_semidom
begin

lemma horner_sum_nonnegative:
‹0 ≤ horner_sum of_bool 2 bs›
by (induction bs) simp_all

end

context discrete_linordered_semidom
begin

lemma horner_sum_bound:
‹horner_sum of_bool 2 bs < 2 ^ length bs›
proof (induction bs)
case Nil
then show ?case
by simp
next
case (Cons b bs)
moreover define a where ‹a = 2 ^ length bs - horner_sum of_bool 2 bs›
ultimately have *: ‹2 ^ length bs = horner_sum of_bool 2 bs + a›
by simp
have ‹0 < a›
using Cons * by simp
moreover have ‹1 ≤ a›
using ‹0 < a› by (simp add: less_eq_iff_succ_less)
ultimately have ‹0 + 1 < a + a›
then have ‹1 < a * 2›
with Cons show ?case
qed

lemma horner_sum_of_bool_2_less:
‹(horner_sum of_bool 2 bs) < 2 ^ length bs›
by (fact horner_sum_bound)

end

lemma nat_horner_sum [simp]:
‹nat (horner_sum of_bool 2 bs) = horner_sum of_bool 2 bs›

context discrete_linordered_semidom
begin

lemma horner_sum_less_eq_iff_lexordp_eq:
‹horner_sum of_bool 2 bs ≤ horner_sum of_bool 2 cs ⟷ lexordp_eq (rev bs) (rev cs)›
if ‹length bs = length cs›
proof -
have ‹horner_sum of_bool 2 (rev bs) ≤ horner_sum of_bool 2 (rev cs) ⟷ lexordp_eq bs cs›
if ‹length bs = length cs› for bs cs
using that proof (induction bs cs rule: list_induct2)
case Nil
then show ?case
by simp
next
case (Cons b bs c cs)
with horner_sum_nonnegative [of ‹rev bs›] horner_sum_nonnegative [of ‹rev cs›]
horner_sum_bound [of ‹rev bs›] horner_sum_bound [of ‹rev cs›]
show ?case
qed
from that this [of ‹rev bs› ‹rev cs›] show ?thesis
by simp
qed

lemma horner_sum_less_iff_lexordp:
‹horner_sum of_bool 2 bs < horner_sum of_bool 2 cs ⟷ ord_class.lexordp (rev bs) (rev cs)›
if ‹length bs = length cs›
proof -
have ‹horner_sum of_bool 2 (rev bs) < horner_sum of_bool 2 (rev cs) ⟷ ord_class.lexordp bs cs›
if ‹length bs = length cs› for bs cs
using that proof (induction bs cs rule: list_induct2)
case Nil
then show ?case
by simp
next
case (Cons b bs c cs)
with horner_sum_nonnegative [of ‹rev bs›] horner_sum_nonnegative [of ‹rev cs›]
horner_sum_bound [of ‹rev bs›] horner_sum_bound [of ‹rev cs›]
show ?case
qed
from that this [of ‹rev bs› ‹rev cs›] show ?thesis
by simp
qed

end

lemma length_n_lists: "length (List.n_lists n xs) = length xs ^ n"
by (induct n) (auto simp add: comp_def length_concat sum_list_triv)

lemma distinct_n_lists:
assumes "distinct xs"
shows "distinct (List.n_lists n xs)"
proof (rule card_distinct)
from assms have card_length: "card (set xs) = length xs" by (rule distinct_card)
have "card (set (List.n_lists n xs)) = card (set xs) ^ n"
proof (induct n)
case 0 then show ?case by simp
next
case (Suc n)
moreover have "card (⋃ys∈set (List.n_lists n xs). (λy. y # ys) ` set xs)
= (∑ys∈set (List.n_lists n xs). card ((λy. y # ys) ` set xs))"
by (rule card_UN_disjoint) auto
moreover have "⋀ys. card ((λy. y # ys) ` set xs) = card (set xs)"
by (rule card_image) (simp add: inj_on_def)
ultimately show ?case by auto
qed
also have "… = length xs ^ n" by (simp add: card_length)
finally show "card (set (List.n_lists n xs)) = length (List.n_lists n xs)"
qed

subsection ‹Tools setup›

lemmas sum_code = sum.set_conv_list

lemma sum_set_upto_conv_sum_list_int [code_unfold]:
"sum f (set [i..j::int]) = sum_list (map f [i..j])"

lemma sum_set_upt_conv_sum_list_nat [code_unfold]:
"sum f (set [m..<n]) = sum_list (map f [m..<n])"

subsection ‹List product›

context monoid_mult
begin

sublocale prod_list: monoid_list times 1
defines
prod_list = prod_list.F ..

end

context comm_monoid_mult
begin

sublocale prod_list: comm_monoid_list times 1
rewrites
"monoid_list.F times 1 = prod_list"
proof -
show "comm_monoid_list times 1" ..
then interpret prod_list: comm_monoid_list times 1 .
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
qed

sublocale prod: comm_monoid_list_set times 1
rewrites
"monoid_list.F times 1 = prod_list"
and "comm_monoid_set.F times 1 = prod"
proof -
show "comm_monoid_list_set times 1" ..
then interpret prod: comm_monoid_list_set times 1 .
from prod_list_def show "monoid_list.F times 1 = prod_list" by simp
from prod_def show "comm_monoid_set.F times 1 = prod" by (auto intro: sym)
qed

end

text ‹Some syntactic sugar:›

syntax (ASCII)
"_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
syntax
"_prod_list" :: "pttrn => 'a list => 'b => 'b"    ("(3∏_←_. _)" [0, 51, 10] 10)
translations ― ‹Beware of argument permutation!›
"∏x←xs. b" ⇌ "CONST prod_list (CONST map (λx. b) xs)"

context
includes lifting_syntax
begin

lemma prod_list_transfer [transfer_rule]:
"(list_all2 A ===> A) prod_list prod_list"
if [transfer_rule]: "A 1 1" "(A ===> A ===> A) (*) (*)"
unfolding prod_list.eq_foldr [abs_def]
by transfer_prover

end

lemma prod_list_zero_iff:
"prod_list xs = 0 ⟷ (0 :: 'a :: {semiring_no_zero_divisors, semiring_1}) ∈ set xs"
by (induction xs) simp_all

end
```