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