IsarMathLib

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

theory Loop_ZF imports Quasigroup_ZF Fold_ZF

begin

This theory specifies the definition and proves basic properites of loops. Loops are very similar to groups, the only property that is missing is associativity of the operation.

Definitions and notation

In this section we define the notions of identity element and left and right inverse.

A loop is a quasigroup with an identity element.

definition

\( \text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x) \)

The neutral element for a binary operation \(A:G\times G \rightarrow G \) is defined as the only element \(e\) of \(G\) such that \(A\langle x,e\rangle = x\) and \(A\langle e,x\rangle = x\) for all \(x\in G\). Note that although the loop definition guarantees the existence of (some) such element(s) at this point we do not know if this element is unique. We can define this notion h ere but it will become usable only after we prove uniqueness.

definition

\( \text{ TheNeutralElement}(G,f) \equiv \) \( ( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g)) \)

We will reuse the notation defined in the quasigroup0 locale, just adding the assumption about the existence of a neutral element and notation for it.

locale loop0 = quasigroup0 +

assumes ex_ident: \( \exists e\in G.\ \forall x\in G.\ e\cdot x = x \wedge x\cdot e = x \)

defines \( 1 \equiv \text{ TheNeutralElement}(G,A) \)

defines \( \prod s \equiv \text{Fold}(A,1 ,s) \)

defines \( x^{n} \equiv \prod \{\langle k,x\rangle .\ k\in n\} \)

In the loop context the pair \( (G,A) \) forms a loop.

lemma (in loop0) is_loop:

shows \( \text{IsAloop}(G,A) \) unfolding IsAloop_def using ex_ident, qgroupassum

If we know that a pair \( (G,A) \) forms a loop then the assumptions of the loop0 locale hold.

lemma loop_loop0_valid:

assumes \( \text{IsAloop}(G,A) \)

shows \( loop0(G,A) \) using assms unfolding IsAloop_def, loop0_axioms_def, quasigroup0_def, loop0_def

The neutral element is unique in the loop.

lemma (in loop0) neut_uniq_loop:

shows \( \exists !e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x) \)proof

from ex_ident show \( \exists e.\ e \in G \wedge (\forall x\in G.\ e \cdot x = x \wedge x \cdot e = x) \)

next

fix \( e \) \( y \)

assume \( e \in G \wedge (\forall x\in G.\ e \cdot x = x \wedge x \cdot e = x) \), \( y \in G \wedge (\forall x\in G.\ y \cdot x = x \wedge x \cdot y = x) \)

then have \( e\cdot y =y \) and \( e\cdot y = e \)

thus \( e=y \)

qed

The neutral element as defined in the loop0 locale is indeed neutral.

lemma (in loop0) neut_props_loop:

shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)proof

let \( n = \text{The } e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x) \)

have \( 1 = \text{ TheNeutralElement}(G,A) \)

then have \( 1 = n \) unfolding TheNeutralElement_def

moreover

have \( n\in G \wedge (\forall x\in G.\ n\cdot x = x \wedge x\cdot n = x) \) using neut_uniq_loop, theI

ultimately show \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x = x \wedge x\cdot 1 = x \)

qed

A loop is not empty as it contains the neutral element.

corollary (in loop0) loop_not_empty:

shows \( G\neq \emptyset \) using neut_props_loop(1)

Every element of a loop has unique left and right inverse (which need not be the same). Here we define the left inverse as a function on \(G\).

definition

\( \text{LeftInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle y,x\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)

Definition of the right inverse as a function on \(G\):

definition

\( \text{RightInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle x,y\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)

In a loop \(G\) right and left inverses are functions on \(G\).

lemma (in loop0) lr_inv_fun:

shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \) unfolding LeftInv_def, RightInv_def using neut_props_loop, lrdiv_props(1,4), ZF1_1_L9, ZF_fun_from_total

Right and left inverses have desired properties.

lemma (in loop0) lr_inv_props:

assumes \( x\in G \)

shows \( \text{LeftInv}(G,A)(x) \in G \), \( ( \text{LeftInv}(G,A)(x))\cdot x = 1 \), \( \text{RightInv}(G,A)(x) \in G \), \( x\cdot ( \text{RightInv}(G,A)(x)) = 1 \)proof

from assms show \( \text{LeftInv}(G,A)(x) \in G \) and \( \text{RightInv}(G,A)(x) \in G \) using lr_inv_fun, apply_funtype

from assms have \( \exists !y.\ y\in G \wedge y\cdot x = 1 \) using neut_props_loop(1), lrdiv_props(1)

then have \( (\bigcup \{y\in G.\ y\cdot x = 1 \})\cdot x = 1 \) by (rule ZF1_1_L9 )

with assms show \( ( \text{LeftInv}(G,A)(x))\cdot x = 1 \) using lr_inv_fun(1), ZF_fun_from_tot_val unfolding LeftInv_def

from assms have \( \exists !y.\ y\in G \wedge x\cdot y = 1 \) using neut_props_loop(1), lrdiv_props(4)

then have \( x\cdot (\bigcup \{y\in G.\ x\cdot y = 1 \}) = 1 \) by (rule ZF1_1_L9 )

with assms show \( x\cdot ( \text{RightInv}(G,A)(x)) = 1 \) using lr_inv_fun(2), ZF_fun_from_tot_val unfolding RightInv_def

qed

Product of a list of loop elements

Given a list \(s:n\rightarrow L\) of loop elements we can define the product of the elements \(s=[x_0,x_1,...,x_{n-1}]\) as the fold of loop operation over that list. The loop0 locale defined a notation for such fold as \(\prod s\). That locale also defines a notation for the special case when the list is constant i.e. \(x_0 = x_1 = ... x_{n-1} = x\). In such case \(\prod s\) becomes \(x^{n-1}\). There are similar sections on this subject in Semigroup_ZF, Monoid_ZF and Group_ZF.

The product of a list of loop elements is an element of the loop.

lemma (in loop0) list_prod_in_loop:

assumes \( n\in nat \), \( s:n\rightarrow G \)

shows \( (\prod s) \in G \) using qgroupassum, assms, neut_props_loop(1), fold_props(2) unfolding IsAquasigroup_def

In particular a natural power of a loop element is an element of the loop.

lemma (in loop0) loop_prod_type:

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

shows \( x^{n} \in G \) using assms, ZF_fun_from_total, list_prod_in_loop

For a nonempty list of loop element the last element of the list can be pulled out of the product and put after the product. In other words \(\prod{k=0}^n s(n) = (\prod{k=0}^{n-1} s(n))\cdot s(n)\).

lemma (in loop0) loop_prod_pull_last:

assumes \( n \in nat \), \( \forall k\in n + 1.\ s(k) \in G \)

shows \( (\prod \{\langle k,s(k)\rangle .\ k\in n + 1\}) = (\prod \{\langle k,s(k)\rangle .\ k\in n\}) \cdot s(n) \) using qgroupassum, assms, neut_props_loop(1), fold_detach_last unfolding IsAquasigroup_def

The way we defined the product notation implies that the product of an empty list is the neutral element of the loop.

lemma (in loop0) loop_prod_empty:

assumes \( s:\emptyset \rightarrow G \)

shows \( (\prod s) = 1 \) using qgroupassum, assms, neut_props_loop(1), fold_empty unfolding IsAquasigroup_def

In particular, any loop element raised to the natural zero'th power is the neutral element of the loop. In other words \(x^0=1\).

corollary (in loop0) loop_zero_pow:

shows \( x^{0} = 1 \) using loop_prod_empty

Raising a loop element to a power greater by one corresponds to multiplying the power by that loop element.

lemma (in loop0) loop_pow_mult_one:

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

shows \( x^{n + 1} = x^{n}\cdot x \)proof

from assms(2) have \( \forall k\in n + 1.\ x \in G \)

with assms(1) have \( (\prod \{\langle k,x\rangle .\ k\in n + 1\}) = (\prod \{\langle k,x\rangle .\ k\in n\})\cdot x \) by (rule loop_prod_pull_last )

thus \( x^{n + 1} = x^{n}\cdot x \)

qed

end

Definition of IsAloop: \( \text{IsAloop}(G,A) \equiv \text{IsAquasigroup}(G,A) \wedge (\exists e\in G.\ \forall x\in G.\ A\langle e,x\rangle = x \wedge A\langle x,e\rangle = x) \)

Definition of TheNeutralElement: \( \text{ TheNeutralElement}(G,f) \equiv \) \( ( \text{The } e.\ e\in G \wedge (\forall g\in G.\ f\langle e,g\rangle = g \wedge f\langle g,e\rangle = g)) \)

lemma (in loop0) neut_uniq_loop: shows \( \exists !e.\ e\in G \wedge (\forall x\in G.\ e\cdot x = x \wedge x\cdot e = x) \)

lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)

Definition of LeftInv: \( \text{LeftInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle y,x\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)

Definition of RightInv: \( \text{RightInv}(G,A) \equiv \{\langle x,\bigcup \{y\in G.\ A\langle x,y\rangle = \text{ TheNeutralElement}(G,A)\}\rangle .\ x\in G\} \)

lemma (in loop0) neut_props_loop: shows \( 1 \in G \) and \( \forall x\in G.\ 1 \cdot x =x \wedge x\cdot 1 = x \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

shows \( \exists !z.\ z\in G \wedge z\cdot x = y \), \( y/ x \in G \), \( (y/ x)\cdot x = y \) and \( \exists !z.\ z\in G \wedge x\cdot z = y \), \( x\backslash y \in G \), \( x\cdot (x\backslash y) = y \)

lemma ZF1_1_L9:

assumes \( \exists ! x.\ x\in A \wedge \phi (x) \)

shows \( \exists a.\ \{x\in A.\ \phi (x)\} = \{a\} \), \( \bigcup \{x\in A.\ \phi (x)\} \in A \), \( \phi (\bigcup \{x\in A.\ \phi (x)\}) \), \( \exists x\in A.\ \phi (x) \)

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 \)

lemma (in loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)

lemma (in loop0) lr_inv_fun: shows \( \text{LeftInv}(G,A):G\rightarrow G \), \( \text{RightInv}(G,A):G\rightarrow G \)

lemma ZF_fun_from_tot_val:

assumes \( f:X\rightarrow Y \), \( x\in X \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)

shows \( f(x) = b(x) \) and \( b(x)\in Y \)

lemma (in quasigroup0) lrdiv_props:

assumes \( x\in G \), \( y\in G \)