1 (* testexamples for Poly, polynomials
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 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
17 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
18 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
19 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
20 "-------- examples from textbook Schalk I ------------------------------------------------------";
21 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
22 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
23 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
24 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
25 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
26 "-------- norm_Poly NOT COMPLETE ---------------------------------------------------------------";
27 "-------- ord_make_polynomial ------------------------------------------------------------------";
28 "-----------------------------------------------------------------------------------------------";
29 "-----------------------------------------------------------------------------------------------";
30 "-----------------------------------------------------------------------------------------------";
33 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
34 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
35 "-------- survey on parallel rewrite-breakers AND code with @{print} ---------------------------";
36 (* indentation indicates call hierarchy:
37 "~~~~~ fun is_addUnordered
38 "~~~~~~~ fun is_polyexp
39 "~~~~~~~ fun sort_monoms
40 "~~~~~~~~~ fun sort_monList
41 "~~~~~~~~~~~ fun koeff_degree_ord : term list * term list -> order
42 "~~~~~~~~~~~~~ fun degree_ord : term list * term list -> order
43 "~~~~~~~~~~~~~~~ fun dict_cond_ord : ('a * 'a -> order) -> ('a -> bool) -> 'a list * 'a list -> order
44 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow: term * term -> order
45 "~~~~~~~~~~~~~~~~~~~ fun get_basStr : term -> string used twice --vv
46 "~~~~~~~~~~~~~~~~~~~ fun get_potStr : term -> string used twice --vv
47 "~~~~~~~~~~~~~~~ fun monom_degree : term list -> int
48 "~~~~~~~~~~~~~ fun compare_koeff_ord : term list * term list -> order
49 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon: term list -> term option
50 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr : term option -> string
51 "~~~~~ fun is_multUnordered
52 "~~~~~~~ fun sort_variables
53 "~~~~~~~~~ fun sort_varList
54 "~~~~~~~~~~~ fun var_ord
55 "~~~~~~~~~~~~~ fun get_basStr used twice --^^
56 "~~~~~~~~~~~~~ fun get_potStr used twice --^^
58 fun int_ord (i1, i2) =
59 (@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
63 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
64 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
65 prod_ord string_ord string_ord
66 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
68 fun var_ord_revPow (a, b: term) =
69 (@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
70 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
71 prod_ord string_ord string_ord_rev
72 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
75 (@{print} {a = "sort_varList", args = UnparseC.terms ts};
78 fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
79 | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
80 | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
81 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
82 (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms (x :: xs) ^ ", " ^ UnparseC.terms (y :: ys) ^ ")",
83 is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
84 case (cond x, cond y) of
86 (case elem_ord (x, y) of
87 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
89 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
90 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
91 | (true, true) => dict_cond_ord elem_ord cond (xs, ys)
93 fun compare_koeff_ord (xs, ys) =
94 (@{print} {a = "compare_koeff_ord ", ats_bts = "(" ^ UnparseC.terms xs ^ ", " ^ UnparseC.terms ys ^ ")",
95 sort_args = "(" ^ (koeff2ordStr o get_koeff_of_mon) xs ^ ", " ^ (koeff2ordStr o get_koeff_of_mon) ys ^ ")"};
97 ((koeff2ordStr o get_koeff_of_mon) xs,
98 (koeff2ordStr o get_koeff_of_mon) ys)
100 fun var_ord (a,b: term) =
101 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")",
102 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
103 prod_ord string_ord string_ord
104 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
109 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
110 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
111 "-------- thm sym_real_mult_minus1 loops with new numerals -------------------------------------";
112 (* thus ^^^^^^^^^^^^^^^^^^^^^^^^ excluded from rls.
114 sym_real_mult_minus1 = "- ?z = - 1 * ?z" *)
115 @{thm real_mult_minus1}; (* = "- 1 * ?z = - ?z" *)
116 val thm_isac = ThmC.sym_thm @{thm real_mult_minus1}; (* = "- ?z = - 1 * ?z" *)
117 val SOME t_isac = TermC.parseNEW @{context} "3 * a + - 1 * (2 * a):: real";
119 val SOME (t', []) = rewrite_ @{context} tless_true Rule_Set.empty true thm_isac t_isac;
120 if UnparseC.term t' = "3 * a + - 1 * 1 * (2 * a)" then ((*thm did NOT apply to Free ("- 1", _)*))
121 else error "thm - ?z = - 1 * ?z loops with new numerals";
124 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
125 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
126 "-------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) ----------------------------";
127 val thy = Proof_Context.init_global @{theory Partial_Fractions}
128 val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
129 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
131 val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
132 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
134 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
135 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
136 "-------- eval_ for is_expanded_in, is_poly_in, has_degree_in ----------------------------------";
137 val t = TermC.parseNEW' thy "(-8 - 2*x + x \<up> 2) is_expanded_in x";
138 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
139 if UnparseC.term t' = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
140 andalso id = "- 8 - 2 * x + x \<up> 2 is_expanded_in x = True"
141 then () else error "eval_is_expanded_in x ..changed";
143 val thy = Proof_Context.init_global @{theory Partial_Fractions}
144 val t = TermC.parseNEW' thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
145 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
146 if UnparseC.term t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
147 andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
148 then () else error "eval_is_expanded_in AA ..changed";
151 val t = TermC.parseNEW' thy "(8 + 2*x + x \<up> 2) is_poly_in x";
152 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
153 if UnparseC.term t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
154 andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
155 then () else error "is_poly_in x ..changed";
157 val t = TermC.parseNEW' thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
158 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
159 if UnparseC.term t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
160 andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
161 then () else error "is_poly_in AA ..changed";
164 val thy = Proof_Context.init_global @{theory Partial_Fractions}
165 val expr = TermC.parseNEW' thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
166 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
168 val expr = TermC.parseNEW' thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
169 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
171 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
172 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
173 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
174 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
177 *** Const (HOL.Trueprop, bool => prop)
178 *** . Const (HOL.eq, real => real => bool)
179 *** . . Const (Groups.minus_class.minus, real => real => real)
180 *** . . . Const (Groups.zero_class.zero, real)
181 *** . . . Var ((x, 0), real)
182 *** . . Const (Groups.uminus_class.uminus, real => real)
183 *** . . . Var ((x, 0), real)
186 Const (\<^const_name>\<open>Trueprop\<close>, _) $
187 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
188 (Const (\<^const_name>\<open>minus\<close>, _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _) $
190 (Const (\<^const_name>\<open>uminus\<close>, _) $ Var (("x", 0), _))) => ()
191 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
194 val t = TermC.parseNEW' thy "- 1";
202 Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
203 | _ => error "internal representation of \"- 1\" changed";
205 "======= these external values all have the same internal representation";
206 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
207 (*----------------------------------- vvvvv -------------------------------------------*)
208 val t = TermC.parseNEW' thy "-x";
211 *** Free ( -x, real)*)
213 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
214 | _ => error "internal representation of \"-x\" changed";
215 (*----------------------------------- vvvvv -------------------------------------------*)
216 val t = TermC.parseNEW' thy "- x";
219 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
221 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
222 | _ => error "internal representation of \"- x\" changed";
223 (*----------------------------------- vvvvvv ------------------------------------------*)
224 val t = TermC.parseNEW' thy "-(x)";
227 *** Free ( -x, real)*)
229 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
230 | _ => error "internal representation of \"-(x)\" changed";
233 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
234 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
235 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
236 (* indentation partially indicates call hierarchy:
237 "~~~~~ fun is_addUnordered
238 "~~~~~~~ fun is_polyexp
239 "~~~~~~~ fun sort_monoms
240 "~~~~~~~~~ fun sort_monList
241 "~~~~~~~~~~~ fun koeff_degree_ord
242 "~~~~~~~~~~~~~ fun degree_ord
243 "~~~~~~~~~~~~~~~ fun dict_cond_ord
244 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow
245 "~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
246 "~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
247 "~~~~~~~~~~~~~~~ fun monom_degree
248 "~~~~~~~~~~~~~ fun compare_koeff_ord
249 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon
250 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr
251 "~~~~~ fun is_multUnordered
252 "~~~~~~~ fun sort_variables
253 "~~~~~~~~~ fun sort_varList
254 "~~~~~~~~~~~ fun var_ord
255 "~~~~~~~~~~~~~ fun get_basStr used twice --^^
256 "~~~~~~~~~~~~~ fun get_potStr used twice --^^
258 val t = TermC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
260 eval_is_addUnordered "xxx" "yyy" t @{context};
261 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
262 (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =
263 ("xxx", "yyy", t, @{context});
265 (*if*) is_addUnordered arg;
266 "~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
267 ((is_polyexp t) andalso not (t = sort_monoms t));
270 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
271 val ll = map monom2list (poly2list t);
275 "~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
278 sort koeff_degree_ord ll(*return value*);
279 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
280 koeff_degree_ord: term list * term list -> order;
281 (*we check all elements at once..*)
282 val eee1 = ll |> nth 1;
283 val eee2 = ll |> nth 2;
284 val eee3 = ll |> nth 3;
285 val eee3 = ll |> nth 3;
286 val eee4 = ll |> nth 4;
288 if UnparseC.terms eee1 = "[\"1\"]" then () else error "eee1 CHANGED";
289 if UnparseC.terms eee2 = "[\"2\", \"x \<up> 4\"]" then () else error "eee2 CHANGED";
290 if UnparseC.terms eee3 = "[\"- 4\", \"x \<up> 4\"]" then () else error "eee3 CHANGED";
291 if UnparseC.terms eee4 = "[\"x \<up> 8\"]" then () else error "eee4 CHANGED";
293 if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
294 if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
295 if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
296 if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
298 if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
299 if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
300 if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
301 if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
303 if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
304 if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
305 if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
306 if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
308 if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
309 if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
310 if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
311 if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
313 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
314 degree_ord: term list * term list -> order;
316 if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
317 if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
318 if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
319 if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
321 if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
322 if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
323 if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
324 if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
326 if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
327 if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
328 if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
329 if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
331 if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
332 if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
333 if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
334 if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
336 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
337 dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
338 dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
339 dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
340 val xxx = dict_cond_ord var_ord_revPow is_nums;
342 fun var_ord_revPow (a,b: term) =
343 (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term a ^ ", " ^ UnparseC.term b ^ ")"};
344 @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
345 prod_ord string_ord string_ord_rev
346 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
348 if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
349 if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
350 if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
351 if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
352 (*-------------------------------------------------------------------------------------*)
353 if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
354 if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
355 if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
356 if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
357 (*-------------------------------------------------------------------------------------*)
358 if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
359 if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
360 if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
361 if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
362 (*-------------------------------------------------------------------------------------*)
363 if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
364 if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
365 if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
366 if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
367 (*-------------------------------------------------------------------------------------*)
369 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
370 (* we check all at once//*)
371 if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
372 if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
373 if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
374 if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
376 "~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
377 compare_koeff_ord: term list * term list -> order;
378 (* we check all at once//*)
379 if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
380 if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
381 if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
382 if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
384 if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
385 if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
386 if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
387 if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
389 if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
390 if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
391 if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
392 if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
394 if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
395 if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
396 if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
397 if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
399 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
400 get_koeff_of_mon: term list -> term option;
402 val SOME xxx1 = get_koeff_of_mon eee1;
403 val SOME xxx2 = get_koeff_of_mon eee2;
404 val SOME xxx3 = get_koeff_of_mon eee3;
405 val NONE = get_koeff_of_mon eee4;
407 if UnparseC.term xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
408 if UnparseC.term xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
409 if UnparseC.term xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
411 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
412 koeff2ordStr: term option -> string;
413 if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
414 if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
415 if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
416 if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
419 "-------- examples from textbook Schalk I ------------------------------------------------------";
420 "-------- examples from textbook Schalk I ------------------------------------------------------";
421 "-------- examples from textbook Schalk I ------------------------------------------------------";
422 "-----SPB Schalk I p.63 No.267b ---";
423 val t = TermC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
424 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
425 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"
426 then () else error "poly.sml: diff.behav. in make_polynomial 1";
428 "-----SPB Schalk I p.63 No.275b ---";
429 val t = TermC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
430 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
432 "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"
433 then () else error "poly.sml: diff.behav. in make_polynomial 2";
435 "-----SPB Schalk I p.63 No.279b ---";
436 val t = TermC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";
437 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
439 ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
440 "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
441 "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
442 " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
443 then () else error "poly.sml: diff.behav. in make_polynomial 3";
446 "-----SPB Schalk I p.63 No.291 ---";
447 val t = TermC.parse_test @{context} "(5+96*x \<up> 3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (- 15*x*(-8*x- 5)))";
448 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
449 if UnparseC.term t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
450 then () else error "poly.sml: diff.behav. in make_polynomial 4";
452 "-----SPB Schalk I p.64 No.295c ---";
453 val t = TermC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
454 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
456 "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"
457 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
459 "-----SPB Schalk I p.64 No.299a ---";
460 val t = TermC.parse_test @{context} "(x - y)*(x + y)";
461 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
462 if UnparseC.term t = "x \<up> 2 + - 1 * y \<up> 2"
463 then () else error "poly.sml: diff.behav. in make_polynomial 6";
465 "-----SPB Schalk I p.64 No.300c ---";
466 val t = TermC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
467 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
468 if UnparseC.term t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
469 then () else error "poly.sml: diff.behav. in make_polynomial 7";
471 "-----SPB Schalk I p.64 No.302 ---";
472 val t = TermC.parse_test @{context}
473 "(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)";
474 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
475 if UnparseC.term t = "0"
476 then () else error "poly.sml: diff.behav. in make_polynomial 8";
477 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
479 "-----SPB Schalk I p.64 No.306a ---";
480 val t = TermC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
481 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
482 if UnparseC.term t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
483 else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 = - 2 * x \<up> 4";
485 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
486 the above resulted in the term below ... but reduces from then correctly*)
487 val t = TermC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
488 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
489 if UnparseC.term t = "1 + - 2 * x \<up> 4 + x \<up> 8"
490 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
492 "-----SPB Schalk I p.64 No.296a ---";
493 val t = TermC.parse_test @{context} "(x - a) \<up> 3";
494 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
496 val NONE = eval_is_even "aaa" "bbb" (TermC.parse_test @{context} "3::real") "ccc";
498 if UnparseC.term t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
499 then () else error "poly.sml: diff.behav. in make_polynomial 10";
501 "-----SPB Schalk I p.64 No.296c ---";
502 val t = TermC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
503 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
504 if UnparseC.term t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
505 then () else error "poly.sml: diff.behav. in make_polynomial 11";
507 "-----SPB Schalk I p.62 No.242c ---";
508 val t = TermC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
509 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
510 if UnparseC.term t = "1"
511 then () else error "poly.sml: diff.behav. in make_polynomial 12";
513 "-----SPB Schalk I p.60 No.209a ---";
514 val t = TermC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
515 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
516 if UnparseC.term t = "a \<up> 7"
517 then () else error "poly.sml: diff.behav. in make_polynomial 13";
519 "-----SPB Schalk I p.60 No.209d ---";
520 val t = TermC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
521 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
522 if UnparseC.term t = "d \<up> 3"
523 then () else error "poly.sml: diff.behav. in make_polynomial 14";
525 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
526 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
527 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
528 "-----Schalk I p.64 No.303 ---";
529 val t = TermC.parse_test @{context} "(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)";
530 (*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
531 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
532 if UnparseC.term t = "1280 * b \<up> 4"
533 then () else error "poly.sml: diff.behav. in make_polynomial 14b";
534 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
535 (*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
537 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
538 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
539 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
541 val t = TermC.parse_test @{context} "a + a + a";
542 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
543 if UnparseC.term t = "3 * a" then ()
544 else error "poly.sml: diff.behav. in make_polynomial 16";
546 val t = TermC.parse_test @{context} "a + b + b + b";
547 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
548 if UnparseC.term t = "a + 3 * b" then ()
549 else error "poly.sml: diff.behav. in make_polynomial 17";
551 val t = TermC.parse_test @{context} "b * a * a";
552 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
553 if UnparseC.term t = "a \<up> 2 * b" then ()
554 else error "poly.sml: diff.behav. in make_polynomial 21";
556 val t = TermC.parse_test @{context} "(a \<up> 2) \<up> 3";
557 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
558 if UnparseC.term t = "a \<up> 6" then ()
559 else error "poly.sml: diff.behav. in make_polynomial 22";
561 val t = TermC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
562 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
563 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
564 else error "poly.sml: diff.behav. in make_polynomial 23";
566 val t = TermC.parse_test @{context} "a * b * b \<up> (- 1) + a";
567 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
568 if UnparseC.term t = "2 * a" then ()
569 else error "poly.sml: diff.behav. in make_polynomial 25";
571 val t = TermC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
572 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term t;
573 if UnparseC.term t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
574 then () else error "poly.sml: diff.behav. in make_polynomial 26";
576 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
578 val t = TermC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
579 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
580 if UnparseC.term t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
581 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
583 val t = TermC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
584 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
585 if UnparseC.term t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
586 then () else error "poly.sml: diff.behav. in make_polynomial 28";
588 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
589 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
590 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
591 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"];
593 case Refine.refine_PIDE @{context} fmz ["polynomial", "simplification"] of
594 [M_Match.Matches (["polynomial", "simplification"], _)] => ()
595 | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
596 (*...if there is an error, then ...*)
599 (*default_print_depth 7;*)
600 val pbt = Problem.from_store @{context} ["polynomial", "simplification"];
601 (*default_print_depth 3;*)
603 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
604 ... then Rewrite.trace_on:*)
607 M_Match.match_pbl fmz pbt;
608 (*... if there is no rewrite, then there is something wrong with prls*)
611 (*default_print_depth 7;*)
612 val prls = (#prls o Problem.from_store @{context}) ["polynomial", "simplification"];
613 (*default_print_depth 3;*)
614 val t = TermC.parse_test @{context} "((5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)) is_polyexp";
615 val SOME (t',_) = rewrite_set_ thy false prls t;
616 if t' = @{term True} then ()
617 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
618 (*... if this works, but -- 1-- does still NOT work, check types:*)
621 (*show_types:=true;*)
623 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
624 val wh = [False "(t_::real => real) (is_polyexp::real)"]
625 ...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
626 val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
627 (*show_types:=false;*)
630 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
631 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
632 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
633 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"];
635 ("Poly",["polynomial", "simplification"],
636 ["simplification", "for_polynomials"]);
637 val p = e_pos'; val c = [];
638 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
639 (*[], 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))"*)
640 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
642 (*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
643 (*+*) "[\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)]))]"
644 (*+*)then () else error "No.267b: I_Model.T CHANGED";
645 ( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
647 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
648 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
649 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
650 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
651 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
653 (*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
654 (*+*)then () else error "";
656 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
658 (*+*)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"
659 (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b - 1";
661 (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
665 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
666 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
667 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
670 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],
671 ("Poly",["polynomial", "simplification"],
672 ["simplification", "for_polynomials"]))];
675 autoCalculate 1 CompleteCalc;
676 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
678 interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
679 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
680 if existpt' ([1,1], Frm) pt then ()
681 else error "poly.sml: interSteps doesnt work again 1";
683 interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
684 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
685 (*============ inhibit exn WN120316 ==============================================
686 if existpt' ([1,1,1], Frm) pt then ()
687 else error "poly.sml: interSteps doesnt work again 2";
688 ============ inhibit exn WN120316 ==============================================*)
690 "-------- ord_make_polynomial ------------------------------------------------------------------";
691 "-------- ord_make_polynomial ------------------------------------------------------------------";
692 "-------- ord_make_polynomial ------------------------------------------------------------------";
693 val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
694 val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
696 if ord_make_polynomial true @{theory} [] (t1, t2) then ()
697 else error "poly.sml: diff.behav. in ord_make_polynomial";
698 (*SO: WHY IS THERE NO REWRITING ...*)
700 val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)";
701 (*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;
703 WHY IS THERE NO REWRITING ?!?
704 most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
705 while order_add_mult uses isac's rewriter -- and this is used rarely!