1 (* use"tests/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 --------------";
19 "---------------- miniscript with mini-subpbl -------------";
20 "---------------- miniscript with mini-subpbl -------------";
21 "---------------- miniscript with mini-subpbl -------------";
22 val fmz = ["equality (x+1=2)",
23 "solveFor x","errorBound (eps=0)",
26 ("Test.thy",["sqroot-test","univariate","equation","test"],
27 ("Test.thy","squ-equ-test-subpbl1"));
28 val Script sc = (#scr o get_met) ("Test.thy","squ-equ-test-subpbl1");
29 (writeln o term2str) sc;
31 val p = e_pos'; val c = [];
32 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
33 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
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 * mstep*)
38 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
39 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*)
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.thy","squ-equ-test-subpbl1"))*)
44 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
45 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","squ-equ-test-subpbl1"*)
46 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
47 (*val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation") : string * mstep*)
48 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
49 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
50 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
51 (*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep
52 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
53 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
55 writeln(istate2str (get_istate pt ([3],Frm)));
56 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
57 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
58 (*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *)
59 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
60 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep*)
61 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
62 (*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * mstep*)
63 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
64 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
67 (*-----30.9.02----------------------------------------------*)
69 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
70 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
71 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
72 (*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
73 val Script sc = (#scr o get_met) ("Test.thy","solve_linear");
74 (writeln o term2str) sc;
75 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
76 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
77 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
78 (*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
79 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
80 (*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*)
81 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
82 (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*)
83 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
85 writeln(istate2str (get_istate pt ([3],Res)));
87 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
88 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
89 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
90 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
91 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
92 else raise error "new behaviour in test: miniscript with mini-subpbl";
95 "---------------- solve_linear as rootpbl -----------------";
96 "---------------- solve_linear as rootpbl -----------------";
97 "---------------- solve_linear as rootpbl -----------------";
98 val fmz = ["equality (1+-1*2+x=0)",
99 "solveFor x","solutions L"];
101 ("Test.thy",["linear","univariate","equation","test"],
102 ("Test.thy","solve_linear"));
103 val p = e_pos'; val c = [];
104 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
105 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
106 (*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*)
107 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
108 (*val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep*)
109 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
110 (*val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep*)
111 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
112 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*)
113 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
114 (*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*)
115 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
116 (*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*)
117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
118 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
119 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
120 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0"))
121 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*)
122 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
123 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)"))
124 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * mstep*)
125 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
126 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*)
127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
128 (*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout
129 val nxt = ("End_Proof'",End_Proof') : string * mstep*)
130 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
131 if (snd nxt)=End_Proof' andalso res="[x = 1]" then ()
132 else raise error "new behaviour in test: solve_linear as rootpbl";
135 "---------------- solve_plain_square as rootpbl -----------";
136 "---------------- solve_plain_square as rootpbl -----------";
137 "---------------- solve_plain_square as rootpbl -----------";
138 val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x",
141 ("Test.thy",["plain_square","univariate","equation","test"],
142 ("Test.thy","solve_plain_square"));
143 val p = e_pos'; val c = [];
144 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
145 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
147 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
148 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
149 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
150 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
151 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
152 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
153 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
154 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
155 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
156 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
157 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
158 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
159 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
160 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
161 if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then ()
162 else raise error "new behaviour in test: solve_plain_square as rootpbl";
167 "---------------- root-eq + subpbl: solve_linear ----------";
168 "---------------- root-eq + subpbl: solve_linear ----------";
169 "---------------- root-eq + subpbl: solve_linear ----------";
170 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
171 "solveFor x","errorBound (eps=0)",
174 ("Test.thy",["sqroot-test","univariate","equation","test"],
175 ("Test.thy","square_equation1"));
176 val p = e_pos'; val c = [];
177 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
178 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
179 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
180 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
181 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
182 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
183 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
184 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
185 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
186 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
187 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"
188 square_equation_left*)
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 (*"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
193 (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
196 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
199 (*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)"
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 (*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*)
208 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
210 val nxt =("Subproblem",Subproblem ("Test.thy",["linear","univariate"...*)
211 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
212 (*val nxt =("Model_Problem",Model_Problem ["linear","univariate"...*)
213 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
214 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
215 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
216 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
217 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
218 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
219 (*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*)
220 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
221 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
222 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
224 (*"x = 0 + -1 * -4", nxt Test_simplify*)
225 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
226 (*"x = 4", nxt Check_Postcond ["linear","univariate","equation","test"]*)
227 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
228 (*"[x = 4]", nxt Check_elementwise "Assumptions"*)
229 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
230 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
231 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
232 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
233 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
234 else raise error "new behaviour in test: root-eq + subpbl: solve_linear";
238 "---------------- root-eq + subpbl: solve_plain_square ----";
239 "---------------- root-eq + subpbl: solve_plain_square ----";
240 "---------------- root-eq + subpbl: solve_plain_square ----";
241 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
242 "solveFor x","errorBound (eps=0)",
245 ("Test.thy",["sqroot-test","univariate","equation","test"],
246 ("Test.thy","square_equation2"));
247 val Script sc = (#scr o get_met) ("Test.thy","square_equation2");
248 (writeln o term2str) sc;
250 val p = e_pos'; val c = [];
251 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
252 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
259 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
260 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
261 val (p,_,f,nxt,_,pt) =
264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
265 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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
269 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
271 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
272 (*"9 + -1 * x ^^^ 2 = 0"
273 Subproblem ("Test.thy",["plain_square","univariate","equation"]))*)
274 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
275 (*Model_Problem ["plain_square","univariate","equation"]*)
276 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
277 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
278 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
280 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
281 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
282 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
283 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
284 (*Apply_Method ("Test.thy","solve_plain_square")*)
285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
286 (*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*)
287 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
288 (*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*)
289 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
290 (*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*)
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
292 (*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*)
293 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
294 (*"x = -3 | x = 3", nxt Or_to_List*)
295 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
297 nxt Check_Postcond ["plain_square","univariate","equation","test"]*)
298 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
302 (*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*)
303 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
304 (*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*)
305 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
306 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
307 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
308 else raise error "new behaviour in test: root-eq + subpbl: solve_plain_square";
311 writeln (pr_ptree pr_short pt);
315 val Script s = (#scr o get_met) ("Test.thy","square_equation");
321 "---------------- root-eq + subpbl: no_met: linear ----";
322 "---------------- root-eq + subpbl: no_met: linear ----";
323 "---------------- root-eq + subpbl: no_met: linear ----";
324 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
325 "solveFor x","errorBound (eps=0)",
328 ("Test.thy",["squareroot","univariate","equation","test"],
329 ("Test.thy","square_equation"));
330 val p = e_pos'; val c = [];
331 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
332 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
337 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
339 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
340 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
341 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
342 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
343 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
344 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
345 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
346 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
347 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
348 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
349 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
350 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
351 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
352 (*"-4 + x = 0", nxt Subproblem ("Test.thy",["univariate","equation"]))*)
353 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
354 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
356 (*val nxt =("Model_Problem",Model_Problem ["linear","univar...*)
357 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
358 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
359 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
360 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
361 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
362 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
363 (*val nxt = ("Specify_Problem",Specify_Problem ["linear","univariate","equ*)
364 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
365 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
366 (*Apply_Method ("Test.thy","norm_univar_equation")*)
367 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
368 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
369 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
370 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
371 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
372 if p = ([13],Res) then ()
373 else raise error ("new behaviour in test: \
374 \root-eq + subpbl: solve_linear, p ="^(pos'2str p));
375 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
376 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
377 if (snd nxt)=End_Proof' andalso res="[x = 4]" then ()
378 else raise error "new behaviour in test: root-eq + subpbl: solve_plain_square";
383 "---------------- root-eq + subpbl: no_met: square ----";
384 "---------------- root-eq + subpbl: no_met: square ----";
385 "---------------- root-eq + subpbl: no_met: square ----";
386 val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)",
387 "solveFor x","errorBound (eps=0)",
390 ("Test.thy",["squareroot","univariate","equation","test"],
391 ("Test.thy","square_equation"));
392 val Script sc = (#scr o get_met) ("Test.thy","square_equation");
393 (writeln o term2str) sc;
395 val p = e_pos'; val c = [];
396 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
397 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
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 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
405 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*)
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 (p,_,f,nxt,_,pt) = me nxt p [1] pt;
411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
415 (*Subproblem ("Test.thy",["univariate","equation"]))*)
416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
417 (*("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
419 (*Model_Problem ["plain_square","univariate","equation"]*)
420 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
421 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
422 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
423 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
424 (*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*)
425 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
426 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
427 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
428 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
429 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
430 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
431 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
432 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
433 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
434 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
435 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
436 (*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*)
437 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
438 val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f;
439 if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then ()
440 else raise error "new behaviour in test: root-eq + subpbl: no_met: square";
444 "---------------- no_met in rootpbl -> linear --------------";
445 "---------------- no_met in rootpbl -> linear --------------";
446 "---------------- no_met in rootpbl -> linear --------------";
447 val fmz = ["equality (1+2*x+3=4*x- 6)",
448 "solveFor x","solutions L"];
450 ("Test.thy",["univariate","equation","test"],
451 ("Test.thy","no_met"));
452 val p = e_pos'; val c = [];
453 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
454 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
455 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
456 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
457 (*val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*)
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 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","norm_univar_equation"*)
466 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
467 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
468 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
469 (*val nxt = ("Subproblem",Subproblem ("Test.thy",["univariate","equation"])*)
470 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
471 (*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
472 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
473 (*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*)
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 nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*)
482 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
483 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
484 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
485 (*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","equatio*)
486 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
487 (*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*)
488 val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) =
490 if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then ()
491 else raise error "new behaviour in test: no_met in rootpbl -> linear ---";