author  nipkow 
Mon, 16 Aug 2004 14:22:27 +0200  
changeset 15131  c69542757a4d 
parent 15085  5693a977a767 
child 15140  322485b816ac 
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 
11 
import "../Hyperreal/HLog" 

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 

30 
constdefs 

31 

32 
(* modulus *) 

33 

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

13957  36 

14323  37 
(* injection from reals *) 
38 

39 
complex_of_real :: "real => complex" 

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

13957  42 
(* complex conjugate *) 
43 

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

14323  47 
(* Argand *) 
13957  48 

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

14323  52 
arg :: "complex => real" 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

53 
"arg z == @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 

84 
constdefs 

85 

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

14323  87 
cis :: "real => complex" 
14377  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" 
13957  92 
"rcis r a == complex_of_real r * cis a" 
93 

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

14323  95 
expi :: "complex => complex" 
13957  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) 

215 
apply (auto simp add: complex_mult complex_inverse complex_one_def 

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

216 
complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac) 
14334  217 
apply (drule_tac y = y in real_sum_squares_not_zero) 
218 
apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto) 

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 

262 
subsection{*Embedding Properties for @{term complex_of_real} Map*} 

263 

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

266 
by (simp add: complex_of_real_def) 

267 

268 
lemma complex_of_real_add_Complex [simp]: 

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

270 
by (simp add: i_def complex_of_real_def) 

271 

272 
lemma Complex_mult_complex_of_real: 

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

274 
by (simp add: complex_of_real_def) 

275 

276 
lemma complex_of_real_mult_Complex: 

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

278 
by (simp add: i_def complex_of_real_def) 

279 

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

281 
by (simp add: i_def complex_of_real_def) 

282 

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

284 
by (simp add: i_def complex_of_real_def) 

285 

14374  286 
lemma complex_of_real_one [simp]: "complex_of_real 1 = 1" 
14373  287 
by (simp add: complex_one_def complex_of_real_def) 
14323  288 

14374  289 
lemma complex_of_real_zero [simp]: "complex_of_real 0 = 0" 
14373  290 
by (simp add: complex_zero_def complex_of_real_def) 
14323  291 

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

293 
"(complex_of_real x = complex_of_real y) = (x = y)" 
14374  294 
by (simp add: complex_of_real_def) 
14323  295 

15013  296 
lemma complex_of_real_minus [simp]: "complex_of_real(x) =  complex_of_real x" 
14373  297 
by (simp add: complex_of_real_def complex_minus) 
14323  298 

15013  299 
lemma complex_of_real_inverse [simp]: 
14374  300 
"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

301 
apply (case_tac "x=0", simp) 
15013  302 
apply (simp add: complex_of_real_def divide_inverse power2_eq_square) 
14323  303 
done 
304 

15013  305 
lemma complex_of_real_add [simp]: 
306 
"complex_of_real (x + y) = complex_of_real x + complex_of_real y" 

14373  307 
by (simp add: complex_add complex_of_real_def) 
14323  308 

15013  309 
lemma complex_of_real_diff [simp]: 
310 
"complex_of_real (x  y) = complex_of_real x  complex_of_real y" 

311 
by (simp add: complex_of_real_minus diff_minus) 

14323  312 

15013  313 
lemma complex_of_real_mult [simp]: 
314 
"complex_of_real (x * y) = complex_of_real x * complex_of_real y" 

14373  315 
by (simp add: complex_mult complex_of_real_def) 
14323  316 

15013  317 
lemma complex_of_real_divide [simp]: 
318 
"complex_of_real(x/y) = complex_of_real x / complex_of_real y" 

14373  319 
apply (simp add: complex_divide_def) 
320 
apply (case_tac "y=0", simp) 

15013  321 
apply (simp add: complex_of_real_mult complex_of_real_inverse 
322 
divide_inverse) 

14323  323 
done 
324 

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

14374  328 
lemma complex_mod_zero [simp]: "cmod(0) = 0" 
14373  329 
by (simp add: cmod_def) 
14323  330 

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

331 
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

332 
by (simp add: cmod_def power2_eq_square) 
14323  333 

14374  334 
lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x" 
14373  335 
by (simp add: complex_of_real_def power2_eq_square complex_mod) 
14323  336 

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

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

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

340 

14323  341 

14377  342 
subsection{*The Functions @{term Re} and @{term Im}*} 
343 

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

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

346 

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

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

349 

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

351 
by (simp add: complex_Re_mult_eq) 

352 

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

354 
by (simp add: complex_Re_mult_eq) 

355 

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

357 
by (simp add: complex_Im_mult_eq) 

358 

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

360 
by (simp add: complex_Im_mult_eq) 

361 

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

363 
by (simp add: complex_Re_mult_eq) 

364 

365 
lemma complex_Re_mult_complex_of_real [simp]: 

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

367 
by (simp add: complex_Re_mult_eq) 

368 

369 
lemma complex_Im_mult_complex_of_real [simp]: 

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

371 
by (simp add: complex_Im_mult_eq) 

372 

373 
lemma complex_Re_mult_complex_of_real2 [simp]: 

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

375 
by (simp add: complex_Re_mult_eq) 

376 

377 
lemma complex_Im_mult_complex_of_real2 [simp]: 

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

379 
by (simp add: complex_Im_mult_eq) 

380 

381 

14323  382 
subsection{*Conjugation is an Automorphism*} 
383 

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

14323  386 

14374  387 
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" 
14373  388 
by (simp add: cnj_def complex_Re_Im_cancel_iff) 
14323  389 

14374  390 
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" 
14373  391 
by (simp add: cnj_def) 
14323  392 

14374  393 
lemma complex_cnj_complex_of_real [simp]: 
14373  394 
"cnj (complex_of_real x) = complex_of_real x" 
395 
by (simp add: complex_of_real_def complex_cnj) 

14323  396 

14374  397 
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" 
14373  398 
by (induct z, simp add: complex_cnj complex_mod power2_eq_square) 
14323  399 

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

14373  401 
by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus) 
14323  402 

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

14373  404 
by (induct z, simp add: complex_cnj complex_inverse power2_eq_square) 
14323  405 

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

14373  407 
by (induct w, induct z, simp add: complex_cnj complex_add) 
14323  408 

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

15013  410 
by (simp add: diff_minus complex_cnj_add complex_cnj_minus) 
14323  411 

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

14373  413 
by (induct w, induct z, simp add: complex_cnj complex_mult) 
14323  414 

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

14373  416 
by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) 
14323  417 

14374  418 
lemma complex_cnj_one [simp]: "cnj 1 = 1" 
14373  419 
by (simp add: cnj_def complex_one_def) 
14323  420 

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

14373  422 
by (induct z, simp add: complex_add complex_cnj complex_of_real_def) 
14323  423 

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

14373  425 
apply (induct z) 
15013  426 
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

427 
complex_minus i_def complex_mult) 
14323  428 
done 
429 

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

430 
lemma complex_cnj_zero [simp]: "cnj 0 = 0" 
14334  431 
by (simp add: cnj_def complex_zero_def) 
14323  432 

14374  433 
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" 
14373  434 
by (induct z, simp add: complex_zero_def complex_cnj) 
14323  435 

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

14374  437 
by (induct z, 
438 
simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square) 

14323  439 

440 

441 
subsection{*Modulus*} 

442 

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

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

446 
intro: real_sum_squares_cancel real_sum_squares_cancel2 
14373  447 
simp add: complex_mod complex_zero_def power2_eq_square) 
14323  448 
done 
449 

14374  450 
lemma complex_mod_complex_of_real_of_nat [simp]: 
14373  451 
"cmod (complex_of_real(real (n::nat))) = real n" 
452 
by simp 

14323  453 

14374  454 
lemma complex_mod_minus [simp]: "cmod (x) = cmod(x)" 
14373  455 
by (induct x, simp add: complex_mod complex_minus power2_eq_square) 
14323  456 

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

14373  458 
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

459 
apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff) 
14323  460 
done 
461 

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

14323  464 

14374  465 
lemma complex_mod_ge_zero [simp]: "0 \<le> cmod x" 
14373  466 
by (simp add: cmod_def) 
14323  467 

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

14323  470 

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

14373  472 
apply (induct x, induct y) 
14377  473 
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

474 
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

475 
apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc) 
14374  476 
apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib 
477 
add_ac mult_ac) 

14323  478 
done 
479 

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

482 

483 
lemma cmod_complex_polar [simp]: 

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

485 
by (simp only: cmod_unit_one complex_mod_mult, simp) 

486 

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

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

491 
apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) 
14323  492 
done 
493 

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

498 

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

14374  502 
lemma real_sum_squared_expand: 
503 
"((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" 

14373  504 
by (simp add: left_distrib right_distrib power2_eq_square) 
14323  505 

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

14373  508 
by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric]) 
14323  509 

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

14374  513 
lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)" 
14334  514 
apply (rule_tac n = 1 in realpow_increasing) 
14323  515 
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

516 
simp add: add_increasing power2_eq_square [symmetric]) 
14323  517 
done 
518 

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

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

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

524 
apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac) 
14323  525 
done 
526 

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

14334  529 
by (auto intro: order_le_less_trans complex_mod_triangle_ineq) 
14323  530 

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

14334  533 
by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) 
14323  534 

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

14334  538 
apply (rule order_trans [of _ 0], rule order_less_imp_le) 
14374  539 
apply (simp add: compare_rls, simp) 
14323  540 
apply (simp add: compare_rls) 
541 
apply (rule complex_mod_minus [THEN subst]) 

542 
apply (rule order_trans) 

543 
apply (rule_tac [2] complex_mod_triangle_ineq) 

14373  544 
apply (auto simp add: add_ac) 
14323  545 
done 
546 

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

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

550 
lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z" 
14373  551 
apply (insert complex_mod_ge_zero [of z]) 
14334  552 
apply (drule order_le_imp_less_or_eq, auto) 
14323  553 
done 
554 

555 

556 
subsection{*A Few More Theorems*} 

557 

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

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

562 
done 

563 

14373  564 
lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)" 
15013  565 
by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse) 
14323  566 

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

567 

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

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

569 

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

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

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

572 
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

573 

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

574 

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

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

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

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

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

580 
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

581 
qed 
14323  582 

583 

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

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

586 
apply (auto simp add: complex_of_real_mult [symmetric]) 
14323  587 
done 
588 

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

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

591 
apply (auto simp add: complex_cnj_mult) 
14323  592 
done 
593 

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

594 
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

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

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

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

598 

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

599 
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

600 
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

601 

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

602 
lemma complex_i_not_zero [simp]: "ii \<noteq> 0" 
14373  603 
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

604 

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

605 

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

606 
subsection{*The Function @{term sgn}*} 
14323  607 

14374  608 
lemma sgn_zero [simp]: "sgn 0 = 0" 
14373  609 
by (simp add: sgn_def) 
14323  610 

14374  611 
lemma sgn_one [simp]: "sgn 1 = 1" 
14373  612 
by (simp add: sgn_def) 
14323  613 

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

14373  615 
by (simp add: sgn_def) 
14323  616 

14374  617 
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" 
14377  618 
by (simp add: sgn_def) 
14323  619 

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

14373  621 
by (simp add: i_def complex_of_real_def complex_mult complex_add) 
14323  622 

14374  623 
lemma i_mult_eq2 [simp]: "ii * ii = (1::complex)" 
14373  624 
by (simp add: i_def complex_one_def complex_mult complex_minus) 
14323  625 

14374  626 
lemma complex_eq_cancel_iff2 [simp]: 
14377  627 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
628 
by (simp add: complex_of_real_def) 

14323  629 

14374  630 
lemma complex_eq_cancel_iff2a [simp]: 
14377  631 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
632 
by (simp add: complex_of_real_def) 

14323  633 

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

14323  636 

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

14323  639 

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

14323  642 

15013  643 

644 

14374  645 
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" 
15013  646 
proof (induct z) 
647 
case (Complex x y) 

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

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

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

651 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

652 
qed 

653 

14323  654 

14374  655 
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" 
15013  656 
proof (induct z) 
657 
case (Complex x y) 

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

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

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

661 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

662 
qed 

14323  663 

664 
lemma complex_inverse_complex_split: 

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

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

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

14374  668 
by (simp add: complex_of_real_def i_def complex_mult complex_add 
15013  669 
diff_minus complex_minus complex_inverse divide_inverse) 
14323  670 

671 
(**) 

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

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

674 
(**) 

675 

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

676 
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

677 
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

678 

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

679 
lemma cos_arg_i_mult_zero_pos: 
14377  680 
"0 < y ==> cos (arg(Complex 0 y)) = 0" 
14373  681 
apply (simp add: arg_def abs_if) 
14334  682 
apply (rule_tac a = "pi/2" in someI2, auto) 
683 
apply (rule order_less_trans [of _ 0], auto) 

14323  684 
done 
685 

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

686 
lemma cos_arg_i_mult_zero_neg: 
14377  687 
"y < 0 ==> cos (arg(Complex 0 y)) = 0" 
14373  688 
apply (simp add: arg_def abs_if) 
14334  689 
apply (rule_tac a = " pi/2" in someI2, auto) 
690 
apply (rule order_trans [of _ 0], auto) 

14323  691 
done 
692 

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

14323  696 

697 

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

699 

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

703 
apply (auto simp add: polar_Ex complex_of_real_mult_Complex) 

14323  704 
done 
705 

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

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

14323  709 
done 
710 

14374  711 
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" 
14373  712 
by (simp add: rcis_def cis_def) 
14323  713 

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

714 
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" 
14373  715 
by (simp add: rcis_def cis_def) 
14323  716 

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

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

720 
by (simp only: power_mult_distrib right_distrib) 

721 
thus ?thesis by simp 

722 
qed 

14323  723 

14374  724 
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" 
14377  725 
by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) 
14323  726 

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

14373  728 
apply (simp add: cmod_def) 
14323  729 
apply (rule real_sqrt_eq_iff [THEN iffD2]) 
730 
apply (auto simp add: complex_mult_cnj) 

731 
done 

732 

14374  733 
lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" 
14373  734 
by (induct z, simp add: complex_cnj) 
14323  735 

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

738 

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

14373  740 
by (induct z, simp add: complex_cnj complex_mult) 
14323  741 

742 

743 
(**) 

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

745 
(**) 

746 

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

14373  748 
by (simp add: rcis_def) 
14323  749 

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

14323  753 

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

14373  755 
by (simp add: cis_rcis_eq rcis_mult) 
14323  756 

14374  757 
lemma cis_zero [simp]: "cis 0 = 1" 
14377  758 
by (simp add: cis_def complex_one_def) 
14323  759 

14374  760 
lemma rcis_zero_mod [simp]: "rcis 0 a = 0" 
14373  761 
by (simp add: rcis_def) 
14323  762 

14374  763 
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" 
14373  764 
by (simp add: rcis_def) 
14323  765 

766 
lemma complex_of_real_minus_one: 

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

14377  768 
by (simp add: complex_of_real_def complex_one_def complex_minus) 
14323  769 

14374  770 
lemma complex_i_mult_minus [simp]: "ii * (ii * x) =  x" 
14373  771 
by (simp add: complex_mult_assoc [symmetric]) 
14323  772 

773 

774 
lemma cis_real_of_nat_Suc_mult: 

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

14377  776 
by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) 
14323  777 

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

779 
apply (induct_tac "n") 

780 
apply (auto simp add: cis_real_of_nat_Suc_mult) 

781 
done 

782 

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

14323  785 

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

15013  788 
diff_minus) 
14323  789 

790 
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

791 
by (simp add: divide_inverse rcis_def complex_of_real_inverse) 
14323  792 

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

14373  794 
by (simp add: complex_divide_def cis_mult real_diff_def) 
14323  795 

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

796 
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a  b)" 
14373  797 
apply (simp add: complex_divide_def) 
798 
apply (case_tac "r2=0", simp) 

799 
apply (simp add: rcis_inverse rcis_mult real_diff_def) 

14323  800 
done 
801 

14374  802 
lemma Re_cis [simp]: "Re(cis a) = cos a" 
14373  803 
by (simp add: cis_def) 
14323  804 

14374  805 
lemma Im_cis [simp]: "Im(cis a) = sin a" 
14373  806 
by (simp add: cis_def) 
14323  807 

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

14334  809 
by (auto simp add: DeMoivre) 
14323  810 

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

14334  812 
by (auto simp add: DeMoivre) 
14323  813 

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

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

14323  817 

14374  818 
lemma expi_zero [simp]: "expi (0::complex) = 1" 
14373  819 
by (simp add: expi_def) 
14323  820 

14374  821 
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a" 
14373  822 
apply (insert rcis_Ex [of z]) 
14323  823 
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult) 
14334  824 
apply (rule_tac x = "ii * complex_of_real a" in exI, auto) 
14323  825 
done 
826 

827 

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

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

829 

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

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

831 

15013  832 
defs (overloaded) 
833 
complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)" 

834 
{*the type constraint is essential!*} 

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

835 

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

836 
instance complex :: number_ring 
15013  837 
by (intro_classes, simp add: complex_number_of_def) 
838 

839 

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

841 
by (induct n, simp_all) 

842 

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

844 
proof (cases z) 

845 
case (1 n) 

846 
thus ?thesis by simp 

847 
next 

848 
case (2 n) 

849 
thus ?thesis 

850 
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

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

852 

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

853 

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

854 
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

855 
lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w" 
15013  856 
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

857 

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

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

859 
@{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

860 
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

861 
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

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

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

864 
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

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

866 

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

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

868 
apply (subst complex_number_of [symmetric]) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

869 
apply (rule complex_cnj_complex_of_real) 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

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

871 

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

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

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

874 
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

875 

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

876 
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

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

878 

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

879 
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

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

881 

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

882 
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

883 
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

884 

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

885 

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

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

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

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

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

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

891 

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

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

893 

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

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

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

896 
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

897 

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

898 
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

899 
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

900 

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

901 

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

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

903 

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

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

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

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

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

908 

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

909 

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

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

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

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

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

914 

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

916 
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

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

918 

14323  919 

920 
ML 

921 
{* 

922 
val complex_zero_def = thm"complex_zero_def"; 

923 
val complex_one_def = thm"complex_one_def"; 

924 
val complex_minus_def = thm"complex_minus_def"; 

925 
val complex_divide_def = thm"complex_divide_def"; 

926 
val complex_mult_def = thm"complex_mult_def"; 

927 
val complex_add_def = thm"complex_add_def"; 

928 
val complex_of_real_def = thm"complex_of_real_def"; 

929 
val i_def = thm"i_def"; 

930 
val expi_def = thm"expi_def"; 

931 
val cis_def = thm"cis_def"; 

932 
val rcis_def = thm"rcis_def"; 

933 
val cmod_def = thm"cmod_def"; 

934 
val cnj_def = thm"cnj_def"; 

935 
val sgn_def = thm"sgn_def"; 

936 
val arg_def = thm"arg_def"; 

937 
val complexpow_0 = thm"complexpow_0"; 

938 
val complexpow_Suc = thm"complexpow_Suc"; 

939 

940 
val Re = thm"Re"; 

941 
val Im = thm"Im"; 

942 
val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff"; 

943 
val complex_Re_zero = thm"complex_Re_zero"; 

944 
val complex_Im_zero = thm"complex_Im_zero"; 

945 
val complex_Re_one = thm"complex_Re_one"; 

946 
val complex_Im_one = thm"complex_Im_one"; 

947 
val complex_Re_i = thm"complex_Re_i"; 

948 
val complex_Im_i = thm"complex_Im_i"; 

949 
val Re_complex_of_real = thm"Re_complex_of_real"; 

950 
val Im_complex_of_real = thm"Im_complex_of_real"; 

951 
val complex_minus = thm"complex_minus"; 

952 
val complex_Re_minus = thm"complex_Re_minus"; 

953 
val complex_Im_minus = thm"complex_Im_minus"; 

954 
val complex_add = thm"complex_add"; 

955 
val complex_Re_add = thm"complex_Re_add"; 

956 
val complex_Im_add = thm"complex_Im_add"; 

957 
val complex_add_commute = thm"complex_add_commute"; 

958 
val complex_add_assoc = thm"complex_add_assoc"; 

959 
val complex_add_zero_left = thm"complex_add_zero_left"; 

960 
val complex_add_zero_right = thm"complex_add_zero_right"; 

961 
val complex_diff = thm"complex_diff"; 

962 
val complex_mult = thm"complex_mult"; 

963 
val complex_mult_one_left = thm"complex_mult_one_left"; 

964 
val complex_mult_one_right = thm"complex_mult_one_right"; 

965 
val complex_inverse = thm"complex_inverse"; 

966 
val complex_of_real_one = thm"complex_of_real_one"; 

967 
val complex_of_real_zero = thm"complex_of_real_zero"; 

968 
val complex_of_real_eq_iff = thm"complex_of_real_eq_iff"; 

969 
val complex_of_real_minus = thm"complex_of_real_minus"; 

970 
val complex_of_real_inverse = thm"complex_of_real_inverse"; 

971 
val complex_of_real_add = thm"complex_of_real_add"; 

972 
val complex_of_real_diff = thm"complex_of_real_diff"; 

973 
val complex_of_real_mult = thm"complex_of_real_mult"; 

974 
val complex_of_real_divide = thm"complex_of_real_divide"; 

975 
val complex_of_real_pow = thm"complex_of_real_pow"; 

976 
val complex_mod = thm"complex_mod"; 

977 
val complex_mod_zero = thm"complex_mod_zero"; 

978 
val complex_mod_one = thm"complex_mod_one"; 

979 
val complex_mod_complex_of_real = thm"complex_mod_complex_of_real"; 

980 
val complex_of_real_abs = thm"complex_of_real_abs"; 

981 
val complex_cnj = thm"complex_cnj"; 

982 
val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff"; 

983 
val complex_cnj_cnj = thm"complex_cnj_cnj"; 

984 
val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real"; 

985 
val complex_mod_cnj = thm"complex_mod_cnj"; 

986 
val complex_cnj_minus = thm"complex_cnj_minus"; 

987 
val complex_cnj_inverse = thm"complex_cnj_inverse"; 

988 
val complex_cnj_add = thm"complex_cnj_add"; 

989 
val complex_cnj_diff = thm"complex_cnj_diff"; 

990 
val complex_cnj_mult = thm"complex_cnj_mult"; 

991 
val complex_cnj_divide = thm"complex_cnj_divide"; 

992 
val complex_cnj_one = thm"complex_cnj_one"; 

993 
val complex_cnj_pow = thm"complex_cnj_pow"; 

994 
val complex_add_cnj = thm"complex_add_cnj"; 

995 
val complex_diff_cnj = thm"complex_diff_cnj"; 

996 
val complex_cnj_zero = thm"complex_cnj_zero"; 

997 
val complex_cnj_zero_iff = thm"complex_cnj_zero_iff"; 

998 
val complex_mult_cnj = thm"complex_mult_cnj"; 

999 
val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel"; 

1000 
val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat"; 

1001 
val complex_mod_minus = thm"complex_mod_minus"; 

1002 
val complex_mod_mult_cnj = thm"complex_mod_mult_cnj"; 

1003 
val complex_mod_squared = thm"complex_mod_squared"; 

1004 
val complex_mod_ge_zero = thm"complex_mod_ge_zero"; 

1005 
val abs_cmod_cancel = thm"abs_cmod_cancel"; 

1006 
val complex_mod_mult = thm"complex_mod_mult"; 

1007 
val complex_mod_add_squared_eq = thm"complex_mod_add_squared_eq"; 

1008 
val complex_Re_mult_cnj_le_cmod = thm"complex_Re_mult_cnj_le_cmod"; 

1009 
val complex_Re_mult_cnj_le_cmod2 = thm"complex_Re_mult_cnj_le_cmod2"; 

1010 
val real_sum_squared_expand = thm"real_sum_squared_expand"; 

1011 
val complex_mod_triangle_squared = thm"complex_mod_triangle_squared"; 

1012 
val complex_mod_minus_le_complex_mod = thm"complex_mod_minus_le_complex_mod"; 

1013 
val complex_mod_triangle_ineq = thm"complex_mod_triangle_ineq"; 

1014 
val complex_mod_triangle_ineq2 = thm"complex_mod_triangle_ineq2"; 

1015 
val complex_mod_diff_commute = thm"complex_mod_diff_commute"; 

1016 
val complex_mod_add_less = thm"complex_mod_add_less"; 

1017 
val complex_mod_mult_less = thm"complex_mod_mult_less"; 

1018 
val complex_mod_diff_ineq = thm"complex_mod_diff_ineq"; 

1019 
val complex_Re_le_cmod = thm"complex_Re_le_cmod"; 

1020 
val complex_mod_gt_zero = thm"complex_mod_gt_zero"; 

1021 
val complex_mod_complexpow = thm"complex_mod_complexpow"; 

1022 
val complex_mod_inverse = thm"complex_mod_inverse"; 

1023 
val complex_mod_divide = thm"complex_mod_divide"; 

1024 
val complexpow_i_squared = thm"complexpow_i_squared"; 

1025 
val complex_i_not_zero = thm"complex_i_not_zero"; 

1026 
val sgn_zero = thm"sgn_zero"; 

1027 
val sgn_one = thm"sgn_one"; 

1028 
val sgn_minus = thm"sgn_minus"; 

1029 
val sgn_eq = thm"sgn_eq"; 

1030 
val i_mult_eq = thm"i_mult_eq"; 

1031 
val i_mult_eq2 = thm"i_mult_eq2"; 

1032 
val Re_sgn = thm"Re_sgn"; 

1033 
val Im_sgn = thm"Im_sgn"; 

1034 
val complex_inverse_complex_split = thm"complex_inverse_complex_split"; 

1035 
val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero"; 

1036 
val complex_of_real_zero_iff = thm"complex_of_real_zero_iff"; 

1037 
val rcis_Ex = thm"rcis_Ex"; 

1038 
val Re_rcis = thm"Re_rcis"; 

1039 
val Im_rcis = thm"Im_rcis"; 

1040 
val complex_mod_rcis = thm"complex_mod_rcis"; 

1041 
val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj"; 

1042 
val complex_Re_cnj = thm"complex_Re_cnj"; 

1043 
val complex_Im_cnj = thm"complex_Im_cnj"; 

1044 
val complex_In_mult_cnj_zero = thm"complex_In_mult_cnj_zero"; 

1045 
val complex_Re_mult = thm"complex_Re_mult"; 

1046 
val complex_Re_mult_complex_of_real = thm"complex_Re_mult_complex_of_real"; 

1047 
val complex_Im_mult_complex_of_real = thm"complex_Im_mult_complex_of_real"; 

1048 
val complex_Re_mult_complex_of_real2 = thm"complex_Re_mult_complex_of_real2"; 

1049 
val complex_Im_mult_complex_of_real2 = thm"complex_Im_mult_complex_of_real2"; 

1050 
val cis_rcis_eq = thm"cis_rcis_eq"; 

1051 
val rcis_mult = thm"rcis_mult"; 

1052 
val cis_mult = thm"cis_mult"; 

1053 
val cis_zero = thm"cis_zero"; 

1054 
val rcis_zero_mod = thm"rcis_zero_mod"; 

1055 
val rcis_zero_arg = thm"rcis_zero_arg"; 

1056 
val complex_of_real_minus_one = thm"complex_of_real_minus_one"; 

1057 
val complex_i_mult_minus = thm"complex_i_mult_minus"; 

1058 
val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult"; 

1059 
val DeMoivre = thm"DeMoivre"; 

1060 
val DeMoivre2 = thm"DeMoivre2"; 

1061 
val cis_inverse = thm"cis_inverse"; 

1062 
val rcis_inverse = thm"rcis_inverse"; 

1063 
val cis_divide = thm"cis_divide"; 

1064 
val rcis_divide = thm"rcis_divide"; 

1065 
val Re_cis = thm"Re_cis"; 

1066 
val Im_cis = thm"Im_cis"; 

1067 
val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n"; 

1068 
val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n"; 

1069 
val expi_add = thm"expi_add"; 

1070 
val expi_zero = thm"expi_zero"; 

1071 
val complex_Re_mult_eq = thm"complex_Re_mult_eq"; 

1072 
val complex_Im_mult_eq = thm"complex_Im_mult_eq"; 

1073 
val complex_expi_Ex = thm"complex_expi_Ex"; 

1074 
*} 

1075 

13957  1076 
end 
1077 

1078 