author | paulson |
Thu, 27 Nov 2003 10:47:55 +0100 | |
changeset 14268 | 5cf13e80be0e |
parent 13810 | c3fbfd472365 |
child 14371 | c78c7da09519 |
permissions | -rw-r--r-- |
10751 | 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 |
||
13810 | 73 |
Goalw [starsetNat_def] "*sNat* (-A) = -( *sNat* A)"; |
10751 | 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 |
||
13810 | 81 |
Goalw [starsetNat_n_def] "*sNatn* ((%n. - A n)) = -( *sNatn* A)"; |
10751 | 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 |
||
10834 | 120 |
Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A"; |
10751 | 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 |
||
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
125 |
Goal "Nats <= *sNat* (UNIV:: nat set)"; |
10751 | 126 |
by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff, |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10751
diff
changeset
|
127 |
NatStar_hypreal_of_real_image_subset]) 1); |
10751 | 128 |
qed "NatStar_SHNat_subset"; |
129 |
||
130 |
Goalw [starsetNat_def] |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
131 |
"*sNat* X Int Nats = hypnat_of_nat ` X"; |
10751 | 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 |
||
10834 | 143 |
Goal "x ~: hypnat_of_nat ` A ==> ALL y: A. x ~= hypnat_of_nat y"; |
10751 | 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 |
||
13810 | 151 |
Goalw [InternalNatSets_def] "( *sNat* X) : InternalNatSets"; |
10751 | 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] |
|
10834 | 191 |
"congruent hypnatrel (%X. hypnatrel``{%n. f (X n)})"; |
12486 | 192 |
by Safe_tac; |
10751 | 193 |
by (ALLGOALS(Fuf_tac)); |
194 |
qed "starfunNat_congruent"; |
|
195 |
||
196 |
(* f::nat=>real *) |
|
197 |
Goalw [starfunNat_def] |
|
13810 | 198 |
"( *fNat* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ |
10834 | 199 |
\ Abs_hypreal(hyprel `` {%n. f (X n)})"; |
10751 | 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] |
|
13810 | 208 |
"( *fNat2* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ |
10834 | 209 |
\ Abs_hypnat(hypnatrel `` {%n. f (X n)})"; |
10751 | 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 |
---------------------------------------------*) |
|
13810 | 219 |
Goal "( *fNat* f) z * ( *fNat* g) z = ( *fNat* (%x. f x * g x)) z"; |
10751 | 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 |
||
13810 | 224 |
Goal "( *fNat2* f) z * ( *fNat2* g) z = ( *fNat2* (%x. f x * g x)) z"; |
10751 | 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 |
---------------------------------------*) |
|
13810 | 232 |
Goal "( *fNat* f) z + ( *fNat* g) z = ( *fNat* (%x. f x + g x)) z"; |
10751 | 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 |
||
13810 | 237 |
Goal "( *fNat2* f) z + ( *fNat2* g) z = ( *fNat2* (%x. f x + g x)) z"; |
10751 | 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 |
||
13810 | 242 |
Goal "( *fNat2* f) z - ( *fNat2* g) z = ( *fNat2* (%x. f x - g x)) z"; |
10751 | 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 |
||
13810 | 252 |
Goal "( *fNat* f) o ( *fNat2* g) = ( *fNat* (f o g))"; |
10751 | 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 |
||
13810 | 258 |
Goal "(%x. ( *fNat* f) (( *fNat2* g) x)) = ( *fNat* (%x. f(g x)))"; |
10751 | 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) *****) |
|
13810 | 263 |
Goal "( *fNat2* f) o ( *fNat2* g) = ( *fNat2* (f o g))"; |
10751 | 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 |
||
13810 | 271 |
Goal "( *f* f) o ( *fNat* g) = ( *fNat* (f o g))"; |
10751 | 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 |
||
13810 | 277 |
Goal "(%x. ( *f* f) (( *fNat* g) x)) = ( *fNat* (%x. f (g x)))"; |
10751 | 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 |
--------------------------------------*) |
|
13810 | 284 |
Goal "( *fNat* (%x. k)) z = hypreal_of_real k"; |
10751 | 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 |
||
13810 | 290 |
Goal "( *fNat2* (%x. k)) z = hypnat_of_nat k"; |
10751 | 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 |
||
13810 | 297 |
Goal "- ( *fNat* f) x = ( *fNat* (%x. - f x)) x"; |
10751 | 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 |
||
13810 | 302 |
Goal "inverse (( *fNat* f) x) = ( *fNat* (%x. inverse (f x))) x"; |
10751 | 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 |
||
13810 | 313 |
Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)"; |
10751 | 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 |
||
13810 | 320 |
Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)"; |
10751 | 321 |
by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def])); |
322 |
qed "starfunNat2_eq"; |
|
323 |
||
324 |
Addsimps [starfunNat2_eq]; |
|
325 |
||
13810 | 326 |
Goal "( *fNat* f) (hypnat_of_nat a) @= hypreal_of_real (f a)"; |
10751 | 327 |
by (Auto_tac); |
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
328 |
qed "starfunNat_approx"; |
10751 | 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 \ |
|
13810 | 336 |
\ ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n <= ( *fNat* g) n"; |
10751 | 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 \ |
|
13810 | 348 |
\ ==> ALL n. hypnat_of_nat N <= n --> ( *fNat* f) n < ( *fNat* g) n"; |
10751 | 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 |
---------------------------------------------------------------*) |
|
13810 | 361 |
Goal "( *fNat* (%n. f (Suc n))) N = ( *fNat* f) (N + (1::hypnat))"; |
10751 | 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 |
---------------------------------------------------------------*) |
|
13810 | 370 |
Goal "( *fNat* (%n. abs (f n))) N = abs(( *fNat* f) N)"; |
10751 | 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 |
----------------------------------------------------------------*) |
|
13810 | 378 |
Goal "( *fNat* (%n. r ^ n)) N = (hypreal_of_real r) pow N"; |
10751 | 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 |
||
13810 | 384 |
Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m"; |
10751 | 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 |
||
13810 | 390 |
Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n"; |
10751 | 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 |
(*----------------------------------------------------- |
|
10919
144ede948e58
renamings: real_of_nat, real_of_int -> (overloaded) real
paulson
parents:
10834
diff
changeset
|
396 |
hypreal_of_hypnat as NS extension of real (from "nat")! |
10751 | 397 |
-------------------------------------------------------*) |
13810 | 398 |
Goal "( *fNat* real) = hypreal_of_hypnat"; |
10751 | 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 \ |
|
13810 | 405 |
\ ==> ( *fNat* (%x::nat. inverse(real x))) N = inverse(hypreal_of_hypnat N)"; |
10751 | 406 |
by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11713
diff
changeset
|
407 |
by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1); |
10751 | 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] |
|
10834 | 416 |
"congruent hypnatrel (%X. hypnatrel``{%n. f n (X n)})"; |
12486 | 417 |
by Safe_tac; |
10751 | 418 |
by (ALLGOALS(Fuf_tac)); |
419 |
qed "starfunNat_n_congruent"; |
|
420 |
||
421 |
Goalw [starfunNat_n_def] |
|
13810 | 422 |
"( *fNatn* f) (Abs_hypnat(hypnatrel``{%n. X n})) = \ |
10834 | 423 |
\ Abs_hypreal(hyprel `` {%n. f n (X n)})"; |
10751 | 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 |
-------------------------------------------------*) |
|
13810 | 432 |
Goal "( *fNatn* f) z * ( *fNatn* g) z = ( *fNatn* (% i x. f i x * g i x)) z"; |
10751 | 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 |
-----------------------------------------------*) |
|
13810 | 440 |
Goal "( *fNatn* f) z + ( *fNatn* g) z = ( *fNatn* (%i x. f i x + g i x)) z"; |
10751 | 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 |
-------------------------------------------------*) |
|
13810 | 448 |
Goal "( *fNatn* f) z + -( *fNatn* g) z = ( *fNatn* (%i x. f i x + -g i x)) z"; |
10751 | 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 |
||
13810 | 458 |
Goal "( *fNatn* (%i x. k)) z = hypreal_of_real k"; |
10751 | 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 |
||
13810 | 466 |
Goal "- ( *fNatn* f) x = ( *fNatn* (%i x. - (f i) x)) x"; |
10751 | 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 |
||
13810 | 471 |
Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})"; |
10751 | 472 |
by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def])); |
473 |
qed "starfunNat_n_eq"; |
|
474 |
Addsimps [starfunNat_n_eq]; |
|
475 |
||
13810 | 476 |
Goal "(( *fNat* f) = ( *fNat* g)) = (f = g)"; |
10751 | 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"; |
|
14268
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
482 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
483 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
484 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
485 |
(*MOVE UP*) |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
486 |
|
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
487 |
Goal "N : HNatInfinite \ |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
488 |
\ ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal"; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
489 |
by (res_inst_tac [("f1","inverse")] (starfun_stafunNat_o2 RS subst) 1); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
490 |
by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
491 |
by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat])); |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
492 |
qed "starfunNat_inverse_real_of_nat_Infinitesimal"; |
5cf13e80be0e
Removal of Hyperreal/ExtraThms2.ML, sending the material to the correct files.
paulson
parents:
13810
diff
changeset
|
493 |
Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal]; |