1.1 --- a/src/Tools/isac/IsacKnowledge/DiffApp-oldscr.sml	Wed Aug 25 15:15:01 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,96 +0,0 @@
     1.4 -(*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
     1.5 -
     1.6 -(* Das erste Script aus dem Maximum-Beispiel.
     1.7 -   parse erzeugt aus dem string 's' den 
     1.8 -  'cterm 's' im Isabelle-Format (pretty-printing !)*)
     1.9 -
    1.10 -ML> ...
    1.11 -ML> val c = (the o (parse thy)) s; 
    1.12 -val c =
    1.13 -  "Script1 Maximum_value fix_ m_ rs_ v_ itv_ err_ =
    1.14 -    let e_ = (hd o filter (Testvar m_)) rs_;
    1.15 -        t_ =
    1.16 -          if #1 < Length rs_
    1.17 -          then make_fun (R, [make, function], no_met) m_ v_ rs_
    1.18 -          else (Lhs o hd) rs_;
    1.19 -        mx_ =
    1.20 -          max_on_interval (R, [on_interval, max_of, function],
    1.21 -                           maximum_on_interval) t_ v_ itv_
    1.22 -    in find_vals (R, [find_values, tool], find_values)
    1.23 -       mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
    1.24 -
    1.25 -ML> set show_types;
    1.26 -ML> c;
    1.27 -val c =
    1.28 -  "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_::real itv_::real set err_::bool =
    1.29 -    let e_::bool = (hd o filter (Testvar m_)) rs_;
    1.30 -        t_::real =
    1.31 -          if (#1::real) < Length rs_
    1.32 -          then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_ rs_
    1.33 -          else (Lhs o hd) rs_;
    1.34 -        mx_::real =
    1.35 -          max_on_interval (R, [on_interval::ID, max_of::ID, function],
    1.36 -                           maximum_on_interval::ID) t_ v_ itv_
    1.37 -    in find_vals (R, [find_values::ID, tool::ID], find_values)
    1.38 -       mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
    1.39 -
    1.40 -
    1.41 -
    1.42 -(* Die ersten 3 Scripts aus dem Maximum-Beispiel.
    1.43 -   parse erzeugt aus dem string 's' den 
    1.44 -  'cterm 's' im Isabelle-Format (pretty-printing !)*)
    1.45 -
    1.46 -ML> ...
    1.47 -ML> val c = (the o (parse thy)) s; 
    1.48 -val c =
    1.49 -  "Script maximum =
    1.50 -    Input [Bool fix_, Real m_, BoolList rs_, Real v_, RealSet itv_, Bool err_]
    1.51 -    Local [Bool e_, Real t_, Real mx_, RealList vs_]
    1.52 -    Tacs [SEQU
    1.53 -           [let e_ = (hd o filter (Testvar m_)) rs_
    1.54 -            in if #1 < Length rs_
    1.55 -               then Subproblem Spec (R, [make, function], no_met)
    1.56 -                     InOut [In m_, In v_, In rs_, Out t_]
    1.57 -               else t_ := (Lhs o hd) rs_ ;
    1.58 -            Subproblem Spec (R, [on_interval, max_of, function],
    1.59 -                             maximum_on_interval)
    1.60 -             InOut [In t_, In v_, In itv_, In err_, Out mx_] ;
    1.61 -            Subproblem Spec (R, [find_values, tool], find_values)
    1.62 -             InOut [In mx_, In t_, In v_, In m_, In (dropWhile (op = e_) rs_),
    1.63 -                    Out vs_]]]
    1.64 -    Return []" : cterm
    1.65 -
    1.66 -ML> ...
    1.67 -ML> val c = (the o (parse thy)) s; 
    1.68 -val c =
    1.69 -  "Script make_fun_by_new_variable =
    1.70 -    Input [Real f_, Real v_, BoolList eqs_]
    1.71 -    Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
    1.72 -           Bool e2_, BoolList s_1, BoolList s_2]
    1.73 -    Tacs [SEQU
    1.74 -           [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];
    1.75 -                vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
    1.76 -                e1_ = (hd o filter (Testvar v1_)) es_;
    1.77 -                e2_ = (hd o filter (Testvar v2_)) es_
    1.78 -            in Subproblem Spec (R, [univar, equation], no_met)
    1.79 -                InOut [In e1_, In v1_, Out s_1] ;
    1.80 -               Subproblem Spec (R, [univar, equation], no_met)
    1.81 -                InOut [In e2_, In v2_, Out s_2]],
    1.82 -          Take (Bool h_) ;
    1.83 -          Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
    1.84 -    Return [Currform]" : cterm
    1.85 -
    1.86 -ML> ...
    1.87 -ML> val c = (the o (parse thy)) s; 
    1.88 -val c =
    1.89 -  "Script make_fun_explicit =
    1.90 -    Input [Real f_, Real v_, BoolList eqs_]
    1.91 -    Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
    1.92 -    Tacs [SEQU
    1.93 -           [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);
    1.94 -                vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
    1.95 -            in Subproblem Spec (R, [univar, equation], no_met)
    1.96 -                InOut [In eq_, In v1_, Out ss_]],
    1.97 -          Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
    1.98 -    Return [Currform]" : cterm
    1.99 -ML>