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 ----------------------";
304 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
306 ["sqroot-test","univariate","equation","test"],
307 ["Test","squ-equ-test-subpbl1"]))];
308 Iterator 1; moveActiveRoot 1;
309 autoCalculate 1 CompleteCalcHead;
310 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1) (*x + 1 = 2*);
312 appendFormula 1 "2+ -1 + x = 2"; refFormula 1 (get_pos 1 1);
314 moveDown 1 ([],Pbl); refFormula 1 ([1],Frm) (*x + 1 = 2*);
316 moveDown 1 ([1 ],Frm); refFormula 1 ([1,1],Frm);
317 moveDown 1 ([1,1],Frm); refFormula 1 ([1,1],Res);
318 moveDown 1 ([1,1],Res); refFormula 1 ([1,2],Res);
319 moveDown 1 ([1,2],Res); refFormula 1 ([1,3],Res);
320 moveDown 1 ([1,3],Res); refFormula 1 ([1,4],Res);
321 moveDown 1 ([1,4],Res); refFormula 1 ([1,5],Res);
322 moveDown 1 ([1,5],Res); refFormula 1 ([1,6],Res);
323 val ((pt,_),_) = get_calc 1;
324 if "2 + -1 + x = 2" = term2str (fst (get_obj g_result pt [1,6])) then()
325 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 1";
327 fetchProposedTactic 1; (*takes Iterator 1 _1_*)
328 val (_,(tac,_,_)::_) = get_calc 1;
329 if tac = Rewrite_Set "norm_equation" then ()
330 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 2";
331 autoCalculate 1 CompleteCalc;
332 val ((pt,_),_) = get_calc 1;
333 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
334 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
337 "--------- appendFormula: on Res + NO deriv ----------------------";
338 "--------- appendFormula: on Res + NO deriv ----------------------";
339 "--------- appendFormula: on Res + NO deriv ----------------------";
341 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
343 ["sqroot-test","univariate","equation","test"],
344 ["Test","squ-equ-test-subpbl1"]))];
345 Iterator 1; moveActiveRoot 1;
346 autoCalculate 1 CompleteCalcHead;
347 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
348 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
350 appendFormula 1 "x = 2";
351 val ((pt,p),_) = get_calc 1;
352 val str = pr_ptree pr_short pt;
354 if str = ". ----- pblobj -----\n1. x + 1 = 2\n" andalso p = ([1], Res)
356 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + NOder 1";
358 fetchProposedTactic 1;
359 val (_,(tac,_,_)::_) = get_calc 1;
360 if tac = Rewrite_Set "Test_simplify" then ()
361 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + NOder 2";
362 autoCalculate 1 CompleteCalc;
363 val ((pt,_),_) = get_calc 1;
364 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
365 else raise error "auto-inform.sml: diff.behav.appendFormula: on Frm + equ 3";
368 "--------- appendFormula: on Res + late deriv --------------------";
369 "--------- appendFormula: on Res + late deriv --------------------";
370 "--------- appendFormula: on Res + late deriv --------------------";
372 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
374 ["sqroot-test","univariate","equation","test"],
375 ["Test","squ-equ-test-subpbl1"]))];
376 Iterator 1; moveActiveRoot 1;
377 autoCalculate 1 CompleteCalcHead;
378 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
379 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
381 appendFormula 1 "x = 1";
382 val ((pt,p),_) = get_calc 1;
383 val str = pr_ptree pr_short pt;
385 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)
386 then () (*finds 1 step too early: ([3,2], Res) "x = 1" also by script !!!*)
387 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 1";
389 fetchProposedTactic 1;
390 val (_,(tac,_,_)::_) = get_calc 1;
391 if tac = Check_Postcond ["linear", "univariate", "equation", "test"] then ()
392 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 2";
393 autoCalculate 1 CompleteCalc;
394 val ((pt,_),_) = get_calc 1;
395 if "[x = 1]" = term2str (fst (get_obj g_result pt [])) then ()
396 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + late d 3";
399 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
400 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
401 "--------- appendFormula: on Res + late deriv [x = 3 + -2]---///--";
403 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
405 ["sqroot-test","univariate","equation","test"],
406 ["Test","squ-equ-test-subpbl1"]))];
407 Iterator 1; moveActiveRoot 1;
408 autoCalculate 1 CompleteCalcHead;
409 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
410 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
411 appendFormula 1 "[x = 3 + -2*1]";
412 val ((pt,p),_) = get_calc 1;
413 val str = pr_ptree pr_short pt;
415 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 ()
416 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + latEE 1";
417 autoCalculate 1 CompleteCalc;
418 val ((pt,p),_) = get_calc 1;
419 if "[x = 3 + -2 * 1]" = term2str (fst (get_obj g_result pt [])) then ()
420 (* ~~~~~~~~~~ simplify as last step in any script ?!*)
421 else raise error "auto-inform.sml: diff.behav.appendFormula: Res + latEE 2";
425 "--------- replaceFormula: on Res + = ----------------------------";
426 "--------- replaceFormula: on Res + = ----------------------------";
427 "--------- replaceFormula: on Res + = ----------------------------";
429 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
431 ["sqroot-test","univariate","equation","test"],
432 ["Test","squ-equ-test-subpbl1"]))];
433 Iterator 1; moveActiveRoot 1;
434 autoCalculate 1 CompleteCalcHead;
435 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
436 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
437 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*-1 + x*);
439 replaceFormula 1 "-2 * 1 + (1 + x) = 0"; refFormula 1 (get_pos 1 1);
440 val ((pt,_),_) = get_calc 1;
441 val str = pr_ptree pr_short pt;
443 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()
444 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res += 1";
445 autoCalculate 1 CompleteCalc;
446 val ((pt,pos as(p,_)),_) = get_calc 1;
447 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
448 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
451 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
452 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
453 "--------- replaceFormula: on Res + = 1st Nd ---------------------";
455 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
457 ["sqroot-test","univariate","equation","test"],
458 ["Test","squ-equ-test-subpbl1"]))];
459 Iterator 1; moveActiveRoot 1;
460 autoCalculate 1 CompleteCalcHead;
461 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
462 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 + -1 * 2 = 0*);
464 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
465 val ((pt,_),_) = get_calc 1;
466 val str = pr_ptree pr_short pt;
468 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 ()
469 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res 1 + = 1";
470 autoCalculate 1 CompleteCalc;
471 val ((pt,pos as(p,_)),_) = get_calc 1;
472 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
473 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Res + = 2";
476 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
477 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
478 "--------- replaceFormula: on Frm + = 1st Nd ---------------------";
480 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
482 ["sqroot-test","univariate","equation","test"],
483 ["Test","squ-equ-test-subpbl1"]))];
484 Iterator 1; moveActiveRoot 1;
485 autoCalculate 1 CompleteCalcHead;
486 autoCalculate 1 (Step 1); refFormula 1 (get_pos 1 1);(*x + 1 = 2*)
488 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
489 val ((pt,_),_) = get_calc 1;
490 val str = pr_ptree pr_short pt;
492 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 ()
493 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Frm 1 + = 1";
494 autoCalculate 1 CompleteCalc;
495 val ((pt,pos as(p,_)),_) = get_calc 1;
496 if pos=([],Res)andalso"[x = 1]"=(term2str o fst)(get_obj g_result pt p)then()
497 else raise error "auto-inform.sml: diff.behav.replaceFormula: on Frm 1 + = 2";
500 "--------- replaceFormula: cut calculation -----------------------";
501 "--------- replaceFormula: cut calculation -----------------------";
502 "--------- replaceFormula: cut calculation -----------------------";
504 CalcTree [(["equality (x+1=2)", "solveFor x","solutions L"],
506 ["sqroot-test","univariate","equation","test"],
507 ["Test","squ-equ-test-subpbl1"]))];
508 Iterator 1; moveActiveRoot 1;
509 autoCalculate 1 CompleteCalc;
510 moveActiveRoot 1; moveActiveDown 1;
511 if get_pos 1 1 = ([1], Frm) then ()
512 else raise error "auto-inform.sml: diff.behav. cut calculation 1";
514 replaceFormula 1 "x + 1 = 4 + -2"; refFormula 1 (get_pos 1 1);
515 val ((pt,p),_) = get_calc 1;
516 val str = pr_ptree pr_short pt;
518 if p = ([1], Res) then ()
519 else raise error "auto-inform.sml: diff.behav. cut calculation 2";
526 (* 040307 copied from informtest.sml; ... old version
527 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
528 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
529 "---------------- maximum-example, UC: Modeling / modifyCalcHead -";
532 val elems = ["fixedValues [r=Arbfix]","maximum A","valuesFor [a,b]",
533 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
534 "relations [A=a*b, (a/2)^^^2 + (b/2)^^^2 = r^^^2]",
535 "relations [A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]",
536 (*^^^ these are the elements for the root-problem (in variants)*)
537 (*vvv these are elements required for subproblems*)
538 "boundVariable a","boundVariable b","boundVariable alpha",
539 "interval {x::real. 0 <= x & x <= 2*r}",
540 "interval {x::real. 0 <= x & x <= 2*r}",
541 "interval {x::real. 0 <= x & x <= pi}",
542 "errorBound (eps=(0::real))"]
543 (*specifying is not interesting for this example*)
544 val spec = ("DiffApp.thy", ["maximum_of","function"],
545 ["DiffApp","max_by_calculus"]);
546 (*the empty model with descriptions for user-guidance by Model_Problem*)
547 val empty_model = [Given ["fixedValues []"],
548 Find ["maximum", "valuesFor"],
549 Relate ["relations []"]];
552 (*!!!!!!!!!!!!!!!!! DON'T USE me FOR FINDING nxt !!!!!!!!!!!!!!!!!!*)
553 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(elems, spec)];
554 (*val nxt = ("Model_Problem", ...*)
555 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
557 val (p,_,f,nxt,_,pt) = me nxt p c pt;
558 (*nxt = Add_Given "fixedValues [r = Arbfix]"*)
559 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
561 (0 ,[] ,false ,#Given ,Inc fixedValues [] ,(??.empty, [])),
562 (0 ,[] ,false ,#Find ,Inc maximum ,(??.empty, [])),
563 (0 ,[] ,false ,#Find ,Inc valuesFor ,(??.empty, [])),
564 (0 ,[] ,false ,#Relate ,Inc relations [] ,(??.empty, []))]*)
566 (*the empty CalcHead is checked w.r.t the model and re-established as such*)
567 val (b,pt,ocalhd) = input_icalhd pt (p,"", empty_model, Pbl, e_spec);
568 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
569 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";
571 (*there is one input to the model (could be more)*)
573 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
574 Find ["maximum", "valuesFor"],
575 Relate ["relations"]], Pbl, e_spec);
576 val pbl = get_obj g_pbl pt (fst p); (writeln o (itms2str thy)) pbl;
577 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 ()
578 else raise error "informtest.sml: diff.behav. max 2";
580 (*this input is complete in variant 3, but the ME doesn't recognize FIXXXXME
581 val (b,pt''''',ocalhd) =
582 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
583 Find ["maximum A", "valuesFor [a,b]"],
584 Relate ["relations [A=a*b, a/2=r*sin alpha, \
585 \b/2=r*cos alpha]"]], Pbl, e_spec);
586 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
587 if ocalhd2str ocalhd = ------------^^^^^^^^^^ missing GOON !!!*)
589 (*this input is complete in variant 1 (variant 3 does not work yet)*)
590 val (b,pt''''',ocalhd) =
591 input_icalhd pt (p,"", [Given ["fixedValues [r=Arbfix]"],
592 Find ["maximum A", "valuesFor [a,b]"],
593 Relate ["relations [A=a*b, \
594 \(a/2)^^^2 + (b/2)^^^2 = r^^^2]"]],
596 val pbl = get_obj g_pbl pt''''' (fst p); (writeln o (itms2str thy)) pbl;
598 modifycalcheadOK2xml 111 (bool2str b) ocalhd;