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 (_ =))// (_))" 9)
28 (*-------------------- rules------------------------------------------------*)
29 axiomatization where (*.not contained in Isabelle2002,
30 stated as axioms, TODO: prove as theorems;
31 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
33 realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
34 realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
35 realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
36 realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
38 realpow_oneI: "r ^^^ 1 = r" and
39 realpow_zeroI: "r ^^^ 0 = 1" and
40 realpow_eq_oneI: "1 ^^^ n = 1" and
41 realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
42 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
43 (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
44 realpow_minus_oneI: "(- 1) ^^^ (2 * n) = 1" and
46 realpow_twoI: "r ^^^ 2 = r * r" and
47 realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
48 realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
49 realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
50 realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
51 realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
52 realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
53 realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
54 realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
55 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
56 ==> r ^^^ n = r * r ^^^ (n + -1)" and
57 realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
60 realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
61 realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
65 real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
66 real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
67 real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
68 real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
69 real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
70 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
71 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
72 real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
73 real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
75 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
76 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
77 real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
79 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
80 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
82 real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
83 *(a^^^2 + 2*a*b + b^^^2)" and
84 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
85 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
86 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
87 real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
88 real_diff_minus: "a - b = a + -1 * b" and
89 real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
90 real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
91 (*WN071229 changed for Schaerding -----vvv*)
92 (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
93 real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
94 (*WN071229 changed for Schaerding -----^^^*)
95 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
96 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
97 real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
98 real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
99 real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
100 real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
101 real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
102 real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
103 real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
104 real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
105 real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
106 real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
108 real_num_collect: "[| l is_const; m is_const |] ==>
109 l * n + m * n = (l + m) * n" and
110 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
111 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
112 real_num_collect_assoc: "[| l is_const; m is_const |] ==>
113 l * n + (m * n + k) = (l + m) * n + k" and
114 real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
115 l * n + (m * n + k) = (l + m)
117 real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
118 (k + m * n) + l * n = k + (l + m) * n" and
119 real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
120 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
121 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
122 real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
124 real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
125 real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
127 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
128 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
129 real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
130 real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
131 real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
133 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
134 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
136 text {* remark on 'polynomials'
138 *** there are 5 kinds of expanded normalforms ***
140 [1] 'complete polynomial' (Komplettes Polynom), univariate
141 a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
142 not (a_n = 0), some a_i may be zero (DON'T disappear),
143 variables in monomials lexicographically ordered and complete,
144 x written as 1*x^1, ...
145 [2] 'polynomial' (Polynom), univariate and multivariate
146 a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
147 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
148 not (a_n = 0), some a_i may be zero (ie. monomials disappear),
149 exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
150 and variables in monomials are lexicographically ordered
151 examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
152 [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
153 [2]: "x + (-50) * x ^^^ 3"
154 [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
156 [3] 'expanded_term' (Ausmultiplizierter Term):
157 pull out unary minus to binary minus,
158 as frequently exercised in schools; other conditions for [2] hold however
159 examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
160 "4 * x ^^^ 2 - 9 * y ^^^ 2"
161 [4] 'polynomial_in' (Polynom in):
162 polynomial in 1 variable with arbitrary coefficients
163 examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
164 "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
165 [5] 'expanded_in' (Ausmultiplizierter Termin in):
166 analoguous to [3] with binary minus like [3]
167 examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
168 "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
174 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
175 fun is_polyrat_in t v =
176 let fun coeff_in c v = member op = (TermC.vars c) v;
177 fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
178 (* at the moment there is no term like this, but ....*)
179 | finddivide (t as (Const ("Rings.divide_class.divide",_) $ _ $ b)) v =
181 | finddivide (_ $ t1 $ t2) v =
182 (finddivide t1 v) orelse (finddivide t2 v)
183 | finddivide (_ $ t1) v = (finddivide t1 v)
184 | finddivide _ _ = false;
185 in finddivide t v end;
187 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
189 then SOME ((Rule.term2str p) ^ " = True",
190 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
191 else SOME ((Rule.term2str p) ^ " = True",
192 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
193 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
196 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
197 fun coeff_in c v = not (member op = (TermC.vars c) v);
198 (* FIXME.WN100826 shift this into test--------------
199 val v = (Thm.term_of o the o (parse thy)) "x";
200 val t = (Thm.term_of o the o (parse thy)) "1";
202 (*val it = true : bool*)
203 val t = (Thm.term_of o the o (parse thy)) "a*b+c";
205 (*val it = true : bool*)
206 val t = (Thm.term_of o the o (parse thy)) "a*x+c";
208 (*val it = false : bool*)
209 ----------------------------------------------------*)
210 (*. a 'monomial t in variable v' is a term t with
211 either (1) v NOT existent in t, or (2) v contained in t,
213 if (2) then v is a factor on the very right, ev. with exponent.*)
214 fun factor_right_deg (*case 2*)
215 (t as Const ("Groups.times_class.times",_) $ t1 $
216 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
217 if ((vv = v) andalso (coeff_in t1 v)) then SOME (TermC.int_of_str d) else NONE
218 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
219 if (vv = v) then SOME (TermC.int_of_str d) else NONE
220 | factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v =
221 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
222 | factor_right_deg vv v =
223 if (vv = v) then SOME 1 else NONE;
224 fun mono_deg_in m v =
225 if coeff_in m v then (*case 1*) SOME 0
226 else factor_right_deg m v;
227 (* FIXME.WN100826 shift this into test-----------------------------
228 val v = (Thm.term_of o the o (parse thy)) "x";
229 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
232 val t = (Thm.term_of o the o (parse thy)) "x^^^7";
235 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
238 val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
241 val t = (Thm.term_of o the o (parse thy)) "x";
244 val t = (Thm.term_of o the o (parse thy)) "(a*b+c)";
247 val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
250 ------------------------------------------------------------------*)
251 fun expand_deg_in t v =
252 let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
253 (case mono_deg_in t2 v of (* $ is left associative*)
254 SOME d' => edi d' d' t1
256 | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
257 (case mono_deg_in t2 v of
258 SOME d' => edi d' d' t1
260 | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
261 (case mono_deg_in t2 v of
262 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
263 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
264 then edi d' dmax t1 else NONE
266 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
267 (case mono_deg_in t2 v of
268 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
269 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
270 then edi d' dmax t1 else NONE
272 | edi ~1 ~1 t = (case mono_deg_in t v of
275 | edi d dmax t = (*basecase last*)
276 (case mono_deg_in t v of
277 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
278 then SOME dmax else NONE
281 (* FIXME.WN100826 shift this into test-----------------------------
282 val v = (Thm.term_of o the o (parse thy)) "x";
283 val t = (Thm.term_of o the o (parse thy)) "a+b";
286 val t = (Thm.term_of o the o (parse thy)) "(a+b)*x";
289 val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x";
292 val t = (Thm.term_of o the o (parse thy)) "a*b + (a-b)*x";
295 val t = (Thm.term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
297 -------------------------------------------------------------------*)
298 fun poly_deg_in t v =
299 let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
300 (case mono_deg_in t2 v of (* $ is left associative*)
301 SOME d' => edi d' d' t1
303 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
304 (case mono_deg_in t2 v of
305 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
306 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
307 then edi d' dmax t1 else NONE
309 | edi ~1 ~1 t = (case mono_deg_in t v of
312 | edi d dmax t = (*basecase last*)
313 (case mono_deg_in t v of
314 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
315 then SOME dmax else NONE
320 fun is_expanded_in t v =
321 case expand_deg_in t v of SOME _ => true | NONE => false;
323 case poly_deg_in t v of SOME _ => true | NONE => false;
324 fun has_degree_in t v =
325 case expand_deg_in t v of SOME d => d | NONE => ~1;
327 (* FIXME.WN100826 shift this into test-----------------------------
328 val v = (Thm.term_of o the o (parse thy)) "x";
329 val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
332 val t = (Thm.term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
335 val t = (Thm.term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
338 -------------------------------------------------------------------*)
340 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
341 fun eval_is_expanded_in _ _
342 (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
343 if is_expanded_in t v
344 then SOME ((Rule.term2str p) ^ " = True",
345 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
346 else SOME ((Rule.term2str p) ^ " = True",
347 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
348 | eval_is_expanded_in _ _ _ _ = NONE;
350 val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
351 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
352 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
354 (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
357 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
358 fun eval_is_poly_in _ _
359 (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
361 then SOME ((Rule.term2str p) ^ " = True",
362 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
363 else SOME ((Rule.term2str p) ^ " = True",
364 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
365 | eval_is_poly_in _ _ _ _ = NONE;
367 val t = (Thm.term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
368 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
369 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
371 (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
374 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
375 fun eval_has_degree_in _ _
376 (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
377 let val d = has_degree_in t v
378 val d' = TermC.term_of_num HOLogic.realT d
379 in SOME ((Rule.term2str p) ^ " = " ^ (string_of_int d),
380 HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
382 | eval_has_degree_in _ _ _ _ = NONE;
384 > val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
385 > val SOME (id, t') = eval_has_degree_in 0 0 t 0;
386 val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
388 val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
393 Rule.append_rls "calculate_PolyFIXXXME.not.impl." Rule.e_rls
396 (*.for evaluation of conditions in rewrite rules.*)
397 val Poly_erls = Rule.append_rls "Poly_erls" Atools_erls
398 [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
399 Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
400 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
401 Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
402 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
403 Rule.Calc ("Atools.pow", eval_binop "#power_")];
405 val poly_crls = Rule.append_rls "poly_crls" Atools_crls
406 [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
407 Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
408 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
409 Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
410 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
411 Rule.Calc ("Atools.pow" ,eval_binop "#power_")];
413 local (*. for make_polynomial .*)
415 open Term; (* for type order = EQUAL | LESS | GREATER *)
417 fun pr_ord EQUAL = "EQUAL"
418 | pr_ord LESS = "LESS"
419 | pr_ord GREATER = "GREATER";
421 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
423 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
424 | _ => (((a, 0), T), 0))
425 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
426 | dest_hd' (Var v) = (v, 2)
427 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
428 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
430 fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
431 (case TermC.int_of_str_opt (order) of
434 | get_order_pow _ = 0;
436 fun size_of_term' (Const(str,_) $ t) =
437 if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
438 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
439 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
440 | size_of_term' _ = 1;
442 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
443 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
444 | term_ord' pr thy (t, u) =
447 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
448 val _ = tracing ("t= f@ts= \"" ^ Rule.term_to_string''' thy f ^ "\" @ \"[" ^
449 commas (map (Rule.term_to_string''' thy) ts) ^ "]\"");
450 val _ = tracing("u= g@us= \"" ^ Rule.term_to_string''' thy g ^ "\" @ \"[" ^
451 commas (map (Rule.term_to_string''' thy) us) ^ "]\"");
452 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
453 string_of_int (size_of_term' u) ^ ")");
454 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
455 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
456 val _ = tracing ("-------");
459 case int_ord (size_of_term' t, size_of_term' u) of
461 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
462 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
466 and hd_ord (f, g) = (* ~ term.ML *)
467 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
468 and terms_ord str pr (ts, us) =
469 list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
473 fun ord_make_polynomial (pr:bool) thy (_: Rule.subst) tu =
474 (term_ord' pr thy(***) tu = LESS );
479 Rule.rew_ord' := overwritel (! Rule.rew_ord',
480 [("termlessI", termlessI),
481 ("ord_make_polynomial", ord_make_polynomial false thy)
486 Rule.Rls {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
487 erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
488 rules = [Rule.Thm ("distrib_right" , TermC.num_str @{thm distrib_right}),
489 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
490 Rule.Thm ("distrib_left", TermC.num_str @{thm distrib_left})
491 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
492 ], scr = Rule.EmptyScr};
494 (*----------------- Begin: rulesets for make_polynomial_ -----------------
495 'rlsIDs' redefined by MG as 'rlsIDs_'
499 Rule.Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
500 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
502 [Rule.Thm ("real_diff_minus", TermC.num_str @{thm real_diff_minus}),
503 (*"a - b = a + -1 * b"*)
504 Rule.Thm ("sym_real_mult_minus1", TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
505 (*- ?z = "-1 * ?z"*)],
506 scr = Rule.EmptyScr};
509 Rule.Rls{id = "expand_poly_", preconds = [],
510 rew_ord = ("dummy_ord", Rule.dummy_ord),
511 erls = Rule.e_rls,srls = Rule.Erls,
512 calc = [], errpatts = [],
514 [Rule.Thm ("real_plus_binom_pow4", TermC.num_str @{thm real_plus_binom_pow4}),
515 (*"(a + b)^^^4 = ... "*)
516 Rule.Thm ("real_plus_binom_pow5",TermC.num_str @{thm real_plus_binom_pow5}),
517 (*"(a + b)^^^5 = ... "*)
518 Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
519 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
520 (*WN071229 changed/removed for Schaerding -----vvv*)
521 (*Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),*)
522 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
523 Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
524 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
525 (*Rule.Thm ("real_plus_minus_binom1_p_p", TermC.num_str @{thm real_plus_minus_binom1_p_p}),*)
526 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
527 (*Rule.Thm ("real_plus_minus_binom2_p_p", TermC.num_str @{thm real_plus_minus_binom2_p_p}),*)
528 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
529 (*WN071229 changed/removed for Schaerding -----^^^*)
531 Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
532 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
533 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
534 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
536 Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
537 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
538 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
539 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
540 ], scr = Rule.EmptyScr};
542 (*.the expression contains + - * ^ only ?
543 this is weaker than 'is_polynomial' !.*)
544 fun is_polyexp (Free _) = true
545 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
546 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
547 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
548 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
549 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
550 ((is_polyexp t1) andalso (is_polyexp t2))
551 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
552 ((is_polyexp t1) andalso (is_polyexp t2))
553 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
554 ((is_polyexp t1) andalso (is_polyexp t2))
555 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
556 ((is_polyexp t1) andalso (is_polyexp t2))
557 | is_polyexp _ = false;
559 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
560 fun eval_is_polyexp (thmid:string) _
561 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
563 then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
564 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
565 else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
566 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
567 | eval_is_polyexp _ _ _ _ = NONE;
569 val expand_poly_rat_ =
570 Rule.Rls{id = "expand_poly_rat_", preconds = [],
571 rew_ord = ("dummy_ord", Rule.dummy_ord),
572 erls = Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
573 [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")
576 calc = [], errpatts = [],
578 [Rule.Thm ("real_plus_binom_pow4_poly", TermC.num_str @{thm real_plus_binom_pow4_poly}),
579 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
580 Rule.Thm ("real_plus_binom_pow5_poly", TermC.num_str @{thm real_plus_binom_pow5_poly}),
581 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
582 Rule.Thm ("real_plus_binom_pow2_poly",TermC.num_str @{thm real_plus_binom_pow2_poly}),
583 (*"[| a is_polyexp; b is_polyexp |] ==>
584 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
585 Rule.Thm ("real_plus_binom_pow3_poly",TermC.num_str @{thm real_plus_binom_pow3_poly}),
586 (*"[| a is_polyexp; b is_polyexp |] ==>
587 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
588 Rule.Thm ("real_plus_minus_binom1_p_p",TermC.num_str @{thm real_plus_minus_binom1_p_p}),
589 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
590 Rule.Thm ("real_plus_minus_binom2_p_p",TermC.num_str @{thm real_plus_minus_binom2_p_p}),
591 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
593 Rule.Thm ("real_add_mult_distrib_poly",
594 TermC.num_str @{thm real_add_mult_distrib_poly}),
595 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
596 Rule.Thm("real_add_mult_distrib2_poly",
597 TermC.num_str @{thm real_add_mult_distrib2_poly}),
598 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
600 Rule.Thm ("realpow_multI_poly", TermC.num_str @{thm realpow_multI_poly}),
601 (*"[| r is_polyexp; s is_polyexp |] ==>
602 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
603 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
604 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
605 ], scr = Rule.EmptyScr};
607 val simplify_power_ =
608 Rule.Rls{id = "simplify_power_", preconds = [],
609 rew_ord = ("dummy_ord", Rule.dummy_ord),
610 erls = Rule.e_rls, srls = Rule.Erls,
611 calc = [], errpatts = [],
612 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
613 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
614 Rule.Thm ("sym_realpow_twoI",
615 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
616 (*"r * r = r ^^^ 2"*)
617 Rule.Thm ("realpow_twoI_assoc_l",TermC.num_str @{thm realpow_twoI_assoc_l}),
618 (*"r * (r * s) = r ^^^ 2 * s"*)
620 Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
621 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
622 Rule.Thm ("realpow_plus_1_assoc_l",
623 TermC.num_str @{thm realpow_plus_1_assoc_l}),
624 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
625 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
626 Rule.Thm ("realpow_plus_1_assoc_l2",
627 TermC.num_str @{thm realpow_plus_1_assoc_l2}),
628 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
630 Rule.Thm ("sym_realpow_addI",
631 TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
632 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
633 Rule.Thm ("realpow_addI_assoc_l",TermC.num_str @{thm realpow_addI_assoc_l}),
634 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
636 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
637 "r * r = r ^^^ 2" wenn r=a^^^b*)
638 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
639 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
640 ], scr = Rule.EmptyScr};
642 val calc_add_mult_pow_ =
643 Rule.Rls{id = "calc_add_mult_pow_", preconds = [],
644 rew_ord = ("dummy_ord", Rule.dummy_ord),
645 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
646 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
647 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
648 ("POWER", ("Atools.pow", eval_binop "#power_"))
651 rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
652 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
653 Rule.Calc ("Atools.pow", eval_binop "#power_")
654 ], scr = Rule.EmptyScr};
656 val reduce_012_mult_ =
657 Rule.Rls{id = "reduce_012_mult_", preconds = [],
658 rew_ord = ("dummy_ord", Rule.dummy_ord),
659 erls = Rule.e_rls,srls = Rule.Erls,
660 calc = [], errpatts = [],
661 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
662 Rule.Thm ("mult_1_right",TermC.num_str @{thm mult_1_right}),
663 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
664 Rule.Thm ("realpow_zeroI",TermC.num_str @{thm realpow_zeroI}),
665 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
666 Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
668 Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
670 ], scr = Rule.EmptyScr};
672 val collect_numerals_ =
673 Rule.Rls{id = "collect_numerals_", preconds = [],
674 rew_ord = ("dummy_ord", Rule.dummy_ord),
675 erls = Atools_erls, srls = Rule.Erls,
676 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
679 [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
680 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
681 Rule.Thm ("real_num_collect_assoc_r",TermC.num_str @{thm real_num_collect_assoc_r}),
682 (*"[| l is_const; m is_const |] ==> \
683 \(k + m * n) + l * n = k + (l + m)*n"*)
684 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
685 (*"m is_const ==> n + m * n = (1 + m) * n"*)
686 Rule.Thm ("real_one_collect_assoc_r",TermC.num_str @{thm real_one_collect_assoc_r}),
687 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
689 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
691 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
692 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
693 Rule.Thm ("real_mult_2_assoc_r",TermC.num_str @{thm real_mult_2_assoc_r}),
694 (*"(k + z1) + z1 = k + 2 * z1"*)
695 Rule.Thm ("sym_real_mult_2",TermC.num_str (@{thm real_mult_2} RS @{thm sym}))
696 (*"z1 + z1 = 2 * z1"*)
697 ], scr = Rule.EmptyScr};
700 Rule.Rls{id = "reduce_012_", preconds = [],
701 rew_ord = ("dummy_ord", Rule.dummy_ord),
702 erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
703 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
705 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
707 Rule.Thm ("mult_zero_right",TermC.num_str @{thm mult_zero_right}),
709 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
711 Rule.Thm ("add_0_right",TermC.num_str @{thm add_0_right}),
712 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
714 (*Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI})*)
716 Rule.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
718 ], scr = Rule.EmptyScr};
720 val discard_parentheses1 =
721 Rule.append_rls "discard_parentheses1" Rule.e_rls
722 [Rule.Thm ("sym_mult_assoc",
723 TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
724 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
725 (*Rule.Thm ("sym_add_assoc",
726 TermC.num_str (@{thm add_assoc} RS @{thm sym}))*)
727 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
730 (*----------------- End: rulesets for make_polynomial_ -----------------*)
732 (*MG.0401 ev. for use in rls with ordered rewriting ?
733 val collect_numerals_left =
734 Rule.Rls{id = "collect_numerals", preconds = [],
735 rew_ord = ("dummy_ord", Rule.dummy_ord),
736 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
737 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
738 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
739 ("POWER", ("Atools.pow", eval_binop "#power_"))
742 rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
743 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
744 Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
745 (*"[| l is_const; m is_const |] ==>
746 l * n + (m * n + k) = (l + m) * n + k"*)
747 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
748 (*"m is_const ==> n + m * n = (1 + m) * n"*)
749 Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
750 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
752 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
754 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
755 Rule.Thm ("sym_real_mult_2",
756 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
757 (*"z1 + z1 = 2 * z1"*)
758 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc})
759 (*"z1 + (z1 + k) = 2 * z1 + k"*)
760 ], scr = Rule.EmptyScr};*)
763 Rule.Rls{id = "expand_poly", preconds = [],
764 rew_ord = ("dummy_ord", Rule.dummy_ord),
765 erls = Rule.e_rls,srls = Rule.Erls,
766 calc = [], errpatts = [],
768 rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
769 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
770 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
771 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
772 (*Rule.Thm ("distrib_right1",TermC.num_str @{thm distrib_right}1),
773 ....... 18.3.03 undefined???*)
775 Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
776 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
777 Rule.Thm ("real_minus_binom_pow2_p",TermC.num_str @{thm real_minus_binom_pow2_p}),
778 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
779 Rule.Thm ("real_plus_minus_binom1_p",
780 TermC.num_str @{thm real_plus_minus_binom1_p}),
781 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
782 Rule.Thm ("real_plus_minus_binom2_p",
783 TermC.num_str @{thm real_plus_minus_binom2_p}),
784 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
786 Rule.Thm ("minus_minus",TermC.num_str @{thm minus_minus}),
788 Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
789 (*"a - b = a + -1 * b"*)
790 Rule.Thm ("sym_real_mult_minus1",
791 TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
794 (*Rule.Thm ("real_minus_add_distrib",
795 TermC.num_str @{thm real_minus_add_distrib}),*)
796 (*"- (?x + ?y) = - ?x + - ?y"*)
797 (*Rule.Thm ("real_diff_plus",TermC.num_str @{thm real_diff_plus})*)
799 ], scr = Rule.EmptyScr};
802 Rule.Rls{id = "simplify_power", preconds = [],
803 rew_ord = ("dummy_ord", Rule.dummy_ord),
804 erls = Rule.e_rls, srls = Rule.Erls,
805 calc = [], errpatts = [],
806 rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
807 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
809 Rule.Thm ("sym_realpow_twoI",
810 TermC.num_str( @{thm realpow_twoI} RS @{thm sym})),
811 (*"r1 * r1 = r1 ^^^ 2"*)
812 Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
813 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
814 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
815 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
816 Rule.Thm ("sym_realpow_addI",
817 TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
818 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
819 Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
821 Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
823 ], scr = Rule.EmptyScr};
824 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
825 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
827 Rule.Rls{id = "order_add_mult", preconds = [],
828 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
829 erls = Rule.e_rls,srls = Rule.Erls,
830 calc = [], errpatts = [],
831 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
833 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
834 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
835 Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
836 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
837 Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
839 Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
840 (*x + (y + z) = y + (x + z)*)
841 Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
842 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
843 ], scr = Rule.EmptyScr};
844 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
845 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
847 Rule.Rls{id = "order_mult", preconds = [],
848 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
849 erls = Rule.e_rls,srls = Rule.Erls,
850 calc = [], errpatts = [],
851 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
853 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
854 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
855 Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc})
856 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
857 ], scr = Rule.EmptyScr};
861 val collect_numerals =
862 Rule.Rls{id = "collect_numerals", preconds = [],
863 rew_ord = ("dummy_ord", Rule.dummy_ord),
864 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
865 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
866 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
867 ("POWER", ("Atools.pow", eval_binop "#power_"))
869 rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
870 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
871 Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
872 (*"[| l is_const; m is_const |] ==>
873 l * n + (m * n + k) = (l + m) * n + k"*)
874 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
875 (*"m is_const ==> n + m * n = (1 + m) * n"*)
876 Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
877 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
878 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
879 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
880 Rule.Calc ("Atools.pow", eval_binop "#power_")
881 ], scr = Rule.EmptyScr};
883 Rule.Rls{id = "reduce_012", preconds = [],
884 rew_ord = ("dummy_ord", Rule.dummy_ord),
885 erls = Rule.e_rls,srls = Rule.Erls,
886 calc = [], errpatts = [],
887 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
889 (*Rule.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),14.3.03*)
891 Rule.Thm ("minus_mult_left",
892 TermC.num_str (@{thm minus_mult_left} RS @{thm sym})),
893 (*- (?x * ?y) = "- ?x * ?y"*)
894 (*Rule.Thm ("real_minus_mult_cancel",
895 TermC.num_str @{thm real_minus_mult_cancel}),
896 (*"- ?x * - ?y = ?x * ?y"*)---*)
897 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
899 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
901 Rule.Thm ("right_minus",TermC.num_str @{thm right_minus}),
903 Rule.Thm ("sym_real_mult_2",
904 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
905 (*"z1 + z1 = 2 * z1"*)
906 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc})
907 (*"z1 + (z1 + k) = 2 * z1 + k"*)
908 ], scr = Rule.EmptyScr};
910 val discard_parentheses =
911 Rule.append_rls "discard_parentheses" Rule.e_rls
912 [Rule.Thm ("sym_mult_assoc",
913 TermC.num_str (@{thm mult.assoc} RS @{thm sym})),
914 Rule.Thm ("sym_add_assoc",
915 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
917 (* probably perfectly replaced by auto-generated version *)
918 val scr_make_polynomial =
919 "Script Expand_binoms t_t = " ^
921 "((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
923 " (Try (Repeat (Rewrite distrib_right False))) @@ " ^
924 " (Try (Repeat (Rewrite distrib_left False))) @@ " ^
925 " (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
926 " (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
928 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
929 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
930 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
932 " (Try (Repeat (Rewrite mult_commute False))) @@ " ^
933 " (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
934 " (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
935 " (Try (Repeat (Rewrite add_commute False))) @@ " ^
936 " (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
937 " (Try (Repeat (Rewrite add_assoc False))) @@ " ^
939 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
940 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
941 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
942 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
944 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
945 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
947 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
948 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
950 " (Try (Repeat (Calculate PLUS ))) @@ " ^
951 " (Try (Repeat (Calculate TIMES ))) @@ " ^
952 " (Try (Repeat (Calculate POWER)))) " ^
955 (*version used by MG.02/03, overwritten by version AG in 04 below
956 val make_polynomial = prep_rls'(
957 Rule.Seq{id = "make_polynomial", preconds = []:term list,
958 rew_ord = ("dummy_ord", Rule.dummy_ord),
959 erls = Atools_erls, srls = Rule.Erls,
960 calc = [], errpatts = [],
961 rules = [Rule.Rls_ expand_poly,
962 Rule.Rls_ order_add_mult,
963 Rule.Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
964 Rule.Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
965 Rule.Rls_ reduce_012,
966 Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),(*in --^*)
967 Rule.Rls_ discard_parentheses
972 (* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
973 val scr_expand_binoms =
974 "Script Expand_binoms t_t =" ^
976 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
977 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
978 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
979 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
980 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
981 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
983 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
984 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
985 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
987 " (Try (Repeat (Calculate PLUS ))) @@ " ^
988 " (Try (Repeat (Calculate TIMES ))) @@ " ^
989 " (Try (Repeat (Calculate POWER))) @@ " ^
991 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
992 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
993 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
994 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
996 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
997 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
999 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
1000 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1002 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1003 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1004 " (Try (Repeat (Calculate POWER)))) " ^
1008 Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1009 erls = Atools_erls, srls = Rule.Erls,
1010 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1011 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1012 ("POWER", ("Atools.pow", eval_binop "#power_"))
1014 rules = [Rule.Thm ("real_plus_binom_pow2",
1015 TermC.num_str @{thm real_plus_binom_pow2}),
1016 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1017 Rule.Thm ("real_plus_binom_times",
1018 TermC.num_str @{thm real_plus_binom_times}),
1019 (*"(a + b)*(a + b) = ...*)
1020 Rule.Thm ("real_minus_binom_pow2",
1021 TermC.num_str @{thm real_minus_binom_pow2}),
1022 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1023 Rule.Thm ("real_minus_binom_times",
1024 TermC.num_str @{thm real_minus_binom_times}),
1025 (*"(a - b)*(a - b) = ...*)
1026 Rule.Thm ("real_plus_minus_binom1",
1027 TermC.num_str @{thm real_plus_minus_binom1}),
1028 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1029 Rule.Thm ("real_plus_minus_binom2",
1030 TermC.num_str @{thm real_plus_minus_binom2}),
1031 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1033 Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
1034 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1035 Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
1036 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1037 Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
1038 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1039 Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
1040 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1041 Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1042 (*(a*b)^^^n = a^^^n * b^^^n*)
1043 Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
1044 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1045 Rule.Thm ("real_minus_binom_pow3",
1046 TermC.num_str @{thm real_minus_binom_pow3}),
1047 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1050 (*Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1051 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1052 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1053 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1054 Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1055 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1056 Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1057 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1059 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1061 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1063 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),(*"0 + z = z"*)
1065 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1066 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1067 Rule.Calc ("Atools.pow", eval_binop "#power_"),
1068 (*Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
1070 Rule.Thm ("real_mult_left_commute",
1071 TermC.num_str @{thm real_mult_left_commute}),
1072 Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1073 Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1074 Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1075 Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1077 Rule.Thm ("sym_realpow_twoI",
1078 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1079 (*"r1 * r1 = r1 ^^^ 2"*)
1080 Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1081 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1082 (*Rule.Thm ("sym_real_mult_2",
1083 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1084 (*"z1 + z1 = 2 * z1"*)*)
1085 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1086 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1088 Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1089 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
1090 Rule.Thm ("real_num_collect_assoc",
1091 TermC.num_str @{thm real_num_collect_assoc}),
1092 (*"[| l is_const; m is_const |] ==>
1093 l * n + (m * n + k) = (l + m) * n + k"*)
1094 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1095 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1096 Rule.Thm ("real_one_collect_assoc",
1097 TermC.num_str @{thm real_one_collect_assoc}),
1098 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1100 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1101 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1102 Rule.Calc ("Atools.pow", eval_binop "#power_")
1104 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) scr_expand_binoms)
1108 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
1110 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
1111 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
1112 (* Polynom --> List von Monomen *)
1113 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1114 (poly2list t1) @ (poly2list t2)
1115 | poly2list t = [t];
1117 (* Monom --> Liste von Variablen *)
1118 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1119 (monom2list t1) @ (monom2list t2)
1120 | monom2list t = [t];
1122 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
1123 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
1124 | get_basStr (Free (str, _)) = str
1125 | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
1127 error("get_basStr: called with t= "^(Rule.term2str t));*)
1129 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
1130 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
1131 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1132 | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
1133 | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
1135 error("get_potStr: called with t= "^(Rule.term2str t));*)
1137 (* Umgekehrte string_ord *)
1138 val string_ord_rev = rev_order o string_ord;
1140 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
1141 innerhalb eines Monomes:
1142 - zuerst lexikographisch nach Variablenname
1143 - wenn gleich: nach steigender Potenz *)
1144 fun var_ord (a,b: term) = prod_ord string_ord string_ord
1145 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1147 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
1148 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
1149 - zuerst lexikographisch nach Variablenname
1150 - wenn gleich: nach sinkender Potenz*)
1151 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
1152 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1155 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
1156 val sort_varList = sort var_ord;
1158 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
1159 Argumente in eine Liste *)
1160 fun args u : term list =
1161 let fun stripc (f$t, ts) = stripc (f, t::ts)
1162 | stripc (t as Free _, ts) = (t::ts)
1163 | stripc (_, ts) = ts
1164 in stripc (u, []) end;
1166 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
1167 (keine Variablen) enthaelt *)
1168 fun filter_num [] = true
1169 | filter_num [Free x] = if (TermC.is_num (Free x)) then true
1171 | filter_num ((Free _)::_) = false
1173 (filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;
1175 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
1176 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
1177 fun is_nums t = filter_num [t];
1179 (* Berechnet den Gesamtgrad eines Monoms *)
1181 fun counter (n, []) = n
1182 | counter (n, x :: xs) =
1187 (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
1188 if (is_nums (Free (str_h, T))) then
1189 counter (n + (the (TermC.int_of_str_opt str_h)), xs)
1190 else counter (n + 1000, xs) (*FIXME.MG?!*)
1191 | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
1192 counter (n + 1000, xs) (*FIXME.MG?!*)
1193 | (Free (str, _)) => counter (n + 1, xs)
1194 (*| _ => error("monom_degree: called with factor: "^(Rule.term2str x)))*)
1195 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
1197 fun monom_degree l = counter (0, l)
1200 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
1201 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
1202 werden jedoch dabei ignoriert (uebersprungen) *)
1203 fun dict_cond_ord _ _ ([], []) = EQUAL
1204 | dict_cond_ord _ _ ([], _ :: _) = LESS
1205 | dict_cond_ord _ _ (_ :: _, []) = GREATER
1206 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
1207 (case (cond x, cond y) of
1208 (false, false) => (case elem_ord (x, y) of
1209 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
1211 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
1212 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
1213 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
1215 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
1216 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
1217 dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
1218 fun degree_ord (xs, ys) =
1219 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
1220 ((monom_degree xs, xs), (monom_degree ys, ys));
1222 fun hd_str str = substring (str, 0, 1);
1223 fun tl_str str = substring (str, 1, (size str) - 1);
1225 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
1226 fun get_koeff_of_mon [] = error("get_koeff_of_mon: called with l = []")
1227 | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
1230 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
1231 fun koeff2ordStr (SOME x) = (case x of
1233 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
1235 | _ => "aaa") (* "num.Ausdruck" --> gross *)
1236 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
1238 (* Order zum Vergleich von Koeffizienten (strings):
1239 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
1240 fun compare_koeff_ord (xs, ys) =
1241 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
1242 (koeff2ordStr o get_koeff_of_mon) ys);
1244 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
1245 fun koeff_degree_ord (xs, ys) =
1246 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
1248 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
1249 Gesamtgradordnung *)
1250 val sort_monList = sort koeff_degree_ord;
1252 (* Alternativ zu degree_ord koennte auch die viel einfachere und
1253 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
1254 fuer unsere Zwecke geeignet!
1256 fun simple_ord (al,bl: term list) = dict_ord string_ord
1257 (map get_basStr al, map get_basStr bl);
1259 val sort_monList = sort simple_ord; *)
1261 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1262 (mit gewuenschtem Typen T) *)
1263 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
1264 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
1265 fun binop op_ t1 t2 = op_ $ t1 $ t2;
1266 fun create_prod T (a,b) = binop (mult T) a b;
1267 fun create_sum T (a,b) = binop (plus T) a b;
1269 (* löscht letztes Element einer Liste *)
1270 fun drop_last l = take ((length l)-1,l);
1272 (* Liste von Variablen --> Monom *)
1273 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
1275 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
1276 gleiche Monome zusammengefasst werden können (collect_numerals)!
1277 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
1279 (* Liste von Monomen --> Polynom *)
1280 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
1282 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
1283 bessere Darstellung, da keine Klammern sichtbar!
1284 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
1286 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
1287 fun sort_variables t =
1289 val ll = map monom2list (poly2list t);
1290 val lls = map sort_varList ll;
1292 val ls = map (create_monom T) lls;
1293 in create_polynom T ls end;
1295 (* sorts the monoms of an expanded and variable-sorted polynomial
1299 val ll = map monom2list (poly2list t);
1300 val lls = sort_monList ll;
1302 val ls = map (create_monom T) lls;
1303 in create_polynom T ls end;
1305 (* auch Klammerung muss übereinstimmen;
1306 sort_variables klammert Produkte rechtslastig*)
1307 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
1311 fun eval_is_multUnordered (thmid:string) _
1312 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
1313 if is_multUnordered arg
1314 then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1315 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1316 else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1317 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1318 | eval_is_multUnordered _ _ _ _ = NONE;
1320 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1321 []:(Rule.rule * (term * term list)) list;
1322 fun init_state (_: term) = Rule.e_rrlsstate;
1323 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1324 ([]:(Rule.rule * (term * term list)) list);
1325 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1326 fun normal_form t = SOME (sort_variables t, []: term list);
1329 Rule.Rrls {id = "order_mult_",
1331 (* ?p matched with the current term gives an environment,
1332 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1333 [([TermC.parse_patt thy "?p is_multUnordered"],
1334 TermC.parse_patt thy "?p :: real")],
1335 rew_ord = ("dummy_ord", Rule.dummy_ord),
1336 erls = Rule.append_rls "Rule.e_rls-is_multUnordered" Rule.e_rls
1337 [Rule.Calc ("Poly.is'_multUnordered",
1338 eval_is_multUnordered "")],
1339 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1340 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1341 ("DIVIDE", ("Rings.divide_class.divide",
1342 eval_cancel "#divide_e")),
1343 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
1345 scr = Rule.Rfuns {init_state = init_state,
1346 normal_form = normal_form,
1347 locate_rule = locate_rule,
1348 next_rule = next_rule,
1349 attach_form = attach_form}};
1350 val order_mult_rls_ =
1351 Rule.Rls {id = "order_mult_rls_", preconds = [],
1352 rew_ord = ("dummy_ord", Rule.dummy_ord),
1353 erls = Rule.e_rls,srls = Rule.Erls,
1354 calc = [], errpatts = [],
1355 rules = [Rule.Rls_ order_mult_
1356 ], scr = Rule.EmptyScr};
1360 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
1363 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
1364 fun eval_is_addUnordered (thmid:string) _
1365 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
1366 if is_addUnordered arg
1367 then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1368 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1369 else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
1370 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1371 | eval_is_addUnordered _ _ _ _ = NONE;
1373 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1374 []: (Rule.rule * (term * term list)) list;
1375 fun init_state (_: term) = Rule.e_rrlsstate;
1376 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1377 ([]: (Rule.rule * (term * term list)) list);
1378 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1379 fun normal_form t = SOME (sort_monoms t,[]: term list);
1383 Rule.Rrls {id = "order_add_",
1384 prepat = (*WN.18.6.03 Preconditions und Pattern,
1385 die beide passen muessen, damit das Rule.Rrls angewandt wird*)
1386 [([TermC.parse_patt @{theory} "?p is_addUnordered"],
1387 TermC.parse_patt @{theory} "?p :: real"
1388 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1389 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1390 rew_ord = ("dummy_ord", Rule.dummy_ord),
1391 erls = Rule.append_rls "Rule.e_rls-is_addUnordered" Rule.e_rls(*MG: poly_erls*)
1392 [Rule.Calc ("Poly.is'_addUnordered",
1393 eval_is_addUnordered "")],
1394 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
1395 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
1396 ("DIVIDE",("Rings.divide_class.divide",
1397 eval_cancel "#divide_e")),
1398 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1400 scr = Rule.Rfuns {init_state = init_state,
1401 normal_form = normal_form,
1402 locate_rule = locate_rule,
1403 next_rule = next_rule,
1404 attach_form = attach_form}};
1406 val order_add_rls_ =
1407 Rule.Rls {id = "order_add_rls_", preconds = [],
1408 rew_ord = ("dummy_ord", Rule.dummy_ord),
1409 erls = Rule.e_rls,srls = Rule.Erls,
1410 calc = [], errpatts = [],
1411 rules = [Rule.Rls_ order_add_
1412 ], scr = Rule.EmptyScr};
1415 text {* rule-set make_polynomial also named norm_Poly:
1416 Rewrite order has not been implemented properly; the order is better in
1417 make_polynomial_in (coded in SML).
1418 Notes on state of development:
1419 \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
1420 \# migration Isabelle2002 --> 2011 weakened the rule set, see test
1421 --- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
1424 (*. see MG-DA.p.52ff .*)
1425 val make_polynomial(*MG.03, overwrites version from above,
1426 previously 'make_polynomial_'*) =
1427 Rule.Seq {id = "make_polynomial", preconds = []:term list,
1428 rew_ord = ("dummy_ord", Rule.dummy_ord),
1429 erls = Atools_erls, srls = Rule.Erls,calc = [], errpatts = [],
1430 rules = [Rule.Rls_ discard_minus,
1431 Rule.Rls_ expand_poly_,
1432 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1433 Rule.Rls_ order_mult_rls_,
1434 Rule.Rls_ simplify_power_,
1435 Rule.Rls_ calc_add_mult_pow_,
1436 Rule.Rls_ reduce_012_mult_,
1437 Rule.Rls_ order_add_rls_,
1438 Rule.Rls_ collect_numerals_,
1439 Rule.Rls_ reduce_012_,
1440 Rule.Rls_ discard_parentheses1
1446 val norm_Poly(*=make_polynomial*) =
1447 Rule.Seq {id = "norm_Poly", preconds = []:term list,
1448 rew_ord = ("dummy_ord", Rule.dummy_ord),
1449 erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1450 rules = [Rule.Rls_ discard_minus,
1451 Rule.Rls_ expand_poly_,
1452 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1453 Rule.Rls_ order_mult_rls_,
1454 Rule.Rls_ simplify_power_,
1455 Rule.Rls_ calc_add_mult_pow_,
1456 Rule.Rls_ reduce_012_mult_,
1457 Rule.Rls_ order_add_rls_,
1458 Rule.Rls_ collect_numerals_,
1459 Rule.Rls_ reduce_012_,
1460 Rule.Rls_ discard_parentheses1
1466 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1
1467 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1468 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1469 val make_rat_poly_with_parentheses =
1470 Rule.Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1471 rew_ord = ("dummy_ord", Rule.dummy_ord),
1472 erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1473 rules = [Rule.Rls_ discard_minus,
1474 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1475 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1476 Rule.Rls_ order_mult_rls_,
1477 Rule.Rls_ simplify_power_,
1478 Rule.Rls_ calc_add_mult_pow_,
1479 Rule.Rls_ reduce_012_mult_,
1480 Rule.Rls_ order_add_rls_,
1481 Rule.Rls_ collect_numerals_,
1482 Rule.Rls_ reduce_012_
1483 (*Rule.Rls_ discard_parentheses1 *)
1489 (*.a minimal ruleset for reverse rewriting of factions [2];
1490 compare expand_binoms.*)
1492 Rule.Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1493 erls = Atools_erls, srls = Rule.Erls,
1494 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1495 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1496 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1498 rules = [Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
1499 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1500 Rule.Thm ("real_plus_binom_times1" ,TermC.num_str @{thm real_plus_binom_times1}),
1501 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1502 Rule.Thm ("real_plus_binom_times2" ,TermC.num_str @{thm real_plus_binom_times2}),
1503 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1505 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
1507 Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1508 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1509 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1510 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1512 Rule.Thm ("mult_assoc", TermC.num_str @{thm mult.assoc}),
1513 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1514 Rule.Rls_ order_mult_rls_,
1515 (*Rule.Rls_ order_add_rls_,*)
1517 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1518 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1519 Rule.Calc ("Atools.pow", eval_binop "#power_"),
1521 Rule.Thm ("sym_realpow_twoI",
1522 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1523 (*"r1 * r1 = r1 ^^^ 2"*)
1524 Rule.Thm ("sym_real_mult_2",
1525 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1526 (*"z1 + z1 = 2 * z1"*)
1527 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1528 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1530 Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1531 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1532 Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1533 (*"[| l is_const; m is_const |] ==>
1534 l * n + (m * n + k) = (l + m) * n + k"*)
1535 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1536 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1537 Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1538 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1540 Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
1541 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1543 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1544 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1545 Rule.Calc ("Atools.pow", eval_binop "#power_"),
1547 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
1548 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
1549 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left})(*0 + z = z*)
1551 (*Rule.Rls_ order_add_rls_*)
1554 scr = Rule.EmptyScr};
1557 ML {* val prep_rls' = LTool.prep_rls @{theory} *}
1559 setup {* KEStore_Elems.add_rlss
1560 [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
1561 ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*)
1562 ("expand", (Context.theory_name @{theory}, prep_rls' expand)),
1563 ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)),
1564 ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
1566 ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)),
1567 ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)),
1568 ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)),
1569 ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)),
1570 ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
1572 ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)),
1573 ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)),
1574 ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)),
1575 ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)),
1576 ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
1578 ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)),
1579 ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)),
1580 ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)),
1581 ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)),
1582 ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
1584 ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)),
1585 ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)),
1586 ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)),
1587 ("make_rat_poly_with_parentheses",
1588 (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))] *}
1589 setup {* KEStore_Elems.add_calcs
1590 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
1591 eval_is_polyrat_in "#eval_is_polyrat_in")),
1592 ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
1593 ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
1594 ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
1595 ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
1596 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
1597 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))] *}
1600 setup {* KEStore_Elems.add_pbts
1601 [(Specify.prep_pbt thy "pbl_simp_poly" [] Celem.e_pblID
1602 (["polynomial","simplification"],
1603 [("#Given" ,["Term t_t"]),
1604 ("#Where" ,["t_t is_polyexp"]),
1605 ("#Find" ,["normalform n_n"])],
1606 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)
1607 Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1608 SOME "Simplify t_t",
1609 [["simplification","for_polynomials"]]))] *}
1615 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
1617 "simplify term = ((Rewrite_Set norm_Poly False) term)"
1620 setup {* KEStore_Elems.add_mets
1621 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
1622 (["simplification","for_polynomials"],
1623 [("#Given" ,["Term t_t"]),
1624 ("#Where" ,["t_t is_polyexp"]),
1625 ("#Find" ,["normalform n_n"])],
1626 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls,
1627 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
1628 [(*for preds in where_*)
1629 Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1630 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
1631 "Script SimplifyScript (t_t::real) = " ^
1632 " ((Rewrite_Set norm_Poly False) t_t)")]