1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/isac/IsacKnowledge/DiffApp-oldscr.sml Wed Jul 21 13:53:39 2010 +0200
1.3 @@ -0,0 +1,96 @@
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>