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