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@37995
|
10 |
"Script1 Maximum_value f_ix m_ r_s v_v itv_ err_ =
|
neuper@37995
|
11 |
let e_e = (hd o filter (Testvar m_)) r_s;
|
neuper@37906
|
12 |
t_ =
|
neuper@37995
|
13 |
if #1 < Length r_s
|
neuper@37995
|
14 |
then make_fun (R, [make, function], no_met) m_ v_v r_s
|
neuper@37995
|
15 |
else (Lhs o hd) r_s;
|
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@37995
|
20 |
mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : cterm
|
neuper@37906
|
21 |
|
neuper@37906
|
22 |
ML> set show_types;
|
neuper@37906
|
23 |
ML> c;
|
neuper@37906
|
24 |
val c =
|
neuper@37995
|
25 |
"Script1 Maximum_value f_ix::bool list m_::real r_s::bool list v_v::real itv_v::real set err_::bool =
|
neuper@37995
|
26 |
let e_e::bool = (hd o filter (Testvar m_)) r_s;
|
neuper@37906
|
27 |
t_::real =
|
neuper@37995
|
28 |
if (#1::real) < Length r_s
|
neuper@37995
|
29 |
then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v r_s
|
neuper@37995
|
30 |
else (Lhs o hd) r_s;
|
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@37995
|
35 |
mx_ t_ v_v m_ dropWhile (op = e_e) r_s" : 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@37995
|
47 |
Input [Bool f_ix, Real m_, BoolList r_s, Real v_v, RealSet itv_, Bool err_]
|
neuper@37995
|
48 |
Local [Bool e_e, Real t_, Real mx_, RealList v_s]
|
neuper@37906
|
49 |
Tacs [SEQU
|
neuper@37995
|
50 |
[let e_e = (hd o filter (Testvar m_)) r_s
|
neuper@37995
|
51 |
in if #1 < Length r_s
|
neuper@37906
|
52 |
then Subproblem Spec (R, [make, function], no_met)
|
neuper@37995
|
53 |
InOut [In m_, In v_v, In r_s, Out t_]
|
neuper@37995
|
54 |
else t_ := (Lhs o hd) r_s ;
|
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@37995
|
59 |
InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) r_s),
|
neuper@37995
|
60 |
Out v_s]]]
|
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@37994
|
67 |
Input [Real f_f, Real v_v, BoolList eqs]
|
neuper@37995
|
68 |
Local [Bool h_, BoolList es_, RealList v_s, Real v1_, Real v2_, Bool e1,
|
neuper@37906
|
69 |
Bool e2_, BoolList s_1, BoolList s_2]
|
neuper@37906
|
70 |
Tacs [SEQU
|
neuper@37994
|
71 |
[let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_];
|
neuper@37995
|
72 |
v_s = Var h_ -- [f_]; v1_ = Nth #1 v_s; v2_ = Nth #2 v_s;
|
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@37994
|
87 |
Input [Real f_f, Real v_v, BoolList eqs]
|
neuper@37995
|
88 |
Local [Bool h_, Bool eq_, RealList v_s, Real v1_, BoolList ss_]
|
neuper@37906
|
89 |
Tacs [SEQU
|
neuper@37994
|
90 |
[let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]);
|
neuper@37995
|
91 |
v_s = Var h_ -- [f_]; v1_ = hd (v_s -- [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>
|