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---------------------*)
25 fun add0 l d d_ = if (d_+1) < d then add0 (str2term"0"::l) d (d_+1) else l;
26 fun poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("Atools.pow",_) $ v_ $ Free (d_,_)))) v l d =
28 then poly2list_ t1 v (((str2term("1")))::(add0 l d (int_of_str' d_))) (int_of_str' d_)
30 | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $
31 (Const ("Atools.pow",_) $ v_ $ Free (d_,_))))) v l d =
33 then poly2list_ t1 v (((t11))::(add0 l d (int_of_str' d_))) (int_of_str' d_)
35 | poly2list_ (t as (Const ("op +",_) $ t1 $ (Free (v_ , _)) )) v l d =
36 if (v = (str2term v_))
37 then poly2list_ t1 v (((str2term("1")))::(add0 l d 1 )) 1
39 | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ (Free (v_,_)) ))) v l d =
41 then poly2list_ t1 v ( (t11)::(add0 l d 1 )) 1
43 | poly2list_ (t as (Const ("op +",_) $ _ $ _))_ l d = t::(add0 l d 0)
44 | poly2list_ (t as (Free (_,_))) _ l d = t::(add0 l d 0)
45 | poly2list_ t _ l d = t::(add0 l d 0);
47 fun poly2list t v = poly2list_ t v [] 0;
48 fun diffpolylist_ [] _ = []
49 | diffpolylist_ (x::xs) d = (str2term (if term2str(x)="0"
51 else term2str(x)^"*"^str_of_int(d)))::diffpolylist_ xs (d+1);
52 fun diffpolylist [] = []
53 | diffpolylist (x::xs) = diffpolylist_ xs 1;
54 (* diffpolylist(poly2list (str2term "1+ x +3*x^^^3") (str2term "x"));*)
59 (*-------------------------rulse-------------------------*)
60 val PolyEq_prls = (*3.10.02:just the following order due to subterm evaluation*)
61 append_rls "PolyEq_prls" e_rls
62 [Calc ("Atools.ident",eval_ident "#ident_"),
63 Calc ("Tools.matches",eval_matches ""),
64 Calc ("Tools.lhs" ,eval_lhs ""),
65 Calc ("Tools.rhs" ,eval_rhs ""),
66 Calc ("Poly.is'_expanded'_in",eval_is_expanded_in ""),
67 Calc ("Poly.is'_poly'_in",eval_is_poly_in ""),
68 Calc ("Poly.has'_degree'_in",eval_has_degree_in ""),
69 Calc ("Poly.is'_polyrat'_in",eval_is_polyrat_in ""),
70 (*Calc ("Atools.occurs'_in",eval_occurs_in ""), *)
71 (*Calc ("Atools.is'_const",eval_const "#is_const_"),*)
72 Calc ("op =",eval_equal "#equal_"),
73 Calc ("RootEq.is'_rootTerm'_in",eval_is_rootTerm_in ""),
74 Calc ("RatEq.is'_ratequation'_in",eval_is_ratequation_in ""),
75 Thm ("not_true",num_str not_true),
76 Thm ("not_false",num_str not_false),
77 Thm ("and_true",num_str and_true),
78 Thm ("and_false",num_str and_false),
79 Thm ("or_true",num_str or_true),
80 Thm ("or_false",num_str or_false)
84 merge_rls "PolyEq_erls" LinEq_erls
85 (append_rls "ops_preds" calculate_Rational
86 [Calc ("op =",eval_equal "#equal_"),
87 Thm ("plus_leq", num_str plus_leq),
88 Thm ("minus_leq", num_str minus_leq),
89 Thm ("rat_leq1", num_str rat_leq1),
90 Thm ("rat_leq2", num_str rat_leq2),
91 Thm ("rat_leq3", num_str rat_leq3)
95 merge_rls "PolyEq_crls" LinEq_crls
96 (append_rls "ops_preds" calculate_Rational
97 [Calc ("op =",eval_equal "#equal_"),
98 Thm ("plus_leq", num_str plus_leq),
99 Thm ("minus_leq", num_str minus_leq),
100 Thm ("rat_leq1", num_str rat_leq1),
101 Thm ("rat_leq2", num_str rat_leq2),
102 Thm ("rat_leq3", num_str rat_leq3)
106 merge_rls "PolyEq_erls"
107 (append_rls "" (Rls {(*asm_thm=[],*)calc=[],
108 erls= Rls {(*asm_thm=[],*)calc=[],
110 id="e_rls",preconds=[],
111 rew_ord=("dummy_ord",dummy_ord),
119 scr=EmptyScr,srls=Erls},
120 id="e_rls",preconds=[],rew_ord=("dummy_ord",
122 rules=[],scr=EmptyScr,srls=Erls}
124 ((#rules o rep_rls) LinEq_erls))
125 (append_rls "ops_preds" calculate_Rational
126 [Calc ("op =",eval_equal "#equal_"),
127 Thm ("plus_leq", num_str plus_leq),
128 Thm ("minus_leq", num_str minus_leq),
129 Thm ("rat_leq1", num_str rat_leq1),
130 Thm ("rat_leq2", num_str rat_leq2),
131 Thm ("rat_leq3", num_str rat_leq3)
136 val cancel_leading_coeff = prep_rls(
137 Rls {id = "cancel_leading_coeff", preconds = [],
138 rew_ord = ("e_rew_ord",e_rew_ord),
139 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
140 rules = [Thm ("cancel_leading_coeff1",num_str cancel_leading_coeff1),
141 Thm ("cancel_leading_coeff2",num_str cancel_leading_coeff2),
142 Thm ("cancel_leading_coeff3",num_str cancel_leading_coeff3),
143 Thm ("cancel_leading_coeff4",num_str cancel_leading_coeff4),
144 Thm ("cancel_leading_coeff5",num_str cancel_leading_coeff5),
145 Thm ("cancel_leading_coeff6",num_str cancel_leading_coeff6),
146 Thm ("cancel_leading_coeff7",num_str cancel_leading_coeff7),
147 Thm ("cancel_leading_coeff8",num_str cancel_leading_coeff8),
148 Thm ("cancel_leading_coeff9",num_str cancel_leading_coeff9),
149 Thm ("cancel_leading_coeff10",num_str cancel_leading_coeff10),
150 Thm ("cancel_leading_coeff11",num_str cancel_leading_coeff11),
151 Thm ("cancel_leading_coeff12",num_str cancel_leading_coeff12),
152 Thm ("cancel_leading_coeff13",num_str cancel_leading_coeff13)
154 scr = Script ((term_of o the o (parse thy))
157 val complete_square = prep_rls(
158 Rls {id = "complete_square", preconds = [],
159 rew_ord = ("e_rew_ord",e_rew_ord),
160 erls = PolyEq_erls, srls = Erls, calc = [], (*asm_thm = [],*)
161 rules = [Thm ("complete_square1",num_str complete_square1),
162 Thm ("complete_square2",num_str complete_square2),
163 Thm ("complete_square3",num_str complete_square3),
164 Thm ("complete_square4",num_str complete_square4),
165 Thm ("complete_square5",num_str complete_square5)
167 scr = Script ((term_of o the o (parse thy))
170 ruleset' := overwritelthy thy (!ruleset',
171 [("cancel_leading_coeff",cancel_leading_coeff),
172 ("complete_square",complete_square),
173 ("PolyEq_erls",PolyEq_erls)(*FIXXXME:del with rls.rls'*)
175 val polyeq_simplify = prep_rls(
176 Rls {id = "polyeq_simplify", preconds = [],
177 rew_ord = ("termlessI",termlessI),
182 rules = [Thm ("real_assoc_1",num_str real_assoc_1),
183 Thm ("real_assoc_2",num_str real_assoc_2),
184 Thm ("real_diff_minus",num_str real_diff_minus),
185 Thm ("real_unari_minus",num_str real_unari_minus),
186 Thm ("realpow_multI",num_str realpow_multI),
187 Calc ("op +",eval_binop "#add_"),
188 Calc ("op -",eval_binop "#sub_"),
189 Calc ("op *",eval_binop "#mult_"),
190 Calc ("HOL.divide", eval_cancel "#divide_"),
191 Calc ("Root.sqrt",eval_sqrt "#sqrt_"),
192 Calc ("Atools.pow" ,eval_binop "#power_"),
195 scr = Script ((term_of o the o (parse thy)) "empty_script")
197 ruleset' := overwritelthy thy (!ruleset',
198 [("polyeq_simplify",polyeq_simplify)]);
201 (* ------------- polySolve ------------------ *)
203 (*isolate the bound variable in an d0 equation; 'bdv' is a meta-constant*)
204 val d0_polyeq_simplify = prep_rls(
205 Rls {id = "d0_polyeq_simplify", preconds = [],
206 rew_ord = ("e_rew_ord",e_rew_ord),
211 rules = [Thm("d0_true",num_str d0_true),
212 Thm("d0_false",num_str d0_false)
214 scr = Script ((term_of o the o (parse thy)) "empty_script")
217 (*isolate the bound variable in an d1 equation; 'bdv' is a meta-constant*)
218 val d1_polyeq_simplify = prep_rls(
219 Rls {id = "d1_polyeq_simplify", preconds = [],
220 rew_ord = ("e_rew_ord",e_rew_ord),
224 (*asm_thm = [("d1_isolate_div","")],*)
226 Thm("d1_isolate_add1",num_str d1_isolate_add1),
227 (* a+bx=0 -> bx=-a *)
228 Thm("d1_isolate_add2",num_str d1_isolate_add2),
230 Thm("d1_isolate_div",num_str d1_isolate_div)
233 scr = Script ((term_of o the o (parse thy)) "empty_script")
236 (*isolate the bound variable in an d2 equation with bdv only; 'bdv' is a meta-constant*)
237 val d2_polyeq_bdv_only_simplify = prep_rls(
238 Rls {id = "d2_polyeq_bdv_only_simplify", preconds = [],
239 rew_ord = ("e_rew_ord",e_rew_ord),
243 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
244 ("d2_isolate_div","")],*)
246 Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *)
247 Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *)
248 Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *)
249 Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *)
250 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*)
251 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg), (* [0<c] x^2=c -> [] *)
252 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *)
253 Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*)
254 Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*)
255 Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*)
257 scr = Script ((term_of o the o (parse thy)) "empty_script")
259 (*isolate the bound variable in an d2 equation with sqrt only; 'bdv' is a meta-constant*)
260 val d2_polyeq_sq_only_simplify = prep_rls(
261 Rls {id = "d2_polyeq_sq_only_simplify", preconds = [],
262 rew_ord = ("e_rew_ord",e_rew_ord),
266 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
267 ("d2_isolate_div","")],*)
269 Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*)
270 Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*)
271 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *)
272 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*)
273 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),(* [c<0] x^2=c -> x=[] *)
274 Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*)
276 scr = Script ((term_of o the o (parse thy)) "empty_script")
278 (*isolate the bound variable in an d2 equation with pqFormula; 'bdv' is a meta-constant*)
279 val d2_polyeq_pqFormula_simplify = prep_rls(
280 Rls {id = "d2_polyeq_pqFormula_simplify", preconds = [],
281 rew_ord = ("e_rew_ord",e_rew_ord),
285 (*asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
286 ("d2_pqformula5",""),("d2_pqformula6",""),("d2_pqformula7",""),("d2_pqformula8",""),
287 ("d2_pqformula9",""),("d2_pqformula10",""),
288 ("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),("d2_pqformula3_neg",""),
289 ("d2_pqformula4_neg",""),("d2_pqformula9_neg",""),("d2_pqformula10_neg","")],*)
291 Thm("d2_pqformula1",num_str d2_pqformula1), (* q+px+ x^2=0 *)
292 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), (* q+px+ x^2=0 *)
293 Thm("d2_pqformula2",num_str d2_pqformula2), (* q+px+1x^2=0 *)
294 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), (* q+px+1x^2=0 *)
295 Thm("d2_pqformula3",num_str d2_pqformula3), (* q+ x+ x^2=0 *)
296 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), (* q+ x+ x^2=0 *)
297 Thm("d2_pqformula4",num_str d2_pqformula4), (* q+ x+1x^2=0 *)
298 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), (* q+ x+1x^2=0 *)
299 Thm("d2_pqformula5",num_str d2_pqformula5), (* qx+ x^2=0 *)
300 Thm("d2_pqformula6",num_str d2_pqformula6), (* qx+1x^2=0 *)
301 Thm("d2_pqformula7",num_str d2_pqformula7), (* x+ x^2=0 *)
302 Thm("d2_pqformula8",num_str d2_pqformula8), (* x+1x^2=0 *)
303 Thm("d2_pqformula9",num_str d2_pqformula9), (* q +1x^2=0 *)
304 Thm("d2_pqformula9_neg",num_str d2_pqformula9_neg), (* q +1x^2=0 *)
305 Thm("d2_pqformula10",num_str d2_pqformula10), (* q + x^2=0 *)
306 Thm("d2_pqformula10_neg",num_str d2_pqformula10_neg), (* q + x^2=0 *)
307 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *)
308 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* 1x^2=0 *)
310 scr = Script ((term_of o the o (parse thy)) "empty_script")
312 (*isolate the bound variable in an d2 equation with abcFormula; 'bdv' is a meta-constant*)
313 val d2_polyeq_abcFormula_simplify = prep_rls(
314 Rls {id = "d2_polyeq_abcFormula_simplify", preconds = [],
315 rew_ord = ("e_rew_ord",e_rew_ord),
319 (*asm_thm = [("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""),
320 ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""),
321 ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""),
322 ("d2_abcformula10",""),("d2_abcformula1_neg",""),("d2_abcformula2_neg",""),
323 ("d2_abcformula3_neg",""),("d2_abcformula4_neg",""),("d2_abcformula5_neg",""),
324 ("d2_abcformula6_neg","")],*)
326 Thm("d2_abcformula1",num_str d2_abcformula1), (*c+bx+cx^2=0 *)
327 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), (*c+bx+cx^2=0 *)
328 Thm("d2_abcformula2",num_str d2_abcformula2), (*c+ x+cx^2=0 *)
329 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), (*c+ x+cx^2=0 *)
330 Thm("d2_abcformula3",num_str d2_abcformula3), (*c+bx+ x^2=0 *)
331 Thm("d2_abcformula3_neg",num_str d2_abcformula3_neg), (*c+bx+ x^2=0 *)
332 Thm("d2_abcformula4",num_str d2_abcformula4), (*c+ x+ x^2=0 *)
333 Thm("d2_abcformula4_neg",num_str d2_abcformula4_neg), (*c+ x+ x^2=0 *)
334 Thm("d2_abcformula5",num_str d2_abcformula5), (*c+ cx^2=0 *)
335 Thm("d2_abcformula5_neg",num_str d2_abcformula5_neg), (*c+ cx^2=0 *)
336 Thm("d2_abcformula6",num_str d2_abcformula6), (*c+ x^2=0 *)
337 Thm("d2_abcformula6_neg",num_str d2_abcformula6_neg), (*c+ x^2=0 *)
338 Thm("d2_abcformula7",num_str d2_abcformula7), (* bx+ax^2=0 *)
339 Thm("d2_abcformula8",num_str d2_abcformula8), (* bx+ x^2=0 *)
340 Thm("d2_abcformula9",num_str d2_abcformula9), (* x+ax^2=0 *)
341 Thm("d2_abcformula10",num_str d2_abcformula10), (* x+ x^2=0 *)
342 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 *)
343 Thm("d2_sqrt_equation3",num_str d2_sqrt_equation3) (* bx^2=0 *)
345 scr = Script ((term_of o the o (parse thy)) "empty_script")
347 (*isolate the bound variable in an d2 equation; 'bdv' is a meta-constant*)
348 val d2_polyeq_simplify = prep_rls(
349 Rls {id = "d2_polyeq_simplify", preconds = [],
350 rew_ord = ("e_rew_ord",e_rew_ord),
354 (*asm_thm = [("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
355 ("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),("d2_pqformula3_neg",""),
356 ("d2_pqformula4_neg",""),
357 ("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula1_neg",""),
358 ("d2_abcformula2_neg",""), ("d2_sqrt_equation1",""),
359 ("d2_sqrt_equation1_neg",""),("d2_isolate_div","")],*)
361 Thm("d2_pqformula1",num_str d2_pqformula1), (* p+qx+ x^2=0 *)
362 Thm("d2_pqformula1_neg",num_str d2_pqformula1_neg), (* p+qx+ x^2=0 *)
363 Thm("d2_pqformula2",num_str d2_pqformula2), (* p+qx+1x^2=0 *)
364 Thm("d2_pqformula2_neg",num_str d2_pqformula2_neg), (* p+qx+1x^2=0 *)
365 Thm("d2_pqformula3",num_str d2_pqformula3), (* p+ x+ x^2=0 *)
366 Thm("d2_pqformula3_neg",num_str d2_pqformula3_neg), (* p+ x+ x^2=0 *)
367 Thm("d2_pqformula4",num_str d2_pqformula4), (* p+ x+1x^2=0 *)
368 Thm("d2_pqformula4_neg",num_str d2_pqformula4_neg), (* p+ x+1x^2=0 *)
369 Thm("d2_abcformula1",num_str d2_abcformula1), (* c+bx+cx^2=0 *)
370 Thm("d2_abcformula1_neg",num_str d2_abcformula1_neg), (* c+bx+cx^2=0 *)
371 Thm("d2_abcformula2",num_str d2_abcformula2), (* c+ x+cx^2=0 *)
372 Thm("d2_abcformula2_neg",num_str d2_abcformula2_neg), (* c+ x+cx^2=0 *)
373 Thm("d2_prescind1",num_str d2_prescind1), (* ax+bx^2=0 -> x(a+bx)=0 *)
374 Thm("d2_prescind2",num_str d2_prescind2), (* ax+ x^2=0 -> x(a+ x)=0 *)
375 Thm("d2_prescind3",num_str d2_prescind3), (* x+bx^2=0 -> x(1+bx)=0 *)
376 Thm("d2_prescind4",num_str d2_prescind4), (* x+ x^2=0 -> x(1+ x)=0 *)
377 Thm("d2_isolate_add1",num_str d2_isolate_add1), (* a+ bx^2=0 -> bx^2=(-1)a*)
378 Thm("d2_isolate_add2",num_str d2_isolate_add2), (* a+ x^2=0 -> x^2=(-1)a*)
379 Thm("d2_sqrt_equation1",num_str d2_sqrt_equation1), (* x^2=c -> x=+-sqrt(c)*)
380 Thm("d2_sqrt_equation1_neg",num_str d2_sqrt_equation1_neg),(* [c<0] x^2=c -> x=[]*)
381 Thm("d2_sqrt_equation2",num_str d2_sqrt_equation2), (* x^2=0 -> x=0 *)
382 Thm("d2_reduce_equation1",num_str d2_reduce_equation1),(* x(a+bx)=0 -> x=0 | a+bx=0*)
383 Thm("d2_reduce_equation2",num_str d2_reduce_equation2),(* x(a+ x)=0 -> x=0 | a+ x=0*)
384 Thm("d2_isolate_div",num_str d2_isolate_div) (* bx^2=c -> x^2=c/b*)
386 scr = Script ((term_of o the o (parse thy)) "empty_script")
389 (*isolate the bound variable in an d3 equation; 'bdv' is a meta-constant*)
390 val d3_polyeq_simplify = prep_rls(
391 Rls {id = "d3_polyeq_simplify", preconds = [],
392 rew_ord = ("e_rew_ord",e_rew_ord),
396 (*asm_thm = [("d3_isolate_div","")],*)
398 Thm("d3_reduce_equation1",num_str d3_reduce_equation1),
399 (*a*bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + b*bdv + c*bdv^^^2=0)*)
400 Thm("d3_reduce_equation2",num_str d3_reduce_equation2),
401 (* bdv + b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + b*bdv + c*bdv^^^2=0)*)
402 Thm("d3_reduce_equation3",num_str d3_reduce_equation3),
403 (*a*bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (a + bdv + c*bdv^^^2=0)*)
404 Thm("d3_reduce_equation4",num_str d3_reduce_equation4),
405 (* bdv + bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | (1 + bdv + c*bdv^^^2=0)*)
406 Thm("d3_reduce_equation5",num_str d3_reduce_equation5),
407 (*a*bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (a + b*bdv + bdv^^^2=0)*)
408 Thm("d3_reduce_equation6",num_str d3_reduce_equation6),
409 (* bdv + b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + b*bdv + bdv^^^2=0)*)
410 Thm("d3_reduce_equation7",num_str d3_reduce_equation7),
411 (*a*bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*)
412 Thm("d3_reduce_equation8",num_str d3_reduce_equation8),
413 (* bdv + bdv^^^2 + bdv^^^3=0) = (bdv=0 | (1 + bdv + bdv^^^2=0)*)
414 Thm("d3_reduce_equation9",num_str d3_reduce_equation9),
415 (*a*bdv + c*bdv^^^3=0) = (bdv=0 | (a + c*bdv^^^2=0)*)
416 Thm("d3_reduce_equation10",num_str d3_reduce_equation10),
417 (* bdv + c*bdv^^^3=0) = (bdv=0 | (1 + c*bdv^^^2=0)*)
418 Thm("d3_reduce_equation11",num_str d3_reduce_equation11),
419 (*a*bdv + bdv^^^3=0) = (bdv=0 | (a + bdv^^^2=0)*)
420 Thm("d3_reduce_equation12",num_str d3_reduce_equation12),
421 (* bdv + bdv^^^3=0) = (bdv=0 | (1 + bdv^^^2=0)*)
422 Thm("d3_reduce_equation13",num_str d3_reduce_equation13),
423 (* b*bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( b*bdv + c*bdv^^^2=0)*)
424 Thm("d3_reduce_equation14",num_str d3_reduce_equation14),
425 (* bdv^^^2 + c*bdv^^^3=0) = (bdv=0 | ( bdv + c*bdv^^^2=0)*)
426 Thm("d3_reduce_equation15",num_str d3_reduce_equation15),
427 (* b*bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( b*bdv + bdv^^^2=0)*)
428 Thm("d3_reduce_equation16",num_str d3_reduce_equation16),
429 (* bdv^^^2 + bdv^^^3=0) = (bdv=0 | ( bdv + bdv^^^2=0)*)
430 Thm("d3_isolate_add1",num_str d3_isolate_add1),
431 (*[|Not(bdv occurs_in a)|] ==> (a + b*bdv^^^3=0) = (bdv=0 | (b*bdv^^^3=a)*)
432 Thm("d3_isolate_add2",num_str d3_isolate_add2),
433 (*[|Not(bdv occurs_in a)|] ==> (a + bdv^^^3=0) = (bdv=0 | ( bdv^^^3=a)*)
434 Thm("d3_isolate_div",num_str d3_isolate_div),
435 (*[|Not(b=0)|] ==> (b*bdv^^^3=c) = (bdv^^^3=c/b*)
436 Thm("d3_root_equation2",num_str d3_root_equation2),
437 (*(bdv^^^3=0) = (bdv=0) *)
438 Thm("d3_root_equation1",num_str d3_root_equation1)
439 (*bdv^^^3=c) = (bdv = nroot 3 c*)
441 scr = Script ((term_of o the o (parse thy)) "empty_script")
444 (*isolate the bound variable in an d4 equation; 'bdv' is a meta-constant*)
445 val d4_polyeq_simplify = prep_rls(
446 Rls {id = "d4_polyeq_simplify", preconds = [],
447 rew_ord = ("e_rew_ord",e_rew_ord),
452 rules = [Thm("d4_sub_u1",num_str d4_sub_u1)
453 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *)
455 scr = Script ((term_of o the o (parse thy)) "empty_script")
458 ruleset' := overwritelthy thy (!ruleset',
459 [("d0_polyeq_simplify", d0_polyeq_simplify),
460 ("d1_polyeq_simplify", d1_polyeq_simplify),
461 ("d2_polyeq_simplify", d2_polyeq_simplify),
462 ("d2_polyeq_bdv_only_simplify", d2_polyeq_bdv_only_simplify),
463 ("d2_polyeq_sq_only_simplify", d2_polyeq_sq_only_simplify),
464 ("d2_polyeq_pqFormula_simplify", d2_polyeq_pqFormula_simplify),
465 ("d2_polyeq_abcFormula_simplify", d2_polyeq_abcFormula_simplify),
466 ("d3_polyeq_simplify", d3_polyeq_simplify),
467 ("d4_polyeq_simplify", d4_polyeq_simplify)
470 (*------------------------problems------------------------*)
472 (get_pbt ["degree_2","polynomial","univariate","equation"]);
476 (*-------------------------poly-----------------------*)
478 (prep_pbt PolyEq.thy "pbl_equ_univ_poly" [] e_pblID
479 (["polynomial","univariate","equation"],
480 [("#Given" ,["equality e_","solveFor v_"]),
481 ("#Where" ,["~((e_::bool) is_ratequation_in (v_::real))",
482 "~((lhs e_) is_rootTerm_in (v_::real))",
483 "~((rhs e_) is_rootTerm_in (v_::real))"]),
484 ("#Find" ,["solutions v_i_"])
486 PolyEq_prls, SOME "solve (e_::bool, v_)",
490 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg0" [] e_pblID
491 (["degree_0","polynomial","univariate","equation"],
492 [("#Given" ,["equality e_","solveFor v_"]),
493 ("#Where" ,["matches (?a = 0) e_",
494 "(lhs e_) is_poly_in v_",
495 "((lhs e_) has_degree_in v_ ) = 0"
497 ("#Find" ,["solutions v_i_"])
499 PolyEq_prls, SOME "solve (e_::bool, v_)",
500 [["PolyEq","solve_d0_polyeq_equation"]]));
504 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg1" [] e_pblID
505 (["degree_1","polynomial","univariate","equation"],
506 [("#Given" ,["equality e_","solveFor v_"]),
507 ("#Where" ,["matches (?a = 0) e_",
508 "(lhs e_) is_poly_in v_",
509 "((lhs e_) has_degree_in v_ ) = 1"
511 ("#Find" ,["solutions v_i_"])
513 PolyEq_prls, SOME "solve (e_::bool, v_)",
514 [["PolyEq","solve_d1_polyeq_equation"]]));
518 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2" [] e_pblID
519 (["degree_2","polynomial","univariate","equation"],
520 [("#Given" ,["equality e_","solveFor v_"]),
521 ("#Where" ,["matches (?a = 0) e_",
522 "(lhs e_) is_poly_in v_ ",
523 "((lhs e_) has_degree_in v_ ) = 2"]),
524 ("#Find" ,["solutions v_i_"])
526 PolyEq_prls, SOME "solve (e_::bool, v_)",
527 [["PolyEq","solve_d2_polyeq_equation"]]));
530 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_sqonly" [] e_pblID
531 (["sq_only","degree_2","polynomial","univariate","equation"],
532 [("#Given" ,["equality e_","solveFor v_"]),
533 ("#Where" ,["matches ( ?a + ?v_^^^2 = 0) e_ | \
534 \matches ( ?a + ?b*?v_^^^2 = 0) e_ | \
535 \matches ( ?v_^^^2 = 0) e_ | \
536 \matches ( ?b*?v_^^^2 = 0) e_" ,
537 "Not (matches (?a + ?v_ + ?v_^^^2 = 0) e_) &\
538 \Not (matches (?a + ?b*?v_ + ?v_^^^2 = 0) e_) &\
539 \Not (matches (?a + ?v_ + ?c*?v_^^^2 = 0) e_) &\
540 \Not (matches (?a + ?b*?v_ + ?c*?v_^^^2 = 0) e_) &\
541 \Not (matches ( ?v_ + ?v_^^^2 = 0) e_) &\
542 \Not (matches ( ?b*?v_ + ?v_^^^2 = 0) e_) &\
543 \Not (matches ( ?v_ + ?c*?v_^^^2 = 0) e_) &\
544 \Not (matches ( ?b*?v_ + ?c*?v_^^^2 = 0) e_)"]),
545 ("#Find" ,["solutions v_i_"])
547 PolyEq_prls, SOME "solve (e_::bool, v_)",
548 [["PolyEq","solve_d2_polyeq_sqonly_equation"]]));
551 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_bdvonly" [] e_pblID
552 (["bdv_only","degree_2","polynomial","univariate","equation"],
553 [("#Given" ,["equality e_","solveFor v_"]),
554 ("#Where" ,["matches (?a*?v_ + ?v_^^^2 = 0) e_ | \
555 \matches ( ?v_ + ?v_^^^2 = 0) e_ | \
556 \matches ( ?v_ + ?b*?v_^^^2 = 0) e_ | \
557 \matches (?a*?v_ + ?b*?v_^^^2 = 0) e_ | \
558 \matches ( ?v_^^^2 = 0) e_ | \
559 \matches ( ?b*?v_^^^2 = 0) e_ "]),
560 ("#Find" ,["solutions v_i_"])
562 PolyEq_prls, SOME "solve (e_::bool, v_)",
563 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]]));
566 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_pq" [] e_pblID
567 (["pqFormula","degree_2","polynomial","univariate","equation"],
568 [("#Given" ,["equality e_","solveFor v_"]),
569 ("#Where" ,["matches (?a + 1*?v_^^^2 = 0) e_ | \
570 \matches (?a + ?v_^^^2 = 0) e_"]),
571 ("#Find" ,["solutions v_i_"])
573 PolyEq_prls, SOME "solve (e_::bool, v_)",
574 [["PolyEq","solve_d2_polyeq_pq_equation"]]));
577 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg2_abc" [] e_pblID
578 (["abcFormula","degree_2","polynomial","univariate","equation"],
579 [("#Given" ,["equality e_","solveFor v_"]),
580 ("#Where" ,["matches (?a + ?v_^^^2 = 0) e_ | \
581 \matches (?a + ?b*?v_^^^2 = 0) e_"]),
582 ("#Find" ,["solutions v_i_"])
584 PolyEq_prls, SOME "solve (e_::bool, v_)",
585 [["PolyEq","solve_d2_polyeq_abc_equation"]]));
589 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg3" [] e_pblID
590 (["degree_3","polynomial","univariate","equation"],
591 [("#Given" ,["equality e_","solveFor v_"]),
592 ("#Where" ,["matches (?a = 0) e_",
593 "(lhs e_) is_poly_in v_ ",
594 "((lhs e_) has_degree_in v_) = 3"]),
595 ("#Find" ,["solutions v_i_"])
597 PolyEq_prls, SOME "solve (e_::bool, v_)",
598 [["PolyEq","solve_d3_polyeq_equation"]]));
602 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_deg4" [] e_pblID
603 (["degree_4","polynomial","univariate","equation"],
604 [("#Given" ,["equality e_","solveFor v_"]),
605 ("#Where" ,["matches (?a = 0) e_",
606 "(lhs e_) is_poly_in v_ ",
607 "((lhs e_) has_degree_in v_) = 4"]),
608 ("#Find" ,["solutions v_i_"])
610 PolyEq_prls, SOME "solve (e_::bool, v_)",
611 [(*["PolyEq","solve_d4_polyeq_equation"]*)]));
613 (*--- normalize ---*)
615 (prep_pbt PolyEq.thy "pbl_equ_univ_poly_norm" [] e_pblID
616 (["normalize","polynomial","univariate","equation"],
617 [("#Given" ,["equality e_","solveFor v_"]),
618 ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |\
619 \(Not(((lhs e_) is_poly_in v_)))"]),
620 ("#Find" ,["solutions v_i_"])
622 PolyEq_prls, SOME "solve (e_::bool, v_)",
623 [["PolyEq","normalize_poly"]]));
624 (*-------------------------expanded-----------------------*)
626 (prep_pbt PolyEq.thy "pbl_equ_univ_expand" [] e_pblID
627 (["expanded","univariate","equation"],
628 [("#Given" ,["equality e_","solveFor v_"]),
629 ("#Where" ,["matches (?a = 0) e_",
630 "(lhs e_) is_expanded_in v_ "]),
631 ("#Find" ,["solutions v_i_"])
633 PolyEq_prls, SOME "solve (e_::bool, v_)",
638 (prep_pbt PolyEq.thy "pbl_equ_univ_expand_deg2" [] e_pblID
639 (["degree_2","expanded","univariate","equation"],
640 [("#Given" ,["equality e_","solveFor v_"]),
641 ("#Where" ,["((lhs e_) has_degree_in v_) = 2"]),
642 ("#Find" ,["solutions v_i_"])
644 PolyEq_prls, SOME "solve (e_::bool, v_)",
645 [["PolyEq","complete_square"]]));
648 "-------------------------methods-----------------------";
650 (prep_met PolyEq.thy "met_polyeq" [] e_metID
653 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls,
654 crls=PolyEq_crls, nrls=norm_Rational
655 (*, asm_rls=[],asm_thm=[]*)}, "empty_script"));
658 (prep_met PolyEq.thy "met_polyeq_norm" [] e_metID
659 (["PolyEq","normalize_poly"],
660 [("#Given" ,["equality e_","solveFor v_"]),
661 ("#Where" ,["(Not((matches (?a = 0 ) e_ ))) |\
662 \(Not(((lhs e_) is_poly_in v_)))"]),
663 ("#Find" ,["solutions v_i_"])
665 {rew_ord'="termlessI",
670 crls=PolyEq_crls, nrls=norm_Rational(*,
673 (*RL: Ratpoly loest Brueche ohne bdv*)
674 "Script Normalize_poly (e_::bool) (v_::real) = \
675 \(let e_ =((Try (Rewrite all_left False)) @@ \
676 \ (Try (Repeat (Rewrite makex1_x False))) @@ \
677 \ (Try (Repeat (Rewrite_Set expand_binoms False))) @@ \
678 \ (Try (Repeat (Rewrite_Set_Inst [(bdv,v_::real)] \
679 \ make_ratpoly_in False))) @@ \
680 \ (Try (Repeat (Rewrite_Set polyeq_simplify False)))) e_ \
681 \ in (SubProblem (PolyEq_,[polynomial,univariate,equation], \
682 \ [no_met]) [bool_ e_, real_ v_]))"
686 (prep_met PolyEq.thy "met_polyeq_d0" [] e_metID
687 (["PolyEq","solve_d0_polyeq_equation"],
688 [("#Given" ,["equality e_","solveFor v_"]),
689 ("#Where" ,["(lhs e_) is_poly_in v_ ",
690 "((lhs e_) has_degree_in v_) = 0"]),
691 ("#Find" ,["solutions v_i_"])
693 {rew_ord'="termlessI",
697 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
698 crls=PolyEq_crls, nrls=norm_Rational(*,
701 "Script Solve_d0_polyeq_equation (e_::bool) (v_::real) = \
702 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
703 \ d0_polyeq_simplify False))) e_ \
704 \ in ((Or_to_List e_)::bool list))"
708 (prep_met PolyEq.thy "met_polyeq_d1" [] e_metID
709 (["PolyEq","solve_d1_polyeq_equation"],
710 [("#Given" ,["equality e_","solveFor v_"]),
711 ("#Where" ,["(lhs e_) is_poly_in v_ ",
712 "((lhs e_) has_degree_in v_) = 1"]),
713 ("#Find" ,["solutions v_i_"])
715 {rew_ord'="termlessI",
719 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
720 crls=PolyEq_crls, nrls=norm_Rational(*,
721 (* asm_rls=["d1_polyeq_simplify"],*)
723 asm_thm=[("d1_isolate_div","")]*)},
724 "Script Solve_d1_polyeq_equation (e_::bool) (v_::real) = \
725 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
726 \ d1_polyeq_simplify True)) @@ \
727 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
728 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\
729 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
730 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
734 (prep_met PolyEq.thy "met_polyeq_d22" [] e_metID
735 (["PolyEq","solve_d2_polyeq_equation"],
736 [("#Given" ,["equality e_","solveFor v_"]),
737 ("#Where" ,["(lhs e_) is_poly_in v_ ",
738 "((lhs e_) has_degree_in v_) = 2"]),
739 ("#Find" ,["solutions v_i_"])
741 {rew_ord'="termlessI",
745 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
746 crls=PolyEq_crls, nrls=norm_Rational(*,
747 (*asm_rls=["d2_polyeq_simplify","d1_polyeq_simplify"],*)
749 asm_thm = [("d1_isolate_div",""),("d2_pqformula1",""),("d2_pqformula2",""),
750 ("d2_pqformula3",""),("d2_pqformula4",""),("d2_pqformula1_neg",""),
751 ("d2_pqformula2_neg",""),("d2_pqformula3_neg",""),("d2_pqformula4_neg",""),
752 ("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula1_neg",""),
753 ("d2_abcformula2_neg",""), ("d2_sqrt_equation1",""),
754 ("d2_sqrt_equation1_neg",""), ("d2_isolate_div","")]*)},
755 "Script Solve_d2_polyeq_equation (e_::bool) (v_::real) = \
756 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
757 \ d2_polyeq_simplify True)) @@ \
758 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
759 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
760 \ d1_polyeq_simplify True)) @@ \
761 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
762 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\
763 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
764 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
768 (prep_met PolyEq.thy "met_polyeq_d2_bdvonly" [] e_metID
769 (["PolyEq","solve_d2_polyeq_bdvonly_equation"],
770 [("#Given" ,["equality e_","solveFor v_"]),
771 ("#Where" ,["(lhs e_) is_poly_in v_ ",
772 "((lhs e_) has_degree_in v_) = 2"]),
773 ("#Find" ,["solutions v_i_"])
775 {rew_ord'="termlessI",
779 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
780 crls=PolyEq_crls, nrls=norm_Rational(*,
781 (*asm_rls=["d2_polyeq_bdv_only_simplify","d1_polyeq_simplify "],*)
783 asm_thm=[("d1_isolate_div",""),("d2_isolate_div",""),
784 ("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg","")]*)},
785 "Script Solve_d2_polyeq_bdvonly_equation (e_::bool) (v_::real) =\
786 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
787 \ d2_polyeq_bdv_only_simplify True)) @@ \
788 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
789 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
790 \ d1_polyeq_simplify True)) @@ \
791 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
792 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\
793 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
794 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
798 (prep_met PolyEq.thy "met_polyeq_d2_sqonly" [] e_metID
799 (["PolyEq","solve_d2_polyeq_sqonly_equation"],
800 [("#Given" ,["equality e_","solveFor v_"]),
801 ("#Where" ,["(lhs e_) is_poly_in v_ ",
802 "((lhs e_) has_degree_in v_) = 2"]),
803 ("#Find" ,["solutions v_i_"])
805 {rew_ord'="termlessI",
809 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
810 crls=PolyEq_crls, nrls=norm_Rational(*,
811 (*asm_rls=["d2_polyeq_sq_only_simplify"],*)
813 asm_thm=[("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""),
814 ("d2_isolate_div","")]*)},
815 "Script Solve_d2_polyeq_sqonly_equation (e_::bool) (v_::real) =\
816 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
817 \ d2_polyeq_sq_only_simplify True)) @@ \
818 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
819 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_; \
820 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
821 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
825 (prep_met PolyEq.thy "met_polyeq_d2_pq" [] e_metID
826 (["PolyEq","solve_d2_polyeq_pq_equation"],
827 [("#Given" ,["equality e_","solveFor v_"]),
828 ("#Where" ,["(lhs e_) is_poly_in v_ ",
829 "((lhs e_) has_degree_in v_) = 2"]),
830 ("#Find" ,["solutions v_i_"])
832 {rew_ord'="termlessI",
836 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
837 crls=PolyEq_crls, nrls=norm_Rational(*,
838 (*asm_rls=["d2_polyeq_pqFormula_simplify"],*)
840 asm_thm=[("d2_pqformula1",""),("d2_pqformula2",""),("d2_pqformula3",""),
841 ("d2_pqformula4",""),("d2_pqformula5",""),("d2_pqformula6",""),
842 ("d2_pqformula7",""),("d2_pqformula8",""),("d2_pqformula9",""),
843 ("d2_pqformula10",""),("d2_pqformula1_neg",""),("d2_pqformula2_neg",""),
844 ("d2_pqformula3_neg",""), ("d2_pqformula4_neg",""),("d2_pqformula9_neg",""),
845 ("d2_pqformula10_neg","")]*)},
846 "Script Solve_d2_polyeq_pq_equation (e_::bool) (v_::real) = \
847 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
848 \ d2_polyeq_pqFormula_simplify True)) @@ \
849 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
850 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\
851 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
852 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
856 (prep_met PolyEq.thy "met_polyeq_d2_abc" [] e_metID
857 (["PolyEq","solve_d2_polyeq_abc_equation"],
858 [("#Given" ,["equality e_","solveFor v_"]),
859 ("#Where" ,["(lhs e_) is_poly_in v_ ",
860 "((lhs e_) has_degree_in v_) = 2"]),
861 ("#Find" ,["solutions v_i_"])
863 {rew_ord'="termlessI",
867 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
868 crls=PolyEq_crls, nrls=norm_Rational(*,
869 (*asm_rls=["d2_polyeq_abcFormula_simplify"],*)
871 asm_thm=[("d2_abcformula1",""),("d2_abcformula2",""),("d2_abcformula3",""),
872 ("d2_abcformula4",""),("d2_abcformula5",""),("d2_abcformula6",""),
873 ("d2_abcformula7",""),("d2_abcformula8",""),("d2_abcformula9",""),
874 ("d2_abcformula10",""),("d2_abcformula1_neg",""),("d2_abcformula2_neg",""),
875 ("d2_abcformula3_neg",""), ("d2_abcformula4_neg",""),("d2_abcformula5_neg",""),
876 ("d2_abcformula6_neg","")]*)},
877 "Script Solve_d2_polyeq_abc_equation (e_::bool) (v_::real) = \
878 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
879 \ d2_polyeq_abcFormula_simplify True)) @@ \
880 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
881 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\
882 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
883 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
887 (prep_met PolyEq.thy "met_polyeq_d3" [] e_metID
888 (["PolyEq","solve_d3_polyeq_equation"],
889 [("#Given" ,["equality e_","solveFor v_"]),
890 ("#Where" ,["(lhs e_) is_poly_in v_ ",
891 "((lhs e_) has_degree_in v_) = 3"]),
892 ("#Find" ,["solutions v_i_"])
894 {rew_ord'="termlessI",
898 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
899 crls=PolyEq_crls, nrls=norm_Rational(*,
900 (* asm_rls=["d1_polyeq_simplify","d2_polyeq_simplify","d1_polyeq_simplify"],*)
902 asm_thm=[("d3_isolate_div",""),("d1_isolate_div",""),("d2_pqformula1",""),
903 ("d2_pqformula2",""),("d2_pqformula3",""),("d2_pqformula4",""),
904 ("d2_pqformula1_neg",""), ("d2_pqformula2_neg",""),("d2_pqformula3_neg",""),
905 ("d2_pqformula4_neg",""), ("d2_abcformula1",""),("d2_abcformula2",""),
906 ("d2_abcformula1_neg",""),("d2_abcformula2_neg",""),
907 ("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), ("d2_isolate_div","")]*)},
908 "Script Solve_d3_polyeq_equation (e_::bool) (v_::real) = \
909 \ (let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_::real)] \
910 \ d3_polyeq_simplify True)) @@ \
911 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
912 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
913 \ d2_polyeq_simplify True)) @@ \
914 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
915 \ (Try (Rewrite_Set_Inst [(bdv,v_::real)] \
916 \ d1_polyeq_simplify True)) @@ \
917 \ (Try (Rewrite_Set polyeq_simplify False)) @@ \
918 \ (Try (Rewrite_Set norm_Rational_parenthesized False))) e_;\
919 \ (L_::bool list) = ((Or_to_List e_)::bool list) \
920 \ in Check_elementwise L_ {(v_::real). Assumptions} )"
923 (*.solves all expanded (ie. normalized) terms of degree 2.*)
924 (*Oct.02 restriction: 'eval_true 0 =< discriminant' ony for integer values
925 by 'PolyEq_erls'; restricted until Float.thy is implemented*)
927 (prep_met PolyEq.thy "met_polyeq_complsq" [] e_metID
928 (["PolyEq","complete_square"],
929 [("#Given" ,["equality e_","solveFor v_"]),
930 ("#Where" ,["matches (?a = 0) e_",
931 "((lhs e_) has_degree_in v_) = 2"]),
932 ("#Find" ,["solutions v_i_"])
934 {rew_ord'="termlessI",rls'=PolyEq_erls,srls=e_rls,prls=PolyEq_prls,
935 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))],
936 crls=PolyEq_crls, nrls=norm_Rational(*,
938 asm_thm=[("root_plus_minus","")]*)},
939 "Script Complete_square (e_::bool) (v_::real) = \
940 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\
941 \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \
942 \ @@ (Try (Rewrite square_explicit1 False)) \
943 \ @@ (Try (Rewrite square_explicit2 False)) \
944 \ @@ (Rewrite root_plus_minus True) \
945 \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False))) \
946 \ @@ (Try (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \
948 \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \
949 \ @@ (Try (Rewrite_Set calculate_RootRat False)) \
950 \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \
951 \ in ((Or_to_List e_)::bool list))"
953 (*6.10.02: x^2=64: root_plus_minus -/-/->
954 "Script Complete_square (e_::bool) (v_::real) = \
955 \(let e_ = ((Try (Rewrite_Set_Inst [(bdv,v_)] cancel_leading_coeff True))\
956 \ @@ (Try (Rewrite_Set_Inst [(bdv,v_)] complete_square True)) \
957 \ @@ (Try ((Rewrite square_explicit1 False) \
958 \ Or (Rewrite square_explicit2 False))) \
959 \ @@ (Rewrite root_plus_minus True) \
960 \ @@ ((Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit1 False)) \
961 \ Or (Repeat (Rewrite_Inst [(bdv,v_)] bdv_explicit2 False))) \
963 \ (Rewrite_Inst [(bdv,v_)] bdv_explicit3 False))) \
964 \ @@ (Try (Rewrite_Set calculate_RootRat False)) \
965 \ @@ (Try (Repeat (Calculate sqrt_)))) e_ \
966 \ in ((Or_to_List e_)::bool list))"*)
968 "******* PolyEq.ML end *******";
970 (*eine gehackte termorder*)
971 local (*. for make_polynomial_in .*)
973 open Term; (* for type order = EQUAL | LESS | GREATER *)
975 fun pr_ord EQUAL = "EQUAL"
976 | pr_ord LESS = "LESS"
977 | pr_ord GREATER = "GREATER";
979 fun dest_hd' x (Const (a, T)) = (((a, 0), T), 0)
980 | dest_hd' x (t as Free (a, T)) =
981 if x = t then ((("|||||||||||||", 0), T), 0) (*WN*)
982 else (((a, 0), T), 1)
983 | dest_hd' x (Var v) = (v, 2)
984 | dest_hd' x (Bound i) = ((("", i), dummyT), 3)
985 | dest_hd' x (Abs (_, T, _)) = ((("", 0), T), 4);
987 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) =
990 (if xstr = var then 1000*(the (int_of_str pot)) else 3)
991 | _ => raise error ("size_of_term' called with subst = "^
993 | size_of_term' x (Free (subst,_)) =
995 (Free (xstr,_)) => (if xstr = subst then 1000 else 1)
996 | _ => raise error ("size_of_term' called with subst = "^
998 | size_of_term' x (Abs (_,_,body)) = 1 + size_of_term' x body
999 | size_of_term' x (f$t) = size_of_term' x f + size_of_term' x t
1000 | size_of_term' x _ = 1;
1003 fun term_ord' x pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
1004 (case term_ord' x pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
1005 | term_ord' x pr thy (t, u) =
1008 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
1009 val _=writeln("t= f@ts= \""^
1010 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
1011 (commas(map(string_of_cterm o cterm_of(sign_of thy)) ts))^"]\"");
1012 val _=writeln("u= g@us= \""^
1013 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
1014 (commas(map(string_of_cterm o cterm_of(sign_of thy)) us))^"]\"");
1015 val _=writeln("size_of_term(t,u)= ("^
1016 (string_of_int(size_of_term' x t))^", "^
1017 (string_of_int(size_of_term' x u))^")");
1018 val _=writeln("hd_ord(f,g) = "^((pr_ord o (hd_ord x))(f,g)));
1019 val _=writeln("terms_ord(ts,us) = "^
1020 ((pr_ord o (terms_ord x) str false)(ts,us)));
1021 val _=writeln("-------");
1024 case int_ord (size_of_term' x t, size_of_term' x u) of
1026 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
1027 (case hd_ord x (f, g) of EQUAL => (terms_ord x str pr) (ts, us)
1031 and hd_ord x (f, g) = (* ~ term.ML *)
1032 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' x f,
1034 and terms_ord x str pr (ts, us) =
1035 list_ord (term_ord' x pr (assoc_thy "Isac.thy"))(ts, us);
1036 (*val x = (term_of o the o (parse thy)) "x"; (*FIXXXXXXME*)
1041 fun ord_make_polynomial_in (pr:bool) thy subst tu =
1043 (* val _=writeln("*** subs variable is: "^(subst2str subst)); *)
1046 (_,x)::_ => (term_ord' x pr thy tu = LESS)
1047 | _ => raise error ("ord_make_polynomial_in called with subst = "^
1052 val order_add_mult_in = prep_rls(
1053 Rls{id = "order_add_mult_in", preconds = [],
1054 rew_ord = ("ord_make_polynomial_in",
1055 ord_make_polynomial_in false Poly.thy),
1056 erls = e_rls,srls = Erls,
1059 rules = [Thm ("real_mult_commute",num_str real_mult_commute),
1061 Thm ("real_mult_left_commute",num_str real_mult_left_commute),
1062 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1063 Thm ("real_mult_assoc",num_str real_mult_assoc),
1064 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1065 Thm ("real_add_commute",num_str real_add_commute),
1067 Thm ("real_add_left_commute",num_str real_add_left_commute),
1068 (*x + (y + z) = y + (x + z)*)
1069 Thm ("real_add_assoc",num_str real_add_assoc)
1070 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1071 ], scr = EmptyScr}:rls);
1073 val collect_bdv = prep_rls(
1074 Rls{id = "collect_bdv", preconds = [],
1075 rew_ord = ("dummy_ord", dummy_ord),
1076 erls = e_rls,srls = Erls,
1079 rules = [Thm ("bdv_collect_1",num_str bdv_collect_1),
1080 Thm ("bdv_collect_2",num_str bdv_collect_2),
1081 Thm ("bdv_collect_3",num_str bdv_collect_3),
1083 Thm ("bdv_collect_assoc1_1",num_str bdv_collect_assoc1_1),
1084 Thm ("bdv_collect_assoc1_2",num_str bdv_collect_assoc1_2),
1085 Thm ("bdv_collect_assoc1_3",num_str bdv_collect_assoc1_3),
1087 Thm ("bdv_collect_assoc2_1",num_str bdv_collect_assoc2_1),
1088 Thm ("bdv_collect_assoc2_2",num_str bdv_collect_assoc2_2),
1089 Thm ("bdv_collect_assoc2_3",num_str bdv_collect_assoc2_3),
1092 Thm ("bdv_n_collect_1",num_str bdv_n_collect_1),
1093 Thm ("bdv_n_collect_2",num_str bdv_n_collect_2),
1094 Thm ("bdv_n_collect_3",num_str bdv_n_collect_3),
1096 Thm ("bdv_n_collect_assoc1_1",num_str bdv_n_collect_assoc1_1),
1097 Thm ("bdv_n_collect_assoc1_2",num_str bdv_n_collect_assoc1_2),
1098 Thm ("bdv_n_collect_assoc1_3",num_str bdv_n_collect_assoc1_3),
1100 Thm ("bdv_n_collect_assoc2_1",num_str bdv_n_collect_assoc2_1),
1101 Thm ("bdv_n_collect_assoc2_2",num_str bdv_n_collect_assoc2_2),
1102 Thm ("bdv_n_collect_assoc2_3",num_str bdv_n_collect_assoc2_3)
1103 ], scr = EmptyScr}:rls);
1105 (*.transforms an arbitrary term without roots to a polynomial [4]
1106 according to knowledge/Poly.sml.*)
1107 val make_polynomial_in = prep_rls(
1108 Seq {id = "make_polynomial_in", preconds = []:term list,
1109 rew_ord = ("dummy_ord", dummy_ord),
1110 erls = Atools_erls, srls = Erls,
1111 calc = [], (*asm_thm = [],*)
1112 rules = [Rls_ expand_poly,
1113 Rls_ order_add_mult_in,
1114 Rls_ simplify_power,
1115 Rls_ collect_numerals,
1117 Thm ("realpow_oneI",num_str realpow_oneI),
1118 Rls_ discard_parentheses,
1125 append_rls "separate_bdvs"
1127 [Thm ("separate_bdv", num_str separate_bdv),
1128 (*"?a * ?bdv / ?b = ?a / ?b * ?bdv"*)
1129 Thm ("separate_bdv_n", num_str separate_bdv_n),
1130 Thm ("separate_1_bdv", num_str separate_1_bdv),
1131 (*"?bdv / ?b = (1 / ?b) * ?bdv"*)
1132 Thm ("separate_1_bdv_n", num_str separate_1_bdv_n),
1133 (*"?bdv ^^^ ?n / ?b = 1 / ?b * ?bdv ^^^ ?n"*)
1134 Thm ("real_add_divide_distrib",
1135 num_str real_add_divide_distrib)
1136 (*"(?x + ?y) / ?z = ?x / ?z + ?y / ?z"
1137 WN051031 DOES NOT BELONG TO HERE*)
1139 val make_ratpoly_in = prep_rls(
1140 Seq {id = "make_ratpoly_in", preconds = []:term list,
1141 rew_ord = ("dummy_ord", dummy_ord),
1142 erls = Atools_erls, srls = Erls,
1143 calc = [], (*asm_thm = [],*)
1144 rules = [Rls_ norm_Rational,
1145 Rls_ order_add_mult_in,
1146 Rls_ discard_parentheses,
1148 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*)
1150 (*Calc ("HOL.divide" ,eval_cancel "#divide_") too weak!*)
1152 scr = EmptyScr}:rls);
1155 ruleset' := overwritelthy thy (!ruleset',
1156 [("order_add_mult_in", order_add_mult_in),
1157 ("collect_bdv", collect_bdv),
1158 ("make_polynomial_in", make_polynomial_in),
1159 ("make_ratpoly_in", make_ratpoly_in),
1160 ("separate_bdvs", separate_bdvs)