327 = Step.specify_do_next ptp; |
327 = Step.specify_do_next ptp; |
328 val ("ok", ([(Specify_Method ["Diff_App", "max_by_calculus"], _, _)], _, ptp)) |
328 val ("ok", ([(Specify_Method ["Diff_App", "max_by_calculus"], _, _)], _, ptp)) |
329 = Step.specify_do_next ptp; |
329 = Step.specify_do_next ptp; |
330 |
330 |
331 (*** stepwise Specification: MethodC model ================================================ ***) |
331 (*** stepwise Specification: MethodC model ================================================ ***) |
332 val ("ok", ([(Add_Given "boundVariable a", _, _)], _, ptp)) |
332 val ("ok", ([(Add_Given "boundVariable b", _, _)], _, ptp)) |
333 = Step.specify_do_next ptp; |
333 = Step.specify_do_next ptp; |
334 val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp)) |
334 val ("ok", ([(Add_Given "interval {x. 0 \<le> x \<and> x \<le> 2 * r}", _, _)], _, ptp)) |
335 = Step.specify_do_next ptp; |
335 = Step.specify_do_next ptp; |
336 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp)) |
336 val ("ok", ([(Add_Given "errorBound (eps = 0)", _, _)], _, ptp)) |
337 = Step.specify_do_next ptp; |
337 = Step.specify_do_next ptp; |
338 |
338 |
339 val PblObj {meth, ...} = get_obj I (fst ptp) []; |
339 val PblObj {meth, ...} = get_obj I (fst ptp) []; |
340 if I_Model.to_string @{context} meth = "[\n" ^ |
340 |
341 "(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n" ^ |
341 (*+*)val "[\n(1 ,[1, 2, 3] ,true ,#Given ,Cor fixedValues [r = Arbfix] , pen2str), \n(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n(7 ,[2] ,true ,#Given ,Cor boundVariable b , pen2str), \n(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) , pen2str)]" |
342 "(2 ,[1, 2, 3] ,true ,#Find ,Cor maximum A , pen2str), \n" ^ |
342 = meth |> I_Model.to_string @{context} |
343 "(3 ,[1, 2, 3] ,true ,#Find ,Cor valuesFor [a, b] , pen2str), \n" ^ |
343 |
344 "(4 ,[1, 2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) \<up> 2 + (b / 2) \<up> 2 = r \<up> 2] , pen2str), \n" ^ |
|
345 "(6 ,[1] ,true ,#Given ,Cor boundVariable a , pen2str), \n" ^ |
|
346 "(9 ,[1, 2] ,true ,#Given ,Cor interval {x. 0 \<le> x \<and> x \<le> 2 * r} , pen2str), \n" ^ |
|
347 "(11 ,[1, 2, 3] ,true ,#Given ,Cor errorBound (eps = 0) , pen2str)]" |
|
348 then () else error "I_Model.to_string meth CHANGED"; |
|
349 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***) |
344 (*** Specification of Problem and MethodC model is complete, Solution starts ============== ***) |
350 |
345 |
351 (* Step.specify_do_next ptp; |
346 (* Step.specify_do_next ptp; |
352 ERROR |
347 ERROR |
353 ---------------------------------------------------------------------- |
348 ---------------------------------------------------------------------- |