|
1 (* use"../tests/test-root-equ.sml"; |
|
2 use"tests/test-root-equ.sml"; |
|
3 use"test-root-equ.sml"; |
|
4 trace_rewrite:= true; |
|
5 trace_rewrite:= false; |
|
6 |
|
7 method "sqrt-equ-test", _NOT_ "square-equation" |
|
8 *) |
|
9 |
|
10 |
|
11 " ================= equation with x =(-12)/5, but L ={} ======= "; |
|
12 " _________________ rewrite _________________ "; |
|
13 |
|
14 |
|
15 " ================= equation with result={4} ================== "; |
|
16 " -------------- model, specify ------------ "; |
|
17 " ________________ rewrite _________________"; |
|
18 " _________________ rewrite_ x=4_________________ "; |
|
19 " _________________ rewrite + cappend _________________ "; |
|
20 " _________________ me Free_Solve _________________ "; |
|
21 " _________________ me + msteps input _________________ "; |
|
22 (*" _______________ me + nxt_step from script _________---> scriptnew.sml*) |
|
23 (*" _________________ me + nxt_step from script (check_elementwise..)______ |
|
24 ... L_a = Mstep subproblem_equation_dummy; ";*) |
|
25 (*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*) |
|
26 |
|
27 (* |
|
28 > val t = (term_of o the o (parse thy)) "#2^^^#3"; |
|
29 > val eval_fn = the (assoc (!eval_list, "pow")); |
|
30 > val (Some (id,t')) = get_pair thy "pow" eval_fn t; |
|
31 > Sign.string_of_term (sign_of thy) t'; |
|
32 *) |
|
33 (******************************************************************) |
|
34 (* ------------------------------------- *) |
|
35 " _________________ equation with x =(-12)/5, but L ={} ------- "; |
|
36 (* ------------------------------------- *) |
|
37 " _________________ rewrite _________________ "; |
|
38 val thy' = "Test.thy"; |
|
39 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)"; |
|
40 val thm = ("square_equation_left",""); |
|
41 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
|
42 (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*) |
|
43 val rls = ("Test_simplify"); |
|
44 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
45 (*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*) |
|
46 val rls = ("rearrange_assoc"); |
|
47 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
48 (*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*) |
|
49 val rls = ("isolate_root"); |
|
50 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
51 (*"sqrt (x ^^^ 2 + -3 * x) = |
|
52 (-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*) |
|
53 val rls = ("Test_simplify"); |
|
54 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
55 (*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*) |
|
56 val thm = ("square_equation_left",""); |
|
57 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
|
58 val asm = asm union asm'; |
|
59 (*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*) |
|
60 val rls = ("Test_simplify"); |
|
61 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
62 (*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*) |
|
63 val rls = ("norm_equation"); |
|
64 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
65 (*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*) |
|
66 val rls = ("Test_simplify"); |
|
67 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
68 (*"-36 + -15 * x = 0"*) |
|
69 val rls = ("isolate_bdv"); |
|
70 val (ct,_) = the (rewrite_set_inst thy' false |
|
71 [("bdv","x::real")] rls ct); |
|
72 (*"x = (0 + -1 * -36) // -15"*) |
|
73 val rls = ("Test_simplify"); |
|
74 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
75 if ct<>"x = -12 / 5"then raise error "new behaviour in testexample"else (); |
|
76 |
|
77 (* |
|
78 val ct = "x = (-12) / 5" : cterm' |
|
79 > asm; |
|
80 val it = |
|
81 ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x", |
|
82 "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list |
|
83 *) |
|
84 |
|
85 |
|
86 |
|
87 |
|
88 |
|
89 " ================== equation with result={4} ================== "; |
|
90 " ================== equation with result={4} ================== "; |
|
91 " ================== equation with result={4} ================== "; |
|
92 |
|
93 " -------------- model, specify ------------ "; |
|
94 " -------------- model, specify ------------ "; |
|
95 " -------------- model, specify ------------ "; |
|
96 " --- subproblem 1: linear-equation --- "; |
|
97 val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
98 "bound_variable x","error_bound 0"(*, |
|
99 "solutions L::real set" , |
|
100 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)]; |
|
101 val thy = Isac.thy; |
|
102 val formals = map (the o (parse thy)) origin; |
|
103 |
|
104 val given = ["equation (l=(r::real))", |
|
105 "bound_variable bdv", (* TODO type *) |
|
106 "error_bound eps"]; |
|
107 val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.*) |
|
108 "bdv is_var", |
|
109 "eps is_const_expr"]; |
|
110 val find = ["solutions (L::bool list)"]; |
|
111 val with_ = [(* parseold ... |
|
112 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)]; |
|
113 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); |
|
114 val givens = map (the o (parse thy)) given; |
|
115 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}"; |
|
116 (* 31.1.00 |
|
117 val tag__forms = chktyps thy (formals, givens); |
|
118 map ((atomty thy) o term_of) tag__forms; *) |
|
119 |
|
120 " --- subproblem 2: linear-equation --- "; |
|
121 val origin = ["x + 4 = (0::real)","x::real"]; |
|
122 val formals = map (the o (parse thy)) origin; |
|
123 |
|
124 val given = ["equation (l=(0::real))", |
|
125 "bound_variable bdv"]; |
|
126 val where_ = ["l is_linear_in bdv","bdv is_const"]; |
|
127 val find = ["l::real"]; |
|
128 val with_ = ["l = (%x. l) bdv"]; |
|
129 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_); |
|
130 val givens = map (the o (parse thy)) given; |
|
131 |
|
132 val tag__forms = chktyps thy (formals, givens); |
|
133 map ((atomty thy) o term_of) tag__forms; |
|
134 |
|
135 |
|
136 |
|
137 " _________________ rewrite_ x+4_________________ "; |
|
138 " _________________ rewrite_ x+4_________________ "; |
|
139 " _________________ rewrite_ x+4_________________ "; |
|
140 val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
|
141 val thm = num_str square_equation_left; |
|
142 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t); |
|
143 val rls = Test_simplify; |
|
144 val (t,_) = the (rewrite_set_ thy false rls t); |
|
145 val rls = rearrange_assoc; |
|
146 val (t,_) = the (rewrite_set_ thy false rls t); |
|
147 val rls = isolate_root; |
|
148 val (t,_) = the (rewrite_set_ thy false rls t); |
|
149 |
|
150 val rls = Test_simplify; |
|
151 val (t,_) = the (rewrite_set_ thy false rls t); |
|
152 (* |
|
153 sqrt (x ^^^ 2 + 5 * x) = |
|
154 (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2) |
|
155 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
156 ### trying thm 'rdistr_div_right' |
|
157 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
158 (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2) |
|
159 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
160 (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2)) |
|
161 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
162 5 / (-1 * 2) + 2 * x / (-1 * 2) + |
|
163 (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2)) |
|
164 |
|
165 ### trying thm 'radd_left_commute' |
|
166 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
167 -1 * 9 / (-1 * 2) + |
|
168 (5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)) |
|
169 ### trying thm 'radd_assoc' |
|
170 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
171 -1 * 9 / (-1 * 2) + |
|
172 (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))) |
|
173 |
|
174 ### trying thm 'radd_real_const_eq' |
|
175 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
176 -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2)) |
|
177 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
178 -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2) |
|
179 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = |
|
180 (-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2) |
|
181 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ |
|
182 |
|
183 28.8.02: ruleset besser zusammenstellen !!! |
|
184 *) |
|
185 val thm = num_str square_equation_left; |
|
186 val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t); |
|
187 val asm = asm union asm'; |
|
188 val rls = Test_simplify; |
|
189 val (t,_) = the (rewrite_set_ thy false rls t); |
|
190 val rls = norm_equation; |
|
191 val (t,_) = the (rewrite_set_ thy false rls t); |
|
192 val rls = Test_simplify; |
|
193 val (t,_) = the (rewrite_set_ thy false rls t); |
|
194 val rls = isolate_bdv; |
|
195 val subst = [(str2term "bdv", str2term "x")]; |
|
196 val (t,_) = the (rewrite_set_inst_ thy false subst rls t); |
|
197 val rls = Test_simplify; |
|
198 val (t,_) = the (rewrite_set_ thy false rls t); |
|
199 val t' = term2str t; |
|
200 if t' = "x = 4" then () |
|
201 else raise error "root-equ.sml: new behav. in rewrite_ x+4"; |
|
202 |
|
203 " _________________ rewrite x=4_________________ "; |
|
204 " _________________ rewrite x=4_________________ "; |
|
205 " _________________ rewrite x=4_________________ "; |
|
206 (* |
|
207 rewrite thy' "tless_true" "tval_rls" true (num_str rbinom_power_2) ct; |
|
208 atomty thy ((#prop o rep_thm) (!tthm)); |
|
209 atomty thy (term_of (!tct)); |
|
210 *) |
|
211 val thy' = "Test.thy"; |
|
212 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
|
213 (*1*)val thm = ("square_equation_left",""); |
|
214 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
|
215 "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"; |
|
216 (*2*)val rls = "Test_simplify"; |
|
217 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
218 "9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"; |
|
219 (*3*)val rls = "rearrange_assoc"; |
|
220 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
221 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"; |
|
222 (*4*)val rls = "isolate_root"; |
|
223 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
224 "sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"; |
|
225 (*5*)val rls = "Test_simplify"; |
|
226 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
227 "sqrt (x ^^^ 2 + 5 * x) = 2 + x"; |
|
228 (*6*)val thm = ("square_equation_left",""); |
|
229 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
|
230 val asm = asm union asm'; |
|
231 "x ^^^ 2 + 5 * x = (2 + x) ^^^ 2"; |
|
232 (*7*)val rls = "Test_simplify"; |
|
233 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
234 "x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)"; |
|
235 (*8*)val rls = "norm_equation"; |
|
236 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
237 "x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"; |
|
238 (*9*)val rls = "Test_simplify"; |
|
239 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
240 "-4 + x = 0"; |
|
241 (*10*)val rls = "isolate_bdv"; |
|
242 val (ct,_) = the (rewrite_set_inst thy' false |
|
243 [("bdv","x")] rls ct); |
|
244 "x = 0 + -1 * -4"; |
|
245 (*11*)val rls = "Test_simplify"; |
|
246 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
247 if ct="x = 4" then () else raise error "new behaviour in test-example"; |
|
248 |
|
249 |
|
250 |
|
251 |
|
252 " _________________ rewrite + cappend _________________ "; |
|
253 " _________________ rewrite + cappend _________________ "; |
|
254 " _________________ rewrite + cappend _________________ "; |
|
255 val thy' = "Test.thy"; |
|
256 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; |
|
257 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"]; |
|
258 val oris = prep_ori ctl thy ((#ppc o get_pbt) |
|
259 ["sqroot-test","univariate","equation","test"]); |
|
260 val loc = e_istate; |
|
261 val (pt,pos) = (e_ptree,[]); |
|
262 val (pt,_) = cappend_problem pt pos loc (oris,empty_spec); |
|
263 val pt = update_branch pt [] Transitive; |
|
264 (* |
|
265 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt []))); |
|
266 *) |
|
267 (*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *) |
|
268 val pt = update_domID pt [] "Test"; |
|
269 val pt = update_pblID pt [] ["Test", |
|
270 "equations","univariate","square-root"]; |
|
271 val pt = update_metID pt [] ("Test","sqrt-equ-test"); |
|
272 val pt = update_pbl pt [] []; |
|
273 val pt = update_met pt [] []; |
|
274 (* |
|
275 > get_obj g_spec pt []; |
|
276 val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec |
|
277 > val pt = update_domID pt [] "RatArith"; |
|
278 > get_obj g_spec pt []; |
|
279 val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec |
|
280 > val pt = update_pblID pt [] ["RatArith", |
|
281 "equations","univariate","square-root"]; |
|
282 > get_obj g_spec pt []; |
|
283 ("RatArith",["RatArith","equations","univariate","square-root"], |
|
284 ("e_domID","e_metID")) : spec |
|
285 > val pt = update_metID pt [] ("RatArith","sqrt-equ-test"); |
|
286 > get_obj g_spec pt []; |
|
287 ("RatArith",["RatArith","equations","univariate","square-root"], |
|
288 ("RatArith","sqrt-equ-test")) : spec |
|
289 *) |
|
290 |
|
291 val pos = [1]; |
|
292 val (pt,_) = cappend_parent pt pos loc ct (Mstep "repeat") Transitive; |
|
293 |
|
294 val pos = (lev_on o lev_dn) pos; |
|
295 val thm = ("square_equation_left",""); val ctold = ct; |
|
296 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm ct); |
|
297 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep (fst thm)) ct Complete; |
|
298 val pt = union_asm pt [] (map (rpair []) asm); |
|
299 |
|
300 val pos = lev_on pos; |
|
301 val rls = ("Test_simplify"); val ctold = ct; |
|
302 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
303 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
304 |
|
305 val pos = lev_on pos; |
|
306 val rls = ("rearrange_assoc"); val ctold = ct; |
|
307 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
308 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
309 |
|
310 val pos = lev_on pos; |
|
311 val rls = ("isolate_root"); val ctold = ct; |
|
312 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
313 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
314 |
|
315 val pos = lev_on pos; |
|
316 val rls = ("Test_simplify"); val ctold = ct; |
|
317 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
318 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
319 |
|
320 val pos = lev_on pos; |
|
321 val thm = ("square_equation_left",""); val ctold = ct; |
|
322 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); |
|
323 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
324 val pt = union_asm pt [] (map (rpair []) asm); |
|
325 |
|
326 val pos = lev_up pos; |
|
327 val (pt,_) = append_result pt pos e_istate ct Complete; |
|
328 |
|
329 val pos = lev_on pos; |
|
330 val rls = ("Test_simplify"); val ctold = ct; |
|
331 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
332 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
333 |
|
334 val pos = lev_on pos; |
|
335 val rls = ("norm_equation"); val ctold = ct; |
|
336 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
337 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
338 |
|
339 val pos = lev_on pos; |
|
340 val rls = ("Test_simplify"); val ctold = ct; |
|
341 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
342 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
343 |
|
344 (* --- see comments in interface_ME_ISA/instantiate'' |
|
345 val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv"); |
|
346 val (ct,_) = the (rewrite_set thy' false |
|
347 ("#isolate_bdv",rlsdat') ct); *) |
|
348 val pos = lev_on pos; |
|
349 val rls = ("isolate_bdv"); val ctold = ct; |
|
350 val (ct,_) = the (rewrite_set_inst thy' false |
|
351 [("bdv","x")] rls ct); |
|
352 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
353 |
|
354 val pos = lev_on pos; |
|
355 val rls = ("Test_simplify"); val ctold = ct; |
|
356 val (ct,_) = the (rewrite_set thy' false rls ct); |
|
357 val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; |
|
358 |
|
359 val pos = lev_up pos; |
|
360 val (pt,pos) = append_result pt pos e_istate ct Complete; |
|
361 get_obj g_asm pt []; |
|
362 |
|
363 writeln (pr_ptree pr_short pt); |
|
364 (* aus src.24-11-99: |
|
365 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) |
|
366 1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
|
367 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x) |
|
368 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2 |
|
369 1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) ) |
|
370 1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) |
|
371 1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2)) |
|
372 1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x |
|
373 2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2 |
|
374 3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?! |
|
375 4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0) |
|
376 5. (-4) + x = (+0) |
|
377 6. x = (+0) + (-1) * (-4) |
|
378 *) |
|
379 |
|
380 (* |
|
381 val t = (term_of o the o (parse thy)) "solutions (L::real set)"; |
|
382 atomty thy t; |
|
383 *) |
|
384 |
|
385 |
|
386 (*- 20.9.02: Free_Solve would need the erls (for conditions of rules) |
|
387 from thy ???, i.e. together with the *_simplify ?!!!? ---------- |
|
388 " _________________ me Free_Solve _________________ "; |
|
389 " _________________ me Free_Solve _________________ "; |
|
390 " _________________ me Free_Solve _________________ "; |
|
391 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
392 "solveFor x","errorBound (eps=0)", |
|
393 "solutions L"(*, |
|
394 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)]; |
|
395 val (dI',pI',mI') = |
|
396 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
397 ("Test.thy","sqrt-equ-test")); |
|
398 val p = e_pos'; val c = []; |
|
399 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
400 |
|
401 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
402 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*) |
|
403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
404 (* val nxt = ("Add_Given",Add_Given "bound_variable x");*) |
|
405 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
406 (* val nxt = ("Add_Given",Add_Given "error_bound #0");*) |
|
407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
408 (* val nxt = ("Add_Find",Add_Find "solutions L"); *) |
|
409 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
410 (* val nxt = ("Specify_Domain",Specify_Domain "DiffAppl.thy"); |
|
411 > get_obj g_spec pt (fst p); |
|
412 val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*) |
|
413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
414 (*val nxt = ("Specify_Problem", Specify_Problem *) |
|
415 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
416 (*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*) |
|
417 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
418 (*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*) |
|
419 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
420 val nxt = ("Free_Solve",Free_Solve); |
|
421 val (p,_,f,nxt,_,pt) = me nxt p [] pt; |
|
422 get_obj g_spec pt []; |
|
423 |
|
424 "--- -2 ---"; |
|
425 get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt; |
|
426 val (p,_,f,nxt,_,pt)= |
|
427 me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt; |
|
428 (* 15.4. |
|
429 "--- -1 ---"; |
|
430 get_form ("Begin_Trans",Begin_Trans) p pt; |
|
431 val (p,_,f,nxt,_,pt)= |
|
432 me ("Begin_Trans",Begin_Trans) p [4] pt; *) |
|
433 |
|
434 "--- 1 ---"; |
|
435 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt; |
|
436 val (p,_,f,nxt,_,pt)= |
|
437 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt; |
|
438 "--- 2 ---"; |
|
439 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt; |
|
440 val (p,_,f,nxt,_,pt)= |
|
441 me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt; |
|
442 "--- 3 ---"; |
|
443 get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt; |
|
444 val (p,_,f,nxt,_,pt)= |
|
445 me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt; |
|
446 "--- 4 ---"; |
|
447 get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt; |
|
448 val (p,_,f,nxt,_,pt)= |
|
449 me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt; |
|
450 "--- 5 ---"; |
|
451 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
|
452 val (p,_,f,nxt,_,pt)= |
|
453 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt; |
|
454 "--- 6 ---"; |
|
455 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt; |
|
456 val (p,_,f,nxt,_,pt)= |
|
457 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt; |
|
458 (* 15.4. |
|
459 "--- ---"; |
|
460 get_form ("End_Trans",End_Trans) p pt; |
|
461 val (p,_,f,nxt,_,pt)= |
|
462 me ("End_Trans",End_Trans) p [11] pt; *) |
|
463 "--- 7 ---"; |
|
464 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
|
465 val (p,_,f,nxt,_,pt)= |
|
466 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt; |
|
467 "--- 8 ---"; |
|
468 get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt; |
|
469 val (p,_,f,nxt,_,pt)= |
|
470 me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt; |
|
471 "--- 9 ---"; |
|
472 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
|
473 val (p,_,f,nxt,_,pt)= |
|
474 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt; |
|
475 "--- 10 ---."; |
|
476 get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt; |
|
477 val (p,_,f,nxt,_,pt)= |
|
478 me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt; |
|
479 "--- 11 ---"; |
|
480 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; |
|
481 val ((p,p_),_,f,nxt,_,pt)= |
|
482 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt; |
|
483 (* 5.4.00.: --- |
|
484 get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt; |
|
485 val (p,_,f,nxt,_,pt)= |
|
486 me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt; |
|
487 --- *) |
|
488 writeln (pr_ptree pr_short pt); |
|
489 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; |
|
490 *) |
|
491 |
|
492 |
|
493 " _________________ me + msteps input _________________ "; |
|
494 " _________________ me + msteps input _________________ "; |
|
495 " _________________ me + msteps input _________________ "; |
|
496 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", |
|
497 "solveFor x","errorBound (eps=0)", |
|
498 "solutions L"]; |
|
499 val (dI',pI',mI') = |
|
500 ("Test.thy",["sqroot-test","univariate","equation","test"], |
|
501 ("Test.thy","sqrt-equ-test")); |
|
502 val p = e_pos'; val c = []; |
|
503 "--- s1 ---"; |
|
504 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); |
|
505 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; |
|
506 "--- s2 ---"; |
|
507 val nxt = ("Add_Given", |
|
508 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); |
|
509 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
510 "--- s3 ---"; |
|
511 val nxt = ("Add_Given",Add_Given "solveFor x"); |
|
512 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
513 "--- s4 ---"; |
|
514 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)"); |
|
515 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
516 "--- s5 ---"; |
|
517 val nxt = ("Add_Find",Add_Find "solutions L"); |
|
518 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
519 "--- s6 ---"; |
|
520 val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); |
|
521 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
522 "--- s7 ---"; |
|
523 val nxt = ("Specify_Problem", |
|
524 Specify_Problem ["sqroot-test","univariate","equation","test"]); |
|
525 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
526 "--- s8 ---"; |
|
527 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); |
|
528 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
529 "--- s9 ---"; |
|
530 val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test")); |
|
531 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
532 "--- 1 ---"; |
|
533 val nxt = ("Rewrite",Rewrite ("square_equation_left","")); |
|
534 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
535 |
|
536 (*me------------ |
|
537 val (mI,m) = nxt; val pos' as (p,p_) = p; |
|
538 |
|
539 val Appl m = applicable_in (p,p_) pt m; |
|
540 (*solve*) |
|
541 val pp = par_pblobj pt p; |
|
542 val metID = get_obj g_metID pt pp; |
|
543 val sc = (#scr o get_met) metID; |
|
544 val is = get_istate pt (p,p_); |
|
545 val thy' = get_obj g_domID pt pp; |
|
546 val thy = assoc_thy thy'; |
|
547 val d = e_rls; |
|
548 val Steps [(m',f',pt',p',c',s')] = |
|
549 locate_gen thy' m (pt,(p,p_)) (sc,d) is; |
|
550 val is' = get_istate pt' p'; |
|
551 next_tac thy' (pt'(*'*),p') sc is'; |
|
552 |
|
553 |
|
554 |
|
555 |
|
556 val ttt = (term_of o the o (parse Test.thy)) |
|
557 "Let (((While contains_root e_ Do\ |
|
558 \Rewrite square_equation_left True @@\ |
|
559 \Try (Rewrite_Set Test_simplify False) @@\ |
|
560 \Try (Rewrite_Set rearrange_assoc False) @@\ |
|
561 \Try (Rewrite_Set Test_simplify False)) @@\ |
|
562 \Try (Rewrite_Set norm_equation False) @@\ |
|
563 \Try (Rewrite_Set Test_simplify False) @@\ |
|
564 \Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False @@\ |
|
565 \Try (Rewrite_Set Test_simplify False))\ |
|
566 \e_)"; |
|
567 |
|
568 -------------------------*) |
|
569 |
|
570 |
|
571 "--- 2 ---"; |
|
572 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
573 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
574 "--- 3 ---"; |
|
575 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); |
|
576 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
577 "--- 4 ---"; |
|
578 val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root"); |
|
579 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
580 "--- 5 ---"; |
|
581 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
582 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
583 "--- 6 ---"; |
|
584 val nxt = ("Rewrite",Rewrite ("square_equation_left","")); |
|
585 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
586 "--- 7 ---"; |
|
587 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
588 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
589 "--- 8<> ---"; |
|
590 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); |
|
591 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
592 "--- 9<> ---"; |
|
593 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
594 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
595 "--- 10<> ---"; |
|
596 val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation"); |
|
597 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
598 "--- 11<> ---."; |
|
599 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
600 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
601 "--- 12<> ---"; |
|
602 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")); |
|
603 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
604 "--- 13<> ---"; |
|
605 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); |
|
606 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
607 "--- 1<> ---"; |
|
608 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]); |
|
609 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
|
610 (* val nxt = ("End_Proof'",End_Proof');*) |
|
611 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
|
612 then raise error "me + msteps input: not finished correctly" |
|
613 else "root-equation, me + msteps input: OK"; |
|
614 |
|
615 writeln (pr_ptree pr_short pt); |
|
616 writeln("result: "^(get_obj g_result pt [])^ |
|
617 "\n=============================================================="); |
|
618 |
|
619 |
|
620 |