10 \<close> |
10 \<close> |
11 |
11 |
12 consts |
12 consts |
13 |
13 |
14 d_d :: "[real, real]=> real" |
14 d_d :: "[real, real]=> real" |
15 (*sin, cos :: "real => real" already in Isabelle2009-2*) |
15 |
16 (* |
|
17 log, ln :: "real => real" |
|
18 nlog :: "[real, real] => real" |
|
19 exp :: "real => real" ("E'_ ^^^ _" 80) |
|
20 *) |
|
21 (*descriptions in the related problems*) |
16 (*descriptions in the related problems*) |
22 derivativeEq :: "bool => una" |
17 derivativeEq :: "bool => una" |
23 |
18 |
24 (*predicates*) |
19 (*predicates*) |
25 primed :: "'a => 'a" (*"primed A" -> "A'"*) |
20 primed :: "'a => 'a" (*"primed A" -> "A'"*) |
27 (*the CAS-commands, eg. "Diff (2*x^^^3, x)", |
22 (*the CAS-commands, eg. "Diff (2*x^^^3, x)", |
28 "Differentiate (A = s * (a - s), s)"*) |
23 "Differentiate (A = s * (a - s), s)"*) |
29 Diff :: "[real * real] => real" |
24 Diff :: "[real * real] => real" |
30 Differentiate :: "[bool * real] => bool" |
25 Differentiate :: "[bool * real] => bool" |
31 |
26 |
32 (*subproblem and script-name*) |
27 (*subproblem-name*) |
33 differentiate :: "[char list * char list list * char list, real, real] => real" |
28 differentiate :: "[char list * char list list * char list, real, real] => real" |
34 ("(differentiate (_)/ (_ _ ))" 9) |
29 ("(differentiate (_)/ (_ _ ))" 9) |
35 DiffScr :: "[real,real, real] => real" |
|
36 ("((Script DiffScr (_ _ =))// (_))" 9) |
|
37 DiffEqScr :: "[bool,real, bool] => bool" |
|
38 ("((Script DiffEqScr (_ _ =))// (_))" 9) |
|
39 |
30 |
40 text \<open>a variant of the derivatives defintion: |
31 text \<open>a variant of the derivatives defintion: |
41 |
32 |
42 d_d :: "(real => real) => (real => real)" |
33 d_d :: "(real => real) => (real => real)" |
43 |
34 |
317 (["diff","differentiate_on_R"], |
308 (["diff","differentiate_on_R"], |
318 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
309 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
319 ("#Find" ,["derivative f_f'"])], |
310 ("#Find" ,["derivative f_f'"])], |
320 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
311 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
321 crls = Atools_erls, errpats = [], nrls = norm_diff}, |
312 crls = Atools_erls, errpats = [], nrls = norm_diff}, |
322 @{thm differentiate_on_R.simps} |
313 @{thm differentiate_on_R.simps})] |
323 (*"Script DiffScr (f_f::real) (v_v::real) = " ^ |
|
324 " (let f_f' = Take (d_d v_v f_f) " ^ |
|
325 " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^ |
|
326 " (Repeat " ^ |
|
327 " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^ |
|
328 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^ |
|
329 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^ |
|
330 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or " ^ |
|
331 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^ |
|
332 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^ |
|
333 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^ |
|
334 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^ |
|
335 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^ |
|
336 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^ |
|
337 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^ |
|
338 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^ |
|
339 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^ |
|
340 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^ |
|
341 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^ |
|
342 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^ |
|
343 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^ |
|
344 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f')"*))] |
|
345 \<close> |
314 \<close> |
346 |
315 |
347 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real" |
316 partial_function (tailrec) differentiateX :: "real \<Rightarrow> real \<Rightarrow> real" |
348 where |
317 where |
349 "differentiateX f_f v_v = |
318 "differentiateX f_f v_v = |
373 (["diff","diff_simpl"], |
342 (["diff","diff_simpl"], |
374 [("#Given", ["functionTerm f_f","differentiateFor v_v"]), |
343 [("#Given", ["functionTerm f_f","differentiateFor v_v"]), |
375 ("#Find" , ["derivative f_f'"])], |
344 ("#Find" , ["derivative f_f'"])], |
376 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
345 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
377 crls = Atools_erls, errpats = [], nrls = norm_diff}, |
346 crls = Atools_erls, errpats = [], nrls = norm_diff}, |
378 @{thm differentiateX.simps} |
347 @{thm differentiateX.simps})] |
379 (*"Script DiffScr (f_f::real) (v_v::real) = " ^ |
|
380 " (let f_f' = Take (d_d v_v f_f) " ^ |
|
381 " in (( " ^ |
|
382 " (Repeat " ^ |
|
383 " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^ |
|
384 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^ |
|
385 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^ |
|
386 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' False)) Or " ^ |
|
387 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^ |
|
388 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^ |
|
389 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^ |
|
390 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^ |
|
391 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^ |
|
392 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^ |
|
393 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^ |
|
394 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^ |
|
395 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^ |
|
396 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^ |
|
397 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^ |
|
398 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^ |
|
399 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) " ^ |
|
400 " )) f_f')"*))] |
|
401 \<close> |
348 \<close> |
402 |
349 |
403 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool" |
350 partial_function (tailrec) differentiate_equality :: "bool \<Rightarrow> real \<Rightarrow> bool" |
404 where |
351 where |
405 "differentiate_equality f_f v_v = |
352 "differentiate_equality f_f v_v = |
432 (["diff","differentiate_equality"], |
379 (["diff","differentiate_equality"], |
433 [("#Given" ,["functionEq f_f","differentiateFor v_v"]), |
380 [("#Given" ,["functionEq f_f","differentiateFor v_v"]), |
434 ("#Find" ,["derivativeEq f_f'"])], |
381 ("#Find" ,["derivativeEq f_f'"])], |
435 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule.e_rls, |
382 {rew_ord'="tless_true", rls' = erls_diff, calc = [], srls = srls_diff, prls=Rule.e_rls, |
436 crls=Atools_erls, errpats = [], nrls = norm_diff}, |
383 crls=Atools_erls, errpats = [], nrls = norm_diff}, |
437 @{thm differentiate_equality.simps} |
384 @{thm differentiate_equality.simps})] |
438 (*"Script DiffEqScr (f_f::bool) (v_v::real) = " ^ |
|
439 " (let f_f' = Take ((primed (lhs f_f)) = d_d v_v (rhs f_f)) " ^ |
|
440 " in (((Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^ |
|
441 " (Repeat " ^ |
|
442 " ((Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sum'' False)) Or " ^ |
|
443 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_dif'' False)) Or " ^ |
|
444 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod_const'' False)) Or " ^ |
|
445 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_prod'' False)) Or " ^ |
|
446 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_quot'' True )) Or " ^ |
|
447 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin'' False)) Or " ^ |
|
448 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_sin_chain'' False)) Or " ^ |
|
449 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos'' False)) Or " ^ |
|
450 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_cos_chain'' False)) Or " ^ |
|
451 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow'' False)) Or " ^ |
|
452 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_pow_chain'' False)) Or " ^ |
|
453 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln'' False)) Or " ^ |
|
454 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_ln_chain'' False)) Or " ^ |
|
455 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp'' False)) Or " ^ |
|
456 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_exp_chain'' False)) Or " ^ |
|
457 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_const'' False)) Or " ^ |
|
458 " (Repeat (Rewrite_Inst [(''bdv'',v_v)] ''diff_var'' False)) Or " ^ |
|
459 " (Repeat (Rewrite_Set ''make_polynomial'' False)))) @@ " ^ |
|
460 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)))) f_f') "*))] |
|
461 \<close> |
385 \<close> |
462 |
386 |
463 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real" |
387 partial_function (tailrec) simplify_derivative :: "real \<Rightarrow> real \<Rightarrow> real" |
464 where |
388 where |
465 "simplify_derivative f_f v_v = |
389 "simplify_derivative f_f v_v = |
475 (["diff","after_simplification"], |
399 (["diff","after_simplification"], |
476 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
400 [("#Given" ,["functionTerm f_f","differentiateFor v_v"]), |
477 ("#Find" ,["derivative f_f'"])], |
401 ("#Find" ,["derivative f_f'"])], |
478 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
402 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls, prls=Rule.e_rls, |
479 crls=Atools_erls, errpats = [], nrls = norm_Rational}, |
403 crls=Atools_erls, errpats = [], nrls = norm_Rational}, |
480 @{thm simplify_derivative.simps} |
404 @{thm simplify_derivative.simps})] |
481 (*"Script DiffScr (f_f::real) (v_v::real) = " ^ |
|
482 " (let f_f' = Take (d_d v_v f_f) " ^ |
|
483 " in ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^ |
|
484 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_conv'' False)) @@ " ^ |
|
485 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''norm_diff'' False)) @@ " ^ |
|
486 " (Try (Rewrite_Set_Inst [(''bdv'',v_v)] ''diff_sym_conv'' False)) @@ " ^ |
|
487 " (Try (Rewrite_Set ''norm_Rational'' False))) f_f')"*))] |
|
488 \<close> |
405 \<close> |
489 setup \<open>KEStore_Elems.add_cas |
406 setup \<open>KEStore_Elems.add_cas |
490 [((Thm.term_of o the o (TermC.parse thy)) "Diff", |
407 [((Thm.term_of o the o (TermC.parse thy)) "Diff", |
491 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))]\<close> |
408 (("Isac", ["derivative_of","function"], ["no_met"]), argl2dtss))]\<close> |
492 ML \<open> |
409 ML \<open> |