1 (*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
3 (* Das erste Script aus dem Maximum-Beispiel.
4 parse erzeugt aus dem string 's' den
5 'cterm 's' im Isabelle-Format (pretty-printing !)*)
8 ML> val c = (the o (parse thy)) s;
10 "Script1 Maximum_value fix_ m_ rs_ v_ itv_ err_ =
11 let e_ = (hd o filter (Testvar m_)) rs_;
14 then make_fun (R, [make, function], no_met) m_ v_ rs_
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
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_;
28 if (#1::real) < Length rs_
29 then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_ rs_
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
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 !)*)
44 ML> val c = (the o (parse thy)) s;
47 Input [Bool fix_, Real m_, BoolList rs_, Real v_, RealSet itv_, Bool err_]
48 Local [Bool e_, Real t_, Real mx_, RealList vs_]
50 [let e_ = (hd o filter (Testvar m_)) 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],
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_),
64 ML> val c = (the o (parse thy)) s;
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]
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]],
80 Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
81 Return [Currform]" : cterm
84 ML> val c = (the o (parse thy)) s;
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_]
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