24 "----------- try fun applyTactics -----------------------"; |
24 "----------- try fun applyTactics -----------------------"; |
25 "----------- pbl binom polynom vereinfachen p.39 --------"; |
25 "----------- pbl binom polynom vereinfachen p.39 --------"; |
26 "----------- pbl binom polynom vereinfachen: cube -------"; |
26 "----------- pbl binom polynom vereinfachen: cube -------"; |
27 "----------- refine Vereinfache -------------------------"; |
27 "----------- refine Vereinfache -------------------------"; |
28 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
28 "----------- *** prep_pbt: syntax error in '#Where' of [v"; |
|
29 "----------- check: fmz matches pbt ---------------------"; |
29 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
30 "--------------------------------------------------------"; |
31 "--------------------------------------------------------"; |
31 "--------------------------------------------------------"; |
32 "--------------------------------------------------------"; |
32 |
33 |
33 val thy = theory "PolyMinus"; |
34 val thy = theory "PolyMinus"; |
254 "----------- me simplification.for_polynomials.with_minus"; |
255 "----------- me simplification.for_polynomials.with_minus"; |
255 "----------- me simplification.for_polynomials.with_minus"; |
256 "----------- me simplification.for_polynomials.with_minus"; |
256 val c = []; |
257 val c = []; |
257 val (p,_,f,nxt,_,pt) = |
258 val (p,_,f,nxt,_,pt) = |
258 CalcTreeTEST |
259 CalcTreeTEST |
259 [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
260 [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
260 "normalform N"], |
261 "normalform N"], |
261 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
262 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
262 ["simplification","for_polynomials","with_minus"]))]; |
263 ["simplification","for_polynomials","with_minus"]))]; |
263 (*========== inhibit exn ======================================================= |
264 (*========== inhibit exn ======================================================= |
264 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
265 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
268 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
269 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
269 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
270 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
270 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
271 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
271 "----------- 140 c ---"; |
272 "----------- 140 c ---"; |
272 states:=[]; |
273 states:=[]; |
273 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
274 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
274 "normalform N"], |
275 "normalform N"], |
275 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
276 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
276 ["simplification","for_polynomials","with_minus"]))]; |
277 ["simplification","for_polynomials","with_minus"]))]; |
277 moveActiveRoot 1; |
278 moveActiveRoot 1; |
278 autoCalculate 1 CompleteCalc; |
279 autoCalculate 1 CompleteCalc; |
281 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
282 term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g" |
282 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; |
283 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f..."; |
283 |
284 |
284 "----------- 140 d ---"; |
285 "----------- 140 d ---"; |
285 states:=[]; |
286 states:=[]; |
286 CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)", |
287 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)", |
287 "normalform N"], |
288 "normalform N"], |
288 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
289 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
289 ["simplification","for_polynomials","with_minus"]))]; |
290 ["simplification","for_polynomials","with_minus"]))]; |
290 moveActiveRoot 1; |
291 moveActiveRoot 1; |
291 autoCalculate 1 CompleteCalc; |
292 autoCalculate 1 CompleteCalc; |
295 then () else error "polyminus.sml: Vereinfache 140 d)"; |
296 then () else error "polyminus.sml: Vereinfache 140 d)"; |
296 |
297 |
297 |
298 |
298 "----------- 139 c ---"; |
299 "----------- 139 c ---"; |
299 states:=[]; |
300 states:=[]; |
300 CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)", |
301 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)", |
301 "normalform N"], |
302 "normalform N"], |
302 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
303 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
303 ["simplification","for_polynomials","with_minus"]))]; |
304 ["simplification","for_polynomials","with_minus"]))]; |
304 moveActiveRoot 1; |
305 moveActiveRoot 1; |
305 autoCalculate 1 CompleteCalc; |
306 autoCalculate 1 CompleteCalc; |
308 term2str (get_obj g_res pt (fst p)) = "- (3 * f)" |
309 term2str (get_obj g_res pt (fst p)) = "- (3 * f)" |
309 then () else error "polyminus.sml: Vereinfache 139 c)"; |
310 then () else error "polyminus.sml: Vereinfache 139 c)"; |
310 |
311 |
311 "----------- 139 b ---"; |
312 "----------- 139 b ---"; |
312 states:=[]; |
313 states:=[]; |
313 CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)", |
314 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)", |
314 "normalform N"], |
315 "normalform N"], |
315 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
316 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
316 ["simplification","for_polynomials","with_minus"]))]; |
317 ["simplification","for_polynomials","with_minus"]))]; |
317 moveActiveRoot 1; |
318 moveActiveRoot 1; |
318 autoCalculate 1 CompleteCalc; |
319 autoCalculate 1 CompleteCalc; |
321 term2str (get_obj g_res pt (fst p)) = "-3 * u - v" |
322 term2str (get_obj g_res pt (fst p)) = "-3 * u - v" |
322 then () else error "polyminus.sml: Vereinfache 139 b)"; |
323 then () else error "polyminus.sml: Vereinfache 139 b)"; |
323 |
324 |
324 "----------- 138 a ---"; |
325 "----------- 138 a ---"; |
325 states:=[]; |
326 states:=[]; |
326 CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)", |
327 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)", |
327 "normalform N"], |
328 "normalform N"], |
328 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
329 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
329 ["simplification","for_polynomials","with_minus"]))]; |
330 ["simplification","for_polynomials","with_minus"]))]; |
330 moveActiveRoot 1; |
331 moveActiveRoot 1; |
331 autoCalculate 1 CompleteCalc; |
332 autoCalculate 1 CompleteCalc; |
375 |
376 |
376 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
377 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
377 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
378 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
378 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
379 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
379 states:=[]; |
380 states:=[]; |
380 CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))", |
381 CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))", |
381 "normalform N"], |
382 "normalform N"], |
382 ("PolyMinus",["klammer","polynom","vereinfachen"], |
383 ("PolyMinus",["klammer","polynom","vereinfachen"], |
383 ["simplification","for_polynomials","with_parentheses"]))]; |
384 ["simplification","for_polynomials","with_parentheses"]))]; |
384 moveActiveRoot 1; |
385 moveActiveRoot 1; |
385 autoCalculate 1 CompleteCalc; |
386 autoCalculate 1 CompleteCalc; |
406 |
407 |
407 "----------- try fun applyTactics --------------------------------"; |
408 "----------- try fun applyTactics --------------------------------"; |
408 "----------- try fun applyTactics --------------------------------"; |
409 "----------- try fun applyTactics --------------------------------"; |
409 "----------- try fun applyTactics --------------------------------"; |
410 "----------- try fun applyTactics --------------------------------"; |
410 states:=[]; |
411 states:=[]; |
411 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
412 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
412 "normalform N"], |
413 "normalform N"], |
413 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
414 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
414 ["simplification","for_polynomials","with_minus"]))]; |
415 ["simplification","for_polynomials","with_minus"]))]; |
415 moveActiveRoot 1; |
416 moveActiveRoot 1; |
416 autoCalculate 1 CompleteCalcHead; |
417 autoCalculate 1 CompleteCalcHead; |
466 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)), |
467 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)), |
467 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))] |
468 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))] |
468 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) |
469 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) |
469 |
470 |
470 states:=[]; |
471 states:=[]; |
471 CalcTree [(["TERM (- (8 * g) + 10 * g + h)", |
472 CalcTree [(["Term (- (8 * g) + 10 * g + h)", |
472 "normalform N"], |
473 "normalform N"], |
473 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
474 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
474 ["simplification","for_polynomials","with_minus"]))]; |
475 ["simplification","for_polynomials","with_minus"]))]; |
475 moveActiveRoot 1; |
476 moveActiveRoot 1; |
476 autoCalculate 1 CompleteCalc; |
477 autoCalculate 1 CompleteCalc; |
478 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h" |
479 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h" |
479 then () else error "polyminus.sml: addiere_vor_minus"; |
480 then () else error "polyminus.sml: addiere_vor_minus"; |
480 |
481 |
481 |
482 |
482 states:=[]; |
483 states:=[]; |
483 CalcTree [(["TERM (- (8 * g) + 10 * g + f)", |
484 CalcTree [(["Term (- (8 * g) + 10 * g + f)", |
484 "normalform N"], |
485 "normalform N"], |
485 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
486 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
486 ["simplification","for_polynomials","with_minus"]))]; |
487 ["simplification","for_polynomials","with_minus"]))]; |
487 moveActiveRoot 1; |
488 moveActiveRoot 1; |
488 autoCalculate 1 CompleteCalc; |
489 autoCalculate 1 CompleteCalc; |
527 trace_rewrite := true; |
528 trace_rewrite := true; |
528 trace_rewrite := false; |
529 trace_rewrite := false; |
529 |
530 |
530 (*@@@@@@@*) |
531 (*@@@@@@@*) |
531 states:=[]; |
532 states:=[]; |
532 CalcTree [(["TERM ((3*a + 2) * (4*a - 1))", |
533 CalcTree [(["Term ((3*a + 2) * (4*a - 1))", |
533 "normalform N"], |
534 "normalform N"], |
534 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
535 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
535 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
536 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
536 moveActiveRoot 1; |
537 moveActiveRoot 1; |
537 autoCalculate 1 CompleteCalc; |
538 autoCalculate 1 CompleteCalc; |
546 |
547 |
547 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
548 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
548 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
549 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
549 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
550 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
550 states:=[]; |
551 states:=[]; |
551 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"], |
552 CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"], |
552 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
553 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
553 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
554 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
554 moveActiveRoot 1; |
555 moveActiveRoot 1; |
555 autoCalculate 1 CompleteCalc; |
556 autoCalculate 1 CompleteCalc; |
556 val ((pt,p),_) = get_calc 1; show_pt pt; |
557 val ((pt,p),_) = get_calc 1; show_pt pt; |
557 |
558 |
558 |
559 |
559 "----------- refine Vereinfache ----------------------------------"; |
560 "----------- refine Vereinfache ----------------------------------"; |
560 "----------- refine Vereinfache ----------------------------------"; |
561 "----------- refine Vereinfache ----------------------------------"; |
561 "----------- refine Vereinfache ----------------------------------"; |
562 "----------- refine Vereinfache ----------------------------------"; |
562 val fmz = ["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", |
563 val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", |
563 "normalform N"]; |
564 "normalform N"]; |
564 print_depth 11; |
565 print_depth 11; |
565 val matches = refine fmz ["vereinfachen"]; |
566 val matches = refine fmz ["vereinfachen"]; |
566 print_depth 3; |
567 print_depth 3; |
567 |
568 |
619 show_types := true; |
620 show_types := true; |
620 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" |
621 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n matchsub (?a + (?b - ?c)) t_t |\n matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)" |
621 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1"; |
622 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1"; |
622 show_types := false; |
623 show_types := false; |
623 |
624 |
624 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
625 "----------- check: fmz matches pbt ---------------------"; |
625 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |
626 "----------- check: fmz matches pbt ---------------------"; |
626 |
627 "----------- check: fmz matches pbt ---------------------"; |
|
628 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))"; |
|
629 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"]; |
|
630 val pI = ["plus_minus","polynom","vereinfachen"]; |
|
631 prep_ori fmz thy ((#ppc o get_pbt) pI); |
|
632 (*val it = |
|
633 [(1, [1], "#undef", Const (...), [...]), <<<=== |
|
634 (2, [1], "#Find", Const (...), [...])] |
|
635 : ori list |
|
636 *) |
|
637 val t = str2term "TERM ttt"; |
|
638 atomwy t; |
|
639 val t = str2term "term ttt"; |
|
640 atomwy t; |
|
641 val t = str2term "Term ttt"; |
|
642 atomwy t; |