|
1 (* use"tests/subp-rooteq.sml"; |
|
2 use"subp-rooteq.sml"; |
|
3 *) |
|
4 |
|
5 |
|
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 |
|
15 |
|
16 |
|
17 |
|
18 |
|
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)", |
|
24 "solutions L"]; |
|
25 val (dI',pI',mI') = |
|
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; |
|
30 |
|
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; |
|
54 p; |
|
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")*) |
|
65 |
|
66 |
|
67 (*-----30.9.02----------------------------------------------*) |
|
68 |
|
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; |
|
84 p; |
|
85 writeln(istate2str (get_istate pt ([3],Res))); |
|
86 |
|
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"; |
|
93 |
|
94 |
|
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"]; |
|
100 val (dI',pI',mI') = |
|
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"; |
|
133 |
|
134 |
|
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", |
|
139 "solutions L"]; |
|
140 val (dI',pI',mI') = |
|
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; |
|
146 |
|
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"; |
|
163 |
|
164 |
|
165 |
|
166 |
|
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)", |
|
172 "solutions L"]; |
|
173 val (dI',pI',mI') = |
|
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" |
|
191 Test_simplify*) |
|
192 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
193 (*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))" |
|
194 rearrange_assoc*) |
|
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
196 (*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)" |
|
197 isolate_root*) |
|
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)" |
|
200 Test_simplify*) |
|
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; |
|
209 (*"-4 + x = 0" |
|
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"; |
|
235 |
|
236 |
|
237 |
|
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)", |
|
243 "solutions L"]; |
|
244 val (dI',pI',mI') = |
|
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; |
|
249 |
|
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) = |
|
262 |
|
263 me nxt p [1] 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; |
|
296 (*"[x = -3, x = 3]", |
|
297 nxt Check_Postcond ["plain_square","univariate","equation","test"]*) |
|
298 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
299 |
|
300 |
|
301 |
|
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"; |
|
309 |
|
310 |
|
311 writeln (pr_ptree pr_short pt); |
|
312 |
|
313 |
|
314 |
|
315 val Script s = (#scr o get_met) ("Test.thy","square_equation"); |
|
316 atomt s; |
|
317 |
|
318 |
|
319 |
|
320 |
|
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)", |
|
326 "solutions L"]; |
|
327 val (dI',pI',mI') = |
|
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"; |
|
379 |
|
380 |
|
381 |
|
382 |
|
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)", |
|
388 "solutions L"]; |
|
389 val (dI',pI',mI') = |
|
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; |
|
394 |
|
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"; |
|
441 |
|
442 |
|
443 |
|
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"]; |
|
449 val (dI',pI',mI') = |
|
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,_,_) = |
|
489 me nxt p [1] pt; |
|
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 ---"; |
|
492 |