1 (* differentiation over the reals
6 theory Diff imports Calculus Trig LogExp Rational Root Poly Atools begin
10 d_d :: "[real, real]=> real"
11 sin, cos :: "real => real"
13 log, ln :: "real => real"
14 nlog :: "[real, real] => real"
15 exp :: "real => real" ("E'_ ^^^ _" 80)
17 (*descriptions in the related problems*)
18 derivativeEq :: bool => una
21 primed :: "'a => 'a" (*"primed A" -> "A'"*)
23 (*the CAS-commands, eg. "Diff (2*x^^^3, x)",
24 "Differentiate (A = s * (a - s), s)"*)
25 Diff :: "[real * real] => real"
26 Differentiate :: "[bool * real] => bool"
28 (*subproblem and script-name*)
29 differentiate :: "[ID * (ID list) * ID, real,real] => real"
30 ("(differentiate (_)/ (_ _ ))" 9)
31 DiffScr :: "[real,real, real] => real"
32 ("((Script DiffScr (_ _ =))// (_))" 9)
33 DiffEqScr :: "[bool,real, bool] => bool"
34 ("((Script DiffEqScr (_ _ =))// (_))" 9)
36 text {*a variant of the derivatives defintion:
38 d_d :: "(real => real) => (real => real)"
41 (1) no variable 'bdv' on the meta-level required
42 (2) chain_rule "d_d (%x. (u (v x))) = (%x. (d_d u)) (v x) * d_d v"
43 (3) and no specialized chain-rules required like
44 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
46 disadvantage: d_d (%x. 1 + x^2) = ... differs from high-school notation
49 axioms (*stated as axioms, todo: prove as theorems
50 'bdv' is a constant on the meta-level *)
51 diff_const "[| Not (bdv occurs_in a) |] ==> d_d bdv a = 0"
52 diff_var "d_d bdv bdv = 1"
53 diff_prod_const"[| Not (bdv occurs_in u) |] ==>
54 d_d bdv (u * v) = u * d_d bdv v"
56 diff_sum "d_d bdv (u + v) = d_d bdv u + d_d bdv v"
57 diff_dif "d_d bdv (u - v) = d_d bdv u - d_d bdv v"
58 diff_prod "d_d bdv (u * v) = d_d bdv u * v + u * d_d bdv v"
59 diff_quot "Not (v = 0) ==> (d_d bdv (u / v) =
60 (d_d bdv u * v - u * d_d bdv v) / v ^^^ 2)"
62 diff_sin "d_d bdv (sin bdv) = cos bdv"
63 diff_sin_chain "d_d bdv (sin u) = cos u * d_d bdv u"
64 diff_cos "d_d bdv (cos bdv) = - sin bdv"
65 diff_cos_chain "d_d bdv (cos u) = - sin u * d_d bdv u"
66 diff_pow "d_d bdv (bdv ^^^ n) = n * (bdv ^^^ (n - 1))"
67 diff_pow_chain "d_d bdv (u ^^^ n) = n * (u ^^^ (n - 1)) * d_d bdv u"
68 diff_ln "d_d bdv (ln bdv) = 1 / bdv"
69 diff_ln_chain "d_d bdv (ln u) = d_d bdv u / u"
70 diff_exp "d_d bdv (exp bdv) = exp bdv"
71 diff_exp_chain "d_d bdv (exp u) = exp u * d_d x u"
73 diff_sqrt "d_d bdv (sqrt bdv) = 1 / (2 * sqrt bdv)"
74 diff_sqrt_chain"d_d bdv (sqrt u) = d_d bdv u / (2 * sqrt u)"
78 frac_conv "[| bdv occurs_in b; 0 < n |] ==>
79 a / (b ^^^ n) = a * b ^^^ (-n)"
80 frac_sym_conv "n < 0 ==> a * b ^^^ n = a / b ^^^ (-n)"
82 sqrt_conv_bdv "sqrt bdv = bdv ^^^ (1 / 2)"
83 sqrt_conv_bdv_n "sqrt (bdv ^^^ n) = bdv ^^^ (n / 2)"
84 sqrt_conv "bdv occurs_in u ==> sqrt u = u ^^^ (1 / 2)"
85 sqrt_sym_conv "u ^^^ (a / 2) = sqrt (u ^^^ a)"
87 root_conv "bdv occurs_in u ==> nroot n u = u ^^^ (1 / n)"
88 root_sym_conv "u ^^^ (a / b) = nroot b (u ^^^ a)"
90 realpow_pow_bdv "(bdv ^^^ b) ^^^ c = bdv ^^^ (b * c)"
93 (** eval functions **)
95 fun primed (Const (id, T)) = Const (id ^ "'", T)
96 | primed (Free (id, T)) = Free (id ^ "'", T)
97 | primed t = raise error ("primed called with arg = '"^ term2str t ^"'");
99 (*("primed", ("Diff.primed", eval_primed "#primed"))*)
100 fun eval_primed _ _ (p as (Const ("Diff.primed",_) $ t)) _ =
101 SOME ((term2str p) ^ " = " ^ term2str (primed t),
102 Trueprop $ (mk_equality (p, primed t)))
103 | eval_primed _ _ _ _ = NONE;
105 calclist':= overwritel (!calclist',
106 [("primed", ("Diff.primed", eval_primed "#primed"))
112 (*.converts a term such that differentiation works optimally.*)
116 rew_ord = ("termlessI",termlessI),
117 erls = append_rls "erls_diff_conv" e_rls
118 [Calc ("Atools.occurs'_in", eval_occurs_in ""),
119 Thm ("not_true",num_str @{thm not_true}),
120 Thm ("not_false",num_str @{thm not_false}),
121 Calc ("op <",eval_equ "#less_"),
122 Thm ("and_true",num_str @{thm and_true}),
123 Thm ("and_false",num_str @{thm and_false)
125 srls = Erls, calc = [],
126 rules = [Thm ("frac_conv", num_str @{thm frac_conv}),
127 Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}),
128 Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}),
129 Thm ("sqrt_conv", num_str @{thm sqrt_conv}),
130 Thm ("root_conv", num_str @{thm root_conv}),
131 Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}),
132 Calc ("op *", eval_binop "#mult_"),
133 Thm ("rat_mult",num_str @{thm rat_mult}),
134 (*a / b * (c / d) = a * c / (b * d)*)
135 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
136 (*?x * (?y / ?z) = ?x * ?y / ?z*)
137 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left})
138 (*?y / ?z * ?x = ?y * ?x / ?z*)
140 Thm ("", num_str @{}),*)
144 (*.beautifies a term after differentiation.*)
146 Rls {id="diff_sym_conv",
148 rew_ord = ("termlessI",termlessI),
149 erls = append_rls "erls_diff_sym_conv" e_rls
150 [Calc ("op <",eval_equ "#less_")
152 srls = Erls, calc = [],
153 rules = [Thm ("frac_sym_conv", num_str @{thm frac_sym_conv}),
154 Thm ("sqrt_sym_conv", num_str @{thm sqrt_sym_conv}),
155 Thm ("root_sym_conv", num_str @{thm root_sym_conv}),
156 Thm ("sym_real_mult_minus1",
157 num_str (@{thm real_mult_minus1} RS @{thm sym})),
159 Thm ("rat_mult",num_str @{thm rat_mult}),
160 (*a / b * (c / d) = a * c / (b * d)*)
161 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}),
162 (*?x * (?y / ?z) = ?x * ?y / ?z*)
163 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}),
164 (*?y / ?z * ?x = ?y * ?x / ?z*)
165 Calc ("op *", eval_binop "#mult_")
171 Rls {id="srls_differentiate..",
173 rew_ord = ("termlessI",termlessI),
175 srls = Erls, calc = [],
176 rules = [Calc("Tools.lhs", eval_lhs "eval_lhs_"),
177 Calc("Tools.rhs", eval_rhs "eval_rhs_"),
178 Calc("Diff.primed", eval_primed "Diff.primed")
184 append_rls "erls_differentiate.." e_rls
185 [Thm ("not_true",num_str @{thm not_true}),
186 Thm ("not_false",num_str @{thm not_false}),
188 Calc ("Atools.ident",eval_ident "#ident_"),
189 Calc ("Atools.is'_atom",eval_is_atom "#is_atom_"),
190 Calc ("Atools.occurs'_in",eval_occurs_in ""),
191 Calc ("Atools.is'_const",eval_const "#is_const_")
194 (*.rules for differentiation, _no_ simplification.*)
196 Rls {id="diff_rules", preconds = [], rew_ord = ("termlessI",termlessI),
197 erls = erls_diff, srls = Erls, calc = [],
198 rules = [Thm ("diff_sum",num_str @{thm diff_sum}),
199 Thm ("diff_dif",num_str @{thm diff_dif}),
200 Thm ("diff_prod_const",num_str @{thm diff_prod_const}),
201 Thm ("diff_prod",num_str @{thm diff_prod}),
202 Thm ("diff_quot",num_str @{thm diff_quot}),
203 Thm ("diff_sin",num_str @{thm diff_sin}),
204 Thm ("diff_sin_chain",num_str @{thm diff_sin_chain}),
205 Thm ("diff_cos",num_str @{thm diff_cos}),
206 Thm ("diff_cos_chain",num_str @{thm diff_cos_chain}),
207 Thm ("diff_pow",num_str @{thm diff_pow}),
208 Thm ("diff_pow_chain",num_str @{thm diff_pow_chain}),
209 Thm ("diff_ln",num_str @{thm diff_ln}),
210 Thm ("diff_ln_chain",num_str @{thm diff_ln_chain}),
211 Thm ("diff_exp",num_str @{thm diff_exp}),
212 Thm ("diff_exp_chain",num_str @{thm diff_exp_chain}),
214 Thm ("diff_sqrt",num_str @{thm diff_sqrt}),
215 Thm ("diff_sqrt_chain",num_str @{thm diff_sqrt_chain}),
217 Thm ("diff_const",num_str @{thm diff_const}),
218 Thm ("diff_var",num_str @{thm diff_var})
222 (*.normalisation for checking user-input.*)
224 Rls {id="diff_rls", preconds = [], rew_ord = ("termlessI",termlessI),
225 erls = Erls, srls = Erls, calc = [],
226 rules = [Rls_ diff_rules,
231 overwritelthy @{theory} (!ruleset',
232 [("diff_rules", prep_rls norm_diff),
233 ("norm_diff", prep_rls norm_diff),
234 ("diff_conv", prep_rls diff_conv),
235 ("diff_sym_conv", prep_rls diff_sym_conv)
239 (** problem types **)
242 (prep_pbt (theory "Diff") "pbl_fun" [] e_pblID
243 (["function"], [], e_rls, NONE, []));
246 (prep_pbt (theory "Diff") "pbl_fun_deriv" [] e_pblID
247 (["derivative_of","function"],
248 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
249 ("#Find" ,["derivative f_'_"])
251 append_rls "e_rls" e_rls [],
252 SOME "Diff (f_, v_)", [["diff","differentiate_on_R"],
253 ["diff","after_simplification"]]));
255 (*here "named" is used differently from Integration"*)
257 (prep_pbt (theory "Diff") "pbl_fun_deriv_nam" [] e_pblID
258 (["named","derivative_of","function"],
259 [("#Given" ,["functionEq f_","differentiateFor v_"]),
260 ("#Find" ,["derivativeEq f_'_"])
262 append_rls "e_rls" e_rls [],
263 SOME "Differentiate (f_, v_)", [["diff","differentiate_equality"]]));
269 (prep_met (theory "Diff") "met_diff" [] e_metID
271 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
272 crls = Atools_erls, nrls = norm_diff}, "empty_script"));
275 (prep_met (theory "Diff") "met_diff_onR" [] e_metID
276 (["diff","differentiate_on_R"],
277 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
278 ("#Find" ,["derivative f_'_"])
280 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
281 prls=e_rls, crls = Atools_erls, nrls = norm_diff},
282 "Script DiffScr (f_::real) (v_::real) = " ^
283 " (let f'_ = Take (d_d v_ f_) " ^
284 " in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
286 " ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
287 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
288 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
289 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
290 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
291 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
292 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
293 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
294 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
295 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
296 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
297 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
298 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
299 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
300 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
301 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
302 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
303 " (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
307 (prep_met (theory "Diff") "met_diff_simpl" [] e_metID
308 (["diff","diff_simpl"],
309 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
310 ("#Find" ,["derivative f_'_"])
312 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = e_rls,
313 prls=e_rls, crls = Atools_erls, nrls = norm_diff},
314 "Script DiffScr (f_::real) (v_::real) = " ^
315 " (let f'_ = Take (d_d v_ f_) " ^
318 " ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
319 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
320 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
321 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
322 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
323 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
324 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
325 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
326 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
327 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
328 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
329 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
330 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
331 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
332 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
333 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
334 " (Repeat (Rewrite_Set make_polynomial False)))) " ^
339 (prep_met (theory "Diff") "met_diff_equ" [] e_metID
340 (["diff","differentiate_equality"],
341 [("#Given" ,["functionEq f_","differentiateFor v_"]),
342 ("#Find" ,["derivativeEq f_'_"])
344 {rew_ord'="tless_true", rls' = erls_diff, calc = [],
345 srls = srls_diff, prls=e_rls, crls=Atools_erls, nrls = norm_diff},
346 "Script DiffEqScr (f_::bool) (v_::real) = " ^
347 " (let f'_ = Take ((primed (lhs f_)) = d_d v_ (rhs f_)) " ^
348 " in (((Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
350 " ((Repeat (Rewrite_Inst [(bdv,v_)] diff_sum False)) Or " ^
351 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_dif False)) Or " ^
352 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod_const False)) Or " ^
353 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_prod False)) Or " ^
354 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_quot True )) Or " ^
355 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin False)) Or " ^
356 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_sin_chain False)) Or " ^
357 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos False)) Or " ^
358 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_cos_chain False)) Or " ^
359 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow False)) Or " ^
360 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_pow_chain False)) Or " ^
361 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln False)) Or " ^
362 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_ln_chain False)) Or " ^
363 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp False)) Or " ^
364 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_exp_chain False)) Or " ^
365 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_const False)) Or " ^
366 " (Repeat (Rewrite_Inst [(bdv,v_)] diff_var False)) Or " ^
367 " (Repeat (Rewrite_Set make_polynomial False)))) @@ " ^
368 " (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)))) f'_)"
372 (prep_met (theory "Diff") "met_diff_after_simp" [] e_metID
373 (["diff","after_simplification"],
374 [("#Given" ,["functionTerm f_","differentiateFor v_"]),
375 ("#Find" ,["derivative f_'_"])
377 {rew_ord'="tless_true", rls' = e_rls, calc = [], srls = e_rls, prls=e_rls,
378 crls=Atools_erls, nrls = norm_Rational},
379 "Script DiffScr (f_::real) (v_::real) = " ^
380 " (let f'_ = Take (d_d v_ f_) " ^
381 " in ((Try (Rewrite_Set norm_Rational False)) @@ " ^
382 " (Try (Rewrite_Set_Inst [(bdv,v_)] diff_conv False)) @@ " ^
383 " (Try (Rewrite_Set_Inst [(bdv,v_)] norm_diff False)) @@ " ^
384 " (Try (Rewrite_Set_Inst [(bdv,v_)] diff_sym_conv False)) @@ " ^
385 " (Try (Rewrite_Set norm_Rational False))) f'_)"
391 (*.handle cas-input like "Diff (a * x^3 + b, x)".*)
392 (* val (t, pairl) = strip_comb (str2term "Diff (a * x^3 + b, x)");
393 val [Const ("Pair", _) $ t $ bdv] = pairl;
395 fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
396 [((term_of o the o (parse thy)) "functionTerm", [t]),
397 ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
398 ((term_of o the o (parse thy)) "derivative",
399 [(term_of o the o (parse thy)) "f_'_"])
401 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
404 [((term_of o the o (parse thy)) "Diff",
405 (("Isac.thy", ["derivative_of","function"], ["no_met"]),
409 (*.handle cas-input like "Differentiate (A = s * (a - s), s)".*)
410 (* val (t, pairl) = strip_comb (str2term "Differentiate (A = s * (a - s), s)");
411 val [Const ("Pair", _) $ t $ bdv] = pairl;
413 fun argl2dtss [Const ("Pair", _) $ t $ bdv] =
414 [((term_of o the o (parse thy)) "functionEq", [t]),
415 ((term_of o the o (parse thy)) "differentiateFor", [bdv]),
416 ((term_of o the o (parse thy)) "derivativeEq",
417 [(term_of o the o (parse thy)) "f_'_::bool"])
419 | argl2dtss _ = raise error "Diff.ML: wrong argument for argl2dtss";
422 [((term_of o the o (parse thy)) "Differentiate",
423 (("Isac.thy", ["named","derivative_of","function"], ["no_met"]),