Theory Real_ZF_2
section ‹ Basic properties of real numbers ›
theory Real_ZF_2 imports OrderedField_ZF MetricSpace_ZF
begin
text‹ 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. ›
subsection‹Basic notation for real numbers›
text‹ In this section we define notation that we will use whenever real numbers play a role, i.e.
most of mathematics.›
text‹ The next locale sets up notation for contexts where real numbers are used.
Note we define the (real) natural numbers $\mathbb{N}$ as starting from one. ›
locale reals =
fixes Reals("ℝ") and Add and Mul and ROrd
assumes R_are_reals: "IsAmodelOfReals(ℝ,Add,Mul, ROrd)"
fixes zero ("𝟬")
defines zero_def[simp]: "𝟬 ≡ TheNeutralElement(ℝ,Add)"
fixes one ("𝟭")
defines one_def[simp]: "𝟭 ≡ TheNeutralElement(ℝ,Mul)"
fixes realmul (infixl "⋅" 71)
defines realmul_def[simp]: "x ⋅ y ≡ Mul`⟨x,y⟩"
fixes realadd (infixl "\<ra>" 69)
defines realadd_def[simp]: "x \<ra> y ≡ Add`⟨x,y⟩"
fixes realminus("\<rm> _" 89)
defines realminus_def[simp]: "(\<rm>x) ≡ GroupInv(ℝ,Add)`(x)"
fixes realsub (infixl "\<rs>" 90)
defines realsub_def [simp]: "x\<rs>y ≡ x\<ra>(\<rm>y)"
fixes lesseq (infix "\<lsq>" 68)
defines lesseq_def [simp]: "x \<lsq> y ≡ ⟨x,y⟩ ∈ ROrd"
fixes sless (infix "\<ls>" 68)
defines sless_def [simp]: "x \<ls> y ≡ x\<lsq>y ∧ x≠y"
fixes nonnegative ("ℝ⇧+")
defines nonnegative_def[simp]: "ℝ⇧+ ≡ Nonnegative(ℝ,Add, ROrd)"
fixes positiveset ("ℝ⇩+")
defines positiveset_def[simp]: "ℝ⇩+ ≡ PositiveSet(ℝ,Add, ROrd)"
fixes setinv ("\<sm> _" 72)
defines setninv_def [simp]: "\<sm>A ≡ GroupInv(ℝ,Add)``(A)"
fixes non_zero ("ℝ⇩0")
defines non_zero_def[simp]: "ℝ⇩0 ≡ ℝ-{𝟬}"
fixes abs ("¦ _ ¦")
defines abs_def [simp]: "¦x¦ ≡ AbsoluteValue(ℝ,Add,ROrd)`(x)"
fixes dist
defines dist_def[simp]: "dist ≡ {⟨p,¦fst(p) \<rs> snd(p)¦⟩ . p ∈ ℝ×ℝ}"
fixes two ("𝟮")
defines two_def[simp]: "𝟮 ≡ 𝟭 \<ra> 𝟭"
fixes inv ("_¯ " [96] 97)
defines inv_def[simp]:
"x¯ ≡ GroupInv(ℝ⇩0,restrict(Mul,ℝ⇩0×ℝ⇩0))`(x)"
fixes listsum ("∑ _" 70)
defines listsum_def[simp]: "∑s ≡ Fold(Add,𝟬,s)"
fixes nat_mult (infix "\<nm>" 95)
defines nat_mult_def [simp]: "n\<nm>x ≡ ∑{⟨k,x⟩. k∈n}"
fixes realsq ("_⇧2" [96] 97)
defines realsq_def [simp]: "x⇧2 ≡ x⋅x"
fixes oddext ("_ °")
defines oddext_def [simp]: "f° ≡ OddExtension(ℝ,Add,ROrd,f)"
fixes disk
defines disk_def [simp]: "disk(c,r) ≡ Disk(ℝ,dist,ROrd,c,r)"
fixes rxn ("ℕ")
defines rxn_def [simp]: "ℕ ≡ ⋂ {N ∈ Pow(ℝ). 𝟭 ∈ N ∧ (∀n. n∈N ⟶ n\<ra>𝟭 ∈ N)}"
text‹ 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(ℝ, Add, Mul,ROrd)"
proof
from R_are_reals show "IsAring(ℝ, Add, Mul)" and "Mul {is commutative on} ℝ"
and "ROrd ⊆ ℝ × ℝ" and "IsLinOrder(ℝ, ROrd)"
and "∀x y. ∀z∈ℝ. ⟨x, y⟩ ∈ ROrd ⟶ ⟨Add`⟨x, z⟩, Add`⟨y, z⟩⟩ ∈ ROrd"
and "Nonnegative(ℝ, Add, ROrd) {is closed under} Mul"
and "TheNeutralElement(ℝ, Add) ≠ TheNeutralElement(ℝ, Mul)"
and "∀x∈ℝ. x ≠ TheNeutralElement(ℝ,Add) ⟶ (∃y∈ℝ. Mul`⟨x, y⟩ = TheNeutralElement(ℝ,Mul))"
using IsAmodelOfReals_def IsAnOrdField_def IsAnOrdRing_def by auto
qed
text‹ We 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. ›
sublocale reals < field1 Reals Add Mul realadd realminus realsub realmul
zero one two realsq listsum nat_mult ROrd
using field1_is_valid by auto
text‹ 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. ›
sublocale reals < group3 Reals Add ROrd zero realadd realminus lesseq sless nonnegative positiveset
unfolding group3_def using OrdRing_ZF_1_L4 by auto
text‹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. ›
sublocale reals < group0 Reals Add zero realadd realminus listsum nat_mult
unfolding group3_def using OrderedGroup_ZF_1_L1 by auto
text‹Let's recall basic properties of the real line. ›
lemma (in reals) basic_props: shows "ROrd {is total on} ℝ" and "Add {is commutative on} ℝ"
using OrdRing_ZF_1_L4(2,3) by auto
text‹ The distance function ‹dist› defined in the ‹reals› locale is a metric. ›
lemma (in reals) dist_is_metric: shows
"dist : ℝ×ℝ → ℝ⇧+"
"∀x∈ℝ.∀y∈ℝ. dist`⟨x,y⟩ = ¦x \<rs> y¦"
"∀x∈ℝ.dist`⟨x,x⟩ = 𝟬"
"∀x∈ℝ.∀y∈ℝ. dist`⟨x,y⟩ = dist`⟨y,x⟩"
"∀x∈ℝ.∀y∈ℝ.∀z∈ℝ. ¦x \<rs> z¦ \<lsq> ¦x \<rs> y¦ \<ra> ¦y \<rs> z¦"
"∀x∈ℝ.∀y∈ℝ.∀z∈ℝ. dist`⟨x,z⟩ \<lsq> dist`⟨x, y⟩ \<ra> dist`⟨y,z⟩"
"∀x∈ℝ.∀y∈ℝ. dist`⟨x,y⟩ = 𝟬 ⟶ x=y"
"IsApseudoMetric(dist,ℝ,ℝ,Add,ROrd)"
"IsAmetric(dist,ℝ,ℝ,Add,ROrd)"
proof -
show I: "dist : ℝ×ℝ → ℝ⇧+" using add_group.group_op_closed add_group.inverse_in_group OrdRing_ZF_1_L4
OrderedGroup_ZF_3_L3B ZF_fun_from_total by simp
then show II:"∀x∈ℝ.∀y∈ℝ. dist`⟨x,y⟩ = ¦x\<rs>y¦" using ZF_fun_from_tot_val0 by auto
then show III: "∀x∈ℝ.dist`⟨x,x⟩ = 𝟬" using add_group.group0_2_L6 OrderedGroup_ZF_3_L2A by simp
{ fix x y
assume "x∈ℝ" "y∈ℝ"
then have "(\<rm>(x\<rs>y)) = y\<rs>x" using add_group.group0_2_L12 by simp
moreover from ‹x∈ℝ› ‹y∈ℝ› have "¦\<rm>(x\<rs>y)¦ =¦x\<rs>y¦"
using add_group.group_op_closed add_group.inverse_in_group basic_props(1) OrderedGroup_ZF_3_L7A
by simp
ultimately have "¦y\<rs>x¦ = ¦x\<rs>y¦" by simp
with ‹x∈ℝ› ‹y∈ℝ› II have "dist`⟨x,y⟩ = dist`⟨y,x⟩" by simp
} thus IV: "∀x∈ℝ.∀y∈ℝ. dist`⟨x,y⟩ = dist`⟨y,x⟩" by simp
{ fix x y
assume "x∈ℝ" "y∈ℝ" "dist`⟨x,y⟩ = 𝟬"
with II have "¦x\<rs>y¦ = 𝟬" by simp
with ‹x∈ℝ› ‹y∈ℝ› have "x\<rs>y = 𝟬"
using add_group.group_op_closed add_group.inverse_in_group OrderedGroup_ZF_3_L3D by auto
with ‹x∈ℝ› ‹y∈ℝ› have"x=y" using add_group.group0_2_L11A by simp
} thus V: "∀x∈ℝ.∀y∈ℝ. dist`⟨x,y⟩ = 𝟬 ⟶ x=y" by auto
{ fix x y z
assume "x∈ℝ" "y∈ℝ" "z∈ℝ"
then have "¦x\<rs>z¦ = ¦(x\<rs>y)\<ra>(y \<rs> z)¦" using add_group.cancel_middle(5) by simp
with ‹x∈ℝ› ‹y∈ℝ› ‹z∈ℝ› have "¦x\<rs>z¦ \<lsq> ¦x\<rs>y¦ \<ra> ¦y \<rs> z¦"
using add_group.group_op_closed add_group.inverse_in_group OrdRing_ZF_1_L4(2,3) OrdGroup_triangle_ineq
by simp
} thus "∀x∈ℝ.∀y∈ℝ.∀z∈ℝ. ¦x \<rs> z¦ \<lsq> ¦x \<rs> y¦ \<ra> ¦y \<rs> z¦" by simp
with II show "∀x∈ℝ.∀y∈ℝ.∀z∈ℝ. dist`⟨x,z⟩ \<lsq> dist`⟨x, y⟩ \<ra> dist`⟨y,z⟩" by auto
with I III IV V show "IsApseudoMetric(dist,ℝ,ℝ,Add,ROrd)" and "IsAmetric(dist,ℝ,ℝ,Add,ROrd)"
unfolding IsApseudoMetric_def IsAmetric_def by auto
qed
text‹Real numbers form an ordered loop.›
lemma (in reals) reals_loop: shows "IsAnOrdLoop(ℝ,Add,ROrd)"
proof -
have "IsAloop(ℝ,Add)" using add_group.group_is_loop by simp
moreover from R_are_reals have "ROrd ⊆ ℝ × ℝ" and "IsPartOrder(ℝ,ROrd)"
using IsAmodelOfReals_def IsAnOrdField_def IsAnOrdRing_def Order_ZF_1_L2
by auto
moreover
{ fix x y z assume A: "x∈ℝ" "y∈ℝ" "z∈ℝ"
then have "x\<lsq>y ⟷ x\<ra>z \<lsq> y\<ra>z"
using ord_transl_inv ineq_cancel_right by blast
moreover from A have "x\<lsq>y ⟷ z\<ra>x \<lsq> z\<ra>y"
using ord_transl_inv OrderedGroup_ZF_1_L5AE by blast
ultimately have "(x\<lsq>y ⟷ x\<ra>z \<lsq> y\<ra>z) ∧ (x\<lsq>y ⟷ z\<ra>x \<lsq> z\<ra>y)"
by simp
}
ultimately show "IsAnOrdLoop(ℝ,Add,ROrd)" unfolding IsAnOrdLoop_def by auto
qed
text‹ The assumptions of the ‹pmetric_space› locale hold in the ‹reals› locale. ›
lemma (in reals) pmetric_space_valid: shows "pmetric_space(ℝ,Add, ROrd,dist,ℝ)"
unfolding pmetric_space_def pmetric_space_axioms_def loop1_def
using reals_loop dist_is_metric(8)
by blast
text‹ The assumptions of the ‹metric_space› locale hold in the ‹reals› locale. ›
lemma (in reals) metric_space_valid: shows "metric_space(ℝ,Add, ROrd,dist,ℝ)"
proof -
have "∀x∈ℝ. ∀y∈ℝ. dist`⟨x,y⟩=𝟬 ⟶ x=y"
using dist_is_metric(9) unfolding IsAmetric_def by auto
then show ?thesis unfolding metric_space_def metric_space_axioms_def
using pmetric_space_valid by simp
qed
text‹Some properties of the order relation on reals: ›
lemma (in reals) pos_is_lattice: shows
"IsLinOrder(ℝ,ROrd)"
"IsLinOrder(ℝ⇩+,ROrd ∩ ℝ⇩+×ℝ⇩+)"
"(ROrd ∩ ℝ⇩+×ℝ⇩+) {is a lattice on} ℝ⇩+"
proof -
show "IsLinOrder(ℝ,ROrd)" using OrdRing_ZF_1_L1 unfolding IsAnOrdRing_def by simp
moreover have "ℝ⇩+ ⊆ ℝ" using pos_set_in_gr by simp
ultimately show "IsLinOrder(ℝ⇩+,ROrd ∩ ℝ⇩+×ℝ⇩+)" using ord_linear_subset(2) by simp
moreover have "(ROrd ∩ ℝ⇩+×ℝ⇩+) ⊆ ℝ⇩+×ℝ⇩+" by auto
ultimately show "(ROrd ∩ ℝ⇩+×ℝ⇩+) {is a lattice on} ℝ⇩+" using lin_is_latt by simp
qed
text‹Of course the set of positive real numbers is nonempty as one is there.›
lemma (in reals) pos_non_empty: shows "ℝ⇩+≠0"
using R_are_reals ordring_one_is_pos
unfolding IsAmodelOfReals_def IsAnOrdField_def by auto
text‹We say that a relation $r$ ‹down-directs› a set $R$ if every two-element subset
of $R$ has a lower bound. The next lemma states that the natural order relation on real numbers
down-directs the set of positive reals. ›
lemma (in reals) rord_down_directs: shows "ROrd {down-directs} ℝ⇩+"
using pos_is_lattice(3) pos_non_empty meet_down_directs down_dir_mono
unfolding IsAlattice_def by blast
text‹ We define the topology on reals as the metric topology
coming from the ‹dist› metric (i.e. consisting of the unions of open disks). ›
definition (in reals) RealTopology ("τ⇩ℝ")
where "τ⇩ℝ ≡ MetricTopology(ℝ,ℝ,Add,ROrd,dist)"
text‹A more explicit definition of the real topology in notation used in the ‹reals› context. ›
lemma (in reals) real_toplology_def_alt:
shows "τ⇩ℝ = {⋃A. A ∈ Pow(⋃c∈ℝ.{disk(c,r). r ∈ ℝ⇩+})}"
unfolding MetricTopology_def RealTopology_def by simp
text‹Real numbers form a Hausdorff topological space with topology generated by open disks. ›
theorem (in reals) reals_is_top:
shows "τ⇩ℝ {is a topology}" "⋃τ⇩ℝ = ℝ" "τ⇩ℝ {is T⇩2}"
using rord_down_directs metric_space_valid pmetric_space_valid pmetric_space.pmetric_is_top
pmetric_space.metric_top_carrier metric_space.metric_space_T2
unfolding RealTopology_def by simp_all
end