|
1 (* Title : NatStar.ML |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : *-transforms in NSA which extends |
|
5 sets of reals, and nat=>real, |
|
6 nat=>nat functions |
|
7 *) |
|
8 |
|
9 Goalw [starsetNat_def] |
|
10 "*sNat*(UNIV::nat set) = (UNIV::hypnat set)"; |
|
11 by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set])); |
|
12 qed "NatStar_real_set"; |
|
13 |
|
14 Goalw [starsetNat_def] "*sNat* {} = {}"; |
|
15 by (Step_tac 1); |
|
16 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
17 by (dres_inst_tac [("x","%n. xa n")] bspec 1); |
|
18 by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_empty])); |
|
19 qed "NatStar_empty_set"; |
|
20 |
|
21 Addsimps [NatStar_empty_set]; |
|
22 |
|
23 Goalw [starsetNat_def] |
|
24 "*sNat* (A Un B) = *sNat* A Un *sNat* B"; |
|
25 by (Auto_tac); |
|
26 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2)); |
|
27 by (dtac FreeUltrafilterNat_Compl_mem 1); |
|
28 by (dtac bspec 1 THEN assume_tac 1); |
|
29 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
30 by (Auto_tac); |
|
31 by (Fuf_tac 1); |
|
32 qed "NatStar_Un"; |
|
33 |
|
34 Goalw [starsetNat_n_def] |
|
35 "*sNatn* (%n. (A n) Un (B n)) = *sNatn* A Un *sNatn* B"; |
|
36 by Auto_tac; |
|
37 by (dres_inst_tac [("x","Xa")] bspec 1); |
|
38 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); |
|
39 by (auto_tac (claset() addSDs [bspec], simpset())); |
|
40 by (TRYALL(Ultra_tac)); |
|
41 qed "starsetNat_n_Un"; |
|
42 |
|
43 Goalw [InternalNatSets_def] |
|
44 "[| X : InternalNatSets; Y : InternalNatSets |] \ |
|
45 \ ==> (X Un Y) : InternalNatSets"; |
|
46 by (auto_tac (claset(), |
|
47 simpset() addsimps [starsetNat_n_Un RS sym])); |
|
48 qed "InternalNatSets_Un"; |
|
49 |
|
50 Goalw [starsetNat_def] "*sNat* (A Int B) = *sNat* A Int *sNat* B"; |
|
51 by (Auto_tac); |
|
52 by (blast_tac (claset() addIs [FreeUltrafilterNat_Int, |
|
53 FreeUltrafilterNat_subset]) 3); |
|
54 by (REPEAT(blast_tac (claset() addIs |
|
55 [FreeUltrafilterNat_subset]) 1)); |
|
56 qed "NatStar_Int"; |
|
57 |
|
58 Goalw [starsetNat_n_def] |
|
59 "*sNatn* (%n. (A n) Int (B n)) = *sNatn* A Int *sNatn* B"; |
|
60 by (Auto_tac); |
|
61 by (auto_tac (claset() addSDs [bspec], |
|
62 simpset())); |
|
63 by (TRYALL(Ultra_tac)); |
|
64 qed "starsetNat_n_Int"; |
|
65 |
|
66 Goalw [InternalNatSets_def] |
|
67 "[| X : InternalNatSets; Y : InternalNatSets |] \ |
|
68 \ ==> (X Int Y) : InternalNatSets"; |
|
69 by (auto_tac (claset(), |
|
70 simpset() addsimps [starsetNat_n_Int RS sym])); |
|
71 qed "InternalNatSets_Int"; |
|
72 |
|
73 Goalw [starsetNat_def] "*sNat* (-A) = -(*sNat* A)"; |
|
74 by (Auto_tac); |
|
75 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
76 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); |
|
77 by (REPEAT(Step_tac 1) THEN Auto_tac); |
|
78 by (TRYALL(Ultra_tac)); |
|
79 qed "NatStar_Compl"; |
|
80 |
|
81 Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -(*sNatn* A)"; |
|
82 by (Auto_tac); |
|
83 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
84 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); |
|
85 by (REPEAT(Step_tac 1) THEN Auto_tac); |
|
86 by (TRYALL(Ultra_tac)); |
|
87 qed "starsetNat_n_Compl"; |
|
88 |
|
89 Goalw [InternalNatSets_def] |
|
90 "X :InternalNatSets ==> -X : InternalNatSets"; |
|
91 by (auto_tac (claset(), |
|
92 simpset() addsimps [starsetNat_n_Compl RS sym])); |
|
93 qed "InternalNatSets_Compl"; |
|
94 |
|
95 Goalw [starsetNat_n_def] |
|
96 "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"; |
|
97 by (Auto_tac); |
|
98 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); |
|
99 by (res_inst_tac [("z","x")] eq_Abs_hypnat 3); |
|
100 by (auto_tac (claset() addSDs [bspec], simpset())); |
|
101 by (TRYALL(Ultra_tac)); |
|
102 qed "starsetNat_n_diff"; |
|
103 |
|
104 Goalw [InternalNatSets_def] |
|
105 "[| X : InternalNatSets; Y : InternalNatSets |] \ |
|
106 \ ==> (X - Y) : InternalNatSets"; |
|
107 by (auto_tac (claset(), simpset() addsimps [starsetNat_n_diff RS sym])); |
|
108 qed "InternalNatSets_diff"; |
|
109 |
|
110 Goalw [starsetNat_def] "A <= B ==> *sNat* A <= *sNat* B"; |
|
111 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1)); |
|
112 qed "NatStar_subset"; |
|
113 |
|
114 Goalw [starsetNat_def,hypnat_of_nat_def] |
|
115 "a : A ==> hypnat_of_nat a : *sNat* A"; |
|
116 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset], |
|
117 simpset())); |
|
118 qed "NatStar_mem"; |
|
119 |
|
120 Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A"; |
|
121 by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def])); |
|
122 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1); |
|
123 qed "NatStar_hypreal_of_real_image_subset"; |
|
124 |
|
125 Goal "SHNat <= *sNat* (UNIV:: nat set)"; |
|
126 by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff, |
|
127 NatStar_hypreal_of_real_image_subset]) 1); |
|
128 qed "NatStar_SHNat_subset"; |
|
129 |
|
130 Goalw [starsetNat_def] |
|
131 "*sNat* X Int SHNat = hypnat_of_nat `` X"; |
|
132 by (auto_tac (claset(), |
|
133 simpset() addsimps |
|
134 [hypnat_of_nat_def,SHNat_def])); |
|
135 by (fold_tac [hypnat_of_nat_def]); |
|
136 by (rtac imageI 1 THEN rtac ccontr 1); |
|
137 by (dtac bspec 1); |
|
138 by (rtac lemma_hypnatrel_refl 1); |
|
139 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2); |
|
140 by (Auto_tac); |
|
141 qed "NatStar_hypreal_of_real_Int"; |
|
142 |
|
143 Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y"; |
|
144 by (Auto_tac); |
|
145 qed "lemma_not_hypnatA"; |
|
146 |
|
147 Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)"; |
|
148 by Auto_tac; |
|
149 qed "starsetNat_starsetNat_n_eq"; |
|
150 |
|
151 Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets"; |
|
152 by (auto_tac (claset(), |
|
153 simpset() addsimps [starsetNat_starsetNat_n_eq])); |
|
154 qed "InternalNatSets_starsetNat_n"; |
|
155 Addsimps [InternalNatSets_starsetNat_n]; |
|
156 |
|
157 Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets"; |
|
158 by (auto_tac (claset() addIs [InternalNatSets_Compl], simpset())); |
|
159 qed "InternalNatSets_UNIV_diff"; |
|
160 |
|
161 (*------------------------------------------------------------------ |
|
162 Nonstandard extension of a set (defined using a constant |
|
163 sequence) as a special case of an internal set |
|
164 -----------------------------------------------------------------*) |
|
165 |
|
166 Goalw [starsetNat_n_def,starsetNat_def] |
|
167 "ALL n. (As n = A) ==> *sNatn* As = *sNat* A"; |
|
168 by (Auto_tac); |
|
169 qed "starsetNat_n_starsetNat"; |
|
170 |
|
171 (*------------------------------------------------------ |
|
172 Theorems about nonstandard extensions of functions |
|
173 ------------------------------------------------------*) |
|
174 |
|
175 (*------------------------------------------------------------------ |
|
176 Nonstandard extension of a function (defined using a constant |
|
177 sequence) as a special case of an internal function |
|
178 -----------------------------------------------------------------*) |
|
179 |
|
180 Goalw [starfunNat_n_def,starfunNat_def] |
|
181 "ALL n. (F n = f) ==> *fNatn* F = *fNat* f"; |
|
182 by (Auto_tac); |
|
183 qed "starfunNat_n_starfunNat"; |
|
184 |
|
185 Goalw [starfunNat2_n_def,starfunNat2_def] |
|
186 "ALL n. (F n = f) ==> *fNat2n* F = *fNat2* f"; |
|
187 by (Auto_tac); |
|
188 qed "starfunNat2_n_starfunNat2"; |
|
189 |
|
190 Goalw [congruent_def] |
|
191 "congruent hypnatrel (%X. hypnatrel^^{%n. f (X n)})"; |
|
192 by (safe_tac (claset())); |
|
193 by (ALLGOALS(Fuf_tac)); |
|
194 qed "starfunNat_congruent"; |
|
195 |
|
196 (* f::nat=>real *) |
|
197 Goalw [starfunNat_def] |
|
198 "(*fNat* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \ |
|
199 \ Abs_hypreal(hyprel ^^ {%n. f (X n)})"; |
|
200 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
201 by (simp_tac (simpset() addsimps |
|
202 [hyprel_in_hypreal RS Abs_hypreal_inverse]) 1); |
|
203 by (Auto_tac THEN Fuf_tac 1); |
|
204 qed "starfunNat"; |
|
205 |
|
206 (* f::nat=>nat *) |
|
207 Goalw [starfunNat2_def] |
|
208 "(*fNat2* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \ |
|
209 \ Abs_hypnat(hypnatrel ^^ {%n. f (X n)})"; |
|
210 by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1); |
|
211 by (simp_tac (simpset() addsimps |
|
212 [hypnatrel_in_hypnat RS Abs_hypnat_inverse, |
|
213 [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1); |
|
214 qed "starfunNat2"; |
|
215 |
|
216 (*--------------------------------------------- |
|
217 multiplication: ( *f ) x ( *g ) = *(f x g) |
|
218 ---------------------------------------------*) |
|
219 Goal "(*fNat* f) z * (*fNat* g) z = (*fNat* (%x. f x * g x)) z"; |
|
220 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
221 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult])); |
|
222 qed "starfunNat_mult"; |
|
223 |
|
224 Goal "(*fNat2* f) z * (*fNat2* g) z = (*fNat2* (%x. f x * g x)) z"; |
|
225 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
226 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult])); |
|
227 qed "starfunNat2_mult"; |
|
228 |
|
229 (*--------------------------------------- |
|
230 addition: ( *f ) + ( *g ) = *(f + g) |
|
231 ---------------------------------------*) |
|
232 Goal "(*fNat* f) z + (*fNat* g) z = (*fNat* (%x. f x + g x)) z"; |
|
233 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
234 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add])); |
|
235 qed "starfunNat_add"; |
|
236 |
|
237 Goal "(*fNat2* f) z + (*fNat2* g) z = (*fNat2* (%x. f x + g x)) z"; |
|
238 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
239 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add])); |
|
240 qed "starfunNat2_add"; |
|
241 |
|
242 Goal "(*fNat2* f) z - (*fNat2* g) z = (*fNat2* (%x. f x - g x)) z"; |
|
243 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
244 by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus])); |
|
245 qed "starfunNat2_minus"; |
|
246 |
|
247 (*-------------------------------------- |
|
248 composition: ( *f ) o ( *g ) = *(f o g) |
|
249 ---------------------------------------*) |
|
250 (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****) |
|
251 |
|
252 Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))"; |
|
253 by (rtac ext 1); |
|
254 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
255 by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat])); |
|
256 qed "starfunNatNat2_o"; |
|
257 |
|
258 Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))"; |
|
259 by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1); |
|
260 qed "starfunNatNat2_o2"; |
|
261 |
|
262 (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****) |
|
263 Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))"; |
|
264 by (rtac ext 1); |
|
265 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
266 by (auto_tac (claset(), simpset() addsimps [starfunNat2])); |
|
267 qed "starfunNat2_o"; |
|
268 |
|
269 (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****) |
|
270 |
|
271 Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; |
|
272 by (rtac ext 1); |
|
273 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
274 by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun])); |
|
275 qed "starfun_stafunNat_o"; |
|
276 |
|
277 Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; |
|
278 by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1); |
|
279 qed "starfun_stafunNat_o2"; |
|
280 |
|
281 (*-------------------------------------- |
|
282 NS extension of constant function |
|
283 --------------------------------------*) |
|
284 Goal "(*fNat* (%x. k)) z = hypreal_of_real k"; |
|
285 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
286 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def])); |
|
287 qed "starfunNat_const_fun"; |
|
288 Addsimps [starfunNat_const_fun]; |
|
289 |
|
290 Goal "(*fNat2* (%x. k)) z = hypnat_of_nat k"; |
|
291 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
292 by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def])); |
|
293 qed "starfunNat2_const_fun"; |
|
294 |
|
295 Addsimps [starfunNat2_const_fun]; |
|
296 |
|
297 Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x"; |
|
298 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
299 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus])); |
|
300 qed "starfunNat_minus"; |
|
301 |
|
302 Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x"; |
|
303 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
304 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse])); |
|
305 qed "starfunNat_inverse"; |
|
306 |
|
307 (*-------------------------------------------------------- |
|
308 extented 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 |
|
313 Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"; |
|
314 by (auto_tac (claset(), |
|
315 simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def])); |
|
316 qed "starfunNat_eq"; |
|
317 |
|
318 Addsimps [starfunNat_eq]; |
|
319 |
|
320 Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"; |
|
321 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def])); |
|
322 qed "starfunNat2_eq"; |
|
323 |
|
324 Addsimps [starfunNat2_eq]; |
|
325 |
|
326 Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"; |
|
327 by (Auto_tac); |
|
328 qed "starfunNat_inf_close"; |
|
329 |
|
330 |
|
331 (*----------------------------------------------------------------- |
|
332 Example of transfer of a property from reals to hyperreals |
|
333 --- used for limit comparison of sequences |
|
334 ----------------------------------------------------------------*) |
|
335 Goal "ALL n. N <= n --> f n <= g n \ |
|
336 \ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n"; |
|
337 by (Step_tac 1); |
|
338 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
339 by (auto_tac (claset(), |
|
340 simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le, |
|
341 hypreal_less, hypnat_le,hypnat_less])); |
|
342 by (Ultra_tac 1); |
|
343 by Auto_tac; |
|
344 qed "starfun_le_mono"; |
|
345 |
|
346 (*****----- and another -----*****) |
|
347 Goal "ALL n. N <= n --> f n < g n \ |
|
348 \ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n"; |
|
349 by (Step_tac 1); |
|
350 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
351 by (auto_tac (claset(), |
|
352 simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le, |
|
353 hypreal_less, hypnat_le,hypnat_less])); |
|
354 by (Ultra_tac 1); |
|
355 by Auto_tac; |
|
356 qed "starfun_less_mono"; |
|
357 |
|
358 (*---------------------------------------------------------------- |
|
359 NS extension when we displace argument by one |
|
360 ---------------------------------------------------------------*) |
|
361 Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)"; |
|
362 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
|
363 by (auto_tac (claset(), |
|
364 simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add])); |
|
365 qed "starfunNat_shift_one"; |
|
366 |
|
367 (*---------------------------------------------------------------- |
|
368 NS extension with rabs |
|
369 ---------------------------------------------------------------*) |
|
370 Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)"; |
|
371 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
|
372 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs])); |
|
373 qed "starfunNat_rabs"; |
|
374 |
|
375 (*---------------------------------------------------------------- |
|
376 The hyperpow function as a NS extension of realpow |
|
377 ----------------------------------------------------------------*) |
|
378 Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"; |
|
379 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
|
380 by (auto_tac (claset(), |
|
381 simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat])); |
|
382 qed "starfunNat_pow"; |
|
383 |
|
384 Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m"; |
|
385 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
|
386 by (auto_tac (claset(), |
|
387 simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat])); |
|
388 qed "starfunNat_pow2"; |
|
389 |
|
390 Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"; |
|
391 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
|
392 by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun])); |
|
393 qed "starfun_pow"; |
|
394 |
|
395 (*----------------------------------------------------- |
|
396 hypreal_of_hypnat as NS extension of real_of_nat! |
|
397 -------------------------------------------------------*) |
|
398 Goal "(*fNat* real_of_nat) = hypreal_of_hypnat"; |
|
399 by (rtac ext 1); |
|
400 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
401 by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat])); |
|
402 qed "starfunNat_real_of_nat"; |
|
403 |
|
404 Goal "N : HNatInfinite \ |
|
405 \ ==> (*fNat* (%x. inverse(real_of_nat x))) N = inverse(hypreal_of_hypnat N)"; |
|
406 by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); |
|
407 by (subgoal_tac "hypreal_of_hypnat N ~= #0" 1); |
|
408 by (auto_tac (claset(), |
|
409 simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse])); |
|
410 qed "starfunNat_inverse_real_of_nat_eq"; |
|
411 |
|
412 (*---------------------------------------------------------- |
|
413 Internal functions - some redundancy with *fNat* now |
|
414 ---------------------------------------------------------*) |
|
415 Goalw [congruent_def] |
|
416 "congruent hypnatrel (%X. hypnatrel^^{%n. f n (X n)})"; |
|
417 by (safe_tac (claset())); |
|
418 by (ALLGOALS(Fuf_tac)); |
|
419 qed "starfunNat_n_congruent"; |
|
420 |
|
421 Goalw [starfunNat_n_def] |
|
422 "(*fNatn* f) (Abs_hypnat(hypnatrel^^{%n. X n})) = \ |
|
423 \ Abs_hypreal(hyprel ^^ {%n. f n (X n)})"; |
|
424 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
425 by Auto_tac; |
|
426 by (Ultra_tac 1); |
|
427 qed "starfunNat_n"; |
|
428 |
|
429 (*------------------------------------------------- |
|
430 multiplication: ( *fn ) x ( *gn ) = *(fn x gn) |
|
431 -------------------------------------------------*) |
|
432 Goal "(*fNatn* f) z * (*fNatn* g) z = (*fNatn* (% i x. f i x * g i x)) z"; |
|
433 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
434 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult])); |
|
435 qed "starfunNat_n_mult"; |
|
436 |
|
437 (*----------------------------------------------- |
|
438 addition: ( *fn ) + ( *gn ) = *(fn + gn) |
|
439 -----------------------------------------------*) |
|
440 Goal "(*fNatn* f) z + (*fNatn* g) z = (*fNatn* (%i x. f i x + g i x)) z"; |
|
441 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
442 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add])); |
|
443 qed "starfunNat_n_add"; |
|
444 |
|
445 (*------------------------------------------------- |
|
446 subtraction: ( *fn ) + -( *gn ) = *(fn + -gn) |
|
447 -------------------------------------------------*) |
|
448 Goal "(*fNatn* f) z + -(*fNatn* g) z = (*fNatn* (%i x. f i x + -g i x)) z"; |
|
449 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
450 by (auto_tac (claset(), |
|
451 simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add])); |
|
452 qed "starfunNat_n_add_minus"; |
|
453 |
|
454 (*-------------------------------------------------- |
|
455 composition: ( *fn ) o ( *gn ) = *(fn o gn) |
|
456 -------------------------------------------------*) |
|
457 |
|
458 Goal "(*fNatn* (%i x. k)) z = hypreal_of_real k"; |
|
459 by (res_inst_tac [("z","z")] eq_Abs_hypnat 1); |
|
460 by (auto_tac (claset(), |
|
461 simpset() addsimps [starfunNat_n, hypreal_of_real_def])); |
|
462 qed "starfunNat_n_const_fun"; |
|
463 |
|
464 Addsimps [starfunNat_n_const_fun]; |
|
465 |
|
466 Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x"; |
|
467 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
|
468 by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus])); |
|
469 qed "starfunNat_n_minus"; |
|
470 |
|
471 Goal "(*fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel ^^ {%i. f i n})"; |
|
472 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def])); |
|
473 qed "starfunNat_n_eq"; |
|
474 Addsimps [starfunNat_n_eq]; |
|
475 |
|
476 Goal "((*fNat* f) = (*fNat* g)) = (f = g)"; |
|
477 by Auto_tac; |
|
478 by (rtac ext 1 THEN rtac ccontr 1); |
|
479 by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1); |
|
480 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def])); |
|
481 qed "starfun_eq_iff"; |