avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
authorhoelzl
Wed May 07 12:25:35 2014 +0200 (2014-05-07)
changeset 5688948a745e1bde7
parent 56888 3e8cbb624cc5
child 56900 beea3ee118af
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
NEWS
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Int.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Fundamental_Theorem_Algebra.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/NSA/CLim.thy
src/HOL/NSA/NSCA.thy
src/HOL/NSA/NSComplex.thy
src/HOL/NthRoot.thy
src/HOL/Real.thy
src/HOL/Real_Vector_Spaces.thy
     1.1 --- a/NEWS	Tue May 06 23:35:24 2014 +0200
     1.2 +++ b/NEWS	Wed May 07 12:25:35 2014 +0200
     1.3 @@ -590,6 +590,48 @@
     1.4  * Include more theorems in continuous_intros. Remove the continuous_on_intros,
     1.5    isCont_intros collections, these facts are now in continuous_intros.
     1.6  
     1.7 +* Theorems about complex numbers are now stated only using Re and Im, the Complex
     1.8 +  constructor is not used anymore. It is possible to use primcorec to defined the
     1.9 +  behaviour of a complex-valued function.
    1.10 +
    1.11 +  Removed theorems about the Complex constructor from the simpset, they are
    1.12 +  available as the lemma collection legacy_Complex_simps. This especially
    1.13 +  removes
    1.14 +    i_complex_of_real: "ii * complex_of_real r = Complex 0 r".
    1.15 +
    1.16 +  Instead the reverse direction is supported with
    1.17 +    Complex_eq: "Complex a b = a + \<i> * b"
    1.18 +
    1.19 +  Moved csqrt from Fundamental_Algebra_Theorem to Complex.
    1.20 +
    1.21 +  Renamings:
    1.22 +    Re/Im                  ~>  complex.sel
    1.23 +    complex_Re/Im_zero     ~>  zero_complex.sel
    1.24 +    complex_Re/Im_add      ~>  plus_complex.sel
    1.25 +    complex_Re/Im_minus    ~>  uminus_complex.sel
    1.26 +    complex_Re/Im_diff     ~>  minus_complex.sel
    1.27 +    complex_Re/Im_one      ~>  one_complex.sel
    1.28 +    complex_Re/Im_mult     ~>  times_complex.sel
    1.29 +    complex_Re/Im_inverse  ~>  inverse_complex.sel
    1.30 +    complex_Re/Im_scaleR   ~>  scaleR_complex.sel
    1.31 +    complex_Re/Im_i        ~>  ii.sel
    1.32 +    complex_Re/Im_cnj      ~>  cnj.sel
    1.33 +    Re/Im_cis              ~>  cis.sel
    1.34 +
    1.35 +    complex_divide_def   ~>  divide_complex_def
    1.36 +    complex_norm_def     ~>  norm_complex_def
    1.37 +    cmod_def             ~>  norm_complex_de
    1.38 +
    1.39 +  Removed theorems:
    1.40 +    complex_zero_def
    1.41 +    complex_add_def
    1.42 +    complex_minus_def
    1.43 +    complex_diff_def
    1.44 +    complex_one_def
    1.45 +    complex_mult_def
    1.46 +    complex_inverse_def
    1.47 +    complex_scaleR_def
    1.48 +
    1.49  * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead.
    1.50  
    1.51  * Nitpick:
     2.1 --- a/src/HOL/Complex.thy	Tue May 06 23:35:24 2014 +0200
     2.2 +++ b/src/HOL/Complex.thy	Wed May 07 12:25:35 2014 +0200
     2.3 @@ -10,202 +10,105 @@
     2.4  imports Transcendental
     2.5  begin
     2.6  
     2.7 -datatype complex = Complex real real
     2.8 +text {*
     2.9  
    2.10 -primrec Re :: "complex \<Rightarrow> real"
    2.11 -  where Re: "Re (Complex x y) = x"
    2.12 +We use the @{text codatatype}-command to define the type of complex numbers. This might look strange
    2.13 +at first, but allows us to use @{text primcorec} to define complex-functions by defining their
    2.14 +real and imaginary result separate.
    2.15  
    2.16 -primrec Im :: "complex \<Rightarrow> real"
    2.17 -  where Im: "Im (Complex x y) = y"
    2.18 +*}
    2.19  
    2.20 -lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
    2.21 -  by (induct z) simp
    2.22 +codatatype complex = Complex (Re: real) (Im: real)
    2.23 +
    2.24 +lemma complex_surj: "Complex (Re z) (Im z) = z"
    2.25 +  by (rule complex.collapse)
    2.26  
    2.27  lemma complex_eqI [intro?]: "\<lbrakk>Re x = Re y; Im x = Im y\<rbrakk> \<Longrightarrow> x = y"
    2.28 -  by (induct x, induct y) simp
    2.29 +  by (rule complex.expand) simp
    2.30  
    2.31  lemma complex_eq_iff: "x = y \<longleftrightarrow> Re x = Re y \<and> Im x = Im y"
    2.32 -  by (induct x, induct y) simp
    2.33 -
    2.34 +  by (auto intro: complex.expand)
    2.35  
    2.36  subsection {* Addition and Subtraction *}
    2.37  
    2.38  instantiation complex :: ab_group_add
    2.39  begin
    2.40  
    2.41 -definition complex_zero_def:
    2.42 -  "0 = Complex 0 0"
    2.43 -
    2.44 -definition complex_add_def:
    2.45 -  "x + y = Complex (Re x + Re y) (Im x + Im y)"
    2.46 -
    2.47 -definition complex_minus_def:
    2.48 -  "- x = Complex (- Re x) (- Im x)"
    2.49 -
    2.50 -definition complex_diff_def:
    2.51 -  "x - (y\<Colon>complex) = x + - y"
    2.52 +primcorec zero_complex where
    2.53 +  "Re 0 = 0"
    2.54 +| "Im 0 = 0"
    2.55  
    2.56 -lemma Complex_eq_0 [simp]: "Complex a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
    2.57 -  by (simp add: complex_zero_def)
    2.58 -
    2.59 -lemma complex_Re_zero [simp]: "Re 0 = 0"
    2.60 -  by (simp add: complex_zero_def)
    2.61 -
    2.62 -lemma complex_Im_zero [simp]: "Im 0 = 0"
    2.63 -  by (simp add: complex_zero_def)
    2.64 -
    2.65 -lemma complex_add [simp]:
    2.66 -  "Complex a b + Complex c d = Complex (a + c) (b + d)"
    2.67 -  by (simp add: complex_add_def)
    2.68 +primcorec plus_complex where
    2.69 +  "Re (x + y) = Re x + Re y"
    2.70 +| "Im (x + y) = Im x + Im y"
    2.71  
    2.72 -lemma complex_Re_add [simp]: "Re (x + y) = Re x + Re y"
    2.73 -  by (simp add: complex_add_def)
    2.74 -
    2.75 -lemma complex_Im_add [simp]: "Im (x + y) = Im x + Im y"
    2.76 -  by (simp add: complex_add_def)
    2.77 -
    2.78 -lemma complex_minus [simp]:
    2.79 -  "- (Complex a b) = Complex (- a) (- b)"
    2.80 -  by (simp add: complex_minus_def)
    2.81 -
    2.82 -lemma complex_Re_minus [simp]: "Re (- x) = - Re x"
    2.83 -  by (simp add: complex_minus_def)
    2.84 +primcorec uminus_complex where
    2.85 +  "Re (- x) = - Re x"
    2.86 +| "Im (- x) = - Im x"
    2.87  
    2.88 -lemma complex_Im_minus [simp]: "Im (- x) = - Im x"
    2.89 -  by (simp add: complex_minus_def)
    2.90 -
    2.91 -lemma complex_diff [simp]:
    2.92 -  "Complex a b - Complex c d = Complex (a - c) (b - d)"
    2.93 -  by (simp add: complex_diff_def)
    2.94 -
    2.95 -lemma complex_Re_diff [simp]: "Re (x - y) = Re x - Re y"
    2.96 -  by (simp add: complex_diff_def)
    2.97 -
    2.98 -lemma complex_Im_diff [simp]: "Im (x - y) = Im x - Im y"
    2.99 -  by (simp add: complex_diff_def)
   2.100 +primcorec minus_complex where
   2.101 +  "Re (x - y) = Re x - Re y"
   2.102 +| "Im (x - y) = Im x - Im y"
   2.103  
   2.104  instance
   2.105 -  by intro_classes (simp_all add: complex_add_def complex_diff_def)
   2.106 +  by intro_classes (simp_all add: complex_eq_iff)
   2.107  
   2.108  end
   2.109  
   2.110 -
   2.111  subsection {* Multiplication and Division *}
   2.112  
   2.113  instantiation complex :: field_inverse_zero
   2.114  begin
   2.115  
   2.116 -definition complex_one_def:
   2.117 -  "1 = Complex 1 0"
   2.118 -
   2.119 -definition complex_mult_def:
   2.120 -  "x * y = Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)"
   2.121 -
   2.122 -definition complex_inverse_def:
   2.123 -  "inverse x =
   2.124 -    Complex (Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)) (- Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2))"
   2.125 -
   2.126 -definition complex_divide_def:
   2.127 -  "x / (y\<Colon>complex) = x * inverse y"
   2.128 -
   2.129 -lemma Complex_eq_1 [simp]:
   2.130 -  "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
   2.131 -  by (simp add: complex_one_def)
   2.132 -
   2.133 -lemma Complex_eq_neg_1 [simp]:
   2.134 -  "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
   2.135 -  by (simp add: complex_one_def)
   2.136 -
   2.137 -lemma complex_Re_one [simp]: "Re 1 = 1"
   2.138 -  by (simp add: complex_one_def)
   2.139 +primcorec one_complex where
   2.140 +  "Re 1 = 1"
   2.141 +| "Im 1 = 0"
   2.142  
   2.143 -lemma complex_Im_one [simp]: "Im 1 = 0"
   2.144 -  by (simp add: complex_one_def)
   2.145 -
   2.146 -lemma complex_mult [simp]:
   2.147 -  "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)"
   2.148 -  by (simp add: complex_mult_def)
   2.149 -
   2.150 -lemma complex_Re_mult [simp]: "Re (x * y) = Re x * Re y - Im x * Im y"
   2.151 -  by (simp add: complex_mult_def)
   2.152 +primcorec times_complex where
   2.153 +  "Re (x * y) = Re x * Re y - Im x * Im y"
   2.154 +| "Im (x * y) = Re x * Im y + Im x * Re y"
   2.155  
   2.156 -lemma complex_Im_mult [simp]: "Im (x * y) = Re x * Im y + Im x * Re y"
   2.157 -  by (simp add: complex_mult_def)
   2.158 -
   2.159 -lemma complex_inverse [simp]:
   2.160 -  "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"
   2.161 -  by (simp add: complex_inverse_def)
   2.162 +primcorec inverse_complex where
   2.163 +  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
   2.164 +| "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
   2.165  
   2.166 -lemma complex_Re_inverse:
   2.167 -  "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
   2.168 -  by (simp add: complex_inverse_def)
   2.169 -
   2.170 -lemma complex_Im_inverse:
   2.171 -  "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)"
   2.172 -  by (simp add: complex_inverse_def)
   2.173 +definition "x / (y\<Colon>complex) = x * inverse y"
   2.174  
   2.175  instance
   2.176 -  by intro_classes (simp_all add: complex_mult_def
   2.177 -    distrib_left distrib_right right_diff_distrib left_diff_distrib
   2.178 -    complex_inverse_def complex_divide_def
   2.179 -    power2_eq_square add_divide_distrib [symmetric]
   2.180 -    complex_eq_iff)
   2.181 +  by intro_classes 
   2.182 +     (simp_all add: complex_eq_iff divide_complex_def
   2.183 +      distrib_left distrib_right right_diff_distrib left_diff_distrib
   2.184 +      power2_eq_square add_divide_distrib [symmetric])
   2.185  
   2.186  end
   2.187  
   2.188 +lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
   2.189 +  unfolding divide_complex_def by (simp add: add_divide_distrib)
   2.190  
   2.191 -subsection {* Numerals and Arithmetic *}
   2.192 +lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)"
   2.193 +  unfolding divide_complex_def times_complex.sel inverse_complex.sel
   2.194 +  by (simp_all add: divide_simps)
   2.195  
   2.196 -lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
   2.197 -  by (induct n) simp_all
   2.198 +lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
   2.199 +  by (simp add: power2_eq_square)
   2.200  
   2.201 -lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0"
   2.202 +lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x"
   2.203 +  by (simp add: power2_eq_square)
   2.204 +
   2.205 +lemma Re_power_real: "Im x = 0 \<Longrightarrow> Re (x ^ n) = Re x ^ n "
   2.206    by (induct n) simp_all
   2.207  
   2.208 -lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z"
   2.209 -  by (cases z rule: int_diff_cases) simp
   2.210 -
   2.211 -lemma complex_Im_of_int [simp]: "Im (of_int z) = 0"
   2.212 -  by (cases z rule: int_diff_cases) simp
   2.213 -
   2.214 -lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
   2.215 -  using complex_Re_of_int [of "numeral v"] by simp
   2.216 -
   2.217 -lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v"
   2.218 -  using complex_Re_of_int [of "- numeral v"] by simp
   2.219 -
   2.220 -lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
   2.221 -  using complex_Im_of_int [of "numeral v"] by simp
   2.222 -
   2.223 -lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0"
   2.224 -  using complex_Im_of_int [of "- numeral v"] by simp
   2.225 -
   2.226 -lemma Complex_eq_numeral [simp]:
   2.227 -  "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
   2.228 -  by (simp add: complex_eq_iff)
   2.229 -
   2.230 -lemma Complex_eq_neg_numeral [simp]:
   2.231 -  "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
   2.232 -  by (simp add: complex_eq_iff)
   2.233 -
   2.234 +lemma Im_power_real: "Im x = 0 \<Longrightarrow> Im (x ^ n) = 0"
   2.235 +  by (induct n) simp_all
   2.236  
   2.237  subsection {* Scalar Multiplication *}
   2.238  
   2.239  instantiation complex :: real_field
   2.240  begin
   2.241  
   2.242 -definition complex_scaleR_def:
   2.243 -  "scaleR r x = Complex (r * Re x) (r * Im x)"
   2.244 -
   2.245 -lemma complex_scaleR [simp]:
   2.246 -  "scaleR r (Complex a b) = Complex (r * a) (r * b)"
   2.247 -  unfolding complex_scaleR_def by simp
   2.248 -
   2.249 -lemma complex_Re_scaleR [simp]: "Re (scaleR r x) = r * Re x"
   2.250 -  unfolding complex_scaleR_def by simp
   2.251 -
   2.252 -lemma complex_Im_scaleR [simp]: "Im (scaleR r x) = r * Im x"
   2.253 -  unfolding complex_scaleR_def by simp
   2.254 +primcorec scaleR_complex where
   2.255 +  "Re (scaleR r x) = r * Re x"
   2.256 +| "Im (scaleR r x) = r * Im x"
   2.257  
   2.258  instance
   2.259  proof
   2.260 @@ -226,55 +129,84 @@
   2.261  
   2.262  end
   2.263  
   2.264 -
   2.265 -subsection{* Properties of Embedding from Reals *}
   2.266 +subsection {* Numerals, Arithmetic, and Embedding from Reals *}
   2.267  
   2.268  abbreviation complex_of_real :: "real \<Rightarrow> complex"
   2.269    where "complex_of_real \<equiv> of_real"
   2.270  
   2.271  declare [[coercion complex_of_real]]
   2.272 +declare [[coercion "of_int :: int \<Rightarrow> complex"]]
   2.273 +declare [[coercion "of_nat :: nat \<Rightarrow> complex"]]
   2.274  
   2.275 -lemma complex_of_real_def: "complex_of_real r = Complex r 0"
   2.276 -  by (simp add: of_real_def complex_scaleR_def)
   2.277 +lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n"
   2.278 +  by (induct n) simp_all
   2.279 +
   2.280 +lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0"
   2.281 +  by (induct n) simp_all
   2.282 +
   2.283 +lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z"
   2.284 +  by (cases z rule: int_diff_cases) simp
   2.285 +
   2.286 +lemma complex_Im_of_int [simp]: "Im (of_int z) = 0"
   2.287 +  by (cases z rule: int_diff_cases) simp
   2.288 +
   2.289 +lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v"
   2.290 +  using complex_Re_of_int [of "numeral v"] by simp
   2.291 +
   2.292 +lemma complex_Im_numeral [simp]: "Im (numeral v) = 0"
   2.293 +  using complex_Im_of_int [of "numeral v"] by simp
   2.294  
   2.295  lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z"
   2.296 -  by (simp add: complex_of_real_def)
   2.297 +  by (simp add: of_real_def)
   2.298  
   2.299  lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0"
   2.300 -  by (simp add: complex_of_real_def)
   2.301 +  by (simp add: of_real_def)
   2.302 +
   2.303 +subsection {* The Complex Number $i$ *}
   2.304 +
   2.305 +primcorec "ii" :: complex  ("\<i>") where
   2.306 +  "Re ii = 0"
   2.307 +| "Im ii = 1"
   2.308  
   2.309 -lemma Complex_add_complex_of_real [simp]:
   2.310 -  shows "Complex x y + complex_of_real r = Complex (x+r) y"
   2.311 -  by (simp add: complex_of_real_def)
   2.312 +lemma i_squared [simp]: "ii * ii = -1"
   2.313 +  by (simp add: complex_eq_iff)
   2.314 +
   2.315 +lemma power2_i [simp]: "ii\<^sup>2 = -1"
   2.316 +  by (simp add: power2_eq_square)
   2.317  
   2.318 -lemma complex_of_real_add_Complex [simp]:
   2.319 -  shows "complex_of_real r + Complex x y = Complex (r+x) y"
   2.320 -  by (simp add: complex_of_real_def)
   2.321 +lemma inverse_i [simp]: "inverse ii = - ii"
   2.322 +  by (rule inverse_unique) simp
   2.323 +
   2.324 +lemma divide_i [simp]: "x / ii = - ii * x"
   2.325 +  by (simp add: divide_complex_def)
   2.326  
   2.327 -lemma Complex_mult_complex_of_real:
   2.328 -  shows "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
   2.329 -  by (simp add: complex_of_real_def)
   2.330 +lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
   2.331 +  by (simp add: mult_assoc [symmetric])
   2.332  
   2.333 -lemma complex_of_real_mult_Complex:
   2.334 -  shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
   2.335 -  by (simp add: complex_of_real_def)
   2.336 +lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
   2.337 +  by (simp add: complex_eq_iff)
   2.338 +
   2.339 +lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
   2.340 +  by (simp add: complex_eq_iff)
   2.341  
   2.342 -lemma complex_eq_cancel_iff2 [simp]:
   2.343 -  shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
   2.344 -  by (simp add: complex_of_real_def)
   2.345 +lemma complex_i_not_one [simp]: "ii \<noteq> 1"
   2.346 +  by (simp add: complex_eq_iff)
   2.347 +
   2.348 +lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
   2.349 +  by (simp add: complex_eq_iff)
   2.350  
   2.351 -lemma complex_split_polar:
   2.352 -     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
   2.353 +lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
   2.354 +  by (simp add: complex_eq_iff)
   2.355 +
   2.356 +lemma complex_split_polar: "\<exists>r a. z = complex_of_real r * (cos a + \<i> * sin a)"
   2.357    by (simp add: complex_eq_iff polar_Ex)
   2.358  
   2.359 -
   2.360  subsection {* Vector Norm *}
   2.361  
   2.362  instantiation complex :: real_normed_field
   2.363  begin
   2.364  
   2.365 -definition complex_norm_def:
   2.366 -  "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
   2.367 +definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)"
   2.368  
   2.369  abbreviation cmod :: "complex \<Rightarrow> real"
   2.370    where "cmod \<equiv> norm"
   2.371 @@ -288,57 +220,60 @@
   2.372  definition open_complex_def:
   2.373    "open (S :: complex set) \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   2.374  
   2.375 -lemmas cmod_def = complex_norm_def
   2.376 -
   2.377 -lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
   2.378 -  by (simp add: complex_norm_def)
   2.379 -
   2.380  instance proof
   2.381    fix r :: real and x y :: complex and S :: "complex set"
   2.382    show "(norm x = 0) = (x = 0)"
   2.383 -    by (induct x) simp
   2.384 +    by (simp add: norm_complex_def complex_eq_iff)
   2.385    show "norm (x + y) \<le> norm x + norm y"
   2.386 -    by (induct x, induct y)
   2.387 -       (simp add: real_sqrt_sum_squares_triangle_ineq)
   2.388 +    by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq)
   2.389    show "norm (scaleR r x) = \<bar>r\<bar> * norm x"
   2.390 -    by (induct x)
   2.391 -       (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
   2.392 +    by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult)
   2.393    show "norm (x * y) = norm x * norm y"
   2.394 -    by (induct x, induct y)
   2.395 -       (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
   2.396 -  show "sgn x = x /\<^sub>R cmod x"
   2.397 -    by (rule complex_sgn_def)
   2.398 -  show "dist x y = cmod (x - y)"
   2.399 -    by (rule dist_complex_def)
   2.400 -  show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
   2.401 -    by (rule open_complex_def)
   2.402 -qed
   2.403 +    by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
   2.404 +qed (rule complex_sgn_def dist_complex_def open_complex_def)+
   2.405  
   2.406  end
   2.407  
   2.408 -lemma cmod_unit_one: "cmod (Complex (cos a) (sin a)) = 1"
   2.409 -  by simp
   2.410 +lemma norm_ii [simp]: "norm ii = 1"
   2.411 +  by (simp add: norm_complex_def)
   2.412  
   2.413 -lemma cmod_complex_polar:
   2.414 -  "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
   2.415 -  by (simp add: norm_mult)
   2.416 +lemma cmod_unit_one: "cmod (cos a + \<i> * sin a) = 1"
   2.417 +  by (simp add: norm_complex_def)
   2.418 +
   2.419 +lemma cmod_complex_polar: "cmod (r * (cos a + \<i> * sin a)) = \<bar>r\<bar>"
   2.420 +  by (simp add: norm_mult cmod_unit_one)
   2.421  
   2.422  lemma complex_Re_le_cmod: "Re x \<le> cmod x"
   2.423 -  unfolding complex_norm_def
   2.424 +  unfolding norm_complex_def
   2.425    by (rule real_sqrt_sum_squares_ge1)
   2.426  
   2.427  lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
   2.428 -  by (rule order_trans [OF _ norm_ge_zero], simp)
   2.429 +  by (rule order_trans [OF _ norm_ge_zero]) simp
   2.430  
   2.431 -lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
   2.432 -  by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
   2.433 +lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \<le> cmod a"
   2.434 +  by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp
   2.435  
   2.436  lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
   2.437 -  by (cases x) simp
   2.438 +  by (simp add: norm_complex_def)
   2.439  
   2.440  lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x"
   2.441 -  by (cases x) simp
   2.442 +  by (simp add: norm_complex_def)
   2.443 +
   2.444 +lemma cmod_eq_Re: "Im z = 0 \<Longrightarrow> cmod z = \<bar>Re z\<bar>"
   2.445 +  by (simp add: norm_complex_def)
   2.446 +
   2.447 +lemma cmod_eq_Im: "Re z = 0 \<Longrightarrow> cmod z = \<bar>Im z\<bar>"
   2.448 +  by (simp add: norm_complex_def)
   2.449  
   2.450 +lemma cmod_power2: "cmod z ^ 2 = (Re z)^2 + (Im z)^2"
   2.451 +  by (simp add: norm_complex_def)
   2.452 +
   2.453 +lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \<le> 0 \<longleftrightarrow> Re z = - cmod z"
   2.454 +  using abs_Re_le_cmod[of z] by auto
   2.455 +
   2.456 +lemma Im_eq_0: "\<bar>Re z\<bar> = cmod z \<Longrightarrow> Im z = 0"
   2.457 +  by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2])
   2.458 +     (auto simp add: norm_complex_def)
   2.459  
   2.460  lemma abs_sqrt_wlog:
   2.461    fixes x::"'a::linordered_idom"
   2.462 @@ -346,7 +281,7 @@
   2.463  by (metis abs_ge_zero assms power2_abs)
   2.464  
   2.465  lemma complex_abs_le_norm: "\<bar>Re z\<bar> + \<bar>Im z\<bar> \<le> sqrt 2 * norm z"
   2.466 -  unfolding complex_norm_def
   2.467 +  unfolding norm_complex_def
   2.468    apply (rule abs_sqrt_wlog [where x="Re z"])
   2.469    apply (rule abs_sqrt_wlog [where x="Im z"])
   2.470    apply (rule power2_le_imp_le)
   2.471 @@ -369,10 +304,10 @@
   2.472  subsection {* Completeness of the Complexes *}
   2.473  
   2.474  lemma bounded_linear_Re: "bounded_linear Re"
   2.475 -  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
   2.476 +  by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
   2.477  
   2.478  lemma bounded_linear_Im: "bounded_linear Im"
   2.479 -  by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def)
   2.480 +  by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def)
   2.481  
   2.482  lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re]
   2.483  lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im]
   2.484 @@ -390,127 +325,41 @@
   2.485  lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im]
   2.486  
   2.487  lemma tendsto_Complex [tendsto_intros]:
   2.488 -  assumes "(f ---> a) F" and "(g ---> b) F"
   2.489 -  shows "((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
   2.490 -proof (rule tendstoI)
   2.491 -  fix r :: real assume "0 < r"
   2.492 -  hence "0 < r / sqrt 2" by simp
   2.493 -  have "eventually (\<lambda>x. dist (f x) a < r / sqrt 2) F"
   2.494 -    using `(f ---> a) F` and `0 < r / sqrt 2` by (rule tendstoD)
   2.495 -  moreover
   2.496 -  have "eventually (\<lambda>x. dist (g x) b < r / sqrt 2) F"
   2.497 -    using `(g ---> b) F` and `0 < r / sqrt 2` by (rule tendstoD)
   2.498 -  ultimately
   2.499 -  show "eventually (\<lambda>x. dist (Complex (f x) (g x)) (Complex a b) < r) F"
   2.500 -    by (rule eventually_elim2)
   2.501 -       (simp add: dist_norm real_sqrt_sum_squares_less)
   2.502 -qed
   2.503 -
   2.504 +  "(f ---> a) F \<Longrightarrow> (g ---> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) ---> Complex a b) F"
   2.505 +  by (auto intro!: tendsto_intros)
   2.506  
   2.507  lemma tendsto_complex_iff:
   2.508    "(f ---> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) ---> Re x) F \<and> ((\<lambda>x. Im (f x)) ---> Im x) F)"
   2.509 -proof -
   2.510 -  have f: "f = (\<lambda>x. Complex (Re (f x)) (Im (f x)))" and x: "x = Complex (Re x) (Im x)"
   2.511 -    by simp_all
   2.512 -  show ?thesis
   2.513 -    apply (subst f)
   2.514 -    apply (subst x)
   2.515 -    apply (intro iffI tendsto_Complex conjI)
   2.516 -    apply (simp_all add: tendsto_Re tendsto_Im)
   2.517 -    done
   2.518 -qed
   2.519 +proof safe
   2.520 +  assume "((\<lambda>x. Re (f x)) ---> Re x) F" "((\<lambda>x. Im (f x)) ---> Im x) F"
   2.521 +  from tendsto_Complex[OF this] show "(f ---> x) F"
   2.522 +    unfolding complex.collapse .
   2.523 +qed (auto intro: tendsto_intros)
   2.524  
   2.525  instance complex :: banach
   2.526  proof
   2.527    fix X :: "nat \<Rightarrow> complex"
   2.528    assume X: "Cauchy X"
   2.529 -  from Cauchy_Re [OF X] have 1: "(\<lambda>n. Re (X n)) ----> lim (\<lambda>n. Re (X n))"
   2.530 -    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   2.531 -  from Cauchy_Im [OF X] have 2: "(\<lambda>n. Im (X n)) ----> lim (\<lambda>n. Im (X n))"
   2.532 -    by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff)
   2.533 -  have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
   2.534 -    using tendsto_Complex [OF 1 2] by simp
   2.535 -  thus "convergent X"
   2.536 -    by (rule convergentI)
   2.537 +  then have "(\<lambda>n. Complex (Re (X n)) (Im (X n))) ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
   2.538 +    by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im)
   2.539 +  then show "convergent X"
   2.540 +    unfolding complex.collapse by (rule convergentI)
   2.541  qed
   2.542  
   2.543  declare
   2.544    DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros]
   2.545  
   2.546 -
   2.547 -subsection {* The Complex Number $i$ *}
   2.548 -
   2.549 -definition "ii" :: complex  ("\<i>")
   2.550 -  where i_def: "ii \<equiv> Complex 0 1"
   2.551 -
   2.552 -lemma complex_Re_i [simp]: "Re ii = 0"
   2.553 -  by (simp add: i_def)
   2.554 -
   2.555 -lemma complex_Im_i [simp]: "Im ii = 1"
   2.556 -  by (simp add: i_def)
   2.557 -
   2.558 -lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
   2.559 -  by (simp add: i_def)
   2.560 -
   2.561 -lemma norm_ii [simp]: "norm ii = 1"
   2.562 -  by (simp add: i_def)
   2.563 -
   2.564 -lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
   2.565 -  by (simp add: complex_eq_iff)
   2.566 -
   2.567 -lemma complex_i_not_one [simp]: "ii \<noteq> 1"
   2.568 -  by (simp add: complex_eq_iff)
   2.569 -
   2.570 -lemma complex_i_not_numeral [simp]: "ii \<noteq> numeral w"
   2.571 -  by (simp add: complex_eq_iff)
   2.572 -
   2.573 -lemma complex_i_not_neg_numeral [simp]: "ii \<noteq> - numeral w"
   2.574 -  by (simp add: complex_eq_iff)
   2.575 -
   2.576 -lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a"
   2.577 -  by (simp add: complex_eq_iff)
   2.578 -
   2.579 -lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a"
   2.580 -  by (simp add: complex_eq_iff)
   2.581 -
   2.582 -lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r"
   2.583 -  by (simp add: i_def complex_of_real_def)
   2.584 -
   2.585 -lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r"
   2.586 -  by (simp add: i_def complex_of_real_def)
   2.587 -
   2.588 -lemma i_squared [simp]: "ii * ii = -1"
   2.589 -  by (simp add: i_def)
   2.590 -
   2.591 -lemma power2_i [simp]: "ii\<^sup>2 = -1"
   2.592 -  by (simp add: power2_eq_square)
   2.593 -
   2.594 -lemma inverse_i [simp]: "inverse ii = - ii"
   2.595 -  by (rule inverse_unique, simp)
   2.596 -
   2.597 -lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
   2.598 -  by (simp add: mult_assoc [symmetric])
   2.599 -
   2.600 -
   2.601  subsection {* Complex Conjugation *}
   2.602  
   2.603 -definition cnj :: "complex \<Rightarrow> complex" where
   2.604 -  "cnj z = Complex (Re z) (- Im z)"
   2.605 -
   2.606 -lemma complex_cnj [simp]: "cnj (Complex a b) = Complex a (- b)"
   2.607 -  by (simp add: cnj_def)
   2.608 -
   2.609 -lemma complex_Re_cnj [simp]: "Re (cnj x) = Re x"
   2.610 -  by (simp add: cnj_def)
   2.611 -
   2.612 -lemma complex_Im_cnj [simp]: "Im (cnj x) = - Im x"
   2.613 -  by (simp add: cnj_def)
   2.614 +primcorec cnj :: "complex \<Rightarrow> complex" where
   2.615 +  "Re (cnj z) = Re z"
   2.616 +| "Im (cnj z) = - Im z"
   2.617  
   2.618  lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)"
   2.619    by (simp add: complex_eq_iff)
   2.620  
   2.621  lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z"
   2.622 -  by (simp add: cnj_def)
   2.623 +  by (simp add: complex_eq_iff)
   2.624  
   2.625  lemma complex_cnj_zero [simp]: "cnj 0 = 0"
   2.626    by (simp add: complex_eq_iff)
   2.627 @@ -518,35 +367,35 @@
   2.628  lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)"
   2.629    by (simp add: complex_eq_iff)
   2.630  
   2.631 -lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y"
   2.632 +lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y"
   2.633    by (simp add: complex_eq_iff)
   2.634  
   2.635 -lemma cnj_setsum: "cnj (setsum f s) = (\<Sum>x\<in>s. cnj (f x))"
   2.636 -  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_add)
   2.637 +lemma cnj_setsum [simp]: "cnj (setsum f s) = (\<Sum>x\<in>s. cnj (f x))"
   2.638 +  by (induct s rule: infinite_finite_induct) auto
   2.639  
   2.640 -lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y"
   2.641 +lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y"
   2.642    by (simp add: complex_eq_iff)
   2.643  
   2.644 -lemma complex_cnj_minus: "cnj (- x) = - cnj x"
   2.645 +lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x"
   2.646    by (simp add: complex_eq_iff)
   2.647  
   2.648  lemma complex_cnj_one [simp]: "cnj 1 = 1"
   2.649    by (simp add: complex_eq_iff)
   2.650  
   2.651 -lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y"
   2.652 +lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"
   2.653    by (simp add: complex_eq_iff)
   2.654  
   2.655 -lemma cnj_setprod: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
   2.656 -  by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_mult)
   2.657 +lemma cnj_setprod [simp]: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
   2.658 +  by (induct s rule: infinite_finite_induct) auto
   2.659  
   2.660 -lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)"
   2.661 -  by (simp add: complex_inverse_def)
   2.662 +lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"
   2.663 +  by (simp add: complex_eq_iff)
   2.664  
   2.665 -lemma complex_cnj_divide: "cnj (x / y) = cnj x / cnj y"
   2.666 -  by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse)
   2.667 +lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y"
   2.668 +  by (simp add: divide_complex_def)
   2.669  
   2.670 -lemma complex_cnj_power: "cnj (x ^ n) = cnj x ^ n"
   2.671 -  by (induct n, simp_all add: complex_cnj_mult)
   2.672 +lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n"
   2.673 +  by (induct n) simp_all
   2.674  
   2.675  lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n"
   2.676    by (simp add: complex_eq_iff)
   2.677 @@ -560,11 +409,11 @@
   2.678  lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w"
   2.679    by (simp add: complex_eq_iff)
   2.680  
   2.681 -lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)"
   2.682 +lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)"
   2.683    by (simp add: complex_eq_iff)
   2.684  
   2.685  lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z"
   2.686 -  by (simp add: complex_norm_def)
   2.687 +  by (simp add: norm_complex_def)
   2.688  
   2.689  lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x"
   2.690    by (simp add: complex_eq_iff)
   2.691 @@ -585,7 +434,7 @@
   2.692    by (simp add: norm_mult power2_eq_square)
   2.693  
   2.694  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
   2.695 -  by (simp add: cmod_def power2_eq_square)
   2.696 +  by (simp add: norm_complex_def power2_eq_square)
   2.697  
   2.698  lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
   2.699    by simp
   2.700 @@ -601,70 +450,46 @@
   2.701  lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj]
   2.702  
   2.703  lemma lim_cnj: "((\<lambda>x. cnj(f x)) ---> cnj l) F \<longleftrightarrow> (f ---> l) F"
   2.704 -  by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric])
   2.705 +  by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff)
   2.706  
   2.707  lemma sums_cnj: "((\<lambda>x. cnj(f x)) sums cnj l) \<longleftrightarrow> (f sums l)"
   2.708 -  by (simp add: sums_def lim_cnj cnj_setsum [symmetric])
   2.709 +  by (simp add: sums_def lim_cnj cnj_setsum [symmetric] del: cnj_setsum)
   2.710  
   2.711  
   2.712  subsection{*Basic Lemmas*}
   2.713  
   2.714  lemma complex_eq_0: "z=0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0"
   2.715 -  by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff)
   2.716 +  by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff)
   2.717  
   2.718  lemma complex_neq_0: "z\<noteq>0 \<longleftrightarrow> (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0"
   2.719 -by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
   2.720 +  by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff)
   2.721  
   2.722  lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z"
   2.723 -apply (cases z, auto)
   2.724 -by (metis complex_of_real_def of_real_add of_real_power power2_eq_square)
   2.725 +by (cases z)
   2.726 +   (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric]
   2.727 +         simp del: of_real_power)
   2.728  
   2.729 -lemma complex_div_eq_0: 
   2.730 -    "(Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0) & (Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0)"
   2.731 -proof (cases "b=0")
   2.732 -  case True then show ?thesis by auto
   2.733 +lemma re_complex_div_eq_0: "Re (a / b) = 0 \<longleftrightarrow> Re (a * cnj b) = 0"
   2.734 +  by (auto simp add: Re_divide)
   2.735 +  
   2.736 +lemma im_complex_div_eq_0: "Im (a / b) = 0 \<longleftrightarrow> Im (a * cnj b) = 0"
   2.737 +  by (auto simp add: Im_divide)
   2.738 +
   2.739 +lemma complex_div_gt_0: 
   2.740 +  "(Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0) \<and> (Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0)"
   2.741 +proof cases
   2.742 +  assume "b = 0" then show ?thesis by auto
   2.743  next
   2.744 -  case False
   2.745 -  show ?thesis
   2.746 -  proof (cases b)
   2.747 -    case (Complex x y)
   2.748 -    then have "x\<^sup>2 + y\<^sup>2 > 0"
   2.749 -      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
   2.750 -    then have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
   2.751 -      by (metis add_divide_distrib)
   2.752 -    with Complex False show ?thesis
   2.753 -      by (auto simp: complex_divide_def)
   2.754 -  qed
   2.755 +  assume "b \<noteq> 0"
   2.756 +  then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2"
   2.757 +    by (simp add: complex_eq_iff sum_power2_gt_zero_iff)
   2.758 +  then show ?thesis
   2.759 +    by (simp add: Re_divide Im_divide zero_less_divide_iff)
   2.760  qed
   2.761  
   2.762 -lemma re_complex_div_eq_0: "Re(a / b) = 0 \<longleftrightarrow> Re(a * cnj b) = 0"
   2.763 -  and im_complex_div_eq_0: "Im(a / b) = 0 \<longleftrightarrow> Im(a * cnj b) = 0"
   2.764 -using complex_div_eq_0 by auto
   2.765 -
   2.766 -
   2.767 -lemma complex_div_gt_0: 
   2.768 -    "(Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0) & (Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0)"
   2.769 -proof (cases "b=0")
   2.770 -  case True then show ?thesis by auto
   2.771 -next
   2.772 -  case False
   2.773 -  show ?thesis
   2.774 -  proof (cases b)
   2.775 -    case (Complex x y)
   2.776 -    then have "x\<^sup>2 + y\<^sup>2 > 0"
   2.777 -      by (metis Complex_eq_0 False sum_power2_gt_zero_iff)
   2.778 -    moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)"
   2.779 -      by (metis add_divide_distrib)
   2.780 -    ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2`
   2.781 -      apply (simp add: complex_divide_def  zero_less_divide_iff less_divide_eq)
   2.782 -      apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left)
   2.783 -      done
   2.784 -  qed
   2.785 -qed
   2.786 -
   2.787 -lemma re_complex_div_gt_0: "Re(a / b) > 0 \<longleftrightarrow> Re(a * cnj b) > 0"
   2.788 -  and im_complex_div_gt_0: "Im(a / b) > 0 \<longleftrightarrow> Im(a * cnj b) > 0"
   2.789 -using complex_div_gt_0 by auto
   2.790 +lemma re_complex_div_gt_0: "Re (a / b) > 0 \<longleftrightarrow> Re (a * cnj b) > 0"
   2.791 +  and im_complex_div_gt_0: "Im (a / b) > 0 \<longleftrightarrow> Im (a * cnj b) > 0"
   2.792 +  using complex_div_gt_0 by auto
   2.793  
   2.794  lemma re_complex_div_ge_0: "Re(a / b) \<ge> 0 \<longleftrightarrow> Re(a * cnj b) \<ge> 0"
   2.795    by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0)
   2.796 @@ -684,17 +509,17 @@
   2.797  lemma im_complex_div_le_0: "Im(a / b) \<le> 0 \<longleftrightarrow> Im(a * cnj b) \<le> 0"
   2.798    by (metis im_complex_div_gt_0 not_le)
   2.799  
   2.800 -lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s"
   2.801 +lemma Re_setsum[simp]: "Re (setsum f s) = (\<Sum>x\<in>s. Re (f x))"
   2.802    by (induct s rule: infinite_finite_induct) auto
   2.803  
   2.804 -lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s"
   2.805 +lemma Im_setsum[simp]: "Im (setsum f s) = (\<Sum>x\<in>s. Im(f x))"
   2.806    by (induct s rule: infinite_finite_induct) auto
   2.807  
   2.808  lemma sums_complex_iff: "f sums x \<longleftrightarrow> ((\<lambda>x. Re (f x)) sums Re x) \<and> ((\<lambda>x. Im (f x)) sums Im x)"
   2.809    unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum ..
   2.810    
   2.811  lemma summable_complex_iff: "summable f \<longleftrightarrow> summable (\<lambda>x. Re (f x)) \<and>  summable (\<lambda>x. Im (f x))"
   2.812 -  unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps)
   2.813 +  unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel)
   2.814  
   2.815  lemma summable_complex_of_real [simp]: "summable (\<lambda>n. complex_of_real (f n)) \<longleftrightarrow> summable f"
   2.816    unfolding summable_complex_iff by simp
   2.817 @@ -705,30 +530,14 @@
   2.818  lemma summable_Im: "summable f \<Longrightarrow> summable (\<lambda>x. Im (f x))"
   2.819    unfolding summable_complex_iff by blast
   2.820  
   2.821 -lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
   2.822 -  by (induct s rule: infinite_finite_induct) auto
   2.823 -
   2.824 -lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
   2.825 -  by (metis Complex_setsum')
   2.826 -
   2.827 -lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s"
   2.828 -  by (induct s rule: infinite_finite_induct) auto
   2.829 -
   2.830 -lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s"
   2.831 -  by (induct s rule: infinite_finite_induct) auto
   2.832 +lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   2.833 +  by (auto simp: Reals_def complex_eq_iff)
   2.834  
   2.835  lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
   2.836 -by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj 
   2.837 -          complex_of_real_def equal_neg_zero)
   2.838 -
   2.839 -lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
   2.840 -  by (metis Reals_of_real complex_of_real_def)
   2.841 +  by (auto simp: complex_is_Real_iff complex_eq_iff)
   2.842  
   2.843  lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
   2.844 -  by (metis Re_complex_of_real Reals_cases norm_of_real)
   2.845 -
   2.846 -lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   2.847 -  by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj)
   2.848 +  by (simp add: complex_is_Real_iff norm_complex_def)
   2.849  
   2.850  lemma series_comparison_complex:
   2.851    fixes f:: "nat \<Rightarrow> 'a::banach"
   2.852 @@ -753,20 +562,15 @@
   2.853  
   2.854  subsubsection {* $\cos \theta + i \sin \theta$ *}
   2.855  
   2.856 -definition cis :: "real \<Rightarrow> complex" where
   2.857 -  "cis a = Complex (cos a) (sin a)"
   2.858 -
   2.859 -lemma Re_cis [simp]: "Re (cis a) = cos a"
   2.860 -  by (simp add: cis_def)
   2.861 -
   2.862 -lemma Im_cis [simp]: "Im (cis a) = sin a"
   2.863 -  by (simp add: cis_def)
   2.864 +primcorec cis :: "real \<Rightarrow> complex" where
   2.865 +  "Re (cis a) = cos a"
   2.866 +| "Im (cis a) = sin a"
   2.867  
   2.868  lemma cis_zero [simp]: "cis 0 = 1"
   2.869 -  by (simp add: cis_def)
   2.870 +  by (simp add: complex_eq_iff)
   2.871  
   2.872  lemma norm_cis [simp]: "norm (cis a) = 1"
   2.873 -  by (simp add: cis_def)
   2.874 +  by (simp add: norm_complex_def)
   2.875  
   2.876  lemma sgn_cis [simp]: "sgn (cis a) = cis a"
   2.877    by (simp add: sgn_div_norm)
   2.878 @@ -775,16 +579,16 @@
   2.879    by (metis norm_cis norm_zero zero_neq_one)
   2.880  
   2.881  lemma cis_mult: "cis a * cis b = cis (a + b)"
   2.882 -  by (simp add: cis_def cos_add sin_add)
   2.883 +  by (simp add: complex_eq_iff cos_add sin_add)
   2.884  
   2.885  lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
   2.886    by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
   2.887  
   2.888  lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
   2.889 -  by (simp add: cis_def)
   2.890 +  by (simp add: complex_eq_iff)
   2.891  
   2.892  lemma cis_divide: "cis a / cis b = cis (a - b)"
   2.893 -  by (simp add: complex_divide_def cis_mult)
   2.894 +  by (simp add: divide_complex_def cis_mult)
   2.895  
   2.896  lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
   2.897    by (auto simp add: DeMoivre)
   2.898 @@ -792,9 +596,12 @@
   2.899  lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
   2.900    by (auto simp add: DeMoivre)
   2.901  
   2.902 +lemma cis_pi: "cis pi = -1"
   2.903 +  by (simp add: complex_eq_iff)
   2.904 +
   2.905  subsubsection {* $r(\cos \theta + i \sin \theta)$ *}
   2.906  
   2.907 -definition rcis :: "[real, real] \<Rightarrow> complex" where
   2.908 +definition rcis :: "real \<Rightarrow> real \<Rightarrow> complex" where
   2.909    "rcis r a = complex_of_real r * cis a"
   2.910  
   2.911  lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
   2.912 @@ -838,26 +645,24 @@
   2.913  abbreviation expi :: "complex \<Rightarrow> complex"
   2.914    where "expi \<equiv> exp"
   2.915  
   2.916 -lemma cis_conv_exp: "cis b = exp (Complex 0 b)"
   2.917 -proof (rule complex_eqI)
   2.918 -  { fix n have "Complex 0 b ^ n =
   2.919 -    real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)"
   2.920 -      apply (induct n)
   2.921 -      apply (simp add: cos_coeff_def sin_coeff_def)
   2.922 -      apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc)
   2.923 -      done } note * = this
   2.924 -  show "Re (cis b) = Re (exp (Complex 0 b))"
   2.925 -    unfolding exp_def cis_def cos_def
   2.926 -    by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic],
   2.927 -      simp add: * mult_assoc [symmetric])
   2.928 -  show "Im (cis b) = Im (exp (Complex 0 b))"
   2.929 -    unfolding exp_def cis_def sin_def
   2.930 -    by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic],
   2.931 -      simp add: * mult_assoc [symmetric])
   2.932 +lemma cis_conv_exp: "cis b = exp (\<i> * b)"
   2.933 +proof -
   2.934 +  { fix n :: nat
   2.935 +    have "\<i> ^ n = fact n *\<^sub>R (cos_coeff n + \<i> * sin_coeff n)"
   2.936 +      by (induct n)
   2.937 +         (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps
   2.938 +                        power2_eq_square real_of_nat_Suc add_nonneg_eq_0_iff
   2.939 +                        real_of_nat_def[symmetric])
   2.940 +    then have "(\<i> * complex_of_real b) ^ n /\<^sub>R fact n =
   2.941 +        of_real (cos_coeff n * b^n) + \<i> * of_real (sin_coeff n * b^n)"
   2.942 +      by (simp add: field_simps) }
   2.943 +  then show ?thesis
   2.944 +    by (auto simp add: cis.ctr exp_def simp del: of_real_mult
   2.945 +             intro!: sums_unique sums_add sums_mult sums_of_real sin_converges cos_converges)
   2.946  qed
   2.947  
   2.948 -lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
   2.949 -  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
   2.950 +lemma expi_def: "expi z = exp (Re z) * cis (Im z)"
   2.951 +  unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp
   2.952  
   2.953  lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
   2.954    unfolding expi_def by simp
   2.955 @@ -872,7 +677,7 @@
   2.956  done
   2.957  
   2.958  lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1"
   2.959 -  by (simp add: expi_def cis_def)
   2.960 +  by (simp add: expi_def complex_eq_iff)
   2.961  
   2.962  subsubsection {* Complex argument *}
   2.963  
   2.964 @@ -882,15 +687,6 @@
   2.965  lemma arg_zero: "arg 0 = 0"
   2.966    by (simp add: arg_def)
   2.967  
   2.968 -lemma of_nat_less_of_int_iff: (* TODO: move *)
   2.969 -  "(of_nat n :: 'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
   2.970 -  by (metis of_int_of_nat_eq of_int_less_iff)
   2.971 -
   2.972 -lemma real_of_nat_less_numeral_iff [simp]: (* TODO: move *)
   2.973 -  "real (n::nat) < numeral w \<longleftrightarrow> n < numeral w"
   2.974 -  using of_nat_less_of_int_iff [of n "numeral w", where 'a=real]
   2.975 -  by (simp add: real_of_nat_def zless_nat_eq_int_zless [symmetric])
   2.976 -
   2.977  lemma arg_unique:
   2.978    assumes "sgn z = cis x" and "-pi < x" and "x \<le> pi"
   2.979    shows "arg z = x"
   2.980 @@ -923,13 +719,12 @@
   2.981    def b \<equiv> "if 0 < r then a else a + pi"
   2.982    have b: "sgn z = cis b"
   2.983      unfolding z b_def rcis_def using `r \<noteq> 0`
   2.984 -    by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def)
   2.985 +    by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff)
   2.986    have cis_2pi_nat: "\<And>n. cis (2 * pi * real_of_nat n) = 1"
   2.987 -    by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric],
   2.988 -      simp add: cis_def)
   2.989 +    by (induct_tac n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff)
   2.990    have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
   2.991 -    by (case_tac x rule: int_diff_cases,
   2.992 -      simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
   2.993 +    by (case_tac x rule: int_diff_cases)
   2.994 +       (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
   2.995    def c \<equiv> "b - 2*pi * of_int \<lceil>(b - pi) / (2*pi)\<rceil>"
   2.996    have "sgn z = cis c"
   2.997      unfolding b c_def
   2.998 @@ -941,22 +736,136 @@
   2.999  qed
  2.1000  
  2.1001  lemma arg_bounded: "- pi < arg z \<and> arg z \<le> pi"
  2.1002 -  by (cases "z = 0", simp_all add: arg_zero arg_correct)
  2.1003 +  by (cases "z = 0") (simp_all add: arg_zero arg_correct)
  2.1004  
  2.1005  lemma cis_arg: "z \<noteq> 0 \<Longrightarrow> cis (arg z) = sgn z"
  2.1006    by (simp add: arg_correct)
  2.1007  
  2.1008  lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"
  2.1009 -  by (cases "z = 0", simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
  2.1010 +  by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
  2.1011 +
  2.1012 +lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
  2.1013 +  using cis_arg [of y] by (simp add: complex_eq_iff)
  2.1014 +
  2.1015 +subsection {* Square root of complex numbers *}
  2.1016 +
  2.1017 +primcorec csqrt :: "complex \<Rightarrow> complex" where
  2.1018 +  "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)"
  2.1019 +| "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)"
  2.1020 +
  2.1021 +lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \<Longrightarrow> Re x \<ge> 0 \<Longrightarrow> csqrt x = sqrt (Re x)"
  2.1022 +  by (simp add: complex_eq_iff norm_complex_def)
  2.1023 +
  2.1024 +lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \<Longrightarrow> Re x \<le> 0 \<Longrightarrow> csqrt x = \<i> * sqrt \<bar>Re x\<bar>"
  2.1025 +  by (simp add: complex_eq_iff norm_complex_def)
  2.1026 +
  2.1027 +lemma csqrt_0 [simp]: "csqrt 0 = 0"
  2.1028 +  by simp
  2.1029 +
  2.1030 +lemma csqrt_1 [simp]: "csqrt 1 = 1"
  2.1031 +  by simp
  2.1032 +
  2.1033 +lemma csqrt_ii [simp]: "csqrt \<i> = (1 + \<i>) / sqrt 2"
  2.1034 +  by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt)
  2.1035  
  2.1036 -lemma cos_arg_i_mult_zero [simp]:
  2.1037 -     "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
  2.1038 -  using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
  2.1039 +lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
  2.1040 +proof cases
  2.1041 +  assume "Im z = 0" then show ?thesis
  2.1042 +    using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"]
  2.1043 +    by (cases "0::real" "Re z" rule: linorder_cases)
  2.1044 +       (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re)
  2.1045 +next
  2.1046 +  assume "Im z \<noteq> 0"
  2.1047 +  moreover
  2.1048 +  have "cmod z * cmod z - Re z * Re z = Im z * Im z"
  2.1049 +    by (simp add: norm_complex_def power2_eq_square)
  2.1050 +  moreover
  2.1051 +  have "\<bar>Re z\<bar> \<le> cmod z"
  2.1052 +    by (simp add: norm_complex_def)
  2.1053 +  ultimately show ?thesis
  2.1054 +    by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq
  2.1055 +                  field_simps real_sqrt_mult[symmetric] real_sqrt_divide)
  2.1056 +qed
  2.1057 +
  2.1058 +lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
  2.1059 +  by auto (metis power2_csqrt power_eq_0_iff)
  2.1060 +
  2.1061 +lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
  2.1062 +  by auto (metis power2_csqrt power2_eq_1_iff)
  2.1063 +
  2.1064 +lemma csqrt_principal: "0 < Re (csqrt z) \<or> Re (csqrt z) = 0 \<and> 0 \<le> Im (csqrt z)"
  2.1065 +  by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0)
  2.1066 +
  2.1067 +lemma Re_csqrt: "0 \<le> Re (csqrt z)"
  2.1068 +  by (metis csqrt_principal le_less)
  2.1069 +
  2.1070 +lemma csqrt_square:
  2.1071 +  assumes "0 < Re b \<or> (Re b = 0 \<and> 0 \<le> Im b)"
  2.1072 +  shows "csqrt (b^2) = b"
  2.1073 +proof -
  2.1074 +  have "csqrt (b^2) = b \<or> csqrt (b^2) = - b"
  2.1075 +    unfolding power2_eq_iff[symmetric] by (simp add: power2_csqrt)
  2.1076 +  moreover have "csqrt (b^2) \<noteq> -b \<or> b = 0"
  2.1077 +    using csqrt_principal[of "b ^ 2"] assms by (intro disjCI notI) (auto simp: complex_eq_iff)
  2.1078 +  ultimately show ?thesis
  2.1079 +    by auto
  2.1080 +qed
  2.1081 +
  2.1082 +lemma csqrt_minus [simp]: 
  2.1083 +  assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
  2.1084 +  shows "csqrt (- x) = \<i> * csqrt x"
  2.1085 +proof -
  2.1086 +  have "csqrt ((\<i> * csqrt x)^2) = \<i> * csqrt x"
  2.1087 +  proof (rule csqrt_square)
  2.1088 +    have "Im (csqrt x) \<le> 0"
  2.1089 +      using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod)
  2.1090 +    then show "0 < Re (\<i> * csqrt x) \<or> Re (\<i> * csqrt x) = 0 \<and> 0 \<le> Im (\<i> * csqrt x)"
  2.1091 +      by (auto simp add: Re_csqrt simp del: csqrt.simps)
  2.1092 +  qed
  2.1093 +  also have "(\<i> * csqrt x)^2 = - x"
  2.1094 +    by (simp add: power2_csqrt power_mult_distrib)
  2.1095 +  finally show ?thesis .
  2.1096 +qed
  2.1097  
  2.1098  text {* Legacy theorem names *}
  2.1099  
  2.1100  lemmas expand_complex_eq = complex_eq_iff
  2.1101  lemmas complex_Re_Im_cancel_iff = complex_eq_iff
  2.1102  lemmas complex_equality = complex_eqI
  2.1103 +lemmas cmod_def = norm_complex_def
  2.1104 +lemmas complex_norm_def = norm_complex_def
  2.1105 +lemmas complex_divide_def = divide_complex_def
  2.1106 +
  2.1107 +lemma legacy_Complex_simps:
  2.1108 +  shows Complex_eq_0: "Complex a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
  2.1109 +    and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)"
  2.1110 +    and complex_minus: "- (Complex a b) = Complex (- a) (- b)"
  2.1111 +    and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)"
  2.1112 +    and Complex_eq_1: "Complex a b = 1 \<longleftrightarrow> a = 1 \<and> b = 0"
  2.1113 +    and Complex_eq_neg_1: "Complex a b = - 1 \<longleftrightarrow> a = - 1 \<and> b = 0"
  2.1114 +    and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)"
  2.1115 +    and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))"
  2.1116 +    and Complex_eq_numeral: "Complex a b = numeral w \<longleftrightarrow> a = numeral w \<and> b = 0"
  2.1117 +    and Complex_eq_neg_numeral: "Complex a b = - numeral w \<longleftrightarrow> a = - numeral w \<and> b = 0"
  2.1118 +    and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)"
  2.1119 +    and Complex_eq_i: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
  2.1120 +    and i_mult_Complex: "ii * Complex a b = Complex (- b) a"
  2.1121 +    and Complex_mult_i: "Complex a b * ii = Complex (- b) a"
  2.1122 +    and i_complex_of_real: "ii * complex_of_real r = Complex 0 r"
  2.1123 +    and complex_of_real_i: "complex_of_real r * ii = Complex 0 r"
  2.1124 +    and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y"
  2.1125 +    and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y"
  2.1126 +    and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)"
  2.1127 +    and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
  2.1128 +    and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa & y = 0)"
  2.1129 +    and complex_cn: "cnj (Complex a b) = Complex a (- b)"
  2.1130 +    and Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0"
  2.1131 +    and Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s"
  2.1132 +    and complex_of_real_def: "complex_of_real r = Complex r 0"
  2.1133 +    and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
  2.1134 +  by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq)
  2.1135 +
  2.1136 +lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
  2.1137 +  by (metis Reals_of_real complex_of_real_def)
  2.1138  
  2.1139  end
     3.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue May 06 23:35:24 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed May 07 12:25:35 2014 +0200
     3.3 @@ -235,8 +235,9 @@
     3.4          from xt1(5)[OF `0 \<le> ?E mod 2` this]
     3.5          show ?thesis by auto
     3.6        qed
     3.7 -      hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)" by auto
     3.8 -      hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" unfolding real_sqrt_abs2 by auto
     3.9 +      hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)"
    3.10 +        by (auto simp del: real_sqrt_four)
    3.11 +      hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" by auto
    3.12  
    3.13        have E_eq: "2 powr ?E = 2 powr (?E div 2 + ?E div 2 + ?E mod 2)" by auto
    3.14        have "sqrt (2 powr ?E) = sqrt (2 powr (?E div 2) * 2 powr (?E div 2) * 2 powr (?E mod 2))"
     4.1 --- a/src/HOL/Int.thy	Tue May 06 23:35:24 2014 +0200
     4.2 +++ b/src/HOL/Int.thy	Wed May 07 12:25:35 2014 +0200
     4.3 @@ -293,6 +293,10 @@
     4.4  
     4.5  end
     4.6  
     4.7 +lemma of_nat_less_of_int_iff:
     4.8 +  "(of_nat n::'a::linordered_idom) < of_int x \<longleftrightarrow> int n < x"
     4.9 +  by (metis of_int_of_nat_eq of_int_less_iff)
    4.10 +
    4.11  lemma of_int_eq_id [simp]: "of_int = id"
    4.12  proof
    4.13    fix z show "of_int z = id z"
     5.1 --- a/src/HOL/Library/Extended_Real.thy	Tue May 06 23:35:24 2014 +0200
     5.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed May 07 12:25:35 2014 +0200
     5.3 @@ -1894,7 +1894,7 @@
     5.4    by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1])
     5.5  
     5.6  lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \<longleftrightarrow> numeral m < n"
     5.7 -  by (cases n) (auto simp: real_of_nat_less_iff[symmetric])
     5.8 +  by (cases n) auto
     5.9  
    5.10  lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \<le> ereal_of_enat n \<longleftrightarrow> 0 \<le> n"
    5.11    by (cases n) (auto simp: enat_0[symmetric])
     6.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue May 06 23:35:24 2014 +0200
     6.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed May 07 12:25:35 2014 +0200
     6.3 @@ -6,126 +6,12 @@
     6.4  imports Polynomial Complex_Main
     6.5  begin
     6.6  
     6.7 -subsection {* Square root of complex numbers *}
     6.8 -
     6.9 -definition csqrt :: "complex \<Rightarrow> complex"
    6.10 -where
    6.11 -  "csqrt z =
    6.12 -    (if Im z = 0 then
    6.13 -       if 0 \<le> Re z then Complex (sqrt(Re z)) 0
    6.14 -       else Complex 0 (sqrt(- Re z))
    6.15 -     else Complex (sqrt((cmod z + Re z) /2)) ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))"
    6.16 -
    6.17 -lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z"
    6.18 -proof -
    6.19 -  obtain x y where xy: "z = Complex x y" by (cases z)
    6.20 -  {
    6.21 -    assume y0: "y = 0"
    6.22 -    {
    6.23 -      assume x0: "x \<ge> 0"
    6.24 -      then have ?thesis
    6.25 -        using y0 xy real_sqrt_pow2[OF x0]
    6.26 -        by (simp add: csqrt_def power2_eq_square)
    6.27 -    }
    6.28 -    moreover
    6.29 -    {
    6.30 -      assume "\<not> x \<ge> 0"
    6.31 -      then have x0: "- x \<ge> 0" by arith
    6.32 -      then have ?thesis
    6.33 -        using y0 xy real_sqrt_pow2[OF x0]
    6.34 -        by (simp add: csqrt_def power2_eq_square)
    6.35 -    }
    6.36 -    ultimately have ?thesis by blast
    6.37 -  }
    6.38 -  moreover
    6.39 -  {
    6.40 -    assume y0: "y \<noteq> 0"
    6.41 -    {
    6.42 -      fix x y
    6.43 -      let ?z = "Complex x y"
    6.44 -      from abs_Re_le_cmod[of ?z] have tha: "abs x \<le> cmod ?z"
    6.45 -        by auto
    6.46 -      then have "cmod ?z - x \<ge> 0" "cmod ?z + x \<ge> 0"
    6.47 -        by arith+
    6.48 -      then have "(sqrt (x * x + y * y) + x) / 2 \<ge> 0" "(sqrt (x * x + y * y) - x) / 2 \<ge> 0"
    6.49 -        by (simp_all add: power2_eq_square)
    6.50 -    }
    6.51 -    note th = this
    6.52 -    have sq4: "\<And>x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2"
    6.53 -      by (simp add: power2_eq_square)
    6.54 -    from th[of x y]
    6.55 -    have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2"
    6.56 -      "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2"
    6.57 -      unfolding sq4 by simp_all
    6.58 -    then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) -
    6.59 -        sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x"
    6.60 -      unfolding power2_eq_square by simp
    6.61 -    have "sqrt 4 = sqrt (2\<^sup>2)"
    6.62 -      by simp
    6.63 -    then have sqrt4: "sqrt 4 = 2"
    6.64 -      by (simp only: real_sqrt_abs)
    6.65 -    have th2: "2 * (y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \<bar>y\<bar> = y"
    6.66 -      using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0
    6.67 -      unfolding power2_eq_square
    6.68 -      by (simp add: algebra_simps real_sqrt_divide sqrt4)
    6.69 -    from y0 xy have ?thesis
    6.70 -      apply (simp add: csqrt_def power2_eq_square)
    6.71 -      apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y]
    6.72 -        real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square]
    6.73 -        real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square]
    6.74 -        real_sqrt_mult[symmetric])
    6.75 -      using th1 th2  ..
    6.76 -  }
    6.77 -  ultimately show ?thesis by blast
    6.78 -qed
    6.79 -
    6.80 -lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
    6.81 -  by (simp add: csqrt_def)
    6.82 -
    6.83 -lemma csqrt_0 [simp]: "csqrt 0 = 0"
    6.84 -  by (simp add: csqrt_def)
    6.85 -
    6.86 -lemma csqrt_1 [simp]: "csqrt 1 = 1"
    6.87 -  by (simp add: csqrt_def)
    6.88 -
    6.89 -lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
    6.90 -proof (cases z)
    6.91 -  case (Complex x y)
    6.92 -  then show ?thesis
    6.93 -    using real_sqrt_sum_squares_ge1 [of "x" y]
    6.94 -          real_sqrt_sum_squares_ge1 [of "-x" y]
    6.95 -          real_sqrt_sum_squares_eq_cancel [of x y]
    6.96 -    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
    6.97 -    apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1)
    6.98 -    apply (metis add_commute less_eq_real_def power_minus_Bit0
    6.99 -            real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
   6.100 -    done
   6.101 -qed
   6.102 -
   6.103 -lemma Re_csqrt: "0 \<le> Re(csqrt z)"
   6.104 -  by (metis csqrt_principal le_less)
   6.105 -
   6.106 -lemma csqrt_square: "0 < Re z \<or> Re z = 0 \<and> 0 \<le> Im z \<Longrightarrow> csqrt (z\<^sup>2) = z"
   6.107 -  using csqrt [of "z\<^sup>2"] csqrt_principal [of "z\<^sup>2"]
   6.108 -  by (cases z) (auto simp: power2_eq_iff)
   6.109 -
   6.110 -lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
   6.111 -  by auto (metis csqrt power_eq_0_iff)
   6.112 -
   6.113 -lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
   6.114 -  by auto (metis csqrt power2_eq_1_iff)
   6.115 -
   6.116 -
   6.117  subsection {* More lemmas about module of complex numbers *}
   6.118  
   6.119 -lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
   6.120 -  by (rule of_real_power [symmetric])
   6.121 -
   6.122  text{* The triangle inequality for cmod *}
   6.123  lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
   6.124    using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
   6.125  
   6.126 -
   6.127  subsection {* Basic lemmas about polynomials *}
   6.128  
   6.129  lemma poly_bound_exists:
   6.130 @@ -281,7 +167,7 @@
   6.131      with IH[rule_format, of m] obtain z where z: "?P z m"
   6.132        by blast
   6.133      from z have "?P (csqrt z) n"
   6.134 -      by (simp add: m power_mult csqrt)
   6.135 +      by (simp add: m power_mult power2_csqrt)
   6.136      then have "\<exists>z. ?P z n" ..
   6.137    }
   6.138    moreover
   6.139 @@ -319,7 +205,7 @@
   6.140      let ?w = "v / complex_of_real (root n (cmod b))"
   6.141      from odd_real_root_pow[OF o, of "cmod b"]
   6.142      have th1: "?w ^ n = v^n / complex_of_real (cmod b)"
   6.143 -      by (simp add: power_divide complex_of_real_power)
   6.144 +      by (simp add: power_divide of_real_power[symmetric])
   6.145      have th2:"cmod (complex_of_real (cmod b) / b) = 1"
   6.146        using b by (simp add: norm_divide)
   6.147      then have th3: "cmod (complex_of_real (cmod b) / b) \<ge> 0"
   6.148 @@ -600,21 +486,6 @@
   6.149    ultimately show ?thesis by blast
   6.150  qed
   6.151  
   6.152 -lemma "(rcis (sqrt (abs r)) (a/2))\<^sup>2 = rcis (abs r) a"
   6.153 -  unfolding power2_eq_square
   6.154 -  apply (simp add: rcis_mult)
   6.155 -  apply (simp add: power2_eq_square[symmetric])
   6.156 -  done
   6.157 -
   6.158 -lemma cispi: "cis pi = -1"
   6.159 -  by (simp add: cis_def)
   6.160 -
   6.161 -lemma "(rcis (sqrt (abs r)) ((pi + a) / 2))\<^sup>2 = rcis (- abs r) a"
   6.162 -  unfolding power2_eq_square
   6.163 -  apply (simp add: rcis_mult add_divide_distrib)
   6.164 -  apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric])
   6.165 -  done
   6.166 -
   6.167  text {* Nonzero polynomial in z goes to infinity as z does. *}
   6.168  
   6.169  lemma poly_infinity:
     7.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Tue May 06 23:35:24 2014 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Wed May 07 12:25:35 2014 +0200
     7.3 @@ -28,6 +28,7 @@
     7.4    fixes c :: "'a::real_field"
     7.5    shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)"
     7.6    by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps)
     7.7 +
     7.8  lemma linear_times:
     7.9    fixes c::"'a::real_algebra" shows "linear (\<lambda>x. c * x)"
    7.10    by (auto simp: linearI distrib_left)
    7.11 @@ -260,8 +261,8 @@
    7.12  by (metis real_lim_sequentially setsum_in_Reals)
    7.13  
    7.14  lemma Lim_null_comparison_Re:
    7.15 -   "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F \<Longrightarrow>  (g ---> 0) F \<Longrightarrow> (f ---> 0) F"
    7.16 -  by (metis Lim_null_comparison complex_Re_zero tendsto_Re)
    7.17 +  assumes "eventually (\<lambda>x. norm(f x) \<le> Re(g x)) F" "(g ---> 0) F" shows "(f ---> 0) F"
    7.18 +  by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp
    7.19  
    7.20  subsection{*Holomorphic functions*}
    7.21  
     8.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Tue May 06 23:35:24 2014 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed May 07 12:25:35 2014 +0200
     8.3 @@ -3716,7 +3716,7 @@
     8.4      where b: "\<forall>x\<in>s. 0 < b x \<and> cball x (b x) \<subseteq> s"
     8.5      using bchoice[of s "\<lambda>x e. e > 0 \<and> cball x e \<subseteq> s"] by auto
     8.6    have "b ` t \<noteq> {}"
     8.7 -    unfolding i_def using obt by auto
     8.8 +    using obt by auto
     8.9    def i \<equiv> "b ` t"
    8.10  
    8.11    show "\<exists>e > 0.
     9.1 --- a/src/HOL/NSA/CLim.thy	Tue May 06 23:35:24 2014 +0200
     9.2 +++ b/src/HOL/NSA/CLim.thy	Wed May 07 12:25:35 2014 +0200
     9.3 @@ -58,12 +58,12 @@
     9.4  lemma LIM_cnj:
     9.5    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
     9.6    shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
     9.7 -by (simp add: LIM_eq complex_cnj_diff [symmetric])
     9.8 +by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
     9.9  
    9.10  lemma LIM_cnj_iff:
    9.11    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    9.12    shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
    9.13 -by (simp add: LIM_eq complex_cnj_diff [symmetric])
    9.14 +by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff)
    9.15  
    9.16  lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
    9.17  by transfer (rule refl)
    9.18 @@ -148,7 +148,7 @@
    9.19  text{*Nonstandard version*}
    9.20  lemma NSCDERIV_pow:
    9.21       "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
    9.22 -by (simp add: NSDERIV_DERIV_iff)
    9.23 +by (simp add: NSDERIV_DERIV_iff del: of_real_real_of_nat_eq)
    9.24  
    9.25  text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
    9.26  lemma NSCDERIV_inverse:
    10.1 --- a/src/HOL/NSA/NSCA.thy	Tue May 06 23:35:24 2014 +0200
    10.2 +++ b/src/HOL/NSA/NSCA.thy	Wed May 07 12:25:35 2014 +0200
    10.3 @@ -291,10 +291,10 @@
    10.4  done
    10.5  
    10.6  lemma hRe_diff [simp]: "\<And>x y. hRe (x - y) = hRe x - hRe y"
    10.7 -by transfer (rule complex_Re_diff)
    10.8 +by transfer simp
    10.9  
   10.10  lemma hIm_diff [simp]: "\<And>x y. hIm (x - y) = hIm x - hIm y"
   10.11 -by transfer (rule complex_Im_diff)
   10.12 +by transfer simp
   10.13  
   10.14  lemma approx_hRe: "x \<approx> y \<Longrightarrow> hRe x \<approx> hRe y"
   10.15  unfolding approx_def by (drule Infinitesimal_hRe) simp
    11.1 --- a/src/HOL/NSA/NSComplex.thy	Tue May 06 23:35:24 2014 +0200
    11.2 +++ b/src/HOL/NSA/NSComplex.thy	Wed May 07 12:25:35 2014 +0200
    11.3 @@ -129,33 +129,33 @@
    11.4  by transfer (rule complex_equality)
    11.5  
    11.6  lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0"
    11.7 -by transfer (rule complex_Re_zero)
    11.8 +by transfer simp
    11.9  
   11.10  lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0"
   11.11 -by transfer (rule complex_Im_zero)
   11.12 +by transfer simp
   11.13  
   11.14  lemma hcomplex_hRe_one [simp]: "hRe 1 = 1"
   11.15 -by transfer (rule complex_Re_one)
   11.16 +by transfer simp
   11.17  
   11.18  lemma hcomplex_hIm_one [simp]: "hIm 1 = 0"
   11.19 -by transfer (rule complex_Im_one)
   11.20 +by transfer simp
   11.21  
   11.22  
   11.23  subsection{*Addition for Nonstandard Complex Numbers*}
   11.24  
   11.25  lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)"
   11.26 -by transfer (rule complex_Re_add)
   11.27 +by transfer simp
   11.28  
   11.29  lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)"
   11.30 -by transfer (rule complex_Im_add)
   11.31 +by transfer simp
   11.32  
   11.33  subsection{*More Minus Laws*}
   11.34  
   11.35  lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)"
   11.36 -by transfer (rule complex_Re_minus)
   11.37 +by transfer (rule uminus_complex.sel)
   11.38  
   11.39  lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)"
   11.40 -by transfer (rule complex_Im_minus)
   11.41 +by transfer (rule uminus_complex.sel)
   11.42  
   11.43  lemma hcomplex_add_minus_eq_minus:
   11.44        "x + y = (0::hcomplex) ==> x = -y"
   11.45 @@ -212,10 +212,10 @@
   11.46  subsection{*HComplex theorems*}
   11.47  
   11.48  lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x"
   11.49 -by transfer (rule Re)
   11.50 +by transfer simp
   11.51  
   11.52  lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y"
   11.53 -by transfer (rule Im)
   11.54 +by transfer simp
   11.55  
   11.56  lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z"
   11.57  by transfer (rule complex_surj)
   11.58 @@ -423,7 +423,7 @@
   11.59  by transfer (rule Complex_eq_1)
   11.60  
   11.61  lemma i_eq_HComplex_0_1: "iii = HComplex 0 1"
   11.62 -by transfer (rule i_def [THEN meta_eq_to_obj_eq])
   11.63 +by transfer (simp add: complex_eq_iff)
   11.64  
   11.65  lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)"
   11.66  by transfer (rule Complex_eq_i)
   11.67 @@ -447,10 +447,10 @@
   11.68  by transfer simp
   11.69  
   11.70  lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y"
   11.71 -by transfer simp
   11.72 +by transfer (simp add: norm_complex_def)
   11.73  
   11.74  lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y"
   11.75 -by transfer simp
   11.76 +by transfer (simp add: norm_complex_def)
   11.77  
   11.78  (*---------------------------------------------------------------------------*)
   11.79  (*  harg                                                                     *)
   11.80 @@ -458,7 +458,7 @@
   11.81  
   11.82  lemma cos_harg_i_mult_zero [simp]:
   11.83       "!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
   11.84 -by transfer (rule cos_arg_i_mult_zero)
   11.85 +by transfer simp
   11.86  
   11.87  lemma hcomplex_of_hypreal_zero_iff [simp]:
   11.88       "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)"
   11.89 @@ -469,17 +469,17 @@
   11.90  
   11.91  lemma complex_split_polar2:
   11.92       "\<forall>n. \<exists>r a. (z n) =  complex_of_real r * (Complex (cos a) (sin a))"
   11.93 -by (blast intro: complex_split_polar)
   11.94 +by (auto intro: complex_split_polar)
   11.95  
   11.96  lemma hcomplex_split_polar:
   11.97    "!!z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))"
   11.98 -by transfer (rule complex_split_polar)
   11.99 +by transfer (simp add: complex_split_polar)
  11.100  
  11.101  lemma hcis_eq:
  11.102     "!!a. hcis a =
  11.103      (hcomplex_of_hypreal(( *f* cos) a) +
  11.104      iii * hcomplex_of_hypreal(( *f* sin) a))"
  11.105 -by transfer (simp add: cis_def)
  11.106 +by transfer (simp add: complex_eq_iff)
  11.107  
  11.108  lemma hrcis_Ex: "!!z. \<exists>r a. z = hrcis r a"
  11.109  by transfer (rule rcis_Ex)
  11.110 @@ -502,12 +502,12 @@
  11.111  
  11.112  lemma hcmod_unit_one [simp]:
  11.113       "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1"
  11.114 -by transfer (rule cmod_unit_one)
  11.115 +by transfer (simp add: cmod_unit_one)
  11.116  
  11.117  lemma hcmod_complex_polar [simp]:
  11.118    "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
  11.119        abs r"
  11.120 -by transfer (rule cmod_complex_polar)
  11.121 +by transfer (simp add: cmod_complex_polar)
  11.122  
  11.123  lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r"
  11.124  by transfer (rule complex_mod_rcis)
  11.125 @@ -579,10 +579,10 @@
  11.126  by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric])
  11.127  
  11.128  lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a"
  11.129 -by transfer (rule Re_cis)
  11.130 +by transfer simp
  11.131  
  11.132  lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a"
  11.133 -by transfer (rule Im_cis)
  11.134 +by transfer simp
  11.135  
  11.136  lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)"
  11.137  by (simp add: NSDeMoivre)
    12.1 --- a/src/HOL/NthRoot.thy	Tue May 06 23:35:24 2014 +0200
    12.2 +++ b/src/HOL/NthRoot.thy	Wed May 07 12:25:35 2014 +0200
    12.3 @@ -374,12 +374,18 @@
    12.4  lemma real_sqrt_one [simp]: "sqrt 1 = 1"
    12.5  unfolding sqrt_def by (rule real_root_one [OF pos2])
    12.6  
    12.7 +lemma real_sqrt_four [simp]: "sqrt 4 = 2"
    12.8 +  using real_sqrt_abs[of 2] by simp
    12.9 +
   12.10  lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
   12.11  unfolding sqrt_def by (rule real_root_minus)
   12.12  
   12.13  lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
   12.14  unfolding sqrt_def by (rule real_root_mult)
   12.15  
   12.16 +lemma real_sqrt_mult_self[simp]: "sqrt a * sqrt a = \<bar>a\<bar>"
   12.17 +  using real_sqrt_abs[of a] unfolding power2_eq_square real_sqrt_mult .
   12.18 +
   12.19  lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
   12.20  unfolding sqrt_def by (rule real_root_inverse)
   12.21  
    13.1 --- a/src/HOL/Real.thy	Tue May 06 23:35:24 2014 +0200
    13.2 +++ b/src/HOL/Real.thy	Wed May 07 12:25:35 2014 +0200
    13.3 @@ -1555,6 +1555,7 @@
    13.4    "real a \<le> (- numeral x::real) ^ n \<longleftrightarrow> a \<le> (- numeral x::int) ^ n"
    13.5    unfolding real_of_int_le_iff[symmetric] by simp
    13.6  
    13.7 +
    13.8  subsection{*Density of the Reals*}
    13.9  
   13.10  lemma real_lbound_gt_zero:
   13.11 @@ -1613,6 +1614,14 @@
   13.12  apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto)
   13.13  done
   13.14  
   13.15 +lemma real_of_nat_less_numeral_iff [simp]:
   13.16 +  "real (n::nat) < numeral w \<longleftrightarrow> n < numeral w"
   13.17 +  using real_of_nat_less_iff[of n "numeral w"] by simp
   13.18 +
   13.19 +lemma numeral_less_real_of_nat_iff [simp]:
   13.20 +  "numeral w < real (n::nat) \<longleftrightarrow> numeral w < n"
   13.21 +  using real_of_nat_less_iff[of "numeral w" n] by simp
   13.22 +
   13.23  lemma numeral_le_real_of_int_iff [simp]:
   13.24       "((numeral n) \<le> real (m::int)) = (numeral n \<le> m)"
   13.25  by (simp add: linorder_not_less [symmetric])
    14.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue May 06 23:35:24 2014 +0200
    14.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed May 07 12:25:35 2014 +0200
    14.3 @@ -257,6 +257,12 @@
    14.4  lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y"
    14.5  by (simp add: of_real_def mult_commute)
    14.6  
    14.7 +lemma of_real_setsum[simp]: "of_real (setsum f s) = (\<Sum>x\<in>s. of_real (f x))"
    14.8 +  by (induct s rule: infinite_finite_induct) auto
    14.9 +
   14.10 +lemma of_real_setprod[simp]: "of_real (setprod f s) = (\<Prod>x\<in>s. of_real (f x))"
   14.11 +  by (induct s rule: infinite_finite_induct) auto
   14.12 +
   14.13  lemma nonzero_of_real_inverse:
   14.14    "x \<noteq> 0 \<Longrightarrow> of_real (inverse x) =
   14.15     inverse (of_real x :: 'a::real_div_algebra)"
   14.16 @@ -304,6 +310,12 @@
   14.17  lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z"
   14.18  by (cases z rule: int_diff_cases, simp)
   14.19  
   14.20 +lemma of_real_real_of_nat_eq [simp]: "of_real (real n) = of_nat n"
   14.21 +  by (simp add: real_of_nat_def)
   14.22 +
   14.23 +lemma of_real_real_of_int_eq [simp]: "of_real (real z) = of_int z"
   14.24 +  by (simp add: real_of_int_def)
   14.25 +
   14.26  lemma of_real_numeral: "of_real (numeral w) = numeral w"
   14.27  using of_real_of_int_eq [of "numeral w"] by simp
   14.28  
   14.29 @@ -1121,6 +1133,18 @@
   14.30  lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
   14.31  unfolding real_sgn_eq by simp
   14.32  
   14.33 +lemma zero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> (x::real)"
   14.34 +  by (cases "0::real" x rule: linorder_cases) simp_all
   14.35 +  
   14.36 +lemma zero_less_sgn_iff [simp]: "0 < sgn x \<longleftrightarrow> 0 < (x::real)"
   14.37 +  by (cases "0::real" x rule: linorder_cases) simp_all
   14.38 +
   14.39 +lemma sgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> (x::real) \<le> 0"
   14.40 +  by (cases "0::real" x rule: linorder_cases) simp_all
   14.41 +  
   14.42 +lemma sgn_less_0_iff [simp]: "sgn x < 0 \<longleftrightarrow> (x::real) < 0"
   14.43 +  by (cases "0::real" x rule: linorder_cases) simp_all
   14.44 +
   14.45  lemma norm_conv_dist: "norm x = dist x 0"
   14.46    unfolding dist_norm by simp
   14.47