|
1 (*.eval_funs, rulesets, problems and methods concerning polynamials |
|
2 authors: Matthias Goldgruber 2003 |
|
3 (c) due to copyright terms |
|
4 |
|
5 use"../Knowledge/Poly.ML"; |
|
6 use"Knowledge/Poly.ML"; |
|
7 use"Poly.ML"; |
|
8 |
|
9 remove_thy"Poly"; |
|
10 use_thy"Knowledge/Isac"; |
|
11 ****************************************************************.*) |
|
12 |
|
13 (*.**************************************************************** |
|
14 remark on 'polynomials' |
|
15 WN020919 |
|
16 there are 5 kinds of expanded normalforms: |
|
17 [1] 'complete polynomial' (Komplettes Polynom), univariate |
|
18 a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0) |
|
19 not (a_n = 0), some a_i may be zero (DON'T disappear), |
|
20 variables in monomials lexicographically ordered and complete, |
|
21 x written as 1*x^1, ... |
|
22 [2] 'polynomial' (Polynom), univariate and multivariate |
|
23 a_0 + a_1.x +...+ a_n.x^n not (a_n = 0) |
|
24 a_0 + a_1.x_1.x_2^n_12...x_m^n_1m +...+ a_n.x_1^n.x_2^n_n2...x_m^n_nm |
|
25 not (a_n = 0), some a_i may be zero (ie. monomials disappear), |
|
26 exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown, |
|
27 and variables in monomials are lexicographically ordered |
|
28 examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2" |
|
29 [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2" |
|
30 [2]: "x + (-50) * x ^^^ 3" |
|
31 [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3" |
|
32 |
|
33 [3] 'expanded_term' (Ausmultiplizierter Term): |
|
34 pull out unary minus to binary minus, |
|
35 as frequently exercised in schools; other conditions for [2] hold however |
|
36 examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2" |
|
37 "4 * x ^^^ 2 - 9 * y ^^^ 2" |
|
38 [4] 'polynomial_in' (Polynom in): |
|
39 polynomial in 1 variable with arbitrary coefficients |
|
40 examples: "2 * x + (-50) * x ^^^ 3" (poly in x) |
|
41 "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a) |
|
42 [5] 'expanded_in' (Ausmultiplizierter Termin in): |
|
43 analoguous to [3] with binary minus like [3] |
|
44 examples: "2 * x - 50 * x ^^^ 3" (expanded in x) |
|
45 "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a) |
|
46 *****************************************************************.*) |
|
47 |
|
48 "******** Poly.ML begin ******************************************"; |
|
49 theory' := overwritel (!theory', [("Poly.thy",Poly.thy)]); |
|
50 |
|
51 |
|
52 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*) |
|
53 fun is_polyrat_in t v = |
|
54 let |
|
55 fun coeff_in c v = member op = (vars c) v; |
|
56 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:") |
|
57 (* at the moment there is no term like this, but ....*) |
|
58 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v = not(coeff_in b v) |
|
59 | finddivide (_ $ t1 $ t2) v = (finddivide t1 v) orelse (finddivide t2 v) |
|
60 | finddivide (_ $ t1) v = (finddivide t1 v) |
|
61 | finddivide _ _ = false; |
|
62 in |
|
63 finddivide t v |
|
64 end; |
|
65 |
|
66 fun eval_is_polyrat_in _ _ (p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ = |
|
67 if is_polyrat_in t v then |
|
68 SOME ((term2str p) ^ " = True", |
|
69 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
70 else SOME ((term2str p) ^ " = True", |
|
71 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
72 | eval_is_polyrat_in _ _ _ _ = ((*writeln"### nichts matcht";*) NONE); |
|
73 |
|
74 |
|
75 local |
|
76 (*.a 'c is coefficient of v' if v does NOT occur in c.*) |
|
77 fun coeff_in c v = not (member op = (vars c) v); |
|
78 (* |
|
79 val v = (term_of o the o (parse thy)) "x"; |
|
80 val t = (term_of o the o (parse thy)) "1"; |
|
81 coeff_in t v; |
|
82 (*val it = true : bool*) |
|
83 val t = (term_of o the o (parse thy)) "a*b+c"; |
|
84 coeff_in t v; |
|
85 (*val it = true : bool*) |
|
86 val t = (term_of o the o (parse thy)) "a*x+c"; |
|
87 coeff_in t v; |
|
88 (*val it = false : bool*) |
|
89 *) |
|
90 (*. a 'monomial t in variable v' is a term t with |
|
91 either (1) v NOT existent in t, or (2) v contained in t, |
|
92 if (1) then degree 0 |
|
93 if (2) then v is a factor on the very right, ev. with exponent.*) |
|
94 fun factor_right_deg (*case 2*) |
|
95 (t as Const ("op *",_) $ t1 $ |
|
96 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v = |
|
97 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE |
|
98 | factor_right_deg |
|
99 (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v = |
|
100 if (vv = v) then SOME (int_of_str' d) else NONE |
|
101 | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v = |
|
102 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE |
|
103 | factor_right_deg vv v = |
|
104 if (vv = v) then SOME 1 else NONE; |
|
105 fun mono_deg_in m v = |
|
106 if coeff_in m v then (*case 1*) SOME 0 |
|
107 else factor_right_deg m v; |
|
108 (* |
|
109 val v = (term_of o the o (parse thy)) "x"; |
|
110 val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7"; |
|
111 mono_deg_in t v; |
|
112 (*val it = SOME 7*) |
|
113 val t = (term_of o the o (parse thy)) "x^^^7"; |
|
114 mono_deg_in t v; |
|
115 (*val it = SOME 7*) |
|
116 val t = (term_of o the o (parse thy)) "(a*b+c)*x"; |
|
117 mono_deg_in t v; |
|
118 (*val it = SOME 1*) |
|
119 val t = (term_of o the o (parse thy)) "(a*b+x)*x"; |
|
120 mono_deg_in t v; |
|
121 (*val it = NONE*) |
|
122 val t = (term_of o the o (parse thy)) "x"; |
|
123 mono_deg_in t v; |
|
124 (*val it = SOME 1*) |
|
125 val t = (term_of o the o (parse thy)) "(a*b+c)"; |
|
126 mono_deg_in t v; |
|
127 (*val it = SOME 0*) |
|
128 val t = (term_of o the o (parse thy)) "ab - (a*b)*x"; |
|
129 mono_deg_in t v; |
|
130 (*val it = NONE*) |
|
131 *) |
|
132 fun expand_deg_in t v = |
|
133 let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) = |
|
134 (case mono_deg_in t2 v of (* $ is left associative*) |
|
135 SOME d' => edi d' d' t1 |
|
136 | NONE => NONE) |
|
137 | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) = |
|
138 (case mono_deg_in t2 v of |
|
139 SOME d' => edi d' d' t1 |
|
140 | NONE => NONE) |
|
141 | edi d dmax (Const ("op -",_) $ t1 $ t2) = |
|
142 (case mono_deg_in t2 v of |
|
143 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
|
144 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else NONE |
|
145 | NONE => NONE) |
|
146 | edi d dmax (Const ("op +",_) $ t1 $ t2) = |
|
147 (case mono_deg_in t2 v of |
|
148 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
|
149 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else NONE |
|
150 | NONE => NONE) |
|
151 | edi ~1 ~1 t = |
|
152 (case mono_deg_in t v of |
|
153 d as SOME _ => d |
|
154 | NONE => NONE) |
|
155 | edi d dmax t = (*basecase last*) |
|
156 (case mono_deg_in t v of |
|
157 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then SOME dmax else NONE |
|
158 | NONE => NONE) |
|
159 in edi ~1 ~1 t end; |
|
160 (* |
|
161 val v = (term_of o the o (parse thy)) "x"; |
|
162 val t = (term_of o the o (parse thy)) "a+b"; |
|
163 expand_deg_in t v; |
|
164 (*val it = SOME 0*) |
|
165 val t = (term_of o the o (parse thy)) "(a+b)*x"; |
|
166 expand_deg_in t v; |
|
167 (*SOME 1*) |
|
168 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x"; |
|
169 expand_deg_in t v; |
|
170 (*SOME 1*) |
|
171 val t = (term_of o the o (parse thy)) "a*b + (a-b)*x"; |
|
172 expand_deg_in t v; |
|
173 (*SOME 1*) |
|
174 val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2"; |
|
175 expand_deg_in t v; |
|
176 *) |
|
177 fun poly_deg_in t v = |
|
178 let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) = |
|
179 (case mono_deg_in t2 v of (* $ is left associative*) |
|
180 SOME d' => edi d' d' t1 |
|
181 | NONE => NONE) |
|
182 | edi d dmax (Const ("op +",_) $ t1 $ t2) = |
|
183 (case mono_deg_in t2 v of |
|
184 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*) |
|
185 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then edi d' dmax t1 else NONE |
|
186 | NONE => NONE) |
|
187 | edi ~1 ~1 t = |
|
188 (case mono_deg_in t v of |
|
189 d as SOME _ => d |
|
190 | NONE => NONE) |
|
191 | edi d dmax t = (*basecase last*) |
|
192 (case mono_deg_in t v of |
|
193 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0))) then SOME dmax else NONE |
|
194 | NONE => NONE) |
|
195 in edi ~1 ~1 t end; |
|
196 in |
|
197 |
|
198 fun is_expanded_in t v = |
|
199 case expand_deg_in t v of SOME _ => true | NONE => false; |
|
200 fun is_poly_in t v = |
|
201 case poly_deg_in t v of SOME _ => true | NONE => false; |
|
202 fun has_degree_in t v = |
|
203 case expand_deg_in t v of SOME d => d | NONE => ~1; |
|
204 end; |
|
205 (* |
|
206 val v = (term_of o the o (parse thy)) "x"; |
|
207 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2"; |
|
208 has_degree_in t v; |
|
209 (*val it = 2*) |
|
210 val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2"; |
|
211 has_degree_in t v; |
|
212 (*val it = 2*) |
|
213 val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2"; |
|
214 has_degree_in t v; |
|
215 (*val it = 2*) |
|
216 *) |
|
217 |
|
218 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*) |
|
219 fun eval_is_expanded_in _ _ |
|
220 (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ = |
|
221 if is_expanded_in t v |
|
222 then SOME ((term2str p) ^ " = True", |
|
223 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
224 else SOME ((term2str p) ^ " = True", |
|
225 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
226 | eval_is_expanded_in _ _ _ _ = NONE; |
|
227 (* |
|
228 val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x"; |
|
229 val SOME (id, t') = eval_is_expanded_in 0 0 t 0; |
|
230 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*) |
|
231 term2str t'; |
|
232 (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*) |
|
233 *) |
|
234 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*) |
|
235 fun eval_is_poly_in _ _ |
|
236 (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ = |
|
237 if is_poly_in t v |
|
238 then SOME ((term2str p) ^ " = True", |
|
239 Trueprop $ (mk_equality (p, HOLogic.true_const))) |
|
240 else SOME ((term2str p) ^ " = True", |
|
241 Trueprop $ (mk_equality (p, HOLogic.false_const))) |
|
242 | eval_is_poly_in _ _ _ _ = NONE; |
|
243 (* |
|
244 val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x"; |
|
245 val SOME (id, t') = eval_is_poly_in 0 0 t 0; |
|
246 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*) |
|
247 term2str t'; |
|
248 (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*) |
|
249 *) |
|
250 |
|
251 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*) |
|
252 fun eval_has_degree_in _ _ |
|
253 (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ = |
|
254 let val d = has_degree_in t v |
|
255 val d' = term_of_num HOLogic.realT d |
|
256 in SOME ((term2str p) ^ " = " ^ (string_of_int d), |
|
257 Trueprop $ (mk_equality (p, d'))) |
|
258 end |
|
259 | eval_has_degree_in _ _ _ _ = NONE; |
|
260 (* |
|
261 > val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x"; |
|
262 > val SOME (id, t') = eval_has_degree_in 0 0 t 0; |
|
263 val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string |
|
264 > term2str t'; |
|
265 val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string |
|
266 *) |
|
267 |
|
268 (*..*) |
|
269 val calculate_Poly = |
|
270 append_rls "calculate_PolyFIXXXME.not.impl." e_rls |
|
271 []; |
|
272 |
|
273 (*.for evaluation of conditions in rewrite rules.*) |
|
274 val Poly_erls = |
|
275 append_rls "Poly_erls" Atools_erls |
|
276 [ Calc ("op =",eval_equal "#equal_"), |
|
277 Thm ("real_unari_minus",num_str real_unari_minus), |
|
278 Calc ("op +",eval_binop "#add_"), |
|
279 Calc ("op -",eval_binop "#sub_"), |
|
280 Calc ("op *",eval_binop "#mult_"), |
|
281 Calc ("Atools.pow" ,eval_binop "#power_") |
|
282 ]; |
|
283 |
|
284 val poly_crls = |
|
285 append_rls "poly_crls" Atools_crls |
|
286 [ Calc ("op =",eval_equal "#equal_"), |
|
287 Thm ("real_unari_minus",num_str real_unari_minus), |
|
288 Calc ("op +",eval_binop "#add_"), |
|
289 Calc ("op -",eval_binop "#sub_"), |
|
290 Calc ("op *",eval_binop "#mult_"), |
|
291 Calc ("Atools.pow" ,eval_binop "#power_") |
|
292 ]; |
|
293 |
|
294 |
|
295 local (*. for make_polynomial .*) |
|
296 |
|
297 open Term; (* for type order = EQUAL | LESS | GREATER *) |
|
298 |
|
299 fun pr_ord EQUAL = "EQUAL" |
|
300 | pr_ord LESS = "LESS" |
|
301 | pr_ord GREATER = "GREATER"; |
|
302 |
|
303 fun dest_hd' (Const (a, T)) = (* ~ term.ML *) |
|
304 (case a of |
|
305 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*) |
|
306 | _ => (((a, 0), T), 0)) |
|
307 | dest_hd' (Free (a, T)) = (((a, 0), T), 1) |
|
308 | dest_hd' (Var v) = (v, 2) |
|
309 | dest_hd' (Bound i) = ((("", i), dummyT), 3) |
|
310 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4); |
|
311 |
|
312 fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*) |
|
313 (case int_of_str (order) of |
|
314 SOME d => d |
|
315 | NONE => 0) |
|
316 | get_order_pow _ = 0; |
|
317 |
|
318 fun size_of_term' (Const(str,_) $ t) = |
|
319 if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*) |
|
320 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body |
|
321 | size_of_term' (f$t) = size_of_term' f + size_of_term' t |
|
322 | size_of_term' _ = 1; |
|
323 |
|
324 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *) |
|
325 (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord) |
|
326 | term_ord' pr thy (t, u) = |
|
327 (if pr then |
|
328 let |
|
329 val (f, ts) = strip_comb t and (g, us) = strip_comb u; |
|
330 val _=writeln("t= f@ts= \""^ |
|
331 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^ |
|
332 (commas(map(Syntax.string_of_term (thy2ctxt thy))ts))^"]\""); |
|
333 val _=writeln("u= g@us= \""^ |
|
334 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^ |
|
335 (commas(map(Syntax.string_of_term (thy2ctxt thy))us))^"]\""); |
|
336 val _=writeln("size_of_term(t,u)= ("^ |
|
337 (string_of_int(size_of_term' t))^", "^ |
|
338 (string_of_int(size_of_term' u))^")"); |
|
339 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g))); |
|
340 val _=writeln("terms_ord(ts,us) = "^ |
|
341 ((pr_ord o terms_ord str false)(ts,us))); |
|
342 val _=writeln("-------"); |
|
343 in () end |
|
344 else (); |
|
345 case int_ord (size_of_term' t, size_of_term' u) of |
|
346 EQUAL => |
|
347 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in |
|
348 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us) |
|
349 | ord => ord) |
|
350 end |
|
351 | ord => ord) |
|
352 and hd_ord (f, g) = (* ~ term.ML *) |
|
353 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g) |
|
354 and terms_ord str pr (ts, us) = |
|
355 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us); |
|
356 in |
|
357 |
|
358 fun ord_make_polynomial (pr:bool) thy (_:subst) tu = |
|
359 (term_ord' pr thy(***) tu = LESS ); |
|
360 |
|
361 end;(*local*) |
|
362 |
|
363 |
|
364 rew_ord' := overwritel (!rew_ord', |
|
365 [("termlessI", termlessI), |
|
366 ("ord_make_polynomial", ord_make_polynomial false thy) |
|
367 ]); |
|
368 |
|
369 |
|
370 val expand = |
|
371 Rls{id = "expand", preconds = [], |
|
372 rew_ord = ("dummy_ord", dummy_ord), |
|
373 erls = e_rls,srls = Erls, |
|
374 calc = [], |
|
375 (*asm_thm = [],*) |
|
376 rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
377 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
378 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2) |
|
379 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
380 ], scr = EmptyScr}:rls; |
|
381 |
|
382 (*----------------- Begin: rulesets for make_polynomial_ ----------------- |
|
383 'rlsIDs' redefined by MG as 'rlsIDs_' |
|
384 ^^^*) |
|
385 |
|
386 val discard_minus_ = |
|
387 Rls{id = "discard_minus_", preconds = [], |
|
388 rew_ord = ("dummy_ord", dummy_ord), |
|
389 erls = e_rls,srls = Erls, |
|
390 calc = [], |
|
391 (*asm_thm = [],*) |
|
392 rules = [Thm ("real_diff_minus",num_str real_diff_minus), |
|
393 (*"a - b = a + -1 * b"*) |
|
394 Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)) |
|
395 (*- ?z = "-1 * ?z"*) |
|
396 ], scr = EmptyScr}:rls; |
|
397 val expand_poly_ = |
|
398 Rls{id = "expand_poly_", preconds = [], |
|
399 rew_ord = ("dummy_ord", dummy_ord), |
|
400 erls = e_rls,srls = Erls, |
|
401 calc = [], |
|
402 (*asm_thm = [],*) |
|
403 rules = [Thm ("real_plus_binom_pow4",num_str real_plus_binom_pow4), |
|
404 (*"(a + b)^^^4 = ... "*) |
|
405 Thm ("real_plus_binom_pow5",num_str real_plus_binom_pow5), |
|
406 (*"(a + b)^^^5 = ... "*) |
|
407 Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3), |
|
408 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *) |
|
409 |
|
410 (*WN071229 changed/removed for Schaerding -----vvv*) |
|
411 (*Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2),*) |
|
412 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*) |
|
413 Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2), |
|
414 (*"(a + b)^^^2 = (a + b) * (a + b)"*) |
|
415 (*Thm ("real_plus_minus_binom1_p_p", |
|
416 num_str real_plus_minus_binom1_p_p),*) |
|
417 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*) |
|
418 (*Thm ("real_plus_minus_binom2_p_p", |
|
419 num_str real_plus_minus_binom2_p_p),*) |
|
420 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*) |
|
421 (*WN071229 changed/removed for Schaerding -----^^^*) |
|
422 |
|
423 Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
424 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
425 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
426 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
427 |
|
428 Thm ("realpow_multI", num_str realpow_multI), |
|
429 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
|
430 Thm ("realpow_pow",num_str realpow_pow) |
|
431 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
|
432 ], scr = EmptyScr}:rls; |
|
433 |
|
434 (*.the expression contains + - * ^ only ? |
|
435 this is weaker than 'is_polynomial' !.*) |
|
436 fun is_polyexp (Free _) = true |
|
437 | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true |
|
438 | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true |
|
439 | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true |
|
440 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true |
|
441 | is_polyexp (Const ("op +",_) $ t1 $ t2) = |
|
442 ((is_polyexp t1) andalso (is_polyexp t2)) |
|
443 | is_polyexp (Const ("op -",_) $ t1 $ t2) = |
|
444 ((is_polyexp t1) andalso (is_polyexp t2)) |
|
445 | is_polyexp (Const ("op *",_) $ t1 $ t2) = |
|
446 ((is_polyexp t1) andalso (is_polyexp t2)) |
|
447 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) = |
|
448 ((is_polyexp t1) andalso (is_polyexp t2)) |
|
449 | is_polyexp _ = false; |
|
450 |
|
451 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*) |
|
452 fun eval_is_polyexp (thmid:string) _ |
|
453 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy = |
|
454 if is_polyexp arg |
|
455 then SOME (mk_thmid thmid "" |
|
456 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
457 Trueprop $ (mk_equality (t, HOLogic.true_const))) |
|
458 else SOME (mk_thmid thmid "" |
|
459 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
460 Trueprop $ (mk_equality (t, HOLogic.false_const))) |
|
461 | eval_is_polyexp _ _ _ _ = NONE; |
|
462 |
|
463 val expand_poly_rat_ = |
|
464 Rls{id = "expand_poly_rat_", preconds = [], |
|
465 rew_ord = ("dummy_ord", dummy_ord), |
|
466 erls = append_rls "e_rls-is_polyexp" e_rls |
|
467 [Calc ("Poly.is'_polyexp", eval_is_polyexp "") |
|
468 ], |
|
469 srls = Erls, |
|
470 calc = [], |
|
471 (*asm_thm = [],*) |
|
472 rules = [Thm ("real_plus_binom_pow4_poly",num_str real_plus_binom_pow4_poly), |
|
473 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*) |
|
474 Thm ("real_plus_binom_pow5_poly",num_str real_plus_binom_pow5_poly), |
|
475 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*) |
|
476 Thm ("real_plus_binom_pow2_poly",num_str real_plus_binom_pow2_poly), |
|
477 (*"[| a is_polyexp; b is_polyexp |] ==> |
|
478 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*) |
|
479 Thm ("real_plus_binom_pow3_poly",num_str real_plus_binom_pow3_poly), |
|
480 (*"[| a is_polyexp; b is_polyexp |] ==> |
|
481 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *) |
|
482 Thm ("real_plus_minus_binom1_p_p",num_str real_plus_minus_binom1_p_p), |
|
483 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*) |
|
484 Thm ("real_plus_minus_binom2_p_p",num_str real_plus_minus_binom2_p_p), |
|
485 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*) |
|
486 |
|
487 Thm ("real_add_mult_distrib_poly" ,num_str real_add_mult_distrib_poly), |
|
488 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
489 Thm ("real_add_mult_distrib2_poly",num_str real_add_mult_distrib2_poly), |
|
490 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
491 |
|
492 Thm ("realpow_multI_poly", num_str realpow_multI_poly), |
|
493 (*"[| r is_polyexp; s is_polyexp |] ==> |
|
494 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
|
495 Thm ("realpow_pow",num_str realpow_pow) |
|
496 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
|
497 ], scr = EmptyScr}:rls; |
|
498 |
|
499 val simplify_power_ = |
|
500 Rls{id = "simplify_power_", preconds = [], |
|
501 rew_ord = ("dummy_ord", dummy_ord), |
|
502 erls = e_rls, srls = Erls, |
|
503 calc = [], |
|
504 (*asm_thm = [],*) |
|
505 rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
|
506 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *) |
|
507 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)), |
|
508 (*"r * r = r ^^^ 2"*) |
|
509 Thm ("realpow_twoI_assoc_l",num_str realpow_twoI_assoc_l), |
|
510 (*"r * (r * s) = r ^^^ 2 * s"*) |
|
511 |
|
512 Thm ("realpow_plus_1",num_str realpow_plus_1), |
|
513 (*"r * r ^^^ n = r ^^^ (n + 1)"*) |
|
514 Thm ("realpow_plus_1_assoc_l", num_str realpow_plus_1_assoc_l), |
|
515 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*) |
|
516 (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *) |
|
517 Thm ("realpow_plus_1_assoc_l2", num_str realpow_plus_1_assoc_l2), |
|
518 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*) |
|
519 |
|
520 Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)), |
|
521 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*) |
|
522 Thm ("realpow_addI_assoc_l", num_str realpow_addI_assoc_l), |
|
523 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*) |
|
524 |
|
525 (* ist in expand_poly - wird hier aber auch gebraucht, wegen: |
|
526 "r * r = r ^^^ 2" wenn r=a^^^b*) |
|
527 Thm ("realpow_pow",num_str realpow_pow) |
|
528 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
|
529 ], scr = EmptyScr}:rls; |
|
530 |
|
531 val calc_add_mult_pow_ = |
|
532 Rls{id = "calc_add_mult_pow_", preconds = [], |
|
533 rew_ord = ("dummy_ord", dummy_ord), |
|
534 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
|
535 calc = [("PLUS" , ("op +", eval_binop "#add_")), |
|
536 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
537 ("POWER", ("Atools.pow", eval_binop "#power_")) |
|
538 ], |
|
539 (*asm_thm = [],*) |
|
540 rules = [Calc ("op +", eval_binop "#add_"), |
|
541 Calc ("op *", eval_binop "#mult_"), |
|
542 Calc ("Atools.pow", eval_binop "#power_") |
|
543 ], scr = EmptyScr}:rls; |
|
544 |
|
545 val reduce_012_mult_ = |
|
546 Rls{id = "reduce_012_mult_", preconds = [], |
|
547 rew_ord = ("dummy_ord", dummy_ord), |
|
548 erls = e_rls,srls = Erls, |
|
549 calc = [], |
|
550 (*asm_thm = [],*) |
|
551 rules = [(* MG: folgende Thm müssen hier stehen bleiben: *) |
|
552 Thm ("real_mult_1_right",num_str real_mult_1_right), |
|
553 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*) |
|
554 Thm ("realpow_zeroI",num_str realpow_zeroI), |
|
555 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*) |
|
556 Thm ("realpow_oneI",num_str realpow_oneI), |
|
557 (*"r ^^^ 1 = r"*) |
|
558 Thm ("realpow_eq_oneI",num_str realpow_eq_oneI) |
|
559 (*"1 ^^^ n = 1"*) |
|
560 ], scr = EmptyScr}:rls; |
|
561 |
|
562 val collect_numerals_ = |
|
563 Rls{id = "collect_numerals_", preconds = [], |
|
564 rew_ord = ("dummy_ord", dummy_ord), |
|
565 erls = Atools_erls, srls = Erls, |
|
566 calc = [("PLUS" , ("op +", eval_binop "#add_")) |
|
567 ], |
|
568 rules = [Thm ("real_num_collect",num_str real_num_collect), |
|
569 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
570 Thm ("real_num_collect_assoc_r",num_str real_num_collect_assoc_r), |
|
571 (*"[| l is_const; m is_const |] ==> \ |
|
572 \(k + m * n) + l * n = k + (l + m)*n"*) |
|
573 Thm ("real_one_collect",num_str real_one_collect), |
|
574 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
575 Thm ("real_one_collect_assoc_r",num_str real_one_collect_assoc_r), |
|
576 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*) |
|
577 |
|
578 Calc ("op +", eval_binop "#add_"), |
|
579 |
|
580 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen |
|
581 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *) |
|
582 Thm ("real_mult_2_assoc_r",num_str real_mult_2_assoc_r), |
|
583 (*"(k + z1) + z1 = k + 2 * z1"*) |
|
584 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)) |
|
585 (*"z1 + z1 = 2 * z1"*) |
|
586 |
|
587 ], scr = EmptyScr}:rls; |
|
588 |
|
589 val reduce_012_ = |
|
590 Rls{id = "reduce_012_", preconds = [], |
|
591 rew_ord = ("dummy_ord", dummy_ord), |
|
592 erls = e_rls,srls = Erls, |
|
593 calc = [], |
|
594 (*asm_thm = [],*) |
|
595 rules = [Thm ("real_mult_1",num_str real_mult_1), |
|
596 (*"1 * z = z"*) |
|
597 Thm ("real_mult_0",num_str real_mult_0), |
|
598 (*"0 * z = 0"*) |
|
599 Thm ("real_mult_0_right",num_str real_mult_0_right), |
|
600 (*"z * 0 = 0"*) |
|
601 Thm ("real_add_zero_left",num_str real_add_zero_left), |
|
602 (*"0 + z = z"*) |
|
603 Thm ("real_add_zero_right",num_str real_add_zero_right), |
|
604 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*) |
|
605 |
|
606 (*Thm ("realpow_oneI",num_str realpow_oneI)*) |
|
607 (*"?r ^^^ 1 = ?r"*) |
|
608 Thm ("real_0_divide",num_str real_0_divide)(*WN060914*) |
|
609 (*"0 / ?x = 0"*) |
|
610 ], scr = EmptyScr}:rls; |
|
611 |
|
612 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*) |
|
613 val discard_parentheses_ = |
|
614 append_rls "discard_parentheses_" e_rls |
|
615 [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)) |
|
616 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*) |
|
617 (*Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))*) |
|
618 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*) |
|
619 ]; |
|
620 |
|
621 (*----------------- End: rulesets for make_polynomial_ -----------------*) |
|
622 |
|
623 (*MG.0401 ev. for use in rls with ordered rewriting ? |
|
624 val collect_numerals_left = |
|
625 Rls{id = "collect_numerals", preconds = [], |
|
626 rew_ord = ("dummy_ord", dummy_ord), |
|
627 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
|
628 calc = [("PLUS" , ("op +", eval_binop "#add_")), |
|
629 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
630 ("POWER", ("Atools.pow", eval_binop "#power_")) |
|
631 ], |
|
632 (*asm_thm = [],*) |
|
633 rules = [Thm ("real_num_collect",num_str real_num_collect), |
|
634 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
635 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc), |
|
636 (*"[| l is_const; m is_const |] ==> |
|
637 l * n + (m * n + k) = (l + m) * n + k"*) |
|
638 Thm ("real_one_collect",num_str real_one_collect), |
|
639 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
640 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), |
|
641 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*) |
|
642 |
|
643 Calc ("op +", eval_binop "#add_"), |
|
644 |
|
645 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*) |
|
646 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
647 (*"z1 + z1 = 2 * z1"*) |
|
648 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc) |
|
649 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
650 ], scr = EmptyScr}:rls;*) |
|
651 |
|
652 val expand_poly = |
|
653 Rls{id = "expand_poly", preconds = [], |
|
654 rew_ord = ("dummy_ord", dummy_ord), |
|
655 erls = e_rls,srls = Erls, |
|
656 calc = [], |
|
657 (*asm_thm = [],*) |
|
658 rules = [Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
659 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
660 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
661 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
662 (*Thm ("real_add_mult_distrib1",num_str real_add_mult_distrib1), |
|
663 ....... 18.3.03 undefined???*) |
|
664 |
|
665 Thm ("real_plus_binom_pow2",num_str real_plus_binom_pow2), |
|
666 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*) |
|
667 Thm ("real_minus_binom_pow2_p",num_str real_minus_binom_pow2_p), |
|
668 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*) |
|
669 Thm ("real_plus_minus_binom1_p", |
|
670 num_str real_plus_minus_binom1_p), |
|
671 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*) |
|
672 Thm ("real_plus_minus_binom2_p", |
|
673 num_str real_plus_minus_binom2_p), |
|
674 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*) |
|
675 |
|
676 Thm ("real_minus_minus",num_str real_minus_minus), |
|
677 (*"- (- ?z) = ?z"*) |
|
678 Thm ("real_diff_minus",num_str real_diff_minus), |
|
679 (*"a - b = a + -1 * b"*) |
|
680 Thm ("sym_real_mult_minus1",num_str (real_mult_minus1 RS sym)) |
|
681 (*- ?z = "-1 * ?z"*) |
|
682 |
|
683 (*Thm ("",num_str ), |
|
684 Thm ("",num_str ), |
|
685 Thm ("",num_str ),*) |
|
686 (*Thm ("real_minus_add_distrib", |
|
687 num_str real_minus_add_distrib),*) |
|
688 (*"- (?x + ?y) = - ?x + - ?y"*) |
|
689 (*Thm ("real_diff_plus",num_str real_diff_plus)*) |
|
690 (*"a - b = a + -b"*) |
|
691 ], scr = EmptyScr}:rls; |
|
692 val simplify_power = |
|
693 Rls{id = "simplify_power", preconds = [], |
|
694 rew_ord = ("dummy_ord", dummy_ord), |
|
695 erls = e_rls, srls = Erls, |
|
696 calc = [], |
|
697 (*asm_thm = [],*) |
|
698 rules = [Thm ("realpow_multI", num_str realpow_multI), |
|
699 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
|
700 |
|
701 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)), |
|
702 (*"r1 * r1 = r1 ^^^ 2"*) |
|
703 Thm ("realpow_plus_1",num_str realpow_plus_1), |
|
704 (*"r * r ^^^ n = r ^^^ (n + 1)"*) |
|
705 Thm ("realpow_pow",num_str realpow_pow), |
|
706 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*) |
|
707 Thm ("sym_realpow_addI",num_str (realpow_addI RS sym)), |
|
708 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*) |
|
709 Thm ("realpow_oneI",num_str realpow_oneI), |
|
710 (*"r ^^^ 1 = r"*) |
|
711 Thm ("realpow_eq_oneI",num_str realpow_eq_oneI) |
|
712 (*"1 ^^^ n = 1"*) |
|
713 ], scr = EmptyScr}:rls; |
|
714 (*MG.0401: termorders for multivariate polys dropped due to principal problems: |
|
715 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*) |
|
716 val order_add_mult = |
|
717 Rls{id = "order_add_mult", preconds = [], |
|
718 rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy), |
|
719 erls = e_rls,srls = Erls, |
|
720 calc = [], |
|
721 (*asm_thm = [],*) |
|
722 rules = [Thm ("real_mult_commute",num_str real_mult_commute), |
|
723 (* z * w = w * z *) |
|
724 Thm ("real_mult_left_commute",num_str real_mult_left_commute), |
|
725 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
|
726 Thm ("real_mult_assoc",num_str real_mult_assoc), |
|
727 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) |
|
728 Thm ("real_add_commute",num_str real_add_commute), |
|
729 (*z + w = w + z*) |
|
730 Thm ("real_add_left_commute",num_str real_add_left_commute), |
|
731 (*x + (y + z) = y + (x + z)*) |
|
732 Thm ("real_add_assoc",num_str real_add_assoc) |
|
733 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*) |
|
734 ], scr = EmptyScr}:rls; |
|
735 (*MG.0401: termorders for multivariate polys dropped due to principal problems: |
|
736 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*) |
|
737 val order_mult = |
|
738 Rls{id = "order_mult", preconds = [], |
|
739 rew_ord = ("ord_make_polynomial",ord_make_polynomial false Poly.thy), |
|
740 erls = e_rls,srls = Erls, |
|
741 calc = [], |
|
742 (*asm_thm = [],*) |
|
743 rules = [Thm ("real_mult_commute",num_str real_mult_commute), |
|
744 (* z * w = w * z *) |
|
745 Thm ("real_mult_left_commute",num_str real_mult_left_commute), |
|
746 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*) |
|
747 Thm ("real_mult_assoc",num_str real_mult_assoc) |
|
748 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*) |
|
749 ], scr = EmptyScr}:rls; |
|
750 val collect_numerals = |
|
751 Rls{id = "collect_numerals", preconds = [], |
|
752 rew_ord = ("dummy_ord", dummy_ord), |
|
753 erls = Atools_erls(*erls3.4.03*),srls = Erls, |
|
754 calc = [("PLUS" , ("op +", eval_binop "#add_")), |
|
755 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
756 ("POWER", ("Atools.pow", eval_binop "#power_")) |
|
757 ], |
|
758 (*asm_thm = [],*) |
|
759 rules = [Thm ("real_num_collect",num_str real_num_collect), |
|
760 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
761 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc), |
|
762 (*"[| l is_const; m is_const |] ==> |
|
763 l * n + (m * n + k) = (l + m) * n + k"*) |
|
764 Thm ("real_one_collect",num_str real_one_collect), |
|
765 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
766 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), |
|
767 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
768 Calc ("op +", eval_binop "#add_"), |
|
769 Calc ("op *", eval_binop "#mult_"), |
|
770 Calc ("Atools.pow", eval_binop "#power_") |
|
771 ], scr = EmptyScr}:rls; |
|
772 val reduce_012 = |
|
773 Rls{id = "reduce_012", preconds = [], |
|
774 rew_ord = ("dummy_ord", dummy_ord), |
|
775 erls = e_rls,srls = Erls, |
|
776 calc = [], |
|
777 (*asm_thm = [],*) |
|
778 rules = [Thm ("real_mult_1",num_str real_mult_1), |
|
779 (*"1 * z = z"*) |
|
780 (*Thm ("real_mult_minus1",num_str real_mult_minus1),14.3.03*) |
|
781 (*"-1 * z = - z"*) |
|
782 Thm ("sym_real_mult_minus_eq1", |
|
783 num_str (real_mult_minus_eq1 RS sym)), |
|
784 (*- (?x * ?y) = "- ?x * ?y"*) |
|
785 (*Thm ("real_minus_mult_cancel",num_str real_minus_mult_cancel), |
|
786 (*"- ?x * - ?y = ?x * ?y"*)---*) |
|
787 Thm ("real_mult_0",num_str real_mult_0), |
|
788 (*"0 * z = 0"*) |
|
789 Thm ("real_add_zero_left",num_str real_add_zero_left), |
|
790 (*"0 + z = z"*) |
|
791 Thm ("real_add_minus",num_str real_add_minus), |
|
792 (*"?z + - ?z = 0"*) |
|
793 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
794 (*"z1 + z1 = 2 * z1"*) |
|
795 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc) |
|
796 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
797 ], scr = EmptyScr}:rls; |
|
798 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*) |
|
799 val discard_parentheses = |
|
800 append_rls "discard_parentheses" e_rls |
|
801 [Thm ("sym_real_mult_assoc", num_str (real_mult_assoc RS sym)), |
|
802 Thm ("sym_real_add_assoc",num_str (real_add_assoc RS sym))]; |
|
803 |
|
804 val scr_make_polynomial = |
|
805 "Script Expand_binoms t_ =\ |
|
806 \(Repeat \ |
|
807 \((Try (Repeat (Rewrite real_diff_minus False))) @@ \ |
|
808 |
|
809 \ (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ \ |
|
810 \ (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ \ |
|
811 \ (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ \ |
|
812 \ (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ \ |
|
813 |
|
814 \ (Try (Repeat (Rewrite real_mult_1 False))) @@ \ |
|
815 \ (Try (Repeat (Rewrite real_mult_0 False))) @@ \ |
|
816 \ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \ |
|
817 |
|
818 \ (Try (Repeat (Rewrite real_mult_commute False))) @@ \ |
|
819 \ (Try (Repeat (Rewrite real_mult_left_commute False))) @@ \ |
|
820 \ (Try (Repeat (Rewrite real_mult_assoc False))) @@ \ |
|
821 \ (Try (Repeat (Rewrite real_add_commute False))) @@ \ |
|
822 \ (Try (Repeat (Rewrite real_add_left_commute False))) @@ \ |
|
823 \ (Try (Repeat (Rewrite real_add_assoc False))) @@ \ |
|
824 |
|
825 \ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \ |
|
826 \ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \ |
|
827 \ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \ |
|
828 \ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \ |
|
829 |
|
830 \ (Try (Repeat (Rewrite real_num_collect False))) @@ \ |
|
831 \ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \ |
|
832 |
|
833 \ (Try (Repeat (Rewrite real_one_collect False))) @@ \ |
|
834 \ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \ |
|
835 |
|
836 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
837 \ (Try (Repeat (Calculate times ))) @@ \ |
|
838 \ (Try (Repeat (Calculate power_)))) \ |
|
839 \ t_)"; |
|
840 |
|
841 (*version used by MG.02/03, overwritten by version AG in 04 below |
|
842 val make_polynomial = prep_rls( |
|
843 Seq{id = "make_polynomial", preconds = []:term list, |
|
844 rew_ord = ("dummy_ord", dummy_ord), |
|
845 erls = Atools_erls, srls = Erls, |
|
846 calc = [],(*asm_thm = [],*) |
|
847 rules = [Rls_ expand_poly, |
|
848 Rls_ order_add_mult, |
|
849 Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *) |
|
850 Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *) |
|
851 Rls_ reduce_012, |
|
852 Thm ("realpow_oneI",num_str realpow_oneI),(*in --^*) |
|
853 Rls_ discard_parentheses |
|
854 ], |
|
855 scr = EmptyScr |
|
856 }:rls); *) |
|
857 |
|
858 val scr_expand_binoms = |
|
859 "Script Expand_binoms t_ =\ |
|
860 \(Repeat \ |
|
861 \((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ \ |
|
862 \ (Try (Repeat (Rewrite real_plus_binom_times False))) @@ \ |
|
863 \ (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ \ |
|
864 \ (Try (Repeat (Rewrite real_minus_binom_times False))) @@ \ |
|
865 \ (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ \ |
|
866 \ (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ \ |
|
867 |
|
868 \ (Try (Repeat (Rewrite real_mult_1 False))) @@ \ |
|
869 \ (Try (Repeat (Rewrite real_mult_0 False))) @@ \ |
|
870 \ (Try (Repeat (Rewrite real_add_zero_left False))) @@ \ |
|
871 |
|
872 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
873 \ (Try (Repeat (Calculate times ))) @@ \ |
|
874 \ (Try (Repeat (Calculate power_))) @@ \ |
|
875 |
|
876 \ (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ \ |
|
877 \ (Try (Repeat (Rewrite realpow_plus_1 False))) @@ \ |
|
878 \ (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ \ |
|
879 \ (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ \ |
|
880 |
|
881 \ (Try (Repeat (Rewrite real_num_collect False))) @@ \ |
|
882 \ (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ \ |
|
883 |
|
884 \ (Try (Repeat (Rewrite real_one_collect False))) @@ \ |
|
885 \ (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ \ |
|
886 |
|
887 \ (Try (Repeat (Calculate plus ))) @@ \ |
|
888 \ (Try (Repeat (Calculate times ))) @@ \ |
|
889 \ (Try (Repeat (Calculate power_)))) \ |
|
890 \ t_)"; |
|
891 |
|
892 val expand_binoms = |
|
893 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI), |
|
894 erls = Atools_erls, srls = Erls, |
|
895 calc = [("PLUS" , ("op +", eval_binop "#add_")), |
|
896 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
897 ("POWER", ("Atools.pow", eval_binop "#power_")) |
|
898 ], |
|
899 (*asm_thm = [],*) |
|
900 rules = [Thm ("real_plus_binom_pow2" ,num_str real_plus_binom_pow2), |
|
901 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*) |
|
902 Thm ("real_plus_binom_times" ,num_str real_plus_binom_times), |
|
903 (*"(a + b)*(a + b) = ...*) |
|
904 Thm ("real_minus_binom_pow2" ,num_str real_minus_binom_pow2), |
|
905 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*) |
|
906 Thm ("real_minus_binom_times",num_str real_minus_binom_times), |
|
907 (*"(a - b)*(a - b) = ...*) |
|
908 Thm ("real_plus_minus_binom1",num_str real_plus_minus_binom1), |
|
909 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*) |
|
910 Thm ("real_plus_minus_binom2",num_str real_plus_minus_binom2), |
|
911 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*) |
|
912 (*RL 020915*) |
|
913 Thm ("real_pp_binom_times",num_str real_pp_binom_times), |
|
914 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*) |
|
915 Thm ("real_pm_binom_times",num_str real_pm_binom_times), |
|
916 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*) |
|
917 Thm ("real_mp_binom_times",num_str real_mp_binom_times), |
|
918 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*) |
|
919 Thm ("real_mm_binom_times",num_str real_mm_binom_times), |
|
920 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*) |
|
921 Thm ("realpow_multI",num_str realpow_multI), |
|
922 (*(a*b)^^^n = a^^^n * b^^^n*) |
|
923 Thm ("real_plus_binom_pow3",num_str real_plus_binom_pow3), |
|
924 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *) |
|
925 Thm ("real_minus_binom_pow3",num_str real_minus_binom_pow3), |
|
926 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *) |
|
927 |
|
928 |
|
929 (* Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
930 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
931 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
932 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
933 Thm ("real_diff_mult_distrib" ,num_str real_diff_mult_distrib), |
|
934 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*) |
|
935 Thm ("real_diff_mult_distrib2",num_str real_diff_mult_distrib2), |
|
936 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*) |
|
937 *) |
|
938 |
|
939 Thm ("real_mult_1",num_str real_mult_1), (*"1 * z = z"*) |
|
940 Thm ("real_mult_0",num_str real_mult_0), (*"0 * z = 0"*) |
|
941 Thm ("real_add_zero_left",num_str real_add_zero_left),(*"0 + z = z"*) |
|
942 |
|
943 Calc ("op +", eval_binop "#add_"), |
|
944 Calc ("op *", eval_binop "#mult_"), |
|
945 Calc ("Atools.pow", eval_binop "#power_"), |
|
946 (* |
|
947 Thm ("real_mult_commute",num_str real_mult_commute), (*AC-rewriting*) |
|
948 Thm ("real_mult_left_commute",num_str real_mult_left_commute), (**) |
|
949 Thm ("real_mult_assoc",num_str real_mult_assoc), (**) |
|
950 Thm ("real_add_commute",num_str real_add_commute), (**) |
|
951 Thm ("real_add_left_commute",num_str real_add_left_commute), (**) |
|
952 Thm ("real_add_assoc",num_str real_add_assoc), (**) |
|
953 *) |
|
954 |
|
955 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)), |
|
956 (*"r1 * r1 = r1 ^^^ 2"*) |
|
957 Thm ("realpow_plus_1",num_str realpow_plus_1), |
|
958 (*"r * r ^^^ n = r ^^^ (n + 1)"*) |
|
959 (*Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
960 (*"z1 + z1 = 2 * z1"*)*) |
|
961 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc), |
|
962 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
963 |
|
964 Thm ("real_num_collect",num_str real_num_collect), |
|
965 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*) |
|
966 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc), |
|
967 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*) |
|
968 Thm ("real_one_collect",num_str real_one_collect), |
|
969 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
970 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), |
|
971 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
972 |
|
973 Calc ("op +", eval_binop "#add_"), |
|
974 Calc ("op *", eval_binop "#mult_"), |
|
975 Calc ("Atools.pow", eval_binop "#power_") |
|
976 ], |
|
977 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms) |
|
978 }:rls; |
|
979 |
|
980 |
|
981 "******* Poly.ML end ******* ...RL"; |
|
982 |
|
983 |
|
984 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**) |
|
985 |
|
986 (*FIXME.0401: make SML-order local to make_polynomial(_) *) |
|
987 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *) |
|
988 (* Polynom --> List von Monomen *) |
|
989 fun poly2list (Const ("op +",_) $ t1 $ t2) = |
|
990 (poly2list t1) @ (poly2list t2) |
|
991 | poly2list t = [t]; |
|
992 |
|
993 (* Monom --> Liste von Variablen *) |
|
994 fun monom2list (Const ("op *",_) $ t1 $ t2) = |
|
995 (monom2list t1) @ (monom2list t2) |
|
996 | monom2list t = [t]; |
|
997 |
|
998 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *) |
|
999 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str |
|
1000 | get_basStr (Free (str, _)) = str |
|
1001 | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *) |
|
1002 (*| get_basStr t = |
|
1003 raise error("get_basStr: called with t= "^(term2str t));*) |
|
1004 |
|
1005 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *) |
|
1006 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str |
|
1007 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *) |
|
1008 | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *) |
|
1009 | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *) |
|
1010 (*| get_potStr t = |
|
1011 raise error("get_potStr: called with t= "^(term2str t));*) |
|
1012 |
|
1013 (* Umgekehrte string_ord *) |
|
1014 val string_ord_rev = rev_order o string_ord; |
|
1015 |
|
1016 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen) |
|
1017 innerhalb eines Monomes: |
|
1018 - zuerst lexikographisch nach Variablenname |
|
1019 - wenn gleich: nach steigender Potenz *) |
|
1020 fun var_ord (a,b: term) = prod_ord string_ord string_ord |
|
1021 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)); |
|
1022 |
|
1023 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen); |
|
1024 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung: |
|
1025 - zuerst lexikographisch nach Variablenname |
|
1026 - wenn gleich: nach sinkender Potenz*) |
|
1027 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev |
|
1028 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b)); |
|
1029 |
|
1030 |
|
1031 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *) |
|
1032 val sort_varList = sort var_ord; |
|
1033 |
|
1034 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt |
|
1035 Argumente in eine Liste *) |
|
1036 fun args u : term list = |
|
1037 let fun stripc (f$t, ts) = stripc (f, t::ts) |
|
1038 | stripc (t as Free _, ts) = (t::ts) |
|
1039 | stripc (_, ts) = ts |
|
1040 in stripc (u, []) end; |
|
1041 |
|
1042 (* liefert True, falls der Term (Liste von Termen) nur Zahlen |
|
1043 (keine Variablen) enthaelt *) |
|
1044 fun filter_num [] = true |
|
1045 | filter_num [Free x] = if (is_num (Free x)) then true |
|
1046 else false |
|
1047 | filter_num ((Free _)::_) = false |
|
1048 | filter_num ts = |
|
1049 (filter_num o (filter_out is_num) o flat o (map args)) ts; |
|
1050 |
|
1051 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt |
|
1052 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *) |
|
1053 fun is_nums t = filter_num [t]; |
|
1054 |
|
1055 (* Berechnet den Gesamtgrad eines Monoms *) |
|
1056 local |
|
1057 fun counter (n, []) = n |
|
1058 | counter (n, x :: xs) = |
|
1059 if (is_nums x) then |
|
1060 counter (n, xs) |
|
1061 else |
|
1062 (case x of |
|
1063 (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) => |
|
1064 if (is_nums (Free (str_h, T))) then |
|
1065 counter (n + (the (int_of_str str_h)), xs) |
|
1066 else counter (n + 1000, xs) (*FIXME.MG?!*) |
|
1067 | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) => |
|
1068 counter (n + 1000, xs) (*FIXME.MG?!*) |
|
1069 | (Free (str, _)) => counter (n + 1, xs) |
|
1070 (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*) |
|
1071 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*) |
|
1072 in |
|
1073 fun monom_degree l = counter (0, l) |
|
1074 end; |
|
1075 |
|
1076 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich |
|
1077 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen, |
|
1078 werden jedoch dabei ignoriert (uebersprungen) *) |
|
1079 fun dict_cond_ord _ _ ([], []) = EQUAL |
|
1080 | dict_cond_ord _ _ ([], _ :: _) = LESS |
|
1081 | dict_cond_ord _ _ (_ :: _, []) = GREATER |
|
1082 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) = |
|
1083 (case (cond x, cond y) of |
|
1084 (false, false) => (case elem_ord (x, y) of |
|
1085 EQUAL => dict_cond_ord elem_ord cond (xs, ys) |
|
1086 | ord => ord) |
|
1087 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys) |
|
1088 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys) |
|
1089 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) ); |
|
1090 |
|
1091 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen): |
|
1092 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen - |
|
1093 dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *) |
|
1094 fun degree_ord (xs, ys) = |
|
1095 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums) |
|
1096 ((monom_degree xs, xs), (monom_degree ys, ys)); |
|
1097 |
|
1098 fun hd_str str = substring (str, 0, 1); |
|
1099 fun tl_str str = substring (str, 1, (size str) - 1); |
|
1100 |
|
1101 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *) |
|
1102 fun get_koeff_of_mon [] = raise error("get_koeff_of_mon: called with l = []") |
|
1103 | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x |
|
1104 else NONE; |
|
1105 |
|
1106 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *) |
|
1107 fun koeff2ordStr (SOME x) = (case x of |
|
1108 (Free (str, T)) => |
|
1109 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *) |
|
1110 else str |
|
1111 | _ => "aaa") (* "num.Ausdruck" --> gross *) |
|
1112 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *) |
|
1113 |
|
1114 (* Order zum Vergleich von Koeffizienten (strings): |
|
1115 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *) |
|
1116 fun compare_koeff_ord (xs, ys) = |
|
1117 string_ord ((koeff2ordStr o get_koeff_of_mon) xs, |
|
1118 (koeff2ordStr o get_koeff_of_mon) ys); |
|
1119 |
|
1120 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *) |
|
1121 fun koeff_degree_ord (xs, ys) = |
|
1122 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys)); |
|
1123 |
|
1124 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels |
|
1125 Gesamtgradordnung *) |
|
1126 val sort_monList = sort koeff_degree_ord; |
|
1127 |
|
1128 (* Alternativ zu degree_ord koennte auch die viel einfachere und |
|
1129 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht |
|
1130 fuer unsere Zwecke geeignet! |
|
1131 |
|
1132 fun simple_ord (al,bl: term list) = dict_ord string_ord |
|
1133 (map get_basStr al, map get_basStr bl); |
|
1134 |
|
1135 val sort_monList = sort simple_ord; *) |
|
1136 |
|
1137 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt |
|
1138 (mit gewuenschtem Typen T) *) |
|
1139 fun plus T = Const ("op +", [T,T] ---> T); |
|
1140 fun mult T = Const ("op *", [T,T] ---> T); |
|
1141 fun binop op_ t1 t2 = op_ $ t1 $ t2; |
|
1142 fun create_prod T (a,b) = binop (mult T) a b; |
|
1143 fun create_sum T (a,b) = binop (plus T) a b; |
|
1144 |
|
1145 (* löscht letztes Element einer Liste *) |
|
1146 fun drop_last l = take ((length l)-1,l); |
|
1147 |
|
1148 (* Liste von Variablen --> Monom *) |
|
1149 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl); |
|
1150 (* Bemerkung: |
|
1151 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei |
|
1152 gleiche Monome zusammengefasst werden können (collect_numerals)! |
|
1153 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*) |
|
1154 |
|
1155 (* Liste von Monomen --> Polynom *) |
|
1156 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml); |
|
1157 (* Bemerkung: |
|
1158 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) - |
|
1159 bessere Darstellung, da keine Klammern sichtbar! |
|
1160 (und discard_parentheses in make_polynomial hat weniger zu tun) *) |
|
1161 |
|
1162 (* sorts the variables (faktors) of an expanded polynomial lexicographical *) |
|
1163 fun sort_variables t = |
|
1164 let |
|
1165 val ll = map monom2list (poly2list t); |
|
1166 val lls = map sort_varList ll; |
|
1167 val T = type_of t; |
|
1168 val ls = map (create_monom T) lls; |
|
1169 in create_polynom T ls end; |
|
1170 |
|
1171 (* sorts the monoms of an expanded and variable-sorted polynomial |
|
1172 by total_degree *) |
|
1173 fun sort_monoms t = |
|
1174 let |
|
1175 val ll = map monom2list (poly2list t); |
|
1176 val lls = sort_monList ll; |
|
1177 val T = type_of t; |
|
1178 val ls = map (create_monom T) lls; |
|
1179 in create_polynom T ls end; |
|
1180 |
|
1181 (* auch Klammerung muss übereinstimmen; |
|
1182 sort_variables klammert Produkte rechtslastig*) |
|
1183 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t)); |
|
1184 |
|
1185 fun eval_is_multUnordered (thmid:string) _ |
|
1186 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy = |
|
1187 if is_multUnordered arg |
|
1188 then SOME (mk_thmid thmid "" |
|
1189 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
1190 Trueprop $ (mk_equality (t, HOLogic.true_const))) |
|
1191 else SOME (mk_thmid thmid "" |
|
1192 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
1193 Trueprop $ (mk_equality (t, HOLogic.false_const))) |
|
1194 | eval_is_multUnordered _ _ _ _ = NONE; |
|
1195 |
|
1196 |
|
1197 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
|
1198 []:(rule * (term * term list)) list; |
|
1199 fun init_state (_:term) = e_rrlsstate; |
|
1200 fun locate_rule (_:rule list list) (_:term) (_:rule) = |
|
1201 ([]:(rule * (term * term list)) list); |
|
1202 fun next_rule (_:rule list list) (_:term) = (NONE:rule option); |
|
1203 fun normal_form t = SOME (sort_variables t,[]:term list); |
|
1204 |
|
1205 val order_mult_ = |
|
1206 Rrls {id = "order_mult_", |
|
1207 prepat = |
|
1208 [([(term_of o the o (parse thy)) "p is_multUnordered"], |
|
1209 (term_of o the o (parse thy)) "?p" )], |
|
1210 rew_ord = ("dummy_ord", dummy_ord), |
|
1211 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*) |
|
1212 [Calc ("Poly.is'_multUnordered", eval_is_multUnordered "") |
|
1213 ], |
|
1214 calc = [("PLUS" ,("op +" ,eval_binop "#add_")), |
|
1215 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
|
1216 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), |
|
1217 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
|
1218 (*asm_thm=[],*) |
|
1219 scr=Rfuns {init_state = init_state, |
|
1220 normal_form = normal_form, |
|
1221 locate_rule = locate_rule, |
|
1222 next_rule = next_rule, |
|
1223 attach_form = attach_form}}; |
|
1224 |
|
1225 val order_mult_rls_ = |
|
1226 Rls{id = "order_mult_rls_", preconds = [], |
|
1227 rew_ord = ("dummy_ord", dummy_ord), |
|
1228 erls = e_rls,srls = Erls, |
|
1229 calc = [], |
|
1230 (*asm_thm = [],*) |
|
1231 rules = [Rls_ order_mult_ |
|
1232 ], scr = EmptyScr}:rls; |
|
1233 |
|
1234 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t)); |
|
1235 |
|
1236 (*WN.18.6.03 *) |
|
1237 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*) |
|
1238 fun eval_is_addUnordered (thmid:string) _ |
|
1239 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy = |
|
1240 if is_addUnordered arg |
|
1241 then SOME (mk_thmid thmid "" |
|
1242 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
1243 Trueprop $ (mk_equality (t, HOLogic.true_const))) |
|
1244 else SOME (mk_thmid thmid "" |
|
1245 ((Syntax.string_of_term (thy2ctxt thy)) arg) "", |
|
1246 Trueprop $ (mk_equality (t, HOLogic.false_const))) |
|
1247 | eval_is_addUnordered _ _ _ _ = NONE; |
|
1248 |
|
1249 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*) |
|
1250 []:(rule * (term * term list)) list; |
|
1251 fun init_state (_:term) = e_rrlsstate; |
|
1252 fun locate_rule (_:rule list list) (_:term) (_:rule) = |
|
1253 ([]:(rule * (term * term list)) list); |
|
1254 fun next_rule (_:rule list list) (_:term) = (NONE:rule option); |
|
1255 fun normal_form t = SOME (sort_monoms t,[]:term list); |
|
1256 |
|
1257 val order_add_ = |
|
1258 Rrls {id = "order_add_", |
|
1259 prepat = (*WN.18.6.03 Preconditions und Pattern, |
|
1260 die beide passen muessen, damit das Rrls angewandt wird*) |
|
1261 [([(term_of o the o (parse thy)) "p is_addUnordered"], |
|
1262 (term_of o the o (parse thy)) "?p" |
|
1263 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment |
|
1264 fuer die Evaluation der Precondition "p is_addUnordered"*))], |
|
1265 rew_ord = ("dummy_ord", dummy_ord), |
|
1266 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*) |
|
1267 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "") |
|
1268 (*WN.18.6.03 definiert in Poly.thy, |
|
1269 evaluiert prepat*)], |
|
1270 calc = [("PLUS" ,("op +" ,eval_binop "#add_")), |
|
1271 ("TIMES" ,("op *" ,eval_binop "#mult_")), |
|
1272 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")), |
|
1273 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))], |
|
1274 (*asm_thm=[],*) |
|
1275 scr=Rfuns {init_state = init_state, |
|
1276 normal_form = normal_form, |
|
1277 locate_rule = locate_rule, |
|
1278 next_rule = next_rule, |
|
1279 attach_form = attach_form}}; |
|
1280 |
|
1281 val order_add_rls_ = |
|
1282 Rls{id = "order_add_rls_", preconds = [], |
|
1283 rew_ord = ("dummy_ord", dummy_ord), |
|
1284 erls = e_rls,srls = Erls, |
|
1285 calc = [], |
|
1286 (*asm_thm = [],*) |
|
1287 rules = [Rls_ order_add_ |
|
1288 ], scr = EmptyScr}:rls; |
|
1289 |
|
1290 (*. see MG-DA.p.52ff .*) |
|
1291 val make_polynomial(*MG.03, overwrites version from above, |
|
1292 previously 'make_polynomial_'*) = |
|
1293 Seq {id = "make_polynomial", preconds = []:term list, |
|
1294 rew_ord = ("dummy_ord", dummy_ord), |
|
1295 erls = Atools_erls, srls = Erls,calc = [], |
|
1296 rules = [Rls_ discard_minus_, |
|
1297 Rls_ expand_poly_, |
|
1298 Calc ("op *", eval_binop "#mult_"), |
|
1299 Rls_ order_mult_rls_, |
|
1300 Rls_ simplify_power_, |
|
1301 Rls_ calc_add_mult_pow_, |
|
1302 Rls_ reduce_012_mult_, |
|
1303 Rls_ order_add_rls_, |
|
1304 Rls_ collect_numerals_, |
|
1305 Rls_ reduce_012_, |
|
1306 Rls_ discard_parentheses_ |
|
1307 ], |
|
1308 scr = EmptyScr |
|
1309 }:rls; |
|
1310 val norm_Poly(*=make_polynomial*) = |
|
1311 Seq {id = "norm_Poly", preconds = []:term list, |
|
1312 rew_ord = ("dummy_ord", dummy_ord), |
|
1313 erls = Atools_erls, srls = Erls, calc = [], |
|
1314 rules = [Rls_ discard_minus_, |
|
1315 Rls_ expand_poly_, |
|
1316 Calc ("op *", eval_binop "#mult_"), |
|
1317 Rls_ order_mult_rls_, |
|
1318 Rls_ simplify_power_, |
|
1319 Rls_ calc_add_mult_pow_, |
|
1320 Rls_ reduce_012_mult_, |
|
1321 Rls_ order_add_rls_, |
|
1322 Rls_ collect_numerals_, |
|
1323 Rls_ reduce_012_, |
|
1324 Rls_ discard_parentheses_ |
|
1325 ], |
|
1326 scr = EmptyScr |
|
1327 }:rls; |
|
1328 |
|
1329 (* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses_ |
|
1330 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*) |
|
1331 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*) |
|
1332 val make_rat_poly_with_parentheses = |
|
1333 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list, |
|
1334 rew_ord = ("dummy_ord", dummy_ord), |
|
1335 erls = Atools_erls, srls = Erls, calc = [], |
|
1336 rules = [Rls_ discard_minus_, |
|
1337 Rls_ expand_poly_rat_,(*ignors rationals*) |
|
1338 Calc ("op *", eval_binop "#mult_"), |
|
1339 Rls_ order_mult_rls_, |
|
1340 Rls_ simplify_power_, |
|
1341 Rls_ calc_add_mult_pow_, |
|
1342 Rls_ reduce_012_mult_, |
|
1343 Rls_ order_add_rls_, |
|
1344 Rls_ collect_numerals_, |
|
1345 Rls_ reduce_012_ |
|
1346 (*Rls_ discard_parentheses_ *) |
|
1347 ], |
|
1348 scr = EmptyScr |
|
1349 }:rls; |
|
1350 |
|
1351 (*.a minimal ruleset for reverse rewriting of factions [2]; |
|
1352 compare expand_binoms.*) |
|
1353 val rev_rew_p = |
|
1354 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI), |
|
1355 erls = Atools_erls, srls = Erls, |
|
1356 calc = [(*("PLUS" , ("op +", eval_binop "#add_")), |
|
1357 ("TIMES" , ("op *", eval_binop "#mult_")), |
|
1358 ("POWER", ("Atools.pow", eval_binop "#power_"))*) |
|
1359 ], |
|
1360 rules = [Thm ("real_plus_binom_times" ,num_str real_plus_binom_times), |
|
1361 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*) |
|
1362 Thm ("real_plus_binom_times1" ,num_str real_plus_binom_times1), |
|
1363 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*) |
|
1364 Thm ("real_plus_binom_times2" ,num_str real_plus_binom_times2), |
|
1365 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*) |
|
1366 |
|
1367 Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*) |
|
1368 |
|
1369 Thm ("real_add_mult_distrib" ,num_str real_add_mult_distrib), |
|
1370 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*) |
|
1371 Thm ("real_add_mult_distrib2",num_str real_add_mult_distrib2), |
|
1372 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*) |
|
1373 |
|
1374 Thm ("real_mult_assoc", num_str real_mult_assoc), |
|
1375 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*) |
|
1376 Rls_ order_mult_rls_, |
|
1377 (*Rls_ order_add_rls_,*) |
|
1378 |
|
1379 Calc ("op +", eval_binop "#add_"), |
|
1380 Calc ("op *", eval_binop "#mult_"), |
|
1381 Calc ("Atools.pow", eval_binop "#power_"), |
|
1382 |
|
1383 Thm ("sym_realpow_twoI",num_str (realpow_twoI RS sym)), |
|
1384 (*"r1 * r1 = r1 ^^^ 2"*) |
|
1385 Thm ("sym_real_mult_2",num_str (real_mult_2 RS sym)), |
|
1386 (*"z1 + z1 = 2 * z1"*) |
|
1387 Thm ("real_mult_2_assoc",num_str real_mult_2_assoc), |
|
1388 (*"z1 + (z1 + k) = 2 * z1 + k"*) |
|
1389 |
|
1390 Thm ("real_num_collect",num_str real_num_collect), |
|
1391 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*) |
|
1392 Thm ("real_num_collect_assoc",num_str real_num_collect_assoc), |
|
1393 (*"[| l is_const; m is_const |] ==> |
|
1394 l * n + (m * n + k) = (l + m) * n + k"*) |
|
1395 Thm ("real_one_collect",num_str real_one_collect), |
|
1396 (*"m is_const ==> n + m * n = (1 + m) * n"*) |
|
1397 Thm ("real_one_collect_assoc",num_str real_one_collect_assoc), |
|
1398 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*) |
|
1399 |
|
1400 Thm ("realpow_multI", num_str realpow_multI), |
|
1401 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*) |
|
1402 |
|
1403 Calc ("op +", eval_binop "#add_"), |
|
1404 Calc ("op *", eval_binop "#mult_"), |
|
1405 Calc ("Atools.pow", eval_binop "#power_"), |
|
1406 |
|
1407 Thm ("real_mult_1",num_str real_mult_1),(*"1 * z = z"*) |
|
1408 Thm ("real_mult_0",num_str real_mult_0),(*"0 * z = 0"*) |
|
1409 Thm ("real_add_zero_left",num_str real_add_zero_left)(*0 + z = z*) |
|
1410 |
|
1411 (*Rls_ order_add_rls_*) |
|
1412 ], |
|
1413 |
|
1414 scr = EmptyScr}:rls; |
|
1415 |
|
1416 ruleset' := |
|
1417 overwritelthy thy (!ruleset', |
|
1418 [("norm_Poly", prep_rls norm_Poly), |
|
1419 ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*), |
|
1420 ("expand", prep_rls expand), |
|
1421 ("expand_poly", prep_rls expand_poly), |
|
1422 ("simplify_power", prep_rls simplify_power), |
|
1423 ("order_add_mult", prep_rls order_add_mult), |
|
1424 ("collect_numerals", prep_rls collect_numerals), |
|
1425 ("collect_numerals_", prep_rls collect_numerals_), |
|
1426 ("reduce_012", prep_rls reduce_012), |
|
1427 ("discard_parentheses", prep_rls discard_parentheses), |
|
1428 ("make_polynomial", prep_rls make_polynomial), |
|
1429 ("expand_binoms", prep_rls expand_binoms), |
|
1430 ("rev_rew_p", prep_rls rev_rew_p), |
|
1431 ("discard_minus_", prep_rls discard_minus_), |
|
1432 ("expand_poly_", prep_rls expand_poly_), |
|
1433 ("expand_poly_rat_", prep_rls expand_poly_rat_), |
|
1434 ("simplify_power_", prep_rls simplify_power_), |
|
1435 ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_), |
|
1436 ("reduce_012_mult_", prep_rls reduce_012_mult_), |
|
1437 ("reduce_012_", prep_rls reduce_012_), |
|
1438 ("discard_parentheses_",prep_rls discard_parentheses_), |
|
1439 ("order_mult_rls_", prep_rls order_mult_rls_), |
|
1440 ("order_add_rls_", prep_rls order_add_rls_), |
|
1441 ("make_rat_poly_with_parentheses", |
|
1442 prep_rls make_rat_poly_with_parentheses) |
|
1443 (*("", prep_rls ), |
|
1444 ("", prep_rls ), |
|
1445 ("", prep_rls ) |
|
1446 *) |
|
1447 ]); |
|
1448 |
|
1449 calclist':= overwritel (!calclist', |
|
1450 [("is_polyrat_in", ("Poly.is'_polyrat'_in", |
|
1451 eval_is_polyrat_in "#eval_is_polyrat_in")), |
|
1452 ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")), |
|
1453 ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")), |
|
1454 ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")), |
|
1455 ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")), |
|
1456 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")), |
|
1457 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered "")) |
|
1458 ]); |
|
1459 |
|
1460 |
|
1461 (** problems **) |
|
1462 |
|
1463 store_pbt |
|
1464 (prep_pbt Poly.thy "pbl_simp_poly" [] e_pblID |
|
1465 (["polynomial","simplification"], |
|
1466 [("#Given" ,["term t_"]), |
|
1467 ("#Where" ,["t_ is_polyexp"]), |
|
1468 ("#Find" ,["normalform n_"]) |
|
1469 ], |
|
1470 append_rls "e_rls" e_rls [(*for preds in where_*) |
|
1471 Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
|
1472 SOME "Simplify t_", |
|
1473 [["simplification","for_polynomials"]])); |
|
1474 |
|
1475 |
|
1476 (** methods **) |
|
1477 |
|
1478 store_met |
|
1479 (prep_met Poly.thy "met_simp_poly" [] e_metID |
|
1480 (["simplification","for_polynomials"], |
|
1481 [("#Given" ,["term t_"]), |
|
1482 ("#Where" ,["t_ is_polyexp"]), |
|
1483 ("#Find" ,["normalform n_"]) |
|
1484 ], |
|
1485 {rew_ord'="tless_true", |
|
1486 rls' = e_rls, |
|
1487 calc = [], |
|
1488 srls = e_rls, |
|
1489 prls = append_rls "simplification_for_polynomials_prls" e_rls |
|
1490 [(*for preds in where_*) |
|
1491 Calc ("Poly.is'_polyexp",eval_is_polyexp"")], |
|
1492 crls = e_rls, nrls = norm_Poly}, |
|
1493 "Script SimplifyScript (t_::real) = \ |
|
1494 \ ((Rewrite_Set norm_Poly False) t_)" |
|
1495 )); |