author | wenzelm |
Wed, 29 Aug 2001 21:17:24 +0200 | |
changeset 11506 | 244a02a2968b |
parent 10834 | a7897aebbffc |
child 14415 | 60aa114e2dba |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : NatStar.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
4 |
Description : defining *-transforms in NSA which extends |
|
5 |
sets of reals, and nat=>real, nat=>nat functions |
|
6 |
*) |
|
7 |
||
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
8 |
NatStar = RealPow + HyperPow + |
10751 | 9 |
|
10 |
constdefs |
|
11 |
||
12 |
(* internal sets and nonstandard extensions -- see Star.thy as well *) |
|
13 |
||
14 |
starsetNat :: nat set => hypnat set ("*sNat* _" [80] 80) |
|
15 |
"*sNat* A == {x. ALL X: Rep_hypnat(x). {n::nat. X n : A}: FreeUltrafilterNat}" |
|
16 |
||
17 |
starsetNat_n :: (nat => nat set) => hypnat set ("*sNatn* _" [80] 80) |
|
18 |
"*sNatn* As == {x. ALL X: Rep_hypnat(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}" |
|
19 |
||
20 |
InternalNatSets :: "hypnat set set" |
|
21 |
"InternalNatSets == {X. EX As. X = *sNatn* As}" |
|
22 |
||
23 |
(* star transform of functions f:Nat --> Real *) |
|
24 |
||
25 |
starfunNat :: (nat => real) => hypnat => hypreal ("*fNat* _" [80] 80) |
|
10834 | 26 |
"*fNat* f == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. f (X n)}))" |
10751 | 27 |
|
28 |
starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal ("*fNatn* _" [80] 80) |
|
10834 | 29 |
"*fNatn* F == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))" |
10751 | 30 |
|
31 |
InternalNatFuns :: (hypnat => hypreal) set |
|
32 |
"InternalNatFuns == {X. EX F. X = *fNatn* F}" |
|
33 |
||
34 |
(* star transform of functions f:Nat --> Nat *) |
|
35 |
||
36 |
starfunNat2 :: (nat => nat) => hypnat => hypnat ("*fNat2* _" [80] 80) |
|
10834 | 37 |
"*fNat2* f == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. f (X n)}))" |
10751 | 38 |
|
39 |
starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat ("*fNat2n* _" [80] 80) |
|
10834 | 40 |
"*fNat2n* F == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)}))" |
10751 | 41 |
|
42 |
InternalNatFuns2 :: (hypnat => hypnat) set |
|
43 |
"InternalNatFuns2 == {X. EX F. X = *fNat2n* F}" |
|
44 |
end |
|
45 |
||
46 |