Isabelle/ZF and IsarMathLib do not have a set of real numbers built-in. The Real_ZF and Real_ZF_1 theories provide a construction but here we do not use it in any way and we just assume that we have a model of real numbers (i.e. a completely ordered field) as defined in the Ordered_Field theory. The construction only assures us that objects with the desired properties exist in the ZF world.
In this section we define notation that we will use whenever real numbers play a role, i.e. most of mathematics.
The next locale sets up notation for contexts where real numbers are used.
Locale reals
assumes R_are_reals: \( \text{IsAmodelOfReals}(\mathbb{R} ,Add,Mul, ROrd) \)
defines \( 0 \equiv \text{TheNeutralElement}(\mathbb{R} ,Add) \)
defines \( 1 \equiv \text{TheNeutralElement}(\mathbb{R} ,Mul) \)
defines \( x \cdot y \equiv Mul\langle x,y\rangle \)
defines \( x + y \equiv Add\langle x,y\rangle \)
defines \( ( - x) \equiv \text{GroupInv}(\mathbb{R} ,Add)(x) \)
defines \( x - y \equiv x + ( - y) \)
defines \( x \leq y \equiv \langle x,y\rangle \in ROrd \)
defines \( x \lt y \equiv x\leq y \wedge x\neq y \)
defines \( \mathbb{R} ^+ \equiv \text{Nonnegative}(\mathbb{R} ,Add, ROrd) \)
defines \( \mathbb{R} _+ \equiv \text{PositiveSet}(\mathbb{R} ,Add, ROrd) \)
defines \( -A \equiv \text{GroupInv}(\mathbb{R} ,Add)(A) \)
defines \( \mathbb{R} _0 \equiv \mathbb{R} -\{ 0 \} \)
defines \( \vert x\vert \equiv \text{AbsoluteValue}(\mathbb{R} ,Add,ROrd)(x) \)
defines \( dist \equiv \{\langle p,\vert \text{fst}(p) - \text{snd}(p)\vert \rangle .\ p \in \mathbb{R} \times \mathbb{R} \} \)
defines \( 2 \equiv 1 + 1 \)
defines \( x^{-1} \equiv \text{GroupInv}(\mathbb{R} _0,\text{restrict}(Mul,\mathbb{R} _0\times \mathbb{R} _0))(x) \)
defines \( x^2 \equiv x\cdot x \)
defines \( f^\circ \equiv \text{OddExtension}(\mathbb{R} ,Add,ROrd,f) \)
defines \( disk(c,r) \equiv \text{Disk}(\mathbb{R} ,dist,ROrd,c,r) \)
The assumtions of the field1 locale (that sets the context for ordered fields) hold in the reals locale
lemma (in reals) field1_is_valid:
shows \( field1(\mathbb{R} , Add, Mul,ROrd) \)proofWe can use theorems proven in the field1 locale in the reals locale. Note that since the the field1 locale is an extension of the ring1 locale, which is an extension of ring0 locale , this makes available also the theorems proven in the ring1 and ring0 locales.
using field1_is_valid
The group3 locale from the OrderedGroup_ZF theory defines context for theorems about ordered groups. We can use theorems proven in there in the reals locale as real numbers with addition form an ordered group.
unfolding group3_def using OrdRing_ZF_1_L4
Since real numbers with addition form a group we can use the theorems proven in the group0 locale defined in the Group_ZF theory in the reals locale.
unfolding group3_def using OrderedGroup_ZF_1_L1
Let's recall basic properties of the real line.
lemma (in reals) basic_props:
shows \( ROrd \text{ is total on } \mathbb{R} \) and \( Add \text{ is commutative on } \mathbb{R} \) using OrdRing_ZF_1_L4(2,3)The distance function dist defined in the reals locale is a metric.
lemma (in reals) dist_is_metric:
shows \( dist : \mathbb{R} \times \mathbb{R} \rightarrow \mathbb{R} ^+ \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = \vert x - y\vert \), \( \forall x\in \mathbb{R} .\ dist\langle x,x\rangle = 0 \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = dist\langle y,x\rangle \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ \vert x - z\vert \leq \vert x - y\vert + \vert y - z\vert \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ \forall z\in \mathbb{R} .\ dist\langle x,z\rangle \leq dist\langle x, y\rangle + dist\langle y,z\rangle \), \( \forall x\in \mathbb{R} .\ \forall y\in \mathbb{R} .\ dist\langle x,y\rangle = 0 \longrightarrow x=y \), \( \text{IsAmetric}(dist,\mathbb{R} ,\mathbb{R} ,Add,ROrd) \)proofThe assumptions of the pmetric_space locale hold in the reals locale.
lemma (in reals) pmetric_space_valid:
shows \( pmetric\_space(dist, \mathbb{R} , \mathbb{R} , Add, ROrd) \) using OrdRing_ZF_1_L4(1) , dist_is_metric unfolding IsAmetric_def , pmetric_space_defTheorems proven in the pmetric_space locale are valid in the reals locale.
using OrdRing_ZF_1_L4(1) , dist_is_metric unfolding IsAmetric_def , pmetric_space_def
Some properties of the order relation on reals:
lemma (in reals) pos_is_lattice:
shows \( \text{IsLinOrder}(\mathbb{R} ,ROrd) \), \( \text{IsLinOrder}(\mathbb{R} _+,ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \), \( (ROrd \cap \mathbb{R} _+\times \mathbb{R} _+) \text{ is a lattice on } \mathbb{R} _+ \)proofWe define the topology on reals as one consisting of the unions of open disks.
Definition (in reals)
\( \tau _\mathbb{R} \equiv \{\bigcup A.\ A \in Pow(\bigcup c\in \mathbb{R} .\ \{disk(c,r).\ r \in \mathbb{R} _+\})\} \)
Real numbers form a topological space with topology generated by open disks.
theorem (in reals) reals_is_top:
shows \( \tau _\mathbb{R} \text{ is a topology } \) and \( \bigcup \tau _\mathbb{R} = \mathbb{R} \) using R_are_reals , pos_is_lattice(3) , ordring_one_is_pos , pmetric_is_top unfolding IsAlattice_def , IsAmodelOfReals_def , IsAnOrdField_def , RealTopology_defassumes \( a\in G \), \( b\in G \)
shows \( a\cdot b \in G \)assumes \( x\in G \)
shows \( x^{-1}\in G \)assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( |a| \in G^+ \)assumes \( \forall x\in X.\ b(x) \in Y \)
shows \( \{\langle x,b(x)\rangle .\ x\in X\} : X\rightarrow Y \)assumes \( f:X\rightarrow Y \) and \( f = \{\langle x,b(x)\rangle .\ x\in X\} \)
shows \( \forall x\in X.\ f(x) = b(x) \)assumes \( x\in G \)
shows \( x\cdot x^{-1} = 1 \wedge x^{-1}\cdot x = 1 \)assumes \( a\in G \), \( b\in G \)
shows \( (a\cdot b^{-1})^{-1} = b\cdot a^{-1} \), \( (a^{-1}\cdot b)^{-1} = b^{-1}\cdot a \)assumes \( r \text{ is total on } G \) and \( a\in G \)
shows \( |a^{-1}| = |a| \)assumes \( a\in G \) and \( |a| = 1 \)
shows \( a = 1 \)assumes \( a\in G \), \( b\in G \) and \( a\cdot b^{-1} = 1 \)
shows \( a=b \)assumes \( a\in G \), \( b\in G \), \( c\in G \)
shows \( (a\cdot b)^{-1}\cdot (a\cdot c) = b^{-1}\cdot c \), \( (a\cdot b)\cdot (c\cdot b)^{-1} = a\cdot c^{-1} \), \( a^{-1}\cdot (a\cdot b\cdot c)\cdot c^{-1} = b \), \( a\cdot (b\cdot c^{-1})\cdot c = a\cdot b \), \( a\cdot b^{-1}\cdot (b\cdot c^{-1}) = a\cdot c^{-1} \)assumes \( P \text{ is commutative on } G \) and \( r \text{ is total on } G \) and \( a\in G \), \( b\in G \)
shows \( |a\cdot b| \leq |a|\cdot |b| \)assumes \( \text{IsLinOrder}(X,r) \) and \( A\subseteq X \)
shows \( \text{IsLinOrder}(A,r) \) and \( \text{IsLinOrder}(A,r \cap A\times A) \)assumes \( r\subseteq L\times L \) and \( \text{IsLinOrder}(L,r) \)
shows \( r \text{ is a lattice on } L \)assumes \( 0 \neq 1 \)
shows \( 1 \in R_+ \)assumes \( \text{IsMeetSemilattice}(G_+,r \cap G_+\times G_+) \), \( G_+\neq 0 \)
defines \( B \equiv \bigcup c\in X.\ \{disk(c,R).\ R\in G_+\} \)
defines \( T \equiv \{\bigcup A.\ A \in Pow(B)\} \)
shows \( T \text{ is a topology } \), \( B \text{ is a base for } T \), \( \bigcup T = X \)