src/HOL/MacLaurin.thy
changeset 31882 3578434d645d
parent 31881 eba74a5790d2
child 32038 4127b89f48ab
     1.1 --- a/src/HOL/MacLaurin.thy	Tue Jun 30 18:21:55 2009 +0200
     1.2 +++ b/src/HOL/MacLaurin.thy	Tue Jun 30 18:24:00 2009 +0200
     1.3 @@ -27,36 +27,6 @@
     1.4  lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
     1.5  by arith
     1.6  
     1.7 -text{*A crude tactic to differentiate by proof.*}
     1.8 -
     1.9 -lemmas deriv_rulesI =
    1.10 -  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
    1.11 -  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
    1.12 -  DERIV_add DERIV_diff DERIV_mult DERIV_minus
    1.13 -  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
    1.14 -  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
    1.15 -  DERIV_ident DERIV_const DERIV_cos
    1.16 -
    1.17 -ML
    1.18 -{*
    1.19 -local
    1.20 -exception DERIV_name;
    1.21 -fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
    1.22 -|   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
    1.23 -|   get_fun_name _ = raise DERIV_name;
    1.24 -
    1.25 -in
    1.26 -
    1.27 -fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
    1.28 -  resolve_tac @{thms deriv_rulesI} i ORELSE
    1.29 -    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
    1.30 -                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
    1.31 -
    1.32 -fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
    1.33 -
    1.34 -end
    1.35 -*}
    1.36 -
    1.37  lemma Maclaurin_lemma2:
    1.38    assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    1.39    assumes n: "n = Suc k"
    1.40 @@ -97,7 +67,6 @@
    1.41   apply (simp add: mult_ac)
    1.42  done
    1.43  
    1.44 -
    1.45  lemma Maclaurin:
    1.46    assumes h: "0 < h"
    1.47    assumes n: "0 < n"