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 " --- subproblem 2: linear-equation --- ";
120 val origin = ["x + 4 = (0::real)", "x::real"];
121 val formals = map (the o (parse thy)) origin;
123 val given = ["equation (l=(0::real))",
124 "bound_variable bdv"];
125 val where_ = ["l is_linear_in bdv", "bdv is_const"];
126 val find = ["l::real"];
127 val with_ = ["l = (%x. l) bdv"];
128 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
129 val givens = map (the o (parse thy)) given;
132 " _________________ rewrite_ x+4_________________ ";
133 " _________________ rewrite_ x+4_________________ ";
134 " _________________ rewrite_ x+4_________________ ";
135 val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
136 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
137 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
138 val rls = Test_simplify;
139 val (t,_) = the (rewrite_set_ thy false rls t);
140 val rls = rearrange_assoc;
141 val (t,_) = the (rewrite_set_ thy false rls t);
142 val rls = isolate_root;
143 val (t,_) = the (rewrite_set_ thy false rls t);
145 val rls = Test_simplify;
146 val (t,_) = the (rewrite_set_ thy false rls t);
148 sqrt (x ^^^ 2 + 5 * x) =
149 (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
150 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
151 ### trying thm 'rdistr_div_right'
152 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
153 (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
154 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
155 (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
156 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
157 5 / (-1 * 2) + 2 * x / (-1 * 2) +
158 (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
160 ### trying thm 'radd_left_commute'
161 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
163 (5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
164 ### trying thm 'radd_assoc'
165 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
167 (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
169 ### trying thm 'radd_real_const_eq'
170 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
171 -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
172 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
173 -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
174 ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
175 (-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
176 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
178 28.8.02: ruleset besser zusammenstellen !!!
180 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
181 val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
182 val asm = asm union asm';
183 val rls = Test_simplify;
184 val (t,_) = the (rewrite_set_ thy false rls t);
185 val rls = norm_equation;
186 val (t,_) = the (rewrite_set_ thy false rls t);
187 val rls = Test_simplify;
188 val (t,_) = the (rewrite_set_ thy false rls t);
189 val rls = isolate_bdv;
190 val subst = [(str2term "bdv", str2term "x")];
191 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
192 val rls = Test_simplify;
193 val (t,_) = the (rewrite_set_ thy false rls t);
194 val t' = UnparseC.term t;
195 if t' = "x = 4" then ()
196 else error "root-equ.sml: new behav. in rewrite_ x+4";
198 " _________________ rewrite x=4_________________ ";
199 " _________________ rewrite x=4_________________ ";
200 " _________________ rewrite x=4_________________ ";
202 rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
203 atomty ((#prop o Thm.rep_thm) (!tthm));
204 atomty (Thm.term_of (!tct));
207 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
208 (*1*)val thm = ("square_equation_left", "");
209 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
210 "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
211 (*2*)val rls = "Test_simplify";
212 val (ct,_) = the (rewrite_set thy' false rls ct);
213 "9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";
214 (*3*)val rls = "rearrange_assoc";
215 val (ct,_) = the (rewrite_set thy' false rls ct);
216 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";
217 (*4*)val rls = "isolate_root";
218 val (ct,_) = the (rewrite_set thy' false rls ct);
219 "sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
220 (*5*)val rls = "Test_simplify";
221 val (ct,_) = the (rewrite_set thy' false rls ct);
222 "sqrt (x ^^^ 2 + 5 * x) = 2 + x";
223 (*6*)val thm = ("square_equation_left", "");
224 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
225 val asm = asm union asm';
226 "x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
227 (*7*)val rls = "Test_simplify";
228 val (ct,_) = the (rewrite_set thy' false rls ct);
229 "x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";
230 (*8*)val rls = "norm_equation";
231 val (ct,_) = the (rewrite_set thy' false rls ct);
232 "x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";
233 (*9*)val rls = "Test_simplify";
234 val (ct,_) = the (rewrite_set thy' false rls ct);
236 (*10*)val rls = "isolate_bdv";
237 val (ct,_) = the (rewrite_set_inst thy' false
238 [("bdv", "x")] rls ct);
240 (*11*)val rls = "Test_simplify";
241 val (ct,_) = the (rewrite_set thy' false rls ct);
242 if ct="x = 4" then () else error "new behaviour in test-example";
247 " _________________ rewrite + cappend _________________ ";
248 " _________________ rewrite + cappend _________________ ";
249 " _________________ rewrite + cappend _________________ ";
251 val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
252 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
253 val oris = O_Model.init ctl thy
254 ((#ppc o Problem.from_store)
255 ["sqroot-test", "univariate", "equation", "test"]);
256 val loc = Istate.empty;
257 val (pt,pos) = (e_ctree,[]);
258 val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)
259 val pt = update_branch pt [] TransitiveB;
261 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
263 (*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
264 val pt = update_domID pt [] "Test";
265 val pt = update_pblID pt [] ["Test",
266 "equations", "univariate", "square-root"];
267 val pt = update_metID pt [] ["Test", "sqrt-equ-test"];
268 val pt = update_pbl pt [] [];
269 val pt = update_met pt [] [];
271 > get_obj g_spec pt [];
272 val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
273 > val pt = update_domID pt [] "RatArith";
274 > get_obj g_spec pt [];
275 val it = ("RatArith",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
276 > val pt = update_pblID pt [] ["RatArith",
277 "equations", "univariate", "square-root"];
278 > get_obj g_spec pt [];
279 ("RatArith",["RatArith", "equations", "univariate", "square-root"],
280 ("empty_thy_id", "empty_meth_id")) : spec
281 > val pt = update_metID pt [] ("RatArith", "sqrt-equ-test");
282 > get_obj g_spec pt [];
283 ("RatArith",["RatArith", "equations", "univariate", "square-root"],
284 ("RatArith", "sqrt-equ-test")) : spec
289 val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
291 val pos = (lev_on o lev_dn) pos;
292 val thm = ("square_equation_left", ""); val ctold = ct;
293 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
294 val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
295 (*val pt = union_asm pt [] (map (rpair []) asm);*)
297 val pos = lev_on pos;
298 val rls = ("Test_simplify"); val ctold = str2term ct;
299 val (ct,_) = the (rewrite_set thy' false rls ct);
300 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
302 val pos = lev_on pos;
303 val rls = ("rearrange_assoc"); val ctold = str2term ct;
304 val (ct,_) = the (rewrite_set thy' false rls ct);
305 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
307 val pos = lev_on pos;
308 val rls = ("isolate_root"); val ctold = str2term ct;
309 val (ct,_) = the (rewrite_set thy' false rls ct);
310 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
312 val pos = lev_on pos;
313 val rls = ("Test_simplify"); val ctold = str2term ct;
314 val (ct,_) = the (rewrite_set thy' false rls ct);
315 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
317 val pos = lev_on pos;
318 val thm = ("square_equation_left", ""); val ctold = str2term ct;
319 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
320 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
321 (*val pt = union_asm pt [] (map (rpair []) asm);*)
323 val pos = lev_up pos;
324 val (pt,_) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
326 val pos = lev_on pos;
327 val rls = ("Test_simplify"); val ctold = str2term ct;
328 val (ct,_) = the (rewrite_set thy' false rls ct);
329 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
331 val pos = lev_on pos;
332 val rls = ("norm_equation"); val ctold = str2term ct;
333 val (ct,_) = the (rewrite_set thy' false rls ct);
334 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
336 val pos = lev_on pos;
337 val rls = ("Test_simplify"); val ctold = str2term ct;
338 val (ct,_) = the (rewrite_set thy' false rls ct);
339 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
341 (* --- see comments in interface_ME_ISA/instantiate''
342 val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
343 val (ct,_) = the (rewrite_set thy' false
344 ("#isolate_bdv",rlsdat') ct); *)
345 val pos = lev_on pos;
346 val rls = ("isolate_bdv"); val ctold = str2term ct;
347 val (ct,_) = the (rewrite_set_inst thy' false
348 [("bdv", "x")] rls ct);
349 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
351 val pos = lev_on pos;
352 val rls = ("Test_simplify"); val ctold = str2term ct;
353 val (ct,_) = the (rewrite_set thy' false rls ct);
354 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
356 val pos = lev_up pos;
357 val (pt,pos) = append_result pt pos Istate.empty (str2term ct,[]) Complete;
358 Ctree.get_assumptions pt ([],Res);
360 writeln (pr_ctree pr_short pt);
362 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
363 1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
364 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
365 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2
366 1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )
367 1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2)
368 1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
369 1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x
370 2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2
371 3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?!
372 4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)
374 6. x = (+0) + (-1) * (-4)
378 val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";
383 (*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
384 from thy ???, i.e. together with the *_simplify ?!!!? ----------
385 " _________________ me Free_Solve _________________ ";
386 " _________________ me Free_Solve _________________ ";
387 " _________________ me Free_Solve _________________ ";
388 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
389 "solveFor x", "errorBound (eps=0)",
391 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
393 ("Test",["sqroot-test", "univariate", "equation", "test"],
394 ("Test", "sqrt-equ-test"));
395 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
396 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
398 (* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
399 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
400 (* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
401 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
402 (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
403 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
404 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
405 > get_obj g_spec pt (fst p);
406 val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec*)
407 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
408 (*val nxt = ("Specify_Problem", Specify_Problem *)
409 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
410 (*val nxt = ("Specify_Method",Specify_Method ("DiffAppl", "sqrt-equ-test"));*)
411 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
412 (*val nxt = ("Apply_Method",Apply_Method ("DiffAppl", "sqrt-equ-test"));*)
413 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
414 val nxt = ("Free_Solve",Free_Solve);
415 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
416 get_obj g_spec pt [];
419 get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
420 val (p,_,f,nxt,_,pt)=
421 me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
424 get_form ("Begin_Trans",Begin_Trans) p pt;
425 val (p,_,f,nxt,_,pt)=
426 me ("Begin_Trans",Begin_Trans) p [4] pt; *)
429 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
430 val (p,_,f,nxt,_,pt)=
431 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [5] pt;
433 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
434 val (p,_,f,nxt,_,pt)=
435 me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
437 get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
438 val (p,_,f,nxt,_,pt)=
439 me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
441 get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
442 val (p,_,f,nxt,_,pt)=
443 me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
445 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
446 val (p,_,f,nxt,_,pt)=
447 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
449 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
450 val (p,_,f,nxt,_,pt)=
451 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [10] pt;
454 get_form ("End_Trans",End_Trans) p pt;
455 val (p,_,f,nxt,_,pt)=
456 me ("End_Trans",End_Trans) p [11] pt; *)
458 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
459 val (p,_,f,nxt,_,pt)=
460 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
462 get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
463 val (p,_,f,nxt,_,pt)=
464 me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;
466 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
467 val (p,_,f,nxt,_,pt)=
468 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
470 get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt;
471 val (p,_,f,nxt,_,pt)=
472 me ("Rewrite_Set",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p [15] pt;
474 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
475 val ((p,p_),_,f,nxt,_,pt)=
476 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
478 get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt;
479 val (p,_,f,nxt,_,pt)=
480 me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt;
482 writeln (pr_ctree pr_short pt);
483 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
487 " _________________ me + tacs input _________________ ";
488 " _________________ me + tacs input _________________ ";
489 " _________________ me + tacs input _________________ ";
490 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
491 "solveFor x", "errorBound (eps=0)",
494 ("Test",["sqroot-test", "univariate", "equation", "test"],
495 ["Test", "sqrt-equ-test"]);
497 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
499 val nxt = ("Model_Problem",
500 Model_Problem(*["sqroot-test", "univariate", "equation", "test"]*));
501 val (p,_,f,nxt,_,pt) = me nxt p c pt;
503 val nxt = ("Add_Given",
504 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
505 val (p,_,f,nxt,_,pt) = me nxt p c pt;
507 val nxt = ("Add_Given",Add_Given "solveFor x");
508 val (p,_,f,nxt,_,pt) = me nxt p c pt;
510 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
511 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
513 val nxt = ("Add_Find",Add_Find "solutions L");
514 val (p,_,f,nxt,_,pt) = me nxt p c pt;
516 val nxt = ("Specify_Theory",Specify_Theory "Test");
517 val (p,_,f,nxt,_,pt) = me nxt p c pt;
519 val nxt = ("Specify_Problem",
520 Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);
521 val (p,_,f,nxt,_,pt) = me nxt p c pt;
523 val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]);
524 val (p,_,f,nxt,_,pt) = me nxt p c pt;
526 val nxt = ("Apply_Method",Apply_Method ["Test", "sqrt-equ-test"]);
527 val (p,_,f,nxt,_,pt) = me nxt p c pt;
529 val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
530 val (p,_,f,nxt,_,pt) = me nxt p c pt;
533 val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
534 val SOME (t',asm) = rewrite_set_ thy false rls t;
536 > Rewrite.trace_on:=true;
537 Rewrite.trace_on:=false;
541 val (mI,m) = nxt; val pos' as (p,p_) = p;
543 val Applicable.Yes m = Step.check m (pt, (p,p_));
545 val pp = par_pblobj pt p;
546 val metID = get_obj g_metID pt pp;
547 val sc = (#scr o Method.from_store) metID;
548 val is = get_istate_LI pt (p,p_);
549 val thy' = get_obj g_domID pt pp;
550 val thy = ThyC.get_theory thy';
551 val d = Rule_Set.empty;
552 val Steps [(m',f',pt',p',c',s')] =
553 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
554 val is' = get_istate_LI pt' p';
555 LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
560 val ttt = (Thm.term_of o the o (parse Test.thy))
561 "Let (((While contains_root e_e Do\
562 \Rewrite square_equation_left #>\
563 \Try (Rewrite_Set Test_simplify) #>\
564 \Try (Rewrite_Set rearrange_assoc) #>\
565 \Try (Rewrite_Set Test_simplify)) #>\
566 \Try (Rewrite_Set norm_equation) #>\
567 \Try (Rewrite_Set Test_simplify) #>\
568 \Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
569 \Try (Rewrite_Set Test_simplify))\
572 -------------------------*)
576 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
577 val (p,_,f,nxt,_,pt) = me nxt p c pt;
579 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
580 val (p,_,f,nxt,_,pt) = me nxt p c pt;
582 val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
583 val (p,_,f,nxt,_,pt) = me nxt p c pt;
585 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
586 val (p,_,f,nxt,_,pt) = me nxt p c pt;
588 val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
589 val (p,_,f,nxt,_,pt) = me nxt p c pt;
591 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
592 val (p,_,f,nxt,_,pt) = me nxt p c pt;
594 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
595 val (p,_,f,nxt,_,pt) = me nxt p c pt;
597 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
598 val (p,_,f,nxt,_,pt) = me nxt p c pt;
600 val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
601 val (p,_,f,nxt,_,pt) = me nxt p c pt;
603 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
604 val (p,_,f,nxt,_,pt) = me nxt p c pt;
606 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));
607 val (p,_,f,nxt,_,pt) = me nxt p c pt;
609 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
610 val (p,_,f,nxt,_,pt) = me nxt p c pt;
612 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test", "univariate", "equation", "test"]);
613 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
614 (* val nxt = ("End_Proof'",End_Proof');*)
615 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
616 then error "root-equ.sml: diff.behav. in me + tacs input"
619 writeln (pr_ctree pr_short pt);
620 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
621 "\n==============================================================");