src/HOL/Transcendental.thy
 changeset 59746 ddae5727c5a9 parent 59741 5b762cd73a8e child 59751 916c0f6c83e3
```     1.1 --- a/src/HOL/Transcendental.thy	Wed Mar 18 14:55:17 2015 +0000
1.2 +++ b/src/HOL/Transcendental.thy	Wed Mar 18 17:23:22 2015 +0000
1.3 @@ -1303,6 +1303,10 @@
1.4  lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
1.6
1.7 +lemma ln_setprod:
1.8 +    "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i > 0\<rbrakk> \<Longrightarrow> ln(setprod f I) = setsum (\<lambda>x. ln(f x)) I"
1.9 +  by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
1.10 +
1.11  lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.12    by (rule ln_unique) (simp add: exp_minus)
1.13
1.14 @@ -4153,6 +4157,85 @@
1.15    by simp
1.16
1.17
1.18 +subsection{* Prove Totality of the Trigonometric Functions *}
1.19 +
1.20 +lemma arccos_0 [simp]: "arccos 0 = pi/2"
1.21 +by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero pi_half_ge_zero not_le not_zero_less_neg_numeral numeral_One)
1.22 +
1.23 +lemma arccos_1 [simp]: "arccos 1 = 0"
1.24 +  using arccos_cos by force
1.25 +
1.26 +lemma arccos_le_pi2: "\<lbrakk>0 \<le> y; y \<le> 1\<rbrakk> \<Longrightarrow> arccos y \<le> pi/2"
1.27 +  by (metis (mono_tags) arccos_0 arccos cos_le_one cos_monotone_0_pi'
1.28 +      cos_pi cos_pi_half pi_half_ge_zero antisym_conv less_eq_neg_nonpos linear minus_minus order.trans order_refl)
1.29 +
1.30 +lemma sincos_total_pi_half:
1.31 +  assumes "0 \<le> x" "0 \<le> y" "x\<^sup>2 + y\<^sup>2 = 1"
1.32 +    shows "\<exists>t. 0 \<le> t \<and> t \<le> pi/2 \<and> x = cos t \<and> y = sin t"
1.33 +proof -
1.34 +  have x1: "x \<le> 1"
1.35 +    using assms
1.36 +    by (metis le_add_same_cancel1 power2_le_imp_le power_one zero_le_power2)
1.37 +  moreover with assms have ax: "0 \<le> arccos x" "cos(arccos x) = x"
1.38 +    by (auto simp: arccos)
1.39 +  moreover have "y = sqrt (1 - x\<^sup>2)" using assms
1.41 +  ultimately show ?thesis using assms arccos_le_pi2 [of x]
1.42 +    by (rule_tac x="arccos x" in exI) (auto simp: sin_arccos)
1.43 +qed
1.44 +
1.45 +lemma sincos_total_pi:
1.46 +  assumes "0 \<le> y" and "x\<^sup>2 + y\<^sup>2 = 1"
1.47 +    shows "\<exists>t. 0 \<le> t \<and> t \<le> pi \<and> x = cos t \<and> y = sin t"
1.48 +proof (cases rule: le_cases [of 0 x])
1.49 +  case le from sincos_total_pi_half [OF le]
1.50 +  show ?thesis
1.52 +next
1.53 +  case ge
1.54 +  then have "0 \<le> -x"
1.55 +    by simp
1.56 +  then obtain t where "t\<ge>0" "t \<le> pi/2" "-x = cos t" "y = sin t"
1.57 +    using sincos_total_pi_half assms
1.58 +    apply auto
1.59 +    by (metis `0 \<le> - x` power2_minus)
1.60 +  then show ?thesis
1.61 +    by (rule_tac x="pi-t" in exI, auto)
1.62 +qed
1.63 +
1.64 +lemma sincos_total_2pi_le:
1.65 +  assumes "x\<^sup>2 + y\<^sup>2 = 1"
1.66 +    shows "\<exists>t. 0 \<le> t \<and> t \<le> 2*pi \<and> x = cos t \<and> y = sin t"
1.67 +proof (cases rule: le_cases [of 0 y])
1.68 +  case le from sincos_total_pi [OF le]
1.69 +  show ?thesis
1.70 +    by (metis assms le_add_same_cancel1 mult.commute mult_2_right order.trans)
1.71 +next
1.72 +  case ge
1.73 +  then have "0 \<le> -y"
1.74 +    by simp
1.75 +  then obtain t where "t\<ge>0" "t \<le> pi" "x = cos t" "-y = sin t"
1.76 +    using sincos_total_pi assms
1.77 +    apply auto
1.78 +    by (metis `0 \<le> - y` power2_minus)
1.79 +  then show ?thesis
1.80 +    by (rule_tac x="2*pi-t" in exI, auto)
1.81 +qed
1.82 +
1.83 +lemma sincos_total_2pi:
1.84 +  assumes "x\<^sup>2 + y\<^sup>2 = 1"
1.85 +    obtains t where "0 \<le> t" "t < 2*pi" "x = cos t" "y = sin t"
1.86 +proof -
1.87 +  from sincos_total_2pi_le [OF assms]
1.88 +  obtain t where t: "0 \<le> t" "t \<le> 2*pi" "x = cos t" "y = sin t"
1.89 +    by blast
1.90 +  show ?thesis
1.91 +    apply (cases "t = 2*pi")
1.92 +    using t that
1.93 +    apply force+
1.94 +    done
1.95 +qed
1.96 +
1.97  subsection {* Machins formula *}
1.98
1.99  lemma arctan_one: "arctan 1 = pi / 4"
```