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