Removed [simp] status for Complex_eq. Also tidied some proofs
authorpaulson <lp15@cam.ac.uk>
Thu Mar 16 16:02:18 2017 +0000 (2017-03-16)
changeset 65274db2de50de28e
parent 65273 917ae0ba03a2
child 65299 6b840c704441
Removed [simp] status for Complex_eq. Also tidied some proofs
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Generalised_Binomial_Theorem.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Complex.thy
src/HOL/Nonstandard_Analysis/NSComplex.thy
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Mar 16 13:55:29 2017 +0000
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Mar 16 16:02:18 2017 +0000
     1.3 @@ -176,7 +176,7 @@
     1.4  
     1.5  lemma Euler: "exp(z) = of_real(exp(Re z)) *
     1.6                (of_real(cos(Im z)) + \<i> * of_real(sin(Im z)))"
     1.7 -by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real)
     1.8 +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq)
     1.9  
    1.10  lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2"
    1.11    by (simp add: sin_exp_eq field_simps Re_divide Im_exp)
    1.12 @@ -202,13 +202,20 @@
    1.13  subsection\<open>More on the Polar Representation of Complex Numbers\<close>
    1.14  
    1.15  lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)"
    1.16 -  by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    1.17 +  by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real)
    1.18  
    1.19  lemma exp_eq_1: "exp z = 1 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>n::int. Im(z) = of_int (2 * n) * pi)"
    1.20 -apply auto
    1.21 -apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
    1.22 -apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1))
    1.23 -by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 sin_zero_iff_int2)
    1.24 +                 (is "?lhs = ?rhs")
    1.25 +proof 
    1.26 +  assume "exp z = 1"
    1.27 +  then have "Re z = 0"
    1.28 +    by (metis exp_eq_one_iff norm_exp_eq_Re norm_one)
    1.29 +  with \<open>?lhs\<close> show ?rhs
    1.30 +    by (metis Re_exp complex_Re_of_int cos_one_2pi_int exp_zero mult.commute mult_numeral_1 numeral_One of_int_mult of_int_numeral)
    1.31 +next
    1.32 +  assume ?rhs then show ?lhs
    1.33 +    using Im_exp Re_exp complex_Re_Im_cancel_iff by force
    1.34 +qed
    1.35  
    1.36  lemma exp_eq: "exp w = exp z \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
    1.37                  (is "?lhs = ?rhs")
    1.38 @@ -487,7 +494,7 @@
    1.39  lemma sinh_complex:
    1.40    fixes z :: complex
    1.41    shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
    1.42 -  by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
    1.43 +  by (simp add: sin_exp_eq divide_simps exp_minus)
    1.44  
    1.45  lemma sin_i_times:
    1.46    fixes z :: complex
    1.47 @@ -497,24 +504,24 @@
    1.48  lemma sinh_real:
    1.49    fixes x :: real
    1.50    shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
    1.51 -  by (simp add: exp_of_real sin_i_times of_real_numeral)
    1.52 +  by (simp add: exp_of_real sin_i_times)
    1.53  
    1.54  lemma cosh_complex:
    1.55    fixes z :: complex
    1.56    shows "(exp z + inverse (exp z)) / 2 = cos(\<i> * z)"
    1.57 -  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
    1.58 +  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)
    1.59  
    1.60  lemma cosh_real:
    1.61    fixes x :: real
    1.62    shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
    1.63 -  by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
    1.64 +  by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real)
    1.65  
    1.66  lemmas cos_i_times = cosh_complex [symmetric]
    1.67  
    1.68  lemma norm_cos_squared:
    1.69      "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
    1.70    apply (cases z)
    1.71 -  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real)
    1.72 +  apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq)
    1.73    apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
    1.74    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
    1.75    apply (simp add: sin_squared_eq)
    1.76 @@ -524,7 +531,7 @@
    1.77  lemma norm_sin_squared:
    1.78      "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4"
    1.79    apply (cases z)
    1.80 -  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double)
    1.81 +  apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq)
    1.82    apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide)
    1.83    apply (simp only: left_diff_distrib [symmetric] power_mult_distrib)
    1.84    apply (simp add: cos_squared_eq)
    1.85 @@ -969,7 +976,7 @@
    1.86  
    1.87  lemma complex_split_polar:
    1.88    obtains r a::real where "z = complex_of_real r * (cos a + \<i> * sin a)" "0 \<le> r" "0 \<le> a" "a < 2*pi"
    1.89 -  using Arg cis.ctr cis_conv_exp by fastforce
    1.90 +  using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce
    1.91  
    1.92  lemma Re_Im_le_cmod: "Im w * sin \<phi> + Re w * cos \<phi> \<le> cmod w"
    1.93  proof (cases w rule: complex_split_polar)
    1.94 @@ -2112,7 +2119,7 @@
    1.95  proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
    1.96    case True
    1.97    then have "Im z = 0" "Re z < 0 \<or> z = 0"
    1.98 -    using cnj.code complex_cnj_zero_iff  by (auto simp: complex_nonpos_Reals_iff) fastforce
    1.99 +    using cnj.code complex_cnj_zero_iff  by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce
   1.100    then show ?thesis
   1.101      apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge])
   1.102      apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric])
     2.1 --- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Thu Mar 16 13:55:29 2017 +0000
     2.2 +++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Thu Mar 16 16:02:18 2017 +0000
     2.3 @@ -123,7 +123,7 @@
     2.4      hence z: "norm z < K" by simp
     2.5      with K have nz: "1 + z \<noteq> 0" by (auto dest!: minus_unique)
     2.6      from z K have "norm z < 1" by simp
     2.7 -    hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff)
     2.8 +    hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: Complex_eq complex_nonpos_Reals_iff)
     2.9      hence "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative
    2.10                f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z
    2.11        by (auto intro!: derivative_eq_intros)
     3.1 --- a/src/HOL/Analysis/Great_Picard.thy	Thu Mar 16 13:55:29 2017 +0000
     3.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Thu Mar 16 16:02:18 2017 +0000
     3.3 @@ -211,7 +211,7 @@
     3.4    have "\<exists>x. cos (complex_of_real pi * z) = of_int x"
     3.5      using assms
     3.6      apply safe
     3.7 -      apply (auto simp: Ints_def cos_exp_eq exp_minus)
     3.8 +      apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq)
     3.9       apply (auto simp: algebra_simps dest: 1 2)
    3.10        done
    3.11    then have "sin(pi * cos(pi * z)) ^ 2 = 0"
     4.1 --- a/src/HOL/Complex.thy	Thu Mar 16 13:55:29 2017 +0000
     4.2 +++ b/src/HOL/Complex.thy	Thu Mar 16 16:02:18 2017 +0000
     4.3 @@ -207,7 +207,7 @@
     4.4      "Re \<i> = 0"
     4.5    | "Im \<i> = 1"
     4.6  
     4.7 -lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
     4.8 +lemma Complex_eq: "Complex a b = a + \<i> * b"
     4.9    by (simp add: complex_eq_iff)
    4.10  
    4.11  lemma complex_eq: "a = Re a + \<i> * Im a"
    4.12 @@ -423,7 +423,7 @@
    4.13  
    4.14  lemma tendsto_Complex [tendsto_intros]:
    4.15    "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
    4.16 -  by (auto intro!: tendsto_intros)
    4.17 +  unfolding Complex_eq by (auto intro!: tendsto_intros)
    4.18  
    4.19  lemma tendsto_complex_iff:
    4.20    "(f \<longlongrightarrow> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) \<longlongrightarrow> Re x) F \<and> ((\<lambda>x. Im (f x)) \<longlongrightarrow> Im x) F)"
    4.21 @@ -819,13 +819,13 @@
    4.22    qed
    4.23    then show ?thesis
    4.24      using sin_converges [of b] cos_converges [of b]
    4.25 -    by (auto simp add: cis.ctr exp_def simp del: of_real_mult
    4.26 +    by (auto simp add: Complex_eq cis.ctr exp_def simp del: of_real_mult
    4.27          intro!: sums_unique sums_add sums_mult sums_of_real)
    4.28  qed
    4.29  
    4.30  lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)"
    4.31    unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp
    4.32 -  by (cases z) simp
    4.33 +  by (cases z) (simp add: Complex_eq)
    4.34  
    4.35  lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
    4.36    unfolding exp_eq_polar by simp
    4.37 @@ -837,7 +837,7 @@
    4.38    by (simp add: norm_complex_def)
    4.39  
    4.40  lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
    4.41 -  by (simp add: cis.code cmod_complex_polar exp_eq_polar)
    4.42 +  by (simp add: cis.code cmod_complex_polar exp_eq_polar Complex_eq)
    4.43  
    4.44  lemma complex_exp_exists: "\<exists>a r. z = complex_of_real r * exp a"
    4.45    apply (insert rcis_Ex [of z])
    4.46 @@ -1057,7 +1057,7 @@
    4.47      and Complex_sum: "Complex (sum f s) 0 = sum (\<lambda>x. Complex (f x) 0) s"
    4.48      and complex_of_real_def: "complex_of_real r = Complex r 0"
    4.49      and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)"
    4.50 -  by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq)
    4.51 +  by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide)
    4.52  
    4.53  lemma Complex_in_Reals: "Complex x 0 \<in> \<real>"
    4.54    by (metis Reals_of_real complex_of_real_def)
     5.1 --- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Thu Mar 16 13:55:29 2017 +0000
     5.2 +++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Thu Mar 16 16:02:18 2017 +0000
     5.3 @@ -438,20 +438,17 @@
     5.4  subsubsection \<open>\<open>harg\<close>\<close>
     5.5  
     5.6  lemma cos_harg_i_mult_zero [simp]: "\<And>y. y \<noteq> 0 \<Longrightarrow> ( *f* cos) (harg (HComplex 0 y)) = 0"
     5.7 -  by transfer simp
     5.8 -
     5.9 -lemma hcomplex_of_hypreal_zero_iff [simp]: "\<And>y. hcomplex_of_hypreal y = 0 \<longleftrightarrow> y = 0"
    5.10 -  by transfer (rule of_real_eq_0_iff)
    5.11 +  by transfer (simp add: Complex_eq)
    5.12  
    5.13  
    5.14  subsection \<open>Polar Form for Nonstandard Complex Numbers\<close>
    5.15  
    5.16  lemma complex_split_polar2: "\<forall>n. \<exists>r a. (z n) = complex_of_real r * Complex (cos a) (sin a)"
    5.17 -  by (auto intro: complex_split_polar)
    5.18 +  unfolding Complex_eq by (auto intro: complex_split_polar)
    5.19  
    5.20  lemma hcomplex_split_polar:
    5.21    "\<And>z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex (( *f* cos) a) (( *f* sin) a))"
    5.22 -  by transfer (simp add: complex_split_polar)
    5.23 +  by transfer (simp add: Complex_eq complex_split_polar)
    5.24  
    5.25  lemma hcis_eq:
    5.26    "\<And>a. hcis a = hcomplex_of_hypreal (( *f* cos) a) + iii * hcomplex_of_hypreal (( *f* sin) a)"
    5.27 @@ -479,7 +476,7 @@
    5.28  
    5.29  lemma hcmod_complex_polar [simp]:
    5.30    "\<And>r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \<bar>r\<bar>"
    5.31 -  by transfer (simp add: cmod_complex_polar)
    5.32 +  by transfer (simp add: Complex_eq cmod_complex_polar)
    5.33  
    5.34  lemma hcmod_hrcis [simp]: "\<And>r a. hcmod(hrcis r a) = \<bar>r\<bar>"
    5.35    by transfer (rule complex_mod_rcis)