# HG changeset patch # User Walther Neuper # Date 1379327240 -7200 # Node ID 7f3760f39bdcf8bd43d242f0210377d2cb62b361 # Parent 2786cc9704c80a1ae1845cbd4a8d4480a3815ee4 review of examples for non-termination of rls norm_Rational diff -r 2786cc9704c8 -r 7f3760f39bdc test/Tools/isac/Knowledge/rational.sml --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 16 12:20:00 2013 +0200 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 16 12:27:20 2013 +0200 @@ -37,6 +37,7 @@ "-------- investigate rulesets for cancel_p ----------------------------------"; "-------- fun eval_get_denominator -------------------------------------------"; "-------- several errpats in complicated term --------------------------------"; +"-------- WN1309xx non-terminating rls norm_Rational -------------------------"; "-----------------------------------------------------------------------------"; "-----------------------------------------------------------------------------"; @@ -1638,4 +1639,122 @@ (([], Res), (5 + b) / (a * b + b ^^^ 2))] *) +"-------- WN1309xx non-terminating rls norm_Rational -------------------------"; +"-------- WN1309xx non-terminating rls norm_Rational -------------------------"; +"-------- WN1309xx non-terminating rls norm_Rational -------------------------"; +(*------- Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*) +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)))"); +(*1st factor separately simplified *) +val t = str2term "((12*x*y / (9*x^^^2 - y^^^2)) / (1 / (3*x - y)^^^2 - 1 / (3*x + y)^^^2))"; +val SOME (t', _) = rewrite_set_ thy false norm_Rational t; +if term2str t' = "(-9 * x ^^^ 2 + y ^^^ 2) / -1" then () else error "Nr. 480b lhs changed"; +(*2nd factor separately simplified *) +val t = str2term "((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 t; term2str t'; +if term2str t' = "-1 / (-1 * x ^^^ 2 + 25 * y ^^^ 2)" then () else error "Nr. 480b rhs changed"; + +"-------- Schalk I, p.70 Nr. 477a: terms are exploding ?!?"; +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 t; +: +### rls: cancel_p on: (a ^^^ 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x ^^^ 2 * y)) / +(b + -2 * y) / +((b ^^^ 2 + -1 * y ^^^ 2) / (b + 2 * y)) / +(b ^^^ 2 * y + b * y ^^^ 2) / +(a ^^^ 2 * b ^^^ 2 + -4 * (a ^^^ 2 * y ^^^ 2) + 4 * (a * (b ^^^ 2 * x)) + + -16 * (a * (x * y ^^^ 2)) + + 4 * (b ^^^ 2 * x ^^^ 2) + + -16 * (x ^^^ 2 * y ^^^ 2)) +exception Div raised + +BUT +val t = str2term + ("(a ^^^ 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x ^^^ 2 * y)) /" ^ + "(b + -2 * y) /" ^ + "((b ^^^ 2 + -1 * y ^^^ 2) / (b + 2 * y)) /" ^ + "(b ^^^ 2 * y + b * y ^^^ 2) /" ^ + "(a ^^^ 2 * b ^^^ 2 + -4 * (a ^^^ 2 * y ^^^ 2) + 4 * (a * (b ^^^ 2 * x)) +" ^ + "-16 * (a * (x * y ^^^ 2)) +" ^ + "4 * (b ^^^ 2 * x ^^^ 2) +" ^ + "-16 * (x ^^^ 2 * y ^^^ 2))"); +NONE = cancel_p_ thy t; +*) + +(*------- Schalk I, p.70 Nr. 476b in 2003 this worked using 10 sec. *) +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)"); +(* +trace_rewrite := true; +rewrite_set_ thy false norm_Rational t; +: +#### rls: cancel_p on: (2 * (a ^^^ 7 * b) + 4 * (a ^^^ 6 * b ^^^ 2) + 6 * (a ^^^ 5 * b ^^^ 3) + + 8 * (a ^^^ 4 * b ^^^ 4) + + 6 * (a ^^^ 3 * b ^^^ 5) + + 4 * (a ^^^ 2 * b ^^^ 6) + + 2 * (a * b ^^^ 7)) / +(2 * (a ^^^ 9 * b) + 4 * (a ^^^ 8 * b ^^^ 2) + + 2 * (2 * (a ^^^ 7 * b ^^^ 3)) + + 4 * (a ^^^ 6 * b ^^^ 4) + + -4 * (a ^^^ 4 * b ^^^ 6) + + -4 * (a ^^^ 3 * b ^^^ 7) + + -4 * (a ^^^ 2 * b ^^^ 8) + + -2 * (a * b ^^^ 9)) + +if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then () +else error "rational.sml: diff.behav. in norm_Rational_mg 49"; +*) + +"-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?"; +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)))"); +(* +trace_rewrite := true; +rewrite_set_ thy false norm_Rational t; +: +#### rls: cancel_p on: (2 * (x ^^^ 6 * (y ^^^ 2 * z)) + 2 * (x ^^^ 6 * (y * z ^^^ 2)) + + 2 * (x ^^^ 5 * (y ^^^ 2 * z ^^^ 2)) + + -2 * (x ^^^ 4 * (y ^^^ 2 * z ^^^ 3)) + + -2 * (x ^^^ 4 * (y * z ^^^ 4)) + + -2 * (x ^^^ 3 * (y ^^^ 2 * z ^^^ 4))) / +(-2 * (x ^^^ 6 * (y ^^^ 2 * z)) + -2 * (x ^^^ 6 * (y * z ^^^ 2)) + + 2 * (x ^^^ 5 * (y ^^^ 2 * z ^^^ 2)) + + 2 * (x ^^^ 4 * (y ^^^ 2 * z ^^^ 3)) + + 2 * (x ^^^ 4 * (y * z ^^^ 4)) + + -2 * (x ^^^ 3 * (y ^^^ 2 * z ^^^ 4))) +*) + +"-------- Schalk I, p.60 Nr. 215d: terms are exploding, internal loop does not terminate"; +val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)"; +(* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt: + +val t = str2term "(a-b)^^^3 * (x+y)^^^4"; +val SOME (t, _) = rewrite_set_ thy false norm_Rational t; +term2str t; +"a^^^3 * x^^^4 + 4 * a^^^3 * x^^^3 * y +6 * a^^^3 * x^^^2 * y^^^2 +4 * a^^^3 * x * y^^^3 +a^^^3 * y^^^4 +-3 * a^^^2 * b * x^^^4 +-12 * a^^^2 * b * x^^^3 * y +-18 * a^^^2 * b * x^^^2 * y^^^2 +-12 * a^^^2 * b * x * y^^^3 +-3 * a^^^2 * b * y^^^4 +3 * a * b^^^2 * x^^^4 +12 * a * b^^^2 * x^^^3 * y +18 * a * b^^^2 * x^^^2 * y^^^2 +12 * a * b^^^2 * x * y^^^3 +3 * a * b^^^2 * y^^^4 +-1 * b^^^3 * x^^^4 +-4 * b^^^3 * x^^^3 * y +-6 * b^^^3 * x^^^2 * y^^^2 +-4 * b^^^3 * x * y^^^3 +-1 * b^^^3 * y^^^4"; +val t = str2term "((x+y)^^^2 * (a-b)^^^5)"; +val SOME (t, _) = rewrite_set_ thy false norm_Rational t; +term2str t; +"a^^^5 * x^^^2 + 2 * a^^^5 * x * y + a^^^5 * y^^^2 +-5 * a^^^4 * b * x^^^2 +-10 * a^^^4 * b * x * y +-5 * a^^^4 * b * y^^^2 +10 * a^^^3 * b^^^2 * x^^^2 +20 * a^^^3 * b^^^2 * x * y +10 * a^^^3 * b^^^2 * y^^^2 +-10 * a^^^2 * b^^^3 * x^^^2 +-20 * a^^^2 * b^^^3 * x * y +-10 * a^^^2 * b^^^3 * y^^^2 +5 * a * b^^^4 * x^^^2 +10 * a * b^^^4 * x * y +5 * a * b^^^4 * y^^^2 +-1 * b^^^5 * x^^^2 +-2 * b^^^5 * x * y +-1 * b^^^5 * y^^^2"; + +anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*) + +"-------- Schalk I, p.70 Nr. 480b: terms are exploding, trace_rewrite stops at"; +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 t; +: +#### rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) + + 108240 * (x ^^^ 4 * y ^^^ 6) + + -6000 * (x ^^^ 2 * y ^^^ 8)) / +(2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) + + 1362000 * (x ^^^ 4 * y ^^^ 6) + + -150000 * (x ^^^ 2 * y ^^^ 8)) +*) + diff -r 2786cc9704c8 -r 7f3760f39bdc test/Tools/isac/Test_Isac.thy --- a/test/Tools/isac/Test_Isac.thy Mon Sep 16 12:20:00 2013 +0200 +++ b/test/Tools/isac/Test_Isac.thy Mon Sep 16 12:27:20 2013 +0200 @@ -155,6 +155,9 @@ subsection {* isac on Isabelle2013 *} subsubsection {* Summary of development *} text {* + # + # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into + simplification of multivariate rationals (without improving the rulesets involved). *} subsubsection {* Run tests *} text {*