78 }:rls); |
78 }:rls); |
79 ruleset' := overwritelthy @{theory} |
79 ruleset' := overwritelthy @{theory} |
80 (!ruleset', |
80 (!ruleset', |
81 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*) |
81 [("eval_rls",Atools_erls)(*FIXXXME:del with rls.rls'*) |
82 ]); |
82 ]); |
83 |
83 *} |
|
84 ML{* |
84 |
85 |
85 (** problem types **) |
86 (** problem types **) |
86 |
87 |
87 store_pbt |
88 store_pbt |
88 (prep_pbt thy "pbl_fun_max" [] e_pblID |
89 (prep_pbt thy "pbl_fun_max" [] e_pblID |
89 (["maximum_of","function"], |
90 (["maximum_of","function"], |
90 [("#Given" ,["fixedValues fix_"]), |
91 [("#Given" ,["fixedValues f_ix"]), |
91 ("#Find" ,["maximum m_","valuesFor vs_"]), |
92 ("#Find" ,["maximum m_m","valuesFor v_s"]), |
92 ("#Relate",["relations rs_"]) |
93 ("#Relate",["relations r_s"]) |
93 ], |
94 ], |
94 e_rls, NONE, [])); |
95 e_rls, NONE, [])); |
95 |
96 |
96 store_pbt |
97 store_pbt |
97 (prep_pbt thy "pbl_fun_make" [] e_pblID |
98 (prep_pbt thy "pbl_fun_make" [] e_pblID |
98 (["make","function"]:pblID, |
99 (["make","function"]:pblID, |
99 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
100 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
100 ("#Find" ,["functionEq f_1_"]) |
101 ("#Find" ,["functionEq f_1"]) |
101 ], |
102 ], |
102 e_rls, NONE, [])); |
103 e_rls, NONE, [])); |
103 store_pbt |
104 store_pbt |
104 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID |
105 (prep_pbt thy "pbl_fun_max_expl" [] e_pblID |
105 (["by_explicit","make","function"]:pblID, |
106 (["by_explicit","make","function"]:pblID, |
106 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
107 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
107 ("#Find" ,["functionEq f_1_"]) |
108 ("#Find" ,["functionEq f_1"]) |
108 ], |
109 ], |
109 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])); |
110 e_rls, NONE, [["DiffApp","make_fun_by_explicit"]])); |
110 store_pbt |
111 store_pbt |
111 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID |
112 (prep_pbt thy "pbl_fun_max_newvar" [] e_pblID |
112 (["by_new_variable","make","function"]:pblID, |
113 (["by_new_variable","make","function"]:pblID, |
113 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
114 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
114 (*WN.12.5.03: precond for distinction still missing*) |
115 (*WN.12.5.03: precond for distinction still missing*) |
115 ("#Find" ,["functionEq f_1_"]) |
116 ("#Find" ,["functionEq f_1"]) |
116 ], |
117 ], |
117 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])); |
118 e_rls, NONE, [["DiffApp","make_fun_by_new_variable"]])); |
118 |
119 |
119 store_pbt |
120 store_pbt |
120 (prep_pbt thy "pbl_fun_max_interv" [] e_pblID |
121 (prep_pbt thy "pbl_fun_max_interv" [] e_pblID |
121 (["on_interval","maximum_of","function"]:pblID, |
122 (["on_interval","maximum_of","function"]:pblID, |
122 [("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"]), |
123 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"]), |
123 (*WN.12.5.03: precond for distinction still missing*) |
124 (*WN.12.5.03: precond for distinction still missing*) |
124 ("#Find" ,["maxArgument v_0_"]) |
125 ("#Find" ,["maxArgument v_0"]) |
125 ], |
126 ], |
126 e_rls, NONE, [])); |
127 e_rls, NONE, [])); |
127 |
128 |
128 store_pbt |
129 store_pbt |
129 (prep_pbt thy "pbl_tool" [] e_pblID |
130 (prep_pbt thy "pbl_tool" [] e_pblID |
132 e_rls, NONE, [])); |
133 e_rls, NONE, [])); |
133 |
134 |
134 store_pbt |
135 store_pbt |
135 (prep_pbt thy "pbl_tool_findvals" [] e_pblID |
136 (prep_pbt thy "pbl_tool_findvals" [] e_pblID |
136 (["find_values","tool"]:pblID, |
137 (["find_values","tool"]:pblID, |
137 [("#Given" ,["maxArgument ma_","functionEq f_f","boundVariable v_v"]), |
138 [("#Given" ,["maxArgument m_ax","functionEq f_f","boundVariable v_v"]), |
138 ("#Find" ,["valuesFor vls_"]), |
139 ("#Find" ,["valuesFor v_ls"]), |
139 ("#Relate",["additionalRels rs_"]) |
140 ("#Relate",["additionalRels r_s"]) |
140 ], |
141 ], |
141 e_rls, NONE, [])); |
142 e_rls, NONE, [])); |
142 |
143 |
|
144 *} |
|
145 ML{* |
143 |
146 |
144 (** methods, scripts not yet implemented **) |
147 (** methods, scripts not yet implemented **) |
145 |
148 |
146 store_met |
149 store_met |
147 (prep_met thy "met_diffapp" [] e_metID |
150 (prep_met thy "met_diffapp" [] e_metID |
148 (["DiffApp"], |
151 (["DiffApp"], |
149 [], |
152 [], |
150 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
153 {rew_ord'="tless_true",rls'=Atools_erls,calc = [], srls = e_rls, prls=e_rls, |
151 crls = Atools_erls, nrls=norm_Rational |
154 crls = Atools_erls, nrls=norm_Rational |
152 (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); |
155 (*, asm_rls=[],asm_thm=[]*)}, "empty_script")); |
|
156 *} |
|
157 ML{* |
153 store_met |
158 store_met |
154 (prep_met thy "met_diffapp_max" [] e_metID |
159 (prep_met thy "met_diffapp_max" [] e_metID |
155 (["DiffApp","max_by_calculus"]:metID, |
160 (["DiffApp","max_by_calculus"]:metID, |
156 [("#Given" ,["fixedValues fix_","maximum m_","relations rs_", |
161 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", |
157 "boundVariable v_v","interval itv_","errorBound err_"]), |
162 "boundVariable v_v","interval i_tv","errorBound e_rr"]), |
158 ("#Find" ,["valuesFor vs_"]), |
163 ("#Find" ,["valuesFor v_s"]), |
159 ("#Relate",[]) |
164 ("#Relate",[]) |
160 ], |
165 ], |
161 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, |
166 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, |
162 crls = eval_rls, nrls=norm_Rational |
167 crls = eval_rls, nrls=norm_Rational |
163 (*, asm_rls=[],asm_thm=[]*)}, |
168 (*, asm_rls=[],asm_thm=[]*)}, |
164 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list) " ^ |
169 "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^ |
165 " (v_v::real) (itv_v::real set) (err_::bool) = " ^ |
170 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^ |
166 " (let e_e = (hd o (filterVar m_)) rs_; " ^ |
171 " (let e_e = (hd o (filterVar m_m)) r_s; " ^ |
167 " t_ = (if 1 < length_ rs_ " ^ |
172 " t_t = (if 1 < LENGTH r_s " ^ |
168 " then (SubProblem (DiffApp_,[make,function],[no_met]) " ^ |
173 " then (SubProblem (DiffApp',[make,function],[no_met]) " ^ |
169 " [REAL m_, REAL v_v, BOOL_LIST rs_]) " ^ |
174 " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^ |
170 " else (hd rs_)); " ^ |
175 " else (hd r_s)); " ^ |
171 " (mx_::real) = " ^ |
176 " (m_x::real) = " ^ |
172 "SubProblem(DiffApp_,[on_interval,maximum_of,function], " ^ |
177 "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^ |
173 " [DiffApp,max_on_interval_by_calculus]) " ^ |
178 " [DiffApp,max_on_interval_by_calculus]) " ^ |
174 " [BOOL t_, REAL v_v, REAL_SET itv_] " ^ |
179 " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^ |
175 " in ((SubProblem (DiffApp_,[find_values,tool],[Isac,find_values]) " ^ |
180 " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^ |
176 " [REAL mx_, REAL (Rhs t_), REAL v_v, REAL m_, " ^ |
181 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^ |
177 " BOOL_LIST (dropWhile (ident e_e) rs_)])::bool list)) " |
182 " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) " |
178 )); |
183 )); |
|
184 *} |
|
185 ML{* |
179 store_met |
186 store_met |
180 (prep_met thy "met_diffapp_funnew" [] e_metID |
187 (prep_met thy "met_diffapp_funnew" [] e_metID |
181 (["DiffApp","make_fun_by_new_variable"]:metID, |
188 (["DiffApp","make_fun_by_new_variable"]:metID, |
182 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
189 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
183 ("#Find" ,["functionEq f_1_"]) |
190 ("#Find" ,["functionEq f_1"]) |
184 ], |
191 ], |
185 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, |
192 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, |
186 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
193 calc=[], crls = eval_rls, nrls=norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
187 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^ |
194 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^ |
188 " (eqs::bool list) = " ^ |
195 " (eqs::bool list) = " ^ |
189 "(let h_ = (hd o (filterVar f_)) eqs; " ^ |
196 "(let h_h = (hd o (filterVar f_f)) eqs; " ^ |
190 " es_ = dropWhile (ident h_) eqs; " ^ |
197 " e_s = dropWhile (ident h_h) eqs; " ^ |
191 " vs_ = dropWhile (ident f_) (Vars h_); " ^ |
198 " v_s = dropWhile (ident f_f) (Vars h_h); " ^ |
192 " v_1 = nth_ 1 vs_; " ^ |
199 " v_1 = NTH 1 v_s; " ^ |
193 " v_2 = nth_ 2 vs_; " ^ |
200 " v_2 = NTH 2 v_s; " ^ |
194 " e_1 = (hd o (filterVar v_1)) es_; " ^ |
201 " e_1 = (hd o (filterVar v_1)) e_s; " ^ |
195 " e_2 = (hd o (filterVar v_2)) es_; " ^ |
202 " e_2 = (hd o (filterVar v_2)) e_s; " ^ |
196 " (s_1::bool list) = " ^ |
203 " (s_1::bool list) = " ^ |
197 " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^ |
204 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^ |
198 " [BOOL e_1, REAL v_1]); " ^ |
205 " [BOOL e_1, REAL v_1]); " ^ |
199 " (s_2::bool list) = " ^ |
206 " (s_2::bool list) = " ^ |
200 " (SubProblem (DiffApp_,[univariate,equation],[no_met])" ^ |
207 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^ |
201 " [BOOL e_2, REAL v_2])" ^ |
208 " [BOOL e_2, REAL v_2])" ^ |
202 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_)" |
209 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)" |
203 )); |
210 )); |
|
211 *} |
|
212 ML{* |
204 store_met |
213 store_met |
205 (prep_met thy "met_diffapp_funexp" [] e_metID |
214 (prep_met thy "met_diffapp_funexp" [] e_metID |
206 (["DiffApp","make_fun_by_explicit"]:metID, |
215 (["DiffApp","make_fun_by_explicit"]:metID, |
207 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
216 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
208 ("#Find" ,["functionEq f_1_"]) |
217 ("#Find" ,["functionEq f_1"]) |
209 ], |
218 ], |
210 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, |
219 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, |
211 crls = eval_rls, nrls=norm_Rational |
220 crls = eval_rls, nrls=norm_Rational |
212 (*, asm_rls=[],asm_thm=[]*)}, |
221 (*, asm_rls=[],asm_thm=[]*)}, |
213 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^ |
222 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^ |
214 " (eqs::bool list) = " ^ |
223 " (eqs::bool list) = " ^ |
215 " (let h_ = (hd o (filterVar f_)) eqs; " ^ |
224 " (let h_h = (hd o (filterVar f_f)) eqs; " ^ |
216 " e_1 = hd (dropWhile (ident h_) eqs); " ^ |
225 " e_1 = hd (dropWhile (ident h_h) eqs); " ^ |
217 " vs_ = dropWhile (ident f_) (Vars h_); " ^ |
226 " v_s = dropWhile (ident f_f) (Vars h_h); " ^ |
218 " v_1 = hd (dropWhile (ident v_v) vs_); " ^ |
227 " v_1 = hd (dropWhile (ident v_v) v_s); " ^ |
219 " (s_1::bool list)= " ^ |
228 " (s_1::bool list)= " ^ |
220 " (SubProblem(DiffApp_,[univariate,equation],[no_met])" ^ |
229 " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^ |
221 " [BOOL e_1, REAL v_1]) " ^ |
230 " [BOOL e_1, REAL v_1]) " ^ |
222 " in Substitute [(v_1 = (rhs o hd) s_1)] h_) " |
231 " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) " |
223 )); |
232 )); |
|
233 *} |
|
234 ML{* |
224 store_met |
235 store_met |
225 (prep_met thy "met_diffapp_max_oninterval" [] e_metID |
236 (prep_met thy "met_diffapp_max_oninterval" [] e_metID |
226 (["DiffApp","max_on_interval_by_calculus"]:metID, |
237 (["DiffApp","max_on_interval_by_calculus"]:metID, |
227 [("#Given" ,["functionEq t_","boundVariable v_v","interval itv_"(*, |
238 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, |
228 "errorBound err_"*)]), |
239 "errorBound e_rr"*)]), |
229 ("#Find" ,["maxArgument v_0_"]) |
240 ("#Find" ,["maxArgument v_0"]) |
230 ], |
241 ], |
231 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, |
242 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, |
232 crls = eval_rls, nrls=norm_Rational |
243 crls = eval_rls, nrls=norm_Rational |
233 (*, asm_rls=[],asm_thm=[]*)}, |
244 (*, asm_rls=[],asm_thm=[]*)}, |
234 "empty_script" |
245 "empty_script" |
235 )); |
246 )); |
|
247 *} |
|
248 ML{* |
236 store_met |
249 store_met |
237 (prep_met thy "met_diffapp_findvals" [] e_metID |
250 (prep_met thy "met_diffapp_findvals" [] e_metID |
238 (["DiffApp","find_values"]:metID, |
251 (["DiffApp","find_values"]:metID, |
239 [], |
252 [], |
240 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, |
253 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, |