src/HOL/Complex/Complex.thy
author paulson
Tue Jan 13 10:37:52 2004 +0100 (2004-01-13)
changeset 14354 988aa4648597
parent 14353 79f9fbef9106
child 14373 67a628beb981
permissions -rw-r--r--
types complex and hcomplex are now instances of class ringpower:
omitting redundant lemmas
     1 (*  Title:       Complex.thy
     2     Author:      Jacques D. Fleuriot
     3     Copyright:   2001 University of Edinburgh
     4     Description: Complex numbers
     5 *)
     6 
     7 theory Complex = HLog:
     8 
     9 typedef complex = "{p::(real*real). True}"
    10   by blast
    11 
    12 instance complex :: zero ..
    13 instance complex :: one ..
    14 instance complex :: plus ..
    15 instance complex :: times ..
    16 instance complex :: minus ..
    17 instance complex :: inverse ..
    18 instance complex :: power ..
    19 
    20 consts
    21   "ii"    :: complex        ("ii")
    22 
    23 constdefs
    24 
    25   (*--- real and Imaginary parts ---*)
    26 
    27   Re :: "complex => real"
    28   "Re(z) == fst(Rep_complex z)"
    29 
    30   Im :: "complex => real"
    31   "Im(z) == snd(Rep_complex z)"
    32 
    33   (*----------- modulus ------------*)
    34 
    35   cmod :: "complex => real"
    36   "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"
    37 
    38   (*----- injection from reals -----*)
    39 
    40   complex_of_real :: "real => complex"
    41   "complex_of_real r == Abs_complex(r,0::real)"
    42 
    43   (*------- complex conjugate ------*)
    44 
    45   cnj :: "complex => complex"
    46   "cnj z == Abs_complex(Re z, -Im z)"
    47 
    48   (*------------ Argand -------------*)
    49 
    50   sgn :: "complex => complex"
    51   "sgn z == z / complex_of_real(cmod z)"
    52 
    53   arg :: "complex => real"
    54   "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"
    55 
    56 
    57 defs (overloaded)
    58 
    59   complex_zero_def:
    60   "0 == Abs_complex(0::real,0)"
    61 
    62   complex_one_def:
    63   "1 == Abs_complex(1,0::real)"
    64 
    65   (*------ imaginary unit ----------*)
    66 
    67   i_def:
    68   "ii == Abs_complex(0::real,1)"
    69 
    70   (*----------- negation -----------*)
    71 
    72   complex_minus_def:
    73   "- (z::complex) == Abs_complex(-Re z, -Im z)"
    74 
    75 
    76   (*----------- inverse -----------*)
    77   complex_inverse_def:
    78   "inverse (z::complex) == Abs_complex(Re(z)/(Re(z) ^ 2 + Im(z) ^ 2),
    79                             -Im(z)/(Re(z) ^ 2 + Im(z) ^ 2))"
    80 
    81   complex_add_def:
    82   "w + (z::complex) == Abs_complex(Re(w) + Re(z),Im(w) + Im(z))"
    83 
    84   complex_diff_def:
    85   "w - (z::complex) == w + -(z::complex)"
    86 
    87   complex_mult_def:
    88   "w * (z::complex) == Abs_complex(Re(w) * Re(z) - Im(w) * Im(z),
    89 			Re(w) * Im(z) + Im(w) * Re(z))"
    90 
    91 
    92   (*----------- division ----------*)
    93   complex_divide_def:
    94   "w / (z::complex) == w * inverse z"
    95 
    96 
    97 constdefs
    98 
    99   (* abbreviation for (cos a + i sin a) *)
   100   cis :: "real => complex"
   101   "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)"
   102 
   103   (* abbreviation for r*(cos a + i sin a) *)
   104   rcis :: "[real, real] => complex"
   105   "rcis r a == complex_of_real r * cis a"
   106 
   107   (* e ^ (x + iy) *)
   108   expi :: "complex => complex"
   109   "expi z == complex_of_real(exp (Re z)) * cis (Im z)"
   110 
   111 
   112 lemma inj_Rep_complex: "inj Rep_complex"
   113 apply (rule inj_on_inverseI)
   114 apply (rule Rep_complex_inverse)
   115 done
   116 
   117 lemma inj_Abs_complex: "inj Abs_complex"
   118 apply (rule inj_on_inverseI)
   119 apply (rule Abs_complex_inverse)
   120 apply (simp (no_asm) add: complex_def)
   121 done
   122 declare inj_Abs_complex [THEN injD, simp]
   123 
   124 lemma Abs_complex_cancel_iff: "(Abs_complex x = Abs_complex y) = (x = y)"
   125 by (auto dest: inj_Abs_complex [THEN injD])
   126 declare Abs_complex_cancel_iff [simp]
   127 
   128 lemma pair_mem_complex: "(x,y) : complex"
   129 by (unfold complex_def, auto)
   130 declare pair_mem_complex [simp]
   131 
   132 lemma Abs_complex_inverse2: "Rep_complex (Abs_complex (x,y)) = (x,y)"
   133 apply (simp (no_asm) add: Abs_complex_inverse)
   134 done
   135 declare Abs_complex_inverse2 [simp]
   136 
   137 lemma eq_Abs_complex: "(!!x y. z = Abs_complex(x,y) ==> P) ==> P"
   138 apply (rule_tac p = "Rep_complex z" in PairE)
   139 apply (drule_tac f = Abs_complex in arg_cong)
   140 apply (force simp add: Rep_complex_inverse)
   141 done
   142 
   143 lemma Re: "Re(Abs_complex(x,y)) = x"
   144 apply (unfold Re_def)
   145 apply (simp (no_asm))
   146 done
   147 declare Re [simp]
   148 
   149 lemma Im: "Im(Abs_complex(x,y)) = y"
   150 apply (unfold Im_def)
   151 apply (simp (no_asm))
   152 done
   153 declare Im [simp]
   154 
   155 lemma Abs_complex_cancel: "Abs_complex(Re(z),Im(z)) = z"
   156 apply (rule_tac z = z in eq_Abs_complex)
   157 apply (simp (no_asm_simp))
   158 done
   159 declare Abs_complex_cancel [simp]
   160 
   161 lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))"
   162 apply (rule_tac z = w in eq_Abs_complex)
   163 apply (rule_tac z = z in eq_Abs_complex)
   164 apply (auto dest: inj_Abs_complex [THEN injD])
   165 done
   166 
   167 lemma complex_Re_zero: "Re 0 = 0"
   168 apply (unfold complex_zero_def)
   169 apply (simp (no_asm))
   170 done
   171 
   172 lemma complex_Im_zero: "Im 0 = 0"
   173 apply (unfold complex_zero_def)
   174 apply (simp (no_asm))
   175 done
   176 declare complex_Re_zero [simp] complex_Im_zero [simp]
   177 
   178 lemma complex_Re_one: "Re 1 = 1"
   179 apply (unfold complex_one_def)
   180 apply (simp (no_asm))
   181 done
   182 declare complex_Re_one [simp]
   183 
   184 lemma complex_Im_one: "Im 1 = 0"
   185 apply (unfold complex_one_def)
   186 apply (simp (no_asm))
   187 done
   188 declare complex_Im_one [simp]
   189 
   190 lemma complex_Re_i: "Re(ii) = 0"
   191 by (unfold i_def, auto)
   192 declare complex_Re_i [simp]
   193 
   194 lemma complex_Im_i: "Im(ii) = 1"
   195 by (unfold i_def, auto)
   196 declare complex_Im_i [simp]
   197 
   198 lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0"
   199 apply (unfold complex_of_real_def)
   200 apply (simp (no_asm))
   201 done
   202 declare Re_complex_of_real_zero [simp]
   203 
   204 lemma Im_complex_of_real_zero: "Im(complex_of_real 0) = 0"
   205 apply (unfold complex_of_real_def)
   206 apply (simp (no_asm))
   207 done
   208 declare Im_complex_of_real_zero [simp]
   209 
   210 lemma Re_complex_of_real_one: "Re(complex_of_real 1) = 1"
   211 apply (unfold complex_of_real_def)
   212 apply (simp (no_asm))
   213 done
   214 declare Re_complex_of_real_one [simp]
   215 
   216 lemma Im_complex_of_real_one: "Im(complex_of_real 1) = 0"
   217 apply (unfold complex_of_real_def)
   218 apply (simp (no_asm))
   219 done
   220 declare Im_complex_of_real_one [simp]
   221 
   222 lemma Re_complex_of_real: "Re(complex_of_real z) = z"
   223 by (unfold complex_of_real_def, auto)
   224 declare Re_complex_of_real [simp]
   225 
   226 lemma Im_complex_of_real: "Im(complex_of_real z) = 0"
   227 by (unfold complex_of_real_def, auto)
   228 declare Im_complex_of_real [simp]
   229 
   230 
   231 subsection{*Negation*}
   232 
   233 lemma complex_minus: "- Abs_complex(x,y) = Abs_complex(-x,-y)"
   234 apply (unfold complex_minus_def)
   235 apply (simp (no_asm))
   236 done
   237 
   238 lemma complex_Re_minus: "Re (-z) = - Re z"
   239 apply (unfold Re_def)
   240 apply (rule_tac z = z in eq_Abs_complex)
   241 apply (auto simp add: complex_minus)
   242 done
   243 
   244 lemma complex_Im_minus: "Im (-z) = - Im z"
   245 apply (unfold Im_def)
   246 apply (rule_tac z = z in eq_Abs_complex)
   247 apply (auto simp add: complex_minus)
   248 done
   249 
   250 lemma complex_minus_minus: "- (- z) = (z::complex)"
   251 apply (unfold complex_minus_def)
   252 apply (simp (no_asm))
   253 done
   254 declare complex_minus_minus [simp]
   255 
   256 lemma inj_complex_minus: "inj(%r::complex. -r)"
   257 apply (rule inj_onI)
   258 apply (drule_tac f = uminus in arg_cong, simp)
   259 done
   260 
   261 lemma complex_minus_zero: "-(0::complex) = 0"
   262 apply (unfold complex_zero_def)
   263 apply (simp (no_asm) add: complex_minus)
   264 done
   265 declare complex_minus_zero [simp]
   266 
   267 lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))"
   268 apply (rule_tac z = x in eq_Abs_complex)
   269 apply (auto dest: inj_Abs_complex [THEN injD]
   270             simp add: complex_zero_def complex_minus)
   271 done
   272 declare complex_minus_zero_iff [simp]
   273 
   274 lemma complex_minus_zero_iff2: "(0 = -x) = (x = (0::real))"
   275 by (auto dest: sym)
   276 declare complex_minus_zero_iff2 [simp]
   277 
   278 lemma complex_minus_not_zero_iff: "(-x \<noteq> 0) = (x \<noteq> (0::complex))"
   279 by auto
   280 
   281 
   282 subsection{*Addition*}
   283 
   284 lemma complex_add:
   285       "Abs_complex(x1,y1) + Abs_complex(x2,y2) = Abs_complex(x1+x2,y1+y2)"
   286 apply (unfold complex_add_def)
   287 apply (simp (no_asm))
   288 done
   289 
   290 lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)"
   291 apply (unfold Re_def)
   292 apply (rule_tac z = x in eq_Abs_complex)
   293 apply (rule_tac z = y in eq_Abs_complex)
   294 apply (auto simp add: complex_add)
   295 done
   296 
   297 lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)"
   298 apply (unfold Im_def)
   299 apply (rule_tac z = x in eq_Abs_complex)
   300 apply (rule_tac z = y in eq_Abs_complex)
   301 apply (auto simp add: complex_add)
   302 done
   303 
   304 lemma complex_add_commute: "(u::complex) + v = v + u"
   305 apply (unfold complex_add_def)
   306 apply (simp (no_asm) add: real_add_commute)
   307 done
   308 
   309 lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)"
   310 apply (unfold complex_add_def)
   311 apply (simp (no_asm) add: real_add_assoc)
   312 done
   313 
   314 lemma complex_add_left_commute: "(x::complex) + (y + z) = y + (x + z)"
   315 apply (unfold complex_add_def)
   316 apply (simp (no_asm) add: add_left_commute)
   317 done
   318 
   319 lemmas complex_add_ac = complex_add_assoc complex_add_commute
   320                       complex_add_left_commute
   321 
   322 lemma complex_add_zero_left: "(0::complex) + z = z"
   323 apply (unfold complex_add_def complex_zero_def)
   324 apply (simp (no_asm))
   325 done
   326 declare complex_add_zero_left [simp]
   327 
   328 lemma complex_add_zero_right: "z + (0::complex) = z"
   329 apply (unfold complex_add_def complex_zero_def)
   330 apply (simp (no_asm))
   331 done
   332 declare complex_add_zero_right [simp]
   333 
   334 lemma complex_add_minus_right_zero:
   335       "z + -z = (0::complex)"
   336 apply (unfold complex_add_def complex_minus_def complex_zero_def)
   337 apply (simp (no_asm))
   338 done
   339 declare complex_add_minus_right_zero [simp]
   340 
   341 lemma complex_add_minus_left:
   342       "-z + z = (0::complex)"
   343 apply (unfold complex_add_def complex_minus_def complex_zero_def)
   344 apply (simp (no_asm))
   345 done
   346 
   347 lemma complex_add_minus_cancel: "z + (- z + w) = (w::complex)"
   348 apply (simp (no_asm) add: complex_add_assoc [symmetric])
   349 done
   350 
   351 lemma complex_minus_add_cancel: "(-z) + (z + w) = (w::complex)"
   352 by (simp add: complex_add_minus_left complex_add_assoc [symmetric])
   353 
   354 declare complex_add_minus_cancel [simp] complex_minus_add_cancel [simp]
   355 
   356 lemma complex_add_minus_eq_minus: "x + y = (0::complex) ==> x = -y"
   357 by (auto simp add: complex_Re_Im_cancel_iff complex_Re_add complex_Im_add complex_Re_minus complex_Im_minus)
   358 
   359 lemma complex_minus_add_distrib: "-(x + y) = -x + -(y::complex)"
   360 apply (rule_tac z = x in eq_Abs_complex)
   361 apply (rule_tac z = y in eq_Abs_complex)
   362 apply (auto simp add: complex_minus complex_add)
   363 done
   364 declare complex_minus_add_distrib [simp]
   365 
   366 lemma complex_add_left_cancel: "((x::complex) + y = x + z) = (y = z)"
   367 apply safe
   368 apply (drule_tac f = "%t.-x + t" in arg_cong)
   369 apply (simp add: complex_add_minus_left complex_add_assoc [symmetric])
   370 done
   371 declare complex_add_left_cancel [iff]
   372 
   373 lemma complex_add_right_cancel: "(y + (x::complex)= z + x) = (y = z)"
   374 apply (simp (no_asm) add: complex_add_commute)
   375 done
   376 declare complex_add_right_cancel [simp]
   377 
   378 lemma complex_eq_minus_iff: "((x::complex) = y) = (0 = x + - y)"
   379 apply safe
   380 apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto)
   381 done
   382 
   383 lemma complex_eq_minus_iff2: "((x::complex) = y) = (x + - y = 0)"
   384 apply safe
   385 apply (rule_tac [2] x1 = "-y" in complex_add_right_cancel [THEN iffD1], auto)
   386 done
   387 
   388 lemma complex_diff_0: "(0::complex) - x = -x"
   389 apply (simp (no_asm) add: complex_diff_def)
   390 done
   391 
   392 lemma complex_diff_0_right: "x - (0::complex) = x"
   393 apply (simp (no_asm) add: complex_diff_def)
   394 done
   395 
   396 lemma complex_diff_self: "x - x = (0::complex)"
   397 apply (simp (no_asm) add: complex_diff_def)
   398 done
   399 
   400 declare complex_diff_0 [simp] complex_diff_0_right [simp] complex_diff_self [simp]
   401 
   402 lemma complex_diff:
   403       "Abs_complex(x1,y1) - Abs_complex(x2,y2) = Abs_complex(x1-x2,y1-y2)"
   404 apply (unfold complex_diff_def)
   405 apply (simp (no_asm) add: complex_add complex_minus)
   406 done
   407 
   408 lemma complex_diff_eq_eq: "((x::complex) - y = z) = (x = z + y)"
   409 by (auto simp add: complex_add_minus_left complex_diff_def complex_add_assoc)
   410 
   411 
   412 subsection{*Multiplication*}
   413 
   414 lemma complex_mult:
   415       "Abs_complex(x1,y1) * Abs_complex(x2,y2) =
   416        Abs_complex(x1*x2 - y1*y2,x1*y2 + y1*x2)"
   417 apply (unfold complex_mult_def)
   418 apply (simp (no_asm))
   419 done
   420 
   421 lemma complex_mult_commute: "(w::complex) * z = z * w"
   422 apply (unfold complex_mult_def)
   423 apply (simp (no_asm) add: real_mult_commute real_add_commute)
   424 done
   425 
   426 lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"
   427 apply (unfold complex_mult_def)
   428 apply (simp (no_asm) add: complex_Re_Im_cancel_iff real_mult_assoc right_diff_distrib right_distrib left_diff_distrib left_distrib mult_left_commute)
   429 done
   430 
   431 lemma complex_mult_left_commute: "(x::complex) * (y * z) = y * (x * z)"
   432 apply (unfold complex_mult_def)
   433 apply (simp (no_asm) add: complex_Re_Im_cancel_iff mult_left_commute right_diff_distrib right_distrib)
   434 done
   435 
   436 lemmas complex_mult_ac = complex_mult_assoc complex_mult_commute
   437                       complex_mult_left_commute
   438 
   439 lemma complex_mult_one_left: "(1::complex) * z = z"
   440 apply (unfold complex_one_def)
   441 apply (rule_tac z = z in eq_Abs_complex)
   442 apply (simp (no_asm_simp) add: complex_mult)
   443 done
   444 declare complex_mult_one_left [simp]
   445 
   446 lemma complex_mult_one_right: "z * (1::complex) = z"
   447 apply (simp (no_asm) add: complex_mult_commute)
   448 done
   449 declare complex_mult_one_right [simp]
   450 
   451 lemma complex_mult_zero_left: "(0::complex) * z = 0"
   452 apply (unfold complex_zero_def)
   453 apply (rule_tac z = z in eq_Abs_complex)
   454 apply (simp (no_asm_simp) add: complex_mult)
   455 done
   456 declare complex_mult_zero_left [simp]
   457 
   458 lemma complex_mult_zero_right: "z * 0 = (0::complex)"
   459 apply (simp (no_asm) add: complex_mult_commute)
   460 done
   461 declare complex_mult_zero_right [simp]
   462 
   463 lemma complex_divide_zero: "0 / z = (0::complex)"
   464 by (unfold complex_divide_def, auto)
   465 declare complex_divide_zero [simp]
   466 
   467 lemma complex_minus_mult_eq1: "-(x * y) = -x * (y::complex)"
   468 apply (rule_tac z = x in eq_Abs_complex)
   469 apply (rule_tac z = y in eq_Abs_complex)
   470 apply (auto simp add: complex_mult complex_minus real_diff_def)
   471 done
   472 
   473 lemma complex_minus_mult_eq2: "-(x * y) = x * -(y::complex)"
   474 apply (rule_tac z = x in eq_Abs_complex)
   475 apply (rule_tac z = y in eq_Abs_complex)
   476 apply (auto simp add: complex_mult complex_minus real_diff_def)
   477 done
   478 
   479 lemma complex_add_mult_distrib: "((z1::complex) + z2) * w = (z1 * w) + (z2 * w)"
   480 apply (rule_tac z = z1 in eq_Abs_complex)
   481 apply (rule_tac z = z2 in eq_Abs_complex)
   482 apply (rule_tac z = w in eq_Abs_complex)
   483 apply (auto simp add: complex_mult complex_add left_distrib real_diff_def add_ac)
   484 done
   485 
   486 lemma complex_add_mult_distrib2: "(w::complex) * (z1 + z2) = (w * z1) + (w * z2)"
   487 apply (rule_tac z1 = "z1 + z2" in complex_mult_commute [THEN ssubst])
   488 apply (simp (no_asm) add: complex_add_mult_distrib)
   489 apply (simp (no_asm) add: complex_mult_commute)
   490 done
   491 
   492 lemma complex_zero_not_eq_one: "(0::complex) \<noteq> 1"
   493 apply (unfold complex_zero_def complex_one_def)
   494 apply (simp (no_asm) add: complex_Re_Im_cancel_iff)
   495 done
   496 declare complex_zero_not_eq_one [simp]
   497 declare complex_zero_not_eq_one [THEN not_sym, simp]
   498 
   499 
   500 subsection{*Inverse*}
   501 
   502 lemma complex_inverse:
   503      "inverse (Abs_complex(x,y)) =
   504       Abs_complex(x/(x ^ 2 + y ^ 2),-y/(x ^ 2 + y ^ 2))"
   505 apply (unfold complex_inverse_def)
   506 apply (simp (no_asm))
   507 done
   508 
   509 lemma COMPLEX_INVERSE_ZERO: "inverse 0 = (0::complex)"
   510 by (unfold complex_inverse_def complex_zero_def, auto)
   511 
   512 lemma COMPLEX_DIVISION_BY_ZERO: "a / (0::complex) = 0"
   513 apply (simp (no_asm) add: complex_divide_def COMPLEX_INVERSE_ZERO)
   514 done
   515 
   516 instance complex :: division_by_zero
   517 proof
   518   fix x :: complex
   519   show "inverse 0 = (0::complex)" by (rule COMPLEX_INVERSE_ZERO)
   520   show "x/0 = 0" by (rule COMPLEX_DIVISION_BY_ZERO) 
   521 qed
   522 
   523 lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
   524 apply (rule_tac z = z in eq_Abs_complex)
   525 apply (auto simp add: complex_mult complex_inverse complex_one_def 
   526        complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
   527 apply (drule_tac y = y in real_sum_squares_not_zero)
   528 apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
   529 done
   530 declare complex_mult_inv_left [simp]
   531 
   532 lemma complex_mult_inv_right: "z \<noteq> (0::complex) ==> z * inverse(z) = 1"
   533 by (auto intro: complex_mult_commute [THEN subst])
   534 declare complex_mult_inv_right [simp]
   535 
   536 
   537 subsection {* The field of complex numbers *}
   538 
   539 instance complex :: field
   540 proof
   541   fix z u v w :: complex
   542   show "(u + v) + w = u + (v + w)"
   543     by (rule complex_add_assoc) 
   544   show "z + w = w + z"
   545     by (rule complex_add_commute) 
   546   show "0 + z = z"
   547     by (rule complex_add_zero_left) 
   548   show "-z + z = 0"
   549     by (rule complex_add_minus_left) 
   550   show "z - w = z + -w"
   551     by (simp add: complex_diff_def)
   552   show "(u * v) * w = u * (v * w)"
   553     by (rule complex_mult_assoc) 
   554   show "z * w = w * z"
   555     by (rule complex_mult_commute) 
   556   show "1 * z = z"
   557     by (rule complex_mult_one_left) 
   558   show "0 \<noteq> (1::complex)"
   559     by (rule complex_zero_not_eq_one) 
   560   show "(u + v) * w = u * w + v * w"
   561     by (rule complex_add_mult_distrib) 
   562   show "z+u = z+v ==> u=v"
   563     proof -
   564       assume eq: "z+u = z+v" 
   565       hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
   566       thus "u = v" by (simp add: complex_add_minus_left)
   567     qed
   568   assume neq: "w \<noteq> 0"
   569   thus "z / w = z * inverse w"
   570     by (simp add: complex_divide_def)
   571   show "inverse w * w = 1"
   572     by (simp add: neq complex_mult_inv_left) 
   573 qed
   574 
   575 
   576 lemma complex_minus_mult_commute: "-x * y = x * -(y::complex)"
   577 apply (simp)
   578 done
   579 
   580 subsection{*Embedding Properties for @{term complex_of_real} Map*}
   581 
   582 lemma inj_complex_of_real: "inj complex_of_real"
   583 apply (rule inj_onI)
   584 apply (auto dest: inj_Abs_complex [THEN injD] simp add: complex_of_real_def)
   585 done
   586 
   587 lemma complex_of_real_one:
   588       "complex_of_real 1 = 1"
   589 apply (unfold complex_one_def complex_of_real_def)
   590 apply (rule refl)
   591 done
   592 declare complex_of_real_one [simp]
   593 
   594 lemma complex_of_real_zero:
   595       "complex_of_real 0 = 0"
   596 apply (unfold complex_zero_def complex_of_real_def)
   597 apply (rule refl)
   598 done
   599 declare complex_of_real_zero [simp]
   600 
   601 lemma complex_of_real_eq_iff:
   602      "(complex_of_real x = complex_of_real y) = (x = y)"
   603 by (auto dest: inj_complex_of_real [THEN injD])
   604 declare complex_of_real_eq_iff [iff]
   605 
   606 lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
   607 apply (simp (no_asm) add: complex_of_real_def complex_minus)
   608 done
   609 
   610 lemma complex_of_real_inverse:
   611  "complex_of_real(inverse x) = inverse(complex_of_real x)"
   612 apply (case_tac "x=0", simp)
   613 apply (simp add: complex_inverse complex_of_real_def real_divide_def 
   614                  inverse_mult_distrib power2_eq_square)
   615 done
   616 
   617 lemma complex_of_real_add:
   618  "complex_of_real x + complex_of_real y = complex_of_real (x + y)"
   619 apply (simp (no_asm) add: complex_add complex_of_real_def)
   620 done
   621 
   622 lemma complex_of_real_diff:
   623  "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
   624 apply (simp (no_asm) add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)
   625 done
   626 
   627 lemma complex_of_real_mult:
   628  "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
   629 apply (simp (no_asm) add: complex_mult complex_of_real_def)
   630 done
   631 
   632 lemma complex_of_real_divide:
   633       "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
   634 apply (unfold complex_divide_def)
   635 apply (case_tac "y=0")
   636 apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
   637 apply (simp (no_asm_simp) add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)
   638 done
   639 
   640 lemma complex_mod: "cmod (Abs_complex(x,y)) = sqrt(x ^ 2 + y ^ 2)"
   641 apply (unfold cmod_def)
   642 apply (simp (no_asm))
   643 done
   644 
   645 lemma complex_mod_zero: "cmod(0) = 0"
   646 apply (unfold cmod_def)
   647 apply (simp (no_asm))
   648 done
   649 declare complex_mod_zero [simp]
   650 
   651 lemma complex_mod_one [simp]: "cmod(1) = 1"
   652 by (simp add: cmod_def power2_eq_square)
   653 
   654 lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
   655 apply (simp add: complex_of_real_def power2_eq_square complex_mod)
   656 done
   657 declare complex_mod_complex_of_real [simp]
   658 
   659 lemma complex_of_real_abs:
   660      "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
   661 by (simp)
   662 
   663 
   664 
   665 subsection{*Conjugation is an Automorphism*}
   666 
   667 lemma complex_cnj: "cnj (Abs_complex(x,y)) = Abs_complex(x,-y)"
   668 apply (unfold cnj_def)
   669 apply (simp (no_asm))
   670 done
   671 
   672 lemma inj_cnj: "inj cnj"
   673 apply (rule inj_onI)
   674 apply (auto simp add: cnj_def Abs_complex_cancel_iff complex_Re_Im_cancel_iff)
   675 done
   676 
   677 lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)"
   678 by (auto dest: inj_cnj [THEN injD])
   679 declare complex_cnj_cancel_iff [simp]
   680 
   681 lemma complex_cnj_cnj: "cnj (cnj z) = z"
   682 apply (unfold cnj_def)
   683 apply (simp (no_asm))
   684 done
   685 declare complex_cnj_cnj [simp]
   686 
   687 lemma complex_cnj_complex_of_real:
   688  "cnj (complex_of_real x) = complex_of_real x"
   689 apply (unfold complex_of_real_def)
   690 apply (simp (no_asm) add: complex_cnj)
   691 done
   692 declare complex_cnj_complex_of_real [simp]
   693 
   694 lemma complex_mod_cnj: "cmod (cnj z) = cmod z"
   695 apply (rule_tac z = z in eq_Abs_complex)
   696 apply (simp (no_asm_simp) add: complex_cnj complex_mod power2_eq_square)
   697 done
   698 declare complex_mod_cnj [simp]
   699 
   700 lemma complex_cnj_minus: "cnj (-z) = - cnj z"
   701 apply (unfold cnj_def)
   702 apply (simp (no_asm) add: complex_minus complex_Re_minus complex_Im_minus)
   703 done
   704 
   705 lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"
   706 apply (rule_tac z = z in eq_Abs_complex)
   707 apply (simp (no_asm_simp) add: complex_cnj complex_inverse power2_eq_square)
   708 done
   709 
   710 lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"
   711 apply (rule_tac z = w in eq_Abs_complex)
   712 apply (rule_tac z = z in eq_Abs_complex)
   713 apply (simp (no_asm_simp) add: complex_cnj complex_add)
   714 done
   715 
   716 lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
   717 apply (unfold complex_diff_def)
   718 apply (simp (no_asm) add: complex_cnj_add complex_cnj_minus)
   719 done
   720 
   721 lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
   722 apply (rule_tac z = w in eq_Abs_complex)
   723 apply (rule_tac z = z in eq_Abs_complex)
   724 apply (simp (no_asm_simp) add: complex_cnj complex_mult)
   725 done
   726 
   727 lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)"
   728 apply (unfold complex_divide_def)
   729 apply (simp (no_asm) add: complex_cnj_mult complex_cnj_inverse)
   730 done
   731 
   732 lemma complex_cnj_one: "cnj 1 = 1"
   733 apply (unfold cnj_def complex_one_def)
   734 apply (simp (no_asm))
   735 done
   736 declare complex_cnj_one [simp]
   737 
   738 lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
   739 apply (rule_tac z = z in eq_Abs_complex)
   740 apply (simp (no_asm_simp) add: complex_add complex_cnj complex_of_real_def)
   741 done
   742 
   743 lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
   744 apply (rule_tac z = z in eq_Abs_complex)
   745 apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def 
   746                  complex_minus i_def complex_mult)
   747 done
   748 
   749 lemma complex_cnj_zero [simp]: "cnj 0 = 0"
   750 by (simp add: cnj_def complex_zero_def)
   751 
   752 lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)"
   753 apply (rule_tac z = z in eq_Abs_complex)
   754 apply (auto simp add: complex_zero_def complex_cnj)
   755 done
   756 declare complex_cnj_zero_iff [iff]
   757 
   758 lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
   759 apply (rule_tac z = z in eq_Abs_complex)
   760 apply (auto simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
   761 done
   762 
   763 
   764 subsection{*Algebra*}
   765 
   766 lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))"
   767 apply (unfold complex_zero_def)
   768 apply (rule_tac z = x in eq_Abs_complex)
   769 apply (rule_tac z = y in eq_Abs_complex)
   770 apply (auto simp add: complex_add)
   771 done
   772 declare complex_add_left_cancel_zero [simp]
   773 
   774 lemma complex_diff_mult_distrib:
   775       "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)"
   776 apply (unfold complex_diff_def)
   777 apply (simp (no_asm) add: complex_add_mult_distrib)
   778 done
   779 
   780 lemma complex_diff_mult_distrib2:
   781       "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)"
   782 apply (unfold complex_diff_def)
   783 apply (simp (no_asm) add: complex_add_mult_distrib2)
   784 done
   785 
   786 
   787 subsection{*Modulus*}
   788 
   789 lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
   790 apply (rule_tac z = x in eq_Abs_complex)
   791 apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square)
   792 done
   793 declare complex_mod_eq_zero_cancel [simp]
   794 
   795 lemma complex_mod_complex_of_real_of_nat: "cmod (complex_of_real(real (n::nat))) = real n"
   796 apply (simp (no_asm))
   797 done
   798 declare complex_mod_complex_of_real_of_nat [simp]
   799 
   800 lemma complex_mod_minus: "cmod (-x) = cmod(x)"
   801 apply (rule_tac z = x in eq_Abs_complex)
   802 apply (simp (no_asm_simp) add: complex_mod complex_minus power2_eq_square)
   803 done
   804 declare complex_mod_minus [simp]
   805 
   806 lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
   807 apply (rule_tac z = z in eq_Abs_complex)
   808 apply (simp (no_asm_simp) add: complex_mod complex_cnj complex_mult);
   809 apply (simp (no_asm) add: power2_eq_square real_abs_def)
   810 done
   811 
   812 lemma complex_mod_squared: "cmod(Abs_complex(x,y)) ^ 2 = x ^ 2 + y ^ 2"
   813 by (unfold cmod_def, auto)
   814 
   815 lemma complex_mod_ge_zero: "0 \<le> cmod x"
   816 apply (unfold cmod_def)
   817 apply (auto intro: real_sqrt_ge_zero)
   818 done
   819 declare complex_mod_ge_zero [simp]
   820 
   821 lemma abs_cmod_cancel: "abs(cmod x) = cmod x"
   822 by (auto intro: abs_eqI1)
   823 declare abs_cmod_cancel [simp]
   824 
   825 lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
   826 apply (rule_tac z = x in eq_Abs_complex)
   827 apply (rule_tac z = y in eq_Abs_complex)
   828 apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
   829 apply (rule_tac n = 1 in power_inject_base)
   830 apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
   831 apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac)
   832 done
   833 
   834 lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
   835 apply (rule_tac z = x in eq_Abs_complex)
   836 apply (rule_tac z = y in eq_Abs_complex)
   837 apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   838 apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
   839 done
   840 
   841 lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)"
   842 apply (rule_tac z = x in eq_Abs_complex)
   843 apply (rule_tac z = y in eq_Abs_complex)
   844 apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
   845 done
   846 declare complex_Re_mult_cnj_le_cmod [simp]
   847 
   848 lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)"
   849 apply (cut_tac x = x and y = y in complex_Re_mult_cnj_le_cmod)
   850 apply (simp add: complex_mod_mult)
   851 done
   852 declare complex_Re_mult_cnj_le_cmod2 [simp]
   853 
   854 lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
   855 apply (simp (no_asm) add: left_distrib right_distrib power2_eq_square)
   856 done
   857 
   858 lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
   859 apply (simp (no_asm) add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
   860 done
   861 declare complex_mod_triangle_squared [simp]
   862 
   863 lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
   864 apply (rule order_trans [OF _ complex_mod_ge_zero]) 
   865 apply (simp (no_asm))
   866 done
   867 declare complex_mod_minus_le_complex_mod [simp]
   868 
   869 lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)"
   870 apply (rule_tac n = 1 in realpow_increasing)
   871 apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
   872             simp add: power2_eq_square [symmetric])
   873 done
   874 declare complex_mod_triangle_ineq [simp]
   875 
   876 lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
   877 apply (cut_tac x1 = b and y1 = a and c = "-cmod b" 
   878        in complex_mod_triangle_ineq [THEN add_right_mono])
   879 apply (simp (no_asm))
   880 done
   881 declare complex_mod_triangle_ineq2 [simp]
   882 
   883 lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"
   884 apply (rule_tac z = x in eq_Abs_complex)
   885 apply (rule_tac z = y in eq_Abs_complex)
   886 apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)
   887 done
   888 
   889 lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"
   890 by (auto intro: order_le_less_trans complex_mod_triangle_ineq)
   891 
   892 lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"
   893 by (auto intro: real_mult_less_mono' simp add: complex_mod_mult)
   894 
   895 lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \<le> cmod(a + b)"
   896 apply (rule linorder_cases [of "cmod(a)" "cmod (b)"])
   897 apply auto
   898 apply (rule order_trans [of _ 0], rule order_less_imp_le)
   899 apply (simp add: compare_rls, simp)  
   900 apply (simp add: compare_rls)
   901 apply (rule complex_mod_minus [THEN subst])
   902 apply (rule order_trans)
   903 apply (rule_tac [2] complex_mod_triangle_ineq)
   904 apply (auto simp add: complex_add_ac)
   905 done
   906 declare complex_mod_diff_ineq [simp]
   907 
   908 lemma complex_Re_le_cmod: "Re z \<le> cmod z"
   909 apply (rule_tac z = z in eq_Abs_complex)
   910 apply (auto simp add: complex_mod simp del: realpow_Suc)
   911 done
   912 declare complex_Re_le_cmod [simp]
   913 
   914 lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"
   915 apply (cut_tac x = z in complex_mod_ge_zero)
   916 apply (drule order_le_imp_less_or_eq, auto)
   917 done
   918 
   919 
   920 subsection{*A Few More Theorems*}
   921 
   922 lemma complex_mod_inverse: "cmod(inverse x) = inverse(cmod x)"
   923 apply (case_tac "x=0", simp add: COMPLEX_INVERSE_ZERO)
   924 apply (rule_tac c1 = "cmod x" in real_mult_left_cancel [THEN iffD1])
   925 apply (auto simp add: complex_mod_mult [symmetric])
   926 done
   927 
   928 lemma complex_mod_divide:
   929       "cmod(x/y) = cmod(x)/(cmod y)"
   930 apply (unfold complex_divide_def real_divide_def)
   931 apply (auto simp add: complex_mod_mult complex_mod_inverse)
   932 done
   933 
   934 lemma complex_inverse_divide:
   935       "inverse(x/y) = y/(x::complex)"
   936 apply (unfold complex_divide_def)
   937 apply (auto simp add: inverse_mult_distrib complex_mult_commute)
   938 done
   939 declare complex_inverse_divide [simp]
   940 
   941 
   942 subsection{*Exponentiation*}
   943 
   944 primrec
   945      complexpow_0:   "z ^ 0       = 1"
   946      complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
   947 
   948 
   949 instance complex :: ringpower
   950 proof
   951   fix z :: complex
   952   fix n :: nat
   953   show "z^0 = 1" by simp
   954   show "z^(Suc n) = z * (z^n)" by simp
   955 qed
   956 
   957 
   958 lemma complex_of_real_pow: "complex_of_real (x ^ n) = (complex_of_real x) ^ n"
   959 apply (induct_tac "n")
   960 apply (auto simp add: complex_of_real_mult [symmetric])
   961 done
   962 
   963 lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
   964 apply (induct_tac "n")
   965 apply (auto simp add: complex_cnj_mult)
   966 done
   967 
   968 lemma complex_mod_complexpow: "cmod(x ^ n) = cmod(x) ^ n"
   969 apply (induct_tac "n")
   970 apply (auto simp add: complex_mod_mult)
   971 done
   972 
   973 lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
   974 by (induct_tac "n", auto)
   975 
   976 lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
   977 by (simp add: i_def complex_mult complex_one_def complex_minus numeral_2_eq_2)
   978 
   979 lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
   980 by (unfold i_def complex_zero_def, auto)
   981 
   982 
   983 subsection{*The Function @{term sgn}*}
   984 
   985 lemma sgn_zero: "sgn 0 = 0"
   986 apply (unfold sgn_def)
   987 apply (simp (no_asm))
   988 done
   989 declare sgn_zero [simp]
   990 
   991 lemma sgn_one: "sgn 1 = 1"
   992 apply (unfold sgn_def)
   993 apply (simp (no_asm))
   994 done
   995 declare sgn_one [simp]
   996 
   997 lemma sgn_minus: "sgn (-z) = - sgn(z)"
   998 by (unfold sgn_def, auto)
   999 
  1000 lemma sgn_eq:
  1001     "sgn z = z / complex_of_real (cmod z)"
  1002 apply (unfold sgn_def)
  1003 apply (simp (no_asm))
  1004 done
  1005 
  1006 lemma complex_split: "\<exists>x y. z = complex_of_real(x) + ii * complex_of_real(y)"
  1007 apply (rule_tac z = z in eq_Abs_complex)
  1008 apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
  1009 done
  1010 
  1011 lemma Re_complex_i: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x"
  1012 by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
  1013 declare Re_complex_i [simp]
  1014 
  1015 lemma Im_complex_i: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
  1016 by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
  1017 declare Im_complex_i [simp]
  1018 
  1019 lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
  1020 apply (unfold i_def complex_of_real_def)
  1021 apply (auto simp add: complex_mult complex_add)
  1022 done
  1023 
  1024 lemma i_mult_eq2: "ii * ii = -(1::complex)"
  1025 apply (unfold i_def complex_one_def)
  1026 apply (simp (no_asm) add: complex_mult complex_minus)
  1027 done
  1028 declare i_mult_eq2 [simp]
  1029 
  1030 lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) =
  1031       sqrt (x ^ 2 + y ^ 2)"
  1032 apply (auto simp add: complex_mult complex_add i_def complex_of_real_def cmod_def)
  1033 done
  1034 
  1035 lemma complex_eq_Re_eq:
  1036      "complex_of_real xa + ii * complex_of_real ya =
  1037       complex_of_real xb + ii * complex_of_real yb
  1038        ==> xa = xb"
  1039 apply (unfold complex_of_real_def i_def)
  1040 apply (auto simp add: complex_mult complex_add)
  1041 done
  1042 
  1043 lemma complex_eq_Im_eq:
  1044      "complex_of_real xa + ii * complex_of_real ya =
  1045       complex_of_real xb + ii * complex_of_real yb
  1046        ==> ya = yb"
  1047 apply (unfold complex_of_real_def i_def)
  1048 apply (auto simp add: complex_mult complex_add)
  1049 done
  1050 
  1051 lemma complex_eq_cancel_iff: "(complex_of_real xa + ii * complex_of_real ya =
  1052        complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
  1053 apply (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
  1054 done
  1055 declare complex_eq_cancel_iff [iff]
  1056 
  1057 lemma complex_eq_cancel_iffA: "(complex_of_real xa + complex_of_real ya * ii =
  1058        complex_of_real xb + complex_of_real yb * ii ) = ((xa = xb) & (ya = yb))"
  1059 apply (auto simp add: complex_mult_commute)
  1060 done
  1061 declare complex_eq_cancel_iffA [iff]
  1062 
  1063 lemma complex_eq_cancel_iffB: "(complex_of_real xa + complex_of_real ya * ii =
  1064        complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
  1065 apply (auto simp add: complex_mult_commute)
  1066 done
  1067 declare complex_eq_cancel_iffB [iff]
  1068 
  1069 lemma complex_eq_cancel_iffC: "(complex_of_real xa + ii * complex_of_real ya  =
  1070        complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
  1071 apply (auto simp add: complex_mult_commute)
  1072 done
  1073 declare complex_eq_cancel_iffC [iff]
  1074 
  1075 lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y =
  1076       complex_of_real xa) = (x = xa & y = 0)"
  1077 apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff)
  1078 apply (simp del: complex_eq_cancel_iff)
  1079 done
  1080 declare complex_eq_cancel_iff2 [simp]
  1081 
  1082 lemma complex_eq_cancel_iff2a: "(complex_of_real x + complex_of_real y * ii =
  1083       complex_of_real xa) = (x = xa & y = 0)"
  1084 apply (auto simp add: complex_mult_commute)
  1085 done
  1086 declare complex_eq_cancel_iff2a [simp]
  1087 
  1088 lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y =
  1089       ii * complex_of_real ya) = (x = 0 & y = ya)"
  1090 apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff)
  1091 apply (simp del: complex_eq_cancel_iff)
  1092 done
  1093 declare complex_eq_cancel_iff3 [simp]
  1094 
  1095 lemma complex_eq_cancel_iff3a: "(complex_of_real x + complex_of_real y * ii =
  1096       ii * complex_of_real ya) = (x = 0 & y = ya)"
  1097 apply (auto simp add: complex_mult_commute)
  1098 done
  1099 declare complex_eq_cancel_iff3a [simp]
  1100 
  1101 lemma complex_split_Re_zero:
  1102      "complex_of_real x + ii * complex_of_real y = 0
  1103       ==> x = 0"
  1104 apply (unfold complex_of_real_def i_def complex_zero_def)
  1105 apply (auto simp add: complex_mult complex_add)
  1106 done
  1107 
  1108 lemma complex_split_Im_zero:
  1109      "complex_of_real x + ii * complex_of_real y = 0
  1110       ==> y = 0"
  1111 apply (unfold complex_of_real_def i_def complex_zero_def)
  1112 apply (auto simp add: complex_mult complex_add)
  1113 done
  1114 
  1115 lemma Re_sgn:
  1116       "Re(sgn z) = Re(z)/cmod z"
  1117 apply (unfold sgn_def complex_divide_def)
  1118 apply (rule_tac z = z in eq_Abs_complex)
  1119 apply (auto simp add: complex_of_real_inverse [symmetric])
  1120 apply (auto simp add: complex_of_real_def complex_mult real_divide_def)
  1121 done
  1122 declare Re_sgn [simp]
  1123 
  1124 lemma Im_sgn:
  1125       "Im(sgn z) = Im(z)/cmod z"
  1126 apply (unfold sgn_def complex_divide_def)
  1127 apply (rule_tac z = z in eq_Abs_complex)
  1128 apply (auto simp add: complex_of_real_inverse [symmetric])
  1129 apply (auto simp add: complex_of_real_def complex_mult real_divide_def)
  1130 done
  1131 declare Im_sgn [simp]
  1132 
  1133 lemma complex_inverse_complex_split:
  1134      "inverse(complex_of_real x + ii * complex_of_real y) =
  1135       complex_of_real(x/(x ^ 2 + y ^ 2)) -
  1136       ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
  1137 apply (unfold complex_of_real_def i_def)
  1138 apply (auto simp add: complex_mult complex_add complex_diff_def complex_minus complex_inverse real_divide_def)
  1139 done
  1140 
  1141 (*----------------------------------------------------------------------------*)
  1142 (* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
  1143 (* many of the theorems are not used - so should they be kept?                *)
  1144 (*----------------------------------------------------------------------------*)
  1145 
  1146 lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
  1147 by (auto simp add: complex_zero_def complex_of_real_def)
  1148 
  1149 lemma Re_mult_i_eq:
  1150     "Re (ii * complex_of_real y) = 0"
  1151 apply (unfold i_def complex_of_real_def)
  1152 apply (auto simp add: complex_mult)
  1153 done
  1154 declare Re_mult_i_eq [simp]
  1155 
  1156 lemma Im_mult_i_eq:
  1157     "Im (ii * complex_of_real y) = y"
  1158 apply (unfold i_def complex_of_real_def)
  1159 apply (auto simp add: complex_mult)
  1160 done
  1161 declare Im_mult_i_eq [simp]
  1162 
  1163 lemma complex_mod_mult_i:
  1164     "cmod (ii * complex_of_real y) = abs y"
  1165 apply (unfold i_def complex_of_real_def)
  1166 apply (auto simp add: complex_mult complex_mod power2_eq_square)
  1167 done
  1168 declare complex_mod_mult_i [simp]
  1169 
  1170 lemma cos_arg_i_mult_zero_pos:
  1171    "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
  1172 apply (unfold arg_def)
  1173 apply (auto simp add: abs_eqI2)
  1174 apply (rule_tac a = "pi/2" in someI2, auto)
  1175 apply (rule order_less_trans [of _ 0], auto)
  1176 done
  1177 
  1178 lemma cos_arg_i_mult_zero_neg:
  1179    "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0"
  1180 apply (unfold arg_def)
  1181 apply (auto simp add: abs_minus_eqI2)
  1182 apply (rule_tac a = "- pi/2" in someI2, auto)
  1183 apply (rule order_trans [of _ 0], auto)
  1184 done
  1185 
  1186 lemma cos_arg_i_mult_zero [simp]
  1187     : "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
  1188 by (cut_tac x = y and y = 0 in linorder_less_linear, 
  1189     auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
  1190 
  1191 
  1192 subsection{*Finally! Polar Form for Complex Numbers*}
  1193 
  1194 lemma complex_split_polar: "\<exists>r a. z = complex_of_real r *
  1195       (complex_of_real(cos a) + ii * complex_of_real(sin a))"
  1196 apply (cut_tac z = z in complex_split)
  1197 apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac)
  1198 done
  1199 
  1200 lemma rcis_Ex: "\<exists>r a. z = rcis r a"
  1201 apply (unfold rcis_def cis_def)
  1202 apply (rule complex_split_polar)
  1203 done
  1204 
  1205 lemma Re_complex_polar: "Re(complex_of_real r *
  1206       (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a"
  1207 apply (auto simp add: complex_add_mult_distrib2 complex_of_real_mult complex_mult_ac)
  1208 done
  1209 declare Re_complex_polar [simp]
  1210 
  1211 lemma Re_rcis: "Re(rcis r a) = r * cos a"
  1212 by (unfold rcis_def cis_def, auto)
  1213 declare Re_rcis [simp]
  1214 
  1215 lemma Im_complex_polar [simp]:
  1216      "Im(complex_of_real r * 
  1217          (complex_of_real(cos a) + ii * complex_of_real(sin a))) = 
  1218       r * sin a"
  1219 by (auto simp add: complex_add_mult_distrib2 complex_of_real_mult mult_ac)
  1220 
  1221 lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
  1222 by (unfold rcis_def cis_def, auto)
  1223 
  1224 lemma complex_mod_complex_polar [simp]:
  1225      "cmod (complex_of_real r * 
  1226             (complex_of_real(cos a) + ii * complex_of_real(sin a))) = 
  1227       abs r"
  1228 by (auto simp add: complex_add_mult_distrib2 cmod_i complex_of_real_mult
  1229                       right_distrib [symmetric] power_mult_distrib mult_ac 
  1230          simp del: realpow_Suc)
  1231 
  1232 lemma complex_mod_rcis: "cmod(rcis r a) = abs r"
  1233 by (unfold rcis_def cis_def, auto)
  1234 declare complex_mod_rcis [simp]
  1235 
  1236 lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
  1237 apply (unfold cmod_def)
  1238 apply (rule real_sqrt_eq_iff [THEN iffD2])
  1239 apply (auto simp add: complex_mult_cnj)
  1240 done
  1241 
  1242 lemma complex_Re_cnj: "Re(cnj z) = Re z"
  1243 apply (rule_tac z = z in eq_Abs_complex)
  1244 apply (auto simp add: complex_cnj)
  1245 done
  1246 declare complex_Re_cnj [simp]
  1247 
  1248 lemma complex_Im_cnj: "Im(cnj z) = - Im z"
  1249 apply (rule_tac z = z in eq_Abs_complex)
  1250 apply (auto simp add: complex_cnj)
  1251 done
  1252 declare complex_Im_cnj [simp]
  1253 
  1254 lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0"
  1255 apply (rule_tac z = z in eq_Abs_complex)
  1256 apply (auto simp add: complex_cnj complex_mult)
  1257 done
  1258 declare complex_In_mult_cnj_zero [simp]
  1259 
  1260 lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
  1261 apply (rule_tac z = z in eq_Abs_complex)
  1262 apply (rule_tac z = w in eq_Abs_complex)
  1263 apply (auto simp add: complex_mult)
  1264 done
  1265 
  1266 lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c"
  1267 apply (unfold complex_of_real_def)
  1268 apply (rule_tac z = z in eq_Abs_complex)
  1269 apply (auto simp add: complex_mult)
  1270 done
  1271 declare complex_Re_mult_complex_of_real [simp]
  1272 
  1273 lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c"
  1274 apply (unfold complex_of_real_def)
  1275 apply (rule_tac z = z in eq_Abs_complex)
  1276 apply (auto simp add: complex_mult)
  1277 done
  1278 declare complex_Im_mult_complex_of_real [simp]
  1279 
  1280 lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)"
  1281 apply (unfold complex_of_real_def)
  1282 apply (rule_tac z = z in eq_Abs_complex)
  1283 apply (auto simp add: complex_mult)
  1284 done
  1285 declare complex_Re_mult_complex_of_real2 [simp]
  1286 
  1287 lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)"
  1288 apply (unfold complex_of_real_def)
  1289 apply (rule_tac z = z in eq_Abs_complex)
  1290 apply (auto simp add: complex_mult)
  1291 done
  1292 declare complex_Im_mult_complex_of_real2 [simp]
  1293 
  1294 (*---------------------------------------------------------------------------*)
  1295 (*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
  1296 (*---------------------------------------------------------------------------*)
  1297 
  1298 lemma cis_rcis_eq: "cis a = rcis 1 a"
  1299 apply (unfold rcis_def)
  1300 apply (simp (no_asm))
  1301 done
  1302 
  1303 lemma rcis_mult:
  1304   "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
  1305 apply (unfold rcis_def cis_def)
  1306 apply (auto simp add: cos_add sin_add complex_add_mult_distrib2 complex_add_mult_distrib complex_mult_ac complex_add_ac)
  1307 apply (auto simp add: complex_add_mult_distrib2 [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)
  1308 apply (auto simp add: complex_add_ac)
  1309 apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac)
  1310 done
  1311 
  1312 lemma cis_mult: "cis a * cis b = cis (a + b)"
  1313 apply (simp (no_asm) add: cis_rcis_eq rcis_mult)
  1314 done
  1315 
  1316 lemma cis_zero: "cis 0 = 1"
  1317 by (unfold cis_def, auto)
  1318 declare cis_zero [simp]
  1319 
  1320 lemma cis_zero2: "cis 0 = complex_of_real 1"
  1321 by (unfold cis_def, auto)
  1322 declare cis_zero2 [simp]
  1323 
  1324 lemma rcis_zero_mod: "rcis 0 a = 0"
  1325 apply (unfold rcis_def)
  1326 apply (simp (no_asm))
  1327 done
  1328 declare rcis_zero_mod [simp]
  1329 
  1330 lemma rcis_zero_arg: "rcis r 0 = complex_of_real r"
  1331 apply (unfold rcis_def)
  1332 apply (simp (no_asm))
  1333 done
  1334 declare rcis_zero_arg [simp]
  1335 
  1336 lemma complex_of_real_minus_one:
  1337    "complex_of_real (-(1::real)) = -(1::complex)"
  1338 apply (unfold complex_of_real_def complex_one_def)
  1339 apply (simp (no_asm) add: complex_minus)
  1340 done
  1341 
  1342 lemma complex_i_mult_minus: "ii * (ii * x) = - x"
  1343 apply (simp (no_asm) add: complex_mult_assoc [symmetric])
  1344 done
  1345 declare complex_i_mult_minus [simp]
  1346 
  1347 lemma complex_i_mult_minus2: "ii * ii * x = - x"
  1348 apply (simp (no_asm))
  1349 done
  1350 declare complex_i_mult_minus2 [simp]
  1351 
  1352 lemma cis_real_of_nat_Suc_mult:
  1353    "cis (real (Suc n) * a) = cis a * cis (real n * a)"
  1354 apply (unfold cis_def)
  1355 apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add complex_add_mult_distrib complex_add_mult_distrib2 complex_of_real_add complex_of_real_mult complex_mult_ac complex_add_ac)
  1356 apply (auto simp add: complex_add_mult_distrib2 [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)
  1357 done
  1358 
  1359 lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
  1360 apply (induct_tac "n")
  1361 apply (auto simp add: cis_real_of_nat_Suc_mult)
  1362 done
  1363 
  1364 lemma DeMoivre2:
  1365    "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
  1366 apply (unfold rcis_def)
  1367 apply (auto simp add: power_mult_distrib DeMoivre complex_of_real_pow)
  1368 done
  1369 
  1370 lemma cis_inverse: "inverse(cis a) = cis (-a)"
  1371 apply (unfold cis_def)
  1372 apply (auto simp add: complex_inverse_complex_split complex_of_real_minus complex_diff_def)
  1373 done
  1374 declare cis_inverse [simp]
  1375 
  1376 lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
  1377 apply (case_tac "r=0", simp)
  1378 apply (auto simp add: complex_inverse_complex_split right_distrib 
  1379             complex_of_real_mult rcis_def cis_def power2_eq_square mult_ac)
  1380 apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def)
  1381 done
  1382 
  1383 lemma cis_divide: "cis a / cis b = cis (a - b)"
  1384 apply (unfold complex_divide_def)
  1385 apply (auto simp add: cis_mult real_diff_def)
  1386 done
  1387 
  1388 lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
  1389 apply (unfold complex_divide_def)
  1390 apply (case_tac "r2=0")
  1391 apply (simp (no_asm_simp) add: DIVISION_BY_ZERO COMPLEX_INVERSE_ZERO)
  1392 apply (auto simp add: rcis_inverse rcis_mult real_diff_def)
  1393 done
  1394 
  1395 lemma Re_cis: "Re(cis a) = cos a"
  1396 by (unfold cis_def, auto)
  1397 declare Re_cis [simp]
  1398 
  1399 lemma Im_cis: "Im(cis a) = sin a"
  1400 by (unfold cis_def, auto)
  1401 declare Im_cis [simp]
  1402 
  1403 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
  1404 by (auto simp add: DeMoivre)
  1405 
  1406 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
  1407 by (auto simp add: DeMoivre)
  1408 
  1409 lemma expi_Im_split:
  1410     "expi (ii * complex_of_real y) =
  1411      complex_of_real (cos y) + ii * complex_of_real (sin y)"
  1412 by (unfold expi_def cis_def, auto)
  1413 
  1414 lemma expi_Im_cis:
  1415     "expi (ii * complex_of_real y) = cis y"
  1416 by (unfold expi_def, auto)
  1417 
  1418 lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
  1419 apply (unfold expi_def)
  1420 apply (auto simp add: complex_Re_add exp_add complex_Im_add cis_mult [symmetric] complex_of_real_mult complex_mult_ac)
  1421 done
  1422 
  1423 lemma expi_complex_split:
  1424      "expi(complex_of_real x + ii * complex_of_real y) =
  1425       complex_of_real (exp(x)) * cis y"
  1426 by (unfold expi_def, auto)
  1427 
  1428 lemma expi_zero: "expi (0::complex) = 1"
  1429 by (unfold expi_def, auto)
  1430 declare expi_zero [simp]
  1431 
  1432 lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
  1433 apply (rule_tac z = z in eq_Abs_complex)
  1434 apply (rule_tac z = w in eq_Abs_complex)
  1435 apply (auto simp add: complex_mult)
  1436 done
  1437 
  1438 lemma complex_Im_mult_eq:
  1439      "Im (w * z) = Re w * Im z + Im w * Re z"
  1440 apply (rule_tac z = z in eq_Abs_complex)
  1441 apply (rule_tac z = w in eq_Abs_complex)
  1442 apply (auto simp add: complex_mult)
  1443 done
  1444 
  1445 lemma complex_expi_Ex: 
  1446    "\<exists>a r. z = complex_of_real r * expi a"
  1447 apply (cut_tac z = z in rcis_Ex)
  1448 apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
  1449 apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
  1450 done
  1451 
  1452 
  1453 (****
  1454 Goal "[| - pi < a; a \<le> pi |] ==> (-pi < a & a \<le> 0) | (0 \<le> a & a \<le> pi)"
  1455 by Auto_tac
  1456 qed "lemma_split_interval";
  1457 
  1458 Goalw [arg_def]
  1459   "[| r \<noteq> 0; - pi < a; a \<le> pi |] \
  1460 \  ==> arg(complex_of_real r * \
  1461 \      (complex_of_real(cos a) + ii * complex_of_real(sin a))) = a";
  1462 by Auto_tac
  1463 by (cut_inst_tac [("x","0"),("y","r")] linorder_less_linear 1);
  1464 by (auto_tac (claset(),simpset() addsimps (map (full_rename_numerals thy)
  1465     [rabs_eqI2,rabs_minus_eqI2,real_minus_rinv]) [real_divide_def,
  1466     minus_mult_right RS sym] mult_ac));
  1467 by (auto_tac (claset(),simpset() addsimps [real_mult_assoc RS sym]));
  1468 by (dtac lemma_split_interval 1 THEN safe)
  1469 ****)
  1470 
  1471 
  1472 ML
  1473 {*
  1474 val complex_zero_def = thm"complex_zero_def";
  1475 val complex_one_def = thm"complex_one_def";
  1476 val complex_minus_def = thm"complex_minus_def";
  1477 val complex_diff_def = thm"complex_diff_def";
  1478 val complex_divide_def = thm"complex_divide_def";
  1479 val complex_mult_def = thm"complex_mult_def";
  1480 val complex_add_def = thm"complex_add_def";
  1481 val complex_of_real_def = thm"complex_of_real_def";
  1482 val i_def = thm"i_def";
  1483 val expi_def = thm"expi_def";
  1484 val cis_def = thm"cis_def";
  1485 val rcis_def = thm"rcis_def";
  1486 val cmod_def = thm"cmod_def";
  1487 val cnj_def = thm"cnj_def";
  1488 val sgn_def = thm"sgn_def";
  1489 val arg_def = thm"arg_def";
  1490 val complexpow_0 = thm"complexpow_0";
  1491 val complexpow_Suc = thm"complexpow_Suc";
  1492 
  1493 val inj_Rep_complex = thm"inj_Rep_complex";
  1494 val inj_Abs_complex = thm"inj_Abs_complex";
  1495 val Abs_complex_cancel_iff = thm"Abs_complex_cancel_iff";
  1496 val pair_mem_complex = thm"pair_mem_complex";
  1497 val Abs_complex_inverse2 = thm"Abs_complex_inverse2";
  1498 val eq_Abs_complex = thm"eq_Abs_complex";
  1499 val Re = thm"Re";
  1500 val Im = thm"Im";
  1501 val Abs_complex_cancel = thm"Abs_complex_cancel";
  1502 val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff";
  1503 val complex_Re_zero = thm"complex_Re_zero";
  1504 val complex_Im_zero = thm"complex_Im_zero";
  1505 val complex_Re_one = thm"complex_Re_one";
  1506 val complex_Im_one = thm"complex_Im_one";
  1507 val complex_Re_i = thm"complex_Re_i";
  1508 val complex_Im_i = thm"complex_Im_i";
  1509 val Re_complex_of_real_zero = thm"Re_complex_of_real_zero";
  1510 val Im_complex_of_real_zero = thm"Im_complex_of_real_zero";
  1511 val Re_complex_of_real_one = thm"Re_complex_of_real_one";
  1512 val Im_complex_of_real_one = thm"Im_complex_of_real_one";
  1513 val Re_complex_of_real = thm"Re_complex_of_real";
  1514 val Im_complex_of_real = thm"Im_complex_of_real";
  1515 val complex_minus = thm"complex_minus";
  1516 val complex_Re_minus = thm"complex_Re_minus";
  1517 val complex_Im_minus = thm"complex_Im_minus";
  1518 val complex_minus_minus = thm"complex_minus_minus";
  1519 val inj_complex_minus = thm"inj_complex_minus";
  1520 val complex_minus_zero = thm"complex_minus_zero";
  1521 val complex_minus_zero_iff = thm"complex_minus_zero_iff";
  1522 val complex_minus_zero_iff2 = thm"complex_minus_zero_iff2";
  1523 val complex_minus_not_zero_iff = thm"complex_minus_not_zero_iff";
  1524 val complex_add = thm"complex_add";
  1525 val complex_Re_add = thm"complex_Re_add";
  1526 val complex_Im_add = thm"complex_Im_add";
  1527 val complex_add_commute = thm"complex_add_commute";
  1528 val complex_add_assoc = thm"complex_add_assoc";
  1529 val complex_add_left_commute = thm"complex_add_left_commute";
  1530 val complex_add_zero_left = thm"complex_add_zero_left";
  1531 val complex_add_zero_right = thm"complex_add_zero_right";
  1532 val complex_add_minus_right_zero = thm"complex_add_minus_right_zero";
  1533 val complex_add_minus_cancel = thm"complex_add_minus_cancel";
  1534 val complex_minus_add_cancel = thm"complex_minus_add_cancel";
  1535 val complex_add_minus_eq_minus = thm"complex_add_minus_eq_minus";
  1536 val complex_minus_add_distrib = thm"complex_minus_add_distrib";
  1537 val complex_add_left_cancel = thm"complex_add_left_cancel";
  1538 val complex_add_right_cancel = thm"complex_add_right_cancel";
  1539 val complex_eq_minus_iff = thm"complex_eq_minus_iff";
  1540 val complex_eq_minus_iff2 = thm"complex_eq_minus_iff2";
  1541 val complex_diff_0 = thm"complex_diff_0";
  1542 val complex_diff_0_right = thm"complex_diff_0_right";
  1543 val complex_diff_self = thm"complex_diff_self";
  1544 val complex_diff = thm"complex_diff";
  1545 val complex_diff_eq_eq = thm"complex_diff_eq_eq";
  1546 val complex_mult = thm"complex_mult";
  1547 val complex_mult_commute = thm"complex_mult_commute";
  1548 val complex_mult_assoc = thm"complex_mult_assoc";
  1549 val complex_mult_left_commute = thm"complex_mult_left_commute";
  1550 val complex_mult_one_left = thm"complex_mult_one_left";
  1551 val complex_mult_one_right = thm"complex_mult_one_right";
  1552 val complex_mult_zero_left = thm"complex_mult_zero_left";
  1553 val complex_mult_zero_right = thm"complex_mult_zero_right";
  1554 val complex_divide_zero = thm"complex_divide_zero";
  1555 val complex_minus_mult_eq1 = thm"complex_minus_mult_eq1";
  1556 val complex_minus_mult_eq2 = thm"complex_minus_mult_eq2";
  1557 val complex_minus_mult_commute = thm"complex_minus_mult_commute";
  1558 val complex_add_mult_distrib = thm"complex_add_mult_distrib";
  1559 val complex_add_mult_distrib2 = thm"complex_add_mult_distrib2";
  1560 val complex_zero_not_eq_one = thm"complex_zero_not_eq_one";
  1561 val complex_inverse = thm"complex_inverse";
  1562 val COMPLEX_INVERSE_ZERO = thm"COMPLEX_INVERSE_ZERO";
  1563 val COMPLEX_DIVISION_BY_ZERO = thm"COMPLEX_DIVISION_BY_ZERO";
  1564 val complex_mult_inv_left = thm"complex_mult_inv_left";
  1565 val complex_mult_inv_right = thm"complex_mult_inv_right";
  1566 val inj_complex_of_real = thm"inj_complex_of_real";
  1567 val complex_of_real_one = thm"complex_of_real_one";
  1568 val complex_of_real_zero = thm"complex_of_real_zero";
  1569 val complex_of_real_eq_iff = thm"complex_of_real_eq_iff";
  1570 val complex_of_real_minus = thm"complex_of_real_minus";
  1571 val complex_of_real_inverse = thm"complex_of_real_inverse";
  1572 val complex_of_real_add = thm"complex_of_real_add";
  1573 val complex_of_real_diff = thm"complex_of_real_diff";
  1574 val complex_of_real_mult = thm"complex_of_real_mult";
  1575 val complex_of_real_divide = thm"complex_of_real_divide";
  1576 val complex_of_real_pow = thm"complex_of_real_pow";
  1577 val complex_mod = thm"complex_mod";
  1578 val complex_mod_zero = thm"complex_mod_zero";
  1579 val complex_mod_one = thm"complex_mod_one";
  1580 val complex_mod_complex_of_real = thm"complex_mod_complex_of_real";
  1581 val complex_of_real_abs = thm"complex_of_real_abs";
  1582 val complex_cnj = thm"complex_cnj";
  1583 val inj_cnj = thm"inj_cnj";
  1584 val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff";
  1585 val complex_cnj_cnj = thm"complex_cnj_cnj";
  1586 val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real";
  1587 val complex_mod_cnj = thm"complex_mod_cnj";
  1588 val complex_cnj_minus = thm"complex_cnj_minus";
  1589 val complex_cnj_inverse = thm"complex_cnj_inverse";
  1590 val complex_cnj_add = thm"complex_cnj_add";
  1591 val complex_cnj_diff = thm"complex_cnj_diff";
  1592 val complex_cnj_mult = thm"complex_cnj_mult";
  1593 val complex_cnj_divide = thm"complex_cnj_divide";
  1594 val complex_cnj_one = thm"complex_cnj_one";
  1595 val complex_cnj_pow = thm"complex_cnj_pow";
  1596 val complex_add_cnj = thm"complex_add_cnj";
  1597 val complex_diff_cnj = thm"complex_diff_cnj";
  1598 val complex_cnj_zero = thm"complex_cnj_zero";
  1599 val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
  1600 val complex_mult_cnj = thm"complex_mult_cnj";
  1601 val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero";
  1602 val complex_diff_mult_distrib = thm"complex_diff_mult_distrib";
  1603 val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2";
  1604 val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel";
  1605 val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat";
  1606 val complex_mod_minus = thm"complex_mod_minus";
  1607 val complex_mod_mult_cnj = thm"complex_mod_mult_cnj";
  1608 val complex_mod_squared = thm"complex_mod_squared";
  1609 val complex_mod_ge_zero = thm"complex_mod_ge_zero";
  1610 val abs_cmod_cancel = thm"abs_cmod_cancel";
  1611 val complex_mod_mult = thm"complex_mod_mult";
  1612 val complex_mod_add_squared_eq = thm"complex_mod_add_squared_eq";
  1613 val complex_Re_mult_cnj_le_cmod = thm"complex_Re_mult_cnj_le_cmod";
  1614 val complex_Re_mult_cnj_le_cmod2 = thm"complex_Re_mult_cnj_le_cmod2";
  1615 val real_sum_squared_expand = thm"real_sum_squared_expand";
  1616 val complex_mod_triangle_squared = thm"complex_mod_triangle_squared";
  1617 val complex_mod_minus_le_complex_mod = thm"complex_mod_minus_le_complex_mod";
  1618 val complex_mod_triangle_ineq = thm"complex_mod_triangle_ineq";
  1619 val complex_mod_triangle_ineq2 = thm"complex_mod_triangle_ineq2";
  1620 val complex_mod_diff_commute = thm"complex_mod_diff_commute";
  1621 val complex_mod_add_less = thm"complex_mod_add_less";
  1622 val complex_mod_mult_less = thm"complex_mod_mult_less";
  1623 val complex_mod_diff_ineq = thm"complex_mod_diff_ineq";
  1624 val complex_Re_le_cmod = thm"complex_Re_le_cmod";
  1625 val complex_mod_gt_zero = thm"complex_mod_gt_zero";
  1626 val complex_mod_complexpow = thm"complex_mod_complexpow";
  1627 val complexpow_minus = thm"complexpow_minus";
  1628 val complex_mod_inverse = thm"complex_mod_inverse";
  1629 val complex_mod_divide = thm"complex_mod_divide";
  1630 val complex_inverse_divide = thm"complex_inverse_divide";
  1631 val complexpow_i_squared = thm"complexpow_i_squared";
  1632 val complex_i_not_zero = thm"complex_i_not_zero";
  1633 val sgn_zero = thm"sgn_zero";
  1634 val sgn_one = thm"sgn_one";
  1635 val sgn_minus = thm"sgn_minus";
  1636 val sgn_eq = thm"sgn_eq";
  1637 val complex_split = thm"complex_split";
  1638 val Re_complex_i = thm"Re_complex_i";
  1639 val Im_complex_i = thm"Im_complex_i";
  1640 val i_mult_eq = thm"i_mult_eq";
  1641 val i_mult_eq2 = thm"i_mult_eq2";
  1642 val cmod_i = thm"cmod_i";
  1643 val complex_eq_Re_eq = thm"complex_eq_Re_eq";
  1644 val complex_eq_Im_eq = thm"complex_eq_Im_eq";
  1645 val complex_eq_cancel_iff = thm"complex_eq_cancel_iff";
  1646 val complex_eq_cancel_iffA = thm"complex_eq_cancel_iffA";
  1647 val complex_eq_cancel_iffB = thm"complex_eq_cancel_iffB";
  1648 val complex_eq_cancel_iffC = thm"complex_eq_cancel_iffC";
  1649 val complex_eq_cancel_iff2 = thm"complex_eq_cancel_iff2";
  1650 val complex_eq_cancel_iff2a = thm"complex_eq_cancel_iff2a";
  1651 val complex_eq_cancel_iff3 = thm"complex_eq_cancel_iff3";
  1652 val complex_eq_cancel_iff3a = thm"complex_eq_cancel_iff3a";
  1653 val complex_split_Re_zero = thm"complex_split_Re_zero";
  1654 val complex_split_Im_zero = thm"complex_split_Im_zero";
  1655 val Re_sgn = thm"Re_sgn";
  1656 val Im_sgn = thm"Im_sgn";
  1657 val complex_inverse_complex_split = thm"complex_inverse_complex_split";
  1658 val Re_mult_i_eq = thm"Re_mult_i_eq";
  1659 val Im_mult_i_eq = thm"Im_mult_i_eq";
  1660 val complex_mod_mult_i = thm"complex_mod_mult_i";
  1661 val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
  1662 val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
  1663 val complex_split_polar = thm"complex_split_polar";
  1664 val rcis_Ex = thm"rcis_Ex";
  1665 val Re_complex_polar = thm"Re_complex_polar";
  1666 val Re_rcis = thm"Re_rcis";
  1667 val Im_complex_polar = thm"Im_complex_polar";
  1668 val Im_rcis = thm"Im_rcis";
  1669 val complex_mod_complex_polar = thm"complex_mod_complex_polar";
  1670 val complex_mod_rcis = thm"complex_mod_rcis";
  1671 val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
  1672 val complex_Re_cnj = thm"complex_Re_cnj";
  1673 val complex_Im_cnj = thm"complex_Im_cnj";
  1674 val complex_In_mult_cnj_zero = thm"complex_In_mult_cnj_zero";
  1675 val complex_Re_mult = thm"complex_Re_mult";
  1676 val complex_Re_mult_complex_of_real = thm"complex_Re_mult_complex_of_real";
  1677 val complex_Im_mult_complex_of_real = thm"complex_Im_mult_complex_of_real";
  1678 val complex_Re_mult_complex_of_real2 = thm"complex_Re_mult_complex_of_real2";
  1679 val complex_Im_mult_complex_of_real2 = thm"complex_Im_mult_complex_of_real2";
  1680 val cis_rcis_eq = thm"cis_rcis_eq";
  1681 val rcis_mult = thm"rcis_mult";
  1682 val cis_mult = thm"cis_mult";
  1683 val cis_zero = thm"cis_zero";
  1684 val cis_zero2 = thm"cis_zero2";
  1685 val rcis_zero_mod = thm"rcis_zero_mod";
  1686 val rcis_zero_arg = thm"rcis_zero_arg";
  1687 val complex_of_real_minus_one = thm"complex_of_real_minus_one";
  1688 val complex_i_mult_minus = thm"complex_i_mult_minus";
  1689 val complex_i_mult_minus2 = thm"complex_i_mult_minus2";
  1690 val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult";
  1691 val DeMoivre = thm"DeMoivre";
  1692 val DeMoivre2 = thm"DeMoivre2";
  1693 val cis_inverse = thm"cis_inverse";
  1694 val rcis_inverse = thm"rcis_inverse";
  1695 val cis_divide = thm"cis_divide";
  1696 val rcis_divide = thm"rcis_divide";
  1697 val Re_cis = thm"Re_cis";
  1698 val Im_cis = thm"Im_cis";
  1699 val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
  1700 val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
  1701 val expi_Im_split = thm"expi_Im_split";
  1702 val expi_Im_cis = thm"expi_Im_cis";
  1703 val expi_add = thm"expi_add";
  1704 val expi_complex_split = thm"expi_complex_split";
  1705 val expi_zero = thm"expi_zero";
  1706 val complex_Re_mult_eq = thm"complex_Re_mult_eq";
  1707 val complex_Im_mult_eq = thm"complex_Im_mult_eq";
  1708 val complex_expi_Ex = thm"complex_expi_Ex";
  1709 
  1710 val complex_add_ac = thms"complex_add_ac";
  1711 val complex_mult_ac = thms"complex_mult_ac";
  1712 *}
  1713 
  1714 end
  1715 
  1716