Theory VectorSpace.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)
qed
text ‹Scalar multiplication distributes over scalar multiplication (on left).›
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).›
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.›
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)
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⇙"
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