wneuper/isac: comparison src/smltest/IsacKnowledge/rational.sml

equal deleted inserted replaced

-:0b0dc38b1106
+:72f0be16d83b
 Copyright (c) Stefan Karnel 2002
 Use is subject to license terms.
 use"../smltest/IsacKnowledge/rational.sml";
 use"rational.sml";
+LEGEND WN070906
+nonterm.SK   marks non-terminating examples
+ord.SK       PARTIALLY marks crucial ordering examples
+*SK*         of some (secondary) interest (on 070906)
 ****************************************************************.*)
 (******************************************************************
 WN060104 transfer marked (*SR..*)examples to the exp-collection
 # exp_IsacCore_Simp_Rat_Cancel.xml     from rational.sml    (*SRC*)  10 exp
 term2str t'' = "(-1 - x - y) / (x - y)" (*true*);
 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
 val Some (t',_) = common_nominator_ thy t;
 val Some (t'',_) = add_fraction_ thy t;
-term2str t' =
+if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\
-"(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x)) +\n1\
+\ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then ()
-\ * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" (*true*);
+else raise error "rational.sml lex-ord 1";
-term2str t'' = "(-1 - y - x) / (y - x)" (*true*);
+if term2str t'' = "(-1 - y - x) / (y - x)" then ()
-(*WN.16.10.02 lexicographische ^^^^^^^ Ordnung  ???SK-*)
+else raise error "rational.sml lex-ord 2";
+(*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*)
-val t=(term_of o the o (parse thy))
-	    "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
+val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
 val Some (t',_) = norm_expanded_rat_ thy t;
-term2str t';
+if term2str t' = "(x + y) / (x - y)" then ()
-"(y + x) / (y - x)";
+else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
 (*val Some (t'',_) = norm_rational_ thy t;
-term2str t'';
+*** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
-*** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
+WN.16.10.02 ?! + WN060831???SK4
-WN.16.10.02 ?! + WN060831???SK4*)
+WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*)
-val t=(term_of o the o (parse thy))
+val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
-	    "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
+val Some (t',_) = norm_expanded_rat_ thy t;
-val Some (t',_) = norm_expanded_rat_ thy t;
+if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then ()
-term2str t';
+else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
-"(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
 (*val Some (t'',_) = norm_rational_ thy t;
-term2str t'';
+*** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!
-*** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
+WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*)
-WN.16.10.02 ?!*)
 val t=(term_of o the o (parse thy))
 	    "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
 val Some (t',_) = norm_expanded_rat_ thy t;
 val Some (t'',_) = norm_rational_ thy t;
 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
 else raise error "rational.sml 3";
-trace_rewrite:=true;
+(*trace_rewrite:=true;*)
 val t = str2term "Not (6*x is_atom)";
 val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
 "True";
 val t = str2term "1 < 2";
 val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
 "(-500 * (x * y ^^^ 3) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2))) +\n 20 * (x * (y * x ^^^ 2)) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2)))) /\n(20 * (x * y))";
 trace_rewrite:=true;
 trace_rewrite:=false;
-(*WN.17.3.03 =========================================================^^^---*)
+"nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
+(*WN.2.6.03 from rlang.sml 56a
-"----- SK060904-2a non-termination of add_fraction_p_";
-(*WN.2.6.03 from rlang.sml 56a =======================================vvv---*)
-(*... takes uncredible much time:*)
-(*
-WN060831????SK6
-"----- SK060904-2a non-termination of add_fraction_p_";
 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
 val None = rewrite_set_ thy false common_nominator_p t;
-writeln
-"----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
+WN060831 nonterm.SK7
-\----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
-\----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
-\----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
-\----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n";
-WN060831????SK7
 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
 val None = add_fraction_p_ thy t;
 *)
-(*
-GC #1.48.88.223.2775.290178:   (0 ms)
+(* ------------------------------------------------------------------- *)
-GC #1.48.88.223.2776.290363:   (0 ms)
-GC #1.48.88.223.2777.290712:   (0 ms)
-GC #1.48.88.223.2778.291102:   (0 ms)
-GC #1.48.88.223.2779.291684:   (0 ms)
-GC #1.48.88.223.2780.292389:   (0 ms)
-GC #1.48.88.223.2781.293163:   (0 ms)
-GC #1.48.88.223.2782.294133:   (0 ms)
-GC #1.48.88.223.2783.295181:   (0 ms)
-*)
-(*WN.2.6.03 from rlang.sml 56a =======================================^^^---*)
-(* 25.08.03:  Durchlauf(rechen)zeit: 1 min *)
 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
+(*                 Simplifier fuer beliebige Buchterme                 *)
 (* ------------------------------------------------------------------- *)
-(*                  Simplifier fr beliebige Buchterme                 *)
+(*----------------------- norm_Rational_mg ----------------------------*)
 (* ------------------------------------------------------------------- *)
-(*----------------------- norm_Rational_mg --------------------------*)
-(* ------------------------------------------------------------------- *)
 "-------- numeral rationals --------------------------------------";
 "-------- numeral rationals --------------------------------------";
 "-------- numeral rationals --------------------------------------";
 (*SRA Schalk I, p.40 Nr. 164b *)
 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
-if (term2str t) =
+if (term2str t) = "19 / 21" then ()
-"19 / 21"
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
 (*SRA Schalk I, p.40 Nr. 166a *)
 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
-if (term2str t) =
+if (term2str t) = "45 / 2" then ()
-"45 / 2"
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
 "-------- cancellation -------------------------------------------";
 "-------- cancellation -------------------------------------------";
 "5 * a / (a + -1 * b)"
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
 (*Schalk I, p.68 Nr. 437a *)
-(* SK loops: rechnet ewig; cancel_p h???gt sich auf... WN060420????MG4 *)
-(* corrected *)
 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 if (term2str t) = "1 / (4 * c + 3 * e)" then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
-(**)
+"----- S.K. corrected non-termination 060904";
-(*SK loops .. WN060420????MG5 not canceled to "1 / (4*c + 3*e)"*)
-(* corrected *)
 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
 val Some (t',_) = rewrite_set_ thy false make_polynomial t;
-term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)";
+if term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)" then ()
-(*..WN060831 _with_ parentheses ...*)
+else raise error "rational.sml.sml: S.K.8..corrected 060904-6";
-"----- SK060904-1b non-termination of cancel_p_";
+"----- S.K. corrected non-termination of cancel_p_";
 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
-(* WN060831????SK8*)
 val Some (t',_) = rewrite_set_ thy false cancel_p t'';
-term2str t';
+if term2str t' = "1 / (4 * c + 3 * e)" then ()
+else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
 (**)
 (*Schalk I, p.68 Nr. 437b *)
-(* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter krzen!!! *)
+(* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
-val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
+val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
-(*
+(* val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
-val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+*)
-term2str t; WN060831????SK9
-"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
+(*a casual output from above*)
+val t = str2term
+"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
+(* WN060831 nonterm.SK10
+val Some (t,_) = rewrite_set_ thy false cancel_p t;
+term2str t;
 *)
-(* *)
-val t = str2term
-"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
-(* WN060831????SK10
-val Some (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
-*)
 (*SRM Schalk I, p.68 Nr. 438a *)
 val t = str2term
 "x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 "(-3 + x) / (2 + x)"
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
-(*Schalk I, p.68 Nr. 440b *)
+"----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
-(* Achtung: rechnet ewig; cancel_p h???gt sich auf... WN060831????SK11
 val t = str2term
 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
-trace_rewrite := true;
+val Some (t,_) = rewrite_set_ thy false norm_Rational t;
-val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
-###  rls: cancel_p on:
+else raise error "rational.sml.sml: diff.behav. in norm_Rational 27";
-(-9 * (a ^ 3 * b) + -9 * (a ^ 2 * b ^ 2) + a ^ 5 * b + a ^ 4 * b ^ 2) /
-(3 * (a ^ 3 * b) + -3 * (a * b ^ 3) + a ^ 4 * b + -1 * (a ^ 2 * b ^ 3))
+"----- SK12 works since 0707xx";
-trace_rewrite := false;
-term2str t;
-if (term2str t) =
-then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27";
 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
-val Some (t',_) = rewrite_set_ thy false make_polynomial t;
+val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
-term2str t';
+if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
-"(-9 * a ^^^ 3 * b + -9 * a ^^^ 2 * b ^^^ 2 + a ^^^ 5 * b + a ^^^ 4 * b ^^^ 2)/
+else raise error "rational.sml.sml: diff.behav. in norm_Rational 28";
-(3 * a ^^^ 3 * b + -3 * a * b ^^^ 3 + a ^^^ 4 * b + -1 * a ^^^ 2 * b ^^^ 3)";
-val Some (t',_) = rewrite_set_ thy false cancel_p t;
-term2str t';
-WN060831????SK12*)
 "-------- common denominator and multiplication ------------------";
 "-------- common denominator and multiplication ------------------";
 "-------- common denominator and multiplication ------------------";
 (*----------------------------------------------------------------------*)
-(*--------- Gemeinsamer Nenner und Multiplikation von Brchen ----------*)
+(*--------- Gemeinsamer Nenner und Multiplikation von Bruechen ---------*)
 (*----------------------------------------------------------------------*)
 (*SRAM Schalk I, p.69 Nr. 441b *)
 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
 val t = str2term
 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
-"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)"
+"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
-(*Schalk I, p.69 Nr. 455b *)
+"----- Schalk I, p.69 Nr. 455b";
-(* Achtung: Endlosschleife
 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
+if term2str t = "(2 + -1 * x) / (3 + y)" then ()
-if (term2str t) =
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
-"----- SK060904-1a non-termination of cancel_p_";
+"----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
-val Some (t,_) = rewrite_set_ thy false make_polynomial t;
+val Some (t,_) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "(2 + -1 * x) / (3 + y)" then ()
-"(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /
+else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
-(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"
-val Some (t,_) = rewrite_set_ thy false cancel_p t;
+"----- ?: worked before 0707xx";
-term2str t;
-(* Achtung: rechnet ewig; cancel_p h???gt sich auf... ????SK*)
 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
-val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val Some (t,_) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "-1 / (3 + y)" then ()
-(*ENDLOSSCHLEIFE!!! ???MG!!!*)
+else raise error "rational.sml: -1 / (3 + y) norm_Rational";
-val t = str2term "-1 / (3 + y)";
-(*                ~~         *)
-val Some (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t = "-1 / (3 + 1 * y)";
-(********* Das ist das PROBLEM !!!!!!!??? *******************)
-(*MG: -1 im Z???ler der Angabe verursacht das Problem ! WN060831???MG!!SK0*)
-*)
 (*SRD Schalk I, p.69 Nr. 456b *)
 val t = str2term
 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
-if (term2str t) =
+if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
-"b / (1 + 2 * b + b ^^^ 2)"
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
 (*SRD Schalk I, p.69 Nr. 457b *)
 val t = str2term
 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
 if (term2str t) =
 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
-(*Schalk I, p.69 Nr. 458b *)
+"----- Schalk I, p.69 Nr. 458b works since 0707";
-(* Achtung: rechnet ewig; cancel_p h???gt sich auf... ????SK
 val t = str2term
 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
-val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val Some (t,_) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
-if (term2str t) =
+else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
-then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 40";
-*)
 (*SRD Schalk I, p.69 Nr. 459b *)
-val t = str2term
+val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
-"(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
+val Some (t,_) = rewrite_set_ thy false norm_Rational t;
-val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
-term2str t;
-if (term2str t) =
-"(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
-(*Schalk I, p.69 Nr. 460b *)
+(*Schalk I, p.69 Nr. 460b nonterm.SK
-(* Achtung: rechnet ewig; cancel_p h???gt sich auf... ????SK
 val t = str2term
 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
+if term2str t =
-if (term2str t) =
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
 val t = str2term
 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
-val Some (t,_) = rewrite_set_ thy false make_polynomial t;
+val Some (t',_) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+... non terminating.
+val Some (t',_) = rewrite_set_ thy false make_polynomial t;
 "(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
-val Some (t,_) = rewrite_set_ thy false cancel_p t;
+val Some (t,_) = rewrite_set_ thy false cancel_p t';
-term2str t;
+... non terminating.*)
-????SK*)
 (*SRD Schalk I, p.70 Nr. 472a *)
 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
 		 \((4*x - 8*y)/(x + y))";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 "3 * b ^^^ 3 / (2 * a + -2 * b)"
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
 (*----------------------------------------------------------------------*)
-(*---------------------- Mehrfache Dppelbrche -------------------------*)
+(*---------------------- Mehrfache Dppelbrueche ------------------------*)
 (*----------------------------------------------------------------------*)
 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
 (*WN060419 crashes with method 'simplify' ????SK*)
 val t = str2term
 "((a^^^2 - b^^^2)/(2*a*b)+2*a*b/(a^^^2 - b^^^2))/((a^^^2+b^^^2)/(2*a*b)+1) / ((a^^^2+b^^^2)^^^2/(a+b)^^^2)";
-val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val Some (t,_) = rewrite_set_ thy false norm_Rational t;
-term2str t;
+if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
-if (term2str t) =
-"1 / (a ^^^ 2 + -1 * b ^^^ 2)"
-then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
 "----- Schalk I, p.70 Nr. 477a";
-(* Achtung: rechnet ewig; Bsp zu komplex;
+(* MG Achtung: terme explodieren; Bsp zu komplex;
 L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
 val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
 		 \(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
-val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
+val Some (t',_) = rewrite_set_ thy false norm_Rational t;
-term2str t';
-if (term2str t') = ????SK ???MG
-then ()
-else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 50";
 val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / \
 		 \((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
-term2str t; ????SK ???MG
+????SK ???MG*)
-"(a ^^^ 2 * b ^^^ 4 * y + 2 * a ^^^ 2 * b ^^^ 3 * y ^^^ 2 +\n -4 * a ^^^ 2 * b ^^^ 2 * y ^^^ 3 +\n -8 * a ^^^ 2 * b * y ^^^ 4 +\n 4 * a * b ^^^ 4 * x * y +\n 8 * a * b ^^^ 3 * x * y ^^^ 2 +\n -16 * a * b ^^^ 2 * x * y ^^^ 3 +\n -32 * a * b * x * y ^^^ 4 +\n 4 * b ^^^ 4 * x ^^^ 2 * y +\n 8 * b ^^^ 3 * x ^^^ 2 * y ^^^ 2 +\n -16 * b ^^^ 2 * x ^^^ 2 * y ^^^ 3 +\n -32 * b * x ^^^ 2 * y ^^^ 4)
-/\n(a ^^^ 2 * b ^^^ 5 * y + -1 * a ^^^ 2 * b ^^^ 4 * y ^^^ 2 +\n -3 * a ^^^ 2 * b ^^^ 3 * y ^^^ 3 +\n a ^^^ 2 * b ^^^ 2 * y ^^^ 4 +\n 2 * a ^^^ 2 * b * y ^^^ 5 +\n 2 * a * b ^^^ 5 * x * y +\n -2 * a * b ^^^ 4 * x * y ^^^ 2 +\n -6 * a * b ^^^ 3 * x * y ^^^ 3 +\n 2 * a * b ^^^ 2 * x * y ^^^ 4 +\n 4 * a * b * x * y ^^^ 5 +\n b ^^^ 5 * x ^^^ 2 * y +\n -1 * b ^^^ 4 * x ^^^ 2 * y ^^^ 2 +\n -3 * b ^^^ 3 * x ^^^ 2 * y ^^^ 3 +\n b ^^^ 2 * x ^^^ 2 * y ^^^ 4 +\n 2 * b * x ^^^ 2 * y ^^^ 5)";
-*)
+"----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
-(*Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec *)
 val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
 		 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t';
-(* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
-????SK ???MG
 if term2str t' =
 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
------------------------------------------------------------------------*)
+(* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
+if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /\n(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) *\n (a + -1 * b))" then ()
+else raise error "rational.sml: works again";
+re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
 (*Schalk I, p.70 Nr. 480a *)
-(* SK Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831????SK00
+(* Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831 nonterm.SK00
 val t = str2term
 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z) / (2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z)))";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 if (term2str t) =
 then ()
 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
-(*MG Berechne Zwischenergebnisse: WN060831????SK00*)
+(*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
 val t = str2term
 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
 term2str t;
 "(x ^^^ 2 * y ^^^ 2 * z + x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2) /
 (*Schalk I, p.60 Nr. 215d *)
 (* Achtung: rechnet ewig ...
 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
+term2str t; noterm.SK
 *)
 (* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
 (*
 val t = str2term "(a-b)^^^3 * (x+y)^^^4";
 "a^^^5 * x^^^2 + 2 * a^^^5 * x * y + a^^^5 * y^^^2 +\n-5 * a^^^4 * b * x^^^2 +\n-10 * a^^^4 * b * x * y +\n-5 * a^^^4 * b * y^^^2 +\n10 * a^^^3 * b^^^2 * x^^^2 +\n20 * a^^^3 * b^^^2 * x * y +\n10 * a^^^3 * b^^^2 * y^^^2 +\n-10 * a^^^2 * b^^^3 * x^^^2 +\n-20 * a^^^2 * b^^^3 * x * y +\n-10 * a^^^2 * b^^^3 * y^^^2 +\n5 * a * b^^^4 * x^^^2 +\n10 * a * b^^^4 * x * y +\n5 * a * b^^^4 * y^^^2 +\n-1 * b^^^5 * x^^^2 +\n-2 * b^^^5 * x * y +\n-1 * b^^^5 * y^^^2";
 *)
 (*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
 (*--------------------------------------------------------------------*)
-(*Schalk I, p.70 Nr. 480b *)
+(*Schalk I, p.70 Nr. 480b
-(*
-trace_rewrite:=false; (*sonst dauert Berechnung sehr lange!*)
 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
 		 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
 		 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
 		 \(20*x*y/(x^^^2 - 25*y^^^2))";
 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t;
+SK.nonterm
-"((180 * x^^^4 * y + 675 * x^^^3 * y^^^2 + 1105 * x^^^2 * y^^^3 +\n  -75 * x * y^^^4 +\n  -125 * y^^^5) /\n (x^^^3 + 5 * x^^^2 * y + -25 * x * y^^^2 + -125 * y^^^3) +\n (225 * x^^^2 * y^^^2 + -25 * y^^^4) /\n (x^^^2 + 10 * x * y + 25 * y^^^2)) /\n(20 * x * y)";
+Kann nicht weiter vereinfacht werden !!!!?? *)
-*)
-(* Kann nicht weiter vereinfacht werden !!!!?? *)
 (*--------------------------------------------------------------------*)
-(*Seltsames in common_nominator_p: *)
+"---- MGs test set";
-(*
+val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
-val t = str2term " (1 + x^^^5) / (x + y) + x^^^3 / x ";
-(*                                  ~~~~~  !!! *)
 val Some (t,_) = rewrite_set_ thy false common_nominator_p t;
-term2str t;
+if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
-*)
+else raise error "";
-(*### add_fraction_p_ called
-uncaught exception nonexhaustive binding failure
-raised at: stdIn:175.1-175.61*)
-val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
-(*                                  ~~~~~  !!! *)
-val Some (t,_) = rewrite_set_ thy false common_nominator_p t;
-term2str t;
-"(1 + 1 * x^^^3 + 1 * x^^^5 + 1 * (y * x^^^2)) / (1 * x + 1 * y)";
 (*--------------------------------------------------------------------*)
 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
 ---> Sortierung FALSCH !!  *)
 val t = str2term "b^^^3 * a^^^5/a ";
 (********* Das ist das PROBLEM !!!!!!!??? *******************)
 (* -1 im Z???ler der Angabe verursacht das Problem !*)
 *)
 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
-(*Eigenes*)
+"----- MGs test set";
-(* Achtung: Endlosschleife bei cancel_p:
 val t = str2term "(a^^^2 + -1)/(a+1)";
-val Some (t,_) = rewrite_set_ thy false make_polynomial t;
+val Some (t',_) = rewrite_set_ thy false cancel_p t;
-term2str t;
+if term2str t' = "(-1 + a) / 1" then ()
-"(-1 + a^^^2) / (1 + a)";
+else raise error "rational.sml MG tests 3d";
-val Some (t,_) = rewrite_set_ thy false cancel_p t;
-term2str t;
+"----- NOT TERMINATING ?: worked before 0707xx";
-"(-1 + 1 * a) / 1"; (*OK*)
-*)
-"----- NOT TERMINATING";
 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
-val Some (t',_) = rewrite_set_ thy false make_polynomial t;
+val Some (t'',_) = rewrite_set_ thy false norm_Rational t;
-term2str t' =
+if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
-"(-1 + -1 * b + a ^^^ 2 + a ^^^ 2 * b) /\n(-1 + -1 * a + b ^^^ 2 + a * b ^^^ 2)";
+else raise error "rational.sml MG tests 3e";
-(* NOT TERMINATING
-val Some (t'',_) = rewrite_set_ thy false cancel_p t';
-term2str t'';
-Endlosschleife*)
 "----- corrected SK060905";
 val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
-term2str t' = "-1 / (5 + -2 * x)" (*true*);
+if term2str t' = "-1 / (5 + -2 * x)" then ()
+else raise error "rational.sml corrected SK060905";
 "--------------------------------------------------------------------";
 "----------------------- Muster-Beispiele fuer DA -------------------";
 "--------------------------------------------------------------------";
 val t = str2term "a*b*c*d / (d*e*f*g)";
 val Some (t', _) = cancel_p_ thy t; term2str t';
 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
 val Some (t', _) = cancel_p_ thy t; term2str t';
-(*???SK order ???*)
+(*???order.SK  ???*)
-"----- SK060904-1a non-termination of cancel_p_ NOT CANCELED";
+"----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
-val Some (t',_) = rewrite_set_ thy false norm_Poly t;
+val Some (t',_) = rewrite_set_ thy false norm_Rational t;
-term2str t' =
+if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
-"(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true NOT CANCELED*);
+else raise error "rational.sml SK060904-1a worked since 0707xx";
-val Some (t'',_) = cancel_p_ thy t'; term2str t' =
-"(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /\n(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)" (*true NOT CANCELED*);
+"----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
-"----- SK060904-1b non-termination of cancel_p_ ... corrected";
 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
-val Some (t',_) = cancel_p_ thy t; term2str t' = "1 / (4 * c + 3 * e)"(*true*);
+val Some (t',_) = cancel_p_ thy t;
+if term2str t' = "1 / (4 * c + 3 * e)" then ()
+else raise error "rational.sml SK060904-1b";
 "----- SK060904-2a non-termination of add_fraction_p_";
 val t = str2term " (a + b * x) / (a + -1 * (b * x)) +  \
 		 \ (-1 * a + b * x) / (a + b * x)      ";
-(*
+(* nonterm.SK
 val Some (t',_) = rewrite_set_ thy false common_nominator_p t;
 common_nominator_p_ thy t;
 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) +  \
 \ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";

changeset 3881	72f0be16d83b
parent 3742	c62938a26b3e