src/HOL/Hyperreal/NSA.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/NSA.thy	Sat Dec 30 22:03:47 2000 +0100
@@ -0,0 +1,48 @@
+(*  Title       : NSA.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Description : Infinite numbers, Infinitesimals,
+                  infinitely close relation etc.
+*) 
+
+NSA = HRealAbs + RComplete +
+
+constdefs
+
+  Infinitesimal  :: "hypreal set"
+   "Infinitesimal == {x. ALL r: SReal. 0 < r --> abs x < r}"
+
+  HFinite :: "hypreal set"
+   "HFinite == {x. EX r: SReal. abs x < r}"
+
+  HInfinite :: "hypreal set"
+   "HInfinite == {x. ALL r: SReal. r < abs x}"
+
+  (* standard part map *)
+  st        :: hypreal => hypreal
+   "st           == (%x. @r. x : HFinite & r:SReal & r @= x)"
+
+  monad     :: hypreal => hypreal set
+   "monad x      == {y. x @= y}"
+
+  galaxy    :: hypreal => hypreal set
+   "galaxy x     == {y. (x + -y) : HFinite}"
+ 
+  (* infinitely close *)
+  inf_close :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
+   "x @= y       == (x + -y) : Infinitesimal"     
+
+
+defs  
+
+   (*standard real numbers as a subset of the hyperreals*)
+   SReal_def      "SReal == {x. EX r. x = hypreal_of_real r}"
+
+syntax (symbols)
+    inf_close :: "[hypreal, hypreal] => bool"    (infixl "\\<approx>" 50)
+  
+end
+
+
+
+