Theory OrderedField_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{OrderedField\_ZF.thy}*}

theory OrderedField_ZF imports OrderedRing_ZF Field_ZF

begin

text{*This theory covers basic facts about ordered fiels.*}

section{*Definition and basic properties*}

text{*Ordered field is a notrivial ordered ring such that all 
  non-zero elements have an inverse. We define the notion of being a ordered 
  field as
  a statement about four sets. The first set, denoted @{text "K"} is the 
  carrier of the field. The second set, denoted @{text "A"} represents the 
  additive operation on @{text "K"} (recall that in ZF set theory functions 
  are sets). The third set @{text "M"} represents the multiplicative operation 
  on @{text "K"}. The fourth set @{text "r"} is the order 
  relation on @{text "K"}.*}

constdefs
  "IsAnOrdField(K,A,M,r) ≡ (IsAnOrdRing(K,A,M,r) ∧
  (M {is commutative on} K) ∧
  TheNeutralElement(K,A) ≠ TheNeutralElement(K,M) ∧
  (∀a∈K. a≠TheNeutralElement(K,A)-->
  (∃b∈K. M`⟨a,b⟩ = TheNeutralElement(K,M))))"

text{*The next context (locale) defines notation used for ordered fields. 
  We do that by extending the notation defined in the 
  @{text "ring1"} context that is used for oredered rings and 
  adding some assumptions to make sure we are 
  talking about ordered fields in this context. 
  We should rename the carrier from $R$ used in the @{text "ring1"} 
  context to $K$, more appriopriate for fields. Theoretically the Isar locale
  facility supports such renaming, but we experienced diffculties using
  some lemmas from @{text "ring1"} locale after renaming. 
  *}

locale field1 = ring1 +

  assumes mult_commute: "M {is commutative on} R"
  
  assumes not_triv: "\<zero> ≠ \<one>"

  assumes inv_exists: "∀a∈R. a≠\<zero> --> (∃b∈R. a·b = \<one>)"

  fixes non_zero ("R0")
  defines non_zero_def[simp]: "R0 ≡ R-{\<zero>}"

  fixes inv ("_¯ " [96] 97)
  defines inv_def[simp]: "a¯ ≡ GroupInv(R0,restrict(M,R0×R0))`(a)"

text{*The next lemma assures us that we are talking fields 
  in the @{text "field1"} context.*}

lemma (in field1) OrdField_ZF_1_L1: shows "IsAnOrdField(R,A,M,r)"
  using OrdRing_ZF_1_L1 mult_commute not_triv inv_exists IsAnOrdField_def
  by simp;

text{*Ordered field is a field, of course.*}

lemma OrdField_ZF_1_L1A: assumes "IsAnOrdField(K,A,M,r)"
  shows "IsAfield(K,A,M)"
  using prems IsAnOrdField_def IsAnOrdRing_def IsAfield_def
  by simp;

text{*Theorems proven in @{text "field0"} (about fields) context are valid
  in the @{text "field1"} context (about ordered fields). *}

lemma (in field1) OrdField_ZF_1_L1B: shows "field0(R,A,M)"
  using  OrdField_ZF_1_L1 OrdField_ZF_1_L1A Field_ZF_1_L2 
  by simp;

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

lemma OrdField_ZF_1_L2: assumes "IsAnOrdField(K,A,M,r)"
  shows "field1(K,A,M,r)"
  using prems IsAnOrdField_def OrdRing_ZF_1_L2 ring1_def
    IsAnOrdField_def field1_axioms_def field1_def
  by auto;

text{*In ordered rings the existence of a right inverse for all positive
  elements implies the existence of an inverse for all non zero elements.*}

lemma (in ring1) OrdField_ZF_1_L3: 
  assumes A1: "∀a∈R+. ∃b∈R. a·b = \<one>" and A2: "c∈R"  "c≠\<zero>"
  shows "∃b∈R. c·b = \<one>"
proof (cases "c∈R+");
  assume "c∈R+"
  with A1 show "∃b∈R. c·b = \<one>" by simp;
next assume "c∉R+"
  with A2 have "(\<rm>c) ∈ R+"
    using OrdRing_ZF_3_L2A by simp;
  with A1 obtain b where "b∈R" and "(\<rm>c)·b = \<one>"
    by auto;
  with A2 have "(\<rm>b) ∈ R"  "c·(\<rm>b) = \<one>"
    using Ring_ZF_1_L3 Ring_ZF_1_L7 by auto;
  then show "∃b∈R. c·b = \<one>" by auto;
qed;
  
text{*Ordered fields are easier to deal with, because it is sufficient 
  to show the existence of an inverse for the set of positive elements.*}

lemma (in ring1) OrdField_ZF_1_L4: 
  assumes "\<zero> ≠ \<one>" and "M {is commutative on} R" 
  and "∀a∈R+. ∃b∈R. a·b = \<one>"
  shows "IsAnOrdField(R,A,M,r)"
  using prems OrdRing_ZF_1_L1 OrdField_ZF_1_L3 IsAnOrdField_def
  by simp;

text{*The set of positive field elements is closed under multiplication.*}

lemma (in field1) OrdField_ZF_1_L5: shows "R+ {is closed under} M"
  using OrdField_ZF_1_L1B field0.field_has_no_zero_divs OrdRing_ZF_3_L3
  by simp;

text{*The set of positive field elements is closed under multiplication:
  the explicit version.*}

lemma (in field1) pos_mul_closed: 
  assumes A1: "\<zero> \<ls> a"  "\<zero> \<ls> b"
  shows "\<zero> \<ls> a·b"
proof -
  from A1 have "a ∈ R+" and  "b ∈ R+"
    using OrdRing_ZF_3_L14 by auto;
  then show "\<zero> \<ls> a·b" 
    using OrdField_ZF_1_L5 IsOpClosed_def PositiveSet_def
    by simp;
qed;


text{*In fields square of a nonzero element is positive. *}

lemma (in field1) OrdField_ZF_1_L6: assumes "a∈R"  "a≠\<zero>"
  shows "a² ∈ R+"
  using prems OrdField_ZF_1_L1B field0.field_has_no_zero_divs
    OrdRing_ZF_3_L15 by simp;

text{*The next lemma restates the fact @{text "Field_ZF"} that out notation
  for the field inverse means what it is supposed to mean.*}

lemma (in field1) OrdField_ZF_1_L7: assumes "a∈R"  "a≠\<zero>"
  shows "a·(a¯) = \<one>"  "(a¯)·a = \<one>"
  using prems OrdField_ZF_1_L1B field0.Field_ZF_1_L6
  by auto;

text{*A simple lemma about multiplication and cancelling of a positive field
   element.*}

lemma (in field1) OrdField_ZF_1_L7A: 
  assumes A1: "a∈R"  "b ∈ R+"
  shows 
  "a·b·b¯ = a"
  "a·b¯·b = a"
proof -
  from A1 have "b∈R"  "b≠\<zero>" using PositiveSet_def
    by auto
  with A1 show  "a·b·b¯ = a" and "a·b¯·b = a"
    using OrdField_ZF_1_L1B field0.Field_ZF_1_L7
    by auto;
qed;
    
text{*Some properties of the inverse of a positive element.*}

lemma (in field1) OrdField_ZF_1_L8: assumes A1: "a ∈ R+"
  shows "a¯ ∈ R+"  "a·(a¯) = \<one>"  "(a¯)·a = \<one>"
proof -
  from A1 have I: "a∈R"  "a≠\<zero>" using PositiveSet_def 
    by auto;
  with A1 have "a·(a¯)² ∈ R+" 
    using OrdField_ZF_1_L1B field0.Field_ZF_1_L5 OrdField_ZF_1_L6
      OrdField_ZF_1_L5 IsOpClosed_def by simp;
  with I show "a¯ ∈ R+"
    using OrdField_ZF_1_L1B field0.Field_ZF_2_L1
    by simp;
  from I show  "a·(a¯) = \<one>"  "(a¯)·a = \<one>"
    using OrdField_ZF_1_L7 by auto
qed;

text{*If $a<b$, then $(b-a)^{-1}$ is positive.*}

lemma (in field1) OrdField_ZF_1_L9: assumes "a\<ls>b"
  shows  "(b\<rs>a)¯ ∈ R+"  
  using prems OrdRing_ZF_1_L14 OrdField_ZF_1_L8
  by simp;

text{*In ordered fields if at least one of $a,b$ is not zero, then
  $a^2+b^2 > 0$, in particular $a^2+b^2\neq 0$ and exists the 
  (multiplicative) inverse of $a^2+b^2$. *}

lemma (in field1) OrdField_ZF_1_L10: 
  assumes A1: "a∈R"  "b∈R" and A2: "a ≠ \<zero> ∨ b ≠ \<zero>"
  shows "\<zero> \<ls> a² \<ra> b²"  and "∃c∈R. (a² \<ra> b²)·c = \<one>"
proof -
  from A1 A2 show "\<zero> \<ls> a² \<ra> b²"
    using OrdField_ZF_1_L1B field0.field_has_no_zero_divs 
      OrdRing_ZF_3_L19 by simp;
  then have 
    "(a² \<ra> b²)¯ ∈ R" and "(a² \<ra> b²)·(a² \<ra> b²)¯ = \<one>"
    using OrdRing_ZF_1_L3 PositiveSet_def OrdField_ZF_1_L8
    by auto;
  then show "∃c∈R. (a² \<ra> b²)·c = \<one>" by auto;
qed;
  
section{*Inequalities*}

text{*In this section we develop tools to deal inequalities in fields.*}

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

lemma (in field1) OrdField_ZF_2_L1: 
  assumes "a\<ls>b" and "c∈R+"
  shows "a·c \<ls> b·c"
  using prems OrdField_ZF_1_L1B field0.field_has_no_zero_divs
    OrdRing_ZF_3_L13
  by simp;

text{*A special case of @{text "OrdField_ZF_2_L1"} when we multiply
  an inverse by an element.*}

lemma (in field1) OrdField_ZF_2_L2: 
  assumes A1: "a∈R+" and A2: "a¯ \<ls> b"
  shows "\<one> \<ls> b·a"
proof -
  from A1 A2 have "(a¯)·a \<ls> b·a"
    using OrdField_ZF_2_L1 by simp;
  with A1 show "\<one> \<ls> b·a"
    using OrdField_ZF_1_L8 by simp
qed;

text{*We can multiply an inequality by the inverse of a positive element.*}

lemma (in field1) OrdField_ZF_2_L3:
  assumes "a\<lsq>b"  and "c∈R+" shows "a·(c¯) \<lsq> b·(c¯)"
  using prems OrdField_ZF_1_L8 OrdRing_ZF_1_L9A
  by simp;

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

lemma (in field1) OrdField_ZF_2_L4:
  assumes "a\<ls>b" and "c∈R+"
  shows 
  "a·c \<ls> b·c"
  "c·a \<ls> c·b"
  "a·c¯ \<ls> b·c¯"
   using prems OrdField_ZF_1_L1B field0.field_has_no_zero_divs
    OrdField_ZF_1_L8 OrdRing_ZF_3_L13 by auto;

text{*We can put a positive factor on the other side of an inequality,
  changing it to its inverse.*}

lemma (in field1) OrdField_ZF_2_L5:
  assumes A1: "a∈R"  "b∈R+" and A2: "a·b \<lsq> c"
  shows "a \<lsq> c·b¯"
proof -
  from A1 A2 have "a·b·b¯ \<lsq> c·b¯"
    using OrdField_ZF_2_L3 by simp;
  with A1 show "a \<lsq> c·b¯" using OrdField_ZF_1_L7A
    by simp;
qed;

text{*We can put a positive factor on the other side of an inequality,
  changing it to its inverse, version with a product initially on the 
  right hand side.*}

lemma (in field1) OrdField_ZF_2_L5A:
  assumes A1: "b∈R"  "c∈R+" and A2: "a \<lsq> b·c"
  shows "a·c¯ \<lsq> b"
proof -
  from A1 A2 have "a·c¯ \<lsq> b·c·c¯"
    using OrdField_ZF_2_L3 by simp
  with A1 show "a·c¯ \<lsq> b" using OrdField_ZF_1_L7A
    by simp
qed;

text{*We can put a positive factor on the other side of a strict
  inequality, changing it to its inverse, version with a product
  initially on the left hand side.*}

lemma (in field1) OrdField_ZF_2_L6:
  assumes A1: "a∈R"  "b∈R+" and A2: "a·b \<ls> c"
  shows "a \<ls> c·b¯"
proof -
  from A1 A2 have "a·b·b¯ \<ls> c·b¯"
    using OrdField_ZF_2_L4 by simp
  with A1 show "a \<ls> c·b¯" using OrdField_ZF_1_L7A
    by simp;
qed;

text{*We can put a positive factor on the other side of a strict
  inequality, changing it to its inverse, version with a product
  initially on the right hand side.*}

lemma (in field1) OrdField_ZF_2_L6A:
  assumes A1: "b∈R"  "c∈R+" and A2: "a \<ls> b·c"
  shows "a·c¯ \<ls> b"
proof -
  from A1 A2 have "a·c¯ \<ls> b·c·c¯"
    using OrdField_ZF_2_L4 by simp
  with A1 show "a·c¯ \<ls> b" using OrdField_ZF_1_L7A
    by simp
qed;

text{*Sometimes we can reverse an inequality by taking inverse
  on both sides.*}

lemma (in field1) OrdField_ZF_2_L7: 
  assumes A1: "a∈R+" and A2: "a¯ \<lsq> b"
  shows "b¯ \<lsq> a"
proof -
  from A1 have "a¯ ∈ R+" using OrdField_ZF_1_L8
    by simp;
  with A2 have "b ∈ R+" using  OrdRing_ZF_3_L7
    by blast;
  then have T: "b ∈ R+"  "b¯ ∈ R+" using OrdField_ZF_1_L8
    by auto
  with A1 A2 have "b¯·a¯·a \<lsq> b¯·b·a"
    using OrdRing_ZF_1_L9A by simp;
  moreover 
  from A1 A2 T have
    "b¯ ∈ R"  "a∈R" "a≠\<zero>"  "b∈R"  "b≠\<zero>"
    using PositiveSet_def OrdRing_ZF_1_L3 by auto;
  then have "b¯·a¯·a = b¯" and  "b¯·b·a = a"
    using OrdField_ZF_1_L1B field0.Field_ZF_1_L7 
      field0.Field_ZF_1_L6 Ring_ZF_1_L3
    by auto;
  ultimately show "b¯ \<lsq> a" by simp;
qed;

text{*Sometimes we can reverse a strict inequality by taking inverse
  on both sides.*}

lemma (in field1) OrdField_ZF_2_L8: 
  assumes A1: "a∈R+" and A2: "a¯ \<ls> b"
  shows "b¯ \<ls> a"
proof -
  from A1 A2 have "a¯ ∈ R+"  "a¯ \<lsq>b"
    using OrdField_ZF_1_L8 by auto;
  then have "b ∈ R+" using OrdRing_ZF_3_L7
    by blast;
  then have "b∈R"  "b≠\<zero>" using PositiveSet_def by auto;
  with A2 have "b¯ ≠ a"
    using OrdField_ZF_1_L1B field0.Field_ZF_2_L4
    by simp;
  with A1 A2 show "b¯ \<ls> a"
    using OrdField_ZF_2_L7 by simp;
qed;
    
text{*A technical lemma about solving a strict inequality with three
  field elements and inverse of a difference.*}

lemma (in field1) OrdField_ZF_2_L9: 
  assumes A1: "a\<ls>b" and A2: "(b\<rs>a)¯ \<ls> c"
  shows "\<one> \<ra> a·c \<ls> b·c"
proof -
  from A1 A2 have "(b\<rs>a)¯ ∈ R+"  "(b\<rs>a)¯ \<lsq> c" 
    using OrdField_ZF_1_L9 by auto;
  then have T1: "c ∈ R+" using OrdRing_ZF_3_L7 by blast;
  with A1 A2 have T2: 
    "a∈R"  "b∈R"  "c∈R"  "c≠\<zero>"   "c¯ ∈ R"
    using OrdRing_ZF_1_L3 OrdField_ZF_1_L8 PositiveSet_def 
    by auto;
  with A1 A2  have "c¯ \<ra> a \<ls> b\<rs>a \<ra> a"
    using OrdRing_ZF_1_L14 OrdField_ZF_2_L8 ring_strict_ord_trans_inv
    by simp;
  with T1 T2 have "(c¯ \<ra> a)·c \<ls> b·c"
    using Ring_ZF_2_L1A OrdField_ZF_2_L1 by simp;
  with T1 T2 show "\<one> \<ra> a·c \<ls> b·c"
    using ring_oper_distr OrdField_ZF_1_L8
    by simp;
qed;

section{*Definition of real numbers*}

text{*The only purpose of this section is to define what does it mean
  to be a model of real numbers.*}

text{*We define model of real numbers as any quadruple (?) of sets $(K,A,M,r)$ 
  such that $(K,A,M,r)$ is an ordered field and the order relation $r$
  is complete, that is every set that is nonempty and bounded above in this 
  relation has a supremum. *}

constdefs
  "IsAmodelOfReals(K,A,M,r) ≡ IsAnOrdField(K,A,M,r) ∧ (r {is complete})";


  
end