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)",
26 "solveFor x","solutions L"];
28 ("Test.thy",["sqroot-test","univariate","equation","test"],
29 ["Test","squ-equ-test-subpbl1"]);
31 val Script sc = (#scr o get_met) ["Test","squ-equ-test-subpbl1"];
32 (writeln o term2str) sc;
34 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
35 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
36 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
37 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
38 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
40 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
41 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
42 (*("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation"]*)
43 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
44 (*("Specify_Method",Specify_Method ("Test.thy","squ-equ-test-subpbl1"))*)
45 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
46 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","squ-equ-test-subpbl1"*)
47 (*---vvv--- nxt_ here = loc_ below ------------------vvv-------------------*)
48 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
49 (*val f = "x + 1 = 2"; val nxt = Rewrite_Set "norm_equation"*)
50 (*### solve Apply_Method: is = ### nxt_solv1 Apply_Method: store is
55 ??.empty, Safe, true) ########## OK*)
56 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
57 (*val f = "x + 1 + -1 * 2 = 0"; val nxt = Rewrite_Set "Test_simplify"*)
58 (*### locate_gen----------: is= ### next_tac----------------:E =
63 ??.empty, Safe, true) ########## OK von loc_ uebernommen
64 ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
68 [R,L,R,L,L,R,R], SOME e_e,
69 x + 1 + -1 * 2 = 0, Safe, true) ########## OK*)
70 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
73 (*val f = "-1 + x = 0"; val nxt = Subproblem ("Test.thy",[#,#,#])
74 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
75 (*### locate_gen-----------: is= ### next_tac-----------------: E=
79 [R,L,R,L,L,R,R], SOME e_e,
80 x + 1 + -1 * 2 = 0, Safe, true) ########## OK von loc_ uebernommen
81 ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
85 [R,L,R,L,R,R], SOME e_e,
86 -1 + x = 0, Safe, false) ########## OK*)
87 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
88 (*### locate_gen------------: is= ### next_tac-----------------: E=
92 [R,L,R,L,R,R], SOME e_e,
93 -1 + x = 0, Safe, false) ########## OK von loc_ uebernommen
94 ### solve, after locate_gen: is= ### nxt_solv4 Apply_Method: stored is =
98 [R,R,D,L,R], SOME e_e,
99 Subproblem (Test.thy, [linear, univariate, equation, test]), Safe, true)
102 writeln(istate2str (get_istate pt ([3],Frm)));
103 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
104 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
105 (*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
106 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
107 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
108 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
109 (*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * tac*)
110 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
111 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
112 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
113 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
114 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
115 (*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
116 val Script sc = (#scr o get_met) ["Test","solve_linear"];
117 (writeln o term2str) sc;
118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
119 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
120 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
121 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
126 (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
128 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
130 writeln(istate2str (get_istate pt ([3],Res)));
131 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
132 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
134 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
135 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
136 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
137 else error "subp-rooteq.sml: new.behav. in miniscript with mini-subpbl";
140 "---------------- solve_linear as rootpbl -----------------";
141 "---------------- solve_linear as rootpbl -----------------";
142 "---------------- solve_linear as rootpbl -----------------";
143 val fmz = ["equality (1+-1*2+x=0)",
144 "solveFor x","solutions L"];
146 ("Test.thy",["linear","univariate","equation","test"],
147 ["Test","solve_linear"]);
149 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
153 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * tac*)
154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
155 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * tac*)
156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
157 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy") : string * tac*)
158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
159 (*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
160 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
161 (*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
162 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
163 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
164 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
165 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
166 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
168 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
169 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
170 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * tac*)
172 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
173 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)
175 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
176 (*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout
177 val nxt = ("End_Proof'",End_Proof') : string * tac*)
178 val Form' (FormKF (_,EdUndef,0,Nundef,res)) = f;
179 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
180 else error "subp-rooteq.sml: new.behav. in solve_linear as rootpbl";
183 "---------------- solve_plain_square as rootpbl -----------";
184 "---------------- solve_plain_square as rootpbl -----------";
185 "---------------- solve_plain_square as rootpbl -----------";
186 val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
189 ("Test.thy",["plain_square","univariate","equation","test"],
190 ["Test","solve_plain_square"]);
191 (*val p = e_pos'; val c = [];
192 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
193 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
195 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
196 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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
211 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
212 if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
213 else error "subp-rooteq.sml: new.behav. in solve_plain_square as rootpbl";
218 "---------------- root-eq + subpbl: solve_linear ----------";
219 "---------------- root-eq + subpbl: solve_linear ----------";
220 "---------------- root-eq + subpbl: solve_linear ----------";
221 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
222 "solveFor x","solutions L"];
224 ("Test.thy",["sqroot-test","univariate","equation","test"],
225 ["Test","square_equation1"]);
226 (*val p = e_pos'; val c = [];
227 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
228 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
229 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
238 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
239 square_equation_left*)
240 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
241 (*"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"
243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
244 (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"
246 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
247 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"
249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
250 (*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
258 (*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
259 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
261 val nxt =("Subproblem",Subproblem ("Test.thy",["linear","univariate"...*)
262 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
263 (*val nxt =("Model_Problem",Model_Problem ["linear","univariate"...*)
264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
265 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
267 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
268 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
269 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
271 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
276 (*"x = 0 + -1 * -4", nxt Test_simplify*)
277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
278 (*"x = 4", nxt Check_Postcond ["linear","univariate","equation","test"]*)
279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
280 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
282 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
284 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
285 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
286 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_linear";
290 "---------------- root-eq + subpbl: solve_plain_square ----";
291 "---------------- root-eq + subpbl: solve_plain_square ----";
292 "---------------- root-eq + subpbl: solve_plain_square ----";
293 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
294 "solveFor x","solutions L"];
296 ("Test.thy",["sqroot-test","univariate","equation","test"],
297 ["Test","square_equation2"]);
298 val Script sc = (#scr o get_met) ["Test","square_equation2"];
299 (writeln o term2str) sc;
301 (*val p = e_pos'; val c = [];
302 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
303 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
304 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
312 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
313 val (p,_,f,nxt,_,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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
324 (*"9 + -1 * x ^^^ 2 = 0"
325 Subproblem ("Test.thy",["plain_square","univariate","equation"]))*)
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
327 (*Model_Problem ["plain_square","univariate","equation"]*)
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
332 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
333 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
334 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
335 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
336 (*Apply_Method ("Test.thy","solve_plain_square")*)
337 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
338 (*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
339 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
340 (*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)
341 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
342 (*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*)
343 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
344 (*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
345 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
346 (*"x = -3 | x = 3", nxt Or_to_List*)
347 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
349 nxt Check_Postcond ["plain_square","univariate","equation","test"]*)
350 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
354 (*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
356 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
357 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
358 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
359 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
360 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
363 writeln (pr_ptree pr_short pt);
367 val Script s = (#scr o get_met) ["Test","square_equation"];
373 "---------------- root-eq + subpbl: no_met: linear ----";
374 "---------------- root-eq + subpbl: no_met: linear ----";
375 "---------------- root-eq + subpbl: no_met: linear ----";
376 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
377 "solveFor x","solutions L"];
379 ("Test.thy",["squareroot","univariate","equation","test"],
380 ["Test","square_equation"]);
381 (*val p = e_pos'; val c = [];
382 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
383 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
384 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
404 (*"-4 + x = 0", nxt Subproblem ("Test.thy",["univariate","equation"]))*)
405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
406 (*val nxt =("Model_Problem",Model_Problem ["linear","univar...*)
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
411 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
413 (*val nxt = ("Specify_Problem",Specify_Problem ["linear","univariate","equ*)
414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
416 (*Apply_Method ("Test.thy","norm_univar_equation")*)
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
422 if p = ([13],Res) then ()
423 else error ("subp-rooteq.sml: new.behav. in \
424 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
425 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
426 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
427 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
428 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: solve_plain_square";
433 "---------------- root-eq + subpbl: no_met: square ----";
434 "---------------- root-eq + subpbl: no_met: square ----";
435 "---------------- root-eq + subpbl: no_met: square ----";
436 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
437 "solveFor x","solutions L"];
439 ("Test.thy",["squareroot","univariate","equation","test"],
440 ["Test","square_equation"]);
441 val Script sc = (#scr o get_met) ["Test","square_equation"];
442 (writeln o term2str) sc;
444 (*val p = e_pos'; val c = [];
445 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
446 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
447 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
455 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
465 (*Subproblem ("Test.thy",["univariate","equation"]))*)
466 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
467 (*Model_Problem ["plain_square","univariate","equation"]*)
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
472 (*val nxt = ("Specify_Theory",Specify_Theory "Test.thy")*)
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
484 (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*)
485 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
486 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
487 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
488 else error "subp-rooteq.sml: new.behav. in root-eq + subpbl: no_met: square";
492 "---------------- no_met in rootpbl -> linear --------------";
493 "---------------- no_met in rootpbl -> linear --------------";
494 "---------------- no_met in rootpbl -> linear --------------";
495 val fmz = ["equality (1+2*x+3=4*x- 6)",
496 "solveFor x","solutions L"];
498 ("Test.thy",["univariate","equation","test"],
500 (*val p = e_pos'; val c = [];
501 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
502 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
503 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
504 (*val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*)
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 (p,_,f,nxt,_,pt) = me nxt p c pt;
512 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","norm_univar_equation"*)
513 val (p,_,f,nxt,_,pt) = me nxt p c pt;
514 val (p,_,f,nxt,_,pt) = me nxt p c pt;
515 val (p,_,f,nxt,_,pt) = me nxt p c pt;
516 (*val nxt = ("Subproblem",Subproblem ("Test.thy",["univariate","equation"])*)
517 val (p,_,f,nxt,_,pt) = me nxt p c pt;
518 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
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 (p,_,f,nxt,_,pt) = me nxt p c pt;
526 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;
530 (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","equatio*)
531 val (p,_,f,nxt,_,pt) = me nxt p c pt;
532 (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)
533 val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) =
535 if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
536 else error "subp-rooteq.sml: new.behav. in no_met in rootpbl -> linear ---";
539 refine fmz ["univariate","equation","test"];
540 match_pbl fmz (get_pbt ["polynomial","univariate","equation","test"]);