author  huffman 
Tue, 29 May 2007 20:53:13 +0200  
changeset 23124  892e0a4551da 
parent 23123  e2e370bccde1 
child 23125  6f7b5b96241f 
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 
22655  11 
imports "../Hyperreal/Transcendental" 
15131  12 
begin 
13957  13 

14373  14 
datatype complex = Complex real real 
13957  15 

23124  16 
definition 
14373  17 
"ii" :: complex ("\<i>") 
23124  18 
where 
19 
i_def: "ii == Complex 0 1" 

14373  20 

21 
consts Re :: "complex => real" 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

22 
primrec Re: "Re (Complex x y) = x" 
14373  23 

24 
consts Im :: "complex => real" 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

25 
primrec Im: "Im (Complex x y) = y" 
14373  26 

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

28 
by (induct z) simp 

13957  29 

23124  30 
instance complex :: zero 
14323  31 
complex_zero_def: 
23124  32 
"0 == Complex 0 0" .. 
13957  33 

23124  34 
instance complex :: one 
14323  35 
complex_one_def: 
23124  36 
"1 == Complex 1 0" .. 
37 

38 
instance complex :: plus 

39 
complex_add_def: 

40 
"z + w == Complex (Re z + Re w) (Im z + Im w)" .. 

14323  41 

23124  42 
instance complex :: minus 
43 
complex_minus_def: " z == Complex ( Re z) ( Im z)" 

44 
complex_diff_def: 

45 
"z  w == z +  (w::complex)" .. 

14323  46 

23124  47 
instance complex :: times 
48 
complex_mult_def: 

49 
"z * w == Complex (Re z * Re w  Im z * Im w) (Re z * Im w + Im z * Re w)" .. 

14323  50 

23124  51 
instance complex :: inverse 
14323  52 
complex_inverse_def: 
14373  53 
"inverse z == 
54 
Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) ( Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))" 

23124  55 
complex_divide_def: "w / (z::complex) == w * inverse z" .. 
14323  56 

13957  57 

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

14323  60 

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

14373  62 
by (induct w, induct z, simp) 
14323  63 

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

66 

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

14373  68 
by (simp add: complex_zero_def) 
14323  69 

22968  70 
lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 \<and> y = 0)" 
71 
by (simp add: complex_zero_def) 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

72 

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

14323  75 

14374  76 
lemma complex_Im_one [simp]: "Im 1 = 0" 
14373  77 
by (simp add: complex_one_def) 
14323  78 

22968  79 
lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 \<and> y = 0)" 
80 
by (simp add: complex_one_def) 

81 

14374  82 
lemma complex_Re_i [simp]: "Re(ii) = 0" 
14373  83 
by (simp add: i_def) 
14323  84 

14374  85 
lemma complex_Im_i [simp]: "Im(ii) = 1" 
14373  86 
by (simp add: i_def) 
14323  87 

22968  88 
lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)" 
89 
by (simp add: i_def) 

90 

14323  91 

14374  92 
subsection{*Unary Minus*} 
14323  93 

14377  94 
lemma complex_minus [simp]: " (Complex x y) = Complex (x) (y)" 
14373  95 
by (simp add: complex_minus_def) 
14323  96 

14374  97 
lemma complex_Re_minus [simp]: "Re (z) =  Re z" 
14373  98 
by (simp add: complex_minus_def) 
14323  99 

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

14323  102 

103 

104 
subsection{*Addition*} 

105 

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

14373  108 
by (simp add: complex_add_def) 
14323  109 

14374  110 
lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)" 
14373  111 
by (simp add: complex_add_def) 
14323  112 

14374  113 
lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)" 
14373  114 
by (simp add: complex_add_def) 
14323  115 

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

14373  117 
by (simp add: complex_add_def add_commute) 
14323  118 

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

14373  120 
by (simp add: complex_add_def add_assoc) 
14323  121 

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

14373  123 
by (simp add: complex_add_def complex_zero_def) 
14323  124 

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

14373  126 
by (simp add: complex_add_def complex_zero_def) 
14323  127 

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

14323  130 

131 
lemma complex_diff: 

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

14323  134 

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

137 

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

139 
by (simp add: complex_diff_def) 

140 

141 

14323  142 
subsection{*Multiplication*} 
143 

14377  144 
lemma complex_mult [simp]: 
14373  145 
"Complex x1 y1 * Complex x2 y2 = Complex (x1*x2  y1*y2) (x1*y2 + y1*x2)" 
146 
by (simp add: complex_mult_def) 

14323  147 

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

14373  149 
by (simp add: complex_mult_def mult_commute add_commute) 
14323  150 

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

14374  152 
by (simp add: complex_mult_def mult_ac add_ac 
14373  153 
right_diff_distrib right_distrib left_diff_distrib left_distrib) 
14323  154 

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

14373  156 
by (simp add: complex_mult_def complex_one_def) 
14323  157 

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

14373  159 
by (simp add: complex_mult_def complex_one_def) 
14323  160 

161 

162 
subsection{*Inverse*} 

163 

14377  164 
lemma complex_inverse [simp]: 
22968  165 
"inverse (Complex x y) = Complex (x / (x\<twosuperior> + y\<twosuperior>)) ( y / (x\<twosuperior> + y\<twosuperior>))" 
14373  166 
by (simp add: complex_inverse_def) 
14335  167 

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

168 
lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1" 
14374  169 
apply (induct z) 
22968  170 
apply (simp add: power2_eq_square [symmetric] add_divide_distrib [symmetric]) 
14323  171 
done 
172 

14335  173 

174 
subsection {* The field of complex numbers *} 

175 

176 
instance complex :: field 

177 
proof 

178 
fix z u v w :: complex 

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

14374  180 
by (rule complex_add_assoc) 
14335  181 
show "z + w = w + z" 
14374  182 
by (rule complex_add_commute) 
14335  183 
show "0 + z = z" 
14374  184 
by (rule complex_add_zero_left) 
14335  185 
show "z + z = 0" 
14374  186 
by (rule complex_add_minus_left) 
14335  187 
show "z  w = z + w" 
188 
by (simp add: complex_diff_def) 

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

14374  190 
by (rule complex_mult_assoc) 
14335  191 
show "z * w = w * z" 
14374  192 
by (rule complex_mult_commute) 
14335  193 
show "1 * z = z" 
14374  194 
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

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

198 
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

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

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

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

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

204 
by (simp add: complex_mult_inv_left) 
14335  205 
qed 
206 

14373  207 
instance complex :: division_by_zero 
208 
proof 

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

209 
show "inverse 0 = (0::complex)" 
14373  210 
by (simp add: complex_inverse_def complex_zero_def) 
211 
qed 

14335  212 

14323  213 

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

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

215 

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

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

217 

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

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

219 
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

220 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

221 
lemma Re_scaleR [simp]: "Re (scaleR r x) = r * Re x" 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

222 
unfolding complex_scaleR_def by (induct x, simp) 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

223 

3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

224 
lemma Im_scaleR [simp]: "Im (scaleR r x) = r * Im x" 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

225 
unfolding complex_scaleR_def by (induct x, simp) 
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

226 

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

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

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

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

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

231 
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

232 
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

233 
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

234 
by (simp add: complex_scaleR_def left_distrib [symmetric]) 
20763  235 
show "a *# b *# x = (a * b) *# x" 
20556
2e8227b81bf1
add instance for real_algebra_1 and real_normed_div_algebra
huffman
parents:
20485
diff
changeset

236 
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

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

238 
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

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

240 
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

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

242 
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

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

244 

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

245 

14323  246 
subsection{*Embedding Properties for @{term complex_of_real} Map*} 
247 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

248 
abbreviation 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

249 
complex_of_real :: "real => complex" where 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

250 
"complex_of_real == of_real" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

251 

81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

252 
lemma complex_of_real_def: "complex_of_real r = Complex r 0" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

253 
by (simp add: of_real_def complex_scaleR_def) 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

254 

81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

255 
lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

256 
by (simp add: complex_of_real_def) 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

257 

81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

258 
lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

259 
by (simp add: complex_of_real_def) 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

260 

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

263 
by (simp add: complex_of_real_def) 

264 

265 
lemma complex_of_real_add_Complex [simp]: 

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

267 
by (simp add: i_def complex_of_real_def) 

268 

269 
lemma Complex_mult_complex_of_real: 

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

271 
by (simp add: complex_of_real_def) 

272 

273 
lemma complex_of_real_mult_Complex: 

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

275 
by (simp add: i_def complex_of_real_def) 

276 

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

278 
by (simp add: i_def complex_of_real_def) 

279 

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

281 
by (simp add: i_def complex_of_real_def) 

282 

14323  283 

14377  284 
subsection{*The Functions @{term Re} and @{term Im}*} 
285 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

287 
by (induct z, induct w, simp) 
14377  288 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

290 
by (induct z, induct w, simp) 
14377  291 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

293 
by (simp add: complex_Re_mult_eq) 
14377  294 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

296 
by (simp add: complex_Re_mult_eq) 
14377  297 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

299 
by (simp add: complex_Im_mult_eq) 
14377  300 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

302 
by (simp add: complex_Im_mult_eq) 
14377  303 

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

305 
by (simp add: complex_Re_mult_eq) 

306 

307 
lemma complex_Re_mult_complex_of_real [simp]: 

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

309 
by (simp add: complex_Re_mult_eq) 

310 

311 
lemma complex_Im_mult_complex_of_real [simp]: 

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

313 
by (simp add: complex_Im_mult_eq) 

314 

315 
lemma complex_Re_mult_complex_of_real2 [simp]: 

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

317 
by (simp add: complex_Re_mult_eq) 

318 

319 
lemma complex_Im_mult_complex_of_real2 [simp]: 

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

321 
by (simp add: complex_Im_mult_eq) 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

322 

14377  323 

14323  324 
subsection{*Conjugation is an Automorphism*} 
325 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

326 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

327 
cnj :: "complex => complex" where 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

328 
"cnj z = Complex (Re z) (Im z)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

329 

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

14323  332 

14374  333 
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" 
14373  334 
by (simp add: cnj_def complex_Re_Im_cancel_iff) 
14323  335 

14374  336 
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" 
14373  337 
by (simp add: cnj_def) 
14323  338 

14374  339 
lemma complex_cnj_complex_of_real [simp]: 
14373  340 
"cnj (complex_of_real x) = complex_of_real x" 
341 
by (simp add: complex_of_real_def complex_cnj) 

14323  342 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

344 
by (simp add: cnj_def) 
14323  345 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

347 
by (induct z, simp add: complex_cnj power2_eq_square) 
14323  348 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

350 
by (induct w, induct z, simp add: complex_cnj) 
14323  351 

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

15013  353 
by (simp add: diff_minus complex_cnj_add complex_cnj_minus) 
14323  354 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

356 
by (induct w, induct z, simp add: complex_cnj) 
14323  357 

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

14373  359 
by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) 
14323  360 

14374  361 
lemma complex_cnj_one [simp]: "cnj 1 = 1" 
14373  362 
by (simp add: cnj_def complex_one_def) 
14323  363 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

365 
by (induct z, simp add: complex_cnj complex_of_real_def) 
14323  366 

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

14373  368 
apply (induct z) 
15013  369 
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

370 
complex_minus i_def complex_mult) 
14323  371 
done 
372 

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

373 
lemma complex_cnj_zero [simp]: "cnj 0 = 0" 
14334  374 
by (simp add: cnj_def complex_zero_def) 
14323  375 

14374  376 
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" 
14373  377 
by (induct z, simp add: complex_zero_def complex_cnj) 
14323  378 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

380 
by (induct z, simp add: complex_cnj complex_of_real_def power2_eq_square) 
14323  381 

382 

383 
subsection{*Modulus*} 

384 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

385 
instance complex :: norm 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

386 
complex_norm_def: "norm z \<equiv> sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" .. 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

387 

81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

388 
abbreviation 
22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

389 
cmod :: "complex \<Rightarrow> real" where 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

390 
"cmod \<equiv> norm" 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

391 

81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

392 
lemmas cmod_def = complex_norm_def 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

393 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

394 
lemma complex_mod [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)" 
14373  395 
by (simp add: cmod_def) 
14323  396 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

397 
lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod x + cmod y" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

398 
apply (simp add: cmod_def) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

399 
apply (rule real_sqrt_sum_squares_triangle_ineq) 
14323  400 
done 
401 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

402 
lemma complex_mod_mult: "cmod (x * y) = cmod x * cmod y" 
14373  403 
apply (induct x, induct y) 
22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

404 
apply (simp add: real_sqrt_mult_distrib [symmetric]) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

405 
apply (simp add: power2_sum power2_diff power_mult_distrib ring_distrib) 
14323  406 
done 
407 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

408 
lemma complex_mod_complex_of_real: "cmod (complex_of_real x) = \<bar>x\<bar>" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

409 
by (simp add: complex_of_real_def) 
14323  410 

22852  411 
lemma complex_norm_scaleR: 
412 
"norm (scaleR a x) = \<bar>a\<bar> * norm (x::complex)" 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

413 
unfolding scaleR_conv_of_real 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

414 
by (simp only: complex_mod_mult complex_mod_complex_of_real) 
22852  415 

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

416 
instance complex :: real_normed_field 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

417 
proof 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

418 
fix r :: real 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

419 
fix x y :: complex 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

420 
show "0 \<le> cmod x" 
22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

421 
by (induct x) simp 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

422 
show "(cmod x = 0) = (x = 0)" 
22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

423 
by (induct x) simp 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

424 
show "cmod (x + y) \<le> cmod x + cmod y" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

425 
by (rule complex_mod_triangle_ineq) 
22852  426 
show "cmod (scaleR r x) = \<bar>r\<bar> * cmod x" 
427 
by (rule complex_norm_scaleR) 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

428 
show "cmod (x * y) = cmod x * cmod y" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

429 
by (rule complex_mod_mult) 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

430 
qed 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

431 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

432 
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

433 
by (induct z, simp add: complex_cnj) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

434 

8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

435 
lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

436 
by (simp add: complex_mod_mult power2_eq_square) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

437 

8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

438 
lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

439 
by simp 
14323  440 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

441 
lemma cmod_complex_polar [simp]: 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

442 
"cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

443 
apply (simp only: cmod_unit_one complex_mod_mult) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

444 
apply (simp add: complex_mod_complex_of_real) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

445 
done 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

446 

8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

447 
lemma complex_Re_le_cmod: "Re x \<le> cmod x" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

448 
unfolding complex_norm_def 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

449 
by (rule real_sqrt_sum_squares_ge1) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

450 

8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

451 
lemma complex_mod_minus_le_complex_mod [simp]: " cmod x \<le> cmod x" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

452 
by (rule order_trans [OF _ norm_ge_zero], simp) 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

453 

8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

454 
lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a)  cmod b \<le> cmod a" 
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

455 
by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) 
14323  456 

22861
8ec47039614e
clean up complex norm proofs, remove redundant lemmas
huffman
parents:
22852
diff
changeset

457 
lemmas real_sum_squared_expand = power2_sum [where 'a=real] 
14323  458 

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

459 

23123  460 
subsection {* Completeness of the Complexes *} 
461 

462 
interpretation Re: bounded_linear ["Re"] 

463 
apply (unfold_locales, simp, simp) 

464 
apply (rule_tac x=1 in exI) 

465 
apply (simp add: complex_norm_def) 

466 
done 

467 

468 
interpretation Im: bounded_linear ["Im"] 

469 
apply (unfold_locales, simp, simp) 

470 
apply (rule_tac x=1 in exI) 

471 
apply (simp add: complex_norm_def) 

472 
done 

473 

474 
lemma LIMSEQ_Complex: 

475 
"\<lbrakk>X > a; Y > b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) > Complex a b" 

476 
apply (rule LIMSEQ_I) 

477 
apply (subgoal_tac "0 < r / sqrt 2") 

478 
apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe) 

479 
apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe) 

480 
apply (rename_tac M N, rule_tac x="max M N" in exI, safe) 

481 
apply (simp add: complex_diff) 

482 
apply (simp add: real_sqrt_sum_squares_less) 

483 
apply (simp add: divide_pos_pos) 

484 
done 

485 

486 
instance complex :: banach 

487 
proof 

488 
fix X :: "nat \<Rightarrow> complex" 

489 
assume X: "Cauchy X" 

490 
from Re.Cauchy [OF X] have 1: "(\<lambda>n. Re (X n)) > lim (\<lambda>n. Re (X n))" 

491 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 

492 
from Im.Cauchy [OF X] have 2: "(\<lambda>n. Im (X n)) > lim (\<lambda>n. Im (X n))" 

493 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 

494 
have "X > Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))" 

495 
using LIMSEQ_Complex [OF 1 2] by simp 

496 
thus "convergent X" 

497 
by (rule convergentI) 

498 
qed 

499 

500 

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

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

502 

23124  503 
instance complex :: power .. 
504 

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

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

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

507 
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

508 

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

509 

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

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

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

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

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

515 
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

516 
qed 
14323  517 

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

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

520 
apply (auto simp add: complex_cnj_mult) 
14323  521 
done 
522 

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

523 
lemma complexpow_i_squared [simp]: "ii ^ 2 = (1::complex)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

524 
by (simp add: i_def complex_one_def numeral_2_eq_2) 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

525 

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

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

528 

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

529 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

530 
subsection{*The Functions @{term sgn} and @{term arg}*} 
14323  531 

22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

532 
text {* Argand *} 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

533 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

534 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

535 
arg :: "complex => real" where 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

536 
"arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & pi < a & a \<le> pi)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

537 

14374  538 
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

539 
by (simp add: sgn_def divide_inverse scaleR_conv_of_real mult_commute) 
14323  540 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

542 
by (simp add: i_def complex_of_real_def) 
14323  543 

14374  544 
lemma i_mult_eq2 [simp]: "ii * ii = (1::complex)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

545 
by (simp add: i_def complex_one_def) 
14323  546 

14374  547 
lemma complex_eq_cancel_iff2 [simp]: 
14377  548 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
549 
by (simp add: complex_of_real_def) 

14323  550 

14374  551 
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

552 
unfolding sgn_def by (simp add: divide_inverse) 
14323  553 

14374  554 
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" 
22972
3e96b98d37c6
generalized sgn function to work on any real normed vector space
huffman
parents:
22968
diff
changeset

555 
unfolding sgn_def by (simp add: divide_inverse) 
14323  556 

557 
lemma complex_inverse_complex_split: 

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

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

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

561 
by (simp add: complex_of_real_def i_def diff_minus divide_inverse) 
14323  562 

563 
(**) 

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

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

566 
(**) 

567 

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

568 
lemma cos_arg_i_mult_zero_pos: 
14377  569 
"0 < y ==> cos (arg(Complex 0 y)) = 0" 
14373  570 
apply (simp add: arg_def abs_if) 
14334  571 
apply (rule_tac a = "pi/2" in someI2, auto) 
572 
apply (rule order_less_trans [of _ 0], auto) 

14323  573 
done 
574 

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

575 
lemma cos_arg_i_mult_zero_neg: 
14377  576 
"y < 0 ==> cos (arg(Complex 0 y)) = 0" 
14373  577 
apply (simp add: arg_def abs_if) 
14334  578 
apply (rule_tac a = " pi/2" in someI2, auto) 
579 
apply (rule order_trans [of _ 0], auto) 

14323  580 
done 
581 

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

14323  585 

586 

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

588 

20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

589 
definition 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

590 

81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

591 
(* abbreviation for (cos a + i sin a) *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

592 
cis :: "real => complex" where 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

593 
"cis a = Complex (cos a) (sin a)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

594 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

595 
definition 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

596 
(* abbreviation for r*(cos a + i sin a) *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

597 
rcis :: "[real, real] => complex" where 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

598 
"rcis r a = complex_of_real r * cis a" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

599 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

600 
definition 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

601 
(* e ^ (x + iy) *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

602 
expi :: "complex => complex" where 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

603 
"expi z = complex_of_real(exp (Re z)) * cis (Im z)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

604 

14374  605 
lemma complex_split_polar: 
14377  606 
"\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

607 
apply (induct z) 
14377  608 
apply (auto simp add: polar_Ex complex_of_real_mult_Complex) 
14323  609 
done 
610 

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

611 
lemma rcis_Ex: "\<exists>r a. z = rcis r a" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

612 
apply (induct z) 
14377  613 
apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex) 
14323  614 
done 
615 

14374  616 
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" 
14373  617 
by (simp add: rcis_def cis_def) 
14323  618 

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

619 
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" 
14373  620 
by (simp add: rcis_def cis_def) 
14323  621 

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

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

625 
by (simp only: power_mult_distrib right_distrib) 
14377  626 
thus ?thesis by simp 
627 
qed 

14323  628 

14374  629 
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" 
14377  630 
by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) 
14323  631 

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

14373  633 
apply (simp add: cmod_def) 
22956
617140080e6a
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman
parents:
22914
diff
changeset

634 
apply (simp add: complex_mult_cnj del: of_real_add) 
14323  635 
done 
636 

14374  637 
lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" 
14373  638 
by (induct z, simp add: complex_cnj) 
14323  639 

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

642 

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

14373  644 
by (induct z, simp add: complex_cnj complex_mult) 
14323  645 

646 

647 
(**) 

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

649 
(**) 

650 

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

14373  652 
by (simp add: rcis_def) 
14323  653 

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

14323  657 

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

14373  659 
by (simp add: cis_rcis_eq rcis_mult) 
14323  660 

14374  661 
lemma cis_zero [simp]: "cis 0 = 1" 
14377  662 
by (simp add: cis_def complex_one_def) 
14323  663 

14374  664 
lemma rcis_zero_mod [simp]: "rcis 0 a = 0" 
14373  665 
by (simp add: rcis_def) 
14323  666 

14374  667 
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" 
14373  668 
by (simp add: rcis_def) 
14323  669 

670 
lemma complex_of_real_minus_one: 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

672 
by (simp add: complex_of_real_def complex_one_def) 
14323  673 

14374  674 
lemma complex_i_mult_minus [simp]: "ii * (ii * x) =  x" 
14373  675 
by (simp add: complex_mult_assoc [symmetric]) 
14323  676 

677 

678 
lemma cis_real_of_nat_Suc_mult: 

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

14377  680 
by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) 
14323  681 

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

683 
apply (induct_tac "n") 

684 
apply (auto simp add: cis_real_of_nat_Suc_mult) 

685 
done 

686 

14374  687 
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" 
22890  688 
by (simp add: rcis_def power_mult_distrib DeMoivre) 
14323  689 

14374  690 
lemma cis_inverse [simp]: "inverse(cis a) = cis (a)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

691 
by (simp add: cis_def complex_inverse_complex_split diff_minus) 
14323  692 

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

22884  694 
by (simp add: divide_inverse rcis_def) 
14323  695 

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

14373  697 
by (simp add: complex_divide_def cis_mult real_diff_def) 
14323  698 

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

699 
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a  b)" 
14373  700 
apply (simp add: complex_divide_def) 
701 
apply (case_tac "r2=0", simp) 

702 
apply (simp add: rcis_inverse rcis_mult real_diff_def) 

14323  703 
done 
704 

14374  705 
lemma Re_cis [simp]: "Re(cis a) = cos a" 
14373  706 
by (simp add: cis_def) 
14323  707 

14374  708 
lemma Im_cis [simp]: "Im(cis a) = sin a" 
14373  709 
by (simp add: cis_def) 
14323  710 

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

14334  712 
by (auto simp add: DeMoivre) 
14323  713 

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

14334  715 
by (auto simp add: DeMoivre) 
14323  716 

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

20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

718 
by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac) 
14323  719 

14374  720 
lemma expi_zero [simp]: "expi (0::complex) = 1" 
14373  721 
by (simp add: expi_def) 
14323  722 

14374  723 
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a" 
14373  724 
apply (insert rcis_Ex [of z]) 
22884  725 
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric]) 
14334  726 
apply (rule_tac x = "ii * complex_of_real a" in exI, auto) 
14323  727 
done 
728 

729 

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

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

731 

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

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

733 

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

737 

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

738 
instance complex :: number_ring 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

739 
by (intro_classes, simp add: complex_number_of_def) 
15013  740 

22914  741 
lemma complex_number_of: "complex_of_real (number_of w) = number_of w" 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

742 
by (rule of_real_number_of_eq) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

743 

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

744 
lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v" 
15481  745 
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

746 

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

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

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

749 
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

750 

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

751 
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

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

753 

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

754 
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

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

756 

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

757 
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

758 
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

759 

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

760 

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

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

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

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

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

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

766 

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

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

768 

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

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

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

771 
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

772 

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

773 
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

774 
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

775 

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

776 

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

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

778 

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

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

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

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

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

783 

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

784 

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

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

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

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

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

789 

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

791 
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

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

793 

13957  794 
end 