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 @{context} a ^ ", " ^ UnparseC.term @{context} 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 @{context} a ^ ", " ^ UnparseC.term @{context} 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 @{context} 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 @{context} (x :: xs) ^ ", " ^ UnparseC.terms @{context} (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 @{context} xs ^ ", " ^ UnparseC.terms @{context} 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 @{context} a ^ ", " ^ UnparseC.term @{context} 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 = ParseC.term_opt @{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 @{context} 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 = ParseC.parse_test 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 = ParseC.parse_test 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 = ParseC.parse_test 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 @{context} 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 = ParseC.parse_test thy "(-8 - 2*AA + AA \<up> 2) is_expanded_in AA";
145 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
147 "- 8 - 2 * ??.Partial_Fractions.AA +\n??.Partial_Fractions.AA \<up> 2 is_expanded_in ??.Partial_Fractions.AA = True"*)
148 (*/----------- eval_is_expanded_in needs ctxt in order to know ??.Partial_Fractions -----------\* )
149 if UnparseC.term @{context} t' = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
150 andalso id = "- 8 - 2 * AA + AA \<up> 2 is_expanded_in AA = True"
151 then () else error "eval_is_expanded_in AA ..changed";
153 val t = ParseC.parse_test thy "(8 + 2*x + x \<up> 2) is_poly_in x";
154 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
155 if UnparseC.term @{context} t' = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
156 andalso id = "8 + 2 * x + x \<up> 2 is_poly_in x = True"
157 then () else error "is_poly_in x ..changed";
159 val t = ParseC.parse_test thy "(8 + 2*AA + AA \<up> 2) is_poly_in AA";
160 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
161 if UnparseC.term @{context} t' = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
162 andalso id = "8 + 2 * AA + AA \<up> 2 is_poly_in AA = True"
163 then () else error "is_poly_in AA ..changed";
164 ( *\----------- eval_is_expanded_in needs ctxt in order to know ??.Partial_Fractions -----------/*)
166 val thy = Proof_Context.init_global @{theory Partial_Fractions}
167 val expr = ParseC.parse_test thy "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
168 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
170 val expr = ParseC.parse_test thy "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
171 val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
173 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
174 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
175 "-------- investigate (new 2002) uniary minus --------------------------------------------------";
176 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
177 TermC.atom_trace_detail @{context} t;
179 *** Const (HOL.Trueprop, bool => prop)
180 *** . Const (HOL.eq, real => real => bool)
181 *** . . Const (Groups.minus_class.minus, real => real => real)
182 *** . . . Const (Groups.zero_class.zero, real)
183 *** . . . Var ((x, 0), real)
184 *** . . Const (Groups.uminus_class.uminus, real => real)
185 *** . . . Var ((x, 0), real)
188 Const (\<^const_name>\<open>Trueprop\<close>, _) $
189 (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
190 (Const (\<^const_name>\<open>minus\<close>, _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _) $
192 (Const (\<^const_name>\<open>uminus\<close>, _) $ Var (("x", 0), _))) => ()
193 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
196 val t = ParseC.parse_test thy "- 1";
197 TermC.atom_trace_detail @{context} t;
204 Const (\<^const_name>\<open>uminus\<close>, _) $ Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
205 | _ => error "internal representation of \"- 1\" changed";
207 "======= these external values all have the same internal representation";
208 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
209 (*----------------------------------- vvvvv -------------------------------------------*)
210 val t = ParseC.parse_test thy "-x";
211 TermC.atom_trace_detail @{context} t;
213 *** Free ( -x, real)*)
215 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
216 | _ => error "internal representation of \"-x\" changed";
217 (*----------------------------------- vvvvv -------------------------------------------*)
218 val t = ParseC.parse_test thy "- x";
219 TermC.atom_trace_detail @{context} t;
221 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
223 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
224 | _ => error "internal representation of \"- x\" changed";
225 (*----------------------------------- vvvvvv ------------------------------------------*)
226 val t = ParseC.parse_test thy "-(x)";
227 TermC.atom_trace_detail @{context} t;
229 *** Free ( -x, real)*)
231 Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
232 | _ => error "internal representation of \"-(x)\" changed";
235 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
236 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
237 "-------- rebuild fun is_addUnordered (1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) ---------------------";
238 (* indentation partially indicates call hierarchy:
239 "~~~~~ fun is_addUnordered
240 "~~~~~~~ fun is_polyexp
241 "~~~~~~~ fun sort_monoms
242 "~~~~~~~~~ fun sort_monList
243 "~~~~~~~~~~~ fun koeff_degree_ord
244 "~~~~~~~~~~~~~ fun degree_ord
245 "~~~~~~~~~~~~~~~ fun dict_cond_ord
246 "~~~~~~~~~~~~~~~~~ fun var_ord_revPow
247 "~~~~~~~~~~~~~~~~~~~ fun get_basStr used twice --vv
248 "~~~~~~~~~~~~~~~~~~~ fun get_potStr used twice --vv
249 "~~~~~~~~~~~~~~~ fun monom_degree
250 "~~~~~~~~~~~~~ fun compare_koeff_ord
251 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon
252 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr
253 "~~~~~ fun is_multUnordered
254 "~~~~~~~ fun sort_variables
255 "~~~~~~~~~ fun sort_varList
256 "~~~~~~~~~~~ fun var_ord
257 "~~~~~~~~~~~~~ fun get_basStr used twice --^^
258 "~~~~~~~~~~~~~ fun get_potStr used twice --^^
260 val t = ParseC.parse_test @{context} "(1 + 2 * x \<up> 4 + - 4 * x \<up> 4 + x \<up> 8) is_addUnordered";
262 eval_is_addUnordered "xxx" "yyy" t @{context};
263 "~~~~~ fun eval_is_addUnordered , args:"; val ((thmid:string), _,
264 (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)), thy) =
265 ("xxx", "yyy", t, @{context});
267 (*if*) is_addUnordered arg;
268 "~~~~~ fun is_addUnordered , args:"; val (t) = (arg);
269 ((is_polyexp t) andalso not (t = sort_monoms t));
272 "~~~~~~~ fun sort_monoms , args:"; val (t) = (t);
273 val ll = map monom2list (poly2list t);
277 "~~~~~~~~~ fun sort_monList , args:"; val (ll) = (ll);
280 sort koeff_degree_ord ll(*return value*);
281 "~~~~~~~~~~~ fun koeff_degree_ord , args:"; val (ll) = (ll);
282 koeff_degree_ord: term list * term list -> order;
283 (*we check all elements at once..*)
284 val eee1 = ll |> nth 1;
285 val eee2 = ll |> nth 2;
286 val eee3 = ll |> nth 3;
287 val eee3 = ll |> nth 3;
288 val eee4 = ll |> nth 4;
290 if UnparseC.terms @{context} eee1 = "[1]" then () else error "eee1 CHANGED";
291 if UnparseC.terms @{context} eee2 = "[2, x \<up> 4]" then () else error "eee2 CHANGED";
292 if UnparseC.terms @{context} eee3 = "[- 4, x \<up> 4]" then () else error "eee3 CHANGED";
293 if UnparseC.terms @{context} eee4 = "[x \<up> 8]" then () else error "eee4 CHANGED";
295 if koeff_degree_ord (eee1, eee1) = EQUAL then () else error "(eee1, eee1) CHANGED";
296 if koeff_degree_ord (eee1, eee2) = LESS then () else error "(eee1, eee2) CHANGED";
297 if koeff_degree_ord (eee1, eee3) = LESS then () else error "(eee1, eee3) CHANGED";
298 if koeff_degree_ord (eee1, eee4) = LESS then () else error "(eee1, eee4) CHANGED";
300 if koeff_degree_ord (eee2, eee1) = GREATER then () else error "(eee2, eee1) CHANGED";
301 if koeff_degree_ord (eee2, eee2) = EQUAL then () else error "(eee2, eee4) CHANGED";
302 if koeff_degree_ord (eee2, eee3) = LESS then () else error "(eee2, eee3) CHANGED";
303 if koeff_degree_ord (eee2, eee4) = LESS then () else error "(eee2, eee4) CHANGED";
305 if koeff_degree_ord (eee3, eee1) = GREATER then () else error "(eee3, eee1) CHANGED";
306 if koeff_degree_ord (eee3, eee2) = GREATER then () else error "(eee3, eee4) CHANGED";
307 if koeff_degree_ord (eee3, eee3) = EQUAL then () else error "(eee3, eee3) CHANGED";
308 if koeff_degree_ord (eee3, eee4) = LESS then () else error "(eee3, eee4) CHANGED";
310 if koeff_degree_ord (eee4, eee1) = GREATER then () else error "(eee4, eee1) CHANGED";
311 if koeff_degree_ord (eee4, eee2) = GREATER then () else error "(eee4, eee4) CHANGED";
312 if koeff_degree_ord (eee4, eee3) = GREATER then () else error "(eee4, eee3) CHANGED";
313 if koeff_degree_ord (eee4, eee4) = EQUAL then () else error "(eee4, eee4) CHANGED";
315 "~~~~~~~~~~~~~ fun degree_ord , args:"; val () = ();
316 degree_ord: term list * term list -> order;
318 if degree_ord (eee1, eee1) = EQUAL then () else error "degree_ord (eee1, eee1) CHANGED";
319 if degree_ord (eee1, eee2) = LESS then () else error "degree_ord (eee1, eee2) CHANGED";
320 if degree_ord (eee1, eee3) = LESS then () else error "degree_ord (eee1, eee3) CHANGED";
321 if degree_ord (eee1, eee4) = LESS then () else error "degree_ord (eee1, eee4) CHANGED";
323 if degree_ord (eee2, eee1) = GREATER then () else error "degree_ord (eee2, eee1) CHANGED";
324 if degree_ord (eee2, eee2) = EQUAL then () else error "degree_ord (eee2, eee4) CHANGED";
325 if degree_ord (eee2, eee3) = EQUAL then () else error "degree_ord (eee2, eee3) CHANGED";
326 if degree_ord (eee2, eee4) = LESS then () else error "degree_ord (eee2, eee4) CHANGED";
328 if degree_ord (eee3, eee1) = GREATER then () else error "degree_ord (eee3, eee1) CHANGED";
329 if degree_ord (eee3, eee2) = EQUAL then () else error "degree_ord (eee3, eee4) CHANGED";
330 if degree_ord (eee3, eee3) = EQUAL then () else error "degree_ord (eee3, eee3) CHANGED";
331 if degree_ord (eee3, eee4) = LESS then () else error "degree_ord (eee3, eee4) CHANGED";
333 if degree_ord (eee4, eee1) = GREATER then () else error "degree_ord (eee4, eee1) CHANGED";
334 if degree_ord (eee4, eee2) = GREATER then () else error "degree_ord (eee4, eee4) CHANGED";
335 if degree_ord (eee4, eee3) = GREATER then () else error "degree_ord (eee4, eee3) CHANGED";
336 if degree_ord (eee4, eee4) = EQUAL then () else error "degree_ord (eee4, eee4) CHANGED";
338 "~~~~~~~~~~~~~~~ fun dict_cond_ord , args:"; val () = ();
339 dict_cond_ord: (term * term -> order) -> (term -> bool) -> term list * term list -> order;
340 dict_cond_ord var_ord_revPow: (term -> bool) -> term list * term list -> order;
341 dict_cond_ord var_ord_revPow is_nums: term list * term list -> order;
342 val xxx = dict_cond_ord var_ord_revPow is_nums;
344 fun var_ord_revPow (a,b: term) =
345 (@ {print} {a = "var_ord_revPow ", ab = "(" ^ UnparseC.term @{context} a ^ ", " ^ UnparseC.term @{context} b ^ ")"};
346 @ {print} {z = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
347 prod_ord string_ord string_ord_rev
348 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)));
350 if xxx (eee1, eee1) = EQUAL then () else error "dict_cond_ord ..(eee1, eee1) CHANGED";
351 if xxx (eee1, eee2) = LESS then () else error "dict_cond_ord ..(eee1, eee2) CHANGED";
352 if xxx (eee1, eee3) = LESS then () else error "dict_cond_ord ..(eee1, eee3) CHANGED";
353 if xxx (eee1, eee4) = LESS then () else error "dict_cond_ord ..(eee1, eee4) CHANGED";
354 (*-------------------------------------------------------------------------------------*)
355 if xxx (eee2, eee1) = GREATER then () else error "dict_cond_ord ..(eee2, eee1) CHANGED";
356 if xxx (eee2, eee2) = EQUAL then () else error "dict_cond_ord ..(eee2, eee2) CHANGED";
357 if xxx (eee2, eee3) = EQUAL then () else error "dict_cond_ord ..(eee2, eee3) CHANGED";
358 if xxx (eee2, eee4) = GREATER then () else error "dict_cond_ord ..(eee2, eee4) CHANGED";
359 (*-------------------------------------------------------------------------------------*)
360 if xxx (eee3, eee1) = GREATER then () else error "dict_cond_ord ..(eee3, eee1) CHANGED";
361 if xxx (eee3, eee2) = EQUAL then () else error "dict_cond_ord ..(eee3, eee2) CHANGED";
362 if xxx (eee3, eee3) = EQUAL then () else error "dict_cond_ord ..(eee3, eee3) CHANGED";
363 if xxx (eee3, eee4) = GREATER then () else error "dict_cond_ord ..(eee3, eee4) CHANGED";
364 (*-------------------------------------------------------------------------------------*)
365 if xxx (eee4, eee1) = GREATER then () else error "dict_cond_ord ..(eee4, eee1) CHANGED";
366 if xxx (eee4, eee2) = LESS then () else error "dict_cond_ord ..(eee4, eee2) CHANGED";
367 if xxx (eee4, eee3) = LESS then () else error "dict_cond_ord ..(eee4, eee3) CHANGED";
368 if xxx (eee4, eee4) = EQUAL then () else error "dict_cond_ord ..(eee4, eee4) CHANGED";
369 (*-------------------------------------------------------------------------------------*)
371 "~~~~~~~~~~~~~~~ fun monom_degree , args:"; val () = ();
372 (* we check all at once//*)
373 if monom_degree eee1 = 0 then () else error "monom_degree eee1 CHANGED";
374 if monom_degree eee2 = 4 then () else error "monom_degree eee2 CHANGED";
375 if monom_degree eee3 = 4 then () else error "monom_degree eee3 CHANGED";
376 if monom_degree eee4 = 8 then () else error "monom_degree eee4 CHANGED";
378 "~~~~~~~~~~~~~ fun compare_koeff_ord , args:"; val () = ();
379 compare_koeff_ord: term list * term list -> order;
380 (* we check all at once//*)
381 if compare_koeff_ord (eee1, eee1) = EQUAL then () else error "_koeff_ord (eee1, eee1) CHANGED";
382 if compare_koeff_ord (eee1, eee2) = LESS then () else error "_koeff_ord (eee1, eee2) CHANGED";
383 if compare_koeff_ord (eee1, eee3) = LESS then () else error "_koeff_ord (eee1, eee3) CHANGED";
384 if compare_koeff_ord (eee1, eee4) = GREATER then () else error "_koeff_ord (eee1, eee4) CHANGED";
386 if compare_koeff_ord (eee2, eee1) = GREATER then () else error "_koeff_ord (eee2, eee1) CHANGED";
387 if compare_koeff_ord (eee2, eee2) = EQUAL then () else error "_koeff_ord (eee2, eee2) CHANGED";
388 if compare_koeff_ord (eee2, eee3) = LESS then () else error "_koeff_ord (eee2, eee3) CHANGED";
389 if compare_koeff_ord (eee2, eee4) = GREATER then () else error "_koeff_ord (eee2, eee4) CHANGED";
391 if compare_koeff_ord (eee3, eee1) = GREATER then () else error "_koeff_ord (eee3, eee1) CHANGED";
392 if compare_koeff_ord (eee3, eee2) = GREATER then () else error "_koeff_ord (eee3, eee2) CHANGED";
393 if compare_koeff_ord (eee3, eee3) = EQUAL then () else error "_koeff_ord (eee3, eee3) CHANGED";
394 if compare_koeff_ord (eee3, eee4) = GREATER then () else error "_koeff_ord (eee3, eee4) CHANGED";
396 if compare_koeff_ord (eee4, eee1) = LESS then () else error "_koeff_ord (eee4, eee1) CHANGED";
397 if compare_koeff_ord (eee4, eee2) = LESS then () else error "_koeff_ord (eee4, eee2) CHANGED";
398 if compare_koeff_ord (eee4, eee3) = LESS then () else error "_koeff_ord (eee4, eee3) CHANGED";
399 if compare_koeff_ord (eee4, eee4) = EQUAL then () else error "_koeff_ord (eee4, eee4) CHANGED";
401 "~~~~~~~~~~~~~~~ fun get_koeff_of_mon , args:"; val () = ();
402 get_koeff_of_mon: term list -> term option;
404 val SOME xxx1 = get_koeff_of_mon eee1;
405 val SOME xxx2 = get_koeff_of_mon eee2;
406 val SOME xxx3 = get_koeff_of_mon eee3;
407 val NONE = get_koeff_of_mon eee4;
409 if UnparseC.term @{context} xxx1 = "1" then () else error "get_koeff_of_mon eee1 CHANGED";
410 if UnparseC.term @{context} xxx2 = "2" then () else error "get_koeff_of_mon eee2 CHANGED";
411 if UnparseC.term @{context} xxx3 = "- 4" then () else error "get_koeff_of_mon eee3 CHANGED";
413 "~~~~~~~~~~~~~~~~~ fun koeff2ordStr , args:"; val () = ();
414 koeff2ordStr: term option -> string;
415 if koeff2ordStr (SOME xxx1) = "1" then () else error "koeff2ordStr eee1 CHANGED";
416 if koeff2ordStr (SOME xxx2) = "2" then () else error "koeff2ordStr eee2 CHANGED";
417 if koeff2ordStr (SOME xxx3) = "40" then () else error "koeff2ordStr eee3 CHANGED";
418 if koeff2ordStr NONE = "---" then () else error "koeff2ordStr eee4 CHANGED";
421 "-------- examples from textbook Schalk I ------------------------------------------------------";
422 "-------- examples from textbook Schalk I ------------------------------------------------------";
423 "-------- examples from textbook Schalk I ------------------------------------------------------";
424 "-----SPB Schalk I p.63 No.267b ---";
425 val t = ParseC.parse_test @{context} "(5*x \<up> 2 + 3) * (2*x \<up> 7 + 3) - (3*x \<up> 5 + 8) * (6*x \<up> 4 - 1)";
426 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
427 if UnparseC.term @{context} t = "17 + 15 * x \<up> 2 + - 48 * x \<up> 4 + 3 * x \<up> 5 + 6 * x \<up> 7 +\n- 8 * x \<up> 9"
428 then () else error "poly.sml: diff.behav. in make_polynomial 1";
430 "-----SPB Schalk I p.63 No.275b ---";
431 val t = ParseC.parse_test @{context} "(3*x \<up> 2 - 2*x*y + y \<up> 2) * (x \<up> 2 - 2*y \<up> 2)";
432 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
433 if UnparseC.term @{context} t =
434 "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"
435 then () else error "poly.sml: diff.behav. in make_polynomial 2";
437 "-----SPB Schalk I p.63 No.279b ---";
438 val t = ParseC.parse_test @{context} "(x-a)*(x-b)*(x-c)*(x-d)";
439 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
440 if UnparseC.term @{context} t =
441 ("a * b * c * d + - 1 * a * b * c * x + - 1 * a * b * d * x +\na * b * x \<up> 2 +\n" ^
442 "- 1 * a * c * d * x +\na * c * x \<up> 2 +\na * d * x \<up> 2 +\n- 1 * a * x \<up> 3 +\n" ^
443 "- 1 * b * c * d * x +\nb * c * x \<up> 2 +\nb * d * x \<up> 2 +\n- 1 * b * x \<up> 3 +\nc" ^
444 " * d * x \<up> 2 +\n- 1 * c * x \<up> 3 +\n- 1 * d * x \<up> 3 +\nx \<up> 4")
445 then () else error "poly.sml: diff.behav. in make_polynomial 3";
448 "-----SPB Schalk I p.63 No.291 ---";
449 val t = ParseC.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)))";
450 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
451 if UnparseC.term @{context} t = "50 + - 770 * x + 4520 * x \<up> 2 + - 16320 * x \<up> 3 +\n- 26880 * x \<up> 4"
452 then () else error "poly.sml: diff.behav. in make_polynomial 4";
454 "-----SPB Schalk I p.64 No.295c ---";
455 val t = ParseC.parse_test @{context} "(13*a \<up> 4*b \<up> 9*c - 12*a \<up> 3*b \<up> 6*c \<up> 9) \<up> 2";
456 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
457 if UnparseC.term @{context} t =
458 "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"
459 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
461 "-----SPB Schalk I p.64 No.299a ---";
462 val t = ParseC.parse_test @{context} "(x - y)*(x + y)";
463 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
464 if UnparseC.term @{context} t = "x \<up> 2 + - 1 * y \<up> 2"
465 then () else error "poly.sml: diff.behav. in make_polynomial 6";
467 "-----SPB Schalk I p.64 No.300c ---";
468 val t = ParseC.parse_test @{context} "(3*x \<up> 2*y - 1)*(3*x \<up> 2*y + 1)";
469 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
470 if UnparseC.term @{context} t = "- 1 + 9 * x \<up> 4 * y \<up> 2"
471 then () else error "poly.sml: diff.behav. in make_polynomial 7";
473 "-----SPB Schalk I p.64 No.302 ---";
474 val t = ParseC.parse_test @{context}
475 "(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)";
476 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
477 if UnparseC.term @{context} t = "0"
478 then () else error "poly.sml: diff.behav. in make_polynomial 8";
479 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
481 "-----SPB Schalk I p.64 No.306a ---";
482 val t = ParseC.parse_test @{context} "((x \<up> 2 + 1)*(x \<up> 2 - 1)) \<up> 2";
483 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
484 if UnparseC.term @{context} t = "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8" then ()
485 else error "poly.sml: diff.behav. in 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 = - 2 * x \<up> 4";
487 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
488 the above resulted in the term below ... but reduces from then correctly*)
489 val t = ParseC.parse_test @{context} "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
490 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
491 if UnparseC.term @{context} t = "1 + - 2 * x \<up> 4 + x \<up> 8"
492 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
494 "-----SPB Schalk I p.64 No.296a ---";
495 val t = ParseC.parse_test @{context} "(x - a) \<up> 3";
496 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
498 val NONE = eval_is_even "aaa" "bbb" (ParseC.parse_test @{context} "3::real") "ccc";
500 if UnparseC.term @{context} t = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
501 then () else error "poly.sml: diff.behav. in make_polynomial 10";
503 "-----SPB Schalk I p.64 No.296c ---";
504 val t = ParseC.parse_test @{context} "(-3*x - 4*y) \<up> 3";
505 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
506 if UnparseC.term @{context} t = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
507 then () else error "poly.sml: diff.behav. in make_polynomial 11";
509 "-----SPB Schalk I p.62 No.242c ---";
510 val t = ParseC.parse_test @{context} "x \<up> (-4)*(x \<up> (-4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
511 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
512 if UnparseC.term @{context} t = "1"
513 then () else error "poly.sml: diff.behav. in make_polynomial 12";
515 "-----SPB Schalk I p.60 No.209a ---";
516 val t = ParseC.parse_test @{context} "a \<up> (7-x) * a \<up> x";
517 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
518 if UnparseC.term @{context} t = "a \<up> 7"
519 then () else error "poly.sml: diff.behav. in make_polynomial 13";
521 "-----SPB Schalk I p.60 No.209d ---";
522 val t = ParseC.parse_test @{context} "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
523 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
524 if UnparseC.term @{context} t = "d \<up> 3"
525 then () else error "poly.sml: diff.behav. in make_polynomial 14";
527 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
528 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
529 "-------- ?RL?Bsple bei denen es Probleme gibt--------------------------------------------------";
530 "-----Schalk I p.64 No.303 ---";
531 val t = ParseC.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)";
532 (*SOMETIMES LOOPS---------------------------------------------------------------------------\\*)
533 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
534 if UnparseC.term @{context} t = "1280 * b \<up> 4"
535 then () else error "poly.sml: diff.behav. in make_polynomial 14b";
536 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
537 (*SOMETIMES LOOPS--------------------------------------------------------------------------//*)
539 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
540 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
541 "-------- Eigene Beispiele (Mathias Goldgruber) ------------------------------------------------";
543 val t = ParseC.parse_test @{context} "a + a + a";
544 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
545 if UnparseC.term @{context} t = "3 * a" then ()
546 else error "poly.sml: diff.behav. in make_polynomial 16";
548 val t = ParseC.parse_test @{context} "a + b + b + b";
549 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
550 if UnparseC.term @{context} t = "a + 3 * b" then ()
551 else error "poly.sml: diff.behav. in make_polynomial 17";
553 val t = ParseC.parse_test @{context} "b * a * a";
554 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
555 if UnparseC.term @{context} t = "a \<up> 2 * b" then ()
556 else error "poly.sml: diff.behav. in make_polynomial 21";
558 val t = ParseC.parse_test @{context} "(a \<up> 2) \<up> 3";
559 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
560 if UnparseC.term @{context} t = "a \<up> 6" then ()
561 else error "poly.sml: diff.behav. in make_polynomial 22";
563 val t = ParseC.parse_test @{context} "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
564 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term @{context} t;
565 if UnparseC.term @{context} t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
566 else error "poly.sml: diff.behav. in make_polynomial 23";
568 val t = ParseC.parse_test @{context} "a * b * b \<up> (- 1) + a";
569 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term @{context} t;
570 if UnparseC.term @{context} t = "2 * a" then ()
571 else error "poly.sml: diff.behav. in make_polynomial 25";
573 val t = ParseC.parse_test @{context} "a*c*b \<up> (2*n) + 3*a + 5*b \<up> (2*n)*c*b";
574 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t; UnparseC.term @{context} t;
575 if UnparseC.term @{context} t = "3 * a + 5 * b \<up> (1 + 2 * n) * c + a * b \<up> (2 * n) * c"
576 then () else error "poly.sml: diff.behav. in make_polynomial 26";
578 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
580 val t = ParseC.parse_test @{context} "(1 + (x*y*a) + x) \<up> (1 + (x*y*a) + x)";
581 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
582 if UnparseC.term @{context} t = "(1 + x + a * x * y) \<up> (1 + x + a * x * y)"
583 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
585 val t = ParseC.parse_test @{context} "(1 + x*(y*z)*zz) \<up> (1 + x*(y*z)*zz)";
586 val SOME (t,_) = rewrite_set_ @{context} false make_polynomial t;
587 if UnparseC.term @{context} t = "(1 + x * y * z * zz) \<up> (1 + x * y * z * zz)"
588 then () else error "poly.sml: diff.behav. in make_polynomial 28";
590 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
591 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
592 "-------- check pbl 'polynomial simplification' -----------------------------------------------";
593 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"];
595 case Refine.xxxxx @{context} fmz ["polynomial", "simplification"] of
596 [M_Match.Matches (["polynomial", "simplification"], _)] => ()
597 | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
598 (*...if there is an error, then ...*)
601 (*default_print_depth 7;*)
602 val pbt = Problem.from_store @{context} ["polynomial", "simplification"];
603 (*default_print_depth 3;*)
605 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
606 ... then Rewrite.trace_on:*)
609 M_Match.match_pbl fmz pbt;
610 (*... if there is no rewrite, then there is something wrong with where_rls*)
613 (*default_print_depth 7;*)
614 val where_rls = (#where_rls o Problem.from_store @{context}) ["polynomial", "simplification"];
615 (*default_print_depth 3;*)
616 val t = ParseC.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";
617 val SOME (t',_) = rewrite_set_ thy false where_rls t;
618 if t' = @{term True} then ()
619 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
620 (*... if this works, but -- 1-- does still NOT work, check types:*)
623 (*show_types:=true;*)
625 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
626 val wh = [False "(t_::real => real) (is_polyexp::real)"]
627 ...................... \<up> \<up> \<up> \<up> ............... \<up> ^*)
628 val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
629 (*show_types:=false;*)
632 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
633 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
634 "-------- me 'poly. simpl.' Schalk I p.63 No.267b ----------------------------------------------";
635 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"];
637 ("Poly",["polynomial", "simplification"],
638 ["simplification", "for_polynomials"]);
639 val p = e_pos'; val c = [];
640 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
641 (*[], 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))"*)
642 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
644 (*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
645 (*+*) "[\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)]))]"
646 (*+*)then () else error "No.267b: I_Model.T CHANGED";
647 ( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
649 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
650 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
651 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
652 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
653 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
655 (*+*)if f2str f = "(5 * x \<up> 2 + 3) * (2 * x \<up> 7 + 3) -\n(3 * x \<up> 5 + 8) * (6 * x \<up> 4 - 1)"
656 (*+*)then () else error "";
658 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
660 (*+*)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"
661 (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b - 1";
663 (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
667 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
668 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
669 "-------- interSteps for Schalk 299a -----------------------------------------------------------";
672 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],
673 ("Poly",["polynomial", "simplification"],
674 ["simplification", "for_polynomials"]))];
677 autoCalculate 1 CompleteCalc;
678 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
680 interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
681 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
682 if existpt' ([1,1], Frm) pt then ()
683 else error "poly.sml: interSteps doesnt work again 1";
685 interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
686 val ((pt,p),_) = States.get_calc 1; Test_Tool.show_pt pt;
687 (*============ inhibit exn WN120316 ==============================================
688 if existpt' ([1,1,1], Frm) pt then ()
689 else error "poly.sml: interSteps doesnt work again 2";
690 ============ inhibit exn WN120316 ==============================================*)
692 "-------- ord_make_polynomial ------------------------------------------------------------------";
693 "-------- ord_make_polynomial ------------------------------------------------------------------";
694 "-------- ord_make_polynomial ------------------------------------------------------------------";
695 val t1 = ParseC.parse_test @{context} "2 * b + (3 * a + 3 * b)";
696 val t2 = ParseC.parse_test @{context} "(3 * a + 3 * b) + 2 * b";
698 if ord_make_polynomial true @{context} [] (t1, t2) then ()
699 else error "poly.sml: diff.behav. in ord_make_polynomial";
700 (*SO: WHY IS THERE NO REWRITING ...*)
702 val term = ParseC.parse_test @{context} "2*b + (3*a + 3*b)";
703 (*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term;
705 WHY IS THERE NO REWRITING ?!?
706 most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML,
707 while order_add_mult uses isac's rewriter -- and this is used rarely!