src/HOL/Complex/Complex.thy
 changeset 14374 61de62096768 parent 14373 67a628beb981 child 14377 f454b3004f8f
```     1.1 --- a/src/HOL/Complex/Complex.thy	Tue Feb 03 11:06:36 2004 +0100
1.2 +++ b/src/HOL/Complex/Complex.thy	Tue Feb 03 15:58:31 2004 +0100
1.3 @@ -79,7 +79,7 @@
1.4    complex_diff_def:
1.5      "z - w == z + - (w::complex)"
1.6
1.7 -  complex_mult_def:
1.8 +  complex_mult_def:
1.9      "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)"
1.10
1.11    complex_divide_def: "w / (z::complex) == w * inverse z"
1.12 @@ -103,83 +103,50 @@
1.13  lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
1.14    by (induct z, induct w) simp
1.15
1.16 -lemma Re: "Re(Complex x y) = x"
1.17 +lemma Re [simp]: "Re(Complex x y) = x"
1.18  by simp
1.19 -declare Re [simp]
1.20
1.21 -lemma Im: "Im(Complex x y) = y"
1.22 +lemma Im [simp]: "Im(Complex x y) = y"
1.23  by simp
1.24 -declare Im [simp]
1.25
1.26  lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))"
1.27  by (induct w, induct z, simp)
1.28
1.29 -lemma complex_Re_zero: "Re 0 = 0"
1.30 +lemma complex_Re_zero [simp]: "Re 0 = 0"
1.32 +
1.33 +lemma complex_Im_zero [simp]: "Im 0 = 0"
1.35
1.36 -lemma complex_Im_zero: "Im 0 = 0"
1.38 -declare complex_Re_zero [simp] complex_Im_zero [simp]
1.39 +lemma complex_Re_one [simp]: "Re 1 = 1"
1.41
1.42 -lemma complex_Re_one: "Re 1 = 1"
1.44 -declare complex_Re_one [simp]
1.45 -
1.46 -lemma complex_Im_one: "Im 1 = 0"
1.47 +lemma complex_Im_one [simp]: "Im 1 = 0"
1.49 -declare complex_Im_one [simp]
1.50
1.51 -lemma complex_Re_i: "Re(ii) = 0"
1.52 +lemma complex_Re_i [simp]: "Re(ii) = 0"
1.54 -declare complex_Re_i [simp]
1.55
1.56 -lemma complex_Im_i: "Im(ii) = 1"
1.57 +lemma complex_Im_i [simp]: "Im(ii) = 1"
1.59 -declare complex_Im_i [simp]
1.60
1.61 -lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0"
1.62 +lemma Re_complex_of_real [simp]: "Re(complex_of_real z) = z"
1.64 -declare Re_complex_of_real_zero [simp]
1.65
1.66 -lemma Im_complex_of_real_zero: "Im(complex_of_real 0) = 0"
1.68 -declare Im_complex_of_real_zero [simp]
1.69 -
1.70 -lemma Re_complex_of_real_one: "Re(complex_of_real 1) = 1"
1.71 +lemma Im_complex_of_real [simp]: "Im(complex_of_real z) = 0"
1.73 -declare Re_complex_of_real_one [simp]
1.74 -
1.75 -lemma Im_complex_of_real_one: "Im(complex_of_real 1) = 0"
1.77 -declare Im_complex_of_real_one [simp]
1.78 -
1.79 -lemma Re_complex_of_real: "Re(complex_of_real z) = z"
1.81 -declare Re_complex_of_real [simp]
1.82 -
1.83 -lemma Im_complex_of_real: "Im(complex_of_real z) = 0"
1.85 -declare Im_complex_of_real [simp]
1.86
1.87
1.88 -subsection{*Negation*}
1.89 +subsection{*Unary Minus*}
1.90
1.91  lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)"
1.93
1.94 -lemma complex_Re_minus: "Re (-z) = - Re z"
1.96 -
1.97 -lemma complex_Im_minus: "Im (-z) = - Im z"
1.98 +lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
1.100
1.101 -lemma complex_minus_zero: "-(0::complex) = 0"
1.102 -by (simp add: complex_minus_def complex_zero_def)
1.103 -declare complex_minus_zero [simp]
1.104 -
1.105 -lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))"
1.106 -by (induct x, simp add: complex_minus_def complex_zero_def)
1.107 -declare complex_minus_zero_iff [simp]
1.108 +lemma complex_Im_minus [simp]: "Im (-z) = - Im z"
1.110
1.111
1.113 @@ -187,10 +154,10 @@
1.114  lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
1.116
1.117 -lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)"
1.118 +lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)"
1.120
1.121 -lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)"
1.122 +lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)"
1.124
1.125  lemma complex_add_commute: "(u::complex) + v = v + u"
1.126 @@ -212,6 +179,13 @@
1.127        "Complex x1 y1 - Complex x2 y2 = Complex (x1-x2) (y1-y2)"
1.129
1.130 +lemma complex_Re_diff [simp]: "Re(x - y) = Re(x) - Re(y)"
1.132 +
1.133 +lemma complex_Im_diff [simp]: "Im(x - y) = Im(x) - Im(y)"
1.135 +
1.136 +
1.137  subsection{*Multiplication*}
1.138
1.139  lemma complex_mult:
1.140 @@ -222,7 +196,7 @@
1.142
1.143  lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"
1.146                right_diff_distrib right_distrib left_diff_distrib left_distrib)
1.147
1.148  lemma complex_mult_one_left: "(1::complex) * z = z"
1.149 @@ -239,9 +213,9 @@
1.151
1.152  lemma complex_mult_inv_left: "z \<noteq> (0::complex) ==> inverse(z) * z = 1"
1.153 -apply (induct z)
1.154 -apply (rename_tac x y)
1.155 -apply (auto simp add: complex_mult complex_inverse complex_one_def
1.156 +apply (induct z)
1.157 +apply (rename_tac x y)
1.158 +apply (auto simp add: complex_mult complex_inverse complex_one_def
1.159         complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac)
1.160  apply (drule_tac y = y in real_sum_squares_not_zero)
1.161  apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto)
1.162 @@ -254,28 +228,28 @@
1.163  proof
1.164    fix z u v w :: complex
1.165    show "(u + v) + w = u + (v + w)"
1.168    show "z + w = w + z"
1.171    show "0 + z = z"
1.174    show "-z + z = 0"
1.177    show "z - w = z + -w"
1.179    show "(u * v) * w = u * (v * w)"
1.180 -    by (rule complex_mult_assoc)
1.181 +    by (rule complex_mult_assoc)
1.182    show "z * w = w * z"
1.183 -    by (rule complex_mult_commute)
1.184 +    by (rule complex_mult_commute)
1.185    show "1 * z = z"
1.186 -    by (rule complex_mult_one_left)
1.187 +    by (rule complex_mult_one_left)
1.188    show "0 \<noteq> (1::complex)"
1.189      by (simp add: complex_zero_def complex_one_def)
1.190    show "(u + v) * w = u * w + v * w"
1.192    show "z+u = z+v ==> u=v"
1.193      proof -
1.194 -      assume eq: "z+u = z+v"
1.195 +      assume eq: "z+u = z+v"
1.196        hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc)
1.198      qed
1.199 @@ -283,7 +257,7 @@
1.200    thus "z / w = z * inverse w"
1.202    show "inverse w * w = 1"
1.203 -    by (simp add: neq complex_mult_inv_left)
1.204 +    by (simp add: neq complex_mult_inv_left)
1.205  qed
1.206
1.207  instance complex :: division_by_zero
1.208 @@ -291,33 +265,30 @@
1.209    show inv: "inverse 0 = (0::complex)"
1.210      by (simp add: complex_inverse_def complex_zero_def)
1.211    fix x :: complex
1.212 -  show "x/0 = 0"
1.213 +  show "x/0 = 0"
1.214      by (simp add: complex_divide_def inv)
1.215  qed
1.216
1.217
1.218  subsection{*Embedding Properties for @{term complex_of_real} Map*}
1.219
1.220 -lemma complex_of_real_one: "complex_of_real 1 = 1"
1.221 +lemma complex_of_real_one [simp]: "complex_of_real 1 = 1"
1.222  by (simp add: complex_one_def complex_of_real_def)
1.223 -declare complex_of_real_one [simp]
1.224
1.225 -lemma complex_of_real_zero: "complex_of_real 0 = 0"
1.226 +lemma complex_of_real_zero [simp]: "complex_of_real 0 = 0"
1.227  by (simp add: complex_zero_def complex_of_real_def)
1.228 -declare complex_of_real_zero [simp]
1.229
1.230 -lemma complex_of_real_eq_iff:
1.231 +lemma complex_of_real_eq_iff [iff]:
1.232       "(complex_of_real x = complex_of_real y) = (x = y)"
1.234 -declare complex_of_real_eq_iff [iff]
1.236
1.237  lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x"
1.238  by (simp add: complex_of_real_def complex_minus)
1.239
1.240  lemma complex_of_real_inverse:
1.241 - "complex_of_real(inverse x) = inverse(complex_of_real x)"
1.242 +     "complex_of_real(inverse x) = inverse(complex_of_real x)"
1.243  apply (case_tac "x=0", simp)
1.244 -apply (simp add: complex_inverse complex_of_real_def real_divide_def
1.245 +apply (simp add: complex_inverse complex_of_real_def real_divide_def
1.246                   inverse_mult_distrib power2_eq_square)
1.247  done
1.248
1.249 @@ -327,7 +298,8 @@
1.250
1.251  lemma complex_of_real_diff:
1.252       "complex_of_real x - complex_of_real y = complex_of_real (x - y)"
1.254 +by (simp add: complex_of_real_minus [symmetric] complex_diff_def
1.256
1.257  lemma complex_of_real_mult:
1.258       "complex_of_real x * complex_of_real y = complex_of_real (x * y)"
1.259 @@ -337,50 +309,44 @@
1.260        "complex_of_real x / complex_of_real y = complex_of_real(x/y)"
1.262  apply (case_tac "y=0", simp)
1.263 -apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def)
1.264 +apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse
1.265 +                 real_divide_def)
1.266  done
1.267
1.268  lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)"
1.270
1.271 -lemma complex_mod_zero: "cmod(0) = 0"
1.272 +lemma complex_mod_zero [simp]: "cmod(0) = 0"
1.274 -declare complex_mod_zero [simp]
1.275
1.276  lemma complex_mod_one [simp]: "cmod(1) = 1"
1.277  by (simp add: cmod_def power2_eq_square)
1.278
1.279 -lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x"
1.280 +lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x"
1.281  by (simp add: complex_of_real_def power2_eq_square complex_mod)
1.282 -declare complex_mod_complex_of_real [simp]
1.283
1.284  lemma complex_of_real_abs:
1.285       "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))"
1.286  by simp
1.287
1.288
1.289 -
1.290  subsection{*Conjugation is an Automorphism*}
1.291
1.292  lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)"
1.294
1.295 -lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)"
1.296 +lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
1.297  by (simp add: cnj_def complex_Re_Im_cancel_iff)
1.298 -declare complex_cnj_cancel_iff [simp]
1.299
1.300 -lemma complex_cnj_cnj: "cnj (cnj z) = z"
1.301 +lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
1.303 -declare complex_cnj_cnj [simp]
1.304
1.305 -lemma complex_cnj_complex_of_real:
1.306 +lemma complex_cnj_complex_of_real [simp]:
1.307       "cnj (complex_of_real x) = complex_of_real x"
1.308  by (simp add: complex_of_real_def complex_cnj)
1.309 -declare complex_cnj_complex_of_real [simp]
1.310
1.311 -lemma complex_mod_cnj: "cmod (cnj z) = cmod z"
1.312 +lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
1.313  by (induct z, simp add: complex_cnj complex_mod power2_eq_square)
1.314 -declare complex_mod_cnj [simp]
1.315
1.316  lemma complex_cnj_minus: "cnj (-z) = - cnj z"
1.317  by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus)
1.318 @@ -400,60 +366,43 @@
1.319  lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)"
1.320  by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse)
1.321
1.322 -lemma complex_cnj_one: "cnj 1 = 1"
1.323 +lemma complex_cnj_one [simp]: "cnj 1 = 1"
1.324  by (simp add: cnj_def complex_one_def)
1.325 -declare complex_cnj_one [simp]
1.326
1.327  lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))"
1.329
1.330  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
1.331  apply (induct z)
1.334                   complex_minus i_def complex_mult)
1.335  done
1.336
1.337  lemma complex_cnj_zero [simp]: "cnj 0 = 0"
1.338  by (simp add: cnj_def complex_zero_def)
1.339
1.340 -lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)"
1.341 +lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
1.342  by (induct z, simp add: complex_zero_def complex_cnj)
1.343 -declare complex_cnj_zero_iff [iff]
1.344
1.345  lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)"
1.346 -by (induct z, simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
1.347 -
1.348 -
1.349 -subsection{*Algebra*}
1.350 -
1.351 -lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))"
1.354 -
1.355 -lemma complex_diff_mult_distrib: "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)"
1.356 -by (simp add: complex_diff_def left_distrib)
1.357 -
1.358 -lemma complex_diff_mult_distrib2: "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)"
1.359 -by (simp add: complex_diff_def right_distrib)
1.360 +by (induct z,
1.361 +    simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square)
1.362
1.363
1.364  subsection{*Modulus*}
1.365
1.366 -lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)"
1.367 +lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)"
1.368  apply (induct x)
1.369 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2
1.370 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2
1.371              simp add: complex_mod complex_zero_def power2_eq_square)
1.372  done
1.373 -declare complex_mod_eq_zero_cancel [simp]
1.374
1.375 -lemma complex_mod_complex_of_real_of_nat:
1.376 +lemma complex_mod_complex_of_real_of_nat [simp]:
1.377       "cmod (complex_of_real(real (n::nat))) = real n"
1.378  by simp
1.379 -declare complex_mod_complex_of_real_of_nat [simp]
1.380
1.381 -lemma complex_mod_minus: "cmod (-x) = cmod(x)"
1.382 +lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)"
1.383  by (induct x, simp add: complex_mod complex_minus power2_eq_square)
1.384 -declare complex_mod_minus [simp]
1.385
1.386  lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2"
1.387  apply (induct z, simp add: complex_mod complex_cnj complex_mult)
1.388 @@ -463,87 +412,84 @@
1.389  lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2"
1.391
1.392 -lemma complex_mod_ge_zero: "0 \<le> cmod x"
1.393 +lemma complex_mod_ge_zero [simp]: "0 \<le> cmod x"
1.395 -declare complex_mod_ge_zero [simp]
1.396
1.397 -lemma abs_cmod_cancel: "abs(cmod x) = cmod x"
1.398 -by (simp add: abs_if linorder_not_less)
1.399 -declare abs_cmod_cancel [simp]
1.400 +lemma abs_cmod_cancel [simp]: "abs(cmod x) = cmod x"
1.401 +by (simp add: abs_if linorder_not_less)
1.402
1.403  lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)"
1.404  apply (induct x, induct y)
1.405 -apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc)
1.406 +apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric]
1.407 +         simp del: realpow_Suc)
1.408  apply (rule_tac n = 1 in power_inject_base)
1.409  apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc)
1.411 +apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib
1.413  done
1.414
1.415 -lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
1.417 +     "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)"
1.418  apply (induct x, induct y)
1.419  apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
1.421  done
1.422
1.423 -lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \<le> cmod(x * cnj y)"
1.424 +lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \<le> cmod(x * cnj y)"
1.425  apply (induct x, induct y)
1.426  apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc)
1.427  done
1.428 -declare complex_Re_mult_cnj_le_cmod [simp]
1.429
1.430 -lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \<le> cmod(x * y)"
1.431 +lemma complex_Re_mult_cnj_le_cmod2 [simp]: "Re(x * cnj y) \<le> cmod(x * y)"
1.432  by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult)
1.433 -declare complex_Re_mult_cnj_le_cmod2 [simp]
1.434
1.435 -lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
1.436 +lemma real_sum_squared_expand:
1.437 +     "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y"
1.438  by (simp add: left_distrib right_distrib power2_eq_square)
1.439
1.440 -lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
1.441 +lemma complex_mod_triangle_squared [simp]:
1.442 +     "cmod (x + y) ^ 2 \<le> (cmod(x) + cmod(y)) ^ 2"
1.444 -declare complex_mod_triangle_squared [simp]
1.445
1.446 -lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
1.447 +lemma complex_mod_minus_le_complex_mod [simp]: "- cmod x \<le> cmod x"
1.448  by (rule order_trans [OF _ complex_mod_ge_zero], simp)
1.449 -declare complex_mod_minus_le_complex_mod [simp]
1.450
1.451 -lemma complex_mod_triangle_ineq: "cmod (x + y) \<le> cmod(x) + cmod(y)"
1.452 +lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \<le> cmod(x) + cmod(y)"
1.453  apply (rule_tac n = 1 in realpow_increasing)
1.454  apply (auto intro:  order_trans [OF _ complex_mod_ge_zero]
1.456  done
1.457 -declare complex_mod_triangle_ineq [simp]
1.458
1.459 -lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
1.460 +lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
1.461  by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"-cmod b"], simp)
1.462 -declare complex_mod_triangle_ineq2 [simp]
1.463
1.464  lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)"
1.465  apply (induct x, induct y)
1.466  apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac)
1.467  done
1.468
1.469 -lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"
1.471 +     "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s"
1.472  by (auto intro: order_le_less_trans complex_mod_triangle_ineq)
1.473
1.474 -lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"
1.475 +lemma complex_mod_mult_less:
1.476 +     "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s"
1.477  by (auto intro: real_mult_less_mono' simp add: complex_mod_mult)
1.478
1.479 -lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \<le> cmod(a + b)"
1.480 +lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \<le> cmod(a + b)"
1.481  apply (rule linorder_cases [of "cmod(a)" "cmod (b)"])
1.482  apply auto
1.483  apply (rule order_trans [of _ 0], rule order_less_imp_le)
1.484 -apply (simp add: compare_rls, simp)
1.485 +apply (simp add: compare_rls, simp)
1.487  apply (rule complex_mod_minus [THEN subst])
1.488  apply (rule order_trans)
1.489  apply (rule_tac [2] complex_mod_triangle_ineq)
1.491  done
1.492 -declare complex_mod_diff_ineq [simp]
1.493
1.494 -lemma complex_Re_le_cmod: "Re z \<le> cmod z"
1.495 +lemma complex_Re_le_cmod [simp]: "Re z \<le> cmod z"
1.496  by (induct z, simp add: complex_mod del: realpow_Suc)
1.497 -declare complex_Re_le_cmod [simp]
1.498
1.499  lemma complex_mod_gt_zero: "z \<noteq> 0 ==> 0 < cmod z"
1.500  apply (insert complex_mod_ge_zero [of z])
1.501 @@ -562,9 +508,8 @@
1.502  lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)"
1.504
1.505 -lemma complex_inverse_divide: "inverse(x/y) = y/(x::complex)"
1.506 +lemma complex_inverse_divide [simp]: "inverse(x/y) = y/(x::complex)"
1.507  by (simp add: complex_divide_def inverse_mult_distrib mult_commute)
1.508 -declare complex_inverse_divide [simp]
1.509
1.510
1.511  subsection{*Exponentiation*}
1.512 @@ -598,7 +543,8 @@
1.513  apply (auto simp add: complex_mod_mult)
1.514  done
1.515
1.516 -lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
1.517 +lemma complexpow_minus:
1.518 +     "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
1.519  by (induct_tac "n", auto)
1.520
1.521  lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)"
1.522 @@ -610,19 +556,16 @@
1.523
1.524  subsection{*The Function @{term sgn}*}
1.525
1.526 -lemma sgn_zero: "sgn 0 = 0"
1.527 +lemma sgn_zero [simp]: "sgn 0 = 0"
1.529 -declare sgn_zero [simp]
1.530
1.531 -lemma sgn_one: "sgn 1 = 1"
1.532 +lemma sgn_one [simp]: "sgn 1 = 1"
1.534 -declare sgn_one [simp]
1.535
1.536  lemma sgn_minus: "sgn (-z) = - sgn(z)"
1.538
1.539 -lemma sgn_eq:
1.540 -    "sgn z = z / complex_of_real (cmod z)"
1.541 +lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)"
1.543  done
1.544
1.545 @@ -631,20 +574,18 @@
1.547  done
1.548
1.549 -lemma Re_complex_i: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x"
1.550 +(*????delete????*)
1.551 +lemma Re_complex_i [simp]: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x"
1.553 -declare Re_complex_i [simp]
1.554
1.555 -lemma Im_complex_i: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
1.556 +lemma Im_complex_i [simp]: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y"
1.558 -declare Im_complex_i [simp]
1.559
1.560  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
1.562
1.563 -lemma i_mult_eq2: "ii * ii = -(1::complex)"
1.564 +lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)"
1.565  by (simp add: i_def complex_one_def complex_mult complex_minus)
1.566 -declare i_mult_eq2 [simp]
1.567
1.568  lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) =
1.569        sqrt (x ^ 2 + y ^ 2)"
1.570 @@ -662,49 +603,52 @@
1.571         ==> ya = yb"
1.573
1.574 -lemma complex_eq_cancel_iff: "(complex_of_real xa + ii * complex_of_real ya =
1.575 +(*FIXME: tidy up this mess by fixing a canonical form for complex expressions,
1.576 +e.g. x + y*ii*)
1.577 +
1.578 +lemma complex_eq_cancel_iff [iff]:
1.579 +     "(complex_of_real xa + ii * complex_of_real ya =
1.580         complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
1.581  by (auto intro: complex_eq_Im_eq complex_eq_Re_eq)
1.582 -declare complex_eq_cancel_iff [iff]
1.583
1.584 -lemma complex_eq_cancel_iffA: "(complex_of_real xa + complex_of_real ya * ii =
1.585 +lemma complex_eq_cancel_iffA [iff]:
1.586 +     "(complex_of_real xa + complex_of_real ya * ii =
1.587         complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
1.589 -declare complex_eq_cancel_iffA [iff]
1.590
1.591 -lemma complex_eq_cancel_iffB: "(complex_of_real xa + complex_of_real ya * ii =
1.592 +lemma complex_eq_cancel_iffB [iff]:
1.593 +     "(complex_of_real xa + complex_of_real ya * ii =
1.594         complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))"
1.595  by (auto simp add: mult_commute)
1.596 -declare complex_eq_cancel_iffB [iff]
1.597
1.598 -lemma complex_eq_cancel_iffC: "(complex_of_real xa + ii * complex_of_real ya  =
1.599 +lemma complex_eq_cancel_iffC [iff]:
1.600 +     "(complex_of_real xa + ii * complex_of_real ya  =
1.601         complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))"
1.602  by (auto simp add: mult_commute)
1.603 -declare complex_eq_cancel_iffC [iff]
1.604
1.605 -lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y =
1.606 +lemma complex_eq_cancel_iff2 [simp]:
1.607 +     "(complex_of_real x + ii * complex_of_real y =
1.608        complex_of_real xa) = (x = xa & y = 0)"
1.609  apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff)
1.610  apply (simp del: complex_eq_cancel_iff)
1.611  done
1.612 -declare complex_eq_cancel_iff2 [simp]
1.613
1.614 -lemma complex_eq_cancel_iff2a: "(complex_of_real x + complex_of_real y * ii =
1.615 +lemma complex_eq_cancel_iff2a [simp]:
1.616 +     "(complex_of_real x + complex_of_real y * ii =
1.617        complex_of_real xa) = (x = xa & y = 0)"
1.618  by (auto simp add: mult_commute)
1.619 -declare complex_eq_cancel_iff2a [simp]
1.620
1.621 -lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y =
1.622 +lemma complex_eq_cancel_iff3 [simp]:
1.623 +     "(complex_of_real x + ii * complex_of_real y =
1.624        ii * complex_of_real ya) = (x = 0 & y = ya)"
1.625  apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff)
1.626  apply (simp del: complex_eq_cancel_iff)
1.627  done
1.628 -declare complex_eq_cancel_iff3 [simp]
1.629
1.630 -lemma complex_eq_cancel_iff3a: "(complex_of_real x + complex_of_real y * ii =
1.631 +lemma complex_eq_cancel_iff3a [simp]:
1.632 +     "(complex_of_real x + complex_of_real y * ii =
1.633        ii * complex_of_real ya) = (x = 0 & y = ya)"
1.634  by (auto simp add: mult_commute)
1.635 -declare complex_eq_cancel_iff3a [simp]
1.636
1.637  lemma complex_split_Re_zero:
1.638       "complex_of_real x + ii * complex_of_real y = 0
1.639 @@ -716,26 +660,23 @@
1.640        ==> y = 0"
1.642
1.643 -lemma Re_sgn: "Re(sgn z) = Re(z)/cmod z"
1.644 +lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z"
1.645  apply (induct z)
1.646  apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
1.647  apply (simp add: complex_of_real_def complex_mult real_divide_def)
1.648  done
1.649 -declare Re_sgn [simp]
1.650
1.651 -lemma Im_sgn:
1.652 -      "Im(sgn z) = Im(z)/cmod z"
1.653 +lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z"
1.654  apply (induct z)
1.655  apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric])
1.656  apply (simp add: complex_of_real_def complex_mult real_divide_def)
1.657  done
1.658 -declare Im_sgn [simp]
1.659
1.660  lemma complex_inverse_complex_split:
1.661       "inverse(complex_of_real x + ii * complex_of_real y) =
1.662        complex_of_real(x/(x ^ 2 + y ^ 2)) -
1.663        ii * complex_of_real(y/(x ^ 2 + y ^ 2))"
1.666           complex_diff_def complex_minus complex_inverse real_divide_def)
1.667
1.668  (*----------------------------------------------------------------------------*)
1.669 @@ -746,17 +687,14 @@
1.670  lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)"
1.671  by (auto simp add: complex_zero_def complex_of_real_def)
1.672
1.673 -lemma Re_mult_i_eq: "Re (ii * complex_of_real y) = 0"
1.674 -by (simp add: i_def complex_of_real_def complex_mult)
1.675 -declare Re_mult_i_eq [simp]
1.676 -
1.677 -lemma Im_mult_i_eq: "Im (ii * complex_of_real y) = y"
1.678 +lemma Re_mult_i_eq [simp]: "Re (ii * complex_of_real y) = 0"
1.679  by (simp add: i_def complex_of_real_def complex_mult)
1.680 -declare Im_mult_i_eq [simp]
1.681
1.682 -lemma complex_mod_mult_i: "cmod (ii * complex_of_real y) = abs y"
1.683 +lemma Im_mult_i_eq [simp]: "Im (ii * complex_of_real y) = y"
1.684 +by (simp add: i_def complex_of_real_def complex_mult)
1.685 +
1.686 +lemma complex_mod_mult_i [simp]: "cmod (ii * complex_of_real y) = abs y"
1.687  by (simp add: i_def complex_of_real_def complex_mult complex_mod power2_eq_square)
1.688 -declare complex_mod_mult_i [simp]
1.689
1.690  lemma cos_arg_i_mult_zero_pos:
1.691     "0 < y ==> cos (arg(ii * complex_of_real y)) = 0"
1.692 @@ -772,16 +710,17 @@
1.693  apply (rule order_trans [of _ 0], auto)
1.694  done
1.695
1.696 -lemma cos_arg_i_mult_zero [simp]
1.697 -    : "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
1.698 -apply (insert linorder_less_linear [of y 0])
1.699 +lemma cos_arg_i_mult_zero [simp]:
1.700 +     "y \<noteq> 0 ==> cos (arg(ii * complex_of_real y)) = 0"
1.701 +apply (insert linorder_less_linear [of y 0])
1.702  apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg)
1.703  done
1.704
1.705
1.706  subsection{*Finally! Polar Form for Complex Numbers*}
1.707
1.708 -lemma complex_split_polar: "\<exists>r a. z = complex_of_real r *
1.709 +lemma complex_split_polar:
1.710 +     "\<exists>r a. z = complex_of_real r *
1.711        (complex_of_real(cos a) + ii * complex_of_real(sin a))"
1.712  apply (cut_tac z = z in complex_split)
1.713  apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac)
1.714 @@ -792,18 +731,17 @@
1.715  apply (rule complex_split_polar)
1.716  done
1.717
1.718 -lemma Re_complex_polar: "Re(complex_of_real r *
1.719 +lemma Re_complex_polar [simp]:
1.720 +     "Re(complex_of_real r *
1.721        (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a"
1.722  by (auto simp add: right_distrib complex_of_real_mult mult_ac)
1.723 -declare Re_complex_polar [simp]
1.724
1.725 -lemma Re_rcis: "Re(rcis r a) = r * cos a"
1.726 +lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
1.727  by (simp add: rcis_def cis_def)
1.728 -declare Re_rcis [simp]
1.729
1.730  lemma Im_complex_polar [simp]:
1.731 -     "Im(complex_of_real r *
1.732 -         (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
1.733 +     "Im(complex_of_real r *
1.734 +         (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
1.735        r * sin a"
1.736  by (auto simp add: right_distrib complex_of_real_mult mult_ac)
1.737
1.738 @@ -811,16 +749,15 @@
1.739  by (simp add: rcis_def cis_def)
1.740
1.741  lemma complex_mod_complex_polar [simp]:
1.742 -     "cmod (complex_of_real r *
1.743 -            (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
1.744 +     "cmod (complex_of_real r *
1.745 +            (complex_of_real(cos a) + ii * complex_of_real(sin a))) =
1.746        abs r"
1.747  by (auto simp add: right_distrib cmod_i complex_of_real_mult
1.748 -                      right_distrib [symmetric] power_mult_distrib mult_ac
1.749 +                      right_distrib [symmetric] power_mult_distrib mult_ac
1.750           simp del: realpow_Suc)
1.751
1.752 -lemma complex_mod_rcis: "cmod(rcis r a) = abs r"
1.753 +lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
1.754  by (simp add: rcis_def cis_def)
1.755 -declare complex_mod_rcis [simp]
1.756
1.757  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
1.759 @@ -828,36 +765,33 @@
1.760  apply (auto simp add: complex_mult_cnj)
1.761  done
1.762
1.763 -lemma complex_Re_cnj: "Re(cnj z) = Re z"
1.764 -by (induct z, simp add: complex_cnj)
1.765 -declare complex_Re_cnj [simp]
1.766 -
1.767 -lemma complex_Im_cnj: "Im(cnj z) = - Im z"
1.768 +lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z"
1.769  by (induct z, simp add: complex_cnj)
1.770 -declare complex_Im_cnj [simp]
1.771
1.772 -lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0"
1.773 +lemma complex_Im_cnj [simp]: "Im(cnj z) = - Im z"
1.774 +by (induct z, simp add: complex_cnj)
1.775 +
1.776 +lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
1.777  by (induct z, simp add: complex_cnj complex_mult)
1.778 -declare complex_In_mult_cnj_zero [simp]
1.779
1.780  lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)"
1.781  by (induct z, induct w, simp add: complex_mult)
1.782
1.783 -lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c"
1.784 +lemma complex_Re_mult_complex_of_real [simp]:
1.785 +     "Re (z * complex_of_real c) = Re(z) * c"
1.786  by (induct z, simp add: complex_of_real_def complex_mult)
1.787 -declare complex_Re_mult_complex_of_real [simp]
1.788
1.789 -lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c"
1.790 +lemma complex_Im_mult_complex_of_real [simp]:
1.791 +     "Im (z * complex_of_real c) = Im(z) * c"
1.792  by (induct z, simp add: complex_of_real_def complex_mult)
1.793 -declare complex_Im_mult_complex_of_real [simp]
1.794
1.795 -lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)"
1.796 +lemma complex_Re_mult_complex_of_real2 [simp]:
1.797 +     "Re (complex_of_real c * z) = c * Re(z)"
1.798  by (induct z, simp add: complex_of_real_def complex_mult)
1.799 -declare complex_Re_mult_complex_of_real2 [simp]
1.800
1.801 -lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)"
1.802 +lemma complex_Im_mult_complex_of_real2 [simp]:
1.803 +     "Im (complex_of_real c * z) = c * Im(z)"
1.804  by (induct z, simp add: complex_of_real_def complex_mult)
1.805 -declare complex_Im_mult_complex_of_real2 [simp]
1.806
1.807  (*---------------------------------------------------------------------------*)
1.808  (*  (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b)                      *)
1.809 @@ -866,9 +800,8 @@
1.810  lemma cis_rcis_eq: "cis a = rcis 1 a"
1.812
1.813 -lemma rcis_mult:
1.814 -  "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
1.816 +lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
1.819  apply (auto simp add: right_distrib [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)
1.821 @@ -878,30 +811,25 @@
1.822  lemma cis_mult: "cis a * cis b = cis (a + b)"
1.823  by (simp add: cis_rcis_eq rcis_mult)
1.824
1.825 -lemma cis_zero: "cis 0 = 1"
1.826 +lemma cis_zero [simp]: "cis 0 = 1"
1.828 -declare cis_zero [simp]
1.829
1.830 -lemma cis_zero2: "cis 0 = complex_of_real 1"
1.831 +lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1"
1.833 -declare cis_zero2 [simp]
1.834
1.835 -lemma rcis_zero_mod: "rcis 0 a = 0"
1.836 +lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
1.838 -declare rcis_zero_mod [simp]
1.839
1.840 -lemma rcis_zero_arg: "rcis r 0 = complex_of_real r"
1.841 +lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
1.843 -declare rcis_zero_arg [simp]
1.844
1.845  lemma complex_of_real_minus_one:
1.846     "complex_of_real (-(1::real)) = -(1::complex)"
1.847  apply (simp add: complex_of_real_def complex_one_def complex_minus)
1.848  done
1.849
1.850 -lemma complex_i_mult_minus: "ii * (ii * x) = - x"
1.851 +lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
1.852  by (simp add: complex_mult_assoc [symmetric])
1.853 -declare complex_i_mult_minus [simp]
1.854
1.855
1.856  lemma cis_real_of_nat_Suc_mult:
1.857 @@ -916,20 +844,19 @@
1.858  apply (auto simp add: cis_real_of_nat_Suc_mult)
1.859  done
1.860
1.861 -lemma DeMoivre2:
1.862 -   "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
1.863 -apply (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow)
1.864 -done
1.865 +lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
1.866 +by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow)
1.867
1.868 -lemma cis_inverse: "inverse(cis a) = cis (-a)"
1.869 -by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus complex_diff_def)
1.870 -declare cis_inverse [simp]
1.871 +lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
1.872 +by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus
1.873 +              complex_diff_def)
1.874
1.875  lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
1.876  apply (case_tac "r=0", simp)
1.877 -apply (auto simp add: complex_inverse_complex_split right_distrib
1.878 +apply (auto simp add: complex_inverse_complex_split right_distrib
1.879              complex_of_real_mult rcis_def cis_def power2_eq_square mult_ac)
1.880 -apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def)
1.881 +apply (auto simp add: right_distrib [symmetric] complex_of_real_minus
1.882 +                      complex_diff_def)
1.883  done
1.884
1.885  lemma cis_divide: "cis a / cis b = cis (a - b)"
1.886 @@ -941,13 +868,11 @@
1.887  apply (simp add: rcis_inverse rcis_mult real_diff_def)
1.888  done
1.889
1.890 -lemma Re_cis: "Re(cis a) = cos a"
1.891 +lemma Re_cis [simp]: "Re(cis a) = cos a"
1.893 -declare Re_cis [simp]
1.894
1.895 -lemma Im_cis: "Im(cis a) = sin a"
1.896 +lemma Im_cis [simp]: "Im(cis a) = sin a"
1.898 -declare Im_cis [simp]
1.899
1.900  lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
1.901  by (auto simp add: DeMoivre)
1.902 @@ -965,16 +890,16 @@
1.904
1.905  lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
1.908 +              cis_mult [symmetric] complex_of_real_mult mult_ac)
1.909
1.910  lemma expi_complex_split:
1.911       "expi(complex_of_real x + ii * complex_of_real y) =
1.912        complex_of_real (exp(x)) * cis y"
1.914
1.915 -lemma expi_zero: "expi (0::complex) = 1"
1.916 +lemma expi_zero [simp]: "expi (0::complex) = 1"
1.918 -declare expi_zero [simp]
1.919
1.920  lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z"
1.921  by (induct z, induct w, simp add: complex_mult)
1.922 @@ -984,8 +909,7 @@
1.923  apply (induct z, induct w, simp add: complex_mult)
1.924  done
1.925
1.926 -lemma complex_expi_Ex:
1.927 -   "\<exists>a r. z = complex_of_real r * expi a"
1.928 +lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
1.929  apply (insert rcis_Ex [of z])
1.930  apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult)
1.931  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
1.932 @@ -1023,17 +947,11 @@
1.933  val complex_Im_one = thm"complex_Im_one";
1.934  val complex_Re_i = thm"complex_Re_i";
1.935  val complex_Im_i = thm"complex_Im_i";
1.936 -val Re_complex_of_real_zero = thm"Re_complex_of_real_zero";
1.937 -val Im_complex_of_real_zero = thm"Im_complex_of_real_zero";
1.938 -val Re_complex_of_real_one = thm"Re_complex_of_real_one";
1.939 -val Im_complex_of_real_one = thm"Im_complex_of_real_one";
1.940  val Re_complex_of_real = thm"Re_complex_of_real";
1.941  val Im_complex_of_real = thm"Im_complex_of_real";
1.942  val complex_minus = thm"complex_minus";
1.943  val complex_Re_minus = thm"complex_Re_minus";
1.944  val complex_Im_minus = thm"complex_Im_minus";
1.945 -val complex_minus_zero = thm"complex_minus_zero";
1.946 -val complex_minus_zero_iff = thm"complex_minus_zero_iff";