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.5    by (rule ln_unique) (simp add: exp_add)
     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.40 +    by (metis abs_of_nonneg add.commute add_diff_cancel real_sqrt_abs)
    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.51 +    by (metis pi_ge_two pi_half_le_two add.commute add_le_cancel_left add_mono assms)
    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"