541 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
541 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
542 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
542 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
543 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
543 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
544 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
544 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
545 " (let e_1 = Take (hd e_s); " ^ |
545 " (let e_1 = Take (hd e_s); " ^ |
546 " e_1 = ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
546 " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
547 " isolate_bdvs False)) @@ " ^ |
547 " ''isolate_bdvs'' False)) @@ " ^ |
548 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
548 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
549 " simplify_System False))) e_1; " ^ |
549 " ''simplify_System'' False))) e_1; " ^ |
550 " e_2 = Take (hd (tl e_s)); " ^ |
550 " e_2 = Take (hd (tl e_s)); " ^ |
551 " e_2 = ((Substitute [e_1]) @@ " ^ |
551 " e_2 = ((Substitute [e_1]) @@ " ^ |
552 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
552 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
553 " simplify_System_parenthesized False)) @@ " ^ |
553 " ''simplify_System_parenthesized'' False)) @@ " ^ |
554 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
554 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
555 " isolate_bdvs False)) @@ " ^ |
555 " ''isolate_bdvs'' False)) @@ " ^ |
556 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
556 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
557 " simplify_System False))) e_2; " ^ |
557 " ''simplify_System'' False))) e_2; " ^ |
558 " e__s = Take [e_1, e_2] " ^ |
558 " e__s = Take [e_1, e_2] " ^ |
559 " in (Try (Rewrite_Set order_system False)) e__s)" |
559 " in (Try (Rewrite_Set ''order_system'' False)) e__s)" |
560 (*--------------------------------------------------------------------------- |
560 (*--------------------------------------------------------------------------- |
561 this script does NOT separate the equations as above, |
561 this script does NOT separate the equations as above, |
562 but it does not yet work due to preliminary script-interpreter, |
562 but it does not yet work due to preliminary script-interpreter, |
563 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' |
563 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' |
564 |
564 |
565 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
565 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
566 " (let e__s = Take e_s; " ^ |
566 " (let e__s = Take e_s; " ^ |
567 " e_1 = hd e__s; " ^ |
567 " e_1 = hd e__s; " ^ |
568 " e_2 = hd (tl e__s); " ^ |
568 " e_2 = hd (tl e__s); " ^ |
569 " e__s = [e_1, Substitute [e_1] e_2] " ^ |
569 " e__s = [e_1, Substitute [e_1] e_2] " ^ |
570 " in ((Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
570 " in ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
571 " simplify_System_parenthesized False)) @@ " ^ |
571 " ''simplify_System_parenthesized'' False)) @@ " ^ |
572 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))] " ^ |
572 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] " ^ |
573 " isolate_bdvs False)) @@ " ^ |
573 " ''isolate_bdvs'' False)) @@ " ^ |
574 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
574 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
575 " simplify_System False))) e__s)" |
575 " ''simplify_System'' False))) e__s)" |
576 ---------------------------------------------------------------------------*))] |
576 ---------------------------------------------------------------------------*))] |
577 \<close> |
577 \<close> |
578 setup \<open>KEStore_Elems.add_mets |
578 setup \<open>KEStore_Elems.add_mets |
579 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID |
579 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID |
580 (["EqSystem", "normalise"], [], |
580 (["EqSystem", "normalise"], [], |
592 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
592 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
593 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
593 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
594 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
594 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
595 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
595 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
596 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
596 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
597 " (let e__s = ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
597 " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^ |
598 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
598 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
599 " simplify_System_parenthesized False)) @@ " ^ |
599 " ''simplify_System_parenthesized'' False)) @@ " ^ |
600 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
600 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
601 " isolate_bdvs False)) @@ " ^ |
601 " ''isolate_bdvs'' False)) @@ " ^ |
602 " (Try (Rewrite_Set_Inst [(bdv_1, hd v_s),(bdv_2, hd (tl v_s))]" ^ |
602 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
603 " simplify_System_parenthesized False)) @@ " ^ |
603 " ''simplify_System_parenthesized'' False)) @@ " ^ |
604 " (Try (Rewrite_Set order_system False))) e_s " ^ |
604 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^ |
605 " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^ |
605 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^ |
606 " [BOOL_LIST e__s, REAL_LIST v_s]))")] |
606 " [BOOL_LIST e__s, REAL_LIST v_s]))")] |
607 \<close> |
607 \<close> |
608 setup \<open>KEStore_Elems.add_mets |
608 setup \<open>KEStore_Elems.add_mets |
609 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID |
609 [Specify.prep_met thy "met_eqsys_norm_4x4" [] Celem.e_metID |
610 (["EqSystem","normalise","4x4"], |
610 (["EqSystem","normalise","4x4"], |
617 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
617 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
618 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
618 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
619 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
619 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
620 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
620 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
621 " (let e__s = " ^ |
621 " (let e__s = " ^ |
622 " ((Try (Rewrite_Set norm_Rational False)) @@ " ^ |
622 " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^ |
623 " (Repeat (Rewrite commute_0_equality False)) @@ " ^ |
623 " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^ |
624 " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ |
624 " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^ |
625 " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ |
625 " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^ |
626 " simplify_System_parenthesized False)) @@ " ^ |
626 " ''simplify_System_parenthesized'' False)) @@ " ^ |
627 " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ |
627 " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^ |
628 " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ |
628 " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^ |
629 " isolate_bdvs_4x4 False)) @@ " ^ |
629 " ''isolate_bdvs_4x4'' False)) @@ " ^ |
630 " (Try (Rewrite_Set_Inst [(bdv_1, NTH 1 v_s),(bdv_2, NTH 2 v_s ), " ^ |
630 " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^ |
631 " (bdv_3, NTH 3 v_s),(bdv_3, NTH 4 v_s )] " ^ |
631 " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^ |
632 " simplify_System_parenthesized False)) @@ " ^ |
632 " ''simplify_System_parenthesized'' False)) @@ " ^ |
633 " (Try (Rewrite_Set order_system False))) e_s " ^ |
633 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^ |
634 " in (SubProblem (EqSystem',[LINEAR,system],[no_met]) " ^ |
634 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^ |
635 " [BOOL_LIST e__s, REAL_LIST v_s]))")] |
635 " [BOOL_LIST e__s, REAL_LIST v_s]))")] |
636 \<close> |
636 \<close> |
637 setup \<open>KEStore_Elems.add_mets |
637 setup \<open>KEStore_Elems.add_mets |
638 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID |
638 [Specify.prep_met thy "met_eqsys_topdown_4x4" [] Celem.e_metID |
639 (["EqSystem","top_down_substitution","4x4"], |
639 (["EqSystem","top_down_substitution","4x4"], |
652 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
652 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
653 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
653 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
654 " (let e_1 = NTH 1 e_s; " ^ |
654 " (let e_1 = NTH 1 e_s; " ^ |
655 " e_2 = Take (NTH 2 e_s); " ^ |
655 " e_2 = Take (NTH 2 e_s); " ^ |
656 " e_2 = ((Substitute [e_1]) @@ " ^ |
656 " e_2 = ((Substitute [e_1]) @@ " ^ |
657 " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ |
657 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^ |
658 " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ |
658 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^ |
659 " simplify_System_parenthesized False)) @@ " ^ |
659 " ''simplify_System_parenthesized'' False)) @@ " ^ |
660 " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ |
660 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^ |
661 " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ |
661 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^ |
662 " isolate_bdvs False)) @@ " ^ |
662 " ''isolate_bdvs'' False)) @@ " ^ |
663 " (Try (Rewrite_Set_Inst [(bdv_1,NTH 1 v_s),(bdv_2,NTH 2 v_s)," ^ |
663 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^ |
664 " (bdv_3,NTH 3 v_s),(bdv_4,NTH 4 v_s)]" ^ |
664 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^ |
665 " norm_Rational False))) e_2 " ^ |
665 " ''norm_Rational'' False))) e_2 " ^ |
666 " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")] |
666 " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])")] |
667 \<close> |
667 \<close> |
668 |
668 |
669 end |
669 end |