1 (* tests on integration over the reals
2 author: Walther Neuper 2005
3 (c) due to copyright terms
5 "--------------------------------------------------------";
6 "table of contents --------------------------------------";
7 "--------------------------------------------------------";
8 "----------- parsing ------------------------------------";
9 "----------- integrate by rewriting ---------------------";
10 "----------- test add_new_c, is_f_x ---------------------";
11 "----------- simplify by ruleset reducing make_ratpoly_in";
12 "----------- integrate by ruleset -----------------------";
13 "----------- rewrite 3rd integration in 7.27 ------------";
14 "----------- check probem type --------------------------";
15 "----------- me method [diff,integration] ---------------";
16 "----------- autoCalculate [diff,integration] -----------";
17 "----------- me method [diff,integration,named] ---------";
18 "----------- me met [diff,integration,named] Biegelinie.Q";
19 "----------- method analog to rls 'integration' ---------";
20 "--------------------------------------------------------";
21 "--------------------------------------------------------";
22 "--------------------------------------------------------";
24 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
25 they are used several times below; TODO remove duplicates*)
26 val thy = @{theory "Integrate"};
27 val ctxt = ThyC.to_ctxt thy;
29 fun str2t str = parseNEW ctxt str |> the;
30 fun term2s t = UnparseC.term_in_ctxt ctxt t;
32 val conditions_in_integration_rules =
33 Rule_Set.Repeat {id="conditions_in_integration_rules",
35 rew_ord = ("termlessI",termlessI),
36 erls = Rule_Set.Empty,
37 srls = Rule_Set.Empty, calc = [], errpatts = [],
38 rules = [(*for rewriting conditions in Thm's*)
39 Eval ("Prog_Expr.occurs'_in",
40 eval_occurs_in "#occurs_in_"),
41 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
42 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})],
44 val subs = [(str2t "bdv::real", str2t "x::real")];
46 fst (the (rewrite_inst_ thy tless_true
47 conditions_in_integration_rules
51 "----------- parsing ------------------------------------";
52 "----------- parsing ------------------------------------";
53 "----------- parsing ------------------------------------";
54 val t = str2t "Integral x D x";
55 val t = str2t "Integral x^^^2 D x";
57 Const ("Integrate.Integral", _) $
58 (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
59 | _ => error "integrate.sml: parsing: Integral x^^^2 D x";
61 val t = str2t "ff x is_f_x";
62 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
63 | _ => error "integrate.sml: parsing: ff x is_f_x";
66 "----------- integrate by rewriting ---------------------";
67 "----------- integrate by rewriting ---------------------";
68 "----------- integrate by rewriting ---------------------";
69 val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
70 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
72 val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
73 if term2s str = "M' / EJ * x" then ()
74 else error "Integral M'/EJ D x BY integral_const";
76 val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
77 if term2s str = "x ^^^ 2 / 2" then ()
78 else error "Integral x D x BY integral_var";
80 val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
81 if term2s str = "Integral x D x + Integral 1 D x" then ()
82 else error "Integral x + 1 D x BY integral_add";
84 val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");
85 if term2s str = "M' / EJ * Integral x ^^^ 3 D x" then ()
86 else error "Integral M'/EJ * x^^^3 D x BY integral_mult";
88 val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");
89 if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()
90 else error "integrate.sml Integral x^^^3 D x";
93 "----------- test add_new_c, is_f_x ---------------------";
94 "----------- test add_new_c, is_f_x ---------------------";
95 "----------- test add_new_c, is_f_x ---------------------";
96 val term = str2t "x^^^2 * c + c_2";
98 if UnparseC.term cc = "c_3" then () else error "integrate.sml: new_c ???";
100 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
101 if UnparseC.term t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
102 else error "intergrate.sml: diff. eval_add_new_c";
104 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
105 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
107 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
108 if UnparseC.term t' = "x ^^^ 2 * c + c_2 + c_3" then ()
109 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
111 val term = str2t "ff x = x^^^2*c + c_2";
112 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
113 if UnparseC.term t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
114 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
117 (*WN080222 replace call_new_c with add_new_c----------------------
118 val term = str2t "new_c (c * x^^^2 + c_2)";
119 val SOME (_,t') = eval_new_c 0 0 term 0;
120 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
121 else error "integrate.sml: eval_new_c ???";
123 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
124 val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
125 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
126 else error "integrate.sml: matches new_c = False";
128 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
129 val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
130 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
131 then () else error "integrate.sml: matches new_c = True";
133 val t = str2t "ff x is_f_x";
134 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
135 if term2s t' = "(ff x is_f_x) = True" then ()
136 else error "integrate.sml: eval_is_f_x --> true";
138 val t = str2t "q_0/2 * L * x is_f_x";
139 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
140 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
141 else error "integrate.sml: eval_is_f_x --> false";
143 val conditions_in_integration =
144 Rule_Set.Repeat {id="conditions_in_integration",
146 rew_ord = ("termlessI",termlessI),
147 erls = Rule_Set.Empty,
148 srls = Rule_Set.Empty, calc = [], errpatts = [],
149 rules = [Eval ("Prog_Expr.matches",eval_matches ""),
150 Eval ("Integrate.is'_f'_x",
151 eval_is_f_x "is_f_x_"),
152 Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
153 Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
157 fst (the (rewrite_inst_ thy tless_true
158 conditions_in_integration true subs thm t));
159 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
160 val t = (rewrit call_for_new_c t)
161 handle OPTION => str2t "no_rewrite";
163 val t = rewrit call_for_new_c
164 (str2t "ff x = q_0/2 *L*x"); term2s t;
165 val t = (rewrit call_for_new_c
166 (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
167 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
168 --------------------------------------------------------------------*)
171 "----------- simplify by ruleset reducing make_ratpoly_in";
172 "----------- simplify by ruleset reducing make_ratpoly_in";
173 "----------- simplify by ruleset reducing make_ratpoly_in";
174 val thy = @{theory "Isac_Knowledge"};
176 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
178 "----- stepwise from the rulesets in simplify_Integral and below-----";
179 val rls = norm_Rational_noadd_fractions;
180 case rewrite_set_inst_ thy true subs rls t of
181 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
185 val rls = order_add_mult_in;
186 val SOME (t,[]) = rewrite_set_ thy true rls t;
187 if UnparseC.term t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
188 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
191 val rls = discard_parentheses;
192 val SOME (t,[]) = rewrite_set_ thy true rls t;
193 if UnparseC.term t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
194 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
197 val subs = [(str2t "bdv::real", str2t "x::real")];
199 (Rule_Set.append_rules "separate_bdv" collect_bdv
200 [Thm ("separate_bdv", ThmC.numerals_to_Free @{thm separate_bdv}),
201 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
202 Thm ("separate_bdv_n", ThmC.numerals_to_Free @{thm separate_bdv_n}),
203 (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
204 Thm ("separate_1_bdv", ThmC.numerals_to_Free @{thm separate_1_bdv}),
205 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
206 Thm ("separate_1_bdv_n", ThmC.numerals_to_Free @{thm separate_1_bdv_n})
207 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
209 (*show_types := true; --- do we need type-constraint in thms? *)
210 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
211 @{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
212 @{thm separate_1_bdv}; (*::?'a*)
213 val xxx = ThmC.numerals_to_Free @{thm separate_1_bdv}; (*::?'a*)
214 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
215 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
217 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
218 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
219 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
222 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
223 val rls = simplify_Integral;
224 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
225 (* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
226 if UnparseC.term t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
227 else error "integrate.sml, simplify_Integral #99";
229 "........... 2nd integral ........................................";
230 "........... 2nd integral ........................................";
231 "........... 2nd integral ........................................";
233 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
234 val rls = simplify_Integral;
235 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
237 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
238 then () else raise error "integrate.sml, simplify_Integral #198";
240 val rls = integration_rules;
241 val SOME (t,[]) = rewrite_set_ thy true rls t;
244 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
245 then () else error "integrate.sml, simplify_Integral #199";
248 "----------- integrate by ruleset -----------------------";
249 "----------- integrate by ruleset -----------------------";
250 "----------- integrate by ruleset -----------------------";
251 val thy = @{theory "Integrate"};
252 val rls = integration_rules;
253 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
254 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
256 val t = (Thm.term_of o the o (parse thy)) "Integral x D x";
257 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
258 if UnparseC.term res = "x ^^^ 2 / 2" then () else error "Integral x D x changed";
260 val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
261 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
262 if UnparseC.term res = "c * (x ^^^ 3 / 3) + c_2 * x" then () else error "Integral c * x ^^^ 2 + c_2 D x";
265 val t = (Thm.term_of o the o (parse thy)) "c * (x ^^^ 3 / 3) + c_2 * x";
266 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
267 if UnparseC.term res = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
268 else error "integrate.sml: diff.behav. in add_new_c simpl.";
270 val t = (Thm.term_of o the o (parse thy)) "F x = x ^^^ 3 / 3 + x";
271 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
272 if UnparseC.term res = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
273 else error "integrate.sml: diff.behav. in add_new_c equation";
275 val rls = simplify_Integral;
276 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
277 val t = (Thm.term_of o the o (parse thy)) "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
278 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
279 if UnparseC.term res = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
280 then () else error "integrate.sml: diff.behav. in simplify_I #1";
282 val rls = integration;
283 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
284 val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
285 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
286 if UnparseC.term res = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
287 then () else error "integrate.sml: diff.behav. in integration #1";
289 val t = (Thm.term_of o the o (parse thy)) "Integral 3*x^^^2 + 2*x + 1 D x";
290 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
291 if UnparseC.term res = "c + x + x ^^^ 2 + x ^^^ 3" then ()
292 else error "integrate.sml: diff.behav. in integration #2";
294 val t = (Thm.term_of o the o (parse thy))
295 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
296 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
297 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
298 if UnparseC.term res = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
299 then () else error "integrate.sml: diff.behav. in integration #3";
301 val t = (Thm.term_of o the o (parse thy)) ("Integral " ^ UnparseC.term res ^ " D x");
302 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
303 if UnparseC.term res = "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
304 then () else error "integrate.sml: diff.behav. in integration #4";
306 "----------- rewrite 3rd integration in 7.27 ------------";
307 "----------- rewrite 3rd integration in 7.27 ------------";
308 "----------- rewrite 3rd integration in 7.27 ------------";
309 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
310 val t = str2t "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
311 val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;
313 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
314 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
316 val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
319 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
320 then () else error "integrate.sml 3rd integration in 7.27, integration";
323 "----------- check probem type --------------------------";
324 "----------- check probem type --------------------------";
325 "----------- check probem type --------------------------";
326 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
328 Find =["antiDerivative F_F"],
330 Relate=[]}:string ppc;
331 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
332 val t1 = (Thm.term_of o hd) chkmodel;
333 val t2 = (Thm.term_of o hd o tl) chkmodel;
334 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
335 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
336 | _ => error "integrate.sml: Integrate.antiDerivative ???";
338 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
340 Find =["antiDerivativeName F_F"],
342 Relate=[]}:string ppc;
343 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
344 val t1 = (Thm.term_of o hd) chkmodel;
345 val t2 = (Thm.term_of o hd o tl) chkmodel;
346 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
347 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
348 | _ => error "integrate.sml: Integrate.antiDerivativeName";
350 "----- compare 'Find's from problem, script, formalization -------";
351 val {ppc,...} = Problem.from_store ["named","integrate","function"];
352 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
353 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
354 val {scr = Prog sc,... } = Method.from_store ["diff","integration","named"];
355 val [_,_, F2_] = formal_args sc;
356 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
358 val ((dsc as Const ("Integrate.antiDerivativeName", _))
359 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
360 if Input_Descript.is_a dsc then () else error "integrate.sml: no description";
361 if F1_type = F3_type then ()
362 else error "integrate.sml: unequal types in find's";
364 Test_Tool.show_ptyps();
365 val pbl = Problem.from_store ["integrate","function"];
366 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
367 | _ => error "integrate.sml: Integrate.Integrate ???";
370 "----------- me method [diff,integration] ---------------";
371 "----------- me method [diff,integration] ---------------";
372 "----------- me method [diff,integration] ---------------";
373 (*exp_CalcInt_No-1.xml*)
374 val p = e_pos'; val c = [];
375 "----- step 0: returns nxt = Model_Problem ---";
376 val (p,_,f,nxt,_,pt) =
378 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
379 ("Integrate", ["integrate","function"], ["diff","integration"]))];
380 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
381 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
382 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
383 val (p,_,f,nxt,_,pt) = me nxt p c pt;
384 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
385 val (p,_,f,nxt,_,pt) = me nxt p c pt;
386 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
387 val (p,_,f,nxt,_,pt) = me nxt p c pt;
388 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
389 val (p,_,f,nxt,_,pt) = me nxt p c pt;
390 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
391 val (p,_,f,nxt,_,pt) = me nxt p c pt;
392 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
393 val (p,_,f,nxt,_,pt) = me nxt p c pt;
394 case nxt of (Apply_Method ["diff", "integration"]) => ()
395 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
396 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
397 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
398 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
399 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
400 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
401 else error "integrate.sml -- me method [diff,integration] -- end";
404 "----------- autoCalculate [diff,integration] -----------";
405 "----------- autoCalculate [diff,integration] -----------";
406 "----------- autoCalculate [diff,integration] -----------";
409 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
410 ("Integrate", ["integrate","function"], ["diff","integration"]))];
413 autoCalculate 1 CompleteCalc;
414 val ((pt,p),_) = get_calc 1; @{make_string} p; show_pt pt;
415 val (Form t,_,_) = pt_extract (pt, p);
416 if UnparseC.term t = "c + x + 1 / 3 * x ^^^ 3" then ()
417 else error "integrate.sml -- interSteps [diff,integration] -- result";
420 "----------- me method [diff,integration,named] ---------";
421 "----------- me method [diff,integration,named] ---------";
422 "----------- me method [diff,integration,named] ---------";
423 (*exp_CalcInt_No-2.xml*)
424 val fmz = ["functionTerm (x^^^2 + (1::real))",
425 "integrateBy x","antiDerivativeName F"];
427 ("Integrate",["named","integrate","function"],
428 ["diff","integration","named"]);
429 val p = e_pos'; val c = [];
430 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
431 val (p,_,f,nxt,_,pt) = me nxt p c pt;
432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
433 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
434 val (p,_,f,nxt,_,pt) = me nxt p c pt;
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 val (p,_,f,nxt,_,pt) = me nxt p c pt;
437 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
438 val (p,_,f,nxt,_,pt) = me nxt p c pt;
439 val (p,_,f,nxt,_,pt) = me nxt p c pt;
440 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
441 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
442 else error "integrate.sml: method [diff,integration,named]";
445 "----------- me met [diff,integration,named] Biegelinie.Q";
446 "----------- me met [diff,integration,named] Biegelinie.Q";
447 "----------- me met [diff,integration,named] Biegelinie.Q";
448 (*exp_CalcInt_No-3.xml*)
449 val fmz = ["functionTerm (- q_0)",
450 "integrateBy x","antiDerivativeName Q"];
452 ("Biegelinie",["named","integrate","function"],
453 ["diff","integration","named"]);
454 val p = e_pos'; val c = [];
455 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
456 val (p,_,f,nxt,_,pt) = me nxt p c pt;
457 val (p,_,f,nxt,_,pt) = me nxt p c pt;
458 (*Error Tac Q not in ...*)
459 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
460 val (p,_,f,nxt,_,pt) = me nxt p c pt;
461 val (p,_,f,nxt,_,pt) = me nxt p c pt;
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
464 val (p,_,f,nxt,_,pt) = me nxt p c pt;
465 val (p,_,f,nxt,_,pt) = me nxt p c pt;
466 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
468 if f2str f = "Q x = c + -1 * q_0 * x" then()
469 else error "integrate.sml: method [diff,integration,named] .Q";