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.str2term "x / x";
34 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
36 val t = TermC.str2term "-1 * A * 3";
37 if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
39 val t = TermC.str2term "-1 * AA * 3";
40 if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
42 val t = TermC.str2term "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 --------------------------------------------------------------------";
48 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
49 val t = (Thm.term_of o the o (TermC.parse thy)) "1";
50 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
52 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
53 val t = (Thm.term_of o the o (TermC.parse thy)) "1";
54 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
57 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
58 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
59 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
61 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
62 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
63 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
66 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
67 val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
68 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
70 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
71 val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
72 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
75 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
76 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
77 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
79 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
80 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
81 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
84 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
85 val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
86 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
88 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
89 val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
90 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
93 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
94 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
95 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
97 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
98 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
99 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
102 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
103 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
104 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
106 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
107 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
108 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
111 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
112 val t = (Thm.term_of o the o (TermC.parse thy)) "x";
113 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
115 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
116 val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
117 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
120 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
121 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
122 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
124 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
125 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
126 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
128 "-------- fun mono_deg_in ----------------------------------------------------------------------";
129 "-------- fun mono_deg_in ----------------------------------------------------------------------";
130 "-------- fun mono_deg_in ----------------------------------------------------------------------";
131 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
133 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
134 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
136 val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
137 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
139 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
140 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
142 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
143 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
145 val t = (Thm.term_of o the o (TermC.parse thy)) "x";
146 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
148 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
149 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
151 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
152 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
154 (*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
155 val thy = @{theory Partial_Fractions}
156 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
158 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
159 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
161 val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
162 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
164 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
165 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
167 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
168 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
170 val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
171 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
173 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
174 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
176 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
177 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
180 "-------- fun sort_variables -------------------------------------------------------------------";
181 "-------- fun sort_variables -------------------------------------------------------------------";
182 "-------- fun sort_variables -------------------------------------------------------------------";
183 if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
184 else error "lexicographic order CHANGED";
186 (*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
187 val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
188 val t' = sort_variables t;
189 if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
190 else error "sort_variables 3 * b + a * 2 CHANGED";
192 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
193 val ll = map monom2list (poly2list t);
195 (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
196 (*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
197 (*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
198 (*+*) ] = map monom2list (poly2list t);
200 val lls = map sort_varList ll;
202 (*+*)case map sort_varList ll of
203 (*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
204 (*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
206 (*+*)| _ => error "map sort_varList CHANGED";
209 val ls = map (create_monom T) lls;
211 (*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
212 (*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
214 (*+*)case map (create_monom T) lls of
215 (*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
216 (*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
218 (*+*)| _ => error "map (create_monom T) CHANGED";
220 val xxx = (*in*) create_polynom T ls (*end*);
222 (*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
223 (*+*)else error "create_polynom CHANGED";
224 (* done by rewriting> 2 * a + 3 * b ? *)
226 (*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
227 val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
228 val t' = sort_variables t;
229 if UnparseC.term t' = "3 * a + - 2 * a" then ()
230 else error "sort_variables 3 * a + - 2 * a CHANGED";
232 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
233 val ll = map monom2list (poly2list t);
235 (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
236 (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
237 (*+*) ] = map monom2list (poly2list t);
242 (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
243 (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
244 (*+*) ] = map sort_varList ll;
247 "~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
248 val sorted = sort var_ord ts;
250 (*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
251 (*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED";
254 (*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
255 (*+*)then () else error "get_basStr - 2 CHANGED";
256 (*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
257 (*+*)then () else error "get_basStr a CHANGED";
260 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
261 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
262 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
263 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
264 Rewrite.trace_on := false;
265 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
266 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
267 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
268 else error "poly.sml: diff.behav. in make_polynomial 23";
271 ## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
272 ### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
273 ###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered
274 ####### try calc: "Poly.is_addUnordered"
275 ######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*)
277 ####### calc. to: False (*isa*)
280 if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
281 else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
282 "~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
283 ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
285 (*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
287 (*+*) if t = sort_monoms t = false then () else error "sort_monoms 123";
288 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
289 val ll = map monom2list (poly2list t);
290 val lls = sort_monList ll;
292 (*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
293 (*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
295 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
296 (* we check all elements at once..*)
297 val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
298 val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";
300 (*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
301 (*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
302 (*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*)
303 (*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED";
305 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*)
306 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*)
307 (*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*)
309 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*)
311 (*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
313 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
314 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
315 (*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*)
319 val it = true: bool*)
321 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
322 (*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
323 (*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
324 (*{a = "int_ord (4, 10003) = ", z = LESS} isa
325 {a = "int_ord (4, 4) = ", z = EQUAL} isa2*)
326 (*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
327 (*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED";
329 (*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*)
330 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
331 (*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
332 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*)
333 (*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
334 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*)
335 (*1*){a = "dict_cond_ord ([], [])"} (*isa*)
337 (*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*)
338 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
339 {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
340 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*)
342 (*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*)
343 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
344 {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
345 (*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
347 (*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*)
348 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
349 (*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
350 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
351 (*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
352 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
353 (*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*)
361 (*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
362 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
363 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
364 (*if*) (is_nums x) (*else*);
365 val (Const ("Transcendental.powr", _) $ Free _ $ t) =
367 (*+*)UnparseC.term x = "x \<up> 2";
368 (*if*) TermC.is_num t (*then*);
370 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
371 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
372 (*if*) (is_nums x) (*else*);
373 val (Const ("Transcendental.powr", _) $ Free _ $ t) =
375 (*+*)UnparseC.term x = "y \<up> 2";
376 (*if*) TermC.is_num t (*then*);
379 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
380 if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
381 ( *---------------------------------------------------------------------------------OPEN local/*)
383 (*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
384 else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED";
385 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
386 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
387 (*if*) (is_nums x) (*else*);
388 val (Const ("Transcendental.powr", _) $ Free _ $ t) =
390 (*+*)UnparseC.term x = "x \<up> 3";
391 (*if*) TermC.is_num t (*then*);
393 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
394 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
395 (*if*) (is_nums x) (*else*);
396 val _ = (*the default case*)
398 ( *---------------------------------------------------------------------------------OPEN local/*)
400 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
401 val xxx = dict_cond_ord var_ord_revPow is_nums;
402 (*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED";
403 (*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
404 (*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED";
405 (*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED";
408 "-------- check make_polynomial with simple terms ----------------------------------------------";
409 "-------- check make_polynomial with simple terms ----------------------------------------------";
410 "-------- check make_polynomial with simple terms ----------------------------------------------";
412 val t = TermC.str2term "2*3*a";
413 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
414 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
417 val t = TermC.str2term "2*a + 3*a";
418 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
419 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
422 val t = TermC.str2term "2*a + 3*a + 3*a";
423 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
424 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
427 val t = TermC.str2term "3*a - 2*a";
428 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
429 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
432 val t = TermC.str2term "4*(3*a - 2*a)";
433 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
434 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
437 val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
438 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
439 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
441 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
442 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
443 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
444 val thy = @{theory "Isac_Knowledge"};
445 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
446 val t = TermC.str2term "x \<up> 2 * x";
447 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
448 if UnparseC.term t' = "x * x \<up> 2" then ()
449 else error "poly.sml Poly.is_multUnordered doesn't work";
451 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
452 ### 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) +
453 (-48 * x \<up> 4 + 8))
454 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
455 ####### try calc: Poly.is_multUnordered'
456 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
458 val t = TermC.str2term "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))";
460 "----- is_multUnordered ---";
461 val tsort = sort_variables t;
462 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";
465 is_polyexp t andalso not (t = sort_variables t);
466 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
468 "----- eval_is_multUnordered ---";
469 val tm = TermC.str2term "(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";
470 case eval_is_multUnordered "testid" "" tm thy of
471 SOME (_, Const ("HOL.Trueprop", _) $
472 (Const ("HOL.eq", _) $
473 (Const ("Poly.is_multUnordered", _) $ _) $
474 Const ("HOL.True", _))) => ()
475 | _ => error "poly.sml diff. eval_is_multUnordered";
477 "----- rewrite_set_ STILL DIDN'T WORK";
478 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
482 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
483 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
484 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
485 val thy = @{theory "Isac_Knowledge"};
486 val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
488 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
489 (*+*) andalso not (is_multUnordered arg)
490 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
492 case eval_is_multUnordered "xxx " "yyy " t thy of
494 ("xxx 3 * a + - 2 * a_",
495 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
496 Const ("HOL.False", _))) => ()
497 (* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
498 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
500 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
501 val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
503 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
504 (*+*) andalso not (is_multUnordered arg)
505 (*+*)then () else error "sort_variables - 2 * a CHANGED";
507 case eval_is_multUnordered "xxx " "yyy " t thy of
510 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
511 Const ("HOL.False", _))) => ()
512 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
514 "----- is_multUnordered --- (a) is_multUnordered = False";
515 val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
517 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
518 (*+*) andalso not (is_multUnordered arg)
519 (*+*)then () else error "sort_variables a CHANGED";
521 case eval_is_multUnordered "xxx " "yyy " t thy of
524 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
525 Const ("HOL.False", _))) => ()
526 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
528 "----- is_multUnordered --- (- 2) is_multUnordered = False";
529 val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
531 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
532 (*+*) andalso not (is_multUnordered arg)
533 (*+*)then () else error "sort_variables - 2 CHANGED";
535 case eval_is_multUnordered "xxx " "yyy " t thy of
538 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
539 Const ("HOL.False", _))) => ()
540 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
543 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
544 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
545 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
546 (* ca.line 45 of Rewrite.trace_on:
547 ## rls: order_mult_rls_ on:
548 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
549 ### rls: order_mult_ on:
550 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
551 ###### rls: Rule_Set.empty-is_multUnordered on:
552 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
553 ####### try calc: "Poly.is_multUnordered"
555 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"
556 -------------------------------------------------------------------------------------------------==
557 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"
558 ####### calc. to: True
559 ####### try calc: "Poly.is_multUnordered"
560 ####### try calc: "Poly.is_multUnordered"
561 ### rls: order_mult_ on:
562 N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + 3 * (a \<up> 2 * (x * (- 1) \<up> 2)) + a \<up> 3 * (- 1) \<up> 3
563 --------+--------------------------+---------------------------------+---------------------------<>
564 O:x \<up> 3 + -1 * (3 * (a * x \<up> 2)) + -1 \<up> 2 * (3 * (a \<up> 2 * x)) + -1 \<up> 3 * a \<up> 3
565 -------------------------------------------------------------------------------------------------<>
567 val t = TermC.str2term "x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3";
569 "~~~~~ fun is_multUnordered
570 "~~~~~~~ fun sort_variables
571 "~~~~~~~~~ val sort_varList
573 "~~~~~ fun is_multUnordered , args:"; val (t) = (t);
578 (*+*)if UnparseC.term return =
579 (*+*) "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"
580 (*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
582 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
583 val ll = map monom2list (poly2list t);
584 val lls = map sort_varList ll;
586 (*+*)val ori3 = nth 3 ll;
587 (*+*)val mon3 = nth 3 lls;
589 (*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
590 (*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
591 (*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
592 (*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
594 (*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
595 (*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
596 (*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
597 (*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
599 "~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
600 (* Output below with:
601 val sort_varList = sort var_ord;
602 fun var_ord (a,b: term) =
603 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
604 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
605 prod_ord string_ord string_ord
606 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
609 (*+*)val xxx = sort_varList ori3;
611 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
612 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
615 {a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"}
616 {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"}
617 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
618 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
619 {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
620 {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"}
623 {a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"}
624 {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"}
626 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
627 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
628 {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
629 {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"}
633 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
634 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
635 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
636 val t = TermC.str2term "b * a * a";
637 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
638 if UnparseC.term t = "a \<up> 2 * b" then ()
639 else error "poly.sml: diff.behav. in make_polynomial 21";
641 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
642 ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
644 (*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
645 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
646 (*if*) TermC.is_num num (*else*);
648 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
649 (*if*) TermC.is_num num (*else*);
650 (*if*) TermC.is_variable num (*then*);
652 val xxx = sort_variables t;
653 (*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
656 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
657 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
658 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
659 val t = TermC.str2term "2*3*a";
660 val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
661 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
663 ## try calc: "Groups.times_class.times"
664 ## rls: order_mult_rls_ on: 6 * a
665 ### rls: order_mult_ on: 6 * a
666 ###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered
667 ####### try calc: "Poly.is_multUnordered"
668 ######## eval asms: "6 * a is_multUnordered = True" (*isa*)
670 ####### calc. to: True (*isa*)
673 val t = TermC.str2term "(6 * a) is_multUnordered";
676 eval_is_multUnordered "xxx" () t @{theory};
677 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
678 (*+*)else error "6 * a is_multUnordered = False CHANGED";
680 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
681 (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
682 (*if*) is_multUnordered arg (*else*);
684 "~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
686 ((is_polyexp t) andalso not (t = sort_variables t));
688 (*+*)return = false; (*isa*)
689 (*+*) is_polyexp t = true; (*isa*)
690 (*+*) not (t = sort_variables t) = false; (*isa*)
692 val xxx = sort_variables t;
693 (*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
695 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
696 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
697 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
698 val thy = @{theory AlgEin};
700 val SOME (f',_) = rewrite_set_ thy false norm_Poly
701 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
702 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
703 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
704 else error "norm_Poly changed behavior";
706 ## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
707 ### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
708 ###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
710 ####### try calc: "Poly.is_addUnordered"
711 ######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
712 oben is_addUnordered = True"
713 ####### calc. to: True
714 ####### try calc: "Poly.is_addUnordered"
715 ####### try calc: "Poly.is_addUnordered"
716 ### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
718 "~~~~~ fun sort_monoms , args:"; val (t) =
719 (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
722 (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
725 "-------- complex examples from textbook Schalk I ----------------------------------------------";
726 "-------- complex examples from textbook Schalk I ----------------------------------------------";
727 "-------- complex examples from textbook Schalk I ----------------------------------------------";
728 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
729 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
730 if (UnparseC.term t) = "1 + -2 * x \<up> 4 + x \<up> 8"
731 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
733 "-----SPB Schalk I p.64 No.296a ---";
734 val t = TermC.str2term "(x - a) \<up> 3";
735 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
736 if (UnparseC.term t) = "-1 * a \<up> 3 + 3 * a \<up> 2 * x + -3 * a * x \<up> 2 + x \<up> 3"
737 then () else error "poly.sml: diff.behav. in make_polynomial 10";
739 "-----SPB Schalk I p.64 No.296c ---";
740 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
741 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
742 if (UnparseC.term t) = "-27 * x \<up> 3 + -108 * x \<up> 2 * y + -144 * x * y \<up> 2 +\n-64 * y \<up> 3"
743 then () else error "poly.sml: diff.behav. in make_polynomial 11";
745 "-----SPB Schalk I p.62 No.242c ---";
746 val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
747 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
748 if (UnparseC.term t) = "1"
749 then () else error "poly.sml: diff.behav. in make_polynomial 12";
751 "-----SPB Schalk I p.60 No.209a ---";
752 val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
753 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
754 if UnparseC.term t = "a \<up> 7"
755 then () else error "poly.sml: diff.behav. in make_polynomial 13";
757 "-----SPB Schalk I p.60 No.209d ---";
758 val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
759 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
760 if UnparseC.term t = "d \<up> 3"
761 then () else error "poly.sml: diff.behav. in make_polynomial 14";
764 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
765 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
766 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
768 val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
769 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
770 if UnparseC.term t = "1" then ()
771 else error "poly.sml: diff.behav. in make_polynomial 15";
774 val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
775 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
776 if UnparseC.term t = "a \<up> 2" then ()
777 else error "poly.sml: diff.behav. in make_polynomial 18";
779 val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
780 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
781 if (UnparseC.term t) = "1" then ()
782 else error "poly.sml: diff.behav. in make_polynomial 19";
784 val t = TermC.str2term "b + a - b";
785 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
786 if (UnparseC.term t) = "a" then ()
787 else error "poly.sml: diff.behav. in make_polynomial 20";
790 val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
791 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
792 if (UnparseC.term t) = "a \<up> 4" then ()
793 else error "poly.sml: diff.behav. in make_polynomial 24";