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^^^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 ^^^ 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 ^^^ n) = n * (bdv ^^^ (n - 1))" and
62 diff_pow_chain: "d_d bdv (u ^^^ n) = n * (u ^^^ (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 ^^^ n) = a * b ^^^ (-n)" and
75 frac_sym_conv: "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)" and
77 sqrt_conv_bdv: "sqrt bdv = bdv ^^^ (1 / 2)" and
78 sqrt_conv_bdv_n: "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)" and
79 sqrt_conv: "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)" and
80 sqrt_sym_conv: "u ^^^ (a / 2) = sqrt (u ^^^ a)" and
82 root_conv: "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)" and
83 root_sym_conv: "u ^^^ (a / b) = nroot b (u ^^^ a)" and
85 realpow_pow_bdv: "(bdv ^^^ b) ^^^ c = bdv ^^^ (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 ("Diff.primed",_) $ t)) _ =
98 SOME ((UnparseC.term p) ^ " = " ^ UnparseC.term (primed t),
99 HOLogic.Trueprop $ (TermC.mk_equality (p, primed t)))
100 | eval_primed _ _ _ _ = NONE;
102 setup \<open>KEStore_Elems.add_calcs
103 [("primed", ("Diff.primed", eval_primed "#primed"))]\<close>
107 (*.converts a term such that differentiation works optimally.*)
109 Rule_Def.Repeat {id="diff_conv",
111 rew_ord = ("termlessI",termlessI),
112 erls = Rule_Set.append_rules "erls_diff_conv" Rule_Set.empty
113 [Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
114 Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
115 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
116 Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_"),
117 Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
118 Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false})
120 srls = Rule_Set.Empty, calc = [], errpatts = [],
122 [Rule.Thm ("frac_conv", ThmC.numerals_to_Free @{thm frac_conv}),
123 (*"?bdv occurs_in ?b \<Longrightarrow> 0 < ?n \<Longrightarrow> ?a / ?b ^^^ ?n = ?a * ?b ^^^ - ?n"*)
124 Rule.Thm ("sqrt_conv_bdv", ThmC.numerals_to_Free @{thm sqrt_conv_bdv}),
125 (*"sqrt ?bdv = ?bdv ^^^ (1 / 2)"*)
126 Rule.Thm ("sqrt_conv_bdv_n", ThmC.numerals_to_Free @{thm sqrt_conv_bdv_n}),
127 (*"sqrt (?bdv ^^^ ?n) = ?bdv ^^^ (?n / 2)"*)
128 Rule.Thm ("sqrt_conv", ThmC.numerals_to_Free @{thm sqrt_conv}),
129 (*"?bdv occurs_in ?u \<Longrightarrow> sqrt ?u = ?u ^^^ (1 / 2)"*)
130 Rule.Thm ("root_conv", ThmC.numerals_to_Free @{thm root_conv}),
131 (*"?bdv occurs_in ?u \<Longrightarrow> nroot ?n ?u = ?u ^^^ (1 / ?n)"*)
132 Rule.Thm ("realpow_pow_bdv", ThmC.numerals_to_Free @{thm realpow_pow_bdv}),
133 (* "(?bdv ^^^ ?b) ^^^ ?c = ?bdv ^^^ (?b * ?c)"*)
134 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
135 Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
136 (*a / b * (c / d) = a * c / (b * d)*)
137 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
138 (*?x * (?y / ?z) = ?x * ?y / ?z*)
139 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left})
140 (*?y / ?z * ?x = ?y * ?x / ?z*)
142 scr = Rule.Empty_Prog};
145 (*.beautifies a term after differentiation.*)
147 Rule_Def.Repeat {id="diff_sym_conv",
149 rew_ord = ("termlessI",termlessI),
150 erls = Rule_Set.append_rules "erls_diff_sym_conv" Rule_Set.empty
151 [Rule.Eval ("Orderings.ord_class.less", Prog_Expr.eval_equ "#less_")
153 srls = Rule_Set.Empty, calc = [], errpatts = [],
154 rules = [Rule.Thm ("frac_sym_conv", ThmC.numerals_to_Free @{thm frac_sym_conv}),
155 Rule.Thm ("sqrt_sym_conv", ThmC.numerals_to_Free @{thm sqrt_sym_conv}),
156 Rule.Thm ("root_sym_conv", ThmC.numerals_to_Free @{thm root_sym_conv}),
157 Rule.Thm ("sym_real_mult_minus1",
158 ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym})),
160 Rule.Thm ("rat_mult",ThmC.numerals_to_Free @{thm rat_mult}),
161 (*a / b * (c / d) = a * c / (b * d)*)
162 Rule.Thm ("times_divide_eq_right",ThmC.numerals_to_Free @{thm times_divide_eq_right}),
163 (*?x * (?y / ?z) = ?x * ?y / ?z*)
164 Rule.Thm ("times_divide_eq_left",ThmC.numerals_to_Free @{thm times_divide_eq_left}),
165 (*?y / ?z * ?x = ?y * ?x / ?z*)
166 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_")
168 scr = Rule.Empty_Prog};
172 Rule_Def.Repeat {id="srls_differentiate..",
174 rew_ord = ("termlessI",termlessI),
175 erls = Rule_Set.empty,
176 srls = Rule_Set.Empty, calc = [], errpatts = [],
177 rules = [Rule.Eval("Prog_Expr.lhs", Prog_Expr.eval_lhs "eval_lhs_"),
178 Rule.Eval("Prog_Expr.rhs", Prog_Expr.eval_rhs "eval_rhs_"),
179 Rule.Eval("Diff.primed", eval_primed "Diff.primed")
181 scr = Rule.Empty_Prog};
186 Rule_Set.append_rules "erls_differentiate.." Rule_Set.empty
187 [Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
188 Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
190 Rule.Eval ("Prog_Expr.ident", Prog_Expr.eval_ident "#ident_"),
191 Rule.Eval ("Prog_Expr.is'_atom", Prog_Expr.eval_is_atom "#is_atom_"),
192 Rule.Eval ("Prog_Expr.occurs'_in", Prog_Expr.eval_occurs_in ""),
193 Rule.Eval ("Prog_Expr.is'_const", Prog_Expr.eval_const "#is_const_")
196 (*.rules for differentiation, _no_ simplification.*)
198 Rule_Def.Repeat {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
199 erls = erls_diff, srls = Rule_Set.Empty, calc = [], errpatts = [],
200 rules = [Rule.Thm ("diff_sum",ThmC.numerals_to_Free @{thm diff_sum}),
201 Rule.Thm ("diff_dif",ThmC.numerals_to_Free @{thm diff_dif}),
202 Rule.Thm ("diff_prod_const",ThmC.numerals_to_Free @{thm diff_prod_const}),
203 Rule.Thm ("diff_prod",ThmC.numerals_to_Free @{thm diff_prod}),
204 Rule.Thm ("diff_quot",ThmC.numerals_to_Free @{thm diff_quot}),
205 Rule.Thm ("diff_sin",ThmC.numerals_to_Free @{thm diff_sin}),
206 Rule.Thm ("diff_sin_chain",ThmC.numerals_to_Free @{thm diff_sin_chain}),
207 Rule.Thm ("diff_cos",ThmC.numerals_to_Free @{thm diff_cos}),
208 Rule.Thm ("diff_cos_chain",ThmC.numerals_to_Free @{thm diff_cos_chain}),
209 Rule.Thm ("diff_pow",ThmC.numerals_to_Free @{thm diff_pow}),
210 Rule.Thm ("diff_pow_chain",ThmC.numerals_to_Free @{thm diff_pow_chain}),
211 Rule.Thm ("diff_ln",ThmC.numerals_to_Free @{thm diff_ln}),
212 Rule.Thm ("diff_ln_chain",ThmC.numerals_to_Free @{thm diff_ln_chain}),
213 Rule.Thm ("diff_exp",ThmC.numerals_to_Free @{thm diff_exp}),
214 Rule.Thm ("diff_exp_chain",ThmC.numerals_to_Free @{thm diff_exp_chain}),
216 Rule.Thm ("diff_sqrt",ThmC.numerals_to_Free @{thm diff_sqrt}),
217 Rule.Thm ("diff_sqrt_chain",ThmC.numerals_to_Free @{thm diff_sqrt_chain}),
219 Rule.Thm ("diff_const",ThmC.numerals_to_Free @{thm diff_const}),
220 Rule.Thm ("diff_var",ThmC.numerals_to_Free @{thm diff_var})
222 scr = Rule.Empty_Prog};
225 (*.normalisation for checking user-input.*)
228 {id="norm_diff", preconds = [], rew_ord = ("termlessI",termlessI),
229 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
230 rules = [Rule.Rls_ diff_rules, Rule.Rls_ norm_Poly ],
231 scr = Rule.Empty_Prog};
233 setup \<open>KEStore_Elems.add_rlss
234 [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)),
235 ("diff_rules", (Context.theory_name @{theory}, prep_rls' diff_rules)),
236 ("norm_diff", (Context.theory_name @{theory}, prep_rls' norm_diff)),
237 ("diff_conv", (Context.theory_name @{theory}, prep_rls' diff_conv)),
238 ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls' diff_sym_conv))]\<close>
240 (** problem types **)
241 setup \<open>KEStore_Elems.add_pbts
242 [(Problem.prep_input thy "pbl_fun" [] Problem.id_empty (["function"], [], Rule_Set.empty, NONE, [])),
243 (Problem.prep_input thy "pbl_fun_deriv" [] Problem.id_empty
244 (["derivative_of","function"],
245 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
246 ("#Find" ,["derivative f_f'"])],
247 Rule_Set.append_rules "empty" Rule_Set.empty [],
248 SOME "Diff (f_f, v_v)", [["diff","differentiate_on_R"],
249 ["diff","after_simplification"]])),
250 (*here "named" is used differently from Integration"*)
251 (Problem.prep_input thy "pbl_fun_deriv_nam" [] Problem.id_empty
252 (["named","derivative_of","function"],
253 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
254 ("#Find" ,["derivativeEq f_f'"])],
255 Rule_Set.append_rules "empty" Rule_Set.empty [],
256 SOME "Differentiate (f_f, v_v)",
257 [["diff","differentiate_equality"]]))]\<close>
262 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
263 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
264 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
266 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
267 [((Thm.term_of o the o (TermC.parse thy)) "functionTerm", [t]),
268 ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),
269 ((Thm.term_of o the o (TermC.parse thy)) "derivative",
270 [(Thm.term_of o the o (TermC.parse thy)) "f_f'"])
272 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
274 setup \<open>KEStore_Elems.add_mets
275 [Method.prep_input thy "met_diff" [] Method.id_empty
277 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
278 crls = Atools_erls, errpats = [], nrls = norm_diff},
282 partial_function (tailrec) differentiate_on_R :: "real \<Rightarrow> real \<Rightarrow> real"
284 "differentiate_on_R f_f v_v = (
286 f_f' = Take (d_d v_v f_f)
288 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'')) #> (
290 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
291 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'')) Or
292 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
293 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
294 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
295 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
296 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
297 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
298 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
299 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
300 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
301 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
302 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
303 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
304 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
305 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
306 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
307 Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv''))
309 setup \<open>KEStore_Elems.add_mets
310 [Method.prep_input thy "met_diff_onR" [] Method.id_empty
311 (["diff","differentiate_on_R"],
312 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]),
313 ("#Find" ,["derivative f_f'"])],
314 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
315 crls = Atools_erls, errpats = [], nrls = norm_diff},
316 @{thm differentiate_on_R.simps})]
319 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real"
321 "differentiateX f_f v_v = (
323 f_f' = Take (d_d v_v f_f)
326 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'')) Or
327 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' )) Or
328 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'')) Or
329 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'')) Or
330 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'')) Or
331 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'')) Or
332 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'')) Or
333 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'')) Or
334 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'')) Or
335 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'')) Or
336 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'')) Or
337 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'')) Or
338 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'')) Or
339 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'')) Or
340 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'')) Or
341 (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'')) Or
342 (Repeat (Rewrite_Set ''make_polynomial'')))
344 setup \<open>KEStore_Elems.add_mets
345 [Method.prep_input thy "met_diff_simpl" [] Method.id_empty
346 (["diff","diff_simpl"],
347 [("#Given", ["functionTerm f_f","differentiateFor v_v"]),
348 ("#Find" , ["derivative f_f'"])],
349 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
350 crls = Atools_erls, errpats = [], nrls = norm_diff},
351 @{thm differentiateX.simps})]
354 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool"
356 "differentiate_equality f_f v_v = (
358 f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f))
360 (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' )) #> (
362 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sum'')) Or
363 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_dif'' )) Or
364 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod_const'')) Or
365 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_prod'')) Or
366 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_quot'')) Or
367 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin'')) Or
368 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_sin_chain'')) Or
369 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos'')) Or
370 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_cos_chain'')) Or
371 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow'')) Or
372 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_pow_chain'')) Or
373 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln'')) Or
374 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_ln_chain'')) Or
375 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp'')) Or
376 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_exp_chain'')) Or
377 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_const'')) Or
378 (Repeat (Rewrite_Inst [(''bdv'', v_v)] ''diff_var'')) Or
379 (Repeat (Rewrite_Set ''make_polynomial'')))) #> (
380 Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''diff_sym_conv'' ))
382 setup \<open>KEStore_Elems.add_mets
383 [Method.prep_input thy "met_diff_equ" [] Method.id_empty
384 (["diff","differentiate_equality"],
385 [("#Given" ,["functionEq f_f","differentiateFor v_v"]),
386 ("#Find" ,["derivativeEq f_f'"])],
387 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule_Set.empty,
388 crls=Atools_erls, errpats = [], nrls = norm_diff},
389 @{thm differentiate_equality.simps})]
392 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real"
394 "simplify_derivative term bound_variable = (
396 term' = Take (d_d bound_variable term)
398 (Try (Rewrite_Set ''norm_Rational'')) #>
399 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_conv'')) #>
400 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''norm_diff'')) #>
401 (Try (Rewrite_Set_Inst [(''bdv'', bound_variable)] ''diff_sym_conv'')) #>
402 (Try (Rewrite_Set ''norm_Rational''))
405 setup \<open>KEStore_Elems.add_mets
406 [Method.prep_input thy "met_diff_after_simp" [] Method.id_empty
407 (["diff","after_simplification"],
408 [("#Given" ,["functionTerm term","differentiateFor bound_variable"]),
409 ("#Find" ,["derivative term'"])],
410 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
411 crls=Atools_erls, errpats = [], nrls = norm_Rational},
412 @{thm simplify_derivative.simps})]
414 setup \<open>KEStore_Elems.add_cas
415 [((Thm.term_of o the o (TermC.parse thy)) "Diff",
416 (("Isac_Knowledge", ["derivative_of","function"], ["no_met"]), argl2dtss))]\<close>
419 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
420 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
421 val [Const ("Product_Type.Pair", _) $ t $ bdv] = pairl;
423 fun argl2dtss [Const ("Product_Type.Pair", _) $ t $ bdv] =
424 [((Thm.term_of o the o (TermC.parse thy)) "functionEq", [t]),
425 ((Thm.term_of o the o (TermC.parse thy)) "differentiateFor", [bdv]),
426 ((Thm.term_of o the o (TermC.parse thy)) "derivativeEq",
427 [(Thm.term_of o the o (TermC.parse thy)) "f_f'::bool"])
429 | argl2dtss _ = raise ERROR "Diff.ML: wrong argument for argl2dtss";
431 setup \<open>KEStore_Elems.add_cas
432 [((Thm.term_of o the o (TermC.parse thy)) "Differentiate",
433 (("Isac_Knowledge", ["named","derivative_of","function"], ["no_met"]), argl2dtss))]\<close>