1 (* differentiation over the reals
6 theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin
14 d_d :: "[real, real]=> real"
15 (*sin, cos :: "real => real" already in Isabelle2009-2*)
17 log, ln :: "real => real"
18 nlog :: "[real, real] => real"
19 exp :: "real => real" ("E'_ ^^^ _" 80)
21 (*descriptions in the related problems*)
22 derivativeEq :: "bool => una"
25 primed :: "'a => 'a" (*"primed A" -> "A'"*)
27 (*the CAS-commands, eg. "Diff (2*x^^^3, x)",
28 "Differentiate (A = s * (a - s), s)"*)
29 Diff :: "[real * real] => real"
30 Differentiate :: "[bool * real] => bool"
32 (*subproblem and script-name*)
33 differentiate :: "[ID * (ID list) * ID, real,real] => real"
34 ("(differentiate (_)/ (_ _ ))" 9)
35 DiffScr :: "[real,real, real] => real"
36 ("((Script DiffScr (_ _ =))// (_))" 9)
37 DiffEqScr :: "[bool,real, bool] => bool"
38 ("((Script DiffEqScr (_ _ =))// (_))" 9)
40 text {*a variant of the derivatives defintion:
42 d_d :: "(real => real) => (real => real)"
45 (1) no variable 'bdv' on the meta-level required
46 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
47 (3) and no specialized chain-rules required like
48 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
50 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
53 axiomatization where (*stated as axioms, todo: prove as theorems
54 'bdv' is a constant on the meta-level *)
55 diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" and
56 diff_var: "d_d bdv bdv = 1" and
57 diff_prod_const:"[| Not (bdv occurs_in u) |] ==>
58 d_d bdv (u * v) = u * d_d bdv v" and
60 diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" and
61 diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" and
62 diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" and
63 diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) =
64 (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)" and
66 diff_sin: "d_d bdv (sin bdv) = cos bdv" and
67 diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" and
68 diff_cos: "d_d bdv (cos bdv) = - sin bdv" and
69 diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" and
70 diff_pow: "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))" and
71 diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u" and
72 diff_ln: "d_d bdv (ln bdv) = 1 / bdv" and
73 diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" and
74 diff_exp: "d_d bdv (exp bdv) = exp bdv" and
75 diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" and
77 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
78 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
82 frac_conv: "[| bdv occurs_in b; 0 < n |] ==>
83 a / (b ^^^ n) = a * b ^^^ (-n)" and
84 frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" and
86 sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" and
87 sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" and
88 sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" and
89 sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" and
91 root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" and
92 root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" and
94 realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
99 (** eval functions **)
101 fun primed (Const (id, T)) = Const (id ^ "'", T)
102 | primed (Free (id, T)) = Free (id ^ "'", T)
103 | primed t = error ("primed called with arg = '"^ Celem.term2str t ^"'");
105 (*("primed", ("Diff.primed", eval_primed "#primed"))*)
106 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
107 SOME ((Celem.term2str p) ^ " = " ^ Celem.term2str (primed t),
108 HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
109 | eval_primed _ _ _ _ = NONE;
111 setup {* KEStore_Elems.add_calcs
112 [("primed", ("Diff.primed", eval_primed "#primed"))] *}
116 (*.converts a term such that differentiation works optimally.*)
118 Celem.Rls {id="diff_conv",
120 rew_ord = ("termlessI",termlessI),
121 erls = Celem.append_rls "erls_diff_conv" Celem.e_rls
122 [Celem.Calc ("Atools.occurs'_in", eval_occurs_in ""),
123 Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
124 Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
125 Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_"),
126 Celem.Thm ("and_true",TermC.num_str @{thm and_true}),
127 Celem.Thm ("and_false",TermC.num_str @{thm and_false})
129 srls = Celem.Erls, calc = [], errpatts = [],
131 [Celem.Thm ("frac_conv", TermC.num_str @{thm frac_conv}),
132 (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b ^^^ ?n = ?a * ?b ^^^ - ?n"*)
133 Celem.Thm ("sqrt_conv_bdv", TermC.num_str @{thm sqrt_conv_bdv}),
134 (*"sqrt ?bdv = ?bdv ^^^ (1 / 2)"*)
135 Celem.Thm ("sqrt_conv_bdv_n", TermC.num_str @{thm sqrt_conv_bdv_n}),
136 (*"sqrt (?bdv ^^^ ?n) = ?bdv ^^^ (?n / 2)"*)
137 Celem.Thm ("sqrt_conv", TermC.num_str @{thm sqrt_conv}),
138 (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u ^^^ (1 / 2)"*)
139 Celem.Thm ("root_conv", TermC.num_str @{thm root_conv}),
140 (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u ^^^ (1 / ?n)"*)
141 Celem.Thm ("realpow_pow_bdv", TermC.num_str @{thm realpow_pow_bdv}),
142 (* "(?bdv ^^^ ?b) ^^^ ?c = ?bdv ^^^ (?b * ?c)"*)
143 Celem.Calc ("Groups.times_class.times", eval_binop "#mult_"),
144 Celem.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
145 (*a / b * (c / d) = a * c / (b * d)*)
146 Celem.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
147 (*?x * (?y / ?z) = ?x * ?y / ?z*)
148 Celem.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left})
149 (*?y / ?z * ?x = ?y * ?x / ?z*)
151 scr = Celem.EmptyScr};
154 (*.beautifies a term after differentiation.*)
156 Celem.Rls {id="diff_sym_conv",
158 rew_ord = ("termlessI",termlessI),
159 erls = Celem.append_rls "erls_diff_sym_conv" Celem.e_rls
160 [Celem.Calc ("Orderings.ord_class.less",eval_equ "#less_")
162 srls = Celem.Erls, calc = [], errpatts = [],
163 rules = [Celem.Thm ("frac_sym_conv", TermC.num_str @{thm frac_sym_conv}),
164 Celem.Thm ("sqrt_sym_conv", TermC.num_str @{thm sqrt_sym_conv}),
165 Celem.Thm ("root_sym_conv", TermC.num_str @{thm root_sym_conv}),
166 Celem.Thm ("sym_real_mult_minus1",
167 TermC.num_str (@{thm real_mult_minus1} RS @{thm sym})),
169 Celem.Thm ("rat_mult",TermC.num_str @{thm rat_mult}),
170 (*a / b * (c / d) = a * c / (b * d)*)
171 Celem.Thm ("times_divide_eq_right",TermC.num_str @{thm times_divide_eq_right}),
172 (*?x * (?y / ?z) = ?x * ?y / ?z*)
173 Celem.Thm ("times_divide_eq_left",TermC.num_str @{thm times_divide_eq_left}),
174 (*?y / ?z * ?x = ?y * ?x / ?z*)
175 Celem.Calc ("Groups.times_class.times", eval_binop "#mult_")
177 scr = Celem.EmptyScr};
181 Celem.Rls {id="srls_differentiate..",
183 rew_ord = ("termlessI",termlessI),
185 srls = Celem.Erls, calc = [], errpatts = [],
186 rules = [Celem.Calc("Tools.lhs", eval_lhs "eval_lhs_"),
187 Celem.Calc("Tools.rhs", eval_rhs "eval_rhs_"),
188 Celem.Calc("Diff.primed", eval_primed "Diff.primed")
190 scr = Celem.EmptyScr};
195 Celem.append_rls "erls_differentiate.." Celem.e_rls
196 [Celem.Thm ("not_true",TermC.num_str @{thm not_true}),
197 Celem.Thm ("not_false",TermC.num_str @{thm not_false}),
199 Celem.Calc ("Atools.ident",eval_ident "#ident_"),
200 Celem.Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
201 Celem.Calc ("Atools.occurs'_in",eval_occurs_in ""),
202 Celem.Calc ("Atools.is'_const",eval_const "#is_const_")
205 (*.rules for differentiation, _no_ simplification.*)
207 Celem.Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
208 erls = erls_diff, srls = Celem.Erls, calc = [], errpatts = [],
209 rules = [Celem.Thm ("diff_sum",TermC.num_str @{thm diff_sum}),
210 Celem.Thm ("diff_dif",TermC.num_str @{thm diff_dif}),
211 Celem.Thm ("diff_prod_const",TermC.num_str @{thm diff_prod_const}),
212 Celem.Thm ("diff_prod",TermC.num_str @{thm diff_prod}),
213 Celem.Thm ("diff_quot",TermC.num_str @{thm diff_quot}),
214 Celem.Thm ("diff_sin",TermC.num_str @{thm diff_sin}),
215 Celem.Thm ("diff_sin_chain",TermC.num_str @{thm diff_sin_chain}),
216 Celem.Thm ("diff_cos",TermC.num_str @{thm diff_cos}),
217 Celem.Thm ("diff_cos_chain",TermC.num_str @{thm diff_cos_chain}),
218 Celem.Thm ("diff_pow",TermC.num_str @{thm diff_pow}),
219 Celem.Thm ("diff_pow_chain",TermC.num_str @{thm diff_pow_chain}),
220 Celem.Thm ("diff_ln",TermC.num_str @{thm diff_ln}),
221 Celem.Thm ("diff_ln_chain",TermC.num_str @{thm diff_ln_chain}),
222 Celem.Thm ("diff_exp",TermC.num_str @{thm diff_exp}),
223 Celem.Thm ("diff_exp_chain",TermC.num_str @{thm diff_exp_chain}),
225 Celem.Thm ("diff_sqrt",TermC.num_str @{thm diff_sqrt}),
226 Celem.Thm ("diff_sqrt_chain",TermC.num_str @{thm diff_sqrt_chain}),
228 Celem.Thm ("diff_const",TermC.num_str @{thm diff_const}),
229 Celem.Thm ("diff_var",TermC.num_str @{thm diff_var})
231 scr = Celem.EmptyScr};
234 (*.normalisation for checking user-input.*)
237 {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI),
238 erls = Celem.Erls, srls = Celem.Erls, calc = [], errpatts = [],
239 rules = [Celem.Rls_ diff_rules, Celem.Rls_ norm_Poly ],
240 scr = Celem.EmptyScr};
242 setup {* KEStore_Elems.add_rlss
243 [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)),
244 ("diff_rules", (Context.theory_name @{theory}, prep_rls' diff_rules)),
245 ("norm_diff", (Context.theory_name @{theory}, prep_rls' norm_diff)),
246 ("diff_conv", (Context.theory_name @{theory}, prep_rls' diff_conv)),
247 ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls' diff_sym_conv))] *}
249 (** problem types **)
250 setup {* KEStore_Elems.add_pbts
251 [(Specify.prep_pbt thy "pbl_fun" [] Celem.e_pblID (["function"], [], Celem.e_rls, NONE, [])),
252 (Specify.prep_pbt thy "pbl_fun_deriv" [] Celem.e_pblID
253 (["derivative_of","function"],
254 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
255 ("#Find" ,["derivative f_f'"])],
256 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [],
257 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
258 ["diff","after_simplification"]])),
259 (*here "named" is used differently from Integration"*)
260 (Specify.prep_pbt thy "pbl_fun_deriv_nam" [] Celem.e_pblID
261 (["named","derivative_of","function"],
262 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
263 ("#Find" ,["derivativeEq f_f'"])],
264 Celem.append_rls "xxxe_rlsxxx" Celem.e_rls [],
265 SOME "Differentiate (f_f, v_v)",
266 [["diff","differentiate_equality"]]))] *}
271 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
272 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
273 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
275 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
276 [((Thm.term_of o the o (TermC.parse thy)) "functionTerm", [t]),
277 ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),
278 ((Thm.term_of o the o (TermC.parse thy)) "derivative",
279 [(Thm.term_of o the o (TermC.parse thy)) "f_f'"])
281 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
283 setup {* KEStore_Elems.add_mets
284 [Specify.prep_met thy "met_diff" [] Celem.e_metID
286 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
287 crls = Atools_erls, errpats = [], nrls = norm_diff},
289 Specify.prep_met thy "met_diff_onR" [] Celem.e_metID
290 (["diff","differentiate_on_R"],
291 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
292 ("#Find" ,["derivative f_f'"])],
293 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
294 crls = Atools_erls, errpats = [], nrls = norm_diff},
295 "Script DiffScr (f_f::real) (v_v::real) = " ^
296 " (let f_f' = Take (d_d v_v f_f) " ^
297 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
299 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
300 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
301 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
302 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
303 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
304 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
305 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
306 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
307 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
308 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
309 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
310 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
311 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
312 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
313 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
314 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
315 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
316 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
317 Specify.prep_met thy "met_diff_simpl" [] Celem.e_metID
318 (["diff","diff_simpl"],
319 [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
320 ("#Find" , ["derivative f_f'"])],
321 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
322 crls = Atools_erls, errpats = [], nrls = norm_diff},
323 "Script DiffScr (f_f::real) (v_v::real) = " ^
324 " (let f_f' = Take (d_d v_v f_f) " ^
327 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
328 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
329 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
330 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot False)) Or " ^
331 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
332 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
333 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
334 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
335 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
336 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
337 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
338 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
339 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
340 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
341 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
342 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
343 " (Repeat (Rewrite_Set make_polynomial False)))) " ^
345 Specify.prep_met thy "met_diff_equ" [] Celem.e_metID
346 (["diff","differentiate_equality"],
347 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
348 ("#Find" ,["derivativeEq f_f'"])],
349 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Celem.e_rls,
350 crls=Atools_erls, errpats = [], nrls = norm_diff},
351 "Script DiffEqScr (f_f::bool) (v_v::real) = " ^
352 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^
353 " in (((Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
355 " ((Repeat (Rewrite_Inst [(bdv,v_v)] diff_sum False)) Or " ^
356 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_dif False)) Or " ^
357 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod_const False)) Or " ^
358 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_prod False)) Or " ^
359 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_quot True )) Or " ^
360 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin False)) Or " ^
361 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_sin_chain False)) Or " ^
362 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos False)) Or " ^
363 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_cos_chain False)) Or " ^
364 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow False)) Or " ^
365 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_pow_chain False)) Or " ^
366 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln False)) Or " ^
367 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_ln_chain False)) Or " ^
368 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp False)) Or " ^
369 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_exp_chain False)) Or " ^
370 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_const False)) Or " ^
371 " (Repeat (Rewrite_Inst [(bdv,v_v)] diff_var False)) Or " ^
372 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
373 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)))) f_f')"),
374 Specify.prep_met thy "met_diff_after_simp" [] Celem.e_metID
375 (["diff","after_simplification"],
376 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
377 ("#Find" ,["derivative f_f'"])],
378 {rew_ord'="tless_true", rls' = Celem.e_rls, calc = [], srls = Celem.e_rls, prls=Celem.e_rls,
379 crls=Atools_erls, errpats = [], nrls = norm_Rational},
380 "Script DiffScr (f_f::real) (v_v::real) = " ^
381 " (let f_f' = Take (d_d v_v f_f) " ^
382 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
383 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_conv False)) @@ " ^
384 " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^
385 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^
386 " (Try (Rewrite_Set norm_Rational False))) f_f')")]
388 setup {* KEStore_Elems.add_cas
389 [((Thm.term_of o the o (TermC.parse thy)) "Diff",
390 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))] *}
393 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
394 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
395 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
397 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
398 [((Thm.term_of o the o (TermC.parse thy)) "functionEq", [t]),
399 ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),
400 ((Thm.term_of o the o (TermC.parse thy)) "derivativeEq",
401 [(Thm.term_of o the o (TermC.parse thy)) "f_f'::bool"])
403 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss";
405 setup {* KEStore_Elems.add_cas
406 [((Thm.term_of o the o (TermC.parse thy)) "Differentiate",
407 (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))] *}