further tidying of the complex numbers
authorpaulson
Tue Feb 03 15:58:31 2004 +0100 (2004-02-03)
changeset 1437461de62096768
parent 14373 67a628beb981
child 14375 a545da363b23
further tidying of the complex numbers
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSCA.ML
src/HOL/Complex/NSComplex.thy
src/HOL/Real/Complex_Numbers.thy
src/HOL/Real/Real.thy
     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.31 +by (simp add: complex_zero_def)
    1.32 +
    1.33 +lemma complex_Im_zero [simp]: "Im 0 = 0"
    1.34  by (simp add: complex_zero_def)
    1.35  
    1.36 -lemma complex_Im_zero: "Im 0 = 0"
    1.37 -by (simp add: complex_zero_def)
    1.38 -declare complex_Re_zero [simp] complex_Im_zero [simp]
    1.39 +lemma complex_Re_one [simp]: "Re 1 = 1"
    1.40 +by (simp add: complex_one_def)
    1.41  
    1.42 -lemma complex_Re_one: "Re 1 = 1"
    1.43 -by (simp add: complex_one_def)
    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.48  by (simp add: complex_one_def)
    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.53  by (simp add: i_def)
    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.58  by (simp add: i_def)
    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.63  by (simp add: complex_of_real_def)
    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.67 -by (simp add: complex_of_real_def)
    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.72  by (simp add: complex_of_real_def)
    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.76 -by (simp add: complex_of_real_def)
    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.80 -by (simp add: complex_of_real_def)
    1.81 -declare Re_complex_of_real [simp]
    1.82 -
    1.83 -lemma Im_complex_of_real: "Im(complex_of_real z) = 0"
    1.84 -by (simp add: complex_of_real_def)
    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.92  by (simp add: complex_minus_def)
    1.93  
    1.94 -lemma complex_Re_minus: "Re (-z) = - Re z"
    1.95 -by (simp add: complex_minus_def)
    1.96 -
    1.97 -lemma complex_Im_minus: "Im (-z) = - Im z"
    1.98 +lemma complex_Re_minus [simp]: "Re (-z) = - Re z"
    1.99  by (simp add: complex_minus_def)
   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.109 +by (simp add: complex_minus_def)
   1.110  
   1.111  
   1.112  subsection{*Addition*}
   1.113 @@ -187,10 +154,10 @@
   1.114  lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)"
   1.115  by (simp add: complex_add_def)
   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.119  by (simp add: complex_add_def)
   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.123  by (simp add: complex_add_def)
   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.128  by (simp add: complex_add_def complex_minus_def complex_diff_def)
   1.129  
   1.130 +lemma complex_Re_diff [simp]: "Re(x - y) = Re(x) - Re(y)"
   1.131 +by (simp add: complex_diff_def)
   1.132 +
   1.133 +lemma complex_Im_diff [simp]: "Im(x - y) = Im(x) - Im(y)"
   1.134 +by (simp add: complex_diff_def)
   1.135 +
   1.136 +
   1.137  subsection{*Multiplication*}
   1.138  
   1.139  lemma complex_mult:
   1.140 @@ -222,7 +196,7 @@
   1.141  by (simp add: complex_mult_def mult_commute add_commute)
   1.142  
   1.143  lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)"
   1.144 -by (simp add: complex_mult_def mult_ac add_ac 
   1.145 +by (simp add: complex_mult_def mult_ac add_ac
   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.150  by (simp add: complex_inverse_def)
   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.166 -    by (rule complex_add_assoc) 
   1.167 +    by (rule complex_add_assoc)
   1.168    show "z + w = w + z"
   1.169 -    by (rule complex_add_commute) 
   1.170 +    by (rule complex_add_commute)
   1.171    show "0 + z = z"
   1.172 -    by (rule complex_add_zero_left) 
   1.173 +    by (rule complex_add_zero_left)
   1.174    show "-z + z = 0"
   1.175 -    by (rule complex_add_minus_left) 
   1.176 +    by (rule complex_add_minus_left)
   1.177    show "z - w = z + -w"
   1.178      by (simp add: complex_diff_def)
   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.191      by (simp add: complex_mult_def complex_add_def left_distrib real_diff_def add_ac)
   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.197        thus "u = v" by (simp add: complex_add_minus_left complex_add_zero_left)
   1.198      qed
   1.199 @@ -283,7 +257,7 @@
   1.200    thus "z / w = z * inverse w"
   1.201      by (simp add: complex_divide_def)
   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.233 -by (simp add: complex_of_real_def) 
   1.234 -declare complex_of_real_eq_iff [iff]
   1.235 +by (simp add: complex_of_real_def)
   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.253 -by (simp add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add)
   1.254 +by (simp add: complex_of_real_minus [symmetric] complex_diff_def 
   1.255 +              complex_of_real_add)
   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.261  apply (simp add: complex_divide_def)
   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.269  by (simp add: cmod_def)
   1.270  
   1.271 -lemma complex_mod_zero: "cmod(0) = 0"
   1.272 +lemma complex_mod_zero [simp]: "cmod(0) = 0"
   1.273  by (simp add: cmod_def)
   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.293  by (simp add: cnj_def)
   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.302  by (simp add: cnj_def)
   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.328  by (induct z, simp add: complex_add complex_cnj complex_of_real_def)
   1.329  
   1.330  lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii"
   1.331  apply (induct z)
   1.332 -apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def 
   1.333 +apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def
   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.352 -by (induct x, induct y, simp add: complex_zero_def complex_add)
   1.353 -declare complex_add_left_cancel_zero [simp]
   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.390  by (simp add: cmod_def)
   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.394  by (simp add: cmod_def)
   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.410 -apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac)
   1.411 +apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib 
   1.412 +                      add_ac mult_ac)
   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.416 +lemma complex_mod_add_squared_eq:
   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.420  apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac)
   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.443  by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric])
   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.455              simp add: power2_eq_square [symmetric])
   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.470 +lemma complex_mod_add_less:
   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.486  apply (simp add: compare_rls)
   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.490  apply (auto simp add: add_ac)
   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.503  by (simp add: complex_divide_def real_divide_def, simp add: complex_mod_mult complex_mod_inverse)
   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.528  by (simp add: sgn_def)
   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.533  by (simp add: sgn_def)
   1.534 -declare sgn_one [simp]
   1.535  
   1.536  lemma sgn_minus: "sgn (-z) = - sgn(z)"
   1.537  by (simp add: sgn_def)
   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.542  apply (simp add: sgn_def)
   1.543  done
   1.544  
   1.545 @@ -631,20 +574,18 @@
   1.546  apply (auto simp add: complex_of_real_def i_def complex_mult complex_add)
   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.552  by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
   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.557  by (auto simp add: complex_of_real_def i_def complex_mult complex_add)
   1.558 -declare Im_complex_i [simp]
   1.559  
   1.560  lemma i_mult_eq: "ii * ii = complex_of_real (-1)"
   1.561  by (simp add: i_def complex_of_real_def complex_mult complex_add)
   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.572  by (simp add: complex_of_real_def i_def complex_mult complex_add)
   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.588  by (simp add: mult_commute)
   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.641  by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add)
   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.664 -by (simp add: complex_of_real_def i_def complex_mult complex_add 
   1.665 +by (simp add: complex_of_real_def i_def complex_mult complex_add
   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.758  apply (simp add: cmod_def)
   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.811  by (simp add: rcis_def)
   1.812  
   1.813 -lemma rcis_mult:
   1.814 -  "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
   1.815 -apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib 
   1.816 +lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
   1.817 +apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib
   1.818                   mult_ac add_ac)
   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.820  apply (auto simp add: add_ac)
   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.827  by (simp add: cis_def)
   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.832  by (simp add: cis_def)
   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.837  by (simp add: rcis_def)
   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.842  by (simp add: rcis_def)
   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.892  by (simp add: cis_def)
   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.897  by (simp add: cis_def)
   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.903  by (simp add: expi_def)
   1.904  
   1.905  lemma expi_add: "expi(a + b) = expi(a) * expi(b)"
   1.906 -by (simp add: expi_def complex_Re_add exp_add complex_Im_add cis_mult [symmetric] complex_of_real_mult mult_ac)
   1.907 +by (simp add: expi_def complex_Re_add exp_add complex_Im_add 
   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.913  by (simp add: expi_def)
   1.914  
   1.915 -lemma expi_zero: "expi (0::complex) = 1"
   1.916 +lemma expi_zero [simp]: "expi (0::complex) = 1"
   1.917  by (simp add: expi_def)
   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.947  val complex_add = thm"complex_add";
   1.948  val complex_Re_add = thm"complex_Re_add";
   1.949  val complex_Im_add = thm"complex_Im_add";
   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.954 -val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero";
   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.7 -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym]));
     2.8 +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1); 
     2.9  qed "CInfinitesimal_add_capprox";
    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.14 -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym]));
    2.15 +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1);
    2.16  qed "CInfinitesimal_add_capprox_self";
    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.14 -apply (simp add: hcomplexrel_iff) 
    3.15 -done
    3.16 +by (simp add: hcomplexrel_def)
    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.25 -apply (simp add: hcomplexrel_iff) 
    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.66 +by (simp add: hcomplexrel_def)
    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.95 +by (simp add: hcomplexrel_def)
    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.106 +apply (simp add: hRe_def)
   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.117 +apply (simp add: hIm_def)
   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.167  lemma hcomplex_add_congruent2:
   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.175  lemma hcomplex_add:
   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.178 -apply (unfold hcomplex_add_def)
   3.179 -apply (rule_tac f = "Abs_hcomplex" in arg_cong)
   3.180 +apply (simp add: hcomplex_add_def)
   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.190  apply (simp add: complex_add_commute hcomplex_add)
   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.200  apply (simp add: hcomplex_add complex_add_assoc)
   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.206 -apply (simp add: hcomplex_add)
   3.207 +apply (rule eq_Abs_hcomplex [of z])
   3.208 +apply (simp add: hcomplex_zero_def hcomplex_add)
   3.209  done
   3.210  
   3.211  lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z"
   3.212 -apply (simp add: hcomplex_add_zero_left hcomplex_add_commute)
   3.213 -done
   3.214 +by (simp add: hcomplex_add_zero_left hcomplex_add_commute)
   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.219 -apply (auto simp add: hRe hcomplex_add hypreal_add complex_Re_add)
   3.220 +apply (rule eq_Abs_hcomplex [of x])
   3.221 +apply (rule eq_Abs_hcomplex [of y])
   3.222 +apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add)
   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.228 -apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add)
   3.229 +apply (rule eq_Abs_hcomplex [of x])
   3.230 +apply (rule eq_Abs_hcomplex [of y])
   3.231 +apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add)
   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.244 +by (simp add: congruent_def)
   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.251 +apply (simp add: hcomplex_minus_def)
   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.258 -apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
   3.259 +apply (rule eq_Abs_hcomplex [of z])
   3.260 +apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def)
   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.274 +apply (simp add: hcomplex_mult_def)
   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.315  lemma hcomplex_add_mult_distrib:
   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.320 -apply (auto simp add: hcomplex_mult hcomplex_add left_distrib)
   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.324 +apply (simp add: hcomplex_mult hcomplex_add left_distrib)
   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.343 +apply (simp add: hcinv_def)
   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.364      by (simp add: hcomplex_add_mult_distrib)
   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.372          by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left)
   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.421  lemma hcomplex_add_minus_eq_minus:
   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.454 -by (simp add: field_mult_cancel_left) 
   3.455 +by (simp add: field_mult_cancel_left)
   3.456  
   3.457  lemma hcomplex_mult_right_cancel:
   3.458       "(c::hcomplex) \<noteq> (0::hcomplex) ==> (a*c=b*c) = (a=b)"
   3.459 -apply (simp add: Ring_and_Field.field_mult_cancel_right); 
   3.460 -done
   3.461 +by (simp add: Ring_and_Field.field_mult_cancel_right)
   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.470 -apply (auto simp add: hcomplex_minus hcomplex_add complex_diff_def)
   3.471 -done
   3.472 +by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def)
   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.481 -apply (rule Ring_and_Field.add_divide_distrib) 
   3.482 -done
   3.483 +by (rule Ring_and_Field.add_divide_distrib)
   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.495 +apply (simp add: hcomplex_of_hypreal_def)
   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.508 +apply (simp add: hcomplex_of_hypreal)
   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.533  lemma hcomplex_of_hypreal_add:
   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.538 -apply (auto simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
   3.539 +apply (rule eq_Abs_hypreal [of x])
   3.540 +apply (rule eq_Abs_hypreal [of y])
   3.541 +apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add)
   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.548 -apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
   3.549 -done
   3.550 +by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def)
   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.569 +apply (simp add: hcomplex_divide_def)
   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.579 +apply (simp add: hypreal_divide_def)
   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.625 +apply (simp add: hcmod_def)
   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.670 +apply (simp add: hcnj_def)
   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.683 +apply (simp add: hcnj)
   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.688 +apply (simp add: hcnj)
   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.739 -apply (auto simp add: hcnj hcomplex_add complex_cnj_add)
   3.740 +apply (rule eq_Abs_hcomplex [of z])
   3.741 +apply (rule eq_Abs_hcomplex [of w])
   3.742 +apply (simp add: hcnj hcomplex_add complex_cnj_add)
   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.801 +apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add
   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.874  lemma hcmod_add_squared_eq:
   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.878 -apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
   3.879 -                      numeral_2_eq_2 realpow_two [symmetric] 
   3.880 -                 simp del: realpow_Suc)
   3.881 -apply (auto simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
   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.885 +apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult
   3.886 +                      numeral_2_eq_2 realpow_two [symmetric]
   3.887 +                  del: realpow_Suc)
   3.888 +apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq
   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.908  apply (simp add: hcmod_mult)
   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.915 -apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
   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.919 +apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add
   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.931 -apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le)
   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.935 +apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le)
   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.943  apply (simp add: add_ac)
   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.956  lemma hcmod_add_less:
   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.962 -apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_less)
   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.968 +apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra)
   3.969  apply (auto intro: complex_mod_add_less)
   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.991 -apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
   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.995 +apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le)
   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.1008 +apply (simp add: hcpow_def)
  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.1094 -apply (auto simp add: hcpow hypnat_add)
  3.1095 +apply (simp add: hcomplex_zero_def hypnat_one_def)
  3.1096 +apply (rule eq_Abs_hypnat [of n])
  3.1097 +apply (simp add: hcpow hypnat_add)
  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.1104 +by (simp add: hSuc_def)
  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.1134 +by (simp add: numeral_2_eq_2)
  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.1161 +apply (simp add: hsgn_def)
  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.1219  apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult)
  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.1237  apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  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.1246 -apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  3.1247 +apply (rule eq_Abs_hypreal [of x])
  3.1248 +apply (rule eq_Abs_hypreal [of y])
  3.1249 +apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal)
  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.1258 -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
  3.1259 +apply (rule eq_Abs_hypreal [of x])
  3.1260 +apply (rule eq_Abs_hypreal [of y])
  3.1261 +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2)
  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.1273 -apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
  3.1274 -apply (ultra)
  3.1275 +apply (simp add: iii_def)
  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.1280 +apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
  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.1292 -apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal)
  3.1293 -apply (ultra)
  3.1294 +apply (simp add: iii_def)
  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.1299 +apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra)
  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.1318 +apply (simp add: hcomplex_mult_commute)
  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.1327 +apply (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.1336 +apply (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.1355 +apply (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.1374 +apply (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.1384 -apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
  3.1385 -apply ultra
  3.1386 -apply (auto simp add: complex_split_Re_zero)
  3.1387 +apply (simp add: iii_def)
  3.1388 +apply (rule eq_Abs_hypreal [of x])
  3.1389 +apply (rule eq_Abs_hypreal [of y])
  3.1390 +apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
  3.1391 +apply (simp add: complex_split_Re_zero)
  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.1400 -apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num)
  3.1401 -apply ultra
  3.1402 -apply (auto simp add: complex_split_Im_zero)
  3.1403 +apply (simp add: iii_def)
  3.1404 +apply (rule eq_Abs_hypreal [of x])
  3.1405 +apply (rule eq_Abs_hypreal [of y])
  3.1406 +apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra)
  3.1407 +apply (simp add: complex_split_Im_zero)
  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.1428 -lemma real_two_squares_add_zero_iff:
  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.1433 -declare real_two_squares_add_zero_iff [simp]
  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.1444 +apply (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.1445 +done
  3.1446 +
  3.1447 +lemma hRe_mult_i_eq[simp]:
  3.1448 +    "hRe (iii * hcomplex_of_hypreal y) = 0"
  3.1449 +apply (simp add: iii_def)
  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.1468 +apply (simp add: iii_def)
  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.1488 +by (simp add: hcomplex_mult_commute)
  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.1498 +apply (simp add: harg_def)
  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.1546 -apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
  3.1547 -apply (cut_tac z = "x" in complex_split_polar2)
  3.1548 +apply (rule eq_Abs_hcomplex [of z])
  3.1549 +apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult)
  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.1566 +apply (simp add: hcis_def)
  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.1577 +apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def)
  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.1640 +apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs)
  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.1660 +by (simp add: hrcis_def)
  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.1670 -apply (auto simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
  3.1671 -                      hcomplex_mult cis_mult [symmetric] 
  3.1672 +apply (simp add: hrcis_def)
  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.1677 +apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal
  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.1685 -apply (auto simp add: hcis hcomplex_mult hypreal_add cis_mult)
  3.1686 +apply (rule eq_Abs_hypreal [of a])
  3.1687 +apply (rule eq_Abs_hypreal [of b])
  3.1688 +apply (simp add: hcis hcomplex_mult hypreal_add cis_mult)
  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.1706 +apply (simp add: hcomplex_zero_def)
  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.1746 +apply (simp_all 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.1757 +apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult)
  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.1795 +apply (simp add: real_divide_def)
  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.1830 +apply (simp add: NSDeMoivre)
  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.1837 +apply (simp add: NSDeMoivre)
  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.1844 +apply (simp add: NSDeMoivre_ext)
  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.1851 +apply (simp add: NSDeMoivre_ext)
  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.1858 -apply (auto simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult)
  3.1859 +apply (simp add: hexpi_def)
  3.1860 +apply (rule eq_Abs_hcomplex [of a])
  3.1861 +apply (rule eq_Abs_hcomplex [of b])
  3.1862 +apply (simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult)
  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.1874 +apply (simp add: hcomplex_of_complex_def)
  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.1883 -lemma hcomplex_of_complex_add:
  3.1884 +lemma hcomplex_of_complex_add [simp]:
  3.1885       "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2"
  3.1886 -apply (unfold hcomplex_of_complex_def)
  3.1887 -apply (simp (no_asm) add: hcomplex_add)
  3.1888 -done
  3.1889 -declare hcomplex_of_complex_add [simp]
  3.1890 +by (simp add: hcomplex_of_complex_def hcomplex_add)
  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.1909 +by (simp add: hcomplex_of_complex_def)
  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.1946  apply (simp add: hcomplex_of_complex_zero)
  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.1989  val hIm_add = thm"hIm_add";
  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.1993  val hcomplex_add_minus_left = thm"hcomplex_add_minus_left";
  3.1994  val hRe_minus = thm"hRe_minus";
  3.1995  val hIm_minus = thm"hIm_minus";
  3.1996 @@ -1728,14 +1464,11 @@
  3.1997  val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib";
  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.2005  val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
  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.7 -    License:    GPL (GNU GENERAL PUBLIC LICENSE)
     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.35 -defs (overloaded)
    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.60 -  by (simp add: add_complex_def)
    4.61 -
    4.62 -lemma Im_add [simp]: "Im (z + w) = Im z + Im w"
    4.63 -  by (simp add: add_complex_def)
    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.94 -    by (simp add: add_complex_def)
    4.95 -  show "z + w = w + z"
    4.96 -    by (simp add: add_complex_def)
    4.97 -  show "0 + z = z"
    4.98 -    by (simp add: add_complex_def zero_complex_def)
    4.99 -  show "-z + z = 0"
   4.100 -    by (simp add: complex_equality minus_complex_def)
   4.101 -  show "z - w = z + -w"
   4.102 -    by (simp add: add_complex_def minus_complex_def uminus_complex_def)
   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.112 -    by (simp add: add_complex_def mult_complex_def ring_distrib)
   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.117 -      thus "u = v" by (simp add: 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.132 -      by (simp add: inverse_complex_def power2_eq_square add_divide_distrib [symmetric])
   4.133 -    from neq show "Im (inverse w * w) = Im 1"
   4.134 -      by (simp add: inverse_complex_def power2_eq_square
   4.135 -        mult_ac add_divide_distrib [symmetric])
   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