1 (* tests on integration over the reals
2 author: Walther Neuper 2005
3 (c) due to copyright terms
5 trace_rewrite := false;
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- parsing ------------------------------------";
10 "----------- integrate by rewriting ---------------------";
11 "----------- test add_new_c, is_f_x ---------------------";
12 "----------- simplify by ruleset reducing make_ratpoly_in";
13 "----------- integrate by ruleset -----------------------";
14 "----------- rewrite 3rd integration in 7.27 ------------";
15 "----------- check probem type --------------------------";
16 "----------- check Scripts ------------------------------";
17 "----------- me method [diff,integration] ---------------";
18 "----------- autoCalculate [diff,integration] -----------";
19 "----------- me method [diff,integration,named] ---------";
20 "----------- me met [diff,integration,named] Biegelinie.Q";
21 "----------- interSteps [diff,integration] --------------";
22 "----------- method analog to rls 'integration' ---------";
23 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
24 "----------- CAS input ----------------------------------";
25 "--------------------------------------------------------";
26 "--------------------------------------------------------";
27 "--------------------------------------------------------";
29 (*these val/fun provide for exact parsing in Integrate.thy, not Isac.thy;
30 they are used several times below; TODO remove duplicates*)
31 val thy = @{theory "Integrate"};
32 val ctxt = thy2ctxt thy;
34 fun str2t str = parseNEW ctxt str |> the;
35 fun term2s t = term_to_string' ctxt t;
37 val conditions_in_integration_rules =
38 Rls {id="conditions_in_integration_rules",
40 rew_ord = ("termlessI",termlessI),
42 srls = Erls, calc = [], errpatts = [],
43 rules = [(*for rewriting conditions in Thm's*)
44 Calc ("Atools.occurs'_in",
45 eval_occurs_in "#occurs_in_"),
46 Thm ("not_true",num_str @{thm not_true}),
47 Thm ("not_false",num_str @{thm not_false})],
49 val subs = [(str2t "bdv::real", str2t "x::real")];
51 fst (the (rewrite_inst_ thy tless_true
52 conditions_in_integration_rules
56 "----------- parsing ------------------------------------";
57 "----------- parsing ------------------------------------";
58 "----------- parsing ------------------------------------";
59 val t = str2t "Integral x D x";
60 val t = str2t "Integral x^^^2 D x";
62 Const ("Integrate.Integral", _) $
63 (Const ("Atools.pow", _) $ Free _ $ Free _) $ Free ("x", _) => ()
64 | _ => error "integrate.sml: parsing: Integral x^^^2 D x";
66 val t = str2t "ff x is_f_x";
67 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
68 | _ => error "integrate.sml: parsing: ff x is_f_x";
71 "----------- integrate by rewriting ---------------------";
72 "----------- integrate by rewriting ---------------------";
73 "----------- integrate by rewriting ---------------------";
74 val str = rewrit @{thm "integral_const"} (str2t "Integral 1 D x");
75 if term2s str = "1 * x" then () else error "integrate.sml Integral 1 D x";
77 val str = rewrit @{thm "integral_const"} (str2t "Integral M'/EJ D x");
78 if term2s str = "M' / EJ * x" then ()
79 else error "Integral M'/EJ D x BY integral_const";
81 val str = rewrit @{thm "integral_var"} (str2t "Integral x D x");
82 if term2s str = "x ^^^ 2 / 2" then ()
83 else error "Integral x D x BY integral_var";
85 val str = rewrit @{thm "integral_add"} (str2t "Integral x + 1 D x");
86 if term2s str = "Integral x D x + Integral 1 D x" then ()
87 else error "Integral x + 1 D x BY integral_add";
89 val str = rewrit @{thm "integral_mult"} (str2t "Integral M'/EJ * x^^^3 D x");
90 if term2s str = "M' / EJ * Integral x ^^^ 3 D x" then ()
91 else error "Integral M'/EJ * x^^^3 D x BY integral_mult";
93 val str = rewrit @{thm "integral_pow"} (str2t "Integral x^^^3 D x");
94 if term2s str = "x ^^^ (3 + 1) / (3 + 1)" then ()
95 else error "integrate.sml Integral x^^^3 D x";
98 "----------- test add_new_c, is_f_x ---------------------";
99 "----------- test add_new_c, is_f_x ---------------------";
100 "----------- test add_new_c, is_f_x ---------------------";
101 val term = str2t "x^^^2 * c + c_2";
103 if term2str cc = "c_3" then () else error "integrate.sml: new_c ???";
105 val SOME (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
106 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
107 else error "intergrate.sml: diff. eval_add_new_c";
109 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
110 val SOME (thmstr, thm) = adhoc_thm1_ thy cc term;
112 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
113 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
114 else error "intergrate.sml: diff. rewrite_set add_new_c 1";
116 val term = str2t "ff x = x^^^2*c + c_2";
117 val SOME (t',_) = rewrite_set_ thy true add_new_c term;
118 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
119 else error "intergrate.sml: diff. rewrite_set add_new_c 2";
122 (*WN080222 replace call_new_c with add_new_c----------------------
123 val term = str2t "new_c (c * x^^^2 + c_2)";
124 val SOME (_,t') = eval_new_c 0 0 term 0;
125 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
126 else error "integrate.sml: eval_new_c ???";
128 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
129 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
130 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
131 else error "integrate.sml: matches new_c = False";
133 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
134 val SOME (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
135 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
136 then () else error "integrate.sml: matches new_c = True";
138 val t = str2t "ff x is_f_x";
139 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
140 if term2s t' = "(ff x is_f_x) = True" then ()
141 else error "integrate.sml: eval_is_f_x --> true";
143 val t = str2t "q_0/2 * L * x is_f_x";
144 val SOME (_,t') = eval_is_f_x "" "" t thy; term2s t';
145 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
146 else error "integrate.sml: eval_is_f_x --> false";
148 val conditions_in_integration =
149 Rls {id="conditions_in_integration",
151 rew_ord = ("termlessI",termlessI),
153 srls = Erls, calc = [], errpatts = [],
154 rules = [Calc ("Tools.matches",eval_matches ""),
155 Calc ("Integrate.is'_f'_x",
156 eval_is_f_x "is_f_x_"),
157 Thm ("not_true",num_str @{thm not_true}),
158 Thm ("not_false",num_str @{thm not_false})
162 fst (the (rewrite_inst_ thy tless_true
163 conditions_in_integration true subs thm t));
164 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
165 val t = (rewrit call_for_new_c t)
166 handle OPTION => str2t "no_rewrite";
168 val t = rewrit call_for_new_c
169 (str2t "ff x = q_0/2 *L*x"); term2s t;
170 val t = (rewrit call_for_new_c
171 (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
172 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
173 --------------------------------------------------------------------*)
176 "----------- simplify by ruleset reducing make_ratpoly_in";
177 "----------- simplify by ruleset reducing make_ratpoly_in";
178 "----------- simplify by ruleset reducing make_ratpoly_in";
179 val thy = @{theory "Isac"};
181 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
183 "----- stepwise from the rulesets in simplify_Integral and below-----";
184 val rls = norm_Rational_noadd_fractions;
185 case rewrite_set_inst_ thy true subs rls t of
186 SOME _ => error "integrate.sml simplify by ruleset norm_Rational_.#2"
190 val rls = order_add_mult_in;
191 val SOME (t,[]) = rewrite_set_ thy true rls t;
192 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)" then()
193 else error "integrate.sml simplify by ruleset order_add_mult_in #2";
196 val rls = discard_parentheses;
197 val SOME (t,[]) = rewrite_set_ thy true rls t;
198 if term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
199 else error "integrate.sml simplify by ruleset discard_parenth.. #3";
202 val subs = [(str2t "bdv::real", str2t "x::real")];
204 (append_rls "separate_bdv" collect_bdv
205 [Thm ("separate_bdv", num_str @{thm separate_bdv}),
206 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
207 Thm ("separate_bdv_n", num_str @{thm separate_bdv_n}),
208 (*"?a * ?bdv ^^^ ?n / ?b = ?a / ?b * ?bdv ^^^ ?n"*)
209 Thm ("separate_1_bdv", num_str @{thm separate_1_bdv}),
210 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
211 Thm ("separate_1_bdv_n", num_str @{thm separate_1_bdv_n})
212 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
214 (*show_types := true; --- do we need type-constraint in thms? *)
215 @{thm separate_bdv}; (*::?'a does NOT rewrite here WITHOUT type constraint*)
216 @{thm separate_bdv_n}; (*::real ..because of ^^^, rewrites*)
217 @{thm separate_1_bdv}; (*::?'a*)
218 val xxx = num_str @{thm separate_1_bdv}; (*::?'a*)
219 @{thm separate_1_bdv_n}; (*::real ..because of ^^^*)
220 (*show_types := false; --- do we need type-constraint in thms? YES ?!?!?!*)
222 val SOME (t, []) = rewrite_set_inst_ thy true subs rls t;
223 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
224 else error "integrate.sml simplify by ruleset separate_bdv.. #4";
227 val t = str2t "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
228 val rls = simplify_Integral;
229 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
230 (* given was: "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)" *)
231 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
232 else error "integrate.sml, simplify_Integral #99";
234 "........... 2nd integral ........................................";
235 "........... 2nd integral ........................................";
236 "........... 2nd integral ........................................";
238 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + -1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
239 val rls = simplify_Integral;
240 val SOME (t,[]) = rewrite_set_inst_ thy true subs rls t;
242 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
243 then () else raise error "integrate.sml, simplify_Integral #198";
245 val rls = integration_rules;
246 val SOME (t,[]) = rewrite_set_ thy true rls t;
249 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
250 then () else error "integrate.sml, simplify_Integral #199";
253 "----------- integrate by ruleset -----------------------";
254 "----------- integrate by ruleset -----------------------";
255 "----------- integrate by ruleset -----------------------";
256 val thy = @{theory "Integrate"};
257 val rls = integration_rules;
258 val subs = [(@{term "bdv::real"}, @{term "x::real"})];
259 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
261 val t = (Thm.term_of o the o (parse thy)) "Integral x D x";
262 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
263 if term2str res = "x ^^^ 2 / 2" then () else error "Integral x D x changed";
265 val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
266 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
267 if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x" then () else error "Integral c * x ^^^ 2 + c_2 D x";
270 val t = (Thm.term_of o the o (parse thy)) "c * (x ^^^ 3 / 3) + c_2 * x";
271 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
272 if term2str res = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
273 else error "integrate.sml: diff.behav. in add_new_c simpl.";
275 val t = (Thm.term_of o the o (parse thy)) "F x = x ^^^ 3 / 3 + x";
276 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
277 if term2str res = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
278 else error "integrate.sml: diff.behav. in add_new_c equation";
280 val rls = simplify_Integral;
281 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
282 val t = (Thm.term_of o the o (parse thy)) "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
283 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
284 if term2str res = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
285 then () else error "integrate.sml: diff.behav. in simplify_I #1";
287 val rls = integration;
288 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
289 val t = (Thm.term_of o the o (parse thy)) "Integral c * x ^^^ 2 + c_2 D x";
290 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
291 if term2str res = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
292 then () else error "integrate.sml: diff.behav. in integration #1";
294 val t = (Thm.term_of o the o (parse thy)) "Integral 3*x^^^2 + 2*x + 1 D x";
295 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
296 if term2str res = "c + x + x ^^^ 2 + x ^^^ 3" then ()
297 else error "integrate.sml: diff.behav. in integration #2";
299 val t = (Thm.term_of o the o (parse thy))
300 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
301 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
302 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
303 if term2str res = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
304 then () else error "integrate.sml: diff.behav. in integration #3";
306 val t = (Thm.term_of o the o (parse thy)) ("Integral " ^ term2str res ^ " D x");
307 val SOME (res, _) = rewrite_set_inst_ thy true subs rls t;
308 if term2str res = "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
309 then () else error "integrate.sml: diff.behav. in integration #4";
311 "----------- rewrite 3rd integration in 7.27 ------------";
312 "----------- rewrite 3rd integration in 7.27 ------------";
313 "----------- rewrite 3rd integration in 7.27 ------------";
314 val thy = @{theory "Isac"} (*because of Undeclared constant "Biegelinie.EI*);
315 val t = str2t "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
316 val SOME(t,_)= rewrite_set_inst_ thy true subs simplify_Integral t;
318 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x"
319 then () else error "integrate.sml 3rd integration in 7.27, simplify_Integral";
321 val SOME(t,_)= rewrite_set_inst_ thy true subs integration t;
324 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
325 then () else error "integrate.sml 3rd integration in 7.27, integration";
328 "----------- check probem type --------------------------";
329 "----------- check probem type --------------------------";
330 "----------- check probem type --------------------------";
331 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
333 Find =["antiDerivative F_F"],
335 Relate=[]}:string ppc;
336 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
337 val t1 = (Thm.term_of o hd) chkmodel;
338 val t2 = (Thm.term_of o hd o tl) chkmodel;
339 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
340 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
341 | _ => error "integrate.sml: Integrate.antiDerivative ???";
343 val model = {Given =["functionTerm f_f", "integrateBy v_v"],
345 Find =["antiDerivativeName F_F"],
347 Relate=[]}:string ppc;
348 val chkmodel = ((map (the o (parse thy))) o ppc2list) model;
349 val t1 = (Thm.term_of o hd) chkmodel;
350 val t2 = (Thm.term_of o hd o tl) chkmodel;
351 val t3 = (Thm.term_of o hd o tl o tl) chkmodel;
352 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
353 | _ => error "integrate.sml: Integrate.antiDerivativeName";
355 "----- compare 'Find's from problem, script, formalization -------";
356 val {ppc,...} = get_pbt ["named","integrate","function"];
357 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
358 F1_ as Free ("F_F", F1_type))) = last_elem ppc;
359 val {scr = Prog sc,... } = get_met ["diff","integration","named"];
360 val [_,_, F2_] = formal_args sc;
361 if F1_ = F2_ then () else error "integrate.sml: unequal find's";
363 val ((dsc as Const ("Integrate.antiDerivativeName", _))
364 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
365 if is_dsc dsc then () else error "integrate.sml: no description";
366 if F1_type = F3_type then ()
367 else error "integrate.sml: unequal types in find's";
370 val pbl = get_pbt ["integrate","function"];
371 case #cas pbl of SOME (Const ("Integrate.Integrate",_) $ _) => ()
372 | _ => error "integrate.sml: Integrate.Integrate ???";
375 "----------- check Scripts ------------------------------";
376 "----------- check Scripts ------------------------------";
377 "----------- check Scripts ------------------------------";
379 "Program IntegrationScript (f_f::real) (v_v::real) = \
380 \ (let t_t = Take (Integral f_f D v_v) \
381 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) (t_t::real))";
382 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
386 "Program NamedIntegrationScript (f_f::real) (v_v::real) (F_F::real=>real) = \
387 \ (let t_t = Take (F_F v_v = Integral f_f D v_v) \
388 \ in (Rewrite_Set_Inst [(''bdv'',v_v)] integration False) t_t)";
389 val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
394 "----------- me method [diff,integration] ---------------";
395 "----------- me method [diff,integration] ---------------";
396 "----------- me method [diff,integration] ---------------";
397 (*exp_CalcInt_No-1.xml*)
398 val p = e_pos'; val c = [];
399 "----- step 0: returns nxt = Model_Problem ---";
400 val (p,_,f,nxt,_,pt) =
402 [(["functionTerm (x^^^2 + 1)", "integrateBy x", "antiDerivative FF"],
403 ("Integrate", ["integrate","function"], ["diff","integration"]))];
404 "----- step 1: returns nxt = Add_Given \"functionTerm (x ^^^ 2 + 1)\" ---";
405 val (p,_,f,nxt,_,pt) = me nxt p c pt; (*nxt = ("Tac ", ...) --> Add_Given...*)
406 "----- step 2: returns nxt = Add_Given \"integrateBy x\" ---";
407 val (p,_,f,nxt,_,pt) = me nxt p c pt;
408 "----- step 3: returns nxt = Add_Find \"Integrate.antiDerivative FF\" ---";
409 val (p,_,f,nxt,_,pt) = me nxt p c pt;
410 "----- step 4: returns nxt = Specify_Theory \"Integrate\" ---";
411 val (p,_,f,nxt,_,pt) = me nxt p c pt;
412 "----- step 5: returns nxt = Specify_Problem [\"integrate\", \"function\"] ---";
413 val (p,_,f,nxt,_,pt) = me nxt p c pt;
414 "----- step 6: returns nxt = Specify_Method [\"diff\", \"integration\"] ---";
415 val (p,_,f,nxt,_,pt) = me nxt p c pt;
416 "----- step 7: returns nxt = Apply_Method [\"diff\", \"integration\"] ---";
417 val (p,_,f,nxt,_,pt) = me nxt p c pt;
418 case nxt of (_, Apply_Method ["diff", "integration"]) => ()
419 | _ => error "integrate.sml -- me method [diff,integration] -- spec";
420 "----- step 8: returns nxt = Rewrite_Set_Inst ([\"(''bdv'', x)\"],\"integration\")";
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 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
424 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
425 else error "integrate.sml -- me method [diff,integration] -- end";
428 "----------- autoCalculate [diff,integration] -----------";
429 "----------- autoCalculate [diff,integration] -----------";
430 "----------- autoCalculate [diff,integration] -----------";
433 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
434 ("Integrate", ["integrate","function"], ["diff","integration"]))];
437 autoCalculate 1 CompleteCalc;
438 val ((pt,p),_) = get_calc 1; @{make_string} p; show_pt pt;
439 val (Form t,_,_) = pt_extract (pt, p);
440 if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
441 else error "integrate.sml -- interSteps [diff,integration] -- result";
444 "----------- me method [diff,integration,named] ---------";
445 "----------- me method [diff,integration,named] ---------";
446 "----------- me method [diff,integration,named] ---------";
447 (*exp_CalcInt_No-2.xml*)
448 val fmz = ["functionTerm (x^^^2 + (1::real))",
449 "integrateBy x","antiDerivativeName F"];
451 ("Integrate",["named","integrate","function"],
452 ["diff","integration","named"]);
453 val p = e_pos'; val c = [];
454 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
455 val (p,_,f,nxt,_,pt) = me nxt p c pt;
456 val (p,_,f,nxt,_,pt) = me nxt p c pt;
457 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
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;
461 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
462 val (p,_,f,nxt,_,pt) = me nxt p c pt;
463 val (p,_,f,nxt,_,pt) = me nxt p c pt;
464 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
465 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
466 else error "integrate.sml: method [diff,integration,named]";
469 "----------- me met [diff,integration,named] Biegelinie.Q";
470 "----------- me met [diff,integration,named] Biegelinie.Q";
471 "----------- me met [diff,integration,named] Biegelinie.Q";
472 (*exp_CalcInt_No-3.xml*)
473 val fmz = ["functionTerm (- q_0)",
474 "integrateBy x","antiDerivativeName Q"];
476 ("Biegelinie",["named","integrate","function"],
477 ["diff","integration","named"]);
478 val p = e_pos'; val c = [];
479 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
480 val (p,_,f,nxt,_,pt) = me nxt p c pt;
481 val (p,_,f,nxt,_,pt) = me nxt p c pt;
482 (*Error Tac Q not in ...*)
483 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
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;
487 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
488 val (p,_,f,nxt,_,pt) = me nxt p c pt;
489 val (p,_,f,nxt,_,pt) = me nxt p c pt;
490 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
492 if f2str f = "Q x = c + -1 * q_0 * x" then()
493 else error "integrate.sml: method [diff,integration,named] .Q";
496 "----------- interSteps [diff,integration] --------------";
497 "----------- interSteps [diff,integration] --------------";
498 "----------- interSteps [diff,integration] --------------";
501 [(["functionTerm (x^2 + 1)", "integrateBy x", "antiDerivative FF"],
502 ("Integrate", ["integrate","function"], ["diff","integration"]))];
505 autoCalculate 1 CompleteCalc;
506 interSteps 1 ([1],Res);
507 val ((pt,p),_) = get_calc 1; show_pt pt;
508 if existpt' ([1,3], Res) pt then ()
509 else error "integrate.sml: interSteps on Rewrite_Set_Inst";
514 [(["functionTerm (Integral x^2 + 1 D x)", "integrateBy x", "antiDerivative FF"],
515 ("Integrate", ["integrate","function"], ["diff","integration","test"]))];
518 autoCalculate 1 CompleteCalcHead;
520 fetchProposedTactic 1 (*..Apply_Method*);
521 autoCalculate 1 (Step 1);
522 getTactic 1 ([1], Frm) (*still empty*);
524 fetchProposedTactic 1 (*Rewrite_Set_Inst ''integration_rules''*);
525 autoCalculate 1 (Step 1);
527 fetchProposedTactic 1 (*Rewrite_Set_Inst ''add_new_c''*);
528 autoCalculate 1 (Step 1);
530 fetchProposedTactic 1 (*Rewrite_Set_Inst ''simplify_Integral''*);
531 autoCalculate 1 (Step 1);
533 autoCalculate 1 CompleteCalc;
534 val ((pt,p),_) = get_calc 1; show_pt pt;
535 val (Form t,_,_) = pt_extract (pt, p); term2str t;
536 if existpt' ([3], Res) pt andalso term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
537 else error "integrate.sml: test-script doesnt work";
540 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
541 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
542 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = .";
545 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
546 ("Integrate",["integrate","function"],
547 ["diff","integration"]))];
550 autoCalculate 1 CompleteCalc;
551 val ((pt,p),_) = get_calc 1; show_pt pt;
552 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "c + x + 1 / 3 * x ^^^ 3"
553 then () else error "Ambiguous input: Integral ?u + ?v D ?bdv ="
555 interSteps 1 ([1],Res);
556 val ((pt,p),_) = get_calc 1; show_pt pt;
557 interSteps 1 ([1,1],Res);
558 val ((pt,p),_) = get_calc 1; show_pt pt;
559 (*getTactic 1 ([1,1,1],Frm); TODO.WN111207 kind of error unclear:
564 <ERROR> syserror in getTactic </ERROR>
568 val str = (unenclose o Thm.get_name_hint) @{thm integral_add};
569 str = "ntegrate.integral_ad"; (*WN111207 begin+end cut off*)
571 (*WN111207 was outcommented already:
572 read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
574 *** More than one term is type correct:
575 *** ((Integral (?u + ?v) D ?bdv) =
576 *** (Integral ?u D (?bdv + (Integral ?v D ?bdv))))
578 *** ((Integral (?u + ?v) D ?bdv) =
579 *** ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
582 (*============ inhibit exn WN120314 ==============================================
583 (*??? WN111205: this check succeeds erratically : asyncronous Isar/jEdit ???*)
584 if existpt' ([1,1,5], Res) pt then ()
585 else error "integrate.sml: interSteps on Rewrite_Set_Inst 2 ERRATICAL???";
586 ============ inhibit exn WN120314 ==============================================*)
589 "----------- CAS input ----------------------------------";
590 "----------- CAS input ----------------------------------";
591 "----------- CAS input ----------------------------------";
592 val t = str2t "Integrate (x^^^2 + x + 1, x)";
593 case t of Const ("Integrate.Integrate", _) $ _ => ()
594 | _ => error "diff.sml behav.changed for Integrate (..., x)";
598 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
601 replaceFormula 1 "Integrate (x^2 + x + 1, x)";
602 autoCalculate 1 CompleteCalc;
603 val ((pt,p),_) = get_calc 1;
604 val Form res = (#1 o pt_extract) (pt, ([],Res));
607 WN101010 this test produced <SYSERROR>.."error in kernel" already in CVS-version
608 from 2007; not touched since then.
610 WN070703 does not work like Diff due to error in next-pos
611 if p = ([], Res) andalso term2str res = "5 * a" then ()
612 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";