src/HOL/Transcendental.thy
changeset 44730 11a1290fd0ac
parent 44728 86f43cca4886
child 44745 b068207a7400
     1.1 --- a/src/HOL/Transcendental.thy	Mon Sep 05 17:05:00 2011 -0700
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Sep 05 17:45:37 2011 -0700
     1.3 @@ -1528,19 +1528,24 @@
     1.4  lemmas cos_two_le_zero [simp] = cos_two_less_zero [THEN order_less_imp_le]
     1.5  
     1.6  lemma cos_is_zero: "EX! x. 0 \<le> x & x \<le> 2 & cos x = 0"
     1.7 -apply (subgoal_tac "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0")
     1.8 -apply (rule_tac [2] IVT2)
     1.9 -apply (auto intro: DERIV_isCont DERIV_cos)
    1.10 -apply (cut_tac x = xa and y = y in linorder_less_linear)
    1.11 -apply (rule ccontr)
    1.12 -apply (subgoal_tac " (\<forall>x. cos differentiable x) & (\<forall>x. isCont cos x) ")
    1.13 -apply (auto intro: DERIV_cos DERIV_isCont simp add: differentiable_def)
    1.14 -apply (drule_tac f = cos in Rolle)
    1.15 -apply (drule_tac [5] f = cos in Rolle)
    1.16 -apply (auto dest!: DERIV_cos [THEN DERIV_unique] simp add: differentiable_def)
    1.17 -apply (metis order_less_le_trans less_le sin_gt_zero)
    1.18 -apply (metis order_less_le_trans less_le sin_gt_zero)
    1.19 -done
    1.20 +proof (rule ex_ex1I)
    1.21 +  show "\<exists>x. 0 \<le> x & x \<le> 2 & cos x = 0"
    1.22 +    by (rule IVT2, simp_all)
    1.23 +next
    1.24 +  fix x y
    1.25 +  assume x: "0 \<le> x \<and> x \<le> 2 \<and> cos x = 0"
    1.26 +  assume y: "0 \<le> y \<and> y \<le> 2 \<and> cos y = 0"
    1.27 +  have [simp]: "\<forall>x. cos differentiable x"
    1.28 +    unfolding differentiable_def by (auto intro: DERIV_cos)
    1.29 +  from x y show "x = y"
    1.30 +    apply (cut_tac less_linear [of x y], auto)
    1.31 +    apply (drule_tac f = cos in Rolle)
    1.32 +    apply (drule_tac [5] f = cos in Rolle)
    1.33 +    apply (auto dest!: DERIV_cos [THEN DERIV_unique])
    1.34 +    apply (metis order_less_le_trans less_le sin_gt_zero)
    1.35 +    apply (metis order_less_le_trans less_le sin_gt_zero)
    1.36 +    done
    1.37 +qed
    1.38  
    1.39  lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
    1.40  by (simp add: pi_def)