1 (* use"systest/subp-rooteq.sml";
6 "---------------- miniscript with mini-subpbl -------------";
7 "---------------- solve_linear as rootpbl -----------------";
8 "---------------- solve_plain_square as rootpbl -----------";
9 "---------------- root-eq + subpbl: solve_linear ----------";
10 "---------------- root-eq + subpbl: solve_plain_square ----";
11 "---------------- root-eq + subpbl: no_met: linear --------";
12 "---------------- root-eq + subpbl: no_met: square --------";
13 "---------------- no_met in rootpbl -> linear -------------";
14 "==========================================================";
19 "---------------- miniscript with mini-subpbl -------------";
20 "---------------- miniscript with mini-subpbl -------------";
21 "---------------- miniscript with mini-subpbl -------------";
22 (*###########################################################
23 ## 12.03 next_tac repariert (gab keine Value zurueck ###
24 ###########################################################*)
25 val fmz = ["equality (x+1=(2::real))", "solveFor x","solutions L"];
27 ("Test",["sqroot-test","univariate","equation","test"],
28 ["Test","squ-equ-test-subpbl1"]);
30 val Prog sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
31 (writeln o term2str) sc;
33 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
34 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
35 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
37 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
38 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
39 (*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
40 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
41 (*("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation"]*)
42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
43 (*("Specify_Method",Specify_Method ("Test","squ-equ-test-subpbl1"))*)
44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
45 (*val nxt = ("Apply_Method",Apply_Method ("Test","squ-equ-test-subpbl1"*)
46 (*---vvv--- nxt_ here = loc_ below ------------------vvv-------------------*)
47 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
48 (*val f = "x + 1 = 2"; val nxt = Rewrite_Set "norm_equation"*)
49 (*### solve Apply_Method: is = ### nxt_solv1 Apply_Method: store is
54 ??.empty, Safe, true) ########## OK*)
55 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
56 (*val f = "x + 1 + -1 * 2 = 0"; val nxt = Rewrite_Set "Test_simplify"*)
57 (*### locate_gen----------: is= ### next_tac----------------:E =
62 ??.empty, Safe, true) ########## OK von loc_ uebernommen
63 ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
67 [R,L,R,L,L,R,R], SOME e_e,
68 x + 1 + -1 * 2 = 0, Safe, true) ########## OK*)
69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
72 (*val f = "-1 + x = 0"; val nxt = Subproblem ("Test",[#,#,#])
73 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
74 (*### locate_gen-----------: is= ### next_tac-----------------: E=
78 [R,L,R,L,L,R,R], SOME e_e,
79 x + 1 + -1 * 2 = 0, Safe, true) ########## OK von loc_ uebernommen
80 ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
84 [R,L,R,L,R,R], SOME e_e,
85 -1 + x = 0, Safe, false) ########## OK*)
86 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
87 (*### locate_gen------------: is= ### next_tac-----------------: E=
91 [R,L,R,L,R,R], SOME e_e,
92 -1 + x = 0, Safe, false) ########## OK von loc_ uebernommen
93 ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
97 [R,R,D,L,R], SOME e_e,
98 Subproblem (Test.thy, [linear, univariate, equation, test]), Safe, true)
101 writeln(istate2str (fst (get_istate pt ([3],Frm))));
102 (*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)
103 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
104 (*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
105 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
106 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 (*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * tac*)
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
110 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
112 (*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
114 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
115 val Prog sc = (#scr o get_met) ["Test","solve_linear"];
116 (writeln o term2str) sc;
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
121 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
122 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
125 (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","eq*)
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
129 writeln(istate2str (fst (get_istate pt ([3],Res))));
130 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
131 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
133 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
135 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
136 else error "subp-rooteq.sml: new.behav. in miniscript with mini-subpbl";
139 "---------------- solve_linear as rootpbl -----------------";
140 "---------------- solve_linear as rootpbl -----------------";
141 "---------------- solve_linear as rootpbl -----------------";
142 val fmz = ["equality (1+-1*2+x=(0::real))",
143 "solveFor x","solutions L"];
145 ("Test",["LINEAR","univariate","equation","test"],
146 ["Test","solve_linear"]);
148 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 (*val nxt = ("Specify_Theory",Specify_Theory "Test") : string * tac*)
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 (*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
160 (*val nxt = ("Specify_Method",Specify_Method ("Test","solve_linear"))*)
161 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
162 (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
163 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
164 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
165 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
167 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
168 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
169 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * tac*)
171 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
172 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)
174 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
175 (*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout
176 val nxt = ("End_Proof'",End_Proof') : string * tac*)
177 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
178 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
179 else error "subp-rooteq.sml: new.behav. in solve_linear as rootpbl";
182 "---------------- solve_plain_square as rootpbl -----------";
183 "---------------- solve_plain_square as rootpbl -----------";
184 "---------------- solve_plain_square as rootpbl -----------";
185 val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
188 ("Test",["plain_square","univariate","equation","test"],
189 ["Test","solve_plain_square"]);
190 (*val p = e_pos'; val c = [];
191 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
192 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
194 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
197 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
199 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
200 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
201 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
202 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
203 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
204 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
205 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
206 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
207 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
209 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
210 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
211 if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
212 else error "subp-rooteq.sml: new.behav. in solve_plain_square as rootpbl";
217 "---------------- root-eq + subpbl: solve_linear ----------";
218 "---------------- root-eq + subpbl: solve_linear ----------";
219 "---------------- root-eq + subpbl: solve_linear ----------";
220 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
221 "solveFor x","solutions L"];
223 ("Test",["sqroot-test","univariate","equation","test"],
224 ["Test","square_equation1"]);
225 (*val p = e_pos'; val c = [];
226 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
227 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
228 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
232 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
233 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
234 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
235 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
236 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
237 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
238 square_equation_left*)
239 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
240 (*"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"
242 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
243 (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"
245 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
246 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"
248 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
249 (*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
251 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
253 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
254 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
256 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
257 (*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
260 val nxt =("Subproblem",Subproblem ("Test",["LINEAR","univariate"...*)
261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
262 (*val nxt =("Model_Problem",Model_Problem ["LINEAR","univariate"...*)
263 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
266 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
267 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
268 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
269 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
270 (*("Specify_Problem",Specify_Problem ["LINEAR","univariate","equation"])*)
271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
272 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
273 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
275 (*"x = 0 + -1 * -4", nxt Test_simplify*)
276 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
277 (*"x = 4", nxt Check_Postcond ["LINEAR","univariate","equation","test"]*)
278 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
279 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
280 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
281 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
282 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
283 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
284 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
285 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_linear";
289 "---------------- root-eq + subpbl: solve_plain_square ----";
290 "---------------- root-eq + subpbl: solve_plain_square ----";
291 "---------------- root-eq + subpbl: solve_plain_square ----";
292 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
293 "solveFor x","solutions L"];
295 ("Test",["sqroot-test","univariate","equation","test"],
296 ["Test","square_equation2"]);
297 val Prog sc = (#scr o get_met) ["Test","square_equation2"];
298 (writeln o term2str) sc;
300 (*val p = e_pos'; val c = [];
301 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
302 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
303 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
304 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
305 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
306 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
307 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
308 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
309 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
310 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
311 (*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)
312 val (p,_,f,nxt,_,pt) =
315 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
316 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
317 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
318 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
319 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
320 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
321 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
322 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
323 (*"9 + -1 * x ^^^ 2 = 0"
324 Subproblem ("Test",["plain_square","univariate","equation"]))*)
325 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
326 (*Model_Problem ["plain_square","univariate","equation"]*)
327 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
328 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
329 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
330 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
331 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
334 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
335 (*Apply_Method ("Test","solve_plain_square")*)
336 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
337 (*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
339 (*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)
340 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
341 (*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*)
342 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
343 (*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
345 (*"x = -3 | x = 3", nxt Or_to_List*)
346 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
348 nxt Check_Postcond ["plain_square","univariate","equation","test"]*)
349 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
353 (*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
354 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
355 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
356 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
357 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
358 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
359 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
362 writeln (pr_ctree pr_short pt);
366 val Prog s = (#scr o get_met) ["Test","square_equation"];
372 "---------------- root-eq + subpbl: no_met: linear ----";
373 "---------------- root-eq + subpbl: no_met: linear ----";
374 "---------------- root-eq + subpbl: no_met: linear ----";
375 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
376 "solveFor x","solutions L"];
378 ("Test",["squareroot","univariate","equation","test"],
379 ["Test","square_equation"]);
380 (*val p = e_pos'; val c = [];
381 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
382 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
383 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
384 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
385 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
386 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
387 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
388 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
389 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
390 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
391 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
392 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
393 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
394 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
395 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
396 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
403 (*"-4 + x = 0", nxt Subproblem ("Test",["univariate","equation"]))*)
404 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
405 (*val nxt =("Model_Problem",Model_Problem ["LINEAR","univar...*)
406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
409 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
410 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
412 (*val nxt = ("Specify_Problem",Specify_Problem ["LINEAR","univariate","equ*)
413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
415 (*Apply_Method ("Test","norm_univar_equation")*)
416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
419 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
420 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
421 if p = ([13],Res) then ()
422 else error ("subp-rooteq.sml: new.behav. in \
423 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
424 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
425 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
426 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
427 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
432 "---------------- root-eq + subpbl: no_met: square ----";
433 "---------------- root-eq + subpbl: no_met: square ----";
434 "---------------- root-eq + subpbl: no_met: square ----";
435 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
436 "solveFor x","solutions L"];
438 ("Test",["squareroot","univariate","equation","test"],
439 ["Test","square_equation"]);
440 val Prog sc = (#scr o get_met) ["Test","square_equation"];
441 (writeln o term2str) sc;
443 (*val p = e_pos'; val c = [];
444 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
445 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
446 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
447 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
448 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
449 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
450 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
451 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
452 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
453 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
454 (*val nxt = ("Apply_Method",Apply_Method ("Test","square_equation1"))*)
455 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
456 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
457 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
458 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
459 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
460 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
461 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
462 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
463 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
464 (*Subproblem ("Test",["univariate","equation"]))*)
465 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
466 (*Model_Problem ["plain_square","univariate","equation"]*)
467 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
468 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
469 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
471 (*val nxt = ("Specify_Theory",Specify_Theory "Test")*)
472 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
473 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
474 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
475 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
476 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
477 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
478 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
479 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
480 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
481 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
482 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
483 (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*)
484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
485 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
486 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
487 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: no_met: square";
491 "---------------- no_met in rootpbl -> linear --------------";
492 "---------------- no_met in rootpbl -> linear --------------";
493 "---------------- no_met in rootpbl -> linear --------------";
494 val fmz = ["equality (1+2*x+3=4*x- 6)",
495 "solveFor x","solutions L"];
497 ("Test",["univariate","equation","test"],
499 (*val p = e_pos'; val c = [];
500 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
501 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
502 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
503 (*val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*)
504 val (p,_,f,nxt,_,pt) = me nxt p c pt;
505 val (p,_,f,nxt,_,pt) = me nxt p c pt;
506 val (p,_,f,nxt,_,pt) = me nxt p c pt;
507 val (p,_,f,nxt,_,pt) = me nxt p c pt;
508 val (p,_,f,nxt,_,pt) = me nxt p c pt;
509 val (p,_,f,nxt,_,pt) = me nxt p c pt;
510 val (p,_,f,nxt,_,pt) = me nxt p c pt;
511 (*val nxt = ("Apply_Method",Apply_Method ("Test","norm_univar_equation"*)
512 val (p,_,f,nxt,_,pt) = me nxt p c pt;
513 val (p,_,f,nxt,_,pt) = me nxt p c pt;
514 val (p,_,f,nxt,_,pt) = me nxt p c pt;
515 (*val nxt = ("Subproblem",Subproblem ("Test",["univariate","equation"])*)
516 val (p,_,f,nxt,_,pt) = me nxt p c pt;
517 (*val nxt = ("Model_Problem",Model_Problem ["LINEAR","univariate","equation"]*)
518 val (p,_,f,nxt,_,pt) = me nxt p c pt;
519 val (p,_,f,nxt,_,pt) = me nxt p c pt;
520 val (p,_,f,nxt,_,pt) = me nxt p c pt;
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
522 val (p,_,f,nxt,_,pt) = me nxt p c pt;
523 val (p,_,f,nxt,_,pt) = me nxt p c pt;
524 val (p,_,f,nxt,_,pt) = me nxt p c pt;
525 (*val nxt = ("Apply_Method",Apply_Method ("Test","solve_linear"))*)
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;
529 (*val nxt = ("Check_Postcond",Check_Postcond ["LINEAR","univariate","equatio*)
530 val (p,_,f,nxt,_,pt) = me nxt p c pt;
531 (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)
532 val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) =
534 if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
535 else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
538 refine fmz ["univariate","equation","test"];
539 match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]);