13957
|
1 |
(* Title : CStar.ML
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 2001 University of Edinburgh
|
|
4 |
Description : defining *-transforms in NSA which extends sets of complex numbers,
|
|
5 |
and complex functions
|
|
6 |
*)
|
|
7 |
|
|
8 |
|
|
9 |
|
|
10 |
(*-----------------------------------------------------------------------------------*)
|
|
11 |
(* Properties of the *-transform applied to sets of reals *)
|
|
12 |
(* ----------------------------------------------------------------------------------*)
|
|
13 |
|
|
14 |
Goalw [starsetC_def] "*sc*(UNIV::complex set) = (UNIV::hcomplex set)";
|
|
15 |
by (Auto_tac);
|
|
16 |
qed "STARC_complex_set";
|
|
17 |
Addsimps [STARC_complex_set];
|
|
18 |
|
|
19 |
Goalw [starsetC_def] "*sc* {} = {}";
|
|
20 |
by (Auto_tac);
|
|
21 |
qed "STARC_empty_set";
|
|
22 |
Addsimps [STARC_empty_set];
|
|
23 |
|
|
24 |
Goalw [starsetC_def] "*sc* (A Un B) = *sc* A Un *sc* B";
|
|
25 |
by (Auto_tac);
|
|
26 |
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2));
|
|
27 |
by (dtac bspec 1 THEN assume_tac 1);
|
|
28 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
29 |
by (Auto_tac);
|
|
30 |
by (Ultra_tac 1);
|
|
31 |
qed "STARC_Un";
|
|
32 |
|
|
33 |
Goalw [starsetC_n_def]
|
|
34 |
"*scn* (%n. (A n) Un (B n)) = *scn* A Un *scn* B";
|
|
35 |
by Auto_tac;
|
|
36 |
by (dres_inst_tac [("x","Xa")] bspec 1);
|
|
37 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
|
|
38 |
by (auto_tac (claset() addSDs [bspec], simpset()));
|
|
39 |
by (TRYALL(Ultra_tac));
|
|
40 |
qed "starsetC_n_Un";
|
|
41 |
|
|
42 |
Goalw [InternalCSets_def]
|
|
43 |
"[| X : InternalCSets; Y : InternalCSets |] \
|
|
44 |
\ ==> (X Un Y) : InternalCSets";
|
|
45 |
by (auto_tac (claset(),
|
|
46 |
simpset() addsimps [starsetC_n_Un RS sym]));
|
|
47 |
qed "InternalCSets_Un";
|
|
48 |
|
|
49 |
Goalw [starsetC_def] "*sc* (A Int B) = *sc* A Int *sc* B";
|
|
50 |
by (Auto_tac);
|
|
51 |
by (blast_tac (claset() addIs [FreeUltrafilterNat_Int,
|
|
52 |
FreeUltrafilterNat_subset]) 3);
|
|
53 |
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
|
|
54 |
qed "STARC_Int";
|
|
55 |
|
|
56 |
Goalw [starsetC_n_def]
|
|
57 |
"*scn* (%n. (A n) Int (B n)) = *scn* A Int *scn* B";
|
|
58 |
by (Auto_tac);
|
|
59 |
by (auto_tac (claset() addSDs [bspec],simpset()));
|
|
60 |
by (TRYALL(Ultra_tac));
|
|
61 |
qed "starsetC_n_Int";
|
|
62 |
|
|
63 |
Goalw [InternalCSets_def]
|
|
64 |
"[| X : InternalCSets; Y : InternalCSets |] \
|
|
65 |
\ ==> (X Int Y) : InternalCSets";
|
|
66 |
by (auto_tac (claset(),
|
|
67 |
simpset() addsimps [starsetC_n_Int RS sym]));
|
|
68 |
qed "InternalCSets_Int";
|
|
69 |
|
|
70 |
Goalw [starsetC_def] "*sc* -A = -( *sc* A)";
|
|
71 |
by (Auto_tac);
|
|
72 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
73 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
|
|
74 |
by (REPEAT(Step_tac 1) THEN Auto_tac);
|
|
75 |
by (ALLGOALS(Ultra_tac));
|
|
76 |
qed "STARC_Compl";
|
|
77 |
|
|
78 |
Goalw [starsetC_n_def] "*scn* ((%n. - A n)) = -( *scn* A)";
|
|
79 |
by (Auto_tac);
|
|
80 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
81 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
|
|
82 |
by (REPEAT(Step_tac 1) THEN Auto_tac);
|
|
83 |
by (TRYALL(Ultra_tac));
|
|
84 |
qed "starsetC_n_Compl";
|
|
85 |
|
|
86 |
Goalw [InternalCSets_def]
|
|
87 |
"X :InternalCSets ==> -X : InternalCSets";
|
|
88 |
by (auto_tac (claset(),
|
|
89 |
simpset() addsimps [starsetC_n_Compl RS sym]));
|
|
90 |
qed "InternalCSets_Compl";
|
|
91 |
|
|
92 |
Goal "x ~: *sc* F ==> x : *sc* (- F)";
|
|
93 |
by (auto_tac (claset(),simpset() addsimps [STARC_Compl]));
|
|
94 |
qed "STARC_mem_Compl";
|
|
95 |
|
|
96 |
Goal "*sc* (A - B) = *sc* A - *sc* B";
|
|
97 |
by (auto_tac (claset(),simpset() addsimps
|
|
98 |
[set_diff_iff2,STARC_Int,STARC_Compl]));
|
|
99 |
qed "STARC_diff";
|
|
100 |
|
|
101 |
Goalw [starsetC_n_def]
|
|
102 |
"*scn* (%n. (A n) - (B n)) = *scn* A - *scn* B";
|
|
103 |
by (Auto_tac);
|
|
104 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2);
|
|
105 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 3);
|
|
106 |
by (auto_tac (claset() addSDs [bspec], simpset()));
|
|
107 |
by (TRYALL(Ultra_tac));
|
|
108 |
qed "starsetC_n_diff";
|
|
109 |
|
|
110 |
Goalw [InternalCSets_def]
|
|
111 |
"[| X : InternalCSets; Y : InternalCSets |] \
|
|
112 |
\ ==> (X - Y) : InternalCSets";
|
|
113 |
by (auto_tac (claset(), simpset() addsimps [starsetC_n_diff RS sym]));
|
|
114 |
qed "InternalCSets_diff";
|
|
115 |
|
|
116 |
Goalw [starsetC_def] "A <= B ==> *sc* A <= *sc* B";
|
|
117 |
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
|
|
118 |
qed "STARC_subset";
|
|
119 |
|
|
120 |
Goalw [starsetC_def,hcomplex_of_complex_def]
|
|
121 |
"a : A ==> hcomplex_of_complex a : *sc* A";
|
|
122 |
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
|
|
123 |
simpset()));
|
|
124 |
qed "STARC_mem";
|
|
125 |
|
|
126 |
Goalw [starsetC_def] "hcomplex_of_complex ` A <= *sc* A";
|
|
127 |
by (auto_tac (claset(), simpset() addsimps [hcomplex_of_complex_def]));
|
|
128 |
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
|
|
129 |
qed "STARC_hcomplex_of_complex_image_subset";
|
|
130 |
|
|
131 |
Goal "SComplex <= *sc* (UNIV:: complex set)";
|
|
132 |
by Auto_tac;
|
|
133 |
qed "STARC_SComplex_subset";
|
|
134 |
|
|
135 |
Goalw [starsetC_def]
|
|
136 |
"*sc* X Int SComplex = hcomplex_of_complex ` X";
|
|
137 |
by (auto_tac (claset(),
|
|
138 |
simpset() addsimps
|
|
139 |
[hcomplex_of_complex_def,SComplex_def]));
|
|
140 |
by (fold_tac [hcomplex_of_complex_def]);
|
|
141 |
by (rtac imageI 1 THEN rtac ccontr 1);
|
|
142 |
by (dtac bspec 1);
|
|
143 |
by (rtac lemma_hcomplexrel_refl 1);
|
|
144 |
by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2);
|
|
145 |
by (Auto_tac);
|
|
146 |
qed "STARC_hcomplex_of_complex_Int";
|
|
147 |
|
|
148 |
Goal "x ~: hcomplex_of_complex ` A ==> ALL y: A. x ~= hcomplex_of_complex y";
|
|
149 |
by (Auto_tac);
|
|
150 |
qed "lemma_not_hcomplexA";
|
|
151 |
|
|
152 |
Goalw [starsetC_n_def,starsetC_def] "*sc* X = *scn* (%n. X)";
|
|
153 |
by Auto_tac;
|
|
154 |
qed "starsetC_starsetC_n_eq";
|
|
155 |
|
|
156 |
Goalw [InternalCSets_def] "( *sc* X) : InternalCSets";
|
|
157 |
by (auto_tac (claset(),
|
|
158 |
simpset() addsimps [starsetC_starsetC_n_eq]));
|
|
159 |
qed "InternalCSets_starsetC_n";
|
|
160 |
Addsimps [InternalCSets_starsetC_n];
|
|
161 |
|
|
162 |
Goal "X : InternalCSets ==> UNIV - X : InternalCSets";
|
|
163 |
by (auto_tac (claset() addIs [InternalCSets_Compl], simpset()));
|
|
164 |
qed "InternalCSets_UNIV_diff";
|
|
165 |
|
|
166 |
(*-----------------------------------------------------------------------------------*)
|
|
167 |
(* Nonstandard extension of a set (defined using a constant sequence) as a special *)
|
|
168 |
(* case of an internal set *)
|
|
169 |
(*-----------------------------------------------------------------------------------*)
|
|
170 |
|
|
171 |
Goalw [starsetC_n_def,starsetC_def]
|
|
172 |
"ALL n. (As n = A) ==> *scn* As = *sc* A";
|
|
173 |
by (Auto_tac);
|
|
174 |
qed "starsetC_n_starsetC";
|
|
175 |
|
|
176 |
(*-----------------------------------------------------------------------------------*)
|
|
177 |
(* Theorems about nonstandard extensions of functions *)
|
|
178 |
(*-----------------------------------------------------------------------------------*)
|
|
179 |
|
|
180 |
Goalw [starfunC_n_def,starfunC_def]
|
|
181 |
"ALL n. (F n = f) ==> *fcn* F = *fc* f";
|
|
182 |
by (Auto_tac);
|
|
183 |
qed "starfunC_n_starfunC";
|
|
184 |
|
|
185 |
Goalw [starfunRC_n_def,starfunRC_def]
|
|
186 |
"ALL n. (F n = f) ==> *fRcn* F = *fRc* f";
|
|
187 |
by (Auto_tac);
|
|
188 |
qed "starfunRC_n_starfunRC";
|
|
189 |
|
|
190 |
Goalw [starfunCR_n_def,starfunCR_def]
|
|
191 |
"ALL n. (F n = f) ==> *fcRn* F = *fcR* f";
|
|
192 |
by (Auto_tac);
|
|
193 |
qed "starfunCR_n_starfunCR";
|
|
194 |
|
|
195 |
Goalw [congruent_def]
|
|
196 |
"congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})";
|
|
197 |
by (safe_tac (claset()));
|
|
198 |
by (ALLGOALS(Ultra_tac));
|
|
199 |
qed "starfunC_congruent";
|
|
200 |
|
|
201 |
(* f::complex => complex *)
|
|
202 |
Goalw [starfunC_def]
|
|
203 |
"( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
|
|
204 |
\ Abs_hcomplex(hcomplexrel `` {%n. f (X n)})";
|
|
205 |
by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
|
|
206 |
by Auto_tac;
|
|
207 |
by (Ultra_tac 1);
|
|
208 |
qed "starfunC";
|
|
209 |
|
|
210 |
Goalw [starfunRC_def]
|
|
211 |
"( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) = \
|
|
212 |
\ Abs_hcomplex(hcomplexrel `` {%n. f (X n)})";
|
|
213 |
by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
|
|
214 |
by Auto_tac;
|
|
215 |
by (Ultra_tac 1);
|
|
216 |
qed "starfunRC";
|
|
217 |
|
|
218 |
Goalw [starfunCR_def]
|
|
219 |
"( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
|
|
220 |
\ Abs_hypreal(hyprel `` {%n. f (X n)})";
|
|
221 |
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
|
|
222 |
by Auto_tac;
|
|
223 |
by (Ultra_tac 1);
|
|
224 |
qed "starfunCR";
|
|
225 |
|
|
226 |
(** multiplication: ( *f ) x ( *g ) = *(f x g) **)
|
|
227 |
|
|
228 |
Goal "( *fc* f) z * ( *fc* g) z = ( *fc* (%x. f x * g x)) z";
|
|
229 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
230 |
by (auto_tac (claset(), simpset() addsimps [starfunC,hcomplex_mult]));
|
|
231 |
qed "starfunC_mult";
|
|
232 |
Addsimps [starfunC_mult RS sym];
|
|
233 |
|
|
234 |
Goal "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z";
|
|
235 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
236 |
by (auto_tac (claset(), simpset() addsimps [starfunRC,hcomplex_mult]));
|
|
237 |
qed "starfunRC_mult";
|
|
238 |
Addsimps [starfunRC_mult RS sym];
|
|
239 |
|
|
240 |
Goal "( *fcR* f) z * ( *fcR* g) z = ( *fcR* (%x. f x * g x)) z";
|
|
241 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
242 |
by (auto_tac (claset(), simpset() addsimps [starfunCR,hypreal_mult]));
|
|
243 |
qed "starfunCR_mult";
|
|
244 |
Addsimps [starfunCR_mult RS sym];
|
|
245 |
|
|
246 |
(** addition: ( *f ) + ( *g ) = *(f + g) **)
|
|
247 |
|
|
248 |
Goal "( *fc* f) z + ( *fc* g) z = ( *fc* (%x. f x + g x)) z";
|
|
249 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
250 |
by (auto_tac (claset(), simpset() addsimps [starfunC,hcomplex_add]));
|
|
251 |
qed "starfunC_add";
|
|
252 |
Addsimps [starfunC_add RS sym];
|
|
253 |
|
|
254 |
Goal "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z";
|
|
255 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
256 |
by (auto_tac (claset(), simpset() addsimps [starfunRC,hcomplex_add]));
|
|
257 |
qed "starfunRC_add";
|
|
258 |
Addsimps [starfunRC_add RS sym];
|
|
259 |
|
|
260 |
Goal "( *fcR* f) z + ( *fcR* g) z = ( *fcR* (%x. f x + g x)) z";
|
|
261 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
262 |
by (auto_tac (claset(), simpset() addsimps [starfunCR,hypreal_add]));
|
|
263 |
qed "starfunCR_add";
|
|
264 |
Addsimps [starfunCR_add RS sym];
|
|
265 |
|
|
266 |
(** uminus **)
|
|
267 |
Goal "( *fc* (%x. - f x)) x = - ( *fc* f) x";
|
|
268 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
269 |
by (auto_tac (claset(),simpset() addsimps [starfunC, hcomplex_minus]));
|
|
270 |
qed "starfunC_minus";
|
|
271 |
Addsimps [starfunC_minus];
|
|
272 |
|
|
273 |
Goal "( *fRc* (%x. - f x)) x = - ( *fRc* f) x";
|
|
274 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
275 |
by (auto_tac (claset(),simpset() addsimps [starfunRC, hcomplex_minus]));
|
|
276 |
qed "starfunRC_minus";
|
|
277 |
Addsimps [starfunRC_minus];
|
|
278 |
|
|
279 |
Goal "( *fcR* (%x. - f x)) x = - ( *fcR* f) x";
|
|
280 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
281 |
by (auto_tac (claset(),simpset() addsimps [starfunCR, hypreal_minus]));
|
|
282 |
qed "starfunCR_minus";
|
|
283 |
Addsimps [starfunCR_minus];
|
|
284 |
|
|
285 |
(** addition: ( *f ) - ( *g ) = *(f - g) **)
|
|
286 |
|
|
287 |
Goalw [hcomplex_diff_def,complex_diff_def]
|
|
288 |
"( *fc* f) xa - ( *fc* g) xa = ( *fc* (%x. f x - g x)) xa";
|
|
289 |
by (auto_tac (claset(),simpset() addsimps [starfunC_minus,starfunC_add RS sym]));
|
|
290 |
qed "starfunC_diff";
|
|
291 |
Addsimps [starfunC_diff RS sym];
|
|
292 |
|
|
293 |
Goalw [hcomplex_diff_def,complex_diff_def]
|
|
294 |
"( *fRc* f) xa - ( *fRc* g) xa = ( *fRc* (%x. f x - g x)) xa";
|
|
295 |
by (auto_tac (claset(),simpset() addsimps [starfunRC_minus,starfunRC_add RS sym]));
|
|
296 |
qed "starfunRC_diff";
|
|
297 |
Addsimps [starfunRC_diff RS sym];
|
|
298 |
|
|
299 |
Goalw [hypreal_diff_def,real_diff_def]
|
|
300 |
"( *fcR* f) xa - ( *fcR* g) xa = ( *fcR* (%x. f x - g x)) xa";
|
|
301 |
by (auto_tac (claset(),simpset() addsimps [starfunCR_minus,starfunCR_add RS sym]));
|
|
302 |
qed "starfunCR_diff";
|
|
303 |
Addsimps [starfunCR_diff RS sym];
|
|
304 |
|
|
305 |
(** composition: ( *f ) o ( *g ) = *(f o g) **)
|
|
306 |
|
|
307 |
Goal "(%x. ( *fc* f) (( *fc* g) x)) = *fc* (%x. f (g x))";
|
|
308 |
by (rtac ext 1);
|
|
309 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
310 |
by (auto_tac (claset(),simpset() addsimps [starfunC]));
|
|
311 |
qed "starfunC_o2";
|
|
312 |
|
|
313 |
Goalw [o_def] "( *fc* f) o ( *fc* g) = ( *fc* (f o g))";
|
|
314 |
by (simp_tac (simpset() addsimps [starfunC_o2]) 1);
|
|
315 |
qed "starfunC_o";
|
|
316 |
|
|
317 |
Goal "(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))";
|
|
318 |
by (rtac ext 1);
|
|
319 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
320 |
by (auto_tac (claset(),simpset() addsimps [starfunRC,starfunC]));
|
|
321 |
qed "starfunC_starfunRC_o2";
|
|
322 |
|
|
323 |
Goal "(%x. ( *f* f) (( *fcR* g) x)) = *fcR* (%x. f (g x))";
|
|
324 |
by (rtac ext 1);
|
|
325 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
326 |
by (auto_tac (claset(),simpset() addsimps [starfunCR,starfun]));
|
|
327 |
qed "starfun_starfunCR_o2";
|
|
328 |
|
|
329 |
Goalw [o_def] "( *fc* f) o ( *fRc* g) = ( *fRc* (f o g))";
|
|
330 |
by (simp_tac (simpset() addsimps [starfunC_starfunRC_o2]) 1);
|
|
331 |
qed "starfunC_starfunRC_o";
|
|
332 |
|
|
333 |
Goalw [o_def] "( *f* f) o ( *fcR* g) = ( *fcR* (f o g))";
|
|
334 |
by (simp_tac (simpset() addsimps [starfun_starfunCR_o2]) 1);
|
|
335 |
qed "starfun_starfunCR_o";
|
|
336 |
|
|
337 |
Goal "( *fc* (%x. k)) z = hcomplex_of_complex k";
|
|
338 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
339 |
by (auto_tac (claset(), simpset() addsimps [starfunC, hcomplex_of_complex_def]));
|
|
340 |
qed "starfunC_const_fun";
|
|
341 |
Addsimps [starfunC_const_fun];
|
|
342 |
|
|
343 |
Goal "( *fRc* (%x. k)) z = hcomplex_of_complex k";
|
|
344 |
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
|
|
345 |
by (auto_tac (claset(), simpset() addsimps [starfunRC, hcomplex_of_complex_def]));
|
|
346 |
qed "starfunRC_const_fun";
|
|
347 |
Addsimps [starfunRC_const_fun];
|
|
348 |
|
|
349 |
Goal "( *fcR* (%x. k)) z = hypreal_of_real k";
|
|
350 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
351 |
by (auto_tac (claset(), simpset() addsimps [starfunCR, hypreal_of_real_def]));
|
|
352 |
qed "starfunCR_const_fun";
|
|
353 |
Addsimps [starfunCR_const_fun];
|
|
354 |
|
|
355 |
Goal "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x";
|
|
356 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
357 |
by (auto_tac (claset(), simpset() addsimps [starfunC, hcomplex_inverse]));
|
|
358 |
qed "starfunC_inverse";
|
|
359 |
Addsimps [starfunC_inverse RS sym];
|
|
360 |
|
|
361 |
Goal "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x";
|
|
362 |
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
|
|
363 |
by (auto_tac (claset(), simpset() addsimps [starfunRC, hcomplex_inverse]));
|
|
364 |
qed "starfunRC_inverse";
|
|
365 |
Addsimps [starfunRC_inverse RS sym];
|
|
366 |
|
|
367 |
Goal "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x";
|
|
368 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
369 |
by (auto_tac (claset(), simpset() addsimps [starfunCR, hypreal_inverse]));
|
|
370 |
qed "starfunCR_inverse";
|
|
371 |
Addsimps [starfunCR_inverse RS sym];
|
|
372 |
|
|
373 |
Goal "( *fc* f) (hcomplex_of_complex a) = hcomplex_of_complex (f a)";
|
|
374 |
by (auto_tac (claset(),
|
|
375 |
simpset() addsimps [starfunC,hcomplex_of_complex_def]));
|
|
376 |
qed "starfunC_eq";
|
|
377 |
Addsimps [starfunC_eq];
|
|
378 |
|
|
379 |
Goal "( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)";
|
|
380 |
by (auto_tac (claset(),
|
|
381 |
simpset() addsimps [starfunRC,hcomplex_of_complex_def,hypreal_of_real_def]));
|
|
382 |
qed "starfunRC_eq";
|
|
383 |
Addsimps [starfunRC_eq];
|
|
384 |
|
|
385 |
Goal "( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)";
|
|
386 |
by (auto_tac (claset(),
|
|
387 |
simpset() addsimps [starfunCR,hcomplex_of_complex_def,hypreal_of_real_def]));
|
|
388 |
qed "starfunCR_eq";
|
|
389 |
Addsimps [starfunCR_eq];
|
|
390 |
|
|
391 |
Goal "( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)";
|
|
392 |
by (Auto_tac);
|
|
393 |
qed "starfunC_capprox";
|
|
394 |
|
|
395 |
Goal "( *fRc* f) (hypreal_of_real a) @c= hcomplex_of_complex (f a)";
|
|
396 |
by (Auto_tac);
|
|
397 |
qed "starfunRC_capprox";
|
|
398 |
|
|
399 |
Goal "( *fcR* f) (hcomplex_of_complex a) @= hypreal_of_real (f a)";
|
|
400 |
by (Auto_tac);
|
|
401 |
qed "starfunCR_approx";
|
|
402 |
|
|
403 |
(*
|
|
404 |
Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N";
|
|
405 |
*)
|
|
406 |
|
|
407 |
Goalw [hypnat_of_nat_def]
|
|
408 |
"( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n";
|
|
409 |
by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1);
|
|
410 |
by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC]));
|
|
411 |
qed "starfunC_hcpow";
|
|
412 |
|
|
413 |
Goal "( *fc* (%h. f (x + h))) xa = ( *fc* f) (hcomplex_of_complex x + xa)";
|
|
414 |
by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1);
|
|
415 |
by (auto_tac (claset(),simpset() addsimps [starfunC,
|
|
416 |
hcomplex_of_complex_def,hcomplex_add]));
|
|
417 |
qed "starfunC_lambda_cancel";
|
|
418 |
|
|
419 |
Goal "( *fcR* (%h. f (x + h))) xa = ( *fcR* f) (hcomplex_of_complex x + xa)";
|
|
420 |
by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1);
|
|
421 |
by (auto_tac (claset(),simpset() addsimps [starfunCR,
|
|
422 |
hcomplex_of_complex_def,hcomplex_add]));
|
|
423 |
qed "starfunCR_lambda_cancel";
|
|
424 |
|
|
425 |
Goal "( *fRc* (%h. f (x + h))) xa = ( *fRc* f) (hypreal_of_real x + xa)";
|
|
426 |
by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
|
|
427 |
by (auto_tac (claset(),simpset() addsimps [starfunRC,
|
|
428 |
hypreal_of_real_def,hypreal_add]));
|
|
429 |
qed "starfunRC_lambda_cancel";
|
|
430 |
|
|
431 |
Goal "( *fc* (%h. f(g(x + h)))) xa = ( *fc* (f o g)) (hcomplex_of_complex x + xa)";
|
|
432 |
by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1);
|
|
433 |
by (auto_tac (claset(),simpset() addsimps [starfunC,
|
|
434 |
hcomplex_of_complex_def,hcomplex_add]));
|
|
435 |
qed "starfunC_lambda_cancel2";
|
|
436 |
|
|
437 |
Goal "( *fcR* (%h. f(g(x + h)))) xa = ( *fcR* (f o g)) (hcomplex_of_complex x + xa)";
|
|
438 |
by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1);
|
|
439 |
by (auto_tac (claset(),simpset() addsimps [starfunCR,
|
|
440 |
hcomplex_of_complex_def,hcomplex_add]));
|
|
441 |
qed "starfunCR_lambda_cancel2";
|
|
442 |
|
|
443 |
Goal "( *fRc* (%h. f(g(x + h)))) xa = ( *fRc* (f o g)) (hypreal_of_real x + xa)";
|
|
444 |
by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
|
|
445 |
by (auto_tac (claset(),simpset() addsimps [starfunRC,
|
|
446 |
hypreal_of_real_def,hypreal_add]));
|
|
447 |
qed "starfunRC_lambda_cancel2";
|
|
448 |
|
|
449 |
Goal "[| ( *fc* f) xa @c= l; ( *fc* g) xa @c= m; \
|
|
450 |
\ l: CFinite; m: CFinite \
|
|
451 |
\ |] ==> ( *fc* (%x. f x * g x)) xa @c= l * m";
|
|
452 |
by (dtac capprox_mult_CFinite 1);
|
|
453 |
by (REPEAT(assume_tac 1));
|
|
454 |
by (auto_tac (claset() addIs [capprox_sym RSN (2,capprox_CFinite)],
|
|
455 |
simpset()));
|
|
456 |
qed "starfunC_mult_CFinite_capprox";
|
|
457 |
|
|
458 |
Goal "[| ( *fcR* f) xa @= l; ( *fcR* g) xa @= m; \
|
|
459 |
\ l: HFinite; m: HFinite \
|
|
460 |
\ |] ==> ( *fcR* (%x. f x * g x)) xa @= l * m";
|
|
461 |
by (dtac approx_mult_HFinite 1);
|
|
462 |
by (REPEAT(assume_tac 1));
|
|
463 |
by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)],
|
|
464 |
simpset()));
|
|
465 |
qed "starfunCR_mult_HFinite_capprox";
|
|
466 |
|
|
467 |
Goal "[| ( *fRc* f) xa @c= l; ( *fRc* g) xa @c= m; \
|
|
468 |
\ l: CFinite; m: CFinite \
|
|
469 |
\ |] ==> ( *fRc* (%x. f x * g x)) xa @c= l * m";
|
|
470 |
by (dtac capprox_mult_CFinite 1);
|
|
471 |
by (REPEAT(assume_tac 1));
|
|
472 |
by (auto_tac (claset() addIs [capprox_sym RSN (2,capprox_CFinite)],
|
|
473 |
simpset()));
|
|
474 |
qed "starfunRC_mult_CFinite_capprox";
|
|
475 |
|
|
476 |
Goal "[| ( *fc* f) xa @c= l; ( *fc* g) xa @c= m \
|
|
477 |
\ |] ==> ( *fc* (%x. f x + g x)) xa @c= l + m";
|
|
478 |
by (auto_tac (claset() addIs [capprox_add], simpset()));
|
|
479 |
qed "starfunC_add_capprox";
|
|
480 |
|
|
481 |
Goal "[| ( *fRc* f) xa @c= l; ( *fRc* g) xa @c= m \
|
|
482 |
\ |] ==> ( *fRc* (%x. f x + g x)) xa @c= l + m";
|
|
483 |
by (auto_tac (claset() addIs [capprox_add], simpset()));
|
|
484 |
qed "starfunRC_add_capprox";
|
|
485 |
|
|
486 |
Goal "[| ( *fcR* f) xa @= l; ( *fcR* g) xa @= m \
|
|
487 |
\ |] ==> ( *fcR* (%x. f x + g x)) xa @= l + m";
|
|
488 |
by (auto_tac (claset() addIs [approx_add], simpset()));
|
|
489 |
qed "starfunCR_add_approx";
|
|
490 |
|
|
491 |
Goal "*fcR* cmod = hcmod";
|
|
492 |
by (rtac ext 1);
|
|
493 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
494 |
by (auto_tac (claset(),simpset() addsimps [starfunCR,hcmod]));
|
|
495 |
qed "starfunCR_cmod";
|
|
496 |
|
|
497 |
Goal "( *fc* inverse) x = inverse(x)";
|
|
498 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
499 |
by (auto_tac (claset(),simpset() addsimps [starfunC,hcomplex_inverse]));
|
|
500 |
qed "starfunC_inverse_inverse";
|
|
501 |
|
|
502 |
Goalw [hcomplex_divide_def,complex_divide_def]
|
|
503 |
"( *fc* f) xa / ( *fc* g) xa = ( *fc* (%x. f x / g x)) xa";
|
|
504 |
by Auto_tac;
|
|
505 |
qed "starfunC_divide";
|
|
506 |
Addsimps [starfunC_divide RS sym];
|
|
507 |
|
|
508 |
Goalw [hypreal_divide_def,real_divide_def]
|
|
509 |
"( *fcR* f) xa / ( *fcR* g) xa = ( *fcR* (%x. f x / g x)) xa";
|
|
510 |
by Auto_tac;
|
|
511 |
qed "starfunCR_divide";
|
|
512 |
Addsimps [starfunCR_divide RS sym];
|
|
513 |
|
|
514 |
Goalw [hcomplex_divide_def,complex_divide_def]
|
|
515 |
"( *fRc* f) xa / ( *fRc* g) xa = ( *fRc* (%x. f x / g x)) xa";
|
|
516 |
by Auto_tac;
|
|
517 |
qed "starfunRC_divide";
|
|
518 |
Addsimps [starfunRC_divide RS sym];
|
|
519 |
|
|
520 |
(*-----------------------------------------------------------------------------------*)
|
|
521 |
(* Internal functions - some redundancy with *fc* now *)
|
|
522 |
(*-----------------------------------------------------------------------------------*)
|
|
523 |
|
|
524 |
Goalw [congruent_def]
|
|
525 |
"congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})";
|
|
526 |
by (safe_tac (claset()));
|
|
527 |
by (ALLGOALS(Fuf_tac));
|
|
528 |
qed "starfunC_n_congruent";
|
|
529 |
|
|
530 |
Goalw [starfunC_n_def]
|
|
531 |
"( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \
|
|
532 |
\ Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})";
|
|
533 |
by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
|
|
534 |
by Auto_tac;
|
|
535 |
by (Ultra_tac 1);
|
|
536 |
qed "starfunC_n";
|
|
537 |
|
|
538 |
(** multiplication: ( *fn ) x ( *gn ) = *(fn x gn) **)
|
|
539 |
|
|
540 |
Goal "( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z";
|
|
541 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
542 |
by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_mult]));
|
|
543 |
qed "starfunC_n_mult";
|
|
544 |
|
|
545 |
(** addition: ( *fn ) + ( *gn ) = *(fn + gn) **)
|
|
546 |
|
|
547 |
Goal "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z";
|
|
548 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
549 |
by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_add]));
|
|
550 |
qed "starfunC_n_add";
|
|
551 |
|
|
552 |
(** uminus **)
|
|
553 |
|
|
554 |
Goal "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z";
|
|
555 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
556 |
by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_minus]));
|
|
557 |
qed "starfunC_n_minus";
|
|
558 |
|
|
559 |
(** subtraction: ( *fn ) - ( *gn ) = *(fn - gn) **)
|
|
560 |
|
|
561 |
Goalw [hcomplex_diff_def,complex_diff_def]
|
|
562 |
"( *fcn* f) z - ( *fcn* g) z = ( *fcn* (%i x. f i x - g i x)) z";
|
|
563 |
by (auto_tac (claset(),
|
|
564 |
simpset() addsimps [starfunC_n_add,starfunC_n_minus]));
|
|
565 |
qed "starfunNat_n_diff";
|
|
566 |
|
|
567 |
(** composition: ( *fn ) o ( *gn ) = *(fn o gn) **)
|
|
568 |
|
|
569 |
Goal "( *fcn* (%i x. k)) z = hcomplex_of_complex k";
|
|
570 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
571 |
by (auto_tac (claset(),
|
|
572 |
simpset() addsimps [starfunC_n, hcomplex_of_complex_def]));
|
|
573 |
qed "starfunC_n_const_fun";
|
|
574 |
Addsimps [starfunC_n_const_fun];
|
|
575 |
|
|
576 |
Goal "( *fcn* f) (hcomplex_of_complex n) = Abs_hcomplex(hcomplexrel `` {%i. f i n})";
|
|
577 |
by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_of_complex_def]));
|
|
578 |
qed "starfunC_n_eq";
|
|
579 |
Addsimps [starfunC_n_eq];
|
|
580 |
|
|
581 |
Goal "(( *fc* f) = ( *fc* g)) = (f = g)";
|
|
582 |
by Auto_tac;
|
|
583 |
by (rtac ext 1 THEN rtac ccontr 1);
|
|
584 |
by (dres_inst_tac [("x","hcomplex_of_complex(x)")] fun_cong 1);
|
|
585 |
by (auto_tac (claset(), simpset() addsimps [starfunC,hcomplex_of_complex_def]));
|
|
586 |
qed "starfunC_eq_iff";
|
|
587 |
|
|
588 |
Goal "(( *fRc* f) = ( *fRc* g)) = (f = g)";
|
|
589 |
by Auto_tac;
|
|
590 |
by (rtac ext 1 THEN rtac ccontr 1);
|
|
591 |
by (dres_inst_tac [("x","hypreal_of_real(x)")] fun_cong 1);
|
|
592 |
by Auto_tac;
|
|
593 |
qed "starfunRC_eq_iff";
|
|
594 |
|
|
595 |
Goal "(( *fcR* f) = ( *fcR* g)) = (f = g)";
|
|
596 |
by Auto_tac;
|
|
597 |
by (rtac ext 1 THEN rtac ccontr 1);
|
|
598 |
by (dres_inst_tac [("x","hcomplex_of_complex(x)")] fun_cong 1);
|
|
599 |
by Auto_tac;
|
|
600 |
qed "starfunCR_eq_iff";
|
|
601 |
|
|
602 |
(*** more theorems ***)
|
|
603 |
|
|
604 |
Goal "(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) & \
|
|
605 |
\ (( *fcR* (%x. Im(f x))) x = hIm (z)))";
|
|
606 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
607 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
608 |
by (auto_tac (claset(),simpset() addsimps [starfunCR,starfunC,
|
|
609 |
hIm,hRe,complex_Re_Im_cancel_iff]));
|
|
610 |
by (ALLGOALS(Ultra_tac));
|
|
611 |
qed "starfunC_eq_Re_Im_iff";
|
|
612 |
|
|
613 |
Goal "(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) & \
|
|
614 |
\ (( *fcR* (%x. Im(f x))) x @= hIm (z)))";
|
|
615 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
616 |
by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1);
|
|
617 |
by (auto_tac (claset(),simpset() addsimps [starfunCR,starfunC,
|
|
618 |
hIm,hRe,capprox_approx_iff]));
|
|
619 |
qed "starfunC_approx_Re_Im_iff";
|
|
620 |
|
|
621 |
Goal "x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex a";
|
|
622 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
623 |
by (auto_tac (claset(),simpset() addsimps [starfunC]));
|
|
624 |
qed "starfunC_Idfun_capprox";
|
|
625 |
|
|
626 |
Goal "( *fc* (%x. x)) x = x";
|
|
627 |
by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1);
|
|
628 |
by (auto_tac (claset(),simpset() addsimps [starfunC]));
|
|
629 |
qed "starfunC_Id";
|
|
630 |
Addsimps [starfunC_Id];
|