22 \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \ |
22 \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \ |
23 \ --> m' <= m_)))") *) |
23 \ --> m' <= m_)))") *) |
24 ]), |
24 ]), |
25 |
25 |
26 prep_pbt DiffAppl.thy |
26 prep_pbt DiffAppl.thy |
27 (["DiffAppl","make","function"]:pblID, |
27 (["DiffAppl","make","function"], |
28 [("#Given" ,"functionOf f_f"), |
28 [("#Given" ,"functionOf f_f"), |
29 ("#Given" ,"boundVariable v_v"), |
29 ("#Given" ,"boundVariable v_v"), |
30 ("#Given" ,"equalities eqs"), |
30 ("#Given" ,"equalities eqs"), |
31 ("#Find" ,"functionTerm f_0_") |
31 ("#Find" ,"functionTerm f_0_") |
32 ]), |
32 ]), |
33 |
33 |
34 prep_pbt DiffAppl.thy |
34 prep_pbt DiffAppl.thy |
35 (["DiffAppl","on_interval","maximum_of","function"]:pblID, |
35 (["DiffAppl","on_interval","maximum_of","function"], |
36 [("#Given" ,"functionTerm t_"), |
36 [("#Given" ,"functionTerm t_"), |
37 ("#Given" ,"boundVariable v_v"), |
37 ("#Given" ,"boundVariable v_v"), |
38 ("#Given" ,"interval itv_"), |
38 ("#Given" ,"interval itv_"), |
39 ("#Find" ,"maxArgument v_0") |
39 ("#Find" ,"maxArgument v_0") |
40 ]), |
40 ]), |
41 |
41 |
42 prep_pbt DiffAppl.thy |
42 prep_pbt DiffAppl.thy |
43 (["DiffAppl","find_values","tool"]:pblID, |
43 (["DiffAppl","find_values","tool"], |
44 [("#Given" ,"maxArgument ma_"), |
44 [("#Given" ,"maxArgument ma_"), |
45 ("#Given" ,"functionTerm f_f"), |
45 ("#Given" ,"functionTerm f_f"), |
46 ("#Given" ,"boundVariable v_v"), |
46 ("#Given" ,"boundVariable v_v"), |
47 ("#Find" ,"valuesFor vls_"), |
47 ("#Find" ,"valuesFor vls_"), |
48 ("#Relate","additionalRels r_s") |
48 ("#Relate","additionalRels r_s") |
50 ]); |
50 ]); |
51 |
51 |
52 |
52 |
53 methods:= overwritel (!methods, |
53 methods:= overwritel (!methods, |
54 [ |
54 [ |
55 (("DiffAppl","max_by_calculus"):metID, |
55 (("DiffAppl","max_by_calculus"), |
56 {ppc = prep_met DiffAppl.thy |
56 {ppc = prep_met DiffAppl.thy |
57 [("#Given" ,"fixedValues f_ix"), |
57 [("#Given" ,"fixedValues f_ix"), |
58 ("#Given" ,"boundVariable v_v"), |
58 ("#Given" ,"boundVariable v_v"), |
59 ("#Given" ,"interval itv_"), |
59 ("#Given" ,"interval itv_"), |
60 ("#Given" ,"errorBound err_"), |
60 ("#Given" ,"errorBound err_"), |
61 ("#Find" ,"maximum m_"), |
61 ("#Find" ,"maximum m_"), |
62 ("#Find" ,"valuesFor v_s"), |
62 ("#Find" ,"valuesFor v_s"), |
63 ("#Relate","relations r_s") |
63 ("#Relate","relations r_s") |
64 ], |
64 ], |
65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
65 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
66 scr=EmptyScr} : met), |
66 scr=Celem.EmptyScr} : met), |
67 |
67 |
68 (("DiffAppl","make_fun_by_new_variable"):metID, |
68 (("DiffAppl","make_fun_by_new_variable"), |
69 {ppc = prep_met DiffAppl.thy |
69 {ppc = prep_met DiffAppl.thy |
70 [("#Given" ,"functionOf f_f"), |
70 [("#Given" ,"functionOf f_f"), |
71 ("#Given" ,"boundVariable v_v"), |
71 ("#Given" ,"boundVariable v_v"), |
72 ("#Given" ,"equalities eqs"), |
72 ("#Given" ,"equalities eqs"), |
73 ("#Find" ,"functionTerm f_0_") |
73 ("#Find" ,"functionTerm f_0_") |
74 ], |
74 ], |
75 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
75 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
76 scr=EmptyScr} : met), |
76 scr=Celem.EmptyScr} : met), |
77 |
77 |
78 (("DiffAppl","make_fun_by_explicit"):metID, |
78 (("DiffAppl","make_fun_by_explicit"), |
79 {ppc = prep_met DiffAppl.thy |
79 {ppc = prep_met DiffAppl.thy |
80 [("#Given" ,"functionOf f_f"), |
80 [("#Given" ,"functionOf f_f"), |
81 ("#Given" ,"boundVariable v_v"), |
81 ("#Given" ,"boundVariable v_v"), |
82 ("#Given" ,"equalities eqs"), |
82 ("#Given" ,"equalities eqs"), |
83 ("#Find" ,"functionTerm f_0_") |
83 ("#Find" ,"functionTerm f_0_") |
84 ], |
84 ], |
85 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
85 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
86 scr=EmptyScr} : met), |
86 scr=Celem.EmptyScr} : met), |
87 |
87 |
88 (("DiffAppl","max_on_interval_by_calculus"):metID, |
88 (("DiffAppl","max_on_interval_by_calculus"), |
89 {ppc = prep_met DiffAppl.thy |
89 {ppc = prep_met DiffAppl.thy |
90 [("#Given" ,"functionTerm t_"), |
90 [("#Given" ,"functionTerm t_"), |
91 ("#Given" ,"boundVariable v_v"), |
91 ("#Given" ,"boundVariable v_v"), |
92 ("#Given" ,"interval itv_"), |
92 ("#Given" ,"interval itv_"), |
93 ("#Given" ,"errorBound err_"), |
93 ("#Given" ,"errorBound err_"), |
94 ("#Find" ,"maxArgument v_0") |
94 ("#Find" ,"maxArgument v_0") |
95 ], |
95 ], |
96 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
96 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
97 scr=EmptyScr} : met), |
97 scr=Celem.EmptyScr} : met), |
98 |
98 |
99 (("DiffAppl","find_values"):metID, |
99 (("DiffAppl","find_values"), |
100 {ppc = prep_met DiffAppl.thy |
100 {ppc = prep_met DiffAppl.thy |
101 [], |
101 [], |
102 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
102 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
103 scr=EmptyScr} : met) |
103 scr=Celem.EmptyScr} : met) |
104 ]); |
104 ]); |