src/HOL/Real/RealDef.thy
author wenzelm
Mon Oct 08 15:23:20 2001 +0200 (2001-10-08)
changeset 11713 883d559b0b8c
parent 11701 3d51fbf81c17
child 12018 ec054019c910
permissions -rw-r--r--
sane numerals (stage 3): provide generic "1" on all number types;
paulson@5588
     1
(*  Title       : Real/RealDef.thy
paulson@7219
     2
    ID          : $Id$
paulson@5588
     3
    Author      : Jacques D. Fleuriot
paulson@5588
     4
    Copyright   : 1998  University of Cambridge
paulson@5588
     5
    Description : The reals
paulson@5588
     6
*) 
paulson@5588
     7
paulson@5588
     8
RealDef = PReal +
paulson@5588
     9
paulson@10752
    10
instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym,
paulson@10752
    11
                         preal_less_le)
paulson@10752
    12
paulson@5588
    13
constdefs
paulson@5588
    14
  realrel   ::  "((preal * preal) * (preal * preal)) set"
paulson@10919
    15
  "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
paulson@5588
    16
paulson@10919
    17
typedef (REAL)
paulson@10919
    18
  real = "UNIV//realrel"  (Equiv.quotient_def)
paulson@5588
    19
paulson@5588
    20
paulson@5588
    21
instance
wenzelm@11713
    22
   real  :: {ord, zero, one, plus, times, minus, inverse}
paulson@5588
    23
paulson@5588
    24
consts 
paulson@10778
    25
   (*Overloaded constants denoting the Nat and Real subsets of enclosing
paulson@10778
    26
     types such as hypreal and complex*)
paulson@10919
    27
   Nats, Reals :: "'a set"
paulson@10778
    28
  
paulson@10919
    29
   (*overloaded constant for injecting other types into "real"*)
paulson@10919
    30
   real :: 'a => real
paulson@10919
    31
paulson@5588
    32
paulson@5588
    33
defs
paulson@5588
    34
paulson@7077
    35
  real_zero_def  
paulson@10919
    36
  "0 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1p),
paulson@7077
    37
                                preal_of_prat(prat_of_pnat 1p))})"
paulson@7077
    38
  real_one_def   
wenzelm@11713
    39
  "1 == Abs_REAL(realrel``{(preal_of_prat(prat_of_pnat 1p) + 
paulson@7077
    40
            preal_of_prat(prat_of_pnat 1p),preal_of_prat(prat_of_pnat 1p))})"
paulson@5588
    41
paulson@5588
    42
  real_minus_def
paulson@10919
    43
  "- R ==  Abs_REAL(UN (x,y):Rep_REAL(R). realrel``{(y,x)})"
bauerg@10606
    44
bauerg@10606
    45
  real_diff_def
bauerg@10606
    46
  "R - (S::real) == R + - S"
paulson@5588
    47
bauerg@10606
    48
  real_inverse_def
wenzelm@11713
    49
  "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)"
paulson@5588
    50
bauerg@10606
    51
  real_divide_def
bauerg@10606
    52
  "R / (S::real) == R * inverse S"
bauerg@10606
    53
  
paulson@5588
    54
constdefs
paulson@5588
    55
paulson@10919
    56
  (** these don't use the overloaded real because users don't see them **)
paulson@10919
    57
  
paulson@7077
    58
  real_of_preal :: preal => real            
paulson@7077
    59
  "real_of_preal m     ==
paulson@10919
    60
           Abs_REAL(realrel``{(m+preal_of_prat(prat_of_pnat 1p),
paulson@7077
    61
                               preal_of_prat(prat_of_pnat 1p))})"
paulson@5588
    62
paulson@7077
    63
  real_of_posnat :: nat => real             
paulson@7077
    64
  "real_of_posnat n == real_of_preal(preal_of_prat(prat_of_pnat(pnat_of_nat n)))"
paulson@7077
    65
paulson@5588
    66
paulson@5588
    67
defs
paulson@5588
    68
paulson@10919
    69
  (*overloaded*)
wenzelm@11713
    70
  real_of_nat_def   "real n == real_of_posnat n + (- 1)"
paulson@10919
    71
paulson@5588
    72
  real_add_def  
paulson@10919
    73
  "P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
nipkow@10834
    74
                   (%(x1,y1). (%(x2,y2). realrel``{(x1+x2, y1+y2)}) p2) p1)"
paulson@5588
    75
  
paulson@5588
    76
  real_mult_def  
paulson@10919
    77
  "P*Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).
nipkow@10834
    78
                   (%(x1,y1). (%(x2,y2). realrel``{(x1*x2+y1*y2,x1*y2+x2*y1)})
paulson@10752
    79
		   p2) p1)"
paulson@5588
    80
paulson@5588
    81
  real_less_def
paulson@10752
    82
  "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
paulson@10919
    83
                            (x1,y1):Rep_REAL(P) & (x2,y2):Rep_REAL(Q)" 
paulson@5588
    84
  real_le_def
paulson@5588
    85
  "P <= (Q::real) == ~(Q < P)"
paulson@5588
    86
paulson@10752
    87
syntax (symbols)
paulson@10919
    88
  Reals     :: "'a set"                   ("\\<real>")
paulson@10919
    89
  Nats      :: "'a set"                   ("\\<nat>")
paulson@10752
    90
paulson@5588
    91
end