312 |
312 |
313 |
313 |
314 "----------- check probem type -----------------------------------"; |
314 "----------- check probem type -----------------------------------"; |
315 "----------- check probem type -----------------------------------"; |
315 "----------- check probem type -----------------------------------"; |
316 "----------- check probem type -----------------------------------"; |
316 "----------- check probem type -----------------------------------"; |
317 val model = {Given =["functionTerm f_", "integrateBy v_v"], |
317 val model = {Given =["functionTerm f_f", "integrateBy v_v"], |
318 Where =[], |
318 Where =[], |
319 Find =["antiDerivative F_"], |
319 Find =["antiDerivative F_"], |
320 With =[], |
320 With =[], |
321 Relate=[]}:string ppc; |
321 Relate=[]}:string ppc; |
322 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model; |
322 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model; |
324 val t2 = (term_of o hd o tl) chkmodel; |
324 val t2 = (term_of o hd o tl) chkmodel; |
325 val t3 = (term_of o hd o tl o tl) chkmodel; |
325 val t3 = (term_of o hd o tl o tl) chkmodel; |
326 case t3 of Const ("Integrate.antiDerivative", _) $ _ => () |
326 case t3 of Const ("Integrate.antiDerivative", _) $ _ => () |
327 | _ => raise error "integrate.sml: Integrate.antiDerivative ???"; |
327 | _ => raise error "integrate.sml: Integrate.antiDerivative ???"; |
328 |
328 |
329 val model = {Given =["functionTerm f_", "integrateBy v_v"], |
329 val model = {Given =["functionTerm f_f", "integrateBy v_v"], |
330 Where =[], |
330 Where =[], |
331 Find =["antiDerivativeName F_"], |
331 Find =["antiDerivativeName F_"], |
332 With =[], |
332 With =[], |
333 Relate=[]}:string ppc; |
333 Relate=[]}:string ppc; |
334 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model; |
334 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model; |
360 |
360 |
361 "----------- check Scripts ---------------------------------------"; |
361 "----------- check Scripts ---------------------------------------"; |
362 "----------- check Scripts ---------------------------------------"; |
362 "----------- check Scripts ---------------------------------------"; |
363 "----------- check Scripts ---------------------------------------"; |
363 "----------- check Scripts ---------------------------------------"; |
364 val str = |
364 val str = |
365 "Script IntegrationScript (f_::real) (v_v::real) = \ |
365 "Script IntegrationScript (f_f::real) (v_v::real) = \ |
366 \ (let t_ = Take (Integral f_ D v_v) \ |
366 \ (let t_ = Take (Integral f_ D v_v) \ |
367 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"; |
367 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))"; |
368 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
368 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
369 atomty sc; |
369 atomty sc; |
370 |
370 |
371 val str = |
371 val str = |
372 "Script NamedIntegrationScript (f_::real) (v_v::real) (F_::real=>real) = \ |
372 "Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \ |
373 \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \ |
373 \ (let t_ = Take (F_ v_v = Integral f_ D v_v) \ |
374 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)"; |
374 \ in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)"; |
375 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
375 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
376 atomty sc; |
376 atomty sc; |
377 show_mets(); |
377 show_mets(); |
477 "----------- method analog to rls 'integration' ------------------"; |
477 "----------- method analog to rls 'integration' ------------------"; |
478 "----------- method analog to rls 'integration' ------------------"; |
478 "----------- method analog to rls 'integration' ------------------"; |
479 store_met |
479 store_met |
480 (prep_met Integrate.thy "met_testint" [] e_metID |
480 (prep_met Integrate.thy "met_testint" [] e_metID |
481 (["diff","integration","test"], |
481 (["diff","integration","test"], |
482 [("#Given" ,["functionTerm f_", "integrateBy v_v"]), |
482 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), |
483 ("#Find" ,["antiDerivative F_"]) |
483 ("#Find" ,["antiDerivative F_"]) |
484 ], |
484 ], |
485 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
485 {rew_ord'="tless_true", rls'=Atools_erls, calc = [], |
486 srls = e_rls, |
486 srls = e_rls, |
487 prls=e_rls, |
487 prls=e_rls, |
488 crls = Atools_erls, nrls = e_rls}, |
488 crls = Atools_erls, nrls = e_rls}, |
489 "Script IntegrationScript (f_::real) (v_v::real) = \ |
489 "Script IntegrationScript (f_f::real) (v_v::real) = \ |
490 \ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \ |
490 \ (((Rewrite_Set_Inst [(bdv,v_v)] integration_rules False) @@ \ |
491 \ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \ |
491 \ (Rewrite_Set_Inst [(bdv,v_v)] add_new_c False) @@ \ |
492 \ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_::real))" |
492 \ (Rewrite_Set_Inst [(bdv,v_v)] simplify_Integral False)) (f_f::real))" |
493 )); |
493 )); |
494 |
494 |
495 states:=[]; |
495 states:=[]; |
496 CalcTree |
496 CalcTree |
497 [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x", |
497 [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x", |