841 Repeat ( |
841 Repeat ( |
842 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #> |
842 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'') #> |
843 (Rewrite_Set ''Test_simplify'')) e_e |
843 (Rewrite_Set ''Test_simplify'')) e_e |
844 in |
844 in |
845 [e_e])" |
845 [e_e])" |
846 setup \<open>KEStore_Elems.add_mets |
846 method met_test_solvelin : "Test/solve_linear" = |
847 [MethodC.prep_input @{theory} "met_test_solvelin" [] MethodC.id_empty |
847 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, |
848 (["Test", "solve_linear"], |
848 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [], |
849 [("#Given" ,["equality e_e", "solveFor v_v"]), |
849 nrls = Test_simplify}\<close> |
850 ("#Where" ,["matches (?a = ?b) e_e"]), |
850 Program: solve_linear.simps |
851 ("#Find" ,["solutions v_v'i'"])], |
851 Given: "equality e_e" "solveFor v_v" |
852 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, |
852 Where: "matches (?a = ?b) e_e" |
853 prls = assoc_rls' @{theory} "matches", calc = [], crls = tval_rls, errpats = [], |
853 Find: "solutions v_v'i'" |
854 nrls = Test_simplify}, |
854 |
855 @{thm solve_linear.simps})] |
|
856 \<close> |
|
857 subsection \<open>root equation\<close> |
855 subsection \<open>root equation\<close> |
858 |
856 |
859 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
857 partial_function (tailrec) solve_root_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
860 where |
858 where |
861 "solve_root_equ e_e v_v = ( |
859 "solve_root_equ e_e v_v = ( |
872 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #> |
870 (Rewrite_Set_Inst [(''bdv'', v_v)] ''isolate_bdv'' ) #> |
873 (Try (Rewrite_Set ''Test_simplify'' )) |
871 (Try (Rewrite_Set ''Test_simplify'' )) |
874 ) e_e |
872 ) e_e |
875 in |
873 in |
876 [e_e])" |
874 [e_e])" |
877 setup \<open>KEStore_Elems.add_mets |
875 |
878 [MethodC.prep_input @{theory} "met_test_sqrt" [] MethodC.id_empty |
876 method met_test_sqrt : "Test/sqrt-equ-test" = |
879 (*root-equation, version for tests before 8.01.01*) |
877 (*root-equation, version for tests before 8.01.01*) |
880 (["Test", "sqrt-equ-test"], |
878 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
881 [("#Given" ,["equality e_e", "solveFor v_v"]), |
879 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
882 ("#Where" ,["contains_root (e_e::bool)"]), |
880 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
883 ("#Find" ,["solutions v_v'i'"])], |
881 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty |
884 {rew_ord'="e_rew_ord",rls'=tval_rls, |
882 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
885 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
883 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[], |
886 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
884 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close> |
887 prls = Rule_Set.append_rules "prls_contains_root" Rule_Set.empty |
885 Program: solve_root_equ.simps |
888 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root "")], |
886 Given: "equality e_e" "solveFor v_v" |
889 calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[], |
887 Where: "contains_root (e_e::bool)" |
890 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}, |
888 Find: "solutions v_v'i'" |
891 @{thm solve_root_equ.simps})] |
|
892 \<close> |
|
893 |
889 |
894 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
890 partial_function (tailrec) minisubpbl :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
895 where |
891 where |
896 "minisubpbl e_e v_v = ( |
892 "minisubpbl e_e v_v = ( |
897 let |
893 let |
900 (Try (Rewrite_Set ''Test_simplify'' ))) e_e; |
896 (Try (Rewrite_Set ''Test_simplify'' ))) e_e; |
901 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''], |
897 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''], |
902 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v] |
898 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v] |
903 in |
899 in |
904 Check_elementwise L_L {(v_v::real). Assumptions})" |
900 Check_elementwise L_L {(v_v::real). Assumptions})" |
905 setup \<open>KEStore_Elems.add_mets |
901 |
906 [MethodC.prep_input @{theory} "met_test_squ_sub" [] MethodC.id_empty |
902 method met_test_squ_sub : "Test/squ-equ-test-subpbl1" = |
907 (*tests subproblem fixed linear*) |
903 (*tests subproblem fixed linear*) |
908 (["Test", "squ-equ-test-subpbl1"], |
904 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, |
909 [("#Given" ,["equality e_e", "solveFor v_v"]), |
|
910 ("#Where" ,["precond_rootmet v_v"]), |
|
911 ("#Find" ,["solutions v_v'i'"])], |
|
912 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, |
|
913 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty |
905 prls = Rule_Set.append_rules "prls_met_test_squ_sub" Rule_Set.empty |
914 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")], |
906 [\<^rule_eval>\<open>precond_rootmet\<close> (eval_precond_rootmet "")], |
915 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}, |
907 calc=[], crls=tval_rls, errpats = [], nrls = Test_simplify}\<close> |
916 @{thm minisubpbl.simps})] |
908 Program: minisubpbl.simps |
917 \<close> |
909 Given: "equality e_e" "solveFor v_v" |
|
910 Where: "precond_rootmet v_v" |
|
911 Find: "solutions v_v'i'" |
918 |
912 |
919 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
913 partial_function (tailrec) solve_root_equ2 :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
920 where |
914 where |
921 "solve_root_equ2 e_e v_v = ( |
915 "solve_root_equ2 e_e v_v = ( |
922 let |
916 let |
932 ) e_e; |
926 ) e_e; |
933 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''], |
927 L_L = SubProblem (''Test'', [''LINEAR'', ''univariate'', ''equation'', ''test''], |
934 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v] |
928 [''Test'', ''solve_linear'']) [BOOL e_e, REAL v_v] |
935 in |
929 in |
936 Check_elementwise L_L {(v_v::real). Assumptions}) " |
930 Check_elementwise L_L {(v_v::real). Assumptions}) " |
937 setup \<open>KEStore_Elems.add_mets |
931 |
938 [MethodC.prep_input @{theory} "met_test_eq1" [] MethodC.id_empty |
932 method met_test_eq1 : "Test/square_equation1" = |
939 (*root-equation1:*) |
933 (*root-equation1:*) |
940 (["Test", "square_equation1"], |
934 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
941 [("#Given" ,["equality e_e", "solveFor v_v"]), |
935 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
942 ("#Find" ,["solutions v_v'i'"])], |
936 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls, |
943 {rew_ord'="e_rew_ord",rls'=tval_rls, |
937 errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""), |
944 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
938 ("square_equation_right", "")]*)}\<close> |
945 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], prls=Rule_Set.empty, calc=[], crls=tval_rls, |
939 Program: solve_root_equ2.simps |
946 errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], asm_thm=[("square_equation_left", ""), |
940 Given: "equality e_e" "solveFor v_v" |
947 ("square_equation_right", "")]*)}, |
941 Find: "solutions v_v'i'" |
948 @{thm solve_root_equ2.simps})] |
|
949 \<close> |
|
950 |
942 |
951 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
943 partial_function (tailrec) solve_root_equ3 :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
952 where |
944 where |
953 "solve_root_equ3 e_e v_v = ( |
945 "solve_root_equ3 e_e v_v = ( |
954 let |
946 let |
965 ) e_e; |
957 ) e_e; |
966 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''], |
958 L_L = SubProblem (''Test'', [''plain_square'', ''univariate'', ''equation'', ''test''], |
967 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v] |
959 [''Test'', ''solve_plain_square'']) [BOOL e_e, REAL v_v] |
968 in |
960 in |
969 Check_elementwise L_L {(v_v::real). Assumptions})" |
961 Check_elementwise L_L {(v_v::real). Assumptions})" |
970 setup \<open>KEStore_Elems.add_mets |
962 |
971 [MethodC.prep_input @{theory} "met_test_squ2" [] MethodC.id_empty |
963 method met_test_squ2 : "Test/square_equation2" = |
972 (*root-equation2*) |
964 (*root-equation2*) |
973 (["Test", "square_equation2"], |
965 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
974 [("#Given" ,["equality e_e", "solveFor v_v"]), |
966 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
975 ("#Find" ,["solutions v_v'i'"])], |
967 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
976 {rew_ord'="e_rew_ord",rls'=tval_rls, |
968 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], |
977 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
969 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close> |
978 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
970 Program: solve_root_equ3.simps |
979 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*,asm_rls=[], |
971 Given: "equality e_e" "solveFor v_v" |
980 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}, |
972 Find: "solutions v_v'i'" |
981 @{thm solve_root_equ3.simps})] |
|
982 \<close> |
|
983 |
973 |
984 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
974 partial_function (tailrec) solve_root_equ4 :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
985 where |
975 where |
986 "solve_root_equ4 e_e v_v = ( |
976 "solve_root_equ4 e_e v_v = ( |
987 let |
977 let |
998 ) e_e; |
988 ) e_e; |
999 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''], |
989 L_L = SubProblem (''Test'', [''univariate'', ''equation'', ''test''], |
1000 [''no_met'']) [BOOL e_e, REAL v_v] |
990 [''no_met'']) [BOOL e_e, REAL v_v] |
1001 in |
991 in |
1002 Check_elementwise L_L {(v_v::real). Assumptions})" |
992 Check_elementwise L_L {(v_v::real). Assumptions})" |
1003 setup \<open>KEStore_Elems.add_mets |
993 |
1004 [MethodC.prep_input @{theory} "met_test_squeq" [] MethodC.id_empty |
994 method met_test_squeq : "Test/square_equation" = |
1005 (*root-equation*) |
995 (*root-equation*) |
1006 (["Test", "square_equation"], |
996 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls, |
1007 [("#Given" ,["equality e_e", "solveFor v_v"]), |
997 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
1008 ("#Find" ,["solutions v_v'i'"])], |
998 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
1009 {rew_ord'="e_rew_ord",rls'=tval_rls, |
999 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[], |
1010 srls = Rule_Set.append_rules "srls_contains_root" Rule_Set.empty |
1000 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}\<close> |
1011 [\<^rule_eval>\<open>contains_root\<close> (eval_contains_root"")], |
1001 Program: solve_root_equ4.simps |
1012 prls=Rule_Set.empty,calc=[], crls=tval_rls, errpats = [], nrls = Rule_Set.empty (*,asm_rls=[], |
1002 Given: "equality e_e" "solveFor v_v" |
1013 asm_thm=[("square_equation_left", ""), ("square_equation_right", "")]*)}, |
1003 Find: "solutions v_v'i'" |
1014 @{thm solve_root_equ4.simps})] |
|
1015 \<close> |
|
1016 |
1004 |
1017 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
1005 partial_function (tailrec) solve_plain_square :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
1018 where |
1006 where |
1019 "solve_plain_square e_e v_v = ( |
1007 "solve_plain_square e_e v_v = ( |
1020 let |
1008 let |
1024 ((Rewrite ''square_equality_0'' ) Or |
1012 ((Rewrite ''square_equality_0'' ) Or |
1025 (Rewrite ''square_equality'' )) #> |
1013 (Rewrite ''square_equality'' )) #> |
1026 (Try (Rewrite_Set ''tval_rls'' ))) e_e |
1014 (Try (Rewrite_Set ''tval_rls'' ))) e_e |
1027 in |
1015 in |
1028 Or_to_List e_e)" |
1016 Or_to_List e_e)" |
1029 setup \<open>KEStore_Elems.add_mets |
1017 |
1030 [MethodC.prep_input @{theory} "met_test_eq_plain" [] MethodC.id_empty |
1018 method met_test_eq_plain : "Test/solve_plain_square" = |
1031 (*solve_plain_square*) |
1019 (*solve_plain_square*) |
1032 (["Test", "solve_plain_square"], |
1020 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty, |
1033 [("#Given",["equality e_e", "solveFor v_v"]), |
1021 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*, |
1034 ("#Where" ,["(matches (?a + ?b*v_v \<up> 2 = 0) e_e) |" ^ |
1022 asm_rls=[],asm_thm=[]*)}\<close> |
1035 "(matches ( ?b*v_v \<up> 2 = 0) e_e) |" ^ |
1023 Program: solve_plain_square.simps |
1036 "(matches (?a + v_v \<up> 2 = 0) e_e) |" ^ |
1024 Given: "equality e_e" "solveFor v_v" |
1037 "(matches ( v_v \<up> 2 = 0) e_e)"]), |
1025 Where: |
1038 ("#Find" ,["solutions v_v'i'"])], |
1026 "(matches (?a + ?b*v_v \<up> 2 = 0) e_e) | |
1039 {rew_ord'="e_rew_ord",rls'=tval_rls,calc=[],srls=Rule_Set.empty, |
1027 (matches ( ?b*v_v \<up> 2 = 0) e_e) | |
1040 prls = assoc_rls' @{theory} "matches", crls=tval_rls, errpats = [], nrls = Rule_Set.empty(*, |
1028 (matches (?a + v_v \<up> 2 = 0) e_e) | |
1041 asm_rls=[],asm_thm=[]*)}, |
1029 (matches ( v_v \<up> 2 = 0) e_e)" |
1042 @{thm solve_plain_square.simps})] |
1030 Find: "solutions v_v'i'" |
1043 \<close> |
1031 |
|
1032 |
1044 subsection \<open>polynomial equation\<close> |
1033 subsection \<open>polynomial equation\<close> |
1045 |
1034 |
1046 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
1035 partial_function (tailrec) norm_univariate_equ :: "bool \<Rightarrow> real \<Rightarrow> bool list" |
1047 where |
1036 where |
1048 "norm_univariate_equ e_e v_v = ( |
1037 "norm_univariate_equ e_e v_v = ( |
1051 (Try (Rewrite ''rnorm_equation_add'' )) #> |
1040 (Try (Rewrite ''rnorm_equation_add'' )) #> |
1052 (Try (Rewrite_Set ''Test_simplify'' )) ) e_e |
1041 (Try (Rewrite_Set ''Test_simplify'' )) ) e_e |
1053 in |
1042 in |
1054 SubProblem (''Test'', [''univariate'', ''equation'', ''test''], |
1043 SubProblem (''Test'', [''univariate'', ''equation'', ''test''], |
1055 [''no_met'']) [BOOL e_e, REAL v_v])" |
1044 [''no_met'']) [BOOL e_e, REAL v_v])" |
1056 setup \<open>KEStore_Elems.add_mets |
1045 |
1057 [MethodC.prep_input @{theory} "met_test_norm_univ" [] MethodC.id_empty |
1046 method met_test_norm_univ : "Test/norm_univar_equation" = |
1058 (["Test", "norm_univar_equation"], |
1047 \<open>{rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls, |
1059 [("#Given",["equality e_e", "solveFor v_v"]), |
1048 errpats = [], nrls = Rule_Set.empty}\<close> |
1060 ("#Where" ,[]), |
1049 Program: norm_univariate_equ.simps |
1061 ("#Find" ,["solutions v_v'i'"])], |
1050 Given: "equality e_e" "solveFor v_v" |
1062 {rew_ord'="e_rew_ord",rls'=tval_rls,srls = Rule_Set.empty,prls=Rule_Set.empty, calc=[], crls=tval_rls, |
1051 Where: |
1063 errpats = [], nrls = Rule_Set.empty}, |
1052 Find: "solutions v_v'i'" |
1064 @{thm norm_univariate_equ.simps})] |
1053 |
1065 \<close> |
1054 |
1066 subsection \<open>diophantine equation\<close> |
1055 subsection \<open>diophantine equation\<close> |
1067 |
1056 |
1068 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int" |
1057 partial_function (tailrec) test_simplify :: "int \<Rightarrow> int" |
1069 where |
1058 where |
1070 "test_simplify t_t = ( |
1059 "test_simplify t_t = ( |
1071 Repeat ( |
1060 Repeat ( |
1072 (Try (Calculate ''PLUS'')) #> |
1061 (Try (Calculate ''PLUS'')) #> |
1073 (Try (Calculate ''TIMES''))) t_t)" |
1062 (Try (Calculate ''TIMES''))) t_t)" |
1074 setup \<open>KEStore_Elems.add_mets |
1063 |
1075 [MethodC.prep_input @{theory} "met_test_intsimp" [] MethodC.id_empty |
1064 method met_test_intsimp : "Test/intsimp" = |
1076 (["Test", "intsimp"], |
1065 \<open>{rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], |
1077 [("#Given" ,["intTestGiven t_t"]), |
1066 crls = tval_rls, errpats = [], nrls = Test_simplify}\<close> |
1078 ("#Where" ,[]), |
1067 Program: test_simplify.simps |
1079 ("#Find" ,["intTestFind s_s"])], |
1068 Given: "intTestGiven t_t" |
1080 {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = Rule_Set.empty, prls = Rule_Set.empty, calc = [], |
1069 Where: |
1081 crls = tval_rls, errpats = [], nrls = Test_simplify}, |
1070 Find: "intTestFind s_s" |
1082 @{thm test_simplify.simps})] |
1071 |
1083 \<close> ML \<open> |
1072 ML \<open> |
1084 \<close> |
1073 \<close> |
1085 |
1074 |
1086 end |
1075 end |