225 [], |
225 [], |
226 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, |
226 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, |
227 crls = eval_rls, errpats = [], nrls = norm_Rational(*, |
227 crls = eval_rls, errpats = [], nrls = norm_Rational(*, |
228 asm_rls=[],asm_thm=[]*)}, |
228 asm_rls=[],asm_thm=[]*)}, |
229 "empty_script")); |
229 "empty_script")); |
230 |
230 *} |
|
231 setup {* KEStore_Elems.add_mets |
|
232 [prep_met thy "met_diffapp" [] e_metID |
|
233 (["DiffApp"], [], |
|
234 {rew_ord'="tless_true", rls'=Atools_erls,calc = [], srls = e_rls, prls = e_rls, |
|
235 crls = Atools_erls, errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
|
236 "empty_script"), |
|
237 prep_met thy "met_diffapp_max" [] e_metID |
|
238 (["DiffApp","max_by_calculus"]:metID, |
|
239 [("#Given" ,["fixedValues f_ix","maximum m_m","relations r_s", "boundVariable v_v", |
|
240 "interval i_tv","errorBound e_rr"]), |
|
241 ("#Find" ,["valuesFor v_s"]), |
|
242 ("#Relate",[])], |
|
243 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, crls = eval_rls, |
|
244 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
|
245 "Script Maximum_value(f_ix::bool list)(m_m::real) (r_s::bool list) " ^ |
|
246 " (v_v::real) (itv_v::real set) (e_rr::bool) = " ^ |
|
247 " (let e_e = (hd o (filterVar m_m)) r_s; " ^ |
|
248 " t_t = (if 1 < LENGTH r_s " ^ |
|
249 " then (SubProblem (DiffApp',[make,function],[no_met]) " ^ |
|
250 " [REAL m_m, REAL v_v, BOOL_LIST r_s]) " ^ |
|
251 " else (hd r_s)); " ^ |
|
252 " (m_x::real) = " ^ |
|
253 "SubProblem(DiffApp',[on_interval,maximum_of,function], " ^ |
|
254 " [DiffApp,max_on_interval_by_calculus]) " ^ |
|
255 " [BOOL t_t, REAL v_v, REAL_SET i_tv] " ^ |
|
256 " in ((SubProblem (DiffApp',[find_values,tool],[Isac,find_values]) " ^ |
|
257 " [REAL m_x, REAL (Rhs t_t), REAL v_v, REAL m_m, " ^ |
|
258 " BOOL_LIST (dropWhile (ident e_e) r_s)])::bool list)) "), |
|
259 prep_met thy "met_diffapp_funnew" [] e_metID |
|
260 (["DiffApp","make_fun_by_new_variable"]:metID, |
|
261 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
|
262 ("#Find" ,["functionEq f_1"])], |
|
263 {rew_ord'="tless_true",rls'=eval_rls,srls=list_rls,prls=e_rls, calc=[], crls = eval_rls, |
|
264 errpats = [], nrls = norm_Rational(*,asm_rls=[],asm_thm=[]*)}, |
|
265 "Script Make_fun_by_new_variable (f_f::real) (v_v::real) " ^ |
|
266 " (eqs::bool list) = " ^ |
|
267 "(let h_h = (hd o (filterVar f_f)) eqs; " ^ |
|
268 " e_s = dropWhile (ident h_h) eqs; " ^ |
|
269 " v_s = dropWhile (ident f_f) (Vars h_h); " ^ |
|
270 " v_1 = NTH 1 v_s; " ^ |
|
271 " v_2 = NTH 2 v_s; " ^ |
|
272 " e_1 = (hd o (filterVar v_1)) e_s; " ^ |
|
273 " e_2 = (hd o (filterVar v_2)) e_s; " ^ |
|
274 " (s_1::bool list) = " ^ |
|
275 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^ |
|
276 " [BOOL e_1, REAL v_1]); " ^ |
|
277 " (s_2::bool list) = " ^ |
|
278 " (SubProblem (DiffApp',[univariate,equation],[no_met])" ^ |
|
279 " [BOOL e_2, REAL v_2])" ^ |
|
280 "in Substitute [(v_1 = (rhs o hd) s_1),(v_2 = (rhs o hd) s_2)] h_h)"), |
|
281 prep_met thy "met_diffapp_funexp" [] e_metID |
|
282 (["DiffApp","make_fun_by_explicit"]:metID, |
|
283 [("#Given" ,["functionOf f_f","boundVariable v_v","equalities eqs"]), |
|
284 ("#Find" ,["functionEq f_1"])], |
|
285 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls=list_rls,prls=e_rls, crls = eval_rls, |
|
286 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
|
287 "Script Make_fun_by_explicit (f_f::real) (v_v::real) " ^ |
|
288 " (eqs::bool list) = " ^ |
|
289 " (let h_h = (hd o (filterVar f_f)) eqs; " ^ |
|
290 " e_1 = hd (dropWhile (ident h_h) eqs); " ^ |
|
291 " v_s = dropWhile (ident f_f) (Vars h_h); " ^ |
|
292 " v_1 = hd (dropWhile (ident v_v) v_s); " ^ |
|
293 " (s_1::bool list)= " ^ |
|
294 " (SubProblem(DiffApp',[univariate,equation],[no_met])" ^ |
|
295 " [BOOL e_1, REAL v_1]) " ^ |
|
296 " in Substitute [(v_1 = (rhs o hd) s_1)] h_h) "), |
|
297 prep_met thy "met_diffapp_max_oninterval" [] e_metID |
|
298 (["DiffApp","max_on_interval_by_calculus"]:metID, |
|
299 [("#Given" ,["functionEq t_t","boundVariable v_v","interval i_tv"(*, "errorBound e_rr"*)]), |
|
300 ("#Find" ,["maxArgument v_0"])], |
|
301 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, crls = eval_rls, |
|
302 errpats = [], nrls = norm_Rational (*, asm_rls=[],asm_thm=[]*)}, |
|
303 "empty_script"), |
|
304 prep_met thy "met_diffapp_findvals" [] e_metID |
|
305 (["DiffApp","find_values"]:metID, [], |
|
306 {rew_ord'="tless_true",rls'=eval_rls,calc=[],srls = e_rls,prls=e_rls, crls = eval_rls, |
|
307 errpats = [], nrls = norm_Rational(*, asm_rls = [], asm_thm = []*)}, |
|
308 "empty_script")] |
|
309 *} |
|
310 ML {* |
231 val list_rls = append_rls "list_rls" list_rls |
311 val list_rls = append_rls "list_rls" list_rls |
232 [Thm ("filterVar_Const", num_str @{thm filterVar_Const}), |
312 [Thm ("filterVar_Const", num_str @{thm filterVar_Const}), |
233 Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})]; |
313 Thm ("filterVar_Nil", num_str @{thm filterVar_Nil})]; |
234 *} |
314 *} |
235 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
315 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |