--- /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
+
+
+
+