29 by arith |
29 by arith |
30 |
30 |
31 text{*A crude tactic to differentiate by proof.*} |
31 text{*A crude tactic to differentiate by proof.*} |
32 ML |
32 ML |
33 {* |
33 {* |
|
34 local |
|
35 val deriv_rulesI = |
|
36 [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult", |
|
37 thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow", |
|
38 thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus", |
|
39 thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow", |
|
40 thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos", |
|
41 thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"]; |
|
42 |
|
43 val DERIV_chain2 = thm "DERIV_chain2"; |
|
44 |
|
45 in |
|
46 |
34 exception DERIV_name; |
47 exception DERIV_name; |
35 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f |
48 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f |
36 | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f |
49 | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f |
37 | get_fun_name _ = raise DERIV_name; |
50 | get_fun_name _ = raise DERIV_name; |
38 |
|
39 val deriv_rulesI = [DERIV_Id,DERIV_const,DERIV_cos,DERIV_cmult, |
|
40 DERIV_sin, DERIV_exp, DERIV_inverse,DERIV_pow, |
|
41 DERIV_add, DERIV_diff, DERIV_mult, DERIV_minus, |
|
42 DERIV_inverse_fun,DERIV_quotient,DERIV_fun_pow, |
|
43 DERIV_fun_exp,DERIV_fun_sin,DERIV_fun_cos, |
|
44 DERIV_Id,DERIV_const,DERIV_cos]; |
|
45 |
51 |
46 val deriv_tac = |
52 val deriv_tac = |
47 SUBGOAL (fn (prem,i) => |
53 SUBGOAL (fn (prem,i) => |
48 (resolve_tac deriv_rulesI i) ORELSE |
54 (resolve_tac deriv_rulesI i) ORELSE |
49 ((rtac (read_instantiate [("f",get_fun_name prem)] |
55 ((rtac (read_instantiate [("f",get_fun_name prem)] |
50 DERIV_chain2) i) handle DERIV_name => no_tac));; |
56 DERIV_chain2) i) handle DERIV_name => no_tac));; |
51 |
57 |
52 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); |
58 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); |
|
59 |
|
60 end |
53 *} |
61 *} |
54 |
62 |
55 lemma Maclaurin_lemma2: |
63 lemma Maclaurin_lemma2: |
56 "[| \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t; |
64 "[| \<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t; |
57 n = Suc k; |
65 n = Suc k; |