1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy Thu Jun 10 11:54:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy Thu Jun 10 12:23:57 2021 +0200
1.3 @@ -770,7 +770,7 @@
1.4 d4_polyeq_simplify = d4_polyeq_simplify
1.5
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Problem.prep_input thy "pbl_equ_univ_poly" [] Problem.id_empty
1.8 + [(Problem.prep_input @{theory} "pbl_equ_univ_poly" [] Problem.id_empty
1.9 (["polynomial", "univariate", "equation"],
1.10 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.11 ("#Where" ,["~((e_e::bool) is_ratequation_in (v_v::real))",
1.12 @@ -779,7 +779,7 @@
1.13 ("#Find" ,["solutions v_v'i'"])],
1.14 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
1.15 (*--- d0 ---*)
1.16 - (Problem.prep_input thy "pbl_equ_univ_poly_deg0" [] Problem.id_empty
1.17 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg0" [] Problem.id_empty
1.18 (["degree_0", "polynomial", "univariate", "equation"],
1.19 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.20 ("#Where" ,["matches (?a = 0) e_e",
1.21 @@ -788,7 +788,7 @@
1.22 ("#Find" ,["solutions v_v'i'"])],
1.23 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d0_polyeq_equation"]])),
1.24 (*--- d1 ---*)
1.25 - (Problem.prep_input thy "pbl_equ_univ_poly_deg1" [] Problem.id_empty
1.26 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg1" [] Problem.id_empty
1.27 (["degree_1", "polynomial", "univariate", "equation"],
1.28 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.29 ("#Where" ,["matches (?a = 0) e_e",
1.30 @@ -797,7 +797,7 @@
1.31 ("#Find" ,["solutions v_v'i'"])],
1.32 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d1_polyeq_equation"]])),
1.33 (*--- d2 ---*)
1.34 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2" [] Problem.id_empty
1.35 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2" [] Problem.id_empty
1.36 (["degree_2", "polynomial", "univariate", "equation"],
1.37 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.38 ("#Where" ,["matches (?a = 0) e_e",
1.39 @@ -805,7 +805,7 @@
1.40 "((lhs e_e) has_degree_in v_v ) = 2"]),
1.41 ("#Find" ,["solutions v_v'i'"])],
1.42 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_equation"]])),
1.43 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
1.44 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_sqonly" [] Problem.id_empty
1.45 (["sq_only", "degree_2", "polynomial", "univariate", "equation"],
1.46 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.47 ("#Where" ,["matches ( ?a + ?v_ \<up> 2 = 0) e_e | " ^
1.48 @@ -823,7 +823,7 @@
1.49 ("#Find" ,["solutions v_v'i'"])],
1.50 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.51 [["PolyEq", "solve_d2_polyeq_sqonly_equation"]])),
1.52 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
1.53 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_bdvonly" [] Problem.id_empty
1.54 (["bdv_only", "degree_2", "polynomial", "univariate", "equation"],
1.55 [("#Given", ["equality e_e", "solveFor v_v"]),
1.56 ("#Where", ["matches (?a*?v_ + ?v_ \<up> 2 = 0) e_e | " ^
1.57 @@ -835,14 +835,14 @@
1.58 ("#Find", ["solutions v_v'i'"])],
1.59 PolyEq_prls, SOME "solve (e_e::bool, v_v)",
1.60 [["PolyEq", "solve_d2_polyeq_bdvonly_equation"]])),
1.61 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
1.62 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_pq" [] Problem.id_empty
1.63 (["pqFormula", "degree_2", "polynomial", "univariate", "equation"],
1.64 [("#Given", ["equality e_e", "solveFor v_v"]),
1.65 ("#Where", ["matches (?a + 1*?v_ \<up> 2 = 0) e_e | " ^
1.66 "matches (?a + ?v_ \<up> 2 = 0) e_e"]),
1.67 ("#Find", ["solutions v_v'i'"])],
1.68 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_pq_equation"]])),
1.69 - (Problem.prep_input thy "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
1.70 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg2_abc" [] Problem.id_empty
1.71 (["abcFormula", "degree_2", "polynomial", "univariate", "equation"],
1.72 [("#Given", ["equality e_e", "solveFor v_v"]),
1.73 ("#Where", ["matches (?a + ?v_ \<up> 2 = 0) e_e | " ^
1.74 @@ -850,7 +850,7 @@
1.75 ("#Find", ["solutions v_v'i'"])],
1.76 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d2_polyeq_abc_equation"]])),
1.77 (*--- d3 ---*)
1.78 - (Problem.prep_input thy "pbl_equ_univ_poly_deg3" [] Problem.id_empty
1.79 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg3" [] Problem.id_empty
1.80 (["degree_3", "polynomial", "univariate", "equation"],
1.81 [("#Given", ["equality e_e", "solveFor v_v"]),
1.82 ("#Where", ["matches (?a = 0) e_e",
1.83 @@ -859,7 +859,7 @@
1.84 ("#Find", ["solutions v_v'i'"])],
1.85 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "solve_d3_polyeq_equation"]])),
1.86 (*--- d4 ---*)
1.87 - (Problem.prep_input thy "pbl_equ_univ_poly_deg4" [] Problem.id_empty
1.88 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_deg4" [] Problem.id_empty
1.89 (["degree_4", "polynomial", "univariate", "equation"],
1.90 [("#Given", ["equality e_e", "solveFor v_v"]),
1.91 ("#Where", ["matches (?a = 0) e_e",
1.92 @@ -868,7 +868,7 @@
1.93 ("#Find", ["solutions v_v'i'"])],
1.94 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [(*["PolyEq", "solve_d4_polyeq_equation"]*)])),
1.95 (*--- normalise ---*)
1.96 - (Problem.prep_input thy "pbl_equ_univ_poly_norm" [] Problem.id_empty
1.97 + (Problem.prep_input @{theory} "pbl_equ_univ_poly_norm" [] Problem.id_empty
1.98 (["normalise", "polynomial", "univariate", "equation"],
1.99 [("#Given", ["equality e_e", "solveFor v_v"]),
1.100 ("#Where", ["(Not((matches (?a = 0 ) e_e ))) |" ^
1.101 @@ -876,7 +876,7 @@
1.102 ("#Find", ["solutions v_v'i'"])],
1.103 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [["PolyEq", "normalise_poly"]])),
1.104 (*-------------------------expanded-----------------------*)
1.105 - (Problem.prep_input thy "pbl_equ_univ_expand" [] Problem.id_empty
1.106 + (Problem.prep_input @{theory} "pbl_equ_univ_expand" [] Problem.id_empty
1.107 (["expanded", "univariate", "equation"],
1.108 [("#Given", ["equality e_e", "solveFor v_v"]),
1.109 ("#Where", ["matches (?a = 0) e_e",
1.110 @@ -884,7 +884,7 @@
1.111 ("#Find", ["solutions v_v'i'"])],
1.112 PolyEq_prls, SOME "solve (e_e::bool, v_v)", [])),
1.113 (*--- d2 ---*)
1.114 - (Problem.prep_input thy "pbl_equ_univ_expand_deg2" [] Problem.id_empty
1.115 + (Problem.prep_input @{theory} "pbl_equ_univ_expand_deg2" [] Problem.id_empty
1.116 (["degree_2", "expanded", "univariate", "equation"],
1.117 [("#Given", ["equality e_e", "solveFor v_v"]),
1.118 ("#Where", ["((lhs e_e) has_degree_in v_v) = 2"]),
1.119 @@ -893,7 +893,7 @@
1.120
1.121 text \<open>"-------------------------methods-----------------------"\<close>
1.122 setup \<open>KEStore_Elems.add_mets
1.123 - [MethodC.prep_input thy "met_polyeq" [] MethodC.id_empty
1.124 + [MethodC.prep_input @{theory} "met_polyeq" [] MethodC.id_empty
1.125 (["PolyEq"], [],
1.126 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = Rule_Set.empty, prls=Rule_Set.empty,
1.127 crls=PolyEq_crls, errpats = [], nrls = norm_Rational},
1.128 @@ -914,7 +914,7 @@
1.129 SubProblem (''PolyEq'', [''polynomial'', ''univariate'', ''equation''], [''no_met''])
1.130 [BOOL e_e, REAL v_v])"
1.131 setup \<open>KEStore_Elems.add_mets
1.132 - [MethodC.prep_input thy "met_polyeq_norm" [] MethodC.id_empty
1.133 + [MethodC.prep_input @{theory} "met_polyeq_norm" [] MethodC.id_empty
1.134 (["PolyEq", "normalise_poly"],
1.135 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.136 ("#Where" ,["(Not((matches (?a = 0 ) e_e ))) | (Not(((lhs e_e) is_poly_in v_v)))"]),
1.137 @@ -932,7 +932,7 @@
1.138 in
1.139 Or_to_List e_e)"
1.140 setup \<open>KEStore_Elems.add_mets
1.141 - [MethodC.prep_input thy "met_polyeq_d0" [] MethodC.id_empty
1.142 + [MethodC.prep_input @{theory} "met_polyeq_d0" [] MethodC.id_empty
1.143 (["PolyEq", "solve_d0_polyeq_equation"],
1.144 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.145 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 0"]),
1.146 @@ -955,7 +955,7 @@
1.147 in
1.148 Check_elementwise L_L {(v_v::real). Assumptions})"
1.149 setup \<open>KEStore_Elems.add_mets
1.150 - [MethodC.prep_input thy "met_polyeq_d1" [] MethodC.id_empty
1.151 + [MethodC.prep_input @{theory} "met_polyeq_d1" [] MethodC.id_empty
1.152 (["PolyEq", "solve_d1_polyeq_equation"],
1.153 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.154 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 1"]),
1.155 @@ -980,7 +980,7 @@
1.156 in
1.157 Check_elementwise L_L {(v_v::real). Assumptions})"
1.158 setup \<open>KEStore_Elems.add_mets
1.159 - [MethodC.prep_input thy "met_polyeq_d22" [] MethodC.id_empty
1.160 + [MethodC.prep_input @{theory} "met_polyeq_d22" [] MethodC.id_empty
1.161 (["PolyEq", "solve_d2_polyeq_equation"],
1.162 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.163 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.164 @@ -1005,7 +1005,7 @@
1.165 in
1.166 Check_elementwise L_L {(v_v::real). Assumptions})"
1.167 setup \<open>KEStore_Elems.add_mets
1.168 - [MethodC.prep_input thy "met_polyeq_d2_bdvonly" [] MethodC.id_empty
1.169 + [MethodC.prep_input @{theory} "met_polyeq_d2_bdvonly" [] MethodC.id_empty
1.170 (["PolyEq", "solve_d2_polyeq_bdvonly_equation"],
1.171 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.172 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.173 @@ -1028,7 +1028,7 @@
1.174 in
1.175 Check_elementwise L_L {(v_v::real). Assumptions})"
1.176 setup \<open>KEStore_Elems.add_mets
1.177 - [MethodC.prep_input thy "met_polyeq_d2_sqonly" [] MethodC.id_empty
1.178 + [MethodC.prep_input @{theory} "met_polyeq_d2_sqonly" [] MethodC.id_empty
1.179 (["PolyEq", "solve_d2_polyeq_sqonly_equation"],
1.180 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.181 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.182 @@ -1051,7 +1051,7 @@
1.183 in
1.184 Check_elementwise L_L {(v_v::real). Assumptions})"
1.185 setup \<open>KEStore_Elems.add_mets
1.186 - [MethodC.prep_input thy "met_polyeq_d2_pq" [] MethodC.id_empty
1.187 + [MethodC.prep_input @{theory} "met_polyeq_d2_pq" [] MethodC.id_empty
1.188 (["PolyEq", "solve_d2_polyeq_pq_equation"],
1.189 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.190 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.191 @@ -1073,7 +1073,7 @@
1.192 L_L = Or_to_List e_e
1.193 in Check_elementwise L_L {(v_v::real). Assumptions})"
1.194 setup \<open>KEStore_Elems.add_mets
1.195 - [MethodC.prep_input thy "met_polyeq_d2_abc" [] MethodC.id_empty
1.196 + [MethodC.prep_input @{theory} "met_polyeq_d2_abc" [] MethodC.id_empty
1.197 (["PolyEq", "solve_d2_polyeq_abc_equation"],
1.198 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.199 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 2"]),
1.200 @@ -1100,7 +1100,7 @@
1.201 in
1.202 Check_elementwise L_L {(v_v::real). Assumptions})"
1.203 setup \<open>KEStore_Elems.add_mets
1.204 - [MethodC.prep_input thy "met_polyeq_d3" [] MethodC.id_empty
1.205 + [MethodC.prep_input @{theory} "met_polyeq_d3" [] MethodC.id_empty
1.206 (["PolyEq", "solve_d3_polyeq_equation"],
1.207 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.208 ("#Where" ,["(lhs e_e) is_poly_in v_v ", "((lhs e_e) has_degree_in v_v) = 3"]),
1.209 @@ -1130,7 +1130,7 @@
1.210 in
1.211 Or_to_List e_e)"
1.212 setup \<open>KEStore_Elems.add_mets
1.213 - [MethodC.prep_input thy "met_polyeq_complsq" [] MethodC.id_empty
1.214 + [MethodC.prep_input @{theory} "met_polyeq_complsq" [] MethodC.id_empty
1.215 (["PolyEq", "complete_square"],
1.216 [("#Given" ,["equality e_e", "solveFor v_v"]),
1.217 ("#Where" ,["matches (?a = 0) e_e", "((lhs e_e) has_degree_in v_v) = 2"]),