1 (* use"systest/auto-inform.sml";
6 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
7 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
8 "--------- maximum-example: complete_metitms ---------------------";
9 "--------- maximum-example: complete_mod -------------------------";
10 "appendForm with miniscript with mini-subpbl:";
11 "--------- appendFormula: on Res + equ_nrls ----------------------";
12 "--------- appendFormula: on Frm + equ_nrls ----------------------";
13 "--------- appendFormula: on Res + NO deriv ----------------------";
14 "--------- appendFormula: on Res + late deriv --------------------";
15 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
16 "replaceForm with miniscript with mini-subpbl:";
17 "--------- replaceFormula: on Res + = ----------------------------";
18 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
19 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
20 "--------- replaceFormula: cut calculation -----------------------";
25 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
26 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
27 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteModel ---";
29 val (p,_,f,nxt,_,pt) = CalcTreeTEST
30 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
32 ["linear","univariate","equation","test"],
33 ["Test","solve_linear"]))];
34 val (p,_,f,nxt,_,pt) = me nxt p c pt;
35 val (p,_,f,nxt,_,pt) = me nxt p c pt;
36 (*xt = Add_Given "solveFor x"*)
37 writeln (itms2str thy (get_obj g_pbl pt (fst p)));
39 (0 ,[] ,false ,#Given ,Inc solveFor ,(??.empty, [])),
40 (0 ,[] ,false ,#Find ,Inc solutions [] ,(??.empty, [])),
41 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0]))]*)
42 val (pt,p) = complete_mod (pt, p);
43 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 ()
44 else raise error "completetest.sml: new behav. in complete_mod 1";
45 writeln (itms2str thy (get_obj g_pbl pt (fst p)));
47 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
48 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
49 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
50 val mits = get_obj g_met pt (fst p);
51 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]))]"
52 then () else raise error "completetest.sml: new behav. in complete_mod 2";
53 writeln (itms2str thy mits);
55 (1 ,[1] ,true ,#Given ,Cor equality (1 + -1 * 2 + x = 0) ,(e_, [1 + -1 * 2 + x = 0])),
56 (2 ,[1] ,true ,#Given ,Cor solveFor x ,(solveFor, [x])),
57 (3 ,[1] ,true ,#Find ,Cor solutions L ,(solutions, [L]))]*)
61 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
62 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
63 "--------- solve_linear as rootpbl AUTOCALCULATE CompleteCalcHead-";
65 CalcTree (*start of calculation, return No.1*)
66 [(["equality (1+-1*2+x=0)", "solveFor x","solutions L"],
68 ["linear","univariate","equation","test"],
69 ["Test","solve_linear"]))];
70 Iterator 1; moveActiveRoot 1;
73 autoCalculate 1 CompleteCalcHead;
74 autoCalculate 1 (Step 1);
79 autoCalculate 1 CompleteCalcHead;
80 fetchProposedTactic 1; (*-> Apply_Method*);
81 setNextTactic 1 (Apply_Method ["Test","solve_linear"]);
82 autoCalculate 1 (Step 1);
87 autoCalculate 1 (Step 1);
88 refFormula 1 (get_pos 1 1);
90 autoCalculate 1 CompleteModel;
91 refFormula 1 (get_pos 1 1);
93 autoCalculate 1 CompleteCalcHead;
94 (* *** complete_mod: only impl.for Pbl, called with ([], Met) FIXXXXXXXXXXME*)
98 "--------- maximum-example: complete_metitms ---------------------";
99 "--------- maximum-example: complete_metitms ---------------------";
100 "--------- maximum-example: complete_metitms ---------------------";
101 val (p,_,f,nxt,_,pt) =
103 [(["fixedValues [r=Arbfix]","maximum A",
105 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
106 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
107 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
109 "boundVariable a","boundVariable b","boundVariable alpha",
110 "interval {x::real. 0 <= x & x <= 2*r}",
111 "interval {x::real. 0 <= x & x <= 2*r}",
112 "interval {x::real. 0 <= x & x <= pi}",
113 "errorBound (eps=(0::real))"],
114 ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
116 val (p,_,f,nxt,_,pt) = me nxt p c pt;
117 val (p,_,f,nxt,_,pt) = me nxt p c pt;
118 val (p,_,f,nxt,_,pt) = me nxt p c pt;
119 val (p,_,f,nxt,_,pt) = me nxt p c pt;
120 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
121 val (p,_,f,nxt,_,pt) = me nxt p c pt;
122 val (p,_,f,nxt,_,pt) = me nxt p c pt;
123 (*nxt = Specify_Theory "DiffApp.thy"*)
124 val (oris, _, _) = get_obj g_origin pt (fst p);
125 writeln (oris2str oris);
127 (1, ["1","2","3"], #Given,fixedValues, ["[r = Arbfix]"]),
128 (2, ["1","2","3"], #Find,maximum, ["A"]),
129 (3, ["1","2","3"], #Find,valuesFor, ["[a]","[b]"]),
130 (4, ["1","2"], #Relate,relations, ["[A = a * b]","[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]"]),
131 (5, ["3"], #Relate,relations, ["[A = a * b]","[a / 2 = r * sin alpha]","[b / 2 = r * cos alpha]"]),
132 (6, ["1"], #undef,boundVariable, ["a"]),
133 (7, ["2"], #undef,boundVariable, ["b"]),
134 (8, ["3"], #undef,boundVariable, ["alpha"]),
135 (9, ["1","2"], #undef,interval, ["{x. 0 <= x & x <= 2 * r}"]),
136 (10, ["3"], #undef,interval, ["{x. 0 <= x & x <= pi}"]),
137 (11, ["1","2","3"], #undef,errorBound, ["eps = 0"])]*)
138 val pits = get_obj g_pbl pt (fst p);
139 writeln (itms2str thy pits);
141 (1 ,[1,2,3] ,true,#Given ,Cor fixedValues [r = Arbfix],(fix_, [[r = Arbfix]])),
142 (2 ,[1,2,3] ,true,#Find ,Cor maximum A ,(m_, [A])),
143 (3 ,[1,2,3] ,true,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
144 (4 ,[1,2] ,true,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
145 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
146 val mits = get_obj g_met pt (fst p);
147 val mits = complete_metitms oris pits []
148 ((#ppc o get_met) ["DiffApp","max_by_calculus"]);
149 writeln (itms2str thy mits);
151 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
152 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
153 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(vs_, [[a, b]])),
154 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
155 2 = r ^^^ 2] ,(rs_, [[A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
156 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
157 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
158 0 <= x & x <= 2 * r}])),
159 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
160 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 ()
161 else raise error "completetest.sml: new behav. in complete_metitms 1";
164 "--------- maximum-example: complete_mod -------------------------";
165 "--------- maximum-example: complete_mod -------------------------";
166 "--------- maximum-example: complete_mod -------------------------";
167 val (p,_,f,nxt,_,pt) =
169 [(["fixedValues [r=Arbfix]","maximum A",
171 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
172 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
173 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
175 "boundVariable a","boundVariable b","boundVariable alpha",
176 "interval {x::real. 0 <= x & x <= 2*r}",
177 "interval {x::real. 0 <= x & x <= 2*r}",
178 "interval {x::real. 0 <= x & x <= pi}",
179 "errorBound (eps=(0::real))"],
180 ("DiffApp.thy",["maximum_of","function"],["DiffApp","max_by_calculus"])
182 val (p,_,f,nxt,_,pt) = me nxt p c pt;
183 val (p,_,f,nxt,_,pt) = me nxt p c pt;
184 val (p,_,f,nxt,_,pt) = me nxt p c pt;
185 (*nxt = nxt = Add_Find "valuesFor [a]" FIXME.12.03 +handle Inc !*)
186 val pits = get_obj g_pbl pt (fst p);
187 writeln (itms2str thy pits);
189 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
190 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, [])),
191 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
192 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A]))]*)
193 val (pt,p) = complete_mod (pt,p);
194 val pits = get_obj g_pbl pt (fst p);
195 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]]))]"
196 then () else raise error "completetest.sml: new behav. in complete_mod 3";
197 writeln (itms2str thy pits);
199 (1 ,[1,2,3] ,true,#Given,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
200 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
201 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
202 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
203 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]]))]*)
204 val mits = get_obj g_met pt (fst p);
205 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]))]"
206 then () else raise error "completetest.sml: new behav. in complete_mod 3";
207 writeln (itms2str thy mits);
209 (1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),
210 (2 ,[1,2,3] ,true ,#Find ,Cor maximum A ,(m_, [A])),
211 (3 ,[1,2,3] ,true ,#Find ,Cor valuesFor [a, b] ,(valuesFor, [[a],[b]])),
212 (4 ,[1,2] ,true ,#Relate ,Cor relations [A = a * b, (a / 2) ^^^ 2 + (b / 2) ^^^
213 2 = r ^^^ 2] ,(relations, [[A = a * b],[(a / 2) ^^^ 2 + (b / 2) ^^^ 2 = r ^^^ 2]])),
214 (6 ,[1] ,true ,#undef ,Cor boundVariable a ,(boundVariable, [a])),
215 (9 ,[1,2] ,true ,#undef ,Cor interval {x. 0 <= x & x <= 2 * r} ,(interval, [{x.
216 0 <= x & x <= 2 * r}])),
217 (11 ,[1,2,3] ,true ,#undef ,Cor errorBound (eps = 0) ,(errorBound, [eps = 0]))]*)
222 "--------- appendFormula: on Res + equ_nrls ----------------------";
223 "--------- appendFormula: on Res + equ_nrls ----------------------";
224 "--------- appendFormula: on Res + equ_nrls ----------------------";
225 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
226 (writeln o term2str) sc;
227 val Script sc = (#scr o get_met) ["Test","solve_linear"];
228 (writeln o term2str) sc;
231 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
233 ["sqroot-test","univariate","equation","test"],
234 ["Test","squ-equ-test-subpbl1"]))];
235 Iterator 1; moveActiveRoot 1;
236 autoCalculate 1 CompleteCalcHead;
237 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
238 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
240 appendFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
241 val ((pt,_),_) = get_calc 1;
242 val str = pr_ptree pr_short pt;
244 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then ()
245 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 1";
247 moveDown 1 ([ ],Pbl); refFormula 1 ([1],Frm); (*x + 1 = 2*)
248 moveDown 1 ([1],Frm); refFormula 1 ([1],Res); (*x + 1 + -1 * 2 = 0*)
250 (*the seven steps of detailed derivation*)
251 moveDown 1 ([1 ],Res); refFormula 1 ([2,1],Frm);
252 moveDown 1 ([2,1],Frm); refFormula 1 ([2,1],Res);
253 moveDown 1 ([2,1],Res); refFormula 1 ([2,2],Res);
254 moveDown 1 ([2,2],Res); refFormula 1 ([2,3],Res);
255 moveDown 1 ([2,3],Res); refFormula 1 ([2,4],Res);
256 moveDown 1 ([2,4],Res); refFormula 1 ([2,5],Res);
257 moveDown 1 ([2,5],Res); refFormula 1 ([2,6],Res);
258 val ((pt,_),_) = get_calc 1;
259 if "-2 * 1 + (1 + x) = 0" = term2str (fst (get_obj g_result pt [2,6])) then()
260 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 2";
262 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
263 val (_,(tac,_,_)::_) = get_calc 1;
264 if tac = Rewrite_Set "Test_simplify" then ()
265 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 3";
266 autoCalculate 1 CompleteCalc;
267 val ((pt,_),_) = get_calc 1;
268 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
269 else raise error "auto-inform.sml: diff.behav.appendFormula: on Res + equ 4";
270 (* autoCalculate 1 CompleteCalc;
271 val ((pt,p),_) = get_calc 1;
272 (writeln o istates2str) (get_obj g_loc pt [ ]);
273 (writeln o istates2str) (get_obj g_loc pt [1]);
274 (writeln o istates2str) (get_obj g_loc pt [2]);
275 (writeln o istates2str) (get_obj g_loc pt [3]);
276 (writeln o istates2str) (get_obj g_loc pt [3,1]);
277 (writeln o istates2str) (get_obj g_loc pt [3,2]);
278 (writeln o istates2str) (get_obj g_loc pt [4]);
281 "----------------------------------------------------------";
282 val fod = make_deriv Isac.thy Atools_erls
283 ((#rules o rep_rls) Test_simplify)
284 (sqrt_right false ProtoPure.thy) None
285 (str2term "x + 1 + -1 * 2 = 0");
286 (writeln o trtas2str) fod;
288 val ifod = make_deriv Isac.thy Atools_erls
289 ((#rules o rep_rls) Test_simplify)
290 (sqrt_right false ProtoPure.thy) None
291 (str2term "-2 * 1 + (1 + x) = 0");
292 (writeln o trtas2str) ifod;
293 fun equal (_,_,(t1, _)) (_,_,(t2, _)) = t1=t2;
294 val (fod', rifod') = dropwhile' equal (rev fod) (rev ifod);
295 val der = fod' @ (map rev_deriv' rifod');
296 (writeln o trtas2str) der;
297 "----------------------------------------------------------";
300 "--------- appendFormula: on Frm + equ_nrls ----------------------";
301 "--------- appendFormula: on Frm + equ_nrls ----------------------";
302 "--------- appendFormula: on Frm + equ_nrls ----------------------";
303 (**@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@**)
305 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
307 ["sqroot-test","univariate","equation","test"],
308 ["Test","squ-equ-test-subpbl1"]))];
309 Iterator 1; moveActiveRoot 1;
310 autoCalculate 1 CompleteCalcHead;
311 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
313 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
315 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
318 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
319 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
320 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
321 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
322 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
323 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
324 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
325 val ((pt,_),_) = get_calc 1;
326 if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
327 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 1";
329 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
330 val (_,(tac,_,_)::_) = get_calc 1;
331 if tac = Rewrite_Set "norm_equation" then ()
332 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 2";
333 autoCalculate 1 CompleteCalc;
334 val ((pt,_),_) = get_calc 1;
335 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
336 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
339 "--------- appendFormula: on Res + NO deriv ----------------------";
340 "--------- appendFormula: on Res + NO deriv ----------------------";
341 "--------- appendFormula: on Res + NO deriv ----------------------";
343 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
345 ["sqroot-test","univariate","equation","test"],
346 ["Test","squ-equ-test-subpbl1"]))];
347 Iterator 1; moveActiveRoot 1;
348 autoCalculate 1 CompleteCalcHead;
349 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
350 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
352 appendFormula 1 "x = 2";
353 val ((pt,p),_) = get_calc 1;
354 val str = pr_ptree pr_short pt;
356 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
358 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + NOder 1";
360 fetchProposedTactic 1;
361 val (_,(tac,_,_)::_) = get_calc 1;
362 if tac = Rewrite_Set "Test_simplify" then ()
363 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + NOder 2";
364 autoCalculate 1 CompleteCalc;
365 val ((pt,_),_) = get_calc 1;
366 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
367 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
370 "--------- appendFormula: on Res + late deriv --------------------";
371 "--------- appendFormula: on Res + late deriv --------------------";
372 "--------- appendFormula: on Res + late deriv --------------------";
374 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
376 ["sqroot-test","univariate","equation","test"],
377 ["Test","squ-equ-test-subpbl1"]))];
378 Iterator 1; moveActiveRoot 1;
379 autoCalculate 1 CompleteCalcHead;
380 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
381 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
383 appendFormula 1 "x = 1";
384 val ((pt,p),_) = get_calc 1;
385 val str = pr_ptree pr_short pt;
387 if str = ". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n3.2.1. x = 0 + -1 * -1\n3.2.2. x = 0 + 1\n" andalso p = ([3,2], Res)
388 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
389 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 1";
391 fetchProposedTactic 1;
392 val (_,(tac,_,_)::_) = get_calc 1;
393 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
394 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 2";
395 autoCalculate 1 CompleteCalc;
396 val ((pt,_),_) = get_calc 1;
397 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
398 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 3";
401 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
402 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
403 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
405 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
407 ["sqroot-test","univariate","equation","test"],
408 ["Test","squ-equ-test-subpbl1"]))];
409 Iterator 1; moveActiveRoot 1;
410 autoCalculate 1 CompleteCalcHead;
411 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
412 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
413 appendFormula 1 "[x = 3 + -2*1]";
414 val ((pt,p),_) = get_calc 1;
415 val str = pr_ptree pr_short pt;
417 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n3. ----- pblobj -----\n3.1. -1 + x = 0\n3.2. x = 0 + -1 * -1\n4. [x = 1]\n4.1. [x = 1]\n4.2. [x = -2 + 3]\n4.3. [x = 3 + -2]\n" then ()
418 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + latEE 1";
419 autoCalculate 1 CompleteCalc;
420 val ((pt,p),_) = get_calc 1;
421 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
422 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
423 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + latEE 2";
427 "--------- replaceFormula: on Res + = ----------------------------";
428 "--------- replaceFormula: on Res + = ----------------------------";
429 "--------- replaceFormula: on Res + = ----------------------------";
431 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
433 ["sqroot-test","univariate","equation","test"],
434 ["Test","squ-equ-test-subpbl1"]))];
435 Iterator 1; moveActiveRoot 1;
436 autoCalculate 1 CompleteCalcHead;
437 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
438 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
439 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
441 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
442 val ((pt,_),_) = get_calc 1;
443 val str = pr_ptree pr_short pt;
445 if str=". ----- pblobj -----\n1. x + 1 = 2\n2. x + 1 + -1 * 2 = 0\n2.1. x + 1 + -1 * 2 = 0\n2.2. -1 * 2 + (x + 1) = 0\n2.3. -1 * 2 + (1 + x) = 0\n2.4. 1 + (-1 * 2 + x) = 0\n2.5. 1 + (-2 + x) = 0\n2.6. 1 + (-2 * 1 + x) = 0\n" then()
446 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1";
447 autoCalculate 1 CompleteCalc;
448 val ((pt,pos as(p,_)),_) = get_calc 1;
449 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
450 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
453 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
454 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
455 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
457 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
459 ["sqroot-test","univariate","equation","test"],
460 ["Test","squ-equ-test-subpbl1"]))];
461 Iterator 1; moveActiveRoot 1;
462 autoCalculate 1 CompleteCalcHead;
463 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
464 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
466 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
467 val ((pt,_),_) = get_calc 1;
468 val str = pr_ptree pr_short pt;
470 if str=". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
471 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
472 autoCalculate 1 CompleteCalc;
473 val ((pt,pos as(p,_)),_) = get_calc 1;
474 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
475 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
478 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
479 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
480 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
482 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
484 ["sqroot-test","univariate","equation","test"],
485 ["Test","squ-equ-test-subpbl1"]))];
486 Iterator 1; moveActiveRoot 1;
487 autoCalculate 1 CompleteCalcHead;
488 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
490 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
491 val ((pt,_),_) = get_calc 1;
492 val str = pr_ptree pr_short pt;
494 if str=". ----- pblobj -----\n1. x + 1 = 2\n1.1. x + 1 = 2\n1.2. 1 + x = 2\n1.3. 1 + x = -2 + 4\n1.4. x + 1 = -2 + 4\n" then ()
495 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
496 autoCalculate 1 CompleteCalc;
497 val ((pt,pos as(p,_)),_) = get_calc 1;
498 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
499 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
502 "--------- replaceFormula: cut calculation -----------------------";
503 "--------- replaceFormula: cut calculation -----------------------";
504 "--------- replaceFormula: cut calculation -----------------------";
506 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
508 ["sqroot-test","univariate","equation","test"],
509 ["Test","squ-equ-test-subpbl1"]))];
510 Iterator 1; moveActiveRoot 1;
511 autoCalculate 1 CompleteCalc;
512 moveActiveRoot 1; moveActiveDown 1;
513 if get_pos 1 1 = ([1], Frm) then ()
514 else raise error "auto-inform.sml: diff.behav. cut calculation 1";
516 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
517 val ((pt,p),_) = get_calc 1;
518 val str = pr_ptree pr_short pt;
520 if p = ([1], Res) then ()
521 else raise error "auto-inform.sml: diff.behav. cut calculation 2";
528 (* 040307 copied from informtest.sml; ... old version
529 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
530 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
531 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
534 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
535 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
536 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
537 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
538 (*^^^ these are the elements for the root-problem (in variants)*)
539 (*vvv these are elements required for subproblems*)
540 "boundVariable a","boundVariable b","boundVariable alpha",
541 "interval {x::real. 0 <= x & x <= 2*r}",
542 "interval {x::real. 0 <= x & x <= 2*r}",
543 "interval {x::real. 0 <= x & x <= pi}",
544 "errorBound (eps=(0::real))"]
545 (*specifying is not interesting for this example*)
546 val spec = ("DiffApp.thy", ["maximum_of","function"],
547 ["DiffApp","max_by_calculus"]);
548 (*the empty model with descriptions for user-guidance by Model_Problem*)
549 val empty_model = [Given ["fixedValues []"],
550 Find ["maximum", "valuesFor"],
551 Relate ["relations []"]];
554 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
555 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
556 (*val nxt = ("Model_Problem", ...*)
557 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
559 val (p,_,f,nxt,_,pt) = me nxt p c pt;
560 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
561 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
563 (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
564 (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
565 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
566 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
568 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
569 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
570 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
571 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then () else raise error "informtest.sml: diff.behav. max 1";
573 (*there is one input to the model (could be more)*)
575 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
576 Find ["maximum", "valuesFor"],
577 Relate ["relations"]], Pbl, e_spec);
578 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
579 if ocalhd2str ocalhd = "(Pbl, ??.empty, [\n(1 ,[1,2,3] ,true ,#Given ,Cor fixedValues [r = Arbfix] ,(fix_, [[r = Arbfix]])),\n(0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),\n(0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),\n(0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))], [], \n(\"e_domID\", [\"e_pblID\"], [\"e_metID\"]) )" then ()
580 else raise error "informtest.sml: diff.behav. max 2";
582 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
583 val (b,pt''''',ocalhd) =
584 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
585 Find ["maximum A", "valuesFor [a,b]"],
586 Relate ["relations [A=a*b, a/2=r*sin alpha, \
587 \b/2=r*cos alpha]"]], Pbl, e_spec);
588 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
589 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing GOON !!!*)
591 (*this input is complete in variant 1 (variant 3 does not work yet)*)
592 val (b,pt''''',ocalhd) =
593 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
594 Find ["maximum A", "valuesFor [a,b]"],
595 Relate ["relations [A=a*b, \
596 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
598 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
600 modifycalcheadOK2xml 111 (bool2str b) ocalhd;