equal
deleted
inserted
replaced
1360 |
1360 |
1361 lemma isCont_cos [simp]: "isCont cos x" |
1361 lemma isCont_cos [simp]: "isCont cos x" |
1362 by (rule DERIV_cos [THEN DERIV_isCont]) |
1362 by (rule DERIV_cos [THEN DERIV_isCont]) |
1363 |
1363 |
1364 |
1364 |
|
1365 declare |
|
1366 DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
|
1367 DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
|
1368 DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
|
1369 DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
|
1370 |
1365 subsection {* Properties of Sine and Cosine *} |
1371 subsection {* Properties of Sine and Cosine *} |
1366 |
1372 |
1367 lemma sin_zero [simp]: "sin 0 = 0" |
1373 lemma sin_zero [simp]: "sin 0 = 0" |
1368 unfolding sin_def sin_coeff_def by (simp add: powser_zero) |
1374 unfolding sin_def sin_coeff_def by (simp add: powser_zero) |
1369 |
1375 |
1510 "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m" |
1516 "DERIV g x :> m ==> DERIV (%x. cos(g x)) x :> -sin(g x) * m" |
1511 apply (rule lemma_DERIV_subst) |
1517 apply (rule lemma_DERIV_subst) |
1512 apply (rule_tac f = cos in DERIV_chain2) |
1518 apply (rule_tac f = cos in DERIV_chain2) |
1513 apply (rule DERIV_cos, auto) |
1519 apply (rule DERIV_cos, auto) |
1514 done |
1520 done |
1515 |
|
1516 lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult |
|
1517 DERIV_sin DERIV_exp DERIV_inverse DERIV_pow |
|
1518 DERIV_add DERIV_diff DERIV_mult DERIV_minus |
|
1519 DERIV_inverse_fun DERIV_quotient DERIV_fun_pow |
|
1520 DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos |
|
1521 |
1521 |
1522 (* lemma *) |
1522 (* lemma *) |
1523 lemma lemma_DERIV_sin_cos_add: |
1523 lemma lemma_DERIV_sin_cos_add: |
1524 "\<forall>x. |
1524 "\<forall>x. |
1525 DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + |
1525 DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 + |
1720 apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def) |
1720 apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def) |
1721 apply (drule_tac y1 = xa in order_le_less_trans [THEN sin_gt_zero]) |
1721 apply (drule_tac y1 = xa in order_le_less_trans [THEN sin_gt_zero]) |
1722 apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) |
1722 apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) |
1723 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) |
1723 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) |
1724 done |
1724 done |
1725 |
1725 |
1726 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)" |
1726 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)" |
1727 by (simp add: pi_def) |
1727 by (simp add: pi_def) |
1728 |
1728 |
1729 lemma cos_pi_half [simp]: "cos (pi / 2) = 0" |
1729 lemma cos_pi_half [simp]: "cos (pi / 2) = 0" |
1730 by (simp add: pi_half cos_is_zero [THEN theI']) |
1730 by (simp add: pi_half cos_is_zero [THEN theI']) |
2497 apply (simp add: power_inverse tan_sec [symmetric]) |
2497 apply (simp add: power_inverse tan_sec [symmetric]) |
2498 apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp) |
2498 apply (subgoal_tac "0 < 1 + x\<twosuperior>", simp) |
2499 apply (simp add: add_pos_nonneg) |
2499 apply (simp add: add_pos_nonneg) |
2500 apply (simp, simp, simp, rule isCont_arctan) |
2500 apply (simp, simp, simp, rule isCont_arctan) |
2501 done |
2501 done |
|
2502 |
|
2503 declare |
|
2504 DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
|
2505 DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
|
2506 DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros] |
2502 |
2507 |
2503 subsection {* More Theorems about Sin and Cos *} |
2508 subsection {* More Theorems about Sin and Cos *} |
2504 |
2509 |
2505 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2" |
2510 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2" |
2506 proof - |
2511 proof - |