437 ML \<open> |
437 ML \<open> |
438 (*make () dissappear*) |
438 (*make () dissappear*) |
439 val rearrange_assoc = |
439 val rearrange_assoc = |
440 Rule_Def.Repeat{ |
440 Rule_Def.Repeat{ |
441 id = "rearrange_assoc", preconds = [], |
441 id = "rearrange_assoc", preconds = [], |
442 rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
442 rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
443 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [], |
443 erls = Rule_Set.empty, srls = Rule_Set.empty, calc = [], errpatts = [], |
444 rules = [ |
444 rules = [ |
445 \<^rule_thm_sym>\<open>add.assoc\<close>, |
445 \<^rule_thm_sym>\<open>add.assoc\<close>, |
446 \<^rule_thm_sym>\<open>rmult_assoc\<close>], |
446 \<^rule_thm_sym>\<open>rmult_assoc\<close>], |
447 scr = Rule.Empty_Prog}; |
447 scr = Rule.Empty_Prog}; |
459 \<^rule_thm>\<open>rmult_assoc\<close>], |
459 \<^rule_thm>\<open>rmult_assoc\<close>], |
460 scr = Rule.Empty_Prog}; |
460 scr = Rule.Empty_Prog}; |
461 |
461 |
462 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*) |
462 (*todo: replace by Rewrite("rnorm_equation_add", @{thm rnorm_equation_add)*) |
463 val norm_equation = |
463 val norm_equation = |
464 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
464 Rule_Def.Repeat{id = "norm_equation", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
465 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [], |
465 erls = tval_rls, srls = Rule_Set.empty, calc = [], errpatts = [], |
466 rules = [ |
466 rules = [ |
467 \<^rule_thm>\<open>rnorm_equation_add\<close>], |
467 \<^rule_thm>\<open>rnorm_equation_add\<close>], |
468 scr = Rule.Empty_Prog}; |
468 scr = Rule.Empty_Prog}; |
469 \<close> |
469 \<close> |
523 scr = Rule.Empty_Prog}; |
523 scr = Rule.Empty_Prog}; |
524 \<close> |
524 \<close> |
525 ML \<open> |
525 ML \<open> |
526 (*isolate the root in a root-equation*) |
526 (*isolate the root in a root-equation*) |
527 val isolate_root = |
527 val isolate_root = |
528 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
528 Rule_Def.Repeat{id = "isolate_root", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
529 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [], |
529 erls=tval_rls,srls = Rule_Set.empty, calc=[], errpatts = [], |
530 rules = [ |
530 rules = [ |
531 \<^rule_thm>\<open>rroot_to_lhs\<close>, |
531 \<^rule_thm>\<open>rroot_to_lhs\<close>, |
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>, |
532 \<^rule_thm>\<open>rroot_to_lhs_mult\<close>, |
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>, |
533 \<^rule_thm>\<open>rroot_to_lhs_add_mult\<close>, |
537 scr = Rule.Empty_Prog}; |
537 scr = Rule.Empty_Prog}; |
538 |
538 |
539 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
539 (*isolate the bound variable in an equation; 'bdv' is a meta-constant*) |
540 val isolate_bdv = |
540 val isolate_bdv = |
541 Rule_Def.Repeat{ |
541 Rule_Def.Repeat{ |
542 id = "isolate_bdv", preconds = [], rew_ord = ("e_rew_ord",Rewrite_Ord.e_rew_ord), |
542 id = "isolate_bdv", preconds = [], rew_ord = ("Rewrite_Ord.id_empty",Rewrite_Ord.function_empty), |
543 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [], |
543 erls=tval_rls,srls = Rule_Set.empty, calc= [], errpatts = [], |
544 rules = [ |
544 rules = [ |
545 \<^rule_thm>\<open>risolate_bdv_add\<close>, |
545 \<^rule_thm>\<open>risolate_bdv_add\<close>, |
546 \<^rule_thm>\<open>risolate_bdv_mult_add\<close>, |
546 \<^rule_thm>\<open>risolate_bdv_mult_add\<close>, |
547 \<^rule_thm>\<open>risolate_bdv_mult\<close>, |
547 \<^rule_thm>\<open>risolate_bdv_mult\<close>, |
775 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #> |
775 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #> |
776 (Rewrite_Set ''Test_simplify'')) e_e |
776 (Rewrite_Set ''Test_simplify'')) e_e |
777 in |
777 in |
778 [e_e])" |
778 [e_e])" |
779 method met_test_solvelin : "Test/solve_linear" = |
779 method met_test_solvelin : "Test/solve_linear" = |
780 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, |
780 \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, |
781 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [], |
781 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [], |
782 nrls = Test_simplify}\<close> |
782 nrls = Test_simplify}\<close> |
783 Program: solve_linear.simps |
783 Program: solve_linear.simps |
784 Given: "equality e_e" "solveFor v_v" |
784 Given: "equality e_e" "solveFor v_v" |
785 Where: "matches (?a = ?b) e_e" |
785 Where: "matches (?a = ?b) e_e" |
806 in |
806 in |
807 [e_e])" |
807 [e_e])" |
808 |
808 |
809 method met_test_sqrt : "Test/sqrt-equ-test" = |
809 method met_test_sqrt : "Test/sqrt-equ-test" = |
810 (*root-equation, version for tests before 8.01.01*) |
810 (*root-equation, version for tests before 8.01.01*) |
811 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
811 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls, |
812 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
812 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
813 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
813 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
814 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty |
814 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty |
815 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
815 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
816 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[], |
816 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[], |
832 in |
832 in |
833 Check_elementwise L_L {(v_v::real). Assumptions})" |
833 Check_elementwise L_L {(v_v::real). Assumptions})" |
834 |
834 |
835 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" = |
835 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" = |
836 (*tests subproblem fixed linear*) |
836 (*tests subproblem fixed linear*) |
837 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, |
837 \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, |
838 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty |
838 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty |
839 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")], |
839 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")], |
840 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close> |
840 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close> |
841 Program: minisubpbl.simps |
841 Program: minisubpbl.simps |
842 Given: "equality e_e" "solveFor v_v" |
842 Given: "equality e_e" "solveFor v_v" |
862 in |
862 in |
863 Check_elementwise L_L {(v_v::real). Assumptions}) " |
863 Check_elementwise L_L {(v_v::real). Assumptions}) " |
864 |
864 |
865 method met_test_eq1 : "Test/square_equation1" = |
865 method met_test_eq1 : "Test/square_equation1" = |
866 (*root-equation1:*) |
866 (*root-equation1:*) |
867 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
867 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls, |
868 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
868 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
869 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
869 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
870 prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close> |
870 prls=Rule_Set.empty, calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close> |
871 Program: solve_root_equ2.simps |
871 Program: solve_root_equ2.simps |
872 Given: "equality e_e" "solveFor v_v" |
872 Given: "equality e_e" "solveFor v_v" |
892 in |
892 in |
893 Check_elementwise L_L {(v_v::real). Assumptions})" |
893 Check_elementwise L_L {(v_v::real). Assumptions})" |
894 |
894 |
895 method met_test_squ2 : "Test/square_equation2" = |
895 method met_test_squ2 : "Test/square_equation2" = |
896 (*root-equation2*) |
896 (*root-equation2*) |
897 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
897 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls, |
898 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
898 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
899 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
899 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
900 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close> |
900 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close> |
901 Program: solve_root_equ3.simps |
901 Program: solve_root_equ3.simps |
902 Given: "equality e_e" "solveFor v_v" |
902 Given: "equality e_e" "solveFor v_v" |
922 in |
922 in |
923 Check_elementwise L_L {(v_v::real). Assumptions})" |
923 Check_elementwise L_L {(v_v::real). Assumptions})" |
924 |
924 |
925 method met_test_squeq : "Test/square_equation" = |
925 method met_test_squeq : "Test/square_equation" = |
926 (*root-equation*) |
926 (*root-equation*) |
927 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
927 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls, |
928 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
928 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
929 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
929 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
930 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close> |
930 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty}\<close> |
931 Program: solve_root_equ4.simps |
931 Program: solve_root_equ4.simps |
932 Given: "equality e_e" "solveFor v_v" |
932 Given: "equality e_e" "solveFor v_v" |
945 in |
945 in |
946 Or_to_List e_e)" |
946 Or_to_List e_e)" |
947 |
947 |
948 method met_test_eq_plain : "Test/solve_plain_square" = |
948 method met_test_eq_plain : "Test/solve_plain_square" = |
949 (*solve_plain_square*) |
949 (*solve_plain_square*) |
950 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty, |
950 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,calc=[],srls=Rule_Set.empty, |
951 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*, |
951 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*, |
952 asm_rls=[],asm_thm=[]*)}\<close> |
952 asm_rls=[],asm_thm=[]*)}\<close> |
953 Program: solve_plain_square.simps |
953 Program: solve_plain_square.simps |
954 Given: "equality e_e" "solveFor v_v" |
954 Given: "equality e_e" "solveFor v_v" |
955 Where: |
955 Where: |
972 in |
972 in |
973 SubProblem (''Test'', [''univariate'', ''equation'', ''test''], |
973 SubProblem (''Test'', [''univariate'', ''equation'', ''test''], |
974 [''no_met'']) [BOOL e_e, REAL v_v])" |
974 [''no_met'']) [BOOL e_e, REAL v_v])" |
975 |
975 |
976 method met_test_norm_univ : "Test/norm_univar_equation" = |
976 method met_test_norm_univ : "Test/norm_univar_equation" = |
977 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls, |
977 \<open>{rew_ord'="Rewrite_Ord.id_empty",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls, |
978 errpats = [], nrls = Rule_Set.empty}\<close> |
978 errpats = [], nrls = Rule_Set.empty}\<close> |
979 Program: norm_univariate_equ.simps |
979 Program: norm_univariate_equ.simps |
980 Given: "equality e_e" "solveFor v_v" |
980 Given: "equality e_e" "solveFor v_v" |
981 Where: |
981 Where: |
982 Find: "solutions v_v'i'" |
982 Find: "solutions v_v'i'" |
990 Repeat ( |
990 Repeat ( |
991 (Try (Calculate ''PLUS'')) #> |
991 (Try (Calculate ''PLUS'')) #> |
992 (Try (Calculate ''TIMES''))) t_t)" |
992 (Try (Calculate ''TIMES''))) t_t)" |
993 |
993 |
994 method met_test_intsimp : "Test/intsimp" = |
994 method met_test_intsimp : "Test/intsimp" = |
995 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], |
995 \<open>{rew_ord' = "Rewrite_Ord.id_empty", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], |
996 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close> |
996 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close> |
997 Program: test_simplify.simps |
997 Program: test_simplify.simps |
998 Given: "intTestGiven t_t" |
998 Given: "intTestGiven t_t" |
999 Where: |
999 Where: |
1000 Find: "intTestFind s_s" |
1000 Find: "intTestFind s_s" |