Complex roots of unity. Better definition of ln for complex numbers. Used [code del] to stop code generation for powr.

--- a/NEWS	Sat Apr 11 16:19:59 2015 +0100
+++ b/NEWS	Sat Apr 11 22:18:33 2015 +0100
@@ -261,6 +261,10 @@
 * Classes cancel_ab_semigroup_add / cancel_monoid_add specify explicit
 additive inverse operation. INCOMPATIBILITY.
 
+* Complex powers and square roots. The functions "ln" and "powr" are now
+  overloaded for types real and complex, and 0 powr y = 0 by definition.
+  INCOMPATIBILITY: type constraints may be necessary.
+
 * The functions "sin" and "cos" are now defined for any type of sort
 "{real_normed_algebra_1,banach}" type, so in particular on "real" and
 "complex" uniformly. Minor INCOMPATIBILITY: type constraints may be

--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 16:19:59 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 22:18:33 2015 +0100
@@ -899,15 +899,17 @@
 
 subsection{*Complex logarithms (the conventional principal value)*}
 
-definition Ln :: "complex \<Rightarrow> complex"
-  where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
+instantiation complex :: ln
+begin
 
+definition ln_complex :: "complex \<Rightarrow> complex"
+  where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
 
 lemma
   assumes "z \<noteq> 0"
-    shows exp_Ln [simp]: "exp(Ln z) = z"
-      and mpi_less_Im_Ln: "-pi < Im(Ln z)"
-      and Im_Ln_le_pi:    "Im(Ln z) \<le> pi"
+    shows exp_Ln [simp]:  "exp(ln z) = z"
+      and mpi_less_Im_Ln: "-pi < Im(ln z)"
+      and Im_Ln_le_pi:    "Im(ln z) \<le> pi"
 proof -
   obtain \<psi> where z: "z / (cmod z) = Complex (cos \<psi>) (sin \<psi>)"
     using complex_unimodular_polar [of "z / (norm z)"] assms
@@ -915,23 +917,57 @@
   obtain \<phi> where \<phi>: "- pi < \<phi>" "\<phi> \<le> pi" "sin \<phi> = sin \<psi>" "cos \<phi> = cos \<psi>"
     using sincos_principal_value [of "\<psi>"] assms
     by (auto simp: norm_divide divide_simps)
-  have "exp(Ln z) = z & -pi < Im(Ln z) & Im(Ln z) \<le> pi" unfolding Ln_def
+  have "exp(ln z) = z & -pi < Im(ln z) & Im(ln z) \<le> pi" unfolding ln_complex_def
     apply (rule theI [where a = "Complex (ln(norm z)) \<phi>"])
     using z assms \<phi>
     apply (auto simp: field_simps exp_complex_eqI Exp_eq_polar cis.code)
     done
-  then show "exp(Ln z) = z" "-pi < Im(Ln z)" "Im(Ln z) \<le> pi"
+  then show "exp(ln z) = z" "-pi < Im(ln z)" "Im(ln z) \<le> pi"
     by auto
 qed
 
 lemma Ln_exp [simp]:
   assumes "-pi < Im(z)" "Im(z) \<le> pi"
-    shows "Ln(exp z) = z"
+    shows "ln(exp z) = z"
   apply (rule exp_complex_eqI)
   using assms mpi_less_Im_Ln  [of "exp z"] Im_Ln_le_pi [of "exp z"]
   apply auto
   done
 
+subsection{*Relation to Real Logarithm*}
+
+lemma Ln_of_real:
+  assumes "0 < z"
+    shows "ln(of_real z::complex) = of_real(ln z)"
+proof -
+  have "ln(of_real (exp (ln z))::complex) = ln (exp (of_real (ln z)))"
+    by (simp add: exp_of_real)
+  also have "... = of_real(ln z)"
+    using assms
+    by (subst Ln_exp) auto
+  finally show ?thesis
+    using assms by simp
+qed
+
+corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> ln z \<in> \<real>"
+  by (auto simp: Ln_of_real elim: Reals_cases)
+
+lemma Ln_1: "ln 1 = (0::complex)"
+proof -
+  have "ln (exp 0) = (0::complex)"
+    by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
+  then show ?thesis
+    by simp
+qed
+
+instance
+  by intro_classes (rule ln_complex_def Ln_1)
+
+end
+
+abbreviation Ln :: "complex \<Rightarrow> complex"
+  where "Ln \<equiv> ln"
+
 lemma Ln_eq_iff: "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (Ln w = Ln z \<longleftrightarrow> w = z)"
   by (metis exp_Ln)
 
@@ -1013,25 +1049,6 @@
   by (simp add: complex_differentiable_within_Ln holomorphic_on_def)
 
 
-subsection{*Relation to Real Logarithm*}
-
-lemma Ln_of_real:
-  assumes "0 < z"
-    shows "Ln(of_real z) = of_real(ln z)"
-proof -
-  have "Ln(of_real (exp (ln z))) = Ln (exp (of_real (ln z)))"
-    by (simp add: exp_of_real)
-  also have "... = of_real(ln z)"
-    using assms
-    by (subst Ln_exp) auto
-  finally show ?thesis
-    using assms by simp
-qed
-
-corollary Ln_in_Reals [simp]: "z \<in> \<real> \<Longrightarrow> Re z > 0 \<Longrightarrow> Ln z \<in> \<real>"
-  by (auto simp: Ln_of_real elim: Reals_cases)
-
-
 subsection{*Quadrant-type results for Ln*}
 
 lemma cos_lt_zero_pi: "pi/2 < x \<Longrightarrow> x < 3*pi/2 \<Longrightarrow> cos x < 0"
@@ -1150,26 +1167,6 @@
                inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
   done
 
-lemma Ln_1 [simp]: "Ln 1 = 0"
-proof -
-  have "Ln (exp 0) = 0"
-    by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
-  then show ?thesis
-    by simp
-qed
-
-instantiation complex :: ln
-begin
-
-definition ln_complex :: "complex \<Rightarrow> complex"
-  where "ln_complex \<equiv> Ln"
-
-instance 
-  by intro_classes (simp add: ln_complex_def)
-
-end
-
-
 lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
   apply (rule exp_complex_eqI)
   using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
@@ -1270,11 +1267,11 @@
   by (simp add: powr_def)
 
 lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
-  by (simp add: powr_def ln_complex_def)
+  by (simp add: powr_def)
 
 lemma powr_nat:
   fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
-  by (simp add: exp_of_nat_mult powr_def ln_complex_def)
+  by (simp add: exp_of_nat_mult powr_def)
 
 lemma powr_add:
   fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
@@ -1289,45 +1286,45 @@
   by (simp add: powr_def algebra_simps exp_diff)
 
 lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
-  apply (simp add: powr_def ln_complex_def)
+  apply (simp add: powr_def)
   using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
   by auto
 
 lemma powr_real_real:
     "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
-  apply (simp add: powr_def ln_complex_def)
+  apply (simp add: powr_def)
   by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
        exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
 
 lemma powr_of_real:
-  fixes x::real
-  shows "0 < x \<Longrightarrow> x powr y = x powr y"
-  by (simp add: powr_def powr_real_real)
+  fixes x::real and y::real
+  shows "0 < x \<Longrightarrow> of_real x powr (of_real y::complex) = of_real (x powr y)"
+  by (simp add: powr_def) (metis exp_of_real of_real_mult Ln_of_real)
 
 lemma norm_powr_real_mono:
-    "w \<in> \<real> \<Longrightarrow> 1 < Re w
-             \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
-  by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
+    "\<lbrakk>w \<in> \<real>; 1 < Re w\<rbrakk>
+     \<Longrightarrow> cmod(w powr z1) \<le> cmod(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
+  by (auto simp: powr_def algebra_simps Reals_def Ln_of_real)
 
 lemma powr_times_real:
     "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
            \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
-  by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
+  by (auto simp: Reals_def powr_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
 
 lemma has_field_derivative_powr:
     "(Im z = 0 \<Longrightarrow> 0 < Re z)
      \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
   apply (cases "z=0", auto)
-  apply (simp add: powr_def ln_complex_def)
+  apply (simp add: powr_def)
   apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
-  apply (auto simp: dist_complex_def ln_complex_def)
+  apply (auto simp: dist_complex_def)
   apply (intro derivative_eq_intros | simp add: assms)+
   apply (simp add: field_simps exp_diff)
   done
 
 lemma has_field_derivative_powr_right:
     "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
-  apply (simp add: powr_def ln_complex_def)
+  apply (simp add: powr_def)
   apply (intro derivative_eq_intros | simp add: assms)+
   done
 
@@ -1335,16 +1332,14 @@
     "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
 using complex_differentiable_def has_field_derivative_powr_right by blast
 
-
 lemma holomorphic_on_powr_right:
     "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
     unfolding holomorphic_on_def
     using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
 
-
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
-  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
+  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm)
 
 lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
   using Ln_of_real by force
@@ -2406,4 +2401,94 @@
 qed
 
 
+subsection{*Roots of unity*}
+
+lemma complex_root_unity:
+  fixes j::nat
+  assumes "n \<noteq> 0"
+    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n)^n = 1"
+proof -
+  have *: "of_nat j * (complex_of_real pi * 2) = complex_of_real (2 * real j * pi)"
+    by (simp add: of_real_numeral)
+  then show ?thesis
+    apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler)
+    apply (simp only: * cos_of_real sin_of_real)
+    apply (simp add: )
+    done
+qed
+
+lemma complex_root_unity_eq:
+  fixes j::nat and k::nat
+  assumes "1 \<le> n"
+    shows "(exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = exp(2 * of_real pi * \<i> * of_nat k / of_nat n)
+           \<longleftrightarrow> j mod n = k mod n)"
+proof -
+    have "(\<exists>z::int. \<i> * (of_nat j * (of_real pi * 2)) =
+               \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow>
+          (\<exists>z::int. of_nat j * (\<i> * (of_real pi * 2)) =
+              (of_nat k + of_nat n * of_int z) * (\<i> * (of_real pi * 2)))"
+      by (simp add: algebra_simps)
+    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))"
+      by simp
+    also have "... \<longleftrightarrow> (\<exists>z::int. of_nat j = of_nat k + of_nat n * z)"
+      apply (rule HOL.iff_exI)
+      apply (auto simp: )
+      using of_int_eq_iff apply fastforce
+      by (metis of_int_add of_int_mult of_int_of_nat_eq)
+    also have "... \<longleftrightarrow> int j mod int n = int k mod int n"
+      by (auto simp: zmod_eq_dvd_iff dvd_def algebra_simps)
+    also have "... \<longleftrightarrow> j mod n = k mod n"
+      by (metis of_nat_eq_iff zmod_int)
+    finally have "(\<exists>z. \<i> * (of_nat j * (of_real pi * 2)) =
+             \<i> * (of_nat k * (of_real pi * 2)) + \<i> * (of_int z * (of_nat n * (of_real pi * 2)))) \<longleftrightarrow> j mod n = k mod n" .
+   note * = this
+  show ?thesis
+    using assms
+    by (simp add: exp_eq divide_simps mult_ac of_real_numeral *)
+qed
+
+corollary bij_betw_roots_unity:
+    "bij_betw (\<lambda>j. exp(2 * of_real pi * \<i> * of_nat j / of_nat n))
+              {..<n}  {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j. j < n}"
+  by (auto simp: bij_betw_def inj_on_def complex_root_unity_eq)
+
+lemma complex_root_unity_eq_1:
+  fixes j::nat and k::nat
+  assumes "1 \<le> n"
+    shows "exp(2 * of_real pi * \<i> * of_nat j / of_nat n) = 1 \<longleftrightarrow> n dvd j"
+proof -
+  have "1 = exp(2 * of_real pi * \<i> * (of_nat n / of_nat n))"
+    using assms by simp
+  then have "exp(2 * of_real pi * \<i> * (of_nat j / of_nat n)) = 1 \<longleftrightarrow> j mod n = n mod n"
+     using complex_root_unity_eq [of n j n] assms
+     by simp
+  then show ?thesis
+    by auto
+qed
+
+lemma finite_complex_roots_unity_explicit:
+     "finite {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
+by simp
+
+lemma card_complex_roots_unity_explicit:
+     "card {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n} = n"
+  by (simp add:  Finite_Set.bij_betw_same_card [OF bij_betw_roots_unity, symmetric])
+
+lemma complex_roots_unity:
+  assumes "1 \<le> n"
+    shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \<i> * of_nat j / of_nat n) | j::nat. j < n}"
+  apply (rule Finite_Set.card_seteq [symmetric])
+  using assms
+  apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity)
+  done
+
+lemma card_complex_roots_unity: "1 \<le> n \<Longrightarrow> card {z::complex. z^n = 1} = n"
+  by (simp add: card_complex_roots_unity_explicit complex_roots_unity)
+
+lemma complex_not_root_unity:
+    "1 \<le> n \<Longrightarrow> \<exists>u::complex. norm u = 1 \<and> u^n \<noteq> 1"
+  apply (rule_tac x="exp (of_real pi * \<i> * of_real (1 / n))" in exI)
+  apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler)
+  done
+
 end

--- a/src/HOL/Transcendental.thy	Sat Apr 11 16:19:59 2015 +0100
+++ b/src/HOL/Transcendental.thy	Sat Apr 11 22:18:33 2015 +0100
@@ -1291,7 +1291,7 @@
 
 definition powr :: "['a,'a] => 'a::ln"     (infixr "powr" 80)
   -- {*exponentation via ln and exp*}
-  where "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
+  where  [code del]: "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
 
 
 instantiation real :: ln