neuper@37906
|
1 |
(*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
|
neuper@37906
|
2 |
|
neuper@37906
|
3 |
(* Das erste Script aus dem Maximum-Beispiel.
|
neuper@37906
|
4 |
parse erzeugt aus dem string 's' den
|
neuper@37906
|
5 |
'cterm 's' im Isabelle-Format (pretty-printing !)*)
|
neuper@37906
|
6 |
|
neuper@37906
|
7 |
ML> ...
|
neuper@37906
|
8 |
ML> val c = (the o (parse thy)) s;
|
neuper@37906
|
9 |
val c =
|
neuper@37981
|
10 |
"Script1 Maximum_value fix_ m_ rs_ v_v itv_ err_ =
|
neuper@37981
|
11 |
let e_e = (hd o filter (Testvar m_)) rs_;
|
neuper@37906
|
12 |
t_ =
|
neuper@37906
|
13 |
if #1 < Length rs_
|
neuper@37981
|
14 |
then make_fun (R, [make, function], no_met) m_ v_v rs_
|
neuper@37906
|
15 |
else (Lhs o hd) rs_;
|
neuper@37906
|
16 |
mx_ =
|
neuper@37906
|
17 |
max_on_interval (R, [on_interval, max_of, function],
|
neuper@37981
|
18 |
maximum_on_interval) t_ v_v itv_
|
neuper@37906
|
19 |
in find_vals (R, [find_values, tool], find_values)
|
neuper@37981
|
20 |
mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
ML> set show_types;
|
neuper@37906
|
23 |
ML> c;
|
neuper@37906
|
24 |
val c =
|
neuper@37991
|
25 |
"Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool =
|
neuper@37981
|
26 |
let e_e::bool = (hd o filter (Testvar m_)) rs_;
|
neuper@37906
|
27 |
t_::real =
|
neuper@37906
|
28 |
if (#1::real) < Length rs_
|
neuper@37981
|
29 |
then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v rs_
|
neuper@37906
|
30 |
else (Lhs o hd) rs_;
|
neuper@37906
|
31 |
mx_::real =
|
neuper@37906
|
32 |
max_on_interval (R, [on_interval::ID, max_of::ID, function],
|
neuper@37981
|
33 |
maximum_on_interval::ID) t_ v_v itv_
|
neuper@37906
|
34 |
in find_vals (R, [find_values::ID, tool::ID], find_values)
|
neuper@37981
|
35 |
mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
|
neuper@37906
|
36 |
|
neuper@37906
|
37 |
|
neuper@37906
|
38 |
|
neuper@37906
|
39 |
(* Die ersten 3 Scripts aus dem Maximum-Beispiel.
|
neuper@37906
|
40 |
parse erzeugt aus dem string 's' den
|
neuper@37906
|
41 |
'cterm 's' im Isabelle-Format (pretty-printing !)*)
|
neuper@37906
|
42 |
|
neuper@37906
|
43 |
ML> ...
|
neuper@37906
|
44 |
ML> val c = (the o (parse thy)) s;
|
neuper@37906
|
45 |
val c =
|
neuper@37906
|
46 |
"Script maximum =
|
neuper@37981
|
47 |
Input [Bool fix_, Real m_, BoolList rs_, Real v_v, RealSet itv_, Bool err_]
|
neuper@37981
|
48 |
Local [Bool e_e, Real t_, Real mx_, RealList vs_]
|
neuper@37906
|
49 |
Tacs [SEQU
|
neuper@37981
|
50 |
[let e_e = (hd o filter (Testvar m_)) rs_
|
neuper@37906
|
51 |
in if #1 < Length rs_
|
neuper@37906
|
52 |
then Subproblem Spec (R, [make, function], no_met)
|
neuper@37981
|
53 |
InOut [In m_, In v_v, In rs_, Out t_]
|
neuper@37906
|
54 |
else t_ := (Lhs o hd) rs_ ;
|
neuper@37906
|
55 |
Subproblem Spec (R, [on_interval, max_of, function],
|
neuper@37906
|
56 |
maximum_on_interval)
|
neuper@37981
|
57 |
InOut [In t_, In v_v, In itv_, In err_, Out mx_] ;
|
neuper@37906
|
58 |
Subproblem Spec (R, [find_values, tool], find_values)
|
neuper@37981
|
59 |
InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) rs_),
|
neuper@37906
|
60 |
Out vs_]]]
|
neuper@37906
|
61 |
Return []" : cterm
|
neuper@37906
|
62 |
|
neuper@37906
|
63 |
ML> ...
|
neuper@37906
|
64 |
ML> val c = (the o (parse thy)) s;
|
neuper@37906
|
65 |
val c =
|
neuper@37906
|
66 |
"Script make_fun_by_new_variable =
|
neuper@37981
|
67 |
Input [Real f_, Real v_v, BoolList eqs_]
|
neuper@37906
|
68 |
Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
|
neuper@37906
|
69 |
Bool e2_, BoolList s_1, BoolList s_2]
|
neuper@37906
|
70 |
Tacs [SEQU
|
neuper@37906
|
71 |
[let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];
|
neuper@37906
|
72 |
vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
|
neuper@37906
|
73 |
e1_ = (hd o filter (Testvar v1_)) es_;
|
neuper@37906
|
74 |
e2_ = (hd o filter (Testvar v2_)) es_
|
neuper@37906
|
75 |
in Subproblem Spec (R, [univar, equation], no_met)
|
neuper@37906
|
76 |
InOut [In e1_, In v1_, Out s_1] ;
|
neuper@37906
|
77 |
Subproblem Spec (R, [univar, equation], no_met)
|
neuper@37906
|
78 |
InOut [In e2_, In v2_, Out s_2]],
|
neuper@37906
|
79 |
Take (Bool h_) ;
|
neuper@37906
|
80 |
Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
|
neuper@37906
|
81 |
Return [Currform]" : cterm
|
neuper@37906
|
82 |
|
neuper@37906
|
83 |
ML> ...
|
neuper@37906
|
84 |
ML> val c = (the o (parse thy)) s;
|
neuper@37906
|
85 |
val c =
|
neuper@37906
|
86 |
"Script make_fun_explicit =
|
neuper@37981
|
87 |
Input [Real f_, Real v_v, BoolList eqs_]
|
neuper@37906
|
88 |
Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
|
neuper@37906
|
89 |
Tacs [SEQU
|
neuper@37906
|
90 |
[let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);
|
neuper@37906
|
91 |
vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
|
neuper@37906
|
92 |
in Subproblem Spec (R, [univar, equation], no_met)
|
neuper@37906
|
93 |
InOut [In eq_, In v1_, Out ss_]],
|
neuper@37906
|
94 |
Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
|
neuper@37906
|
95 |
Return [Currform]" : cterm
|
neuper@37906
|
96 |
ML>
|