271 (*.handle cas-input like "Diff (a * x^3 + b, x)".*) |
271 (*.handle cas-input like "Diff (a * x^3 + b, x)".*) |
272 (* val (t, pairl) = strip_comb (str2term "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; |
273 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl; |
274 *) |
274 *) |
275 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] = |
275 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] = |
276 [((term_of o the o (parse thy)) "functionTerm", [t]), |
276 [((Thm.term_of o the o (parse thy)) "functionTerm", [t]), |
277 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
277 ((Thm.term_of o the o (parse thy)) "differentiateFor", [bdv]), |
278 ((term_of o the o (parse thy)) "derivative", |
278 ((Thm.term_of o the o (parse thy)) "derivative", |
279 [(term_of o the o (parse thy)) "f_f'"]) |
279 [(Thm.term_of o the o (parse thy)) "f_f'"]) |
280 ] |
280 ] |
281 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; |
281 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; |
282 *} |
282 *} |
283 setup {* KEStore_Elems.add_mets |
283 setup {* KEStore_Elems.add_mets |
284 [prep_met thy "met_diff" [] e_metID |
284 [prep_met thy "met_diff" [] e_metID |
384 " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^ |
384 " (Try (Rewrite_Set_Inst [(bdv,v_v)] norm_diff False)) @@ " ^ |
385 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^ |
385 " (Try (Rewrite_Set_Inst [(bdv,v_v)] diff_sym_conv False)) @@ " ^ |
386 " (Try (Rewrite_Set norm_Rational False))) f_f')")] |
386 " (Try (Rewrite_Set norm_Rational False))) f_f')")] |
387 *} |
387 *} |
388 setup {* KEStore_Elems.add_cas |
388 setup {* KEStore_Elems.add_cas |
389 [((term_of o the o (parse thy)) "Diff", |
389 [((Thm.term_of o the o (parse thy)) "Diff", |
390 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))] *} |
390 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))] *} |
391 ML {* |
391 ML {* |
392 |
392 |
393 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) |
393 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*) |
394 (* val (t, pairl) = strip_comb (str2term "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; |
395 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl; |
396 *) |
396 *) |
397 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] = |
397 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] = |
398 [((term_of o the o (parse thy)) "functionEq", [t]), |
398 [((Thm.term_of o the o (parse thy)) "functionEq", [t]), |
399 ((term_of o the o (parse thy)) "differentiateFor", [bdv]), |
399 ((Thm.term_of o the o (parse thy)) "differentiateFor", [bdv]), |
400 ((term_of o the o (parse thy)) "derivativeEq", |
400 ((Thm.term_of o the o (parse thy)) "derivativeEq", |
401 [(term_of o the o (parse thy)) "f_f'::bool"]) |
401 [(Thm.term_of o the o (parse thy)) "f_f'::bool"]) |
402 ] |
402 ] |
403 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; |
403 | argl2dtss _ = error "Diff.ML: wrong argument for argl2dtss"; |
404 *} |
404 *} |
405 setup {* KEStore_Elems.add_cas |
405 setup {* KEStore_Elems.add_cas |
406 [((term_of o the o (parse thy)) "Differentiate", |
406 [((Thm.term_of o the o (parse thy)) "Differentiate", |
407 (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))] *} |
407 (("Isac", ["named","derivative_of","function"], ["no_met"]), argl2dtss))] *} |
408 |
408 |
409 end |
409 end |