IsarMathLib

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

theory OrderedLoop_ZF imports Loop_ZF Order_ZF

begin

This theory file is about properties of loops (the algebraic structures introduced in IsarMathLib in the Loop_ZF theory) with an additional order relation that is in a way compatible with the loop's binary operation. The oldest reference I have found on the subject is \cite{Zelinski1948}.

Definition and notation

An ordered loop \((G,A)\) is a loop with a partial order relation r that is "translation invariant" with respect to the loop operation \(A\).

A triple \((G,A,r)\) is an ordered loop if \((G,A)\) is a loop and \(r\) is a relation on \(G\) (i.e. a subset of \(G\times G\) with is a partial order and for all elements \(x,y,z \in G\) the condition \(\langle x,y\rangle \in r\) is equivalent to both \(\langle A\langle x,z\rangle, A\langle x,z\rangle\rangle \in r\) and \(\langle A\langle z,x\rangle, A\langle z,x\rangle\rangle \in r\). This looks a bit awkward in the basic set theory notation, but using the additive notation for the group operation and \(x\leq y\) to instead of \(\langle x,y \rangle \in r\) this just means that \(x\leq y\) if and only if \(x+z\leq y+z\) and \(x\leq y\) if and only if \(z+x\leq z+y\).

definition

\( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)

We define the set of nonnegative elements in the obvious way as \(L^+ =\{x\in L: 0 \leq x\}\).

definition

\( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)

The \( \text{PositiveSet}(L,A,r) \) is a set similar to \( \text{Nonnegative}(L,A,r) \), but without the neutral element.

definition

\( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)

We will use the additive notation for ordered loops.

locale loop1

assumes ordLoopAssum: \( \text{IsAnOrdLoop}(L,A,r) \)

defines \( 0 \equiv \text{ TheNeutralElement}(L,A) \)

defines \( x + y \equiv A\langle x,y\rangle \)

defines \( x \leq y \equiv \langle x,y\rangle \in r \)

defines \( x \lt y \equiv x\leq y \wedge x\neq y \)

defines \( L^+ \equiv \text{Nonnegative}(L,A,r) \)

defines \( L_+ \equiv \text{PositiveSet}(L,A,r) \)

defines \( - x + y \equiv \text{ LeftDiv}(L,A)\langle x,y\rangle \)

defines \( x - y \equiv \text{ RightDiv}(L,A)\langle y,x\rangle \)

Theorems proven in the loop0 locale are valid in the loop1 locale

sublocale loop1 < loop0

using ordLoopAssum, loop_loop0_valid unfolding IsAnOrdLoop_def

The notation \(-x+y\) and \(x-y\) denotes left and right division, resp. These two operations are closed in a loop, see lemma lrdiv_binop in the Quasigroup_ZF theory. The next lemma reiterates that fact using the notation of the loop1 context.

lemma (in loop1) left_right_sub_closed:

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

shows \( ( - x + y) \in L \) and \( x - y \in L \)proof

from qgroupassum have \( \text{ LeftDiv}(L,A):L\times L \rightarrow L \) and \( \text{ RightDiv}(L,A):L\times L \rightarrow L \) using lrdiv_binop

with assms show \( ( - x + y) \in L \) and \( x - y \in L \) using apply_funtype

qed

In this context \(x \leq y\) implies that both \(x\) and \(y\) belong to \(L\).

lemma (in loop1) lsq_members:

assumes \( x\leq y \)

shows \( x\in L \) and \( y\in L \) using ordLoopAssum, assms, IsAnOrdLoop_def

In this context \(x < y\) implies that both \(x\) and \(y\) belong to \(L\).

lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \) using ordLoopAssum, assms, IsAnOrdLoop_def

In an ordered loop the order is translation invariant.

lemma (in loop1) ord_trans_inv:

assumes \( x\leq y \), \( z\in L \)

shows \( x + z \leq y + z \) and \( z + x \leq z + y \)proof

from ordLoopAssum, assms have \( (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ) \) using lsq_members unfolding IsAnOrdLoop_def

with assms(1) show \( x + z \leq y + z \) and \( z + x \leq z + y \)

qed

In an ordered loop the strict order is translation invariant.

lemma (in loop1) strict_ord_trans_inv:

assumes \( x \lt y \), \( z\in L \)

shows \( x + z \lt y + z \) and \( z + x \lt z + y \)proof

from assms have \( x + z \leq y + z \) and \( z + x \leq z + y \) using ord_trans_inv

moreover

have \( x + z \neq y + z \) and \( z + x \neq z + y \)proof

{

assume \( x + z = y + z \)

with assms have \( x=y \) using less_members, qg_cancel_right

with assms(1) have \( False \)

}

thus \( x + z \neq y + z \)

{

assume \( z + x = z + y \)

with assms have \( x=y \) using less_members, qg_cancel_left

with assms(1) have \( False \)

}

thus \( z + x \neq z + y \)

qed

ultimately show \( x + z \lt y + z \) and \( z + x \lt z + y \)

qed

We can cancel an element from both sides of an inequality on the right side.

lemma (in loop1) ineq_cancel_right:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \leq y + z \)

shows \( x\leq y \)proof

from ordLoopAssum, assms(1,2,3) have \( \langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r \) unfolding IsAnOrdLoop_def

with assms(4) show \( x\leq y \)

qed

We can cancel an element from both sides of a strict inequality on the right side.

lemma (in loop1) strict_ineq_cancel_right:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \lt y + z \)

shows \( x \lt y \) using assms, ineq_cancel_right

We can cancel an element from both sides of an inequality on the left side.

lemma (in loop1) ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \leq z + y \)

shows \( x\leq y \)proof

from ordLoopAssum, assms(1,2,3) have \( \langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r \) unfolding IsAnOrdLoop_def

with assms(4) show \( x\leq y \)

qed

We can cancel an element from both sides of a strict inequality on the left side.

lemma (in loop1) strict_ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \lt z + y \)

shows \( x \lt y \) using assms, ineq_cancel_left

The definition of the nonnegative set in the notation used in the loop1 locale:

lemma (in loop1) nonneg_definition:

shows \( x \in L^+ \longleftrightarrow 0 \leq x \) using ordLoopAssum, IsAnOrdLoop_def, Nonnegative_def

The nonnegative set is contained in the loop.

lemma (in loop1) nonneg_subset:

shows \( L^+ \subseteq L \) using Nonnegative_def

The positive set is contained in the loop.

lemma (in loop1) positive_subset:

shows \( L_+ \subseteq L \) using PositiveSet_def

The definition of the positive set in the notation used in the loop1 locale:

lemma (in loop1) posset_definition:

shows \( x \in L_+ \longleftrightarrow ( 0 \leq x \wedge x\neq 0 ) \) using ordLoopAssum, IsAnOrdLoop_def, PositiveSet_def

Another form of the definition of the positive set in the notation used in the loop1 locale:

lemma (in loop1) posset_definition1:

shows \( x \in L_+ \longleftrightarrow 0 \lt x \) using ordLoopAssum, IsAnOrdLoop_def, PositiveSet_def

The order in an ordered loop is antisymmeric.

lemma (in loop1) loop_ord_antisym:

assumes \( x\leq y \) and \( y\leq x \)

shows \( x=y \)proof

from ordLoopAssum, assms have \( \text{antisym}(r) \), \( \langle x,y\rangle \in r \), \( \langle y,x\rangle \in r \) unfolding IsAnOrdLoop_def, IsPartOrder_def

then show \( x=y \) by (rule Fol1_L4 )

qed

The loop order is transitive.

lemma (in loop1) loop_ord_trans:

assumes \( x\leq y \) and \( y\leq z \)

shows \( x\leq z \)proof

from ordLoopAssum, assms have \( \text{trans}(r) \) and \( \langle x,y\rangle \in r \wedge \langle y,z\rangle \in r \) unfolding IsAnOrdLoop_def, IsPartOrder_def

then have \( \langle x,z\rangle \in r \) by (rule Fol1_L3 )

thus \( thesis \)

qed

The loop order is reflexive.

lemma (in loop1) loop_ord_refl:

assumes \( x\in L \)

shows \( x\leq x \) using assms, ordLoopAssum unfolding IsAnOrdLoop_def, IsPartOrder_def, refl_def

The neutral element is nonnegative.

lemma (in loop1) loop_zero_nonneg:

shows \( 0 \in L^+ \) using neut_props_loop(1), loop_ord_refl, nonneg_definition

A form of mixed transitivity for the strict order:

lemma (in loop1) loop_strict_ord_trans:

assumes \( x\leq y \) and \( y \lt z \)

shows \( x \lt z \)proof

from assms have \( x\leq y \) and \( y\leq z \)

then have \( x\leq z \) by (rule loop_ord_trans )

with assms show \( x \lt z \) using loop_ord_antisym

qed

Another form of mixed transitivity for the strict order:

lemma (in loop1) loop_strict_ord_trans1:

assumes \( x \lt y \) and \( y\leq z \)

shows \( x \lt z \)proof

from assms have \( x\leq y \) and \( y\leq z \)

then have \( x\leq z \) by (rule loop_ord_trans )

with assms show \( x \lt z \) using loop_ord_antisym

qed

Yet another form of mixed transitivity for the strict order:

lemma (in loop1) loop_strict_ord_trans2:

assumes \( x \lt y \) and \( y \lt z \)

shows \( x \lt z \)proof

from assms have \( x\leq y \) and \( y\leq z \)

then have \( x\leq z \) by (rule loop_ord_trans )

with assms show \( x \lt z \) using loop_ord_antisym

qed

We can move an element to the other side of an inequality. Well, not exactly, but our notation creates an illusion to that effect.

lemma (in loop1) lsq_other_side:

assumes \( x\leq y \)

shows \( 0 \leq - x + y \), \( ( - x + y) \in L^+ \), \( 0 \leq y - x \), \( (y - x) \in L^+ \)proof

from assms have \( x\in L \), \( y\in L \), \( 0 \in L \), \( ( - x + y) \in L \), \( (y - x) \in L \) using lsq_members, neut_props_loop(1), lrdiv_props(2,5)

then have \( x = x + 0 \) and \( y = x + ( - x + y) \) using neut_props_loop(2), lrdiv_props(6)

with assms have \( x + 0 \leq x + ( - x + y) \)

with \( x\in L \), \( 0 \in L \), \( ( - x + y) \in L \) show \( 0 \leq - x + y \) using ineq_cancel_left

then show \( ( - x + y) \in L^+ \) using nonneg_definition

from \( x\in L \), \( y\in L \) have \( x = 0 + x \) and \( y = (y - x) + x \) using neut_props_loop(2), lrdiv_props(3)

with assms have \( 0 + x \leq (y - x) + x \)

with \( x\in L \), \( 0 \in L \), \( (y - x) \in L \) show \( 0 \leq y - x \) using ineq_cancel_right

then show \( (y - x) \in L^+ \) using nonneg_definition

qed

We can move an element to the other side of a strict inequality.

lemma (in loop1) ls_other_side:

assumes \( x \lt y \)

shows \( 0 \lt - x + y \), \( ( - x + y) \in L_+ \), \( 0 \lt y - x \), \( (y - x) \in L_+ \)proof

from assms have \( x\in L \), \( y\in L \), \( 0 \in L \), \( ( - x + y) \in L \), \( (y - x) \in L \) using lsq_members, neut_props_loop(1), lrdiv_props(2,5)

then have \( x = x + 0 \) and \( y = x + ( - x + y) \) using neut_props_loop(2), lrdiv_props(6)

with assms have \( x + 0 \lt x + ( - x + y) \)

with \( x\in L \), \( 0 \in L \), \( ( - x + y) \in L \) show \( 0 \lt - x + y \) using strict_ineq_cancel_left

then show \( ( - x + y) \in L_+ \) using posset_definition1

from \( x\in L \), \( y\in L \) have \( x = 0 + x \) and \( y = (y - x) + x \) using neut_props_loop(2), lrdiv_props(3)

with assms have \( 0 + x \lt (y - x) + x \)

with \( x\in L \), \( 0 \in L \), \( (y - x) \in L \) show \( 0 \lt y - x \) using strict_ineq_cancel_right

then show \( (y - x) \in L_+ \) using posset_definition1

qed

We can add sides of inequalities.

lemma (in loop1) add_ineq:

assumes \( x\leq y \), \( z\leq t \)

shows \( x + z \leq y + t \)proof

from assms have \( x + z \leq y + z \) using lsq_members(1), ord_trans_inv(1)

with assms show \( thesis \) using lsq_members(2), ord_trans_inv(2), loop_ord_trans

qed

We can add sides of strict inequalities. The proof uses a lemma that relies on the antisymmetry of the order relation.

lemma (in loop1) add_ineq_strict:

assumes \( x \lt y \), \( z \lt t \)

shows \( x + z \lt y + t \)proof

from assms have \( x + z \lt y + z \) using less_members(1), strict_ord_trans_inv(1)

moreover

from assms have \( y + z \lt y + t \) using less_members(2), strict_ord_trans_inv(2)

ultimately show \( thesis \) by (rule loop_strict_ord_trans2 )

qed

We can add sides of inequalities one of which is strict.

lemma (in loop1) add_ineq_strict1:

assumes \( x\leq y \), \( z \lt t \)

shows \( x + z \lt y + t \) and \( z + x \lt t + y \)proof

from assms have \( x + z \leq y + z \) using less_members(1), ord_trans_inv(1)

with assms show \( x + z \lt y + t \) using lsq_members(2), strict_ord_trans_inv(2), loop_strict_ord_trans

from assms have \( z + x \lt t + x \) using lsq_members(1), strict_ord_trans_inv(1)

with assms show \( z + x \lt t + y \) using less_members(2), ord_trans_inv(2), loop_strict_ord_trans1

qed

Subtracting a positive element decreases the value, while adding a positive element increases the value.

lemma (in loop1) add_subtract_pos:

assumes \( x\in L \), \( 0 \lt y \)

shows \( x - y \lt x \), \( ( - y + x) \lt x \), \( x \lt x + y \), \( x \lt y + x \)proof

from assms(2) have \( y\in L \) using less_members(2)

from assms(1) have \( x\leq x \) using ordLoopAssum unfolding IsAnOrdLoop_def, IsPartOrder_def, refl_def

with assms(2) have \( x + 0 \lt x + y \) using add_ineq_strict1(1)

with assms, \( y\in L \) show \( x - y \lt x \) using neut_props_loop(2), lrdiv_props(3), lrdiv_props(2), strict_ineq_cancel_right

from assms(2), \( x\leq x \) have \( 0 + x \lt y + x \) using add_ineq_strict1(2)

with assms, \( y\in L \) show \( ( - y + x) \lt x \) using neut_props_loop(2), lrdiv_props(6), lrdiv_props(5), strict_ineq_cancel_left

from assms(1), \( x + 0 \lt x + y \), \( 0 + x \lt y + x \) show \( x \lt x + y \), \( x \lt y + x \) using neut_props_loop(2)

qed

end

lemma loop_loop0_valid:

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

shows \( loop0(G,A) \)

Definition of IsAnOrdLoop: \( \text{IsAnOrdLoop}(L,A,r) \equiv \) \( \text{IsAloop}(L,A) \wedge r\subseteq L\times L \wedge \text{IsPartOrder}(L,r) \wedge (\forall x\in L.\ \forall y\in L.\ \forall z\in L.\ \) \( ((\langle x,y\rangle \in r \longleftrightarrow \langle A\langle x,z\rangle ,A\langle y,z\rangle \rangle \in r) \wedge (\langle x,y\rangle \in r \longleftrightarrow \langle A\langle z,x\rangle ,A\langle z,y\rangle \rangle \in r ))) \)

lemma lrdiv_binop:

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

shows \( \text{ LeftDiv}(G,A):G\times G\rightarrow G \) and \( \text{ RightDiv}(G,A):G\times G\rightarrow G \)

lemma (in loop1) lsq_members:

assumes \( x\leq y \)

shows \( x\in L \) and \( y\in L \)

lemma (in loop1) ord_trans_inv:

assumes \( x\leq y \), \( z\in L \)

shows \( x + z \leq y + z \) and \( z + x \leq z + y \)

lemma (in loop1) less_members:

assumes \( x \lt y \)

shows \( x\in L \) and \( y\in L \)

lemma (in quasigroup0) qg_cancel_right:

assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( y\cdot x = z\cdot x \)

shows \( y=z \)

lemma (in quasigroup0) qg_cancel_left:

assumes \( x\in G \), \( y\in G \), \( z\in G \) and \( x\cdot y = x\cdot z \)

shows \( y=z \)

lemma (in group3) ineq_cancel_right:

assumes \( a\in G \), \( b\in G \), \( c\in G \) and \( a\cdot b \leq c\cdot b \)

shows \( a\leq c \)

lemma (in loop1) ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \leq z + y \)

shows \( x\leq y \)

Definition of Nonnegative: \( \text{Nonnegative}(L,A,r) \equiv \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r\} \)

Definition of PositiveSet: \( \text{PositiveSet}(L,A,r) \equiv \) \( \{x\in L.\ \langle \text{ TheNeutralElement}(L,A),x\rangle \in r \wedge \text{ TheNeutralElement}(L,A)\neq x\} \)

Definition of IsPartOrder: \( \text{IsPartOrder}(X,r) \equiv \text{refl}(X,r) \wedge \text{antisym}(r) \wedge \text{trans}(r) \)

lemma Fol1_L4:

assumes \( \text{antisym}(r) \) and \( \langle a,b\rangle \in r \), \( \langle b,a\rangle \in r \)

shows \( a=b \)

lemma Fol1_L3:

assumes \( \text{trans}(r) \) and \( \langle a,b\rangle \in r \wedge \langle b,c\rangle \in r \)

shows \( \langle a,c\rangle \in r \)

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 loop1) loop_ord_refl:

assumes \( x\in L \)

shows \( x\leq x \)

lemma (in loop1) nonneg_definition: shows \( x \in L^+ \longleftrightarrow 0 \leq x \)

lemma (in loop1) loop_ord_trans:

assumes \( x\leq y \) and \( y\leq z \)

shows \( x\leq z \)

lemma (in loop1) loop_ord_antisym:

assumes \( x\leq y \) and \( y\leq x \)

shows \( x=y \)

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

lemma (in quasigroup0) lrdiv_props:

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

lemma (in loop1) strict_ineq_cancel_left:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( z + x \lt z + y \)

shows \( x \lt y \)

lemma (in loop1) posset_definition1: shows \( x \in L_+ \longleftrightarrow 0 \lt x \)

lemma (in loop1) strict_ineq_cancel_right:

assumes \( x\in L \), \( y\in L \), \( z\in L \) and \( x + z \lt y + z \)

shows \( x \lt y \)