1.1 --- a/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 16:46:29 2006 +0200
1.2 +++ b/src/smltest/IsacKnowledge/rational.sml Tue Sep 05 16:54:36 2006 +0200
1.3 @@ -1052,7 +1052,8 @@
1.4 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1.5 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1.6 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n";
1.7 -WN060831????SK7
1.8 +WN060831????SK7
1.9 +
1.10 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.11 val None = add_fraction_p_ thy t;
1.12 *)
1.13 @@ -1077,7 +1078,7 @@
1.14 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
1.15
1.16 (* ------------------------------------------------------------------- *)
1.17 -(* Simplifier für beliebige Buchterme *)
1.18 +(* Simplifier fr beliebige Buchterme *)
1.19 (* ------------------------------------------------------------------- *)
1.20 (*----------------------- norm_Rational_mg --------------------------*)
1.21 (* ------------------------------------------------------------------- *)
1.22 @@ -1151,8 +1152,8 @@
1.23 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1.24
1.25 (*Schalk I, p.60 Nr. 215c *)
1.26 -(* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter kürzen!!!*)
1.27 -(* WN060831????MG1
1.28 +(* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
1.29 +(* WN060831????MG1
1.30 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1.31 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.32 term2str t;
1.33 @@ -1341,13 +1342,16 @@
1.34 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1.35
1.36 (*Schalk I, p.68 Nr. 437a *)
1.37 -(* SK loops: rechnet ewig; cancel_p hängt sich auf... WN060420????MG4
1.38 +(* SK loops: rechnet ewig; cancel_p h???gt sich auf... WN060420????MG4 *)
1.39 +(* corrected *)
1.40 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.41 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.42 -term2str t;
1.43 -*)
1.44 +if (term2str t) = "1 / (4 * c + 3 * e)" then ()
1.45 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.46 +(**)
1.47
1.48 (*SK loops .. WN060420????MG5 not canceled to "1 / (4*c + 3*e)"*)
1.49 +(* corrected *)
1.50 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1.51 val Some (t',_) = rewrite_set_ thy false make_polynomial t;
1.52 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)";
1.53 @@ -1355,25 +1359,28 @@
1.54 "----- SK060904-1b non-termination of cancel_p_";
1.55 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.56 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.57 -(* WN060831????SK8
1.58 +(* WN060831????SK8*)
1.59 val Some (t',_) = rewrite_set_ thy false cancel_p t'';
1.60 term2str t';
1.61 -*)
1.62 +
1.63 +(**)
1.64
1.65 (*Schalk I, p.68 Nr. 437b *)
1.66 -(* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter kürzen!!!
1.67 +(* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter krzen!!! *)
1.68 val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.69 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.70 term2str t; WN060831????SK9
1.71 "(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)";
1.72
1.73 -*)
1.74 +(**)
1.75
1.76 -(*
1.77 +(* *)
1.78 val t = str2term
1.79 -"(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
1.80 +"(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)";
1.81 +(* WN060831????SK10 *)
1.82 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.83 term2str t;
1.84 +(*
1.85 uncaught exception nonexhaustive binding failure
1.86 raised at: stdIn:270.1-270.51
1.87 *)
1.88 @@ -1408,8 +1415,8 @@
1.89 then ()
1.90 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.91
1.92 -"----- Schalk I, p.68 Nr. 440b";
1.93 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831????SK11
1.94 +(*Schalk I, p.68 Nr. 440b *)
1.95 +(* Achtung: rechnet ewig; cancel_p h???gt sich auf... WN060831????SK11
1.96 val t = str2term
1.97 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1.98 trace_rewrite := true;
1.99 @@ -1435,73 +1442,103 @@
1.100 "-------- common denominator and multiplication ------------------";
1.101 "-------- common denominator and multiplication ------------------";
1.102 "-------- common denominator and multiplication ------------------";
1.103 +
1.104 (*----------------------------------------------------------------------*)
1.105 -(*--------- Gemeinsamer Nenner und Multiplikation von Brüchen ----------*)
1.106 +(*--------- Gemeinsamer Nenner und Multiplikation von Brchen ----------*)
1.107 (*----------------------------------------------------------------------*)
1.108
1.109 -"----- SRAM Schalk I, p.69 Nr. 441b";
1.110 +
1.111 +(*SRAM Schalk I, p.69 Nr. 441b *)
1.112 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1.113 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.114 +term2str t;
1.115 if (term2str t) =
1.116 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.117 -then() else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.118 +then ()
1.119 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.120
1.121 -"----- SRAM Schalk I, p.69 Nr. 442b";
1.122 +(*SRAM Schalk I, p.69 Nr. 442b *)
1.123 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.124 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.125 -if (term2str t) = "5 * x ^^^ 2 / (a * b ^^^ 3 * c)" then ()
1.126 +term2str t;
1.127 +if (term2str t) =
1.128 +"5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.129 +then ()
1.130 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1.131
1.132 -"----- SRAM Schalk I, p.69 Nr. 443b";
1.133 +(*SRAM Schalk I, p.69 Nr. 443b *)
1.134 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1.135 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.136 -if (term2str t) ="(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36" then ()
1.137 +term2str t;
1.138 +if (term2str t) =
1.139 +"(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.140 +then ()
1.141 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1.142
1.143 -"----- SRAM Schalk I, p.69 Nr. 445b";
1.144 +(*SRAM Schalk I, p.69 Nr. 445b *)
1.145 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1.146 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.147 -if (term2str t) = "a ^^^ 3 / 27" then ()
1.148 +term2str t;
1.149 +if (term2str t) =
1.150 +"a ^^^ 3 / 27"
1.151 +then ()
1.152 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1.153
1.154 -"----- SRAM Schalk I, p.69 Nr. 446b";
1.155 +(*SRAM Schalk I, p.69 Nr. 446b *)
1.156 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1.157 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.158 -if (term2str t) = "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2" then ()
1.159 +term2str t;
1.160 +if (term2str t) =
1.161 +"30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.162 +then ()
1.163 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1.164
1.165 -"----- SRAM Schalk I, p.69 Nr. 449a Achtung: rechnet ca 8 Sekunden";
1.166 +(*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.167 val t = str2term
1.168 "(2*x^^^2/(3*y)+x/y^^^2)*(4*x^^^4/(9*y^^^2)+x^^^2/y^^^4)*(2*x^^^2/(3*y) - x/y^^^2)";
1.169 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.170 -if (term2str t) = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.171 -then() else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.172 +term2str t;
1.173 +if (term2str t) =
1.174 +"(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.175 +then ()
1.176 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.177
1.178 -"----- SRAM Schalk I, p.69 Nr. 450a";
1.179 +(*SRAM Schalk I, p.69 Nr. 450a *)
1.180 val t = str2term
1.181 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1.182 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.183 -if (term2str t) = "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)" then ()
1.184 +term2str t;
1.185 +if (term2str t) =
1.186 +"(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.187 +then ()
1.188 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1.189
1.190 "-------- double fractions ---------------------------------------";
1.191 "-------- double fractions ---------------------------------------";
1.192 "-------- double fractions ---------------------------------------";
1.193
1.194 -"----- SRD Schalk I, p.69 Nr. 454b";
1.195 -val t = str2term "((2 - x)/(2*a)) / (2*a/(x - 2))";
1.196 +(*SRD Schalk I, p.69 Nr. 454b *)
1.197 +val t = str2term
1.198 +"((2 - x)/(2*a)) / (2*a/(x - 2))";
1.199 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.200 -if (term2str t) = "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)" then ()
1.201 +term2str t;
1.202 +if (term2str t) =
1.203 +"(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.204 +then ()
1.205 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1.206
1.207 -"----- SRD Schalk I, p.69 Nr. 455a";
1.208 -val t = str2term "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.209 +(*SRD Schalk I, p.69 Nr. 455a *)
1.210 +val t = str2term
1.211 +"(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.212 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.213 -if (term2str t) = "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1.214 +term2str t;
1.215 +if (term2str t) =
1.216 +"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)"
1.217 +then ()
1.218 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1.219
1.220
1.221 -"----- Schalk I, p.69 Nr. 455b";
1.222 +(*Schalk I, p.69 Nr. 455b *)
1.223 (* Achtung: Endlosschleife
1.224 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.225 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.226 @@ -1519,7 +1556,7 @@
1.227 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"
1.228 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.229 term2str t;
1.230 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK*)
1.231 +(* Achtung: rechnet ewig; cancel_p h???gt sich auf... ????SK*)
1.232
1.233 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1.234 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.235 @@ -1531,25 +1568,31 @@
1.236 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.237 term2str t = "-1 / (3 + 1 * y)";
1.238 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1.239 -(*MG: -1 im Zähler der Angabe verursacht das Problem ! WN060831???MG!!SK0*)
1.240 +(*MG: -1 im Z???ler der Angabe verursacht das Problem ! WN060831???MG!!SK0*)
1.241 *)
1.242
1.243 -"----- SRD Schalk I, p.69 Nr. 456b";
1.244 -val t = str2term "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1.245 +(*SRD Schalk I, p.69 Nr. 456b *)
1.246 +val t = str2term
1.247 +"(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1.248 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.249 -if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1.250 +term2str t;
1.251 +if (term2str t) =
1.252 +"b / (1 + 2 * b + b ^^^ 2)"
1.253 +then ()
1.254 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1.255
1.256 -"----- SRD Schalk I, p.69 Nr. 457b";
1.257 +(*SRD Schalk I, p.69 Nr. 457b *)
1.258 val t = str2term
1.259 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1.260 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.261 +term2str t;
1.262 if (term2str t) =
1.263 -"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2" then ()
1.264 +"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.265 +then ()
1.266 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.267
1.268 -"----- Schalk I, p.69 Nr. 458b";
1.269 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK
1.270 +(*Schalk I, p.69 Nr. 458b *)
1.271 +(* Achtung: rechnet ewig; cancel_p h???gt sich auf... ????SK
1.272 val t = str2term
1.273 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1.274 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.275 @@ -1560,77 +1603,104 @@
1.276 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 40";
1.277 *)
1.278
1.279 -"----- SRD Schalk I, p.69 Nr. 459b";
1.280 -val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.281 +(*SRD Schalk I, p.69 Nr. 459b *)
1.282 +val t = str2term
1.283 +"(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.284 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.285 -if (term2str t) = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"then ()
1.286 +term2str t;
1.287 +if (term2str t) =
1.288 +"(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"
1.289 +then ()
1.290 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1.291
1.292 -"----- Schalk I, p.69 Nr. 460b";
1.293 -(* Achtung: rechnet ewig; cancel_p hängt sich auf... ????SK*)
1.294 +
1.295 +(*Schalk I, p.69 Nr. 460b *)
1.296 +(* Achtung: rechnet ewig; cancel_p h???gt sich auf... ????SK
1.297 val t = str2term
1.298 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.299 -(*
1.300 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.301 +term2str t;
1.302 if (term2str t) =
1.303 +
1.304 then ()
1.305 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1.306 -*)
1.307 +
1.308 val t = str2term
1.309 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.310 -val Some (t',_) = rewrite_set_ thy false make_polynomial t;
1.311 -term2str t' = "(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y +\n 144 * x ^^^ 2 * y) /\n(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.312 -(* ????SK NOT terminating
1.313 -val Some (t'',_) = rewrite_set_ thy false cancel_p t';
1.314 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.315 term2str t;
1.316 -*)
1.317 +"(-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)";
1.318 +val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.319 +term2str t;
1.320 + ????SK*)
1.321
1.322 -"----- SRD Schalk I, p.70 Nr. 472a";
1.323 +(*SRD Schalk I, p.70 Nr. 472a *)
1.324 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1.325 \((4*x - 8*y)/(x + y))";
1.326 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.327 -if (term2str t) = "x + y" then ()
1.328 +term2str t;
1.329 +if (term2str t) =
1.330 +"x + y"
1.331 +then ()
1.332 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1.333
1.334
1.335 (*----------------------------------------------------------------------*)
1.336 -(*---------------------- Einfache Dppelbrüche --------------------------*)
1.337 +(*---------------------- Einfache Dppelbrche --------------------------*)
1.338 (*----------------------------------------------------------------------*)
1.339
1.340 -"----- Schalk I, p.69 Nr. 461a";
1.341 -val t = str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.342 +(*SRD Schalk I, p.69 Nr. 461a *)
1.343 +val t = str2term
1.344 +"(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.345 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.346 -if (term2str t) = "1 / 2" then ()
1.347 +term2str t;
1.348 +if (term2str t) =
1.349 +"1 / 2"
1.350 +then ()
1.351 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1.352
1.353 -"----- SRD Schalk I, p.69 Nr. 464b";
1.354 -val t = str2term "(a - a/(a - 2)) / (a + a/(a - 2))";
1.355 +(*SRD Schalk I, p.69 Nr. 464b *)
1.356 +val t = str2term
1.357 +"(a - a/(a - 2)) / (a + a/(a - 2))";
1.358 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.359 -if (term2str t) = "(3 + -1 * a) / (1 + -1 * a)" then ()
1.360 +term2str t;
1.361 +if (term2str t) =
1.362 +"(3 + -1 * a) / (1 + -1 * a)"
1.363 +then ()
1.364 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1.365
1.366 -"----- SRD Schalk I, p.69 Nr. 465b";
1.367 -val t = str2term "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1.368 +(*SRD Schalk I, p.69 Nr. 465b *)
1.369 +val t = str2term
1.370 +"((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1.371 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.372 -if (term2str t) = "(4 * x + 6 * y + -9 * z) / (4 * x)" then ()
1.373 +term2str t;
1.374 +if (term2str t) =
1.375 +"(4 * x + 6 * y + -9 * z) / (4 * x)"
1.376 +then ()
1.377 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1.378
1.379 -"-----SRD Schalk I, p.69 Nr. 466b";
1.380 +(*SRD Schalk I, p.69 Nr. 466b *)
1.381 val t = str2term
1.382 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1.383 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.384 -if (term2str t) = "(25 + -10 * x + x ^^^ 2) / 18" then ()
1.385 +term2str t;
1.386 +if (term2str t) =
1.387 +"(25 + -10 * x + x ^^^ 2) / 18"
1.388 +then ()
1.389 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1.390
1.391 -"-----SRD Schalk I, p.70 Nr. 469";
1.392 +(*SRD Schalk I, p.70 Nr. 469 *)
1.393 val t = str2term
1.394 "3*b^^^2/(4*a^^^2 - 8*a*b + 4*b^^^2)/(a/(a^^^2*b - b^^^3) + (a - b)/(4*a*b^^^2+4*b^^^3) - 1/(4*b^^^2))";
1.395 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.396 -if (term2str t) = "3 * b ^^^ 3 / (2 * a + -2 * b)" then ()
1.397 +term2str t;
1.398 +if (term2str t) =
1.399 +"3 * b ^^^ 3 / (2 * a + -2 * b)"
1.400 +then ()
1.401 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1.402
1.403 (*----------------------------------------------------------------------*)
1.404 -(*---------------------- Mehrfache Dppelbrüche -------------------------*)
1.405 +(*---------------------- Mehrfache Dppelbrche -------------------------*)
1.406 (*----------------------------------------------------------------------*)
1.407
1.408 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1.409 @@ -1646,7 +1716,7 @@
1.410
1.411 "----- Schalk I, p.70 Nr. 477a";
1.412 (* Achtung: rechnet ewig; Bsp zu komplex;
1.413 - Lösung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1.414 + L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1.415 val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
1.416 \(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1.417 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.418 @@ -1664,24 +1734,23 @@
1.419 /\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)";
1.420 *)
1.421
1.422 -"----- Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec";
1.423 +(*Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec *)
1.424 val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
1.425 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1.426 val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.427 term2str t';
1.428 (* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
1.429 - ???MG
1.430 + ????SK ???MG
1.431 if term2str t' =
1.432 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.433 then ()
1.434 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.435 -*)
1.436 +-----------------------------------------------------------------------*)
1.437
1.438 (*Schalk I, p.70 Nr. 480a *)
1.439 -(* WN060831????SK NOT terminating*)
1.440 +(* SK Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831????SK00
1.441 val t = str2term
1.442 "(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)))";
1.443 -(*
1.444 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.445 term2str t;
1.446 if (term2str t) =
1.447 @@ -1702,7 +1771,7 @@
1.448 term2str t;
1.449 "1"
1.450
1.451 -(* SK 1. Ausdruck kann nicht weiter gekürzt werden; cancel_p !!!*)
1.452 +(* SK 1. Ausdruck kann nicht weiter gekrzt werden; cancel_p !!!*)
1.453 ### rls: cancel_p on:
1.454 (x ^^^ 2 * (y ^^^ 2 * z) + x ^^^ 2 * (y * z ^^^ 2) + x * (y ^^^ 2 * z ^^^ 2)) /
1.455 (-1 * (x ^^^ 2 * (y ^^^ 2 * z)) + -1 * (x ^^^ 2 * (y * z ^^^ 2)) + x * (y ^^^ 2 * z ^^^ 2))
1.456 @@ -1714,13 +1783,18 @@
1.457 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.458 term2str t;
1.459 (*uncaught exception nonexhaustive binding failure*)
1.460 -*)
1.461
1.462 -(*MG Das kann er aber kürzen !!????: *)
1.463 +(* Das kann er aber krzen !!????: *)
1.464 val t = str2term
1.465 "(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1.466 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.467 -term2str t = "(-1 * (y * x) + -1 * (z * y)) / (z * x + -1 * (z * y))";
1.468 +term2str t;
1.469 +"(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1.470 +*)
1.471 +
1.472 +
1.473 +
1.474 +
1.475
1.476
1.477 (*--------------------------------------------------------------------*)
1.478 @@ -1734,7 +1808,7 @@
1.479 term2str t;
1.480 *)
1.481
1.482 -(* Kein Wunder, denn Zähler und Nenner extra als Polynom dargestellt ergibt:*)
1.483 +(* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
1.484 (*
1.485 val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1.486 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.487 @@ -1745,7 +1819,7 @@
1.488 term2str t;
1.489 "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";
1.490 *)
1.491 -(*anscheinend macht dem Rechner das Kürzen diese Bruches keinen Spass mehr ...*)
1.492 +(*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1.493
1.494 (*--------------------------------------------------------------------*)
1.495 (*Schalk I, p.70 Nr. 480b *)
1.496 @@ -1804,7 +1878,7 @@
1.497
1.498 (*--------------------------------------------------------------------*)
1.499 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
1.500 - ---> erzeugt überflüssige "1 * ..."
1.501 + ---> erzeugt berflssige "1 * ..."
1.502
1.503 val t = str2term "-1 / (3 + y)";
1.504 (*~~ *)
1.505 @@ -1812,13 +1886,20 @@
1.506 term2str t;
1.507 "-1 / (3 + 1 * y)";
1.508 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1.509 -(* -1 im Zähler der Angabe verursacht das Problem !*)
1.510 +(* -1 im Z???ler der Angabe verursacht das Problem !*)
1.511 *)
1.512
1.513 -"----- corrected SK060905";
1.514 +(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1.515 +(*Eigenes*)
1.516 +(* Achtung: Endlosschleife bei cancel_p:
1.517 val t = str2term "(a^^^2 + -1)/(a+1)";
1.518 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.519 +term2str t;
1.520 +"(-1 + a^^^2) / (1 + a)";
1.521 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.522 -term2str t = "(-1 + a) / 1";
1.523 +term2str t;
1.524 +"(-1 + 1 * a) / 1"; (*OK*)
1.525 +*)
1.526
1.527 "----- NOT TERMINATING";
1.528 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";