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