Theory OrderedRing_ZF

(*
    This file is a part of IsarMathLib - 
    a library of formalized mathematics for Isabelle/Isar.

    Copyright (C) 2005, 2006  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.

*)

header {*\isaheader{OrderedRing\_ZF.thy}*}

theory OrderedRing_ZF imports Ring_ZF OrderedGroup_ZF 

begin

text{*In this theory file we consider ordered rings.*}

section{*Definition and notation*}

text{*This section defines ordered rings and sets up appriopriate notation.*}

text{*We define ordered ring as a commutative ring with linear order 
  that is preserved by 
  translations and such that the set of nonnegative elements is closed
  under multiplication. Note that this definition does not guarantee 
  that there are no zero divisors in the ring.*}

constdefs 

  "IsAnOrdRing(R,A,M,r) ≡ 
  ( IsAring(R,A,M) ∧ (M {is commutative on} R) ∧ 
  r⊆R×R ∧ IsLinOrder(R,r) ∧
  (∀a b. ∀ c∈R. <a,b> ∈ r --> ⟨A`<a,c>,A`<b,c>⟩ ∈ r) ∧
  (Nonnegative(R,A,r) {is closed under} M))"

text{*The next context (locale) defines notation used for ordered rings. 
  We do that by extending the notation defined in the 
  @{text "ring0"} locale and adding some assumptions to make sure we are 
  talking about ordered rings in this context.*}

locale ring1 = ring0 +

  assumes mult_commut: "M {is commutative on} R" 

  fixes r
  
  assumes ordincl: "r ⊆ R×R"

  assumes linord: "IsLinOrder(R,r)"
  
  fixes lesseq (infix "\<lsq>" 68)
  defines lesseq_def [simp]: "a \<lsq> b ≡ <a,b> ∈ r"

  fixes sless (infix "\<ls>" 68)
  defines sless_def [simp]: "a \<ls> b ≡ a\<lsq>b ∧ a≠b"

  assumes ordgroup: "∀a b. ∀ c∈R. a\<lsq>b --> a\<ra>c \<lsq> b\<ra>c"

  assumes pos_mult_closed: "Nonnegative(R,A,r) {is closed under} M"

  fixes abs ("| _ |")
  defines abs_def [simp]: "|a| ≡ AbsoluteValue(R,A,r)`(a)"

  fixes positiveset ("R+")
  defines positiveset_def [simp]: "R+ ≡ PositiveSet(R,A,r)"

text{*The next lemma assures us that we are talking about ordered rings 
  in the @{text "ring1"} context.*}

lemma (in ring1) OrdRing_ZF_1_L1: shows "IsAnOrdRing(R,A,M,r)"
  using ring0_def ringAssum mult_commut ordincl linord ordgroup 
    pos_mult_closed IsAnOrdRing_def by simp;

text{*We can use theorems proven in the @{text "ring1"} context whenever we
  talk about an ordered ring.*}

lemma OrdRing_ZF_1_L2: assumes "IsAnOrdRing(R,A,M,r)"
  shows "ring1(R,A,M,r)"
  using prems IsAnOrdRing_def ring1_axioms.intro ring0_def ring1_def
  by simp;

text{*In the @{text "ring1"} context $a\leq b$ implies that $a,b$ are
  elements of the ring.*}

lemma (in  ring1) OrdRing_ZF_1_L3: assumes "a\<lsq>b"
  shows "a∈R"  "b∈R"
  using prems ordincl by auto;

text{*Ordered ring is an ordered group, hence we can use theorems
  proven in the @{text "group3"} context.*}

lemma (in  ring1) OrdRing_ZF_1_L4: shows 
  "IsAnOrdGroup(R,A,r)"
  "r {is total on} R"
  "A {is commutative on} R"
  "group3(R,A,r)"
proof -;
  { fix a b g assume A1: "g∈R" and A2: "a\<lsq>b" 
    with ordgroup have "a\<ra>g \<lsq> b\<ra>g"
      by simp;
    moreover from ringAssum A1 A2 have 
      "a\<ra>g = g\<ra>a"  "b\<ra>g = g\<ra>b"
      using OrdRing_ZF_1_L3 IsAring_def IsCommutative_def by auto;
    ultimately have
      "a\<ra>g \<lsq> b\<ra>g"  "g\<ra>a \<lsq> g\<ra>b"
      by auto;
  } hence 
    "∀g∈R. ∀a b. a\<lsq>b --> a\<ra>g \<lsq> b\<ra>g ∧ g\<ra>a \<lsq> g\<ra>b"
    by simp;
  with ringAssum ordincl linord show  
    "IsAnOrdGroup(R,A,r)"
    "group3(R,A,r)"
    "r {is total on} R"
    "A {is commutative on} R"
    using IsAring_def Order_ZF_1_L2 IsAnOrdGroup_def group3_def IsLinOrder_def
    by auto;
qed;

text{*The order relation in rings is transitive.*}

lemma (in ring1) ring_ord_transitive: assumes A1: "a\<lsq>b"  "b\<lsq>c"
  shows "a\<lsq>c"
proof -
  from A1 have 
    "group3(R,A,r)"  "⟨a,b⟩ ∈ r"   "⟨b,c⟩ ∈ r"
    using OrdRing_ZF_1_L4 by auto;
  then have "⟨a,c⟩ ∈ r" by (rule group3.Group_order_transitive);
  then show  "a\<lsq>c" by simp
qed

text{*Transitivity for the strict order: if $a<b$ and $b\leq c$, then $a<c$. 
  Property of ordered groups.*}

lemma (in ring1) ring_strict_ord_trans:  
  assumes A1: "a\<ls>b" and A2: "b\<lsq>c"
  shows "a\<ls>c"
proof -
  from A1 A2 have
    "group3(R,A,r)"  
    "⟨a,b⟩ ∈ r ∧ a≠b"  "⟨b,c⟩ ∈ r"
    using OrdRing_ZF_1_L4 by auto
    then have "⟨a,c⟩ ∈ r ∧ a≠c" by (rule group3.OrderedGroup_ZF_1_L4A)
    then show "a\<ls>c" by simp
qed;

text{*Another version of transitivity for the strict order: 
  if $a\leq b$ and $b<c$, then $a<c$. Property of ordered groups.*}

lemma (in ring1) ring_strict_ord_transit: 
  assumes A1: "a\<lsq>b" and A2: "b\<ls>c"
  shows "a\<ls>c"
proof -
  from A1 A2 have
    "group3(R,A,r)"  
    "⟨a,b⟩ ∈ r"  "⟨b,c⟩ ∈ r ∧ b≠c"
    using OrdRing_ZF_1_L4 by auto
  then have "⟨a,c⟩ ∈ r ∧ a≠c" by (rule group3.group_strict_ord_transit)
  then show "a\<ls>c" by simp
qed;

text{*The next lemma shows what happens when one element of an ordered
  ring is not greater or equal than another.*}

lemma (in ring1) OrdRing_ZF_1_L4A: assumes A1: "a∈R"  "b∈R"
  and A2: "¬(a\<lsq>b)"
  shows "b \<lsq> a"  "(\<rm>a) \<lsq> (\<rm>b)"  "a≠b"
proof -
  from A1 A2 have I: 
    "group3(R,A,r)"
    "r {is total on} R"
    "a ∈ R"  "b ∈ R"  "⟨a, b⟩ ∉ r"
    using OrdRing_ZF_1_L4 by auto;
  then have "⟨b,a⟩ ∈ r" by (rule  group3.OrderedGroup_ZF_1_L8);
  then show "b \<lsq> a" by simp;
  from I have "⟨GroupInv(R,A)`(a),GroupInv(R,A)`(b)⟩ ∈ r"
    by (rule  group3.OrderedGroup_ZF_1_L8);
  then show  "(\<rm>a) \<lsq> (\<rm>b)" by simp;
  from I show "a≠b" by (rule group3.OrderedGroup_ZF_1_L8);
qed;

text{*A special case of @{text "OrdRing_ZF_1_L4A"} when one of the
  constants is $0$. This is useful for many proofs by cases.*}

corollary (in ring1) ord_ring_split2: assumes A1: "a∈R" 
  shows "a\<lsq>\<zero> ∨ (\<zero>\<lsq>a ∧ a≠\<zero>)"
proof -
  { from A1 have  I: "a∈R"  "\<zero>∈R"
      using Ring_ZF_1_L2 by auto; 
    moreover assume A2: "¬(a\<lsq>\<zero>)"
    ultimately have "\<zero>\<lsq>a" by (rule OrdRing_ZF_1_L4A);
    moreover from I A2 have "a≠\<zero>" by (rule OrdRing_ZF_1_L4A);
    ultimately have "\<zero>\<lsq>a ∧ a≠\<zero>" by simp}
  then show ?thesis by auto
qed;

text{*Taking minus on both sides reverses an inequality.*}

lemma (in ring1) OrdRing_ZF_1_L4B: assumes "a\<lsq>b"
  shows "(\<rm>b) \<lsq> (\<rm>a)"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L5
  by simp;

text{*The next lemma just expands the condition that requires the set
  of nonnegative elements to be closed with respect to multiplication.
  These are properties of totally ordered groups.*}
  
lemma (in  ring1) OrdRing_ZF_1_L5: 
  assumes "\<zero>\<lsq>a"  "\<zero>\<lsq>b"
  shows "\<zero> \<lsq> a·b"
  using pos_mult_closed prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L2
  IsOpClosed_def by simp;

text{*Double nonnegative is nonnegative.*}

lemma (in  ring1) OrdRing_ZF_1_L5A: assumes A1: "\<zero>\<lsq>a"
  shows "\<zero>\<lsq>\<two>·a"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L5G
  OrdRing_ZF_1_L3 Ring_ZF_1_L3 by simp;

text{*A sufficient (somewhat redundant) condition for a structure to be an 
  ordered ring. It says that a commutative ring that is a totally ordered
  group with respect to the additive operation such that set of nonnegative 
  elements is closed under multiplication, is an ordered ring.*}

lemma OrdRing_ZF_1_L6:
  assumes  
  "IsAring(R,A,M)"   
  "M {is commutative on} R"
  "Nonnegative(R,A,r) {is closed under} M"
  "IsAnOrdGroup(R,A,r)"  
  "r {is total on} R"
  shows "IsAnOrdRing(R,A,M,r)"
  using prems IsAnOrdGroup_def Order_ZF_1_L3 IsAnOrdRing_def
  by simp;

text{*$a\leq b$ iff $a-b\leq 0$. This is a fact from 
  @{text "OrderedGroup.thy"}, where it is stated in multiplicative notation.*}

lemma (in ring1) OrdRing_ZF_1_L7:
  assumes "a∈R"  "b∈R"
  shows "a\<lsq>b <-> a\<rs>b \<lsq> \<zero>"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L9
  by simp;

text{*Negative times positive is negative.*}

lemma (in ring1) OrdRing_ZF_1_L8:
  assumes A1: "a\<lsq>\<zero>"  and A2: "\<zero>\<lsq>b"
  shows "a·b \<lsq> \<zero>"
proof -
  from A1 A2 have T1: "a∈R"  "b∈R"  "a·b ∈ R"
    using OrdRing_ZF_1_L3 Ring_ZF_1_L4 by auto;
  from A1 A2 have "\<zero>\<lsq>(\<rm>a)·b" 
    using OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L5A OrdRing_ZF_1_L5
    by simp;
  with T1 show "a·b \<lsq> \<zero>"
    using Ring_ZF_1_L7 OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L5AA
    by simp;
qed;

text{*We can multiply both sides of an inequality by a nonnegative ring
  element. This property is sometimes (not here) used to define
  ordered rings. *}

lemma (in ring1) OrdRing_ZF_1_L9:
  assumes A1: "a\<lsq>b" and A2: "\<zero>\<lsq>c"
  shows 
  "a·c \<lsq> b·c"  
  "c·a \<lsq> c·b"
proof -
  from A1 A2 have T1:
    "a∈R"  "b∈R"  "c∈R"  "a·c ∈ R"  "b·c ∈ R"
    using OrdRing_ZF_1_L3 Ring_ZF_1_L4 by auto;
  with A1 A2 have "(a\<rs>b)·c \<lsq> \<zero>"
    using OrdRing_ZF_1_L7 OrdRing_ZF_1_L8 by simp;
  with T1 show "a·c \<lsq> b·c"
    using Ring_ZF_1_L8 OrdRing_ZF_1_L7 by simp;
  with mult_commut T1 show "c·a \<lsq> c·b"
    using IsCommutative_def by simp;
qed;

text{*A special case of @{text "OrdRing_ZF_1_L9"}: we can multiply
  an inequality by a positive ring element.*}

lemma (in ring1) OrdRing_ZF_1_L9A:
  assumes A1: "a\<lsq>b" and A2: "c∈R+"
  shows  
  "a·c \<lsq> b·c"  
  "c·a \<lsq> c·b"
proof -
  from A2 have "\<zero> \<lsq> c" using PositiveSet_def
    by simp;
  with A1 show "a·c \<lsq> b·c"  "c·a \<lsq> c·b"
    using OrdRing_ZF_1_L9 by auto;
qed;    

text{*A square is nonnegative.*}

lemma (in ring1) OrdRing_ZF_1_L10:
  assumes A1: "a∈R" shows "\<zero>\<lsq>(a²)"
proof (cases "\<zero>\<lsq>a");
  assume "\<zero>\<lsq>a"
  then show "\<zero>\<lsq>(a²)" using OrdRing_ZF_1_L5
    by simp;
next assume "¬(\<zero>\<lsq>a)"
  with A1 have "\<zero>\<lsq>((\<rm>a)²)"
    using OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L8A
      OrdRing_ZF_1_L5 by simp;
  with A1 show "\<zero>\<lsq>(a²)" using Ring_ZF_1_L14
    by simp;
qed;

text{*$1$ is nonnegative.*}

corollary (in ring1) ordring_one_is_nonneg: shows "\<zero> \<lsq> \<one>"
proof -
  have "\<zero> \<lsq> (\<one>²)" using Ring_ZF_1_L2 OrdRing_ZF_1_L10
    by simp;
  then show "\<zero> \<lsq> \<one>" using Ring_ZF_1_L2 Ring_ZF_1_L3
    by simp;
qed;

text{*In nontrivial rings one is positive.*}

lemma (in ring1) ordring_one_is_pos: assumes "\<zero>≠\<one>"
  shows "\<one> ∈ R+"
  using prems Ring_ZF_1_L2 ordring_one_is_nonneg PositiveSet_def
  by auto;
    
text{*Nonnegative is not negative. Property of ordered groups.*}

lemma (in ring1) OrdRing_ZF_1_L11: assumes "\<zero>\<lsq>a"
  shows "¬(a\<lsq>\<zero> ∧ a≠\<zero>)"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L5AB
  by simp;

text{*A negative element cannot be a square.*}

lemma (in ring1) OrdRing_ZF_1_L12: 
  assumes A1: "a\<lsq>\<zero>"  "a≠\<zero>"
  shows "¬(∃b∈R. a = (b²))"
proof -
  { assume "∃b∈R. a = (b²)"
    with A1 have False using OrdRing_ZF_1_L10 OrdRing_ZF_1_L11
      by auto;
  } then show ?thesis by auto;
qed;

text{*If $a\leq b$, then $0\leq b-a$.*}

lemma (in ring1) OrdRing_ZF_1_L13: assumes "a\<lsq>b"
  shows "\<zero> \<lsq> b\<rs>a"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L9D
  by simp;

text{*If $a<b$, then $0<b-a$.*}

lemma (in ring1) OrdRing_ZF_1_L14: assumes "a\<lsq>b"  "a≠b"
  shows 
  "\<zero> \<lsq> b\<rs>a"  "\<zero> ≠ b\<rs>a"  
  "b\<rs>a ∈ R+"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L9E
  by auto;

text{*If the difference is nonnegative, then $a\leq b$. *}

lemma (in ring1) OrdRing_ZF_1_L15: 
  assumes "a∈R" "b∈R" and "\<zero> \<lsq> b\<rs>a"
  shows "a\<lsq>b"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L9F
  by simp;
  

text{*A nonnegative number is does not decrease when multiplied by 
  a number greater or equal $1$.*}

lemma (in ring1) OrdRing_ZF_1_L16: 
  assumes A1: "\<zero>\<lsq>a" and A2: "\<one>\<lsq>b"
  shows "a\<lsq>a·b"
proof -
  from A1 A2 have T: "a∈R"  "b∈R"  "a·b ∈ R"
    using OrdRing_ZF_1_L3 Ring_ZF_1_L4 by auto
  from A1 A2 have "\<zero> \<lsq> a·(b\<rs>\<one>)"
    using OrdRing_ZF_1_L13 OrdRing_ZF_1_L5 by simp;
  with T show "a\<lsq>a·b"
    using Ring_ZF_1_L8 Ring_ZF_1_L2 Ring_ZF_1_L3 OrdRing_ZF_1_L15
    by simp;
qed;
  
text{*We can multiply the right hand side of an inequality between
  nonnegative ring elements by an element greater or equal $1$.*}

lemma (in ring1) OrdRing_ZF_1_L17: 
  assumes A1: "\<zero>\<lsq>a" and A2: "a\<lsq>b" and A3: "\<one>\<lsq>c"
  shows "a\<lsq>b·c"
proof -
  from A1 A2 have "\<zero>\<lsq>b" by (rule ring_ord_transitive);
  with A3 have "b\<lsq>b·c" using OrdRing_ZF_1_L16
    by simp;
  with A2 show "a\<lsq>b·c" by (rule ring_ord_transitive);
qed;

text{*Strict order is preserved by translations.*}

lemma (in ring1) ring_strict_ord_trans_inv: 
  assumes "a\<ls>b" and "c∈R"
  shows  
  "a\<ra>c \<ls> b\<ra>c"
  "c\<ra>a \<ls> c\<ra>b"
  using prems OrdRing_ZF_1_L4 group3.group_strict_ord_transl_inv
  by auto;

text{*We can put an element on the other side of a strict inequality,
  changing its sign.*}

lemma (in ring1) OrdRing_ZF_1_L18:
  assumes "a∈R"  "b∈R" and  "a\<rs>b \<ls> c"
  shows "a \<ls> c\<ra>b"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L12B
  by simp;

text{*We can add the sides of two inequalities,
  the first of them strict, and we get a strict inequality. 
  Property of ordered groups.*}

lemma (in ring1) OrdRing_ZF_1_L19:
  assumes "a\<ls>b" and "c\<lsq>d"
  shows "a\<ra>c \<ls> b\<ra>d"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L12C
  by simp;

text{*We can add the sides of two inequalities,
  the second of them strict and we get a strict inequality. 
  Property of ordered groups.*}

lemma (in ring1) OrdRing_ZF_1_L20:
  assumes "a\<lsq>b" and "c\<ls>d"
  shows "a\<ra>c \<ls> b\<ra>d"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L12D
  by simp;

section{*Absolute value for ordered rings*}

text{*Absolute value is defined for ordered groups as a function 
  that is the identity on the nonnegative set and the negative of the element 
  (the inverse in the multiplicative notation) on the rest. In this section
  we consider properties of absolute value related to multiplication in 
  ordered rings.*}


text{*Absolute value of a product is the product of absolute values: 
  the case when both elements of the ring are nonnegative.*}

lemma (in ring1) OrdRing_ZF_2_L1: 
  assumes "\<zero>\<lsq>a" "\<zero>\<lsq>b"
  shows "|a·b| = |a|·|b|"
  using prems OrdRing_ZF_1_L5 OrdRing_ZF_1_L4 
    group3.OrderedGroup_ZF_1_L2 group3.OrderedGroup_ZF_3_L2
  by simp;

text{*The absolue value of an element and its negative are the same.*}

lemma (in ring1) OrdRing_ZF_2_L2: assumes "a∈R"
  shows "|\<rm>a| = |a|"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_3_L7A by simp;

text{*The next lemma states that 
  $|a\cdot (-b)| = |(-a)\cdot b| = |(-a)\cdot (-b)| = |a\cdot b|$.*}

lemma (in ring1) OrdRing_ZF_2_L3:
  assumes "a∈R"  "b∈R"
  shows 
  "|(\<rm>a)·b| = |a·b|"
  "|a·(\<rm>b)| = |a·b|"
  "|(\<rm>a)·(\<rm>b)| = |a·b|"
  using prems Ring_ZF_1_L4 Ring_ZF_1_L7 Ring_ZF_1_L7A 
   OrdRing_ZF_2_L2 by auto;

text{*This lemma allows to prove theorems for the case of positive and 
  negative elements of the ring separately.*}

lemma (in ring1) OrdRing_ZF_2_L4: assumes "a∈R" and "¬(\<zero>\<lsq>a)" 
  shows "\<zero> \<lsq> (\<rm>a)"  "\<zero>≠a"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L8A
  by auto;
  
text{*Absolute value of a product is the product of absolute values.*}

lemma (in ring1) OrdRing_ZF_2_L5:
  assumes A1: "a∈R" "b∈R"
  shows "|a·b| = |a|·|b|"
proof (cases "\<zero>\<lsq>a")
  assume A2: "\<zero>\<lsq>a" show "|a·b| = |a|·|b|"
  proof (cases "\<zero>\<lsq>b")
    assume "\<zero>\<lsq>b"
    with A2 show "|a·b| = |a|·|b|"
      using OrdRing_ZF_2_L1 by simp;
  next assume "¬(\<zero>\<lsq>b)" 
    with A1 A2 have "|a·(\<rm>b)| = |a|·|\<rm>b|"
       using OrdRing_ZF_2_L4 OrdRing_ZF_2_L1 by simp;
    with A1 show "|a·b| = |a|·|b|"
      using OrdRing_ZF_2_L2 OrdRing_ZF_2_L3 by simp;
  qed;
next assume "¬(\<zero>\<lsq>a)"
  with A1 have A3: "\<zero> \<lsq> (\<rm>a)"
    using OrdRing_ZF_2_L4 by simp;
  show "|a·b| = |a|·|b|"
  proof (cases "\<zero>\<lsq>b")
    assume "\<zero>\<lsq>b" 
    with A3 have "|(\<rm>a)·b| = |\<rm>a|·|b|"
      using OrdRing_ZF_2_L1 by simp;
    with A1 show "|a·b| = |a|·|b|"
      using OrdRing_ZF_2_L2 OrdRing_ZF_2_L3 by simp;
  next assume "¬(\<zero>\<lsq>b)"
    with A1 A3 have "|(\<rm>a)·(\<rm>b)| = |\<rm>a|·|\<rm>b|"
      using OrdRing_ZF_2_L4 OrdRing_ZF_2_L1 by simp;
    with A1 show "|a·b| = |a|·|b|"
      using OrdRing_ZF_2_L2 OrdRing_ZF_2_L3 by simp;
  qed;
qed;

text{*Triangle inequality. Property of linearly ordered abelian groups.*}

lemma (in ring1) ord_ring_triangle_ineq:  assumes "a∈R" "b∈R"
  shows "|a\<ra>b| \<lsq> |a|\<ra>|b|"
  using prems OrdRing_ZF_1_L4 group3.OrdGroup_triangle_ineq 
  by simp;

text{*If $a\leq c$ and $b\leq c$, then $a+b\leq 2\cdot c$.*}

lemma (in ring1) OrdRing_ZF_2_L6:
  assumes "a\<lsq>c"  "b\<lsq>c" shows "a\<ra>b \<lsq> \<two>·c"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L5B 
    OrdRing_ZF_1_L3 Ring_ZF_1_L3 by simp;

section{*Positivity in ordered rings*}

text{*This section is about properties of the set of positive
  elements @{text "R+"}. *}

text{*The set of positive elements is closed under ring addition. 
  This is a property of ordered groups, we just reference a theorem
  from @{text "OrderedGroup_ZF"} theory in the proof.*}

lemma (in ring1) OrdRing_ZF_3_L1: shows "R+ {is closed under} A"
  using OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L13
  by simp;

text{*Every element of a ring can be either in the postitive set, equal to
  zero or its opposite (the additive inverse) is in the positive set. 
  This is a property of ordered groups, we just reference a theorem
  from @{text "OrderedGroup_ZF"} theory.*}

lemma (in ring1) OrdRing_ZF_3_L2: assumes "a∈R"
  shows "Exactly_1_of_3_holds (a=\<zero>, a∈R+, (\<rm>a) ∈ R+)"
  using prems OrdRing_ZF_1_L4 group3.OrdGroup_decomp
  by simp;

text{*If a ring element $a\neq 0$, and it is not positive, then 
  $-a$ is positive.*}

lemma (in ring1) OrdRing_ZF_3_L2A: assumes "a∈R"  "a≠\<zero>"  "a ∉ R+"
  shows "(\<rm>a) ∈  R+"
  using prems OrdRing_ZF_1_L4 group3.OrdGroup_cases
  by simp;

text{*@{text "R+"} is closed under
  multiplication iff the ring has no zero divisors. *}

lemma (in ring1) OrdRing_ZF_3_L3: 
  shows "(R+ {is closed under} M)<-> HasNoZeroDivs(R,A,M)"
proof;
  assume A1: "HasNoZeroDivs(R,A,M)"
  { fix a b assume "a∈R+"  "b∈R+"
    then have "\<zero>\<lsq>a"  "a≠\<zero>"  "\<zero>\<lsq>b"  "b≠\<zero>"
      using PositiveSet_def by auto;
    with A1 have "a·b ∈ R+"
      using OrdRing_ZF_1_L5 Ring_ZF_1_L2 OrdRing_ZF_1_L3 Ring_ZF_1_L12
        OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L2A
      by simp;
  } then show  "R+ {is closed under} M" using IsOpClosed_def
    by simp;
next assume A2: "R+ {is closed under} M"
  { fix a b assume A3: "a∈R"  "b∈R"  and "a≠\<zero>"  "b≠\<zero>"
    with A2 have "|a·b| ∈ R+"
      using OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_3_L12 IsOpClosed_def
        OrdRing_ZF_2_L5 by simp;
    with A3 have "a·b ≠ \<zero>" 
      using PositiveSet_def Ring_ZF_1_L4 
        OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_3_L2A 
      by auto;
  } then show "HasNoZeroDivs(R,A,M)" using HasNoZeroDivs_def 
    by auto;
qed;

text{*Another (in addition to @{text "OrdRing_ZF_1_L6"} sufficient condition 
  that defines order in an ordered ring starting from the positive set.*}

theorem (in ring0) ring_ord_by_positive_set:
  assumes
  A1: "M {is commutative on} R" and 
  A2: "P⊆R"  "P {is closed under} A"  "\<zero> ∉ P" and
  A3: "∀a∈R. a≠\<zero> --> (a∈P) Xor ((\<rm>a) ∈ P)" and
  A4: "P {is closed under} M" and 
  A5: "r = OrderFromPosSet(R,A,P)"
  shows
  "IsAnOrdGroup(R,A,r)"
  "IsAnOrdRing(R,A,M,r)"
  "r {is total on} R"
  "PositiveSet(R,A,r) = P"
  "Nonnegative(R,A,r) = P ∪ {\<zero>}"
  "HasNoZeroDivs(R,A,M)"
proof -
  from A2 A3 A5 show
    I: "IsAnOrdGroup(R,A,r)"  "r {is total on} R" and 
    II: "PositiveSet(R,A,r) = P" and 
    III: "Nonnegative(R,A,r) = P ∪ {\<zero>}"
    using Ring_ZF_1_L1 group0.Group_ord_by_positive_set
    by auto;
  from A2 A4 III have "Nonnegative(R,A,r) {is closed under} M"
    using Ring_ZF_1_L16 by simp;
  with ringAssum A1 I show "IsAnOrdRing(R,A,M,r)"
    using OrdRing_ZF_1_L6 by simp;
  with A4 II show "HasNoZeroDivs(R,A,M)"
    using OrdRing_ZF_1_L2 ring1.OrdRing_ZF_3_L3
    by auto;
qed;

text{*Nontrivial ordered rings are infinite. More precisely we assume 
  that the neutral
  element of the additive operation is not equal to the multiplicative neutral
  element and show that the the set of positive elements of the ring is not a 
  finite subset of the ring and the ring is not a finite subset of itself.*}

theorem (in ring1) ord_ring_infinite: assumes "\<zero>≠\<one>"
  shows 
  "R+ ∉ Fin(R)"
  "R ∉ Fin(R)"
  using prems Ring_ZF_1_L17 OrdRing_ZF_1_L4 group3.Linord_group_infinite
  by auto;

lemma (in ring1) OrdRing_ZF_3_L4: 
  assumes "\<zero>≠\<one>" and "∀a∈R. ∃b∈B. a\<lsq>b"
  shows 
  "¬IsBoundedAbove(B,r)"
  "B ∉ Fin(R)"
  using prems Ring_ZF_1_L17 OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_2_L2A
  by auto;
  

text{*If $m$ is greater or equal the multiplicative unit, then the set
  $\{m\cdot n: n\in R\}$ is infinite (unless the ring is trivial).*}

lemma (in ring1) OrdRing_ZF_3_L5: assumes A1: "\<zero>≠\<one>" and A2: "\<one>\<lsq>m"
  shows
  "{m·x. x∈R+} ∉ Fin(R)"
  "{m·x. x∈R} ∉ Fin(R)"
  "{(\<rm>m)·x. x∈R} ∉ Fin(R)"
proof -
  from A2 have T: "m∈R" using OrdRing_ZF_1_L3 by simp
  from A2 have "\<zero>\<lsq>\<one>"  "\<one>\<lsq>m"
    using ordring_one_is_nonneg by auto;
  then have I: "\<zero>\<lsq>m" by (rule ring_ord_transitive);
  let ?B = "{m·x. x∈R+}"
  { fix a assume A3: "a∈R"
    then have "a\<lsq>\<zero> ∨ (\<zero>\<lsq>a ∧ a≠\<zero>)"
      using ord_ring_split2 by simp;
    moreover
    { assume A4: "a\<lsq>\<zero>"
      from A1 have "m·\<one> ∈ ?B" using ordring_one_is_pos
        by auto;
      with T have "m∈?B" using Ring_ZF_1_L3 by simp;
      moreover from A4 I have "a\<lsq>m" by (rule ring_ord_transitive);
      ultimately have "∃b∈?B. a\<lsq>b" by blast }
    moreover
    { assume A4: "\<zero>\<lsq>a ∧ a≠\<zero>"
      with A3 have "m·a ∈ ?B" using PositiveSet_def
        by auto;
      moreover
      from A2 A4 have "\<one>·a \<lsq> m·a" using OrdRing_ZF_1_L9
        by simp;
      with A3 have "a \<lsq> m·a" using Ring_ZF_1_L3 
        by simp;
      ultimately have "∃b∈?B. a\<lsq>b" by auto }
    ultimately have "∃b∈?B. a\<lsq>b" by auto;
  } then have "∀a∈R. ∃b∈?B. a\<lsq>b"
    by simp;
  with A1 show "?B ∉ Fin(R)" using OrdRing_ZF_3_L4
    by simp;
  moreover have "?B ⊆ {m·x. x∈R}"
    using PositiveSet_def by auto;
  ultimately show "{m·x. x∈R} ∉ Fin(R)" using Fin_subset
    by auto;
  with T show "{(\<rm>m)·x. x∈R} ∉ Fin(R)" using Ring_ZF_1_L18
    by simp
qed;

text{*If $m$ is less or equal than the negative of 
  multiplicative unit, then the set
  $\{m\cdot n: n\in R\}$ is infinite (unless the ring is trivial).*}

lemma (in ring1) OrdRing_ZF_3_L6: assumes A1: "\<zero>≠\<one>" and A2: "m \<lsq> \<rm>\<one>"
  shows "{m·x. x∈R} ∉ Fin(R)"
proof -
  from A2 have "(\<rm>(\<rm>\<one>)) \<lsq> \<rm>m"
    using OrdRing_ZF_1_L4B by simp;
  with A1 have "{(\<rm>m)·x. x∈R} ∉ Fin(R)"
    using Ring_ZF_1_L2 Ring_ZF_1_L3 OrdRing_ZF_3_L5
    by simp;
  with A2 show "{m·x. x∈R} ∉ Fin(R)"
    using OrdRing_ZF_1_L3 Ring_ZF_1_L18 by simp;
qed;

text{*All elements greater or equal than an element of @{text "R+"}
  belong to @{text "R+"}. Property of ordered groups.*}

lemma (in ring1) OrdRing_ZF_3_L7: assumes A1: "a ∈ R+" and A2: "a\<lsq>b"
  shows "b ∈ R+"
proof -
  from A1 A2 have 
    "group3(R,A,r)"
    "a ∈ PositiveSet(R,A,r)"
    "⟨a,b⟩ ∈ r"
    using OrdRing_ZF_1_L4 by auto;
  then have "b ∈ PositiveSet(R,A,r)" 
    by (rule group3.OrderedGroup_ZF_1_L19);
  then show "b ∈ R+" by simp;
qed;

text{*A special case of @{text "OrdRing_ZF_3_L7"}: a ring element greater
  or equal than $1$ is positive.*}

corollary (in ring1) OrdRing_ZF_3_L8: assumes A1: "\<zero>≠\<one>" and A2: "\<one>\<lsq>a"
  shows "a ∈ R+"
proof -
  from A1 A2 have "\<one> ∈ R+"  "\<one>\<lsq>a"
    using ordring_one_is_pos by auto
  then show "a ∈ R+" by (rule OrdRing_ZF_3_L7);
qed;

text{*Adding a positive element to $a$ strictly increases $a$.
  Property of ordered groups.*}

lemma (in ring1) OrdRing_ZF_3_L9: assumes A1: "a∈R"  "b∈R+"
  shows "a \<lsq> a\<ra>b"  "a ≠ a\<ra>b"
  using prems OrdRing_ZF_1_L4 group3.OrderedGroup_ZF_1_L22
  by auto;

text{*A special case of @{text " OrdRing_ZF_3_L9"}: in nontrivial
  rings adding one to $a$ increases $a$. *}

corollary (in ring1) OrdRing_ZF_3_L10: assumes A1: "\<zero>≠\<one>" and A2: "a∈R"
  shows "a \<lsq> a\<ra>\<one>"  "a ≠ a\<ra>\<one>"
  using prems ordring_one_is_pos OrdRing_ZF_3_L9
  by auto;

text{*If $a$ is not greater than $b$, then it is strictly less than
  $b+1$.*}

lemma (in ring1) OrdRing_ZF_3_L11: assumes A1: "\<zero>≠\<one>" and A2: "a\<lsq>b"
  shows "a\<ls> b\<ra>\<one>"
proof -
  from A1 A2 have I: "b \<ls> b\<ra>\<one>"
    using OrdRing_ZF_1_L3 OrdRing_ZF_3_L10 by auto;
  with A2 show "a\<ls> b\<ra>\<one>" by (rule ring_strict_ord_transit);
qed;
  

text{*For any ring element $a$ the greater of $a$ and $1$ is a positive
  element that is greater or equal than $m$. If we add $1$ to it we
  get a positive element that is strictly greater than $m$. This holds
  in nontrivial rings.*}

lemma (in ring1) OrdRing_ZF_3_L12: assumes A1: "\<zero>≠\<one>" and A2: "a∈R"
  shows 
  "a \<lsq> GreaterOf(r,\<one>,a)"
  "GreaterOf(r,\<one>,a) ∈ R+"
  "GreaterOf(r,\<one>,a) \<ra> \<one> ∈ R+"
  "a \<lsq> GreaterOf(r,\<one>,a) \<ra> \<one>"  "a ≠ GreaterOf(r,\<one>,a) \<ra> \<one>"
proof -
  from linord have "r {is total on} R" using IsLinOrder_def
    by simp
  moreover from A2 have "\<one> ∈ R"  "a∈R"
    using Ring_ZF_1_L2 by auto
  ultimately have
    "\<one> \<lsq> GreaterOf(r,\<one>,a)" and
    I: "a \<lsq> GreaterOf(r,\<one>,a)"
    using Order_ZF_3_L2 by auto;
  with A1 show 
    "a \<lsq> GreaterOf(r,\<one>,a)" and 
    "GreaterOf(r,\<one>,a) ∈ R+"
    using OrdRing_ZF_3_L8 by auto;
  with A1 show "GreaterOf(r,\<one>,a) \<ra> \<one> ∈ R+"
    using ordring_one_is_pos OrdRing_ZF_3_L1 IsOpClosed_def
    by simp;
  from A1 I show 
    "a \<lsq> GreaterOf(r,\<one>,a) \<ra> \<one>"  "a ≠ GreaterOf(r,\<one>,a) \<ra> \<one>"
    using OrdRing_ZF_3_L11 by auto;
qed;

text{*We can multiply strict inequality by a positive element.*}

lemma (in ring1) OrdRing_ZF_3_L13: 
  assumes A1: "HasNoZeroDivs(R,A,M)" and 
  A2: "a\<ls>b" and A3: "c∈R+"
  shows 
  "a·c \<ls> b·c"
  "c·a \<ls> c·b"
proof -
  from A2 A3 have T: "a∈R"  "b∈R"  "c∈R"  "c≠\<zero>"
    using OrdRing_ZF_1_L3 PositiveSet_def by auto;
  from A2 A3 have "a·c \<lsq> b·c" using OrdRing_ZF_1_L9A
    by simp;
  moreover from A1 A2 T have "a·c ≠ b·c"
    using Ring_ZF_1_L12A by auto;
  ultimately show "a·c \<ls> b·c" by simp
  moreover from mult_commut T have "a·c = c·a" and "b·c = c·b"
    using IsCommutative_def by auto;
  ultimately show "c·a \<ls> c·b" by simp;
qed;

text{*A sufficient condition for an element to be in the set
  of positive ring elements. *}

lemma (in ring1) OrdRing_ZF_3_L14: assumes "\<zero>\<lsq>a" and "a≠\<zero>"
  shows "a ∈ R+"
  using prems OrdRing_ZF_1_L3 PositiveSet_def
  by auto;

text{*If a ring has no zero divisors, the square of a nonzero
  element is positive.*}

lemma (in ring1) OrdRing_ZF_3_L15: 
  assumes "HasNoZeroDivs(R,A,M)" and "a∈R"  "a≠\<zero>"
  shows "\<zero> \<lsq> a²"  "a² ≠ \<zero>"  "a² ∈ R+"
  using prems OrdRing_ZF_1_L10 Ring_ZF_1_L12 OrdRing_ZF_3_L14
  by auto;

text{*In rings with no zero divisors we can (strictly) increase a 
  positive element by  multiplying it by an element that is greater than $1$.*}

lemma (in ring1) OrdRing_ZF_3_L16: 
  assumes "HasNoZeroDivs(R,A,M)" and "a ∈ R+" and "\<one>\<lsq>b"  "\<one>≠b"
  shows "a\<lsq>a·b"  "a ≠ a·b"
  using prems PositiveSet_def OrdRing_ZF_1_L16 OrdRing_ZF_1_L3 
    Ring_ZF_1_L12C by auto;

text{*If the right hand side of an inequality is positive we can multiply it 
  by a number that is greater than one.*}

lemma (in ring1) OrdRing_ZF_3_L17: 
   assumes A1: "HasNoZeroDivs(R,A,M)" and A2: "b∈R+" and 
  A3: "a\<lsq>b"  and A4: "\<one>\<ls>c"
  shows "a\<ls>b·c"
proof -
  from A1 A2 A4 have "b \<ls> b·c"
    using OrdRing_ZF_3_L16 by auto;
  with A3 show "a\<ls>b·c" by (rule ring_strict_ord_transit);
qed;

text{*We can multiply a right hand side of an inequality between
  positive numbers by a number that is greater than one.*}

lemma (in ring1) OrdRing_ZF_3_L18: 
  assumes A1: "HasNoZeroDivs(R,A,M)" and A2: "a ∈ R+" and 
  A3: "a\<lsq>b" and A4: "\<one>\<ls>c"
  shows "a\<ls>b·c"
proof -
  from A2 A3 have "b ∈ R+" using OrdRing_ZF_3_L7
    by blast;
  with A1 A3 A4 show "a\<ls>b·c"
    using OrdRing_ZF_3_L17 by simp
qed;

text{*In ordered rings with no zero divisors if at 
  least one of $a,b$ is not zero, then
  $a^2+b^2 > 0$, in particular $a^2+b^2\neq 0$.*}

lemma (in ring1) OrdRing_ZF_3_L19: 
  assumes A1: "HasNoZeroDivs(R,A,M)" and A2: "a∈R"  "b∈R" and
  A3: "a ≠ \<zero> ∨ b ≠ \<zero>"
  shows "\<zero> \<ls> a² \<ra> b²"
proof -
  { assume "a ≠ \<zero>"
    with A1 A2 have "\<zero> \<lsq> a²"  "a² ≠ \<zero>"  
      using OrdRing_ZF_3_L15 by auto;
    then have "\<zero> \<ls> a²" by auto;
    moreover from A2 have "\<zero> \<lsq> b²"
      using OrdRing_ZF_1_L10 by simp
    ultimately have "\<zero> \<ra> \<zero> \<ls> a² \<ra> b²"
      using OrdRing_ZF_1_L19 by simp;
    hence "\<zero> \<ls> a² \<ra> b²"
      using Ring_ZF_1_L2 Ring_ZF_1_L3 by simp }
  moreover
  { assume A4: "a = \<zero>"
    then have "a² \<ra> b² = \<zero> \<ra> b²"
      using  Ring_ZF_1_L2 Ring_ZF_1_L6 by simp;
    also from A2 have "… = b²"
      using Ring_ZF_1_L4 Ring_ZF_1_L3 by simp
    finally have "a² \<ra> b² = b²" by simp;
    moreover 
    from A3 A4 have "b ≠ \<zero>" by simp;
    with A1 A2 have "\<zero> \<lsq> b²" and "b² ≠ \<zero>" 
      using OrdRing_ZF_3_L15 by auto;
    hence "\<zero> \<ls> b²" by auto;
    ultimately have "\<zero> \<ls> a² \<ra> b²" by simp }
  ultimately show "\<zero> \<ls> a² \<ra> b²"
    by auto;
qed;

    


end