add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
authorhuffman
Sun May 20 17:49:10 2007 +0200 (2007-05-20)
changeset 230520e36f0dbfa1c
parent 23051 e98ed26577a2
child 23053 03fe1dafa418
add lemmas for sin,cos,tan of 30,45,60 degrees; cleaned up
src/HOL/Hyperreal/Transcendental.thy
     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.26  apply (simp add: cos_squared_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.40  apply (simp add: sin_squared_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.78 +    by (simp only: cos_add sin_add)
    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) =