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.32  by (simp add: complex_minus_def)
    1.33  
    1.34  lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
    1.35 @@ -151,7 +149,8 @@
    1.36  
    1.37  subsection{*Addition*}
    1.38  
    1.39 -lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
    1.40 +lemma complex_add [simp]:
    1.41 +     "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
    1.42  by (simp add: complex_add_def)
    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.52  by (simp add: complex_mult_def)
    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.61  by (simp add: complex_inverse_def)
    1.62  
    1.63 @@ -272,6 +271,28 @@
    1.64  
    1.65  subsection{*Embedding Properties for @{term complex_of_real} Map*}
    1.66  
    1.67 +lemma Complex_add_complex_of_real [simp]:
    1.68 +     "Complex x y + complex_of_real r = Complex (x+r) y"
    1.69 +by (simp add: complex_of_real_def)
    1.70 +
    1.71 +lemma complex_of_real_add_Complex [simp]:
    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.77 +by (simp add: complex_of_real_def)
    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.98  by (simp add: cmod_def)
    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.114 +by (simp add: complex_Re_mult_eq) 
   1.115 +
   1.116 +lemma Re_times_i [simp]: "Re(z * ii) = - Im z"
   1.117 +by (simp add: complex_Re_mult_eq) 
   1.118 +
   1.119 +lemma Im_i_times [simp]: "Im(ii * z) = Re z"
   1.120 +by (simp add: complex_Im_mult_eq) 
   1.121 +
   1.122 +lemma Im_times_i [simp]: "Im(z * ii) = Re z"
   1.123 +by (simp add: complex_Im_mult_eq) 
   1.124 +
   1.125 +lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
   1.126 +by (simp add: complex_Re_mult_eq)
   1.127 +
   1.128 +lemma complex_Re_mult_complex_of_real [simp]:
   1.129 +     "Re (z * complex_of_real c) = Re(z) * c"
   1.130 +by (simp add: complex_Re_mult_eq)
   1.131 +
   1.132 +lemma complex_Im_mult_complex_of_real [simp]:
   1.133 +     "Im (z * complex_of_real c) = Im(z) * c"
   1.134 +by (simp add: complex_Im_mult_eq)
   1.135 +
   1.136 +lemma complex_Re_mult_complex_of_real2 [simp]:
   1.137 +     "Re (complex_of_real c * z) = c * Re(z)"
   1.138 +by (simp add: complex_Re_mult_eq)
   1.139 +
   1.140 +lemma complex_Im_mult_complex_of_real2 [simp]:
   1.141 +     "Im (complex_of_real c * z) = c * Im(z)"
   1.142 +by (simp add: complex_Im_mult_eq)
   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.158                        add_ac mult_ac)
   1.159  done
   1.160  
   1.161 +lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
   1.162 +by (simp add: cmod_def) 
   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.168  lemma complex_mod_add_squared_eq:
   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.175 -by (simp add: complex_divide_def real_divide_def, simp add: complex_mod_mult complex_mod_inverse)
   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.184  by (simp add: sgn_def)
   1.185  
   1.186  lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
   1.187 -apply (simp add: sgn_def)
   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.192 -apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
   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.197 -by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
   1.198 -
   1.199 -lemma Im_complex_i [simp]: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
   1.200 -by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
   1.201 +by (simp add: sgn_def)
   1.202  
   1.203  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
   1.204  by (simp add: i_def complex_of_real_def complex_mult complex_add)
   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.211 -by (simp add: complex_mult complex_add i_def complex_of_real_def cmod_def)
   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.217 -by (simp add: complex_of_real_def i_def complex_mult complex_add)
   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.223 -by (simp add: complex_of_real_def i_def complex_mult complex_add)
   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.236 -by (simp add: mult_commute)
   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.255 +by (simp add: complex_of_real_def) 
   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.262 +by (simp add: complex_of_real_def)
   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.271 +by (simp add: complex_zero_def)
   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.278 +by (simp add: complex_one_def)
   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.283 -by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
   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.288 -by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
   1.289 +lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
   1.290 +by (simp add: i_def)
   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.384 +by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
   1.385  
   1.386  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
   1.387  apply (simp add: cmod_def)
   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.414  by (simp add: rcis_def)
   1.415  
   1.416  lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
   1.417 -apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib
   1.418 -                 mult_ac add_ac)
   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.420 -apply (auto simp add: add_ac)
   1.421 -apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac)
   1.422 -done
   1.423 +by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib)
   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.429 -by (simp add: cis_def)
   1.430 -
   1.431 -lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1"
   1.432 -by (simp add: cis_def)
   1.433 +by (simp add: cis_def complex_one_def)
   1.434  
   1.435  lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
   1.436  by (simp add: rcis_def)
   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.451 -apply (simp add: cis_def)
   1.452 -apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add left_distrib right_distrib complex_of_real_add complex_of_real_mult mult_ac add_ac)
   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.455 +by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
   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.484 -by (simp add: expi_def)
   1.485 -
   1.486  lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
   1.487  by (simp add: expi_def complex_Re_add exp_add complex_Im_add 
   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.493 -by (simp add: expi_def)
   1.494 -
   1.495  lemma expi_zero [simp]: "expi (0::complex) = 1"
   1.496  by (simp add: expi_def)
   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";
   1.570  val expi_add = thm"expi_add";
   1.571 -val expi_complex_split = thm"expi_complex_split";
   1.572  val expi_zero = thm"expi_zero";
   1.573  val complex_Re_mult_eq = thm"complex_Re_mult_eq";
   1.574  val complex_Im_mult_eq = thm"complex_Im_mult_eq";