src/HOL/Hyperreal/NSA.thy
author wenzelm
Fri, 09 Nov 2001 00:09:47 +0100
changeset 12114 a8e860c86252
parent 10919 144ede948e58
child 14370 b0064703967b
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     1
(*  Title       : NSA.thy
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    Author      : Jacques D. Fleuriot
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Copyright   : 1998  University of Cambridge
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
    Description : Infinite numbers, Infinitesimals,
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
                  infinitely close relation etc.
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     6
*) 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     7
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     8
NSA = HRealAbs + RComplete +
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
constdefs
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
  Infinitesimal  :: "hypreal set"
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    13
   "Infinitesimal == {x. ALL r: Reals. 0 < r --> abs x < r}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    14
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    15
  HFinite :: "hypreal set"
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    16
   "HFinite == {x. EX r: Reals. abs x < r}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    17
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    18
  HInfinite :: "hypreal set"
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    19
   "HInfinite == {x. ALL r: Reals. r < abs x}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    20
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    21
  (* standard part map *)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    22
  st        :: hypreal => hypreal
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    23
   "st           == (%x. @r. x : HFinite & r:Reals & r @= x)"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    24
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
  monad     :: hypreal => hypreal set
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    26
   "monad x      == {y. x @= y}"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    27
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    28
  galaxy    :: hypreal => hypreal set
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    29
   "galaxy x     == {y. (x + -y) : HFinite}"
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    30
 
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    31
  (* infinitely close *)
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    32
  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    33
   "x @= y       == (x + -y) : Infinitesimal"     
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    34
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    35
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    36
defs  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    37
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    38
   (*standard real numbers as a subset of the hyperreals*)
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    39
   SReal_def      "Reals == {x. EX r. x = hypreal_of_real r}"
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    40
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 10919
diff changeset
    41
syntax (xsymbols)
10919
144ede948e58 renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents: 10751
diff changeset
    42
    approx :: "[hypreal, hypreal] => bool"    (infixl "\\<approx>" 50)
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    43
  
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    44
end
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    45
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    46
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    47
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    48