(* Title:  test/Tools/isac/Knowledge/integrate.sml

    Author: Walther Neuper 050826

    (c) due to copyright terms

 *)

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

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

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

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

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

 "----------- test add_new_c, TermC.is_f_x ---------------------";

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

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

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

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

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

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

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

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

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

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

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

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

 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;

 they are used several times below; TODO remove duplicates*)

 val thy = @{theory "Integrate"};

 val ctxt = ThyC.to_ctxt thy;

 fun str2t str = parseNEW ctxt str |> the;

 fun term2s t = UnparseC.term_in_ctxt ctxt t;

 val conditions_in_integration_rules =

   Rule_Set.Repeat {id="conditions_in_integration_rules", 

     preconds = [], 

     rew_ord = ("termlessI",termlessI), 

     erls = Rule_Set.Empty, 

     srls = Rule_Set.Empty, calc = [], errpatts = [],

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

 	    Eval ("Prog_Expr.occurs_in", 

 		  eval_occurs_in "#occurs_in_"),

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

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

     scr = Empty_Prog};

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

 fun rewrit thm str = 

     fst (the (rewrite_inst_ thy tless_true 

 			   conditions_in_integration_rules 

 			   true subs thm str));

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

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

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

 val t = TermC.str2term "Integral x D x";

 val t = TermC.str2term "Integral x \<up> 2 D x";

 case t of 

     Const (\<^const_name>\<open>Integral\<close>, _) $

      (Const (\<^const_name>\<open>powr\<close>, _) $ Free _ $ _) $ Free ("x", _) => ()

   | _ => error "integrate.sml: parsing: Integral x \<up> 2 D x";

 val t = TermC.str2term "ff x is_f_x";

 case t of Const (\<^const_name>\<open>is_f_x\<close>, _) $ _ => ()

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

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

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

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

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

 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";

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

 if term2s str = "M' / EJ * x" then ()

 else error "Integral M'/EJ D x   BY integral_const";

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

 if term2s str = "x \<up> 2 / 2" then ()

 else error "Integral x D x   BY integral_var";

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

 if term2s str = "Integral x D x + Integral 1 D x" then ()

 else error "Integral x + 1 D x   BY integral_add";

 val str = rewrit @{thm "integral_mult"} (TermC.str2term "Integral M'/EJ * x \<up> 3 D x");

 if term2s str = "M' / EJ * Integral x \<up> 3 D x" then ()

 else error "Integral M'/EJ * x \<up> 3 D x   BY integral_mult";

 val str = rewrit @{thm "integral_pow"} (TermC.str2term "Integral x \<up> 3 D x");

 if term2s str = "x \<up> (3 + 1) / (3 + 1)" then ()

 else error "integrate.sml Integral x \<up> 3 D x";

 "----------- test add_new_c, TermC.is_f_x ---------------------";

 "----------- test add_new_c, TermC.is_f_x ---------------------";

 "----------- test add_new_c, TermC.is_f_x ---------------------";

 val term = TermC.str2term "x \<up> 2 * c + c_2";

 val cc = new_c term;

 if UnparseC.term 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 UnparseC.term t' = "x \<up> 2 * c + c_2 = x \<up> 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) = adhoc_thm1_ thy cc term;

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

 if UnparseC.term t' = "x \<up> 2 * c + c_2 + c_3" then ()

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

 val term = TermC.str2term "ff x = x \<up> 2*c + c_2";

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

 if UnparseC.term t' = "ff x = x \<up> 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 = str2t "new_c (c * x \<up> 2 + c_2)";

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

 if term2s t' = "new_c c * x \<up> 2 + c_2 = c_3" then ()

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

 val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2)";

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

 if term2s t' = "matches (?u + new_c ?v) (x \<up> 2 / 2) = False" then ()

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

 val t = str2t "matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2)";

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

 if term2s t'="matches (?u + new_c ?v) (x \<up> 2 / 2 + new_c x \<up> 2 / 2) = True"

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

 val t = str2t "ff x TermC.is_f_x";

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

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

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

 val t = str2t "q_0/2 * L * x TermC.is_f_x";

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

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

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

 val conditions_in_integration =

 Rule_Set.Repeat {id="conditions_in_integration", 

      preconds = [], 

      rew_ord = ("termlessI",termlessI), 

      erls = Rule_Set.Empty, 

      srls = Rule_Set.Empty, calc = [], errpatts = [],

      rules = [Eval ("Prog_Expr.matches",eval_matches ""),

       	Eval ("Integrate.is_f_x", 

       	      eval_is_f_x "is_f_x_"),

       	Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),

       	Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})

       	],

      scr = Empty_Prog};

 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 (str2t "x \<up> 2 / 2"); term2s t;

 val t = (rewrit call_for_new_c t)

     handle OPTION =>  str2t "no_rewrite";

 val t = rewrit call_for_new_c 

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

 val t = (rewrit call_for_new_c 

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

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

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

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

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

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

 \<close> ML \<open>

 val subst = [(TermC.str2term "bdv ::real", TermC.str2term "x ::real")]

 \<close> ML \<open>

 val thy = @{theory "Isac_Knowledge"};

 "===== test 1";

 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 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";

 \<close> ML \<open>

 val rls = order_add_mult_in;

 \<close> text \<open> (*GOON*)

 (*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\*)

         assume flawed test setup hidden by "handle _ => ..."

         ERROR ord_make_polynomial_in called with subst = []

 \<close> text \<open>

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

 UnparseC.term t

 if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + - 1 * (q_0 * x \<up> 2) / 2)" then()

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

 (*\\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite -----//*)

 "===== test 3";

 \<close> ML \<open>

 val rls = discard_parentheses;

 (*//--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO\\

         assume flawed test setup hidden by "handle _ => ..."

         ERROR ord_make_polynomial_in called with subst = []

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

 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" then ()

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

   \\--- broken in child of.1790e1073acc : eliminate "handle _ => ..." from Rewrite.rewrite TOODOO//*)

 "===== test 4";

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

 val rls = 

   (Rule_Set.append_rules "separate_bdv" collect_bdv

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

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

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

       (*"?a * ?bdv \<up> ?n / ?b = ?a / ?b * ?bdv \<up> ?n"*)

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

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

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

        (*"?bdv \<up> ?n / ?b = 1 / ?b * ?bdv \<up> ?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  \<up> , rewrites*)

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

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

 @{thm separate_1_bdv_n}; (*::real ..because of  \<up> *)

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

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

 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()

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

 "===== test 5";

 val t = TermC.str2term "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";

 val rls = simplify_Integral;

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

 (* given was:   "1 / EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)" *)

 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2)" then ()

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

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

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

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

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

 val thy = @{theory Biegelinie};

 val t = TermC.str2term 

   "Integral 1 / EI * (L * q_0 / 2 * (x \<up> 2 / 2) + - 1 * q_0 / 2 * (x \<up> 3 / 3)) D x";

 val rls = simplify_Integral;

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

 if UnparseC.term t = "Integral 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3) D x"

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

 val rls = integration_rules;

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

 if UnparseC.term t = "1 / EI * (L * q_0 / 4 * (x \<up> 3 / 3) + - 1 * q_0 / 6 * (x \<up> 4 / 4))"

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

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

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

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

 val thy = @{theory "Integrate"};

 val rls = integration_rules;

 val subs = [(@{term "bdv::real"}, @{term "x::real"})];

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

 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral x D x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "x \<up> 2 / 2" then () else error "Integral x D x changed";

 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x" then () else error "Integral c * x \<up> 2 + c_2 D x";

 val rls = add_new_c;

 val t = (Thm.term_of o the o (TermC.parse thy)) "c * (x \<up> 3 / 3) + c_2 * x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "c * (x \<up> 3 / 3) + c_2 * x + c_3" then () 

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

 val t = (Thm.term_of o the o (TermC.parse thy)) "F x = x \<up> 3 / 3 + x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "F x = x \<up> 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 t = (Thm.term_of o the o (TermC.parse thy)) "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "ff x = c_2 + c * x + - 1 * q_0 / 2 * x \<up> 2"

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

 val rls = integration;

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

 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral c * x \<up> 2 + c_2 D x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x \<up> 3"

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

 val t = (Thm.term_of o the o (TermC.parse thy)) "Integral 3*x \<up> 2 + 2*x + 1 D x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "c + x + x \<up> 2 + x \<up> 3" then () 

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

 val t = (Thm.term_of o the o (TermC.parse thy))

   "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x";

 if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"

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

 val t = (Thm.term_of o the o (TermC.parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");

 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;

 if UnparseC.term res = "c_2 + c * x +\n1 / EI * (L * q_0 / 12 * x \<up> 3 + - 1 * q_0 / 24 * x \<up> 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 = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);

 val t = TermC.str2term "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";

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

 if UnparseC.term t = 

   "Integral 1 / EI * (L * q_0 / 2 * x + - 1 * q_0 / 2 * x \<up> 2) D x"

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

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

 if UnparseC.term t = 

   "c + 1 / EI * (L * q_0 / 4 * x \<up> 2 + - 1 * q_0 / 6 * x \<up> 3)"

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

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

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

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

 val thy = @{theory Integrate};

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

 	     Where =[],

 	     Find  =["antiDerivative F_F"],

 	     With  =[],

 	     Relate=[]}:string ppc;

 val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;

 val t1 = (Thm.term_of o hd) chkmodel;

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

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

 case t3 of Const (\<^const_name>\<open>antiDerivative\<close>, _) $ _ => ()

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

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

 	     Where =[],

 	     Find  =["antiDerivativeName F_F"],

 	     With  =[],

 	     Relate=[]}:string ppc;

 val chkmodel = ((map (the o (TermC.parse thy))) o P_Model.to_list) model;

 val t1 = (Thm.term_of o hd) chkmodel;

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

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

 case t3 of Const (\<^const_name>\<open>antiDerivativeName\<close>, _) $ _ => ()

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

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

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

 val ("#Find", (Const (\<^const_name>\<open>antiDerivativeName\<close>, _),

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

 val {scr = Prog sc,... } = MethodC.from_store ["diff", "integration", "named"];

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

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

 val ((dsc as Const (\<^const_name>\<open>antiDerivativeName\<close>, _)) 

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

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

 if F1_type = F3_type then () 

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

 Test_Tool.show_ptyps();

 val pbl = Problem.from_store ["integrate", "function"];

 case #cas pbl of SOME (Const (\<^const_name>\<open>Integrate\<close>, _) $ _) => ()

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

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

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

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

 (*exp_CalcInt_No- 1.xml*)

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

 "----- step 0: returns nxt = Model_Problem ---";

 val (p,_,f,nxt,_,pt) = 

     CalcTreeTEST 

         [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"],

           ("Integrate", ["integrate", "function"], ["diff", "integration"]))];

 "----- step 1: returns nxt = Add_Given \"functionTerm (x \<up> 2 + 1)\" ---";

 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)

 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";

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

 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";

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

 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";

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

 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";

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

 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";

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

 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";

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

 case nxt of (Apply_Method ["diff", "integration"]) => ()

           | _ => error "integrate.sml -- me method [diff,integration] -- spec";

 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";

 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 \<up> 3" then ()

 else error "integrate.sml -- me method [diff,integration] -- end";

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

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

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

 reset_states ();

 CalcTree

     [(["functionTerm (x \<up> 2 + 1)", "integrateBy x", "antiDerivative FF"], 

       ("Integrate", ["integrate", "function"], ["diff", "integration"]))];

 Iterator 1;

 moveActiveRoot 1;

 autoCalculate 1 CompleteCalc;

 val ((pt,p),_) = get_calc 1; @{make_string} p; Test_Tool.show_pt pt;

 val (Form t,_,_) = ME_Misc.pt_extract (pt, p); 

 if UnparseC.term t = "c + x + 1 / 3 * x \<up> 3" then ()

 else error "integrate.sml -- interSteps [diff,integration] -- result";

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

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

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

 (*exp_CalcInt_No- 2.xml*)

 val fmz = ["functionTerm (x \<up> 2 + (1::real))", 

 	   "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 \<up> 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";