279 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\ |
278 \ L * c_3 + c_4 = q_0 * L ^^^ 2 / 2,\ |
280 \ c_2 + (c_3 + c_4) = 0,\n\ |
279 \ c_2 + (c_3 + c_4) = 0,\n\ |
281 \ c + (c_2 + (c_3 + c_4)) = 0]" |
280 \ c + (c_2 + (c_3 + c_4)) = 0]" |
282 then () else error "eqsystem.sml rewrite in 4x4 order_system"; |
281 then () else error "eqsystem.sml rewrite in 4x4 order_system"; |
283 |
282 |
284 (*=== inhibit exn 110722============================================================= |
|
285 |
|
286 "----------- script [EqSystem,normalize,2x2] ---------------------"; |
|
287 "----------- script [EqSystem,normalize,2x2] ---------------------"; |
|
288 "----------- script [EqSystem,normalize,2x2] ---------------------"; |
|
289 val str = |
|
290 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
291 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
292 \ simplify_System_parenthesized False) es_ \ |
|
293 \ in ([]))"; |
|
294 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
295 val str = |
|
296 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
297 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
298 \ simplify_System_parenthesized False) es_ \ |
|
299 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
300 \ []))"; |
|
301 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
302 val str = |
|
303 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
304 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
305 \ simplify_System_parenthesized False) es_ \ |
|
306 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
307 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
308 ; |
|
309 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
310 val str = |
|
311 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
312 \ (let es__ = Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
313 \ simplify_System_parenthesized False) es_ \ |
|
314 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
315 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
316 ; |
|
317 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
318 val str = |
|
319 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
320 \ (let es__ = (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
321 \ simplify_System_parenthesized False)) es_ \ |
|
322 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
323 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
324 ; |
|
325 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
326 val str = |
|
327 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
328 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
329 \ simplify_System_parenthesized False)) @@\ |
|
330 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
331 \ simplify_System_parenthesized False))) es_\ |
|
332 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
333 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
334 ; |
|
335 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
336 val str = |
|
337 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
338 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
339 \ simplify_System_parenthesized False)) @@\ |
|
340 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
341 \ simplify_System_parenthesized False)) @@\ |
|
342 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
343 \ simplify_System_parenthesized False))) es_\ |
|
344 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
345 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
346 ; |
|
347 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
348 val str = |
|
349 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
350 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
351 \ simplify_System_parenthesized False)) @@\ |
|
352 \ (Try (Rewrite_Set_Inst [] isolate_bdvs False)) @@\ |
|
353 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
354 \ simplify_System_parenthesized False)) @@\ |
|
355 \ (Try (Rewrite_Set order_system False))) es_\ |
|
356 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
357 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
358 ; |
|
359 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
360 val str = |
|
361 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
362 \ (let es__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
363 \ simplify_System_parenthesized False)) @@\ |
|
364 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s)]\ |
|
365 \ isolate_bdvs False)) @@\ |
|
366 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
367 \ simplify_System_parenthesized False)) @@\ |
|
368 \ (Try (Rewrite_Set order_system False))) es_\ |
|
369 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
370 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
371 ; |
|
372 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
373 val str = |
|
374 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
375 \ (let es__ = ((Try (Rewrite_Set simplify_System_parenthesized False)) @@\ |
|
376 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
377 \ isolate_bdvs False)) @@\ |
|
378 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
379 \ simplify_System_parenthesized False)) @@\ |
|
380 \ (Try (Rewrite_Set order_system False))) es_\ |
|
381 \ in (SubProblem (Biegelinie_,[linear,system],[no_met])\ |
|
382 \ [BOOL_LIST es__, REAL_LIST v_s]))" |
|
383 ; |
|
384 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
385 |
|
386 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; |
|
387 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; |
|
388 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; |
|
389 val str = |
|
390 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
391 \ (let es__ = (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
392 \ simplify_System_parenthesized False) es_ \ |
|
393 \ in ([]))"; |
|
394 |
|
395 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
396 val str = |
|
397 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
398 \ (let e1__ = Take (hd es_) \ |
|
399 \ in ([]))"; |
|
400 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
401 val str = |
|
402 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
403 \ (let e1__ = Take (hd es_); \ |
|
404 \ e1__ = Take (hd es_) \ |
|
405 \ in ([]))"; |
|
406 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
407 val str = |
|
408 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
409 \ (let e1__ = Take (hd es_); \ |
|
410 \ e1__ = (Take (hd es_))\ |
|
411 \ in ([]))"; |
|
412 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
413 val str = |
|
414 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
415 \ (let e1__ = Take (hd es_); \ |
|
416 \ e1__ = ((Rewrite_Set order_system False)) e1__\ |
|
417 \ in ([]))"; |
|
418 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
419 val str = |
|
420 "(Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
421 \ isolate_bdvs False) (e1__::bool)"; |
|
422 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
423 val str = |
|
424 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
425 \ (let e1__ = Take (hd es_); \ |
|
426 \ e1__ = ((Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
427 \ isolate_bdvs False)) e1__\ |
|
428 \ in ([]))"; |
|
429 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
430 val str = |
|
431 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
432 \ (let e1__ = Take (hd es_); \ |
|
433 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
434 \ isolate_bdvs False)) @@\ |
|
435 \ (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
436 \ simplify_System False)) e1__\ |
|
437 \ in ([]))"; |
|
438 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
439 val str = |
|
440 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
441 \ (let e1__ = Take (hd es_); \ |
|
442 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
443 \ isolate_bdvs False)) @@\ |
|
444 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
445 \ simplify_System False))) e1__\ |
|
446 \ in ([]))"; |
|
447 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
448 val str = |
|
449 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
450 \ (let e1__ = Take (hd es_); \ |
|
451 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
452 \ isolate_bdvs False)) @@ \ |
|
453 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
454 \ simplify_System False))) e1__; \ |
|
455 \ e2__ = Take (hd (tl es_)) \ |
|
456 \ in ([]))"; |
|
457 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
458 val str = |
|
459 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
460 \ (let e1__ = Take (hd es_); \ |
|
461 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
462 \ isolate_bdvs False)) @@ \ |
|
463 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
464 \ simplify_System False))) e1__; \ |
|
465 \ e2__ = Take (hd (tl es_)); \ |
|
466 \ e2__ = Substitute [e1__] e2__ \ |
|
467 \ in ([]))"; |
|
468 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
469 val str = |
|
470 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
471 \ (let e1__ = Take (hd es_); \ |
|
472 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
473 \ isolate_bdvs False)) @@ \ |
|
474 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
475 \ simplify_System False))) e1__; \ |
|
476 \ e2__ = Take (hd (tl es_)); \ |
|
477 \ e2__ = ((Substitute [e1__])) e2__ \ |
|
478 \ in ([]))"; |
|
479 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
480 val str = |
|
481 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
482 \ (let e1__ = Take (hd es_); \ |
|
483 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
484 \ isolate_bdvs False)) @@ \ |
|
485 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
486 \ simplify_System False))) e1__; \ |
|
487 \ e2__ = Take (hd (tl es_)); \ |
|
488 \ e2__ = ((Substitute [e1__]) @@ \ |
|
489 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
490 \ isolate_bdvs False)) @@ \ |
|
491 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
492 \ simplify_System False))) e2__ \ |
|
493 \ in [e1__, e2__])" |
|
494 ; |
|
495 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
496 val str = |
|
497 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
|
498 \ (let e1__ = Take (hd es_); \ |
|
499 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
500 \ isolate_bdvs False)) @@ \ |
|
501 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
502 \ simplify_System False))) e1__; \ |
|
503 \ e2__ = Take (hd (tl es_)); \ |
|
504 \ e2__ = ((Substitute [e1__]) @@ \ |
|
505 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
506 \ simplify_System_parenthesized False)) @@ \ |
|
507 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
508 \ isolate_bdvs False)) @@ \ |
|
509 \ (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
|
510 \ simplify_System False)) @@ \ |
|
511 \ (Try (Rewrite_Set order_system False))) e2__ \ |
|
512 \ in [e1__, e2__])" |
|
513 ; |
|
514 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str; |
|
515 === inhibit exn 110722=============================================================*) |
|
516 |
283 |
517 val str = |
284 val str = |
518 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
285 "Script SolveSystemScript (es_::bool list) (v_s::real list) = \ |
519 \ (let e1__ = Take (hd es_); \ |
286 \ (let e1__ = Take (hd es_); \ |
520 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |
287 \ e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]\ |