9 "----------- method analog to rls 'integration' ---------"; |
9 "----------- method analog to rls 'integration' ---------"; |
10 \<close> |
10 \<close> |
11 partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real" |
11 partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real" |
12 where |
12 where |
13 "integration_test f_f v_v = |
13 "integration_test f_f v_v = |
14 (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') @@ |
14 (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'') #> |
15 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') @@ |
15 (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'') #> |
16 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))" |
16 (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'')) (f_f::real))" |
17 setup \<open>KEStore_Elems.add_mets |
17 setup \<open>KEStore_Elems.add_mets |
18 [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID |
18 [Specify.prep_met @{theory "Isac_Knowledge"} "met_testint" [] Celem.e_metID |
19 (["diff","integration","test"], |
19 (["diff","integration","test"], |
20 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])], |
20 [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])], |