1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/IsacKnowledge/DiffApp-oldpbl.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,369 @@
1.4 +(*8.01: aufgehoben wegen alter preconds, postconds*)
1.5 +
1.6 +(* rectangle with maximal area, inscribed in a circle of fixed radius
1.7 +
1.8 +problem-types and methods solving the respective problem-type
1.9 +
1.10 +(1) names of the problem-types and methods and their hierarchy
1.11 + as subproblems.
1.12 + names of problem-types are string lists (diss 5.3.), not shown
1.13 + here with exception of ["equation","univariate"] in order to
1.14 + indicate, that this particular problem needs refinement to a
1.15 + more specific type of equation solvable by tan-square, etc.
1.16 +
1.17 +problem-types methods
1.18 +------------------------------- ----------------------
1.19 +maximum maximum-by-differentiation
1.20 + maximum-by-experimentation
1.21 + make-fun make-explicit-and-substitute
1.22 + introduce-a-new-variable
1.23 + max-of-fun-on-interval max-of-fun-on-interval
1.24 + derivative differentiate
1.25 + ["equation","univariate"] tan-square
1.26 +
1.27 + find-values find-values
1.28 +
1.29 +(2) specification of the problem-types
1.30 +*)
1.31 +
1.32 +(* maximum *)
1.33 +(* ------- *)
1.34 +(* problem-type *)
1.35 +{given = ["fixed_values (cs::bool list)"],
1.36 + where_= ["foldl (op &) True (map is_equality cs)",
1.37 + "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
1.38 + find=["maximum m","values_for (ms::real list)"],
1.39 + with_=["Ex_frees ((foldl (op &) True (r#RS)) & \
1.40 + \ (ALL m'. (subst (m,m') (foldl (op &) True (r#RS)) \
1.41 + \ --> m' <= m)))"],
1.42 + relate=["max_relation r","additional_relations RS"]};
1.43 +(* ^^^ is exponenation *)
1.44 +
1.45 +(* the functions Ex_frees, Rhs provide for the instantiation below *)
1.46 +
1.47 +(* (1) instantiation of maximum, + variant in "values_for" *)
1.48 +{given = ["fixed_values (R = #7)"],
1.49 + where_= ["is_equality (R = #7)",
1.50 + "Not (R <= #0)"],
1.51 + find =["maximum A","values_for [a,b]"],
1.52 + with_ =["EX A. A = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.53 + \ (ALL A'. A' = a*b & (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2 \
1.54 + \ --> A' <= A)))"],
1.55 + relate=["max_relation (A = a*b)",
1.56 + "additional_relations [(a//#2)^^^#2 +(b//#2)^^^#2 =R^^^#2]"]};
1.57 +(* R,a,b are bound by given, find *)
1.58 +
1.59 +(* (2) instantiation of maximum *)
1.60 +{given = ["fixed_values (R = #7)"],
1.61 + where_= ["is_equality (R = #7)",
1.62 + "Not (R <= #0)"],
1.63 + find =["maximum A","values_for [A]"],
1.64 + with_ =["EX a b alpha. A = a*b & \
1.65 + \ a = #2*R*sin alpha & b =#2*R*cos alpha &\
1.66 + \ (ALL A'. A' = a*b & a = #2*R*sin alpha & b =#2*R*cos alpha \
1.67 + \ --> A' <= A)))"],
1.68 + relate=["max_relation (A = a*b)",
1.69 + "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]};
1.70 +(* R,A are bound by given, find *)
1.71 +
1.72 +
1.73 +(* make-fun *)
1.74 +(* -------- *)
1.75 +(* problem-type *)
1.76 +{given = ["equality (lhs = rhs)","bound_variable v","equalities es"],
1.77 + where_= [],
1.78 + find = ["function_term lhs_"],
1.79 + with_ = [(*???*)],
1.80 + relate= [(*???*)]};
1.81 +(*the _ in lhs is used to transfer the lhs-identifier of equality*)
1.82 +
1.83 +(* (1) instantiation for make-explicit-and-substitute *)
1.84 +{given = ["equality A = a * b","bound_variable a",
1.85 + "equalities [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]"],
1.86 + where_= [],
1.87 + find = ["function_term A_"(*=(a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))*)],
1.88 + with_ = [],
1.89 + relate= []};
1.90 +
1.91 +(* (2) instantiation for introduce-a-new-variable *)
1.92 +{given = ["equality A = a * b","bound_variable alpha",
1.93 + "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.94 + where_= [],
1.95 + find = ["function_term A_"(*=(#2*R*sin alpha *#2*R*cos alpha)*)],
1.96 + with_ = [],
1.97 + relate= []};
1.98 +
1.99 +
1.100 +(* max-of-fun-on-interval *)
1.101 +(* ---------------------- *)
1.102 +(* problem-type *)
1.103 +{given = ["function_term t","bound_variable v",
1.104 + "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.105 + where_= [],
1.106 + find = ["maximums ms"],
1.107 + with_ = ["ALL m. m : ms --> \
1.108 + \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.109 + \ --> (%v. t) x <= m)"],
1.110 + relate= []}: string ppc;
1.111 +(* ':' is 'element', '::' is a type constraint *)
1.112 +
1.113 +(* (1) variant of instantiation *)
1.114 +{given = ["function_term (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))",
1.115 + "bound_variable a",
1.116 + "domain {x::real. #0 <= x & x <= #2*R}"],
1.117 + where_= [],
1.118 + find = ["maximums AM"],
1.119 + with_ = ["ALL am. am : AM --> \
1.120 + \ (ALL x::real. #0 <= x & x <= #2*R \
1.121 + \ --> (%a. (a * #2 * sqrt(R^^^#2 - (a//#2)^^^#2))) x <= am)"],
1.122 + relate= []};
1.123 +
1.124 +(* (2) variant of instantiation *)
1.125 +{given = ["function_term (#2*R*sin alpha * #2*R*cos alpha)",
1.126 + "bound_variable alpha",
1.127 + "domain {x::real. #0 <= x & x <= pi//#2}"],
1.128 + where_= [],
1.129 + find = ["maximums AM"],
1.130 + with_ = ["ALL am. am : AM --> \
1.131 + \ (ALL x::real. #0 <= x & x <= pi//#2 \
1.132 + \ --> (%alpha. (#2*R*sin alpha * #2*R*cos alpha)) x <= am)"],
1.133 + relate= []};
1.134 +
1.135 +
1.136 +(* derivative *)
1.137 +(* ---------- *)
1.138 +(* problem-type *)
1.139 +{given = ["function_term t","bound_variable bdv"],
1.140 + where_= [],
1.141 + find = ["derivative t'"],
1.142 + with_ = ["t' is_derivative_of (%bdv. t)"],
1.143 + relate= []};
1.144 +(*the ' in t' is used to transfer the identifier from function_term*)
1.145 +
1.146 +
1.147 +(* ["equation","univariate"] *)
1.148 +(* ------------------------- *)
1.149 +(* problem-type *)
1.150 +{given = ["equality (lhs = rhs)",
1.151 + "bound_variable v","error_bound eps"],
1.152 + where_= [],
1.153 + find = ["solutions S"],
1.154 + with_ = ["ALL s. s : S --> || (%v. lhs) s - (%v. rhs) s || <= eps"],
1.155 + relate= []};
1.156 +
1.157 +
1.158 +(* find-values *)
1.159 +(* ----------- *)
1.160 +(* problem-type *)
1.161 +{given = ["max_relation r","additional_relations RS"],
1.162 + where_= [],
1.163 + find = ["values_for VS"],
1.164 + with_ = [(*???*)],
1.165 + relate= []};
1.166 +
1.167 +(* (1) variant of instantiation *)
1.168 +{given = ["max_relation (A = a*b)",
1.169 + "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]"],
1.170 + where_= [],
1.171 + find = ["values_for [a,b]"],
1.172 + with_ = [],
1.173 + relate= []};
1.174 +
1.175 +(* (2) variant of instantiation *)
1.176 +{given = ["max_relation (A = a*b)",],
1.177 + where_= [],
1.178 + find = ["values_for [A]",
1.179 + "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.180 + with_ = [],
1.181 + relate= []};
1.182 +
1.183 +(*
1.184 +(3) data-transfer between the the hidden formalization,
1.185 + the root-problem and the sub-problems;
1.186 +
1.187 +maximum -> #given.make-fun
1.188 +-------------------
1.189 +maximum.#relate "max_relation r" -> "equality (lhs = rhs)"
1.190 +formalization "bound_variable v" -> "bound_variable v"
1.191 +maximum.#relate "additional_relations RS"-> "equalities es"
1.192 +
1.193 +
1.194 +maximum + make-fun -> #given.max-of-fun-on-interval
1.195 +--------------------------------------------
1.196 +make-fun.#find "function_term lhs_" -> "function_term t"
1.197 +make-fun.#given "bound_variable v" -> "bound_variable v"
1.198 +formalization -> "domain {x::real. ...}"
1.199 +
1.200 +
1.201 +max-of-fun-on-interval -> #given.derivative
1.202 +------------------------------------
1.203 +make-fun.#find "function_term lhs_" -> "function_term t"
1.204 +make-fun.#given "bound_variable v" -> "bound_variable bdv"
1.205 +
1.206 +
1.207 +max-of-fun-on-interval + derivative ->
1.208 + #given.["equation","univariate"]
1.209 +----------------------------------------------------------------
1.210 +derivative.#find "derivative t'" -> "equality (lhs = rhs)"
1.211 + (* t'= #0 *)
1.212 +make-fun.#given "bound_variable v" -> "bound_variable v"
1.213 +formalization -> "error_bound eps"
1.214 +
1.215 +
1.216 +maximum + make-fun + max-of-fun-on-interval -> #given.find-values
1.217 +----------------------------------------------------------
1.218 +maximum.#relate "max_relation r" -> "max_relation r"
1.219 +maximum.#relate "additional_relations RS"-> "additional_relations RS"
1.220 +*)
1.221 +
1.222 +
1.223 +
1.224 +
1.225 +(* vvv--- geht nicht wegen fun-types
1.226 +parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";
1.227 +parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";
1.228 +parse thy "if a=b then a else b";
1.229 +parse thy "maxmin = is_max";
1.230 +parse thy "maxmin =!= is_max";
1.231 + ^^^--- geht nicht wegen fun-types *)
1.232 +
1.233 +"pbltyp --- maximum ---";
1.234 +val pbltyp = {given=["fixed_values (cs::bool list)"],
1.235 + where_=["foldl (op &) True (map is_equality cs)",
1.236 + "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"],
1.237 + find=["maximum m","values_for (ms::real list)"],
1.238 + with_=["Ex_frees ((foldl (op &) True (r#rs)) & \
1.239 + \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
1.240 + \ --> m' <= m)))"],
1.241 + relate=["max_relation r","additional_relations rs"]}:string ppc;
1.242 +val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.243 +"coil";
1.244 +val org = ["fixed_values [R=(R::real)]",
1.245 + "bound_variable a", "bound_variable b", "bound_variable alpha",
1.246 + "domain {x::real. #0 <= x & x <= #2*R}",
1.247 + "domain {x::real. #0 <= x & x <= #2*R}",
1.248 + "domain {x::real. #0 <= x & x <= pi}",
1.249 + "maximum A",
1.250 + "max_relation A=#2*a*b - a^^^#2",
1.251 + "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.252 + "additional_relations [(a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
1.253 + "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
1.254 +val chkorg = map (the o (parse thy)) org;
1.255 +val pbl = {given=["fixed_values [R=(R::real)]"],where_=[],
1.256 + find=["maximum A","values_for [a,b]"],
1.257 + with_=["EX alpha. A=#2*a*b - a^^^#2 & \
1.258 + \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
1.259 + \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha & b=#2*R*cos alpha \
1.260 + \ --> A' <= A)"],
1.261 + relate=["max_relation (A=#2*a*b - a^^^#2)",
1.262 + "additional_relations [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
1.263 + }: string ppc;
1.264 +val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.265 +
1.266 +"met --- maximum_by_differentiation ---";
1.267 +val met = {given=["fixed_values (cs::bool list)","bound_variable v",
1.268 + "domain {x::real. lower_bound <= x & x <= upper_bound}",
1.269 + "approximation apx"],
1.270 + where_=[],
1.271 + find=["maximum m","values_for (ms::real list)",
1.272 + "function_term t","max_argument mx"],
1.273 + with_=["Ex_frees ((foldl (op &) True (rs::bool list)) & \
1.274 + \ (ALL m'. (subst (m,m') (foldl (op &) True rs) \
1.275 + \ --> m' <= m))) & \
1.276 + \m = (%v. t) mx & \
1.277 + \( ALL x. lower_bound <= x & x <= upper_bound \
1.278 + \ --> (%v. t) x <= m)"],
1.279 + relate=["rs::bool list"]}: string ppc;
1.280 +val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
1.281 +
1.282 +
1.283 +"pbltyp --- make_fun ---";
1.284 +(* subproblem [(hd #relate root, equality),
1.285 + (bound_variable formalization, bound_variable),
1.286 + (tl #relate root, equalities)] *)
1.287 +val pbltyp = {given=["equality e","bound_variable v", "equalities es"],
1.288 + where_=[],
1.289 + find=["function_term t"],with_=[(*???*)],
1.290 + relate=[(*???*)]}: string ppc;
1.291 +val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.292 +"coil";
1.293 +val pbl = {given=["equality (A=#2*a*b - a^^^#2)","bound_variable alpha",
1.294 + "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
1.295 + where_=[],
1.296 + find=["function_term t"],
1.297 + with_=[],relate=[]}: string ppc;
1.298 +val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.299 +
1.300 +"met --- make_explicit_and_substitute ---";
1.301 +val met = {given=["equality e","bound_variable v", "equalities es"],
1.302 + where_=[],
1.303 + find=["function_term t"],with_=[(*???*)],
1.304 + relate=[(*???*)]}: string ppc;
1.305 +val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.306 +"met --- introduce_a_new_variable ---";
1.307 +val met = {given=["equality e","bound_variable v", "substitutions es"],
1.308 + where_=[],
1.309 + find=["function_term t"],with_=[(*???*)],
1.310 + relate=[(*???*)]}: string ppc;
1.311 +val chkmet = ((map (the o (parse thy))) o ppc2list) met;
1.312 +
1.313 +
1.314 +"pbltyp --- max_of_fun_on_interval ---";
1.315 +val pbltyp = {given=["function_term t","bound_variable v",
1.316 + "domain {x::real. lower_bound <= x & x <= upper_bound}"],
1.317 + where_=[],
1.318 + find=["maximums ms"],
1.319 + with_=["ALL m. m : ms --> \
1.320 + \ (ALL x::real. lower_bound <= x & x <= upper_bound \
1.321 + \ --> (%v. t) x <= m)"],
1.322 + relate=[]}: string ppc;
1.323 +val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
1.324 +"coil";
1.325 +val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
1.326 + \ (#2*R*sin alpha)^^^#2","bound_variable alpha",
1.327 + "domain {x::real. #0 <= x & x <= pi}"],where_=[],
1.328 + find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
1.329 +val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
1.330 +
1.331 +
1.332 +(* pbltyp --- max_of_fun --- *)
1.333 +(*
1.334 +{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.335 +val (Some ct) = parse thy ;
1.336 +atomty thy (term_of ct);
1.337 +*)
1.338 +
1.339 +
1.340 +
1.341 +
1.342 +
1.343 +
1.344 +
1.345 +
1.346 +(* --- 14.1.00 --- *)
1.347 +"p.114";
1.348 +val org = {given=["[u=(#12::real)]"],where_=[],
1.349 + find=["[a,(b::real)]"],with_=[],
1.350 + relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
1.351 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.352 +"p.116";
1.353 +val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
1.354 + find=["[x,(y::real)]"],with_=[],
1.355 + relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
1.356 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.357 +"p.117";
1.358 +val org = {given=["[r=#5]"],where_=[],
1.359 + find=["[x,(y::real)]"],with_=[],
1.360 + relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
1.361 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.362 +"#241";
1.363 +val org = {given=["[s=(#10::real)]"],where_=[],
1.364 + find=["[p::real]"],with_=[],
1.365 + relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
1.366 +val chkorg = ((map (the o (parse thy))) o ppc2list) org;
1.367 +
1.368 +(*
1.369 +{given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
1.370 +val (Some ct) = parse thy ;
1.371 +atomty thy (term_of ct);
1.372 +*)
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/IsacKnowledge/DiffApp-oldscr.sml Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,96 @@
2.4 +(*8.01: alte Scripts f"ur Extremwertaufgabe gesammelt*)
2.5 +
2.6 +(* Das erste Script aus dem Maximum-Beispiel.
2.7 + parse erzeugt aus dem string 's' den
2.8 + 'cterm 's' im Isabelle-Format (pretty-printing !)*)
2.9 +
2.10 +ML> ...
2.11 +ML> val c = (the o (parse thy)) s;
2.12 +val c =
2.13 + "Script1 Maximum_value fix_ m_ rs_ v_ itv_ err_ =
2.14 + let e_ = (hd o filter (Testvar m_)) rs_;
2.15 + t_ =
2.16 + if #1 < Length rs_
2.17 + then make_fun (R, [make, function], no_met) m_ v_ rs_
2.18 + else (Lhs o hd) rs_;
2.19 + mx_ =
2.20 + max_on_interval (R, [on_interval, max_of, function],
2.21 + maximum_on_interval) t_ v_ itv_
2.22 + in find_vals (R, [find_values, tool], find_values)
2.23 + mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
2.24 +
2.25 +ML> set show_types;
2.26 +ML> c;
2.27 +val c =
2.28 + "Script1 Maximum_value fix_::bool list m_::real rs_::bool list v_::real itv_::real set err_::bool =
2.29 + let e_::bool = (hd o filter (Testvar m_)) rs_;
2.30 + t_::real =
2.31 + if (#1::real) < Length rs_
2.32 + then make_fun (R::ID, [make::ID, function::ID], no_met::ID) m_ v_ rs_
2.33 + else (Lhs o hd) rs_;
2.34 + mx_::real =
2.35 + max_on_interval (R, [on_interval::ID, max_of::ID, function],
2.36 + maximum_on_interval::ID) t_ v_ itv_
2.37 + in find_vals (R, [find_values::ID, tool::ID], find_values)
2.38 + mx_ t_ v_ m_ dropWhile (op = e_) rs_" : cterm
2.39 +
2.40 +
2.41 +
2.42 +(* Die ersten 3 Scripts aus dem Maximum-Beispiel.
2.43 + parse erzeugt aus dem string 's' den
2.44 + 'cterm 's' im Isabelle-Format (pretty-printing !)*)
2.45 +
2.46 +ML> ...
2.47 +ML> val c = (the o (parse thy)) s;
2.48 +val c =
2.49 + "Script maximum =
2.50 + Input [Bool fix_, Real m_, BoolList rs_, Real v_, RealSet itv_, Bool err_]
2.51 + Local [Bool e_, Real t_, Real mx_, RealList vs_]
2.52 + Tacs [SEQU
2.53 + [let e_ = (hd o filter (Testvar m_)) rs_
2.54 + in if #1 < Length rs_
2.55 + then Subproblem Spec (R, [make, function], no_met)
2.56 + InOut [In m_, In v_, In rs_, Out t_]
2.57 + else t_ := (Lhs o hd) rs_ ;
2.58 + Subproblem Spec (R, [on_interval, max_of, function],
2.59 + maximum_on_interval)
2.60 + InOut [In t_, In v_, In itv_, In err_, Out mx_] ;
2.61 + Subproblem Spec (R, [find_values, tool], find_values)
2.62 + InOut [In mx_, In t_, In v_, In m_, In (dropWhile (op = e_) rs_),
2.63 + Out vs_]]]
2.64 + Return []" : cterm
2.65 +
2.66 +ML> ...
2.67 +ML> val c = (the o (parse thy)) s;
2.68 +val c =
2.69 + "Script make_fun_by_new_variable =
2.70 + Input [Real f_, Real v_, BoolList eqs_]
2.71 + Local [Bool h_, BoolList es_, RealList vs_, Real v1_, Real v2_, Bool e1,
2.72 + Bool e2_, BoolList s_1, BoolList s_2]
2.73 + Tacs [SEQU
2.74 + [let h_ = (hd o filter (Testvar m_)) eqs_; es_ = eqs_ -- [h_];
2.75 + vs_ = Var h_ -- [f_]; v1_ = Nth #1 vs_; v2_ = Nth #2 vs_;
2.76 + e1_ = (hd o filter (Testvar v1_)) es_;
2.77 + e2_ = (hd o filter (Testvar v2_)) es_
2.78 + in Subproblem Spec (R, [univar, equation], no_met)
2.79 + InOut [In e1_, In v1_, Out s_1] ;
2.80 + Subproblem Spec (R, [univar, equation], no_met)
2.81 + InOut [In e2_, In v2_, Out s_2]],
2.82 + Take (Bool h_) ;
2.83 + Substitute [(v_1, (Rhs o hd) s_1), (v_2, (Rhs o hd) s_2)]]
2.84 + Return [Currform]" : cterm
2.85 +
2.86 +ML> ...
2.87 +ML> val c = (the o (parse thy)) s;
2.88 +val c =
2.89 + "Script make_fun_explicit =
2.90 + Input [Real f_, Real v_, BoolList eqs_]
2.91 + Local [Bool h_, Bool eq_, RealList vs_, Real v1_, BoolList ss_]
2.92 + Tacs [SEQU
2.93 + [let h_ = (hd o filter (Testvar m_)) eqs_; eq_ = hd (eqs_ -- [h_]);
2.94 + vs_ = Var h_ -- [f_]; v1_ = hd (vs_ -- [v_])
2.95 + in Subproblem Spec (R, [univar, equation], no_met)
2.96 + InOut [In eq_, In v1_, Out ss_]],
2.97 + Take (Bool h_) ; Substitute [(v1_, (Rhs o hd) ss_)]]
2.98 + Return [Currform]" : cterm
2.99 +ML>