IsarMathLib

Proofs by humans, for humans, formally verified by Isabelle/ZF proof assistant

theory IntGroup_ZF imports Int_ZF_1
begin

In the Monoid_ZF_1 theory we consider multiplicities of \(n\cdot x\) of monoid elements, i.e. special cases of expressions of the form \(x_1\oplus x_2\oplus\dots\oplus x_n\) where \(x_i=x\) for \(i=1..n\). In the group context where we usually use multiplicative notation this translates to the "power" \(x^n\) where \(n\in \mathbb{N}\), see also section "Product of a list of group elements" in the Group_ZF theory. In the group setting the notion of raising an element to natural power can be naturally generalized to the notion of raising an element to an integer power.

Properties of natural powers of an element and its inverse

The integer power is defined in terms of natural powers of an element and its inverse. In this section we study properties of expressions \((x^n)\cdot(x^{-1})^k\), where \(x\) is a group element and \(n,k\) are natural numbers.

The natural power of \(x\) multiplied by the same power of \(x^{-1}\) cancel out to give the neutral element of the group.

lemma (in group0) nat_pow_inv_cancel:

assumes \( n\in nat \), \( x\in G \)

shows \( x^{n}\cdot (x^{-1})^{n} = 1 \)proof
from assms(1) have \( n\in nat \) and \( x^{0}\cdot (x^{-1})^{0} = 1 \) using nat_mult_zero, group0_2_L2
moreover
have \( \forall k\in nat.\ x^{k}\cdot (x^{-1})^{k} = 1 \longrightarrow x^{k + 1}\cdot (x^{-1})^{k + 1} = 1 \)proof
{
fix \( k \)
assume \( k\in nat \) and \( x^{k}\cdot (x^{-1})^{k} = 1 \)
from assms(2), \( k\in nat \) have \( x^{k + 1}\cdot (x^{-1})^{k + 1} = x^{k}\cdot x\cdot (x^{-1}\cdot (x^{-1})^{k}) \) using inverse_in_group, nat_pow_add_one
with assms(2), \( k\in nat \), \( x^{k}\cdot (x^{-1})^{k} = 1 \) have \( x^{k + 1}\cdot (x^{-1})^{k + 1} = 1 \) using nat_mult_type, inverse_in_group, rearr4elem_monoid, group0_2_L6(1), group0_2_L2
}
thus \( thesis \)
qed
ultimately show \( thesis \) by (rule ind_on_nat1 )
qed

The natural power of \(x^{-1}\) multiplied by the same power of \(x\) cancel out to give the neutral element of the group. Same as nat_pow_inv_cancel written with \(x^{-1}\) instead of \(x\).

lemma (in group0) nat_pow_inv_cancel1:

assumes \( n\in nat \), \( x\in G \)

shows \( (x^{-1})^{n}\cdot x^{n} = 1 \)proof
from assms have \( (x^{-1})^{n}\cdot ((x^{-1})^{-1})^{n} = 1 \) using inverse_in_group, nat_pow_inv_cancel
with assms(2) show \( (x^{-1})^{n}\cdot x^{n} = 1 \) using group_inv_of_inv
qed

If \(k\leq n\) are natural numbers and \(x\) an element of the group, then \(x^n\cdot (x^{-1})^k = x^(k-n)\).

lemma (in group0) nat_pow_cancel_less:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( x^{n}\cdot (x^{-1})^{k} = x^{n - k} \)proof
from assms have \( k\in nat \), \( n - k \in nat \), \( x^{(n - k)} \in G \), \( x^{k} \in G \), \( (x^{-1})^{k} \in G \) using leq_nat_is_nat, diff_type, nat_mult_type, inverse_in_group
from assms(3), \( k\in nat \), \( n - k \in nat \) have \( x^{(n - k) + k} = x^{(n - k)}\cdot x^{k} \) using nat_mult_add
with assms(1,2), \( x^{(n - k)} \in G \), \( x^{k} \in G \), \( (x^{-1})^{k} \in G \) have \( x^{n}\cdot (x^{-1})^{k} = x^{n - k}\cdot (x^{k}\cdot (x^{-1})^{k}) \) using add_diff_inverse2, group_oper_assoc
with assms(3), \( k\in nat \), \( x^{(n - k)} \in G \) show \( thesis \) using nat_pow_inv_cancel, group0_2_L2
qed

If \(k\leq n\) are natural numbers and \(x\) an element of the group, then \((x^{-1})^n\cdot x^k = (x^{-1})^(k-n)\).

lemma (in group0) nat_pow_cancel_less1:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( (x^{-1})^{n}\cdot x^{k} = (x^{-1})^{n - k} \)proof
from assms have \( (x^{-1})^{n}\cdot ((x^{-1})^{-1})^{k} = (x^{-1})^{n - k} \) using inverse_in_group, nat_pow_cancel_less
with assms(3) show \( thesis \) using group_inv_of_inv
qed

If \(k\leq n\) are natural numbers and \(x\) an element of the group, then \(x^k\cdot (x^{-1})^n = (x^{-1})^(k-n)\).

lemma (in group0) nat_pow_cancel_more:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( (x^{-1})^{k}\cdot x^{n} = x^{n - k} \)proof
from assms have \( k\in nat \), \( n - k \in nat \), \( x^{(n - k)} \in G \), \( x^{k} \in G \), \( (x^{-1})^{k} \in G \) using leq_nat_is_nat, diff_type, nat_mult_type, inverse_in_group
from assms(3), \( k\in nat \), \( n - k \in nat \) have \( x^{k + (n - k)} = x^{k}\cdot x^{(n - k)} \) using nat_mult_add
with assms(1,2), \( x^{(n - k)} \in G \), \( x^{k} \in G \), \( (x^{-1})^{k} \in G \) have \( (x^{-1})^{k}\cdot x^{n} = ((x^{-1})^{k}\cdot x^{k})\cdot x^{n - k} \) using add_diff_inverse, group_oper_assoc
with assms(3), \( k\in nat \), \( x^{(n - k)} \in G \) show \( thesis \) using nat_pow_inv_cancel1, group0_2_L2
qed

If \(k\leq n\) are natural numbers and \(x\) an element of the group, then \((x^{-1})^k\cdot x^n = x^(k-n)\).

lemma (in group0) nat_pow_cancel_more1:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( x^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} \)proof
from assms have \( ((x^{-1})^{-1})^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} \) using inverse_in_group, nat_pow_cancel_more
with assms(3) show \( thesis \) using group_inv_of_inv
qed

Integer powers

In this section we introduce notation basic properties of integer power in group context. The goal is to show that the power homomorphism property: if \(x\) is an element of the group and \(n,m\) are integers then \(x^{n+m}=x^n\cdot x^m\).

We extend the group0 context with some notation from int0 context. We also define notation for the integer power \( x^{z} \). The difficulty there is that in ZF set theory nonnegative integers and natural numbers are different things. However, standard Isabelle/ZF defines a meta-function nat_of that we can use to convert one into the other. Hence, we define the integer power \( x^{z} \) as \(x\) raised to the corresponding natural power if \(z\) is a nonnegative and \(x^{-1}\) raised to natural power corresponding to \(-z\) otherwise.

locale group_int0 = group0 +

defines \( \mathbb{Z} \equiv int \)

defines \( a + b \equiv IntegerAddition\langle a,b\rangle \)

defines \( - a \equiv \text{GroupInv}(\mathbb{Z} ,IntegerAddition)(a) \)

defines \( a - b \equiv a + ( - b) \)

defines \( 0 \equiv \text{ TheNeutralElement}(\mathbb{Z} ,IntegerAddition) \)

defines \( \mathbb{Z} ^+ \equiv \text{Nonnegative}(\mathbb{Z} ,IntegerAddition,IntegerOrder) \)

defines \( m \leq n \equiv \langle m,n\rangle \in IntegerOrder \)

defines \( a \lt b \equiv a\leq b \wedge a\neq b \)

defines \( x^{z} \equiv (\text{if } 0 \leq z\text{ then }x\text{ else }x^{-1})^{| z|_N } \)

If \(x\) is an element of the group and \(z_1,z_2\) are nonnegative integers then \(x^{z_1+z_2}=x^{z_1}\cdot x^{z_2}\), i.e. the power homomorphism property holds.

lemma (in group_int0) powz_hom_nneg_nneg:

assumes \( 0 \leq z_1 \), \( 0 \leq z_2 \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_nonneg_ints(1,2), nat_mult_add

If \(x\) is an element of the group and \(z_1,z_2\) are negative integers then the power homomorphism property holds.

lemma (in group_int0) powz_hom_neg_neg:

assumes \( z_1 \lt 0 \), \( z_2 \lt 0 \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, neg_not_nonneg, add_neg_ints(1,2), inverse_in_group, nat_mult_add

When the integers are of different signs we further split into cases depending on which magnitude is greater. If \(x\) is an element of the group and \(z_1\) is nonnegative, \(z_2\) is negative and \(|z_2|\leq |z_1|\) then the power homomorphism property holds. The proof of this lemma is presented with more detail than necessary, to show the schema of the proofs of the remaining lemmas that we let Isabelle prove automatically.

lemma (in group_int0) powz_hom_nneg_neg1:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)proof
let \( m_1 = \left| z_1 \right|_N \)
let \( m_2 = \left| z_2 \right|_N \)
from assms(1,2,3) have \( x^{z_1 + z_2} = x^{\left| z_1 + z_2 \right|_N } \) using add_nonneg_neg1(1)
also
from assms(1,2,3) have \( .\ .\ .\ = x^{m_1 - m_2} \) using add_nonneg_neg1(2)
also
from assms(3,4) have \( .\ .\ .\ = x^{m_1}\cdot (x^{-1})^{m_2} \) using nat_pow_cancel_less
also
from assms(1,2) have \( .\ .\ .\ = x^{z_1}\cdot x^{z_2} \) using neg_not_nonneg
finally show \( thesis \)
qed

If \(x\) is an element of the group and \(z_1\) is nonnegative, \(z_2\) is negative and \(|z_1|<|z_2|\) then the power homomorphism property holds.

lemma (in group_int0) powz_hom_nneg_neg2:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_1 \right|_N \lt \left| z_2 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_nonneg_neg2, neg_not_nonneg, leI, nat_pow_cancel_more1

If \(x\) is an element of the group and \(z_1\) is negative, \(z_2\) is nonnegative and \(|z_1|\leq |z_2|\) then the power homomorphism property holds.

lemma (in group_int0) powz_hom_neg_nneg1:

assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_1 \right|_N \leq \left| z_2 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_neg_nonneg1, nat_pow_cancel_more, neg_not_nonneg

If \(x\) is an element of the group and \(z_1\) is negative, \(z_2\) is nonnegative and \(|z_2| < |z_1|\) then the power homomorphism property holds.

lemma (in group_int0) powz_hom_neg_nneg2:

assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_2 \right|_N \lt \left| z_1 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \) using assms, add_neg_nonneg2, neg_not_nonneg, leI, nat_pow_cancel_less1

The next theorem collects the results from the above lemmas to show the power homomorphism property holds for any pair of integer numbers and any group element.

theorem (in group_int0) powz_hom_prop:

assumes \( z_1\in \mathbb{Z} \), \( z_2\in \mathbb{Z} \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)proof
from assms(1,2) have \( ( 0 \leq z_1 \wedge 0 \leq z_2) \vee (z_1 \lt 0 \wedge z_2 \lt 0 ) \vee \) \( ( 0 \leq z_1 \wedge z_2 \lt 0 \wedge \left| z_2 \right|_N \leq \left| z_1 \right|_N ) \vee \) \( ( 0 \leq z_1 \wedge z_2 \lt 0 \wedge \left| z_1 \right|_N \lt \left| z_2 \right|_N ) \vee \) \( (z_1 \lt 0 \wedge 0 \leq z_2 \wedge \left| z_1 \right|_N \leq \left| z_2 \right|_N ) \vee \) \( (z_1 \lt 0 \wedge 0 \leq z_2 \wedge \left| z_2 \right|_N \lt \left| z_1 \right|_N ) \) using int_pair_6cases
with assms(3) show \( thesis \) using powz_hom_nneg_nneg, powz_hom_neg_neg, powz_hom_nneg_neg1, powz_hom_nneg_neg2, powz_hom_neg_nneg1, powz_hom_neg_nneg2
qed
end
lemma (in monoid1) nat_mult_zero: shows \( 0\cdot x = 0 \)
lemma (in group0) group0_2_L2: shows \( 1 \in G \wedge (\forall g\in G.\ (1 \cdot g = g \wedge g\cdot 1 = g)) \)
lemma (in group0) inverse_in_group:

assumes \( x\in G \)

shows \( x^{-1}\in G \)
lemma (in group0) nat_pow_add_one:

assumes \( n\in nat \), \( x\in G \)

shows \( x^{n + 1} = x^{n}\cdot x \) and \( x^{n + 1} = x\cdot x^{n} \)
lemma (in monoid1) nat_mult_type:

assumes \( n\in nat \), \( x\in G \)

shows \( n\cdot x \in G \)
lemma (in monoid0) rearr4elem_monoid:

assumes \( a\in G \), \( b\in G \), \( c\in G \), \( d\in G \)

shows \( a\oplus b\oplus (c\oplus d) = a\oplus (b\oplus c)\oplus d \)
lemma (in group0) group0_2_L6:

assumes \( x\in G \)

shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)
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) \)
lemma (in group0) nat_pow_inv_cancel:

assumes \( n\in nat \), \( x\in G \)

shows \( x^{n}\cdot (x^{-1})^{n} = 1 \)
lemma (in group0) group_inv_of_inv:

assumes \( a\in G \)

shows \( a = (a^{-1})^{-1} \)
lemma leq_nat_is_nat:

assumes \( n\in nat \), \( k\leq n \)

shows \( k\in nat \)
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 \)
lemma (in group0) group_oper_assoc:

assumes \( a\in G \), \( b\in G \), \( c\in G \)

shows \( a\cdot (b\cdot c) = a\cdot b\cdot c \)
lemma (in group0) nat_pow_cancel_less:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( x^{n}\cdot (x^{-1})^{k} = x^{n - k} \)
lemma (in group0) nat_pow_inv_cancel1:

assumes \( n\in nat \), \( x\in G \)

shows \( (x^{-1})^{n}\cdot x^{n} = 1 \)
lemma (in group0) nat_pow_cancel_more:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( (x^{-1})^{k}\cdot x^{n} = x^{n - k} \)
lemma (in int0) add_nonneg_ints:

assumes \( 0 \leq z_1 \), \( 0 \leq z_2 \)

shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N + \left| z_2 \right|_N \), \( z_1 + z_2 = \$\!\#\! (\left| z_1 \right|_N + \left| z_2 \right|_N ) \)
corollary (in int0) neg_not_nonneg:

assumes \( m \lt 0 \)

shows \( \neg ( 0 \leq m) \)
lemma (in int0) add_neg_ints:

assumes \( z_1 \lt 0 \), \( z_2 \lt 0 \)

shows \( z_1 + z_2 \lt 0 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N + \left| z_2 \right|_N \), \( z_1 + z_2 = \ \$\!-\!(\$\!\#\!(\left| z_1 \right|_N + \left| z_2 \right|_N )) \)
lemma (in int0) add_nonneg_neg1:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \)

shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N - \left| z_2 \right|_N \), \( z_1 + z_2 = \$\!\#\!(\left| z_1 \right|_N - \left| z_2 \right|_N ) \)
lemma (in int0) add_nonneg_neg1:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \)

shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N - \left| z_2 \right|_N \), \( z_1 + z_2 = \$\!\#\!(\left| z_1 \right|_N - \left| z_2 \right|_N ) \)
lemma (in int0) add_nonneg_neg2:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_1 \right|_N \lt \left| z_2 \right|_N \)

shows \( z_1 + z_2 \lt 0 \), \( \left| z_1 + z_2 \right|_N = \left| z_2 \right|_N - \left| z_1 \right|_N \), \( z_1 + z_2 = \ \$\!-\!(\$\!\#\!(\left| z_2 \right|_N - \left| z_1 \right|_N )) \)
lemma (in group0) nat_pow_cancel_more1:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( x^{k}\cdot (x^{-1})^{n} = (x^{-1})^{n - k} \)
lemma (in int0) add_neg_nonneg1:

assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_1 \right|_N \leq \left| z_2 \right|_N \)

shows \( 0 \leq z_1 + z_2 \), \( \left| z_1 + z_2 \right|_N = \left| z_2 \right|_N - \left| z_1 \right|_N \), \( z_1 + z_2 = \$\!\#\!(\left| z_2 \right|_N - \left| z_1 \right|_N ) \)
lemma (in int0) add_neg_nonneg2:

assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_2 \right|_N \lt \left| z_1 \right|_N \)

shows \( z_1 + z_2 \lt 0 \), \( \left| z_1 + z_2 \right|_N = \left| z_1 \right|_N - \left| z_2 \right|_N \), \( z_1 + z_2 = \ \$\!-\!(\$\!\#\!(\left| z_1 \right|_N - \left| z_2 \right|_N )) \)
lemma (in group0) nat_pow_cancel_less1:

assumes \( n\in nat \), \( k\leq n \), \( x\in G \)

shows \( (x^{-1})^{n}\cdot x^{k} = (x^{-1})^{n - k} \)
lemma (in int0) int_pair_6cases:

assumes \( z_1\in \mathbb{Z} \), \( z_2\in \mathbb{Z} \)

shows \( ( 0 \leq z_1 \wedge 0 \leq z_2) \vee (z_1 \lt 0 \wedge z_2 \lt 0 ) \vee \) \( ( 0 \leq z_1 \wedge z_2 \lt 0 \wedge \left| z_2 \right|_N \leq \left| z_1 \right|_N ) \vee \) \( ( 0 \leq z_1 \wedge z_2 \lt 0 \wedge \left| z_1 \right|_N \lt \left| z_2 \right|_N ) \vee \) \( (z_1 \lt 0 \wedge 0 \leq z_2 \wedge \left| z_1 \right|_N \leq \left| z_2 \right|_N ) \vee \) \( (z_1 \lt 0 \wedge 0 \leq z_2 \wedge \left| z_2 \right|_N \lt \left| z_1 \right|_N ) \)
lemma (in group_int0) powz_hom_nneg_nneg:

assumes \( 0 \leq z_1 \), \( 0 \leq z_2 \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)
lemma (in group_int0) powz_hom_neg_neg:

assumes \( z_1 \lt 0 \), \( z_2 \lt 0 \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)
lemma (in group_int0) powz_hom_nneg_neg1:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_2 \right|_N \leq \left| z_1 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)
lemma (in group_int0) powz_hom_nneg_neg2:

assumes \( 0 \leq z_1 \), \( z_2 \lt 0 \), \( \left| z_1 \right|_N \lt \left| z_2 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)
lemma (in group_int0) powz_hom_neg_nneg1:

assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_1 \right|_N \leq \left| z_2 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)
lemma (in group_int0) powz_hom_neg_nneg2:

assumes \( z_1 \lt 0 \), \( 0 \leq z_2 \), \( \left| z_2 \right|_N \lt \left| z_1 \right|_N \), \( x\in G \)

shows \( x^{z_1 + z_2} = x^{z_1}\cdot x^{z_2} \)