168 declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp] |
156 declare inj_on_Abs_hcomplex [THEN inj_on_iff, simp] |
169 Abs_hcomplex_inverse [simp] |
157 Abs_hcomplex_inverse [simp] |
170 |
158 |
171 declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp] |
159 declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp] |
172 |
160 |
173 declare hcomplexrel_iff [iff] |
|
174 |
161 |
175 lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)" |
162 lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)" |
176 apply (rule inj_on_inverseI) |
163 apply (rule inj_on_inverseI) |
177 apply (rule Rep_hcomplex_inverse) |
164 apply (rule Rep_hcomplex_inverse) |
178 done |
165 done |
179 |
166 |
180 lemma lemma_hcomplexrel_refl: "x: hcomplexrel `` {x}" |
167 lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}" |
181 apply (unfold hcomplexrel_def) |
168 by (simp add: hcomplexrel_def) |
182 apply (safe) |
169 |
183 apply auto |
170 lemma hcomplex_empty_not_mem [simp]: "{} \<notin> hcomplex" |
184 done |
171 apply (simp add: hcomplex_def hcomplexrel_def) |
185 declare lemma_hcomplexrel_refl [simp] |
|
186 |
|
187 lemma hcomplex_empty_not_mem: "{} \<notin> hcomplex" |
|
188 apply (unfold hcomplex_def) |
|
189 apply (auto elim!: quotientE) |
172 apply (auto elim!: quotientE) |
190 done |
173 done |
191 declare hcomplex_empty_not_mem [simp] |
174 |
192 |
175 lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \<noteq> {}" |
193 lemma Rep_hcomplex_nonempty: "Rep_hcomplex x \<noteq> {}" |
176 by (cut_tac x = x in Rep_hcomplex, auto) |
194 apply (cut_tac x = "x" in Rep_hcomplex) |
|
195 apply auto |
|
196 done |
|
197 declare Rep_hcomplex_nonempty [simp] |
|
198 |
177 |
199 lemma eq_Abs_hcomplex: |
178 lemma eq_Abs_hcomplex: |
200 "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P" |
179 "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P" |
201 apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE]) |
180 apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE]) |
202 apply (drule_tac f = Abs_hcomplex in arg_cong) |
181 apply (drule_tac f = Abs_hcomplex in arg_cong) |
203 apply (force simp add: Rep_hcomplex_inverse) |
182 apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def) |
204 done |
183 done |
|
184 |
|
185 (*??delete*) |
|
186 lemma hcomplexrel_iff [iff]: |
|
187 "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)" |
|
188 by (simp add: hcomplexrel_def) |
205 |
189 |
206 |
190 |
207 subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
191 subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
208 |
192 |
209 lemma hRe: |
193 lemma hRe: |
210 "hRe(Abs_hcomplex (hcomplexrel `` {X})) = |
194 "hRe(Abs_hcomplex (hcomplexrel `` {X})) = |
211 Abs_hypreal(hyprel `` {%n. Re(X n)})" |
195 Abs_hypreal(hyprel `` {%n. Re(X n)})" |
212 apply (unfold hRe_def) |
196 apply (simp add: hRe_def) |
213 apply (rule_tac f = "Abs_hypreal" in arg_cong) |
197 apply (rule_tac f = Abs_hypreal in arg_cong) |
214 apply (auto , ultra) |
198 apply (auto, ultra) |
215 done |
199 done |
216 |
200 |
217 lemma hIm: |
201 lemma hIm: |
218 "hIm(Abs_hcomplex (hcomplexrel `` {X})) = |
202 "hIm(Abs_hcomplex (hcomplexrel `` {X})) = |
219 Abs_hypreal(hyprel `` {%n. Im(X n)})" |
203 Abs_hypreal(hyprel `` {%n. Im(X n)})" |
220 apply (unfold hIm_def) |
204 apply (simp add: hIm_def) |
221 apply (rule_tac f = "Abs_hypreal" in arg_cong) |
205 apply (rule_tac f = Abs_hypreal in arg_cong) |
222 apply (auto , ultra) |
206 apply (auto, ultra) |
223 done |
207 done |
224 |
208 |
225 lemma hcomplex_hRe_hIm_cancel_iff: |
209 lemma hcomplex_hRe_hIm_cancel_iff: |
226 "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
210 "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
227 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
211 apply (rule eq_Abs_hcomplex [of z]) |
228 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
212 apply (rule eq_Abs_hcomplex [of w]) |
229 apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff) |
213 apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff) |
230 apply (ultra+) |
214 apply (ultra+) |
231 done |
215 done |
232 |
216 |
233 lemma hcomplex_hRe_zero: "hRe 0 = 0" |
217 lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" |
234 apply (unfold hcomplex_zero_def) |
218 by (simp add: hcomplex_zero_def hRe hypreal_zero_num) |
235 apply (simp (no_asm) add: hRe hypreal_zero_num) |
219 |
236 done |
220 lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" |
237 declare hcomplex_hRe_zero [simp] |
221 by (simp add: hcomplex_zero_def hIm hypreal_zero_num) |
238 |
222 |
239 lemma hcomplex_hIm_zero: "hIm 0 = 0" |
223 lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" |
240 apply (unfold hcomplex_zero_def) |
224 by (simp add: hcomplex_one_def hRe hypreal_one_num) |
241 apply (simp (no_asm) add: hIm hypreal_zero_num) |
225 |
242 done |
226 lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" |
243 declare hcomplex_hIm_zero [simp] |
227 by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num) |
244 |
|
245 lemma hcomplex_hRe_one: "hRe 1 = 1" |
|
246 apply (unfold hcomplex_one_def) |
|
247 apply (simp (no_asm) add: hRe hypreal_one_num) |
|
248 done |
|
249 declare hcomplex_hRe_one [simp] |
|
250 |
|
251 lemma hcomplex_hIm_one: "hIm 1 = 0" |
|
252 apply (unfold hcomplex_one_def) |
|
253 apply (simp (no_asm) add: hIm hypreal_one_def hypreal_zero_num) |
|
254 done |
|
255 declare hcomplex_hIm_one [simp] |
|
256 |
228 |
257 |
229 |
258 subsection{*Addition for Nonstandard Complex Numbers*} |
230 subsection{*Addition for Nonstandard Complex Numbers*} |
259 |
231 |
260 lemma hcomplex_add_congruent2: |
232 lemma hcomplex_add_congruent2: |
261 "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" |
233 "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" |
262 apply (unfold congruent2_def) |
234 by (auto simp add: congruent2_def, ultra) |
263 apply safe |
|
264 apply (ultra+) |
|
265 done |
|
266 |
235 |
267 lemma hcomplex_add: |
236 lemma hcomplex_add: |
268 "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
237 "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
269 Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" |
238 Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" |
270 apply (unfold hcomplex_add_def) |
239 apply (simp add: hcomplex_add_def) |
271 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
240 apply (rule_tac f = Abs_hcomplex in arg_cong) |
272 apply (auto, ultra) |
241 apply (auto, ultra) |
273 done |
242 done |
274 |
243 |
275 lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z" |
244 lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z" |
276 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
245 apply (rule eq_Abs_hcomplex [of z]) |
277 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
246 apply (rule eq_Abs_hcomplex [of w]) |
278 apply (simp add: complex_add_commute hcomplex_add) |
247 apply (simp add: complex_add_commute hcomplex_add) |
279 done |
248 done |
280 |
249 |
281 lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)" |
250 lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)" |
282 apply (rule_tac z = "z1" in eq_Abs_hcomplex) |
251 apply (rule eq_Abs_hcomplex [of z1]) |
283 apply (rule_tac z = "z2" in eq_Abs_hcomplex) |
252 apply (rule eq_Abs_hcomplex [of z2]) |
284 apply (rule_tac z = "z3" in eq_Abs_hcomplex) |
253 apply (rule eq_Abs_hcomplex [of z3]) |
285 apply (simp add: hcomplex_add complex_add_assoc) |
254 apply (simp add: hcomplex_add complex_add_assoc) |
286 done |
255 done |
287 |
256 |
288 lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z" |
257 lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z" |
289 apply (unfold hcomplex_zero_def) |
258 apply (rule eq_Abs_hcomplex [of z]) |
290 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
259 apply (simp add: hcomplex_zero_def hcomplex_add) |
291 apply (simp add: hcomplex_add) |
|
292 done |
260 done |
293 |
261 |
294 lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z" |
262 lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z" |
295 apply (simp add: hcomplex_add_zero_left hcomplex_add_commute) |
263 by (simp add: hcomplex_add_zero_left hcomplex_add_commute) |
296 done |
|
297 |
264 |
298 lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)" |
265 lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)" |
299 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
266 apply (rule eq_Abs_hcomplex [of x]) |
300 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
267 apply (rule eq_Abs_hcomplex [of y]) |
301 apply (auto simp add: hRe hcomplex_add hypreal_add complex_Re_add) |
268 apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add) |
302 done |
269 done |
303 |
270 |
304 lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)" |
271 lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)" |
305 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
272 apply (rule eq_Abs_hcomplex [of x]) |
306 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
273 apply (rule eq_Abs_hcomplex [of y]) |
307 apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add) |
274 apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add) |
308 done |
275 done |
309 |
276 |
310 |
277 |
311 subsection{*Additive Inverse on Nonstandard Complex Numbers*} |
278 subsection{*Additive Inverse on Nonstandard Complex Numbers*} |
312 |
279 |
313 lemma hcomplex_minus_congruent: |
280 lemma hcomplex_minus_congruent: |
314 "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})" |
281 "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})" |
315 apply (unfold congruent_def) |
282 by (simp add: congruent_def) |
316 apply safe |
|
317 apply (ultra+) |
|
318 done |
|
319 |
283 |
320 lemma hcomplex_minus: |
284 lemma hcomplex_minus: |
321 "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
285 "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
322 Abs_hcomplex(hcomplexrel `` {%n. -(X n)})" |
286 Abs_hcomplex(hcomplexrel `` {%n. -(X n)})" |
323 apply (unfold hcomplex_minus_def) |
287 apply (simp add: hcomplex_minus_def) |
324 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
288 apply (rule_tac f = Abs_hcomplex in arg_cong) |
325 apply (auto, ultra) |
289 apply (auto, ultra) |
326 done |
290 done |
327 |
291 |
328 lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)" |
292 lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)" |
329 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
293 apply (rule eq_Abs_hcomplex [of z]) |
330 apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) |
294 apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) |
331 done |
295 done |
332 |
296 |
333 |
297 |
334 subsection{*Multiplication for Nonstandard Complex Numbers*} |
298 subsection{*Multiplication for Nonstandard Complex Numbers*} |
335 |
299 |
336 lemma hcomplex_mult: |
300 lemma hcomplex_mult: |
337 "Abs_hcomplex(hcomplexrel``{%n. X n}) * |
301 "Abs_hcomplex(hcomplexrel``{%n. X n}) * |
338 Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
302 Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
339 Abs_hcomplex(hcomplexrel``{%n. X n * Y n})" |
303 Abs_hcomplex(hcomplexrel``{%n. X n * Y n})" |
340 apply (unfold hcomplex_mult_def) |
304 apply (simp add: hcomplex_mult_def) |
341 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
305 apply (rule_tac f = Abs_hcomplex in arg_cong) |
342 apply (auto, ultra) |
306 apply (auto, ultra) |
343 done |
307 done |
344 |
308 |
345 lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w" |
309 lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w" |
346 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
310 apply (rule eq_Abs_hcomplex [of w]) |
347 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
311 apply (rule eq_Abs_hcomplex [of z]) |
348 apply (auto simp add: hcomplex_mult complex_mult_commute) |
312 apply (simp add: hcomplex_mult complex_mult_commute) |
349 done |
313 done |
350 |
314 |
351 lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)" |
315 lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)" |
352 apply (rule_tac z = "u" in eq_Abs_hcomplex) |
316 apply (rule eq_Abs_hcomplex [of u]) |
353 apply (rule_tac z = "v" in eq_Abs_hcomplex) |
317 apply (rule eq_Abs_hcomplex [of v]) |
354 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
318 apply (rule eq_Abs_hcomplex [of w]) |
355 apply (auto simp add: hcomplex_mult complex_mult_assoc) |
319 apply (simp add: hcomplex_mult complex_mult_assoc) |
356 done |
320 done |
357 |
321 |
358 lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z" |
322 lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z" |
359 apply (unfold hcomplex_one_def) |
323 apply (rule eq_Abs_hcomplex [of z]) |
360 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
324 apply (simp add: hcomplex_one_def hcomplex_mult) |
361 apply (auto simp add: hcomplex_mult) |
|
362 done |
325 done |
363 |
326 |
364 lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0" |
327 lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0" |
365 apply (unfold hcomplex_zero_def) |
328 apply (rule eq_Abs_hcomplex [of z]) |
366 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
329 apply (simp add: hcomplex_zero_def hcomplex_mult) |
367 apply (auto simp add: hcomplex_mult) |
|
368 done |
330 done |
369 |
331 |
370 lemma hcomplex_add_mult_distrib: |
332 lemma hcomplex_add_mult_distrib: |
371 "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)" |
333 "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)" |
372 apply (rule_tac z = "z1" in eq_Abs_hcomplex) |
334 apply (rule eq_Abs_hcomplex [of z1]) |
373 apply (rule_tac z = "z2" in eq_Abs_hcomplex) |
335 apply (rule eq_Abs_hcomplex [of z2]) |
374 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
336 apply (rule eq_Abs_hcomplex [of w]) |
375 apply (auto simp add: hcomplex_mult hcomplex_add left_distrib) |
337 apply (simp add: hcomplex_mult hcomplex_add left_distrib) |
376 done |
338 done |
377 |
339 |
378 lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)" |
340 lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)" |
379 apply (unfold hcomplex_zero_def hcomplex_one_def) |
341 by (simp add: hcomplex_zero_def hcomplex_one_def) |
380 apply auto |
342 |
381 done |
|
382 declare hcomplex_zero_not_eq_one [simp] |
|
383 declare hcomplex_zero_not_eq_one [THEN not_sym, simp] |
343 declare hcomplex_zero_not_eq_one [THEN not_sym, simp] |
384 |
344 |
385 |
345 |
386 subsection{*Inverse of Nonstandard Complex Number*} |
346 subsection{*Inverse of Nonstandard Complex Number*} |
387 |
347 |
388 lemma hcomplex_inverse: |
348 lemma hcomplex_inverse: |
389 "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
349 "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
390 Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})" |
350 Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})" |
391 apply (unfold hcinv_def) |
351 apply (simp add: hcinv_def) |
392 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
352 apply (rule_tac f = Abs_hcomplex in arg_cong) |
393 apply (auto, ultra) |
353 apply (auto, ultra) |
394 done |
354 done |
395 |
355 |
396 lemma hcomplex_mult_inv_left: |
356 lemma hcomplex_mult_inv_left: |
397 "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)" |
357 "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)" |
398 apply (unfold hcomplex_zero_def hcomplex_one_def) |
358 apply (rule eq_Abs_hcomplex [of z]) |
399 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
359 apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra) |
400 apply (auto simp add: hcomplex_inverse hcomplex_mult) |
|
401 apply (ultra) |
|
402 apply (rule ccontr) |
360 apply (rule ccontr) |
403 apply (drule left_inverse) |
361 apply (drule left_inverse, auto) |
404 apply auto |
|
405 done |
362 done |
406 |
363 |
407 subsection {* The Field of Nonstandard Complex Numbers *} |
364 subsection {* The Field of Nonstandard Complex Numbers *} |
408 |
365 |
409 instance hcomplex :: field |
366 instance hcomplex :: field |
429 by (rule hcomplex_zero_not_eq_one) |
386 by (rule hcomplex_zero_not_eq_one) |
430 show "(u + v) * w = u * w + v * w" |
387 show "(u + v) * w = u * w + v * w" |
431 by (simp add: hcomplex_add_mult_distrib) |
388 by (simp add: hcomplex_add_mult_distrib) |
432 show "z+u = z+v ==> u=v" |
389 show "z+u = z+v ==> u=v" |
433 proof - |
390 proof - |
434 assume eq: "z+u = z+v" |
391 assume eq: "z+u = z+v" |
435 hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc) |
392 hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc) |
436 thus "u = v" |
393 thus "u = v" |
437 by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left) |
394 by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left) |
438 qed |
395 qed |
439 assume neq: "w \<noteq> 0" |
396 assume neq: "w \<noteq> 0" |
440 thus "z / w = z * inverse w" |
397 thus "z / w = z * inverse w" |
441 by (simp add: hcomplex_divide_def) |
398 by (simp add: hcomplex_divide_def) |
442 show "inverse w * w = 1" |
399 show "inverse w * w = 1" |
443 by (rule hcomplex_mult_inv_left) |
400 by (rule hcomplex_mult_inv_left) |
444 qed |
401 qed |
445 |
402 |
446 lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0" |
|
447 apply (simp add: hcomplex_zero_def hcomplex_inverse) |
|
448 done |
|
449 |
|
450 lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0" |
|
451 apply (simp add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO) |
|
452 done |
|
453 |
|
454 instance hcomplex :: division_by_zero |
403 instance hcomplex :: division_by_zero |
455 proof |
404 proof |
|
405 show inv: "inverse 0 = (0::hcomplex)" |
|
406 by (simp add: hcomplex_inverse hcomplex_zero_def) |
456 fix x :: hcomplex |
407 fix x :: hcomplex |
457 show "inverse 0 = (0::hcomplex)" by (rule HCOMPLEX_INVERSE_ZERO) |
408 show "x/0 = 0" |
458 show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) |
409 by (simp add: hcomplex_divide_def inv) |
459 qed |
410 qed |
460 |
411 |
|
412 |
461 subsection{*More Minus Laws*} |
413 subsection{*More Minus Laws*} |
462 |
414 |
463 lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)" |
|
464 apply (rule inj_onI) |
|
465 apply (drule_tac f = "uminus" in arg_cong) |
|
466 apply simp |
|
467 done |
|
468 |
|
469 lemma hRe_minus: "hRe(-z) = - hRe(z)" |
415 lemma hRe_minus: "hRe(-z) = - hRe(z)" |
470 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
416 apply (rule eq_Abs_hcomplex [of z]) |
471 apply (auto simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus) |
417 apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus) |
472 done |
418 done |
473 |
419 |
474 lemma hIm_minus: "hIm(-z) = - hIm(z)" |
420 lemma hIm_minus: "hIm(-z) = - hIm(z)" |
475 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
421 apply (rule eq_Abs_hcomplex [of z]) |
476 apply (auto simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus) |
422 apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus) |
477 done |
423 done |
478 |
424 |
479 lemma hcomplex_add_minus_eq_minus: |
425 lemma hcomplex_add_minus_eq_minus: |
480 "x + y = (0::hcomplex) ==> x = -y" |
426 "x + y = (0::hcomplex) ==> x = -y" |
481 apply (drule Ring_and_Field.equals_zero_I) |
427 apply (drule Ring_and_Field.equals_zero_I) |
482 apply (simp add: minus_equation_iff [of x y]) |
428 apply (simp add: minus_equation_iff [of x y]) |
483 done |
429 done |
484 |
430 |
485 |
431 |
486 subsection{*More Multiplication Laws*} |
432 subsection{*More Multiplication Laws*} |
487 |
433 |
488 lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" |
434 lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" |
489 apply (rule Ring_and_Field.mult_1_right) |
435 by (rule Ring_and_Field.mult_1_right) |
490 done |
436 |
491 |
437 lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z" |
492 lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z" |
438 by simp |
493 apply (simp (no_asm)) |
439 |
494 done |
440 lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z" |
495 declare hcomplex_mult_minus_one [simp] |
441 by (subst hcomplex_mult_commute, simp) |
496 |
|
497 lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z" |
|
498 apply (subst hcomplex_mult_commute) |
|
499 apply (simp (no_asm)) |
|
500 done |
|
501 declare hcomplex_mult_minus_one_right [simp] |
|
502 |
442 |
503 lemma hcomplex_mult_left_cancel: |
443 lemma hcomplex_mult_left_cancel: |
504 "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)" |
444 "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)" |
505 by (simp add: field_mult_cancel_left) |
445 by (simp add: field_mult_cancel_left) |
506 |
446 |
507 lemma hcomplex_mult_right_cancel: |
447 lemma hcomplex_mult_right_cancel: |
508 "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)" |
448 "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)" |
509 apply (simp add: Ring_and_Field.field_mult_cancel_right); |
449 by (simp add: Ring_and_Field.field_mult_cancel_right) |
510 done |
|
511 |
450 |
512 |
451 |
513 subsection{*Subraction and Division*} |
452 subsection{*Subraction and Division*} |
514 |
453 |
515 lemma hcomplex_diff: |
454 lemma hcomplex_diff: |
516 "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
455 "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
517 Abs_hcomplex(hcomplexrel``{%n. X n - Y n})" |
456 Abs_hcomplex(hcomplexrel``{%n. X n - Y n})" |
518 apply (unfold hcomplex_diff_def) |
457 by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def) |
519 apply (auto simp add: hcomplex_minus hcomplex_add complex_diff_def) |
458 |
520 done |
459 lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" |
521 |
460 by (rule Ring_and_Field.diff_eq_eq) |
522 lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)" |
|
523 apply (rule Ring_and_Field.diff_eq_eq) |
|
524 done |
|
525 |
461 |
526 lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" |
462 lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" |
527 apply (rule Ring_and_Field.add_divide_distrib) |
463 by (rule Ring_and_Field.add_divide_distrib) |
528 done |
|
529 |
464 |
530 |
465 |
531 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} |
466 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} |
532 |
467 |
533 lemma hcomplex_of_hypreal: |
468 lemma hcomplex_of_hypreal: |
534 "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = |
469 "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = |
535 Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})" |
470 Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})" |
536 apply (unfold hcomplex_of_hypreal_def) |
471 apply (simp add: hcomplex_of_hypreal_def) |
537 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
472 apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra) |
538 apply auto |
473 done |
539 apply (ultra) |
474 |
540 done |
475 lemma hcomplex_of_hypreal_cancel_iff [iff]: |
541 |
|
542 lemma inj_hcomplex_of_hypreal: "inj hcomplex_of_hypreal" |
|
543 apply (rule inj_onI) |
|
544 apply (rule_tac z = "x" in eq_Abs_hypreal) |
|
545 apply (rule_tac z = "y" in eq_Abs_hypreal) |
|
546 apply (auto simp add: hcomplex_of_hypreal) |
|
547 done |
|
548 |
|
549 lemma hcomplex_of_hypreal_cancel_iff: |
|
550 "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" |
476 "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" |
551 apply (auto dest: inj_hcomplex_of_hypreal [THEN injD]) |
477 apply (rule eq_Abs_hypreal [of x]) |
552 done |
478 apply (rule eq_Abs_hypreal [of y]) |
553 declare hcomplex_of_hypreal_cancel_iff [iff] |
479 apply (simp add: hcomplex_of_hypreal) |
|
480 done |
554 |
481 |
555 lemma hcomplex_of_hypreal_minus: |
482 lemma hcomplex_of_hypreal_minus: |
556 "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" |
483 "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" |
557 apply (rule_tac z = "x" in eq_Abs_hypreal) |
484 apply (rule eq_Abs_hypreal [of x]) |
558 apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus) |
485 apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus) |
559 done |
486 done |
560 |
487 |
561 lemma hcomplex_of_hypreal_inverse: |
488 lemma hcomplex_of_hypreal_inverse: |
562 "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" |
489 "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" |
563 apply (rule_tac z = "x" in eq_Abs_hypreal) |
490 apply (rule eq_Abs_hypreal [of x]) |
564 apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse) |
491 apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse) |
565 done |
492 done |
566 |
493 |
567 lemma hcomplex_of_hypreal_add: |
494 lemma hcomplex_of_hypreal_add: |
568 "hcomplex_of_hypreal x + hcomplex_of_hypreal y = |
495 "hcomplex_of_hypreal x + hcomplex_of_hypreal y = |
569 hcomplex_of_hypreal (x + y)" |
496 hcomplex_of_hypreal (x + y)" |
570 apply (rule_tac z = "x" in eq_Abs_hypreal) |
497 apply (rule eq_Abs_hypreal [of x]) |
571 apply (rule_tac z = "y" in eq_Abs_hypreal) |
498 apply (rule eq_Abs_hypreal [of y]) |
572 apply (auto simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add) |
499 apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add) |
573 done |
500 done |
574 |
501 |
575 lemma hcomplex_of_hypreal_diff: |
502 lemma hcomplex_of_hypreal_diff: |
576 "hcomplex_of_hypreal x - hcomplex_of_hypreal y = |
503 "hcomplex_of_hypreal x - hcomplex_of_hypreal y = |
577 hcomplex_of_hypreal (x - y)" |
504 hcomplex_of_hypreal (x - y)" |
578 apply (unfold hcomplex_diff_def) |
505 by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def) |
579 apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def) |
|
580 done |
|
581 |
506 |
582 lemma hcomplex_of_hypreal_mult: |
507 lemma hcomplex_of_hypreal_mult: |
583 "hcomplex_of_hypreal x * hcomplex_of_hypreal y = |
508 "hcomplex_of_hypreal x * hcomplex_of_hypreal y = |
584 hcomplex_of_hypreal (x * y)" |
509 hcomplex_of_hypreal (x * y)" |
585 apply (rule_tac z = "x" in eq_Abs_hypreal) |
510 apply (rule eq_Abs_hypreal [of x]) |
586 apply (rule_tac z = "y" in eq_Abs_hypreal) |
511 apply (rule eq_Abs_hypreal [of y]) |
587 apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult |
512 apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult) |
588 complex_of_real_mult) |
|
589 done |
513 done |
590 |
514 |
591 lemma hcomplex_of_hypreal_divide: |
515 lemma hcomplex_of_hypreal_divide: |
592 "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)" |
516 "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)" |
593 apply (unfold hcomplex_divide_def) |
517 apply (simp add: hcomplex_divide_def) |
594 apply (case_tac "y=0") |
518 apply (case_tac "y=0", simp) |
595 apply (simp) |
|
596 apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric]) |
519 apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric]) |
597 apply (simp (no_asm) add: hypreal_divide_def) |
520 apply (simp add: hypreal_divide_def) |
598 done |
521 done |
599 |
522 |
600 lemma hcomplex_of_hypreal_one [simp]: |
523 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" |
601 "hcomplex_of_hypreal 1 = 1" |
524 by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num) |
602 apply (unfold hcomplex_one_def) |
525 |
603 apply (auto simp add: hcomplex_of_hypreal hypreal_one_num) |
526 lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0" |
604 done |
527 by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal) |
605 |
528 |
606 lemma hcomplex_of_hypreal_zero [simp]: |
529 lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z" |
607 "hcomplex_of_hypreal 0 = 0" |
530 apply (rule eq_Abs_hypreal [of z]) |
608 apply (unfold hcomplex_zero_def hypreal_zero_def) |
|
609 apply (auto simp add: hcomplex_of_hypreal) |
|
610 done |
|
611 |
|
612 lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z" |
|
613 apply (rule_tac z = "z" in eq_Abs_hypreal) |
|
614 apply (auto simp add: hcomplex_of_hypreal hRe) |
531 apply (auto simp add: hcomplex_of_hypreal hRe) |
615 done |
532 done |
616 declare hRe_hcomplex_of_hypreal [simp] |
533 |
617 |
534 lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0" |
618 lemma hIm_hcomplex_of_hypreal: "hIm(hcomplex_of_hypreal z) = 0" |
535 apply (rule eq_Abs_hypreal [of z]) |
619 apply (rule_tac z = "z" in eq_Abs_hypreal) |
|
620 apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num) |
536 apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num) |
621 done |
537 done |
622 declare hIm_hcomplex_of_hypreal [simp] |
538 |
623 |
539 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
624 lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon \<noteq> 0" |
540 "hcomplex_of_hypreal epsilon \<noteq> 0" |
625 apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def) |
541 by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def) |
626 done |
|
627 declare hcomplex_of_hypreal_epsilon_not_zero [simp] |
|
628 |
542 |
629 |
543 |
630 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} |
544 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} |
631 |
545 |
632 lemma hcmod: |
546 lemma hcmod: |
633 "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
547 "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
634 Abs_hypreal(hyprel `` {%n. cmod (X n)})" |
548 Abs_hypreal(hyprel `` {%n. cmod (X n)})" |
635 |
549 |
636 apply (unfold hcmod_def) |
550 apply (simp add: hcmod_def) |
637 apply (rule_tac f = "Abs_hypreal" in arg_cong) |
551 apply (rule_tac f = Abs_hypreal in arg_cong) |
638 apply (auto, ultra) |
552 apply (auto, ultra) |
639 done |
553 done |
640 |
554 |
641 lemma hcmod_zero [simp]: |
555 lemma hcmod_zero [simp]: "hcmod(0) = 0" |
642 "hcmod(0) = 0" |
556 apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod) |
643 apply (unfold hcomplex_zero_def hypreal_zero_def) |
557 done |
644 apply (auto simp add: hcmod) |
558 |
645 done |
559 lemma hcmod_one [simp]: "hcmod(1) = 1" |
646 |
560 by (simp add: hcomplex_one_def hcmod hypreal_one_num) |
647 lemma hcmod_one: |
561 |
648 "hcmod(1) = 1" |
562 lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x" |
649 apply (unfold hcomplex_one_def) |
563 apply (rule eq_Abs_hypreal [of x]) |
650 apply (auto simp add: hcmod hypreal_one_num) |
|
651 done |
|
652 declare hcmod_one [simp] |
|
653 |
|
654 lemma hcmod_hcomplex_of_hypreal: "hcmod(hcomplex_of_hypreal x) = abs x" |
|
655 apply (rule_tac z = "x" in eq_Abs_hypreal) |
|
656 apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs) |
564 apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs) |
657 done |
565 done |
658 declare hcmod_hcomplex_of_hypreal [simp] |
|
659 |
566 |
660 lemma hcomplex_of_hypreal_abs: |
567 lemma hcomplex_of_hypreal_abs: |
661 "hcomplex_of_hypreal (abs x) = |
568 "hcomplex_of_hypreal (abs x) = |
662 hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" |
569 hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" |
663 apply (simp (no_asm)) |
570 by simp |
664 done |
|
665 |
571 |
666 |
572 |
667 subsection{*Conjugation*} |
573 subsection{*Conjugation*} |
668 |
574 |
669 lemma hcnj: |
575 lemma hcnj: |
670 "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
576 "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
671 Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" |
577 Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" |
672 apply (unfold hcnj_def) |
578 apply (simp add: hcnj_def) |
673 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
579 apply (rule_tac f = Abs_hcomplex in arg_cong) |
674 apply (auto, ultra) |
580 apply (auto, ultra) |
675 done |
581 done |
676 |
582 |
677 lemma inj_hcnj: "inj hcnj" |
583 lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)" |
678 apply (rule inj_onI) |
584 apply (rule eq_Abs_hcomplex [of x]) |
679 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
585 apply (rule eq_Abs_hcomplex [of y]) |
680 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
586 apply (simp add: hcnj) |
681 apply (auto simp add: hcnj) |
587 done |
682 done |
588 |
683 |
589 lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z" |
684 lemma hcomplex_hcnj_cancel_iff: "(hcnj x = hcnj y) = (x = y)" |
590 apply (rule eq_Abs_hcomplex [of z]) |
685 apply (auto dest: inj_hcnj [THEN injD]) |
591 apply (simp add: hcnj) |
686 done |
592 done |
687 declare hcomplex_hcnj_cancel_iff [simp] |
593 |
688 |
594 lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]: |
689 lemma hcomplex_hcnj_hcnj: "hcnj (hcnj z) = z" |
|
690 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
|
691 apply (auto simp add: hcnj) |
|
692 done |
|
693 declare hcomplex_hcnj_hcnj [simp] |
|
694 |
|
695 lemma hcomplex_hcnj_hcomplex_of_hypreal: |
|
696 "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" |
595 "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" |
697 apply (rule_tac z = "x" in eq_Abs_hypreal) |
596 apply (rule eq_Abs_hypreal [of x]) |
698 apply (auto simp add: hcnj hcomplex_of_hypreal) |
597 apply (simp add: hcnj hcomplex_of_hypreal) |
699 done |
598 done |
700 declare hcomplex_hcnj_hcomplex_of_hypreal [simp] |
599 |
701 |
600 lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z" |
702 lemma hcomplex_hmod_hcnj: "hcmod (hcnj z) = hcmod z" |
601 apply (rule eq_Abs_hcomplex [of z]) |
703 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
602 apply (simp add: hcnj hcmod) |
704 apply (auto simp add: hcnj hcmod) |
603 done |
705 done |
|
706 declare hcomplex_hmod_hcnj [simp] |
|
707 |
604 |
708 lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z" |
605 lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z" |
709 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
606 apply (rule eq_Abs_hcomplex [of z]) |
710 apply (auto simp add: hcnj hcomplex_minus complex_cnj_minus) |
607 apply (simp add: hcnj hcomplex_minus complex_cnj_minus) |
711 done |
608 done |
712 |
609 |
713 lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)" |
610 lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)" |
714 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
611 apply (rule eq_Abs_hcomplex [of z]) |
715 apply (auto simp add: hcnj hcomplex_inverse complex_cnj_inverse) |
612 apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse) |
716 done |
613 done |
717 |
614 |
718 lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)" |
615 lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)" |
719 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
616 apply (rule eq_Abs_hcomplex [of z]) |
720 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
617 apply (rule eq_Abs_hcomplex [of w]) |
721 apply (auto simp add: hcnj hcomplex_add complex_cnj_add) |
618 apply (simp add: hcnj hcomplex_add complex_cnj_add) |
722 done |
619 done |
723 |
620 |
724 lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)" |
621 lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)" |
725 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
622 apply (rule eq_Abs_hcomplex [of z]) |
726 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
623 apply (rule eq_Abs_hcomplex [of w]) |
727 apply (auto simp add: hcnj hcomplex_diff complex_cnj_diff) |
624 apply (simp add: hcnj hcomplex_diff complex_cnj_diff) |
728 done |
625 done |
729 |
626 |
730 lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)" |
627 lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)" |
731 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
628 apply (rule eq_Abs_hcomplex [of z]) |
732 apply (rule_tac z = "w" in eq_Abs_hcomplex) |
629 apply (rule eq_Abs_hcomplex [of w]) |
733 apply (auto simp add: hcnj hcomplex_mult complex_cnj_mult) |
630 apply (simp add: hcnj hcomplex_mult complex_cnj_mult) |
734 done |
631 done |
735 |
632 |
736 lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)" |
633 lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)" |
737 apply (unfold hcomplex_divide_def) |
634 by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse) |
738 apply (simp (no_asm) add: hcomplex_hcnj_mult hcomplex_hcnj_inverse) |
635 |
739 done |
636 lemma hcnj_one [simp]: "hcnj 1 = 1" |
740 |
637 by (simp add: hcomplex_one_def hcnj) |
741 lemma hcnj_one: "hcnj 1 = 1" |
638 |
742 apply (unfold hcomplex_one_def) |
639 lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0" |
743 apply (simp (no_asm) add: hcnj) |
640 by (simp add: hcomplex_zero_def hcnj) |
744 done |
641 |
745 declare hcnj_one [simp] |
642 lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)" |
746 |
643 apply (rule eq_Abs_hcomplex [of z]) |
747 lemma hcomplex_hcnj_zero: |
644 apply (simp add: hcomplex_zero_def hcnj) |
748 "hcnj 0 = 0" |
645 done |
749 apply (unfold hcomplex_zero_def) |
|
750 apply (auto simp add: hcnj) |
|
751 done |
|
752 declare hcomplex_hcnj_zero [simp] |
|
753 |
|
754 lemma hcomplex_hcnj_zero_iff: "(hcnj z = 0) = (z = 0)" |
|
755 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
|
756 apply (auto simp add: hcomplex_zero_def hcnj) |
|
757 done |
|
758 declare hcomplex_hcnj_zero_iff [iff] |
|
759 |
646 |
760 lemma hcomplex_mult_hcnj: |
647 lemma hcomplex_mult_hcnj: |
761 "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" |
648 "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" |
762 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
649 apply (rule eq_Abs_hcomplex [of z]) |
763 apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2) |
650 apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add |
|
651 hypreal_mult complex_mult_cnj numeral_2_eq_2) |
764 done |
652 done |
765 |
653 |
766 |
654 |
767 subsection{*More Theorems about the Function @{term hcmod}*} |
655 subsection{*More Theorems about the Function @{term hcmod}*} |
768 |
656 |
769 lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)" |
657 lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)" |
770 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
658 apply (rule eq_Abs_hcomplex [of x]) |
771 apply (auto simp add: hcmod hcomplex_zero_def hypreal_zero_num) |
659 apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num) |
772 done |
660 done |
773 declare hcomplex_hcmod_eq_zero_cancel [simp] |
661 |
774 |
662 lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: |
775 lemma hcmod_hcomplex_of_hypreal_of_nat: |
|
776 "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" |
663 "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" |
777 apply (simp add: abs_if linorder_not_less) |
664 apply (simp add: abs_if linorder_not_less) |
778 done |
665 done |
779 declare hcmod_hcomplex_of_hypreal_of_nat [simp] |
666 |
780 |
667 lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]: |
781 lemma hcmod_hcomplex_of_hypreal_of_hypnat: |
|
782 "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" |
668 "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" |
783 apply (simp add: abs_if linorder_not_less) |
669 apply (simp add: abs_if linorder_not_less) |
784 done |
670 done |
785 declare hcmod_hcomplex_of_hypreal_of_hypnat [simp] |
671 |
786 |
672 lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)" |
787 lemma hcmod_minus: "hcmod (-x) = hcmod(x)" |
673 apply (rule eq_Abs_hcomplex [of x]) |
788 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
674 apply (simp add: hcmod hcomplex_minus) |
789 apply (auto simp add: hcmod hcomplex_minus) |
675 done |
790 done |
|
791 declare hcmod_minus [simp] |
|
792 |
676 |
793 lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2" |
677 lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2" |
794 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
678 apply (rule eq_Abs_hcomplex [of z]) |
795 apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2) |
679 apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2) |
796 done |
680 done |
797 |
681 |
798 lemma hcmod_ge_zero: "(0::hypreal) \<le> hcmod x" |
682 lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x" |
799 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
683 apply (rule eq_Abs_hcomplex [of x]) |
800 apply (auto simp add: hcmod hypreal_zero_num hypreal_le) |
684 apply (simp add: hcmod hypreal_zero_num hypreal_le) |
801 done |
685 done |
802 declare hcmod_ge_zero [simp] |
686 |
803 |
687 lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x" |
804 lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x" |
688 by (simp add: abs_if linorder_not_less) |
805 apply (simp add: abs_if linorder_not_less) |
|
806 done |
|
807 declare hrabs_hcmod_cancel [simp] |
|
808 |
689 |
809 lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)" |
690 lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)" |
810 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
691 apply (rule eq_Abs_hcomplex [of x]) |
811 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
692 apply (rule eq_Abs_hcomplex [of y]) |
812 apply (auto simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult) |
693 apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult) |
813 done |
694 done |
814 |
695 |
815 lemma hcmod_add_squared_eq: |
696 lemma hcmod_add_squared_eq: |
816 "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)" |
697 "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)" |
817 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
698 apply (rule eq_Abs_hcomplex [of x]) |
818 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
699 apply (rule eq_Abs_hcomplex [of y]) |
819 apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult |
700 apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult |
820 numeral_2_eq_2 realpow_two [symmetric] |
701 numeral_2_eq_2 realpow_two [symmetric] |
821 simp del: realpow_Suc) |
702 del: realpow_Suc) |
822 apply (auto simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq |
703 apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq |
823 hypreal_add [symmetric] hypreal_mult [symmetric] |
704 hypreal_add [symmetric] hypreal_mult [symmetric] |
824 hypreal_of_real_def [symmetric]) |
705 hypreal_of_real_def [symmetric]) |
825 done |
706 done |
826 |
707 |
827 lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)" |
708 lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)" |
828 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
709 apply (rule eq_Abs_hcomplex [of x]) |
829 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
710 apply (rule eq_Abs_hcomplex [of y]) |
830 apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le) |
711 apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le) |
831 done |
712 done |
832 declare hcomplex_hRe_mult_hcnj_le_hcmod [simp] |
713 |
833 |
714 lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: "hRe(x * hcnj y) \<le> hcmod(x * y)" |
834 lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) \<le> hcmod(x * y)" |
715 apply (cut_tac x = x and y = y in hcomplex_hRe_mult_hcnj_le_hcmod) |
835 apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod) |
|
836 apply (simp add: hcmod_mult) |
716 apply (simp add: hcmod_mult) |
837 done |
717 done |
838 declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp] |
718 |
839 |
719 lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2" |
840 lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2" |
720 apply (rule eq_Abs_hcomplex [of x]) |
841 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
721 apply (rule eq_Abs_hcomplex [of y]) |
842 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
722 apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add |
843 apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add |
|
844 hypreal_le realpow_two [symmetric] numeral_2_eq_2 |
723 hypreal_le realpow_two [symmetric] numeral_2_eq_2 |
845 simp del: realpow_Suc) |
724 del: realpow_Suc) |
846 apply (simp (no_asm) add: numeral_2_eq_2 [symmetric]) |
725 apply (simp add: numeral_2_eq_2 [symmetric]) |
847 done |
726 done |
848 declare hcmod_triangle_squared [simp] |
727 |
849 |
728 lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)" |
850 lemma hcmod_triangle_ineq: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)" |
729 apply (rule eq_Abs_hcomplex [of x]) |
851 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
730 apply (rule eq_Abs_hcomplex [of y]) |
852 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
731 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le) |
853 apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le) |
732 done |
854 done |
733 |
855 declare hcmod_triangle_ineq [simp] |
734 lemma hcmod_triangle_ineq2 [simp]: "hcmod(b + a) - hcmod b \<le> hcmod a" |
856 |
735 apply (cut_tac x1 = b and y1 = a and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono]) |
857 lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b \<le> hcmod a" |
|
858 apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono]) |
|
859 apply (simp add: add_ac) |
736 apply (simp add: add_ac) |
860 done |
737 done |
861 declare hcmod_triangle_ineq2 [simp] |
|
862 |
738 |
863 lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)" |
739 lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)" |
864 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
740 apply (rule eq_Abs_hcomplex [of x]) |
865 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
741 apply (rule eq_Abs_hcomplex [of y]) |
866 apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute) |
742 apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute) |
867 done |
743 done |
868 |
744 |
869 lemma hcmod_add_less: |
745 lemma hcmod_add_less: |
870 "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" |
746 "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" |
871 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
747 apply (rule eq_Abs_hcomplex [of x]) |
872 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
748 apply (rule eq_Abs_hcomplex [of y]) |
873 apply (rule_tac z = "r" in eq_Abs_hypreal) |
749 apply (rule eq_Abs_hypreal [of r]) |
874 apply (rule_tac z = "s" in eq_Abs_hypreal) |
750 apply (rule eq_Abs_hypreal [of s]) |
875 apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_less) |
751 apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra) |
876 apply ultra |
|
877 apply (auto intro: complex_mod_add_less) |
752 apply (auto intro: complex_mod_add_less) |
878 done |
753 done |
879 |
754 |
880 lemma hcmod_mult_less: |
755 lemma hcmod_mult_less: |
881 "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" |
756 "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" |
882 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
757 apply (rule eq_Abs_hcomplex [of x]) |
883 apply (rule_tac z = "y" in eq_Abs_hcomplex) |
758 apply (rule eq_Abs_hcomplex [of y]) |
884 apply (rule_tac z = "r" in eq_Abs_hypreal) |
759 apply (rule eq_Abs_hypreal [of r]) |
885 apply (rule_tac z = "s" in eq_Abs_hypreal) |
760 apply (rule eq_Abs_hypreal [of s]) |
886 apply (auto simp add: hcmod hypreal_mult hypreal_less hcomplex_mult) |
761 apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra) |
887 apply ultra |
|
888 apply (auto intro: complex_mod_mult_less) |
762 apply (auto intro: complex_mod_mult_less) |
889 done |
763 done |
890 |
764 |
891 lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
765 lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
892 apply (rule_tac z = "a" in eq_Abs_hcomplex) |
766 apply (rule eq_Abs_hcomplex [of a]) |
893 apply (rule_tac z = "b" in eq_Abs_hcomplex) |
767 apply (rule eq_Abs_hcomplex [of b]) |
894 apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le) |
768 apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le) |
895 done |
769 done |
896 declare hcmod_diff_ineq [simp] |
|
897 |
|
898 |
770 |
899 |
771 |
900 subsection{*A Few Nonlinear Theorems*} |
772 subsection{*A Few Nonlinear Theorems*} |
901 |
773 |
902 lemma hcpow: |
774 lemma hcpow: |
903 "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow |
775 "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow |
904 Abs_hypnat(hypnatrel``{%n. Y n}) = |
776 Abs_hypnat(hypnatrel``{%n. Y n}) = |
905 Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})" |
777 Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})" |
906 apply (unfold hcpow_def) |
778 apply (simp add: hcpow_def) |
907 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
779 apply (rule_tac f = Abs_hcomplex in arg_cong) |
908 apply (auto, ultra) |
780 apply (auto, ultra) |
909 done |
781 done |
910 |
782 |
911 lemma hcomplex_of_hypreal_hyperpow: |
783 lemma hcomplex_of_hypreal_hyperpow: |
912 "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
784 "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
913 apply (rule_tac z = "x" in eq_Abs_hypreal) |
785 apply (rule eq_Abs_hypreal [of x]) |
914 apply (rule_tac z = "n" in eq_Abs_hypnat) |
786 apply (rule eq_Abs_hypnat [of n]) |
915 apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow) |
787 apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow) |
916 done |
788 done |
917 |
789 |
918 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n" |
790 lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n" |
919 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
791 apply (rule eq_Abs_hcomplex [of x]) |
920 apply (rule_tac z = "n" in eq_Abs_hypnat) |
792 apply (rule eq_Abs_hypnat [of n]) |
921 apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow) |
793 apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow) |
922 done |
794 done |
923 |
795 |
924 lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)" |
796 lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)" |
925 apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO) |
797 apply (case_tac "x = 0", simp) |
926 apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1]) |
798 apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1]) |
927 apply (auto simp add: hcmod_mult [symmetric]) |
799 apply (auto simp add: hcmod_mult [symmetric]) |
928 done |
800 done |
929 |
801 |
930 lemma hcmod_divide: |
802 lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)" |
931 "hcmod(x/y) = hcmod(x)/(hcmod y)" |
803 by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse) |
932 apply (unfold hcomplex_divide_def hypreal_divide_def) |
|
933 apply (auto simp add: hcmod_mult hcmod_hcomplex_inverse) |
|
934 done |
|
935 |
|
936 lemma hcomplex_inverse_divide: |
|
937 "inverse(x/y) = y/(x::hcomplex)" |
|
938 apply (unfold hcomplex_divide_def) |
|
939 apply (auto simp add: inverse_mult_distrib hcomplex_mult_commute) |
|
940 done |
|
941 declare hcomplex_inverse_divide [simp] |
|
942 |
804 |
943 |
805 |
944 subsection{*Exponentiation*} |
806 subsection{*Exponentiation*} |
945 |
807 |
946 primrec |
808 primrec |
972 apply (auto simp add: hcmod_mult) |
834 apply (auto simp add: hcmod_mult) |
973 done |
835 done |
974 |
836 |
975 lemma hcomplexpow_minus: |
837 lemma hcomplexpow_minus: |
976 "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))" |
838 "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))" |
977 apply (induct_tac "n") |
839 by (induct_tac "n", auto) |
978 apply auto |
|
979 done |
|
980 |
840 |
981 lemma hcpow_minus: |
841 lemma hcpow_minus: |
982 "(-x::hcomplex) hcpow n = |
842 "(-x::hcomplex) hcpow n = |
983 (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))" |
843 (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))" |
984 apply (rule_tac z = "x" in eq_Abs_hcomplex) |
844 apply (rule eq_Abs_hcomplex [of x]) |
985 apply (rule_tac z = "n" in eq_Abs_hypnat) |
845 apply (rule eq_Abs_hypnat [of n]) |
986 apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus) |
846 apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra) |
987 apply ultra |
847 apply (auto simp add: complexpow_minus, ultra) |
988 apply (auto simp add: complexpow_minus) |
|
989 apply ultra |
|
990 done |
848 done |
991 |
849 |
992 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" |
850 lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" |
993 apply (rule_tac z = "r" in eq_Abs_hcomplex) |
851 apply (rule eq_Abs_hcomplex [of r]) |
994 apply (rule_tac z = "s" in eq_Abs_hcomplex) |
852 apply (rule eq_Abs_hcomplex [of s]) |
995 apply (rule_tac z = "n" in eq_Abs_hypnat) |
853 apply (rule eq_Abs_hypnat [of n]) |
996 apply (auto simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib) |
854 apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib) |
997 done |
855 done |
998 |
856 |
999 lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0" |
857 lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0" |
1000 apply (unfold hcomplex_zero_def hypnat_one_def) |
858 apply (simp add: hcomplex_zero_def hypnat_one_def) |
1001 apply (rule_tac z = "n" in eq_Abs_hypnat) |
859 apply (rule eq_Abs_hypnat [of n]) |
1002 apply (auto simp add: hcpow hypnat_add) |
860 apply (simp add: hcpow hypnat_add) |
1003 done |
861 done |
1004 |
862 |
1005 lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0" |
863 lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0" |
1006 apply (unfold hSuc_def) |
864 by (simp add: hSuc_def) |
1007 apply (simp (no_asm)) |
|
1008 done |
|
1009 |
865 |
1010 lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)" |
866 lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)" |
1011 apply (rule_tac z = "r" in eq_Abs_hcomplex) |
867 apply (rule eq_Abs_hcomplex [of r]) |
1012 apply (rule_tac z = "n" in eq_Abs_hypnat) |
868 apply (rule eq_Abs_hypnat [of n]) |
1013 apply (auto simp add: hcpow hcomplex_zero_def) |
869 apply (auto simp add: hcpow hcomplex_zero_def, ultra) |
1014 apply ultra |
|
1015 done |
870 done |
1016 |
871 |
1017 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
872 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
1018 apply (blast intro: ccontr dest: hcpow_not_zero) |
873 by (blast intro: ccontr dest: hcpow_not_zero) |
1019 done |
874 |
1020 |
875 lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" |
1021 lemma hcomplex_i_mult_eq: "iii * iii = - 1" |
876 by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus) |
1022 apply (unfold iii_def) |
877 |
1023 apply (auto simp add: hcomplex_mult hcomplex_one_def hcomplex_minus) |
878 lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1" |
1024 done |
879 by (simp add: numeral_2_eq_2) |
1025 declare hcomplex_i_mult_eq [simp] |
880 |
1026 |
881 lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0" |
1027 lemma hcomplexpow_i_squared: "iii ^ 2 = - 1" |
882 by (simp add: iii_def hcomplex_zero_def) |
1028 apply (simp (no_asm) add: numeral_2_eq_2) |
|
1029 done |
|
1030 declare hcomplexpow_i_squared [simp] |
|
1031 |
|
1032 lemma hcomplex_i_not_zero: "iii \<noteq> 0" |
|
1033 apply (unfold iii_def hcomplex_zero_def) |
|
1034 apply auto |
|
1035 done |
|
1036 declare hcomplex_i_not_zero [simp] |
|
1037 |
883 |
1038 lemma hcomplex_divide: |
884 lemma hcomplex_divide: |
1039 "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
885 "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) = |
1040 Abs_hcomplex(hcomplexrel``{%n. X n / Y n})" |
886 Abs_hcomplex(hcomplexrel``{%n. X n / Y n})" |
1041 apply (unfold hcomplex_divide_def complex_divide_def) |
887 by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult) |
1042 apply (auto simp add: hcomplex_inverse hcomplex_mult) |
888 |
1043 done |
|
1044 |
889 |
1045 |
890 |
1046 subsection{*The Function @{term hsgn}*} |
891 subsection{*The Function @{term hsgn}*} |
1047 |
892 |
1048 lemma hsgn: |
893 lemma hsgn: |
1049 "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
894 "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
1050 Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})" |
895 Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})" |
1051 apply (unfold hsgn_def) |
896 apply (simp add: hsgn_def) |
1052 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
897 apply (rule_tac f = Abs_hcomplex in arg_cong) |
1053 apply (auto, ultra) |
898 apply (auto, ultra) |
1054 done |
899 done |
1055 |
900 |
1056 lemma hsgn_zero: "hsgn 0 = 0" |
901 lemma hsgn_zero [simp]: "hsgn 0 = 0" |
1057 apply (unfold hcomplex_zero_def) |
902 by (simp add: hcomplex_zero_def hsgn) |
1058 apply (simp (no_asm) add: hsgn) |
903 |
1059 done |
904 lemma hsgn_one [simp]: "hsgn 1 = 1" |
1060 declare hsgn_zero [simp] |
905 by (simp add: hcomplex_one_def hsgn) |
1061 |
|
1062 |
|
1063 lemma hsgn_one: "hsgn 1 = 1" |
|
1064 apply (unfold hcomplex_one_def) |
|
1065 apply (simp (no_asm) add: hsgn) |
|
1066 done |
|
1067 declare hsgn_one [simp] |
|
1068 |
906 |
1069 lemma hsgn_minus: "hsgn (-z) = - hsgn(z)" |
907 lemma hsgn_minus: "hsgn (-z) = - hsgn(z)" |
1070 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
908 apply (rule eq_Abs_hcomplex [of z]) |
1071 apply (auto simp add: hsgn hcomplex_minus sgn_minus) |
909 apply (simp add: hsgn hcomplex_minus sgn_minus) |
1072 done |
910 done |
1073 |
911 |
1074 lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)" |
912 lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)" |
1075 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
913 apply (rule eq_Abs_hcomplex [of z]) |
1076 apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq) |
914 apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq) |
1077 done |
915 done |
1078 |
916 |
1079 lemma lemma_hypreal_P_EX2: |
917 lemma lemma_hypreal_P_EX2: |
1080 "(\<exists>(x::hypreal) y. P x y) = |
918 "(\<exists>(x::hypreal) y. P x y) = |
1081 (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))" |
919 (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))" |
1082 apply auto |
920 apply auto |
1083 apply (rule_tac z = "x" in eq_Abs_hypreal) |
921 apply (rule_tac z = x in eq_Abs_hypreal) |
1084 apply (rule_tac z = "y" in eq_Abs_hypreal) |
922 apply (rule_tac z = y in eq_Abs_hypreal, auto) |
1085 apply auto |
|
1086 done |
923 done |
1087 |
924 |
1088 lemma complex_split2: |
925 lemma complex_split2: |
1089 "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)" |
926 "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)" |
1090 apply (blast intro: complex_split) |
927 by (blast intro: complex_split) |
1091 done |
|
1092 |
928 |
1093 (* Interesting proof! *) |
929 (* Interesting proof! *) |
1094 lemma hcomplex_split: |
930 lemma hcomplex_split: |
1095 "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)" |
931 "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)" |
1096 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
932 apply (rule eq_Abs_hcomplex [of z]) |
1097 apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult) |
933 apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult) |
1098 apply (cut_tac z = "x" in complex_split2) |
934 apply (cut_tac z = x in complex_split2) |
1099 apply (drule choice, safe)+ |
935 apply (drule choice, safe)+ |
1100 apply (rule_tac x = "f" in exI) |
936 apply (rule_tac x = f in exI) |
1101 apply (rule_tac x = "fa" in exI) |
937 apply (rule_tac x = fa in exI, auto) |
1102 apply auto |
938 done |
1103 done |
939 |
1104 |
940 lemma hRe_hcomplex_i [simp]: |
1105 lemma hRe_hcomplex_i: |
|
1106 "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x" |
941 "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x" |
1107 apply (rule_tac z = "x" in eq_Abs_hypreal) |
942 apply (rule eq_Abs_hypreal [of x]) |
1108 apply (rule_tac z = "y" in eq_Abs_hypreal) |
943 apply (rule eq_Abs_hypreal [of y]) |
1109 apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) |
944 apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) |
1110 done |
945 done |
1111 declare hRe_hcomplex_i [simp] |
946 |
1112 |
947 lemma hIm_hcomplex_i [simp]: |
1113 lemma hIm_hcomplex_i: |
|
1114 "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y" |
948 "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y" |
1115 apply (rule_tac z = "x" in eq_Abs_hypreal) |
949 apply (rule eq_Abs_hypreal [of x]) |
1116 apply (rule_tac z = "y" in eq_Abs_hypreal) |
950 apply (rule eq_Abs_hypreal [of y]) |
1117 apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) |
951 apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) |
1118 done |
952 done |
1119 declare hIm_hcomplex_i [simp] |
|
1120 |
953 |
1121 lemma hcmod_i: |
954 lemma hcmod_i: |
1122 "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = |
955 "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = |
1123 ( *f* sqrt) (x ^ 2 + y ^ 2)" |
956 ( *f* sqrt) (x ^ 2 + y ^ 2)" |
1124 apply (rule_tac z = "x" in eq_Abs_hypreal) |
957 apply (rule eq_Abs_hypreal [of x]) |
1125 apply (rule_tac z = "y" in eq_Abs_hypreal) |
958 apply (rule eq_Abs_hypreal [of y]) |
1126 apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2) |
959 apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2) |
1127 done |
960 done |
1128 |
961 |
1129 lemma hcomplex_eq_hRe_eq: |
962 lemma hcomplex_eq_hRe_eq: |
1130 "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
963 "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
1131 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb |
964 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb |
1132 ==> xa = xb" |
965 ==> xa = xb" |
1133 apply (unfold iii_def) |
966 apply (simp add: iii_def) |
1134 apply (rule_tac z = "xa" in eq_Abs_hypreal) |
967 apply (rule eq_Abs_hypreal [of xa]) |
1135 apply (rule_tac z = "ya" in eq_Abs_hypreal) |
968 apply (rule eq_Abs_hypreal [of ya]) |
1136 apply (rule_tac z = "xb" in eq_Abs_hypreal) |
969 apply (rule eq_Abs_hypreal [of xb]) |
1137 apply (rule_tac z = "yb" in eq_Abs_hypreal) |
970 apply (rule eq_Abs_hypreal [of yb]) |
1138 apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal) |
971 apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra) |
1139 apply (ultra) |
|
1140 done |
972 done |
1141 |
973 |
1142 lemma hcomplex_eq_hIm_eq: |
974 lemma hcomplex_eq_hIm_eq: |
1143 "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
975 "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
1144 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb |
976 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb |
1145 ==> ya = yb" |
977 ==> ya = yb" |
1146 apply (unfold iii_def) |
978 apply (simp add: iii_def) |
1147 apply (rule_tac z = "xa" in eq_Abs_hypreal) |
979 apply (rule eq_Abs_hypreal [of xa]) |
1148 apply (rule_tac z = "ya" in eq_Abs_hypreal) |
980 apply (rule eq_Abs_hypreal [of ya]) |
1149 apply (rule_tac z = "xb" in eq_Abs_hypreal) |
981 apply (rule eq_Abs_hypreal [of xb]) |
1150 apply (rule_tac z = "yb" in eq_Abs_hypreal) |
982 apply (rule eq_Abs_hypreal [of yb]) |
1151 apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal) |
983 apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra) |
1152 apply (ultra) |
984 done |
1153 done |
985 |
1154 |
986 lemma hcomplex_eq_cancel_iff [simp]: |
1155 lemma hcomplex_eq_cancel_iff: |
|
1156 "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
987 "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
1157 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = |
988 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = |
1158 ((xa = xb) & (ya = yb))" |
989 ((xa = xb) & (ya = yb))" |
1159 apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq) |
990 by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq) |
1160 done |
991 |
1161 declare hcomplex_eq_cancel_iff [simp] |
992 lemma hcomplex_eq_cancel_iffA [iff]: |
1162 |
|
1163 lemma hcomplex_eq_cancel_iffA: |
|
1164 "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = |
993 "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = |
1165 hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))" |
994 hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))" |
1166 apply (auto simp add: hcomplex_mult_commute) |
995 apply (simp add: hcomplex_mult_commute) |
1167 done |
996 done |
1168 declare hcomplex_eq_cancel_iffA [iff] |
997 |
1169 |
998 lemma hcomplex_eq_cancel_iffB [iff]: |
1170 lemma hcomplex_eq_cancel_iffB: |
|
1171 "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = |
999 "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = |
1172 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))" |
1000 hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))" |
1173 apply (auto simp add: hcomplex_mult_commute) |
1001 apply (simp add: hcomplex_mult_commute) |
1174 done |
1002 done |
1175 declare hcomplex_eq_cancel_iffB [iff] |
1003 |
1176 |
1004 lemma hcomplex_eq_cancel_iffC [iff]: |
1177 lemma hcomplex_eq_cancel_iffC: |
|
1178 "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
1005 "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = |
1179 hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))" |
1006 hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))" |
1180 apply (auto simp add: hcomplex_mult_commute) |
1007 apply (simp add: hcomplex_mult_commute) |
1181 done |
1008 done |
1182 declare hcomplex_eq_cancel_iffC [iff] |
1009 |
1183 |
1010 lemma hcomplex_eq_cancel_iff2 [simp]: |
1184 lemma hcomplex_eq_cancel_iff2: |
|
1185 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = |
1011 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = |
1186 hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
1012 hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
1187 apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff) |
1013 apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff) |
1188 apply (simp del: hcomplex_eq_cancel_iff) |
1014 apply (simp del: hcomplex_eq_cancel_iff) |
1189 done |
1015 done |
1190 declare hcomplex_eq_cancel_iff2 [simp] |
1016 |
1191 |
1017 lemma hcomplex_eq_cancel_iff2a [simp]: |
1192 lemma hcomplex_eq_cancel_iff2a: |
|
1193 "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = |
1018 "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = |
1194 hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
1019 hcomplex_of_hypreal xa) = (x = xa & y = 0)" |
1195 apply (auto simp add: hcomplex_mult_commute) |
1020 apply (simp add: hcomplex_mult_commute) |
1196 done |
1021 done |
1197 declare hcomplex_eq_cancel_iff2a [simp] |
1022 |
1198 |
1023 lemma hcomplex_eq_cancel_iff3 [simp]: |
1199 lemma hcomplex_eq_cancel_iff3: |
|
1200 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = |
1024 "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = |
1201 iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" |
1025 iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" |
1202 apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff) |
1026 apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff) |
1203 apply (simp del: hcomplex_eq_cancel_iff) |
1027 apply (simp del: hcomplex_eq_cancel_iff) |
1204 done |
1028 done |
1205 declare hcomplex_eq_cancel_iff3 [simp] |
1029 |
1206 |
1030 lemma hcomplex_eq_cancel_iff3a [simp]: |
1207 lemma hcomplex_eq_cancel_iff3a: |
|
1208 "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = |
1031 "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = |
1209 iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" |
1032 iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" |
1210 apply (auto simp add: hcomplex_mult_commute) |
1033 apply (simp add: hcomplex_mult_commute) |
1211 done |
1034 done |
1212 declare hcomplex_eq_cancel_iff3a [simp] |
|
1213 |
1035 |
1214 lemma hcomplex_split_hRe_zero: |
1036 lemma hcomplex_split_hRe_zero: |
1215 "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 |
1037 "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 |
1216 ==> x = 0" |
1038 ==> x = 0" |
1217 apply (unfold iii_def) |
1039 apply (simp add: iii_def) |
1218 apply (rule_tac z = "x" in eq_Abs_hypreal) |
1040 apply (rule eq_Abs_hypreal [of x]) |
1219 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1041 apply (rule eq_Abs_hypreal [of y]) |
1220 apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num) |
1042 apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra) |
1221 apply ultra |
1043 apply (simp add: complex_split_Re_zero) |
1222 apply (auto simp add: complex_split_Re_zero) |
|
1223 done |
1044 done |
1224 |
1045 |
1225 lemma hcomplex_split_hIm_zero: |
1046 lemma hcomplex_split_hIm_zero: |
1226 "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 |
1047 "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 |
1227 ==> y = 0" |
1048 ==> y = 0" |
1228 apply (unfold iii_def) |
1049 apply (simp add: iii_def) |
1229 apply (rule_tac z = "x" in eq_Abs_hypreal) |
1050 apply (rule eq_Abs_hypreal [of x]) |
1230 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1051 apply (rule eq_Abs_hypreal [of y]) |
1231 apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num) |
1052 apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra) |
1232 apply ultra |
1053 apply (simp add: complex_split_Im_zero) |
1233 apply (auto simp add: complex_split_Im_zero) |
1054 done |
1234 done |
1055 |
1235 |
1056 lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z" |
1236 lemma hRe_hsgn: "hRe(hsgn z) = hRe(z)/hcmod z" |
1057 apply (rule eq_Abs_hcomplex [of z]) |
1237 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
1058 apply (simp add: hsgn hcmod hRe hypreal_divide) |
1238 apply (auto simp add: hsgn hcmod hRe hypreal_divide) |
1059 done |
1239 done |
1060 |
1240 declare hRe_hsgn [simp] |
1061 lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z" |
1241 |
1062 apply (rule eq_Abs_hcomplex [of z]) |
1242 lemma hIm_hsgn: "hIm(hsgn z) = hIm(z)/hcmod z" |
1063 apply (simp add: hsgn hcmod hIm hypreal_divide) |
1243 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
1064 done |
1244 apply (auto simp add: hsgn hcmod hIm hypreal_divide) |
1065 |
1245 done |
1066 lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" |
1246 declare hIm_hsgn [simp] |
|
1247 |
|
1248 lemma real_two_squares_add_zero_iff: |
|
1249 "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" |
|
1250 apply (auto intro: real_sum_squares_cancel) |
1067 apply (auto intro: real_sum_squares_cancel) |
1251 done |
1068 done |
1252 declare real_two_squares_add_zero_iff [simp] |
|
1253 |
1069 |
1254 lemma hcomplex_inverse_complex_split: |
1070 lemma hcomplex_inverse_complex_split: |
1255 "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = |
1071 "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = |
1256 hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - |
1072 hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - |
1257 iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" |
1073 iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" |
1258 apply (rule_tac z = "x" in eq_Abs_hypreal) |
1074 apply (rule eq_Abs_hypreal [of x]) |
1259 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1075 apply (rule eq_Abs_hypreal [of y]) |
1260 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2) |
1076 apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2) |
1261 done |
1077 done |
1262 |
1078 |
1263 lemma hRe_mult_i_eq: |
1079 lemma hRe_mult_i_eq[simp]: |
1264 "hRe (iii * hcomplex_of_hypreal y) = 0" |
1080 "hRe (iii * hcomplex_of_hypreal y) = 0" |
1265 apply (unfold iii_def) |
1081 apply (simp add: iii_def) |
1266 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1082 apply (rule eq_Abs_hypreal [of y]) |
1267 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num) |
1083 apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num) |
1268 done |
1084 done |
1269 declare hRe_mult_i_eq [simp] |
1085 |
1270 |
1086 lemma hIm_mult_i_eq [simp]: |
1271 lemma hIm_mult_i_eq: |
|
1272 "hIm (iii * hcomplex_of_hypreal y) = y" |
1087 "hIm (iii * hcomplex_of_hypreal y) = y" |
1273 apply (unfold iii_def) |
1088 apply (simp add: iii_def) |
1274 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1089 apply (rule eq_Abs_hypreal [of y]) |
1275 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num) |
1090 apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num) |
1276 done |
1091 done |
1277 declare hIm_mult_i_eq [simp] |
1092 |
1278 |
1093 lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y" |
1279 lemma hcmod_mult_i: "hcmod (iii * hcomplex_of_hypreal y) = abs y" |
1094 apply (rule eq_Abs_hypreal [of y]) |
1280 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1095 apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult) |
1281 apply (auto simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult) |
1096 done |
1282 done |
1097 |
1283 declare hcmod_mult_i [simp] |
1098 lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y" |
1284 |
1099 by (simp add: hcomplex_mult_commute) |
1285 lemma hcmod_mult_i2: "hcmod (hcomplex_of_hypreal y * iii) = abs y" |
|
1286 apply (auto simp add: hcomplex_mult_commute) |
|
1287 done |
|
1288 declare hcmod_mult_i2 [simp] |
|
1289 |
1100 |
1290 (*---------------------------------------------------------------------------*) |
1101 (*---------------------------------------------------------------------------*) |
1291 (* harg *) |
1102 (* harg *) |
1292 (*---------------------------------------------------------------------------*) |
1103 (*---------------------------------------------------------------------------*) |
1293 |
1104 |
1294 lemma harg: |
1105 lemma harg: |
1295 "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
1106 "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) = |
1296 Abs_hypreal(hyprel `` {%n. arg (X n)})" |
1107 Abs_hypreal(hyprel `` {%n. arg (X n)})" |
1297 |
1108 |
1298 apply (unfold harg_def) |
1109 apply (simp add: harg_def) |
1299 apply (rule_tac f = "Abs_hypreal" in arg_cong) |
1110 apply (rule_tac f = Abs_hypreal in arg_cong) |
1300 apply (auto, ultra) |
1111 apply (auto, ultra) |
1301 done |
1112 done |
1302 |
1113 |
1303 lemma cos_harg_i_mult_zero_pos: |
1114 lemma cos_harg_i_mult_zero_pos: |
1304 "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" |
1115 "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" |
1305 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1116 apply (rule eq_Abs_hypreal [of y]) |
1306 apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult |
1117 apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult |
1307 hypreal_zero_num hypreal_less starfun harg) |
1118 hypreal_zero_num hypreal_less starfun harg, ultra) |
1308 apply (ultra) |
|
1309 done |
1119 done |
1310 |
1120 |
1311 lemma cos_harg_i_mult_zero_neg: |
1121 lemma cos_harg_i_mult_zero_neg: |
1312 "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" |
1122 "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" |
1313 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1123 apply (rule eq_Abs_hypreal [of y]) |
1314 apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult |
1124 apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult |
1315 hypreal_zero_num hypreal_less starfun harg) |
1125 hypreal_zero_num hypreal_less starfun harg, ultra) |
1316 apply (ultra) |
|
1317 done |
1126 done |
1318 |
1127 |
1319 lemma cos_harg_i_mult_zero [simp]: |
1128 lemma cos_harg_i_mult_zero [simp]: |
1320 "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" |
1129 "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" |
1321 apply (cut_tac x = "y" and y = "0" in linorder_less_linear) |
1130 apply (cut_tac x = y and y = 0 in linorder_less_linear) |
1322 apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg) |
1131 apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg) |
1323 done |
1132 done |
1324 |
1133 |
1325 lemma hcomplex_of_hypreal_zero_iff [simp]: |
1134 lemma hcomplex_of_hypreal_zero_iff [simp]: |
1326 "(hcomplex_of_hypreal y = 0) = (y = 0)" |
1135 "(hcomplex_of_hypreal y = 0) = (y = 0)" |
1327 apply (rule_tac z = "y" in eq_Abs_hypreal) |
1136 apply (rule eq_Abs_hypreal [of y]) |
1328 apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def) |
1137 apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def) |
1329 done |
1138 done |
1330 |
1139 |
1331 |
1140 |
1332 subsection{*Polar Form for Nonstandard Complex Numbers*} |
1141 subsection{*Polar Form for Nonstandard Complex Numbers*} |
1333 |
1142 |
1338 done |
1147 done |
1339 |
1148 |
1340 lemma hcomplex_split_polar: |
1149 lemma hcomplex_split_polar: |
1341 "\<exists>r a. z = hcomplex_of_hypreal r * |
1150 "\<exists>r a. z = hcomplex_of_hypreal r * |
1342 (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" |
1151 (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" |
1343 apply (rule_tac z = "z" in eq_Abs_hcomplex) |
1152 apply (rule eq_Abs_hcomplex [of z]) |
1344 apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult) |
1153 apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult) |
1345 apply (cut_tac z = "x" in complex_split_polar2) |
1154 apply (cut_tac z = x in complex_split_polar2) |
1346 apply (drule choice, safe)+ |
1155 apply (drule choice, safe)+ |
1347 apply (rule_tac x = "f" in exI) |
1156 apply (rule_tac x = f in exI) |
1348 apply (rule_tac x = "fa" in exI) |
1157 apply (rule_tac x = fa in exI, auto) |
1349 apply auto |
|
1350 done |
1158 done |
1351 |
1159 |
1352 lemma hcis: |
1160 lemma hcis: |
1353 "hcis (Abs_hypreal(hyprel `` {%n. X n})) = |
1161 "hcis (Abs_hypreal(hyprel `` {%n. X n})) = |
1354 Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})" |
1162 Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})" |
1355 apply (unfold hcis_def) |
1163 apply (simp add: hcis_def) |
1356 apply (rule_tac f = "Abs_hcomplex" in arg_cong) |
1164 apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra) |
1357 apply auto |
|
1358 apply (ultra) |
|
1359 done |
1165 done |
1360 |
1166 |
1361 lemma hcis_eq: |
1167 lemma hcis_eq: |
1362 "hcis a = |
1168 "hcis a = |
1363 (hcomplex_of_hypreal(( *f* cos) a) + |
1169 (hcomplex_of_hypreal(( *f* cos) a) + |
1364 iii * hcomplex_of_hypreal(( *f* sin) a))" |
1170 iii * hcomplex_of_hypreal(( *f* sin) a))" |
1365 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1171 apply (rule eq_Abs_hypreal [of a]) |
1366 apply (auto simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def) |
1172 apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def) |
1367 done |
1173 done |
1368 |
1174 |
1369 lemma hrcis: |
1175 lemma hrcis: |
1370 "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) = |
1176 "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) = |
1371 Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})" |
1177 Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})" |
1372 apply (unfold hrcis_def) |
1178 by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def) |
1373 apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def) |
|
1374 done |
|
1375 |
1179 |
1376 lemma hrcis_Ex: "\<exists>r a. z = hrcis r a" |
1180 lemma hrcis_Ex: "\<exists>r a. z = hrcis r a" |
1377 apply (simp (no_asm) add: hrcis_def hcis_eq) |
1181 apply (simp add: hrcis_def hcis_eq) |
1378 apply (rule hcomplex_split_polar) |
1182 apply (rule hcomplex_split_polar) |
1379 done |
1183 done |
1380 |
1184 |
1381 lemma hRe_hcomplex_polar: |
1185 lemma hRe_hcomplex_polar [simp]: |
1382 "hRe(hcomplex_of_hypreal r * |
1186 "hRe(hcomplex_of_hypreal r * |
1383 (hcomplex_of_hypreal(( *f* cos) a) + |
1187 (hcomplex_of_hypreal(( *f* cos) a) + |
1384 iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a" |
1188 iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a" |
1385 apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) |
1189 by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) |
1386 done |
1190 |
1387 declare hRe_hcomplex_polar [simp] |
1191 lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a" |
1388 |
1192 by (simp add: hrcis_def hcis_eq) |
1389 lemma hRe_hrcis: "hRe(hrcis r a) = r * ( *f* cos) a" |
1193 |
1390 apply (unfold hrcis_def) |
1194 lemma hIm_hcomplex_polar [simp]: |
1391 apply (auto simp add: hcis_eq) |
|
1392 done |
|
1393 declare hRe_hrcis [simp] |
|
1394 |
|
1395 lemma hIm_hcomplex_polar: |
|
1396 "hIm(hcomplex_of_hypreal r * |
1195 "hIm(hcomplex_of_hypreal r * |
1397 (hcomplex_of_hypreal(( *f* cos) a) + |
1196 (hcomplex_of_hypreal(( *f* cos) a) + |
1398 iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a" |
1197 iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a" |
1399 apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) |
1198 by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) |
1400 done |
1199 |
1401 declare hIm_hcomplex_polar [simp] |
1200 lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a" |
1402 |
1201 by (simp add: hrcis_def hcis_eq) |
1403 lemma hIm_hrcis: "hIm(hrcis r a) = r * ( *f* sin) a" |
1202 |
1404 apply (unfold hrcis_def) |
1203 lemma hcmod_complex_polar [simp]: |
1405 apply (auto simp add: hcis_eq) |
|
1406 done |
|
1407 declare hIm_hrcis [simp] |
|
1408 |
|
1409 lemma hcmod_complex_polar: |
|
1410 "hcmod (hcomplex_of_hypreal r * |
1204 "hcmod (hcomplex_of_hypreal r * |
1411 (hcomplex_of_hypreal(( *f* cos) a) + |
1205 (hcomplex_of_hypreal(( *f* cos) a) + |
1412 iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r" |
1206 iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r" |
1413 apply (rule_tac z = "r" in eq_Abs_hypreal) |
1207 apply (rule eq_Abs_hypreal [of r]) |
1414 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1208 apply (rule eq_Abs_hypreal [of a]) |
1415 apply (auto simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs) |
1209 apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs) |
1416 done |
1210 done |
1417 declare hcmod_complex_polar [simp] |
1211 |
1418 |
1212 lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r" |
1419 lemma hcmod_hrcis: "hcmod(hrcis r a) = abs r" |
1213 by (simp add: hrcis_def hcis_eq) |
1420 apply (unfold hrcis_def) |
|
1421 apply (auto simp add: hcis_eq) |
|
1422 done |
|
1423 declare hcmod_hrcis [simp] |
|
1424 |
1214 |
1425 (*---------------------------------------------------------------------------*) |
1215 (*---------------------------------------------------------------------------*) |
1426 (* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
1216 (* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) |
1427 (*---------------------------------------------------------------------------*) |
1217 (*---------------------------------------------------------------------------*) |
1428 |
1218 |
1429 lemma hcis_hrcis_eq: "hcis a = hrcis 1 a" |
1219 lemma hcis_hrcis_eq: "hcis a = hrcis 1 a" |
1430 apply (unfold hrcis_def) |
1220 by (simp add: hrcis_def) |
1431 apply (simp (no_asm)) |
|
1432 done |
|
1433 declare hcis_hrcis_eq [symmetric, simp] |
1221 declare hcis_hrcis_eq [symmetric, simp] |
1434 |
1222 |
1435 lemma hrcis_mult: |
1223 lemma hrcis_mult: |
1436 "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
1224 "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" |
1437 apply (unfold hrcis_def) |
1225 apply (simp add: hrcis_def) |
1438 apply (rule_tac z = "r1" in eq_Abs_hypreal) |
1226 apply (rule eq_Abs_hypreal [of r1]) |
1439 apply (rule_tac z = "r2" in eq_Abs_hypreal) |
1227 apply (rule eq_Abs_hypreal [of r2]) |
1440 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1228 apply (rule eq_Abs_hypreal [of a]) |
1441 apply (rule_tac z = "b" in eq_Abs_hypreal) |
1229 apply (rule eq_Abs_hypreal [of b]) |
1442 apply (auto simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal |
1230 apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal |
1443 hcomplex_mult cis_mult [symmetric] |
1231 hcomplex_mult cis_mult [symmetric] |
1444 complex_of_real_mult [symmetric]) |
1232 complex_of_real_mult [symmetric]) |
1445 done |
1233 done |
1446 |
1234 |
1447 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)" |
1235 lemma hcis_mult: "hcis a * hcis b = hcis (a + b)" |
1448 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1236 apply (rule eq_Abs_hypreal [of a]) |
1449 apply (rule_tac z = "b" in eq_Abs_hypreal) |
1237 apply (rule eq_Abs_hypreal [of b]) |
1450 apply (auto simp add: hcis hcomplex_mult hypreal_add cis_mult) |
1238 apply (simp add: hcis hcomplex_mult hypreal_add cis_mult) |
1451 done |
1239 done |
1452 |
1240 |
1453 lemma hcis_zero: |
1241 lemma hcis_zero [simp]: "hcis 0 = 1" |
1454 "hcis 0 = 1" |
1242 by (simp add: hcomplex_one_def hcis hypreal_zero_num) |
1455 apply (unfold hcomplex_one_def) |
1243 |
1456 apply (auto simp add: hcis hypreal_zero_num) |
1244 lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0" |
1457 done |
1245 apply (simp add: hcomplex_zero_def) |
1458 declare hcis_zero [simp] |
1246 apply (rule eq_Abs_hypreal [of a]) |
1459 |
1247 apply (simp add: hrcis hypreal_zero_num) |
1460 lemma hrcis_zero_mod: |
1248 done |
1461 "hrcis 0 a = 0" |
1249 |
1462 apply (unfold hcomplex_zero_def) |
1250 lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r" |
1463 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1251 apply (rule eq_Abs_hypreal [of r]) |
1464 apply (auto simp add: hrcis hypreal_zero_num) |
1252 apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal) |
1465 done |
1253 done |
1466 declare hrcis_zero_mod [simp] |
1254 |
1467 |
1255 lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x" |
1468 lemma hrcis_zero_arg: "hrcis r 0 = hcomplex_of_hypreal r" |
1256 by (simp add: hcomplex_mult_assoc [symmetric]) |
1469 apply (rule_tac z = "r" in eq_Abs_hypreal) |
1257 |
1470 apply (auto simp add: hrcis hypreal_zero_num hcomplex_of_hypreal) |
1258 lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" |
1471 done |
1259 by simp |
1472 declare hrcis_zero_arg [simp] |
|
1473 |
|
1474 lemma hcomplex_i_mult_minus: "iii * (iii * x) = - x" |
|
1475 apply (simp (no_asm) add: hcomplex_mult_assoc [symmetric]) |
|
1476 done |
|
1477 declare hcomplex_i_mult_minus [simp] |
|
1478 |
|
1479 lemma hcomplex_i_mult_minus2: "iii * iii * x = - x" |
|
1480 apply (simp (no_asm)) |
|
1481 done |
|
1482 declare hcomplex_i_mult_minus2 [simp] |
|
1483 |
1260 |
1484 lemma hcis_hypreal_of_nat_Suc_mult: |
1261 lemma hcis_hypreal_of_nat_Suc_mult: |
1485 "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)" |
1262 "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)" |
1486 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1263 apply (rule eq_Abs_hypreal [of a]) |
1487 apply (auto simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) |
1264 apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) |
1488 done |
1265 done |
1489 |
1266 |
1490 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
1267 lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)" |
1491 apply (induct_tac "n") |
1268 apply (induct_tac "n") |
1492 apply (auto simp add: hcis_hypreal_of_nat_Suc_mult) |
1269 apply (simp_all add: hcis_hypreal_of_nat_Suc_mult) |
1493 done |
1270 done |
1494 |
1271 |
1495 lemma hcis_hypreal_of_hypnat_Suc_mult: |
1272 lemma hcis_hypreal_of_hypnat_Suc_mult: |
1496 "hcis (hypreal_of_hypnat (n + 1) * a) = |
1273 "hcis (hypreal_of_hypnat (n + 1) * a) = |
1497 hcis a * hcis (hypreal_of_hypnat n * a)" |
1274 hcis a * hcis (hypreal_of_hypnat n * a)" |
1498 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1275 apply (rule eq_Abs_hypreal [of a]) |
1499 apply (rule_tac z = "n" in eq_Abs_hypnat) |
1276 apply (rule eq_Abs_hypnat [of n]) |
1500 apply (auto simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) |
1277 apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) |
1501 done |
1278 done |
1502 |
1279 |
1503 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
1280 lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" |
1504 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1281 apply (rule eq_Abs_hypreal [of a]) |
1505 apply (rule_tac z = "n" in eq_Abs_hypnat) |
1282 apply (rule eq_Abs_hypnat [of n]) |
1506 apply (auto simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre) |
1283 apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre) |
1507 done |
1284 done |
1508 |
1285 |
1509 lemma DeMoivre2: |
1286 lemma DeMoivre2: |
1510 "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
1287 "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" |
1511 apply (unfold hrcis_def) |
1288 apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow) |
1512 apply (auto simp add: power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow) |
|
1513 done |
1289 done |
1514 |
1290 |
1515 lemma DeMoivre2_ext: |
1291 lemma DeMoivre2_ext: |
1516 "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
1292 "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" |
1517 apply (unfold hrcis_def) |
1293 apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow) |
1518 apply (auto simp add: hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow) |
1294 done |
1519 done |
1295 |
1520 |
1296 lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)" |
1521 lemma hcis_inverse: "inverse(hcis a) = hcis (-a)" |
1297 apply (rule eq_Abs_hypreal [of a]) |
1522 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1298 apply (simp add: hcomplex_inverse hcis hypreal_minus) |
1523 apply (auto simp add: hcomplex_inverse hcis hypreal_minus) |
1299 done |
1524 done |
|
1525 declare hcis_inverse [simp] |
|
1526 |
1300 |
1527 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)" |
1301 lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)" |
1528 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1302 apply (rule eq_Abs_hypreal [of a]) |
1529 apply (rule_tac z = "r" in eq_Abs_hypreal) |
1303 apply (rule eq_Abs_hypreal [of r]) |
1530 apply (auto simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse) |
1304 apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra) |
1531 apply (ultra) |
1305 apply (simp add: real_divide_def) |
1532 apply (unfold real_divide_def) |
1306 done |
1533 apply (auto simp add: INVERSE_ZERO) |
1307 |
1534 done |
1308 lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a" |
1535 |
1309 apply (rule eq_Abs_hypreal [of a]) |
1536 lemma hRe_hcis: "hRe(hcis a) = ( *f* cos) a" |
1310 apply (simp add: hcis starfun hRe) |
1537 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1311 done |
1538 apply (auto simp add: hcis starfun hRe) |
1312 |
1539 done |
1313 lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a" |
1540 declare hRe_hcis [simp] |
1314 apply (rule eq_Abs_hypreal [of a]) |
1541 |
1315 apply (simp add: hcis starfun hIm) |
1542 lemma hIm_hcis: "hIm(hcis a) = ( *f* sin) a" |
1316 done |
1543 apply (rule_tac z = "a" in eq_Abs_hypreal) |
1317 |
1544 apply (auto simp add: hcis starfun hIm) |
1318 lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
1545 done |
1319 apply (simp add: NSDeMoivre) |
1546 declare hIm_hcis [simp] |
1320 done |
1547 |
1321 |
1548 lemma cos_n_hRe_hcis_pow_n: |
1322 lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
1549 "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" |
1323 apply (simp add: NSDeMoivre) |
1550 apply (auto simp add: NSDeMoivre) |
1324 done |
1551 done |
1325 |
1552 |
1326 lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" |
1553 lemma sin_n_hIm_hcis_pow_n: |
1327 apply (simp add: NSDeMoivre_ext) |
1554 "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" |
1328 done |
1555 apply (auto simp add: NSDeMoivre) |
1329 |
1556 done |
1330 lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
1557 |
1331 apply (simp add: NSDeMoivre_ext) |
1558 lemma cos_n_hRe_hcis_hcpow_n: |
|
1559 "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" |
|
1560 apply (auto simp add: NSDeMoivre_ext) |
|
1561 done |
|
1562 |
|
1563 lemma sin_n_hIm_hcis_hcpow_n: |
|
1564 "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" |
|
1565 apply (auto simp add: NSDeMoivre_ext) |
|
1566 done |
1332 done |
1567 |
1333 |
1568 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)" |
1334 lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)" |
1569 apply (unfold hexpi_def) |
1335 apply (simp add: hexpi_def) |
1570 apply (rule_tac z = "a" in eq_Abs_hcomplex) |
1336 apply (rule eq_Abs_hcomplex [of a]) |
1571 apply (rule_tac z = "b" in eq_Abs_hcomplex) |
1337 apply (rule eq_Abs_hcomplex [of b]) |
1572 apply (auto simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult) |
1338 apply (simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult) |
1573 done |
1339 done |
1574 |
1340 |
1575 |
1341 |
1576 subsection{*@{term hcomplex_of_complex}: the Injection from |
1342 subsection{*@{term hcomplex_of_complex}: the Injection from |
1577 type @{typ complex} to to @{typ hcomplex}*} |
1343 type @{typ complex} to to @{typ hcomplex}*} |
1578 |
1344 |
1579 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" |
1345 lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" |
1580 apply (rule inj_onI , rule ccontr) |
1346 apply (rule inj_onI, rule ccontr) |
1581 apply (auto simp add: hcomplex_of_complex_def) |
1347 apply (simp add: hcomplex_of_complex_def) |
1582 done |
1348 done |
1583 |
1349 |
1584 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
1350 lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" |
1585 apply (unfold iii_def hcomplex_of_complex_def) |
1351 by (simp add: iii_def hcomplex_of_complex_def) |
1586 apply (simp (no_asm)) |
1352 |
1587 done |
1353 lemma hcomplex_of_complex_add [simp]: |
1588 |
|
1589 lemma hcomplex_of_complex_add: |
|
1590 "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2" |
1354 "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2" |
1591 apply (unfold hcomplex_of_complex_def) |
1355 by (simp add: hcomplex_of_complex_def hcomplex_add) |
1592 apply (simp (no_asm) add: hcomplex_add) |
1356 |
1593 done |
1357 lemma hcomplex_of_complex_mult [simp]: |
1594 declare hcomplex_of_complex_add [simp] |
|
1595 |
|
1596 lemma hcomplex_of_complex_mult: |
|
1597 "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2" |
1358 "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2" |
1598 apply (unfold hcomplex_of_complex_def) |
1359 by (simp add: hcomplex_of_complex_def hcomplex_mult) |
1599 apply (simp (no_asm) add: hcomplex_mult) |
1360 |
1600 done |
1361 lemma hcomplex_of_complex_eq_iff [simp]: |
1601 declare hcomplex_of_complex_mult [simp] |
1362 "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)" |
1602 |
1363 by (simp add: hcomplex_of_complex_def) |
1603 lemma hcomplex_of_complex_eq_iff: |
1364 |
1604 "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)" |
1365 |
1605 apply (unfold hcomplex_of_complex_def) |
1366 lemma hcomplex_of_complex_minus [simp]: |
1606 apply auto |
|
1607 done |
|
1608 declare hcomplex_of_complex_eq_iff [simp] |
|
1609 |
|
1610 lemma hcomplex_of_complex_minus: |
|
1611 "hcomplex_of_complex (-r) = - hcomplex_of_complex r" |
1367 "hcomplex_of_complex (-r) = - hcomplex_of_complex r" |
1612 apply (unfold hcomplex_of_complex_def) |
1368 by (simp add: hcomplex_of_complex_def hcomplex_minus) |
1613 apply (auto simp add: hcomplex_minus) |
1369 |
1614 done |
1370 lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1" |
1615 declare hcomplex_of_complex_minus [simp] |
1371 by (simp add: hcomplex_of_complex_def hcomplex_one_def) |
1616 |
1372 |
1617 lemma hcomplex_of_complex_one [simp]: |
1373 lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0" |
1618 "hcomplex_of_complex 1 = 1" |
1374 by (simp add: hcomplex_of_complex_def hcomplex_zero_def) |
1619 apply (unfold hcomplex_of_complex_def hcomplex_one_def) |
|
1620 apply auto |
|
1621 done |
|
1622 |
|
1623 lemma hcomplex_of_complex_zero [simp]: |
|
1624 "hcomplex_of_complex 0 = 0" |
|
1625 apply (unfold hcomplex_of_complex_def hcomplex_zero_def) |
|
1626 apply (simp (no_asm)) |
|
1627 done |
|
1628 |
1375 |
1629 lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)" |
1376 lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)" |
1630 apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def) |
1377 by (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def) |
1631 done |
1378 |
1632 |
1379 lemma hcomplex_of_complex_inverse [simp]: |
1633 lemma hcomplex_of_complex_inverse: |
|
1634 "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" |
1380 "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" |
1635 apply (case_tac "r=0") |
1381 apply (case_tac "r=0") |
1636 apply (simp add: hcomplex_of_complex_zero) |
1382 apply (simp add: hcomplex_of_complex_zero) |
1637 apply (rule_tac c1 = "hcomplex_of_complex r" |
1383 apply (rule_tac c1 = "hcomplex_of_complex r" |
1638 in hcomplex_mult_left_cancel [THEN iffD1]) |
1384 in hcomplex_mult_left_cancel [THEN iffD1]) |
1639 apply (force simp add: hcomplex_of_complex_zero_iff) |
1385 apply (force simp add: hcomplex_of_complex_zero_iff) |
1640 apply (subst hcomplex_of_complex_mult [symmetric]) |
1386 apply (subst hcomplex_of_complex_mult [symmetric]) |
1641 apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff) |
1387 apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff) |
1642 done |
1388 done |
1643 declare hcomplex_of_complex_inverse [simp] |
1389 |
1644 |
1390 lemma hcomplex_of_complex_divide [simp]: |
1645 lemma hcomplex_of_complex_divide: |
|
1646 "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2" |
1391 "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2" |
1647 apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def) |
1392 by (simp add: hcomplex_divide_def complex_divide_def) |
1648 done |
|
1649 declare hcomplex_of_complex_divide [simp] |
|
1650 |
1393 |
1651 lemma hRe_hcomplex_of_complex: |
1394 lemma hRe_hcomplex_of_complex: |
1652 "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
1395 "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" |
1653 apply (unfold hcomplex_of_complex_def hypreal_of_real_def) |
1396 by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe) |
1654 apply (auto simp add: hRe) |
|
1655 done |
|
1656 |
1397 |
1657 lemma hIm_hcomplex_of_complex: |
1398 lemma hIm_hcomplex_of_complex: |
1658 "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
1399 "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" |
1659 apply (unfold hcomplex_of_complex_def hypreal_of_real_def) |
1400 by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm) |
1660 apply (auto simp add: hIm) |
|
1661 done |
|
1662 |
1401 |
1663 lemma hcmod_hcomplex_of_complex: |
1402 lemma hcmod_hcomplex_of_complex: |
1664 "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
1403 "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" |
1665 apply (unfold hypreal_of_real_def hcomplex_of_complex_def) |
1404 by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod) |
1666 apply (auto simp add: hcmod) |
|
1667 done |
|
1668 |
1405 |
1669 ML |
1406 ML |
1670 {* |
1407 {* |
1671 val hcomplex_zero_def = thm"hcomplex_zero_def"; |
1408 val hcomplex_zero_def = thm"hcomplex_zero_def"; |
1672 val hcomplex_one_def = thm"hcomplex_one_def"; |
1409 val hcomplex_one_def = thm"hcomplex_one_def"; |