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
12 subsection \<open>remark on term-structure of polynomials\<close>
15 the code below reflects missing coordination between two authors:
16 * ML: built the equation solver; simple rule-sets, programs; better predicates for specifications.
17 * MG: built simplification of polynomials with AC rewriting by ML code
20 *** there are 5 kinds of expanded normalforms ***
22 [1] 'complete polynomial' (Komplettes Polynom), univariate
23 a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
24 not (a_n = 0), some a_i may be zero (DON'T disappear),
25 variables in monomials lexicographically ordered and complete,
26 x written as 1*x^1, ...
27 [2] 'polynomial' (Polynom), univariate and multivariate
28 a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
29 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
30 not (a_n = 0), some a_i may be zero (ie. monomials disappear),
31 exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
32 and variables in monomials are lexicographically ordered
33 examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
34 [1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
35 [2]: "x + (-50) * x ^^^ 3"
36 [2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
38 [3] 'expanded_term' (Ausmultiplizierter Term):
39 pull out unary minus to binary minus,
40 as frequently exercised in schools; other conditions for [2] hold however
41 examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
42 "4 * x ^^^ 2 - 9 * y ^^^ 2"
43 [4] 'polynomial_in' (Polynom in):
44 polynomial in 1 variable with arbitrary coefficients
45 examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
46 "(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
47 [5] 'expanded_in' (Ausmultiplizierter Termin in):
48 analoguous to [3] with binary minus like [3]
49 examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
50 "(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
52 subsection \<open>consts definition for predicates in specifications\<close>
55 is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
56 is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
57 has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
58 is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
60 is'_multUnordered:: "real => bool" ("_ is'_multUnordered")
61 is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
62 is'_polyexp :: "real => bool" ("_ is'_polyexp")
67 ("((Script Expand'_binoms (_ =))// (_))" 9)
69 subsection \<open>theorems not yet adopted from Isabelle\<close>
70 axiomatization where (*.not contained in Isabelle2002,
71 stated as axioms, TODO: prove as theorems;
72 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
74 realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
75 realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
76 realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
77 realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
79 realpow_oneI: "r ^^^ 1 = r" and
80 realpow_zeroI: "r ^^^ 0 = 1" and
81 realpow_eq_oneI: "1 ^^^ n = 1" and
82 realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
83 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
84 (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
85 realpow_minus_oneI: "(- 1) ^^^ (2 * n) = 1" and
87 realpow_twoI: "r ^^^ 2 = r * r" and
88 realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
89 realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
90 realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
91 realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
92 realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
93 realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
94 realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
95 realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
96 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
97 ==> r ^^^ n = r * r ^^^ (n + -1)" and
98 realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
101 realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
102 realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
106 real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
107 real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
108 real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
109 real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
110 real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
111 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
112 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
113 real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
114 real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
116 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
117 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
118 real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
120 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
121 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
123 real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
124 *(a^^^2 + 2*a*b + b^^^2)" and
125 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
126 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
127 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
128 real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
129 real_diff_minus: "a - b = a + -1 * b" and
130 real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
131 real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
132 (*WN071229 changed for Schaerding -----vvv*)
133 (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
134 real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
135 (*WN071229 changed for Schaerding -----^^^*)
136 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
137 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
138 real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
139 real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
140 real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
141 real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
142 real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
143 real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
144 real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
145 real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
146 real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
147 real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
149 real_num_collect: "[| l is_const; m is_const |] ==>
150 l * n + m * n = (l + m) * n" and
151 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
152 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
153 real_num_collect_assoc: "[| l is_const; m is_const |] ==>
154 l * n + (m * n + k) = (l + m) * n + k" and
155 real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
156 l * n + (m * n + k) = (l + m)
158 real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
159 (k + m * n) + l * n = k + (l + m) * n" and
160 real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
161 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
162 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
163 real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
165 real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
166 real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
168 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
169 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
170 real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
171 real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
172 real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
174 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
175 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
177 subsection \<open>auxiliary functions\<close>
178 subsubsection \<open>for predicates in specifications (ML)\<close>
183 (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)
184 (*. a 'monomial t in variable v' is a term t with
185 either (1) v NOT existent in t, or (2) v contained in t,
187 if (2) then v is a factor on the very right, ev. with exponent.*)
188 fun factor_right_deg (*case 2*)
189 (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Atools.pow",_) $ vv $ Free (d, _))) v =
190 if vv = v andalso not (TermC.coeff_in t1 v) then SOME (TermC.int_of_str d) else NONE
191 | factor_right_deg (Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
192 if (vv = v) then SOME (TermC.int_of_str d) else NONE
193 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =
194 if vv = v andalso not (TermC.coeff_in t1 v) then SOME 1 else NONE
195 | factor_right_deg vv v =
196 if (vv = v) then SOME 1 else NONE;
197 fun mono_deg_in m v = (*case 1*)
198 if not (TermC.coeff_in m v) then (*case 1*) SOME 0 else factor_right_deg m v;
200 fun expand_deg_in t v =
202 fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) =
203 (case mono_deg_in t2 v of (* $ is left associative*)
204 SOME d' => edi d' d' t1 | NONE => NONE)
205 | edi ~1 ~1 (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
206 (case mono_deg_in t2 v of
207 SOME d' => edi d' d' t1 | NONE => NONE)
208 | edi d dmax (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
209 (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)
210 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
212 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
213 (case mono_deg_in t2 v of
214 SOME d' => (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)
215 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
218 (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)
219 | edi d dmax t = (*basecase last*)
220 (case mono_deg_in t v of
221 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
225 fun poly_deg_in t v =
227 fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
228 (case mono_deg_in t2 v of (* $ is left associative *)
229 SOME d' => edi d' d' t1
231 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
232 (case mono_deg_in t2 v of
233 SOME d' => (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)
234 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
237 (case mono_deg_in t v of
240 | edi d dmax t = (* basecase last *)
241 (case mono_deg_in t v of
243 if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
248 subsubsection \<open>for hard-coded AC rewriting (MG)\<close>
250 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
252 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
253 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
254 (* Polynom --> List von Monomen *)
255 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
256 (poly2list t1) @ (poly2list t2)
259 (* Monom --> Liste von Variablen *)
260 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
261 (monom2list t1) @ (monom2list t2)
262 | monom2list t = [t];
264 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
265 fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
266 | get_basStr (Free (str, _)) = str
267 | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
269 error("get_basStr: called with t= "^(Rule.term2str t));*)
271 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
272 fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
273 | get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
274 | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
275 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
277 error("get_potStr: called with t= "^(Rule.term2str t));*)
279 (* Umgekehrte string_ord *)
280 val string_ord_rev = rev_order o string_ord;
282 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
283 innerhalb eines Monomes:
284 - zuerst lexikographisch nach Variablenname
285 - wenn gleich: nach steigender Potenz *)
286 fun var_ord (a,b: term) = prod_ord string_ord string_ord
287 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
289 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
290 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
291 - zuerst lexikographisch nach Variablenname
292 - wenn gleich: nach sinkender Potenz*)
293 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
294 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
297 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
298 val sort_varList = sort var_ord;
300 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
301 Argumente in eine Liste *)
302 fun args u : term list =
303 let fun stripc (f$t, ts) = stripc (f, t::ts)
304 | stripc (t as Free _, ts) = (t::ts)
305 | stripc (_, ts) = ts
306 in stripc (u, []) end;
308 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
309 (keine Variablen) enthaelt *)
310 fun filter_num [] = true
311 | filter_num [Free x] = if (TermC.is_num (Free x)) then true
313 | filter_num ((Free _)::_) = false
315 (filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;
317 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
318 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
319 fun is_nums t = filter_num [t];
321 (* Berechnet den Gesamtgrad eines Monoms *)
323 fun counter (n, []) = n
324 | counter (n, x :: xs) =
329 (Const ("Atools.pow", _) $ Free _ $ Free (str_h, T)) =>
330 if (is_nums (Free (str_h, T))) then
331 counter (n + (the (TermC.int_of_str_opt str_h)), xs)
332 else counter (n + 1000, xs) (*FIXME.MG?!*)
333 | (Const ("Atools.pow", _) $ Free _ $ _ ) =>
334 counter (n + 1000, xs) (*FIXME.MG?!*)
335 | (Free _) => counter (n + 1, xs)
336 (*| _ => error("monom_degree: called with factor: "^(Rule.term2str x)))*)
337 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
339 fun monom_degree l = counter (0, l)
342 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
343 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
344 werden jedoch dabei ignoriert (uebersprungen) *)
345 fun dict_cond_ord _ _ ([], []) = EQUAL
346 | dict_cond_ord _ _ ([], _ :: _) = LESS
347 | dict_cond_ord _ _ (_ :: _, []) = GREATER
348 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
349 (case (cond x, cond y) of
350 (false, false) => (case elem_ord (x, y) of
351 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
353 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
354 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
355 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
357 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
358 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
359 dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
360 fun degree_ord (xs, ys) =
361 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
362 ((monom_degree xs, xs), (monom_degree ys, ys));
364 fun hd_str str = substring (str, 0, 1);
365 fun tl_str str = substring (str, 1, (size str) - 1);
367 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
368 fun get_koeff_of_mon [] = error("get_koeff_of_mon: called with l = []")
369 | get_koeff_of_mon (x::_) = if is_nums x then SOME x else NONE;
371 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
372 fun koeff2ordStr (SOME x) = (case x of
374 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
376 | _ => "aaa") (* "num.Ausdruck" --> gross *)
377 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
379 (* Order zum Vergleich von Koeffizienten (strings):
380 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
381 fun compare_koeff_ord (xs, ys) =
382 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
383 (koeff2ordStr o get_koeff_of_mon) ys);
385 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
386 fun koeff_degree_ord (xs, ys) =
387 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
389 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
391 val sort_monList = sort koeff_degree_ord;
393 (* Alternativ zu degree_ord koennte auch die viel einfachere und
394 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
395 fuer unsere Zwecke geeignet!
397 fun simple_ord (al,bl: term list) = dict_ord string_ord
398 (map get_basStr al, map get_basStr bl);
400 val sort_monList = sort simple_ord; *)
402 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
403 (mit gewuenschtem Typen T) *)
404 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
405 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
406 fun binop op_ t1 t2 = op_ $ t1 $ t2;
407 fun create_prod T (a,b) = binop (mult T) a b;
408 fun create_sum T (a,b) = binop (plus T) a b;
410 (* löscht letztes Element einer Liste *)
411 fun drop_last l = take ((length l)-1,l);
413 (* Liste von Variablen --> Monom *)
414 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
416 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
417 gleiche Monome zusammengefasst werden können (collect_numerals)!
418 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
420 (* Liste von Monomen --> Polynom *)
421 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
423 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
424 bessere Darstellung, da keine Klammern sichtbar!
425 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
427 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
428 fun sort_variables t =
430 val ll = map monom2list (poly2list t);
431 val lls = map sort_varList ll;
433 val ls = map (create_monom T) lls;
434 in create_polynom T ls end;
436 (* sorts the monoms of an expanded and variable-sorted polynomial
440 val ll = map monom2list (poly2list t);
441 val lls = sort_monList ll;
443 val ls = map (create_monom T) lls;
444 in create_polynom T ls end;
447 subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>
449 local (*. for make_polynomial .*)
451 open Term; (* for type order = EQUAL | LESS | GREATER *)
453 fun pr_ord EQUAL = "EQUAL"
454 | pr_ord LESS = "LESS"
455 | pr_ord GREATER = "GREATER";
457 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
459 "Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
460 | _ => (((a, 0), T), 0))
461 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
462 | dest_hd' (Var v) = (v, 2)
463 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
464 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
465 | dest_hd' t = raise TERM ("dest_hd'", [t]);
467 fun size_of_term' (Const(str,_) $ t) =
468 if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
469 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
470 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
471 | size_of_term' _ = 1;
473 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
474 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
475 | term_ord' pr thy (t, u) =
478 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
479 val _ = tracing ("t= f@ts= \"" ^ Rule.term_to_string''' thy f ^ "\" @ \"[" ^
480 commas (map (Rule.term_to_string''' thy) ts) ^ "]\"");
481 val _ = tracing("u= g@us= \"" ^ Rule.term_to_string''' thy g ^ "\" @ \"[" ^
482 commas (map (Rule.term_to_string''' thy) us) ^ "]\"");
483 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
484 string_of_int (size_of_term' u) ^ ")");
485 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
486 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
487 val _ = tracing ("-------");
490 case int_ord (size_of_term' t, size_of_term' u) of
492 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
493 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
497 and hd_ord (f, g) = (* ~ term.ML *)
498 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
499 and terms_ord _ pr (ts, us) =
500 list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
504 fun ord_make_polynomial (pr:bool) thy (_: Rule.subst) tu =
505 (term_ord' pr thy(***) tu = LESS );
509 Rule.rew_ord' := overwritel (! Rule.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
510 [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
513 subsection \<open>predicates\<close>
514 subsubsection \<open>in specifications\<close>
516 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
517 fun is_polyrat_in t v =
519 fun finddivide (_ $ _ $ _ $ _) _ = error("is_polyrat_in:")
520 (* at the moment there is no term like this, but ....*)
521 | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (TermC.coeff_in b v)
522 | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
523 | finddivide (_ $ t1) v = finddivide t1 v
524 | finddivide _ _ = false;
525 in finddivide t v end;
527 fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;
528 fun is_poly_in t v = case poly_deg_in t v of SOME _ => true | NONE => false;
529 fun has_degree_in t v = case expand_deg_in t v of SOME d => d | NONE => ~1;
531 (*.the expression contains + - * ^ only ?
532 this is weaker than 'is_polynomial' !.*)
533 fun is_polyexp (Free _) = true
534 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
535 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
536 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
537 | is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
538 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
539 ((is_polyexp t1) andalso (is_polyexp t2))
540 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
541 ((is_polyexp t1) andalso (is_polyexp t2))
542 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
543 ((is_polyexp t1) andalso (is_polyexp t2))
544 | is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
545 ((is_polyexp t1) andalso (is_polyexp t2))
546 | is_polyexp _ = false;
549 subsubsection \<open>for hard-coded AC rewriting\<close>
551 (* auch Klammerung muss übereinstimmen;
552 sort_variables klammert Produkte rechtslastig*)
553 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
555 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
558 subsection \<open>evaluations functions\<close>
559 subsubsection \<open>for predicates\<close>
561 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
563 then SOME ((Rule.term2str p) ^ " = True",
564 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
565 else SOME ((Rule.term2str p) ^ " = True",
566 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
567 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
569 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
570 fun eval_is_expanded_in _ _
571 (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
572 if is_expanded_in t v
573 then SOME ((Rule.term2str p) ^ " = True",
574 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
575 else SOME ((Rule.term2str p) ^ " = True",
576 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
577 | eval_is_expanded_in _ _ _ _ = NONE;
579 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
580 fun eval_is_poly_in _ _
581 (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
583 then SOME ((Rule.term2str p) ^ " = True",
584 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
585 else SOME ((Rule.term2str p) ^ " = True",
586 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
587 | eval_is_poly_in _ _ _ _ = NONE;
589 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
590 fun eval_has_degree_in _ _
591 (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
592 let val d = has_degree_in t v
593 val d' = TermC.term_of_num HOLogic.realT d
594 in SOME ((Rule.term2str p) ^ " = " ^ (string_of_int d),
595 HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
597 | eval_has_degree_in _ _ _ _ = NONE;
599 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
600 fun eval_is_polyexp (thmid:string) _
601 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
603 then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
604 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
605 else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
606 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
607 | eval_is_polyexp _ _ _ _ = NONE;
610 subsubsection \<open>for hard-coded AC rewriting\<close>
613 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
614 fun eval_is_addUnordered (thmid:string) _
615 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
616 if is_addUnordered arg
617 then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
618 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
619 else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
620 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
621 | eval_is_addUnordered _ _ _ _ = NONE;
623 fun eval_is_multUnordered (thmid:string) _
624 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
625 if is_multUnordered arg
626 then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
627 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
628 else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
629 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
630 | eval_is_multUnordered _ _ _ _ = NONE;
633 subsection \<open>rule-sets\<close>
634 subsubsection \<open>without specific order\<close>
636 (* used only for merge *)
637 val calculate_Poly = Rule.append_rls "calculate_PolyFIXXXME.not.impl." Rule.e_rls [];
639 (*.for evaluation of conditions in rewrite rules.*)
640 val Poly_erls = Rule.append_rls "Poly_erls" Atools_erls
641 [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
642 Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
643 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
644 Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
645 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
646 Rule.Calc ("Atools.pow", eval_binop "#power_")];
648 val poly_crls = Rule.append_rls "poly_crls" Atools_crls
649 [Rule.Calc ("HOL.eq", eval_equal "#equal_"),
650 Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
651 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
652 Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
653 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
654 Rule.Calc ("Atools.pow" ,eval_binop "#power_")];
658 Rule.Rls {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
659 erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
660 rules = [Rule.Thm ("distrib_right" , TermC.num_str @{thm distrib_right}),
661 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
662 Rule.Thm ("distrib_left", TermC.num_str @{thm distrib_left})
663 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
664 ], scr = Rule.EmptyScr};
667 Rule.Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
668 erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
670 [Rule.Thm ("real_diff_minus", TermC.num_str @{thm real_diff_minus}),
671 (*"a - b = a + -1 * b"*)
672 Rule.Thm ("sym_real_mult_minus1", TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
673 (*- ?z = "-1 * ?z"*)],
674 scr = Rule.EmptyScr};
677 Rule.Rls{id = "expand_poly_", preconds = [],
678 rew_ord = ("dummy_ord", Rule.dummy_ord),
679 erls = Rule.e_rls,srls = Rule.Erls,
680 calc = [], errpatts = [],
682 [Rule.Thm ("real_plus_binom_pow4", TermC.num_str @{thm real_plus_binom_pow4}),
683 (*"(a + b)^^^4 = ... "*)
684 Rule.Thm ("real_plus_binom_pow5",TermC.num_str @{thm real_plus_binom_pow5}),
685 (*"(a + b)^^^5 = ... "*)
686 Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
687 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
688 (*WN071229 changed/removed for Schaerding -----vvv*)
689 (*Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),*)
690 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
691 Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
692 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
693 (*Rule.Thm ("real_plus_minus_binom1_p_p", TermC.num_str @{thm real_plus_minus_binom1_p_p}),*)
694 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
695 (*Rule.Thm ("real_plus_minus_binom2_p_p", TermC.num_str @{thm real_plus_minus_binom2_p_p}),*)
696 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
697 (*WN071229 changed/removed for Schaerding -----^^^*)
699 Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
700 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
701 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
702 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
704 Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
705 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
706 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
707 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
708 ], scr = Rule.EmptyScr};
710 val expand_poly_rat_ =
711 Rule.Rls{id = "expand_poly_rat_", preconds = [],
712 rew_ord = ("dummy_ord", Rule.dummy_ord),
713 erls = Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
714 [Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")
717 calc = [], errpatts = [],
719 [Rule.Thm ("real_plus_binom_pow4_poly", TermC.num_str @{thm real_plus_binom_pow4_poly}),
720 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
721 Rule.Thm ("real_plus_binom_pow5_poly", TermC.num_str @{thm real_plus_binom_pow5_poly}),
722 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
723 Rule.Thm ("real_plus_binom_pow2_poly",TermC.num_str @{thm real_plus_binom_pow2_poly}),
724 (*"[| a is_polyexp; b is_polyexp |] ==>
725 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
726 Rule.Thm ("real_plus_binom_pow3_poly",TermC.num_str @{thm real_plus_binom_pow3_poly}),
727 (*"[| a is_polyexp; b is_polyexp |] ==>
728 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
729 Rule.Thm ("real_plus_minus_binom1_p_p",TermC.num_str @{thm real_plus_minus_binom1_p_p}),
730 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
731 Rule.Thm ("real_plus_minus_binom2_p_p",TermC.num_str @{thm real_plus_minus_binom2_p_p}),
732 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
734 Rule.Thm ("real_add_mult_distrib_poly",
735 TermC.num_str @{thm real_add_mult_distrib_poly}),
736 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
737 Rule.Thm("real_add_mult_distrib2_poly",
738 TermC.num_str @{thm real_add_mult_distrib2_poly}),
739 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
741 Rule.Thm ("realpow_multI_poly", TermC.num_str @{thm realpow_multI_poly}),
742 (*"[| r is_polyexp; s is_polyexp |] ==>
743 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
744 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
745 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
746 ], scr = Rule.EmptyScr};
748 val simplify_power_ =
749 Rule.Rls{id = "simplify_power_", preconds = [],
750 rew_ord = ("dummy_ord", Rule.dummy_ord),
751 erls = Rule.e_rls, srls = Rule.Erls,
752 calc = [], errpatts = [],
753 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
754 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
755 Rule.Thm ("sym_realpow_twoI",
756 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
757 (*"r * r = r ^^^ 2"*)
758 Rule.Thm ("realpow_twoI_assoc_l",TermC.num_str @{thm realpow_twoI_assoc_l}),
759 (*"r * (r * s) = r ^^^ 2 * s"*)
761 Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
762 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
763 Rule.Thm ("realpow_plus_1_assoc_l",
764 TermC.num_str @{thm realpow_plus_1_assoc_l}),
765 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
766 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
767 Rule.Thm ("realpow_plus_1_assoc_l2",
768 TermC.num_str @{thm realpow_plus_1_assoc_l2}),
769 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
771 Rule.Thm ("sym_realpow_addI",
772 TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
773 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
774 Rule.Thm ("realpow_addI_assoc_l",TermC.num_str @{thm realpow_addI_assoc_l}),
775 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
777 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
778 "r * r = r ^^^ 2" wenn r=a^^^b*)
779 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
780 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
781 ], scr = Rule.EmptyScr};
783 val calc_add_mult_pow_ =
784 Rule.Rls{id = "calc_add_mult_pow_", preconds = [],
785 rew_ord = ("dummy_ord", Rule.dummy_ord),
786 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
787 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
788 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
789 ("POWER", ("Atools.pow", eval_binop "#power_"))
792 rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
793 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
794 Rule.Calc ("Atools.pow", eval_binop "#power_")
795 ], scr = Rule.EmptyScr};
797 val reduce_012_mult_ =
798 Rule.Rls{id = "reduce_012_mult_", preconds = [],
799 rew_ord = ("dummy_ord", Rule.dummy_ord),
800 erls = Rule.e_rls,srls = Rule.Erls,
801 calc = [], errpatts = [],
802 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
803 Rule.Thm ("mult_1_right",TermC.num_str @{thm mult_1_right}),
804 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
805 Rule.Thm ("realpow_zeroI",TermC.num_str @{thm realpow_zeroI}),
806 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
807 Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
809 Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
811 ], scr = Rule.EmptyScr};
813 val collect_numerals_ =
814 Rule.Rls{id = "collect_numerals_", preconds = [],
815 rew_ord = ("dummy_ord", Rule.dummy_ord),
816 erls = Atools_erls, srls = Rule.Erls,
817 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
820 [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
821 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
822 Rule.Thm ("real_num_collect_assoc_r",TermC.num_str @{thm real_num_collect_assoc_r}),
823 (*"[| l is_const; m is_const |] ==> \
824 \(k + m * n) + l * n = k + (l + m)*n"*)
825 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
826 (*"m is_const ==> n + m * n = (1 + m) * n"*)
827 Rule.Thm ("real_one_collect_assoc_r",TermC.num_str @{thm real_one_collect_assoc_r}),
828 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
830 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
832 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
833 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
834 Rule.Thm ("real_mult_2_assoc_r",TermC.num_str @{thm real_mult_2_assoc_r}),
835 (*"(k + z1) + z1 = k + 2 * z1"*)
836 Rule.Thm ("sym_real_mult_2",TermC.num_str (@{thm real_mult_2} RS @{thm sym}))
837 (*"z1 + z1 = 2 * z1"*)
838 ], scr = Rule.EmptyScr};
841 Rule.Rls{id = "reduce_012_", preconds = [],
842 rew_ord = ("dummy_ord", Rule.dummy_ord),
843 erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
844 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
846 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
848 Rule.Thm ("mult_zero_right",TermC.num_str @{thm mult_zero_right}),
850 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
852 Rule.Thm ("add_0_right",TermC.num_str @{thm add_0_right}),
853 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
855 (*Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI})*)
857 Rule.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
859 ], scr = Rule.EmptyScr};
861 val discard_parentheses1 =
862 Rule.append_rls "discard_parentheses1" Rule.e_rls
863 [Rule.Thm ("sym_mult_assoc",
864 TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
865 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
866 (*Rule.Thm ("sym_add_assoc",
867 TermC.num_str (@{thm add_assoc} RS @{thm sym}))*)
868 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
872 Rule.Rls{id = "expand_poly", preconds = [],
873 rew_ord = ("dummy_ord", Rule.dummy_ord),
874 erls = Rule.e_rls,srls = Rule.Erls,
875 calc = [], errpatts = [],
877 rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
878 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
879 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
880 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
881 (*Rule.Thm ("distrib_right1",TermC.num_str @{thm distrib_right}1),
882 ....... 18.3.03 undefined???*)
884 Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
885 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
886 Rule.Thm ("real_minus_binom_pow2_p",TermC.num_str @{thm real_minus_binom_pow2_p}),
887 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
888 Rule.Thm ("real_plus_minus_binom1_p",
889 TermC.num_str @{thm real_plus_minus_binom1_p}),
890 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
891 Rule.Thm ("real_plus_minus_binom2_p",
892 TermC.num_str @{thm real_plus_minus_binom2_p}),
893 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
895 Rule.Thm ("minus_minus",TermC.num_str @{thm minus_minus}),
897 Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
898 (*"a - b = a + -1 * b"*)
899 Rule.Thm ("sym_real_mult_minus1",
900 TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
903 (*Rule.Thm ("real_minus_add_distrib",
904 TermC.num_str @{thm real_minus_add_distrib}),*)
905 (*"- (?x + ?y) = - ?x + - ?y"*)
906 (*Rule.Thm ("real_diff_plus",TermC.num_str @{thm real_diff_plus})*)
908 ], scr = Rule.EmptyScr};
911 Rule.Rls{id = "simplify_power", preconds = [],
912 rew_ord = ("dummy_ord", Rule.dummy_ord),
913 erls = Rule.e_rls, srls = Rule.Erls,
914 calc = [], errpatts = [],
915 rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
916 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
918 Rule.Thm ("sym_realpow_twoI",
919 TermC.num_str( @{thm realpow_twoI} RS @{thm sym})),
920 (*"r1 * r1 = r1 ^^^ 2"*)
921 Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
922 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
923 Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
924 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
925 Rule.Thm ("sym_realpow_addI",
926 TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
927 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
928 Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
930 Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
932 ], scr = Rule.EmptyScr};
934 val collect_numerals =
935 Rule.Rls{id = "collect_numerals", preconds = [],
936 rew_ord = ("dummy_ord", Rule.dummy_ord),
937 erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
938 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
939 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
940 ("POWER", ("Atools.pow", eval_binop "#power_"))
942 rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
943 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
944 Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
945 (*"[| l is_const; m is_const |] ==>
946 l * n + (m * n + k) = (l + m) * n + k"*)
947 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
948 (*"m is_const ==> n + m * n = (1 + m) * n"*)
949 Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
950 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
951 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
952 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
953 Rule.Calc ("Atools.pow", eval_binop "#power_")
954 ], scr = Rule.EmptyScr};
956 Rule.Rls{id = "reduce_012", preconds = [],
957 rew_ord = ("dummy_ord", Rule.dummy_ord),
958 erls = Rule.e_rls,srls = Rule.Erls,
959 calc = [], errpatts = [],
960 rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
962 (*Rule.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),14.3.03*)
964 Rule.Thm ("minus_mult_left",
965 TermC.num_str (@{thm minus_mult_left} RS @{thm sym})),
966 (*- (?x * ?y) = "- ?x * ?y"*)
967 (*Rule.Thm ("real_minus_mult_cancel",
968 TermC.num_str @{thm real_minus_mult_cancel}),
969 (*"- ?x * - ?y = ?x * ?y"*)---*)
970 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
972 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
974 Rule.Thm ("right_minus",TermC.num_str @{thm right_minus}),
976 Rule.Thm ("sym_real_mult_2",
977 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
978 (*"z1 + z1 = 2 * z1"*)
979 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc})
980 (*"z1 + (z1 + k) = 2 * z1 + k"*)
981 ], scr = Rule.EmptyScr};
983 val discard_parentheses =
984 Rule.append_rls "discard_parentheses" Rule.e_rls
985 [Rule.Thm ("sym_mult_assoc",
986 TermC.num_str (@{thm mult.assoc} RS @{thm sym})),
987 Rule.Thm ("sym_add_assoc",
988 TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
991 subsubsection \<open>hard-coded AC rewriting\<close>
993 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
994 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
996 Rule.Rls{id = "order_add_mult", preconds = [],
997 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
998 erls = Rule.e_rls,srls = Rule.Erls,
999 calc = [], errpatts = [],
1000 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1002 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1003 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1004 Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1005 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1006 Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1008 Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1009 (*x + (y + z) = y + (x + z)*)
1010 Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
1011 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1012 ], scr = Rule.EmptyScr};
1013 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1014 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1016 Rule.Rls{id = "order_mult", preconds = [],
1017 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
1018 erls = Rule.e_rls,srls = Rule.Erls,
1019 calc = [], errpatts = [],
1020 rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
1022 Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
1023 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1024 Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc})
1025 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1026 ], scr = Rule.EmptyScr};
1029 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1030 []:(Rule.rule * (term * term list)) list;
1031 fun init_state (_: term) = Rule.e_rrlsstate;
1032 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1033 ([]:(Rule.rule * (term * term list)) list);
1034 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1035 fun normal_form t = SOME (sort_variables t, []: term list);
1038 Rule.Rrls {id = "order_mult_",
1040 (* ?p matched with the current term gives an environment,
1041 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1042 [([TermC.parse_patt thy "?p is_multUnordered"],
1043 TermC.parse_patt thy "?p :: real")],
1044 rew_ord = ("dummy_ord", Rule.dummy_ord),
1045 erls = Rule.append_rls "Rule.e_rls-is_multUnordered" Rule.e_rls
1046 [Rule.Calc ("Poly.is'_multUnordered",
1047 eval_is_multUnordered "")],
1048 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1049 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1050 ("DIVIDE", ("Rings.divide_class.divide",
1051 eval_cancel "#divide_e")),
1052 ("POWER" , ("Atools.pow", eval_binop "#power_"))],
1054 scr = Rule.Rfuns {init_state = init_state,
1055 normal_form = normal_form,
1056 locate_rule = locate_rule,
1057 next_rule = next_rule,
1058 attach_form = attach_form}};
1059 val order_mult_rls_ =
1060 Rule.Rls {id = "order_mult_rls_", preconds = [],
1061 rew_ord = ("dummy_ord", Rule.dummy_ord),
1062 erls = Rule.e_rls,srls = Rule.Erls,
1063 calc = [], errpatts = [],
1064 rules = [Rule.Rls_ order_mult_
1065 ], scr = Rule.EmptyScr};
1069 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1070 []: (Rule.rule * (term * term list)) list;
1071 fun init_state (_: term) = Rule.e_rrlsstate;
1072 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1073 ([]: (Rule.rule * (term * term list)) list);
1074 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1075 fun normal_form t = SOME (sort_monoms t,[]: term list);
1078 Rule.Rrls {id = "order_add_",
1079 prepat = (*WN.18.6.03 Preconditions und Pattern,
1080 die beide passen muessen, damit das Rule.Rrls angewandt wird*)
1081 [([TermC.parse_patt @{theory} "?p is_addUnordered"],
1082 TermC.parse_patt @{theory} "?p :: real"
1083 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1084 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1085 rew_ord = ("dummy_ord", Rule.dummy_ord),
1086 erls = Rule.append_rls "Rule.e_rls-is_addUnordered" Rule.e_rls(*MG: poly_erls*)
1087 [Rule.Calc ("Poly.is'_addUnordered",
1088 eval_is_addUnordered "")],
1089 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
1090 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
1091 ("DIVIDE",("Rings.divide_class.divide",
1092 eval_cancel "#divide_e")),
1093 ("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
1095 scr = Rule.Rfuns {init_state = init_state,
1096 normal_form = normal_form,
1097 locate_rule = locate_rule,
1098 next_rule = next_rule,
1099 attach_form = attach_form}};
1101 val order_add_rls_ =
1102 Rule.Rls {id = "order_add_rls_", preconds = [],
1103 rew_ord = ("dummy_ord", Rule.dummy_ord),
1104 erls = Rule.e_rls,srls = Rule.Erls,
1105 calc = [], errpatts = [],
1106 rules = [Rule.Rls_ order_add_
1107 ], scr = Rule.EmptyScr};
1110 text \<open>rule-set make_polynomial also named norm_Poly:
1111 Rewrite order has not been implemented properly; the order is better in
1112 make_polynomial_in (coded in SML).
1113 Notes on state of development:
1114 \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
1115 \# migration Isabelle2002 --> 2011 weakened the rule set, see test
1116 --- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
1119 (*. see MG-DA.p.52ff .*)
1120 val make_polynomial(*MG.03, overwrites version from above,
1121 previously 'make_polynomial_'*) =
1122 Rule.Seq {id = "make_polynomial", preconds = []:term list,
1123 rew_ord = ("dummy_ord", Rule.dummy_ord),
1124 erls = Atools_erls, srls = Rule.Erls,calc = [], errpatts = [],
1125 rules = [Rule.Rls_ discard_minus,
1126 Rule.Rls_ expand_poly_,
1127 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1128 Rule.Rls_ order_mult_rls_,
1129 Rule.Rls_ simplify_power_,
1130 Rule.Rls_ calc_add_mult_pow_,
1131 Rule.Rls_ reduce_012_mult_,
1132 Rule.Rls_ order_add_rls_,
1133 Rule.Rls_ collect_numerals_,
1134 Rule.Rls_ reduce_012_,
1135 Rule.Rls_ discard_parentheses1
1141 val norm_Poly(*=make_polynomial*) =
1142 Rule.Seq {id = "norm_Poly", preconds = []:term list,
1143 rew_ord = ("dummy_ord", Rule.dummy_ord),
1144 erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1145 rules = [Rule.Rls_ discard_minus,
1146 Rule.Rls_ expand_poly_,
1147 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1148 Rule.Rls_ order_mult_rls_,
1149 Rule.Rls_ simplify_power_,
1150 Rule.Rls_ calc_add_mult_pow_,
1151 Rule.Rls_ reduce_012_mult_,
1152 Rule.Rls_ order_add_rls_,
1153 Rule.Rls_ collect_numerals_,
1154 Rule.Rls_ reduce_012_,
1155 Rule.Rls_ discard_parentheses1
1161 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1
1162 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1163 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1164 val make_rat_poly_with_parentheses =
1165 Rule.Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1166 rew_ord = ("dummy_ord", Rule.dummy_ord),
1167 erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
1168 rules = [Rule.Rls_ discard_minus,
1169 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1170 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1171 Rule.Rls_ order_mult_rls_,
1172 Rule.Rls_ simplify_power_,
1173 Rule.Rls_ calc_add_mult_pow_,
1174 Rule.Rls_ reduce_012_mult_,
1175 Rule.Rls_ order_add_rls_,
1176 Rule.Rls_ collect_numerals_,
1177 Rule.Rls_ reduce_012_
1178 (*Rule.Rls_ discard_parentheses1 *)
1184 (*.a minimal ruleset for reverse rewriting of factions [2];
1185 compare expand_binoms.*)
1187 Rule.Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1188 erls = Atools_erls, srls = Rule.Erls,
1189 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1190 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1191 ("POWER", ("Atools.pow", eval_binop "#power_"))*)
1193 rules = [Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
1194 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1195 Rule.Thm ("real_plus_binom_times1" ,TermC.num_str @{thm real_plus_binom_times1}),
1196 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1197 Rule.Thm ("real_plus_binom_times2" ,TermC.num_str @{thm real_plus_binom_times2}),
1198 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1200 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
1202 Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1203 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1204 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1205 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1207 Rule.Thm ("mult_assoc", TermC.num_str @{thm mult.assoc}),
1208 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1209 Rule.Rls_ order_mult_rls_,
1210 (*Rule.Rls_ order_add_rls_,*)
1212 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1213 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1214 Rule.Calc ("Atools.pow", eval_binop "#power_"),
1216 Rule.Thm ("sym_realpow_twoI",
1217 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1218 (*"r1 * r1 = r1 ^^^ 2"*)
1219 Rule.Thm ("sym_real_mult_2",
1220 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1221 (*"z1 + z1 = 2 * z1"*)
1222 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1223 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1225 Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1226 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1227 Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
1228 (*"[| l is_const; m is_const |] ==>
1229 l * n + (m * n + k) = (l + m) * n + k"*)
1230 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1231 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1232 Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
1233 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1235 Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
1236 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1238 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1239 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1240 Rule.Calc ("Atools.pow", eval_binop "#power_"),
1242 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
1243 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
1244 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left})(*0 + z = z*)
1246 (*Rule.Rls_ order_add_rls_*)
1249 scr = Rule.EmptyScr};
1252 subsection \<open>rule-sets with explicit program for intermediate steps\<close>
1253 text \<open>such rule-sets are generated automatically in general\<close>
1254 (* probably perfectly replaced by auto-generated version *)
1255 partial_function (tailrec) expand_binoms :: "real \<Rightarrow> real"
1257 "expand_binoms term =
1259 ((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@
1261 (Try (Repeat (Rewrite ''distrib_right'' False))) @@
1262 (Try (Repeat (Rewrite ''distrib_left'' False))) @@
1263 (Try (Repeat (Rewrite ''left_diff_distrib'' False))) @@
1264 (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@
1266 (Try (Repeat (Rewrite ''mult_1_left'' False))) @@
1267 (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@
1268 (Try (Repeat (Rewrite ''add_0_left'' False))) @@
1270 (Try (Repeat (Rewrite ''mult_commute'' False))) @@
1271 (Try (Repeat (Rewrite ''real_mult_left_commute'' False))) @@
1272 (Try (Repeat (Rewrite ''mult_assoc'' False))) @@
1273 (Try (Repeat (Rewrite ''add_commute'' False))) @@
1274 (Try (Repeat (Rewrite ''add_left_commute'' False))) @@
1275 (Try (Repeat (Rewrite ''add_assoc'' False))) @@
1277 (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@
1278 (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@
1279 (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@
1280 (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@
1282 (Try (Repeat (Rewrite ''real_num_collect'' False))) @@
1283 (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@
1285 (Try (Repeat (Rewrite ''real_one_collect'' False))) @@
1286 (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@
1288 (Try (Repeat (Calculate ''PLUS'' ))) @@
1289 (Try (Repeat (Calculate ''TIMES'' ))) @@
1290 (Try (Repeat (Calculate ''POWER''))))
1294 val scr_make_polynomial =
1295 "Script Expand_binoms t_t = " ^
1297 "((Try (Repeat (Rewrite ''real_diff_minus'' False))) @@ " ^
1299 " (Try (Repeat (Rewrite ''distrib_right'' False))) @@ " ^
1300 " (Try (Repeat (Rewrite ''distrib_left'' False))) @@ " ^
1301 " (Try (Repeat (Rewrite ''left_diff_distrib'' False))) @@ " ^
1302 " (Try (Repeat (Rewrite ''right_diff_distrib'' False))) @@ " ^
1304 " (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
1305 " (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
1306 " (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
1308 " (Try (Repeat (Rewrite ''mult_commute'' False))) @@ " ^
1309 " (Try (Repeat (Rewrite ''real_mult_left_commute'' False))) @@ " ^
1310 " (Try (Repeat (Rewrite ''mult_assoc'' False))) @@ " ^
1311 " (Try (Repeat (Rewrite ''add_commute'' False))) @@ " ^
1312 " (Try (Repeat (Rewrite ''add_left_commute'' False))) @@ " ^
1313 " (Try (Repeat (Rewrite ''add_assoc'' False))) @@ " ^
1315 " (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
1316 " (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
1317 " (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
1318 " (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
1320 " (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
1321 " (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
1323 " (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
1324 " (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
1326 " (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
1327 " (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
1328 " (Try (Repeat (Calculate ''POWER'')))) " ^
1331 (*version used by MG.02/03, overwritten by version AG in 04 below
1332 val make_polynomial = prep_rls'(
1333 Rule.Seq{id = "make_polynomial", preconds = []:term list,
1334 rew_ord = ("dummy_ord", Rule.dummy_ord),
1335 erls = Atools_erls, srls = Rule.Erls,
1336 calc = [], errpatts = [],
1337 rules = [Rule.Rls_ expand_poly,
1338 Rule.Rls_ order_add_mult,
1339 Rule.Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
1340 Rule.Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
1341 Rule.Rls_ reduce_012,
1342 Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),(*in --^*)
1343 Rule.Rls_ discard_parentheses
1349 (* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
1350 partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
1352 "expand_binoms term =
1354 ((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@
1355 (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@
1356 (Try (Repeat (Rewrite ''real_minus_binom_pow2'' False))) @@
1357 (Try (Repeat (Rewrite ''real_minus_binom_times'' False))) @@
1358 (Try (Repeat (Rewrite ''real_plus_minus_binom1'' False))) @@
1359 (Try (Repeat (Rewrite ''real_plus_minus_binom2'' False))) @@
1361 (Try (Repeat (Rewrite ''mult_1_left'' False))) @@
1362 (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@
1363 (Try (Repeat (Rewrite ''add_0_left'' False))) @@
1365 (Try (Repeat (Calculate ''PLUS'' ))) @@
1366 (Try (Repeat (Calculate ''TIMES'' ))) @@
1367 (Try (Repeat (Calculate ''POWER''))) @@
1369 (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@
1370 (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@
1371 (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@
1372 (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@
1374 (Try (Repeat (Rewrite ''real_num_collect'' False))) @@
1375 (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@
1377 (Try (Repeat (Rewrite ''real_one_collect'' False))) @@
1378 (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@
1380 (Try (Repeat (Calculate ''PLUS'' ))) @@
1381 (Try (Repeat (Calculate ''TIMES'' ))) @@
1382 (Try (Repeat (Calculate ''POWER''))))
1385 val scr_expand_binoms =
1386 "Script Expand_binoms t_t = " ^
1388 "((Try (Repeat (Rewrite ''real_plus_binom_pow2'' False))) @@ " ^
1389 " (Try (Repeat (Rewrite ''real_plus_binom_times'' False))) @@ " ^
1390 " (Try (Repeat (Rewrite ''real_minus_binom_pow2'' False))) @@ " ^
1391 " (Try (Repeat (Rewrite ''real_minus_binom_times'' False))) @@ " ^
1392 " (Try (Repeat (Rewrite ''real_plus_minus_binom1'' False))) @@ " ^
1393 " (Try (Repeat (Rewrite ''real_plus_minus_binom2'' False))) @@ " ^
1395 " (Try (Repeat (Rewrite ''mult_1_left'' False))) @@ " ^
1396 " (Try (Repeat (Rewrite ''mult_zero_left'' False))) @@ " ^
1397 " (Try (Repeat (Rewrite ''add_0_left'' False))) @@ " ^
1399 " (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
1400 " (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
1401 " (Try (Repeat (Calculate ''POWER''))) @@ " ^
1403 " (Try (Repeat (Rewrite ''sym_realpow_twoI'' False))) @@ " ^
1404 " (Try (Repeat (Rewrite ''realpow_plus_1'' False))) @@ " ^
1405 " (Try (Repeat (Rewrite ''sym_real_mult_2'' False))) @@ " ^
1406 " (Try (Repeat (Rewrite ''real_mult_2_assoc'' False))) @@ " ^
1408 " (Try (Repeat (Rewrite ''real_num_collect'' False))) @@ " ^
1409 " (Try (Repeat (Rewrite ''real_num_collect_assoc'' False))) @@ " ^
1411 " (Try (Repeat (Rewrite ''real_one_collect'' False))) @@ " ^
1412 " (Try (Repeat (Rewrite ''real_one_collect_assoc'' False))) @@ " ^
1414 " (Try (Repeat (Calculate ''PLUS'' ))) @@ " ^
1415 " (Try (Repeat (Calculate ''TIMES'' ))) @@ " ^
1416 " (Try (Repeat (Calculate ''POWER'')))) " ^
1420 Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1421 erls = Atools_erls, srls = Rule.Erls,
1422 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1423 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1424 ("POWER", ("Atools.pow", eval_binop "#power_"))
1426 rules = [Rule.Thm ("real_plus_binom_pow2",
1427 TermC.num_str @{thm real_plus_binom_pow2}),
1428 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1429 Rule.Thm ("real_plus_binom_times",
1430 TermC.num_str @{thm real_plus_binom_times}),
1431 (*"(a + b)*(a + b) = ...*)
1432 Rule.Thm ("real_minus_binom_pow2",
1433 TermC.num_str @{thm real_minus_binom_pow2}),
1434 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1435 Rule.Thm ("real_minus_binom_times",
1436 TermC.num_str @{thm real_minus_binom_times}),
1437 (*"(a - b)*(a - b) = ...*)
1438 Rule.Thm ("real_plus_minus_binom1",
1439 TermC.num_str @{thm real_plus_minus_binom1}),
1440 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1441 Rule.Thm ("real_plus_minus_binom2",
1442 TermC.num_str @{thm real_plus_minus_binom2}),
1443 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1445 Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
1446 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1447 Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
1448 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1449 Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
1450 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1451 Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
1452 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1453 Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
1454 (*(a*b)^^^n = a^^^n * b^^^n*)
1455 Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
1456 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1457 Rule.Thm ("real_minus_binom_pow3",
1458 TermC.num_str @{thm real_minus_binom_pow3}),
1459 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1462 (*Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
1463 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1464 Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
1465 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1466 Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
1467 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1468 Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
1469 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1471 Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
1473 Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
1475 Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),(*"0 + z = z"*)
1477 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1478 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1479 Rule.Calc ("Atools.pow", eval_binop "#power_"),
1480 (*Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
1482 Rule.Thm ("real_mult_left_commute",
1483 TermC.num_str @{thm real_mult_left_commute}),
1484 Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
1485 Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
1486 Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
1487 Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
1489 Rule.Thm ("sym_realpow_twoI",
1490 TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
1491 (*"r1 * r1 = r1 ^^^ 2"*)
1492 Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
1493 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1494 (*Rule.Thm ("sym_real_mult_2",
1495 TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
1496 (*"z1 + z1 = 2 * z1"*)*)
1497 Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
1498 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1500 Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
1501 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
1502 Rule.Thm ("real_num_collect_assoc",
1503 TermC.num_str @{thm real_num_collect_assoc}),
1504 (*"[| l is_const; m is_const |] ==>
1505 l * n + (m * n + k) = (l + m) * n + k"*)
1506 Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
1507 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1508 Rule.Thm ("real_one_collect_assoc",
1509 TermC.num_str @{thm real_one_collect_assoc}),
1510 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1512 Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
1513 Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
1514 Rule.Calc ("Atools.pow", eval_binop "#power_")
1516 scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) scr_expand_binoms)
1520 subsection \<open>add to KEStore\<close>
1521 subsubsection \<open>rule-sets\<close>
1522 ML \<open>val prep_rls' = LTool.prep_rls @{theory}\<close>
1524 setup \<open>KEStore_Elems.add_rlss
1525 [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
1526 ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*)
1527 ("expand", (Context.theory_name @{theory}, prep_rls' expand)),
1528 ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)),
1529 ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
1531 ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)),
1532 ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)),
1533 ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)),
1534 ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)),
1535 ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
1537 ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)),
1538 ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)),
1539 ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)),
1540 ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)),
1541 ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
1543 ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)),
1544 ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)),
1545 ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)),
1546 ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)),
1547 ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
1549 ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)),
1550 ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)),
1551 ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)),
1552 ("make_rat_poly_with_parentheses",
1553 (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close>
1555 subsubsection \<open>predicates\<close>
1556 setup \<open>KEStore_Elems.add_calcs
1557 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
1558 eval_is_polyrat_in "#eval_is_polyrat_in")),
1559 ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
1560 ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
1561 ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
1562 ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
1563 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
1564 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))]\<close>
1566 subsubsection \<open>problems\<close>
1567 setup \<open>KEStore_Elems.add_pbts
1568 [(Specify.prep_pbt thy "pbl_simp_poly" [] Celem.e_pblID
1569 (["polynomial","simplification"],
1570 [("#Given" ,["Term t_t"]),
1571 ("#Where" ,["t_t is_polyexp"]),
1572 ("#Find" ,["normalform n_n"])],
1573 Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)
1574 Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
1575 SOME "Simplify t_t",
1576 [["simplification","for_polynomials"]]))]\<close>
1578 subsubsection \<open>methods\<close>
1579 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
1581 "simplify term = ((Rewrite_Set ''norm_Poly'' False) term)"
1582 setup \<open>KEStore_Elems.add_mets
1583 [Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
1584 (["simplification","for_polynomials"],
1585 [("#Given" ,["Term t_t"]),
1586 ("#Where" ,["t_t is_polyexp"]),
1587 ("#Find" ,["normalform n_n"])],
1588 {rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls,
1589 prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
1590 [(*for preds in where_*)
1591 Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
1592 crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
1593 "Script SimplifyScript (t_t::real) = " ^
1594 " ((Rewrite_Set ''norm_Poly'' False) t_t)")]