src/HOL/Multivariate_Analysis/Complex_Transcendental.thy

 
 
 
 subsection{*Complex Powers*}
 
-lemma powr_0 [simp]: "0 powr z = 0"
-  by (simp add: powr_def)
-
 lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
   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)"

   shows Re_Arctan_bounds: "abs(Re(Arctan z)) < pi/2"
     and has_field_derivative_Arctan: "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)"
 proof -
   have nz0: "1 + \<i>*z \<noteq> 0"
     using assms
-    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2) 
+    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
               less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
   have "z \<noteq> -\<i>" using assms
     by auto
   then have zz: "1 + z * z \<noteq> 0"
     by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)

 lemma isCont_Arcsin' [simp]:
   shows "isCont f z \<Longrightarrow> (Im (f z) = 0 \<Longrightarrow> \<bar>Re (f z)\<bar> < 1) \<Longrightarrow> isCont (\<lambda>x. Arcsin (f x)) z"
   by (blast intro: isCont_o2 [OF _ isCont_Arcsin])
 
 lemma sin_Arcsin [simp]: "sin(Arcsin z) = z"
-proof -  
+proof -
   have "\<i>*z*2 + csqrt (1 - z\<^sup>2)*2 = 0 \<longleftrightarrow> (\<i>*z)*2 + csqrt (1 - z\<^sup>2)*2 = 0"
     by (simp add: algebra_simps)  --{*Cancelling a factor of 2*}
   moreover have "... \<longleftrightarrow> (\<i>*z) + csqrt (1 - z\<^sup>2) = 0"
     by (metis Arcsin_body_lemma distrib_right no_zero_divisors zero_neq_numeral)
   ultimately show ?thesis

   assumes "(Im z = 0 \<Longrightarrow> \<bar>Re z\<bar> < 1)"  "Im (z + \<i> * csqrt (1 - z\<^sup>2)) = 0"
     shows "0 < Re (z + \<i> * csqrt (1 - z\<^sup>2))"
 proof (cases "Im z = 0")
   case True
   then show ?thesis
-    using assms 
+    using assms
     by (fastforce simp add: cmod_def Re_power2 Im_power2 algebra_simps abs_square_less_1 [symmetric])
 next
   case False
   have Imz: "Im z = - sqrt ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)"
     using assms abs_Re_le_cmod [of "1-z\<^sup>2"]