43 |
43 |
44 case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of |
44 case eval_ist_monom 0 0 (TermC.str2term "(3*a) ist_monom") 0 of |
45 SOME ("3 * a ist_monom = True", _) => () |
45 SOME ("3 * a ist_monom = True", _) => () |
46 | _ => error "polyminus.sml: 3 * a ist_monom = True"; |
46 | _ => error "polyminus.sml: 3 * a ist_monom = True"; |
47 |
47 |
48 case eval_ist_monom 0 0 (TermC.str2term "(a^^^2) ist_monom") 0 of |
48 case eval_ist_monom 0 0 (TermC.str2term "(a \<up> 2) ist_monom") 0 of |
49 SOME ("a ^^^ 2 ist_monom = True", _) => () |
49 SOME ("a \<up> 2 ist_monom = True", _) => () |
50 | _ => error "polyminus.sml: a^^^2 ist_monom = True"; |
50 | _ => error "polyminus.sml: a \<up> 2 ist_monom = True"; |
51 |
51 |
52 case eval_ist_monom 0 0 (TermC.str2term "(3*a^^^2) ist_monom") 0 of |
52 case eval_ist_monom 0 0 (TermC.str2term "(3*a \<up> 2) ist_monom") 0 of |
53 SOME ("3 * a ^^^ 2 ist_monom = True", _) => () |
53 SOME ("3 * a \<up> 2 ist_monom = True", _) => () |
54 | _ => error "polyminus.sml: 3*a^^^2 ist_monom = True"; |
54 | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True"; |
55 |
55 |
56 case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of |
56 case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of |
57 SOME ("a * b ist_monom = True", _) => () |
57 SOME ("a * b ist_monom = True", _) => () |
58 | _ => error "polyminus.sml: a*b ist_monom = True"; |
58 | _ => error "polyminus.sml: a*b ist_monom = True"; |
59 |
59 |
137 |
137 |
138 case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of |
138 case eval_kleiner 0 0 (TermC.str2term "(10*g) kleiner f") 0 of |
139 SOME ("10 * g kleiner f = False", _) => () |
139 SOME ("10 * g kleiner f = False", _) => () |
140 | _ => error "polyminus.sml: 10 * g kleiner f = False"; |
140 | _ => error "polyminus.sml: 10 * g kleiner f = False"; |
141 |
141 |
142 case eval_kleiner 0 0 (TermC.str2term "(a^^^2) kleiner b") 0 of |
142 case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of |
143 SOME ("a ^^^ 2 kleiner b = True", _) => () |
143 SOME ("a \<up> 2 kleiner b = True", _) => () |
144 | _ => error "polyminus.sml: a ^^^ 2 kleiner b = True"; |
144 | _ => error "polyminus.sml: a \<up> 2 kleiner b = True"; |
145 |
145 |
146 case eval_kleiner 0 0 (TermC.str2term "(3*a^^^2) kleiner b") 0 of |
146 case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of |
147 SOME ("3 * a ^^^ 2 kleiner b = True", _) => () |
147 SOME ("3 * a \<up> 2 kleiner b = True", _) => () |
148 | _ => error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True"; |
148 | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True"; |
149 |
149 |
150 case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of |
150 case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of |
151 SOME ("a * b kleiner c = True", _) => () |
151 SOME ("a * b kleiner c = True", _) => () |
152 | _ => error "polyminus.sml: a * b kleiner b = True"; |
152 | _ => error "polyminus.sml: a * b kleiner b = True"; |
153 |
153 |
412 moveActiveRoot 1; |
412 moveActiveRoot 1; |
413 autoCalculate 1 CompleteCalcHead; |
413 autoCalculate 1 CompleteCalcHead; |
414 autoCalculate 1 (Steps 1); |
414 autoCalculate 1 (Steps 1); |
415 autoCalculate 1 (Steps 1); |
415 autoCalculate 1 (Steps 1); |
416 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
416 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
417 "----- 1 ^^^"; |
417 "----- 1 \<up> "; |
418 fetchApplicableTactics 1 0 p; |
418 fetchApplicableTactics 1 0 p; |
419 val appltacs = specific_from_prog pt p; |
419 val appltacs = specific_from_prog pt p; |
420 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*); |
420 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*); |
421 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
421 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
422 "----- 2 ^^^"; |
422 "----- 2 \<up> "; |
423 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) |
423 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) |
424 val erls = erls_ordne_alphabetisch; |
424 val erls = erls_ordne_alphabetisch; |
425 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
425 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
426 val SOME (t',_) = |
426 val SOME (t',_) = |
427 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t; |
427 rewrite_ (@{theory "Isac_Knowledge"}) e_rew_ord erls false @{thm tausche_minus} t; |
438 Rewrite.trace_on := false; |
438 Rewrite.trace_on := false; |
439 |
439 |
440 |
440 |
441 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*); |
441 applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*); |
442 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
442 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
443 "----- 3 ^^^"; |
443 "----- 3 \<up> "; |
444 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
444 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
445 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
445 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
446 "----- 4 ^^^"; |
446 "----- 4 \<up> "; |
447 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
447 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
448 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
448 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
449 "----- 5 ^^^"; |
449 "----- 5 \<up> "; |
450 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
450 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
451 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
451 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
452 "----- 6 ^^^"; |
452 "----- 6 \<up> "; |
453 |
453 |
454 (*<CALCMESSAGE> failure </CALCMESSAGE> |
454 (*<CALCMESSAGE> failure </CALCMESSAGE> |
455 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
455 applyTactic 1 p (hd (specific_from_prog pt p)) (**); |
456 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
456 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
457 "----- 7 ^^^"; |
457 "----- 7 \<up> "; |
458 *) |
458 *) |
459 autoCalculate 1 CompleteCalc; |
459 autoCalculate 1 CompleteCalc; |
460 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
460 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
461 (*independent from failure above: met_simp_poly_minus not confluent: |
461 (*independent from failure above: met_simp_poly_minus not confluent: |
462 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)), |
462 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)), |
529 ["simplification", "for_polynomials", "with_parentheses_mult"]))]; |
529 ["simplification", "for_polynomials", "with_parentheses_mult"]))]; |
530 moveActiveRoot 1; |
530 moveActiveRoot 1; |
531 autoCalculate 1 CompleteCalc; |
531 autoCalculate 1 CompleteCalc; |
532 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
532 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt; |
533 if p = ([], Res) andalso |
533 if p = ([], Res) andalso |
534 UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a" |
534 UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \<up> 2 + 5 * a" |
535 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ..."; |
535 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ..."; |
536 |
536 |
537 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
537 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
538 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
538 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
539 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
539 "----------- pbl binom polynom vereinfachen: cube ----------------"; |