Theory OrderedLoop_ZF

(*    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}. 

subsectionDefinition 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)  rL×L  IsPartOrder(L,r)  (xL. yL. zL. 
  ((x,y  r  A` x,z,A`y,z  r)  (x,y  r  A`z,x,A`z,y  r )))"

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

definition
  "Nonnegative(L,A,r)  {xL.  TheNeutralElement(L,A),x  r}"

textThe PositiveSet(L,A,r)› is a set similar to  Nonnegative(L,A,r)›, but without the neutral element.

definition
  "PositiveSet(L,A,r)  
  {xL.  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  xy"
  
  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"
    
textTheorems 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

textIn this context $x \leq y$ implies that both $x$ and $y$ belong
  to $L$.

lemma (in loop1) lsq_members: assumes "x\<lsq>y" shows "xL" and "yL" 
  using ordLoopAssum assms IsAnOrdLoop_def by auto

textIn this context $x < y$ implies that both $x$ and $y$ belong
  to $L$.

lemma (in loop1) less_members: assumes "x\<ls>y" shows "xL" and "yL" 
  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" "zL"
  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" "zL"
  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

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

lemma (in loop1) ineq_cancel_right: assumes "xL" "yL" "zL" 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

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

lemma (in loop1) strict_ineq_cancel_right: assumes "xL" "yL" "zL" and "x\<ra>z \<ls> y\<ra>z" 
  shows  "x\<ls>y"
  using assms ineq_cancel_right by auto

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

lemma (in loop1) ineq_cancel_left: assumes "xL" "yL" "zL" 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

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

lemma (in loop1) strict_ineq_cancel_left: 
  assumes "xL" "yL" "zL" and "z\<ra>x \<ls> z\<ra>y" 
  shows  "x\<ls>y"
  using assms ineq_cancel_left by auto

textThe 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

textThe nonnegative set is contained in the loop.

lemma (in loop1) nonneg_subset: shows "L+  L"
  using Nonnegative_def by auto 

textThe positive set is contained in the loop.

lemma (in loop1) positive_subset: shows "L+  L"
  using PositiveSet_def by auto

textThe 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

textAnother 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 "xL" 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 "xL" "yL" "𝟬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 xL 𝟬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 xL yL 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 xL 𝟬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 "xL" "yL" "𝟬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 xL 𝟬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 xL yL 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 xL 𝟬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

textWe 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

textWe 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

textWe 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

textSubtracting a positive element decreases the value. 

lemma (in loop1) subtract_pos: assumes "xL" "𝟬\<ls>y"
  shows "x\<rs>y \<ls> x" and "(\<rm>y\<ad>x) \<ls> x"
proof -
  from assms(2) have "yL" 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 yL 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 yL 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