src/HOL/Real/Hyperreal/NSA.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/NSA.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,49 @@
     1.4 +(*  Title       : NSA.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Infinite numbers, Infinitesimals,
     1.8 +                  infinitely close relation etc.
     1.9 +*) 
    1.10 +
    1.11 +NSA = HRealAbs + RComplete +
    1.12 +
    1.13 +constdefs
    1.14 +
    1.15 +   (* standard real numbers reagarded as *)
    1.16 +   (* an embedded subset of hyperreals   *)
    1.17 +   SReal  :: "hypreal set"
    1.18 +   "SReal == {x. EX r. x = hypreal_of_real r}"
    1.19 +
    1.20 +   Infinitesimal  :: "hypreal set"
    1.21 +   "Infinitesimal == {x. ALL r: SReal. 0 < r --> abs x < r}"
    1.22 +
    1.23 +   HFinite :: "hypreal set"
    1.24 +   "HFinite == {x. EX r: SReal. abs x < r}"
    1.25 +
    1.26 +   HInfinite :: "hypreal set"
    1.27 +   "HInfinite == {x. ALL r: SReal. r < abs x}"
    1.28 +
    1.29 +consts   
    1.30 +
    1.31 +    (* standard part map *)
    1.32 +    st       :: hypreal => hypreal
    1.33 +
    1.34 +    (* infinitely close *)
    1.35 +    "@="     :: [hypreal,hypreal] => bool  (infixl 50)  
    1.36 +
    1.37 +    monad    :: hypreal => hypreal set
    1.38 +    galaxy   :: hypreal => hypreal set
    1.39 +
    1.40 +defs  
    1.41 +
    1.42 +   inf_close_def  "x @= y       == (x + -y) : Infinitesimal"     
    1.43 +   st_def         "st           == (%x. @r. x : HFinite & r:SReal & r @= x)"
    1.44 +
    1.45 +   monad_def      "monad x      == {y. x @= y}"
    1.46 +   galaxy_def     "galaxy x     == {y. (x + -y) : HFinite}"
    1.47 + 
    1.48 +end
    1.49 +
    1.50 +
    1.51 +
    1.52 +