42 |
42 |
43 |
43 |
44 "-------- integration lev.1 fun factout_p_ -----------------------------------"; |
44 "-------- integration lev.1 fun factout_p_ -----------------------------------"; |
45 "-------- integration lev.1 fun factout_p_ -----------------------------------"; |
45 "-------- integration lev.1 fun factout_p_ -----------------------------------"; |
46 "-------- integration lev.1 fun factout_p_ -----------------------------------"; |
46 "-------- integration lev.1 fun factout_p_ -----------------------------------"; |
47 val t = TermC.str2term "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)" |
47 val t = TermC.parse_test @{context} "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)" |
48 val SOME (t', asm) = factout_p_ thy t; |
48 val SOME (t', asm) = factout_p_ thy t; |
49 if UnparseC.term t' = "(x + y) * (x + - 1 * y) / (x * (x + - 1 * y))" |
49 if UnparseC.term t' = "(x + y) * (x + - 1 * y) / (x * (x + - 1 * y))" |
50 then () else error ("factout_p_ term 1 changed: " ^ UnparseC.term t') |
50 then () else error ("factout_p_ term 1 changed: " ^ UnparseC.term t') |
51 ; |
51 ; |
52 if UnparseC.terms asm = "[\"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]" |
52 if UnparseC.terms asm = "[\"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]" |
53 then () else error "factout_p_ asm 1 changed" |
53 then () else error "factout_p_ asm 1 changed" |
54 ; |
54 ; |
55 val t = TermC.str2term "nothing + to_cancel ::real"; |
55 val t = TermC.parse_test @{context} "nothing + to_cancel ::real"; |
56 if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable"; |
56 if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable"; |
57 ; |
57 ; |
58 val t = TermC.str2term "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))"; |
58 val t = TermC.parse_test @{context} "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))"; |
59 val SOME (t', asm) = factout_p_ thy t; |
59 val SOME (t', asm) = factout_p_ thy t; |
60 if UnparseC.term t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso |
60 if UnparseC.term t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso |
61 UnparseC.terms asm = "[\"1 + x \<noteq> 0\"]" |
61 UnparseC.terms asm = "[\"1 + x \<noteq> 0\"]" |
62 then () else error "factout_p_ 1 changed"; |
62 then () else error "factout_p_ 1 changed"; |
63 |
63 |
64 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
64 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
65 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
65 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
66 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
66 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
67 val t = TermC.str2term "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)" |
67 val t = TermC.parse_test @{context} "(x \<up> 2 + - 1*y \<up> 2) / (x \<up> 2 + - 1*x*y)" |
68 val SOME (t', asm) = cancel_p_ thy t; |
68 val SOME (t', asm) = cancel_p_ thy t; |
69 if (UnparseC.term t', UnparseC.terms asm) = ("(x + y) / x", "[\"x \<noteq> 0\"]") |
69 if (UnparseC.term t', UnparseC.terms asm) = ("(x + y) / x", "[\"x \<noteq> 0\"]") |
70 then () else error ("cancel_p_ (t', asm) 1 changed: " ^ UnparseC.term t') |
70 then () else error ("cancel_p_ (t', asm) 1 changed: " ^ UnparseC.term t') |
71 ; |
71 ; |
72 val t = TermC.str2term "nothing + to_cancel ::real"; |
72 val t = TermC.parse_test @{context} "nothing + to_cancel ::real"; |
73 if NONE = cancel_p_ thy t then () else error "cancel_p_ doesn't report non-applicable"; |
73 if NONE = cancel_p_ thy t then () else error "cancel_p_ doesn't report non-applicable"; |
74 ; |
74 ; |
75 val t = TermC.str2term "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))"; |
75 val t = TermC.parse_test @{context} "((3 * x \<up> 2 + 6 *x + 3) / (2*x + 2))"; |
76 val SOME (t', asm) = cancel_p_ thy t; |
76 val SOME (t', asm) = cancel_p_ thy t; |
77 if UnparseC.term t' = "(3 + 3 * x) / 2" andalso UnparseC.terms asm = "[]" |
77 if UnparseC.term t' = "(3 + 3 * x) / 2" andalso UnparseC.terms asm = "[]" |
78 then () else error "cancel_p_ 1 changed"; |
78 then () else error "cancel_p_ 1 changed"; |
79 |
79 |
80 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
80 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
81 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
81 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
82 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
82 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
83 val t = TermC.str2term ("y / (a*x + b*x + c*x) " ^ |
83 val t = TermC.parse_test @{context} ("y / (a*x + b*x + c*x) " ^ |
84 (* n1 d1 *) |
84 (* n1 d1 *) |
85 "+ a / (x*y)"); |
85 "+ a / (x*y)"); |
86 (* n2 d2 *) |
86 (* n2 d2 *) |
87 val SOME (t', asm) = common_nominator_p_ thy t; |
87 val SOME (t', asm) = common_nominator_p_ thy t; |
88 if UnparseC.term t' = |
88 if UnparseC.term t' = |
93 then () else error "common_nominator_p_ term 1 changed"; |
93 then () else error "common_nominator_p_ term 1 changed"; |
94 if UnparseC.terms asm = "[\"a + b + c \<noteq> 0\", \"y \<noteq> 0\", \"x \<noteq> 0\"]" |
94 if UnparseC.terms asm = "[\"a + b + c \<noteq> 0\", \"y \<noteq> 0\", \"x \<noteq> 0\"]" |
95 then () else error "common_nominator_p_ asm 1 changed" |
95 then () else error "common_nominator_p_ asm 1 changed" |
96 |
96 |
97 "-------- example in mail Nipkow"; |
97 "-------- example in mail Nipkow"; |
98 val t = TermC.str2term "x/(x \<up> 2 + - 1*y \<up> 2) + y/(x \<up> 2 + - 1*x*y)"; |
98 val t = TermC.parse_test @{context} "x/(x \<up> 2 + - 1*y \<up> 2) + y/(x \<up> 2 + - 1*x*y)"; |
99 val SOME (t', asm) = common_nominator_p_ thy t; |
99 val SOME (t', asm) = common_nominator_p_ thy t; |
100 if UnparseC.term t' = |
100 if UnparseC.term t' = |
101 "x * x / ((x + - 1 * y) * ((x + y) * x)) +\ny * (x + y) / ((x + - 1 * y) * ((x + y) * x))" |
101 "x * x / ((x + - 1 * y) * ((x + y) * x)) +\ny * (x + y) / ((x + - 1 * y) * ((x + y) * x))" |
102 then () else error "common_nominator_p_ term 2 changed" |
102 then () else error "common_nominator_p_ term 2 changed" |
103 ; |
103 ; |
104 if UnparseC.terms asm = "[\"x + y \<noteq> 0\", \"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]" |
104 if UnparseC.terms asm = "[\"x + y \<noteq> 0\", \"x \<noteq> 0\", \"x + - 1 * y \<noteq> 0\"]" |
105 then () else error "common_nominator_p_ asm 2 changed" |
105 then () else error "common_nominator_p_ asm 2 changed" |
106 |
106 |
107 "-------- example: applicable tested by SML code"; |
107 "-------- example: applicable tested by SML code"; |
108 val t = TermC.str2term "nothing / to_add"; |
108 val t = TermC.parse_test @{context} "nothing / to_add"; |
109 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed"; |
109 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed"; |
110 ; |
110 ; |
111 val t = TermC.str2term "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))"; |
111 val t = TermC.parse_test @{context} "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))"; |
112 val SOME (t', asm) = common_nominator_p_ thy t; |
112 val SOME (t', asm) = common_nominator_p_ thy t; |
113 if UnparseC.term t' = |
113 if UnparseC.term t' = |
114 "(x + - 1) * (- 1 + x) / ((1 + x) * (- 1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (- 1 + x))" |
114 "(x + - 1) * (- 1 + x) / ((1 + x) * (- 1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (- 1 + x))" |
115 andalso UnparseC.terms asm = "[\"1 + x \<noteq> 0\", \"- 1 + x \<noteq> 0\"]" |
115 andalso UnparseC.terms asm = "[\"1 + x \<noteq> 0\", \"- 1 + x \<noteq> 0\"]" |
116 then () else error "common_nominator_p_ 3 changed"; |
116 then () else error "common_nominator_p_ 3 changed"; |
117 |
117 |
118 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
118 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
119 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
119 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
120 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
120 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
121 val t = TermC.str2term "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))"; |
121 val t = TermC.parse_test @{context} "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))"; |
122 val SOME (t', asm) = add_fraction_p_ thy t; |
122 val SOME (t', asm) = add_fraction_p_ thy t; |
123 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" |
123 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" |
124 then () else error "add_fraction_p_ 3 changed"; |
124 then () else error "add_fraction_p_ 3 changed"; |
125 ; |
125 ; |
126 if UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]" |
126 if UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]" |
127 then () else error "add_fraction_p_ 3 changed"; |
127 then () else error "add_fraction_p_ 3 changed"; |
128 ; |
128 ; |
129 val t = TermC.str2term "nothing / to_add"; |
129 val t = TermC.parse_test @{context} "nothing / to_add"; |
130 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed"; |
130 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed"; |
131 ; |
131 ; |
132 val t = TermC.str2term "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))"; |
132 val t = TermC.parse_test @{context} "((x + (- 1)) / (x + 1)) + ((x + 1) / (x + (- 1)))"; |
133 val SOME (t', asm) = add_fraction_p_ thy t; |
133 val SOME (t', asm) = add_fraction_p_ thy t; |
134 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" andalso |
134 if UnparseC.term t' = "(2 + 2 * x \<up> 2) / (- 1 + x \<up> 2)" andalso |
135 UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]" |
135 UnparseC.terms asm = "[\"- 1 + x \<up> 2 \<noteq> 0\"]" |
136 then () else error "add_fraction_p_ 3 changed"; |
136 then () else error "add_fraction_p_ 3 changed"; |
137 |
137 |
454 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
454 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
455 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
455 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
456 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
456 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
457 val thy = @{theory "Rational"}; |
457 val thy = @{theory "Rational"}; |
458 "-------- WN"; |
458 "-------- WN"; |
459 val t = TermC.str2term "(2 + -3 * x) / 9"; |
459 val t = TermC.parse_test @{context} "(2 + -3 * x) / 9"; |
460 if NONE = rewrite_set_ ctxt false cancel_p t then () |
460 if NONE = rewrite_set_ ctxt false cancel_p t then () |
461 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled"; |
461 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled"; |
462 |
462 |
463 "-------- example 186a"; |
463 "-------- example 186a"; |
464 val t = TermC.str2term "(14 * x * y) / (x * y)"; |
464 val t = TermC.parse_test @{context} "(14 * x * y) / (x * y)"; |
465 is_expanded (TermC.str2term "14 * x * y"); |
465 is_expanded (TermC.parse_test @{context} "14 * x * y"); |
466 is_expanded (TermC.str2term "x * y"); |
466 is_expanded (TermC.parse_test @{context} "x * y"); |
467 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
467 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
468 if (UnparseC.term t', UnparseC.terms asm) = ("14 / 1", "[]") |
468 if (UnparseC.term t', UnparseC.terms asm) = ("14 / 1", "[]") |
469 then () else error "rational.sml cancel Schalk 186a"; |
469 then () else error "rational.sml cancel Schalk 186a"; |
470 |
470 |
471 "-------- example 186b"; |
471 "-------- example 186b"; |
472 val t = TermC.str2term "(60 * a * b) / ( 15 * a * b )"; |
472 val t = TermC.parse_test @{context} "(60 * a * b) / ( 15 * a * b )"; |
473 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
473 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
474 if (UnparseC.term t', UnparseC.terms asm) = ("4 / 1", "[]") |
474 if (UnparseC.term t', UnparseC.terms asm) = ("4 / 1", "[]") |
475 then () else error "rational.sml cancel Schalk 186b"; |
475 then () else error "rational.sml cancel Schalk 186b"; |
476 |
476 |
477 "-------- example 186c"; |
477 "-------- example 186c"; |
478 val t = TermC.str2term "(144 * a \<up> 2 * b * c) / (12 * a * b * c)"; |
478 val t = TermC.parse_test @{context} "(144 * a \<up> 2 * b * c) / (12 * a * b * c)"; |
479 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
479 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
480 if (UnparseC.term t', UnparseC.terms asm) = ("12 * a / 1", "[]") |
480 if (UnparseC.term t', UnparseC.terms asm) = ("12 * a / 1", "[]") |
481 then () else error "rational.sml cancel Schalk 186c"; |
481 then () else error "rational.sml cancel Schalk 186c"; |
482 |
482 |
483 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! exception Div raised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
483 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! exception Div raised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
484 see --- fun rewrite_set_ downto fun gcd_poly --- |
484 see --- fun rewrite_set_ downto fun gcd_poly --- |
485 "-------- example 187a"; |
485 "-------- example 187a"; |
486 val t = TermC.str2term "(12 * x * y) / (8 * y \<up> 2 )"; |
486 val t = TermC.parse_test @{context} "(12 * x * y) / (8 * y \<up> 2 )"; |
487 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
487 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
488 if (UnparseC.term t', UnparseC.terms asm) = ("3 * x / (2 * y)", "[\"4 * y ~= 0\"]") |
488 if (UnparseC.term t', UnparseC.terms asm) = ("3 * x / (2 * y)", "[\"4 * y ~= 0\"]") |
489 then () else error "rational.sml cancel Schalk 187a"; |
489 then () else error "rational.sml cancel Schalk 187a"; |
490 *) |
490 *) |
491 |
491 |
492 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
492 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
493 see --- fun rewrite_set_ downto fun gcd_poly --- |
493 see --- fun rewrite_set_ downto fun gcd_poly --- |
494 "-------- example 187b"; |
494 "-------- example 187b"; |
495 val t = TermC.str2term "(8 * x \<up> 2 * y * z ) / (18 * x * y \<up> 2 * z )"; |
495 val t = TermC.parse_test @{context} "(8 * x \<up> 2 * y * z ) / (18 * x * y \<up> 2 * z )"; |
496 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
496 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
497 if (UnparseC.term t', UnparseC.terms asm) = ("4 * x / (9 * y)", "[\"2 * (z * (y * x)) ~= 0\"]") |
497 if (UnparseC.term t', UnparseC.terms asm) = ("4 * x / (9 * y)", "[\"2 * (z * (y * x)) ~= 0\"]") |
498 then () else error "rational.sml cancel Schalk 187b"; |
498 then () else error "rational.sml cancel Schalk 187b"; |
499 *) |
499 *) |
500 |
500 |
501 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
501 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
502 see --- fun rewrite_set_ downto fun gcd_poly --- |
502 see --- fun rewrite_set_ downto fun gcd_poly --- |
503 "-------- example 187c"; |
503 "-------- example 187c"; |
504 val t = TermC.str2term "(9 * x \<up> 5 * y \<up> 2 * z \<up> 4) / (15 * x \<up> 6 * y \<up> 3 * z )"; |
504 val t = TermC.parse_test @{context} "(9 * x \<up> 5 * y \<up> 2 * z \<up> 4) / (15 * x \<up> 6 * y \<up> 3 * z )"; |
505 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
505 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
506 if (UnparseC.term t', UnparseC.terms asm) = |
506 if (UnparseC.term t', UnparseC.terms asm) = |
507 ("3 * z \<up> 3 / (5 * (y * x))", "[\"3 * (z * (y \<up> 2 * x \<up> 5)) ~= 0\"]") |
507 ("3 * z \<up> 3 / (5 * (y * x))", "[\"3 * (z * (y \<up> 2 * x \<up> 5)) ~= 0\"]") |
508 then () else error "rational.sml cancel Schalk 187c"; |
508 then () else error "rational.sml cancel Schalk 187c"; |
509 *) |
509 *) |
510 |
510 |
511 "-------- example 188a"; |
511 "-------- example 188a"; |
512 val t = TermC.str2term "(-8 + 8 * x) / (-9 + 9 * x)"; |
512 val t = TermC.parse_test @{context} "(-8 + 8 * x) / (-9 + 9 * x)"; |
513 is_expanded (TermC.str2term "8 * x + -8"); |
513 is_expanded (TermC.parse_test @{context} "8 * x + -8"); |
514 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
514 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
515 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]") |
515 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]") |
516 then () else error "rational.sml cancel Schalk 188a"; |
516 then () else error "rational.sml cancel Schalk 188a"; |
517 |
517 |
518 val t = TermC.str2term "(8*((- 1) + x))/(9*((- 1) + x))"; |
518 val t = TermC.parse_test @{context} "(8*((- 1) + x))/(9*((- 1) + x))"; |
519 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; |
519 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; |
520 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]") |
520 if (UnparseC.term t', UnparseC.terms asm) = ("8 / 9", "[]") |
521 then () else error "rational.sml cancel Schalk make_polynomial 1"; |
521 then () else error "rational.sml cancel Schalk make_polynomial 1"; |
522 |
522 |
523 "-------- example 188b"; |
523 "-------- example 188b"; |
524 val t = TermC.str2term "(- 15 + 5 * x) / (- 18 + 6 * x)"; |
524 val t = TermC.parse_test @{context} "(- 15 + 5 * x) / (- 18 + 6 * x)"; |
525 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
525 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
526 if (UnparseC.term t', UnparseC.terms asm) = ("5 / 6", "[]") |
526 if (UnparseC.term t', UnparseC.terms asm) = ("5 / 6", "[]") |
527 then () else error "rational.sml cancel Schalk 188b"; |
527 then () else error "rational.sml cancel Schalk 188b"; |
528 |
528 |
529 "-------- example 188c"; |
529 "-------- example 188c"; |
530 val t = TermC.str2term "(a + - 1 * b) / (b + - 1 * a)"; |
530 val t = TermC.parse_test @{context} "(a + - 1 * b) / (b + - 1 * a)"; |
531 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
531 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
532 if (UnparseC.term t', UnparseC.terms asm) = ("- 1 / 1", "[]") |
532 if (UnparseC.term t', UnparseC.terms asm) = ("- 1 / 1", "[]") |
533 then () else error "rational.sml cancel Schalk 188c"; |
533 then () else error "rational.sml cancel Schalk 188c"; |
534 |
534 |
535 is_expanded (TermC.str2term "a + - 1 * b") = true; |
535 is_expanded (TermC.parse_test @{context} "a + - 1 * b") = true; |
536 val t = TermC.str2term "((- 1)*(b + (- 1) * a))/(1*(b + (- 1) * a))"; |
536 val t = TermC.parse_test @{context} "((- 1)*(b + (- 1) * a))/(1*(b + (- 1) * a))"; |
537 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
537 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
538 if (UnparseC.term t', UnparseC.terms asm) = ("(a + - 1 * b) / (- 1 * a + b)", "[]") |
538 if (UnparseC.term t', UnparseC.terms asm) = ("(a + - 1 * b) / (- 1 * a + b)", "[]") |
539 then () else error "rational.sml cancel Schalk make_polynomial 2"; |
539 then () else error "rational.sml cancel Schalk make_polynomial 2"; |
540 |
540 |
541 "-------- example 190a"; |
541 "-------- example 190a"; |
542 val t = TermC.str2term "( 27 * a \<up> 3 + 9 * a \<up> 2 + 3 * a + 1 ) / ( 27 * a \<up> 3 + 18 * a \<up> 2 + 3 * a )"; |
542 val t = TermC.parse_test @{context} "( 27 * a \<up> 3 + 9 * a \<up> 2 + 3 * a + 1 ) / ( 27 * a \<up> 3 + 18 * a \<up> 2 + 3 * a )"; |
543 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
543 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
544 if (UnparseC.term t', UnparseC.terms asm) = |
544 if (UnparseC.term t', UnparseC.terms asm) = |
545 ("(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)", "[\"3 * a + 9 * a \<up> 2 \<noteq> 0\"]") |
545 ("(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)", "[\"3 * a + 9 * a \<up> 2 \<noteq> 0\"]") |
546 then () else error "rational.sml cancel Schalk 190a"; |
546 then () else error "rational.sml cancel Schalk 190a"; |
547 |
547 |
548 "-------- example 190c"; |
548 "-------- example 190c"; |
549 val t = TermC.str2term "((1 + 9 * a \<up> 2)*(1 + 3 * a))/((3 * a + 9 * a \<up> 2)*(1 + 3 * a))"; |
549 val t = TermC.parse_test @{context} "((1 + 9 * a \<up> 2)*(1 + 3 * a))/((3 * a + 9 * a \<up> 2)*(1 + 3 * a))"; |
550 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
550 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
551 if (UnparseC.term t', UnparseC.terms asm) = |
551 if (UnparseC.term t', UnparseC.terms asm) = |
552 ("(1 + 3 * a + 9 * a \<up> 2 + 27 * a \<up> 3) /\n(3 * a + 18 * a \<up> 2 + 27 * a \<up> 3)", "[]") |
552 ("(1 + 3 * a + 9 * a \<up> 2 + 27 * a \<up> 3) /\n(3 * a + 18 * a \<up> 2 + 27 * a \<up> 3)", "[]") |
553 then () else error "rational.sml make_polynomial Schalk 190c"; |
553 then () else error "rational.sml make_polynomial Schalk 190c"; |
554 |
554 |
555 "-------- example 191a"; |
555 "-------- example 191a"; |
556 val t = TermC.str2term "( x \<up> 2 + - 1 * y \<up> 2 ) / ( x + y )"; |
556 val t = TermC.parse_test @{context} "( x \<up> 2 + - 1 * y \<up> 2 ) / ( x + y )"; |
557 is_expanded (TermC.str2term "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*) |
557 is_expanded (TermC.parse_test @{context} "x \<up> 2 + - 1 * y \<up> 2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*) |
558 is_expanded (TermC.str2term "x + y") = true; |
558 is_expanded (TermC.parse_test @{context} "x + y") = true; |
559 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
559 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
560 if (UnparseC.term t', UnparseC.terms asm) = ("(x + - 1 * y) / 1", "[]") |
560 if (UnparseC.term t', UnparseC.terms asm) = ("(x + - 1 * y) / 1", "[]") |
561 then () else error "rational.sml make_polynomial Schalk 191a"; |
561 then () else error "rational.sml make_polynomial Schalk 191a"; |
562 |
562 |
563 "-------- example 191b"; |
563 "-------- example 191b"; |
564 val t = TermC.str2term "((x + (- 1) * y)*(x + y))/((1)*(x + y))"; |
564 val t = TermC.parse_test @{context} "((x + (- 1) * y)*(x + y))/((1)*(x + y))"; |
565 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
565 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
566 if (UnparseC.term t', UnparseC.terms asm) = ("(x \<up> 2 + - 1 * y \<up> 2) / (x + y)", "[]") |
566 if (UnparseC.term t', UnparseC.terms asm) = ("(x \<up> 2 + - 1 * y \<up> 2) / (x + y)", "[]") |
567 then () else error "rational.sml make_polynomial Schalk 191b"; |
567 then () else error "rational.sml make_polynomial Schalk 191b"; |
568 |
568 |
569 "-------- example 191c"; |
569 "-------- example 191c"; |
570 val t = TermC.str2term "( 9 * x \<up> 2 + -30 * x + 25 ) / ( 9 * x \<up> 2 + - 25 )"; |
570 val t = TermC.parse_test @{context} "( 9 * x \<up> 2 + -30 * x + 25 ) / ( 9 * x \<up> 2 + - 25 )"; |
571 is_expanded (TermC.str2term "9 * x \<up> 2 + -30 * x + 25") = true; |
571 is_expanded (TermC.parse_test @{context} "9 * x \<up> 2 + -30 * x + 25") = true; |
572 is_expanded (TermC.str2term "25 + -30*x + 9*x \<up> 2") = true; |
572 is_expanded (TermC.parse_test @{context} "25 + -30*x + 9*x \<up> 2") = true; |
573 is_expanded (TermC.str2term "- 25 + 9*x \<up> 2") = true; |
573 is_expanded (TermC.parse_test @{context} "- 25 + 9*x \<up> 2") = true; |
574 |
574 |
575 val t = TermC.str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))"; |
575 val t = TermC.parse_test @{context} "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))"; |
576 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
576 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
577 if (UnparseC.term t', UnparseC.terms asm) = ("(25 + - 30 * x + 9 * x \<up> 2) / (- 25 + 9 * x \<up> 2)", "[]") |
577 if (UnparseC.term t', UnparseC.terms asm) = ("(25 + - 30 * x + 9 * x \<up> 2) / (- 25 + 9 * x \<up> 2)", "[]") |
578 then () else error "rational.sml make_polynomial Schalk 191c"; |
578 then () else error "rational.sml make_polynomial Schalk 191c"; |
579 |
579 |
580 "-------- example 192b"; |
580 "-------- example 192b"; |
581 val t = TermC.str2term "( 7 * x \<up> 3 + - 1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + - 1 * y \<up> 3 )"; |
581 val t = TermC.parse_test @{context} "( 7 * x \<up> 3 + - 1 * x \<up> 2 * y ) / ( 7 * x * y \<up> 2 + - 1 * y \<up> 3 )"; |
582 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
582 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
583 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]") |
583 if (UnparseC.term t', UnparseC.terms asm) = ("x \<up> 2 / y \<up> 2", "[\"y \<up> 2 \<noteq> 0\"]") |
584 then () else error "rational.sml cancel_p Schalk 192b"; |
584 then () else error "rational.sml cancel_p Schalk 192b"; |
585 |
585 |
586 val t = TermC.str2term "((x \<up> 2)*(7 * x + (- 1) * y))/((y \<up> 2)*(7 * x + (- 1) * y))"; |
586 val t = TermC.parse_test @{context} "((x \<up> 2)*(7 * x + (- 1) * y))/((y \<up> 2)*(7 * x + (- 1) * y))"; |
587 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
587 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
588 if (UnparseC.term t', UnparseC.terms asm) = |
588 if (UnparseC.term t', UnparseC.terms asm) = |
589 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]") |
589 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]") |
590 then () else error "rational.sml make_polynomial Schalk 192b"; |
590 then () else error "rational.sml make_polynomial Schalk 192b"; |
591 |
591 |
592 val t = TermC.str2term "((x \<up> 2)*(7 * x + (- 1) * y))/((y \<up> 2)*(7 * x + (- 1) * y))"; |
592 val t = TermC.parse_test @{context} "((x \<up> 2)*(7 * x + (- 1) * y))/((y \<up> 2)*(7 * x + (- 1) * y))"; |
593 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
593 val SOME (t', asm) = rewrite_set_ ctxt false make_polynomial t; |
594 if (UnparseC.term t', UnparseC.terms asm) = |
594 if (UnparseC.term t', UnparseC.terms asm) = |
595 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]") |
595 ("(7 * x \<up> 3 + - 1 * x \<up> 2 * y) /\n(7 * x * y \<up> 2 + - 1 * y \<up> 3)", "[]") |
596 then () else error "rational.sml make_polynomial Schalk WN050929 not working"; |
596 then () else error "rational.sml make_polynomial Schalk WN050929 not working"; |
597 |
597 |
598 "-------- example 193a"; |
598 "-------- example 193a"; |
599 val t = TermC.str2term "( x \<up> 2 + -6 * x + 9 ) / ( x \<up> 2 + -9 )"; |
599 val t = TermC.parse_test @{context} "( x \<up> 2 + -6 * x + 9 ) / ( x \<up> 2 + -9 )"; |
600 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
600 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
601 if (UnparseC.term t', UnparseC.terms asm) = ("(- 3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]") |
601 if (UnparseC.term t', UnparseC.terms asm) = ("(- 3 + x) / (3 + x)", "[\"3 + x \<noteq> 0\"]") |
602 then () else error "rational.sml cancel_p Schalk 193a"; |
602 then () else error "rational.sml cancel_p Schalk 193a"; |
603 |
603 |
604 "-------- example 193b"; |
604 "-------- example 193b"; |
605 val t = TermC.str2term "( x \<up> 2 + -8 * x + 16 ) / ( 2 * x \<up> 2 + -32 )"; |
605 val t = TermC.parse_test @{context} "( x \<up> 2 + -8 * x + 16 ) / ( 2 * x \<up> 2 + -32 )"; |
606 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
606 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
607 if (UnparseC.term t', UnparseC.terms asm) = ("(- 4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]") |
607 if (UnparseC.term t', UnparseC.terms asm) = ("(- 4 + x) / (8 + 2 * x)", "[\"8 + 2 * x \<noteq> 0\"]") |
608 then () else error "rational.sml cancel_p Schalk 193b"; |
608 then () else error "rational.sml cancel_p Schalk 193b"; |
609 |
609 |
610 "-------- example 193c"; |
610 "-------- example 193c"; |
611 val t = TermC.str2term "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + - 10 * x + 1 )"; |
611 val t = TermC.parse_test @{context} "( 2 * x + -50 * x \<up> 3 ) / ( 25 * x \<up> 2 + - 10 * x + 1 )"; |
612 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
612 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
613 if (UnparseC.term t', UnparseC.terms asm) = |
613 if (UnparseC.term t', UnparseC.terms asm) = |
614 ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]") |
614 ("(2 * x + 10 * x \<up> 2) / (1 + - 5 * x)", "[\"1 + - 5 * x \<noteq> 0\"]") |
615 then () else error "rational.sml cancel_p Schalk 193c"; |
615 then () else error "rational.sml cancel_p Schalk 193c"; |
616 |
616 |
617 (*WN: improved with new numerals*) |
617 (*WN: improved with new numerals*) |
618 val t = TermC.str2term "(- 25 + 9*x \<up> 2)/(5 + 3*x)"; |
618 val t = TermC.parse_test @{context} "(- 25 + 9*x \<up> 2)/(5 + 3*x)"; |
619 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
619 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
620 if (UnparseC.term t', UnparseC.terms asm) = ("(- 5 + 3 * x) / 1", "[]") |
620 if (UnparseC.term t', UnparseC.terms asm) = ("(- 5 + 3 * x) / 1", "[]") |
621 then () else error "rational.sml cancel WN 1"; |
621 then () else error "rational.sml cancel WN 1"; |
622 |
622 |
623 "-------- example heuberger"; |
623 "-------- example heuberger"; |
624 val t = TermC.str2term ("(x \<up> 4 + x * y + x \<up> 3 * y + y \<up> 2) / " ^ |
624 val t = TermC.parse_test @{context} ("(x \<up> 4 + x * y + x \<up> 3 * y + y \<up> 2) / " ^ |
625 "(x + 5 * x \<up> 2 + y + 5 * x * y + x \<up> 2 * y \<up> 3 + x * y \<up> 4)"); |
625 "(x + 5 * x \<up> 2 + y + 5 * x * y + x \<up> 2 * y \<up> 3 + x * y \<up> 4)"); |
626 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
626 val SOME (t', asm) = rewrite_set_ ctxt false cancel_p t; |
627 if (UnparseC.term t', UnparseC.terms asm) = |
627 if (UnparseC.term t', UnparseC.terms asm) = |
628 ("(x \<up> 3 + y) / (1 + 5 * x + x * y \<up> 3)", "[\"1 + 5 * x + x * y \<up> 3 \<noteq> 0\"]") |
628 ("(x \<up> 3 + y) / (1 + 5 * x + x * y \<up> 3)", "[\"1 + 5 * x + x * y \<up> 3 \<noteq> 0\"]") |
629 then () else error "rational.sml cancel_p heuberger"; |
629 then () else error "rational.sml cancel_p heuberger"; |
844 *) |
844 *) |
845 |
845 |
846 "-------- examples: rls norm_Rational ----------------------------------------"; |
846 "-------- examples: rls norm_Rational ----------------------------------------"; |
847 "-------- examples: rls norm_Rational ----------------------------------------"; |
847 "-------- examples: rls norm_Rational ----------------------------------------"; |
848 "-------- examples: rls norm_Rational ----------------------------------------"; |
848 "-------- examples: rls norm_Rational ----------------------------------------"; |
849 val t = TermC.str2term "Not (6*x is_atom)"; |
849 val t = TermC.parse_test @{context} "Not (6*x is_atom)"; |
850 val SOME (t',_) = rewrite_set_ ctxt false powers_erls t; UnparseC.term t'; |
850 val SOME (t',_) = rewrite_set_ ctxt false powers_erls t; UnparseC.term t'; |
851 "HOL.True"; |
851 "HOL.True"; |
852 val t = TermC.str2term "1 < 2"; |
852 val t = TermC.parse_test @{context} "1 < 2"; |
853 val SOME (t',_) = rewrite_set_ ctxt false powers_erls t; UnparseC.term t'; |
853 val SOME (t',_) = rewrite_set_ ctxt false powers_erls t; UnparseC.term t'; |
854 "HOL.True"; |
854 "HOL.True"; |
855 |
855 |
856 val t = TermC.str2term "(6*x) \<up> 2"; |
856 val t = TermC.parse_test @{context} "(6*x) \<up> 2"; |
857 val SOME (t',_) = rewrite_ ctxt Rewrite_Ord.function_empty powers_erls false @{thm realpow_def_atom} t; |
857 val SOME (t',_) = rewrite_ ctxt Rewrite_Ord.function_empty powers_erls false @{thm realpow_def_atom} t; |
858 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then () |
858 if UnparseC.term t' = "6 * x * (6 * x) \<up> (2 + - 1)" then () |
859 else error "rational.sml powers_erls (6*x) \<up> 2"; |
859 else error "rational.sml powers_erls (6*x) \<up> 2"; |
860 |
860 |
861 val t = TermC.str2term "- 1 * (- 2 * (5 / 2 * (13 * x / 2)))"; |
861 val t = TermC.parse_test @{context} "- 1 * (- 2 * (5 / 2 * (13 * x / 2)))"; |
862 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
862 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
863 if UnparseC.term t' = "65 * x / 2" then () else error "rational.sml 4"; |
863 if UnparseC.term t' = "65 * x / 2" then () else error "rational.sml 4"; |
864 |
864 |
865 val t = TermC.str2term "1 - ((13*x)/2 - 5/2) \<up> 2"; |
865 val t = TermC.parse_test @{context} "1 - ((13*x)/2 - 5/2) \<up> 2"; |
866 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
866 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
867 if UnparseC.term t' = "(- 21 + 130 * x + - 169 * x \<up> 2) / 4" then () |
867 if UnparseC.term t' = "(- 21 + 130 * x + - 169 * x \<up> 2) / 4" then () |
868 else error "rational.sml 5"; |
868 else error "rational.sml 5"; |
869 |
869 |
870 (*SRAM Schalk I, p.92 Nr. 609a*) |
870 (*SRAM Schalk I, p.92 Nr. 609a*) |
871 val t = TermC.str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54"; |
871 val t = TermC.parse_test @{context} "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54"; |
872 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
872 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
873 if UnparseC.term t' = "(- 255 + 112 * x) / 135" then () |
873 if UnparseC.term t' = "(- 255 + 112 * x) / 135" then () |
874 else error "rational.sml 6"; |
874 else error "rational.sml 6"; |
875 |
875 |
876 (*SRAM Schalk I, p.92 Nr. 610c*) |
876 (*SRAM Schalk I, p.92 Nr. 610c*) |
877 val t = TermC.str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2"; |
877 val t = TermC.parse_test @{context} "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2"; |
878 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
878 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
879 if UnparseC.term t' = "(3 + x) / - 2" then () else error "rational.sml 7"; |
879 if UnparseC.term t' = "(3 + x) / - 2" then () else error "rational.sml 7"; |
880 |
880 |
881 (*SRAM Schalk I, p.92 Nr. 476a*) |
881 (*SRAM Schalk I, p.92 Nr. 476a*) |
882 val t = TermC.str2term "(x \<up> 2/(1 - x \<up> 2) + 1)/(x/(1 - x) + 1) * (1 + x)"; |
882 val t = TermC.parse_test @{context} "(x \<up> 2/(1 - x \<up> 2) + 1)/(x/(1 - x) + 1) * (1 + x)"; |
883 (*. a/b : c/d translated to a/b * d/c .*) |
883 (*. a/b : c/d translated to a/b * d/c .*) |
884 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
884 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
885 if UnparseC.term t' = "1" then () else error "rational.sml 8"; |
885 if UnparseC.term t' = "1" then () else error "rational.sml 8"; |
886 |
886 |
887 (*Schalk I, p.92 Nr. 472a*) |
887 (*Schalk I, p.92 Nr. 472a*) |
888 val t = TermC.str2term "((8*x \<up> 2 - 32*y \<up> 2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))"; |
888 val t = TermC.parse_test @{context} "((8*x \<up> 2 - 32*y \<up> 2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))"; |
889 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
889 val SOME (t',_) = rewrite_set_ ctxt false norm_Rational t; UnparseC.term t'; |
890 if UnparseC.term t' = "x + y" then () else error "rational.sml p.92 Nr. 472a"; |
890 if UnparseC.term t' = "x + y" then () else error "rational.sml p.92 Nr. 472a"; |
891 |
891 |
892 (*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*) |
892 (*Schalk I, p.70 Nr. 480b: SEE rational.sml --- nonterminating rls norm_Rational ---*) |
893 |
893 |
894 (*WN130910 add_fractions_p exception Div raised + history: |
894 (*WN130910 add_fractions_p exception Div raised + history: |
895 ### WN.2.6.03 from rlang.sml 56a |
895 ### WN.2.6.03 from rlang.sml 56a |
896 val t = TermC.str2term "(a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)"; |
896 val t = TermC.parse_test @{context} "(a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a \<up> 2 + - 1 * b \<up> 2)"; |
897 val NONE = rewrite_set_ ctxt false add_fractions_p t; |
897 val NONE = rewrite_set_ ctxt false add_fractions_p t; |
898 |
898 |
899 THE ERROR ALREADY OCCURS IN THIS PART: |
899 THE ERROR ALREADY OCCURS IN THIS PART: |
900 val t = TermC.str2term "(a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x)"; |
900 val t = TermC.parse_test @{context} "(a + b * x) / (a + - 1 * (b * x)) + (- 1 * a + b * x) / (a + b * x)"; |
901 val NONE = add_fraction_p_ ctxt t; |
901 val NONE = add_fraction_p_ ctxt t; |
902 |
902 |
903 SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised === |
903 SEE Test_Some.thy: section {* add_fractions_p downto exception Div raised === |
904 *) |
904 *) |
905 |
905 |
906 "-------- rational numerals --------------------------------------------------"; |
906 "-------- rational numerals --------------------------------------------------"; |
907 "-------- rational numerals --------------------------------------------------"; |
907 "-------- rational numerals --------------------------------------------------"; |
908 "-------- rational numerals --------------------------------------------------"; |
908 "-------- rational numerals --------------------------------------------------"; |
909 (*SRA Schalk I, p.40 Nr. 164b *) |
909 (*SRA Schalk I, p.40 Nr. 164b *) |
910 val t = TermC.str2term "(47/6 - 76/9 + 13/4)/(35/12)"; |
910 val t = TermC.parse_test @{context} "(47/6 - 76/9 + 13/4)/(35/12)"; |
911 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
911 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
912 if UnparseC.term t = "19 / 21" then () |
912 if UnparseC.term t = "19 / 21" then () |
913 else error "rational.sml: diff.behav. in norm_Rational_mg 1"; |
913 else error "rational.sml: diff.behav. in norm_Rational_mg 1"; |
914 |
914 |
915 (*SRA Schalk I, p.40 Nr. 166a *) |
915 (*SRA Schalk I, p.40 Nr. 166a *) |
916 val t = TermC.str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)"; |
916 val t = TermC.parse_test @{context} "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)"; |
917 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
917 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
918 if UnparseC.term t = "45 / 2" then () |
918 if UnparseC.term t = "45 / 2" then () |
919 else error "rational.sml: diff.behav. in norm_Rational_mg 2"; |
919 else error "rational.sml: diff.behav. in norm_Rational_mg 2"; |
920 |
920 |
921 "-------- examples cancellation from: Mathematik 1 Schalk --------------------"; |
921 "-------- examples cancellation from: Mathematik 1 Schalk --------------------"; |
922 "-------- examples cancellation from: Mathematik 1 Schalk --------------------"; |
922 "-------- examples cancellation from: Mathematik 1 Schalk --------------------"; |
923 "-------- examples cancellation from: Mathematik 1 Schalk --------------------"; |
923 "-------- examples cancellation from: Mathematik 1 Schalk --------------------"; |
924 (* e190c Stefan K.*) |
924 (* e190c Stefan K.*) |
925 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3*a))"; |
925 val t = TermC.parse_test @{context} "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3*a))"; |
926 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
926 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
927 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)" |
927 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)" |
928 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3"; |
928 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3"; |
929 |
929 |
930 (* e192b Stefan K.*) |
930 (* e192b Stefan K.*) |
931 val t = TermC.str2term "(x \<up> 2 * (7*x + (- 1)*y)) / (y \<up> 2 * (7*x + (- 1)*y))"; |
931 val t = TermC.parse_test @{context} "(x \<up> 2 * (7*x + (- 1)*y)) / (y \<up> 2 * (7*x + (- 1)*y))"; |
932 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
932 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
933 if UnparseC.term t = "x \<up> 2 / y \<up> 2" |
933 if UnparseC.term t = "x \<up> 2 / y \<up> 2" |
934 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4"; |
934 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4"; |
935 |
935 |
936 (*SRC Schalk I, p.66 Nr. 379c *) |
936 (*SRC Schalk I, p.66 Nr. 379c *) |
937 val t = TermC.str2term "(a - b)/(b - a)"; |
937 val t = TermC.parse_test @{context} "(a - b)/(b - a)"; |
938 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
938 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
939 if UnparseC.term t = "- 1" |
939 if UnparseC.term t = "- 1" |
940 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5"; |
940 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5"; |
941 |
941 |
942 (*SRC Schalk I, p.66 Nr. 380b *) |
942 (*SRC Schalk I, p.66 Nr. 380b *) |
943 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))"; |
943 val t = TermC.parse_test @{context} "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))"; |
944 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
944 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
945 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)" |
945 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)" |
946 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6"; |
946 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6"; |
947 |
947 |
948 (* e190c Stefan K.*) |
948 (* e190c Stefan K.*) |
949 val t = TermC.str2term "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3 * a))"; |
949 val t = TermC.parse_test @{context} "((1 + 9*a \<up> 2) * (1 + 3*a)) / ((3*a + 9*a \<up> 2) * (1 + 3 * a))"; |
950 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
950 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
951 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)" |
951 if UnparseC.term t = "(1 + 9 * a \<up> 2) / (3 * a + 9 * a \<up> 2)" |
952 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3"; |
952 then () else error "rational.sml: diff.behav. in norm_Rational_mg 3"; |
953 |
953 |
954 (* e192b Stefan K.*) |
954 (* e192b Stefan K.*) |
955 val t = TermC.str2term "(x \<up> 2 * (7*x + (- 1)*y)) / (y \<up> 2 * (7*x + (- 1)*y))"; |
955 val t = TermC.parse_test @{context} "(x \<up> 2 * (7*x + (- 1)*y)) / (y \<up> 2 * (7*x + (- 1)*y))"; |
956 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
956 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
957 if UnparseC.term t = "x \<up> 2 / y \<up> 2" |
957 if UnparseC.term t = "x \<up> 2 / y \<up> 2" |
958 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4"; |
958 then () else error "rational.sml: diff.behav. in norm_Rational_mg 4"; |
959 |
959 |
960 (*SRC Schalk I, p.66 Nr. 379c *) |
960 (*SRC Schalk I, p.66 Nr. 379c *) |
961 val t = TermC.str2term "(a - b) / (b - a)"; |
961 val t = TermC.parse_test @{context} "(a - b) / (b - a)"; |
962 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
962 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
963 if UnparseC.term t = "- 1" |
963 if UnparseC.term t = "- 1" |
964 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5"; |
964 then () else error "rational.sml: diff.behav. in norm_Rational_mg 5"; |
965 |
965 |
966 (*SRC Schalk I, p.66 Nr. 380b *) |
966 (*SRC Schalk I, p.66 Nr. 380b *) |
967 val t = TermC.str2term "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))"; |
967 val t = TermC.parse_test @{context} "15*(3*x + 3) * (4*x + 9) / (12*(2*x + 7) * (5*x + 5))"; |
968 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
968 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
969 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)" |
969 if UnparseC.term t = "(27 + 12 * x) / (28 + 8 * x)" |
970 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6"; |
970 then () else error "rational.sml: diff.behav. in norm_Rational_mg 6"; |
971 |
971 |
972 (* extreme example from somewhere *) |
972 (* extreme example from somewhere *) |
973 val t = TermC.str2term |
973 val t = TermC.parse_test @{context} |
974 ("(a \<up> 4 * x + - 1*a \<up> 4 * y + 4*a \<up> 3 * b * x + -4*a \<up> 3 * b * y + " ^ |
974 ("(a \<up> 4 * x + - 1*a \<up> 4 * y + 4*a \<up> 3 * b * x + -4*a \<up> 3 * b * y + " ^ |
975 "6*a \<up> 2 * b \<up> 2 * x + -6*a \<up> 2 * b \<up> 2 * y + 4*a * b \<up> 3 * x + -4*a * b \<up> 3 * y + " ^ |
975 "6*a \<up> 2 * b \<up> 2 * x + -6*a \<up> 2 * b \<up> 2 * y + 4*a * b \<up> 3 * x + -4*a * b \<up> 3 * y + " ^ |
976 "b \<up> 4 * x + - 1*b \<up> 4 * y) " ^ |
976 "b \<up> 4 * x + - 1*b \<up> 4 * y) " ^ |
977 " / (a \<up> 2 * x \<up> 3 + -3*a \<up> 2 * x \<up> 2 * y + 3*a \<up> 2 * x * y \<up> 2 + - 1*a \<up> 2 * y \<up> 3 + " ^ |
977 " / (a \<up> 2 * x \<up> 3 + -3*a \<up> 2 * x \<up> 2 * y + 3*a \<up> 2 * x * y \<up> 2 + - 1*a \<up> 2 * y \<up> 3 + " ^ |
978 "2*a * b * x \<up> 3 + -6*a * b * x \<up> 2 * y + 6*a * b * x * y \<up> 2 + - 2*a * b * y \<up> 3 + " ^ |
978 "2*a * b * x \<up> 3 + -6*a * b * x \<up> 2 * y + 6*a * b * x * y \<up> 2 + - 2*a * b * y \<up> 3 + " ^ |
1019 |
1019 |
1020 "-------- examples common denominator from: Mathematik 1 Schalk --------------"; |
1020 "-------- examples common denominator from: Mathematik 1 Schalk --------------"; |
1021 "-------- examples common denominator from: Mathematik 1 Schalk --------------"; |
1021 "-------- examples common denominator from: Mathematik 1 Schalk --------------"; |
1022 "-------- examples common denominator from: Mathematik 1 Schalk --------------"; |
1022 "-------- examples common denominator from: Mathematik 1 Schalk --------------"; |
1023 (*SRA Schalk I, p.67 Nr. 403a *) |
1023 (*SRA Schalk I, p.67 Nr. 403a *) |
1024 val t = TermC.str2term "4/x - 3/y - 1"; |
1024 val t = TermC.parse_test @{context} "4/x - 3/y - 1"; |
1025 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1025 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1026 if UnparseC.term t = "(- 3 * x + 4 * y + - 1 * x * y) / (x * y)" |
1026 if UnparseC.term t = "(- 3 * x + 4 * y + - 1 * x * y) / (x * y)" |
1027 then () else error "rational.sml: diff.behav. in norm_Rational_mg 12"; |
1027 then () else error "rational.sml: diff.behav. in norm_Rational_mg 12"; |
1028 |
1028 |
1029 val t = TermC.str2term "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a \<up> 2+3*b*c)/(a*b*c)"; |
1029 val t = TermC.parse_test @{context} "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a \<up> 2+3*b*c)/(a*b*c)"; |
1030 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1030 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1031 if UnparseC.term t = "4 / c" |
1031 if UnparseC.term t = "4 / c" |
1032 then () else error "rational.sml: diff.behav. in norm_Rational_mg 13"; |
1032 then () else error "rational.sml: diff.behav. in norm_Rational_mg 13"; |
1033 |
1033 |
1034 (*SRA Schalk I, p.67 Nr. 410b *) |
1034 (*SRA Schalk I, p.67 Nr. 410b *) |
1035 val t = TermC.str2term "1/(x+1) + 1/(x+2) - 2/(x+3)"; |
1035 val t = TermC.parse_test @{context} "1/(x+1) + 1/(x+2) - 2/(x+3)"; |
1036 (* WN130911 non-termination due to non-termination of |
1036 (* WN130911 non-termination due to non-termination of |
1037 cancel_p_ thy (TermC.str2term "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)") |
1037 cancel_p_ thy (TermC.parse_test @{context} "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)") |
1038 |
1038 |
1039 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1039 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1040 if UnparseC.term t = "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)" |
1040 if UnparseC.term t = "(5 + 3 * x) / (6 + 11 * x + 6 * x \<up> 2 + x \<up> 3)" |
1041 then () else error "rational.sml: diff.behav. in norm_Rational_mg 14"; |
1041 then () else error "rational.sml: diff.behav. in norm_Rational_mg 14"; |
1042 *) |
1042 *) |
1043 |
1043 |
1044 (*SRA Schalk I, p.67 Nr. 413b *) |
1044 (*SRA Schalk I, p.67 Nr. 413b *) |
1045 val t = TermC.str2term "(1 + x)/(1 - x) - (1 - x)/(1 + x) + 2*x/(1 - x \<up> 2)"; |
1045 val t = TermC.parse_test @{context} "(1 + x)/(1 - x) - (1 - x)/(1 + x) + 2*x/(1 - x \<up> 2)"; |
1046 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1046 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1047 if UnparseC.term t = "6 * x / (1 + - 1 * x \<up> 2)" |
1047 if UnparseC.term t = "6 * x / (1 + - 1 * x \<up> 2)" |
1048 then () else error "rational.sml: diff.behav. in norm_Rational_mg 15"; |
1048 then () else error "rational.sml: diff.behav. in norm_Rational_mg 15"; |
1049 |
1049 |
1050 (*SRA Schalk I, p.68 Nr. 414a *) |
1050 (*SRA Schalk I, p.68 Nr. 414a *) |
1051 val t = TermC.str2term "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))"; |
1051 val t = TermC.parse_test @{context} "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))"; |
1052 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1052 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1053 if UnparseC.term t ="(- 2 + - 5 * x + 2 * x \<up> 2) / (2 + - 3 * x + x \<up> 2)" |
1053 if UnparseC.term t ="(- 2 + - 5 * x + 2 * x \<up> 2) / (2 + - 3 * x + x \<up> 2)" |
1054 then () else error "rational.sml: diff.behav. in norm_Rational_mg 16"; |
1054 then () else error "rational.sml: diff.behav. in norm_Rational_mg 16"; |
1055 |
1055 |
1056 (*SRA Schalk I, p.68 Nr. 428b *) |
1056 (*SRA Schalk I, p.68 Nr. 428b *) |
1057 val t = TermC.str2term |
1057 val t = TermC.parse_test @{context} |
1058 "1/(a - b) \<up> 2 + 1/(a + b) \<up> 2 - 2/(a \<up> 2 - b \<up> 2) - 4*(b \<up> 2 - 1)/(a \<up> 2 - b \<up> 2) \<up> 2"; |
1058 "1/(a - b) \<up> 2 + 1/(a + b) \<up> 2 - 2/(a \<up> 2 - b \<up> 2) - 4*(b \<up> 2 - 1)/(a \<up> 2 - b \<up> 2) \<up> 2"; |
1059 (* WN130911 non-termination due to non-termination of |
1059 (* WN130911 non-termination due to non-termination of |
1060 cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + - 2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)") |
1060 cancel_p_ thy (TermC.parse_test @{context} "(4 + -4 * b \<up> 2) / (a \<up> 4 + - 2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)") |
1061 |
1061 |
1062 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1062 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1063 if UnparseC.term t = "4 / (a \<up> 4 + - 2 * a \<up> 2 * b \<up> 2 + b \<up> 4)" |
1063 if UnparseC.term t = "4 / (a \<up> 4 + - 2 * a \<up> 2 * b \<up> 2 + b \<up> 4)" |
1064 then () else error "rational.sml: diff.behav. in norm_Rational_mg 18"; |
1064 then () else error "rational.sml: diff.behav. in norm_Rational_mg 18"; |
1065 *) |
1065 *) |
1066 |
1066 |
1067 (*SRA Schalk I, p.68 Nr. 430b *) |
1067 (*SRA Schalk I, p.68 Nr. 430b *) |
1068 val t = TermC.str2term |
1068 val t = TermC.parse_test @{context} |
1069 "a \<up> 2/(a - 3*b) - 108*a*b \<up> 3/((a+3*b)*(a \<up> 2 - 9*b \<up> 2)) - 9*b \<up> 2*(a - 3*b)/(a+3*b) \<up> 2"; |
1069 "a \<up> 2/(a - 3*b) - 108*a*b \<up> 3/((a+3*b)*(a \<up> 2 - 9*b \<up> 2)) - 9*b \<up> 2*(a - 3*b)/(a+3*b) \<up> 2"; |
1070 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1070 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1071 if UnparseC.term t = "a + 3 * b" |
1071 if UnparseC.term t = "a + 3 * b" |
1072 then () else error "rational.sml: diff.behav. in norm_Rational_mg 19"; |
1072 then () else error "rational.sml: diff.behav. in norm_Rational_mg 19"; |
1073 |
1073 |
1074 (*SRA Schalk I, p.68 Nr. 432 *) |
1074 (*SRA Schalk I, p.68 Nr. 432 *) |
1075 val t = TermC.str2term |
1075 val t = TermC.parse_test @{context} |
1076 ("(a \<up> 2 + a*b) / (a \<up> 2 - b \<up> 2) - (b \<up> 2 - a*b) / (b \<up> 2 - a \<up> 2) + " ^ |
1076 ("(a \<up> 2 + a*b) / (a \<up> 2 - b \<up> 2) - (b \<up> 2 - a*b) / (b \<up> 2 - a \<up> 2) + " ^ |
1077 "a \<up> 2*(a - b) / (a \<up> 3 - a \<up> 2*b) - 2*a*(a \<up> 2 - b \<up> 2) / (a \<up> 3 - a*b \<up> 2) - " ^ |
1077 "a \<up> 2*(a - b) / (a \<up> 3 - a \<up> 2*b) - 2*a*(a \<up> 2 - b \<up> 2) / (a \<up> 3 - a*b \<up> 2) - " ^ |
1078 "2*b \<up> 2 / (a \<up> 2 - b \<up> 2)"); |
1078 "2*b \<up> 2 / (a \<up> 2 - b \<up> 2)"); |
1079 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1079 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1080 if UnparseC.term t = (*"0" ..isabisac15 | Isabelle2017..*) "0 / (a \<up> 2 + - 1 * b \<up> 2)" |
1080 if UnparseC.term t = (*"0" ..isabisac15 | Isabelle2017..*) "0 / (a \<up> 2 + - 1 * b \<up> 2)" |
1081 then () else error "rational.sml: diff.behav. in norm_Rational_mg 20"; |
1081 then () else error "rational.sml: diff.behav. in norm_Rational_mg 20"; |
1082 |
1082 |
1083 (* some example *) |
1083 (* some example *) |
1084 val t = TermC.str2term "3*a / (a*b) + x/y"; |
1084 val t = TermC.parse_test @{context} "3*a / (a*b) + x/y"; |
1085 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1085 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1086 if UnparseC.term t = "(3 * y + b * x) / (b * y)" |
1086 if UnparseC.term t = "(3 * y + b * x) / (b * y)" |
1087 then () else error "rational.sml: diff.behav. in norm_Rational_mg 21"; |
1087 then () else error "rational.sml: diff.behav. in norm_Rational_mg 21"; |
1088 |
1088 |
1089 |
1089 |
1090 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------"; |
1090 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------"; |
1091 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------"; |
1091 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------"; |
1092 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------"; |
1092 "-------- examples multiply and cancel from: Mathematik 1 Schalk -------------"; |
1093 (*------- SRM Schalk I, p.68 Nr. 436a *) |
1093 (*------- SRM Schalk I, p.68 Nr. 436a *) |
1094 val t = TermC.str2term "3*(x+y) / (15*(x - y)) * 25*(x - y) \<up> 2 / (18*(x + y) \<up> 2)"; |
1094 val t = TermC.parse_test @{context} "3*(x+y) / (15*(x - y)) * 25*(x - y) \<up> 2 / (18*(x + y) \<up> 2)"; |
1095 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1095 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1096 if UnparseC.term t = "(- 5 * x + 5 * y) / (- 18 * x + - 18 * y)" |
1096 if UnparseC.term t = "(- 5 * x + 5 * y) / (- 18 * x + - 18 * y)" |
1097 then () else error "rational.sml: diff.behav. in norm_Rational_mg 22"; |
1097 then () else error "rational.sml: diff.behav. in norm_Rational_mg 22"; |
1098 |
1098 |
1099 (*------- SRM.test Schalk I, p.68 Nr. 436b *) |
1099 (*------- SRM.test Schalk I, p.68 Nr. 436b *) |
1100 val t = TermC.str2term "5*a*(a - b) \<up> 2*(a + b) \<up> 3/(7*b*(a - b) \<up> 3) * 7*b/(a + b) \<up> 3"; |
1100 val t = TermC.parse_test @{context} "5*a*(a - b) \<up> 2*(a + b) \<up> 3/(7*b*(a - b) \<up> 3) * 7*b/(a + b) \<up> 3"; |
1101 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1101 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1102 if UnparseC.term t = "5 * a / (a + - 1 * b)" |
1102 if UnparseC.term t = "5 * a / (a + - 1 * b)" |
1103 then () else error "rational.sml: diff.behav. in norm_Rational_mg 23"; |
1103 then () else error "rational.sml: diff.behav. in norm_Rational_mg 23"; |
1104 |
1104 |
1105 (*------- Schalk I, p.68 Nr. 437a *) |
1105 (*------- Schalk I, p.68 Nr. 437a *) |
1106 val t = TermC.str2term "(3*a - 4*b) / (4*c+3*e) * (3*a+4*b)/(9*a \<up> 2 - 16*b \<up> 2)"; |
1106 val t = TermC.parse_test @{context} "(3*a - 4*b) / (4*c+3*e) * (3*a+4*b)/(9*a \<up> 2 - 16*b \<up> 2)"; |
1107 (* raises an exception for unclear reasons: |
1107 (* raises an exception for unclear reasons: |
1108 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1108 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1109 : |
1109 : |
1110 ### rls: cancel_p on: (9 * a \<up> 2 + - 16 * b \<up> 2) / (4 * c + 3 * e) / |
1110 ### rls: cancel_p on: (9 * a \<up> 2 + - 16 * b \<up> 2) / (4 * c + 3 * e) / |
1111 (9 * a \<up> 2 + - 16 * b \<up> 2) |
1111 (9 * a \<up> 2 + - 16 * b \<up> 2) |
1112 exception Div raised |
1112 exception Div raised |
1113 |
1113 |
1114 BUT |
1114 BUT |
1115 val t = TermC.str2term |
1115 val t = TermC.parse_test @{context} |
1116 ("(9 * a \<up> 2 + - 16 * b \<up> 2) / (4 * c + 3 * e) /" ^ |
1116 ("(9 * a \<up> 2 + - 16 * b \<up> 2) / (4 * c + 3 * e) /" ^ |
1117 "(9 * a \<up> 2 + - 16 * b \<up> 2)"); |
1117 "(9 * a \<up> 2 + - 16 * b \<up> 2)"); |
1118 NONE = cancel_p_ thy t; |
1118 NONE = cancel_p_ thy t; |
1119 |
1119 |
1120 if UnparseC.term t = "1 / (4 * c + 3 * e)" then () |
1120 if UnparseC.term t = "1 / (4 * c + 3 * e)" then () |
1121 else error "rational.sml: diff.behav. in norm_Rational_mg 24"; |
1121 else error "rational.sml: diff.behav. in norm_Rational_mg 24"; |
1122 *) |
1122 *) |
1123 |
1123 |
1124 "----- S.K. corrected non-termination 060904"; |
1124 "----- S.K. corrected non-termination 060904"; |
1125 val t = TermC.str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a \<up> 2 - 16*b \<up> 2))"; |
1125 val t = TermC.parse_test @{context} "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a \<up> 2 - 16*b \<up> 2))"; |
1126 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; |
1126 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; |
1127 if UnparseC.term t = |
1127 if UnparseC.term t = |
1128 "(9 * a \<up> 2 + - 16 * b \<up> 2) /\n(36 * a \<up> 2 * c + 27 * a \<up> 2 * e + - 64 * b \<up> 2 * c +\n - 48 * b \<up> 2 * e)" |
1128 "(9 * a \<up> 2 + - 16 * b \<up> 2) /\n(36 * a \<up> 2 * c + 27 * a \<up> 2 * e + - 64 * b \<up> 2 * c +\n - 48 * b \<up> 2 * e)" |
1129 then () else error "rational.sml: S.K.8..corrected 060904-6"; |
1129 then () else error "rational.sml: S.K.8..corrected 060904-6"; |
1130 |
1130 |
1131 "----- S.K. corrected non-termination of cancel_p_"; |
1131 "----- S.K. corrected non-termination of cancel_p_"; |
1132 val t'' = TermC.str2term ("(9 * a \<up> 2 + - 16 * b \<up> 2) /" ^ |
1132 val t'' = TermC.parse_test @{context} ("(9 * a \<up> 2 + - 16 * b \<up> 2) /" ^ |
1133 "(36 * a \<up> 2 * c + (27 * a \<up> 2 * e + (-64 * b \<up> 2 * c + -48 * b \<up> 2 * e)))"); |
1133 "(36 * a \<up> 2 * c + (27 * a \<up> 2 * e + (-64 * b \<up> 2 * c + -48 * b \<up> 2 * e)))"); |
1134 (* /--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------\ |
1134 (* /--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------\ |
1135 val SOME (t',_) = rewrite_set_ ctxt false cancel_p t''; |
1135 val SOME (t',_) = rewrite_set_ ctxt false cancel_p t''; |
1136 if UnparseC.term t' = "1 / (4 * c + 3 * e)" |
1136 if UnparseC.term t' = "1 / (4 * c + 3 * e)" |
1137 then () else error "rational.sml: diff.behav. in cancel_p S.K.8"; |
1137 then () else error "rational.sml: diff.behav. in cancel_p S.K.8"; |
1138 \--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------/*) |
1138 \--- DOES NOT TERMINATE AT TRANSITION isabisac15 --> Isabelle2017 --------------------------/*) |
1139 |
1139 |
1140 (*------- Schalk I, p.68 Nr. 437b*) |
1140 (*------- Schalk I, p.68 Nr. 437b*) |
1141 val t = TermC.str2term "(a + b)/(x \<up> 2 - y \<up> 2) * ((x - y) \<up> 2/(a \<up> 2 - b \<up> 2))"; |
1141 val t = TermC.parse_test @{context} "(a + b)/(x \<up> 2 - y \<up> 2) * ((x - y) \<up> 2/(a \<up> 2 - b \<up> 2))"; |
1142 (*val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1142 (*val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1143 : |
1143 : |
1144 #### rls: cancel_p on: (a * x \<up> 2 + - 2 * (a * (x * y)) + a * y \<up> 2 + b * x \<up> 2 + |
1144 #### rls: cancel_p on: (a * x \<up> 2 + - 2 * (a * (x * y)) + a * y \<up> 2 + b * x \<up> 2 + |
1145 - 2 * (b * (x * y)) + |
1145 - 2 * (b * (x * y)) + |
1146 b * y \<up> 2) / |
1146 b * y \<up> 2) / |
1148 b \<up> 2 * y \<up> 2) |
1148 b \<up> 2 * y \<up> 2) |
1149 exception Div raised |
1149 exception Div raised |
1150 *) |
1150 *) |
1151 |
1151 |
1152 (*------- SRM Schalk I, p.68 Nr. 438a *) |
1152 (*------- SRM Schalk I, p.68 Nr. 438a *) |
1153 val t = TermC.str2term "x*y / (x*y - y \<up> 2) * (x \<up> 2 - x*y)"; |
1153 val t = TermC.parse_test @{context} "x*y / (x*y - y \<up> 2) * (x \<up> 2 - x*y)"; |
1154 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1154 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1155 if UnparseC.term t = "x \<up> 2" |
1155 if UnparseC.term t = "x \<up> 2" |
1156 then () else error "rational.sml: diff.behav. in norm_Rational_mg 24"; |
1156 then () else error "rational.sml: diff.behav. in norm_Rational_mg 24"; |
1157 |
1157 |
1158 (*------- SRM Schalk I, p.68 Nr. 439b *) |
1158 (*------- SRM Schalk I, p.68 Nr. 439b *) |
1159 val t = TermC.str2term "(4*x \<up> 2 + 4*x + 1) * ((x \<up> 2 - 2*x \<up> 3) / (4*x \<up> 2 + 2*x))"; |
1159 val t = TermC.parse_test @{context} "(4*x \<up> 2 + 4*x + 1) * ((x \<up> 2 - 2*x \<up> 3) / (4*x \<up> 2 + 2*x))"; |
1160 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1160 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1161 if UnparseC.term t = "(x + - 4 * x \<up> 3) / 2" |
1161 if UnparseC.term t = "(x + - 4 * x \<up> 3) / 2" |
1162 then () else error "rational.sml: diff.behav. in norm_Rational_mg 25"; |
1162 then () else error "rational.sml: diff.behav. in norm_Rational_mg 25"; |
1163 |
1163 |
1164 (*------- SRM Schalk I, p.68 Nr. 440a *) |
1164 (*------- SRM Schalk I, p.68 Nr. 440a *) |
1165 val t = TermC.str2term "(x \<up> 2 - 2*x) / (x \<up> 2 - 3*x) * (x - 3) \<up> 2 / (x \<up> 2 - 4)"; |
1165 val t = TermC.parse_test @{context} "(x \<up> 2 - 2*x) / (x \<up> 2 - 3*x) * (x - 3) \<up> 2 / (x \<up> 2 - 4)"; |
1166 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1166 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1167 if UnparseC.term t = "(- 3 + x) / (2 + x)" |
1167 if UnparseC.term t = "(- 3 + x) / (2 + x)" |
1168 then () else error "rational.sml: diff.behav. in norm_Rational_mg 26"; |
1168 then () else error "rational.sml: diff.behav. in norm_Rational_mg 26"; |
1169 |
1169 |
1170 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx"; |
1170 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx"; |
1171 val t = TermC.str2term "(a \<up> 3 - 9*a) / (a \<up> 3*b - a*b \<up> 3) * (a \<up> 2*b + a*b \<up> 2) / (a+3)"; |
1171 val t = TermC.parse_test @{context} "(a \<up> 3 - 9*a) / (a \<up> 3*b - a*b \<up> 3) * (a \<up> 2*b + a*b \<up> 2) / (a+3)"; |
1172 (* WN130911 non-termination for unclear reasons: |
1172 (* WN130911 non-termination for unclear reasons: |
1173 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1173 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1174 |
1174 |
1175 ... ENDS WITH THIS TRACE: |
1175 ... ENDS WITH THIS TRACE: |
1176 : |
1176 : |
1177 ### rls: cancel_p on: (-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + |
1177 ### rls: cancel_p on: (-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + |
1178 a \<up> 4 * b \<up> 2) / |
1178 a \<up> 4 * b \<up> 2) / |
1179 (a \<up> 3 * b + - 1 * (a * b \<up> 3)) / |
1179 (a \<up> 3 * b + - 1 * (a * b \<up> 3)) / |
1180 (3 + a) |
1180 (3 + a) |
1181 BUT THIS IS CORRECTLY RECOGNISED |
1181 BUT THIS IS CORRECTLY RECOGNISED |
1182 val t = TermC.str2term |
1182 val t = TermC.parse_test @{context} |
1183 ("(-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + a \<up> 4 * b \<up> 2) /" ^ |
1183 ("(-9 * (a \<up> 3 * b) + -9 * (a \<up> 2 * b \<up> 2) + a \<up> 5 * b + a \<up> 4 * b \<up> 2) /" ^ |
1184 "(a \<up> 3 * b + - 1 * (a * b \<up> 3)) / (3 + (a::real))"); |
1184 "(a \<up> 3 * b + - 1 * (a * b \<up> 3)) / (3 + (a::real))"); |
1185 AS |
1185 AS |
1186 NONE = cancel_p_ thy t; |
1186 NONE = cancel_p_ thy t; |
1187 |
1187 |
1188 if UnparseC.term t = "(-3 * a + a \<up> 2) / (a + - 1 * b)" then () |
1188 if UnparseC.term t = "(-3 * a + a \<up> 2) / (a + - 1 * b)" then () |
1189 else error "rational.sml: diff.behav. in norm_Rational 27"; |
1189 else error "rational.sml: diff.behav. in norm_Rational 27"; |
1190 *) |
1190 *) |
1191 |
1191 |
1192 "----- SK12 works since 0707xx"; |
1192 "----- SK12 works since 0707xx"; |
1193 val t = TermC.str2term "(a \<up> 3 - 9*a) * (a \<up> 2*b+a*b \<up> 2) / ((a \<up> 3*b - a*b \<up> 3) * (a+3))"; |
1193 val t = TermC.parse_test @{context} "(a \<up> 3 - 9*a) * (a \<up> 2*b+a*b \<up> 2) / ((a \<up> 3*b - a*b \<up> 3) * (a+3))"; |
1194 (* WN130911 non-termination due to non-termination of |
1194 (* WN130911 non-termination due to non-termination of |
1195 cancel_p_ thy (TermC.str2term "(4 + -4 * b \<up> 2) / (a \<up> 4 + - 2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)") |
1195 cancel_p_ thy (TermC.parse_test @{context} "(4 + -4 * b \<up> 2) / (a \<up> 4 + - 2 * (a \<up> 2 * b \<up> 2) + b \<up> 4)") |
1196 |
1196 |
1197 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1197 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1198 if UnparseC.term t' = "(-3 * a + a \<up> 2) / (a + - 1 * b)" then () |
1198 if UnparseC.term t' = "(-3 * a + a \<up> 2) / (a + - 1 * b)" then () |
1199 else error "rational.sml: diff.behav. in norm_Rational 28"; |
1199 else error "rational.sml: diff.behav. in norm_Rational 28"; |
1200 *) |
1200 *) |
1201 |
1201 |
1202 "-------- examples common denominator and multiplication from: Schalk --------"; |
1202 "-------- examples common denominator and multiplication from: Schalk --------"; |
1203 "-------- examples common denominator and multiplication from: Schalk --------"; |
1203 "-------- examples common denominator and multiplication from: Schalk --------"; |
1204 "-------- examples common denominator and multiplication from: Schalk --------"; |
1204 "-------- examples common denominator and multiplication from: Schalk --------"; |
1205 (*------- SRAM Schalk I, p.69 Nr. 441b *) |
1205 (*------- SRAM Schalk I, p.69 Nr. 441b *) |
1206 val t = TermC.str2term "(4*a/3 + 3*b \<up> 2/a \<up> 3 + b/(4*a))*(4*b/(3*a))"; |
1206 val t = TermC.parse_test @{context} "(4*a/3 + 3*b \<up> 2/a \<up> 3 + b/(4*a))*(4*b/(3*a))"; |
1207 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1207 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1208 if UnparseC.term t = "(36 * b \<up> 3 + 3 * a \<up> 2 * b \<up> 2 + 16 * a \<up> 4 * b) /\n(9 * a \<up> 4)" |
1208 if UnparseC.term t = "(36 * b \<up> 3 + 3 * a \<up> 2 * b \<up> 2 + 16 * a \<up> 4 * b) /\n(9 * a \<up> 4)" |
1209 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28"; |
1209 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28"; |
1210 |
1210 |
1211 (*------- SRAM Schalk I, p.69 Nr. 442b *) |
1211 (*------- SRAM Schalk I, p.69 Nr. 442b *) |
1212 val t = TermC.str2term ("(15*a \<up> 2/x \<up> 3 - 5*b \<up> 4/x \<up> 2 + 25*c \<up> 2/x) * " ^ |
1212 val t = TermC.parse_test @{context} ("(15*a \<up> 2/x \<up> 3 - 5*b \<up> 4/x \<up> 2 + 25*c \<up> 2/x) * " ^ |
1213 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + 1/c \<up> 3 * (b*x/a - 3*a/b \<up> 3)"); |
1213 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + 1/c \<up> 3 * (b*x/a - 3*a/b \<up> 3)"); |
1214 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1214 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1215 if UnparseC.term t = "5 * x \<up> 2 / (a * b \<up> 3 * c)" |
1215 if UnparseC.term t = "5 * x \<up> 2 / (a * b \<up> 3 * c)" |
1216 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29"; |
1216 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29"; |
1217 |
1217 |
1218 (*------- SRAM Schalk I, p.69 Nr. 443b *) |
1218 (*------- SRAM Schalk I, p.69 Nr. 443b *) |
1219 val t = TermC.str2term "(a/2 + b/3) * (b/3 - a/2)"; |
1219 val t = TermC.parse_test @{context} "(a/2 + b/3) * (b/3 - a/2)"; |
1220 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1220 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1221 if UnparseC.term t = "(- 9 * a \<up> 2 + 4 * b \<up> 2) / 36" |
1221 if UnparseC.term t = "(- 9 * a \<up> 2 + 4 * b \<up> 2) / 36" |
1222 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30"; |
1222 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30"; |
1223 |
1223 |
1224 (*------- SRAM Schalk I, p.69 Nr. 445b *) |
1224 (*------- SRAM Schalk I, p.69 Nr. 445b *) |
1225 val t = TermC.str2term "(a \<up> 2/9 + 2*a/(3*b) + 4/b \<up> 2)*(a/3 - 2/b) + 8/b \<up> 3"; |
1225 val t = TermC.parse_test @{context} "(a \<up> 2/9 + 2*a/(3*b) + 4/b \<up> 2)*(a/3 - 2/b) + 8/b \<up> 3"; |
1226 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1226 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1227 if UnparseC.term t = "a \<up> 3 / 27" |
1227 if UnparseC.term t = "a \<up> 3 / 27" |
1228 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31"; |
1228 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31"; |
1229 |
1229 |
1230 (*------- SRAM Schalk I, p.69 Nr. 446b *) |
1230 (*------- SRAM Schalk I, p.69 Nr. 446b *) |
1231 val t = TermC.str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x \<up> 2 - 16*y \<up> 2)"; |
1231 val t = TermC.parse_test @{context} "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x \<up> 2 - 16*y \<up> 2)"; |
1232 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1232 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1233 if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + - 20 * y \<up> 2" ..isabisac15 | Isabelle2017..*) |
1233 if UnparseC.term t = (*"30 * x \<up> 2 + -9 * x * y + - 20 * y \<up> 2" ..isabisac15 | Isabelle2017..*) |
1234 "(- 30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / - 1" |
1234 "(- 30 * x \<up> 2 + 9 * x * y + 20 * y \<up> 2) / - 1" |
1235 then () else error "rational.sml: diff.behav. in norm_Rational_mg 32"; |
1235 then () else error "rational.sml: diff.behav. in norm_Rational_mg 32"; |
1236 |
1236 |
1237 (*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*) |
1237 (*------- SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*) |
1238 val t = TermC.str2term |
1238 val t = TermC.parse_test @{context} |
1239 "(2*x \<up> 2/(3*y)+x/y \<up> 2)*(4*x \<up> 4/(9*y \<up> 2)+x \<up> 2/y \<up> 4)*(2*x \<up> 2/(3*y) - x/y \<up> 2)"; |
1239 "(2*x \<up> 2/(3*y)+x/y \<up> 2)*(4*x \<up> 4/(9*y \<up> 2)+x \<up> 2/y \<up> 4)*(2*x \<up> 2/(3*y) - x/y \<up> 2)"; |
1240 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1240 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1241 if UnparseC.term t = "(- 81 * x \<up> 4 + 16 * x \<up> 8 * y \<up> 4) / (81 * y \<up> 8)" |
1241 if UnparseC.term t = "(- 81 * x \<up> 4 + 16 * x \<up> 8 * y \<up> 4) / (81 * y \<up> 8)" |
1242 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33"; |
1242 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33"; |
1243 |
1243 |
1244 (*------- SRAM Schalk I, p.69 Nr. 450a *) |
1244 (*------- SRAM Schalk I, p.69 Nr. 450a *) |
1245 val t = TermC.str2term |
1245 val t = TermC.parse_test @{context} |
1246 "(4*x/(3*y)+2*y/(3*x)) \<up> 2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)"; |
1246 "(4*x/(3*y)+2*y/(3*x)) \<up> 2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)"; |
1247 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1247 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1248 if UnparseC.term t = "(52 * x \<up> 2 + 16 * y \<up> 2) / (9 * y \<up> 2)" |
1248 if UnparseC.term t = "(52 * x \<up> 2 + 16 * y \<up> 2) / (9 * y \<up> 2)" |
1249 then () else error "rational.sml: diff.behav. in norm_Rational_mg 34"; |
1249 then () else error "rational.sml: diff.behav. in norm_Rational_mg 34"; |
1250 |
1250 |
1251 (*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*) |
1251 (*------- SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*) |
1252 val t = TermC.str2term |
1252 val t = TermC.parse_test @{context} |
1253 ("(15*a \<up> 4/(a*x \<up> 3) - 5*a*((b \<up> 4 - 5*c \<up> 2*x) / x \<up> 2)) * " ^ |
1253 ("(15*a \<up> 4/(a*x \<up> 3) - 5*a*((b \<up> 4 - 5*c \<up> 2*x) / x \<up> 2)) * " ^ |
1254 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + a/c \<up> 3 * (x*(b/a) - 3*b*(a/b \<up> 4))"); |
1254 "(x \<up> 3/(5*a*b \<up> 3*c \<up> 3)) + a/c \<up> 3 * (x*(b/a) - 3*b*(a/b \<up> 4))"); |
1255 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1255 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1256 if UnparseC.term t = "5 * x \<up> 2 / (b \<up> 3 * c)" |
1256 if UnparseC.term t = "5 * x \<up> 2 / (b \<up> 3 * c)" |
1257 then () else error "rational.sml: diff.behav. in norm_Rational_mg 53"; |
1257 then () else error "rational.sml: diff.behav. in norm_Rational_mg 53"; |
1259 |
1259 |
1260 "-------- examples double fractions from: Mathematik 1 Schalk ----------------"; |
1260 "-------- examples double fractions from: Mathematik 1 Schalk ----------------"; |
1261 "-------- examples double fractions from: Mathematik 1 Schalk ----------------"; |
1261 "-------- examples double fractions from: Mathematik 1 Schalk ----------------"; |
1262 "-------- examples double fractions from: Mathematik 1 Schalk ----------------"; |
1262 "-------- examples double fractions from: Mathematik 1 Schalk ----------------"; |
1263 "----- SRD Schalk I, p.69 Nr. 454b"; |
1263 "----- SRD Schalk I, p.69 Nr. 454b"; |
1264 val t = TermC.str2term "((2 - x)/(2*a)) / (2*a/(x - 2))"; |
1264 val t = TermC.parse_test @{context} "((2 - x)/(2*a)) / (2*a/(x - 2))"; |
1265 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1265 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1266 if UnparseC.term t = "(- 4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)" |
1266 if UnparseC.term t = "(- 4 + 4 * x + - 1 * x \<up> 2) / (4 * a \<up> 2)" |
1267 then () else error "rational.sml: diff.behav. in norm_Rational_mg 35"; |
1267 then () else error "rational.sml: diff.behav. in norm_Rational_mg 35"; |
1268 |
1268 |
1269 "----- SRD Schalk I, p.69 Nr. 455a"; |
1269 "----- SRD Schalk I, p.69 Nr. 455a"; |
1270 val t = TermC.str2term "(a \<up> 2 + 1)/(a \<up> 2 - 1) / ((a+1)/(a - 1))"; |
1270 val t = TermC.parse_test @{context} "(a \<up> 2 + 1)/(a \<up> 2 - 1) / ((a+1)/(a - 1))"; |
1271 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1271 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1272 if UnparseC.term t = "(1 + a \<up> 2) / (1 + 2 * a + a \<up> 2)" then () |
1272 if UnparseC.term t = "(1 + a \<up> 2) / (1 + 2 * a + a \<up> 2)" then () |
1273 else error "rational.sml: diff.behav. in norm_Rational_mg 36"; |
1273 else error "rational.sml: diff.behav. in norm_Rational_mg 36"; |
1274 |
1274 |
1275 "----- Schalk I, p.69 Nr. 455b"; |
1275 "----- Schalk I, p.69 Nr. 455b"; |
1276 val t = TermC.str2term "(x \<up> 2 - 4)/(y \<up> 2 - 9)/((2+x)/(3 - y))"; |
1276 val t = TermC.parse_test @{context} "(x \<up> 2 - 4)/(y \<up> 2 - 9)/((2+x)/(3 - y))"; |
1277 (* WN130911 non-termination due to non-termination of |
1277 (* WN130911 non-termination due to non-termination of |
1278 cancel_p_ thy (TermC.str2term ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^ |
1278 cancel_p_ thy (TermC.parse_test @{context} ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^ |
1279 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)")) |
1279 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)")) |
1280 |
1280 |
1281 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1281 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1282 if UnparseC.term t = "(2 + - 1 * x) / (3 + y)" then () |
1282 if UnparseC.term t = "(2 + - 1 * x) / (3 + y)" then () |
1283 else error "rational.sml: diff.behav. in norm_Rational_mg 37"; |
1283 else error "rational.sml: diff.behav. in norm_Rational_mg 37"; |
1284 *) |
1284 *) |
1285 |
1285 |
1286 "----- SK060904- 1a non-termination of cancel_p_ ?: worked before 0707xx"; |
1286 "----- SK060904- 1a non-termination of cancel_p_ ?: worked before 0707xx"; |
1287 val t = TermC.str2term "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))"; |
1287 val t = TermC.parse_test @{context} "(x \<up> 2 - 4)*(3 - y) / ((y \<up> 2 - 9)*(2+x))"; |
1288 (* WN130911 non-termination due to non-termination of |
1288 (* WN130911 non-termination due to non-termination of |
1289 cancel_p_ thy (TermC.str2term ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^ |
1289 cancel_p_ thy (TermC.parse_test @{context} ("(- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)) /" ^ |
1290 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)")) |
1290 "(- 18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)")) |
1291 |
1291 |
1292 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1292 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1293 if UnparseC.term t = "(2 + - 1 * x) / (3 + y)" then () |
1293 if UnparseC.term t = "(2 + - 1 * x) / (3 + y)" then () |
1294 else error "rational.sml: diff.behav. in norm_Rational_mg 37b"; |
1294 else error "rational.sml: diff.behav. in norm_Rational_mg 37b"; |
1295 *) |
1295 *) |
1296 |
1296 |
1297 "----- ?: worked before 0707xx"; |
1297 "----- ?: worked before 0707xx"; |
1298 val t = TermC.str2term "(3 + - 1 * y) / (-9 + y \<up> 2)"; |
1298 val t = TermC.parse_test @{context} "(3 + - 1 * y) / (-9 + y \<up> 2)"; |
1299 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1299 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1300 if UnparseC.term t = "- 1 / (3 + y)" |
1300 if UnparseC.term t = "- 1 / (3 + y)" |
1301 then () else error "rational.sml: - 1 / (3 + y) norm_Rational"; |
1301 then () else error "rational.sml: - 1 / (3 + y) norm_Rational"; |
1302 |
1302 |
1303 "----- SRD Schalk I, p.69 Nr. 456b"; |
1303 "----- SRD Schalk I, p.69 Nr. 456b"; |
1304 val t = TermC.str2term "(b \<up> 3 - b \<up> 2) / (b \<up> 2+b) / (b \<up> 2 - 1)"; |
1304 val t = TermC.parse_test @{context} "(b \<up> 3 - b \<up> 2) / (b \<up> 2+b) / (b \<up> 2 - 1)"; |
1305 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1305 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1306 if UnparseC.term t = "b / (1 + 2 * b + b \<up> 2)" |
1306 if UnparseC.term t = "b / (1 + 2 * b + b \<up> 2)" |
1307 then () else error "rational.sml: diff.behav. in norm_Rational_mg 38"; |
1307 then () else error "rational.sml: diff.behav. in norm_Rational_mg 38"; |
1308 |
1308 |
1309 "----- SRD Schalk I, p.69 Nr. 457b"; |
1309 "----- SRD Schalk I, p.69 Nr. 457b"; |
1310 val t = TermC.str2term "(16*a \<up> 2 - 9*b \<up> 2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a \<up> 2 - 9*a \<up> 2*b \<up> 2))"; |
1310 val t = TermC.parse_test @{context} "(16*a \<up> 2 - 9*b \<up> 2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a \<up> 2 - 9*a \<up> 2*b \<up> 2))"; |
1311 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1311 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1312 if UnparseC.term t = "8 * a \<up> 2 + - 6 * a * b + - 12 * a \<up> 2 * b + 9 * a * b \<up> 2" |
1312 if UnparseC.term t = "8 * a \<up> 2 + - 6 * a * b + - 12 * a \<up> 2 * b + 9 * a * b \<up> 2" |
1313 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39"; |
1313 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39"; |
1314 |
1314 |
1315 "----- Schalk I, p.69 Nr. 458b works since 0707"; |
1315 "----- Schalk I, p.69 Nr. 458b works since 0707"; |
1316 val t = TermC.str2term "(2*a \<up> 2*x - a \<up> 2) / (a*x - b*x) / (b \<up> 2*(2*x - 1) / (x*(a - b)))"; |
1316 val t = TermC.parse_test @{context} "(2*a \<up> 2*x - a \<up> 2) / (a*x - b*x) / (b \<up> 2*(2*x - 1) / (x*(a - b)))"; |
1317 (*val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1317 (*val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1318 : |
1318 : |
1319 ### rls: cancel_p on: (- 1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + - 1 * (b * x)) / |
1319 ### rls: cancel_p on: (- 1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + - 1 * (b * x)) / |
1320 ((- 1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + - 1 * (b * x))) |
1320 ((- 1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + - 1 * (b * x))) |
1321 exception Div raised |
1321 exception Div raised |
1322 |
1322 |
1323 BUT |
1323 BUT |
1324 val t = TermC.str2term |
1324 val t = TermC.parse_test @{context} |
1325 ("(- 1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + - 1 * (b * x)) /" ^ |
1325 ("(- 1 * a \<up> 2 + 2 * (a \<up> 2 * x)) / (a * x + - 1 * (b * x)) /" ^ |
1326 "((- 1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + - 1 * (b * x)))"); |
1326 "((- 1 * b \<up> 2 + 2 * (b \<up> 2 * x)) / (a * x + - 1 * (b * x)))"); |
1327 NONE = cancel_p_ thy t; |
1327 NONE = cancel_p_ thy t; |
1328 |
1328 |
1329 if UnparseC.term t = "a \<up> 2 / b \<up> 2" then () |
1329 if UnparseC.term t = "a \<up> 2 / b \<up> 2" then () |
1330 else error "rational.sml: diff.behav. in norm_Rational_mg 39b"; |
1330 else error "rational.sml: diff.behav. in norm_Rational_mg 39b"; |
1331 *) |
1331 *) |
1332 |
1332 |
1333 "----- SRD Schalk I, p.69 Nr. 459b"; |
1333 "----- SRD Schalk I, p.69 Nr. 459b"; |
1334 val t = TermC.str2term "(a \<up> 2 - b \<up> 2)/(a*b) / (4*(a+b) \<up> 2/a)"; |
1334 val t = TermC.parse_test @{context} "(a \<up> 2 - b \<up> 2)/(a*b) / (4*(a+b) \<up> 2/a)"; |
1335 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1335 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1336 if UnparseC.term t = "(a + - 1 * b) / (4 * a * b + 4 * b \<up> 2)" then () |
1336 if UnparseC.term t = "(a + - 1 * b) / (4 * a * b + 4 * b \<up> 2)" then () |
1337 else error "rational.sml: diff.behav. in norm_Rational_mg 41"; |
1337 else error "rational.sml: diff.behav. in norm_Rational_mg 41"; |
1338 |
1338 |
1339 "----- Schalk I, p.69 Nr. 460b nonterm.SK"; |
1339 "----- Schalk I, p.69 Nr. 460b nonterm.SK"; |
1340 val t = TermC.str2term "(9*(x \<up> 2 - 8*x + 16) / (4*(y \<up> 2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))"; |
1340 val t = TermC.parse_test @{context} "(9*(x \<up> 2 - 8*x + 16) / (4*(y \<up> 2 - 2*y + 1))) / ((3*x - 12) / (16*y - 16))"; |
1341 (*val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1341 (*val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1342 exception Div raised |
1342 exception Div raised |
1343 |
1343 |
1344 BUT |
1344 BUT |
1345 val t = TermC.str2term |
1345 val t = TermC.parse_test @{context} |
1346 ("(144 + -72 * x + 9 * x \<up> 2) / (4 + -8 * y + 4 * y \<up> 2) /" ^ |
1346 ("(144 + -72 * x + 9 * x \<up> 2) / (4 + -8 * y + 4 * y \<up> 2) /" ^ |
1347 "((- 12 + 3 * x) / (- 16 + 16 * y))"); |
1347 "((- 12 + 3 * x) / (- 16 + 16 * y))"); |
1348 NONE = cancel_p_ thy t; |
1348 NONE = cancel_p_ thy t; |
1349 |
1349 |
1350 if UnparseC.term t = !!!!!!!!!!!!!!!!!!!!!!!!! |
1350 if UnparseC.term t = !!!!!!!!!!!!!!!!!!!!!!!!! |
1351 then () else error "rational.sml: diff.behav. in norm_Rational_mg 42"; |
1351 then () else error "rational.sml: diff.behav. in norm_Rational_mg 42"; |
1352 *) |
1352 *) |
1353 |
1353 |
1354 "----- some variant of the above; was non-terminating before"; |
1354 "----- some variant of the above; was non-terminating before"; |
1355 val t = TermC.str2term "9*(x \<up> 2 - 8*x+16)*(16*y - 16)/(4*(y \<up> 2 - 2*y+1)*(3*x - 12))"; |
1355 val t = TermC.parse_test @{context} "9*(x \<up> 2 - 8*x+16)*(16*y - 16)/(4*(y \<up> 2 - 2*y+1)*(3*x - 12))"; |
1356 val SOME (t , _) = rewrite_set_ ctxt false norm_Rational t; |
1356 val SOME (t , _) = rewrite_set_ ctxt false norm_Rational t; |
1357 if UnparseC.term t = "(48 + - 12 * x) / (1 + - 1 * y)" |
1357 if UnparseC.term t = "(48 + - 12 * x) / (1 + - 1 * y)" |
1358 then () else error "some variant of the above; was non-terminating before"; |
1358 then () else error "some variant of the above; was non-terminating before"; |
1359 |
1359 |
1360 "----- SRD Schalk I, p.70 Nr. 472a"; |
1360 "----- SRD Schalk I, p.70 Nr. 472a"; |
1361 val t = TermC.str2term ("((8*x \<up> 2 - 32*y \<up> 2) / (2*x + 4*y)) / ((4*x - 8*y) / (x + y))"); |
1361 val t = TermC.parse_test @{context} ("((8*x \<up> 2 - 32*y \<up> 2) / (2*x + 4*y)) / ((4*x - 8*y) / (x + y))"); |
1362 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1362 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1363 if UnparseC.term t = "x + y" |
1363 if UnparseC.term t = "x + y" |
1364 then () else error "rational.sml: diff.behav. in norm_Rational_mg 43"; |
1364 then () else error "rational.sml: diff.behav. in norm_Rational_mg 43"; |
1365 |
1365 |
1366 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec"; |
1366 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec"; |
1367 val t = TermC.str2term ("(a - (a*b + b \<up> 2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^ |
1367 val t = TermC.parse_test @{context} ("(a - (a*b + b \<up> 2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^ |
1368 "((a - a \<up> 2/(a+b))/(a+(a*b)/(a - b)))"); |
1368 "((a - a \<up> 2/(a+b))/(a+(a*b)/(a - b)))"); |
1369 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1369 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1370 if UnparseC.term t = "(2 * a \<up> 3 + 2 * a \<up> 2 * b) / (a \<up> 2 * b + b \<up> 3)" |
1370 if UnparseC.term t = "(2 * a \<up> 3 + 2 * a \<up> 2 * b) / (a \<up> 2 * b + b \<up> 3)" |
1371 then () else error "rational.sml: diff.behav. in norm_Rational_mg 51"; |
1371 then () else error "rational.sml: diff.behav. in norm_Rational_mg 51"; |
1372 |
1372 |
1373 (*SRD Schalk I, p.69 Nr. 461a *) |
1373 (*SRD Schalk I, p.69 Nr. 461a *) |
1374 val t = TermC.str2term "(2/(x+3) + 2/(x - 3)) / (8*x/(x \<up> 2 - 9))"; |
1374 val t = TermC.parse_test @{context} "(2/(x+3) + 2/(x - 3)) / (8*x/(x \<up> 2 - 9))"; |
1375 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1375 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1376 if UnparseC.term t = "1 / 2" |
1376 if UnparseC.term t = "1 / 2" |
1377 then () else error "rational.sml: diff.behav. in norm_Rational_mg 44"; |
1377 then () else error "rational.sml: diff.behav. in norm_Rational_mg 44"; |
1378 |
1378 |
1379 (*SRD Schalk I, p.69 Nr. 464b *) |
1379 (*SRD Schalk I, p.69 Nr. 464b *) |
1380 val t = TermC.str2term "(a - a/(a - 2)) / (a + a/(a - 2))"; |
1380 val t = TermC.parse_test @{context} "(a - a/(a - 2)) / (a + a/(a - 2))"; |
1381 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1381 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1382 if UnparseC.term t = "(- 3 + a) / (- 1 + a)" |
1382 if UnparseC.term t = "(- 3 + a) / (- 1 + a)" |
1383 then () else error "rational.sml: diff.behav. in norm_Rational_mg 45"; |
1383 then () else error "rational.sml: diff.behav. in norm_Rational_mg 45"; |
1384 |
1384 |
1385 (*SRD Schalk I, p.69 Nr. 465b *) |
1385 (*SRD Schalk I, p.69 Nr. 465b *) |
1386 val t = TermC.str2term "((x+3*y)/9 + (4*y \<up> 2 - 9*z \<up> 2)/(16*x)) / (x/9 + y/6 + z/4)"; |
1386 val t = TermC.parse_test @{context} "((x+3*y)/9 + (4*y \<up> 2 - 9*z \<up> 2)/(16*x)) / (x/9 + y/6 + z/4)"; |
1387 (* WN130911 non-termination due to non-termination of |
1387 (* WN130911 non-termination due to non-termination of |
1388 cancel_p_ thy (TermC.str2term |
1388 cancel_p_ thy (TermC.parse_test @{context} |
1389 ("("(576 * x \<up> 2 + 1728 * (x * y) + 1296 * y \<up> 2 + - 2916 * z \<up> 2) /" ^ |
1389 ("("(576 * x \<up> 2 + 1728 * (x * y) + 1296 * y \<up> 2 + - 2916 * z \<up> 2) /" ^ |
1390 "(576 * x \<up> 2 + 864 * (x * y) + 1296 * (x * z))")) |
1390 "(576 * x \<up> 2 + 864 * (x * y) + 1296 * (x * z))")) |
1391 |
1391 |
1392 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1392 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1393 if UnparseC.term t = "(4 * x + 6 * y + -9 * z) / (4 * x)" |
1393 if UnparseC.term t = "(4 * x + 6 * y + -9 * z) / (4 * x)" |
1394 then () else error "rational.sml: diff.behav. in norm_Rational_mg 46"; |
1394 then () else error "rational.sml: diff.behav. in norm_Rational_mg 46"; |
1395 *) |
1395 *) |
1396 |
1396 |
1397 (*SRD Schalk I, p.69 Nr. 466b *) |
1397 (*SRD Schalk I, p.69 Nr. 466b *) |
1398 val t = TermC.str2term "((1 - 7*(x - 2)/(x \<up> 2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x \<up> 2 - 25))"; |
1398 val t = TermC.parse_test @{context} "((1 - 7*(x - 2)/(x \<up> 2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x \<up> 2 - 25))"; |
1399 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1399 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1400 if UnparseC.term t = "(25 + - 10 * x + x \<up> 2) / 18" |
1400 if UnparseC.term t = "(25 + - 10 * x + x \<up> 2) / 18" |
1401 then () else error "rational.sml: diff.behav. in norm_Rational_mg 47"; |
1401 then () else error "rational.sml: diff.behav. in norm_Rational_mg 47"; |
1402 |
1402 |
1403 (*SRD Schalk I, p.70 Nr. 469 *) |
1403 (*SRD Schalk I, p.70 Nr. 469 *) |
1404 val t = TermC.str2term ("3*b \<up> 2 / (4*a \<up> 2 - 8*a*b + 4*b \<up> 2) / " ^ |
1404 val t = TermC.parse_test @{context} ("3*b \<up> 2 / (4*a \<up> 2 - 8*a*b + 4*b \<up> 2) / " ^ |
1405 "(a / (a \<up> 2*b - b \<up> 3) + (a - b) / (4*a*b \<up> 2 + 4*b \<up> 3) - 1 / (4*b \<up> 2))"); |
1405 "(a / (a \<up> 2*b - b \<up> 3) + (a - b) / (4*a*b \<up> 2 + 4*b \<up> 3) - 1 / (4*b \<up> 2))"); |
1406 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1406 val SOME (t, _) = rewrite_set_ ctxt false norm_Rational t; |
1407 if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)" |
1407 if UnparseC.term t = "- 3 * b \<up> 3 / (- 2 * a + 2 * b)" |
1408 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48"; |
1408 then () else error "rational.sml: diff.behav. in norm_Rational_mg 48"; |
1409 |
1409 |