12 *) |
12 *) |
13 pbltypes:= overwritel (!pbltypes, |
13 pbltypes:= overwritel (!pbltypes, |
14 [ |
14 [ |
15 prep_pbt DiffAppl.thy |
15 prep_pbt DiffAppl.thy |
16 (["DiffAppl","maximum_of","function"], |
16 (["DiffAppl","maximum_of","function"], |
17 [("#Given" ,"fixedValues fix_"), |
17 [("#Given" ,"fixedValues f_ix"), |
18 ("#Find" ,"maximum m_"), |
18 ("#Find" ,"maximum m_"), |
19 ("#Find" ,"valuesFor vs_"), |
19 ("#Find" ,"valuesFor v_s"), |
20 ("#Relate","relations rs_") (*, |
20 ("#Relate","relations r_s") (*, |
21 ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"), |
21 ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) f_ix)"), |
22 ("#with" ,"Ex_frees ((foldl (op &) True rs_) & \ |
22 ("#with" ,"Ex_frees ((foldl (op &) True r_s) & \ |
23 \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \ |
23 \ (ALL m'. (subst (m_,m') (foldl (op &) True r_s) \ |
24 \ --> m' <= m_)))") *) |
24 \ --> m' <= m_)))") *) |
25 ]), |
25 ]), |
26 |
26 |
27 prep_pbt DiffAppl.thy |
27 prep_pbt DiffAppl.thy |
28 (["DiffAppl","make","function"]:pblID, |
28 (["DiffAppl","make","function"]:pblID, |
35 prep_pbt DiffAppl.thy |
35 prep_pbt DiffAppl.thy |
36 (["DiffAppl","on_interval","maximum_of","function"]:pblID, |
36 (["DiffAppl","on_interval","maximum_of","function"]:pblID, |
37 [("#Given" ,"functionTerm t_"), |
37 [("#Given" ,"functionTerm t_"), |
38 ("#Given" ,"boundVariable v_v"), |
38 ("#Given" ,"boundVariable v_v"), |
39 ("#Given" ,"interval itv_"), |
39 ("#Given" ,"interval itv_"), |
40 ("#Find" ,"maxArgument v_0_") |
40 ("#Find" ,"maxArgument v_0") |
41 ]), |
41 ]), |
42 |
42 |
43 prep_pbt DiffAppl.thy |
43 prep_pbt DiffAppl.thy |
44 (["DiffAppl","find_values","tool"]:pblID, |
44 (["DiffAppl","find_values","tool"]:pblID, |
45 [("#Given" ,"maxArgument ma_"), |
45 [("#Given" ,"maxArgument ma_"), |
46 ("#Given" ,"functionTerm f_f"), |
46 ("#Given" ,"functionTerm f_f"), |
47 ("#Given" ,"boundVariable v_v"), |
47 ("#Given" ,"boundVariable v_v"), |
48 ("#Find" ,"valuesFor vls_"), |
48 ("#Find" ,"valuesFor vls_"), |
49 ("#Relate","additionalRels rs_") |
49 ("#Relate","additionalRels r_s") |
50 ]) |
50 ]) |
51 ]); |
51 ]); |
52 |
52 |
53 |
53 |
54 methods:= overwritel (!methods, |
54 methods:= overwritel (!methods, |
55 [ |
55 [ |
56 (("DiffAppl","max_by_calculus"):metID, |
56 (("DiffAppl","max_by_calculus"):metID, |
57 {ppc = prep_met DiffAppl.thy |
57 {ppc = prep_met DiffAppl.thy |
58 [("#Given" ,"fixedValues fix_"), |
58 [("#Given" ,"fixedValues f_ix"), |
59 ("#Given" ,"boundVariable v_v"), |
59 ("#Given" ,"boundVariable v_v"), |
60 ("#Given" ,"interval itv_"), |
60 ("#Given" ,"interval itv_"), |
61 ("#Given" ,"errorBound err_"), |
61 ("#Given" ,"errorBound err_"), |
62 ("#Find" ,"maximum m_"), |
62 ("#Find" ,"maximum m_"), |
63 ("#Find" ,"valuesFor vs_"), |
63 ("#Find" ,"valuesFor v_s"), |
64 ("#Relate","relations rs_") |
64 ("#Relate","relations r_s") |
65 ], |
65 ], |
66 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
66 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
67 scr=EmptyScr} : met), |
67 scr=EmptyScr} : met), |
68 |
68 |
69 (("DiffAppl","make_fun_by_new_variable"):metID, |
69 (("DiffAppl","make_fun_by_new_variable"):metID, |
90 {ppc = prep_met DiffAppl.thy |
90 {ppc = prep_met DiffAppl.thy |
91 [("#Given" ,"functionTerm t_"), |
91 [("#Given" ,"functionTerm t_"), |
92 ("#Given" ,"boundVariable v_v"), |
92 ("#Given" ,"boundVariable v_v"), |
93 ("#Given" ,"interval itv_"), |
93 ("#Given" ,"interval itv_"), |
94 ("#Given" ,"errorBound err_"), |
94 ("#Given" ,"errorBound err_"), |
95 ("#Find" ,"maxArgument v_0_") |
95 ("#Find" ,"maxArgument v_0") |
96 ], |
96 ], |
97 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
97 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
98 scr=EmptyScr} : met), |
98 scr=EmptyScr} : met), |
99 |
99 |
100 (("DiffAppl","find_values"):metID, |
100 (("DiffAppl","find_values"):metID, |