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