src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 61070 b72a990adfe2
parent 60809 457abb82fb9e
child 61426 d53db136e8fd
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -211,7 +211,7 @@
     1.4    by (auto simp: exp_eq abs_mult)
     1.5  
     1.6  lemma exp_integer_2pi:
     1.7 -  assumes "n \<in> Ints"
     1.8 +  assumes "n \<in> \<int>"
     1.9    shows "exp((2 * n * pi) * ii) = 1"
    1.10  proof -
    1.11    have "exp((2 * n * pi) * ii) = exp 0"
    1.12 @@ -751,15 +751,15 @@
    1.13      by blast
    1.14  qed
    1.15  
    1.16 -lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re z"
    1.17 +lemma Arg_eq_0: "Arg z = 0 \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re z"
    1.18  proof (cases "z=0")
    1.19    case True then show ?thesis
    1.20      by simp
    1.21  next
    1.22    case False
    1.23 -  have "z \<in> Reals \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
    1.24 +  have "z \<in> \<real> \<and> 0 \<le> Re z \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (of_real (cmod z) * exp (\<i> * complex_of_real (Arg z)))"
    1.25      by (metis Arg_eq)
    1.26 -  also have "... \<longleftrightarrow> z \<in> Reals \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
    1.27 +  also have "... \<longleftrightarrow> z \<in> \<real> \<and> 0 \<le> Re (exp (\<i> * complex_of_real (Arg z)))"
    1.28      using False
    1.29      by (simp add: zero_le_mult_iff)
    1.30    also have "... \<longleftrightarrow> Arg z = 0"
    1.31 @@ -955,7 +955,7 @@
    1.32  corollary Im_Ln_of_real [simp]: "r > 0 \<Longrightarrow> Im (ln (of_real r)) = 0"
    1.33    by (simp add: Ln_of_real)
    1.34  
    1.35 -lemma cmod_Ln_Reals [simp]: "z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    1.36 +lemma cmod_Ln_Reals [simp]: "z \<in> \<real> \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (ln z) = norm (ln (Re z))"
    1.37    using Ln_of_real by force
    1.38  
    1.39  lemma Ln_1: "ln 1 = (0::complex)"
    1.40 @@ -1565,10 +1565,10 @@
    1.41    using lim_Ln_over_power [of 1]
    1.42    by simp
    1.43  
    1.44 -lemma Ln_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
    1.45 +lemma Ln_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> Ln x = of_real (ln (Re x))"
    1.46    using Ln_of_real by force
    1.47  
    1.48 -lemma powr_Reals_eq: "x \<in> Reals \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
    1.49 +lemma powr_Reals_eq: "x \<in> \<real> \<Longrightarrow> Re x > 0 \<Longrightarrow> x powr complex_of_real y = of_real (x powr y)"
    1.50    by (simp add: powr_of_real)
    1.51  
    1.52  lemma lim_ln_over_power: