equal
deleted
inserted
replaced
250 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
250 "----------- pbl polynom vereinfachen p.33 -----------------------"; |
251 "----------- 140 c ---"; |
251 "----------- 140 c ---"; |
252 states:=[]; |
252 states:=[]; |
253 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
253 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
254 "normalform N"], |
254 "normalform N"], |
255 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
255 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
256 ["simplification","for_polynomials","with_minus"]))]; |
256 ["simplification","for_polynomials","with_minus"]))]; |
257 moveActiveRoot 1; |
257 moveActiveRoot 1; |
258 autoCalculate 1 CompleteCalc; |
258 autoCalculate 1 CompleteCalc; |
259 val ((pt,p),_) = get_calc 1; show_pt pt; |
259 val ((pt,p),_) = get_calc 1; show_pt pt; |
260 if p = ([], Res) andalso |
260 if p = ([], Res) andalso |
263 |
263 |
264 "----------- 140 d ---"; |
264 "----------- 140 d ---"; |
265 states:=[]; |
265 states:=[]; |
266 CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)", |
266 CalcTree [(["TERM (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)", |
267 "normalform N"], |
267 "normalform N"], |
268 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
268 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
269 ["simplification","for_polynomials","with_minus"]))]; |
269 ["simplification","for_polynomials","with_minus"]))]; |
270 moveActiveRoot 1; |
270 moveActiveRoot 1; |
271 autoCalculate 1 CompleteCalc; |
271 autoCalculate 1 CompleteCalc; |
272 val ((pt,p),_) = get_calc 1; show_pt pt; |
272 val ((pt,p),_) = get_calc 1; show_pt pt; |
273 if p = ([], Res) andalso |
273 if p = ([], Res) andalso |
277 |
277 |
278 "----------- 139 c ---"; |
278 "----------- 139 c ---"; |
279 states:=[]; |
279 states:=[]; |
280 CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)", |
280 CalcTree [(["TERM (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)", |
281 "normalform N"], |
281 "normalform N"], |
282 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
282 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
283 ["simplification","for_polynomials","with_minus"]))]; |
283 ["simplification","for_polynomials","with_minus"]))]; |
284 moveActiveRoot 1; |
284 moveActiveRoot 1; |
285 autoCalculate 1 CompleteCalc; |
285 autoCalculate 1 CompleteCalc; |
286 val ((pt,p),_) = get_calc 1; show_pt pt; |
286 val ((pt,p),_) = get_calc 1; show_pt pt; |
287 if p = ([], Res) andalso |
287 if p = ([], Res) andalso |
290 |
290 |
291 "----------- 139 b ---"; |
291 "----------- 139 b ---"; |
292 states:=[]; |
292 states:=[]; |
293 CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)", |
293 CalcTree [(["TERM (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)", |
294 "normalform N"], |
294 "normalform N"], |
295 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
295 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
296 ["simplification","for_polynomials","with_minus"]))]; |
296 ["simplification","for_polynomials","with_minus"]))]; |
297 moveActiveRoot 1; |
297 moveActiveRoot 1; |
298 autoCalculate 1 CompleteCalc; |
298 autoCalculate 1 CompleteCalc; |
299 val ((pt,p),_) = get_calc 1; show_pt pt; |
299 val ((pt,p),_) = get_calc 1; show_pt pt; |
300 if p = ([], Res) andalso |
300 if p = ([], Res) andalso |
303 |
303 |
304 "----------- 138 a ---"; |
304 "----------- 138 a ---"; |
305 states:=[]; |
305 states:=[]; |
306 CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)", |
306 CalcTree [(["TERM (2*u - 3*v - 6*u + 5*v)", |
307 "normalform N"], |
307 "normalform N"], |
308 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
308 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
309 ["simplification","for_polynomials","with_minus"]))]; |
309 ["simplification","for_polynomials","with_minus"]))]; |
310 moveActiveRoot 1; |
310 moveActiveRoot 1; |
311 autoCalculate 1 CompleteCalc; |
311 autoCalculate 1 CompleteCalc; |
312 val ((pt,p),_) = get_calc 1; show_pt pt; |
312 val ((pt,p),_) = get_calc 1; show_pt pt; |
313 if p = ([], Res) andalso |
313 if p = ([], Res) andalso |
318 "----------- met probe fuer_polynom ------------------------------"; |
318 "----------- met probe fuer_polynom ------------------------------"; |
319 "----------- met probe fuer_polynom ------------------------------"; |
319 "----------- met probe fuer_polynom ------------------------------"; |
320 "----------- met probe fuer_polynom ------------------------------"; |
320 "----------- met probe fuer_polynom ------------------------------"; |
321 val str = |
321 val str = |
322 "Script ProbeScript (e_e::bool) (ws_::bool list) =\ |
322 "Script ProbeScript (e_e::bool) (ws_::bool list) =\ |
323 \ (let e_e = Take e_; \ |
323 \ (let e_e = Take e_e; \ |
324 \ e_e = Substitute ws_ e_e \ |
324 \ e_e = Substitute ws_ e_e \ |
325 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \ |
325 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@ \ |
326 \ (Try (Repeat (Calculate PLUS ))) @@ \ |
326 \ (Try (Repeat (Calculate PLUS ))) @@ \ |
327 \ (Try (Repeat (Calculate MINUS))))) e_e)" |
327 \ (Try (Repeat (Calculate MINUS))))) e_e)" |
328 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
328 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
335 states:=[]; |
335 states:=[]; |
336 CalcTree [(["Pruefe (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\ |
336 CalcTree [(["Pruefe (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\ |
337 \3 - 2 * e + 2 * f + 2 * g)", |
337 \3 - 2 * e + 2 * f + 2 * g)", |
338 "mitWert [e = 1, f = 2, g = 3]", |
338 "mitWert [e = 1, f = 2, g = 3]", |
339 "Geprueft b"], |
339 "Geprueft b"], |
340 ("PolyMinus.thy",["polynom","probe"], |
340 ("PolyMinus",["polynom","probe"], |
341 ["probe","fuer_polynom"]))]; |
341 ["probe","fuer_polynom"]))]; |
342 moveActiveRoot 1; |
342 moveActiveRoot 1; |
343 autoCalculate 1 CompleteCalc; |
343 autoCalculate 1 CompleteCalc; |
344 (* autoCalculate 1 CompleteCalcHead; |
344 (* autoCalculate 1 CompleteCalcHead; |
345 autoCalculate 1 (Step 1); |
345 autoCalculate 1 (Step 1); |
357 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
357 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
358 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
358 "----------- pbl klammer polynom vereinfachen p.34 ---------------"; |
359 states:=[]; |
359 states:=[]; |
360 CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))", |
360 CalcTree [(["TERM (2*u - 5 - (3 - 4*u) + (8*u + 9))", |
361 "normalform N"], |
361 "normalform N"], |
362 ("PolyMinus.thy",["klammer","polynom","vereinfachen"], |
362 ("PolyMinus",["klammer","polynom","vereinfachen"], |
363 ["simplification","for_polynomials","with_parentheses"]))]; |
363 ["simplification","for_polynomials","with_parentheses"]))]; |
364 moveActiveRoot 1; |
364 moveActiveRoot 1; |
365 autoCalculate 1 CompleteCalc; |
365 autoCalculate 1 CompleteCalc; |
366 val ((pt,p),_) = get_calc 1; |
366 val ((pt,p),_) = get_calc 1; |
367 if p = ([], Res) andalso |
367 if p = ([], Res) andalso |
372 "----- probe p.34 -----"; |
372 "----- probe p.34 -----"; |
373 states:=[]; |
373 states:=[]; |
374 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)", |
374 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)", |
375 "mitWert [u = 2]", |
375 "mitWert [u = 2]", |
376 "Geprueft b"], |
376 "Geprueft b"], |
377 ("PolyMinus.thy",["polynom","probe"], |
377 ("PolyMinus",["polynom","probe"], |
378 ["probe","fuer_polynom"]))]; |
378 ["probe","fuer_polynom"]))]; |
379 moveActiveRoot 1; |
379 moveActiveRoot 1; |
380 autoCalculate 1 CompleteCalc; |
380 autoCalculate 1 CompleteCalc; |
381 val ((pt,p),_) = get_calc 1; |
381 val ((pt,p),_) = get_calc 1; |
382 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29" |
382 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29" |
388 "----------- try fun applyTactics --------------------------------"; |
388 "----------- try fun applyTactics --------------------------------"; |
389 "----------- try fun applyTactics --------------------------------"; |
389 "----------- try fun applyTactics --------------------------------"; |
390 states:=[]; |
390 states:=[]; |
391 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
391 CalcTree [(["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)", |
392 "normalform N"], |
392 "normalform N"], |
393 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
393 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
394 ["simplification","for_polynomials","with_minus"]))]; |
394 ["simplification","for_polynomials","with_minus"]))]; |
395 moveActiveRoot 1; |
395 moveActiveRoot 1; |
396 autoCalculate 1 CompleteCalcHead; |
396 autoCalculate 1 CompleteCalcHead; |
397 autoCalculate 1 (Step 1); |
397 autoCalculate 1 (Step 1); |
398 autoCalculate 1 (Step 1); |
398 autoCalculate 1 (Step 1); |
448 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) |
448 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) |
449 |
449 |
450 states:=[]; |
450 states:=[]; |
451 CalcTree [(["TERM (- (8 * g) + 10 * g + h)", |
451 CalcTree [(["TERM (- (8 * g) + 10 * g + h)", |
452 "normalform N"], |
452 "normalform N"], |
453 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
453 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
454 ["simplification","for_polynomials","with_minus"]))]; |
454 ["simplification","for_polynomials","with_minus"]))]; |
455 moveActiveRoot 1; |
455 moveActiveRoot 1; |
456 autoCalculate 1 CompleteCalc; |
456 autoCalculate 1 CompleteCalc; |
457 val ((pt,p),_) = get_calc 1; show_pt pt; |
457 val ((pt,p),_) = get_calc 1; show_pt pt; |
458 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h" |
458 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h" |
460 |
460 |
461 |
461 |
462 states:=[]; |
462 states:=[]; |
463 CalcTree [(["TERM (- (8 * g) + 10 * g + f)", |
463 CalcTree [(["TERM (- (8 * g) + 10 * g + f)", |
464 "normalform N"], |
464 "normalform N"], |
465 ("PolyMinus.thy",["plus_minus","polynom","vereinfachen"], |
465 ("PolyMinus",["plus_minus","polynom","vereinfachen"], |
466 ["simplification","for_polynomials","with_minus"]))]; |
466 ["simplification","for_polynomials","with_minus"]))]; |
467 moveActiveRoot 1; |
467 moveActiveRoot 1; |
468 autoCalculate 1 CompleteCalc; |
468 autoCalculate 1 CompleteCalc; |
469 val ((pt,p),_) = get_calc 1; show_pt pt; |
469 val ((pt,p),_) = get_calc 1; show_pt pt; |
470 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g" |
470 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g" |
509 |
509 |
510 (*@@@@@@@*) |
510 (*@@@@@@@*) |
511 states:=[]; |
511 states:=[]; |
512 CalcTree [(["TERM ((3*a + 2) * (4*a - 1))", |
512 CalcTree [(["TERM ((3*a + 2) * (4*a - 1))", |
513 "normalform N"], |
513 "normalform N"], |
514 ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"], |
514 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
515 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
515 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
516 moveActiveRoot 1; |
516 moveActiveRoot 1; |
517 autoCalculate 1 CompleteCalc; |
517 autoCalculate 1 CompleteCalc; |
518 val ((pt,p),_) = get_calc 1; show_pt pt; |
518 val ((pt,p),_) = get_calc 1; show_pt pt; |
519 |
519 |
528 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
528 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
529 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
529 "----------- pbl binom polynom vereinfachen: cube ----------------"; |
530 states:=[]; |
530 states:=[]; |
531 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", |
531 CalcTree [(["TERM (8*(a - q) + a - 2*q + 3*(a - 2*q))", |
532 "normalform N"], |
532 "normalform N"], |
533 ("PolyMinus.thy",["binom_klammer","polynom","vereinfachen"], |
533 ("PolyMinus",["binom_klammer","polynom","vereinfachen"], |
534 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
534 ["simplification","for_polynomials","with_parentheses_mult"]))]; |
535 moveActiveRoot 1; |
535 moveActiveRoot 1; |
536 autoCalculate 1 CompleteCalc; |
536 autoCalculate 1 CompleteCalc; |
537 val ((pt,p),_) = get_calc 1; show_pt pt; |
537 val ((pt,p),_) = get_calc 1; show_pt pt; |
538 |
538 |