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