4 method "sqrt-equ-test", _NOT_ "square-equation"
7 " ================= equation with x =(-12)/5, but L ={} ======= ";
8 " _________________ rewrite _________________ ";
11 " ================= equation with result={4} ================== ";
12 " -------------- model, specify ------------ ";
13 " ________________ rewrite _________________";
14 " _________________ rewrite_ x=4_________________ ";
15 " _________________ rewrite + cappend _________________ ";
16 " _________________ me Free_Solve _________________ ";
17 " _________________ me + tacs input _________________ ";
18 (*" _______________ me + nxt_step from script _________---> scriptnew.sml*)
19 (*" _________________ me + nxt_step from script (check_elementwise..)______
20 ... L_a = Tac subproblem_equation_dummy; ";*)
21 (*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*)
29 > val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";
30 > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
31 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
32 > Syntax.string_of_term (Proof_Context.init_global thy) t';
34 (******************************************************************)
35 (* ------------------------------------- *)
36 " _________________ equation with x =(-12)/5, but L ={} ------- ";
37 (* ------------------------------------- *)
38 " _________________ rewrite _________________ ";
40 val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
41 val thm = ("square_equation_left", "");
42 val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
43 (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) \<up> 2"*)
44 val rls = ("Test_simplify");
45 val (ct,_) = the (rewrite_set thy' false rls ct);
46 (*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x \<up> 2 + -3 * x))"*)
47 val rls = ("rearrange_assoc");
48 val (ct,_) = the (rewrite_set thy' false rls ct);
49 (*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x \<up> 2 + -3 * x)"*)
50 val rls = ("isolate_root");
51 val (ct,_) = the (rewrite_set thy' false rls ct);
52 (*"sqrt (x \<up> 2 + -3 * x) =
53 (-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
54 val rls = ("Test_simplify");
55 val (ct,_) = the (rewrite_set thy' false rls ct);
56 (*"sqrt (x \<up> 2 + -3 * x) = 6 + x"*)
57 val thm = ("square_equation_left", "");
58 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
59 val asm = asm union asm';
60 (*"x \<up> 2 + -3 * x = (6 + x) \<up> 2"*)
61 val rls = ("Test_simplify");
62 val (ct,_) = the (rewrite_set thy' false rls ct);
63 (*"x \<up> 2 + -3 * x = 36 + (x \<up> 2 + 12 * x)"*)
64 val rls = ("norm_equation");
65 val (ct,_) = the (rewrite_set thy' false rls ct);
66 (*"x \<up> 2 + -3 * x + -1 * (36 + (x \<up> 2 + 12 * x)) = 0"*)
67 val rls = ("Test_simplify");
68 val (ct,_) = the (rewrite_set thy' false rls ct);
69 (*"-36 + -15 * x = 0"*)
70 val rls = ("isolate_bdv");
71 val (ct,_) = the (rewrite_set_inst thy' false
72 [("bdv", "x::real")] rls ct);
73 (*"x = (0 + -1 * -36) // -15"*)
74 val rls = ("Test_simplify");
75 val (ct,_) = the (rewrite_set thy' false rls ct);
76 if ct<>"x = -12 / 5"then error "new behaviour in testexample"else ();
79 val ct = "x = (-12) / 5" : TermC.as_string
82 ["(+0) <= sqrt x + sqrt ((-3) + x) ", "(+0) <= 9 + 4 * x",
83 "(+0) <= (-3) * x + x \<up> 2", "(+0) <= 6 + x"] : TermC.as_string list
90 " ================== equation with result={4} ================== ";
91 " ================== equation with result={4} ================== ";
92 " ================== equation with result={4} ================== ";
94 " -------------- model, specify ------------ ";
95 " -------------- model, specify ------------ ";
96 " -------------- model, specify ------------ ";
97 " --- subproblem 1: linear-equation --- ";
98 val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
99 "bound_variable x", "error_bound 0"(*,
100 "solutions L::real set" ,
101 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
102 val thy = (theory "Isac_Knowledge");
103 val formals = map (the o (TermC.parse thy)) origin;
105 val given = ["equation (l=(r::real))",
106 "bound_variable bdv", (* TODO type *)
108 val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.yy*)
110 "eps is_const_expr"];
111 val find = ["solutions (L::bool list)"];
112 val with_ = [(* parseold ...
113 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
114 val chkpbl = map (the o (TermC.parse thy)) (given @ where_ @ find @ with_);
115 val givens = map (the o (TermC.parse thy)) given;
116 parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
118 " --- subproblem 2: linear-equation --- ";
119 val origin = ["x + 4 = (0::real)", "x::real"];
120 val formals = map (the o (TermC.parse thy)) origin;
122 val given = ["equation (l=(0::real))",
123 "bound_variable bdv"];
124 val where_ = ["l is_linear_in bdv", "bdv is_atom"];
125 val find = ["l::real"];
126 val with_ = ["l = (%x. l) bdv"];
127 val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
128 val givens = map (the o (TermC.parse thy)) given;
131 " _________________ rewrite_ x+4_________________ ";
132 " _________________ rewrite_ x+4_________________ ";
133 " _________________ rewrite_ x+4_________________ ";
134 val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
135 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
136 val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
137 val rls = Test_simplify;
138 val (t,_) = the (rewrite_set_ thy false rls t);
139 val rls = rearrange_assoc;
140 val (t,_) = the (rewrite_set_ thy false rls t);
141 val rls = isolate_root;
142 val (t,_) = the (rewrite_set_ thy false rls t);
144 val rls = Test_simplify;
145 val (t,_) = the (rewrite_set_ thy false rls t);
147 sqrt (x \<up> 2 + 5 * x) =
148 (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
149 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
150 ### trying thm 'rdistr_div_right'
151 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
152 (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
153 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
154 (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
155 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
156 5 / (-1 * 2) + 2 * x / (-1 * 2) +
157 (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
159 ### trying thm 'radd_left_commute'
160 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
162 (5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
163 ### trying thm 'radd_assoc'
164 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
166 (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
168 ### trying thm 'radd_real_const_eq'
169 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
170 -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
171 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
172 -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
173 ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
174 (-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
175 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
177 28.8.02: ruleset besser zusammenstellen !!!
179 val thm = ThmC.numerals_to_Free @{thm square_equation_left};
180 val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
181 val asm = asm union asm';
182 val rls = Test_simplify;
183 val (t,_) = the (rewrite_set_ thy false rls t);
184 val rls = norm_equation;
185 val (t,_) = the (rewrite_set_ thy false rls t);
186 val rls = Test_simplify;
187 val (t,_) = the (rewrite_set_ thy false rls t);
188 val rls = isolate_bdv;
189 val subst = [(TermC.str2term "bdv", TermC.str2term "x")];
190 val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
191 val rls = Test_simplify;
192 val (t,_) = the (rewrite_set_ thy false rls t);
193 val t' = UnparseC.term t;
194 if t' = "x = 4" then ()
195 else error "root-equ.sml: new behav. in rewrite_ x+4";
197 " _________________ rewrite x=4_________________ ";
198 " _________________ rewrite x=4_________________ ";
199 " _________________ rewrite x=4_________________ ";
201 rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
202 TermC.atomty (Thm.prop_of (!tthm));
203 TermC.atomty (Thm.term_of (!tct));
206 val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
207 (*1*)val thm = ("square_equation_left", "");
208 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
209 "9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2";
210 (*2*)val rls = "Test_simplify";
211 val (ct,_) = the (rewrite_set thy' false rls ct);
212 "9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 2 + 5 * x))";
213 (*3*)val rls = "rearrange_assoc";
214 val (ct,_) = the (rewrite_set thy' false rls ct);
215 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)";
216 (*4*)val rls = "isolate_root";
217 val (ct,_) = the (rewrite_set thy' false rls ct);
218 "sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
219 (*5*)val rls = "Test_simplify";
220 val (ct,_) = the (rewrite_set thy' false rls ct);
221 "sqrt (x \<up> 2 + 5 * x) = 2 + x";
222 (*6*)val thm = ("square_equation_left", "");
223 val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
224 val asm = asm union asm';
225 "x \<up> 2 + 5 * x = (2 + x) \<up> 2";
226 (*7*)val rls = "Test_simplify";
227 val (ct,_) = the (rewrite_set thy' false rls ct);
228 "x \<up> 2 + 5 * x = 4 + (x \<up> 2 + 4 * x)";
229 (*8*)val rls = "norm_equation";
230 val (ct,_) = the (rewrite_set thy' false rls ct);
231 "x \<up> 2 + 5 * x + -1 * (4 + (x \<up> 2 + 4 * x)) = 0";
232 (*9*)val rls = "Test_simplify";
233 val (ct,_) = the (rewrite_set thy' false rls ct);
235 (*10*)val rls = "isolate_bdv";
236 val (ct,_) = the (rewrite_set_inst thy' false
237 [("bdv", "x")] rls ct);
239 (*11*)val rls = "Test_simplify";
240 val (ct,_) = the (rewrite_set thy' false rls ct);
241 if ct="x = 4" then () else error "new behaviour in test-example";
246 " _________________ rewrite + cappend _________________ ";
247 " _________________ rewrite + cappend _________________ ";
248 " _________________ rewrite + cappend _________________ ";
250 val ct = TermC.str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
251 val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
252 val oris = O_Model.init ctl thy
253 ((#ppc o Problem.from_store)
254 ["sqroot-test", "univariate", "equation", "test"]);
255 val loc = Istate.empty;
256 val (pt,pos) = (e_ctree,[]);
257 val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)
258 val pt = update_branch pt [] TransitiveB;
260 val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
262 (*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
263 val pt = update_domID pt [] "Test";
264 val pt = update_pblID pt [] ["Test",
265 "equations", "univariate", "square-root"];
266 val pt = update_metID pt [] ["Test", "sqrt-equ-test"];
267 val pt = update_pbl pt [] [];
268 val pt = update_met pt [] [];
270 > get_obj g_spec pt [];
271 val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
272 > val pt = update_domID pt [] "RatArith";
273 > get_obj g_spec pt [];
274 val it = ("RatArith",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec
275 > val pt = update_pblID pt [] ["RatArith",
276 "equations", "univariate", "square-root"];
277 > get_obj g_spec pt [];
278 ("RatArith",["RatArith", "equations", "univariate", "square-root"],
279 ("empty_thy_id", "empty_meth_id")) : spec
280 > val pt = update_metID pt [] ("RatArith", "sqrt-equ-test");
281 > get_obj g_spec pt [];
282 ("RatArith",["RatArith", "equations", "univariate", "square-root"],
283 ("RatArith", "sqrt-equ-test")) : spec
288 val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
290 val pos = (lev_on o lev_dn) pos;
291 val thm = ("square_equation_left", ""); val ctold = ct;
292 val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
293 val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.str2term ct,[])Complete;
294 (*val pt = union_asm pt [] (map (rpair []) asm);*)
296 val pos = lev_on pos;
297 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
298 val (ct,_) = the (rewrite_set thy' false rls ct);
299 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
301 val pos = lev_on pos;
302 val rls = ("rearrange_assoc"); val ctold = TermC.str2term ct;
303 val (ct,_) = the (rewrite_set thy' false rls ct);
304 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
306 val pos = lev_on pos;
307 val rls = ("isolate_root"); val ctold = TermC.str2term ct;
308 val (ct,_) = the (rewrite_set thy' false rls ct);
309 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
311 val pos = lev_on pos;
312 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
313 val (ct,_) = the (rewrite_set thy' false rls ct);
314 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
316 val pos = lev_on pos;
317 val thm = ("square_equation_left", ""); val ctold = TermC.str2term ct;
318 val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
319 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
320 (*val pt = union_asm pt [] (map (rpair []) asm);*)
322 val pos = lev_up pos;
323 val (pt,_) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
325 val pos = lev_on pos;
326 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
327 val (ct,_) = the (rewrite_set thy' false rls ct);
328 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
330 val pos = lev_on pos;
331 val rls = ("norm_equation"); val ctold = TermC.str2term ct;
332 val (ct,_) = the (rewrite_set thy' false rls ct);
333 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
335 val pos = lev_on pos;
336 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
337 val (ct,_) = the (rewrite_set thy' false rls ct);
338 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
340 (* --- see comments in interface_ME_ISA/instantiate''
341 val rlsdat' = instantiate_rls' thy' [("bdv", "x")] ("isolate_bdv");
342 val (ct,_) = the (rewrite_set thy' false
343 ("#isolate_bdv",rlsdat') ct); *)
344 val pos = lev_on pos;
345 val rls = ("isolate_bdv"); val ctold = TermC.str2term ct;
346 val (ct,_) = the (rewrite_set_inst thy' false
347 [("bdv", "x")] rls ct);
348 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
350 val pos = lev_on pos;
351 val rls = ("Test_simplify"); val ctold = TermC.str2term ct;
352 val (ct,_) = the (rewrite_set thy' false rls ct);
353 val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.str2term ct,[]) Complete;
355 val pos = lev_up pos;
356 val (pt,pos) = append_result pt pos Istate.empty (TermC.str2term ct,[]) Complete;
357 Ctree.get_assumptions pt ([],Res);
359 writeln (pr_ctree pr_short pt);
361 . sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
362 1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
363 1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x)
364 1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) \<up> 2
365 1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x \<up> 2) )
366 1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x \<up> 2)
367 1.5. sqrt (5 * x + x \<up> 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
368 1.6. sqrt (5 * x + x \<up> 2) = (+2) + x
369 2. 5 * x + x \<up> 2 = ((+2) + x) \<up> 2
370 3. 5 * x + x \<up> 2 = 4 + (4 * x + x \<up> 2) ###12.12.99: indent 2.1. !?!
371 4. 5 * x + x \<up> 2 + (-1) * (4 + (4 * x + x \<up> 2)) = (+0)
373 6. x = (+0) + (-1) * (-4)
377 val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
382 (*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
383 from thy ???, i.e. together with the *_simplify ?!!!? ----------
384 " _________________ me Free_Solve _________________ ";
385 " _________________ me Free_Solve _________________ ";
386 " _________________ me Free_Solve _________________ ";
387 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
388 "solveFor x", "errorBound (eps=0)",
390 "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
392 ("Test",["sqroot-test", "univariate", "equation", "test"],
393 ("Test", "sqrt-equ-test"));
394 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
395 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*)
396 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
397 (* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
398 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
399 (* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
400 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
401 (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
402 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
403 (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
404 > get_obj g_spec pt (fst p);
405 val it = ("empty_thy_id",["empty_probl_id"],("empty_thy_id", "empty_meth_id")) : spec*)
406 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
407 (*val nxt = ("Specify_Problem", Specify_Problem *)
408 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
409 (*val nxt = ("Specify_Method",Specify_Method ("DiffAppl", "sqrt-equ-test"));*)
410 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
411 (*val nxt = ("Apply_Method",Apply_Method ("DiffAppl", "sqrt-equ-test"));*)
412 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
413 val nxt = ("Free_Solve",Free_Solve);
414 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
415 get_obj g_spec pt [];
418 get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
419 val (p,_,f,nxt,_,pt)=
420 me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
423 get_form ("Begin_Trans",Begin_Trans) p pt;
424 val (p,_,f,nxt,_,pt)=
425 me ("Begin_Trans",Begin_Trans) p [4] pt; *)
428 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
429 val (p,_,f,nxt,_,pt)=
430 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [5] pt;
432 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
433 val (p,_,f,nxt,_,pt)=
434 me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
436 get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
437 val (p,_,f,nxt,_,pt)=
438 me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
440 get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
441 val (p,_,f,nxt,_,pt)=
442 me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
444 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
445 val (p,_,f,nxt,_,pt)=
446 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
448 get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
449 val (p,_,f,nxt,_,pt)=
450 me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p [10] pt;
453 get_form ("End_Trans",End_Trans) p pt;
454 val (p,_,f,nxt,_,pt)=
455 me ("End_Trans",End_Trans) p [11] pt; *)
457 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
458 val (p,_,f,nxt,_,pt)=
459 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
461 get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
462 val (p,_,f,nxt,_,pt)=
463 me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] 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 [14] pt;
469 get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt;
470 val (p,_,f,nxt,_,pt)=
471 me ("Rewrite_Set",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p [15] pt;
473 get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
474 val ((p,p_),_,f,nxt,_,pt)=
475 me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
477 get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt;
478 val (p,_,f,nxt,_,pt)=
479 me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt;
481 writeln (pr_ctree pr_short pt);
482 writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
486 " _________________ me + tacs input _________________ ";
487 " _________________ me + tacs input _________________ ";
488 " _________________ me + tacs input _________________ ";
489 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
490 "solveFor x", "errorBound (eps=0)",
493 ("Test",["sqroot-test", "univariate", "equation", "test"],
494 ["Test", "sqrt-equ-test"]);
496 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
498 val nxt = ("Model_Problem",
499 Model_Problem(*["sqroot-test", "univariate", "equation", "test"]*));
500 val (p,_,f,nxt,_,pt) = me nxt p c pt;
502 val nxt = ("Add_Given",
503 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
504 val (p,_,f,nxt,_,pt) = me nxt p c pt;
506 val nxt = ("Add_Given",Add_Given "solveFor x");
507 val (p,_,f,nxt,_,pt) = me nxt p c pt;
509 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
510 val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
512 val nxt = ("Add_Find",Add_Find "solutions L");
513 val (p,_,f,nxt,_,pt) = me nxt p c pt;
515 val nxt = ("Specify_Theory",Specify_Theory "Test");
516 val (p,_,f,nxt,_,pt) = me nxt p c pt;
518 val nxt = ("Specify_Problem",
519 Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);
520 val (p,_,f,nxt,_,pt) = me nxt p c pt;
522 val nxt = ("Specify_Method",Specify_Method ["Test", "sqrt-equ-test"]);
523 val (p,_,f,nxt,_,pt) = me nxt p c pt;
525 val nxt = ("Apply_Method",Apply_Method ["Test", "sqrt-equ-test"]);
526 val (p,_,f,nxt,_,pt) = me nxt p c pt;
528 val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
529 val (p,_,f,nxt,_,pt) = me nxt p c pt;
532 val t = TermC.str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
533 val SOME (t',asm) = rewrite_set_ thy false rls t;
535 Rewrite.trace_on:=false; (*true false*)
539 val (mI,m) = nxt; val pos' as (p,p_) = p;
541 val Applicable.Yes m = Step.check m (pt, (p,p_));
543 val pp = par_pblobj pt p;
544 val metID = get_obj g_metID pt pp;
545 val sc = (#scr o MethodC.from_store) metID;
546 val is = get_istate_LI pt (p,p_);
547 val thy' = get_obj g_domID pt pp;
548 val thy = ThyC.get_theory thy';
549 val d = Rule_Set.empty;
550 val Steps [(m',f',pt',p',c',s')] =
551 locate_input_tactic thy' m (pt,(p,p_)) (sc,d) is;
552 val is' = get_istate_LI pt' p';
553 LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);
558 val ttt = (Thm.term_of o the o (TermC.parse Test.thy))
559 "Let (((While contains_root e_e Do\
560 \Rewrite square_equation_left #>\
561 \Try (Rewrite_Set Test_simplify) #>\
562 \Try (Rewrite_Set rearrange_assoc) #>\
563 \Try (Rewrite_Set Test_simplify)) #>\
564 \Try (Rewrite_Set norm_equation) #>\
565 \Try (Rewrite_Set Test_simplify) #>\
566 \Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
567 \Try (Rewrite_Set Test_simplify))\
570 -------------------------*)
574 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
575 val (p,_,f,nxt,_,pt) = me nxt p c pt;
577 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
578 val (p,_,f,nxt,_,pt) = me nxt p c pt;
580 val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
581 val (p,_,f,nxt,_,pt) = me nxt p c pt;
583 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
584 val (p,_,f,nxt,_,pt) = me nxt p c pt;
586 val nxt = ("Rewrite",Rewrite ("square_equation_left", ""));
587 val (p,_,f,nxt,_,pt) = me nxt p c pt;
589 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
590 val (p,_,f,nxt,_,pt) = me nxt p c pt;
592 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
593 val (p,_,f,nxt,_,pt) = me nxt p c pt;
595 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
596 val (p,_,f,nxt,_,pt) = me nxt p c pt;
598 val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
599 val (p,_,f,nxt,_,pt) = me nxt p c pt;
601 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
602 val (p,_,f,nxt,_,pt) = me nxt p c pt;
604 val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv"));
605 val (p,_,f,nxt,_,pt) = me nxt p c pt;
607 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
608 val (p,_,f,nxt,_,pt) = me nxt p c pt;
610 val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test", "univariate", "equation", "test"]);
611 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
612 (* val nxt = ("End_Proof'",End_Proof');*)
613 if f <> (Form' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
614 then error "root-equ.sml: diff.behav. in me + tacs input"
617 writeln (pr_ctree pr_short pt);
618 writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
619 "\n==============================================================");