author  wenzelm 
Fri, 17 Nov 2006 02:20:03 +0100  
changeset 21404  eb85850d3eb7 
parent 20763  052b348a98a9 
child 22655  83878e551c8c 
permissions  rwrr 
13957  1 
(* Title: Complex.thy 
14430
5cb24165a2e1
new material from Avigad, and simplified treatment of division by 0
paulson
parents:
14421
diff
changeset

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

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

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

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

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

14373  14 
datatype complex = Complex real real 
13957  15 

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

18 
consts 

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

21 
consts Re :: "complex => real" 

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 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

503 

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

507 
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

508 
by (rule norm_minus_commute) 
14323  509 

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

14334  512 
by (auto intro: order_le_less_trans complex_mod_triangle_ineq) 
14323  513 

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

14334  516 
by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) 
14323  517 

14374  518 
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

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

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

521 
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

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

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

524 
qed 
14323  525 

14374  526 
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

527 
by (induct z, simp) 
14323  528 

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

529 
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

530 
by (rule zero_less_norm_iff [THEN iffD2]) 
14323  531 

532 
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

533 
by (rule norm_inverse) 
14323  534 

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

536 
by (rule norm_divide) 
14323  537 

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

538 

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

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

540 

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

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

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

543 
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

544 

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

545 

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

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

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

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

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

551 
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

552 
qed 
14323  553 

554 

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

555 
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

556 
by (rule of_real_power) 
14323  557 

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

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

560 
apply (auto simp add: complex_cnj_mult) 
14323  561 
done 
562 

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

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

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

565 

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

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

567 
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

568 

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

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

571 

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

572 

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

573 
subsection{*The Function @{term sgn}*} 
14323  574 

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

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

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

577 

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

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

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

580 

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

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

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

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

584 

14374  585 
lemma sgn_zero [simp]: "sgn 0 = 0" 
14373  586 
by (simp add: sgn_def) 
14323  587 

14374  588 
lemma sgn_one [simp]: "sgn 1 = 1" 
14373  589 
by (simp add: sgn_def) 
14323  590 

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

14373  592 
by (simp add: sgn_def) 
14323  593 

14374  594 
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" 
14377  595 
by (simp add: sgn_def) 
14323  596 

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

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

598 
by (simp add: i_def complex_of_real_def) 
14323  599 

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

601 
by (simp add: i_def complex_one_def) 
14323  602 

14374  603 
lemma complex_eq_cancel_iff2 [simp]: 
14377  604 
"(Complex x y = complex_of_real xa) = (x = xa & y = 0)" 
605 
by (simp add: complex_of_real_def) 

14323  606 

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

14323  609 

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

14323  612 

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

14323  615 

15013  616 

617 

14374  618 
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" 
15013  619 
proof (induct z) 
620 
case (Complex x y) 

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

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

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

624 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

625 
qed 

626 

14323  627 

14374  628 
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" 
15013  629 
proof (induct z) 
630 
case (Complex x y) 

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

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

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

634 
by (simp add: sgn_def complex_of_real_def divide_inverse) 

635 
qed 

14323  636 

637 
lemma complex_inverse_complex_split: 

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

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

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

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

641 
by (simp add: complex_of_real_def i_def diff_minus divide_inverse) 
14323  642 

643 
(**) 

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

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

646 
(**) 

647 

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

648 
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

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

650 

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

651 
lemma cos_arg_i_mult_zero_pos: 
14377  652 
"0 < y ==> cos (arg(Complex 0 y)) = 0" 
14373  653 
apply (simp add: arg_def abs_if) 
14334  654 
apply (rule_tac a = "pi/2" in someI2, auto) 
655 
apply (rule order_less_trans [of _ 0], auto) 

14323  656 
done 
657 

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

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

14323  663 
done 
664 

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

14323  668 

669 

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

671 

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

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

673 

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

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

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

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

677 

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

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

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

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

681 
"rcis r a = complex_of_real r * cis 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 
(* e ^ (x + iy) *) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20763
diff
changeset

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

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

687 

14374  688 
lemma complex_split_polar: 
14377  689 
"\<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

690 
apply (induct z) 
14377  691 
apply (auto simp add: polar_Ex complex_of_real_mult_Complex) 
14323  692 
done 
693 

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

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

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

14374  699 
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" 
14373  700 
by (simp add: rcis_def cis_def) 
14323  701 

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

702 
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" 
14373  703 
by (simp add: rcis_def cis_def) 
14323  704 

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

707 
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

708 
by (simp only: power_mult_distrib right_distrib) 
14377  709 
thus ?thesis by simp 
710 
qed 

14323  711 

14374  712 
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" 
14377  713 
by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) 
14323  714 

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

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

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

719 
simp del: of_real_add) 
14323  720 
done 
721 

14374  722 
lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" 
14373  723 
by (induct z, simp add: complex_cnj) 
14323  724 

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

727 

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

14373  729 
by (induct z, simp add: complex_cnj complex_mult) 
14323  730 

731 

732 
(**) 

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

734 
(**) 

735 

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

14373  737 
by (simp add: rcis_def) 
14323  738 

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

14323  742 

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

14373  744 
by (simp add: cis_rcis_eq rcis_mult) 
14323  745 

14374  746 
lemma cis_zero [simp]: "cis 0 = 1" 
14377  747 
by (simp add: cis_def complex_one_def) 
14323  748 

14374  749 
lemma rcis_zero_mod [simp]: "rcis 0 a = 0" 
14373  750 
by (simp add: rcis_def) 
14323  751 

14374  752 
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" 
14373  753 
by (simp add: rcis_def) 
14323  754 

755 
lemma complex_of_real_minus_one: 

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

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

757 
by (simp add: complex_of_real_def complex_one_def) 
14323  758 

14374  759 
lemma complex_i_mult_minus [simp]: "ii * (ii * x) =  x" 
14373  760 
by (simp add: complex_mult_assoc [symmetric]) 
14323  761 

762 

763 
lemma cis_real_of_nat_Suc_mult: 

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

14377  765 
by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) 
14323  766 

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

768 
apply (induct_tac "n") 

769 
apply (auto simp add: cis_real_of_nat_Suc_mult) 

770 
done 

771 

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

14323  774 

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

776 
by (simp add: cis_def complex_inverse_complex_split diff_minus) 
14323  777 

778 
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

779 
by (simp add: divide_inverse rcis_def complex_of_real_inverse) 
14323  780 

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

14373  782 
by (simp add: complex_divide_def cis_mult real_diff_def) 
14323  783 

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

784 
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a  b)" 
14373  785 
apply (simp add: complex_divide_def) 
786 
apply (case_tac "r2=0", simp) 

787 
apply (simp add: rcis_inverse rcis_mult real_diff_def) 

14323  788 
done 
789 

14374  790 
lemma Re_cis [simp]: "Re(cis a) = cos a" 
14373  791 
by (simp add: cis_def) 
14323  792 

14374  793 
lemma Im_cis [simp]: "Im(cis a) = sin a" 
14373  794 
by (simp add: cis_def) 
14323  795 

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

14334  797 
by (auto simp add: DeMoivre) 
14323  798 

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

14334  800 
by (auto simp add: DeMoivre) 
14323  801 

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

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

803 
by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac) 
14323  804 

14374  805 
lemma expi_zero [simp]: "expi (0::complex) = 1" 
14373  806 
by (simp add: expi_def) 
14323  807 

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

810 
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] of_real_mult) 
14334  811 
apply (rule_tac x = "ii * complex_of_real a" in exI, auto) 
14323  812 
done 
813 

814 

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

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

816 

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

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

818 

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

822 

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

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

824 
by (intro_classes, simp add: complex_number_of_def) 
15013  825 

826 

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

827 
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

828 
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

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

830 

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

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

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

833 
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

834 
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

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

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

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

838 
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

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

840 

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

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

843 

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

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

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

846 
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

847 

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

848 
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

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

850 

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

851 
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

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

853 

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

854 
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

855 
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

856 

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

857 

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

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

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

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

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

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

863 

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

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

865 

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

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

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

868 
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

869 

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

870 
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

871 
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

872 

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

873 

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

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

875 

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

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

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

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

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

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

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

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

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

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

886 

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

888 
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

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

890 

13957  891 
end 