src/HOL/Hyperreal/HyperDef.thy
author nipkow
Tue Jan 09 15:32:27 2001 +0100 (2001-01-09)
changeset 10834 a7897aebbffc
parent 10797 028d22926a41
child 10919 144ede948e58
permissions -rw-r--r--
*** empty log message ***
     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"   (Equiv.quotient_def)
    26 
    27 instance
    28    hypreal  :: {ord, zero, plus, times, minus, inverse}
    29 
    30 consts 
    31 
    32   "1hr"       :: hypreal               ("1hr")  
    33   "whr"       :: hypreal               ("whr")  
    34   "ehr"       :: hypreal               ("ehr")  
    35 
    36 
    37 defs
    38 
    39   hypreal_zero_def
    40   "0 == Abs_hypreal(hyprel``{%n::nat. (#0::real)})"
    41 
    42   hypreal_one_def
    43   "1hr == Abs_hypreal(hyprel``{%n::nat. (#1::real)})"
    44 
    45   (* an infinite number = [<1,2,3,...>] *)
    46   omega_def
    47   "whr == Abs_hypreal(hyprel``{%n::nat. real_of_nat (Suc n)})"
    48     
    49   (* an infinitesimal number = [<1,1/2,1/3,...>] *)
    50   epsilon_def
    51   "ehr == Abs_hypreal(hyprel``{%n::nat. inverse (real_of_nat (Suc n))})"
    52 
    53   hypreal_minus_def
    54   "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    55 
    56   hypreal_diff_def 
    57   "x - y == x + -(y::hypreal)"
    58 
    59   hypreal_inverse_def
    60   "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
    61                     hyprel``{%n. if X n = #0 then #0 else inverse (X n)})"
    62 
    63   hypreal_divide_def
    64   "P / Q::hypreal == P * inverse Q"
    65   
    66 constdefs
    67 
    68   hypreal_of_real  :: real => hypreal                 
    69   "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    70 
    71 defs 
    72 
    73   hypreal_add_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_mult_def  
    78   "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    79                 hyprel``{%n::nat. X n * Y n})"
    80 
    81   hypreal_less_def
    82   "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
    83                                Y: Rep_hypreal(Q) & 
    84                                {n::nat. X n < Y n} : FreeUltrafilterNat"
    85   hypreal_le_def
    86   "P <= (Q::hypreal) == ~(Q < P)" 
    87 
    88 end
    89  
    90