Theory Real_ZF
section ‹Construction real numbers - the generic part›
theory Real_ZF imports Int_ZF_IML Ring_ZF_1
begin
text‹The goal of the ‹Real_ZF› series of theory files is
to provide a contruction of the set of
real numbers. There are several ways to construct real numbers.
Most common start from the rational numbers and use Dedekind cuts
or Cauchy sequences. ‹Real_ZF_x.thy› series formalizes
an alternative
approach that constructs real numbers directly from the group of integers.
Our formalization is mostly based on \cite{Arthan2004}.
Different variants of this contruction are also
described in \cite{Campo2003} and \cite{Street2003}.
I recommend to read these papers, but for the impatient here is a short
description: we take a set of maps $s : Z\rightarrow Z$ such that
the set $\{s(m+n)-s(m)-s(n)\}_{n,m \in Z}$ is finite
($Z$ means the integers here). We call these maps slopes.
Slopes form a group with the natural addition
$(s+r)(n) = s(n)+r(n)$. The maps such that the set $s(Z)$ is finite
(finite range functions) form a subgroup of slopes.
The additive group of real numbers is defined as the
quotient group of slopes by the (sub)group of finite range functions.
The multiplication is defined as the projection of the composition of slopes
into the resulting quotient (coset) space.
›
subsection‹The definition of real numbers›
text‹This section contains the construction of the ring of real numbers
as classes of slopes - integer almost homomorphisms. The real definitions
are in ‹Group_ZF_2› theory, here we just specialize the definitions
of almost homomorphisms, their equivalence and operations to the
additive group of integers from the general case of abelian groups considered
in ‹Group_ZF_2›.›
text‹The set of slopes is defined as the set of almost homomorphisms
on the additive group of integers.›
definition
"Slopes ≡ AlmostHoms(int,IntegerAddition)"
text‹The first operation on slopes (pointwise addition) is a special case
of the first operation on almost homomorphisms.›
definition
"SlopeOp1 ≡ AlHomOp1(int,IntegerAddition)"
text‹The second operation on slopes (composition) is a special case
of the second operation on almost homomorphisms.›
definition
"SlopeOp2 ≡ AlHomOp2(int,IntegerAddition)"
text‹Bounded integer maps are functions from integers
to integers that have finite range. They play a role of
zero in the set of real numbers we are constructing.›
definition
"BoundedIntMaps ≡ FinRangeFunctions(int,int)"
text‹Bounded integer maps form a normal subgroup of slopes.
The equivalence relation on slopes is the (group) quotient
relation defined by this subgroup.
›
definition
"SlopeEquivalenceRel ≡ QuotientGroupRel(Slopes,SlopeOp1,BoundedIntMaps)"
text‹The set of real numbers is the set of equivalence classes of
slopes.›
definition
"RealNumbers ≡ Slopes//SlopeEquivalenceRel"
text‹The addition on real numbers is defined as the projection of
pointwise addition of slopes on the quotient. This means that
the additive group of real numbers is the quotient group:
the group of slopes (with pointwise addition) defined by the
normal subgroup of bounded integer maps.›
definition
"RealAddition ≡ ProjFun2(Slopes,SlopeEquivalenceRel,SlopeOp1)"
text‹Multiplication is defined as the projection of composition
of slopes on the quotient. The fact that it works is probably the
most surprising part of the construction.›
definition
"RealMultiplication ≡ ProjFun2(Slopes,SlopeEquivalenceRel,SlopeOp2)"
text‹We first show that we can use theorems proven in some proof contexts
(locales). The locale ‹group1› requires assumption that we deal with
an abelian group. The next lemma allows to use all theorems proven
in the context called ‹group1›.›
lemma Real_ZF_1_L1: shows "group1(int,IntegerAddition)"
using group1_axioms.intro group1_def Int_ZF_1_T2 by simp
text‹Real numbers form a ring. This is a special case of the theorem
proven in ‹Ring_ZF_1.thy›, where we show the same in general for
almost homomorphisms rather than slopes.›
theorem Real_ZF_1_T1: shows "IsAring(RealNumbers,RealAddition,RealMultiplication)"
proof -
let ?AH = "AlmostHoms(int,IntegerAddition)"
let ?Op1 = "AlHomOp1(int,IntegerAddition)"
let ?FR = "FinRangeFunctions(int,int)"
let ?Op2 = "AlHomOp2(int,IntegerAddition)"
let ?R = "QuotientGroupRel(?AH,?Op1,?FR)"
let ?A = "ProjFun2(?AH,?R,?Op1)"
let ?M = "ProjFun2(?AH,?R,?Op2)"
have "IsAring(?AH//?R,?A,?M)" using Real_ZF_1_L1 group1.Ring_ZF_1_1_T1
by simp
then show ?thesis using Slopes_def SlopeOp2_def SlopeOp1_def
BoundedIntMaps_def SlopeEquivalenceRel_def RealNumbers_def
RealAddition_def RealMultiplication_def by simp
qed
text‹We can use theorems proven in ‹group0› and ‹group1›
contexts applied to the group of real numbers.›
lemma Real_ZF_1_L2: shows
"group0(RealNumbers,RealAddition)"
"RealAddition {is commutative on} RealNumbers"
"group1(RealNumbers,RealAddition)"
proof -
have
"IsAgroup(RealNumbers,RealAddition)"
"RealAddition {is commutative on} RealNumbers"
using Real_ZF_1_T1 IsAring_def by auto
then show
"group0(RealNumbers,RealAddition)"
"RealAddition {is commutative on} RealNumbers"
"group1(RealNumbers,RealAddition)"
using group1_axioms.intro group0_def group1_def
by auto
qed
text‹Let's define some notation.›
locale real0 =
fixes real ("ℝ")
defines real_def [simp]: "ℝ ≡ RealNumbers"
fixes ra (infixl "\<ra>" 69)
defines ra_def [simp]: "a\<ra> b ≡ RealAddition`⟨a,b⟩"
fixes rminus ("\<rm> _" 72)
defines rminus_def [simp]:"\<rm>a ≡ GroupInv(ℝ,RealAddition)`(a)"
fixes rsub (infixl "\<rs>" 69)
defines rsub_def [simp]: "a\<rs>b ≡ a\<ra>(\<rm>b)"
fixes rm (infixl "⋅" 70)
defines rm_def [simp]: "a⋅b ≡ RealMultiplication`⟨a,b⟩"
fixes rzero ("𝟬")
defines rzero_def [simp]:
"𝟬 ≡ TheNeutralElement(RealNumbers,RealAddition)"
fixes rone ("𝟭")
defines rone_def [simp]:
"𝟭 ≡ TheNeutralElement(RealNumbers,RealMultiplication)"
fixes rtwo ("𝟮")
defines rtwo_def [simp]: "𝟮 ≡ 𝟭\<ra>𝟭"
fixes non_zero ("ℝ⇩0")
defines non_zero_def[simp]: "ℝ⇩0 ≡ ℝ-{𝟬}"
fixes inv ("_¯ " [90] 91)
defines inv_def[simp]:
"a¯ ≡ GroupInv(ℝ⇩0,restrict(RealMultiplication,ℝ⇩0×ℝ⇩0))`(a)"
text‹In ‹real0› context all theorems proven in the ‹ring0›,
context are valid.›
lemma (in real0) Real_ZF_1_L3: shows
"ring0(ℝ,RealAddition,RealMultiplication)"
using Real_ZF_1_T1 ring0_def ring0.Ring_ZF_1_L1
by auto
text‹Lets try out our notation to see that zero and one are real numbers.›
lemma (in real0) Real_ZF_1_L4: shows "𝟬∈ℝ" "𝟭∈ℝ"
using Real_ZF_1_L3 ring0.Ring_ZF_1_L2 by auto
text‹The lemma below lists some properties that
require one real number to state.›
lemma (in real0) Real_ZF_1_L5: assumes A1: "a∈ℝ"
shows
"(\<rm>a) ∈ ℝ"
"(\<rm>(\<rm>a)) = a"
"a\<ra>𝟬 = a"
"𝟬\<ra>a = a"
"a⋅𝟭 = a"
"𝟭⋅a = a"
"a\<rs>a = 𝟬"
"a\<rs>𝟬 = a"
using assms Real_ZF_1_L3 ring0.Ring_ZF_1_L3 by auto
text‹The lemma below lists some properties that
require two real numbers to state.›
lemma (in real0) Real_ZF_1_L6: assumes "a∈ℝ" "b∈ℝ"
shows
"a\<ra>b ∈ ℝ"
"a\<rs>b ∈ ℝ"
"a⋅b ∈ ℝ"
"a\<ra>b = b\<ra>a"
"(\<rm>a)⋅b = \<rm>(a⋅b)"
"a⋅(\<rm>b) = \<rm>(a⋅b)"
using assms Real_ZF_1_L3 ring0.Ring_ZF_1_L4 ring0.Ring_ZF_1_L7
by auto
text‹Multiplication of reals is associative.›
lemma (in real0) Real_ZF_1_L6A: assumes "a∈ℝ" "b∈ℝ" "c∈ℝ"
shows "a⋅(b⋅c) = (a⋅b)⋅c"
using assms Real_ZF_1_L3 ring0.Ring_ZF_1_L11
by simp
text‹Addition is distributive with respect to multiplication.›
lemma (in real0) Real_ZF_1_L7: assumes "a∈ℝ" "b∈ℝ" "c∈ℝ"
shows
"a⋅(b\<ra>c) = a⋅b \<ra> a⋅c"
"(b\<ra>c)⋅a = b⋅a \<ra> c⋅a"
"a⋅(b\<rs>c) = a⋅b \<rs> a⋅c"
"(b\<rs>c)⋅a = b⋅a \<rs> c⋅a"
using assms Real_ZF_1_L3 ring0.ring_oper_distr ring0.Ring_ZF_1_L8
by auto
text‹A simple rearrangement with four real numbers.›
lemma (in real0) Real_ZF_1_L7A:
assumes "a∈ℝ" "b∈ℝ" "c∈ℝ" "d∈ℝ"
shows "a\<rs>b \<ra> (c\<rs>d) = a\<ra>c\<rs>b\<rs>d"
using assms Real_ZF_1_L2 group0.group0_4_L8A by simp
text‹‹RealAddition› is defined as the projection of the
first operation on slopes (that is, slope addition) on the quotient
(slopes divided by the "almost equal" relation. The next lemma plays with
definitions to show that this is the same as the operation induced on the
appriopriate quotient group. The names ‹AH›, ‹Op1›
and ‹FR› are used in ‹group1› context to denote almost
homomorphisms, the first operation on ‹AH› and finite range
functions resp.›
lemma Real_ZF_1_L8: assumes
"AH = AlmostHoms(int,IntegerAddition)" and
"Op1 = AlHomOp1(int,IntegerAddition)" and
"FR = FinRangeFunctions(int,int)"
shows "RealAddition = QuotientGroupOp(AH,Op1,FR)"
using assms RealAddition_def SlopeEquivalenceRel_def
QuotientGroupOp_def Slopes_def SlopeOp1_def BoundedIntMaps_def
by simp
text‹The symbol ‹𝟬› in the ‹real0› context is defined
as the neutral element of real addition. The next lemma shows that this
is the same as the neutral element of the appriopriate quotient group.›
lemma (in real0) Real_ZF_1_L9: assumes
"AH = AlmostHoms(int,IntegerAddition)" and
"Op1 = AlHomOp1(int,IntegerAddition)" and
"FR = FinRangeFunctions(int,int)" and
"r = QuotientGroupRel(AH,Op1,FR)"
shows
"TheNeutralElement(AH//r,QuotientGroupOp(AH,Op1,FR)) = 𝟬"
"SlopeEquivalenceRel = r"
using assms Slopes_def Real_ZF_1_L8 RealNumbers_def
SlopeEquivalenceRel_def SlopeOp1_def BoundedIntMaps_def
by auto
text‹Zero is the class of any finite range function.›
lemma (in real0) Real_ZF_1_L10:
assumes A1: "s ∈ Slopes"
shows "SlopeEquivalenceRel``{s} = 𝟬 ⟷ s ∈ BoundedIntMaps"
proof -
let ?AH = "AlmostHoms(int,IntegerAddition)"
let ?Op1 = "AlHomOp1(int,IntegerAddition)"
let ?FR = "FinRangeFunctions(int,int)"
let ?r = "QuotientGroupRel(?AH,?Op1,?FR)"
let ?e = "TheNeutralElement(?AH//?r,QuotientGroupOp(?AH,?Op1,?FR))"
from A1 have
"group1(int,IntegerAddition)"
"s∈?AH"
using Real_ZF_1_L1 Slopes_def
by auto
then have "?r``{s} = ?e ⟷ s ∈ ?FR"
using group1.Group_ZF_3_3_L5 by simp
moreover have
"?r = SlopeEquivalenceRel"
"?e = 𝟬"
"?FR = BoundedIntMaps"
using SlopeEquivalenceRel_def Slopes_def SlopeOp1_def
BoundedIntMaps_def Real_ZF_1_L9 by auto
ultimately show ?thesis by simp
qed
text‹We will need a couple of results from ‹Group_ZF_3.thy›
The first two that state that the definition
of addition and multiplication of real numbers are consistent,
that is the result
does not depend on the choice of the slopes representing the numbers.
The second one implies that what we call ‹SlopeEquivalenceRel›
is actually an equivalence relation on the set of slopes.
We also show that the neutral element of the multiplicative operation on
reals (in short number $1$) is the class of the identity function on
integers.›
lemma Real_ZF_1_L11: shows
"Congruent2(SlopeEquivalenceRel,SlopeOp1)"
"Congruent2(SlopeEquivalenceRel,SlopeOp2)"
"SlopeEquivalenceRel ⊆ Slopes × Slopes"
"equiv(Slopes, SlopeEquivalenceRel)"
"SlopeEquivalenceRel``{id(int)} =
TheNeutralElement(RealNumbers,RealMultiplication)"
"BoundedIntMaps ⊆ Slopes"
proof -
let ?G = "int"
let ?f = "IntegerAddition"
let ?AH = "AlmostHoms(int,IntegerAddition)"
let ?Op1 = "AlHomOp1(int,IntegerAddition)"
let ?Op2 = "AlHomOp2(int,IntegerAddition)"
let ?FR = "FinRangeFunctions(int,int)"
let ?R = "QuotientGroupRel(?AH,?Op1,?FR)"
have
"Congruent2(?R,?Op1)"
"Congruent2(?R,?Op2)"
using Real_ZF_1_L1 group1.Group_ZF_3_4_L13A group1.Group_ZF_3_3_L4
by auto
then show
"Congruent2(SlopeEquivalenceRel,SlopeOp1)"
"Congruent2(SlopeEquivalenceRel,SlopeOp2)"
using SlopeEquivalenceRel_def SlopeOp1_def Slopes_def
BoundedIntMaps_def SlopeOp2_def by auto
have "equiv(?AH,?R)"
using Real_ZF_1_L1 group1.Group_ZF_3_3_L3 by simp
then show "equiv(Slopes,SlopeEquivalenceRel)"
using BoundedIntMaps_def SlopeEquivalenceRel_def SlopeOp1_def Slopes_def
by simp
then show "SlopeEquivalenceRel ⊆ Slopes × Slopes"
using equiv_type by simp
have "?R``{id(int)} = TheNeutralElement(?AH//?R,ProjFun2(?AH,?R,?Op2))"
using Real_ZF_1_L1 group1.Group_ZF_3_4_T2 by simp
then show "SlopeEquivalenceRel``{id(int)} =
TheNeutralElement(RealNumbers,RealMultiplication)"
using Slopes_def RealNumbers_def
SlopeEquivalenceRel_def SlopeOp1_def BoundedIntMaps_def
RealMultiplication_def SlopeOp2_def
by simp
have "?FR ⊆ ?AH" using Real_ZF_1_L1 group1.Group_ZF_3_3_L1
by simp
then show "BoundedIntMaps ⊆ Slopes"
using BoundedIntMaps_def Slopes_def by simp
qed
text‹A one-side implication of the equivalence from ‹Real_ZF_1_L10›:
the class of a bounded integer map is the real zero.›
lemma (in real0) Real_ZF_1_L11A: assumes "s ∈ BoundedIntMaps"
shows "SlopeEquivalenceRel``{s} = 𝟬"
using assms Real_ZF_1_L11 Real_ZF_1_L10 by auto
text‹The next lemma is rephrases the result from ‹Group_ZF_3.thy›
that says that the negative (the group inverse with respect to real
addition) of the class of a slope is the class of that slope
composed with the integer additive group inverse. The result and proof is not
very readable as we use mostly generic set theory notation with long names
here. ‹Real_ZF_1.thy› contains the same statement written in a more
readable notation: $[-s] = -[s]$.›
lemma (in real0) Real_ZF_1_L12: assumes A1: "s ∈ Slopes" and
Dr: "r = QuotientGroupRel(Slopes,SlopeOp1,BoundedIntMaps)"
shows "r``{GroupInv(int,IntegerAddition) O s} = \<rm>(r``{s})"
proof -
let ?G = "int"
let ?f = "IntegerAddition"
let ?AH = "AlmostHoms(int,IntegerAddition)"
let ?Op1 = "AlHomOp1(int,IntegerAddition)"
let ?FR = "FinRangeFunctions(int,int)"
let ?F = "ProjFun2(Slopes,r,SlopeOp1)"
from A1 Dr have
"group1(?G, ?f)"
"s ∈ AlmostHoms(?G, ?f)"
"r = QuotientGroupRel(
AlmostHoms(?G, ?f), AlHomOp1(?G, ?f), FinRangeFunctions(?G, ?G))"
and "?F = ProjFun2(AlmostHoms(?G, ?f), r, AlHomOp1(?G, ?f))"
using Real_ZF_1_L1 Slopes_def SlopeOp1_def BoundedIntMaps_def
by auto
then have
"r``{GroupInv(?G, ?f) O s} =
GroupInv(AlmostHoms(?G, ?f) // r, ?F)`(r `` {s})"
using group1.Group_ZF_3_3_L6 by simp
with Dr show ?thesis
using RealNumbers_def Slopes_def SlopeEquivalenceRel_def RealAddition_def
by simp
qed
text‹Two classes are equal iff the slopes that represent them
are almost equal.›
lemma Real_ZF_1_L13: assumes "s ∈ Slopes" "p ∈ Slopes"
and "r = SlopeEquivalenceRel"
shows "r``{s} = r``{p} ⟷ ⟨s,p⟩ ∈ r"
using assms Real_ZF_1_L11 eq_equiv_class equiv_class_eq
by blast
text‹Identity function on integers is a slope.
This lemma concludes the easy part of the construction that follows from
the fact that slope equivalence classes form a ring. It is easy to see
that multiplication of classes of almost homomorphisms is not
commutative in general.
The remaining properties of real numbers, like commutativity of
multiplication and the existence of multiplicative inverses have to be
proven using properties of the group of integers, rather that in general
setting of abelian groups. This is done in the ‹Real_ZF_1› theory.›
lemma Real_ZF_1_L14: shows "id(int) ∈ Slopes"
proof -
have "id(int) ∈ AlmostHoms(int,IntegerAddition)"
using Real_ZF_1_L1 group1.Group_ZF_3_4_L15
by simp
then show ?thesis using Slopes_def by simp
qed
end