Theory OrderedLoop_ZF
section ‹ Ordered loops ›
theory OrderedLoop_ZF imports Loop_ZF Fold_ZF
begin
text‹ 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}. ›
subsection‹Definition, notation and basic properties›
text‹ 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$.›
text‹ 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
"IsAnOrdLoop(L,A,r) ≡
IsAloop(L,A) ∧ r⊆L×L ∧ IsPartOrder(L,r) ∧ (∀x∈L. ∀y∈L. ∀z∈L.
((⟨x,y⟩ ∈ r ⟷ ⟨A`⟨ x,z⟩,A`⟨y,z⟩⟩ ∈ r) ∧ (⟨x,y⟩ ∈ r ⟷ ⟨A`⟨z,x⟩,A`⟨z,y⟩⟩ ∈ r )))"
text‹We define the set of nonnegative elements in the obvious way as $L^+ =\{x\in L: 0 \leq x\}$.›
definition
"Nonnegative(L,A,r) ≡ {x∈L. ⟨ TheNeutralElement(L,A),x⟩ ∈ r}"
text‹The ‹PositiveSet(L,A,r)› is a set similar to ‹Nonnegative(L,A,r)›, but without the
neutral element. What we call the positive set here is sometimes called "the positive cone"
of an ordered loop. ›
definition
"PositiveSet(L,A,r) ≡
{x∈L. ⟨ TheNeutralElement(L,A),x⟩ ∈ r ∧ TheNeutralElement(L,A)≠ x}"
text‹ We will use the additive notation for ordered loops.›
locale loop1 =
fixes L and A and r
assumes ordLoopAssum: "IsAnOrdLoop(L,A,r)"
fixes neut ("𝟬")
defines neut_def[simp]: "𝟬 ≡ TheNeutralElement(L,A)"
fixes looper (infixl "\<ra>" 69)
defines looper_def[simp]: "x \<ra> y ≡ A`⟨ x,y⟩"
fixes lesseq (infix "\<lsq>" 68)
defines lesseq_def [simp]: "x \<lsq> y ≡ ⟨x,y⟩ ∈ r"
fixes sless (infix "\<ls>" 68)
defines sless_def[simp]: "x \<ls> y ≡ x\<lsq>y ∧ x≠y"
fixes nonnegative ("L⇧+")
defines nonnegative_def [simp]: "L⇧+ ≡ Nonnegative(L,A,r)"
fixes positive ("L⇩+")
defines positive_def[simp]: "L⇩+ ≡ PositiveSet(L,A,r)"
fixes leftdiv ("\<rm> _ \<ad> _")
defines leftdiv_def[simp]: "\<rm>x\<ad>y ≡ LeftDiv(L,A)`⟨x,y⟩"
fixes rightdiv (infixl "\<rs>" 69)
defines rightdiv_def[simp]:"x\<rs>y ≡ RightDiv(L,A)`⟨y,x⟩"
fixes listsum ("∑ _" 70)
defines listsum_def[simp]: "∑s ≡ Fold(A,𝟬,s)"
fixes nat_mult (infix "⋅" 95)
defines nat_mult_def [simp]: "n⋅x ≡ ∑{⟨k,x⟩. k∈n}"
text‹Theorems proven in the ‹loop0› locale are valid in the ‹loop1› locale›
sublocale loop1 < loop0 L A looper leftdiv rightdiv neut listsum nat_mult
using ordLoopAssum loop_loop0_valid unfolding IsAnOrdLoop_def by auto
text‹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∈L" "y∈L"
shows "(\<rm>x\<ad>y) ∈ L" and "x\<rs>y ∈ L"
proof -
from qgroupassum have "LeftDiv(L,A):L×L →L" and "RightDiv(L,A):L×L →L"
using lrdiv_binop by simp_all
with assms show "(\<rm>x\<ad>y) ∈ L" and "x\<rs>y ∈ L"
using apply_funtype by simp_all
qed
text‹In this context $x \leq y$ implies that both $x$ and $y$ belong
to $L$.›
lemma (in loop1) lsq_members: assumes "x\<lsq>y" shows "x∈L" and "y∈L"
using ordLoopAssum assms IsAnOrdLoop_def by auto
text‹In this context $x < y$ implies that both $x$ and $y$ belong
to $L$.›
lemma (in loop1) less_members: assumes "x\<ls>y" shows "x∈L" and "y∈L"
using ordLoopAssum assms IsAnOrdLoop_def by auto
text‹ In an ordered loop the order is translation invariant. ›
lemma (in loop1) ord_trans_inv: assumes "x\<lsq>y" "z∈L"
shows "x\<ra>z \<lsq> y\<ra>z" and "z\<ra>x \<lsq> z\<ra>y"
proof -
from ordLoopAssum assms have
"(⟨x,y⟩ ∈ r ⟷ ⟨A`⟨ x,z⟩,A`⟨y,z⟩⟩ ∈ r) ∧ (⟨x,y⟩ ∈ r ⟷ ⟨A`⟨z,x⟩,A`⟨z,y⟩⟩ ∈ r )"
using lsq_members unfolding IsAnOrdLoop_def by blast
with assms(1) show "x\<ra>z \<lsq> y\<ra>z" and "z\<ra>x \<lsq> z\<ra>y" by auto
qed
text‹ In an ordered loop the strict order is translation invariant. ›
lemma (in loop1) strict_ord_trans_inv: assumes "x\<ls>y" "z∈L"
shows "x\<ra>z \<ls> y\<ra>z" and "z\<ra>x \<ls> z\<ra>y"
proof -
from assms have "x\<ra>z \<lsq> y\<ra>z" and "z\<ra>x \<lsq> z\<ra>y"
using ord_trans_inv by auto
moreover have "x\<ra>z ≠ y\<ra>z" and "z\<ra>x ≠ z\<ra>y"
proof -
{ assume "x\<ra>z = y\<ra>z"
with assms have "x=y" using less_members qg_cancel_right by blast
with assms(1) have False by simp
} thus "x\<ra>z ≠ y\<ra>z" by auto
{ assume "z\<ra>x = z\<ra>y"
with assms have "x=y" using less_members qg_cancel_left by blast
with assms(1) have False by simp
} thus "z\<ra>x ≠ z\<ra>y" by auto
qed
ultimately show "x\<ra>z \<ls> y\<ra>z" and "z\<ra>x \<ls> z\<ra>y"
by auto
qed
text‹We can cancel an element from both sides of an inequality on the right side. ›
lemma (in loop1) ineq_cancel_right: assumes "x∈L" "y∈L" "z∈L" and "x\<ra>z \<lsq> y\<ra>z"
shows "x\<lsq>y"
proof -
from ordLoopAssum assms(1,2,3) have "⟨x,y⟩ ∈ r ⟷ ⟨A`⟨ x,z⟩,A`⟨y,z⟩⟩ ∈ r"
unfolding IsAnOrdLoop_def by blast
with assms(4) show "x\<lsq>y" by simp
qed
text‹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∈L" "y∈L" "z∈L" and "x\<ra>z \<ls> y\<ra>z"
shows "x\<ls>y"
using assms ineq_cancel_right by auto
text‹We can cancel an element from both sides of an inequality on the left side. ›
lemma (in loop1) ineq_cancel_left: assumes "x∈L" "y∈L" "z∈L" and "z\<ra>x \<lsq> z\<ra>y"
shows "x\<lsq>y"
proof -
from ordLoopAssum assms(1,2,3) have "⟨x,y⟩ ∈ r ⟷ ⟨A`⟨z,x⟩,A`⟨z,y⟩⟩ ∈ r"
unfolding IsAnOrdLoop_def by blast
with assms(4) show "x\<lsq>y" by simp
qed
text‹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∈L" "y∈L" "z∈L" and "z\<ra>x \<ls> z\<ra>y"
shows "x\<ls>y"
using assms ineq_cancel_left by auto
text‹We can subtract a loop element from both sides of inequality
both on the left side and right.›
lemma (in loop1) ineq_subtr_from_sides: assumes "x\<lsq>y" "z∈L"
shows "x\<rs>z \<lsq> y\<rs>z" and "(\<rm>z\<ad>x) \<lsq> \<rm>z\<ad>y"
proof -
from assms have
T: "x\<rs>z∈L" "y\<rs>z∈L" "(\<rm>z\<ad>x)∈L" "(\<rm>z\<ad>y)∈L" and
"x = (x\<rs>z)\<ra>z" "y = (y\<rs>z)\<ra>z" and
"x = z\<ra>(\<rm>z\<ad>x)" "y = z\<ra>(\<rm>z\<ad>y)"
using lsq_members lrdiv_props(2,3,5,6) by simp_all
with assms(1) have
"(x\<rs>z)\<ra>z \<lsq> (y\<rs>z)\<ra>z" and
"z\<ra>(\<rm>z\<ad>x) \<lsq> z\<ra>(\<rm>z\<ad>y)"
by simp_all
with assms(2) T show
"x\<rs>z \<lsq> y\<rs>z" and "(\<rm>z\<ad>x) \<lsq> \<rm>z\<ad>y"
using ineq_cancel_left ineq_cancel_right by simp_all
qed
text‹We can subtract a loop element from both sides of of a strict inequality
both on the left side and right.›
lemma (in loop1) strict_ineq_subtr: assumes "x\<ls>y" "z∈L"
shows "x\<rs>z \<ls> y\<rs>z" and "(\<rm>z\<ad>x) \<ls> \<rm>z\<ad>y"
proof -
from assms have
T: "x\<rs>z∈L" "y\<rs>z∈L" "(\<rm>z\<ad>x)∈L" "(\<rm>z\<ad>y)∈L" and
"x = (x\<rs>z)\<ra>z" "y = (y\<rs>z)\<ra>z" and
"x = z\<ra>(\<rm>z\<ad>x)" "y = z\<ra>(\<rm>z\<ad>y)"
using less_members lrdiv_props(2,3,5,6) by auto
with assms(1) have
"(x\<rs>z)\<ra>z \<ls> (y\<rs>z)\<ra>z" and
"z\<ra>(\<rm>z\<ad>x) \<ls> z\<ra>(\<rm>z\<ad>y)"
by simp_all
with assms(2) T show
"x\<rs>z \<ls> y\<rs>z" and "(\<rm>z\<ad>x) \<ls> \<rm>z\<ad>y"
using strict_ineq_cancel_left strict_ineq_cancel_right
by auto
qed
text‹We can move an element to the other side of a strict inequality with three
loop elements - right side variant.›
lemma (in loop1) strict_ineq_move_side_right: assumes "x∈L" "y∈L" "x\<ra>y\<ls>z"
shows "x\<ls>z\<rs>y"
proof -
from assms(2,3) have "(x\<ra>y)\<rs>y \<ls> z\<rs>y"
using strict_ineq_subtr by simp
with assms(1,2) show "x\<ls>z\<rs>y" using lrdiv_ident(1) by simp
qed
text‹We can move an element to the other side of an inequality with three
loop elements - right side variant.›
lemma (in loop1) ineq_move_side_right: assumes "x∈L" "y∈L" "x\<ra>y\<lsq>z"
shows "x\<lsq>z\<rs>y"
using assms ineq_subtr_from_sides lrdiv_ident(1) by force
text‹The definition of the nonnegative set in the notation used in the ‹loop1› locale: ›
lemma (in loop1) nonneg_definition:
shows "x ∈ L⇧+ ⟷ 𝟬 \<lsq> x" using ordLoopAssum IsAnOrdLoop_def Nonnegative_def by auto
text‹The nonnegative set is contained in the loop.›
lemma (in loop1) nonneg_subset: shows "L⇧+ ⊆ L"
using Nonnegative_def by auto
text‹The positive set is contained in the loop.›
lemma (in loop1) positive_subset: shows "L⇩+ ⊆ L"
using PositiveSet_def by auto
text‹The definition of the positive set in the notation used in the ‹loop1› locale: ›
lemma (in loop1) posset_definition:
shows "x ∈ L⇩+ ⟷ (𝟬\<lsq>x ∧ x≠𝟬)"
using ordLoopAssum IsAnOrdLoop_def PositiveSet_def by auto
text‹Another form of the definition of the positive set in the notation used in the ‹loop1› locale: ›
lemma (in loop1) posset_definition1:
shows "x ∈ L⇩+ ⟷ 𝟬\<ls>x"
using ordLoopAssum IsAnOrdLoop_def PositiveSet_def by auto
text‹ The order in an ordered loop is antisymmeric. ›
lemma (in loop1) loop_ord_antisym: assumes "x\<lsq>y" and "y\<lsq>x"
shows "x=y"
proof -
from ordLoopAssum assms have "antisym(r)" "⟨x,y⟩ ∈ r" "⟨y,x⟩ ∈ r"
unfolding IsAnOrdLoop_def IsPartOrder_def by auto
then show "x=y" by (rule Fol1_L4)
qed
text‹ The loop order is transitive. ›
lemma (in loop1) loop_ord_trans: assumes "x\<lsq>y" and "y\<lsq>z" shows "x\<lsq>z"
proof -
from ordLoopAssum assms have "trans(r)" and "⟨x,y⟩ ∈ r ∧ ⟨y,z⟩ ∈ r"
unfolding IsAnOrdLoop_def IsPartOrder_def by auto
then have "⟨x,z⟩ ∈ r" by (rule Fol1_L3)
thus ?thesis by simp
qed
text‹ The loop order is reflexive. ›
lemma (in loop1) loop_ord_refl: assumes "x∈L" shows "x\<lsq>x"
using assms ordLoopAssum unfolding IsAnOrdLoop_def IsPartOrder_def refl_def
by simp
text‹The neutral element is nonnegative.›
lemma (in loop1) loop_zero_nonneg: shows "𝟬∈L⇧+"
using neut_props_loop(1) loop_ord_refl nonneg_definition
by simp
text‹ A form of mixed transitivity for the strict order: ›
lemma (in loop1) loop_strict_ord_trans: assumes "x\<lsq>y" and "y\<ls>z"
shows "x\<ls>z"
proof -
from assms have "x\<lsq>y" and "y\<lsq>z" by auto
then have "x\<lsq>z" by (rule loop_ord_trans)
with assms show "x\<ls>z" using loop_ord_antisym by auto
qed
text‹ Another form of mixed transitivity for the strict order: ›
lemma (in loop1) loop_strict_ord_trans1: assumes "x\<ls>y" and "y\<lsq>z"
shows "x\<ls>z"
proof -
from assms have "x\<lsq>y" and "y\<lsq>z" by auto
then have "x\<lsq>z" by (rule loop_ord_trans)
with assms show "x\<ls>z" using loop_ord_antisym by auto
qed
text‹ Yet another form of mixed transitivity for the strict order: ›
lemma (in loop1) loop_strict_ord_trans2: assumes "x\<ls>y" and "y\<ls>z"
shows "x\<ls>z"
proof -
from assms have "x\<lsq>y" and "y\<lsq>z" by auto
then have "x\<lsq>z" by (rule loop_ord_trans)
with assms show "x\<ls>z" using loop_ord_antisym by auto
qed
text‹ 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\<lsq>y"
shows "𝟬 \<lsq> \<rm>x\<ad>y" "(\<rm>x\<ad>y) ∈ L⇧+" "𝟬 \<lsq> y\<rs>x" "(y\<rs>x) ∈ L⇧+"
proof -
from assms have "x∈L" "y∈L" "𝟬∈L" "(\<rm>x\<ad>y) ∈ L" "(y\<rs>x) ∈ L"
using lsq_members neut_props_loop(1) lrdiv_props(2,5) by auto
then have "x = x\<ra>𝟬" and "y = x\<ra>(\<rm>x\<ad>y)" using neut_props_loop(2) lrdiv_props(6)
by auto
with assms have "x\<ra>𝟬 \<lsq> x\<ra>(\<rm>x\<ad>y)" by simp
with ‹x∈L› ‹𝟬∈L› ‹(\<rm>x\<ad>y) ∈ L› show "𝟬 \<lsq> \<rm>x\<ad>y" using ineq_cancel_left
by simp
then show "(\<rm>x\<ad>y) ∈ L⇧+" using nonneg_definition by simp
from ‹x∈L› ‹y∈L› have "x = 𝟬\<ra>x" and "y = (y\<rs>x)\<ra>x"
using neut_props_loop(2) lrdiv_props(3) by auto
with assms have "𝟬\<ra>x \<lsq> (y\<rs>x)\<ra>x" by simp
with ‹x∈L› ‹𝟬∈L› ‹(y\<rs>x) ∈ L› show "𝟬 \<lsq> y\<rs>x" using ineq_cancel_right
by simp
then show "(y\<rs>x) ∈ L⇧+" using nonneg_definition by simp
qed
text‹We can move an element to the other side of a strict inequality.›
lemma (in loop1) ls_other_side: assumes "x\<ls>y"
shows "𝟬 \<ls> \<rm>x\<ad>y" "(\<rm>x\<ad>y) ∈ L⇩+" "𝟬 \<ls> y\<rs>x" "(y\<rs>x) ∈ L⇩+"
proof -
from assms have "x∈L" "y∈L" "𝟬∈L" "(\<rm>x\<ad>y) ∈ L" "(y\<rs>x) ∈ L"
using lsq_members neut_props_loop(1) lrdiv_props(2,5) by auto
then have "x = x\<ra>𝟬" and "y = x\<ra>(\<rm>x\<ad>y)" using neut_props_loop(2) lrdiv_props(6)
by auto
with assms have "x\<ra>𝟬 \<ls> x\<ra>(\<rm>x\<ad>y)" by simp
with ‹x∈L› ‹𝟬∈L› ‹(\<rm>x\<ad>y) ∈ L› show "𝟬 \<ls> \<rm>x\<ad>y" using strict_ineq_cancel_left
by simp
then show "(\<rm>x\<ad>y) ∈ L⇩+" using posset_definition1 by simp
from ‹x∈L› ‹y∈L› have "x = 𝟬\<ra>x" and "y = (y\<rs>x)\<ra>x"
using neut_props_loop(2) lrdiv_props(3) by auto
with assms have "𝟬\<ra>x \<ls> (y\<rs>x)\<ra>x" by simp
with ‹x∈L› ‹𝟬∈L› ‹(y\<rs>x) ∈ L› show "𝟬 \<ls> y\<rs>x" using strict_ineq_cancel_right
by simp
then show "(y\<rs>x) ∈ L⇩+" using posset_definition1 by simp
qed
text‹We can add sides of inequalities.›
lemma (in loop1) add_ineq: assumes "x\<lsq>y" "z\<lsq>t"
shows "x\<ra>z \<lsq> y\<ra>t"
proof -
from assms have "x\<ra>z \<lsq> y\<ra>z"
using lsq_members(1) ord_trans_inv(1) by simp
with assms show ?thesis using lsq_members(2) ord_trans_inv(2) loop_ord_trans
by simp
qed
text‹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\<ls>y" "z\<ls>t"
shows "x\<ra>z \<ls> y\<ra>t"
proof -
from assms have "x\<ra>z \<ls> y\<ra>z"
using less_members(1) strict_ord_trans_inv(1) by auto
moreover from assms have "y\<ra>z \<ls> y\<ra>t"
using less_members(2) strict_ord_trans_inv(2) by auto
ultimately show ?thesis by (rule loop_strict_ord_trans2)
qed
text‹We can add sides of inequalities one of which is strict. ›
lemma (in loop1) add_ineq_strict1: assumes "x\<lsq>y" "z\<ls>t"
shows "x\<ra>z \<ls> y\<ra>t" and "z\<ra>x \<ls> t\<ra>y"
proof -
from assms have "x\<ra>z \<lsq> y\<ra>z"
using less_members(1) ord_trans_inv(1) by auto
with assms show "x\<ra>z \<ls> y\<ra>t"
using lsq_members(2) strict_ord_trans_inv(2) loop_strict_ord_trans
by blast
from assms have "z\<ra>x \<ls> t\<ra>x"
using lsq_members(1) strict_ord_trans_inv(1) by simp
with assms show "z\<ra>x \<ls> t\<ra>y"
using less_members(2) ord_trans_inv(2) loop_strict_ord_trans1
by blast
qed
text‹Subtracting a positive element decreases the value, while adding a positive element
increases the value. ›
lemma (in loop1) add_subtract_pos: assumes "x∈L" "𝟬\<ls>y"
shows
"x\<rs>y \<ls> x" "(\<rm>y\<ad>x) \<ls> x" "x \<ls> x\<ra>y" "x \<ls> y\<ra>x"
proof -
from assms(2) have "y∈L" using less_members(2) by simp
from assms(1) have "x\<lsq>x"
using ordLoopAssum unfolding IsAnOrdLoop_def IsPartOrder_def refl_def
by simp
with assms(2) have "x\<ra>𝟬 \<ls> x\<ra>y"
using add_ineq_strict1(1) by simp
with assms ‹y∈L› show "x\<rs>y \<ls> x"
using neut_props_loop(2) lrdiv_props(3) lrdiv_props(2) strict_ineq_cancel_right
by simp
from assms(2) ‹x\<lsq>x› have "𝟬\<ra>x \<ls> y\<ra>x"
using add_ineq_strict1(2) by simp
with assms ‹y∈L› show "(\<rm>y\<ad>x) \<ls> x"
using neut_props_loop(2) lrdiv_props(6) lrdiv_props(5) strict_ineq_cancel_left
by simp
from assms(1) ‹x\<ra>𝟬 \<ls> x\<ra>y› ‹𝟬\<ra>x \<ls> y\<ra>x›
show "x \<ls> x\<ra>y" "x \<ls> y\<ra>x"
using neut_props_loop(2) by simp_all
qed
text‹In an ordered loop if the order relation down-directs the set of positive elements $L_+$
then $L_+$ is a down-directed set (see ‹Order_ZF› for definitions of those related but different
notions).›
lemma (in loop1) down_directs_directed: assumes "r {down-directs} L⇩+"
shows "IsDownDirectedSet(L⇩+,r)"
using ordLoopAssum assms positive_subset down_directs_subset
unfolding IsAnOrdLoop_def by auto
subsection‹Completness vs Archimedean property›
text‹For ordered fields the completeness of the order implies the Archimedean property:
for every two positive elements there is a natural number $n$ such that $y < n x$.
In 1891 Otto Stolz "succeeded in proving that the positive cone of a Dedekind complete ordered
abelian group is Archimedean". In this section we consider the relation between the
completeness of the order and the Archimedean property of the positive set of an ordered loop
(not necessarily abelian).›
text‹Multiples of a positive element are positive.›
lemma (in loop1) mults_pos_pos: assumes "𝟬\<ls>x" "n∈nat∖{0}"
shows "𝟬\<ls>n⋅x"
proof -
from assms(1) have "x∈L" using less_members(2) by simp
{ fix m assume "m∈nat"
from ‹x∈L› have "(0 #+ 1)⋅x = 0⋅x\<ra>x" using loop_pow_mult_one
by blast
with assms(1) ‹x∈L› have "𝟬\<ls>(0 #+ 1)⋅x"
using loop_zero_pow neut_props_loop(2) by simp
{ fix j assume "j∈nat" and "𝟬\<ls>(j #+ 1)⋅x"
from ‹x∈L› have I: "(j #+ 1 #+ 1)⋅x = (j #+ 1)⋅x \<ra> x"
using loop_pow_mult_one by blast
from assms(1) ‹x∈L› ‹j∈nat› have "(j #+ 1)⋅x \<ls> (j #+ 1)⋅x \<ra> x"
using loop_prod_type add_subtract_pos(3) by blast
with I have "(j #+ 1)⋅x \<ls> (j #+ 1 #+ 1)⋅x" by simp
with ‹𝟬\<ls>(j #+ 1)⋅x› have "𝟬 \<ls> (j #+ 1 #+ 1)⋅x"
using loop_strict_ord_trans2 by blast
} hence "∀j∈nat. 𝟬\<ls>(j #+ 1)⋅x ⟶ 𝟬 \<ls> (j #+ 1 #+ 1)⋅x"
by simp
with ‹m∈nat› ‹𝟬\<ls>(0 #+ 1)⋅x› have "𝟬 \<ls> (m #+ 1)⋅x"
by (rule ind_on_nat1)
} hence "∀m∈nat. 𝟬 \<ls> (m #+ 1)⋅x" by simp
with assms(2) show "𝟬\<ls>n⋅x" using nat_not0_succ by blast
qed
text‹If the order is complete and $x$ is a positive element of an ordered loop, then
the set $\{n\cdot x: n\in \mathbb{N}, n\neq 0\}$ is not bounded above.›
lemma (in loop1) nat_mult_not_bounded: assumes "r {is complete}" and "𝟬\<ls>x"
shows "¬IsBoundedAbove({n⋅x. n∈nat∖{0}},r)"
proof -
let ?M = "{n⋅x. n∈nat∖{0}}"
{ assume C: "IsBoundedAbove(?M,r)"
let ?S = "Supremum(r,?M)"
from ordLoopAssum assms(1) have
I: "r⊆L×L" "antisym(r)" "r {is complete}" "?M≠∅"
using loop_not_empty unfolding IsAnOrdLoop_def IsPartOrder_def
by auto
from I C have "?S∈L" using compl_bounded_sup_props(1) by simp
from I C have "∀y∈?M. ⟨y,?S⟩ ∈ r" by (rule compl_bounded_sup_props)
hence II: "∀n∈nat∖{0}. n⋅x\<lsq>?S" by simp
{ fix n assume "n∈nat∖{0}"
then have "n #+ 1 ∈ nat∖{0}" by simp
with assms(2) II ‹n∈nat∖{0}› have "n⋅x\<lsq>?S\<rs>x"
using less_members(2) loop_pow_mult_one loop_prod_type ineq_move_side_right
by auto
} hence "∀y∈?M. ⟨y,?S\<rs>x⟩ ∈ r" by auto
with ‹antisym(r)› assms(1) ‹?M≠∅› have "⟨?S,?S\<rs>x⟩ ∈ r"
by (rule compl_sup_leq_up_bnd)
hence "?S\<lsq>?S\<rs>x" by simp
from assms(2) ‹?S∈L› have "?S\<rs>x \<ls> ?S"
using add_subtract_pos(1) by simp
with ‹?S\<lsq>?S\<rs>x› have False using loop_strict_ord_trans
by auto
} thus ?thesis by auto
qed
text‹We say that a nonempty subset $A$ of a ordered loop is Archimedean if
for any two elements $x,y$ of $A$ there is a non-zero natural number $n$ such that
$n\cdot x$ exceeds $y$. ›
definition (in loop1)
IsArchimedean ("_ {is Archimedean}" [90] 91) where
"B {is Archimedean} ≡ B≠∅ ∧ (∀x∈B. ∀y∈B. ∃n∈nat∖{0}. y\<ls>n⋅x)"
text‹If the order of the loop is complete and total on the positive set, then the positive set
is Archimedean.›
theorem (in loop1) loop_pos_set_archimedean:
assumes "L⇩+≠∅" "r {is complete}" and "r {is total on} L⇩+"
shows "L⇩+ {is Archimedean}"
proof -
{ fix x y
assume "x∈L⇩+" "y∈L⇩+"
then have "𝟬\<ls>x" and "y∈L" using posset_definition1 positive_subset
by auto
let ?M = "{n⋅x. n∈nat∖{0}}"
from assms(1,2) ‹𝟬\<ls>x› have "¬(∃u.∀z∈?M. z\<lsq>u)"
using nat_mult_not_bounded IsBoundedAbove_def by simp
then obtain z where "z∈?M" and "¬(z\<lsq>y)" by auto
from ‹z∈?M› obtain n where "n∈nat∖{0}" and "z=n⋅x" by auto
from ‹z=n⋅x› ‹¬(z\<lsq>y)› have "¬(n⋅x\<lsq>y)" by simp
from ‹𝟬\<ls>x› ‹n∈nat∖{0}› have "n⋅x ∈ L⇩+"
using mults_pos_pos posset_definition by force
with assms(3) ‹y∈L⇩+› ‹¬(n⋅x\<lsq>y)› ‹n∈nat∖{0}›
have "∃n∈nat∖{0}. y\<ls>n⋅x" unfolding IsTotal_def by auto
} with assms(1) show "L⇩+ {is Archimedean}"
unfolding IsArchimedean_def by simp
qed
end