Theory OrderedLoop_ZF
section ‹ Ordered loops ›
theory OrderedLoop_ZF imports Loop_ZF Order_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 and notation›
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.›
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⟩"
text‹Theorems proven in the ‹loop0› locale are valid in the ‹loop1› locale›
sublocale loop1 < loop0 L A looper
using ordLoopAssum loop_loop0_valid unfolding IsAnOrdLoop_def by auto
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‹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‹ 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. ›
lemma (in loop1) subtract_pos: assumes "x∈L" "𝟬\<ls>y"
shows "x\<rs>y \<ls> x" and "(\<rm>y\<ad>x) \<ls> 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
qed
end