25 (* nonstandard extension of function *) |
25 (* nonstandard extension of function *) |
26 is_starext :: "['a star => 'a star, 'a => 'a] => bool" |
26 is_starext :: "['a star => 'a star, 'a => 'a] => bool" |
27 "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). |
27 "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y). |
28 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" |
28 ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))" |
29 |
29 |
30 starfun :: "('a => 'a) => 'a star => 'a star" ("*f* _" [80] 80) |
30 starfun :: "('a => 'b) => 'a star => 'b star" ("*f* _" [80] 80) |
31 "*f* f == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. f(X n)}))" |
31 "*f* f == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. f(X n)}))" |
32 |
32 |
33 (* internal functions *) |
33 (* internal functions *) |
34 starfun_n :: "(nat => ('a => 'a)) => 'a star => 'a star" |
34 starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star" |
35 ("*fn* _" [80] 80) |
35 ("*fn* _" [80] 80) |
36 "*fn* F == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. (F n)(X n)}))" |
36 "*fn* F == (%x. Abs_star(\<Union>X \<in> Rep_star(x). starrel``{%n. (F n)(X n)}))" |
37 |
37 |
38 InternalFuns :: "('a star => 'a star) set" |
38 InternalFuns :: "('a star => 'b star) set" |
39 "InternalFuns == {X. \<exists>F. X = *fn* F}" |
39 "InternalFuns == {X. \<exists>F. X = *fn* F}" |
40 |
40 |
41 |
41 |
42 |
42 |
43 (*-------------------------------------------------------- |
43 (*-------------------------------------------------------- |
53 apply (blast intro: LeastI) |
53 apply (blast intro: LeastI) |
54 done |
54 done |
55 |
55 |
56 subsection{*Properties of the Star-transform Applied to Sets of Reals*} |
56 subsection{*Properties of the Star-transform Applied to Sets of Reals*} |
57 |
57 |
58 lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)" |
58 lemma STAR_real_set: "*s*(UNIV::'a set) = (UNIV::'a star set)" |
59 by (simp add: starset_def) |
59 by (simp add: starset_def) |
60 declare STAR_real_set [simp] |
60 declare STAR_real_set [simp] |
61 |
61 |
62 lemma STAR_empty_set: "*s* {} = {}" |
62 lemma STAR_empty_set: "*s* {} = {}" |
63 by (simp add: starset_def) |
63 by (simp add: starset_def) |