Theory Real_ZF

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

    Copyright (C) 2005, 2006  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.

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

*)

header {*\isaheader{Real\_ZF.thy}*}

theory Real_ZF imports Int_ZF Ring_ZF_1

begin

text{*The goal of the @{text "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. @{text "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.
  *}

section{*The definition of real numbers*}

text{*First we define slopes and real numbers as the set of their classes.
  The definition of slopes references the notion of almost homomorphisms 
  defined in @{text "Group_ZF_2.thy"}: slopes 
  are defined as almost homomorphisms
  on integers with integer addition as the operation. Similarly the notions
  of the first and second operation on slopes (which is really the addition 
  and composition of slopes) is 
  derived as a special case of the first and second operation on almost 
  homomorphisms. 
  *}

constdefs

  "Slopes ≡ AlmostHoms(int,IntegerAddition)"

  "SlopeOp1 ≡ AlHomOp1(int,IntegerAddition)"

  "SlopeOp2 ≡ AlHomOp2(int,IntegerAddition)"

  "BoundedIntMaps ≡ FinRangeFunctions(int,int)"

  "SlopeEquivalenceRel ≡ QuotientGroupRel(Slopes,SlopeOp1,BoundedIntMaps)"

  "RealNumbers ≡ Slopes//SlopeEquivalenceRel"

  "RealAddition ≡ ProjFun2(Slopes,SlopeEquivalenceRel,SlopeOp1)"

  "RealMultiplication ≡ ProjFun2(Slopes,SlopeEquivalenceRel,SlopeOp2)"

  (*"RealZero ≡ TheNeutralElement(RealNumbers,RealAddition)"
 
  "RealOne ≡ TheNeutralElement(RealNumbers,RealMultiplication)"*)

text{*We first show that we can use theorems proven in some proof contexts
  (locales). The locale @{text "group1"} requires assumption that we deal with
  an abelian group. The next lemma allows to use all theorems proven 
  in the context called @{text "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 @{text "Ring_ZF_1.thy"}, where we show the same in general for 
  almost homomorphisms rather than slopes.*}

theorem Real_ZF_1_T1: "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 @{text "group0"} and @{text "group1"}
  contexts applied to the group of real numbers.*}

lemma Real_ZF_1_L2:
  "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 ("\<real>")
  defines real_def [simp]: "\<real> ≡ RealNumbers"

  fixes ra (infixl "\<ra>" 69)
  defines ra_def [simp]: "a\<ra> b ≡ RealAddition`⟨a,b⟩"

  fixes rminus :: "i=>i" ("\<rm> _" 72)
  defines rminus_def [simp]:"\<rm>a ≡ GroupInv(\<real>,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 ("\<zero>")
  defines rzero_def [simp]: 
  "\<zero> ≡ TheNeutralElement(RealNumbers,RealAddition)"
 
  fixes rone ("\<one>")
  defines rone_def [simp]: 
  "\<one> ≡ TheNeutralElement(RealNumbers,RealMultiplication)"

  fixes rtwo ("\<two>")
  defines rtwo_def [simp]: "\<two>  ≡ \<one>\<ra>\<one>"

  fixes non_zero ("\<real>0")
  defines non_zero_def[simp]: "\<real>0 ≡ \<real>-{\<zero>}"

  fixes inv ("_¯ " [90] 91)
  defines inv_def[simp]: 
  "a¯ ≡ GroupInv(\<real>0,restrict(RealMultiplication,\<real>0×\<real>0))`(a)";

text{*In @{text "real0"} context all theorems proven in the @{text "ring0"},
  context are valid.*}

lemma (in real0) Real_ZF_1_L3: shows 
  "ring0(\<real>,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 "\<zero>∈\<real>"  "\<one>∈\<real>"
  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∈\<real>"
  shows 
  "(\<rm>a) ∈ \<real>"
  "(\<rm>(\<rm>a)) = a"
  "a\<ra>\<zero> = a" 
  "\<zero>\<ra>a = a" 
  "a·\<one> = a" 
  "\<one>·a = a" 
  "a\<rs>a = \<zero>" 
  "a\<rs>\<zero> = a"  
  using prems 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∈\<real>"  "b∈\<real>"
  shows 
  "a\<ra>b ∈ \<real>" 
  "a\<rs>b ∈ \<real>" 
  "a·b ∈ \<real>" 
  "a\<ra>b = b\<ra>a"
  "(\<rm>a)·b = \<rm>(a·b)" 
  "a·(\<rm>b) = \<rm>(a·b)"
  using prems 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∈\<real>"  "b∈\<real>"  "c∈\<real>"
  shows "a·(b·c) = (a·b)·c"
  using prems 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∈\<real>"  "b∈\<real>"  "c∈\<real>" 
  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 prems 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∈\<real>"  "b∈\<real>"  "c∈\<real>"  "d∈\<real>"
  shows "a\<rs>b \<ra> (c\<rs>d) = a\<ra>c\<rs>b\<rs>d"
  using prems Real_ZF_1_L2 group0.group0_4_L8A by simp;

text{*@{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 @{text "AH"}, @{text "Op1"} 
  and @{text "FR"} are used in @{text "group1"} context to denote almost 
  homomorphisms, the first operation on @{text "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 prems RealAddition_def SlopeEquivalenceRel_def
    QuotientGroupOp_def Slopes_def SlopeOp1_def BoundedIntMaps_def
  by simp;

text{*The symbol @{text "\<zero>"} in the @{text "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)) = \<zero>"
  "SlopeEquivalenceRel = r"
  using prems 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} = \<zero> <-> 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 = \<zero>"
    "?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 @{text "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 @{text "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 @{text "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} = \<zero>"
  using prems Real_ZF_1_L11 Real_ZF_1_L10 by auto;

text{*The next lemma is rephrases the result from @{text "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. @{text "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 prems Real_ZF_1_L11 eq_equiv_class equiv_class_eq
  by blast;

text{*Identity function on integers is a slope.*}

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;

text{*This 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.*}

end;