neuper@37906: (*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
neuper@37906: 
neuper@37906: (* Das erste Script aus dem Maximum-Beispiel.
neuper@37906:    parse erzeugt aus dem string 's' den 
neuper@37906:   'cterm 's' im Isabelle-Format (pretty-printing !)*)
neuper@37906: 
neuper@37906: ML> ...
neuper@37906: ML> val c = (the o (parse thy)) s; 
neuper@37906: val c =
neuper@37981:   "Script1 Maximum_value fix_ m_ rs_ v_v itv_ err_ =
neuper@37981:     let e_e = (hd o filter (Testvar m_)) rs_;
neuper@37906:         t_ =
neuper@37906:           if #1 < Length rs_
neuper@37981:           then make_fun (R, [make, function], no_met) m_ v_v rs_
neuper@37906:           else (Lhs o hd) rs_;
neuper@37906:         mx_ =
neuper@37906:           max_on_interval (R, [on_interval, max_of, function],
neuper@37981:                            maximum_on_interval) t_ v_v itv_
neuper@37906:     in find_vals (R, [find_values, tool], find_values)
neuper@37981:        mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
neuper@37906: 
neuper@37906: ML> set show_types;
neuper@37906: ML> c;
neuper@37906: val c =
neuper@37991:   "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_v::real itv_v::real set err_::bool =
neuper@37981:     let e_e::bool = (hd o filter (Testvar m_)) rs_;
neuper@37906:         t_::real =
neuper@37906:           if (#1::real) < Length rs_
neuper@37981:           then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_v rs_
neuper@37906:           else (Lhs o hd) rs_;
neuper@37906:         mx_::real =
neuper@37906:           max_on_interval (R, [on_interval::ID, max_of::ID, function],
neuper@37981:                            maximum_on_interval::ID) t_ v_v itv_
neuper@37906:     in find_vals (R, [find_values::ID, tool::ID], find_values)
neuper@37981:        mx_ t_ v_v m_ dropWhile (op = e_e) rs_" : cterm
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (* Die ersten 3 Scripts aus dem Maximum-Beispiel.
neuper@37906:    parse erzeugt aus dem string 's' den 
neuper@37906:   'cterm 's' im Isabelle-Format (pretty-printing !)*)
neuper@37906: 
neuper@37906: ML> ...
neuper@37906: ML> val c = (the o (parse thy)) s; 
neuper@37906: val c =
neuper@37906:   "Script maximum =
neuper@37981:     Input [Bool fix_, Real m_, BoolList rs_, Real v_v, RealSet itv_, Bool err_]
neuper@37981:     Local [Bool e_e, Real t_, Real mx_, RealList vs_]
neuper@37906:     Tacs [SEQU
neuper@37981:            [let e_e = (hd o filter (Testvar m_)) rs_
neuper@37906:             in if #1 < Length rs_
neuper@37906:                then Subproblem Spec (R, [make, function], no_met)
neuper@37981:                      InOut [In m_, In v_v, In rs_, Out t_]
neuper@37906:                else t_ := (Lhs o hd) rs_ ;
neuper@37906:             Subproblem Spec (R, [on_interval, max_of, function],
neuper@37906:                              maximum_on_interval)
neuper@37981:              InOut [In t_, In v_v, In itv_, In err_, Out mx_] ;
neuper@37906:             Subproblem Spec (R, [find_values, tool], find_values)
neuper@37981:              InOut [In mx_, In t_, In v_v, In m_, In (dropWhile (op = e_e) rs_),
neuper@37906:                     Out vs_]]]
neuper@37906:     Return []" : cterm
neuper@37906: 
neuper@37906: ML> ...
neuper@37906: ML> val c = (the o (parse thy)) s; 
neuper@37906: val c =
neuper@37906:   "Script make_fun_by_new_variable =
neuper@37994:     Input [Real f_f, Real v_v, BoolList eqs]
neuper@37906:     Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
neuper@37906:            Bool e2_, BoolList s_1, BoolList s_2]
neuper@37906:     Tacs [SEQU
neuper@37994:            [let h_ = (hd o filter (Testvar m_)) eqs; es_ = eqs -- [h_];
neuper@37906:                 vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
neuper@37906:                 e1_ = (hd o filter (Testvar v1_)) es_;
neuper@37906:                 e2_ = (hd o filter (Testvar v2_)) es_
neuper@37906:             in Subproblem Spec (R, [univar, equation], no_met)
neuper@37906:                 InOut [In e1_, In v1_, Out s_1] ;
neuper@37906:                Subproblem Spec (R, [univar, equation], no_met)
neuper@37906:                 InOut [In e2_, In v2_, Out s_2]],
neuper@37906:           Take (Bool h_) ;
neuper@37906:           Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
neuper@37906:     Return [Currform]" : cterm
neuper@37906: 
neuper@37906: ML> ...
neuper@37906: ML> val c = (the o (parse thy)) s; 
neuper@37906: val c =
neuper@37906:   "Script make_fun_explicit =
neuper@37994:     Input [Real f_f, Real v_v, BoolList eqs]
neuper@37906:     Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
neuper@37906:     Tacs [SEQU
neuper@37994:            [let h_ = (hd o filter (Testvar m_)) eqs; eq_ = hd (eqs -- [h_]);
neuper@37906:                 vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
neuper@37906:             in Subproblem Spec (R, [univar, equation], no_met)
neuper@37906:                 InOut [In eq_, In v1_, Out ss_]],
neuper@37906:           Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
neuper@37906:     Return [Currform]" : cterm
neuper@37906: ML>