Theory Real_ZF_2

(* 
    This file is a part of IsarMathLib - 
    a library of formalized mathematics written for Isabelle/Isar.

    Copyright (C) 2020,2021 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. *)

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. ›

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 "\<rmu>" 71)
  defines realmul_def[simp]: "x \<rmu> 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 ("ℝ⇩₀")
  defines non_zero_def[simp]: "ℝ⇩₀ ≡ ℝ-{𝟬}"

  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(ℝ⇩₀,restrict(Mul,ℝ⇩₀×ℝ⇩₀))`(x)"

  fixes realsq ("_⇧²" [96] 97)
  defines realsq_def [simp]: "x⇧² ≡ x\<rmu>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)"

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 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 
  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 one consisting of the unions of open disks. ›

definition (in reals) RealTopology ("τ⇩_ℝ") 
  where "τ⇩_ℝ ≡ {⋃A. A ∈ Pow(⋃c∈ℝ.{disk(c,r). r ∈ ℝ⇩₊})}"
  
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⇩₂}"
  using rord_down_directs metric_space_valid pmetric_space_valid 
    pmetric_space.pmetric_is_top  metric_space.metric_space_T2
  unfolding RealTopology_def
    by simp_all

end