src/HOL/Complex/Complex.thy
changeset 14374 61de62096768
parent 14373 67a628beb981
child 14377 f454b3004f8f
     1.1 --- a/src/HOL/Complex/Complex.thy	Tue Feb 03 11:06:36 2004 +0100
     1.2 +++ b/src/HOL/Complex/Complex.thy	Tue Feb 03 15:58:31 2004 +0100
     1.3 @@ -79,7 +79,7 @@
     1.4    complex_diff_def:
     1.5      "z - w == z + - (w::complex)"
     1.6  
     1.7 -  complex_mult_def: 
     1.8 +  complex_mult_def:
     1.9      "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)"
    1.10  
    1.11    complex_divide_def: "w / (z::complex) == w * inverse z"
    1.12 @@ -103,83 +103,50 @@
    1.13  lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
    1.14    by (induct z, induct w) simp
    1.15  
    1.16 -lemma Re: "Re(Complex x y) = x"
    1.17 +lemma Re [simp]: "Re(Complex x y) = x"
    1.18  by simp
    1.19 -declare Re [simp]
    1.20  
    1.21 -lemma Im: "Im(Complex x y) = y"
    1.22 +lemma Im [simp]: "Im(Complex x y) = y"
    1.23  by simp
    1.24 -declare Im [simp]
    1.25  
    1.26  lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))"
    1.27  by (induct w, induct z, simp)
    1.28  
    1.29 -lemma complex_Re_zero: "Re 0 = 0"
    1.30 +lemma complex_Re_zero [simp]: "Re 0 = 0"
    1.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";