413 (** problems **) |
413 (** problems **) |
414 |
414 |
415 store_pbt |
415 store_pbt |
416 (prep_pbt thy "pbl_equsys" [] e_pblID |
416 (prep_pbt thy "pbl_equsys" [] e_pblID |
417 (["system"], |
417 (["system"], |
418 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
418 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
419 ("#Find" ,["solution ss___"](*___ is copy-named*)) |
419 ("#Find" ,["solution ss___"](*___ is copy-named*)) |
420 ], |
420 ], |
421 append_rls "e_rls" e_rls [(*for preds in where_*)], |
421 append_rls "e_rls" e_rls [(*for preds in where_*)], |
422 SOME "solveSystem es_ vs_", |
422 SOME "solveSystem es_ v_s", |
423 [])); |
423 [])); |
424 store_pbt |
424 store_pbt |
425 (prep_pbt thy "pbl_equsys_lin" [] e_pblID |
425 (prep_pbt thy "pbl_equsys_lin" [] e_pblID |
426 (["linear", "system"], |
426 (["linear", "system"], |
427 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
427 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
428 (*TODO.WN050929 check linearity*) |
428 (*TODO.WN050929 check linearity*) |
429 ("#Find" ,["solution ss___"]) |
429 ("#Find" ,["solution ss___"]) |
430 ], |
430 ], |
431 append_rls "e_rls" e_rls [(*for preds in where_*)], |
431 append_rls "e_rls" e_rls [(*for preds in where_*)], |
432 SOME "solveSystem es_ vs_", |
432 SOME "solveSystem es_ v_s", |
433 [])); |
433 [])); |
434 store_pbt |
434 store_pbt |
435 (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID |
435 (prep_pbt thy "pbl_equsys_lin_2x2" [] e_pblID |
436 (["2x2", "linear", "system"], |
436 (["2x2", "linear", "system"], |
437 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
437 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
438 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
438 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
439 ("#Where" ,["length_ (es_:: bool list) = 2", "length_ vs_ = 2"]), |
439 ("#Where" ,["length_ (es_:: bool list) = 2", "length_ v_s = 2"]), |
440 ("#Find" ,["solution ss___"]) |
440 ("#Find" ,["solution ss___"]) |
441 ], |
441 ], |
442 append_rls "prls_2x2_linear_system" e_rls |
442 append_rls "prls_2x2_linear_system" e_rls |
443 [Thm ("length_Cons_",num_str @{thm length_Cons_}), |
443 [Thm ("length_Cons_",num_str @{thm length_Cons_}), |
444 Thm ("length_Nil_",num_str @{thm length_Nil_}), |
444 Thm ("length_Nil_",num_str @{thm length_Nil_}), |
445 Calc ("op +", eval_binop "#add_"), |
445 Calc ("op +", eval_binop "#add_"), |
446 Calc ("op =",eval_equal "#equal_") |
446 Calc ("op =",eval_equal "#equal_") |
447 ], |
447 ], |
448 SOME "solveSystem es_ vs_", |
448 SOME "solveSystem es_ v_s", |
449 [])); |
449 [])); |
450 store_pbt |
450 store_pbt |
451 (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID |
451 (prep_pbt thy "pbl_equsys_lin_2x2_tri" [] e_pblID |
452 (["triangular", "2x2", "linear", "system"], |
452 (["triangular", "2x2", "linear", "system"], |
453 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
453 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
454 ("#Where" , |
454 ("#Where" , |
455 ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", |
455 ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))", |
456 " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), |
456 " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]), |
457 ("#Find" ,["solution ss___"]) |
457 ("#Find" ,["solution ss___"]) |
458 ], |
458 ], |
459 prls_triangular, |
459 prls_triangular, |
460 SOME "solveSystem es_ vs_", |
460 SOME "solveSystem es_ v_s", |
461 [["EqSystem","top_down_substitution","2x2"]])); |
461 [["EqSystem","top_down_substitution","2x2"]])); |
462 store_pbt |
462 store_pbt |
463 (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID |
463 (prep_pbt thy "pbl_equsys_lin_2x2_norm" [] e_pblID |
464 (["normalize", "2x2", "linear", "system"], |
464 (["normalize", "2x2", "linear", "system"], |
465 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
465 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
466 ("#Find" ,["solution ss___"]) |
466 ("#Find" ,["solution ss___"]) |
467 ], |
467 ], |
468 append_rls "e_rls" e_rls [(*for preds in where_*)], |
468 append_rls "e_rls" e_rls [(*for preds in where_*)], |
469 SOME "solveSystem es_ vs_", |
469 SOME "solveSystem es_ v_s", |
470 [["EqSystem","normalize","2x2"]])); |
470 [["EqSystem","normalize","2x2"]])); |
471 store_pbt |
471 store_pbt |
472 (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID |
472 (prep_pbt thy "pbl_equsys_lin_3x3" [] e_pblID |
473 (["3x3", "linear", "system"], |
473 (["3x3", "linear", "system"], |
474 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
474 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
475 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
475 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
476 ("#Where" ,["length_ (es_:: bool list) = 3", "length_ vs_ = 3"]), |
476 ("#Where" ,["length_ (es_:: bool list) = 3", "length_ v_s = 3"]), |
477 ("#Find" ,["solution ss___"]) |
477 ("#Find" ,["solution ss___"]) |
478 ], |
478 ], |
479 append_rls "prls_3x3_linear_system" e_rls |
479 append_rls "prls_3x3_linear_system" e_rls |
480 [Thm ("length_Cons_",num_str @{thm length_Cons_}), |
480 [Thm ("length_Cons_",num_str @{thm length_Cons_}), |
481 Thm ("length_Nil_",num_str @{thm length_Nil_}), |
481 Thm ("length_Nil_",num_str @{thm length_Nil_}), |
482 Calc ("op +", eval_binop "#add_"), |
482 Calc ("op +", eval_binop "#add_"), |
483 Calc ("op =",eval_equal "#equal_") |
483 Calc ("op =",eval_equal "#equal_") |
484 ], |
484 ], |
485 SOME "solveSystem es_ vs_", |
485 SOME "solveSystem es_ v_s", |
486 [])); |
486 [])); |
487 store_pbt |
487 store_pbt |
488 (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID |
488 (prep_pbt thy "pbl_equsys_lin_4x4" [] e_pblID |
489 (["4x4", "linear", "system"], |
489 (["4x4", "linear", "system"], |
490 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
490 (*~~~~~~~~~~~~~~~~~~~~~~~~~*) |
491 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
491 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
492 ("#Where" ,["length_ (es_:: bool list) = 4", "length_ vs_ = 4"]), |
492 ("#Where" ,["length_ (es_:: bool list) = 4", "length_ v_s = 4"]), |
493 ("#Find" ,["solution ss___"]) |
493 ("#Find" ,["solution ss___"]) |
494 ], |
494 ], |
495 append_rls "prls_4x4_linear_system" e_rls |
495 append_rls "prls_4x4_linear_system" e_rls |
496 [Thm ("length_Cons_",num_str @{thm length_Cons_}), |
496 [Thm ("length_Cons_",num_str @{thm length_Cons_}), |
497 Thm ("length_Nil_",num_str @{thm length_Nil_}), |
497 Thm ("length_Nil_",num_str @{thm length_Nil_}), |
498 Calc ("op +", eval_binop "#add_"), |
498 Calc ("op +", eval_binop "#add_"), |
499 Calc ("op =",eval_equal "#equal_") |
499 Calc ("op =",eval_equal "#equal_") |
500 ], |
500 ], |
501 SOME "solveSystem es_ vs_", |
501 SOME "solveSystem es_ v_s", |
502 [])); |
502 [])); |
503 store_pbt |
503 store_pbt |
504 (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID |
504 (prep_pbt thy "pbl_equsys_lin_4x4_tri" [] e_pblID |
505 (["triangular", "4x4", "linear", "system"], |
505 (["triangular", "4x4", "linear", "system"], |
506 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
506 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
507 ("#Where" , (*accepts missing variables up to diagional form*) |
507 ("#Where" , (*accepts missing variables up to diagional form*) |
508 ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", |
508 ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))", |
509 "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", |
509 "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))", |
510 "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", |
510 "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))", |
511 "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" |
511 "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))" |
512 ]), |
512 ]), |
513 ("#Find" ,["solution ss___"]) |
513 ("#Find" ,["solution ss___"]) |
514 ], |
514 ], |
515 append_rls "prls_tri_4x4_lin_sys" prls_triangular |
515 append_rls "prls_tri_4x4_lin_sys" prls_triangular |
516 [Calc ("Atools.occurs'_in",eval_occurs_in "")], |
516 [Calc ("Atools.occurs'_in",eval_occurs_in "")], |
517 SOME "solveSystem es_ vs_", |
517 SOME "solveSystem es_ v_s", |
518 [["EqSystem","top_down_substitution","4x4"]])); |
518 [["EqSystem","top_down_substitution","4x4"]])); |
519 |
519 |
520 store_pbt |
520 store_pbt |
521 (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID |
521 (prep_pbt thy "pbl_equsys_lin_4x4_norm" [] e_pblID |
522 (["normalize", "4x4", "linear", "system"], |
522 (["normalize", "4x4", "linear", "system"], |
523 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
523 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
524 (*length_ is checked 1 level above*) |
524 (*length_ is checked 1 level above*) |
525 ("#Find" ,["solution ss___"]) |
525 ("#Find" ,["solution ss___"]) |
526 ], |
526 ], |
527 append_rls "e_rls" e_rls [(*for preds in where_*)], |
527 append_rls "e_rls" e_rls [(*for preds in where_*)], |
528 SOME "solveSystem es_ vs_", |
528 SOME "solveSystem es_ v_s", |
529 [["EqSystem","normalize","4x4"]])); |
529 [["EqSystem","normalize","4x4"]])); |
530 |
530 |
531 |
531 |
532 (* show_ptyps(); |
532 (* show_ptyps(); |
533 *) |
533 *) |
551 "empty_script" |
551 "empty_script" |
552 )); |
552 )); |
553 store_met |
553 store_met |
554 (prep_met thy "met_eqsys_topdown_2x2" [] e_metID |
554 (prep_met thy "met_eqsys_topdown_2x2" [] e_metID |
555 (["EqSystem","top_down_substitution","2x2"], |
555 (["EqSystem","top_down_substitution","2x2"], |
556 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
556 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
557 ("#Where" , |
557 ("#Where" , |
558 ["(tl vs_) from_ vs_ occur_exactly_in (nth_ 1 (es_::bool list))", |
558 ["(tl v_s) from_ v_s occur_exactly_in (nth_ 1 (es_::bool list))", |
559 " vs_ from_ vs_ occur_exactly_in (nth_ 2 (es_::bool list))"]), |
559 " v_s from_ v_s occur_exactly_in (nth_ 2 (es_::bool list))"]), |
560 ("#Find" ,["solution ss___"]) |
560 ("#Find" ,["solution ss___"]) |
561 ], |
561 ], |
562 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], |
562 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], |
563 srls = append_rls "srls_top_down_2x2" e_rls |
563 srls = append_rls "srls_top_down_2x2" e_rls |
564 [Thm ("hd_thm",num_str @{thm hd_thm}), |
564 [Thm ("hd_thm",num_str @{thm hd_thm}), |
565 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
565 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
566 Thm ("tl_Nil",num_str @{thm tl_Nil}) |
566 Thm ("tl_Nil",num_str @{thm tl_Nil}) |
567 ], |
567 ], |
568 prls = prls_triangular, crls = Erls, nrls = Erls}, |
568 prls = prls_triangular, crls = Erls, nrls = Erls}, |
569 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
569 "Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ |
570 " (let e1__ = Take (hd es_); " ^ |
570 " (let e1__ = Take (hd es_); " ^ |
571 " e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
571 " e1__ = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
572 " isolate_bdvs False)) @@ " ^ |
572 " isolate_bdvs False)) @@ " ^ |
573 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
573 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
574 " simplify_System False))) e1__; " ^ |
574 " simplify_System False))) e1__; " ^ |
575 " e2__ = Take (hd (tl es_)); " ^ |
575 " e2__ = Take (hd (tl es_)); " ^ |
576 " e2__ = ((Substitute [e1__]) @@ " ^ |
576 " e2__ = ((Substitute [e1__]) @@ " ^ |
577 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
577 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
578 " simplify_System_parenthesized False)) @@ " ^ |
578 " simplify_System_parenthesized False)) @@ " ^ |
579 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
579 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
580 " isolate_bdvs False)) @@ " ^ |
580 " isolate_bdvs False)) @@ " ^ |
581 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
581 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
582 " simplify_System False))) e2__; " ^ |
582 " simplify_System False))) e2__; " ^ |
583 " es__ = Take [e1__, e2__] " ^ |
583 " es__ = Take [e1__, e2__] " ^ |
584 " in (Try (Rewrite_Set order_system False)) es__)" |
584 " in (Try (Rewrite_Set order_system False)) es__)" |
585 (*--------------------------------------------------------------------------- |
585 (*--------------------------------------------------------------------------- |
586 this script does NOT separate the equations as abolve, |
586 this script does NOT separate the equations as abolve, |
587 but it does not yet work due to preliminary script-interpreter, |
587 but it does not yet work due to preliminary script-interpreter, |
588 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' |
588 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' |
589 |
589 |
590 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
590 "Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ |
591 " (let es__ = Take es_; " ^ |
591 " (let es__ = Take es_; " ^ |
592 " e1__ = hd es__; " ^ |
592 " e1__ = hd es__; " ^ |
593 " e2__ = hd (tl es__); " ^ |
593 " e2__ = hd (tl es__); " ^ |
594 " es__ = [e1__, Substitute [e1__] e2__] " ^ |
594 " es__ = [e1__, Substitute [e1__] e2__] " ^ |
595 " in ((Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
595 " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
596 " simplify_System_parenthesized False)) @@ " ^ |
596 " simplify_System_parenthesized False)) @@ " ^ |
597 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))] " ^ |
597 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^ |
598 " isolate_bdvs False)) @@ " ^ |
598 " isolate_bdvs False)) @@ " ^ |
599 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
599 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
600 " simplify_System False))) es__)" |
600 " simplify_System False))) es__)" |
601 ---------------------------------------------------------------------------*) |
601 ---------------------------------------------------------------------------*) |
602 )); |
602 )); |
603 store_met |
603 store_met |
604 (prep_met thy "met_eqsys_norm" [] e_metID |
604 (prep_met thy "met_eqsys_norm" [] e_metID |
609 "empty_script" |
609 "empty_script" |
610 )); |
610 )); |
611 store_met |
611 store_met |
612 (prep_met thy "met_eqsys_norm_2x2" [] e_metID |
612 (prep_met thy "met_eqsys_norm_2x2" [] e_metID |
613 (["EqSystem","normalize","2x2"], |
613 (["EqSystem","normalize","2x2"], |
614 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
614 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
615 ("#Find" ,["solution ss___"])], |
615 ("#Find" ,["solution ss___"])], |
616 {rew_ord'="tless_true", rls' = Erls, calc = [], |
616 {rew_ord'="tless_true", rls' = Erls, calc = [], |
617 srls = append_rls "srls_normalize_2x2" e_rls |
617 srls = append_rls "srls_normalize_2x2" e_rls |
618 [Thm ("hd_thm",num_str @{thm hd_thm}), |
618 [Thm ("hd_thm",num_str @{thm hd_thm}), |
619 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
619 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
620 Thm ("tl_Nil",num_str @{thm tl_Nil}) |
620 Thm ("tl_Nil",num_str @{thm tl_Nil}) |
621 ], |
621 ], |
622 prls = Erls, crls = Erls, nrls = Erls}, |
622 prls = Erls, crls = Erls, nrls = Erls}, |
623 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
623 "Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ |
624 " (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
624 " (let es__ = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
625 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
625 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
626 " simplify_System_parenthesized False)) @@ " ^ |
626 " simplify_System_parenthesized False)) @@ " ^ |
627 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
627 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
628 " isolate_bdvs False)) @@ " ^ |
628 " isolate_bdvs False)) @@ " ^ |
629 " (Try (Rewrite_Set_Inst [(bdv_1, hd vs_),(bdv_2, hd (tl vs_))]" ^ |
629 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
630 " simplify_System_parenthesized False)) @@ " ^ |
630 " simplify_System_parenthesized False)) @@ " ^ |
631 " (Try (Rewrite_Set order_system False))) es_ " ^ |
631 " (Try (Rewrite_Set order_system False))) es_ " ^ |
632 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
632 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
633 " [BOOL_LIST es__, REAL_LIST vs_]))" |
633 " [BOOL_LIST es__, REAL_LIST v_s]))" |
634 )); |
634 )); |
635 |
635 |
636 (*this is for nth_ only*) |
636 (*this is for nth_ only*) |
637 val srls = Rls {id="srls_normalize_4x4", |
637 val srls = Rls {id="srls_normalize_4x4", |
638 preconds = [], |
638 preconds = [], |
649 Thm ("nth_Nil_",num_str @{thm nth_Nil_})], |
649 Thm ("nth_Nil_",num_str @{thm nth_Nil_})], |
650 scr = EmptyScr}; |
650 scr = EmptyScr}; |
651 store_met |
651 store_met |
652 (prep_met thy "met_eqsys_norm_4x4" [] e_metID |
652 (prep_met thy "met_eqsys_norm_4x4" [] e_metID |
653 (["EqSystem","normalize","4x4"], |
653 (["EqSystem","normalize","4x4"], |
654 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
654 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
655 ("#Find" ,["solution ss___"])], |
655 ("#Find" ,["solution ss___"])], |
656 {rew_ord'="tless_true", rls' = Erls, calc = [], |
656 {rew_ord'="tless_true", rls' = Erls, calc = [], |
657 srls = append_rls "srls_normalize_4x4" srls |
657 srls = append_rls "srls_normalize_4x4" srls |
658 [Thm ("hd_thm",num_str @{thm hd_thm}), |
658 [Thm ("hd_thm",num_str @{thm hd_thm}), |
659 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
659 Thm ("tl_Cons",num_str @{thm tl_Cons}), |
660 Thm ("tl_Nil",num_str @{thm tl_Nil}) |
660 Thm ("tl_Nil",num_str @{thm tl_Nil}) |
661 ], |
661 ], |
662 prls = Erls, crls = Erls, nrls = Erls}, |
662 prls = Erls, crls = Erls, nrls = Erls}, |
663 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
663 (*GOON met ["EqSystem","normalize","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
664 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
664 "Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ |
665 " (let es__ = " ^ |
665 " (let es__ = " ^ |
666 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
666 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
667 " (Repeat (Rewrite commute_0_equality False)) @@ " ^ |
667 " (Repeat (Rewrite commute_0_equality False)) @@ " ^ |
668 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
668 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^ |
669 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
669 " (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^ |
670 " simplify_System_parenthesized False)) @@ " ^ |
670 " simplify_System_parenthesized False)) @@ " ^ |
671 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
671 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^ |
672 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
672 " (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^ |
673 " isolate_bdvs_4x4 False)) @@ " ^ |
673 " isolate_bdvs_4x4 False)) @@ " ^ |
674 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 vs_),(bdv_2, nth_ 2 vs_ ), " ^ |
674 " (Try (Rewrite_Set_Inst [(bdv_1, nth_ 1 v_s),(bdv_2, nth_ 2 v_s ), " ^ |
675 " (bdv_3, nth_ 3 vs_),(bdv_3, nth_ 4 vs_ )] " ^ |
675 " (bdv_3, nth_ 3 v_s),(bdv_3, nth_ 4 v_s )] " ^ |
676 " simplify_System_parenthesized False)) @@ " ^ |
676 " simplify_System_parenthesized False)) @@ " ^ |
677 " (Try (Rewrite_Set order_system False))) es_ " ^ |
677 " (Try (Rewrite_Set order_system False))) es_ " ^ |
678 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
678 " in (SubProblem (EqSystem_,[linear,system],[no_met]) " ^ |
679 " [BOOL_LIST es__, REAL_LIST vs_]))" |
679 " [BOOL_LIST es__, REAL_LIST v_s]))" |
680 )); |
680 )); |
681 store_met |
681 store_met |
682 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID |
682 (prep_met thy "met_eqsys_topdown_4x4" [] e_metID |
683 (["EqSystem","top_down_substitution","4x4"], |
683 (["EqSystem","top_down_substitution","4x4"], |
684 [("#Given" ,["equalities es_", "solveForVars vs_"]), |
684 [("#Given" ,["equalities es_", "solveForVars v_s"]), |
685 ("#Where" , (*accepts missing variables up to diagonal form*) |
685 ("#Where" , (*accepts missing variables up to diagonal form*) |
686 ["(nth_ 1 (vs_::real list)) occurs_in (nth_ 1 (es_::bool list))", |
686 ["(nth_ 1 (v_s::real list)) occurs_in (nth_ 1 (es_::bool list))", |
687 "(nth_ 2 (vs_::real list)) occurs_in (nth_ 2 (es_::bool list))", |
687 "(nth_ 2 (v_s::real list)) occurs_in (nth_ 2 (es_::bool list))", |
688 "(nth_ 3 (vs_::real list)) occurs_in (nth_ 3 (es_::bool list))", |
688 "(nth_ 3 (v_s::real list)) occurs_in (nth_ 3 (es_::bool list))", |
689 "(nth_ 4 (vs_::real list)) occurs_in (nth_ 4 (es_::bool list))" |
689 "(nth_ 4 (v_s::real list)) occurs_in (nth_ 4 (es_::bool list))" |
690 ]), |
690 ]), |
691 ("#Find" ,["solution ss___"]) |
691 ("#Find" ,["solution ss___"]) |
692 ], |
692 ], |
693 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], |
693 {rew_ord'="ord_simplify_System", rls' = Erls, calc = [], |
694 srls = append_rls "srls_top_down_4x4" srls [], |
694 srls = append_rls "srls_top_down_4x4" srls [], |
695 prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular |
695 prls = append_rls "prls_tri_4x4_lin_sys" prls_triangular |
696 [Calc ("Atools.occurs'_in",eval_occurs_in "")], |
696 [Calc ("Atools.occurs'_in",eval_occurs_in "")], |
697 crls = Erls, nrls = Erls}, |
697 crls = Erls, nrls = Erls}, |
698 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
698 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
699 "Script SolveSystemScript (es_::bool list) (vs_::real list) = " ^ |
699 "Script SolveSystemScript (es_::bool list) (v_s::real list) = " ^ |
700 " (let e1_ = nth_ 1 es_; " ^ |
700 " (let e1_ = nth_ 1 es_; " ^ |
701 " e2_ = Take (nth_ 2 es_); " ^ |
701 " e2_ = Take (nth_ 2 es_); " ^ |
702 " e2_ = ((Substitute [e1_]) @@ " ^ |
702 " e2_ = ((Substitute [e1_]) @@ " ^ |
703 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ |
703 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^ |
704 " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ |
704 " (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^ |
705 " simplify_System_parenthesized False)) @@ " ^ |
705 " simplify_System_parenthesized False)) @@ " ^ |
706 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ |
706 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^ |
707 " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ |
707 " (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^ |
708 " isolate_bdvs False)) @@ " ^ |
708 " isolate_bdvs False)) @@ " ^ |
709 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 vs_),(bdv_2,nth_ 2 vs_)," ^ |
709 " (Try (Rewrite_Set_Inst [(bdv_1,nth_ 1 v_s),(bdv_2,nth_ 2 v_s)," ^ |
710 " (bdv_3,nth_ 3 vs_),(bdv_4,nth_ 4 vs_)]" ^ |
710 " (bdv_3,nth_ 3 v_s),(bdv_4,nth_ 4 v_s)]" ^ |
711 " norm_Rational False))) e2_ " ^ |
711 " norm_Rational False))) e2_ " ^ |
712 " in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])" |
712 " in [e1_, e2_, nth_ 3 es_, nth_ 4 es_])" |
713 )); |
713 )); |
714 *} |
714 *} |
715 |
715 |