Quelle  MonoidSums.thy

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
  finite sums (see "lemmas" in Ring.thy).›

text ‹Use as an intro rule›
lemma (in comm_monoid) factors_equal:
  "[a=b; c=d] ==> a⊗c = b⊗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 "(⨂ x∈S. (if x∈A then a x else 1)) = (⨂ x∈A. a x)"
  (is "(⨂ x∈S. ?b x) = (⨂ 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 ⊙ finsum M g A) = finsum M (%x. c ⊙ 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 ⊕ finsum M g A"
    by (intro finsum_insert, auto)
  from insert.hyps insert.prems have 2: "(⨁x∈insert a A. c ⊙ g x) = c ⊙ g a ⊕(⨁x∈A. c ⊙ 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 ⊙ v) = finsum M (%x. f x ⊙ 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 ⊕ finsum R f A"
    by (intro R.finsum_insert, auto)
  from insert.hyps insert.prems have 2: "(⨁x∈insert a A. f x ⊙ v) = f a ⊙ v ⊕(⨁x∈A. f x ⊙ 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.
  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)\<in>f*)
  from 3 6 show ?thesis by auto
qed

lemma (in comm_monoid) finprod_all1[simp]:
  assumes all1:" ∧a. a∈A==>f a = 1"
  shows "(⨂ a∈A. f a) = 1"
(*  "[| \<And>a. a\<in>A\<Longrightarrow>f a = \<one>\<^bsub>G\<^esub> |] ==> (\<Otimes>\<^bsub>G\<^esub> a\<in>A. f a) = \<one>\<^bsub>G\<^esub>" 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