1 (* Title : NatStar.thy |
1 (* Title : NatStar.thy |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 1998 University of Cambridge |
3 Copyright : 1998 University of Cambridge |
4 Description : defining *-transforms in NSA which extends |
4 |
5 sets of reals, and nat=>real, nat=>nat functions |
5 Converted to Isar and polished by lcp |
6 *) |
6 *) |
7 |
7 |
8 NatStar = RealPow + HyperPow + |
8 header{*Star-transforms for the Hypernaturals*} |
|
9 |
|
10 theory NatStar = RealPow + HyperPow: |
|
11 |
|
12 |
|
13 text{*Extends sets of nats, and functions from the nats to nats or reals*} |
|
14 |
9 |
15 |
10 constdefs |
16 constdefs |
11 |
17 |
12 (* internal sets and nonstandard extensions -- see Star.thy as well *) |
18 (* internal sets and nonstandard extensions -- see Star.thy as well *) |
13 |
19 |
14 starsetNat :: nat set => hypnat set ("*sNat* _" [80] 80) |
20 starsetNat :: "nat set => hypnat set" ("*sNat* _" [80] 80) |
15 "*sNat* A == {x. ALL X: Rep_hypnat(x). {n::nat. X n : A}: FreeUltrafilterNat}" |
21 "*sNat* A == |
16 |
22 {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> A}: FreeUltrafilterNat}" |
17 starsetNat_n :: (nat => nat set) => hypnat set ("*sNatn* _" [80] 80) |
23 |
18 "*sNatn* As == {x. ALL X: Rep_hypnat(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}" |
24 starsetNat_n :: "(nat => nat set) => hypnat set" ("*sNatn* _" [80] 80) |
19 |
25 "*sNatn* As == |
20 InternalNatSets :: "hypnat set set" |
26 {x. \<forall>X\<in>Rep_hypnat(x). {n::nat. X n \<in> (As n)}: FreeUltrafilterNat}" |
21 "InternalNatSets == {X. EX As. X = *sNatn* As}" |
27 |
|
28 InternalNatSets :: "hypnat set set" |
|
29 "InternalNatSets == {X. \<exists>As. X = *sNatn* As}" |
22 |
30 |
23 (* star transform of functions f:Nat --> Real *) |
31 (* star transform of functions f:Nat --> Real *) |
24 |
32 |
25 starfunNat :: (nat => real) => hypnat => hypreal ("*fNat* _" [80] 80) |
33 starfunNat :: "(nat => real) => hypnat => hypreal" |
26 "*fNat* f == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. f (X n)}))" |
34 ("*fNat* _" [80] 80) |
27 |
35 "*fNat* f == (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. f (X n)}))" |
28 starfunNat_n :: (nat => (nat => real)) => hypnat => hypreal ("*fNatn* _" [80] 80) |
36 |
29 "*fNatn* F == (%x. Abs_hypreal(UN X: Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))" |
37 starfunNat_n :: "(nat => (nat => real)) => hypnat => hypreal" |
30 |
38 ("*fNatn* _" [80] 80) |
31 InternalNatFuns :: (hypnat => hypreal) set |
39 "*fNatn* F == |
32 "InternalNatFuns == {X. EX F. X = *fNatn* F}" |
40 (%x. Abs_hypreal(\<Union>X\<in>Rep_hypnat(x). hyprel``{%n. (F n)(X n)}))" |
|
41 |
|
42 InternalNatFuns :: "(hypnat => hypreal) set" |
|
43 "InternalNatFuns == {X. \<exists>F. X = *fNatn* F}" |
33 |
44 |
34 (* star transform of functions f:Nat --> Nat *) |
45 (* star transform of functions f:Nat --> Nat *) |
35 |
46 |
36 starfunNat2 :: (nat => nat) => hypnat => hypnat ("*fNat2* _" [80] 80) |
47 starfunNat2 :: "(nat => nat) => hypnat => hypnat" |
37 "*fNat2* f == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. f (X n)}))" |
48 ("*fNat2* _" [80] 80) |
38 |
49 "*fNat2* f == %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. f (X n)})" |
39 starfunNat2_n :: (nat => (nat => nat)) => hypnat => hypnat ("*fNat2n* _" [80] 80) |
50 |
40 "*fNat2n* F == (%x. Abs_hypnat(UN X: Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)}))" |
51 starfunNat2_n :: "(nat => (nat => nat)) => hypnat => hypnat" |
41 |
52 ("*fNat2n* _" [80] 80) |
42 InternalNatFuns2 :: (hypnat => hypnat) set |
53 "*fNat2n* F == |
43 "InternalNatFuns2 == {X. EX F. X = *fNat2n* F}" |
54 %x. Abs_hypnat(\<Union>X\<in>Rep_hypnat(x). hypnatrel``{%n. (F n)(X n)})" |
|
55 |
|
56 InternalNatFuns2 :: "(hypnat => hypnat) set" |
|
57 "InternalNatFuns2 == {X. \<exists>F. X = *fNat2n* F}" |
|
58 |
|
59 |
|
60 lemma NatStar_real_set: "*sNat*(UNIV::nat set) = (UNIV::hypnat set)" |
|
61 by (simp add: starsetNat_def) |
|
62 |
|
63 lemma NatStar_empty_set [simp]: "*sNat* {} = {}" |
|
64 by (simp add: starsetNat_def) |
|
65 |
|
66 lemma NatStar_Un: "*sNat* (A Un B) = *sNat* A Un *sNat* B" |
|
67 apply (auto simp add: starsetNat_def) |
|
68 prefer 2 apply (blast intro: FreeUltrafilterNat_subset) |
|
69 prefer 2 apply (blast intro: FreeUltrafilterNat_subset) |
|
70 apply (drule FreeUltrafilterNat_Compl_mem) |
|
71 apply (drule bspec, assumption) |
|
72 apply (rule_tac z = x in eq_Abs_hypnat, auto, ultra) |
|
73 done |
|
74 |
|
75 lemma starsetNat_n_Un: "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B" |
|
76 apply (auto simp add: starsetNat_n_def) |
|
77 apply (drule_tac x = Xa in bspec) |
|
78 apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
79 apply (auto dest!: bspec, ultra+) |
|
80 done |
|
81 |
|
82 lemma InternalNatSets_Un: |
|
83 "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |] |
|
84 ==> (X Un Y) \<in> InternalNatSets" |
|
85 by (auto simp add: InternalNatSets_def starsetNat_n_Un [symmetric]) |
|
86 |
|
87 lemma NatStar_Int: "*sNat* (A Int B) = *sNat* A Int *sNat* B" |
|
88 apply (auto simp add: starsetNat_def) |
|
89 prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset) |
|
90 apply (blast intro: FreeUltrafilterNat_subset)+ |
|
91 done |
|
92 |
|
93 lemma starsetNat_n_Int: |
|
94 "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B" |
|
95 apply (auto simp add: starsetNat_n_def) |
|
96 apply (auto dest!: bspec, ultra+) |
|
97 done |
|
98 |
|
99 lemma InternalNatSets_Int: |
|
100 "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |] |
|
101 ==> (X Int Y) \<in> InternalNatSets" |
|
102 by (auto simp add: InternalNatSets_def starsetNat_n_Int [symmetric]) |
|
103 |
|
104 lemma NatStar_Compl: "*sNat* (-A) = -( *sNat* A)" |
|
105 apply (auto simp add: starsetNat_def) |
|
106 apply (rule_tac z = x in eq_Abs_hypnat) |
|
107 apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
108 apply (auto dest!: bspec, ultra+) |
|
109 done |
|
110 |
|
111 lemma starsetNat_n_Compl: "*sNatn* ((%n. - A n)) = -( *sNatn* A)" |
|
112 apply (auto simp add: starsetNat_n_def) |
|
113 apply (rule_tac z = x in eq_Abs_hypnat) |
|
114 apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
115 apply (auto dest!: bspec, ultra+) |
|
116 done |
|
117 |
|
118 lemma InternalNatSets_Compl: "X \<in> InternalNatSets ==> -X \<in> InternalNatSets" |
|
119 by (auto simp add: InternalNatSets_def starsetNat_n_Compl [symmetric]) |
|
120 |
|
121 lemma starsetNat_n_diff: "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B" |
|
122 apply (auto simp add: starsetNat_n_def) |
|
123 apply (rule_tac [2] z = x in eq_Abs_hypnat) |
|
124 apply (rule_tac [3] z = x in eq_Abs_hypnat) |
|
125 apply (auto dest!: bspec, ultra+) |
|
126 done |
|
127 |
|
128 lemma InternalNatSets_diff: |
|
129 "[| X \<in> InternalNatSets; Y \<in> InternalNatSets |] |
|
130 ==> (X - Y) \<in> InternalNatSets" |
|
131 by (auto simp add: InternalNatSets_def starsetNat_n_diff [symmetric]) |
|
132 |
|
133 lemma NatStar_subset: "A \<le> B ==> *sNat* A \<le> *sNat* B" |
|
134 apply (simp add: starsetNat_def) |
|
135 apply (blast intro: FreeUltrafilterNat_subset) |
|
136 done |
|
137 |
|
138 lemma NatStar_mem: "a \<in> A ==> hypnat_of_nat a \<in> *sNat* A" |
|
139 by (auto intro: FreeUltrafilterNat_subset |
|
140 simp add: starsetNat_def hypnat_of_nat_eq) |
|
141 |
|
142 lemma NatStar_hypreal_of_real_image_subset: "hypnat_of_nat ` A \<le> *sNat* A" |
|
143 apply (auto simp add: starsetNat_def hypnat_of_nat_eq) |
|
144 apply (blast intro: FreeUltrafilterNat_subset) |
|
145 done |
|
146 |
|
147 lemma NatStar_SHNat_subset: "Nats \<le> *sNat* (UNIV:: nat set)" |
|
148 by (simp add: starsetNat_def SHNat_eq hypnat_of_nat_eq) |
|
149 |
|
150 lemma NatStar_hypreal_of_real_Int: |
|
151 "*sNat* X Int Nats = hypnat_of_nat ` X" |
|
152 apply (auto simp add: starsetNat_def hypnat_of_nat_eq SHNat_eq) |
|
153 apply (simp add: hypnat_of_nat_eq [symmetric]) |
|
154 apply (rule imageI, rule ccontr) |
|
155 apply (drule bspec) |
|
156 apply (rule lemma_hypnatrel_refl) |
|
157 prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto) |
|
158 done |
|
159 |
|
160 lemma starsetNat_starsetNat_n_eq: "*sNat* X = *sNatn* (%n. X)" |
|
161 by (simp add: starsetNat_n_def starsetNat_def) |
|
162 |
|
163 lemma InternalNatSets_starsetNat_n [simp]: "( *sNat* X) \<in> InternalNatSets" |
|
164 by (auto simp add: InternalNatSets_def starsetNat_starsetNat_n_eq) |
|
165 |
|
166 lemma InternalNatSets_UNIV_diff: |
|
167 "X \<in> InternalNatSets ==> UNIV - X \<in> InternalNatSets" |
|
168 by (auto intro: InternalNatSets_Compl) |
|
169 |
|
170 text{*Nonstandard extension of a set (defined using a constant |
|
171 sequence) as a special case of an internal set*} |
|
172 lemma starsetNat_n_starsetNat: "\<forall>n. (As n = A) ==> *sNatn* As = *sNat* A" |
|
173 by (simp add: starsetNat_n_def starsetNat_def) |
|
174 |
|
175 |
|
176 subsection{*Nonstandard Extensions of Functions*} |
|
177 |
|
178 text{* Nonstandard extension of a function (defined using a constant |
|
179 sequence) as a special case of an internal function*} |
|
180 |
|
181 lemma starfunNat_n_starfunNat: "\<forall>n. (F n = f) ==> *fNatn* F = *fNat* f" |
|
182 by (simp add: starfunNat_n_def starfunNat_def) |
|
183 |
|
184 lemma starfunNat2_n_starfunNat2: "\<forall>n. (F n = f) ==> *fNat2n* F = *fNat2* f" |
|
185 by (simp add: starfunNat2_n_def starfunNat2_def) |
|
186 |
|
187 lemma starfunNat_congruent: |
|
188 "congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})" |
|
189 apply (simp add: congruent_def, safe) |
|
190 apply (ultra+) |
|
191 done |
|
192 |
|
193 (* f::nat=>real *) |
|
194 lemma starfunNat: |
|
195 "( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = |
|
196 Abs_hypreal(hyprel `` {%n. f (X n)})" |
|
197 apply (simp add: starfunNat_def) |
|
198 apply (rule arg_cong [where f = Abs_hypreal]) |
|
199 apply (auto, ultra) |
|
200 done |
|
201 |
|
202 (* f::nat=>nat *) |
|
203 lemma starfunNat2: |
|
204 "( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = |
|
205 Abs_hypnat(hypnatrel `` {%n. f (X n)})" |
|
206 apply (simp add: starfunNat2_def) |
|
207 apply (rule arg_cong [where f = Abs_hypnat]) |
|
208 apply (simp add: hypnatrel_in_hypnat [THEN Abs_hypnat_inverse] |
|
209 UN_equiv_class [OF equiv_hypnatrel starfunNat_congruent]) |
|
210 done |
|
211 |
|
212 subsubsection{*Multiplication: @{text "( *f) x ( *g) = *(f x g)"}*} |
|
213 |
|
214 lemma starfunNat_mult: |
|
215 "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z" |
|
216 apply (rule eq_Abs_hypnat [of z]) |
|
217 apply (simp add: starfunNat hypreal_mult) |
|
218 done |
|
219 |
|
220 lemma starfunNat2_mult: |
|
221 "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z" |
|
222 apply (rule eq_Abs_hypnat [of z]) |
|
223 apply (simp add: starfunNat2 hypnat_mult) |
|
224 done |
|
225 |
|
226 subsubsection{*Addition: @{text "( *f) + ( *g) = *(f + g)"}*} |
|
227 |
|
228 lemma starfunNat_add: |
|
229 "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z" |
|
230 apply (rule eq_Abs_hypnat [of z]) |
|
231 apply (simp add: starfunNat hypreal_add) |
|
232 done |
|
233 |
|
234 lemma starfunNat2_add: |
|
235 "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z" |
|
236 apply (rule eq_Abs_hypnat [of z]) |
|
237 apply (simp add: starfunNat2 hypnat_add) |
|
238 done |
|
239 |
|
240 lemma starfunNat2_minus: |
|
241 "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z" |
|
242 apply (rule eq_Abs_hypnat [of z]) |
|
243 apply (simp add: starfunNat2 hypnat_minus) |
|
244 done |
|
245 |
|
246 subsubsection{*Composition: @{text "( *f) o ( *g) = *(f o g)"}*} |
|
247 |
|
248 (***** ( *f::nat=>real) o ( *g::nat=>nat) = *(f o g) *****) |
|
249 |
|
250 lemma starfunNatNat2_o: |
|
251 "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))" |
|
252 apply (rule ext) |
|
253 apply (rule_tac z = x in eq_Abs_hypnat) |
|
254 apply (simp add: starfunNat2 starfunNat) |
|
255 done |
|
256 |
|
257 lemma starfunNatNat2_o2: |
|
258 "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))" |
|
259 apply (insert starfunNatNat2_o [of f g]) |
|
260 apply (simp add: o_def) |
|
261 done |
|
262 |
|
263 (***** ( *f::nat=>nat) o ( *g::nat=>nat) = *(f o g) *****) |
|
264 lemma starfunNat2_o: "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))" |
|
265 apply (rule ext) |
|
266 apply (rule_tac z = x in eq_Abs_hypnat) |
|
267 apply (simp add: starfunNat2) |
|
268 done |
|
269 |
|
270 (***** ( *f::real=>real) o ( *g::nat=>real) = *(f o g) *****) |
|
271 |
|
272 lemma starfun_stafunNat_o: "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))" |
|
273 apply (rule ext) |
|
274 apply (rule_tac z = x in eq_Abs_hypnat) |
|
275 apply (simp add: starfunNat starfun) |
|
276 done |
|
277 |
|
278 lemma starfun_stafunNat_o2: |
|
279 "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))" |
|
280 apply (insert starfun_stafunNat_o [of f g]) |
|
281 apply (simp add: o_def) |
|
282 done |
|
283 |
|
284 |
|
285 text{*NS extension of constant function*} |
|
286 |
|
287 lemma starfunNat_const_fun [simp]: "( *fNat* (%x. k)) z = hypreal_of_real k" |
|
288 apply (rule eq_Abs_hypnat [of z]) |
|
289 apply (simp add: starfunNat hypreal_of_real_def) |
|
290 done |
|
291 |
|
292 lemma starfunNat2_const_fun [simp]: "( *fNat2* (%x. k)) z = hypnat_of_nat k" |
|
293 apply (rule eq_Abs_hypnat [of z]) |
|
294 apply (simp add: starfunNat2 hypnat_of_nat_eq) |
|
295 done |
|
296 |
|
297 lemma starfunNat_minus: "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x" |
|
298 apply (rule eq_Abs_hypnat [of x]) |
|
299 apply (simp add: starfunNat hypreal_minus) |
|
300 done |
|
301 |
|
302 lemma starfunNat_inverse: |
|
303 "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x" |
|
304 apply (rule eq_Abs_hypnat [of x]) |
|
305 apply (simp add: starfunNat hypreal_inverse) |
|
306 done |
|
307 |
|
308 text{* Extended function has same solution as its standard |
|
309 version for natural arguments. i.e they are the same |
|
310 for all natural arguments (c.f. Hoskins pg. 107- SEQ)*} |
|
311 |
|
312 lemma starfunNat_eq [simp]: |
|
313 "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)" |
|
314 by (simp add: starfunNat hypnat_of_nat_eq hypreal_of_real_def) |
|
315 |
|
316 lemma starfunNat2_eq [simp]: |
|
317 "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)" |
|
318 by (simp add: starfunNat2 hypnat_of_nat_eq) |
|
319 |
|
320 lemma starfunNat_approx: |
|
321 "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)" |
|
322 by auto |
|
323 |
|
324 |
|
325 text{* Example of transfer of a property from reals to hyperreals |
|
326 --- used for limit comparison of sequences*} |
|
327 |
|
328 lemma starfun_le_mono: |
|
329 "\<forall>n. N \<le> n --> f n \<le> g n |
|
330 ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n \<le> ( *fNat* g) n" |
|
331 apply safe |
|
332 apply (rule_tac z = n in eq_Abs_hypnat) |
|
333 apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto) |
|
334 done |
|
335 |
|
336 (*****----- and another -----*****) |
|
337 lemma starfun_less_mono: |
|
338 "\<forall>n. N \<le> n --> f n < g n |
|
339 ==> \<forall>n. hypnat_of_nat N \<le> n --> ( *fNat* f) n < ( *fNat* g) n" |
|
340 apply safe |
|
341 apply (rule_tac z = n in eq_Abs_hypnat) |
|
342 apply (auto simp add: starfunNat hypnat_of_nat_eq hypreal_le hypreal_less hypnat_le hypnat_less, ultra, auto) |
|
343 done |
|
344 |
|
345 text{*Nonstandard extension when we increment the argument by one*} |
|
346 |
|
347 lemma starfunNat_shift_one: |
|
348 "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))" |
|
349 apply (rule eq_Abs_hypnat [of N]) |
|
350 apply (simp add: starfunNat hypnat_one_def hypnat_add) |
|
351 done |
|
352 |
|
353 text{*Nonstandard extension with absolute value*} |
|
354 |
|
355 lemma starfunNat_rabs: "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)" |
|
356 apply (rule eq_Abs_hypnat [of N]) |
|
357 apply (simp add: starfunNat hypreal_hrabs) |
|
358 done |
|
359 |
|
360 text{*The hyperpow function as a nonstandard extension of realpow*} |
|
361 |
|
362 lemma starfunNat_pow: "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N" |
|
363 apply (rule eq_Abs_hypnat [of N]) |
|
364 apply (simp add: hyperpow hypreal_of_real_def starfunNat) |
|
365 done |
|
366 |
|
367 lemma starfunNat_pow2: |
|
368 "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m" |
|
369 apply (rule eq_Abs_hypnat [of N]) |
|
370 apply (simp add: hyperpow hypnat_of_nat_eq starfunNat) |
|
371 done |
|
372 |
|
373 lemma starfun_pow: "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n" |
|
374 apply (rule_tac z = R in eq_Abs_hypreal) |
|
375 apply (simp add: hyperpow starfun hypnat_of_nat_eq) |
|
376 done |
|
377 |
|
378 text{*The @{term hypreal_of_hypnat} function as a nonstandard extension of |
|
379 @{term real_of_nat} *} |
|
380 |
|
381 lemma starfunNat_real_of_nat: "( *fNat* real) = hypreal_of_hypnat" |
|
382 apply (rule ext) |
|
383 apply (rule_tac z = x in eq_Abs_hypnat) |
|
384 apply (simp add: hypreal_of_hypnat starfunNat) |
|
385 done |
|
386 |
|
387 lemma starfunNat_inverse_real_of_nat_eq: |
|
388 "N \<in> HNatInfinite |
|
389 ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)" |
|
390 apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst]) |
|
391 apply (subgoal_tac "hypreal_of_hypnat N ~= 0") |
|
392 apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat starfun_inverse_inverse) |
|
393 done |
|
394 |
|
395 text{*Internal functions - some redundancy with *fNat* now*} |
|
396 |
|
397 lemma starfunNat_n_congruent: |
|
398 "congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})" |
|
399 apply (simp add: congruent_def, safe) |
|
400 apply (ultra+) |
|
401 done |
|
402 |
|
403 lemma starfunNat_n: |
|
404 "( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = |
|
405 Abs_hypreal(hyprel `` {%n. f n (X n)})" |
|
406 apply (simp add: starfunNat_n_def) |
|
407 apply (rule_tac f = Abs_hypreal in arg_cong, auto, ultra) |
|
408 done |
|
409 |
|
410 text{*Multiplication: @{text "( *fn) x ( *gn) = *(fn x gn)"}*} |
|
411 |
|
412 lemma starfunNat_n_mult: |
|
413 "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z" |
|
414 apply (rule eq_Abs_hypnat [of z]) |
|
415 apply (simp add: starfunNat_n hypreal_mult) |
|
416 done |
|
417 |
|
418 text{*Addition: @{text "( *fn) + ( *gn) = *(fn + gn)"}*} |
|
419 |
|
420 lemma starfunNat_n_add: |
|
421 "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z" |
|
422 apply (rule eq_Abs_hypnat [of z]) |
|
423 apply (simp add: starfunNat_n hypreal_add) |
|
424 done |
|
425 |
|
426 text{*Subtraction: @{text "( *fn) - ( *gn) = *(fn + - gn)"}*} |
|
427 |
|
428 lemma starfunNat_n_add_minus: |
|
429 "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z" |
|
430 apply (rule eq_Abs_hypnat [of z]) |
|
431 apply (simp add: starfunNat_n hypreal_minus hypreal_add) |
|
432 done |
|
433 |
|
434 |
|
435 text{*Composition: @{text "( *fn) o ( *gn) = *(fn o gn)"}*} |
|
436 |
|
437 lemma starfunNat_n_const_fun [simp]: |
|
438 "( *fNatn* (%i x. k)) z = hypreal_of_real k" |
|
439 apply (rule eq_Abs_hypnat [of z]) |
|
440 apply (simp add: starfunNat_n hypreal_of_real_def) |
|
441 done |
|
442 |
|
443 lemma starfunNat_n_minus: "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x" |
|
444 apply (rule eq_Abs_hypnat [of x]) |
|
445 apply (simp add: starfunNat_n hypreal_minus) |
|
446 done |
|
447 |
|
448 lemma starfunNat_n_eq [simp]: |
|
449 "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})" |
|
450 by (simp add: starfunNat_n hypnat_of_nat_eq) |
|
451 |
|
452 lemma starfun_eq_iff: "(( *fNat* f) = ( *fNat* g)) = (f = g)" |
|
453 apply auto |
|
454 apply (rule ext, rule ccontr) |
|
455 apply (drule_tac x = "hypnat_of_nat (x) " in fun_cong) |
|
456 apply (simp add: starfunNat hypnat_of_nat_eq) |
|
457 done |
|
458 |
|
459 |
|
460 lemma starfunNat_inverse_real_of_nat_Infinitesimal [simp]: |
|
461 "N \<in> HNatInfinite ==> ( *fNat* (%x. inverse (real x))) N \<in> Infinitesimal" |
|
462 apply (rule_tac f1 = inverse in starfun_stafunNat_o2 [THEN subst]) |
|
463 apply (subgoal_tac "hypreal_of_hypnat N ~= 0") |
|
464 apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat) |
|
465 done |
|
466 |
|
467 ML |
|
468 {* |
|
469 val starsetNat_def = thm "starsetNat_def"; |
|
470 |
|
471 val NatStar_real_set = thm "NatStar_real_set"; |
|
472 val NatStar_empty_set = thm "NatStar_empty_set"; |
|
473 val NatStar_Un = thm "NatStar_Un"; |
|
474 val starsetNat_n_Un = thm "starsetNat_n_Un"; |
|
475 val InternalNatSets_Un = thm "InternalNatSets_Un"; |
|
476 val NatStar_Int = thm "NatStar_Int"; |
|
477 val starsetNat_n_Int = thm "starsetNat_n_Int"; |
|
478 val InternalNatSets_Int = thm "InternalNatSets_Int"; |
|
479 val NatStar_Compl = thm "NatStar_Compl"; |
|
480 val starsetNat_n_Compl = thm "starsetNat_n_Compl"; |
|
481 val InternalNatSets_Compl = thm "InternalNatSets_Compl"; |
|
482 val starsetNat_n_diff = thm "starsetNat_n_diff"; |
|
483 val InternalNatSets_diff = thm "InternalNatSets_diff"; |
|
484 val NatStar_subset = thm "NatStar_subset"; |
|
485 val NatStar_mem = thm "NatStar_mem"; |
|
486 val NatStar_hypreal_of_real_image_subset = thm "NatStar_hypreal_of_real_image_subset"; |
|
487 val NatStar_SHNat_subset = thm "NatStar_SHNat_subset"; |
|
488 val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int"; |
|
489 val starsetNat_starsetNat_n_eq = thm "starsetNat_starsetNat_n_eq"; |
|
490 val InternalNatSets_starsetNat_n = thm "InternalNatSets_starsetNat_n"; |
|
491 val InternalNatSets_UNIV_diff = thm "InternalNatSets_UNIV_diff"; |
|
492 val starsetNat_n_starsetNat = thm "starsetNat_n_starsetNat"; |
|
493 val starfunNat_n_starfunNat = thm "starfunNat_n_starfunNat"; |
|
494 val starfunNat2_n_starfunNat2 = thm "starfunNat2_n_starfunNat2"; |
|
495 val starfunNat_congruent = thm "starfunNat_congruent"; |
|
496 val starfunNat = thm "starfunNat"; |
|
497 val starfunNat2 = thm "starfunNat2"; |
|
498 val starfunNat_mult = thm "starfunNat_mult"; |
|
499 val starfunNat2_mult = thm "starfunNat2_mult"; |
|
500 val starfunNat_add = thm "starfunNat_add"; |
|
501 val starfunNat2_add = thm "starfunNat2_add"; |
|
502 val starfunNat2_minus = thm "starfunNat2_minus"; |
|
503 val starfunNatNat2_o = thm "starfunNatNat2_o"; |
|
504 val starfunNatNat2_o2 = thm "starfunNatNat2_o2"; |
|
505 val starfunNat2_o = thm "starfunNat2_o"; |
|
506 val starfun_stafunNat_o = thm "starfun_stafunNat_o"; |
|
507 val starfun_stafunNat_o2 = thm "starfun_stafunNat_o2"; |
|
508 val starfunNat_const_fun = thm "starfunNat_const_fun"; |
|
509 val starfunNat2_const_fun = thm "starfunNat2_const_fun"; |
|
510 val starfunNat_minus = thm "starfunNat_minus"; |
|
511 val starfunNat_inverse = thm "starfunNat_inverse"; |
|
512 val starfunNat_eq = thm "starfunNat_eq"; |
|
513 val starfunNat2_eq = thm "starfunNat2_eq"; |
|
514 val starfunNat_approx = thm "starfunNat_approx"; |
|
515 val starfun_le_mono = thm "starfun_le_mono"; |
|
516 val starfun_less_mono = thm "starfun_less_mono"; |
|
517 val starfunNat_shift_one = thm "starfunNat_shift_one"; |
|
518 val starfunNat_rabs = thm "starfunNat_rabs"; |
|
519 val starfunNat_pow = thm "starfunNat_pow"; |
|
520 val starfunNat_pow2 = thm "starfunNat_pow2"; |
|
521 val starfun_pow = thm "starfun_pow"; |
|
522 val starfunNat_real_of_nat = thm "starfunNat_real_of_nat"; |
|
523 val starfunNat_inverse_real_of_nat_eq = thm "starfunNat_inverse_real_of_nat_eq"; |
|
524 val starfunNat_n_congruent = thm "starfunNat_n_congruent"; |
|
525 val starfunNat_n = thm "starfunNat_n"; |
|
526 val starfunNat_n_mult = thm "starfunNat_n_mult"; |
|
527 val starfunNat_n_add = thm "starfunNat_n_add"; |
|
528 val starfunNat_n_add_minus = thm "starfunNat_n_add_minus"; |
|
529 val starfunNat_n_const_fun = thm "starfunNat_n_const_fun"; |
|
530 val starfunNat_n_minus = thm "starfunNat_n_minus"; |
|
531 val starfunNat_n_eq = thm "starfunNat_n_eq"; |
|
532 val starfun_eq_iff = thm "starfun_eq_iff"; |
|
533 val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal"; |
|
534 *} |
|
535 |
44 end |
536 end |
45 |
537 |
46 |
538 |