# Theory MonoidSums

```section ‹Sums in monoids›

theory MonoidSums

imports Main
"HOL-Algebra.Module"
RingModuleFacts
FunctionLemmas
begin

text ‹We build on the finite product simplifications in FiniteProduct.thy and the analogous ones
for finite sums (see "lemmas" in Ring.thy).›

text ‹Use as an intro rule›
lemma (in comm_monoid) factors_equal:
"⟦a=b; c=d⟧ ⟹ a⊗⇘G⇙c =  b⊗⇘G⇙d"
by simp

lemma (in comm_monoid) extend_prod:
fixes a A S
assumes fin: "finite S" and subset: "A⊆S" and a: "a∈A→carrier G"
shows "(⨂⇘G⇙ x∈S. (if x∈A then a x else 𝟭⇘G⇙)) = (⨂⇘G⇙ x∈A. a x)"
(is "(⨂⇘G⇙ x∈S. ?b x) = (⨂⇘G⇙ x∈A. a x)")
proof -
from subset have uni:"S = A ∪ (S-A)" by auto
from assms subset show ?thesis
apply (subst uni)
apply (subst finprod_Un_disjoint, auto)
by (auto cong: finprod_cong if_cong elim: finite_subset simp add:Pi_def finite_subset)
(*Pi_def is key for automation here*)
qed

text ‹Scalar multiplication distributes over scalar multiplication (on left).›(*Add to module.*)
lemma (in module) finsum_smult:
"[| c∈ carrier R; g ∈ A → carrier M |] ==>
(c ⊙⇘M⇙ finsum M g A) = finsum M (%x. c ⊙⇘M⇙ g x) A "
proof (induct A rule: infinite_finite_induct)
case (insert a A)
from insert.hyps insert.prems have 1: "finsum M g (insert a A) = g a ⊕⇘M⇙ finsum M g A"
by (intro finsum_insert, auto)
from insert.hyps insert.prems have 2: "(⨁⇘M⇙x∈insert a A. c ⊙⇘M⇙ g x) = c ⊙⇘M⇙ g a ⊕⇘M⇙(⨁⇘M⇙x∈A. c ⊙⇘M⇙ g x)"
by (intro finsum_insert, auto)
from insert.hyps insert.prems show ?case
by (auto simp add:1 2 smult_r_distr)
qed auto

text ‹Scalar multiplication distributes over scalar multiplication (on right).›(*Add to module.*)
lemma (in module) finsum_smult_r:
"[| v∈ carrier M; f ∈ A → carrier R |] ==>
(finsum R f A ⊙⇘M⇙ v) = finsum M (%x. f x ⊙⇘M⇙ v) A "
proof (induct A rule: infinite_finite_induct)
case (insert a A)
from insert.hyps insert.prems have 1: "finsum R f (insert a A) = f a ⊕⇘R⇙ finsum R f A"
by (intro R.finsum_insert, auto)
from insert.hyps insert.prems have 2: "(⨁⇘M⇙x∈insert a A. f x ⊙⇘M⇙ v) = f a ⊙⇘M⇙ v ⊕⇘M⇙(⨁⇘M⇙x∈A. f x ⊙⇘M⇙ v)"
by (intro finsum_insert, auto)
from insert.hyps insert.prems show ?case
by (auto simp add:1 2 smult_l_distr)
qed auto

text ‹A sequence of lemmas that shows that the product does not depend on the ambient group.
Note I had to dig back into the definitions of foldSet to show this.›
(*Add the following 2 lemmas to Group.*)
lemma foldSet_not_depend:
fixes A E
assumes h1: "D⊆E"
shows "foldSetD D f e ⊆foldSetD E f e"
proof -
from h1 have 1: "⋀x1 x2. (x1,x2) ∈ foldSetD D f e ⟹ (x1, x2) ∈ foldSetD E f e"
proof -
fix x1 x2
assume 2: "(x1,x2) ∈ foldSetD D f e"
from h1 2 show "?thesis x1 x2"
apply (intro foldSetD.induct[where ?D="D" and ?f="f" and ?e="e" and ?x1.0="x1" and ?x2.0="x2"
and ?P = "λx1 x2. ((x1, x2)∈ foldSetD E f e)"])
apply auto
apply (intro emptyI, auto)
by (intro insertI, auto)
qed
from 1 show ?thesis by auto
qed

lemma foldD_not_depend:
fixes D E B f e A
assumes h1: "LCD B D f" and h2: "LCD B E f" and h3: "D⊆E" and h4: "e∈D" and h5: "A⊆B" and h6: "finite B"
shows "foldD D f e A = foldD E f e A"
proof -
from assms have 1: "∃y. (A,y)∈foldSetD D f e"
apply (intro finite_imp_foldSetD, auto)
apply (metis finite_subset)
by (unfold LCD_def, auto)
from 1 obtain y where 2: "(A,y)∈foldSetD D f e" by auto
from assms 2 have 3: "foldD D f e A = y" by (intro LCD.foldD_equality[of B], auto)
from h3 have 4: "foldSetD D f e ⊆ foldSetD E f e" by (rule foldSet_not_depend)
from 2 4 have 5: "(A,y)∈foldSetD E f e" by auto
from assms 5 have 6: "foldD E f e A = y" by (intro LCD.foldD_equality[of B], auto)
(*(A,y)∈f*)
from 3 6 show ?thesis by auto
qed

lemma (in comm_monoid) finprod_all1[simp]:
assumes all1:" ⋀a. a∈A⟹f a = 𝟭⇘G⇙"
shows "(⨂⇘G⇙ a∈A. f a) = 𝟭⇘G⇙"
(*  "[| ⋀a. a∈A⟹f a = 𝟭⇘G⇙ |] ==> (⨂⇘G⇙ a∈A. f a) = 𝟭⇘G⇙" won't work with proof - *)
proof -
from assms show ?thesis
by (simp cong: finprod_cong)
qed

context abelian_monoid
begin
lemmas summands_equal = add.factors_equal
lemmas extend_sum = add.extend_prod
lemmas finsum_all0 = add.finprod_all1
end

end
```