src/HOL/Complex/Complex.thy
 changeset 14377 f454b3004f8f parent 14374 61de62096768 child 14387 e96d5c42c4b0
```     1.1 --- a/src/HOL/Complex/Complex.thy	Thu Feb 05 04:30:38 2004 +0100
1.2 +++ b/src/HOL/Complex/Complex.thy	Thu Feb 05 10:45:28 2004 +0100
1.3 @@ -3,12 +3,10 @@
1.4      Copyright:   2001 University of Edinburgh
1.5  *)
1.6
1.7 -header {* Complex numbers *}
1.8 +header {* Complex Numbers: Rectangular and Polar Representations *}
1.9
1.10  theory Complex = HLog:
1.11
1.12 -subsection {* Representation of complex numbers *}
1.13 -
1.14  datatype complex = Complex real real
1.15
1.16  instance complex :: zero ..
1.17 @@ -89,7 +87,7 @@
1.18
1.19    (* abbreviation for (cos a + i sin a) *)
1.20    cis :: "real => complex"
1.21 -  "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"
1.22 +  "cis a == Complex (cos a) (sin a)"
1.23
1.24    (* abbreviation for r*(cos a + i sin a) *)
1.25    rcis :: "[real, real] => complex"
1.26 @@ -139,7 +137,7 @@
1.27
1.28  subsection{*Unary Minus*}
1.29
1.30 -lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)"
1.31 +lemma complex_minus [simp]: "- (Complex x y) = Complex (-x) (-y)"
1.33
1.34  lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
1.35 @@ -151,7 +149,8 @@
1.36
1.38
1.39 -lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
1.41 +     "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
1.43
1.44  lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)"
1.45 @@ -188,7 +187,7 @@
1.46
1.47  subsection{*Multiplication*}
1.48
1.49 -lemma complex_mult:
1.50 +lemma complex_mult [simp]:
1.51       "Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
1.53
1.54 @@ -208,7 +207,7 @@
1.55
1.56  subsection{*Inverse*}
1.57
1.58 -lemma complex_inverse:
1.59 +lemma complex_inverse [simp]:
1.60       "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
1.62
1.63 @@ -272,6 +271,28 @@
1.64
1.65  subsection{*Embedding Properties for @{term complex_of_real} Map*}
1.66
1.68 +     "Complex x y + complex_of_real r = Complex (x+r) y"
1.70 +
1.72 +     "complex_of_real r + Complex x y = Complex (r+x) y"
1.73 +by (simp add: i_def complex_of_real_def)
1.74 +
1.75 +lemma Complex_mult_complex_of_real:
1.76 +     "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
1.78 +
1.79 +lemma complex_of_real_mult_Complex:
1.80 +     "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
1.81 +by (simp add: i_def complex_of_real_def)
1.82 +
1.83 +lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
1.84 +by (simp add: i_def complex_of_real_def)
1.85 +
1.86 +lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r"
1.87 +by (simp add: i_def complex_of_real_def)
1.88 +
1.89  lemma complex_of_real_one [simp]: "complex_of_real 1 = 1"
1.90  by (simp add: complex_one_def complex_of_real_def)
1.91
1.92 @@ -313,7 +334,7 @@
1.93                   real_divide_def)
1.94  done
1.95
1.96 -lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
1.97 +lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
1.99
1.100  lemma complex_mod_zero [simp]: "cmod(0) = 0"
1.101 @@ -330,6 +351,46 @@
1.102  by simp
1.103
1.104
1.105 +subsection{*The Functions @{term Re} and @{term Im}*}
1.106 +
1.107 +lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
1.108 +by (induct z, induct w, simp add: complex_mult)
1.109 +
1.110 +lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z"
1.111 +by (induct z, induct w, simp add: complex_mult)
1.112 +
1.113 +lemma Re_i_times [simp]: "Re(ii * z) = - Im z"
1.115 +
1.116 +lemma Re_times_i [simp]: "Re(z * ii) = - Im z"
1.118 +
1.119 +lemma Im_i_times [simp]: "Im(ii * z) = Re z"
1.121 +
1.122 +lemma Im_times_i [simp]: "Im(z * ii) = Re z"
1.124 +
1.125 +lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
1.127 +
1.128 +lemma complex_Re_mult_complex_of_real [simp]:
1.129 +     "Re (z * complex_of_real c) = Re(z) * c"
1.131 +
1.132 +lemma complex_Im_mult_complex_of_real [simp]:
1.133 +     "Im (z * complex_of_real c) = Im(z) * c"
1.135 +
1.136 +lemma complex_Re_mult_complex_of_real2 [simp]:
1.137 +     "Re (complex_of_real c * z) = c * Re(z)"
1.139 +
1.140 +lemma complex_Im_mult_complex_of_real2 [simp]:
1.141 +     "Im (complex_of_real c * z) = c * Im(z)"
1.143 +
1.144 +
1.145  subsection{*Conjugation is an Automorphism*}
1.146
1.147  lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
1.148 @@ -420,14 +481,20 @@
1.149
1.150  lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
1.151  apply (induct x, induct y)
1.152 -apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric]
1.153 -         simp del: realpow_Suc)
1.154 +apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric])
1.155  apply (rule_tac n = 1 in power_inject_base)
1.156  apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
1.157  apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib
1.159  done
1.160
1.161 +lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
1.163 +
1.164 +lemma cmod_complex_polar [simp]:
1.165 +     "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
1.166 +by (simp only: cmod_unit_one complex_mod_mult, simp)
1.167 +
1.169       "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
1.170  apply (induct x, induct y)
1.171 @@ -506,10 +573,7 @@
1.172  done
1.173
1.174  lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
1.176 -
1.177 -lemma complex_inverse_divide [simp]: "inverse(x/y) = y/(x::complex)"
1.178 -by (simp add: complex_divide_def inverse_mult_distrib mult_commute)
1.179 +by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse)
1.180
1.181
1.182  subsection{*Exponentiation*}
1.183 @@ -566,20 +630,7 @@
1.185
1.186  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
1.188 -done
1.189 -
1.190 -lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
1.191 -apply (induct z)
1.193 -done
1.194 -
1.195 -(*????delete????*)
1.196 -lemma Re_complex_i [simp]: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x"
1.198 -
1.199 -lemma Im_complex_i [simp]: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
1.202
1.203  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
1.205 @@ -587,78 +638,22 @@
1.206  lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
1.207  by (simp add: i_def complex_one_def complex_mult complex_minus)
1.208
1.209 -lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) =
1.210 -      sqrt (x ^ 2 + y ^ 2)"
1.212 -
1.213 -lemma complex_eq_Re_eq:
1.214 -     "complex_of_real xa + ii * complex_of_real ya =
1.215 -      complex_of_real xb + ii * complex_of_real yb
1.216 -       ==> xa = xb"
1.218 -
1.219 -lemma complex_eq_Im_eq:
1.220 -     "complex_of_real xa + ii * complex_of_real ya =
1.221 -      complex_of_real xb + ii * complex_of_real yb
1.222 -       ==> ya = yb"
1.224 -
1.225 -(*FIXME: tidy up this mess by fixing a canonical form for complex expressions,
1.226 -e.g. x + y*ii*)
1.227 -
1.228 -lemma complex_eq_cancel_iff [iff]:
1.229 -     "(complex_of_real xa + ii * complex_of_real ya =
1.230 -       complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
1.231 -by (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
1.232 -
1.233 -lemma complex_eq_cancel_iffA [iff]:
1.234 -     "(complex_of_real xa + complex_of_real ya * ii =
1.235 -       complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
1.237 -
1.238 -lemma complex_eq_cancel_iffB [iff]:
1.239 -     "(complex_of_real xa + complex_of_real ya * ii =
1.240 -       complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
1.241 -by (auto simp add: mult_commute)
1.242 -
1.243 -lemma complex_eq_cancel_iffC [iff]:
1.244 -     "(complex_of_real xa + ii * complex_of_real ya  =
1.245 -       complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
1.246 -by (auto simp add: mult_commute)
1.247 -
1.248  lemma complex_eq_cancel_iff2 [simp]:
1.249 -     "(complex_of_real x + ii * complex_of_real y =
1.250 -      complex_of_real xa) = (x = xa & y = 0)"
1.251 -apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff)
1.252 -apply (simp del: complex_eq_cancel_iff)
1.253 -done
1.254 +     "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
1.256
1.257  lemma complex_eq_cancel_iff2a [simp]:
1.258 -     "(complex_of_real x + complex_of_real y * ii =
1.259 -      complex_of_real xa) = (x = xa & y = 0)"
1.260 -by (auto simp add: mult_commute)
1.261 +     "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
1.263
1.264 -lemma complex_eq_cancel_iff3 [simp]:
1.265 -     "(complex_of_real x + ii * complex_of_real y =
1.266 -      ii * complex_of_real ya) = (x = 0 & y = ya)"
1.267 -apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff)
1.268 -apply (simp del: complex_eq_cancel_iff)
1.269 -done
1.270 +lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)"
1.272
1.273 -lemma complex_eq_cancel_iff3a [simp]:
1.274 -     "(complex_of_real x + complex_of_real y * ii =
1.275 -      ii * complex_of_real ya) = (x = 0 & y = ya)"
1.276 -by (auto simp add: mult_commute)
1.277 +lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)"
1.279
1.280 -lemma complex_split_Re_zero:
1.281 -     "complex_of_real x + ii * complex_of_real y = 0
1.282 -      ==> x = 0"
1.284 -
1.285 -lemma complex_split_Im_zero:
1.286 -     "complex_of_real x + ii * complex_of_real y = 0
1.287 -      ==> y = 0"
1.289 +lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
1.291
1.292  lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
1.293  apply (induct z)
1.294 @@ -687,77 +682,53 @@
1.295  lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
1.296  by (auto simp add: complex_zero_def complex_of_real_def)
1.297
1.298 -lemma Re_mult_i_eq [simp]: "Re (ii * complex_of_real y) = 0"
1.299 -by (simp add: i_def complex_of_real_def complex_mult)
1.300 -
1.301 -lemma Im_mult_i_eq [simp]: "Im (ii * complex_of_real y) = y"
1.302 -by (simp add: i_def complex_of_real_def complex_mult)
1.303 -
1.304 -lemma complex_mod_mult_i [simp]: "cmod (ii * complex_of_real y) = abs y"
1.305 -by (simp add: i_def complex_of_real_def complex_mult complex_mod power2_eq_square)
1.306 -
1.307  lemma cos_arg_i_mult_zero_pos:
1.308 -   "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
1.309 +   "0 < y ==> cos (arg(Complex 0 y)) = 0"
1.310  apply (simp add: arg_def abs_if)
1.311  apply (rule_tac a = "pi/2" in someI2, auto)
1.312  apply (rule order_less_trans [of _ 0], auto)
1.313  done
1.314
1.315  lemma cos_arg_i_mult_zero_neg:
1.316 -   "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
1.317 +   "y < 0 ==> cos (arg(Complex 0 y)) = 0"
1.318  apply (simp add: arg_def abs_if)
1.319  apply (rule_tac a = "- pi/2" in someI2, auto)
1.320  apply (rule order_trans [of _ 0], auto)
1.321  done
1.322
1.323  lemma cos_arg_i_mult_zero [simp]:
1.324 -     "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
1.325 -apply (insert linorder_less_linear [of y 0])
1.326 -apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
1.327 -done
1.328 +     "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
1.329 +by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
1.330
1.331
1.332  subsection{*Finally! Polar Form for Complex Numbers*}
1.333
1.334  lemma complex_split_polar:
1.335 -     "\<exists>r a. z = complex_of_real r *
1.336 -      (complex_of_real(cos a) + ii * complex_of_real(sin a))"
1.337 -apply (cut_tac z = z in complex_split)
1.338 -apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac)
1.339 +     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
1.340 +apply (induct z)
1.341 +apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
1.342  done
1.343
1.344  lemma rcis_Ex: "\<exists>r a. z = rcis r a"
1.345 -apply (simp add: rcis_def cis_def)
1.346 -apply (rule complex_split_polar)
1.347 +apply (induct z)
1.348 +apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
1.349  done
1.350
1.351 -lemma Re_complex_polar [simp]:
1.352 -     "Re(complex_of_real r *
1.353 -      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a"
1.354 -by (auto simp add: right_distrib complex_of_real_mult mult_ac)
1.355 -
1.356  lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
1.357  by (simp add: rcis_def cis_def)
1.358
1.359 -lemma Im_complex_polar [simp]:
1.360 -     "Im(complex_of_real r *
1.361 -         (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
1.362 -      r * sin a"
1.363 -by (auto simp add: right_distrib complex_of_real_mult mult_ac)
1.364 -
1.365  lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
1.366  by (simp add: rcis_def cis_def)
1.367
1.368 -lemma complex_mod_complex_polar [simp]:
1.369 -     "cmod (complex_of_real r *
1.370 -            (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
1.371 -      abs r"
1.372 -by (auto simp add: right_distrib cmod_i complex_of_real_mult
1.373 -                      right_distrib [symmetric] power_mult_distrib mult_ac
1.374 -         simp del: realpow_Suc)
1.375 +lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
1.376 +proof -
1.377 +  have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
1.378 +    by (simp only: power_mult_distrib right_distrib)
1.379 +  thus ?thesis by simp
1.380 +qed
1.381
1.382  lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
1.383 -by (simp add: rcis_def cis_def)
1.385
1.386  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
1.388 @@ -774,24 +745,6 @@
1.389  lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
1.390  by (induct z, simp add: complex_cnj complex_mult)
1.391
1.392 -lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
1.393 -by (induct z, induct w, simp add: complex_mult)
1.394 -
1.395 -lemma complex_Re_mult_complex_of_real [simp]:
1.396 -     "Re (z * complex_of_real c) = Re(z) * c"
1.397 -by (induct z, simp add: complex_of_real_def complex_mult)
1.398 -
1.399 -lemma complex_Im_mult_complex_of_real [simp]:
1.400 -     "Im (z * complex_of_real c) = Im(z) * c"
1.401 -by (induct z, simp add: complex_of_real_def complex_mult)
1.402 -
1.403 -lemma complex_Re_mult_complex_of_real2 [simp]:
1.404 -     "Re (complex_of_real c * z) = c * Re(z)"
1.405 -by (induct z, simp add: complex_of_real_def complex_mult)
1.406 -
1.407 -lemma complex_Im_mult_complex_of_real2 [simp]:
1.408 -     "Im (complex_of_real c * z) = c * Im(z)"
1.409 -by (induct z, simp add: complex_of_real_def complex_mult)
1.410
1.411  (*---------------------------------------------------------------------------*)
1.412  (*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
1.413 @@ -801,21 +754,13 @@
1.415
1.416  lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
1.419 -apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] i_mult_eq simp del: i_mult_eq2)
1.422 -done
1.424
1.425  lemma cis_mult: "cis a * cis b = cis (a + b)"
1.426  by (simp add: cis_rcis_eq rcis_mult)
1.427
1.428  lemma cis_zero [simp]: "cis 0 = 1"
1.430 -
1.431 -lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1"
1.433 +by (simp add: cis_def complex_one_def)
1.434
1.435  lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
1.437 @@ -825,8 +770,7 @@
1.438
1.439  lemma complex_of_real_minus_one:
1.440     "complex_of_real (-(1::real)) = -(1::complex)"
1.441 -apply (simp add: complex_of_real_def complex_one_def complex_minus)
1.442 -done
1.443 +by (simp add: complex_of_real_def complex_one_def complex_minus)
1.444
1.445  lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
1.446  by (simp add: complex_mult_assoc [symmetric])
1.447 @@ -834,10 +778,7 @@
1.448
1.449  lemma cis_real_of_nat_Suc_mult:
1.450     "cis (real (Suc n) * a) = cis a * cis (real n * a)"
1.453 -apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] i_mult_eq complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] complex_of_real_minus [symmetric] real_diff_def mult_ac simp del: i_mult_eq2)
1.454 -done
1.456
1.457  lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
1.458  apply (induct_tac "n")
1.459 @@ -852,12 +793,7 @@
1.460                complex_diff_def)
1.461
1.462  lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
1.463 -apply (case_tac "r=0", simp)
1.464 -apply (auto simp add: complex_inverse_complex_split right_distrib
1.465 -            complex_of_real_mult rcis_def cis_def power2_eq_square mult_ac)
1.466 -apply (auto simp add: right_distrib [symmetric] complex_of_real_minus
1.467 -                      complex_diff_def)
1.468 -done
1.469 +by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse)
1.470
1.471  lemma cis_divide: "cis a / cis b = cis (a - b)"
1.472  by (simp add: complex_divide_def cis_mult real_diff_def)
1.473 @@ -880,35 +816,13 @@
1.474  lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
1.475  by (auto simp add: DeMoivre)
1.476
1.477 -lemma expi_Im_split:
1.478 -    "expi (ii * complex_of_real y) =
1.479 -     complex_of_real (cos y) + ii * complex_of_real (sin y)"
1.480 -by (simp add: expi_def cis_def)
1.481 -
1.482 -lemma expi_Im_cis:
1.483 -    "expi (ii * complex_of_real y) = cis y"
1.485 -
1.486  lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
1.488                cis_mult [symmetric] complex_of_real_mult mult_ac)
1.489
1.490 -lemma expi_complex_split:
1.491 -     "expi(complex_of_real x + ii * complex_of_real y) =
1.492 -      complex_of_real (exp(x)) * cis y"
1.494 -
1.495  lemma expi_zero [simp]: "expi (0::complex) = 1"
1.497
1.498 -lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
1.499 -by (induct z, induct w, simp add: complex_mult)
1.500 -
1.501 -lemma complex_Im_mult_eq:
1.502 -     "Im (w * z) = Re w * Im z + Im w * Re z"
1.503 -apply (induct z, induct w, simp add: complex_mult)
1.504 -done
1.505 -
1.506  lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
1.507  apply (insert rcis_Ex [of z])
1.508  apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
1.509 @@ -1023,46 +937,22 @@
1.510  val complexpow_minus = thm"complexpow_minus";
1.511  val complex_mod_inverse = thm"complex_mod_inverse";
1.512  val complex_mod_divide = thm"complex_mod_divide";
1.513 -val complex_inverse_divide = thm"complex_inverse_divide";
1.514  val complexpow_i_squared = thm"complexpow_i_squared";
1.515  val complex_i_not_zero = thm"complex_i_not_zero";
1.516  val sgn_zero = thm"sgn_zero";
1.517  val sgn_one = thm"sgn_one";
1.518  val sgn_minus = thm"sgn_minus";
1.519  val sgn_eq = thm"sgn_eq";
1.520 -val complex_split = thm"complex_split";
1.521 -val Re_complex_i = thm"Re_complex_i";
1.522 -val Im_complex_i = thm"Im_complex_i";
1.523  val i_mult_eq = thm"i_mult_eq";
1.524  val i_mult_eq2 = thm"i_mult_eq2";
1.525 -val cmod_i = thm"cmod_i";
1.526 -val complex_eq_Re_eq = thm"complex_eq_Re_eq";
1.527 -val complex_eq_Im_eq = thm"complex_eq_Im_eq";
1.528 -val complex_eq_cancel_iff = thm"complex_eq_cancel_iff";
1.529 -val complex_eq_cancel_iffA = thm"complex_eq_cancel_iffA";
1.530 -val complex_eq_cancel_iffB = thm"complex_eq_cancel_iffB";
1.531 -val complex_eq_cancel_iffC = thm"complex_eq_cancel_iffC";
1.532 -val complex_eq_cancel_iff2 = thm"complex_eq_cancel_iff2";
1.533 -val complex_eq_cancel_iff2a = thm"complex_eq_cancel_iff2a";
1.534 -val complex_eq_cancel_iff3 = thm"complex_eq_cancel_iff3";
1.535 -val complex_eq_cancel_iff3a = thm"complex_eq_cancel_iff3a";
1.536 -val complex_split_Re_zero = thm"complex_split_Re_zero";
1.537 -val complex_split_Im_zero = thm"complex_split_Im_zero";
1.538  val Re_sgn = thm"Re_sgn";
1.539  val Im_sgn = thm"Im_sgn";
1.540  val complex_inverse_complex_split = thm"complex_inverse_complex_split";
1.541 -val Re_mult_i_eq = thm"Re_mult_i_eq";
1.542 -val Im_mult_i_eq = thm"Im_mult_i_eq";
1.543 -val complex_mod_mult_i = thm"complex_mod_mult_i";
1.544  val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
1.545  val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
1.546 -val complex_split_polar = thm"complex_split_polar";
1.547  val rcis_Ex = thm"rcis_Ex";
1.548 -val Re_complex_polar = thm"Re_complex_polar";
1.549  val Re_rcis = thm"Re_rcis";
1.550 -val Im_complex_polar = thm"Im_complex_polar";
1.551  val Im_rcis = thm"Im_rcis";
1.552 -val complex_mod_complex_polar = thm"complex_mod_complex_polar";
1.553  val complex_mod_rcis = thm"complex_mod_rcis";
1.554  val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
1.555  val complex_Re_cnj = thm"complex_Re_cnj";
1.556 @@ -1077,7 +967,6 @@
1.557  val rcis_mult = thm"rcis_mult";
1.558  val cis_mult = thm"cis_mult";
1.559  val cis_zero = thm"cis_zero";
1.560 -val cis_zero2 = thm"cis_zero2";
1.561  val rcis_zero_mod = thm"rcis_zero_mod";
1.562  val rcis_zero_arg = thm"rcis_zero_arg";
1.563  val complex_of_real_minus_one = thm"complex_of_real_minus_one";
1.564 @@ -1093,10 +982,7 @@
1.565  val Im_cis = thm"Im_cis";
1.566  val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
1.567  val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
1.568 -val expi_Im_split = thm"expi_Im_split";
1.569 -val expi_Im_cis = thm"expi_Im_cis";