neuper@37906
|
1 |
(* WN.020812: theorems in the Reals,
|
neuper@37906
|
2 |
necessary for special rule sets, in addition to Isabelle2002.
|
neuper@37906
|
3 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@37906
|
4 |
!!! THIS IS THE _least_ NUMBER OF ADDITIONAL THEOREMS !!!
|
neuper@37906
|
5 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
|
neuper@37906
|
6 |
xxxI contain ^^^ instead of ^ in the respective theorem xxx in 2002
|
neuper@37906
|
7 |
changed by: Richard Lang 020912
|
neuper@37906
|
8 |
*)
|
neuper@37906
|
9 |
|
neuper@37950
|
10 |
theory Poly imports Simplify begin
|
neuper@37906
|
11 |
|
neuper@37906
|
12 |
consts
|
neuper@37906
|
13 |
|
neuper@37906
|
14 |
is'_expanded'_in :: "[real, real] => bool" ("_ is'_expanded'_in _")
|
neuper@37950
|
15 |
is'_poly'_in :: "[real, real] => bool" ("_ is'_poly'_in _") (*RL DA *)
|
neuper@37950
|
16 |
has'_degree'_in :: "[real, real] => real" ("_ has'_degree'_in _")(*RL DA *)
|
neuper@37950
|
17 |
is'_polyrat'_in :: "[real, real] => bool" ("_ is'_polyrat'_in _")(*RL030626*)
|
neuper@37906
|
18 |
|
neuper@37950
|
19 |
is'_multUnordered:: "real => bool" ("_ is'_multUnordered")
|
neuper@37950
|
20 |
is'_addUnordered :: "real => bool" ("_ is'_addUnordered") (*WN030618*)
|
neuper@37950
|
21 |
is'_polyexp :: "real => bool" ("_ is'_polyexp")
|
neuper@37906
|
22 |
|
neuper@37906
|
23 |
Expand'_binoms
|
neuper@37950
|
24 |
:: "['y,
|
neuper@37950
|
25 |
'y] => 'y"
|
wneuper@59334
|
26 |
("((Script Expand'_binoms (_ =))// (_))" 9)
|
neuper@37906
|
27 |
|
neuper@37906
|
28 |
(*-------------------- rules------------------------------------------------*)
|
neuper@52148
|
29 |
axiomatization where (*.not contained in Isabelle2002,
|
neuper@37906
|
30 |
stated as axioms, TODO: prove as theorems;
|
neuper@37906
|
31 |
theorem-IDs 'xxxI' with ^^^ instead of ^ in 'xxx' in Isabelle2002.*)
|
neuper@37906
|
32 |
|
neuper@52148
|
33 |
realpow_pow: "(a ^^^ b) ^^^ c = a ^^^ (b * c)" and
|
neuper@52148
|
34 |
realpow_addI: "r ^^^ (n + m) = r ^^^ n * r ^^^ m" and
|
neuper@52148
|
35 |
realpow_addI_assoc_l: "r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s" and
|
neuper@52148
|
36 |
realpow_addI_assoc_r: "s * r ^^^ n * r ^^^ m = s * r ^^^ (n + m)" and
|
neuper@37906
|
37 |
|
neuper@52148
|
38 |
realpow_oneI: "r ^^^ 1 = r" and
|
neuper@52148
|
39 |
realpow_zeroI: "r ^^^ 0 = 1" and
|
neuper@52148
|
40 |
realpow_eq_oneI: "1 ^^^ n = 1" and
|
neuper@52148
|
41 |
realpow_multI: "(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
|
neuper@37974
|
42 |
realpow_multI_poly: "[| r is_polyexp; s is_polyexp |] ==>
|
neuper@52148
|
43 |
(r * s) ^^^ n = r ^^^ n * s ^^^ n" and
|
wneuper@59189
|
44 |
realpow_minus_oneI: "(- 1) ^^^ (2 * n) = 1" and
|
neuper@37906
|
45 |
|
neuper@52148
|
46 |
realpow_twoI: "r ^^^ 2 = r * r" and
|
neuper@52148
|
47 |
realpow_twoI_assoc_l: "r * (r * s) = r ^^^ 2 * s" and
|
neuper@52148
|
48 |
realpow_twoI_assoc_r: "s * r * r = s * r ^^^ 2" and
|
neuper@52148
|
49 |
realpow_two_atom: "r is_atom ==> r * r = r ^^^ 2" and
|
neuper@52148
|
50 |
realpow_plus_1: "r * r ^^^ n = r ^^^ (n + 1)" and
|
neuper@52148
|
51 |
realpow_plus_1_assoc_l: "r * (r ^^^ m * s) = r ^^^ (1 + m) * s" and
|
neuper@52148
|
52 |
realpow_plus_1_assoc_l2: "r ^^^ m * (r * s) = r ^^^ (1 + m) * s" and
|
neuper@52148
|
53 |
realpow_plus_1_assoc_r: "s * r * r ^^^ m = s * r ^^^ (1 + m)" and
|
neuper@52148
|
54 |
realpow_plus_1_atom: "r is_atom ==> r * r ^^^ n = r ^^^ (1 + n)" and
|
neuper@37974
|
55 |
realpow_def_atom: "[| Not (r is_atom); 1 < n |]
|
neuper@52148
|
56 |
==> r ^^^ n = r * r ^^^ (n + -1)" and
|
neuper@52148
|
57 |
realpow_addI_atom: "r is_atom ==> r ^^^ n * r ^^^ m = r ^^^ (n + m)" and
|
neuper@37906
|
58 |
|
neuper@37906
|
59 |
|
neuper@52148
|
60 |
realpow_minus_even: "n is_even ==> (- r) ^^^ n = r ^^^ n" and
|
neuper@52148
|
61 |
realpow_minus_odd: "Not (n is_even) ==> (- r) ^^^ n = -1 * r ^^^ n" and
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
|
neuper@37906
|
64 |
(* RL 020914 *)
|
neuper@52148
|
65 |
real_pp_binom_times: "(a + b)*(c + d) = a*c + a*d + b*c + b*d" and
|
neuper@52148
|
66 |
real_pm_binom_times: "(a + b)*(c - d) = a*c - a*d + b*c - b*d" and
|
neuper@52148
|
67 |
real_mp_binom_times: "(a - b)*(c + d) = a*c + a*d - b*c - b*d" and
|
neuper@52148
|
68 |
real_mm_binom_times: "(a - b)*(c - d) = a*c - a*d - b*c + b*d" and
|
neuper@52148
|
69 |
real_plus_binom_pow3: "(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
|
neuper@37974
|
70 |
real_plus_binom_pow3_poly: "[| a is_polyexp; b is_polyexp |] ==>
|
neuper@52148
|
71 |
(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" and
|
neuper@52148
|
72 |
real_minus_binom_pow3: "(a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3" and
|
neuper@37974
|
73 |
real_minus_binom_pow3_p: "(a + -1 * b)^^^3 = a^^^3 + -3*a^^^2*b + 3*a*b^^^2 +
|
neuper@52148
|
74 |
-1*b^^^3" and
|
neuper@37974
|
75 |
(* real_plus_binom_pow: "[| n is_const; 3 < n |] ==>
|
neuper@37950
|
76 |
(a + b)^^^n = (a + b) * (a + b)^^^(n - 1)" *)
|
neuper@37974
|
77 |
real_plus_binom_pow4: "(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
|
neuper@52148
|
78 |
*(a + b)" and
|
neuper@37974
|
79 |
real_plus_binom_pow4_poly: "[| a is_polyexp; b is_polyexp |] ==>
|
neuper@37950
|
80 |
(a + b)^^^4 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
|
neuper@52148
|
81 |
*(a + b)" and
|
neuper@37974
|
82 |
real_plus_binom_pow5: "(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3)
|
neuper@52148
|
83 |
*(a^^^2 + 2*a*b + b^^^2)" and
|
neuper@37974
|
84 |
real_plus_binom_pow5_poly: "[| a is_polyexp; b is_polyexp |] ==>
|
neuper@37950
|
85 |
(a + b)^^^5 = (a^^^3 + 3*a^^^2*b + 3*a*b^^^2
|
neuper@52148
|
86 |
+ b^^^3)*(a^^^2 + 2*a*b + b^^^2)" and
|
neuper@52148
|
87 |
real_diff_plus: "a - b = a + -b" (*17.3.03: do_NOT_use*) and
|
neuper@52148
|
88 |
real_diff_minus: "a - b = a + -1 * b" and
|
neuper@52148
|
89 |
real_plus_binom_times: "(a + b)*(a + b) = a^^^2 + 2*a*b + b^^^2" and
|
neuper@52148
|
90 |
real_minus_binom_times: "(a - b)*(a - b) = a^^^2 - 2*a*b + b^^^2" and
|
neuper@37906
|
91 |
(*WN071229 changed for Schaerding -----vvv*)
|
neuper@37974
|
92 |
(*real_plus_binom_pow2: "(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
|
neuper@52148
|
93 |
real_plus_binom_pow2: "(a + b)^^^2 = (a + b) * (a + b)" and
|
neuper@37906
|
94 |
(*WN071229 changed for Schaerding -----^^^*)
|
neuper@37974
|
95 |
real_plus_binom_pow2_poly: "[| a is_polyexp; b is_polyexp |] ==>
|
neuper@52148
|
96 |
(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2" and
|
neuper@52148
|
97 |
real_minus_binom_pow2: "(a - b)^^^2 = a^^^2 - 2*a*b + b^^^2" and
|
neuper@52148
|
98 |
real_minus_binom_pow2_p: "(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2" and
|
neuper@52148
|
99 |
real_plus_minus_binom1: "(a + b)*(a - b) = a^^^2 - b^^^2" and
|
neuper@52148
|
100 |
real_plus_minus_binom1_p: "(a + b)*(a - b) = a^^^2 + -1*b^^^2" and
|
neuper@52148
|
101 |
real_plus_minus_binom1_p_p: "(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2" and
|
neuper@52148
|
102 |
real_plus_minus_binom2: "(a - b)*(a + b) = a^^^2 - b^^^2" and
|
neuper@52148
|
103 |
real_plus_minus_binom2_p: "(a - b)*(a + b) = a^^^2 + -1*b^^^2" and
|
neuper@52148
|
104 |
real_plus_minus_binom2_p_p: "(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2" and
|
neuper@52148
|
105 |
real_plus_binom_times1: "(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2" and
|
neuper@52148
|
106 |
real_plus_binom_times2: "(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2" and
|
neuper@37906
|
107 |
|
neuper@37974
|
108 |
real_num_collect: "[| l is_const; m is_const |] ==>
|
neuper@52148
|
109 |
l * n + m * n = (l + m) * n" and
|
neuper@37906
|
110 |
(* FIXME.MG.0401: replace 'real_num_collect_assoc'
|
neuper@37906
|
111 |
by 'real_num_collect_assoc_l' ... are equal, introduced by MG ! *)
|
neuper@37974
|
112 |
real_num_collect_assoc: "[| l is_const; m is_const |] ==>
|
neuper@52148
|
113 |
l * n + (m * n + k) = (l + m) * n + k" and
|
neuper@37974
|
114 |
real_num_collect_assoc_l: "[| l is_const; m is_const |] ==>
|
neuper@37950
|
115 |
l * n + (m * n + k) = (l + m)
|
neuper@52148
|
116 |
* n + k" and
|
neuper@37974
|
117 |
real_num_collect_assoc_r: "[| l is_const; m is_const |] ==>
|
neuper@52148
|
118 |
(k + m * n) + l * n = k + (l + m) * n" and
|
neuper@52148
|
119 |
real_one_collect: "m is_const ==> n + m * n = (1 + m) * n" and
|
neuper@37906
|
120 |
(* FIXME.MG.0401: replace 'real_one_collect_assoc'
|
neuper@37906
|
121 |
by 'real_one_collect_assoc_l' ... are equal, introduced by MG ! *)
|
neuper@52148
|
122 |
real_one_collect_assoc: "m is_const ==> n + (m * n + k) = (1 + m)* n + k" and
|
neuper@37906
|
123 |
|
neuper@52148
|
124 |
real_one_collect_assoc_l: "m is_const ==> n + (m * n + k) = (1 + m) * n + k" and
|
neuper@52148
|
125 |
real_one_collect_assoc_r: "m is_const ==> (k + n) + m * n = k + (1 + m) * n" and
|
neuper@37906
|
126 |
|
neuper@37906
|
127 |
(* FIXME.MG.0401: replace 'real_mult_2_assoc'
|
neuper@37906
|
128 |
by 'real_mult_2_assoc_l' ... are equal, introduced by MG ! *)
|
neuper@52148
|
129 |
real_mult_2_assoc: "z1 + (z1 + k) = 2 * z1 + k" and
|
neuper@52148
|
130 |
real_mult_2_assoc_l: "z1 + (z1 + k) = 2 * z1 + k" and
|
neuper@52148
|
131 |
real_mult_2_assoc_r: "(k + z1) + z1 = k + 2 * z1" and
|
neuper@37906
|
132 |
|
neuper@52148
|
133 |
real_add_mult_distrib_poly: "w is_polyexp ==> (z1 + z2) * w = z1 * w + z2 * w" and
|
neuper@37974
|
134 |
real_add_mult_distrib2_poly:"w is_polyexp ==> w * (z1 + z2) = w * z1 + w * z2"
|
neuper@37950
|
135 |
|
neuper@37950
|
136 |
text {* remark on 'polynomials'
|
neuper@37950
|
137 |
WN020919
|
neuper@37950
|
138 |
*** there are 5 kinds of expanded normalforms ***
|
neuper@37950
|
139 |
|
neuper@37950
|
140 |
[1] 'complete polynomial' (Komplettes Polynom), univariate
|
neuper@37950
|
141 |
a_0 + a_1.x^1 +...+ a_n.x^n not (a_n = 0)
|
neuper@37950
|
142 |
not (a_n = 0), some a_i may be zero (DON'T disappear),
|
neuper@37950
|
143 |
variables in monomials lexicographically ordered and complete,
|
neuper@37950
|
144 |
x written as 1*x^1, ...
|
neuper@37950
|
145 |
[2] 'polynomial' (Polynom), univariate and multivariate
|
neuper@37950
|
146 |
a_0 + a_1.x +...+ a_n.x^n not (a_n = 0)
|
neuper@37950
|
147 |
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
|
neuper@37950
|
148 |
not (a_n = 0), some a_i may be zero (ie. monomials disappear),
|
neuper@37950
|
149 |
exponents and coefficients equal 1 are not (WN060904.TODO in cancel_p_)shown,
|
neuper@37950
|
150 |
and variables in monomials are lexicographically ordered
|
neuper@37950
|
151 |
examples: [1]: "1 + (-10) * x ^^^ 1 + 25 * x ^^^ 2"
|
neuper@37950
|
152 |
[1]: "11 + 0 * x ^^^ 1 + 1 * x ^^^ 2"
|
neuper@37950
|
153 |
[2]: "x + (-50) * x ^^^ 3"
|
neuper@37950
|
154 |
[2]: "(-1) * x * y ^^^ 2 + 7 * x ^^^ 3"
|
neuper@37950
|
155 |
|
neuper@37950
|
156 |
[3] 'expanded_term' (Ausmultiplizierter Term):
|
neuper@37950
|
157 |
pull out unary minus to binary minus,
|
neuper@37950
|
158 |
as frequently exercised in schools; other conditions for [2] hold however
|
neuper@37950
|
159 |
examples: "a ^^^ 2 - 2 * a * b + b ^^^ 2"
|
neuper@37950
|
160 |
"4 * x ^^^ 2 - 9 * y ^^^ 2"
|
neuper@37950
|
161 |
[4] 'polynomial_in' (Polynom in):
|
neuper@37950
|
162 |
polynomial in 1 variable with arbitrary coefficients
|
neuper@37950
|
163 |
examples: "2 * x + (-50) * x ^^^ 3" (poly in x)
|
neuper@37950
|
164 |
"(u + v) + (2 * u ^^^ 2) * a + (-u) * a ^^^ 2 (poly in a)
|
neuper@37950
|
165 |
[5] 'expanded_in' (Ausmultiplizierter Termin in):
|
neuper@37950
|
166 |
analoguous to [3] with binary minus like [3]
|
neuper@37950
|
167 |
examples: "2 * x - 50 * x ^^^ 3" (expanded in x)
|
neuper@37950
|
168 |
"(u + v) + (2 * u ^^^ 2) * a - u * a ^^^ 2 (expanded in a)
|
neuper@37950
|
169 |
*}
|
neuper@37950
|
170 |
|
neuper@37950
|
171 |
ML {*
|
neuper@37972
|
172 |
val thy = @{theory};
|
neuper@37972
|
173 |
|
neuper@37950
|
174 |
(* is_polyrat_in becomes true, if no bdv is in the denominator of a fraction*)
|
neuper@37950
|
175 |
fun is_polyrat_in t v =
|
wneuper@59389
|
176 |
let fun coeff_in c v = member op = (TermC.vars c) v;
|
neuper@38031
|
177 |
fun finddivide (_ $ _ $ _ $ _) v = error("is_polyrat_in:")
|
neuper@37950
|
178 |
(* at the moment there is no term like this, but ....*)
|
wneuper@59360
|
179 |
| finddivide (t as (Const ("Rings.divide_class.divide",_) $ _ $ b)) v =
|
neuper@37950
|
180 |
not(coeff_in b v)
|
neuper@37950
|
181 |
| finddivide (_ $ t1 $ t2) v =
|
neuper@37950
|
182 |
(finddivide t1 v) orelse (finddivide t2 v)
|
neuper@37950
|
183 |
| finddivide (_ $ t1) v = (finddivide t1 v)
|
neuper@37950
|
184 |
| finddivide _ _ = false;
|
neuper@37950
|
185 |
in finddivide t v end;
|
neuper@37950
|
186 |
|
neuper@37950
|
187 |
fun eval_is_polyrat_in _ _(p as (Const ("Poly.is'_polyrat'_in",_) $ t $ v)) _ =
|
neuper@37950
|
188 |
if is_polyrat_in t v
|
wneuper@59416
|
189 |
then SOME ((Rule.term2str p) ^ " = True",
|
wneuper@59390
|
190 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
wneuper@59416
|
191 |
else SOME ((Rule.term2str p) ^ " = True",
|
wneuper@59390
|
192 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@38015
|
193 |
| eval_is_polyrat_in _ _ _ _ = ((*tracing"### no matches";*) NONE);
|
neuper@37950
|
194 |
|
neuper@37950
|
195 |
local
|
neuper@37950
|
196 |
(*.a 'c is coefficient of v' if v does NOT occur in c.*)
|
wneuper@59389
|
197 |
fun coeff_in c v = not (member op = (TermC.vars c) v);
|
neuper@37950
|
198 |
(* FIXME.WN100826 shift this into test--------------
|
wneuper@59186
|
199 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
wneuper@59186
|
200 |
val t = (Thm.term_of o the o (parse thy)) "1";
|
neuper@37950
|
201 |
coeff_in t v;
|
neuper@37950
|
202 |
(*val it = true : bool*)
|
wneuper@59186
|
203 |
val t = (Thm.term_of o the o (parse thy)) "a*b+c";
|
neuper@37950
|
204 |
coeff_in t v;
|
neuper@37950
|
205 |
(*val it = true : bool*)
|
wneuper@59186
|
206 |
val t = (Thm.term_of o the o (parse thy)) "a*x+c";
|
neuper@37950
|
207 |
coeff_in t v;
|
neuper@37950
|
208 |
(*val it = false : bool*)
|
neuper@37950
|
209 |
----------------------------------------------------*)
|
neuper@37950
|
210 |
(*. a 'monomial t in variable v' is a term t with
|
neuper@37950
|
211 |
either (1) v NOT existent in t, or (2) v contained in t,
|
neuper@37950
|
212 |
if (1) then degree 0
|
neuper@37950
|
213 |
if (2) then v is a factor on the very right, ev. with exponent.*)
|
neuper@37950
|
214 |
fun factor_right_deg (*case 2*)
|
neuper@38034
|
215 |
(t as Const ("Groups.times_class.times",_) $ t1 $
|
neuper@37950
|
216 |
(Const ("Atools.pow",_) $ vv $ Free (d,_))) v =
|
wneuper@59390
|
217 |
if ((vv = v) andalso (coeff_in t1 v)) then SOME (TermC.int_of_str d) else NONE
|
neuper@37950
|
218 |
| factor_right_deg (t as Const ("Atools.pow",_) $ vv $ Free (d,_)) v =
|
wneuper@59390
|
219 |
if (vv = v) then SOME (TermC.int_of_str d) else NONE
|
neuper@38034
|
220 |
| factor_right_deg (t as Const ("Groups.times_class.times",_) $ t1 $ vv) v =
|
neuper@37950
|
221 |
if ((vv = v) andalso (coeff_in t1 v))then SOME 1 else NONE
|
neuper@37950
|
222 |
| factor_right_deg vv v =
|
neuper@37950
|
223 |
if (vv = v) then SOME 1 else NONE;
|
neuper@37950
|
224 |
fun mono_deg_in m v =
|
neuper@37950
|
225 |
if coeff_in m v then (*case 1*) SOME 0
|
neuper@37950
|
226 |
else factor_right_deg m v;
|
neuper@37950
|
227 |
(* FIXME.WN100826 shift this into test-----------------------------
|
wneuper@59186
|
228 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
wneuper@59186
|
229 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x^^^7";
|
neuper@37950
|
230 |
mono_deg_in t v;
|
neuper@37950
|
231 |
(*val it = SOME 7*)
|
wneuper@59186
|
232 |
val t = (Thm.term_of o the o (parse thy)) "x^^^7";
|
neuper@37950
|
233 |
mono_deg_in t v;
|
neuper@37950
|
234 |
(*val it = SOME 7*)
|
wneuper@59186
|
235 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)*x";
|
neuper@37950
|
236 |
mono_deg_in t v;
|
neuper@37950
|
237 |
(*val it = SOME 1*)
|
wneuper@59186
|
238 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+x)*x";
|
neuper@37950
|
239 |
mono_deg_in t v;
|
neuper@37950
|
240 |
(*val it = NONE*)
|
wneuper@59186
|
241 |
val t = (Thm.term_of o the o (parse thy)) "x";
|
neuper@37950
|
242 |
mono_deg_in t v;
|
neuper@37950
|
243 |
(*val it = SOME 1*)
|
wneuper@59186
|
244 |
val t = (Thm.term_of o the o (parse thy)) "(a*b+c)";
|
neuper@37950
|
245 |
mono_deg_in t v;
|
neuper@37950
|
246 |
(*val it = SOME 0*)
|
wneuper@59186
|
247 |
val t = (Thm.term_of o the o (parse thy)) "ab - (a*b)*x";
|
neuper@37950
|
248 |
mono_deg_in t v;
|
neuper@37950
|
249 |
(*val it = NONE*)
|
neuper@37950
|
250 |
------------------------------------------------------------------*)
|
neuper@37950
|
251 |
fun expand_deg_in t v =
|
neuper@38014
|
252 |
let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
|
neuper@37950
|
253 |
(case mono_deg_in t2 v of (* $ is left associative*)
|
neuper@37950
|
254 |
SOME d' => edi d' d' t1
|
neuper@37950
|
255 |
| NONE => NONE)
|
neuper@38014
|
256 |
| edi ~1 ~1 (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
|
neuper@37950
|
257 |
(case mono_deg_in t2 v of
|
neuper@37950
|
258 |
SOME d' => edi d' d' t1
|
neuper@37950
|
259 |
| NONE => NONE)
|
neuper@38014
|
260 |
| edi d dmax (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
|
neuper@37950
|
261 |
(case mono_deg_in t2 v of
|
neuper@37950
|
262 |
(*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
|
neuper@37950
|
263 |
SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
|
neuper@37950
|
264 |
then edi d' dmax t1 else NONE
|
neuper@37950
|
265 |
| NONE => NONE)
|
neuper@38014
|
266 |
| edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
|
neuper@37950
|
267 |
(case mono_deg_in t2 v of
|
neuper@37950
|
268 |
(*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
|
neuper@37950
|
269 |
SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
|
neuper@37950
|
270 |
then edi d' dmax t1 else NONE
|
neuper@37950
|
271 |
| NONE => NONE)
|
neuper@37950
|
272 |
| edi ~1 ~1 t = (case mono_deg_in t v of
|
neuper@37950
|
273 |
d as SOME _ => d
|
neuper@37950
|
274 |
| NONE => NONE)
|
neuper@37950
|
275 |
| edi d dmax t = (*basecase last*)
|
neuper@37950
|
276 |
(case mono_deg_in t v of
|
neuper@37950
|
277 |
SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
|
neuper@37950
|
278 |
then SOME dmax else NONE
|
neuper@37950
|
279 |
| NONE => NONE)
|
neuper@37950
|
280 |
in edi ~1 ~1 t end;
|
neuper@37950
|
281 |
(* FIXME.WN100826 shift this into test-----------------------------
|
wneuper@59186
|
282 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
wneuper@59186
|
283 |
val t = (Thm.term_of o the o (parse thy)) "a+b";
|
neuper@37950
|
284 |
expand_deg_in t v;
|
neuper@37950
|
285 |
(*val it = SOME 0*)
|
wneuper@59186
|
286 |
val t = (Thm.term_of o the o (parse thy)) "(a+b)*x";
|
neuper@37950
|
287 |
expand_deg_in t v;
|
neuper@37950
|
288 |
(*SOME 1*)
|
wneuper@59186
|
289 |
val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x";
|
neuper@37950
|
290 |
expand_deg_in t v;
|
neuper@37950
|
291 |
(*SOME 1*)
|
wneuper@59186
|
292 |
val t = (Thm.term_of o the o (parse thy)) "a*b + (a-b)*x";
|
neuper@37950
|
293 |
expand_deg_in t v;
|
neuper@37950
|
294 |
(*SOME 1*)
|
wneuper@59186
|
295 |
val t = (Thm.term_of o the o (parse thy)) "a*b + (a+b)*x + x^^^2";
|
neuper@37950
|
296 |
expand_deg_in t v;
|
neuper@37950
|
297 |
-------------------------------------------------------------------*)
|
neuper@37950
|
298 |
fun poly_deg_in t v =
|
neuper@38014
|
299 |
let fun edi ~1 ~1 (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
|
neuper@37950
|
300 |
(case mono_deg_in t2 v of (* $ is left associative*)
|
neuper@37950
|
301 |
SOME d' => edi d' d' t1
|
neuper@37950
|
302 |
| NONE => NONE)
|
neuper@38014
|
303 |
| edi d dmax (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
|
neuper@37950
|
304 |
(case mono_deg_in t2 v of
|
neuper@37950
|
305 |
(*RL orelse ((d=0) andalso (d'=0)) need to handle 3+4-...4 +x*)
|
neuper@37950
|
306 |
SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
|
neuper@37950
|
307 |
then edi d' dmax t1 else NONE
|
neuper@37950
|
308 |
| NONE => NONE)
|
neuper@37950
|
309 |
| edi ~1 ~1 t = (case mono_deg_in t v of
|
neuper@37950
|
310 |
d as SOME _ => d
|
neuper@37950
|
311 |
| NONE => NONE)
|
neuper@37950
|
312 |
| edi d dmax t = (*basecase last*)
|
neuper@37950
|
313 |
(case mono_deg_in t v of
|
neuper@37950
|
314 |
SOME d' => if ((d > d') orelse ((d=0) andalso (d'=0)))
|
neuper@37950
|
315 |
then SOME dmax else NONE
|
neuper@37950
|
316 |
| NONE => NONE)
|
neuper@37950
|
317 |
in edi ~1 ~1 t end;
|
neuper@37950
|
318 |
in
|
neuper@37950
|
319 |
|
neuper@37950
|
320 |
fun is_expanded_in t v =
|
neuper@37950
|
321 |
case expand_deg_in t v of SOME _ => true | NONE => false;
|
neuper@37950
|
322 |
fun is_poly_in t v =
|
neuper@37950
|
323 |
case poly_deg_in t v of SOME _ => true | NONE => false;
|
neuper@37950
|
324 |
fun has_degree_in t v =
|
neuper@37950
|
325 |
case expand_deg_in t v of SOME d => d | NONE => ~1;
|
neuper@37980
|
326 |
end;(*local*)
|
neuper@37950
|
327 |
(* FIXME.WN100826 shift this into test-----------------------------
|
wneuper@59186
|
328 |
val v = (Thm.term_of o the o (parse thy)) "x";
|
wneuper@59186
|
329 |
val t = (Thm.term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2";
|
neuper@37950
|
330 |
has_degree_in t v;
|
neuper@37950
|
331 |
(*val it = 2*)
|
wneuper@59186
|
332 |
val t = (Thm.term_of o the o (parse thy)) "-8 - 2*x + x^^^2";
|
neuper@37950
|
333 |
has_degree_in t v;
|
neuper@37950
|
334 |
(*val it = 2*)
|
wneuper@59186
|
335 |
val t = (Thm.term_of o the o (parse thy)) "6 + 13*x + 6*x^^^2";
|
neuper@37950
|
336 |
has_degree_in t v;
|
neuper@37950
|
337 |
(*val it = 2*)
|
neuper@37950
|
338 |
-------------------------------------------------------------------*)
|
neuper@37950
|
339 |
|
neuper@37950
|
340 |
(*("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in ""))*)
|
neuper@37950
|
341 |
fun eval_is_expanded_in _ _
|
neuper@37950
|
342 |
(p as (Const ("Poly.is'_expanded'_in",_) $ t $ v)) _ =
|
neuper@37950
|
343 |
if is_expanded_in t v
|
wneuper@59416
|
344 |
then SOME ((Rule.term2str p) ^ " = True",
|
wneuper@59390
|
345 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
wneuper@59416
|
346 |
else SOME ((Rule.term2str p) ^ " = True",
|
wneuper@59390
|
347 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@37950
|
348 |
| eval_is_expanded_in _ _ _ _ = NONE;
|
neuper@37950
|
349 |
(*
|
wneuper@59186
|
350 |
val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
|
neuper@37950
|
351 |
val SOME (id, t') = eval_is_expanded_in 0 0 t 0;
|
neuper@37950
|
352 |
(*val id = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
|
wneuper@59416
|
353 |
Rule.term2str t';
|
neuper@37950
|
354 |
(*val it = "Poly.is'_expanded'_in (-8 - 2 * x + x ^^^ 2) x = True"*)
|
neuper@37950
|
355 |
*)
|
neuper@37950
|
356 |
|
neuper@37950
|
357 |
(*("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in ""))*)
|
neuper@37950
|
358 |
fun eval_is_poly_in _ _
|
neuper@37950
|
359 |
(p as (Const ("Poly.is'_poly'_in",_) $ t $ v)) _ =
|
neuper@37950
|
360 |
if is_poly_in t v
|
wneuper@59416
|
361 |
then SOME ((Rule.term2str p) ^ " = True",
|
wneuper@59390
|
362 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
|
wneuper@59416
|
363 |
else SOME ((Rule.term2str p) ^ " = True",
|
wneuper@59390
|
364 |
HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
|
neuper@37950
|
365 |
| eval_is_poly_in _ _ _ _ = NONE;
|
neuper@37950
|
366 |
(*
|
wneuper@59186
|
367 |
val t = (Thm.term_of o the o (parse thy)) "(8 + 2*x + x^^^2) is_poly_in x";
|
neuper@37950
|
368 |
val SOME (id, t') = eval_is_poly_in 0 0 t 0;
|
neuper@37950
|
369 |
(*val id = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
|
wneuper@59416
|
370 |
Rule.term2str t';
|
neuper@37950
|
371 |
(*val it = "Poly.is'_poly'_in (8 + 2 * x + x ^^^ 2) x = True"*)
|
neuper@37950
|
372 |
*)
|
neuper@37950
|
373 |
|
neuper@37950
|
374 |
(*("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in ""))*)
|
neuper@37950
|
375 |
fun eval_has_degree_in _ _
|
neuper@37950
|
376 |
(p as (Const ("Poly.has'_degree'_in",_) $ t $ v)) _ =
|
neuper@37950
|
377 |
let val d = has_degree_in t v
|
wneuper@59389
|
378 |
val d' = TermC.term_of_num HOLogic.realT d
|
wneuper@59416
|
379 |
in SOME ((Rule.term2str p) ^ " = " ^ (string_of_int d),
|
wneuper@59390
|
380 |
HOLogic.Trueprop $ (TermC.mk_equality (p, d')))
|
neuper@37950
|
381 |
end
|
neuper@37950
|
382 |
| eval_has_degree_in _ _ _ _ = NONE;
|
neuper@37950
|
383 |
(*
|
wneuper@59186
|
384 |
> val t = (Thm.term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) has_degree_in x";
|
neuper@37950
|
385 |
> val SOME (id, t') = eval_has_degree_in 0 0 t 0;
|
neuper@37950
|
386 |
val id = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
|
wneuper@59416
|
387 |
> Rule.term2str t';
|
neuper@37950
|
388 |
val it = "Poly.has'_degree'_in (-8 - 2 * x + x ^^^ 2) x = 2" : string
|
neuper@37950
|
389 |
*)
|
neuper@37950
|
390 |
|
neuper@37978
|
391 |
(*..*)
|
neuper@37978
|
392 |
val calculate_Poly =
|
wneuper@59416
|
393 |
Rule.append_rls "calculate_PolyFIXXXME.not.impl." Rule.e_rls
|
neuper@37978
|
394 |
[];
|
neuper@37978
|
395 |
|
neuper@37950
|
396 |
(*.for evaluation of conditions in rewrite rules.*)
|
wneuper@59416
|
397 |
val Poly_erls = Rule.append_rls "Poly_erls" Atools_erls
|
wneuper@59416
|
398 |
[Rule.Calc ("HOL.eq", eval_equal "#equal_"),
|
wneuper@59416
|
399 |
Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
|
wneuper@59416
|
400 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
401 |
Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
|
wneuper@59416
|
402 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
403 |
Rule.Calc ("Atools.pow", eval_binop "#power_")];
|
neuper@37950
|
404 |
|
wneuper@59416
|
405 |
val poly_crls = Rule.append_rls "poly_crls" Atools_crls
|
wneuper@59416
|
406 |
[Rule.Calc ("HOL.eq", eval_equal "#equal_"),
|
wneuper@59416
|
407 |
Rule.Thm ("real_unari_minus", TermC.num_str @{thm real_unari_minus}),
|
wneuper@59416
|
408 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
409 |
Rule.Calc ("Groups.minus_class.minus", eval_binop "#sub_"),
|
wneuper@59416
|
410 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
411 |
Rule.Calc ("Atools.pow" ,eval_binop "#power_")];
|
neuper@37950
|
412 |
|
neuper@37950
|
413 |
local (*. for make_polynomial .*)
|
neuper@37950
|
414 |
|
neuper@37950
|
415 |
open Term; (* for type order = EQUAL | LESS | GREATER *)
|
neuper@37950
|
416 |
|
neuper@37950
|
417 |
fun pr_ord EQUAL = "EQUAL"
|
neuper@37950
|
418 |
| pr_ord LESS = "LESS"
|
neuper@37950
|
419 |
| pr_ord GREATER = "GREATER";
|
neuper@37950
|
420 |
|
neuper@37950
|
421 |
fun dest_hd' (Const (a, T)) = (* ~ term.ML *)
|
neuper@37950
|
422 |
(case a of
|
neuper@37950
|
423 |
"Atools.pow" => ((("|||||||||||||", 0), T), 0) (*WN greatest string*)
|
neuper@37950
|
424 |
| _ => (((a, 0), T), 0))
|
neuper@37950
|
425 |
| dest_hd' (Free (a, T)) = (((a, 0), T), 1)
|
neuper@37950
|
426 |
| dest_hd' (Var v) = (v, 2)
|
neuper@37950
|
427 |
| dest_hd' (Bound i) = ((("", i), dummyT), 3)
|
neuper@37950
|
428 |
| dest_hd' (Abs (_, T, _)) = ((("", 0), T), 4);
|
neuper@37950
|
429 |
|
neuper@37950
|
430 |
fun get_order_pow (t $ (Free(order,_))) = (* RL FIXXXME:geht zufaellig?WN*)
|
wneuper@59390
|
431 |
(case TermC.int_of_str_opt (order) of
|
neuper@37950
|
432 |
SOME d => d
|
neuper@37950
|
433 |
| NONE => 0)
|
neuper@37950
|
434 |
| get_order_pow _ = 0;
|
neuper@37950
|
435 |
|
neuper@37950
|
436 |
fun size_of_term' (Const(str,_) $ t) =
|
neuper@37950
|
437 |
if "Atools.pow"= str then 1000 + size_of_term' t else 1+size_of_term' t(*WN*)
|
neuper@37950
|
438 |
| size_of_term' (Abs (_,_,body)) = 1 + size_of_term' body
|
neuper@37950
|
439 |
| size_of_term' (f$t) = size_of_term' f + size_of_term' t
|
neuper@37950
|
440 |
| size_of_term' _ = 1;
|
neuper@37950
|
441 |
|
neuper@37950
|
442 |
fun term_ord' pr thy (Abs (_, T, t), Abs(_, U, u)) = (* ~ term.ML *)
|
neuper@52070
|
443 |
(case term_ord' pr thy (t, u) of EQUAL => Term_Ord.typ_ord (T, U) | ord => ord)
|
neuper@37950
|
444 |
| term_ord' pr thy (t, u) =
|
neuper@52070
|
445 |
(if pr then
|
neuper@52070
|
446 |
let
|
neuper@52070
|
447 |
val (f, ts) = strip_comb t and (g, us) = strip_comb u;
|
wneuper@59416
|
448 |
val _ = tracing ("t= f@ts= \"" ^ Rule.term_to_string''' thy f ^ "\" @ \"[" ^
|
wneuper@59416
|
449 |
commas (map (Rule.term_to_string''' thy) ts) ^ "]\"");
|
wneuper@59416
|
450 |
val _ = tracing("u= g@us= \"" ^ Rule.term_to_string''' thy g ^ "\" @ \"[" ^
|
wneuper@59416
|
451 |
commas (map (Rule.term_to_string''' thy) us) ^ "]\"");
|
neuper@52070
|
452 |
val _ = tracing ("size_of_term(t,u)= (" ^ string_of_int (size_of_term' t) ^ ", " ^
|
neuper@52070
|
453 |
string_of_int (size_of_term' u) ^ ")");
|
neuper@52070
|
454 |
val _ = tracing ("hd_ord(f,g) = " ^ (pr_ord o hd_ord) (f,g));
|
neuper@52070
|
455 |
val _ = tracing ("terms_ord(ts,us) = " ^ (pr_ord o terms_ord str false) (ts, us));
|
neuper@52070
|
456 |
val _ = tracing ("-------");
|
neuper@52070
|
457 |
in () end
|
neuper@37950
|
458 |
else ();
|
neuper@37950
|
459 |
case int_ord (size_of_term' t, size_of_term' u) of
|
neuper@37950
|
460 |
EQUAL =>
|
neuper@37950
|
461 |
let val (f, ts) = strip_comb t and (g, us) = strip_comb u in
|
neuper@37950
|
462 |
(case hd_ord (f, g) of EQUAL => (terms_ord str pr) (ts, us)
|
neuper@37950
|
463 |
| ord => ord)
|
neuper@37950
|
464 |
end
|
neuper@37950
|
465 |
| ord => ord)
|
neuper@37950
|
466 |
and hd_ord (f, g) = (* ~ term.ML *)
|
neuper@37974
|
467 |
prod_ord (prod_ord Term_Ord.indexname_ord Term_Ord.typ_ord) int_ord (dest_hd' f, dest_hd' g)
|
neuper@37950
|
468 |
and terms_ord str pr (ts, us) =
|
wneuper@59406
|
469 |
list_ord (term_ord' pr (Celem.assoc_thy "Isac"))(ts, us);
|
neuper@52070
|
470 |
|
neuper@37950
|
471 |
in
|
neuper@37950
|
472 |
|
wneuper@59416
|
473 |
fun ord_make_polynomial (pr:bool) thy (_: Rule.subst) tu =
|
neuper@37950
|
474 |
(term_ord' pr thy(***) tu = LESS );
|
neuper@37950
|
475 |
|
neuper@37950
|
476 |
end;(*local*)
|
neuper@37950
|
477 |
|
neuper@37950
|
478 |
|
wneuper@59416
|
479 |
Rule.rew_ord' := overwritel (! Rule.rew_ord',
|
neuper@37950
|
480 |
[("termlessI", termlessI),
|
neuper@37950
|
481 |
("ord_make_polynomial", ord_make_polynomial false thy)
|
neuper@37950
|
482 |
]);
|
neuper@37950
|
483 |
|
neuper@37950
|
484 |
|
neuper@37950
|
485 |
val expand =
|
wneuper@59416
|
486 |
Rule.Rls {id = "expand", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
487 |
erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
|
wneuper@59416
|
488 |
rules = [Rule.Thm ("distrib_right" , TermC.num_str @{thm distrib_right}),
|
neuper@37950
|
489 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
wneuper@59416
|
490 |
Rule.Thm ("distrib_left", TermC.num_str @{thm distrib_left})
|
neuper@37950
|
491 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
wneuper@59416
|
492 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
493 |
|
neuper@37950
|
494 |
(*----------------- Begin: rulesets for make_polynomial_ -----------------
|
neuper@37950
|
495 |
'rlsIDs' redefined by MG as 'rlsIDs_'
|
neuper@37950
|
496 |
^^^*)
|
neuper@37950
|
497 |
|
neuper@37980
|
498 |
val discard_minus =
|
wneuper@59416
|
499 |
Rule.Rls {id = "discard_minus", preconds = [], rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
500 |
erls = Rule.e_rls, srls = Rule.Erls, calc = [], errpatts = [],
|
neuper@42407
|
501 |
rules =
|
wneuper@59416
|
502 |
[Rule.Thm ("real_diff_minus", TermC.num_str @{thm real_diff_minus}),
|
neuper@42407
|
503 |
(*"a - b = a + -1 * b"*)
|
wneuper@59416
|
504 |
Rule.Thm ("sym_real_mult_minus1", TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
|
neuper@42407
|
505 |
(*- ?z = "-1 * ?z"*)],
|
wneuper@59416
|
506 |
scr = Rule.EmptyScr};
|
neuper@37980
|
507 |
|
neuper@37950
|
508 |
val expand_poly_ =
|
wneuper@59416
|
509 |
Rule.Rls{id = "expand_poly_", preconds = [],
|
wneuper@59416
|
510 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
511 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
512 |
calc = [], errpatts = [],
|
neuper@42407
|
513 |
rules =
|
wneuper@59416
|
514 |
[Rule.Thm ("real_plus_binom_pow4", TermC.num_str @{thm real_plus_binom_pow4}),
|
neuper@42407
|
515 |
(*"(a + b)^^^4 = ... "*)
|
wneuper@59416
|
516 |
Rule.Thm ("real_plus_binom_pow5",TermC.num_str @{thm real_plus_binom_pow5}),
|
neuper@42407
|
517 |
(*"(a + b)^^^5 = ... "*)
|
wneuper@59416
|
518 |
Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
|
neuper@42407
|
519 |
(*"(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
|
neuper@42407
|
520 |
(*WN071229 changed/removed for Schaerding -----vvv*)
|
wneuper@59416
|
521 |
(*Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),*)
|
neuper@42407
|
522 |
(*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
|
wneuper@59416
|
523 |
Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
|
neuper@42407
|
524 |
(*"(a + b)^^^2 = (a + b) * (a + b)"*)
|
wneuper@59416
|
525 |
(*Rule.Thm ("real_plus_minus_binom1_p_p", TermC.num_str @{thm real_plus_minus_binom1_p_p}),*)
|
neuper@42407
|
526 |
(*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
|
wneuper@59416
|
527 |
(*Rule.Thm ("real_plus_minus_binom2_p_p", TermC.num_str @{thm real_plus_minus_binom2_p_p}),*)
|
neuper@42407
|
528 |
(*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
|
neuper@42407
|
529 |
(*WN071229 changed/removed for Schaerding -----^^^*)
|
neuper@37950
|
530 |
|
wneuper@59416
|
531 |
Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
|
neuper@42407
|
532 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
wneuper@59416
|
533 |
Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
|
neuper@42407
|
534 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@37950
|
535 |
|
wneuper@59416
|
536 |
Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
|
neuper@42407
|
537 |
(*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
|
wneuper@59416
|
538 |
Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
|
neuper@42407
|
539 |
(*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
|
wneuper@59416
|
540 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
541 |
|
neuper@37950
|
542 |
(*.the expression contains + - * ^ only ?
|
neuper@37950
|
543 |
this is weaker than 'is_polynomial' !.*)
|
neuper@37950
|
544 |
fun is_polyexp (Free _) = true
|
neuper@38014
|
545 |
| is_polyexp (Const ("Groups.plus_class.plus",_) $ Free _ $ Free _) = true
|
neuper@38014
|
546 |
| is_polyexp (Const ("Groups.minus_class.minus",_) $ Free _ $ Free _) = true
|
neuper@38034
|
547 |
| is_polyexp (Const ("Groups.times_class.times",_) $ Free _ $ Free _) = true
|
neuper@37950
|
548 |
| is_polyexp (Const ("Atools.pow",_) $ Free _ $ Free _) = true
|
neuper@38014
|
549 |
| is_polyexp (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
|
neuper@37950
|
550 |
((is_polyexp t1) andalso (is_polyexp t2))
|
neuper@38014
|
551 |
| is_polyexp (Const ("Groups.minus_class.minus",_) $ t1 $ t2) =
|
neuper@37950
|
552 |
((is_polyexp t1) andalso (is_polyexp t2))
|
neuper@38034
|
553 |
| is_polyexp (Const ("Groups.times_class.times",_) $ t1 $ t2) =
|
neuper@37950
|
554 |
((is_polyexp t1) andalso (is_polyexp t2))
|
neuper@37950
|
555 |
| is_polyexp (Const ("Atools.pow",_) $ t1 $ t2) =
|
neuper@37950
|
556 |
((is_polyexp t1) andalso (is_polyexp t2))
|
neuper@37950
|
557 |
| is_polyexp _ = false;
|
neuper@37950
|
558 |
|
neuper@37950
|
559 |
(*("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp ""))*)
|
neuper@37950
|
560 |
fun eval_is_polyexp (thmid:string) _
|
neuper@37950
|
561 |
(t as (Const("Poly.is'_polyexp", _) $ arg)) thy =
|
neuper@37950
|
562 |
if is_polyexp arg
|
wneuper@59416
|
563 |
then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
|
wneuper@59390
|
564 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
wneuper@59416
|
565 |
else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
|
wneuper@59390
|
566 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
neuper@37950
|
567 |
| eval_is_polyexp _ _ _ _ = NONE;
|
neuper@37950
|
568 |
|
neuper@37950
|
569 |
val expand_poly_rat_ =
|
wneuper@59416
|
570 |
Rule.Rls{id = "expand_poly_rat_", preconds = [],
|
wneuper@59416
|
571 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
572 |
erls = Rule.append_rls "Rule.e_rls-is_polyexp" Rule.e_rls
|
wneuper@59416
|
573 |
[Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")
|
neuper@37950
|
574 |
],
|
wneuper@59416
|
575 |
srls = Rule.Erls,
|
neuper@42451
|
576 |
calc = [], errpatts = [],
|
neuper@37950
|
577 |
rules =
|
wneuper@59416
|
578 |
[Rule.Thm ("real_plus_binom_pow4_poly", TermC.num_str @{thm real_plus_binom_pow4_poly}),
|
neuper@37950
|
579 |
(*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^4 = ... "*)
|
wneuper@59416
|
580 |
Rule.Thm ("real_plus_binom_pow5_poly", TermC.num_str @{thm real_plus_binom_pow5_poly}),
|
neuper@37950
|
581 |
(*"[| a is_polyexp; b is_polyexp |] ==> (a + b)^^^5 = ... "*)
|
wneuper@59416
|
582 |
Rule.Thm ("real_plus_binom_pow2_poly",TermC.num_str @{thm real_plus_binom_pow2_poly}),
|
neuper@37950
|
583 |
(*"[| a is_polyexp; b is_polyexp |] ==>
|
neuper@37950
|
584 |
(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
|
wneuper@59416
|
585 |
Rule.Thm ("real_plus_binom_pow3_poly",TermC.num_str @{thm real_plus_binom_pow3_poly}),
|
neuper@37950
|
586 |
(*"[| a is_polyexp; b is_polyexp |] ==>
|
neuper@37950
|
587 |
(a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3" *)
|
wneuper@59416
|
588 |
Rule.Thm ("real_plus_minus_binom1_p_p",TermC.num_str @{thm real_plus_minus_binom1_p_p}),
|
neuper@37950
|
589 |
(*"(a + b)*(a + -1 * b) = a^^^2 + -1*b^^^2"*)
|
wneuper@59416
|
590 |
Rule.Thm ("real_plus_minus_binom2_p_p",TermC.num_str @{thm real_plus_minus_binom2_p_p}),
|
neuper@37950
|
591 |
(*"(a + -1 * b)*(a + b) = a^^^2 + -1*b^^^2"*)
|
neuper@37950
|
592 |
|
wneuper@59416
|
593 |
Rule.Thm ("real_add_mult_distrib_poly",
|
wneuper@59389
|
594 |
TermC.num_str @{thm real_add_mult_distrib_poly}),
|
neuper@37950
|
595 |
(*"w is_polyexp ==> (z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
wneuper@59416
|
596 |
Rule.Thm("real_add_mult_distrib2_poly",
|
wneuper@59389
|
597 |
TermC.num_str @{thm real_add_mult_distrib2_poly}),
|
neuper@37950
|
598 |
(*"w is_polyexp ==> w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@37950
|
599 |
|
wneuper@59416
|
600 |
Rule.Thm ("realpow_multI_poly", TermC.num_str @{thm realpow_multI_poly}),
|
neuper@37950
|
601 |
(*"[| r is_polyexp; s is_polyexp |] ==>
|
neuper@37950
|
602 |
(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
|
wneuper@59416
|
603 |
Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
|
neuper@37950
|
604 |
(*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
|
wneuper@59416
|
605 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
606 |
|
neuper@37950
|
607 |
val simplify_power_ =
|
wneuper@59416
|
608 |
Rule.Rls{id = "simplify_power_", preconds = [],
|
wneuper@59416
|
609 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
610 |
erls = Rule.e_rls, srls = Rule.Erls,
|
neuper@42451
|
611 |
calc = [], errpatts = [],
|
wneuper@59416
|
612 |
rules = [(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
|
neuper@37950
|
613 |
a*(a*a) --> a*a^^^2 und nicht a*(a*a) --> a^^^2*a *)
|
wneuper@59416
|
614 |
Rule.Thm ("sym_realpow_twoI",
|
wneuper@59389
|
615 |
TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@37950
|
616 |
(*"r * r = r ^^^ 2"*)
|
wneuper@59416
|
617 |
Rule.Thm ("realpow_twoI_assoc_l",TermC.num_str @{thm realpow_twoI_assoc_l}),
|
neuper@37950
|
618 |
(*"r * (r * s) = r ^^^ 2 * s"*)
|
neuper@37950
|
619 |
|
wneuper@59416
|
620 |
Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
|
neuper@37950
|
621 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
wneuper@59416
|
622 |
Rule.Thm ("realpow_plus_1_assoc_l",
|
wneuper@59389
|
623 |
TermC.num_str @{thm realpow_plus_1_assoc_l}),
|
neuper@37950
|
624 |
(*"r * (r ^^^ m * s) = r ^^^ (1 + m) * s"*)
|
wneuper@59416
|
625 |
(*MG 9.7.03: neues Rule.Thm wegen a*(a*(a*b)) --> a^^^2*(a*b) *)
|
wneuper@59416
|
626 |
Rule.Thm ("realpow_plus_1_assoc_l2",
|
wneuper@59389
|
627 |
TermC.num_str @{thm realpow_plus_1_assoc_l2}),
|
neuper@37950
|
628 |
(*"r ^^^ m * (r * s) = r ^^^ (1 + m) * s"*)
|
neuper@37950
|
629 |
|
wneuper@59416
|
630 |
Rule.Thm ("sym_realpow_addI",
|
wneuper@59389
|
631 |
TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
|
neuper@37950
|
632 |
(*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
|
wneuper@59416
|
633 |
Rule.Thm ("realpow_addI_assoc_l",TermC.num_str @{thm realpow_addI_assoc_l}),
|
neuper@37950
|
634 |
(*"r ^^^ n * (r ^^^ m * s) = r ^^^ (n + m) * s"*)
|
neuper@37950
|
635 |
|
neuper@37950
|
636 |
(* ist in expand_poly - wird hier aber auch gebraucht, wegen:
|
neuper@37950
|
637 |
"r * r = r ^^^ 2" wenn r=a^^^b*)
|
wneuper@59416
|
638 |
Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow})
|
neuper@37950
|
639 |
(*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
|
wneuper@59416
|
640 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
641 |
|
neuper@37950
|
642 |
val calc_add_mult_pow_ =
|
wneuper@59416
|
643 |
Rule.Rls{id = "calc_add_mult_pow_", preconds = [],
|
wneuper@59416
|
644 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
645 |
erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
|
neuper@38014
|
646 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
647 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37950
|
648 |
("POWER", ("Atools.pow", eval_binop "#power_"))
|
neuper@37950
|
649 |
],
|
neuper@42451
|
650 |
errpatts = [],
|
wneuper@59416
|
651 |
rules = [Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
652 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
653 |
Rule.Calc ("Atools.pow", eval_binop "#power_")
|
wneuper@59416
|
654 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
655 |
|
neuper@37950
|
656 |
val reduce_012_mult_ =
|
wneuper@59416
|
657 |
Rule.Rls{id = "reduce_012_mult_", preconds = [],
|
wneuper@59416
|
658 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
659 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
660 |
calc = [], errpatts = [],
|
wneuper@59416
|
661 |
rules = [(* MG: folgende Rule.Thm müssen hier stehen bleiben: *)
|
wneuper@59416
|
662 |
Rule.Thm ("mult_1_right",TermC.num_str @{thm mult_1_right}),
|
neuper@37950
|
663 |
(*"z * 1 = z"*) (*wegen "a * b * b^^^(-1) + a"*)
|
wneuper@59416
|
664 |
Rule.Thm ("realpow_zeroI",TermC.num_str @{thm realpow_zeroI}),
|
neuper@37950
|
665 |
(*"r ^^^ 0 = 1"*) (*wegen "a*a^^^(-1)*c + b + c"*)
|
wneuper@59416
|
666 |
Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
|
neuper@37950
|
667 |
(*"r ^^^ 1 = r"*)
|
wneuper@59416
|
668 |
Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
|
neuper@37950
|
669 |
(*"1 ^^^ n = 1"*)
|
wneuper@59416
|
670 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
671 |
|
neuper@37950
|
672 |
val collect_numerals_ =
|
wneuper@59416
|
673 |
Rule.Rls{id = "collect_numerals_", preconds = [],
|
wneuper@59416
|
674 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
675 |
erls = Atools_erls, srls = Rule.Erls,
|
neuper@38014
|
676 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_"))
|
neuper@42451
|
677 |
], errpatts = [],
|
neuper@37950
|
678 |
rules =
|
wneuper@59416
|
679 |
[Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
|
neuper@37950
|
680 |
(*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
|
wneuper@59416
|
681 |
Rule.Thm ("real_num_collect_assoc_r",TermC.num_str @{thm real_num_collect_assoc_r}),
|
neuper@37950
|
682 |
(*"[| l is_const; m is_const |] ==> \
|
neuper@37950
|
683 |
\(k + m * n) + l * n = k + (l + m)*n"*)
|
wneuper@59416
|
684 |
Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
|
neuper@37950
|
685 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
wneuper@59416
|
686 |
Rule.Thm ("real_one_collect_assoc_r",TermC.num_str @{thm real_one_collect_assoc_r}),
|
neuper@37950
|
687 |
(*"m is_const ==> (k + n) + m * n = k + (m + 1) * n"*)
|
neuper@37950
|
688 |
|
wneuper@59416
|
689 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@37950
|
690 |
|
wneuper@59416
|
691 |
(*MG: Reihenfolge der folgenden 2 Rule.Thm muss so bleiben, wegen
|
neuper@37950
|
692 |
(a+a)+a --> a + 2*a --> 3*a and not (a+a)+a --> 2*a + a *)
|
wneuper@59416
|
693 |
Rule.Thm ("real_mult_2_assoc_r",TermC.num_str @{thm real_mult_2_assoc_r}),
|
neuper@37950
|
694 |
(*"(k + z1) + z1 = k + 2 * z1"*)
|
wneuper@59416
|
695 |
Rule.Thm ("sym_real_mult_2",TermC.num_str (@{thm real_mult_2} RS @{thm sym}))
|
neuper@37950
|
696 |
(*"z1 + z1 = 2 * z1"*)
|
wneuper@59416
|
697 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
698 |
|
neuper@37950
|
699 |
val reduce_012_ =
|
wneuper@59416
|
700 |
Rule.Rls{id = "reduce_012_", preconds = [],
|
wneuper@59416
|
701 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
702 |
erls = Rule.e_rls,srls = Rule.Erls, calc = [], errpatts = [],
|
wneuper@59416
|
703 |
rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
|
neuper@37950
|
704 |
(*"1 * z = z"*)
|
wneuper@59416
|
705 |
Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
|
neuper@37950
|
706 |
(*"0 * z = 0"*)
|
wneuper@59416
|
707 |
Rule.Thm ("mult_zero_right",TermC.num_str @{thm mult_zero_right}),
|
neuper@37950
|
708 |
(*"z * 0 = 0"*)
|
wneuper@59416
|
709 |
Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
|
neuper@37950
|
710 |
(*"0 + z = z"*)
|
wneuper@59416
|
711 |
Rule.Thm ("add_0_right",TermC.num_str @{thm add_0_right}),
|
neuper@37950
|
712 |
(*"z + 0 = z"*) (*wegen a+b-b --> a+(1-1)*b --> a+0 --> a*)
|
neuper@37950
|
713 |
|
wneuper@59416
|
714 |
(*Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI})*)
|
neuper@37950
|
715 |
(*"?r ^^^ 1 = ?r"*)
|
wneuper@59416
|
716 |
Rule.Thm ("division_ring_divide_zero",TermC.num_str @{thm division_ring_divide_zero})
|
neuper@37950
|
717 |
(*"0 / ?x = 0"*)
|
wneuper@59416
|
718 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
719 |
|
neuper@37979
|
720 |
val discard_parentheses1 =
|
wneuper@59416
|
721 |
Rule.append_rls "discard_parentheses1" Rule.e_rls
|
wneuper@59416
|
722 |
[Rule.Thm ("sym_mult_assoc",
|
wneuper@59389
|
723 |
TermC.num_str (@{thm mult.assoc} RS @{thm sym}))
|
neuper@37950
|
724 |
(*"?z1.1 * (?z2.1 * ?z3.1) = ?z1.1 * ?z2.1 * ?z3.1"*)
|
wneuper@59416
|
725 |
(*Rule.Thm ("sym_add_assoc",
|
wneuper@59389
|
726 |
TermC.num_str (@{thm add_assoc} RS @{thm sym}))*)
|
neuper@37950
|
727 |
(*"?z1.1 + (?z2.1 + ?z3.1) = ?z1.1 + ?z2.1 + ?z3.1"*)
|
neuper@37950
|
728 |
];
|
neuper@37950
|
729 |
|
neuper@37950
|
730 |
(*----------------- End: rulesets for make_polynomial_ -----------------*)
|
neuper@37950
|
731 |
|
neuper@37950
|
732 |
(*MG.0401 ev. for use in rls with ordered rewriting ?
|
neuper@37950
|
733 |
val collect_numerals_left =
|
wneuper@59416
|
734 |
Rule.Rls{id = "collect_numerals", preconds = [],
|
wneuper@59416
|
735 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
736 |
erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
|
neuper@38014
|
737 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
738 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37950
|
739 |
("POWER", ("Atools.pow", eval_binop "#power_"))
|
neuper@37950
|
740 |
],
|
neuper@42451
|
741 |
errpatts = [],
|
wneuper@59416
|
742 |
rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
|
neuper@37950
|
743 |
(*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
|
wneuper@59416
|
744 |
Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
|
neuper@37950
|
745 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
746 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
wneuper@59416
|
747 |
Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
|
neuper@37950
|
748 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
wneuper@59416
|
749 |
Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
|
neuper@37950
|
750 |
(*"m is_const ==> n + (m * n + k) = (1 + m) * n + k"*)
|
neuper@37950
|
751 |
|
wneuper@59416
|
752 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
neuper@37950
|
753 |
|
neuper@37950
|
754 |
(*MG am 2.5.03: 2 Theoreme aus reduce_012 hierher verschoben*)
|
wneuper@59416
|
755 |
Rule.Thm ("sym_real_mult_2",
|
wneuper@59389
|
756 |
TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37950
|
757 |
(*"z1 + z1 = 2 * z1"*)
|
wneuper@59416
|
758 |
Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc})
|
neuper@37950
|
759 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
wneuper@59416
|
760 |
], scr = Rule.EmptyScr};*)
|
neuper@37950
|
761 |
|
neuper@37950
|
762 |
val expand_poly =
|
wneuper@59416
|
763 |
Rule.Rls{id = "expand_poly", preconds = [],
|
wneuper@59416
|
764 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
765 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
766 |
calc = [], errpatts = [],
|
neuper@37950
|
767 |
(*asm_thm = [],*)
|
wneuper@59416
|
768 |
rules = [Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
|
neuper@37950
|
769 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
wneuper@59416
|
770 |
Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
|
neuper@37950
|
771 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
wneuper@59416
|
772 |
(*Rule.Thm ("distrib_right1",TermC.num_str @{thm distrib_right}1),
|
neuper@37950
|
773 |
....... 18.3.03 undefined???*)
|
neuper@37950
|
774 |
|
wneuper@59416
|
775 |
Rule.Thm ("real_plus_binom_pow2",TermC.num_str @{thm real_plus_binom_pow2}),
|
neuper@37950
|
776 |
(*"(a + b)^^^2 = a^^^2 + 2*a*b + b^^^2"*)
|
wneuper@59416
|
777 |
Rule.Thm ("real_minus_binom_pow2_p",TermC.num_str @{thm real_minus_binom_pow2_p}),
|
neuper@37950
|
778 |
(*"(a - b)^^^2 = a^^^2 + -2*a*b + b^^^2"*)
|
wneuper@59416
|
779 |
Rule.Thm ("real_plus_minus_binom1_p",
|
wneuper@59389
|
780 |
TermC.num_str @{thm real_plus_minus_binom1_p}),
|
neuper@37950
|
781 |
(*"(a + b)*(a - b) = a^^^2 + -1*b^^^2"*)
|
wneuper@59416
|
782 |
Rule.Thm ("real_plus_minus_binom2_p",
|
wneuper@59389
|
783 |
TermC.num_str @{thm real_plus_minus_binom2_p}),
|
neuper@37950
|
784 |
(*"(a - b)*(a + b) = a^^^2 + -1*b^^^2"*)
|
neuper@37950
|
785 |
|
wneuper@59416
|
786 |
Rule.Thm ("minus_minus",TermC.num_str @{thm minus_minus}),
|
neuper@37950
|
787 |
(*"- (- ?z) = ?z"*)
|
wneuper@59416
|
788 |
Rule.Thm ("real_diff_minus",TermC.num_str @{thm real_diff_minus}),
|
neuper@37950
|
789 |
(*"a - b = a + -1 * b"*)
|
wneuper@59416
|
790 |
Rule.Thm ("sym_real_mult_minus1",
|
wneuper@59389
|
791 |
TermC.num_str (@{thm real_mult_minus1} RS @{thm sym}))
|
neuper@37950
|
792 |
(*- ?z = "-1 * ?z"*)
|
neuper@37950
|
793 |
|
wneuper@59416
|
794 |
(*Rule.Thm ("real_minus_add_distrib",
|
wneuper@59389
|
795 |
TermC.num_str @{thm real_minus_add_distrib}),*)
|
neuper@37950
|
796 |
(*"- (?x + ?y) = - ?x + - ?y"*)
|
wneuper@59416
|
797 |
(*Rule.Thm ("real_diff_plus",TermC.num_str @{thm real_diff_plus})*)
|
neuper@37950
|
798 |
(*"a - b = a + -b"*)
|
wneuper@59416
|
799 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
800 |
|
neuper@37950
|
801 |
val simplify_power =
|
wneuper@59416
|
802 |
Rule.Rls{id = "simplify_power", preconds = [],
|
wneuper@59416
|
803 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
804 |
erls = Rule.e_rls, srls = Rule.Erls,
|
neuper@42451
|
805 |
calc = [], errpatts = [],
|
wneuper@59416
|
806 |
rules = [Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
|
neuper@37950
|
807 |
(*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
|
neuper@37950
|
808 |
|
wneuper@59416
|
809 |
Rule.Thm ("sym_realpow_twoI",
|
wneuper@59389
|
810 |
TermC.num_str( @{thm realpow_twoI} RS @{thm sym})),
|
neuper@37950
|
811 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
wneuper@59416
|
812 |
Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
|
neuper@37950
|
813 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
wneuper@59416
|
814 |
Rule.Thm ("realpow_pow",TermC.num_str @{thm realpow_pow}),
|
neuper@37950
|
815 |
(*"(a ^^^ b) ^^^ c = a ^^^ (b * c)"*)
|
wneuper@59416
|
816 |
Rule.Thm ("sym_realpow_addI",
|
wneuper@59389
|
817 |
TermC.num_str (@{thm realpow_addI} RS @{thm sym})),
|
neuper@37950
|
818 |
(*"r ^^^ n * r ^^^ m = r ^^^ (n + m)"*)
|
wneuper@59416
|
819 |
Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),
|
neuper@37950
|
820 |
(*"r ^^^ 1 = r"*)
|
wneuper@59416
|
821 |
Rule.Thm ("realpow_eq_oneI",TermC.num_str @{thm realpow_eq_oneI})
|
neuper@37950
|
822 |
(*"1 ^^^ n = 1"*)
|
wneuper@59416
|
823 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
824 |
(*MG.0401: termorders for multivariate polys dropped due to principal problems:
|
neuper@37950
|
825 |
(total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
|
neuper@37950
|
826 |
val order_add_mult =
|
wneuper@59416
|
827 |
Rule.Rls{id = "order_add_mult", preconds = [],
|
neuper@37972
|
828 |
rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
|
wneuper@59416
|
829 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
830 |
calc = [], errpatts = [],
|
wneuper@59416
|
831 |
rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
|
neuper@37950
|
832 |
(* z * w = w * z *)
|
wneuper@59416
|
833 |
Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
|
neuper@37950
|
834 |
(*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
|
wneuper@59416
|
835 |
Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
|
neuper@37950
|
836 |
(*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
|
wneuper@59416
|
837 |
Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
|
neuper@37950
|
838 |
(*z + w = w + z*)
|
wneuper@59416
|
839 |
Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
|
neuper@37950
|
840 |
(*x + (y + z) = y + (x + z)*)
|
wneuper@59416
|
841 |
Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc})
|
neuper@37950
|
842 |
(*z1.0 + z2.0 + z3.0 = z1.0 + (z2.0 + z3.0)*)
|
wneuper@59416
|
843 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
844 |
(*MG.0401: termorders for multivariate polys dropped due to principal problems:
|
neuper@37950
|
845 |
(total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
|
neuper@37950
|
846 |
val order_mult =
|
wneuper@59416
|
847 |
Rule.Rls{id = "order_mult", preconds = [],
|
neuper@37972
|
848 |
rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
|
wneuper@59416
|
849 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
850 |
calc = [], errpatts = [],
|
wneuper@59416
|
851 |
rules = [Rule.Thm ("mult_commute",TermC.num_str @{thm mult.commute}),
|
neuper@37950
|
852 |
(* z * w = w * z *)
|
wneuper@59416
|
853 |
Rule.Thm ("real_mult_left_commute",TermC.num_str @{thm real_mult_left_commute}),
|
neuper@37950
|
854 |
(*z1.0 * (z2.0 * z3.0) = z2.0 * (z1.0 * z3.0)*)
|
wneuper@59416
|
855 |
Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc})
|
neuper@37950
|
856 |
(*z1.0 * z2.0 * z3.0 = z1.0 * (z2.0 * z3.0)*)
|
wneuper@59416
|
857 |
], scr = Rule.EmptyScr};
|
neuper@42451
|
858 |
*}
|
neuper@42451
|
859 |
|
neuper@42451
|
860 |
ML {*
|
neuper@37950
|
861 |
val collect_numerals =
|
wneuper@59416
|
862 |
Rule.Rls{id = "collect_numerals", preconds = [],
|
wneuper@59416
|
863 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
864 |
erls = Atools_erls(*erls3.4.03*),srls = Rule.Erls,
|
neuper@38014
|
865 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
866 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37950
|
867 |
("POWER", ("Atools.pow", eval_binop "#power_"))
|
neuper@42451
|
868 |
], errpatts = [],
|
wneuper@59416
|
869 |
rules = [Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
|
neuper@37950
|
870 |
(*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
|
wneuper@59416
|
871 |
Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
|
neuper@37950
|
872 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
873 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
wneuper@59416
|
874 |
Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
|
neuper@37950
|
875 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
wneuper@59416
|
876 |
Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
|
neuper@37950
|
877 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
wneuper@59416
|
878 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
879 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
880 |
Rule.Calc ("Atools.pow", eval_binop "#power_")
|
wneuper@59416
|
881 |
], scr = Rule.EmptyScr};
|
neuper@37950
|
882 |
val reduce_012 =
|
wneuper@59416
|
883 |
Rule.Rls{id = "reduce_012", preconds = [],
|
wneuper@59416
|
884 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
885 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
886 |
calc = [], errpatts = [],
|
wneuper@59416
|
887 |
rules = [Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
|
neuper@37950
|
888 |
(*"1 * z = z"*)
|
wneuper@59416
|
889 |
(*Rule.Thm ("real_mult_minus1",TermC.num_str @{thm real_mult_minus1}),14.3.03*)
|
neuper@37950
|
890 |
(*"-1 * z = - z"*)
|
wneuper@59416
|
891 |
Rule.Thm ("minus_mult_left",
|
wneuper@59389
|
892 |
TermC.num_str (@{thm minus_mult_left} RS @{thm sym})),
|
neuper@37950
|
893 |
(*- (?x * ?y) = "- ?x * ?y"*)
|
wneuper@59416
|
894 |
(*Rule.Thm ("real_minus_mult_cancel",
|
wneuper@59389
|
895 |
TermC.num_str @{thm real_minus_mult_cancel}),
|
neuper@37950
|
896 |
(*"- ?x * - ?y = ?x * ?y"*)---*)
|
wneuper@59416
|
897 |
Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
|
neuper@37950
|
898 |
(*"0 * z = 0"*)
|
wneuper@59416
|
899 |
Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),
|
neuper@37950
|
900 |
(*"0 + z = z"*)
|
wneuper@59416
|
901 |
Rule.Thm ("right_minus",TermC.num_str @{thm right_minus}),
|
neuper@37950
|
902 |
(*"?z + - ?z = 0"*)
|
wneuper@59416
|
903 |
Rule.Thm ("sym_real_mult_2",
|
wneuper@59389
|
904 |
TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37950
|
905 |
(*"z1 + z1 = 2 * z1"*)
|
wneuper@59416
|
906 |
Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc})
|
neuper@37950
|
907 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
wneuper@59416
|
908 |
], scr = Rule.EmptyScr};
|
neuper@52139
|
909 |
|
neuper@37950
|
910 |
val discard_parentheses =
|
wneuper@59416
|
911 |
Rule.append_rls "discard_parentheses" Rule.e_rls
|
wneuper@59416
|
912 |
[Rule.Thm ("sym_mult_assoc",
|
wneuper@59389
|
913 |
TermC.num_str (@{thm mult.assoc} RS @{thm sym})),
|
wneuper@59416
|
914 |
Rule.Thm ("sym_add_assoc",
|
wneuper@59389
|
915 |
TermC.num_str (@{thm add.assoc} RS @{thm sym}))];
|
neuper@37950
|
916 |
|
wneuper@59429
|
917 |
(* probably perfectly replaced by auto-generated version *)
|
neuper@37950
|
918 |
val scr_make_polynomial =
|
neuper@37976
|
919 |
"Script Expand_binoms t_t = " ^
|
neuper@37950
|
920 |
"(Repeat " ^
|
neuper@37950
|
921 |
"((Try (Repeat (Rewrite real_diff_minus False))) @@ " ^
|
neuper@37950
|
922 |
|
neuper@52062
|
923 |
" (Try (Repeat (Rewrite distrib_right False))) @@ " ^
|
neuper@52062
|
924 |
" (Try (Repeat (Rewrite distrib_left False))) @@ " ^
|
neuper@37971
|
925 |
" (Try (Repeat (Rewrite left_diff_distrib False))) @@ " ^
|
neuper@37971
|
926 |
" (Try (Repeat (Rewrite right_diff_distrib False))) @@ " ^
|
neuper@37950
|
927 |
|
neuper@37971
|
928 |
" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
|
neuper@37971
|
929 |
" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
|
neuper@37971
|
930 |
" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
|
neuper@37950
|
931 |
|
neuper@48763
|
932 |
" (Try (Repeat (Rewrite mult_commute False))) @@ " ^
|
neuper@37950
|
933 |
" (Try (Repeat (Rewrite real_mult_left_commute False))) @@ " ^
|
neuper@48763
|
934 |
" (Try (Repeat (Rewrite mult_assoc False))) @@ " ^
|
neuper@37971
|
935 |
" (Try (Repeat (Rewrite add_commute False))) @@ " ^
|
neuper@37971
|
936 |
" (Try (Repeat (Rewrite add_left_commute False))) @@ " ^
|
neuper@37971
|
937 |
" (Try (Repeat (Rewrite add_assoc False))) @@ " ^
|
neuper@37950
|
938 |
|
neuper@37950
|
939 |
" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
|
neuper@37950
|
940 |
" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
|
neuper@37950
|
941 |
" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
|
neuper@37950
|
942 |
" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
|
neuper@37950
|
943 |
|
neuper@37950
|
944 |
" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
|
neuper@37950
|
945 |
" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
|
neuper@37950
|
946 |
|
neuper@37950
|
947 |
" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
|
neuper@37950
|
948 |
" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
|
neuper@37950
|
949 |
|
neuper@37975
|
950 |
" (Try (Repeat (Calculate PLUS ))) @@ " ^
|
neuper@37975
|
951 |
" (Try (Repeat (Calculate TIMES ))) @@ " ^
|
neuper@37975
|
952 |
" (Try (Repeat (Calculate POWER)))) " ^
|
neuper@37976
|
953 |
" t_t)";
|
neuper@37950
|
954 |
|
neuper@37950
|
955 |
(*version used by MG.02/03, overwritten by version AG in 04 below
|
s1210629013@55444
|
956 |
val make_polynomial = prep_rls'(
|
wneuper@59416
|
957 |
Rule.Seq{id = "make_polynomial", preconds = []:term list,
|
wneuper@59416
|
958 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
959 |
erls = Atools_erls, srls = Rule.Erls,
|
neuper@42451
|
960 |
calc = [], errpatts = [],
|
wneuper@59416
|
961 |
rules = [Rule.Rls_ expand_poly,
|
wneuper@59416
|
962 |
Rule.Rls_ order_add_mult,
|
wneuper@59416
|
963 |
Rule.Rls_ simplify_power, (*realpow_eq_oneI, eg. x^1 --> x *)
|
wneuper@59416
|
964 |
Rule.Rls_ collect_numerals, (*eg. x^(2+ -1) --> x^1 *)
|
wneuper@59416
|
965 |
Rule.Rls_ reduce_012,
|
wneuper@59416
|
966 |
Rule.Thm ("realpow_oneI",TermC.num_str @{thm realpow_oneI}),(*in --^*)
|
wneuper@59416
|
967 |
Rule.Rls_ discard_parentheses
|
neuper@37950
|
968 |
],
|
wneuper@59416
|
969 |
scr = Rule.EmptyScr
|
wneuper@59406
|
970 |
}); *)
|
neuper@37950
|
971 |
|
wneuper@59429
|
972 |
(* replacement by auto-generated version seemed to cause ERROR in algein.sml *)
|
neuper@37950
|
973 |
val scr_expand_binoms =
|
neuper@37974
|
974 |
"Script Expand_binoms t_t =" ^
|
neuper@37950
|
975 |
"(Repeat " ^
|
neuper@37950
|
976 |
"((Try (Repeat (Rewrite real_plus_binom_pow2 False))) @@ " ^
|
neuper@37950
|
977 |
" (Try (Repeat (Rewrite real_plus_binom_times False))) @@ " ^
|
neuper@37950
|
978 |
" (Try (Repeat (Rewrite real_minus_binom_pow2 False))) @@ " ^
|
neuper@37950
|
979 |
" (Try (Repeat (Rewrite real_minus_binom_times False))) @@ " ^
|
neuper@37950
|
980 |
" (Try (Repeat (Rewrite real_plus_minus_binom1 False))) @@ " ^
|
neuper@37950
|
981 |
" (Try (Repeat (Rewrite real_plus_minus_binom2 False))) @@ " ^
|
neuper@37950
|
982 |
|
neuper@37971
|
983 |
" (Try (Repeat (Rewrite mult_1_left False))) @@ " ^
|
neuper@37971
|
984 |
" (Try (Repeat (Rewrite mult_zero_left False))) @@ " ^
|
neuper@37971
|
985 |
" (Try (Repeat (Rewrite add_0_left False))) @@ " ^
|
neuper@37950
|
986 |
|
neuper@37975
|
987 |
" (Try (Repeat (Calculate PLUS ))) @@ " ^
|
neuper@37975
|
988 |
" (Try (Repeat (Calculate TIMES ))) @@ " ^
|
neuper@37975
|
989 |
" (Try (Repeat (Calculate POWER))) @@ " ^
|
neuper@37950
|
990 |
|
neuper@37950
|
991 |
" (Try (Repeat (Rewrite sym_realpow_twoI False))) @@ " ^
|
neuper@37950
|
992 |
" (Try (Repeat (Rewrite realpow_plus_1 False))) @@ " ^
|
neuper@37950
|
993 |
" (Try (Repeat (Rewrite sym_real_mult_2 False))) @@ " ^
|
neuper@37950
|
994 |
" (Try (Repeat (Rewrite real_mult_2_assoc False))) @@ " ^
|
neuper@37950
|
995 |
|
neuper@37950
|
996 |
" (Try (Repeat (Rewrite real_num_collect False))) @@ " ^
|
neuper@37950
|
997 |
" (Try (Repeat (Rewrite real_num_collect_assoc False))) @@ " ^
|
neuper@37950
|
998 |
|
neuper@37950
|
999 |
" (Try (Repeat (Rewrite real_one_collect False))) @@ " ^
|
neuper@37950
|
1000 |
" (Try (Repeat (Rewrite real_one_collect_assoc False))) @@ " ^
|
neuper@37950
|
1001 |
|
neuper@37975
|
1002 |
" (Try (Repeat (Calculate PLUS ))) @@ " ^
|
neuper@37975
|
1003 |
" (Try (Repeat (Calculate TIMES ))) @@ " ^
|
neuper@37975
|
1004 |
" (Try (Repeat (Calculate POWER)))) " ^
|
neuper@37974
|
1005 |
" t_t)";
|
neuper@37974
|
1006 |
|
neuper@37950
|
1007 |
val expand_binoms =
|
wneuper@59416
|
1008 |
Rule.Rls{id = "expand_binoms", preconds = [], rew_ord = ("termlessI",termlessI),
|
wneuper@59416
|
1009 |
erls = Atools_erls, srls = Rule.Erls,
|
neuper@38014
|
1010 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
1011 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37950
|
1012 |
("POWER", ("Atools.pow", eval_binop "#power_"))
|
neuper@42451
|
1013 |
], errpatts = [],
|
wneuper@59416
|
1014 |
rules = [Rule.Thm ("real_plus_binom_pow2",
|
wneuper@59389
|
1015 |
TermC.num_str @{thm real_plus_binom_pow2}),
|
neuper@37950
|
1016 |
(*"(a + b) ^^^ 2 = a ^^^ 2 + 2 * a * b + b ^^^ 2"*)
|
wneuper@59416
|
1017 |
Rule.Thm ("real_plus_binom_times",
|
wneuper@59389
|
1018 |
TermC.num_str @{thm real_plus_binom_times}),
|
neuper@37950
|
1019 |
(*"(a + b)*(a + b) = ...*)
|
wneuper@59416
|
1020 |
Rule.Thm ("real_minus_binom_pow2",
|
wneuper@59389
|
1021 |
TermC.num_str @{thm real_minus_binom_pow2}),
|
neuper@37950
|
1022 |
(*"(a - b) ^^^ 2 = a ^^^ 2 - 2 * a * b + b ^^^ 2"*)
|
wneuper@59416
|
1023 |
Rule.Thm ("real_minus_binom_times",
|
wneuper@59389
|
1024 |
TermC.num_str @{thm real_minus_binom_times}),
|
neuper@37950
|
1025 |
(*"(a - b)*(a - b) = ...*)
|
wneuper@59416
|
1026 |
Rule.Thm ("real_plus_minus_binom1",
|
wneuper@59389
|
1027 |
TermC.num_str @{thm real_plus_minus_binom1}),
|
neuper@37950
|
1028 |
(*"(a + b) * (a - b) = a ^^^ 2 - b ^^^ 2"*)
|
wneuper@59416
|
1029 |
Rule.Thm ("real_plus_minus_binom2",
|
wneuper@59389
|
1030 |
TermC.num_str @{thm real_plus_minus_binom2}),
|
neuper@37950
|
1031 |
(*"(a - b) * (a + b) = a ^^^ 2 - b ^^^ 2"*)
|
neuper@37950
|
1032 |
(*RL 020915*)
|
wneuper@59416
|
1033 |
Rule.Thm ("real_pp_binom_times",TermC.num_str @{thm real_pp_binom_times}),
|
neuper@37950
|
1034 |
(*(a + b)*(c + d) = a*c + a*d + b*c + b*d*)
|
wneuper@59416
|
1035 |
Rule.Thm ("real_pm_binom_times",TermC.num_str @{thm real_pm_binom_times}),
|
neuper@37950
|
1036 |
(*(a + b)*(c - d) = a*c - a*d + b*c - b*d*)
|
wneuper@59416
|
1037 |
Rule.Thm ("real_mp_binom_times",TermC.num_str @{thm real_mp_binom_times}),
|
neuper@37950
|
1038 |
(*(a - b)*(c + d) = a*c + a*d - b*c - b*d*)
|
wneuper@59416
|
1039 |
Rule.Thm ("real_mm_binom_times",TermC.num_str @{thm real_mm_binom_times}),
|
neuper@37950
|
1040 |
(*(a - b)*(c - d) = a*c - a*d - b*c + b*d*)
|
wneuper@59416
|
1041 |
Rule.Thm ("realpow_multI",TermC.num_str @{thm realpow_multI}),
|
neuper@37950
|
1042 |
(*(a*b)^^^n = a^^^n * b^^^n*)
|
wneuper@59416
|
1043 |
Rule.Thm ("real_plus_binom_pow3",TermC.num_str @{thm real_plus_binom_pow3}),
|
neuper@37950
|
1044 |
(* (a + b)^^^3 = a^^^3 + 3*a^^^2*b + 3*a*b^^^2 + b^^^3 *)
|
wneuper@59416
|
1045 |
Rule.Thm ("real_minus_binom_pow3",
|
wneuper@59389
|
1046 |
TermC.num_str @{thm real_minus_binom_pow3}),
|
neuper@37950
|
1047 |
(* (a - b)^^^3 = a^^^3 - 3*a^^^2*b + 3*a*b^^^2 - b^^^3 *)
|
neuper@37950
|
1048 |
|
neuper@37950
|
1049 |
|
wneuper@59416
|
1050 |
(*Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
|
neuper@37950
|
1051 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
wneuper@59416
|
1052 |
Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
|
neuper@37950
|
1053 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
wneuper@59416
|
1054 |
Rule.Thm ("left_diff_distrib" ,TermC.num_str @{thm left_diff_distrib}),
|
neuper@37950
|
1055 |
(*"(z1.0 - z2.0) * w = z1.0 * w - z2.0 * w"*)
|
wneuper@59416
|
1056 |
Rule.Thm ("right_diff_distrib",TermC.num_str @{thm right_diff_distrib}),
|
neuper@37950
|
1057 |
(*"w * (z1.0 - z2.0) = w * z1.0 - w * z2.0"*)
|
neuper@37974
|
1058 |
*)
|
wneuper@59416
|
1059 |
Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),
|
neuper@37974
|
1060 |
(*"1 * z = z"*)
|
wneuper@59416
|
1061 |
Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),
|
neuper@37974
|
1062 |
(*"0 * z = 0"*)
|
wneuper@59416
|
1063 |
Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left}),(*"0 + z = z"*)
|
neuper@37950
|
1064 |
|
wneuper@59416
|
1065 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
1066 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1067 |
Rule.Calc ("Atools.pow", eval_binop "#power_"),
|
wneuper@59416
|
1068 |
(*Rule.Thm ("mult_commute",TermC.num_str @{thm mult_commute}),
|
neuper@37974
|
1069 |
(*AC-rewriting*)
|
wneuper@59416
|
1070 |
Rule.Thm ("real_mult_left_commute",
|
wneuper@59389
|
1071 |
TermC.num_str @{thm real_mult_left_commute}),
|
wneuper@59416
|
1072 |
Rule.Thm ("mult_assoc",TermC.num_str @{thm mult.assoc}),
|
wneuper@59416
|
1073 |
Rule.Thm ("add_commute",TermC.num_str @{thm add.commute}),
|
wneuper@59416
|
1074 |
Rule.Thm ("add_left_commute",TermC.num_str @{thm add.left_commute}),
|
wneuper@59416
|
1075 |
Rule.Thm ("add_assoc",TermC.num_str @{thm add.assoc}),
|
neuper@37974
|
1076 |
*)
|
wneuper@59416
|
1077 |
Rule.Thm ("sym_realpow_twoI",
|
wneuper@59389
|
1078 |
TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@37950
|
1079 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
wneuper@59416
|
1080 |
Rule.Thm ("realpow_plus_1",TermC.num_str @{thm realpow_plus_1}),
|
neuper@37950
|
1081 |
(*"r * r ^^^ n = r ^^^ (n + 1)"*)
|
wneuper@59416
|
1082 |
(*Rule.Thm ("sym_real_mult_2",
|
wneuper@59389
|
1083 |
TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37950
|
1084 |
(*"z1 + z1 = 2 * z1"*)*)
|
wneuper@59416
|
1085 |
Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
|
neuper@37950
|
1086 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
1087 |
|
wneuper@59416
|
1088 |
Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
|
neuper@37974
|
1089 |
(*"[| l is_const; m is_const |] ==>l * n + m * n = (l + m) * n"*)
|
wneuper@59416
|
1090 |
Rule.Thm ("real_num_collect_assoc",
|
wneuper@59389
|
1091 |
TermC.num_str @{thm real_num_collect_assoc}),
|
neuper@37974
|
1092 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37974
|
1093 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
wneuper@59416
|
1094 |
Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
|
neuper@37950
|
1095 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
wneuper@59416
|
1096 |
Rule.Thm ("real_one_collect_assoc",
|
wneuper@59389
|
1097 |
TermC.num_str @{thm real_one_collect_assoc}),
|
neuper@37950
|
1098 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37950
|
1099 |
|
wneuper@59416
|
1100 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
1101 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1102 |
Rule.Calc ("Atools.pow", eval_binop "#power_")
|
neuper@37950
|
1103 |
],
|
wneuper@59416
|
1104 |
scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) scr_expand_binoms)
|
wneuper@59406
|
1105 |
};
|
neuper@37950
|
1106 |
|
neuper@37950
|
1107 |
|
neuper@37950
|
1108 |
(**. MG.03: make_polynomial_ ... uses SML-fun for ordering .**)
|
neuper@37950
|
1109 |
|
neuper@37950
|
1110 |
(*FIXME.0401: make SML-order local to make_polynomial(_) *)
|
neuper@37950
|
1111 |
(*FIXME.0401: replace 'make_polynomial'(old) by 'make_polynomial_'(MG) *)
|
neuper@37950
|
1112 |
(* Polynom --> List von Monomen *)
|
neuper@38014
|
1113 |
fun poly2list (Const ("Groups.plus_class.plus",_) $ t1 $ t2) =
|
neuper@37950
|
1114 |
(poly2list t1) @ (poly2list t2)
|
neuper@37950
|
1115 |
| poly2list t = [t];
|
neuper@37950
|
1116 |
|
neuper@37950
|
1117 |
(* Monom --> Liste von Variablen *)
|
neuper@38034
|
1118 |
fun monom2list (Const ("Groups.times_class.times",_) $ t1 $ t2) =
|
neuper@37950
|
1119 |
(monom2list t1) @ (monom2list t2)
|
neuper@37950
|
1120 |
| monom2list t = [t];
|
neuper@37950
|
1121 |
|
neuper@37950
|
1122 |
(* liefert Variablenname (String) einer Variablen und Basis bei Potenz *)
|
neuper@37950
|
1123 |
fun get_basStr (Const ("Atools.pow",_) $ Free (str, _) $ _) = str
|
neuper@37950
|
1124 |
| get_basStr (Free (str, _)) = str
|
neuper@37950
|
1125 |
| get_basStr t = "|||"; (* gross gewichtet; für Brüch ect. *)
|
neuper@37950
|
1126 |
(*| get_basStr t =
|
wneuper@59416
|
1127 |
error("get_basStr: called with t= "^(Rule.term2str t));*)
|
neuper@37950
|
1128 |
|
neuper@37950
|
1129 |
(* liefert Hochzahl (String) einer Variablen bzw Gewichtstring (zum Sortieren) *)
|
neuper@37950
|
1130 |
fun get_potStr (Const ("Atools.pow",_) $ Free _ $ Free (str, _)) = str
|
neuper@37950
|
1131 |
| get_potStr (Const ("Atools.pow",_) $ Free _ $ _ ) = "|||" (* gross gewichtet *)
|
neuper@37950
|
1132 |
| get_potStr (Free (str, _)) = "---" (* keine Hochzahl --> kleinst gewichtet *)
|
neuper@37950
|
1133 |
| get_potStr t = "||||||"; (* gross gewichtet; für Brüch ect. *)
|
neuper@37950
|
1134 |
(*| get_potStr t =
|
wneuper@59416
|
1135 |
error("get_potStr: called with t= "^(Rule.term2str t));*)
|
neuper@37950
|
1136 |
|
neuper@37950
|
1137 |
(* Umgekehrte string_ord *)
|
neuper@37950
|
1138 |
val string_ord_rev = rev_order o string_ord;
|
neuper@37950
|
1139 |
|
neuper@37950
|
1140 |
(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen)
|
neuper@37950
|
1141 |
innerhalb eines Monomes:
|
neuper@37950
|
1142 |
- zuerst lexikographisch nach Variablenname
|
neuper@37950
|
1143 |
- wenn gleich: nach steigender Potenz *)
|
neuper@37950
|
1144 |
fun var_ord (a,b: term) = prod_ord string_ord string_ord
|
neuper@37950
|
1145 |
((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
|
neuper@37950
|
1146 |
|
neuper@37950
|
1147 |
(* Ordnung zum lexikographischen Vergleich zweier Variablen (oder Potenzen);
|
neuper@37950
|
1148 |
verwendet zum Sortieren von Monomen mittels Gesamtgradordnung:
|
neuper@37950
|
1149 |
- zuerst lexikographisch nach Variablenname
|
neuper@37950
|
1150 |
- wenn gleich: nach sinkender Potenz*)
|
neuper@37950
|
1151 |
fun var_ord_revPow (a,b: term) = prod_ord string_ord string_ord_rev
|
neuper@37950
|
1152 |
((get_basStr a, get_potStr a), (get_basStr b, get_potStr b));
|
neuper@37950
|
1153 |
|
neuper@37950
|
1154 |
|
neuper@37950
|
1155 |
(* Ordnet ein Liste von Variablen (und Potenzen) lexikographisch *)
|
neuper@37950
|
1156 |
val sort_varList = sort var_ord;
|
neuper@37950
|
1157 |
|
neuper@37950
|
1158 |
(* Entfernet aeussersten Operator (Wurzel) aus einem Term und schreibt
|
neuper@37950
|
1159 |
Argumente in eine Liste *)
|
neuper@37950
|
1160 |
fun args u : term list =
|
neuper@37950
|
1161 |
let fun stripc (f$t, ts) = stripc (f, t::ts)
|
neuper@37950
|
1162 |
| stripc (t as Free _, ts) = (t::ts)
|
neuper@37950
|
1163 |
| stripc (_, ts) = ts
|
neuper@37950
|
1164 |
in stripc (u, []) end;
|
neuper@37950
|
1165 |
|
neuper@37950
|
1166 |
(* liefert True, falls der Term (Liste von Termen) nur Zahlen
|
neuper@37950
|
1167 |
(keine Variablen) enthaelt *)
|
neuper@37950
|
1168 |
fun filter_num [] = true
|
wneuper@59389
|
1169 |
| filter_num [Free x] = if (TermC.is_num (Free x)) then true
|
neuper@37950
|
1170 |
else false
|
neuper@37950
|
1171 |
| filter_num ((Free _)::_) = false
|
neuper@37950
|
1172 |
| filter_num ts =
|
wneuper@59389
|
1173 |
(filter_num o (filter_out TermC.is_num) o flat o (map args)) ts;
|
neuper@37950
|
1174 |
|
neuper@37950
|
1175 |
(* liefert True, falls der Term nur Zahlen (keine Variablen) enthaelt
|
neuper@37950
|
1176 |
dh. er ist ein numerischer Wert und entspricht einem Koeffizienten *)
|
neuper@37950
|
1177 |
fun is_nums t = filter_num [t];
|
neuper@37950
|
1178 |
|
neuper@37950
|
1179 |
(* Berechnet den Gesamtgrad eines Monoms *)
|
neuper@37950
|
1180 |
local
|
neuper@37950
|
1181 |
fun counter (n, []) = n
|
neuper@37950
|
1182 |
| counter (n, x :: xs) =
|
neuper@37950
|
1183 |
if (is_nums x) then
|
neuper@37950
|
1184 |
counter (n, xs)
|
neuper@37950
|
1185 |
else
|
neuper@37950
|
1186 |
(case x of
|
neuper@37950
|
1187 |
(Const ("Atools.pow", _) $ Free (str_b, _) $ Free (str_h, T)) =>
|
neuper@37950
|
1188 |
if (is_nums (Free (str_h, T))) then
|
wneuper@59390
|
1189 |
counter (n + (the (TermC.int_of_str_opt str_h)), xs)
|
neuper@37950
|
1190 |
else counter (n + 1000, xs) (*FIXME.MG?!*)
|
neuper@37950
|
1191 |
| (Const ("Atools.pow", _) $ Free (str_b, _) $ _ ) =>
|
neuper@37950
|
1192 |
counter (n + 1000, xs) (*FIXME.MG?!*)
|
neuper@37950
|
1193 |
| (Free (str, _)) => counter (n + 1, xs)
|
wneuper@59416
|
1194 |
(*| _ => error("monom_degree: called with factor: "^(Rule.term2str x)))*)
|
neuper@37950
|
1195 |
| _ => counter (n + 10000, xs)) (*FIXME.MG?! ... Brüche ect.*)
|
neuper@37950
|
1196 |
in
|
neuper@37950
|
1197 |
fun monom_degree l = counter (0, l)
|
neuper@37980
|
1198 |
end;(*local*)
|
neuper@37950
|
1199 |
|
neuper@37950
|
1200 |
(* wie Ordnung dict_ord (lexicographische Ordnung zweier Listen, mit Vergleich
|
neuper@37950
|
1201 |
der Listen-Elemente mit elem_ord) - Elemente die Bedingung cond erfuellen,
|
neuper@37950
|
1202 |
werden jedoch dabei ignoriert (uebersprungen) *)
|
neuper@37950
|
1203 |
fun dict_cond_ord _ _ ([], []) = EQUAL
|
neuper@37950
|
1204 |
| dict_cond_ord _ _ ([], _ :: _) = LESS
|
neuper@37950
|
1205 |
| dict_cond_ord _ _ (_ :: _, []) = GREATER
|
neuper@37950
|
1206 |
| dict_cond_ord elem_ord cond (x :: xs, y :: ys) =
|
neuper@37950
|
1207 |
(case (cond x, cond y) of
|
neuper@37950
|
1208 |
(false, false) => (case elem_ord (x, y) of
|
neuper@37950
|
1209 |
EQUAL => dict_cond_ord elem_ord cond (xs, ys)
|
neuper@37950
|
1210 |
| ord => ord)
|
neuper@37950
|
1211 |
| (false, true) => dict_cond_ord elem_ord cond (x :: xs, ys)
|
neuper@37950
|
1212 |
| (true, false) => dict_cond_ord elem_ord cond (xs, y :: ys)
|
neuper@37950
|
1213 |
| (true, true) => dict_cond_ord elem_ord cond (xs, ys) );
|
neuper@37950
|
1214 |
|
neuper@37950
|
1215 |
(* Gesamtgradordnung zum Vergleich von Monomen (Liste von Variablen/Potenzen):
|
neuper@37950
|
1216 |
zuerst nach Gesamtgrad, bei gleichem Gesamtgrad lexikographisch ordnen -
|
neuper@37950
|
1217 |
dabei werden Koeffizienten ignoriert (2*3*a^^^2*4*b gilt wie a^^^2*b) *)
|
neuper@37950
|
1218 |
fun degree_ord (xs, ys) =
|
neuper@37950
|
1219 |
prod_ord int_ord (dict_cond_ord var_ord_revPow is_nums)
|
neuper@37950
|
1220 |
((monom_degree xs, xs), (monom_degree ys, ys));
|
neuper@37950
|
1221 |
|
neuper@37950
|
1222 |
fun hd_str str = substring (str, 0, 1);
|
neuper@37950
|
1223 |
fun tl_str str = substring (str, 1, (size str) - 1);
|
neuper@37950
|
1224 |
|
neuper@37950
|
1225 |
(* liefert nummerischen Koeffizienten eines Monoms oder NONE *)
|
neuper@38031
|
1226 |
fun get_koeff_of_mon [] = error("get_koeff_of_mon: called with l = []")
|
neuper@37950
|
1227 |
| get_koeff_of_mon (l as x::xs) = if is_nums x then SOME x
|
neuper@37950
|
1228 |
else NONE;
|
neuper@37950
|
1229 |
|
neuper@37950
|
1230 |
(* wandelt Koeffizient in (zum sortieren geeigneten) String um *)
|
neuper@37950
|
1231 |
fun koeff2ordStr (SOME x) = (case x of
|
neuper@37950
|
1232 |
(Free (str, T)) =>
|
neuper@37950
|
1233 |
if (hd_str str) = "-" then (tl_str str)^"0" (* 3 < -3 *)
|
neuper@37950
|
1234 |
else str
|
neuper@37950
|
1235 |
| _ => "aaa") (* "num.Ausdruck" --> gross *)
|
neuper@37950
|
1236 |
| koeff2ordStr NONE = "---"; (* "kein Koeff" --> kleinste *)
|
neuper@37950
|
1237 |
|
neuper@37950
|
1238 |
(* Order zum Vergleich von Koeffizienten (strings):
|
neuper@37950
|
1239 |
"kein Koeff" < "0" < "1" < "-1" < "2" < "-2" < ... < "num.Ausdruck" *)
|
neuper@37950
|
1240 |
fun compare_koeff_ord (xs, ys) =
|
neuper@37950
|
1241 |
string_ord ((koeff2ordStr o get_koeff_of_mon) xs,
|
neuper@37950
|
1242 |
(koeff2ordStr o get_koeff_of_mon) ys);
|
neuper@37950
|
1243 |
|
neuper@37950
|
1244 |
(* Gesamtgradordnung degree_ord + Ordnen nach Koeffizienten falls EQUAL *)
|
neuper@37950
|
1245 |
fun koeff_degree_ord (xs, ys) =
|
neuper@37950
|
1246 |
prod_ord degree_ord compare_koeff_ord ((xs, xs), (ys, ys));
|
neuper@37950
|
1247 |
|
neuper@37950
|
1248 |
(* Ordnet ein Liste von Monomen (Monom = Liste von Variablen) mittels
|
neuper@37950
|
1249 |
Gesamtgradordnung *)
|
neuper@37950
|
1250 |
val sort_monList = sort koeff_degree_ord;
|
neuper@37950
|
1251 |
|
neuper@37950
|
1252 |
(* Alternativ zu degree_ord koennte auch die viel einfachere und
|
neuper@37950
|
1253 |
kuerzere Ordnung simple_ord verwendet werden - ist aber nicht
|
neuper@37950
|
1254 |
fuer unsere Zwecke geeignet!
|
neuper@37950
|
1255 |
|
neuper@37950
|
1256 |
fun simple_ord (al,bl: term list) = dict_ord string_ord
|
neuper@37950
|
1257 |
(map get_basStr al, map get_basStr bl);
|
neuper@37950
|
1258 |
|
neuper@37950
|
1259 |
val sort_monList = sort simple_ord; *)
|
neuper@37950
|
1260 |
|
neuper@37950
|
1261 |
(* aus 2 Variablen wird eine Summe bzw ein Produkt erzeugt
|
neuper@37950
|
1262 |
(mit gewuenschtem Typen T) *)
|
neuper@38014
|
1263 |
fun plus T = Const ("Groups.plus_class.plus", [T,T] ---> T);
|
neuper@38034
|
1264 |
fun mult T = Const ("Groups.times_class.times", [T,T] ---> T);
|
neuper@37950
|
1265 |
fun binop op_ t1 t2 = op_ $ t1 $ t2;
|
neuper@37950
|
1266 |
fun create_prod T (a,b) = binop (mult T) a b;
|
neuper@37950
|
1267 |
fun create_sum T (a,b) = binop (plus T) a b;
|
neuper@37950
|
1268 |
|
neuper@37950
|
1269 |
(* löscht letztes Element einer Liste *)
|
neuper@37950
|
1270 |
fun drop_last l = take ((length l)-1,l);
|
neuper@37950
|
1271 |
|
neuper@37950
|
1272 |
(* Liste von Variablen --> Monom *)
|
neuper@37950
|
1273 |
fun create_monom T vl = foldr (create_prod T) (drop_last vl, last_elem vl);
|
neuper@37950
|
1274 |
(* Bemerkung:
|
neuper@37950
|
1275 |
foldr bewirkt rechtslastige Klammerung des Monoms - ist notwendig, damit zwei
|
neuper@37950
|
1276 |
gleiche Monome zusammengefasst werden können (collect_numerals)!
|
neuper@37950
|
1277 |
zB: 2*(x*(y*z)) + 3*(x*(y*z)) --> (2+3)*(x*(y*z))*)
|
neuper@37950
|
1278 |
|
neuper@37950
|
1279 |
(* Liste von Monomen --> Polynom *)
|
neuper@37950
|
1280 |
fun create_polynom T ml = foldl (create_sum T) (hd ml, tl ml);
|
neuper@37950
|
1281 |
(* Bemerkung:
|
neuper@37950
|
1282 |
foldl bewirkt linkslastige Klammerung des Polynoms (der Summanten) -
|
neuper@37950
|
1283 |
bessere Darstellung, da keine Klammern sichtbar!
|
neuper@37950
|
1284 |
(und discard_parentheses in make_polynomial hat weniger zu tun) *)
|
neuper@37950
|
1285 |
|
neuper@37950
|
1286 |
(* sorts the variables (faktors) of an expanded polynomial lexicographical *)
|
neuper@37950
|
1287 |
fun sort_variables t =
|
neuper@37950
|
1288 |
let
|
neuper@37950
|
1289 |
val ll = map monom2list (poly2list t);
|
neuper@37950
|
1290 |
val lls = map sort_varList ll;
|
neuper@37950
|
1291 |
val T = type_of t;
|
neuper@37950
|
1292 |
val ls = map (create_monom T) lls;
|
neuper@37950
|
1293 |
in create_polynom T ls end;
|
neuper@37950
|
1294 |
|
neuper@37950
|
1295 |
(* sorts the monoms of an expanded and variable-sorted polynomial
|
neuper@37950
|
1296 |
by total_degree *)
|
neuper@37950
|
1297 |
fun sort_monoms t =
|
neuper@37950
|
1298 |
let
|
neuper@37950
|
1299 |
val ll = map monom2list (poly2list t);
|
neuper@37950
|
1300 |
val lls = sort_monList ll;
|
neuper@37950
|
1301 |
val T = type_of t;
|
neuper@37950
|
1302 |
val ls = map (create_monom T) lls;
|
neuper@37950
|
1303 |
in create_polynom T ls end;
|
neuper@37950
|
1304 |
|
neuper@37950
|
1305 |
(* auch Klammerung muss übereinstimmen;
|
neuper@37950
|
1306 |
sort_variables klammert Produkte rechtslastig*)
|
neuper@37950
|
1307 |
fun is_multUnordered t = ((is_polyexp t) andalso not (t = sort_variables t));
|
neuper@37950
|
1308 |
|
neuper@42451
|
1309 |
*}
|
neuper@42451
|
1310 |
ML {*
|
neuper@37950
|
1311 |
fun eval_is_multUnordered (thmid:string) _
|
neuper@37950
|
1312 |
(t as (Const("Poly.is'_multUnordered", _) $ arg)) thy =
|
neuper@37950
|
1313 |
if is_multUnordered arg
|
wneuper@59416
|
1314 |
then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
|
wneuper@59390
|
1315 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
wneuper@59416
|
1316 |
else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
|
wneuper@59390
|
1317 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
neuper@37950
|
1318 |
| eval_is_multUnordered _ _ _ _ = NONE;
|
neuper@37950
|
1319 |
|
wneuper@59416
|
1320 |
fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
|
wneuper@59416
|
1321 |
[]:(Rule.rule * (term * term list)) list;
|
wneuper@59416
|
1322 |
fun init_state (_: term) = Rule.e_rrlsstate;
|
wneuper@59416
|
1323 |
fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
|
wneuper@59416
|
1324 |
([]:(Rule.rule * (term * term list)) list);
|
wneuper@59416
|
1325 |
fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
|
wneuper@59406
|
1326 |
fun normal_form t = SOME (sort_variables t, []: term list);
|
neuper@37950
|
1327 |
|
neuper@37950
|
1328 |
val order_mult_ =
|
wneuper@59416
|
1329 |
Rule.Rrls {id = "order_mult_",
|
neuper@37950
|
1330 |
prepat =
|
neuper@38036
|
1331 |
(* ?p matched with the current term gives an environment,
|
neuper@38037
|
1332 |
which evaluates (the instantiated) "?p is_multUnordered" to true *)
|
wneuper@59389
|
1333 |
[([TermC.parse_patt thy "?p is_multUnordered"],
|
wneuper@59389
|
1334 |
TermC.parse_patt thy "?p :: real")],
|
wneuper@59416
|
1335 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1336 |
erls = Rule.append_rls "Rule.e_rls-is_multUnordered" Rule.e_rls
|
wneuper@59416
|
1337 |
[Rule.Calc ("Poly.is'_multUnordered",
|
neuper@37976
|
1338 |
eval_is_multUnordered "")],
|
neuper@38036
|
1339 |
calc = [("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38036
|
1340 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
wneuper@59360
|
1341 |
("DIVIDE", ("Rings.divide_class.divide",
|
neuper@38036
|
1342 |
eval_cancel "#divide_e")),
|
neuper@37976
|
1343 |
("POWER" , ("Atools.pow", eval_binop "#power_"))],
|
wneuper@59406
|
1344 |
errpatts = [],
|
wneuper@59416
|
1345 |
scr = Rule.Rfuns {init_state = init_state,
|
neuper@37950
|
1346 |
normal_form = normal_form,
|
neuper@37950
|
1347 |
locate_rule = locate_rule,
|
neuper@37950
|
1348 |
next_rule = next_rule,
|
neuper@37950
|
1349 |
attach_form = attach_form}};
|
neuper@37950
|
1350 |
val order_mult_rls_ =
|
wneuper@59416
|
1351 |
Rule.Rls {id = "order_mult_rls_", preconds = [],
|
wneuper@59416
|
1352 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1353 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
1354 |
calc = [], errpatts = [],
|
wneuper@59416
|
1355 |
rules = [Rule.Rls_ order_mult_
|
wneuper@59416
|
1356 |
], scr = Rule.EmptyScr};
|
neuper@42451
|
1357 |
*}
|
neuper@42451
|
1358 |
ML {*
|
neuper@37950
|
1359 |
|
neuper@37950
|
1360 |
fun is_addUnordered t = ((is_polyexp t) andalso not (t = sort_monoms t));
|
neuper@37950
|
1361 |
|
neuper@37950
|
1362 |
(*WN.18.6.03 *)
|
neuper@37950
|
1363 |
(*("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))*)
|
neuper@37950
|
1364 |
fun eval_is_addUnordered (thmid:string) _
|
neuper@37950
|
1365 |
(t as (Const("Poly.is'_addUnordered", _) $ arg)) thy =
|
neuper@37950
|
1366 |
if is_addUnordered arg
|
wneuper@59416
|
1367 |
then SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
|
wneuper@59390
|
1368 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
|
wneuper@59416
|
1369 |
else SOME (TermC.mk_thmid thmid (Rule.term_to_string''' thy arg) "",
|
wneuper@59390
|
1370 |
HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
|
neuper@37950
|
1371 |
| eval_is_addUnordered _ _ _ _ = NONE;
|
neuper@37950
|
1372 |
|
wneuper@59416
|
1373 |
fun attach_form (_: Rule.rule list list) (_: term) (_: term) = (*still missing*)
|
wneuper@59416
|
1374 |
[]: (Rule.rule * (term * term list)) list;
|
wneuper@59416
|
1375 |
fun init_state (_: term) = Rule.e_rrlsstate;
|
wneuper@59416
|
1376 |
fun locate_rule (_: Rule.rule list list) (_: term) (_: Rule.rule) =
|
wneuper@59416
|
1377 |
([]: (Rule.rule * (term * term list)) list);
|
wneuper@59416
|
1378 |
fun next_rule (_: Rule.rule list list) (_: term) = (NONE: Rule.rule option);
|
wneuper@59406
|
1379 |
fun normal_form t = SOME (sort_monoms t,[]: term list);
|
neuper@37950
|
1380 |
|
wneuper@59406
|
1381 |
*} ML {*
|
neuper@37950
|
1382 |
val order_add_ =
|
wneuper@59416
|
1383 |
Rule.Rrls {id = "order_add_",
|
neuper@37950
|
1384 |
prepat = (*WN.18.6.03 Preconditions und Pattern,
|
wneuper@59416
|
1385 |
die beide passen muessen, damit das Rule.Rrls angewandt wird*)
|
wneuper@59389
|
1386 |
[([TermC.parse_patt @{theory} "?p is_addUnordered"],
|
wneuper@59389
|
1387 |
TermC.parse_patt @{theory} "?p :: real"
|
neuper@37950
|
1388 |
(*WN.18.6.03 also KEIN pattern, dieses erzeugt nur das Environment
|
neuper@37950
|
1389 |
fuer die Evaluation der Precondition "p is_addUnordered"*))],
|
wneuper@59416
|
1390 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1391 |
erls = Rule.append_rls "Rule.e_rls-is_addUnordered" Rule.e_rls(*MG: poly_erls*)
|
wneuper@59416
|
1392 |
[Rule.Calc ("Poly.is'_addUnordered",
|
neuper@38037
|
1393 |
eval_is_addUnordered "")],
|
neuper@38037
|
1394 |
calc = [("PLUS" ,("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38037
|
1395 |
("TIMES" ,("Groups.times_class.times", eval_binop "#mult_")),
|
wneuper@59360
|
1396 |
("DIVIDE",("Rings.divide_class.divide",
|
neuper@38037
|
1397 |
eval_cancel "#divide_e")),
|
neuper@38037
|
1398 |
("POWER" ,("Atools.pow" ,eval_binop "#power_"))],
|
neuper@42451
|
1399 |
errpatts = [],
|
wneuper@59416
|
1400 |
scr = Rule.Rfuns {init_state = init_state,
|
neuper@37950
|
1401 |
normal_form = normal_form,
|
neuper@37950
|
1402 |
locate_rule = locate_rule,
|
neuper@37950
|
1403 |
next_rule = next_rule,
|
neuper@37950
|
1404 |
attach_form = attach_form}};
|
neuper@37950
|
1405 |
|
wneuper@59406
|
1406 |
val order_add_rls_ =
|
wneuper@59416
|
1407 |
Rule.Rls {id = "order_add_rls_", preconds = [],
|
wneuper@59416
|
1408 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1409 |
erls = Rule.e_rls,srls = Rule.Erls,
|
neuper@42451
|
1410 |
calc = [], errpatts = [],
|
wneuper@59416
|
1411 |
rules = [Rule.Rls_ order_add_
|
wneuper@59416
|
1412 |
], scr = Rule.EmptyScr};
|
neuper@42398
|
1413 |
*}
|
neuper@37950
|
1414 |
|
neuper@42398
|
1415 |
text {* rule-set make_polynomial also named norm_Poly:
|
neuper@42398
|
1416 |
Rewrite order has not been implemented properly; the order is better in
|
neuper@42398
|
1417 |
make_polynomial_in (coded in SML).
|
neuper@42398
|
1418 |
Notes on state of development:
|
neuper@42398
|
1419 |
\# surprise 2006: test --- norm_Poly NOT COMPLETE ---
|
neuper@42398
|
1420 |
\# migration Isabelle2002 --> 2011 weakened the rule set, see test
|
neuper@42398
|
1421 |
--- Matthias Goldgruber 2003 rewrite orders ---, error "ord_make_polynomial_in #16b"
|
neuper@42398
|
1422 |
*}
|
neuper@42398
|
1423 |
ML {*
|
neuper@37950
|
1424 |
(*. see MG-DA.p.52ff .*)
|
neuper@37950
|
1425 |
val make_polynomial(*MG.03, overwrites version from above,
|
neuper@37950
|
1426 |
previously 'make_polynomial_'*) =
|
wneuper@59416
|
1427 |
Rule.Seq {id = "make_polynomial", preconds = []:term list,
|
wneuper@59416
|
1428 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1429 |
erls = Atools_erls, srls = Rule.Erls,calc = [], errpatts = [],
|
wneuper@59416
|
1430 |
rules = [Rule.Rls_ discard_minus,
|
wneuper@59416
|
1431 |
Rule.Rls_ expand_poly_,
|
wneuper@59416
|
1432 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1433 |
Rule.Rls_ order_mult_rls_,
|
wneuper@59416
|
1434 |
Rule.Rls_ simplify_power_,
|
wneuper@59416
|
1435 |
Rule.Rls_ calc_add_mult_pow_,
|
wneuper@59416
|
1436 |
Rule.Rls_ reduce_012_mult_,
|
wneuper@59416
|
1437 |
Rule.Rls_ order_add_rls_,
|
wneuper@59416
|
1438 |
Rule.Rls_ collect_numerals_,
|
wneuper@59416
|
1439 |
Rule.Rls_ reduce_012_,
|
wneuper@59416
|
1440 |
Rule.Rls_ discard_parentheses1
|
neuper@37950
|
1441 |
],
|
wneuper@59416
|
1442 |
scr = Rule.EmptyScr
|
wneuper@59406
|
1443 |
};
|
neuper@48763
|
1444 |
*}
|
neuper@48763
|
1445 |
ML {*
|
neuper@37950
|
1446 |
val norm_Poly(*=make_polynomial*) =
|
wneuper@59416
|
1447 |
Rule.Seq {id = "norm_Poly", preconds = []:term list,
|
wneuper@59416
|
1448 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1449 |
erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
|
wneuper@59416
|
1450 |
rules = [Rule.Rls_ discard_minus,
|
wneuper@59416
|
1451 |
Rule.Rls_ expand_poly_,
|
wneuper@59416
|
1452 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1453 |
Rule.Rls_ order_mult_rls_,
|
wneuper@59416
|
1454 |
Rule.Rls_ simplify_power_,
|
wneuper@59416
|
1455 |
Rule.Rls_ calc_add_mult_pow_,
|
wneuper@59416
|
1456 |
Rule.Rls_ reduce_012_mult_,
|
wneuper@59416
|
1457 |
Rule.Rls_ order_add_rls_,
|
wneuper@59416
|
1458 |
Rule.Rls_ collect_numerals_,
|
wneuper@59416
|
1459 |
Rule.Rls_ reduce_012_,
|
wneuper@59416
|
1460 |
Rule.Rls_ discard_parentheses1
|
neuper@37950
|
1461 |
],
|
wneuper@59416
|
1462 |
scr = Rule.EmptyScr
|
wneuper@59406
|
1463 |
};
|
neuper@48763
|
1464 |
*}
|
neuper@48763
|
1465 |
ML {*
|
wneuper@59416
|
1466 |
(* MG:03 Like make_polynomial_ but without Rule.Rls_ discard_parentheses1
|
neuper@37950
|
1467 |
and expand_poly_rat_ instead of expand_poly_, see MG-DA.p.56ff*)
|
neuper@37950
|
1468 |
(* MG necessary for termination of norm_Rational(*_mg*) in Rational.ML*)
|
neuper@37950
|
1469 |
val make_rat_poly_with_parentheses =
|
wneuper@59416
|
1470 |
Rule.Seq{id = "make_rat_poly_with_parentheses", preconds = []:term list,
|
wneuper@59416
|
1471 |
rew_ord = ("dummy_ord", Rule.dummy_ord),
|
wneuper@59416
|
1472 |
erls = Atools_erls, srls = Rule.Erls, calc = [], errpatts = [],
|
wneuper@59416
|
1473 |
rules = [Rule.Rls_ discard_minus,
|
wneuper@59416
|
1474 |
Rule.Rls_ expand_poly_rat_,(*ignors rationals*)
|
wneuper@59416
|
1475 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1476 |
Rule.Rls_ order_mult_rls_,
|
wneuper@59416
|
1477 |
Rule.Rls_ simplify_power_,
|
wneuper@59416
|
1478 |
Rule.Rls_ calc_add_mult_pow_,
|
wneuper@59416
|
1479 |
Rule.Rls_ reduce_012_mult_,
|
wneuper@59416
|
1480 |
Rule.Rls_ order_add_rls_,
|
wneuper@59416
|
1481 |
Rule.Rls_ collect_numerals_,
|
wneuper@59416
|
1482 |
Rule.Rls_ reduce_012_
|
wneuper@59416
|
1483 |
(*Rule.Rls_ discard_parentheses1 *)
|
neuper@37950
|
1484 |
],
|
wneuper@59416
|
1485 |
scr = Rule.EmptyScr
|
wneuper@59406
|
1486 |
};
|
neuper@48763
|
1487 |
*}
|
neuper@48763
|
1488 |
ML {*
|
neuper@37950
|
1489 |
(*.a minimal ruleset for reverse rewriting of factions [2];
|
neuper@37950
|
1490 |
compare expand_binoms.*)
|
neuper@37950
|
1491 |
val rev_rew_p =
|
wneuper@59416
|
1492 |
Rule.Seq{id = "rev_rew_p", preconds = [], rew_ord = ("termlessI",termlessI),
|
wneuper@59416
|
1493 |
erls = Atools_erls, srls = Rule.Erls,
|
neuper@38014
|
1494 |
calc = [(*("PLUS" , ("Groups.plus_class.plus", eval_binop "#add_")),
|
neuper@38034
|
1495 |
("TIMES" , ("Groups.times_class.times", eval_binop "#mult_")),
|
neuper@37950
|
1496 |
("POWER", ("Atools.pow", eval_binop "#power_"))*)
|
neuper@42451
|
1497 |
], errpatts = [],
|
wneuper@59416
|
1498 |
rules = [Rule.Thm ("real_plus_binom_times" ,TermC.num_str @{thm real_plus_binom_times}),
|
neuper@37950
|
1499 |
(*"(a + b)*(a + b) = a ^ 2 + 2 * a * b + b ^ 2*)
|
wneuper@59416
|
1500 |
Rule.Thm ("real_plus_binom_times1" ,TermC.num_str @{thm real_plus_binom_times1}),
|
neuper@37950
|
1501 |
(*"(a + 1*b)*(a + -1*b) = a^^^2 + -1*b^^^2"*)
|
wneuper@59416
|
1502 |
Rule.Thm ("real_plus_binom_times2" ,TermC.num_str @{thm real_plus_binom_times2}),
|
neuper@37950
|
1503 |
(*"(a + -1*b)*(a + 1*b) = a^^^2 + -1*b^^^2"*)
|
neuper@37950
|
1504 |
|
wneuper@59416
|
1505 |
Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
|
neuper@37950
|
1506 |
|
wneuper@59416
|
1507 |
Rule.Thm ("distrib_right" ,TermC.num_str @{thm distrib_right}),
|
neuper@37950
|
1508 |
(*"(z1.0 + z2.0) * w = z1.0 * w + z2.0 * w"*)
|
wneuper@59416
|
1509 |
Rule.Thm ("distrib_left",TermC.num_str @{thm distrib_left}),
|
neuper@37950
|
1510 |
(*"w * (z1.0 + z2.0) = w * z1.0 + w * z2.0"*)
|
neuper@37950
|
1511 |
|
wneuper@59416
|
1512 |
Rule.Thm ("mult_assoc", TermC.num_str @{thm mult.assoc}),
|
neuper@37950
|
1513 |
(*"?z1.1 * ?z2.1 * ?z3. =1 ?z1.1 * (?z2.1 * ?z3.1)"*)
|
wneuper@59416
|
1514 |
Rule.Rls_ order_mult_rls_,
|
wneuper@59416
|
1515 |
(*Rule.Rls_ order_add_rls_,*)
|
neuper@37950
|
1516 |
|
wneuper@59416
|
1517 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
1518 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1519 |
Rule.Calc ("Atools.pow", eval_binop "#power_"),
|
neuper@37950
|
1520 |
|
wneuper@59416
|
1521 |
Rule.Thm ("sym_realpow_twoI",
|
wneuper@59389
|
1522 |
TermC.num_str (@{thm realpow_twoI} RS @{thm sym})),
|
neuper@37950
|
1523 |
(*"r1 * r1 = r1 ^^^ 2"*)
|
wneuper@59416
|
1524 |
Rule.Thm ("sym_real_mult_2",
|
wneuper@59389
|
1525 |
TermC.num_str (@{thm real_mult_2} RS @{thm sym})),
|
neuper@37950
|
1526 |
(*"z1 + z1 = 2 * z1"*)
|
wneuper@59416
|
1527 |
Rule.Thm ("real_mult_2_assoc",TermC.num_str @{thm real_mult_2_assoc}),
|
neuper@37950
|
1528 |
(*"z1 + (z1 + k) = 2 * z1 + k"*)
|
neuper@37950
|
1529 |
|
wneuper@59416
|
1530 |
Rule.Thm ("real_num_collect",TermC.num_str @{thm real_num_collect}),
|
neuper@37950
|
1531 |
(*"[| l is_const; m is_const |]==>l * n + m * n = (l + m) * n"*)
|
wneuper@59416
|
1532 |
Rule.Thm ("real_num_collect_assoc",TermC.num_str @{thm real_num_collect_assoc}),
|
neuper@37950
|
1533 |
(*"[| l is_const; m is_const |] ==>
|
neuper@37950
|
1534 |
l * n + (m * n + k) = (l + m) * n + k"*)
|
wneuper@59416
|
1535 |
Rule.Thm ("real_one_collect",TermC.num_str @{thm real_one_collect}),
|
neuper@37950
|
1536 |
(*"m is_const ==> n + m * n = (1 + m) * n"*)
|
wneuper@59416
|
1537 |
Rule.Thm ("real_one_collect_assoc",TermC.num_str @{thm real_one_collect_assoc}),
|
neuper@37950
|
1538 |
(*"m is_const ==> k + (n + m * n) = k + (1 + m) * n"*)
|
neuper@37950
|
1539 |
|
wneuper@59416
|
1540 |
Rule.Thm ("realpow_multI", TermC.num_str @{thm realpow_multI}),
|
neuper@37950
|
1541 |
(*"(r * s) ^^^ n = r ^^^ n * s ^^^ n"*)
|
neuper@37950
|
1542 |
|
wneuper@59416
|
1543 |
Rule.Calc ("Groups.plus_class.plus", eval_binop "#add_"),
|
wneuper@59416
|
1544 |
Rule.Calc ("Groups.times_class.times", eval_binop "#mult_"),
|
wneuper@59416
|
1545 |
Rule.Calc ("Atools.pow", eval_binop "#power_"),
|
neuper@37950
|
1546 |
|
wneuper@59416
|
1547 |
Rule.Thm ("mult_1_left",TermC.num_str @{thm mult_1_left}),(*"1 * z = z"*)
|
wneuper@59416
|
1548 |
Rule.Thm ("mult_zero_left",TermC.num_str @{thm mult_zero_left}),(*"0 * z = 0"*)
|
wneuper@59416
|
1549 |
Rule.Thm ("add_0_left",TermC.num_str @{thm add_0_left})(*0 + z = z*)
|
neuper@37950
|
1550 |
|
wneuper@59416
|
1551 |
(*Rule.Rls_ order_add_rls_*)
|
neuper@37950
|
1552 |
],
|
neuper@37950
|
1553 |
|
wneuper@59416
|
1554 |
scr = Rule.EmptyScr};
|
neuper@48763
|
1555 |
*}
|
neuper@52125
|
1556 |
|
wneuper@59374
|
1557 |
ML {* val prep_rls' = LTool.prep_rls @{theory} *}
|
s1210629013@55444
|
1558 |
|
neuper@52125
|
1559 |
setup {* KEStore_Elems.add_rlss
|
s1210629013@55444
|
1560 |
[("norm_Poly", (Context.theory_name @{theory}, prep_rls' norm_Poly)),
|
s1210629013@55444
|
1561 |
("Poly_erls", (Context.theory_name @{theory}, prep_rls' Poly_erls)),(*FIXXXME:del with rls.rls'*)
|
s1210629013@55444
|
1562 |
("expand", (Context.theory_name @{theory}, prep_rls' expand)),
|
s1210629013@55444
|
1563 |
("expand_poly", (Context.theory_name @{theory}, prep_rls' expand_poly)),
|
s1210629013@55444
|
1564 |
("simplify_power", (Context.theory_name @{theory}, prep_rls' simplify_power)),
|
neuper@52125
|
1565 |
|
s1210629013@55444
|
1566 |
("order_add_mult", (Context.theory_name @{theory}, prep_rls' order_add_mult)),
|
s1210629013@55444
|
1567 |
("collect_numerals", (Context.theory_name @{theory}, prep_rls' collect_numerals)),
|
s1210629013@55444
|
1568 |
("collect_numerals_", (Context.theory_name @{theory}, prep_rls' collect_numerals_)),
|
s1210629013@55444
|
1569 |
("reduce_012", (Context.theory_name @{theory}, prep_rls' reduce_012)),
|
s1210629013@55444
|
1570 |
("discard_parentheses", (Context.theory_name @{theory}, prep_rls' discard_parentheses)),
|
neuper@52125
|
1571 |
|
s1210629013@55444
|
1572 |
("make_polynomial", (Context.theory_name @{theory}, prep_rls' make_polynomial)),
|
s1210629013@55444
|
1573 |
("expand_binoms", (Context.theory_name @{theory}, prep_rls' expand_binoms)),
|
s1210629013@55444
|
1574 |
("rev_rew_p", (Context.theory_name @{theory}, prep_rls' rev_rew_p)),
|
s1210629013@55444
|
1575 |
("discard_minus", (Context.theory_name @{theory}, prep_rls' discard_minus)),
|
s1210629013@55444
|
1576 |
("expand_poly_", (Context.theory_name @{theory}, prep_rls' expand_poly_)),
|
neuper@52125
|
1577 |
|
s1210629013@55444
|
1578 |
("expand_poly_rat_", (Context.theory_name @{theory}, prep_rls' expand_poly_rat_)),
|
s1210629013@55444
|
1579 |
("simplify_power_", (Context.theory_name @{theory}, prep_rls' simplify_power_)),
|
s1210629013@55444
|
1580 |
("calc_add_mult_pow_", (Context.theory_name @{theory}, prep_rls' calc_add_mult_pow_)),
|
s1210629013@55444
|
1581 |
("reduce_012_mult_", (Context.theory_name @{theory}, prep_rls' reduce_012_mult_)),
|
s1210629013@55444
|
1582 |
("reduce_012_", (Context.theory_name @{theory}, prep_rls' reduce_012_)),
|
neuper@52125
|
1583 |
|
s1210629013@55444
|
1584 |
("discard_parentheses1", (Context.theory_name @{theory}, prep_rls' discard_parentheses1)),
|
s1210629013@55444
|
1585 |
("order_mult_rls_", (Context.theory_name @{theory}, prep_rls' order_mult_rls_)),
|
s1210629013@55444
|
1586 |
("order_add_rls_", (Context.theory_name @{theory}, prep_rls' order_add_rls_)),
|
neuper@52125
|
1587 |
("make_rat_poly_with_parentheses",
|
s1210629013@55444
|
1588 |
(Context.theory_name @{theory}, prep_rls' make_rat_poly_with_parentheses))] *}
|
s1210629013@52145
|
1589 |
setup {* KEStore_Elems.add_calcs
|
s1210629013@52145
|
1590 |
[("is_polyrat_in", ("Poly.is'_polyrat'_in",
|
s1210629013@52145
|
1591 |
eval_is_polyrat_in "#eval_is_polyrat_in")),
|
s1210629013@52145
|
1592 |
("is_expanded_in", ("Poly.is'_expanded'_in", eval_is_expanded_in "")),
|
s1210629013@52145
|
1593 |
("is_poly_in", ("Poly.is'_poly'_in", eval_is_poly_in "")),
|
s1210629013@52145
|
1594 |
("has_degree_in", ("Poly.has'_degree'_in", eval_has_degree_in "")),
|
s1210629013@52145
|
1595 |
("is_polyexp", ("Poly.is'_polyexp", eval_is_polyexp "")),
|
s1210629013@52145
|
1596 |
("is_multUnordered", ("Poly.is'_multUnordered", eval_is_multUnordered"")),
|
s1210629013@52145
|
1597 |
("is_addUnordered", ("Poly.is'_addUnordered", eval_is_addUnordered ""))] *}
|
s1210629013@52145
|
1598 |
|
neuper@37950
|
1599 |
(** problems **)
|
s1210629013@55359
|
1600 |
setup {* KEStore_Elems.add_pbts
|
wneuper@59406
|
1601 |
[(Specify.prep_pbt thy "pbl_simp_poly" [] Celem.e_pblID
|
s1210629013@55339
|
1602 |
(["polynomial","simplification"],
|
s1210629013@55339
|
1603 |
[("#Given" ,["Term t_t"]),
|
s1210629013@55339
|
1604 |
("#Where" ,["t_t is_polyexp"]),
|
s1210629013@55339
|
1605 |
("#Find" ,["normalform n_n"])],
|
wneuper@59416
|
1606 |
Rule.append_rls "e_rls" Rule.e_rls [(*for preds in where_*)
|
wneuper@59416
|
1607 |
Rule.Calc ("Poly.is'_polyexp", eval_is_polyexp "")],
|
s1210629013@55339
|
1608 |
SOME "Simplify t_t",
|
s1210629013@55339
|
1609 |
[["simplification","for_polynomials"]]))] *}
|
wneuper@59429
|
1610 |
|
neuper@37950
|
1611 |
(** methods **)
|
wneuper@59429
|
1612 |
(*-----
|
wneuper@59429
|
1613 |
consts
|
wneuper@59429
|
1614 |
norm_Poly :: ID
|
wneuper@59429
|
1615 |
partial_function (tailrec) simplify :: "real \<Rightarrow> real"
|
wneuper@59429
|
1616 |
where
|
wneuper@59429
|
1617 |
"simplify term = ((Rewrite_Set norm_Poly False) term)"
|
wneuper@59429
|
1618 |
|
wneuper@59429
|
1619 |
-----*)
|
s1210629013@55373
|
1620 |
setup {* KEStore_Elems.add_mets
|
wneuper@59406
|
1621 |
[Specify.prep_met thy "met_simp_poly" [] Celem.e_metID
|
s1210629013@55373
|
1622 |
(["simplification","for_polynomials"],
|
s1210629013@55373
|
1623 |
[("#Given" ,["Term t_t"]),
|
s1210629013@55373
|
1624 |
("#Where" ,["t_t is_polyexp"]),
|
s1210629013@55373
|
1625 |
("#Find" ,["normalform n_n"])],
|
wneuper@59416
|
1626 |
{rew_ord'="tless_true", rls' = Rule.e_rls, calc = [], srls = Rule.e_rls,
|
wneuper@59416
|
1627 |
prls = Rule.append_rls "simplification_for_polynomials_prls" Rule.e_rls
|
s1210629013@55373
|
1628 |
[(*for preds in where_*)
|
wneuper@59416
|
1629 |
Rule.Calc ("Poly.is'_polyexp",eval_is_polyexp"")],
|
wneuper@59416
|
1630 |
crls = Rule.e_rls, errpats = [], nrls = norm_Poly},
|
s1210629013@55373
|
1631 |
"Script SimplifyScript (t_t::real) = " ^
|
s1210629013@55373
|
1632 |
" ((Rewrite_Set norm_Poly False) t_t)")]
|
s1210629013@55373
|
1633 |
*}
|
neuper@37950
|
1634 |
|
wneuper@59429
|
1635 |
ML {*
|
wneuper@59429
|
1636 |
*} ML {*
|
wneuper@59429
|
1637 |
*}
|
neuper@37906
|
1638 |
end
|