src/HOL/Hyperreal/MacLaurin.thy
changeset 19765 dfe940911617
parent 16924 04246269386e
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 20:12:59 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 23:22:29 2006 +0200
     1.3 @@ -31,18 +31,24 @@
     1.4  text{*A crude tactic to differentiate by proof.*}
     1.5  ML
     1.6  {*
     1.7 +local
     1.8 +val deriv_rulesI =
     1.9 +  [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
    1.10 +  thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
    1.11 +  thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
    1.12 +  thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
    1.13 +  thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
    1.14 +  thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
    1.15 +
    1.16 +val DERIV_chain2 = thm "DERIV_chain2";
    1.17 +
    1.18 +in
    1.19 +
    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 -val deriv_rulesI = [DERIV_Id,DERIV_const,DERIV_cos,DERIV_cmult,
    1.26 -                    DERIV_sin, DERIV_exp, DERIV_inverse,DERIV_pow,
    1.27 -                    DERIV_add, DERIV_diff, DERIV_mult, DERIV_minus,
    1.28 -                    DERIV_inverse_fun,DERIV_quotient,DERIV_fun_pow,
    1.29 -                    DERIV_fun_exp,DERIV_fun_sin,DERIV_fun_cos,
    1.30 -                    DERIV_Id,DERIV_const,DERIV_cos];
    1.31 -
    1.32  val deriv_tac =
    1.33    SUBGOAL (fn (prem,i) =>
    1.34     (resolve_tac deriv_rulesI i) ORELSE
    1.35 @@ -50,6 +56,8 @@
    1.36                       DERIV_chain2) i) handle DERIV_name => no_tac));;
    1.37  
    1.38  val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
    1.39 +
    1.40 +end
    1.41  *}
    1.42  
    1.43  lemma Maclaurin_lemma2: