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)"
90 (** eval functions **)
92 fun primed (Const (id, T)) = Const (id ^ "'", T)
93 | primed (Free (id, T)) = Free (id ^ "'", T)
94 | primed t = raise ERROR ("primed called with arg = '"^ UnparseC.term t ^"'");
96 (*("primed", ("Diff.primed", eval_primed "#primed"))*)
97 fun eval_primed _ _ (p as (Const (\<^const_name>\<open>Diff.primed\<close>,_) $ t)) _ =
98 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (primed t),
99 HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
100 | eval_primed _ _ _ _ = NONE;
103 calculation primed = \<open>eval_primed "#primed"\<close>
108 (*.converts a term such that differentiation works optimally.*)
110 Rule_Def.Repeat {id="diff_conv", preconds = [], rew_ord = ("termlessI",termlessI),
111 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty [
112 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
113 \<^rule_thm>\<open>not_true\<close>,
114 \<^rule_thm>\<open>not_false\<close>,
115 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
116 \<^rule_thm>\<open>and_true\<close>,
117 \<^rule_thm>\<open>and_false\<close>],
118 srls = Rule_Set.Empty, calc = [], errpatts = [],
120 \<^rule_thm>\<open>frac_conv\<close>, (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b \<up> ?n = ?a * ?b \<up> - ?n"*)
121 \<^rule_thm>\<open>sqrt_conv_bdv\<close>, (*"sqrt ?bdv = ?bdv \<up> (1 / 2)"*)
122 \<^rule_thm>\<open>sqrt_conv_bdv_n\<close>, (*"sqrt (?bdv \<up> ?n) = ?bdv \<up> (?n / 2)"*)
123 \<^rule_thm>\<open>sqrt_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u \<up> (1 / 2)"*)
124 \<^rule_thm>\<open>root_conv\<close>, (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u \<up> (1 / ?n)"*)
125 \<^rule_thm>\<open>realpow_pow_bdv\<close>, (* "(?bdv \<up> ?b) \<up> ?c = ?bdv \<up> (?b * ?c)"*)
126 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_"),
127 \<^rule_thm>\<open>rat_mult\<close>, (*a / b * (c / d) = a * c / (b * d)*)
128 \<^rule_thm>\<open>times_divide_eq_right\<close>, (*?x * (?y / ?z) = ?x * ?y / ?z*)
129 \<^rule_thm>\<open>times_divide_eq_left\<close>], (*?y / ?z * ?x = ?y * ?x / ?z*)
130 scr = Rule.Empty_Prog};
133 (*.beautifies a term after differentiation.*)
135 Rule_Def.Repeat {id="diff_sym_conv", preconds = [], rew_ord = ("termlessI",termlessI),
136 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty [
137 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
138 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
139 \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
140 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
141 \<^rule_eval>\<open>less\<close> (Prog_Expr.eval_equ "#less_"),
142 \<^rule_thm>\<open>not_false\<close>,
143 \<^rule_thm>\<open>not_true\<close>],
144 srls = Rule_Set.Empty, calc = [], errpatts = [],
146 \<^rule_thm>\<open>frac_sym_conv\<close>,
147 \<^rule_thm>\<open>sqrt_sym_conv\<close>,
148 \<^rule_thm>\<open>root_sym_conv\<close>,
149 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_atom) ==> - (z::real) = -1 * z"*),
150 \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?a) = ?a"*),
151 \<^rule_thm>\<open>rat_mult\<close> (*a / b * (c / d) = a * c / (b * d)*),
152 \<^rule_thm>\<open>times_divide_eq_right\<close> (*?x * (?y / ?z) = ?x * ?y / ?z*),
153 \<^rule_thm>\<open>times_divide_eq_left\<close> (*?y / ?z * ?x = ?y * ?x / ?z*),
154 \<^rule_eval>\<open>times\<close> (**)(Calc_Binop.numeric "#mult_")],
155 scr = Rule.Empty_Prog};
159 Rule_Def.Repeat {id="srls_differentiate..", preconds = [], rew_ord = ("termlessI",termlessI),
160 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
162 \<^rule_eval>\<open>Prog_Expr.lhs\<close> (Prog_Expr.eval_lhs "eval_lhs_"),
163 \<^rule_eval>\<open>Prog_Expr.rhs\<close> (Prog_Expr.eval_rhs "eval_rhs_"),
164 \<^rule_eval>\<open>Diff.primed\<close> (eval_primed "Diff.primed")],
165 scr = Rule.Empty_Prog};
170 Rule_Set.append_rules "erls_differentiate.." Rule_Set.empty [
171 \<^rule_thm>\<open>not_true\<close>,
172 \<^rule_thm>\<open>not_false\<close>,
174 \<^rule_eval>\<open>Prog_Expr.ident\<close> (Prog_Expr.eval_ident "#ident_"),
175 \<^rule_eval>\<open>Prog_Expr.is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
176 \<^rule_eval>\<open>Prog_Expr.occurs_in\<close> (Prog_Expr.eval_occurs_in ""),
177 \<^rule_eval>\<open>Prog_Expr.is_num\<close> (Prog_Expr.eval_is_num "#is_num_")];
179 (*.rules for differentiation, _no_ simplification.*)
181 Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
182 erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],
184 \<^rule_thm>\<open>diff_sum\<close>,
185 \<^rule_thm>\<open>diff_dif\<close>,
186 \<^rule_thm>\<open>diff_prod_const\<close>,
187 \<^rule_thm>\<open>diff_prod\<close>,
188 \<^rule_thm>\<open>diff_quot\<close>,
189 \<^rule_thm>\<open>diff_sin\<close>,
190 \<^rule_thm>\<open>diff_sin_chain\<close>,
191 \<^rule_thm>\<open>diff_cos\<close>,
192 \<^rule_thm>\<open>diff_cos_chain\<close>,
193 \<^rule_thm>\<open>diff_pow\<close>,
194 \<^rule_thm>\<open>diff_pow_chain\<close>,
195 \<^rule_thm>\<open>diff_ln\<close>,
196 \<^rule_thm>\<open>diff_ln_chain\<close>,
197 \<^rule_thm>\<open>diff_exp\<close>,
198 \<^rule_thm>\<open>diff_exp_chain\<close>,
200 \<^rule_thm>\<open>diff_sqrt\<close>,
201 \<^rule_thm>\<open>diff_sqrt_chain\<close>,
203 \<^rule_thm>\<open>diff_const\<close>,
204 \<^rule_thm>\<open>diff_var\<close>],
205 scr = Rule.Empty_Prog};
208 (*.normalisation for checking user-input.*)
211 {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI),
212 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
213 rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
214 scr = Rule.Empty_Prog};
217 erls_diff = \<open>prep_rls' erls_diff\<close> and
218 diff_rules = \<open>prep_rls' diff_rules\<close> and
219 norm_diff = \<open>prep_rls' norm_diff\<close> and
220 diff_conv = \<open>prep_rls' diff_conv\<close> and
221 diff_sym_conv = \<open>prep_rls' diff_sym_conv\<close>
226 problem pbl_fun : "function" = \<open>Rule_Set.empty\<close>
228 problem pbl_fun_deriv : "derivative_of/function" =
229 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
230 Method_Ref: "diff/differentiate_on_R" "diff/after_simplification"
231 CAS: "Diff (f_f, v_v)"
232 Given: "functionTerm f_f" "differentiateFor v_v"
233 Find: "derivative f_f'"
235 problem pbl_fun_deriv_nam :
236 "named/derivative_of/function" (*here "named" is used differently from Integration"*) =
237 \<open>Rule_Set.append_rules "empty" Rule_Set.empty []\<close>
238 Method_Ref: "diff/differentiate_equality"
239 CAS: "Differentiate (f_f, v_v)"
240 Given: "functionEq f_f" "differentiateFor v_v"
241 Find: "derivativeEq f_f'"
246 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
247 (* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Diff (a * x^3 + b, x)");
248 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
250 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
251 [((TermC.parseNEW''\<^theory>) "functionTerm", [t]),
252 ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]),
253 ((TermC.parseNEW''\<^theory>) "derivative",
254 [(TermC.parseNEW''\<^theory>) "f_f'"])
256 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
259 method met_diff : "diff" =
260 \<open>{rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
261 crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
263 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
265 "differentiate_on_R f_f v_v = (
267 f_f' = Take (d_d v_v f_f)
269 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) #> (
271 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
272 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'')) Or
273 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
274 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
275 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
276 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
277 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
278 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
279 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
280 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
281 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
282 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
283 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
284 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
285 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
286 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
287 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
288 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
291 method met_diff_onR : "diff/differentiate_on_R" =
292 \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
293 crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
294 Program: differentiate_on_R.simps
295 Given: "functionTerm f_f" "differentiateFor v_v"
296 Find: "derivative f_f'"
298 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
300 "differentiateX f_f v_v = (
302 f_f' = Take (d_d v_v f_f)
305 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
306 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' )) Or
307 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
308 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
309 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
310 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
311 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
312 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
313 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
314 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
315 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
316 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
317 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
318 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
319 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
320 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
321 (Repeat (Rewrite_Set ''make_polynomial'')))
324 method met_diff_simpl : "diff/diff_simpl" =
325 \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
326 crls = Atools_erls, errpats = [], nrls = norm_diff}\<close>
327 Program: differentiateX.simps
328 Given: "functionTerm f_f" " differentiateFor v_v"
329 Find: "derivative f_f'"
331 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
333 "differentiate_equality f_f v_v = (
335 f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
337 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) #> (
339 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'')) Or
340 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' )) Or
341 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'')) Or
342 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'')) Or
343 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'')) Or
344 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'')) Or
345 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'')) Or
346 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'')) Or
347 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'')) Or
348 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'')) Or
349 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'')) Or
350 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'')) Or
351 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'')) Or
352 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'')) Or
353 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'')) Or
354 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'')) Or
355 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'')) Or
356 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
357 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
360 method met_diff_equ : "diff/differentiate_equality" =
361 \<open>{rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule_Set.empty,
362 crls=Atools_erls, errpats = [], nrls = norm_diff}\<close>
363 Program: differentiate_equality.simps
364 Given: "functionEq f_f" "differentiateFor v_v"
365 Find: "derivativeEq f_f'"
367 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
369 "simplify_derivative term bound_variable = (
371 term' = Take (d_d bound_variable term)
373 (Try (Rewrite_Set ''norm_Rational'')) #>
374 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) #>
375 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) #>
376 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) #>
377 (Try (Rewrite_Set ''norm_Rational''))
380 method met_diff_after_simp : "diff/after_simplification" =
381 \<open>{rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
382 crls=Atools_erls, errpats = [], nrls = norm_Rational}\<close>
383 Program: simplify_derivative.simps
384 Given: "functionTerm term" "differentiateFor bound_variable"
385 Find: "derivative term'"
387 cas Diff = \<open>argl2dtss\<close>
388 Problem_Ref: "derivative_of/function"
392 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
393 (* val (t, pairl) = strip_comb (TermC.parse_test @{context} "Differentiate (A = s * (a - s), s)");
394 val [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] = pairl;
396 fun argl2dtss [Const (\<^const_name>\<open>Pair\<close>, _) $ t $ bdv] =
397 [((TermC.parseNEW''\<^theory>) "functionEq", [t]),
398 ((TermC.parseNEW''\<^theory>) "differentiateFor", [bdv]),
399 ((TermC.parseNEW''\<^theory>) "derivativeEq",
400 [(TermC.parseNEW''\<^theory>) "f_f'::bool"])
402 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
404 cas Differentiate = \<open>argl2dtss\<close>
405 Problem_Ref: "named/derivative_of/function"