1 (* testexamples for Poly, polynomials
2 author: Matthias Goldgruber 2003
3 (c) due to copyright terms
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890
6 10 20 30 40 50 60 70 80
8 WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
9 examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
12 "--------------------------------------------------------";
13 "--------------------------------------------------------";
14 "table of contents --------------------------------------";
15 "--------------------------------------------------------";
16 "----------- fun is_polyexp --------------------------------------------------------------------";
17 "----------- fun has_degree_in -----------------------------------------------------------------";
18 "----------- fun mono_deg_in -------------------------------------------------------------------";
19 "----------- fun mono_deg_in -------------------------------------------------------------------";
20 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
21 "-------- investigate (new 2002) uniary minus -----------";
22 "-------- check make_polynomial with simple terms -------";
23 "-------- fun is_multUnordered --------------------------";
24 "-------- examples from textbook Schalk I ---------------";
25 "-------- check pbl 'polynomial simplification' --------";
26 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
27 "-------- interSteps for Schalk 299a --------------------";
28 "-------- norm_Poly NOT COMPLETE ------------------------";
29 "-------- ord_make_polynomial ---------------------------";
30 "--------------------------------------------------------";
31 "--------------------------------------------------------";
32 "--------------------------------------------------------";
35 "----------- fun is_polyexp --------------------------------------------------------------------";
36 "----------- fun is_polyexp --------------------------------------------------------------------";
37 "----------- fun is_polyexp --------------------------------------------------------------------";
38 val thy = @{theory Partial_Fractions};
39 val ctxt = Proof_Context.init_global thy;
41 val t = (the o (parseNEW ctxt)) "x / x";
42 if is_polyexp t then error "NOT is_polyexp (x / x)" else ();
44 val t = (the o (parseNEW ctxt)) "-1 * A * 3";
45 if is_polyexp t then () else error "is_polyexp (-1 * A * 3)";
47 val t = (the o (parseNEW ctxt)) "-1 * AA * 3";
48 if is_polyexp t then () else error "is_polyexp (-1 * AA * 3)";
50 "----------- fun has_degree_in -----------------------------------------------------------------";
51 "----------- fun has_degree_in -----------------------------------------------------------------";
52 "----------- fun has_degree_in -----------------------------------------------------------------";
53 val v = (Thm.term_of o the o (parse thy)) "x";
54 val t = (Thm.term_of o the o (parse thy)) "1";
55 if has_degree_in t v = 0 then () else error "has_degree_in (1) x";
57 val v = (Thm.term_of o the o (parse thy)) "AA";
58 val t = (Thm.term_of o the o (parse thy)) "1";
59 if has_degree_in t v = 0 then () else error "has_degree_in (1) AA";
62 val v = (Thm.term_of o the o (parse thy)) "x";
63 val t = (Thm.term_of o the o (parse thy)) "a*b+c";
64 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) x";
66 val v = (Thm.term_of o the o (parse thy)) "AA";
67 val t = (Thm.term_of o the o (parse thy)) "a*b+c";
68 if has_degree_in t v = 0 then () else error "has_degree_in (a*b+c) AA";
71 val v = (Thm.term_of o the o (parse thy)) "x";
72 val t = (Thm.term_of o the o (parse thy)) "a*x+c";
73 if has_degree_in t v = ~1 then () else error "has_degree_in (a*x+c) x";
75 val v = (Thm.term_of o the o (parse thy)) "AA";
76 val t = (Thm.term_of o the o (parse thy)) "a*AA+c";
77 if has_degree_in t v = ~1 then () else error "has_degree_in (a*AA+c) AA";
80 val v = (Thm.term_of o the o (parse thy)) "x";
81 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
82 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*x^^^7) x";
84 val v = (Thm.term_of o the o (parse thy)) "AA";
85 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";
86 if has_degree_in t v = 7 then () else error "has_degree_in ((a*b+c)*AA^^^7) AA";
89 val v = (Thm.term_of o the o (parse thy)) "x";
90 val t = (Thm.term_of o the o (parse thy)) "x^^^7";
91 if has_degree_in t v = 7 then () else error "has_degree_in (x^^^7) x";
93 val v = (Thm.term_of o the o (parse thy)) "AA";
94 val t = (Thm.term_of o the o (parse thy)) "AA^^^7";
95 if has_degree_in t v = 7 then () else error "has_degree_in (AA^^^7) AA";
98 val v = (Thm.term_of o the o (parse thy)) "x";
99 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
100 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*x) x";
102 val v = (Thm.term_of o the o (parse thy)) "AA";
103 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";
104 if has_degree_in t v = 1 then () else error "has_degree_in ((a*b+c)*AA) AA";
107 val v = (Thm.term_of o the o (parse thy)) "x";
108 val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
109 if has_degree_in t v = ~1 then () else error "has_degree_in (a*b+x)*x() x";
111 val v = (Thm.term_of o the o (parse thy)) "AA";
112 val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";
113 if has_degree_in t v = ~1 then () else error "has_degree_in ((a*b+AA)*AA) AA";
116 val v = (Thm.term_of o the o (parse thy)) "x";
117 val t = (Thm.term_of o the o (parse thy)) "x";
118 if has_degree_in t v = 1 then () else error "has_degree_in (x) x";
120 val v = (Thm.term_of o the o (parse thy)) "AA";
121 val t = (Thm.term_of o the o (parse thy)) "AA";
122 if has_degree_in t v = 1 then () else error "has_degree_in (AA) AA";
125 val v = (Thm.term_of o the o (parse thy)) "x";
126 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
127 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*x) x";
129 val v = (Thm.term_of o the o (parse thy)) "AA";
130 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";
131 if has_degree_in t v = 1 then () else error "has_degree_in (ab - (a*b)*AA) AA";
133 "----------- fun mono_deg_in -------------------------------------------------------------------";
134 "----------- fun mono_deg_in -------------------------------------------------------------------";
135 "----------- fun mono_deg_in -------------------------------------------------------------------";
136 val v = (Thm.term_of o the o (parse thy)) "x";
138 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
139 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*x^^^7) x changed";
141 val t = (Thm.term_of o the o (parse thy)) "x^^^7";
142 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (x^^^7) x changed";
144 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
145 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*x) x changed";
147 val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
148 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+x)*x) x changed";
150 val t = (Thm.term_of o the o (parse thy)) "x";
151 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (x) x changed";
153 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)";
154 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) x changed";
156 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
157 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*x) x changed";
159 (*. . . . . . . . . . . . the same with Const ("Partial_Functions.AA", _) . . . . . . . . . . . *)
160 val thy = @{theory Partial_Fractions}
161 val v = (Thm.term_of o the o (parse thy)) "AA";
163 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA^^^7";
164 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in ((a*b+c)*AA^^^7) AA changed";
166 val t = (Thm.term_of o the o (parse thy)) "AA^^^7";
167 if mono_deg_in t v = SOME 7 then () else error "mono_deg_in (AA^^^7) AA changed";
169 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*AA";
170 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in ((a*b+c)*AA) AA changed";
172 val t = (Thm.term_of o the o (parse thy)) "(a*b+AA)*AA";
173 if mono_deg_in t v = NONE then () else error "mono_deg_in ((a*b+AA)*AA) AA changed";
175 val t = (Thm.term_of o the o (parse thy)) "AA";
176 if mono_deg_in t v = SOME 1 then () else error "mono_deg_in (AA) AA changed";
178 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)";
179 if mono_deg_in t v = SOME 0 then () else error "mono_deg_in ((a*b+c)) AA changed";
181 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*AA";
182 if mono_deg_in t v = NONE then () else error "mono_deg_in (ab - (a*b)*AA) AA changed";
184 "----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
185 "----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
186 "----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
187 val thy = @{theory Partial_Fractions}
188 val expr = (Thm.term_of o the o (parse thy)) "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
189 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
191 val expr = (Thm.term_of o the o (parse thy)) "((-8 - 2*AA + AA^^^2) has_degree_in AA) = 2";
192 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
194 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
195 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
196 "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
197 val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
198 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
199 if UnparseC.term t' = "-8 - 2 * x + x ^^^ 2 is_expanded_in x = True"
200 andalso id = "-8 - 2 * x + x ^^^ 2 is_expanded_in x = True"
201 then () else error "eval_is_expanded_in x ..changed";
203 val thy = @{theory Partial_Fractions}
204 val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*AA + AA^^^2) is_expanded_in AA";
205 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
206 if UnparseC.term t' = "-8 - 2 * AA + AA ^^^ 2 is_expanded_in AA = True"
207 andalso id = "-8 - 2 * AA + AA ^^^ 2 is_expanded_in AA = True"
208 then () else error "eval_is_expanded_in AA ..changed";
211 val t = (Thm.term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
212 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
213 if UnparseC.term t' = "8 + 2 * x + x ^^^ 2 is_poly_in x = True"
214 andalso id = "8 + 2 * x + x ^^^ 2 is_poly_in x = True"
215 then () else error "is_poly_in x ..changed";
217 val t = (Thm.term_of o the o (parse thy)) "(8 + 2*AA + AA^^^2) is_poly_in AA";
218 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
219 if UnparseC.term t' = "8 + 2 * AA + AA ^^^ 2 is_poly_in AA = True"
220 andalso id = "8 + 2 * AA + AA ^^^ 2 is_poly_in AA = True"
221 then () else error "is_poly_in AA ..changed";
224 val thy = @{theory Partial_Fractions}
225 val expr = (Thm.term_of o the o (parse thy)) "((-8 - 2*x + x^^^2) has_degree_in x) = 2";
226 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
228 val expr = (Thm.term_of o the o (parse thy)) "((-8 - 2*AA + AA^^^2) has_degree_in AA) = 2";
229 val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
231 "-------- investigate (new 2002) uniary minus -----------";
232 "-------- investigate (new 2002) uniary minus -----------";
233 "-------- investigate (new 2002) uniary minus -----------";
234 (*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)
235 val t = Thm.prop_of @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
238 *** Const (HOL.Trueprop, bool => prop)
239 *** . Const (HOL.eq, real => real => bool)
240 *** . . Const (Groups.minus_class.minus, real => real => real)
241 *** . . . Const (Groups.zero_class.zero, real)
242 *** . . . Var ((x, 0), real)
243 *** . . Const (Groups.uminus_class.uminus, real => real)
244 *** . . . Var ((x, 0), real)
247 Const ("HOL.Trueprop", _) $
248 (Const ("HOL.eq", _) $
249 (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $
251 (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
252 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
254 (*----------------------------------- vvvv --------------------------------------------*)
255 val t = (Thm.term_of o the o (parse thy)) "-1";
258 *** Free ( -1, real) *)
261 | _ => error "internal representation of \"-1\" changed";
262 (*----------------------------------- vvvvv -------------------------------------------*)
263 val t = (Thm.term_of o the o (parse thy)) "- 1";
272 | _ => error "internal representation of \"- 1\" changed";
274 "======= these external values all have the same internal representation";
275 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)
276 (*----------------------------------- vvvvv -------------------------------------------*)
277 val t = (Thm.term_of o the o (parse thy)) "-x";
280 *** Free ( -x, real)*)
282 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
283 | _ => error "internal representation of \"-x\" changed";
284 (*----------------------------------- vvvvv -------------------------------------------*)
285 val t = (Thm.term_of o the o (parse thy)) "- x";
288 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
290 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
291 | _ => error "internal representation of \"- x\" changed";
292 (*----------------------------------- vvvvvv ------------------------------------------*)
293 val t = (Thm.term_of o the o (parse thy)) "-(x)";
296 *** Free ( -x, real)*)
298 Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
299 | _ => error "internal representation of \"-(x)\" changed";
301 "-------- check make_polynomial with simple terms -------";
302 "-------- check make_polynomial with simple terms -------";
303 "-------- check make_polynomial with simple terms -------";
305 val t = str2term "2*3*a";
306 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
307 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
310 val t = str2term "2*a + 3*a";
311 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
312 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
315 val t = str2term "2*a + 3*a + 3*a";
316 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
317 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
320 val t = str2term "3*a - 2*a";
321 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
322 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
325 val t = str2term "4*(3*a - 2*a)";
326 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
327 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
330 val t = str2term "4*(3*a^^^2 - 2*a^^^2)";
331 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
332 if UnparseC.term t = "4 * a ^^^ 2" then () else error "check make_polynomial 6";
334 "-------- fun is_multUnordered --------------------------";
335 "-------- fun is_multUnordered --------------------------";
336 "-------- fun is_multUnordered --------------------------";
337 val thy = @{theory "Isac_Knowledge"};
338 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
339 val t = str2term "x^^^2 * x";
340 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
341 if UnparseC.term t' = "x * x ^^^ 2" then ()
342 else error "poly.sml Poly.is'_multUnordered doesn't work";
344 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
345 ### rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +
347 ###### rls: Rule_Set.empty-is_multUnordered on: p is_multUnordered
348 ####### try calc: Poly.is'_multUnordered'
349 ======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
351 val t = str2term "5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))";
353 "----- is_multUnordered ---";
354 val tsort = sort_variables t;
355 UnparseC.term tsort = "2 * (5 * (x ^^^ 2 * x ^^^ 7)) + 3 * (5 * x ^^^ 2) + 6 * x ^^^ 7 + 9 +\n-1 * (3 * (6 * (x ^^^ 4 * x ^^^ 5))) +\n-1 * (-1 * (3 * x ^^^ 5)) +\n-48 * x ^^^ 4 +\n8";
358 is_polyexp t andalso not (t = sort_variables t);
359 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
361 "----- eval_is_multUnordered ---";
362 val tm = str2term "(5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) + (-48 * x ^^^ 4 + 8))) is_multUnordered";
363 case eval_is_multUnordered "testid" "" tm thy of
364 SOME (_, Const ("HOL.Trueprop", _) $
365 (Const ("HOL.eq", _) $
366 (Const ("Poly.is'_multUnordered", _) $ _) $
367 Const ("HOL.True", _))) => ()
368 | _ => error "poly.sml diff. eval_is_multUnordered";
370 "----- rewrite_set_ STILL DIDN'T WORK";
371 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
374 "-------- examples from textbook Schalk I ---------------";
375 "-------- examples from textbook Schalk I ---------------";
376 "-------- examples from textbook Schalk I ---------------";
377 "-----SPB Schalk I p.63 No.267b ---";
378 val t = str2term "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
379 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
380 if (UnparseC.term t) = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
381 then () else error "poly.sml: diff.behav. in make_polynomial 1";
383 "-----SPB Schalk I p.63 No.275b ---";
384 val t = str2term "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
385 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
386 if (UnparseC.term t) = ("3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + " ^
387 "4 * x * y ^^^ 3 +\n-2 * y ^^^ 4")
388 then () else error "poly.sml: diff.behav. in make_polynomial 2";
390 "-----SPB Schalk I p.63 No.279b ---";
391 val t = str2term "(x-a)*(x-b)*(x-c)*(x-d)";
392 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
393 if (UnparseC.term t) =
394 ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n" ^
395 "-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n" ^
396 "-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\n" ^
397 "c * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4")
398 then () else error "poly.sml: diff.behav. in make_polynomial 3";
400 "-----SPB Schalk I p.63 No.291 ---";
401 val t = str2term "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
402 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
403 if (UnparseC.term t) = "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
404 then () else error "poly.sml: diff.behav. in make_polynomial 4";
406 "-----SPB Schalk I p.64 No.295c ---";
407 val t = str2term "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
408 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
409 if (UnparseC.term t) = ("169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10" ^
410 " +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18")
411 then ()else error "poly.sml: diff.behav. in make_polynomial 5";
413 "-----SPB Schalk I p.64 No.299a ---";
414 val t = str2term "(x - y)*(x + y)";
415 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
416 if (UnparseC.term t) = "x ^^^ 2 + -1 * y ^^^ 2"
417 then () else error "poly.sml: diff.behav. in make_polynomial 6";
419 "-----SPB Schalk I p.64 No.300c ---";
420 val t = str2term "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
421 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
422 if (UnparseC.term t) = "-1 + 9 * x ^^^ 4 * y ^^^ 2"
423 then () else error "poly.sml: diff.behav. in make_polynomial 7";
425 "-----SPB Schalk I p.64 No.302 ---";
427 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
428 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
429 if UnparseC.term t = "0"
430 then () else error "poly.sml: diff.behav. in make_polynomial 8";
431 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
433 "-----SPB Schalk I p.64 No.306a ---";
434 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
435 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
436 if (UnparseC.term t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
437 else error "poly.sml: diff.behav. in 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4";
439 (*WN071729 when reducing "rls reduce_012_" for Schaerding,
440 the above resulted in the term below ... but reduces from then correctly*)
441 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
442 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
443 if (UnparseC.term t) = "1 + -2 * x ^^^ 4 + x ^^^ 8"
444 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
446 "-----SPB Schalk I p.64 No.296a ---";
447 val t = str2term "(x - a)^^^3";
448 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
449 if (UnparseC.term t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
450 then () else error "poly.sml: diff.behav. in make_polynomial 10";
452 "-----SPB Schalk I p.64 No.296c ---";
453 val t = str2term "(-3*x - 4*y)^^^3";
454 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
455 if (UnparseC.term t) = "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
456 then () else error "poly.sml: diff.behav. in make_polynomial 11";
458 "-----SPB Schalk I p.62 No.242c ---";
459 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
460 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
461 if (UnparseC.term t) = "1"
462 then () else error "poly.sml: diff.behav. in make_polynomial 12";
464 "-----SPB Schalk I p.60 No.209a ---";
465 val t = str2term "a^^^(7-x) * a^^^x";
466 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
467 if UnparseC.term t = "a ^^^ 7"
468 then () else error "poly.sml: diff.behav. in make_polynomial 13";
470 "-----SPB Schalk I p.60 No.209d ---";
471 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
472 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
473 if UnparseC.term t = "d ^^^ 3"
474 then () else error "poly.sml: diff.behav. in make_polynomial 14";
476 (*---------------------------------------------------------------------*)
477 (*---------------- ?RL?Bsple bei denen es Probleme gibt----------------*)
478 (*---------------------------------------------------------------------*)
479 "-----Schalk I p.64 No.303 ---";
480 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
481 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
482 if UnparseC.term t = "1280 * b ^^^ 4"
483 then () else error "poly.sml: diff.behav. in make_polynomial 14b";
484 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
486 (*--------------------------------------------------------------------*)
487 (*----------------------- Eigene Beispiele ---------------------------*)
488 (*--------------------------------------------------------------------*)
490 val t = str2term "a^^^2*a^^^(-2)";
491 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
492 if UnparseC.term t = "1" then ()
493 else error "poly.sml: diff.behav. in make_polynomial 15";
495 val t = str2term "a + a + a";
496 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
497 if UnparseC.term t = "3 * a" then ()
498 else error "poly.sml: diff.behav. in make_polynomial 16";
500 val t = str2term "a + b + b + b";
501 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
502 if UnparseC.term t = "a + 3 * b" then ()
503 else error "poly.sml: diff.behav. in make_polynomial 17";
505 val t = str2term "a^^^2*b*b^^^(-1)";
506 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
507 if UnparseC.term t = "a ^^^ 2" then ()
508 else error "poly.sml: diff.behav. in make_polynomial 18";
510 val t = str2term "a^^^2*a^^^(-2)";
511 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
512 if (UnparseC.term t) = "1" then ()
513 else error "poly.sml: diff.behav. in make_polynomial 19";
515 val t = str2term "b + a - b";
516 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
517 if (UnparseC.term t) = "a" then ()
518 else error "poly.sml: diff.behav. in make_polynomial 20";
520 val t = str2term "b * a * a";
521 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
522 if UnparseC.term t = "a ^^^ 2 * b" then ()
523 else error "poly.sml: diff.behav. in make_polynomial 21";
525 val t = str2term "(a^^^2)^^^3";
526 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
527 if UnparseC.term t = "a ^^^ 6" then ()
528 else error "poly.sml: diff.behav. in make_polynomial 22";
530 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
531 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
532 if UnparseC.term t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
533 else error "poly.sml: diff.behav. in make_polynomial 23";
535 val t = (Thm.term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
536 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
537 if (UnparseC.term t) = "a ^^^ 4" then ()
538 else error "poly.sml: diff.behav. in make_polynomial 24";
540 val t = str2term "a * b * b^^^(-1) + a";
541 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
542 if (UnparseC.term t) = "2 * a" then ()
543 else error "poly.sml: diff.behav. in make_polynomial 25";
545 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
546 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
547 if (UnparseC.term t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
548 then () else error "poly.sml: diff.behav. in make_polynomial 26";
550 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)
552 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
553 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
554 if UnparseC.term t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
555 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
557 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
558 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
559 if UnparseC.term t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
560 then () else error "poly.sml: diff.behav. in make_polynomial 28";
562 "-------- check pbl 'polynomial simplification' --------";
563 "-------- check pbl 'polynomial simplification' --------";
564 "-------- check pbl 'polynomial simplification' --------";
565 val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];
567 case Refine.refine fmz ["polynomial", "simplification"]of
568 [M_Match.Matches (["polynomial", "simplification"], _)] => ()
569 | _ => error "poly.sml diff.behav. in check pbl, Refine.refine";
570 (*...if there is an error, then ...*)
573 (*default_print_depth 7;*)
574 val pbt = Problem.from_store ["polynomial", "simplification"];
575 (*default_print_depth 3;*)
577 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
578 ... then Rewrite.trace_on:*)
581 Rewrite.trace_on := false;
582 M_Match.match_pbl fmz pbt;
583 Rewrite.trace_on := false;
584 (*... if there is no rewrite, then there is something wrong with prls*)
587 (*default_print_depth 7;*)
588 val prls = (#prls o Problem.from_store) ["polynomial", "simplification"];
589 (*default_print_depth 3;*)
590 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
591 val SOME (t',_) = rewrite_set_ thy false prls t;
592 if t' = @{term True} then ()
593 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
594 (*... if this works, but --1-- does still NOT work, check types:*)
597 (*show_types:=true;*)
599 > val M_Match.NoMatch' {Given=gi, Where=wh, Find=fi,...} = M_Match.match_pbl fmz pbt;
600 val wh = [False "(t_::real => real) (is_polyexp::real)"]
601 ......................^^^^^^^^^^^^...............^^^^*)
602 val M_Match.Matches' _ = M_Match.match_pbl fmz pbt;
603 (*show_types:=false;*)
606 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
607 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
608 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
609 val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];
611 ("Poly",["polynomial", "simplification"],
612 ["simplification", "for_polynomials"]);
613 val p = e_pos'; val c = [];
614 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
615 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Given "Term\n ((5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n (3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1))"*)
616 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Add_Find "normalform N"*)
618 (*+* )if I_Model.to_string ctxt (get_obj g_pbl pt (fst p)) =
619 (*+*) "[\n(0 ,[] ,false ,#Find ,Inc ??.Simplify.normalform ,(??.empty, [])), \n(1 ,[1] ,true ,#Given ,Cor ??.Simplify.Term\n ((5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n (3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)) ,(t_t, [(5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n(3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)]))]"
620 (*+*)then () else error "No.267b: I_Model.T CHANGED";
621 ( *+ ...could not be repaired in child of 7e314dd233fd ?!?*)
623 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*nxt = Specify_Theory "Poly"*)
624 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Problem ["polynomial", "simplification"]*)
625 (*[], Pbl*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Specify_Method ["simplification", "for_polynomials"]*)
626 (*[], Met*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Apply_Method ["simplification", "for_polynomials"]*)
627 (*[1], Frm*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Rewrite_Set "norm_Poly"*)
629 (*+*)if f2str f = "(5 * x ^^^ 2 + 3) * (2 * x ^^^ 7 + 3) -\n(3 * x ^^^ 5 + 8) * (6 * x ^^^ 4 - 1)"
630 (*+*)then () else error "";
632 (*[1], Res*)val (p,_,f,nxt,_,pt) = me nxt p c pt;(*Empty_Tac: ERROR DETECTED Feb.2020*)
634 (*+*)if f2str f = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
635 (*+*)then () else error "";
637 (*[1], Res* )val (p,_,f,nxt,_,pt) = me nxt p c pt;( *SINCE Feb.2020 LItool.find_next_step without result*)
639 (*+*)if f2str f = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
640 (*+*)then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
643 "-------- interSteps for Schalk 299a --------------------";
644 "-------- interSteps for Schalk 299a --------------------";
645 "-------- interSteps for Schalk 299a --------------------";
648 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],
649 ("Poly",["polynomial", "simplification"],
650 ["simplification", "for_polynomials"]))];
653 autoCalculate 1 CompleteCalc;
654 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
656 interSteps 1 ([1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
657 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
658 if existpt' ([1,1], Frm) pt then ()
659 else error "poly.sml: interSteps doesnt work again 1";
661 interSteps 1 ([1,1],Res)(*<ERROR> syserror in Detail_Step.go </ERROR>*);
662 val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
663 (*============ inhibit exn WN120316 ==============================================
664 if existpt' ([1,1,1], Frm) pt then ()
665 else error "poly.sml: interSteps doesnt work again 2";
666 ============ inhibit exn WN120316 ==============================================*)
668 "-------- norm_Poly NOT COMPLETE ------------------------";
669 "-------- norm_Poly NOT COMPLETE ------------------------";
670 "-------- norm_Poly NOT COMPLETE ------------------------";
671 val thy = @{theory Simplify};
673 val SOME (f',_) = rewrite_set_ thy false norm_Poly
674 (str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
675 if UnparseC.term f' = "L = 2 * 2 * (k + -2 * q) + senkrecht + oben"
676 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
677 else error "norm_Poly changed behavior";
679 "-------- ord_make_polynomial ---------------------------";
680 "-------- ord_make_polynomial ---------------------------";
681 "-------- ord_make_polynomial ---------------------------";
682 val t1 = str2term "2 * b + (3 * a + 3 * b)";
683 val t2 = str2term "3 * a + 3 * b + 2 * b";
685 if ord_make_polynomial true thy [] (t1, t2) then ()
686 else error "poly.sml: diff.behav. in ord_make_polynomial";
688 (*WN071202: ^^^ why then is there no rewriting ...*)
689 val term = str2term "2*b + (3*a + 3*b)";
690 val NONE = rewrite_set_ (@{theory "Isac_Knowledge"}) false order_add_mult term;
692 (*or why is there no rewriting this way...*)
693 val t1 = str2term "2 * b + (3 * a + 3 * b)";
694 val t2 = str2term "3 * a + (2 * b + 3 * b)";