Theory OrderedField_ZF
section ‹Ordered fields›
theory OrderedField_ZF imports OrderedRing_ZF Field_ZF
begin
text‹This theory covers basic facts about ordered fiels.›
subsection‹Definition and basic properties›
text‹Here we define ordered fields and proove their 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 ‹K› is the
carrier of the field. The second set, denoted ‹A› represents the
additive operation on ‹K› (recall that in ZF set theory functions
are sets). The third set ‹M› represents the multiplicative operation
on ‹K›. The fourth set ‹r› is the order
relation on ‹K›.›
definition
"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
‹ring1› context that is used for ordered 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 ‹ring1›
context to $K$, more appriopriate for fields. Theoretically the Isar locale
facility supports such renaming, but we experienced diffculties using
some lemmas from ‹ring1› locale after renaming.
›
locale field1 = ring1 +
assumes mult_commute: "M {is commutative on} R"
assumes not_triv: "𝟬 ≠ 𝟭"
assumes inv_exists: "∀a∈R. a≠𝟬 ⟶ (∃b∈R. a⋅b = 𝟭)"
fixes non_zero ("R⇩0")
defines non_zero_def[simp]: "R⇩0 ≡ R-{𝟬}"
fixes inv ("_¯ " [96] 97)
defines inv_def[simp]: "a¯ ≡ GroupInv(R⇩0,restrict(M,R⇩0×R⇩0))`(a)"
text‹The next lemma assures us that we are talking fields
in the ‹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 assms IsAnOrdField_def IsAnOrdRing_def IsAfield_def
by simp
text‹Theorems proven in ‹field0› (about fields) context are valid
in the ‹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_field0
by simp
text‹We can use theorems proven in the ‹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 assms 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 = 𝟭" and A2: "c∈R" "c≠𝟬"
shows "∃b∈R. c⋅b = 𝟭"
proof -
{ assume "c∈R⇩+"
with A1 have "∃b∈R. c⋅b = 𝟭" by simp }
moreover
{ 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 = 𝟭"
by auto
with A2 have "(\<rm>b) ∈ R" "c⋅(\<rm>b) = 𝟭"
using Ring_ZF_1_L3 Ring_ZF_1_L7 by auto
then have "∃b∈R. c⋅b = 𝟭" by auto }
ultimately show ?thesis by blast
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 "𝟬 ≠ 𝟭" and "M {is commutative on} R"
and "∀a∈R⇩+. ∃b∈R. a⋅b = 𝟭"
shows "IsAnOrdField(R,A,M,r)"
using assms 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: "𝟬 \<ls> a" "𝟬 \<ls> b"
shows "𝟬 \<ls> a⋅b"
proof -
from A1 have "a ∈ R⇩+" and "b ∈ R⇩+"
using OrdRing_ZF_3_L14 by auto
then show "𝟬 \<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≠𝟬"
shows "a⇧2 ∈ R⇩+"
using assms OrdField_ZF_1_L1B field0.field_has_no_zero_divs
OrdRing_ZF_3_L15 by simp
text‹The next lemma restates the fact ‹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≠𝟬"
shows "a⋅(a¯) = 𝟭" "(a¯)⋅a = 𝟭"
using assms 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≠𝟬" 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¯) = 𝟭" "(a¯)⋅a = 𝟭"
proof -
from A1 have I: "a∈R" "a≠𝟬" using PositiveSet_def
by auto
with A1 have "a⋅(a¯)⇧2 ∈ 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¯) = 𝟭" "(a¯)⋅a = 𝟭"
using OrdField_ZF_1_L7 by auto
qed
text‹If $a$ is smaller than $b$, then $(b-a)^{-1}$ is positive.›
lemma (in field1) OrdField_ZF_1_L9: assumes "a\<ls>b"
shows "(b\<rs>a)¯ ∈ R⇩+"
using assms 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 ≠ 𝟬 ∨ b ≠ 𝟬"
shows "𝟬 \<ls> a⇧2 \<ra> b⇧2" and "∃c∈R. (a⇧2 \<ra> b⇧2)⋅c = 𝟭"
proof -
from A1 A2 show "𝟬 \<ls> a⇧2 \<ra> b⇧2"
using OrdField_ZF_1_L1B field0.field_has_no_zero_divs
OrdRing_ZF_3_L19 by simp
then have
"(a⇧2 \<ra> b⇧2)¯ ∈ R" and "(a⇧2 \<ra> b⇧2)⋅(a⇧2 \<ra> b⇧2)¯ = 𝟭"
using OrdRing_ZF_1_L3 PositiveSet_def OrdField_ZF_1_L8
by auto
then show "∃c∈R. (a⇧2 \<ra> b⇧2)⋅c = 𝟭" by auto
qed
subsection‹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 assms OrdField_ZF_1_L1B field0.field_has_no_zero_divs
OrdRing_ZF_3_L13
by simp
text‹A special case of ‹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 "𝟭 \<ls> b⋅a"
proof -
from A1 A2 have "(a¯)⋅a \<ls> b⋅a"
using OrdField_ZF_2_L1 by simp
with A1 show "𝟭 \<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 assms 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 assms 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≠𝟬" "b∈R" "b≠𝟬"
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≠𝟬" 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 "𝟭 \<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≠𝟬" "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 "𝟭 \<ra> a⋅c \<ls> b⋅c"
using ring_oper_distr OrdField_ZF_1_L8
by simp
qed
subsection‹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.›
definition
"IsAmodelOfReals(K,A,M,r) ≡ IsAnOrdField(K,A,M,r) ∧ (r {is complete})"
end