1 (* Title: NSComplex.ML |
|
2 Author: Jacques D. Fleuriot |
|
3 Copyhright: 2001 University of Edinburgh |
|
4 Description: Nonstandard Complex numbers |
|
5 *) |
|
6 |
|
7 Goalw [hcomplexrel_def] |
|
8 "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"; |
|
9 by (Fast_tac 1); |
|
10 qed "hcomplexrel_iff"; |
|
11 |
|
12 Goalw [hcomplexrel_def] |
|
13 "!!X. {n. X n = Y n}: FreeUltrafilterNat \ |
|
14 \ ==> (X,Y): hcomplexrel"; |
|
15 by (Fast_tac 1); |
|
16 qed "hcomplexrelI"; |
|
17 |
|
18 Goalw [hcomplexrel_def] |
|
19 "p: hcomplexrel --> (EX X Y. \ |
|
20 \ p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)"; |
|
21 by (Fast_tac 1); |
|
22 qed "hcomplexrelE_lemma"; |
|
23 |
|
24 val [major,minor] = goal thy |
|
25 "[| p: hcomplexrel; \ |
|
26 \ !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\ |
|
27 \ |] ==> Q |] ==> Q"; |
|
28 by (cut_facts_tac [major RS (hcomplexrelE_lemma RS mp)] 1); |
|
29 by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); |
|
30 qed "hcomplexrelE"; |
|
31 |
|
32 AddSIs [hcomplexrelI]; |
|
33 AddSEs [hcomplexrelE]; |
|
34 |
|
35 Goalw [hcomplexrel_def] "(x,x): hcomplexrel"; |
|
36 by (Auto_tac); |
|
37 qed "hcomplexrel_refl"; |
|
38 |
|
39 Goalw [hcomplexrel_def] "(x,y): hcomplexrel ==> (y,x):hcomplexrel"; |
|
40 by (auto_tac (claset(), simpset() addsimps [eq_commute])); |
|
41 qed "hcomplexrel_sym"; |
|
42 |
|
43 Goalw [hcomplexrel_def] |
|
44 "(x,y): hcomplexrel --> (y,z):hcomplexrel --> (x,z):hcomplexrel"; |
|
45 by (Auto_tac); |
|
46 by (Ultra_tac 1); |
|
47 qed_spec_mp "hcomplexrel_trans"; |
|
48 |
|
49 Goalw [equiv_def, refl_def, sym_def, trans_def] |
|
50 "equiv {x::nat=>complex. True} hcomplexrel"; |
|
51 by (auto_tac (claset() addSIs [hcomplexrel_refl] addSEs |
|
52 [hcomplexrel_sym,hcomplexrel_trans] delrules [hcomplexrelI,hcomplexrelE], |
|
53 simpset())); |
|
54 qed "equiv_hcomplexrel"; |
|
55 |
|
56 val equiv_hcomplexrel_iff = |
|
57 [TrueI, TrueI] MRS |
|
58 ([CollectI, CollectI] MRS |
|
59 (equiv_hcomplexrel RS eq_equiv_class_iff)); |
|
60 |
|
61 Goalw [hcomplex_def,hcomplexrel_def,quotient_def] "hcomplexrel``{x}:hcomplex"; |
|
62 by (Blast_tac 1); |
|
63 qed "hcomplexrel_in_hcomplex"; |
|
64 |
|
65 Goal "inj_on Abs_hcomplex hcomplex"; |
|
66 by (rtac inj_on_inverseI 1); |
|
67 by (etac Abs_hcomplex_inverse 1); |
|
68 qed "inj_on_Abs_hcomplex"; |
|
69 |
|
70 Addsimps [equiv_hcomplexrel_iff,inj_on_Abs_hcomplex RS inj_on_iff, |
|
71 hcomplexrel_iff, hcomplexrel_in_hcomplex, Abs_hcomplex_inverse]; |
|
72 |
|
73 Addsimps [equiv_hcomplexrel RS eq_equiv_class_iff]; |
|
74 val eq_hcomplexrelD = equiv_hcomplexrel RSN (2,eq_equiv_class); |
|
75 |
|
76 Goal "inj(Rep_hcomplex)"; |
|
77 by (rtac inj_inverseI 1); |
|
78 by (rtac Rep_hcomplex_inverse 1); |
|
79 qed "inj_Rep_hcomplex"; |
|
80 |
|
81 Goalw [hcomplexrel_def] "x: hcomplexrel `` {x}"; |
|
82 by (Step_tac 1); |
|
83 by (Auto_tac); |
|
84 qed "lemma_hcomplexrel_refl"; |
|
85 Addsimps [lemma_hcomplexrel_refl]; |
|
86 |
|
87 Goalw [hcomplex_def] "{} ~: hcomplex"; |
|
88 by (auto_tac (claset() addSEs [quotientE],simpset())); |
|
89 qed "hcomplex_empty_not_mem"; |
|
90 Addsimps [hcomplex_empty_not_mem]; |
|
91 |
|
92 Goal "Rep_hcomplex x ~= {}"; |
|
93 by (cut_inst_tac [("x","x")] Rep_hcomplex 1); |
|
94 by (Auto_tac); |
|
95 qed "Rep_hcomplex_nonempty"; |
|
96 Addsimps [Rep_hcomplex_nonempty]; |
|
97 |
|
98 val [prem] = goal thy |
|
99 "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"; |
|
100 by (res_inst_tac [("x1","z")] |
|
101 (rewrite_rule [hcomplex_def] Rep_hcomplex RS quotientE) 1); |
|
102 by (dres_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
103 by (res_inst_tac [("x","x")] prem 1); |
|
104 by (asm_full_simp_tac (simpset() addsimps [Rep_hcomplex_inverse]) 1); |
|
105 qed "eq_Abs_hcomplex"; |
|
106 |
|
107 (*-----------------------------------------------------------------------*) |
|
108 (* Properties of nonstandard real and imaginary parts *) |
|
109 (*-----------------------------------------------------------------------*) |
|
110 |
|
111 Goalw [hRe_def] |
|
112 "hRe(Abs_hcomplex (hcomplexrel `` {X})) = \ |
|
113 \ Abs_hypreal(hyprel `` {%n. Re(X n)})"; |
|
114 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
115 by (Auto_tac THEN Ultra_tac 1); |
|
116 qed "hRe"; |
|
117 |
|
118 Goalw [hIm_def] |
|
119 "hIm(Abs_hcomplex (hcomplexrel `` {X})) = \ |
|
120 \ Abs_hypreal(hyprel `` {%n. Im(X n)})"; |
|
121 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
122 by (Auto_tac THEN Ultra_tac 1); |
|
123 qed "hIm"; |
|
124 |
|
125 Goal "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"; |
|
126 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
127 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
128 by (auto_tac (claset(),simpset() addsimps [hRe,hIm, |
|
129 complex_Re_Im_cancel_iff])); |
|
130 by (ALLGOALS(Ultra_tac)); |
|
131 qed "hcomplex_hRe_hIm_cancel_iff"; |
|
132 |
|
133 Goalw [hcomplex_zero_def] "hRe 0 = 0"; |
|
134 by (simp_tac (simpset() addsimps [hRe,hypreal_zero_num]) 1); |
|
135 qed "hcomplex_hRe_zero"; |
|
136 Addsimps [hcomplex_hRe_zero]; |
|
137 |
|
138 Goalw [hcomplex_zero_def] "hIm 0 = 0"; |
|
139 by (simp_tac (simpset() addsimps [hIm,hypreal_zero_num]) 1); |
|
140 qed "hcomplex_hIm_zero"; |
|
141 Addsimps [hcomplex_hIm_zero]; |
|
142 |
|
143 Goalw [hcomplex_one_def] "hRe 1 = 1"; |
|
144 by (simp_tac (simpset() addsimps [hRe,hypreal_one_num]) 1); |
|
145 qed "hcomplex_hRe_one"; |
|
146 Addsimps [hcomplex_hRe_one]; |
|
147 |
|
148 Goalw [hcomplex_one_def] "hIm 1 = 0"; |
|
149 by (simp_tac (simpset() addsimps [hIm,hypreal_one_def,hypreal_zero_num]) 1); |
|
150 qed "hcomplex_hIm_one"; |
|
151 Addsimps [hcomplex_hIm_one]; |
|
152 |
|
153 (*-----------------------------------------------------------------------*) |
|
154 (* hcomplex_of_complex: the injection from complex to hcomplex *) |
|
155 (* ----------------------------------------------------------------------*) |
|
156 |
|
157 Goal "inj(hcomplex_of_complex)"; |
|
158 by (rtac injI 1 THEN rtac ccontr 1); |
|
159 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_def])); |
|
160 qed "inj_hcomplex_of_complex"; |
|
161 |
|
162 Goalw [iii_def,hcomplex_of_complex_def] "iii = hcomplex_of_complex ii"; |
|
163 by (Simp_tac 1); |
|
164 qed "hcomplex_of_complex_i"; |
|
165 |
|
166 (*-----------------------------------------------------------------------*) |
|
167 (* Addition for nonstandard complex numbers: hcomplex_add *) |
|
168 (* ----------------------------------------------------------------------*) |
|
169 |
|
170 Goalw [congruent2_def] |
|
171 "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"; |
|
172 by (safe_tac (claset())); |
|
173 by (ALLGOALS(Ultra_tac)); |
|
174 qed "hcomplex_add_congruent2"; |
|
175 |
|
176 Goalw [hcomplex_add_def] |
|
177 "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) = \ |
|
178 \ Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"; |
|
179 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
180 by Auto_tac; |
|
181 by (Ultra_tac 1); |
|
182 qed "hcomplex_add"; |
|
183 |
|
184 Goal "(z::hcomplex) + w = w + z"; |
|
185 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
186 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
187 by (asm_simp_tac (simpset() addsimps (complex_add_ac @ [hcomplex_add])) 1); |
|
188 qed "hcomplex_add_commute"; |
|
189 |
|
190 Goal "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"; |
|
191 by (res_inst_tac [("z","z1")] eq_Abs_hcomplex 1); |
|
192 by (res_inst_tac [("z","z2")] eq_Abs_hcomplex 1); |
|
193 by (res_inst_tac [("z","z3")] eq_Abs_hcomplex 1); |
|
194 by (asm_simp_tac (simpset() addsimps [hcomplex_add,complex_add_assoc]) 1); |
|
195 qed "hcomplex_add_assoc"; |
|
196 |
|
197 (*For AC rewriting*) |
|
198 Goal "(x::hcomplex)+(y+z)=y+(x+z)"; |
|
199 by (rtac (hcomplex_add_commute RS trans) 1); |
|
200 by (rtac (hcomplex_add_assoc RS trans) 1); |
|
201 by (rtac (hcomplex_add_commute RS arg_cong) 1); |
|
202 qed "hcomplex_add_left_commute"; |
|
203 |
|
204 (* hcomplex addition is an AC operator *) |
|
205 val hcomplex_add_ac = [hcomplex_add_assoc,hcomplex_add_commute, |
|
206 hcomplex_add_left_commute]; |
|
207 |
|
208 Goalw [hcomplex_zero_def] "(0::hcomplex) + z = z"; |
|
209 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
210 by (asm_full_simp_tac (simpset() addsimps |
|
211 [hcomplex_add]) 1); |
|
212 qed "hcomplex_add_zero_left"; |
|
213 |
|
214 Goal "z + (0::hcomplex) = z"; |
|
215 by (simp_tac (simpset() addsimps |
|
216 [hcomplex_add_zero_left,hcomplex_add_commute]) 1); |
|
217 qed "hcomplex_add_zero_right"; |
|
218 Addsimps [hcomplex_add_zero_left,hcomplex_add_zero_right]; |
|
219 |
|
220 Goal "hRe(x + y) = hRe(x) + hRe(y)"; |
|
221 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
222 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
223 by (auto_tac (claset(),simpset() addsimps [hRe,hcomplex_add, |
|
224 hypreal_add,complex_Re_add])); |
|
225 qed "hRe_add"; |
|
226 |
|
227 Goal "hIm(x + y) = hIm(x) + hIm(y)"; |
|
228 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
229 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
230 by (auto_tac (claset(),simpset() addsimps [hIm,hcomplex_add, |
|
231 hypreal_add,complex_Im_add])); |
|
232 qed "hIm_add"; |
|
233 |
|
234 (*-----------------------------------------------------------------------*) |
|
235 (* hypreal_minus: additive inverse on nonstandard complex *) |
|
236 (* ----------------------------------------------------------------------*) |
|
237 |
|
238 Goalw [congruent_def] |
|
239 "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"; |
|
240 by (safe_tac (claset())); |
|
241 by (ALLGOALS(Ultra_tac)); |
|
242 qed "hcomplex_minus_congruent"; |
|
243 |
|
244 Goalw [hcomplex_minus_def] |
|
245 "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) = \ |
|
246 \ Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"; |
|
247 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
248 by (Auto_tac THEN Ultra_tac 1); |
|
249 qed "hcomplex_minus"; |
|
250 |
|
251 Goal "- (- z) = (z::hcomplex)"; |
|
252 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
253 by (asm_simp_tac (simpset() addsimps [hcomplex_minus]) 1); |
|
254 qed "hcomplex_minus_minus"; |
|
255 Addsimps [hcomplex_minus_minus]; |
|
256 |
|
257 Goal "inj(%z::hcomplex. -z)"; |
|
258 by (rtac injI 1); |
|
259 by (dres_inst_tac [("f","uminus")] arg_cong 1); |
|
260 by (Asm_full_simp_tac 1); |
|
261 qed "inj_hcomplex_minus"; |
|
262 |
|
263 Goalw [hcomplex_zero_def] "- 0 = (0::hcomplex)"; |
|
264 by (simp_tac (simpset() addsimps [hcomplex_minus]) 1); |
|
265 qed "hcomplex_minus_zero"; |
|
266 Addsimps [hcomplex_minus_zero]; |
|
267 |
|
268 Goal "(-x = 0) = (x = (0::hcomplex))"; |
|
269 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
270 by (auto_tac (claset(),simpset() addsimps [hcomplex_zero_def, |
|
271 hcomplex_minus] @ complex_add_ac)); |
|
272 qed "hcomplex_minus_zero_iff"; |
|
273 Addsimps [hcomplex_minus_zero_iff]; |
|
274 |
|
275 Goal "(0 = -x) = (x = (0::hcomplex))"; |
|
276 by (auto_tac (claset() addDs [sym],simpset())); |
|
277 qed "hcomplex_minus_zero_iff2"; |
|
278 Addsimps [hcomplex_minus_zero_iff2]; |
|
279 |
|
280 Goal "(-x ~= 0) = (x ~= (0::hcomplex))"; |
|
281 by Auto_tac; |
|
282 qed "hcomplex_minus_not_zero_iff"; |
|
283 |
|
284 Goal "z + - z = (0::hcomplex)"; |
|
285 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
286 by (auto_tac (claset(),simpset() addsimps [hcomplex_add,hcomplex_minus, |
|
287 hcomplex_zero_def])); |
|
288 qed "hcomplex_add_minus_right"; |
|
289 Addsimps [hcomplex_add_minus_right]; |
|
290 |
|
291 Goal "-z + z = (0::hcomplex)"; |
|
292 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
293 by (auto_tac (claset(),simpset() addsimps [hcomplex_add,hcomplex_minus, |
|
294 hcomplex_zero_def])); |
|
295 qed "hcomplex_add_minus_left"; |
|
296 Addsimps [hcomplex_add_minus_left]; |
|
297 |
|
298 Goal "z + (- z + w) = (w::hcomplex)"; |
|
299 by (simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1); |
|
300 qed "hcomplex_add_minus_cancel"; |
|
301 |
|
302 Goal "(-z) + (z + w) = (w::hcomplex)"; |
|
303 by (simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1); |
|
304 qed "hcomplex_minus_add_cancel"; |
|
305 |
|
306 Goal "hRe(-z) = - hRe(z)"; |
|
307 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
308 by (auto_tac (claset(),simpset() addsimps [hRe,hcomplex_minus, |
|
309 hypreal_minus,complex_Re_minus])); |
|
310 qed "hRe_minus"; |
|
311 |
|
312 Goal "hIm(-z) = - hIm(z)"; |
|
313 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
314 by (auto_tac (claset(),simpset() addsimps [hIm,hcomplex_minus, |
|
315 hypreal_minus,complex_Im_minus])); |
|
316 qed "hIm_minus"; |
|
317 |
|
318 Goalw [hcomplex_zero_def] |
|
319 "x + y = (0::hcomplex) ==> x = -y"; |
|
320 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
321 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
322 by (auto_tac (claset(),simpset() addsimps [hcomplex_add,hcomplex_minus])); |
|
323 by (ultra_tac (claset() addIs [complex_add_minus_eq_minus],simpset()) 1); |
|
324 qed "hcomplex_add_minus_eq_minus"; |
|
325 |
|
326 Goal "-(x + y) = -x + -(y::hcomplex)"; |
|
327 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
328 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
329 by (auto_tac (claset(),simpset() addsimps [hcomplex_add,hcomplex_minus])); |
|
330 qed "hcomplex_minus_add_distrib"; |
|
331 Addsimps [hcomplex_minus_add_distrib]; |
|
332 |
|
333 Goal "((x::hcomplex) + y = x + z) = (y = z)"; |
|
334 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
335 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
336 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
337 by (auto_tac (claset(),simpset() addsimps [hcomplex_add])); |
|
338 qed "hcomplex_add_left_cancel"; |
|
339 AddIffs [hcomplex_add_left_cancel]; |
|
340 |
|
341 Goal "(y + (x::hcomplex)= z + x) = (y = z)"; |
|
342 by (simp_tac (simpset() addsimps [hcomplex_add_commute]) 1); |
|
343 qed "hcomplex_add_right_cancel"; |
|
344 AddIffs [hcomplex_add_right_cancel]; |
|
345 |
|
346 Goal "((x::hcomplex) = y) = ((0::hcomplex) = x + - y)"; |
|
347 by (Step_tac 1); |
|
348 by (res_inst_tac [("x1","-y")] |
|
349 (hcomplex_add_right_cancel RS iffD1) 2); |
|
350 by (Auto_tac); |
|
351 qed "hcomplex_eq_minus_iff"; |
|
352 |
|
353 Goal "((x::hcomplex) = y) = (x + - y = (0::hcomplex))"; |
|
354 by (Step_tac 1); |
|
355 by (res_inst_tac [("x1","-y")] |
|
356 (hcomplex_add_right_cancel RS iffD1) 2); |
|
357 by (Auto_tac); |
|
358 qed "hcomplex_eq_minus_iff2"; |
|
359 |
|
360 (*-----------------------------------------------------------------------*) |
|
361 (* Subraction for nonstandard complex numbers: hcomplex_diff *) |
|
362 (* ----------------------------------------------------------------------*) |
|
363 |
|
364 Goalw [hcomplex_diff_def] |
|
365 "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) = \ |
|
366 \ Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"; |
|
367 by (auto_tac (claset(),simpset() addsimps [hcomplex_minus,hcomplex_add, |
|
368 complex_diff_def])); |
|
369 qed "hcomplex_diff"; |
|
370 |
|
371 Goalw [hcomplex_diff_def] "(z::hcomplex) - z = (0::hcomplex)"; |
|
372 by (Simp_tac 1); |
|
373 qed "hcomplex_diff_zero"; |
|
374 Addsimps [hcomplex_diff_zero]; |
|
375 |
|
376 Goal "(0::hcomplex) - x = -x"; |
|
377 by (simp_tac (simpset() addsimps [hcomplex_diff_def]) 1); |
|
378 qed "hcomplex_diff_0"; |
|
379 |
|
380 Goal "x - (0::hcomplex) = x"; |
|
381 by (simp_tac (simpset() addsimps [hcomplex_diff_def]) 1); |
|
382 qed "hcomplex_diff_0_right"; |
|
383 |
|
384 Goal "x - x = (0::hcomplex)"; |
|
385 by (simp_tac (simpset() addsimps [hcomplex_diff_def]) 1); |
|
386 qed "hcomplex_diff_self"; |
|
387 |
|
388 Addsimps [hcomplex_diff_0, hcomplex_diff_0_right, hcomplex_diff_self]; |
|
389 |
|
390 Goal "((x::hcomplex) - y = z) = (x = z + y)"; |
|
391 by (auto_tac (claset(),simpset() addsimps [hcomplex_diff_def,hcomplex_add_assoc])); |
|
392 qed "hcomplex_diff_eq_eq"; |
|
393 |
|
394 (*-----------------------------------------------------------------------*) |
|
395 (* Multiplication for nonstandard complex numbers: hcomplex_mult *) |
|
396 (* ----------------------------------------------------------------------*) |
|
397 |
|
398 Goalw [hcomplex_mult_def] |
|
399 "Abs_hcomplex(hcomplexrel``{%n. X n}) * Abs_hcomplex(hcomplexrel``{%n. Y n}) = \ |
|
400 \ Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"; |
|
401 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
402 by (Auto_tac THEN Ultra_tac 1); |
|
403 qed "hcomplex_mult"; |
|
404 |
|
405 Goal "(w::hcomplex) * z = z * w"; |
|
406 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
407 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
408 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult, |
|
409 complex_mult_commute])); |
|
410 qed "hcomplex_mult_commute"; |
|
411 |
|
412 Goal "((u::hcomplex) * v) * w = u * (v * w)"; |
|
413 by (res_inst_tac [("z","u")] eq_Abs_hcomplex 1); |
|
414 by (res_inst_tac [("z","v")] eq_Abs_hcomplex 1); |
|
415 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
416 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult, |
|
417 complex_mult_assoc])); |
|
418 qed "hcomplex_mult_assoc"; |
|
419 |
|
420 Goal "(x::hcomplex) * (y * z) = y * (x * z)"; |
|
421 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
422 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
423 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
424 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult, |
|
425 complex_mult_left_commute])); |
|
426 qed "hcomplex_mult_left_commute"; |
|
427 |
|
428 val hcomplex_mult_ac = [hcomplex_mult_assoc,hcomplex_mult_commute, |
|
429 hcomplex_mult_left_commute]; |
|
430 |
|
431 Goalw [hcomplex_one_def] "(1::hcomplex) * z = z"; |
|
432 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
433 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult])); |
|
434 qed "hcomplex_mult_one_left"; |
|
435 Addsimps [hcomplex_mult_one_left]; |
|
436 |
|
437 Goal "z * (1::hcomplex) = z"; |
|
438 by (simp_tac (simpset() addsimps [hcomplex_mult_commute]) 1); |
|
439 qed "hcomplex_mult_one_right"; |
|
440 Addsimps [hcomplex_mult_one_right]; |
|
441 |
|
442 Goalw [hcomplex_zero_def] "(0::hcomplex) * z = 0"; |
|
443 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
444 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult])); |
|
445 qed "hcomplex_mult_zero_left"; |
|
446 Addsimps [hcomplex_mult_zero_left]; |
|
447 |
|
448 Goal "z * (0::hcomplex) = 0"; |
|
449 by (simp_tac (simpset() addsimps [hcomplex_mult_commute]) 1); |
|
450 qed "hcomplex_mult_zero_right"; |
|
451 Addsimps [hcomplex_mult_zero_right]; |
|
452 |
|
453 Goal "-(x * y) = -x * (y::hcomplex)"; |
|
454 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
455 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
456 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult, |
|
457 hcomplex_minus])); |
|
458 qed "hcomplex_minus_mult_eq1"; |
|
459 |
|
460 Goal "-(x * y) = x * -(y::hcomplex)"; |
|
461 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
462 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
463 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult, |
|
464 hcomplex_minus])); |
|
465 qed "hcomplex_minus_mult_eq2"; |
|
466 |
|
467 Addsimps [hcomplex_minus_mult_eq1 RS sym,hcomplex_minus_mult_eq2 RS sym]; |
|
468 |
|
469 Goal "- 1 * (z::hcomplex) = -z"; |
|
470 by (Simp_tac 1); |
|
471 qed "hcomplex_mult_minus_one"; |
|
472 Addsimps [hcomplex_mult_minus_one]; |
|
473 |
|
474 Goal "(z::hcomplex) * - 1 = -z"; |
|
475 by (stac hcomplex_mult_commute 1); |
|
476 by (Simp_tac 1); |
|
477 qed "hcomplex_mult_minus_one_right"; |
|
478 Addsimps [hcomplex_mult_minus_one_right]; |
|
479 |
|
480 Goal "-x * -y = x * (y::hcomplex)"; |
|
481 by Auto_tac; |
|
482 qed "hcomplex_minus_mult_cancel"; |
|
483 Addsimps [hcomplex_minus_mult_cancel]; |
|
484 |
|
485 Goal "-x * y = x * -(y::hcomplex)"; |
|
486 by Auto_tac; |
|
487 qed "hcomplex_minus_mult_commute"; |
|
488 |
|
489 qed_goal "hcomplex_add_assoc_cong" thy |
|
490 "!!z. (z::hcomplex) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" |
|
491 (fn _ => [(asm_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 1)]); |
|
492 |
|
493 qed_goal "hcomplex_add_assoc_swap" thy "(z::hcomplex) + (v + w) = v + (z + w)" |
|
494 (fn _ => [(REPEAT (ares_tac [hcomplex_add_commute RS hcomplex_add_assoc_cong] 1))]); |
|
495 |
|
496 Goal "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"; |
|
497 by (res_inst_tac [("z","z1")] eq_Abs_hcomplex 1); |
|
498 by (res_inst_tac [("z","z2")] eq_Abs_hcomplex 1); |
|
499 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
500 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult,hcomplex_add, |
|
501 complex_add_mult_distrib])); |
|
502 qed "hcomplex_add_mult_distrib"; |
|
503 |
|
504 Goal "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)"; |
|
505 by (res_inst_tac [("z1","z1 + z2")] (hcomplex_mult_commute RS ssubst) 1); |
|
506 by (simp_tac (simpset() addsimps [hcomplex_add_mult_distrib]) 1); |
|
507 by (simp_tac (simpset() addsimps [hcomplex_mult_commute]) 1); |
|
508 qed "hcomplex_add_mult_distrib2"; |
|
509 |
|
510 Goalw [hcomplex_zero_def,hcomplex_one_def] "(0::hcomplex) ~= (1::hcomplex)"; |
|
511 by Auto_tac; |
|
512 qed "hcomplex_zero_not_eq_one"; |
|
513 Addsimps [hcomplex_zero_not_eq_one]; |
|
514 Addsimps [hcomplex_zero_not_eq_one RS not_sym]; |
|
515 |
|
516 (*-----------------------------------------------------------------------*) |
|
517 (* Inverse of nonstandard complex number *) |
|
518 (*-----------------------------------------------------------------------*) |
|
519 |
|
520 Goalw [hcinv_def] |
|
521 "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) = \ |
|
522 \ Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"; |
|
523 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
524 by (Auto_tac THEN Ultra_tac 1); |
|
525 qed "hcomplex_inverse"; |
|
526 |
|
527 Goalw [hcomplex_zero_def] "inverse (0::hcomplex) = 0"; |
|
528 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse])); |
|
529 qed "HCOMPLEX_INVERSE_ZERO"; |
|
530 |
|
531 Goal "a / (0::hcomplex) = 0"; |
|
532 by (simp_tac (simpset() addsimps [hcomplex_divide_def, HCOMPLEX_INVERSE_ZERO]) 1); |
|
533 qed "HCOMPLEX_DIVISION_BY_ZERO"; (*NOT for adding to default simpset*) |
|
534 |
|
535 fun hcomplex_div_undefined_case_tac s i = |
|
536 case_tac s i THEN |
|
537 asm_simp_tac (simpset() addsimps [HCOMPLEX_DIVISION_BY_ZERO, HCOMPLEX_INVERSE_ZERO]) i; |
|
538 |
|
539 Goalw [hcomplex_zero_def,hcomplex_one_def] |
|
540 "z ~= (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"; |
|
541 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
542 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse,hcomplex_mult])); |
|
543 by (Ultra_tac 1); |
|
544 by (rtac ccontr 1 THEN dtac (complex_mult_inv_left) 1); |
|
545 by Auto_tac; |
|
546 qed "hcomplex_mult_inv_left"; |
|
547 Addsimps [hcomplex_mult_inv_left]; |
|
548 |
|
549 Goal "z ~= (0::hcomplex) ==> z * inverse(z) = (1::hcomplex)"; |
|
550 by (auto_tac (claset() addIs [hcomplex_mult_commute RS subst],simpset())); |
|
551 qed "hcomplex_mult_inv_right"; |
|
552 Addsimps [hcomplex_mult_inv_right]; |
|
553 |
|
554 Goal "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)"; |
|
555 by Auto_tac; |
|
556 by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); |
|
557 by (asm_full_simp_tac (simpset() addsimps hcomplex_mult_ac) 1); |
|
558 qed "hcomplex_mult_left_cancel"; |
|
559 |
|
560 Goal "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)"; |
|
561 by (Step_tac 1); |
|
562 by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); |
|
563 by (asm_full_simp_tac (simpset() addsimps hcomplex_mult_ac) 1); |
|
564 qed "hcomplex_mult_right_cancel"; |
|
565 |
|
566 Goal "z ~= (0::hcomplex) ==> inverse(z) ~= 0"; |
|
567 by (Step_tac 1); |
|
568 by (ftac (hcomplex_mult_right_cancel RS iffD2) 1); |
|
569 by (thin_tac "inverse z = 0" 2); |
|
570 by (assume_tac 1 THEN Auto_tac); |
|
571 qed "hcomplex_inverse_not_zero"; |
|
572 Addsimps [hcomplex_inverse_not_zero]; |
|
573 |
|
574 Goal "[| x ~= (0::hcomplex); y ~= 0 |] ==> x * y ~= 0"; |
|
575 by (Step_tac 1); |
|
576 by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1); |
|
577 by (asm_full_simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym]) 1); |
|
578 qed "hcomplex_mult_not_zero"; |
|
579 |
|
580 bind_thm ("hcomplex_mult_not_zeroE",hcomplex_mult_not_zero RS notE); |
|
581 |
|
582 Goal "inverse(inverse x) = (x::hcomplex)"; |
|
583 by (hcomplex_div_undefined_case_tac "x = 0" 1); |
|
584 by (res_inst_tac [("c1","inverse x")] (hcomplex_mult_right_cancel RS iffD1) 1); |
|
585 by (etac hcomplex_inverse_not_zero 1); |
|
586 by (auto_tac (claset() addDs [hcomplex_inverse_not_zero],simpset())); |
|
587 qed "hcomplex_inverse_inverse"; |
|
588 Addsimps [hcomplex_inverse_inverse]; |
|
589 |
|
590 Goalw [hcomplex_one_def] "inverse((1::hcomplex)) = 1"; |
|
591 by (simp_tac (simpset() addsimps [hcomplex_inverse]) 1); |
|
592 qed "hcomplex_inverse_one"; |
|
593 Addsimps [hcomplex_inverse_one]; |
|
594 |
|
595 Goal "inverse(-x) = -inverse(x::hcomplex)"; |
|
596 by (hcomplex_div_undefined_case_tac "x = 0" 1); |
|
597 by (res_inst_tac [("c1","-x")] (hcomplex_mult_right_cancel RS iffD1) 1); |
|
598 by (stac hcomplex_mult_inv_left 2); |
|
599 by Auto_tac; |
|
600 qed "hcomplex_minus_inverse"; |
|
601 |
|
602 Goal "inverse(x*y) = inverse x * inverse (y::hcomplex)"; |
|
603 by (hcomplex_div_undefined_case_tac "x = 0" 1); |
|
604 by (hcomplex_div_undefined_case_tac "y = 0" 1); |
|
605 by (res_inst_tac [("c1","x*y")] (hcomplex_mult_left_cancel RS iffD1) 1); |
|
606 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_not_zero] |
|
607 @ hcomplex_mult_ac)); |
|
608 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_not_zero, |
|
609 hcomplex_mult_assoc RS sym])); |
|
610 qed "hcomplex_inverse_distrib"; |
|
611 |
|
612 (*** division ***) |
|
613 |
|
614 (* adding some of these theorems to simpset as for reals: not 100% convinced for some*) |
|
615 |
|
616 Goal "(x::hcomplex) * (y/z) = (x*y)/z"; |
|
617 by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 1); |
|
618 qed "hcomplex_times_divide1_eq"; |
|
619 |
|
620 Goal "(y/z) * (x::hcomplex) = (y*x)/z"; |
|
621 by (simp_tac (simpset() addsimps [hcomplex_divide_def] @ hcomplex_mult_ac) 1); |
|
622 qed "hcomplex_times_divide2_eq"; |
|
623 |
|
624 Addsimps [hcomplex_times_divide1_eq, hcomplex_times_divide2_eq]; |
|
625 |
|
626 Goal "(x::hcomplex) / (y/z) = (x*z)/y"; |
|
627 by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_inverse_distrib]@ |
|
628 hcomplex_mult_ac) 1); |
|
629 qed "hcomplex_divide_divide1_eq"; |
|
630 |
|
631 Goal "((x::hcomplex) / y) / z = x/(y*z)"; |
|
632 by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_inverse_distrib, |
|
633 hcomplex_mult_assoc]) 1); |
|
634 qed "hcomplex_divide_divide2_eq"; |
|
635 |
|
636 Addsimps [hcomplex_divide_divide1_eq, hcomplex_divide_divide2_eq]; |
|
637 |
|
638 (** As with multiplication, pull minus signs OUT of the / operator **) |
|
639 |
|
640 Goal "(-x) / (y::hcomplex) = - (x/y)"; |
|
641 by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); |
|
642 qed "hcomplex_minus_divide_eq"; |
|
643 Addsimps [hcomplex_minus_divide_eq]; |
|
644 |
|
645 Goal "(x / -(y::hcomplex)) = - (x/y)"; |
|
646 by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_minus_inverse]) 1); |
|
647 qed "hcomplex_divide_minus_eq"; |
|
648 Addsimps [hcomplex_divide_minus_eq]; |
|
649 |
|
650 Goal "(x+y)/(z::hcomplex) = x/z + y/z"; |
|
651 by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_add_mult_distrib]) 1); |
|
652 qed "hcomplex_add_divide_distrib"; |
|
653 |
|
654 (*---------------------------------------------------------------------------*) |
|
655 (* Embedding properties for hcomplex_of_hypreal map *) |
|
656 (*---------------------------------------------------------------------------*) |
|
657 |
|
658 Goalw [hcomplex_of_hypreal_def] |
|
659 "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = \ |
|
660 \ Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"; |
|
661 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
662 by Auto_tac; |
|
663 by (Ultra_tac 1); |
|
664 qed "hcomplex_of_hypreal"; |
|
665 |
|
666 Goal "inj hcomplex_of_hypreal"; |
|
667 by (rtac injI 1); |
|
668 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
669 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
670 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal])); |
|
671 qed "inj_hcomplex_of_hypreal"; |
|
672 |
|
673 Goal "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"; |
|
674 by (auto_tac (claset() addDs [inj_hcomplex_of_hypreal RS injD],simpset())); |
|
675 qed "hcomplex_of_hypreal_cancel_iff"; |
|
676 AddIffs [hcomplex_of_hypreal_cancel_iff]; |
|
677 |
|
678 Goal "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"; |
|
679 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
680 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
681 hcomplex_minus,hypreal_minus,complex_of_real_minus])); |
|
682 qed "hcomplex_of_hypreal_minus"; |
|
683 |
|
684 Goal "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"; |
|
685 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
686 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
687 hypreal_inverse,hcomplex_inverse,complex_of_real_inverse])); |
|
688 qed "hcomplex_of_hypreal_inverse"; |
|
689 |
|
690 Goal "hcomplex_of_hypreal x + hcomplex_of_hypreal y = \ |
|
691 \ hcomplex_of_hypreal (x + y)"; |
|
692 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
693 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
694 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
695 hypreal_add,hcomplex_add,complex_of_real_add])); |
|
696 qed "hcomplex_of_hypreal_add"; |
|
697 |
|
698 Goalw [hcomplex_diff_def] |
|
699 "hcomplex_of_hypreal x - hcomplex_of_hypreal y = \ |
|
700 \ hcomplex_of_hypreal (x - y)"; |
|
701 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal_minus |
|
702 RS sym,hcomplex_of_hypreal_add,hypreal_diff_def])); |
|
703 qed "hcomplex_of_hypreal_diff"; |
|
704 |
|
705 Goal "hcomplex_of_hypreal x * hcomplex_of_hypreal y = \ |
|
706 \ hcomplex_of_hypreal (x * y)"; |
|
707 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
708 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
709 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
710 hypreal_mult,hcomplex_mult,complex_of_real_mult])); |
|
711 qed "hcomplex_of_hypreal_mult"; |
|
712 |
|
713 Goalw [hcomplex_divide_def] |
|
714 "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"; |
|
715 by (case_tac "y=0" 1); |
|
716 by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO,HYPREAL_INVERSE_ZERO, |
|
717 HCOMPLEX_INVERSE_ZERO]) 1); |
|
718 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal_mult, |
|
719 hcomplex_of_hypreal_inverse RS sym])); |
|
720 by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
|
721 qed "hcomplex_of_hypreal_divide"; |
|
722 |
|
723 Goalw [hcomplex_one_def] |
|
724 "hcomplex_of_hypreal 1 = 1"; |
|
725 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,hypreal_one_num])); |
|
726 qed "hcomplex_of_hypreal_one"; |
|
727 |
|
728 Goalw [hcomplex_zero_def,hypreal_zero_def] |
|
729 "hcomplex_of_hypreal 0 = 0"; |
|
730 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal])); |
|
731 qed "hcomplex_of_hypreal_zero"; |
|
732 |
|
733 Addsimps [hcomplex_of_hypreal_one,hcomplex_of_hypreal_zero, |
|
734 rename_numerals hcomplex_of_hypreal_zero]; |
|
735 |
|
736 Goal "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"; |
|
737 by (induct_tac "n" 1); |
|
738 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal_mult RS sym])); |
|
739 qed "hcomplex_of_hypreal_pow"; |
|
740 |
|
741 Goal "hRe(hcomplex_of_hypreal z) = z"; |
|
742 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
743 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,hRe])); |
|
744 qed "hRe_hcomplex_of_hypreal"; |
|
745 Addsimps [hRe_hcomplex_of_hypreal]; |
|
746 |
|
747 Goal "hIm(hcomplex_of_hypreal z) = 0"; |
|
748 by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); |
|
749 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,hIm, |
|
750 hypreal_zero_num])); |
|
751 qed "hIm_hcomplex_of_hypreal"; |
|
752 Addsimps [hIm_hcomplex_of_hypreal]; |
|
753 |
|
754 Goal "hcomplex_of_hypreal epsilon ~= 0"; |
|
755 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
756 epsilon_def,hcomplex_zero_def])); |
|
757 qed "hcomplex_of_hypreal_epsilon_not_zero"; |
|
758 Addsimps [hcomplex_of_hypreal_epsilon_not_zero]; |
|
759 |
|
760 (*---------------------------------------------------------------------------*) |
|
761 (* Modulus (absolute value) of nonstandard complex number *) |
|
762 (*---------------------------------------------------------------------------*) |
|
763 |
|
764 Goalw [hcmod_def] |
|
765 "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) = \ |
|
766 \ Abs_hypreal(hyprel `` {%n. cmod (X n)})"; |
|
767 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
768 by (Auto_tac THEN Ultra_tac 1); |
|
769 qed "hcmod"; |
|
770 |
|
771 Goalw [hcomplex_zero_def,hypreal_zero_def] |
|
772 "hcmod(0) = 0"; |
|
773 by (auto_tac (claset(),simpset() addsimps [hcmod])); |
|
774 qed "hcmod_zero"; |
|
775 Addsimps [hcmod_zero,rename_numerals hcmod_zero]; |
|
776 |
|
777 Goalw [hcomplex_one_def] |
|
778 "hcmod(1) = 1"; |
|
779 by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_one_num])); |
|
780 qed "hcmod_one"; |
|
781 Addsimps [hcmod_one]; |
|
782 |
|
783 Goal "hcmod(hcomplex_of_hypreal x) = abs x"; |
|
784 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
785 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_of_hypreal, |
|
786 hypreal_hrabs])); |
|
787 qed "hcmod_hcomplex_of_hypreal"; |
|
788 Addsimps [hcmod_hcomplex_of_hypreal]; |
|
789 |
|
790 Goal "hcomplex_of_hypreal (abs x) = \ |
|
791 \ hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"; |
|
792 by (Simp_tac 1); |
|
793 qed "hcomplex_of_hypreal_abs"; |
|
794 |
|
795 (*---------------------------------------------------------------------------*) |
|
796 (* conjugation *) |
|
797 (*---------------------------------------------------------------------------*) |
|
798 |
|
799 Goalw [hcnj_def] |
|
800 "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) = \ |
|
801 \ Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"; |
|
802 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
803 by (Auto_tac THEN Ultra_tac 1); |
|
804 qed "hcnj"; |
|
805 |
|
806 Goal "inj hcnj"; |
|
807 by (rtac injI 1); |
|
808 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
809 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
810 by (auto_tac (claset(),simpset() addsimps [hcnj])); |
|
811 qed "inj_hcnj"; |
|
812 |
|
813 Goal "(hcnj x = hcnj y) = (x = y)"; |
|
814 by (auto_tac (claset() addDs [inj_hcnj RS injD],simpset())); |
|
815 qed "hcomplex_hcnj_cancel_iff"; |
|
816 Addsimps [hcomplex_hcnj_cancel_iff]; |
|
817 |
|
818 Goal "hcnj (hcnj z) = z"; |
|
819 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
820 by (auto_tac (claset(),simpset() addsimps [hcnj])); |
|
821 qed "hcomplex_hcnj_hcnj"; |
|
822 Addsimps [hcomplex_hcnj_hcnj]; |
|
823 |
|
824 Goal "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"; |
|
825 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
826 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_of_hypreal])); |
|
827 qed "hcomplex_hcnj_hcomplex_of_hypreal"; |
|
828 Addsimps [hcomplex_hcnj_hcomplex_of_hypreal]; |
|
829 |
|
830 Goal "hcmod (hcnj z) = hcmod z"; |
|
831 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
832 by (auto_tac (claset(),simpset() addsimps [hcnj,hcmod])); |
|
833 qed "hcomplex_hmod_hcnj"; |
|
834 Addsimps [hcomplex_hmod_hcnj]; |
|
835 |
|
836 Goal "hcnj (-z) = - hcnj z"; |
|
837 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
838 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_minus, |
|
839 complex_cnj_minus])); |
|
840 qed "hcomplex_hcnj_minus"; |
|
841 |
|
842 Goal "hcnj(inverse z) = inverse(hcnj z)"; |
|
843 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
844 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_inverse, |
|
845 complex_cnj_inverse])); |
|
846 qed "hcomplex_hcnj_inverse"; |
|
847 |
|
848 Goal "hcnj(w + z) = hcnj(w) + hcnj(z)"; |
|
849 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
850 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
851 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_add, |
|
852 complex_cnj_add])); |
|
853 qed "hcomplex_hcnj_add"; |
|
854 |
|
855 Goal "hcnj(w - z) = hcnj(w) - hcnj(z)"; |
|
856 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
857 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
858 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_diff, |
|
859 complex_cnj_diff])); |
|
860 qed "hcomplex_hcnj_diff"; |
|
861 |
|
862 Goal "hcnj(w * z) = hcnj(w) * hcnj(z)"; |
|
863 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
864 by (res_inst_tac [("z","w")] eq_Abs_hcomplex 1); |
|
865 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_mult, |
|
866 complex_cnj_mult])); |
|
867 qed "hcomplex_hcnj_mult"; |
|
868 |
|
869 Goalw [hcomplex_divide_def] "hcnj(w / z) = (hcnj w)/(hcnj z)"; |
|
870 by (simp_tac (simpset() addsimps [hcomplex_hcnj_mult,hcomplex_hcnj_inverse]) 1); |
|
871 qed "hcomplex_hcnj_divide"; |
|
872 |
|
873 Goalw [hcomplex_one_def] "hcnj 1 = 1"; |
|
874 by (simp_tac (simpset() addsimps [hcnj]) 1); |
|
875 qed "hcnj_one"; |
|
876 Addsimps [hcnj_one]; |
|
877 |
|
878 Goal "hcnj(z ^ n) = hcnj(z) ^ n"; |
|
879 by (induct_tac "n" 1); |
|
880 by (auto_tac (claset(),simpset() addsimps [hcomplex_hcnj_mult])); |
|
881 qed "hcomplex_hcnj_pow"; |
|
882 |
|
883 (* MOVE to NSComplexBin |
|
884 Goal "z + hcnj z = \ |
|
885 \ hcomplex_of_hypreal (2 * hRe(z))"; |
|
886 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
887 by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add, |
|
888 hypreal_mult,hcomplex_of_hypreal,complex_add_cnj])); |
|
889 qed "hcomplex_add_hcnj"; |
|
890 |
|
891 Goal "z - hcnj z = \ |
|
892 \ hcomplex_of_hypreal (hypreal_of_real 2 * hIm(z)) * iii"; |
|
893 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
894 by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff, |
|
895 hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal, |
|
896 complex_diff_cnj,iii_def,hcomplex_mult])); |
|
897 qed "hcomplex_diff_hcnj"; |
|
898 *) |
|
899 |
|
900 Goalw [hcomplex_zero_def] |
|
901 "hcnj 0 = 0"; |
|
902 by (auto_tac (claset(),simpset() addsimps [hcnj])); |
|
903 qed "hcomplex_hcnj_zero"; |
|
904 Addsimps [hcomplex_hcnj_zero]; |
|
905 |
|
906 Goal "(hcnj z = 0) = (z = 0)"; |
|
907 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
908 by (auto_tac (claset(),simpset() addsimps [hcomplex_zero_def, |
|
909 hcnj])); |
|
910 qed "hcomplex_hcnj_zero_iff"; |
|
911 AddIffs [hcomplex_hcnj_zero_iff]; |
|
912 |
|
913 Goal "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"; |
|
914 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
915 by (auto_tac (claset(),simpset() addsimps [hcnj,hcomplex_mult, |
|
916 hcomplex_of_hypreal,hRe,hIm,hypreal_add,hypreal_mult, |
|
917 complex_mult_cnj,two_eq_Suc_Suc])); |
|
918 qed "hcomplex_mult_hcnj"; |
|
919 |
|
920 |
|
921 (*---------------------------------------------------------------------------*) |
|
922 (* some algebra etc. *) |
|
923 (*---------------------------------------------------------------------------*) |
|
924 |
|
925 Goal "(x*y = (0::hcomplex)) = (x = 0 | y = 0)"; |
|
926 by Auto_tac; |
|
927 by (auto_tac (claset() addIs [ccontr] addDs |
|
928 [hcomplex_mult_not_zero],simpset())); |
|
929 qed "hcomplex_mult_zero_iff"; |
|
930 Addsimps [hcomplex_mult_zero_iff]; |
|
931 |
|
932 Goal "(x + y = x) = (y = (0::hcomplex))"; |
|
933 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
934 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
935 by (auto_tac (claset(),simpset() addsimps [hcomplex_add, |
|
936 hcomplex_zero_def])); |
|
937 qed "hcomplex_add_left_cancel_zero"; |
|
938 Addsimps [hcomplex_add_left_cancel_zero]; |
|
939 |
|
940 Goalw [hcomplex_diff_def] |
|
941 "((z1::hcomplex) - z2) * w = (z1 * w) - (z2 * w)"; |
|
942 by (simp_tac (simpset() addsimps [hcomplex_add_mult_distrib]) 1); |
|
943 qed "hcomplex_diff_mult_distrib"; |
|
944 |
|
945 Goalw [hcomplex_diff_def] |
|
946 "(w::hcomplex) * (z1 - z2) = (w * z1) - (w * z2)"; |
|
947 by (simp_tac (simpset() addsimps [hcomplex_add_mult_distrib2]) 1); |
|
948 qed "hcomplex_diff_mult_distrib2"; |
|
949 |
|
950 (*---------------------------------------------------------------------------*) |
|
951 (* More theorems about hcmod *) |
|
952 (*---------------------------------------------------------------------------*) |
|
953 |
|
954 Goal "(hcmod x = 0) = (x = 0)"; |
|
955 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
956 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_zero_def, |
|
957 hypreal_zero_num])); |
|
958 qed "hcomplex_hcmod_eq_zero_cancel"; |
|
959 Addsimps [hcomplex_hcmod_eq_zero_cancel]; |
|
960 |
|
961 (* not proved already? strange! *) |
|
962 Goalw [hypreal_le_def] |
|
963 "(hypreal_of_nat n <= hypreal_of_nat m) = (n <= m)"; |
|
964 by Auto_tac; |
|
965 qed "hypreal_of_nat_le_iff"; |
|
966 Addsimps [hypreal_of_nat_le_iff]; |
|
967 |
|
968 Goal "0 <= hypreal_of_nat n"; |
|
969 by (simp_tac (simpset() addsimps [hypreal_of_nat_zero RS sym] |
|
970 delsimps [hypreal_of_nat_zero]) 1); |
|
971 qed "hypreal_of_nat_ge_zero"; |
|
972 Addsimps [hypreal_of_nat_ge_zero]; |
|
973 |
|
974 Addsimps [hypreal_of_nat_ge_zero RS hrabs_eqI1]; |
|
975 |
|
976 Goal "0 <= hypreal_of_hypnat n"; |
|
977 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
978 by (asm_simp_tac (simpset() addsimps [hypreal_of_hypnat, |
|
979 hypreal_zero_num,hypreal_le]) 1); |
|
980 qed "hypreal_of_hypnat_ge_zero"; |
|
981 Addsimps [hypreal_of_hypnat_ge_zero]; |
|
982 |
|
983 Addsimps [hypreal_of_hypnat_ge_zero RS hrabs_eqI1]; |
|
984 |
|
985 Goal "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"; |
|
986 by Auto_tac; |
|
987 qed "hcmod_hcomplex_of_hypreal_of_nat"; |
|
988 Addsimps [hcmod_hcomplex_of_hypreal_of_nat]; |
|
989 |
|
990 Goal "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"; |
|
991 by Auto_tac; |
|
992 qed "hcmod_hcomplex_of_hypreal_of_hypnat"; |
|
993 Addsimps [hcmod_hcomplex_of_hypreal_of_hypnat]; |
|
994 |
|
995 Goal "hcmod (-x) = hcmod(x)"; |
|
996 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
997 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_minus])); |
|
998 qed "hcmod_minus"; |
|
999 Addsimps [hcmod_minus]; |
|
1000 |
|
1001 Goal "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"; |
|
1002 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1003 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_mult, |
|
1004 hcnj,hypreal_mult,complex_mod_mult_cnj,two_eq_Suc_Suc])); |
|
1005 qed "hcmod_mult_hcnj"; |
|
1006 |
|
1007 Goal "(0::hypreal) <= hcmod x"; |
|
1008 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1009 by (auto_tac (claset(),simpset() addsimps [hcmod, |
|
1010 hypreal_zero_num,hypreal_le])); |
|
1011 qed "hcmod_ge_zero"; |
|
1012 Addsimps [hcmod_ge_zero]; |
|
1013 |
|
1014 Goal "abs(hcmod x) = hcmod x"; |
|
1015 by (auto_tac (claset() addIs [hrabs_eqI1],simpset())); |
|
1016 qed "hrabs_hcmod_cancel"; |
|
1017 Addsimps [hrabs_hcmod_cancel]; |
|
1018 |
|
1019 Goal "hcmod(x*y) = hcmod(x) * hcmod(y)"; |
|
1020 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1021 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1022 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_mult, |
|
1023 hypreal_mult,complex_mod_mult])); |
|
1024 qed "hcmod_mult"; |
|
1025 |
|
1026 Goal "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"; |
|
1027 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1028 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1029 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_add, |
|
1030 hypreal_mult,hRe,hcnj,hcomplex_mult,two_eq_Suc_Suc, |
|
1031 realpow_two RS sym] delsimps [realpow_Suc])); |
|
1032 by (auto_tac (claset(),simpset() addsimps [two_eq_Suc_Suc RS sym, |
|
1033 complex_mod_add_squared_eq,hypreal_add RS sym,hypreal_mult RS sym, |
|
1034 symmetric hypreal_of_real_def])); |
|
1035 qed "hcmod_add_squared_eq"; |
|
1036 |
|
1037 Goal "hRe(x * hcnj y) <= hcmod(x * hcnj y)"; |
|
1038 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1039 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1040 by (auto_tac (claset(),simpset() addsimps [hcmod,hcnj, |
|
1041 hcomplex_mult,hRe,hypreal_le])); |
|
1042 qed "hcomplex_hRe_mult_hcnj_le_hcmod"; |
|
1043 Addsimps [hcomplex_hRe_mult_hcnj_le_hcmod]; |
|
1044 |
|
1045 Goal "hRe(x * hcnj y) <= hcmod(x * y)"; |
|
1046 by (cut_inst_tac [("x","x"),("y","y")] hcomplex_hRe_mult_hcnj_le_hcmod 1); |
|
1047 by (asm_full_simp_tac (simpset() addsimps [hcmod_mult]) 1); |
|
1048 qed "hcomplex_hRe_mult_hcnj_le_hcmod2"; |
|
1049 Addsimps [hcomplex_hRe_mult_hcnj_le_hcmod2]; |
|
1050 |
|
1051 Goal "hcmod (x + y) ^ 2 <= (hcmod(x) + hcmod(y)) ^ 2"; |
|
1052 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1053 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1054 by (auto_tac (claset(),simpset() addsimps [hcmod,hcnj, |
|
1055 hcomplex_add,hypreal_mult,hypreal_add,hypreal_le, |
|
1056 realpow_two RS sym,two_eq_Suc_Suc] delsimps [realpow_Suc])); |
|
1057 by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1); |
|
1058 qed "hcmod_triangle_squared"; |
|
1059 Addsimps [hcmod_triangle_squared]; |
|
1060 |
|
1061 Goal "hcmod (x + y) <= hcmod(x) + hcmod(y)"; |
|
1062 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1063 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1064 by (auto_tac (claset(),simpset() addsimps [hcmod, |
|
1065 hcomplex_add,hypreal_add,hypreal_le])); |
|
1066 qed "hcmod_triangle_ineq"; |
|
1067 Addsimps [hcmod_triangle_ineq]; |
|
1068 |
|
1069 Goal "hcmod(b + a) - hcmod b <= hcmod a"; |
|
1070 by (cut_inst_tac [("x1","b"),("y1","a"),("c","-hcmod b")] |
|
1071 (hcmod_triangle_ineq RS add_right_mono) 1); |
|
1072 by (asm_full_simp_tac (simpset() addsimps hypreal_add_ac) 1); |
|
1073 qed "hcmod_triangle_ineq2"; |
|
1074 Addsimps [hcmod_triangle_ineq2]; |
|
1075 |
|
1076 Goal "hcmod (x - y) = hcmod (y - x)"; |
|
1077 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1078 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1079 by (auto_tac (claset(),simpset() addsimps [hcmod, |
|
1080 hcomplex_diff,complex_mod_diff_commute])); |
|
1081 qed "hcmod_diff_commute"; |
|
1082 |
|
1083 Goal "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"; |
|
1084 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1085 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1086 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
1087 by (res_inst_tac [("z","s")] eq_Abs_hypreal 1); |
|
1088 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_add, |
|
1089 hypreal_add,hypreal_less])); |
|
1090 by (ultra_tac (claset() addIs [complex_mod_add_less],simpset()) 1); |
|
1091 qed "hcmod_add_less"; |
|
1092 |
|
1093 Goal "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"; |
|
1094 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1095 by (res_inst_tac [("z","y")] eq_Abs_hcomplex 1); |
|
1096 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
1097 by (res_inst_tac [("z","s")] eq_Abs_hypreal 1); |
|
1098 by (auto_tac (claset(),simpset() addsimps [hcmod,hypreal_mult, |
|
1099 hypreal_less,hcomplex_mult])); |
|
1100 by (ultra_tac (claset() addIs [complex_mod_mult_less],simpset()) 1); |
|
1101 qed "hcmod_mult_less"; |
|
1102 |
|
1103 goal NSComplex.thy "hcmod(a) - hcmod(b) <= hcmod(a + b)"; |
|
1104 by (res_inst_tac [("z","a")] eq_Abs_hcomplex 1); |
|
1105 by (res_inst_tac [("z","b")] eq_Abs_hcomplex 1); |
|
1106 by (auto_tac (claset(),simpset() addsimps [hcmod,hcomplex_add, |
|
1107 hypreal_diff,hypreal_le])); |
|
1108 qed "hcmod_diff_ineq"; |
|
1109 Addsimps [hcmod_diff_ineq]; |
|
1110 |
|
1111 |
|
1112 (*---------------------------------------------------------------------------*) |
|
1113 (* a few nonlinear theorems *) |
|
1114 (*---------------------------------------------------------------------------*) |
|
1115 |
|
1116 Goalw [hcpow_def] |
|
1117 "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow \ |
|
1118 \ Abs_hypnat(hypnatrel``{%n. Y n}) = \ |
|
1119 \ Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"; |
|
1120 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
1121 by (Auto_tac THEN Ultra_tac 1); |
|
1122 qed "hcpow"; |
|
1123 |
|
1124 Goal "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"; |
|
1125 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1126 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1127 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1128 hyperpow,hcpow,complex_of_real_pow])); |
|
1129 qed "hcomplex_of_hypreal_hyperpow"; |
|
1130 |
|
1131 Goal "hcmod(x ^ n) = hcmod(x) ^ n"; |
|
1132 by (induct_tac "n" 1); |
|
1133 by (auto_tac (claset(),simpset() addsimps [hcmod_mult])); |
|
1134 qed "hcmod_hcomplexpow"; |
|
1135 |
|
1136 Goal "hcmod(x hcpow n) = hcmod(x) pow n"; |
|
1137 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1138 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1139 by (auto_tac (claset(),simpset() addsimps [hcpow,hyperpow, |
|
1140 hcmod,complex_mod_complexpow])); |
|
1141 qed "hcmod_hcpow"; |
|
1142 |
|
1143 Goal "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"; |
|
1144 by (induct_tac "n" 1); |
|
1145 by Auto_tac; |
|
1146 qed "hcomplexpow_minus"; |
|
1147 |
|
1148 Goal "(-x::hcomplex) hcpow n = \ |
|
1149 \ (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"; |
|
1150 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1151 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1152 by (auto_tac (claset(),simpset() addsimps [hcpow,hyperpow,starPNat, |
|
1153 hcomplex_minus])); |
|
1154 by (ALLGOALS(ultra_tac (claset(),simpset() addsimps [complexpow_minus]))); |
|
1155 qed "hcpow_minus"; |
|
1156 |
|
1157 Goal "inverse(-x) = - inverse (x::hcomplex)"; |
|
1158 by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); |
|
1159 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse,hcomplex_minus, |
|
1160 complex_inverse_minus])); |
|
1161 qed "hccomplex_inverse_minus"; |
|
1162 |
|
1163 Goalw [hcomplex_divide_def] "x / (1::hcomplex) = x"; |
|
1164 by (Simp_tac 1); |
|
1165 qed "hcomplex_div_one"; |
|
1166 Addsimps [hcomplex_div_one]; |
|
1167 |
|
1168 Goal "hcmod(inverse x) = inverse(hcmod x)"; |
|
1169 by (hcomplex_div_undefined_case_tac "x = 0" 1); |
|
1170 by (res_inst_tac [("c1","hcmod x")] (hypreal_mult_left_cancel RS iffD1) 1); |
|
1171 by (auto_tac (claset(),simpset() addsimps [hcmod_mult RS sym])); |
|
1172 qed "hcmod_hcomplex_inverse"; |
|
1173 |
|
1174 Goalw [hcomplex_divide_def,hypreal_divide_def] |
|
1175 "hcmod(x/y) = hcmod(x)/(hcmod y)"; |
|
1176 by (auto_tac (claset(),simpset() addsimps [hcmod_mult, |
|
1177 hcmod_hcomplex_inverse])); |
|
1178 qed "hcmod_divide"; |
|
1179 |
|
1180 Goalw [hcomplex_divide_def] |
|
1181 "inverse(x/y) = y/(x::hcomplex)"; |
|
1182 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse_distrib, |
|
1183 hcomplex_mult_commute])); |
|
1184 qed "hcomplex_inverse_divide"; |
|
1185 Addsimps [hcomplex_inverse_divide]; |
|
1186 |
|
1187 Goal "((r::hcomplex) * s) ^ n = (r ^ n) * (s ^ n)"; |
|
1188 by (induct_tac "n" 1); |
|
1189 by (auto_tac (claset(),simpset() addsimps hcomplex_mult_ac)); |
|
1190 qed "hcomplexpow_mult"; |
|
1191 |
|
1192 Goal "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"; |
|
1193 by (res_inst_tac [("z","r")] eq_Abs_hcomplex 1); |
|
1194 by (res_inst_tac [("z","s")] eq_Abs_hcomplex 1); |
|
1195 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1196 by (auto_tac (claset(),simpset() addsimps [hcpow,hypreal_mult, |
|
1197 hcomplex_mult,complexpow_mult])); |
|
1198 qed "hcpow_mult"; |
|
1199 |
|
1200 Goal "(0::hcomplex) ^ (Suc n) = 0"; |
|
1201 by (Auto_tac); |
|
1202 qed "hcomplexpow_zero"; |
|
1203 Addsimps [hcomplexpow_zero]; |
|
1204 |
|
1205 Goalw [hcomplex_zero_def,hypnat_one_def] |
|
1206 "0 hcpow (n + 1) = 0"; |
|
1207 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1208 by (auto_tac (claset(),simpset() addsimps [hcpow,hypnat_add])); |
|
1209 qed "hcpow_zero"; |
|
1210 Addsimps [hcpow_zero]; |
|
1211 |
|
1212 Goalw [hSuc_def] |
|
1213 "0 hcpow (hSuc n) = 0"; |
|
1214 by (Simp_tac 1); |
|
1215 qed "hcpow_zero2"; |
|
1216 Addsimps [hcpow_zero2]; |
|
1217 |
|
1218 Goal "r ~= (0::hcomplex) --> r ^ n ~= 0"; |
|
1219 by (induct_tac "n" 1); |
|
1220 by (auto_tac (claset(),simpset() addsimps |
|
1221 [hcomplex_mult_not_zero])); |
|
1222 qed_spec_mp "hcomplexpow_not_zero"; |
|
1223 Addsimps [hcomplexpow_not_zero]; |
|
1224 AddIs [hcomplexpow_not_zero]; |
|
1225 |
|
1226 Goal "r ~= 0 ==> r hcpow n ~= (0::hcomplex)"; |
|
1227 by (res_inst_tac [("z","r")] eq_Abs_hcomplex 1); |
|
1228 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1229 by (auto_tac (claset(),simpset() addsimps [hcpow, |
|
1230 hcomplex_zero_def])); |
|
1231 by (ultra_tac (claset() addDs [complexpow_zero_zero],simpset()) 1); |
|
1232 qed "hcpow_not_zero"; |
|
1233 Addsimps [hcpow_not_zero]; |
|
1234 AddIs [hcpow_not_zero]; |
|
1235 |
|
1236 Goal "r ^ n = (0::hcomplex) ==> r = 0"; |
|
1237 by (blast_tac (claset() addIs [ccontr] |
|
1238 addDs [hcomplexpow_not_zero]) 1); |
|
1239 qed "hcomplexpow_zero_zero"; |
|
1240 |
|
1241 Goal "r hcpow n = (0::hcomplex) ==> r = 0"; |
|
1242 by (blast_tac (claset() addIs [ccontr] |
|
1243 addDs [hcpow_not_zero]) 1); |
|
1244 qed "hcpow_zero_zero"; |
|
1245 |
|
1246 Goalw [iii_def] "iii * iii = - 1"; |
|
1247 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult, |
|
1248 hcomplex_one_def,hcomplex_minus])); |
|
1249 qed "hcomplex_i_mult_eq"; |
|
1250 Addsimps [hcomplex_i_mult_eq]; |
|
1251 |
|
1252 Goal "iii ^ 2 = - 1"; |
|
1253 by (simp_tac (simpset() addsimps [two_eq_Suc_Suc]) 1); |
|
1254 qed "hcomplexpow_i_squared"; |
|
1255 Addsimps [hcomplexpow_i_squared]; |
|
1256 |
|
1257 Goalw [iii_def,hcomplex_zero_def] "iii ~= 0"; |
|
1258 by Auto_tac; |
|
1259 qed "hcomplex_i_not_zero"; |
|
1260 Addsimps [hcomplex_i_not_zero]; |
|
1261 |
|
1262 Goal "x * y ~= (0::hcomplex) ==> x ~= 0"; |
|
1263 by Auto_tac; |
|
1264 qed "hcomplex_mult_eq_zero_cancel1"; |
|
1265 |
|
1266 Goal "x * y ~= (0::hcomplex) ==> y ~= 0"; |
|
1267 by Auto_tac; |
|
1268 qed "hcomplex_mult_eq_zero_cancel2"; |
|
1269 |
|
1270 Goal "(x * y ~= (0::hcomplex)) = (x ~= 0 & y ~= 0)"; |
|
1271 by Auto_tac; |
|
1272 qed "hcomplex_mult_not_eq_zero_iff"; |
|
1273 AddIffs [hcomplex_mult_not_eq_zero_iff]; |
|
1274 |
|
1275 Goalw [hcomplex_divide_def,complex_divide_def] |
|
1276 "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) = \ |
|
1277 \ Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"; |
|
1278 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse,hcomplex_mult])); |
|
1279 qed "hcomplex_divide"; |
|
1280 |
|
1281 (*---------------------------------------------------------------------------*) |
|
1282 (* hsgn *) |
|
1283 (*---------------------------------------------------------------------------*) |
|
1284 |
|
1285 Goalw [hsgn_def] |
|
1286 "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) = \ |
|
1287 \ Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"; |
|
1288 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
1289 by (Auto_tac THEN Ultra_tac 1); |
|
1290 qed "hsgn"; |
|
1291 |
|
1292 Addsimps [rename_numerals sgn_zero]; |
|
1293 Goalw [hcomplex_zero_def] "hsgn 0 = 0"; |
|
1294 by (simp_tac (simpset() addsimps [hsgn]) 1); |
|
1295 qed "hsgn_zero"; |
|
1296 Addsimps[hsgn_zero]; |
|
1297 |
|
1298 Addsimps [rename_numerals sgn_one]; |
|
1299 |
|
1300 Goalw [hcomplex_one_def] "hsgn 1 = 1"; |
|
1301 by (simp_tac (simpset() addsimps [hsgn]) 1); |
|
1302 qed "hsgn_one"; |
|
1303 Addsimps[hsgn_one]; |
|
1304 |
|
1305 Goal "hsgn (-z) = - hsgn(z)"; |
|
1306 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1307 by (auto_tac (claset(),simpset() addsimps [hsgn,hcomplex_minus, |
|
1308 sgn_minus])); |
|
1309 qed "hsgn_minus"; |
|
1310 |
|
1311 Goal "hsgn z = z / hcomplex_of_hypreal (hcmod z)"; |
|
1312 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1313 by (auto_tac (claset(),simpset() addsimps [hsgn,hcomplex_divide, |
|
1314 hcomplex_of_hypreal,hcmod,sgn_eq])); |
|
1315 qed "hsgn_eq"; |
|
1316 |
|
1317 Goal "(EX (x::hypreal) y. P x y) = \ |
|
1318 \ (EX f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"; |
|
1319 by Auto_tac; |
|
1320 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1321 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1322 by Auto_tac; |
|
1323 qed "lemma_hypreal_P_EX2"; |
|
1324 |
|
1325 Goal "ALL (n::nat). EX x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"; |
|
1326 by (blast_tac (claset() addIs [complex_split]) 1); |
|
1327 qed "complex_split2"; |
|
1328 |
|
1329 (* Interesting proof! *) |
|
1330 Goal "EX x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"; |
|
1331 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1332 by (auto_tac (claset(),simpset() addsimps [lemma_hypreal_P_EX2, |
|
1333 hcomplex_of_hypreal,iii_def,hcomplex_add,hcomplex_mult])); |
|
1334 by (cut_inst_tac [("z","x")] complex_split2 1); |
|
1335 by (REPEAT(dtac choice 1 THEN Step_tac 1)); |
|
1336 by (res_inst_tac [("x","f")] exI 1); |
|
1337 by (res_inst_tac [("x","fa")] exI 1); |
|
1338 by Auto_tac; |
|
1339 qed "hcomplex_split"; |
|
1340 |
|
1341 Goal "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"; |
|
1342 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1343 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1344 by (auto_tac (claset(),simpset() addsimps [hRe,iii_def,hcomplex_add, |
|
1345 hcomplex_mult,hcomplex_of_hypreal])); |
|
1346 qed "hRe_hcomplex_i"; |
|
1347 Addsimps [hRe_hcomplex_i]; |
|
1348 |
|
1349 Goal "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"; |
|
1350 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1351 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1352 by (auto_tac (claset(),simpset() addsimps [hIm,iii_def,hcomplex_add, |
|
1353 hcomplex_mult,hcomplex_of_hypreal])); |
|
1354 qed "hIm_hcomplex_i"; |
|
1355 Addsimps [hIm_hcomplex_i]; |
|
1356 |
|
1357 Goal "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = \ |
|
1358 \ ( *f* sqrt) (x ^ 2 + y ^ 2)"; |
|
1359 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1360 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1361 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1362 iii_def,hcomplex_add,hcomplex_mult,starfun,hypreal_mult, |
|
1363 hypreal_add,hcmod,cmod_i,two_eq_Suc_Suc])); |
|
1364 qed "hcmod_i"; |
|
1365 |
|
1366 Goalw [iii_def] |
|
1367 "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = \ |
|
1368 \ hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb \ |
|
1369 \ ==> xa = xb"; |
|
1370 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); |
|
1371 by (res_inst_tac [("z","ya")] eq_Abs_hypreal 1); |
|
1372 by (res_inst_tac [("z","xb")] eq_Abs_hypreal 1); |
|
1373 by (res_inst_tac [("z","yb")] eq_Abs_hypreal 1); |
|
1374 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult,hcomplex_add, |
|
1375 hcomplex_of_hypreal])); |
|
1376 by (Ultra_tac 1); |
|
1377 qed "hcomplex_eq_hRe_eq"; |
|
1378 |
|
1379 Goalw [iii_def] |
|
1380 "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = \ |
|
1381 \ hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb \ |
|
1382 \ ==> ya = yb"; |
|
1383 by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); |
|
1384 by (res_inst_tac [("z","ya")] eq_Abs_hypreal 1); |
|
1385 by (res_inst_tac [("z","xb")] eq_Abs_hypreal 1); |
|
1386 by (res_inst_tac [("z","yb")] eq_Abs_hypreal 1); |
|
1387 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult,hcomplex_add, |
|
1388 hcomplex_of_hypreal])); |
|
1389 by (Ultra_tac 1); |
|
1390 qed "hcomplex_eq_hIm_eq"; |
|
1391 |
|
1392 Goal "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = \ |
|
1393 \ hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = \ |
|
1394 \ ((xa = xb) & (ya = yb))"; |
|
1395 by (auto_tac (claset() addIs [hcomplex_eq_hIm_eq,hcomplex_eq_hRe_eq],simpset())); |
|
1396 qed "hcomplex_eq_cancel_iff"; |
|
1397 Addsimps [hcomplex_eq_cancel_iff]; |
|
1398 |
|
1399 Goal "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = \ |
|
1400 \ hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))"; |
|
1401 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_commute])); |
|
1402 qed "hcomplex_eq_cancel_iffA"; |
|
1403 AddIffs [hcomplex_eq_cancel_iffA]; |
|
1404 |
|
1405 Goal "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = \ |
|
1406 \ hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"; |
|
1407 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_commute])); |
|
1408 qed "hcomplex_eq_cancel_iffB"; |
|
1409 AddIffs [hcomplex_eq_cancel_iffB]; |
|
1410 |
|
1411 Goal "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = \ |
|
1412 \ hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"; |
|
1413 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_commute])); |
|
1414 qed "hcomplex_eq_cancel_iffC"; |
|
1415 AddIffs [hcomplex_eq_cancel_iffC]; |
|
1416 |
|
1417 Goal"(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = \ |
|
1418 \ hcomplex_of_hypreal xa) = (x = xa & y = 0)"; |
|
1419 by (cut_inst_tac [("xa","x"),("ya","y"),("xb","xa"),("yb","0")] |
|
1420 hcomplex_eq_cancel_iff 1); |
|
1421 by (asm_full_simp_tac (simpset() delsimps [hcomplex_eq_cancel_iff]) 1); |
|
1422 qed "hcomplex_eq_cancel_iff2"; |
|
1423 Addsimps [hcomplex_eq_cancel_iff2]; |
|
1424 |
|
1425 Goal"(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = \ |
|
1426 \ hcomplex_of_hypreal xa) = (x = xa & y = 0)"; |
|
1427 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_commute])); |
|
1428 qed "hcomplex_eq_cancel_iff2a"; |
|
1429 Addsimps [hcomplex_eq_cancel_iff2a]; |
|
1430 |
|
1431 Goal "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = \ |
|
1432 \ iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"; |
|
1433 by (cut_inst_tac [("xa","x"),("ya","y"),("xb","0"),("yb","ya")] |
|
1434 hcomplex_eq_cancel_iff 1); |
|
1435 by (asm_full_simp_tac (simpset() delsimps [hcomplex_eq_cancel_iff]) 1); |
|
1436 qed "hcomplex_eq_cancel_iff3"; |
|
1437 Addsimps [hcomplex_eq_cancel_iff3]; |
|
1438 |
|
1439 Goal "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = \ |
|
1440 \ iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"; |
|
1441 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_commute])); |
|
1442 qed "hcomplex_eq_cancel_iff3a"; |
|
1443 Addsimps [hcomplex_eq_cancel_iff3a]; |
|
1444 |
|
1445 Goalw [iii_def] |
|
1446 "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 \ |
|
1447 \ ==> x = 0"; |
|
1448 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1449 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1450 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1451 hcomplex_add,hcomplex_mult,hcomplex_zero_def,hypreal_zero_num])); |
|
1452 by (ultra_tac (claset(),simpset() addsimps [complex_split_Re_zero]) 1); |
|
1453 qed "hcomplex_split_hRe_zero"; |
|
1454 |
|
1455 Goalw [iii_def] |
|
1456 "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 \ |
|
1457 \ ==> y = 0"; |
|
1458 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1459 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1460 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1461 hcomplex_add,hcomplex_mult,hcomplex_zero_def,hypreal_zero_num])); |
|
1462 by (ultra_tac (claset(),simpset() addsimps [complex_split_Im_zero]) 1); |
|
1463 qed "hcomplex_split_hIm_zero"; |
|
1464 |
|
1465 Goal "hRe(hsgn z) = hRe(z)/hcmod z"; |
|
1466 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1467 by (auto_tac (claset(),simpset() addsimps [hsgn,hcmod,hRe,hypreal_divide])); |
|
1468 qed "hRe_hsgn"; |
|
1469 Addsimps [hRe_hsgn]; |
|
1470 |
|
1471 Goal "hIm(hsgn z) = hIm(z)/hcmod z"; |
|
1472 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1473 by (auto_tac (claset(),simpset() addsimps [hsgn,hcmod,hIm,hypreal_divide])); |
|
1474 qed "hIm_hsgn"; |
|
1475 Addsimps [hIm_hsgn]; |
|
1476 |
|
1477 Goal "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"; |
|
1478 by (auto_tac (claset() addIs [real_sum_squares_cancel],simpset())); |
|
1479 qed "real_two_squares_add_zero_iff"; |
|
1480 Addsimps [real_two_squares_add_zero_iff]; |
|
1481 |
|
1482 Goal "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = \ |
|
1483 \ hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - \ |
|
1484 \ iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"; |
|
1485 by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); |
|
1486 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1487 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1488 hcomplex_mult,hcomplex_add,iii_def,starfun,hypreal_mult, |
|
1489 hypreal_add,hcomplex_inverse,hypreal_divide,hcomplex_diff, |
|
1490 complex_inverse_complex_split,two_eq_Suc_Suc])); |
|
1491 qed "hcomplex_inverse_complex_split"; |
|
1492 |
|
1493 Goalw [iii_def] |
|
1494 "hRe (iii * hcomplex_of_hypreal y) = 0"; |
|
1495 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1496 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1497 hcomplex_mult,hRe,hypreal_zero_num])); |
|
1498 qed "hRe_mult_i_eq"; |
|
1499 Addsimps [hRe_mult_i_eq]; |
|
1500 |
|
1501 Goalw [iii_def] |
|
1502 "hIm (iii * hcomplex_of_hypreal y) = y"; |
|
1503 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1504 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1505 hcomplex_mult,hIm,hypreal_zero_num])); |
|
1506 qed "hIm_mult_i_eq"; |
|
1507 Addsimps [hIm_mult_i_eq]; |
|
1508 |
|
1509 Goal "hcmod (iii * hcomplex_of_hypreal y) = abs y"; |
|
1510 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1511 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1512 hcmod,hypreal_hrabs,iii_def,hcomplex_mult])); |
|
1513 qed "hcmod_mult_i"; |
|
1514 Addsimps [hcmod_mult_i]; |
|
1515 |
|
1516 Goal "hcmod (hcomplex_of_hypreal y * iii) = abs y"; |
|
1517 by (auto_tac (claset(),simpset() addsimps [hcomplex_mult_commute])); |
|
1518 qed "hcmod_mult_i2"; |
|
1519 Addsimps [hcmod_mult_i2]; |
|
1520 |
|
1521 (*---------------------------------------------------------------------------*) |
|
1522 (* harg *) |
|
1523 (*---------------------------------------------------------------------------*) |
|
1524 |
|
1525 Goalw [harg_def] |
|
1526 "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) = \ |
|
1527 \ Abs_hypreal(hyprel `` {%n. arg (X n)})"; |
|
1528 by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); |
|
1529 by (Auto_tac THEN Ultra_tac 1); |
|
1530 qed "harg"; |
|
1531 |
|
1532 Goal "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"; |
|
1533 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1534 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1535 iii_def,hcomplex_mult,hypreal_zero_num,hypreal_less,starfun, |
|
1536 harg])); |
|
1537 by (Ultra_tac 1); |
|
1538 qed "cos_harg_i_mult_zero"; |
|
1539 Addsimps [cos_harg_i_mult_zero]; |
|
1540 |
|
1541 Goal "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"; |
|
1542 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1543 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1544 iii_def,hcomplex_mult,hypreal_zero_num,hypreal_less,starfun, |
|
1545 harg])); |
|
1546 by (Ultra_tac 1); |
|
1547 qed "cos_harg_i_mult_zero2"; |
|
1548 Addsimps [cos_harg_i_mult_zero2]; |
|
1549 |
|
1550 Goal "(hcomplex_of_hypreal y ~= 0) = (y ~= 0)"; |
|
1551 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1552 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1553 hypreal_zero_num,hcomplex_zero_def])); |
|
1554 qed "hcomplex_of_hypreal_not_zero_iff"; |
|
1555 Addsimps [hcomplex_of_hypreal_not_zero_iff]; |
|
1556 |
|
1557 Goal "(hcomplex_of_hypreal y = 0) = (y = 0)"; |
|
1558 by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); |
|
1559 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal, |
|
1560 hypreal_zero_num,hcomplex_zero_def])); |
|
1561 qed "hcomplex_of_hypreal_zero_iff"; |
|
1562 Addsimps [hcomplex_of_hypreal_zero_iff]; |
|
1563 |
|
1564 Goal "y ~= 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"; |
|
1565 by (cut_inst_tac [("x","y"),("y","0")] hypreal_linear 1); |
|
1566 by Auto_tac; |
|
1567 qed "cos_harg_i_mult_zero3"; |
|
1568 Addsimps [cos_harg_i_mult_zero3]; |
|
1569 |
|
1570 (*---------------------------------------------------------------------------*) |
|
1571 (* Polar form for nonstandard complex numbers *) |
|
1572 (*---------------------------------------------------------------------------*) |
|
1573 |
|
1574 Goal "ALL n. EX r a. (z n) = complex_of_real r * \ |
|
1575 \ (complex_of_real(cos a) + ii * complex_of_real(sin a))"; |
|
1576 by (blast_tac (claset() addIs [complex_split_polar]) 1); |
|
1577 qed "complex_split_polar2"; |
|
1578 |
|
1579 Goal |
|
1580 "EX r a. z = hcomplex_of_hypreal r * \ |
|
1581 \ (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"; |
|
1582 by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); |
|
1583 by (auto_tac (claset(),simpset() addsimps [lemma_hypreal_P_EX2, |
|
1584 hcomplex_of_hypreal,iii_def,starfun,hcomplex_add,hcomplex_mult])); |
|
1585 by (cut_inst_tac [("z","x")] complex_split_polar2 1); |
|
1586 by (REPEAT(dtac choice 1 THEN Step_tac 1)); |
|
1587 by (res_inst_tac [("x","f")] exI 1); |
|
1588 by (res_inst_tac [("x","fa")] exI 1); |
|
1589 by Auto_tac; |
|
1590 qed "hcomplex_split_polar"; |
|
1591 |
|
1592 Goalw [hcis_def] |
|
1593 "hcis (Abs_hypreal(hyprel `` {%n. X n})) = \ |
|
1594 \ Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"; |
|
1595 by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); |
|
1596 by Auto_tac; |
|
1597 by (Ultra_tac 1); |
|
1598 qed "hcis"; |
|
1599 |
|
1600 Goal |
|
1601 "hcis a = \ |
|
1602 \ (hcomplex_of_hypreal(( *f* cos) a) + \ |
|
1603 \ iii * hcomplex_of_hypreal(( *f* sin) a))"; |
|
1604 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1605 by (auto_tac (claset(),simpset() addsimps [starfun, hcis, |
|
1606 hcomplex_of_hypreal,iii_def,hcomplex_mult,hcomplex_add, |
|
1607 cis_def])); |
|
1608 qed "hcis_eq"; |
|
1609 |
|
1610 Goalw [hrcis_def] |
|
1611 "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) = \ |
|
1612 \ Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"; |
|
1613 by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal,hcomplex_mult, |
|
1614 hcis,rcis_def])); |
|
1615 qed "hrcis"; |
|
1616 |
|
1617 Goal "EX r a. z = hrcis r a"; |
|
1618 by (simp_tac (simpset() addsimps [hrcis_def,hcis_eq]) 1); |
|
1619 by (rtac hcomplex_split_polar 1); |
|
1620 qed "hrcis_Ex"; |
|
1621 |
|
1622 Goal "hRe(hcomplex_of_hypreal r * \ |
|
1623 \ (hcomplex_of_hypreal(( *f* cos) a) + \ |
|
1624 \ iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"; |
|
1625 by (auto_tac (claset(),simpset() addsimps [hcomplex_add_mult_distrib2, |
|
1626 hcomplex_of_hypreal_mult] @ hcomplex_mult_ac)); |
|
1627 qed "hRe_hcomplex_polar"; |
|
1628 Addsimps [hRe_hcomplex_polar]; |
|
1629 |
|
1630 Goalw [hrcis_def] "hRe(hrcis r a) = r * ( *f* cos) a"; |
|
1631 by (auto_tac (claset(),simpset() addsimps [hcis_eq])); |
|
1632 qed "hRe_hrcis"; |
|
1633 Addsimps [hRe_hrcis]; |
|
1634 |
|
1635 Goal "hIm(hcomplex_of_hypreal r * \ |
|
1636 \ (hcomplex_of_hypreal(( *f* cos) a) + \ |
|
1637 \ iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"; |
|
1638 by (auto_tac (claset(),simpset() addsimps [hcomplex_add_mult_distrib2, |
|
1639 hcomplex_of_hypreal_mult] @ hcomplex_mult_ac)); |
|
1640 qed "hIm_hcomplex_polar"; |
|
1641 Addsimps [hIm_hcomplex_polar]; |
|
1642 |
|
1643 Goalw [hrcis_def] "hIm(hrcis r a) = r * ( *f* sin) a"; |
|
1644 by (auto_tac (claset(),simpset() addsimps [hcis_eq])); |
|
1645 qed "hIm_hrcis"; |
|
1646 Addsimps [hIm_hrcis]; |
|
1647 |
|
1648 Goal "hcmod (hcomplex_of_hypreal r * \ |
|
1649 \ (hcomplex_of_hypreal(( *f* cos) a) + \ |
|
1650 \ iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"; |
|
1651 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
1652 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1653 by (auto_tac (claset(),simpset() addsimps [iii_def,starfun, |
|
1654 hcomplex_of_hypreal,hcomplex_mult,hcmod,hcomplex_add, |
|
1655 hypreal_hrabs])); |
|
1656 qed "hcmod_complex_polar"; |
|
1657 Addsimps [hcmod_complex_polar]; |
|
1658 |
|
1659 Goalw [hrcis_def] "hcmod(hrcis r a) = abs r"; |
|
1660 by (auto_tac (claset(),simpset() addsimps [hcis_eq])); |
|
1661 qed "hcmod_hrcis"; |
|
1662 Addsimps [hcmod_hrcis]; |
|
1663 |
|
1664 (*---------------------------------------------------------------------------*) |
|
1665 (* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
|
1666 (*---------------------------------------------------------------------------*) |
|
1667 |
|
1668 Goalw [hrcis_def] "hcis a = hrcis 1 a"; |
|
1669 by (Simp_tac 1); |
|
1670 qed "hcis_hrcis_eq"; |
|
1671 Addsimps [hcis_hrcis_eq RS sym]; |
|
1672 |
|
1673 Goalw [hrcis_def] |
|
1674 "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"; |
|
1675 by (res_inst_tac [("z","r1")] eq_Abs_hypreal 1); |
|
1676 by (res_inst_tac [("z","r2")] eq_Abs_hypreal 1); |
|
1677 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1678 by (res_inst_tac [("z","b")] eq_Abs_hypreal 1); |
|
1679 by (auto_tac (claset(),simpset() addsimps [hrcis,hcis, |
|
1680 hypreal_add,hypreal_mult,hcomplex_of_hypreal, |
|
1681 hcomplex_mult,cis_mult RS sym,complex_of_real_mult |
|
1682 RS sym] addsimps complex_mult_ac)); |
|
1683 qed "hrcis_mult"; |
|
1684 |
|
1685 Goal "hcis a * hcis b = hcis (a + b)"; |
|
1686 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1687 by (res_inst_tac [("z","b")] eq_Abs_hypreal 1); |
|
1688 by (auto_tac (claset(),simpset() addsimps [hcis,hcomplex_mult, |
|
1689 hypreal_add,cis_mult])); |
|
1690 qed "hcis_mult"; |
|
1691 |
|
1692 Goalw [hcomplex_one_def] |
|
1693 "hcis 0 = 1"; |
|
1694 by (auto_tac (claset(),simpset() addsimps [hcis,hypreal_zero_num])); |
|
1695 qed "hcis_zero"; |
|
1696 Addsimps [hcis_zero]; |
|
1697 |
|
1698 Goalw [hcomplex_zero_def] |
|
1699 "hrcis 0 a = 0"; |
|
1700 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1701 by (auto_tac (claset(),simpset() addsimps [hrcis,hypreal_zero_num])); |
|
1702 qed "hrcis_zero_mod"; |
|
1703 Addsimps [hrcis_zero_mod]; |
|
1704 |
|
1705 Goal "hrcis r 0 = hcomplex_of_hypreal r"; |
|
1706 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
1707 by (auto_tac (claset(),simpset() addsimps [hrcis, |
|
1708 hypreal_zero_num,hcomplex_of_hypreal])); |
|
1709 qed "hrcis_zero_arg"; |
|
1710 Addsimps [hrcis_zero_arg]; |
|
1711 |
|
1712 Goal "iii * (iii * x) = - x"; |
|
1713 by (simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym]) 1); |
|
1714 qed "hcomplex_i_mult_minus"; |
|
1715 Addsimps [hcomplex_i_mult_minus]; |
|
1716 |
|
1717 Goal "iii * iii * x = - x"; |
|
1718 by (Simp_tac 1); |
|
1719 qed "hcomplex_i_mult_minus2"; |
|
1720 Addsimps [hcomplex_i_mult_minus2]; |
|
1721 |
|
1722 (* Move to one of the hyperreal theories *) |
|
1723 Goal "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"; |
|
1724 by (induct_tac "m" 1); |
|
1725 by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def, |
|
1726 hypreal_of_nat_Suc,hypreal_zero_num, |
|
1727 hypreal_one_num,hypreal_add,real_of_nat_Suc])); |
|
1728 qed "hypreal_of_nat"; |
|
1729 |
|
1730 Goal |
|
1731 "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"; |
|
1732 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1733 by (auto_tac (claset(),simpset() addsimps [hypreal_of_nat,hcis, |
|
1734 hypreal_mult,hcomplex_mult,cis_real_of_nat_Suc_mult])); |
|
1735 qed "hcis_hypreal_of_nat_Suc_mult"; |
|
1736 |
|
1737 Goal "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"; |
|
1738 by (induct_tac "n" 1); |
|
1739 by (auto_tac (claset(),simpset() addsimps [hcis_hypreal_of_nat_Suc_mult])); |
|
1740 qed "NSDeMoivre"; |
|
1741 |
|
1742 Goal "hcis (hypreal_of_hypnat (n + 1) * a) = \ |
|
1743 \ hcis a * hcis (hypreal_of_hypnat n * a)"; |
|
1744 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1745 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1746 by (auto_tac (claset(),simpset() addsimps [hcis,hypreal_of_hypnat, |
|
1747 hypnat_add,hypnat_one_def,hypreal_mult,hcomplex_mult, |
|
1748 cis_real_of_nat_Suc_mult])); |
|
1749 qed "hcis_hypreal_of_hypnat_Suc_mult"; |
|
1750 |
|
1751 Goal "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"; |
|
1752 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1753 by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); |
|
1754 by (auto_tac (claset(),simpset() addsimps [hcis,hypreal_of_hypnat, |
|
1755 hypreal_mult,hcpow,DeMoivre])); |
|
1756 qed "NSDeMoivre_ext"; |
|
1757 |
|
1758 Goalw [hrcis_def] |
|
1759 "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"; |
|
1760 by (auto_tac (claset(),simpset() addsimps [hcomplexpow_mult, |
|
1761 NSDeMoivre,hcomplex_of_hypreal_pow])); |
|
1762 qed "DeMoivre2"; |
|
1763 |
|
1764 Goalw [hrcis_def] |
|
1765 "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"; |
|
1766 by (auto_tac (claset(),simpset() addsimps [hcpow_mult, |
|
1767 NSDeMoivre_ext,hcomplex_of_hypreal_hyperpow])); |
|
1768 qed "DeMoivre2_ext"; |
|
1769 |
|
1770 Goal "inverse(hcis a) = hcis (-a)"; |
|
1771 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1772 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse,hcis,hypreal_minus])); |
|
1773 qed "hcis_inverse"; |
|
1774 Addsimps [hcis_inverse]; |
|
1775 |
|
1776 Goal "inverse(hrcis r a) = hrcis (inverse r) (-a)"; |
|
1777 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1778 by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); |
|
1779 by (auto_tac (claset(),simpset() addsimps [hcomplex_inverse,hrcis,hypreal_minus, |
|
1780 hypreal_inverse,rcis_inverse])); |
|
1781 by (Ultra_tac 1); |
|
1782 by (rewtac real_divide_def); |
|
1783 by (auto_tac (claset(),simpset() addsimps [INVERSE_ZERO])); |
|
1784 qed "hrcis_inverse"; |
|
1785 |
|
1786 Goal "hRe(hcis a) = ( *f* cos) a"; |
|
1787 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1788 by (auto_tac (claset(),simpset() addsimps [hcis,starfun,hRe])); |
|
1789 qed "hRe_hcis"; |
|
1790 Addsimps [hRe_hcis]; |
|
1791 |
|
1792 Goal "hIm(hcis a) = ( *f* sin) a"; |
|
1793 by (res_inst_tac [("z","a")] eq_Abs_hypreal 1); |
|
1794 by (auto_tac (claset(),simpset() addsimps [hcis,starfun,hIm])); |
|
1795 qed "hIm_hcis"; |
|
1796 Addsimps [hIm_hcis]; |
|
1797 |
|
1798 Goal "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"; |
|
1799 by (auto_tac (claset(),simpset() addsimps [NSDeMoivre])); |
|
1800 qed "cos_n_hRe_hcis_pow_n"; |
|
1801 |
|
1802 Goal "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"; |
|
1803 by (auto_tac (claset(),simpset() addsimps [NSDeMoivre])); |
|
1804 qed "sin_n_hIm_hcis_pow_n"; |
|
1805 |
|
1806 Goal "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"; |
|
1807 by (auto_tac (claset(),simpset() addsimps [NSDeMoivre_ext])); |
|
1808 qed "cos_n_hRe_hcis_hcpow_n"; |
|
1809 |
|
1810 Goal "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"; |
|
1811 by (auto_tac (claset(),simpset() addsimps [NSDeMoivre_ext])); |
|
1812 qed "sin_n_hIm_hcis_hcpow_n"; |
|
1813 |
|
1814 Goalw [hexpi_def] "hexpi(a + b) = hexpi(a) * hexpi(b)"; |
|
1815 by (res_inst_tac [("z","a")] eq_Abs_hcomplex 1); |
|
1816 by (res_inst_tac [("z","b")] eq_Abs_hcomplex 1); |
|
1817 by (auto_tac (claset(),simpset() addsimps [hcis,hRe,hIm, |
|
1818 hcomplex_add,hcomplex_mult,hypreal_mult,starfun, |
|
1819 hcomplex_of_hypreal,cis_mult RS sym,complex_Im_add, |
|
1820 complex_Re_add,exp_add,complex_of_real_mult])); |
|
1821 qed "hexpi_add"; |
|
1822 |
|
1823 (*----------------------------------------------------------------------------------*) |
|
1824 (* hcomplex_of_complex preserves field and order properties *) |
|
1825 (*----------------------------------------------------------------------------------*) |
|
1826 |
|
1827 Goalw [hcomplex_of_complex_def] |
|
1828 "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"; |
|
1829 by (simp_tac (simpset() addsimps [hcomplex_add]) 1); |
|
1830 qed "hcomplex_of_complex_add"; |
|
1831 Addsimps [hcomplex_of_complex_add]; |
|
1832 |
|
1833 Goalw [hcomplex_of_complex_def] |
|
1834 "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"; |
|
1835 by (simp_tac (simpset() addsimps [hcomplex_mult]) 1); |
|
1836 qed "hcomplex_of_complex_mult"; |
|
1837 Addsimps [hcomplex_of_complex_mult]; |
|
1838 |
|
1839 Goalw [hcomplex_of_complex_def] |
|
1840 "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"; |
|
1841 by Auto_tac; |
|
1842 qed "hcomplex_of_complex_eq_iff"; |
|
1843 Addsimps [hcomplex_of_complex_eq_iff]; |
|
1844 |
|
1845 Goalw [hcomplex_of_complex_def] "hcomplex_of_complex (-r) = - hcomplex_of_complex r"; |
|
1846 by (auto_tac (claset(),simpset() addsimps [hcomplex_minus])); |
|
1847 qed "hcomplex_of_complex_minus"; |
|
1848 Addsimps [hcomplex_of_complex_minus]; |
|
1849 |
|
1850 Goalw [hcomplex_of_complex_def,hcomplex_one_def] |
|
1851 "hcomplex_of_complex 1 = 1"; |
|
1852 by Auto_tac; |
|
1853 qed "hcomplex_of_complex_one"; |
|
1854 |
|
1855 Goalw [hcomplex_of_complex_def,hcomplex_zero_def] |
|
1856 "hcomplex_of_complex 0 = 0"; |
|
1857 by (Simp_tac 1); |
|
1858 qed "hcomplex_of_complex_zero"; |
|
1859 |
|
1860 Goal "(hcomplex_of_complex r = 0) = (r = 0)"; |
|
1861 by (auto_tac (claset() addIs [FreeUltrafilterNat_P], |
|
1862 simpset() addsimps [hcomplex_of_complex_def, |
|
1863 hcomplex_zero_def])); |
|
1864 qed "hcomplex_of_complex_zero_iff"; |
|
1865 |
|
1866 Goal "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"; |
|
1867 by (case_tac "r=0" 1); |
|
1868 by (asm_simp_tac (simpset() addsimps [COMPLEX_INVERSE_ZERO, |
|
1869 HCOMPLEX_INVERSE_ZERO, hcomplex_of_complex_zero, |
|
1870 COMPLEX_DIVIDE_ZERO]) 1); |
|
1871 by (res_inst_tac [("c1","hcomplex_of_complex r")] |
|
1872 (hcomplex_mult_left_cancel RS iffD1) 1); |
|
1873 by (stac (hcomplex_of_complex_mult RS sym) 2); |
|
1874 by (auto_tac (claset(), |
|
1875 simpset() addsimps [hcomplex_of_complex_one, hcomplex_of_complex_zero_iff])); |
|
1876 qed "hcomplex_of_complex_inverse"; |
|
1877 Addsimps [hcomplex_of_complex_inverse]; |
|
1878 |
|
1879 Goal "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"; |
|
1880 by (simp_tac (simpset() addsimps [hcomplex_divide_def, complex_divide_def]) 1); |
|
1881 qed "hcomplex_of_complex_divide"; |
|
1882 Addsimps [hcomplex_of_complex_divide]; |
|
1883 |
|
1884 Goalw [hcomplex_of_complex_def,hypreal_of_real_def] |
|
1885 "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"; |
|
1886 by (auto_tac (claset(),simpset() addsimps [hRe])); |
|
1887 qed "hRe_hcomplex_of_complex"; |
|
1888 |
|
1889 Goalw [hcomplex_of_complex_def,hypreal_of_real_def] |
|
1890 "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"; |
|
1891 by (auto_tac (claset(),simpset() addsimps [hIm])); |
|
1892 qed "hIm_hcomplex_of_complex"; |
|
1893 |
|
1894 Goalw [hypreal_of_real_def,hcomplex_of_complex_def] |
|
1895 "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"; |
|
1896 by (auto_tac (claset(),simpset() addsimps [hcmod])); |
|
1897 qed "hcmod_hcomplex_of_complex"; |
|