1 (* use"test-coil-kernel.sml";
6 (* vvv--- geht nicht wegen fun-types
7 parse thy "case maxmin of is_max => (m' <= m) | is_min => (m <= m')";
8 parse thy "if maxmin = is_max then (m' <= m) else (m <= m')";
9 parse thy "if a=b then a else b";
10 parse thy "maxmin = is_max";
11 parse thy "maxmin =!= is_max";
12 ^^^--- geht nicht wegen fun-types *)
14 "pbltyp --- maximum ---";
15 val pbltyp = {given=["fixedValues (cs::bool list)"],
16 where_=[(*"foldl (op &) True (map is_equality cs)",
17 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"*)],
18 find=["maximum m","values_for (ms::real list)"],
19 with_=[(*"Ex_frees ((foldl (op &) True (r#rs)) & \
20 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \
22 relate=["max_relation r","additionalRels rs"]}:string ppc;
23 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
25 val org = ["fixedValues [R=(R::real)]",
26 "boundVariable a","boundVariable b","boundVariable alpha",
27 "domain {x::real. #0 <= x & x <= #2*R}",
28 "domain {x::real. #0 <= x & x <= #2*R}",
29 "domain {x::real. #0 <= x & x <= pi}",
30 "errorBound (eps = #1//#1000)",
32 (*"max_relation A=#2*a*b - a^^^#2",*)
33 "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
34 "relations [A=#2*a*b - a^^^#2, (a//#2)^^^#2 + (b//#2)^^^#2 = R^^^#2]",
35 "relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"];
36 val chkorg = map (the o (parse thy)) org;
37 val pbl = {given=["fixedValues [R=(R::real)]"],where_=[],
38 find=["maximum A","values_for [a,b]"],
39 with_=[(* incompat.w. parse, ok with parseold
40 "EX alpha. A=#2*a*b - a^^^#2 & \
41 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \
42 \ (ALL A'. A'=#2*a*b - a^^^#2 & a=#2*R*sin alpha \
43 \ & b=#2*R*cos alpha \
45 relate=["relations [A=#2*a*b - a^^^#2, a=#2*R*sin alpha, b=#2*R*cos alpha]"]
47 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
49 "met --- maximum_by_differentiation ---";
50 val met = {given=["fixedValues (cs::bool list)","boundVariable v",
51 "domain {x::real. lower_bound <= x & x<=upper_bound}",
52 "errorBound epsilon"],
54 find=["maximum m","valuesFor (ms::bool list)",
55 "function_term t","max_argument mx"],
56 with_=[(* incompat.w. parse, ok with parseold
57 "Ex_frees ((foldl (op &) True (mr#ars)) & \
58 \ (ALL m'. (subst (m,m') (foldl (op &) True (mr#ars))\
61 \( ALL x. lower_bound <= x & x <= upper_bound \
62 \ --> (%v. t) x <= m)"*)],
63 relate=["max_relation mr",
64 "additionalRels ars"]}: string ppc;
65 val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
67 "data --- maximum_by_differentiation ---";
68 val met = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
69 "domain {x::real. #0 <= x & x <= pi//#2}",
70 "errorBound (eps = #1//#1000)"],
72 find=["maximum A","valuesFor [a=Undef]",
73 "function_term t","max_argument mx"],
74 with_=[(* incompat.w. parse, ok with parseold
75 "EX b alpha. A = #2*a*b - a^^^#2 & \
76 \ a = #2*R*sin alpha & \
77 \ b = #2*R*cos alpha & \
78 \ (ALL A'. A'= #2*a*b - a^^^#2 & \
79 \ a = #2*R*sin alpha & \
80 \ b = #2*R*cos alpha --> A' <= A) & \
81 \ A = (%alpha. t) mx & \
82 \ (ALL x. #0 <= x & x <= pi --> \
83 \ (%alpha. t) x <= A)"*)],
84 relate=["max_relation mr",
85 "additionalRels ars"]}: string ppc;
86 val chkpbl = ((map (the o (parse thy))) o ppc2list) met;
88 val (SOME ct) = parseold thy "EX b. (EX alpha. A = #2*a*b - a^^^#2)";
90 "pbltyp --- make_fun ---";
91 (* subproblem [(hd #relate root, equality),
92 (boundVariable formalization, boundVariable),
93 (tl #relate root, equalities)] *)
94 val pbltyp = {given=["equality e","boundVariable v", "equalities es"],
96 find=["functionTerm t"],with_=[(*???*)],
97 relate=[(*???*)]}: string ppc;
98 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
100 val pbl = {given=["equality (A=#2*a*b - a^^^#2)","boundVariable alpha",
101 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"],
103 find=["functionTerm t"],
104 with_=[],relate=[]}: string ppc;
105 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
107 "met --- make_explicit_and_substitute ---";
108 val met = {given=["equality e","boundVariable v", "equalities es"],
110 find=["functionTerm t"],with_=[(*???*)],
111 relate=[(*???*)]}: string ppc;
112 val chkmet = ((map (the o (parse thy))) o ppc2list) met;
113 "met --- introduce_a_new_variable ---";
114 val met = {given=["equality e","boundVariable v", "substitutions es"],
116 find=["functionTerm t"],with_=[(*???*)],
117 relate=[(*???*)]}: string ppc;
118 val chkmet = ((map (the o (parse thy))) o ppc2list) met;
121 "pbltyp --- max_of_fun_on_interval ---";
122 val pbltyp = {given=["functionTerm t","boundVariable v",
123 "domain {x::real. lower_bound <= x & x <= upper_bound}"],
125 find=["maximums ms"],
126 with_=[(* incompat.w. parse, ok with parseold
128 \ (ALL x::real. lower_bound <= x & x <= upper_bound \
129 \ --> (%v. t) x <= m)"*)],
130 relate=[]}: string ppc;
131 val chkpbltyp = ((map (the o (parse thy))) o ppc2list) pbltyp;
133 val pbl = {given=["functionTerm (f = #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \
134 \ (#2*R*sin alpha)^^^#2)","boundVariable alpha",
135 "domain {x::real. #0 <= x & x <= pi}"],where_=[],
136 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc;
137 val chkpbl = ((map (the o (parse thy))) o ppc2list) pbl;
140 (* pbltyp --- max_of_fun --- *)
142 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc;
143 val (SOME ct) = parse thy ;
144 atomty (Thm.term_of ct);
148 (* --- 14.1.00 ev. nicht ganz up to date bzg. oberem --- *)
150 val org = {given=["[u=(#12::real)]"],where_=[],
151 find=["[a,(b::real)]"],with_=[],
152 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc;
153 val chkorg = ((map (the o (parse thy))) o ppc2list) org;
155 val org = {given=["[c=#10, h=(#4::real)]"],where_=[],
156 find=["[x,(y::real)]"],with_=[],
157 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc;
158 val chkorg = ((map (the o (parse thy))) o ppc2list) org;
160 val org = {given=["[r=#5]"],where_=[],
161 find=["[x,(y::real)]"],with_=[],
162 relate=["[is_max #0=pi*x^^^#2 + pi*x*(r::real)]"]}: string ppc;
163 val chkorg = ((map (the o (parse thy))) o ppc2list) org;
165 val org = {given=["[s=(#10::real)]"],where_=[],
166 find=["[p::real]"],with_=[],
167 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc;
168 val chkorg = ((map (the o (parse thy))) o ppc2list) org;
172 (* -------------- coil-kernel -------------- vor 19.1.00 *)
173 (* --- subproblem: make-function-by-subst ~~~~~~~~~~~ *)
174 (* --- subproblem: max-of-function *)
175 (* --- subproblem: derivative *)
176 (* --- subproblem: tan-quadrat-equation *)
177 "-------------- coil-kernel --------------";
178 val origin = ["A=#2*a*b - a^^^#2",
179 "a::real","b::real","{x. #0<x & x<R//#2}",
180 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
181 "alpha::real","{alpha::real. #0<alpha & alpha<pi//#2}",
182 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
184 (* --- for a isa-users-mail --- FIXME
185 Goal "{x. x < a} = ?z";
187 Goal "{x. x < #3} = {a}";
188 {x::'a. x < (#3::'a)} = {a}
189 Goal "{x. #3 < x} = ?z";
190 Collect (op < (#3::'a)) = ?z
191 ---------------------------- *)
193 val formals = map (the o (parse thy)) origin;
195 val given = ["formula_for_max (lhs=rhs)","boundVariable bdv",
196 "interval {x. low < x & x < high}",
197 "additional_conds ac","constants cs"];
198 val where_ = ["lhs is_const","bdv is_const","low is_const","high is_const",
199 "||| Vars equ ||| = ||| VarsSet ac ||| - ||| ac ||| + #1"];
200 val find = ["f::real => real","maxs::real set"];
201 val with_ = [(* incompat.w. parse, ok with parseold
202 "maxs = {m. low < m & m < high & \
203 \ (m is_local_max_of (%bdv. f))}"*)];
204 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
205 val givens = map (the o (parse thy)) given;
207 "------- 1.1 -------";
209 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
210 "a::real","{x. #0<x & x<R//#2}",
211 "{(a//#2)^^^#2 + (b//#2)^^^#2 = (R//#2)^^^#2}",
213 val tag__forms = chktyps thy (formals, givens);
214 map ((atomty) o Thm.term_of) tag__forms;
216 val formals = map (the o (parse thy)) ["A=#2*a*b - a^^^#2",
217 "alpha::real","{alpha. #0<alpha & alpha<pi//#2}",
218 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
220 val tag__forms = chktyps thy (formals, givens);
221 map ((atomty) o Thm.term_of) tag__forms;
224 " --- subproblem: make-function-by-subst --- ";
225 val origin = ["A=#2*a*b - a^^^#2",
226 "{a//#2 = R*(sin alpha), b//#2 = R*(cos alpha)}",
228 val formals = map (the o (parse thy)) origin;
230 val given = ["equation (lhs=rhs)","substitutions ss",
233 val find = ["t::real"];
234 val with_ = ["||| Vars t ||| = #1"];
235 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
236 val givens = map (the o (parse thy)) given;
238 val tag__forms = chktyps thy (formals, givens);
239 map ((atomty) o Thm.term_of) tag__forms;
241 " --- subproblem: max-of-function --- ";
242 val origin = ["A = #2*(#2*R*(sin alpha))*(#2*R*(sin alpha)) - \
243 \ (#2*R*(sin alpha))^^^#2",
244 "{alpha. #0<alpha & alpha<pi//#2}",
246 val formals = map (the o (parse thy)) origin;
248 val given = ["equation (lhs=rhs)",
249 "interval {x. low < x & x < high}",
251 val where_ = ["lhs is_const","low is_const","high is_const"];
252 val find = ["t::real"];
253 val with_ = ["||| Vars t ||| = #1"];
254 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
255 val givens = map (the o (parse thy)) given;
257 val tag__forms = chktyps thy (formals, givens);
258 map ((atomty) o Thm.term_of) tag__forms;
260 " --- subproblem: derivative --- ";
261 val origin = ["x^^^#3-y^^^#3+#-3*x+#12*y+#10","x::real"];
262 val formals = map (the o (parse thy)) origin;
264 val given = ["functionTerm t",
265 "boundVariable bdv"];
266 val where_ = ["bdv is_const"];
267 val find = ["t'::real"];
268 val with_ = ["t' is_derivative_of (%bdv. t)"];
269 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
270 val givens = map (the o (parse thy)) given;
272 val tag__forms = chktyps thy (formals, givens);
273 map ((atomty) o Thm.term_of) tag__forms;
275 " --- subproblem: tan-quadrat-equation --- ";
276 val origin = ["#8*R^^^#2*(cos alpha)^^^#2 + #-8*R^^^#2* \
277 \ (cos alpha)*(sin alpha) + #8*R^^^#2*(sin alpha)^^^#2 = #0",
278 "alpha::real","#1//#1000"];
279 val formals = map (the o (parse thy)) origin;
281 val given = ["equation (a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
282 \ c*(sin bdv) = #0)",
283 "boundVariable bdv","errorBound epsilon"];
284 val where_ = ["bdv is_const","epsilon is_const_expr"];
285 val find = ["L::real set"];
286 val with_ = ["L = {x. || (%bdv. a*(cos bdv)^^^#2 + b*(cos bdv)*(sin bdv) + \
287 \ c*(sin bdv)) x || < epsilon}"];
289 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
290 val givens = map (the o (parse thy)) given;
291 val tag__forms = chktyps thy (formals, givens);
292 map ((atomty) o Thm.term_of) tag__forms;
294 (* use"test-coil-kernel.sml";
298 " #################################################### ";
300 " #################################################### ";
304 ["fixedValues [R=(R::real)]",
305 "boundVariable a", "boundVariable b",
306 "boundVariable alpha",
307 "domain {x::real. #0 <= x & x <= #2*R}",
308 "domain {x::real. #0 <= x & x <= #2*R}",
309 "domain {x::real. #0 <= x & x <= pi//#2}",
310 "errorBound (eps = #1//#1000)",
311 "maximum A","valuesFor [a=Undef]",
312 (*"functionTerm t","max_argument mx",
313 "max_relation (A=#2*a*b - a^^^#2)", *)
314 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
315 "additionalRels [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
316 "additionalRels [A=#2*a*b - a^^^#2,a=#2*R*sin alpha, b=#2*R*cos alpha]"];
318 ("DiffAppl",["Script","maximum_of","function"],e_metID);
322 val pbl = {given=["fixedValues [R=(R::real)]","boundVariable alpha",
323 "domain {x::real. #0 <= x & x <= pi//#2}",
324 "errorBound (eps = #1//#1000)"],
326 find=["maximum A","valuesFor [a=Undef]"(*,
327 "functionTerm t","max_argument mx"*)],
329 relate=["max_relation (A=#2*a*b - a^^^#2)",
330 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
331 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
332 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"]
335 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
336 specify (Init_Proof (cts,(dI',pI',mI'))) e_pos' [] EmptyPtree;
338 val ct = "fixedValues [R=(R::real)]";
339 (*l(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify(Add_Given ct) p c pt*)
340 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
342 val ct = "boundVariable a";
343 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
344 val ct = "boundVariable alpha";
345 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
347 val ct = "domain {x::real. #0 <= x & x <= pi//#2}";
348 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
350 val ct = "errorBound (eps = (#1::real) // #1000)";
351 val ct = "maximum A";
352 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
354 val ct = "valuesFor [a=Undef]";
355 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
357 val ct = "max_relation ()";
358 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
360 val ct = "relations [A=#2*a*b - a^^^#2,(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]";
361 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
363 (* ... nxt = Specify_Domain ...
364 val ct = "additionalRels [b=#2*R*cos alpha]";
365 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
366 specify(Add_Relation ct) p c pt;
368 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
370 val ct = "additionalRels [a=#2*R*sin alpha]";
371 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
372 specify(Add_Relation ct) p c pt;
374 val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
377 (* --- tricky case (termlist interleaving variants):
378 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
379 specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
381 > val ct = "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2, b=#2*R*cos alpha]";
382 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
385 (* --- incomplete input ---
386 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) =
387 specify (Init_Proof (cts,(dI,pI,mI))) [] [] EmptyPtree;
389 > val ct = "[R=(R::real)]";
390 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
392 > val ct = "R=(R::real)";
393 > val(p,_,Form'(PpcKF(_,_,ppc)),nxt,_,pt) = specify nxt p c pt;
395 > val ct = "(R::real)";
396 > specify nxt p c pt;
400 " #################################################### ";
401 " test do_ specify ";
402 " #################################################### ";
405 val cts = ["fixedValues [R=(R::real)]",
406 "boundVariable a", "boundVariable b",
407 "boundVariable alpha",
408 "domain {x::real. #0 <= x & x <= #2*R}",
409 "domain {x::real. #0 <= x & x <= #2*R}",
410 "domain {x::real. #0 <= x & x <= pi//#2}",
411 "errorBound (eps=#1//#1000)",
412 "maximum A","valuesFor [a=Undef]",
413 (*"functionTerm t","max_argument mx", *)
414 "max_relation (A=#2*a*b - a^^^#2)",
415 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
416 "additionalRels [(a//#2)^^^#2 + (b//#2)^^^#2 =R^^^#2]",
417 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"];
419 ("DiffAppl",["DiffAppl","test_maximum"],e_metID);
420 val p = e_pos'; val c = [];
422 val (mI,m) = ("Init_Proof",Init_Proof (cts, (dI',pI',mI')));
423 val (pst as (sc,pt,cl):pstate) = (EmptyScr, e_ctree, []);
424 val (p,_,f,nxt,_,(_,pt,_)) = do_ (mI,m) p c pst;
425 (*val nxt = ("Add_Given",Add_Given "fixedValues [R = R]")*)
427 val (p,_,Form' (PpcKF (_,_,ppc)),nxt,_,(_,pt,_)) =
428 do_ nxt p c (EmptyScr,pt,[]);
429 (*val nxt = ("Add_Given",Add_Given "boundVariable a") *)