1 (* Title: test/Tools/isac/Knowledge/rational-1.sml
3 Use is subject to license terms.
5 Test of basic functions and application to complex examples.
8 "-----------------------------------------------------------------------------------------------";
9 "-----------------------------------------------------------------------------------------------";
10 "table of contents -----------------------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "-------- fun poly_of_term ---------------------------------------------------------------------";
13 "-------- fun is_poly --------------------------------------------------------------------------";
14 "-------- fun term_of_poly ---------------------------------------------------------------------";
15 "-------- complex examples: rls norm_Rational --------------------------------------------------";
16 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
17 "-----------------------------------------------------------------------------------------------";
18 "-----------------------------------------------------------------------------------------------";
21 "-------- fun poly_of_term ---------------------------------------------------------------------";
22 "-------- fun poly_of_term ---------------------------------------------------------------------";
23 "-------- fun poly_of_term ---------------------------------------------------------------------";
24 val thy = @{theory Partial_Fractions};
25 val vs = TermC.vars_of (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6");
27 val t = TermC.str2term "-3 + -2 * x ::real";
28 if poly_of_term vs t = SOME [(~3, [0, 0, 0]), (~2, [1, 0, 0])]
29 then () else error "poly_of_term uminus changed";
31 if poly_of_term vs (TermC.str2term "12::real") = SOME [(12, [0, 0, 0])]
32 then () else error "poly_of_term 1 changed";
34 if poly_of_term vs (TermC.str2term "x::real") = SOME [(1, [1, 0, 0])]
35 then () else error "poly_of_term 2 changed";
37 if poly_of_term vs (TermC.str2term "12 * x \<up> 3") = SOME [(12, [3, 0, 0])]
38 then () else error "poly_of_term 3 changed";
39 "~~~~~ fun poly_of_term , args:"; val (vs, t) =
40 (vs, (TermC.str2term "12 * x \<up> 3"));
42 monom_of_term vs (1, replicate (length vs) 0) t;(*poly malformed 1 with x \<up> 3*)
43 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Groups.times_class.times", _) $ m1 $ m2)) =
44 (vs, (1, replicate (length vs) 0), t);
47 monom_of_term vs (c, es) m1;
48 "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const ("Transcendental.powr", _) $ (t as Free _) $ (Const ("Num.numeral_class.numeral", _) $ num)) ) =
51 (*+*)(num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = [3, 0, 0];
53 if (c, num |> HOLogic.dest_numeral |> list_update es (find_index (curry op = t) vs)) = (12, [3, 0, 0])
54 then () else error "monom_of_term (powr): return value CHANGED";
56 if poly_of_term vs (TermC.str2term "12 * x \<up> 3 * y \<up> 4 * z \<up> 6") = SOME [(12, [3, 4, 6])]
57 then () else error "poly_of_term 4 changed";
59 if poly_of_term vs (TermC.str2term "1 + 2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + y") =
60 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
61 then () else error "poly_of_term 5 changed";
63 (*poly_of_term is quite liberal:*)
64 (*the coefficient may be somewhere, the order of variables and the parentheses
65 within a monomial are arbitrary*)
66 if poly_of_term vs (TermC.str2term "y \<up> 4 * (x \<up> 3 * 12 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
67 then () else error "poly_of_term 6 changed";
69 (*there may even be more than 1 coefficient:*)
70 if poly_of_term vs (TermC.str2term "2 * y \<up> 4 * (x \<up> 3 * 6 * z \<up> 6)") = SOME [(12, [3, 4, 6])]
71 then () else error "poly_of_term 7 changed";
73 (*the order and the parentheses within monomials are arbitrary:*)
74 if poly_of_term vs (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + (7 * y \<up> 8 + 1)")
75 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
76 then () else error "poly_of_term 8 changed";
78 (*from --- rls norm_Rational downto fun gcd_poly ---*)
79 val t = TermC.str2term (*copy from above: "::real" is not required due to " \<up> "*)
80 ("(-12 + 4 * y + 3 * x \<up> 2 + -1 * (x \<up> 2 * y)) /" ^
81 "(-18 + -9 * x + 2 * y \<up> 2 + x * y \<up> 2)");
82 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
83 val opt = check_fraction t;
84 val SOME (numerator, denominator) = opt;
85 (*+*)UnparseC.term numerator = "- 12 + 4 * y + 3 * x \<up> 2 + - 1 * (x \<up> 2 * y)"; (*isa -- isa2*);
86 (*+*)UnparseC.term denominator = "- 18 + - 9 * x + 2 * y \<up> 2 + x * y \<up> 2"; (*isa -- isa2*);
87 val vs = TermC.vars_of t;
88 (*+*)UnparseC.terms vs = "[\"x\", \"y\"]";
89 val baseT = type_of numerator
90 val expT = HOLogic.realT;
91 val (SOME _, SOME _) = (poly_of_term vs numerator, poly_of_term vs denominator); (*isa <> isa2*)
93 "-------- fun is_poly --------------------------------------------------------------------------";
94 "-------- fun is_poly --------------------------------------------------------------------------";
95 "-------- fun is_poly --------------------------------------------------------------------------";
96 if is_poly (TermC.str2term "2 * x \<up> 3 * y \<up> 4 * z \<up> 6 + 7 * y \<up> 8 + 1")
97 then () else error "is_poly 1 changed";
98 if not (is_poly (TermC.str2term "2 * (x \<up> 3 * y \<up> 4 * z \<up> 6 + 7) * y \<up> 8 + 1"))
99 then () else error "is_poly 2 changed";
101 "-------- fun term_of_poly ---------------------------------------------------------------------";
102 "-------- fun term_of_poly ---------------------------------------------------------------------";
103 "-------- fun term_of_poly ---------------------------------------------------------------------";
104 val expT = HOLogic.realT
105 val Free (_, baseT) = (hd o vars o TermC.str2term) "12 * x \<up> 3 * y \<up> 4 * z \<up> 6";
106 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
107 val vs = TermC.vars_of (the (parseNEW ctxt "12 * x \<up> 3 * y \<up> 4 * z \<up> 6"))
108 (*precondition for [(c, es),...]: legth es = length vs*)
110 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"
111 then () else error "term_of_poly 1 changed";
113 "-------- complex examples: rls norm_Rational --------------------------------------------------";
114 "-------- complex examples: rls norm_Rational --------------------------------------------------";
115 "-------- complex examples: rls norm_Rational --------------------------------------------------";
116 val t = TermC.str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
117 val SOME (t', _) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
118 if UnparseC.term t' = "1 / 18 = 0" then () else error "rational.sml 1";
120 val t = TermC.str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
121 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
122 if UnparseC.term t' = "(237 + 65 * x) / 36 = 0" then ()
123 else error "rational.sml 2";
125 val t = TermC.str2term "(1/2 + (5*x)/2) \<up> 2 - ((13*x)/2 - 5/2) \<up> 2 - (6*x) \<up> 2 + 29";
126 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; UnparseC.term t';
127 if UnparseC.term t' = "23 + 35 * x + - 72 * x \<up> 2" then ()
128 else error "rational.sml 3";
130 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
131 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
132 "-------- complex examples cancellation from: Mathematik 1 Schalk ------------------------------";
133 (*Schalk I, p.60 Nr. 215c *)
134 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
135 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
136 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
137 then () else error "rational.sml: diff.behav. in norm_Rational_mg 7";
139 (*SRC Schalk I, p.66 Nr. 381b *)
140 val t = TermC.str2term
141 "(4*x \<up> 2 - 20*x + 25)/(2*x - 5) \<up> 3";
142 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
143 if UnparseC.term t = "1 / (- 5 + 2 * x)"
144 then () else error "rational.sml: diff.behav. in norm_Rational_mg 9";
146 (*Schalk I, p.60 Nr. 215c *)
147 val t = TermC.str2term "(a + b) \<up> 4 * (x - y) / ((x - y) \<up> 3 * (a + b) \<up> 2)";
148 val SOME (t, _) = rewrite_set_ thy false norm_Rational t;
149 if UnparseC.term t = "(a \<up> 2 + 2 * a * b + b \<up> 2) / (x \<up> 2 + - 2 * x * y + y \<up> 2)"
150 then () else error "Schalk I, p.60 Nr. 215c: with Isabelle2002 cancellation incomplete, changed";