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_num; 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_num; m is_num |] ==>
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_num; m is_num |] ==>
150 l * n + (m * n + k) = (l + m) * n + k" and
151 real_num_collect_assoc_l: "[| l is_num; m is_num |] ==>
152 l * n + (m * n + k) = (l + m)
154 real_num_collect_assoc_r: "[| l is_num; m is_num |] ==>
155 (k + m * n) + l * n = k + (l + m) * n" and
156 real_one_collect: "m is_num ==> 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_num ==> n + (m * n + k) = (1 + m)* n + k" and
161 real_one_collect_assoc_l: "m is_num ==> n + (m * n + k) = (1 + m) * n + k" and
162 real_one_collect_assoc_r: "m is_num ==> (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 (*sym_real_mult_minus1 expands indefinitely without assumptions ...*)
173 real_mult_minus1_sym: "[| \<not>(matches (- 1 * x) z); \<not>(z is_num) |] ==> - (z::real) = -1 * z" and
174 real_minus_mult_left: "\<not> ((a::real) is_num) ==> (- a) * b = - (a * b)" and
175 real_mult_2: "2 * z = z + (z::real)" and
177 real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
178 real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
181 subsection \<open>auxiliary functions\<close>
184 [\<^const_name>\<open>plus\<close>, \<^const_name>\<open>minus\<close>,
185 \<^const_name>\<open>divide\<close>, \<^const_name>\<open>times\<close>,
186 \<^const_name>\<open>realpow\<close>];
188 val int_ord_SAVE = int_ord;
189 (*for tests on rewrite orders*)
190 fun int_ord (i1, i2) =
191 (@{print} {a = "int_ord (" ^ string_of_int i1 ^ ", " ^ string_of_int i2 ^ ") = ", z = Int.compare (i1, i2)};
192 Int.compare (i1, i2));
193 (**)val int_ord = int_ord_SAVE; (*..outcomment for tests*)
195 subsubsection \<open>for predicates in specifications (ML)\<close>
197 (*--- auxiliary for is_expanded_in, is_poly_in, has_degree_in ---*)
198 (*. a "monomial t in variable v" is a term t with
199 either (1) v NOT existent in t, or (2) v contained in t,
201 if (2) then v is a factor on the very right, casually with exponent.*)
202 fun factor_right_deg (*case 2*)
203 (Const (\<^const_name>\<open>Groups.times_class.times\<close>, _) $
204 t1 $ (Const (\<^const_name>\<open>realpow\<close>,_) $ vv $ num)) v =
205 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME (snd (HOLogic.dest_number num))
207 | factor_right_deg (Const (\<^const_name>\<open>realpow\<close>,_) $ vv $ num) v =
208 if (vv = v) then SOME (snd (HOLogic.dest_number num)) else NONE
210 | factor_right_deg (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ vv) v =
211 if vv = v andalso not (Prog_Expr.occurs_in v t1) then SOME 1 else NONE
212 | factor_right_deg vv v =
213 if (vv = v) then SOME 1 else NONE;
214 fun mono_deg_in m v = (*case 1*)
215 if not (Prog_Expr.occurs_in v m) then (*case 1*) SOME 0 else factor_right_deg m v;
217 fun expand_deg_in t v =
219 fun edi ~1 ~1 (Const (\<^const_name>\<open>plus\<close>, _) $ t1 $ t2) =
220 (case mono_deg_in t2 v of (* $ is left associative*)
221 SOME d' => edi d' d' t1 | NONE => NONE)
222 | edi ~1 ~1 (Const (\<^const_name>\<open>minus\<close>, _) $ t1 $ t2) =
223 (case mono_deg_in t2 v of
224 SOME d' => edi d' d' t1 | NONE => NONE)
225 | edi d dmax (Const (\<^const_name>\<open>minus\<close>, _) $ t1 $ t2) =
226 (case mono_deg_in t2 v of (*(d = 0 andalso d' = 0) handle 3+4-...4 +x*)
227 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
229 | edi d dmax (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
230 (case mono_deg_in t2 v of
231 SOME d' => (*RL (d = 0 andalso d' = 0) need to handle 3+4-...4 +x*)
232 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
235 (case mono_deg_in t v of d as SOME _ => d | NONE => NONE)
236 | edi d dmax t = (*basecase last*)
237 (case mono_deg_in t v of
238 SOME d' => if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
242 fun poly_deg_in t v =
244 fun edi ~1 ~1 (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
245 (case mono_deg_in t2 v of (* $ is left associative *)
246 SOME d' => edi d' d' t1
248 | edi d dmax (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
249 (case mono_deg_in t2 v of
250 SOME d' => (*RL (d = 0 andalso (d' = 0)) handle 3+4-...4 +x*)
251 if d > d' orelse (d = 0 andalso d' = 0) then edi d' dmax t1 else NONE
254 (case mono_deg_in t v of
257 | edi d dmax t = (* basecase last *)
258 (case mono_deg_in t v of
260 if d > d' orelse (d = 0 andalso d' = 0) then SOME dmax else NONE
265 subsubsection \<open>for hard-coded AC rewriting (MG)\<close>
267 (**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
269 (*FIXME.0401: make SML-order local to make_polynomial(_) *)
270 (*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
271 (* Polynom --> List von Monomen *)
272 fun poly2list (Const (\<^const_name>\<open>plus\<close>,_) $ t1 $ t2) =
273 (poly2list t1) @ (poly2list t2)
276 (* Monom --> Liste von Variablen *)
277 fun monom2list (Const (\<^const_name>\<open>times\<close>,_) $ t1 $ t2) =
278 (monom2list t1) @ (monom2list t2)
279 | monom2list t = [t];
281 (* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
282 fun get_basStr (Const (\<^const_name>\<open>realpow\<close>,_) $ Free (str, _) $ _) = str
283 | get_basStr (Const (\<^const_name>\<open>realpow\<close>,_) $ n $ _) = TermC.to_string n
284 | get_basStr (Free (str, _)) = str
286 if TermC.is_num t then TermC.to_string t
287 else "|||"; (* gross gewichtet; für Brüche ect. *)
289 (* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
290 fun get_potStr (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ Free (str, _)) = str
291 | get_potStr (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =
292 if TermC.is_num t then TermC.to_string t else "|||"
293 | get_potStr (Free _) = "---" (* keine Hochzahl --> kleinst gewichtet *)
294 | get_potStr _ = "||||||"; (* gross gewichtet; für Brüch ect. *)
296 (* Umgekehrte string_ord *)
297 val string_ord_rev = rev_order o string_ord;
299 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
300 innerhalb eines Monomes:
301 - zuerst lexikographisch nach Variablenname
302 - wenn gleich: nach steigender Potenz *)
304 (@{print} {a = "var_ord ", a_b = "(" ^ UnparseC.term @{context} a ^ ", " ^ UnparseC.term @{context} b ^ ")",
305 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
306 prod_ord string_ord string_ord
307 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
309 fun var_ord (a,b: term) =
310 prod_ord string_ord string_ord
311 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
313 (* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
314 verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
315 - zuerst lexikographisch nach Variablenname
316 - wenn gleich: nach sinkender Potenz*)
317 fun var_ord_revPow (a, b: term) =
318 (@{print} {a = "var_ord_revPow ", at_bt = "(" ^ UnparseC.term @{context} a ^ ", " ^ UnparseC.term @{context} b ^ ")",
319 sort_args = "(" ^ get_basStr a ^ ", " ^ get_potStr a ^ "), (" ^ get_basStr b ^ ", " ^ get_potStr b ^ ")"};
320 prod_ord string_ord string_ord_rev
321 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b))
323 fun var_ord_revPow (a, b: term) =
324 prod_ord string_ord string_ord_rev
325 ((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
328 (* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
329 fun sort_varList ts =
330 (@{print} {a = "sort_varList", args = UnparseC.terms @{context} ts};
332 val sort_varList = sort var_ord;
334 (* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
335 Argumente in eine Liste *)
336 fun args u : term list =
338 fun stripc (f $ t, ts) = stripc (f, t::ts)
339 | stripc (t as Free _, ts) = (t::ts)
340 | stripc (_, ts) = ts
341 in stripc (u, []) end;
343 (* liefert True, falls der Term (Liste von Termen) nur Zahlen
344 (keine Variablen) enthaelt *)
345 fun filter_num ts = fold (curry and_) (map TermC.is_num ts) true
347 (* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
348 dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
349 fun is_nums t = filter_num [t];
351 (* Berechnet den Gesamtgrad eines Monoms *)
353 fun counter (n, []) = n
354 | counter (n, x :: xs) =
355 if (is_nums x) then counter (n, xs)
358 (Const (\<^const_name>\<open>realpow\<close>, _) $ Free _ $ t) =>
360 then counter (t |> HOLogic.dest_number |> snd |> curry op + n, xs)
361 else counter (n + 1000, xs) (*FIXME.MG?!*)
362 | (Const (\<^const_name>\<open>numeral\<close>, _) $ num) =>
363 counter (n + 1 + HOLogic.dest_numeral num, xs)
364 | _ => counter (n + 1, xs)) (*FIXME.MG?! ... Brüche ect.*)
366 fun monom_degree l = counter (0, l)
369 (* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
370 der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
371 werden jedoch dabei ignoriert (uebersprungen) *)
372 fun dict_cond_ord _ _ ([], []) = (@{print} {a = "dict_cond_ord ([], [])"}; EQUAL)
373 | dict_cond_ord _ _ ([], _ :: _) = (@{print} {a = "dict_cond_ord ([], _ :: _)"}; LESS)
374 | dict_cond_ord _ _ (_ :: _, []) = (@{print} {a = "dict_cond_ord (_ :: _, [])"}; GREATER)
375 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
376 (@{print} {a = "dict_cond_ord", args = "(" ^ UnparseC.terms @{context} (x :: xs) ^ ", " ^
377 UnparseC.terms @{context} (y :: ys) ^ ")",
378 is_nums = "(" ^ LibraryC.bool2str (cond x) ^ ", " ^ LibraryC.bool2str (cond y) ^ ")"};
379 case (cond x, cond y) of
381 (case elem_ord (x, y) of
382 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
384 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
385 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
386 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
387 fun dict_cond_ord _ _ ([], []) = EQUAL
388 | dict_cond_ord _ _ ([], _ :: _) = LESS
389 | dict_cond_ord _ _ (_ :: _, []) = GREATER
390 | dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
391 (case (cond x, cond y) of
393 (case elem_ord (x, y) of
394 EQUAL => dict_cond_ord elem_ord cond (xs, ys)
396 | (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
397 | (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
398 | (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
400 (* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
401 zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
402 dabei werden Koeffizienten ignoriert (2*3*a \<up> 2*4*b gilt wie a \<up> 2*b) *)
403 fun degree_ord (xs, ys) =
404 prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
405 ((monom_degree xs, xs), (monom_degree ys, ys));
407 fun hd_str str = substring (str, 0, 1);
408 fun tl_str str = substring (str, 1, (size str) - 1);
410 (* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
411 fun get_koeff_of_mon [] = raise ERROR "get_koeff_of_mon: called with l = []"
412 | get_koeff_of_mon (x :: _) = if is_nums x then SOME x else NONE;
414 (* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
415 fun koeff2ordStr (SOME t) =
418 if (t |> HOLogic.dest_number |> snd) < 0
419 then (t |> HOLogic.dest_number |> snd |> curry op * ~1 |> string_of_int) ^ "0" (* 3 < -3 *)
420 else (t |> HOLogic.dest_number |> snd |> string_of_int)
421 else "aaa" (* "num.Ausdruck" --> gross *)
422 | koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
424 (* Order zum Vergleich von Koeffizienten (strings):
425 "kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
426 fun compare_koeff_ord (xs, ys) = string_ord
427 ((koeff2ordStr o get_koeff_of_mon) xs,
428 (koeff2ordStr o get_koeff_of_mon) ys);
430 (* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
431 fun koeff_degree_ord (xs, ys) =
432 prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
434 (* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
436 val sort_monList = sort koeff_degree_ord;
438 (* Alternativ zu degree_ord koennte auch die viel einfachere und
439 kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
440 fuer unsere Zwecke geeignet!
442 fun simple_ord (al,bl: term list) = dict_ord string_ord
443 (map get_basStr al, map get_basStr bl);
445 val sort_monList = sort simple_ord; *)
447 (* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
448 (mit gewuenschtem Typen T) *)
449 fun plus T = Const (\<^const_name>\<open>plus\<close>, [T,T] ---> T);
450 fun mult T = Const (\<^const_name>\<open>times\<close>, [T,T] ---> T);
451 fun binop op_ t1 t2 = op_ $ t1 $ t2;
452 fun create_prod T (a,b) = binop (mult T) a b;
453 fun create_sum T (a,b) = binop (plus T) a b;
455 (* löscht letztes Element einer Liste *)
456 fun drop_last l = take ((length l)-1,l);
458 (* Liste von Variablen --> Monom *)
459 fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
461 foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
462 gleiche Monome zusammengefasst werden können (collect_numerals)!
463 zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
465 (* Liste von Monomen --> Polynom *)
466 fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
468 foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
469 bessere Darstellung, da keine Klammern sichtbar!
470 (und discard_parentheses in make_polynomial hat weniger zu tun) *)
472 (* sorts the variables (faktors) of an expanded polynomial lexicographical *)
473 fun sort_variables t =
475 val ll = map monom2list (poly2list t);
476 val lls = map sort_varList ll;
478 val ls = map (create_monom T) lls;
479 in create_polynom T ls end;
481 (* sorts the monoms of an expanded and variable-sorted polynomial
485 val ll = map monom2list (poly2list t);
486 val lls = sort_monList ll;
487 val T = Term.type_of t;
488 val ls = map (create_monom T) lls;
489 in create_polynom T ls end;
492 subsubsection \<open>rewrite order for hard-coded AC rewriting\<close>
494 local (*. for make_polynomial .*)
496 open Term; (* for type order = EQUAL | LESS | GREATER *)
498 fun pr_ord EQUAL = "EQUAL"
499 | pr_ord LESS = "LESS"
500 | pr_ord GREATER = "GREATER";
502 fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
504 \<^const_name>\<open>realpow\<close> => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
505 | _ => (((a, 0), T), 0))
506 | dest_hd' (Free (a, T)) = (((a, 0), T), 1)(*TODOO handle this as numeral, too? see EqSystem.thy*)
507 | dest_hd' (Var v) = (v, 2)
508 | dest_hd' (Bound i) = ((("", i), dummyT), 3)
509 | dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4)
510 | dest_hd' t = raise TERM ("dest_hd'", [t]);
512 fun size_of_term' (Const(str,_) $ t) =
513 if \<^const_name>\<open>realpow\<close>= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
514 | size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
515 | size_of_term' (f$t) = size_of_term' f + size_of_term' t
516 | size_of_term' _ = 1;
518 fun term_ord' pr ctxt (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
519 (case term_ord' pr ctxt (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
520 | term_ord' pr ctxt (t, u) =
523 val (f, ts) = strip_comb t and (g, us) = strip_comb u;
524 val _ = tracing ("t= f@ts= \"" ^ UnparseC.term ctxt f ^ "\" @ \"[" ^
525 commas (map (UnparseC.term ctxt) ts) ^ "]\"");
526 val _ = tracing("u= g@us= \"" ^ UnparseC.term ctxt g ^ "\" @ \"[" ^
527 commas (map (UnparseC.term ctxt) us) ^ "]\"");
528 val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
529 string_of_int (size_of_term' u) ^ ")");
530 val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
531 val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false ctxt) (ts, us));
532 val _ = tracing ("-------");
535 case int_ord (size_of_term' t, size_of_term' u) of
537 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
538 (case hd_ord (f, g) of EQUAL => (terms_ord str pr ctxt) (ts, us)
542 and hd_ord (f, g) = (* ~ term.ML *)
543 prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
544 and terms_ord _ pr ctxt (ts, us) =
545 list_ord (term_ord' pr ctxt) (ts, us);
549 fun ord_make_polynomial (pr:bool) ctxt (_: subst) (ts, us) =
550 (term_ord' pr ctxt (TermC.numerals_to_Free ts, TermC.numerals_to_Free us) = LESS );
558 setup \<open>Know_Store.add_rew_ords [
559 ("termlessI", termlessI),
560 ("ord_make_polynomial", ord_make_polynomial false)]\<close>
562 subsection \<open>predicates\<close>
563 subsubsection \<open>in specifications\<close>
565 (* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
566 fun is_polyrat_in t v =
568 fun finddivide (_ $ _ $ _ $ _) _ = raise ERROR("is_polyrat_in:")
569 (* at the moment there is no term like this, but ....*)
570 | finddivide (Const (\<^const_name>\<open>divide\<close>,_) $ _ $ b) v = not (Prog_Expr.occurs_in v b)
571 | finddivide (_ $ t1 $ t2) v = finddivide t1 v orelse finddivide t2 v
572 | finddivide (_ $ t1) v = finddivide t1 v
573 | finddivide _ _ = false;
574 in finddivide t v end;
576 fun is_expanded_in t v = case expand_deg_in t v of SOME _ => true | NONE => false;
577 fun is_poly_in t v = case poly_deg_in t v of SOME _ => true | NONE => false;
578 fun has_degree_in t v = case expand_deg_in t v of SOME d => d | NONE => ~1;
580 (*.the expression contains + - * ^ only ?
581 this is weaker than 'is_polynomial' !.*)
582 fun is_polyexp (Free _) = true
583 | is_polyexp (Const _) = true (* potential danger: bdv is not considered *)
584 | is_polyexp (Const (\<^const_name>\<open>plus\<close>,_) $ Free _ $ num) =
585 if TermC.is_num num then true
586 else if TermC.is_variable num then true
588 | is_polyexp (Const (\<^const_name>\<open>plus\<close>, _) $ num $ Free _) =
589 if TermC.is_num num then true
590 else if TermC.is_variable num then true
592 | is_polyexp (Const (\<^const_name>\<open>minus\<close>, _) $ Free _ $ num) =
593 if TermC.is_num num then true
594 else if TermC.is_variable num then true
596 | is_polyexp (Const (\<^const_name>\<open>times\<close>, _) $ num $ Free _) =
597 if TermC.is_num num then true
598 else if TermC.is_variable num then true
600 | is_polyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ Free _ $ num) =
601 if TermC.is_num num then true
602 else if TermC.is_variable num then true
604 | is_polyexp (Const (\<^const_name>\<open>plus_class.plus\<close>,_) $ t1 $ t2) =
605 ((is_polyexp t1) andalso (is_polyexp t2))
606 | is_polyexp (Const (\<^const_name>\<open>Groups.minus_class.minus\<close>,_) $ t1 $ t2) =
607 ((is_polyexp t1) andalso (is_polyexp t2))
608 | is_polyexp (Const (\<^const_name>\<open>Groups.times_class.times\<close>,_) $ t1 $ t2) =
609 ((is_polyexp t1) andalso (is_polyexp t2))
610 | is_polyexp (Const (\<^const_name>\<open>realpow\<close>,_) $ t1 $ t2) =
611 ((is_polyexp t1) andalso (is_polyexp t2))
612 | is_polyexp num = TermC.is_num num;
615 subsubsection \<open>for hard-coded AC rewriting\<close>
617 (* auch Klammerung muss übereinstimmen;
618 sort_variables klammert Produkte rechtslastig*)
619 fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
621 fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
624 subsection \<open>evaluations functions\<close>
625 subsubsection \<open>for predicates\<close>
627 fun eval_is_polyrat_in _ _(p as (Const (\<^const_name>\<open>Poly.is_polyrat_in\<close>, _) $ t $ v)) _ =
629 then SOME ((UnparseC.term @{context} p) ^ " = True",
630 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
631 else SOME ((UnparseC.term @{context} p) ^ " = True",
632 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
633 | eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
635 (*("is_expanded_in", ("Poly.is_expanded_in", eval_is_expanded_in ""))*)
636 fun eval_is_expanded_in _ _
637 (p as (Const (\<^const_name>\<open>Poly.is_expanded_in\<close>, _) $ t $ v)) _ =
638 if is_expanded_in t v
639 then SOME ((UnparseC.term @{context} p) ^ " = True",
640 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
641 else SOME ((UnparseC.term @{context} p) ^ " = True",
642 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
643 | eval_is_expanded_in _ _ _ _ = NONE;
645 (*("is_poly_in", ("Poly.is_poly_in", eval_is_poly_in ""))*)
646 fun eval_is_poly_in _ _
647 (p as (Const (\<^const_name>\<open>Poly.is_poly_in\<close>, _) $ t $ v)) _ =
649 then SOME ((UnparseC.term @{context} p) ^ " = True",
650 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
651 else SOME ((UnparseC.term @{context} p) ^ " = True",
652 HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
653 | eval_is_poly_in _ _ _ _ = NONE;
655 (*("has_degree_in", ("Poly.has_degree_in", eval_has_degree_in ""))*)
656 fun eval_has_degree_in _ _
657 (p as (Const (\<^const_name>\<open>Poly.has_degree_in\<close>, _) $ t $ v)) _ =
658 let val d = has_degree_in t v
659 val d' = TermC.term_of_num HOLogic.realT d
660 in SOME ((UnparseC.term @{context} p) ^ " = " ^ (string_of_int d),
661 HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
663 | eval_has_degree_in _ _ _ _ = NONE;
665 (*("is_polyexp", ("Poly.is_polyexp", eval_is_polyexp ""))*)
666 fun eval_is_polyexp (thmid:string) _
667 (t as (Const (\<^const_name>\<open>is_polyexp\<close>, _) $ arg)) ctxt =
669 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
670 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
671 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
672 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
673 | eval_is_polyexp _ _ _ _ = NONE;
676 subsubsection \<open>for hard-coded AC rewriting\<close>
679 (*("is_addUnordered", ("Poly.is_addUnordered", eval_is_addUnordered ""))*)
680 fun eval_is_addUnordered (thmid:string) _
681 (t as (Const (\<^const_name>\<open>is_addUnordered\<close>, _) $ arg)) ctxt =
682 if is_addUnordered arg
683 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
684 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
685 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
686 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
687 | eval_is_addUnordered _ _ _ _ = NONE;
689 fun eval_is_multUnordered (thmid:string) _
690 (t as (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ arg)) ctxt =
691 if is_multUnordered arg
692 then SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
693 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
694 else SOME (TermC.mk_thmid thmid (UnparseC.term ctxt arg) "",
695 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
696 | eval_is_multUnordered _ _ _ _ = NONE;
698 calculation is_polyrat_in = \<open>eval_is_polyrat_in "#eval_is_polyrat_in"\<close>
699 calculation is_expanded_in = \<open>eval_is_expanded_in ""\<close>
700 calculation is_poly_in = \<open>eval_is_poly_in ""\<close>
701 calculation has_degree_in = \<open>eval_has_degree_in ""\<close>
702 calculation is_polyexp = \<open>eval_is_polyexp ""\<close>
703 calculation is_multUnordered = \<open>eval_is_multUnordered ""\<close>
704 calculation is_addUnordered = \<open>eval_is_addUnordered ""\<close>
706 subsection \<open>rule-sets\<close>
707 subsubsection \<open>without specific order\<close>
709 (* used only for merge *)
710 val calculate_Poly = Rule_Set.append_rules "calculate_PolyFIXXXME.not.impl." Rule_Set.empty [];
712 (*.for evaluation of conditions in rewrite rules.*)
713 val Poly_erls = Rule_Set.append_rules "Poly_erls" Atools_erls [
714 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
715 \<^rule_thm>\<open>real_unari_minus\<close>,
716 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
717 \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
718 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
719 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
721 val poly_crls = Rule_Set.append_rules "poly_crls" Atools_crls [
722 \<^rule_eval>\<open>HOL.eq\<close> (Prog_Expr.eval_equal "#equal_"),
723 \<^rule_thm>\<open>real_unari_minus\<close>,
724 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
725 \<^rule_eval>\<open>minus\<close> (Calc_Binop.numeric "#sub_"),
726 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
727 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")];
731 Rule_Def.Repeat {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
732 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
734 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
735 \<^rule_thm>\<open>distrib_left\<close> (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)],
736 program = Rule.Empty_Prog};
739 \<close> ML \<open>@{term "1 is_num"}\<close>
741 (* asm_rls for calculate_Rational + etc *)
743 Rule_Def.Repeat {id = "powers_erls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
744 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
746 \<^rule_eval>\<open>matches\<close> (Prog_Expr.eval_matches "#matches_"),
747 \<^rule_eval>\<open>is_atom\<close> (Prog_Expr.eval_is_atom "#is_atom_"),
748 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
749 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
750 \<^rule_eval>\<open>ord_class.less\<close> (Prog_Expr.eval_equ "#less_"),
751 \<^rule_thm>\<open>not_false\<close>,
752 \<^rule_thm>\<open>not_true\<close>,
753 \<^rule_eval>\<open>plus_class.plus\<close> (Calc_Binop.numeric "#add_")],
754 program = Rule.Empty_Prog};
758 Rule_Def.Repeat {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
759 asm_rls = powers_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
761 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
762 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)],
763 program = Rule.Empty_Prog};
766 Rule_Def.Repeat{id = "expand_poly_", preconds = [],
767 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
768 asm_rls = powers_erls, prog_rls = Rule_Set.Empty,
769 calc = [], errpatts = [],
771 \<^rule_thm>\<open>real_plus_binom_pow4\<close>, (*"(a + b) \<up> 4 = ... "*)
772 \<^rule_thm>\<open>real_plus_binom_pow5\<close>, (*"(a + b) \<up> 5 = ... "*)
773 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, (*"(a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
774 (*WN071229 changed/removed for Schaerding -----vvv*)
775 (*\<^rule_thm>\<open>real_plus_binom_pow2\<close>,*) (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
776 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = (a + b) * (a + b)"*)
777 (*\<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>,*) (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
778 (*\<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>,*) (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
779 (*WN071229 changed/removed for Schaerding -----^^^*)
781 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
782 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
784 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
785 \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
787 \<^rule_thm>\<open>realpow_minus_even\<close>, (*"n is_even ==> (- r) \<up> n = r \<up> n"*)
788 \<^rule_thm>\<open>realpow_minus_odd\<close> (*"Not (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*)],
789 program = Rule.Empty_Prog};
791 val expand_poly_rat_ =
792 Rule_Def.Repeat{id = "expand_poly_rat_", preconds = [],
793 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
794 asm_rls = Rule_Set.append_rules "Rule_Set.empty-expand_poly_rat_" Rule_Set.empty [
795 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp ""),
796 \<^rule_eval>\<open>is_even\<close> (Prog_Expr.eval_is_even "#is_even_"),
797 \<^rule_thm>\<open>not_false\<close>,
798 \<^rule_thm>\<open>not_true\<close> ],
799 prog_rls = Rule_Set.Empty,
800 calc = [], errpatts = [],
802 \<^rule_thm>\<open>real_plus_binom_pow4_poly\<close>, (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 4 = ... "*)
803 \<^rule_thm>\<open>real_plus_binom_pow5_poly\<close>, (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 5 = ... "*)
804 \<^rule_thm>\<open>real_plus_binom_pow2_poly\<close>, (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
805 \<^rule_thm>\<open>real_plus_binom_pow3_poly\<close>,
806 (*"[| a is_polyexp; b is_polyexp |] ==> (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3" *)
807 \<^rule_thm>\<open>real_plus_minus_binom1_p_p\<close>, (*"(a + b)*(a + -1 * b) = a \<up> 2 + -1*b \<up> 2"*)
808 \<^rule_thm>\<open>real_plus_minus_binom2_p_p\<close>, (*"(a + -1 * b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
810 \<^rule_thm>\<open>real_add_mult_distrib_poly\<close>, (*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
811 \<^rule_thm>\<open>real_add_mult_distrib2_poly\<close>, (*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
813 \<^rule_thm>\<open>realpow_multI_poly\<close>, (*"[| r is_polyexp; s is_polyexp |] ==> (r * s) \<up> n = r \<up> n * s \<up> n"*)
814 \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
815 \<^rule_thm>\<open>realpow_minus_even\<close>, (*"n is_even ==> (- r) \<up> n = r \<up> n"*)
816 \<^rule_thm>\<open>realpow_minus_odd\<close> (*"\<not> (n is_even) ==> (- r) \<up> n = -1 * r \<up> n"*) ],
817 program = Rule.Empty_Prog};
819 val simplify_power_ =
820 Rule_Def.Repeat{id = "simplify_power_", preconds = [],
821 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
822 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty,
823 calc = [], errpatts = [],
825 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
826 a*(a*a) --> a*a \<up> 2 und nicht a*(a*a) --> a \<up> 2*a *)
827 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r * r = r \<up> 2"*)
828 \<^rule_thm>\<open>realpow_twoI_assoc_l\<close>, (*"r * (r * s) = r \<up> 2 * s"*)
830 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
831 \<^rule_thm>\<open>realpow_plus_1_assoc_l\<close>, (*"r * (r \<up> m * s) = r \<up> (1 + m) * s"*)
832 (*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a \<up> 2*(a*b) *)
833 \<^rule_thm>\<open>realpow_plus_1_assoc_l2\<close>, (*"r \<up> m * (r * s) = r \<up> (1 + m) * s"*)
835 \<^rule_thm_sym>\<open>realpow_addI\<close>, (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
836 \<^rule_thm>\<open>realpow_addI_assoc_l\<close>, (*"r \<up> n * (r \<up> m * s) = r \<up> (n + m) * s"*)
838 (* ist in expand_poly - wird hier aber auch gebraucht, wegen: "r * r = r \<up> 2" wenn r=a \<up> b*)
839 \<^rule_thm>\<open>realpow_pow\<close> (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)],
840 program = Rule.Empty_Prog};
842 val calc_add_mult_pow_ =
843 Rule_Def.Repeat{id = "calc_add_mult_pow_", preconds = [],
844 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
845 asm_rls = Atools_erls(*erls3.4.03*),prog_rls = Rule_Set.Empty,
846 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
847 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
848 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
852 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
853 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
854 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
855 program = Rule.Empty_Prog};
857 val reduce_012_mult_ =
858 Rule_Def.Repeat{id = "reduce_012_mult_", preconds = [],
859 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
860 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
861 calc = [], errpatts = [],
862 rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
863 \<^rule_thm>\<open>mult_1_right\<close>, (*"z * 1 = z"*) (*wegen "a * b * b \<up> (-1) + a"*)
864 \<^rule_thm>\<open>realpow_zeroI\<close>, (*"r \<up> 0 = 1"*) (*wegen "a*a \<up> (-1)*c + b + c"*)
865 \<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*)
866 \<^rule_thm>\<open>realpow_eq_oneI\<close> (*"1 \<up> n = 1"*)],
867 program = Rule.Empty_Prog};
869 val collect_numerals_ =
870 Rule_Def.Repeat{id = "collect_numerals_", preconds = [],
871 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
872 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
873 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_"))
876 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
877 \<^rule_thm>\<open>real_num_collect_assoc_r\<close>,
878 (*"[| l is_num; m is_num |] ==> (k + m * n) + l * n = k + (l + m)*n"*)
879 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
880 \<^rule_thm>\<open>real_one_collect_assoc_r\<close>, (*"m is_num ==> (k + n) + m * n = k + (m + 1) * n"*)
882 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
884 (*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
885 (a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
886 \<^rule_thm>\<open>real_mult_2_assoc_r\<close>, (*"(k + z1) + z1 = k + 2 * z1"*)
887 \<^rule_thm_sym>\<open>real_mult_2\<close> (*"z1 + z1 = 2 * z1"*)],
888 program = Rule.Empty_Prog};
891 Rule_Def.Repeat{id = "reduce_012_", preconds = [],
892 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
893 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
895 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
896 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
897 \<^rule_thm>\<open>mult_zero_right\<close>, (*"z * 0 = 0"*)
898 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
899 \<^rule_thm>\<open>add_0_right\<close>, (*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
901 (*\<^rule_thm>\<open>realpow_oneI\<close>*) (*"?r \<up> 1 = ?r"*)
902 \<^rule_thm>\<open>division_ring_divide_zero\<close> (*"0 / ?x = 0"*)],
903 program = Rule.Empty_Prog};
905 val discard_parentheses1 =
906 Rule_Set.append_rules "discard_parentheses1" Rule_Set.empty [
907 \<^rule_thm_sym>\<open>mult.assoc\<close> (*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
908 (*\<^rule_thm_sym>\<open>add.assoc\<close>*) (*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)];
911 Rule_Def.Repeat{id = "expand_poly", preconds = [],
912 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
913 asm_rls = powers_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
915 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
916 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
918 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2*a*b + b \<up> 2"*)
919 \<^rule_thm>\<open>real_minus_binom_pow2_p\<close>, (*"(a - b) \<up> 2 = a \<up> 2 + -2*a*b + b \<up> 2"*)
920 \<^rule_thm>\<open>real_plus_minus_binom1_p\<close>, (*"(a + b)*(a - b) = a \<up> 2 + -1*b \<up> 2"*)
921 \<^rule_thm>\<open>real_plus_minus_binom2_p\<close>, (*"(a - b)*(a + b) = a \<up> 2 + -1*b \<up> 2"*)
923 \<^rule_thm>\<open>minus_minus\<close> (*"- (- ?z) = ?z"*),
924 \<^rule_thm>\<open>real_diff_minus\<close> (*"a - b = a + -1 * b"*),
925 \<^rule_thm>\<open>real_mult_minus1_sym\<close> (*"\<not>(z is_num) ==> - (z::real) = -1 * z"*)
927 (*\<^rule_thm>\<open>real_minus_add_distrib\<close>,*) (*"- (?x + ?y) = - ?x + - ?y"*)
928 (*\<^rule_thm>\<open>real_diff_plus\<close>*) (*"a - b = a + -b"*)],
929 program = Rule.Empty_Prog};
932 Rule_Def.Repeat{id = "simplify_power", preconds = [],
933 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
934 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty,
935 calc = [], errpatts = [],
937 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
939 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
940 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
941 \<^rule_thm>\<open>realpow_pow\<close>, (*"(a \<up> b) \<up> c = a \<up> (b * c)"*)
942 \<^rule_thm_sym>\<open>realpow_addI\<close>, (*"r \<up> n * r \<up> m = r \<up> (n + m)"*)
943 \<^rule_thm>\<open>realpow_oneI\<close>, (*"r \<up> 1 = r"*)
944 \<^rule_thm>\<open>realpow_eq_oneI\<close> (*"1 \<up> n = 1"*)],
945 program = Rule.Empty_Prog};
947 val collect_numerals =
948 Rule_Def.Repeat{id = "collect_numerals", preconds = [],
949 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
950 asm_rls = Atools_erls(*erls3.4.03*),prog_rls = Rule_Set.Empty,
951 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
952 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
953 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
956 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
957 \<^rule_thm>\<open>real_num_collect_assoc\<close>,
958 (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
959 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
960 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
961 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
962 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
963 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
964 program = Rule.Empty_Prog};
966 Rule_Def.Repeat{id = "reduce_012", preconds = [],
967 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
968 asm_rls = Rule_Set.append_rules "erls_in_reduce_012" Rule_Set.empty [
969 \<^rule_eval>\<open>is_num\<close> (Prog_Expr.eval_is_num "#is_num_"),
970 \<^rule_thm>\<open>not_false\<close>,
971 \<^rule_thm>\<open>not_true\<close>],
972 prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
974 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
975 (*\<^rule_thm>\<open>real_mult_minus1\<close>,14.3.03*) (*"-1 * z = - z"*)
976 \<^rule_thm>\<open>real_minus_mult_left\<close>, (*"\<not> ((a::real) is_num) ==> (- a) * b = - (a * b)"*)
977 (*\<^rule_thm>\<open>real_minus_mult_cancel\<close>, (*"- ?x * - ?y = ?x * ?y"*)---*)
978 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
979 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
980 \<^rule_thm>\<open>add_0_right\<close>, (*"a + - a = 0"*)
981 \<^rule_thm>\<open>right_minus\<close>, (*"?z + - ?z = 0"*)
982 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
983 \<^rule_thm>\<open>real_mult_2_assoc\<close> (*"z1 + (z1 + k) = 2 * z1 + k"*)],
984 program = Rule.Empty_Prog};
986 val discard_parentheses =
987 Rule_Set.append_rules "discard_parentheses" Rule_Set.empty
988 [\<^rule_thm_sym>\<open>mult.assoc\<close>, \<^rule_thm_sym>\<open>add.assoc\<close>];
991 subsubsection \<open>hard-coded AC rewriting\<close>
993 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
994 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
996 Rule_Def.Repeat{id = "order_add_mult", preconds = [],
997 rew_ord = ("ord_make_polynomial", ord_make_polynomial false),
998 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
999 calc = [], errpatts = [],
1001 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
1002 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1003 \<^rule_thm>\<open>mult.assoc\<close>, (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
1004 \<^rule_thm>\<open>add.commute\<close>, (*z + w = w + z*)
1005 \<^rule_thm>\<open>add.left_commute\<close>, (*x + (y + z) = y + (x + z)*)
1006 \<^rule_thm>\<open>add.assoc\<close> (*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)],
1007 program = Rule.Empty_Prog};
1008 (*MG.0401: termorders for multivariate polys dropped due to principal problems:
1009 (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
1011 Rule_Def.Repeat{id = "order_mult", preconds = [],
1012 rew_ord = ("ord_make_polynomial",ord_make_polynomial false),
1013 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
1014 calc = [], errpatts = [],
1016 \<^rule_thm>\<open>mult.commute\<close>, (* z * w = w * z *)
1017 \<^rule_thm>\<open>real_mult_left_commute\<close>, (*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
1018 \<^rule_thm>\<open>mult.assoc\<close> (*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)],
1019 program = Rule.Empty_Prog};
1022 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1023 []:(Rule.rule * (term * term list)) list;
1024 fun init_state (_: term) = Rule_Set.e_rrlsstate;
1025 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1026 ([]:(Rule.rule * (term * term list)) list);
1027 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1028 fun normal_form t = SOME (sort_variables t, []: term list);
1031 Rule_Set.Rrls {id = "order_mult_",
1033 (* ?p matched with the current term gives an environment,
1034 which evaluates (the instantiated) "?p is_multUnordered" to true *)
1035 [([ParseC.patt_opt \<^theory> "?p is_multUnordered" |> the],
1036 ParseC.patt_opt \<^theory> "?p :: real" |> the)],
1037 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1038 asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
1039 [\<^rule_eval>\<open>is_multUnordered\<close> (eval_is_multUnordered "")],
1040 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1041 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1042 ("DIVIDE", (\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
1043 ("POWER" , (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))],
1045 program = Rule.Rfuns {init_state = init_state,
1046 normal_form = normal_form,
1047 locate_rule = locate_rule,
1048 next_rule = next_rule,
1049 attach_form = attach_form}};
1050 val order_mult_rls_ =
1051 Rule_Def.Repeat {id = "order_mult_rls_", preconds = [],
1052 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1053 asm_rls = Rule_Set.empty,prog_rls = Rule_Set.Empty,
1054 calc = [], errpatts = [],
1056 Rule.Rls_ order_mult_],
1057 program = Rule.Empty_Prog};
1061 fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
1062 []: (Rule.rule * (term * term list)) list;
1063 fun init_state (_: term) = Rule_Set.e_rrlsstate;
1064 fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
1065 ([]: (Rule.rule * (term * term list)) list);
1066 fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
1067 fun normal_form t = SOME (sort_monoms t,[]: term list);
1070 Rule_Set.Rrls {id = "order_add_",
1071 prepat = [(*WN.18.6.03 Preconditions und Pattern,
1072 die beide passen muessen, damit das Rule_Set.Rrls angewandt wird*)
1073 ([ParseC.patt_opt @{theory} "?p is_addUnordered" |> the],
1074 ParseC.patt_opt @{theory} "?p :: real" |> the
1075 (*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
1076 fuer die Evaluation der Precondition "p is_addUnordered"*))],
1077 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1078 asm_rls = Rule_Set.append_rules "Rule_Set.empty-is_addUnordered" Rule_Set.empty(*MG: poly_erls*)
1079 [\<^rule_eval>\<open>is_addUnordered\<close> (eval_is_addUnordered "")],
1081 ("PLUS" ,(\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1082 ("TIMES" ,(\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1083 ("DIVIDE",(\<^const_name>\<open>divide\<close>, Prog_Expr.eval_cancel "#divide_e")),
1084 ("POWER" ,(\<^const_name>\<open>realpow\<close> , Calc_Binop.numeric "#power_"))],
1086 program = Rule.Rfuns {
1087 init_state = init_state,
1088 normal_form = normal_form,
1089 locate_rule = locate_rule,
1090 next_rule = next_rule,
1091 attach_form = attach_form}};
1093 val order_add_rls_ =
1094 Rule_Def.Repeat {id = "order_add_rls_", preconds = [],
1095 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1096 asm_rls = Rule_Set.empty, prog_rls = Rule_Set.Empty,
1097 calc = [], errpatts = [],
1099 Rule.Rls_ order_add_],
1100 program = Rule.Empty_Prog};
1103 text \<open>rule-set make_polynomial also named norm_Poly:
1104 Rewrite order has not been implemented properly; the order is better in
1105 make_polynomial_in (coded in SML).
1106 Notes on state of development:
1107 \# surprise 2006: test --- norm_Poly NOT COMPLETE ---
1108 \# migration Isabelle2002 --> 2011 weakened the rule set, see test
1109 --- Matthias Goldgruber 2003 rewrite orders ---, raise ERROR "ord_make_polynomial_in #16b"
1112 (*. see MG-DA.p.52ff .*)
1113 val make_polynomial(*MG.03, overwrites version from above,
1114 previously 'make_polynomial_'*) =
1115 Rule_Set.Sequence {id = "make_polynomial", preconds = []:term list,
1116 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1117 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,calc = [], errpatts = [],
1119 Rule.Rls_ discard_minus,
1120 Rule.Rls_ expand_poly_,
1121 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1122 Rule.Rls_ order_mult_rls_,
1123 Rule.Rls_ simplify_power_,
1124 Rule.Rls_ calc_add_mult_pow_,
1125 Rule.Rls_ reduce_012_mult_,
1126 Rule.Rls_ order_add_rls_,
1127 Rule.Rls_ collect_numerals_,
1128 Rule.Rls_ reduce_012_,
1129 Rule.Rls_ discard_parentheses1],
1130 program = Rule.Empty_Prog};
1133 val norm_Poly(*=make_polynomial*) =
1134 Rule_Set.Sequence {id = "norm_Poly", preconds = []:term list,
1135 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1136 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1138 Rule.Rls_ discard_minus,
1139 Rule.Rls_ expand_poly_,
1140 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1141 Rule.Rls_ order_mult_rls_,
1142 Rule.Rls_ simplify_power_,
1143 Rule.Rls_ calc_add_mult_pow_,
1144 Rule.Rls_ reduce_012_mult_,
1145 Rule.Rls_ order_add_rls_,
1146 Rule.Rls_ collect_numerals_,
1147 Rule.Rls_ reduce_012_,
1148 Rule.Rls_ discard_parentheses1],
1149 program = Rule.Empty_Prog};
1152 (* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1
1153 and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
1154 (* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
1155 val make_rat_poly_with_parentheses =
1156 Rule_Set.Sequence{id = "make_rat_poly_with_parentheses", preconds = []:term list,
1157 rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1158 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty, calc = [], errpatts = [],
1160 Rule.Rls_ discard_minus,
1161 Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
1162 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1163 Rule.Rls_ order_mult_rls_,
1164 Rule.Rls_ simplify_power_,
1165 Rule.Rls_ calc_add_mult_pow_,
1166 Rule.Rls_ reduce_012_mult_,
1167 Rule.Rls_ order_add_rls_,
1168 Rule.Rls_ collect_numerals_,
1169 Rule.Rls_ reduce_012_
1170 (*Rule.Rls_ discard_parentheses1 *)],
1171 program = Rule.Empty_Prog};
1174 (*.a minimal ruleset for reverse rewriting of factions [2];
1175 compare expand_binoms.*)
1177 Rule_Set.Sequence{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
1178 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
1179 calc = [(*("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1180 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1181 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))*)
1184 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
1185 \<^rule_thm>\<open>real_plus_binom_times1\<close>, (*"(a + 1*b)*(a + -1*b) = a \<up> 2 + -1*b \<up> 2"*)
1186 \<^rule_thm>\<open>real_plus_binom_times2\<close>, (*"(a + -1*b)*(a + 1*b) = a \<up> 2 + -1*b \<up> 2"*)
1188 \<^rule_thm>\<open>mult_1_left\<close>,(*"1 * z = z"*)
1190 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1191 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1193 \<^rule_thm>\<open>mult.assoc\<close>, (*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
1194 Rule.Rls_ order_mult_rls_,
1195 (*Rule.Rls_ order_add_rls_,*)
1197 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1198 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1199 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
1201 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
1202 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)
1203 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
1205 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |]==>l * n + m * n = (l + m) * n"*)
1206 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1207 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1208 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
1210 \<^rule_thm>\<open>realpow_multI\<close>, (*"(r * s) \<up> n = r \<up> n * s \<up> n"*)
1212 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1213 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1214 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
1216 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
1217 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
1218 \<^rule_thm>\<open>add_0_left\<close> (*0 + z = z*)
1220 (*Rule.Rls_ order_add_rls_*)
1222 program = Rule.Empty_Prog};
1225 subsection \<open>rule-sets with explicit program for intermediate steps\<close>
1226 partial_function (tailrec) expand_binoms_2 :: "real \<Rightarrow> real"
1228 "expand_binoms_2 term = (
1230 (Try (Repeat (Rewrite ''real_plus_binom_pow2''))) #>
1231 (Try (Repeat (Rewrite ''real_plus_binom_times''))) #>
1232 (Try (Repeat (Rewrite ''real_minus_binom_pow2''))) #>
1233 (Try (Repeat (Rewrite ''real_minus_binom_times''))) #>
1234 (Try (Repeat (Rewrite ''real_plus_minus_binom1''))) #>
1235 (Try (Repeat (Rewrite ''real_plus_minus_binom2''))) #>
1237 (Try (Repeat (Rewrite ''mult_1_left''))) #>
1238 (Try (Repeat (Rewrite ''mult_zero_left''))) #>
1239 (Try (Repeat (Rewrite ''add_0_left''))) #>
1241 (Try (Repeat (Calculate ''PLUS''))) #>
1242 (Try (Repeat (Calculate ''TIMES''))) #>
1243 (Try (Repeat (Calculate ''POWER''))) #>
1245 (Try (Repeat (Rewrite ''sym_realpow_twoI''))) #>
1246 (Try (Repeat (Rewrite ''realpow_plus_1''))) #>
1247 (Try (Repeat (Rewrite ''sym_real_mult_2''))) #>
1248 (Try (Repeat (Rewrite ''real_mult_2_assoc''))) #>
1250 (Try (Repeat (Rewrite ''real_num_collect''))) #>
1251 (Try (Repeat (Rewrite ''real_num_collect_assoc''))) #>
1253 (Try (Repeat (Rewrite ''real_one_collect''))) #>
1254 (Try (Repeat (Rewrite ''real_one_collect_assoc''))) #>
1256 (Try (Repeat (Calculate ''PLUS''))) #>
1257 (Try (Repeat (Calculate ''TIMES''))) #>
1258 (Try (Repeat (Calculate ''POWER''))))
1262 Rule_Def.Repeat{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
1263 asm_rls = Atools_erls, prog_rls = Rule_Set.Empty,
1264 calc = [("PLUS" , (\<^const_name>\<open>plus\<close>, Calc_Binop.numeric "#add_")),
1265 ("TIMES" , (\<^const_name>\<open>times\<close>, Calc_Binop.numeric "#mult_")),
1266 ("POWER", (\<^const_name>\<open>realpow\<close>, Calc_Binop.numeric "#power_"))
1269 \<^rule_thm>\<open>real_plus_binom_pow2\<close>, (*"(a + b) \<up> 2 = a \<up> 2 + 2 * a * b + b \<up> 2"*)
1270 \<^rule_thm>\<open>real_plus_binom_times\<close>, (*"(a + b)*(a + b) = ...*)
1271 \<^rule_thm>\<open>real_minus_binom_pow2\<close>, (*"(a - b) \<up> 2 = a \<up> 2 - 2 * a * b + b \<up> 2"*)
1272 \<^rule_thm>\<open>real_minus_binom_times\<close>, (*"(a - b)*(a - b) = ...*)
1273 \<^rule_thm>\<open>real_plus_minus_binom1\<close>, (*"(a + b) * (a - b) = a \<up> 2 - b \<up> 2"*)
1274 \<^rule_thm>\<open>real_plus_minus_binom2\<close>, (*"(a - b) * (a + b) = a \<up> 2 - b \<up> 2"*)
1276 \<^rule_thm>\<open>real_pp_binom_times\<close>, (*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
1277 \<^rule_thm>\<open>real_pm_binom_times\<close>, (*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
1278 \<^rule_thm>\<open>real_mp_binom_times\<close>, (*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
1279 \<^rule_thm>\<open>real_mm_binom_times\<close>, (*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
1280 \<^rule_thm>\<open>realpow_multI\<close>, (*(a*b) \<up> n = a \<up> n * b \<up> n*)
1281 \<^rule_thm>\<open>real_plus_binom_pow3\<close>, (* (a + b) \<up> 3 = a \<up> 3 + 3*a \<up> 2*b + 3*a*b \<up> 2 + b \<up> 3 *)
1282 \<^rule_thm>\<open>real_minus_binom_pow3\<close>, (* (a - b) \<up> 3 = a \<up> 3 - 3*a \<up> 2*b + 3*a*b \<up> 2 - b \<up> 3 *)
1284 \<^rule_thm>\<open>distrib_right\<close>, (*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
1285 \<^rule_thm>\<open>distrib_left\<close>, (*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
1286 \<^rule_thm>\<open>left_diff_distrib\<close>, (*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
1287 \<^rule_thm>\<open>right_diff_distrib\<close>, (*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
1289 \<^rule_thm>\<open>mult_1_left\<close>, (*"1 * z = z"*)
1290 \<^rule_thm>\<open>mult_zero_left\<close>, (*"0 * z = 0"*)
1291 \<^rule_thm>\<open>add_0_left\<close>, (*"0 + z = z"*)
1293 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1294 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1295 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_"),
1296 (*\<^rule_thm>\<open>mult.commute\<close>,
1298 \<^rule_thm>\<open>real_mult_left_commute\<close>,
1299 \<^rule_thm>\<open>mult.assoc\<close>,
1300 \<^rule_thm>\<open>add.commute\<close>,
1301 \<^rule_thm>\<open>add.left_commute\<close>,
1302 \<^rule_thm>\<open>add.assoc\<close>,
1304 \<^rule_thm_sym>\<open>realpow_twoI\<close>, (*"r1 * r1 = r1 \<up> 2"*)
1305 \<^rule_thm>\<open>realpow_plus_1\<close>, (*"r * r \<up> n = r \<up> (n + 1)"*)
1307 \<^rule_thm_sym>\<open>real_mult_2\<close>, (*"z1 + z1 = 2 * z1"*)*)
1308 \<^rule_thm>\<open>real_mult_2_assoc\<close>, (*"z1 + (z1 + k) = 2 * z1 + k"*)
1310 \<^rule_thm>\<open>real_num_collect\<close>, (*"[| l is_num; m is_num |] ==>l * n + m * n = (l + m) * n"*)
1311 \<^rule_thm>\<open>real_num_collect_assoc\<close>, (*"[| l is_num; m is_num |] ==> l * n + (m * n + k) = (l + m) * n + k"*)
1312 \<^rule_thm>\<open>real_one_collect\<close>, (*"m is_num ==> n + m * n = (1 + m) * n"*)
1313 \<^rule_thm>\<open>real_one_collect_assoc\<close>, (*"m is_num ==> k + (n + m * n) = k + (1 + m) * n"*)
1315 \<^rule_eval>\<open>plus\<close> (Calc_Binop.numeric "#add_"),
1316 \<^rule_eval>\<open>times\<close> (Calc_Binop.numeric "#mult_"),
1317 \<^rule_eval>\<open>realpow\<close> (Calc_Binop.numeric "#power_")],
1318 program = Rule.Prog (Program.prep_program @{thm expand_binoms_2.simps})};
1321 subsection \<open>add to Know_Store\<close>
1322 subsubsection \<open>rule-sets\<close>
1323 ML \<open>val prep_rls' = Auto_Prog.prep_rls @{theory}\<close>
1326 norm_Poly = \<open>prep_rls' norm_Poly\<close> and
1327 Poly_erls = \<open>prep_rls' Poly_erls\<close> and
1328 expand = \<open>prep_rls' expand\<close> and
1329 expand_poly = \<open>prep_rls' expand_poly\<close> and
1330 simplify_power = \<open>prep_rls' simplify_power\<close> and
1332 order_add_mult = \<open>prep_rls' order_add_mult\<close> and
1333 collect_numerals = \<open>prep_rls' collect_numerals\<close> and
1334 collect_numerals_= \<open>prep_rls' collect_numerals_\<close> and
1335 reduce_012 = \<open>prep_rls' reduce_012\<close> and
1336 discard_parentheses = \<open>prep_rls' discard_parentheses\<close> and
1338 make_polynomial = \<open>prep_rls' make_polynomial\<close> and
1339 expand_binoms = \<open>prep_rls' expand_binoms\<close> and
1340 rev_rew_p = \<open>prep_rls' rev_rew_p\<close> and
1341 discard_minus = \<open>prep_rls' discard_minus\<close> and
1342 expand_poly_ = \<open>prep_rls' expand_poly_\<close> and
1344 expand_poly_rat_ = \<open>prep_rls' expand_poly_rat_\<close> and
1345 simplify_power_ = \<open>prep_rls' simplify_power_\<close> and
1346 calc_add_mult_pow_ = \<open>prep_rls' calc_add_mult_pow_\<close> and
1347 reduce_012_mult_ = \<open>prep_rls' reduce_012_mult_\<close> and
1348 reduce_012_ = \<open>prep_rls' reduce_012_\<close> and
1350 discard_parentheses1 = \<open>prep_rls' discard_parentheses1\<close> and
1351 order_mult_rls_ = \<open>prep_rls' order_mult_rls_\<close> and
1352 order_add_rls_ = \<open>prep_rls' order_add_rls_\<close> and
1353 make_rat_poly_with_parentheses = \<open>prep_rls' make_rat_poly_with_parentheses\<close>
1355 subsection \<open>problems\<close>
1357 problem pbl_simp_poly : "polynomial/simplification" =
1358 \<open>Rule_Set.append_rules "empty" Rule_Set.empty [(*for preds in where_*)
1359 \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")]\<close>
1360 Method_Ref: "simplification/for_polynomials"
1363 Where: "t_t is_polyexp"
1364 Find: "normalform n_n"
1366 subsection \<open>methods\<close>
1368 partial_function (tailrec) simplify :: "real \<Rightarrow> real"
1370 "simplify term = ((Rewrite_Set ''norm_Poly'') term)"
1372 method met_simp_poly : "simplification/for_polynomials" =
1373 \<open>{rew_ord="tless_true", rls' = Rule_Set.empty, calc = [], prog_rls = Rule_Set.empty,
1374 where_rls = Rule_Set.append_rules "simplification_for_polynomials_prls" Rule_Set.empty
1375 [(*for preds in where_*) \<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp"")],
1376 errpats = [], rew_rls = norm_Poly}\<close>
1377 Program: simplify.simps
1379 Where: "t_t is_polyexp"
1380 Find: "normalform n_n"