Removed [simp] status for Complex_eq. Also tidied some proofs
--- 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)) + \<i> * 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\<open>More on the Polar Representation of Complex Numbers\<close>
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 \<longleftrightarrow> Re(z) = 0 \<and> (\<exists>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 \<open>?lhs\<close> 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 \<longleftrightarrow> (\<exists>n::int. w = z + (of_int (2 * n) * pi) * \<i>)"
(is "?lhs = ?rhs")
@@ -487,7 +494,7 @@
lemma sinh_complex:
fixes z :: complex
shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * 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) = -\<i> * sin(\<i> * 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(\<i> * 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(\<i> * 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 + \<i> * sin a)" "0 \<le> r" "0 \<le> 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 \<phi> + Re w * cos \<phi> \<le> cmod w"
proof (cases w rule: complex_split_polar)
@@ -2112,7 +2119,7 @@
proof (cases "z \<in> \<real>\<^sub>\<le>\<^sub>0")
case True
then have "Im z = 0" "Re z < 0 \<or> 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])
--- 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 \<noteq> 0" by (auto dest!: minus_unique)
from z K have "norm z < 1" by simp
- hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: complex_nonpos_Reals_iff)
+ hence "(1 + z) \<notin> \<real>\<^sub>\<le>\<^sub>0" by (cases z) (auto simp: Complex_eq complex_nonpos_Reals_iff)
hence "((\<lambda>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)
--- 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 "\<exists>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"
--- 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 \<i> = 0"
| "Im \<i> = 1"
-lemma Complex_eq[simp]: "Complex a b = a + \<i> * b"
+lemma Complex_eq: "Complex a b = a + \<i> * b"
by (simp add: complex_eq_iff)
lemma complex_eq: "a = Re a + \<i> * Im a"
@@ -423,7 +423,7 @@
lemma tendsto_Complex [tendsto_intros]:
"(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
- by (auto intro!: tendsto_intros)
+ unfolding Complex_eq by (auto intro!: tendsto_intros)
lemma tendsto_complex_iff:
"(f \<longlongrightarrow> x) F \<longleftrightarrow> (((\<lambda>x. Re (f x)) \<longlongrightarrow> Re x) F \<and> ((\<lambda>x. Im (f x)) \<longlongrightarrow> 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: "\<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 (\<lambda>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 \<in> \<real>"
by (metis Reals_of_real complex_of_real_def)
--- 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 \<open>\<open>harg\<close>\<close>
lemma cos_harg_i_mult_zero [simp]: "\<And>y. y \<noteq> 0 \<Longrightarrow> ( *f* cos) (harg (HComplex 0 y)) = 0"
- by transfer simp
-
-lemma hcomplex_of_hypreal_zero_iff [simp]: "\<And>y. hcomplex_of_hypreal y = 0 \<longleftrightarrow> y = 0"
- by transfer (rule of_real_eq_0_iff)
+ by transfer (simp add: Complex_eq)
subsection \<open>Polar Form for Nonstandard Complex Numbers\<close>
lemma complex_split_polar2: "\<forall>n. \<exists>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:
"\<And>z. \<exists>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:
"\<And>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]:
"\<And>r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \<bar>r\<bar>"
- by transfer (simp add: cmod_complex_polar)
+ by transfer (simp add: Complex_eq cmod_complex_polar)
lemma hcmod_hrcis [simp]: "\<And>r a. hcmod(hrcis r a) = \<bar>r\<bar>"
by transfer (rule complex_mod_rcis)