src/HOL/Analysis/Complex_Transcendental.thy
changeset 65585 a043de9ad41e
parent 65583 8d53b3bebab4
child 65587 16a8991ab398
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:57:16 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 16:58:31 2017 +0100
     1.3 @@ -1017,6 +1017,7 @@
     1.4  definition ln_complex :: "complex \<Rightarrow> complex"
     1.5    where "ln_complex \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
     1.6  
     1.7 +text\<open>NOTE: within this scope, the constant Ln is not yet available!\<close>
     1.8  lemma
     1.9    assumes "z \<noteq> 0"
    1.10      shows exp_Ln [simp]:  "exp(ln z) = z"
    1.11 @@ -1046,9 +1047,6 @@
    1.12    apply auto
    1.13    done
    1.14  
    1.15 -lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
    1.16 -  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
    1.17 -
    1.18  subsection\<open>Relation to Real Logarithm\<close>
    1.19  
    1.20  lemma Ln_of_real:
    1.21 @@ -1073,14 +1071,18 @@
    1.22  lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    1.23    using Ln_of_real by force
    1.24  
    1.25 -lemma Ln_1: "ln 1 = (0::complex)"
    1.26 +lemma Ln_1 [simp]: "ln 1 = (0::complex)"
    1.27  proof -
    1.28    have "ln (exp 0) = (0::complex)"
    1.29      by (metis (mono_tags, hide_lams) Ln_of_real exp_zero ln_one of_real_0 of_real_1 zero_less_one)
    1.30    then show ?thesis
    1.31 -    by simp
    1.32 +    by simp                              
    1.33  qed
    1.34  
    1.35 +  
    1.36 +lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1" for x::complex
    1.37 +  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
    1.38 +
    1.39  instance
    1.40    by intro_classes (rule ln_complex_def Ln_1)
    1.41