126 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)"; |
126 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)"; |
127 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
127 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
128 if (term2str t) = |
128 if (term2str t) = |
129 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9" |
129 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9" |
130 then () |
130 then () |
131 else raise error "poly.sml: diff.behav. in make_polynomial 1"; |
131 else error "poly.sml: diff.behav. in make_polynomial 1"; |
132 |
132 |
133 (*SPB Schalk I p.63 No.275b*) |
133 (*SPB Schalk I p.63 No.275b*) |
134 val t = str2term |
134 val t = str2term |
135 "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)"; |
135 "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)"; |
136 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
136 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
137 term2str t; |
137 term2str t; |
138 if (term2str t) = |
138 if (term2str t) = |
139 "3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \ |
139 "3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \ |
140 \4 * x * y ^^^ 3 +\n-2 * y ^^^ 4" |
140 \4 * x * y ^^^ 3 +\n-2 * y ^^^ 4" |
141 then () |
141 then () |
142 else raise error "poly.sml: diff.behav. in make_polynomial 2"; |
142 else error "poly.sml: diff.behav. in make_polynomial 2"; |
143 |
143 |
144 (*SPB Schalk I p.63 No.279b*) |
144 (*SPB Schalk I p.63 No.279b*) |
145 val t = str2term |
145 val t = str2term |
146 "(x-a)*(x-b)*(x-c)*(x-d)"; |
146 "(x-a)*(x-b)*(x-c)*(x-d)"; |
147 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
147 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
148 term2str t; |
148 term2str t; |
149 (* Richtig! *) |
149 (* Richtig! *) |
150 if (term2str t) = |
150 if (term2str t) = |
151 "a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4" |
151 "a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4" |
152 then () |
152 then () |
153 else raise error "poly.sml: diff.behav. in make_polynomial 3"; |
153 else error "poly.sml: diff.behav. in make_polynomial 3"; |
154 |
154 |
155 (*SPB Schalk I p.63 No.291*) |
155 (*SPB Schalk I p.63 No.291*) |
156 val t = str2term |
156 val t = str2term |
157 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))"; |
157 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))"; |
158 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
158 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
159 term2str t; |
159 term2str t; |
160 if (term2str t) = |
160 if (term2str t) = |
161 "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4" |
161 "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4" |
162 then () |
162 then () |
163 else raise error "poly.sml: diff.behav. in make_polynomial 4"; |
163 else error "poly.sml: diff.behav. in make_polynomial 4"; |
164 |
164 |
165 (*SPB Schalk I p.64 No.295c*) |
165 (*SPB Schalk I p.64 No.295c*) |
166 val t = str2term |
166 val t = str2term |
167 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2"; |
167 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2"; |
168 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
168 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
169 term2str t; |
169 term2str t; |
170 if (term2str t) = |
170 if (term2str t) = |
171 "169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\ |
171 "169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\ |
172 \ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18" |
172 \ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18" |
173 then () |
173 then () |
174 else raise error "poly.sml: diff.behav. in make_polynomial 5"; |
174 else error "poly.sml: diff.behav. in make_polynomial 5"; |
175 |
175 |
176 (*SPB Schalk I p.64 No.299a*) |
176 (*SPB Schalk I p.64 No.299a*) |
177 val t = str2term |
177 val t = str2term |
178 "(x - y)*(x + y)"; |
178 "(x - y)*(x + y)"; |
179 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
179 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
180 term2str t; |
180 term2str t; |
181 if (term2str t) = |
181 if (term2str t) = |
182 "x ^^^ 2 + -1 * y ^^^ 2" |
182 "x ^^^ 2 + -1 * y ^^^ 2" |
183 then () |
183 then () |
184 else raise error "poly.sml: diff.behav. in make_polynomial 6"; |
184 else error "poly.sml: diff.behav. in make_polynomial 6"; |
185 |
185 |
186 (*SPB Schalk I p.64 No.300c*) |
186 (*SPB Schalk I p.64 No.300c*) |
187 val t = str2term |
187 val t = str2term |
188 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)"; |
188 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)"; |
189 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
189 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
190 term2str t; |
190 term2str t; |
191 if (term2str t) = |
191 if (term2str t) = |
192 "-1 + 9 * x ^^^ 4 * y ^^^ 2" |
192 "-1 + 9 * x ^^^ 4 * y ^^^ 2" |
193 then () |
193 then () |
194 else raise error "poly.sml: diff.behav. in make_polynomial 7"; |
194 else error "poly.sml: diff.behav. in make_polynomial 7"; |
195 |
195 |
196 (*SPB Schalk I p.64 No.302*) |
196 (*SPB Schalk I p.64 No.302*) |
197 val t = str2term |
197 val t = str2term |
198 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)"; |
198 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)"; |
199 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
199 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
200 if term2str t = "0" then () |
200 if term2str t = "0" then () |
201 else raise error "poly.sml: diff.behav. in make_polynomial 8"; |
201 else error "poly.sml: diff.behav. in make_polynomial 8"; |
202 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *) |
202 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *) |
203 |
203 |
204 |
204 |
205 (*SPB Schalk I p.64 No.306a*) |
205 (*SPB Schalk I p.64 No.306a*) |
206 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2"; |
206 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2"; |
207 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
207 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
208 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then () |
208 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then () |
209 else raise error "poly.sml: diff.behav. in make_polynomial: not confluent \ |
209 else error "poly.sml: diff.behav. in make_polynomial: not confluent \ |
210 \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again"; |
210 \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again"; |
211 |
211 |
212 |
212 |
213 (*WN071729 when reducing "rls reduce_012_" for Schaerding, |
213 (*WN071729 when reducing "rls reduce_012_" for Schaerding, |
214 the above resulted in the term below ... but reduces from then correctly*) |
214 the above resulted in the term below ... but reduces from then correctly*) |
215 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8"; |
215 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8"; |
216 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
216 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
217 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then () |
217 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then () |
218 else raise error "poly.sml: diff.behav. in make_polynomial 9b"; |
218 else error "poly.sml: diff.behav. in make_polynomial 9b"; |
219 |
219 |
220 (*SPB Schalk I p.64 No.296a*) |
220 (*SPB Schalk I p.64 No.296a*) |
221 val t = str2term "(x - a)^^^3"; |
221 val t = str2term "(x - a)^^^3"; |
222 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
222 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
223 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3" |
223 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3" |
224 then () else raise error "poly.sml: diff.behav. in make_polynomial 10"; |
224 then () else error "poly.sml: diff.behav. in make_polynomial 10"; |
225 |
225 |
226 (*SPB Schalk I p.64 No.296c*) |
226 (*SPB Schalk I p.64 No.296c*) |
227 val t = str2term "(-3*x - 4*y)^^^3"; |
227 val t = str2term "(-3*x - 4*y)^^^3"; |
228 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
228 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
229 if (term2str t) = |
229 if (term2str t) = |
230 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3" |
230 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3" |
231 then () else raise error "poly.sml: diff.behav. in make_polynomial 11"; |
231 then () else error "poly.sml: diff.behav. in make_polynomial 11"; |
232 |
232 |
233 (*SPB Schalk I p.62 No.242c*) |
233 (*SPB Schalk I p.62 No.242c*) |
234 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)"; |
234 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)"; |
235 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
235 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
236 if (term2str t) = "1" then () |
236 if (term2str t) = "1" then () |
237 else raise error "poly.sml: diff.behav. in make_polynomial 12"; |
237 else error "poly.sml: diff.behav. in make_polynomial 12"; |
238 |
238 |
239 (*SPB Schalk I p.60 No.209a*) |
239 (*SPB Schalk I p.60 No.209a*) |
240 val t = str2term "a^^^(7-x) * a^^^x"; |
240 val t = str2term "a^^^(7-x) * a^^^x"; |
241 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
241 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
242 if term2str t = "a ^^^ 7" then () |
242 if term2str t = "a ^^^ 7" then () |
243 else raise error "poly.sml: diff.behav. in make_polynomial 13"; |
243 else error "poly.sml: diff.behav. in make_polynomial 13"; |
244 |
244 |
245 (*SPB Schalk I p.60 No.209d*) |
245 (*SPB Schalk I p.60 No.209d*) |
246 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)"; |
246 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)"; |
247 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
247 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
248 if term2str t = "d ^^^ 3" then () |
248 if term2str t = "d ^^^ 3" then () |
249 else raise error "poly.sml: diff.behav. in make_polynomial 14"; |
249 else error "poly.sml: diff.behav. in make_polynomial 14"; |
250 |
250 |
251 |
251 |
252 (*---------------------------------------------------------------------*) |
252 (*---------------------------------------------------------------------*) |
253 (*------------------ Bsple bei denen es Probleme gibt------------------*) |
253 (*------------------ Bsple bei denen es Probleme gibt------------------*) |
254 (*---------------------------------------------------------------------*) |
254 (*---------------------------------------------------------------------*) |
255 |
255 |
256 (*Schalk I p.64 No.303*) |
256 (*Schalk I p.64 No.303*) |
257 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)"; |
257 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)"; |
258 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
258 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
259 if term2str t = "1280 * b ^^^ 4" then () |
259 if term2str t = "1280 * b ^^^ 4" then () |
260 else raise error "poly.sml: diff.behav. in make_polynomial 14b"; |
260 else error "poly.sml: diff.behav. in make_polynomial 14b"; |
261 (* Richtig - aber Binomische Formel wurde nicht verwendet! *) |
261 (* Richtig - aber Binomische Formel wurde nicht verwendet! *) |
262 |
262 |
263 |
263 |
264 (*--------------------------------------------------------------------*) |
264 (*--------------------------------------------------------------------*) |
265 (*----------------------- Eigene Beispiele ---------------------------*) |
265 (*----------------------- Eigene Beispiele ---------------------------*) |
266 (*--------------------------------------------------------------------*) |
266 (*--------------------------------------------------------------------*) |
267 (*SPO*) |
267 (*SPO*) |
268 val t = str2term "a^^^2*a^^^(-2)"; |
268 val t = str2term "a^^^2*a^^^(-2)"; |
269 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
269 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
270 if term2str t = "1" then () |
270 if term2str t = "1" then () |
271 else raise error "poly.sml: diff.behav. in make_polynomial 15"; |
271 else error "poly.sml: diff.behav. in make_polynomial 15"; |
272 (*SPO*) |
272 (*SPO*) |
273 val t = str2term "a + a + a"; |
273 val t = str2term "a + a + a"; |
274 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
274 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
275 if term2str t = "3 * a" then () |
275 if term2str t = "3 * a" then () |
276 else raise error "poly.sml: diff.behav. in make_polynomial 16"; |
276 else error "poly.sml: diff.behav. in make_polynomial 16"; |
277 (*SPO*) |
277 (*SPO*) |
278 val t = str2term "a + b + b + b"; |
278 val t = str2term "a + b + b + b"; |
279 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
279 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
280 if term2str t = "a + 3 * b" then () |
280 if term2str t = "a + 3 * b" then () |
281 else raise error "poly.sml: diff.behav. in make_polynomial 17"; |
281 else error "poly.sml: diff.behav. in make_polynomial 17"; |
282 (*SPO*) |
282 (*SPO*) |
283 val t = str2term "a^^^2*b*b^^^(-1)"; |
283 val t = str2term "a^^^2*b*b^^^(-1)"; |
284 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
284 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
285 if term2str t = "a ^^^ 2" then () |
285 if term2str t = "a ^^^ 2" then () |
286 else raise error "poly.sml: diff.behav. in make_polynomial 18"; |
286 else error "poly.sml: diff.behav. in make_polynomial 18"; |
287 (*SPO*) |
287 (*SPO*) |
288 val t = str2term "a^^^2*a^^^(-2)"; |
288 val t = str2term "a^^^2*a^^^(-2)"; |
289 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
289 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
290 if (term2str t) = "1" then () |
290 if (term2str t) = "1" then () |
291 else raise error "poly.sml: diff.behav. in make_polynomial 19"; |
291 else error "poly.sml: diff.behav. in make_polynomial 19"; |
292 (*SPO*) |
292 (*SPO*) |
293 val t = str2term "b + a - b"; |
293 val t = str2term "b + a - b"; |
294 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
294 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
295 if (term2str t) = "a" then () |
295 if (term2str t) = "a" then () |
296 else raise error "poly.sml: diff.behav. in make_polynomial 20"; |
296 else error "poly.sml: diff.behav. in make_polynomial 20"; |
297 (*SPO*) |
297 (*SPO*) |
298 val t = str2term "b * a * a"; |
298 val t = str2term "b * a * a"; |
299 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
299 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
300 if term2str t = "a ^^^ 2 * b" then () |
300 if term2str t = "a ^^^ 2 * b" then () |
301 else raise error "poly.sml: diff.behav. in make_polynomial 21"; |
301 else error "poly.sml: diff.behav. in make_polynomial 21"; |
302 (*SPO*) |
302 (*SPO*) |
303 val t = str2term "(a^^^2)^^^3"; |
303 val t = str2term "(a^^^2)^^^3"; |
304 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
304 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
305 if term2str t = "a ^^^ 6" then () |
305 if term2str t = "a ^^^ 6" then () |
306 else raise error "poly.sml: diff.behav. in make_polynomial 22"; |
306 else error "poly.sml: diff.behav. in make_polynomial 22"; |
307 (*SPO*) |
307 (*SPO*) |
308 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y"; |
308 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y"; |
309 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
309 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
310 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then () |
310 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then () |
311 else raise error "poly.sml: diff.behav. in make_polynomial 23"; |
311 else error "poly.sml: diff.behav. in make_polynomial 23"; |
312 (*SPO*) |
312 (*SPO*) |
313 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2"; |
313 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2"; |
314 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
314 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
315 if (term2str t) = "a ^^^ 4" then () |
315 if (term2str t) = "a ^^^ 4" then () |
316 else raise error "poly.sml: diff.behav. in make_polynomial 24"; |
316 else error "poly.sml: diff.behav. in make_polynomial 24"; |
317 (*SPO*) |
317 (*SPO*) |
318 val t = str2term "a * b * b^^^(-1) + a"; |
318 val t = str2term "a * b * b^^^(-1) + a"; |
319 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
319 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
320 if (term2str t) = "2 * a" then () |
320 if (term2str t) = "2 * a" then () |
321 else raise error "poly.sml: diff.behav. in make_polynomial 25"; |
321 else error "poly.sml: diff.behav. in make_polynomial 25"; |
322 (*SPO*) |
322 (*SPO*) |
323 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b"; |
323 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b"; |
324 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
324 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; |
325 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c" |
325 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c" |
326 then () else raise error "poly.sml: diff.behav. in make_polynomial 26"; |
326 then () else error "poly.sml: diff.behav. in make_polynomial 26"; |
327 |
327 |
328 |
328 |
329 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*) |
329 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*) |
330 (*SPO*) |
330 (*SPO*) |
331 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)"; |
331 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)"; |
332 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
332 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
333 term2str t; |
333 term2str t; |
334 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)" |
334 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)" |
335 then () else raise error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*) |
335 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*) |
336 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)"; |
336 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)"; |
337 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
337 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; |
338 term2str t; |
338 term2str t; |
339 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)" |
339 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)" |
340 then () else raise error "poly.sml: diff.behav. in make_polynomial 28"; |
340 then () else error "poly.sml: diff.behav. in make_polynomial 28"; |
341 |
341 |
342 "-------- Script 'simplification for_polynomials' ----------------"; |
342 "-------- Script 'simplification for_polynomials' ----------------"; |
343 "-------- Script 'simplification for_polynomials' ----------------"; |
343 "-------- Script 'simplification for_polynomials' ----------------"; |
344 "-------- Script 'simplification for_polynomials' ----------------"; |
344 "-------- Script 'simplification for_polynomials' ----------------"; |
345 val str = |
345 val str = |