author huffman Sun May 20 17:49:10 2007 +0200 (2007-05-20) changeset 23052 0e36f0dbfa1c parent 23051 e98ed26577a2 child 23053 03fe1dafa418
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
```     1.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 17:30:21 2007 +0200
1.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 20 17:49:10 2007 +0200
1.3 @@ -510,16 +510,6 @@
1.4  apply (rule summable_cos [THEN summable_sums])
1.5  done
1.6
1.7 -lemma lemma_realpow_diff [rule_format (no_asm)]:
1.8 -     "p \<le> n --> y ^ (Suc n - p) = ((y::real) ^ (n - p)) * y"
1.9 -apply (induct "n", auto)
1.10 -apply (subgoal_tac "p = Suc n")
1.11 -apply (simp (no_asm_simp), auto)
1.12 -apply (drule sym)
1.13 -apply (simp add: Suc_diff_le mult_commute realpow_Suc [symmetric]
1.14 -       del: realpow_Suc)
1.15 -done
1.16 -
1.17
1.18  subsection{*Formal Derivatives of Exp, Sin, and Cos Series*}
1.19
1.20 @@ -1795,26 +1785,24 @@
1.21
1.22  lemma cos_arcsin: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<twosuperior>)"
1.23  apply (subgoal_tac "x\<twosuperior> \<le> 1")
1.24 -apply (rule power_eq_imp_eq_base [where n=2])
1.25 +apply (rule power2_eq_imp_eq)
1.27  apply (rule cos_ge_zero)
1.28  apply (erule (1) arcsin_lbound)
1.29  apply (erule (1) arcsin_ubound)
1.30  apply simp
1.31 -apply simp
1.32  apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> \<le> 1\<twosuperior>", simp)
1.33  apply (rule power_mono, simp, simp)
1.34  done
1.35
1.36  lemma sin_arccos: "\<lbrakk>-1 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<twosuperior>)"
1.37  apply (subgoal_tac "x\<twosuperior> \<le> 1")
1.38 -apply (rule power_eq_imp_eq_base [where n=2])
1.39 +apply (rule power2_eq_imp_eq)
1.41  apply (rule sin_ge_zero)
1.42  apply (erule (1) arccos_lbound)
1.43  apply (erule (1) arccos_ubound)
1.44  apply simp
1.45 -apply simp
1.46  apply (subgoal_tac "\<bar>x\<bar>\<twosuperior> \<le> 1\<twosuperior>", simp)
1.47  apply (rule power_mono, simp, simp)
1.48  done
1.49 @@ -1944,6 +1932,81 @@
1.50
1.51  subsection {* More Theorems about Sin and Cos *}
1.52
1.53 +lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
1.54 +proof -
1.55 +  let ?c = "cos (pi / 4)" and ?s = "sin (pi / 4)"
1.56 +  have nonneg: "0 \<le> ?c"
1.57 +    by (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
1.58 +  have "0 = cos (pi / 4 + pi / 4)"
1.59 +    by simp
1.60 +  also have "cos (pi / 4 + pi / 4) = ?c\<twosuperior> - ?s\<twosuperior>"
1.61 +    by (simp only: cos_add power2_eq_square)
1.62 +  also have "\<dots> = 2 * ?c\<twosuperior> - 1"
1.63 +    by (simp add: sin_squared_eq)
1.64 +  finally have "?c\<twosuperior> = (sqrt 2 / 2)\<twosuperior>"
1.65 +    by (simp add: power_divide)
1.66 +  thus ?thesis
1.67 +    using nonneg by (rule power2_eq_imp_eq) simp
1.68 +qed
1.69 +
1.70 +lemma cos_30: "cos (pi / 6) = sqrt 3 / 2"
1.71 +proof -
1.72 +  let ?c = "cos (pi / 6)" and ?s = "sin (pi / 6)"
1.73 +  have pos_c: "0 < ?c"
1.74 +    by (rule cos_gt_zero, simp, simp)
1.75 +  have "0 = cos (pi / 6 + pi / 6 + pi / 6)"
1.76 +    by (simp only: add_divide_distrib [symmetric], simp)
1.77 +  also have "\<dots> = (?c * ?c - ?s * ?s) * ?c - (?s * ?c + ?c * ?s) * ?s"
1.79 +  also have "\<dots> = ?c * (?c\<twosuperior> - 3 * ?s\<twosuperior>)"
1.80 +    by (simp add: ring_eq_simps power2_eq_square)
1.81 +  finally have "?c\<twosuperior> = (sqrt 3 / 2)\<twosuperior>"
1.82 +    using pos_c by (simp add: sin_squared_eq power_divide)
1.83 +  thus ?thesis
1.84 +    using pos_c [THEN order_less_imp_le]
1.85 +    by (rule power2_eq_imp_eq) simp
1.86 +qed
1.87 +
1.88 +lemma sin_45: "sin (pi / 4) = sqrt 2 / 2"
1.89 +proof -
1.90 +  have "sin (pi / 4) = cos (pi / 2 - pi / 4)" by (rule sin_cos_eq)
1.91 +  also have "pi / 2 - pi / 4 = pi / 4" by simp
1.92 +  also have "cos (pi / 4) = sqrt 2 / 2" by (rule cos_45)
1.93 +  finally show ?thesis .
1.94 +qed
1.95 +
1.96 +lemma sin_60: "sin (pi / 3) = sqrt 3 / 2"
1.97 +proof -
1.98 +  have "sin (pi / 3) = cos (pi / 2 - pi / 3)" by (rule sin_cos_eq)
1.99 +  also have "pi / 2 - pi / 3 = pi / 6" by simp
1.100 +  also have "cos (pi / 6) = sqrt 3 / 2" by (rule cos_30)
1.101 +  finally show ?thesis .
1.102 +qed
1.103 +
1.104 +lemma cos_60: "cos (pi / 3) = 1 / 2"
1.105 +apply (rule power2_eq_imp_eq)
1.106 +apply (simp add: cos_squared_eq sin_60 power_divide)
1.107 +apply (rule cos_ge_zero, rule order_trans [where y=0], simp_all)
1.108 +done
1.109 +
1.110 +lemma sin_30: "sin (pi / 6) = 1 / 2"
1.111 +proof -
1.112 +  have "sin (pi / 6) = cos (pi / 2 - pi / 6)" by (rule sin_cos_eq)
1.113 +  also have "pi / 2 - pi / 6 = pi / 3"
1.114 +    by (simp add: diff_divide_distrib [symmetric])
1.115 +  also have "cos (pi / 3) = 1 / 2" by (rule cos_60)
1.116 +  finally show ?thesis .
1.117 +qed
1.118 +
1.119 +lemma tan_30: "tan (pi / 6) = 1 / sqrt 3"
1.120 +unfolding tan_def by (simp add: sin_30 cos_30)
1.121 +
1.122 +lemma tan_45: "tan (pi / 4) = 1"
1.123 +unfolding tan_def by (simp add: sin_45 cos_45)
1.124 +
1.125 +lemma tan_60: "tan (pi / 3) = sqrt 3"
1.126 +unfolding tan_def by (simp add: sin_60 cos_60)
1.127 +
1.128  text{*NEEDED??*}
1.129  lemma [simp]:
1.130       "sin (x + 1 / 2 * real (Suc m) * pi) =
```