src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
changeset 60141 833adf7db7d8
parent 60020 065ecea354d0
child 60150 bd773c47ad0b
     1.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Mon Apr 20 13:46:36 2015 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Tue Apr 21 17:19:00 2015 +0100
     1.3 @@ -1263,9 +1263,6 @@
     1.4  
     1.5  subsection{*Complex Powers*}
     1.6  
     1.7 -lemma powr_0 [simp]: "0 powr z = 0"
     1.8 -  by (simp add: powr_def)
     1.9 -
    1.10  lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
    1.11    by (simp add: powr_def)
    1.12  
    1.13 @@ -1526,7 +1523,7 @@
    1.14  proof -
    1.15    have nz0: "1 + \<i>*z \<noteq> 0"
    1.16      using assms
    1.17 -    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) 
    1.18 +    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
    1.19                less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
    1.20    have "z \<noteq> -\<i>" using assms
    1.21      by auto
    1.22 @@ -1771,7 +1768,7 @@
    1.23    by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
    1.24  
    1.25  lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
    1.26 -proof -  
    1.27 +proof -
    1.28    have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
    1.29      by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
    1.30    moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
    1.31 @@ -1903,7 +1900,7 @@
    1.32  proof (cases "Im z = 0")
    1.33    case True
    1.34    then show ?thesis
    1.35 -    using assms 
    1.36 +    using assms
    1.37      by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
    1.38  next
    1.39    case False