author  huffman 
Mon, 07 May 2007 23:07:04 +0200  
changeset 22852  2490d4b4671a 
parent 22655  83878e551c8c 
child 22861  8ec47039614e 
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 

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" 

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 

14323  30 
defs (overloaded) 
31 

32 
complex_zero_def: 

14373  33 
"0 == Complex 0 0" 
13957  34 

14323  35 
complex_one_def: 
14373  36 
"1 == Complex 1 0" 
14323  37 

14373  38 
i_def: "ii == Complex 0 1" 
14323  39 

14373  40 
complex_minus_def: " z == Complex ( Re z) ( Im z)" 
14323  41 

42 
complex_inverse_def: 

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

13957  45 

14323  46 
complex_add_def: 
14373  47 
"z + w == Complex (Re z + Re w) (Im z + Im w)" 
13957  48 

14323  49 
complex_diff_def: 
14373  50 
"z  w == z +  (w::complex)" 
13957  51 

14374  52 
complex_mult_def: 
14373  53 
"z * w == Complex (Re z * Re w  Im z * Im w) (Re z * Im w + Im z * Re w)" 
13957  54 

14373  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 

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

14323  72 

14374  73 
lemma complex_Im_one [simp]: "Im 1 = 0" 
14373  74 
by (simp add: complex_one_def) 
14323  75 

14374  76 
lemma complex_Re_i [simp]: "Re(ii) = 0" 
14373  77 
by (simp add: i_def) 
14323  78 

14374  79 
lemma complex_Im_i [simp]: "Im(ii) = 1" 
14373  80 
by (simp add: i_def) 
14323  81 

82 

14374  83 
subsection{*Unary Minus*} 
14323  84 

14377  85 
lemma complex_minus [simp]: " (Complex x y) = Complex (x) (y)" 
14373  86 
by (simp add: complex_minus_def) 
14323  87 

14374  88 
lemma complex_Re_minus [simp]: "Re (z) =  Re z" 
14373  89 
by (simp add: complex_minus_def) 
14323  90 

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

14323  93 

94 

95 
subsection{*Addition*} 

96 

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

14373  99 
by (simp add: complex_add_def) 
14323  100 

14374  101 
lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)" 
14373  102 
by (simp add: complex_add_def) 
14323  103 

14374  104 
lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)" 
14373  105 
by (simp add: complex_add_def) 
14323  106 

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

14373  108 
by (simp add: complex_add_def add_commute) 
14323  109 

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

14373  111 
by (simp add: complex_add_def add_assoc) 
14323  112 

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

14373  114 
by (simp add: complex_add_def complex_zero_def) 
14323  115 

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

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

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

14323  121 

122 
lemma complex_diff: 

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

14323  125 

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

128 

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

130 
by (simp add: complex_diff_def) 

131 

132 

14323  133 
subsection{*Multiplication*} 
134 

14377  135 
lemma complex_mult [simp]: 
14373  136 
"Complex x1 y1 * Complex x2 y2 = Complex (x1*x2  y1*y2) (x1*y2 + y1*x2)" 
137 
by (simp add: complex_mult_def) 

14323  138 

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

14373  140 
by (simp add: complex_mult_def mult_commute add_commute) 
14323  141 

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

14374  143 
by (simp add: complex_mult_def mult_ac add_ac 
14373  144 
right_diff_distrib right_distrib left_diff_distrib left_distrib) 
14323  145 

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

14373  147 
by (simp add: complex_mult_def complex_one_def) 
14323  148 

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

14373  150 
by (simp add: complex_mult_def complex_one_def) 
14323  151 

152 

153 
subsection{*Inverse*} 

154 

14377  155 
lemma complex_inverse [simp]: 
14373  156 
"inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (y/(x ^ 2 + y ^ 2))" 
157 
by (simp add: complex_inverse_def) 

14335  158 

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

159 
lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1" 
14374  160 
apply (induct z) 
161 
apply (rename_tac x y) 

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

162 
apply (auto simp add: 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15140
diff
changeset

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

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

165 
apply (simp_all add: real_sum_squares_not_zero real_sum_squares_not_zero2) 
14323  166 
done 
167 

14335  168 

169 
subsection {* The field of complex numbers *} 

170 

171 
instance complex :: field 

172 
proof 

173 
fix z u v w :: complex 

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

14374  175 
by (rule complex_add_assoc) 
14335  176 
show "z + w = w + z" 
14374  177 
by (rule complex_add_commute) 
14335  178 
show "0 + z = z" 
14374  179 
by (rule complex_add_zero_left) 
14335  180 
show "z + z = 0" 
14374  181 
by (rule complex_add_minus_left) 
14335  182 
show "z  w = z + w" 
183 
by (simp add: complex_diff_def) 

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

14374  185 
by (rule complex_mult_assoc) 
14335  186 
show "z * w = w * z" 
14374  187 
by (rule complex_mult_commute) 
14335  188 
show "1 * z = z" 
14374  189 
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

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

193 
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

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

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

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

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

199 
by (simp add: complex_mult_inv_left) 
14335  200 
qed 
201 

14373  202 
instance complex :: division_by_zero 
203 
proof 

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

204 
show "inverse 0 = (0::complex)" 
14373  205 
by (simp add: complex_inverse_def complex_zero_def) 
206 
qed 

14335  207 

14323  208 

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

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

210 

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

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

212 

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

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

214 
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

215 

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

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

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

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

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

220 
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

221 
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

222 
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

223 
by (simp add: complex_scaleR_def left_distrib [symmetric]) 
20763  224 
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

225 
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

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

227 
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

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

229 
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

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

231 
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

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

233 

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

234 

14323  235 
subsection{*Embedding Properties for @{term complex_of_real} Map*} 
236 

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

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

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

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

240 

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

241 
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

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

243 

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

244 
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

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

246 

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

247 
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

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

249 

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

252 
by (simp add: complex_of_real_def) 

253 

254 
lemma complex_of_real_add_Complex [simp]: 

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

256 
by (simp add: i_def complex_of_real_def) 

257 

258 
lemma Complex_mult_complex_of_real: 

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

260 
by (simp add: complex_of_real_def) 

261 

262 
lemma complex_of_real_mult_Complex: 

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

264 
by (simp add: i_def complex_of_real_def) 

265 

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

267 
by (simp add: i_def complex_of_real_def) 

268 

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

270 
by (simp add: i_def complex_of_real_def) 

271 

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

272 
lemma complex_of_real_inverse: 
14374  273 
"complex_of_real(inverse x) = inverse(complex_of_real x)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

274 
by (rule of_real_inverse) 
14323  275 

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

276 
lemma complex_of_real_divide: 
15013  277 
"complex_of_real(x/y) = complex_of_real x / complex_of_real y" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

278 
by (rule of_real_divide) 
14323  279 

280 

14377  281 
subsection{*The Functions @{term Re} and @{term Im}*} 
282 

283 
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

284 
by (induct z, induct w, simp) 
14377  285 

286 
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

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

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

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

290 
by (simp add: complex_Re_mult_eq) 
14377  291 

292 
lemma Re_times_i [simp]: "Re(z * ii) =  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 Im_i_times [simp]: "Im(ii * z) = Re z" 

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

296 
by (simp add: complex_Im_mult_eq) 
14377  297 

298 
lemma Im_times_i [simp]: "Im(z * ii) = 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 complex_Re_mult: "[ Im w = 0; Im z = 0 ] ==> Re(w * z) = Re(w) * Re(z)" 

302 
by (simp add: complex_Re_mult_eq) 

303 

304 
lemma complex_Re_mult_complex_of_real [simp]: 

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

306 
by (simp add: complex_Re_mult_eq) 

307 

308 
lemma complex_Im_mult_complex_of_real [simp]: 

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

310 
by (simp add: complex_Im_mult_eq) 

311 

312 
lemma complex_Re_mult_complex_of_real2 [simp]: 

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

314 
by (simp add: complex_Re_mult_eq) 

315 

316 
lemma complex_Im_mult_complex_of_real2 [simp]: 

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

318 
by (simp add: complex_Im_mult_eq) 

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

319 

14377  320 

14323  321 
subsection{*Conjugation is an Automorphism*} 
322 

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

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

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

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

326 

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

14323  329 

14374  330 
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" 
14373  331 
by (simp add: cnj_def complex_Re_Im_cancel_iff) 
14323  332 

14374  333 
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" 
14373  334 
by (simp add: cnj_def) 
14323  335 

14374  336 
lemma complex_cnj_complex_of_real [simp]: 
14373  337 
"cnj (complex_of_real x) = complex_of_real x" 
338 
by (simp add: complex_of_real_def complex_cnj) 

14323  339 

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

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

341 
by (simp add: cnj_def) 
14323  342 

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

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

344 
by (induct z, simp add: complex_cnj power2_eq_square) 
14323  345 

346 
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

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

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

15013  350 
by (simp add: diff_minus complex_cnj_add complex_cnj_minus) 
14323  351 

352 
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

353 
by (induct w, induct z, simp add: complex_cnj) 
14323  354 

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

14373  356 
by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) 
14323  357 

14374  358 
lemma complex_cnj_one [simp]: "cnj 1 = 1" 
14373  359 
by (simp add: cnj_def complex_one_def) 
14323  360 

361 
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

362 
by (induct z, simp add: complex_cnj complex_of_real_def) 
14323  363 

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

14373  365 
apply (induct z) 
15013  366 
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

367 
complex_minus i_def complex_mult) 
14323  368 
done 
369 

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

370 
lemma complex_cnj_zero [simp]: "cnj 0 = 0" 
14334  371 
by (simp add: cnj_def complex_zero_def) 
14323  372 

14374  373 
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" 
14373  374 
by (induct z, simp add: complex_zero_def complex_cnj) 
14323  375 

376 
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

377 
by (induct z, simp add: complex_cnj complex_of_real_def power2_eq_square) 
14323  378 

379 

380 
subsection{*Modulus*} 

381 

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

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

383 

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

384 
defs (overloaded) 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

385 
complex_norm_def: "norm z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

386 

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

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

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

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

390 

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

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

392 

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

393 
lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

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

395 

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

396 
lemma complex_mod_zero [simp]: "cmod(0) = 0" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

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

398 

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

399 
lemma complex_mod_one [simp]: "cmod(1) = 1" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

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

401 

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

402 
lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

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

404 

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

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

406 
"complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

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

408 

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

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

412 
intro: real_sum_squares_cancel real_sum_squares_cancel2 
14373  413 
simp add: complex_mod complex_zero_def power2_eq_square) 
14323  414 
done 
415 

14374  416 
lemma complex_mod_complex_of_real_of_nat [simp]: 
14373  417 
"cmod (complex_of_real(real (n::nat))) = real n" 
418 
by simp 

14323  419 

14374  420 
lemma complex_mod_minus [simp]: "cmod (x) = cmod(x)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

421 
by (induct x, simp add: power2_eq_square) 
14323  422 

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

423 
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

424 
by (induct z, simp add: complex_cnj power2_eq_square) 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

425 

14323  426 
lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" 
14373  427 
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

428 
apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff) 
14323  429 
done 
430 

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

14323  433 

14374  434 
lemma complex_mod_ge_zero [simp]: "0 \<le> cmod x" 
14373  435 
by (simp add: cmod_def) 
14323  436 

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

14323  439 

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

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

443 
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

444 
apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc) 
14374  445 
apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib 
446 
add_ac mult_ac) 

14323  447 
done 
448 

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

451 

452 
lemma cmod_complex_polar [simp]: 

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

454 
by (simp only: cmod_unit_one complex_mod_mult, simp) 

455 

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

14373  458 
apply (induct x, induct y) 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

459 
apply (auto simp add: complex_mod_squared 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

460 
apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) 
14323  461 
done 
462 

14374  463 
lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \<le> cmod(x * cnj y)" 
14373  464 
apply (induct x, induct y) 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

465 
apply (auto simp add: complex_mod complex_cnj diff_def simp del: realpow_Suc) 
14323  466 
done 
467 

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

14374  471 
lemma real_sum_squared_expand: 
472 
"((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" 

14373  473 
by (simp add: left_distrib right_distrib power2_eq_square) 
14323  474 

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

14373  477 
by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric]) 
14323  478 

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

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

485 
simp add: add_increasing power2_eq_square [symmetric]) 
14323  486 
done 
487 

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

490 
by (simp only: 

491 
scaleR_conv_of_real complex_mod_mult complex_mod_complex_of_real) 

492 

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

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

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

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

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

497 
show "0 \<le> cmod x" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

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

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

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

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

502 
by (rule complex_mod_triangle_ineq) 
22852  503 
show "cmod (scaleR r x) = \<bar>r\<bar> * cmod x" 
504 
by (rule complex_norm_scaleR) 

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

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

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

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

508 

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

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

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

513 
by (rule norm_minus_commute) 
14323  514 

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

14334  517 
by (auto intro: order_le_less_trans complex_mod_triangle_ineq) 
14323  518 

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

14334  521 
by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) 
14323  522 

14374  523 
lemma complex_mod_diff_ineq [simp]: "cmod(a)  cmod(b) \<le> cmod(a + b)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

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

525 
have "cmod a  cmod b = cmod a  cmod ( b)" by simp 
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

526 
also have "\<dots> \<le> cmod (a   b)" by (rule norm_triangle_ineq2) 
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

527 
also have "\<dots> = cmod (a + b)" by simp 
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

528 
finally show ?thesis . 
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

529 
qed 
14323  530 

14374  531 
lemma complex_Re_le_cmod [simp]: "Re z \<le> cmod z" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

532 
by (induct z, simp) 
14323  533 

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

534 
lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z" 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

535 
by (rule zero_less_norm_iff [THEN iffD2]) 
14323  536 

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

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

538 
by (rule norm_inverse) 
14323  539 

14373  540 
lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

541 
by (rule norm_divide) 
14323  542 

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

543 

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

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

545 

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

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

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

548 
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

549 

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

550 

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

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

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

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

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

556 
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

557 
qed 
14323  558 

559 

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

560 
lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

561 
by (rule of_real_power) 
14323  562 

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

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

565 
apply (auto simp add: complex_cnj_mult) 
14323  566 
done 
567 

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

568 
lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n" 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

569 
by (rule norm_power) 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

570 

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

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

572 
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

573 

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

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

576 

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

577 

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

578 
subsection{*The Function @{term sgn}*} 
14323  579 

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

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

581 
(* Argand *) 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

582 

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

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

584 
"sgn z = z / complex_of_real(cmod z)" 
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

585 

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

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

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

588 
"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

589 

14374  590 
lemma sgn_zero [simp]: "sgn 0 = 0" 
14373  591 
by (simp add: sgn_def) 
14323  592 

14374  593 
lemma sgn_one [simp]: "sgn 1 = 1" 
14373  594 
by (simp add: sgn_def) 
14323  595 

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

14373  597 
by (simp add: sgn_def) 
14323  598 

14374  599 
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" 
14377  600 
by (simp add: sgn_def) 
14323  601 

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

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

603 
by (simp add: i_def complex_of_real_def) 
14323  604 

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

606 
by (simp add: i_def complex_one_def) 
14323  607 

14374  608 
lemma complex_eq_cancel_iff2 [simp]: 
14377  609 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
610 
by (simp add: complex_of_real_def) 

14323  611 

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

14323  614 

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

14323  617 

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

14323  620 

15013  621 

622 

14374  623 
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" 
15013  624 
proof (induct z) 
625 
case (Complex x y) 

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

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

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

629 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

630 
qed 

631 

14323  632 

14374  633 
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" 
15013  634 
proof (induct z) 
635 
case (Complex x y) 

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

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

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

639 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

640 
qed 

14323  641 

642 
lemma complex_inverse_complex_split: 

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

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

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

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

646 
by (simp add: complex_of_real_def i_def diff_minus divide_inverse) 
14323  647 

648 
(**) 

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

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

651 
(**) 

652 

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

653 
lemma complex_of_real_zero_iff: "(complex_of_real y = 0) = (y = 0)" 
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

654 
by (rule of_real_eq_0_iff) 
14354
988aa4648597
types complex and hcomplex are now instances of class ringpower:
paulson
parents:
14353
diff
changeset

655 

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

656 
lemma cos_arg_i_mult_zero_pos: 
14377  657 
"0 < y ==> cos (arg(Complex 0 y)) = 0" 
14373  658 
apply (simp add: arg_def abs_if) 
14334  659 
apply (rule_tac a = "pi/2" in someI2, auto) 
660 
apply (rule order_less_trans [of _ 0], auto) 

14323  661 
done 
662 

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

663 
lemma cos_arg_i_mult_zero_neg: 
14377  664 
"y < 0 ==> cos (arg(Complex 0 y)) = 0" 
14373  665 
apply (simp add: arg_def abs_if) 
14334  666 
apply (rule_tac a = " pi/2" in someI2, auto) 
667 
apply (rule order_trans [of _ 0], auto) 

14323  668 
done 
669 

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

14323  673 

674 

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

676 

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

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

678 

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

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

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

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

682 

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

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

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

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

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

687 

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

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

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

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

691 
"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

692 

14374  693 
lemma complex_split_polar: 
14377  694 
"\<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

695 
apply (induct z) 
14377  696 
apply (auto simp add: polar_Ex complex_of_real_mult_Complex) 
14323  697 
done 
698 

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

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

700 
apply (induct z) 
14377  701 
apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex) 
14323  702 
done 
703 

14374  704 
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" 
14373  705 
by (simp add: rcis_def cis_def) 
14323  706 

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

707 
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" 
14373  708 
by (simp add: rcis_def cis_def) 
14323  709 

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

712 
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

713 
by (simp only: power_mult_distrib right_distrib) 
14377  714 
thus ?thesis by simp 
715 
qed 

14323  716 

14374  717 
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" 
14377  718 
by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) 
14323  719 

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

14373  721 
apply (simp add: cmod_def) 
14323  722 
apply (rule real_sqrt_eq_iff [THEN iffD2]) 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

723 
apply (auto simp add: complex_mult_cnj 
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

724 
simp del: of_real_add) 
14323  725 
done 
726 

14374  727 
lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" 
14373  728 
by (induct z, simp add: complex_cnj) 
14323  729 

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

732 

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

14373  734 
by (induct z, simp add: complex_cnj complex_mult) 
14323  735 

736 

737 
(**) 

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

739 
(**) 

740 

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

14373  742 
by (simp add: rcis_def) 
14323  743 

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

14323  747 

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

14373  749 
by (simp add: cis_rcis_eq rcis_mult) 
14323  750 

14374  751 
lemma cis_zero [simp]: "cis 0 = 1" 
14377  752 
by (simp add: cis_def complex_one_def) 
14323  753 

14374  754 
lemma rcis_zero_mod [simp]: "rcis 0 a = 0" 
14373  755 
by (simp add: rcis_def) 
14323  756 

14374  757 
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" 
14373  758 
by (simp add: rcis_def) 
14323  759 

760 
lemma complex_of_real_minus_one: 

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

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

762 
by (simp add: complex_of_real_def complex_one_def) 
14323  763 

14374  764 
lemma complex_i_mult_minus [simp]: "ii * (ii * x) =  x" 
14373  765 
by (simp add: complex_mult_assoc [symmetric]) 
14323  766 

767 

768 
lemma cis_real_of_nat_Suc_mult: 

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

14377  770 
by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) 
14323  771 

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

773 
apply (induct_tac "n") 

774 
apply (auto simp add: cis_real_of_nat_Suc_mult) 

775 
done 

776 

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

14323  779 

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

781 
by (simp add: cis_def complex_inverse_complex_split diff_minus) 
14323  782 

783 
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

784 
by (simp add: divide_inverse rcis_def complex_of_real_inverse) 
14323  785 

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

14373  787 
by (simp add: complex_divide_def cis_mult real_diff_def) 
14323  788 

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

789 
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a  b)" 
14373  790 
apply (simp add: complex_divide_def) 
791 
apply (case_tac "r2=0", simp) 

792 
apply (simp add: rcis_inverse rcis_mult real_diff_def) 

14323  793 
done 
794 

14374  795 
lemma Re_cis [simp]: "Re(cis a) = cos a" 
14373  796 
by (simp add: cis_def) 
14323  797 

14374  798 
lemma Im_cis [simp]: "Im(cis a) = sin a" 
14373  799 
by (simp add: cis_def) 
14323  800 

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

14334  802 
by (auto simp add: DeMoivre) 
14323  803 

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

14334  805 
by (auto simp add: DeMoivre) 
14323  806 

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

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

808 
by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac) 
14323  809 

14374  810 
lemma expi_zero [simp]: "expi (0::complex) = 1" 
14373  811 
by (simp add: expi_def) 
14323  812 

14374  813 
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a" 
14373  814 
apply (insert rcis_Ex [of z]) 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

815 
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] of_real_mult) 
14334  816 
apply (rule_tac x = "ii * complex_of_real a" in exI, auto) 
14323  817 
done 
818 

819 

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

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

821 

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

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

823 

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

827 

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

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

829 
by (intro_classes, simp add: complex_number_of_def) 
15013  830 

831 

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

832 
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

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

834 
by (rule of_real_number_of_eq) 
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 
text{*This theorem is necessary because theorems such as 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

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

838 
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

839 
They work for type complex because the reals can be embedded in them.*} 
20557
81dd3679f92c
complex_of_real abbreviates of_real::real=>complex;
huffman
parents:
20556
diff
changeset

840 
(* TODO: generalize and move to Real/RealVector.thy *) 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

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

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

843 
by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] 
20725
72e20198f834
instance complex :: real_normed_field; cleaned up
huffman
parents:
20560
diff
changeset

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

845 

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

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

848 

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

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

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

851 
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

852 

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

853 
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

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

855 

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

856 
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

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

858 

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

859 
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

860 
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

861 

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

862 

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

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

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

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

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

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

868 

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

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

870 

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

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

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

873 
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

874 

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

875 
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

876 
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

877 

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 
fun test s = (Goal s; by (Asm_simp_tac 1)); 
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14377
diff
changeset

880 

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

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

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

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

884 
test "a*(b*c) = d*(b::complex)*(x*a)"; 
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 

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

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

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

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

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

891 

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

893 
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

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

895 

13957  896 
end 