27468
|
1 |
(* Title: NSComplex.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Jacques D. Fleuriot
|
|
4 |
Copyright: 2001 University of Edinburgh
|
|
5 |
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
|
|
6 |
*)
|
|
7 |
|
|
8 |
header{*Nonstandard Complex Numbers*}
|
|
9 |
|
|
10 |
theory NSComplex
|
|
11 |
imports Complex "../Hyperreal/NSA"
|
|
12 |
begin
|
|
13 |
|
|
14 |
types hcomplex = "complex star"
|
|
15 |
|
|
16 |
abbreviation
|
|
17 |
hcomplex_of_complex :: "complex => complex star" where
|
|
18 |
"hcomplex_of_complex == star_of"
|
|
19 |
|
|
20 |
abbreviation
|
|
21 |
hcmod :: "complex star => real star" where
|
|
22 |
"hcmod == hnorm"
|
|
23 |
|
|
24 |
|
|
25 |
(*--- real and Imaginary parts ---*)
|
|
26 |
|
|
27 |
definition
|
|
28 |
hRe :: "hcomplex => hypreal" where
|
28562
|
29 |
[code del]: "hRe = *f* Re"
|
27468
|
30 |
|
|
31 |
definition
|
|
32 |
hIm :: "hcomplex => hypreal" where
|
28562
|
33 |
[code del]: "hIm = *f* Im"
|
27468
|
34 |
|
|
35 |
|
|
36 |
(*------ imaginary unit ----------*)
|
|
37 |
|
|
38 |
definition
|
|
39 |
iii :: hcomplex where
|
|
40 |
"iii = star_of ii"
|
|
41 |
|
|
42 |
(*------- complex conjugate ------*)
|
|
43 |
|
|
44 |
definition
|
|
45 |
hcnj :: "hcomplex => hcomplex" where
|
28562
|
46 |
[code del]: "hcnj = *f* cnj"
|
27468
|
47 |
|
|
48 |
(*------------ Argand -------------*)
|
|
49 |
|
|
50 |
definition
|
|
51 |
hsgn :: "hcomplex => hcomplex" where
|
28562
|
52 |
[code del]: "hsgn = *f* sgn"
|
27468
|
53 |
|
|
54 |
definition
|
|
55 |
harg :: "hcomplex => hypreal" where
|
28562
|
56 |
[code del]: "harg = *f* arg"
|
27468
|
57 |
|
|
58 |
definition
|
|
59 |
(* abbreviation for (cos a + i sin a) *)
|
|
60 |
hcis :: "hypreal => hcomplex" where
|
28562
|
61 |
[code del]:"hcis = *f* cis"
|
27468
|
62 |
|
|
63 |
(*----- injection from hyperreals -----*)
|
|
64 |
|
|
65 |
abbreviation
|
|
66 |
hcomplex_of_hypreal :: "hypreal \<Rightarrow> hcomplex" where
|
|
67 |
"hcomplex_of_hypreal \<equiv> of_hypreal"
|
|
68 |
|
|
69 |
definition
|
|
70 |
(* abbreviation for r*(cos a + i sin a) *)
|
|
71 |
hrcis :: "[hypreal, hypreal] => hcomplex" where
|
28562
|
72 |
[code del]: "hrcis = *f2* rcis"
|
27468
|
73 |
|
|
74 |
(*------------ e ^ (x + iy) ------------*)
|
|
75 |
definition
|
|
76 |
hexpi :: "hcomplex => hcomplex" where
|
28562
|
77 |
[code del]: "hexpi = *f* expi"
|
27468
|
78 |
|
|
79 |
definition
|
|
80 |
HComplex :: "[hypreal,hypreal] => hcomplex" where
|
28562
|
81 |
[code del]: "HComplex = *f2* Complex"
|
27468
|
82 |
|
|
83 |
lemmas hcomplex_defs [transfer_unfold] =
|
|
84 |
hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
|
|
85 |
hrcis_def hexpi_def HComplex_def
|
|
86 |
|
|
87 |
lemma Standard_hRe [simp]: "x \<in> Standard \<Longrightarrow> hRe x \<in> Standard"
|
|
88 |
by (simp add: hcomplex_defs)
|
|
89 |
|
|
90 |
lemma Standard_hIm [simp]: "x \<in> Standard \<Longrightarrow> hIm x \<in> Standard"
|
|
91 |
by (simp add: hcomplex_defs)
|
|
92 |
|
|
93 |
lemma Standard_iii [simp]: "iii \<in> Standard"
|
|
94 |
by (simp add: hcomplex_defs)
|
|
95 |
|
|
96 |
lemma Standard_hcnj [simp]: "x \<in> Standard \<Longrightarrow> hcnj x \<in> Standard"
|
|
97 |
by (simp add: hcomplex_defs)
|
|
98 |
|
|
99 |
lemma Standard_hsgn [simp]: "x \<in> Standard \<Longrightarrow> hsgn x \<in> Standard"
|
|
100 |
by (simp add: hcomplex_defs)
|
|
101 |
|
|
102 |
lemma Standard_harg [simp]: "x \<in> Standard \<Longrightarrow> harg x \<in> Standard"
|
|
103 |
by (simp add: hcomplex_defs)
|
|
104 |
|
|
105 |
lemma Standard_hcis [simp]: "r \<in> Standard \<Longrightarrow> hcis r \<in> Standard"
|
|
106 |
by (simp add: hcomplex_defs)
|
|
107 |
|
|
108 |
lemma Standard_hexpi [simp]: "x \<in> Standard \<Longrightarrow> hexpi x \<in> Standard"
|
|
109 |
by (simp add: hcomplex_defs)
|
|
110 |
|
|
111 |
lemma Standard_hrcis [simp]:
|
|
112 |
"\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> hrcis r s \<in> Standard"
|
|
113 |
by (simp add: hcomplex_defs)
|
|
114 |
|
|
115 |
lemma Standard_HComplex [simp]:
|
|
116 |
"\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> HComplex r s \<in> Standard"
|
|
117 |
by (simp add: hcomplex_defs)
|
|
118 |
|
|
119 |
lemma hcmod_def: "hcmod = *f* cmod"
|
|
120 |
by (rule hnorm_def)
|
|
121 |
|
|
122 |
|
|
123 |
subsection{*Properties of Nonstandard Real and Imaginary Parts*}
|
|
124 |
|
|
125 |
lemma hcomplex_hRe_hIm_cancel_iff:
|
|
126 |
"!!w z. (w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
|
|
127 |
by transfer (rule complex_Re_Im_cancel_iff)
|
|
128 |
|
|
129 |
lemma hcomplex_equality [intro?]:
|
|
130 |
"!!z w. hRe z = hRe w ==> hIm z = hIm w ==> z = w"
|
|
131 |
by transfer (rule complex_equality)
|
|
132 |
|
|
133 |
lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
|
|
134 |
by transfer (rule complex_Re_zero)
|
|
135 |
|
|
136 |
lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
|
|
137 |
by transfer (rule complex_Im_zero)
|
|
138 |
|
|
139 |
lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
|
|
140 |
by transfer (rule complex_Re_one)
|
|
141 |
|
|
142 |
lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
|
|
143 |
by transfer (rule complex_Im_one)
|
|
144 |
|
|
145 |
|
|
146 |
subsection{*Addition for Nonstandard Complex Numbers*}
|
|
147 |
|
|
148 |
lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
|
|
149 |
by transfer (rule complex_Re_add)
|
|
150 |
|
|
151 |
lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
|
|
152 |
by transfer (rule complex_Im_add)
|
|
153 |
|
|
154 |
subsection{*More Minus Laws*}
|
|
155 |
|
|
156 |
lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
|
|
157 |
by transfer (rule complex_Re_minus)
|
|
158 |
|
|
159 |
lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
|
|
160 |
by transfer (rule complex_Im_minus)
|
|
161 |
|
|
162 |
lemma hcomplex_add_minus_eq_minus:
|
|
163 |
"x + y = (0::hcomplex) ==> x = -y"
|
|
164 |
apply (drule OrderedGroup.equals_zero_I)
|
|
165 |
apply (simp add: minus_equation_iff [of x y])
|
|
166 |
done
|
|
167 |
|
|
168 |
lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
|
|
169 |
by transfer (rule i_mult_eq2)
|
|
170 |
|
|
171 |
lemma hcomplex_i_mult_left [simp]: "!!z. iii * (iii * z) = -z"
|
|
172 |
by transfer (rule complex_i_mult_minus)
|
|
173 |
|
|
174 |
lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
|
|
175 |
by transfer (rule complex_i_not_zero)
|
|
176 |
|
|
177 |
|
|
178 |
subsection{*More Multiplication Laws*}
|
|
179 |
|
|
180 |
lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
|
|
181 |
by simp
|
|
182 |
|
|
183 |
lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
|
|
184 |
by simp
|
|
185 |
|
|
186 |
lemma hcomplex_mult_left_cancel:
|
|
187 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
|
|
188 |
by simp
|
|
189 |
|
|
190 |
lemma hcomplex_mult_right_cancel:
|
|
191 |
"(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
|
|
192 |
by simp
|
|
193 |
|
|
194 |
|
|
195 |
subsection{*Subraction and Division*}
|
|
196 |
|
|
197 |
lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
|
|
198 |
(* TODO: delete *)
|
|
199 |
by (rule OrderedGroup.diff_eq_eq)
|
|
200 |
|
|
201 |
|
|
202 |
subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
|
|
203 |
|
|
204 |
lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z"
|
|
205 |
by transfer (rule Re_complex_of_real)
|
|
206 |
|
|
207 |
lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0"
|
|
208 |
by transfer (rule Im_complex_of_real)
|
|
209 |
|
|
210 |
lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
|
|
211 |
"hcomplex_of_hypreal epsilon \<noteq> 0"
|
|
212 |
by (simp add: hypreal_epsilon_not_zero)
|
|
213 |
|
|
214 |
subsection{*HComplex theorems*}
|
|
215 |
|
|
216 |
lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
|
|
217 |
by transfer (rule Re)
|
|
218 |
|
|
219 |
lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
|
|
220 |
by transfer (rule Im)
|
|
221 |
|
|
222 |
lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z"
|
|
223 |
by transfer (rule complex_surj)
|
|
224 |
|
|
225 |
lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]:
|
|
226 |
"(\<And>x y. P (HComplex x y)) ==> P z"
|
|
227 |
by (rule hcomplex_surj [THEN subst], blast)
|
|
228 |
|
|
229 |
|
|
230 |
subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
|
|
231 |
|
|
232 |
lemma hcomplex_of_hypreal_abs:
|
|
233 |
"hcomplex_of_hypreal (abs x) =
|
|
234 |
hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
|
|
235 |
by simp
|
|
236 |
|
|
237 |
lemma HComplex_inject [simp]:
|
|
238 |
"!!x y x' y'. HComplex x y = HComplex x' y' = (x=x' & y=y')"
|
|
239 |
by transfer (rule complex.inject)
|
|
240 |
|
|
241 |
lemma HComplex_add [simp]:
|
|
242 |
"!!x1 y1 x2 y2. HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)"
|
|
243 |
by transfer (rule complex_add)
|
|
244 |
|
|
245 |
lemma HComplex_minus [simp]: "!!x y. - HComplex x y = HComplex (-x) (-y)"
|
|
246 |
by transfer (rule complex_minus)
|
|
247 |
|
|
248 |
lemma HComplex_diff [simp]:
|
|
249 |
"!!x1 y1 x2 y2. HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)"
|
|
250 |
by transfer (rule complex_diff)
|
|
251 |
|
|
252 |
lemma HComplex_mult [simp]:
|
|
253 |
"!!x1 y1 x2 y2. HComplex x1 y1 * HComplex x2 y2 =
|
|
254 |
HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
|
|
255 |
by transfer (rule complex_mult)
|
|
256 |
|
|
257 |
(*HComplex_inverse is proved below*)
|
|
258 |
|
|
259 |
lemma hcomplex_of_hypreal_eq: "!!r. hcomplex_of_hypreal r = HComplex r 0"
|
|
260 |
by transfer (rule complex_of_real_def)
|
|
261 |
|
|
262 |
lemma HComplex_add_hcomplex_of_hypreal [simp]:
|
|
263 |
"!!x y r. HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y"
|
|
264 |
by transfer (rule Complex_add_complex_of_real)
|
|
265 |
|
|
266 |
lemma hcomplex_of_hypreal_add_HComplex [simp]:
|
|
267 |
"!!r x y. hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y"
|
|
268 |
by transfer (rule complex_of_real_add_Complex)
|
|
269 |
|
|
270 |
lemma HComplex_mult_hcomplex_of_hypreal:
|
|
271 |
"!!x y r. HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)"
|
|
272 |
by transfer (rule Complex_mult_complex_of_real)
|
|
273 |
|
|
274 |
lemma hcomplex_of_hypreal_mult_HComplex:
|
|
275 |
"!!r x y. hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)"
|
|
276 |
by transfer (rule complex_of_real_mult_Complex)
|
|
277 |
|
|
278 |
lemma i_hcomplex_of_hypreal [simp]:
|
|
279 |
"!!r. iii * hcomplex_of_hypreal r = HComplex 0 r"
|
|
280 |
by transfer (rule i_complex_of_real)
|
|
281 |
|
|
282 |
lemma hcomplex_of_hypreal_i [simp]:
|
|
283 |
"!!r. hcomplex_of_hypreal r * iii = HComplex 0 r"
|
|
284 |
by transfer (rule complex_of_real_i)
|
|
285 |
|
|
286 |
|
|
287 |
subsection{*Conjugation*}
|
|
288 |
|
|
289 |
lemma hcomplex_hcnj_cancel_iff [iff]: "!!x y. (hcnj x = hcnj y) = (x = y)"
|
|
290 |
by transfer (rule complex_cnj_cancel_iff)
|
|
291 |
|
|
292 |
lemma hcomplex_hcnj_hcnj [simp]: "!!z. hcnj (hcnj z) = z"
|
|
293 |
by transfer (rule complex_cnj_cnj)
|
|
294 |
|
|
295 |
lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
|
|
296 |
"!!x. hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
|
|
297 |
by transfer (rule complex_cnj_complex_of_real)
|
|
298 |
|
|
299 |
lemma hcomplex_hmod_hcnj [simp]: "!!z. hcmod (hcnj z) = hcmod z"
|
|
300 |
by transfer (rule complex_mod_cnj)
|
|
301 |
|
|
302 |
lemma hcomplex_hcnj_minus: "!!z. hcnj (-z) = - hcnj z"
|
|
303 |
by transfer (rule complex_cnj_minus)
|
|
304 |
|
|
305 |
lemma hcomplex_hcnj_inverse: "!!z. hcnj(inverse z) = inverse(hcnj z)"
|
|
306 |
by transfer (rule complex_cnj_inverse)
|
|
307 |
|
|
308 |
lemma hcomplex_hcnj_add: "!!w z. hcnj(w + z) = hcnj(w) + hcnj(z)"
|
|
309 |
by transfer (rule complex_cnj_add)
|
|
310 |
|
|
311 |
lemma hcomplex_hcnj_diff: "!!w z. hcnj(w - z) = hcnj(w) - hcnj(z)"
|
|
312 |
by transfer (rule complex_cnj_diff)
|
|
313 |
|
|
314 |
lemma hcomplex_hcnj_mult: "!!w z. hcnj(w * z) = hcnj(w) * hcnj(z)"
|
|
315 |
by transfer (rule complex_cnj_mult)
|
|
316 |
|
|
317 |
lemma hcomplex_hcnj_divide: "!!w z. hcnj(w / z) = (hcnj w)/(hcnj z)"
|
|
318 |
by transfer (rule complex_cnj_divide)
|
|
319 |
|
|
320 |
lemma hcnj_one [simp]: "hcnj 1 = 1"
|
|
321 |
by transfer (rule complex_cnj_one)
|
|
322 |
|
|
323 |
lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
|
|
324 |
by transfer (rule complex_cnj_zero)
|
|
325 |
|
|
326 |
lemma hcomplex_hcnj_zero_iff [iff]: "!!z. (hcnj z = 0) = (z = 0)"
|
|
327 |
by transfer (rule complex_cnj_zero_iff)
|
|
328 |
|
|
329 |
lemma hcomplex_mult_hcnj:
|
|
330 |
"!!z. z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
|
|
331 |
by transfer (rule complex_mult_cnj)
|
|
332 |
|
|
333 |
|
|
334 |
subsection{*More Theorems about the Function @{term hcmod}*}
|
|
335 |
|
|
336 |
lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
|
|
337 |
"hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
|
|
338 |
by simp
|
|
339 |
|
|
340 |
lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
|
|
341 |
"hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
|
|
342 |
by simp
|
|
343 |
|
|
344 |
lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
|
|
345 |
by transfer (rule complex_mod_mult_cnj)
|
|
346 |
|
|
347 |
lemma hcmod_triangle_ineq2 [simp]:
|
|
348 |
"!!a b. hcmod(b + a) - hcmod b \<le> hcmod a"
|
|
349 |
by transfer (rule complex_mod_triangle_ineq2)
|
|
350 |
|
|
351 |
lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
|
|
352 |
by transfer (rule norm_diff_ineq)
|
|
353 |
|
|
354 |
|
|
355 |
subsection{*Exponentiation*}
|
|
356 |
|
|
357 |
lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)"
|
|
358 |
by (rule power_0)
|
|
359 |
|
|
360 |
lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)"
|
|
361 |
by (rule power_Suc)
|
|
362 |
|
|
363 |
lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = -1"
|
|
364 |
by transfer (rule power2_i)
|
|
365 |
|
|
366 |
lemma hcomplex_of_hypreal_pow:
|
|
367 |
"!!x. hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n"
|
|
368 |
by transfer (rule of_real_power)
|
|
369 |
|
|
370 |
lemma hcomplex_hcnj_pow: "!!z. hcnj(z ^ n) = hcnj(z) ^ n"
|
|
371 |
by transfer (rule complex_cnj_power)
|
|
372 |
|
|
373 |
lemma hcmod_hcomplexpow: "!!x. hcmod(x ^ n) = hcmod(x) ^ n"
|
|
374 |
by transfer (rule norm_power)
|
|
375 |
|
|
376 |
lemma hcpow_minus:
|
|
377 |
"!!x n. (-x::hcomplex) pow n =
|
|
378 |
(if ( *p* even) n then (x pow n) else -(x pow n))"
|
|
379 |
by transfer (rule neg_power_if)
|
|
380 |
|
|
381 |
lemma hcpow_mult:
|
|
382 |
"!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
|
|
383 |
by transfer (rule power_mult_distrib)
|
|
384 |
|
|
385 |
lemma hcpow_zero2 [simp]:
|
31017
|
386 |
"\<And>n. 0 pow (hSuc n) = (0::'a::{semiring_0} star)"
|
27468
|
387 |
by transfer (rule power_0_Suc)
|
|
388 |
|
|
389 |
lemma hcpow_not_zero [simp,intro]:
|
|
390 |
"!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
|
|
391 |
by (rule hyperpow_not_zero)
|
|
392 |
|
|
393 |
lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
|
|
394 |
by (blast intro: ccontr dest: hcpow_not_zero)
|
|
395 |
|
|
396 |
subsection{*The Function @{term hsgn}*}
|
|
397 |
|
|
398 |
lemma hsgn_zero [simp]: "hsgn 0 = 0"
|
|
399 |
by transfer (rule sgn_zero)
|
|
400 |
|
|
401 |
lemma hsgn_one [simp]: "hsgn 1 = 1"
|
|
402 |
by transfer (rule sgn_one)
|
|
403 |
|
|
404 |
lemma hsgn_minus: "!!z. hsgn (-z) = - hsgn(z)"
|
|
405 |
by transfer (rule sgn_minus)
|
|
406 |
|
|
407 |
lemma hsgn_eq: "!!z. hsgn z = z / hcomplex_of_hypreal (hcmod z)"
|
|
408 |
by transfer (rule sgn_eq)
|
|
409 |
|
|
410 |
lemma hcmod_i: "!!x y. hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)"
|
|
411 |
by transfer (rule complex_norm)
|
|
412 |
|
|
413 |
lemma hcomplex_eq_cancel_iff1 [simp]:
|
|
414 |
"(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)"
|
|
415 |
by (simp add: hcomplex_of_hypreal_eq)
|
|
416 |
|
|
417 |
lemma hcomplex_eq_cancel_iff2 [simp]:
|
|
418 |
"(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)"
|
|
419 |
by (simp add: hcomplex_of_hypreal_eq)
|
|
420 |
|
|
421 |
lemma HComplex_eq_0 [simp]: "!!x y. (HComplex x y = 0) = (x = 0 & y = 0)"
|
|
422 |
by transfer (rule Complex_eq_0)
|
|
423 |
|
|
424 |
lemma HComplex_eq_1 [simp]: "!!x y. (HComplex x y = 1) = (x = 1 & y = 0)"
|
|
425 |
by transfer (rule Complex_eq_1)
|
|
426 |
|
|
427 |
lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
|
|
428 |
by transfer (rule i_def [THEN meta_eq_to_obj_eq])
|
|
429 |
|
|
430 |
lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)"
|
|
431 |
by transfer (rule Complex_eq_i)
|
|
432 |
|
|
433 |
lemma hRe_hsgn [simp]: "!!z. hRe(hsgn z) = hRe(z)/hcmod z"
|
|
434 |
by transfer (rule Re_sgn)
|
|
435 |
|
|
436 |
lemma hIm_hsgn [simp]: "!!z. hIm(hsgn z) = hIm(z)/hcmod z"
|
|
437 |
by transfer (rule Im_sgn)
|
|
438 |
|
|
439 |
lemma hcomplex_inverse_complex_split:
|
|
440 |
"!!x y. inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
|
|
441 |
hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
|
|
442 |
iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
|
|
443 |
by transfer (rule complex_inverse_complex_split)
|
|
444 |
|
|
445 |
lemma HComplex_inverse:
|
|
446 |
"!!x y. inverse (HComplex x y) =
|
|
447 |
HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
|
|
448 |
by transfer (rule complex_inverse)
|
|
449 |
|
|
450 |
lemma hRe_mult_i_eq[simp]:
|
|
451 |
"!!y. hRe (iii * hcomplex_of_hypreal y) = 0"
|
|
452 |
by transfer simp
|
|
453 |
|
|
454 |
lemma hIm_mult_i_eq [simp]:
|
|
455 |
"!!y. hIm (iii * hcomplex_of_hypreal y) = y"
|
|
456 |
by transfer simp
|
|
457 |
|
|
458 |
lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
|
|
459 |
by transfer simp
|
|
460 |
|
|
461 |
lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
|
|
462 |
by transfer simp
|
|
463 |
|
|
464 |
(*---------------------------------------------------------------------------*)
|
|
465 |
(* harg *)
|
|
466 |
(*---------------------------------------------------------------------------*)
|
|
467 |
|
|
468 |
lemma cos_harg_i_mult_zero_pos:
|
|
469 |
"!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
|
|
470 |
by transfer (rule cos_arg_i_mult_zero_pos)
|
|
471 |
|
|
472 |
lemma cos_harg_i_mult_zero_neg:
|
|
473 |
"!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
|
|
474 |
by transfer (rule cos_arg_i_mult_zero_neg)
|
|
475 |
|
|
476 |
lemma cos_harg_i_mult_zero [simp]:
|
|
477 |
"!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
|
|
478 |
by transfer (rule cos_arg_i_mult_zero)
|
|
479 |
|
|
480 |
lemma hcomplex_of_hypreal_zero_iff [simp]:
|
|
481 |
"!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
|
|
482 |
by transfer (rule of_real_eq_0_iff)
|
|
483 |
|
|
484 |
|
|
485 |
subsection{*Polar Form for Nonstandard Complex Numbers*}
|
|
486 |
|
|
487 |
lemma complex_split_polar2:
|
|
488 |
"\<forall>n. \<exists>r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))"
|
|
489 |
by (blast intro: complex_split_polar)
|
|
490 |
|
|
491 |
lemma hcomplex_split_polar:
|
|
492 |
"!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
|
|
493 |
by transfer (rule complex_split_polar)
|
|
494 |
|
|
495 |
lemma hcis_eq:
|
|
496 |
"!!a. hcis a =
|
|
497 |
(hcomplex_of_hypreal(( *f* cos) a) +
|
|
498 |
iii * hcomplex_of_hypreal(( *f* sin) a))"
|
|
499 |
by transfer (simp add: cis_def)
|
|
500 |
|
|
501 |
lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
|
|
502 |
by transfer (rule rcis_Ex)
|
|
503 |
|
|
504 |
lemma hRe_hcomplex_polar [simp]:
|
|
505 |
"!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
|
|
506 |
r * ( *f* cos) a"
|
|
507 |
by transfer simp
|
|
508 |
|
|
509 |
lemma hRe_hrcis [simp]: "!!r a. hRe(hrcis r a) = r * ( *f* cos) a"
|
|
510 |
by transfer (rule Re_rcis)
|
|
511 |
|
|
512 |
lemma hIm_hcomplex_polar [simp]:
|
|
513 |
"!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
|
|
514 |
r * ( *f* sin) a"
|
|
515 |
by transfer simp
|
|
516 |
|
|
517 |
lemma hIm_hrcis [simp]: "!!r a. hIm(hrcis r a) = r * ( *f* sin) a"
|
|
518 |
by transfer (rule Im_rcis)
|
|
519 |
|
|
520 |
lemma hcmod_unit_one [simp]:
|
|
521 |
"!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
|
|
522 |
by transfer (rule cmod_unit_one)
|
|
523 |
|
|
524 |
lemma hcmod_complex_polar [simp]:
|
|
525 |
"!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
|
|
526 |
abs r"
|
|
527 |
by transfer (rule cmod_complex_polar)
|
|
528 |
|
|
529 |
lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
|
|
530 |
by transfer (rule complex_mod_rcis)
|
|
531 |
|
|
532 |
(*---------------------------------------------------------------------------*)
|
|
533 |
(* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *)
|
|
534 |
(*---------------------------------------------------------------------------*)
|
|
535 |
|
|
536 |
lemma hcis_hrcis_eq: "!!a. hcis a = hrcis 1 a"
|
|
537 |
by transfer (rule cis_rcis_eq)
|
|
538 |
declare hcis_hrcis_eq [symmetric, simp]
|
|
539 |
|
|
540 |
lemma hrcis_mult:
|
|
541 |
"!!a b r1 r2. hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
|
|
542 |
by transfer (rule rcis_mult)
|
|
543 |
|
|
544 |
lemma hcis_mult: "!!a b. hcis a * hcis b = hcis (a + b)"
|
|
545 |
by transfer (rule cis_mult)
|
|
546 |
|
|
547 |
lemma hcis_zero [simp]: "hcis 0 = 1"
|
|
548 |
by transfer (rule cis_zero)
|
|
549 |
|
|
550 |
lemma hrcis_zero_mod [simp]: "!!a. hrcis 0 a = 0"
|
|
551 |
by transfer (rule rcis_zero_mod)
|
|
552 |
|
|
553 |
lemma hrcis_zero_arg [simp]: "!!r. hrcis r 0 = hcomplex_of_hypreal r"
|
|
554 |
by transfer (rule rcis_zero_arg)
|
|
555 |
|
|
556 |
lemma hcomplex_i_mult_minus [simp]: "!!x. iii * (iii * x) = - x"
|
|
557 |
by transfer (rule complex_i_mult_minus)
|
|
558 |
|
|
559 |
lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
|
|
560 |
by simp
|
|
561 |
|
|
562 |
lemma hcis_hypreal_of_nat_Suc_mult:
|
|
563 |
"!!a. hcis (hypreal_of_nat (Suc n) * a) =
|
|
564 |
hcis a * hcis (hypreal_of_nat n * a)"
|
|
565 |
apply transfer
|
|
566 |
apply (fold real_of_nat_def)
|
|
567 |
apply (rule cis_real_of_nat_Suc_mult)
|
|
568 |
done
|
|
569 |
|
|
570 |
lemma NSDeMoivre: "!!a. (hcis a) ^ n = hcis (hypreal_of_nat n * a)"
|
|
571 |
apply transfer
|
|
572 |
apply (fold real_of_nat_def)
|
|
573 |
apply (rule DeMoivre)
|
|
574 |
done
|
|
575 |
|
|
576 |
lemma hcis_hypreal_of_hypnat_Suc_mult:
|
|
577 |
"!! a n. hcis (hypreal_of_hypnat (n + 1) * a) =
|
|
578 |
hcis a * hcis (hypreal_of_hypnat n * a)"
|
|
579 |
by transfer (fold real_of_nat_def, simp add: cis_real_of_nat_Suc_mult)
|
|
580 |
|
|
581 |
lemma NSDeMoivre_ext:
|
|
582 |
"!!a n. (hcis a) pow n = hcis (hypreal_of_hypnat n * a)"
|
|
583 |
by transfer (fold real_of_nat_def, rule DeMoivre)
|
|
584 |
|
|
585 |
lemma NSDeMoivre2:
|
|
586 |
"!!a r. (hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
|
|
587 |
by transfer (fold real_of_nat_def, rule DeMoivre2)
|
|
588 |
|
|
589 |
lemma DeMoivre2_ext:
|
|
590 |
"!! a r n. (hrcis r a) pow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
|
|
591 |
by transfer (fold real_of_nat_def, rule DeMoivre2)
|
|
592 |
|
|
593 |
lemma hcis_inverse [simp]: "!!a. inverse(hcis a) = hcis (-a)"
|
|
594 |
by transfer (rule cis_inverse)
|
|
595 |
|
|
596 |
lemma hrcis_inverse: "!!a r. inverse(hrcis r a) = hrcis (inverse r) (-a)"
|
|
597 |
by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
|
|
598 |
|
|
599 |
lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
|
|
600 |
by transfer (rule Re_cis)
|
|
601 |
|
|
602 |
lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
|
|
603 |
by transfer (rule Im_cis)
|
|
604 |
|
|
605 |
lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
|
|
606 |
by (simp add: NSDeMoivre)
|
|
607 |
|
|
608 |
lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
|
|
609 |
by (simp add: NSDeMoivre)
|
|
610 |
|
|
611 |
lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a pow n)"
|
|
612 |
by (simp add: NSDeMoivre_ext)
|
|
613 |
|
|
614 |
lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a pow n)"
|
|
615 |
by (simp add: NSDeMoivre_ext)
|
|
616 |
|
|
617 |
lemma hexpi_add: "!!a b. hexpi(a + b) = hexpi(a) * hexpi(b)"
|
|
618 |
by transfer (rule expi_add)
|
|
619 |
|
|
620 |
|
|
621 |
subsection{*@{term hcomplex_of_complex}: the Injection from
|
|
622 |
type @{typ complex} to to @{typ hcomplex}*}
|
|
623 |
|
|
624 |
lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
|
|
625 |
(* TODO: delete *)
|
|
626 |
by (rule inj_star_of)
|
|
627 |
|
|
628 |
lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
|
|
629 |
by (rule iii_def)
|
|
630 |
|
|
631 |
lemma hRe_hcomplex_of_complex:
|
|
632 |
"hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
|
|
633 |
by transfer (rule refl)
|
|
634 |
|
|
635 |
lemma hIm_hcomplex_of_complex:
|
|
636 |
"hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
|
|
637 |
by transfer (rule refl)
|
|
638 |
|
|
639 |
lemma hcmod_hcomplex_of_complex:
|
|
640 |
"hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
|
|
641 |
by transfer (rule refl)
|
|
642 |
|
|
643 |
|
|
644 |
subsection{*Numerals and Arithmetic*}
|
|
645 |
|
|
646 |
lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w"
|
|
647 |
by transfer (rule number_of_eq [THEN eq_reflection])
|
|
648 |
|
|
649 |
lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
|
|
650 |
"hcomplex_of_hypreal (hypreal_of_real x) =
|
|
651 |
hcomplex_of_complex (complex_of_real x)"
|
|
652 |
by transfer (rule refl)
|
|
653 |
|
|
654 |
lemma hcomplex_hypreal_number_of:
|
|
655 |
"hcomplex_of_complex (number_of w) = hcomplex_of_hypreal(number_of w)"
|
|
656 |
by transfer (rule of_real_number_of_eq [symmetric])
|
|
657 |
|
|
658 |
lemma hcomplex_number_of_hcnj [simp]:
|
|
659 |
"hcnj (number_of v :: hcomplex) = number_of v"
|
|
660 |
by transfer (rule complex_cnj_number_of)
|
|
661 |
|
|
662 |
lemma hcomplex_number_of_hcmod [simp]:
|
|
663 |
"hcmod(number_of v :: hcomplex) = abs (number_of v :: hypreal)"
|
|
664 |
by transfer (rule norm_number_of)
|
|
665 |
|
|
666 |
lemma hcomplex_number_of_hRe [simp]:
|
|
667 |
"hRe(number_of v :: hcomplex) = number_of v"
|
|
668 |
by transfer (rule complex_Re_number_of)
|
|
669 |
|
|
670 |
lemma hcomplex_number_of_hIm [simp]:
|
|
671 |
"hIm(number_of v :: hcomplex) = 0"
|
|
672 |
by transfer (rule complex_Im_number_of)
|
|
673 |
|
|
674 |
end
|