author  huffman 
Sat, 16 Sep 2006 19:14:37 +0200  
changeset 20556  2e8227b81bf1 
parent 20485  3078fd2eec7b 
child 20557  81dd3679f92c 
permissions  rwrr 
13957  1 
(* Title: Complex.thy 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

2 
ID: $Id$ 
13957  3 
Author: Jacques D. Fleuriot 
4 
Copyright: 2001 University of Edinburgh 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 
13957  6 
*) 
7 

14377  8 
header {* Complex Numbers: Rectangular and Polar Representations *} 
14373  9 

15131  10 
theory Complex 
15140  11 
imports "../Hyperreal/HLog" 
15131  12 
begin 
13957  13 

14373  14 
datatype complex = Complex real real 
13957  15 

14691  16 
instance complex :: "{zero, one, plus, times, minus, inverse, power}" .. 
13957  17 

18 
consts 

14373  19 
"ii" :: complex ("\<i>") 
20 

21 
consts Re :: "complex => real" 

22 
primrec "Re (Complex x y) = x" 

23 

24 
consts Im :: "complex => real" 

25 
primrec "Im (Complex x y) = y" 

26 

27 
lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" 

28 
by (induct z) simp 

13957  29 

19765  30 
definition 
13957  31 

32 
(* modulus *) 

33 

14323  34 
cmod :: "complex => real" 
19765  35 
"cmod z = sqrt(Re(z) ^ 2 + Im(z) ^ 2)" 
13957  36 

14323  37 
(* injection from reals *) 
38 

39 
complex_of_real :: "real => complex" 

19765  40 
"complex_of_real r = Complex r 0" 
14323  41 

13957  42 
(* complex conjugate *) 
43 

14323  44 
cnj :: "complex => complex" 
19765  45 
"cnj z = Complex (Re z) (Im z)" 
13957  46 

14323  47 
(* Argand *) 
13957  48 

14323  49 
sgn :: "complex => complex" 
19765  50 
"sgn z = z / complex_of_real(cmod z)" 
13957  51 

14323  52 
arg :: "complex => real" 
19765  53 
"arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & pi < a & a \<le> pi)" 
14323  54 

13957  55 

14323  56 
defs (overloaded) 
57 

58 
complex_zero_def: 

14373  59 
"0 == Complex 0 0" 
13957  60 

14323  61 
complex_one_def: 
14373  62 
"1 == Complex 1 0" 
14323  63 

14373  64 
i_def: "ii == Complex 0 1" 
14323  65 

14373  66 
complex_minus_def: " z == Complex ( Re z) ( Im z)" 
14323  67 

68 
complex_inverse_def: 

14373  69 
"inverse z == 
70 
Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) ( Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))" 

13957  71 

14323  72 
complex_add_def: 
14373  73 
"z + w == Complex (Re z + Re w) (Im z + Im w)" 
13957  74 

14323  75 
complex_diff_def: 
14373  76 
"z  w == z +  (w::complex)" 
13957  77 

14374  78 
complex_mult_def: 
14373  79 
"z * w == Complex (Re z * Re w  Im z * Im w) (Re z * Im w + Im z * Re w)" 
13957  80 

14373  81 
complex_divide_def: "w / (z::complex) == w * inverse z" 
14323  82 

13957  83 

19765  84 
definition 
13957  85 

86 
(* abbreviation for (cos a + i sin a) *) 

14323  87 
cis :: "real => complex" 
19765  88 
"cis a = Complex (cos a) (sin a)" 
13957  89 

90 
(* abbreviation for r*(cos a + i sin a) *) 

14323  91 
rcis :: "[real, real] => complex" 
19765  92 
"rcis r a = complex_of_real r * cis a" 
13957  93 

94 
(* e ^ (x + iy) *) 

14323  95 
expi :: "complex => complex" 
19765  96 
"expi z = complex_of_real(exp (Re z)) * cis (Im z)" 
14323  97 

98 

14373  99 
lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w" 
100 
by (induct z, induct w) simp 

14323  101 

14374  102 
lemma Re [simp]: "Re(Complex x y) = x" 
14373  103 
by simp 
14323  104 

14374  105 
lemma Im [simp]: "Im(Complex x y) = y" 
14373  106 
by simp 
14323  107 

108 
lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))" 

14373  109 
by (induct w, induct z, simp) 
14323  110 

14374  111 
lemma complex_Re_zero [simp]: "Re 0 = 0" 
112 
by (simp add: complex_zero_def) 

113 

114 
lemma complex_Im_zero [simp]: "Im 0 = 0" 

14373  115 
by (simp add: complex_zero_def) 
14323  116 

14374  117 
lemma complex_Re_one [simp]: "Re 1 = 1" 
118 
by (simp add: complex_one_def) 

14323  119 

14374  120 
lemma complex_Im_one [simp]: "Im 1 = 0" 
14373  121 
by (simp add: complex_one_def) 
14323  122 

14374  123 
lemma complex_Re_i [simp]: "Re(ii) = 0" 
14373  124 
by (simp add: i_def) 
14323  125 

14374  126 
lemma complex_Im_i [simp]: "Im(ii) = 1" 
14373  127 
by (simp add: i_def) 
14323  128 

14374  129 
lemma Re_complex_of_real [simp]: "Re(complex_of_real z) = z" 
14373  130 
by (simp add: complex_of_real_def) 
14323  131 

14374  132 
lemma Im_complex_of_real [simp]: "Im(complex_of_real z) = 0" 
14373  133 
by (simp add: complex_of_real_def) 
14323  134 

135 

14374  136 
subsection{*Unary Minus*} 
14323  137 

14377  138 
lemma complex_minus [simp]: " (Complex x y) = Complex (x) (y)" 
14373  139 
by (simp add: complex_minus_def) 
14323  140 

14374  141 
lemma complex_Re_minus [simp]: "Re (z) =  Re z" 
14373  142 
by (simp add: complex_minus_def) 
14323  143 

14374  144 
lemma complex_Im_minus [simp]: "Im (z) =  Im z" 
145 
by (simp add: complex_minus_def) 

14323  146 

147 

148 
subsection{*Addition*} 

149 

14377  150 
lemma complex_add [simp]: 
151 
"Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)" 

14373  152 
by (simp add: complex_add_def) 
14323  153 

14374  154 
lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)" 
14373  155 
by (simp add: complex_add_def) 
14323  156 

14374  157 
lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)" 
14373  158 
by (simp add: complex_add_def) 
14323  159 

160 
lemma complex_add_commute: "(u::complex) + v = v + u" 

14373  161 
by (simp add: complex_add_def add_commute) 
14323  162 

163 
lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)" 

14373  164 
by (simp add: complex_add_def add_assoc) 
14323  165 

166 
lemma complex_add_zero_left: "(0::complex) + z = z" 

14373  167 
by (simp add: complex_add_def complex_zero_def) 
14323  168 

169 
lemma complex_add_zero_right: "z + (0::complex) = z" 

14373  170 
by (simp add: complex_add_def complex_zero_def) 
14323  171 

14373  172 
lemma complex_add_minus_left: "z + z = (0::complex)" 
173 
by (simp add: complex_add_def complex_minus_def complex_zero_def) 

14323  174 

175 
lemma complex_diff: 

14373  176 
"Complex x1 y1  Complex x2 y2 = Complex (x1x2) (y1y2)" 
177 
by (simp add: complex_add_def complex_minus_def complex_diff_def) 

14323  178 

14374  179 
lemma complex_Re_diff [simp]: "Re(x  y) = Re(x)  Re(y)" 
180 
by (simp add: complex_diff_def) 

181 

182 
lemma complex_Im_diff [simp]: "Im(x  y) = Im(x)  Im(y)" 

183 
by (simp add: complex_diff_def) 

184 

185 

14323  186 
subsection{*Multiplication*} 
187 

14377  188 
lemma complex_mult [simp]: 
14373  189 
"Complex x1 y1 * Complex x2 y2 = Complex (x1*x2  y1*y2) (x1*y2 + y1*x2)" 
190 
by (simp add: complex_mult_def) 

14323  191 

192 
lemma complex_mult_commute: "(w::complex) * z = z * w" 

14373  193 
by (simp add: complex_mult_def mult_commute add_commute) 
14323  194 

195 
lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)" 

14374  196 
by (simp add: complex_mult_def mult_ac add_ac 
14373  197 
right_diff_distrib right_distrib left_diff_distrib left_distrib) 
14323  198 

199 
lemma complex_mult_one_left: "(1::complex) * z = z" 

14373  200 
by (simp add: complex_mult_def complex_one_def) 
14323  201 

202 
lemma complex_mult_one_right: "z * (1::complex) = z" 

14373  203 
by (simp add: complex_mult_def complex_one_def) 
14323  204 

205 

206 
subsection{*Inverse*} 

207 

14377  208 
lemma complex_inverse [simp]: 
14373  209 
"inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (y/(x ^ 2 + y ^ 2))" 
210 
by (simp add: complex_inverse_def) 

14335  211 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

212 
lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1" 
14374  213 
apply (induct z) 
214 
apply (rename_tac x y) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

215 
apply (auto simp add: times_divide_eq complex_mult complex_inverse 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

216 
complex_one_def complex_zero_def add_divide_distrib [symmetric] 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

217 
power2_eq_square mult_ac) 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

218 
apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2) 
14323  219 
done 
220 

14335  221 

222 
subsection {* The field of complex numbers *} 

223 

224 
instance complex :: field 

225 
proof 

226 
fix z u v w :: complex 

227 
show "(u + v) + w = u + (v + w)" 

14374  228 
by (rule complex_add_assoc) 
14335  229 
show "z + w = w + z" 
14374  230 
by (rule complex_add_commute) 
14335  231 
show "0 + z = z" 
14374  232 
by (rule complex_add_zero_left) 
14335  233 
show "z + z = 0" 
14374  234 
by (rule complex_add_minus_left) 
14335  235 
show "z  w = z + w" 
236 
by (simp add: complex_diff_def) 

237 
show "(u * v) * w = u * (v * w)" 

14374  238 
by (rule complex_mult_assoc) 
14335  239 
show "z * w = w * z" 
14374  240 
by (rule complex_mult_commute) 
14335  241 
show "1 * z = z" 
14374  242 
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

243 
show "0 \<noteq> (1::complex)" 
14373  244 
by (simp add: complex_zero_def complex_one_def) 
14335  245 
show "(u + v) * w = u * w + v * w" 
14421
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14387
diff
changeset

246 
by (simp add: complex_mult_def complex_add_def left_distrib 
ee97b6463cb4
new Ring_and_Field hierarchy, eliminating redundant axioms
paulson
parents:
14387
diff
changeset

247 
diff_minus add_ac) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

248 
show "z / w = z * inverse w" 
14335  249 
by (simp add: complex_divide_def) 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

250 
assume "w \<noteq> 0" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

251 
thus "inverse w * w = 1" 
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

252 
by (simp add: complex_mult_inv_left) 
14335  253 
qed 
254 

14373  255 
instance complex :: division_by_zero 
256 
proof 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

257 
show "inverse 0 = (0::complex)" 
14373  258 
by (simp add: complex_inverse_def complex_zero_def) 
259 
qed 

14335  260 

14323  261 

20556
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

262 
subsection{*The real algebra of complex numbers*} 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

263 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

264 
instance complex :: scaleR .. 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

265 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

266 
defs (overloaded) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

267 
complex_scaleR_def: "r *# x == Complex r 0 * x" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

268 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

269 
instance complex :: real_algebra_1 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

270 
proof 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

271 
fix a b :: real 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

272 
fix x y :: complex 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

273 
show "a *# (x + y) = a *# x + a *# y" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

274 
by (simp add: complex_scaleR_def right_distrib) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

275 
show "(a + b) *# x = a *# x + b *# x" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

276 
by (simp add: complex_scaleR_def left_distrib [symmetric]) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

277 
show "(a * b) *# x = a *# b *# x" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

278 
by (simp add: complex_scaleR_def mult_assoc [symmetric]) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

279 
show "1 *# x = x" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

280 
by (simp add: complex_scaleR_def complex_one_def [symmetric]) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

281 
show "a *# x * y = a *# (x * y)" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

282 
by (simp add: complex_scaleR_def mult_assoc) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

283 
show "x * a *# y = a *# (x * y)" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

284 
by (simp add: complex_scaleR_def mult_left_commute) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

285 
qed 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

286 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

287 

14323  288 
subsection{*Embedding Properties for @{term complex_of_real} Map*} 
289 

14377  290 
lemma Complex_add_complex_of_real [simp]: 
291 
"Complex x y + complex_of_real r = Complex (x+r) y" 

292 
by (simp add: complex_of_real_def) 

293 

294 
lemma complex_of_real_add_Complex [simp]: 

295 
"complex_of_real r + Complex x y = Complex (r+x) y" 

296 
by (simp add: i_def complex_of_real_def) 

297 

298 
lemma Complex_mult_complex_of_real: 

299 
"Complex x y * complex_of_real r = Complex (x*r) (y*r)" 

300 
by (simp add: complex_of_real_def) 

301 

302 
lemma complex_of_real_mult_Complex: 

303 
"complex_of_real r * Complex x y = Complex (r*x) (r*y)" 

304 
by (simp add: i_def complex_of_real_def) 

305 

306 
lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r" 

307 
by (simp add: i_def complex_of_real_def) 

308 

309 
lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" 

310 
by (simp add: i_def complex_of_real_def) 

311 

14374  312 
lemma complex_of_real_one [simp]: "complex_of_real 1 = 1" 
14373  313 
by (simp add: complex_one_def complex_of_real_def) 
14323  314 

14374  315 
lemma complex_of_real_zero [simp]: "complex_of_real 0 = 0" 
14373  316 
by (simp add: complex_zero_def complex_of_real_def) 
14323  317 

14374  318 
lemma complex_of_real_eq_iff [iff]: 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

319 
"(complex_of_real x = complex_of_real y) = (x = y)" 
14374  320 
by (simp add: complex_of_real_def) 
14323  321 

15013  322 
lemma complex_of_real_minus [simp]: "complex_of_real(x) =  complex_of_real x" 
14373  323 
by (simp add: complex_of_real_def complex_minus) 
14323  324 

15013  325 
lemma complex_of_real_inverse [simp]: 
14374  326 
"complex_of_real(inverse x) = inverse(complex_of_real x)" 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

327 
apply (case_tac "x=0", simp) 
15013  328 
apply (simp add: complex_of_real_def divide_inverse power2_eq_square) 
14323  329 
done 
330 

15013  331 
lemma complex_of_real_add [simp]: 
332 
"complex_of_real (x + y) = complex_of_real x + complex_of_real y" 

14373  333 
by (simp add: complex_add complex_of_real_def) 
14323  334 

15013  335 
lemma complex_of_real_diff [simp]: 
336 
"complex_of_real (x  y) = complex_of_real x  complex_of_real y" 

337 
by (simp add: complex_of_real_minus diff_minus) 

14323  338 

15013  339 
lemma complex_of_real_mult [simp]: 
340 
"complex_of_real (x * y) = complex_of_real x * complex_of_real y" 

14373  341 
by (simp add: complex_mult complex_of_real_def) 
14323  342 

15013  343 
lemma complex_of_real_divide [simp]: 
344 
"complex_of_real(x/y) = complex_of_real x / complex_of_real y" 

14373  345 
apply (simp add: complex_divide_def) 
346 
apply (case_tac "y=0", simp) 

15013  347 
apply (simp add: complex_of_real_mult complex_of_real_inverse 
348 
divide_inverse) 

14323  349 
done 
350 

14377  351 
lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)" 
14373  352 
by (simp add: cmod_def) 
14323  353 

14374  354 
lemma complex_mod_zero [simp]: "cmod(0) = 0" 
14373  355 
by (simp add: cmod_def) 
14323  356 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

357 
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

358 
by (simp add: cmod_def power2_eq_square) 
14323  359 

14374  360 
lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x" 
14373  361 
by (simp add: complex_of_real_def power2_eq_square complex_mod) 
14323  362 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

363 
lemma complex_of_real_abs: 
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

364 
"complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" 
14373  365 
by simp 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

366 

14323  367 

14377  368 
subsection{*The Functions @{term Re} and @{term Im}*} 
369 

370 
lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z  Im w * Im z" 

371 
by (induct z, induct w, simp add: complex_mult) 

372 

373 
lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z" 

374 
by (induct z, induct w, simp add: complex_mult) 

375 

376 
lemma Re_i_times [simp]: "Re(ii * z) =  Im z" 

377 
by (simp add: complex_Re_mult_eq) 

378 

379 
lemma Re_times_i [simp]: "Re(z * ii) =  Im z" 

380 
by (simp add: complex_Re_mult_eq) 

381 

382 
lemma Im_i_times [simp]: "Im(ii * z) = Re z" 

383 
by (simp add: complex_Im_mult_eq) 

384 

385 
lemma Im_times_i [simp]: "Im(z * ii) = Re z" 

386 
by (simp add: complex_Im_mult_eq) 

387 

388 
lemma complex_Re_mult: "[ Im w = 0; Im z = 0 ] ==> Re(w * z) = Re(w) * Re(z)" 

389 
by (simp add: complex_Re_mult_eq) 

390 

391 
lemma complex_Re_mult_complex_of_real [simp]: 

392 
"Re (z * complex_of_real c) = Re(z) * c" 

393 
by (simp add: complex_Re_mult_eq) 

394 

395 
lemma complex_Im_mult_complex_of_real [simp]: 

396 
"Im (z * complex_of_real c) = Im(z) * c" 

397 
by (simp add: complex_Im_mult_eq) 

398 

399 
lemma complex_Re_mult_complex_of_real2 [simp]: 

400 
"Re (complex_of_real c * z) = c * Re(z)" 

401 
by (simp add: complex_Re_mult_eq) 

402 

403 
lemma complex_Im_mult_complex_of_real2 [simp]: 

404 
"Im (complex_of_real c * z) = c * Im(z)" 

405 
by (simp add: complex_Im_mult_eq) 

406 

407 

14323  408 
subsection{*Conjugation is an Automorphism*} 
409 

14373  410 
lemma complex_cnj: "cnj (Complex x y) = Complex x (y)" 
411 
by (simp add: cnj_def) 

14323  412 

14374  413 
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" 
14373  414 
by (simp add: cnj_def complex_Re_Im_cancel_iff) 
14323  415 

14374  416 
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" 
14373  417 
by (simp add: cnj_def) 
14323  418 

14374  419 
lemma complex_cnj_complex_of_real [simp]: 
14373  420 
"cnj (complex_of_real x) = complex_of_real x" 
421 
by (simp add: complex_of_real_def complex_cnj) 

14323  422 

14374  423 
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" 
14373  424 
by (induct z, simp add: complex_cnj complex_mod power2_eq_square) 
14323  425 

426 
lemma complex_cnj_minus: "cnj (z) =  cnj z" 

14373  427 
by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus) 
14323  428 

429 
lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)" 

14373  430 
by (induct z, simp add: complex_cnj complex_inverse power2_eq_square) 
14323  431 

432 
lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)" 

14373  433 
by (induct w, induct z, simp add: complex_cnj complex_add) 
14323  434 

435 
lemma complex_cnj_diff: "cnj(w  z) = cnj(w)  cnj(z)" 

15013  436 
by (simp add: diff_minus complex_cnj_add complex_cnj_minus) 
14323  437 

438 
lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)" 

14373  439 
by (induct w, induct z, simp add: complex_cnj complex_mult) 
14323  440 

441 
lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)" 

14373  442 
by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) 
14323  443 

14374  444 
lemma complex_cnj_one [simp]: "cnj 1 = 1" 
14373  445 
by (simp add: cnj_def complex_one_def) 
14323  446 

447 
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))" 

14373  448 
by (induct z, simp add: complex_add complex_cnj complex_of_real_def) 
14323  449 

450 
lemma complex_diff_cnj: "z  cnj z = complex_of_real (2 * Im(z)) * ii" 

14373  451 
apply (induct z) 
15013  452 
apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

453 
complex_minus i_def complex_mult) 
14323  454 
done 
455 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

456 
lemma complex_cnj_zero [simp]: "cnj 0 = 0" 
14334  457 
by (simp add: cnj_def complex_zero_def) 
14323  458 

14374  459 
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" 
14373  460 
by (induct z, simp add: complex_zero_def complex_cnj) 
14323  461 

462 
lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)" 

14374  463 
by (induct z, 
464 
simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square) 

14323  465 

466 

467 
subsection{*Modulus*} 

468 

14374  469 
lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)" 
14373  470 
apply (induct x) 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset

471 
apply (auto iff: real_0_le_add_iff 
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset

472 
intro: real_sum_squares_cancel real_sum_squares_cancel2 
14373  473 
simp add: complex_mod complex_zero_def power2_eq_square) 
14323  474 
done 
475 

14374  476 
lemma complex_mod_complex_of_real_of_nat [simp]: 
14373  477 
"cmod (complex_of_real(real (n::nat))) = real n" 
478 
by simp 

14323  479 

14374  480 
lemma complex_mod_minus [simp]: "cmod (x) = cmod(x)" 
14373  481 
by (induct x, simp add: complex_mod complex_minus power2_eq_square) 
14323  482 

483 
lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" 

14373  484 
apply (induct z, simp add: complex_mod complex_cnj complex_mult) 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset

485 
apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff) 
14323  486 
done 
487 

14373  488 
lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2" 
489 
by (simp add: cmod_def) 

14323  490 

14374  491 
lemma complex_mod_ge_zero [simp]: "0 \<le> cmod x" 
14373  492 
by (simp add: cmod_def) 
14323  493 

14374  494 
lemma abs_cmod_cancel [simp]: "abs(cmod x) = cmod x" 
495 
by (simp add: abs_if linorder_not_less) 

14323  496 

497 
lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)" 

14373  498 
apply (induct x, induct y) 
14377  499 
apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric]) 
14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

500 
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

501 
apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc) 
14374  502 
apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib 
503 
add_ac mult_ac) 

14323  504 
done 
505 

14377  506 
lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1" 
507 
by (simp add: cmod_def) 

508 

509 
lemma cmod_complex_polar [simp]: 

510 
"cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r" 

511 
by (simp only: cmod_unit_one complex_mod_mult, simp) 

512 

14374  513 
lemma complex_mod_add_squared_eq: 
514 
"cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" 

14373  515 
apply (induct x, induct y) 
14323  516 
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

517 
apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) 
14323  518 
done 
519 

14374  520 
lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \<le> cmod(x * cnj y)" 
14373  521 
apply (induct x, induct y) 
14323  522 
apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc) 
523 
done 

524 

14374  525 
lemma complex_Re_mult_cnj_le_cmod2 [simp]: "Re(x * cnj y) \<le> cmod(x * y)" 
14373  526 
by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult) 
14323  527 

14374  528 
lemma real_sum_squared_expand: 
529 
"((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" 

14373  530 
by (simp add: left_distrib right_distrib power2_eq_square) 
14323  531 

14374  532 
lemma complex_mod_triangle_squared [simp]: 
533 
"cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2" 

14373  534 
by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric]) 
14323  535 

14374  536 
lemma complex_mod_minus_le_complex_mod [simp]: " cmod x \<le> cmod x" 
14373  537 
by (rule order_trans [OF _ complex_mod_ge_zero], simp) 
14323  538 

14374  539 
lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)" 
14334  540 
apply (rule_tac n = 1 in realpow_increasing) 
14323  541 
apply (auto intro: order_trans [OF _ complex_mod_ge_zero] 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15013
diff
changeset

542 
simp add: add_increasing power2_eq_square [symmetric]) 
14323  543 
done 
544 

14374  545 
lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a)  cmod b \<le> cmod a" 
14373  546 
by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"cmod b"], simp) 
14323  547 

548 
lemma complex_mod_diff_commute: "cmod (x  y) = cmod (y  x)" 

14373  549 
apply (induct x, induct y) 
14353
79f9fbef9106
Added lemmas to Ring_and_Field with slightly modified simplification rules
paulson
parents:
14348
diff
changeset

550 
apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac) 
14323  551 
done 
552 

14374  553 
lemma complex_mod_add_less: 
554 
"[ cmod x < r; cmod y < s ] ==> cmod (x + y) < r + s" 

14334  555 
by (auto intro: order_le_less_trans complex_mod_triangle_ineq) 
14323  556 

14374  557 
lemma complex_mod_mult_less: 
558 
"[ cmod x < r; cmod y < s ] ==> cmod (x * y) < r * s" 

14334  559 
by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) 
14323  560 

14374  561 
lemma complex_mod_diff_ineq [simp]: "cmod(a)  cmod(b) \<le> cmod(a + b)" 
14323  562 
apply (rule linorder_cases [of "cmod(a)" "cmod (b)"]) 
563 
apply auto 

14334  564 
apply (rule order_trans [of _ 0], rule order_less_imp_le) 
14374  565 
apply (simp add: compare_rls, simp) 
14323  566 
apply (simp add: compare_rls) 
567 
apply (rule complex_mod_minus [THEN subst]) 

568 
apply (rule order_trans) 

569 
apply (rule_tac [2] complex_mod_triangle_ineq) 

14373  570 
apply (auto simp add: add_ac) 
14323  571 
done 
572 

14374  573 
lemma complex_Re_le_cmod [simp]: "Re z \<le> cmod z" 
14373  574 
by (induct z, simp add: complex_mod del: realpow_Suc) 
14323  575 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

576 
lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z" 
14373  577 
apply (insert complex_mod_ge_zero [of z]) 
14334  578 
apply (drule order_le_imp_less_or_eq, auto) 
14323  579 
done 
580 

581 

20556
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

582 
subsection{*The normed division algebra of complex numbers*} 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

583 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

584 
instance complex :: norm .. 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

585 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

586 
defs (overloaded) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

587 
complex_norm_def: "norm == cmod" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

588 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

589 
lemma of_real_complex_of_real: "of_real r = complex_of_real r" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

590 
by (simp add: complex_of_real_def of_real_def complex_scaleR_def) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

591 

2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

592 
instance complex :: real_normed_div_algebra 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

593 
proof (intro_classes, unfold complex_norm_def) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

594 
fix r :: real 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

595 
fix x y :: complex 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

596 
show "0 \<le> cmod x" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

597 
by (rule complex_mod_ge_zero) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

598 
show "(cmod x = 0) = (x = 0)" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

599 
by (rule complex_mod_eq_zero_cancel) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

600 
show "cmod (x + y) \<le> cmod x + cmod y" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

601 
by (rule complex_mod_triangle_ineq) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

602 
show "cmod (of_real r) = abs r" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

603 
by (simp add: of_real_complex_of_real) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

604 
show "cmod (x * y) = cmod x * cmod y" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

605 
by (rule complex_mod_mult) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

606 
show "cmod 1 = 1" 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

607 
by (rule complex_mod_one) 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

608 
qed 
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

609 

14323  610 
subsection{*A Few More Theorems*} 
611 

612 
lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)" 

14373  613 
apply (case_tac "x=0", simp) 
14323  614 
apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1]) 
615 
apply (auto simp add: complex_mod_mult [symmetric]) 

616 
done 

617 

14373  618 
lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)" 
15013  619 
by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse) 
14323  620 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

621 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

622 
subsection{*Exponentiation*} 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

623 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

624 
primrec 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

625 
complexpow_0: "z ^ 0 = 1" 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

626 
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

627 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

628 

15003  629 
instance complex :: recpower 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

630 
proof 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

631 
fix z :: complex 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

632 
fix n :: nat 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

633 
show "z^0 = 1" by simp 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

634 
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

635 
qed 
14323  636 

637 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

638 
lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n" 
14323  639 
apply (induct_tac "n") 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

640 
apply (auto simp add: complex_of_real_mult [symmetric]) 
14323  641 
done 
642 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

643 
lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n" 
14323  644 
apply (induct_tac "n") 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

645 
apply (auto simp add: complex_cnj_mult) 
14323  646 
done 
647 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

648 
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

649 
apply (induct_tac "n") 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

650 
apply (auto simp add: complex_mod_mult) 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

651 
done 
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

652 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

653 
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

654 
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

655 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

656 
lemma complex_i_not_zero [simp]: "ii \<noteq> 0" 
14373  657 
by (simp add: i_def complex_zero_def) 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

658 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

659 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

660 
subsection{*The Function @{term sgn}*} 
14323  661 

14374  662 
lemma sgn_zero [simp]: "sgn 0 = 0" 
14373  663 
by (simp add: sgn_def) 
14323  664 

14374  665 
lemma sgn_one [simp]: "sgn 1 = 1" 
14373  666 
by (simp add: sgn_def) 
14323  667 

668 
lemma sgn_minus: "sgn (z) =  sgn(z)" 

14373  669 
by (simp add: sgn_def) 
14323  670 

14374  671 
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" 
14377  672 
by (simp add: sgn_def) 
14323  673 

674 
lemma i_mult_eq: "ii * ii = complex_of_real (1)" 

14373  675 
by (simp add: i_def complex_of_real_def complex_mult complex_add) 
14323  676 

14374  677 
lemma i_mult_eq2 [simp]: "ii * ii = (1::complex)" 
14373  678 
by (simp add: i_def complex_one_def complex_mult complex_minus) 
14323  679 

14374  680 
lemma complex_eq_cancel_iff2 [simp]: 
14377  681 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
682 
by (simp add: complex_of_real_def) 

14323  683 

14374  684 
lemma complex_eq_cancel_iff2a [simp]: 
14377  685 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
686 
by (simp add: complex_of_real_def) 

14323  687 

14377  688 
lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)" 
689 
by (simp add: complex_zero_def) 

14323  690 

14377  691 
lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)" 
692 
by (simp add: complex_one_def) 

14323  693 

14377  694 
lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)" 
695 
by (simp add: i_def) 

14323  696 

15013  697 

698 

14374  699 
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" 
15013  700 
proof (induct z) 
701 
case (Complex x y) 

702 
have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))" 

703 
by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq) 

704 
thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)" 

705 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

706 
qed 

707 

14323  708 

14374  709 
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" 
15013  710 
proof (induct z) 
711 
case (Complex x y) 

712 
have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))" 

713 
by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq) 

714 
thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)" 

715 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

716 
qed 

14323  717 

718 
lemma complex_inverse_complex_split: 

719 
"inverse(complex_of_real x + ii * complex_of_real y) = 

720 
complex_of_real(x/(x ^ 2 + y ^ 2))  

721 
ii * complex_of_real(y/(x ^ 2 + y ^ 2))" 

14374  722 
by (simp add: complex_of_real_def i_def complex_mult complex_add 
15013  723 
diff_minus complex_minus complex_inverse divide_inverse) 
14323  724 

725 
(**) 

726 
(* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *) 

727 
(* many of the theorems are not used  so should they be kept? *) 

728 
(**) 

729 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

730 
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

731 
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

732 

988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

733 
lemma cos_arg_i_mult_zero_pos: 
14377  734 
"0 < y ==> cos (arg(Complex 0 y)) = 0" 
14373  735 
apply (simp add: arg_def abs_if) 
14334  736 
apply (rule_tac a = "pi/2" in someI2, auto) 
737 
apply (rule order_less_trans [of _ 0], auto) 

14323  738 
done 
739 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

740 
lemma cos_arg_i_mult_zero_neg: 
14377  741 
"y < 0 ==> cos (arg(Complex 0 y)) = 0" 
14373  742 
apply (simp add: arg_def abs_if) 
14334  743 
apply (rule_tac a = " pi/2" in someI2, auto) 
744 
apply (rule order_trans [of _ 0], auto) 

14323  745 
done 
746 

14374  747 
lemma cos_arg_i_mult_zero [simp]: 
14377  748 
"y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0" 
749 
by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg) 

14323  750 

751 

752 
subsection{*Finally! Polar Form for Complex Numbers*} 

753 

14374  754 
lemma complex_split_polar: 
14377  755 
"\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))" 
756 
apply (induct z) 

757 
apply (auto simp add: polar_Ex complex_of_real_mult_Complex) 

14323  758 
done 
759 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

760 
lemma rcis_Ex: "\<exists>r a. z = rcis r a" 
14377  761 
apply (induct z) 
762 
apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex) 

14323  763 
done 
764 

14374  765 
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" 
14373  766 
by (simp add: rcis_def cis_def) 
14323  767 

14348
744c868ee0b7
Defining the type class "ringpower" and deleting superseded theorems for
paulson
parents:
14341
diff
changeset

768 
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" 
14373  769 
by (simp add: rcis_def cis_def) 
14323  770 

14377  771 
lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>" 
772 
proof  

773 
have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)" 

774 
by (simp only: power_mult_distrib right_distrib) 

775 
thus ?thesis by simp 

776 
qed 

14323  777 

14374  778 
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" 
14377  779 
by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) 
14323  780 

781 
lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" 

14373  782 
apply (simp add: cmod_def) 
14323  783 
apply (rule real_sqrt_eq_iff [THEN iffD2]) 
784 
apply (auto simp add: complex_mult_cnj) 

785 
done 

786 

14374  787 
lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" 
14373  788 
by (induct z, simp add: complex_cnj) 
14323  789 

14374  790 
lemma complex_Im_cnj [simp]: "Im(cnj z) =  Im z" 
791 
by (induct z, simp add: complex_cnj) 

792 

793 
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0" 

14373  794 
by (induct z, simp add: complex_cnj complex_mult) 
14323  795 

796 

797 
(**) 

798 
(* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *) 

799 
(**) 

800 

801 
lemma cis_rcis_eq: "cis a = rcis 1 a" 

14373  802 
by (simp add: rcis_def) 
14323  803 

14374  804 
lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)" 
15013  805 
by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib 
806 
complex_of_real_def) 

14323  807 

808 
lemma cis_mult: "cis a * cis b = cis (a + b)" 

14373  809 
by (simp add: cis_rcis_eq rcis_mult) 
14323  810 

14374  811 
lemma cis_zero [simp]: "cis 0 = 1" 
14377  812 
by (simp add: cis_def complex_one_def) 
14323  813 

14374  814 
lemma rcis_zero_mod [simp]: "rcis 0 a = 0" 
14373  815 
by (simp add: rcis_def) 
14323  816 

14374  817 
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" 
14373  818 
by (simp add: rcis_def) 
14323  819 

820 
lemma complex_of_real_minus_one: 

821 
"complex_of_real ((1::real)) = (1::complex)" 

14377  822 
by (simp add: complex_of_real_def complex_one_def complex_minus) 
14323  823 

14374  824 
lemma complex_i_mult_minus [simp]: "ii * (ii * x) =  x" 
14373  825 
by (simp add: complex_mult_assoc [symmetric]) 
14323  826 

827 

828 
lemma cis_real_of_nat_Suc_mult: 

829 
"cis (real (Suc n) * a) = cis a * cis (real n * a)" 

14377  830 
by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) 
14323  831 

832 
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" 

833 
apply (induct_tac "n") 

834 
apply (auto simp add: cis_real_of_nat_Suc_mult) 

835 
done 

836 

14374  837 
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" 
838 
by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow) 

14323  839 

14374  840 
lemma cis_inverse [simp]: "inverse(cis a) = cis (a)" 
841 
by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus 

15013  842 
diff_minus) 
14323  843 

844 
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (a)" 

14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

845 
by (simp add: divide_inverse rcis_def complex_of_real_inverse) 
14323  846 

847 
lemma cis_divide: "cis a / cis b = cis (a  b)" 

14373  848 
by (simp add: complex_divide_def cis_mult real_diff_def) 
14323  849 

14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

850 
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a  b)" 
14373  851 
apply (simp add: complex_divide_def) 
852 
apply (case_tac "r2=0", simp) 

853 
apply (simp add: rcis_inverse rcis_mult real_diff_def) 

14323  854 
done 
855 

14374  856 
lemma Re_cis [simp]: "Re(cis a) = cos a" 
14373  857 
by (simp add: cis_def) 
14323  858 

14374  859 
lemma Im_cis [simp]: "Im(cis a) = sin a" 
14373  860 
by (simp add: cis_def) 
14323  861 

862 
lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" 

14334  863 
by (auto simp add: DeMoivre) 
14323  864 

865 
lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" 

14334  866 
by (auto simp add: DeMoivre) 
14323  867 

868 
lemma expi_add: "expi(a + b) = expi(a) * expi(b)" 

14374  869 
by (simp add: expi_def complex_Re_add exp_add complex_Im_add 
870 
cis_mult [symmetric] complex_of_real_mult mult_ac) 

14323  871 

14374  872 
lemma expi_zero [simp]: "expi (0::complex) = 1" 
14373  873 
by (simp add: expi_def) 
14323  874 

14374  875 
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a" 
14373  876 
apply (insert rcis_Ex [of z]) 
14323  877 
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult) 
14334  878 
apply (rule_tac x = "ii * complex_of_real a" in exI, auto) 
14323  879 
done 
880 

881 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

882 
subsection{*Numerals and Arithmetic*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

883 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

884 
instance complex :: number .. 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

885 

15013  886 
defs (overloaded) 
20485  887 
complex_number_of_def: "(number_of w :: complex) == of_int w" 
15013  888 
{*the type constraint is essential!*} 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

889 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

890 
instance complex :: number_ring 
15013  891 
by (intro_classes, simp add: complex_number_of_def) 
892 

893 

894 
lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n" 

19765  895 
by (induct n) simp_all 
15013  896 

897 
lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z" 

898 
proof (cases z) 

899 
case (1 n) 

19765  900 
thus ?thesis by simp 
15013  901 
next 
902 
case (2 n) 

19765  903 
thus ?thesis 
904 
by (simp only: of_int_minus complex_of_real_minus, simp) 

14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

905 
qed 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

906 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

907 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

908 
text{*Collapse applications of @{term complex_of_real} to @{term number_of}*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

909 
lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w" 
15013  910 
by (simp add: complex_number_of_def real_number_of_def) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

911 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

912 
text{*This theorem is necessary because theorems such as 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

913 
@{text iszero_number_of_0} only hold for ordered rings. They cannot 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

914 
be generalized to fields in general because they fail for finite fields. 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

915 
They work for type complex because the reals can be embedded in them.*} 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

916 
lemma iszero_complex_number_of [simp]: 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

917 
"iszero (number_of w :: complex) = iszero (number_of w :: real)" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

918 
by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

919 
iszero_def) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

920 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

921 
lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v" 
15481  922 
by (simp only: complex_number_of [symmetric] complex_cnj_complex_of_real) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

923 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

924 
lemma complex_number_of_cmod: 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

925 
"cmod(number_of v :: complex) = abs (number_of v :: real)" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

926 
by (simp only: complex_number_of [symmetric] complex_mod_complex_of_real) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

927 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

928 
lemma complex_number_of_Re [simp]: "Re(number_of v :: complex) = number_of v" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

929 
by (simp only: complex_number_of [symmetric] Re_complex_of_real) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

930 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

931 
lemma complex_number_of_Im [simp]: "Im(number_of v :: complex) = 0" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

932 
by (simp only: complex_number_of [symmetric] Im_complex_of_real) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

933 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

934 
lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1" 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

935 
by (simp add: expi_def complex_Re_mult_eq complex_Im_mult_eq cis_def) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

936 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

937 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

938 
(*examples: 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

939 
print_depth 22 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

940 
set timing; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

941 
set trace_simp; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

942 
fun test s = (Goal s, by (Simp_tac 1)); 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

943 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

944 
test "23 * ii + 45 * ii= (x::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

945 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

946 
test "5 * ii + 12  45 * ii= (x::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

947 
test "5 * ii + 40  12 * ii + 9 = (x::complex) + 89 * ii"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

948 
test "5 * ii + 40  12 * ii + 9  78 = (x::complex) + 89 * ii"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

949 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

950 
test "l + 10 * ii + 90 + 3*l + 9 + 45 * ii= (x::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

951 
test "87 + 10 * ii + 90 + 3*7 + 9 + 45 * ii= (x::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

952 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

953 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

954 
fun test s = (Goal s; by (Asm_simp_tac 1)); 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

955 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

956 
test "x*k = k*(y::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

957 
test "k = k*(y::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

958 
test "a*(b*c) = (b::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

959 
test "a*(b*c) = d*(b::complex)*(x*a)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

960 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

961 

e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

962 
test "(x*k) / (k*(y::complex)) = (uu::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

963 
test "(k) / (k*(y::complex)) = (uu::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

964 
test "(a*(b*c)) / ((b::complex)) = (uu::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

965 
test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

966 

15003  967 
FIXME: what do we do about this? 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

968 
test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z"; 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

969 
*) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

970 

13957  971 
end 
972 

973 