1.1 --- a/src/Tools/isac/ProgLang/termC.sml Tue Oct 05 15:28:32 2010 +0200
1.2 +++ b/src/Tools/isac/ProgLang/termC.sml Tue Oct 05 16:46:56 2010 +0200
1.3 @@ -612,8 +612,8 @@
1.4 | calc "Rings.inverse_class.divide"(n1, n2) = n1 div n2
1.5 | calc "Atools.pow"(n1, n2) = power n1 n2
1.6 | calc op_ _ = error ("calc: operator = "^op_^" not defined");-----*)
1.7 -fun calc_equ "Orderings.ord_class.less" (n1, n2) = n1 < n2
1.8 - | calc_equ "Orderings.ord_class.less_eq" (n1, n2) = n1 <= n2
1.9 +fun calc_equ "less" (n1, n2) = n1 < n2
1.10 + | calc_equ "less_eq" (n1, n2) = n1 <= n2
1.11 | calc_equ op_ _ =
1.12 error ("calc_equ: operator = "^op_^" not defined");
1.13 fun sqrt (n:int) = if n < 0 then 0
2.1 --- a/src/Tools/isac/Test_Isac.thy Tue Oct 05 15:28:32 2010 +0200
2.2 +++ b/src/Tools/isac/Test_Isac.thy Tue Oct 05 16:46:56 2010 +0200
2.3 @@ -93,11 +93,7 @@
2.4 *}
2.5
2.6 ML {*
2.7 -str2term "1 = (2 :: real)";
2.8 -str2term "1 < (2 :: real)";
2.9 -str2term "1 <= (2 :: real)";
2.10 -str2term "a & b";
2.11 -str2term "a | b";
2.12 +strip_thy "Orderings.ord_class.less";
2.13 *}
2.14
2.15 use"../../../test/Tools/isac/Knowledge/rational.sml"
3.1 --- a/test/Tools/isac/Knowledge/rational.sml Tue Oct 05 15:28:32 2010 +0200
3.2 +++ b/test/Tools/isac/Knowledge/rational.sml Tue Oct 05 16:46:56 2010 +0200
3.3 @@ -996,27 +996,22 @@
3.4
3.5 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
3.6 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
3.7 -(*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
3.8 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
3.9 else error "rational.sml 3";
3.10 +
3.11 (*trace_rewrite:=true;*)
3.12 val t = str2term "Not (6*x is_atom)";
3.13 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
3.14 "True";
3.15 val t = str2term "1 < 2";
3.16 -
3.17 -trace_rewrite:=true; tracing "=== begin 1<2";
3.18 -rewrite_set_ thy false powers_erls t; term2str t';
3.19 -trace_rewrite:=false; tracing "=== end 1<2";
3.20 -
3.21 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.22 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
3.23 "True";
3.24 +
3.25 val t = str2term "(6*x)^^^2";
3.26 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
3.27 (num_str @{thm realpow_def_atom}) t;
3.28 -term2str t';
3.29 -trace_rewrite:=false;
3.30 +if term2str t' = "6 * x * (6 * x) ^^^ (2 + -1)" then ()
3.31 +else error "rational.sml powers_erls (6*x)^^^2";
3.32
3.33 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
3.34 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
3.35 @@ -1040,8 +1035,8 @@
3.36 if term2str t' = "(-3 + -1 * x) / 2" then () else error "rational.sml 7";
3.37
3.38 (*SRAM Schalk I, p.92 Nr. 476a*)
3.39 -val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *" ^
3.40 - " (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
3.41 +val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) * (1 + x)";
3.42 +(*. a/b : c/d translated to a/b * d/c .*)
3.43 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
3.44 (*if term2str t' = "1 / 1" then () else error "rational.sml 8";3.6.03*)
3.45 if term2str t' = "1" then () else error "rational.sml 8";
3.46 @@ -1053,23 +1048,21 @@
3.47 if term2str t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
3.48
3.49 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
3.50 -val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
3.51 +val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
3.52 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
3.53 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
3.54 - "(20*x*y/(x^^^2 - 25*y^^^2))";
3.55 + "(20*x*y/(x^^^2 - 25*y^^^2))");
3.56 (*... nicht simpl, zerlegt ...*)
3.57 -val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
3.58 - "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))";
3.59 +val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
3.60 + "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))");
3.61 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
3.62 "(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
3.63 (* ~~~~~~~~~~ poly_order notwendig!*)
3.64 -val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
3.65 - "(20*x*y/(x^^^2 - 25*y^^^2))";
3.66 +val t = str2term ("(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
3.67 + "(20*x*y/(x^^^2 - 25*y^^^2))");
3.68 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
3.69 -(*bad escape character in string:
3.70 -"(-500 * (x * y ^^^ 3) / (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2))) + 20 * (x * (y * x ^^^ 2)) / (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2)))) / (20 * (x * y))";*)
3.71 -trace_rewrite:=true;
3.72 -trace_rewrite:=false;
3.73 +if term2str t' = "1 / (x ^^^ 2 + -25 * y ^^^ 2)" then ()
3.74 +else error "rational.sml norm_Rational 1 / (x ^^^ 2 + -25 * y ^^^ 2)";
3.75
3.76 "nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
3.77 (*WN.2.6.03 from rlang.sml 56a
3.78 @@ -1097,14 +1090,14 @@
3.79 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.80 term2str t;
3.81 if (term2str t) = "19 / 21" then ()
3.82 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
3.83 +else error "rational.sml: diff.behav. in norm_Rational_mg 1";
3.84
3.85 (*SRA Schalk I, p.40 Nr. 166a *)
3.86 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
3.87 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.88 term2str t;
3.89 if (term2str t) = "45 / 2" then ()
3.90 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
3.91 +else error "rational.sml: diff.behav. in norm_Rational_mg 2";
3.92
3.93
3.94 "-------- cancellation ----------------------------------";
3.95 @@ -1118,7 +1111,7 @@
3.96 if (term2str t) =
3.97 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
3.98 then ()
3.99 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
3.100 +else error "rational.sml: diff.behav. in norm_Rational_mg 3";
3.101
3.102 (* e192b Stefan K.*)
3.103 val t = str2term
3.104 @@ -1128,7 +1121,7 @@
3.105 if (term2str t) =
3.106 "x ^^^ 2 / y ^^^ 2"
3.107 then ()
3.108 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
3.109 +else error "rational.sml: diff.behav. in norm_Rational_mg 4";
3.110
3.111 (*SRC Schalk I, p.66 Nr. 379c *)
3.112 val t = str2term
3.113 @@ -1138,7 +1131,7 @@
3.114 if (term2str t) =
3.115 "-1"
3.116 then ()
3.117 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
3.118 +else error "rational.sml: diff.behav. in norm_Rational_mg 5";
3.119
3.120 (*SRC Schalk I, p.66 Nr. 380b *)
3.121 val t = str2term
3.122 @@ -1148,7 +1141,7 @@
3.123 if (term2str t) =
3.124 "(27 + 12 * x) / (28 + 8 * x)"
3.125 then ()
3.126 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
3.127 +else error "rational.sml: diff.behav. in norm_Rational_mg 6";
3.128
3.129 (*Schalk I, p.60 Nr. 215c *)
3.130 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
3.131 @@ -1159,7 +1152,7 @@
3.132 if (term2str t) =
3.133 "(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)"
3.134 then ()
3.135 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
3.136 +else error "rational.sml: diff.behav. in norm_Rational_mg 7";
3.137 *)
3.138 (*val t = str2term
3.139 "(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)"
3.140 @@ -1176,7 +1169,7 @@
3.141 term2str t;
3.142 if (term2str t) =
3.143 "(a + b) / (4 * a + -4 * b)"
3.144 -then () else error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
3.145 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
3.146 *)
3.147
3.148 (*SRC Schalk I, p.66 Nr. 381b *)
3.149 @@ -1187,7 +1180,7 @@
3.150 if (term2str t) =
3.151 "-1 / (5 + -2 * x)"
3.152 then ()
3.153 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
3.154 +else error "rational.sml: diff.behav. in norm_Rational_mg 9";
3.155
3.156 (*SRC Schalk I, p.66 Nr. 381c *)
3.157 val t = str2term
3.158 @@ -1197,7 +1190,7 @@
3.159 if (term2str t) =
3.160 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
3.161 then ()
3.162 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
3.163 +else error "rational.sml: diff.behav. in norm_Rational_mg 10";
3.164
3.165 (*SRC Schalk I, p.66 Nr. 383a *)
3.166 val t = str2term
3.167 @@ -1207,7 +1200,7 @@
3.168 if (term2str t) =
3.169 "5 * a / (a + -1 * b)"
3.170 then ()
3.171 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
3.172 +else error "rational.sml: diff.behav. in norm_Rational_mg 11";
3.173
3.174
3.175 "-------- common denominator ----------------------------";
3.176 @@ -1221,7 +1214,7 @@
3.177 if (term2str t) =
3.178 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
3.179 then ()
3.180 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
3.181 +else error "rational.sml: diff.behav. in norm_Rational_mg 12";
3.182
3.183 (*SRA Schalk I, p.67 Nr. 407b *)
3.184 val t = str2term
3.185 @@ -1231,7 +1224,7 @@
3.186 if (term2str t) =
3.187 "4 / c"
3.188 then ()
3.189 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
3.190 +else error "rational.sml: diff.behav. in norm_Rational_mg 13";
3.191
3.192 (*SRA Schalk I, p.67 Nr. 410b *)
3.193 val t = str2term
3.194 @@ -1241,7 +1234,7 @@
3.195 if (term2str t) =
3.196 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
3.197 then ()
3.198 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
3.199 +else error "rational.sml: diff.behav. in norm_Rational_mg 14";
3.200
3.201 (*SRA Schalk I, p.67 Nr. 413b *)
3.202 val t = str2term
3.203 @@ -1251,7 +1244,7 @@
3.204 if (term2str t) =
3.205 "6 * x / (1 + -1 * x ^^^ 2)"
3.206 then ()
3.207 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
3.208 +else error "rational.sml: diff.behav. in norm_Rational_mg 15";
3.209
3.210 (*SRA Schalk I, p.68 Nr. 414a *)
3.211 val t = str2term
3.212 @@ -1261,7 +1254,7 @@
3.213 if (term2str t) =
3.214 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
3.215 then ()
3.216 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
3.217 +else error "rational.sml: diff.behav. in norm_Rational_mg 16";
3.218
3.219 (*SRA Schalk I, p.68 Nr. 423a *)
3.220 val t = str2term
3.221 @@ -1271,7 +1264,7 @@
3.222 if (term2str t) =
3.223 "1"
3.224 then ()
3.225 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
3.226 +else error "rational.sml: diff.behav. in norm_Rational_mg 17";
3.227
3.228 (*SRA Schalk I, p.68 Nr. 428b *)
3.229 val t = str2term
3.230 @@ -1281,7 +1274,7 @@
3.231 if (term2str t) =
3.232 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
3.233 then ()
3.234 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
3.235 +else error "rational.sml: diff.behav. in norm_Rational_mg 18";
3.236
3.237 (*SRA Schalk I, p.68 Nr. 430b *)
3.238 val t = str2term
3.239 @@ -1291,7 +1284,7 @@
3.240 if (term2str t) =
3.241 "a + 3 * b"
3.242 then ()
3.243 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
3.244 +else error "rational.sml: diff.behav. in norm_Rational_mg 19";
3.245
3.246
3.247 (*SRA Schalk I, p.68 Nr. 432 *)
3.248 @@ -1302,7 +1295,7 @@
3.249 if (term2str t) =
3.250 "0"
3.251 then ()
3.252 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
3.253 +else error "rational.sml: diff.behav. in norm_Rational_mg 20";
3.254
3.255 (*Eigenes*)
3.256 val t = str2term
3.257 @@ -1312,7 +1305,7 @@
3.258 if (term2str t) =
3.259 "(3 * y + b * x) / (b * y)"
3.260 then ()
3.261 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
3.262 +else error "rational.sml: diff.behav. in norm_Rational_mg 21";
3.263
3.264
3.265 "-------- multiply and cancel ---------------------------";
3.266 @@ -1326,7 +1319,7 @@
3.267 if (term2str t) =
3.268 "(5 * x + -5 * y) / (18 * x + 18 * y)"
3.269 then ()
3.270 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
3.271 +else error "rational.sml: diff.behav. in norm_Rational_mg 22";
3.272
3.273 (*SRM.test Schalk I, p.68 Nr. 436b *)
3.274 (*WN060420???MG3 crashes with method 'simplify' in
3.275 @@ -1337,28 +1330,26 @@
3.276 if (term2str t) =
3.277 "5 * a / (a + -1 * b)"
3.278 then ()
3.279 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
3.280 +else error "rational.sml: diff.behav. in norm_Rational_mg 23";
3.281
3.282 (*Schalk I, p.68 Nr. 437a *)
3.283 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
3.284 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.285 if (term2str t) = "1 / (4 * c + 3 * e)" then ()
3.286 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
3.287 +else error "rational.sml: diff.behav. in norm_Rational_mg 24";
3.288
3.289 "----- S.K. corrected non-termination 060904";
3.290 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
3.291 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
3.292 -if term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)" then ()
3.293 -else error "rational.sml.sml: S.K.8..corrected 060904-6";
3.294 +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 ()
3.295 +else error "rational.sml: S.K.8..corrected 060904-6";
3.296
3.297 "----- S.K. corrected non-termination of cancel_p_";
3.298 -val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
3.299 -"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
3.300 +val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
3.301 +"(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
3.302 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
3.303 if term2str t' = "1 / (4 * c + 3 * e)" then ()
3.304 -else error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
3.305 -
3.306 -(**)
3.307 +else error "rational.sml: diff.behav. in cancel_p S.K.8";
3.308
3.309 (*Schalk I, p.68 Nr. 437b *)
3.310 (* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
3.311 @@ -1366,6 +1357,7 @@
3.312 (* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
3.313 *)
3.314
3.315 +"================delete===";
3.316 (*a casual output from above*)
3.317 val t = str2term
3.318 "(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)";
3.319 @@ -1382,7 +1374,7 @@
3.320 if (term2str t) =
3.321 "x ^^^ 2"
3.322 then ()
3.323 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
3.324 +else error "rational.sml: diff.behav. in norm_Rational_mg 24";
3.325
3.326 (*SRM Schalk I, p.68 Nr. 439b *)
3.327 val t = str2term
3.328 @@ -1392,7 +1384,7 @@
3.329 if (term2str t) =
3.330 "(x + -4 * x ^^^ 3) / 2"
3.331 then ()
3.332 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
3.333 +else error "rational.sml: diff.behav. in norm_Rational_mg 25";
3.334
3.335 (*SRM Schalk I, p.68 Nr. 440a *)
3.336 val t = str2term
3.337 @@ -1402,20 +1394,20 @@
3.338 if (term2str t) =
3.339 "(-3 + x) / (2 + x)"
3.340 then ()
3.341 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
3.342 +else error "rational.sml: diff.behav. in norm_Rational_mg 26";
3.343
3.344 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
3.345 val t = str2term
3.346 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
3.347 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
3.348 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
3.349 -else error "rational.sml.sml: diff.behav. in norm_Rational 27";
3.350 +else error "rational.sml: diff.behav. in norm_Rational 27";
3.351
3.352 "----- SK12 works since 0707xx";
3.353 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
3.354 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
3.355 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
3.356 -else error "rational.sml.sml: diff.behav. in norm_Rational 28";
3.357 +else error "rational.sml: diff.behav. in norm_Rational 28";
3.358
3.359
3.360 "-------- common denominator and multiplication ---------";
3.361 @@ -1427,8 +1419,7 @@
3.362 term2str t;
3.363 if (term2str t) =
3.364 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
3.365 -then ()
3.366 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
3.367 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
3.368
3.369 (*SRAM Schalk I, p.69 Nr. 442b *)
3.370 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)";
3.371 @@ -1436,8 +1427,7 @@
3.372 term2str t;
3.373 if (term2str t) =
3.374 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
3.375 -then ()
3.376 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
3.377 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";
3.378
3.379 (*SRAM Schalk I, p.69 Nr. 443b *)
3.380 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
3.381 @@ -1445,8 +1435,7 @@
3.382 term2str t;
3.383 if (term2str t) =
3.384 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
3.385 -then ()
3.386 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
3.387 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";
3.388
3.389 (*SRAM Schalk I, p.69 Nr. 445b *)
3.390 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
3.391 @@ -1454,8 +1443,7 @@
3.392 term2str t;
3.393 if (term2str t) =
3.394 "a ^^^ 3 / 27"
3.395 -then ()
3.396 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
3.397 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";
3.398
3.399 (*SRAM Schalk I, p.69 Nr. 446b *)
3.400 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
3.401 @@ -1464,17 +1452,16 @@
3.402 if (term2str t) =
3.403 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
3.404 then ()
3.405 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
3.406 +else error "rational.sml: diff.behav. in norm_Rational_mg 32";
3.407
3.408 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
3.409 val t = str2term
3.410 "(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)";
3.411 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.412 term2str t;
3.413 -if (term2str t) =
3.414 -"(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
3.415 -then ()
3.416 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
3.417 +if (term2str t) = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
3.418 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";
3.419 +
3.420
3.421 (*SRAM Schalk I, p.69 Nr. 450a *)
3.422 val t = str2term
3.423 @@ -1484,7 +1471,7 @@
3.424 if (term2str t) =
3.425 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
3.426 then ()
3.427 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
3.428 +else error "rational.sml: diff.behav. in norm_Rational_mg 34";
3.429
3.430
3.431 "-------- double fractions ------------------------------";
3.432 @@ -1498,7 +1485,7 @@
3.433 if (term2str t) =
3.434 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
3.435 then ()
3.436 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
3.437 +else error "rational.sml: diff.behav. in norm_Rational_mg 35";
3.438
3.439 (*SRD Schalk I, p.69 Nr. 455a *)
3.440 val t = str2term
3.441 @@ -1507,20 +1494,20 @@
3.442 term2str t;
3.443 if (term2str t) =
3.444 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
3.445 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
3.446 +else error "rational.sml: diff.behav. in norm_Rational_mg 36";
3.447
3.448
3.449 "----- Schalk I, p.69 Nr. 455b";
3.450 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
3.451 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.452 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
3.453 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
3.454 +else error "rational.sml: diff.behav. in norm_Rational_mg 37";
3.455
3.456 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
3.457 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
3.458 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
3.459 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
3.460 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
3.461 +else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
3.462
3.463 "----- ?: worked before 0707xx";
3.464 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
3.465 @@ -1534,7 +1521,7 @@
3.466 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.467 term2str t;
3.468 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
3.469 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
3.470 +else error "rational.sml: diff.behav. in norm_Rational_mg 38";
3.471
3.472 (*SRD Schalk I, p.69 Nr. 457b *)
3.473 val t = str2term
3.474 @@ -1544,20 +1531,20 @@
3.475 if (term2str t) =
3.476 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
3.477 then ()
3.478 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
3.479 +else error "rational.sml: diff.behav. in norm_Rational_mg 39";
3.480
3.481 "----- Schalk I, p.69 Nr. 458b works since 0707";
3.482 val t = str2term
3.483 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
3.484 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
3.485 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
3.486 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
3.487 +else error "rational.sml: diff.behav. in norm_Rational_mg 39b";
3.488
3.489 (*SRD Schalk I, p.69 Nr. 459b *)
3.490 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
3.491 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
3.492 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
3.493 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
3.494 +else error "rational.sml: diff.behav. in norm_Rational_mg 41";
3.495
3.496
3.497 (*Schalk I, p.69 Nr. 460b nonterm.SK
3.498 @@ -1566,7 +1553,7 @@
3.499 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.500 if term2str t =
3.501 then ()
3.502 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
3.503 +else error "rational.sml: diff.behav. in norm_Rational_mg 42";
3.504
3.505 val t = str2term
3.506 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
3.507 @@ -1578,14 +1565,14 @@
3.508 ... non terminating.*)
3.509
3.510 (*SRD Schalk I, p.70 Nr. 472a *)
3.511 -val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/" ^
3.512 - "((4*x - 8*y)/(x + y))";
3.513 +val t = str2term ("((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/" ^
3.514 + "((4*x - 8*y)/(x + y))");
3.515 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.516 term2str t;
3.517 if (term2str t) =
3.518 "x + y"
3.519 then ()
3.520 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
3.521 +else error "rational.sml: diff.behav. in norm_Rational_mg 43";
3.522
3.523
3.524 (*----------------------------------------------------------------------*)
3.525 @@ -1600,7 +1587,7 @@
3.526 if (term2str t) =
3.527 "1 / 2"
3.528 then ()
3.529 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
3.530 +else error "rational.sml: diff.behav. in norm_Rational_mg 44";
3.531
3.532 (*SRD Schalk I, p.69 Nr. 464b *)
3.533 val t = str2term
3.534 @@ -1610,7 +1597,7 @@
3.535 if (term2str t) =
3.536 "(3 + -1 * a) / (1 + -1 * a)"
3.537 then ()
3.538 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
3.539 +else error "rational.sml: diff.behav. in norm_Rational_mg 45";
3.540
3.541 (*SRD Schalk I, p.69 Nr. 465b *)
3.542 val t = str2term
3.543 @@ -1620,7 +1607,7 @@
3.544 if (term2str t) =
3.545 "(4 * x + 6 * y + -9 * z) / (4 * x)"
3.546 then ()
3.547 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
3.548 +else error "rational.sml: diff.behav. in norm_Rational_mg 46";
3.549
3.550 (*SRD Schalk I, p.69 Nr. 466b *)
3.551 val t = str2term
3.552 @@ -1630,7 +1617,7 @@
3.553 if (term2str t) =
3.554 "(25 + -10 * x + x ^^^ 2) / 18"
3.555 then ()
3.556 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
3.557 +else error "rational.sml: diff.behav. in norm_Rational_mg 47";
3.558
3.559 (*SRD Schalk I, p.70 Nr. 469 *)
3.560 val t = str2term
3.561 @@ -1640,7 +1627,7 @@
3.562 if (term2str t) =
3.563 "3 * b ^^^ 3 / (2 * a + -2 * b)"
3.564 then ()
3.565 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
3.566 +else error "rational.sml: diff.behav. in norm_Rational_mg 48";
3.567
3.568 (*----------------------------------------------------------------------*)
3.569 (*---------------------- Mehrfache Dppelbrueche ------------------------*)
3.570 @@ -1652,7 +1639,7 @@
3.571 "((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)";
3.572 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
3.573 if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
3.574 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
3.575 +else error "rational.sml: diff.behav. in norm_Rational_mg 49";
3.576
3.577 "----- Schalk I, p.70 Nr. 477a";
3.578 (* MG Achtung: terme explodieren; Bsp zu komplex;
3.579 @@ -1669,13 +1656,13 @@
3.580
3.581
3.582 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
3.583 -val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
3.584 - "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
3.585 +val t = str2term ("(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
3.586 + "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))");
3.587 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
3.588 if term2str t' =
3.589 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
3.590 then ()
3.591 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
3.592 +else error "rational.sml: diff.behav. in norm_Rational_mg 51";
3.593
3.594 (* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
3.595 if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) * (a + -1 * b))" then ()
3.596 @@ -1693,7 +1680,7 @@
3.597 if (term2str t) =
3.598
3.599 then ()
3.600 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
3.601 +else error "rational.sml: diff.behav. in norm_Rational_mg 52";
3.602
3.603 (*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
3.604 val t = str2term
3.605 @@ -1836,7 +1823,8 @@
3.606 if (term2str t) =
3.607 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
3.608 then ()
3.609 -else error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
3.610 +else error "rational.sml: diff.behav. in norm_Rational_mg 53";
3.611 +
3.612
3.613 "-------- me Schalk I No.186 ----------------------------";
3.614 "-------- me Schalk I No.186 ----------------------------";
3.615 @@ -1847,6 +1835,7 @@
3.616 ("Rational",["rational","simplification"],
3.617 ["simplification","of_rationals"]);
3.618 val p = e_pos'; val c = [];
3.619 +(*========== inhibit exn =======================================================
3.620 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
3.621 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.622 val (p,_,f,nxt,_,pt) = me nxt p c pt;
3.623 @@ -1931,7 +1920,7 @@
3.624 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
3.625
3.626 "----- with make_deriv";
3.627 -val SOME (tt, _) = factout_p_ Isac.thy t; term2str tt =
3.628 +val SOME (tt, _) = factout_p_ thy t; term2str tt =
3.629 "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
3.630 (*
3.631 "--- with ruleset as before 060829";
3.632 @@ -1996,7 +1985,7 @@
3.633
3.634 "-------- SK 060904 ----------------------------------------------";
3.635 "----- order on polynomials -- input + output";
3.636 -val thy = Isac.thy;
3.637 +val thy = theory "Isac";
3.638 val t = str2term "(a + -1 * b) / (-1 * a + b)";
3.639 val SOME (t', _) = factout_p_ thy t; term2str t';
3.640 val SOME (t', _) = cancel_p_ thy t; term2str t';
3.641 @@ -2042,7 +2031,6 @@
3.642 "-------- how to stepwise construct Scripts -------------";
3.643 "-------- how to stepwise construct Scripts -------------";
3.644 val thy = (theory "Rational");
3.645 -val -------------------------------------------------- = "00000";
3.646 (*no trailing _*)
3.647 val p1 = parse thy (
3.648 "Script SimplifyScript (t_t::real) = " ^
3.649 @@ -2071,7 +2059,6 @@
3.650 " Try (Rewrite_Set discard_parentheses False)) " ^
3.651 " t_t)");
3.652
3.653 -val --------------------------------------------------+ = "11111";
3.654 val p6 = parse thy (
3.655 "Script SimplifyScript (t_t::real) = " ^
3.656 " ((Try (Rewrite_Set discard_minus False) @@ " ^
3.657 @@ -2087,7 +2074,8 @@
3.658 " Try (Rewrite_Set discard_parentheses False)) " ^
3.659 " t_t)"
3.660 );
3.661 -val --------------------------------------------------++ = "22222";
3.662
3.663 +============ inhibit exn =====================================================*)
3.664
3.665 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
3.666 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)