# HG changeset patch # User paulson # Date 1489680138 0 # Node ID db2de50de28ec35c933d9d1949f7901c908fe5ce # Parent 917ae0ba03a26d54bde67b8319f09e25522a0f89 Removed [simp] status for Complex_eq. Also tidied some proofs diff -r 917ae0ba03a2 -r db2de50de28e src/HOL/Analysis/Complex_Transcendental.thy --- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Mar 16 13:55:29 2017 +0000 +++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Mar 16 16:02:18 2017 +0000 @@ -176,7 +176,7 @@ lemma Euler: "exp(z) = of_real(exp(Re z)) * (of_real(cos(Im z)) + \ * of_real(sin(Im z)))" -by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real) +by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real Complex_eq) lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2" by (simp add: sin_exp_eq field_simps Re_divide Im_exp) @@ -202,13 +202,20 @@ subsection\More on the Polar Representation of Complex Numbers\ lemma exp_Complex: "exp(Complex r t) = of_real(exp r) * Complex (cos t) (sin t)" - by (simp add: exp_add exp_Euler exp_of_real sin_of_real cos_of_real) + by (simp add: Complex_eq exp_add exp_Euler exp_of_real sin_of_real cos_of_real) lemma exp_eq_1: "exp z = 1 \ Re(z) = 0 \ (\n::int. Im(z) = of_int (2 * n) * pi)" -apply auto -apply (metis exp_eq_one_iff norm_exp_eq_Re norm_one) -apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1)) -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) + (is "?lhs = ?rhs") +proof + assume "exp z = 1" + then have "Re z = 0" + by (metis exp_eq_one_iff norm_exp_eq_Re norm_one) + with \?lhs\ show ?rhs + 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) +next + assume ?rhs then show ?lhs + using Im_exp Re_exp complex_Re_Im_cancel_iff by force +qed lemma exp_eq: "exp w = exp z \ (\n::int. w = z + (of_int (2 * n) * pi) * \)" (is "?lhs = ?rhs") @@ -487,7 +494,7 @@ lemma sinh_complex: fixes z :: complex shows "(exp z - inverse (exp z)) / 2 = -\ * sin(\ * z)" - by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral) + by (simp add: sin_exp_eq divide_simps exp_minus) lemma sin_i_times: fixes z :: complex @@ -497,24 +504,24 @@ lemma sinh_real: fixes x :: real shows "of_real((exp x - inverse (exp x)) / 2) = -\ * sin(\ * of_real x)" - by (simp add: exp_of_real sin_i_times of_real_numeral) + by (simp add: exp_of_real sin_i_times) lemma cosh_complex: fixes z :: complex shows "(exp z + inverse (exp z)) / 2 = cos(\ * z)" - by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real) + by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real) lemma cosh_real: fixes x :: real shows "of_real((exp x + inverse (exp x)) / 2) = cos(\ * of_real x)" - by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real) + by (simp add: cos_exp_eq divide_simps exp_minus exp_of_real) lemmas cos_i_times = cosh_complex [symmetric] lemma norm_cos_squared: "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4" apply (cases z) - apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real) + apply (simp add: cos_add cmod_power2 cos_of_real sin_of_real Complex_eq) apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide) apply (simp only: left_diff_distrib [symmetric] power_mult_distrib) apply (simp add: sin_squared_eq) @@ -524,7 +531,7 @@ lemma norm_sin_squared: "norm(sin z) ^ 2 = (exp(2 * Im z) + inverse(exp(2 * Im z)) - 2 * cos(2 * Re z)) / 4" apply (cases z) - apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double) + apply (simp add: sin_add cmod_power2 cos_of_real sin_of_real cos_double_cos exp_double Complex_eq) apply (simp add: cos_exp_eq sin_exp_eq exp_minus exp_of_real Re_divide Im_divide power_divide) apply (simp only: left_diff_distrib [symmetric] power_mult_distrib) apply (simp add: cos_squared_eq) @@ -969,7 +976,7 @@ lemma complex_split_polar: obtains r a::real where "z = complex_of_real r * (cos a + \ * sin a)" "0 \ r" "0 \ a" "a < 2*pi" - using Arg cis.ctr cis_conv_exp by fastforce + using Arg cis.ctr cis_conv_exp unfolding Complex_eq by fastforce lemma Re_Im_le_cmod: "Im w * sin \ + Re w * cos \ \ cmod w" proof (cases w rule: complex_split_polar) @@ -2112,7 +2119,7 @@ proof (cases "z \ \\<^sub>\\<^sub>0") case True then have "Im z = 0" "Re z < 0 \ z = 0" - using cnj.code complex_cnj_zero_iff by (auto simp: complex_nonpos_Reals_iff) fastforce + using cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce then show ?thesis apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge]) apply (auto simp: continuous_within_eps_delta norm_conv_dist [symmetric]) diff -r 917ae0ba03a2 -r db2de50de28e src/HOL/Analysis/Generalised_Binomial_Theorem.thy --- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Thu Mar 16 13:55:29 2017 +0000 +++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy Thu Mar 16 16:02:18 2017 +0000 @@ -123,7 +123,7 @@ hence z: "norm z < K" by simp with K have nz: "1 + z \ 0" by (auto dest!: minus_unique) from z K have "norm z < 1" by simp - hence "(1 + z) \ \\<^sub>\\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff) + hence "(1 + z) \ \\<^sub>\\<^sub>0" by (cases z) (auto simp: Complex_eq complex_nonpos_Reals_iff) hence "((\z. f z * (1 + z) powr (-a)) has_field_derivative f' z * (1 + z) powr (-a) - a * f z * (1 + z) powr (-a-1)) (at z)" using z by (auto intro!: derivative_eq_intros) diff -r 917ae0ba03a2 -r db2de50de28e src/HOL/Analysis/Great_Picard.thy --- a/src/HOL/Analysis/Great_Picard.thy Thu Mar 16 13:55:29 2017 +0000 +++ b/src/HOL/Analysis/Great_Picard.thy Thu Mar 16 16:02:18 2017 +0000 @@ -211,7 +211,7 @@ have "\x. cos (complex_of_real pi * z) = of_int x" using assms apply safe - apply (auto simp: Ints_def cos_exp_eq exp_minus) + apply (auto simp: Ints_def cos_exp_eq exp_minus Complex_eq) apply (auto simp: algebra_simps dest: 1 2) done then have "sin(pi * cos(pi * z)) ^ 2 = 0" diff -r 917ae0ba03a2 -r db2de50de28e src/HOL/Complex.thy --- a/src/HOL/Complex.thy Thu Mar 16 13:55:29 2017 +0000 +++ b/src/HOL/Complex.thy Thu Mar 16 16:02:18 2017 +0000 @@ -207,7 +207,7 @@ "Re \ = 0" | "Im \ = 1" -lemma Complex_eq[simp]: "Complex a b = a + \ * b" +lemma Complex_eq: "Complex a b = a + \ * b" by (simp add: complex_eq_iff) lemma complex_eq: "a = Re a + \ * Im a" @@ -423,7 +423,7 @@ lemma tendsto_Complex [tendsto_intros]: "(f \ a) F \ (g \ b) F \ ((\x. Complex (f x) (g x)) \ Complex a b) F" - by (auto intro!: tendsto_intros) + unfolding Complex_eq by (auto intro!: tendsto_intros) lemma tendsto_complex_iff: "(f \ x) F \ (((\x. Re (f x)) \ Re x) F \ ((\x. Im (f x)) \ Im x) F)" @@ -819,13 +819,13 @@ qed then show ?thesis using sin_converges [of b] cos_converges [of b] - by (auto simp add: cis.ctr exp_def simp del: of_real_mult + by (auto simp add: Complex_eq cis.ctr exp_def simp del: of_real_mult intro!: sums_unique sums_add sums_mult sums_of_real) qed lemma exp_eq_polar: "exp z = exp (Re z) * cis (Im z)" unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp - by (cases z) simp + by (cases z) (simp add: Complex_eq) lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)" unfolding exp_eq_polar by simp @@ -837,7 +837,7 @@ by (simp add: norm_complex_def) lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)" - by (simp add: cis.code cmod_complex_polar exp_eq_polar) + by (simp add: cis.code cmod_complex_polar exp_eq_polar Complex_eq) lemma complex_exp_exists: "\a r. z = complex_of_real r * exp a" apply (insert rcis_Ex [of z]) @@ -1057,7 +1057,7 @@ and Complex_sum: "Complex (sum f s) 0 = sum (\x. Complex (f x) 0) s" and complex_of_real_def: "complex_of_real r = Complex r 0" and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)" - by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq) + by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide) lemma Complex_in_Reals: "Complex x 0 \ \" by (metis Reals_of_real complex_of_real_def) diff -r 917ae0ba03a2 -r db2de50de28e src/HOL/Nonstandard_Analysis/NSComplex.thy --- a/src/HOL/Nonstandard_Analysis/NSComplex.thy Thu Mar 16 13:55:29 2017 +0000 +++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy Thu Mar 16 16:02:18 2017 +0000 @@ -438,20 +438,17 @@ subsubsection \\harg\\ lemma cos_harg_i_mult_zero [simp]: "\y. y \ 0 \ ( *f* cos) (harg (HComplex 0 y)) = 0" - by transfer simp - -lemma hcomplex_of_hypreal_zero_iff [simp]: "\y. hcomplex_of_hypreal y = 0 \ y = 0" - by transfer (rule of_real_eq_0_iff) + by transfer (simp add: Complex_eq) subsection \Polar Form for Nonstandard Complex Numbers\ lemma complex_split_polar2: "\n. \r a. (z n) = complex_of_real r * Complex (cos a) (sin a)" - by (auto intro: complex_split_polar) + unfolding Complex_eq by (auto intro: complex_split_polar) lemma hcomplex_split_polar: "\z. \r a. z = hcomplex_of_hypreal r * (HComplex (( *f* cos) a) (( *f* sin) a))" - by transfer (simp add: complex_split_polar) + by transfer (simp add: Complex_eq complex_split_polar) lemma hcis_eq: "\a. hcis a = hcomplex_of_hypreal (( *f* cos) a) + iii * hcomplex_of_hypreal (( *f* sin) a)" @@ -479,7 +476,7 @@ lemma hcmod_complex_polar [simp]: "\r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \r\" - by transfer (simp add: cmod_complex_polar) + by transfer (simp add: Complex_eq cmod_complex_polar) lemma hcmod_hrcis [simp]: "\r a. hcmod(hrcis r a) = \r\" by transfer (rule complex_mod_rcis)