src/HOL/Transcendental.thy
 changeset 44725 d3bf0e33c98a parent 44710 9caf6883f1f4 child 44726 8478eab380e9
```     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])
```