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 @@