src/HOL/Real/Real.thy
changeset 5588 a3ab526bb891
parent 5078 7b5ea59c0275
child 7077 60b098bb8b8a
     1.1 --- a/src/HOL/Real/Real.thy	Tue Sep 29 18:13:05 1998 +0200
     1.2 +++ b/src/HOL/Real/Real.thy	Thu Oct 01 18:18:01 1998 +0200
     1.3 @@ -1,61 +1,14 @@
     1.4 -(*  Title       : Real.thy
     1.5 -    Author      : Jacques D. Fleuriot
     1.6 -    Copyright   : 1998  University of Cambridge
     1.7 -    Description : The reals
     1.8 -*) 
     1.9 -
    1.10 -Real = PReal +
    1.11 -
    1.12 -constdefs
    1.13 -    realrel   ::  "((preal * preal) * (preal * preal)) set"
    1.14 -    "realrel  ==  {p. ? x1 y1 x2 y2. p=((x1::preal,y1),(x2,y2)) & x1+y2 = x2+y1}" 
    1.15 -
    1.16 -typedef real = "{x::(preal*preal).True}/realrel"          (Equiv.quotient_def)
    1.17 -
    1.18 -
    1.19 -instance
    1.20 -   real  :: {ord,plus,times}
    1.21 -
    1.22 -consts 
    1.23 -
    1.24 -  "0r"       :: real               ("0r")   
    1.25 -  "1r"       :: real               ("1r")  
    1.26 -
    1.27 -defs
    1.28 -
    1.29 -  real_zero_def      "0r == Abs_real(realrel^^{(@#($#1p),@#($#1p))})"
    1.30 -  real_one_def       "1r == Abs_real(realrel^^{(@#($#1p) + @#($#1p),@#($#1p))})"
    1.31 -
    1.32 -constdefs
    1.33 +(*  Title:      Real/Real.thy
    1.34 +    ID:         $Id$
    1.35 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    1.36 +    Copyright   1998  University of Cambridge
    1.37  
    1.38 -  real_preal :: preal => real              ("%#_" [80] 80)
    1.39 -  "%# m     == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})"
    1.40 -
    1.41 -  real_minus :: real => real               ("%~ _" [80] 80) 
    1.42 -  "%~ R     ==  Abs_real(UN p:Rep_real(R). split (%x y. realrel^^{(y,x)}) p)"
    1.43 -
    1.44 -  rinv       :: real => real
    1.45 -  "rinv(R)   == (@S. R ~= 0r & S*R = 1r)"
    1.46 -
    1.47 -  real_nat :: nat => real                  ("%%# _" [80] 80) 
    1.48 -  "%%# n      == %#(@#($#(*# n)))"
    1.49 -
    1.50 -defs
    1.51 +Type "real" is a linear order
    1.52 +*)
    1.53  
    1.54 -  real_add_def  
    1.55 -  "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
    1.56 -                split(%x1 y1. split(%x2 y2. realrel^^{(x1+x2, y1+y2)}) p2) p1)"
    1.57 -  
    1.58 -  real_mult_def  
    1.59 -  "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
    1.60 -                split(%x1 y1. split(%x2 y2. realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
    1.61 +Real = RealDef +
    1.62  
    1.63 -  real_less_def
    1.64 -  "P < (Q::real) == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
    1.65 -                                   (x1,y1::preal):Rep_real(P) &
    1.66 -                                   (x2,y2):Rep_real(Q)" 
    1.67 -
    1.68 -  real_le_def
    1.69 -  "P <= (Q::real) == ~(Q < P)"
    1.70 +instance real :: order (real_le_refl,real_le_trans,real_le_anti_sym,real_less_le)
    1.71 +instance real :: linorder (real_le_linear)
    1.72  
    1.73  end