(* tests on integration over the reals

   author: Walther Neuper

   050814, 08:51

   (c) due to copyright terms

use"../smltest/IsacKnowledge/integrate.sml";

use"integrate.sml";

*)

val thy = theory "Integrate";

"--------------------------------------------------------";

"table of contents --------------------------------------";

"--------------------------------------------------------";

"----------- parsing ------------------------------------";

"----------- integrate by rewriting ---------------------";

"----------- test add_new_c, is_f_x ---------------------";

"----------- simplify by ruleset reducing make_ratpoly_in";

"----------- simplify by extending make_polynomial_in ---";

"----------- integrate by ruleset -----------------------";

"----------- rewrite 3rd integration in 7.27 ------------";

"----------- check probem type --------------------------";

"----------- check Scripts ------------------------------";

"----------- me method [diff,integration] ---------------";

"----------- me method [diff,integration,named] ---------";

"----------- me met [diff,integration,named] Biegelinie.Q";

"----------- interSteps [diff,integration] --------------";

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

"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

"----------- CAS input ----------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"--------------------------------------------------------";

"----------- parsing ------------------------------------";

"----------- parsing ------------------------------------";

"----------- parsing ------------------------------------";

fun str2term str = (term_of o the o (parse thy)) str;

fun term2s t = Print_Mode.setmp [] (Syntax.string_of_term

					(ProofContext.init_global thy)) t;

val t = str2term "Integral x D x";

val t = str2term "Integral x^^^2 D x";

atomty t;

val t = str2term "ff x is_f_x";

case t of Const ("Integrate.is'_f'_x", _) $ _ => ()

	| _ => error "integrate.sml: parsing: ff x is_f_x";

"----------- integrate by rewriting ---------------------";

"----------- integrate by rewriting ---------------------";

"----------- integrate by rewriting ---------------------";

val conditions_in_integration_rules =

Rls {id="conditions_in_integration_rules", 

     preconds = [], 

     rew_ord = ("termlessI",termlessI), 

     erls = Erls, 

     srls = Erls, calc = [],

     rules = [(*for rewriting conditions in Thm's*)

	      Calc ("Atools.occurs'_in", 

		    eval_occurs_in "#occurs_in_"),

	      Thm ("not_true",num_str @{thm not_true}),

	      Thm ("not_false",num_str @{thm not_false})

	      ],

     scr = EmptyScr};

val subs = [(str2term "bdv", str2term "x")];

fun rewrit thm str = 

    fst (the (rewrite_inst_ thy tless_true 

			   conditions_in_integration_rules 

			   true subs thm str));

val str = rewrit @{thm "integral_const"} (str2term "Integral 1 D x");

term2s str;

val str = rewrit @{thm "integral_const"} (str2term  "Integral M'/EJ D x");

term2s str;

val str = (rewrit @{thm "integral_const"} (str2term "Integral x D x")) 

    handle OPTION => str2term "no_rewrite";

val str = rewrit @{thm "integral_var"} (str2term "Integral x D x");

term2s str;

val str = (rewrit @{thm "integral_var"} (str2term "Integral a D x"))

    handle OPTION => str2term "no_rewrite";

val str = rewrit @{thm "integral_add"} (str2term "Integral x + 1 D x");

term2s str;

val str = rewrit @{thm "integral_mult"} (str2term "Integral M'/EJ * x^^^3 D x");

term2s str;

val str = (rewrit @{thm "integral_mult"} (str2term "Integral x * x D x"))

    handle OPTION => str2term "no_rewrite";

val str = rewrit @{thm "integral_pow"} (str2term "Integral x^^^3 D x");

term2s str;

"----------- test add_new_c, is_f_x ---------------------";

"----------- test add_new_c, is_f_x ---------------------";

"----------- test add_new_c, is_f_x ---------------------";

val term = str2term "x^^^2*c + c_2";

val cc = new_c term;

if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";

val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;

if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()

else error "intergrate.sml: diff. eval_add_new_c";

val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");

val SOME (thmstr, thm) = get_calculation1_ thy cc term;

val SOME (t',_) = rewrite_set_ thy true add_new_c term;

if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()

else error "intergrate.sml: diff. rewrite_set add_new_c 1";

val term = str2term "ff x = x^^^2*c + c_2";

val SOME (t',_) = rewrite_set_ thy true add_new_c term;

if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()

else error "intergrate.sml: diff. rewrite_set add_new_c 2";

(*WN080222 replace call_new_c with add_new_c----------------------

val term = str2term "new_c (c * x^^^2 + c_2)";

val SOME (_,t') = eval_new_c 0 0 term 0;

if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()

else error "integrate.sml: eval_new_c ???";

val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2)";

val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()

else error "integrate.sml: matches new_c = False";

val t = str2term "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";

val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';

if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"

then () else error "integrate.sml: matches new_c = True";

val t = str2term "ff x is_f_x";

val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';

if term2s t' = "(ff x is_f_x) = True" then ()

else error "integrate.sml: eval_is_f_x --> true";

val t = str2term "q_0/2 * L * x is_f_x";

val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';

if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()

else error "integrate.sml: eval_is_f_x --> false";

val conditions_in_integration =

Rls {id="conditions_in_integration", 

     preconds = [], 

     rew_ord = ("termlessI",termlessI), 

     erls = Erls, 

     srls = Erls, calc = [],

     rules = [Calc ("Tools.matches",eval_matches ""),

      	Calc ("Integrate.is'_f'_x", 

      	      eval_is_f_x "is_f_x_"),

      	Thm ("not_true",num_str @{thm not_true}),

      	Thm ("not_false",num_str @{thm not_false})

      	],

     scr = EmptyScr};

fun rewrit thm t = 

    fst (the (rewrite_inst_ thy tless_true 

			    conditions_in_integration true subs thm t));

val t = rewrit call_for_new_c (str2term "x ^^^ 2 / 2"); term2s t;

val t = (rewrit call_for_new_c t)

    handle OPTION =>  str2term "no_rewrite";

val t = rewrit call_for_new_c 

	       (str2term "ff x = q_0/2 *L*x"); term2s t;

val t = (rewrit call_for_new_c 

	       (str2term "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))

    handle OPTION => (*NOT:  + new_c ..=..!!*)str2term "no_rewrite";

--------------------------------------------------------------------*)

"----------- simplify by ruleset reducing make_ratpoly_in";

"----------- simplify by ruleset reducing make_ratpoly_in";

"----------- simplify by ruleset reducing make_ratpoly_in";

val thy = theory "Isac";

"===== test 1";

val subs = [(str2term "bdv", str2term "x")];

val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";

"----- stepwise from the rulesets in simplify_Integral and below-----";

val rls = norm_Rational_noadd_fractions;

case rewrite_set_inst_ thy true subs rls t of

    SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"

  | NONE => ();

"===== test 2";

val rls = order_add_mult_in;

val SOME (t,[]) = rewrite_set_ thy true rls t;

if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()

else error "integrate.sml simplify by ruleset order_add_mult_in #2";

"===== test 3";

val rls = discard_parentheses;

val SOME (t,[]) = rewrite_set_ thy true rls t;

if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()

else error "integrate.sml simplify by ruleset discard_parenth.. #3";

"===== test 4";

val rls = 

    (append_rls "separate_bdv"

 	       collect_bdv

 	       [Thm ("separate_bdv", num_str @{thm separate_bdv}),

 		(*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

                (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)

 		Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),

                (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)

 		Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),

 		(*"?bdv / ?b = (1 / ?b) * ?bdv"*)

                (*"?bdv / ?b = (1::?'a) / ?b * ?bdv"*)

 		Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})

                (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)

               ]);

(*show_types := true;  --- do we need type-constraint in thms? *)

@{thm separate_bdv};     (*::?'a does NOT rewrite here WITHOUT type constraint*)

@{thm separate_bdv_n};   (*::real ..because of ^^^, rewrites*)

@{thm separate_1_bdv};   (*::?'a*)

val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)

@{thm separate_1_bdv_n}; (*::real ..because of ^^^*)

(*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)

val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;

if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()

else error "integrate.sml simplify by ruleset separate_bdv.. #4";

"===== test 5";

val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";

val rls = simplify_Integral;

val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;

if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()

else error "integrate.sml, simplify_Integral #99";

"........... 2nd integral ........................................";

"........... 2nd integral ........................................";

"........... 2nd integral ........................................";

val t = str2term 

"Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";

val rls = simplify_Integral;

val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;

term2str t;

(*===== inhibit exn ============================================================

if term2str t = 

 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"

GOON: still 2*3 TODO...

 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / (2 * 3) * x ^^^ 3) D x"

then () else error "integrate.sml, simplify_Integral #198";

trace_rewrite := true;

tracing "====== test 4 =============================";

tracing "====== test 4 =============================";

term2str t;

trace_rewrite := false;

(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.

-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

val rls = integration_rules;

val SOME (t,[]) = rewrite_set_ thy true rls t;

if term2str t = 

   "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"

then () else error "integrate.sml, simplify_Integral #199";

"----------- simplify by extending make_polynomial_in ---";

"----------- simplify by extending make_polynomial_in ---";

"----------- simplify by extending make_polynomial_in ---";

trace_rewrite:=true;

trace_rewrite:=false;

(*postponed: see *)

"----------- integrate by ruleset -----------------------";

"----------- integrate by ruleset -----------------------";

"----------- integrate by ruleset -----------------------";

val rls = "integration_rules";

val subs = [("bdv","x::real")];

fun rewrit_sinst subs rls str = 

    fst (the (rewrite_set_inst "Integrate" true subs rls str));

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

val str = rewrit_sinst subs rls "Integral x D x";

val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";

if str = "c * (x ^^^ 3 / 3) + c_2 * x"

then () else error "integrate.sml: diff.behav. in integration_rules";

val rls = "add_new_c";

val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";

if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then () 

else error "integrate.sml: diff.behav. in add_new_c simpl.";

val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";

if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then () 

else error "integrate.sml: diff.behav. in add_new_c equation";

val rls = "simplify_Integral";

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";

val str = rewrit_sinst subs rls str;

if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"

then () else error "integrate.sml: diff.behav. in simplify_I #1";

val rls = "integration";

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";

if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"

then () else error "integrate.sml: diff.behav. in integration #1";

val str = rewrit_sinst subs rls "Integral 3*x^^^2 + 2*x + 1 D x";

if str = "c + x + x ^^^ 2 + x ^^^ 3" then () 

else error "integrate.sml: diff.behav. in integration #2";

val str = rewrit_sinst subs rls 

"Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";

if str =

   "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"

then () else error "integrate.sml: diff.behav. in integration #3";

val str = "Integral "^str^" D x";

val str = rewrit_sinst subs rls str;

if str =

   "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"

then () else error "integrate.sml: diff.behav. in integration #4";

"----------- rewrite 3rd integration in 7.27 ------------";

"----------- rewrite 3rd integration in 7.27 ------------";

"----------- rewrite 3rd integration in 7.27 ------------";

val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);

val bdv = [(str2term"bdv", str2term"x")];

val t = str2term

	    "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";

val SOME(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;

if term2str t = 

   "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then ()

else error "integrate.sml 3rd integration in 7.27, simplify_Integral";

val SOME(t,_)= rewrite_set_inst_ thy true bdv integration t;

if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"

then () else error "integrate.sml 3rd integration in 7.27, integration";

"----------- check probem type --------------------------";

"----------- check probem type --------------------------";

"----------- check probem type --------------------------";

val model = {Given =["functionTerm f_f", "integrateBy v_v"],

	     Where =[],

	     Find  =["antiDerivative F_"],

	     With  =[],

	     Relate=[]}:string ppc;

val chkmodel = ((map (the o (parse thy))) o ppc2list) model;

val t1 = (term_of o hd) chkmodel;

val t2 = (term_of o hd o tl) chkmodel;

val t3 = (term_of o hd o tl o tl) chkmodel;

case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()

	 | _ => error "integrate.sml: Integrate.antiDerivative ???";

val model = {Given =["functionTerm f_f", "integrateBy v_v"],

	     Where =[],

	     Find  =["antiDerivativeName F_"],

	     With  =[],

	     Relate=[]}:string ppc;

val chkmodel = ((map (the o (parse thy))) o ppc2list) model;

val t1 = (term_of o hd) chkmodel;

val t2 = (term_of o hd o tl) chkmodel;

val t3 = (term_of o hd o tl o tl) chkmodel;

case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()

	 | _ => error "integrate.sml: Integrate.antiDerivativeName";

"----- compare 'Find's from problem, script, formalization -------";

val {ppc,...} = get_pbt ["named","integrate","function"];

val ("#Find", (Const ("Integrate.antiDerivativeName", _),

	       F1_ as Free ("F_", F1_type))) = last_elem ppc;

val {scr = Script sc,... } = get_met ["diff","integration","named"];

val [_,_, F2_] = formal_args sc;

if F1_ = F2_ then () else error "integrate.sml: unequal find's";

val ((dsc as Const ("Integrate.antiDerivativeName", _)) 

	 $ Free ("ff", F3_type)) = str2term "antiDerivativeName ff";

if is_dsc dsc then () else error "integrate.sml: no description";

if F1_type = F3_type then () 

else error "integrate.sml: unequal types in find's";

show_ptyps();

val pbl = get_pbt ["integrate","function"];

case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()

	 | _ => error "integrate.sml: Integrate.Integrate ???";

"----------- check Scripts ------------------------------";

"----------- check Scripts ------------------------------";

"----------- check Scripts ------------------------------";

val str = 

"Script IntegrationScript (f_f::real) (v_v::real) =               \

\  (let t_ = Take (Integral f_ D v_v)                                 \

\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) (t_::real))";

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty sc;

val str = 

"Script NamedIntegrationScript (f_f::real) (v_v::real) (F_::real=>real) = \

\  (let t_ = Take (F_ v_v = Integral f_ D v_v)                         \

\   in (Rewrite_Set_Inst [(bdv,v_v)] integration False) t_)";

val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

atomty sc;

show_mets();

"----------- me method [diff,integration] ---------------";

"----------- me method [diff,integration] ---------------";

"----------- me method [diff,integration] ---------------";

(*exp_CalcInt_No-1.xml*)

val fmz = ["functionTerm (x^^^2 + 1)", 

	   "integrateBy x","antiDerivative FF"];

val (dI',pI',mI') =

  ("Integrate",["integrate","function"],

   ["diff","integration"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()

else error "integrate.sml: method [diff,integration]";

"----------- me method [diff,integration,named] ---------";

"----------- me method [diff,integration,named] ---------";

"----------- me method [diff,integration,named] ---------";

(*exp_CalcInt_No-2.xml*)

val fmz = ["functionTerm (x^^^2 + 1)", 

	   "integrateBy x","antiDerivativeName F"];

val (dI',pI',mI') =

  ("Integrate",["named","integrate","function"],

   ["diff","integration","named"]);

val p = e_pos'; val c = []; 

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then() 

else error "integrate.sml: method [diff,integration,named]";

"----------- me met [diff,integration,named] Biegelinie.Q";

"----------- me met [diff,integration,named] Biegelinie.Q";

"----------- me met [diff,integration,named] Biegelinie.Q";

(*exp_CalcInt_No-3.xml*)

val fmz = ["functionTerm (- q_0)", 

	   "integrateBy x","antiDerivativeName Q"];

val (dI',pI',mI') =

  ("Biegelinie",["named","integrate","function"],

   ["diff","integration","named"]);

val p = e_pos'; val c = [];

val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*Error Tac Q not in ...*)

val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt;

val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;

if f2str f = "Q x = c + -1 * q_0 * x" then() 

else error "integrate.sml: method [diff,integration,named] .Q";

"----------- interSteps [diff,integration] --------------";

"----------- interSteps [diff,integration] --------------";

"----------- interSteps [diff,integration] --------------";

states:=[];

CalcTree

[(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], 

  ("Integrate",["integrate","function"],

  ["diff","integration"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1; show_pt pt;

interSteps 1 ([1],Res);

val ((pt,p),_) = get_calc 1; show_pt pt;

if existpt' ([1,3], Res) pt then ()

else error "integrate.sml: interSteps on Rewrite_Set_Inst 1";

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

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

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

store_met

    (prep_met thy "met_testint" [] e_metID

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

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

		("#Find"  ,["antiDerivative F_"])

		],

	       {rew_ord'="tless_true", rls'=Atools_erls, calc = [], 

		srls = e_rls, 

		prls=e_rls,

	     crls = Atools_erls, nrls = e_rls},

"Script 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))"

));

states:=[];

CalcTree

[(["functionTerm (Integral x^2 + 1 D x)","integrateBy x",

   "antiDerivative FF"], 

  ("Integrate",["integrate","function"],

  ["diff","integration","test"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalcHead;

fetchProposedTactic 1  (*..Apply_Method*);

autoCalculate 1 (Step 1);

getTactic 1 ([1], Frm)  (*still empty*);

fetchProposedTactic 1  (*Rewrite_Set_Inst integration_rules*);

autoCalculate 1 (Step 1);

fetchProposedTactic 1  (*Rewrite_Set_Inst add_new_c*);

autoCalculate 1 (Step 1);

fetchProposedTactic 1  (*Rewrite_Set_Inst simplify_Integral*);

autoCalculate 1 (Step 1);

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1; show_pt pt;

if existpt' ([3], Res) pt then ()

else error  "integrate.sml: test-script doesnt work";

"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

"----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";

states:=[];

CalcTree

[(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"], 

  ("Integrate",["integrate","function"],

  ["diff","integration"]))];

Iterator 1;

moveActiveRoot 1;

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1; show_pt pt;

interSteps 1 ([1],Res);

val ((pt,p),_) = get_calc 1; show_pt pt;

interSteps 1 ([1,1],Res);

val ((pt,p),_) = get_calc 1; show_pt pt;

getTactic 1 ([1,1,1],Frm);

val str = (unenclose o string_of_thm) integral_add;

writeln str;

(*

read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));

*** More than one term is type correct:

*** ((Integral (?u + ?v) D ?bdv) =

***  (Integral ?u D (?bdv + (Integral ?v D ?bdv))))

                ###^^^###

*** ((Integral (?u + ?v) D ?bdv) =

***  ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))

*)

if existpt' ([1,1,5], Res) pt then ()

else error "integrate.sml: interSteps on Rewrite_Set_Inst 2";

"----------- CAS input ----------------------------------";

"----------- CAS input ----------------------------------";

"----------- CAS input ----------------------------------";

val t = str2term "Integrate (x^^^2 + x + 1, x)";

case t of Const ("Integrate.Integrate", _) $ _ => ()

	| _ => error "diff.sml behav.changed for Integrate (..., x)";

atomty t;

states:=[];

CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];

Iterator 1;

moveActiveRoot 1;

replaceFormula 1 "Integrate (x^2 + x + 1, x)";

autoCalculate 1 CompleteCalc;

val ((pt,p),_) = get_calc 1;

val Form res = (#1 o pt_extract) (pt, ([],Res));

show_pt pt;

(* WN070703 does not work like Diff due to error in next-pos

if p = ([], Res) andalso term2str res = "5 * a" then ()

else error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";

*)

===== inhibit exn ============================================================*)