src/HOL/Hyperreal/HyperDef.thy
author nipkow
Fri Jan 05 18:48:18 2001 +0100 (2001-01-05)
changeset 10797 028d22926a41
parent 10778 2c6605049646
child 10834 a7897aebbffc
permissions -rw-r--r--
^^ -> ```
Univalent -> single_valued
paulson@10751
     1
(*  Title       : HOL/Real/Hyperreal/HyperDef.thy
paulson@10751
     2
    ID          : $Id$
paulson@10751
     3
    Author      : Jacques D. Fleuriot
paulson@10751
     4
    Copyright   : 1998  University of Cambridge
paulson@10751
     5
    Description : Construction of hyperreals using ultrafilters
paulson@10751
     6
*) 
paulson@10751
     7
paulson@10751
     8
HyperDef = Filter + Real +
paulson@10751
     9
paulson@10751
    10
consts 
paulson@10751
    11
 
paulson@10751
    12
    FreeUltrafilterNat   :: nat set set    ("\\<U>")
paulson@10751
    13
paulson@10751
    14
defs
paulson@10751
    15
paulson@10751
    16
    FreeUltrafilterNat_def
paulson@10751
    17
    "FreeUltrafilterNat    ==   (@U. U : FreeUltrafilter (UNIV:: nat set))"
paulson@10751
    18
paulson@10751
    19
paulson@10751
    20
constdefs
paulson@10751
    21
    hyprel :: "((nat=>real)*(nat=>real)) set"
paulson@10751
    22
    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
paulson@10751
    23
                   {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
paulson@10751
    24
paulson@10751
    25
typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
paulson@10751
    26
paulson@10751
    27
instance
paulson@10751
    28
   hypreal  :: {ord, zero, plus, times, minus, inverse}
paulson@10751
    29
paulson@10751
    30
consts 
paulson@10751
    31
paulson@10751
    32
  "1hr"       :: hypreal               ("1hr")  
paulson@10751
    33
  "whr"       :: hypreal               ("whr")  
paulson@10751
    34
  "ehr"       :: hypreal               ("ehr")  
paulson@10751
    35
paulson@10751
    36
paulson@10751
    37
defs
paulson@10751
    38
paulson@10751
    39
  hypreal_zero_def
nipkow@10797
    40
  "0 == Abs_hypreal(hyprel```{%n::nat. (#0::real)})"
paulson@10751
    41
paulson@10751
    42
  hypreal_one_def
nipkow@10797
    43
  "1hr == Abs_hypreal(hyprel```{%n::nat. (#1::real)})"
paulson@10751
    44
paulson@10751
    45
  (* an infinite number = [<1,2,3,...>] *)
paulson@10751
    46
  omega_def
nipkow@10797
    47
  "whr == Abs_hypreal(hyprel```{%n::nat. real_of_nat (Suc n)})"
paulson@10751
    48
    
paulson@10751
    49
  (* an infinitesimal number = [<1,1/2,1/3,...>] *)
paulson@10751
    50
  epsilon_def
nipkow@10797
    51
  "ehr == Abs_hypreal(hyprel```{%n::nat. inverse (real_of_nat (Suc n))})"
paulson@10751
    52
paulson@10751
    53
  hypreal_minus_def
nipkow@10797
    54
  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel```{%n::nat. - (X n)})"
paulson@10751
    55
paulson@10751
    56
  hypreal_diff_def 
paulson@10751
    57
  "x - y == x + -(y::hypreal)"
paulson@10751
    58
paulson@10751
    59
  hypreal_inverse_def
paulson@10751
    60
  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
nipkow@10797
    61
                    hyprel```{%n. if X n = #0 then #0 else inverse (X n)})"
paulson@10751
    62
paulson@10751
    63
  hypreal_divide_def
paulson@10751
    64
  "P / Q::hypreal == P * inverse Q"
paulson@10751
    65
  
paulson@10751
    66
constdefs
paulson@10751
    67
paulson@10751
    68
  hypreal_of_real  :: real => hypreal                 
nipkow@10797
    69
  "hypreal_of_real r         == Abs_hypreal(hyprel```{%n::nat. r})"
paulson@10751
    70
paulson@10751
    71
defs 
paulson@10751
    72
paulson@10751
    73
  hypreal_add_def  
paulson@10751
    74
  "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
nipkow@10797
    75
                hyprel```{%n::nat. X n + Y n})"
paulson@10751
    76
paulson@10751
    77
  hypreal_mult_def  
paulson@10751
    78
  "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
nipkow@10797
    79
                hyprel```{%n::nat. X n * Y n})"
paulson@10751
    80
paulson@10751
    81
  hypreal_less_def
paulson@10751
    82
  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
paulson@10751
    83
                               Y: Rep_hypreal(Q) & 
paulson@10751
    84
                               {n::nat. X n < Y n} : FreeUltrafilterNat"
paulson@10751
    85
  hypreal_le_def
paulson@10751
    86
  "P <= (Q::hypreal) == ~(Q < P)" 
paulson@10751
    87
paulson@10751
    88
end
paulson@10751
    89
 
paulson@10751
    90