|
1 (* tests on me.sml |
|
2 author: Walther Neuper |
|
3 060225, |
|
4 (c) due to copyright terms |
|
5 |
|
6 use"../smltest/ME/me.sml"; |
|
7 use"me.sml"; |
|
8 *) |
|
9 |
|
10 "-----------------------------------------------------------------"; |
|
11 "table of contents -----------------------------------------------"; |
|
12 "-----------------------------------------------------------------"; |
|
13 "=====new ptree 1: crippled by cut_level_'_ ======================"; |
|
14 "-------------- get_interval from ctree with move_dn:modspec.sml -"; |
|
15 "=====new ptree 2 without changes ================================"; |
|
16 "-------------- getFormulaeFromTo --------------------------------"; |
|
17 "autoCalculate"; |
|
18 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
|
19 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
|
20 "--------- maximum-example: complete_metitms ---------------------"; |
|
21 "--------- maximum-example: complete_mod -------------------------"; |
|
22 "-----------------------------------------------------------------"; |
|
23 "-----------------------------------------------------------------"; |
|
24 "-----------------------------------------------------------------"; |
|
25 |
|
26 |
|
27 |
|
28 "=====new ptree 1: crippled by cut_level_'_ ======================"; |
|
29 "=====new ptree 1: crippled by cut_level_'_ ======================"; |
|
30 "=====new ptree 1: crippled by cut_level_'_ ======================"; |
|
31 states:=[]; |
|
32 CalcTree |
|
33 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
|
34 "solveFor x","solutions L"], |
|
35 ("RatEq.thy",["univariate","equation"],["no_met"]))]; |
|
36 Iterator 1; moveActiveRoot 1; |
|
37 autoCalculate 1 CompleteCalc; |
|
38 |
|
39 getTactic 1 ([1],Res);(*Rewrite_Set RatEq_simplify*) |
|
40 getTactic 1 ([2],Res);(*Rewrite_Set norm_Rational*) |
|
41 getTactic 1 ([3],Res);(*Rewrite_Set RatEq_eliminate*) |
|
42 getTactic 1 ([4,1],Res);(*Rewrite all_left*) |
|
43 getTactic 1 ([4,2],Res);(*Rewrite_Set expand_binoms*) |
|
44 getTactic 1 ([4,3],Res);(*Rewrite_Set_Inst make_ratpoly_in*) |
|
45 |
|
46 moveActiveFormula 1 ([1],Res)(*1.1...1.4*); |
|
47 moveActiveFormula 1 ([2],Res)(**ME_Isa: 'expand' not known*); |
|
48 moveActiveFormula 1 ([3],Res)(*3.1.*); |
|
49 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*); |
|
50 moveActiveFormula 1 ([4,3],Res)(**one_scr_arg: called by Script Stepwise t_=*); |
|
51 |
|
52 moveActiveFormula 1 ([1],Res)(*1.1...1.4*); |
|
53 interSteps 1 ([1],Res)(*..is activeFormula !?!*); |
|
54 |
|
55 getTactic 1 ([1,1],Res);(*Rewrite real_diff_minus*) |
|
56 getTactic 1 ([1,2],Res);(*Rewrite real_diff_minus*) |
|
57 getTactic 1 ([1,3],Res);(*Rewrite real_diff_minus*) |
|
58 getTactic 1 ([1,4],Res);(*Rewrite real_rat_mult_1*) |
|
59 |
|
60 moveActiveFormula 1 ([4,2],Res)(*4.2.1.*); |
|
61 interSteps 1 ([4,2],Res)(*..is activeFormula !?!*); |
|
62 val ((pt,_),_) = get_calc 1; |
|
63 writeln(pr_ptree pr_short pt); |
|
64 (*delete [4,1] in order to make pos [4],[4,4] for pblobjs differen [4],[4,3]: |
|
65 ###########################################################################*) |
|
66 val (pt, _) = cut_level_'_ [] [] pt ([4,1],Frm); (*#*) |
|
67 (*##########################################################################*) |
|
68 writeln(pr_ptree pr_short pt); |
|
69 (*########################################################################## |
|
70 attention: the ctree in states is still the old (perfect) !!! |
|
71 ############################################################################*) |
|
72 |
|
73 |
|
74 |
|
75 "-------------- get_interval from ctree with move_dn:modspec.sml -"; |
|
76 "-------------- get_interval from ctree with move_dn:modspec.sml -"; |
|
77 "-------------- get_interval from ctree with move_dn:modspec.sml -"; |
|
78 writeln(pr_ptree pr_short pt); |
|
79 writeln(posterms2str (get_interval ([],Frm) ([],Res) 99999 pt)); |
|
80 |
|
81 case map fst (get_interval ([],Frm) ([],Res) 99999 pt) of |
|
82 [([], Frm), |
|
83 ([1], Frm), |
|
84 ([1, 1], Frm), |
|
85 ([1, 1], Res), |
|
86 ([1, 2], Res), |
|
87 ([1, 3], Res), |
|
88 ([1, 4], Res), |
|
89 ([1], Res), |
|
90 ([2], Res), |
|
91 ([3], Res), |
|
92 ([4], Pbl), |
|
93 ([4, 1], Frm), |
|
94 ([4, 1, 1], Frm), |
|
95 ([4, 1, 1], Res), |
|
96 ([4, 1], Res), |
|
97 ([4, 2], Res), |
|
98 ([4, 3], Pbl), |
|
99 ([4, 3, 1], Frm), |
|
100 ([4, 3, 1], Res), |
|
101 ([4, 3, 2], Res), |
|
102 ([4, 3, 3], Res), |
|
103 ([4, 3, 4], Res), |
|
104 ([4, 3, 5], Res), |
|
105 ([4, 3], Res), |
|
106 ([4], Res), |
|
107 ([5], Res), |
|
108 ([], Res)] => () |
|
109 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f"; |
|
110 case map fst (get_interval ([],Frm) ([],Res) 1 pt) of |
|
111 [([], Frm), |
|
112 ([1], Frm), |
|
113 ([1], Res), |
|
114 ([2], Res), |
|
115 ([3], Res), |
|
116 ([4], Pbl), |
|
117 ([4], Res), |
|
118 ([5], Res), |
|
119 ([], Res)] => () |
|
120 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f"; |
|
121 case map fst (get_interval ([],Frm) ([],Res) 0 pt) of |
|
122 [([], Frm), |
|
123 ([], Res)] => () |
|
124 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1f"; |
|
125 |
|
126 case map fst (get_interval ([1,3],Res) ([4,1,1],Frm) 99999 pt) of |
|
127 [([1, 3], Res), |
|
128 ([1, 4], Res), |
|
129 ([1], Res), |
|
130 ([2], Res), |
|
131 ([3], Res), |
|
132 ([4], Pbl), |
|
133 ([4, 1], Frm), |
|
134 ([4, 1, 1], Frm)] => () |
|
135 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1a"; |
|
136 |
|
137 (*this pos' is not generated bu move_dn:......vvv: goes to end of calc*) |
|
138 case map fst (get_interval ([2],Res) ([4,3,2],Frm) 99999 pt) of |
|
139 [([2], Res), |
|
140 ([3], Res), |
|
141 ([4], Pbl), |
|
142 ([4, 1], Frm), |
|
143 ([4, 1, 1], Frm), |
|
144 ([4, 1, 1], Res), |
|
145 ([4, 1], Res), |
|
146 ([4, 2], Res), |
|
147 ([4, 3], Pbl), |
|
148 ([4, 3, 1], Frm), |
|
149 ([4, 3, 1], Res), |
|
150 ([4, 3, 2], Res), |
|
151 ([4, 3, 3], Res),(*this is beyond 'to'*) |
|
152 ([4, 3, 4], Res),(*this is beyond 'to'*) |
|
153 ([4, 3, 5], Res),(*this is beyond 'to'*) |
|
154 ([4, 3], Res), (*this is beyond 'to'*) |
|
155 ([4], Res), (*this is beyond 'to'*) |
|
156 ([5], Res), (*this is beyond 'to'*) |
|
157 ([], Res)] => () (*this is beyond 'to'*) |
|
158 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1b"; |
|
159 case map fst (get_interval ([1,4],Res) ([4,3,1],Frm) 99999 pt) of |
|
160 [([1, 4], Res), |
|
161 ([1], Res), |
|
162 ([2], Res), |
|
163 ([3], Res), |
|
164 ([4], Pbl), |
|
165 ([4, 1], Frm), |
|
166 ([4, 1, 1], Frm), |
|
167 ([4, 1, 1], Res), |
|
168 ([4, 1], Res), |
|
169 ([4, 2], Res), |
|
170 ([4, 3], Pbl), |
|
171 ([4, 3, 1], Frm)] => () |
|
172 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1c"; |
|
173 case map fst (get_interval ([4,2],Res) ([5],Res) 99999 pt) of |
|
174 [([4, 2], Res), |
|
175 ([4, 3], Pbl), |
|
176 ([4, 3, 1], Frm), |
|
177 ([4, 3, 1], Res), |
|
178 ([4, 3, 2], Res), |
|
179 ([4, 3, 3], Res), |
|
180 ([4, 3, 4], Res), |
|
181 ([4, 3, 5], Res), |
|
182 ([4, 3], Res), |
|
183 ([4], Res), |
|
184 ([5], Res)]=>() |
|
185 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1d"; |
|
186 case map fst (get_interval ([],Frm) ([4,3,2],Res) 99999 pt) of |
|
187 [([], Frm), |
|
188 ([1], Frm), |
|
189 ([1, 1], Frm), |
|
190 ([1, 1], Res), |
|
191 ([1, 2], Res), |
|
192 ([1, 3], Res), |
|
193 ([1, 4], Res), |
|
194 ([1], Res), |
|
195 ([2], Res), |
|
196 ([3], Res), |
|
197 ([4], Pbl), |
|
198 ([4, 1], Frm), |
|
199 ([4, 1, 1], Frm), |
|
200 ([4, 1, 1], Res), |
|
201 ([4, 1], Res), |
|
202 ([4, 2], Res), |
|
203 ([4, 3], Pbl), |
|
204 ([4, 3, 1], Frm), |
|
205 ([4, 3, 1], Res), |
|
206 ([4, 3, 2], Res)] => () |
|
207 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1e"; |
|
208 case map fst (get_interval ([4,3],Frm) ([4,3],Res) 99999 pt) of |
|
209 [([4, 3], Frm), |
|
210 ([4, 3, 1], Frm), |
|
211 ([4, 3, 1], Res), |
|
212 ([4, 3, 2], Res), |
|
213 ([4, 3, 3], Res), |
|
214 ([4, 3, 4], Res), |
|
215 ([4, 3, 5], Res), |
|
216 ([4, 3], Res)] => () |
|
217 | _ => raise error "diff.behav.in ctree.sml: get_interval lev 1g"; |
|
218 |
|
219 |
|
220 |
|
221 |
|
222 "=====new ptree 2 without changes ================================"; |
|
223 "=====new ptree 2 without changes ================================"; |
|
224 "=====new ptree 2 without changes ================================"; |
|
225 states:=[]; |
|
226 CalcTree |
|
227 [(["equality (x/(x^2 - 6*x+9) - 1/(x^2 - 3*x) =1/x)", |
|
228 "solveFor x","solutions L"], |
|
229 ("RatEq.thy",["univariate","equation"],["no_met"]))]; |
|
230 Iterator 1; moveActiveRoot 1; |
|
231 autoCalculate 1 CompleteCalc; |
|
232 val ((pt,_),_) = get_calc 1; |
|
233 writeln(pr_ptree pr_short pt); |
|
234 |
|
235 |
|
236 "-------------- getFormulaeFromTo --------------------------------"; |
|
237 "-------------- getFormulaeFromTo --------------------------------"; |
|
238 "-------------- getFormulaeFromTo --------------------------------"; |
|
239 getFormulaeFromTo 1 ([4, 2], Res) ([4, 4], Pbl) 000; |
|
240 (* |
|
241 "@@@@@begin@@@@@" //................................................... |
|
242 + " 1" //.............................................................. |
|
243 + "<GETELEMENTSFROMTO>" //................................................... |
|
244 + " <CALCID> 1 </CALCID>" //.......................................... |
|
245 + " <POSFORMHEADS>" //................................................ |
|
246 + " <POSFORM>" //................................................... |
|
247 + " <GENERATED>" //............................................... |
|
248 + " <INTLIST>" //............................................... |
|
249 + " <INT> 4 </INT>" //........................................ |
|
250 + " <INT> 3 </INT>" //........................................ |
|
251 + " </INTLIST>" //.............................................. |
|
252 + " <POS> Res </POS>" //........................................ |
|
253 + " </GENERATED>" //.............................................. |
|
254 + " <FORMULA>" //................................................. |
|
255 + " <MATHML>" //................................................ |
|
256 + " <ISA> -6 * x + 5 * x ^^^ 2 = 0 </ISA>" //................. |
|
257 + " </MATHML>" //............................................... |
|
258 + " </FORMULA>" //................................................ |
|
259 + " </POSFORM>" //.................................................. |
|
260 + " <POSHEAD>" //................................................... |
|
261 + " <GENERATED>" //............................................... |
|
262 + " <INTLIST>" //............................................... |
|
263 + " <INT> 4 </INT>" //........................................ |
|
264 + " <INT> 4 </INT>" //........................................ |
|
265 + " </INTLIST>" //.............................................. |
|
266 + " <POS> Pbl </POS>" //........................................ |
|
267 + " </GENERATED>" //.............................................. |
|
268 + " <CALCHEAD status = "correct">" //............................. |
|
269 + " <HEAD>" //................................................... |
|
270 + " <MATHML>" //............................................... |
|
271 + " <ISA> solve (-6 * x + 5 * x ^^^ 2 = 0, x) </ISA>" //..... |
|
272 + " </MATHML>" //.............................................. |
|
273 + " </HEAD>" //.................................................. |
|
274 + " <MODEL>" //................................................. |
|
275 + " <GIVEN>" //............................................... |
|
276 + " <ITEM status="correct">" //............................. |
|
277 + " <MATHML>" //.......................................... |
|
278 + " <ISA> equality (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" // |
|
279 + " </MATHML>" //......................................... |
|
280 + " </ITEM>" //............................................. |
|
281 + " <ITEM status="correct">" //............................. |
|
282 + " <MATHML>" //.......................................... |
|
283 + " <ISA> solveFor x </ISA>" //......................... |
|
284 + " </MATHML>" //......................................... |
|
285 + " </ITEM>" //............................................. |
|
286 + " </GIVEN>" //.............................................. |
|
287 + " <WHERE>" //............................................... |
|
288 + " <ITEM status="correct">" //............................. |
|
289 + " <MATHML>" //.......................................... |
|
290 + " <ISA> matches (?a * ?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" |
|
291 + "matches (?v_ + ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //...... |
|
292 + "matches (?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" |
|
293 + "matches (?a * ?v_ + ?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" |
|
294 + "matches (?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) |" //............ |
|
295 + "matches (?b * ?v_ ^^^ 2 = 0) (-6 * x + 5 * x ^^^ 2 = 0) </ISA>" //.. |
|
296 + " </MATHML>" //......................................... |
|
297 + " </ITEM>" //............................................. |
|
298 + " </WHERE>" //.............................................. |
|
299 + " <FIND>" //................................................ |
|
300 + " <ITEM status="correct">" //............................. |
|
301 + " <MATHML>" //.......................................... |
|
302 + " <ISA> solutions x_i </ISA>" //...................... |
|
303 + " </MATHML>" //......................................... |
|
304 + " </ITEM>" //............................................. |
|
305 + " </FIND>" //............................................... |
|
306 + " <RELATE> </RELATE>" //................................... |
|
307 + " </MODEL>" //................................................ |
|
308 + " <BELONGSTO> Pbl </BELONGSTO>" //............................ |
|
309 + " <SPECIFICATION>" //......................................... |
|
310 + " <THEORYID> PolyEq.thy </THEORYID>" //..................... |
|
311 + " <PROBLEMID>" //........................................... |
|
312 + " <STRINGLIST>" //........................................ |
|
313 + " <STRING> bdv_only </STRING>" //....................... |
|
314 + " <STRING> degree_2 </STRING>" //....................... |
|
315 + " <STRING> polynomial </STRING>" //..................... |
|
316 + " <STRING> univariate </STRING>" //..................... |
|
317 + " <STRING> equation </STRING>" //....................... |
|
318 + " </STRINGLIST>" //....................................... |
|
319 + " </PROBLEMID>" //.......................................... |
|
320 + " <METHODID>" //............................................ |
|
321 + " <STRINGLIST>" //........................................ |
|
322 + " <STRING> PolyEq </STRING>" //......................... |
|
323 + " <STRING> solve_d2_polyeq_bdvonly_equation </STRING>" |
|
324 + " </STRINGLIST>" //....................................... |
|
325 + " </METHODID>" //........................................... |
|
326 + " </SPECIFICATION>" //........................................ |
|
327 + " </CALCHEAD>" //............................................... |
|
328 + " </POSHEAD>" //.................................................. |
|
329 + " <POSFORMHEADS>" //................................................ |
|
330 + "</GETELEMENTSFROMTO>" //.................................................. |
|
331 + "@@@@@end@@@@@" |
|
332 *) |
|
333 |
|
334 |
|
335 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
|
336 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
|
337 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---"; |
|
338 val c = []; |
|
339 val (p,_,f,nxt,_,pt) = CalcTreeTEST |
|
340 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], |
|
341 ("Test.thy", |
|
342 ["linear","univariate","equation","test"], |
|
343 ["Test","solve_linear"]))]; |
|
344 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
345 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
346 (*xt = Add_Given "solveFor x"*) |
|
347 writeln (itms2str thy (get_obj g_pbl pt (fst p))); |
|
348 (*[ |
|
349 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])), |
|
350 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])), |
|
351 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*) |
|
352 val (pt,p) = complete_mod (pt, p); |
|
353 if itms2str thy (get_obj g_pbl pt (fst p)) = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" then () |
|
354 else raise error "completetest.sml: new behav. in complete_mod 1"; |
|
355 writeln (itms2str thy (get_obj g_pbl pt (fst p))); |
|
356 (*[ |
|
357 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), |
|
358 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), |
|
359 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) |
|
360 val mits = get_obj g_met pt (fst p); |
|
361 if itms2str thy mits = "[\n(1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),\n(2 ,[1] ,true ,#Given ,Cor solveFor x ,(v_, [x])),\n(3 ,[1] ,true ,#Find ,Cor solutions L ,(v_i_, [L]))]" |
|
362 then () else raise error "completetest.sml: new behav. in complete_mod 2"; |
|
363 writeln (itms2str thy mits); |
|
364 (*[ |
|
365 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])), |
|
366 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])), |
|
367 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*) |
|
368 |
|
369 |
|
370 |
|
371 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
|
372 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
|
373 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-"; |
|
374 states:=[]; |
|
375 CalcTree (*start of calculation, return No.1*) |
|
376 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"], |
|
377 ("Test.thy", |
|
378 ["linear","univariate","equation","test"], |
|
379 ["Test","solve_linear"]))]; |
|
380 Iterator 1; moveActiveRoot 1; |
|
381 |
|
382 (* |
|
383 autoCalculate 1 CompleteCalcHead; |
|
384 autoCalculate 1 (Step 1); |
|
385 refFormula 1 (get_pos 1 1); |
|
386 |
|
387 ... works |
|
388 |
|
389 autoCalculate 1 CompleteCalcHead; |
|
390 fetchProposedTactic 1; (*-> Apply_Method*); |
|
391 setNextTactic 1 (Apply_Method ["Test","solve_linear"]); |
|
392 autoCalculate 1 (Step 1); |
|
393 refFormula 1 (get_pos 1 1); |
|
394 |
|
395 ... works *) |
|
396 |
|
397 autoCalculate 1 (Step 1); |
|
398 refFormula 1 (get_pos 1 1); |
|
399 |
|
400 autoCalculate 1 CompleteModel; |
|
401 refFormula 1 (get_pos 1 1); |
|
402 |
|
403 autoCalculate 1 CompleteCalcHead; |
|
404 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*) |
|
405 |
|
406 |
|
407 |
|
408 "--------- maximum-example: complete_metitms ---------------------"; |
|
409 "--------- maximum-example: complete_metitms ---------------------"; |
|
410 "--------- maximum-example: complete_metitms ---------------------"; |
|
411 val (p,_,f,nxt,_,pt) = |
|
412 CalcTreeTEST |
|
413 [(["fixedValues [r=Arbfix]","maximum A", |
|
414 "valuesFor [a,b]", |
|
415 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
416 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
417 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", |
|
418 |
|
419 "boundVariable a","boundVariable b","boundVariable alpha", |
|
420 "interval {x::real. 0 <= x & x <= 2*r}", |
|
421 "interval {x::real. 0 <= x & x <= 2*r}", |
|
422 "interval {x::real. 0 <= x & x <= pi}", |
|
423 "errorBound (eps=(0::real))"], |
|
424 ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"]) |
|
425 )]; |
|
426 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
427 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
428 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
429 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
430 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e; |
|
431 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
432 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
433 (*nxt = Specify_Theory "DiffApp.thy"*) |
|
434 val (oris, _, _) = get_obj g_origin pt (fst p); |
|
435 writeln (oris2str oris); |
|
436 (*[ |
|
437 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]), |
|
438 (2, ["1","2","3"], #Find,maximum, ["A"]), |
|
439 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]), |
|
440 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]), |
|
441 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]), |
|
442 (6, ["1"], #undef,boundVariable, ["a"]), |
|
443 (7, ["2"], #undef,boundVariable, ["b"]), |
|
444 (8, ["3"], #undef,boundVariable, ["alpha"]), |
|
445 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]), |
|
446 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]), |
|
447 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*) |
|
448 val pits = get_obj g_pbl pt (fst p); |
|
449 writeln (itms2str thy pits); |
|
450 (*[ |
|
451 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])), |
|
452 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])), |
|
453 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])), |
|
454 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ |
|
455 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*) |
|
456 val mits = get_obj g_met pt (fst p); |
|
457 val mits = complete_metitms oris pits [] |
|
458 ((#ppc o get_met) ["DiffApp","max_by_calculus"]); |
|
459 writeln (itms2str thy mits); |
|
460 (*[ |
|
461 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
|
462 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), |
|
463 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])), |
|
464 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ |
|
465 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])), |
|
466 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])), |
|
467 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. |
|
468 0 <= x & x <= 2 * r}])), |
|
469 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) |
|
470 if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" then () |
|
471 else raise error "completetest.sml: new behav. in complete_metitms 1"; |
|
472 |
|
473 |
|
474 "--------- maximum-example: complete_mod -------------------------"; |
|
475 "--------- maximum-example: complete_mod -------------------------"; |
|
476 "--------- maximum-example: complete_mod -------------------------"; |
|
477 val (p,_,f,nxt,_,pt) = |
|
478 CalcTreeTEST |
|
479 [(["fixedValues [r=Arbfix]","maximum A", |
|
480 "valuesFor [a,b]", |
|
481 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
482 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]", |
|
483 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]", |
|
484 |
|
485 "boundVariable a","boundVariable b","boundVariable alpha", |
|
486 "interval {x::real. 0 <= x & x <= 2*r}", |
|
487 "interval {x::real. 0 <= x & x <= 2*r}", |
|
488 "interval {x::real. 0 <= x & x <= pi}", |
|
489 "errorBound (eps=(0::real))"], |
|
490 ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"]) |
|
491 )]; |
|
492 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
493 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
494 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
495 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*) |
|
496 val pits = get_obj g_pbl pt (fst p); |
|
497 writeln (itms2str thy pits); |
|
498 (*[ |
|
499 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])), |
|
500 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])), |
|
501 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
|
502 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*) |
|
503 val (pt,p) = complete_mod (pt,p); |
|
504 val pits = get_obj g_pbl pt (fst p); |
|
505 if itms2str thy pits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]" |
|
506 then () else raise error "completetest.sml: new behav. in complete_mod 3"; |
|
507 writeln (itms2str thy pits); |
|
508 (*[ |
|
509 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
|
510 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), |
|
511 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])), |
|
512 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ |
|
513 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*) |
|
514 val mits = get_obj g_met pt (fst p); |
|
515 if itms2str thy mits = "[\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),\n(3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a],[b]])),\n(4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2] ,(rs_, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),\n(6 ,[1] ,true ,#undef ,Cor boundVariable a ,(v_, [a])),\n(9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(itv_, [{x. 0 <= x & x <= 2 * r}])),\n(11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(err_, [eps = 0]))]" |
|
516 then () else raise error "completetest.sml: new behav. in complete_mod 3"; |
|
517 writeln (itms2str thy mits); |
|
518 (*[ |
|
519 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])), |
|
520 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])), |
|
521 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])), |
|
522 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ |
|
523 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])), |
|
524 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])), |
|
525 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x. |
|
526 0 <= x & x <= 2 * r}])), |
|
527 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*) |
|
528 |