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 "----------- check Scripts ------------------------------";
16 "----------- me method [diff,integration] ---------------";
17 "----------- autoCalculate [diff,integration] -----------";
18 "----------- me method [diff,integration,named] ---------";
19 "----------- me met [diff,integration,named] Biegelinie.Q";
20 "----------- interSteps [diff,integration] --------------";
21 "----------- method analog to rls 'integration' ---------";
22 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
23 "----------- CAS input ----------------------------------";
24 "--------------------------------------------------------";
25 "--------------------------------------------------------";
26 "--------------------------------------------------------";
28 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
29 they are used several times below; TODO remove duplicates*)
30 val thy = @{theory "Integrate"};
31 val ctxt = thy2ctxt thy;
33 fun str2t str = parseNEW ctxt str |> the;
34 fun term2s t = term_to_string' ctxt t;
36 val conditions_in_integration_rules =
37 Rls {id="conditions_in_integration_rules",
39 rew_ord = ("termlessI",termlessI),
41 srls = Erls, calc = [], errpatts = [],
42 rules = [(*for rewriting conditions in Thm's*)
43 Calc ("Prog_Expr.occurs'_in",
44 eval_occurs_in "#occurs_in_"),
45 Thm ("not_true",num_str @{thm not_true}),
46 Thm ("not_false",num_str @{thm not_false})],
48 val subs = [(str2t "bdv::real", str2t "x::real")];
50 fst (the (rewrite_inst_ thy tless_true
51 conditions_in_integration_rules
55 "----------- parsing ------------------------------------";
56 "----------- parsing ------------------------------------";
57 "----------- parsing ------------------------------------";
58 val t = str2t "Integral x D x";
59 val t = str2t "Integral x^^^2 D x";
61 Const ("Integrate.Integral", _) $
62 (Const ("Prog_Expr.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
63 | _ => error "integrate.sml: parsing: Integral x^^^2 D x";
65 val t = str2t "ff x is_f_x";
66 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
67 | _ => error "integrate.sml: parsing: ff x is_f_x";
70 "----------- integrate by rewriting ---------------------";
71 "----------- integrate by rewriting ---------------------";
72 "----------- integrate by rewriting ---------------------";
73 val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
74 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
76 val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
77 if term2s str = "M' / EJ * x" then ()
78 else error "Integral M'/EJ D x BY integral_const";
80 val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
81 if term2s str = "x ^^^ 2 / 2" then ()
82 else error "Integral x D x BY integral_var";
84 val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
85 if term2s str = "Integral x D x + Integral 1 D x" then ()
86 else error "Integral x + 1 D x BY integral_add";
88 val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");
89 if term2s str = "M' / EJ * Integral x ^^^ 3 D x" then ()
90 else error "Integral M'/EJ * x^^^3 D x BY integral_mult";
92 val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");
93 if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()
94 else error "integrate.sml Integral x^^^3 D x";
97 "----------- test add_new_c, is_f_x ---------------------";
98 "----------- test add_new_c, is_f_x ---------------------";
99 "----------- test add_new_c, is_f_x ---------------------";
100 val term = str2t "x^^^2 * c + c_2";
102 if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";
104 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
105 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
106 else error "intergrate.sml: diff. eval_add_new_c";
108 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
109 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
111 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
112 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
113 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
115 val term = str2t "ff x = x^^^2*c + c_2";
116 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
117 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
118 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
121 (*WN080222 replace call_new_c with add_new_c----------------------
122 val term = str2t "new_c (c * x^^^2 + c_2)";
123 val SOME (_,t') = eval_new_c 0 0 term 0;
124 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
125 else error "integrate.sml: eval_new_c ???";
127 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
128 val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
129 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
130 else error "integrate.sml: matches new_c = False";
132 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
133 val SOME (_,t') = eval_matches "" "Prog_Expr.matches" t thy; term2s t';
134 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
135 then () else error "integrate.sml: matches new_c = True";
137 val t = str2t "ff x is_f_x";
138 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
139 if term2s t' = "(ff x is_f_x) = True" then ()
140 else error "integrate.sml: eval_is_f_x --> true";
142 val t = str2t "q_0/2 * L * x is_f_x";
143 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
144 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
145 else error "integrate.sml: eval_is_f_x --> false";
147 val conditions_in_integration =
148 Rls {id="conditions_in_integration",
150 rew_ord = ("termlessI",termlessI),
152 srls = Erls, calc = [], errpatts = [],
153 rules = [Calc ("Prog_Expr.matches",eval_matches ""),
154 Calc ("Integrate.is'_f'_x",
155 eval_is_f_x "is_f_x_"),
156 Thm ("not_true",num_str @{thm not_true}),
157 Thm ("not_false",num_str @{thm not_false})
161 fst (the (rewrite_inst_ thy tless_true
162 conditions_in_integration true subs thm t));
163 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
164 val t = (rewrit call_for_new_c t)
165 handle OPTION => str2t "no_rewrite";
167 val t = rewrit call_for_new_c
168 (str2t "ff x = q_0/2 *L*x"); term2s t;
169 val t = (rewrit call_for_new_c
170 (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
171 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
172 --------------------------------------------------------------------*)
175 "----------- simplify by ruleset reducing make_ratpoly_in";
176 "----------- simplify by ruleset reducing make_ratpoly_in";
177 "----------- simplify by ruleset reducing make_ratpoly_in";
178 val thy = @{theory "Isac_Knowledge"};
180 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
182 "----- stepwise from the rulesets in simplify_Integral and below-----";
183 val rls = norm_Rational_noadd_fractions;
184 case rewrite_set_inst_ thy true subs rls t of
185 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
189 val rls = order_add_mult_in;
190 val SOME (t,[]) = rewrite_set_ thy true rls t;
191 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
192 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
195 val rls = discard_parentheses;
196 val SOME (t,[]) = rewrite_set_ thy true rls t;
197 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
198 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
201 val subs = [(str2t "bdv::real", str2t "x::real")];
203 (append_rls "separate_bdv" collect_bdv
204 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
205 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
206 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
207 (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
208 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
209 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
210 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
211 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
213 (*show_types := true; --- do we need type-constraint in thms? *)
214 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
215 @{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
216 @{thm separate_1_bdv}; (*::?'a*)
217 val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
218 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
219 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
221 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
222 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
223 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
226 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
227 val rls = simplify_Integral;
228 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
229 (* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
230 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
231 else error "integrate.sml, simplify_Integral #99";
233 "........... 2nd integral ........................................";
234 "........... 2nd integral ........................................";
235 "........... 2nd integral ........................................";
237 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
238 val rls = simplify_Integral;
239 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
241 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
242 then () else raise error "integrate.sml, simplify_Integral #198";
244 val rls = integration_rules;
245 val SOME (t,[]) = rewrite_set_ thy true rls t;
248 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
249 then () else error "integrate.sml, simplify_Integral #199";
252 "----------- integrate by ruleset -----------------------";
253 "----------- integrate by ruleset -----------------------";
254 "----------- integrate by ruleset -----------------------";
255 val thy = @{theory "Integrate"};
256 val rls = integration_rules;
257 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
258 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
260 val t = (Thm.term_of o the o (parse thy)) "Integral x D x";
261 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
262 if term2str res = "x ^^^ 2 / 2" then () else error "Integral x D x changed";
264 val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
265 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
266 if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x" then () else error "Integral c * x ^^^ 2 + c_2 D x";
269 val t = (Thm.term_of o the o (parse thy)) "c * (x ^^^ 3 / 3) + c_2 * x";
270 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
271 if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
272 else error "integrate.sml: diff.behav. in add_new_c simpl.";
274 val t = (Thm.term_of o the o (parse thy)) "F x = x ^^^ 3 / 3 + x";
275 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
276 if term2str res = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
277 else error "integrate.sml: diff.behav. in add_new_c equation";
279 val rls = simplify_Integral;
280 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
281 val t = (Thm.term_of o the o (parse thy)) "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
282 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
283 if term2str res = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
284 then () else error "integrate.sml: diff.behav. in simplify_I #1";
286 val rls = integration;
287 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
288 val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
289 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
290 if term2str res = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
291 then () else error "integrate.sml: diff.behav. in integration #1";
293 val t = (Thm.term_of o the o (parse thy)) "Integral 3*x^^^2 + 2*x + 1 D x";
294 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
295 if term2str res = "c + x + x ^^^ 2 + x ^^^ 3" then ()
296 else error "integrate.sml: diff.behav. in integration #2";
298 val t = (Thm.term_of o the o (parse thy))
299 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
300 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
301 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
302 if term2str res = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
303 then () else error "integrate.sml: diff.behav. in integration #3";
305 val t = (Thm.term_of o the o (parse thy)) ("Integral " ^ term2str res ^ " D x");
306 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
307 if term2str res = "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
308 then () else error "integrate.sml: diff.behav. in integration #4";
310 "----------- rewrite 3rd integration in 7.27 ------------";
311 "----------- rewrite 3rd integration in 7.27 ------------";
312 "----------- rewrite 3rd integration in 7.27 ------------";
313 val thy = @{theory "Isac_Knowledge"} (*because of Undeclared constant "Biegelinie.EI*);
314 val t = str2t "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
315 val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;
317 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
318 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
320 val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
323 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
324 then () else error "integrate.sml 3rd integration in 7.27, integration";
327 "----------- check probem type --------------------------";
328 "----------- check probem type --------------------------";
329 "----------- check probem type --------------------------";
330 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
332 Find =["antiDerivative F_F"],
334 Relate=[]}:string ppc;
335 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
336 val t1 = (Thm.term_of o hd) chkmodel;
337 val t2 = (Thm.term_of o hd o tl) chkmodel;
338 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
339 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
340 | _ => error "integrate.sml: Integrate.antiDerivative ???";
342 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
344 Find =["antiDerivativeName F_F"],
346 Relate=[]}:string ppc;
347 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
348 val t1 = (Thm.term_of o hd) chkmodel;
349 val t2 = (Thm.term_of o hd o tl) chkmodel;
350 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
351 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
352 | _ => error "integrate.sml: Integrate.antiDerivativeName";
354 "----- compare 'Find's from problem, script, formalization -------";
355 val {ppc,...} = get_pbt ["named","integrate","function"];
356 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
357 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
358 val {scr = Prog sc,... } = get_met ["diff","integration","named"];
359 val [_,_, F2_] = formal_args sc;
360 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
362 val ((dsc as Const ("Integrate.antiDerivativeName", _))
363 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
364 if is_dsc dsc then () else error "integrate.sml: no description";
365 if F1_type = F3_type then ()
366 else error "integrate.sml: unequal types in find's";
369 val pbl = get_pbt ["integrate","function"];
370 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
371 | _ => error "integrate.sml: Integrate.Integrate ???";
374 "----------- check Scripts ------------------------------";
375 "----------- check Scripts ------------------------------";
376 "----------- check Scripts ------------------------------";
378 "Program IntegrationScript (f_f::real) (v_v::real) = \
379 \ (let t_t = Take (Integral f_f D v_v) \
380 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) (t_t::real))";
381 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
385 "Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
386 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
387 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration) t_t)";
388 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
393 "----------- me method [diff,integration] ---------------";
394 "----------- me method [diff,integration] ---------------";
395 "----------- me method [diff,integration] ---------------";
396 (*exp_CalcInt_No-1.xml*)
397 val p = e_pos'; val c = [];
398 "----- step 0: returns nxt = Model_Problem ---";
399 val (p,_,f,nxt,_,pt) =
401 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
402 ("Integrate", ["integrate","function"], ["diff","integration"]))];
403 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
404 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
405 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
406 val (p,_,f,nxt,_,pt) = me nxt p c pt;
407 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
408 val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
410 val (p,_,f,nxt,_,pt) = me nxt p c pt;
411 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
412 val (p,_,f,nxt,_,pt) = me nxt p c pt;
413 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
414 val (p,_,f,nxt,_,pt) = me nxt p c pt;
415 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
416 val (p,_,f,nxt,_,pt) = me nxt p c pt;
417 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
418 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
419 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
420 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
421 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
422 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
423 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
424 else error "integrate.sml -- me method [diff,integration] -- end";
427 "----------- autoCalculate [diff,integration] -----------";
428 "----------- autoCalculate [diff,integration] -----------";
429 "----------- autoCalculate [diff,integration] -----------";
432 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
433 ("Integrate", ["integrate","function"], ["diff","integration"]))];
436 autoCalculate 1 CompleteCalc;
437 val ((pt,p),_) = get_calc 1; @{make_string} p; show_pt pt;
438 val (Form t,_,_) = pt_extract (pt, p);
439 if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
440 else error "integrate.sml -- interSteps [diff,integration] -- result";
443 "----------- me method [diff,integration,named] ---------";
444 "----------- me method [diff,integration,named] ---------";
445 "----------- me method [diff,integration,named] ---------";
446 (*exp_CalcInt_No-2.xml*)
447 val fmz = ["functionTerm (x^^^2 + (1::real))",
448 "integrateBy x","antiDerivativeName F"];
450 ("Integrate",["named","integrate","function"],
451 ["diff","integration","named"]);
452 val p = e_pos'; val c = [];
453 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
454 val (p,_,f,nxt,_,pt) = me nxt p c pt;
455 val (p,_,f,nxt,_,pt) = me nxt p c pt;
456 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
457 val (p,_,f,nxt,_,pt) = me nxt p c pt;
458 val (p,_,f,nxt,_,pt) = me nxt p c pt;
459 val (p,_,f,nxt,_,pt) = me nxt p c pt;
460 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
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; f2str f;
464 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
465 else error "integrate.sml: method [diff,integration,named]";
468 "----------- me met [diff,integration,named] Biegelinie.Q";
469 "----------- me met [diff,integration,named] Biegelinie.Q";
470 "----------- me met [diff,integration,named] Biegelinie.Q";
471 (*exp_CalcInt_No-3.xml*)
472 val fmz = ["functionTerm (- q_0)",
473 "integrateBy x","antiDerivativeName Q"];
475 ("Biegelinie",["named","integrate","function"],
476 ["diff","integration","named"]);
477 val p = e_pos'; val c = [];
478 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
479 val (p,_,f,nxt,_,pt) = me nxt p c pt;
480 val (p,_,f,nxt,_,pt) = me nxt p c pt;
481 (*Error Tac Q not in ...*)
482 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
483 val (p,_,f,nxt,_,pt) = me nxt p c pt;
484 val (p,_,f,nxt,_,pt) = me nxt p c pt;
485 val (p,_,f,nxt,_,pt) = me nxt p c pt;
486 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
487 val (p,_,f,nxt,_,pt) = me nxt p c pt;
488 val (p,_,f,nxt,_,pt) = me nxt p c pt;
489 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
491 if f2str f = "Q x = c + -1 * q_0 * x" then()
492 else error "integrate.sml: method [diff,integration,named] .Q";
495 "----------- interSteps [diff,integration] --------------";
496 "----------- interSteps [diff,integration] --------------";
497 "----------- interSteps [diff,integration] --------------";
500 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
501 ("Integrate", ["integrate","function"], ["diff","integration"]))];
504 autoCalculate 1 CompleteCalc;
505 interSteps 1 ([1],Res);
506 val ((pt,p),_) = get_calc 1; show_pt pt;
507 if existpt' ([1,3], Res) pt then ()
508 else error "integrate.sml: interSteps on Rewrite_Set_Inst";
513 [(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],
514 ("Integrate", ["integrate","function"], ["diff","integration","test"]))];
517 autoCalculate 1 CompleteCalcHead;
519 fetchProposedTactic 1 (*..Apply_Method*);
520 autoCalculate 1 (Step 1);
521 getTactic 1 ([1], Frm) (*still empty*);
523 fetchProposedTactic 1 (*Rewrite_Set_Inst ''integration_rules''*);
524 autoCalculate 1 (Step 1);
526 fetchProposedTactic 1 (*Rewrite_Set_Inst ''add_new_c''*);
527 autoCalculate 1 (Step 1);
529 fetchProposedTactic 1 (*Rewrite_Set_Inst ''simplify_Integral''*);
530 autoCalculate 1 (Step 1);
532 autoCalculate 1 CompleteCalc;
533 val ((pt,p),_) = get_calc 1; show_pt pt;
534 val (Form t,_,_) = pt_extract (pt, p); term2str t;
535 if existpt' ([3], Res) pt andalso term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
536 else error "integrate.sml: test-script doesnt work";
539 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
540 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
541 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
544 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
545 ("Integrate",["integrate","function"],
546 ["diff","integration"]))];
549 autoCalculate 1 CompleteCalc;
550 val ((pt,p),_) = get_calc 1; show_pt pt;
551 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3"
552 then () else error "Ambiguous input: Integral ?u + ?v D ?bdv ="
554 interSteps 1 ([1],Res);
555 val ((pt,p),_) = get_calc 1; show_pt pt;
556 interSteps 1 ([1,1],Res);
557 val ((pt,p),_) = get_calc 1; show_pt pt;
558 (*getTactic 1 ([1,1,1],Frm); TODO.WN111207 kind of error unclear:
563 <ERROR> syserror in getTactic </ERROR>
567 val str = (unenclose o Thm.get_name_hint) @{thm integral_add};
568 str = "ntegrate.integral_ad"; (*WN111207 begin+end cut off*)
570 (*WN111207 was outcommented already:
571 read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
573 *** More than one term is type correct:
574 *** ((Integral (?u + ?v) D ?bdv) =
575 *** (Integral ?u D (?bdv + (Integral ?v D ?bdv))))
577 *** ((Integral (?u + ?v) D ?bdv) =
578 *** ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
581 (*============ inhibit exn WN120314 ==============================================
582 (*??? WN111205: this check succeeds erratically : asyncronous Isar/jEdit ???*)
583 if existpt' ([1,1,5], Res) pt then ()
584 else error "integrate.sml: interSteps on Rewrite_Set_Inst 2 ERRATICAL???";
585 ============ inhibit exn WN120314 ==============================================*)
588 "----------- CAS input ----------------------------------";
589 "----------- CAS input ----------------------------------";
590 "----------- CAS input ----------------------------------";
591 val t = str2t "Integrate (x^^^2 + x + 1, x)";
592 case t of Const ("Integrate.Integrate", _) $ _ => ()
593 | _ => error "diff.sml behav.changed for Integrate (..., x)";
597 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
600 replaceFormula 1 "Integrate (x^2 + x + 1, x)";
601 autoCalculate 1 CompleteCalc;
602 val ((pt,p),_) = get_calc 1;
603 val Form res = (#1 o pt_extract) (pt, ([],Res));
606 WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version
607 from 2007; not touched since then.
609 WN070703 does not work like Diff due to error in next-pos
610 if p = ([], Res) andalso term2str res = "5 * a" then ()
611 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";