add lemmas cos_arctan and sin_arctan
authorhuffman
Mon Sep 05 12:19:04 2011 -0700 (2011-09-05)
changeset 44725d3bf0e33c98a
parent 44724 0b900a9d8023
child 44726 8478eab380e9
add lemmas cos_arctan and sin_arctan
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 08:38:50 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 12:19:04 2011 -0700
     1.3 @@ -2230,14 +2230,26 @@
     1.4  lemma arctan_zero_zero [simp]: "arctan 0 = 0"
     1.5  by (insert arctan_tan [of 0], simp)
     1.6  
     1.7 -lemma cos_arctan_not_zero [simp]: "cos(arctan x) \<noteq> 0"
     1.8 -apply (auto simp add: cos_zero_iff)
     1.9 -apply (case_tac "n")
    1.10 -apply (case_tac [3] "n")
    1.11 -apply (cut_tac [2] y = x in arctan_ubound)
    1.12 -apply (cut_tac [4] y = x in arctan_lbound)
    1.13 -apply (auto simp add: real_of_nat_Suc left_distrib mult_less_0_iff)
    1.14 -done
    1.15 +lemma cos_arctan_not_zero [simp]: "cos (arctan x) \<noteq> 0"
    1.16 +  by (intro less_imp_neq [symmetric] cos_gt_zero_pi
    1.17 +    arctan_lbound arctan_ubound)
    1.18 +
    1.19 +lemma cos_arctan: "cos (arctan x) = 1 / sqrt (1 + x\<twosuperior>)"
    1.20 +proof (rule power2_eq_imp_eq)
    1.21 +  have "0 < 1 + x\<twosuperior>" by (simp add: add_pos_nonneg)
    1.22 +  show "0 \<le> 1 / sqrt (1 + x\<twosuperior>)" by simp
    1.23 +  show "0 \<le> cos (arctan x)"
    1.24 +    by (intro less_imp_le cos_gt_zero_pi arctan_lbound arctan_ubound)
    1.25 +  have "(cos (arctan x))\<twosuperior> * (1 + (tan (arctan x))\<twosuperior>) = 1"
    1.26 +    unfolding tan_def by (simp add: right_distrib power_divide)
    1.27 +  thus "(cos (arctan x))\<twosuperior> = (1 / sqrt (1 + x\<twosuperior>))\<twosuperior>"
    1.28 +    using `0 < 1 + x\<twosuperior>` by (simp add: power_divide eq_divide_eq)
    1.29 +qed
    1.30 +
    1.31 +lemma sin_arctan: "sin (arctan x) = x / sqrt (1 + x\<twosuperior>)"
    1.32 +  using add_pos_nonneg [OF zero_less_one zero_le_power2 [of x]]
    1.33 +  using tan_arctan [of x] unfolding tan_def cos_arctan
    1.34 +  by (simp add: eq_divide_eq)
    1.35  
    1.36  lemma tan_sec: "cos x \<noteq> 0 ==> 1 + tan(x) ^ 2 = inverse(cos x) ^ 2"
    1.37  apply (rule power_inverse [THEN subst])