1 (* WN.020812: theorems in the Reals,
2 necessary for special rule sets, in addition to Isabelle2002.
3 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4 !!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
5 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
6 xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
7 changed by: Richard Lang 020912
10 theory Poly imports Simplify begin
14 is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
15 is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
16 has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
17 is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
19 is'_multUnordered:: "real => bool" ("_ is'_multUnordered")
20 is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
21 is'_polyexp :: "real => bool" ("_ is'_polyexp")
26 ("((Script Expand'_binoms (_ =))//
29 (*-------------------- rules------------------------------------------------*)
30 axioms (*.not contained in Isabelle2002,
31 stated as axioms, TODO: prove as theorems;
32 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
34 realpow_pow "(a ^^^ b) ^^^ c = a ^^^ (b * c)"
35 realpow_addI "r ^^^ (n + m) = r ^^^ n * r ^^^ m"
36 realpow_addI_assoc_l "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"
37 realpow_addI_assoc_r "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)"
39 realpow_oneI "r ^^^ 1 = r"
40 realpow_zeroI "r ^^^ 0 = 1"
41 realpow_eq_oneI "1 ^^^ n = 1"
42 realpow_multI "(r * s) ^^^ n = r ^^^ n * s ^^^ n"
43 realpow_multI_poly "[| r is_polyexp; s is_polyexp |] ==>
44 (r * s) ^^^ n = r ^^^ n * s ^^^ n"
45 realpow_minus_oneI "-1 ^^^ (2 * n) = 1"
47 realpow_twoI "r ^^^ 2 = r * r"
48 realpow_twoI_assoc_l "r * (r * s) = r ^^^ 2 * s"
49 realpow_twoI_assoc_r "s * r * r = s * r ^^^ 2"
50 realpow_two_atom "r is_atom ==> r * r = r ^^^ 2"
51 realpow_plus_1 "r * r ^^^ n = r ^^^ (n + 1)"
52 realpow_plus_1_assoc_l "r * (r ^^^ m * s) = r ^^^ (1 + m) * s"
53 realpow_plus_1_assoc_l2 "r ^^^ m * (r * s) = r ^^^ (1 + m) * s"
54 realpow_plus_1_assoc_r "s * r * r ^^^ m = s * r ^^^ (1 + m)"
55 realpow_plus_1_atom "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)"
56 realpow_def_atom "[| Not (r is_atom); 1 < n |]
57 ==> r ^^^ n = r * r ^^^ (n + -1)"
58 realpow_addI_atom "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)"
61 realpow_minus_even "n is_even ==> (- r) ^^^ n = r ^^^ n"
62 realpow_minus_odd "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n"
66 real_pp_binom_times "(a + b)*(c + d) = a*c + a*d + b*c + b*d"
67 real_pm_binom_times "(a + b)*(c - d) = a*c - a*d + b*c - b*d"
68 real_mp_binom_times "(a - b)*(c + d) = a*c + a*d - b*c - b*d"
69 real_mm_binom_times "(a - b)*(c - d) = a*c - a*d - b*c + b*d"
70 real_plus_binom_pow3 "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
71 real_plus_binom_pow3_poly "[| a is_polyexp; b is_polyexp |] ==>
72 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3"
73 real_minus_binom_pow3 "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3"
74 real_minus_binom_pow3_p "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
76 (* real_plus_binom_pow "[| n is_const; 3 < n |] ==>
77 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
78 real_plus_binom_pow4 "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
80 real_plus_binom_pow4_poly "[| a is_polyexp; b is_polyexp |] ==>
81 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
83 real_plus_binom_pow5 "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
84 *(a^^^2 + 2*a*b + b^^^2)"
85 real_plus_binom_pow5_poly "[| a is_polyexp; b is_polyexp |] ==>
86 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
87 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)"
88 real_diff_plus "a - b = a + -b" (*17.3.03: do_NOT_use*)
89 real_diff_minus "a - b = a + -1 * b"
90 real_plus_binom_times "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2"
91 real_minus_binom_times "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2"
92 (*WN071229 changed for Schaerding -----vvv*)
93 (*real_plus_binom_pow2 "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
94 real_plus_binom_pow2 "(a + b)^^^2 = (a + b) * (a + b)"
95 (*WN071229 changed for Schaerding -----^^^*)
96 real_plus_binom_pow2_poly "[| a is_polyexp; b is_polyexp |] ==>
97 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"
98 real_minus_binom_pow2 "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2"
99 real_minus_binom_pow2_p "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"
100 real_plus_minus_binom1 "(a + b)*(a - b) = a^^^2 - b^^^2"
101 real_plus_minus_binom1_p "(a + b)*(a - b) = a^^^2 + -1*b^^^2"
102 real_plus_minus_binom1_p_p "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"
103 real_plus_minus_binom2 "(a - b)*(a + b) = a^^^2 - b^^^2"
104 real_plus_minus_binom2_p "(a - b)*(a + b) = a^^^2 + -1*b^^^2"
105 real_plus_minus_binom2_p_p "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"
106 real_plus_binom_times1 "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"
107 real_plus_binom_times2 "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"
109 real_num_collect "[| l is_const; m is_const |] ==>
110 l * n + m * n = (l + m) * n"
111 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
112 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
113 real_num_collect_assoc "[| l is_const; m is_const |] ==>
114 l * n + (m * n + k) = (l + m) * n + k"
115 real_num_collect_assoc_l "[| l is_const; m is_const |] ==>
116 l * n + (m * n + k) = (l + m)
118 real_num_collect_assoc_r "[| l is_const; m is_const |] ==>
119 (k + m * n) + l * n = k + (l + m) * n"
120 real_one_collect "m is_const ==> n + m * n = (1 + m) * n"
121 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
122 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
123 real_one_collect_assoc "m is_const ==> n + (m * n + k) = (1 + m)* n + k"
125 real_one_collect_assoc_l "m is_const ==> n + (m * n + k) = (1 + m) * n + k"
126 real_one_collect_assoc_r "m is_const ==> (k + n) + m * n = k + (1 + m) * n"
128 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
129 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
130 real_mult_2_assoc "z1 + (z1 + k) = 2 * z1 + k"
131 real_mult_2_assoc_l "z1 + (z1 + k) = 2 * z1 + k"
132 real_mult_2_assoc_r "(k + z1) + z1 = k + 2 * z1"
134 real_add_mult_distrib_poly "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w"
135 real_add_mult_distrib2_poly "w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
137 text {* remark on 'polynomials'
139 *** there are 5 kinds of expanded normalforms ***
141 [1] 'complete polynomial' (Komplettes Polynom), univariate
142 a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
143 not (a_n = 0), some a_i may be zero (DON'T disappear),
144 variables in monomials lexicographically ordered and complete,
145 x written as 1*x^1, ...
146 [2] 'polynomial' (Polynom), univariate and multivariate
147 a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
148 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
149 not (a_n = 0), some a_i may be zero (ie. monomials disappear),
150 exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
151 and variables in monomials are lexicographically ordered
152 examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
153 [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
154 [2]: "x + (-50) * x ^^^ 3"
155 [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
157 [3] 'expanded_term' (Ausmultiplizierter Term):
158 pull out unary minus to binary minus,
159 as frequently exercised in schools; other conditions for [2] hold however
160 examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
161 "4 * x ^^^ 2 - 9 * y ^^^ 2"
162 [4] 'polynomial_in' (Polynom in):
163 polynomial in 1 variable with arbitrary coefficients
164 examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
165 "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
166 [5] 'expanded_in' (Ausmultiplizierter Termin in):
167 analoguous to [3] with binary minus like [3]
168 examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
169 "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
173 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
174 fun is_polyrat_in t v =
175 let fun coeff_in c v = member op = (vars c) v;
176 fun finddivide (_ $ _ $ _ $ _) v = raise error("is_polyrat_in:")
177 (* at the moment there is no term like this, but ....*)
178 | finddivide (t as (Const ("HOL.divide",_) $ _ $ b)) v =
180 | finddivide (_ $ t1 $ t2) v =
181 (finddivide t1 v) orelse (finddivide t2 v)
182 | finddivide (_ $ t1) v = (finddivide t1 v)
183 | finddivide _ _ = false;
184 in finddivide t v end;
186 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
188 then SOME ((term2str p) ^ " = True",
189 Trueprop $ (mk_equality (p, HOLogic.true_const)))
190 else SOME ((term2str p) ^ " = True",
191 Trueprop $ (mk_equality (p, HOLogic.false_const)))
192 | eval_is_polyrat_in _ _ _ _ = ((*writeln"### no matches";*) NONE);
195 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
196 fun coeff_in c v = not (member op = (vars c) v);
197 (* FIXME.WN100826 shift this into test--------------
198 val v = (term_of o the o (parse thy)) "x";
199 val t = (term_of o the o (parse thy)) "1";
201 (*val it = true : bool*)
202 val t = (term_of o the o (parse thy)) "a*b+c";
204 (*val it = true : bool*)
205 val t = (term_of o the o (parse thy)) "a*x+c";
207 (*val it = false : bool*)
208 ----------------------------------------------------*)
209 (*. a 'monomial t in variable v' is a term t with
210 either (1) v NOT existent in t, or (2) v contained in t,
212 if (2) then v is a factor on the very right, ev. with exponent.*)
213 fun factor_right_deg (*case 2*)
214 (t as Const ("op *",_) $ t1 $
215 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
216 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
217 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
218 if (vv = v) then SOME (int_of_str' d) else NONE
219 | factor_right_deg (t as Const ("op *",_) $ t1 $ vv) v =
220 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
221 | factor_right_deg vv v =
222 if (vv = v) then SOME 1 else NONE;
223 fun mono_deg_in m v =
224 if coeff_in m v then (*case 1*) SOME 0
225 else factor_right_deg m v;
226 (* FIXME.WN100826 shift this into test-----------------------------
227 val v = (term_of o the o (parse thy)) "x";
228 val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";
231 val t = (term_of o the o (parse thy)) "x^^^7";
234 val t = (term_of o the o (parse thy)) "(a*b+c)*x";
237 val t = (term_of o the o (parse thy)) "(a*b+x)*x";
240 val t = (term_of o the o (parse thy)) "x";
243 val t = (term_of o the o (parse thy)) "(a*b+c)";
246 val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
249 ------------------------------------------------------------------*)
250 fun expand_deg_in t v =
251 let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
252 (case mono_deg_in t2 v of (* $ is left associative*)
253 SOME d' => edi d' d' t1
255 | edi ~1 ~1 (Const ("op -",_) $ t1 $ t2) =
256 (case mono_deg_in t2 v of
257 SOME d' => edi d' d' t1
259 | edi d dmax (Const ("op -",_) $ t1 $ t2) =
260 (case mono_deg_in t2 v of
261 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
262 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
263 then edi d' dmax t1 else NONE
265 | edi d dmax (Const ("op +",_) $ t1 $ t2) =
266 (case mono_deg_in t2 v of
267 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
268 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
269 then edi d' dmax t1 else NONE
271 | edi ~1 ~1 t = (case mono_deg_in t v of
274 | edi d dmax t = (*basecase last*)
275 (case mono_deg_in t v of
276 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
277 then SOME dmax else NONE
280 (* FIXME.WN100826 shift this into test-----------------------------
281 val v = (term_of o the o (parse thy)) "x";
282 val t = (term_of o the o (parse thy)) "a+b";
285 val t = (term_of o the o (parse thy)) "(a+b)*x";
288 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
291 val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
294 val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
296 -------------------------------------------------------------------*)
297 fun poly_deg_in t v =
298 let fun edi ~1 ~1 (Const ("op +",_) $ t1 $ t2) =
299 (case mono_deg_in t2 v of (* $ is left associative*)
300 SOME d' => edi d' d' t1
302 | edi d dmax (Const ("op +",_) $ t1 $ t2) =
303 (case mono_deg_in t2 v of
304 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
305 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
306 then edi d' dmax t1 else NONE
308 | edi ~1 ~1 t = (case mono_deg_in t v of
311 | edi d dmax t = (*basecase last*)
312 (case mono_deg_in t v of
313 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
314 then SOME dmax else NONE
319 fun is_expanded_in t v =
320 case expand_deg_in t v of SOME _ => true | NONE => false;
322 case poly_deg_in t v of SOME _ => true | NONE => false;
323 fun has_degree_in t v =
324 case expand_deg_in t v of SOME d => d | NONE => ~1;
326 (* FIXME.WN100826 shift this into test-----------------------------
327 val v = (term_of o the o (parse thy)) "x";
328 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
331 val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
334 val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
337 -------------------------------------------------------------------*)
339 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
340 fun eval_is_expanded_in _ _
341 (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
342 if is_expanded_in t v
343 then SOME ((term2str p) ^ " = True",
344 Trueprop $ (mk_equality (p, HOLogic.true_const)))
345 else SOME ((term2str p) ^ " = True",
346 Trueprop $ (mk_equality (p, HOLogic.false_const)))
347 | eval_is_expanded_in _ _ _ _ = NONE;
349 val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
350 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
351 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
353 (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
356 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
357 fun eval_is_poly_in _ _
358 (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
360 then SOME ((term2str p) ^ " = True",
361 Trueprop $ (mk_equality (p, HOLogic.true_const)))
362 else SOME ((term2str p) ^ " = True",
363 Trueprop $ (mk_equality (p, HOLogic.false_const)))
364 | eval_is_poly_in _ _ _ _ = NONE;
366 val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
367 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
368 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
370 (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
373 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
374 fun eval_has_degree_in _ _
375 (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
376 let val d = has_degree_in t v
377 val d' = term_of_num HOLogic.realT d
378 in SOME ((term2str p) ^ " = " ^ (string_of_int d),
379 Trueprop $ (mk_equality (p, d')))
381 | eval_has_degree_in _ _ _ _ = NONE;
383 > val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
384 > val SOME (id, t') = eval_has_degree_in 0 0 t 0;
385 val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
387 val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
390 (*.for evaluation of conditions in rewrite rules.*)
392 append_rls "Poly_erls" Atools_erls
393 [ Calc ("op =",eval_equal "#equal_"),
394 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
395 Calc ("op +",eval_binop "#add_"),
396 Calc ("op -",eval_binop "#sub_"),
397 Calc ("op *",eval_binop "#mult_"),
398 Calc ("Atools.pow" ,eval_binop "#power_")
402 append_rls "poly_crls" Atools_crls
403 [ Calc ("op =",eval_equal "#equal_"),
404 Thm ("real_unari_minus",num_str @{thm real_unari_minus}),
405 Calc ("op +",eval_binop "#add_"),
406 Calc ("op -",eval_binop "#sub_"),
407 Calc ("op *",eval_binop "#mult_"),
408 Calc ("Atools.pow" ,eval_binop "#power_")
411 local (*. for make_polynomial .*)
413 open Term; (* for type order = EQUAL | LESS | GREATER *)
415 fun pr_ord EQUAL = "EQUAL"
416 | pr_ord LESS = "LESS"
417 | pr_ord GREATER = "GREATER";
419 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
421 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
422 | _ => (((a, 0), T), 0))
423 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
424 | dest_hd' (Var v) = (v, 2)
425 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
426 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
428 fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
429 (case int_of_str (order) of
432 | get_order_pow _ = 0;
434 fun size_of_term' (Const(str,_) $ t) =
435 if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
436 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
437 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
438 | size_of_term' _ = 1;
440 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
441 (case term_ord' pr thy (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
442 | term_ord' pr thy (t, u) =
445 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
446 val _=writeln("t= f@ts= \""^
447 ((Syntax.string_of_term (thy2ctxt thy)) f)^"\" @ \"["^
448 (commas(map(Syntax.string_of_term (thy2ctxt thy))ts))^"]\"");
449 val _=writeln("u= g@us= \""^
450 ((Syntax.string_of_term (thy2ctxt thy)) g)^"\" @ \"["^
451 (commas(map(Syntax.string_of_term (thy2ctxt thy))us))^"]\"");
452 val _=writeln("size_of_term(t,u)= ("^
453 (string_of_int(size_of_term' t))^", "^
454 (string_of_int(size_of_term' u))^")");
455 val _=writeln("hd_ord(f,g) = "^((pr_ord o hd_ord)(f,g)));
456 val _=writeln("terms_ord(ts,us) = "^
457 ((pr_ord o terms_ord str false)(ts,us)));
458 val _=writeln("-------");
461 case int_ord (size_of_term' t, size_of_term' u) of
463 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
464 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
468 and hd_ord (f, g) = (* ~ term.ML *)
469 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd' f, dest_hd' g)
470 and terms_ord str pr (ts, us) =
471 list_ord (term_ord' pr (assoc_thy "Isac.thy"))(ts, us);
474 fun ord_make_polynomial (pr:bool) thy (_:subst) tu =
475 (term_ord' pr thy(***) tu = LESS );
480 rew_ord' := overwritel (!rew_ord',
481 [("termlessI", termlessI),
482 ("ord_make_polynomial", ord_make_polynomial false thy)
487 Rls{id = "expand", preconds = [],
488 rew_ord = ("dummy_ord", dummy_ord),
489 erls = e_rls,srls = Erls,
492 rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
493 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
494 Thm ("left_distrib2",num_str @{thm left_distrib2})
495 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
496 ], scr = EmptyScr}:rls;
498 (*----------------- Begin: rulesets for make_polynomial_ -----------------
499 'rlsIDs' redefined by MG as 'rlsIDs_'
503 Rls{id = "discard_minus_", preconds = [],
504 rew_ord = ("dummy_ord", dummy_ord),
505 erls = e_rls,srls = Erls,
508 rules = [Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
509 (*"a - b = a + -1 * b"*)
510 Thm ("sym_real_mult_minus1",
511 num_str (@{thm sym_real_mult_minus1} RS @{thm sym}))
513 ], scr = EmptyScr}:rls;
515 Rls{id = "expand_poly_", preconds = [],
516 rew_ord = ("dummy_ord", dummy_ord),
517 erls = e_rls,srls = Erls,
520 rules = [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),
521 (*"(a + b)^^^4 = ... "*)
522 Thm ("real_plus_binom_pow5",num_str @{thm real_plus_binom_pow5}),
523 (*"(a + b)^^^5 = ... "*)
524 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
525 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
526 (*WN071229 changed/removed for Schaerding -----vvv*)
527 (*Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),*)
528 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
529 Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
530 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
531 (*Thm ("real_plus_minus_binom1_p_p",
532 num_str @{thm real_plus_minus_binom1_p_p}),*)
533 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
534 (*Thm ("real_plus_minus_binom2_p_p",
535 num_str @{thm real_plus_minus_binom2_p_p}),*)
536 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
537 (*WN071229 changed/removed for Schaerding -----^^^*)
539 Thm ("left_distrib" ,num_str @{thm left_distrib}),
540 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
541 Thm ("left_distrib2",num_str @{thm left_distrib}2),
542 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
544 Thm ("realpow_multI", num_str @{thm realpow_multI}),
545 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
546 Thm ("realpow_pow",num_str @{thm realpow_pow})
547 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
548 ], scr = EmptyScr}:rls;
550 (*.the expression contains + - * ^ only ?
551 this is weaker than 'is_polynomial' !.*)
552 fun is_polyexp (Free _) = true
553 | is_polyexp (Const ("op +",_) $ Free _ $ Free _) = true
554 | is_polyexp (Const ("op -",_) $ Free _ $ Free _) = true
555 | is_polyexp (Const ("op *",_) $ Free _ $ Free _) = true
556 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
557 | is_polyexp (Const ("op +",_) $ t1 $ t2) =
558 ((is_polyexp t1) andalso (is_polyexp t2))
559 | is_polyexp (Const ("op -",_) $ t1 $ t2) =
560 ((is_polyexp t1) andalso (is_polyexp t2))
561 | is_polyexp (Const ("op *",_) $ t1 $ t2) =
562 ((is_polyexp t1) andalso (is_polyexp t2))
563 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
564 ((is_polyexp t1) andalso (is_polyexp t2))
565 | is_polyexp _ = false;
567 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
568 fun eval_is_polyexp (thmid:string) _
569 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
571 then SOME (mk_thmid thmid ""
572 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
573 Trueprop $ (mk_equality (t, HOLogic.true_const)))
574 else SOME (mk_thmid thmid ""
575 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
576 Trueprop $ (mk_equality (t, HOLogic.false_const)))
577 | eval_is_polyexp _ _ _ _ = NONE;
579 val expand_poly_rat_ =
580 Rls{id = "expand_poly_rat_", preconds = [],
581 rew_ord = ("dummy_ord", dummy_ord),
582 erls = append_rls "e_rls-is_polyexp" e_rls
583 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")
589 [Thm ("real_plus_binom_pow4_poly", num_str @{thm real_plus_binom_pow4_poly}),
590 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
591 Thm ("real_plus_binom_pow5_poly", num_str @{thm real_plus_binom_pow5_poly}),
592 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
593 Thm ("real_plus_binom_pow2_poly",num_str @{thm real_plus_binom_pow2_poly}),
594 (*"[| a is_polyexp; b is_polyexp |] ==>
595 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
596 Thm ("real_plus_binom_pow3_poly",num_str @{thm real_plus_binom_pow3_poly}),
597 (*"[| a is_polyexp; b is_polyexp |] ==>
598 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
599 Thm ("real_plus_minus_binom1_p_p",num_str @{thm real_plus_minus_binom1_p_p}),
600 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
601 Thm ("real_plus_minus_binom2_p_p",num_str @{thm real_plus_minus_binom2_p_p}),
602 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
604 Thm ("left_distrib_poly" ,num_str @{thm left_distrib_poly}),
605 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
606 Thm("left_distrib2_poly",num_str @{thm left_distrib2_poly}),
607 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
609 Thm ("realpow_multI_poly", num_str @{thm realpow_multI_poly}),
610 (*"[| r is_polyexp; s is_polyexp |] ==>
611 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
612 Thm ("realpow_pow",num_str @{thm realpow_pow})
613 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
614 ], scr = EmptyScr}:rls;
616 val simplify_power_ =
617 Rls{id = "simplify_power_", preconds = [],
618 rew_ord = ("dummy_ord", dummy_ord),
619 erls = e_rls, srls = Erls,
622 rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
623 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
624 Thm ("sym_realpow_twoI",
625 num_str (@{thm realpow_twoI} RS @{thm sym})),
626 (*"r * r = r ^^^ 2"*)
627 Thm ("realpow_twoI_assoc_l",num_str @{thm realpow_twoI_assoc_l}),
628 (*"r * (r * s) = r ^^^ 2 * s"*)
630 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
631 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
632 Thm ("realpow_plus_1_assoc_l",
633 num_str @{thm realpow_plus_1_assoc_l}),
634 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
635 (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
636 Thm ("realpow_plus_1_assoc_l2",
637 num_str @{thm realpow_plus_1_assoc_l2}),
638 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
640 Thm ("sym_realpow_addI",
641 num_str (@{thm realpow_addI} RS @{thm sym})),
642 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
643 Thm ("realpow_addI_assoc_l",num_str @{thm realpow_addI_assoc_l}),
644 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
646 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
647 "r * r = r ^^^ 2" wenn r=a^^^b*)
648 Thm ("realpow_pow",num_str @{thm realpow_pow})
649 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
650 ], scr = EmptyScr}:rls;
652 val calc_add_mult_pow_ =
653 Rls{id = "calc_add_mult_pow_", preconds = [],
654 rew_ord = ("dummy_ord", dummy_ord),
655 erls = Atools_erls(*erls3.4.03*),srls = Erls,
656 calc = [("PLUS" , ("op +", eval_binop "#add_")),
657 ("TIMES" , ("op *", eval_binop "#mult_")),
658 ("POWER", ("Atools.pow", eval_binop "#power_"))
661 rules = [Calc ("op +", eval_binop "#add_"),
662 Calc ("op *", eval_binop "#mult_"),
663 Calc ("Atools.pow", eval_binop "#power_")
664 ], scr = EmptyScr}:rls;
666 val reduce_012_mult_ =
667 Rls{id = "reduce_012_mult_", preconds = [],
668 rew_ord = ("dummy_ord", dummy_ord),
669 erls = e_rls,srls = Erls,
672 rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
673 Thm ("mult_1_right",num_str @{thm mult_1_right}),
674 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
675 Thm ("realpow_zeroI",num_str @{thm realpow_zeroI}),
676 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
677 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
679 Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI)
681 ], scr = EmptyScr}:rls;
683 val collect_numerals_ =
684 Rls{id = "collect_numerals_", preconds = [],
685 rew_ord = ("dummy_ord", dummy_ord),
686 erls = Atools_erls, srls = Erls,
687 calc = [("PLUS" , ("op +", eval_binop "#add_"))
690 [Thm ("real_num_collect",num_str @{thm real_num_collect}),
691 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
692 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}),
693 (*"[| l is_const; m is_const |] ==> \
694 \(k + m * n) + l * n = k + (l + m)*n"*)
695 Thm ("real_one_collect",num_str @{thm real_one_collect}),
696 (*"m is_const ==> n + m * n = (1 + m) * n"*)
697 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}),
698 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
700 Calc ("op +", eval_binop "#add_"),
702 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
703 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
704 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}),
705 (*"(k + z1) + z1 = k + 2 * z1"*)
706 Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym}))
707 (*"z1 + z1 = 2 * z1"*)
708 ], scr = EmptyScr}:rls;
711 Rls{id = "reduce_012_", preconds = [],
712 rew_ord = ("dummy_ord", dummy_ord),
713 erls = e_rls,srls = Erls,
716 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
718 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
720 Thm ("mult_zero_left_right",num_str @{thm mult_zero_left}_right),
722 Thm ("add_0_left",num_str @{thm add_0_left}),
724 Thm ("add_0_right",num_str @{thm add_0_right}),
725 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
727 (*Thm ("realpow_oneI",num_str @{thm realpow_oneI})*)
729 Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)
731 ], scr = EmptyScr}:rls;
733 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
734 val discard_parentheses_ =
735 append_rls "discard_parentheses_" e_rls
736 [Thm ("sym_real_mult_assoc",
737 num_str (@{thm real_mult_assoc} RS @{thm sym}))
738 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
739 (*Thm ("sym_real_add_assoc",
740 num_str (@{thm real_add_assoc} RS @{thm sym}))*)
741 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
744 (*----------------- End: rulesets for make_polynomial_ -----------------*)
746 (*MG.0401 ev. for use in rls with ordered rewriting ?
747 val collect_numerals_left =
748 Rls{id = "collect_numerals", preconds = [],
749 rew_ord = ("dummy_ord", dummy_ord),
750 erls = Atools_erls(*erls3.4.03*),srls = Erls,
751 calc = [("PLUS" , ("op +", eval_binop "#add_")),
752 ("TIMES" , ("op *", eval_binop "#mult_")),
753 ("POWER", ("Atools.pow", eval_binop "#power_"))
756 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}),
757 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
758 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
759 (*"[| l is_const; m is_const |] ==>
760 l * n + (m * n + k) = (l + m) * n + k"*)
761 Thm ("real_one_collect",num_str @{thm real_one_collect}),
762 (*"m is_const ==> n + m * n = (1 + m) * n"*)
763 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
764 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
766 Calc ("op +", eval_binop "#add_"),
768 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
769 Thm ("sym_real_mult_2",
770 num_str (@{thm real_mult_2} RS @{thm sym})),
771 (*"z1 + z1 = 2 * z1"*)
772 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
773 (*"z1 + (z1 + k) = 2 * z1 + k"*)
774 ], scr = EmptyScr}:rls;*)
777 Rls{id = "expand_poly", preconds = [],
778 rew_ord = ("dummy_ord", dummy_ord),
779 erls = e_rls,srls = Erls,
782 rules = [Thm ("left_distrib" ,num_str @{thm left_distrib}),
783 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
784 Thm ("left_distrib2",num_str @{thm left_distrib}2),
785 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
786 (*Thm ("left_distrib1",num_str @{thm left_distrib}1),
787 ....... 18.3.03 undefined???*)
789 Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
790 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
791 Thm ("real_minus_binom_pow2_p",num_str @{thm real_minus_binom_pow2_p}),
792 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
793 Thm ("real_plus_minus_binom1_p",
794 num_str @{thm real_plus_minus_binom1_p}),
795 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
796 Thm ("real_plus_minus_binom2_p",
797 num_str @{thm real_plus_minus_binom2_p}),
798 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
800 Thm ("minus_minus",num_str @{thm minus_minus}),
802 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
803 (*"a - b = a + -1 * b"*)
804 Thm ("sym_real_mult_minus1",
805 num_str (@{thm real_mult_minus1} RS @{thm sym}))
808 (*Thm ("real_minus_add_distrib",
809 num_str @{thm real_minus_add_distrib}),*)
810 (*"- (?x + ?y) = - ?x + - ?y"*)
811 (*Thm ("real_diff_plus",num_str @{thm real_diff_plus})*)
813 ], scr = EmptyScr}:rls;
816 Rls{id = "simplify_power", preconds = [],
817 rew_ord = ("dummy_ord", dummy_ord),
818 erls = e_rls, srls = Erls,
821 rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),
822 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
824 Thm ("sym_realpow_twoI",
825 num_str( @{thm realpow_twoI} RS @{thm sym})),
826 (*"r1 * r1 = r1 ^^^ 2"*)
827 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
828 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
829 Thm ("realpow_pow",num_str @{thm realpow_pow}),
830 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
831 Thm ("sym_realpow_addI",
832 num_str (@{thm realpow_addI} RS @{thm sym})),
833 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
834 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
836 Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
838 ], scr = EmptyScr}:rls;
839 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
840 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
842 Rls{id = "order_add_mult", preconds = [],
843 rew_ord = ("ord_make_polynomial",ord_make_polynomial false (theory "Poly")),
844 erls = e_rls,srls = Erls,
847 rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
849 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
850 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
851 Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}),
852 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
853 Thm ("add_commute",num_str @{thm add_commute}),
855 Thm ("add_left_commute",num_str @{thm add_left_commute}),
856 (*x + (y + z) = y + (x + z)*)
857 Thm ("add_assoc",num_str @{thm add_assoc})
858 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
859 ], scr = EmptyScr}:rls;
860 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
861 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
863 Rls{id = "order_mult", preconds = [],
864 rew_ord = ("ord_make_polynomial",ord_make_polynomial false (theory "Poly")),
865 erls = e_rls,srls = Erls,
868 rules = [Thm ("real_mult_commute",num_str @{thm real_mult_commute}),
870 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
871 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
872 Thm ("real_mult_assoc",num_str @{thm real_mult_assoc})
873 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
874 ], scr = EmptyScr}:rls;
875 val collect_numerals =
876 Rls{id = "collect_numerals", preconds = [],
877 rew_ord = ("dummy_ord", dummy_ord),
878 erls = Atools_erls(*erls3.4.03*),srls = Erls,
879 calc = [("PLUS" , ("op +", eval_binop "#add_")),
880 ("TIMES" , ("op *", eval_binop "#mult_")),
881 ("POWER", ("Atools.pow", eval_binop "#power_"))
884 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}),
885 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
886 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
887 (*"[| l is_const; m is_const |] ==>
888 l * n + (m * n + k) = (l + m) * n + k"*)
889 Thm ("real_one_collect",num_str @{thm real_one_collect}),
890 (*"m is_const ==> n + m * n = (1 + m) * n"*)
891 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
892 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
893 Calc ("op +", eval_binop "#add_"),
894 Calc ("op *", eval_binop "#mult_"),
895 Calc ("Atools.pow", eval_binop "#power_")
896 ], scr = EmptyScr}:rls;
898 Rls{id = "reduce_012", preconds = [],
899 rew_ord = ("dummy_ord", dummy_ord),
900 erls = e_rls,srls = Erls,
903 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
905 (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),14.3.03*)
907 Thm ("minus_mult_left",
908 num_str (@{thm real_mult_minus_eq1} RS @{thm sym})),
909 (*- (?x * ?y) = "- ?x * ?y"*)
910 (*Thm ("real_minus_mult_cancel",
911 num_str @{thm real_minus_mult_cancel}),
912 (*"- ?x * - ?y = ?x * ?y"*)---*)
913 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
915 Thm ("add_0_left",num_str @{thm add_0_left}),
917 Thm ("right_minus",num_str @{thm right_minus}),
919 Thm ("sym_real_mult_2",
920 num_str (@{thm real_mult_2} RS @{thm sym})),
921 (*"z1 + z1 = 2 * z1"*)
922 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
923 (*"z1 + (z1 + k) = 2 * z1 + k"*)
924 ], scr = EmptyScr}:rls;
925 (*ein Hilfs-'ruleset' (benutzt das leere 'ruleset')*)
926 val discard_parentheses =
927 append_rls "discard_parentheses" e_rls
928 [Thm ("sym_real_mult_assoc",
929 num_str (@{thm real_mult_assoc} RS @{thm sym})),
930 Thm ("sym_real_add_assoc",
931 num_str (@{thm real_add_assoc} RS @{thm sym}))];
933 val scr_make_polynomial =
934 "Script Expand_binoms t_ = " ^
936 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
938 " (Try (Repeat (Rewrite real_add_mult_distrib False))) @@ " ^
939 " (Try (Repeat (Rewrite real_add_mult_distrib2 False))) @@ " ^
940 " (Try (Repeat (Rewrite real_diff_mult_distrib False))) @@ " ^
941 " (Try (Repeat (Rewrite real_diff_mult_distrib2 False))) @@ " ^
943 " (Try (Repeat (Rewrite real_mult_1 False))) @@ " ^
944 " (Try (Repeat (Rewrite real_mult_0 False))) @@ " ^
945 " (Try (Repeat (Rewrite real_add_zero_left False))) @@ " ^
947 " (Try (Repeat (Rewrite real_mult_commute False))) @@ " ^
948 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
949 " (Try (Repeat (Rewrite real_mult_assoc False))) @@ " ^
950 " (Try (Repeat (Rewrite real_add_commute False))) @@ " ^
951 " (Try (Repeat (Rewrite real_add_left_commute False))) @@ " ^
952 " (Try (Repeat (Rewrite real_add_assoc False))) @@ " ^
954 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
955 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
956 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
957 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
959 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
960 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
962 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
963 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
965 " (Try (Repeat (Calculate plus ))) @@ " ^
966 " (Try (Repeat (Calculate times ))) @@ " ^
967 " (Try (Repeat (Calculate power_)))) " ^
970 (*version used by MG.02/03, overwritten by version AG in 04 below
971 val make_polynomial = prep_rls(
972 Seq{id = "make_polynomial", preconds = []:term list,
973 rew_ord = ("dummy_ord", dummy_ord),
974 erls = Atools_erls, srls = Erls,
975 calc = [],(*asm_thm = [],*)
976 rules = [Rls_ expand_poly,
978 Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
979 Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
981 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),(*in --^*)
982 Rls_ discard_parentheses
987 val scr_expand_binoms =
988 "Script Expand_binoms t_ =" ^
990 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
991 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
992 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
993 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
994 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
995 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
997 " (Try (Repeat (Rewrite real_mult_1 False))) @@ " ^
998 " (Try (Repeat (Rewrite real_mult_0 False))) @@ " ^
999 " (Try (Repeat (Rewrite real_add_zero_left False))) @@ " ^
1001 " (Try (Repeat (Calculate plus ))) @@ " ^
1002 " (Try (Repeat (Calculate times ))) @@ " ^
1003 " (Try (Repeat (Calculate power_))) @@ " ^
1005 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
1006 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
1007 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
1008 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
1010 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
1011 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
1013 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1014 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1016 " (Try (Repeat (Calculate plus ))) @@ " ^
1017 " (Try (Repeat (Calculate times ))) @@ " ^
1018 " (Try (Repeat (Calculate power_)))) " ^
1022 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1023 erls = Atools_erls, srls = Erls,
1024 calc = [("PLUS" , ("op +", eval_binop "#add_")),
1025 ("TIMES" , ("op *", eval_binop "#mult_")),
1026 ("POWER", ("Atools.pow", eval_binop "#power_"))
1029 rules = [Thm ("real_plus_binom_pow2" ,num_str @{thm real_plus_binom_pow2}),
1030 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1031 Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1032 (*"(a + b)*(a + b) = ...*)
1033 Thm ("real_minus_binom_pow2" ,num_str @{thm real_minus_binom_pow2}),
1034 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1035 Thm ("real_minus_binom_times",num_str @{thm real_minus_binom_times}),
1036 (*"(a - b)*(a - b) = ...*)
1037 Thm ("real_plus_minus_binom1",num_str @{thm real_plus_minus_binom1}),
1038 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1039 Thm ("real_plus_minus_binom2",num_str @{thm real_plus_minus_binom2}),
1040 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1042 Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
1043 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1044 Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
1045 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1046 Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
1047 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1048 Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
1049 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1050 Thm ("realpow_multI",num_str @{thm realpow_multI}),
1051 (*(a*b)^^^n = a^^^n * b^^^n*)
1052 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
1053 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1054 Thm ("real_minus_binom_pow3",num_str @{thm real_minus_binom_pow3}),
1055 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1058 (* Thm ("left_distrib" ,num_str @{thm left_distrib}),
1059 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1060 Thm ("left_distrib2",num_str @{thm left_distrib2}),
1061 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1062 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1063 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1064 Thm ("left_diff_distrib2",num_str @{thm left_diff_distrib2}),
1065 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1068 Thm ("mult_1_left",num_str @{thm mult_1_left}), (*"1 * z = z"*)
1069 Thm ("mult_zero_left",num_str @{thm mult_zero_left}), (*"0 * z = 0"*)
1070 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
1072 Calc ("op +", eval_binop "#add_"),
1073 Calc ("op *", eval_binop "#mult_"),
1074 Calc ("Atools.pow", eval_binop "#power_"),
1076 Thm ("real_mult_commute",num_str @{thm real_mult_commute}), (*AC-rewriting*)
1077 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}), (**)
1078 Thm ("real_mult_assoc",num_str @{thm real_mult_assoc}), (**)
1079 Thm ("add_commute",num_str @{thm add_commute}), (**)
1080 Thm ("add_left_commute",num_str @{thm add_left_commute}), (**)
1081 Thm ("add_assoc",num_str @{thm add_assoc}), (**)
1084 Thm ("sym_realpow_twoI",
1085 num_str (@{thm realpow_twoI} RS @{thm sym})),
1086 (*"r1 * r1 = r1 ^^^ 2"*)
1087 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1088 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1089 (*Thm ("sym_real_mult_2",num_str @{(real_mult_2 RS sym})),
1090 (*"z1 + z1 = 2 * z1"*)*)
1091 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1092 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1094 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1095 (*"[| l is_const; m is_const |] ==> l * n + m * n = (l + m) * n"*)
1096 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1097 (*"[| l is_const; m is_const |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1098 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1099 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1100 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1101 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1103 Calc ("op +", eval_binop "#add_"),
1104 Calc ("op *", eval_binop "#mult_"),
1105 Calc ("Atools.pow", eval_binop "#power_")
1107 scr = Script ((term_of o the o (parse thy)) scr_expand_binoms)
1111 "******* Poly.ML end ******* ...RL";
1114 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
1116 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
1117 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
1118 (* Polynom --> List von Monomen *)
1119 fun poly2list (Const ("op +",_) $ t1 $ t2) =
1120 (poly2list t1) @ (poly2list t2)
1121 | poly2list t = [t];
1123 (* Monom --> Liste von Variablen *)
1124 fun monom2list (Const ("op *",_) $ t1 $ t2) =
1125 (monom2list t1) @ (monom2list t2)
1126 | monom2list t = [t];
1128 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
1129 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
1130 | get_basStr (Free (str, _)) = str
1131 | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
1133 raise error("get_basStr: called with t= "^(term2str t));*)
1135 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
1136 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
1137 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1138 | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
1139 | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
1141 raise error("get_potStr: called with t= "^(term2str t));*)
1143 (* Umgekehrte string_ord *)
1144 val string_ord_rev = rev_order o string_ord;
1146 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
1147 innerhalb eines Monomes:
1148 - zuerst lexikographisch nach Variablenname
1149 - wenn gleich: nach steigender Potenz *)
1150 fun var_ord (a,b: term) = prod_ord string_ord string_ord
1151 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1153 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
1154 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
1155 - zuerst lexikographisch nach Variablenname
1156 - wenn gleich: nach sinkender Potenz*)
1157 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
1158 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1161 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
1162 val sort_varList = sort var_ord;
1164 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
1165 Argumente in eine Liste *)
1166 fun args u : term list =
1167 let fun stripc (f$t, ts) = stripc (f, t::ts)
1168 | stripc (t as Free _, ts) = (t::ts)
1169 | stripc (_, ts) = ts
1170 in stripc (u, []) end;
1172 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
1173 (keine Variablen) enthaelt *)
1174 fun filter_num [] = true
1175 | filter_num [Free x] = if (is_num (Free x)) then true
1177 | filter_num ((Free _)::_) = false
1179 (filter_num o (filter_out is_num) o flat o (map args)) ts;
1181 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
1182 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
1183 fun is_nums t = filter_num [t];
1185 (* Berechnet den Gesamtgrad eines Monoms *)
1187 fun counter (n, []) = n
1188 | counter (n, x :: xs) =
1193 (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
1194 if (is_nums (Free (str_h, T))) then
1195 counter (n + (the (int_of_str str_h)), xs)
1196 else counter (n + 1000, xs) (*FIXME.MG?!*)
1197 | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
1198 counter (n + 1000, xs) (*FIXME.MG?!*)
1199 | (Free (str, _)) => counter (n + 1, xs)
1200 (*| _ => raise error("monom_degree: called with factor: "^(term2str x)))*)
1201 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
1203 fun monom_degree l = counter (0, l)
1206 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
1207 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
1208 werden jedoch dabei ignoriert (uebersprungen) *)
1209 fun dict_cond_ord _ _ ([], []) = EQUAL
1210 | dict_cond_ord _ _ ([], _ :: _) = LESS
1211 | dict_cond_ord _ _ (_ :: _, []) = GREATER
1212 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
1213 (case (cond x, cond y) of
1214 (false, false) => (case elem_ord (x, y) of
1215 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
1217 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
1218 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
1219 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
1221 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
1222 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
1223 dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
1224 fun degree_ord (xs, ys) =
1225 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
1226 ((monom_degree xs, xs), (monom_degree ys, ys));
1228 fun hd_str str = substring (str, 0, 1);
1229 fun tl_str str = substring (str, 1, (size str) - 1);
1231 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
1232 fun get_koeff_of_mon [] = raise error("get_koeff_of_mon: called with l = []")
1233 | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
1236 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
1237 fun koeff2ordStr (SOME x) = (case x of
1239 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
1241 | _ => "aaa") (* "num.Ausdruck" --> gross *)
1242 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
1244 (* Order zum Vergleich von Koeffizienten (strings):
1245 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
1246 fun compare_koeff_ord (xs, ys) =
1247 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
1248 (koeff2ordStr o get_koeff_of_mon) ys);
1250 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
1251 fun koeff_degree_ord (xs, ys) =
1252 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
1254 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
1255 Gesamtgradordnung *)
1256 val sort_monList = sort koeff_degree_ord;
1258 (* Alternativ zu degree_ord koennte auch die viel einfachere und
1259 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
1260 fuer unsere Zwecke geeignet!
1262 fun simple_ord (al,bl: term list) = dict_ord string_ord
1263 (map get_basStr al, map get_basStr bl);
1265 val sort_monList = sort simple_ord; *)
1267 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1268 (mit gewuenschtem Typen T) *)
1269 fun plus T = Const ("op +", [T,T] ---> T);
1270 fun mult T = Const ("op *", [T,T] ---> T);
1271 fun binop op_ t1 t2 = op_ $ t1 $ t2;
1272 fun create_prod T (a,b) = binop (mult T) a b;
1273 fun create_sum T (a,b) = binop (plus T) a b;
1275 (* löscht letztes Element einer Liste *)
1276 fun drop_last l = take ((length l)-1,l);
1278 (* Liste von Variablen --> Monom *)
1279 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
1281 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
1282 gleiche Monome zusammengefasst werden können (collect_numerals)!
1283 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
1285 (* Liste von Monomen --> Polynom *)
1286 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
1288 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
1289 bessere Darstellung, da keine Klammern sichtbar!
1290 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
1292 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
1293 fun sort_variables t =
1295 val ll = map monom2list (poly2list t);
1296 val lls = map sort_varList ll;
1298 val ls = map (create_monom T) lls;
1299 in create_polynom T ls end;
1301 (* sorts the monoms of an expanded and variable-sorted polynomial
1305 val ll = map monom2list (poly2list t);
1306 val lls = sort_monList ll;
1308 val ls = map (create_monom T) lls;
1309 in create_polynom T ls end;
1311 (* auch Klammerung muss übereinstimmen;
1312 sort_variables klammert Produkte rechtslastig*)
1313 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
1315 fun eval_is_multUnordered (thmid:string) _
1316 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
1317 if is_multUnordered arg
1318 then SOME (mk_thmid thmid ""
1319 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1320 Trueprop $ (mk_equality (t, HOLogic.true_const)))
1321 else SOME (mk_thmid thmid ""
1322 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1323 Trueprop $ (mk_equality (t, HOLogic.false_const)))
1324 | eval_is_multUnordered _ _ _ _ = NONE;
1327 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1328 []:(rule * (term * term list)) list;
1329 fun init_state (_:term) = e_rrlsstate;
1330 fun locate_rule (_:rule list list) (_:term) (_:rule) =
1331 ([]:(rule * (term * term list)) list);
1332 fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
1333 fun normal_form t = SOME (sort_variables t,[]:term list);
1336 Rrls {id = "order_mult_",
1338 [([(term_of o the o (parse thy)) "p is_multUnordered"],
1339 (term_of o the o (parse thy)) "?p" )],
1340 rew_ord = ("dummy_ord", dummy_ord),
1341 erls = append_rls "e_rls-is_multUnordered" e_rls(*MG: poly_erls*)
1342 [Calc ("Poly.is'_multUnordered", eval_is_multUnordered "")
1344 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1345 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1346 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
1347 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1349 scr=Rfuns {init_state = init_state,
1350 normal_form = normal_form,
1351 locate_rule = locate_rule,
1352 next_rule = next_rule,
1353 attach_form = attach_form}};
1355 val order_mult_rls_ =
1356 Rls{id = "order_mult_rls_", preconds = [],
1357 rew_ord = ("dummy_ord", dummy_ord),
1358 erls = e_rls,srls = Erls,
1361 rules = [Rls_ order_mult_
1362 ], scr = EmptyScr}:rls;
1364 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
1367 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
1368 fun eval_is_addUnordered (thmid:string) _
1369 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
1370 if is_addUnordered arg
1371 then SOME (mk_thmid thmid ""
1372 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1373 Trueprop $ (mk_equality (t, HOLogic.true_const)))
1374 else SOME (mk_thmid thmid ""
1375 ((Syntax.string_of_term (thy2ctxt thy)) arg) "",
1376 Trueprop $ (mk_equality (t, HOLogic.false_const)))
1377 | eval_is_addUnordered _ _ _ _ = NONE;
1379 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1380 []:(rule * (term * term list)) list;
1381 fun init_state (_:term) = e_rrlsstate;
1382 fun locate_rule (_:rule list list) (_:term) (_:rule) =
1383 ([]:(rule * (term * term list)) list);
1384 fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
1385 fun normal_form t = SOME (sort_monoms t,[]:term list);
1388 Rrls {id = "order_add_",
1389 prepat = (*WN.18.6.03 Preconditions und Pattern,
1390 die beide passen muessen, damit das Rrls angewandt wird*)
1391 [([(term_of o the o (parse thy)) "p is_addUnordered"],
1392 (term_of o the o (parse thy)) "?p"
1393 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1394 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1395 rew_ord = ("dummy_ord", dummy_ord),
1396 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
1397 [Calc ("Poly.is'_addUnordered", eval_is_addUnordered "")
1398 (*WN.18.6.03 definiert in (theory "Poly"),
1399 evaluiert prepat*)],
1400 calc = [("PLUS" ,("op +" ,eval_binop "#add_")),
1401 ("TIMES" ,("op *" ,eval_binop "#mult_")),
1402 ("DIVIDE" ,("HOL.divide" ,eval_cancel "#divide_")),
1403 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1405 scr=Rfuns {init_state = init_state,
1406 normal_form = normal_form,
1407 locate_rule = locate_rule,
1408 next_rule = next_rule,
1409 attach_form = attach_form}};
1411 val order_add_rls_ =
1412 Rls{id = "order_add_rls_", preconds = [],
1413 rew_ord = ("dummy_ord", dummy_ord),
1414 erls = e_rls,srls = Erls,
1417 rules = [Rls_ order_add_
1418 ], scr = EmptyScr}:rls;
1420 (*. see MG-DA.p.52ff .*)
1421 val make_polynomial(*MG.03, overwrites version from above,
1422 previously 'make_polynomial_'*) =
1423 Seq {id = "make_polynomial", preconds = []:term list,
1424 rew_ord = ("dummy_ord", dummy_ord),
1425 erls = Atools_erls, srls = Erls,calc = [],
1426 rules = [Rls_ discard_minus_,
1428 Calc ("op *", eval_binop "#mult_"),
1429 Rls_ order_mult_rls_,
1430 Rls_ simplify_power_,
1431 Rls_ calc_add_mult_pow_,
1432 Rls_ reduce_012_mult_,
1433 Rls_ order_add_rls_,
1434 Rls_ collect_numerals_,
1436 Rls_ discard_parentheses_
1440 val norm_Poly(*=make_polynomial*) =
1441 Seq {id = "norm_Poly", preconds = []:term list,
1442 rew_ord = ("dummy_ord", dummy_ord),
1443 erls = Atools_erls, srls = Erls, calc = [],
1444 rules = [Rls_ discard_minus_,
1446 Calc ("op *", eval_binop "#mult_"),
1447 Rls_ order_mult_rls_,
1448 Rls_ simplify_power_,
1449 Rls_ calc_add_mult_pow_,
1450 Rls_ reduce_012_mult_,
1451 Rls_ order_add_rls_,
1452 Rls_ collect_numerals_,
1454 Rls_ discard_parentheses_
1459 (* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses_
1460 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1461 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1462 val make_rat_poly_with_parentheses =
1463 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1464 rew_ord = ("dummy_ord", dummy_ord),
1465 erls = Atools_erls, srls = Erls, calc = [],
1466 rules = [Rls_ discard_minus_,
1467 Rls_ expand_poly_rat_,(*ignors rationals*)
1468 Calc ("op *", eval_binop "#mult_"),
1469 Rls_ order_mult_rls_,
1470 Rls_ simplify_power_,
1471 Rls_ calc_add_mult_pow_,
1472 Rls_ reduce_012_mult_,
1473 Rls_ order_add_rls_,
1474 Rls_ collect_numerals_,
1476 (*Rls_ discard_parentheses_ *)
1481 (*.a minimal ruleset for reverse rewriting of factions [2];
1482 compare expand_binoms.*)
1484 Seq{id = "reverse_rewriting", preconds = [], rew_ord = ("termlessI",termlessI),
1485 erls = Atools_erls, srls = Erls,
1486 calc = [(*("PLUS" , ("op +", eval_binop "#add_")),
1487 ("TIMES" , ("op *", eval_binop "#mult_")),
1488 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1490 rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1491 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1492 Thm ("real_plus_binom_times1" ,num_str @{thm real_plus_binom_times1}),
1493 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1494 Thm ("real_plus_binom_times2" ,num_str @{thm real_plus_binom_times2}),
1495 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1497 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
1499 Thm ("left_distrib" ,num_str @{thm left_distrib}),
1500 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1501 Thm ("left_distrib2",num_str @{thm left_distrib2}),
1502 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1504 Thm ("real_mult_assoc", num_str @{thm real_mult_assoc}),
1505 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1506 Rls_ order_mult_rls_,
1507 (*Rls_ order_add_rls_,*)
1509 Calc ("op +", eval_binop "#add_"),
1510 Calc ("op *", eval_binop "#mult_"),
1511 Calc ("Atools.pow", eval_binop "#power_"),
1513 Thm ("sym_realpow_twoI",
1514 num_str (@{thm realpow_twoI} RS @{thm sym})),
1515 (*"r1 * r1 = r1 ^^^ 2"*)
1516 Thm ("sym_real_mult_2",
1517 num_str (@{thm real_mult_2} RS @{thm sym})),
1518 (*"z1 + z1 = 2 * z1"*)
1519 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1520 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1522 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1523 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1524 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1525 (*"[| l is_const; m is_const |] ==>
1526 l * n + (m * n + k) = (l + m) * n + k"*)
1527 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1528 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1529 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1530 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1532 Thm ("realpow_multI", num_str @{thm realpow_multI}),
1533 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1535 Calc ("op +", eval_binop "#add_"),
1536 Calc ("op *", eval_binop "#mult_"),
1537 Calc ("Atools.pow", eval_binop "#power_"),
1539 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
1540 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
1541 Thm ("add_0_left",num_str @{thm add_0_left})(*0 + z = z*)
1543 (*Rls_ order_add_rls_*)
1546 scr = EmptyScr}:rls;
1549 overwritelthy @{theory} (!ruleset',
1550 [("norm_Poly", prep_rls norm_Poly),
1551 ("Poly_erls",Poly_erls)(*FIXXXME:del with rls.rls'*),
1552 ("expand", prep_rls expand),
1553 ("expand_poly", prep_rls expand_poly),
1554 ("simplify_power", prep_rls simplify_power),
1555 ("order_add_mult", prep_rls order_add_mult),
1556 ("collect_numerals", prep_rls collect_numerals),
1557 ("collect_numerals_", prep_rls collect_numerals_),
1558 ("reduce_012", prep_rls reduce_012),
1559 ("discard_parentheses", prep_rls discard_parentheses),
1560 ("make_polynomial", prep_rls make_polynomial),
1561 ("expand_binoms", prep_rls expand_binoms),
1562 ("rev_rew_p", prep_rls rev_rew_p),
1563 ("discard_minus_", prep_rls discard_minus_),
1564 ("expand_poly_", prep_rls expand_poly_),
1565 ("expand_poly_rat_", prep_rls expand_poly_rat_),
1566 ("simplify_power_", prep_rls simplify_power_),
1567 ("calc_add_mult_pow_", prep_rls calc_add_mult_pow_),
1568 ("reduce_012_mult_", prep_rls reduce_012_mult_),
1569 ("reduce_012_", prep_rls reduce_012_),
1570 ("discard_parentheses_",prep_rls discard_parentheses_),
1571 ("order_mult_rls_", prep_rls order_mult_rls_),
1572 ("order_add_rls_", prep_rls order_add_rls_),
1573 ("make_rat_poly_with_parentheses",
1574 prep_rls make_rat_poly_with_parentheses)
1581 calclist':= overwritel (!calclist',
1582 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
1583 eval_is_polyrat_in "#eval_is_polyrat_in")),
1584 ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
1585 ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
1586 ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
1587 ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
1588 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
1589 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))
1596 (prep_pbt (theory "Poly") "pbl_simp_poly" [] e_pblID
1597 (["polynomial","simplification"],
1598 [("#Given" ,["TERM t_"]),
1599 ("#Where" ,["t_ is_polyexp"]),
1600 ("#Find" ,["normalform n_"])
1602 append_rls "e_rls" e_rls [(*for preds in where_*)
1603 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1605 [["simplification","for_polynomials"]]));
1611 (prep_met (theory "Poly") "met_simp_poly" [] e_metID
1612 (["simplification","for_polynomials"],
1613 [("#Given" ,["TERM t_"]),
1614 ("#Where" ,["t_ is_polyexp"]),
1615 ("#Find" ,["normalform n_"])
1617 {rew_ord'="tless_true",
1621 prls = append_rls "simplification_for_polynomials_prls" e_rls
1622 [(*for preds in where_*)
1623 Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1624 crls = e_rls, nrls = norm_Poly},
1625 "Script SimplifyScript (t_::real) = " ^
1626 " ((Rewrite_Set norm_Poly False) t_)"