1 (* use"../tests/test-root-equ.sml";
2 use"tests/test-root-equ.sml";
3 use"test-root-equ.sml";
7 method "sqrt-equ-test", _NOT_ "square-equation"
11 " ================= equation with x =(-12)/5, but L ={} ======= ";
12 " _________________ rewrite _________________ ";
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*)
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';
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 ();
78 val ct = "x = (-12) / 5" : cterm'
81 ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
82 "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list
89 " ================== equation with result={4} ================== ";
90 " ================== equation with result={4} ================== ";
91 " ================== equation with result={4} ================== ";
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}"*)];
102 val formals = map (the o (parse thy)) origin;
104 val given = ["equation (l=(r::real))",
105 "bound_variable bdv", (* TODO type *)
107 val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.*)
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}";
117 val tag__forms = chktyps thy (formals, givens);
118 map ((atomty thy) o term_of) tag__forms; *)
120 " --- subproblem 2: linear-equation --- ";
121 val origin = ["x + 4 = (0::real)","x::real"];
122 val formals = map (the o (parse thy)) origin;
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;
132 val tag__forms = chktyps thy (formals, givens);
133 map ((atomty thy) o term_of) tag__forms;
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);
150 val rls = Test_simplify;
151 val (t,_) = the (rewrite_set_ thy false rls t);
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))
165 ### trying thm 'radd_left_commute'
166 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
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) =
172 (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
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 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
183 28.8.02: ruleset besser zusammenstellen !!!
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);
200 if t' = "x = 4" then ()
201 else raise error "root-equ.sml: new behav. in rewrite_ x+4";
203 " _________________ rewrite x=4_________________ ";
204 " _________________ rewrite x=4_________________ ";
205 " _________________ rewrite x=4_________________ ";
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));
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);
241 (*10*)val rls = "isolate_bdv";
242 val (ct,_) = the (rewrite_set_inst thy' false
243 [("bdv","x")] rls ct);
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";
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"]);
261 val (pt,pos) = (e_ptree,[]);
262 val (pt,_) = cappend_problem pt pos loc (oris,empty_spec);
263 val pt = update_branch pt [] Transitive;
265 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
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 [] [];
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
292 val (pt,_) = cappend_parent pt pos loc ct (Mstep "repeat") Transitive;
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);
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;
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;
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;
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;
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);
326 val pos = lev_up pos;
327 val (pt,_) = append_result pt pos e_istate ct Complete;
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;
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;
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;
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;
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;
359 val pos = lev_up pos;
360 val (pt,pos) = append_result pt pos e_istate ct Complete;
363 writeln (pr_ptree pr_short pt);
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)
377 6. x = (+0) + (-1) * (-4)
381 val t = (term_of o the o (parse thy)) "solutions (L::real set)";
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)",
394 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
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')));
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 [];
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;
430 get_form ("Begin_Trans",Begin_Trans) p pt;
431 val (p,_,f,nxt,_,pt)=
432 me ("Begin_Trans",Begin_Trans) p [4] pt; *)
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;
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;
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;
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;
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;
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;
460 get_form ("End_Trans",End_Trans) p pt;
461 val (p,_,f,nxt,_,pt)=
462 me ("End_Trans",End_Trans) p [11] pt; *)
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;
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;
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;
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;
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;
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;
488 writeln (pr_ptree pr_short pt);
489 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
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)",
500 ("Test.thy",["sqroot-test","univariate","equation","test"],
501 ("Test.thy","sqrt-equ-test"));
502 val p = e_pos'; val c = [];
504 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
505 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
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;
511 val nxt = ("Add_Given",Add_Given "solveFor x");
512 val (p,_,f,nxt,_,pt) = me nxt p c pt;
514 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
515 val (p,_,f,nxt,_,pt) = me nxt p c pt;
517 val nxt = ("Add_Find",Add_Find "solutions L");
518 val (p,_,f,nxt,_,pt) = me nxt p c pt;
520 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
523 val nxt = ("Specify_Problem",
524 Specify_Problem ["sqroot-test","univariate","equation","test"]);
525 val (p,_,f,nxt,_,pt) = me nxt p c pt;
527 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;
530 val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));
531 val (p,_,f,nxt,_,pt) = me nxt p c pt;
533 val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
534 val (p,_,f,nxt,_,pt) = me nxt p c pt;
537 val (mI,m) = nxt; val pos' as (p,p_) = p;
539 val Appl m = applicable_in (p,p_) pt m;
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';
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';
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))\
568 -------------------------*)
572 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
573 val (p,_,f,nxt,_,pt) = me nxt p c pt;
575 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
576 val (p,_,f,nxt,_,pt) = me nxt p c pt;
578 val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
579 val (p,_,f,nxt,_,pt) = me nxt p c pt;
581 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
582 val (p,_,f,nxt,_,pt) = me nxt p c pt;
584 val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
585 val (p,_,f,nxt,_,pt) = me nxt p c pt;
587 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
588 val (p,_,f,nxt,_,pt) = me nxt p c pt;
590 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
591 val (p,_,f,nxt,_,pt) = me nxt p c pt;
593 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
594 val (p,_,f,nxt,_,pt) = me nxt p c pt;
596 val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
597 val (p,_,f,nxt,_,pt) = me nxt p c pt;
599 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
600 val (p,_,f,nxt,_,pt) = me nxt p c pt;
602 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));
603 val (p,_,f,nxt,_,pt) = me nxt p c pt;
605 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
606 val (p,_,f,nxt,_,pt) = me nxt p c pt;
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";
615 writeln (pr_ptree pr_short pt);
616 writeln("result: "^(get_obj g_result pt [])^
617 "\n==============================================================");