|
1 (* = DiffAppl.ML |
|
2 +++ outcommented tests |
|
3 *) |
|
4 |
|
5 |
|
6 theory' := overwritel (!theory', [("DiffAppl.thy",DiffAppl.thy)]); |
|
7 |
|
8 (* |
|
9 > get_pbt ["DiffAppl.thy","maximum_of","function"]; |
|
10 > get_met ("Script.thy","max_on_interval_by_calculus"); |
|
11 > !pbltypes; |
|
12 *) |
|
13 pbltypes:= overwritel (!pbltypes, |
|
14 [ |
|
15 prep_pbt DiffAppl.thy |
|
16 (["DiffAppl.thy","maximum_of","function"], |
|
17 [("#Given" ,"fixedValues fix_"), |
|
18 ("#Find" ,"maximum m_"), |
|
19 ("#Find" ,"valuesFor vs_"), |
|
20 ("#Relate","relations rs_") (*, |
|
21 ("#where" ,"foldl (op&) True (map (Not o ((op<=) #0) o Rhs) fix_)"), |
|
22 ("#with" ,"Ex_frees ((foldl (op &) True rs_) & \ |
|
23 \ (ALL m'. (subst (m_,m') (foldl (op &) True rs_) \ |
|
24 \ --> m' <= m_)))") *) |
|
25 ]), |
|
26 |
|
27 prep_pbt DiffAppl.thy |
|
28 (["DiffAppl.thy","make","function"]:pblID, |
|
29 [("#Given" ,"functionOf f_"), |
|
30 ("#Given" ,"boundVariable v_"), |
|
31 ("#Given" ,"equalities eqs_"), |
|
32 ("#Find" ,"functionTerm f_0_") |
|
33 ]), |
|
34 |
|
35 prep_pbt DiffAppl.thy |
|
36 (["DiffAppl.thy","on_interval","maximum_of","function"]:pblID, |
|
37 [("#Given" ,"functionTerm t_"), |
|
38 ("#Given" ,"boundVariable v_"), |
|
39 ("#Given" ,"interval itv_"), |
|
40 ("#Find" ,"maxArgument v_0_") |
|
41 ]), |
|
42 |
|
43 prep_pbt DiffAppl.thy |
|
44 (["DiffAppl.thy","find_values","tool"]:pblID, |
|
45 [("#Given" ,"maxArgument ma_"), |
|
46 ("#Given" ,"functionTerm f_"), |
|
47 ("#Given" ,"boundVariable v_"), |
|
48 ("#Find" ,"valuesFor vls_"), |
|
49 ("#Relate","additionalRels rs_") |
|
50 ]) |
|
51 ]); |
|
52 |
|
53 |
|
54 methods:= overwritel (!methods, |
|
55 [ |
|
56 (("DiffAppl.thy","max_by_calculus"):metID, |
|
57 {ppc = prep_met DiffAppl.thy |
|
58 [("#Given" ,"fixedValues fix_"), |
|
59 ("#Given" ,"boundVariable v_"), |
|
60 ("#Given" ,"interval itv_"), |
|
61 ("#Given" ,"errorBound err_"), |
|
62 ("#Find" ,"maximum m_"), |
|
63 ("#Find" ,"valuesFor vs_"), |
|
64 ("#Relate","relations rs_") |
|
65 ], |
|
66 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
67 scr=EmptyScr} : met), |
|
68 |
|
69 (("DiffAppl.thy","make_fun_by_new_variable"):metID, |
|
70 {ppc = prep_met DiffAppl.thy |
|
71 [("#Given" ,"functionOf f_"), |
|
72 ("#Given" ,"boundVariable v_"), |
|
73 ("#Given" ,"equalities eqs_"), |
|
74 ("#Find" ,"functionTerm f_0_") |
|
75 ], |
|
76 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
77 scr=EmptyScr} : met), |
|
78 |
|
79 (("DiffAppl.thy","make_fun_by_explicit"):metID, |
|
80 {ppc = prep_met DiffAppl.thy |
|
81 [("#Given" ,"functionOf f_"), |
|
82 ("#Given" ,"boundVariable v_"), |
|
83 ("#Given" ,"equalities eqs_"), |
|
84 ("#Find" ,"functionTerm f_0_") |
|
85 ], |
|
86 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
87 scr=EmptyScr} : met), |
|
88 |
|
89 (("DiffAppl.thy","max_on_interval_by_calculus"):metID, |
|
90 {ppc = prep_met DiffAppl.thy |
|
91 [("#Given" ,"functionTerm t_"), |
|
92 ("#Given" ,"boundVariable v_"), |
|
93 ("#Given" ,"interval itv_"), |
|
94 ("#Given" ,"errorBound err_"), |
|
95 ("#Find" ,"maxArgument v_0_") |
|
96 ], |
|
97 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
98 scr=EmptyScr} : met), |
|
99 |
|
100 (("DiffAppl.thy","find_values"):metID, |
|
101 {ppc = prep_met DiffAppl.thy |
|
102 [], |
|
103 rew_ord'="tless_true",rls'="eval_rls",asm_rls=[],asm_thm=[], |
|
104 scr=EmptyScr} : met) |
|
105 ]); |