102 where_= [], |
102 where_= [], |
103 find = ["maximums ms"], |
103 find = ["maximums ms"], |
104 with_ = ["ALL m. m : ms --> \ |
104 with_ = ["ALL m. m : ms --> \ |
105 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
105 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
106 \ --> (%v. t) x <= m)"], |
106 \ --> (%v. t) x <= m)"], |
107 relate= []}: string ppc; |
107 relate= []}: string model; |
108 (* ':' is 'element', '::' is a type constraint *) |
108 (* ':' is 'element', '::' is a type constraint *) |
109 |
109 |
110 (* (1) variant of instantiation *) |
110 (* (1) variant of instantiation *) |
111 {given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))", |
111 {given = ["function_term (a * #2 * sqrt(R \<up> #2 - (a//#2) \<up> #2))", |
112 "bound_variable a", |
112 "bound_variable a", |
233 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"], |
233 "foldl (op &) True (map (Not o ((op <=) #0) o Rhs) cs)"], |
234 find=["maximum m", "values_for (ms::real list)"], |
234 find=["maximum m", "values_for (ms::real list)"], |
235 with_=["Ex_frees ((foldl (op &) True (r#rs)) & \ |
235 with_=["Ex_frees ((foldl (op &) True (r#rs)) & \ |
236 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \ |
236 \ (ALL m'. (subst (m,m') (foldl (op &) True (r#rs)) \ |
237 \ --> m' <= m)))"], |
237 \ --> m' <= m)))"], |
238 relate=["max_relation r", "additionalRels rs"]}:string ppc; |
238 relate=["max_relation r", "additionalRels rs"]}:string model; |
239 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp; |
239 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp; |
240 "coil"; |
240 "coil"; |
241 val org = ["fixed_values [R=(R::real)]", |
241 val org = ["fixed_values [R=(R::real)]", |
242 "bound_variable a", "bound_variable b", "bound_variable alpha", |
242 "bound_variable a", "bound_variable b", "bound_variable alpha", |
243 "domain {x::real. #0 <= x & x <= #2*R}", |
243 "domain {x::real. #0 <= x & x <= #2*R}", |
255 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \ |
255 \ a=#2*R*sin alpha & b=#2*R*cos alpha & \ |
256 \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \ |
256 \ (ALL A'. A'=#2*a*b - a \<up> #2 & a=#2*R*sin alpha & b=#2*R*cos alpha \ |
257 \ --> A' <= A)"], |
257 \ --> A' <= A)"], |
258 relate=["max_relation (A=#2*a*b - a \<up> #2)", |
258 relate=["max_relation (A=#2*a*b - a \<up> #2)", |
259 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"] |
259 "additionalRels [a=#2*R*sin alpha, b=#2*R*cos alpha]"] |
260 }: string ppc; |
260 }: string model; |
261 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl; |
261 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl; |
262 |
262 |
263 "met --- maximum_by_differentiation ---"; |
263 "met --- maximum_by_differentiation ---"; |
264 val met = {given=["fixed_values (cs::bool list)", "bound_variable v", |
264 val met = {given=["fixed_values (cs::bool list)", "bound_variable v", |
265 "domain {x::real. lower_bound <= x & x <= upper_bound}", |
265 "domain {x::real. lower_bound <= x & x <= upper_bound}", |
271 \ (ALL m'. (subst (m,m') (foldl (op &) True rs) \ |
271 \ (ALL m'. (subst (m,m') (foldl (op &) True rs) \ |
272 \ --> m' <= m))) & \ |
272 \ --> m' <= m))) & \ |
273 \m = (%v. t) mx & \ |
273 \m = (%v. t) mx & \ |
274 \( ALL x. lower_bound <= x & x <= upper_bound \ |
274 \( ALL x. lower_bound <= x & x <= upper_bound \ |
275 \ --> (%v. t) x <= m)"], |
275 \ --> (%v. t) x <= m)"], |
276 relate=["rs::bool list"]}: string ppc; |
276 relate=["rs::bool list"]}: string model; |
277 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met; |
277 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) met; |
278 |
278 |
279 |
279 |
280 "pbltyp --- make_fun ---"; |
280 "pbltyp --- make_fun ---"; |
281 (* subproblem [(hd #relate root, equality), |
281 (* subproblem [(hd #relate root, equality), |
282 (bound_variable formalization, bound_variable), |
282 (bound_variable formalization, bound_variable), |
283 (tl #relate root, equalities)] *) |
283 (tl #relate root, equalities)] *) |
284 val pbltyp = {given=["equality e", "bound_variable v", "equalities es"], |
284 val pbltyp = {given=["equality e", "bound_variable v", "equalities es"], |
285 where_=[], |
285 where_=[], |
286 find=["function_term t"],with_=[(*???*)], |
286 find=["function_term t"],with_=[(*???*)], |
287 relate=[(*???*)]}: string ppc; |
287 relate=[(*???*)]}: string model; |
288 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp; |
288 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp; |
289 "coil"; |
289 "coil"; |
290 val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha", |
290 val pbl = {given=["equality (A=#2*a*b - a \<up> #2)", "bound_variable alpha", |
291 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"], |
291 "equalities [a=#2*R*sin alpha, b=#2*R*cos alpha]"], |
292 where_=[], |
292 where_=[], |
293 find=["function_term t"], |
293 find=["function_term t"], |
294 with_=[],relate=[]}: string ppc; |
294 with_=[],relate=[]}: string model; |
295 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl; |
295 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl; |
296 |
296 |
297 "met --- make_explicit_and_substitute ---"; |
297 "met --- make_explicit_and_substitute ---"; |
298 val met = {given=["equality e", "bound_variable v", "equalities es"], |
298 val met = {given=["equality e", "bound_variable v", "equalities es"], |
299 where_=[], |
299 where_=[], |
300 find=["function_term t"],with_=[(*???*)], |
300 find=["function_term t"],with_=[(*???*)], |
301 relate=[(*???*)]}: string ppc; |
301 relate=[(*???*)]}: string model; |
302 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met; |
302 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met; |
303 "met --- introduce_a_new_variable ---"; |
303 "met --- introduce_a_new_variable ---"; |
304 val met = {given=["equality e", "bound_variable v", "substitutions es"], |
304 val met = {given=["equality e", "bound_variable v", "substitutions es"], |
305 where_=[], |
305 where_=[], |
306 find=["function_term t"],with_=[(*???*)], |
306 find=["function_term t"],with_=[(*???*)], |
307 relate=[(*???*)]}: string ppc; |
307 relate=[(*???*)]}: string model; |
308 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met; |
308 val chkmet = ((map (the o (parse thy))) o P_Model.to_list) met; |
309 |
309 |
310 |
310 |
311 "pbltyp --- max_of_fun_on_interval ---"; |
311 "pbltyp --- max_of_fun_on_interval ---"; |
312 val pbltyp = {given=["function_term t", "bound_variable v", |
312 val pbltyp = {given=["function_term t", "bound_variable v", |
314 where_=[], |
314 where_=[], |
315 find=["maximums ms"], |
315 find=["maximums ms"], |
316 with_=["ALL m. m : ms --> \ |
316 with_=["ALL m. m : ms --> \ |
317 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
317 \ (ALL x::real. lower_bound <= x & x <= upper_bound \ |
318 \ --> (%v. t) x <= m)"], |
318 \ --> (%v. t) x <= m)"], |
319 relate=[]}: string ppc; |
319 relate=[]}: string model; |
320 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp; |
320 val chkpbltyp = ((map (the o (parse thy))) o P_Model.to_list) pbltyp; |
321 "coil"; |
321 "coil"; |
322 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \ |
322 val pbl = {given=["function_term #2*(#2*R*sin alpha)*(#2*R*cos alpha) - \ |
323 \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha", |
323 \ (#2*R*sin alpha) \<up> #2", "bound_variable alpha", |
324 "domain {x::real. #0 <= x & x <= pi}"],where_=[], |
324 "domain {x::real. #0 <= x & x <= pi}"],where_=[], |
325 find=["maximums [#1234]"],with_=[],relate=[]}: string ppc; |
325 find=["maximums [#1234]"],with_=[],relate=[]}: string model; |
326 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl; |
326 val chkpbl = ((map (the o (parse thy))) o P_Model.to_list) pbl; |
327 |
327 |
328 |
328 |
329 (* pbltyp --- max_of_fun --- *) |
329 (* pbltyp --- max_of_fun --- *) |
330 (* |
330 (* |
331 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
331 {given=[],where_=[],find=[],with_=[],relate=[]}: string model; |
332 val (SOME ct) = parse thy ; |
332 val (SOME ct) = parse thy ; |
333 atomty thy (Thm.term_of ct); |
333 atomty thy (Thm.term_of ct); |
334 *) |
334 *) |
335 |
335 |
336 |
336 |
342 |
342 |
343 (* --- 14.1.00 --- *) |
343 (* --- 14.1.00 --- *) |
344 "p.114"; |
344 "p.114"; |
345 val org = {given=["[u=(#12::real)]"],where_=[], |
345 val org = {given=["[u=(#12::real)]"],where_=[], |
346 find=["[a,(b::real)]"],with_=[], |
346 find=["[a,(b::real)]"],with_=[], |
347 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string ppc; |
347 relate=["[is_max A=a*(b::real), #2*a+#2*b=(u::real)]"]}: string model; |
348 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
348 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
349 "p.116"; |
349 "p.116"; |
350 val org = {given=["[c=#10, h=(#4::real)]"],where_=[], |
350 val org = {given=["[c=#10, h=(#4::real)]"],where_=[], |
351 find=["[x,(y::real)]"],with_=[], |
351 find=["[x,(y::real)]"],with_=[], |
352 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string ppc; |
352 relate=["[A=x*(y::real), c//h=x//(h-(y::real))]"]}: string model; |
353 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
353 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
354 "p.117"; |
354 "p.117"; |
355 val org = {given=["[r=#5]"],where_=[], |
355 val org = {given=["[r=#5]"],where_=[], |
356 find=["[x,(y::real)]"],with_=[], |
356 find=["[x,(y::real)]"],with_=[], |
357 relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string ppc; |
357 relate=["[is_max #0=pi*x \<up> #2 + pi*x*(r::real)]"]}: string model; |
358 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
358 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
359 "#241"; |
359 "#241"; |
360 val org = {given=["[s=(#10::real)]"],where_=[], |
360 val org = {given=["[s=(#10::real)]"],where_=[], |
361 find=["[p::real]"],with_=[], |
361 find=["[p::real]"],with_=[], |
362 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string ppc; |
362 relate=["[is_max p=n*m, s=n+(m::real)]"]}: string model; |
363 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
363 val chkorg = ((map (the o (parse thy))) o P_Model.to_list) org; |
364 |
364 |
365 (* |
365 (* |
366 {given=[],where_=[],find=[],with_=[],relate=[]}: string ppc; |
366 {given=[],where_=[],find=[],with_=[],relate=[]}: string model; |
367 val (SOME ct) = parse thy ; |
367 val (SOME ct) = parse thy ; |
368 atomty thy (Thm.term_of ct); |
368 atomty thy (Thm.term_of ct); |
369 *) |
369 *) |