1 (*. (c) by Richard Lang, 2003 .*)
2 (* collecting all knowledge for PolynomialEquations
10 (* use"Knowledge/PolyEq.ML";
17 use_thy"Knowledge/Isac";
19 "******* PolyEq.ML begin *******";
21 theory' := overwritel (!theory', [("PolyEq.thy",PolyEq.thy)]);
22 (*-------------------------functions---------------------*)
24 (*-------------------------rulse-------------------------*)
25 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
26 append_rls "PolyEq_prls" e_rls
27 [Calc ("Atools.ident",eval_ident "#ident_"),
28 Calc ("Tools.matches",eval_matches ""),
29 Calc ("Tools.lhs" ,eval_lhs ""),
30 Calc ("Tools.rhs" ,eval_rhs ""),
31 Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
32 Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
33 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
34 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
35 (*Calc ("Atools.occurs'_in",eval_occurs_in ""), *)
36 (*Calc ("Atools.is'_const",eval_const "#is_const_"),*)
37 Calc ("op =",eval_equal "#equal_"),
38 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
39 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
40 Thm ("not_true",num_str not_true),
41 Thm ("not_false",num_str not_false),
42 Thm ("and_true",num_str and_true),
43 Thm ("and_false",num_str and_false),
44 Thm ("or_true",num_str or_true),
45 Thm ("or_false",num_str or_false)
49 merge_rls "PolyEq_erls" LinEq_erls
50 (append_rls "ops_preds" calculate_Rational
51 [Calc ("op =",eval_equal "#equal_"),
52 Thm ("plus_leq", num_str plus_leq),
53 Thm ("minus_leq", num_str minus_leq),
54 Thm ("rat_leq1", num_str rat_leq1),
55 Thm ("rat_leq2", num_str rat_leq2),
56 Thm ("rat_leq3", num_str rat_leq3)
60 merge_rls "PolyEq_crls" LinEq_crls
61 (append_rls "ops_preds" calculate_Rational
62 [Calc ("op =",eval_equal "#equal_"),
63 Thm ("plus_leq", num_str plus_leq),
64 Thm ("minus_leq", num_str minus_leq),
65 Thm ("rat_leq1", num_str rat_leq1),
66 Thm ("rat_leq2", num_str rat_leq2),
67 Thm ("rat_leq3", num_str rat_leq3)
70 val cancel_leading_coeff = prep_rls(
71 Rls {id = "cancel_leading_coeff", preconds = [],
72 rew_ord = ("e_rew_ord",e_rew_ord),
73 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
74 rules = [Thm ("cancel_leading_coeff1",num_str cancel_leading_coeff1),
75 Thm ("cancel_leading_coeff2",num_str cancel_leading_coeff2),
76 Thm ("cancel_leading_coeff3",num_str cancel_leading_coeff3),
77 Thm ("cancel_leading_coeff4",num_str cancel_leading_coeff4),
78 Thm ("cancel_leading_coeff5",num_str cancel_leading_coeff5),
79 Thm ("cancel_leading_coeff6",num_str cancel_leading_coeff6),
80 Thm ("cancel_leading_coeff7",num_str cancel_leading_coeff7),
81 Thm ("cancel_leading_coeff8",num_str cancel_leading_coeff8),
82 Thm ("cancel_leading_coeff9",num_str cancel_leading_coeff9),
83 Thm ("cancel_leading_coeff10",num_str cancel_leading_coeff10),
84 Thm ("cancel_leading_coeff11",num_str cancel_leading_coeff11),
85 Thm ("cancel_leading_coeff12",num_str cancel_leading_coeff12),
86 Thm ("cancel_leading_coeff13",num_str cancel_leading_coeff13)
88 scr = Script ((term_of o the o (parse thy))
92 val complete_square = prep_rls(
93 Rls {id = "complete_square", preconds = [],
94 rew_ord = ("e_rew_ord",e_rew_ord),
95 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
96 rules = [Thm ("complete_square1",num_str complete_square1),
97 Thm ("complete_square2",num_str complete_square2),
98 Thm ("complete_square3",num_str complete_square3),
99 Thm ("complete_square4",num_str complete_square4),
100 Thm ("complete_square5",num_str complete_square5)
102 scr = Script ((term_of o the o (parse thy))
106 val polyeq_simplify = prep_rls(
107 Rls {id = "polyeq_simplify", preconds = [],
108 rew_ord = ("termlessI",termlessI),
113 rules = [Thm ("real_assoc_1",num_str real_assoc_1),
114 Thm ("real_assoc_2",num_str real_assoc_2),
115 Thm ("real_diff_minus",num_str real_diff_minus),
116 Thm ("real_unari_minus",num_str real_unari_minus),
117 Thm ("realpow_multI",num_str realpow_multI),
118 Calc ("op +",eval_binop "#add_"),
119 Calc ("op -",eval_binop "#sub_"),
120 Calc ("op *",eval_binop "#mult_"),
121 Calc ("HOL.divide", eval_cancel "#divide_"),
122 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
123 Calc ("Atools.pow" ,eval_binop "#power_"),
126 scr = Script ((term_of o the o (parse thy)) "empty_script")
129 ruleset' := overwritelthy thy (!ruleset',
130 [("cancel_leading_coeff",cancel_leading_coeff),
131 ("complete_square",complete_square),
132 ("PolyEq_erls",PolyEq_erls),(*FIXXXME:del with rls.rls'*)
133 ("polyeq_simplify",polyeq_simplify)]);
136 (* ------------- polySolve ------------------ *)
138 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
139 val d0_polyeq_simplify = prep_rls(
140 Rls {id = "d0_polyeq_simplify", preconds = [],
141 rew_ord = ("e_rew_ord",e_rew_ord),
146 rules = [Thm("d0_true",num_str d0_true),
147 Thm("d0_false",num_str d0_false)
149 scr = Script ((term_of o the o (parse thy)) "empty_script")
153 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
154 val d1_polyeq_simplify = prep_rls(
155 Rls {id = "d1_polyeq_simplify", preconds = [],
156 rew_ord = ("e_rew_ord",e_rew_ord),
160 (*asm_thm = [("d1_isolate_div","")],*)
162 Thm("d1_isolate_add1",num_str d1_isolate_add1),
163 (* a+bx=0 -> bx=-a *)
164 Thm("d1_isolate_add2",num_str d1_isolate_add2),
166 Thm("d1_isolate_div",num_str d1_isolate_div)
169 scr = Script ((term_of o the o (parse thy)) "empty_script")
173 (* isolate the bound variable in an d2 equation with bdv only;
174 'bdv' is a meta-constant*)
175 val d2_polyeq_bdv_only_simplify = prep_rls(
176 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [],
177 rew_ord = ("e_rew_ord",e_rew_ord),
181 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
182 ("d2_isolate_div","")],*)
183 rules = [Thm("d2_prescind1",num_str d2_prescind1),
184 (* ax+bx^2=0 -> x(a+bx)=0 *)
185 Thm("d2_prescind2",num_str d2_prescind2),
186 (* ax+ x^2=0 -> x(a+ x)=0 *)
187 Thm("d2_prescind3",num_str d2_prescind3),
188 (* x+bx^2=0 -> x(1+bx)=0 *)
189 Thm("d2_prescind4",num_str d2_prescind4),
190 (* x+ x^2=0 -> x(1+ x)=0 *)
191 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
192 (* x^2=c -> x=+-sqrt(c)*)
193 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
194 (* [0<c] x^2=c -> [] *)
195 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
197 Thm("d2_reduce_equation1",num_str d2_reduce_equation1),
198 (* x(a+bx)=0 -> x=0 | a+bx=0*)
199 Thm("d2_reduce_equation2",num_str d2_reduce_equation2),
200 (* x(a+ x)=0 -> x=0 | a+ x=0*)
201 Thm("d2_isolate_div",num_str d2_isolate_div)
202 (* bx^2=c -> x^2=c/b*)
204 scr = Script ((term_of o the o (parse thy)) "empty_script")
207 (* isolate the bound variable in an d2 equation with sqrt only;
208 'bdv' is a meta-constant*)
209 val d2_polyeq_sq_only_simplify = prep_rls(
210 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
211 rew_ord = ("e_rew_ord",e_rew_ord),
215 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
216 ("d2_isolate_div","")],*)
217 rules = [Thm("d2_isolate_add1",num_str d2_isolate_add1),
218 (* a+ bx^2=0 -> bx^2=(-1)a*)
219 Thm("d2_isolate_add2",num_str d2_isolate_add2),
220 (* a+ x^2=0 -> x^2=(-1)a*)
221 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
223 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
224 (* x^2=c -> x=+-sqrt(c)*)
225 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
226 (* [c<0] x^2=c -> x=[] *)
227 Thm("d2_isolate_div",num_str d2_isolate_div)
228 (* bx^2=c -> x^2=c/b*)
230 scr = Script ((term_of o the o (parse thy)) "empty_script")
233 (* isolate the bound variable in an d2 equation with pqFormula;
234 'bdv' is a meta-constant*)
235 val d2_polyeq_pqFormula_simplify = prep_rls(
236 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
237 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
238 srls = Erls, calc = [],
239 rules = [Thm("d2_pqformula1",num_str d2_pqformula1),
241 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg),
243 Thm("d2_pqformula2",num_str d2_pqformula2),
245 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg),
247 Thm("d2_pqformula3",num_str d2_pqformula3),
249 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg),
251 Thm("d2_pqformula4",num_str d2_pqformula4),
253 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg),
255 Thm("d2_pqformula5",num_str d2_pqformula5),
257 Thm("d2_pqformula6",num_str d2_pqformula6),
259 Thm("d2_pqformula7",num_str d2_pqformula7),
261 Thm("d2_pqformula8",num_str d2_pqformula8),
263 Thm("d2_pqformula9",num_str d2_pqformula9),
265 Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg),
267 Thm("d2_pqformula10",num_str d2_pqformula10),
269 Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg),
271 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
273 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3)
276 scr = Script ((term_of o the o (parse thy)) "empty_script")
279 (* isolate the bound variable in an d2 equation with abcFormula;
280 'bdv' is a meta-constant*)
281 val d2_polyeq_abcFormula_simplify = prep_rls(
282 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
283 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
284 srls = Erls, calc = [],
285 rules = [Thm("d2_abcformula1",num_str d2_abcformula1),
287 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg),
289 Thm("d2_abcformula2",num_str d2_abcformula2),
291 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg),
293 Thm("d2_abcformula3",num_str d2_abcformula3),
295 Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg),
297 Thm("d2_abcformula4",num_str d2_abcformula4),
299 Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg),
301 Thm("d2_abcformula5",num_str d2_abcformula5),
303 Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg),
305 Thm("d2_abcformula6",num_str d2_abcformula6),
307 Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg),
309 Thm("d2_abcformula7",num_str d2_abcformula7),
311 Thm("d2_abcformula8",num_str d2_abcformula8),
313 Thm("d2_abcformula9",num_str d2_abcformula9),
315 Thm("d2_abcformula10",num_str d2_abcformula10),
317 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
319 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3)
322 scr = Script ((term_of o the o (parse thy)) "empty_script")
325 (* isolate the bound variable in an d2 equation;
326 'bdv' is a meta-constant*)
327 val d2_polyeq_simplify = prep_rls(
328 Rls {id = "d2_polyeq_simplify", preconds = [],
329 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
330 srls = Erls, calc = [],
331 rules = [Thm("d2_pqformula1",num_str d2_pqformula1),
333 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg),
335 Thm("d2_pqformula2",num_str d2_pqformula2),
337 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg),
339 Thm("d2_pqformula3",num_str d2_pqformula3),
341 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg),
343 Thm("d2_pqformula4",num_str d2_pqformula4),
345 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg),
347 Thm("d2_abcformula1",num_str d2_abcformula1),
349 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg),
351 Thm("d2_abcformula2",num_str d2_abcformula2),
353 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg),
355 Thm("d2_prescind1",num_str d2_prescind1),
356 (* ax+bx^2=0 -> x(a+bx)=0 *)
357 Thm("d2_prescind2",num_str d2_prescind2),
358 (* ax+ x^2=0 -> x(a+ x)=0 *)
359 Thm("d2_prescind3",num_str d2_prescind3),
360 (* x+bx^2=0 -> x(1+bx)=0 *)
361 Thm("d2_prescind4",num_str d2_prescind4),
362 (* x+ x^2=0 -> x(1+ x)=0 *)
363 Thm("d2_isolate_add1",num_str d2_isolate_add1),
364 (* a+ bx^2=0 -> bx^2=(-1)a*)
365 Thm("d2_isolate_add2",num_str d2_isolate_add2),
366 (* a+ x^2=0 -> x^2=(-1)a*)
367 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1),
368 (* x^2=c -> x=+-sqrt(c)*)
369 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),
370 (* [c<0] x^2=c -> x=[]*)
371 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2),
373 Thm("d2_reduce_equation1",num_str d2_reduce_equation1),
374 (* x(a+bx)=0 -> x=0 | a+bx=0*)
375 Thm("d2_reduce_equation2",num_str d2_reduce_equation2),
376 (* x(a+ x)=0 -> x=0 | a+ x=0*)
377 Thm("d2_isolate_div",num_str d2_isolate_div)
378 (* bx^2=c -> x^2=c/b*)
380 scr = Script ((term_of o the o (parse thy)) "empty_script")
384 (* isolate the bound variable in an d3 equation; 'bdv' is a meta-constant *)
385 val d3_polyeq_simplify = prep_rls(
386 Rls {id = "d3_polyeq_simplify", preconds = [],
387 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
388 srls = Erls, calc = [],
390 [Thm("d3_reduce_equation1",num_str d3_reduce_equation1),
391 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) =
392 (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*)
393 Thm("d3_reduce_equation2",num_str d3_reduce_equation2),
394 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) =
395 (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*)
396 Thm("d3_reduce_equation3",num_str d3_reduce_equation3),
397 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) =
398 (bdv=0 | (a + bdv + c*bdv^^^2=0)*)
399 Thm("d3_reduce_equation4",num_str d3_reduce_equation4),
400 (* bdv + bdv^^^2 + c*bdv^^^3=0) =
401 (bdv=0 | (1 + bdv + c*bdv^^^2=0)*)
402 Thm("d3_reduce_equation5",num_str d3_reduce_equation5),
403 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) =
404 (bdv=0 | (a + b*bdv + bdv^^^2=0)*)
405 Thm("d3_reduce_equation6",num_str d3_reduce_equation6),
406 (* bdv + b*bdv^^^2 + bdv^^^3=0) =
407 (bdv=0 | (1 + b*bdv + bdv^^^2=0)*)
408 Thm("d3_reduce_equation7",num_str d3_reduce_equation7),
409 (*a*bdv + bdv^^^2 + bdv^^^3=0) =
410 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
411 Thm("d3_reduce_equation8",num_str d3_reduce_equation8),
412 (* bdv + bdv^^^2 + bdv^^^3=0) =
413 (bdv=0 | (1 + bdv + bdv^^^2=0)*)
414 Thm("d3_reduce_equation9",num_str d3_reduce_equation9),
415 (*a*bdv + c*bdv^^^3=0) =
416 (bdv=0 | (a + c*bdv^^^2=0)*)
417 Thm("d3_reduce_equation10",num_str d3_reduce_equation10),
418 (* bdv + c*bdv^^^3=0) =
419 (bdv=0 | (1 + c*bdv^^^2=0)*)
420 Thm("d3_reduce_equation11",num_str d3_reduce_equation11),
421 (*a*bdv + bdv^^^3=0) =
422 (bdv=0 | (a + bdv^^^2=0)*)
423 Thm("d3_reduce_equation12",num_str d3_reduce_equation12),
424 (* bdv + bdv^^^3=0) =
425 (bdv=0 | (1 + bdv^^^2=0)*)
426 Thm("d3_reduce_equation13",num_str d3_reduce_equation13),
427 (* b*bdv^^^2 + c*bdv^^^3=0) =
428 (bdv=0 | ( b*bdv + c*bdv^^^2=0)*)
429 Thm("d3_reduce_equation14",num_str d3_reduce_equation14),
430 (* bdv^^^2 + c*bdv^^^3=0) =
431 (bdv=0 | ( bdv + c*bdv^^^2=0)*)
432 Thm("d3_reduce_equation15",num_str d3_reduce_equation15),
433 (* b*bdv^^^2 + bdv^^^3=0) =
434 (bdv=0 | ( b*bdv + bdv^^^2=0)*)
435 Thm("d3_reduce_equation16",num_str d3_reduce_equation16),
436 (* bdv^^^2 + bdv^^^3=0) =
437 (bdv=0 | ( bdv + bdv^^^2=0)*)
438 Thm("d3_isolate_add1",num_str d3_isolate_add1),
439 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) =
440 (bdv=0 | (b*bdv^^^3=a)*)
441 Thm("d3_isolate_add2",num_str d3_isolate_add2),
442 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) =
443 (bdv=0 | ( bdv^^^3=a)*)
444 Thm("d3_isolate_div",num_str d3_isolate_div),
445 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)
446 Thm("d3_root_equation2",num_str d3_root_equation2),
447 (*(bdv^^^3=0) = (bdv=0) *)
448 Thm("d3_root_equation1",num_str d3_root_equation1)
449 (*bdv^^^3=c) = (bdv = nroot 3 c*)
451 scr = Script ((term_of o the o (parse thy)) "empty_script")
455 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
456 val d4_polyeq_simplify = prep_rls(
457 Rls {id = "d4_polyeq_simplify", preconds = [],
458 rew_ord = ("e_rew_ord",e_rew_ord), erls = PolyEq_erls,
459 srls = Erls, calc = [],
461 [Thm("d4_sub_u1",num_str d4_sub_u1)
462 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
464 scr = Script ((term_of o the o (parse thy)) "empty_script")
470 [("d0_polyeq_simplify", d0_polyeq_simplify),
471 ("d1_polyeq_simplify", d1_polyeq_simplify),
472 ("d2_polyeq_simplify", d2_polyeq_simplify),
473 ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify),
474 ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify),
475 ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify),
476 ("d2_polyeq_abcFormula_simplify",
477 d2_polyeq_abcFormula_simplify),
478 ("d3_polyeq_simplify", d3_polyeq_simplify),
479 ("d4_polyeq_simplify", d4_polyeq_simplify)
482 (*------------------------problems------------------------*)
484 (get_pbt ["degree_2","polynomial","univariate","equation"]);
488 (*-------------------------poly-----------------------*)
490 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly" [] e_pblID
491 (["polynomial","univariate","equation"],
492 [("#Given" ,["equality e_","solveFor v_"]),
493 ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))",
494 "~((lhs e_) is_rootTerm_in (v_::real))",
495 "~((rhs e_) is_rootTerm_in (v_::real))"]),
496 ("#Find" ,["solutions v_i_"])
498 PolyEq_prls, SOME "solve (e_::bool, v_)",
502 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg0" [] e_pblID
503 (["degree_0","polynomial","univariate","equation"],
504 [("#Given" ,["equality e_","solveFor v_"]),
505 ("#Where" ,["matches (?a = 0) e_",
506 "(lhs e_) is_poly_in v_",
507 "((lhs e_) has_degree_in v_ ) = 0"
509 ("#Find" ,["solutions v_i_"])
511 PolyEq_prls, SOME "solve (e_::bool, v_)",
512 [["PolyEq","solve_d0_polyeq_equation"]]));
516 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg1" [] e_pblID
517 (["degree_1","polynomial","univariate","equation"],
518 [("#Given" ,["equality e_","solveFor v_"]),
519 ("#Where" ,["matches (?a = 0) e_",
520 "(lhs e_) is_poly_in v_",
521 "((lhs e_) has_degree_in v_ ) = 1"
523 ("#Find" ,["solutions v_i_"])
525 PolyEq_prls, SOME "solve (e_::bool, v_)",
526 [["PolyEq","solve_d1_polyeq_equation"]]));
530 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2" [] e_pblID
531 (["degree_2","polynomial","univariate","equation"],
532 [("#Given" ,["equality e_","solveFor v_"]),
533 ("#Where" ,["matches (?a = 0) e_",
534 "(lhs e_) is_poly_in v_ ",
535 "((lhs e_) has_degree_in v_ ) = 2"]),
536 ("#Find" ,["solutions v_i_"])
538 PolyEq_prls, SOME "solve (e_::bool, v_)",
539 [["PolyEq","solve_d2_polyeq_equation"]]));
542 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
543 (["sq_only","degree_2","polynomial","univariate","equation"],
544 [("#Given" ,["equality e_","solveFor v_"]),
545 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | " ^
546 "matches ( ?a + ?b*?v_^^^2 = 0) e_ | " ^
547 "matches ( ?v_^^^2 = 0) e_ | " ^
548 "matches ( ?b*?v_^^^2 = 0) e_" ,
549 "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &" ^
550 "Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &" ^
551 "Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &" ^
552 "Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_) &" ^
553 "Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &" ^
554 "Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &" ^
555 "Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &" ^
556 "Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_)"]),
557 ("#Find" ,["solutions v_i_"])
559 PolyEq_prls, SOME "solve (e_::bool, v_)",
560 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
563 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
564 (["bdv_only","degree_2","polynomial","univariate","equation"],
565 [("#Given" ,["equality e_","solveFor v_"]),
566 ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | " ^
567 "matches ( ?v_ + ?v_^^^2 = 0) e_ | " ^
568 "matches ( ?v_ + ?b*?v_^^^2 = 0) e_ | " ^
569 "matches (?a*?v_ + ?b*?v_^^^2 = 0) e_ | " ^
570 "matches ( ?v_^^^2 = 0) e_ | " ^
571 "matches ( ?b*?v_^^^2 = 0) e_ "]),
572 ("#Find" ,["solutions v_i_"])
574 PolyEq_prls, SOME "solve (e_::bool, v_)",
575 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
578 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_pq" [] e_pblID
579 (["pqFormula","degree_2","polynomial","univariate","equation"],
580 [("#Given" ,["equality e_","solveFor v_"]),
581 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | " ^
582 "matches (?a + ?v_^^^2 = 0) e_"]),
583 ("#Find" ,["solutions v_i_"])
585 PolyEq_prls, SOME "solve (e_::bool, v_)",
586 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
589 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg2_abc" [] e_pblID
590 (["abcFormula","degree_2","polynomial","univariate","equation"],
591 [("#Given" ,["equality e_","solveFor v_"]),
592 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | " ^
593 "matches (?a + ?b*?v_^^^2 = 0) e_"]),
594 ("#Find" ,["solutions v_i_"])
596 PolyEq_prls, SOME "solve (e_::bool, v_)",
597 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
601 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg3" [] e_pblID
602 (["degree_3","polynomial","univariate","equation"],
603 [("#Given" ,["equality e_","solveFor v_"]),
604 ("#Where" ,["matches (?a = 0) e_",
605 "(lhs e_) is_poly_in v_ ",
606 "((lhs e_) has_degree_in v_) = 3"]),
607 ("#Find" ,["solutions v_i_"])
609 PolyEq_prls, SOME "solve (e_::bool, v_)",
610 [["PolyEq","solve_d3_polyeq_equation"]]));
614 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_deg4" [] e_pblID
615 (["degree_4","polynomial","univariate","equation"],
616 [("#Given" ,["equality e_","solveFor v_"]),
617 ("#Where" ,["matches (?a = 0) e_",
618 "(lhs e_) is_poly_in v_ ",
619 "((lhs e_) has_degree_in v_) = 4"]),
620 ("#Find" ,["solutions v_i_"])
622 PolyEq_prls, SOME "solve (e_::bool, v_)",
623 [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
625 (*--- normalize ---*)
627 (prep_pbt (theory "PolyEq") "pbl_equ_univ_poly_norm" [] e_pblID
628 (["normalize","polynomial","univariate","equation"],
629 [("#Given" ,["equality e_","solveFor v_"]),
630 ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |" ^
631 "(Not(((lhs e_) is_poly_in v_)))"]),
632 ("#Find" ,["solutions v_i_"])
634 PolyEq_prls, SOME "solve (e_::bool, v_)",
635 [["PolyEq","normalize_poly"]]));
636 (*-------------------------expanded-----------------------*)
638 (prep_pbt (theory "PolyEq") "pbl_equ_univ_expand" [] e_pblID
639 (["expanded","univariate","equation"],
640 [("#Given" ,["equality e_","solveFor v_"]),
641 ("#Where" ,["matches (?a = 0) e_",
642 "(lhs e_) is_expanded_in v_ "]),
643 ("#Find" ,["solutions v_i_"])
645 PolyEq_prls, SOME "solve (e_::bool, v_)",
650 (prep_pbt (theory "PolyEq") "pbl_equ_univ_expand_deg2" [] e_pblID
651 (["degree_2","expanded","univariate","equation"],
652 [("#Given" ,["equality e_","solveFor v_"]),
653 ("#Where" ,["((lhs e_) has_degree_in v_) = 2"]),
654 ("#Find" ,["solutions v_i_"])
656 PolyEq_prls, SOME "solve (e_::bool, v_)",
657 [["PolyEq","complete_square"]]));
660 "-------------------------methods-----------------------";
662 (prep_met (theory "PolyEq") "met_polyeq" [] e_metID
665 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
666 crls=PolyEq_crls, nrls=norm_Rational}, "empty_script"));
669 (prep_met (theory "PolyEq") "met_polyeq_norm" [] e_metID
670 (["PolyEq","normalize_poly"],
671 [("#Given" ,["equality e_","solveFor v_"]),
672 ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |" ^
673 "(Not(((lhs e_) is_poly_in v_)))"]),
674 ("#Find" ,["solutions v_i_"])
676 {rew_ord'="termlessI",
681 crls=PolyEq_crls, nrls=norm_Rational
682 "Script Normalize_poly (e_::bool) (v_::real) = " ^
683 "(let e_ =((Try (Rewrite all_left False)) @@ " ^
684 " (Try (Repeat (Rewrite makex1_x False))) @@ " ^
685 " (Try (Repeat (Rewrite_Set expand_binoms False))) @@ " ^
686 " (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] " ^
687 " make_ratpoly_in False))) @@ " ^
688 " (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_ " ^
689 " in (SubProblem (PolyEq_,[polynomial,univariate,equation], " ^
690 " [no_met]) [bool_ e_, real_ v_]))"
694 (prep_met (theory "PolyEq") "met_polyeq_d0" [] e_metID
695 (["PolyEq","solve_d0_polyeq_equation"],
696 [("#Given" ,["equality e_","solveFor v_"]),
697 ("#Where" ,["(lhs e_) is_poly_in v_ ",
698 "((lhs e_) has_degree_in v_) = 0"]),
699 ("#Find" ,["solutions v_i_"])
701 {rew_ord'="termlessI",
705 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
706 crls=PolyEq_crls, nrls=norm_Rational},
707 "Script Solve_d0_polyeq_equation (e_::bool) (v_::real) = " ^
708 "(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
709 " d0_polyeq_simplify False))) e_ " ^
710 " in ((Or_to_List e_)::bool list))"
714 (prep_met (theory "PolyEq") "met_polyeq_d1" [] e_metID
715 (["PolyEq","solve_d1_polyeq_equation"],
716 [("#Given" ,["equality e_","solveFor v_"]),
717 ("#Where" ,["(lhs e_) is_poly_in v_ ",
718 "((lhs e_) has_degree_in v_) = 1"]),
719 ("#Find" ,["solutions v_i_"])
721 {rew_ord'="termlessI",
725 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
726 crls=PolyEq_crls, nrls=norm_Rational(*,
727 (* asm_rls=["d1_polyeq_simplify"],*)
729 asm_thm=[("d1_isolate_div","")]*)},
730 "Script Solve_d1_polyeq_equation (e_::bool) (v_::real) = " ^
731 "(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
732 " d1_polyeq_simplify True)) @@ " ^
733 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
734 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
735 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
736 " in Check_elementwise L_ {(v_::real). Assumptions} )"
740 (prep_met (theory "PolyEq") "met_polyeq_d22" [] e_metID
741 (["PolyEq","solve_d2_polyeq_equation"],
742 [("#Given" ,["equality e_","solveFor v_"]),
743 ("#Where" ,["(lhs e_) is_poly_in v_ ",
744 "((lhs e_) has_degree_in v_) = 2"]),
745 ("#Find" ,["solutions v_i_"])
747 {rew_ord'="termlessI",
751 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
752 crls=PolyEq_crls, nrls=norm_Rational},
753 "Script Solve_d2_polyeq_equation (e_::bool) (v_::real) = " ^
754 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
755 " d2_polyeq_simplify True)) @@ " ^
756 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
757 " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
758 " d1_polyeq_simplify True)) @@ " ^
759 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
760 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
761 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
762 " in Check_elementwise L_ {(v_::real). Assumptions} )"
766 (prep_met (theory "PolyEq") "met_polyeq_d2_bdvonly" [] e_metID
767 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
768 [("#Given" ,["equality e_","solveFor v_"]),
769 ("#Where" ,["(lhs e_) is_poly_in v_ ",
770 "((lhs e_) has_degree_in v_) = 2"]),
771 ("#Find" ,["solutions v_i_"])
773 {rew_ord'="termlessI",
777 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
778 crls=PolyEq_crls, nrls=norm_Rational},
779 "Script Solve_d2_polyeq_bdvonly_equation (e_::bool) (v_::real) =" ^
780 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
781 " d2_polyeq_bdv_only_simplify True)) @@ " ^
782 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
783 " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
784 " d1_polyeq_simplify True)) @@ " ^
785 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
786 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
787 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
788 " in Check_elementwise L_ {(v_::real). Assumptions} )"
792 (prep_met (theory "PolyEq") "met_polyeq_d2_sqonly" [] e_metID
793 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
794 [("#Given" ,["equality e_","solveFor v_"]),
795 ("#Where" ,["(lhs e_) is_poly_in v_ ",
796 "((lhs e_) has_degree_in v_) = 2"]),
797 ("#Find" ,["solutions v_i_"])
799 {rew_ord'="termlessI",
803 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
804 crls=PolyEq_crls, nrls=norm_Rational},
805 "Script Solve_d2_polyeq_sqonly_equation (e_::bool) (v_::real) =" ^
806 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
807 " d2_polyeq_sq_only_simplify True)) @@ " ^
808 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
809 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_; " ^
810 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
811 " in Check_elementwise L_ {(v_::real). Assumptions} )"
815 (prep_met (theory "PolyEq") "met_polyeq_d2_pq" [] e_metID
816 (["PolyEq","solve_d2_polyeq_pq_equation"],
817 [("#Given" ,["equality e_","solveFor v_"]),
818 ("#Where" ,["(lhs e_) is_poly_in v_ ",
819 "((lhs e_) has_degree_in v_) = 2"]),
820 ("#Find" ,["solutions v_i_"])
822 {rew_ord'="termlessI",
826 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
827 crls=PolyEq_crls, nrls=norm_Rational},
828 "Script Solve_d2_polyeq_pq_equation (e_::bool) (v_::real) = " ^
829 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
830 " d2_polyeq_pqFormula_simplify True)) @@ " ^
831 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
832 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
833 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
834 " in Check_elementwise L_ {(v_::real). Assumptions} )"
838 (prep_met (theory "PolyEq") "met_polyeq_d2_abc" [] e_metID
839 (["PolyEq","solve_d2_polyeq_abc_equation"],
840 [("#Given" ,["equality e_","solveFor v_"]),
841 ("#Where" ,["(lhs e_) is_poly_in v_ ",
842 "((lhs e_) has_degree_in v_) = 2"]),
843 ("#Find" ,["solutions v_i_"])
845 {rew_ord'="termlessI",
849 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
850 crls=PolyEq_crls, nrls=norm_Rational},
851 "Script Solve_d2_polyeq_abc_equation (e_::bool) (v_::real) = " ^
852 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
853 " d2_polyeq_abcFormula_simplify True)) @@ " ^
854 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
855 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
856 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
857 " in Check_elementwise L_ {(v_::real). Assumptions} )"
861 (prep_met (theory "PolyEq") "met_polyeq_d3" [] e_metID
862 (["PolyEq","solve_d3_polyeq_equation"],
863 [("#Given" ,["equality e_","solveFor v_"]),
864 ("#Where" ,["(lhs e_) is_poly_in v_ ",
865 "((lhs e_) has_degree_in v_) = 3"]),
866 ("#Find" ,["solutions v_i_"])
868 {rew_ord'="termlessI",
872 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
873 crls=PolyEq_crls, nrls=norm_Rational},
874 "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = " ^
875 " (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
876 " d3_polyeq_simplify True)) @@ " ^
877 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
878 " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
879 " d2_polyeq_simplify True)) @@ " ^
880 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
881 " (Try (Rewrite_Set_Inst [(bdv,v_::real)] " ^
882 " d1_polyeq_simplify True)) @@ " ^
883 " (Try (Rewrite_Set polyeq_simplify False)) @@ " ^
884 " (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;" ^
885 " (L_::bool list) = ((Or_to_List e_)::bool list) " ^
886 " in Check_elementwise L_ {(v_::real). Assumptions} )"
889 (*.solves all expanded (ie. normalized) terms of degree 2.*)
890 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
891 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
893 (prep_met (theory "PolyEq") "met_polyeq_complsq" [] e_metID
894 (["PolyEq","complete_square"],
895 [("#Given" ,["equality e_","solveFor v_"]),
896 ("#Where" ,["matches (?a = 0) e_",
897 "((lhs e_) has_degree_in v_) = 2"]),
898 ("#Find" ,["solutions v_i_"])
900 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
901 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
902 crls=PolyEq_crls, nrls=norm_Rational},
903 "Script Complete_square (e_::bool) (v_::real) = " ^
904 "(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))" ^
905 " @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) " ^
906 " @@ (Try (Rewrite square_explicit1 False)) " ^
907 " @@ (Try (Rewrite square_explicit2 False)) " ^
908 " @@ (Rewrite root_plus_minus True) " ^
909 " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) " ^
910 " @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) " ^
911 " @@ (Try (Repeat " ^
912 " (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) " ^
913 " @@ (Try (Rewrite_Set calculate_RootRat False)) " ^
914 " @@ (Try (Repeat (Calculate sqrt_)))) e_ " ^
915 " in ((Or_to_List e_)::bool list))"
919 (* termorder hacked by MG *)
920 local (*. for make_polynomial_in .*)
922 open Term; (* for type order = EQUAL | LESS | GREATER *)
924 fun pr_ord EQUAL = "EQUAL"
925 | pr_ord LESS = "LESS"
926 | pr_ord GREATER = "GREATER";
928 fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
929 | dest_hd' x (t as Free (a, T)) =
930 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
931 else (((a, 0), T), 1)
932 | dest_hd' x (Var v) = (v, 2)
933 | dest_hd' x (Bound i) = ((("", i), dummyT), 3)
934 | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
936 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =
939 (if xstr = var then 1000*(the (int_of_str pot)) else 3)
940 | _ => raise error ("size_of_term' called with subst = "^
942 | size_of_term' x (Free (subst,_)) =
944 (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
945 | _ => raise error ("size_of_term' called with subst = "^
947 | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
948 | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
949 | size_of_term' x _ = 1;
952 fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
953 (case term_ord' x pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
954 | term_ord' x pr thy (t, u) =
957 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
958 val _=writeln("t= f@ts= \""^
959 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
960 (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
961 val _=writeln("u= g@us= \""^
962 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
963 (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
964 val _=writeln("size_of_term(t,u)= ("^
965 (string_of_int(size_of_term' x t))^", "^
966 (string_of_int(size_of_term' x u))^")");
967 val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
968 val _=writeln("terms_ord(ts,us) = "^
969 ((pr_ord o (terms_ord x) str false)(ts,us)));
970 val _=writeln("-------");
973 case int_ord (size_of_term' x t, size_of_term' x u) of
975 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
976 (case hd_ord x (f, g) of EQUAL => (terms_ord x str pr) (ts, us)
980 and hd_ord x (f, g) = (* ~ term.ML *)
981 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' x f,
983 and terms_ord x str pr (ts, us) =
984 list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us);
987 fun ord_make_polynomial_in (pr:bool) thy subst tu =
989 (* val _=writeln("*** subs variable is: "^(subst2str subst)); *)
992 (_,x)::_ => (term_ord' x pr thy tu = LESS)
993 | _ => raise error ("ord_make_polynomial_in called with subst = "^
998 val order_add_mult_in = prep_rls(
999 Rls{id = "order_add_mult_in", preconds = [],
1000 rew_ord = ("ord_make_polynomial_in",
1001 ord_make_polynomial_in false Poly.thy),
1002 erls = e_rls,srls = Erls,
1005 rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1007 Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1008 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1009 Thm ("real_mult_assoc",num_str real_mult_assoc),
1010 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1011 Thm ("real_add_commute",num_str real_add_commute),
1013 Thm ("real_add_left_commute",num_str real_add_left_commute),
1014 (*x + (y + z) = y + (x + z)*)
1015 Thm ("real_add_assoc",num_str real_add_assoc)
1016 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1017 ], scr = EmptyScr}:rls);
1019 val collect_bdv = prep_rls(
1020 Rls{id = "collect_bdv", preconds = [],
1021 rew_ord = ("dummy_ord", dummy_ord),
1022 erls = e_rls,srls = Erls,
1025 rules = [Thm ("bdv_collect_1",num_str bdv_collect_1),
1026 Thm ("bdv_collect_2",num_str bdv_collect_2),
1027 Thm ("bdv_collect_3",num_str bdv_collect_3),
1029 Thm ("bdv_collect_assoc1_1",num_str bdv_collect_assoc1_1),
1030 Thm ("bdv_collect_assoc1_2",num_str bdv_collect_assoc1_2),
1031 Thm ("bdv_collect_assoc1_3",num_str bdv_collect_assoc1_3),
1033 Thm ("bdv_collect_assoc2_1",num_str bdv_collect_assoc2_1),
1034 Thm ("bdv_collect_assoc2_2",num_str bdv_collect_assoc2_2),
1035 Thm ("bdv_collect_assoc2_3",num_str bdv_collect_assoc2_3),
1038 Thm ("bdv_n_collect_1",num_str bdv_n_collect_1),
1039 Thm ("bdv_n_collect_2",num_str bdv_n_collect_2),
1040 Thm ("bdv_n_collect_3",num_str bdv_n_collect_3),
1042 Thm ("bdv_n_collect_assoc1_1",num_str bdv_n_collect_assoc1_1),
1043 Thm ("bdv_n_collect_assoc1_2",num_str bdv_n_collect_assoc1_2),
1044 Thm ("bdv_n_collect_assoc1_3",num_str bdv_n_collect_assoc1_3),
1046 Thm ("bdv_n_collect_assoc2_1",num_str bdv_n_collect_assoc2_1),
1047 Thm ("bdv_n_collect_assoc2_2",num_str bdv_n_collect_assoc2_2),
1048 Thm ("bdv_n_collect_assoc2_3",num_str bdv_n_collect_assoc2_3)
1049 ], scr = EmptyScr}:rls);
1051 (*.transforms an arbitrary term without roots to a polynomial [4]
1052 according to knowledge/Poly.sml.*)
1053 val make_polynomial_in = prep_rls(
1054 Seq {id = "make_polynomial_in", preconds = []:term list,
1055 rew_ord = ("dummy_ord", dummy_ord),
1056 erls = Atools_erls, srls = Erls,
1057 calc = [], (*asm_thm = [],*)
1058 rules = [Rls_ expand_poly,
1059 Rls_ order_add_mult_in,
1060 Rls_ simplify_power,
1061 Rls_ collect_numerals,
1063 Thm ("realpow_oneI",num_str realpow_oneI),
1064 Rls_ discard_parentheses,
1071 append_rls "separate_bdvs"
1073 [Thm ("separate_bdv", num_str separate_bdv),
1074 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1075 Thm ("separate_bdv_n", num_str separate_bdv_n),
1076 Thm ("separate_1_bdv", num_str separate_1_bdv),
1077 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1078 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
1079 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1080 Thm ("real_add_divide_distrib",
1081 num_str real_add_divide_distrib)
1082 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1083 WN051031 DOES NOT BELONG TO HERE*)
1085 val make_ratpoly_in = prep_rls(
1086 Seq {id = "make_ratpoly_in", preconds = []:term list,
1087 rew_ord = ("dummy_ord", dummy_ord),
1088 erls = Atools_erls, srls = Erls,
1089 calc = [], (*asm_thm = [],*)
1090 rules = [Rls_ norm_Rational,
1091 Rls_ order_add_mult_in,
1092 Rls_ discard_parentheses,
1094 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
1096 (*Calc ("HOL.divide" ,eval_cancel "#divide_") too weak!*)
1098 scr = EmptyScr}:rls);
1101 ruleset' := overwritelthy thy (!ruleset',
1102 [("order_add_mult_in", order_add_mult_in),
1103 ("collect_bdv", collect_bdv),
1104 ("make_polynomial_in", make_polynomial_in),
1105 ("make_ratpoly_in", make_ratpoly_in),
1106 ("separate_bdvs", separate_bdvs)