15 starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80) where |
15 starset_n :: "(nat => 'a set) => 'a star set" ("*sn* _" [80] 80) where |
16 "*sn* As = Iset (star_n As)" |
16 "*sn* As = Iset (star_n As)" |
17 |
17 |
18 definition |
18 definition |
19 InternalSets :: "'a star set set" where |
19 InternalSets :: "'a star set set" where |
20 [code del]: "InternalSets = {X. \<exists>As. X = *sn* As}" |
20 "InternalSets = {X. \<exists>As. X = *sn* As}" |
21 |
21 |
22 definition |
22 definition |
23 (* nonstandard extension of function *) |
23 (* nonstandard extension of function *) |
24 is_starext :: "['a star => 'a star, 'a => 'a] => bool" where |
24 is_starext :: "['a star => 'a star, 'a => 'a] => bool" where |
25 [code del]: "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). |
25 "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). |
26 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" |
26 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" |
27 |
27 |
28 definition |
28 definition |
29 (* internal functions *) |
29 (* internal functions *) |
30 starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star" ("*fn* _" [80] 80) where |
30 starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star" ("*fn* _" [80] 80) where |
31 "*fn* F = Ifun (star_n F)" |
31 "*fn* F = Ifun (star_n F)" |
32 |
32 |
33 definition |
33 definition |
34 InternalFuns :: "('a star => 'b star) set" where |
34 InternalFuns :: "('a star => 'b star) set" where |
35 [code del]:"InternalFuns = {X. \<exists>F. X = *fn* F}" |
35 "InternalFuns = {X. \<exists>F. X = *fn* F}" |
36 |
36 |
37 |
37 |
38 (*-------------------------------------------------------- |
38 (*-------------------------------------------------------- |
39 Preamble - Pulling "EX" over "ALL" |
39 Preamble - Pulling "EX" over "ALL" |
40 ---------------------------------------------------------*) |
40 ---------------------------------------------------------*) |