86 by (TRYALL(Ultra_tac)); |
86 by (TRYALL(Ultra_tac)); |
87 qed "starsetNat_n_Compl"; |
87 qed "starsetNat_n_Compl"; |
88 |
88 |
89 Goalw [InternalNatSets_def] |
89 Goalw [InternalNatSets_def] |
90 "X :InternalNatSets ==> -X : InternalNatSets"; |
90 "X :InternalNatSets ==> -X : InternalNatSets"; |
91 by (auto_tac (claset(),simpset() addsimps [starsetNat_n_Compl RS sym])); |
91 by (auto_tac (claset(), |
|
92 simpset() addsimps [starsetNat_n_Compl RS sym])); |
92 qed "InternalNatSets_Compl"; |
93 qed "InternalNatSets_Compl"; |
93 |
94 |
94 Goalw [starsetNat_n_def] |
95 Goalw [starsetNat_n_def] |
95 "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"; |
96 "*sNatn* (%n. (A n) - (B n)) = *sNatn* A - *sNatn* B"; |
96 by (Auto_tac); |
97 by (Auto_tac); |
97 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); |
98 by (res_inst_tac [("z","x")] eq_Abs_hypnat 2); |
98 by (res_inst_tac [("z","x")] eq_Abs_hypnat 3); |
99 by (res_inst_tac [("z","x")] eq_Abs_hypnat 3); |
99 by (auto_tac (claset() addSDs [bspec],simpset())); |
100 by (auto_tac (claset() addSDs [bspec], simpset())); |
100 by (TRYALL(Ultra_tac)); |
101 by (TRYALL(Ultra_tac)); |
101 qed "starsetNat_n_diff"; |
102 qed "starsetNat_n_diff"; |
102 |
103 |
103 Goalw [InternalNatSets_def] |
104 Goalw [InternalNatSets_def] |
104 "[| X : InternalNatSets; Y : InternalNatSets |] \ |
105 "[| X : InternalNatSets; Y : InternalNatSets |] \ |
105 \ ==> (X - Y) : InternalNatSets"; |
106 \ ==> (X - Y) : InternalNatSets"; |
106 by (auto_tac (claset(),simpset() addsimps [starsetNat_n_diff RS sym])); |
107 by (auto_tac (claset(), simpset() addsimps [starsetNat_n_diff RS sym])); |
107 qed "InternalNatSets_diff"; |
108 qed "InternalNatSets_diff"; |
108 |
109 |
109 Goalw [starsetNat_def] "!!A. A <= B ==> *sNat* A <= *sNat* B"; |
110 Goalw [starsetNat_def] "A <= B ==> *sNat* A <= *sNat* B"; |
110 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1)); |
111 by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1)); |
111 qed "NatStar_subset"; |
112 qed "NatStar_subset"; |
112 |
113 |
113 Goalw [starsetNat_def,hypnat_of_nat_def] |
114 Goalw [starsetNat_def,hypnat_of_nat_def] |
114 "!!A. a : A ==> hypnat_of_nat a : *sNat* A"; |
115 "a : A ==> hypnat_of_nat a : *sNat* A"; |
115 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset())); |
116 by (auto_tac (claset() addIs [FreeUltrafilterNat_subset], |
|
117 simpset())); |
116 qed "NatStar_mem"; |
118 qed "NatStar_mem"; |
117 |
119 |
118 Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A"; |
120 Goalw [starsetNat_def] "hypnat_of_nat `` A <= *sNat* A"; |
119 by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_def])); |
121 by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def])); |
120 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1); |
122 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1); |
121 qed "NatStar_hypreal_of_real_image_subset"; |
123 qed "NatStar_hypreal_of_real_image_subset"; |
122 |
124 |
123 Goal "SHNat <= *sNat* (UNIV:: nat set)"; |
125 Goal "SHNat <= *sNat* (UNIV:: nat set)"; |
124 by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff, |
126 by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff, |
125 NatStar_hypreal_of_real_image_subset]) 1); |
127 NatStar_hypreal_of_real_image_subset]) 1); |
126 qed "NatStar_SHNat_subset"; |
128 qed "NatStar_SHNat_subset"; |
127 |
129 |
128 Goalw [starsetNat_def] |
130 Goalw [starsetNat_def] |
129 "*sNat* X Int SHNat = hypnat_of_nat `` X"; |
131 "*sNat* X Int SHNat = hypnat_of_nat `` X"; |
130 by (auto_tac (claset(),simpset() addsimps |
132 by (auto_tac (claset(), |
|
133 simpset() addsimps |
131 [hypnat_of_nat_def,SHNat_def])); |
134 [hypnat_of_nat_def,SHNat_def])); |
132 by (fold_tac [hypnat_of_nat_def]); |
135 by (fold_tac [hypnat_of_nat_def]); |
133 by (rtac imageI 1 THEN rtac ccontr 1); |
136 by (rtac imageI 1 THEN rtac ccontr 1); |
134 by (dtac bspec 1); |
137 by (dtac bspec 1); |
135 by (rtac lemma_hypnatrel_refl 1); |
138 by (rtac lemma_hypnatrel_refl 1); |
136 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2); |
139 by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2); |
137 by (Auto_tac); |
140 by (Auto_tac); |
138 qed "NatStar_hypreal_of_real_Int"; |
141 qed "NatStar_hypreal_of_real_Int"; |
139 |
142 |
140 Goal "!!x. x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y"; |
143 Goal "x ~: hypnat_of_nat `` A ==> ALL y: A. x ~= hypnat_of_nat y"; |
141 by (Auto_tac); |
144 by (Auto_tac); |
142 qed "lemma_not_hypnatA"; |
145 qed "lemma_not_hypnatA"; |
143 |
146 |
144 Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)"; |
147 Goalw [starsetNat_n_def,starsetNat_def] "*sNat* X = *sNatn* (%n. X)"; |
145 by Auto_tac; |
148 by Auto_tac; |
146 qed "starsetNat_starsetNat_n_eq"; |
149 qed "starsetNat_starsetNat_n_eq"; |
147 |
150 |
148 Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets"; |
151 Goalw [InternalNatSets_def] "(*sNat* X) : InternalNatSets"; |
149 by (auto_tac (claset(),simpset() addsimps [starsetNat_starsetNat_n_eq])); |
152 by (auto_tac (claset(), |
|
153 simpset() addsimps [starsetNat_starsetNat_n_eq])); |
150 qed "InternalNatSets_starsetNat_n"; |
154 qed "InternalNatSets_starsetNat_n"; |
151 Addsimps [InternalNatSets_starsetNat_n]; |
155 Addsimps [InternalNatSets_starsetNat_n]; |
152 |
156 |
153 Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets"; |
157 Goal "X : InternalNatSets ==> UNIV - X : InternalNatSets"; |
154 by (auto_tac (claset() addIs [InternalNatSets_Compl],simpset())); |
158 by (auto_tac (claset() addIs [InternalNatSets_Compl], simpset())); |
155 qed "InternalNatSets_UNIV_diff"; |
159 qed "InternalNatSets_UNIV_diff"; |
156 |
160 |
157 (*------------------------------------------------------------------ |
161 (*------------------------------------------------------------------ |
158 Nonstandard extension of a set (defined using a constant |
162 Nonstandard extension of a set (defined using a constant |
159 sequence) as a special case of an internal set |
163 sequence) as a special case of an internal set |
160 -----------------------------------------------------------------*) |
164 -----------------------------------------------------------------*) |
161 |
165 |
162 Goalw [starsetNat_n_def,starsetNat_def] |
166 Goalw [starsetNat_n_def,starsetNat_def] |
163 "!!A. ALL n. (As n = A) ==> *sNatn* As = *sNat* A"; |
167 "ALL n. (As n = A) ==> *sNatn* As = *sNat* A"; |
164 by (Auto_tac); |
168 by (Auto_tac); |
165 qed "starsetNat_n_starsetNat"; |
169 qed "starsetNat_n_starsetNat"; |
166 |
170 |
167 (*------------------------------------------------------ |
171 (*------------------------------------------------------ |
168 Theorems about nonstandard extensions of functions |
172 Theorems about nonstandard extensions of functions |
212 (*--------------------------------------------- |
216 (*--------------------------------------------- |
213 multiplication: ( *f ) x ( *g ) = *(f x g) |
217 multiplication: ( *f ) x ( *g ) = *(f x g) |
214 ---------------------------------------------*) |
218 ---------------------------------------------*) |
215 Goal "(*fNat* f) xa * (*fNat* g) xa = (*fNat* (%x. f x * g x)) xa"; |
219 Goal "(*fNat* f) xa * (*fNat* g) xa = (*fNat* (%x. f x * g x)) xa"; |
216 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
220 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
217 by (auto_tac (claset(),simpset() addsimps |
221 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_mult])); |
218 [starfunNat,hypreal_mult])); |
|
219 qed "starfunNat_mult"; |
222 qed "starfunNat_mult"; |
220 |
223 |
221 Goal "(*fNat2* f) xa * (*fNat2* g) xa = (*fNat2* (%x. f x * g x)) xa"; |
224 Goal "(*fNat2* f) xa * (*fNat2* g) xa = (*fNat2* (%x. f x * g x)) xa"; |
222 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
225 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
223 by (auto_tac (claset(),simpset() addsimps |
226 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_mult])); |
224 [starfunNat2,hypnat_mult])); |
|
225 qed "starfunNat2_mult"; |
227 qed "starfunNat2_mult"; |
226 |
228 |
227 (*--------------------------------------- |
229 (*--------------------------------------- |
228 addition: ( *f ) + ( *g ) = *(f + g) |
230 addition: ( *f ) + ( *g ) = *(f + g) |
229 ---------------------------------------*) |
231 ---------------------------------------*) |
230 Goal "(*fNat* f) xa + (*fNat* g) xa = (*fNat* (%x. f x + g x)) xa"; |
232 Goal "(*fNat* f) xa + (*fNat* g) xa = (*fNat* (%x. f x + g x)) xa"; |
231 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
233 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
232 by (auto_tac (claset(),simpset() addsimps |
234 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypreal_add])); |
233 [starfunNat,hypreal_add])); |
|
234 qed "starfunNat_add"; |
235 qed "starfunNat_add"; |
235 |
236 |
236 Goal "(*fNat2* f) xa + (*fNat2* g) xa = (*fNat2* (%x. f x + g x)) xa"; |
237 Goal "(*fNat2* f) xa + (*fNat2* g) xa = (*fNat2* (%x. f x + g x)) xa"; |
237 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
238 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
238 by (auto_tac (claset(),simpset() addsimps |
239 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_add])); |
239 [starfunNat2,hypnat_add])); |
|
240 qed "starfunNat2_add"; |
240 qed "starfunNat2_add"; |
241 |
241 |
242 (*-------------------------------------------- |
|
243 subtraction: ( *f ) + -( *g ) = *(f + -g) |
|
244 --------------------------------------------*) |
|
245 Goal "(*fNat* f) xa + -(*fNat* g) xa = (*fNat* (%x. f x + -g x)) xa"; |
|
246 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
|
247 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
|
248 hypreal_minus,hypreal_add])); |
|
249 qed "starfunNat_add_minus"; |
|
250 |
|
251 Goal "(*fNat2* f) xa - (*fNat2* g) xa = (*fNat2* (%x. f x - g x)) xa"; |
242 Goal "(*fNat2* f) xa - (*fNat2* g) xa = (*fNat2* (%x. f x - g x)) xa"; |
252 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
243 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
253 by (auto_tac (claset(),simpset() addsimps [starfunNat2, |
244 by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_minus])); |
254 hypnat_minus])); |
|
255 qed "starfunNat2_minus"; |
245 qed "starfunNat2_minus"; |
256 |
246 |
257 (*-------------------------------------- |
247 (*-------------------------------------- |
258 composition: ( *f ) o ( *g ) = *(f o g) |
248 composition: ( *f ) o ( *g ) = *(f o g) |
259 ---------------------------------------*) |
249 ---------------------------------------*) |
260 (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****) |
250 (***** ( *f::nat=>real ) o ( *g::nat=>nat ) = *(f o g) *****) |
261 |
251 |
262 Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))"; |
252 Goal "(*fNat* f) o (*fNat2* g) = (*fNat* (f o g))"; |
263 by (rtac ext 1); |
253 by (rtac ext 1); |
264 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
254 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
265 by (auto_tac (claset(),simpset() addsimps [starfunNat2, |
255 by (auto_tac (claset(), simpset() addsimps [starfunNat2, starfunNat])); |
266 starfunNat])); |
|
267 qed "starfunNatNat2_o"; |
256 qed "starfunNatNat2_o"; |
268 |
257 |
269 Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))"; |
258 Goal "(%x. (*fNat* f) ((*fNat2* g) x)) = (*fNat* (%x. f(g x)))"; |
270 by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1); |
259 by (rtac ( simplify (simpset() addsimps [o_def]) starfunNatNat2_o) 1); |
271 qed "starfunNatNat2_o2"; |
260 qed "starfunNatNat2_o2"; |
272 |
261 |
273 (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****) |
262 (***** ( *f::nat=>nat ) o ( *g::nat=>nat ) = *(f o g) *****) |
274 Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))"; |
263 Goal "(*fNat2* f) o (*fNat2* g) = (*fNat2* (f o g))"; |
275 by (rtac ext 1); |
264 by (rtac ext 1); |
276 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
265 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
277 by (auto_tac (claset(),simpset() addsimps [starfunNat2])); |
266 by (auto_tac (claset(), simpset() addsimps [starfunNat2])); |
278 qed "starfunNat2_o"; |
267 qed "starfunNat2_o"; |
279 |
268 |
280 (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****) |
269 (***** ( *f::real=>real ) o ( *g::nat=>real ) = *(f o g) *****) |
281 |
270 |
282 Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; |
271 Goal "(*f* f) o (*fNat* g) = (*fNat* (f o g))"; |
283 by (rtac ext 1); |
272 by (rtac ext 1); |
284 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
273 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
285 by (auto_tac (claset(),simpset() addsimps [starfunNat,starfun])); |
274 by (auto_tac (claset(), simpset() addsimps [starfunNat,starfun])); |
286 qed "starfun_stafunNat_o"; |
275 qed "starfun_stafunNat_o"; |
287 |
276 |
288 Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; |
277 Goal "(%x. (*f* f) ((*fNat* g) x)) = (*fNat* (%x. f (g x)))"; |
289 by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1); |
278 by (rtac ( simplify (simpset() addsimps [o_def]) starfun_stafunNat_o) 1); |
290 qed "starfun_stafunNat_o2"; |
279 qed "starfun_stafunNat_o2"; |
292 (*-------------------------------------- |
281 (*-------------------------------------- |
293 NS extension of constant function |
282 NS extension of constant function |
294 --------------------------------------*) |
283 --------------------------------------*) |
295 Goal "(*fNat* (%x. k)) xa = hypreal_of_real k"; |
284 Goal "(*fNat* (%x. k)) xa = hypreal_of_real k"; |
296 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
285 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
297 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
286 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_of_real_def])); |
298 hypreal_of_real_def])); |
|
299 qed "starfunNat_const_fun"; |
287 qed "starfunNat_const_fun"; |
300 Addsimps [starfunNat_const_fun]; |
288 Addsimps [starfunNat_const_fun]; |
301 |
289 |
302 Goal "(*fNat2* (%x. k)) xa = hypnat_of_nat k"; |
290 Goal "(*fNat2* (%x. k)) xa = hypnat_of_nat k"; |
303 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
291 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
304 by (auto_tac (claset(),simpset() addsimps [starfunNat2, |
292 by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def])); |
305 hypnat_of_nat_def])); |
|
306 qed "starfunNat2_const_fun"; |
293 qed "starfunNat2_const_fun"; |
307 |
294 |
308 Addsimps [starfunNat2_const_fun]; |
295 Addsimps [starfunNat2_const_fun]; |
309 |
296 |
310 Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x"; |
297 Goal "- (*fNat* f) x = (*fNat* (%x. - f x)) x"; |
311 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
298 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
312 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
299 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_minus])); |
313 hypreal_minus])); |
|
314 qed "starfunNat_minus"; |
300 qed "starfunNat_minus"; |
315 |
301 |
316 Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x"; |
302 Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x"; |
317 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
303 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
318 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse])); |
304 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse])); |
323 version for natural arguments. i.e they are the same |
309 version for natural arguments. i.e they are the same |
324 for all natural arguments (c.f. Hoskins pg. 107- SEQ) |
310 for all natural arguments (c.f. Hoskins pg. 107- SEQ) |
325 -------------------------------------------------------*) |
311 -------------------------------------------------------*) |
326 |
312 |
327 Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"; |
313 Goal "(*fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"; |
328 by (auto_tac (claset(),simpset() addsimps |
314 by (auto_tac (claset(), |
329 [starfunNat,hypnat_of_nat_def,hypreal_of_real_def])); |
315 simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def])); |
330 qed "starfunNat_eq"; |
316 qed "starfunNat_eq"; |
331 |
317 |
332 Addsimps [starfunNat_eq]; |
318 Addsimps [starfunNat_eq]; |
333 |
319 |
334 Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"; |
320 Goal "(*fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"; |
335 by (auto_tac (claset(),simpset() addsimps |
321 by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def])); |
336 [starfunNat2,hypnat_of_nat_def])); |
|
337 qed "starfunNat2_eq"; |
322 qed "starfunNat2_eq"; |
338 |
323 |
339 Addsimps [starfunNat2_eq]; |
324 Addsimps [starfunNat2_eq]; |
340 |
325 |
341 Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"; |
326 Goal "(*fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"; |
342 by (Auto_tac); |
327 by (Auto_tac); |
343 qed "starfunNat_inf_close"; |
328 qed "starfunNat_inf_close"; |
344 |
|
345 Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m; \ |
|
346 \ l: HFinite; m: HFinite \ |
|
347 \ |] ==> (*fNat* (%x. f x * g x)) xa @= l * m"; |
|
348 by (dtac inf_close_mult_HFinite 1); |
|
349 by (REPEAT(assume_tac 1)); |
|
350 by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)], |
|
351 simpset() addsimps [starfunNat_mult])); |
|
352 qed "starfunNat_mult_HFinite_inf_close"; |
|
353 |
|
354 Goal "!!f. [| (*fNat* f) xa @= l; (*fNat* g) xa @= m \ |
|
355 \ |] ==> (*fNat* (%x. f x + g x)) xa @= l + m"; |
|
356 by (auto_tac (claset() addIs [inf_close_add], |
|
357 simpset() addsimps [starfunNat_add RS sym])); |
|
358 qed "starfunNat_add_inf_close"; |
|
359 |
329 |
360 |
330 |
361 (*----------------------------------------------------------------- |
331 (*----------------------------------------------------------------- |
362 Example of transfer of a property from reals to hyperreals |
332 Example of transfer of a property from reals to hyperreals |
363 --- used for limit comparison of sequences |
333 --- used for limit comparison of sequences |
364 ----------------------------------------------------------------*) |
334 ----------------------------------------------------------------*) |
365 Goal "!!f. ALL n. N <= n --> f n <= g n \ |
335 Goal "ALL n. N <= n --> f n <= g n \ |
366 \ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n"; |
336 \ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n <= (*fNat* g) n"; |
367 by (Step_tac 1); |
337 by (Step_tac 1); |
368 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
338 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
369 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
339 by (auto_tac (claset(), |
370 hypnat_of_nat_def,hypreal_le,hypreal_less, |
340 simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le, |
371 hypnat_le,hypnat_less])); |
341 hypreal_less, hypnat_le,hypnat_less])); |
372 by (Ultra_tac 1); |
342 by (Ultra_tac 1); |
373 by Auto_tac; |
343 by Auto_tac; |
374 qed "starfun_le_mono"; |
344 qed "starfun_le_mono"; |
375 |
345 |
376 (*****----- and another -----*****) |
346 (*****----- and another -----*****) |
377 goal NatStar.thy |
347 Goal "ALL n. N <= n --> f n < g n \ |
378 "!!f. ALL n. N <= n --> f n < g n \ |
|
379 \ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n"; |
348 \ ==> ALL n. hypnat_of_nat N <= n --> (*fNat* f) n < (*fNat* g) n"; |
380 by (Step_tac 1); |
349 by (Step_tac 1); |
381 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
350 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
382 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
351 by (auto_tac (claset(), |
383 hypnat_of_nat_def,hypreal_le,hypreal_less, |
352 simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le, |
384 hypnat_le,hypnat_less])); |
353 hypreal_less, hypnat_le,hypnat_less])); |
385 by (Ultra_tac 1); |
354 by (Ultra_tac 1); |
386 by Auto_tac; |
355 by Auto_tac; |
387 qed "starfun_less_mono"; |
356 qed "starfun_less_mono"; |
388 |
357 |
389 (*---------------------------------------------------------------- |
358 (*---------------------------------------------------------------- |
390 NS extension when we displace argument by one |
359 NS extension when we displace argument by one |
391 ---------------------------------------------------------------*) |
360 ---------------------------------------------------------------*) |
392 Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)"; |
361 Goal "(*fNat* (%n. f (Suc n))) N = (*fNat* f) (N + 1hn)"; |
393 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
362 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
394 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
363 by (auto_tac (claset(), |
395 hypnat_one_def,hypnat_add])); |
364 simpset() addsimps [starfunNat, hypnat_one_def,hypnat_add])); |
396 qed "starfunNat_shift_one"; |
365 qed "starfunNat_shift_one"; |
397 |
366 |
398 (*---------------------------------------------------------------- |
367 (*---------------------------------------------------------------- |
399 NS extension with rabs |
368 NS extension with rabs |
400 ---------------------------------------------------------------*) |
369 ---------------------------------------------------------------*) |
401 Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)"; |
370 Goal "(*fNat* (%n. abs (f n))) N = abs((*fNat* f) N)"; |
402 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
371 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
403 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
372 by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_hrabs])); |
404 hypreal_hrabs])); |
|
405 qed "starfunNat_rabs"; |
373 qed "starfunNat_rabs"; |
406 |
374 |
407 (*---------------------------------------------------------------- |
375 (*---------------------------------------------------------------- |
408 The hyperpow function as a NS extension of realpow |
376 The hyperpow function as a NS extension of realpow |
409 ----------------------------------------------------------------*) |
377 ----------------------------------------------------------------*) |
410 Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"; |
378 Goal "(*fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"; |
411 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
379 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
412 by (auto_tac (claset(),simpset() addsimps [hyperpow, |
380 by (auto_tac (claset(), |
413 hypreal_of_real_def,starfunNat])); |
381 simpset() addsimps [hyperpow, hypreal_of_real_def,starfunNat])); |
414 qed "starfunNat_pow"; |
382 qed "starfunNat_pow"; |
415 |
383 |
416 Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m"; |
384 Goal "(*fNat* (%n. (X n) ^ m)) N = (*fNat* X) N pow hypnat_of_nat m"; |
417 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
385 by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); |
418 by (auto_tac (claset(),simpset() addsimps [hyperpow, |
386 by (auto_tac (claset(), |
419 hypnat_of_nat_def,starfunNat])); |
387 simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat])); |
420 qed "starfunNat_pow2"; |
388 qed "starfunNat_pow2"; |
421 |
389 |
422 Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"; |
390 Goalw [hypnat_of_nat_def] "(*f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"; |
423 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
391 by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); |
424 by (auto_tac (claset(),simpset() addsimps [hyperpow,starfun])); |
392 by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun])); |
425 qed "starfun_pow"; |
393 qed "starfun_pow"; |
426 |
394 |
427 (*----------------------------------------------------- |
395 (*----------------------------------------------------- |
428 hypreal_of_hypnat as NS extension of real_of_nat! |
396 hypreal_of_hypnat as NS extension of real_of_nat! |
429 -------------------------------------------------------*) |
397 -------------------------------------------------------*) |
430 Goal "(*fNat* real_of_nat) = hypreal_of_hypnat"; |
398 Goal "(*fNat* real_of_nat) = hypreal_of_hypnat"; |
431 by (rtac ext 1); |
399 by (rtac ext 1); |
432 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
400 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
433 by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,starfunNat])); |
401 by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat,starfunNat])); |
434 qed "starfunNat_real_of_nat"; |
402 qed "starfunNat_real_of_nat"; |
435 |
403 |
436 Goal "N : HNatInfinite \ |
404 Goal "N : HNatInfinite \ |
437 \ ==> (*fNat* (%x. inverse (real_of_nat x))) N = inverse(hypreal_of_hypnat N)"; |
405 \ ==> (*fNat* (%x. inverse (real_of_nat x))) N = inverse(hypreal_of_hypnat N)"; |
438 by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); |
406 by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); |
439 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1); |
407 by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1); |
440 by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat, |
408 by (auto_tac (claset(), |
441 starfun_inverse_inverse])); |
409 simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse])); |
442 qed "starfunNat_inverse_real_of_nat_eq"; |
410 qed "starfunNat_inverse_real_of_nat_eq"; |
443 |
411 |
444 (*---------------------------------------------------------- |
412 (*---------------------------------------------------------- |
445 Internal functions - some redundancy with *fNat* now |
413 Internal functions - some redundancy with *fNat* now |
446 ---------------------------------------------------------*) |
414 ---------------------------------------------------------*) |
462 multiplication: ( *fn ) x ( *gn ) = *(fn x gn) |
430 multiplication: ( *fn ) x ( *gn ) = *(fn x gn) |
463 -------------------------------------------------*) |
431 -------------------------------------------------*) |
464 Goal "(*fNatn* f) xa * (*fNatn* g) xa = \ |
432 Goal "(*fNatn* f) xa * (*fNatn* g) xa = \ |
465 \ (*fNatn* (% i x. f i x * g i x)) xa"; |
433 \ (*fNatn* (% i x. f i x * g i x)) xa"; |
466 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
434 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
467 by (auto_tac (claset(),simpset() addsimps |
435 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_mult])); |
468 [starfunNat_n,hypreal_mult])); |
|
469 qed "starfunNat_n_mult"; |
436 qed "starfunNat_n_mult"; |
470 |
437 |
471 (*----------------------------------------------- |
438 (*----------------------------------------------- |
472 addition: ( *fn ) + ( *gn ) = *(fn + gn) |
439 addition: ( *fn ) + ( *gn ) = *(fn + gn) |
473 -----------------------------------------------*) |
440 -----------------------------------------------*) |
474 Goal "(*fNatn* f) xa + (*fNatn* g) xa = \ |
441 Goal "(*fNatn* f) xa + (*fNatn* g) xa = \ |
475 \ (*fNatn* (%i x. f i x + g i x)) xa"; |
442 \ (*fNatn* (%i x. f i x + g i x)) xa"; |
476 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
443 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
477 by (auto_tac (claset(),simpset() addsimps |
444 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypreal_add])); |
478 [starfunNat_n,hypreal_add])); |
|
479 qed "starfunNat_n_add"; |
445 qed "starfunNat_n_add"; |
480 |
446 |
481 (*------------------------------------------------- |
447 (*------------------------------------------------- |
482 subtraction: ( *fn ) + -( *gn ) = *(fn + -gn) |
448 subtraction: ( *fn ) + -( *gn ) = *(fn + -gn) |
483 -------------------------------------------------*) |
449 -------------------------------------------------*) |
484 Goal "(*fNatn* f) xa + -(*fNatn* g) xa = \ |
450 Goal "(*fNatn* f) xa + -(*fNatn* g) xa = \ |
485 \ (*fNatn* (%i x. f i x + -g i x)) xa"; |
451 \ (*fNatn* (%i x. f i x + -g i x)) xa"; |
486 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
452 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
487 by (auto_tac (claset(),simpset() addsimps [starfunNat_n, |
453 by (auto_tac (claset(), |
488 hypreal_minus,hypreal_add])); |
454 simpset() addsimps [starfunNat_n, hypreal_minus,hypreal_add])); |
489 qed "starfunNat_n_add_minus"; |
455 qed "starfunNat_n_add_minus"; |
490 |
456 |
491 (*-------------------------------------------------- |
457 (*-------------------------------------------------- |
492 composition: ( *fn ) o ( *gn ) = *(fn o gn) |
458 composition: ( *fn ) o ( *gn ) = *(fn o gn) |
493 -------------------------------------------------*) |
459 -------------------------------------------------*) |
494 |
460 |
495 Goal "(*fNatn* (%i x. k)) xa = hypreal_of_real k"; |
461 Goal "(*fNatn* (%i x. k)) xa = hypreal_of_real k"; |
496 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
462 by (res_inst_tac [("z","xa")] eq_Abs_hypnat 1); |
497 by (auto_tac (claset(),simpset() addsimps [starfunNat_n, |
463 by (auto_tac (claset(), |
498 hypreal_of_real_def])); |
464 simpset() addsimps [starfunNat_n, hypreal_of_real_def])); |
499 qed "starfunNat_n_const_fun"; |
465 qed "starfunNat_n_const_fun"; |
500 |
466 |
501 Addsimps [starfunNat_n_const_fun]; |
467 Addsimps [starfunNat_n_const_fun]; |
502 |
468 |
503 Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x"; |
469 Goal "- (*fNatn* f) x = (*fNatn* (%i x. - (f i) x)) x"; |
504 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
470 by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); |
505 by (auto_tac (claset(),simpset() addsimps [starfunNat_n, |
471 by (auto_tac (claset(), simpset() addsimps [starfunNat_n, hypreal_minus])); |
506 hypreal_minus])); |
|
507 qed "starfunNat_n_minus"; |
472 qed "starfunNat_n_minus"; |
508 |
473 |
509 Goal "(*fNatn* f) (hypnat_of_nat n) = \ |
474 Goal "(*fNatn* f) (hypnat_of_nat n) = \ |
510 \ Abs_hypreal(hyprel ^^ {%i. f i n})"; |
475 \ Abs_hypreal(hyprel ^^ {%i. f i n})"; |
511 by (auto_tac (claset(),simpset() addsimps |
476 by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def])); |
512 [starfunNat_n,hypnat_of_nat_def])); |
|
513 qed "starfunNat_n_eq"; |
477 qed "starfunNat_n_eq"; |
514 Addsimps [starfunNat_n_eq]; |
478 Addsimps [starfunNat_n_eq]; |
515 |
479 |
516 Goal "((*fNat* f) = (*fNat* g)) = (f = g)"; |
480 Goal "((*fNat* f) = (*fNat* g)) = (f = g)"; |
517 by Auto_tac; |
481 by Auto_tac; |
518 by (rtac ext 1 THEN rtac ccontr 1); |
482 by (rtac ext 1 THEN rtac ccontr 1); |
519 by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1); |
483 by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1); |
520 by (auto_tac (claset(),simpset() addsimps [starfunNat,hypnat_of_nat_def])); |
484 by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def])); |
521 qed "starfun_eq_iff"; |
485 qed "starfun_eq_iff"; |
522 |
486 |
523 |
487 |
524 |
488 |
525 |
489 |