1.1 --- a/src/smltest/IsacKnowledge/rational.sml Sat Aug 20 18:04:54 2005 +0200
1.2 +++ b/src/smltest/IsacKnowledge/rational.sml Sat Aug 20 18:04:54 2005 +0200
1.3 @@ -1,9 +1,7 @@
1.4 (*.tests for rationals
1.5 - Stefan Karnel
1.6 - 2002
1.7 - use"../kbtest/rational.sml";
1.8 - use"kbtest/rational.sml";
1.9 - use"rational.sml";
1.10 + (c) Stefan Karnel 2002
1.11 +
1.12 +use"~/proto2/isac/src/smltest/IsacKnowledge/rational.sml";
1.13 .*)
1.14
1.15
1.16 @@ -1069,7 +1067,7 @@
1.17 if (term2str t) =
1.18 "19 / 21"
1.19 then ()
1.20 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.21 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
1.22
1.23 (*Schalk I, p.40 Nr. 166a *)
1.24 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1.25 @@ -1078,7 +1076,7 @@
1.26 if (term2str t) =
1.27 "45 / 2"
1.28 then ()
1.29 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.30 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
1.31
1.32
1.33 (*----------------------------------------------------------------------*)
1.34 @@ -1093,7 +1091,7 @@
1.35 if (term2str t) =
1.36 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.37 then ()
1.38 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.39 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
1.40
1.41 (* e192b Stefan K.*)
1.42 val t = str2term
1.43 @@ -1103,7 +1101,7 @@
1.44 if (term2str t) =
1.45 "x ^^^ 2 / y ^^^ 2"
1.46 then ()
1.47 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.48 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
1.49
1.50 (*Schalk I, p.66 Nr. 379c *)
1.51 val t = str2term
1.52 @@ -1113,7 +1111,7 @@
1.53 if (term2str t) =
1.54 "-1"
1.55 then ()
1.56 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.57 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
1.58
1.59 (*Schalk I, p.66 Nr. 380b *)
1.60 val t = str2term
1.61 @@ -1123,7 +1121,7 @@
1.62 if (term2str t) =
1.63 "(27 + 12 * x) / (28 + 8 * x)"
1.64 then ()
1.65 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.66 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1.67
1.68 (*Schalk I, p.60 Nr. 215c *)
1.69 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter kürzen!!!*)
1.70 @@ -1134,7 +1132,7 @@
1.71 if (term2str t) =
1.72 "(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.73 then ()
1.74 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.75 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
1.76 *)
1.77 (*val t = str2term
1.78 "(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.79 @@ -1152,7 +1150,7 @@
1.80 if (term2str t) =
1.81 "(a + b) / (4 * a + -4 * b)"
1.82 then ()
1.83 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.84 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1.85 *)
1.86
1.87 (*Schalk I, p.66 Nr. 381b *)
1.88 @@ -1163,7 +1161,7 @@
1.89 if (term2str t) =
1.90 "-1 / (5 + -2 * x)"
1.91 then ()
1.92 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.93 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
1.94
1.95 (*Schalk I, p.66 Nr. 381c *)
1.96 val t = str2term
1.97 @@ -1173,7 +1171,7 @@
1.98 if (term2str t) =
1.99 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.100 then ()
1.101 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.102 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
1.103
1.104 (*Schalk I, p.66 Nr. 383a *)
1.105 val t = str2term
1.106 @@ -1183,7 +1181,7 @@
1.107 if (term2str t) =
1.108 "5 * a / (a + -1 * b)"
1.109 then ()
1.110 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.111 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
1.112
1.113 (*----------------------------------------------------------------------*)
1.114 (*------------------------- Gemeinsamer Nenner ------------------------*)
1.115 @@ -1197,7 +1195,7 @@
1.116 if (term2str t) =
1.117 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1.118 then ()
1.119 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.120 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
1.121
1.122 (*Schalk I, p.67 Nr. 407b *)
1.123 val t = str2term
1.124 @@ -1207,7 +1205,7 @@
1.125 if (term2str t) =
1.126 "4 / c"
1.127 then ()
1.128 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.129 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
1.130
1.131 (*Schalk I, p.67 Nr. 410b *)
1.132 val t = str2term
1.133 @@ -1217,7 +1215,7 @@
1.134 if (term2str t) =
1.135 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1.136 then ()
1.137 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.138 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
1.139
1.140 (*Schalk I, p.67 Nr. 413b *)
1.141 val t = str2term
1.142 @@ -1227,7 +1225,7 @@
1.143 if (term2str t) =
1.144 "6 * x / (1 + -1 * x ^^^ 2)"
1.145 then ()
1.146 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.147 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
1.148
1.149 (*Schalk I, p.68 Nr. 414a *)
1.150 val t = str2term
1.151 @@ -1237,7 +1235,7 @@
1.152 if (term2str t) =
1.153 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1.154 then ()
1.155 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.156 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
1.157
1.158 (*Schalk I, p.68 Nr. 423a *)
1.159 val t = str2term
1.160 @@ -1247,7 +1245,7 @@
1.161 if (term2str t) =
1.162 "1"
1.163 then ()
1.164 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.165 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
1.166
1.167 (*Schalk I, p.68 Nr. 428b *)
1.168 val t = str2term
1.169 @@ -1257,7 +1255,7 @@
1.170 if (term2str t) =
1.171 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1.172 then ()
1.173 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.174 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
1.175
1.176 (*Schalk I, p.68 Nr. 430b *)
1.177 val t = str2term
1.178 @@ -1267,7 +1265,7 @@
1.179 if (term2str t) =
1.180 "a + 3 * b"
1.181 then ()
1.182 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.183 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
1.184
1.185
1.186 (*Schalk I, p.68 Nr. 432 *)
1.187 @@ -1278,7 +1276,7 @@
1.188 if (term2str t) =
1.189 "0"
1.190 then ()
1.191 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.192 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
1.193
1.194 (*Eigenes*)
1.195 val t = str2term
1.196 @@ -1288,7 +1286,7 @@
1.197 if (term2str t) =
1.198 "(3 * y + b * x) / (b * y)"
1.199 then ()
1.200 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.201 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
1.202
1.203
1.204
1.205 @@ -1304,7 +1302,7 @@
1.206 if (term2str t) =
1.207 "(5 * x + -5 * y) / (18 * x + 18 * y)"
1.208 then ()
1.209 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.210 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1.211
1.212 (*Schalk I, p.68 Nr. 436b *)
1.213 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1.214 @@ -1313,7 +1311,7 @@
1.215 if (term2str t) =
1.216 "5 * a / (a + -1 * b)"
1.217 then ()
1.218 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.219 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1.220
1.221 (*Schalk I, p.68 Nr. 437a *)
1.222 (* SK loops: rechnet ewig; cancel_p hängt sich auf...
1.223 @@ -1362,7 +1360,7 @@
1.224 if (term2str t) =
1.225 "x ^^^ 2"
1.226 then ()
1.227 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.228 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.229
1.230 (*Schalk I, p.68 Nr. 439b *)
1.231 val t = str2term
1.232 @@ -1372,7 +1370,7 @@
1.233 if (term2str t) =
1.234 "(x + -4 * x ^^^ 3) / 2"
1.235 then ()
1.236 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.237 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
1.238
1.239 (*Schalk I, p.68 Nr. 440a *)
1.240 val t = str2term
1.241 @@ -1382,7 +1380,7 @@
1.242 if (term2str t) =
1.243 "(-3 + x) / (2 + x)"
1.244 then ()
1.245 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.246 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.247
1.248 (*Schalk I, p.68 Nr. 440b *)
1.249 (* Achtung: rechnet ewig; cancel_p hängt sich auf...
1.250 @@ -1393,7 +1391,7 @@
1.251 if (term2str t) =
1.252
1.253 then ()
1.254 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.255 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27";
1.256
1.257 val t = str2term
1.258 "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1.259 @@ -1416,7 +1414,7 @@
1.260 if (term2str t) =
1.261 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.262 then ()
1.263 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.264 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.265
1.266 (*Schalk I, p.69 Nr. 442b *)
1.267 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)";
1.268 @@ -1425,7 +1423,7 @@
1.269 if (term2str t) =
1.270 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.271 then ()
1.272 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.273 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1.274
1.275 (*Schalk I, p.69 Nr. 443b *)
1.276 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1.277 @@ -1434,7 +1432,7 @@
1.278 if (term2str t) =
1.279 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.280 then ()
1.281 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.282 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1.283
1.284 (*Schalk I, p.69 Nr. 445b *)
1.285 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1.286 @@ -1443,7 +1441,7 @@
1.287 if (term2str t) =
1.288 "a ^^^ 3 / 27"
1.289 then ()
1.290 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.291 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1.292
1.293 (*Schalk I, p.69 Nr. 446b *)
1.294 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1.295 @@ -1452,7 +1450,7 @@
1.296 if (term2str t) =
1.297 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.298 then ()
1.299 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.300 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1.301
1.302 (*Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.303 val t = str2term
1.304 @@ -1462,7 +1460,7 @@
1.305 if (term2str t) =
1.306 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.307 then ()
1.308 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.309 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.310
1.311 (*Schalk I, p.69 Nr. 450a *)
1.312 val t = str2term
1.313 @@ -1472,7 +1470,7 @@
1.314 if (term2str t) =
1.315 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.316 then ()
1.317 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.318 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1.319
1.320
1.321 (*----------------------------------------------------------------------*)
1.322 @@ -1487,7 +1485,7 @@
1.323 if (term2str t) =
1.324 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.325 then ()
1.326 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.327 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1.328
1.329 (*Schalk I, p.69 Nr. 455a *)
1.330 val t = str2term
1.331 @@ -1497,7 +1495,7 @@
1.332 if (term2str t) =
1.333 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)"
1.334 then ()
1.335 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.336 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1.337
1.338 (*Schalk I, p.69 Nr. 455b *)
1.339 (* Achtung: Endlosschleife
1.340 @@ -1508,7 +1506,7 @@
1.341 if (term2str t) =
1.342
1.343 then ()
1.344 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.345 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1.346
1.347 val t = str2term
1.348 "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1.349 @@ -1544,7 +1542,7 @@
1.350 if (term2str t) =
1.351 "b / (1 + 2 * b + b ^^^ 2)"
1.352 then ()
1.353 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.354 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1.355
1.356 (*Schalk I, p.69 Nr. 457b *)
1.357 val t = str2term
1.358 @@ -1554,7 +1552,7 @@
1.359 if (term2str t) =
1.360 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.361 then ()
1.362 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.363 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.364
1.365 (*Schalk I, p.69 Nr. 458b *)
1.366 (* Achtung: rechnet ewig; cancel_p hängt sich auf...
1.367 @@ -1565,7 +1563,7 @@
1.368 if (term2str t) =
1.369
1.370 then ()
1.371 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.372 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 40";
1.373 *)
1.374
1.375 (*Schalk I, p.69 Nr. 459b *)
1.376 @@ -1576,7 +1574,7 @@
1.377 if (term2str t) =
1.378 "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"
1.379 then ()
1.380 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.381 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1.382
1.383
1.384 (*Schalk I, p.69 Nr. 460b *)
1.385 @@ -1588,7 +1586,7 @@
1.386 if (term2str t) =
1.387
1.388 then ()
1.389 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.390 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1.391
1.392 val t = str2term
1.393 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.394 @@ -1607,7 +1605,7 @@
1.395 if (term2str t) =
1.396 "x + y"
1.397 then ()
1.398 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.399 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1.400
1.401 (*----------------------------------------------------------------------*)
1.402 (*---------------------- Einfache Dppelbrüche --------------------------*)
1.403 @@ -1621,7 +1619,7 @@
1.404 if (term2str t) =
1.405 "1 / 2"
1.406 then ()
1.407 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.408 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1.409
1.410 (*Schalk I, p.69 Nr. 464b *)
1.411 val t = str2term
1.412 @@ -1631,7 +1629,7 @@
1.413 if (term2str t) =
1.414 "(3 + -1 * a) / (1 + -1 * a)"
1.415 then ()
1.416 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.417 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1.418
1.419 (*Schalk I, p.69 Nr. 465b *)
1.420 val t = str2term
1.421 @@ -1641,7 +1639,7 @@
1.422 if (term2str t) =
1.423 "(4 * x + 6 * y + -9 * z) / (4 * x)"
1.424 then ()
1.425 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.426 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1.427
1.428 (*Schalk I, p.69 Nr. 466b *)
1.429 val t = str2term
1.430 @@ -1651,7 +1649,7 @@
1.431 if (term2str t) =
1.432 "(25 + -10 * x + x ^^^ 2) / 18"
1.433 then ()
1.434 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.435 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1.436
1.437 (*Schalk I, p.70 Nr. 469 *)
1.438 val t = str2term
1.439 @@ -1661,7 +1659,7 @@
1.440 if (term2str t) =
1.441 "3 * b ^^^ 3 / (2 * a + -2 * b)"
1.442 then ()
1.443 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.444 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1.445
1.446 (*----------------------------------------------------------------------*)
1.447 (*---------------------- Mehrfache Dppelbrüche -------------------------*)
1.448 @@ -1675,7 +1673,7 @@
1.449 if (term2str t) =
1.450 "1 / (a ^^^ 2 + -1 * b ^^^ 2)"
1.451 then ()
1.452 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.453 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1.454
1.455 (*Schalk I, p.70 Nr. 477a *)
1.456 (* Achtung: rechnet ewig; Bsp zu komplex;
1.457 @@ -1687,7 +1685,7 @@
1.458 if (term2str t) =
1.459
1.460 then ()
1.461 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.462 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 50";
1.463
1.464 val t = str2term
1.465 "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)";
1.466 @@ -1702,11 +1700,12 @@
1.467 "(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)))";
1.468 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.469 term2str t;
1.470 +(* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
1.471 if (term2str t) =
1.472 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.473 then ()
1.474 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.475 -
1.476 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.477 +-----------------------------------------------------------------------*)
1.478
1.479 (*Schalk I, p.70 Nr. 480a *)
1.480 (* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen:
1.481 @@ -1717,7 +1716,7 @@
1.482 if (term2str t) =
1.483
1.484 then ()
1.485 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.486 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1.487
1.488 (* Berechne Zwischenergebnisse:*)
1.489 val t = str2term
1.490 @@ -1922,7 +1921,7 @@
1.491 if (term2str t) =
1.492 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
1.493 then ()
1.494 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg";
1.495 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
1.496
1.497
1.498
2.1 --- a/src/smltest/IsacKnowledge/rlang.sml Sat Aug 20 18:04:54 2005 +0200
2.2 +++ b/src/smltest/IsacKnowledge/rlang.sml Sat Aug 20 18:04:54 2005 +0200
2.3 @@ -703,6 +703,7 @@
2.4 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = R * R2 / (R2 + -1 * R)]")) => ()
2.5 | _ => raise error "rlang.sml: diff.behav. in 98a(1) [R1 = ...]";
2.6 if get_assumptions_ pt p = [(str2term"R * R2 * R2 ~= (R2 + -1 * R) * 0",[]),
2.7 + (str2term"R2 + -1 * R ~= 0",[]),
2.8 (str2term"R2 + -1 * R ~= 0",[])]
2.9 then writeln "asm should be simplified"
2.10 else raise error "rlang.sml: diff.behav. in 98a(1) asm";
2.11 @@ -800,10 +801,11 @@
2.12 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2),\n x = -1 * sqrt ((a ^^^ 2 * b ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2) / b ^^^ 2)]")) => writeln"should be simplified MG"
2.13 | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
2.14 val asms = get_assumptions_ pt p;
2.15 -if asms = [(str2term"b ^^^ 2 ~= 0", []),
2.16 +if asms = [(str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", []),
2.17 + (str2term"b ^^^ 2 ~= 0", []),
2.18 (str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", []),
2.19 - (str2term"b ^^^ 2 ~= 0", []),
2.20 - (str2term"0 * b ^^^ 2 <= -1 * (a ^^^ 2 * y ^^^ 2 + -1 * a ^^^ 2 * b ^^^ 2)", [])] then writeln"should be simplified MG"
2.21 + (str2term"b ^^^ 2 ~= 0", [])
2.22 + ] then writeln"should be simplified MG"
2.23 else raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) asms";
2.24
2.25 (*----------------- Schalk I s.102 Bsp 268(1) ------------------------*)