src/HOL/Complex.thy
 changeset 59746 ddae5727c5a9 parent 59741 5b762cd73a8e child 59862 44b3f4fa33ca
     1.1 --- a/src/HOL/Complex.thy	Wed Mar 18 14:55:17 2015 +0000
1.2 +++ b/src/HOL/Complex.thy	Wed Mar 18 17:23:22 2015 +0000
1.3 @@ -612,7 +612,11 @@
1.4      done
1.5  qed
1.6
1.7 -subsection{*Finally! Polar Form for Complex Numbers*}
1.8 +subsection{*Polar Form for Complex Numbers*}
1.9 +
1.10 +lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)"
1.11 +  using sincos_total_2pi [of "Re z" "Im z"]
1.12 +  by auto (metis cmod_power2 complex_eq power_one)
1.13
1.14  subsubsection {* $\cos \theta + i \sin \theta$ *}
1.15
1.16 @@ -724,11 +728,17 @@
1.17  lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
1.18    unfolding Exp_eq_polar by simp
1.19
1.20 +lemma norm_cos_sin [simp]: "norm (Complex (cos t) (sin t)) = 1"
1.21 +  by (simp add: norm_complex_def)
1.22 +
1.23 +lemma norm_exp_eq_Re [simp]: "norm (exp z) = exp (Re z)"
1.24 +  by (simp add: cis.code cmod_complex_polar Exp_eq_polar)
1.25 +
1.26  lemma complex_Exp_Ex: "\<exists>a r. z = complex_of_real r * Exp a"
1.27 -apply (insert rcis_Ex [of z])
1.28 -apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
1.29 -apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
1.30 -done
1.31 +  apply (insert rcis_Ex [of z])
1.32 +  apply (auto simp add: Exp_eq_polar rcis_def mult.assoc [symmetric])
1.33 +  apply (rule_tac x = "ii * complex_of_real a" in exI, auto)
1.34 +  done
1.35
1.36  lemma Exp_two_pi_i [simp]: "Exp((2::complex) * complex_of_real pi * ii) = 1"
1.37    by (simp add: Exp_eq_polar complex_eq_iff)
1.38 @@ -865,6 +875,10 @@
1.39      by auto
1.40  qed
1.41
1.42 +lemma csqrt_unique:
1.43 +    "w^2 = z \<Longrightarrow> (0 < Re w \<or> Re w = 0 \<and> 0 \<le> Im w) \<Longrightarrow> csqrt z = w"
1.44 +  by (auto simp: csqrt_square)
1.45 +
1.46  lemma csqrt_minus [simp]:
1.47    assumes "Im x < 0 \<or> (Im x = 0 \<and> 0 \<le> Re x)"
1.48    shows "csqrt (- x) = \<i> * csqrt x"
1.49 @@ -877,7 +891,7 @@
1.50        by (auto simp add: Re_csqrt simp del: csqrt.simps)
1.51    qed
1.52    also have "(\<i> * csqrt x)^2 = - x"
1.53 -    by (simp add: power2_csqrt power_mult_distrib)
1.54 +    by (simp add: power_mult_distrib)
1.55    finally show ?thesis .
1.56  qed
1.57