src/HOL/Hyperreal/Star.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/Star.thy	Sat Dec 30 22:03:47 2000 +0100
@@ -0,0 +1,39 @@
+(*  Title       : Star.thy
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Description : defining *-transforms in NSA which extends sets of reals, 
+                  and real=>real functions
+*) 
+
+Star = NSA +
+
+constdefs
+    (* nonstandard extension of sets *)
+    starset :: real set => hypreal set          ("*s* _" [80] 80)
+    "*s* A  == {x. ALL X: Rep_hypreal(x). {n::nat. X n : A}: FreeUltrafilterNat}"
+
+    (* internal sets *)
+    starset_n :: (nat => real set) => hypreal set        ("*sn* _" [80] 80)
+    "*sn* As  == {x. ALL X: Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"   
+    
+    InternalSets :: "hypreal set set"
+    "InternalSets == {X. EX As. X = *sn* As}"
+
+    (* nonstandard extension of function *)
+    is_starext  ::  [hypreal => hypreal, real => real] => bool
+    "is_starext F f == (ALL x y. EX X: Rep_hypreal(x). EX Y: Rep_hypreal(y).
+                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
+    
+    starfun :: (real => real) => hypreal => hypreal        ("*f* _" [80] 80)
+    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. f (X n)}))" 
+
+    (* internal functions *)
+    starfun_n :: (nat => (real => real)) => hypreal => hypreal        ("*fn* _" [80] 80)
+    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. (F n)(X n)}))" 
+
+    InternalFuns :: (hypreal => hypreal) set
+    "InternalFuns == {X. EX F. X = *fn* F}"
+end
+
+
+