theory Monoid_ZF_1 imports Monoid_ZF FiniteSeq_ZF
begin
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}\)).
Notation and basic properties of sums of lists of monoid elements
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.
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 +
defines \( 0 \equiv \text{ TheNeutralElement}(G,f) \)
defines \( \sum s \equiv \text{Fold}(f, 0 ,s) \)
defines \( n\cdot x \equiv \sum \{\langle k,x\rangle .\ k\in n\} \)
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 \( 0 \in G \) and \( f:G\times G \rightarrow G \) using monoidAssum, unit_is_neutral unfolding IsAmonoid_def, IsAssociative_defThe sum of a list of monoid elements is a monoid element.
lemma (in monoid1) sum_in_mono:
assumes \( n\in nat \), \( \forall k\in n.\ q(k)\in G \)
shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \in G \)proof let \( a = \{\langle k,q(k)\rangle .\ k\in n\} \)
from assms have \( n \in nat \), \( f:G\times G \rightarrow G \), \( a:n \rightarrow G \), \( 0 \in G \), \( G\neq 0 \) using zero_monoid_oper, ZF_fun_from_total
then show \( thesis \) using fold_props
qed
A different expression of the fact the sum of a list valued in monoid is a monoid element.
lemma (in monoid1) sum_in_mono1:
assumes \( n\in nat \), \( b:n\rightarrow G \)
shows \( (\sum b) \in G \)proof from assms have \( (\sum \{\langle k,b(k)\rangle .\ k\in n\}) \in G \) using apply_funtype, sum_in_mono
with assms(2) show \( (\sum b) \in G \) using fun_is_set_of_pairs
qed
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\rightarrow G \)
shows \( (\sum s) = 0 \) using assms, zero_monoid_oper, fold_empty, group0_1_L3AFor nonempty lists our \(\Sigma\) is the same as Fold1.
lemma (in monoid1) sum_nonempty:
assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)
shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \)proof from assms have \( s(0) \in G \) using empty_in_every_succ, apply_funtype
with assms have \( (\sum s) = \text{Fold}(f, 0 \oplus s(0), \text{Tail}(s)) \) using zero_monoid_oper, fold_detach_first
with \( s(0) \in G \) show \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \) using unit_is_neutral
then show \( (\sum s) = \text{Fold1}(f,s) \) unfolding Fold1_def
qed
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 \in nat \), \( s:succ(n)\rightarrow G \)
shows \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \)proof from assms have \( s(0) \in G \) using empty_in_every_succ, apply_funtype
{
assume \( n=0 \)
with assms have \( \text{Tail}(s):0\rightarrow G \) using tail_props(1)
with assms, \( s(0) \in G \) have \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \) using sum_nonempty(1), sum_empty, zero_monoid_oper(2), group0_1_L3A, fold_empty, unit_is_neutral
moreover {
}
ultimately show \( thesis \)
qed
assume \( n\neq 0 \)
with assms(1) obtain \( m \) where \( m\in nat \) and \( n = succ(m) \) using Nat_ZF_1_L3
with assms have \( \text{Tail}(s):succ(m)\rightarrow G \) using tail_props(1)
let \( a = \{\langle 0,s(0)\rangle \} \)
from \( s(0) \in G \) have \( 0\in nat \), \( a:succ(0)\rightarrow G \) using pair_func_singleton, succ_explained
with \( m\in nat \), \( \text{Tail}(s):succ(m)\rightarrow G \) have \( f\langle \text{Fold1}(f,a), \text{Fold1}(f, \text{Tail}(s))\rangle = \text{Fold1}(f, \text{Concat}(a, \text{Tail}(s))) \) using semigr0_valid_in_monoid0, prod_conc_distr
with assms, \( a:succ(0)\rightarrow G \), \( m\in nat \), \( \text{Tail}(s):succ(m)\rightarrow G \) have \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \) using semigr0_valid_in_monoid0, prod_of_1elem, pair_val, sum_nonempty(2), first_concat_tail
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 \in nat \), \( \forall k\in n + 1.\ q(k) \in G \)
shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \), \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \)proof let \( s = \{\langle k,q(k)\rangle .\ k\in n + 1\} \)
from assms(1) have \( 0 \in n + 1 \) using empty_in_every_succ, succ_add_one(1)
then have \( s(0) = q(0) \) by (rule ZF_fun_from_tot_val1 )
from assms(2) have \( s: n + 1 \rightarrow G \) by (rule ZF_fun_from_total )
with assms(1), \( s(0) = q(0) \) have \( (\sum s) = q(0) \oplus (\sum \text{Tail}(s)) \) using seq_sum_pull_first0
moreover
from assms have \( \text{Tail}(s) = \{\langle k,q(k + 1)\rangle .\ k \in n\} \) using tail_formula
ultimately show \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \)
from assms show \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \) using zero_monoid_oper, fold_detach_last
qed
If we append an element to a list then its sum increases by that element.
lemma (in monoid1) seq_sum_append:
assumes \( n\in nat \), \( s:n\rightarrow G \), \( x\in G \)
shows \( (\sum \text{Append}(s,x)) = (\sum s)\oplus x \)proof let \( q = \text{Append}(s,x) \)
from assms have \( q:n + 1 \rightarrow G \) and I: \( \forall k\in n + 1.\ q(k)\in G \) and II: \( \forall k\in n.\ q(k) = s(k) \), \( q(n) = x \) using append_props, apply_funtype
from \( q:n + 1 \rightarrow G \) have \( q = \{\langle k,q(k)\rangle .\ k\in n + 1\} \) using fun_is_set_of_pairs
hence \( (\sum q) = (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) \)
also
qed
from assms(1), I have \( .\ .\ .\ = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \) using seq_sum_pull_one_elem(2)
also from assms(2), II have \( .\ .\ .\ = (\sum s) \oplus x \) using fun_is_set_of_pairs
finally show \( (\sum q) = (\sum s) \oplus x \)
The sum of a nonempty list is the sum of its init plus the last element.
lemma (in monoid1) seq_sum_init_last:
assumes \( n\in nat \), \( s:(n + 1)\rightarrow G \)
shows \( (\sum s) = (\sum \text{Init}(s))\oplus (s(n)) \)proof from assms have \( \text{Init}(s):n\rightarrow G \), \( s= \text{Append}( \text{Init}(s),s(n)) \), \( s(n)\in G \) using init_props(1,3), nat_less_add_one(2), apply_funtype
with assms(1), \( \text{Init}(s):n\rightarrow G \), \( s(n)\in G \) show \( thesis \) using seq_sum_append
qed
Sum of concatenation of two lists is the sum of sums.
lemma (in monoid1) seq_sum_concat:
assumes \( n\in nat \), \( s:n\rightarrow G \), \( m\in nat \), \( q:m\rightarrow G \)
shows \( (\sum \text{Concat}(s,q)) = (\sum s)\oplus (\sum q) \)proof from assms(1,2) have I: \( \forall r\in 0\rightarrow G.\ (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r) \) using sum_empty, fun_empty_empty, concat_empty(1), sum_in_mono1, unit_is_neutral
have \( \forall k\in nat.\ ((\forall r\in k\rightarrow G.\ (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r))\)
\( \longrightarrow (\forall r\in (k + 1)\rightarrow G.\ (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r))) \)proof
{
}
}
fix \( k \)
assume \( k\in nat \)
assume A: \( (\forall r\in k\rightarrow G.\ (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r)) \)
{
fix \( r \)
assume \( r:(k + 1)\rightarrow G \)
with assms(1,2), \( k\in nat \) have \( \text{Init}(r):k\rightarrow G \), \( r(k)\in G \) and T1: \( (\sum s)\in G \), \( (\sum \text{Init}(r))\in G \) and T2: \( \text{Concat}(s, \text{Init}(r)):(n + k)\rightarrow G \) using init_props(1), nat_less_add_one(2), apply_funtype, sum_in_mono1, concat_props(1)
from assms(1,2), \( k\in nat \), \( r:(k + 1)\rightarrow G \) have \( (\sum \text{Concat}(s,r)) = \sum \text{Append}( \text{Concat}(s, \text{Init}(r)),r(k)) \) using concat_init_last_elem
also
from T2, \( r(k)\in G \), A, \( \text{Init}(r):k\rightarrow G \) have \( .\ .\ .\ = ((\sum s)\oplus (\sum \text{Init}(r)))\oplus (r(k)) \) using seq_sum_append
also from T1, \( r(k)\in G \), \( k\in nat \), \( r:(k + 1)\rightarrow G \) have \( .\ .\ .\ = (\sum s)\oplus (\sum r) \) using sum_associative, seq_sum_init_last
finally have \( (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r) \)
hence \( \forall r\in (k + 1)\rightarrow G.\ (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r) \)
thus \( thesis \)
qed
with assms(3), I have \( (\forall r\in m\rightarrow G.\ (\sum \text{Concat}(s,r)) = (\sum s)\oplus (\sum r)) \) by (rule ind_on_nat1 )
with assms(4) show \( (\sum \text{Concat}(s,q)) = (\sum s)\oplus (\sum q) \)
qed
The sum of a singleton list is its only element,
lemma (in monoid1) seq_sum_singleton:
assumes \( q(0) \in G \)
shows \( (\sum \{\langle k,q(k)\rangle .\ k\in 1\}) = q(0) \)proof from assms have \( 0\in nat \) and \( \forall k\in 0 + 1.\ q(k) \in G \)
then have \( (\sum \{\langle k,q(k)\rangle .\ k\in 0 + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in 0\}) \) by (rule seq_sum_pull_one_elem )
with assms show \( thesis \) using sum_empty, unit_is_neutral
qed
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 \text{ is commutative on } G \), \( n\in nat \) and \( a : n + 1 \rightarrow G \), \( b : n + 1 \rightarrow G \), \( c : n + 1 \rightarrow G \) and \( \forall j\in n + 1.\ c(j) = a(j) \oplus b(j) \)
shows \( (\sum c) = (\sum a) \oplus (\sum b) \) using assms, succ_add_one(1), sum_nonempty, semigr0_valid_in_monoid0, prod_comm_distribAnother 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 \text{ is commutative on } G \), \( n\in nat \) and \( \forall k\in n.\ p(k) \in G \), \( \forall k\in n.\ q(k) \in G \)
shows \( (\sum \{\langle k,p(k)\oplus q(k)\rangle .\ k\in n\}) = (\sum \{\langle k,p(k)\rangle .\ k\in n\}) \oplus (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \)proof let \( a = \{\langle k,p(k)\rangle .\ k\in n\} \)
let \( b = \{\langle k,q(k)\rangle .\ k\in n\} \)
let \( c = \{\langle k,p(k)\oplus q(k)\rangle .\ k\in n\} \)
{
assume \( n=0 \)
then have \( (\sum c) = (\sum a) \oplus (\sum b) \) using sum_empty, unit_is_neutral
moreover {
}
ultimately show \( thesis \)
qed
assume \( n\neq 0 \)
with assms(2) obtain \( m \) where \( m\in nat \) and \( n = m + 1 \) using nat_not0_succ
from assms(3,4) have \( a:n\rightarrow G \), \( b:n\rightarrow G \), \( c:n\rightarrow G \) using group0_1_L1, ZF_fun_from_total
with assms(1), \( m\in nat \), \( n = m + 1 \) have \( f \text{ is commutative on } G \), \( m\in nat \) and \( a:m + 1\rightarrow G \), \( b:m + 1\rightarrow G \), \( c:m + 1\rightarrow G \)
moreover
have \( \forall k\in m + 1.\ c(k) = a(k) \oplus b(k) \)proof
ultimately have \( (\sum c) = (\sum a) \oplus (\sum b) \) using sum_comm_distrib0
{
}
fix \( k \)
assume \( k \in m + 1 \)
with \( n = m + 1 \) have \( k\in n \)
then have \( c(k) = a(k) \oplus b(k) \) using ZF_fun_from_tot_val1
thus \( thesis \)
qed
Multiplying monoid elements by natural numbers
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.
Another way of looking at a multiple of a monoid element: it's a sum of the cartesian product of \(n\) and the singleton \(\{x\}\). This is because the expression \(\{\langle k,x\rangle : k\in n\}\) in the defintion of the notation for natural multiple i.e. a constant list of the length \(n\) is the same as the set \(n\times\{ x\}\).
lemma (in monoid1) monoid_nat_mult_def_alt:
shows \( n\cdot x = \sum n\times \{x\} \) using const_fun_def_alt, const_fun_def_alt1The zero's multiple of a monoid element is its neutral element.
lemma (in monoid1) nat_mult_zero:
shows \( 0\cdot x = 0 \) using sum_emptyAny multiple of a monoid element is a monoid element.
lemma (in monoid1) nat_mult_type:
assumes \( n\in nat \), \( x\in G \)
shows \( n\cdot x \in G \) using assms, sum_in_monoTaking one more multiple of \(x\) adds \(x\).
lemma (in monoid1) nat_mult_add_one:
assumes \( n\in nat \), \( x\in G \)
shows \( (n + 1)\cdot x = n\cdot x \oplus x \) and \( (n + 1)\cdot x = x \oplus n\cdot x \)proof from assms(2) have I: \( \forall k\in n + 1.\ x \in G \)
with assms(1) have \( (\sum \{\langle k,x\rangle .\ k \in n + 1\}) = x \oplus (\sum \{\langle k,x\rangle .\ k\in n\}) \) by (rule seq_sum_pull_one_elem )
thus \( (n + 1)\cdot x = x \oplus n\cdot x \)
from assms(1), I have \( (\sum \{\langle k,x\rangle .\ k\in n + 1\}) = (\sum \{\langle k,x\rangle .\ k\in n\}) \oplus x \) by (rule seq_sum_pull_one_elem )
thus \( (n + 1)\cdot x = n\cdot x \oplus x \)
qed
One element of a monoid is that element.
lemma (in monoid1) nat_mult_one:
assumes \( x\in G \)
shows \( 1\cdot x = x \)proof from assms have \( (0 + 1)\cdot x = 0\cdot x \oplus x \) using nat_mult_add_one(1)
with assms show \( thesis \) using nat_mult_zero, unit_is_neutral
qed
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\in nat \), \( m\in nat \), \( x\in G \)
shows \( (n + m)\cdot x = n\cdot x \oplus m\cdot x \)proof from assms have \( m\in nat \) and \( (n + 0)\cdot x = n\cdot x \oplus 0\cdot x \) using nat_mult_type, unit_is_neutral, nat_mult_zero
moreover
qed
from assms(1,3) have \( \forall k\in nat.\ (n + k)\cdot x = n\cdot x \oplus k\cdot x \longrightarrow (n + (k + 1))\cdot x = n\cdot x \oplus (k + 1)\cdot x \) using nat_mult_type, nat_mult_add_one(1), sum_associative
ultimately show \( thesis \) by (rule ind_on_nat1 )
The neutral element is fixed by this operation.
lemma (in monoid1) nat_mult_neutral:
assumes \( n\in nat \)
shows \( n\cdot 0 = 0 \)proof from assms have \( n\in nat \) and \( 0\cdot 0 = 0 \) using nat_mult_zero
moreover
qed
have \( \forall k\in nat.\ k\cdot 0 = 0 \longrightarrow (k + 1)\cdot 0 = 0 \) using nat_mult_add_one, nat_mult_one, unit_is_neutral
ultimately show \( thesis \) by (rule ind_on_nat1 )
Chains weighted in a monoid
In the FiniteSeq_ZF theory we define the notions of chains, which are essentially lists of points of some set \(X\) and their chain links, which are lists of elements of \(X\times X\). Here we consider what happens when the chain intervals are composed with a function valued in a monoid.
For a chain \(c\) and a weight function \(w:X\times X\rightarrow G\) we define the chain weight as the sum of its intervals composed with \(w\).
definition (in monoid1)
\( \text{ChainWeight}(w,c) \equiv \sum (w\circ \text{ChainLinks}(c)) \)
If \(c\) is a chain in \(X\) of a natural length \(n\) connecting \(x\) and \(y\) and if the weight function \(w\) maps \(X\times X\) to the monoid \(G\), then the weight of the chain \(c\) is an element of \(G\).
lemma (in monoid1) chain_weight_type:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( w:X\times X\rightarrow G \)
shows \( \text{ChainWeight}(w,c) \in G \) using assms, chain_links_fun(2), comp_fun, sum_in_mono1 unfolding ChainWeight_defThe weight of the concatenation of chains is equal to the weight of the first chain plus the the weight of the link connecting the chains plus the weight of the second chain.
lemma (in monoid1) chain_concat_weight:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x_1,y_1) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,x_2,y_2) \) and \( w:X\times X\rightarrow G \)
shows \( \text{ChainWeight}(w, \text{Concat}(c_1,c_2)) = \) \( \text{ChainWeight}(w,c_1)\oplus (w\langle y_1,x_2\rangle )\oplus \text{ChainWeight}(w,c_2) \)proof let \( L_1 = \text{ChainLinks}(c_1) \)
let \( L_2 = \text{ChainLinks}(c_2) \)
from assms(1,2) have \( y_1\in X \) using chain_props(5)
from assms(3,4) have \( x_2\in X \) using chain_props(4)
from assms(1,2,3,4), \( y_1\in X \), \( x_2\in X \) have \( L_1:n_1\rightarrow X\times X \), \( L_2:n_2\rightarrow X\times X \), \( \langle y_1,x_2\rangle \in X\times X \) and \( \text{Append}(L_1,\langle y_1,x_2\rangle ):(n_1 + 1)\rightarrow X\times X \) using chain_links_fun(2), append_props(1)
with assms(1,3,5), \( L_2:n_2\rightarrow X\times X \) have I: \( w\circ \text{Concat}( \text{Append}(L_1,\langle y_1,x_2\rangle ),L_2) = \)
\( \text{Concat}(w\circ \text{Append}(L_1,\langle y_1,x_2\rangle ), w\circ L_2) \) using list_compose_concat
from assms(1,5), \( L_1:n_1\rightarrow X\times X \), \( L_2:n_2\rightarrow X\times X \), \( \langle y_1,x_2\rangle \in X\times X \) have \( (w\circ L_1):n_1\rightarrow G \), \( (w\circ L_2): n_2\rightarrow G \), \( w\langle y_1,x_2\rangle \in G \) and II: \( \text{Append}(w\circ L_1,w(\langle y_1,x_2\rangle )):(n_1 + 1)\rightarrow G \) using comp_fun, apply_funtype, append_props(1)
from assms(1,2,3,4), I have \( \text{ChainWeight}(w, \text{Concat}(c_1,c_2)) = \)
\( \sum \text{Concat}(w\circ \text{Append}(L_1,\langle y_1,x_2\rangle ), w\circ L_2) \) unfolding ChainWeight_def using concat_chains(4)
also
qed
from assms(1,5), \( L_1:n_1\rightarrow X\times X \), \( \langle y_1,x_2\rangle \in X\times X \) have \( .\ .\ .\ = \sum \text{Concat}( \text{Append}(w\circ L_1,w(\langle y_1,x_2\rangle )), w\circ L_2) \) using list_compose_append(2)
also from assms(1,3), II, \( (w\circ L_2): n_2\rightarrow G \) have \( .\ .\ .\ = (\sum \text{Append}(w\circ L_1,w\langle y_1,x_2\rangle ))\oplus (\sum (w\circ L_2)) \) using seq_sum_concat
also from assms(1), \( (w\circ L_1):n_1\rightarrow G \), \( w\langle y_1,x_2\rangle \in G \) have \( .\ .\ .\ = \text{ChainWeight}(w,c_1)\oplus (w\langle y_1,x_2\rangle )\oplus \text{ChainWeight}(w,c_2) \) using seq_sum_append unfolding ChainWeight_def
finally show \( thesis \)
If, in addition to assumptions of chain_weight_concat the weight function \(w\) vanishes on the diagonal and the first chain ends at the beginning of the second one, then the weight of the concatenated chain is the sum of the chain weights.
lemma (in monoid1) chain_concat_weight1:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x,y) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,y,z) \) and \( w:X\times X\rightarrow G \), \( \forall x\in X.\ w\langle x,x\rangle = 0 \)
shows \( \text{ChainWeight}(w, \text{Concat}(c_1,c_2)) = \text{ChainWeight}(w,c_1)\oplus \text{ChainWeight}(w,c_2) \)proof from assms(1,2) have \( y\in X \) using chain_props(5)
with assms show \( thesis \) using chain_weight_type, chain_concat_weight, unit_is_neutral
qed
end
lemma (in monoid0) unit_is_neutral:
assumes \( e = \text{ TheNeutralElement}(G,f) \)
shows \( e \in G \wedge (\forall g\in G.\ e \oplus g = g \wedge g \oplus e = g) \)Definition of IsAmonoid:
\( \text{IsAmonoid}(G,f) \equiv \)
\( f \text{ is associative on } G \wedge \)
\( (\exists e\in G.\ (\forall g\in G.\ ( (f(\langle e,g\rangle ) = g) \wedge (f(\langle g,e\rangle ) = g)))) \)
Definition of IsAssociative:
\( P \text{ is associative on } G \equiv P : G\times G\rightarrow G \wedge \)
\( (\forall x \in G.\ \forall y \in G.\ \forall z \in G.\ \)
\( ( P(\langle P(\langle x,y\rangle ),z\rangle ) = P( \langle x,P(\langle y,z\rangle )\rangle ))) \)
lemma (in monoid1) zero_monoid_oper: shows \( 0 \in G \) and \( f:G\times G \rightarrow G \)
lemma ZF_fun_from_total:
assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \) theorem fold_props:
assumes \( n \in nat \) and \( f : X\times Y \rightarrow X \), \( a:n \rightarrow Y \), \( x\in X \), \( Y\neq 0 \)
shows \( \text{Fold}(f,x,a) = \text{FoldSeq}(f,x,a)(n) \) and \( \text{Fold}(f,x,a) \in X \) lemma (in monoid1) sum_in_mono:
assumes \( n\in nat \), \( \forall k\in n.\ q(k)\in G \)
shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \in G \) theorem fun_is_set_of_pairs:
assumes \( f:X\rightarrow Y \)
shows \( f = \{\langle x,f(x)\rangle .\ x \in X\} \) theorem fold_empty:
assumes \( f : X\times Y \rightarrow X \) and \( a:0\rightarrow Y \), \( x\in X \), \( Y\neq 0 \)
shows \( \text{Fold}(f,x,a) = x \) lemma (in monoid0) group0_1_L3A: shows \( G\neq 0 \)
lemma empty_in_every_succ:
assumes \( n \in nat \)
shows \( 0 \in succ(n) \) lemma fold_detach_first:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( y:succ(n)\rightarrow Y \), \( x\in X \)
shows \( \text{Fold}(f,x,y) = \text{Fold}(f,f\langle x,y(0)\rangle , \text{Tail}(y)) \)Definition of Fold1:
\( \text{Fold1}(f,a) \equiv \text{Fold}(f,a(0), \text{Tail}(a)) \)
theorem tail_props:
assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)
shows \( \text{Tail}(a) : n \rightarrow X \), \( \forall k \in n.\ \text{Tail}(a)(k) = a(succ(k)) \) lemma (in monoid1) sum_nonempty:
assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)
shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \) lemma (in monoid1) sum_empty:
assumes \( s:0\rightarrow G \)
shows \( (\sum s) = 0 \) lemma (in monoid1) zero_monoid_oper: shows \( 0 \in G \) and \( f:G\times G \rightarrow G \)
lemma Nat_ZF_1_L3:
assumes \( n \in nat \) and \( n\neq 0 \)
shows \( \exists k\in nat.\ n = succ(k) \) lemma pair_func_singleton:
assumes \( y \in Y \)
shows \( \{\langle x,y\rangle \} : \{x\} \rightarrow Y \) lemma succ_explained: shows \( succ(n) = n \cup \{n\} \)
lemma (in monoid0) semigr0_valid_in_monoid0: shows \( semigr0(G,f) \)
theorem (in semigr0) prod_conc_distr:
assumes \( n \in nat \), \( k \in nat \) and \( a : succ(n) \rightarrow G \), \( b: succ(k) \rightarrow G \)
shows \( (\prod a) \cdot (\prod b) = \prod (a \sqcup b) \) lemma (in semigr0) prod_of_1elem:
assumes \( a: 1 \rightarrow G \)
shows \( (\prod a) = a(0) \) lemma pair_val: shows \( \{\langle x,y\rangle \}(x) = y \)
lemma (in monoid1) sum_nonempty:
assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)
shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \) lemma first_concat_tail:
assumes \( n\in nat \), \( a:succ(n)\rightarrow X \)
shows \( a = \text{Concat}(\{\langle 0,a(0)\rangle \}, \text{Tail}(a)) \) lemma succ_add_one:
assumes \( n\in nat \)
shows \( n + 1 = succ(n) \), \( n + 1 \in nat \), \( \{0\} + n = succ(n) \), \( n + \{0\} = succ(n) \), \( succ(n) \in nat \), \( 0 \in n + 1 \), \( n \subseteq n + 1 \) lemma ZF_fun_from_tot_val1:
assumes \( x\in X \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\}(x)=b(x) \) lemma (in monoid1) seq_sum_pull_first0:
assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)
shows \( (\sum s) = s(0) \oplus (\sum \text{Tail}(s)) \) lemma tail_formula:
assumes \( n \in nat \) and \( \forall k \in n + 1.\ q(k) \in X \)
shows \( \text{Tail}(\{\langle k,q(k)\rangle .\ k \in n + 1\}) = \{\langle k,q(k + 1)\rangle .\ k \in n\} \) lemma fold_detach_last:
assumes \( n \in nat \), \( f : X\times Y \rightarrow X \), \( x\in X \), \( \forall k\in n + 1.\ q(k) \in Y \)
shows \( \text{Fold}(f,x,\{\langle k,q(k)\rangle .\ k\in n + 1\}) = f\langle \text{Fold}(f,x,\{\langle k,q(k)\rangle .\ k\in n\}), q(n)\rangle \) theorem append_props:
assumes \( a: n \rightarrow X \) and \( x\in X \) and \( b = \text{Append}(a,x) \)
shows \( b : succ(n) \rightarrow X \), \( \forall k\in n.\ b(k) = a(k) \), \( b(n) = x \) theorem (in monoid1) seq_sum_pull_one_elem:
assumes \( n \in nat \), \( \forall k\in n + 1.\ q(k) \in G \)
shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \), \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \) theorem init_props:
assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)
shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \) lemma nat_less_add_one:
assumes \( n\in nat \)
shows \( n \lt n + 1 \) and \( n \in n + 1 \) lemma (in monoid1) seq_sum_append:
assumes \( n\in nat \), \( s:n\rightarrow G \), \( x\in G \)
shows \( (\sum \text{Append}(s,x)) = (\sum s)\oplus x \) lemma fun_empty_empty: shows \( (f:\emptyset \rightarrow X) \longleftrightarrow f=\emptyset \)
lemma concat_empty:
assumes \( n\in nat \), \( x:n\rightarrow X \)
shows \( \text{Concat}(x,\emptyset ) = x \) and \( \text{Concat}(\emptyset ,x) = x \) lemma (in monoid1) sum_in_mono1:
assumes \( n\in nat \), \( b:n\rightarrow G \)
shows \( (\sum b) \in G \) theorem init_props:
assumes \( n \in nat \) and \( a: succ(n) \rightarrow X \)
shows \( \text{Init}(a) : n \rightarrow X \), \( \forall k\in n.\ \text{Init}(a)(k) = a(k) \), \( a = \text{Append}( \text{Init}(a), a(n)) \) theorem concat_props:
assumes \( n \in nat \), \( k \in nat \) and \( a:n\rightarrow X \), \( b:k\rightarrow X \)
shows \( \text{Concat}(a,b): n + k \rightarrow X \), \( \forall i\in n.\ \text{Concat}(a,b)(i) = a(i) \), \( \forall i \in \text{NatInterval}(n,k).\ \text{Concat}(a,b)(i) = b(i - n) \), \( \forall j \in k.\ \text{Concat}(a,b)(n + j) = b(j) \) lemma concat_init_last_elem:
assumes \( n \in nat \), \( k \in nat \) and \( a: n \rightarrow X \) and \( b : succ(k) \rightarrow X \)
shows \( \text{Append}( \text{Concat}(a, \text{Init}(b)),b(k)) = \text{Concat}(a,b) \) lemma (in monoid0) sum_associative:
assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( (a\oplus b)\oplus c = a\oplus (b\oplus c) \) lemma (in monoid1) seq_sum_init_last:
assumes \( n\in nat \), \( s:(n + 1)\rightarrow G \)
shows \( (\sum s) = (\sum \text{Init}(s))\oplus (s(n)) \) lemma ind_on_nat1:
assumes \( n\in nat \) and \( P(0) \) and \( \forall k\in nat.\ P(k)\longrightarrow P(k + 1) \)
shows \( P(n) \) theorem (in monoid1) seq_sum_pull_one_elem:
assumes \( n \in nat \), \( \forall k\in n + 1.\ q(k) \in G \)
shows \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = q(0) \oplus (\sum \{\langle k,q(k + 1)\rangle .\ k\in n\}) \), \( (\sum \{\langle k,q(k)\rangle .\ k\in n + 1\}) = (\sum \{\langle k,q(k)\rangle .\ k\in n\}) \oplus q(n) \) lemma (in monoid1) sum_nonempty:
assumes \( n \in nat \), \( s:succ(n)\rightarrow G \)
shows \( (\sum s) = \text{Fold}(f,s(0), \text{Tail}(s)) \), \( (\sum s) = \text{Fold1}(f,s) \) theorem (in semigr0) prod_comm_distrib:
assumes \( f \text{ is commutative on } G \) and \( n\in nat \) and \( a : succ(n)\rightarrow G \), \( b : succ(n)\rightarrow G \), \( c : succ(n)\rightarrow G \) and \( \forall j\in succ(n).\ c(j) = a(j) \cdot b(j) \)
shows \( (\prod c) = (\prod a) \cdot (\prod b) \) lemma nat_not0_succ:
assumes \( n\in nat \), \( n\neq 0 \)
shows \( \exists m\in nat.\ n = m + 1 \) lemma (in monoid0) group0_1_L1:
assumes \( a\in G \), \( b\in G \)
shows \( a\oplus b \in G \) lemma (in monoid1) sum_comm_distrib0:
assumes \( f \text{ is commutative on } G \), \( n\in nat \) and \( a : n + 1 \rightarrow G \), \( b : n + 1 \rightarrow G \), \( c : n + 1 \rightarrow G \) and \( \forall j\in n + 1.\ c(j) = a(j) \oplus b(j) \)
shows \( (\sum c) = (\sum a) \oplus (\sum b) \) lemma const_fun_def_alt: shows \( \text{ConstantFunction}(X,c) = \{\langle x,c\rangle .\ x\in X\} \)
lemma const_fun_def_alt1: shows \( \text{ConstantFunction}(X,c) = X\times \{c\} \)
lemma (in monoid1) nat_mult_add_one:
assumes \( n\in nat \), \( x\in G \)
shows \( (n + 1)\cdot x = n\cdot x \oplus x \) and \( (n + 1)\cdot x = x \oplus n\cdot x \) lemma (in monoid1) nat_mult_zero: shows \( 0\cdot x = 0 \)
lemma (in monoid1) nat_mult_type:
assumes \( n\in nat \), \( x\in G \)
shows \( n\cdot x \in G \) lemma (in monoid1) nat_mult_add_one:
assumes \( n\in nat \), \( x\in G \)
shows \( (n + 1)\cdot x = n\cdot x \oplus x \) and \( (n + 1)\cdot x = x \oplus n\cdot x \) lemma (in monoid1) nat_mult_one:
assumes \( x\in G \)
shows \( 1\cdot x = x \) lemma chain_links_fun:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( domain(c) - 1 = n \) and \( \text{ChainLinks}(c):n\rightarrow X\times X \)Definition of ChainWeight:
\( \text{ChainWeight}(w,c) \equiv \sum (w\circ \text{ChainLinks}(c)) \)
lemma chain_props:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( c \in (n + 1)\rightarrow X \), \( c(0) = x \), \( c(n) = y \), \( x\in X \), \( y\in X \) lemma chain_props:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \)
shows \( c \in (n + 1)\rightarrow X \), \( c(0) = x \), \( c(n) = y \), \( x\in X \), \( y\in X \) theorem append_props:
assumes \( a: n \rightarrow X \) and \( x\in X \) and \( b = \text{Append}(a,x) \)
shows \( b : succ(n) \rightarrow X \), \( \forall k\in n.\ b(k) = a(k) \), \( b(n) = x \) lemma list_compose_concat:
assumes \( n \in nat \), \( m\in nat \), \( a:n\rightarrow X \), \( b:m\rightarrow X \), \( c:X\rightarrow Y \)
shows \( c\circ \text{Concat}(a,b) = \text{Concat}(c\circ a, c\circ b) \) lemma concat_chains:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x_1,y_1) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,x_2,y_2) \)
defines \( c_3 \equiv \text{Concat}(c_1,c_2) \)
shows \( c_3 \in \text{Chains}(X,n_1 + n_2 + 1,x_1,y_2) \), \( \text{ChainLinks}(c_3): (n_1 + n_2 + 1)\rightarrow X\times X \), \( \text{ChainLinks}(c_3) = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle c_1(n_1),c_2(0)\rangle ), \text{ChainLinks}(c_2)) \), \( \text{ChainLinks}(c_3) = \text{Concat}( \text{Append}( \text{ChainLinks}(c_1),\langle y_1,x_2\rangle ), \text{ChainLinks}(c_2)) \) lemma list_compose_append:
assumes \( n \in nat \) and \( a : n \rightarrow X \) and \( x \in X \) and \( c : X \rightarrow Y \)
shows \( c\circ \text{Append}(a,x) : succ(n) \rightarrow Y \), \( c\circ \text{Append}(a,x) = \text{Append}(c\circ a, c(x)) \) lemma (in monoid1) seq_sum_concat:
assumes \( n\in nat \), \( s:n\rightarrow G \), \( m\in nat \), \( q:m\rightarrow G \)
shows \( (\sum \text{Concat}(s,q)) = (\sum s)\oplus (\sum q) \) lemma (in monoid1) chain_weight_type:
assumes \( n\in nat \), \( c\in \text{Chains}(X,n,x,y) \), \( w:X\times X\rightarrow G \)
shows \( \text{ChainWeight}(w,c) \in G \) lemma (in monoid1) chain_concat_weight:
assumes \( n_1\in nat \), \( c_1\in \text{Chains}(X,n_1,x_1,y_1) \), \( n_2\in nat \), \( c_2\in \text{Chains}(X,n_2,x_2,y_2) \) and \( w:X\times X\rightarrow G \)
shows \( \text{ChainWeight}(w, \text{Concat}(c_1,c_2)) = \) \( \text{ChainWeight}(w,c_1)\oplus (w\langle y_1,x_2\rangle )\oplus \text{ChainWeight}(w,c_2) \)
This page by Sławomir Kołodyński is licensed under CC BY 4.0. BTC: 189qAMLvqevxMrCsZaABMJ3cLkXdSwMNK8
