src/HOL/Real/Hyperreal/NatStar.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/NatStar.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,46 @@
     1.4 +(*  Title       : NatStar.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : defining *-transforms in NSA which extends 
     1.8 +                  sets of reals, and nat=>real, nat=>nat functions
     1.9 +*) 
    1.10 +
    1.11 +NatStar = HyperNat + RealPow + HyperPow + 
    1.12 +
    1.13 +constdefs
    1.14 +
    1.15 +  (* internal sets and nonstandard extensions -- see Star.thy as well *)
    1.16 +
    1.17 +    starsetNat :: nat set => hypnat set          ("*sNat* _" [80] 80)
    1.18 +    "*sNat* A  == {x. ALL X: Rep_hypnat(x). {n::nat. X n : A}: FreeUltrafilterNat}"
    1.19 +
    1.20 +    starsetNat_n :: (nat => nat set) => hypnat set        ("*sNatn* _" [80] 80)
    1.21 +    "*sNatn* As  == {x. ALL X: Rep_hypnat(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}"   
    1.22 +
    1.23 +    InternalNatSets :: "hypnat set set"
    1.24 +    "InternalNatSets == {X. EX As. X = *sNatn* As}"
    1.25 +
    1.26 +    (* star transform of functions f:Nat --> Real *)
    1.27 +
    1.28 +    starfunNat :: (nat => real) => hypnat => hypreal        ("*fNat* _" [80] 80)
    1.29 +    "*fNat* f  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel^^{%n. f (X n)}))" 
    1.30 +
    1.31 +    starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal        ("*fNatn* _" [80] 80)
    1.32 +    "*fNatn* F  == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel^^{%n. (F n)(X n)}))" 
    1.33 +
    1.34 +    InternalNatFuns :: (hypnat => hypreal) set
    1.35 +    "InternalNatFuns == {X. EX F. X = *fNatn* F}"
    1.36 +
    1.37 +    (* star transform of functions f:Nat --> Nat *)
    1.38 +
    1.39 +    starfunNat2 :: (nat => nat) => hypnat => hypnat        ("*fNat2* _" [80] 80)
    1.40 +    "*fNat2* f  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel^^{%n. f (X n)}))" 
    1.41 +
    1.42 +    starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat        ("*fNat2n* _" [80] 80)
    1.43 +    "*fNat2n* F  == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel^^{%n. (F n)(X n)}))" 
    1.44 +
    1.45 +    InternalNatFuns2 :: (hypnat => hypnat) set
    1.46 +    "InternalNatFuns2 == {X. EX F. X = *fNat2n* F}"
    1.47 +end
    1.48 +
    1.49 +