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 \<up> 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 \<up> 1 + 25 * x \<up> 2"
34 [1]: "11 + 0 * x \<up> 1 + 1 * x \<up> 2"
35 [2]: "x + (-50) * x \<up> 3"
36 [2]: "(-1) * x * y \<up> 2 + 7 * x \<up> 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 \<up> 2 - 2 * a * b + b \<up> 2"
42 "4 * x \<up> 2 - 9 * y \<up> 2"
43 [4] 'polynomial_in' (Polynom in):
44 polynomial in 1 variable with arbitrary coefficients
45 examples: "2 * x + (-50) * x \<up> 3" (poly in x)
46 "(u + v) + (2 * u \<up> 2) * a + (-u) * a \<up> 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 \<up> 3" (expanded in x)
50 "(u + v) + (2 * u \<up> 2) * a - u * a \<up> 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 \<up> instead of ^ in 'xxx' in Isabelle2002.*)
69 realpow_pow: "(a \<up> b) \<up> c = a \<up> (b * c)" and
70 realpow_addI: "r \<up> (n + m) = r \<up> n * r \<up> m" and
71 realpow_addI_assoc_l: "r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s" and
72 realpow_addI_assoc_r: "s * r \<up> n * r \<up> m = s * r \<up> (n + m)" and
74 realpow_oneI: "r \<up> 1 = r" and
75 realpow_zeroI: "r \<up> 0 = 1" and
76 realpow_eq_oneI: "1 \<up> n = 1" and
77 realpow_multI: "(r * s) \<up> n = r \<up> n * s \<up> n" and
78 realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
79 (r * s) \<up> n = r \<up> n * s \<up> n" and
80 realpow_minus_oneI: "(- 1) \<up> (2 * n) = 1" and
81 real_diff_0: "0 - x = - (x::real)" and
83 realpow_twoI: "r \<up> 2 = r * r" and
84 realpow_twoI_assoc_l: "r * (r * s) = r \<up> 2 * s" and
85 realpow_twoI_assoc_r: "s * r * r = s * r \<up> 2" and
86 realpow_two_atom: "r is_atom ==> r * r = r \<up> 2" and
87 realpow_plus_1: "r * r \<up> n = r \<up> (n + 1)" and
88 realpow_plus_1_assoc_l: "r * (r \<up> m * s) = r \<up> (1 + m) * s" and
89 realpow_plus_1_assoc_l2: "r \<up> m * (r * s) = r \<up> (1 + m) * s" and
90 realpow_plus_1_assoc_r: "s * r * r \<up> m = s * r \<up> (1 + m)" and
91 realpow_plus_1_atom: "r is_atom ==> r * r \<up> n = r \<up> (1 + n)" and
92 realpow_def_atom: "[| Not (r is_atom); 1 < n |]
93 ==> r \<up> n = r * r \<up> (n + -1)" and
94 realpow_addI_atom: "r is_atom ==> r \<up> n * r \<up> m = r \<up> (n + m)" and
97 realpow_minus_even: "n is_even ==> (- r) \<up> n = r \<up> n" and
98 realpow_minus_odd: "Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> 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) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" and
107 real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
108 (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" and
109 real_minus_binom_pow3: "(a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3" and
110 real_minus_binom_pow3_p: "(a + -1 * b) \<up> 3 = a \<up> 3 + -3*a \<up> 2*b + 3*a*b \<up> 2 +
112 (* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
113 (a + b) \<up> n = (a + b) * (a + b)\<up>(n - 1)" *)
114 real_plus_binom_pow4: "(a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
116 real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
117 (a + b) \<up> 4 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
119 real_plus_binom_pow5: "(a + b) \<up> 5 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3)
120 *(a \<up> 2 + 2*a*b + b \<up> 2)" and
121 real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
122 (a + b) \<up> 5 = (a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2
123 + b \<up> 3)*(a \<up> 2 + 2*a*b + b \<up> 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 \<up> 2 + 2*a*b + b \<up> 2" and
127 real_minus_binom_times: "(a - b)*(a - b) = a \<up> 2 - 2*a*b + b \<up> 2" and
128 (*WN071229 changed for Schaerding -----vvv*)
129 (*real_plus_binom_pow2: "(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
130 real_plus_binom_pow2: "(a + b) \<up> 2 = (a + b) * (a + b)" and
131 (*WN071229 changed for Schaerding -----\<up>*)
132 real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
133 (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2" and
134 real_minus_binom_pow2: "(a - b) \<up> 2 = a \<up> 2 - 2*a*b + b \<up> 2" and
135 real_minus_binom_pow2_p: "(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2" and
136 real_plus_minus_binom1: "(a + b)*(a - b) = a \<up> 2 - b \<up> 2" and
137 real_plus_minus_binom1_p: "(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2" and
138 real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2" and
139 real_plus_minus_binom2: "(a - b)*(a + b) = a \<up> 2 - b \<up> 2" and
140 real_plus_minus_binom2_p: "(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2" and
141 real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2" and
142 real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2" and
143 real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 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"
178 subsection \<open>auxiliary functions\<close>
182 ["Groups.plus_class.plus", "Groups.minus_class.minus",
183 "Rings.divide_class.divide", "Groups.times_class.times",
184 "Transcendental.powr"];
186 subsubsection \<open>for predicates in specifications (ML)\<close>
188 (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)
189 (*. a "monomial t in variable v" is a term t with
190 either (1) v NOT existent in t, or (2) v contained in t,
192 if (2) then v is a factor on the very right, casually with exponent.*)
193 fun factor_right_deg (*case 2*)
194 (Const ("Groups.times_class.times", _) $
195 t1 $ (Const ("Transcendental.powr",_) $ vv $ num)) v =
196 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (snd (HOLogic.dest_number num))
198 | factor_right_deg (Const ("Transcendental.powr",_) $ vv $ num) v =
199 if (vv = v) then SOME (snd (HOLogic.dest_number num)) else NONE
200 | factor_right_deg (Const ("Groups.times_class.times",_) $ t1 $ vv) v =
201 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
202 | factor_right_deg vv v =
203 if (vv = v) then SOME 1 else NONE;
204 fun mono_deg_in m v = (*case 1*)
205 if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;
207 fun expand_deg_in t v =
209 fun edi ~1 ~1 (Const ("Groups.plus_class.plus", _) $ t1 $ t2) =
210 (case mono_deg_in t2 v of (* $ is left associative*)
211 SOME d' => edi d' d' t1 | NONE => NONE)
212 | edi ~1 ~1 (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
213 (case mono_deg_in t2 v of
214 SOME d' => edi d' d' t1 | NONE => NONE)
215 | edi d dmax (Const ("Groups.minus_class.minus", _) $ t1 $ t2) =
216 (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)
217 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
219 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
220 (case mono_deg_in t2 v of
221 SOME d' => (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)
222 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
225 (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)
226 | edi d dmax t = (*basecase last*)
227 (case mono_deg_in t v of
228 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
232 fun poly_deg_in t v =
234 fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
235 (case mono_deg_in t2 v of (* $ is left associative *)
236 SOME d' => edi d' d' t1
238 | edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
239 (case mono_deg_in t2 v of
240 SOME d' => (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)
241 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
244 (case mono_deg_in t v of
247 | edi d dmax t = (* basecase last *)
248 (case mono_deg_in t v of
250 if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
255 subsubsection \<open>for hard-coded AC rewriting (MG)\<close>
257 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
259 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
260 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
261 (* Polynom --> List von Monomen *)
262 fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
263 (poly2list t1) @ (poly2list t2)
266 (* Monom --> Liste von Variablen *)
267 fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
268 (monom2list t1) @ (monom2list t2)
269 | monom2list t = [t];
271 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
272 fun get_basStr (Const ("Transcendental.powr",_) $ Free (str, _) $ _) = str
273 | get_basStr (Free (str, _)) = str
274 | get_basStr (Const ("Num.numeral_class.numeral", _) $ _) = "123"
275 | get_basStr _ = "|||"; (* gross gewichtet; für Brüch ect. *)
277 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
278 fun get_potStr (Const ("Transcendental.powr",_) $ Free _ $ t) =
282 if TermC.is_num t then "123" else "|||" (* gross gewichtet *))
283 | get_potStr (Free (_, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
284 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
286 (* Umgekehrte string_ord *)
287 val string_ord_rev = rev_order o string_ord;
289 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
290 innerhalb eines Monomes:
291 - zuerst lexikographisch nach Variablenname
292 - wenn gleich: nach steigender Potenz *)
293 fun var_ord (a,b: term) = prod_ord string_ord string_ord
294 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
296 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
297 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
298 - zuerst lexikographisch nach Variablenname
299 - wenn gleich: nach sinkender Potenz*)
300 fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
301 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
304 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
305 val sort_varList = sort var_ord;
307 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
308 Argumente in eine Liste *)
309 fun args u : term list =
310 let fun stripc (f$t, ts) = stripc (f, t::ts)
311 | stripc (t as Free _, ts) = (t::ts)
312 | stripc (_, ts) = ts
313 in stripc (u, []) end;
315 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
316 (keine Variablen) enthaelt *)
317 fun filter_num ts = fold (curry and_) (map TermC.is_num ts) true
319 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
320 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
321 fun is_nums t = filter_num [t];
323 (* Berechnet den Gesamtgrad eines Monoms *)
325 fun counter (n, []) = n
326 | counter (n, x :: xs) =
327 if (is_nums x) then counter (n, xs)
330 (Const ("Transcendental.powr", _) $ Free _ $ Const ("Num.numeral_class.numeral", _) $ num) =>
331 counter (n + HOLogic.dest_numeral num, xs)
332 | (Const ("Transcendental.powr", _) $ Free _ $ _ ) => counter (n + 1000, xs) (*FIXME.MG?!*)
333 | (Free _) => counter (n + 1, xs)
334 (*| _ => raise ERROR("monom_degree: called with factor: "^(UnparseC.term x)))*)
335 | _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
337 fun monom_degree l = counter (0, l)
340 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
341 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
342 werden jedoch dabei ignoriert (uebersprungen) *)
343 fun dict_cond_ord _ _ ([], []) = EQUAL
344 | dict_cond_ord _ _ ([], _ :: _) = LESS
345 | dict_cond_ord _ _ (_ :: _, []) = GREATER
346 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
347 (case (cond x, cond y) of
348 (false, false) => (case elem_ord (x, y) of
349 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
351 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
352 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
353 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
355 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
356 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
357 dabei werden Koeffizienten ignoriert (2*3*a \<up> 2*4*b gilt wie a \<up> 2*b) *)
358 fun degree_ord (xs, ys) =
359 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
360 ((monom_degree xs, xs), (monom_degree ys, ys));
362 fun hd_str str = substring (str, 0, 1);
363 fun tl_str str = substring (str, 1, (size str) - 1);
365 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
366 fun get_koeff_of_mon [] = raise ERROR("get_koeff_of_mon: called with l = []")
367 | get_koeff_of_mon (x::_) = if is_nums x then SOME x else NONE;
369 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
370 fun koeff2ordStr (SOME x) = (case x of
372 if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
374 | _ => "aaa") (* "num.Ausdruck" --> gross *)
375 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
377 (* Order zum Vergleich von Koeffizienten (strings):
378 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
379 fun compare_koeff_ord (xs, ys) =
380 string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
381 (koeff2ordStr o get_koeff_of_mon) ys);
383 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
384 fun koeff_degree_ord (xs, ys) =
385 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
387 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
389 val sort_monList = sort koeff_degree_ord;
391 (* Alternativ zu degree_ord koennte auch die viel einfachere und
392 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
393 fuer unsere Zwecke geeignet!
395 fun simple_ord (al,bl: term list) = dict_ord string_ord
396 (map get_basStr al, map get_basStr bl);
398 val sort_monList = sort simple_ord; *)
400 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
401 (mit gewuenschtem Typen T) *)
402 fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
403 fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
404 fun binop op_ t1 t2 = op_ $ t1 $ t2;
405 fun create_prod T (a,b) = binop (mult T) a b;
406 fun create_sum T (a,b) = binop (plus T) a b;
408 (* löscht letztes Element einer Liste *)
409 fun drop_last l = take ((length l)-1,l);
411 (* Liste von Variablen --> Monom *)
412 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
414 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
415 gleiche Monome zusammengefasst werden können (collect_numerals)!
416 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
418 (* Liste von Monomen --> Polynom *)
419 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
421 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
422 bessere Darstellung, da keine Klammern sichtbar!
423 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
425 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
426 fun sort_variables t =
428 val ll = map monom2list (poly2list t);
429 val lls = map sort_varList ll;
431 val ls = map (create_monom T) lls;
432 in create_polynom T ls end;
434 (* sorts the monoms of an expanded and variable-sorted polynomial
438 val ll = map monom2list (poly2list t);
439 val lls = sort_monList ll;
441 val ls = map (create_monom T) lls;
442 in create_polynom T ls end;
445 subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>
447 local (*. for make_polynomial .*)
449 open Term; (* for type order = EQUAL | LESS | GREATER *)
451 fun pr_ord EQUAL = "EQUAL"
452 | pr_ord LESS = "LESS"
453 | pr_ord GREATER = "GREATER";
455 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
457 "Transcendental.powr" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
458 | _ => (((a, 0), T), 0))
459 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
460 | dest_hd' (Var v) = (v, 2)
461 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
462 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
463 | dest_hd' t = raise TERM ("dest_hd'", [t]);
465 fun size_of_term' (Const(str,_) $ t) =
466 if "Transcendental.powr"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
467 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
468 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
469 | size_of_term' _ = 1;
471 fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
472 (case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
473 | term_ord' pr thy (t, u) =
476 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
477 val _ = tracing ("t= f@ts= \"" ^ UnparseC.term_in_thy thy f ^ "\" @ \"[" ^
478 commas (map (UnparseC.term_in_thy thy) ts) ^ "]\"");
479 val _ = tracing("u= g@us= \"" ^ UnparseC.term_in_thy thy g ^ "\" @ \"[" ^
480 commas (map (UnparseC.term_in_thy thy) us) ^ "]\"");
481 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
482 string_of_int (size_of_term' u) ^ ")");
483 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
484 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
485 val _ = tracing ("-------");
488 case int_ord (size_of_term' t, size_of_term' u) of
490 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
491 (case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
495 and hd_ord (f, g) = (* ~ term.ML *)
496 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
497 and terms_ord _ pr (ts, us) =
498 list_ord (term_ord' pr (ThyC.get_theory "Isac_Knowledge"))(ts, us);
502 fun ord_make_polynomial (pr:bool) thy (_: subst) tu =
503 (term_ord' pr thy(***) tu = LESS );
507 Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
508 [("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
511 subsection \<open>predicates\<close>
512 subsubsection \<open>in specifications\<close>
514 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
515 fun is_polyrat_in t v =
517 fun finddivide (_ $ _ $ _ $ _) _ = raise ERROR("is_polyrat_in:")
518 (* at the moment there is no term like this, but ....*)
519 | finddivide (Const ("Rings.divide_class.divide",_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)
520 | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
521 | finddivide (_ $ t1) v = finddivide t1 v
522 | finddivide _ _ = false;
523 in finddivide t v end;
525 fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;
526 fun is_poly_in t v = case poly_deg_in t v of SOME _ => true | NONE => false;
527 fun has_degree_in t v = case expand_deg_in t v of SOME d => d | NONE => ~1;
529 (*.the expression contains + - * ^ only ?
530 this is weaker than 'is_polynomial' !.*)
531 fun is_polyexp (Free _) = true
532 | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)
533 | is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
534 | is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
535 | is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
536 | is_polyexp (Const ("Transcendental.powr",_) $ Free _ $ Free _) = true
537 | is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
538 ((is_polyexp t1) andalso (is_polyexp t2))
539 | is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
540 ((is_polyexp t1) andalso (is_polyexp t2))
541 | is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
542 ((is_polyexp t1) andalso (is_polyexp t2))
543 | is_polyexp (Const ("Transcendental.powr",_) $ t1 $ t2) =
544 ((is_polyexp t1) andalso (is_polyexp t2))
545 | is_polyexp num = TermC.is_num num;
548 subsubsection \<open>for hard-coded AC rewriting\<close>
550 (* auch Klammerung muss übereinstimmen;
551 sort_variables klammert Produkte rechtslastig*)
552 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
554 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
557 subsection \<open>evaluations functions\<close>
558 subsubsection \<open>for predicates\<close>
560 fun eval_is_polyrat_in _ _(p as (Const ("Poly.is_polyrat_in",_) $ t $ v)) _ =
562 then SOME ((UnparseC.term p) ^ " = True",
563 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
564 else SOME ((UnparseC.term p) ^ " = True",
565 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
566 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
568 (*("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in ""))*)
569 fun eval_is_expanded_in _ _
570 (p as (Const ("Poly.is_expanded_in",_) $ t $ v)) _ =
571 if is_expanded_in t v
572 then SOME ((UnparseC.term p) ^ " = True",
573 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
574 else SOME ((UnparseC.term p) ^ " = True",
575 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
576 | eval_is_expanded_in _ _ _ _ = NONE;
578 (*("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in ""))*)
579 fun eval_is_poly_in _ _
580 (p as (Const ("Poly.is_poly_in",_) $ t $ v)) _ =
582 then SOME ((UnparseC.term p) ^ " = True",
583 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
584 else SOME ((UnparseC.term p) ^ " = True",
585 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
586 | eval_is_poly_in _ _ _ _ = NONE;
588 (*("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in ""))*)
589 fun eval_has_degree_in _ _
590 (p as (Const ("Poly.has_degree_in",_) $ t $ v)) _ =
591 let val d = has_degree_in t v
592 val d' = TermC.term_of_num HOLogic.realT d
593 in SOME ((UnparseC.term p) ^ " = " ^ (string_of_int d),
594 HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
596 | eval_has_degree_in _ _ _ _ = NONE;
598 (*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)
599 fun eval_is_polyexp (thmid:string) _
600 (t as (Const("Poly.is_polyexp", _) $ arg)) thy =
602 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
603 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
604 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
605 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
606 | eval_is_polyexp _ _ _ _ = NONE;
609 subsubsection \<open>for hard-coded AC rewriting\<close>
612 (*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)
613 fun eval_is_addUnordered (thmid:string) _
614 (t as (Const("Poly.is_addUnordered", _) $ arg)) thy =
615 if is_addUnordered arg
616 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
617 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
618 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
619 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
620 | eval_is_addUnordered _ _ _ _ = NONE;
622 fun eval_is_multUnordered (thmid:string) _
623 (t as (Const("Poly.is_multUnordered", _) $ arg)) thy =
624 if is_multUnordered arg
625 then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
626 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
627 else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
628 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
629 | eval_is_multUnordered _ _ _ _ = NONE;
631 setup \<open>KEStore_Elems.add_calcs
632 [("is_polyrat_in", ("Poly.is_polyrat_in",
633 eval_is_polyrat_in "#eval_is_polyrat_in")),
634 ("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in "")),
635 ("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in "")),
636 ("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in "")),
637 ("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp "")),
638 ("is_multUnordered", ("Poly.is_multUnordered", eval_is_multUnordered"")),
639 ("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))]\<close>
641 subsection \<open>rule-sets\<close>
642 subsubsection \<open>without specific order\<close>
644 (* used only for merge *)
645 val calculate_Poly = Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty [];
647 (*.for evaluation of conditions in rewrite rules.*)
648 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls
649 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
650 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
651 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
652 Rule.Eval ("Groups.minus_class.minus", eval_binop "#sub_"),
653 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
654 Rule.Eval ("Transcendental.powr", eval_binop "#power_")];
656 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls
657 [Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
658 Rule.Thm ("real_unari_minus", ThmC.numerals_to_Free @{thm real_unari_minus}),
659 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
660 Rule.Eval ("Groups.minus_class.minus", eval_binop "#sub_"),
661 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
662 Rule.Eval ("Transcendental.powr" , eval_binop "#power_")];
666 Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
667 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
668 rules = [Rule.Thm ("distrib_right" , ThmC.numerals_to_Free @{thm distrib_right}),
669 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
670 Rule.Thm ("distrib_left", ThmC.numerals_to_Free @{thm distrib_left})
671 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
672 ], scr = Rule.Empty_Prog};
675 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
676 erls = Rule_Set.empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
678 [Rule.Thm ("real_diff_minus", ThmC.numerals_to_Free @{thm real_diff_minus}),
679 (*"a - b = a + -1 * b"*)
680 Rule.Thm ("sym_real_mult_minus1", ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
681 (*- ?z = "-1 * ?z"*)],
682 scr = Rule.Empty_Prog};
685 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
686 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
687 erls = Rule_Set.empty,srls = Rule_Set.Empty,
688 calc = [], errpatts = [],
690 [Rule.Thm ("real_plus_binom_pow4", ThmC.numerals_to_Free @{thm real_plus_binom_pow4}),
691 (*"(a + b) \<up> 4 = ... "*)
692 Rule.Thm ("real_plus_binom_pow5",ThmC.numerals_to_Free @{thm real_plus_binom_pow5}),
693 (*"(a + b) \<up> 5 = ... "*)
694 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
695 (*"(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
696 (*WN071229 changed/removed for Schaerding -----vvv*)
697 (*Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),*)
698 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
699 Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
700 (*"(a + b) \<up> 2 = (a + b) * (a + b)"*)
701 (*Rule.Thm ("real_plus_minus_binom1_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),*)
702 (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
703 (*Rule.Thm ("real_plus_minus_binom2_p_p", ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),*)
704 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
705 (*WN071229 changed/removed for Schaerding -----\<up>*)
707 Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
708 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
709 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
710 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
712 Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
713 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
714 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
715 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
716 ], scr = Rule.Empty_Prog};
718 val expand_poly_rat_ =
719 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
720 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
721 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
722 [Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")
724 srls = Rule_Set.Empty,
725 calc = [], errpatts = [],
727 [Rule.Thm ("real_plus_binom_pow4_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow4_poly}),
728 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 4 = ... "*)
729 Rule.Thm ("real_plus_binom_pow5_poly", ThmC.numerals_to_Free @{thm real_plus_binom_pow5_poly}),
730 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 5 = ... "*)
731 Rule.Thm ("real_plus_binom_pow2_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow2_poly}),
732 (*"[| a is_polyexp; b is_polyexp |] ==>
733 (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
734 Rule.Thm ("real_plus_binom_pow3_poly",ThmC.numerals_to_Free @{thm real_plus_binom_pow3_poly}),
735 (*"[| a is_polyexp; b is_polyexp |] ==>
736 (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
737 Rule.Thm ("real_plus_minus_binom1_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p_p}),
738 (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
739 Rule.Thm ("real_plus_minus_binom2_p_p",ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p_p}),
740 (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
742 Rule.Thm ("real_add_mult_distrib_poly",
743 ThmC.numerals_to_Free @{thm real_add_mult_distrib_poly}),
744 (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
745 Rule.Thm("real_add_mult_distrib2_poly",
746 ThmC.numerals_to_Free @{thm real_add_mult_distrib2_poly}),
747 (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
749 Rule.Thm ("realpow_multI_poly", ThmC.numerals_to_Free @{thm realpow_multI_poly}),
750 (*"[| r is_polyexp; s is_polyexp |] ==>
751 (r * s) \<up> n = r \<up> n * s \<up> n"*)
752 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
753 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
754 ], scr = Rule.Empty_Prog};
756 val simplify_power_ =
757 Rule_Def.Repeat{id = "simplify_power_", preconds = [],
758 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
759 erls = Rule_Set.empty, srls = Rule_Set.Empty,
760 calc = [], errpatts = [],
761 rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
762 a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *)
763 Rule.Thm ("sym_realpow_twoI",
764 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
765 (*"r * r = r \<up> 2"*)
766 Rule.Thm ("realpow_twoI_assoc_l",ThmC.numerals_to_Free @{thm realpow_twoI_assoc_l}),
767 (*"r * (r * s) = r \<up> 2 * s"*)
769 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
770 (*"r * r \<up> n = r \<up> (n + 1)"*)
771 Rule.Thm ("realpow_plus_1_assoc_l",
772 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l}),
773 (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)
774 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)
775 Rule.Thm ("realpow_plus_1_assoc_l2",
776 ThmC.numerals_to_Free @{thm realpow_plus_1_assoc_l2}),
777 (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
779 Rule.Thm ("sym_realpow_addI",
780 ThmC.numerals_to_Free (@{thm realpow_addI} RS @{thm sym})),
781 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
782 Rule.Thm ("realpow_addI_assoc_l",ThmC.numerals_to_Free @{thm realpow_addI_assoc_l}),
783 (*"r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s"*)
785 (* ist in expand_poly - wird hier aber auch gebraucht, wegen:
786 "r * r = r \<up> 2" wenn r=a \<up> b*)
787 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow})
788 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
789 ], scr = Rule.Empty_Prog};
791 val calc_add_mult_pow_ =
792 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
793 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
794 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
795 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
796 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
797 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
800 rules = [Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
801 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
802 Rule.Eval ("Transcendental.powr", eval_binop "#power_")
803 ], scr = Rule.Empty_Prog};
805 val reduce_012_mult_ =
806 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
807 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
808 erls = Rule_Set.empty,srls = Rule_Set.Empty,
809 calc = [], errpatts = [],
810 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
811 Rule.Thm ("mult_1_right",ThmC.numerals_to_Free @{thm mult_1_right}),
812 (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*)
813 Rule.Thm ("realpow_zeroI",ThmC.numerals_to_Free @{thm realpow_zeroI}),
814 (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*)
815 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
817 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
819 ], scr = Rule.Empty_Prog};
821 val collect_numerals_ =
822 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
823 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
824 erls = Atools_erls, srls = Rule_Set.Empty,
825 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
828 [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
829 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
830 Rule.Thm ("real_num_collect_assoc_r",ThmC.numerals_to_Free @{thm real_num_collect_assoc_r}),
831 (*"[| l is_const; m is_const |] ==> \
832 \(k + m * n) + l * n = k + (l + m)*n"*)
833 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
834 (*"m is_const ==> n + m * n = (1 + m) * n"*)
835 Rule.Thm ("real_one_collect_assoc_r",ThmC.numerals_to_Free @{thm real_one_collect_assoc_r}),
836 (*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
838 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
840 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
841 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
842 Rule.Thm ("real_mult_2_assoc_r",ThmC.numerals_to_Free @{thm real_mult_2_assoc_r}),
843 (*"(k + z1) + z1 = k + 2 * z1"*)
844 Rule.Thm ("sym_real_mult_2",ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym}))
845 (*"z1 + z1 = 2 * z1"*)
846 ], scr = Rule.Empty_Prog};
849 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
850 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
851 erls = Rule_Set.empty,srls = Rule_Set.Empty, calc = [], errpatts = [],
852 rules = [Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
854 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
856 Rule.Thm ("mult_zero_right",ThmC.numerals_to_Free @{thm mult_zero_right}),
858 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
860 Rule.Thm ("add_0_right",ThmC.numerals_to_Free @{thm add_0_right}),
861 (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
863 (*Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI})*)
864 (*"?r \<up> 1 = ?r"*)
865 Rule.Thm ("division_ring_divide_zero",ThmC.numerals_to_Free @{thm division_ring_divide_zero})
867 ], scr = Rule.Empty_Prog};
869 val discard_parentheses1 =
870 Rule_Set.append_rules "discard_parentheses1" Rule_Set.empty
871 [Rule.Thm ("sym_mult.assoc",
872 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym}))
873 (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
874 (*Rule.Thm ("sym_add.assoc",
875 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))*)
876 (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
880 Rule_Def.Repeat{id = "expand_poly", preconds = [],
881 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
882 erls = Rule_Set.empty,srls = Rule_Set.Empty,
883 calc = [], errpatts = [],
885 rules = [Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
886 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
887 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
888 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
889 (*Rule.Thm ("distrib_right1",ThmC.numerals_to_Free @{thm distrib_right}1),
890 ....... 18.3.03 undefined???*)
892 Rule.Thm ("real_plus_binom_pow2",ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
893 (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
894 Rule.Thm ("real_minus_binom_pow2_p",ThmC.numerals_to_Free @{thm real_minus_binom_pow2_p}),
895 (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
896 Rule.Thm ("real_plus_minus_binom1_p",
897 ThmC.numerals_to_Free @{thm real_plus_minus_binom1_p}),
898 (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
899 Rule.Thm ("real_plus_minus_binom2_p",
900 ThmC.numerals_to_Free @{thm real_plus_minus_binom2_p}),
901 (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
903 Rule.Thm ("minus_minus",ThmC.numerals_to_Free @{thm minus_minus}),
905 Rule.Thm ("real_diff_minus",ThmC.numerals_to_Free @{thm real_diff_minus}),
906 (*"a - b = a + -1 * b"*)
907 Rule.Thm ("sym_real_mult_minus1",
908 ThmC.numerals_to_Free (@{thm real_mult_minus1} RS @{thm sym}))
911 (*Rule.Thm ("real_minus_add_distrib",
912 ThmC.numerals_to_Free @{thm real_minus_add_distrib}),*)
913 (*"- (?x + ?y) = - ?x + - ?y"*)
914 (*Rule.Thm ("real_diff_plus",ThmC.numerals_to_Free @{thm real_diff_plus})*)
916 ], scr = Rule.Empty_Prog};
919 Rule_Def.Repeat{id = "simplify_power", preconds = [],
920 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
921 erls = Rule_Set.empty, srls = Rule_Set.Empty,
922 calc = [], errpatts = [],
923 rules = [Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
924 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
926 Rule.Thm ("sym_realpow_twoI",
927 ThmC.numerals_to_Free( @{thm realpow_twoI} RS @{thm sym})),
928 (*"r1 * r1 = r1 \<up> 2"*)
929 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
930 (*"r * r \<up> n = r \<up> (n + 1)"*)
931 Rule.Thm ("realpow_pow",ThmC.numerals_to_Free @{thm realpow_pow}),
932 (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
933 Rule.Thm ("sym_realpow_addI",
934 ThmC.numerals_to_Free (@{thm realpow_addI} RS @{thm sym})),
935 (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
936 Rule.Thm ("realpow_oneI",ThmC.numerals_to_Free @{thm realpow_oneI}),
938 Rule.Thm ("realpow_eq_oneI",ThmC.numerals_to_Free @{thm realpow_eq_oneI})
940 ], scr = Rule.Empty_Prog};
942 val collect_numerals =
943 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
944 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
945 erls = Atools_erls(*erls3.4.03*),srls = Rule_Set.Empty,
946 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
947 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
948 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
950 rules = [Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
951 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
952 Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
953 (*"[| l is_const; m is_const |] ==>
954 l * n + (m * n + k) = (l + m) * n + k"*)
955 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
956 (*"m is_const ==> n + m * n = (1 + m) * n"*)
957 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
958 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
959 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
960 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
961 Rule.Eval ("Transcendental.powr", eval_binop "#power_")
962 ], scr = Rule.Empty_Prog};
964 Rule_Def.Repeat{id = "reduce_012", preconds = [],
965 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
966 erls = Rule_Set.empty,srls = Rule_Set.Empty,
967 calc = [], errpatts = [],
968 rules = [Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
970 (*Rule.Thm ("real_mult_minus1",ThmC.numerals_to_Free @{thm real_mult_minus1}),14.3.03*)
972 Rule.Thm ("minus_mult_left",
973 ThmC.numerals_to_Free (@{thm minus_mult_left} RS @{thm sym})),
974 (*- (?x * ?y) = "- ?x * ?y"*)
975 (*Rule.Thm ("real_minus_mult_cancel",
976 ThmC.numerals_to_Free @{thm real_minus_mult_cancel}),
977 (*"- ?x * - ?y = ?x * ?y"*)---*)
978 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
980 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),
982 Rule.Thm ("right_minus",ThmC.numerals_to_Free @{thm right_minus}),
984 Rule.Thm ("sym_real_mult_2",
985 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
986 (*"z1 + z1 = 2 * z1"*)
987 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc})
988 (*"z1 + (z1 + k) = 2 * z1 + k"*)
989 ], scr = Rule.Empty_Prog};
991 val discard_parentheses =
992 Rule_Set.append_rules "discard_parentheses" Rule_Set.empty
993 [Rule.Thm ("sym_mult.assoc",
994 ThmC.numerals_to_Free (@{thm mult.assoc} RS @{thm sym})),
995 Rule.Thm ("sym_add.assoc",
996 ThmC.numerals_to_Free (@{thm add.assoc} RS @{thm sym}))];
999 subsubsection \<open>hard-coded AC rewriting\<close>
1001 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1002 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1003 val order_add_mult =
1004 Rule_Def.Repeat{id = "order_add_mult", preconds = [],
1005 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
1006 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1007 calc = [], errpatts = [],
1008 rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1010 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1011 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1012 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1013 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1014 Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
1016 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1017 (*x + (y + z) = y + (x + z)*)
1018 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc})
1019 (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
1020 ], scr = Rule.Empty_Prog};
1021 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1022 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1024 Rule_Def.Repeat{id = "order_mult", preconds = [],
1025 rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
1026 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1027 calc = [], errpatts = [],
1028 rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1030 Rule.Thm ("real_mult_left_commute",ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1031 (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1032 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc})
1033 (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1034 ], scr = Rule.Empty_Prog};
1037 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1038 []:(Rule.rule * (term * term list)) list;
1039 fun init_state (_: term) = Rule_Set.e_rrlsstate;
1040 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1041 ([]:(Rule.rule * (term * term list)) list);
1042 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1043 fun normal_form t = SOME (sort_variables t, []: term list);
1046 Rule_Set.Rrls {id = "order_mult_",
1048 (* ?p matched with the current term gives an environment,
1049 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1050 [([TermC.parse_patt thy "?p is_multUnordered"],
1051 TermC.parse_patt thy "?p :: real")],
1052 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1053 erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1054 [Rule.Eval ("Poly.is_multUnordered",
1055 eval_is_multUnordered "")],
1056 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1057 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1058 ("DIVIDE", ("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1059 ("POWER" , ("Transcendental.powr", eval_binop "#power_"))],
1061 scr = Rule.Rfuns {init_state = init_state,
1062 normal_form = normal_form,
1063 locate_rule = locate_rule,
1064 next_rule = next_rule,
1065 attach_form = attach_form}};
1066 val order_mult_rls_ =
1067 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
1068 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1069 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1070 calc = [], errpatts = [],
1071 rules = [Rule.Rls_ order_mult_
1072 ], scr = Rule.Empty_Prog};
1076 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1077 []: (Rule.rule * (term * term list)) list;
1078 fun init_state (_: term) = Rule_Set.e_rrlsstate;
1079 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1080 ([]: (Rule.rule * (term * term list)) list);
1081 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1082 fun normal_form t = SOME (sort_monoms t,[]: term list);
1085 Rule_Set.Rrls {id = "order_add_",
1086 prepat = (*WN.18.6.03 Preconditions und Pattern,
1087 die beide passen muessen, damit das Rule_Set.Rrls angewandt wird*)
1088 [([TermC.parse_patt @{theory} "?p is_addUnordered"],
1089 TermC.parse_patt @{theory} "?p :: real"
1090 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1091 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1092 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1093 erls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
1094 [Rule.Eval ("Poly.is_addUnordered", eval_is_addUnordered "")],
1095 calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
1096 ("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
1097 ("DIVIDE",("Rings.divide_class.divide", Prog_Expr.eval_cancel "#divide_e")),
1098 ("POWER" ,("Transcendental.powr" , eval_binop "#power_"))],
1100 scr = Rule.Rfuns {init_state = init_state,
1101 normal_form = normal_form,
1102 locate_rule = locate_rule,
1103 next_rule = next_rule,
1104 attach_form = attach_form}};
1106 val order_add_rls_ =
1107 Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
1108 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1109 erls = Rule_Set.empty,srls = Rule_Set.Empty,
1110 calc = [], errpatts = [],
1111 rules = [Rule.Rls_ order_add_
1112 ], scr = Rule.Empty_Prog};
1115 text \<open>rule-set make_polynomial also named norm_Poly:
1116 Rewrite order has not been implemented properly; the order is better in
1117 make_polynomial_in (coded in SML).
1118 Notes on state of development:
1119 \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
1120 \# migration Isabelle2002 --> 2011 weakened the rule set, see test
1121 --- Matthias Goldgruber 2003 rewrite orders ---, raise ERROR "ord_make_polynomial_in #16b"
1124 (*. see MG-DA.p.52ff .*)
1125 val make_polynomial(*MG.03, overwrites version from above,
1126 previously 'make_polynomial_'*) =
1127 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list,
1128 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1129 erls = Atools_erls, srls = Rule_Set.Empty,calc = [], errpatts = [],
1130 rules = [Rule.Rls_ discard_minus,
1131 Rule.Rls_ expand_poly_,
1132 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1133 Rule.Rls_ order_mult_rls_,
1134 Rule.Rls_ simplify_power_,
1135 Rule.Rls_ calc_add_mult_pow_,
1136 Rule.Rls_ reduce_012_mult_,
1137 Rule.Rls_ order_add_rls_,
1138 Rule.Rls_ collect_numerals_,
1139 Rule.Rls_ reduce_012_,
1140 Rule.Rls_ discard_parentheses1
1142 scr = Rule.Empty_Prog
1146 val norm_Poly(*=make_polynomial*) =
1147 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list,
1148 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1149 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1150 rules = [Rule.Rls_ discard_minus,
1151 Rule.Rls_ expand_poly_,
1152 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1153 Rule.Rls_ order_mult_rls_,
1154 Rule.Rls_ simplify_power_,
1155 Rule.Rls_ calc_add_mult_pow_,
1156 Rule.Rls_ reduce_012_mult_,
1157 Rule.Rls_ order_add_rls_,
1158 Rule.Rls_ collect_numerals_,
1159 Rule.Rls_ reduce_012_,
1160 Rule.Rls_ discard_parentheses1
1162 scr = Rule.Empty_Prog
1166 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1
1167 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1168 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1169 val make_rat_poly_with_parentheses =
1170 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1171 rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1172 erls = Atools_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1173 rules = [Rule.Rls_ discard_minus,
1174 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1175 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1176 Rule.Rls_ order_mult_rls_,
1177 Rule.Rls_ simplify_power_,
1178 Rule.Rls_ calc_add_mult_pow_,
1179 Rule.Rls_ reduce_012_mult_,
1180 Rule.Rls_ order_add_rls_,
1181 Rule.Rls_ collect_numerals_,
1182 Rule.Rls_ reduce_012_
1183 (*Rule.Rls_ discard_parentheses1 *)
1185 scr = Rule.Empty_Prog
1189 (*.a minimal ruleset for reverse rewriting of factions [2];
1190 compare expand_binoms.*)
1192 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1193 erls = Atools_erls, srls = Rule_Set.Empty,
1194 calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1195 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1196 ("POWER", ("Transcendental.powr", eval_binop "#power_"))*)
1198 rules = [Rule.Thm ("real_plus_binom_times" ,ThmC.numerals_to_Free @{thm real_plus_binom_times}),
1199 (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1200 Rule.Thm ("real_plus_binom_times1" ,ThmC.numerals_to_Free @{thm real_plus_binom_times1}),
1201 (*"(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2"*)
1202 Rule.Thm ("real_plus_binom_times2" ,ThmC.numerals_to_Free @{thm real_plus_binom_times2}),
1203 (*"(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 2"*)
1205 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
1207 Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
1208 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1209 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
1210 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1212 Rule.Thm ("mult.assoc", ThmC.numerals_to_Free @{thm mult.assoc}),
1213 (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1214 Rule.Rls_ order_mult_rls_,
1215 (*Rule.Rls_ order_add_rls_,*)
1217 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
1218 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1219 Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
1221 Rule.Thm ("sym_realpow_twoI",
1222 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
1223 (*"r1 * r1 = r1 \<up> 2"*)
1224 Rule.Thm ("sym_real_mult_2",
1225 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
1226 (*"z1 + z1 = 2 * z1"*)
1227 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
1228 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1230 Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
1231 (*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
1232 Rule.Thm ("real_num_collect_assoc",ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
1233 (*"[| l is_const; m is_const |] ==>
1234 l * n + (m * n + k) = (l + m) * n + k"*)
1235 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
1236 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1237 Rule.Thm ("real_one_collect_assoc",ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
1238 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1240 Rule.Thm ("realpow_multI", ThmC.numerals_to_Free @{thm realpow_multI}),
1241 (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
1243 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
1244 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1245 Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
1247 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),(*"1 * z = z"*)
1248 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),(*"0 * z = 0"*)
1249 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left})(*0 + z = z*)
1251 (*Rule.Rls_ order_add_rls_*)
1254 scr = Rule.Empty_Prog};
1257 subsection \<open>rule-sets with explicit program for intermediate steps\<close>
1258 partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
1260 "expand_binoms_2 term = (
1262 (Try (Repeat (Rewrite ''real_plus_binom_pow2''))) #>
1263 (Try (Repeat (Rewrite ''real_plus_binom_times''))) #>
1264 (Try (Repeat (Rewrite ''real_minus_binom_pow2''))) #>
1265 (Try (Repeat (Rewrite ''real_minus_binom_times''))) #>
1266 (Try (Repeat (Rewrite ''real_plus_minus_binom1''))) #>
1267 (Try (Repeat (Rewrite ''real_plus_minus_binom2''))) #>
1269 (Try (Repeat (Rewrite ''mult_1_left''))) #>
1270 (Try (Repeat (Rewrite ''mult_zero_left''))) #>
1271 (Try (Repeat (Rewrite ''add_0_left''))) #>
1273 (Try (Repeat (Calculate ''PLUS''))) #>
1274 (Try (Repeat (Calculate ''TIMES''))) #>
1275 (Try (Repeat (Calculate ''POWER''))) #>
1277 (Try (Repeat (Rewrite ''sym_realpow_twoI''))) #>
1278 (Try (Repeat (Rewrite ''realpow_plus_1''))) #>
1279 (Try (Repeat (Rewrite ''sym_real_mult_2''))) #>
1280 (Try (Repeat (Rewrite ''real_mult_2_assoc''))) #>
1282 (Try (Repeat (Rewrite ''real_num_collect''))) #>
1283 (Try (Repeat (Rewrite ''real_num_collect_assoc''))) #>
1285 (Try (Repeat (Rewrite ''real_one_collect''))) #>
1286 (Try (Repeat (Rewrite ''real_one_collect_assoc''))) #>
1288 (Try (Repeat (Calculate ''PLUS''))) #>
1289 (Try (Repeat (Calculate ''TIMES''))) #>
1290 (Try (Repeat (Calculate ''POWER''))))
1294 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1295 erls = Atools_erls, srls = Rule_Set.Empty,
1296 calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
1297 ("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
1298 ("POWER", ("Transcendental.powr", eval_binop "#power_"))
1300 rules = [Rule.Thm ("real_plus_binom_pow2",
1301 ThmC.numerals_to_Free @{thm real_plus_binom_pow2}),
1302 (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
1303 Rule.Thm ("real_plus_binom_times",
1304 ThmC.numerals_to_Free @{thm real_plus_binom_times}),
1305 (*"(a + b)*(a + b) = ...*)
1306 Rule.Thm ("real_minus_binom_pow2",
1307 ThmC.numerals_to_Free @{thm real_minus_binom_pow2}),
1308 (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
1309 Rule.Thm ("real_minus_binom_times",
1310 ThmC.numerals_to_Free @{thm real_minus_binom_times}),
1311 (*"(a - b)*(a - b) = ...*)
1312 Rule.Thm ("real_plus_minus_binom1",
1313 ThmC.numerals_to_Free @{thm real_plus_minus_binom1}),
1314 (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
1315 Rule.Thm ("real_plus_minus_binom2",
1316 ThmC.numerals_to_Free @{thm real_plus_minus_binom2}),
1317 (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
1319 Rule.Thm ("real_pp_binom_times",ThmC.numerals_to_Free @{thm real_pp_binom_times}),
1320 (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1321 Rule.Thm ("real_pm_binom_times",ThmC.numerals_to_Free @{thm real_pm_binom_times}),
1322 (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1323 Rule.Thm ("real_mp_binom_times",ThmC.numerals_to_Free @{thm real_mp_binom_times}),
1324 (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1325 Rule.Thm ("real_mm_binom_times",ThmC.numerals_to_Free @{thm real_mm_binom_times}),
1326 (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1327 Rule.Thm ("realpow_multI",ThmC.numerals_to_Free @{thm realpow_multI}),
1328 (*(a*b) \<up> n = a \<up> n * b \<up> n*)
1329 Rule.Thm ("real_plus_binom_pow3",ThmC.numerals_to_Free @{thm real_plus_binom_pow3}),
1330 (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
1331 Rule.Thm ("real_minus_binom_pow3",
1332 ThmC.numerals_to_Free @{thm real_minus_binom_pow3}),
1333 (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
1336 (*Rule.Thm ("distrib_right" ,ThmC.numerals_to_Free @{thm distrib_right}),
1337 (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1338 Rule.Thm ("distrib_left",ThmC.numerals_to_Free @{thm distrib_left}),
1339 (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1340 Rule.Thm ("left_diff_distrib" ,ThmC.numerals_to_Free @{thm left_diff_distrib}),
1341 (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1342 Rule.Thm ("right_diff_distrib",ThmC.numerals_to_Free @{thm right_diff_distrib}),
1343 (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1345 Rule.Thm ("mult_1_left",ThmC.numerals_to_Free @{thm mult_1_left}),
1347 Rule.Thm ("mult_zero_left",ThmC.numerals_to_Free @{thm mult_zero_left}),
1349 Rule.Thm ("add_0_left",ThmC.numerals_to_Free @{thm add_0_left}),(*"0 + z = z"*)
1351 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
1352 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1353 Rule.Eval ("Transcendental.powr", eval_binop "#power_"),
1354 (*Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
1356 Rule.Thm ("real_mult_left_commute",
1357 ThmC.numerals_to_Free @{thm real_mult_left_commute}),
1358 Rule.Thm ("mult.assoc",ThmC.numerals_to_Free @{thm mult.assoc}),
1359 Rule.Thm ("add.commute",ThmC.numerals_to_Free @{thm add.commute}),
1360 Rule.Thm ("add.left_commute",ThmC.numerals_to_Free @{thm add.left_commute}),
1361 Rule.Thm ("add.assoc",ThmC.numerals_to_Free @{thm add.assoc}),
1363 Rule.Thm ("sym_realpow_twoI",
1364 ThmC.numerals_to_Free (@{thm realpow_twoI} RS @{thm sym})),
1365 (*"r1 * r1 = r1 \<up> 2"*)
1366 Rule.Thm ("realpow_plus_1",ThmC.numerals_to_Free @{thm realpow_plus_1}),
1367 (*"r * r \<up> n = r \<up> (n + 1)"*)
1368 (*Rule.Thm ("sym_real_mult_2",
1369 ThmC.numerals_to_Free (@{thm real_mult_2} RS @{thm sym})),
1370 (*"z1 + z1 = 2 * z1"*)*)
1371 Rule.Thm ("real_mult_2_assoc",ThmC.numerals_to_Free @{thm real_mult_2_assoc}),
1372 (*"z1 + (z1 + k) = 2 * z1 + k"*)
1374 Rule.Thm ("real_num_collect",ThmC.numerals_to_Free @{thm real_num_collect}),
1375 (*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
1376 Rule.Thm ("real_num_collect_assoc",
1377 ThmC.numerals_to_Free @{thm real_num_collect_assoc}),
1378 (*"[| l is_const; m is_const |] ==>
1379 l * n + (m * n + k) = (l + m) * n + k"*)
1380 Rule.Thm ("real_one_collect",ThmC.numerals_to_Free @{thm real_one_collect}),
1381 (*"m is_const ==> n + m * n = (1 + m) * n"*)
1382 Rule.Thm ("real_one_collect_assoc",
1383 ThmC.numerals_to_Free @{thm real_one_collect_assoc}),
1384 (*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
1386 Rule.Eval ("Groups.plus_class.plus", eval_binop "#add_"),
1387 Rule.Eval ("Groups.times_class.times", eval_binop "#mult_"),
1388 Rule.Eval ("Transcendental.powr", eval_binop "#power_")
1390 scr = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})
1394 subsection \<open>add to Know_Store\<close>
1395 subsubsection \<open>rule-sets\<close>
1396 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
1398 setup \<open>KEStore_Elems.add_rlss
1399 [("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
1400 ("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*)
1401 ("expand", (Context.theory_name @{theory}, prep_rls' expand)),
1402 ("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)),
1403 ("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
1405 ("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)),
1406 ("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)),
1407 ("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)),
1408 ("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)),
1409 ("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
1411 ("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)),
1412 ("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)),
1413 ("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)),
1414 ("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)),
1415 ("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
1417 ("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)),
1418 ("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)),
1419 ("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)),
1420 ("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)),
1421 ("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
1423 ("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)),
1424 ("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)),
1425 ("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)),
1426 ("make_rat_poly_with_parentheses",
1427 (Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))]\<close>
1429 subsection \<open>problems\<close>
1430 setup \<open>KEStore_Elems.add_pbts
1431 [(Problem.prep_input thy "pbl_simp_poly" [] Problem.id_empty
1432 (["polynomial", "simplification"],
1433 [("#Given" ,["Term t_t"]),
1434 ("#Where" ,["t_t is_polyexp"]),
1435 ("#Find" ,["normalform n_n"])],
1436 Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
1437 Rule.Eval ("Poly.is_polyexp", eval_is_polyexp "")],
1438 SOME "Simplify t_t",
1439 [["simplification", "for_polynomials"]]))]\<close>
1441 subsection \<open>methods\<close>
1443 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
1445 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
1446 setup \<open>KEStore_Elems.add_mets
1447 [MethodC.prep_input thy "met_simp_poly" [] MethodC.id_empty
1448 (["simplification", "for_polynomials"],
1449 [("#Given" ,["Term t_t"]),
1450 ("#Where" ,["t_t is_polyexp"]),
1451 ("#Find" ,["normalform n_n"])],
1452 {rew_ord'="tless_true", rls' = Rule_Set.empty, calc = [], srls = Rule_Set.empty,
1453 prls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1454 [(*for preds in where_*)
1455 Rule.Eval ("Poly.is_polyexp", eval_is_polyexp"")],
1456 crls = Rule_Set.empty, errpats = [], nrls = norm_Poly},
1457 @{thm simplify.simps})]