src/HOL/Hyperreal/Star.thy

even more theories from Jacques

(*  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