1 (* Rewrite.trace_on:= true;
2 Rewrite.trace_on:= false;
4 method "sqrt-equ-test", _NOT_ "square-equation"
8 " ================= equation with x =(-12)/5, but L ={} ======= ";
9 " _________________ rewrite _________________ ";
12 " ================= equation with result={4} ================== ";
13 " -------------- model, specify ------------ ";
14 " ________________ rewrite _________________";
15 " _________________ rewrite_ x=4_________________ ";
16 " _________________ rewrite + cappend _________________ ";
17 " _________________ me Free_Solve _________________ ";
18 " _________________ me + tacs input _________________ ";
19 (*" _______________ me + nxt_step from script _________---> scriptnew.sml*)
20 (*" _________________ me + nxt_step from script (check_elementwise..)______
21 ... L_a = Tac subproblem_equation_dummy; ";*)
22 (*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*)
30 > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
31 > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
32 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
33 > Syntax.string_of_term (ThyC.to_ctxt thy) t';
35 (******************************************************************)
36 (* ------------------------------------- *)
37 " _________________ equation with x =(-12)/5, but L ={} ------- ";
38 (* ------------------------------------- *)
39 " _________________ rewrite _________________ ";
41 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
42 val thm = ("square_equation_left","");
43 val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
44 (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)
45 val rls = ("Test_simplify");
46 val (ct,_) = the (rewrite_set thy' false rls ct);
47 (*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*)
48 val rls = ("rearrange_assoc");
49 val (ct,_) = the (rewrite_set thy' false rls ct);
50 (*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*)
51 val rls = ("isolate_root");
52 val (ct,_) = the (rewrite_set thy' false rls ct);
53 (*"sqrt (x ^^^ 2 + -3 * x) =
54 (-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
55 val rls = ("Test_simplify");
56 val (ct,_) = the (rewrite_set thy' false rls ct);
57 (*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)
58 val thm = ("square_equation_left","");
59 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
60 val asm = asm union asm';
61 (*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)
62 val rls = ("Test_simplify");
63 val (ct,_) = the (rewrite_set thy' false rls ct);
64 (*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*)
65 val rls = ("norm_equation");
66 val (ct,_) = the (rewrite_set thy' false rls ct);
67 (*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*)
68 val rls = ("Test_simplify");
69 val (ct,_) = the (rewrite_set thy' false rls ct);
70 (*"-36 + -15 * x = 0"*)
71 val rls = ("isolate_bdv");
72 val (ct,_) = the (rewrite_set_inst thy' false
73 [("bdv","x::real")] rls ct);
74 (*"x = (0 + -1 * -36) // -15"*)
75 val rls = ("Test_simplify");
76 val (ct,_) = the (rewrite_set thy' false rls ct);
77 if ct<>"x = -12 / 5"then error "new behaviour in testexample"else ();
80 val ct = "x = (-12) / 5" : TermC.as_string
83 ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
84 "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : TermC.as_string list
91 " ================== equation with result={4} ================== ";
92 " ================== equation with result={4} ================== ";
93 " ================== equation with result={4} ================== ";
95 " -------------- model, specify ------------ ";
96 " -------------- model, specify ------------ ";
97 " -------------- model, specify ------------ ";
98 " --- subproblem 1: linear-equation --- ";
99 val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
100 "bound_variable x","error_bound 0"(*,
101 "solutions L::real set" ,
102 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
103 val thy = (theory "Isac_Knowledge");
104 val formals = map (the o (parse thy)) origin;
106 val given = ["equation (l=(r::real))",
107 "bound_variable bdv", (* TODO type *)
109 val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.yy*)
111 "eps is_const_expr"];
112 val find = ["solutions (L::bool list)"];
113 val with_ = [(* parseold ...
114 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
115 val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
116 val givens = map (the o (parse thy)) given;
117 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
119 val tag__forms = chktyps thy (formals, givens);
120 map ((atomty) o Thm.term_of) tag__forms; *)
122 " --- subproblem 2: linear-equation --- ";
123 val origin = ["x + 4 = (0::real)","x::real"];
124 val formals = map (the o (parse thy)) origin;
126 val given = ["equation (l=(0::real))",
127 "bound_variable bdv"];
128 val where_ = ["l is_linear_in bdv","bdv is_const"];
129 val find = ["l::real"];
130 val with_ = ["l = (%x. l) bdv"];
131 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
132 val givens = map (the o (parse thy)) given;
134 val tag__forms = chktyps thy (formals, givens);
135 map ((atomty) o Thm.term_of) tag__forms;
139 " _________________ rewrite_ x+4_________________ ";
140 " _________________ rewrite_ x+4_________________ ";
141 " _________________ rewrite_ x+4_________________ ";
142 val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
143 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
144 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
145 val rls = Test_simplify;
146 val (t,_) = the (rewrite_set_ thy false rls t);
147 val rls = rearrange_assoc;
148 val (t,_) = the (rewrite_set_ thy false rls t);
149 val rls = isolate_root;
150 val (t,_) = the (rewrite_set_ thy false rls t);
152 val rls = Test_simplify;
153 val (t,_) = the (rewrite_set_ thy false rls t);
155 sqrt (x ^^^ 2 + 5 * x) =
156 (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
157 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
158 ### trying thm 'rdistr_div_right'
159 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
160 (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
161 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
162 (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
163 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
164 5 / (-1 * 2) + 2 * x / (-1 * 2) +
165 (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
167 ### trying thm 'radd_left_commute'
168 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
170 (5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
171 ### trying thm 'radd_assoc'
172 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
174 (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
176 ### trying thm 'radd_real_const_eq'
177 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
178 -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
179 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
180 -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
181 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
182 (-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
185 28.8.02: ruleset besser zusammenstellen !!!
187 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
188 val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
189 val asm = asm union asm';
190 val rls = Test_simplify;
191 val (t,_) = the (rewrite_set_ thy false rls t);
192 val rls = norm_equation;
193 val (t,_) = the (rewrite_set_ thy false rls t);
194 val rls = Test_simplify;
195 val (t,_) = the (rewrite_set_ thy false rls t);
196 val rls = isolate_bdv;
197 val subst = [(str2term "bdv", str2term "x")];
198 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
199 val rls = Test_simplify;
200 val (t,_) = the (rewrite_set_ thy false rls t);
201 val t' = UnparseC.term t;
202 if t' = "x = 4" then ()
203 else error "root-equ.sml: new behav. in rewrite_ x+4";
205 " _________________ rewrite x=4_________________ ";
206 " _________________ rewrite x=4_________________ ";
207 " _________________ rewrite x=4_________________ ";
209 rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
210 atomty ((#prop o Thm.rep_thm) (!tthm));
211 atomty (Thm.term_of (!tct));
214 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
215 (*1*)val thm = ("square_equation_left","");
216 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
217 "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
218 (*2*)val rls = "Test_simplify";
219 val (ct,_) = the (rewrite_set thy' false rls ct);
220 "9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";
221 (*3*)val rls = "rearrange_assoc";
222 val (ct,_) = the (rewrite_set thy' false rls ct);
223 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";
224 (*4*)val rls = "isolate_root";
225 val (ct,_) = the (rewrite_set thy' false rls ct);
226 "sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
227 (*5*)val rls = "Test_simplify";
228 val (ct,_) = the (rewrite_set thy' false rls ct);
229 "sqrt (x ^^^ 2 + 5 * x) = 2 + x";
230 (*6*)val thm = ("square_equation_left","");
231 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
232 val asm = asm union asm';
233 "x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
234 (*7*)val rls = "Test_simplify";
235 val (ct,_) = the (rewrite_set thy' false rls ct);
236 "x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";
237 (*8*)val rls = "norm_equation";
238 val (ct,_) = the (rewrite_set thy' false rls ct);
239 "x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";
240 (*9*)val rls = "Test_simplify";
241 val (ct,_) = the (rewrite_set thy' false rls ct);
243 (*10*)val rls = "isolate_bdv";
244 val (ct,_) = the (rewrite_set_inst thy' false
245 [("bdv","x")] rls ct);
247 (*11*)val rls = "Test_simplify";
248 val (ct,_) = the (rewrite_set thy' false rls ct);
249 if ct="x = 4" then () else error "new behaviour in test-example";
254 " _________________ rewrite + cappend _________________ ";
255 " _________________ rewrite + cappend _________________ ";
256 " _________________ rewrite + cappend _________________ ";
258 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
259 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
260 val oris = O_Model.init ctl thy
262 ["sqroot-test","univariate","equation","test"]);
263 val loc = Istate.empty;
264 val (pt,pos) = (e_ctree,[]);
265 val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)
266 val pt = update_branch pt [] TransitiveB;
268 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
270 (*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
271 val pt = update_domID pt [] "Test";
272 val pt = update_pblID pt [] ["Test",
273 "equations","univariate","square-root"];
274 val pt = update_metID pt [] ["Test","sqrt-equ-test"];
275 val pt = update_pbl pt [] [];
276 val pt = update_met pt [] [];
278 > get_obj g_spec pt [];
279 val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec
280 > val pt = update_domID pt [] "RatArith";
281 > get_obj g_spec pt [];
282 val it = ("RatArith",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec
283 > val pt = update_pblID pt [] ["RatArith",
284 "equations","univariate","square-root"];
285 > get_obj g_spec pt [];
286 ("RatArith",["RatArith","equations","univariate","square-root"],
287 ("empty_thy_id","empty_meth_id")) : spec
288 > val pt = update_metID pt [] ("RatArith","sqrt-equ-test");
289 > get_obj g_spec pt [];
290 ("RatArith",["RatArith","equations","univariate","square-root"],
291 ("RatArith","sqrt-equ-test")) : spec
296 val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
298 val pos = (lev_on o lev_dn) pos;
299 val thm = ("square_equation_left",""); val ctold = ct;
300 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
301 val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
302 (*val pt = union_asm pt [] (map (rpair []) asm);*)
304 val pos = lev_on pos;
305 val rls = ("Test_simplify"); val ctold = str2term ct;
306 val (ct,_) = the (rewrite_set thy' false rls ct);
307 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
309 val pos = lev_on pos;
310 val rls = ("rearrange_assoc"); val ctold = str2term ct;
311 val (ct,_) = the (rewrite_set thy' false rls ct);
312 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
314 val pos = lev_on pos;
315 val rls = ("isolate_root"); val ctold = str2term ct;
316 val (ct,_) = the (rewrite_set thy' false rls ct);
317 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
319 val pos = lev_on pos;
320 val rls = ("Test_simplify"); val ctold = str2term ct;
321 val (ct,_) = the (rewrite_set thy' false rls ct);
322 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
324 val pos = lev_on pos;
325 val thm = ("square_equation_left",""); val ctold = str2term ct;
326 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
327 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
328 (*val pt = union_asm pt [] (map (rpair []) asm);*)
330 val pos = lev_up pos;
331 val (pt,_) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
333 val pos = lev_on pos;
334 val rls = ("Test_simplify"); val ctold = str2term ct;
335 val (ct,_) = the (rewrite_set thy' false rls ct);
336 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
338 val pos = lev_on pos;
339 val rls = ("norm_equation"); val ctold = str2term ct;
340 val (ct,_) = the (rewrite_set thy' false rls ct);
341 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
343 val pos = lev_on pos;
344 val rls = ("Test_simplify"); val ctold = str2term ct;
345 val (ct,_) = the (rewrite_set thy' false rls ct);
346 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
348 (* --- see comments in interface_ME_ISA/instantiate''
349 val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv");
350 val (ct,_) = the (rewrite_set thy' false
351 ("#isolate_bdv",rlsdat') ct); *)
352 val pos = lev_on pos;
353 val rls = ("isolate_bdv"); val ctold = str2term ct;
354 val (ct,_) = the (rewrite_set_inst thy' false
355 [("bdv","x")] rls ct);
356 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
358 val pos = lev_on pos;
359 val rls = ("Test_simplify"); val ctold = str2term ct;
360 val (ct,_) = the (rewrite_set thy' false rls ct);
361 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
363 val pos = lev_up pos;
364 val (pt,pos) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
365 Ctree.get_assumptions pt ([],Res);
367 writeln (pr_ctree pr_short pt);
369 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
370 1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
371 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
372 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2
373 1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )
374 1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2)
375 1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
376 1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x
377 2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2
378 3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?!
379 4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)
381 6. x = (+0) + (-1) * (-4)
385 val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";
390 (*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
391 from thy ???, i.e. together with the *_simplify ?!!!? ----------
392 " _________________ me Free_Solve _________________ ";
393 " _________________ me Free_Solve _________________ ";
394 " _________________ me Free_Solve _________________ ";
395 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
396 "solveFor x","errorBound (eps=0)",
398 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
400 ("Test",["sqroot-test","univariate","equation","test"],
401 ("Test","sqrt-equ-test"));
402 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
403 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
404 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
405 (* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
407 (* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
409 (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
411 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
412 > get_obj g_spec pt (fst p);
413 val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id","empty_meth_id")) : spec*)
414 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
415 (*val nxt = ("Specify_Problem", Specify_Problem *)
416 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
417 (*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)
418 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
419 (*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)
420 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
421 val nxt = ("Free_Solve",Free_Solve);
422 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
423 get_obj g_spec pt [];
426 get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
427 val (p,_,f,nxt,_,pt)=
428 me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
431 get_form ("Begin_Trans",Begin_Trans) p pt;
432 val (p,_,f,nxt,_,pt)=
433 me ("Begin_Trans",Begin_Trans) p [4] pt; *)
436 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
437 val (p,_,f,nxt,_,pt)=
438 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt;
440 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
441 val (p,_,f,nxt,_,pt)=
442 me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
444 get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
445 val (p,_,f,nxt,_,pt)=
446 me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
448 get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
449 val (p,_,f,nxt,_,pt)=
450 me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
452 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
453 val (p,_,f,nxt,_,pt)=
454 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
456 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
457 val (p,_,f,nxt,_,pt)=
458 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt;
461 get_form ("End_Trans",End_Trans) p pt;
462 val (p,_,f,nxt,_,pt)=
463 me ("End_Trans",End_Trans) p [11] pt; *)
465 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
466 val (p,_,f,nxt,_,pt)=
467 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
469 get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
470 val (p,_,f,nxt,_,pt)=
471 me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;
473 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
474 val (p,_,f,nxt,_,pt)=
475 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
477 get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt;
478 val (p,_,f,nxt,_,pt)=
479 me ("Rewrite_Set",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p [15] pt;
481 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
482 val ((p,p_),_,f,nxt,_,pt)=
483 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
485 get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;
486 val (p,_,f,nxt,_,pt)=
487 me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
489 writeln (pr_ctree pr_short pt);
490 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
494 " _________________ me + tacs input _________________ ";
495 " _________________ me + tacs input _________________ ";
496 " _________________ me + tacs input _________________ ";
497 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
498 "solveFor x","errorBound (eps=0)",
501 ("Test",["sqroot-test","univariate","equation","test"],
502 ["Test","sqrt-equ-test"]);
504 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
506 val nxt = ("Model_Problem",
507 Model_Problem(*["sqroot-test","univariate","equation","test"]*));
508 val (p,_,f,nxt,_,pt) = me nxt p c pt;
510 val nxt = ("Add_Given",
511 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
512 val (p,_,f,nxt,_,pt) = me nxt p c pt;
514 val nxt = ("Add_Given",Add_Given "solveFor x");
515 val (p,_,f,nxt,_,pt) = me nxt p c pt;
517 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
518 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
520 val nxt = ("Add_Find",Add_Find "solutions L");
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
523 val nxt = ("Specify_Theory",Specify_Theory "Test");
524 val (p,_,f,nxt,_,pt) = me nxt p c pt;
526 val nxt = ("Specify_Problem",
527 Specify_Problem ["sqroot-test","univariate","equation","test"]);
528 val (p,_,f,nxt,_,pt) = me nxt p c pt;
530 val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);
531 val (p,_,f,nxt,_,pt) = me nxt p c pt;
533 val nxt = ("Apply_Method",Apply_Method ["Test","sqrt-equ-test"]);
534 val (p,_,f,nxt,_,pt) = me nxt p c pt;
536 val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
537 val (p,_,f,nxt,_,pt) = me nxt p c pt;
540 val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
541 val SOME (t',asm) = rewrite_set_ thy false rls t;
543 > Rewrite.trace_on:=true;
544 Rewrite.trace_on:=false;
548 val (mI,m) = nxt; val pos' as (p,p_) = p;
550 val Applicable.Yes m = Step.check m (pt, (p,p_));
552 val pp = par_pblobj pt p;
553 val metID = get_obj g_metID pt pp;
554 val sc = (#scr o get_met) metID;
555 val is = get_istate_LI pt (p,p_);
556 val thy' = get_obj g_domID pt pp;
557 val thy = ThyC.get_theory thy';
558 val d = Rule_Set.empty;
559 val Steps [(m',f',pt',p',c',s')] =
560 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
561 val is' = get_istate_LI pt' p';
562 LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
567 val ttt = (Thm.term_of o the o (parse Test.thy))
568 "Let (((While contains_root e_e Do\
569 \Rewrite square_equation_left #>\
570 \Try (Rewrite_Set Test_simplify) #>\
571 \Try (Rewrite_Set rearrange_assoc) #>\
572 \Try (Rewrite_Set Test_simplify)) #>\
573 \Try (Rewrite_Set norm_equation) #>\
574 \Try (Rewrite_Set Test_simplify) #>\
575 \Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
576 \Try (Rewrite_Set Test_simplify))\
579 -------------------------*)
583 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
584 val (p,_,f,nxt,_,pt) = me nxt p c pt;
586 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
587 val (p,_,f,nxt,_,pt) = me nxt p c pt;
589 val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
590 val (p,_,f,nxt,_,pt) = me nxt p c pt;
592 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
593 val (p,_,f,nxt,_,pt) = me nxt p c pt;
595 val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
596 val (p,_,f,nxt,_,pt) = me nxt p c pt;
598 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
599 val (p,_,f,nxt,_,pt) = me nxt p c pt;
601 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
602 val (p,_,f,nxt,_,pt) = me nxt p c pt;
604 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
605 val (p,_,f,nxt,_,pt) = me nxt p c pt;
607 val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
608 val (p,_,f,nxt,_,pt) = me nxt p c pt;
610 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
611 val (p,_,f,nxt,_,pt) = me nxt p c pt;
613 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));
614 val (p,_,f,nxt,_,pt) = me nxt p c pt;
616 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
617 val (p,_,f,nxt,_,pt) = me nxt p c pt;
619 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]);
620 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
621 (* val nxt = ("End_Proof'",End_Proof');*)
622 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
623 then error "root-equ.sml: diff.behav. in me + tacs input"
626 writeln (pr_ctree pr_short pt);
627 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
628 "\n==============================================================");