src/HOL/Hyperreal/MacLaurin.thy
changeset 24998 a339b33adfaf
parent 24180 9f818139951b
child 25112 98824cc791c0
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Oct 12 08:31:57 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Oct 12 10:24:49 2007 +0200
     1.3 @@ -109,15 +109,8 @@
     1.4  apply (rule DERIV_unique)
     1.5  prefer 2 apply assumption
     1.6  apply force
     1.7 -apply (subgoal_tac "\<forall>ta. 0 \<le> ta & ta \<le> t --> (difg (Suc n)) differentiable ta")
     1.8 -apply (simp add: differentiable_def)
     1.9 -apply (blast dest!: DERIV_isCont)
    1.10 -apply (simp add: differentiable_def, clarify)
    1.11 -apply (rule_tac x = "difg (Suc (Suc n)) ta" in exI)
    1.12 -apply force
    1.13 -apply (simp add: differentiable_def, clarify)
    1.14 -apply (rule_tac x = "difg (Suc (Suc n)) x" in exI)
    1.15 -apply force
    1.16 +apply (metis DERIV_isCont dlo_simps(4) dlo_simps(9) less_trans_Suc nat_less_le not_less_eq real_le_trans)
    1.17 +apply (metis Suc_less_eq differentiableI dlo_simps(7) dlo_simps(8) dlo_simps(9)   real_le_trans xt1(8))
    1.18  done
    1.19  
    1.20  lemma Maclaurin:
    1.21 @@ -183,15 +176,8 @@
    1.22  apply force
    1.23  apply (rule allI, induct_tac "ma")
    1.24  apply (rule impI, rule Rolle, assumption, simp, simp)
    1.25 -apply (subgoal_tac "\<forall>t. 0 \<le> t & t \<le> h --> g differentiable t")
    1.26 -apply (simp add: differentiable_def)
    1.27 -apply (blast dest: DERIV_isCont)
    1.28 -apply (simp add: differentiable_def, clarify)
    1.29 -apply (rule_tac x = "difg (Suc 0) t" in exI)
    1.30 -apply force
    1.31 -apply (simp add: differentiable_def, clarify)
    1.32 -apply (rule_tac x = "difg (Suc 0) x" in exI)
    1.33 -apply force
    1.34 +apply (metis DERIV_isCont zero_less_Suc)
    1.35 +apply (metis One_nat_def differentiableI dlo_simps(7))
    1.36  apply safe
    1.37  apply force
    1.38  apply (frule Maclaurin_lemma3, assumption+, safe)