(*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)

 (* Das erste Script aus dem Maximum-Beispiel.

    parse erzeugt aus dem string 's' den 

   'cterm 's' im Isabelle-Format (pretty-printing !)*)

 ML> ...

 ML> val c = (the o (parse thy)) s; 

 val c =

   "Script1 Maximum_value fix_ m_ rs_ v_ itv_ err_ =

     let e_ = (hd o filter (Testvar m_)) rs_;

         t_ =

           if #1 < Length rs_

           then make_fun (R, [make, function], no_met) m_ v_ rs_

           else (Lhs o hd) rs_;

         mx_ =

           max_on_interval (R, [on_interval, max_of, function],

                            maximum_on_interval) t_ v_ itv_

     in find_vals (R, [find_values, tool], find_values)

        mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm

 ML> set show_types;

 ML> c;

 val c =

   "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_::real itv_::real set err_::bool =

     let e_::bool = (hd o filter (Testvar m_)) rs_;

         t_::real =

           if (#1::real) < Length rs_

           then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_ rs_

           else (Lhs o hd) rs_;

         mx_::real =

           max_on_interval (R, [on_interval::ID, max_of::ID, function],

                            maximum_on_interval::ID) t_ v_ itv_

     in find_vals (R, [find_values::ID, tool::ID], find_values)

        mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm

 (* Die ersten 3 Scripts aus dem Maximum-Beispiel.

    parse erzeugt aus dem string 's' den 

   'cterm 's' im Isabelle-Format (pretty-printing !)*)

 ML> ...

 ML> val c = (the o (parse thy)) s; 

 val c =

   "Script maximum =

     Input [Bool fix_, Real m_, BoolList rs_, Real v_, RealSet itv_, Bool err_]

     Local [Bool e_, Real t_, Real mx_, RealList vs_]

     Tacs [SEQU

            [let e_ = (hd o filter (Testvar m_)) rs_

             in if #1 < Length rs_

                then Subproblem Spec (R, [make, function], no_met)

                      InOut [In m_, In v_, In rs_, Out t_]

                else t_ := (Lhs o hd) rs_ ;

             Subproblem Spec (R, [on_interval, max_of, function],

                              maximum_on_interval)

              InOut [In t_, In v_, In itv_, In err_, Out mx_] ;

             Subproblem Spec (R, [find_values, tool], find_values)

              InOut [In mx_, In t_, In v_, In m_, In (dropWhile (op = e_) rs_),

                     Out vs_]]]

     Return []" : cterm

 ML> ...

 ML> val c = (the o (parse thy)) s; 

 val c =

   "Script make_fun_by_new_variable =

     Input [Real f_, Real v_, BoolList eqs_]

     Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,

            Bool e2_, BoolList s_1, BoolList s_2]

     Tacs [SEQU

            [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];

                 vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;

                 e1_ = (hd o filter (Testvar v1_)) es_;

                 e2_ = (hd o filter (Testvar v2_)) es_

             in Subproblem Spec (R, [univar, equation], no_met)

                 InOut [In e1_, In v1_, Out s_1] ;

                Subproblem Spec (R, [univar, equation], no_met)

                 InOut [In e2_, In v2_, Out s_2]],

           Take (Bool h_) ;

           Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]

     Return [Currform]" : cterm

 ML> ...

 ML> val c = (the o (parse thy)) s; 

 val c =

   "Script make_fun_explicit =

     Input [Real f_, Real v_, BoolList eqs_]

     Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]

     Tacs [SEQU

            [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);

                 vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])

             in Subproblem Spec (R, [univar, equation], no_met)

                 InOut [In eq_, In v1_, Out ss_]],

           Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]

     Return [Currform]" : cterm

 ML>