|
1 (*. (c) by Richard Lang, 2003 .*) |
|
2 (* collecting all knowledge for PolynomialEquations |
|
3 created by: rlang |
|
4 date: 02.07 |
|
5 changed by: rlang |
|
6 last change by: rlang |
|
7 date: 02.11.26 |
|
8 *) |
|
9 |
|
10 (* use"Knowledge/PolyEq.ML"; |
|
11 use"PolyEq.ML"; |
|
12 |
|
13 use"ROOT.ML"; |
|
14 cd"IsacKnowledge"; |
|
15 |
|
16 remove_thy"PolyEq"; |
|
17 use_thy"Knowledge/Isac"; |
|
18 *) |
|
19 "******* PolyEq.ML begin *******"; |
|
20 |
|
21 theory' := overwritel (!theory', [("PolyEq.thy",PolyEq.thy)]); |
|
22 (*-------------------------functions---------------------*) |
|
23 (* just for try |
|
24 local |
|
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 = |
|
27 if (v=v_) |
|
28 then poly2list_ t1 v (((str2term("1")))::(add0 l d (int_of_str' d_))) (int_of_str' d_) |
|
29 else t::(add0 l d 0) |
|
30 | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ |
|
31 (Const ("Atools.pow",_) $ v_ $ Free (d_,_))))) v l d = |
|
32 if (v=v_) |
|
33 then poly2list_ t1 v (((t11))::(add0 l d (int_of_str' d_))) (int_of_str' d_) |
|
34 else t::(add0 l d 0) |
|
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 |
|
38 else t::(add0 l d 0) |
|
39 | poly2list_ (t as (Const ("op +",_) $ t1 $ (Const ("op *",_) $ t11 $ (Free (v_,_)) ))) v l d = |
|
40 if (v= (str2term v_)) |
|
41 then poly2list_ t1 v ( (t11)::(add0 l d 1 )) 1 |
|
42 else t::(add0 l d 0) |
|
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); |
|
46 |
|
47 fun poly2list t v = poly2list_ t v [] 0; |
|
48 fun diffpolylist_ [] _ = [] |
|
49 | diffpolylist_ (x::xs) d = (str2term (if term2str(x)="0" |
|
50 then "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"));*) |
|
55 in |
|
56 |
|
57 end; |
|
58 *) |
|
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) |
|
81 ]; |
|
82 |
|
83 val PolyEq_erls = |
|
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) |
|
92 ]); |
|
93 |
|
94 val PolyEq_crls = |
|
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) |
|
103 ]); |
|
104 (*------ |
|
105 val PolyEq_erls = |
|
106 merge_rls "PolyEq_erls" |
|
107 (append_rls "" (Rls {(*asm_thm=[],*)calc=[], |
|
108 erls= Rls {(*asm_thm=[],*)calc=[], |
|
109 erls= Erls, |
|
110 id="e_rls",preconds=[], |
|
111 rew_ord=("dummy_ord",dummy_ord), |
|
112 rules=[Thm ("", |
|
113 num_str ), |
|
114 Thm ("", |
|
115 num_str ), |
|
116 Thm ("", |
|
117 num_str ) |
|
118 ], |
|
119 scr=EmptyScr,srls=Erls}, |
|
120 id="e_rls",preconds=[],rew_ord=("dummy_ord", |
|
121 dummy_ord), |
|
122 rules=[],scr=EmptyScr,srls=Erls} |
|
123 ) |
|
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) |
|
132 ]); |
|
133 -----*) |
|
134 |
|
135 |
|
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) |
|
153 ], |
|
154 scr = Script ((term_of o the o (parse thy)) |
|
155 "empty_script") |
|
156 }:rls); |
|
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) |
|
166 ], |
|
167 scr = Script ((term_of o the o (parse thy)) |
|
168 "empty_script") |
|
169 }:rls); |
|
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'*) |
|
174 ]); |
|
175 val polyeq_simplify = prep_rls( |
|
176 Rls {id = "polyeq_simplify", preconds = [], |
|
177 rew_ord = ("termlessI",termlessI), |
|
178 erls = PolyEq_erls, |
|
179 srls = Erls, |
|
180 calc = [], |
|
181 (*asm_thm = [],*) |
|
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_"), |
|
193 Rls_ reduce_012 |
|
194 ], |
|
195 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
196 }:rls); |
|
197 ruleset' := overwritelthy thy (!ruleset', |
|
198 [("polyeq_simplify",polyeq_simplify)]); |
|
199 |
|
200 |
|
201 (* ------------- polySolve ------------------ *) |
|
202 (* -- d0 -- *) |
|
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), |
|
207 erls = PolyEq_erls, |
|
208 srls = Erls, |
|
209 calc = [], |
|
210 (*asm_thm = [],*) |
|
211 rules = [Thm("d0_true",num_str d0_true), |
|
212 Thm("d0_false",num_str d0_false) |
|
213 ], |
|
214 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
215 }:rls); |
|
216 (* -- d1 -- *) |
|
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), |
|
221 erls = PolyEq_erls, |
|
222 srls = Erls, |
|
223 calc = [], |
|
224 (*asm_thm = [("d1_isolate_div","")],*) |
|
225 rules = [ |
|
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), |
|
229 (* a+ x=0 -> x=-a *) |
|
230 Thm("d1_isolate_div",num_str d1_isolate_div) |
|
231 (* bx=c -> x=c/b *) |
|
232 ], |
|
233 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
234 }:rls); |
|
235 (* -- d2 -- *) |
|
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), |
|
240 erls = PolyEq_erls, |
|
241 srls = Erls, |
|
242 calc = [], |
|
243 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), |
|
244 ("d2_isolate_div","")],*) |
|
245 rules = [ |
|
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*) |
|
256 ], |
|
257 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
258 }:rls); |
|
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), |
|
263 erls = PolyEq_erls, |
|
264 srls = Erls, |
|
265 calc = [], |
|
266 (*asm_thm = [("d2_sqrt_equation1",""),("d2_sqrt_equation1_neg",""), |
|
267 ("d2_isolate_div","")],*) |
|
268 rules = [ |
|
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*) |
|
275 ], |
|
276 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
277 }:rls); |
|
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), |
|
282 erls = PolyEq_erls, |
|
283 srls = Erls, |
|
284 calc = [], |
|
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","")],*) |
|
290 rules = [ |
|
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 *) |
|
309 ], |
|
310 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
311 }:rls); |
|
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), |
|
316 erls = PolyEq_erls, |
|
317 srls = Erls, |
|
318 calc = [], |
|
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","")],*) |
|
325 rules = [ |
|
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 *) |
|
344 ], |
|
345 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
346 }:rls); |
|
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), |
|
351 erls = PolyEq_erls, |
|
352 srls = Erls, |
|
353 calc = [], |
|
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","")],*) |
|
360 rules = [ |
|
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*) |
|
385 ], |
|
386 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
387 }:rls); |
|
388 (* -- d3 -- *) |
|
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), |
|
393 erls = PolyEq_erls, |
|
394 srls = Erls, |
|
395 calc = [], |
|
396 (*asm_thm = [("d3_isolate_div","")],*) |
|
397 rules = [ |
|
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*) |
|
440 ], |
|
441 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
442 }:rls); |
|
443 (* -- d4 -- *) |
|
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), |
|
448 erls = PolyEq_erls, |
|
449 srls = Erls, |
|
450 calc = [], |
|
451 (*asm_thm = [],*) |
|
452 rules = [Thm("d4_sub_u1",num_str d4_sub_u1) |
|
453 (* ax^4+bx^2+c=0 -> x=+-sqrt(ax^2+bx^+c) *) |
|
454 ], |
|
455 scr = Script ((term_of o the o (parse thy)) "empty_script") |
|
456 }:rls); |
|
457 |
|
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) |
|
468 ]); |
|
469 |
|
470 (*------------------------problems------------------------*) |
|
471 (* |
|
472 (get_pbt ["degree_2","polynomial","univariate","equation"]); |
|
473 show_ptyps(); |
|
474 *) |
|
475 |
|
476 (*-------------------------poly-----------------------*) |
|
477 store_pbt |
|
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_"]) |
|
485 ], |
|
486 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
487 [])); |
|
488 (*--- d0 ---*) |
|
489 store_pbt |
|
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" |
|
496 ]), |
|
497 ("#Find" ,["solutions v_i_"]) |
|
498 ], |
|
499 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
500 [["PolyEq","solve_d0_polyeq_equation"]])); |
|
501 |
|
502 (*--- d1 ---*) |
|
503 store_pbt |
|
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" |
|
510 ]), |
|
511 ("#Find" ,["solutions v_i_"]) |
|
512 ], |
|
513 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
514 [["PolyEq","solve_d1_polyeq_equation"]])); |
|
515 |
|
516 (*--- d2 ---*) |
|
517 store_pbt |
|
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_"]) |
|
525 ], |
|
526 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
527 [["PolyEq","solve_d2_polyeq_equation"]])); |
|
528 |
|
529 store_pbt |
|
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_"]) |
|
546 ], |
|
547 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
548 [["PolyEq","solve_d2_polyeq_sqonly_equation"]])); |
|
549 |
|
550 store_pbt |
|
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_"]) |
|
561 ], |
|
562 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
563 [["PolyEq","solve_d2_polyeq_bdvonly_equation"]])); |
|
564 |
|
565 store_pbt |
|
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_"]) |
|
572 ], |
|
573 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
574 [["PolyEq","solve_d2_polyeq_pq_equation"]])); |
|
575 |
|
576 store_pbt |
|
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_"]) |
|
583 ], |
|
584 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
585 [["PolyEq","solve_d2_polyeq_abc_equation"]])); |
|
586 |
|
587 (*--- d3 ---*) |
|
588 store_pbt |
|
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_"]) |
|
596 ], |
|
597 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
598 [["PolyEq","solve_d3_polyeq_equation"]])); |
|
599 |
|
600 (*--- d4 ---*) |
|
601 store_pbt |
|
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_"]) |
|
609 ], |
|
610 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
611 [(*["PolyEq","solve_d4_polyeq_equation"]*)])); |
|
612 |
|
613 (*--- normalize ---*) |
|
614 store_pbt |
|
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_"]) |
|
621 ], |
|
622 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
623 [["PolyEq","normalize_poly"]])); |
|
624 (*-------------------------expanded-----------------------*) |
|
625 store_pbt |
|
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_"]) |
|
632 ], |
|
633 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
634 [])); |
|
635 |
|
636 (*--- d2 ---*) |
|
637 store_pbt |
|
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_"]) |
|
643 ], |
|
644 PolyEq_prls, SOME "solve (e_::bool, v_)", |
|
645 [["PolyEq","complete_square"]])); |
|
646 |
|
647 |
|
648 "-------------------------methods-----------------------"; |
|
649 store_met |
|
650 (prep_met PolyEq.thy "met_polyeq" [] e_metID |
|
651 (["PolyEq"], |
|
652 [], |
|
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")); |
|
656 |
|
657 store_met |
|
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_"]) |
|
664 ], |
|
665 {rew_ord'="termlessI", |
|
666 rls'=PolyEq_erls, |
|
667 srls=e_rls, |
|
668 prls=PolyEq_prls, |
|
669 calc=[], |
|
670 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
671 asm_rls=[], |
|
672 asm_thm=[]*)}, |
|
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_]))" |
|
683 )); |
|
684 |
|
685 store_met |
|
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_"]) |
|
692 ], |
|
693 {rew_ord'="termlessI", |
|
694 rls'=PolyEq_erls, |
|
695 srls=e_rls, |
|
696 prls=PolyEq_prls, |
|
697 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
|
698 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
699 asm_rls=[], |
|
700 asm_thm=[]*)}, |
|
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))" |
|
705 )); |
|
706 |
|
707 store_met |
|
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_"]) |
|
714 ], |
|
715 {rew_ord'="termlessI", |
|
716 rls'=PolyEq_erls, |
|
717 srls=e_rls, |
|
718 prls=PolyEq_prls, |
|
719 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
|
720 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
721 (* asm_rls=["d1_polyeq_simplify"],*) |
|
722 asm_rls=[], |
|
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} )" |
|
731 )); |
|
732 |
|
733 store_met |
|
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_"]) |
|
740 ], |
|
741 {rew_ord'="termlessI", |
|
742 rls'=PolyEq_erls, |
|
743 srls=e_rls, |
|
744 prls=PolyEq_prls, |
|
745 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
|
746 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
747 (*asm_rls=["d2_polyeq_simplify","d1_polyeq_simplify"],*) |
|
748 asm_rls=[], |
|
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} )" |
|
765 )); |
|
766 |
|
767 store_met |
|
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_"]) |
|
774 ], |
|
775 {rew_ord'="termlessI", |
|
776 rls'=PolyEq_erls, |
|
777 srls=e_rls, |
|
778 prls=PolyEq_prls, |
|
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 "],*) |
|
782 asm_rls=[], |
|
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} )" |
|
795 )); |
|
796 |
|
797 store_met |
|
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_"]) |
|
804 ], |
|
805 {rew_ord'="termlessI", |
|
806 rls'=PolyEq_erls, |
|
807 srls=e_rls, |
|
808 prls=PolyEq_prls, |
|
809 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
|
810 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
811 (*asm_rls=["d2_polyeq_sq_only_simplify"],*) |
|
812 asm_rls=[], |
|
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} )" |
|
822 )); |
|
823 |
|
824 store_met |
|
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_"]) |
|
831 ], |
|
832 {rew_ord'="termlessI", |
|
833 rls'=PolyEq_erls, |
|
834 srls=e_rls, |
|
835 prls=PolyEq_prls, |
|
836 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
|
837 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
838 (*asm_rls=["d2_polyeq_pqFormula_simplify"],*) |
|
839 asm_rls=[], |
|
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} )" |
|
853 )); |
|
854 |
|
855 store_met |
|
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_"]) |
|
862 ], |
|
863 {rew_ord'="termlessI", |
|
864 rls'=PolyEq_erls, |
|
865 srls=e_rls, |
|
866 prls=PolyEq_prls, |
|
867 calc=[("sqrt", ("Root.sqrt", eval_sqrt "#sqrt_"))], |
|
868 crls=PolyEq_crls, nrls=norm_Rational(*, |
|
869 (*asm_rls=["d2_polyeq_abcFormula_simplify"],*) |
|
870 asm_rls=[], |
|
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} )" |
|
884 )); |
|
885 |
|
886 store_met |
|
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_"]) |
|
893 ], |
|
894 {rew_ord'="termlessI", |
|
895 rls'=PolyEq_erls, |
|
896 srls=e_rls, |
|
897 prls=PolyEq_prls, |
|
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"],*) |
|
901 asm_rls=[], |
|
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} )" |
|
921 )); |
|
922 |
|
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*) |
|
926 store_met |
|
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_"]) |
|
933 ], |
|
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(*, |
|
937 asm_rls=[], |
|
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))) \ |
|
947 \ @@ (Try (Repeat \ |
|
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))" |
|
952 )); |
|
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))) \ |
|
962 \ @@ (Try (Repeat \ |
|
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))"*) |
|
967 |
|
968 "******* PolyEq.ML end *******"; |
|
969 |
|
970 (*eine gehackte termorder*) |
|
971 local (*. for make_polynomial_in .*) |
|
972 |
|
973 open Term; (* for type order = EQUAL | LESS | GREATER *) |
|
974 |
|
975 fun pr_ord EQUAL = "EQUAL" |
|
976 | pr_ord LESS = "LESS" |
|
977 | pr_ord GREATER = "GREATER"; |
|
978 |
|
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); |
|
986 |
|
987 fun size_of_term' x (Const ("Atools.pow",_) $ Free (var,_) $ Free (pot,_)) = |
|
988 (case x of (*WN*) |
|
989 (Free (xstr,_)) => |
|
990 (if xstr = var then 1000*(the (int_of_str pot)) else 3) |
|
991 | _ => raise error ("size_of_term' called with subst = "^ |
|
992 (term2str x))) |
|
993 | size_of_term' x (Free (subst,_)) = |
|
994 (case x of |
|
995 (Free (xstr,_)) => (if xstr = subst then 1000 else 1) |
|
996 | _ => raise error ("size_of_term' called with subst = "^ |
|
997 (term2str x))) |
|
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; |
|
1001 |
|
1002 |
|
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) = |
|
1006 (if pr then |
|
1007 let |
|
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("-------"); |
|
1022 in () end |
|
1023 else (); |
|
1024 case int_ord (size_of_term' x t, size_of_term' x u) of |
|
1025 EQUAL => |
|
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) |
|
1028 | ord => ord) |
|
1029 end |
|
1030 | ord => ord) |
|
1031 and hd_ord x (f, g) = (* ~ term.ML *) |
|
1032 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' x f, |
|
1033 dest_hd' x g) |
|
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*) |
|
1037 *) |
|
1038 |
|
1039 in |
|
1040 |
|
1041 fun ord_make_polynomial_in (pr:bool) thy subst tu = |
|
1042 let |
|
1043 (* val _=writeln("*** subs variable is: "^(subst2str subst)); *) |
|
1044 in |
|
1045 case subst of |
|
1046 (_,x)::_ => (term_ord' x pr thy tu = LESS) |
|
1047 | _ => raise error ("ord_make_polynomial_in called with subst = "^ |
|
1048 (subst2str subst)) |
|
1049 end; |
|
1050 end; |
|
1051 |
|
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, |
|
1057 calc = [], |
|
1058 (*asm_thm = [],*) |
|
1059 rules = [Thm ("real_mult_commute",num_str real_mult_commute), |
|
1060 (* z * w = w * z *) |
|
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), |
|
1066 (*z + w = w + z*) |
|
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); |
|
1072 |
|
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, |
|
1077 calc = [], |
|
1078 (*asm_thm = [],*) |
|
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), |
|
1082 |
|
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), |
|
1086 |
|
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), |
|
1090 |
|
1091 |
|
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), |
|
1095 |
|
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), |
|
1099 |
|
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); |
|
1104 |
|
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, |
|
1116 Rls_ reduce_012, |
|
1117 Thm ("realpow_oneI",num_str realpow_oneI), |
|
1118 Rls_ discard_parentheses, |
|
1119 Rls_ collect_bdv |
|
1120 ], |
|
1121 scr = EmptyScr |
|
1122 }:rls); |
|
1123 |
|
1124 val separate_bdvs = |
|
1125 append_rls "separate_bdvs" |
|
1126 collect_bdv |
|
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*) |
|
1138 ]; |
|
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, |
|
1147 Rls_ separate_bdvs, |
|
1148 (* Rls_ rearrange_assoc, WN060916 why does cancel_p not work?*) |
|
1149 Rls_ cancel_p |
|
1150 (*Calc ("HOL.divide" ,eval_cancel "#divide_") too weak!*) |
|
1151 ], |
|
1152 scr = EmptyScr}:rls); |
|
1153 |
|
1154 |
|
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) |
|
1161 ]); |
|
1162 |