src/HOL/Complex/NSCA.thy
changeset 13957 10dbf16be15f
child 14320 fb7a114826be
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Mon May 05 18:22:31 2003 +0200
     1.3 @@ -0,0 +1,44 @@
     1.4 +(*  Title       : NSCA.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 2001,2002 University of Edinburgh
     1.7 +    Description : Infinite, infinitesimal complex number etc! 
     1.8 +*)
     1.9 +
    1.10 +NSCA = NSComplexArith0 + 
    1.11 +
    1.12 +consts   
    1.13 +
    1.14 +    (* infinitely close *)
    1.15 +    "@c="     :: [hcomplex,hcomplex] => bool  (infixl 50)  
    1.16 +
    1.17 +  
    1.18 +constdefs
    1.19 +   (* standard complex numbers reagarded as an embedded subset of NS complex *)
    1.20 +   SComplex  :: "hcomplex set"
    1.21 +   "SComplex == {x. EX r. x = hcomplex_of_complex r}"
    1.22 +
    1.23 +   CInfinitesimal  :: "hcomplex set"
    1.24 +   "CInfinitesimal == {x. ALL r: Reals. 0 < r --> hcmod x < r}"
    1.25 +
    1.26 +   CFinite :: "hcomplex set"
    1.27 +   "CFinite == {x. EX r: Reals. hcmod x < r}"
    1.28 +
    1.29 +   CInfinite :: "hcomplex set"
    1.30 +   "CInfinite == {x. ALL r: Reals. r < hcmod x}"
    1.31 +
    1.32 +   (* standard part map *)  
    1.33 +   stc :: hcomplex => hcomplex
    1.34 +   "stc x == (@r. x : CFinite & r:SComplex & r @c= x)"
    1.35 +
    1.36 +   cmonad    :: hcomplex => hcomplex set
    1.37 +   "cmonad x  == {y. x @c= y}"
    1.38 +
    1.39 +   cgalaxy   :: hcomplex => hcomplex set
    1.40 +   "cgalaxy x == {y. (x - y) : CFinite}"
    1.41 +
    1.42 +
    1.43 +defs  
    1.44 +
    1.45 +   capprox_def  "x @c= y == (x - y) : CInfinitesimal"     
    1.46 + 
    1.47 +end