335 (** problems **) |
335 (** problems **) |
336 |
336 |
337 store_pbt |
337 store_pbt |
338 (prep_pbt thy "pbl_fun_integ" [] e_pblID |
338 (prep_pbt thy "pbl_fun_integ" [] e_pblID |
339 (["integrate","function"], |
339 (["integrate","function"], |
340 [("#Given" ,["functionTerm f_", "integrateBy v_v"]), |
340 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
341 ("#Find" ,["antiDerivative F_"]) |
341 ("#Find" ,["antiDerivative F_"]) |
342 ], |
342 ], |
343 append_rls "e_rls" e_rls [(*for preds in where_*)], |
343 append_rls "e_rls" e_rls [(*for preds in where_*)], |
344 SOME "Integrate (f_, v_v)", |
344 SOME "Integrate (f_f, v_v)", |
345 [["diff","integration"]])); |
345 [["diff","integration"]])); |
346 |
346 |
347 (*here "named" is used differently from Differentiation"*) |
347 (*here "named" is used differently from Differentiation"*) |
348 store_pbt |
348 store_pbt |
349 (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID |
349 (prep_pbt thy "pbl_fun_integ_nam" [] e_pblID |
350 (["named","integrate","function"], |
350 (["named","integrate","function"], |
351 [("#Given" ,["functionTerm f_", "integrateBy v_v"]), |
351 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
352 ("#Find" ,["antiDerivativeName F_"]) |
352 ("#Find" ,["antiDerivativeName F_"]) |
353 ], |
353 ], |
354 append_rls "e_rls" e_rls [(*for preds in where_*)], |
354 append_rls "e_rls" e_rls [(*for preds in where_*)], |
355 SOME "Integrate (f_, v_v)", |
355 SOME "Integrate (f_f, v_v)", |
356 [["diff","integration","named"]])); |
356 [["diff","integration","named"]])); |
357 |
357 |
358 (** methods **) |
358 (** methods **) |
359 |
359 |
360 store_met |
360 store_met |
361 (prep_met thy "met_diffint" [] e_metID |
361 (prep_met thy "met_diffint" [] e_metID |
362 (["diff","integration"], |
362 (["diff","integration"], |
363 [("#Given" ,["functionTerm f_", "integrateBy v_v"]), |
363 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
364 ("#Find" ,["antiDerivative F_"]) |
364 ("#Find" ,["antiDerivative F_"]) |
365 ], |
365 ], |
366 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
366 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
367 srls = e_rls, |
367 srls = e_rls, |
368 prls=e_rls, |
368 prls=e_rls, |
369 crls = Atools_erls, nrls = e_rls}, |
369 crls = Atools_erls, nrls = e_rls}, |
370 "Script IntegrationScript (f_::real) (v_v::real) = " ^ |
370 "Script IntegrationScript (f_f::real) (v_v::real) = " ^ |
371 " (let t_ = Take (Integral f_ D v_v) " ^ |
371 " (let t_ = Take (Integral f_ D v_v) " ^ |
372 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))" |
372 " in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))" |
373 )); |
373 )); |
374 |
374 |
375 store_met |
375 store_met |
376 (prep_met thy "met_diffint_named" [] e_metID |
376 (prep_met thy "met_diffint_named" [] e_metID |
377 (["diff","integration","named"], |
377 (["diff","integration","named"], |
378 [("#Given" ,["functionTerm f_", "integrateBy v_v"]), |
378 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
379 ("#Find" ,["antiDerivativeName F_"]) |
379 ("#Find" ,["antiDerivativeName F_"]) |
380 ], |
380 ], |
381 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
381 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
382 srls = e_rls, |
382 srls = e_rls, |
383 prls=e_rls, |
383 prls=e_rls, |
384 crls = Atools_erls, nrls = e_rls}, |
384 crls = Atools_erls, nrls = e_rls}, |
385 "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = " ^ |
385 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = " ^ |
386 " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^ |
386 " (let t_ = Take (F_ v_v = Integral f_ D v_v) " ^ |
387 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ |
387 " in ((Try (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) @@ " ^ |
388 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) " |
388 " (Rewrite_Set_Inst [(bdv,v_v)] integration False)) t_) " |
389 )); |
389 )); |
390 *} |
390 *} |