src/HOL/Complex/Complex.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15234 ec91a90c604e
permissions -rw-r--r--
import -> imports
     1 (*  Title:       Complex.thy
     2     ID:      $Id$
     3     Author:      Jacques D. Fleuriot
     4     Copyright:   2001 University of Edinburgh
     5     Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
     6 *)
     7 
     8 header {* Complex Numbers: Rectangular and Polar Representations *}
     9 
    10 theory Complex
    11 imports "../Hyperreal/HLog"
    12 begin
    13 
    14 datatype complex = Complex real real
    15 
    16 instance complex :: "{zero, one, plus, times, minus, inverse, power}" ..
    17 
    18 consts
    19   "ii"    :: complex    ("\<i>")
    20 
    21 consts Re :: "complex => real"
    22 primrec "Re (Complex x y) = x"
    23 
    24 consts Im :: "complex => real"
    25 primrec "Im (Complex x y) = y"
    26 
    27 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
    28   by (induct z) simp
    29 
    30 constdefs
    31 
    32   (*----------- modulus ------------*)
    33 
    34   cmod :: "complex => real"
    35   "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"
    36 
    37   (*----- injection from reals -----*)
    38 
    39   complex_of_real :: "real => complex"
    40   "complex_of_real r == Complex r 0"
    41 
    42   (*------- complex conjugate ------*)
    43 
    44   cnj :: "complex => complex"
    45   "cnj z == Complex (Re z) (-Im z)"
    46 
    47   (*------------ Argand -------------*)
    48 
    49   sgn :: "complex => complex"
    50   "sgn z == z / complex_of_real(cmod z)"
    51 
    52   arg :: "complex => real"
    53   "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"
    54 
    55 
    56 defs (overloaded)
    57 
    58   complex_zero_def:
    59   "0 == Complex 0 0"
    60 
    61   complex_one_def:
    62   "1 == Complex 1 0"
    63 
    64   i_def: "ii == Complex 0 1"
    65 
    66   complex_minus_def: "- z == Complex (- Re z) (- Im z)"
    67 
    68   complex_inverse_def:
    69    "inverse z ==
    70     Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) (- Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))"
    71 
    72   complex_add_def:
    73     "z + w == Complex (Re z + Re w) (Im z + Im w)"
    74 
    75   complex_diff_def:
    76     "z - w == z + - (w::complex)"
    77 
    78   complex_mult_def:
    79     "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)"
    80 
    81   complex_divide_def: "w / (z::complex) == w * inverse z"
    82 
    83 
    84 constdefs
    85 
    86   (* abbreviation for (cos a + i sin a) *)
    87   cis :: "real => complex"
    88   "cis a == Complex (cos a) (sin a)"
    89 
    90   (* abbreviation for r*(cos a + i sin a) *)
    91   rcis :: "[real, real] => complex"
    92   "rcis r a == complex_of_real r * cis a"
    93 
    94   (* e ^ (x + iy) *)
    95   expi :: "complex => complex"
    96   "expi z == complex_of_real(exp (Re z)) * cis (Im z)"
    97 
    98 
    99 lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
   100   by (induct z, induct w) simp
   101 
   102 lemma Re [simp]: "Re(Complex x y) = x"
   103 by simp
   104 
   105 lemma Im [simp]: "Im(Complex x y) = y"
   106 by simp
   107 
   108 lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))"
   109 by (induct w, induct z, simp)
   110 
   111 lemma complex_Re_zero [simp]: "Re 0 = 0"
   112 by (simp add: complex_zero_def)
   113 
   114 lemma complex_Im_zero [simp]: "Im 0 = 0"
   115 by (simp add: complex_zero_def)
   116 
   117 lemma complex_Re_one [simp]: "Re 1 = 1"
   118 by (simp add: complex_one_def)
   119 
   120 lemma complex_Im_one [simp]: "Im 1 = 0"
   121 by (simp add: complex_one_def)
   122 
   123 lemma complex_Re_i [simp]: "Re(ii) = 0"
   124 by (simp add: i_def)
   125 
   126 lemma complex_Im_i [simp]: "Im(ii) = 1"
   127 by (simp add: i_def)
   128 
   129 lemma Re_complex_of_real [simp]: "Re(complex_of_real z) = z"
   130 by (simp add: complex_of_real_def)
   131 
   132 lemma Im_complex_of_real [simp]: "Im(complex_of_real z) = 0"
   133 by (simp add: complex_of_real_def)
   134 
   135 
   136 subsection{*Unary Minus*}
   137 
   138 lemma complex_minus [simp]: "- (Complex x y) = Complex (-x) (-y)"
   139 by (simp add: complex_minus_def)
   140 
   141 lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
   142 by (simp add: complex_minus_def)
   143 
   144 lemma complex_Im_minus [simp]: "Im (-z) = - Im z"
   145 by (simp add: complex_minus_def)
   146 
   147 
   148 subsection{*Addition*}
   149 
   150 lemma complex_add [simp]:
   151      "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
   152 by (simp add: complex_add_def)
   153 
   154 lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)"
   155 by (simp add: complex_add_def)
   156 
   157 lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)"
   158 by (simp add: complex_add_def)
   159 
   160 lemma complex_add_commute: "(u::complex) + v = v + u"
   161 by (simp add: complex_add_def add_commute)
   162 
   163 lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)"
   164 by (simp add: complex_add_def add_assoc)
   165 
   166 lemma complex_add_zero_left: "(0::complex) + z = z"
   167 by (simp add: complex_add_def complex_zero_def)
   168 
   169 lemma complex_add_zero_right: "z + (0::complex) = z"
   170 by (simp add: complex_add_def complex_zero_def)
   171 
   172 lemma complex_add_minus_left: "-z + z = (0::complex)"
   173 by (simp add: complex_add_def complex_minus_def complex_zero_def)
   174 
   175 lemma complex_diff:
   176       "Complex x1 y1 - Complex x2 y2 = Complex (x1-x2) (y1-y2)"
   177 by (simp add: complex_add_def complex_minus_def complex_diff_def)
   178 
   179 lemma complex_Re_diff [simp]: "Re(x - y) = Re(x) - Re(y)"
   180 by (simp add: complex_diff_def)
   181 
   182 lemma complex_Im_diff [simp]: "Im(x - y) = Im(x) - Im(y)"
   183 by (simp add: complex_diff_def)
   184 
   185 
   186 subsection{*Multiplication*}
   187 
   188 lemma complex_mult [simp]:
   189      "Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
   190 by (simp add: complex_mult_def)
   191 
   192 lemma complex_mult_commute: "(w::complex) * z = z * w"
   193 by (simp add: complex_mult_def mult_commute add_commute)
   194 
   195 lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"
   196 by (simp add: complex_mult_def mult_ac add_ac
   197               right_diff_distrib right_distrib left_diff_distrib left_distrib)
   198 
   199 lemma complex_mult_one_left: "(1::complex) * z = z"
   200 by (simp add: complex_mult_def complex_one_def)
   201 
   202 lemma complex_mult_one_right: "z * (1::complex) = z"
   203 by (simp add: complex_mult_def complex_one_def)
   204 
   205 
   206 subsection{*Inverse*}
   207 
   208 lemma complex_inverse [simp]:
   209      "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))"
   210 by (simp add: complex_inverse_def)
   211 
   212 lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
   213 apply (induct z)
   214 apply (rename_tac x y)
   215 apply (auto simp add: complex_mult complex_inverse complex_one_def
   216       complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
   217 apply (drule_tac y = y in real_sum_squares_not_zero)
   218 apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
   219 done
   220 
   221 
   222 subsection {* The field of complex numbers *}
   223 
   224 instance complex :: field
   225 proof
   226   fix z u v w :: complex
   227   show "(u + v) + w = u + (v + w)"
   228     by (rule complex_add_assoc)
   229   show "z + w = w + z"
   230     by (rule complex_add_commute)
   231   show "0 + z = z"
   232     by (rule complex_add_zero_left)
   233   show "-z + z = 0"
   234     by (rule complex_add_minus_left)
   235   show "z - w = z + -w"
   236     by (simp add: complex_diff_def)
   237   show "(u * v) * w = u * (v * w)"
   238     by (rule complex_mult_assoc)
   239   show "z * w = w * z"
   240     by (rule complex_mult_commute)
   241   show "1 * z = z"
   242     by (rule complex_mult_one_left)
   243   show "0 \<noteq> (1::complex)"
   244     by (simp add: complex_zero_def complex_one_def)
   245   show "(u + v) * w = u * w + v * w"
   246     by (simp add: complex_mult_def complex_add_def left_distrib 
   247                   diff_minus add_ac)
   248   show "z / w = z * inverse w"
   249     by (simp add: complex_divide_def)
   250   assume "w \<noteq> 0"
   251   thus "inverse w * w = 1"
   252     by (simp add: complex_mult_inv_left)
   253 qed
   254 
   255 instance complex :: division_by_zero
   256 proof
   257   show "inverse 0 = (0::complex)"
   258     by (simp add: complex_inverse_def complex_zero_def)
   259 qed
   260 
   261 
   262 subsection{*Embedding Properties for @{term complex_of_real} Map*}
   263 
   264 lemma Complex_add_complex_of_real [simp]:
   265      "Complex x y + complex_of_real r = Complex (x+r) y"
   266 by (simp add: complex_of_real_def)
   267 
   268 lemma complex_of_real_add_Complex [simp]:
   269      "complex_of_real r + Complex x y = Complex (r+x) y"
   270 by (simp add: i_def complex_of_real_def)
   271 
   272 lemma Complex_mult_complex_of_real:
   273      "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
   274 by (simp add: complex_of_real_def)
   275 
   276 lemma complex_of_real_mult_Complex:
   277      "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
   278 by (simp add: i_def complex_of_real_def)
   279 
   280 lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
   281 by (simp add: i_def complex_of_real_def)
   282 
   283 lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r"
   284 by (simp add: i_def complex_of_real_def)
   285 
   286 lemma complex_of_real_one [simp]: "complex_of_real 1 = 1"
   287 by (simp add: complex_one_def complex_of_real_def)
   288 
   289 lemma complex_of_real_zero [simp]: "complex_of_real 0 = 0"
   290 by (simp add: complex_zero_def complex_of_real_def)
   291 
   292 lemma complex_of_real_eq_iff [iff]:
   293      "(complex_of_real x = complex_of_real y) = (x = y)"
   294 by (simp add: complex_of_real_def)
   295 
   296 lemma complex_of_real_minus [simp]: "complex_of_real(-x) = - complex_of_real x"
   297 by (simp add: complex_of_real_def complex_minus)
   298 
   299 lemma complex_of_real_inverse [simp]:
   300      "complex_of_real(inverse x) = inverse(complex_of_real x)"
   301 apply (case_tac "x=0", simp)
   302 apply (simp add: complex_of_real_def divide_inverse power2_eq_square)
   303 done
   304 
   305 lemma complex_of_real_add [simp]:
   306      "complex_of_real (x + y) = complex_of_real x + complex_of_real y"
   307 by (simp add: complex_add complex_of_real_def)
   308 
   309 lemma complex_of_real_diff [simp]:
   310      "complex_of_real (x - y) = complex_of_real x - complex_of_real y"
   311 by (simp add: complex_of_real_minus diff_minus)
   312 
   313 lemma complex_of_real_mult [simp]:
   314      "complex_of_real (x * y) = complex_of_real x * complex_of_real y"
   315 by (simp add: complex_mult complex_of_real_def)
   316 
   317 lemma complex_of_real_divide [simp]:
   318       "complex_of_real(x/y) = complex_of_real x / complex_of_real y"
   319 apply (simp add: complex_divide_def)
   320 apply (case_tac "y=0", simp)
   321 apply (simp add: complex_of_real_mult complex_of_real_inverse 
   322                  divide_inverse)
   323 done
   324 
   325 lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
   326 by (simp add: cmod_def)
   327 
   328 lemma complex_mod_zero [simp]: "cmod(0) = 0"
   329 by (simp add: cmod_def)
   330 
   331 lemma complex_mod_one [simp]: "cmod(1) = 1"
   332 by (simp add: cmod_def power2_eq_square)
   333 
   334 lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x"
   335 by (simp add: complex_of_real_def power2_eq_square complex_mod)
   336 
   337 lemma complex_of_real_abs:
   338      "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
   339 by simp
   340 
   341 
   342 subsection{*The Functions @{term Re} and @{term Im}*}
   343 
   344 lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
   345 by (induct z, induct w, simp add: complex_mult)
   346 
   347 lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z"
   348 by (induct z, induct w, simp add: complex_mult)
   349 
   350 lemma Re_i_times [simp]: "Re(ii * z) = - Im z"
   351 by (simp add: complex_Re_mult_eq) 
   352 
   353 lemma Re_times_i [simp]: "Re(z * ii) = - Im z"
   354 by (simp add: complex_Re_mult_eq) 
   355 
   356 lemma Im_i_times [simp]: "Im(ii * z) = Re z"
   357 by (simp add: complex_Im_mult_eq) 
   358 
   359 lemma Im_times_i [simp]: "Im(z * ii) = Re z"
   360 by (simp add: complex_Im_mult_eq) 
   361 
   362 lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
   363 by (simp add: complex_Re_mult_eq)
   364 
   365 lemma complex_Re_mult_complex_of_real [simp]:
   366      "Re (z * complex_of_real c) = Re(z) * c"
   367 by (simp add: complex_Re_mult_eq)
   368 
   369 lemma complex_Im_mult_complex_of_real [simp]:
   370      "Im (z * complex_of_real c) = Im(z) * c"
   371 by (simp add: complex_Im_mult_eq)
   372 
   373 lemma complex_Re_mult_complex_of_real2 [simp]:
   374      "Re (complex_of_real c * z) = c * Re(z)"
   375 by (simp add: complex_Re_mult_eq)
   376 
   377 lemma complex_Im_mult_complex_of_real2 [simp]:
   378      "Im (complex_of_real c * z) = c * Im(z)"
   379 by (simp add: complex_Im_mult_eq)
   380  
   381 
   382 subsection{*Conjugation is an Automorphism*}
   383 
   384 lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
   385 by (simp add: cnj_def)
   386 
   387 lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
   388 by (simp add: cnj_def complex_Re_Im_cancel_iff)
   389 
   390 lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
   391 by (simp add: cnj_def)
   392 
   393 lemma complex_cnj_complex_of_real [simp]:
   394      "cnj (complex_of_real x) = complex_of_real x"
   395 by (simp add: complex_of_real_def complex_cnj)
   396 
   397 lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
   398 by (induct z, simp add: complex_cnj complex_mod power2_eq_square)
   399 
   400 lemma complex_cnj_minus: "cnj (-z) = - cnj z"
   401 by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus)
   402 
   403 lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"
   404 by (induct z, simp add: complex_cnj complex_inverse power2_eq_square)
   405 
   406 lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"
   407 by (induct w, induct z, simp add: complex_cnj complex_add)
   408 
   409 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
   410 by (simp add: diff_minus complex_cnj_add complex_cnj_minus)
   411 
   412 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
   413 by (induct w, induct z, simp add: complex_cnj complex_mult)
   414 
   415 lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)"
   416 by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse)
   417 
   418 lemma complex_cnj_one [simp]: "cnj 1 = 1"
   419 by (simp add: cnj_def complex_one_def)
   420 
   421 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
   422 by (induct z, simp add: complex_add complex_cnj complex_of_real_def)
   423 
   424 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
   425 apply (induct z)
   426 apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus
   427                  complex_minus i_def complex_mult)
   428 done
   429 
   430 lemma complex_cnj_zero [simp]: "cnj 0 = 0"
   431 by (simp add: cnj_def complex_zero_def)
   432 
   433 lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
   434 by (induct z, simp add: complex_zero_def complex_cnj)
   435 
   436 lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
   437 by (induct z,
   438     simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
   439 
   440 
   441 subsection{*Modulus*}
   442 
   443 lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)"
   444 apply (induct x)
   445 apply (auto iff: real_0_le_add_iff 
   446             intro: real_sum_squares_cancel real_sum_squares_cancel2
   447             simp add: complex_mod complex_zero_def power2_eq_square)
   448 done
   449 
   450 lemma complex_mod_complex_of_real_of_nat [simp]:
   451      "cmod (complex_of_real(real (n::nat))) = real n"
   452 by simp
   453 
   454 lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)"
   455 by (induct x, simp add: complex_mod complex_minus power2_eq_square)
   456 
   457 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
   458 apply (induct z, simp add: complex_mod complex_cnj complex_mult)
   459 apply (simp add: power2_eq_square abs_if linorder_not_less real_0_le_add_iff)
   460 done
   461 
   462 lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
   463 by (simp add: cmod_def)
   464 
   465 lemma complex_mod_ge_zero [simp]: "0 \<le> cmod x"
   466 by (simp add: cmod_def)
   467 
   468 lemma abs_cmod_cancel [simp]: "abs(cmod x) = cmod x"
   469 by (simp add: abs_if linorder_not_less)
   470 
   471 lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
   472 apply (induct x, induct y)
   473 apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric])
   474 apply (rule_tac n = 1 in power_inject_base)
   475 apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
   476 apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib 
   477                       add_ac mult_ac)
   478 done
   479 
   480 lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
   481 by (simp add: cmod_def) 
   482 
   483 lemma cmod_complex_polar [simp]:
   484      "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
   485 by (simp only: cmod_unit_one complex_mod_mult, simp) 
   486 
   487 lemma complex_mod_add_squared_eq:
   488      "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
   489 apply (induct x, induct y)
   490 apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   491 apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
   492 done
   493 
   494 lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \<le> cmod(x * cnj y)"
   495 apply (induct x, induct y)
   496 apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   497 done
   498 
   499 lemma complex_Re_mult_cnj_le_cmod2 [simp]: "Re(x * cnj y) \<le> cmod(x * y)"
   500 by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult)
   501 
   502 lemma real_sum_squared_expand:
   503      "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
   504 by (simp add: left_distrib right_distrib power2_eq_square)
   505 
   506 lemma complex_mod_triangle_squared [simp]:
   507      "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
   508 by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
   509 
   510 lemma complex_mod_minus_le_complex_mod [simp]: "- cmod x \<le> cmod x"
   511 by (rule order_trans [OF _ complex_mod_ge_zero], simp)
   512 
   513 lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)"
   514 apply (rule_tac n = 1 in realpow_increasing)
   515 apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
   516             simp add: add_increasing power2_eq_square [symmetric])
   517 done
   518 
   519 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
   520 by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"-cmod b"], simp)
   521 
   522 lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"
   523 apply (induct x, induct y)
   524 apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)
   525 done
   526 
   527 lemma complex_mod_add_less:
   528      "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"
   529 by (auto intro: order_le_less_trans complex_mod_triangle_ineq)
   530 
   531 lemma complex_mod_mult_less:
   532      "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"
   533 by (auto intro: real_mult_less_mono' simp add: complex_mod_mult)
   534 
   535 lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \<le> cmod(a + b)"
   536 apply (rule linorder_cases [of "cmod(a)" "cmod (b)"])
   537 apply auto
   538 apply (rule order_trans [of _ 0], rule order_less_imp_le)
   539 apply (simp add: compare_rls, simp)
   540 apply (simp add: compare_rls)
   541 apply (rule complex_mod_minus [THEN subst])
   542 apply (rule order_trans)
   543 apply (rule_tac [2] complex_mod_triangle_ineq)
   544 apply (auto simp add: add_ac)
   545 done
   546 
   547 lemma complex_Re_le_cmod [simp]: "Re z \<le> cmod z"
   548 by (induct z, simp add: complex_mod del: realpow_Suc)
   549 
   550 lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"
   551 apply (insert complex_mod_ge_zero [of z])
   552 apply (drule order_le_imp_less_or_eq, auto)
   553 done
   554 
   555 
   556 subsection{*A Few More Theorems*}
   557 
   558 lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"
   559 apply (case_tac "x=0", simp)
   560 apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1])
   561 apply (auto simp add: complex_mod_mult [symmetric])
   562 done
   563 
   564 lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
   565 by (simp add: complex_divide_def divide_inverse complex_mod_mult complex_mod_inverse)
   566 
   567 
   568 subsection{*Exponentiation*}
   569 
   570 primrec
   571      complexpow_0:   "z ^ 0       = 1"
   572      complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
   573 
   574 
   575 instance complex :: recpower
   576 proof
   577   fix z :: complex
   578   fix n :: nat
   579   show "z^0 = 1" by simp
   580   show "z^(Suc n) = z * (z^n)" by simp
   581 qed
   582 
   583 
   584 lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
   585 apply (induct_tac "n")
   586 apply (auto simp add: complex_of_real_mult [symmetric])
   587 done
   588 
   589 lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
   590 apply (induct_tac "n")
   591 apply (auto simp add: complex_cnj_mult)
   592 done
   593 
   594 lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
   595 apply (induct_tac "n")
   596 apply (auto simp add: complex_mod_mult)
   597 done
   598 
   599 lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
   600 by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)
   601 
   602 lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
   603 by (simp add: i_def complex_zero_def)
   604 
   605 
   606 subsection{*The Function @{term sgn}*}
   607 
   608 lemma sgn_zero [simp]: "sgn 0 = 0"
   609 by (simp add: sgn_def)
   610 
   611 lemma sgn_one [simp]: "sgn 1 = 1"
   612 by (simp add: sgn_def)
   613 
   614 lemma sgn_minus: "sgn (-z) = - sgn(z)"
   615 by (simp add: sgn_def)
   616 
   617 lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
   618 by (simp add: sgn_def)
   619 
   620 lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
   621 by (simp add: i_def complex_of_real_def complex_mult complex_add)
   622 
   623 lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
   624 by (simp add: i_def complex_one_def complex_mult complex_minus)
   625 
   626 lemma complex_eq_cancel_iff2 [simp]:
   627      "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
   628 by (simp add: complex_of_real_def) 
   629 
   630 lemma complex_eq_cancel_iff2a [simp]:
   631      "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
   632 by (simp add: complex_of_real_def)
   633 
   634 lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)"
   635 by (simp add: complex_zero_def)
   636 
   637 lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)"
   638 by (simp add: complex_one_def)
   639 
   640 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)"
   641 by (simp add: i_def)
   642 
   643 
   644 
   645 lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
   646 proof (induct z)
   647   case (Complex x y)
   648     have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
   649       by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
   650     thus "Re (sgn (Complex x y)) = Re (Complex x y) /cmod (Complex x y)"
   651        by (simp add: sgn_def complex_of_real_def divide_inverse)
   652 qed
   653 
   654 
   655 lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
   656 proof (induct z)
   657   case (Complex x y)
   658     have "sqrt (x\<twosuperior> + y\<twosuperior>) * inverse (x\<twosuperior> + y\<twosuperior>) = inverse (sqrt (x\<twosuperior> + y\<twosuperior>))"
   659       by (simp add: divide_inverse [symmetric] sqrt_divide_self_eq)
   660     thus "Im (sgn (Complex x y)) = Im (Complex x y) /cmod (Complex x y)"
   661        by (simp add: sgn_def complex_of_real_def divide_inverse)
   662 qed
   663 
   664 lemma complex_inverse_complex_split:
   665      "inverse(complex_of_real x + ii * complex_of_real y) =
   666       complex_of_real(x/(x ^ 2 + y ^ 2)) -
   667       ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
   668 by (simp add: complex_of_real_def i_def complex_mult complex_add
   669          diff_minus complex_minus complex_inverse divide_inverse)
   670 
   671 (*----------------------------------------------------------------------------*)
   672 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
   673 (* many of the theorems are not used - so should they be kept?                *)
   674 (*----------------------------------------------------------------------------*)
   675 
   676 lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
   677 by (auto simp add: complex_zero_def complex_of_real_def)
   678 
   679 lemma cos_arg_i_mult_zero_pos:
   680    "0 < y ==> cos (arg(Complex 0 y)) = 0"
   681 apply (simp add: arg_def abs_if)
   682 apply (rule_tac a = "pi/2" in someI2, auto)
   683 apply (rule order_less_trans [of _ 0], auto)
   684 done
   685 
   686 lemma cos_arg_i_mult_zero_neg:
   687    "y < 0 ==> cos (arg(Complex 0 y)) = 0"
   688 apply (simp add: arg_def abs_if)
   689 apply (rule_tac a = "- pi/2" in someI2, auto)
   690 apply (rule order_trans [of _ 0], auto)
   691 done
   692 
   693 lemma cos_arg_i_mult_zero [simp]:
   694      "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
   695 by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
   696 
   697 
   698 subsection{*Finally! Polar Form for Complex Numbers*}
   699 
   700 lemma complex_split_polar:
   701      "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
   702 apply (induct z) 
   703 apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
   704 done
   705 
   706 lemma rcis_Ex: "\<exists>r a. z = rcis r a"
   707 apply (induct z) 
   708 apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
   709 done
   710 
   711 lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
   712 by (simp add: rcis_def cis_def)
   713 
   714 lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
   715 by (simp add: rcis_def cis_def)
   716 
   717 lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
   718 proof -
   719   have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
   720     by (simp only: power_mult_distrib right_distrib) 
   721   thus ?thesis by simp
   722 qed
   723 
   724 lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
   725 by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
   726 
   727 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
   728 apply (simp add: cmod_def)
   729 apply (rule real_sqrt_eq_iff [THEN iffD2])
   730 apply (auto simp add: complex_mult_cnj)
   731 done
   732 
   733 lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z"
   734 by (induct z, simp add: complex_cnj)
   735 
   736 lemma complex_Im_cnj [simp]: "Im(cnj z) = - Im z"
   737 by (induct z, simp add: complex_cnj)
   738 
   739 lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
   740 by (induct z, simp add: complex_cnj complex_mult)
   741 
   742 
   743 (*---------------------------------------------------------------------------*)
   744 (*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
   745 (*---------------------------------------------------------------------------*)
   746 
   747 lemma cis_rcis_eq: "cis a = rcis 1 a"
   748 by (simp add: rcis_def)
   749 
   750 lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
   751 by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib
   752               complex_of_real_def)
   753 
   754 lemma cis_mult: "cis a * cis b = cis (a + b)"
   755 by (simp add: cis_rcis_eq rcis_mult)
   756 
   757 lemma cis_zero [simp]: "cis 0 = 1"
   758 by (simp add: cis_def complex_one_def)
   759 
   760 lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
   761 by (simp add: rcis_def)
   762 
   763 lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
   764 by (simp add: rcis_def)
   765 
   766 lemma complex_of_real_minus_one:
   767    "complex_of_real (-(1::real)) = -(1::complex)"
   768 by (simp add: complex_of_real_def complex_one_def complex_minus)
   769 
   770 lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
   771 by (simp add: complex_mult_assoc [symmetric])
   772 
   773 
   774 lemma cis_real_of_nat_Suc_mult:
   775    "cis (real (Suc n) * a) = cis a * cis (real n * a)"
   776 by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
   777 
   778 lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
   779 apply (induct_tac "n")
   780 apply (auto simp add: cis_real_of_nat_Suc_mult)
   781 done
   782 
   783 lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
   784 by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow)
   785 
   786 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
   787 by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus 
   788               diff_minus)
   789 
   790 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
   791 by (simp add: divide_inverse rcis_def complex_of_real_inverse)
   792 
   793 lemma cis_divide: "cis a / cis b = cis (a - b)"
   794 by (simp add: complex_divide_def cis_mult real_diff_def)
   795 
   796 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
   797 apply (simp add: complex_divide_def)
   798 apply (case_tac "r2=0", simp)
   799 apply (simp add: rcis_inverse rcis_mult real_diff_def)
   800 done
   801 
   802 lemma Re_cis [simp]: "Re(cis a) = cos a"
   803 by (simp add: cis_def)
   804 
   805 lemma Im_cis [simp]: "Im(cis a) = sin a"
   806 by (simp add: cis_def)
   807 
   808 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
   809 by (auto simp add: DeMoivre)
   810 
   811 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
   812 by (auto simp add: DeMoivre)
   813 
   814 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
   815 by (simp add: expi_def complex_Re_add exp_add complex_Im_add 
   816               cis_mult [symmetric] complex_of_real_mult mult_ac)
   817 
   818 lemma expi_zero [simp]: "expi (0::complex) = 1"
   819 by (simp add: expi_def)
   820 
   821 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
   822 apply (insert rcis_Ex [of z])
   823 apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
   824 apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
   825 done
   826 
   827 
   828 subsection{*Numerals and Arithmetic*}
   829 
   830 instance complex :: number ..
   831 
   832 defs (overloaded)
   833   complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)"
   834     --{*the type constraint is essential!*}
   835 
   836 instance complex :: number_ring
   837 by (intro_classes, simp add: complex_number_of_def) 
   838 
   839 
   840 lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
   841 by (induct n, simp_all) 
   842 
   843 lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
   844 proof (cases z)
   845   case (1 n)
   846     thus ?thesis by simp
   847 next
   848   case (2 n)
   849     thus ?thesis 
   850       by (simp only: of_int_minus complex_of_real_minus, simp)
   851 qed
   852 
   853 
   854 text{*Collapse applications of @{term complex_of_real} to @{term number_of}*}
   855 lemma complex_number_of [simp]: "complex_of_real (number_of w) = number_of w"
   856 by (simp add: complex_number_of_def real_number_of_def) 
   857 
   858 text{*This theorem is necessary because theorems such as
   859    @{text iszero_number_of_0} only hold for ordered rings. They cannot
   860    be generalized to fields in general because they fail for finite fields.
   861    They work for type complex because the reals can be embedded in them.*}
   862 lemma iszero_complex_number_of [simp]:
   863      "iszero (number_of w :: complex) = iszero (number_of w :: real)"
   864 by (simp only: complex_of_real_zero_iff complex_number_of [symmetric] 
   865                iszero_def)  
   866 
   867 lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
   868 apply (subst complex_number_of [symmetric])
   869 apply (rule complex_cnj_complex_of_real)
   870 done
   871 
   872 lemma complex_number_of_cmod: 
   873       "cmod(number_of v :: complex) = abs (number_of v :: real)"
   874 by (simp only: complex_number_of [symmetric] complex_mod_complex_of_real)
   875 
   876 lemma complex_number_of_Re [simp]: "Re(number_of v :: complex) = number_of v"
   877 by (simp only: complex_number_of [symmetric] Re_complex_of_real)
   878 
   879 lemma complex_number_of_Im [simp]: "Im(number_of v :: complex) = 0"
   880 by (simp only: complex_number_of [symmetric] Im_complex_of_real)
   881 
   882 lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
   883 by (simp add: expi_def complex_Re_mult_eq complex_Im_mult_eq cis_def)
   884 
   885 
   886 (*examples:
   887 print_depth 22
   888 set timing;
   889 set trace_simp;
   890 fun test s = (Goal s, by (Simp_tac 1)); 
   891 
   892 test "23 * ii + 45 * ii= (x::complex)";
   893 
   894 test "5 * ii + 12 - 45 * ii= (x::complex)";
   895 test "5 * ii + 40 - 12 * ii + 9 = (x::complex) + 89 * ii";
   896 test "5 * ii + 40 - 12 * ii + 9 - 78 = (x::complex) + 89 * ii";
   897 
   898 test "l + 10 * ii + 90 + 3*l +  9 + 45 * ii= (x::complex)";
   899 test "87 + 10 * ii + 90 + 3*7 +  9 + 45 * ii= (x::complex)";
   900 
   901 
   902 fun test s = (Goal s; by (Asm_simp_tac 1)); 
   903 
   904 test "x*k = k*(y::complex)";
   905 test "k = k*(y::complex)"; 
   906 test "a*(b*c) = (b::complex)";
   907 test "a*(b*c) = d*(b::complex)*(x*a)";
   908 
   909 
   910 test "(x*k) / (k*(y::complex)) = (uu::complex)";
   911 test "(k) / (k*(y::complex)) = (uu::complex)"; 
   912 test "(a*(b*c)) / ((b::complex)) = (uu::complex)";
   913 test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)";
   914 
   915 FIXME: what do we do about this?
   916 test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z";
   917 *)
   918 
   919 
   920 ML
   921 {*
   922 val complex_zero_def = thm"complex_zero_def";
   923 val complex_one_def = thm"complex_one_def";
   924 val complex_minus_def = thm"complex_minus_def";
   925 val complex_divide_def = thm"complex_divide_def";
   926 val complex_mult_def = thm"complex_mult_def";
   927 val complex_add_def = thm"complex_add_def";
   928 val complex_of_real_def = thm"complex_of_real_def";
   929 val i_def = thm"i_def";
   930 val expi_def = thm"expi_def";
   931 val cis_def = thm"cis_def";
   932 val rcis_def = thm"rcis_def";
   933 val cmod_def = thm"cmod_def";
   934 val cnj_def = thm"cnj_def";
   935 val sgn_def = thm"sgn_def";
   936 val arg_def = thm"arg_def";
   937 val complexpow_0 = thm"complexpow_0";
   938 val complexpow_Suc = thm"complexpow_Suc";
   939 
   940 val Re = thm"Re";
   941 val Im = thm"Im";
   942 val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff";
   943 val complex_Re_zero = thm"complex_Re_zero";
   944 val complex_Im_zero = thm"complex_Im_zero";
   945 val complex_Re_one = thm"complex_Re_one";
   946 val complex_Im_one = thm"complex_Im_one";
   947 val complex_Re_i = thm"complex_Re_i";
   948 val complex_Im_i = thm"complex_Im_i";
   949 val Re_complex_of_real = thm"Re_complex_of_real";
   950 val Im_complex_of_real = thm"Im_complex_of_real";
   951 val complex_minus = thm"complex_minus";
   952 val complex_Re_minus = thm"complex_Re_minus";
   953 val complex_Im_minus = thm"complex_Im_minus";
   954 val complex_add = thm"complex_add";
   955 val complex_Re_add = thm"complex_Re_add";
   956 val complex_Im_add = thm"complex_Im_add";
   957 val complex_add_commute = thm"complex_add_commute";
   958 val complex_add_assoc = thm"complex_add_assoc";
   959 val complex_add_zero_left = thm"complex_add_zero_left";
   960 val complex_add_zero_right = thm"complex_add_zero_right";
   961 val complex_diff = thm"complex_diff";
   962 val complex_mult = thm"complex_mult";
   963 val complex_mult_one_left = thm"complex_mult_one_left";
   964 val complex_mult_one_right = thm"complex_mult_one_right";
   965 val complex_inverse = thm"complex_inverse";
   966 val complex_of_real_one = thm"complex_of_real_one";
   967 val complex_of_real_zero = thm"complex_of_real_zero";
   968 val complex_of_real_eq_iff = thm"complex_of_real_eq_iff";
   969 val complex_of_real_minus = thm"complex_of_real_minus";
   970 val complex_of_real_inverse = thm"complex_of_real_inverse";
   971 val complex_of_real_add = thm"complex_of_real_add";
   972 val complex_of_real_diff = thm"complex_of_real_diff";
   973 val complex_of_real_mult = thm"complex_of_real_mult";
   974 val complex_of_real_divide = thm"complex_of_real_divide";
   975 val complex_of_real_pow = thm"complex_of_real_pow";
   976 val complex_mod = thm"complex_mod";
   977 val complex_mod_zero = thm"complex_mod_zero";
   978 val complex_mod_one = thm"complex_mod_one";
   979 val complex_mod_complex_of_real = thm"complex_mod_complex_of_real";
   980 val complex_of_real_abs = thm"complex_of_real_abs";
   981 val complex_cnj = thm"complex_cnj";
   982 val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff";
   983 val complex_cnj_cnj = thm"complex_cnj_cnj";
   984 val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real";
   985 val complex_mod_cnj = thm"complex_mod_cnj";
   986 val complex_cnj_minus = thm"complex_cnj_minus";
   987 val complex_cnj_inverse = thm"complex_cnj_inverse";
   988 val complex_cnj_add = thm"complex_cnj_add";
   989 val complex_cnj_diff = thm"complex_cnj_diff";
   990 val complex_cnj_mult = thm"complex_cnj_mult";
   991 val complex_cnj_divide = thm"complex_cnj_divide";
   992 val complex_cnj_one = thm"complex_cnj_one";
   993 val complex_cnj_pow = thm"complex_cnj_pow";
   994 val complex_add_cnj = thm"complex_add_cnj";
   995 val complex_diff_cnj = thm"complex_diff_cnj";
   996 val complex_cnj_zero = thm"complex_cnj_zero";
   997 val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
   998 val complex_mult_cnj = thm"complex_mult_cnj";
   999 val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel";
  1000 val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat";
  1001 val complex_mod_minus = thm"complex_mod_minus";
  1002 val complex_mod_mult_cnj = thm"complex_mod_mult_cnj";
  1003 val complex_mod_squared = thm"complex_mod_squared";
  1004 val complex_mod_ge_zero = thm"complex_mod_ge_zero";
  1005 val abs_cmod_cancel = thm"abs_cmod_cancel";
  1006 val complex_mod_mult = thm"complex_mod_mult";
  1007 val complex_mod_add_squared_eq = thm"complex_mod_add_squared_eq";
  1008 val complex_Re_mult_cnj_le_cmod = thm"complex_Re_mult_cnj_le_cmod";
  1009 val complex_Re_mult_cnj_le_cmod2 = thm"complex_Re_mult_cnj_le_cmod2";
  1010 val real_sum_squared_expand = thm"real_sum_squared_expand";
  1011 val complex_mod_triangle_squared = thm"complex_mod_triangle_squared";
  1012 val complex_mod_minus_le_complex_mod = thm"complex_mod_minus_le_complex_mod";
  1013 val complex_mod_triangle_ineq = thm"complex_mod_triangle_ineq";
  1014 val complex_mod_triangle_ineq2 = thm"complex_mod_triangle_ineq2";
  1015 val complex_mod_diff_commute = thm"complex_mod_diff_commute";
  1016 val complex_mod_add_less = thm"complex_mod_add_less";
  1017 val complex_mod_mult_less = thm"complex_mod_mult_less";
  1018 val complex_mod_diff_ineq = thm"complex_mod_diff_ineq";
  1019 val complex_Re_le_cmod = thm"complex_Re_le_cmod";
  1020 val complex_mod_gt_zero = thm"complex_mod_gt_zero";
  1021 val complex_mod_complexpow = thm"complex_mod_complexpow";
  1022 val complex_mod_inverse = thm"complex_mod_inverse";
  1023 val complex_mod_divide = thm"complex_mod_divide";
  1024 val complexpow_i_squared = thm"complexpow_i_squared";
  1025 val complex_i_not_zero = thm"complex_i_not_zero";
  1026 val sgn_zero = thm"sgn_zero";
  1027 val sgn_one = thm"sgn_one";
  1028 val sgn_minus = thm"sgn_minus";
  1029 val sgn_eq = thm"sgn_eq";
  1030 val i_mult_eq = thm"i_mult_eq";
  1031 val i_mult_eq2 = thm"i_mult_eq2";
  1032 val Re_sgn = thm"Re_sgn";
  1033 val Im_sgn = thm"Im_sgn";
  1034 val complex_inverse_complex_split = thm"complex_inverse_complex_split";
  1035 val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
  1036 val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
  1037 val rcis_Ex = thm"rcis_Ex";
  1038 val Re_rcis = thm"Re_rcis";
  1039 val Im_rcis = thm"Im_rcis";
  1040 val complex_mod_rcis = thm"complex_mod_rcis";
  1041 val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
  1042 val complex_Re_cnj = thm"complex_Re_cnj";
  1043 val complex_Im_cnj = thm"complex_Im_cnj";
  1044 val complex_In_mult_cnj_zero = thm"complex_In_mult_cnj_zero";
  1045 val complex_Re_mult = thm"complex_Re_mult";
  1046 val complex_Re_mult_complex_of_real = thm"complex_Re_mult_complex_of_real";
  1047 val complex_Im_mult_complex_of_real = thm"complex_Im_mult_complex_of_real";
  1048 val complex_Re_mult_complex_of_real2 = thm"complex_Re_mult_complex_of_real2";
  1049 val complex_Im_mult_complex_of_real2 = thm"complex_Im_mult_complex_of_real2";
  1050 val cis_rcis_eq = thm"cis_rcis_eq";
  1051 val rcis_mult = thm"rcis_mult";
  1052 val cis_mult = thm"cis_mult";
  1053 val cis_zero = thm"cis_zero";
  1054 val rcis_zero_mod = thm"rcis_zero_mod";
  1055 val rcis_zero_arg = thm"rcis_zero_arg";
  1056 val complex_of_real_minus_one = thm"complex_of_real_minus_one";
  1057 val complex_i_mult_minus = thm"complex_i_mult_minus";
  1058 val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult";
  1059 val DeMoivre = thm"DeMoivre";
  1060 val DeMoivre2 = thm"DeMoivre2";
  1061 val cis_inverse = thm"cis_inverse";
  1062 val rcis_inverse = thm"rcis_inverse";
  1063 val cis_divide = thm"cis_divide";
  1064 val rcis_divide = thm"rcis_divide";
  1065 val Re_cis = thm"Re_cis";
  1066 val Im_cis = thm"Im_cis";
  1067 val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
  1068 val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
  1069 val expi_add = thm"expi_add";
  1070 val expi_zero = thm"expi_zero";
  1071 val complex_Re_mult_eq = thm"complex_Re_mult_eq";
  1072 val complex_Im_mult_eq = thm"complex_Im_mult_eq";
  1073 val complex_expi_Ex = thm"complex_expi_Ex";
  1074 *}
  1075 
  1076 end
  1077 
  1078