author | paulson |
Tue, 13 Jan 2004 10:37:52 +0100 | |
changeset 14354 | 988aa4648597 |
parent 14353 | 79f9fbef9106 |
child 14373 | 67a628beb981 |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: Complex.thy |
2 |
Author: Jacques D. Fleuriot |
|
3 |
Copyright: 2001 University of Edinburgh |
|
4 |
Description: Complex numbers |
|
5 |
*) |
|
6 |
||
14323 | 7 |
theory Complex = HLog: |
13957 | 8 |
|
9 |
typedef complex = "{p::(real*real). True}" |
|
14323 | 10 |
by blast |
13957 | 11 |
|
14323 | 12 |
instance complex :: zero .. |
13 |
instance complex :: one .. |
|
14 |
instance complex :: plus .. |
|
15 |
instance complex :: times .. |
|
16 |
instance complex :: minus .. |
|
17 |
instance complex :: inverse .. |
|
18 |
instance complex :: power .. |
|
13957 | 19 |
|
20 |
consts |
|
14323 | 21 |
"ii" :: complex ("ii") |
13957 | 22 |
|
23 |
constdefs |
|
24 |
||
25 |
(*--- real and Imaginary parts ---*) |
|
14323 | 26 |
|
27 |
Re :: "complex => real" |
|
13957 | 28 |
"Re(z) == fst(Rep_complex z)" |
29 |
||
14323 | 30 |
Im :: "complex => real" |
13957 | 31 |
"Im(z) == snd(Rep_complex z)" |
32 |
||
33 |
(*----------- modulus ------------*) |
|
34 |
||
14323 | 35 |
cmod :: "complex => real" |
36 |
"cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)" |
|
13957 | 37 |
|
14323 | 38 |
(*----- injection from reals -----*) |
39 |
||
40 |
complex_of_real :: "real => complex" |
|
13957 | 41 |
"complex_of_real r == Abs_complex(r,0::real)" |
14323 | 42 |
|
13957 | 43 |
(*------- complex conjugate ------*) |
44 |
||
14323 | 45 |
cnj :: "complex => complex" |
13957 | 46 |
"cnj z == Abs_complex(Re z, -Im z)" |
47 |
||
14323 | 48 |
(*------------ Argand -------------*) |
13957 | 49 |
|
14323 | 50 |
sgn :: "complex => complex" |
13957 | 51 |
"sgn z == z / complex_of_real(cmod z)" |
52 |
||
14323 | 53 |
arg :: "complex => real" |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
54 |
"arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi" |
14323 | 55 |
|
13957 | 56 |
|
14323 | 57 |
defs (overloaded) |
58 |
||
59 |
complex_zero_def: |
|
13957 | 60 |
"0 == Abs_complex(0::real,0)" |
61 |
||
14323 | 62 |
complex_one_def: |
13957 | 63 |
"1 == Abs_complex(1,0::real)" |
64 |
||
14323 | 65 |
(*------ imaginary unit ----------*) |
66 |
||
67 |
i_def: |
|
13957 | 68 |
"ii == Abs_complex(0::real,1)" |
69 |
||
70 |
(*----------- negation -----------*) |
|
14323 | 71 |
|
72 |
complex_minus_def: |
|
73 |
"- (z::complex) == Abs_complex(-Re z, -Im z)" |
|
13957 | 74 |
|
14323 | 75 |
|
13957 | 76 |
(*----------- inverse -----------*) |
14323 | 77 |
complex_inverse_def: |
13957 | 78 |
"inverse (z::complex) == Abs_complex(Re(z)/(Re(z) ^ 2 + Im(z) ^ 2), |
79 |
-Im(z)/(Re(z) ^ 2 + Im(z) ^ 2))" |
|
80 |
||
14323 | 81 |
complex_add_def: |
13957 | 82 |
"w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))" |
83 |
||
14323 | 84 |
complex_diff_def: |
13957 | 85 |
"w - (z::complex) == w + -(z::complex)" |
86 |
||
14323 | 87 |
complex_mult_def: |
13957 | 88 |
"w * (z::complex) == Abs_complex(Re(w) * Re(z) - Im(w) * Im(z), |
89 |
Re(w) * Im(z) + Im(w) * Re(z))" |
|
90 |
||
91 |
||
92 |
(*----------- division ----------*) |
|
14323 | 93 |
complex_divide_def: |
13957 | 94 |
"w / (z::complex) == w * inverse z" |
14323 | 95 |
|
13957 | 96 |
|
97 |
constdefs |
|
98 |
||
99 |
(* abbreviation for (cos a + i sin a) *) |
|
14323 | 100 |
cis :: "real => complex" |
13957 | 101 |
"cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)" |
102 |
||
103 |
(* abbreviation for r*(cos a + i sin a) *) |
|
14323 | 104 |
rcis :: "[real, real] => complex" |
13957 | 105 |
"rcis r a == complex_of_real r * cis a" |
106 |
||
107 |
(* e ^ (x + iy) *) |
|
14323 | 108 |
expi :: "complex => complex" |
13957 | 109 |
"expi z == complex_of_real(exp (Re z)) * cis (Im z)" |
14323 | 110 |
|
111 |
||
112 |
lemma inj_Rep_complex: "inj Rep_complex" |
|
113 |
apply (rule inj_on_inverseI) |
|
114 |
apply (rule Rep_complex_inverse) |
|
115 |
done |
|
116 |
||
117 |
lemma inj_Abs_complex: "inj Abs_complex" |
|
118 |
apply (rule inj_on_inverseI) |
|
119 |
apply (rule Abs_complex_inverse) |
|
120 |
apply (simp (no_asm) add: complex_def) |
|
121 |
done |
|
122 |
declare inj_Abs_complex [THEN injD, simp] |
|
123 |
||
124 |
lemma Abs_complex_cancel_iff: "(Abs_complex x = Abs_complex y) = (x = y)" |
|
14334 | 125 |
by (auto dest: inj_Abs_complex [THEN injD]) |
14323 | 126 |
declare Abs_complex_cancel_iff [simp] |
127 |
||
128 |
lemma pair_mem_complex: "(x,y) : complex" |
|
14334 | 129 |
by (unfold complex_def, auto) |
14323 | 130 |
declare pair_mem_complex [simp] |
131 |
||
132 |
lemma Abs_complex_inverse2: "Rep_complex (Abs_complex (x,y)) = (x,y)" |
|
133 |
apply (simp (no_asm) add: Abs_complex_inverse) |
|
134 |
done |
|
135 |
declare Abs_complex_inverse2 [simp] |
|
136 |
||
137 |
lemma eq_Abs_complex: "(!!x y. z = Abs_complex(x,y) ==> P) ==> P" |
|
138 |
apply (rule_tac p = "Rep_complex z" in PairE) |
|
14334 | 139 |
apply (drule_tac f = Abs_complex in arg_cong) |
14323 | 140 |
apply (force simp add: Rep_complex_inverse) |
141 |
done |
|
142 |
||
143 |
lemma Re: "Re(Abs_complex(x,y)) = x" |
|
144 |
apply (unfold Re_def) |
|
145 |
apply (simp (no_asm)) |
|
146 |
done |
|
147 |
declare Re [simp] |
|
148 |
||
149 |
lemma Im: "Im(Abs_complex(x,y)) = y" |
|
150 |
apply (unfold Im_def) |
|
151 |
apply (simp (no_asm)) |
|
152 |
done |
|
153 |
declare Im [simp] |
|
154 |
||
155 |
lemma Abs_complex_cancel: "Abs_complex(Re(z),Im(z)) = z" |
|
14334 | 156 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 157 |
apply (simp (no_asm_simp)) |
158 |
done |
|
159 |
declare Abs_complex_cancel [simp] |
|
160 |
||
161 |
lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))" |
|
14334 | 162 |
apply (rule_tac z = w in eq_Abs_complex) |
163 |
apply (rule_tac z = z in eq_Abs_complex) |
|
14323 | 164 |
apply (auto dest: inj_Abs_complex [THEN injD]) |
165 |
done |
|
166 |
||
167 |
lemma complex_Re_zero: "Re 0 = 0" |
|
168 |
apply (unfold complex_zero_def) |
|
169 |
apply (simp (no_asm)) |
|
170 |
done |
|
171 |
||
172 |
lemma complex_Im_zero: "Im 0 = 0" |
|
173 |
apply (unfold complex_zero_def) |
|
174 |
apply (simp (no_asm)) |
|
175 |
done |
|
176 |
declare complex_Re_zero [simp] complex_Im_zero [simp] |
|
177 |
||
178 |
lemma complex_Re_one: "Re 1 = 1" |
|
179 |
apply (unfold complex_one_def) |
|
180 |
apply (simp (no_asm)) |
|
181 |
done |
|
182 |
declare complex_Re_one [simp] |
|
183 |
||
184 |
lemma complex_Im_one: "Im 1 = 0" |
|
185 |
apply (unfold complex_one_def) |
|
186 |
apply (simp (no_asm)) |
|
187 |
done |
|
188 |
declare complex_Im_one [simp] |
|
189 |
||
190 |
lemma complex_Re_i: "Re(ii) = 0" |
|
14334 | 191 |
by (unfold i_def, auto) |
14323 | 192 |
declare complex_Re_i [simp] |
193 |
||
194 |
lemma complex_Im_i: "Im(ii) = 1" |
|
14334 | 195 |
by (unfold i_def, auto) |
14323 | 196 |
declare complex_Im_i [simp] |
197 |
||
198 |
lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0" |
|
199 |
apply (unfold complex_of_real_def) |
|
200 |
apply (simp (no_asm)) |
|
201 |
done |
|
202 |
declare Re_complex_of_real_zero [simp] |
|
203 |
||
204 |
lemma Im_complex_of_real_zero: "Im(complex_of_real 0) = 0" |
|
205 |
apply (unfold complex_of_real_def) |
|
206 |
apply (simp (no_asm)) |
|
207 |
done |
|
208 |
declare Im_complex_of_real_zero [simp] |
|
209 |
||
210 |
lemma Re_complex_of_real_one: "Re(complex_of_real 1) = 1" |
|
211 |
apply (unfold complex_of_real_def) |
|
212 |
apply (simp (no_asm)) |
|
213 |
done |
|
214 |
declare Re_complex_of_real_one [simp] |
|
215 |
||
216 |
lemma Im_complex_of_real_one: "Im(complex_of_real 1) = 0" |
|
217 |
apply (unfold complex_of_real_def) |
|
218 |
apply (simp (no_asm)) |
|
219 |
done |
|
220 |
declare Im_complex_of_real_one [simp] |
|
221 |
||
222 |
lemma Re_complex_of_real: "Re(complex_of_real z) = z" |
|
14334 | 223 |
by (unfold complex_of_real_def, auto) |
14323 | 224 |
declare Re_complex_of_real [simp] |
225 |
||
226 |
lemma Im_complex_of_real: "Im(complex_of_real z) = 0" |
|
14334 | 227 |
by (unfold complex_of_real_def, auto) |
14323 | 228 |
declare Im_complex_of_real [simp] |
229 |
||
230 |
||
231 |
subsection{*Negation*} |
|
232 |
||
233 |
lemma complex_minus: "- Abs_complex(x,y) = Abs_complex(-x,-y)" |
|
234 |
apply (unfold complex_minus_def) |
|
235 |
apply (simp (no_asm)) |
|
236 |
done |
|
237 |
||
238 |
lemma complex_Re_minus: "Re (-z) = - Re z" |
|
239 |
apply (unfold Re_def) |
|
14334 | 240 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 241 |
apply (auto simp add: complex_minus) |
242 |
done |
|
243 |
||
244 |
lemma complex_Im_minus: "Im (-z) = - Im z" |
|
245 |
apply (unfold Im_def) |
|
14334 | 246 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 247 |
apply (auto simp add: complex_minus) |
248 |
done |
|
249 |
||
250 |
lemma complex_minus_minus: "- (- z) = (z::complex)" |
|
251 |
apply (unfold complex_minus_def) |
|
252 |
apply (simp (no_asm)) |
|
253 |
done |
|
254 |
declare complex_minus_minus [simp] |
|
255 |
||
256 |
lemma inj_complex_minus: "inj(%r::complex. -r)" |
|
257 |
apply (rule inj_onI) |
|
14334 | 258 |
apply (drule_tac f = uminus in arg_cong, simp) |
14323 | 259 |
done |
260 |
||
261 |
lemma complex_minus_zero: "-(0::complex) = 0" |
|
262 |
apply (unfold complex_zero_def) |
|
263 |
apply (simp (no_asm) add: complex_minus) |
|
264 |
done |
|
265 |
declare complex_minus_zero [simp] |
|
266 |
||
267 |
lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))" |
|
14334 | 268 |
apply (rule_tac z = x in eq_Abs_complex) |
14323 | 269 |
apply (auto dest: inj_Abs_complex [THEN injD] |
270 |
simp add: complex_zero_def complex_minus) |
|
271 |
done |
|
272 |
declare complex_minus_zero_iff [simp] |
|
273 |
||
274 |
lemma complex_minus_zero_iff2: "(0 = -x) = (x = (0::real))" |
|
14334 | 275 |
by (auto dest: sym) |
14323 | 276 |
declare complex_minus_zero_iff2 [simp] |
277 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
278 |
lemma complex_minus_not_zero_iff: "(-x \<noteq> 0) = (x \<noteq> (0::complex))" |
14334 | 279 |
by auto |
14323 | 280 |
|
281 |
||
282 |
subsection{*Addition*} |
|
283 |
||
284 |
lemma complex_add: |
|
285 |
"Abs_complex(x1,y1) + Abs_complex(x2,y2) = Abs_complex(x1+x2,y1+y2)" |
|
286 |
apply (unfold complex_add_def) |
|
287 |
apply (simp (no_asm)) |
|
288 |
done |
|
289 |
||
290 |
lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)" |
|
291 |
apply (unfold Re_def) |
|
14334 | 292 |
apply (rule_tac z = x in eq_Abs_complex) |
293 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 294 |
apply (auto simp add: complex_add) |
295 |
done |
|
296 |
||
297 |
lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)" |
|
298 |
apply (unfold Im_def) |
|
14334 | 299 |
apply (rule_tac z = x in eq_Abs_complex) |
300 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 301 |
apply (auto simp add: complex_add) |
302 |
done |
|
303 |
||
304 |
lemma complex_add_commute: "(u::complex) + v = v + u" |
|
305 |
apply (unfold complex_add_def) |
|
306 |
apply (simp (no_asm) add: real_add_commute) |
|
307 |
done |
|
308 |
||
309 |
lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)" |
|
310 |
apply (unfold complex_add_def) |
|
311 |
apply (simp (no_asm) add: real_add_assoc) |
|
312 |
done |
|
313 |
||
314 |
lemma complex_add_left_commute: "(x::complex) + (y + z) = y + (x + z)" |
|
315 |
apply (unfold complex_add_def) |
|
14334 | 316 |
apply (simp (no_asm) add: add_left_commute) |
14323 | 317 |
done |
318 |
||
319 |
lemmas complex_add_ac = complex_add_assoc complex_add_commute |
|
320 |
complex_add_left_commute |
|
321 |
||
322 |
lemma complex_add_zero_left: "(0::complex) + z = z" |
|
323 |
apply (unfold complex_add_def complex_zero_def) |
|
324 |
apply (simp (no_asm)) |
|
325 |
done |
|
326 |
declare complex_add_zero_left [simp] |
|
327 |
||
328 |
lemma complex_add_zero_right: "z + (0::complex) = z" |
|
329 |
apply (unfold complex_add_def complex_zero_def) |
|
330 |
apply (simp (no_asm)) |
|
331 |
done |
|
332 |
declare complex_add_zero_right [simp] |
|
333 |
||
334 |
lemma complex_add_minus_right_zero: |
|
335 |
"z + -z = (0::complex)" |
|
336 |
apply (unfold complex_add_def complex_minus_def complex_zero_def) |
|
337 |
apply (simp (no_asm)) |
|
338 |
done |
|
339 |
declare complex_add_minus_right_zero [simp] |
|
340 |
||
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
341 |
lemma complex_add_minus_left: |
14323 | 342 |
"-z + z = (0::complex)" |
343 |
apply (unfold complex_add_def complex_minus_def complex_zero_def) |
|
344 |
apply (simp (no_asm)) |
|
345 |
done |
|
346 |
||
347 |
lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)" |
|
348 |
apply (simp (no_asm) add: complex_add_assoc [symmetric]) |
|
349 |
done |
|
350 |
||
351 |
lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)" |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
352 |
by (simp add: complex_add_minus_left complex_add_assoc [symmetric]) |
14323 | 353 |
|
354 |
declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp] |
|
355 |
||
356 |
lemma complex_add_minus_eq_minus: "x + y = (0::complex) ==> x = -y" |
|
14334 | 357 |
by (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus) |
14323 | 358 |
|
359 |
lemma complex_minus_add_distrib: "-(x + y) = -x + -(y::complex)" |
|
14334 | 360 |
apply (rule_tac z = x in eq_Abs_complex) |
361 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 362 |
apply (auto simp add: complex_minus complex_add) |
363 |
done |
|
364 |
declare complex_minus_add_distrib [simp] |
|
365 |
||
366 |
lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)" |
|
14334 | 367 |
apply safe |
14323 | 368 |
apply (drule_tac f = "%t.-x + t" in arg_cong) |
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
369 |
apply (simp add: complex_add_minus_left complex_add_assoc [symmetric]) |
14323 | 370 |
done |
371 |
declare complex_add_left_cancel [iff] |
|
372 |
||
373 |
lemma complex_add_right_cancel: "(y + (x::complex)= z + x) = (y = z)" |
|
374 |
apply (simp (no_asm) add: complex_add_commute) |
|
375 |
done |
|
376 |
declare complex_add_right_cancel [simp] |
|
377 |
||
378 |
lemma complex_eq_minus_iff: "((x::complex) = y) = (0 = x + - y)" |
|
14334 | 379 |
apply safe |
380 |
apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto) |
|
14323 | 381 |
done |
382 |
||
383 |
lemma complex_eq_minus_iff2: "((x::complex) = y) = (x + - y = 0)" |
|
14334 | 384 |
apply safe |
385 |
apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto) |
|
14323 | 386 |
done |
387 |
||
388 |
lemma complex_diff_0: "(0::complex) - x = -x" |
|
389 |
apply (simp (no_asm) add: complex_diff_def) |
|
390 |
done |
|
391 |
||
392 |
lemma complex_diff_0_right: "x - (0::complex) = x" |
|
393 |
apply (simp (no_asm) add: complex_diff_def) |
|
394 |
done |
|
395 |
||
396 |
lemma complex_diff_self: "x - x = (0::complex)" |
|
397 |
apply (simp (no_asm) add: complex_diff_def) |
|
398 |
done |
|
399 |
||
400 |
declare complex_diff_0 [simp] complex_diff_0_right [simp] complex_diff_self [simp] |
|
401 |
||
402 |
lemma complex_diff: |
|
403 |
"Abs_complex(x1,y1) - Abs_complex(x2,y2) = Abs_complex(x1-x2,y1-y2)" |
|
404 |
apply (unfold complex_diff_def) |
|
405 |
apply (simp (no_asm) add: complex_add complex_minus) |
|
406 |
done |
|
407 |
||
408 |
lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)" |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
409 |
by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc) |
14323 | 410 |
|
411 |
||
412 |
subsection{*Multiplication*} |
|
413 |
||
414 |
lemma complex_mult: |
|
415 |
"Abs_complex(x1,y1) * Abs_complex(x2,y2) = |
|
416 |
Abs_complex(x1*x2 - y1*y2,x1*y2 + y1*x2)" |
|
417 |
apply (unfold complex_mult_def) |
|
418 |
apply (simp (no_asm)) |
|
419 |
done |
|
420 |
||
421 |
lemma complex_mult_commute: "(w::complex) * z = z * w" |
|
422 |
apply (unfold complex_mult_def) |
|
423 |
apply (simp (no_asm) add: real_mult_commute real_add_commute) |
|
424 |
done |
|
425 |
||
426 |
lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)" |
|
427 |
apply (unfold complex_mult_def) |
|
14334 | 428 |
apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_assoc right_diff_distrib right_distrib left_diff_distrib left_distrib mult_left_commute) |
14323 | 429 |
done |
430 |
||
431 |
lemma complex_mult_left_commute: "(x::complex) * (y * z) = y * (x * z)" |
|
432 |
apply (unfold complex_mult_def) |
|
14334 | 433 |
apply (simp (no_asm) add: complex_Re_Im_cancel_iff mult_left_commute right_diff_distrib right_distrib) |
14323 | 434 |
done |
435 |
||
436 |
lemmas complex_mult_ac = complex_mult_assoc complex_mult_commute |
|
437 |
complex_mult_left_commute |
|
438 |
||
439 |
lemma complex_mult_one_left: "(1::complex) * z = z" |
|
440 |
apply (unfold complex_one_def) |
|
14334 | 441 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 442 |
apply (simp (no_asm_simp) add: complex_mult) |
443 |
done |
|
444 |
declare complex_mult_one_left [simp] |
|
445 |
||
446 |
lemma complex_mult_one_right: "z * (1::complex) = z" |
|
447 |
apply (simp (no_asm) add: complex_mult_commute) |
|
448 |
done |
|
449 |
declare complex_mult_one_right [simp] |
|
450 |
||
451 |
lemma complex_mult_zero_left: "(0::complex) * z = 0" |
|
452 |
apply (unfold complex_zero_def) |
|
14334 | 453 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 454 |
apply (simp (no_asm_simp) add: complex_mult) |
455 |
done |
|
456 |
declare complex_mult_zero_left [simp] |
|
457 |
||
458 |
lemma complex_mult_zero_right: "z * 0 = (0::complex)" |
|
459 |
apply (simp (no_asm) add: complex_mult_commute) |
|
460 |
done |
|
461 |
declare complex_mult_zero_right [simp] |
|
462 |
||
463 |
lemma complex_divide_zero: "0 / z = (0::complex)" |
|
14334 | 464 |
by (unfold complex_divide_def, auto) |
14323 | 465 |
declare complex_divide_zero [simp] |
466 |
||
467 |
lemma complex_minus_mult_eq1: "-(x * y) = -x * (y::complex)" |
|
14334 | 468 |
apply (rule_tac z = x in eq_Abs_complex) |
469 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 470 |
apply (auto simp add: complex_mult complex_minus real_diff_def) |
471 |
done |
|
472 |
||
473 |
lemma complex_minus_mult_eq2: "-(x * y) = x * -(y::complex)" |
|
14334 | 474 |
apply (rule_tac z = x in eq_Abs_complex) |
475 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 476 |
apply (auto simp add: complex_mult complex_minus real_diff_def) |
477 |
done |
|
478 |
||
479 |
lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)" |
|
14334 | 480 |
apply (rule_tac z = z1 in eq_Abs_complex) |
481 |
apply (rule_tac z = z2 in eq_Abs_complex) |
|
482 |
apply (rule_tac z = w in eq_Abs_complex) |
|
483 |
apply (auto simp add: complex_mult complex_add left_distrib real_diff_def add_ac) |
|
14323 | 484 |
done |
485 |
||
486 |
lemma complex_add_mult_distrib2: "(w::complex) * (z1 + z2) = (w * z1) + (w * z2)" |
|
487 |
apply (rule_tac z1 = "z1 + z2" in complex_mult_commute [THEN ssubst]) |
|
488 |
apply (simp (no_asm) add: complex_add_mult_distrib) |
|
489 |
apply (simp (no_asm) add: complex_mult_commute) |
|
490 |
done |
|
491 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
492 |
lemma complex_zero_not_eq_one: "(0::complex) \<noteq> 1" |
14323 | 493 |
apply (unfold complex_zero_def complex_one_def) |
494 |
apply (simp (no_asm) add: complex_Re_Im_cancel_iff) |
|
495 |
done |
|
496 |
declare complex_zero_not_eq_one [simp] |
|
497 |
declare complex_zero_not_eq_one [THEN not_sym, simp] |
|
498 |
||
499 |
||
500 |
subsection{*Inverse*} |
|
501 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
502 |
lemma complex_inverse: |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
503 |
"inverse (Abs_complex(x,y)) = |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
504 |
Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))" |
14323 | 505 |
apply (unfold complex_inverse_def) |
506 |
apply (simp (no_asm)) |
|
507 |
done |
|
508 |
||
509 |
lemma COMPLEX_INVERSE_ZERO: "inverse 0 = (0::complex)" |
|
14334 | 510 |
by (unfold complex_inverse_def complex_zero_def, auto) |
14323 | 511 |
|
512 |
lemma COMPLEX_DIVISION_BY_ZERO: "a / (0::complex) = 0" |
|
513 |
apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO) |
|
514 |
done |
|
515 |
||
14335 | 516 |
instance complex :: division_by_zero |
517 |
proof |
|
518 |
fix x :: complex |
|
519 |
show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO) |
|
520 |
show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) |
|
521 |
qed |
|
522 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
523 |
lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1" |
14334 | 524 |
apply (rule_tac z = z in eq_Abs_complex) |
525 |
apply (auto simp add: complex_mult complex_inverse complex_one_def |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
526 |
complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac) |
14334 | 527 |
apply (drule_tac y = y in real_sum_squares_not_zero) |
528 |
apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto) |
|
14323 | 529 |
done |
530 |
declare complex_mult_inv_left [simp] |
|
531 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
532 |
lemma complex_mult_inv_right: "z \<noteq> (0::complex) ==> z * inverse(z) = 1" |
14334 | 533 |
by (auto intro: complex_mult_commute [THEN subst]) |
14323 | 534 |
declare complex_mult_inv_right [simp] |
535 |
||
14335 | 536 |
|
537 |
subsection {* The field of complex numbers *} |
|
538 |
||
539 |
instance complex :: field |
|
540 |
proof |
|
541 |
fix z u v w :: complex |
|
542 |
show "(u + v) + w = u + (v + w)" |
|
543 |
by (rule complex_add_assoc) |
|
544 |
show "z + w = w + z" |
|
545 |
by (rule complex_add_commute) |
|
546 |
show "0 + z = z" |
|
547 |
by (rule complex_add_zero_left) |
|
548 |
show "-z + z = 0" |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
549 |
by (rule complex_add_minus_left) |
14335 | 550 |
show "z - w = z + -w" |
551 |
by (simp add: complex_diff_def) |
|
552 |
show "(u * v) * w = u * (v * w)" |
|
553 |
by (rule complex_mult_assoc) |
|
554 |
show "z * w = w * z" |
|
555 |
by (rule complex_mult_commute) |
|
556 |
show "1 * z = z" |
|
557 |
by (rule complex_mult_one_left) |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
558 |
show "0 \<noteq> (1::complex)" |
14335 | 559 |
by (rule complex_zero_not_eq_one) |
560 |
show "(u + v) * w = u * w + v * w" |
|
561 |
by (rule complex_add_mult_distrib) |
|
14341
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
562 |
show "z+u = z+v ==> u=v" |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
563 |
proof - |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
564 |
assume eq: "z+u = z+v" |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
565 |
hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
566 |
thus "u = v" by (simp add: complex_add_minus_left) |
a09441bd4f1e
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents:
14335
diff
changeset
|
567 |
qed |
14335 | 568 |
assume neq: "w \<noteq> 0" |
569 |
thus "z / w = z * inverse w" |
|
570 |
by (simp add: complex_divide_def) |
|
571 |
show "inverse w * w = 1" |
|
572 |
by (simp add: neq complex_mult_inv_left) |
|
573 |
qed |
|
574 |
||
575 |
||
576 |
lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)" |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
577 |
apply (simp) |
14323 | 578 |
done |
579 |
||
580 |
subsection{*Embedding Properties for @{term complex_of_real} Map*} |
|
581 |
||
582 |
lemma inj_complex_of_real: "inj complex_of_real" |
|
583 |
apply (rule inj_onI) |
|
584 |
apply (auto dest: inj_Abs_complex [THEN injD] simp add: complex_of_real_def) |
|
585 |
done |
|
586 |
||
587 |
lemma complex_of_real_one: |
|
588 |
"complex_of_real 1 = 1" |
|
589 |
apply (unfold complex_one_def complex_of_real_def) |
|
590 |
apply (rule refl) |
|
591 |
done |
|
592 |
declare complex_of_real_one [simp] |
|
593 |
||
594 |
lemma complex_of_real_zero: |
|
595 |
"complex_of_real 0 = 0" |
|
596 |
apply (unfold complex_zero_def complex_of_real_def) |
|
597 |
apply (rule refl) |
|
598 |
done |
|
599 |
declare complex_of_real_zero [simp] |
|
600 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
601 |
lemma complex_of_real_eq_iff: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
602 |
"(complex_of_real x = complex_of_real y) = (x = y)" |
14334 | 603 |
by (auto dest: inj_complex_of_real [THEN injD]) |
14323 | 604 |
declare complex_of_real_eq_iff [iff] |
605 |
||
606 |
lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x" |
|
607 |
apply (simp (no_asm) add: complex_of_real_def complex_minus) |
|
608 |
done |
|
609 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
610 |
lemma complex_of_real_inverse: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
611 |
"complex_of_real(inverse x) = inverse(complex_of_real x)" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
612 |
apply (case_tac "x=0", simp) |
14334 | 613 |
apply (simp add: complex_inverse complex_of_real_def real_divide_def |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
614 |
inverse_mult_distrib power2_eq_square) |
14323 | 615 |
done |
616 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
617 |
lemma complex_of_real_add: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
618 |
"complex_of_real x + complex_of_real y = complex_of_real (x + y)" |
14323 | 619 |
apply (simp (no_asm) add: complex_add complex_of_real_def) |
620 |
done |
|
621 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
622 |
lemma complex_of_real_diff: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
623 |
"complex_of_real x - complex_of_real y = complex_of_real (x - y)" |
14323 | 624 |
apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add) |
625 |
done |
|
626 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
627 |
lemma complex_of_real_mult: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
628 |
"complex_of_real x * complex_of_real y = complex_of_real (x * y)" |
14323 | 629 |
apply (simp (no_asm) add: complex_mult complex_of_real_def) |
630 |
done |
|
631 |
||
632 |
lemma complex_of_real_divide: |
|
633 |
"complex_of_real x / complex_of_real y = complex_of_real(x/y)" |
|
634 |
apply (unfold complex_divide_def) |
|
635 |
apply (case_tac "y=0") |
|
636 |
apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO) |
|
637 |
apply (simp (no_asm_simp) add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def) |
|
638 |
done |
|
639 |
||
640 |
lemma complex_mod: "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)" |
|
641 |
apply (unfold cmod_def) |
|
642 |
apply (simp (no_asm)) |
|
643 |
done |
|
644 |
||
645 |
lemma complex_mod_zero: "cmod(0) = 0" |
|
646 |
apply (unfold cmod_def) |
|
647 |
apply (simp (no_asm)) |
|
648 |
done |
|
649 |
declare complex_mod_zero [simp] |
|
650 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
651 |
lemma complex_mod_one [simp]: "cmod(1) = 1" |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
652 |
by (simp add: cmod_def power2_eq_square) |
14323 | 653 |
|
654 |
lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x" |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
655 |
apply (simp add: complex_of_real_def power2_eq_square complex_mod) |
14323 | 656 |
done |
657 |
declare complex_mod_complex_of_real [simp] |
|
658 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
659 |
lemma complex_of_real_abs: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
660 |
"complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
661 |
by (simp) |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
662 |
|
14323 | 663 |
|
664 |
||
665 |
subsection{*Conjugation is an Automorphism*} |
|
666 |
||
667 |
lemma complex_cnj: "cnj (Abs_complex(x,y)) = Abs_complex(x,-y)" |
|
668 |
apply (unfold cnj_def) |
|
669 |
apply (simp (no_asm)) |
|
670 |
done |
|
671 |
||
672 |
lemma inj_cnj: "inj cnj" |
|
673 |
apply (rule inj_onI) |
|
674 |
apply (auto simp add: cnj_def Abs_complex_cancel_iff complex_Re_Im_cancel_iff) |
|
675 |
done |
|
676 |
||
677 |
lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)" |
|
14334 | 678 |
by (auto dest: inj_cnj [THEN injD]) |
14323 | 679 |
declare complex_cnj_cancel_iff [simp] |
680 |
||
681 |
lemma complex_cnj_cnj: "cnj (cnj z) = z" |
|
682 |
apply (unfold cnj_def) |
|
683 |
apply (simp (no_asm)) |
|
684 |
done |
|
685 |
declare complex_cnj_cnj [simp] |
|
686 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
687 |
lemma complex_cnj_complex_of_real: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
688 |
"cnj (complex_of_real x) = complex_of_real x" |
14323 | 689 |
apply (unfold complex_of_real_def) |
690 |
apply (simp (no_asm) add: complex_cnj) |
|
691 |
done |
|
692 |
declare complex_cnj_complex_of_real [simp] |
|
693 |
||
694 |
lemma complex_mod_cnj: "cmod (cnj z) = cmod z" |
|
14334 | 695 |
apply (rule_tac z = z in eq_Abs_complex) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
696 |
apply (simp (no_asm_simp) add: complex_cnj complex_mod power2_eq_square) |
14323 | 697 |
done |
698 |
declare complex_mod_cnj [simp] |
|
699 |
||
700 |
lemma complex_cnj_minus: "cnj (-z) = - cnj z" |
|
701 |
apply (unfold cnj_def) |
|
702 |
apply (simp (no_asm) add: complex_minus complex_Re_minus complex_Im_minus) |
|
703 |
done |
|
704 |
||
705 |
lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)" |
|
14334 | 706 |
apply (rule_tac z = z in eq_Abs_complex) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
707 |
apply (simp (no_asm_simp) add: complex_cnj complex_inverse power2_eq_square) |
14323 | 708 |
done |
709 |
||
710 |
lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)" |
|
14334 | 711 |
apply (rule_tac z = w in eq_Abs_complex) |
712 |
apply (rule_tac z = z in eq_Abs_complex) |
|
14323 | 713 |
apply (simp (no_asm_simp) add: complex_cnj complex_add) |
714 |
done |
|
715 |
||
716 |
lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)" |
|
717 |
apply (unfold complex_diff_def) |
|
718 |
apply (simp (no_asm) add: complex_cnj_add complex_cnj_minus) |
|
719 |
done |
|
720 |
||
721 |
lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)" |
|
14334 | 722 |
apply (rule_tac z = w in eq_Abs_complex) |
723 |
apply (rule_tac z = z in eq_Abs_complex) |
|
14323 | 724 |
apply (simp (no_asm_simp) add: complex_cnj complex_mult) |
725 |
done |
|
726 |
||
727 |
lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)" |
|
728 |
apply (unfold complex_divide_def) |
|
729 |
apply (simp (no_asm) add: complex_cnj_mult complex_cnj_inverse) |
|
730 |
done |
|
731 |
||
732 |
lemma complex_cnj_one: "cnj 1 = 1" |
|
733 |
apply (unfold cnj_def complex_one_def) |
|
734 |
apply (simp (no_asm)) |
|
735 |
done |
|
736 |
declare complex_cnj_one [simp] |
|
737 |
||
738 |
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))" |
|
14334 | 739 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 740 |
apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def) |
741 |
done |
|
742 |
||
743 |
lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii" |
|
14334 | 744 |
apply (rule_tac z = z in eq_Abs_complex) |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
745 |
apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
746 |
complex_minus i_def complex_mult) |
14323 | 747 |
done |
748 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
749 |
lemma complex_cnj_zero [simp]: "cnj 0 = 0" |
14334 | 750 |
by (simp add: cnj_def complex_zero_def) |
14323 | 751 |
|
752 |
lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)" |
|
14334 | 753 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 754 |
apply (auto simp add: complex_zero_def complex_cnj) |
755 |
done |
|
756 |
declare complex_cnj_zero_iff [iff] |
|
757 |
||
758 |
lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)" |
|
14334 | 759 |
apply (rule_tac z = z in eq_Abs_complex) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
760 |
apply (auto simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square) |
14323 | 761 |
done |
762 |
||
763 |
||
764 |
subsection{*Algebra*} |
|
765 |
||
766 |
lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))" |
|
767 |
apply (unfold complex_zero_def) |
|
14334 | 768 |
apply (rule_tac z = x in eq_Abs_complex) |
769 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 770 |
apply (auto simp add: complex_add) |
771 |
done |
|
772 |
declare complex_add_left_cancel_zero [simp] |
|
773 |
||
774 |
lemma complex_diff_mult_distrib: |
|
775 |
"((z1::complex) - z2) * w = (z1 * w) - (z2 * w)" |
|
776 |
apply (unfold complex_diff_def) |
|
777 |
apply (simp (no_asm) add: complex_add_mult_distrib) |
|
778 |
done |
|
779 |
||
780 |
lemma complex_diff_mult_distrib2: |
|
781 |
"(w::complex) * (z1 - z2) = (w * z1) - (w * z2)" |
|
782 |
apply (unfold complex_diff_def) |
|
783 |
apply (simp (no_asm) add: complex_add_mult_distrib2) |
|
784 |
done |
|
785 |
||
786 |
||
787 |
subsection{*Modulus*} |
|
788 |
||
789 |
lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)" |
|
14334 | 790 |
apply (rule_tac z = x in eq_Abs_complex) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
791 |
apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square) |
14323 | 792 |
done |
793 |
declare complex_mod_eq_zero_cancel [simp] |
|
794 |
||
795 |
lemma complex_mod_complex_of_real_of_nat: "cmod (complex_of_real(real (n::nat))) = real n" |
|
796 |
apply (simp (no_asm)) |
|
797 |
done |
|
798 |
declare complex_mod_complex_of_real_of_nat [simp] |
|
799 |
||
800 |
lemma complex_mod_minus: "cmod (-x) = cmod(x)" |
|
14334 | 801 |
apply (rule_tac z = x in eq_Abs_complex) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
802 |
apply (simp (no_asm_simp) add: complex_mod complex_minus power2_eq_square) |
14323 | 803 |
done |
804 |
declare complex_mod_minus [simp] |
|
805 |
||
806 |
lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" |
|
14334 | 807 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 808 |
apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult); |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
809 |
apply (simp (no_asm) add: power2_eq_square real_abs_def) |
14323 | 810 |
done |
811 |
||
812 |
lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2" |
|
14334 | 813 |
by (unfold cmod_def, auto) |
14323 | 814 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
815 |
lemma complex_mod_ge_zero: "0 \<le> cmod x" |
14323 | 816 |
apply (unfold cmod_def) |
817 |
apply (auto intro: real_sqrt_ge_zero) |
|
818 |
done |
|
819 |
declare complex_mod_ge_zero [simp] |
|
820 |
||
821 |
lemma abs_cmod_cancel: "abs(cmod x) = cmod x" |
|
14334 | 822 |
by (auto intro: abs_eqI1) |
14323 | 823 |
declare abs_cmod_cancel [simp] |
824 |
||
825 |
lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)" |
|
14334 | 826 |
apply (rule_tac z = x in eq_Abs_complex) |
827 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 828 |
apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc) |
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
829 |
apply (rule_tac n = 1 in power_inject_base) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
830 |
apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc) |
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
831 |
apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac) |
14323 | 832 |
done |
833 |
||
834 |
lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" |
|
14334 | 835 |
apply (rule_tac z = x in eq_Abs_complex) |
836 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 837 |
apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc) |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
838 |
apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) |
14323 | 839 |
done |
840 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
841 |
lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)" |
14334 | 842 |
apply (rule_tac z = x in eq_Abs_complex) |
843 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14323 | 844 |
apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc) |
845 |
done |
|
846 |
declare complex_Re_mult_cnj_le_cmod [simp] |
|
847 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
848 |
lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)" |
14334 | 849 |
apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod) |
14323 | 850 |
apply (simp add: complex_mod_mult) |
851 |
done |
|
852 |
declare complex_Re_mult_cnj_le_cmod2 [simp] |
|
853 |
||
854 |
lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
855 |
apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square) |
14323 | 856 |
done |
857 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
858 |
lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2" |
14323 | 859 |
apply (simp (no_asm) add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric]) |
860 |
done |
|
861 |
declare complex_mod_triangle_squared [simp] |
|
862 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
863 |
lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x" |
14323 | 864 |
apply (rule order_trans [OF _ complex_mod_ge_zero]) |
865 |
apply (simp (no_asm)) |
|
866 |
done |
|
867 |
declare complex_mod_minus_le_complex_mod [simp] |
|
868 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
869 |
lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)" |
14334 | 870 |
apply (rule_tac n = 1 in realpow_increasing) |
14323 | 871 |
apply (auto intro: order_trans [OF _ complex_mod_ge_zero] |
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
872 |
simp add: power2_eq_square [symmetric]) |
14323 | 873 |
done |
874 |
declare complex_mod_triangle_ineq [simp] |
|
875 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
876 |
lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a" |
14334 | 877 |
apply (cut_tac x1 = b and y1 = a and c = "-cmod b" |
878 |
in complex_mod_triangle_ineq [THEN add_right_mono]) |
|
14323 | 879 |
apply (simp (no_asm)) |
880 |
done |
|
881 |
declare complex_mod_triangle_ineq2 [simp] |
|
882 |
||
883 |
lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)" |
|
14334 | 884 |
apply (rule_tac z = x in eq_Abs_complex) |
885 |
apply (rule_tac z = y in eq_Abs_complex) |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
886 |
apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac) |
14323 | 887 |
done |
888 |
||
889 |
lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s" |
|
14334 | 890 |
by (auto intro: order_le_less_trans complex_mod_triangle_ineq) |
14323 | 891 |
|
892 |
lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" |
|
14334 | 893 |
by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) |
14323 | 894 |
|
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
895 |
lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \<le> cmod(a + b)" |
14323 | 896 |
apply (rule linorder_cases [of "cmod(a)" "cmod (b)"]) |
897 |
apply auto |
|
14334 | 898 |
apply (rule order_trans [of _ 0], rule order_less_imp_le) |
899 |
apply (simp add: compare_rls, simp) |
|
14323 | 900 |
apply (simp add: compare_rls) |
901 |
apply (rule complex_mod_minus [THEN subst]) |
|
902 |
apply (rule order_trans) |
|
903 |
apply (rule_tac [2] complex_mod_triangle_ineq) |
|
904 |
apply (auto simp add: complex_add_ac) |
|
905 |
done |
|
906 |
declare complex_mod_diff_ineq [simp] |
|
907 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
908 |
lemma complex_Re_le_cmod: "Re z \<le> cmod z" |
14334 | 909 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 910 |
apply (auto simp add: complex_mod simp del: realpow_Suc) |
911 |
done |
|
912 |
declare complex_Re_le_cmod [simp] |
|
913 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
914 |
lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z" |
14334 | 915 |
apply (cut_tac x = z in complex_mod_ge_zero) |
916 |
apply (drule order_le_imp_less_or_eq, auto) |
|
14323 | 917 |
done |
918 |
||
919 |
||
920 |
subsection{*A Few More Theorems*} |
|
921 |
||
922 |
lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)" |
|
923 |
apply (case_tac "x=0", simp add: COMPLEX_INVERSE_ZERO) |
|
924 |
apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1]) |
|
925 |
apply (auto simp add: complex_mod_mult [symmetric]) |
|
926 |
done |
|
927 |
||
928 |
lemma complex_mod_divide: |
|
929 |
"cmod(x/y) = cmod(x)/(cmod y)" |
|
930 |
apply (unfold complex_divide_def real_divide_def) |
|
931 |
apply (auto simp add: complex_mod_mult complex_mod_inverse) |
|
932 |
done |
|
933 |
||
934 |
lemma complex_inverse_divide: |
|
935 |
"inverse(x/y) = y/(x::complex)" |
|
936 |
apply (unfold complex_divide_def) |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
937 |
apply (auto simp add: inverse_mult_distrib complex_mult_commute) |
14323 | 938 |
done |
939 |
declare complex_inverse_divide [simp] |
|
940 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
941 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
942 |
subsection{*Exponentiation*} |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
943 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
944 |
primrec |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
945 |
complexpow_0: "z ^ 0 = 1" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
946 |
complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
947 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
948 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
949 |
instance complex :: ringpower |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
950 |
proof |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
951 |
fix z :: complex |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
952 |
fix n :: nat |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
953 |
show "z^0 = 1" by simp |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
954 |
show "z^(Suc n) = z * (z^n)" by simp |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
955 |
qed |
14323 | 956 |
|
957 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
958 |
lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n" |
14323 | 959 |
apply (induct_tac "n") |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
960 |
apply (auto simp add: complex_of_real_mult [symmetric]) |
14323 | 961 |
done |
962 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
963 |
lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n" |
14323 | 964 |
apply (induct_tac "n") |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
965 |
apply (auto simp add: complex_cnj_mult) |
14323 | 966 |
done |
967 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
968 |
lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
969 |
apply (induct_tac "n") |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
970 |
apply (auto simp add: complex_mod_mult) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
971 |
done |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
972 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
973 |
lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
974 |
by (induct_tac "n", auto) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
975 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
976 |
lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
977 |
by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
978 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
979 |
lemma complex_i_not_zero [simp]: "ii \<noteq> 0" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
980 |
by (unfold i_def complex_zero_def, auto) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
981 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
982 |
|
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
983 |
subsection{*The Function @{term sgn}*} |
14323 | 984 |
|
985 |
lemma sgn_zero: "sgn 0 = 0" |
|
986 |
apply (unfold sgn_def) |
|
987 |
apply (simp (no_asm)) |
|
988 |
done |
|
989 |
declare sgn_zero [simp] |
|
990 |
||
991 |
lemma sgn_one: "sgn 1 = 1" |
|
992 |
apply (unfold sgn_def) |
|
993 |
apply (simp (no_asm)) |
|
994 |
done |
|
995 |
declare sgn_one [simp] |
|
996 |
||
997 |
lemma sgn_minus: "sgn (-z) = - sgn(z)" |
|
14334 | 998 |
by (unfold sgn_def, auto) |
14323 | 999 |
|
1000 |
lemma sgn_eq: |
|
1001 |
"sgn z = z / complex_of_real (cmod z)" |
|
1002 |
apply (unfold sgn_def) |
|
1003 |
apply (simp (no_asm)) |
|
1004 |
done |
|
1005 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1006 |
lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)" |
14334 | 1007 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1008 |
apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) |
1009 |
done |
|
1010 |
||
1011 |
lemma Re_complex_i: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x" |
|
14334 | 1012 |
by (auto simp add: complex_of_real_def i_def complex_mult complex_add) |
14323 | 1013 |
declare Re_complex_i [simp] |
1014 |
||
1015 |
lemma Im_complex_i: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y" |
|
14334 | 1016 |
by (auto simp add: complex_of_real_def i_def complex_mult complex_add) |
14323 | 1017 |
declare Im_complex_i [simp] |
1018 |
||
1019 |
lemma i_mult_eq: "ii * ii = complex_of_real (-1)" |
|
1020 |
apply (unfold i_def complex_of_real_def) |
|
1021 |
apply (auto simp add: complex_mult complex_add) |
|
1022 |
done |
|
1023 |
||
1024 |
lemma i_mult_eq2: "ii * ii = -(1::complex)" |
|
1025 |
apply (unfold i_def complex_one_def) |
|
1026 |
apply (simp (no_asm) add: complex_mult complex_minus) |
|
1027 |
done |
|
1028 |
declare i_mult_eq2 [simp] |
|
1029 |
||
1030 |
lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) = |
|
1031 |
sqrt (x ^ 2 + y ^ 2)" |
|
1032 |
apply (auto simp add: complex_mult complex_add i_def complex_of_real_def cmod_def) |
|
1033 |
done |
|
1034 |
||
1035 |
lemma complex_eq_Re_eq: |
|
1036 |
"complex_of_real xa + ii * complex_of_real ya = |
|
1037 |
complex_of_real xb + ii * complex_of_real yb |
|
1038 |
==> xa = xb" |
|
1039 |
apply (unfold complex_of_real_def i_def) |
|
1040 |
apply (auto simp add: complex_mult complex_add) |
|
1041 |
done |
|
1042 |
||
1043 |
lemma complex_eq_Im_eq: |
|
1044 |
"complex_of_real xa + ii * complex_of_real ya = |
|
1045 |
complex_of_real xb + ii * complex_of_real yb |
|
1046 |
==> ya = yb" |
|
1047 |
apply (unfold complex_of_real_def i_def) |
|
1048 |
apply (auto simp add: complex_mult complex_add) |
|
1049 |
done |
|
1050 |
||
1051 |
lemma complex_eq_cancel_iff: "(complex_of_real xa + ii * complex_of_real ya = |
|
1052 |
complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))" |
|
1053 |
apply (auto intro: complex_eq_Im_eq complex_eq_Re_eq) |
|
1054 |
done |
|
1055 |
declare complex_eq_cancel_iff [iff] |
|
1056 |
||
1057 |
lemma complex_eq_cancel_iffA: "(complex_of_real xa + complex_of_real ya * ii = |
|
1058 |
complex_of_real xb + complex_of_real yb * ii ) = ((xa = xb) & (ya = yb))" |
|
1059 |
apply (auto simp add: complex_mult_commute) |
|
1060 |
done |
|
1061 |
declare complex_eq_cancel_iffA [iff] |
|
1062 |
||
1063 |
lemma complex_eq_cancel_iffB: "(complex_of_real xa + complex_of_real ya * ii = |
|
1064 |
complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))" |
|
1065 |
apply (auto simp add: complex_mult_commute) |
|
1066 |
done |
|
1067 |
declare complex_eq_cancel_iffB [iff] |
|
1068 |
||
1069 |
lemma complex_eq_cancel_iffC: "(complex_of_real xa + ii * complex_of_real ya = |
|
1070 |
complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))" |
|
1071 |
apply (auto simp add: complex_mult_commute) |
|
1072 |
done |
|
1073 |
declare complex_eq_cancel_iffC [iff] |
|
1074 |
||
1075 |
lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y = |
|
1076 |
complex_of_real xa) = (x = xa & y = 0)" |
|
14334 | 1077 |
apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff) |
14323 | 1078 |
apply (simp del: complex_eq_cancel_iff) |
1079 |
done |
|
1080 |
declare complex_eq_cancel_iff2 [simp] |
|
1081 |
||
1082 |
lemma complex_eq_cancel_iff2a: "(complex_of_real x + complex_of_real y * ii = |
|
1083 |
complex_of_real xa) = (x = xa & y = 0)" |
|
1084 |
apply (auto simp add: complex_mult_commute) |
|
1085 |
done |
|
1086 |
declare complex_eq_cancel_iff2a [simp] |
|
1087 |
||
1088 |
lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y = |
|
1089 |
ii * complex_of_real ya) = (x = 0 & y = ya)" |
|
14334 | 1090 |
apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff) |
14323 | 1091 |
apply (simp del: complex_eq_cancel_iff) |
1092 |
done |
|
1093 |
declare complex_eq_cancel_iff3 [simp] |
|
1094 |
||
1095 |
lemma complex_eq_cancel_iff3a: "(complex_of_real x + complex_of_real y * ii = |
|
1096 |
ii * complex_of_real ya) = (x = 0 & y = ya)" |
|
1097 |
apply (auto simp add: complex_mult_commute) |
|
1098 |
done |
|
1099 |
declare complex_eq_cancel_iff3a [simp] |
|
1100 |
||
1101 |
lemma complex_split_Re_zero: |
|
1102 |
"complex_of_real x + ii * complex_of_real y = 0 |
|
1103 |
==> x = 0" |
|
1104 |
apply (unfold complex_of_real_def i_def complex_zero_def) |
|
1105 |
apply (auto simp add: complex_mult complex_add) |
|
1106 |
done |
|
1107 |
||
1108 |
lemma complex_split_Im_zero: |
|
1109 |
"complex_of_real x + ii * complex_of_real y = 0 |
|
1110 |
==> y = 0" |
|
1111 |
apply (unfold complex_of_real_def i_def complex_zero_def) |
|
1112 |
apply (auto simp add: complex_mult complex_add) |
|
1113 |
done |
|
1114 |
||
1115 |
lemma Re_sgn: |
|
1116 |
"Re(sgn z) = Re(z)/cmod z" |
|
1117 |
apply (unfold sgn_def complex_divide_def) |
|
14334 | 1118 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1119 |
apply (auto simp add: complex_of_real_inverse [symmetric]) |
1120 |
apply (auto simp add: complex_of_real_def complex_mult real_divide_def) |
|
1121 |
done |
|
1122 |
declare Re_sgn [simp] |
|
1123 |
||
1124 |
lemma Im_sgn: |
|
1125 |
"Im(sgn z) = Im(z)/cmod z" |
|
1126 |
apply (unfold sgn_def complex_divide_def) |
|
14334 | 1127 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1128 |
apply (auto simp add: complex_of_real_inverse [symmetric]) |
1129 |
apply (auto simp add: complex_of_real_def complex_mult real_divide_def) |
|
1130 |
done |
|
1131 |
declare Im_sgn [simp] |
|
1132 |
||
1133 |
lemma complex_inverse_complex_split: |
|
1134 |
"inverse(complex_of_real x + ii * complex_of_real y) = |
|
1135 |
complex_of_real(x/(x ^ 2 + y ^ 2)) - |
|
1136 |
ii * complex_of_real(y/(x ^ 2 + y ^ 2))" |
|
1137 |
apply (unfold complex_of_real_def i_def) |
|
1138 |
apply (auto simp add: complex_mult complex_add complex_diff_def complex_minus complex_inverse real_divide_def) |
|
1139 |
done |
|
1140 |
||
1141 |
(*----------------------------------------------------------------------------*) |
|
1142 |
(* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) |
|
1143 |
(* many of the theorems are not used - so should they be kept? *) |
|
1144 |
(*----------------------------------------------------------------------------*) |
|
1145 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1146 |
lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1147 |
by (auto simp add: complex_zero_def complex_of_real_def) |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1148 |
|
14323 | 1149 |
lemma Re_mult_i_eq: |
1150 |
"Re (ii * complex_of_real y) = 0" |
|
1151 |
apply (unfold i_def complex_of_real_def) |
|
1152 |
apply (auto simp add: complex_mult) |
|
1153 |
done |
|
1154 |
declare Re_mult_i_eq [simp] |
|
1155 |
||
1156 |
lemma Im_mult_i_eq: |
|
1157 |
"Im (ii * complex_of_real y) = y" |
|
1158 |
apply (unfold i_def complex_of_real_def) |
|
1159 |
apply (auto simp add: complex_mult) |
|
1160 |
done |
|
1161 |
declare Im_mult_i_eq [simp] |
|
1162 |
||
1163 |
lemma complex_mod_mult_i: |
|
1164 |
"cmod (ii * complex_of_real y) = abs y" |
|
1165 |
apply (unfold i_def complex_of_real_def) |
|
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset
|
1166 |
apply (auto simp add: complex_mult complex_mod power2_eq_square) |
14323 | 1167 |
done |
1168 |
declare complex_mod_mult_i [simp] |
|
1169 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1170 |
lemma cos_arg_i_mult_zero_pos: |
14323 | 1171 |
"0 < y ==> cos (arg(ii * complex_of_real y)) = 0" |
1172 |
apply (unfold arg_def) |
|
1173 |
apply (auto simp add: abs_eqI2) |
|
14334 | 1174 |
apply (rule_tac a = "pi/2" in someI2, auto) |
1175 |
apply (rule order_less_trans [of _ 0], auto) |
|
14323 | 1176 |
done |
1177 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1178 |
lemma cos_arg_i_mult_zero_neg: |
14323 | 1179 |
"y < 0 ==> cos (arg(ii * complex_of_real y)) = 0" |
1180 |
apply (unfold arg_def) |
|
1181 |
apply (auto simp add: abs_minus_eqI2) |
|
14334 | 1182 |
apply (rule_tac a = "- pi/2" in someI2, auto) |
1183 |
apply (rule order_trans [of _ 0], auto) |
|
14323 | 1184 |
done |
1185 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1186 |
lemma cos_arg_i_mult_zero [simp] |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1187 |
: "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0" |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1188 |
by (cut_tac x = y and y = 0 in linorder_less_linear, |
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1189 |
auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg) |
14323 | 1190 |
|
1191 |
||
1192 |
subsection{*Finally! Polar Form for Complex Numbers*} |
|
1193 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1194 |
lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * |
14323 | 1195 |
(complex_of_real(cos a) + ii * complex_of_real(sin a))" |
14334 | 1196 |
apply (cut_tac z = z in complex_split) |
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1197 |
apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac) |
14323 | 1198 |
done |
1199 |
||
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset
|
1200 |
lemma rcis_Ex: "\<exists>r a. z = rcis r a" |
14323 | 1201 |
apply (unfold rcis_def cis_def) |
1202 |
apply (rule complex_split_polar) |
|
1203 |
done |
|
1204 |
||
1205 |
lemma Re_complex_polar: "Re(complex_of_real r * |
|
1206 |
(complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a" |
|
1207 |
apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac) |
|
1208 |
done |
|
1209 |
declare Re_complex_polar [simp] |
|
1210 |
||
1211 |
lemma Re_rcis: "Re(rcis r a) = r * cos a" |
|
14334 | 1212 |
by (unfold rcis_def cis_def, auto) |
14323 | 1213 |
declare Re_rcis [simp] |
1214 |
||
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1215 |
lemma Im_complex_polar [simp]: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1216 |
"Im(complex_of_real r * |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1217 |
(complex_of_real(cos a) + ii * complex_of_real(sin a))) = |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1218 |
r * sin a" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1219 |
by (auto simp add: complex_add_mult_distrib2 complex_of_real_mult mult_ac) |
14323 | 1220 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1221 |
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" |
14334 | 1222 |
by (unfold rcis_def cis_def, auto) |
14323 | 1223 |
|
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1224 |
lemma complex_mod_complex_polar [simp]: |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1225 |
"cmod (complex_of_real r * |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1226 |
(complex_of_real(cos a) + ii * complex_of_real(sin a))) = |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1227 |
abs r" |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1228 |
by (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1229 |
right_distrib [symmetric] power_mult_distrib mult_ac |
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset
|
1230 |
simp del: realpow_Suc) |
14323 | 1231 |
|
1232 |
lemma complex_mod_rcis: "cmod(rcis r a) = abs r" |
|
14334 | 1233 |
by (unfold rcis_def cis_def, auto) |
14323 | 1234 |
declare complex_mod_rcis [simp] |
1235 |
||
1236 |
lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" |
|
1237 |
apply (unfold cmod_def) |
|
1238 |
apply (rule real_sqrt_eq_iff [THEN iffD2]) |
|
1239 |
apply (auto simp add: complex_mult_cnj) |
|
1240 |
done |
|
1241 |
||
1242 |
lemma complex_Re_cnj: "Re(cnj z) = Re z" |
|
14334 | 1243 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1244 |
apply (auto simp add: complex_cnj) |
1245 |
done |
|
1246 |
declare complex_Re_cnj [simp] |
|
1247 |
||
1248 |
lemma complex_Im_cnj: "Im(cnj z) = - Im z" |
|
14334 | 1249 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1250 |
apply (auto simp add: complex_cnj) |
1251 |
done |
|
1252 |
declare complex_Im_cnj [simp] |
|
1253 |
||
1254 |
lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0" |
|
14334 | 1255 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1256 |
apply (auto simp add: complex_cnj complex_mult) |
1257 |
done |
|
1258 |
declare complex_In_mult_cnj_zero [simp] |
|
1259 |
||
1260 |
lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" |
|
14334 | 1261 |
apply (rule_tac z = z in eq_Abs_complex) |
1262 |
apply (rule_tac z = w in eq_Abs_complex) |
|
14323 | 1263 |
apply (auto simp add: complex_mult) |
1264 |
done |
|
1265 |
||
1266 |
lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c" |
|
1267 |
apply (unfold complex_of_real_def) |
|
14334 | 1268 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1269 |
apply (auto simp add: complex_mult) |
1270 |
done |
|
1271 |
declare complex_Re_mult_complex_of_real [simp] |
|
1272 |
||
1273 |
lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c" |
|
1274 |
apply (unfold complex_of_real_def) |
|
14334 | 1275 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1276 |
apply (auto simp add: complex_mult) |
1277 |
done |
|
1278 |
declare complex_Im_mult_complex_of_real [simp] |
|
1279 |
||
1280 |
lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)" |
|
1281 |
apply (unfold complex_of_real_def) |
|
14334 | 1282 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1283 |
apply (auto simp add: complex_mult) |
1284 |
done |
|
1285 |
declare complex_Re_mult_complex_of_real2 [simp] |
|
1286 |
||
1287 |
lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)" |
|
1288 |
apply (unfold complex_of_real_def) |
|
14334 | 1289 |
apply (rule_tac z = z in eq_Abs_complex) |
14323 | 1290 |
apply (auto simp add: complex_mult) |
1291 |
done |
|
1292 |
declare complex_Im_mult_complex_of_real2 [simp] |
|
1293 |
||
1294 |
(*---------------------------------------------------------------------------*) |
|
1295 |
(* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *) |
|
1296 |
(*---------------------------------------------------------------------------*) |
|
1297 |
||
1298 |
lemma cis_rcis_eq: "cis a = rcis 1 a" |
|
1299 |
apply (unfold rcis_def) |
|
1300 |
apply (simp (no_asm)) |
|
1301 |
done |
|
1302 |
||
27724f528f82
converting Complex/Complex.ML to Isar
paulson |