1 (* tests on integration over the reals
4 (c) due to copyright terms
6 use"../smltest/IsacKnowledge/integrate.sml";
9 val thy = Integrate.thy;
11 "-----------------------------------------------------------------";
12 "table of contents -----------------------------------------------";
13 "-----------------------------------------------------------------";
14 "----------- parsing ---------------------------------------------";
15 "----------- integrate by rewriting ------------------------------";
16 "----------- test add_new_c, is_f_x ------------------------------";
17 "----------- simplify by ruleset reducing make_ratpoly_in --------";
18 "----------- simplify by ruleset extending make_polynomial_in ----";
19 "----------- integrate by ruleset --------------------------------";
20 "----------- rewrite 3rd integration in 7.27 ---------------------";
21 "----------- check probem type -----------------------------------";
22 "----------- check Scripts ---------------------------------------";
23 "----------- me method [diff,integration] ------------------------";
24 "----------- me method [diff,integration,named] ------------------";
25 "----------- me method [diff,integration,named] Biegelinie.Q -----";
26 "----------- interSteps [diff,integration] -----------------------";
27 "----------- method analog to rls 'integration' ------------------";
28 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
29 "----------- CAS input -------------------------------------------";
30 "-----------------------------------------------------------------";
31 "-----------------------------------------------------------------";
32 "-----------------------------------------------------------------";
36 "----------- parsing ---------------------------------------------";
37 "----------- parsing ---------------------------------------------";
38 "----------- parsing ---------------------------------------------";
39 fun str2t str = (term_of o the o (parse Integrate.thy)) str;
40 fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;
42 val t = str2t "Integral x D x";
43 val t = str2t "Integral x^^^2 D x";
46 val t = str2t "ff x is_f_x";
47 case t of Const ("Integrate.is'_f'_x", _) $ _ => ()
48 | _ => raise error "integrate.sml: parsing: ff x is_f_x";
51 "----------- integrate by rewriting ------------------------------";
52 "----------- integrate by rewriting ------------------------------";
53 "----------- integrate by rewriting ------------------------------";
54 val conditions_in_integration_rules =
55 Rls {id="conditions_in_integration_rules",
57 rew_ord = ("termlessI",termlessI),
59 srls = Erls, calc = [],
60 rules = [(*for rewriting conditions in Thm's*)
61 Calc ("Atools.occurs'_in",
62 eval_occurs_in "#occurs_in_"),
63 Thm ("not_true",num_str not_true),
64 Thm ("not_false",not_false)
67 val subs = [(str2t "bdv", str2t "x")];
69 fst (the (rewrite_inst_ Integrate.thy tless_true
70 conditions_in_integration_rules
72 val str = rewrit integral_const (str2t "Integral 1 D x"); term2s str;
73 val str = rewrit integral_const (str2t "Integral M'/EJ D x"); term2s str;
74 val str = (rewrit integral_const (str2t "Integral x D x"))
75 handle OPTION => str2t "no_rewrite";
77 val str = rewrit integral_var (str2t "Integral x D x"); term2s str;
78 val str = (rewrit integral_var (str2t "Integral a D x"))
79 handle OPTION => str2t "no_rewrite";
81 val str = rewrit integral_add (str2t "Integral x + 1 D x"); term2s str;
83 val str = rewrit integral_mult (str2t "Integral M'/EJ * x^^^3 D x");term2s str;
84 val str = (rewrit integral_mult (str2t "Integral x * x D x"))
85 handle OPTION => str2t "no_rewrite";
87 val str = rewrit integral_pow (str2t "Integral x^^^3 D x"); term2s str;
90 "----------- test add_new_c, is_f_x ------------------------------";
91 "----------- test add_new_c, is_f_x ------------------------------";
92 "----------- test add_new_c, is_f_x ------------------------------";
93 val term = str2term "x^^^2*c + c_2";
95 if term2str cc = "c_3" then () else raise error "integrate.sml: new_c ???";
97 val Some (id,t') = eval_add_new_c "" "Integrate.add'_new'_c" term thy;
98 if term2str t' = "x ^^^ 2 * c + c_2 = x ^^^ 2 * c + c_2 + c_3" then ()
99 else raise error "intergrate.sml: diff. eval_add_new_c";
101 val cc = ("Integrate.add'_new'_c", eval_add_new_c "add_new_c_");
102 val Some (thmstr, thm) = get_calculation1_ thy cc term;
104 val Some (t',_) = rewrite_set_ thy true add_new_c term;
105 if term2str t' = "x ^^^ 2 * c + c_2 + c_3" then ()
106 else raise error "intergrate.sml: diff. rewrite_set add_new_c 1";
108 val term = str2term "ff x = x^^^2*c + c_2";
109 val Some (t',_) = rewrite_set_ thy true add_new_c term;
110 if term2str t' = "ff x = x ^^^ 2 * c + c_2 + c_3" then ()
111 else raise error "intergrate.sml: diff. rewrite_set add_new_c 2";
114 (*WN080222 replace call_new_c with add_new_c----------------------
115 val term = str2t "new_c (c * x^^^2 + c_2)";
116 val Some (_,t') = eval_new_c 0 0 term 0;
117 if term2s t' = "new_c c * x ^^^ 2 + c_2 = c_3" then ()
118 else raise error "integrate.sml: eval_new_c ???";
120 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2)";
121 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
122 if term2s t' = "matches (?u + new_c ?v) (x ^^^ 2 / 2) = False" then ()
123 else raise error "integrate.sml: matches new_c = False";
125 val t = str2t "matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2)";
126 val Some (_,t') = eval_matches "" "Tools.matches" t thy; term2s t';
127 if term2s t'="matches (?u + new_c ?v) (x ^^^ 2 / 2 + new_c x ^^^ 2 / 2) = True"
128 then () else raise error "integrate.sml: matches new_c = True";
130 val t = str2t "ff x is_f_x";
131 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
132 if term2s t' = "(ff x is_f_x) = True" then ()
133 else raise error "integrate.sml: eval_is_f_x --> true";
135 val t = str2t "q_0/2 * L * x is_f_x";
136 val Some (_,t') = eval_is_f_x "" "" t thy; term2s t';
137 if term2s t' = "(q_0 / 2 * L * x is_f_x) = False" then ()
138 else raise error "integrate.sml: eval_is_f_x --> false";
140 val conditions_in_integration =
141 Rls {id="conditions_in_integration",
143 rew_ord = ("termlessI",termlessI),
145 srls = Erls, calc = [],
146 rules = [Calc ("Tools.matches",eval_matches ""),
147 Calc ("Integrate.is'_f'_x",
148 eval_is_f_x "is_f_x_"),
149 Thm ("not_true",num_str not_true),
150 Thm ("not_false",num_str not_false)
154 fst (the (rewrite_inst_ Integrate.thy tless_true
155 conditions_in_integration true subs thm t));
156 val t = rewrit call_for_new_c (str2t "x ^^^ 2 / 2"); term2s t;
157 val t = (rewrit call_for_new_c t)
158 handle OPTION => str2t "no_rewrite";
160 val t = rewrit call_for_new_c
161 (str2t "ff x = q_0/2 *L*x"); term2s t;
162 val t = (rewrit call_for_new_c
163 (str2t "ff x = q_0 / 2 * L * x + new_c q_0 / 2 * L * x"))
164 handle OPTION => (*NOT: + new_c ..=..!!*)str2t "no_rewrite";
165 --------------------------------------------------------------------*)
168 "----------- simplify by ruleset reducing make_ratpoly_in --------";
169 "----------- simplify by ruleset reducing make_ratpoly_in --------";
170 "----------- simplify by ruleset reducing make_ratpoly_in --------";
172 val subs = [(str2term"bdv",str2term"x")];
173 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
175 "----- stepwise from the rulesets in simplify_Integral and below-----";
176 (*###*)val rls = norm_Rational_noadd_fractions;
177 case rewrite_set_inst_ thy true subs rls t of
178 Some _ => raise error "integrate.sml simplify by ruleset norm_Rational_.#2"
180 (* WN051028 Rational.ML 'rat_mult_div_pow' with erls = e_rls
181 applies 'rat_mult_poly_r'="?c is_polyexp ==> ?a / ?b * ?c = ?a * ?c / ?b"
182 to "(L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2) / EI"
183 and keeps "..." is_polyexp" as an assumption.
184 AFTER CORRECTION in Integrate.ML as above*)
186 (*###*)val rls = order_add_mult_in;
187 val Some (t,[]) = rewrite_set_ thy true rls t;
188 if term2str t = "1 / EI * (L * (q_0 * x) / 2 + -1 * (q_0 * x ^^^ 2) / 2)"then()
189 else raise 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 term2str t = "1 / EI * (L * q_0 * x / 2 + -1 * q_0 * x ^^^ 2 / 2)" then ()
194 else raise error "integrate.sml simplify by ruleset discard_parenth.. #3";
197 (append_rls "separate_bdv"
199 [Thm ("separate_bdv", num_str separate_bdv),
200 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
201 Thm ("separate_bdv_n", num_str separate_bdv_n),
202 Thm ("separate_1_bdv", num_str separate_1_bdv),
203 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
204 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n)
206 val Some (t,[]) = rewrite_set_inst_ thy true subs rls t;
207 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
208 else raise error "integrate.sml simplify by ruleset separate_bdv.. #4";
211 val t = str2term "1/EI * (L * q_0 * x / 2 + -1 * q_0 * x^^^2 / 2)";
212 val rls = simplify_Integral;
213 val Some (t,[]) = rewrite_set_inst_ thy true subs rls t;
214 if term2str t = "1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2)" then ()
215 else raise error "integrate.sml, simplify_Integral #99";
217 "........... 2nd integral ........................................";
218 "........... 2nd integral ........................................";
219 "........... 2nd integral ........................................";
221 "Integral 1 / EI * (L * q_0 / 2 * (x ^^^ 2 / 2) + \
222 \-1 * q_0 / 2 * (x ^^^ 3 / 3)) D x";
223 val rls = simplify_Integral;
224 val Some (t,[]) = rewrite_set_inst_ thy true subs rls t;
226 "Integral 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3) D x"
227 then () else raise error "integrate.sml, simplify_Integral #198";
229 val rls = integration_rules;
230 val Some (t,[]) = rewrite_set_ thy true rls t;
232 "1 / EI * (L * q_0 / 4 * (x ^^^ 3 / 3) + -1 * q_0 / 6 * (x ^^^ 4 / 4))"
233 then () else raise error "integrate.sml, simplify_Integral #199";
237 "----------- simplify by ruleset extending make_polynomial_in ----";
238 "----------- simplify by ruleset extending make_polynomial_in ----";
239 "----------- simplify by ruleset extending make_polynomial_in ----";
241 trace_rewrite:=false;
245 "----------- integrate by ruleset --------------------------------";
246 "----------- integrate by ruleset --------------------------------";
247 "----------- integrate by ruleset --------------------------------";
248 val rls = "integration_rules";
249 val subs = [("bdv","x::real")];
250 fun rewrit_sinst subs rls str =
251 fst (the (rewrite_set_inst "Integrate.thy" true subs rls str));
252 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
253 val str = rewrit_sinst subs rls "Integral x D x";
254 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
255 if str = "c * (x ^^^ 3 / 3) + c_2 * x"
256 then () else raise error "integrate.sml: diff.behav. in integration_rules";
258 val rls = "add_new_c";
259 val str = rewrit_sinst subs rls "c * (x ^^^ 3 / 3) + c_2 * x";
260 if str = "c * (x ^^^ 3 / 3) + c_2 * x + c_3" then ()
261 else raise error "integrate.sml: diff.behav. in add_new_c simpl.";
263 val str = rewrit_sinst subs rls "F x = x ^^^ 3 / 3 + x";
264 if str = "F x = x ^^^ 3 / 3 + x + c"(*not "F x + c =..."*) then ()
265 else raise error "integrate.sml: diff.behav. in add_new_c equation";
267 val rls = "simplify_Integral";
268 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
269 val str = "ff x = c * x + -1 * q_0 * (x ^^^ 2 / 2) + c_2";
270 val str = rewrit_sinst subs rls str;
271 if str = "ff x = c_2 + c * x + -1 * q_0 / 2 * x ^^^ 2"
272 then () else raise error "integrate.sml: diff.behav. in simplify_I #1";
274 val rls = "integration";
275 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
276 val str = rewrit_sinst subs rls "Integral c * x ^^^ 2 + c_2 D x";
277 if str = "c_3 + c_2 * x + c / 3 * x ^^^ 3"
278 then () else raise error "integrate.sml: diff.behav. in integration #1";
280 val str = rewrit_sinst subs rls "Integral 3*x^^^2 + 2*x + 1 D x";
281 if str = "c + x + x ^^^ 2 + x ^^^ 3" then ()
282 else raise error "integrate.sml: diff.behav. in integration #2";
284 val str = rewrit_sinst subs rls
285 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x";
287 "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
288 then () else raise error "integrate.sml: diff.behav. in integration #3";
290 val str = "Integral "^str^" D x";
291 val str = rewrit_sinst subs rls str;
293 "c_2 + c * x + 1 / EI * (L * q_0 / 12 * x ^^^ 3 + -1 * q_0 / 24 * x ^^^ 4)"
294 then () else raise error "integrate.sml: diff.behav. in integration #4";
297 "----------- rewrite 3rd integration in 7.27 ---------------------";
298 "----------- rewrite 3rd integration in 7.27 ---------------------";
299 "----------- rewrite 3rd integration in 7.27 ---------------------";
300 val thy = Isac.thy (*because of Undeclared constant "Biegelinie.EI*);
301 val bdv = [(str2term"bdv", str2term"x")];
303 "Integral 1 / EI * ((L * q_0 * x + -1 * q_0 * x ^^^ 2) / 2) D x";
304 val Some(t,_)= rewrite_set_inst_ thy true bdv simplify_Integral t;
306 "Integral 1 / EI * (L * q_0 / 2 * x + -1 * q_0 / 2 * x ^^^ 2) D x" then ()
307 else raise error "integrate.sml 3rd integration in 7.27, simplify_Integral";
309 val Some(t,_)= rewrite_set_inst_ thy true bdv integration t;
310 if term2str t = "c + 1 / EI * (L * q_0 / 4 * x ^^^ 2 + -1 * q_0 / 6 * x ^^^ 3)"
311 then () else raise error "integrate.sml 3rd integration in 7.27, integration";
314 "----------- check probem type -----------------------------------";
315 "----------- check probem type -----------------------------------";
316 "----------- check probem type -----------------------------------";
317 val model = {Given =["functionTerm f_", "integrateBy v_"],
319 Find =["antiDerivative F_"],
321 Relate=[]}:string ppc;
322 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;
323 val t1 = (term_of o hd) chkmodel;
324 val t2 = (term_of o hd o tl) chkmodel;
325 val t3 = (term_of o hd o tl o tl) chkmodel;
326 case t3 of Const ("Integrate.antiDerivative", _) $ _ => ()
327 | _ => raise error "integrate.sml: Integrate.antiDerivative ???";
329 val model = {Given =["functionTerm f_", "integrateBy v_"],
331 Find =["antiDerivativeName F_"],
333 Relate=[]}:string ppc;
334 val chkmodel = ((map (the o (parse Integrate.thy))) o ppc2list) model;
335 val t1 = (term_of o hd) chkmodel;
336 val t2 = (term_of o hd o tl) chkmodel;
337 val t3 = (term_of o hd o tl o tl) chkmodel;
338 case t3 of Const ("Integrate.antiDerivativeName", _) $ _ => ()
339 | _ => raise error "integrate.sml: Integrate.antiDerivativeName";
341 "----- compare 'Find's from problem, script, formalization -------";
342 val {ppc,...} = get_pbt ["named","integrate","function"];
343 val ("#Find", (Const ("Integrate.antiDerivativeName", _),
344 F1_ as Free ("F_", F1_type))) = last_elem ppc;
345 val {scr = Script sc,... } = get_met ["diff","integration","named"];
346 val [_,_, F2_] = formal_args sc;
347 if F1_ = F2_ then () else raise error "integrate.sml: unequal find's";
349 val ((dsc as Const ("Integrate.antiDerivativeName", _))
350 $ Free ("ff", F3_type)) = str2t "antiDerivativeName ff";
351 if is_dsc dsc then () else raise error "integrate.sml: no description";
352 if F1_type = F3_type then ()
353 else raise error "integrate.sml: unequal types in find's";
356 val pbl = get_pbt ["integrate","function"];
357 case #cas pbl of Some (Const ("Integrate.Integrate",_) $ _) => ()
358 | _ => raise error "integrate.sml: Integrate.Integrate ???";
361 "----------- check Scripts ---------------------------------------";
362 "----------- check Scripts ---------------------------------------";
363 "----------- check Scripts ---------------------------------------";
365 "Script IntegrationScript (f_::real) (v_::real) = \
366 \ (let t_ = Take (Integral f_ D v_) \
367 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) (t_::real))";
368 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
372 "Script NamedIntegrationScript (f_::real) (v_::real) (F_::real=>real) = \
373 \ (let t_ = Take (F_ v_ = Integral f_ D v_) \
374 \ in (Rewrite_Set_Inst [(bdv,v_)] integration False) t_)";
375 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
380 "----------- me method [diff,integration] ---------------------";
381 "----------- me method [diff,integration] ---------------------";
382 "----------- me method [diff,integration] ---------------------";
383 (*exp_CalcInt_No-1.xml*)
384 val fmz = ["functionTerm (x^^^2 + 1)",
385 "integrateBy x","antiDerivative FF"];
387 ("Integrate.thy",["integrate","function"],
388 ["diff","integration"]);
389 val p = e_pos'; val c = [];
390 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
391 val (p,_,f,nxt,_,pt) = me nxt p c pt;
392 val (p,_,f,nxt,_,pt) = me nxt p c pt;
393 val (p,_,f,nxt,_,pt) = me nxt p c pt;
394 val (p,_,f,nxt,_,pt) = me nxt p c pt;
395 val (p,_,f,nxt,_,pt) = me nxt p c pt;
396 val (p,_,f,nxt,_,pt) = me nxt p c pt;
397 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
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 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
401 if f2str f = "c + x + 1 / 3 * x ^^^ 3" then ()
402 else raise error "integrate.sml: method [diff,integration]";
405 "----------- me method [diff,integration,named] ------------------";
406 "----------- me method [diff,integration,named] ------------------";
407 "----------- me method [diff,integration,named] ------------------";
408 (*exp_CalcInt_No-2.xml*)
409 val fmz = ["functionTerm (x^^^2 + 1)",
410 "integrateBy x","antiDerivativeName F"];
412 ("Integrate.thy",["named","integrate","function"],
413 ["diff","integration","named"]);
414 val p = e_pos'; val c = [];
415 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
416 val (p,_,f,nxt,_,pt) = me nxt p c pt;
417 val (p,_,f,nxt,_,pt) = me nxt p c pt;
418 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
419 val (p,_,f,nxt,_,pt) = me nxt p c pt;
420 val (p,_,f,nxt,_,pt) = me nxt p c pt;
421 val (p,_,f,nxt,_,pt) = me nxt p c pt;
422 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
423 val (p,_,f,nxt,_,pt) = me nxt p c pt;
424 val (p,_,f,nxt,_,pt) = me nxt p c pt;
425 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
426 if f2str f = "F x = c + x + 1 / 3 * x ^^^ 3" then()
427 else raise error "integrate.sml: method [diff,integration,named]";
430 "----------- me method [diff,integration,named] Biegelinie.Q -----";
431 "----------- me method [diff,integration,named] Biegelinie.Q -----";
432 "----------- me method [diff,integration,named] Biegelinie.Q -----";
433 (*exp_CalcInt_No-3.xml*)
434 val fmz = ["functionTerm (- q_0)",
435 "integrateBy x","antiDerivativeName Q"];
437 ("Biegelinie.thy",["named","integrate","function"],
438 ["diff","integration","named"]);
439 val p = e_pos'; val c = [];
440 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
441 val (p,_,f,nxt,_,pt) = me nxt p c pt;
442 val (p,_,f,nxt,_,pt) = me nxt p c pt;
443 (*Error Tac Q not in ...*)
444 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Add_Find *);
445 val (p,_,f,nxt,_,pt) = me nxt p c pt;
446 val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 val (p,_,f,nxt,_,pt) = me nxt p c pt;
448 val (p,_,f,nxt,_,pt) = me nxt p c pt(*nxt <- Apply_Method*);
449 val (p,_,f,nxt,_,pt) = me nxt p c pt;
450 val (p,_,f,nxt,_,pt) = me nxt p c pt;
451 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
453 if f2str f = "Q x = c + -1 * q_0 * x" then()
454 else raise error "integrate.sml: method [diff,integration,named] .Q";
457 "----------- interSteps [diff,integration] -----------------------";
458 "----------- interSteps [diff,integration] -----------------------";
459 "----------- interSteps [diff,integration] -----------------------";
462 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
463 ("Integrate.thy",["integrate","function"],
464 ["diff","integration"]))];
467 autoCalculate 1 CompleteCalc;
468 val ((pt,p),_) = get_calc 1; show_pt pt;
470 interSteps 1 ([1],Res);
471 val ((pt,p),_) = get_calc 1; show_pt pt;
472 if existpt' ([1,3], Res) pt then ()
473 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 1";
476 "----------- method analog to rls 'integration' ------------------";
477 "----------- method analog to rls 'integration' ------------------";
478 "----------- method analog to rls 'integration' ------------------";
480 (prep_met Integrate.thy "met_testint" [] e_metID
481 (["diff","integration","test"],
482 [("#Given" ,["functionTerm f_", "integrateBy v_"]),
483 ("#Find" ,["antiDerivative F_"])
485 {rew_ord'="tless_true", rls'=Atools_erls, calc = [],
488 crls = Atools_erls, nrls = e_rls},
489 "Script IntegrationScript (f_::real) (v_::real) = \
490 \ (((Rewrite_Set_Inst [(bdv,v_)] integration_rules False) @@ \
491 \ (Rewrite_Set_Inst [(bdv,v_)] add_new_c False) @@ \
492 \ (Rewrite_Set_Inst [(bdv,v_)] simplify_Integral False)) (f_::real))"
497 [(["functionTerm (Integral x^2 + 1 D x)","integrateBy x",
498 "antiDerivative FF"],
499 ("Integrate.thy",["integrate","function"],
500 ["diff","integration","test"]))];
503 autoCalculate 1 CompleteCalcHead;
505 fetchProposedTactic 1 (*..Apply_Method*);
506 autoCalculate 1 (Step 1);
507 getTactic 1 ([1], Frm) (*still empty*);
509 fetchProposedTactic 1 (*Rewrite_Set_Inst integration_rules*);
510 autoCalculate 1 (Step 1);
512 fetchProposedTactic 1 (*Rewrite_Set_Inst add_new_c*);
513 autoCalculate 1 (Step 1);
515 fetchProposedTactic 1 (*Rewrite_Set_Inst simplify_Integral*);
516 autoCalculate 1 (Step 1);
518 autoCalculate 1 CompleteCalc;
519 val ((pt,p),_) = get_calc 1; show_pt pt;
520 if existpt' ([3], Res) pt then ()
521 else raise error "integrate.sml: test-script doesnt work";
524 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
525 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
526 "----------- Ambiguous input: Integral ?u + ?v D ?bdv = ..--------";
529 [(["functionTerm (x^2 + 1)","integrateBy x","antiDerivative FF"],
530 ("Integrate.thy",["integrate","function"],
531 ["diff","integration"]))];
534 autoCalculate 1 CompleteCalc;
535 val ((pt,p),_) = get_calc 1; show_pt pt;
537 interSteps 1 ([1],Res);
538 val ((pt,p),_) = get_calc 1; show_pt pt;
539 interSteps 1 ([1,1],Res);
540 val ((pt,p),_) = get_calc 1; show_pt pt;
541 getTactic 1 ([1,1,1],Frm);
543 val str = (unenclose o string_of_thm) integral_add;
546 read_cterm (sign_of thy) (str,(TVar(("DUMMY",0),[])));
548 *** More than one term is type correct:
549 *** ((Integral (?u + ?v) D ?bdv) =
550 *** (Integral ?u D (?bdv + (Integral ?v D ?bdv))))
552 *** ((Integral (?u + ?v) D ?bdv) =
553 *** ((Integral ?u D ?bdv) + (Integral ?v D ?bdv)))
556 if existpt' ([1,1,5], Res) pt then ()
557 else raise error "integrate.sml: interSteps on Rewrite_Set_Inst 2";
559 "----------- CAS input -------------------------------------------";
560 "----------- CAS input -------------------------------------------";
561 "----------- CAS input -------------------------------------------";
562 val t = str2term "Integrate (x^^^2 + x + 1, x)";
563 case t of Const ("Integrate.Integrate", _) $ _ => ()
564 | _ => raise error "diff.sml behav.changed for Integrate (..., x)";
568 CalcTree [([], ("e_domID", ["e_pblID"], ["e_metID"]))];
571 replaceFormula 1 "Integrate (x^2 + x + 1, x)";
572 autoCalculate 1 CompleteCalc;
573 val ((pt,p),_) = get_calc 1;
574 val Form res = (#1 o pt_extract) (pt, ([],Res));
576 (* WN070703 does not work like Diff due to error in next-pos
577 if p = ([], Res) andalso term2str res = "5 * a" then ()
578 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";