86 |
86 |
87 lemmas hcomplex_defs [transfer_unfold] = |
87 lemmas hcomplex_defs [transfer_unfold] = |
88 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
88 hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def |
89 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
89 hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def hcpow_def |
90 |
90 |
|
91 lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard" |
|
92 by (simp add: hcomplex_defs) |
|
93 |
|
94 lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard" |
|
95 by (simp add: hcomplex_defs) |
|
96 |
|
97 lemma Standard_iii [simp]: "iii \<in> Standard" |
|
98 by (simp add: hcomplex_defs) |
|
99 |
|
100 lemma Standard_hcnj [simp]: "x \<in> Standard \<Longrightarrow> hcnj x \<in> Standard" |
|
101 by (simp add: hcomplex_defs) |
|
102 |
|
103 lemma Standard_hsgn [simp]: "x \<in> Standard \<Longrightarrow> hsgn x \<in> Standard" |
|
104 by (simp add: hcomplex_defs) |
|
105 |
|
106 lemma Standard_harg [simp]: "x \<in> Standard \<Longrightarrow> harg x \<in> Standard" |
|
107 by (simp add: hcomplex_defs) |
|
108 |
|
109 lemma Standard_hcis [simp]: "r \<in> Standard \<Longrightarrow> hcis r \<in> Standard" |
|
110 by (simp add: hcomplex_defs) |
|
111 |
|
112 lemma Standard_hexpi [simp]: "x \<in> Standard \<Longrightarrow> hexpi x \<in> Standard" |
|
113 by (simp add: hcomplex_defs) |
|
114 |
|
115 lemma Standard_hrcis [simp]: |
|
116 "\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> hrcis r s \<in> Standard" |
|
117 by (simp add: hcomplex_defs) |
|
118 |
|
119 lemma Standard_HComplex [simp]: |
|
120 "\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> HComplex r s \<in> Standard" |
|
121 by (simp add: hcomplex_defs) |
|
122 |
|
123 lemma Standard_hcomplex_of_hypreal [simp]: |
|
124 "r \<in> Standard \<Longrightarrow> hcomplex_of_hypreal r \<in> Standard" |
|
125 by (simp add: hcomplex_defs) |
|
126 |
91 lemma hcmod_def: "hcmod = *f* cmod" |
127 lemma hcmod_def: "hcmod = *f* cmod" |
92 by (rule hnorm_def) |
128 by (rule hnorm_def) |
93 |
129 |
94 |
130 |
95 subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
131 subsection{*Properties of Nonstandard Real and Imaginary Parts*} |
96 |
|
97 lemma hRe: "hRe (star_n X) = star_n (%n. Re(X n))" |
|
98 by (simp add: hRe_def starfun) |
|
99 |
|
100 lemma hIm: "hIm (star_n X) = star_n (%n. Im(X n))" |
|
101 by (simp add: hIm_def starfun) |
|
102 |
132 |
103 lemma hcomplex_hRe_hIm_cancel_iff: |
133 lemma hcomplex_hRe_hIm_cancel_iff: |
104 "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
134 "!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" |
105 by transfer (rule complex_Re_Im_cancel_iff) |
135 by transfer (rule complex_Re_Im_cancel_iff) |
106 |
136 |
179 by (rule Ring_and_Field.add_divide_distrib) |
209 by (rule Ring_and_Field.add_divide_distrib) |
180 |
210 |
181 |
211 |
182 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} |
212 subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} |
183 |
213 |
184 lemma hcomplex_of_hypreal: |
|
185 "hcomplex_of_hypreal (star_n X) = star_n (%n. complex_of_real (X n))" |
|
186 by (simp add: hcomplex_of_hypreal_def starfun) |
|
187 |
|
188 lemma hcomplex_of_hypreal_cancel_iff [iff]: |
214 lemma hcomplex_of_hypreal_cancel_iff [iff]: |
189 "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" |
215 "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" |
190 by transfer (rule of_real_eq_iff) |
216 by transfer (rule of_real_eq_iff) |
191 |
217 |
192 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" |
218 lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" |
227 by transfer (rule Re_complex_of_real) |
253 by transfer (rule Re_complex_of_real) |
228 |
254 |
229 lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
255 lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" |
230 by transfer (rule Im_complex_of_real) |
256 by transfer (rule Im_complex_of_real) |
231 |
257 |
|
258 lemma hcomplex_of_hypreal_zero_iff [simp]: |
|
259 "\<And>x. (hcomplex_of_hypreal x = 0) = (x = 0)" |
|
260 by transfer (rule of_real_eq_0_iff) |
|
261 |
232 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
262 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: |
233 "hcomplex_of_hypreal epsilon \<noteq> 0" |
263 "hcomplex_of_hypreal epsilon \<noteq> 0" |
234 by (simp add: hcomplex_of_hypreal epsilon_def star_n_zero_num star_n_eq_iff) |
264 by (simp add: hypreal_epsilon_not_zero) |
235 |
|
236 |
265 |
237 subsection{*HComplex theorems*} |
266 subsection{*HComplex theorems*} |
238 |
267 |
239 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |
268 lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" |
240 by transfer (rule Re) |
269 by transfer (rule Re) |
241 |
270 |
242 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" |
271 lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" |
243 by transfer (rule Im) |
272 by transfer (rule Im) |
244 |
|
245 text{*Relates the two nonstandard constructions*} |
|
246 lemma HComplex_eq_Abs_star_Complex: |
|
247 "HComplex (star_n X) (star_n Y) = |
|
248 star_n (%n::nat. Complex (X n) (Y n))" |
|
249 by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) |
|
250 |
273 |
251 lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z" |
274 lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z" |
252 by transfer (rule complex_surj) |
275 by transfer (rule complex_surj) |
253 |
276 |
254 lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]: |
277 lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]: |
255 "(\<And>x y. P (HComplex x y)) ==> P z" |
278 "(\<And>x y. P (HComplex x y)) ==> P z" |
256 by (rule hcomplex_surj [THEN subst], blast) |
279 by (rule hcomplex_surj [THEN subst], blast) |
257 |
280 |
258 |
281 |
259 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} |
282 subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} |
260 |
|
261 lemma hcmod: "hcmod (star_n X) = star_n (%n. cmod (X n))" |
|
262 by (simp add: hcmod_def starfun) |
|
263 |
283 |
264 lemma hcmod_zero [simp]: "hcmod(0) = 0" |
284 lemma hcmod_zero [simp]: "hcmod(0) = 0" |
265 by (rule hnorm_zero) |
285 by (rule hnorm_zero) |
266 |
286 |
267 lemma hcmod_one [simp]: "hcmod(1) = 1" |
287 lemma hcmod_one [simp]: "hcmod(1) = 1" |
326 by transfer (rule complex_of_real_i) |
346 by transfer (rule complex_of_real_i) |
327 |
347 |
328 |
348 |
329 subsection{*Conjugation*} |
349 subsection{*Conjugation*} |
330 |
350 |
331 lemma hcnj: "hcnj (star_n X) = star_n (%n. cnj(X n))" |
|
332 by (simp add: hcnj_def starfun) |
|
333 |
|
334 lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)" |
351 lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)" |
335 by transfer (rule complex_cnj_cancel_iff) |
352 by transfer (rule complex_cnj_cancel_iff) |
336 |
353 |
337 lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z" |
354 lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z" |
338 by transfer (rule complex_cnj_cnj) |
355 by transfer (rule complex_cnj_cnj) |
442 lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
459 lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)" |
443 by transfer (rule complex_mod_diff_ineq) |
460 by transfer (rule complex_mod_diff_ineq) |
444 |
461 |
445 |
462 |
446 subsection{*A Few Nonlinear Theorems*} |
463 subsection{*A Few Nonlinear Theorems*} |
447 |
|
448 lemma hcpow: "star_n X hcpow star_n Y = star_n (%n. X n ^ Y n)" |
|
449 by (simp add: hcpow_def starfun2_star_n) |
|
450 |
464 |
451 lemma hcomplex_of_hypreal_hyperpow: |
465 lemma hcomplex_of_hypreal_hyperpow: |
452 "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
466 "!!x n. hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" |
453 by transfer (rule complex_of_real_pow) |
467 by transfer (rule complex_of_real_pow) |
454 |
468 |
503 by transfer (rule field_power_not_zero) |
517 by transfer (rule field_power_not_zero) |
504 |
518 |
505 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
519 lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" |
506 by (blast intro: ccontr dest: hcpow_not_zero) |
520 by (blast intro: ccontr dest: hcpow_not_zero) |
507 |
521 |
508 lemma star_n_divide: "star_n X / star_n Y = star_n (%n. X n / Y n)" |
|
509 by (simp add: star_divide_def starfun2_star_n) |
|
510 |
|
511 subsection{*The Function @{term hsgn}*} |
522 subsection{*The Function @{term hsgn}*} |
512 |
|
513 lemma hsgn: "hsgn (star_n X) = star_n (%n. sgn (X n))" |
|
514 by (simp add: hsgn_def starfun) |
|
515 |
523 |
516 lemma hsgn_zero [simp]: "hsgn 0 = 0" |
524 lemma hsgn_zero [simp]: "hsgn 0 = 0" |
517 by transfer (rule sgn_zero) |
525 by transfer (rule sgn_zero) |
518 |
526 |
519 lemma hsgn_one [simp]: "hsgn 1 = 1" |
527 lemma hsgn_one [simp]: "hsgn 1 = 1" |
585 |
593 |
586 (*---------------------------------------------------------------------------*) |
594 (*---------------------------------------------------------------------------*) |
587 (* harg *) |
595 (* harg *) |
588 (*---------------------------------------------------------------------------*) |
596 (*---------------------------------------------------------------------------*) |
589 |
597 |
590 lemma harg: "harg (star_n X) = star_n (%n. arg (X n))" |
|
591 by (simp add: harg_def starfun) |
|
592 |
|
593 lemma cos_harg_i_mult_zero_pos: |
598 lemma cos_harg_i_mult_zero_pos: |
594 "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
599 "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" |
595 by transfer (rule cos_arg_i_mult_zero_pos) |
600 by transfer (rule cos_arg_i_mult_zero_pos) |
596 |
601 |
597 lemma cos_harg_i_mult_zero_neg: |
602 lemma cos_harg_i_mult_zero_neg: |
611 |
616 |
612 lemma complex_split_polar2: |
617 lemma complex_split_polar2: |
613 "\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" |
618 "\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" |
614 by (blast intro: complex_split_polar) |
619 by (blast intro: complex_split_polar) |
615 |
620 |
616 lemma lemma_hypreal_P_EX2: |
|
617 "(\<exists>(x::hypreal) y. P x y) = |
|
618 (\<exists>f g. P (star_n f) (star_n g))" |
|
619 apply auto |
|
620 apply (rule_tac x = x in star_cases) |
|
621 apply (rule_tac x = y in star_cases, auto) |
|
622 done |
|
623 |
|
624 lemma hcomplex_split_polar: |
621 lemma hcomplex_split_polar: |
625 "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" |
622 "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" |
626 by transfer (rule complex_split_polar) |
623 by transfer (rule complex_split_polar) |
627 |
|
628 lemma hcis: "hcis (star_n X) = star_n (%n. cis (X n))" |
|
629 by (simp add: hcis_def starfun) |
|
630 |
624 |
631 lemma hcis_eq: |
625 lemma hcis_eq: |
632 "!!a. hcis a = |
626 "!!a. hcis a = |
633 (hcomplex_of_hypreal(( *f* cos) a) + |
627 (hcomplex_of_hypreal(( *f* cos) a) + |
634 iii * hcomplex_of_hypreal(( *f* sin) a))" |
628 iii * hcomplex_of_hypreal(( *f* sin) a))" |
635 by transfer (simp add: cis_def) |
629 by transfer (simp add: cis_def) |
636 |
|
637 lemma hrcis: "hrcis (star_n X) (star_n Y) = star_n (%n. rcis (X n) (Y n))" |
|
638 by (simp add: hrcis_def starfun2_star_n) |
|
639 |
630 |
640 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
631 lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a" |
641 by transfer (rule rcis_Ex) |
632 by transfer (rule rcis_Ex) |
642 |
633 |
643 lemma hRe_hcomplex_polar [simp]: |
634 lemma hRe_hcomplex_polar [simp]: |