(* This file is a part of IsarMathLib - a library of formalized mathematics for Isabelle/Isar. Copyright (C) 2021 Slawomir Kolodynski This program is free software; Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: 1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer. 2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution. 3. The name of the author may not be used to endorse or promote products derived from this software without specific prior written permission. THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. *) 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