(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2023 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) section ‹Summing lists in a monoid› theory Monoid_ZF_1 imports Monoid_ZF begin text‹This theory consider properties of sums of monoid elements, similar to the ones formalized in the ‹Semigroup_ZF› theory for sums of semigroup elements. The main difference is that since each monoid has a neutral element it makes sense to define a sum of an empty list of monoid elements. In multiplicative notation the properties considered here can be applied to natural powers of elements ($x^n, n\in \mathbb{N}$) in group or ring theory or, when written additively, to natural multiplicities $n\cdot x, n\in \mathbb{N}$). › subsection‹Notation and basic properties of sums of lists of monoid elements› text‹In this section we setup a contex (locale) with notation for sums of lists of monoid elements and prove basic properties of those sums in terms of that notation. › text‹The locale (context) ‹monoid1› extends the locale ‹monoid1›, adding the notation for the neutral element as $0$ and the sum of a list of monoid elements. It also defines a notation for natural multiple of an element of a monoid, i.e. $n\cdot x = x\oplus x\oplus ... \oplus x$ (n times). › locale monoid1 = monoid0 + fixes mzero ("𝟬") defines mzero_def [simp]: "𝟬 ≡ TheNeutralElement(G,f)" fixes listsum ("∑ _" 70) defines listsum_def [simp]: "∑s ≡ Fold(f,𝟬,s)" fixes nat_mult (infix "⋅" 72) defines nat_mult_def [simp]: "n⋅x ≡ ∑{⟨k,x⟩. k∈n}" text‹Let's recall that the neutral element of the monoid is an element of the monoid (carrier) $G$ and the monoid operation ($f$ in our notation) is a function that maps $G\times G$ to $G$.› lemma (in monoid1) zero_monoid_oper: shows "𝟬∈G" and "f:G×G → G" using monoidAssum unit_is_neutral unfolding IsAmonoid_def IsAssociative_def by simp_all text‹The sum of a list of monoid elements is a monoid element.› lemma (in monoid1) sum_in_mono: assumes "n∈nat" "∀k∈n. q(k)∈G" shows "(∑{⟨k,q(k)⟩. k∈n}) ∈ G" proof - let ?a = "{⟨k,q(k)⟩. k∈n}" from assms have "n ∈ nat" "f:G×G → G" "?a:n → G" "𝟬∈G" "G≠0" using zero_monoid_oper ZF_fun_from_total by auto then show ?thesis using fold_props by simp qed text‹The reason we start from $0$ in the definition of the summation sign in the ‹monoid1› locale is that we want to be able to sum the empty list. Such sum of the empty list is $0$. › lemma (in monoid1) sum_empty: assumes "s:0→G" shows "(∑s) = 𝟬" using assms zero_monoid_oper fold_empty group0_1_L3A by simp text‹For nonempty lists our $\Sigma$ is the same as ‹Fold1›. › lemma (in monoid1) sum_nonempty: assumes "n ∈ nat" "s:succ(n)→G" shows "(∑s) = Fold(f,s`(0),Tail(s))" "(∑s) = Fold1(f,s)" proof - from assms have "s`(0) ∈ G" using empty_in_every_succ apply_funtype by simp with assms have "(∑s) = Fold(f,𝟬⊕s`(0),Tail(s))" using zero_monoid_oper fold_detach_first by simp with ‹s`(0) ∈ G› show "(∑s) = Fold(f,s`(0),Tail(s))" using unit_is_neutral by simp then show "(∑s) = Fold1(f,s)" unfolding Fold1_def by simp qed text‹We can pull the first component of a sum of a nonempty list of monoid elements before the summation sign. › lemma (in monoid1) seq_sum_pull_first0: assumes "n ∈ nat" "s:succ(n)→G" shows "(∑s) = s`(0) ⊕ (∑Tail(s))" proof - from assms have "s`(0) ∈ G" using empty_in_every_succ apply_funtype by simp { assume "n=0" with assms have "Tail(s):0→G" using tail_props(1) by blast with assms ‹s`(0) ∈ G› have "(∑s) = s`(0) ⊕ (∑Tail(s))" using sum_nonempty(1) sum_empty zero_monoid_oper(2) group0_1_L3A fold_empty unit_is_neutral by simp } moreover { assume "n≠0" with assms(1) obtain m where "m∈nat" and "n = succ(m)" using Nat_ZF_1_L3 by blast with assms have "Tail(s):succ(m)→G" using tail_props(1) by simp let ?a = "{⟨0,s`(0)⟩}" from ‹s`(0) ∈ G› have "0∈nat" "?a:succ(0)→G" using pair_func_singleton succ_explained by simp_all with ‹m∈nat› ‹Tail(s):succ(m)→G› have "f`⟨Fold1(f,?a),Fold1(f,Tail(s))⟩ = Fold1(f,Concat(?a,Tail(s)))" using semigr0_valid_in_monoid0 semigr0.prod_conc_distr by blast with assms ‹?a:succ(0)→G› ‹m∈nat› ‹Tail(s):succ(m)→G› have "(∑s) = s`(0) ⊕ (∑Tail(s))" using semigr0_valid_in_monoid0 semigr0.prod_of_1elem pair_val sum_nonempty(2) first_concat_tail by simp } ultimately show ?thesis by auto qed text‹The first assertion of the next theorem is similar in content to ‹seq_sum_pull_first0› formulated in terms of the expression defining the list of monoid elements. The second one shows the dual statement: the last element of a sequence can be pulled out of the sequence and put after the summation sign. So, we are showing here that $\sum_{k=0}^{n} q_k = q_0 \oplus \sum_{k=0}^{n-1} q_{k+1} = (\sum_{k=0}^{n-1} q_k) \oplus q_n. $ › theorem (in monoid1) seq_sum_pull_one_elem: assumes "n ∈ nat" "∀k∈n #+ 1. q(k) ∈ G" shows "(∑{⟨k,q(k)⟩. k∈n #+ 1}) = q(0) ⊕ (∑{⟨k,q(k #+ 1)⟩. k∈n})" "(∑{⟨k,q(k)⟩. k∈n #+ 1}) = (∑{⟨k,q(k)⟩. k∈n}) ⊕ q(n)" proof - let ?s = "{⟨k,q(k)⟩. k∈n #+ 1}" from assms(1) have "0 ∈ n #+ 1" using empty_in_every_succ succ_add_one(1) by simp then have "?s`(0) = q(0)" by (rule ZF_fun_from_tot_val1) from assms(2) have "?s: n #+ 1 → G" by (rule ZF_fun_from_total) with assms(1) ‹?s`(0) = q(0)› have "(∑?s) = q(0) ⊕ (∑Tail(?s))" using seq_sum_pull_first0 by simp moreover from assms have "Tail(?s) = {⟨k,q(k #+ 1)⟩. k ∈ n}" using tail_formula by simp ultimately show "(∑{⟨k,q(k)⟩. k∈n #+ 1}) = q(0) ⊕ (∑{⟨k,q(k #+ 1)⟩. k∈n})" by simp from assms show "(∑{⟨k,q(k)⟩. k∈n #+ 1}) = (∑{⟨k,q(k)⟩. k∈n}) ⊕ q(n)" using zero_monoid_oper fold_detach_last by simp qed text‹The sum of a singleton list is its only element,› lemma (in monoid1) seq_sum_singleton: assumes "q(0) ∈ G" shows "(∑{⟨k,q(k)⟩. k∈1}) = q(0)" proof - from assms have "0∈nat" and "∀k∈0 #+ 1. q(k) ∈ G" by simp_all then have "(∑{⟨k,q(k)⟩. k∈0 #+ 1}) = q(0) ⊕ (∑{⟨k,q(k #+ 1)⟩. k∈0})" by (rule seq_sum_pull_one_elem) with assms show ?thesis using sum_empty unit_is_neutral by simp qed text‹If the monoid operation is commutative, then the sum of a nonempty sequence added to another sum of a nonempty sequence of the same length is equal to the sum of pointwise sums of the sequence elements. This is the same as the theorem ‹prod_comm_distrib› from the ‹Semigroup_ZF› theory, just written in the notation used in the ‹monoid1› locale.› lemma (in monoid1) sum_comm_distrib0: assumes "f {is commutative on} G" "n∈nat" and "a : n #+ 1 → G" "b : n #+ 1 → G" "c : n #+ 1 → G" and "∀j∈n #+ 1. c`(j) = a`(j) ⊕ b`(j)" shows "(∑ c) = (∑ a) ⊕ (∑ b)" using assms succ_add_one(1) sum_nonempty semigr0_valid_in_monoid0 semigr0.prod_comm_distrib by simp text‹Another version of ‹sum_comm_distrib0› written in terms of the expressions defining the sequences, shows that for commutative monoids we have $\sum_{k=0}^{n-1}q(k) \oplus p(k) = (\sum_{k=0}^{n-1} p(k))\oplus (\sum_{k=0}^{n-1} q(k))$. › theorem (in monoid1) sum_comm_distrib: assumes "f {is commutative on} G" "n∈nat" and "∀k∈n. p(k) ∈ G" "∀k∈n. q(k) ∈ G" shows "(∑{⟨k,p(k)⊕q(k)⟩. k∈n}) = (∑{⟨k,p(k)⟩. k∈n}) ⊕ (∑{⟨k,q(k)⟩. k∈n})" proof - let ?a = "{⟨k,p(k)⟩. k∈n}" let ?b = "{⟨k,q(k)⟩. k∈n}" let ?c = "{⟨k,p(k)⊕q(k)⟩. k∈n}" { assume "n=0" then have "(∑?c) = (∑?a) ⊕ (∑?b)" using sum_empty unit_is_neutral by simp } moreover { assume "n≠0" with assms(2) obtain m where "m∈nat" and "n = m #+ 1" using nat_not0_succ by blast from assms(3,4) have "?a:n→G" "?b:n→G" "?c:n→G" using group0_1_L1 ZF_fun_from_total by simp_all with assms(1) ‹m∈nat› ‹n = m #+ 1› have "f {is commutative on} G" "m∈nat" and "?a:m #+ 1→G" "?b:m #+ 1→G" "?c:m #+ 1→G" by simp_all moreover have "∀k∈m #+ 1. ?c`(k) = ?a`(k) ⊕ ?b`(k)" proof - { fix k assume "k ∈ m #+ 1" with ‹n = m #+ 1› have "k∈n" by simp then have "?c`(k) = ?a`(k) ⊕ ?b`(k)" using ZF_fun_from_tot_val1 by simp_all } thus ?thesis by simp qed ultimately have "(∑?c) = (∑?a) ⊕ (∑?b)" using sum_comm_distrib0 by simp } ultimately show ?thesis by blast qed subsection‹Multiplying monoid elements by natural numbers› text‹A special case of summing (or, using more notation-neutral term ‹folding›) a list of monoid elements is taking a natural multiple of a single element. This can be applied to various monoids embedded in other algebraic structures. For example a ring is a monoid with addition as the operation, so the notion of natural multiple directly transfers there. Another monoid in a ring is formed by its multiplication operation. In that case the natural multiple maps into natural powers of a ring element. › text‹The zero's multiple of a monoid element is its neutral element.› lemma (in monoid1) nat_mult_zero: shows "0⋅x = 𝟬" using sum_empty by simp text‹Any multiple of a monoid element is a monoid element.› lemma (in monoid1) nat_mult_type: assumes "n∈nat" "x∈G" shows "n⋅x ∈ G" using assms sum_in_mono by simp text‹Taking one more multiple of $x$ adds $x$. › lemma (in monoid1) nat_mult_add_one: assumes "n∈nat" "x∈G" shows "(n #+ 1)⋅x = n⋅x ⊕ x" and "(n #+ 1)⋅x = x ⊕ n⋅x" proof - from assms(2) have I: "∀k∈n #+ 1. x ∈ G" by simp with assms(1) have "(∑{⟨k,x⟩. k ∈ n #+ 1}) = x ⊕ (∑{⟨k,x⟩. k∈n})" by (rule seq_sum_pull_one_elem) thus "(n #+ 1)⋅x = x ⊕ n⋅x" by simp from assms(1) I have "(∑{⟨k,x⟩. k∈n #+ 1}) = (∑{⟨k,x⟩. k∈n}) ⊕ x" by (rule seq_sum_pull_one_elem) thus "(n #+ 1)⋅x = n⋅x ⊕ x" by simp qed text‹One element of a monoid is that element.› lemma (in monoid1) nat_mult_one: assumes "x∈G" shows "1⋅x = x" proof - from assms have "(0 #+ 1)⋅x = 0⋅x ⊕ x" using nat_mult_add_one(1) by blast with assms show ?thesis using nat_mult_zero unit_is_neutral by simp qed text‹Multiplication of $x$ by a natural number induces a homomorphism between natural numbers with addition and and the natural multiples of $x$. › lemma (in monoid1) nat_mult_add: assumes "n∈nat" "m∈nat" "x∈G" shows "(n #+ m)⋅x = n⋅x ⊕ m⋅x" proof - from assms have "m∈nat" and "(n #+ 0)⋅x = n⋅x ⊕ 0⋅x" using nat_mult_type unit_is_neutral nat_mult_zero by simp_all moreover from assms(1,3) have "∀k∈nat. (n #+ k)⋅x = n⋅x ⊕ k⋅x ⟶ (n #+ (k #+ 1))⋅x = n⋅x ⊕ (k #+ 1)⋅x" using nat_mult_type nat_mult_add_one(1) sum_associative by simp ultimately show ?thesis by (rule ind_on_nat1) qed end