290 rewrite__set_ thy (i+1) false; |
273 rewrite__set_ thy (i+1) false; |
291 term2str a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*) |
274 term2str a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*) |
292 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a |
275 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a |
293 ============ inhibit exn WN130823: prepat is empty ===================================*) |
276 ============ inhibit exn WN130823: prepat is empty ===================================*) |
294 |
277 |
295 (*========== inhibit exn WN130824 TODO ======================================================= |
278 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; |
296 "-------- external calculating functions test -----------"; |
279 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; |
297 "-------- external calculating functions test -----------"; |
280 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; |
298 "-------- external calculating functions test -----------"; |
281 val t = str2term "(12 * x * y) / (8 * y^^^2 )"; |
299 val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; |
282 (* "-------- example 187a": exception Div raised... |
300 val SOME (t', asm) = factout_p_ thy t; |
283 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*) |
301 if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]" |
284 val t = str2term "(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )"; |
302 then () else error "factout_p_ 1 changed"; |
285 (* "-------- example 187b": doesn't terminate... |
303 val SOME (t', asm) = cancel_p_ thy t; |
286 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*) |
304 if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]" |
287 val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )"; |
305 then () else error "cancel_p_ 1 changed"; |
288 (* "-------- example 187c": doesn't terminate... |
306 |
289 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*) |
307 val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; |
290 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac}, false, cancel_p, t); |
308 val SOME (t', asm) = factout_(*p_*) thy t; |
291 (* WN130827: exception Div raised... |
309 if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]" |
292 rewrite__set_ thy 1 bool [] rls term |
310 then () else error "factout_ 2 changed"; |
293 *) |
311 val SOME (t', asm) = cancel_(*p_*) thy t; |
294 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) = |
312 if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]" |
295 (thy, 1, bool, [], rls, term); |
313 then () else error "cancel_ 2 changed"; |
296 (* WN130827: exception Div raised... |
314 |
297 val (t', asm, rew) = app_rev thy (i+1) rrls t |
315 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; |
298 *) |
316 val SOME (t', asm) = add_fraction_p_ thy t; |
299 "~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t); |
317 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" |
300 (* WN130827: exception Div raised... |
318 then () else error "add_fraction_p_ 3 changed"; |
301 val opt = app_rev' thy rrls t |
319 val SOME (t', asm) = common_nominator_p_ thy t; |
302 *) |
320 if term2str t' = |
303 "~~~~~ fun app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) = |
321 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" |
304 (thy, rrls, t); |
322 andalso terms2str asm = "[]" |
305 chk_prepat thy erls prepat t = true; |
323 then () else error "common_nominator_p_ 3 changed"; |
306 (* WN130827: exception Div raised... |
324 |
307 normal_form t |
325 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; |
308 *) |
326 val SOME (t', asm) = add_fraction_ thy t; |
309 (* lookup Rational.thy, cancel_p: normal_form = cancel_p_ thy*) |
327 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" |
310 "~~~~~ fun cancel_p_, args:"; val (t) = (t); |
328 then () else error "factout_ 4 changed"; |
311 val opt = check_fraction t; |
329 val SOME (t', asm) = common_nominator_ thy t; |
312 val SOME (numerator, denominator) = opt |
330 if term2str t' = |
313 val vs = t |> vars |> map free2str |> sort string_ord |
331 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" |
314 val baseT = type_of numerator |
332 andalso terms2str asm = "[]" |
315 val expT = HOLogic.realT |
333 then () else error "cancel_ 4 changed"; |
316 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator); |
334 |
317 (*"-------- example 187a": exception Div raised... |
335 val t = str2term |
318 val a = [(12, [1, 1])]: poly |
336 "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))"; |
319 val b = [(8, [0, 2])]: poly |
337 val SOME (t', asm) = add_fraction_p_ thy t; |
320 val ((a', b'), c) = gcd_poly a b |
338 if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" |
321 *) |
339 then () else error "add_fraction_p_ 5 changed"; |
322 (* "-------- example 187b": doesn't terminate... |
340 val SOME (t', asm) = norm_rational_ thy t; |
323 val a = [(8, [2, 1, 1])]: poly |
341 if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" |
324 val b = [(18, [1, 2, 1])]: poly |
342 then () else error "norm_rational_ 5 changed"; |
325 val ((a', b'), c) = gcd_poly a b |
343 ============ inhibit exn WN130826 TODO ========================================================*) |
326 *) |
344 |
327 (* "-------- example 187c": doesn't terminate... |
345 |
328 val a = [(9, [5, 2, 4])]: poly |
346 "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------"; |
329 val b = [(15, [6, 3, 1])]: poly |
347 "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------"; |
330 val ((a', b'), c) = gcd_poly a b |
348 "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------"; |
331 *) |
|
332 |
|
333 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
|
334 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
|
335 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
349 val thy = @{theory "Rational"}; |
336 val thy = @{theory "Rational"}; |
350 "-------- WN"; |
337 "-------- WN"; |
351 val t = str2term "(2 + -3 * x) / 9"; |
338 val t = str2term "(2 + -3 * x) / 9"; |
352 if NONE = rewrite_set_ thy false cancel_p t then () |
339 if NONE = rewrite_set_ thy false cancel_p t then () |
353 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled"; |
340 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled"; |
510 val t = str2term "(-25 + 9*x^^^2)/(5 + 3*x)"; |
497 val t = str2term "(-25 + 9*x^^^2)/(5 + 3*x)"; |
511 val SOME (t, asm) = rewrite_set_ thy false cancel_p t; |
498 val SOME (t, asm) = rewrite_set_ thy false cancel_p t; |
512 if (term2str t', terms2str asm) = ("(2 * x + 10 * x ^^^ 2) / (1 + -5 * x)", "[]") |
499 if (term2str t', terms2str asm) = ("(2 * x + 10 * x ^^^ 2) / (1 + -5 * x)", "[]") |
513 then () else error "rational.sml cancel WN 1"; |
500 then () else error "rational.sml cancel WN 1"; |
514 |
501 |
515 (*========== inhibit exn WN130826 TODO ========================================================= |
502 "-------- example heuberger"; |
516 "-------- some old tests REVISE ! --------------------------------------------"; |
503 val t = str2term ("(x^^^4 + x * y + x^^^3 * y + y^^^2) / " ^ |
517 "-------- some old tests REVISE ! --------------------------------------------"; |
504 "(x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)"); |
518 "-------- some old tests REVISE ! --------------------------------------------"; |
505 val SOME (t', asm) = rewrite_set_ thy false cancel_p t; |
519 (*WAS --- external calculating functions test ---*) |
506 if (term2str t', terms2str asm) = |
520 val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))"; |
507 ("(x ^^^ 3 + y) / (1 + 5 * x + x * y ^^^ 3)", "[\"1 + 5 * x + x * y ^^^ 3 ~= 0\"]") |
521 val SOME (t', asm) = factout_p_ thy t; |
508 then () else error "rational.sml cancel_p heuberger"; |
522 if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]" |
509 |
523 then () else error "factout_p_ 1 changed"; |
510 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; |
524 val SOME (t', asm) = cancel_p_ thy t; |
511 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; |
525 if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]" |
512 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; |
526 then () else error "cancel_p_ 1 changed"; |
513 (*deleted example 204 ... 236b at update Isabelle2012-->2013*) |
527 |
514 |
528 val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))"; |
|
529 val SOME (t', asm) = factout_(*p_*) thy t; |
|
530 if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]" |
|
531 then () else error "factout_ 2 changed"; |
|
532 val SOME (t', asm) = cancel_(*p_*) thy t; |
|
533 if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]" |
|
534 then () else error "cancel_ 2 changed"; |
|
535 |
|
536 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))"; |
|
537 val SOME (t', asm) = add_fraction_p_ thy t; |
|
538 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" |
|
539 then () else error "add_fraction_p_ 3 changed"; |
|
540 val SOME (t', asm) = common_nominator_p_ thy t; |
|
541 if term2str t' = |
|
542 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" |
|
543 andalso terms2str asm = "[]" |
|
544 then () else error "common_nominator_p_ 3 changed"; |
|
545 |
|
546 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))"; |
|
547 val SOME (t', asm) = add_fraction_ thy t; |
|
548 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]" |
|
549 then () else error "factout_ 4 changed"; |
|
550 val SOME (t', asm) = common_nominator_ thy t; |
|
551 if term2str t' = |
|
552 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))" |
|
553 andalso terms2str asm = "[]" |
|
554 then () else error "cancel_ 4 changed"; |
|
555 |
|
556 val t = str2term |
|
557 "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))"; |
|
558 val SOME (t', asm) = add_fraction_p_ thy t; |
|
559 if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" |
|
560 then () else error "add_fraction_p_ 5 changed"; |
|
561 val SOME (t', asm) = norm_rational_ thy t; |
|
562 if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]" |
|
563 then () else error "norm_rational_ 5 changed"; |
|
564 |
|
565 |
|
566 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))"; |
|
567 val SOME (t3',_) = common_nominator_ thy t3; |
|
568 val SOME (t3'',_) = add_fraction_ thy t3; |
|
569 (term2str t3'); |
|
570 (term2str t3''); |
|
571 |
|
572 val SOME(t4,t5) = norm_expanded_rat_ thy t3; |
|
573 term2str t4; |
|
574 term2str (hd(t5)); |
|
575 |
|
576 |
|
577 |
|
578 val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)"; |
|
579 val SOME (t',_) = factout_ thy t; |
|
580 val SOME (t'',_) = cancel_ thy t; |
|
581 term2str t'; |
|
582 term2str t''; |
|
583 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))"; |
|
584 "(3 + x) / (3 - x)"; |
|
585 |
|
586 val t=(term_of o the o (parse thy)) |
|
587 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)"; |
|
588 val SOME (t',_) = common_nominator_ thy t; |
|
589 val SOME (t'',_) = add_fraction_ thy t; |
|
590 term2str t'; |
|
591 term2str t''; |
|
592 "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))"; |
|
593 "(4 + x) / (3 - x)"; |
|
594 |
|
595 (*WN021016 added -----vv---*) |
|
596 val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1"; |
|
597 val SOME (t',_) = common_nominator_ thy t; |
|
598 val SOME (t'',_) = add_fraction_ thy t; |
|
599 term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1" ^ |
|
600 " * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); |
|
601 term2str t'' = "6 / (3 - x)" (*true*); |
|
602 |
|
603 val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)"; |
|
604 val SOME (t',_) = common_nominator_ thy t; |
|
605 val SOME (t'',_) = add_fraction_ thy t; |
|
606 term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n" ^ |
|
607 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*); |
|
608 term2str t'' = "6 / (3 - x)" (*true*); |
|
609 (*WN021016 added -----^^---*) |
|
610 (*WN030602 added -----vv--- no rewrite -> NONE !*) |
|
611 val t = str2term "1 / a"; |
|
612 val NONE = cancel_p_ thy t; |
|
613 val NONE = rewrite_set_ thy false cancel_p t; |
|
614 (*WN.2.6.03 added -------^^---*) |
|
615 |
|
616 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)"; |
|
617 val SOME (t',_) = factout_ thy t; |
|
618 val SOME (t'',_) = cancel_ thy t; |
|
619 term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*); |
|
620 term2str t'' = "(y + x) / (y - x)"; |
|
621 |
|
622 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)"; |
|
623 val SOME (t',_) = common_nominator_ thy t; |
|
624 val SOME (t'',_) = add_fraction_ thy t; |
|
625 term2str t' = |
|
626 "(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1" ^ |
|
627 " * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*); |
|
628 term2str t'' = "(-1 - x - y) / (x - y)" (*true*); |
|
629 |
|
630 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)"; |
|
631 val SOME (t',_) = common_nominator_ thy t; |
|
632 val SOME (t'',_) = add_fraction_ thy t; |
|
633 if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))" ^ |
|
634 " +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then () |
|
635 else error "rational.sml lex-ord 1"; |
|
636 if term2str t'' = "(-1 - y - x) / (y - x)" then () |
|
637 else error "rational.sml lex-ord 2"; |
|
638 (*WN.16.10.02 WN070905 lexicographische Ordnung erhalten *) |
|
639 |
|
640 |
|
641 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)"; |
|
642 val SOME (t',_) = norm_expanded_rat_ thy t; |
|
643 if term2str t' = "(x + y) / (x - y)" then () |
|
644 else error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 No.1"; |
|
645 (*val SOME (t'',_) = norm_rational_ thy t; |
|
646 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial |
|
647 WN.16.10.02 ?! + WN060831???SK4 |
|
648 WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*) |
|
649 |
|
650 |
|
651 val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)"; |
|
652 val SOME (t',_) = norm_expanded_rat_ thy t; |
|
653 if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then () |
|
654 else error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +..."; |
|
655 (*val SOME (t'',_) = norm_rational_ thy t; |
|
656 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?! |
|
657 WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*) |
|
658 |
|
659 val t=(term_of o the o (parse thy)) |
|
660 "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)"; |
|
661 val SOME (t',_) = norm_expanded_rat_ thy t; |
|
662 val SOME (t'',_) = norm_rational_ thy t; |
|
663 term2str t'; |
|
664 term2str t''; |
|
665 "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)"; |
|
666 "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)"; |
|
667 |
|
668 |
|
669 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; |
|
670 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; |
|
671 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag"; |
|
672 val thy = @{theory "Rational"}; |
|
673 val thy' = "Rational"; |
|
674 val rls' = "cancel"; |
|
675 val mp = "make_polynomial"; |
|
676 |
|
677 writeln ("example 186:"); |
|
678 writeln("a)"); |
|
679 val e186a'="(14 * x * y) / ( x * y )";(*SRC*) |
|
680 rewrite_set_ thy false cancel (str2term e186a'); |
|
681 "@@@@@@@@@@@@@@"; |
|
682 val e186a = the (rewrite_set thy' false "cancel" e186a'); |
|
683 is_expanded (parse_rat "14 * x * y"); |
|
684 is_expanded (parse_rat "x * y"); |
|
685 if e186a = ("14 / 1", "[\"y * x ~= 0\"]") then () |
|
686 else error "rational.sml cancel Schalk e186a"; |
|
687 |
|
688 writeln("b)"); |
|
689 val e186b'="(60 * a * b) / ( 15 * a * b )"; |
|
690 val e186b = the (rewrite_set thy' false "cancel" e186b'); |
|
691 writeln("c)"); |
|
692 val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )"; |
|
693 val e186c = (the (rewrite_set thy' false "cancel" e186c')) |
|
694 handle e => print_exn_G e; |
|
695 val t = (term_of o the o (parse thy)) e186c'; |
|
696 if e186c = ("12 * a / 1", "[\"12 * (c * (b * a)) ~= 0\"]") then () |
|
697 else error "rational.sml cancel Schalk e186c"; |
|
698 |
|
699 writeln ("example 187:"); |
|
700 writeln("a)"); |
|
701 val e187a'="(12 * x * y) / (8 * y^^^2 )";(*SRC*) |
|
702 val e187a = the (rewrite_set thy' false "cancel" e187a'); |
|
703 writeln("b)"); |
|
704 val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )"; |
|
705 val e187b = the (rewrite_set thy' false "cancel" e187b'); |
|
706 writeln("c)"); |
|
707 val e187d'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*) |
|
708 val e187d = the (rewrite_set thy' false "cancel" e187d'); |
|
709 if e187d = ("3 * z ^^^ 3 / (5 * (y * x))", |
|
710 "[\"3 * (z * (y ^^^ 2 * x ^^^ 5)) ~= 0\"]") then () |
|
711 else error "rational.sml cancel Schalk e186d"; |
|
712 |
|
713 writeln "example 188:"; |
|
714 val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*) |
|
715 val e188a = the (rewrite_set thy' false "cancel" e188a'); |
|
716 is_expanded (parse_rat "8 * x + -8"); |
|
717 (* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*) |
|
718 if e188a = ("8 / 9", "[\"-1 + x ~= 0\"]") then () |
|
719 else error "rational.sml: e188a new behaviour"; |
|
720 |
|
721 val SOME (t,_) = rewrite_set thy' false mp "(8*((-1) + x))/(9*((-1) + x))"; |
|
722 writeln("b)"); |
|
723 val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*) |
|
724 val SOME (t, asm) = rewrite_set thy' false "cancel" e188b'; |
|
725 t = "5 / 6" (*true*); |
|
726 writeln("c)"); |
|
727 |
|
728 val e188c'="( a + -1 * b ) / ( b + -1 * a )"; |
|
729 val e188c = the (rewrite_set thy' false "cancel_p" e188c'); |
|
730 (*is_expanded (parse_rat "a + -1 * b");*) |
|
731 val SOME (t,_) = |
|
732 rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))"; |
|
733 if t= "(a + -1 * b) / (-1 * a + b)" then() |
|
734 else error "rational.sml: e188c new behaviour"; |
|
735 |
|
736 writeln ("example 190:"); |
|
737 writeln("c)"); |
|
738 val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )"; |
|
739 val e190c = the (rewrite_set thy' false "cancel" e190c'); |
|
740 val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))"; |
|
741 if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then () |
|
742 else error "rational.sml: e190c new behaviour"; |
|
743 |
|
744 writeln ("example 191:"); |
|
745 writeln("a)"); |
|
746 val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )"; |
|
747 (*WN.23.10.02------- |
|
748 val e191a = the (rewrite_set thy' false "cancel" e191a'); |
|
749 is_expanded (parse_rat "x^^^2 + -1 * y^^^2"); |
|
750 false; |
|
751 is_expanded (parse_rat "x + y"); |
|
752 true; -----------*) |
|
753 val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))"; |
|
754 (* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*) |
|
755 if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() |
|
756 else error "rational.sml: e191a new behaviour"; |
|
757 |
|
758 writeln("c)"); |
|
759 val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )"; |
|
760 (*WN.23.10.02------- |
|
761 val e191c = the (rewrite_set thy' false "cancel" e191c'); |
|
762 is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25"); |
|
763 false; |
|
764 is_expanded (parse_rat "25 + -30*x + 9*x^^^2"); |
|
765 false; |
|
766 is_expanded (parse_rat "-25 + 9*x^^^2"); |
|
767 true;------------*) |
|
768 val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))"; |
|
769 (* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*) |
|
770 if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then() |
|
771 else error "rational.sml: 'e191c' new behaviour"; |
|
772 |
|
773 |
|
774 writeln ("example 192:"); |
|
775 writeln("b)"); |
|
776 val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )"; |
|
777 (*WN.23.10.02------- |
|
778 val e192b = the (rewrite_set thy' false "cancel" e192b'); |
|
779 -------------------*) |
|
780 val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))"; |
|
781 (*========== inhibit exn 110317 ================================================ |
|
782 if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" |
|
783 (*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*) |
|
784 then () else error "rational.sml: 'e192b' new behaviour"; |
|
785 (*^^^ works with MG's simplifier vvv*) |
|
786 val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))"; |
|
787 val SOME (t',_) = rewrite_set_ thy false make_polynomial t; |
|
788 if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else error "rational.sml: 'e192b'MG new behaviour"; |
|
789 ============ inhibit exn 110317 ==============================================*) |
|
790 |
|
791 writeln ("example 193:"); |
|
792 writeln("a)"); |
|
793 val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )"; |
|
794 (*WN.23.10.02------- |
|
795 val e193a = the (rewrite_set thy' false "cancel" e193a'); |
|
796 -------------------*) |
|
797 writeln("b)"); |
|
798 val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )"; |
|
799 (*WN.23.10.02------- |
|
800 val e193b = the (rewrite_set thy' false "cancel" e193b'); |
|
801 writeln("c)"); |
|
802 val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )"; |
|
803 val SOME(t,_) = rewrite_set thy' false "cancel" e193c'; |
|
804 -------------------*) |
|
805 |
|
806 val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)"; |
|
807 val SOME (t, asm) = rewrite_set thy' false "cancel" wn01; |
|
808 (* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*) |
|
809 if t = "(-5 + 3 * x) / 1" andalso asm = "[\"5 + 3 * x ~= 0\"]" then () |
|
810 else error "rational.sml: new behav. in cancel wn01"; |
|
811 |
|
812 "-------- common_nominator_p ----------------------------"; |
|
813 "-------- common_nominator_p ----------------------------"; |
|
814 "-------- common_nominator_p ----------------------------"; |
|
815 val rls' = "common_nominator_p"; |
|
816 |
|
817 writeln ("example 204:"); |
|
818 writeln("a)"); |
|
819 val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)"; |
|
820 val e204a = the (rewrite_set thy' false "common_nominator_p" e204a'); |
|
821 writeln("b)"); |
|
822 val e204b'="5 / x + -3 / x + -1 / x"; |
|
823 val e204b = the (rewrite_set thy' false "common_nominator_p" e204b'); |
|
824 if e204b = ("1 / x", "[]") then () |
|
825 else error "rational.sml common_nominator_p example e204b"; |
|
826 |
|
827 writeln ("example 205:"); |
|
828 writeln("a)"); |
|
829 val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)"; |
|
830 val e205a = the (rewrite_set thy' false "common_nominator_p" e205a'); |
|
831 writeln("b)"); |
|
832 val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)"; |
|
833 val e205b = the (rewrite_set thy' false "common_nominator_p" e205b'); |
|
834 if e205b = ("(1 + x) / 1", "[]") then () |
|
835 else error "rational.sml common_nominator_p example e204b"; |
|
836 |
|
837 writeln ("example 206:"); |
|
838 writeln("a)"); |
|
839 val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))"; |
|
840 val e206a = the (rewrite_set thy' false "common_nominator_p" e206a'); |
|
841 writeln("b)"); |
|
842 val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))"; |
|
843 val e206b = the (rewrite_set thy' false "common_nominator_p" e206b'); |
|
844 |
|
845 writeln ("example 207:"); |
|
846 val e207'="((3 * x * y + 3 * y) / (x * y)) + ((5 * x * y + 7 * y) / (x * y)) + ((9 * x * y + -2 * y) / (x * y)) + ((x * y + 4 * y) / (x * y)) "; |
|
847 val e207 = the (rewrite_set thy' false "common_nominator_p" e207'); |
|
848 |
|
849 writeln ("example 208:"); |
|
850 val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) "; |
|
851 val e208 = the (rewrite_set thy' false "common_nominator_p" e208'); |
|
852 |
|
853 writeln ("example 209:"); |
|
854 val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) "; |
|
855 val e209 = the (rewrite_set thy' false "common_nominator_p" e209'); |
|
856 |
|
857 writeln ("example 210:"); |
|
858 val e210'="((2 * x + 3 + -1 * x^^^2) / (5 * x)) + ((5 * x^^^2 + -2 * x + 1) / (5 * x)) + ((-3 * x^^^2 + -2 * x + 1) / (5 * x)) + ((-1 * x^^^2 + -3 * x + -5) / (5 * x)) "; |
|
859 val e210 = the (rewrite_set thy' false "common_nominator_p" e210'); |
|
860 |
|
861 writeln ("example 211:"); |
|
862 writeln("a)"); |
|
863 val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))"; |
|
864 val e211a = the (rewrite_set thy' false "common_nominator_p" e211a'); |
|
865 writeln("b)"); |
|
866 val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))"; |
|
867 val e211b = the (rewrite_set thy' false "common_nominator_p" e211b'); |
|
868 |
|
869 writeln ("example 212:"); |
|
870 writeln("a)"); |
|
871 val e212a'="((4) / (x)) + ((-3) / (y)) + -1"; |
|
872 val e212a = the (rewrite_set thy' false "common_nominator_p" e212a'); |
|
873 writeln("b)"); |
|
874 val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))"; |
|
875 val e212b = the (rewrite_set thy' false "common_nominator_p" e212b'); |
|
876 |
|
877 writeln ("example 213:"); |
|
878 writeln("a)"); |
|
879 val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) "; |
|
880 val e213a = the (rewrite_set thy' false "common_nominator_p" e213a'); |
|
881 writeln("b)"); |
|
882 val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))"; |
|
883 val e213b = the (rewrite_set thy' false "common_nominator_p" e213b'); |
|
884 |
|
885 writeln ("example 214:"); |
|
886 writeln("a)"); |
|
887 val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))"; |
|
888 val e214a = the (rewrite_set thy' false "common_nominator_p" e214a'); |
|
889 writeln("b)"); |
|
890 val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))"; |
|
891 val e214b = the (rewrite_set thy' false "common_nominator_p" e214b'); |
|
892 |
|
893 writeln ("example 216:"); |
|
894 writeln("a)"); |
|
895 val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))"; |
|
896 val e216a = the (rewrite_set thy' false "common_nominator_p" e216a'); |
|
897 writeln("b)"); |
|
898 val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))"; |
|
899 val e216b = the (rewrite_set thy' false "common_nominator_p" e216b'); |
|
900 |
|
901 writeln ("example 217:"); |
|
902 val e217'="((z + -1) / (z)) + ((3 * z ^^^2 + -6 * z + 5) / (z^^^2)) + ((-4 * z^^^3 + 7 * z^^^2 + -5 * z + 5) / (z^^^3))"; |
|
903 val e217 = the (rewrite_set thy' false "common_nominator_p" e217'); |
|
904 |
|
905 |
|
906 val rls' = "common_nominator"; |
|
907 writeln ("example 218:"); |
|
908 val e218'="((9 * a^^^3 - 5 * a^^^2 + 2 * a + 8) / (108 * a^^^4)) + ((-5 * a + 3 * a^^^2 + 4) / (8 * a^^^3)) + ((-261 * a^^^3 + 19 * a^^^2 + -112 * a + 16) / (216 * a^^^4))"; |
|
909 val e218 = the (rewrite_set thy' false "common_nominator" e218'); |
|
910 if e218 = ("(16 - 63 * a ^^^ 2 - 81 * a ^^^ 3) / (108 * a ^^^ 4)", "[]") then () |
|
911 else error "rationa.sml common_nominator example e218"; |
|
912 |
|
913 writeln ("example 219:"); |
|
914 writeln("a)"); |
|
915 val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))"; |
|
916 val e219a = the (rewrite_set thy' false "common_nominator" e219a'); |
|
917 writeln("b)"); |
|
918 val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))"; |
|
919 val e219b = the (rewrite_set thy' false "common_nominator" e219b'); |
|
920 if e219b = ("(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)", "[]") then () |
|
921 else error "rationa.sml common_nominator example e219b"; |
|
922 |
|
923 writeln ("example 220:"); |
|
924 writeln("a)"); |
|
925 val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))"; |
|
926 val e220a = the (rewrite_set thy' false "common_nominator" e220a'); |
|
927 writeln("b)"); |
|
928 val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))"; |
|
929 val e220b = the (rewrite_set thy' false "common_nominator" e220b'); |
|
930 |
|
931 writeln ("example 221:"); |
|
932 writeln("a)"); |
|
933 val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))"; |
|
934 val e221a = the (rewrite_set thy' false "common_nominator" e221a'); |
|
935 writeln("b)"); |
|
936 val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) "; |
|
937 val e221b = the (rewrite_set thy' false "common_nominator" e221b'); |
|
938 |
|
939 writeln ("example 222:"); |
|
940 writeln("a)"); |
|
941 val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))"; |
|
942 val e222a = the (rewrite_set thy' false "common_nominator" e222a'); |
|
943 writeln("b)"); |
|
944 val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))"; |
|
945 val e222b = the (rewrite_set thy' false "common_nominator" e222b'); |
|
946 |
|
947 writeln ("example 225:"); |
|
948 writeln("a)"); |
|
949 val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))"; |
|
950 val e225a = the (rewrite_set thy' false "common_nominator" e225a'); |
|
951 writeln("b)"); |
|
952 val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))"; |
|
953 val e225b = the (rewrite_set thy' false "common_nominator" e225b'); |
|
954 |
|
955 writeln ("example 226:"); |
|
956 writeln("a)"); |
|
957 val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) "; |
|
958 val e226a = the (rewrite_set thy' false "common_nominator" e226a'); |
|
959 writeln("b)"); |
|
960 val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2"; |
|
961 val e226b = the (rewrite_set thy' false "common_nominator" e226b'); |
|
962 |
|
963 writeln ("example 227:"); |
|
964 writeln("a)"); |
|
965 val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 "; |
|
966 val e227a = the (rewrite_set thy' false "common_nominator" e227a'); |
|
967 writeln("b)"); |
|
968 val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 "; |
|
969 val e227b = the (rewrite_set thy' false "common_nominator" e227b'); |
|
970 |
|
971 writeln ("example 228:"); |
|
972 writeln("a)"); |
|
973 val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))"; |
|
974 val e228a = the (rewrite_set thy' false "common_nominator" e228a'); |
|
975 writeln("b)"); |
|
976 val e228b'="((11 * z + 2 * b) / (4 * b * z + -8 * b^^^2)) + ((-8 * z) / (z^^^2 + -4 * b^^^2)) + ((-9 * z + -2 * b) / (4 * b * z + 8 * b^^^2))"; |
|
977 val e228b = the (rewrite_set thy' false "common_nominator" e228b'); |
|
978 |
|
979 |
|
980 writeln ("example 229:"); |
|
981 writeln("a)"); |
|
982 val e229a'="((5 * x^^^2 + y) / (x + 2 * y)) + ((-8 * x^^^3 + 4 * x^^^2 * y + 3 * x * y) / (x^^^2 + -4 * y^^^2)) + ((3 * x^^^2 + -4 * y) / (x + -2 * y))"; |
|
983 val e229a = the (rewrite_set thy' false "common_nominator" e229a'); |
|
984 writeln("b)"); |
|
985 val e229b'="((7 * x^^^2 + y) / (x + 3 * y)) + ((-24 * x^^^2 * y + 5 * x * y + 21 * y^^^2) / (x^^^2 + -9 * y^^^2)) + ((4 * x^^^2 + -6 * y) / (x + -3 * y))"; |
|
986 val e229b = the (rewrite_set thy' false "common_nominator" e229b'); |
|
987 |
|
988 writeln ("example 230:"); |
|
989 writeln("a)"); |
|
990 val e230a'="((5 * x^^^2 + y) / (2 * x + y)) + ((-16 * x^^^3 + 2 * x^^^2 * y + 6 * x * y) / (4 * x^^^2 + -1 * y^^^2)) + ((3 * x^^^2 + -4 * y) / (2 * x + -1 * y))"; |
|
991 val e230a = the (rewrite_set thy' false "common_nominator" e230a'); |
|
992 writeln("b)"); |
|
993 val e230b'="((7 * x^^^2 + y) / (3 * x + y)) + ((-3 * x^^^3 + 15 * x * y + -7 * x^^^2 * y + 7 * y^^^2) / (9 * x^^^2 + -1 * y^^^2)) + ((4 * x^^^2 + -6 * y) / (3 * x + -1 * y))"; |
|
994 val e230b = the (rewrite_set thy' false "common_nominator" e230b'); |
|
995 |
|
996 writeln ("example 231:"); |
|
997 writeln("a)"); |
|
998 val e231a'="((2 * x + 5 * y) / (x)) + ((2 * x^^^3 + -5 * y^^^3 + 3 * x * y^^^2) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-3 * x + -6 * y) / (x + -1 * y))"; |
|
999 val e231a = the (rewrite_set thy' false "common_nominator" e231a'); |
|
1000 writeln("b)"); |
|
1001 val e231b'="((6 * x + 2 * y) / (x)) + ((6 * x^^^2 * y + -4 * x * y^^^2 + -2 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-5 * x + -3 * y) / (x + -1 * y))"; |
|
1002 val e231b = the (rewrite_set thy' false "common_nominator" e231b'); |
|
1003 |
|
1004 writeln ("example 232:"); |
|
1005 writeln("a)"); |
|
1006 val e232a'="((2 * x + 3 * y) / (x)) + ((4 * x^^^3 + -1 * x * y^^^2 + -3 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-5 * x + -6 * y) / (x + -1 * y))"; |
|
1007 val e232a = the (rewrite_set thy' false "common_nominator" e232a'); |
|
1008 writeln("b)"); |
|
1009 val e232b'="((5 * x + 2 * y) / (x)) + ((2 * x^^^3 + -3 * x * y^^^2 + 3 * x^^^2 * y + -2 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-6 * x + -3 * y) / (x + -1 * y))"; |
|
1010 val e232b = the (rewrite_set thy' false "common_nominator" e232b'); |
|
1011 |
|
1012 writeln ("example 233:"); |
|
1013 writeln("a)"); |
|
1014 val e233a'="((5 * x + 6 * y) / (x)) + ((5 * x * y^^^2 + -6 * y^^^3 + -2 * x^^^3 + 3 * x^^^2 * y) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-2 * x + -3 * y) / (x + -1 * y))"; |
|
1015 val e233a = the (rewrite_set thy' false "common_nominator" e233a'); |
|
1016 writeln("b)"); |
|
1017 val e233b'="((6 * x + 5 * y) / (x)) + ((4 * x^^^2 * y + 3 * x * y^^^2 + -5 * y^^^3 + -2 * x^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-3 * x + -2 * y) / (x + -1 * y))"; |
|
1018 val e233b = the (rewrite_set thy' false "common_nominator" e233b'); |
|
1019 |
|
1020 writeln ("example 234:"); |
|
1021 writeln("a)"); |
|
1022 val e234a'="((5 * a + b) / (2 * a * b + -2 * b^^^2)) + ((-3 * a + -1 * b) / (2 * a * b + 2 * b^^^2)) + ((-2 * a) / (a^^^2 + -1 * b^^^2))"; |
|
1023 val e234a = the (rewrite_set thy' false "common_nominator" e234a'); |
|
1024 writeln("b)"); |
|
1025 val e234b'="((5 * a + 3 * b) / (6 * a * b + -18 * b^^^2)) + ((-3 * a + -3 * b) / (6 * a * b + 18 * b^^^2)) + ((-2 * a) / (a^^^2 + -9 * b^^^2)) "; |
|
1026 val e234b = the (rewrite_set thy' false "common_nominator" e234b'); |
|
1027 |
|
1028 writeln ("example 235:"); |
|
1029 writeln("a)"); |
|
1030 val e235a'="((10 * x + 3 * y) / (12 * x * y + -18 * y^^^2)) + ((-6 * x + -3 * y) / (12 * x * y + 18 * y^^^2)) + ((-4 * x) / (4 * x^^^2 + -9 * y^^^2))"; |
|
1031 val e235a = the (rewrite_set thy' false "common_nominator" e235a'); |
|
1032 writeln("b)"); |
|
1033 val e235b'="((8 * a + b) / (4 * a * b + -2 * b^^^2)) + ((-4 * a + -1 * b) / (4 * a * b + 2 * b^^^2)) + ((-2 * a) / (4 * a^^^2 + -1 * b^^^2)) "; |
|
1034 val e235b = the (rewrite_set thy' false "common_nominator" e235b'); |
|
1035 |
|
1036 writeln ("example 236:"); |
|
1037 writeln("a)"); |
|
1038 val e236a'="((8 * a + 5 * b) / (20 * a * b + -50 * b^^^2)) + ((-4 * a + -5 * b) / (20 * a * b + 50 * b^^^2)) + ((-2 * a) / (4 * a^^^2 + -25 * b^^^2))"; |
|
1039 val e236a = the (rewrite_set thy' false "common_nominator" e236a'); |
|
1040 writeln("b)"); |
|
1041 val e236b'="((24 * x + y) / (6 * x * y + -2 * y^^^2)) + ((-18 * x + -1 * y) / (6 * x * y + 2 * y^^^2)) + ((-15 * x) / (9 * x^^^2 + -1 * y^^^2)) "; |
|
1042 val e236b = the (rewrite_set thy' false "common_nominator" e236b'); |
|
1043 |
|
1044 |
|
1045 val rls' = "cancel"; |
|
1046 writeln ("example heuberger:"); |
|
1047 val eheu'="(x^^^4 + x * y + x^^^3 * y + y^^^2) / (x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)"; |
|
1048 val eheu = the (rewrite_set thy' false "cancel" eheu'); |
|
1049 |
|
1050 val rls' = "common_nominator_p"; |
|
1051 writeln ("example stiefel:"); |
|
1052 val est1'="(7) / (-14) + (-2) / (4)"; |
|
1053 val est1 = the (rewrite_set thy' false "common_nominator_p" est1'); |
|
1054 if est1 = ("-1 / 1", "[]") then () |
|
1055 else error "new behaviour in rational.sml: est1'"; |
|
1056 |
|
1057 val t = (term_of o the o (parse thy)) |
|
1058 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
|
1059 val SOME (t',_) = factout_ thy t; |
|
1060 if term2str t' = "(3 + x) * (3 - x) / ((3 - x) * (3 - x))" then () |
|
1061 else error "rational.sml factout_ (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
|
1062 |
|
1063 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
515 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
1064 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
516 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
1065 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
517 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
1066 val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)"); |
518 val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)"); |
1067 "-------- gcd_poly integration level 1: works on exact term"; |
519 "-------- gcd_poly integration level 1: works on exact term"; |
1122 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational"; |
574 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational"; |
1123 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t; |
575 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t; |
1124 if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)" |
576 if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)" |
1125 then () else error "level 5, rewrite_set_ norm_Rational: changed" |
577 then () else error "level 5, rewrite_set_ norm_Rational: changed" |
1126 |
578 |
1127 "-------- reverse rewrite -------------------------------"; |
579 "-------- reverse rewrite ----------------------------------------------------"; |
1128 "-------- reverse rewrite -------------------------------"; |
580 "-------- reverse rewrite ----------------------------------------------------"; |
1129 "-------- reverse rewrite -------------------------------"; |
581 "-------- reverse rewrite ----------------------------------------------------"; |
1130 (*WN.28.8.02: tests for the 'reverse-rewrite' functions: |
582 (** the term for which reverse rewriting is demonstrated **) |
1131 these are defined in Rationals.ML and stored in |
583 val t = str2term "(9 + -1 * x ^^^ 2) / (9 + 6 * x + x ^^^ 2)"; |
1132 the 'reverse-ruleset' cancel*) |
584 val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc, |
1133 |
585 next_rule = nex, normal_form = nor, ...},...} = cancel_p; |
1134 (*the term for which reverse rewriting is demonstrated*) |
586 |
1135 val t = (term_of o the o (parse thy)) |
587 (** normal_form produces the result in ONE step **) |
1136 "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)"; |
|
1137 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc, |
|
1138 next_rule=nex,normal_form=nor,...},...} = cancel; |
|
1139 |
|
1140 (*normal_form produces the result in ONE step*) |
|
1141 val SOME (t',_) = nor t; |
588 val SOME (t',_) = nor t; |
1142 if term2str t' = "(3 - x) / (3 + x)" then () |
589 if term2str t' = "(3 + -1 * x) / (3 + x)" then () |
1143 else error "rational.sml normal_form (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
590 else error "rational.sml normal_form (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1144 |
591 |
1145 (*initialize the interpreter state used by the 'me'*) |
592 (** initialize the interpreter state used by the 'me' **) |
1146 val (t,_,revsets,_) = ini t; |
593 val (t, _, revsets, _) = ini t; |
1147 |
594 |
1148 (*find the rule 'r' to apply to term 't'*) |
595 if length (hd revsets) = 11 then () else error "length of revset changed"; |
|
596 if (revsets |> nth 1 |> nth 1 |> id_of_thm) = |
|
597 (@{thm realpow_twoI} |> string_of_thm |> thmID_of_derivation_name) |
|
598 then () else error "first element of revset changed"; |
|
599 if |
|
600 (revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",??.unknown)" andalso |
|
601 (revsets |> nth 1 |> nth 2 |> rule2str) = |
|
602 "Thm (\"sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))\",??.unknown)" andalso |
|
603 (revsets |> nth 1 |> nth 3 |> rule2str) = |
|
604 "Thm (\"sym_#mult_Float ((2,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso |
|
605 (revsets |> nth 1 |> nth 4 |> rule2str) = |
|
606 "Thm (\"sym_#mult_Float ((~1,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso |
|
607 (revsets |> nth 1 |> nth 5 |> rule2str) = |
|
608 "Thm (\"sym_#mult_Float ((3,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso |
|
609 (revsets |> nth 1 |> nth 6 |> rule2str) = "Rls_ (\"sym_order_mult_rls_\")" andalso |
|
610 (revsets |> nth 1 |> nth 7 |> rule2str) = |
|
611 "Thm (\"sym_mult_assoc\",Groups.semigroup_mult_class.mult_assoc)" |
|
612 then () else error "first 7 elements in revset changed" |
|
613 |
|
614 (** find the rule 'r' to apply to term 't' **) |
|
615 (*/------- since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_ |
|
616 for Isabelle2013, we don't get a working revset, but non-termination: |
|
617 |
1149 val SOME (r as (Thm (str, thm))) = nex revsets t; |
618 val SOME (r as (Thm (str, thm))) = nex revsets t; |
|
619 : |
|
620 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), |
|
621 Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," |
|
622 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), |
|
623 Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))"," |
|
624 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), |
|
625 Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))"," |
|
626 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))"," |
|
627 : |
|
628 ### Isabelle2002: |
|
629 Thm ("sym_#mult_2_3", "6 = 2 * 3") |
|
630 ### Isabelle2009-2 for cancel_ (not cancel_p_): |
1150 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" |
631 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" |
1151 andalso string_of_thm thm = |
632 andalso string_of_thm thm = |
1152 (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) |
633 (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) |
1153 (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () |
634 (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then () |
1154 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
635 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1155 (* before Isa02->09-2 was not checked automatically, ?was different?: |
636 \---------------------------------------------------------------------------------------/*) |
1156 val SOME r = nex revsets t; |
637 |
1157 val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*) |
638 (** check, if the rule 'r' applied by the user to 't' belongs to the ruleset; |
1158 |
|
1159 (* check, if the rule 'r' applied by the user to 't' belongs to the ruleset; |
|
1160 if the rule is OK, the term resulting from applying the rule is returned,too; |
639 if the rule is OK, the term resulting from applying the rule is returned,too; |
1161 there might be several rule applications inbetween, |
640 there might be several rule applications inbetween, |
1162 which are listed after the head in reverse order *) |
641 which are listed after the head in reverse order **) |
|
642 (*/-------------------------------------------- Isabelle2013: this gives "error id_of_thm"; |
|
643 we don't repair this, because interaction within "reverse rewriting" never worked properly: |
|
644 |
1163 val (r, (t, asm))::_ = loc revsets t r; |
645 val (r, (t, asm))::_ = loc revsets t r; |
1164 if term2str t = "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" andalso asm = [] |
646 if term2str t = "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" andalso asm = [] |
1165 then () |
647 then () else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
1166 else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)"; |
|
1167 |
648 |
1168 (* find the next rule to apply *) |
649 (* find the next rule to apply *) |
1169 val SOME (r as (Thm (str, thm))) = nex revsets t; |
650 val SOME (r as (Thm (str, thm))) = nex revsets t; |
1170 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso |
651 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso |
1171 string_of_thm thm = (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) |
652 string_of_thm thm = (string_of_thm o make_thm o (cterm_of (@{theory "Isac"}))) |