src/HOL/Transcendental.thy
changeset 44745 b068207a7400
parent 44730 11a1290fd0ac
child 44746 9e4f7d3b5376
     1.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 17:45:37 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 18:06:02 2011 -0700
     1.3 @@ -1722,19 +1722,29 @@
     1.4  lemma sin_ge_zero: "[| 0 \<le> x; x \<le> pi |] ==> 0 \<le> sin x"
     1.5  by (auto simp add: order_le_less sin_gt_zero_pi)
     1.6  
     1.7 +text {* FIXME: This proof is almost identical to lemma @{text cos_is_zero}.
     1.8 +  It should be possible to factor out some of the common parts. *}
     1.9 +
    1.10  lemma cos_total: "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. 0 \<le> x & x \<le> pi & (cos x = y)"
    1.11 -apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y")
    1.12 -apply (rule_tac [2] IVT2)
    1.13 -apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos)
    1.14 -apply (cut_tac x = xa and y = y in linorder_less_linear)
    1.15 -apply (rule ccontr, auto)
    1.16 -apply (drule_tac f = cos in Rolle)
    1.17 -apply (drule_tac [5] f = cos in Rolle)
    1.18 -apply (auto intro: order_less_imp_le DERIV_isCont DERIV_cos
    1.19 -            dest!: DERIV_cos [THEN DERIV_unique]
    1.20 -            simp add: differentiable_def)
    1.21 -apply (auto dest: sin_gt_zero_pi [OF order_le_less_trans order_less_le_trans])
    1.22 -done
    1.23 +proof (rule ex_ex1I)
    1.24 +  assume y: "-1 \<le> y" "y \<le> 1"
    1.25 +  show "\<exists>x. 0 \<le> x & x \<le> pi & cos x = y"
    1.26 +    by (rule IVT2, simp_all add: y)
    1.27 +next
    1.28 +  fix a b
    1.29 +  assume a: "0 \<le> a \<and> a \<le> pi \<and> cos a = y"
    1.30 +  assume b: "0 \<le> b \<and> b \<le> pi \<and> cos b = y"
    1.31 +  have [simp]: "\<forall>x. cos differentiable x"
    1.32 +    unfolding differentiable_def by (auto intro: DERIV_cos)
    1.33 +  from a b show "a = b"
    1.34 +    apply (cut_tac less_linear [of a b], auto)
    1.35 +    apply (drule_tac f = cos in Rolle)
    1.36 +    apply (drule_tac [5] f = cos in Rolle)
    1.37 +    apply (auto dest!: DERIV_cos [THEN DERIV_unique])
    1.38 +    apply (metis order_less_le_trans less_le sin_gt_zero_pi)
    1.39 +    apply (metis order_less_le_trans less_le sin_gt_zero_pi)
    1.40 +    done
    1.41 +qed
    1.42  
    1.43  lemma sin_total:
    1.44       "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"