287 powerproduct2term(is, vs); |
287 powerproduct2term(is, vs); |
288 term2str ttt; |
288 term2str ttt; |
289 -------versuche 13.3.03-----*) |
289 -------versuche 13.3.03-----*) |
290 |
290 |
291 val t = str2term "1 - x^^^2 - 5 * x^^^5"; |
291 val t = str2term "1 - x^^^2 - 5 * x^^^5"; |
292 val Some t' = expanded2polynomial t; term2str t'; |
292 val SOME t' = expanded2polynomial t; term2str t'; |
293 "1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5"; |
293 "1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5"; |
294 val t = str2term "1 - x"; |
294 val t = str2term "1 - x"; |
295 val Some t' = expanded2polynomial t; term2str t'; |
295 val SOME t' = expanded2polynomial t; term2str t'; |
296 "1 + - 1 * x"; |
296 "1 + - 1 * x"; |
297 val t = str2term "1 + (-1) * x"; |
297 val t = str2term "1 + (-1) * x"; |
298 val Some t' = expanded2polynomial t; term2str t'; |
298 val SOME t' = expanded2polynomial t; term2str t'; |
299 "1 + - 1 * x"; |
299 "1 + - 1 * x"; |
300 val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5"; |
300 val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5"; |
301 val Some t' = polynomial2expanded t; term2str t'; |
301 val SOME t' = polynomial2expanded t; term2str t'; |
302 "1 - x ^^^ 2 - 5 * x ^^^ 5"; |
302 "1 - x ^^^ 2 - 5 * x ^^^ 5"; |
303 |
303 |
304 |
304 |
305 " external calculating functions test "; |
305 " external calculating functions test "; |
306 " external calculating functions test "; |
306 " external calculating functions test "; |
307 " external calculating functions test "; |
307 " external calculating functions test "; |
308 |
308 |
309 val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; |
309 val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; |
310 val Some (t1',asm)= factout_p_ thy t1; |
310 val SOME (t1',asm)= factout_p_ thy t1; |
311 term2str t1'; terms2str asm; |
311 term2str t1'; terms2str asm; |
312 "(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))"; |
312 "(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))"; |
313 "[]"; |
313 "[]"; |
314 val Some (t1',asm)= cancel_p_ thy t1; |
314 val SOME (t1',asm)= cancel_p_ thy t1; |
315 term2str t1'; terms2str asm; |
315 term2str t1'; terms2str asm; |
316 "(3 + 3 * x) / 2"; |
316 "(3 + 3 * x) / 2"; |
317 "[\"1 + 1 * x ~= 0\"]"; |
317 "[\"1 + 1 * x ~= 0\"]"; |
318 |
318 |
319 val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; |
319 val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; |
320 val Some (t',asm)= cancel_ thy t; |
320 val SOME (t',asm)= cancel_ thy t; |
321 term2str t'; terms2str asm; |
321 term2str t'; terms2str asm; |
322 "(3 - 3 * x) / 2"; |
322 "(3 - 3 * x) / 2"; |
323 "[\"-1 + x ~= 0\"]"; |
323 "[\"-1 + x ~= 0\"]"; |
324 val Some (t',asm)= factout_ thy t; |
324 val SOME (t',asm)= factout_ thy t; |
325 term2str t'; terms2str asm; |
325 term2str t'; terms2str asm; |
326 "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))"; |
326 "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))"; |
327 "[]"; |
327 "[]"; |
328 |
328 |
329 val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; |
329 val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; |
330 val Some (t',asm) = add_fraction_p_ thy t; |
330 val SOME (t',asm) = add_fraction_p_ thy t; |
331 term2str t'; terms2str asm; |
331 term2str t'; terms2str asm; |
332 "(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)"; |
332 "(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)"; |
333 "[]"; |
333 "[]"; |
334 val Some (t',asm) = common_nominator_p_ thy t; |
334 val SOME (t',asm) = common_nominator_p_ thy t; |
335 term2str t'; terms2str asm; |
335 term2str t'; terms2str asm; |
336 "(-1 + 1 * x) * (-1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x)) +\n(1 + 1 * x) * (1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x))"; |
336 "(-1 + 1 * x) * (-1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x)) +\n(1 + 1 * x) * (1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x))"; |
337 "[]"; |
337 "[]"; |
338 |
338 |
339 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; |
339 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; |
340 val Some (t',asm) = add_fraction_ thy t; |
340 val SOME (t',asm) = add_fraction_ thy t; |
341 term2str t'; terms2str asm; |
341 term2str t'; terms2str asm; |
342 "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)"; |
342 "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)"; |
343 "[]"; |
343 "[]"; |
344 val Some (t',asm) = common_nominator_ thy t; |
344 val SOME (t',asm) = common_nominator_ thy t; |
345 term2str t'; terms2str asm; |
345 term2str t'; terms2str asm; |
346 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"; |
346 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"; |
347 "[]"; |
347 "[]"; |
348 |
348 |
349 val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))"; |
349 val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))"; |
350 val Some (t',asm) = common_nominator_p_ thy t; |
350 val SOME (t',asm) = common_nominator_p_ thy t; |
351 term2str t'; terms2str asm; |
351 term2str t'; terms2str asm; |
352 "1 * (1 + -2 * x + 1 * x ^^^ 2) /\n((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n(1 * (-1 + 1 * x ^^^ 2) /\n ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n (1 * (-2 + 2 * x) / ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n 1 * (#"; |
352 "1 * (1 + -2 * x + 1 * x ^^^ 2) /\n((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n(1 * (-1 + 1 * x ^^^ 2) /\n ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n (1 * (-2 + 2 * x) / ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n 1 * (#"; |
353 "[]"; |
353 "[]"; |
354 val Some (t',asm) = add_fraction_p_ thy t; |
354 val SOME (t',asm) = add_fraction_p_ thy t; |
355 term2str t'; terms2str asm; |
355 term2str t'; terms2str asm; |
356 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)"; |
356 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)"; |
357 "[\"1 + 1 * x ~= 0\"]"; |
357 "[\"1 + 1 * x ~= 0\"]"; |
358 val Some(t',asm) = norm_rational_ thy t; |
358 val SOME(t',asm) = norm_rational_ thy t; |
359 term2str t'; terms2str asm; |
359 term2str t'; terms2str asm; |
360 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)"; |
360 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)"; |
361 "[\"1 + 1 * x ~= 0\"]"; |
361 "[\"1 + 1 * x ~= 0\"]"; |
362 |
362 |
363 val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))"; |
363 val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))"; |
364 val Some (t3',_) = common_nominator_ thy t3; |
364 val SOME (t3',_) = common_nominator_ thy t3; |
365 val Some (t3'',_) = add_fraction_ thy t3; |
365 val SOME (t3'',_) = add_fraction_ thy t3; |
366 (term2str t3'); |
366 (term2str t3'); |
367 (term2str t3''); |
367 (term2str t3''); |
368 |
368 |
369 val Some(t4,t5) = norm_expanded_rat_ thy t3; |
369 val SOME(t4,t5) = norm_expanded_rat_ thy t3; |
370 term2str t4; |
370 term2str t4; |
371 term2str (hd(t5)); |
371 term2str (hd(t5)); |
372 |
372 |
373 |
373 |
374 |
374 |
375 val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)"; |
375 val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)"; |
376 val Some (t',_) = factout_ thy t; |
376 val SOME (t',_) = factout_ thy t; |
377 val Some (t'',_) = cancel_ thy t; |
377 val SOME (t'',_) = cancel_ thy t; |
378 term2str t'; |
378 term2str t'; |
379 term2str t''; |
379 term2str t''; |
380 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))"; |
380 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))"; |
381 "(3 + x) / (3 - x)"; |
381 "(3 + x) / (3 - x)"; |
382 |
382 |
383 val t=(term_of o the o (parse thy)) |
383 val t=(term_of o the o (parse thy)) |
384 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)"; |
384 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)"; |
385 val Some (t',_) = common_nominator_ thy t; |
385 val SOME (t',_) = common_nominator_ thy t; |
386 val Some (t'',_) = add_fraction_ thy t; |
386 val SOME (t'',_) = add_fraction_ thy t; |
387 term2str t'; |
387 term2str t'; |
388 term2str t''; |
388 term2str t''; |
389 "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))"; |
389 "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))"; |
390 "(4 + x) / (3 - x)"; |
390 "(4 + x) / (3 - x)"; |
391 |
391 |
392 (*WN021016 added -----vv---*) |
392 (*WN021016 added -----vv---*) |
393 val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1"; |
393 val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1"; |
394 val Some (t',_) = common_nominator_ thy t; |
394 val SOME (t',_) = common_nominator_ thy t; |
395 val Some (t'',_) = add_fraction_ thy t; |
395 val SOME (t'',_) = add_fraction_ thy t; |
396 term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1\ |
396 term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1\ |
397 \ * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); |
397 \ * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); |
398 term2str t'' = "6 / (3 - x)" (*true*); |
398 term2str t'' = "6 / (3 - x)" (*true*); |
399 |
399 |
400 val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)"; |
400 val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)"; |
401 val Some (t',_) = common_nominator_ thy t; |
401 val SOME (t',_) = common_nominator_ thy t; |
402 val Some (t'',_) = add_fraction_ thy t; |
402 val SOME (t'',_) = add_fraction_ thy t; |
403 term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n\ |
403 term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n\ |
404 \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); |
404 \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); |
405 term2str t'' = "6 / (3 - x)" (*true*); |
405 term2str t'' = "6 / (3 - x)" (*true*); |
406 (*WN021016 added -----^^---*) |
406 (*WN021016 added -----^^---*) |
407 (*WN030602 added -----vv--- no rewrite -> None !*) |
407 (*WN030602 added -----vv--- no rewrite -> NONE !*) |
408 val t = str2term "1 / a"; |
408 val t = str2term "1 / a"; |
409 val None = cancel_p_ thy t; |
409 val NONE = cancel_p_ thy t; |
410 val None = rewrite_set_ thy false cancel_p t; |
410 val NONE = rewrite_set_ thy false cancel_p t; |
411 (*WN.2.6.03 added -------^^---*) |
411 (*WN.2.6.03 added -------^^---*) |
412 |
412 |
413 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)"; |
413 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)"; |
414 val Some (t',_) = factout_ thy t; |
414 val SOME (t',_) = factout_ thy t; |
415 val Some (t'',_) = cancel_ thy t; |
415 val SOME (t'',_) = cancel_ thy t; |
416 term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*); |
416 term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*); |
417 term2str t'' = "(y + x) / (y - x)"; |
417 term2str t'' = "(y + x) / (y - x)"; |
418 |
418 |
419 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)"; |
419 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)"; |
420 val Some (t',_) = common_nominator_ thy t; |
420 val SOME (t',_) = common_nominator_ thy t; |
421 val Some (t'',_) = add_fraction_ thy t; |
421 val SOME (t'',_) = add_fraction_ thy t; |
422 term2str t' = |
422 term2str t' = |
423 "(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1\ |
423 "(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1\ |
424 \ * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*); |
424 \ * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*); |
425 term2str t'' = "(-1 - x - y) / (x - y)" (*true*); |
425 term2str t'' = "(-1 - x - y) / (x - y)" (*true*); |
426 |
426 |
427 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)"; |
427 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)"; |
428 val Some (t',_) = common_nominator_ thy t; |
428 val SOME (t',_) = common_nominator_ thy t; |
429 val Some (t'',_) = add_fraction_ thy t; |
429 val SOME (t'',_) = add_fraction_ thy t; |
430 if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\ |
430 if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\ |
431 \ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then () |
431 \ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then () |
432 else raise error "rational.sml lex-ord 1"; |
432 else raise error "rational.sml lex-ord 1"; |
433 if term2str t'' = "(-1 - y - x) / (y - x)" then () |
433 if term2str t'' = "(-1 - y - x) / (y - x)" then () |
434 else raise error "rational.sml lex-ord 2"; |
434 else raise error "rational.sml lex-ord 2"; |
435 (*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*) |
435 (*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*) |
436 |
436 |
437 |
437 |
438 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)"; |
438 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)"; |
439 val Some (t',_) = norm_expanded_rat_ thy t; |
439 val SOME (t',_) = norm_expanded_rat_ thy t; |
440 if term2str t' = "(x + y) / (x - y)" then () |
440 if term2str t' = "(x + y) / (x - y)" then () |
441 else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1"; |
441 else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1"; |
442 (*val Some (t'',_) = norm_rational_ thy t; |
442 (*val SOME (t'',_) = norm_rational_ thy t; |
443 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial |
443 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial |
444 WN.16.10.02 ?! + WN060831???SK4 |
444 WN.16.10.02 ?! + WN060831???SK4 |
445 WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*) |
445 WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*) |
446 |
446 |
447 |
447 |
448 val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)"; |
448 val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)"; |
449 val Some (t',_) = norm_expanded_rat_ thy t; |
449 val SOME (t',_) = norm_expanded_rat_ thy t; |
450 if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then () |
450 if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then () |
451 else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +..."; |
451 else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +..."; |
452 (*val Some (t'',_) = norm_rational_ thy t; |
452 (*val SOME (t'',_) = norm_rational_ thy t; |
453 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?! |
453 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?! |
454 WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*) |
454 WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*) |
455 |
455 |
456 val t=(term_of o the o (parse thy)) |
456 val t=(term_of o the o (parse thy)) |
457 "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)"; |
457 "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)"; |
458 val Some (t',_) = norm_expanded_rat_ thy t; |
458 val SOME (t',_) = norm_expanded_rat_ thy t; |
459 val Some (t'',_) = norm_rational_ thy t; |
459 val SOME (t'',_) = norm_rational_ thy t; |
460 term2str t'; |
460 term2str t'; |
461 term2str t''; |
461 term2str t''; |
462 "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)"; |
462 "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)"; |
463 "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)"; |
463 "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)"; |
464 |
464 |
959 (*WN.17.3.03 =========================================================vvv---*) |
959 (*WN.17.3.03 =========================================================vvv---*) |
960 "-------- norm_Rational ------------------------------------------"; |
960 "-------- norm_Rational ------------------------------------------"; |
961 "-------- norm_Rational ------------------------------------------"; |
961 "-------- norm_Rational ------------------------------------------"; |
962 "-------- norm_Rational ------------------------------------------"; |
962 "-------- norm_Rational ------------------------------------------"; |
963 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0"; |
963 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0"; |
964 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
964 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
965 if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1"; |
965 if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1"; |
966 |
966 |
967 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0"; |
967 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0"; |
968 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
968 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
969 if term2str t' = "(237 + 65 * x) / 36 = 0" then () |
969 if term2str t' = "(237 + 65 * x) / 36 = 0" then () |
970 else raise error "rational.sml 2"; |
970 else raise error "rational.sml 2"; |
971 |
971 |
972 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29"; |
972 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29"; |
973 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
973 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
974 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*) |
974 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*) |
975 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then () |
975 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then () |
976 else raise error "rational.sml 3"; |
976 else raise error "rational.sml 3"; |
977 (*trace_rewrite:=true;*) |
977 (*trace_rewrite:=true;*) |
978 val t = str2term "Not (6*x is_atom)"; |
978 val t = str2term "Not (6*x is_atom)"; |
979 val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t'; |
979 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t'; |
980 "True"; |
980 "True"; |
981 val t = str2term "1 < 2"; |
981 val t = str2term "1 < 2"; |
982 val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t'; |
982 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t'; |
983 "True"; |
983 "True"; |
984 val t = str2term "(6*x)^^^2"; |
984 val t = str2term "(6*x)^^^2"; |
985 val Some (t',_) = rewrite_ thy dummy_ord powers_erls false |
985 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false |
986 (num_str realpow_def_atom) t; |
986 (num_str realpow_def_atom) t; |
987 term2str t'; |
987 term2str t'; |
988 trace_rewrite:=false; |
988 trace_rewrite:=false; |
989 |
989 |
990 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))"; |
990 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))"; |
991 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
991 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
992 if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4"; |
992 if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4"; |
993 |
993 |
994 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2"; |
994 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2"; |
995 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
995 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
996 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*) |
996 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*) |
997 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then () |
997 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then () |
998 else raise error "rational.sml 5"; |
998 else raise error "rational.sml 5"; |
999 |
999 |
1000 (*SRAM Schalk I, p.92 Nr. 609a*) |
1000 (*SRAM Schalk I, p.92 Nr. 609a*) |
1001 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54"; |
1001 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54"; |
1002 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1002 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1003 if term2str t' = "(-255 + 112 * x) / 135" then () |
1003 if term2str t' = "(-255 + 112 * x) / 135" then () |
1004 else raise error "rational.sml 6"; |
1004 else raise error "rational.sml 6"; |
1005 |
1005 |
1006 (*SRAM Schalk I, p.92 Nr. 610c*) |
1006 (*SRAM Schalk I, p.92 Nr. 610c*) |
1007 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2"; |
1007 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2"; |
1008 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1008 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1009 if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7"; |
1009 if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7"; |
1010 |
1010 |
1011 (*SRAM Schalk I, p.92 Nr. 476a*) |
1011 (*SRAM Schalk I, p.92 Nr. 476a*) |
1012 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\ |
1012 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\ |
1013 \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*) |
1013 \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*) |
1014 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1014 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1015 (*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*) |
1015 (*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*) |
1016 if term2str t' = "1" then () else raise error "rational.sml 8"; |
1016 if term2str t' = "1" then () else raise error "rational.sml 8"; |
1017 |
1017 |
1018 (*............................vvv---TODO: sollte gehen mit poly_order *) |
1018 (*............................vvv---TODO: sollte gehen mit poly_order *) |
1019 (*Schalk I, p.92 Nr. 472a*) |
1019 (*Schalk I, p.92 Nr. 472a*) |
1020 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))"; |
1020 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))"; |
1021 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1021 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1022 if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a"; |
1022 if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a"; |
1023 |
1023 |
1024 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*) |
1024 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*) |
1025 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\ |
1025 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\ |
1026 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\ |
1026 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\ |
1027 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\ |
1027 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\ |
1028 \(20*x*y/(x^^^2 - 25*y^^^2))"; |
1028 \(20*x*y/(x^^^2 - 25*y^^^2))"; |
1029 (*... nicht simpl, zerlegt ...*) |
1029 (*... nicht simpl, zerlegt ...*) |
1030 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\ |
1030 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\ |
1031 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))"; |
1031 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))"; |
1032 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1032 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1033 "(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))"; |
1033 "(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))"; |
1034 (* ~~~~~~~~~~ poly_order notwendig!*) |
1034 (* ~~~~~~~~~~ poly_order notwendig!*) |
1035 val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\ |
1035 val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\ |
1036 \(20*x*y/(x^^^2 - 25*y^^^2))"; |
1036 \(20*x*y/(x^^^2 - 25*y^^^2))"; |
1037 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1037 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1038 "(-500 * (x * y ^^^ 3) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2))) +\n 20 * (x * (y * x ^^^ 2)) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2)))) /\n(20 * (x * y))"; |
1038 "(-500 * (x * y ^^^ 3) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2))) +\n 20 * (x * (y * x ^^^ 2)) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2)))) /\n(20 * (x * y))"; |
1039 trace_rewrite:=true; |
1039 trace_rewrite:=true; |
1040 trace_rewrite:=false; |
1040 trace_rewrite:=false; |
1041 |
1041 |
1042 "nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_"; |
1042 "nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_"; |
1043 (*WN.2.6.03 from rlang.sml 56a |
1043 (*WN.2.6.03 from rlang.sml 56a |
1044 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)"; |
1044 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)"; |
1045 val None = rewrite_set_ thy false common_nominator_p t; |
1045 val NONE = rewrite_set_ thy false common_nominator_p t; |
1046 |
1046 |
1047 WN060831 nonterm.SK7 |
1047 WN060831 nonterm.SK7 |
1048 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)"; |
1048 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)"; |
1049 val None = add_fraction_p_ thy t; |
1049 val NONE = add_fraction_p_ thy t; |
1050 *) |
1050 *) |
1051 |
1051 |
1052 |
1052 |
1053 (* ------------------------------------------------------------------- *) |
1053 (* ------------------------------------------------------------------- *) |
1054 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*) |
1054 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*) |
1081 "-------- cancellation -------------------------------------------"; |
1081 "-------- cancellation -------------------------------------------"; |
1082 |
1082 |
1083 (* e190c Stefan K.*) |
1083 (* e190c Stefan K.*) |
1084 val t = str2term |
1084 val t = str2term |
1085 "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))"; |
1085 "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))"; |
1086 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1086 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1087 term2str t; |
1087 term2str t; |
1088 if (term2str t) = |
1088 if (term2str t) = |
1089 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)" |
1089 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)" |
1090 then () |
1090 then () |
1091 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3"; |
1091 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3"; |
1092 |
1092 |
1093 (* e192b Stefan K.*) |
1093 (* e192b Stefan K.*) |
1094 val t = str2term |
1094 val t = str2term |
1095 "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))"; |
1095 "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))"; |
1096 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1096 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1097 term2str t; |
1097 term2str t; |
1098 if (term2str t) = |
1098 if (term2str t) = |
1099 "x ^^^ 2 / y ^^^ 2" |
1099 "x ^^^ 2 / y ^^^ 2" |
1100 then () |
1100 then () |
1101 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4"; |
1101 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4"; |
1102 |
1102 |
1103 (*SRC Schalk I, p.66 Nr. 379c *) |
1103 (*SRC Schalk I, p.66 Nr. 379c *) |
1104 val t = str2term |
1104 val t = str2term |
1105 "(a - b)/(b - a)"; |
1105 "(a - b)/(b - a)"; |
1106 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1106 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1107 term2str t; |
1107 term2str t; |
1108 if (term2str t) = |
1108 if (term2str t) = |
1109 "-1" |
1109 "-1" |
1110 then () |
1110 then () |
1111 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5"; |
1111 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5"; |
1112 |
1112 |
1113 (*SRC Schalk I, p.66 Nr. 380b *) |
1113 (*SRC Schalk I, p.66 Nr. 380b *) |
1114 val t = str2term |
1114 val t = str2term |
1115 "15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))"; |
1115 "15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))"; |
1116 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1116 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1117 term2str t; |
1117 term2str t; |
1118 if (term2str t) = |
1118 if (term2str t) = |
1119 "(27 + 12 * x) / (28 + 8 * x)" |
1119 "(27 + 12 * x) / (28 + 8 * x)" |
1120 then () |
1120 then () |
1121 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6"; |
1121 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6"; |
1122 |
1122 |
1123 (*Schalk I, p.60 Nr. 215c *) |
1123 (*Schalk I, p.60 Nr. 215c *) |
1124 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*) |
1124 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*) |
1125 (* WN060831????MG1 |
1125 (* WN060831????MG1 |
1126 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)"; |
1126 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)"; |
1127 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1127 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1128 term2str t; |
1128 term2str t; |
1129 if (term2str t) = |
1129 if (term2str t) = |
1130 "(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)" |
1130 "(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)" |
1131 then () |
1131 then () |
1132 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7"; |
1132 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7"; |
1133 *) |
1133 *) |
1134 (*val t = str2term |
1134 (*val t = str2term |
1135 "(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)" |
1135 "(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)" |
1136 val Some (t,_) = rewrite_set_ thy false cancel_p t; |
1136 val SOME (t,_) = rewrite_set_ thy false cancel_p t; |
1137 term2str t;*) |
1137 term2str t;*) |
1138 (* uncaught exception nonexhaustive binding failure |
1138 (* uncaught exception nonexhaustive binding failure |
1139 raised at: stdIn:93.1-93.51 *) |
1139 raised at: stdIn:93.1-93.51 *) |
1140 |
1140 |
1141 (*Schalk I, p.66 Nr. 381a *) |
1141 (*Schalk I, p.66 Nr. 381a *) |
1142 (* ACHTUNG: rechnet ca. 2 Minuten !!! *) |
1142 (* ACHTUNG: rechnet ca. 2 Minuten !!! *) |
1143 (* WN060831???MG2 |
1143 (* WN060831???MG2 |
1144 val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)"; |
1144 val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)"; |
1145 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1145 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1146 term2str t; |
1146 term2str t; |
1147 if (term2str t) = |
1147 if (term2str t) = |
1148 "(a + b) / (4 * a + -4 * b)" |
1148 "(a + b) / (4 * a + -4 * b)" |
1149 then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8"; |
1149 then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8"; |
1150 *) |
1150 *) |
1151 |
1151 |
1152 (*SRC Schalk I, p.66 Nr. 381b *) |
1152 (*SRC Schalk I, p.66 Nr. 381b *) |
1153 val t = str2term |
1153 val t = str2term |
1154 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3"; |
1154 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3"; |
1155 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1155 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1156 term2str t; |
1156 term2str t; |
1157 if (term2str t) = |
1157 if (term2str t) = |
1158 "-1 / (5 + -2 * x)" |
1158 "-1 / (5 + -2 * x)" |
1159 then () |
1159 then () |
1160 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9"; |
1160 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9"; |
1161 |
1161 |
1162 (*SRC Schalk I, p.66 Nr. 381c *) |
1162 (*SRC Schalk I, p.66 Nr. 381c *) |
1163 val t = str2term |
1163 val t = str2term |
1164 "(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)"; |
1164 "(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)"; |
1165 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1165 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1166 term2str t; |
1166 term2str t; |
1167 if (term2str t) = |
1167 if (term2str t) = |
1168 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)" |
1168 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)" |
1169 then () |
1169 then () |
1170 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10"; |
1170 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10"; |
1171 |
1171 |
1172 (*SRC Schalk I, p.66 Nr. 383a *) |
1172 (*SRC Schalk I, p.66 Nr. 383a *) |
1173 val t = str2term |
1173 val t = str2term |
1174 "(5*a^^^2 - 5*a*b)/(a - b)^^^2"; |
1174 "(5*a^^^2 - 5*a*b)/(a - b)^^^2"; |
1175 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1175 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1176 term2str t; |
1176 term2str t; |
1177 if (term2str t) = |
1177 if (term2str t) = |
1178 "5 * a / (a + -1 * b)" |
1178 "5 * a / (a + -1 * b)" |
1179 then () |
1179 then () |
1180 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11"; |
1180 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11"; |
1184 "-------- common denominator -------------------------------------"; |
1184 "-------- common denominator -------------------------------------"; |
1185 |
1185 |
1186 (*SRA Schalk I, p.67 Nr. 403a *) |
1186 (*SRA Schalk I, p.67 Nr. 403a *) |
1187 val t = str2term |
1187 val t = str2term |
1188 "4/x - 3/y - 1"; |
1188 "4/x - 3/y - 1"; |
1189 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1189 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1190 term2str t; |
1190 term2str t; |
1191 if (term2str t) = |
1191 if (term2str t) = |
1192 "(-3 * x + 4 * y + -1 * x * y) / (x * y)" |
1192 "(-3 * x + 4 * y + -1 * x * y) / (x * y)" |
1193 then () |
1193 then () |
1194 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12"; |
1194 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12"; |
1195 |
1195 |
1196 (*SRA Schalk I, p.67 Nr. 407b *) |
1196 (*SRA Schalk I, p.67 Nr. 407b *) |
1197 val t = str2term |
1197 val t = str2term |
1198 "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)"; |
1198 "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)"; |
1199 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1199 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1200 term2str t; |
1200 term2str t; |
1201 if (term2str t) = |
1201 if (term2str t) = |
1202 "4 / c" |
1202 "4 / c" |
1203 then () |
1203 then () |
1204 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13"; |
1204 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13"; |
1205 |
1205 |
1206 (*SRA Schalk I, p.67 Nr. 410b *) |
1206 (*SRA Schalk I, p.67 Nr. 410b *) |
1207 val t = str2term |
1207 val t = str2term |
1208 "1/(x+1) + 1/(x+2) - 2/(x+3)"; |
1208 "1/(x+1) + 1/(x+2) - 2/(x+3)"; |
1209 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1209 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1210 term2str t; |
1210 term2str t; |
1211 if (term2str t) = |
1211 if (term2str t) = |
1212 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)" |
1212 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)" |
1213 then () |
1213 then () |
1214 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14"; |
1214 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14"; |
1215 |
1215 |
1216 (*SRA Schalk I, p.67 Nr. 413b *) |
1216 (*SRA Schalk I, p.67 Nr. 413b *) |
1217 val t = str2term |
1217 val t = str2term |
1218 "(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)"; |
1218 "(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)"; |
1219 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1219 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1220 term2str t; |
1220 term2str t; |
1221 if (term2str t) = |
1221 if (term2str t) = |
1222 "6 * x / (1 + -1 * x ^^^ 2)" |
1222 "6 * x / (1 + -1 * x ^^^ 2)" |
1223 then () |
1223 then () |
1224 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15"; |
1224 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15"; |
1225 |
1225 |
1226 (*SRA Schalk I, p.68 Nr. 414a *) |
1226 (*SRA Schalk I, p.68 Nr. 414a *) |
1227 val t = str2term |
1227 val t = str2term |
1228 "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))"; |
1228 "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))"; |
1229 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1229 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1230 term2str t; |
1230 term2str t; |
1231 if (term2str t) = |
1231 if (term2str t) = |
1232 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)" |
1232 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)" |
1233 then () |
1233 then () |
1234 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16"; |
1234 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16"; |
1235 |
1235 |
1236 (*SRA Schalk I, p.68 Nr. 423a *) |
1236 (*SRA Schalk I, p.68 Nr. 423a *) |
1237 val t = str2term |
1237 val t = str2term |
1238 "(2*x+3*y)/x + (4*x^^^3 - x*y^^^2 - 3*y^^^3)/(x^^^3 - 2*x^^^2*y+x*y^^^2) - (5*x+6*y)/(x - y)"; |
1238 "(2*x+3*y)/x + (4*x^^^3 - x*y^^^2 - 3*y^^^3)/(x^^^3 - 2*x^^^2*y+x*y^^^2) - (5*x+6*y)/(x - y)"; |
1239 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1239 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1240 term2str t; |
1240 term2str t; |
1241 if (term2str t) = |
1241 if (term2str t) = |
1242 "1" |
1242 "1" |
1243 then () |
1243 then () |
1244 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17"; |
1244 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17"; |
1245 |
1245 |
1246 (*SRA Schalk I, p.68 Nr. 428b *) |
1246 (*SRA Schalk I, p.68 Nr. 428b *) |
1247 val t = str2term |
1247 val t = str2term |
1248 "1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2"; |
1248 "1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2"; |
1249 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1249 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1250 term2str t; |
1250 term2str t; |
1251 if (term2str t) = |
1251 if (term2str t) = |
1252 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)" |
1252 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)" |
1253 then () |
1253 then () |
1254 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18"; |
1254 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18"; |
1255 |
1255 |
1256 (*SRA Schalk I, p.68 Nr. 430b *) |
1256 (*SRA Schalk I, p.68 Nr. 430b *) |
1257 val t = str2term |
1257 val t = str2term |
1258 "a^^^2/(a - 3*b) - 108*a*b^^^3/((a+3*b)*(a^^^2 - 9*b^^^2)) - 9*b^^^2*(a - 3*b)/(a+3*b)^^^2"; |
1258 "a^^^2/(a - 3*b) - 108*a*b^^^3/((a+3*b)*(a^^^2 - 9*b^^^2)) - 9*b^^^2*(a - 3*b)/(a+3*b)^^^2"; |
1259 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1259 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1260 term2str t; |
1260 term2str t; |
1261 if (term2str t) = |
1261 if (term2str t) = |
1262 "a + 3 * b" |
1262 "a + 3 * b" |
1263 then () |
1263 then () |
1264 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19"; |
1264 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19"; |
1265 |
1265 |
1266 |
1266 |
1267 (*SRA Schalk I, p.68 Nr. 432 *) |
1267 (*SRA Schalk I, p.68 Nr. 432 *) |
1268 val t = str2term |
1268 val t = str2term |
1269 "(a^^^2+a*b)/(a^^^2 - b^^^2) - (b^^^2 - a*b)/(b^^^2 - a^^^2) + a^^^2*(a - b)/(a^^^3 - a^^^2*b) - 2*a*(a^^^2 - b^^^2)/(a^^^3 - a*b^^^2) - 2*b^^^2/(a^^^2 - b^^^2)"; |
1269 "(a^^^2+a*b)/(a^^^2 - b^^^2) - (b^^^2 - a*b)/(b^^^2 - a^^^2) + a^^^2*(a - b)/(a^^^3 - a^^^2*b) - 2*a*(a^^^2 - b^^^2)/(a^^^3 - a*b^^^2) - 2*b^^^2/(a^^^2 - b^^^2)"; |
1270 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1270 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1271 term2str t; |
1271 term2str t; |
1272 if (term2str t) = |
1272 if (term2str t) = |
1273 "0" |
1273 "0" |
1274 then () |
1274 then () |
1275 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20"; |
1275 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20"; |
1276 |
1276 |
1277 (*Eigenes*) |
1277 (*Eigenes*) |
1278 val t = str2term |
1278 val t = str2term |
1279 "3*a/(a*b) + x/y"; |
1279 "3*a/(a*b) + x/y"; |
1280 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1280 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1281 term2str t; |
1281 term2str t; |
1282 if (term2str t) = |
1282 if (term2str t) = |
1283 "(3 * y + b * x) / (b * y)" |
1283 "(3 * y + b * x) / (b * y)" |
1284 then () |
1284 then () |
1285 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21"; |
1285 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21"; |
1290 "-------- multiply and cancel ------------------------------------"; |
1290 "-------- multiply and cancel ------------------------------------"; |
1291 |
1291 |
1292 (*SRM Schalk I, p.68 Nr. 436a *) |
1292 (*SRM Schalk I, p.68 Nr. 436a *) |
1293 val t = str2term |
1293 val t = str2term |
1294 "3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)"; |
1294 "3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)"; |
1295 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1295 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1296 term2str t; |
1296 term2str t; |
1297 if (term2str t) = |
1297 if (term2str t) = |
1298 "(5 * x + -5 * y) / (18 * x + 18 * y)" |
1298 "(5 * x + -5 * y) / (18 * x + 18 * y)" |
1299 then () |
1299 then () |
1300 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22"; |
1300 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22"; |
1301 |
1301 |
1302 (*SRM.test Schalk I, p.68 Nr. 436b *) |
1302 (*SRM.test Schalk I, p.68 Nr. 436b *) |
1303 (*WN060420???MG3 crashes with method 'simplify' in |
1303 (*WN060420???MG3 crashes with method 'simplify' in |
1304 IsacCore > Simplification > Rational Terms > Multiplication > No.2*) |
1304 IsacCore > Simplification > Rational Terms > Multiplication > No.2*) |
1305 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3"; |
1305 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3"; |
1306 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1306 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1307 term2str t; |
1307 term2str t; |
1308 if (term2str t) = |
1308 if (term2str t) = |
1309 "5 * a / (a + -1 * b)" |
1309 "5 * a / (a + -1 * b)" |
1310 then () |
1310 then () |
1311 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23"; |
1311 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23"; |
1312 |
1312 |
1313 (*Schalk I, p.68 Nr. 437a *) |
1313 (*Schalk I, p.68 Nr. 437a *) |
1314 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)"; |
1314 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)"; |
1315 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1315 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1316 if (term2str t) = "1 / (4 * c + 3 * e)" then () |
1316 if (term2str t) = "1 / (4 * c + 3 * e)" then () |
1317 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24"; |
1317 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24"; |
1318 |
1318 |
1319 "----- S.K. corrected non-termination 060904"; |
1319 "----- S.K. corrected non-termination 060904"; |
1320 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))"; |
1320 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))"; |
1321 val Some (t',_) = rewrite_set_ thy false make_polynomial t; |
1321 val SOME (t',_) = rewrite_set_ thy false make_polynomial t; |
1322 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 () |
1322 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 () |
1323 else raise error "rational.sml.sml: S.K.8..corrected 060904-6"; |
1323 else raise error "rational.sml.sml: S.K.8..corrected 060904-6"; |
1324 |
1324 |
1325 "----- S.K. corrected non-termination of cancel_p_"; |
1325 "----- S.K. corrected non-termination of cancel_p_"; |
1326 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
1326 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
1327 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
1327 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
1328 val Some (t',_) = rewrite_set_ thy false cancel_p t''; |
1328 val SOME (t',_) = rewrite_set_ thy false cancel_p t''; |
1329 if term2str t' = "1 / (4 * c + 3 * e)" then () |
1329 if term2str t' = "1 / (4 * c + 3 * e)" then () |
1330 else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8"; |
1330 else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8"; |
1331 |
1331 |
1332 (**) |
1332 (**) |
1333 |
1333 |
1334 (*Schalk I, p.68 Nr. 437b *) |
1334 (*Schalk I, p.68 Nr. 437b *) |
1335 (* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *) |
1335 (* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *) |
1336 val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))"; |
1336 val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))"; |
1337 (* val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t''; |
1337 (* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t''; |
1338 *) |
1338 *) |
1339 |
1339 |
1340 (*a casual output from above*) |
1340 (*a casual output from above*) |
1341 val t = str2term |
1341 val t = str2term |
1342 "(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)"; |
1342 "(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)"; |
1343 (* WN060831 nonterm.SK10 |
1343 (* WN060831 nonterm.SK10 |
1344 val Some (t,_) = rewrite_set_ thy false cancel_p t; |
1344 val SOME (t,_) = rewrite_set_ thy false cancel_p t; |
1345 term2str t; |
1345 term2str t; |
1346 *) |
1346 *) |
1347 |
1347 |
1348 (*SRM Schalk I, p.68 Nr. 438a *) |
1348 (*SRM Schalk I, p.68 Nr. 438a *) |
1349 val t = str2term |
1349 val t = str2term |
1350 "x*y/(x*y - y^^^2)*(x^^^2 - x*y)"; |
1350 "x*y/(x*y - y^^^2)*(x^^^2 - x*y)"; |
1351 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1351 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1352 term2str t; |
1352 term2str t; |
1353 if (term2str t) = |
1353 if (term2str t) = |
1354 "x ^^^ 2" |
1354 "x ^^^ 2" |
1355 then () |
1355 then () |
1356 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24"; |
1356 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24"; |
1357 |
1357 |
1358 (*SRM Schalk I, p.68 Nr. 439b *) |
1358 (*SRM Schalk I, p.68 Nr. 439b *) |
1359 val t = str2term |
1359 val t = str2term |
1360 "(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))"; |
1360 "(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))"; |
1361 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1361 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1362 term2str t; |
1362 term2str t; |
1363 if (term2str t) = |
1363 if (term2str t) = |
1364 "(x + -4 * x ^^^ 3) / 2" |
1364 "(x + -4 * x ^^^ 3) / 2" |
1365 then () |
1365 then () |
1366 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25"; |
1366 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25"; |
1367 |
1367 |
1368 (*SRM Schalk I, p.68 Nr. 440a *) |
1368 (*SRM Schalk I, p.68 Nr. 440a *) |
1369 val t = str2term |
1369 val t = str2term |
1370 "(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)"; |
1370 "(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)"; |
1371 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1371 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1372 term2str t; |
1372 term2str t; |
1373 if (term2str t) = |
1373 if (term2str t) = |
1374 "(-3 + x) / (2 + x)" |
1374 "(-3 + x) / (2 + x)" |
1375 then () |
1375 then () |
1376 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26"; |
1376 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26"; |
1377 |
1377 |
1378 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx"; |
1378 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx"; |
1379 val t = str2term |
1379 val t = str2term |
1380 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)"; |
1380 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)"; |
1381 val Some (t,_) = rewrite_set_ thy false norm_Rational t; |
1381 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
1382 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then () |
1382 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then () |
1383 else raise error "rational.sml.sml: diff.behav. in norm_Rational 27"; |
1383 else raise error "rational.sml.sml: diff.behav. in norm_Rational 27"; |
1384 |
1384 |
1385 "----- SK12 works since 0707xx"; |
1385 "----- SK12 works since 0707xx"; |
1386 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))"; |
1386 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))"; |
1387 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1387 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t'; |
1388 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then () |
1388 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then () |
1389 else raise error "rational.sml.sml: diff.behav. in norm_Rational 28"; |
1389 else raise error "rational.sml.sml: diff.behav. in norm_Rational 28"; |
1390 |
1390 |
1391 |
1391 |
1392 "-------- common denominator and multiplication ------------------"; |
1392 "-------- common denominator and multiplication ------------------"; |
1398 (*----------------------------------------------------------------------*) |
1398 (*----------------------------------------------------------------------*) |
1399 |
1399 |
1400 |
1400 |
1401 (*SRAM Schalk I, p.69 Nr. 441b *) |
1401 (*SRAM Schalk I, p.69 Nr. 441b *) |
1402 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))"; |
1402 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))"; |
1403 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1403 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1404 term2str t; |
1404 term2str t; |
1405 if (term2str t) = |
1405 if (term2str t) = |
1406 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)" |
1406 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)" |
1407 then () |
1407 then () |
1408 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28"; |
1408 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28"; |
1409 |
1409 |
1410 (*SRAM Schalk I, p.69 Nr. 442b *) |
1410 (*SRAM Schalk I, p.69 Nr. 442b *) |
1411 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)"; |
1411 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)"; |
1412 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1412 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1413 term2str t; |
1413 term2str t; |
1414 if (term2str t) = |
1414 if (term2str t) = |
1415 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)" |
1415 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)" |
1416 then () |
1416 then () |
1417 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29"; |
1417 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29"; |
1418 |
1418 |
1419 (*SRAM Schalk I, p.69 Nr. 443b *) |
1419 (*SRAM Schalk I, p.69 Nr. 443b *) |
1420 val t = str2term "(a/2 + b/3)*(b/3 - a/2)"; |
1420 val t = str2term "(a/2 + b/3)*(b/3 - a/2)"; |
1421 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1421 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1422 term2str t; |
1422 term2str t; |
1423 if (term2str t) = |
1423 if (term2str t) = |
1424 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36" |
1424 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36" |
1425 then () |
1425 then () |
1426 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30"; |
1426 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30"; |
1427 |
1427 |
1428 (*SRAM Schalk I, p.69 Nr. 445b *) |
1428 (*SRAM Schalk I, p.69 Nr. 445b *) |
1429 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3"; |
1429 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3"; |
1430 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1430 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1431 term2str t; |
1431 term2str t; |
1432 if (term2str t) = |
1432 if (term2str t) = |
1433 "a ^^^ 3 / 27" |
1433 "a ^^^ 3 / 27" |
1434 then () |
1434 then () |
1435 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31"; |
1435 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31"; |
1436 |
1436 |
1437 (*SRAM Schalk I, p.69 Nr. 446b *) |
1437 (*SRAM Schalk I, p.69 Nr. 446b *) |
1438 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)"; |
1438 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)"; |
1439 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1439 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1440 term2str t; |
1440 term2str t; |
1441 if (term2str t) = |
1441 if (term2str t) = |
1442 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2" |
1442 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2" |
1443 then () |
1443 then () |
1444 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32"; |
1444 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32"; |
1445 |
1445 |
1446 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*) |
1446 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*) |
1447 val t = str2term |
1447 val t = str2term |
1448 "(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)"; |
1448 "(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)"; |
1449 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1449 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1450 term2str t; |
1450 term2str t; |
1451 if (term2str t) = |
1451 if (term2str t) = |
1452 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)" |
1452 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)" |
1453 then () |
1453 then () |
1454 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33"; |
1454 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33"; |
1455 |
1455 |
1456 (*SRAM Schalk I, p.69 Nr. 450a *) |
1456 (*SRAM Schalk I, p.69 Nr. 450a *) |
1457 val t = str2term |
1457 val t = str2term |
1458 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)"; |
1458 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)"; |
1459 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1459 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1460 term2str t; |
1460 term2str t; |
1461 if (term2str t) = |
1461 if (term2str t) = |
1462 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)" |
1462 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)" |
1463 then () |
1463 then () |
1464 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34"; |
1464 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34"; |
1468 "-------- double fractions ---------------------------------------"; |
1468 "-------- double fractions ---------------------------------------"; |
1469 |
1469 |
1470 (*SRD Schalk I, p.69 Nr. 454b *) |
1470 (*SRD Schalk I, p.69 Nr. 454b *) |
1471 val t = str2term |
1471 val t = str2term |
1472 "((2 - x)/(2*a)) / (2*a/(x - 2))"; |
1472 "((2 - x)/(2*a)) / (2*a/(x - 2))"; |
1473 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1473 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1474 term2str t; |
1474 term2str t; |
1475 if (term2str t) = |
1475 if (term2str t) = |
1476 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)" |
1476 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)" |
1477 then () |
1477 then () |
1478 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35"; |
1478 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35"; |
1479 |
1479 |
1480 (*SRD Schalk I, p.69 Nr. 455a *) |
1480 (*SRD Schalk I, p.69 Nr. 455a *) |
1481 val t = str2term |
1481 val t = str2term |
1482 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))"; |
1482 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))"; |
1483 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1483 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1484 term2str t; |
1484 term2str t; |
1485 if (term2str t) = |
1485 if (term2str t) = |
1486 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then () |
1486 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then () |
1487 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36"; |
1487 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36"; |
1488 |
1488 |
1489 |
1489 |
1490 "----- Schalk I, p.69 Nr. 455b"; |
1490 "----- Schalk I, p.69 Nr. 455b"; |
1491 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))"; |
1491 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))"; |
1492 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1492 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1493 if term2str t = "(2 + -1 * x) / (3 + y)" then () |
1493 if term2str t = "(2 + -1 * x) / (3 + y)" then () |
1494 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37"; |
1494 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37"; |
1495 |
1495 |
1496 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx"; |
1496 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx"; |
1497 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))"; |
1497 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))"; |
1498 val Some (t,_) = rewrite_set_ thy false norm_Rational t; |
1498 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
1499 if term2str t = "(2 + -1 * x) / (3 + y)" then () |
1499 if term2str t = "(2 + -1 * x) / (3 + y)" then () |
1500 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b"; |
1500 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b"; |
1501 |
1501 |
1502 "----- ?: worked before 0707xx"; |
1502 "----- ?: worked before 0707xx"; |
1503 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)"; |
1503 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)"; |
1504 val Some (t,_) = rewrite_set_ thy false norm_Rational t; |
1504 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
1505 if term2str t = "-1 / (3 + y)" then () |
1505 if term2str t = "-1 / (3 + y)" then () |
1506 else raise error "rational.sml: -1 / (3 + y) norm_Rational"; |
1506 else raise error "rational.sml: -1 / (3 + y) norm_Rational"; |
1507 |
1507 |
1508 (*SRD Schalk I, p.69 Nr. 456b *) |
1508 (*SRD Schalk I, p.69 Nr. 456b *) |
1509 val t = str2term |
1509 val t = str2term |
1510 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)"; |
1510 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)"; |
1511 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1511 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1512 term2str t; |
1512 term2str t; |
1513 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then () |
1513 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then () |
1514 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38"; |
1514 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38"; |
1515 |
1515 |
1516 (*SRD Schalk I, p.69 Nr. 457b *) |
1516 (*SRD Schalk I, p.69 Nr. 457b *) |
1517 val t = str2term |
1517 val t = str2term |
1518 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))"; |
1518 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))"; |
1519 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1519 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1520 term2str t; |
1520 term2str t; |
1521 if (term2str t) = |
1521 if (term2str t) = |
1522 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2" |
1522 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2" |
1523 then () |
1523 then () |
1524 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39"; |
1524 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39"; |
1525 |
1525 |
1526 "----- Schalk I, p.69 Nr. 458b works since 0707"; |
1526 "----- Schalk I, p.69 Nr. 458b works since 0707"; |
1527 val t = str2term |
1527 val t = str2term |
1528 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))"; |
1528 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))"; |
1529 val Some (t,_) = rewrite_set_ thy false norm_Rational t; |
1529 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
1530 if term2str t = "a ^^^ 2 / b ^^^ 2" then () |
1530 if term2str t = "a ^^^ 2 / b ^^^ 2" then () |
1531 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b"; |
1531 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b"; |
1532 |
1532 |
1533 (*SRD Schalk I, p.69 Nr. 459b *) |
1533 (*SRD Schalk I, p.69 Nr. 459b *) |
1534 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)"; |
1534 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)"; |
1535 val Some (t,_) = rewrite_set_ thy false norm_Rational t; |
1535 val SOME (t,_) = rewrite_set_ thy false norm_Rational t; |
1536 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then () |
1536 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then () |
1537 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41"; |
1537 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41"; |
1538 |
1538 |
1539 |
1539 |
1540 (*Schalk I, p.69 Nr. 460b nonterm.SK |
1540 (*Schalk I, p.69 Nr. 460b nonterm.SK |
1541 val t = str2term |
1541 val t = str2term |
1542 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))"; |
1542 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))"; |
1543 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1543 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1544 if term2str t = |
1544 if term2str t = |
1545 then () |
1545 then () |
1546 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42"; |
1546 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42"; |
1547 |
1547 |
1548 val t = str2term |
1548 val t = str2term |
1549 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))"; |
1549 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))"; |
1550 val Some (t',_) = rewrite_set_ thy false norm_Rational t; |
1550 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; |
1551 ... non terminating. |
1551 ... non terminating. |
1552 val Some (t',_) = rewrite_set_ thy false make_polynomial t; |
1552 val SOME (t',_) = rewrite_set_ thy false make_polynomial t; |
1553 "(-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)"; |
1553 "(-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)"; |
1554 val Some (t,_) = rewrite_set_ thy false cancel_p t'; |
1554 val SOME (t,_) = rewrite_set_ thy false cancel_p t'; |
1555 ... non terminating.*) |
1555 ... non terminating.*) |
1556 |
1556 |
1557 (*SRD Schalk I, p.70 Nr. 472a *) |
1557 (*SRD Schalk I, p.70 Nr. 472a *) |
1558 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\ |
1558 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\ |
1559 \((4*x - 8*y)/(x + y))"; |
1559 \((4*x - 8*y)/(x + y))"; |
1560 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1560 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1561 term2str t; |
1561 term2str t; |
1562 if (term2str t) = |
1562 if (term2str t) = |
1563 "x + y" |
1563 "x + y" |
1564 then () |
1564 then () |
1565 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43"; |
1565 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43"; |
1570 (*----------------------------------------------------------------------*) |
1570 (*----------------------------------------------------------------------*) |
1571 |
1571 |
1572 (*SRD Schalk I, p.69 Nr. 461a *) |
1572 (*SRD Schalk I, p.69 Nr. 461a *) |
1573 val t = str2term |
1573 val t = str2term |
1574 "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))"; |
1574 "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))"; |
1575 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1575 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1576 term2str t; |
1576 term2str t; |
1577 if (term2str t) = |
1577 if (term2str t) = |
1578 "1 / 2" |
1578 "1 / 2" |
1579 then () |
1579 then () |
1580 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44"; |
1580 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44"; |
1581 |
1581 |
1582 (*SRD Schalk I, p.69 Nr. 464b *) |
1582 (*SRD Schalk I, p.69 Nr. 464b *) |
1583 val t = str2term |
1583 val t = str2term |
1584 "(a - a/(a - 2)) / (a + a/(a - 2))"; |
1584 "(a - a/(a - 2)) / (a + a/(a - 2))"; |
1585 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1585 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1586 term2str t; |
1586 term2str t; |
1587 if (term2str t) = |
1587 if (term2str t) = |
1588 "(3 + -1 * a) / (1 + -1 * a)" |
1588 "(3 + -1 * a) / (1 + -1 * a)" |
1589 then () |
1589 then () |
1590 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45"; |
1590 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45"; |
1591 |
1591 |
1592 (*SRD Schalk I, p.69 Nr. 465b *) |
1592 (*SRD Schalk I, p.69 Nr. 465b *) |
1593 val t = str2term |
1593 val t = str2term |
1594 "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)"; |
1594 "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)"; |
1595 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1595 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1596 term2str t; |
1596 term2str t; |
1597 if (term2str t) = |
1597 if (term2str t) = |
1598 "(4 * x + 6 * y + -9 * z) / (4 * x)" |
1598 "(4 * x + 6 * y + -9 * z) / (4 * x)" |
1599 then () |
1599 then () |
1600 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46"; |
1600 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46"; |
1601 |
1601 |
1602 (*SRD Schalk I, p.69 Nr. 466b *) |
1602 (*SRD Schalk I, p.69 Nr. 466b *) |
1603 val t = str2term |
1603 val t = str2term |
1604 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))"; |
1604 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))"; |
1605 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1605 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1606 term2str t; |
1606 term2str t; |
1607 if (term2str t) = |
1607 if (term2str t) = |
1608 "(25 + -10 * x + x ^^^ 2) / 18" |
1608 "(25 + -10 * x + x ^^^ 2) / 18" |
1609 then () |
1609 then () |
1610 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47"; |
1610 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47"; |
1611 |
1611 |
1612 (*SRD Schalk I, p.70 Nr. 469 *) |
1612 (*SRD Schalk I, p.70 Nr. 469 *) |
1613 val t = str2term |
1613 val t = str2term |
1614 "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))"; |
1614 "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))"; |
1615 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1615 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t; |
1616 term2str t; |
1616 term2str t; |
1617 if (term2str t) = |
1617 if (term2str t) = |
1618 "3 * b ^^^ 3 / (2 * a + -2 * b)" |
1618 "3 * b ^^^ 3 / (2 * a + -2 * b)" |
1619 then () |
1619 then () |
1620 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48"; |
1620 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48"; |
1905 val thy = Rational.thy; |
1905 val thy = Rational.thy; |
1906 "---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)"; |
1906 "---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)"; |
1907 val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)"; |
1907 val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)"; |
1908 val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*); |
1908 val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*); |
1909 "----- with rewrite_set_"; |
1909 "----- with rewrite_set_"; |
1910 val Some (tt',asm) = rewrite_set_ thy false make_polynomial tt; |
1910 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt; |
1911 term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*); |
1911 term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*); |
1912 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*); |
1912 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*); |
1913 val Some (tt',asm) = rewrite_set_ thy false make_polynomial tt; |
1913 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt; |
1914 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*); |
1914 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*); |
1915 |
1915 |
1916 "----- with make_deriv"; |
1916 "----- with make_deriv"; |
1917 val Some (tt, _) = factout_p_ Isac.thy t; term2str tt = |
1917 val SOME (tt, _) = factout_p_ Isac.thy t; term2str tt = |
1918 "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))"; |
1918 "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))"; |
1919 (* |
1919 (* |
1920 "--- with ruleset as before 060829"; |
1920 "--- with ruleset as before 060829"; |
1921 val {rules, rew_ord=(_,ro),...} = |
1921 val {rules, rew_ord=(_,ro),...} = |
1922 rep_rls (assoc_rls "make_polynomial"); |
1922 rep_rls (assoc_rls "make_polynomial"); |
1923 val der = make_deriv thy Atools_erls rules ro None tt; |
1923 val der = make_deriv thy Atools_erls rules ro NONE tt; |
1924 print_depth 99; map (term2str o #1) der; print_depth 3; |
1924 print_depth 99; map (term2str o #1) der; print_depth 3; |
1925 print_depth 99; map (rule2str o #2) der; print_depth 3; |
1925 print_depth 99; map (rule2str o #2) der; print_depth 3; |
1926 ... did not terminate"*) |
1926 ... did not terminate"*) |
1927 "--- with simpler ruleset"; |
1927 "--- with simpler ruleset"; |
1928 val {rules, rew_ord=(_,ro),...} = |
1928 val {rules, rew_ord=(_,ro),...} = |
1929 rep_rls (assoc_rls "rev_rew_p"); |
1929 rep_rls (assoc_rls "rev_rew_p"); |
1930 val der = make_deriv thy Atools_erls rules ro None tt; |
1930 val der = make_deriv thy Atools_erls rules ro NONE tt; |
1931 print_depth 99; writeln (deriv2str der); print_depth 3; |
1931 print_depth 99; writeln (deriv2str der); print_depth 3; |
1932 |
1932 |
1933 print_depth 99; map (term2str o #1) der; print_depth 3; |
1933 print_depth 99; map (term2str o #1) der; print_depth 3; |
1934 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]"; |
1934 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]"; |
1935 print_depth 99; map (rule2str o #2) der; print_depth 3; |
1935 print_depth 99; map (rule2str o #2) der; print_depth 3; |
1936 print_depth 99; map (term2str o #1 o #3) der; print_depth 3; |
1936 print_depth 99; map (term2str o #1 o #3) der; print_depth 3; |
1937 |
1937 |
1938 val der = make_deriv thy Atools_erls rules ro None |
1938 val der = make_deriv thy Atools_erls rules ro NONE |
1939 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"); |
1939 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"); |
1940 print_depth 99; writeln (deriv2str der); print_depth 3; |
1940 print_depth 99; writeln (deriv2str der); print_depth 3; |
1941 |
1941 |
1942 val {rules, rew_ord=(_,ro),...} = |
1942 val {rules, rew_ord=(_,ro),...} = |
1943 rep_rls (assoc_rls "rev_rew_p"); |
1943 rep_rls (assoc_rls "rev_rew_p"); |
1944 val der = make_deriv thy Atools_erls rules ro None |
1944 val der = make_deriv thy Atools_erls rules ro NONE |
1945 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)"); |
1945 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)"); |
1946 print_depth 99; writeln (deriv2str der); print_depth 3; |
1946 print_depth 99; writeln (deriv2str der); print_depth 3; |
1947 print_depth 99; map (term2str o #1) der; print_depth 3; |
1947 print_depth 99; map (term2str o #1) der; print_depth 3; |
1948 (*WN060829 ...postponed*) |
1948 (*WN060829 ...postponed*) |
1949 |
1949 |
1981 "-------- SK 060904 ----------------------------------------------"; |
1981 "-------- SK 060904 ----------------------------------------------"; |
1982 "-------- SK 060904 ----------------------------------------------"; |
1982 "-------- SK 060904 ----------------------------------------------"; |
1983 "----- order on polynomials -- input + output"; |
1983 "----- order on polynomials -- input + output"; |
1984 val thy = Isac.thy; |
1984 val thy = Isac.thy; |
1985 val t = str2term "(a + -1 * b) / (-1 * a + b)"; |
1985 val t = str2term "(a + -1 * b) / (-1 * a + b)"; |
1986 val Some (t', _) = factout_p_ thy t; term2str t'; |
1986 val SOME (t', _) = factout_p_ thy t; term2str t'; |
1987 val Some (t', _) = cancel_p_ thy t; term2str t'; |
1987 val SOME (t', _) = cancel_p_ thy t; term2str t'; |
1988 |
1988 |
1989 val t = str2term "a*b*c*d / (d*e*f*g)"; |
1989 val t = str2term "a*b*c*d / (d*e*f*g)"; |
1990 val Some (t', _) = cancel_p_ thy t; term2str t'; |
1990 val SOME (t', _) = cancel_p_ thy t; term2str t'; |
1991 |
1991 |
1992 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))"; |
1992 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))"; |
1993 val Some (t', _) = cancel_p_ thy t; term2str t'; |
1993 val SOME (t', _) = cancel_p_ thy t; term2str t'; |
1994 (*???order.SK ???*) |
1994 (*???order.SK ???*) |
1995 |
1995 |
1996 "----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx"; |
1996 "----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx"; |
1997 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))"; |
1997 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))"; |
1998 val Some (t',_) = rewrite_set_ thy false norm_Rational t; |
1998 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; |
1999 if term2str t' = "(2 + -1 * x) / (3 + y)" then () |
1999 if term2str t' = "(2 + -1 * x) / (3 + y)" then () |
2000 else raise error "rational.sml SK060904-1a worked since 0707xx"; |
2000 else raise error "rational.sml SK060904-1a worked since 0707xx"; |
2001 |
2001 |
2002 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx"; |
2002 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx"; |
2003 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
2003 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\ |
2004 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
2004 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))"; |
2005 val Some (t',_) = cancel_p_ thy t; |
2005 val SOME (t',_) = cancel_p_ thy t; |
2006 if term2str t' = "1 / (4 * c + 3 * e)" then () |
2006 if term2str t' = "1 / (4 * c + 3 * e)" then () |
2007 else raise error "rational.sml SK060904-1b"; |
2007 else raise error "rational.sml SK060904-1b"; |
2008 |
2008 |
2009 |
2009 |
2010 "----- SK060904-2a non-termination of add_fraction_p_"; |
2010 "----- SK060904-2a non-termination of add_fraction_p_"; |
2011 val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \ |
2011 val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \ |
2012 \ (-1 * a + b * x) / (a + b * x) "; |
2012 \ (-1 * a + b * x) / (a + b * x) "; |
2013 (* nonterm.SK |
2013 (* nonterm.SK |
2014 val Some (t',_) = rewrite_set_ thy false common_nominator_p t; |
2014 val SOME (t',_) = rewrite_set_ thy false common_nominator_p t; |
2015 |
2015 |
2016 common_nominator_p_ thy t; |
2016 common_nominator_p_ thy t; |
2017 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \ |
2017 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \ |
2018 \ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) "; |
2018 \ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) "; |
2019 |
2019 |