cleanup, naming: 'KEStore_Elems' in Tests now 'Test_KEStore_Elems', 'store_pbts' now 'add_pbts'
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 axiomatization where (*.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)" and
35 realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
36 realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
37 realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
39 realpow_oneI: "r ^^^ 1 = r" and
40 realpow_zeroI: "r ^^^ 0 = 1" and
41 realpow_eq_oneI: "1 ^^^ n = 1" and
42 realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
43 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
44 (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
45 realpow_minus_oneI: "-1 ^^^ (2 * n) = 1" and
47 realpow_twoI: "r ^^^ 2 = r * r" and
48 realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
49 realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
50 realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
51 realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
52 realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
53 realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
54 realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
55 realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
56 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
57 ==> r ^^^ n = r * r ^^^ (n + -1)" and
58 realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
61 realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
62 realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
66 real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
67 real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
68 real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
69 real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
70 real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
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" and
73 real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
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)" and
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)" and
88 real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
89 real_diff_minus: "a - b = a + -1 * b" and
90 real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
91 real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
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)" and
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" and
98 real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
99 real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
100 real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
101 real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
102 real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
103 real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
104 real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
105 real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
106 real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
107 real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
109 real_num_collect: "[| l is_const; m is_const |] ==>
110 l * n + m * n = (l + m) * n" and
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" and
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" and
120 real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
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" and
125 real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
126 real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
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" and
131 real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
132 real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
134 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
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)
175 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
176 fun is_polyrat_in t v =
177 let fun coeff_in c v = member op = (vars c) v;
178 fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
179 (* at the moment there is no term like this, but ....*)
180 | finddivide (t as (Const ("Fields.inverse_class.divide",_) $ _ $ b)) v =
182 | finddivide (_ $ t1 $ t2) v =
183 (finddivide t1 v) orelse (finddivide t2 v)
184 | finddivide (_ $ t1) v = (finddivide t1 v)
185 | finddivide _ _ = false;
186 in finddivide t v end;
188 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
190 then SOME ((term2str p) ^ " = True",
191 Trueprop $ (mk_equality (p, @{term True})))
192 else SOME ((term2str p) ^ " = True",
193 Trueprop $ (mk_equality (p, @{term False})))
194 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
197 (*.a 'c is coefficient of v' if v does NOT occur in c.*)
198 fun coeff_in c v = not (member op = (vars c) v);
199 (* FIXME.WN100826 shift this into test--------------
200 val v = (term_of o the o (parse thy)) "x";
201 val t = (term_of o the o (parse thy)) "1";
203 (*val it = true : bool*)
204 val t = (term_of o the o (parse thy)) "a*b+c";
206 (*val it = true : bool*)
207 val t = (term_of o the o (parse thy)) "a*x+c";
209 (*val it = false : bool*)
210 ----------------------------------------------------*)
211 (*. a 'monomial t in variable v' is a term t with
212 either (1) v NOT existent in t, or (2) v contained in t,
214 if (2) then v is a factor on the very right, ev. with exponent.*)
215 fun factor_right_deg (*case 2*)
216 (t as Const ("Groups.times_class.times",_) $ t1 $
217 (Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
218 if ((vv = v) andalso (coeff_in t1 v)) then SOME (int_of_str' d) else NONE
219 | factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
220 if (vv = v) then SOME (int_of_str' d) else NONE
221 | factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v =
222 if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
223 | factor_right_deg vv v =
224 if (vv = v) then SOME 1 else NONE;
225 fun mono_deg_in m v =
226 if coeff_in m v then (*case 1*) SOME 0
227 else factor_right_deg m v;
228 (* FIXME.WN100826 shift this into test-----------------------------
229 val v = (term_of o the o (parse thy)) "x";
230 val t = (term_of o the o (parse thy)) "(a*b+c)*x^^^7";
233 val t = (term_of o the o (parse thy)) "x^^^7";
236 val t = (term_of o the o (parse thy)) "(a*b+c)*x";
239 val t = (term_of o the o (parse thy)) "(a*b+x)*x";
242 val t = (term_of o the o (parse thy)) "x";
245 val t = (term_of o the o (parse thy)) "(a*b+c)";
248 val t = (term_of o the o (parse thy)) "ab - (a*b)*x";
251 ------------------------------------------------------------------*)
252 fun expand_deg_in t v =
253 let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
254 (case mono_deg_in t2 v of (* $ is left associative*)
255 SOME d' => edi d' d' t1
257 | edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
258 (case mono_deg_in t2 v of
259 SOME d' => edi d' d' t1
261 | edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
262 (case mono_deg_in t2 v of
263 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
264 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
265 then edi d' dmax t1 else NONE
267 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
268 (case mono_deg_in t2 v of
269 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
270 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
271 then edi d' dmax t1 else NONE
273 | edi ~1 ~1 t = (case mono_deg_in t v of
276 | edi d dmax t = (*basecase last*)
277 (case mono_deg_in t v of
278 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
279 then SOME dmax else NONE
282 (* FIXME.WN100826 shift this into test-----------------------------
283 val v = (term_of o the o (parse thy)) "x";
284 val t = (term_of o the o (parse thy)) "a+b";
287 val t = (term_of o the o (parse thy)) "(a+b)*x";
290 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x";
293 val t = (term_of o the o (parse thy)) "a*b + (a-b)*x";
296 val t = (term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
298 -------------------------------------------------------------------*)
299 fun poly_deg_in t v =
300 let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
301 (case mono_deg_in t2 v of (* $ is left associative*)
302 SOME d' => edi d' d' t1
304 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
305 (case mono_deg_in t2 v of
306 (*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
307 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
308 then edi d' dmax t1 else NONE
310 | edi ~1 ~1 t = (case mono_deg_in t v of
313 | edi d dmax t = (*basecase last*)
314 (case mono_deg_in t v of
315 SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
316 then SOME dmax else NONE
321 fun is_expanded_in t v =
322 case expand_deg_in t v of SOME _ => true | NONE => false;
324 case poly_deg_in t v of SOME _ => true | NONE => false;
325 fun has_degree_in t v =
326 case expand_deg_in t v of SOME d => d | NONE => ~1;
328 (* FIXME.WN100826 shift this into test-----------------------------
329 val v = (term_of o the o (parse thy)) "x";
330 val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
333 val t = (term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
336 val t = (term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
339 -------------------------------------------------------------------*)
341 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
342 fun eval_is_expanded_in _ _
343 (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
344 if is_expanded_in t v
345 then SOME ((term2str p) ^ " = True",
346 Trueprop $ (mk_equality (p, @{term True})))
347 else SOME ((term2str p) ^ " = True",
348 Trueprop $ (mk_equality (p, @{term False})))
349 | eval_is_expanded_in _ _ _ _ = NONE;
351 val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
352 val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
353 (*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
355 (*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
358 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
359 fun eval_is_poly_in _ _
360 (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
362 then SOME ((term2str p) ^ " = True",
363 Trueprop $ (mk_equality (p, @{term True})))
364 else SOME ((term2str p) ^ " = True",
365 Trueprop $ (mk_equality (p, @{term False})))
366 | eval_is_poly_in _ _ _ _ = NONE;
368 val t = (term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
369 val SOME (id, t') = eval_is_poly_in 0 0 t 0;
370 (*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
372 (*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
375 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
376 fun eval_has_degree_in _ _
377 (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
378 let val d = has_degree_in t v
379 val d' = term_of_num HOLogic.realT d
380 in SOME ((term2str p) ^ " = " ^ (string_of_int d),
381 Trueprop $ (mk_equality (p, d')))
383 | eval_has_degree_in _ _ _ _ = NONE;
385 > val t = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
386 > val SOME (id, t') = eval_has_degree_in 0 0 t 0;
387 val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
389 val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
394 append_rls "calculate_PolyFIXXXME.not.impl." e_rls
397 (*.for evaluation of conditions in rewrite rules.*)
398 val Poly_erls = append_rls "Poly_erls" Atools_erls
399 [Calc ("HOL.eq", eval_equal "#equal_"),
400 Thm ("real_unari_minus", num_str @{thm real_unari_minus}),
401 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
402 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
403 Calc ("Groups.times_class.times", eval_binop "#mult_"),
404 Calc ("Atools.pow", eval_binop "#power_")];
406 val poly_crls = append_rls "poly_crls" Atools_crls
407 [Calc ("HOL.eq", eval_equal "#equal_"),
408 Thm ("real_unari_minus", num_str @{thm real_unari_minus}),
409 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
410 Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
411 Calc ("Groups.times_class.times", eval_binop "#mult_"),
412 Calc ("Atools.pow" ,eval_binop "#power_")];
414 local (*. for make_polynomial .*)
416 open Term; (* for type order = EQUAL | LESS | GREATER *)
418 fun pr_ord EQUAL = "EQUAL"
419 | pr_ord LESS = "LESS"
420 | pr_ord GREATER = "GREATER";
422 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
424 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
425 | _ => (((a, 0), T), 0))
426 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
427 | dest_hd' (Var v) = (v, 2)
428 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
429 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
431 fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
432 (case int_of_str (order) of
435 | get_order_pow _ = 0;
437 fun size_of_term' (Const(str,_) $ t) =
438 if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
439 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
440 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
441 | size_of_term' _ = 1;
443 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
444 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
445 | term_ord' pr thy (t, u) =
448 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
449 val _ = tracing ("t= f@ts= \"" ^ term_to_string''' thy f ^ "\" @ \"[" ^
450 commas (map (term_to_string''' thy) ts) ^ "]\"");
451 val _ = tracing("u= g@us= \"" ^ term_to_string''' thy g ^ "\" @ \"[" ^
452 commas (map (term_to_string''' thy) us) ^ "]\"");
453 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
454 string_of_int (size_of_term' u) ^ ")");
455 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
456 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
457 val _ = tracing ("-------");
460 case int_ord (size_of_term' t, size_of_term' u) of
462 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
463 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
467 and hd_ord (f, g) = (* ~ term.ML *)
468 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
469 and terms_ord str pr (ts, us) =
470 list_ord (term_ord' pr (assoc_thy "Isac"))(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 = [], rew_ord = ("dummy_ord", dummy_ord),
488 erls = e_rls,srls = Erls, calc = [], errpatts = [],
489 rules = [Thm ("distrib_right" ,num_str @{thm distrib_right}),
490 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
491 Thm ("distrib_left",num_str @{thm distrib_left})
492 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
493 ], scr = EmptyScr}:rls;
495 (*----------------- Begin: rulesets for make_polynomial_ -----------------
496 'rlsIDs' redefined by MG as 'rlsIDs_'
500 Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", dummy_ord),
501 erls = e_rls, srls = Erls, calc = [], errpatts = [],
503 [Thm ("real_diff_minus", num_str @{thm real_diff_minus}),
504 (*"a - b = a + -1 * b"*)
505 Thm ("sym_real_mult_minus1", num_str (@{thm real_mult_minus1} RS @{thm sym}))
506 (*- ?z = "-1 * ?z"*)],
510 Rls{id = "expand_poly_", preconds = [],
511 rew_ord = ("dummy_ord", dummy_ord),
512 erls = e_rls,srls = Erls,
513 calc = [], errpatts = [],
515 [Thm ("real_plus_binom_pow4",num_str @{thm real_plus_binom_pow4}),
516 (*"(a + b)^^^4 = ... "*)
517 Thm ("real_plus_binom_pow5",num_str @{thm real_plus_binom_pow5}),
518 (*"(a + b)^^^5 = ... "*)
519 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
520 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
521 (*WN071229 changed/removed for Schaerding -----vvv*)
522 (*Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),*)
523 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
524 Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
525 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
526 (*Thm ("real_plus_minus_binom1_p_p", num_str @{thm real_plus_minus_binom1_p_p}),*)
527 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
528 (*Thm ("real_plus_minus_binom2_p_p", num_str @{thm real_plus_minus_binom2_p_p}),*)
529 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
530 (*WN071229 changed/removed for Schaerding -----^^^*)
532 Thm ("distrib_right" ,num_str @{thm distrib_right}),
533 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
534 Thm ("distrib_left",num_str @{thm distrib_left}),
535 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
537 Thm ("realpow_multI", num_str @{thm realpow_multI}),
538 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
539 Thm ("realpow_pow",num_str @{thm realpow_pow})
540 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
541 ], scr = EmptyScr}:rls;
543 (*.the expression contains + - * ^ only ?
544 this is weaker than 'is_polynomial' !.*)
545 fun is_polyexp (Free _) = true
546 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
547 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
548 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
549 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
550 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
551 ((is_polyexp t1) andalso (is_polyexp t2))
552 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
553 ((is_polyexp t1) andalso (is_polyexp t2))
554 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
555 ((is_polyexp t1) andalso (is_polyexp t2))
556 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
557 ((is_polyexp t1) andalso (is_polyexp t2))
558 | is_polyexp _ = false;
560 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
561 fun eval_is_polyexp (thmid:string) _
562 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
564 then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
565 Trueprop $ (mk_equality (t, @{term True})))
566 else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
567 Trueprop $ (mk_equality (t, @{term False})))
568 | eval_is_polyexp _ _ _ _ = NONE;
570 val expand_poly_rat_ =
571 Rls{id = "expand_poly_rat_", preconds = [],
572 rew_ord = ("dummy_ord", dummy_ord),
573 erls = append_rls "e_rls-is_polyexp" e_rls
574 [Calc ("Poly.is'_polyexp", eval_is_polyexp "")
577 calc = [], errpatts = [],
579 [Thm ("real_plus_binom_pow4_poly", num_str @{thm real_plus_binom_pow4_poly}),
580 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
581 Thm ("real_plus_binom_pow5_poly", num_str @{thm real_plus_binom_pow5_poly}),
582 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
583 Thm ("real_plus_binom_pow2_poly",num_str @{thm real_plus_binom_pow2_poly}),
584 (*"[| a is_polyexp; b is_polyexp |] ==>
585 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
586 Thm ("real_plus_binom_pow3_poly",num_str @{thm real_plus_binom_pow3_poly}),
587 (*"[| a is_polyexp; b is_polyexp |] ==>
588 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
589 Thm ("real_plus_minus_binom1_p_p",num_str @{thm real_plus_minus_binom1_p_p}),
590 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
591 Thm ("real_plus_minus_binom2_p_p",num_str @{thm real_plus_minus_binom2_p_p}),
592 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
594 Thm ("real_add_mult_distrib_poly",
595 num_str @{thm real_add_mult_distrib_poly}),
596 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
597 Thm("real_add_mult_distrib2_poly",
598 num_str @{thm real_add_mult_distrib2_poly}),
599 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
601 Thm ("realpow_multI_poly", num_str @{thm realpow_multI_poly}),
602 (*"[| r is_polyexp; s is_polyexp |] ==>
603 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
604 Thm ("realpow_pow",num_str @{thm realpow_pow})
605 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
606 ], scr = EmptyScr}:rls;
608 val simplify_power_ =
609 Rls{id = "simplify_power_", preconds = [],
610 rew_ord = ("dummy_ord", dummy_ord),
611 erls = e_rls, srls = Erls,
612 calc = [], errpatts = [],
613 rules = [(*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
614 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
615 Thm ("sym_realpow_twoI",
616 num_str (@{thm realpow_twoI} RS @{thm sym})),
617 (*"r * r = r ^^^ 2"*)
618 Thm ("realpow_twoI_assoc_l",num_str @{thm realpow_twoI_assoc_l}),
619 (*"r * (r * s) = r ^^^ 2 * s"*)
621 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
622 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
623 Thm ("realpow_plus_1_assoc_l",
624 num_str @{thm realpow_plus_1_assoc_l}),
625 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
626 (*MG 9.7.03: neues Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
627 Thm ("realpow_plus_1_assoc_l2",
628 num_str @{thm realpow_plus_1_assoc_l2}),
629 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
631 Thm ("sym_realpow_addI",
632 num_str (@{thm realpow_addI} RS @{thm sym})),
633 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
634 Thm ("realpow_addI_assoc_l",num_str @{thm realpow_addI_assoc_l}),
635 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
637 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
638 "r * r = r ^^^ 2" wenn r=a^^^b*)
639 Thm ("realpow_pow",num_str @{thm realpow_pow})
640 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
641 ], scr = EmptyScr}:rls;
643 val calc_add_mult_pow_ =
644 Rls{id = "calc_add_mult_pow_", preconds = [],
645 rew_ord = ("dummy_ord", dummy_ord),
646 erls = Atools_erls(*erls3.4.03*),srls = Erls,
647 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
648 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
649 ("POWER", ("Atools.pow", eval_binop "#power_"))
652 rules = [Calc ("Groups.plus_class.plus", eval_binop "#add_"),
653 Calc ("Groups.times_class.times", eval_binop "#mult_"),
654 Calc ("Atools.pow", eval_binop "#power_")
655 ], scr = EmptyScr}:rls;
657 val reduce_012_mult_ =
658 Rls{id = "reduce_012_mult_", preconds = [],
659 rew_ord = ("dummy_ord", dummy_ord),
660 erls = e_rls,srls = Erls,
661 calc = [], errpatts = [],
662 rules = [(* MG: folgende Thm müssen hier stehen bleiben: *)
663 Thm ("mult_1_right",num_str @{thm mult_1_right}),
664 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
665 Thm ("realpow_zeroI",num_str @{thm realpow_zeroI}),
666 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
667 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
669 Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
671 ], scr = EmptyScr}:rls;
673 val collect_numerals_ =
674 Rls{id = "collect_numerals_", preconds = [],
675 rew_ord = ("dummy_ord", dummy_ord),
676 erls = Atools_erls, srls = Erls,
677 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
680 [Thm ("real_num_collect",num_str @{thm real_num_collect}),
681 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
682 Thm ("real_num_collect_assoc_r",num_str @{thm real_num_collect_assoc_r}),
683 (*"[| l is_const; m is_const |] ==> \
684 \(k + m * n) + l * n = k + (l + m)*n"*)
685 Thm ("real_one_collect",num_str @{thm real_one_collect}),
686 (*"m is_const ==> n + m * n = (1 + m) * n"*)
687 Thm ("real_one_collect_assoc_r",num_str @{thm real_one_collect_assoc_r}),
688 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
690 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
692 (*MG: Reihenfolge der folgenden 2 Thm muss so bleiben, wegen
693 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
694 Thm ("real_mult_2_assoc_r",num_str @{thm real_mult_2_assoc_r}),
695 (*"(k + z1) + z1 = k + 2 * z1"*)
696 Thm ("sym_real_mult_2",num_str (@{thm real_mult_2} RS @{thm sym}))
697 (*"z1 + z1 = 2 * z1"*)
698 ], scr = EmptyScr}:rls;
701 Rls{id = "reduce_012_", preconds = [],
702 rew_ord = ("dummy_ord", dummy_ord),
703 erls = e_rls,srls = Erls, calc = [], errpatts = [],
704 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
706 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
708 Thm ("mult_zero_right",num_str @{thm mult_zero_right}),
710 Thm ("add_0_left",num_str @{thm add_0_left}),
712 Thm ("add_0_right",num_str @{thm add_0_right}),
713 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
715 (*Thm ("realpow_oneI",num_str @{thm realpow_oneI})*)
717 Thm ("divide_zero_left",num_str @{thm divide_zero_left})(*WN060914*)
719 ], scr = EmptyScr}:rls;
721 val discard_parentheses1 =
722 append_rls "discard_parentheses1" e_rls
723 [Thm ("sym_mult_assoc",
724 num_str (@{thm mult_assoc} RS @{thm sym}))
725 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
726 (*Thm ("sym_add_assoc",
727 num_str (@{thm add_assoc} RS @{thm sym}))*)
728 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
731 (*----------------- End: rulesets for make_polynomial_ -----------------*)
733 (*MG.0401 ev. for use in rls with ordered rewriting ?
734 val collect_numerals_left =
735 Rls{id = "collect_numerals", preconds = [],
736 rew_ord = ("dummy_ord", dummy_ord),
737 erls = Atools_erls(*erls3.4.03*),srls = Erls,
738 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
739 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
740 ("POWER", ("Atools.pow", eval_binop "#power_"))
743 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}),
744 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
745 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
746 (*"[| l is_const; m is_const |] ==>
747 l * n + (m * n + k) = (l + m) * n + k"*)
748 Thm ("real_one_collect",num_str @{thm real_one_collect}),
749 (*"m is_const ==> n + m * n = (1 + m) * n"*)
750 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
751 (*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
753 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
755 (*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
756 Thm ("sym_real_mult_2",
757 num_str (@{thm real_mult_2} RS @{thm sym})),
758 (*"z1 + z1 = 2 * z1"*)
759 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
760 (*"z1 + (z1 + k) = 2 * z1 + k"*)
761 ], scr = EmptyScr}:rls;*)
764 Rls{id = "expand_poly", preconds = [],
765 rew_ord = ("dummy_ord", dummy_ord),
766 erls = e_rls,srls = Erls,
767 calc = [], errpatts = [],
769 rules = [Thm ("distrib_right" ,num_str @{thm distrib_right}),
770 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
771 Thm ("distrib_left",num_str @{thm distrib_left}),
772 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
773 (*Thm ("distrib_right1",num_str @{thm distrib_right}1),
774 ....... 18.3.03 undefined???*)
776 Thm ("real_plus_binom_pow2",num_str @{thm real_plus_binom_pow2}),
777 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
778 Thm ("real_minus_binom_pow2_p",num_str @{thm real_minus_binom_pow2_p}),
779 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
780 Thm ("real_plus_minus_binom1_p",
781 num_str @{thm real_plus_minus_binom1_p}),
782 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
783 Thm ("real_plus_minus_binom2_p",
784 num_str @{thm real_plus_minus_binom2_p}),
785 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
787 Thm ("minus_minus",num_str @{thm minus_minus}),
789 Thm ("real_diff_minus",num_str @{thm real_diff_minus}),
790 (*"a - b = a + -1 * b"*)
791 Thm ("sym_real_mult_minus1",
792 num_str (@{thm real_mult_minus1} RS @{thm sym}))
795 (*Thm ("real_minus_add_distrib",
796 num_str @{thm real_minus_add_distrib}),*)
797 (*"- (?x + ?y) = - ?x + - ?y"*)
798 (*Thm ("real_diff_plus",num_str @{thm real_diff_plus})*)
800 ], scr = EmptyScr}:rls;
803 Rls{id = "simplify_power", preconds = [],
804 rew_ord = ("dummy_ord", dummy_ord),
805 erls = e_rls, srls = Erls,
806 calc = [], errpatts = [],
807 rules = [Thm ("realpow_multI", num_str @{thm realpow_multI}),
808 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
810 Thm ("sym_realpow_twoI",
811 num_str( @{thm realpow_twoI} RS @{thm sym})),
812 (*"r1 * r1 = r1 ^^^ 2"*)
813 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
814 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
815 Thm ("realpow_pow",num_str @{thm realpow_pow}),
816 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
817 Thm ("sym_realpow_addI",
818 num_str (@{thm realpow_addI} RS @{thm sym})),
819 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
820 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),
822 Thm ("realpow_eq_oneI",num_str @{thm realpow_eq_oneI})
824 ], scr = EmptyScr}:rls;
825 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
826 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
828 Rls{id = "order_add_mult", preconds = [],
829 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
830 erls = e_rls,srls = Erls,
831 calc = [], errpatts = [],
832 rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
834 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
835 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
836 Thm ("mult_assoc",num_str @{thm mult_assoc}),
837 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
838 Thm ("add_commute",num_str @{thm add_commute}),
840 Thm ("add_left_commute",num_str @{thm add_left_commute}),
841 (*x + (y + z) = y + (x + z)*)
842 Thm ("add_assoc",num_str @{thm add_assoc})
843 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
844 ], scr = EmptyScr}:rls;
845 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
846 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
848 Rls{id = "order_mult", preconds = [],
849 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
850 erls = e_rls,srls = Erls,
851 calc = [], errpatts = [],
852 rules = [Thm ("mult_commute",num_str @{thm mult_commute}),
854 Thm ("real_mult_left_commute",num_str @{thm real_mult_left_commute}),
855 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
856 Thm ("mult_assoc",num_str @{thm mult_assoc})
857 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
858 ], scr = EmptyScr}:rls;
862 val collect_numerals =
863 Rls{id = "collect_numerals", preconds = [],
864 rew_ord = ("dummy_ord", dummy_ord),
865 erls = Atools_erls(*erls3.4.03*),srls = Erls,
866 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
867 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
868 ("POWER", ("Atools.pow", eval_binop "#power_"))
870 rules = [Thm ("real_num_collect",num_str @{thm real_num_collect}),
871 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
872 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
873 (*"[| l is_const; m is_const |] ==>
874 l * n + (m * n + k) = (l + m) * n + k"*)
875 Thm ("real_one_collect",num_str @{thm real_one_collect}),
876 (*"m is_const ==> n + m * n = (1 + m) * n"*)
877 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
878 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
879 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
880 Calc ("Groups.times_class.times", eval_binop "#mult_"),
881 Calc ("Atools.pow", eval_binop "#power_")
882 ], scr = EmptyScr}:rls;
884 Rls{id = "reduce_012", preconds = [],
885 rew_ord = ("dummy_ord", dummy_ord),
886 erls = e_rls,srls = Erls,
887 calc = [], errpatts = [],
888 rules = [Thm ("mult_1_left",num_str @{thm mult_1_left}),
890 (*Thm ("real_mult_minus1",num_str @{thm real_mult_minus1}),14.3.03*)
892 Thm ("minus_mult_left",
893 num_str (@{thm minus_mult_left} RS @{thm sym})),
894 (*- (?x * ?y) = "- ?x * ?y"*)
895 (*Thm ("real_minus_mult_cancel",
896 num_str @{thm real_minus_mult_cancel}),
897 (*"- ?x * - ?y = ?x * ?y"*)---*)
898 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
900 Thm ("add_0_left",num_str @{thm add_0_left}),
902 Thm ("right_minus",num_str @{thm right_minus}),
904 Thm ("sym_real_mult_2",
905 num_str (@{thm real_mult_2} RS @{thm sym})),
906 (*"z1 + z1 = 2 * z1"*)
907 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc})
908 (*"z1 + (z1 + k) = 2 * z1 + k"*)
909 ], scr = EmptyScr}:rls;
911 val discard_parentheses =
912 append_rls "discard_parentheses" e_rls
913 [Thm ("sym_mult_assoc",
914 num_str (@{thm mult_assoc} RS @{thm sym})),
915 Thm ("sym_add_assoc",
916 num_str (@{thm add_assoc} RS @{thm sym}))];
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 Seq{id = "make_polynomial", preconds = []:term list,
958 rew_ord = ("dummy_ord", dummy_ord),
959 erls = Atools_erls, srls = Erls,
960 calc = [], errpatts = [],
961 rules = [Rls_ expand_poly,
963 Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
964 Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
966 Thm ("realpow_oneI",num_str @{thm realpow_oneI}),(*in --^*)
967 Rls_ discard_parentheses
972 val scr_expand_binoms =
973 "Script Expand_binoms t_t =" ^
975 "((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
976 " (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
977 " (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
978 " (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
979 " (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
980 " (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
982 " (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
983 " (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
984 " (Try (Repeat (Rewrite add_0_left False))) @@ " ^
986 " (Try (Repeat (Calculate PLUS ))) @@ " ^
987 " (Try (Repeat (Calculate TIMES ))) @@ " ^
988 " (Try (Repeat (Calculate POWER))) @@ " ^
990 " (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
991 " (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
992 " (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
993 " (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
995 " (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
996 " (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
998 " (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
999 " (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
1001 " (Try (Repeat (Calculate PLUS ))) @@ " ^
1002 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1003 " (Try (Repeat (Calculate POWER)))) " ^
1007 Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1008 erls = Atools_erls, srls = Erls,
1009 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1010 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1011 ("POWER", ("Atools.pow", eval_binop "#power_"))
1013 rules = [Thm ("real_plus_binom_pow2",
1014 num_str @{thm real_plus_binom_pow2}),
1015 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1016 Thm ("real_plus_binom_times",
1017 num_str @{thm real_plus_binom_times}),
1018 (*"(a + b)*(a + b) = ...*)
1019 Thm ("real_minus_binom_pow2",
1020 num_str @{thm real_minus_binom_pow2}),
1021 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1022 Thm ("real_minus_binom_times",
1023 num_str @{thm real_minus_binom_times}),
1024 (*"(a - b)*(a - b) = ...*)
1025 Thm ("real_plus_minus_binom1",
1026 num_str @{thm real_plus_minus_binom1}),
1027 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1028 Thm ("real_plus_minus_binom2",
1029 num_str @{thm real_plus_minus_binom2}),
1030 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1032 Thm ("real_pp_binom_times",num_str @{thm real_pp_binom_times}),
1033 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1034 Thm ("real_pm_binom_times",num_str @{thm real_pm_binom_times}),
1035 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1036 Thm ("real_mp_binom_times",num_str @{thm real_mp_binom_times}),
1037 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1038 Thm ("real_mm_binom_times",num_str @{thm real_mm_binom_times}),
1039 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1040 Thm ("realpow_multI",num_str @{thm realpow_multI}),
1041 (*(a*b)^^^n = a^^^n * b^^^n*)
1042 Thm ("real_plus_binom_pow3",num_str @{thm real_plus_binom_pow3}),
1043 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1044 Thm ("real_minus_binom_pow3",
1045 num_str @{thm real_minus_binom_pow3}),
1046 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1049 (*Thm ("distrib_right" ,num_str @{thm distrib_right}),
1050 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1051 Thm ("distrib_left",num_str @{thm distrib_left}),
1052 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1053 Thm ("left_diff_distrib" ,num_str @{thm left_diff_distrib}),
1054 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1055 Thm ("right_diff_distrib",num_str @{thm right_diff_distrib}),
1056 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1058 Thm ("mult_1_left",num_str @{thm mult_1_left}),
1060 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),
1062 Thm ("add_0_left",num_str @{thm add_0_left}),(*"0 + z = z"*)
1064 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1065 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1066 Calc ("Atools.pow", eval_binop "#power_"),
1067 (*Thm ("mult_commute",num_str @{thm mult_commute}),
1069 Thm ("real_mult_left_commute",
1070 num_str @{thm real_mult_left_commute}),
1071 Thm ("mult_assoc",num_str @{thm mult_assoc}),
1072 Thm ("add_commute",num_str @{thm add_commute}),
1073 Thm ("add_left_commute",num_str @{thm add_left_commute}),
1074 Thm ("add_assoc",num_str @{thm add_assoc}),
1076 Thm ("sym_realpow_twoI",
1077 num_str (@{thm realpow_twoI} RS @{thm sym})),
1078 (*"r1 * r1 = r1 ^^^ 2"*)
1079 Thm ("realpow_plus_1",num_str @{thm realpow_plus_1}),
1080 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1081 (*Thm ("sym_real_mult_2",
1082 num_str (@{thm real_mult_2} RS @{thm sym})),
1083 (*"z1 + z1 = 2 * z1"*)*)
1084 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1085 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1087 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1088 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
1089 Thm ("real_num_collect_assoc",
1090 num_str @{thm real_num_collect_assoc}),
1091 (*"[| l is_const; m is_const |] ==>
1092 l * n + (m * n + k) = (l + m) * n + k"*)
1093 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1094 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1095 Thm ("real_one_collect_assoc",
1096 num_str @{thm real_one_collect_assoc}),
1097 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1099 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1100 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1101 Calc ("Atools.pow", eval_binop "#power_")
1103 scr = Prog ((term_of o the o (parse thy)) scr_expand_binoms)
1107 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
1109 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
1110 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
1111 (* Polynom --> List von Monomen *)
1112 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
1113 (poly2list t1) @ (poly2list t2)
1114 | poly2list t = [t];
1116 (* Monom --> Liste von Variablen *)
1117 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
1118 (monom2list t1) @ (monom2list t2)
1119 | monom2list t = [t];
1121 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
1122 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
1123 | get_basStr (Free (str, _)) = str
1124 | get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
1126 error("get_basStr: called with t= "^(term2str t));*)
1128 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
1129 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
1130 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
1131 | get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
1132 | get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
1134 error("get_potStr: called with t= "^(term2str t));*)
1136 (* Umgekehrte string_ord *)
1137 val string_ord_rev = rev_order o string_ord;
1139 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
1140 innerhalb eines Monomes:
1141 - zuerst lexikographisch nach Variablenname
1142 - wenn gleich: nach steigender Potenz *)
1143 fun var_ord (a,b: term) = prod_ord string_ord string_ord
1144 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1146 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
1147 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
1148 - zuerst lexikographisch nach Variablenname
1149 - wenn gleich: nach sinkender Potenz*)
1150 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
1151 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
1154 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
1155 val sort_varList = sort var_ord;
1157 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
1158 Argumente in eine Liste *)
1159 fun args u : term list =
1160 let fun stripc (f$t, ts) = stripc (f, t::ts)
1161 | stripc (t as Free _, ts) = (t::ts)
1162 | stripc (_, ts) = ts
1163 in stripc (u, []) end;
1165 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
1166 (keine Variablen) enthaelt *)
1167 fun filter_num [] = true
1168 | filter_num [Free x] = if (is_num (Free x)) then true
1170 | filter_num ((Free _)::_) = false
1172 (filter_num o (filter_out is_num) o flat o (map args)) ts;
1174 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
1175 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
1176 fun is_nums t = filter_num [t];
1178 (* Berechnet den Gesamtgrad eines Monoms *)
1180 fun counter (n, []) = n
1181 | counter (n, x :: xs) =
1186 (Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
1187 if (is_nums (Free (str_h, T))) then
1188 counter (n + (the (int_of_str str_h)), xs)
1189 else counter (n + 1000, xs) (*FIXME.MG?!*)
1190 | (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
1191 counter (n + 1000, xs) (*FIXME.MG?!*)
1192 | (Free (str, _)) => counter (n + 1, xs)
1193 (*| _ => error("monom_degree: called with factor: "^(term2str x)))*)
1194 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
1196 fun monom_degree l = counter (0, l)
1199 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
1200 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
1201 werden jedoch dabei ignoriert (uebersprungen) *)
1202 fun dict_cond_ord _ _ ([], []) = EQUAL
1203 | dict_cond_ord _ _ ([], _ :: _) = LESS
1204 | dict_cond_ord _ _ (_ :: _, []) = GREATER
1205 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
1206 (case (cond x, cond y) of
1207 (false, false) => (case elem_ord (x, y) of
1208 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
1210 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
1211 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
1212 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
1214 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
1215 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
1216 dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
1217 fun degree_ord (xs, ys) =
1218 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
1219 ((monom_degree xs, xs), (monom_degree ys, ys));
1221 fun hd_str str = substring (str, 0, 1);
1222 fun tl_str str = substring (str, 1, (size str) - 1);
1224 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
1225 fun get_koeff_of_mon [] = error("get_koeff_of_mon: called with l = []")
1226 | get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
1229 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
1230 fun koeff2ordStr (SOME x) = (case x of
1232 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
1234 | _ => "aaa") (* "num.Ausdruck" --> gross *)
1235 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
1237 (* Order zum Vergleich von Koeffizienten (strings):
1238 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
1239 fun compare_koeff_ord (xs, ys) =
1240 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
1241 (koeff2ordStr o get_koeff_of_mon) ys);
1243 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
1244 fun koeff_degree_ord (xs, ys) =
1245 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
1247 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
1248 Gesamtgradordnung *)
1249 val sort_monList = sort koeff_degree_ord;
1251 (* Alternativ zu degree_ord koennte auch die viel einfachere und
1252 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
1253 fuer unsere Zwecke geeignet!
1255 fun simple_ord (al,bl: term list) = dict_ord string_ord
1256 (map get_basStr al, map get_basStr bl);
1258 val sort_monList = sort simple_ord; *)
1260 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
1261 (mit gewuenschtem Typen T) *)
1262 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
1263 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
1264 fun binop op_ t1 t2 = op_ $ t1 $ t2;
1265 fun create_prod T (a,b) = binop (mult T) a b;
1266 fun create_sum T (a,b) = binop (plus T) a b;
1268 (* löscht letztes Element einer Liste *)
1269 fun drop_last l = take ((length l)-1,l);
1271 (* Liste von Variablen --> Monom *)
1272 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
1274 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
1275 gleiche Monome zusammengefasst werden können (collect_numerals)!
1276 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
1278 (* Liste von Monomen --> Polynom *)
1279 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
1281 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
1282 bessere Darstellung, da keine Klammern sichtbar!
1283 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
1285 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
1286 fun sort_variables t =
1288 val ll = map monom2list (poly2list t);
1289 val lls = map sort_varList ll;
1291 val ls = map (create_monom T) lls;
1292 in create_polynom T ls end;
1294 (* sorts the monoms of an expanded and variable-sorted polynomial
1298 val ll = map monom2list (poly2list t);
1299 val lls = sort_monList ll;
1301 val ls = map (create_monom T) lls;
1302 in create_polynom T ls end;
1304 (* auch Klammerung muss übereinstimmen;
1305 sort_variables klammert Produkte rechtslastig*)
1306 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
1310 fun eval_is_multUnordered (thmid:string) _
1311 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
1312 if is_multUnordered arg
1313 then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
1314 Trueprop $ (mk_equality (t, @{term True})))
1315 else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
1316 Trueprop $ (mk_equality (t, @{term False})))
1317 | eval_is_multUnordered _ _ _ _ = NONE;
1319 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1320 []:(rule * (term * term list)) list;
1321 fun init_state (_:term) = e_rrlsstate;
1322 fun locate_rule (_:rule list list) (_:term) (_:rule) =
1323 ([]:(rule * (term * term list)) list);
1324 fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
1325 fun normal_form t = SOME (sort_variables t,[]:term list);
1328 Rrls {id = "order_mult_",
1330 (* ?p matched with the current term gives an environment,
1331 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1332 [([parse_patt thy "?p is_multUnordered"],
1333 parse_patt thy "?p :: real")],
1334 rew_ord = ("dummy_ord", dummy_ord),
1335 erls = append_rls "e_rls-is_multUnordered" e_rls
1336 [Calc ("Poly.is'_multUnordered",
1337 eval_is_multUnordered "")],
1338 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1339 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1340 ("DIVIDE", ("Fields.inverse_class.divide",
1341 eval_cancel "#divide_e")),
1342 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
1344 scr=Rfuns {init_state = init_state,
1345 normal_form = normal_form,
1346 locate_rule = locate_rule,
1347 next_rule = next_rule,
1348 attach_form = attach_form}};
1349 val order_mult_rls_ =
1350 Rls{id = "order_mult_rls_", preconds = [],
1351 rew_ord = ("dummy_ord", dummy_ord),
1352 erls = e_rls,srls = Erls,
1353 calc = [], errpatts = [],
1354 rules = [Rls_ order_mult_
1355 ], scr = EmptyScr}:rls;
1359 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
1362 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
1363 fun eval_is_addUnordered (thmid:string) _
1364 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
1365 if is_addUnordered arg
1366 then SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
1367 Trueprop $ (mk_equality (t, @{term True})))
1368 else SOME (mk_thmid thmid "" (term_to_string''' thy arg) "",
1369 Trueprop $ (mk_equality (t, @{term False})))
1370 | eval_is_addUnordered _ _ _ _ = NONE;
1372 fun attach_form (_:rule list list) (_:term) (_:term) = (*still missing*)
1373 []:(rule * (term * term list)) list;
1374 fun init_state (_:term) = e_rrlsstate;
1375 fun locate_rule (_:rule list list) (_:term) (_:rule) =
1376 ([]:(rule * (term * term list)) list);
1377 fun next_rule (_:rule list list) (_:term) = (NONE:rule option);
1378 fun normal_form t = SOME (sort_monoms t,[]:term list);
1381 Rrls {id = "order_add_",
1382 prepat = (*WN.18.6.03 Preconditions und Pattern,
1383 die beide passen muessen, damit das Rrls angewandt wird*)
1384 [([parse_patt @{theory} "?p is_addUnordered"],
1385 parse_patt @{theory} "?p :: real"
1386 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1387 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1388 rew_ord = ("dummy_ord", dummy_ord),
1389 erls = append_rls "e_rls-is_addUnordered" e_rls(*MG: poly_erls*)
1390 [Calc ("Poly.is'_addUnordered",
1391 eval_is_addUnordered "")],
1392 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
1393 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
1394 ("DIVIDE",("Fields.inverse_class.divide",
1395 eval_cancel "#divide_e")),
1396 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1398 scr=Rfuns {init_state = init_state,
1399 normal_form = normal_form,
1400 locate_rule = locate_rule,
1401 next_rule = next_rule,
1402 attach_form = attach_form}};
1404 val order_add_rls_ =
1405 Rls{id = "order_add_rls_", preconds = [],
1406 rew_ord = ("dummy_ord", dummy_ord),
1407 erls = e_rls,srls = Erls,
1408 calc = [], errpatts = [],
1409 rules = [Rls_ order_add_
1410 ], scr = EmptyScr}:rls;
1413 text {* rule-set make_polynomial also named norm_Poly:
1414 Rewrite order has not been implemented properly; the order is better in
1415 make_polynomial_in (coded in SML).
1416 Notes on state of development:
1417 \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
1418 \# migration Isabelle2002 --> 2011 weakened the rule set, see test
1419 --- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
1422 (*. see MG-DA.p.52ff .*)
1423 val make_polynomial(*MG.03, overwrites version from above,
1424 previously 'make_polynomial_'*) =
1425 Seq {id = "make_polynomial", preconds = []:term list,
1426 rew_ord = ("dummy_ord", dummy_ord),
1427 erls = Atools_erls, srls = Erls,calc = [], errpatts = [],
1428 rules = [Rls_ discard_minus,
1430 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1431 Rls_ order_mult_rls_,
1432 Rls_ simplify_power_,
1433 Rls_ calc_add_mult_pow_,
1434 Rls_ reduce_012_mult_,
1435 Rls_ order_add_rls_,
1436 Rls_ collect_numerals_,
1438 Rls_ discard_parentheses1
1444 val norm_Poly(*=make_polynomial*) =
1445 Seq {id = "norm_Poly", preconds = []:term list,
1446 rew_ord = ("dummy_ord", dummy_ord),
1447 erls = Atools_erls, srls = Erls, calc = [], errpatts = [],
1448 rules = [Rls_ discard_minus,
1450 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1451 Rls_ order_mult_rls_,
1452 Rls_ simplify_power_,
1453 Rls_ calc_add_mult_pow_,
1454 Rls_ reduce_012_mult_,
1455 Rls_ order_add_rls_,
1456 Rls_ collect_numerals_,
1458 Rls_ discard_parentheses1
1464 (* MG:03 Like make_polynomial_ but without Rls_ discard_parentheses1
1465 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1466 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1467 val make_rat_poly_with_parentheses =
1468 Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1469 rew_ord = ("dummy_ord", dummy_ord),
1470 erls = Atools_erls, srls = Erls, calc = [], errpatts = [],
1471 rules = [Rls_ discard_minus,
1472 Rls_ expand_poly_rat_,(*ignors rationals*)
1473 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1474 Rls_ order_mult_rls_,
1475 Rls_ simplify_power_,
1476 Rls_ calc_add_mult_pow_,
1477 Rls_ reduce_012_mult_,
1478 Rls_ order_add_rls_,
1479 Rls_ collect_numerals_,
1481 (*Rls_ discard_parentheses1 *)
1487 (*.a minimal ruleset for reverse rewriting of factions [2];
1488 compare expand_binoms.*)
1490 Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1491 erls = Atools_erls, srls = Erls,
1492 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1493 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1494 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1496 rules = [Thm ("real_plus_binom_times" ,num_str @{thm real_plus_binom_times}),
1497 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1498 Thm ("real_plus_binom_times1" ,num_str @{thm real_plus_binom_times1}),
1499 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1500 Thm ("real_plus_binom_times2" ,num_str @{thm real_plus_binom_times2}),
1501 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1503 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
1505 Thm ("distrib_right" ,num_str @{thm distrib_right}),
1506 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1507 Thm ("distrib_left",num_str @{thm distrib_left}),
1508 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1510 Thm ("mult_assoc", num_str @{thm mult_assoc}),
1511 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1512 Rls_ order_mult_rls_,
1513 (*Rls_ order_add_rls_,*)
1515 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1516 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1517 Calc ("Atools.pow", eval_binop "#power_"),
1519 Thm ("sym_realpow_twoI",
1520 num_str (@{thm realpow_twoI} RS @{thm sym})),
1521 (*"r1 * r1 = r1 ^^^ 2"*)
1522 Thm ("sym_real_mult_2",
1523 num_str (@{thm real_mult_2} RS @{thm sym})),
1524 (*"z1 + z1 = 2 * z1"*)
1525 Thm ("real_mult_2_assoc",num_str @{thm real_mult_2_assoc}),
1526 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1528 Thm ("real_num_collect",num_str @{thm real_num_collect}),
1529 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1530 Thm ("real_num_collect_assoc",num_str @{thm real_num_collect_assoc}),
1531 (*"[| l is_const; m is_const |] ==>
1532 l * n + (m * n + k) = (l + m) * n + k"*)
1533 Thm ("real_one_collect",num_str @{thm real_one_collect}),
1534 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1535 Thm ("real_one_collect_assoc",num_str @{thm real_one_collect_assoc}),
1536 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1538 Thm ("realpow_multI", num_str @{thm realpow_multI}),
1539 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1541 Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1542 Calc ("Groups.times_class.times", eval_binop "#mult_"),
1543 Calc ("Atools.pow", eval_binop "#power_"),
1545 Thm ("mult_1_left",num_str @{thm mult_1_left}),(*"1 * z = z"*)
1546 Thm ("mult_zero_left",num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
1547 Thm ("add_0_left",num_str @{thm add_0_left})(*0 + z = z*)
1549 (*Rls_ order_add_rls_*)
1552 scr = EmptyScr}:rls;
1555 setup {* KEStore_Elems.add_rlss
1556 [("norm_Poly", (Context.theory_name @{theory}, prep_rls norm_Poly)),
1557 ("Poly_erls", (Context.theory_name @{theory}, prep_rls Poly_erls)),(*FIXXXME:del with rls.rls'*)
1558 ("expand", (Context.theory_name @{theory}, prep_rls expand)),
1559 ("expand_poly", (Context.theory_name @{theory}, prep_rls expand_poly)),
1560 ("simplify_power", (Context.theory_name @{theory}, prep_rls simplify_power)),
1562 ("order_add_mult", (Context.theory_name @{theory}, prep_rls order_add_mult)),
1563 ("collect_numerals", (Context.theory_name @{theory}, prep_rls collect_numerals)),
1564 ("collect_numerals_", (Context.theory_name @{theory}, prep_rls collect_numerals_)),
1565 ("reduce_012", (Context.theory_name @{theory}, prep_rls reduce_012)),
1566 ("discard_parentheses", (Context.theory_name @{theory}, prep_rls discard_parentheses)),
1568 ("make_polynomial", (Context.theory_name @{theory}, prep_rls make_polynomial)),
1569 ("expand_binoms", (Context.theory_name @{theory}, prep_rls expand_binoms)),
1570 ("rev_rew_p", (Context.theory_name @{theory}, prep_rls rev_rew_p)),
1571 ("discard_minus", (Context.theory_name @{theory}, prep_rls discard_minus)),
1572 ("expand_poly_", (Context.theory_name @{theory}, prep_rls expand_poly_)),
1574 ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls expand_poly_rat_)),
1575 ("simplify_power_", (Context.theory_name @{theory}, prep_rls simplify_power_)),
1576 ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls calc_add_mult_pow_)),
1577 ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls reduce_012_mult_)),
1578 ("reduce_012_", (Context.theory_name @{theory}, prep_rls reduce_012_)),
1580 ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls discard_parentheses1)),
1581 ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls order_mult_rls_)),
1582 ("order_add_rls_", (Context.theory_name @{theory}, prep_rls order_add_rls_)),
1583 ("make_rat_poly_with_parentheses",
1584 (Context.theory_name @{theory}, prep_rls make_rat_poly_with_parentheses))] *}
1585 setup {* KEStore_Elems.add_calcs
1586 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
1587 eval_is_polyrat_in "#eval_is_polyrat_in")),
1588 ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
1589 ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
1590 ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
1591 ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
1592 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
1593 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))] *}
1599 (prep_pbt thy "pbl_simp_poly" [] e_pblID
1600 (["polynomial","simplification"],
1601 [("#Given" ,["Term t_t"]),
1602 ("#Where" ,["t_t is_polyexp"]),
1603 ("#Find" ,["normalform n_n"])
1605 append_rls "e_rls" e_rls [(*for preds in where_*)
1606 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1607 SOME "Simplify t_t",
1608 [["simplification","for_polynomials"]]));
1610 setup {* KEStore_Elems.add_pbts
1611 [(prep_pbt thy "pbl_simp_poly" [] e_pblID
1612 (["polynomial","simplification"],
1613 [("#Given" ,["Term t_t"]),
1614 ("#Where" ,["t_t is_polyexp"]),
1615 ("#Find" ,["normalform n_n"])],
1616 append_rls "e_rls" e_rls [(*for preds in where_*)
1617 Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1618 SOME "Simplify t_t",
1619 [["simplification","for_polynomials"]]))] *}
1625 (prep_met thy "met_simp_poly" [] e_metID
1626 (["simplification","for_polynomials"],
1627 [("#Given" ,["Term t_t"]),
1628 ("#Where" ,["t_t is_polyexp"]),
1629 ("#Find" ,["normalform n_n"])
1631 {rew_ord'="tless_true",
1635 prls = append_rls "simplification_for_polynomials_prls" e_rls
1636 [(*for preds in where_*)
1637 Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1638 crls = e_rls, errpats = [], nrls = norm_Poly},
1639 "Script SimplifyScript (t_t::real) = " ^
1640 " ((Rewrite_Set norm_Poly False) t_t)"