1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/rational-1.sml Fri Jul 16 06:57:34 2021 +0200
1.3 @@ -0,0 +1,151 @@
1.4 +(* Title: test/Tools/isac/Knowledge/rational-1.sml
1.5 + Author: Walther Neuper
1.6 + Use is subject to license terms.
1.7 +
1.8 +Test of basic functions and application to complex examples.
1.9 +*)
1.10 +
1.11 +"-----------------------------------------------------------------------------------------------";
1.12 +"-----------------------------------------------------------------------------------------------";
1.13 +"table of contents -----------------------------------------------------------------------------";
1.14 +"-----------------------------------------------------------------------------------------------";
1.15 +"-------- fun poly_of_term ---------------------------------------------------------------------";
1.16 +"-------- fun is_poly --------------------------------------------------------------------------";
1.17 +"-------- fun term_of_poly ---------------------------------------------------------------------";
1.18 +"-------- complex examples: rls norm_Rational --------------------------------------------------";
1.19 +"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
1.20 +"-----------------------------------------------------------------------------------------------";
1.21 +"-----------------------------------------------------------------------------------------------";
1.22 +
1.23 +
1.24 +"-------- fun poly_of_term ---------------------------------------------------------------------";
1.25 +"-------- fun poly_of_term ---------------------------------------------------------------------";
1.26 +"-------- fun poly_of_term ---------------------------------------------------------------------";
1.27 +val thy = @{theory Partial_Fractions};
1.28 +val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
1.29 +
1.30 +val t = TermC.str2term "-3 + -2 * x ::real";
1.31 +if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
1.32 +then () else error "poly_of_term uminus changed";
1.33 +
1.34 +if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
1.35 +then () else error "poly_of_term 1 changed";
1.36 +
1.37 +if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])]
1.38 +then () else error "poly_of_term 2 changed";
1.39 +
1.40 +if poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
1.41 +then () else error "poly_of_term 3 changed";
1.42 +"~~~~~ fun poly_of_term , args:"; val (vs, t) =
1.43 + (vs, (TermC.str2term "12 * x \<up> 3"));
1.44 +
1.45 + monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
1.46 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Groups.times_class.times", _) $ m1 $ m2)) =
1.47 + (vs, (1, replicate (length vs) 0), t);
1.48 + val (c', es') =
1.49 +
1.50 + monom_of_term vs (c, es) m1;
1.51 +"~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Transcendental.powr", _) $ (t as Free _) $ (Const ("Num.numeral_class.numeral", _) $ num)) ) =
1.52 + (vs, (c', es'), m2);
1.53 +(*+*)c = 12;
1.54 +(*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
1.55 +
1.56 +if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
1.57 +then () else error "monom_of_term (powr): return value CHANGED";
1.58 +
1.59 +if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
1.60 +then () else error "poly_of_term 4 changed";
1.61 +
1.62 +if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
1.63 + SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
1.64 +then () else error "poly_of_term 5 changed";
1.65 +
1.66 +(*poly_of_term is quite liberal:*)
1.67 +(*the coefficient may be somewhere, the order of variables and the parentheses
1.68 + within a monomial are arbitrary*)
1.69 +if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
1.70 +then () else error "poly_of_term 6 changed";
1.71 +
1.72 +(*there may even be more than 1 coefficient:*)
1.73 +if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
1.74 +then () else error "poly_of_term 7 changed";
1.75 +
1.76 +(*the order and the parentheses within monomials are arbitrary:*)
1.77 +if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
1.78 + = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
1.79 +then () else error "poly_of_term 8 changed";
1.80 +
1.81 +(*from --- rls norm_Rational downto fun gcd_poly ---*)
1.82 +val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
1.83 + ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
1.84 + "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
1.85 +"~~~~~ fun cancel_p_, args:"; val (t) = (t);
1.86 +val opt = check_fraction t;
1.87 +val SOME (numerator, denominator) = opt;
1.88 +(*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);
1.89 +(*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2"; (*isa -- isa2*);
1.90 + val vs = TermC.vars_of t;
1.91 +(*+*)UnparseC.terms vs = "[\"x\", \"y\"]";
1.92 + val baseT = type_of numerator
1.93 + val expT = HOLogic.realT;
1.94 +val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
1.95 +
1.96 +"-------- fun is_poly --------------------------------------------------------------------------";
1.97 +"-------- fun is_poly --------------------------------------------------------------------------";
1.98 +"-------- fun is_poly --------------------------------------------------------------------------";
1.99 +if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
1.100 +then () else error "is_poly 1 changed";
1.101 +if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
1.102 +then () else error "is_poly 2 changed";
1.103 +
1.104 +"-------- fun term_of_poly ---------------------------------------------------------------------";
1.105 +"-------- fun term_of_poly ---------------------------------------------------------------------";
1.106 +"-------- fun term_of_poly ---------------------------------------------------------------------";
1.107 +val expT = HOLogic.realT
1.108 +val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
1.109 +val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
1.110 +val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
1.111 +(*precondition for [(c, es),...]: legth es = length vs*)
1.112 +;
1.113 +if UnparseC.term (term_of_poly baseT expT vs p) = "1 + 7 * y \<up> 8 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 5"
1.114 +then () else error "term_of_poly 1 changed";
1.115 +
1.116 +"-------- complex examples: rls norm_Rational --------------------------------------------------";
1.117 +"-------- complex examples: rls norm_Rational --------------------------------------------------";
1.118 +"-------- complex examples: rls norm_Rational --------------------------------------------------";
1.119 +val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.120 +val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1.121 +if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
1.122 +
1.123 +val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.124 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1.125 +if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
1.126 +else error "rational.sml 2";
1.127 +
1.128 +val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
1.129 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
1.130 +if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
1.131 +else error "rational.sml 3";
1.132 +
1.133 +"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
1.134 +"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
1.135 +"-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
1.136 +(*Schalk I, p.60 Nr. 215c *)
1.137 +val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1.138 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.139 +if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1.140 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
1.141 +
1.142 +(*SRC Schalk I, p.66 Nr. 381b *)
1.143 +val t = TermC.str2term
1.144 +"(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
1.145 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.146 +if UnparseC.term t = "1 / (- 5 + 2 * x)"
1.147 +then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
1.148 +
1.149 +(*Schalk I, p.60 Nr. 215c *)
1.150 +val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
1.151 +val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
1.152 +if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
1.153 +then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";
1.154 +