equal
deleted
inserted
replaced
1341 else error "rational.sml: diff.behav. in norm_Rational_mg 24"; |
1341 else error "rational.sml: diff.behav. in norm_Rational_mg 24"; |
1342 |
1342 |
1343 "----- S.K. corrected non-termination 060904"; |
1343 "----- S.K. corrected non-termination 060904"; |
1344 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))"; |
1344 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))"; |
1345 val SOME (t',_) = rewrite_set_ thy false make_polynomial t; |
1345 val SOME (t',_) = rewrite_set_ thy false make_polynomial t; |
1346 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 () |
1346 term2str t'; |
1347 else error "rational.sml: S.K.8..corrected 060904-6"; |
1347 if term2str t' = |
|
1348 "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)" |
|
1349 (*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*) |
|
1350 then () else error "rational.sml: S.K.8..corrected 060904-6"; |
1348 |
1351 |
1349 "----- S.K. corrected non-termination of cancel_p_"; |
1352 "----- S.K. corrected non-termination of cancel_p_"; |
1350 val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^ |
1353 val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^ |
1351 "(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"); |
1354 "(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"); |
1352 val SOME (t',_) = rewrite_set_ thy false cancel_p t''; |
1355 val SOME (t',_) = rewrite_set_ thy false cancel_p t''; |
1418 (*SRAM Schalk I, p.69 Nr. 441b *) |
1421 (*SRAM Schalk I, p.69 Nr. 441b *) |
1419 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))"; |
1422 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))"; |
1420 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1423 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1421 term2str t; |
1424 term2str t; |
1422 if (term2str t) = |
1425 if (term2str t) = |
1423 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 +\n 16 * a ^^^ 4 * b) /\n(9 * a ^^^ 4)" |
1426 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)" |
1424 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28"; |
1427 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28"; |
1425 |
1428 |
1426 (*SRAM Schalk I, p.69 Nr. 442b *) |
1429 (*SRAM Schalk I, p.69 Nr. 442b *) |
1427 val t = str2term "(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x)*(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)"; |
1430 val t = str2term "(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x)*(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)"; |
1428 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1431 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1529 val t = str2term |
1532 val t = str2term |
1530 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))"; |
1533 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))"; |
1531 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1534 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1532 term2str t; |
1535 term2str t; |
1533 if (term2str t) = |
1536 if (term2str t) = |
1534 (*"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"*) |
1537 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2" |
1535 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b +\n9 * a * b ^^^ 2" |
1538 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39"; |
1536 then () |
|
1537 else error "rational.sml: diff.behav. in norm_Rational_mg 39"; |
|
1538 |
1539 |
1539 "----- Schalk I, p.69 Nr. 458b works since 0707"; |
1540 "----- Schalk I, p.69 Nr. 458b works since 0707"; |
1540 val t = str2term |
1541 val t = str2term |
1541 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))"; |
1542 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))"; |
1542 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
1543 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
2075 " Try (Rewrite_Set cancel_p_rls False) @@ " ^ |
2076 " Try (Rewrite_Set cancel_p_rls False) @@ " ^ |
2076 " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^ |
2077 " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^ |
2077 " Try (Rewrite_Set discard_parentheses False)) " ^ |
2078 " Try (Rewrite_Set discard_parentheses False)) " ^ |
2078 " t_t)" |
2079 " t_t)" |
2079 ); |
2080 ); |
|
2081 (*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-. |
|
2082 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*) |