src/HOL/Hyperreal/HyperDef.thy
author wenzelm
Thu Aug 08 23:52:55 2002 +0200 (2002-08-08)
changeset 13487 1291c6375c29
parent 12018 ec054019c910
child 14299 0b5c0b0a3eba
permissions -rw-r--r--
tuned;
     1 (*  Title       : HOL/Real/Hyperreal/HyperDef.thy
     2     ID          : $Id$
     3     Author      : Jacques D. Fleuriot
     4     Copyright   : 1998  University of Cambridge
     5     Description : Construction of hyperreals using ultrafilters
     6 *)
     7 
     8 HyperDef = Filter + Real +
     9 
    10 consts
    11 
    12     FreeUltrafilterNat   :: nat set set    ("\\<U>")
    13 
    14 defs
    15 
    16     FreeUltrafilterNat_def
    17     "FreeUltrafilterNat    ==   (@U. U : FreeUltrafilter (UNIV:: nat set))"
    18 
    19 
    20 constdefs
    21     hyprel :: "((nat=>real)*(nat=>real)) set"
    22     "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) &
    23                    {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    24 
    25 typedef hypreal = "UNIV//hyprel"   (quotient_def)
    26 
    27 instance
    28    hypreal  :: {ord, zero, one, plus, times, minus, inverse}
    29 
    30 defs
    31 
    32   hypreal_zero_def
    33   "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})"
    34 
    35   hypreal_one_def
    36   "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})"
    37 
    38   hypreal_minus_def
    39   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    40 
    41   hypreal_diff_def
    42   "x - y == x + -(y::hypreal)"
    43 
    44   hypreal_inverse_def
    45   "inverse P == Abs_hypreal(UN X: Rep_hypreal(P).
    46                     hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
    47 
    48   hypreal_divide_def
    49   "P / Q::hypreal == P * inverse Q"
    50 
    51 constdefs
    52 
    53   hypreal_of_real  :: real => hypreal
    54   "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    55 
    56   omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
    57   "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
    58 
    59   epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
    60   "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
    61 
    62 syntax (xsymbols)
    63   omega   :: hypreal   ("\\<omega>")
    64   epsilon :: hypreal   ("\\<epsilon>")
    65 
    66 
    67 defs
    68 
    69   hypreal_add_def
    70   "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    71                 hyprel``{%n::nat. X n + Y n})"
    72 
    73   hypreal_mult_def
    74   "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    75                 hyprel``{%n::nat. X n * Y n})"
    76 
    77   hypreal_less_def
    78   "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) &
    79                                Y: Rep_hypreal(Q) &
    80                                {n::nat. X n < Y n} : FreeUltrafilterNat"
    81   hypreal_le_def
    82   "P <= (Q::hypreal) == ~(Q < P)"
    83 
    84 end