1.1 --- a/src/smltest/IsacKnowledge/rational.sml Thu Aug 31 08:27:39 2006 +0200
1.2 +++ b/src/smltest/IsacKnowledge/rational.sml Thu Aug 31 10:33:44 2006 +0200
1.3 @@ -356,63 +356,59 @@
1.4 "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))";
1.5 "(4 + x) / (3 - x)";
1.6
1.7 - (*WN.16.10.02 hinzugef"ugt -----vv---*)
1.8 - val t=(term_of o the o (parse thy))
1.9 - "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
1.10 - val Some (t',_) = common_nominator_ thy t;
1.11 - val Some (t'',_) = add_fraction_ thy t;
1.12 - term2str t';
1.13 - term2str t'';
1.14 - "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\
1.15 - \1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.16 - "6 / (3 - x)";
1.17 +(*WN021016 added -----vv---*)
1.18 +val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
1.19 +val Some (t',_) = common_nominator_ thy t;
1.20 +val Some (t'',_) = add_fraction_ thy t;
1.21 +term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1\
1.22 + \ * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
1.23 +term2str t'' = "6 / (3 - x)" (*true*);
1.24
1.25 - val t=(term_of o the o (parse thy))
1.26 - "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
1.27 - val Some (t',_) = common_nominator_ thy t;
1.28 - val Some (t'',_) = add_fraction_ thy t;
1.29 - term2str t';
1.30 - term2str t'';
1.31 - "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\
1.32 - \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.33 - "6 / (3 - x)";
1.34 - (*WN.16.10.02 hinzugef"ugt -----^^---*)
1.35 - (*WN.2.6.03 added -------vv--- no rewrite -> None !*)
1.36 - val t = str2term "1 / a";
1.37 - val None = cancel_p_ thy t;
1.38 - val None = rewrite_set_ thy false cancel_p t;
1.39 - (*WN.2.6.03 added -------^^---*)
1.40 +val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
1.41 +val Some (t',_) = common_nominator_ thy t;
1.42 +val Some (t'',_) = add_fraction_ thy t;
1.43 +term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n\
1.44 + \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
1.45 +term2str t'' = "6 / (3 - x)" (*true*);
1.46 +(*WN021016 added -----^^---*)
1.47 +(*WN030602 added -----vv--- no rewrite -> None !*)
1.48 +val t = str2term "1 / a";
1.49 +val None = cancel_p_ thy t;
1.50 +val None = rewrite_set_ thy false cancel_p t;
1.51 +(*WN.2.6.03 added -------^^---*)
1.52
1.53 - val t=(term_of o the o (parse thy))
1.54 - "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
1.55 - val Some (t',_) = factout_ thy t;
1.56 - val Some (t'',_) = cancel_ thy t;
1.57 - term2str t';
1.58 - term2str t'';
1.59 - "(y + x) * (y - x) / ((y - x) * (y - x))";
1.60 - "(y + x) / (y - x)";
1.61 +val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
1.62 +val Some (t',_) = factout_ thy t;
1.63 +val Some (t'',_) = cancel_ thy t;
1.64 +term2str t'= "(1 * y + x) * (1 * y - x) / ((1 * y - x) * (1 * y - x))"(*true*);
1.65 +(*sometime before 060831???SK..*)"(y + x) * (y - x) / ((y - x) * (y - x))";
1.66 +term2str t'' = "(1 * y + x) / (1 * y - x)" (*true*);
1.67 +(*sometime before 060831???SK1..*)"(y + x) / (y - x)";
1.68
1.69 - val t=(term_of o the o (parse thy))
1.70 - "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
1.71 - val Some (t',_) = common_nominator_ thy t;
1.72 - val Some (t'',_) = add_fraction_ thy t;
1.73 - term2str t';
1.74 - term2str t'';
1.75 - "((-1) * x ^^^ 2 + y ^^^ 2) / (((-1) * x + y) * ((-1) * x + y)) +\
1.76 - \1 * ((-1) * x + y) / (((-1) * x + y) * ((-1) * x + y))";
1.77 - "((-1) - x - y) / (x - y)";
1.78 - (*WN.16.10.02 ^^^^^^^ Reihenfolge aus Angabe umgekehrt ?!*)
1.79 +val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
1.80 +val Some (t',_) = common_nominator_ thy t;
1.81 +val Some (t'',_) = add_fraction_ thy t;
1.82 +term2str t' =
1.83 +"(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1\
1.84 +\ * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*);
1.85 +term2str t'' = "(-1 - x - y) / (1 * x - y)" (*true*);
1.86 +(*sometime before 060831???SK2..*)
1.87 +"((-1) * x ^^^ 2 + y ^^^ 2) / (((-1) * x + y) * ((-1) * x + y)) +\
1.88 +\1 * ((-1) * x + y) / (((-1) * x + y) * ((-1) * x + y))";
1.89 +(*sometime before 060831???SK2..*)"((-1) - x - y) / (x - y)";
1.90
1.91 - val t=(term_of o the o (parse thy))
1.92 - "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
1.93 - val Some (t',_) = common_nominator_ thy t;
1.94 - val Some (t'',_) = add_fraction_ thy t;
1.95 - term2str t';
1.96 - term2str t'';
1.97 - "((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
1.98 - \1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
1.99 - "((-1) - y - x) / (y - x)";
1.100 - (*WN.16.10.02 ^^^^^^^ lexicographische Ordnung ?!*)
1.101 +val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
1.102 +val Some (t',_) = common_nominator_ thy t;
1.103 +val Some (t'',_) = add_fraction_ thy t;
1.104 +term2str t' =
1.105 +"(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x)) +\n1\
1.106 +\ * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" (*true*);
1.107 +term2str t'' = "(-1 - y - x) / (1 * y - x)" (*true*);
1.108 +(*sometime before 060831???SK3..*)
1.109 +"((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
1.110 +\1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
1.111 +(*sometime before 060831???SK3..*)"((-1) - y - x) / (y - x)";
1.112 +(*WN.16.10.02 lexicographische Ordnung ^^^^^^^ ?!*)
1.113
1.114 val t=(term_of o the o (parse thy))
1.115 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
1.116 @@ -422,7 +418,7 @@
1.117 (*val Some (t'',_) = norm_rational_ thy t;
1.118 term2str t'';
1.119 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
1.120 - WN.16.10.02 ?!*)
1.121 + WN.16.10.02 ?! + WN060831???SK4*)
1.122
1.123 val t=(term_of o the o (parse thy))
1.124 "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
1.125 @@ -496,12 +492,13 @@
1.126 print("b)\n");
1.127 val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
1.128 val Some (t,_) = rewrite_set thy' false "cancel" e188b';
1.129 +t = "5 / 6" (*true*);
1.130 print("c)\n");
1.131 (*WN.23.10.02-------
1.132 val e188c'="( a + -1 * b ) / ( b + -1 * a )";
1.133 val e188c = the (rewrite_set thy' false "cancel" e188c');
1.134 is_expanded (parse_rat "a + -1 * b");
1.135 - false; -----------!!!*)
1.136 + false; -----------!!! WN060831???SK5*)
1.137 val Some (t,_) =
1.138 rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
1.139 if t= "(a + -1 * b) / (-1 * a + b)" then()
1.140 @@ -898,81 +895,40 @@
1.141 "-------- 'reverse-ruleset' cancel_p -----------------------------";
1.142 (*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
1.143
1.144 - (*the term for which reverse rewriting is demonstrated*)
1.145 - val t = (term_of o the o (parse thy))
1.146 - "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
1.147 - val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.148 - next_rule=nex,normal_form=nor,...},...} = cancel_p;
1.149 +(*the term for which reverse rewriting is demonstrated*)
1.150 +val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
1.151 +val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.152 + next_rule=nex,normal_form=nor,...},...} = cancel_p;
1.153
1.154 - (*normal_form produces the result in ONE step*)
1.155 - val Some (t',_) = nor t; term2str t';
1.156 +(*normal_form produces the result in ONE step*)
1.157 +val Some (t',_) = nor t;
1.158 +term2str t' = "(3 + 1 * x) / (3 + -1 * x)";
1.159
1.160 - (*initialize the interpreter state used by the 'me'*)
1.161 -val Some (t', asm) = cancel_p_ thy t; term2str t'; terms2str asm;
1.162 +(*initialize the interpreter state used by the 'me'*)
1.163 +val Some (t', asm) = cancel_p_ thy t;
1.164 +term2str t' = "(3 + 1 * x) / (3 + -1 * x)" (*true*);
1.165 +terms2str asm = "[\"3 + -1 * x ~= 0\"]" (*true*);
1.166 +val (t,_,revsets,_) = ini t;
1.167
1.168 -
1.169 -(* WN.14.3.03: rewrite__ Thm | Calc | missing: Rls_ FIXXXXME --------
1.170 - val (t,_,revsets,_) = ini t;
1.171 ----------------------------------------------------------------------*)
1.172 -
1.173 -(*
1.174 - val [rs] = revsets;
1.175 - filter_out (eq_Thms ["sym_real_add_zero_left",
1.176 - "sym_real_mult_0",
1.177 - "sym_real_mult_1"]) rs;
1.178 -
1.179 - 10.10.02: dieser Fall terminiert nicht
1.180 +(* WN.10.10.02: dieser Fall terminiert nicht
1.181 (make_polynomial enth"alt zu viele rules)
1.182 WN060823 'init_state' requires rewriting on specified location in the term
1.183 print_depth 99; Rfuns; print_depth 3;
1.184 +WN060831 cycling "sym_order_mult_rls_" "sym_real_mult_assoc"
1.185 + as was with make_polynomial before ?!?*)
1.186
1.187 +val Some r = nex revsets t;
1.188 +eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",
1.189 + mk_thm Rational.thy "9 = 3 ^^^ 2"));
1.190 +(*WN060831 *** id_of_thm
1.191 + Exception- ERROR raised ...
1.192 +val (r,(t,asm))::_ = loc revsets t r;
1.193 +term2str t;
1.194
1.195 val Some r = nex revsets t;
1.196 val (r,(t,asm))::_ = loc revsets t r;
1.197 term2str t;
1.198 -
1.199 - val Some r = nex revsets t;
1.200 - val (r,(t,asm))::_ = loc revsets t r;
1.201 - term2str t;
1.202 -
1.203 - ------ revset ----------------------------------------------------
1.204 -/// [Thm ("sym_real_add_zero_left","?z = 0 + ?z"),
1.205 -/// Thm ("sym_real_mult_0","0 = 0 * ?z"),
1.206 -! Thm ("sym_#mult_2_(-3)","(-6) * x = 2 * ((-3) * x)"),
1.207 -! Thm ("sym_#add_(-3)_3","0 = (-3) + 3"),
1.208 -
1.209 -? Thm ("sym_real_num_collect_assoc",
1.210 - "[| ?l is_const; ?m is_const |]
1.211 - ==> (?l + ?m) * ?n + ?k = ?l * ?n + (?m * ?n + ?k)"),
1.212 -OK Thm ("sym_real_mult_2_assoc","2 * ?z1.0 + ?k = ?z1.0 + (?z1.0 + ?k)"),
1.213 -OK Thm ("sym_real_add_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"),
1.214 -/// Thm ("sym_real_mult_1","?z = 1 * ?z"),
1.215 -! Thm ("sym_#power_3_2","9 = 3 ^^^ 2"),
1.216 -! Thm ("sym_#mult_-1_-1","1 * x ^^^ 2 = -1 * (-1 * x ^^^ 2)"),
1.217 -! Thm ("sym_#mult_-1_3","(-3) * x = -1 * (3 * x)"),
1.218 -OK Thm ("realpow_twoI","?r1 ^^^ 2 = ?r1 * ?r1" [.]),
1.219 -OK Thm ("sym_real_add_assoc",
1.220 - "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"),
1.221 -OK Thm
1.222 - ("sym_real_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
1.223 -OK Thm ("sym_real_mult_left_commute",
1.224 - "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"),
1.225 -OK Thm ("sym_real_mult_commute","?w * ?z = ?z * ?w"),
1.226 -? Thm ("sym_real_add_mult_distrib2",
1.227 - "?w * ?z1.0 + ?w * ?z2.0 = ?w * (?z1.0 + ?z2.0)"),
1.228 -? Thm ("sym_real_add_mult_distrib",
1.229 - "?z1.0 * ?w + ?z2.0 * ?w = (?z1.0 + ?z2.0) * ?w"),
1.230 -OK Thm ("real_mult_div_cancel2","?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n")]
1.231 - -------- revset ----------------------------------------------------
1.232 -
1.233 - val t = (term_of o the o (parse thy)) "(-6) * x";
1.234 - val t = (term_of o the o (parse thy))
1.235 - "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
1.236 - val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)")
1.237 - handle e => print_exn e;
1.238 - val Some (t',_) = rewrite_ thy e_rew_ord e_rls false thm t;
1.239 - term2str t';
1.240 -----------------------------------------------------------------------*)
1.241 +*)
1.242
1.243 print "\n\n\n****************** all tests successfull *************************\n";
1.244
1.245 @@ -1039,11 +995,9 @@
1.246
1.247 (*............................vvv---TODO: sollte gehen mit poly_order *)
1.248 (*Schalk I, p.92 Nr. 472a*)
1.249 -val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1.250 - \((4*x - 8*y)/(x + y))";
1.251 +val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
1.252 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.253 -"(-32 * y ^^^ 3 +\n (8 * x ^^^ 3 + (-32 * (x * y ^^^ 2) + 8 * (y * x ^^^ 2)))) /\n(-32 * y ^^^ 2 + 8 * x ^^^ 2)";
1.254 -(*###########################statt "x + y" poly_order notwendig!*)
1.255 +if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a";
1.256
1.257 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1.258 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.259 @@ -1069,6 +1023,7 @@
1.260 (*WN.2.6.03 from rlang.sml 56a =======================================vvv---*)
1.261 (*... takes uncredible much time:*)
1.262 (*
1.263 +WN060831???SK6
1.264 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.265 val None = rewrite_set_ thy false common_nominator_p t;
1.266 writeln
1.267 @@ -1077,6 +1032,7 @@
1.268 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1.269 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1.270 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n";
1.271 +WN060831???SK7
1.272 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.273 val None = add_fraction_p_ thy t;
1.274 *)
1.275 @@ -1176,8 +1132,8 @@
1.276
1.277 (*Schalk I, p.60 Nr. 215c *)
1.278 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter kürzen!!!*)
1.279 -(*val t = str2term
1.280 -"(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1.281 +(* WN060831???MG1
1.282 +val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1.283 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.284 term2str t;
1.285 if (term2str t) =
1.286 @@ -1194,14 +1150,13 @@
1.287
1.288 (*Schalk I, p.66 Nr. 381a *)
1.289 (* ACHTUNG: rechnet ca. 2 Minuten !!! *)
1.290 -(*val t = str2term
1.291 -"18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
1.292 +(* WN060831???MG2
1.293 +val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
1.294 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.295 term2str t;
1.296 if (term2str t) =
1.297 "(a + b) / (4 * a + -4 * b)"
1.298 -then ()
1.299 -else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1.300 +then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1.301 *)
1.302
1.303 (*SRC Schalk I, p.66 Nr. 381b *)
1.304 @@ -1355,7 +1310,7 @@
1.305 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1.306
1.307 (*SRM.test Schalk I, p.68 Nr. 436b *)
1.308 -(*WN060420 crashes with method 'simplify' in
1.309 +(*WN060420???MG3 crashes with method 'simplify' in
1.310 IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
1.311 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1.312 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.313 @@ -1366,38 +1321,36 @@
1.314 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1.315
1.316 (*Schalk I, p.68 Nr. 437a *)
1.317 -(* SK loops: rechnet ewig; cancel_p hängt sich auf...
1.318 -val t = str2term
1.319 -"(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.320 -val Some (t,_) =
1.321 -rewrite_set_ thy false norm_Rational(*_mg*) t;
1.322 +(* SK loops: rechnet ewig; cancel_p hängt sich auf... WN060420???MG4
1.323 +val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.324 +val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.325 term2str t;
1.326 +*)
1.327
1.328 -SK loops
1.329 -val t = str2term
1.330 -"(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1.331 -val Some (t,_) =
1.332 -rewrite_set_ thy false make_polynomial t;
1.333 -term2str t;
1.334 -"(9 * a ^^^ 2 + -16 * b ^^^ 2) /
1.335 -(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)";
1.336 -val Some (t,_) =
1.337 -rewrite_set_ thy false cancel_p t;
1.338 -term2str t;
1.339 +(*SK loops .. WN060420???MG5 not canceled to "1 / (4*c + 3*e)"*)
1.340 +val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1.341 +val Some (t',_) = rewrite_set_ thy false make_polynomial t;
1.342 +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.343 +(*..WN060831 _with_ parentheses ...*)
1.344 +val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.345 +\(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.346 +(* WN060831???SK8
1.347 +val Some (t',_) = rewrite_set_ thy false cancel_p t'';
1.348 +term2str t';
1.349 *)
1.350
1.351 (*Schalk I, p.68 Nr. 437b *)
1.352 (* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter kürzen!!!
1.353 val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.354 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.355 -term2str t;
1.356 +term2str t; WN060831???SK9
1.357 "(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.358
1.359 *)
1.360
1.361 (*
1.362 val t = str2term
1.363 -"(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.364 +"(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.365 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.366 term2str t;
1.367 uncaught exception nonexhaustive binding failure
1.368 @@ -1435,7 +1388,7 @@
1.369 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.370
1.371 (*Schalk I, p.68 Nr. 440b *)
1.372 -(* Achtung: rechnet ewig; cancel_p hängt sich auf...
1.373 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... WN060831???SK11
1.374 val t = str2term
1.375 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1.376 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.377 @@ -1445,15 +1398,14 @@
1.378 then ()
1.379 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27";
1.380
1.381 -val t = str2term
1.382 -"(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1.383 -val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.384 -term2str t;
1.385 +val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1.386 +val Some (t',_) = rewrite_set_ thy false make_polynomial t;
1.387 +term2str t';
1.388 "(-9 * a ^^^ 3 * b + -9 * a ^^^ 2 * b ^^^ 2 + a ^^^ 5 * b + a ^^^ 4 * b ^^^ 2)/
1.389 (3 * a ^^^ 3 * b + -3 * a * b ^^^ 3 + a ^^^ 4 * b + -1 * a ^^^ 2 * b ^^^ 3)";
1.390 -val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.391 -term2str t;
1.392 -*)
1.393 +val Some (t',_) = rewrite_set_ thy false cancel_p t;
1.394 +term2str t';
1.395 +WN060831???SK12*)
1.396
1.397 "-------- common denominator and multiplication ------------------";
1.398 "-------- common denominator and multiplication ------------------";
1.399 @@ -1555,8 +1507,7 @@
1.400
1.401 (*Schalk I, p.69 Nr. 455b *)
1.402 (* Achtung: Endlosschleife
1.403 -val t = str2term
1.404 -"(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.405 +val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.406 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.407 term2str t;
1.408 if (term2str t) =
1.409 @@ -1564,30 +1515,26 @@
1.410 then ()
1.411 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1.412
1.413 -val t = str2term
1.414 -"(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1.415 +val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1.416 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.417 term2str t;
1.418 "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /
1.419 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"
1.420 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.421 term2str t;
1.422 -(* Achtung: rechnet ewig; cancel_p hängt sich auf...*)
1.423 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ???SK*)
1.424
1.425 -val t = str2term
1.426 -"(3 + -1 * y) / (-9 + y ^^^ 2)";
1.427 +val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1.428 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.429 term2str t;
1.430 -(*ENDLOSSCHLEIFE!!!*)
1.431 +(*ENDLOSSCHLEIFE!!! ???SK*)
1.432
1.433 -val t = str2term
1.434 -"-1 / (3 + y)";
1.435 -(*~~ *)
1.436 +val t = str2term "-1 / (3 + y)";
1.437 +(* ~~ *)
1.438 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.439 -term2str t;
1.440 -"-1 / (3 + 1 * y)";
1.441 +term2str t = "-1 / (3 + 1 * y)";
1.442 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1.443 -(* -1 im Zähler der Angabe verursacht das Problem !*)
1.444 +(*MG: -1 im Zähler der Angabe verursacht das Problem ! WN060831???SK0*)
1.445 *)
1.446
1.447 (*SRD Schalk I, p.69 Nr. 456b *)
1.448 @@ -1611,7 +1558,7 @@
1.449 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.450
1.451 (*Schalk I, p.69 Nr. 458b *)
1.452 -(* Achtung: rechnet ewig; cancel_p hängt sich auf...
1.453 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ???SK
1.454 val t = str2term
1.455 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1.456 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.457 @@ -1634,7 +1581,7 @@
1.458
1.459
1.460 (*Schalk I, p.69 Nr. 460b *)
1.461 -(* Achtung: rechnet ewig; cancel_p hängt sich auf...
1.462 +(* Achtung: rechnet ewig; cancel_p hängt sich auf... ???SK
1.463 val t = str2term
1.464 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.465 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.466 @@ -1651,7 +1598,7 @@
1.467 "(-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.468 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.469 term2str t;
1.470 -*)
1.471 + ???SK*)
1.472
1.473 (*SRD Schalk I, p.70 Nr. 472a *)
1.474 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1.475 @@ -1722,7 +1669,7 @@
1.476 (*----------------------------------------------------------------------*)
1.477
1.478 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1.479 -(*WN060419 crashes with method 'simplify'*)
1.480 +(*WN060419 crashes with method 'simplify' ???SK*)
1.481 val t = str2term
1.482 "((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)";
1.483 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.484 @@ -1735,37 +1682,38 @@
1.485 (*Schalk I, p.70 Nr. 477a *)
1.486 (* Achtung: rechnet ewig; Bsp zu komplex;
1.487 Lösung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1.488 -val t = str2term
1.489 -"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)";
1.490 -val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.491 -term2str t;
1.492 -if (term2str t) =
1.493 +val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
1.494 + \(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1.495 +val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.496 +term2str t';
1.497 +if (term2str t') = ???SK ???MG
1.498
1.499 then ()
1.500 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 50";
1.501
1.502 -val t = str2term
1.503 -"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.504 +val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / \
1.505 + \((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
1.506 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.507 -term2str t;
1.508 +term2str t; ???SK ???MG
1.509 "(a ^^^ 2 * b ^^^ 4 * y + 2 * a ^^^ 2 * b ^^^ 3 * y ^^^ 2 +\n -4 * a ^^^ 2 * b ^^^ 2 * y ^^^ 3 +\n -8 * a ^^^ 2 * b * y ^^^ 4 +\n 4 * a * b ^^^ 4 * x * y +\n 8 * a * b ^^^ 3 * x * y ^^^ 2 +\n -16 * a * b ^^^ 2 * x * y ^^^ 3 +\n -32 * a * b * x * y ^^^ 4 +\n 4 * b ^^^ 4 * x ^^^ 2 * y +\n 8 * b ^^^ 3 * x ^^^ 2 * y ^^^ 2 +\n -16 * b ^^^ 2 * x ^^^ 2 * y ^^^ 3 +\n -32 * b * x ^^^ 2 * y ^^^ 4)
1.510 /\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.511 *)
1.512
1.513 (*Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec *)
1.514 -val t = str2term
1.515 -"(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.516 -val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.517 -term2str t;
1.518 +val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
1.519 + \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1.520 +val Some (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.521 +term2str t';
1.522 (* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
1.523 -if (term2str t) =
1.524 + ???SK ???MG
1.525 +if term2str t' =
1.526 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.527 then ()
1.528 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.529 -----------------------------------------------------------------------*)
1.530
1.531 (*Schalk I, p.70 Nr. 480a *)
1.532 -(* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen:
1.533 +(* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen: WN060831???SK00
1.534 val t = str2term
1.535 "(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.536 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.537 @@ -1775,7 +1723,7 @@
1.538 then ()
1.539 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1.540
1.541 -(* Berechne Zwischenergebnisse:*)
1.542 +(*MG Berechne Zwischenergebnisse: WN060831???SK00*)
1.543 val t = str2term
1.544 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
1.545 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.546 @@ -1872,16 +1820,14 @@
1.547 "(1 + 1 * x^^^3 + 1 * x^^^5 + 1 * (y * x^^^2)) / (1 * x + 1 * y)";
1.548
1.549 (*--------------------------------------------------------------------*)
1.550 -(* cancel_p liefert nicht immer Polynomnormalform (2):
1.551 +(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
1.552 ---> Sortierung FALSCH !! *)
1.553 -val t = str2term
1.554 - "b^^^3 * a^^^5/a ";
1.555 +val t = str2term "b^^^3 * a^^^5/a ";
1.556 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.557 term2str t;
1.558 "1 * (a^^^4 * b^^^3) / 1"; (*OK*)
1.559
1.560 -val t = str2term
1.561 - "b^^^3 * a^^^5/b ";
1.562 +val t = str2term "b^^^3 * a^^^5/b ";
1.563 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.564 term2str t;
1.565 "1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
1.566 @@ -1896,11 +1842,10 @@
1.567 (* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
1.568
1.569 (*--------------------------------------------------------------------*)
1.570 -(* cancel_p liefert nicht immer Polynomnormalform (2):
1.571 +(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
1.572 ---> erzeugt überflüssige "1 * ..."
1.573
1.574 -val t = str2term
1.575 -"-1 / (3 + y)";
1.576 +val t = str2term "-1 / (3 + y)";
1.577 (*~~ *)
1.578 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.579 term2str t;
1.580 @@ -1912,8 +1857,7 @@
1.581 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1.582 (*Eigenes*)
1.583 (* Achtung: Endlosschleife bei cancel_p:
1.584 -val t = str2term
1.585 -"(a^^^2 - 1)/(a+1)";
1.586 +val t = str2term "(a^^^2 - 1)/(a+1)";
1.587 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.588 term2str t;
1.589 "(-1 + a^^^2) / (1 + a)";
1.590 @@ -1921,8 +1865,7 @@
1.591 term2str t;
1.592 "(-1 + 1 * a) / 1"; (*OK*)
1.593
1.594 -val t = str2term
1.595 -"(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1.596 +val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1.597 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1.598 term2str t;
1.599 "(-1 + -1 * b + a^^^2 + a^^^2 * b) /
1.600 @@ -1942,8 +1885,8 @@
1.601
1.602 (* cancel_p liefert nicht immer Polynomnormalform (2):
1.603 ---> Minus (binärer Operator) wird erzeugt !!! *)
1.604 -(*val t = str2term
1.605 -"-1 / (5 + -2 * x)";
1.606 +(*
1.607 +val t = str2term "-1 / (5 + -2 * x)";
1.608 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1.609 term2str t;
1.610 "-1 / (5 - 2 * x)";*)
1.611 @@ -2121,10 +2064,11 @@
1.612
1.613 "----- see Rational.ML, local cancel_p, fun init_state";
1.614 val t = str2term "a^^^2 / a";
1.615 -val Some (t',_) = factout_p_ thy t; term2str t';
1.616 -(*val it = "1 * a * (1 * a) / (1 * (1 * a))" ... can be canceled with
1.617 - real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
1.618 +val Some (t',_) = factout_p_ thy t;
1.619 +term2str t' = "1 * a * (1 * a) / (1 * (1 * a))" (*true*);
1.620 +(*... can be canceled with
1.621 +real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
1.622 (*
1.623 -val rtas = reverse_deriv thy eval_rls rules ro None t';
1.624 +val rtas = reverse_deriv thy Atools_erls rules ro None t';
1.625 writeln(rtas2str rtas);
1.626 *)