(* 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 = Proof_Context.init_global 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_ ctxt tless_true 

			   conditions_in_integration_rules 

			   true subs thm str));

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

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

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

val t = TermC.parse_test @{context} "Integral x D x";

val t = TermC.parse_test @{context} "Integral x \<up> 2 D x";

case t of 

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

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

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

val t = TermC.parse_test @{context} "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.parse_test @{context} "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.parse_test @{context}  "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.parse_test @{context} "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.parse_test @{context} "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.parse_test @{context} "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.parse_test @{context} "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.parse_test @{context} "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 ctxt;

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_ @{context} cc term;

val SOME (t',_) = rewrite_set_ ctxt 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.parse_test @{context} "ff x = x \<up> 2*c + c_2";

val SOME (t',_) = rewrite_set_ ctxt 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";

val thy = @{theory "Isac_Knowledge"};

val ctxt = Proof_Context.init_global thy;

val subst = [(TermC.parse_test @{context} "bdv ::real", TermC.parse_test @{context} "x ::real")]; (*DOESN'T HELP*)

"===== test 1";

val t = TermC.parse_test @{context} "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_ ctxt 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_inst_ ctxt true subst 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 order_add_mult_in #2";

"===== test 3";

val rls = discard_parentheses;

val SOME (t, []) = rewrite_set_ ctxt 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";

"===== test 4";

val subs = [(TermC.parse_test @{context} "bdv::real", TermC.parse_test @{context} "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_ ctxt 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.parse_test @{context} "1/EI * (L * q_0 * x / 2 + - 1 * q_0 * x \<up> 2 / 2)";

val rls = simplify_Integral;

val SOME (t,[]) = rewrite_set_inst_ ctxt 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.parse_test @{context} "bdv::real", TermC.parse_test @{context} "x::real")];

val thy = @{theory Biegelinie};

val t = TermC.parse_test @{context} 

  "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_ ctxt 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_ ctxt 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 = TermC.parseNEW' ctxt "Integral x D x";

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

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

val t = TermC.parseNEW' ctxt "Integral c * x \<up> 2 + c_2 D x";

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt "c * (x \<up> 3 / 3) + c_2 * x";

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt "F x = x \<up> 3 / 3 + x";

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt "ff x = c * x + - 1 * q_0 * (x \<up> 2 / 2) + c_2";

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt "Integral c * x \<up> 2 + c_2 D x";

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt "Integral 3*x \<up> 2 + 2*x + 1 D x";

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt

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

val SOME (res, _) = rewrite_set_inst_ ctxt 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 = TermC.parseNEW' ctxt ("Integral " ^ UnparseC.term res ^ " D x");

val SOME (res, _) = rewrite_set_inst_ ctxt 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 t = TermC.parse_test @{context} "Integral 1 / EI * ((L * q_0 * x + - 1 * q_0 * x \<up> 2) / 2) D x";

val SOME(t, _)= rewrite_set_inst_ ctxt 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_ ctxt 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 (TermC.parseNEW' ctxt)) o P_Model.to_list) model;

val t1 = (hd) chkmodel;

val t2 = (hd o tl) chkmodel;

val t3 = (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 (TermC.parseNEW' ctxt)) o P_Model.to_list) model;

val t1 = (hd) chkmodel;

val t2 = (hd o tl) chkmodel;

val t3 = (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 @{context} ["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 ctxt ["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.parse_test @{context} "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 @{context} ["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] -----------";

States.reset ();

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),_) = States.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";