1 (* differentiation over the reals
6 theory Diff imports Calculus Trig LogExp Rational Root Poly Base_Tools begin
14 d_d :: "[real, real]=> real"
16 (*descriptions in the related problems*)
17 derivativeEq :: "bool => una"
20 primed :: "'a => 'a" (*"primed A" -> "A'"*)
22 (*the CAS-commands, eg. "Diff (2*x \<up> 3, x)",
23 "Differentiate (A = s * (a - s), s)"*)
24 Diff :: "[real * real] => real"
25 Differentiate :: "[bool * real] => bool"
28 differentiate :: "[char list * char list list * char list, real, real] => real"
29 ("(differentiate (_)/ (_ _ ))" 9)
31 text \<open>a variant of the derivatives defintion:
33 d_d :: "(real => real) => (real => real)"
36 (1) no variable 'bdv' on the meta-level required
37 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
38 (3) and no specialized chain-rules required like
39 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
41 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
44 axiomatization where (*stated as axioms, todo: prove as theorems
45 'bdv' is a constant on the meta-level *)
46 diff_const: "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0" and
47 diff_var: "d_d bdv bdv = 1" and
48 diff_prod_const:"[| Not (bdv occurs_in u) |] ==>
49 d_d bdv (u * v) = u * d_d bdv v" and
51 diff_sum: "d_d bdv (u + v) = d_d bdv u + d_d bdv v" and
52 diff_dif: "d_d bdv (u - v) = d_d bdv u - d_d bdv v" and
53 diff_prod: "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v" and
54 diff_quot: "Not (v = 0) ==> (d_d bdv (u / v) =
55 (d_d bdv u * v - u * d_d bdv v) / v \<up> 2)" and
57 diff_sin: "d_d bdv (sin bdv) = cos bdv" and
58 diff_sin_chain: "d_d bdv (sin u) = cos u * d_d bdv u" and
59 diff_cos: "d_d bdv (cos bdv) = - sin bdv" and
60 diff_cos_chain: "d_d bdv (cos u) = - sin u * d_d bdv u" and
61 diff_pow: "d_d bdv (bdv \<up> n) = n * (bdv \<up> (n - 1))" and
62 diff_pow_chain: "d_d bdv (u \<up> n) = n * (u \<up> (n - 1)) * d_d bdv u" and
63 diff_ln: "d_d bdv (ln bdv) = 1 / bdv" and
64 diff_ln_chain: "d_d bdv (ln u) = d_d bdv u / u" and
65 diff_exp: "d_d bdv (exp bdv) = exp bdv" and
66 diff_exp_chain: "d_d bdv (exp u) = exp u * d_d x u" and
68 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
69 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
73 frac_conv: "[| bdv occurs_in b; 0 < n |] ==>
74 a / (b \<up> n) = a * b \<up> (-n)" and
75 frac_sym_conv: "n < 0 ==> a * b \<up> n = a / b \<up> (-n)" and
77 sqrt_conv_bdv: "sqrt bdv = bdv \<up> (1 / 2)" and
78 sqrt_conv_bdv_n: "sqrt (bdv \<up> n) = bdv \<up> (n / 2)" and
79 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------\\*)
80 sqrt_conv: "bdv occurs_in u ==> sqrt u = u \<up> (1 / 2)" and
81 (*Ambiguous input\<^here> produces 3 parse trees -----------------------------//*)
82 sqrt_sym_conv: "u \<up> (a / 2) = sqrt (u \<up> a)" and
84 root_conv: "bdv occurs_in u ==> nroot n u = u \<up> (1 / n)" and
85 root_sym_conv: "u \<up> (a / b) = nroot b (u \<up> a)" and
87 realpow_pow_bdv: "(bdv \<up> b) \<up> c = bdv \<up> (b * c)"
92 (** eval functions **)
94 fun primed (Const (id, T)) = Const (id ^ "'", T)
95 | primed (Free (id, T)) = Free (id ^ "'", T)
96 | primed t = raise ERROR ("primed called with arg = '"^ UnparseC.term t ^"'");
98 (*("primed", ("Diff.primed", eval_primed "#primed"))*)
99 fun eval_primed _ _ (p as (Const (\<^const_name>\<open>Diff.primed\<close>,_) $ t)) _ =
100 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (primed t),
101 HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
102 | eval_primed _ _ _ _ = NONE;
105 calculation primed = \<open>eval_primed "#primed"\<close>
110 (*.converts a term such that differentiation works optimally.*)
112 Rule_Def.Repeat {id="diff_conv",
114 rew_ord = ("termlessI",termlessI),
115 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty
116 [\<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
117 \<^rule_thm>\<open>not_true\<close>,
118 \<^rule_thm>\<open>not_false\<close>,
119 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
120 \<^rule_thm>\<open>and_true\<close>,
121 \<^rule_thm>\<open>and_false\<close>
123 srls = Rule_Set.Empty, calc = [], errpatts = [],
125 [\<^rule_thm>\<open>frac_conv\<close>,
126 (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"*)
127 \<^rule_thm>\<open>sqrt_conv_bdv\<close>,
128 (*"sqrt ?bdv = ?bdv \<up> (1 / 2)"*)
129 \<^rule_thm>\<open>sqrt_conv_bdv_n\<close>,
130 (*"sqrt (?bdv \<up> ?n) = ?bdv \<up> (?n / 2)"*)
131 \<^rule_thm>\<open>sqrt_conv\<close>,
132 (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)
133 \<^rule_thm>\<open>root_conv\<close>,
134 (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)
135 \<^rule_thm>\<open>realpow_pow_bdv\<close>,
136 (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)
137 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_"),
138 \<^rule_thm>\<open>rat_mult\<close>,
139 (*a / b * (c / d) = a * c / (b * d)*)
140 \<^rule_thm>\<open>times_divide_eq_right\<close>,
141 (*?x * (?y / ?z) = ?x * ?y / ?z*)
142 \<^rule_thm>\<open>times_divide_eq_left\<close>
143 (*?y / ?z * ?x = ?y * ?x / ?z*)
145 scr = Rule.Empty_Prog};
148 (*.beautifies a term after differentiation.*)
150 Rule_Def.Repeat {id="diff_sym_conv",
152 rew_ord = ("termlessI",termlessI),
153 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty
154 [\<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
156 Rule.Eval ("Prog_Expr.matches", Prog_Expr.eval_matches "#matches_"),
157 Rule.Eval ("Prog_Expr.is_atom", Prog_Expr.eval_is_atom "#is_atom_"),
158 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
159 Rule.Thm ("not_false", @{thm not_false}),
160 Rule.Thm ("not_true", @{thm not_true})],
161 srls = Rule_Set.Empty, calc = [], errpatts = [],
162 rules = [\<^rule_thm>\<open>frac_sym_conv\<close>,
163 \<^rule_thm>\<open>sqrt_sym_conv\<close>,
164 \<^rule_thm>\<open>root_sym_conv\<close>,
165 \<^rule_thm_sym>\<open>real_mult_minus1\<close>,
167 \<^rule_thm>\<open>rat_mult\<close>,
168 (*a / b * (c / d) = a * c / (b * d)*)
169 \<^rule_thm>\<open>times_divide_eq_right\<close>,
170 (*?x * (?y / ?z) = ?x * ?y / ?z*)
171 \<^rule_thm>\<open>times_divide_eq_left\<close>,
172 (*?y / ?z * ?x = ?y * ?x / ?z*)
173 \<^rule_eval>\<open>times\<close> (**)(eval_binop "#mult_")
175 scr = Rule.Empty_Prog};
179 Rule_Def.Repeat {id="srls_differentiate..",
181 rew_ord = ("termlessI",termlessI),
182 erls = Rule_Set.empty,
183 srls = Rule_Set.Empty, calc = [], errpatts = [],
184 rules = [\<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
185 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_"),
186 \<^rule_eval>\<open>Diff.primed\<close> (eval_primed "Diff.primed")
188 scr = Rule.Empty_Prog};
193 Rule_Set.append_rules "erls_differentiate.." Rule_Set.empty
194 [\<^rule_thm>\<open>not_true\<close>,
195 \<^rule_thm>\<open>not_false\<close>,
197 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
198 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
199 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
200 \<^rule_eval>\<open>Prog_Expr.is_const\<close> (Prog_Expr.eval_const "#is_const_")
203 (*.rules for differentiation, _no_ simplification.*)
205 Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
206 erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],
207 rules = [\<^rule_thm>\<open>diff_sum\<close>,
208 \<^rule_thm>\<open>diff_dif\<close>,
209 \<^rule_thm>\<open>diff_prod_const\<close>,
210 \<^rule_thm>\<open>diff_prod\<close>,
211 \<^rule_thm>\<open>diff_quot\<close>,
212 \<^rule_thm>\<open>diff_sin\<close>,
213 \<^rule_thm>\<open>diff_sin_chain\<close>,
214 \<^rule_thm>\<open>diff_cos\<close>,
215 \<^rule_thm>\<open>diff_cos_chain\<close>,
216 \<^rule_thm>\<open>diff_pow\<close>,
217 \<^rule_thm>\<open>diff_pow_chain\<close>,
218 \<^rule_thm>\<open>diff_ln\<close>,
219 \<^rule_thm>\<open>diff_ln_chain\<close>,
220 \<^rule_thm>\<open>diff_exp\<close>,
221 \<^rule_thm>\<open>diff_exp_chain\<close>,
223 \<^rule_thm>\<open>diff_sqrt\<close>,
224 \<^rule_thm>\<open>diff_sqrt_chain\<close>,
226 \<^rule_thm>\<open>diff_const\<close>,
227 \<^rule_thm>\<open>diff_var\<close>
229 scr = Rule.Empty_Prog};
232 (*.normalisation for checking user-input.*)
235 {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI),
236 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
237 rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
238 scr = Rule.Empty_Prog};
241 erls_diff = \<open>prep_rls' erls_diff\<close> and
242 diff_rules = \<open>prep_rls' diff_rules\<close> and
243 norm_diff = \<open>prep_rls' norm_diff\<close> and
244 diff_conv = \<open>prep_rls' diff_conv\<close> and
245 diff_sym_conv = \<open>prep_rls' diff_sym_conv\<close>
250 problem pbl_fun : "function" = \<open>Rule_Set.empty\<close>
252 problem pbl_fun_deriv : "derivative_of/function" =
253 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
254 Method: "diff/differentiate_on_R" "diff/after_simplification"
255 CAS: "Diff (f_f, v_v)"
256 Given: "functionTerm f_f" "differentiateFor v_v"
257 Find: "derivative f_f'"
259 problem pbl_fun_deriv_nam :
260 "named/derivative_of/function" (*here "named" is used differently from Integration"*) =
261 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
262 Method: "diff/differentiate_equality"
263 CAS: "Differentiate (f_f, v_v)"
264 Given: "functionEq f_f" "differentiateFor v_v"
265 Find: "derivativeEq f_f'"
270 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
271 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
272 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
274 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
275 [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionTerm", [t]),
276 ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
277 ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivative",
278 [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'"])
280 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
283 method met_diff : "diff" =
284 \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
285 crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
287 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
289 "differentiate_on_R f_f v_v = (
291 f_f' = Take (d_d v_v f_f)
293 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) #> (
295 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
296 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'')) Or
297 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
298 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
299 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
300 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
301 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
302 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
303 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
304 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
305 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
306 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
307 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
308 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
309 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
310 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
311 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
312 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
315 method met_diff_onR : "diff/differentiate_on_R" =
316 \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
317 crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
318 Program: differentiate_on_R.simps
319 Given: "functionTerm f_f" "differentiateFor v_v"
320 Find: "derivative f_f'"
322 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
324 "differentiateX f_f v_v = (
326 f_f' = Take (d_d v_v f_f)
329 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
330 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' )) Or
331 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
332 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
333 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
334 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
335 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
336 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
337 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
338 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
339 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
340 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
341 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
342 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
343 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
344 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
345 (Repeat (Rewrite_Set ''make_polynomial'')))
348 method met_diff_simpl : "diff/diff_simpl" =
349 \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
350 crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
351 Program: differentiateX.simps
352 Given: "functionTerm f_f" " differentiateFor v_v"
353 Find: "derivative f_f'"
355 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
357 "differentiate_equality f_f v_v = (
359 f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
361 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) #> (
363 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'')) Or
364 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' )) Or
365 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'')) Or
366 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'')) Or
367 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'')) Or
368 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'')) Or
369 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'')) Or
370 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'')) Or
371 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'')) Or
372 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'')) Or
373 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'')) Or
374 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'')) Or
375 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'')) Or
376 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'')) Or
377 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'')) Or
378 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'')) Or
379 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'')) Or
380 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
381 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
384 method met_diff_equ : "diff/differentiate_equality" =
385 \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule_Set.empty,
386 crls=Atools_erls, errpats = [], nrls = norm_diff}\<close>
387 Program: differentiate_equality.simps
388 Given: "functionEq f_f" "differentiateFor v_v"
389 Find: "derivativeEq f_f'"
391 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
393 "simplify_derivative term bound_variable = (
395 term' = Take (d_d bound_variable term)
397 (Try (Rewrite_Set ''norm_Rational'')) #>
398 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) #>
399 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) #>
400 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) #>
401 (Try (Rewrite_Set ''norm_Rational''))
404 method met_diff_after_simp : "diff/after_simplification" =
405 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
406 crls=Atools_erls, errpats = [], nrls = norm_Rational}\<close>
407 Program: simplify_derivative.simps
408 Given: "functionTerm term" "differentiateFor bound_variable"
409 Find: "derivative term'"
411 cas Diff = \<open>argl2dtss\<close>
412 Problem: "derivative_of/function"
416 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
417 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
418 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
420 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
421 [((Thm.term_of o the o (TermC.parse \<^theory>)) "functionEq", [t]),
422 ((Thm.term_of o the o (TermC.parse \<^theory>)) "differentiateFor", [bdv]),
423 ((Thm.term_of o the o (TermC.parse \<^theory>)) "derivativeEq",
424 [(Thm.term_of o the o (TermC.parse \<^theory>)) "f_f'::bool"])
426 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
428 cas Differentiate = \<open>argl2dtss\<close>
429 Problem: "named/derivative_of/function"