: "exp (s * Ln z) * inverse z = exp ((s - 1) * Ln z)" + by (simp add: divide_complex_def exp_diff left_diff_distrib') show ?thesis unfolding powr_def proof (rule has_field_derivative_transform_within) show "((\z. exp (s * Ln z)) has_field_derivative s * (if z = 0 then 0 else exp ((s - 1) * Ln z))) (at z)" - apply (intro derivative_eq_intros | simp add: assms)+ - by (simp add: False divide_complex_def exp_diff left_diff_distrib') + by (intro derivative_eq_intros | simp add: assms False \

)+ qed (use False in auto) qed (use assms in auto) @@ -2281,11 +2293,11 @@ lemma has_field_derivative_powr_of_int: fixes z :: complex - assumes gderiv:"(g has_field_derivative gd) (at z within s)" and "g z\0" - shows "((\z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within s)" + assumes gderiv:"(g has_field_derivative gd) (at z within S)" and "g z\0" + shows "((\z. g z powr of_int n) has_field_derivative (n * g z powr (of_int n - 1) * gd)) (at z within S)" proof - define dd where "dd = of_int n * g z powr (of_int (n - 1)) * gd" - obtain e where "e>0" and e_dist:"\y\s. dist z y < e \ g y \ 0" + obtain e where "e>0" and e_dist:"\y\S. dist z y < e \ g y \ 0" using DERIV_continuous[OF gderiv,THEN continuous_within_avoid] \g z\0\ by auto have ?thesis when "n\0" proof - @@ -2298,19 +2310,19 @@ using powr_of_int[OF \g z\0\,of "n-1"] by (simp add: nat_diff_distrib') then show ?thesis unfolding dd_def dd'_def by simp qed (simp add:dd_def dd'_def) - then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s) - \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within s)" + then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within S) + \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within S)" by simp - also have "... \ ((\z. g z ^ nat n) has_field_derivative dd') (at z within s)" + also have "... \ ((\z. g z ^ nat n) has_field_derivative dd') (at z within S)" proof (rule has_field_derivative_cong_eventually) - show "\\<^sub>F x in at z within s. g x powr of_int n = g x ^ nat n" + show "\\<^sub>F x in at z within S. g x powr of_int n = g x ^ nat n" unfolding eventually_at apply (rule exI[where x=e]) using powr_of_int that \e>0\ e_dist by (simp add: dist_commute) qed (use powr_of_int \g z\0\ that in simp) also have "..." unfolding dd'_def using gderiv that by (auto intro!: derivative_eq_intros) - finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)" . + finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within S)" . then show ?thesis unfolding dd_def by simp qed moreover have ?thesis when "n<0" @@ -2323,12 +2335,12 @@ then show ?thesis unfolding dd_def dd'_def by (simp add: divide_inverse) qed - then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s) - \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within s)" + then have "((\z. g z powr of_int n) has_field_derivative dd) (at z within S) + \ ((\z. g z powr of_int n) has_field_derivative dd') (at z within S)" by simp - also have "... \ ((\z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within s)" + also have "... \ ((\z. inverse (g z ^ nat (-n))) has_field_derivative dd') (at z within S)" proof (rule has_field_derivative_cong_eventually) - show "\\<^sub>F x in at z within s. g x powr of_int n = inverse (g x ^ nat (- n))" + show "\\<^sub>F x in at z within S. g x powr of_int n = inverse (g x ^ nat (- n))" unfolding eventually_at apply (rule exI[where x=e]) using powr_of_int that \e>0\ e_dist by (simp add: dist_commute) @@ -2341,7 +2353,7 @@ unfolding dd'_def using gderiv that \g z\0\ by (auto intro!: derivative_eq_intros simp add:field_split_simps power_add[symmetric]) qed - finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within s)" . + finally have "((\z. g z powr of_int n) has_field_derivative dd) (at z within S)" . then show ?thesis unfolding dd_def by simp qed ultimately show ?thesis by force @@ -2349,27 +2361,25 @@ lemma field_differentiable_powr_of_int: fixes z :: complex - assumes gderiv:"g field_differentiable (at z within s)" and "g z\0" - shows "(\z. g z powr of_int n) field_differentiable (at z within s)" + assumes gderiv: "g field_differentiable (at z within S)" and "g z \ 0" + shows "(\z. g z powr of_int n) field_differentiable (at z within S)" using has_field_derivative_powr_of_int assms(2) field_differentiable_def gderiv by blast lemma holomorphic_on_powr_of_int [holomorphic_intros]: - assumes "f holomorphic_on s" "\z\s. f z\0" - shows "(\z. (f z) powr of_int n) holomorphic_on s" + assumes holf: "f holomorphic_on S" and 0: "\z. z\S \ f z \ 0" + shows "(\z. (f z) powr of_int n) holomorphic_on S" proof (cases "n\0") case True - then have "?thesis \ (\z. (f z) ^ nat n) holomorphic_on s" - apply (rule_tac holomorphic_cong) - using assms(2) by (auto simp add:powr_of_int) - moreover have "(\z. (f z) ^ nat n) holomorphic_on s" - using assms(1) by (auto intro:holomorphic_intros) + then have "?thesis \ (\z. (f z) ^ nat n) holomorphic_on S" + by (metis (no_types, lifting) 0 holomorphic_cong powr_of_int) + moreover have "(\z. (f z) ^ nat n) holomorphic_on S" + using holf by (auto intro: holomorphic_intros) ultimately show ?thesis by auto next case False - then have "?thesis \ (\z. inverse (f z) ^ nat (-n)) holomorphic_on s" - apply (rule_tac holomorphic_cong) - using assms(2) by (auto simp add:powr_of_int power_inverse) - moreover have "(\z. inverse (f z) ^ nat (-n)) holomorphic_on s" + then have "?thesis \ (\z. inverse (f z) ^ nat (-n)) holomorphic_on S" + by (metis (no_types, lifting) "0" holomorphic_cong power_inverse powr_of_int) + moreover have "(\z. inverse (f z) ^ nat (-n)) holomorphic_on S" using assms by (auto intro!:holomorphic_intros) ultimately show ?thesis by auto qed @@ -2580,10 +2590,12 @@ then obtain xo where "xo > 0" and xo: "\x. x \ xo \ x < e * exp (Re s * x)" using e by (auto simp: field_simps) have "norm (Ln (of_nat n) / of_nat n powr s) < e" if "n \ nat \exp xo\" for n - using e xo [of "ln n"] that - apply (auto simp: norm_divide norm_powr_real field_split_simps) - apply (metis exp_less_mono exp_ln not_le of_nat_0_less_iff) - done + proof - + have "ln (real n) \ xo" + using that exp_gt_zero ln_ge_iff [of n] nat_ceiling_le_eq by fastforce + then show ?thesis + using e xo [of "ln n"] by (auto simp: norm_divide norm_powr_real field_split_simps) + qed then show "\no. \n\no. norm (Ln (of_nat n) / of_nat n powr s) < e" by blast qed @@ -2594,17 +2606,17 @@ lemma lim_ln_over_power: fixes s :: real assumes "0 < s" - shows "((\n. ln n / (n powr s)) \ 0) sequentially" - using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms - apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) - done + shows "((\n. ln n / (n powr s)) \ 0) sequentially" +proof - + have "(\n. ln (Suc n) / (Suc n) powr s) \ 0" + using lim_Ln_over_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms + by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) + then show ?thesis + using filterlim_sequentially_Suc[of "\n::nat. ln n / n powr s"] by auto +qed lemma lim_ln_over_n [tendsto_intros]: "((\n. ln(real_of_nat n) / of_nat n) \ 0) sequentially" - using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]] - apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm) - done + using lim_ln_over_power [of 1] by auto lemma lim_log_over_n [tendsto_intros]: "(\n. log k n/n) \ 0" @@ -2633,12 +2645,10 @@ lemma lim_1_over_real_power: fixes s :: real assumes "0 < s" - shows "((\n. 1 / (of_nat n powr s)) \ 0) sequentially" + shows "((\n. 1 / (of_nat n powr s)) \ 0) sequentially" using lim_1_over_complex_power [of "of_real s", THEN filterlim_sequentially_Suc [THEN iffD2]] assms apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm) - apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide) - done + by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) lemma lim_1_over_Ln: "((\n. 1 / Ln(of_nat n)) \ 0) sequentially" proof (clarsimp simp add: lim_sequentially dist_norm norm_divide field_split_simps) @@ -2665,9 +2675,7 @@ lemma lim_1_over_ln: "((\n. 1 / ln(real_of_nat n)) \ 0) sequentially" using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]] apply (subst filterlim_sequentially_Suc [symmetric]) - apply (simp add: lim_sequentially dist_norm) - apply (simp add: Ln_Reals_eq norm_powr_real_powr norm_divide) - done + by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide) lemma lim_ln1_over_ln: "(\n. ln(Suc n) / ln n) \ 1" proof (rule Lim_transform_eventually) @@ -2719,10 +2727,9 @@ finally have "csqrt z = csqrt ((exp (Ln z / 2))\<^sup>2)" by simp also have "... = exp (Ln z / 2)" - apply (subst csqrt_square) + apply (rule csqrt_square) using cos_gt_zero_pi [of "(Im (Ln z) / 2)"] Im_Ln_le_pi mpi_less_Im_Ln assms - apply (auto simp: Re_exp Im_exp zero_less_mult_iff zero_le_mult_iff, fastforce+) - done + by (fastforce simp: Re_exp Im_exp ) finally show ?thesis using assms csqrt_square by simp qed @@ -2804,19 +2811,24 @@ "continuous (at z within (\ \ {w. 0 \ Re(w)})) csqrt" proof (cases "z \ \\<^sub>\\<^sub>0") case True - have *: "\e. \0 < e\ - \ \x'\\ \ {w. 0 \ Re w}. cmod x' < e^2 \ cmod (csqrt x') < e" - by (auto simp: Reals_def real_less_lsqrt) - have "Im z = 0" "Re z < 0 \ z = 0" + have [simp]: "Im z = 0" and 0: "Re z < 0 \ z = 0" using True cnj.code complex_cnj_zero_iff by (auto simp: Complex_eq complex_nonpos_Reals_iff) fastforce - with * show ?thesis - apply (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge]) - apply (auto simp: continuous_within_eps_delta) - using zero_less_power by blast -next - case False - then show ?thesis by (blast intro: continuous_within_csqrt) -qed + show ?thesis + using 0 + proof + assume "Re z < 0" + then show ?thesis + by (auto simp: continuous_within_closed_nontrivial [OF closed_Real_halfspace_Re_ge]) + next + assume "z = 0" + moreover + have "\e. 0 < e + \ \x'\\ \ {w. 0 \ Re w}. cmod x' < e^2 \ cmod (csqrt x') < e" + by (auto simp: Reals_def real_less_lsqrt) + ultimately show ?thesis + using zero_less_power by (fastforce simp: continuous_within_eps_delta) + qed +qed (blast intro: continuous_within_csqrt) subsection\Complex arctangent\ @@ -2870,32 +2882,32 @@ assumes "\Re z\ < pi/2" shows "Arctan(tan z) = z" proof - - have ge_pi2: "\n::int. \of_int (2*n + 1) * pi/2\ \ pi/2" - by (case_tac n rule: int_cases) (auto simp: abs_mult) - have "exp (\*z)*exp (\*z) = -1 \ exp (2*\*z) = -1" - by (metis distrib_right exp_add mult_2) - also have "... \ exp (2*\*z) = exp (\*pi)" - using cis_conv_exp cis_pi by auto - also have "... \ exp (2*\*z - \*pi) = 1" - by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute) - also have "... \ Re(\*2*z - \*pi) = 0 \ (\n::int. Im(\*2*z - \*pi) = of_int (2 * n) * pi)" - by (simp add: exp_eq_1) - also have "... \ Im z = 0 \ (\n::int. 2 * Re z = of_int (2*n + 1) * pi)" - by (simp add: algebra_simps) - also have "... \ False" - using assms ge_pi2 - apply (auto simp: algebra_simps) - by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral) - finally have *: "exp (\*z)*exp (\*z) + 1 \ 0" - by (auto simp: add.commute minus_unique) - show ?thesis - using assms * - apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps - i_times_eq_iff power2_eq_square [symmetric]) - apply (rule Ln_unique) - apply (auto simp: divide_simps exp_minus) - apply (simp add: algebra_simps exp_double [symmetric]) - done + have "Ln ((1 - \ * tan z) / (1 + \ * tan z)) = 2 * z / \" + proof (rule Ln_unique) + have ge_pi2: "\n::int. \of_int (2*n + 1) * pi/2\ \ pi/2" + by (case_tac n rule: int_cases) (auto simp: abs_mult) + have "exp (\*z)*exp (\*z) = -1 \ exp (2*\*z) = -1" + by (metis distrib_right exp_add mult_2) + also have "... \ exp (2*\*z) = exp (\*pi)" + using cis_conv_exp cis_pi by auto + also have "... \ exp (2*\*z - \*pi) = 1" + by (metis (no_types) diff_add_cancel diff_minus_eq_add exp_add exp_minus_inverse mult.commute) + also have "... \ Re(\*2*z - \*pi) = 0 \ (\n::int. Im(\*2*z - \*pi) = of_int (2 * n) * pi)" + by (simp add: exp_eq_1) + also have "... \ Im z = 0 \ (\n::int. 2 * Re z = of_int (2*n + 1) * pi)" + by (simp add: algebra_simps) + also have "... \ False" + using assms ge_pi2 + apply (auto simp: algebra_simps) + by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral) + finally have "exp (\*z)*exp (\*z) + 1 \ 0" + by (auto simp: add.commute minus_unique) + then show "exp (2 * z / \) = (1 - \ * tan z) / (1 + \ * tan z)" + apply (simp add: tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps) + by (simp add: algebra_simps flip: power2_eq_square exp_double) + qed (use assms in auto) + then show ?thesis + by (auto simp: Arctan_def) qed lemma @@ -2930,12 +2942,11 @@ show "\Re(Arctan z)\ < pi/2" unfolding Arctan_def divide_complex_def using mpi_less_Im_Ln [OF nzi] - apply (auto simp: abs_if intro!: Im_Ln_less_pi * [unfolded divide_complex_def]) - done + by (auto simp: abs_if intro!: Im_Ln_less_pi * [unfolded divide_complex_def]) show "(Arctan has_field_derivative inverse(1 + z\<^sup>2)) (at z)" unfolding Arctan_def scaleR_conv_of_real apply (intro derivative_eq_intros | simp add: nz0 *)+ - using nz0 nz1 zz + using nz1 zz apply (simp add: field_split_simps power2_eq_square) apply algebra done @@ -3077,10 +3088,12 @@ proof - have ne: "1 + x\<^sup>2 \ 0" by (metis power_one sum_power2_eq_zero_iff zero_neq_one) + have ne1: "1 + \ * complex_of_real x \ 0" + using Complex_eq complex_eq_cancel_iff2 by fastforce have "Re (Ln ((1 - \ * x) * inverse (1 + \ * x))) = 0" apply (rule norm_exp_imaginary) - apply (subst exp_Ln) - using ne apply (simp_all add: cmod_def complex_eq_iff) + using ne + apply (simp add: ne1 cmod_def) apply (auto simp: field_split_simps) apply algebra done @@ -3090,11 +3103,10 @@ lemma arctan_eq_Re_Arctan: "arctan x = Re (Arctan (of_real x))" proof (rule arctan_unique) - show "- (pi / 2) < Re (Arctan (complex_of_real x))" - apply (simp add: Arctan_def) - apply (rule Im_Ln_less_pi) - apply (auto simp: Im_complex_div_lemma complex_nonpos_Reals_iff) - done + have "(1 - \ * x) / (1 + \ * x) \ \\<^sub>\\<^sub>0" + by (auto simp: Im_complex_div_lemma complex_nonpos_Reals_iff) + then show "- (pi / 2) < Re (Arctan (complex_of_real x))" + by (simp add: Arctan_def Im_Ln_less_pi) next have *: " (1 - \*x) / (1 + \*x) \ 0" by (simp add: field_split_simps) ( simp add: complex_eq_iff) @@ -3103,12 +3115,14 @@ by (simp add: Arctan_def) next have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))" - apply (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos) - apply (simp add: field_simps) - by (simp add: power2_eq_square) + by (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos field_simps power2_eq_square) also have "... = x" - apply (subst tan_Arctan, auto) - by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one) + proof - + have "(complex_of_real x)\<^sup>2 \ - 1" + by (metis diff_0_right minus_diff_eq mult_zero_left not_le of_real_1 of_real_eq_iff of_real_minus of_real_power power2_eq_square real_minus_mult_self_le zero_less_one) + then show ?thesis + by simp + qed finally show "tan (Re (Arctan (complex_of_real x))) = x" . qed @@ -3169,18 +3183,14 @@ assumes "\x * y\ < 1" shows "(arctan x + arctan y = arctan((x + y) / (1 - x * y)))" proof (cases "x = 0 \ y = 0") - case True then show ?thesis - by auto -next case False - then have *: "\arctan x\ < pi / 2 - \arctan y\" using assms - apply (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff) - apply (simp add: field_split_simps abs_mult) - done - show ?thesis - apply (rule arctan_add_raw) - using * by linarith -qed + with assms have "\x\ < inverse \y\" + by (simp add: field_split_simps abs_mult) + with False have "\arctan x\ < pi / 2 - \arctan y\" using assms + by (auto simp add: abs_arctan arctan_inverse [symmetric] arctan_less_iff) + then show ?thesis + by (intro arctan_add_raw) linarith +qed auto lemma abs_arctan_le: fixes x::real shows "\arctan x\ \ \x\" @@ -3190,9 +3200,8 @@ have "cmod (Arctan w - Arctan z) \ 1 * cmod (w-z)" if "w \ \" "z \ \" for w z apply (rule field_differentiable_bound [OF convex_Reals, of Arctan _ 1]) apply (rule has_field_derivative_at_within [OF has_field_derivative_Arctan]) - using 1 that apply (auto simp: Reals_def) - done - then have "cmod (Arctan (of_real x) - Arctan 0) \ 1 * cmod (of_real x -0)" + using 1 that by (auto simp: Reals_def) + then have "cmod (Arctan (of_real x) - Arctan 0) \ 1 * cmod (of_real x - 0)" using Reals_0 Reals_of_real by blast then show ?thesis by (simp add: Arctan_of_real) @@ -3254,8 +3263,7 @@ lemma Arcsin_body_lemma: "\ * z + csqrt(1 - z\<^sup>2) \ 0" using power2_csqrt [of "1 - z\<^sup>2"] - apply auto - by (metis complex_i_mult_minus diff_add_cancel diff_minus_eq_add diff_self mult.assoc mult.left_commute numeral_One power2_csqrt power2_eq_square zero_neq_numeral) + by (metis add.inverse_inverse complex_i_mult_minus diff_0 diff_add_cancel diff_minus_eq_add mult.assoc mult.commute numeral_One power2_eq_square zero_neq_numeral) lemma Arcsin_range_lemma: "\Re z\ < 1 \ 0 < Re(\ * z + csqrt(1 - z\<^sup>2))" using Complex.cmod_power2 [of z, symmetric] @@ -3268,12 +3276,19 @@ by (simp add: Arcsin_def Arcsin_body_lemma) lemma one_minus_z2_notin_nonpos_Reals: - assumes "(Im z = 0 \ \Re z\ < 1)" + assumes "Im z = 0 \ \Re z\ < 1" shows "1 - z\<^sup>2 \ \\<^sub>\\<^sub>0" - using assms - apply (auto simp: complex_nonpos_Reals_iff Re_power2 Im_power2) - using power2_less_0 [of "Im z"] apply force - using abs_square_less_1 not_le by blast +proof (cases "Im z = 0") + case True + with assms show ?thesis + by (simp add: complex_nonpos_Reals_iff flip: abs_square_less_1) +next + case False + have "\ (Im z)\<^sup>2 \ - 1" + using False power2_less_eq_zero_iff by fastforce + with False show ?thesis + by (auto simp add: complex_nonpos_Reals_iff Re_power2 Im_power2) +qed lemma isCont_Arcsin_lemma: assumes le0: "Re (\ * z + csqrt (1 - z\<^sup>2)) \ 0" and "(Im z = 0 \ \Re z\ < 1)" @@ -3356,9 +3371,7 @@ by (simp add: field_simps power2_eq_square) also have "... = - (\ * Ln (((exp (\*z) + inverse (exp (\*z)))/2) - (inverse (exp (\*z)) - exp (\*z)) / 2))" apply (subst csqrt_square) - using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma - apply auto - done + using assms Re_eq_pihalf_lemma Re_less_pihalf_lemma by auto also have "... = - (\ * Ln (exp (\*z)))" by (simp add: field_simps power2_eq_square) also have "... = z" @@ -3453,11 +3466,8 @@ then show False using False by (simp add: power2_eq_square algebra_simps) qed - moreover have "(Im z)\<^sup>2 = ((1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2)" - apply (subst Imz) - using abs_Re_le_cmod [of "1-z\<^sup>2"] - apply (simp add: Re_power2) - done + moreover have "(Im z)\<^sup>2 = (1 + ((Im z)\<^sup>2 + cmod (1 - z\<^sup>2)) - (Re z)\<^sup>2) / 2" + using abs_Re_le_cmod [of "1-z\<^sup>2"] by (subst Imz) (simp add: Re_power2) ultimately show False by (simp add: cmod_power2) qed @@ -3469,14 +3479,12 @@ have "z + \ * csqrt (1 - z\<^sup>2) \ \\<^sub>\\<^sub>0" by (metis complex_nonpos_Reals_iff isCont_Arccos_lemma assms) with assms show ?thesis - apply (simp add: Arccos_def) - apply (rule isCont_Ln' isCont_csqrt' continuous_intros)+ - apply (simp_all add: one_minus_z2_notin_nonpos_Reals assms) - done + unfolding Arccos_def + by (simp_all add: one_minus_z2_notin_nonpos_Reals assms) qed lemma isCont_Arccos' [simp]: - shows "isCont f z \ (Im (f z) = 0 \ \Re (f z)\ < 1) \ isCont (\x. Arccos (f x)) z" + "isCont f z \ (Im (f z) = 0 \ \Re (f z)\ < 1) \ isCont (\x. Arccos (f x)) z" by (blast intro: isCont_o2 [OF _ isCont_Arccos]) lemma cos_Arccos [simp]: "cos(Arccos z) = z" @@ -3486,15 +3494,13 @@ moreover have "... \ z + \ * csqrt (1 - z\<^sup>2) = 0" by (metis distrib_right mult_eq_0_iff zero_neq_numeral) ultimately show ?thesis - apply (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps) - apply (simp add: power2_eq_square [symmetric]) - done + by (simp add: cos_exp_eq Arccos_def Arccos_body_lemma exp_minus field_simps flip: power2_eq_square) qed lemma Arccos_cos: - assumes "0 < Re z & Re z < pi \ - Re z = 0 & 0 \ Im z \ - Re z = pi & Im z \ 0" + assumes "0 < Re z \ Re z < pi \ + Re z = 0 \ 0 \ Im z \ + Re z = pi \ Im z \ 0" shows "Arccos(cos z) = z" proof - have *: "((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z))) = sin z" @@ -3508,14 +3514,12 @@ \ * ((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z)))))" apply (subst csqrt_square) using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z] - apply (auto simp: * Re_sin Im_sin) - done + by (auto simp: * Re_sin Im_sin) also have "... = - (\ * Ln (exp (\*z)))" by (simp add: field_simps power2_eq_square) also have "... = z" using assms - apply (subst Complex_Transcendental.Ln_exp, auto) - done + by (subst Complex_Transcendental.Ln_exp, auto) finally show ?thesis . qed @@ -3596,9 +3600,7 @@ proof - have "(Im (Arccos w))\<^sup>2 \ (cmod (cos (Arccos w)))\<^sup>2 - (cos (Re (Arccos w)))\<^sup>2" using norm_cos_squared [of "Arccos w"] real_le_abs_sinh [of "Im (Arccos w)"] - apply (simp only: abs_le_square_iff) - apply (simp add: field_split_simps) - done + by (simp only: abs_le_square_iff) (simp add: field_split_simps) also have "... \ (cmod w)\<^sup>2" by (auto simp: cmod_power2) finally show ?thesis @@ -3651,7 +3653,7 @@ by (metis mult_cancel_left zero_neq_numeral) then have "(\ * z + csqrt (1 - z\<^sup>2))\<^sup>2 \ -1" using assms - apply (auto simp: power2_sum) + apply (simp add: power2_sum) apply (simp add: power2_eq_square algebra_simps) done then show ?thesis @@ -3685,9 +3687,7 @@ by (metis mult_cancel_left2 zero_neq_numeral) (*FIXME cancel_numeral_factor*) then have "(z + \ * csqrt (1 - z\<^sup>2))\<^sup>2 \ 1" using assms - apply (auto simp: Power.comm_semiring_1_class.power2_sum power_mult_distrib) - apply (simp add: power2_eq_square algebra_simps) - done + by (metis Arccos_def add.commute add.left_neutral cancel_comm_monoid_add_class.diff_cancel cos_Arccos csqrt_0 mult_zero_right) then show ?thesis apply (simp add: sin_exp_eq Arccos_def exp_minus) apply (simp add: divide_simps Arccos_body_lemma) @@ -3698,20 +3698,18 @@ lemma cos_sin_csqrt: assumes "0 < cos(Re z) \ cos(Re z) = 0 \ Im z * sin(Re z) \ 0" shows "cos z = csqrt(1 - (sin z)\<^sup>2)" - apply (rule csqrt_unique [THEN sym]) - apply (simp add: cos_squared_eq) - using assms - apply (auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff) - done +proof (rule csqrt_unique [THEN sym]) + show "(cos z)\<^sup>2 = 1 - (sin z)\<^sup>2" + by (simp add: cos_squared_eq) +qed (use assms in \auto simp: Re_cos Im_cos add_pos_pos mult_le_0_iff zero_le_mult_iff\) lemma sin_cos_csqrt: assumes "0 < sin(Re z) \ sin(Re z) = 0 \ 0 \ Im z * cos(Re z)" shows "sin z = csqrt(1 - (cos z)\<^sup>2)" - apply (rule csqrt_unique [THEN sym]) - apply (simp add: sin_squared_eq) - using assms - apply (auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff) - done +proof (rule csqrt_unique [THEN sym]) + show "(sin z)\<^sup>2 = 1 - (cos z)\<^sup>2" + by (simp add: sin_squared_eq) +qed (use assms in \auto simp: Re_sin Im_sin add_pos_pos mult_le_0_iff zero_le_mult_iff\) lemma Arcsin_Arccos_csqrt_pos: "(0 < Re z | Re z = 0 & 0 \ Im z) \ Arcsin z = Arccos(csqrt(1 - z\<^sup>2))" @@ -3770,10 +3768,8 @@ fix x' assume "- (pi / 2) \ x'" "x' \ pi / 2" "x = sin x'" then show "x' = Re (Arcsin (complex_of_real (sin x')))" - apply (simp add: sin_of_real [symmetric]) - apply (subst Arcsin_sin) - apply (auto simp: ) - done + unfolding sin_of_real [symmetric] + by (subst Arcsin_sin) auto qed lemma of_real_arcsin: "\x\ \ 1 \ of_real(arcsin x) = Arcsin(of_real x)" @@ -3820,10 +3816,8 @@ fix x' assume "0 \ x'" "x' \ pi" "x = cos x'" then show "x' = Re (Arccos (complex_of_real (cos x')))" - apply (simp add: cos_of_real [symmetric]) - apply (subst Arccos_cos) - apply (auto simp: ) - done + unfolding cos_of_real [symmetric] + by (subst Arccos_cos) auto qed lemma of_real_arccos: "\x\ \ 1 \ of_real(arccos x) = Arccos(of_real x)" @@ -3861,8 +3855,7 @@ have "arcsin x = pi/2 - arccos x" apply (rule sin_inj_pi) using assms arcsin [OF assms] arccos [OF assms] - apply (auto simp: algebra_simps sin_diff) - done + by (auto simp: algebra_simps sin_diff) then show ?thesis by (simp add: algebra_simps) qed @@ -3975,7 +3968,7 @@ then show ?thesis apply (simp add: exp_of_nat_mult [symmetric] mult_ac exp_Euler) apply (simp only: * cos_of_real sin_of_real) - apply (simp add: ) + apply simp done qed @@ -3993,10 +3986,7 @@ also have "... \ (\z::int. of_nat j = of_nat k + of_nat n * (of_int z :: complex))" by simp also have "... \ (\z::int. of_nat j = of_nat k + of_nat n * z)" - apply (rule HOL.iff_exI) - apply (auto simp: ) - using of_int_eq_iff apply fastforce - by (metis of_int_add of_int_mult of_int_of_nat_eq) + by (metis (mono_tags, hide_lams) of_int_add of_int_eq_iff of_int_mult of_int_of_nat_eq) also have "... \ int j mod int n = int k mod int n" by (auto simp: mod_eq_dvd_iff dvd_def algebra_simps) also have "... \ j mod n = k mod n" @@ -4038,7 +4028,7 @@ lemma complex_roots_unity: assumes "1 \ n" - shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j::nat. j < n}" + shows "{z::complex. z^n = 1} = {exp(2 * of_real pi * \ * of_nat j / of_nat n) | j. j < n}" apply (rule Finite_Set.card_seteq [symmetric]) using assms apply (auto simp: card_complex_roots_unity_explicit finite_roots_unity complex_root_unity card_roots_unity) @@ -4053,6 +4043,4 @@ apply (auto simp: Re_complex_div_eq_0 exp_of_nat_mult [symmetric] mult_ac exp_Euler) done - - end