1.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Sep 16 12:20:00 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Sep 16 12:27:20 2013 +0200
1.3 @@ -37,6 +37,7 @@
1.4 "-------- investigate rulesets for cancel_p ----------------------------------";
1.5 "-------- fun eval_get_denominator -------------------------------------------";
1.6 "-------- several errpats in complicated term --------------------------------";
1.7 +"-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1.8 "-----------------------------------------------------------------------------";
1.9 "-----------------------------------------------------------------------------";
1.10
1.11 @@ -1638,4 +1639,122 @@
1.12 (([], Res), (5 + b) / (a * b + b ^^^ 2))] *)
1.13
1.14
1.15 +"-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1.16 +"-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1.17 +"-------- WN1309xx non-terminating rls norm_Rational -------------------------";
1.18 +(*------- Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1.19 +val t = str2term
1.20 + ("((12*x*y / (9*x^^^2 - y^^^2)) / (1 / (3*x - y)^^^2 - 1 / (3*x + y)^^^2)) * " ^
1.21 + "((1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2) / (20*x*y / (x^^^2 - 25*y^^^2)))");
1.22
1.23 +(*1st factor separately simplified *)
1.24 +val t = str2term "((12*x*y / (9*x^^^2 - y^^^2)) / (1 / (3*x - y)^^^2 - 1 / (3*x + y)^^^2))";
1.25 +val SOME (t', _) = rewrite_set_ thy false norm_Rational t;
1.26 +if term2str t' = "(-9 * x ^^^ 2 + y ^^^ 2) / -1" then () else error "Nr. 480b lhs changed";
1.27 +(*2nd factor separately simplified *)
1.28 +val t = str2term "((1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2) / (20*x*y / (x^^^2 - 25*y^^^2)))";
1.29 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.30 +if term2str t' = "-1 / (-1 * x ^^^ 2 + 25 * y ^^^ 2)" then () else error "Nr. 480b rhs changed";
1.31 +
1.32 +"-------- Schalk I, p.70 Nr. 477a: terms are exploding ?!?";
1.33 +val t = str2term ("b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /" ^
1.34 + "(b^^^2*y + b*y^^^2) * (a+x)^^^2 / ((b^^^2 - 4*y^^^2) * (a+2*x)^^^2)");
1.35 +(*val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.36 +:
1.37 +### rls: cancel_p on: (a ^^^ 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x ^^^ 2 * y)) /
1.38 +(b + -2 * y) /
1.39 +((b ^^^ 2 + -1 * y ^^^ 2) / (b + 2 * y)) /
1.40 +(b ^^^ 2 * y + b * y ^^^ 2) /
1.41 +(a ^^^ 2 * b ^^^ 2 + -4 * (a ^^^ 2 * y ^^^ 2) + 4 * (a * (b ^^^ 2 * x)) +
1.42 + -16 * (a * (x * y ^^^ 2)) +
1.43 + 4 * (b ^^^ 2 * x ^^^ 2) +
1.44 + -16 * (x ^^^ 2 * y ^^^ 2))
1.45 +exception Div raised
1.46 +
1.47 +BUT
1.48 +val t = str2term
1.49 + ("(a ^^^ 2 * (b * y) + 2 * (a * (b * (x * y))) + b * (x ^^^ 2 * y)) /" ^
1.50 + "(b + -2 * y) /" ^
1.51 + "((b ^^^ 2 + -1 * y ^^^ 2) / (b + 2 * y)) /" ^
1.52 + "(b ^^^ 2 * y + b * y ^^^ 2) /" ^
1.53 + "(a ^^^ 2 * b ^^^ 2 + -4 * (a ^^^ 2 * y ^^^ 2) + 4 * (a * (b ^^^ 2 * x)) +" ^
1.54 + "-16 * (a * (x * y ^^^ 2)) +" ^
1.55 + "4 * (b ^^^ 2 * x ^^^ 2) +" ^
1.56 + "-16 * (x ^^^ 2 * y ^^^ 2))");
1.57 +NONE = cancel_p_ thy t;
1.58 +*)
1.59 +
1.60 +(*------- Schalk I, p.70 Nr. 476b in 2003 this worked using 10 sec. *)
1.61 +val t = str2term
1.62 + ("((a^^^2 - b^^^2)/(2*a*b) + 2*a*b/(a^^^2 - b^^^2)) / ((a^^^2 + b^^^2)/(2*a*b) + 1) / " ^
1.63 + "((a^^^2 + b^^^2)^^^2 / (a + b)^^^2)");
1.64 +(*
1.65 +trace_rewrite := true;
1.66 +rewrite_set_ thy false norm_Rational t;
1.67 +:
1.68 +#### rls: cancel_p on: (2 * (a ^^^ 7 * b) + 4 * (a ^^^ 6 * b ^^^ 2) + 6 * (a ^^^ 5 * b ^^^ 3) +
1.69 + 8 * (a ^^^ 4 * b ^^^ 4) +
1.70 + 6 * (a ^^^ 3 * b ^^^ 5) +
1.71 + 4 * (a ^^^ 2 * b ^^^ 6) +
1.72 + 2 * (a * b ^^^ 7)) /
1.73 +(2 * (a ^^^ 9 * b) + 4 * (a ^^^ 8 * b ^^^ 2) +
1.74 + 2 * (2 * (a ^^^ 7 * b ^^^ 3)) +
1.75 + 4 * (a ^^^ 6 * b ^^^ 4) +
1.76 + -4 * (a ^^^ 4 * b ^^^ 6) +
1.77 + -4 * (a ^^^ 3 * b ^^^ 7) +
1.78 + -4 * (a ^^^ 2 * b ^^^ 8) +
1.79 + -2 * (a * b ^^^ 9))
1.80 +
1.81 +if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
1.82 +else error "rational.sml: diff.behav. in norm_Rational_mg 49";
1.83 +*)
1.84 +
1.85 +"-------- Schalk I, p.70 Nr. 480a: terms are exploding ?!?";
1.86 +val t = str2term ("(1/x + 1/y + 1/z) / (1/x - 1/y - 1/z) / " ^
1.87 + "(2*x^^^2 / (x^^^2 - z^^^2) / (x / (x + z) + x / (x - z)))");
1.88 +(*
1.89 +trace_rewrite := true;
1.90 +rewrite_set_ thy false norm_Rational t;
1.91 +:
1.92 +#### rls: cancel_p on: (2 * (x ^^^ 6 * (y ^^^ 2 * z)) + 2 * (x ^^^ 6 * (y * z ^^^ 2)) +
1.93 + 2 * (x ^^^ 5 * (y ^^^ 2 * z ^^^ 2)) +
1.94 + -2 * (x ^^^ 4 * (y ^^^ 2 * z ^^^ 3)) +
1.95 + -2 * (x ^^^ 4 * (y * z ^^^ 4)) +
1.96 + -2 * (x ^^^ 3 * (y ^^^ 2 * z ^^^ 4))) /
1.97 +(-2 * (x ^^^ 6 * (y ^^^ 2 * z)) + -2 * (x ^^^ 6 * (y * z ^^^ 2)) +
1.98 + 2 * (x ^^^ 5 * (y ^^^ 2 * z ^^^ 2)) +
1.99 + 2 * (x ^^^ 4 * (y ^^^ 2 * z ^^^ 3)) +
1.100 + 2 * (x ^^^ 4 * (y * z ^^^ 4)) +
1.101 + -2 * (x ^^^ 3 * (y ^^^ 2 * z ^^^ 4)))
1.102 +*)
1.103 +
1.104 +"-------- Schalk I, p.60 Nr. 215d: terms are exploding, internal loop does not terminate";
1.105 +val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.106 +(* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:
1.107 +
1.108 +val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1.109 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.110 +term2str t;
1.111 +"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";
1.112 +val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
1.113 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.114 +term2str t;
1.115 +"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";
1.116 +
1.117 +anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1.118 +
1.119 +"-------- Schalk I, p.70 Nr. 480b: terms are exploding, trace_rewrite stops at";
1.120 +val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
1.121 + "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1.122 + "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1.123 + "(20*x*y/(x^^^2 - 25*y^^^2))");
1.124 +(*val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.125 +:
1.126 +#### rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) +
1.127 + 108240 * (x ^^^ 4 * y ^^^ 6) +
1.128 + -6000 * (x ^^^ 2 * y ^^^ 8)) /
1.129 +(2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) +
1.130 + 1362000 * (x ^^^ 4 * y ^^^ 6) +
1.131 + -150000 * (x ^^^ 2 * y ^^^ 8))
1.132 +*)
1.133 +
2.1 --- a/test/Tools/isac/Test_Isac.thy Mon Sep 16 12:20:00 2013 +0200
2.2 +++ b/test/Tools/isac/Test_Isac.thy Mon Sep 16 12:27:20 2013 +0200
2.3 @@ -155,6 +155,9 @@
2.4 subsection {* isac on Isabelle2013 *}
2.5 subsubsection {* Summary of development *}
2.6 text {*
2.7 + #
2.8 + # Sep.13: integrated gcd_poly (functional, without Unsychronized.ref) into
2.9 + simplification of multivariate rationals (without improving the rulesets involved).
2.10 *}
2.11 subsubsection {* Run tests *}
2.12 text {*