theory integrate

 imports Isac.Build_Thydata

 begin

 ML \<open>

 "----------- method analog to rls 'integration' ---------";

 "----------- method analog to rls 'integration' ---------";

 "----------- method analog to rls 'integration' ---------";

 \<close>

 partial_function (tailrec) integration_test :: "real \<Rightarrow> real \<Rightarrow> real"

   where

 "integration_test f_f v_v =

   (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@

     (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False)         @@

     (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"

 setup \<open>KEStore_Elems.add_mets

   [Specify.prep_met @{theory "Isac"} "met_testint" [] Celem.e_metID

 	    (["diff","integration","test"],

 	      [("#Given" ,["functionTerm f_f", "integrateBy v_v"]), ("#Find", ["antiDerivative F_F"])],

 	      {rew_ord'="tless_true", rls'=Atools_erls, calc = [], srls = Rule.e_rls, prls = Rule.e_rls,

 	        crls = Atools_erls, errpats = [], nrls = Rule.e_rls},

 	      @{thm integration_test.simps}

 	    (*"Program IntegrationScript (f_f::real) (v_v::real) =             \

   	      \  (((Rewrite_Set_Inst [(''bdv'',v_v)] ''integration_rules'' False) @@ \

           \    (Rewrite_Set_Inst [(''bdv'',v_v)] ''add_new_c'' False)         @@ \

           \    (Rewrite_Set_Inst [(''bdv'',v_v)] ''simplify_Integral'' False)) (f_f::real))"*))]

 \<close>

 end