15 solveForVars :: "real list => toreall" |
15 solveForVars :: "real list => toreall" |
16 solution :: "bool list => toreall" |
16 solution :: "bool list => toreall" |
17 |
17 |
18 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*) |
18 (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*) |
19 solveSystem :: "[bool list, real list] => bool list" |
19 solveSystem :: "[bool list, real list] => bool list" |
20 |
|
21 (*Script-names*) |
|
22 SolveSystemScript :: "[bool list, real list, bool list] |
|
23 => bool list" |
|
24 ("((Script SolveSystemScript (_ _ =))// (_))" 9) |
|
25 |
20 |
26 axiomatization where |
21 axiomatization where |
27 (*stated as axioms, todo: prove as theorems |
22 (*stated as axioms, todo: prove as theorems |
28 'bdv' is a constant handled on the meta-level |
23 'bdv' is a constant handled on the meta-level |
29 specifically as a 'bound variable' *) |
24 specifically as a 'bound variable' *) |
558 srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls |
553 srls = Rule.append_rls "srls_top_down_2x2" Rule.e_rls |
559 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
554 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
560 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
555 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
561 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
556 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
562 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
557 prls = prls_triangular, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
563 @{thm solve_system.simps} |
558 @{thm solve_system.simps})] |
564 (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
|
565 " (let e_1 = Take (hd e_s); " ^ |
|
566 " e_1 = ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
567 " ''isolate_bdvs'' False)) @@ " ^ |
|
568 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
569 " ''simplify_System'' False))) e_1; " ^ |
|
570 " e_2 = Take (hd (tl e_s)); " ^ |
|
571 " e_2 = ((Substitute [e_1]) @@ " ^ |
|
572 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
573 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
574 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
575 " ''isolate_bdvs'' False)) @@ " ^ |
|
576 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
577 " ''simplify_System'' False))) e_2; " ^ |
|
578 " e__s = Take [e_1, e_2] " ^ |
|
579 " in (Try (Rewrite_Set ''order_system'' False)) e__s)"*) |
|
580 (*--------------------------------------------------------------------------- |
|
581 this script does NOT separate the equations as above, |
|
582 but it does not yet work due to preliminary script-interpreter, |
|
583 see eqsystem.sml 'script [EqSystem,top_down_substitution,2x2] Vers.2' |
|
584 |
|
585 "Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
|
586 " (let e__s = Take e_s; " ^ |
|
587 " e_1 = hd e__s; " ^ |
|
588 " e_2 = hd (tl e__s); " ^ |
|
589 " e__s = [e_1, Substitute [e_1] e_2] " ^ |
|
590 " in ((Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
591 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
592 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))] " ^ |
|
593 " ''isolate_bdvs'' False)) @@ " ^ |
|
594 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
595 " ''simplify_System'' False))) e__s)" |
|
596 ---------------------------------------------------------------------------*))] |
|
597 \<close> |
559 \<close> |
598 setup \<open>KEStore_Elems.add_mets |
560 setup \<open>KEStore_Elems.add_mets |
599 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID |
561 [Specify.prep_met thy "met_eqsys_norm" [] Celem.e_metID |
600 (["EqSystem", "normalise"], [], |
562 (["EqSystem", "normalise"], [], |
601 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, |
563 {rew_ord'="tless_true", rls' = Rule.Erls, calc = [], srls = Rule.Erls, prls = Rule.Erls, crls = Rule.Erls, |
625 srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls |
587 srls = Rule.append_rls "srls_normalise_2x2" Rule.e_rls |
626 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
588 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
627 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
589 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
628 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
590 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
629 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
591 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
630 @{thm solve_system2.simps} |
592 @{thm solve_system2.simps})] |
631 (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
|
632 " (let e__s = ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^ |
|
633 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
634 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
635 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
636 " ''isolate_bdvs'' False)) @@ " ^ |
|
637 " (Try (Rewrite_Set_Inst [(''bdv_1'', hd v_s),(''bdv_2'', hd (tl v_s))]" ^ |
|
638 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
639 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^ |
|
640 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^ |
|
641 " [BOOL_LIST e__s, REAL_LIST v_s]))"*))] |
|
642 \<close> |
593 \<close> |
643 |
594 |
644 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list" |
595 partial_function (tailrec) solve_system3 :: "bool list => real list => bool list" |
645 where |
596 where |
646 "solve_system3 e_s v_s = |
597 "solve_system3 e_s v_s = |
669 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
620 [Rule.Thm ("hd_thm",TermC.num_str @{thm hd_thm}), |
670 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
621 Rule.Thm ("tl_Cons",TermC.num_str @{thm tl_Cons}), |
671 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
622 Rule.Thm ("tl_Nil",TermC.num_str @{thm tl_Nil})], |
672 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
623 prls = Rule.Erls, crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
673 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
624 (*STOPPED.WN06? met ["EqSystem","normalise","4x4"] @@@@@@@@@@@@@@@@@@@@@@@@@@@*) |
674 @{thm solve_system3.simps} |
625 @{thm solve_system3.simps})] |
675 (*""Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
|
676 " (let e__s = " ^ |
|
677 " ((Try (Rewrite_Set ''norm_Rational'' False)) @@ " ^ |
|
678 " (Repeat (Rewrite ''commute_0_equality'' False)) @@ " ^ |
|
679 " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^ |
|
680 " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^ |
|
681 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
682 " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^ |
|
683 " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^ |
|
684 " ''isolate_bdvs_4x4'' False)) @@ " ^ |
|
685 " (Try (Rewrite_Set_Inst [(''bdv_1'', NTH 1 v_s),(''bdv_2'', NTH 2 v_s ), " ^ |
|
686 " (''bdv_3'', NTH 3 v_s),(''bdv_3'', NTH 4 v_s )] " ^ |
|
687 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
688 " (Try (Rewrite_Set ''order_system'' False))) e_s " ^ |
|
689 " in (SubProblem (''EqSystem'',[''LINEAR'',''system''],[''no_met'']) " ^ |
|
690 " [BOOL_LIST e__s, REAL_LIST v_s]))"*))] |
|
691 \<close> |
626 \<close> |
692 |
627 |
693 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list" |
628 partial_function (tailrec) solve_system4 :: "bool list => real list => bool list" |
694 where |
629 where |
695 "solve_system4 e_s v_s = |
630 "solve_system4 e_s v_s = |
720 srls = Rule.append_rls "srls_top_down_4x4" srls [], |
655 srls = Rule.append_rls "srls_top_down_4x4" srls [], |
721 prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular |
656 prls = Rule.append_rls "prls_tri_4x4_lin_sys" prls_triangular |
722 [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")], |
657 [Rule.Calc ("Atools.occurs'_in",eval_occurs_in "")], |
723 crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
658 crls = Rule.Erls, errpats = [], nrls = Rule.Erls}, |
724 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
659 (*FIXXXXME.WN060916: this script works ONLY for exp 7.79 @@@@@@@@@@@@@@@@@@@@*) |
725 @{thm solve_system4.simps} |
660 @{thm solve_system4.simps})] |
726 (*"Script SolveSystemScript (e_s::bool list) (v_s::real list) = " ^ |
|
727 " (let e_1 = NTH 1 e_s; " ^ |
|
728 " e_2 = Take (NTH 2 e_s); " ^ |
|
729 " e_2 = ((Substitute [e_1]) @@ " ^ |
|
730 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^ |
|
731 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^ |
|
732 " ''simplify_System_parenthesized'' False)) @@ " ^ |
|
733 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^ |
|
734 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^ |
|
735 " ''isolate_bdvs'' False)) @@ " ^ |
|
736 " (Try (Rewrite_Set_Inst [(''bdv_1'',NTH 1 v_s),(''bdv_2'',NTH 2 v_s)," ^ |
|
737 " (''bdv_3'',NTH 3 v_s),(''bdv_4'',NTH 4 v_s)]" ^ |
|
738 " ''norm_Rational'' False))) e_2 " ^ |
|
739 " in [e_1, e_2, NTH 3 e_s, NTH 4 e_s])"*))] |
|
740 \<close> |
661 \<close> |
741 |
662 |
742 end |
663 end |