27 |
27 |
28 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))" |
28 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))" |
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 |
|
33 lemmas deriv_rulesI = |
|
34 DERIV_ident DERIV_const DERIV_cos DERIV_cmult |
|
35 DERIV_sin DERIV_exp DERIV_inverse DERIV_pow |
|
36 DERIV_add DERIV_diff DERIV_mult DERIV_minus |
|
37 DERIV_inverse_fun DERIV_quotient DERIV_fun_pow |
|
38 DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos |
|
39 DERIV_ident DERIV_const DERIV_cos |
|
40 |
32 ML |
41 ML |
33 {* |
42 {* |
34 local |
43 local |
35 val deriv_rulesI = |
|
36 [thm "DERIV_ident", 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_ident", thm "DERIV_const", thm "DERIV_cos"]; |
|
42 |
|
43 val DERIV_chain2 = thm "DERIV_chain2"; |
|
44 |
|
45 in |
|
46 |
|
47 exception DERIV_name; |
44 exception DERIV_name; |
48 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f |
45 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f |
49 | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f |
46 | get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f |
50 | get_fun_name _ = raise DERIV_name; |
47 | get_fun_name _ = raise DERIV_name; |
51 |
48 |
|
49 in |
|
50 |
52 val deriv_tac = |
51 val deriv_tac = |
53 SUBGOAL (fn (prem,i) => |
52 SUBGOAL (fn (prem,i) => |
54 (resolve_tac deriv_rulesI i) ORELSE |
53 (resolve_tac @{thms deriv_rulesI} i) ORELSE |
55 ((rtac (read_instantiate [("f",get_fun_name prem)] |
54 ((rtac (read_instantiate [("f",get_fun_name prem)] |
56 DERIV_chain2) i) handle DERIV_name => no_tac));; |
55 @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));; |
57 |
56 |
58 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); |
57 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i)); |
59 |
58 |
60 end |
59 end |
61 *} |
60 *} |