1 (* Title: test/Tools/isac/Knowledge/poly-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 is_polyexp -----------------------------------------------------------------------";
13 "-------- fun has_degree_in --------------------------------------------------------------------";
14 "-------- fun mono_deg_in ----------------------------------------------------------------------";
15 "-------- fun sort_variables -------------------------------------------------------------------";
16 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
17 "-------- check make_polynomial with simple terms ----------------------------------------------";
18 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
19 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
20 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
21 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
22 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
23 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
24 "-------- complex examples from textbook Schalk I ----------------------------------------------";
25 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
26 "-----------------------------------------------------------------------------------------------";
27 "-----------------------------------------------------------------------------------------------";
30 "-------- fun is_polyexp -----------------------------------------------------------------------";
31 "-------- fun is_polyexp -----------------------------------------------------------------------";
32 "-------- fun is_polyexp -----------------------------------------------------------------------";
33 val t = TermC.parse_test @{context} "x / x";
34 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
36 val t = TermC.parse_test @{context} "- 1 * A * 3";
37 if is_polyexp t then () else error "is_polyexp (- 1 * A * 3)";
39 val t = TermC.parse_test @{context} "- 1 * AA * 3";
40 if is_polyexp t then () else error "is_polyexp (- 1 * AA * 3)";
42 val t = TermC.parse_test @{context} "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
43 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
45 "-------- fun has_degree_in --------------------------------------------------------------------";
46 "-------- fun has_degree_in --------------------------------------------------------------------";
47 "-------- fun has_degree_in --------------------------------------------------------------------";
49 val ctxt = Proof_Context.init_global thy
50 val v = TermC.parseNEW' ctxt "x";
51 val t = TermC.parseNEW' ctxt "1";
52 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
54 val v = TermC.parseNEW' ctxt "AA";
55 val t = TermC.parseNEW' ctxt "1";
56 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
59 val v = TermC.parseNEW' ctxt "x";
60 val t = TermC.parseNEW' ctxt "a*b+c";
61 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
63 val v = TermC.parseNEW' ctxt "AA";
64 val t = TermC.parseNEW' ctxt "a*b+c";
65 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
68 val v = TermC.parseNEW' ctxt "x";
69 val t = TermC.parseNEW' ctxt "a*x+c";
70 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
72 val v = TermC.parseNEW' ctxt "AA";
73 val t = TermC.parseNEW' ctxt "a*AA+c";
74 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
77 val v = TermC.parseNEW' ctxt "x::real";
78 val t = TermC.parseNEW' ctxt "((a::real)*b+c)*x \<up> 7";
79 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
81 val v = TermC.parseNEW' ctxt "AA";
82 val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
83 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
86 val v = TermC.parseNEW' ctxt "x::real";
87 val t = TermC.parseNEW' ctxt "x \<up> 7";
88 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
90 val v = TermC.parseNEW' ctxt "AA";
91 val t = TermC.parseNEW' ctxt "AA \<up> 7";
92 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
95 val v = TermC.parseNEW' ctxt "x::real";
96 val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
97 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
99 val v = TermC.parseNEW' ctxt "AA";
100 val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
101 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
104 val v = TermC.parseNEW' ctxt "x::real";
105 val t = TermC.parseNEW' ctxt "(a*b+x)*x";
106 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
108 val v = TermC.parseNEW' ctxt "AA";
109 val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
110 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
113 val v = TermC.parseNEW' ctxt "x";
114 val t = TermC.parseNEW' ctxt "x";
115 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
117 val v = TermC.parseNEW' ctxt "AA";
118 val t = TermC.parseNEW' ctxt "AA";
119 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
122 val v = TermC.parseNEW' ctxt "x::real";
123 val t = TermC.parseNEW' ctxt "ab - (a*b)*(x::real)";
124 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
126 val v = TermC.parseNEW' ctxt "AA";
127 val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
128 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
130 "-------- fun mono_deg_in ----------------------------------------------------------------------";
131 "-------- fun mono_deg_in ----------------------------------------------------------------------";
132 "-------- fun mono_deg_in ----------------------------------------------------------------------";
133 val v = TermC.parseNEW' ctxt "x::real";
135 val t = TermC.parseNEW' ctxt "(a*b+c)*x \<up> 7";
136 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
138 val t = TermC.parseNEW' ctxt "(x::real) \<up> 7";
139 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
141 val t = TermC.parseNEW' ctxt "(a*b+c)*x::real";
142 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
144 val t = TermC.parseNEW' ctxt "(a*b+x)*x";
145 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
147 val t = TermC.parseNEW' ctxt "x::real";
148 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
150 val t = TermC.parseNEW' ctxt "(a*b+c)";
151 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
153 val t = TermC.parseNEW' ctxt "ab - (a*b)*x";
154 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
156 (*. . . . . . . . . . . . the same with Const (\<^const_name>\<open>AA\<close>, _) . . . . . . . . . . . *)
157 val thy = @{theory Partial_Fractions}
158 val ctxt = Proof_Context.init_global thy
159 val v = TermC.parseNEW' ctxt "AA";
161 val t = TermC.parseNEW' ctxt "(a*b+c)*AA \<up> 7";
162 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
164 val t = TermC.parseNEW' ctxt "AA \<up> 7";
165 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
167 val t = TermC.parseNEW' ctxt "(a*b+c)*AA";
168 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
170 val t = TermC.parseNEW' ctxt "(a*b+AA)*AA";
171 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
173 val t = TermC.parseNEW' ctxt "AA";
174 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
176 val t = TermC.parseNEW' ctxt "(a*b+c)";
177 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
179 val t = TermC.parseNEW' ctxt "ab - (a*b)*AA";
180 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
183 "-------- fun sort_variables -------------------------------------------------------------------";
184 "-------- fun sort_variables -------------------------------------------------------------------";
185 "-------- fun sort_variables -------------------------------------------------------------------";
186 if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
187 else error "lexicographic order CHANGED";
189 (*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
190 val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
191 val t' = sort_variables t;
192 if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
193 else error "sort_variables 3 * b + a * 2 CHANGED";
195 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
196 val ll = map monom2list (poly2list t);
198 (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
199 (*+*)val [ [(Const (\<^const_name>\<open>numeral\<close>, _) $ _), Free ("b", _)],
200 (*+*) [Free ("a", _), (Const (\<^const_name>\<open>numeral\<close>, _) $ _)]
201 (*+*) ] = map monom2list (poly2list t);
203 val lls = map sort_varList ll;
205 (*+*)case map sort_varList ll of
206 (*+*) [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("b", _)],
207 (*+*) [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)]
209 (*+*)| _ => error "map sort_varList CHANGED";
212 val ls = map (create_monom T) lls;
214 (*+*)val [Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("b", _),
215 (*+*) Const (\<^const_name>\<open>times\<close>, _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
217 (*+*)case map (create_monom T) lls of
218 (*+*) [Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("b", _),
219 (*+*) Const (\<^const_name>\<open>times\<close>, _) $ (Const (\<^const_name>\<open>numeral\<close>, _) $ _) $ Free ("a", _)
221 (*+*)| _ => error "map (create_monom T) CHANGED";
223 val xxx = (*in*) create_polynom T ls (*end*);
225 (*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
226 (*+*)else error "create_polynom CHANGED";
227 (* done by rewriting> 2 * a + 3 * b ? *)
229 (*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
230 val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
231 val t' = sort_variables t;
232 if UnparseC.term t' = "3 * a + - 2 * a" then ()
233 else error "sort_variables 3 * a + - 2 * a CHANGED";
235 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
236 val ll = map monom2list (poly2list t);
238 (*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
239 (*+*) [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*already correct order*)
240 (*+*) ] = map monom2list (poly2list t);
245 (*+*)val [ [Const (\<^const_name>\<open>numeral\<close>, _) $ _, Free ("a", _)],
246 (*+*) [Const (\<^const_name>\<open>uminus\<close>, _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
247 (*+*) ] = map sort_varList ll;
250 "~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
251 val sorted = sort var_ord ts;
253 (*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
254 (*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED";
257 (*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
258 (*+*)then () else error "get_basStr - 2 CHANGED";
259 (*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
260 (*+*)then () else error "get_basStr a CHANGED";
263 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
264 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
265 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
266 val ctxt = Proof_Context.init_global @{theory}
267 val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
268 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
269 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
270 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
271 else error "poly.sml: diff.behav. in make_polynomial 23";
274 ## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
275 ### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
276 ###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered
277 ####### try calc: "Poly.is_addUnordered"
278 ######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*)
280 ####### calc. to: False (*isa*)
283 if is_addUnordered (TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
284 else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
285 "~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
286 ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
288 (*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
290 (*+*) if t = sort_monoms t = false then () else error "sort_monoms 123";
291 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
292 val ll = map monom2list (poly2list t);
293 val lls = sort_monList ll;
295 (*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
296 (*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
298 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
299 (* we check all elements at once..*)
300 val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
301 val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";
303 (*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
304 (*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
305 (*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*)
306 (*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED";
308 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*)
309 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*)
310 (*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*)
312 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*)
314 (*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
316 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
317 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
318 (*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*)
322 val it = true: bool*)
324 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
325 (*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
326 (*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
327 (*{a = "int_ord (4, 10003) = ", z = LESS} isa
328 {a = "int_ord (4, 4) = ", z = EQUAL} isa2*)
329 (*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
330 (*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED";
332 (*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*)
333 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
334 (*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
335 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*)
336 (*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
337 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*)
338 (*1*){a = "dict_cond_ord ([], [])"} (*isa*)
340 (*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*)
341 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
342 {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
343 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*)
345 (*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*)
346 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
347 {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
348 (*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
350 (*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*)
351 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
352 (*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
353 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
354 (*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
355 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
356 (*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*)
364 (*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
365 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
366 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
367 (*if*) (is_nums x) (*else*);
368 val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
370 (*+*)UnparseC.term x = "x \<up> 2";
371 (*if*) TermC.is_num t (*then*);
373 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
374 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
375 (*if*) (is_nums x) (*else*);
376 val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
378 (*+*)UnparseC.term x = "y \<up> 2";
379 (*if*) TermC.is_num t (*then*);
382 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
383 if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
384 ( *---------------------------------------------------------------------------------OPEN local/*)
386 (*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
387 else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED";
388 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
389 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
390 (*if*) (is_nums x) (*else*);
391 val (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
393 (*+*)UnparseC.term x = "x \<up> 3";
394 (*if*) TermC.is_num t (*then*);
396 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
397 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
398 (*if*) (is_nums x) (*else*);
399 val _ = (*the default case*)
401 ( *---------------------------------------------------------------------------------OPEN local/*)
403 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
404 val xxx = dict_cond_ord var_ord_revPow is_nums;
405 (*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED";
406 (*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
407 (*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED";
408 (*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED";
411 "-------- check make_polynomial with simple terms ----------------------------------------------";
412 "-------- check make_polynomial with simple terms ----------------------------------------------";
413 "-------- check make_polynomial with simple terms ----------------------------------------------";
415 val t = TermC.parse_test @{context} "2*3*a";
416 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
417 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
420 val t = TermC.parse_test @{context} "2*a + 3*a";
421 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
422 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
425 val t = TermC.parse_test @{context} "2*a + 3*a + 3*a";
426 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
427 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
430 val t = TermC.parse_test @{context} "3*a - 2*a";
431 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
432 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
435 val t = TermC.parse_test @{context} "4*(3*a - 2*a)";
436 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
437 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
440 val t = TermC.parse_test @{context} "4*(3*a \<up> 2 - 2*a \<up> 2)";
441 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
442 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
444 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
445 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
446 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
447 val thy = @{theory "Isac_Knowledge"};
448 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
449 val t = TermC.parse_test @{context} "x \<up> 2 * x";
450 val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
451 if UnparseC.term t' = "x * x \<up> 2" then ()
452 else error "poly.sml Poly.is_multUnordered doesn't work";
454 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
455 ### rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +
456 (-48 * x \<up> 4 + 8))
457 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
458 ####### try calc: Poly.is_multUnordered'
459 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
461 val t = TermC.parse_test @{context} "5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) + (-48 * x \<up> 4 + 8))";
463 "----- is_multUnordered ---";
464 val tsort = sort_variables t;
465 UnparseC.term tsort = "2 * (5 * (x \<up> 2 * x \<up> 7)) + 3 * (5 * x \<up> 2) + 6 * x \<up> 7 + 9 +\n- 1 * (3 * (6 * (x \<up> 4 * x \<up> 5))) +\n- 1 * (- 1 * (3 * x \<up> 5)) +\n-48 * x \<up> 4 +\n8";
468 is_polyexp t andalso not (t = sort_variables t);
469 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
471 "----- eval_is_multUnordered ---";
472 val tm = TermC.parse_test @{context} "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) + (-48 * x \<up> 4 + 8))) is_multUnordered";
473 case eval_is_multUnordered "testid" "" tm @{context} of
474 SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $
475 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
476 (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $
477 Const (\<^const_name>\<open>True\<close>, _))) => ()
478 | _ => error "poly.sml diff. eval_is_multUnordered";
480 "----- rewrite_set_ STILL DIDN'T WORK";
481 val SOME (t, _) = rewrite_set_ ctxt true order_mult_ t;
485 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
486 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
487 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
488 val thy = @{theory "Isac_Knowledge"};
489 val t as (_ $ arg) = TermC.parse_test @{context} "(3 * a + - 2 * a) is_multUnordered";
491 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
492 (*+*) andalso not (is_multUnordered arg)
493 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
495 case eval_is_multUnordered "xxx " "yyy " t @{context} of
497 ("xxx 3 * a + - 2 * a_",
498 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
499 Const (\<^const_name>\<open>False\<close>, _))) => ()
500 (* Const (\<^const_name>\<open>True\<close>, _))) => () <<<<<--------------------------- this is false*)
501 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
503 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
504 val t as (_ $ arg) = TermC.parse_test @{context} "(- 2 * a) is_multUnordered";
506 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
507 (*+*) andalso not (is_multUnordered arg)
508 (*+*)then () else error "sort_variables - 2 * a CHANGED";
510 case eval_is_multUnordered "xxx " "yyy " t @{context} of
513 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
514 Const (\<^const_name>\<open>False\<close>, _))) => ()
515 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
517 "----- is_multUnordered --- (a) is_multUnordered = False";
518 val t as (_ $ arg) = TermC.parse_test @{context} "(a) is_multUnordered";
520 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
521 (*+*) andalso not (is_multUnordered arg)
522 (*+*)then () else error "sort_variables a CHANGED";
524 case eval_is_multUnordered "xxx " "yyy " t @{context} of
527 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
528 Const (\<^const_name>\<open>False\<close>, _))) => ()
529 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
531 "----- is_multUnordered --- (- 2) is_multUnordered = False";
532 val t as (_ $ arg) = TermC.parse_test @{context} "(- 2) is_multUnordered";
534 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
535 (*+*) andalso not (is_multUnordered arg)
536 (*+*)then () else error "sort_variables - 2 CHANGED";
538 case eval_is_multUnordered "xxx " "yyy " t @{context} of
541 Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $
542 Const (\<^const_name>\<open>False\<close>, _))) => ()
543 | _ => error "eval_is_multUnordered 3 * a + - 2 * a CHANGED";
546 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
547 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
548 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
549 (* ca.line 45 of Rewrite.trace_on:
550 ## rls: order_mult_rls_ on:
551 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
552 ### rls: order_mult_ on:
553 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
554 ###### rls: Rule_Set.empty-is_multUnordered on:
555 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered
556 ####### try calc: "Poly.is_multUnordered"
558 N:x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3 is_multUnordered = True"
559 -------------------------------------------------------------------------------------------------==
560 O:x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * (- 1 \<up> 2 * a \<up> 2) + - 1 \<up> 3 * a \<up> 3 is_multUnordered = True"
561 ####### calc. to: True
562 ####### try calc: "Poly.is_multUnordered"
563 ####### try calc: "Poly.is_multUnordered"
564 ### rls: order_mult_ on:
565 N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + 3 * (a \<up> 2 * (x * (- 1) \<up> 2)) + a \<up> 3 * (- 1) \<up> 3
566 --------+--------------------------+---------------------------------+---------------------------<>
567 O:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + - 1 \<up> 2 * (3 * (a \<up> 2 * x)) + - 1 \<up> 3 * a \<up> 3
568 -------------------------------------------------------------------------------------------------<>
570 val t = TermC.parse_test @{context} "x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3";
572 "~~~~~ fun is_multUnordered
573 "~~~~~~~ fun sort_variables
574 "~~~~~~~~~ val sort_varList
576 "~~~~~ fun is_multUnordered , args:"; val (t) = (t);
581 (*+*)if UnparseC.term return =
582 (*+*) "x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) +\n(- 1) \<up> 2 * (3 * (a \<up> 2 * x)) +\n(- 1) \<up> 3 * a \<up> 3"
583 (*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
585 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
586 val ll = map monom2list (poly2list t);
587 val lls = map sort_varList ll;
589 (*+*)val ori3 = nth 3 ll;
590 (*+*)val mon3 = nth 3 lls;
592 (*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
593 (*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
594 (*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
595 (*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
597 (*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
598 (*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
599 (*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
600 (*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
602 "~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
603 (* Output below with:
604 val sort_varList = sort var_ord;
605 fun var_ord (a,b: term) =
606 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
607 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
608 prod_ord string_ord string_ord
609 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
612 (*+*)val xxx = sort_varList ori3;
614 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
615 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
618 {a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"}
619 {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"}
620 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
621 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
622 {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
623 {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"}
626 {a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"}
627 {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"}
629 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
630 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
631 {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
632 {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"}
636 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
637 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
638 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
639 val t = TermC.parse_test @{context} "b * a * a";
640 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
641 if UnparseC.term t = "a \<up> 2 * b" then ()
642 else error "poly.sml: diff.behav. in make_polynomial 21";
644 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
645 ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
647 (*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
648 "~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (t);
649 (*if*) TermC.is_num num (*else*);
651 "~~~~~ fun is_polyexp , args:"; val (Const (\<^const_name>\<open>times\<close>,_) $ num $ Free _) = (num);
652 (*if*) TermC.is_num num (*else*);
653 (*if*) TermC.is_variable num (*then*);
655 val xxx = sort_variables t;
656 (*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
659 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
660 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
661 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
662 val t = TermC.parse_test @{context} "2*3*a";
663 val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;
664 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
666 ## try calc: "Groups.times_class.times"
667 ## rls: order_mult_rls_ on: 6 * a
668 ### rls: order_mult_ on: 6 * a
669 ###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered
670 ####### try calc: "Poly.is_multUnordered"
671 ######## eval asms: "6 * a is_multUnordered = True" (*isa*)
673 ####### calc. to: True (*isa*)
676 val t = TermC.parse_test @{context} "(6 * a) is_multUnordered";
679 eval_is_multUnordered "xxx" () t @{context};
680 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
681 (*+*)else error "6 * a is_multUnordered = False CHANGED";
683 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
684 (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)), thy) = ("xxx", (), t, @{theory});
685 (*if*) is_multUnordered arg (*else*);
687 "~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
689 ((is_polyexp t) andalso not (t = sort_variables t));
691 (*+*)return = false; (*isa*)
692 (*+*) is_polyexp t = true; (*isa*)
693 (*+*) not (t = sort_variables t) = false; (*isa*)
695 val xxx = sort_variables t;
696 (*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
698 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
699 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
700 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
701 val thy = @{theory AlgEin};
702 val ctxt = Proof_Context.init_global thy;
704 val SOME (f',_) = rewrite_set_ ctxt false norm_Poly
705 (TermC.parse_test @{context} "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
706 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
707 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
708 else error "norm_Poly changed behavior";
710 ## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
711 ### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
712 ###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
714 ####### try calc: "Poly.is_addUnordered"
715 ######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
716 oben is_addUnordered = True"
717 ####### calc. to: True
718 ####### try calc: "Poly.is_addUnordered"
719 ####### try calc: "Poly.is_addUnordered"
720 ### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
722 "~~~~~ fun sort_monoms , args:"; val (t) =
723 (TermC.parse_test @{context} "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
726 (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
729 "-------- complex examples from textbook Schalk I ----------------------------------------------";
730 "-------- complex examples from textbook Schalk I ----------------------------------------------";
731 "-------- complex examples from textbook Schalk I ----------------------------------------------";
732 val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
733 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
734 if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
735 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
737 "-----SPB Schalk I p.64 No.296a ---";
738 val t = TermC.parse_test @{context} "(x - a) \<up> 3";
739 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
740 if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
741 then () else error "poly.sml: diff.behav. in make_polynomial 10";
743 "-----SPB Schalk I p.64 No.296c ---";
744 val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
745 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
746 if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
747 then () else error "poly.sml: diff.behav. in make_polynomial 11";
749 "-----SPB Schalk I p.62 No.242c ---";
750 val t = TermC.parse_test @{context} "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
751 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
752 if (UnparseC.term t) = "1"
753 then () else error "poly.sml: diff.behav. in make_polynomial 12";
755 "-----SPB Schalk I p.60 No.209a ---";
756 val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
757 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
758 if UnparseC.term t = "a \<up> 7"
759 then () else error "poly.sml: diff.behav. in make_polynomial 13";
761 "-----SPB Schalk I p.60 No.209d ---";
762 val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
763 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
764 if UnparseC.term t = "d \<up> 3"
765 then () else error "poly.sml: diff.behav. in make_polynomial 14";
768 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
769 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
770 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
772 val t = TermC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";
773 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
774 if UnparseC.term t = "1" then ()
775 else error "poly.sml: diff.behav. in make_polynomial 15";
778 val t = TermC.parse_test @{context} "a \<up> 2*b*b \<up> (- 1)";
779 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
780 if UnparseC.term t = "a \<up> 2" then ()
781 else error "poly.sml: diff.behav. in make_polynomial 18";
783 val t = TermC.parse_test @{context} "a \<up> 2*a \<up> (- 2)";
784 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
785 if (UnparseC.term t) = "1" then ()
786 else error "poly.sml: diff.behav. in make_polynomial 19";
788 val t = TermC.parse_test @{context} "b + a - b";
789 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
790 if (UnparseC.term t) = "a" then ()
791 else error "poly.sml: diff.behav. in make_polynomial 20";
794 val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
795 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
796 if (UnparseC.term t) = "a \<up> 4" then ()
797 else error "poly.sml: diff.behav. in make_polynomial 24";