8 > get_pbt ["DiffAppl","maximum_of","function"];
9 > get_met ("Program","max_on_interval_by_calculus");
12 pbltypes:= overwritel (!pbltypes,
15 (["DiffAppl","maximum_of","function"],
16 [("#Given" ,"fixedValues f_ix"),
17 ("#Find" ,"maximum m_"),
18 ("#Find" ,"valuesFor v_s"),
19 ("#Relate","relations r_s") (*,
20 ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) f_ix)"),
21 ("#with" ,"Ex_frees ((foldl (op &) True r_s) & \
22 \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \
23 \ --> m' <= m_)))") *)
27 (["DiffAppl","make","function"],
28 [("#Given" ,"functionOf f_f"),
29 ("#Given" ,"boundVariable v_v"),
30 ("#Given" ,"equalities eqs"),
31 ("#Find" ,"functionTerm f_0_")
35 (["DiffAppl","on_interval","maximum_of","function"],
36 [("#Given" ,"functionTerm t_"),
37 ("#Given" ,"boundVariable v_v"),
38 ("#Given" ,"interval itv_"),
39 ("#Find" ,"maxArgument v_0")
43 (["DiffAppl","find_values","tool"],
44 [("#Given" ,"maxArgument ma_"),
45 ("#Given" ,"functionTerm f_f"),
46 ("#Given" ,"boundVariable v_v"),
47 ("#Find" ,"valuesFor vls_"),
48 ("#Relate","additionalRels r_s")
53 methods:= overwritel (!methods,
55 (("DiffAppl","max_by_calculus"),
56 {ppc = prep_met DiffAppl.thy
57 [("#Given" ,"fixedValues f_ix"),
58 ("#Given" ,"boundVariable v_v"),
59 ("#Given" ,"interval itv_"),
60 ("#Given" ,"errorBound err_"),
61 ("#Find" ,"maximum m_"),
62 ("#Find" ,"valuesFor v_s"),
63 ("#Relate","relations r_s")
65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
66 scr =Rule.Empty_Prog} : met),
68 (("DiffAppl","make_fun_by_new_variable"),
69 {ppc = prep_met DiffAppl.thy
70 [("#Given" ,"functionOf f_f"),
71 ("#Given" ,"boundVariable v_v"),
72 ("#Given" ,"equalities eqs"),
73 ("#Find" ,"functionTerm f_0_")
75 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
76 scr =Rule.Empty_Prog} : met),
78 (("DiffAppl","make_fun_by_explicit"),
79 {ppc = prep_met DiffAppl.thy
80 [("#Given" ,"functionOf f_f"),
81 ("#Given" ,"boundVariable v_v"),
82 ("#Given" ,"equalities eqs"),
83 ("#Find" ,"functionTerm f_0_")
85 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
86 scr =Rule.Empty_Prog} : met),
88 (("DiffAppl","max_on_interval_by_calculus"),
89 {ppc = prep_met DiffAppl.thy
90 [("#Given" ,"functionTerm t_"),
91 ("#Given" ,"boundVariable v_v"),
92 ("#Given" ,"interval itv_"),
93 ("#Given" ,"errorBound err_"),
94 ("#Find" ,"maxArgument v_0")
96 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
97 scr =Rule.Empty_Prog} : met),
99 (("DiffAppl","find_values"),
100 {ppc = prep_met DiffAppl.thy
102 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[],
103 scr =Rule.Empty_Prog} : met)