src/HOL/Real/PReal.thy

Installation of target HOL-Real

(*   Title       : PReal.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : The positive reals as Dedekind sections of positive
                  rationals. Fundamentals of Abstract Analysis [Gleason- p. 121] 
                  provides some of the definitions.
*)

PReal = PRat +

typedef preal = "{A::prat set. {} < A & A < {q::prat. True} &
                               (!y: A. ((!z. z < y --> z: A) &
                                        (? u: A. y < u)))}"      (preal_1)
instance
   preal :: {ord, plus, times}

constdefs
  preal_prat :: prat => preal              ("@#_" [80] 80)
   "@# q     == Abs_preal({x::prat. x < q})"

  pinv       :: preal => preal
  "pinv(R)   == Abs_preal({w. ? y. w < y & qinv y ~: Rep_preal(R)})" 

  psup       :: preal set => preal
  "psup(P)   == Abs_preal({w. ? X: P. w: Rep_preal(X)})"

defs

  preal_add_def
        "R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})"

  preal_mult_def
        "R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})"

  preal_less_def
        "R < (S::preal) == Rep_preal(R) < Rep_preal(S)"

  preal_le_def
        "R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)"
 
end