author paulson Thu, 16 Mar 2017 16:02:18 +0000 changeset 65274 db2de50de28e parent 65273 917ae0ba03a2 child 65299 6b840c704441
Removed [simp] status for Complex_eq. Also tidied some proofs
 src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Generalised_Binomial_Theorem.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Great_Picard.thy file | annotate | diff | comparison | revisions src/HOL/Complex.thy file | annotate | diff | comparison | revisions src/HOL/Nonstandard_Analysis/NSComplex.thy file | annotate | diff | comparison | revisions
```--- 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)))"

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)"

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_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)
@@ -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: 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)
@@ -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"

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
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 @@

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)```