src/HOL/Complex/Complex.thy
author huffman
Tue May 29 20:31:53 2007 +0200 (2007-05-29)
changeset 23123 e2e370bccde1
parent 22972 3e96b98d37c6
child 23124 892e0a4551da
permissions -rw-r--r--
instance complex :: banach
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
huffman@22655
    11
imports "../Hyperreal/Transcendental"
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
huffman@22968
    70
lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 \<and> y = 0)"
huffman@22968
    71
by (simp add: complex_zero_def)
huffman@22861
    72
paulson@14374
    73
lemma complex_Re_one [simp]: "Re 1 = 1"
paulson@14374
    74
by (simp add: complex_one_def)
paulson@14323
    75
paulson@14374
    76
lemma complex_Im_one [simp]: "Im 1 = 0"
paulson@14373
    77
by (simp add: complex_one_def)
paulson@14323
    78
huffman@22968
    79
lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 \<and> y = 0)"
huffman@22968
    80
by (simp add: complex_one_def)
huffman@22968
    81
paulson@14374
    82
lemma complex_Re_i [simp]: "Re(ii) = 0"
paulson@14373
    83
by (simp add: i_def)
paulson@14323
    84
paulson@14374
    85
lemma complex_Im_i [simp]: "Im(ii) = 1"
paulson@14373
    86
by (simp add: i_def)
paulson@14323
    87
huffman@22968
    88
lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
huffman@22968
    89
by (simp add: i_def)
huffman@22968
    90
paulson@14323
    91
paulson@14374
    92
subsection{*Unary Minus*}
paulson@14323
    93
paulson@14377
    94
lemma complex_minus [simp]: "- (Complex x y) = Complex (-x) (-y)"
paulson@14373
    95
by (simp add: complex_minus_def)
paulson@14323
    96
paulson@14374
    97
lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
paulson@14373
    98
by (simp add: complex_minus_def)
paulson@14323
    99
paulson@14374
   100
lemma complex_Im_minus [simp]: "Im (-z) = - Im z"
paulson@14374
   101
by (simp add: complex_minus_def)
paulson@14323
   102
paulson@14323
   103
paulson@14323
   104
subsection{*Addition*}
paulson@14323
   105
paulson@14377
   106
lemma complex_add [simp]:
paulson@14377
   107
     "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
paulson@14373
   108
by (simp add: complex_add_def)
paulson@14323
   109
paulson@14374
   110
lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)"
paulson@14373
   111
by (simp add: complex_add_def)
paulson@14323
   112
paulson@14374
   113
lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)"
paulson@14373
   114
by (simp add: complex_add_def)
paulson@14323
   115
paulson@14323
   116
lemma complex_add_commute: "(u::complex) + v = v + u"
paulson@14373
   117
by (simp add: complex_add_def add_commute)
paulson@14323
   118
paulson@14323
   119
lemma complex_add_assoc: "((u::complex) + v) + w = u + (v + w)"
paulson@14373
   120
by (simp add: complex_add_def add_assoc)
paulson@14323
   121
paulson@14323
   122
lemma complex_add_zero_left: "(0::complex) + z = z"
paulson@14373
   123
by (simp add: complex_add_def complex_zero_def)
paulson@14323
   124
paulson@14323
   125
lemma complex_add_zero_right: "z + (0::complex) = z"
paulson@14373
   126
by (simp add: complex_add_def complex_zero_def)
paulson@14323
   127
paulson@14373
   128
lemma complex_add_minus_left: "-z + z = (0::complex)"
paulson@14373
   129
by (simp add: complex_add_def complex_minus_def complex_zero_def)
paulson@14323
   130
paulson@14323
   131
lemma complex_diff:
paulson@14373
   132
      "Complex x1 y1 - Complex x2 y2 = Complex (x1-x2) (y1-y2)"
paulson@14373
   133
by (simp add: complex_add_def complex_minus_def complex_diff_def)
paulson@14323
   134
paulson@14374
   135
lemma complex_Re_diff [simp]: "Re(x - y) = Re(x) - Re(y)"
paulson@14374
   136
by (simp add: complex_diff_def)
paulson@14374
   137
paulson@14374
   138
lemma complex_Im_diff [simp]: "Im(x - y) = Im(x) - Im(y)"
paulson@14374
   139
by (simp add: complex_diff_def)
paulson@14374
   140
paulson@14374
   141
paulson@14323
   142
subsection{*Multiplication*}
paulson@14323
   143
paulson@14377
   144
lemma complex_mult [simp]:
paulson@14373
   145
     "Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)"
paulson@14373
   146
by (simp add: complex_mult_def)
paulson@14323
   147
paulson@14323
   148
lemma complex_mult_commute: "(w::complex) * z = z * w"
paulson@14373
   149
by (simp add: complex_mult_def mult_commute add_commute)
paulson@14323
   150
paulson@14323
   151
lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"
paulson@14374
   152
by (simp add: complex_mult_def mult_ac add_ac
paulson@14373
   153
              right_diff_distrib right_distrib left_diff_distrib left_distrib)
paulson@14323
   154
paulson@14323
   155
lemma complex_mult_one_left: "(1::complex) * z = z"
paulson@14373
   156
by (simp add: complex_mult_def complex_one_def)
paulson@14323
   157
paulson@14323
   158
lemma complex_mult_one_right: "z * (1::complex) = z"
paulson@14373
   159
by (simp add: complex_mult_def complex_one_def)
paulson@14323
   160
paulson@14323
   161
paulson@14323
   162
subsection{*Inverse*}
paulson@14323
   163
paulson@14377
   164
lemma complex_inverse [simp]:
huffman@22968
   165
  "inverse (Complex x y) = Complex (x / (x\<twosuperior> + y\<twosuperior>)) (- y / (x\<twosuperior> + y\<twosuperior>))"
paulson@14373
   166
by (simp add: complex_inverse_def)
paulson@14335
   167
paulson@14354
   168
lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
paulson@14374
   169
apply (induct z)
huffman@22968
   170
apply (simp add: power2_eq_square [symmetric] add_divide_distrib [symmetric])
paulson@14323
   171
done
paulson@14323
   172
paulson@14335
   173
paulson@14335
   174
subsection {* The field of complex numbers *}
paulson@14335
   175
paulson@14335
   176
instance complex :: field
paulson@14335
   177
proof
paulson@14335
   178
  fix z u v w :: complex
paulson@14335
   179
  show "(u + v) + w = u + (v + w)"
paulson@14374
   180
    by (rule complex_add_assoc)
paulson@14335
   181
  show "z + w = w + z"
paulson@14374
   182
    by (rule complex_add_commute)
paulson@14335
   183
  show "0 + z = z"
paulson@14374
   184
    by (rule complex_add_zero_left)
paulson@14335
   185
  show "-z + z = 0"
paulson@14374
   186
    by (rule complex_add_minus_left)
paulson@14335
   187
  show "z - w = z + -w"
paulson@14335
   188
    by (simp add: complex_diff_def)
paulson@14335
   189
  show "(u * v) * w = u * (v * w)"
paulson@14374
   190
    by (rule complex_mult_assoc)
paulson@14335
   191
  show "z * w = w * z"
paulson@14374
   192
    by (rule complex_mult_commute)
paulson@14335
   193
  show "1 * z = z"
paulson@14374
   194
    by (rule complex_mult_one_left)
paulson@14341
   195
  show "0 \<noteq> (1::complex)"
paulson@14373
   196
    by (simp add: complex_zero_def complex_one_def)
paulson@14335
   197
  show "(u + v) * w = u * w + v * w"
paulson@14421
   198
    by (simp add: complex_mult_def complex_add_def left_distrib 
paulson@14421
   199
                  diff_minus add_ac)
paulson@14430
   200
  show "z / w = z * inverse w"
paulson@14335
   201
    by (simp add: complex_divide_def)
paulson@14430
   202
  assume "w \<noteq> 0"
paulson@14430
   203
  thus "inverse w * w = 1"
paulson@14430
   204
    by (simp add: complex_mult_inv_left)
paulson@14335
   205
qed
paulson@14335
   206
paulson@14373
   207
instance complex :: division_by_zero
paulson@14373
   208
proof
paulson@14430
   209
  show "inverse 0 = (0::complex)"
paulson@14373
   210
    by (simp add: complex_inverse_def complex_zero_def)
paulson@14373
   211
qed
paulson@14335
   212
paulson@14323
   213
huffman@20556
   214
subsection{*The real algebra of complex numbers*}
huffman@20556
   215
huffman@20556
   216
instance complex :: scaleR ..
huffman@20556
   217
huffman@20556
   218
defs (overloaded)
huffman@20556
   219
  complex_scaleR_def: "r *# x == Complex r 0 * x"
huffman@20556
   220
huffman@22972
   221
lemma Re_scaleR [simp]: "Re (scaleR r x) = r * Re x"
huffman@22972
   222
unfolding complex_scaleR_def by (induct x, simp)
huffman@22972
   223
huffman@22972
   224
lemma Im_scaleR [simp]: "Im (scaleR r x) = r * Im x"
huffman@22972
   225
unfolding complex_scaleR_def by (induct x, simp)
huffman@22972
   226
huffman@20725
   227
instance complex :: real_field
huffman@20556
   228
proof
huffman@20556
   229
  fix a b :: real
huffman@20556
   230
  fix x y :: complex
huffman@20556
   231
  show "a *# (x + y) = a *# x + a *# y"
huffman@20556
   232
    by (simp add: complex_scaleR_def right_distrib)
huffman@20556
   233
  show "(a + b) *# x = a *# x + b *# x"
huffman@20556
   234
    by (simp add: complex_scaleR_def left_distrib [symmetric])
huffman@20763
   235
  show "a *# b *# x = (a * b) *# x"
huffman@20556
   236
    by (simp add: complex_scaleR_def mult_assoc [symmetric])
huffman@20556
   237
  show "1 *# x = x"
huffman@20556
   238
    by (simp add: complex_scaleR_def complex_one_def [symmetric])
huffman@20556
   239
  show "a *# x * y = a *# (x * y)"
huffman@20556
   240
    by (simp add: complex_scaleR_def mult_assoc)
huffman@20556
   241
  show "x * a *# y = a *# (x * y)"
huffman@20556
   242
    by (simp add: complex_scaleR_def mult_left_commute)
huffman@20556
   243
qed
huffman@20556
   244
huffman@20556
   245
paulson@14323
   246
subsection{*Embedding Properties for @{term complex_of_real} Map*}
paulson@14323
   247
huffman@20557
   248
abbreviation
wenzelm@21404
   249
  complex_of_real :: "real => complex" where
huffman@20557
   250
  "complex_of_real == of_real"
huffman@20557
   251
huffman@20557
   252
lemma complex_of_real_def: "complex_of_real r = Complex r 0"
huffman@20557
   253
by (simp add: of_real_def complex_scaleR_def)
huffman@20557
   254
huffman@20557
   255
lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z"
huffman@20557
   256
by (simp add: complex_of_real_def)
huffman@20557
   257
huffman@20557
   258
lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
huffman@20557
   259
by (simp add: complex_of_real_def)
huffman@20557
   260
paulson@14377
   261
lemma Complex_add_complex_of_real [simp]:
paulson@14377
   262
     "Complex x y + complex_of_real r = Complex (x+r) y"
paulson@14377
   263
by (simp add: complex_of_real_def)
paulson@14377
   264
paulson@14377
   265
lemma complex_of_real_add_Complex [simp]:
paulson@14377
   266
     "complex_of_real r + Complex x y = Complex (r+x) y"
paulson@14377
   267
by (simp add: i_def complex_of_real_def)
paulson@14377
   268
paulson@14377
   269
lemma Complex_mult_complex_of_real:
paulson@14377
   270
     "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
paulson@14377
   271
by (simp add: complex_of_real_def)
paulson@14377
   272
paulson@14377
   273
lemma complex_of_real_mult_Complex:
paulson@14377
   274
     "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
paulson@14377
   275
by (simp add: i_def complex_of_real_def)
paulson@14377
   276
paulson@14377
   277
lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
paulson@14377
   278
by (simp add: i_def complex_of_real_def)
paulson@14377
   279
paulson@14377
   280
lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r"
paulson@14377
   281
by (simp add: i_def complex_of_real_def)
paulson@14377
   282
paulson@14323
   283
paulson@14377
   284
subsection{*The Functions @{term Re} and @{term Im}*}
paulson@14377
   285
paulson@14377
   286
lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
huffman@20725
   287
by (induct z, induct w, simp)
paulson@14377
   288
paulson@14377
   289
lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z"
huffman@20725
   290
by (induct z, induct w, simp)
paulson@14377
   291
paulson@14377
   292
lemma Re_i_times [simp]: "Re(ii * z) = - Im z"
huffman@20725
   293
by (simp add: complex_Re_mult_eq)
paulson@14377
   294
paulson@14377
   295
lemma Re_times_i [simp]: "Re(z * ii) = - Im z"
huffman@20725
   296
by (simp add: complex_Re_mult_eq)
paulson@14377
   297
paulson@14377
   298
lemma Im_i_times [simp]: "Im(ii * z) = Re z"
huffman@20725
   299
by (simp add: complex_Im_mult_eq)
paulson@14377
   300
paulson@14377
   301
lemma Im_times_i [simp]: "Im(z * ii) = Re z"
huffman@20725
   302
by (simp add: complex_Im_mult_eq)
paulson@14377
   303
paulson@14377
   304
lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
paulson@14377
   305
by (simp add: complex_Re_mult_eq)
paulson@14377
   306
paulson@14377
   307
lemma complex_Re_mult_complex_of_real [simp]:
paulson@14377
   308
     "Re (z * complex_of_real c) = Re(z) * c"
paulson@14377
   309
by (simp add: complex_Re_mult_eq)
paulson@14377
   310
paulson@14377
   311
lemma complex_Im_mult_complex_of_real [simp]:
paulson@14377
   312
     "Im (z * complex_of_real c) = Im(z) * c"
paulson@14377
   313
by (simp add: complex_Im_mult_eq)
paulson@14377
   314
paulson@14377
   315
lemma complex_Re_mult_complex_of_real2 [simp]:
paulson@14377
   316
     "Re (complex_of_real c * z) = c * Re(z)"
paulson@14377
   317
by (simp add: complex_Re_mult_eq)
paulson@14377
   318
paulson@14377
   319
lemma complex_Im_mult_complex_of_real2 [simp]:
paulson@14377
   320
     "Im (complex_of_real c * z) = c * Im(z)"
paulson@14377
   321
by (simp add: complex_Im_mult_eq)
huffman@20557
   322
paulson@14377
   323
paulson@14323
   324
subsection{*Conjugation is an Automorphism*}
paulson@14323
   325
huffman@20557
   326
definition
wenzelm@21404
   327
  cnj :: "complex => complex" where
huffman@20557
   328
  "cnj z = Complex (Re z) (-Im z)"
huffman@20557
   329
paulson@14373
   330
lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
paulson@14373
   331
by (simp add: cnj_def)
paulson@14323
   332
paulson@14374
   333
lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
paulson@14373
   334
by (simp add: cnj_def complex_Re_Im_cancel_iff)
paulson@14323
   335
paulson@14374
   336
lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
paulson@14373
   337
by (simp add: cnj_def)
paulson@14323
   338
paulson@14374
   339
lemma complex_cnj_complex_of_real [simp]:
paulson@14373
   340
     "cnj (complex_of_real x) = complex_of_real x"
paulson@14373
   341
by (simp add: complex_of_real_def complex_cnj)
paulson@14323
   342
paulson@14323
   343
lemma complex_cnj_minus: "cnj (-z) = - cnj z"
huffman@20725
   344
by (simp add: cnj_def)
paulson@14323
   345
paulson@14323
   346
lemma complex_cnj_inverse: "cnj(inverse z) = inverse(cnj z)"
huffman@20725
   347
by (induct z, simp add: complex_cnj power2_eq_square)
paulson@14323
   348
paulson@14323
   349
lemma complex_cnj_add: "cnj(w + z) = cnj(w) + cnj(z)"
huffman@20725
   350
by (induct w, induct z, simp add: complex_cnj)
paulson@14323
   351
paulson@14323
   352
lemma complex_cnj_diff: "cnj(w - z) = cnj(w) - cnj(z)"
paulson@15013
   353
by (simp add: diff_minus complex_cnj_add complex_cnj_minus)
paulson@14323
   354
paulson@14323
   355
lemma complex_cnj_mult: "cnj(w * z) = cnj(w) * cnj(z)"
huffman@20725
   356
by (induct w, induct z, simp add: complex_cnj)
paulson@14323
   357
paulson@14323
   358
lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)"
paulson@14373
   359
by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse)
paulson@14323
   360
paulson@14374
   361
lemma complex_cnj_one [simp]: "cnj 1 = 1"
paulson@14373
   362
by (simp add: cnj_def complex_one_def)
paulson@14323
   363
paulson@14323
   364
lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
huffman@20725
   365
by (induct z, simp add: complex_cnj complex_of_real_def)
paulson@14323
   366
paulson@14323
   367
lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
paulson@14373
   368
apply (induct z)
paulson@15013
   369
apply (simp add: complex_add complex_cnj complex_of_real_def diff_minus
paulson@14354
   370
                 complex_minus i_def complex_mult)
paulson@14323
   371
done
paulson@14323
   372
paulson@14354
   373
lemma complex_cnj_zero [simp]: "cnj 0 = 0"
paulson@14334
   374
by (simp add: cnj_def complex_zero_def)
paulson@14323
   375
paulson@14374
   376
lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
paulson@14373
   377
by (induct z, simp add: complex_zero_def complex_cnj)
paulson@14323
   378
paulson@14323
   379
lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
huffman@20725
   380
by (induct z, simp add: complex_cnj complex_of_real_def power2_eq_square)
paulson@14323
   381
paulson@14323
   382
paulson@14323
   383
subsection{*Modulus*}
paulson@14323
   384
huffman@22861
   385
instance complex :: norm
huffman@22861
   386
  complex_norm_def: "norm z \<equiv> sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)" ..
huffman@20557
   387
huffman@20557
   388
abbreviation
huffman@22861
   389
  cmod :: "complex \<Rightarrow> real" where
huffman@22861
   390
  "cmod \<equiv> norm"
huffman@20557
   391
huffman@20557
   392
lemmas cmod_def = complex_norm_def
huffman@20557
   393
huffman@22861
   394
lemma complex_mod [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
paulson@14373
   395
by (simp add: cmod_def)
paulson@14323
   396
huffman@22861
   397
lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod x + cmod y"
huffman@22861
   398
apply (simp add: cmod_def)
huffman@22861
   399
apply (rule real_sqrt_sum_squares_triangle_ineq)
paulson@14323
   400
done
paulson@14323
   401
huffman@22861
   402
lemma complex_mod_mult: "cmod (x * y) = cmod x * cmod y"
paulson@14373
   403
apply (induct x, induct y)
huffman@22861
   404
apply (simp add: real_sqrt_mult_distrib [symmetric])
huffman@22861
   405
apply (simp add: power2_sum power2_diff power_mult_distrib ring_distrib)
paulson@14323
   406
done
paulson@14323
   407
huffman@22861
   408
lemma complex_mod_complex_of_real: "cmod (complex_of_real x) = \<bar>x\<bar>"
huffman@22861
   409
by (simp add: complex_of_real_def)
paulson@14323
   410
huffman@22852
   411
lemma complex_norm_scaleR:
huffman@22852
   412
  "norm (scaleR a x) = \<bar>a\<bar> * norm (x::complex)"
huffman@22861
   413
unfolding scaleR_conv_of_real
huffman@22861
   414
by (simp only: complex_mod_mult complex_mod_complex_of_real)
huffman@22852
   415
huffman@20725
   416
instance complex :: real_normed_field
huffman@20557
   417
proof
huffman@20557
   418
  fix r :: real
huffman@20557
   419
  fix x y :: complex
huffman@20557
   420
  show "0 \<le> cmod x"
huffman@22861
   421
    by (induct x) simp
huffman@20557
   422
  show "(cmod x = 0) = (x = 0)"
huffman@22861
   423
    by (induct x) simp
huffman@20557
   424
  show "cmod (x + y) \<le> cmod x + cmod y"
huffman@20557
   425
    by (rule complex_mod_triangle_ineq)
huffman@22852
   426
  show "cmod (scaleR r x) = \<bar>r\<bar> * cmod x"
huffman@22852
   427
    by (rule complex_norm_scaleR)
huffman@20557
   428
  show "cmod (x * y) = cmod x * cmod y"
huffman@20557
   429
    by (rule complex_mod_mult)
huffman@20557
   430
qed
huffman@20557
   431
huffman@22861
   432
lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
huffman@22861
   433
by (induct z, simp add: complex_cnj)
huffman@22861
   434
huffman@22861
   435
lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
huffman@22861
   436
by (simp add: complex_mod_mult power2_eq_square)
huffman@22861
   437
huffman@22861
   438
lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
huffman@22861
   439
by simp
paulson@14323
   440
huffman@22861
   441
lemma cmod_complex_polar [simp]:
huffman@22861
   442
     "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
huffman@22861
   443
apply (simp only: cmod_unit_one complex_mod_mult)
huffman@22861
   444
apply (simp add: complex_mod_complex_of_real)
huffman@22861
   445
done
huffman@22861
   446
huffman@22861
   447
lemma complex_Re_le_cmod: "Re x \<le> cmod x"
huffman@22861
   448
unfolding complex_norm_def
huffman@22861
   449
by (rule real_sqrt_sum_squares_ge1)
huffman@22861
   450
huffman@22861
   451
lemma complex_mod_minus_le_complex_mod [simp]: "- cmod x \<le> cmod x"
huffman@22861
   452
by (rule order_trans [OF _ norm_ge_zero], simp)
huffman@22861
   453
huffman@22861
   454
lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
huffman@22861
   455
by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
paulson@14323
   456
huffman@22861
   457
lemmas real_sum_squared_expand = power2_sum [where 'a=real]
paulson@14323
   458
paulson@14354
   459
huffman@23123
   460
subsection {* Completeness of the Complexes *}
huffman@23123
   461
huffman@23123
   462
interpretation Re: bounded_linear ["Re"]
huffman@23123
   463
apply (unfold_locales, simp, simp)
huffman@23123
   464
apply (rule_tac x=1 in exI)
huffman@23123
   465
apply (simp add: complex_norm_def)
huffman@23123
   466
done
huffman@23123
   467
huffman@23123
   468
interpretation Im: bounded_linear ["Im"]
huffman@23123
   469
apply (unfold_locales, simp, simp)
huffman@23123
   470
apply (rule_tac x=1 in exI)
huffman@23123
   471
apply (simp add: complex_norm_def)
huffman@23123
   472
done
huffman@23123
   473
huffman@23123
   474
lemma LIMSEQ_Complex:
huffman@23123
   475
  "\<lbrakk>X ----> a; Y ----> b\<rbrakk> \<Longrightarrow> (\<lambda>n. Complex (X n) (Y n)) ----> Complex a b"
huffman@23123
   476
apply (rule LIMSEQ_I)
huffman@23123
   477
apply (subgoal_tac "0 < r / sqrt 2")
huffman@23123
   478
apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
huffman@23123
   479
apply (drule_tac r="r / sqrt 2" in LIMSEQ_D, safe)
huffman@23123
   480
apply (rename_tac M N, rule_tac x="max M N" in exI, safe)
huffman@23123
   481
apply (simp add: complex_diff)
huffman@23123
   482
apply (simp add: real_sqrt_sum_squares_less)
huffman@23123
   483
apply (simp add: divide_pos_pos)
huffman@23123
   484
done
huffman@23123
   485
huffman@23123
   486
instance complex :: banach
huffman@23123
   487
proof
huffman@23123
   488
  fix X :: "nat \<Rightarrow> complex"
huffman@23123
   489
  assume X: "Cauchy X"
huffman@23123
   490
  from Re.Cauchy [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
huffman@23123
   491
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
huffman@23123
   492
  from Im.Cauchy [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
huffman@23123
   493
    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
huffman@23123
   494
  have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
huffman@23123
   495
    using LIMSEQ_Complex [OF 1 2] by simp
huffman@23123
   496
  thus "convergent X"
huffman@23123
   497
    by (rule convergentI)
huffman@23123
   498
qed
huffman@23123
   499
huffman@23123
   500
paulson@14354
   501
subsection{*Exponentiation*}
paulson@14354
   502
paulson@14354
   503
primrec
paulson@14354
   504
     complexpow_0:   "z ^ 0       = 1"
paulson@14354
   505
     complexpow_Suc: "z ^ (Suc n) = (z::complex) * (z ^ n)"
paulson@14354
   506
paulson@14354
   507
paulson@15003
   508
instance complex :: recpower
paulson@14354
   509
proof
paulson@14354
   510
  fix z :: complex
paulson@14354
   511
  fix n :: nat
paulson@14354
   512
  show "z^0 = 1" by simp
paulson@14354
   513
  show "z^(Suc n) = z * (z^n)" by simp
paulson@14354
   514
qed
paulson@14323
   515
paulson@14354
   516
lemma complex_cnj_pow: "cnj(z ^ n) = cnj(z) ^ n"
paulson@14323
   517
apply (induct_tac "n")
paulson@14354
   518
apply (auto simp add: complex_cnj_mult)
paulson@14323
   519
done
paulson@14323
   520
paulson@14354
   521
lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
huffman@20725
   522
by (simp add: i_def complex_one_def numeral_2_eq_2)
paulson@14354
   523
paulson@14354
   524
lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
paulson@14373
   525
by (simp add: i_def complex_zero_def)
paulson@14354
   526
paulson@14354
   527
huffman@22972
   528
subsection{*The Functions @{term sgn} and @{term arg}*}
paulson@14323
   529
huffman@22972
   530
text {*------------ Argand -------------*}
huffman@20557
   531
wenzelm@21404
   532
definition
wenzelm@21404
   533
  arg :: "complex => real" where
huffman@20557
   534
  "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
huffman@20557
   535
paulson@14374
   536
lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
huffman@22972
   537
by (simp add: sgn_def divide_inverse scaleR_conv_of_real mult_commute)
paulson@14323
   538
paulson@14323
   539
lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
huffman@20725
   540
by (simp add: i_def complex_of_real_def)
paulson@14323
   541
paulson@14374
   542
lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
huffman@20725
   543
by (simp add: i_def complex_one_def)
paulson@14323
   544
paulson@14374
   545
lemma complex_eq_cancel_iff2 [simp]:
paulson@14377
   546
     "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
paulson@14377
   547
by (simp add: complex_of_real_def)
paulson@14323
   548
paulson@14374
   549
lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
huffman@22972
   550
unfolding sgn_def by (simp add: divide_inverse)
paulson@14323
   551
paulson@14374
   552
lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
huffman@22972
   553
unfolding sgn_def by (simp add: divide_inverse)
paulson@14323
   554
paulson@14323
   555
lemma complex_inverse_complex_split:
paulson@14323
   556
     "inverse(complex_of_real x + ii * complex_of_real y) =
paulson@14323
   557
      complex_of_real(x/(x ^ 2 + y ^ 2)) -
paulson@14323
   558
      ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
huffman@20725
   559
by (simp add: complex_of_real_def i_def diff_minus divide_inverse)
paulson@14323
   560
paulson@14323
   561
(*----------------------------------------------------------------------------*)
paulson@14323
   562
(* Many of the theorems below need to be moved elsewhere e.g. Transc. Also *)
paulson@14323
   563
(* many of the theorems are not used - so should they be kept?                *)
paulson@14323
   564
(*----------------------------------------------------------------------------*)
paulson@14323
   565
paulson@14354
   566
lemma cos_arg_i_mult_zero_pos:
paulson@14377
   567
   "0 < y ==> cos (arg(Complex 0 y)) = 0"
paulson@14373
   568
apply (simp add: arg_def abs_if)
paulson@14334
   569
apply (rule_tac a = "pi/2" in someI2, auto)
paulson@14334
   570
apply (rule order_less_trans [of _ 0], auto)
paulson@14323
   571
done
paulson@14323
   572
paulson@14354
   573
lemma cos_arg_i_mult_zero_neg:
paulson@14377
   574
   "y < 0 ==> cos (arg(Complex 0 y)) = 0"
paulson@14373
   575
apply (simp add: arg_def abs_if)
paulson@14334
   576
apply (rule_tac a = "- pi/2" in someI2, auto)
paulson@14334
   577
apply (rule order_trans [of _ 0], auto)
paulson@14323
   578
done
paulson@14323
   579
paulson@14374
   580
lemma cos_arg_i_mult_zero [simp]:
paulson@14377
   581
     "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
paulson@14377
   582
by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
paulson@14323
   583
paulson@14323
   584
paulson@14323
   585
subsection{*Finally! Polar Form for Complex Numbers*}
paulson@14323
   586
huffman@20557
   587
definition
huffman@20557
   588
huffman@20557
   589
  (* abbreviation for (cos a + i sin a) *)
wenzelm@21404
   590
  cis :: "real => complex" where
huffman@20557
   591
  "cis a = Complex (cos a) (sin a)"
huffman@20557
   592
wenzelm@21404
   593
definition
huffman@20557
   594
  (* abbreviation for r*(cos a + i sin a) *)
wenzelm@21404
   595
  rcis :: "[real, real] => complex" where
huffman@20557
   596
  "rcis r a = complex_of_real r * cis a"
huffman@20557
   597
wenzelm@21404
   598
definition
huffman@20557
   599
  (* e ^ (x + iy) *)
wenzelm@21404
   600
  expi :: "complex => complex" where
huffman@20557
   601
  "expi z = complex_of_real(exp (Re z)) * cis (Im z)"
huffman@20557
   602
paulson@14374
   603
lemma complex_split_polar:
paulson@14377
   604
     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
huffman@20725
   605
apply (induct z)
paulson@14377
   606
apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
paulson@14323
   607
done
paulson@14323
   608
paulson@14354
   609
lemma rcis_Ex: "\<exists>r a. z = rcis r a"
huffman@20725
   610
apply (induct z)
paulson@14377
   611
apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
paulson@14323
   612
done
paulson@14323
   613
paulson@14374
   614
lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
paulson@14373
   615
by (simp add: rcis_def cis_def)
paulson@14323
   616
paulson@14348
   617
lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
paulson@14373
   618
by (simp add: rcis_def cis_def)
paulson@14323
   619
paulson@14377
   620
lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
paulson@14377
   621
proof -
paulson@14377
   622
  have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
huffman@20725
   623
    by (simp only: power_mult_distrib right_distrib)
paulson@14377
   624
  thus ?thesis by simp
paulson@14377
   625
qed
paulson@14323
   626
paulson@14374
   627
lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
paulson@14377
   628
by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
paulson@14323
   629
paulson@14323
   630
lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
paulson@14373
   631
apply (simp add: cmod_def)
huffman@22956
   632
apply (simp add: complex_mult_cnj del: of_real_add)
paulson@14323
   633
done
paulson@14323
   634
paulson@14374
   635
lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z"
paulson@14373
   636
by (induct z, simp add: complex_cnj)
paulson@14323
   637
paulson@14374
   638
lemma complex_Im_cnj [simp]: "Im(cnj z) = - Im z"
paulson@14374
   639
by (induct z, simp add: complex_cnj)
paulson@14374
   640
paulson@14374
   641
lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
paulson@14373
   642
by (induct z, simp add: complex_cnj complex_mult)
paulson@14323
   643
paulson@14323
   644
paulson@14323
   645
(*---------------------------------------------------------------------------*)
paulson@14323
   646
(*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
paulson@14323
   647
(*---------------------------------------------------------------------------*)
paulson@14323
   648
paulson@14323
   649
lemma cis_rcis_eq: "cis a = rcis 1 a"
paulson@14373
   650
by (simp add: rcis_def)
paulson@14323
   651
paulson@14374
   652
lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
paulson@15013
   653
by (simp add: rcis_def cis_def cos_add sin_add right_distrib right_diff_distrib
paulson@15013
   654
              complex_of_real_def)
paulson@14323
   655
paulson@14323
   656
lemma cis_mult: "cis a * cis b = cis (a + b)"
paulson@14373
   657
by (simp add: cis_rcis_eq rcis_mult)
paulson@14323
   658
paulson@14374
   659
lemma cis_zero [simp]: "cis 0 = 1"
paulson@14377
   660
by (simp add: cis_def complex_one_def)
paulson@14323
   661
paulson@14374
   662
lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
paulson@14373
   663
by (simp add: rcis_def)
paulson@14323
   664
paulson@14374
   665
lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
paulson@14373
   666
by (simp add: rcis_def)
paulson@14323
   667
paulson@14323
   668
lemma complex_of_real_minus_one:
paulson@14323
   669
   "complex_of_real (-(1::real)) = -(1::complex)"
huffman@20725
   670
by (simp add: complex_of_real_def complex_one_def)
paulson@14323
   671
paulson@14374
   672
lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
paulson@14373
   673
by (simp add: complex_mult_assoc [symmetric])
paulson@14323
   674
paulson@14323
   675
paulson@14323
   676
lemma cis_real_of_nat_Suc_mult:
paulson@14323
   677
   "cis (real (Suc n) * a) = cis a * cis (real n * a)"
paulson@14377
   678
by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib)
paulson@14323
   679
paulson@14323
   680
lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
paulson@14323
   681
apply (induct_tac "n")
paulson@14323
   682
apply (auto simp add: cis_real_of_nat_Suc_mult)
paulson@14323
   683
done
paulson@14323
   684
paulson@14374
   685
lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
huffman@22890
   686
by (simp add: rcis_def power_mult_distrib DeMoivre)
paulson@14323
   687
paulson@14374
   688
lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
huffman@20725
   689
by (simp add: cis_def complex_inverse_complex_split diff_minus)
paulson@14323
   690
paulson@14323
   691
lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
huffman@22884
   692
by (simp add: divide_inverse rcis_def)
paulson@14323
   693
paulson@14323
   694
lemma cis_divide: "cis a / cis b = cis (a - b)"
paulson@14373
   695
by (simp add: complex_divide_def cis_mult real_diff_def)
paulson@14323
   696
paulson@14354
   697
lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
paulson@14373
   698
apply (simp add: complex_divide_def)
paulson@14373
   699
apply (case_tac "r2=0", simp)
paulson@14373
   700
apply (simp add: rcis_inverse rcis_mult real_diff_def)
paulson@14323
   701
done
paulson@14323
   702
paulson@14374
   703
lemma Re_cis [simp]: "Re(cis a) = cos a"
paulson@14373
   704
by (simp add: cis_def)
paulson@14323
   705
paulson@14374
   706
lemma Im_cis [simp]: "Im(cis a) = sin a"
paulson@14373
   707
by (simp add: cis_def)
paulson@14323
   708
paulson@14323
   709
lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
paulson@14334
   710
by (auto simp add: DeMoivre)
paulson@14323
   711
paulson@14323
   712
lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
paulson@14334
   713
by (auto simp add: DeMoivre)
paulson@14323
   714
paulson@14323
   715
lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
huffman@20725
   716
by (simp add: expi_def exp_add cis_mult [symmetric] mult_ac)
paulson@14323
   717
paulson@14374
   718
lemma expi_zero [simp]: "expi (0::complex) = 1"
paulson@14373
   719
by (simp add: expi_def)
paulson@14323
   720
paulson@14374
   721
lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
paulson@14373
   722
apply (insert rcis_Ex [of z])
huffman@22884
   723
apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric])
paulson@14334
   724
apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
paulson@14323
   725
done
paulson@14323
   726
paulson@14323
   727
paulson@14387
   728
subsection{*Numerals and Arithmetic*}
paulson@14387
   729
paulson@14387
   730
instance complex :: number ..
paulson@14387
   731
paulson@15013
   732
defs (overloaded)
haftmann@20485
   733
  complex_number_of_def: "(number_of w :: complex) == of_int w"
paulson@15013
   734
    --{*the type constraint is essential!*}
paulson@14387
   735
paulson@14387
   736
instance complex :: number_ring
huffman@20725
   737
by (intro_classes, simp add: complex_number_of_def)
paulson@15013
   738
huffman@22914
   739
lemma complex_number_of: "complex_of_real (number_of w) = number_of w"
huffman@20557
   740
by (rule of_real_number_of_eq)
paulson@14387
   741
paulson@14387
   742
lemma complex_number_of_cnj [simp]: "cnj(number_of v :: complex) = number_of v"
paulson@15481
   743
by (simp only: complex_number_of [symmetric] complex_cnj_complex_of_real)
paulson@14387
   744
paulson@14387
   745
lemma complex_number_of_cmod: 
paulson@14387
   746
      "cmod(number_of v :: complex) = abs (number_of v :: real)"
paulson@14387
   747
by (simp only: complex_number_of [symmetric] complex_mod_complex_of_real)
paulson@14387
   748
paulson@14387
   749
lemma complex_number_of_Re [simp]: "Re(number_of v :: complex) = number_of v"
paulson@14387
   750
by (simp only: complex_number_of [symmetric] Re_complex_of_real)
paulson@14387
   751
paulson@14387
   752
lemma complex_number_of_Im [simp]: "Im(number_of v :: complex) = 0"
paulson@14387
   753
by (simp only: complex_number_of [symmetric] Im_complex_of_real)
paulson@14387
   754
paulson@14387
   755
lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
paulson@14387
   756
by (simp add: expi_def complex_Re_mult_eq complex_Im_mult_eq cis_def)
paulson@14387
   757
paulson@14387
   758
paulson@14387
   759
(*examples:
paulson@14387
   760
print_depth 22
paulson@14387
   761
set timing;
paulson@14387
   762
set trace_simp;
paulson@14387
   763
fun test s = (Goal s, by (Simp_tac 1)); 
paulson@14387
   764
paulson@14387
   765
test "23 * ii + 45 * ii= (x::complex)";
paulson@14387
   766
paulson@14387
   767
test "5 * ii + 12 - 45 * ii= (x::complex)";
paulson@14387
   768
test "5 * ii + 40 - 12 * ii + 9 = (x::complex) + 89 * ii";
paulson@14387
   769
test "5 * ii + 40 - 12 * ii + 9 - 78 = (x::complex) + 89 * ii";
paulson@14387
   770
paulson@14387
   771
test "l + 10 * ii + 90 + 3*l +  9 + 45 * ii= (x::complex)";
paulson@14387
   772
test "87 + 10 * ii + 90 + 3*7 +  9 + 45 * ii= (x::complex)";
paulson@14387
   773
paulson@14387
   774
paulson@14387
   775
fun test s = (Goal s; by (Asm_simp_tac 1)); 
paulson@14387
   776
paulson@14387
   777
test "x*k = k*(y::complex)";
paulson@14387
   778
test "k = k*(y::complex)"; 
paulson@14387
   779
test "a*(b*c) = (b::complex)";
paulson@14387
   780
test "a*(b*c) = d*(b::complex)*(x*a)";
paulson@14387
   781
paulson@14387
   782
paulson@14387
   783
test "(x*k) / (k*(y::complex)) = (uu::complex)";
paulson@14387
   784
test "(k) / (k*(y::complex)) = (uu::complex)"; 
paulson@14387
   785
test "(a*(b*c)) / ((b::complex)) = (uu::complex)";
paulson@14387
   786
test "(a*(b*c)) / (d*(b::complex)*(x*a)) = (uu::complex)";
paulson@14387
   787
paulson@15003
   788
FIXME: what do we do about this?
paulson@14387
   789
test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z";
paulson@14387
   790
*)
paulson@14387
   791
paulson@13957
   792
end