author paulson Tue Feb 03 15:58:31 2004 +0100 (2004-02-03) changeset 14374 61de62096768 parent 14373 67a628beb981 child 14375 a545da363b23
further tidying of the complex numbers
 src/HOL/Complex/Complex.thy file | annotate | diff | revisions src/HOL/Complex/NSCA.ML file | annotate | diff | revisions src/HOL/Complex/NSComplex.thy file | annotate | diff | revisions src/HOL/Real/Complex_Numbers.thy file | annotate | diff | revisions src/HOL/Real/Real.thy file | annotate | diff | revisions
```     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";
1.950 @@ -1079,9 +997,6 @@
1.951  val complex_cnj_zero = thm"complex_cnj_zero";
1.952  val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
1.953  val complex_mult_cnj = thm"complex_mult_cnj";
1.955 -val complex_diff_mult_distrib = thm"complex_diff_mult_distrib";
1.956 -val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2";
1.957  val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel";
1.958  val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat";
1.959  val complex_mod_minus = thm"complex_mod_minus";
```
```     2.1 --- a/src/HOL/Complex/NSCA.ML	Tue Feb 03 11:06:36 2004 +0100
2.2 +++ b/src/HOL/Complex/NSCA.ML	Tue Feb 03 15:58:31 2004 +0100
2.3 @@ -493,13 +493,13 @@
2.4  Goal "[| y: CInfinitesimal; x + y = z |] ==> x @c= z";
2.5  by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
2.6  by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
2.8 +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1);
2.10
2.11  Goal "y: CInfinitesimal ==> x @c= x + y";
2.12  by (rtac (bex_CInfinitesimal_iff RS iffD1) 1);
2.13  by (dtac (CInfinitesimal_minus_iff RS iffD2) 1);
2.15 +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1);
2.17
2.18  Goal "y: CInfinitesimal ==> x @c= y + x";
```
```     3.1 --- a/src/HOL/Complex/NSComplex.thy	Tue Feb 03 11:06:36 2004 +0100
3.2 +++ b/src/HOL/Complex/NSComplex.thy	Tue Feb 03 15:58:31 2004 +0100
3.3 @@ -127,38 +127,26 @@
3.4               hcomplexrel `` {%n. (X n) ^ (Y n)})"
3.5
3.6
3.7 -lemma hcomplexrel_iff:
3.8 -   "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
3.9 -apply (unfold hcomplexrel_def)
3.10 -apply fast
3.11 -done
3.12 -
3.13  lemma hcomplexrel_refl: "(x,x): hcomplexrel"
3.15 -done
3.17
3.18  lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel"
3.19 -apply (auto simp add: hcomplexrel_iff eq_commute)
3.20 -done
3.21 +by (auto simp add: hcomplexrel_def eq_commute)
3.22
3.23  lemma hcomplexrel_trans:
3.24        "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel"
3.26 -apply ultra
3.27 -done
3.28 +by (simp add: hcomplexrel_def, ultra)
3.29
3.30  lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel"
3.31 -apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl)
3.32 -apply (blast intro: hcomplexrel_sym hcomplexrel_trans)
3.33 +apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl)
3.34 +apply (blast intro: hcomplexrel_sym hcomplexrel_trans)
3.35  done
3.36
3.37  lemmas equiv_hcomplexrel_iff =
3.38      eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp]
3.39
3.40  lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex"
3.41 -apply (unfold hcomplex_def hcomplexrel_def quotient_def)
3.42 -apply blast
3.43 -done
3.44 +by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast)
3.45
3.46  lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex"
3.47  apply (rule inj_on_inverseI)
3.48 @@ -170,216 +158,188 @@
3.49
3.50  declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp]
3.51
3.52 -declare hcomplexrel_iff [iff]
3.53
3.54  lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)"
3.55  apply (rule inj_on_inverseI)
3.56  apply (rule Rep_hcomplex_inverse)
3.57  done
3.58
3.59 -lemma lemma_hcomplexrel_refl: "x: hcomplexrel `` {x}"
3.60 -apply (unfold hcomplexrel_def)
3.61 -apply (safe)
3.62 -apply auto
3.63 -done
3.64 -declare lemma_hcomplexrel_refl [simp]
3.65 +lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}"
3.67
3.68 -lemma hcomplex_empty_not_mem: "{} \<notin> hcomplex"
3.69 -apply (unfold hcomplex_def)
3.70 +lemma hcomplex_empty_not_mem [simp]: "{} \<notin> hcomplex"
3.71 +apply (simp add: hcomplex_def hcomplexrel_def)
3.72  apply (auto elim!: quotientE)
3.73  done
3.74 -declare hcomplex_empty_not_mem [simp]
3.75
3.76 -lemma Rep_hcomplex_nonempty: "Rep_hcomplex x \<noteq> {}"
3.77 -apply (cut_tac x = "x" in Rep_hcomplex)
3.78 -apply auto
3.79 -done
3.80 -declare Rep_hcomplex_nonempty [simp]
3.81 +lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \<noteq> {}"
3.82 +by (cut_tac x = x in Rep_hcomplex, auto)
3.83
3.84  lemma eq_Abs_hcomplex:
3.85      "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P"
3.86  apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE])
3.87  apply (drule_tac f = Abs_hcomplex in arg_cong)
3.88 -apply (force simp add: Rep_hcomplex_inverse)
3.89 +apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def)
3.90  done
3.91
3.92 +(*??delete*)
3.93 +lemma hcomplexrel_iff [iff]:
3.94 +   "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
3.96 +
3.97
3.98  subsection{*Properties of Nonstandard Real and Imaginary Parts*}
3.99
3.100  lemma hRe:
3.101       "hRe(Abs_hcomplex (hcomplexrel `` {X})) =
3.102        Abs_hypreal(hyprel `` {%n. Re(X n)})"
3.103 -apply (unfold hRe_def)
3.104 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
3.105 -apply (auto , ultra)
3.107 +apply (rule_tac f = Abs_hypreal in arg_cong)
3.108 +apply (auto, ultra)
3.109  done
3.110
3.111  lemma hIm:
3.112       "hIm(Abs_hcomplex (hcomplexrel `` {X})) =
3.113        Abs_hypreal(hyprel `` {%n. Im(X n)})"
3.114 -apply (unfold hIm_def)
3.115 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
3.116 -apply (auto , ultra)
3.118 +apply (rule_tac f = Abs_hypreal in arg_cong)
3.119 +apply (auto, ultra)
3.120  done
3.121
3.122  lemma hcomplex_hRe_hIm_cancel_iff:
3.123       "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))"
3.124 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.125 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.126 +apply (rule eq_Abs_hcomplex [of z])
3.127 +apply (rule eq_Abs_hcomplex [of w])
3.128  apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff)
3.129  apply (ultra+)
3.130  done
3.131
3.132 -lemma hcomplex_hRe_zero: "hRe 0 = 0"
3.133 -apply (unfold hcomplex_zero_def)
3.134 -apply (simp (no_asm) add: hRe hypreal_zero_num)
3.135 -done
3.136 -declare hcomplex_hRe_zero [simp]
3.137 +lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
3.138 +by (simp add: hcomplex_zero_def hRe hypreal_zero_num)
3.139
3.140 -lemma hcomplex_hIm_zero: "hIm 0 = 0"
3.141 -apply (unfold hcomplex_zero_def)
3.142 -apply (simp (no_asm) add: hIm hypreal_zero_num)
3.143 -done
3.144 -declare hcomplex_hIm_zero [simp]
3.145 +lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
3.146 +by (simp add: hcomplex_zero_def hIm hypreal_zero_num)
3.147
3.148 -lemma hcomplex_hRe_one: "hRe 1 = 1"
3.149 -apply (unfold hcomplex_one_def)
3.150 -apply (simp (no_asm) add: hRe hypreal_one_num)
3.151 -done
3.152 -declare hcomplex_hRe_one [simp]
3.153 +lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
3.154 +by (simp add: hcomplex_one_def hRe hypreal_one_num)
3.155
3.156 -lemma hcomplex_hIm_one: "hIm 1 = 0"
3.157 -apply (unfold hcomplex_one_def)
3.158 -apply (simp (no_asm) add: hIm hypreal_one_def hypreal_zero_num)
3.159 -done
3.160 -declare hcomplex_hIm_one [simp]
3.161 +lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
3.162 +by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num)
3.163
3.164
3.165  subsection{*Addition for Nonstandard Complex Numbers*}
3.166
3.168      "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})"
3.169 -apply (unfold congruent2_def)
3.170 -apply safe
3.171 -apply (ultra+)
3.172 -done
3.173 +by (auto simp add: congruent2_def, ultra)
3.174
3.176    "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) =
3.177     Abs_hcomplex(hcomplexrel``{%n. X n + Y n})"
3.179 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.181 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.182  apply (auto, ultra)
3.183  done
3.184
3.185  lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z"
3.186 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.187 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.188 +apply (rule eq_Abs_hcomplex [of z])
3.189 +apply (rule eq_Abs_hcomplex [of w])
3.191  done
3.192
3.193  lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)"
3.194 -apply (rule_tac z = "z1" in eq_Abs_hcomplex)
3.195 -apply (rule_tac z = "z2" in eq_Abs_hcomplex)
3.196 -apply (rule_tac z = "z3" in eq_Abs_hcomplex)
3.197 +apply (rule eq_Abs_hcomplex [of z1])
3.198 +apply (rule eq_Abs_hcomplex [of z2])
3.199 +apply (rule eq_Abs_hcomplex [of z3])
3.201  done
3.202
3.203  lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z"
3.204 -apply (unfold hcomplex_zero_def)
3.205 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.207 +apply (rule eq_Abs_hcomplex [of z])
3.209  done
3.210
3.211  lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
3.213 -done
3.215
3.216  lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)"
3.217 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.218 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.220 +apply (rule eq_Abs_hcomplex [of x])
3.221 +apply (rule eq_Abs_hcomplex [of y])
3.223  done
3.224
3.225  lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)"
3.226 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.227 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.229 +apply (rule eq_Abs_hcomplex [of x])
3.230 +apply (rule eq_Abs_hcomplex [of y])
3.232  done
3.233
3.234
3.235  subsection{*Additive Inverse on Nonstandard Complex Numbers*}
3.236
3.237  lemma hcomplex_minus_congruent:
3.238 -  "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
3.239 -apply (unfold congruent_def)
3.240 -apply safe
3.241 -apply (ultra+)
3.242 -done
3.243 +     "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})"
3.245
3.246  lemma hcomplex_minus:
3.247    "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
3.248        Abs_hcomplex(hcomplexrel `` {%n. -(X n)})"
3.249 -apply (unfold hcomplex_minus_def)
3.250 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.252 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.253  apply (auto, ultra)
3.254  done
3.255
3.256  lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)"
3.257 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.259 +apply (rule eq_Abs_hcomplex [of z])
3.261  done
3.262
3.263
3.264  subsection{*Multiplication for Nonstandard Complex Numbers*}
3.265
3.266  lemma hcomplex_mult:
3.267 -  "Abs_hcomplex(hcomplexrel``{%n. X n}) *
3.268 +  "Abs_hcomplex(hcomplexrel``{%n. X n}) *
3.269       Abs_hcomplex(hcomplexrel``{%n. Y n}) =
3.270 -   Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
3.271 -apply (unfold hcomplex_mult_def)
3.272 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.273 +     Abs_hcomplex(hcomplexrel``{%n. X n * Y n})"
3.275 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.276  apply (auto, ultra)
3.277  done
3.278
3.279  lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w"
3.280 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.281 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.282 -apply (auto simp add: hcomplex_mult complex_mult_commute)
3.283 +apply (rule eq_Abs_hcomplex [of w])
3.284 +apply (rule eq_Abs_hcomplex [of z])
3.285 +apply (simp add: hcomplex_mult complex_mult_commute)
3.286  done
3.287
3.288  lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)"
3.289 -apply (rule_tac z = "u" in eq_Abs_hcomplex)
3.290 -apply (rule_tac z = "v" in eq_Abs_hcomplex)
3.291 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.292 -apply (auto simp add: hcomplex_mult complex_mult_assoc)
3.293 +apply (rule eq_Abs_hcomplex [of u])
3.294 +apply (rule eq_Abs_hcomplex [of v])
3.295 +apply (rule eq_Abs_hcomplex [of w])
3.296 +apply (simp add: hcomplex_mult complex_mult_assoc)
3.297  done
3.298
3.299  lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z"
3.300 -apply (unfold hcomplex_one_def)
3.301 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.302 -apply (auto simp add: hcomplex_mult)
3.303 +apply (rule eq_Abs_hcomplex [of z])
3.304 +apply (simp add: hcomplex_one_def hcomplex_mult)
3.305  done
3.306
3.307  lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0"
3.308 -apply (unfold hcomplex_zero_def)
3.309 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.310 -apply (auto simp add: hcomplex_mult)
3.311 +apply (rule eq_Abs_hcomplex [of z])
3.312 +apply (simp add: hcomplex_zero_def hcomplex_mult)
3.313  done
3.314
3.316       "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)"
3.317 -apply (rule_tac z = "z1" in eq_Abs_hcomplex)
3.318 -apply (rule_tac z = "z2" in eq_Abs_hcomplex)
3.319 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.321 +apply (rule eq_Abs_hcomplex [of z1])
3.322 +apply (rule eq_Abs_hcomplex [of z2])
3.323 +apply (rule eq_Abs_hcomplex [of w])
3.325  done
3.326
3.327  lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \<noteq> (1::hcomplex)"
3.328 -apply (unfold hcomplex_zero_def hcomplex_one_def)
3.329 -apply auto
3.330 -done
3.331 -declare hcomplex_zero_not_eq_one [simp]
3.332 +by (simp add: hcomplex_zero_def hcomplex_one_def)
3.333 +
3.334  declare hcomplex_zero_not_eq_one [THEN not_sym, simp]
3.335
3.336
3.337 @@ -388,20 +348,17 @@
3.338  lemma hcomplex_inverse:
3.339    "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
3.340        Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})"
3.341 -apply (unfold hcinv_def)
3.342 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.344 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.345  apply (auto, ultra)
3.346  done
3.347
3.348  lemma hcomplex_mult_inv_left:
3.349        "z \<noteq> (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)"
3.350 -apply (unfold hcomplex_zero_def hcomplex_one_def)
3.351 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.352 -apply (auto simp add: hcomplex_inverse hcomplex_mult)
3.353 -apply (ultra)
3.354 +apply (rule eq_Abs_hcomplex [of z])
3.355 +apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra)
3.356  apply (rule ccontr)
3.357 -apply (drule left_inverse)
3.358 -apply auto
3.359 +apply (drule left_inverse, auto)
3.360  done
3.361
3.362  subsection {* The Field of Nonstandard Complex Numbers *}
3.363 @@ -431,9 +388,9 @@
3.365    show "z+u = z+v ==> u=v"
3.366      proof -
3.367 -      assume eq: "z+u = z+v"
3.368 +      assume eq: "z+u = z+v"
3.369        hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc)
3.370 -      thus "u = v"
3.371 +      thus "u = v"
3.373      qed
3.374    assume neq: "w \<noteq> 0"
3.375 @@ -443,71 +400,53 @@
3.376      by (rule hcomplex_mult_inv_left)
3.377  qed
3.378
3.379 -lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0"
3.380 -apply (simp add:  hcomplex_zero_def hcomplex_inverse)
3.381 -done
3.382 -
3.383 -lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0"
3.384 -apply (simp add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO)
3.385 -done
3.386 -
3.387  instance hcomplex :: division_by_zero
3.388  proof
3.389 +  show inv: "inverse 0 = (0::hcomplex)"
3.390 +    by (simp add: hcomplex_inverse hcomplex_zero_def)
3.391    fix x :: hcomplex
3.392 -  show "inverse 0 = (0::hcomplex)" by (rule HCOMPLEX_INVERSE_ZERO)
3.393 -  show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO)
3.394 +  show "x/0 = 0"
3.395 +    by (simp add: hcomplex_divide_def inv)
3.396  qed
3.397
3.398 +
3.399  subsection{*More Minus Laws*}
3.400
3.401 -lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)"
3.402 -apply (rule inj_onI)
3.403 -apply (drule_tac f = "uminus" in arg_cong)
3.404 -apply simp
3.405 -done
3.406 -
3.407  lemma hRe_minus: "hRe(-z) = - hRe(z)"
3.408 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.409 -apply (auto simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
3.410 +apply (rule eq_Abs_hcomplex [of z])
3.411 +apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus)
3.412  done
3.413
3.414  lemma hIm_minus: "hIm(-z) = - hIm(z)"
3.415 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.416 -apply (auto simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
3.417 +apply (rule eq_Abs_hcomplex [of z])
3.418 +apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus)
3.419  done
3.420
3.422        "x + y = (0::hcomplex) ==> x = -y"
3.423 -apply (drule Ring_and_Field.equals_zero_I)
3.424 -apply (simp add: minus_equation_iff [of x y])
3.425 +apply (drule Ring_and_Field.equals_zero_I)
3.426 +apply (simp add: minus_equation_iff [of x y])
3.427  done
3.428
3.429
3.430  subsection{*More Multiplication Laws*}
3.431
3.432  lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z"
3.433 -apply (rule Ring_and_Field.mult_1_right)
3.434 -done
3.435 +by (rule Ring_and_Field.mult_1_right)
3.436
3.437 -lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z"
3.438 -apply (simp (no_asm))
3.439 -done
3.440 -declare hcomplex_mult_minus_one [simp]
3.441 +lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z"
3.442 +by simp
3.443
3.444 -lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z"
3.445 -apply (subst hcomplex_mult_commute)
3.446 -apply (simp (no_asm))
3.447 -done
3.448 -declare hcomplex_mult_minus_one_right [simp]
3.449 +lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z"
3.450 +by (subst hcomplex_mult_commute, simp)
3.451
3.452  lemma hcomplex_mult_left_cancel:
3.453       "(c::hcomplex) \<noteq> (0::hcomplex) ==> (c*a=c*b) = (a=b)"
3.456
3.457  lemma hcomplex_mult_right_cancel:
3.458       "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
3.460 -done
3.462
3.463
3.464  subsection{*Subraction and Division*}
3.465 @@ -515,17 +454,13 @@
3.466  lemma hcomplex_diff:
3.467   "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) =
3.468    Abs_hcomplex(hcomplexrel``{%n. X n - Y n})"
3.469 -apply (unfold hcomplex_diff_def)
3.471 -done
3.473
3.474 -lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)"
3.475 -apply (rule Ring_and_Field.diff_eq_eq)
3.476 -done
3.477 +lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)"
3.478 +by (rule Ring_and_Field.diff_eq_eq)
3.479
3.480  lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z"
3.482 -done
3.484
3.485
3.486  subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*}
3.487 @@ -533,98 +468,77 @@
3.488  lemma hcomplex_of_hypreal:
3.489    "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) =
3.490        Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"
3.491 -apply (unfold hcomplex_of_hypreal_def)
3.492 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.493 -apply auto
3.494 -apply (ultra)
3.496 +apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
3.497  done
3.498
3.499 -lemma inj_hcomplex_of_hypreal: "inj hcomplex_of_hypreal"
3.500 -apply (rule inj_onI)
3.501 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.502 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.503 -apply (auto simp add: hcomplex_of_hypreal)
3.504 +lemma hcomplex_of_hypreal_cancel_iff [iff]:
3.505 +     "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
3.506 +apply (rule eq_Abs_hypreal [of x])
3.507 +apply (rule eq_Abs_hypreal [of y])
3.509  done
3.510
3.511 -lemma hcomplex_of_hypreal_cancel_iff:
3.512 -     "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)"
3.513 -apply (auto dest: inj_hcomplex_of_hypreal [THEN injD])
3.514 -done
3.515 -declare hcomplex_of_hypreal_cancel_iff [iff]
3.516 -
3.517  lemma hcomplex_of_hypreal_minus:
3.518       "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x"
3.519 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.520 -apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
3.521 +apply (rule eq_Abs_hypreal [of x])
3.522 +apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus)
3.523  done
3.524
3.525  lemma hcomplex_of_hypreal_inverse:
3.526       "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)"
3.527 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.528 -apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
3.529 +apply (rule eq_Abs_hypreal [of x])
3.530 +apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse)
3.531  done
3.532
3.534       "hcomplex_of_hypreal x + hcomplex_of_hypreal y =
3.535        hcomplex_of_hypreal (x + y)"
3.536 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.537 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.539 +apply (rule eq_Abs_hypreal [of x])
3.540 +apply (rule eq_Abs_hypreal [of y])
3.542  done
3.543
3.544  lemma hcomplex_of_hypreal_diff:
3.545       "hcomplex_of_hypreal x - hcomplex_of_hypreal y =
3.546        hcomplex_of_hypreal (x - y)"
3.547 -apply (unfold hcomplex_diff_def)
3.549 -done
3.551
3.552  lemma hcomplex_of_hypreal_mult:
3.553       "hcomplex_of_hypreal x * hcomplex_of_hypreal y =
3.554        hcomplex_of_hypreal (x * y)"
3.555 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.556 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.557 -apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult
3.558 -                      complex_of_real_mult)
3.559 +apply (rule eq_Abs_hypreal [of x])
3.560 +apply (rule eq_Abs_hypreal [of y])
3.561 +apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult)
3.562  done
3.563
3.564  lemma hcomplex_of_hypreal_divide:
3.565    "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"
3.566 -apply (unfold hcomplex_divide_def)
3.567 -apply (case_tac "y=0")
3.568 -apply (simp)
3.570 +apply (case_tac "y=0", simp)
3.571  apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric])
3.572 -apply (simp (no_asm) add: hypreal_divide_def)
3.573 -done
3.574 -
3.575 -lemma hcomplex_of_hypreal_one [simp]:
3.576 -      "hcomplex_of_hypreal 1 = 1"
3.577 -apply (unfold hcomplex_one_def)
3.578 -apply (auto simp add: hcomplex_of_hypreal hypreal_one_num)
3.580  done
3.581
3.582 -lemma hcomplex_of_hypreal_zero [simp]:
3.583 -      "hcomplex_of_hypreal 0 = 0"
3.584 -apply (unfold hcomplex_zero_def hypreal_zero_def)
3.585 -apply (auto simp add: hcomplex_of_hypreal)
3.586 -done
3.587 +lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1"
3.588 +by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num)
3.589
3.590 -lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z"
3.591 -apply (rule_tac z = "z" in eq_Abs_hypreal)
3.592 +lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0"
3.593 +by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal)
3.594 +
3.595 +lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z"
3.596 +apply (rule eq_Abs_hypreal [of z])
3.597  apply (auto simp add: hcomplex_of_hypreal hRe)
3.598  done
3.599 -declare hRe_hcomplex_of_hypreal [simp]
3.600
3.601 -lemma hIm_hcomplex_of_hypreal: "hIm(hcomplex_of_hypreal z) = 0"
3.602 -apply (rule_tac z = "z" in eq_Abs_hypreal)
3.603 +lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0"
3.604 +apply (rule eq_Abs_hypreal [of z])
3.605  apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num)
3.606  done
3.607 -declare hIm_hcomplex_of_hypreal [simp]
3.608
3.609 -lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon \<noteq> 0"
3.610 -apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
3.611 -done
3.612 -declare hcomplex_of_hypreal_epsilon_not_zero [simp]
3.613 +lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
3.614 +     "hcomplex_of_hypreal epsilon \<noteq> 0"
3.615 +by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def)
3.616
3.617
3.618  subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*}
3.619 @@ -633,35 +547,27 @@
3.620    "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
3.621        Abs_hypreal(hyprel `` {%n. cmod (X n)})"
3.622
3.623 -apply (unfold hcmod_def)
3.624 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
3.626 +apply (rule_tac f = Abs_hypreal in arg_cong)
3.627  apply (auto, ultra)
3.628  done
3.629
3.630 -lemma hcmod_zero [simp]:
3.631 -      "hcmod(0) = 0"
3.632 -apply (unfold hcomplex_zero_def hypreal_zero_def)
3.633 -apply (auto simp add: hcmod)
3.634 +lemma hcmod_zero [simp]: "hcmod(0) = 0"
3.635 +apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod)
3.636  done
3.637
3.638 -lemma hcmod_one:
3.639 -      "hcmod(1) = 1"
3.640 -apply (unfold hcomplex_one_def)
3.641 -apply (auto simp add: hcmod hypreal_one_num)
3.642 -done
3.643 -declare hcmod_one [simp]
3.644 +lemma hcmod_one [simp]: "hcmod(1) = 1"
3.645 +by (simp add: hcomplex_one_def hcmod hypreal_one_num)
3.646
3.647 -lemma hcmod_hcomplex_of_hypreal: "hcmod(hcomplex_of_hypreal x) = abs x"
3.648 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.649 +lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x"
3.650 +apply (rule eq_Abs_hypreal [of x])
3.651  apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs)
3.652  done
3.653 -declare hcmod_hcomplex_of_hypreal [simp]
3.654
3.655  lemma hcomplex_of_hypreal_abs:
3.656       "hcomplex_of_hypreal (abs x) =
3.657        hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))"
3.658 -apply (simp (no_asm))
3.659 -done
3.660 +by simp
3.661
3.662
3.663  subsection{*Conjugation*}
3.664 @@ -669,232 +575,198 @@
3.665  lemma hcnj:
3.666    "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
3.667     Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})"
3.668 -apply (unfold hcnj_def)
3.669 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.671 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.672  apply (auto, ultra)
3.673  done
3.674
3.675 -lemma inj_hcnj: "inj hcnj"
3.676 -apply (rule inj_onI)
3.677 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.678 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.679 -apply (auto simp add: hcnj)
3.680 +lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)"
3.681 +apply (rule eq_Abs_hcomplex [of x])
3.682 +apply (rule eq_Abs_hcomplex [of y])
3.684 +done
3.685 +
3.686 +lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z"
3.687 +apply (rule eq_Abs_hcomplex [of z])
3.689  done
3.690
3.691 -lemma hcomplex_hcnj_cancel_iff: "(hcnj x = hcnj y) = (x = y)"
3.692 -apply (auto dest: inj_hcnj [THEN injD])
3.693 +lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]:
3.694 +     "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
3.695 +apply (rule eq_Abs_hypreal [of x])
3.696 +apply (simp add: hcnj hcomplex_of_hypreal)
3.697  done
3.698 -declare hcomplex_hcnj_cancel_iff [simp]
3.699 -
3.700 -lemma hcomplex_hcnj_hcnj: "hcnj (hcnj z) = z"
3.701 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.702 -apply (auto simp add: hcnj)
3.703 -done
3.704 -declare hcomplex_hcnj_hcnj [simp]
3.705
3.706 -lemma hcomplex_hcnj_hcomplex_of_hypreal:
3.707 -     "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x"
3.708 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.709 -apply (auto simp add: hcnj hcomplex_of_hypreal)
3.710 +lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z"
3.711 +apply (rule eq_Abs_hcomplex [of z])
3.712 +apply (simp add: hcnj hcmod)
3.713  done
3.714 -declare hcomplex_hcnj_hcomplex_of_hypreal [simp]
3.715 -
3.716 -lemma hcomplex_hmod_hcnj: "hcmod (hcnj z) = hcmod z"
3.717 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.718 -apply (auto simp add: hcnj hcmod)
3.719 -done
3.720 -declare hcomplex_hmod_hcnj [simp]
3.721
3.722  lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z"
3.723 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.724 -apply (auto simp add: hcnj hcomplex_minus complex_cnj_minus)
3.725 +apply (rule eq_Abs_hcomplex [of z])
3.726 +apply (simp add: hcnj hcomplex_minus complex_cnj_minus)
3.727  done
3.728
3.729  lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)"
3.730 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.731 -apply (auto simp add: hcnj hcomplex_inverse complex_cnj_inverse)
3.732 +apply (rule eq_Abs_hcomplex [of z])
3.733 +apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse)
3.734  done
3.735
3.736  lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)"
3.737 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.738 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.740 +apply (rule eq_Abs_hcomplex [of z])
3.741 +apply (rule eq_Abs_hcomplex [of w])
3.743  done
3.744
3.745  lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)"
3.746 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.747 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.748 -apply (auto simp add: hcnj hcomplex_diff complex_cnj_diff)
3.749 +apply (rule eq_Abs_hcomplex [of z])
3.750 +apply (rule eq_Abs_hcomplex [of w])
3.751 +apply (simp add: hcnj hcomplex_diff complex_cnj_diff)
3.752  done
3.753
3.754  lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)"
3.755 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.756 -apply (rule_tac z = "w" in eq_Abs_hcomplex)
3.757 -apply (auto simp add: hcnj hcomplex_mult complex_cnj_mult)
3.758 +apply (rule eq_Abs_hcomplex [of z])
3.759 +apply (rule eq_Abs_hcomplex [of w])
3.760 +apply (simp add: hcnj hcomplex_mult complex_cnj_mult)
3.761  done
3.762
3.763  lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)"
3.764 -apply (unfold hcomplex_divide_def)
3.765 -apply (simp (no_asm) add: hcomplex_hcnj_mult hcomplex_hcnj_inverse)
3.766 -done
3.767 +by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse)
3.768
3.769 -lemma hcnj_one: "hcnj 1 = 1"
3.770 -apply (unfold hcomplex_one_def)
3.771 -apply (simp (no_asm) add: hcnj)
3.772 -done
3.773 -declare hcnj_one [simp]
3.774 +lemma hcnj_one [simp]: "hcnj 1 = 1"
3.775 +by (simp add: hcomplex_one_def hcnj)
3.776
3.777 -lemma hcomplex_hcnj_zero:
3.778 -      "hcnj 0 = 0"
3.779 -apply (unfold hcomplex_zero_def)
3.780 -apply (auto simp add: hcnj)
3.781 +lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0"
3.782 +by (simp add: hcomplex_zero_def hcnj)
3.783 +
3.784 +lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)"
3.785 +apply (rule eq_Abs_hcomplex [of z])
3.786 +apply (simp add: hcomplex_zero_def hcnj)
3.787  done
3.788 -declare hcomplex_hcnj_zero [simp]
3.789 -
3.790 -lemma hcomplex_hcnj_zero_iff: "(hcnj z = 0) = (z = 0)"
3.791 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.792 -apply (auto simp add: hcomplex_zero_def hcnj)
3.793 -done
3.794 -declare hcomplex_hcnj_zero_iff [iff]
3.795
3.796  lemma hcomplex_mult_hcnj:
3.797       "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)"
3.798 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.799 -apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2)
3.800 +apply (rule eq_Abs_hcomplex [of z])
3.802 +                      hypreal_mult complex_mult_cnj numeral_2_eq_2)
3.803  done
3.804
3.805
3.806  subsection{*More Theorems about the Function @{term hcmod}*}
3.807
3.808 -lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)"
3.809 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.810 -apply (auto simp add: hcmod hcomplex_zero_def hypreal_zero_num)
3.811 +lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)"
3.812 +apply (rule eq_Abs_hcomplex [of x])
3.813 +apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num)
3.814  done
3.815 -declare hcomplex_hcmod_eq_zero_cancel [simp]
3.816
3.817 -lemma hcmod_hcomplex_of_hypreal_of_nat:
3.818 +lemma hcmod_hcomplex_of_hypreal_of_nat [simp]:
3.819       "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
3.820 -apply (simp add: abs_if linorder_not_less)
3.821 +apply (simp add: abs_if linorder_not_less)
3.822  done
3.823 -declare hcmod_hcomplex_of_hypreal_of_nat [simp]
3.824
3.825 -lemma hcmod_hcomplex_of_hypreal_of_hypnat:
3.826 +lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]:
3.827       "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
3.828 -apply (simp add: abs_if linorder_not_less)
3.829 +apply (simp add: abs_if linorder_not_less)
3.830  done
3.831 -declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
3.832
3.833 -lemma hcmod_minus: "hcmod (-x) = hcmod(x)"
3.834 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.835 -apply (auto simp add: hcmod hcomplex_minus)
3.836 +lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)"
3.837 +apply (rule eq_Abs_hcomplex [of x])
3.838 +apply (simp add: hcmod hcomplex_minus)
3.839  done
3.840 -declare hcmod_minus [simp]
3.841
3.842  lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2"
3.843 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.844 -apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
3.845 +apply (rule eq_Abs_hcomplex [of z])
3.846 +apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2)
3.847  done
3.848
3.849 -lemma hcmod_ge_zero: "(0::hypreal) \<le> hcmod x"
3.850 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.851 -apply (auto simp add: hcmod hypreal_zero_num hypreal_le)
3.852 +lemma hcmod_ge_zero [simp]: "(0::hypreal) \<le> hcmod x"
3.853 +apply (rule eq_Abs_hcomplex [of x])
3.854 +apply (simp add: hcmod hypreal_zero_num hypreal_le)
3.855  done
3.856 -declare hcmod_ge_zero [simp]
3.857
3.858 -lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x"
3.859 -apply (simp add: abs_if linorder_not_less)
3.860 -done
3.861 -declare hrabs_hcmod_cancel [simp]
3.862 +lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x"
3.863 +by (simp add: abs_if linorder_not_less)
3.864
3.865  lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)"
3.866 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.867 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.868 -apply (auto simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
3.869 +apply (rule eq_Abs_hcomplex [of x])
3.870 +apply (rule eq_Abs_hcomplex [of y])
3.871 +apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult)
3.872  done
3.873
3.875       "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)"
3.876 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.877 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.879 -                      numeral_2_eq_2 realpow_two [symmetric]
3.880 -                 simp del: realpow_Suc)
3.882 -                 hypreal_add [symmetric] hypreal_mult [symmetric]
3.883 +apply (rule eq_Abs_hcomplex [of x])
3.884 +apply (rule eq_Abs_hcomplex [of y])
3.886 +                      numeral_2_eq_2 realpow_two [symmetric]
3.887 +                  del: realpow_Suc)
3.889 +                 hypreal_add [symmetric] hypreal_mult [symmetric]
3.890                   hypreal_of_real_def [symmetric])
3.891  done
3.892
3.893 -lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
3.894 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.895 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.896 -apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
3.897 +lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \<le> hcmod(x * hcnj y)"
3.898 +apply (rule eq_Abs_hcomplex [of x])
3.899 +apply (rule eq_Abs_hcomplex [of y])
3.900 +apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le)
3.901  done
3.902 -declare hcomplex_hRe_mult_hcnj_le_hcmod [simp]
3.903
3.904 -lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) \<le> hcmod(x * y)"
3.905 -apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod)
3.906 +lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: "hRe(x * hcnj y) \<le> hcmod(x * y)"
3.907 +apply (cut_tac x = x and y = y in hcomplex_hRe_mult_hcnj_le_hcmod)
3.909  done
3.910 -declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]
3.911
3.912 -lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
3.913 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.914 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.916 +lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \<le> (hcmod(x) + hcmod(y)) ^ 2"
3.917 +apply (rule eq_Abs_hcomplex [of x])
3.918 +apply (rule eq_Abs_hcomplex [of y])
3.920                        hypreal_le realpow_two [symmetric] numeral_2_eq_2
3.921 -            simp del: realpow_Suc)
3.922 -apply (simp (no_asm) add: numeral_2_eq_2 [symmetric])
3.923 +            del: realpow_Suc)
3.924 +apply (simp add: numeral_2_eq_2 [symmetric])
3.925  done
3.926 -declare hcmod_triangle_squared [simp]
3.927
3.928 -lemma hcmod_triangle_ineq: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
3.929 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.930 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.932 +lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \<le> hcmod(x) + hcmod(y)"
3.933 +apply (rule eq_Abs_hcomplex [of x])
3.934 +apply (rule eq_Abs_hcomplex [of y])
3.936  done
3.937 -declare hcmod_triangle_ineq [simp]
3.938
3.939 -lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b \<le> hcmod a"
3.940 -apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
3.941 +lemma hcmod_triangle_ineq2 [simp]: "hcmod(b + a) - hcmod b \<le> hcmod a"
3.942 +apply (cut_tac x1 = b and y1 = a and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono])
3.944  done
3.945 -declare hcmod_triangle_ineq2 [simp]
3.946
3.947  lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)"
3.948 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.949 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.950 -apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute)
3.951 +apply (rule eq_Abs_hcomplex [of x])
3.952 +apply (rule eq_Abs_hcomplex [of y])
3.953 +apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute)
3.954  done
3.955
3.957       "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s"
3.958 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.959 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.960 -apply (rule_tac z = "r" in eq_Abs_hypreal)
3.961 -apply (rule_tac z = "s" in eq_Abs_hypreal)
3.963 -apply ultra
3.964 +apply (rule eq_Abs_hcomplex [of x])
3.965 +apply (rule eq_Abs_hcomplex [of y])
3.966 +apply (rule eq_Abs_hypreal [of r])
3.967 +apply (rule eq_Abs_hypreal [of s])
3.970  done
3.971
3.972  lemma hcmod_mult_less:
3.973       "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s"
3.974 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.975 -apply (rule_tac z = "y" in eq_Abs_hcomplex)
3.976 -apply (rule_tac z = "r" in eq_Abs_hypreal)
3.977 -apply (rule_tac z = "s" in eq_Abs_hypreal)
3.978 -apply (auto simp add: hcmod hypreal_mult hypreal_less hcomplex_mult)
3.979 -apply ultra
3.980 +apply (rule eq_Abs_hcomplex [of x])
3.981 +apply (rule eq_Abs_hcomplex [of y])
3.982 +apply (rule eq_Abs_hypreal [of r])
3.983 +apply (rule eq_Abs_hypreal [of s])
3.984 +apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra)
3.985  apply (auto intro: complex_mod_mult_less)
3.986  done
3.987
3.988 -lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
3.989 -apply (rule_tac z = "a" in eq_Abs_hcomplex)
3.990 -apply (rule_tac z = "b" in eq_Abs_hcomplex)
3.992 +lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \<le> hcmod(a + b)"
3.993 +apply (rule eq_Abs_hcomplex [of a])
3.994 +apply (rule eq_Abs_hcomplex [of b])
3.996  done
3.997 -declare hcmod_diff_ineq [simp]
3.998 -
3.999
3.1000
3.1001  subsection{*A Few Nonlinear Theorems*}
3.1002 @@ -903,42 +775,32 @@
3.1003    "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow
3.1004     Abs_hypnat(hypnatrel``{%n. Y n}) =
3.1005     Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})"
3.1006 -apply (unfold hcpow_def)
3.1007 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.1009 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.1010  apply (auto, ultra)
3.1011  done
3.1012
3.1013  lemma hcomplex_of_hypreal_hyperpow:
3.1014       "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n"
3.1015 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1016 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1017 -apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
3.1018 +apply (rule eq_Abs_hypreal [of x])
3.1019 +apply (rule eq_Abs_hypnat [of n])
3.1020 +apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow)
3.1021  done
3.1022
3.1023  lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n"
3.1024 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.1025 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1026 -apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow)
3.1027 +apply (rule eq_Abs_hcomplex [of x])
3.1028 +apply (rule eq_Abs_hypnat [of n])
3.1029 +apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow)
3.1030  done
3.1031
3.1032  lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)"
3.1033 -apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO)
3.1034 +apply (case_tac "x = 0", simp)
3.1035  apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1])
3.1036  apply (auto simp add: hcmod_mult [symmetric])
3.1037  done
3.1038
3.1039 -lemma hcmod_divide:
3.1040 -      "hcmod(x/y) = hcmod(x)/(hcmod y)"
3.1041 -apply (unfold hcomplex_divide_def hypreal_divide_def)
3.1042 -apply (auto simp add: hcmod_mult hcmod_hcomplex_inverse)
3.1043 -done
3.1044 -
3.1045 -lemma hcomplex_inverse_divide:
3.1046 -      "inverse(x/y) = y/(x::hcomplex)"
3.1047 -apply (unfold hcomplex_divide_def)
3.1048 -apply (auto simp add: inverse_mult_distrib hcomplex_mult_commute)
3.1049 -done
3.1050 -declare hcomplex_inverse_divide [simp]
3.1051 +lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)"
3.1052 +by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse)
3.1053
3.1054
3.1055  subsection{*Exponentiation*}
3.1056 @@ -974,73 +836,56 @@
3.1057
3.1058  lemma hcomplexpow_minus:
3.1059       "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))"
3.1060 -apply (induct_tac "n")
3.1061 -apply auto
3.1062 -done
3.1063 +by (induct_tac "n", auto)
3.1064
3.1065  lemma hcpow_minus:
3.1066       "(-x::hcomplex) hcpow n =
3.1067        (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))"
3.1068 -apply (rule_tac z = "x" in eq_Abs_hcomplex)
3.1069 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1070 -apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus)
3.1071 -apply ultra
3.1072 -apply (auto simp add: complexpow_minus)
3.1073 -apply ultra
3.1074 +apply (rule eq_Abs_hcomplex [of x])
3.1075 +apply (rule eq_Abs_hypnat [of n])
3.1076 +apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra)
3.1077 +apply (auto simp add: complexpow_minus, ultra)
3.1078  done
3.1079
3.1080  lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)"
3.1081 -apply (rule_tac z = "r" in eq_Abs_hcomplex)
3.1082 -apply (rule_tac z = "s" in eq_Abs_hcomplex)
3.1083 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1084 -apply (auto simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
3.1085 +apply (rule eq_Abs_hcomplex [of r])
3.1086 +apply (rule eq_Abs_hcomplex [of s])
3.1087 +apply (rule eq_Abs_hypnat [of n])
3.1088 +apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib)
3.1089  done
3.1090
3.1091  lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0"
3.1092 -apply (unfold hcomplex_zero_def hypnat_one_def)
3.1093 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1095 +apply (simp add: hcomplex_zero_def hypnat_one_def)
3.1096 +apply (rule eq_Abs_hypnat [of n])
3.1098  done
3.1099
3.1100  lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0"
3.1101 -apply (unfold hSuc_def)
3.1102 -apply (simp (no_asm))
3.1103 -done
3.1105
3.1106  lemma hcpow_not_zero [simp,intro]: "r \<noteq> 0 ==> r hcpow n \<noteq> (0::hcomplex)"
3.1107 -apply (rule_tac z = "r" in eq_Abs_hcomplex)
3.1108 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1109 -apply (auto simp add: hcpow hcomplex_zero_def)
3.1110 -apply ultra
3.1111 +apply (rule eq_Abs_hcomplex [of r])
3.1112 +apply (rule eq_Abs_hypnat [of n])
3.1113 +apply (auto simp add: hcpow hcomplex_zero_def, ultra)
3.1114  done
3.1115
3.1116  lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0"
3.1117 -apply (blast intro: ccontr dest: hcpow_not_zero)
3.1118 -done
3.1119 +by (blast intro: ccontr dest: hcpow_not_zero)
3.1120
3.1121 -lemma hcomplex_i_mult_eq: "iii * iii = - 1"
3.1122 -apply (unfold iii_def)
3.1123 -apply (auto simp add: hcomplex_mult hcomplex_one_def hcomplex_minus)
3.1124 -done
3.1125 -declare hcomplex_i_mult_eq [simp]
3.1126 +lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1"
3.1127 +by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus)
3.1128
3.1129 -lemma hcomplexpow_i_squared: "iii ^ 2 = - 1"
3.1130 -apply (simp (no_asm) add: numeral_2_eq_2)
3.1131 -done
3.1132 -declare hcomplexpow_i_squared [simp]
3.1133 +lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1"
3.1135
3.1136 -lemma hcomplex_i_not_zero: "iii \<noteq> 0"
3.1137 -apply (unfold iii_def hcomplex_zero_def)
3.1138 -apply auto
3.1139 -done
3.1140 -declare hcomplex_i_not_zero [simp]
3.1141 +lemma hcomplex_i_not_zero [simp]: "iii \<noteq> 0"
3.1142 +by (simp add: iii_def hcomplex_zero_def)
3.1143
3.1144  lemma hcomplex_divide:
3.1145    "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) =
3.1146     Abs_hcomplex(hcomplexrel``{%n. X n / Y n})"
3.1147 -apply (unfold hcomplex_divide_def complex_divide_def)
3.1148 -apply (auto simp add: hcomplex_inverse hcomplex_mult)
3.1149 -done
3.1150 +by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult)
3.1151 +
3.1152
3.1153
3.1154  subsection{*The Function @{term hsgn}*}
3.1155 @@ -1048,244 +893,210 @@
3.1156  lemma hsgn:
3.1157    "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
3.1158        Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})"
3.1159 -apply (unfold hsgn_def)
3.1160 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.1162 +apply (rule_tac f = Abs_hcomplex in arg_cong)
3.1163  apply (auto, ultra)
3.1164  done
3.1165
3.1166 -lemma hsgn_zero: "hsgn 0 = 0"
3.1167 -apply (unfold hcomplex_zero_def)
3.1168 -apply (simp (no_asm) add: hsgn)
3.1169 -done
3.1170 -declare hsgn_zero [simp]
3.1171 +lemma hsgn_zero [simp]: "hsgn 0 = 0"
3.1172 +by (simp add: hcomplex_zero_def hsgn)
3.1173
3.1174 -
3.1175 -lemma hsgn_one: "hsgn 1 = 1"
3.1176 -apply (unfold hcomplex_one_def)
3.1177 -apply (simp (no_asm) add: hsgn)
3.1178 -done
3.1179 -declare hsgn_one [simp]
3.1180 +lemma hsgn_one [simp]: "hsgn 1 = 1"
3.1181 +by (simp add: hcomplex_one_def hsgn)
3.1182
3.1183  lemma hsgn_minus: "hsgn (-z) = - hsgn(z)"
3.1184 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.1185 -apply (auto simp add: hsgn hcomplex_minus sgn_minus)
3.1186 +apply (rule eq_Abs_hcomplex [of z])
3.1187 +apply (simp add: hsgn hcomplex_minus sgn_minus)
3.1188  done
3.1189
3.1190  lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)"
3.1191 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.1192 -apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
3.1193 +apply (rule eq_Abs_hcomplex [of z])
3.1194 +apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq)
3.1195  done
3.1196
3.1197  lemma lemma_hypreal_P_EX2:
3.1198       "(\<exists>(x::hypreal) y. P x y) =
3.1199        (\<exists>f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))"
3.1200  apply auto
3.1201 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1202 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1203 -apply auto
3.1204 +apply (rule_tac z = x in eq_Abs_hypreal)
3.1205 +apply (rule_tac z = y in eq_Abs_hypreal, auto)
3.1206  done
3.1207
3.1208  lemma complex_split2:
3.1209       "\<forall>(n::nat). \<exists>x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)"
3.1210 -apply (blast intro: complex_split)
3.1211 -done
3.1212 +by (blast intro: complex_split)
3.1213
3.1214  (* Interesting proof! *)
3.1215  lemma hcomplex_split:
3.1216       "\<exists>x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)"
3.1217 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.1218 +apply (rule eq_Abs_hcomplex [of z])
3.1220 -apply (cut_tac z = "x" in complex_split2)
3.1221 +apply (cut_tac z = x in complex_split2)
3.1222  apply (drule choice, safe)+
3.1223 -apply (rule_tac x = "f" in exI)
3.1224 -apply (rule_tac x = "fa" in exI)
3.1225 -apply auto
3.1226 +apply (rule_tac x = f in exI)
3.1227 +apply (rule_tac x = fa in exI, auto)
3.1228  done
3.1229
3.1230 -lemma hRe_hcomplex_i:
3.1231 +lemma hRe_hcomplex_i [simp]:
3.1232       "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x"
3.1233 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1234 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1235 +apply (rule eq_Abs_hypreal [of x])
3.1236 +apply (rule eq_Abs_hypreal [of y])
3.1238  done
3.1239 -declare hRe_hcomplex_i [simp]
3.1240
3.1241 -lemma hIm_hcomplex_i:
3.1242 +lemma hIm_hcomplex_i [simp]:
3.1243       "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y"
3.1244 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1245 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1247 +apply (rule eq_Abs_hypreal [of x])
3.1248 +apply (rule eq_Abs_hypreal [of y])
3.1250  done
3.1251 -declare hIm_hcomplex_i [simp]
3.1252
3.1253  lemma hcmod_i:
3.1254       "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) =
3.1255        ( *f* sqrt) (x ^ 2 + y ^ 2)"
3.1256 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1257 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1259 +apply (rule eq_Abs_hypreal [of x])
3.1260 +apply (rule eq_Abs_hypreal [of y])
3.1262  done
3.1263
3.1264  lemma hcomplex_eq_hRe_eq:
3.1265       "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
3.1266        hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
3.1267         ==> xa = xb"
3.1268 -apply (unfold iii_def)
3.1269 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
3.1270 -apply (rule_tac z = "ya" in eq_Abs_hypreal)
3.1271 -apply (rule_tac z = "xb" in eq_Abs_hypreal)
3.1272 -apply (rule_tac z = "yb" in eq_Abs_hypreal)
3.1274 -apply (ultra)
3.1276 +apply (rule eq_Abs_hypreal [of xa])
3.1277 +apply (rule eq_Abs_hypreal [of ya])
3.1278 +apply (rule eq_Abs_hypreal [of xb])
3.1279 +apply (rule eq_Abs_hypreal [of yb])
3.1281  done
3.1282
3.1283  lemma hcomplex_eq_hIm_eq:
3.1284       "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
3.1285        hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb
3.1286         ==> ya = yb"
3.1287 -apply (unfold iii_def)
3.1288 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
3.1289 -apply (rule_tac z = "ya" in eq_Abs_hypreal)
3.1290 -apply (rule_tac z = "xb" in eq_Abs_hypreal)
3.1291 -apply (rule_tac z = "yb" in eq_Abs_hypreal)
3.1293 -apply (ultra)
3.1295 +apply (rule eq_Abs_hypreal [of xa])
3.1296 +apply (rule eq_Abs_hypreal [of ya])
3.1297 +apply (rule eq_Abs_hypreal [of xb])
3.1298 +apply (rule eq_Abs_hypreal [of yb])
3.1300  done
3.1301
3.1302 -lemma hcomplex_eq_cancel_iff:
3.1303 +lemma hcomplex_eq_cancel_iff [simp]:
3.1304       "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya =
3.1305         hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) =
3.1306        ((xa = xb) & (ya = yb))"
3.1307 -apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
3.1308 -done
3.1309 -declare hcomplex_eq_cancel_iff [simp]
3.1310 +by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq)
3.1311
3.1312 -lemma hcomplex_eq_cancel_iffA:
3.1313 +lemma hcomplex_eq_cancel_iffA [iff]:
3.1314       "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
3.1315 -       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))"
3.1316 -apply (auto simp add: hcomplex_mult_commute)
3.1317 +       hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
3.1319  done
3.1320 -declare hcomplex_eq_cancel_iffA [iff]
3.1321
3.1322 -lemma hcomplex_eq_cancel_iffB:
3.1323 +lemma hcomplex_eq_cancel_iffB [iff]:
3.1324       "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii =
3.1325         hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))"
3.1326 -apply (auto simp add: hcomplex_mult_commute)
3.1328  done
3.1329 -declare hcomplex_eq_cancel_iffB [iff]
3.1330
3.1331 -lemma hcomplex_eq_cancel_iffC:
3.1332 +lemma hcomplex_eq_cancel_iffC [iff]:
3.1333       "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya  =
3.1334         hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))"
3.1335 -apply (auto simp add: hcomplex_mult_commute)
3.1337  done
3.1338 -declare hcomplex_eq_cancel_iffC [iff]
3.1339
3.1340 -lemma hcomplex_eq_cancel_iff2:
3.1341 +lemma hcomplex_eq_cancel_iff2 [simp]:
3.1342       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
3.1343        hcomplex_of_hypreal xa) = (x = xa & y = 0)"
3.1344 -apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff)
3.1345 +apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff)
3.1346  apply (simp del: hcomplex_eq_cancel_iff)
3.1347  done
3.1348 -declare hcomplex_eq_cancel_iff2 [simp]
3.1349
3.1350 -lemma hcomplex_eq_cancel_iff2a:
3.1351 +lemma hcomplex_eq_cancel_iff2a [simp]:
3.1352       "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
3.1353        hcomplex_of_hypreal xa) = (x = xa & y = 0)"
3.1354 -apply (auto simp add: hcomplex_mult_commute)
3.1356  done
3.1357 -declare hcomplex_eq_cancel_iff2a [simp]
3.1358
3.1359 -lemma hcomplex_eq_cancel_iff3:
3.1360 +lemma hcomplex_eq_cancel_iff3 [simp]:
3.1361       "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y =
3.1362        iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
3.1363 -apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff)
3.1364 +apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff)
3.1365  apply (simp del: hcomplex_eq_cancel_iff)
3.1366  done
3.1367 -declare hcomplex_eq_cancel_iff3 [simp]
3.1368
3.1369 -lemma hcomplex_eq_cancel_iff3a:
3.1370 +lemma hcomplex_eq_cancel_iff3a [simp]:
3.1371       "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii =
3.1372        iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)"
3.1373 -apply (auto simp add: hcomplex_mult_commute)
3.1375  done
3.1376 -declare hcomplex_eq_cancel_iff3a [simp]
3.1377
3.1378  lemma hcomplex_split_hRe_zero:
3.1379       "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
3.1380        ==> x = 0"
3.1381 -apply (unfold iii_def)
3.1382 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1383 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1385 -apply ultra
3.1386 -apply (auto simp add: complex_split_Re_zero)
3.1388 +apply (rule eq_Abs_hypreal [of x])
3.1389 +apply (rule eq_Abs_hypreal [of y])
3.1392  done
3.1393
3.1394  lemma hcomplex_split_hIm_zero:
3.1395       "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0
3.1396        ==> y = 0"
3.1397 -apply (unfold iii_def)
3.1398 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1399 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1401 -apply ultra
3.1402 -apply (auto simp add: complex_split_Im_zero)
3.1404 +apply (rule eq_Abs_hypreal [of x])
3.1405 +apply (rule eq_Abs_hypreal [of y])
3.1408  done
3.1409
3.1410 -lemma hRe_hsgn: "hRe(hsgn z) = hRe(z)/hcmod z"
3.1411 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.1412 -apply (auto simp add: hsgn hcmod hRe hypreal_divide)
3.1413 +lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z"
3.1414 +apply (rule eq_Abs_hcomplex [of z])
3.1415 +apply (simp add: hsgn hcmod hRe hypreal_divide)
3.1416  done
3.1417 -declare hRe_hsgn [simp]
3.1418
3.1419 -lemma hIm_hsgn: "hIm(hsgn z) = hIm(z)/hcmod z"
3.1420 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.1421 -apply (auto simp add: hsgn hcmod hIm hypreal_divide)
3.1422 +lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z"
3.1423 +apply (rule eq_Abs_hcomplex [of z])
3.1424 +apply (simp add: hsgn hcmod hIm hypreal_divide)
3.1425  done
3.1426 -declare hIm_hsgn [simp]
3.1427
3.1429 -     "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
3.1430 +lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)"
3.1431  apply (auto intro: real_sum_squares_cancel)
3.1432  done
3.1434
3.1435  lemma hcomplex_inverse_complex_split:
3.1436       "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) =
3.1437        hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) -
3.1438        iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))"
3.1439 -apply (rule_tac z = "x" in eq_Abs_hypreal)
3.1440 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1441 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2)
3.1442 +apply (rule eq_Abs_hypreal [of x])
3.1443 +apply (rule eq_Abs_hypreal [of y])
3.1445 +done
3.1446 +
3.1447 +lemma hRe_mult_i_eq[simp]:
3.1448 +    "hRe (iii * hcomplex_of_hypreal y) = 0"
3.1450 +apply (rule eq_Abs_hypreal [of y])
3.1451 +apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
3.1452  done
3.1453
3.1454 -lemma hRe_mult_i_eq:
3.1455 -    "hRe (iii * hcomplex_of_hypreal y) = 0"
3.1456 -apply (unfold iii_def)
3.1457 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1458 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num)
3.1459 -done
3.1460 -declare hRe_mult_i_eq [simp]
3.1461 -
3.1462 -lemma hIm_mult_i_eq:
3.1463 +lemma hIm_mult_i_eq [simp]:
3.1464      "hIm (iii * hcomplex_of_hypreal y) = y"
3.1465 -apply (unfold iii_def)
3.1466 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1467 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
3.1469 +apply (rule eq_Abs_hypreal [of y])
3.1470 +apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num)
3.1471  done
3.1472 -declare hIm_mult_i_eq [simp]
3.1473
3.1474 -lemma hcmod_mult_i: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
3.1475 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1476 -apply (auto simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
3.1477 +lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y"
3.1478 +apply (rule eq_Abs_hypreal [of y])
3.1479 +apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult)
3.1480  done
3.1481 -declare hcmod_mult_i [simp]
3.1482
3.1483 -lemma hcmod_mult_i2: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
3.1484 -apply (auto simp add: hcomplex_mult_commute)
3.1485 -done
3.1486 -declare hcmod_mult_i2 [simp]
3.1487 +lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y"
3.1489
3.1490  (*---------------------------------------------------------------------------*)
3.1491  (*  harg                                                                     *)
3.1492 @@ -1295,37 +1106,35 @@
3.1493    "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) =
3.1494        Abs_hypreal(hyprel `` {%n. arg (X n)})"
3.1495
3.1496 -apply (unfold harg_def)
3.1497 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
3.1499 +apply (rule_tac f = Abs_hypreal in arg_cong)
3.1500  apply (auto, ultra)
3.1501  done
3.1502
3.1503  lemma cos_harg_i_mult_zero_pos:
3.1504       "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
3.1505 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1506 -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult
3.1507 -                hypreal_zero_num hypreal_less starfun harg)
3.1508 -apply (ultra)
3.1509 +apply (rule eq_Abs_hypreal [of y])
3.1510 +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
3.1511 +                hypreal_zero_num hypreal_less starfun harg, ultra)
3.1512  done
3.1513
3.1514  lemma cos_harg_i_mult_zero_neg:
3.1515       "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
3.1516 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1517 -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult
3.1518 -                      hypreal_zero_num hypreal_less starfun harg)
3.1519 -apply (ultra)
3.1520 +apply (rule eq_Abs_hypreal [of y])
3.1521 +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult
3.1522 +                      hypreal_zero_num hypreal_less starfun harg, ultra)
3.1523  done
3.1524
3.1525  lemma cos_harg_i_mult_zero [simp]:
3.1526       "y \<noteq> 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0"
3.1527 -apply (cut_tac x = "y" and y = "0" in linorder_less_linear)
3.1528 +apply (cut_tac x = y and y = 0 in linorder_less_linear)
3.1529  apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg)
3.1530  done
3.1531
3.1532  lemma hcomplex_of_hypreal_zero_iff [simp]:
3.1533       "(hcomplex_of_hypreal y = 0) = (y = 0)"
3.1534 -apply (rule_tac z = "y" in eq_Abs_hypreal)
3.1535 -apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
3.1536 +apply (rule eq_Abs_hypreal [of y])
3.1537 +apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def)
3.1538  done
3.1539
3.1540
3.1541 @@ -1340,331 +1149,259 @@
3.1542  lemma hcomplex_split_polar:
3.1543    "\<exists>r a. z = hcomplex_of_hypreal r *
3.1544     (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))"
3.1545 -apply (rule_tac z = "z" in eq_Abs_hcomplex)
3.1547 -apply (cut_tac z = "x" in complex_split_polar2)
3.1548 +apply (rule eq_Abs_hcomplex [of z])
3.1550 +apply (cut_tac z = x in complex_split_polar2)
3.1551  apply (drule choice, safe)+
3.1552 -apply (rule_tac x = "f" in exI)
3.1553 -apply (rule_tac x = "fa" in exI)
3.1554 -apply auto
3.1555 +apply (rule_tac x = f in exI)
3.1556 +apply (rule_tac x = fa in exI, auto)
3.1557  done
3.1558
3.1559  lemma hcis:
3.1560    "hcis (Abs_hypreal(hyprel `` {%n. X n})) =
3.1561        Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"
3.1562 -apply (unfold hcis_def)
3.1563 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
3.1564 -apply auto
3.1565 -apply (ultra)
3.1567 +apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra)
3.1568  done
3.1569
3.1570  lemma hcis_eq:
3.1571     "hcis a =
3.1572      (hcomplex_of_hypreal(( *f* cos) a) +
3.1573      iii * hcomplex_of_hypreal(( *f* sin) a))"
3.1574 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1575 -apply (auto simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
3.1576 +apply (rule eq_Abs_hypreal [of a])
3.1578  done
3.1579
3.1580  lemma hrcis:
3.1581    "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) =
3.1582        Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})"
3.1583 -apply (unfold hrcis_def)
3.1584 -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
3.1585 -done
3.1586 +by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def)
3.1587
3.1588  lemma hrcis_Ex: "\<exists>r a. z = hrcis r a"
3.1589 -apply (simp (no_asm) add: hrcis_def hcis_eq)
3.1590 +apply (simp add: hrcis_def hcis_eq)
3.1591  apply (rule hcomplex_split_polar)
3.1592  done
3.1593
3.1594 -lemma hRe_hcomplex_polar:
3.1595 +lemma hRe_hcomplex_polar [simp]:
3.1596       "hRe(hcomplex_of_hypreal r *
3.1597        (hcomplex_of_hypreal(( *f* cos) a) +
3.1598         iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a"
3.1599 -apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
3.1600 -done
3.1601 -declare hRe_hcomplex_polar [simp]
3.1602 +by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
3.1603
3.1604 -lemma hRe_hrcis: "hRe(hrcis r a) = r * ( *f* cos) a"
3.1605 -apply (unfold hrcis_def)
3.1606 -apply (auto simp add: hcis_eq)
3.1607 -done
3.1608 -declare hRe_hrcis [simp]
3.1609 +lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a"
3.1610 +by (simp add: hrcis_def hcis_eq)
3.1611
3.1612 -lemma hIm_hcomplex_polar:
3.1613 +lemma hIm_hcomplex_polar [simp]:
3.1614       "hIm(hcomplex_of_hypreal r *
3.1615        (hcomplex_of_hypreal(( *f* cos) a) +
3.1616         iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a"
3.1617 -apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
3.1618 -done
3.1619 -declare hIm_hcomplex_polar [simp]
3.1620 +by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac)
3.1621
3.1622 -lemma hIm_hrcis: "hIm(hrcis r a) = r * ( *f* sin) a"
3.1623 -apply (unfold hrcis_def)
3.1624 -apply (auto simp add: hcis_eq)
3.1625 -done
3.1626 -declare hIm_hrcis [simp]
3.1627 +lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a"
3.1628 +by (simp add: hrcis_def hcis_eq)
3.1629
3.1630 -lemma hcmod_complex_polar:
3.1631 +lemma hcmod_complex_polar [simp]:
3.1632       "hcmod (hcomplex_of_hypreal r *
3.1633        (hcomplex_of_hypreal(( *f* cos) a) +
3.1634         iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r"
3.1635 -apply (rule_tac z = "r" in eq_Abs_hypreal)
3.1636 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1637 -apply (auto simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
3.1638 +apply (rule eq_Abs_hypreal [of r])
3.1639 +apply (rule eq_Abs_hypreal [of a])
3.1641  done
3.1642 -declare hcmod_complex_polar [simp]
3.1643
3.1644 -lemma hcmod_hrcis: "hcmod(hrcis r a) = abs r"
3.1645 -apply (unfold hrcis_def)
3.1646 -apply (auto simp add: hcis_eq)
3.1647 -done
3.1648 -declare hcmod_hrcis [simp]
3.1649 +lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r"
3.1650 +by (simp add: hrcis_def hcis_eq)
3.1651
3.1652  (*---------------------------------------------------------------------------*)
3.1653  (*  (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b)                *)
3.1654  (*---------------------------------------------------------------------------*)
3.1655
3.1656  lemma hcis_hrcis_eq: "hcis a = hrcis 1 a"
3.1657 -apply (unfold hrcis_def)
3.1658 -apply (simp (no_asm))
3.1659 -done
3.1661  declare hcis_hrcis_eq [symmetric, simp]
3.1662
3.1663  lemma hrcis_mult:
3.1664    "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)"
3.1665 -apply (unfold hrcis_def)
3.1666 -apply (rule_tac z = "r1" in eq_Abs_hypreal)
3.1667 -apply (rule_tac z = "r2" in eq_Abs_hypreal)
3.1668 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1669 -apply (rule_tac z = "b" in eq_Abs_hypreal)
3.1671 -                      hcomplex_mult cis_mult [symmetric]
3.1673 +apply (rule eq_Abs_hypreal [of r1])
3.1674 +apply (rule eq_Abs_hypreal [of r2])
3.1675 +apply (rule eq_Abs_hypreal [of a])
3.1676 +apply (rule eq_Abs_hypreal [of b])
3.1678 +                      hcomplex_mult cis_mult [symmetric]
3.1679                        complex_of_real_mult [symmetric])
3.1680  done
3.1681
3.1682  lemma hcis_mult: "hcis a * hcis b = hcis (a + b)"
3.1683 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1684 -apply (rule_tac z = "b" in eq_Abs_hypreal)
3.1686 +apply (rule eq_Abs_hypreal [of a])
3.1687 +apply (rule eq_Abs_hypreal [of b])
3.1689  done
3.1690
3.1691 -lemma hcis_zero:
3.1692 -  "hcis 0 = 1"
3.1693 -apply (unfold hcomplex_one_def)
3.1694 -apply (auto simp add: hcis hypreal_zero_num)
3.1695 -done
3.1696 -declare hcis_zero [simp]
3.1697 +lemma hcis_zero [simp]: "hcis 0 = 1"
3.1698 +by (simp add: hcomplex_one_def hcis hypreal_zero_num)
3.1699
3.1700 -lemma hrcis_zero_mod:
3.1701 -  "hrcis 0 a = 0"
3.1702 -apply (unfold hcomplex_zero_def)
3.1703 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1704 -apply (auto simp add: hrcis hypreal_zero_num)
3.1705 +lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0"
3.1707 +apply (rule eq_Abs_hypreal [of a])
3.1708 +apply (simp add: hrcis hypreal_zero_num)
3.1709  done
3.1710 -declare hrcis_zero_mod [simp]
3.1711
3.1712 -lemma hrcis_zero_arg: "hrcis r 0 = hcomplex_of_hypreal r"
3.1713 -apply (rule_tac z = "r" in eq_Abs_hypreal)
3.1714 -apply (auto simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
3.1715 +lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r"
3.1716 +apply (rule eq_Abs_hypreal [of r])
3.1717 +apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal)
3.1718  done
3.1719 -declare hrcis_zero_arg [simp]
3.1720
3.1721 -lemma hcomplex_i_mult_minus: "iii * (iii * x) = - x"
3.1722 -apply (simp (no_asm) add: hcomplex_mult_assoc [symmetric])
3.1723 -done
3.1724 -declare hcomplex_i_mult_minus [simp]
3.1725 +lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x"
3.1726 +by (simp add: hcomplex_mult_assoc [symmetric])
3.1727
3.1728 -lemma hcomplex_i_mult_minus2: "iii * iii * x = - x"
3.1729 -apply (simp (no_asm))
3.1730 -done
3.1731 -declare hcomplex_i_mult_minus2 [simp]
3.1732 +lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x"
3.1733 +by simp
3.1734
3.1735  lemma hcis_hypreal_of_nat_Suc_mult:
3.1736     "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)"
3.1737 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1738 -apply (auto simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
3.1739 +apply (rule eq_Abs_hypreal [of a])
3.1740 +apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
3.1741  done
3.1742
3.1743  lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)"
3.1744  apply (induct_tac "n")
3.1745 -apply (auto simp add: hcis_hypreal_of_nat_Suc_mult)
3.1747  done
3.1748
3.1749  lemma hcis_hypreal_of_hypnat_Suc_mult:
3.1750       "hcis (hypreal_of_hypnat (n + 1) * a) =
3.1751        hcis a * hcis (hypreal_of_hypnat n * a)"
3.1752 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1753 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1754 -apply (auto simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
3.1755 +apply (rule eq_Abs_hypreal [of a])
3.1756 +apply (rule eq_Abs_hypnat [of n])
3.1758  done
3.1759
3.1760  lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)"
3.1761 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1762 -apply (rule_tac z = "n" in eq_Abs_hypnat)
3.1763 -apply (auto simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
3.1764 +apply (rule eq_Abs_hypreal [of a])
3.1765 +apply (rule eq_Abs_hypnat [of n])
3.1766 +apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre)
3.1767  done
3.1768
3.1769  lemma DeMoivre2:
3.1770    "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)"
3.1771 -apply (unfold hrcis_def)
3.1772 -apply (auto simp add: power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
3.1773 +apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow)
3.1774  done
3.1775
3.1776  lemma DeMoivre2_ext:
3.1777    "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)"
3.1778 -apply (unfold hrcis_def)
3.1779 -apply (auto simp add: hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
3.1780 +apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow)
3.1781 +done
3.1782 +
3.1783 +lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)"
3.1784 +apply (rule eq_Abs_hypreal [of a])
3.1785 +apply (simp add: hcomplex_inverse hcis hypreal_minus)
3.1786  done
3.1787
3.1788 -lemma hcis_inverse: "inverse(hcis a) = hcis (-a)"
3.1789 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1790 -apply (auto simp add: hcomplex_inverse hcis hypreal_minus)
3.1791 +lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
3.1792 +apply (rule eq_Abs_hypreal [of a])
3.1793 +apply (rule eq_Abs_hypreal [of r])
3.1794 +apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra)
3.1796  done
3.1797 -declare hcis_inverse [simp]
3.1798
3.1799 -lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)"
3.1800 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1801 -apply (rule_tac z = "r" in eq_Abs_hypreal)
3.1802 -apply (auto simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse)
3.1803 -apply (ultra)
3.1804 -apply (unfold real_divide_def)
3.1805 -apply (auto simp add: INVERSE_ZERO)
3.1806 +lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a"
3.1807 +apply (rule eq_Abs_hypreal [of a])
3.1808 +apply (simp add: hcis starfun hRe)
3.1809  done
3.1810
3.1811 -lemma hRe_hcis: "hRe(hcis a) = ( *f* cos) a"
3.1812 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1813 -apply (auto simp add: hcis starfun hRe)
3.1814 +lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a"
3.1815 +apply (rule eq_Abs_hypreal [of a])
3.1816 +apply (simp add: hcis starfun hIm)
3.1817  done
3.1818 -declare hRe_hcis [simp]
3.1819
3.1820 -lemma hIm_hcis: "hIm(hcis a) = ( *f* sin) a"
3.1821 -apply (rule_tac z = "a" in eq_Abs_hypreal)
3.1822 -apply (auto simp add: hcis starfun hIm)
3.1823 -done
3.1824 -declare hIm_hcis [simp]
3.1825 -
3.1826 -lemma cos_n_hRe_hcis_pow_n:
3.1827 -     "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
3.1828 -apply (auto simp add: NSDeMoivre)
3.1829 +lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
3.1831  done
3.1832
3.1833 -lemma sin_n_hIm_hcis_pow_n:
3.1834 -     "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
3.1835 -apply (auto simp add: NSDeMoivre)
3.1836 +lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)"
3.1838  done
3.1839
3.1840 -lemma cos_n_hRe_hcis_hcpow_n:
3.1841 -     "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
3.1842 -apply (auto simp add: NSDeMoivre_ext)
3.1843 +lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)"
3.1845  done
3.1846
3.1847 -lemma sin_n_hIm_hcis_hcpow_n:
3.1848 -     "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
3.1849 -apply (auto simp add: NSDeMoivre_ext)
3.1850 +lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)"
3.1852  done
3.1853
3.1854  lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)"
3.1855 -apply (unfold hexpi_def)
3.1856 -apply (rule_tac z = "a" in eq_Abs_hcomplex)
3.1857 -apply (rule_tac z = "b" in eq_Abs_hcomplex)
3.1860 +apply (rule eq_Abs_hcomplex [of a])
3.1861 +apply (rule eq_Abs_hcomplex [of b])
3.1863  done
3.1864
3.1865
3.1866 -subsection{*@{term hcomplex_of_complex}: the Injection from
3.1867 +subsection{*@{term hcomplex_of_complex}: the Injection from
3.1868    type @{typ complex} to to @{typ hcomplex}*}
3.1869
3.1870  lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)"
3.1871 -apply (rule inj_onI , rule ccontr)
3.1872 -apply (auto simp add: hcomplex_of_complex_def)
3.1873 +apply (rule inj_onI, rule ccontr)
3.1875  done
3.1876
3.1877  lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii"
3.1878 -apply (unfold iii_def hcomplex_of_complex_def)
3.1879 -apply (simp (no_asm))
3.1880 -done
3.1881 +by (simp add: iii_def hcomplex_of_complex_def)
3.1882
3.1885       "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
3.1886 -apply (unfold hcomplex_of_complex_def)
3.1888 -done
3.1891
3.1892 -lemma hcomplex_of_complex_mult:
3.1893 +lemma hcomplex_of_complex_mult [simp]:
3.1894       "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2"
3.1895 -apply (unfold hcomplex_of_complex_def)
3.1896 -apply (simp (no_asm) add: hcomplex_mult)
3.1897 -done
3.1898 -declare hcomplex_of_complex_mult [simp]
3.1899 +by (simp add: hcomplex_of_complex_def hcomplex_mult)
3.1900
3.1901 -lemma hcomplex_of_complex_eq_iff:
3.1902 - "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
3.1903 -apply (unfold hcomplex_of_complex_def)
3.1904 -apply auto
3.1905 -done
3.1906 -declare hcomplex_of_complex_eq_iff [simp]
3.1907 +lemma hcomplex_of_complex_eq_iff [simp]:
3.1908 +     "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)"
3.1910
3.1911 -lemma hcomplex_of_complex_minus:
3.1912 +
3.1913 +lemma hcomplex_of_complex_minus [simp]:
3.1914       "hcomplex_of_complex (-r) = - hcomplex_of_complex  r"
3.1915 -apply (unfold hcomplex_of_complex_def)
3.1916 -apply (auto simp add: hcomplex_minus)
3.1917 -done
3.1918 -declare hcomplex_of_complex_minus [simp]
3.1919 +by (simp add: hcomplex_of_complex_def hcomplex_minus)
3.1920
3.1921 -lemma hcomplex_of_complex_one [simp]:
3.1922 -      "hcomplex_of_complex 1 = 1"
3.1923 -apply (unfold hcomplex_of_complex_def hcomplex_one_def)
3.1924 -apply auto
3.1925 -done
3.1926 +lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1"
3.1927 +by (simp add: hcomplex_of_complex_def hcomplex_one_def)
3.1928
3.1929 -lemma hcomplex_of_complex_zero [simp]:
3.1930 -      "hcomplex_of_complex 0 = 0"
3.1931 -apply (unfold hcomplex_of_complex_def hcomplex_zero_def)
3.1932 -apply (simp (no_asm))
3.1933 -done
3.1934 +lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0"
3.1935 +by (simp add: hcomplex_of_complex_def hcomplex_zero_def)
3.1936
3.1937  lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)"
3.1938 -apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
3.1939 -done
3.1940 +by (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def)
3.1941
3.1942 -lemma hcomplex_of_complex_inverse:
3.1943 +lemma hcomplex_of_complex_inverse [simp]:
3.1944       "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)"
3.1945  apply (case_tac "r=0")
3.1947 -apply (rule_tac c1 = "hcomplex_of_complex r"
3.1948 +apply (rule_tac c1 = "hcomplex_of_complex r"
3.1949         in hcomplex_mult_left_cancel [THEN iffD1])
3.1950  apply (force simp add: hcomplex_of_complex_zero_iff)
3.1951  apply (subst hcomplex_of_complex_mult [symmetric])
3.1952 -apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
3.1953 +apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff)
3.1954  done
3.1955 -declare hcomplex_of_complex_inverse [simp]
3.1956
3.1957 -lemma hcomplex_of_complex_divide:
3.1958 +lemma hcomplex_of_complex_divide [simp]:
3.1959       "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2"
3.1960 -apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def)
3.1961 -done
3.1962 -declare hcomplex_of_complex_divide [simp]
3.1963 +by (simp add: hcomplex_divide_def complex_divide_def)
3.1964
3.1965  lemma hRe_hcomplex_of_complex:
3.1966     "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)"
3.1967 -apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
3.1968 -apply (auto simp add: hRe)
3.1969 -done
3.1970 +by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe)
3.1971
3.1972  lemma hIm_hcomplex_of_complex:
3.1973     "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)"
3.1974 -apply (unfold hcomplex_of_complex_def hypreal_of_real_def)
3.1975 -apply (auto simp add: hIm)
3.1976 -done
3.1977 +by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm)
3.1978
3.1979  lemma hcmod_hcomplex_of_complex:
3.1980       "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)"
3.1981 -apply (unfold hypreal_of_real_def hcomplex_of_complex_def)
3.1982 -apply (auto simp add: hcmod)
3.1983 -done
3.1984 +by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod)
3.1985
3.1986  ML
3.1987  {*
3.1988 @@ -1710,7 +1447,6 @@
3.1990  val hcomplex_minus_congruent = thm"hcomplex_minus_congruent";
3.1991  val hcomplex_minus = thm"hcomplex_minus";
3.1992 -val inj_hcomplex_minus = thm"inj_hcomplex_minus";
3.1994  val hRe_minus = thm"hRe_minus";
3.1995  val hIm_minus = thm"hIm_minus";
3.1996 @@ -1728,14 +1464,11 @@
3.1998  val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one";
3.1999  val hcomplex_inverse = thm"hcomplex_inverse";
3.2000 -val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO";
3.2001 -val HCOMPLEX_DIVISION_BY_ZERO = thm"HCOMPLEX_DIVISION_BY_ZERO";
3.2002  val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left";
3.2003  val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
3.2004  val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
3.2006  val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
3.2007 -val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal";
3.2008  val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
3.2009  val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
3.2010  val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
3.2011 @@ -1755,7 +1488,6 @@
3.2012  val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
3.2013  val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
3.2014  val hcnj = thm"hcnj";
3.2015 -val inj_hcnj = thm"inj_hcnj";
3.2016  val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
3.2017  val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
3.2018  val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
3.2019 @@ -1798,7 +1530,6 @@
3.2020  val hcpow_minus = thm"hcpow_minus";
3.2021  val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
3.2022  val hcmod_divide = thm"hcmod_divide";
3.2023 -val hcomplex_inverse_divide = thm"hcomplex_inverse_divide";
3.2024  val hcpow_mult = thm"hcpow_mult";
3.2025  val hcpow_zero = thm"hcpow_zero";
3.2026  val hcpow_zero2 = thm"hcpow_zero2";
```
```     4.1 --- a/src/HOL/Real/Complex_Numbers.thy	Tue Feb 03 11:06:36 2004 +0100
4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
4.3 @@ -1,182 +0,0 @@
4.4 -(*  Title:      HOL/Real/Complex_Numbers.thy
4.5 -    ID:         \$Id\$
4.6 -    Author:     Gertrud Bauer and Markus Wenzel, TU München
4.8 -*)
4.9 -
4.10 -header {* Complex numbers *}
4.11 -
4.12 -theory Complex_Numbers = RealPow + Ring_and_Field:
4.13 -
4.14 -subsection {* Representation of complex numbers *}
4.15 -
4.16 -datatype complex = Complex real real
4.17 -
4.18 -consts Re :: "complex => real"
4.19 -primrec "Re (Complex x y) = x"
4.20 -
4.21 -consts Im :: "complex => real"
4.22 -primrec "Im (Complex x y) = y"
4.23 -
4.24 -lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
4.25 -  by (induct z) simp
4.26 -
4.27 -instance complex :: zero ..
4.28 -instance complex :: one ..
4.29 -instance complex :: number ..
4.30 -instance complex :: plus ..
4.31 -instance complex :: minus ..
4.32 -instance complex :: times ..
4.33 -instance complex :: inverse ..
4.34 -
4.36 -  zero_complex_def: "0 == Complex 0 0"
4.37 -  one_complex_def: "1 == Complex 1 0"
4.38 -  number_of_complex_def: "number_of b == Complex (number_of b) 0"
4.39 -  add_complex_def: "z + w == Complex (Re z + Re w) (Im z + Im w)"
4.40 -  minus_complex_def: "z - w == Complex (Re z - Re w) (Im z - Im w)"
4.41 -  uminus_complex_def: "- z == Complex (- Re z) (- Im z)"
4.42 -  mult_complex_def: "z * w ==
4.43 -    Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)"
4.44 -  inverse_complex_def: "(z::complex) \<noteq> 0 ==> inverse z ==
4.45 -    Complex (Re z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>)) (- Im z / ((Re z)\<twosuperior> + (Im z)\<twosuperior>))"
4.46 -  divide_complex_def: "(w::complex) \<noteq> 0 ==> z / (w::complex) == z * inverse w"
4.47 -
4.48 -lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
4.49 -  by (induct z, induct w) simp
4.50 -
4.51 -lemma Re_zero [simp]: "Re 0 = 0"
4.52 -  and Im_zero [simp]: "Im 0 = 0"
4.53 -  by (simp_all add: zero_complex_def)
4.54 -
4.55 -lemma Re_one [simp]: "Re 1 = 1"
4.56 -  and Im_one [simp]: "Im 1 = 0"
4.57 -  by (simp_all add: one_complex_def)
4.58 -
4.59 -lemma Re_add [simp]: "Re (z + w) = Re z + Re w"
4.61 -
4.62 -lemma Im_add [simp]: "Im (z + w) = Im z + Im w"
4.64 -
4.65 -lemma Re_diff [simp]: "Re (z - w) = Re z - Re w"
4.66 -  by (simp add: minus_complex_def)
4.67 -
4.68 -lemma Im_diff [simp]: "Im (z - w) = Im z - Im w"
4.69 -  by (simp add: minus_complex_def)
4.70 -
4.71 -lemma Re_uminus [simp]: "Re (-z) = - Re z"
4.72 -  by (simp add: uminus_complex_def)
4.73 -
4.74 -lemma Im_uminus [simp]: "Im (-z) = - Im z"
4.75 -  by (simp add: uminus_complex_def)
4.76 -
4.77 -lemma Re_mult [simp]: "Re (z * w) = Re z * Re w - Im z * Im w"
4.78 -  by (simp add: mult_complex_def)
4.79 -
4.80 -lemma Im_mult [simp]: "Im (z * w) = Re z * Im w + Im z * Re w"
4.81 -  by (simp add: mult_complex_def)
4.82 -
4.83 -lemma zero_complex_iff: "(z = 0) = (Re z = 0 \<and> Im z = 0)"
4.84 -  and one_complex_iff: "(z = 1) = (Re z = 1 \<and> Im z = 0)"
4.85 -  by (auto simp add: complex_equality)
4.86 -
4.87 -
4.88 -subsection {* The field of complex numbers *}
4.89 -
4.90 -instance complex :: field
4.91 -proof
4.92 -  fix z u v w :: complex
4.93 -  show "(u + v) + w = u + (v + w)"
4.95 -  show "z + w = w + z"
4.97 -  show "0 + z = z"
4.99 -  show "-z + z = 0"
4.100 -    by (simp add: complex_equality minus_complex_def)
4.101 -  show "z - w = z + -w"
4.103 -  show "(u * v) * w = u * (v * w)"
4.104 -    by (simp add: mult_complex_def mult_ac ring_distrib real_diff_def)  (* FIXME *)
4.105 -  show "z * w = w * z"
4.106 -    by (simp add: mult_complex_def)
4.107 -  show "1 * z = z"
4.108 -    by (simp add: one_complex_def mult_complex_def)
4.109 -  show "0 \<noteq> (1::complex)"  --{*for some reason it has to be early*}
4.110 -    by (simp add: zero_complex_def one_complex_def)
4.111 -  show "(u + v) * w = u * w + v * w"
4.113 -  show "z+u = z+v ==> u=v"
4.114 -    proof -
4.115 -      assume eq: "z+u = z+v"
4.116 -      hence "(-z + z) + u = (-z + z) + v" by (simp add: eq add_complex_def)
4.118 -    qed
4.119 -  assume neq: "w \<noteq> 0"
4.120 -  thus "z / w = z * inverse w"
4.121 -    by (simp add: divide_complex_def)
4.122 -  show "inverse w * w = 1"
4.123 -  proof
4.124 -    have neq': "Re w * Re w + Im w * Im w \<noteq> 0"
4.125 -    proof -
4.126 -      have ge: "0 \<le> Re w * Re w"  "0 \<le> Im w * Im w" by simp_all
4.127 -      from neq have "Re w \<noteq> 0 \<or> Im w \<noteq> 0" by (simp add: zero_complex_iff)
4.128 -      hence "Re w * Re w \<noteq> 0 \<or> Im w * Im w \<noteq> 0" by simp
4.129 -      thus ?thesis by rule (insert ge, arith+)
4.130 -    qed
4.131 -    with neq show "Re (inverse w * w) = Re 1"
4.133 -    from neq show "Im (inverse w * w) = Im 1"
4.134 -      by (simp add: inverse_complex_def power2_eq_square
4.136 -  qed
4.137 -qed
4.138 -
4.139 -
4.140 -subsection {* Basic operations *}
4.141 -
4.142 -instance complex :: power ..
4.143 -primrec (power_complex)
4.144 -  "z ^ 0 = 1"
4.145 -  "z ^ Suc n = (z::complex) * (z ^ n)"
4.146 -
4.147 -lemma complex_power_two: "z\<twosuperior> = z * (z::complex)"
4.148 -  by (simp add: complex_equality numeral_2_eq_2)
4.149 -
4.150 -
4.151 -constdefs
4.152 -  im_unit :: complex    ("\<i>")
4.153 -  "\<i> == Complex 0 1"
4.154 -
4.155 -lemma im_unit_square: "\<i>\<twosuperior> = -1"
4.156 -  by (simp add: im_unit_def complex_power_two mult_complex_def number_of_complex_def)
4.157 -
4.158 -
4.159 -constdefs
4.160 -  conjg :: "complex => complex"
4.161 -  "conjg z == Complex (Re z) (- Im z)"
4.162 -
4.163 -lemma Re_cong [simp]: "Re (conjg z) = Re z"
4.164 -  by (simp add: conjg_def)
4.165 -
4.166 -lemma Im_cong [simp]: "Im (conjg z) = - Im z"
4.167 -  by (simp add: conjg_def)
4.168 -
4.169 -lemma Re_conjg_self: "Re (z * conjg z) = (Re z)\<twosuperior> + (Im z)\<twosuperior>"
4.170 -  by (simp add: power2_eq_square)
4.171 -
4.172 -lemma Im_conjg_self: "Im (z * conjg z) = 0"
4.173 -  by simp
4.174 -
4.175 -
4.176 -subsection {* Embedding other number domains *}
4.177 -
4.178 -constdefs
4.179 -  complex :: "'a => complex"
4.180 -  "complex x == Complex (real x) 0";
4.181 -
4.182 -lemma Re_complex [simp]: "Re (complex x) = real x"
4.183 -  by (simp add: complex_def)
4.184 -
4.185 -end
```
```     5.1 --- a/src/HOL/Real/Real.thy	Tue Feb 03 11:06:36 2004 +0100
5.2 +++ b/src/HOL/Real/Real.thy	Tue Feb 03 15:58:31 2004 +0100
5.3 @@ -1,2 +1,2 @@
5.4
5.5 -Real = RComplete + Complex_Numbers
5.6 +Real = RComplete + RealPow
```