329 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory}, |
329 ("norm_Rational_rls_noadd_fractions", (Context.theory_name @{theory}, |
330 prep_rls' norm_Rational_rls_noadd_fractions))]\<close> |
330 prep_rls' norm_Rational_rls_noadd_fractions))]\<close> |
331 |
331 |
332 (** problems **) |
332 (** problems **) |
333 setup \<open>KEStore_Elems.add_pbts |
333 setup \<open>KEStore_Elems.add_pbts |
334 [(Specify.prep_pbt thy "pbl_fun_integ" [] Celem.e_pblID |
334 [(Specify.prep_pbt thy "pbl_fun_integ" [] Spec.e_pblID |
335 (["integrate","function"], |
335 (["integrate","function"], |
336 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
336 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
337 ("#Find" ,["antiDerivative F_F"])], |
337 ("#Find" ,["antiDerivative F_F"])], |
338 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], |
338 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], |
339 SOME "Integrate (f_f, v_v)", |
339 SOME "Integrate (f_f, v_v)", |
340 [["diff","integration"]])), |
340 [["diff","integration"]])), |
341 (*here "named" is used differently from Differentiation"*) |
341 (*here "named" is used differently from Differentiation"*) |
342 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Celem.e_pblID |
342 (Specify.prep_pbt thy "pbl_fun_integ_nam" [] Spec.e_pblID |
343 (["named","integrate","function"], |
343 (["named","integrate","function"], |
344 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
344 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
345 ("#Find" ,["antiDerivativeName F_F"])], |
345 ("#Find" ,["antiDerivativeName F_F"])], |
346 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], |
346 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)], |
347 SOME "Integrate (f_f, v_v)", |
347 SOME "Integrate (f_f, v_v)", |
355 let |
355 let |
356 t_t = Take (Integral f_f D v_v) |
356 t_t = Take (Integral f_f D v_v) |
357 in |
357 in |
358 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)" |
358 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') t_t)" |
359 setup \<open>KEStore_Elems.add_mets |
359 setup \<open>KEStore_Elems.add_mets |
360 [Specify.prep_met thy "met_diffint" [] Celem.e_metID |
360 [Specify.prep_met thy "met_diffint" [] Spec.e_metID |
361 (["diff","integration"], |
361 (["diff","integration"], |
362 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])], |
362 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find" ,["antiDerivative F_F"])], |
363 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
363 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
364 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}, |
364 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}, |
365 @{thm integrate.simps})] |
365 @{thm integrate.simps})] |
373 in ( |
373 in ( |
374 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #> |
374 (Try (Rewrite_Set_Inst [(''bdv'', v_v)] ''simplify_Integral'')) #> |
375 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') |
375 (Rewrite_Set_Inst [(''bdv'', v_v)] ''integration'') |
376 ) t_t)" |
376 ) t_t)" |
377 setup \<open>KEStore_Elems.add_mets |
377 setup \<open>KEStore_Elems.add_mets |
378 [Specify.prep_met thy "met_diffint_named" [] Celem.e_metID |
378 [Specify.prep_met thy "met_diffint_named" [] Spec.e_metID |
379 (["diff","integration","named"], |
379 (["diff","integration","named"], |
380 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
380 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
381 ("#Find" ,["antiDerivativeName F_F"])], |
381 ("#Find" ,["antiDerivativeName F_F"])], |
382 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
382 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty, |
383 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}, |
383 crls = Atools_erls, errpats = [], nrls = Rule_Set.empty}, |