(*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_v itv_ err_ =

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

        t_ =

          if #1 < Length rs_

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

          else (Lhs o hd) rs_;

        mx_ =

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

                           maximum_on_interval) t_ v_v itv_

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

       mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm

ML> set show_types;

ML> c;

val c =

  "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool =

    let e_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_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_v itv_

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

       mx_ t_ v_v m_ dropWhile (op = e_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_v, RealSet itv_, Bool err_]

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

    Tacs [SEQU

           [let e_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_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_v, In itv_, In err_, Out mx_] ;

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

             InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_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_f, Real v_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_f, Real v_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>