1720 qed |
1720 qed |
1721 |
1721 |
1722 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x" |
1722 lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x" |
1723 by (auto simp add: order_le_less sin_gt_zero_pi) |
1723 by (auto simp add: order_le_less sin_gt_zero_pi) |
1724 |
1724 |
|
1725 text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}. |
|
1726 It should be possible to factor out some of the common parts. *} |
|
1727 |
1725 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)" |
1728 lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)" |
1726 apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y") |
1729 proof (rule ex_ex1I) |
1727 apply (rule_tac [2] IVT2) |
1730 assume y: "-1 \<le> y" "y \<le> 1" |
1728 apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos) |
1731 show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y" |
1729 apply (cut_tac x = xa and y = y in linorder_less_linear) |
1732 by (rule IVT2, simp_all add: y) |
1730 apply (rule ccontr, auto) |
1733 next |
1731 apply (drule_tac f = cos in Rolle) |
1734 fix a b |
1732 apply (drule_tac [5] f = cos in Rolle) |
1735 assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y" |
1733 apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos |
1736 assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y" |
1734 dest!: DERIV_cos [THEN DERIV_unique] |
1737 have [simp]: "\<forall>x. cos differentiable x" |
1735 simp add: differentiable_def) |
1738 unfolding differentiable_def by (auto intro: DERIV_cos) |
1736 apply (auto dest: sin_gt_zero_pi [OF order_le_less_trans order_less_le_trans]) |
1739 from a b show "a = b" |
1737 done |
1740 apply (cut_tac less_linear [of a b], auto) |
|
1741 apply (drule_tac f = cos in Rolle) |
|
1742 apply (drule_tac [5] f = cos in Rolle) |
|
1743 apply (auto dest!: DERIV_cos [THEN DERIV_unique]) |
|
1744 apply (metis order_less_le_trans less_le sin_gt_zero_pi) |
|
1745 apply (metis order_less_le_trans less_le sin_gt_zero_pi) |
|
1746 done |
|
1747 qed |
1738 |
1748 |
1739 lemma sin_total: |
1749 lemma sin_total: |
1740 "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)" |
1750 "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)" |
1741 apply (rule ccontr) |
1751 apply (rule ccontr) |
1742 apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))") |
1752 apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))") |