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")
64 subsection \<open>theorems not yet adopted from Isabelle\<close>
65 axiomatization where (*.not contained in Isabelle2002,
66 stated as axioms, TODO: prove as theorems;
67 theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
69 realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
70 realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
71 realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
72 realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
74 realpow_oneI: "r ^^^ 1 = r" and
75 realpow_zeroI: "r ^^^ 0 = 1" and
76 realpow_eq_oneI: "1 ^^^ n = 1" and
77 realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
78 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
79 (r * s) ^^^ n = r ^^^ n * s ^^^ n" and
80 realpow_minus_oneI: "(- 1) ^^^ (2 * n) = 1" and
81 real_diff_0: "0 - x = - (x::real)" and
83 realpow_twoI: "r ^^^ 2 = r * r" and
84 realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
85 realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
86 realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
87 realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
88 realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
89 realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
90 realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
91 realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
92 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
93 ==> r ^^^ n = r * r ^^^ (n + -1)" and
94 realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
97 realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
98 realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
102 real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
103 real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
104 real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
105 real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
106 real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
107 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
108 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
109 real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
110 real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
112 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
113 (a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
114 real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
116 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
117 (a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
119 real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
120 *(a^^^2 + 2*a*b + b^^^2)" and
121 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
122 (a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
123 + b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
124 real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
125 real_diff_minus: "a - b = a + -1 * b" and
126 real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
127 real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
128 (*WN071229 changed for Schaerding -----vvv*)
129 (*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
130 real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
131 (*WN071229 changed for Schaerding -----^^^*)
132 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
133 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
134 real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
135 real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
136 real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
137 real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
138 real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
139 real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
140 real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
141 real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
142 real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
143 real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
145 real_num_collect: "[| l is_const; m is_const |] ==>
146 l * n + m * n = (l + m) * n" and
147 (* FIXME.MG.0401: replace 'real_num_collect_assoc'
148 by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
149 real_num_collect_assoc: "[| l is_const; m is_const |] ==>
150 l * n + (m * n + k) = (l + m) * n + k" and
151 real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
152 l * n + (m * n + k) = (l + m)
154 real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
155 (k + m * n) + l * n = k + (l + m) * n" and
156 real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
157 (* FIXME.MG.0401: replace 'real_one_collect_assoc'
158 by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
159 real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
161 real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
162 real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
164 (* FIXME.MG.0401: replace 'real_mult_2_assoc'
165 by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
166 real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
167 real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
168 real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
170 real_mult_left_commute: "z1 * (z2 * z3) = z2 * (z1 * z3)" and
171 real_mult_minus1: "-1 * z = - (z::real)" and
172 real_mult_2: "2 * z = z + (z::real)" 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>
181 ["Groups.plus_class.plus", "Groups.minus_class.minus",
182 "Rings.divide_class.divide", "Groups.times_class.times",
185 subsubsection \<open>for predicates in specifications (ML)\<close>
187 (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)
188 (*. a 'monomial t in variable v' is a term t with
189 either (1) v NOT existent in t, or (2) v contained in t,
191 if (2) then v is a factor on the very right, ev. with exponent.*)
192 fun factor_right_deg (*case 2*)
193 (Const ("Groups.times_class.times", _) $ t1 $ (Const ("Prog_Expr.pow",_) $ vv $ Free (d, _))) v =
194 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (TermC.int_of_str d) else NONE
195 | factor_right_deg (Const ("Prog_Expr.pow",_) $ vv $ Free (d,_)) v =
196 if (vv = v) then SOME (TermC.int_of_str d) else NONE
197 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =
198 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
199 | factor_right_deg vv v =
200 if (vv = v) then SOME 1 else NONE;
201 fun mono_deg_in m v = (*case 1*)
202 if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;
204 fun expand_deg_in t v =
206 fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) =
207 (case mono_deg_in t2 v of (* $ is left associative*)
208 SOME d' => edi d' d' t1 | NONE => NONE)
209 | edi ~1 ~1 (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
210 (case mono_deg_in t2 v of
211 SOME d' => edi d' d' t1 | NONE => NONE)
212 | edi d dmax (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
213 (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)
214 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
216 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
217 (case mono_deg_in t2 v of
218 SOME d' => (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)
219 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
222 (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)
223 | edi d dmax t = (*basecase last*)
224 (case mono_deg_in t v of
225 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
229 fun poly_deg_in t v =
231 fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
232 (case mono_deg_in t2 v of (* $ is left associative *)
233 SOME d' => edi d' d' t1
235 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
236 (case mono_deg_in t2 v of
237 SOME d' => (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)
238 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
241 (case mono_deg_in t v of
244 | edi d dmax t = (* basecase last *)
245 (case mono_deg_in t v of
247 if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
252 subsubsection \<open>for hard-coded AC rewriting (MG)\<close>
254 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
256 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
257 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
258 (* Polynom --> List von Monomen *)
259 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
260 (poly2list t1) @ (poly2list t2)
263 (* Monom --> Liste von Variablen *)
264 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
265 (monom2list t1) @ (monom2list t2)
266 | monom2list t = [t];
268 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
269 fun get_basStr (Const ("Prog_Expr.pow",_) $ Free (str, _) $ _) = str
270 | get_basStr (Free (str, _)) = str
271 | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
273 raise ERROR("get_basStr: called with t= "^(UnparseC.term t));*)
275 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
276 fun get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ Free (str, _)) = str
277 | get_potStr (Const ("Prog_Expr.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
278 | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
279 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
281 raise ERROR("get_potStr: called with t= "^(UnparseC.term t));*)
283 (* Umgekehrte string_ord *)
284 val string_ord_rev = rev_order o string_ord;
286 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
287 innerhalb eines Monomes:
288 - zuerst lexikographisch nach Variablenname
289 - wenn gleich: nach steigender Potenz *)
290 fun var_ord (a,b: term) = prod_ord string_ord string_ord
291 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
293 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
294 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
295 - zuerst lexikographisch nach Variablenname
296 - wenn gleich: nach sinkender Potenz*)
297 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
298 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
301 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
302 val sort_varList = sort var_ord;
304 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
305 Argumente in eine Liste *)
306 fun args u : term list =
307 let fun stripc (f$t, ts) = stripc (f, t::ts)
308 | stripc (t as Free _, ts) = (t::ts)
309 | stripc (_, ts) = ts
310 in stripc (u, []) end;
312 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
313 (keine Variablen) enthaelt *)
314 fun filter_num [] = true
315 | filter_num [Free x] = if (TermC.is_num (Free x)) then true
317 | filter_num ((Free _)::_) = false
319 (filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;
321 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
322 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
323 fun is_nums t = filter_num [t];
325 (* Berechnet den Gesamtgrad eines Monoms *)
327 fun counter (n, []) = n
328 | counter (n, x :: xs) =
333 (Const ("Prog_Expr.pow", _) $ Free _ $ Free (str_h, T)) =>
334 if (is_nums (Free (str_h, T))) then
335 counter (n + (the (TermC.int_opt_of_string str_h)), xs)
336 else counter (n + 1000, xs) (*FIXME.MG?!*)
337 | (Const ("Prog_Expr.pow", _) $ Free _ $ _ ) =>
338 counter (n + 1000, xs) (*FIXME.MG?!*)
339 | (Free _) => counter (n + 1, xs)
340 (*| _ => raise ERROR("monom_degree: called with factor: "^(UnparseC.term x)))*)
341 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
343 fun monom_degree l = counter (0, l)
346 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
347 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
348 werden jedoch dabei ignoriert (uebersprungen) *)
349 fun dict_cond_ord _ _ ([], []) = EQUAL
350 | dict_cond_ord _ _ ([], _ :: _) = LESS
351 | dict_cond_ord _ _ (_ :: _, []) = GREATER
352 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
353 (case (cond x, cond y) of
354 (false, false) => (case elem_ord (x, y) of
355 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
357 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
358 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
359 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
361 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
362 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
363 dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
364 fun degree_ord (xs, ys) =
365 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
366 ((monom_degree xs, xs), (monom_degree ys, ys));
368 fun hd_str str = substring (str, 0, 1);
369 fun tl_str str = substring (str, 1, (size str) - 1);
371 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
372 fun get_koeff_of_mon [] = raise ERROR("get_koeff_of_mon: called with l = []")
373 | get_koeff_of_mon (x::_) = if is_nums x then SOME x else NONE;
375 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
376 fun koeff2ordStr (SOME x) = (case x of
378 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
380 | _ => "aaa") (* "num.Ausdruck" --> gross *)
381 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
383 (* Order zum Vergleich von Koeffizienten (strings):
384 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
385 fun compare_koeff_ord (xs, ys) =
386 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
387 (koeff2ordStr o get_koeff_of_mon) ys);
389 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
390 fun koeff_degree_ord (xs, ys) =
391 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
393 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
395 val sort_monList = sort koeff_degree_ord;
397 (* Alternativ zu degree_ord koennte auch die viel einfachere und
398 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
399 fuer unsere Zwecke geeignet!
401 fun simple_ord (al,bl: term list) = dict_ord string_ord
402 (map get_basStr al, map get_basStr bl);
404 val sort_monList = sort simple_ord; *)
406 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
407 (mit gewuenschtem Typen T) *)
408 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
409 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
410 fun binop op_ t1 t2 = op_ $ t1 $ t2;
411 fun create_prod T (a,b) = binop (mult T) a b;
412 fun create_sum T (a,b) = binop (plus T) a b;
414 (* löscht letztes Element einer Liste *)
415 fun drop_last l = take ((length l)-1,l);
417 (* Liste von Variablen --> Monom *)
418 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
420 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
421 gleiche Monome zusammengefasst werden können (collect_numerals)!
422 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
424 (* Liste von Monomen --> Polynom *)
425 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
427 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
428 bessere Darstellung, da keine Klammern sichtbar!
429 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
431 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
432 fun sort_variables t =
434 val ll = map monom2list (poly2list t);
435 val lls = map sort_varList ll;
437 val ls = map (create_monom T) lls;
438 in create_polynom T ls end;
440 (* sorts the monoms of an expanded and variable-sorted polynomial
444 val ll = map monom2list (poly2list t);
445 val lls = sort_monList ll;
447 val ls = map (create_monom T) lls;
448 in create_polynom T ls end;
451 subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>
453 local (*. for make_polynomial .*)
455 open Term; (* for type order = EQUAL | LESS | GREATER *)
457 fun pr_ord EQUAL = "EQUAL"
458 | pr_ord LESS = "LESS"
459 | pr_ord GREATER = "GREATER";
461 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
463 "Prog_Expr.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
464 | _ => (((a, 0), T), 0))
465 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)
466 | dest_hd' (Var v) = (v, 2)
467 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
468 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
469 | dest_hd' t = raise TERM ("dest_hd'", [t]);
471 fun size_of_term' (Const(str,_) $ t) =
472 if "Prog_Expr.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
473 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
474 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
475 | size_of_term' _ = 1;
477 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
478 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
479 | term_ord' pr thy (t, u) =
482 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
483 val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
484 commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
485 val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
486 commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
487 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
488 string_of_int (size_of_term' u) ^ ")");
489 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
490 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
491 val _ = tracing ("-------");
494 case int_ord (size_of_term' t, size_of_term' u) of
496 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
497 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
501 and hd_ord (f, g) = (* ~ term.ML *)
502 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
503 and terms_ord _ pr (ts, us) =
504 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
508 fun ord_make_polynomial (pr:bool) thy (_: subst) tu =
509 (term_ord' pr thy(***) tu = LESS );
513 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
514 [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
517 subsection \<open>predicates\<close>
518 subsubsection \<open>in specifications\<close>
520 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
521 fun is_polyrat_in t v =
523 fun finddivide (_ $ _ $ _ $ _) _ = raise ERROR("is_polyrat_in:")
524 (* at the moment there is no term like this, but ....*)
525 | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)
526 | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
527 | finddivide (_ $ t1) v = finddivide t1 v
528 | finddivide _ _ = false;
529 in finddivide t v end;
531 fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;
532 fun is_poly_in t v = case poly_deg_in t v of SOME _ => true | NONE => false;
533 fun has_degree_in t v = case expand_deg_in t v of SOME d => d | NONE => ~1;
535 (*.the expression contains + - * ^ only ?
536 this is weaker than 'is_polynomial' !.*)
537 fun is_polyexp (Free _) = true
538 | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)
539 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
540 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
541 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
542 | is_polyexp (Const ("Prog_Expr.pow",_) $ Free _ $ Free _) = true
543 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
544 ((is_polyexp t1) andalso (is_polyexp t2))
545 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
546 ((is_polyexp t1) andalso (is_polyexp t2))
547 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
548 ((is_polyexp t1) andalso (is_polyexp t2))
549 | is_polyexp (Const ("Prog_Expr.pow",_) $ t1 $ t2) =
550 ((is_polyexp t1) andalso (is_polyexp t2))
551 | is_polyexp _ = false;
554 subsubsection \<open>for hard-coded AC rewriting\<close>
556 (* auch Klammerung muss übereinstimmen;
557 sort_variables klammert Produkte rechtslastig*)
558 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
560 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
563 subsection \<open>evaluations functions\<close>
564 subsubsection \<open>for predicates\<close>
566 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
568 then SOME ((UnparseC.term p) ^ " = True",
569 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
570 else SOME ((UnparseC.term p) ^ " = True",
571 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
572 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
574 (*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
575 fun eval_is_expanded_in _ _
576 (p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
577 if is_expanded_in t v
578 then SOME ((UnparseC.term p) ^ " = True",
579 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
580 else SOME ((UnparseC.term p) ^ " = True",
581 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
582 | eval_is_expanded_in _ _ _ _ = NONE;
584 (*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
585 fun eval_is_poly_in _ _
586 (p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
588 then SOME ((UnparseC.term p) ^ " = True",
589 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
590 else SOME ((UnparseC.term p) ^ " = True",
591 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
592 | eval_is_poly_in _ _ _ _ = NONE;
594 (*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
595 fun eval_has_degree_in _ _
596 (p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
597 let val d = has_degree_in t v
598 val d' = TermC.term_of_num HOLogic.realT d
599 in SOME ((UnparseC.term p) ^ " = " ^ (string_of_int d),
600 HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
602 | eval_has_degree_in _ _ _ _ = NONE;
604 (*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
605 fun eval_is_polyexp (thmid:string) _
606 (t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
608 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
609 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
610 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
611 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
612 | eval_is_polyexp _ _ _ _ = NONE;
615 subsubsection \<open>for hard-coded AC rewriting\<close>
618 (*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
619 fun eval_is_addUnordered (thmid:string) _
620 (t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
621 if is_addUnordered arg
622 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
623 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
624 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
625 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
626 | eval_is_addUnordered _ _ _ _ = NONE;
628 fun eval_is_multUnordered (thmid:string) _
629 (t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
630 if is_multUnordered arg
631 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
632 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
633 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
634 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
635 | eval_is_multUnordered _ _ _ _ = NONE;
637 setup \<open>KEStore_Elems.add_calcs
638 [("is_polyrat_in", ("Poly.is'_polyrat'_in",
639 eval_is_polyrat_in "#eval_is_polyrat_in")),
640 ("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
641 ("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
642 ("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
643 ("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
644 ("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
645 ("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))]\<close>
647 subsection \<open>rule-sets\<close>
648 subsubsection \<open>without specific order\<close>
650 (* used only for merge *)
651 val calculate_Poly = Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty [];
653 (*.for evaluation of conditions in rewrite rules.*)
654 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls
655 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
656 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
657 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
658 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
659 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
660 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")];
662 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls
663 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
664 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
665 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
666 Rule.Eval ("Groups.minus_class.minus", (**)eval_binop "#sub_"),
667 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
668 Rule.Eval ("Prog_Expr.pow" , (**)eval_binop "#power_")];
672 Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
673 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
674 rules = [Rule.Thm ("distrib_right" , ThmC.numerals_to_Free @{thm distrib_right}),
675 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
676 Rule.Thm ("distrib_left", ThmC.numerals_to_Free @{thm distrib_left})
677 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
678 ], scr = Rule.Empty_Prog};
681 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
682 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
684 [Rule.Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}),
685 (*"a - b = a + -1 * b"*)
686 Rule.Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
687 (*- ?z = "-1 * ?z"*)],
688 scr = Rule.Empty_Prog};
691 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
692 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
693 erls = Rule_Set.empty,srls = Rule_Set.Empty,
694 calc = [], errpatts = [],
696 [Rule.Thm ("real_plus_binom_pow4", ThmC.numerals_to_Free @{thm real_plus_binom_pow4}),
697 (*"(a + b)^^^4 = ... "*)
698 Rule.Thm ("real_plus_binom_pow5",ThmC.numerals_to_Free @{thm real_plus_binom_pow5}),
699 (*"(a + b)^^^5 = ... "*)
700 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
701 (*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
702 (*WN071229 changed/removed for Schaerding -----vvv*)
703 (*Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),*)
704 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
705 Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
706 (*"(a + b)^^^2 = (a + b) * (a + b)"*)
707 (*Rule.Thm ("real_plus_minus_binom1_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),*)
708 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
709 (*Rule.Thm ("real_plus_minus_binom2_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),*)
710 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
711 (*WN071229 changed/removed for Schaerding -----^^^*)
713 Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
714 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
715 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
716 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
718 Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
719 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
720 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
721 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
722 ], scr = Rule.Empty_Prog};
724 val expand_poly_rat_ =
725 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
726 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
727 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
728 [Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")
730 srls = Rule_Set.Empty,
731 calc = [], errpatts = [],
733 [Rule.Thm ("real_plus_binom_pow4_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow4_poly}),
734 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
735 Rule.Thm ("real_plus_binom_pow5_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow5_poly}),
736 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
737 Rule.Thm ("real_plus_binom_pow2_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow2_poly}),
738 (*"[| a is_polyexp; b is_polyexp |] ==>
739 (a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
740 Rule.Thm ("real_plus_binom_pow3_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow3_poly}),
741 (*"[| a is_polyexp; b is_polyexp |] ==>
742 (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
743 Rule.Thm ("real_plus_minus_binom1_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),
744 (*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
745 Rule.Thm ("real_plus_minus_binom2_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),
746 (*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
748 Rule.Thm ("real_add_mult_distrib_poly",
749 ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}),
750 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
751 Rule.Thm("real_add_mult_distrib2_poly",
752 ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}),
753 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
755 Rule.Thm ("realpow_multI_poly", ThmC.numerals_to_Free @{thm realpow_multI_poly}),
756 (*"[| r is_polyexp; s is_polyexp |] ==>
757 (r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
758 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
759 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
760 ], scr = Rule.Empty_Prog};
762 val simplify_power_ =
763 Rule_Def.Repeat{id = "simplify_power_", preconds = [],
764 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
765 erls = Rule_Set.empty, srls = Rule_Set.Empty,
766 calc = [], errpatts = [],
767 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
768 a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
769 Rule.Thm ("sym_realpow_twoI",
770 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
771 (*"r * r = r ^^^ 2"*)
772 Rule.Thm ("realpow_twoI_assoc_l",ThmC.numerals_to_Free @{thm realpow_twoI_assoc_l}),
773 (*"r * (r * s) = r ^^^ 2 * s"*)
775 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
776 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
777 Rule.Thm ("realpow_plus_1_assoc_l",
778 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
779 (*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
780 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
781 Rule.Thm ("realpow_plus_1_assoc_l2",
782 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
783 (*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
785 Rule.Thm ("sym_realpow_addI",
786 ThmC.numerals_to_Free (@{thm realpow_addI} RS @{thm sym})),
787 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
788 Rule.Thm ("realpow_addI_assoc_l",ThmC.numerals_to_Free @{thm realpow_addI_assoc_l}),
789 (*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
791 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
792 "r * r = r ^^^ 2" wenn r=a^^^b*)
793 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
794 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
795 ], scr = Rule.Empty_Prog};
797 val calc_add_mult_pow_ =
798 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
799 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
800 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
801 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
802 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
803 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
806 rules = [Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
807 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
808 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
809 ], scr = Rule.Empty_Prog};
811 val reduce_012_mult_ =
812 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
813 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
814 erls = Rule_Set.empty,srls = Rule_Set.Empty,
815 calc = [], errpatts = [],
816 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
817 Rule.Thm ("mult_1_right",ThmC.numerals_to_Free @{thm mult_1_right}),
818 (*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
819 Rule.Thm ("realpow_zeroI",ThmC.numerals_to_Free @{thm realpow_zeroI}),
820 (*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
821 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
823 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
825 ], scr = Rule.Empty_Prog};
827 val collect_numerals_ =
828 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
829 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
830 erls = Atools_erls, srls = Rule_Set.Empty,
831 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_"))
834 [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
835 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
836 Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
837 (*"[| l is_const; m is_const |] ==> \
838 \(k + m * n) + l * n = k + (l + m)*n"*)
839 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
840 (*"m is_const ==> n + m * n = (1 + m) * n"*)
841 Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
842 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
844 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
846 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
847 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
848 Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
849 (*"(k + z1) + z1 = k + 2 * z1"*)
850 Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym}))
851 (*"z1 + z1 = 2 * z1"*)
852 ], scr = Rule.Empty_Prog};
855 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
856 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
857 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
858 rules = [Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
860 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
862 Rule.Thm ("mult_zero_right",ThmC.numerals_to_Free @{thm mult_zero_right}),
864 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
866 Rule.Thm ("add_0_right",ThmC.numerals_to_Free @{thm add_0_right}),
867 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
869 (*Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI})*)
871 Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
873 ], scr = Rule.Empty_Prog};
875 val discard_parentheses1 =
876 Rule_Set.append_rules "discard_parentheses1" Rule_Set.empty
877 [Rule.Thm ("sym_mult.assoc",
878 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
879 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
880 (*Rule.Thm ("sym_add.assoc",
881 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))*)
882 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
886 Rule_Def.Repeat{id = "expand_poly", preconds = [],
887 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
888 erls = Rule_Set.empty,srls = Rule_Set.Empty,
889 calc = [], errpatts = [],
891 rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
892 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
893 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
894 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
895 (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1),
896 ....... 18.3.03 undefined???*)
898 Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
899 (*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
900 Rule.Thm ("real_minus_binom_pow2_p",ThmC.numerals_to_Free @{thm real_minus_binom_pow2_p}),
901 (*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
902 Rule.Thm ("real_plus_minus_binom1_p",
903 ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
904 (*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
905 Rule.Thm ("real_plus_minus_binom2_p",
906 ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
907 (*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
909 Rule.Thm ("minus_minus",ThmC.numerals_to_Free @{thm minus_minus}),
911 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
912 (*"a - b = a + -1 * b"*)
913 Rule.Thm ("sym_real_mult_minus1",
914 ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
917 (*Rule.Thm ("real_minus_add_distrib",
918 ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
919 (*"- (?x + ?y) = - ?x + - ?y"*)
920 (*Rule.Thm ("real_diff_plus",ThmC.numerals_to_Free @{thm real_diff_plus})*)
922 ], scr = Rule.Empty_Prog};
925 Rule_Def.Repeat{id = "simplify_power", preconds = [],
926 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
927 erls = Rule_Set.empty, srls = Rule_Set.Empty,
928 calc = [], errpatts = [],
929 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
930 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
932 Rule.Thm ("sym_realpow_twoI",
933 ThmC.numerals_to_Free( @{thm realpow_twoI} RS @{thm sym})),
934 (*"r1 * r1 = r1 ^^^ 2"*)
935 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
936 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
937 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
938 (*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
939 Rule.Thm ("sym_realpow_addI",
940 ThmC.numerals_to_Free (@{thm realpow_addI} RS @{thm sym})),
941 (*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
942 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
944 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
946 ], scr = Rule.Empty_Prog};
948 val collect_numerals =
949 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
950 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
951 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
952 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
953 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
954 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
956 rules = [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
957 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
958 Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
959 (*"[| l is_const; m is_const |] ==>
960 l * n + (m * n + k) = (l + m) * n + k"*)
961 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
962 (*"m is_const ==> n + m * n = (1 + m) * n"*)
963 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
964 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
965 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
966 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
967 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
968 ], scr = Rule.Empty_Prog};
970 Rule_Def.Repeat{id = "reduce_012", preconds = [],
971 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
972 erls = Rule_Set.empty,srls = Rule_Set.Empty,
973 calc = [], errpatts = [],
974 rules = [Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
976 (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),14.3.03*)
978 Rule.Thm ("minus_mult_left",
979 ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
980 (*- (?x * ?y) = "- ?x * ?y"*)
981 (*Rule.Thm ("real_minus_mult_cancel",
982 ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
983 (*"- ?x * - ?y = ?x * ?y"*)---*)
984 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
986 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
988 Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
990 Rule.Thm ("sym_real_mult_2",
991 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
992 (*"z1 + z1 = 2 * z1"*)
993 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc})
994 (*"z1 + (z1 + k) = 2 * z1 + k"*)
995 ], scr = Rule.Empty_Prog};
997 val discard_parentheses =
998 Rule_Set.append_rules "discard_parentheses" Rule_Set.empty
999 [Rule.Thm ("sym_mult.assoc",
1000 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym})),
1001 Rule.Thm ("sym_add.assoc",
1002 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
1005 subsubsection \<open>hard-coded AC rewriting\<close>
1007 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1008 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1009 val order_add_mult =
1010 Rule_Def.Repeat{id = "order_add_mult", preconds = [],
1011 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
1012 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1013 calc = [], errpatts = [],
1014 rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1016 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1017 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1018 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1019 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1020 Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
1022 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1023 (*x + (y + z) = y + (x + z)*)
1024 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
1025 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1026 ], scr = Rule.Empty_Prog};
1027 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1028 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1030 Rule_Def.Repeat{id = "order_mult", preconds = [],
1031 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
1032 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1033 calc = [], errpatts = [],
1034 rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1036 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1037 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1038 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc})
1039 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1040 ], scr = Rule.Empty_Prog};
1043 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1044 []:(Rule.rule * (term * term list)) list;
1045 fun init_state (_: term) = Rule_Set.e_rrlsstate;
1046 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1047 ([]:(Rule.rule * (term * term list)) list);
1048 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1049 fun normal_form t = SOME (sort_variables t, []: term list);
1052 Rule_Set.Rrls {id = "order_mult_",
1054 (* ?p matched with the current term gives an environment,
1055 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1056 [([TermC.parse_patt thy "?p is_multUnordered"],
1057 TermC.parse_patt thy "?p :: real")],
1058 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1059 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1060 [Rule.Eval ("Poly.is'_multUnordered",
1061 eval_is_multUnordered "")],
1062 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1063 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1064 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1065 ("POWER" , ("Prog_Expr.pow", (**)eval_binop "#power_"))],
1067 scr = Rule.Rfuns {init_state = init_state,
1068 normal_form = normal_form,
1069 locate_rule = locate_rule,
1070 next_rule = next_rule,
1071 attach_form = attach_form}};
1072 val order_mult_rls_ =
1073 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
1074 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1075 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1076 calc = [], errpatts = [],
1077 rules = [Rule.Rls_ order_mult_
1078 ], scr = Rule.Empty_Prog};
1082 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1083 []: (Rule.rule * (term * term list)) list;
1084 fun init_state (_: term) = Rule_Set.e_rrlsstate;
1085 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1086 ([]: (Rule.rule * (term * term list)) list);
1087 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1088 fun normal_form t = SOME (sort_monoms t,[]: term list);
1091 Rule_Set.Rrls {id = "order_add_",
1092 prepat = (*WN.18.6.03 Preconditions und Pattern,
1093 die beide passen muessen, damit das Rule_Set.Rrls angewandt wird*)
1094 [([TermC.parse_patt @{theory} "?p is_addUnordered"],
1095 TermC.parse_patt @{theory} "?p :: real"
1096 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1097 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1098 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1099 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
1100 [Rule.Eval ("Poly.is'_addUnordered", eval_is_addUnordered "")],
1101 calc = [("PLUS" ,("Groups.plus_class.plus", (**)eval_binop "#add_")),
1102 ("TIMES" ,("Groups.times_class.times", (**)eval_binop "#mult_")),
1103 ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1104 ("POWER" ,("Prog_Expr.pow" , (**)eval_binop "#power_"))],
1106 scr = Rule.Rfuns {init_state = init_state,
1107 normal_form = normal_form,
1108 locate_rule = locate_rule,
1109 next_rule = next_rule,
1110 attach_form = attach_form}};
1112 val order_add_rls_ =
1113 Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
1114 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1115 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1116 calc = [], errpatts = [],
1117 rules = [Rule.Rls_ order_add_
1118 ], scr = Rule.Empty_Prog};
1121 text \<open>rule-set make_polynomial also named norm_Poly:
1122 Rewrite order has not been implemented properly; the order is better in
1123 make_polynomial_in (coded in SML).
1124 Notes on state of development:
1125 \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
1126 \# migration Isabelle2002 --> 2011 weakened the rule set, see test
1127 --- Matthias Goldgruber 2003 rewrite orders ---, raise ERROR "ord_make_polynomial_in #16b"
1130 (*. see MG-DA.p.52ff .*)
1131 val make_polynomial(*MG.03, overwrites version from above,
1132 previously 'make_polynomial_'*) =
1133 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list,
1134 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1135 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
1136 rules = [Rule.Rls_ discard_minus,
1137 Rule.Rls_ expand_poly_,
1138 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1139 Rule.Rls_ order_mult_rls_,
1140 Rule.Rls_ simplify_power_,
1141 Rule.Rls_ calc_add_mult_pow_,
1142 Rule.Rls_ reduce_012_mult_,
1143 Rule.Rls_ order_add_rls_,
1144 Rule.Rls_ collect_numerals_,
1145 Rule.Rls_ reduce_012_,
1146 Rule.Rls_ discard_parentheses1
1148 scr = Rule.Empty_Prog
1152 val norm_Poly(*=make_polynomial*) =
1153 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list,
1154 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1155 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1156 rules = [Rule.Rls_ discard_minus,
1157 Rule.Rls_ expand_poly_,
1158 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1159 Rule.Rls_ order_mult_rls_,
1160 Rule.Rls_ simplify_power_,
1161 Rule.Rls_ calc_add_mult_pow_,
1162 Rule.Rls_ reduce_012_mult_,
1163 Rule.Rls_ order_add_rls_,
1164 Rule.Rls_ collect_numerals_,
1165 Rule.Rls_ reduce_012_,
1166 Rule.Rls_ discard_parentheses1
1168 scr = Rule.Empty_Prog
1172 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1
1173 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1174 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1175 val make_rat_poly_with_parentheses =
1176 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1177 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1178 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1179 rules = [Rule.Rls_ discard_minus,
1180 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1181 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1182 Rule.Rls_ order_mult_rls_,
1183 Rule.Rls_ simplify_power_,
1184 Rule.Rls_ calc_add_mult_pow_,
1185 Rule.Rls_ reduce_012_mult_,
1186 Rule.Rls_ order_add_rls_,
1187 Rule.Rls_ collect_numerals_,
1188 Rule.Rls_ reduce_012_
1189 (*Rule.Rls_ discard_parentheses1 *)
1191 scr = Rule.Empty_Prog
1195 (*.a minimal ruleset for reverse rewriting of factions [2];
1196 compare expand_binoms.*)
1198 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1199 erls = Atools_erls, srls = Rule_Set.Empty,
1200 calc = [(*("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1201 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1202 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))*)
1204 rules = [Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
1205 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1206 Rule.Thm ("real_plus_binom_times1" ,ThmC.numerals_to_Free @{thm real_plus_binom_times1}),
1207 (*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
1208 Rule.Thm ("real_plus_binom_times2" ,ThmC.numerals_to_Free @{thm real_plus_binom_times2}),
1209 (*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
1211 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
1213 Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
1214 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1215 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
1216 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1218 Rule.Thm ("mult.assoc", ThmC.numerals_to_Free @{thm mult.assoc}),
1219 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1220 Rule.Rls_ order_mult_rls_,
1221 (*Rule.Rls_ order_add_rls_,*)
1223 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1224 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1225 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
1227 Rule.Thm ("sym_realpow_twoI",
1228 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
1229 (*"r1 * r1 = r1 ^^^ 2"*)
1230 Rule.Thm ("sym_real_mult_2",
1231 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
1232 (*"z1 + z1 = 2 * z1"*)
1233 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
1234 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1236 Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
1237 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1238 Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
1239 (*"[| l is_const; m is_const |] ==>
1240 l * n + (m * n + k) = (l + m) * n + k"*)
1241 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
1242 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1243 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
1244 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1246 Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
1247 (*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
1249 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1250 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1251 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
1253 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
1254 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),(*"0 * z = 0"*)
1255 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left})(*0 + z = z*)
1257 (*Rule.Rls_ order_add_rls_*)
1260 scr = Rule.Empty_Prog};
1263 subsection \<open>rule-sets with explicit program for intermediate steps\<close>
1264 partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
1266 "expand_binoms_2 term = (
1268 (Try (Repeat (Rewrite ''real_plus_binom_pow2''))) #>
1269 (Try (Repeat (Rewrite ''real_plus_binom_times''))) #>
1270 (Try (Repeat (Rewrite ''real_minus_binom_pow2''))) #>
1271 (Try (Repeat (Rewrite ''real_minus_binom_times''))) #>
1272 (Try (Repeat (Rewrite ''real_plus_minus_binom1''))) #>
1273 (Try (Repeat (Rewrite ''real_plus_minus_binom2''))) #>
1275 (Try (Repeat (Rewrite ''mult_1_left''))) #>
1276 (Try (Repeat (Rewrite ''mult_zero_left''))) #>
1277 (Try (Repeat (Rewrite ''add_0_left''))) #>
1279 (Try (Repeat (Calculate ''PLUS''))) #>
1280 (Try (Repeat (Calculate ''TIMES''))) #>
1281 (Try (Repeat (Calculate ''POWER''))) #>
1283 (Try (Repeat (Rewrite ''sym_realpow_twoI''))) #>
1284 (Try (Repeat (Rewrite ''realpow_plus_1''))) #>
1285 (Try (Repeat (Rewrite ''sym_real_mult_2''))) #>
1286 (Try (Repeat (Rewrite ''real_mult_2_assoc''))) #>
1288 (Try (Repeat (Rewrite ''real_num_collect''))) #>
1289 (Try (Repeat (Rewrite ''real_num_collect_assoc''))) #>
1291 (Try (Repeat (Rewrite ''real_one_collect''))) #>
1292 (Try (Repeat (Rewrite ''real_one_collect_assoc''))) #>
1294 (Try (Repeat (Calculate ''PLUS''))) #>
1295 (Try (Repeat (Calculate ''TIMES''))) #>
1296 (Try (Repeat (Calculate ''POWER''))))
1300 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1301 erls = Atools_erls, srls = Rule_Set.Empty,
1302 calc = [("PLUS" , ("Groups.plus_class.plus", (**)eval_binop "#add_")),
1303 ("TIMES" , ("Groups.times_class.times", (**)eval_binop "#mult_")),
1304 ("POWER", ("Prog_Expr.pow", (**)eval_binop "#power_"))
1306 rules = [Rule.Thm ("real_plus_binom_pow2",
1307 ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
1308 (*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
1309 Rule.Thm ("real_plus_binom_times",
1310 ThmC.numerals_to_Free @{thm real_plus_binom_times}),
1311 (*"(a + b)*(a + b) = ...*)
1312 Rule.Thm ("real_minus_binom_pow2",
1313 ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
1314 (*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
1315 Rule.Thm ("real_minus_binom_times",
1316 ThmC.numerals_to_Free @{thm real_minus_binom_times}),
1317 (*"(a - b)*(a - b) = ...*)
1318 Rule.Thm ("real_plus_minus_binom1",
1319 ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
1320 (*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
1321 Rule.Thm ("real_plus_minus_binom2",
1322 ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
1323 (*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
1325 Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
1326 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1327 Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
1328 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1329 Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
1330 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1331 Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
1332 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1333 Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
1334 (*(a*b)^^^n = a^^^n * b^^^n*)
1335 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
1336 (* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
1337 Rule.Thm ("real_minus_binom_pow3",
1338 ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
1339 (* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
1342 (*Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
1343 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1344 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
1345 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1346 Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
1347 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1348 Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
1349 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1351 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
1353 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
1355 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),(*"0 + z = z"*)
1357 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1358 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1359 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_"),
1360 (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1362 Rule.Thm ("real_mult_left_commute",
1363 ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1364 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1365 Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
1366 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1367 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
1369 Rule.Thm ("sym_realpow_twoI",
1370 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
1371 (*"r1 * r1 = r1 ^^^ 2"*)
1372 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
1373 (*"r * r ^^^ n = r ^^^ (n + 1)"*)
1374 (*Rule.Thm ("sym_real_mult_2",
1375 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
1376 (*"z1 + z1 = 2 * z1"*)*)
1377 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
1378 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1380 Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
1381 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
1382 Rule.Thm ("real_num_collect_assoc",
1383 ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
1384 (*"[| l is_const; m is_const |] ==>
1385 l * n + (m * n + k) = (l + m) * n + k"*)
1386 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
1387 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1388 Rule.Thm ("real_one_collect_assoc",
1389 ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
1390 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1392 Rule.Eval ("Groups.plus_class.plus", (**)eval_binop "#add_"),
1393 Rule.Eval ("Groups.times_class.times", (**)eval_binop "#mult_"),
1394 Rule.Eval ("Prog_Expr.pow", (**)eval_binop "#power_")
1396 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})
1400 subsection \<open>add to Know_Store\<close>
1401 subsubsection \<open>rule-sets\<close>
1402 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
1404 setup \<open>KEStore_Elems.add_rlss
1405 [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
1406 ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*)
1407 ("expand", (Context.theory_name @{theory}, prep_rls' expand)),
1408 ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)),
1409 ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
1411 ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)),
1412 ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)),
1413 ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)),
1414 ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)),
1415 ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
1417 ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)),
1418 ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)),
1419 ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)),
1420 ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)),
1421 ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
1423 ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)),
1424 ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)),
1425 ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)),
1426 ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)),
1427 ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
1429 ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)),
1430 ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)),
1431 ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)),
1432 ("make_rat_poly_with_parentheses",
1433 (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close>
1435 subsection \<open>problems\<close>
1436 setup \<open>KEStore_Elems.add_pbts
1437 [(Problem.prep_input thy "pbl_simp_poly" [] Problem.id_empty
1438 (["polynomial", "simplification"],
1439 [("#Given" ,["Term t_t"]),
1440 ("#Where" ,["t_t is_polyexp"]),
1441 ("#Find" ,["normalform n_n"])],
1442 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
1443 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp "")],
1444 SOME "Simplify t_t",
1445 [["simplification", "for_polynomials"]]))]\<close>
1447 subsection \<open>methods\<close>
1449 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
1451 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
1452 setup \<open>KEStore_Elems.add_mets
1453 [MethodC.prep_input thy "met_simp_poly" [] MethodC.id_empty
1454 (["simplification", "for_polynomials"],
1455 [("#Given" ,["Term t_t"]),
1456 ("#Where" ,["t_t is_polyexp"]),
1457 ("#Find" ,["normalform n_n"])],
1458 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1459 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1460 [(*for preds in where_*)
1461 Rule.Eval ("Poly.is'_polyexp", eval_is_polyexp"")],
1462 crls = Rule_Set.empty, errpats = [], nrls = norm_Poly},
1463 @{thm simplify.simps})]