Theory Monoid_ZF_1

(* 
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


textThis 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}$). 

subsectionNotation and basic properties of sums of lists of monoid elements

textIn 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. 

textThe 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]: "nx  {k,x. kn}"

textLet'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

textThe sum of a list of monoid elements is a monoid element.

lemma (in monoid1) sum_in_mono: assumes "nnat" "kn. q(k)G"
  shows "({k,q(k). kn})  G"
proof -
  let ?a = "{k,q(k). kn}"
  from assms have "n  nat" "f:G×G  G" "?a:n  G" "𝟬G" "G0"
    using zero_monoid_oper ZF_fun_from_total by auto
  then show ?thesis using fold_props by simp
qed

textThe 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:0G" shows "(s) = 𝟬"
  using assms zero_monoid_oper fold_empty group0_1_L3A by simp

textFor 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

textWe 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):0G" 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 "n0"
    with assms(1) obtain m where "mnat" 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 "0nat" "?a:succ(0)G"
      using pair_func_singleton succ_explained by simp_all
    with mnat 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 mnat 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

textThe 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" "kn #+ 1. q(k)  G"
  shows 
    "({k,q(k). kn #+ 1}) = q(0)  ({k,q(k #+ 1). kn})"
    "({k,q(k). kn #+ 1}) = ({k,q(k). kn})  q(n)"
proof -
  let ?s = "{k,q(k). kn #+ 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). kn #+ 1}) =  q(0)  ({k,q(k #+ 1). kn})" 
    by simp
  from assms show "({k,q(k). kn #+ 1}) =  ({k,q(k). kn})  q(n)"
    using zero_monoid_oper fold_detach_last by simp
qed

textThe sum of a singleton list is its only element,

lemma (in monoid1) seq_sum_singleton: assumes "q(0)  G"
  shows "({k,q(k). k1}) = q(0)"
proof -
  from assms have "0nat" and "k0 #+ 1. q(k)  G" by simp_all
  then have 
    "({k,q(k). k0 #+ 1}) = q(0)  ({k,q(k #+ 1). k0})"
    by (rule seq_sum_pull_one_elem)
  with assms show ?thesis using sum_empty unit_is_neutral by simp
qed

textIf 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" "nnat" and
  "a : n #+ 1  G"  "b : n #+ 1  G"  "c : n #+ 1  G" and
  "jn #+ 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

textAnother 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" "nnat" and
  "kn. p(k)  G" "kn. q(k)  G"
  shows 
    "({k,p(k)q(k). kn}) = ({k,p(k). kn})  ({k,q(k). kn})" 
proof -
  let ?a = "{k,p(k). kn}"
  let ?b = "{k,q(k). kn}"
  let ?c = "{k,p(k)q(k). kn}"
  { assume "n=0"
    then have "(?c) = (?a)  (?b)"
      using sum_empty unit_is_neutral by simp
  }
  moreover
  { assume "n0"
    with assms(2) obtain m where "mnat" and  "n = m #+ 1"
      using nat_not0_succ by blast
    from assms(3,4) have "?a:nG" "?b:nG" "?c:nG" 
      using group0_1_L1 ZF_fun_from_total by simp_all
    with assms(1) mnat n = m #+ 1 have 
      "f {is commutative on} G" "mnat" and
      "?a:m #+ 1G" "?b:m #+ 1G" "?c:m #+ 1G"
      by simp_all
    moreover have "km #+ 1. ?c`(k) = ?a`(k)  ?b`(k)"
    proof -
      { fix k assume "k  m #+ 1"
        with n = m #+ 1 have "kn" 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

subsectionMultiplying monoid elements by natural numbers

textA 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. 

textThe zero's multiple of a monoid element is its neutral element.

lemma (in monoid1) nat_mult_zero: shows "0x = 𝟬" using sum_empty by simp

textAny multiple of a monoid element is a monoid element.

lemma (in monoid1) nat_mult_type: assumes "nnat" "xG"
  shows "nx  G" using assms sum_in_mono by simp

textTaking one more multiple of $x$ adds $x$. 

lemma (in monoid1) nat_mult_add_one: assumes "nnat" "xG" 
  shows "(n #+ 1)x = nx  x" and "(n #+ 1)x = x  nx"
proof -
  from assms(2) have I: "kn #+ 1. x  G" by simp
  with assms(1) have "({k,x. k  n #+ 1}) = x  ({k,x. kn})"
    by (rule seq_sum_pull_one_elem)
  thus "(n #+ 1)x = x  nx" by simp
  from assms(1) I have "({k,x. kn #+ 1}) =  ({k,x. kn})  x"
    by (rule seq_sum_pull_one_elem)
  thus "(n #+ 1)x = nx  x" by simp
qed

textOne element of a monoid is that element.

lemma (in monoid1) nat_mult_one: assumes "xG" shows "1x = x"
proof -
  from assms have "(0 #+ 1)x = 0x  x" using nat_mult_add_one(1) by blast
  with assms show ?thesis using nat_mult_zero unit_is_neutral by simp
qed

textMultiplication 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 "nnat" "mnat" "xG"
  shows "(n #+ m)x = nx  mx"
proof -
  from assms have "mnat" and "(n #+ 0)x = nx  0x" 
    using nat_mult_type unit_is_neutral nat_mult_zero by simp_all
  moreover from assms(1,3) have
    "knat. (n #+ k)x = nx  kx  (n #+ (k #+ 1))x = nx  (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