src/HOL/Real/Hyperreal/Star.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/Star.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,39 @@
     1.4 +(*  Title       : Star.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : defining *-transforms in NSA which extends sets of reals, 
     1.8 +                  and real=>real functions
     1.9 +*) 
    1.10 +
    1.11 +Star = NSA +
    1.12 +
    1.13 +constdefs
    1.14 +    (* nonstandard extension of sets *)
    1.15 +    starset :: real set => hypreal set          ("*s* _" [80] 80)
    1.16 +    "*s* A  == {x. ALL X: Rep_hypreal(x). {n::nat. X n : A}: FreeUltrafilterNat}"
    1.17 +
    1.18 +    (* internal sets *)
    1.19 +    starset_n :: (nat => real set) => hypreal set        ("*sn* _" [80] 80)
    1.20 +    "*sn* As  == {x. ALL X: Rep_hypreal(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"   
    1.21 +    
    1.22 +    InternalSets :: "hypreal set set"
    1.23 +    "InternalSets == {X. EX As. X = *sn* As}"
    1.24 +
    1.25 +    (* nonstandard extension of function *)
    1.26 +    is_starext  ::  [hypreal => hypreal, real => real] => bool
    1.27 +    "is_starext F f == (ALL x y. EX X: Rep_hypreal(x). EX Y: Rep_hypreal(y).
    1.28 +                        ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
    1.29 +    
    1.30 +    starfun :: (real => real) => hypreal => hypreal        ("*f* _" [80] 80)
    1.31 +    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. f (X n)}))" 
    1.32 +
    1.33 +    (* internal functions *)
    1.34 +    starfun_n :: (nat => (real => real)) => hypreal => hypreal        ("*fn* _" [80] 80)
    1.35 +    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel^^{%n. (F n)(X n)}))" 
    1.36 +
    1.37 +    InternalFuns :: (hypreal => hypreal) set
    1.38 +    "InternalFuns == {X. EX F. X = *fn* F}"
    1.39 +end
    1.40 +
    1.41 +
    1.42 +