src/HOL/Complex/NSCA.thy
author paulson
Mon May 05 18:22:31 2003 +0200 (2003-05-05)
changeset 13957 10dbf16be15f
child 14320 fb7a114826be
permissions -rw-r--r--
new session Complex for the complex numbers
     1 (*  Title       : NSCA.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2001,2002 University of Edinburgh
     4     Description : Infinite, infinitesimal complex number etc! 
     5 *)
     6 
     7 NSCA = NSComplexArith0 + 
     8 
     9 consts   
    10 
    11     (* infinitely close *)
    12     "@c="     :: [hcomplex,hcomplex] => bool  (infixl 50)  
    13 
    14   
    15 constdefs
    16    (* standard complex numbers reagarded as an embedded subset of NS complex *)
    17    SComplex  :: "hcomplex set"
    18    "SComplex == {x. EX r. x = hcomplex_of_complex r}"
    19 
    20    CInfinitesimal  :: "hcomplex set"
    21    "CInfinitesimal == {x. ALL r: Reals. 0 < r --> hcmod x < r}"
    22 
    23    CFinite :: "hcomplex set"
    24    "CFinite == {x. EX r: Reals. hcmod x < r}"
    25 
    26    CInfinite :: "hcomplex set"
    27    "CInfinite == {x. ALL r: Reals. r < hcmod x}"
    28 
    29    (* standard part map *)  
    30    stc :: hcomplex => hcomplex
    31    "stc x == (@r. x : CFinite & r:SComplex & r @c= x)"
    32 
    33    cmonad    :: hcomplex => hcomplex set
    34    "cmonad x  == {y. x @c= y}"
    35 
    36    cgalaxy   :: hcomplex => hcomplex set
    37    "cgalaxy x == {y. (x - y) : CFinite}"
    38 
    39 
    40 defs  
    41 
    42    capprox_def  "x @c= y == (x - y) : CInfinitesimal"     
    43  
    44 end