1.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Aug 26 16:32:21 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Wed Aug 28 10:40:53 2013 +0200
1.3 @@ -22,6 +22,7 @@
1.4 "-------- fun is_poly --------------------------------------------------------";
1.5 "-------- fun term_of_poly ---------------------------------------------------";
1.6 "-------- fun factout_p_ -----------------------------------------------------";
1.7 +"-------- fun cancel_p_ ------------------------------------------------------";
1.8 "-------- fun common_nominator_p_ --------------------------------------------";
1.9 "-------- fun add_fraction_p_ ------------------------------------------------";
1.10 "-------- TODO ---------------------------------------------------------------";
1.11 @@ -114,13 +115,33 @@
1.12 if term2str t' = "(x + y) * (x + -1 * y) / (x * (x + -1 * y))"
1.13 then () else error ("factout_p_ term 1 changed: " ^ term2str t')
1.14 ;
1.15 -(*========== inhibit exn WN130822 asm different by Rational.thy | Rational2.thy ================
1.16 -if terms2str asm = "[\"x\",\"x + -1 * y\"]"
1.17 +if terms2str asm = "[\"x ~= 0\",\"x + -1 * y ~= 0\"]"
1.18 then () else error "factout_p_ asm 1 changed"
1.19 -============ inhibit exn WN130822 asm different by Rational.thy | Rational2.thy ===============*)
1.20 ;
1.21 val t = str2term "nothing + to_cancel ::real";
1.22 if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable";
1.23 +;
1.24 +val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.25 +val SOME (t', asm) = factout_p_ thy t;
1.26 +if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso
1.27 + terms2str asm = "[\"2 ~= 0\",\"1 + x ~= 0\"]"
1.28 +then () else error "factout_p_ 1 changed";
1.29 +
1.30 +"-------- fun cancel_p_ ------------------------------------------------------";
1.31 +"-------- fun cancel_p_ ------------------------------------------------------";
1.32 +"-------- fun cancel_p_ ------------------------------------------------------";
1.33 +val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
1.34 +val SOME (t', asm) = cancel_p_ thy t;
1.35 +if (term2str t', terms2str asm) = ("(x + y) / x", "[\"x ~= 0\",\"x + -1 * y ~= 0\"]")
1.36 +then () else error ("cancel_p_ (t', asm) 1 changed: " ^ term2str t')
1.37 +;
1.38 +val t = str2term "nothing + to_cancel ::real";
1.39 +if NONE = cancel_p_ thy t then () else error "cancel_p_ doesn't report non-applicable";
1.40 +;
1.41 +val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.42 +val SOME (t', asm) = cancel_p_ thy t;
1.43 +if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"2 ~= 0\",\"1 + x ~= 0\"]"
1.44 +then () else error "cancel_p_ 1 changed";
1.45
1.46 "-------- fun common_nominator_p_ --------------------------------------------";
1.47 "-------- fun common_nominator_p_ --------------------------------------------";
1.48 @@ -136,10 +157,8 @@
1.49 "+ a * (a + b + c) / (x * ((a + b + c) * y))")
1.50 (* n2 * d1' / (c'* ( d1' *d2')) *)
1.51 then () else error "common_nominator_p_ term 1 changed";
1.52 -(*========== inhibit exn WN130823 asm different Rational<-->2.thy ==============================
1.53 -if terms2str asm = "[\"a + b + c\",\"y\",\"x\"]"
1.54 +if terms2str asm = "[\"a + b + c ~= 0\",\"y ~= 0\",\"x ~= 0\"]"
1.55 then () else error "common_nominator_p_ asm 1 changed"
1.56 -============ inhibit exn WN130823 asm different Rational<-->2.thy =============================*)
1.57
1.58 "-------- example in mail Nipkow";
1.59 val t = str2term "x/(x^^^2 + -1*y^^^2) + y/(x^^^2 + -1*x*y)";
1.60 @@ -151,14 +170,19 @@
1.61 "((x + -1 * y) * ((x + y) * x))"
1.62 then () else error "common_nominator_p_ term 2 changed"
1.63 ;
1.64 -(*========== inhibit exn WN130823 asm different Rational<-->2.thy ==============================
1.65 -if terms2str asm = "[\"x + y\",\"x\",\"x + ~1 * y\"]"
1.66 +if terms2str asm = "[\"x + y ~= 0\",\"x ~= 0\",\"x + -1 * y ~= 0\"]"
1.67 then () else error "common_nominator_p_ asm 2 changed"
1.68 -============ inhibit exn WN130823 asm different Rational<-->2.thy =============================*)
1.69
1.70 "-------- example: applicable tested by SML code";
1.71 val t = str2term "nothing / to_add";
1.72 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed";
1.73 +;
1.74 +val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.75 +val SOME (t', asm) = common_nominator_p_ thy t;
1.76 +if term2str t' =
1.77 + "(x + -1) * (-1 + x) / (1 * ((1 + x) * (-1 + x))) +\n(x + 1) * (1 + x) / (1 * ((1 + x) * (-1 + x)))"
1.78 + andalso terms2str asm = "[\"1 + x ~= 0\",\"-1 + x ~= 0\",\"1 ~= 0\"]"
1.79 +then () else error "common_nominator_p_ 3 changed";
1.80
1.81 "-------- fun add_fraction_p_ ------------------------------------------------";
1.82 "-------- fun add_fraction_p_ ------------------------------------------------";
1.83 @@ -167,10 +191,18 @@
1.84 val SOME (t', asm) = add_fraction_p_ thy t;
1.85 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)"
1.86 then () else error "add_fraction_p_ 3 changed";
1.87 -(*========== inhibit exn WN130823 asm different Rational<-->2.thy ==============================
1.88 -if terms2str asm = "[\"-1 + x ^^^ 2\"]"
1.89 +;
1.90 +if terms2str asm = "[\"-1 + x ^^^ 2 ~= 0\"]"
1.91 then () else error "add_fraction_p_ 3 changed";
1.92 -============ inhibit exn WN130823 asm different Rational<-->2.thy =============================*)
1.93 +;
1.94 +val t = str2term "nothing / to_add";
1.95 +if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed";
1.96 +;
1.97 +val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.98 +val SOME (t', asm) = add_fraction_p_ thy t;
1.99 +if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso
1.100 + terms2str asm = "[\"-1 + x ^^^ 2 ~= 0\"]"
1.101 +then () else error "add_fraction_p_ 3 changed";
1.102
1.103 "-------- TODO ---------------------------------------------------------------";
1.104 "-------- TODO ---------------------------------------------------------------";