2 author: Matthias Goldgruber 2003
3 (c) due to copyright terms
6 WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
7 examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
10 "-----------------------------------------------------------------------------------------------";
11 "-----------------------------------------------------------------------------------------------";
12 "table of contents -----------------------------------------------------------------------------";
13 "-----------------------------------------------------------------------------------------------";
14 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
15 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
16 "-------- fun is_polyexp -----------------------------------------------------------------------";
17 "-------- fun has_degree_in --------------------------------------------------------------------";
18 "-------- fun mono_deg_in ----------------------------------------------------------------------";
19 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
20 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
21 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
22 "-------- fun sort_variables -------------------------------------------------------------------";
23 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
24 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
25 "-------- check make_polynomial with simple terms ----------------------------------------------";
26 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
27 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
28 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
29 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
30 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
31 "-------- examples from textbook Schalk I ------------------------------------------------------";
32 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
33 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
34 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
35 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
36 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
37 "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
38 "-------- ord_make_polynomial ------------------------------------------------------------------";
39 "-----------------------------------------------------------------------------------------------";
40 "-----------------------------------------------------------------------------------------------";
41 "-----------------------------------------------------------------------------------------------";
44 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
45 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
46 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
47 (* indentation indicates call hierarchy:
48 "~~~~~ fun is_addUnordered
49 "~~~~~~~ fun is_polyexp
50 "~~~~~~~ fun sort_monoms
51 "~~~~~~~~~ fun sort_monList
52 "~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order
53 "~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order
54 "~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order
55 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order
56 "~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv
57 "~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv
58 "~~~~~~~~~~~~~~~ fun monom_degree : term list -> int
59 "~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order
60 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option
61 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string
62 "~~~~~ fun is_multUnordered
63 "~~~~~~~ fun sort_variables
64 "~~~~~~~~~ fun sort_varList
65 "~~~~~~~~~~~ fun var_ord
66 "~~~~~~~~~~~~~ fun get_basStr used twice --^^
67 "~~~~~~~~~~~~~ fun get_potStr used twice --^^
69 fun int_ord (i1, i2) =
70 (@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
74 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
75 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
76 prod_ord string_ord string_ord
77 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
79 fun var_ord_revPow (a, b: term) =
80 (@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
81 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
82 prod_ord string_ord string_ord_rev
83 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
86 (@{print} {a = "sort_varList", args = UnparseC.terms ts};
89 fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
90 | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
91 | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
92 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
93 (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",
94 is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
95 case (cond x, cond y) of
97 (case elem_ord (x, y) of
98 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
100 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
101 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
102 | (true, true) => dict_cond_ord elem_ord cond (xs, ys)
104 fun compare_koeff_ord (xs, ys) =
105 (@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",
106 sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};
108 ((koeff2ordStr o get_koeff_of_mon) xs,
109 (koeff2ordStr o get_koeff_of_mon) ys)
111 fun var_ord (a,b: term) =
112 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
113 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
114 prod_ord string_ord string_ord
115 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
120 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
121 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
122 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
123 (* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.
125 sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
126 @{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
127 val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
128 val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
130 val SOME (t', []) = rewrite_ @{theory} tless_true Rule_Set.empty true thm_isac t_isac;
131 if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("-1", _)*))
132 else error "thm - ?z = - 1 * ?z loops with new numerals";
135 "-------- fun is_polyexp -----------------------------------------------------------------------";
136 "-------- fun is_polyexp -----------------------------------------------------------------------";
137 "-------- fun is_polyexp -----------------------------------------------------------------------";
138 val t = TermC.str2term "x / x";
139 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
141 val t = TermC.str2term "-1 * A * 3";
142 if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
144 val t = TermC.str2term "-1 * AA * 3";
145 if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
147 val t = TermC.str2term "x * x + x * y + (- 1 * y * x + - 1 * y * y)::real";
148 if is_polyexp t then () else error "is_polyexp (x * x + x * y + (- 1 * y * x + - 1 * y * y))";
150 "-------- fun has_degree_in --------------------------------------------------------------------";
151 "-------- fun has_degree_in --------------------------------------------------------------------";
152 "-------- fun has_degree_in --------------------------------------------------------------------";
153 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
154 val t = (Thm.term_of o the o (TermC.parse thy)) "1";
155 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
157 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
158 val t = (Thm.term_of o the o (TermC.parse thy)) "1";
159 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
162 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
163 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
164 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
166 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
167 val t = (Thm.term_of o the o (TermC.parse thy)) "a*b+c";
168 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
171 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
172 val t = (Thm.term_of o the o (TermC.parse thy)) "a*x+c";
173 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
175 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
176 val t = (Thm.term_of o the o (TermC.parse thy)) "a*AA+c";
177 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
180 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
181 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
182 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x \<up> 7) x";
184 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
185 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
186 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA \<up> 7) AA";
189 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
190 val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
191 if has_degree_in t v = 7 then () else error "has_degree_in (x \<up> 7) x";
193 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
194 val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
195 if has_degree_in t v = 7 then () else error "has_degree_in (AA \<up> 7) AA";
198 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
199 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
200 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
202 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
203 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
204 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
207 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
208 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
209 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
211 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
212 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
213 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
216 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
217 val t = (Thm.term_of o the o (TermC.parse thy)) "x";
218 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
220 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
221 val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
222 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
225 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
226 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
227 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
229 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
230 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
231 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
233 "-------- fun mono_deg_in ----------------------------------------------------------------------";
234 "-------- fun mono_deg_in ----------------------------------------------------------------------";
235 "-------- fun mono_deg_in ----------------------------------------------------------------------";
236 val v = (Thm.term_of o the o (TermC.parse thy)) "x";
238 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x \<up> 7";
239 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x \<up> 7) x changed";
241 val t = (Thm.term_of o the o (TermC.parse thy)) "x \<up> 7";
242 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x \<up> 7) x changed";
244 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*x";
245 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
247 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+x)*x";
248 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
250 val t = (Thm.term_of o the o (TermC.parse thy)) "x";
251 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
253 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
254 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
256 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*x";
257 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
259 (*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
260 val thy = @{theory Partial_Fractions}
261 val v = (Thm.term_of o the o (TermC.parse thy)) "AA";
263 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA \<up> 7";
264 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA \<up> 7) AA changed";
266 val t = (Thm.term_of o the o (TermC.parse thy)) "AA \<up> 7";
267 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA \<up> 7) AA changed";
269 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)*AA";
270 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
272 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+AA)*AA";
273 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
275 val t = (Thm.term_of o the o (TermC.parse thy)) "AA";
276 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
278 val t = (Thm.term_of o the o (TermC.parse thy)) "(a*b+c)";
279 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
281 val t = (Thm.term_of o the o (TermC.parse thy)) "ab - (a*b)*AA";
282 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
284 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
285 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
286 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
287 val thy = @{theory Partial_Fractions}
288 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
289 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
291 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
292 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
294 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
295 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
296 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
297 val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*x + x \<up> 2) is_expanded_in x";
298 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
299 if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
300 andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
301 then () else error "eval_is_expanded_in x ..changed";
303 val thy = @{theory Partial_Fractions}
304 val t = (Thm.term_of o the o (TermC.parse thy)) "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
305 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
306 if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
307 andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
308 then () else error "eval_is_expanded_in AA ..changed";
311 val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*x + x \<up> 2) is_poly_in x";
312 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
313 if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
314 andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
315 then () else error "is_poly_in x ..changed";
317 val t = (Thm.term_of o the o (TermC.parse thy)) "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
318 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
319 if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
320 andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
321 then () else error "is_poly_in AA ..changed";
324 val thy = @{theory Partial_Fractions}
325 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
326 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
328 val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
329 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
331 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
332 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
333 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
334 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
337 *** Const (HOL.Trueprop, bool => prop)
338 *** . Const (HOL.eq, real => real => bool)
339 *** . . Const (Groups.minus_class.minus, real => real => real)
340 *** . . . Const (Groups.zero_class.zero, real)
341 *** . . . Var ((x, 0), real)
342 *** . . Const (Groups.uminus_class.uminus, real => real)
343 *** . . . Var ((x, 0), real)
346 Const ("HOL.Trueprop", _) $
347 (Const ("HOL.eq", _) $
348 (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $
350 (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
351 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
354 val t = (Thm.term_of o the o (TermC.parse thy)) "- 1";
362 Const ("Groups.uminus_class.uminus", _) $ Const ("Groups.one_class.one", _) => ()
363 | _ => error "internal representation of \"- 1\" changed";
365 "======= these external values all have the same internal representation";
366 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
367 (*----------------------------------- vvvvv -------------------------------------------*)
368 val t = (Thm.term_of o the o (TermC.parse thy)) "-x";
371 *** Free ( -x, real)*)
373 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
374 | _ => error "internal representation of \"-x\" changed";
375 (*----------------------------------- vvvvv -------------------------------------------*)
376 val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
379 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
381 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
382 | _ => error "internal representation of \"- x\" changed";
383 (*----------------------------------- vvvvvv ------------------------------------------*)
384 val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
387 *** Free ( -x, real)*)
389 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
390 | _ => error "internal representation of \"-(x)\" changed";
393 "-------- fun sort_variables -------------------------------------------------------------------";
394 "-------- fun sort_variables -------------------------------------------------------------------";
395 "-------- fun sort_variables -------------------------------------------------------------------";
396 if "---" < "123" andalso "123" < "a" andalso "a" < "cba" then ()
397 else error "lexicographic order CHANGED";
399 (*--------------vvvvvvvvvvvvvvv-----------------------------------------------------------------*)
400 val t = @{term "3 * b + a * 2"}; (*------------------------------------------------------------*)
401 val t' = sort_variables t;
402 if UnparseC.term t' = "(3::'a) * b + (2::'a) * a" then ()
403 else error "sort_variables 3 * b + a * 2 CHANGED";
405 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
406 val ll = map monom2list (poly2list t);
408 (*+*)UnparseC.terms (poly2list t) = "[\"(3::'a) * b\", \"a * (2::'a)\"]";
409 (*+*)val [ [(Const ("Num.numeral_class.numeral", _) $ _), Free ("b", _)],
410 (*+*) [Free ("a", _), (Const ("Num.numeral_class.numeral", _) $ _)]
411 (*+*) ] = map monom2list (poly2list t);
413 val lls = map sort_varList ll;
415 (*+*)case map sort_varList ll of
416 (*+*) [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("b", _)],
417 (*+*) [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)]
419 (*+*)| _ => error "map sort_varList CHANGED";
422 val ls = map (create_monom T) lls;
424 (*+*)val [Const ("Groups.times_class.times", _) $ _ $ Free ("b", _),
425 (*+*) Const ("Groups.times_class.times", _) $ _ $ Free ("a", _)] = map (create_monom T) lls;
427 (*+*)case map (create_monom T) lls of
428 (*+*) [Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("b", _),
429 (*+*) Const ("Groups.times_class.times", _) $ (Const ("Num.numeral_class.numeral", _) $ _) $ Free ("a", _)
431 (*+*)| _ => error "map (create_monom T) CHANGED";
433 val xxx = (*in*) create_polynom T ls (*end*);
435 (*+*)if UnparseC.term xxx = "(3::'a) * b + (2::'a) * a" then ()
436 (*+*)else error "create_polynom CHANGED";
437 (* done by rewriting> 2 * a + 3 * b ? *)
439 (*---------------vvvvvvvvvvvvvvvvvvvvvv---------------------------------------------------------*)
440 val t = @{term "3 * a + - 2 * a ::real"}; (*---------------------------------------------------*)
441 val t' = sort_variables t;
442 if UnparseC.term t' = "3 * a + - 2 * a" then ()
443 else error "sort_variables 3 * a + - 2 * a CHANGED";
445 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
446 val ll = map monom2list (poly2list t);
448 (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
449 (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*already correct order*)
450 (*+*) ] = map monom2list (poly2list t);
455 (*+*)val [ [Const ("Num.numeral_class.numeral", _) $ _, Free ("a", _)],
456 (*+*) [Const ("Groups.uminus_class.uminus", _) $ _, Free ("a", _)] (*ERROR: NO swap here*)
457 (*+*) ] = map sort_varList ll;
460 "~~~~~ val sort_varList , args:"; val (ts) = (nth 2 ll);
461 val sorted = sort var_ord ts;
463 (*+*)if UnparseC.terms ts = "[\"- 2\", \"a\"]" andalso UnparseC.terms sorted = "[\"- 2\", \"a\"]"
464 (*+*)then () else error "sort var_ord [\"- 2\", \"a\"] CHANGED";
467 (*+*)if UnparseC.term (nth 1 ts) = "- 2" andalso get_basStr (nth 1 ts) = "-2"
468 (*+*)then () else error "get_basStr - 2 CHANGED";
469 (*+*)if UnparseC.term (nth 2 ts) = "a" andalso get_basStr (nth 2 ts) = "a"
470 (*+*)then () else error "get_basStr a CHANGED";
473 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
474 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
475 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
476 (* indentation partially indicates call hierarchy:
477 "~~~~~ fun is_addUnordered
478 "~~~~~~~ fun is_polyexp
479 "~~~~~~~ fun sort_monoms
480 "~~~~~~~~~ fun sort_monList
481 "~~~~~~~~~~~ fun koeff_degree_ord
482 "~~~~~~~~~~~~~ fun degree_ord
483 "~~~~~~~~~~~~~~~ fun dict_cond_ord
484 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow
485 "~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
486 "~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
487 "~~~~~~~~~~~~~~~ fun monom_degree
488 "~~~~~~~~~~~~~ fun compare_koeff_ord
489 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon
490 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr
491 "~~~~~ fun is_multUnordered
492 "~~~~~~~ fun sort_variables
493 "~~~~~~~~~ fun sort_varList
494 "~~~~~~~~~~~ fun var_ord
495 "~~~~~~~~~~~~~ fun get_basStr used twice --^^
496 "~~~~~~~~~~~~~ fun get_potStr used twice --^^
498 val t = TermC.str2term "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
500 eval_is_addUnordered "xxx" "yyy" t @{theory};
501 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
502 (t as (Const("Poly.is_addUnordered", _) $ arg)), thy) =
503 ("xxx", "yyy", t, @{theory});
505 (*if*) is_addUnordered arg;
506 "~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
507 ((is_polyexp t) andalso not (t = sort_monoms t));
510 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
511 val ll = map monom2list (poly2list t);
515 "~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
518 sort koeff_degree_ord ll(*return value*);
519 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
520 koeff_degree_ord: term list * term list -> order;
521 (*we check all elements at once..*)
522 val eee1 = ll |> nth 1;
523 val eee2 = ll |> nth 2;
524 val eee3 = ll |> nth 3;
525 val eee3 = ll |> nth 3;
526 val eee4 = ll |> nth 4;
528 if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";
529 if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";
530 if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";
531 if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";
533 if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
534 if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
535 if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
536 if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
538 if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
539 if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
540 if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
541 if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
543 if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
544 if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
545 if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
546 if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
548 if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
549 if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
550 if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
551 if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
553 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
554 degree_ord: term list * term list -> order;
556 if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
557 if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
558 if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
559 if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
561 if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
562 if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
563 if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
564 if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
566 if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
567 if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
568 if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
569 if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
571 if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
572 if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
573 if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
574 if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
576 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
577 dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
578 dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
579 dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
580 val xxx = dict_cond_ord var_ord_revPow is_nums;
582 fun var_ord_revPow (a,b: term) =
583 (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};
584 @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
585 prod_ord string_ord string_ord_rev
586 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
588 if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
589 if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
590 if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
591 if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
592 (*-------------------------------------------------------------------------------------*)
593 if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
594 if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
595 if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
596 if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
597 (*-------------------------------------------------------------------------------------*)
598 if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
599 if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
600 if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
601 if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
602 (*-------------------------------------------------------------------------------------*)
603 if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
604 if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
605 if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
606 if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
607 (*-------------------------------------------------------------------------------------*)
609 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
610 (* we check all at once//*)
611 if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
612 if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
613 if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
614 if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
616 "~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
617 compare_koeff_ord: term list * term list -> order;
618 (* we check all at once//*)
619 if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
620 if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
621 if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
622 if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
624 if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
625 if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
626 if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
627 if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
629 if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
630 if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
631 if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
632 if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
634 if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
635 if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
636 if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
637 if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
639 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
640 get_koeff_of_mon: term list -> term option;
642 val SOME xxx1 = get_koeff_of_mon eee1;
643 val SOME xxx2 = get_koeff_of_mon eee2;
644 val SOME xxx3 = get_koeff_of_mon eee3;
645 val NONE = get_koeff_of_mon eee4;
647 if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
648 if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
649 if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
651 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
652 koeff2ordStr: term option -> string;
653 if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
654 if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
655 if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
656 if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
659 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
660 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
661 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
662 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
663 Rewrite.trace_on := false;
664 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
665 UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
666 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
667 else error "poly.sml: diff.behav. in make_polynomial 23";
670 ## rls: order_add_rls_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
671 ### rls: order_add_ on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y
672 ###### rls: Rule_Set.empty-is_addUnordered on: x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered
673 ####### try calc: "Poly.is_addUnordered"
674 ######## eval asms: "x \<up> 2 * y \<up> 2 + x \<up> 3 * y is_addUnordered = False" (*isa*)
676 ####### calc. to: False (*isa*)
679 if is_addUnordered (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real") then ()
680 else error"is_addUnordered x \<up> 2 * y \<up> 2 + x \<up> 3 * y"; (*isa == isa2*)
681 "~~~~~ fun is_addUnordered , args:"; val (t) = (TermC.str2term "x \<up> 2 * y \<up> 2 + x \<up> 3 * y ::real");
682 ((is_polyexp t) andalso not (t = sort_monoms t)) = false; (*isa == isa2*)
684 (*+*) if is_polyexp t = true then () else error "is_polyexp x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
686 (*+*) if t = sort_monoms t = false then () else error "sort_monoms 123";
687 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
688 val ll = map monom2list (poly2list t);
689 val lls = sort_monList ll;
691 (*+*)map UnparseC.terms lls = ["[\"x \<up> 2\", \"y \<up> 2\"]", "[\"x \<up> 3\", \"y\"]"]; (*isa*)
692 (*+*)map UnparseC.terms lls = ["[\"x \<up> 3\", \"y\"]", "[\"x \<up> 2\", \"y \<up> 2\"]"]; (*isa2*)
694 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val () = ();
695 (* we check all elements at once..*)
696 val eee1 = ll |> nth 1; UnparseC.terms eee1 = "[\"x \<up> 2\", \"y \<up> 2\"]";
697 val eee2 = ll |> nth 2; UnparseC.terms eee2 = "[\"x \<up> 3\", \"y\"]";
699 (*1*)if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
700 (*2*)if koeff_degree_ord (eee1, eee2) = GREATER then () else error "(eee1, eee2) CHANGED";
701 (*3*)if koeff_degree_ord (eee2, eee1) = LESS then () else error "(eee2, eee1) CHANGED"; (*isa*)
702 (*4*)if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee2) CHANGED";
704 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa == isa2*)
705 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa == isa2*)
706 (*1*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", sort_args = "(---, ---)"} (*isa == isa2*)
708 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa == isa2*)
710 (*3*)k{a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
712 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
713 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
714 (*4*){a = "compare_koeff_ord ", ats_bts = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", sort_args = "(---, ---)"} (*isa == isa2*)
718 val it = true: bool*)
720 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
721 (*1*)if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
722 (*2*)if degree_ord (eee1, eee2) = GREATER then () else error "degree_ord (eee1, eee2) CHANGED";(*isa*)
723 (*{a = "int_ord (4, 10003) = ", z = LESS} isa
724 {a = "int_ord (4, 4) = ", z = EQUAL} isa2*)
725 (*3*)if degree_ord (eee2, eee1) = LESS then () else error "degree_ord (eee2, eee1) CHANGED";(*isa*)
726 (*4*)if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee2) CHANGED";
728 (*1*){a = "int_ord (10002, 10002) = ", z = EQUAL} (*isa*)
729 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
730 (*1*){a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
731 (*1*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 2)", sort_args = "(x, 2), (x, 2)"} (*isa*)
732 (*1*){a = "dict_cond_ord", args = "([\"y \<up> 2\"], [\"y \<up> 2\"])", is_nums = "(false, false)"} (*isa*)
733 (*1*){a = "var_ord_revPow ", at_bt = "(y \<up> 2, y \<up> 2)", sort_args = "(y, 2), (y, 2)"} (*isa*)
734 (*1*){a = "dict_cond_ord ([], [])"} (*isa*)
736 (*2*){a = "int_ord (10002, 10003) = ", z = LESS} (*isa*)
737 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
738 {a = "dict_cond_ord", args = "([\"x \<up> 2\", \"y \<up> 2\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa2*)
739 (*2*){a = "var_ord_revPow ", at_bt = "(x \<up> 2, x \<up> 3)", sort_args = "(x, 2), (x, 3)"} (*isa2*)
741 (*3*){a = "int_ord (10003, 10002) = ", z = GREATER} (*isa*)
742 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
743 {a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 2\", \"y \<up> 2\"])", is_nums = "(false, false)"}
744 (*3*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 2)", sort_args = "(x, 3), (x, 2)"} (*isa == isa2*)
746 (*4*){a = "int_ord (10003, 10003) = ", z = EQUAL} (*isa*)
747 {a = "int_ord (4, 4) = ", z = EQUAL} (*isa2*)
748 (*4*){a = "dict_cond_ord", args = "([\"x \<up> 3\", \"y\"], [\"x \<up> 3\", \"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
749 (*4*){a = "var_ord_revPow ", at_bt = "(x \<up> 3, x \<up> 3)", sort_args = "(x, 3), (x, 3)"} (*isa == isa2*)
750 (*4*){a = "dict_cond_ord", args = "([\"y\"], [\"y\"])", is_nums = "(false, false)"} (*isa == isa2*)
751 (*4*){a = "var_ord_revPow ", at_bt = "(y, y)", sort_args = "(y, ---), (y, ---)"} (*isa == isa2*)
752 (*4*){a = "dict_cond_ord ([], [])"} (*isa == isa2*)
760 (*+*) if monom_degree eee1 = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
761 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee1);
762 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
763 (*if*) (is_nums x) (*else*);
764 val (Const ("Transcendental.powr", _) $ Free _ $ t) =
766 (*+*)UnparseC.term x = "x \<up> 2";
767 (*if*) TermC.is_num t (*then*);
769 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
770 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
771 (*if*) (is_nums x) (*else*);
772 val (Const ("Transcendental.powr", _) $ Free _ $ t) =
774 (*+*)UnparseC.term x = "y \<up> 2";
775 (*if*) TermC.is_num t (*then*);
778 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
779 if return = 4 then () else error "monom_degree [\"x \<up> 2\", \"y \<up> 2\"] CHANGED";
780 ( *---------------------------------------------------------------------------------OPEN local/*)
782 (*+*)if monom_degree eee2 = 4 andalso monom_degree eee2 = 4 then ()
783 else error "monom_degree [\"x \<up> 3\", \"y\"] CHANGED";
784 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val (l) = (eee2);
785 "~~~~~ fun counter , args:"; val (n, x :: xs) = (0, l); (*--------------------------OPEN local\* )
786 (*if*) (is_nums x) (*else*);
787 val (Const ("Transcendental.powr", _) $ Free _ $ t) =
789 (*+*)UnparseC.term x = "x \<up> 3";
790 (*if*) TermC.is_num t (*then*);
792 counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
793 "~~~~~ fun counter , args:"; val (n, x :: xs) = (t |> HOLogic.dest_number |> snd |> curry op + n, xs);
794 (*if*) (is_nums x) (*else*);
795 val _ = (*the default case*)
797 ( *---------------------------------------------------------------------------------OPEN local/*)
799 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
800 val xxx = dict_cond_ord var_ord_revPow is_nums;
801 (*1*)if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord (eee1, eee1) CHANGED";
802 (*2*)if xxx (eee1, eee2) = GREATER then () else error "dict_cond_ord (eee1, eee2) CHANGED";
803 (*3*)if xxx (eee2, eee1) = LESS then () else error "dict_cond_ord (eee2, eee1) CHANGED";
804 (*4*)if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord (eee2, eee2) CHANGED";
807 "-------- check make_polynomial with simple terms ----------------------------------------------";
808 "-------- check make_polynomial with simple terms ----------------------------------------------";
809 "-------- check make_polynomial with simple terms ----------------------------------------------";
811 val t = TermC.str2term "2*3*a";
812 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
813 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
816 val t = TermC.str2term "2*a + 3*a";
817 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
818 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
821 val t = TermC.str2term "2*a + 3*a + 3*a";
822 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
823 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
826 val t = TermC.str2term "3*a - 2*a";
827 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
828 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
831 val t = TermC.str2term "4*(3*a - 2*a)";
832 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
833 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
836 val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
837 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
838 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
840 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
841 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
842 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
843 val thy = @{theory "Isac_Knowledge"};
844 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
845 val t = TermC.str2term "x \<up> 2 * x";
846 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
847 if UnparseC.term t' = "x * x \<up> 2" then ()
848 else error "poly.sml Poly.is_multUnordered doesn't work";
850 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
851 ### 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) +
852 (-48 * x \<up> 4 + 8))
853 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
854 ####### try calc: Poly.is_multUnordered'
855 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
857 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))";
859 "----- is_multUnordered ---";
860 val tsort = sort_variables t;
861 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";
864 is_polyexp t andalso not (t = sort_variables t);
865 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
867 "----- eval_is_multUnordered ---";
868 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";
869 case eval_is_multUnordered "testid" "" tm thy of
870 SOME (_, Const ("HOL.Trueprop", _) $
871 (Const ("HOL.eq", _) $
872 (Const ("Poly.is_multUnordered", _) $ _) $
873 Const ("HOL.True", _))) => ()
874 | _ => error "poly.sml diff. eval_is_multUnordered";
876 "----- rewrite_set_ STILL DIDN'T WORK";
877 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
881 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
882 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
883 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
884 val thy = @{theory "Isac_Knowledge"};
885 val t as (_ $ arg) = TermC.str2term "(3 * a + - 2 * a) is_multUnordered";
887 (*+*)if UnparseC.term (sort_variables arg) = "3 * a + - 2 * a" andalso is_polyexp arg = true
888 (*+*) andalso not (is_multUnordered arg)
889 (*+*)then () else error "sort_variables 3 * a + - 2 * a CHANGED";
891 case eval_is_multUnordered "xxx " "yyy " t thy of
893 ("xxx 3 * a + - 2 * a_",
894 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
895 Const ("HOL.False", _))) => ()
896 (* Const ("HOL.True", _))) => () <<<<<--------------------------- this is false*)
897 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
899 "----- is_multUnordered --- (- 2 * a) is_multUnordered = False";
900 val t as (_ $ arg) = TermC.str2term "(- 2 * a) is_multUnordered";
902 (*+*)if UnparseC.term (sort_variables arg) = "- 2 * a" andalso is_polyexp arg = true
903 (*+*) andalso not (is_multUnordered arg)
904 (*+*)then () else error "sort_variables - 2 * a CHANGED";
906 case eval_is_multUnordered "xxx " "yyy " t thy of
909 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
910 Const ("HOL.False", _))) => ()
911 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
913 "----- is_multUnordered --- (a) is_multUnordered = False";
914 val t as (_ $ arg) = TermC.str2term "(a) is_multUnordered";
916 (*+*)if UnparseC.term (sort_variables arg) = "a" andalso is_polyexp arg = true
917 (*+*) andalso not (is_multUnordered arg)
918 (*+*)then () else error "sort_variables a CHANGED";
920 case eval_is_multUnordered "xxx " "yyy " t thy of
923 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
924 Const ("HOL.False", _))) => ()
925 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
927 "----- is_multUnordered --- (- 2) is_multUnordered = False";
928 val t as (_ $ arg) = TermC.str2term "(- 2) is_multUnordered";
930 (*+*)if UnparseC.term (sort_variables arg) = "- 2" andalso is_polyexp arg = true
931 (*+*) andalso not (is_multUnordered arg)
932 (*+*)then () else error "sort_variables - 2 CHANGED";
934 case eval_is_multUnordered "xxx " "yyy " t thy of
937 Const ("HOL.Trueprop", _) $ (Const ("HOL.eq", _) $ _ $
938 Const ("HOL.False", _))) => ()
939 | _ => error "eval_is_multUnordered 3 * a + -2 * a CHANGED";
942 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
943 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
944 "-------- fun is_multUnordered (x - a) \<up> 3 -----------------------------------------------------";
945 (* ca.line 45 of Rewrite.trace_on:
946 ## rls: order_mult_rls_ on:
947 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
948 ### rls: order_mult_ on:
949 x \<up> 3 + 3 * x \<up> 2 * (- 1 * a) + 3 * x * ((- 1) \<up> 2 * a \<up> 2) + (- 1) \<up> 3 * a \<up> 3
950 ###### rls: Rule_Set.empty-is_multUnordered on:
951 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
952 ####### try calc: "Poly.is_multUnordered"
954 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"
955 -------------------------------------------------------------------------------------------------==
956 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"
957 ####### calc. to: True
958 ####### try calc: "Poly.is_multUnordered"
959 ####### try calc: "Poly.is_multUnordered"
960 ### rls: order_mult_ on:
961 N:x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) + 3 * (a \<up> 2 * (x * (- 1) \<up> 2)) + a \<up> 3 * (- 1) \<up> 3
962 --------+--------------------------+---------------------------------+---------------------------<>
963 O:x \<up> 3 + -1 * (3 * (a * x \<up> 2)) + -1 \<up> 2 * (3 * (a \<up> 2 * x)) + -1 \<up> 3 * a \<up> 3
964 -------------------------------------------------------------------------------------------------<>
966 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";
968 "~~~~~ fun is_multUnordered
969 "~~~~~~~ fun sort_variables
970 "~~~~~~~~~ val sort_varList
972 "~~~~~ fun is_multUnordered , args:"; val (t) = (t);
977 (*+*)if UnparseC.term return =
978 (*+*) "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"
979 (*+*)then () else error "sort_variables x \<up> 3 + - 1 * (3 * (a * x \<up> 2)) .. CHANGED";
981 "~~~~~~~ fun sort_variables , args:"; val (t) = (t);
982 val ll = map monom2list (poly2list t);
983 val lls = map sort_varList ll;
985 (*+*)val ori3 = nth 3 ll;
986 (*+*)val mon3 = nth 3 lls;
988 (*+*)if UnparseC.terms (nth 1 ll) = "[\"x \<up> 3\"]" then () else error "nth 1 ll";
989 (*+*)if UnparseC.terms (nth 2 ll) = "[\"3\", \"x \<up> 2\", \"- 1\", \"a\"]" then () else error "nth 3 ll";
990 (*+*)if UnparseC.terms ori3 = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]" then () else error "nth 3 ll";
991 (*+*)if UnparseC.terms (nth 4 ll) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 ll";
993 (*+*)if UnparseC.terms (nth 1 lls) = "[\"x \<up> 3\"]" then () else error "nth 1 lls";
994 (*+*)if UnparseC.terms (nth 2 lls) = "[\"- 1\", \"3\", \"a\", \"x \<up> 2\"]" then () else error "nth 2 lls";
995 (*+*)if UnparseC.terms mon3 = "[\"(- 1) \<up> 2\", \"3\", \"a \<up> 2\", \"x\"]" then () else error "nth 3 lls";
996 (*+*)if UnparseC.terms (nth 4 lls) = "[\"(- 1) \<up> 3\", \"a \<up> 3\"]" then () else error "nth 4 lls";
998 "~~~~~~~~~ val sort_varList , args:"; val (ori3) = (ori3);
999 (* Output below with:
1000 val sort_varList = sort var_ord;
1001 fun var_ord (a,b: term) =
1002 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
1003 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
1004 prod_ord string_ord string_ord
1005 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
1008 (*+*)val xxx = sort_varList ori3;
1010 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa*)
1011 {a = "sort_varList", args = "[\"3\", \"x\", \"(- 1) \<up> 2\", \"a \<up> 2\"]"} (*isa2*)
1014 {a = "var_ord ", a_b = "(3, x)"} {a = "var_ord ", a_b = "(3, x)"}
1015 {sort_args = "(|||, ||||||), (x, ---)"} {sort_args = "(|||, ||||||), (x, ---)"}
1016 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
1017 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
1018 {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"} {a = "var_ord ", a_b = "((- 1) \<up> 2, a \<up> 2)"}
1019 {sort_args = "(|||, ||||||), (a, 2)"} {sort_args = "(|||, ||||||), (a, |||)"}
1022 {a = "var_ord ", a_b = "(x, a \<up> 2)"} {a = "var_ord ", a_b = "(x, a \<up> 2)"}
1023 {sort_args = "(x, ---), (a, 2)"} {sort_args = "(x, ---), (a, |||)"}
1025 {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(x, (- 1) \<up> 2)"}
1026 {sort_args = "(x, ---), (|||, ||||||)"} {sort_args = "(x, ---), (|||, ||||||)"}
1027 {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"} {a = "var_ord ", a_b = "(3, (- 1) \<up> 2)"}
1028 {sort_args = "(|||, ||||||), (|||, ||||||)"} {sort_args = "(|||, ||||||), (|||, ||||||)"}
1032 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1033 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1034 "-------- fun is_multUnordered b * a * a ------------------------------------------------------";
1035 val t = TermC.str2term "b * a * a";
1036 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1037 if UnparseC.term t = "a \<up> 2 * b" then ()
1038 else error "poly.sml: diff.behav. in make_polynomial 21";
1040 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
1041 ((is_polyexp t) andalso not (t = sort_variables t)) = true; (*isa == isa2*)
1043 (*+*)if is_polyexp t then () else error "is_polyexp a \<up> 2 * b CHANGED";
1044 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (t);
1045 (*if*) TermC.is_num num (*else*);
1047 "~~~~~ fun is_polyexp , args:"; val (Const ("Groups.times_class.times",_) $ num $ Free _) = (num);
1048 (*if*) TermC.is_num num (*else*);
1049 (*if*) TermC.is_variable num (*then*);
1051 val xxx = sort_variables t;
1052 (*+*)if UnparseC.term xxx = "a * (a * b)" then () else error "sort_variables a \<up> 2 * b CHANGED";
1055 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1056 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1057 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
1058 val t = TermC.str2term "2*3*a";
1059 val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
1060 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
1062 ## try calc: "Groups.times_class.times"
1063 ## rls: order_mult_rls_ on: 6 * a
1064 ### rls: order_mult_ on: 6 * a
1065 ###### rls: Rule_Set.empty-is_multUnordered on: 6 * a is_multUnordered
1066 ####### try calc: "Poly.is_multUnordered"
1067 ######## eval asms: "6 * a is_multUnordered = True" (*isa*)
1069 ####### calc. to: True (*isa*)
1072 val t = TermC.str2term "(6 * a) is_multUnordered";
1075 eval_is_multUnordered "xxx" () t @{theory};
1076 (*+*)if UnparseC.term t' = "6 * a is_multUnordered = False" then ()
1077 (*+*)else error "6 * a is_multUnordered = False CHANGED";
1079 "~~~~~ fun eval_is_multUnordered , args:"; val ((thmid:string), _,
1080 (t as (Const("Poly.is_multUnordered", _) $ arg)), thy) = ("xxx", (), t, @{theory});
1081 (*if*) is_multUnordered arg (*else*);
1083 "~~~~~ fun is_multUnordered , args:"; val (t) = (arg);
1085 ((is_polyexp t) andalso not (t = sort_variables t));
1087 (*+*)return = false; (*isa*)
1088 (*+*) is_polyexp t = true; (*isa*)
1089 (*+*) not (t = sort_variables t) = false; (*isa*)
1091 val xxx = sort_variables t;
1092 (*+*)if UnparseC.term xxx = "6 * a" then () else error "2*3*a is_multUnordered CHANGED";
1095 "-------- examples from textbook Schalk I ------------------------------------------------------";
1096 "-------- examples from textbook Schalk I ------------------------------------------------------";
1097 "-------- examples from textbook Schalk I ------------------------------------------------------";
1098 "-----SPB Schalk I p.63 No.267b ---";
1099 val t = TermC.str2term "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
1100 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1101 if UnparseC.term t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
1102 then () else error "poly.sml: diff.behav. in make_polynomial 1";
1104 "-----SPB Schalk I p.63 No.275b ---";
1105 val t = TermC.str2term "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
1106 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1107 if UnparseC.term t =
1108 "3 * x \<up> 4 + - 2 * x \<up> 3 * y + - 5 * x \<up> 2 * y \<up> 2 +\n4 * x * y \<up> 3 +\n- 2 * y \<up> 4"
1109 then () else error "poly.sml: diff.behav. in make_polynomial 2";
1111 "-----SPB Schalk I p.63 No.279b ---";
1112 val t = TermC.str2term "(x-a)*(x-b)*(x-c)*(x-d)";
1113 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1114 if UnparseC.term t =
1115 ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
1116 "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
1117 "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
1118 " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
1119 then () else error "poly.sml: diff.behav. in make_polynomial 3";
1122 "-----SPB Schalk I p.63 No.291 ---";
1123 val t = TermC.str2term "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
1124 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1125 if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
1126 then () else error "poly.sml: diff.behav. in make_polynomial 4";
1128 "-----SPB Schalk I p.64 No.295c ---";
1129 val t = TermC.str2term "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
1130 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1131 if UnparseC.term t =
1132 "169 * a \<up> 8 * b \<up> 18 * c \<up> 2 +\n- 312 * a \<up> 7 * b \<up> 15 * c \<up> 10 +\n144 * a \<up> 6 * b \<up> 12 * c \<up> 18"
1133 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
1135 "-----SPB Schalk I p.64 No.299a ---";
1136 val t = TermC.str2term "(x - y)*(x + y)";
1137 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1138 if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
1139 then () else error "poly.sml: diff.behav. in make_polynomial 6";
1141 "-----SPB Schalk I p.64 No.300c ---";
1142 val t = TermC.str2term "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
1143 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1144 if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
1145 then () else error "poly.sml: diff.behav. in make_polynomial 7";
1147 "-----SPB Schalk I p.64 No.302 ---";
1148 val t = TermC.str2term
1149 "(13*x \<up> 2 + 5)*(13*x \<up> 2 - 5) - (5*x \<up> 2 + 3)*(5*x \<up> 2 - 3) - (12*x \<up> 2 + 4)*(12*x \<up> 2 - 4)";
1150 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1151 if UnparseC.term t = "0"
1152 then () else error "poly.sml: diff.behav. in make_polynomial 8";
1153 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
1155 "-----SPB Schalk I p.64 No.306a ---";
1156 val t = TermC.str2term "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
1157 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1158 if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
1159 else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * -2 * x \<up> 4 = -2 * x \<up> 4";
1161 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
1162 the above resulted in the term below ... but reduces from then correctly*)
1163 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * -2 * x \<up> 4 + x \<up> 8";
1164 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1165 if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
1166 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
1168 "-----SPB Schalk I p.64 No.296a ---";
1169 val t = TermC.str2term "(x - a) \<up> 3";
1170 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1172 val NONE = eval_is_even "aaa" "bbb" (TermC.str2term "3::real") "ccc";
1174 if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
1175 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1177 "-----SPB Schalk I p.64 No.296c ---";
1178 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
1179 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1180 if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
1181 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1183 "-----SPB Schalk I p.62 No.242c ---";
1184 val t = TermC.str2term "x \<up> (-4)*(x \<up> (-4)*y \<up> (-2)) \<up> (-1)*y \<up> (-2)";
1185 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1186 if UnparseC.term t = "1"
1187 then () else error "poly.sml: diff.behav. in make_polynomial 12";
1189 "-----SPB Schalk I p.60 No.209a ---";
1190 val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
1191 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1192 if UnparseC.term t = "a \<up> 7"
1193 then () else error "poly.sml: diff.behav. in make_polynomial 13";
1195 "-----SPB Schalk I p.60 No.209d ---";
1196 val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
1197 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1198 if UnparseC.term t = "d \<up> 3"
1199 then () else error "poly.sml: diff.behav. in make_polynomial 14";
1201 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1202 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1203 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
1204 "-----Schalk I p.64 No.303 ---";
1205 val t = TermC.str2term "(a + 2*b)*(a \<up> 2 + 4*b \<up> 2)*(a - 2*b) - (a - 6*b)*(a \<up> 2 + 36*b \<up> 2)*(a + 6*b)";
1206 (*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
1207 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1208 if UnparseC.term t = "1280 * b \<up> 4"
1209 then () else error "poly.sml: diff.behav. in make_polynomial 14b";
1210 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
1211 (*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
1213 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1214 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1215 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
1217 val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1218 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1219 if UnparseC.term t = "1" then ()
1220 else error "poly.sml: diff.behav. in make_polynomial 15";
1222 val t = TermC.str2term "a + a + a";
1223 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1224 if UnparseC.term t = "3 * a" then ()
1225 else error "poly.sml: diff.behav. in make_polynomial 16";
1227 val t = TermC.str2term "a + b + b + b";
1228 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1229 if UnparseC.term t = "a + 3 * b" then ()
1230 else error "poly.sml: diff.behav. in make_polynomial 17";
1232 val t = TermC.str2term "a \<up> 2*b*b \<up> (-1)";
1233 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1234 if UnparseC.term t = "a \<up> 2" then ()
1235 else error "poly.sml: diff.behav. in make_polynomial 18";
1237 val t = TermC.str2term "a \<up> 2*a \<up> (-2)";
1238 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1239 if (UnparseC.term t) = "1" then ()
1240 else error "poly.sml: diff.behav. in make_polynomial 19";
1242 val t = TermC.str2term "b + a - b";
1243 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1244 if (UnparseC.term t) = "a" then ()
1245 else error "poly.sml: diff.behav. in make_polynomial 20";
1247 val t = TermC.str2term "b * a * a";
1248 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1249 if UnparseC.term t = "a \<up> 2 * b" then ()
1250 else error "poly.sml: diff.behav. in make_polynomial 21";
1252 val t = TermC.str2term "(a \<up> 2) \<up> 3";
1253 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1254 if UnparseC.term t = "a \<up> 6" then ()
1255 else error "poly.sml: diff.behav. in make_polynomial 22";
1257 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
1258 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
1259 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
1260 else error "poly.sml: diff.behav. in make_polynomial 23";
1262 val t = (Thm.term_of o the o (TermC.parse thy)) "a \<up> 2 * (-a) \<up> 2";
1263 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1264 if (UnparseC.term t) = "a \<up> 4" then ()
1265 else error "poly.sml: diff.behav. in make_polynomial 24";
1267 val t = TermC.str2term "a * b * b \<up> (-1) + a";
1268 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1269 if UnparseC.term t = "2 * a" then ()
1270 else error "poly.sml: diff.behav. in make_polynomial 25";
1272 val t = TermC.str2term "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
1273 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
1274 if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
1275 then () else error "poly.sml: diff.behav. in make_polynomial 26";
1277 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
1279 val t = TermC.str2term "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
1280 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
1281 if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
1282 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
1284 val t = TermC.str2term "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
1285 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t;
1286 if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
1287 then () else error "poly.sml: diff.behav. in make_polynomial 28";
1289 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
1290 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
1291 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
1292 val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
1294 case Refine.refine fmz ["polynomial", "simplification"] of
1295 [M_Match.Matches (["polynomial", "simplification"], _)] => ()
1296 | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
1297 (*...if there is an error, then ...*)
1300 (*default_print_depth 7;*)
1301 val pbt = Problem.from_store ["polynomial", "simplification"];
1302 (*default_print_depth 3;*)
1304 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
1305 ... then Rewrite.trace_on:*)
1308 Rewrite.trace_on := false;
1309 M_Match.match_pbl fmz pbt;
1310 Rewrite.trace_on := false;
1311 (*... if there is no rewrite, then there is something wrong with prls*)
1314 (*default_print_depth 7;*)
1315 val prls = (#prls o Problem.from_store) ["polynomial", "simplification"];
1316 (*default_print_depth 3;*)
1317 val t = TermC.str2term "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
1318 val SOME (t',_) = rewrite_set_ thy false prls t;
1319 if t' = @{term True} then ()
1320 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
1321 (*... if this works, but --1-- does still NOT work, check types:*)
1324 (*show_types:=true;*)
1326 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
1327 val wh = [False "(t_::real => real) (is_polyexp::real)"]
1328 ...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
1329 val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
1330 (*show_types:=false;*)
1333 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1334 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1335 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
1336 val fmz = ["Term ((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1))", "normalform N"];
1338 ("Poly",["polynomial", "simplification"],
1339 ["simplification", "for_polynomials"]);
1340 val p = e_pos'; val c = [];
1341 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1342 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1))"*)
1343 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
1345 (*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
1346 (*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n (3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)) ,(t_t, [(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)]))]"
1347 (*+*)then () else error "No.267b: I_Model.T CHANGED";
1348 ( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
1350 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
1351 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
1352 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
1353 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
1354 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
1356 (*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
1357 (*+*)then () else error "";
1359 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
1361 (*+*)if f2str f = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
1362 (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b -1";
1364 (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
1368 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
1369 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
1370 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
1373 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],
1374 ("Poly",["polynomial", "simplification"],
1375 ["simplification", "for_polynomials"]))];
1378 autoCalculate 1 CompleteCalc;
1379 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1381 interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
1382 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1383 if existpt' ([1,1], Frm) pt then ()
1384 else error "poly.sml: interSteps doesnt work again 1";
1386 interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
1387 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
1388 (*============ inhibit exn WN120316 ==============================================
1389 if existpt' ([1,1,1], Frm) pt then ()
1390 else error "poly.sml: interSteps doesnt work again 2";
1391 ============ inhibit exn WN120316 ==============================================*)
1393 "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1394 "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1395 "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
1396 val thy = @{theory AlgEin};
1398 val SOME (f',_) = rewrite_set_ thy false norm_Poly
1399 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
1400 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
1401 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
1402 else error "norm_Poly changed behavior";
1404 ## rls: order_add_rls_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
1405 ### rls: order_add_ on: L = k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht + oben
1406 ###### rls: Rule_Set.empty-is_addUnordered on: k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
1407 oben is_addUnordered
1408 ####### try calc: "Poly.is_addUnordered"
1409 ######## eval asms: "k + - 2 * q + k + - 2 * q + k + - 2 * q + k + - 2 * q + senkrecht +
1410 oben is_addUnordered = True"
1411 ####### calc. to: True
1412 ####### try calc: "Poly.is_addUnordered"
1413 ####### try calc: "Poly.is_addUnordered"
1414 ### rls: order_add_ on: L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben
1416 "~~~~~ fun sort_monoms , args:"; val (t) =
1417 (TermC.str2term "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben");
1420 (*+*)UnparseC.term t' = "L = k + k + k + k + - 2 * q + - 2 * q + - 2 * q + - 2 * q + senkrecht + oben"; (*isa*)
1422 "-------- ord_make_polynomial ------------------------------------------------------------------";
1423 "-------- ord_make_polynomial ------------------------------------------------------------------";
1424 "-------- ord_make_polynomial ------------------------------------------------------------------";
1425 val t1 = TermC.str2term "2 * b + (3 * a + 3 * b)";
1426 val t2 = TermC.str2term "(3 * a + 3 * b) + 2 * b";
1428 if ord_make_polynomial true thy [] (t1, t2) then ()
1429 else error "poly.sml: diff.behav. in ord_make_polynomial";
1430 (*SO: WHY IS THERE NO REWRITING ...*)
1432 val term = TermC.str2term "2*b + (3*a + 3*b)";
1433 (*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term;
1435 WHY IS THERE NO REWRITING ?!?
1436 most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
1437 while order_add_mult uses isac's rewriter -- and this is used rarely!