1 (* use"test-script.sml";
5 " scripts: Variante 'funktional' ";
6 "############## Make_fun_by_new_variable ##############";
7 "############## Make_fun_by_explicit ##############";
8 "################ Solve_root_equation #################";
9 "------- Notlocatable: Free_Solve -------";
11 " --- test100: nxt_tac order------------------------------------ ";
12 " --- test100: order 1 3 1 2 ----------------------------------- ";
13 " --- test200: nxt_tac order ------------------------------------- ";
14 " --- test200: order 3 1 1 2 --------------------------------- ";
16 " --- root-equation: nxt_tac order------------------------------ ";
17 " --- root-equation: 1.norm_equation ------------------------------ ";
18 (* --- test200: calculate -----------------------------------------*)
19 " --- check_elementwise ------------------------------ ";
21 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
22 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
29 " #################################################### ";
30 " scripts: Variante 'funktional' ";
31 " #################################################### ";
33 val c = (the o (parse DiffApp.thy))
34 "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\
35 \ (v_::real) (itv_::real set) (err_::bool) = \
36 \ (let e_ = (hd o (filter (Testvar m_))) rs_; \
37 \ t_ = (if 1 < Length rs_ \
38 \ then (SubProblem (Reals_,[make,function],(Isac_,no_met))\
39 \ [real_ m_, real_ v_, bool_list_ rs_])\
41 \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \
42 \ (DiffAppl_,maximum_on_interval))\
43 \ [bool_ t_, real_ v_, real_set_ itv_]\
44 \ in ((SubProblem (Reals_,[find_values,tool],(DiffAppl_,find_values)) \
45 \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \
46 \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))";
49 "######################################################";
50 "############## Make_fun_by_new_variable ##############";
51 "######################################################";
53 val sc = (the o (parse DiffApp.thy)) (*start interpretieren*)
54 "Script Make_fun_by_new_variable (f_::real) (v_::real) \
55 \ (eqs_::bool list) = \
56 \(let h_ = (hd o (filter (Testvar m_))) eqs_; \
57 \ es_ = dropWhile (ident h_) eqs_; \
58 \ vs_ = dropWhile (ident f_) (Var h_); \
61 \ e1_ = (hd o (filter (Testvar v1_))) es_; \
62 \ e2_ = (hd o (filter (Testvar v2_))) es_; \
63 \ (s_1::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\
64 \ [bool_ e1_, real_ v1_]);\
65 \ (s_2::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\
66 \ [bool_ e2_, real_ v2_])\
67 \in Substitute [(v_1, (Rhs o hd) s_1),(v_2, (Rhs o hd) s_2)] h_)";
68 val ags = map (term_of o the o (parse DiffApp.thy))
69 ["A::real", "alpha::real",
70 "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"];
72 (* problem with exn PTREE + eval_to -------------------------
73 "-------------- subproblem with empty formalizaton -------";
75 ("Subproblem", mstep2mstep' pt p
76 (Subproblem (("Reals",["univar","equation","test"],
77 (""(*"ANDERN !!!!!!!*),"no_met")),[])));
78 val (mI2,m2) = (mI1,m1);
80 ("Substitute", mstep2mstep' pt p
81 (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")]));
82 "------- same_tacpbl + eval_to -------";
83 val Some(l1,t1) = same_tacpbl sc ll (mI1,m1);
85 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
86 Sign.string_of_term (sign_of DiffApp.thy) t1;
87 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
89 val Some(l2,t2) = same_tacpbl sc l1 (mI2,m2);
91 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
92 Sign.string_of_term (sign_of DiffApp.thy) t2;
93 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
95 val Some(l3,t3) = same_tacpbl sc l2 (mI3,m3);
97 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
98 Sign.string_of_term (sign_of DiffApp.thy) t3;
99 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
102 "------- eq_tacIDs + eq_consts + eval_args -------";
103 val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) [];
104 val eq_cons = filter (eq_consts m) eq_ids;
105 val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
106 "------- locate -------";
109 "-------------- subproblem with formalizaton -------";
111 ("Subproblem", mstep2mstep' pt []
112 (Subproblem (("Reals",["univar","equation","test"],
113 (""(*"ANDERN !!!!!!!*),"no_met")),
114 ["a//#2=r*sin alpha","a"])));
115 "------- same_tacpbl + eval_to -------";
118 "------- eq_tacIDs + eq_consts + eval_args -------";
119 val eq_ids = eq_tacIDs [] sc (mI,m) [];
120 val eq_cons = filter (eq_consts m) eq_ids;
121 val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons;
124 "------- locate -------";
125 -------------------------------------------------------*)
126 (* use"ME/script.sml";
127 use"test-script.sml";
132 (*#####################################################*)
133 (*#####################################################*)
134 "############## Make_fun_by_explicit ##############";
135 val c = (the o (parse DiffApp.thy))
136 "Script Make_fun_by_explicit (f_::real) (v_::real) \
137 \ (eqs_::bool list) = \
138 \ (let h_ = (hd o (filter (Testvar m_))) eqs_; \
139 \ e1_ = hd (dropWhile (ident h_) eqs_); \
140 \ vs_ = dropWhile (ident f_) (Var h_); \
141 \ v1_ = hd (dropWhile (ident v_) vs_); \
142 \ (s1::bool list) = (SubProblem (Reals_, [univar,equation],(Isac_,no_met))\
143 \ [bool_ e1_, real_ v1_])\
144 \ in Substitute [(v_1, (Rhs o hd) s_1)] h_)";
147 (*#####################################################--------11.5.02
148 "################ Solve_root_equation #################";
149 (*#####################################################*)
150 val sc = (term_of o the o (parse Test.thy))
151 "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\
152 \ (let e_ = Rewrite square_equation_left True eq_; \
153 \ e_ = Rewrite_Set Test_simplify False e_; \
154 \ e_ = Rewrite_Set rearrange_assoc False e_; \
155 \ e_ = Rewrite_Set isolate_root False e_; \
156 \ e_ = Rewrite_Set Test_simplify False e_; \
158 \ e_ = Rewrite square_equation_left True e_; \
159 \ e_ = Rewrite_Set Test_simplify False e_; \
161 \ e_ = Rewrite_Set norm_equation False e_; \
162 \ e_ = Rewrite_Set Test_simplify False e_; \
163 \ e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\
164 \ e_ = Rewrite_Set Test_simplify False e_ \
166 val ags = map (term_of o the o (parse Test.thy))
167 ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"];
169 ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))",
170 "solveFor x","errorBound (eps = #0)","solutions v_i_"];
171 ----------------------------------------------------------------11.5.02...*)
174 (*#####################################################*)
175 "------- Notlocatable: Free_Solve -------";
176 "------- Notlocatable: Free_Solve -------";
177 "------- Notlocatable: Free_Solve -------";
180 ("Test.thy",["sqroot-test","univariate","equation","test"],
181 ("Test.thy","sqrt-equ-test"));
182 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
183 val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree;
186 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
187 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
188 val nxt = ("Add_Given",Add_Given "solveFor x");
189 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
190 val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
191 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
192 val nxt = ("Add_Find",Add_Find "solutions v_i_");
193 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
194 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
195 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
197 ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]);
198 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
199 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));
200 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
203 val nxt = ("Free_Solve",Free_Solve);
204 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
207 val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)");
208 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
209 (*me ("Begin_Trans" ////*)
212 val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left",""));
213 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
216 val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
217 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
220 val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
221 val (p,_,f,nxt,_,pt) = me nxt p [] pt;
224 (~1,EdUndef,1,Nundef,
225 "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"))
226 then () else raise error "behaviour in root-expl. Free_Solve changed";
227 writeln (pr_ptree pr_short pt);
233 " --- test100: nxt_tac order------------------------------------ ";
234 " --- test100: nxt_tac order------------------------------------ ";
236 val scr as (Script sc) = Script (((inst_abs Test.thy)
237 o term_of o the o (parse thy))
238 "Script Testeq (e_::bool) = \
239 \(While (contains_root e_) Do \
240 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
241 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
242 \ (Try (Repeat (Rewrite radd_0 False)))))\
245 val (dI',pI',mI') = ("Test.thy",e_pblID,
246 ("Test.thy","sqrt-equ-test"));
247 val p = e_pos'; val c = [];
248 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
249 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
250 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
251 val (p,_,_,_,_,pt) = me nxt p c pt;
252 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
253 val (p,_,_,_,_,pt) = me nxt p c pt;
254 val p = ([1],Res):pos';
255 val eq_ = (term_of o the o (parse thy))"e_::bool";
257 val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0";
258 val ve0_= (term_of o the o (parse thy)) ct;
259 val ets0=[([],(Mstep'(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
260 e_term,e_term,Safe)),
261 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
263 " --------------- 1. ---------------------------------------------";
264 val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete;
265 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
268 (*-----------11.5.02: ets disabolished ------------------
270 val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0;
271 (*val l = [R,R,L,R,R,R] : loc_
272 val m' = Rewrite'...("rroot_square_inv",..(sqrt (sqrt (sqrt a))..
275 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
276 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
277 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
278 writeln(ets2str ets1);
279 " --------------- 2. ---------------------------------------------";
280 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
282 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
283 (*val l = [R,R,L,R,R,R] : loc_
284 val m' = Rewrite'...("rroot_square_inv",..,sqrt (sqrt a)..
286 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
287 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
288 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
289 writeln(ets2str ets2);
290 " --------------- 3. ---------------------------------------------";
291 val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
293 val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
294 (*val l = [R,R,R,D,R,D,R,R] : loc_
295 val m' = Rewrite'...("radd_0","")..(#0 + sqrt a = #0)..-> sqrt a = #0*)
297 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
298 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
299 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
300 writeln(ets2str ets3);
301 " --------------- 4. ---------------------------------------------";
302 val Appl m'=applicable_in p pt (Rewrite("square_equation_left",""));
304 val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3;
305 (*val l = [R,R,R,D,L,R,R,R] : loc_
306 val m' = Rewrite'...("square_equation_left"..(sqrt a = #0)..a = #0^#2*)
308 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
309 (*=====*) locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
310 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
312 " --------------- 5. ---------------------------------------------";
313 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
315 writeln (pr_ptree pr_short pt);writeln("result: "^res^
316 "\n===================================================================");
317 "--- test100 nxt_tac order: finished correctly ---------------";
318 "--- test100 nxt_tac order: finished correctly ---------------";
319 "--- test100 nxt_tac order: finished correctly ---------------";
324 " --- test100: order 1 3 1 2 ----------------------------------- ";
325 " --- test100: order 1 3 1 2 ----------------------------------- ";
326 val scr as (Script sc) =
327 Script (((inst_abs Test.thy) o term_of o the o (parse thy))
328 "Script Testeq (e_::bool) = \
329 \While (contains_root e_) Do \
330 \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \
331 \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \
332 \ in Try (Repeat (Rewrite radd_0 False e_))) ");
333 val (dI',pI',mI') = ("Test.thy",e_pblID,
334 ("Test.thy","sqrt-equ-test"));
335 val p = e_pos'; val c = [];
336 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
337 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
338 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
339 val (p,_,_,_,_,pt) = me nxt p c pt;
340 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
341 val (p,_,_,_,_,pt) = me nxt p c pt;
342 val p = ([1],Res):pos';
343 val eq_ = (term_of o the o (parse thy))"e_::bool";
345 val ct = "#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0";
346 val ve0_= (term_of o the o (parse thy)) ct;
347 val ets0=[([],(Mstep'(Script.thy,"bS","",""),[(eq_,ve0_)],[(eq_,ve0_)],
348 e_term,e_term,Safe)),
349 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
351 " --------------- 1. --- test100 order 1 3 1 2 --------------------";
352 val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete;
353 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
355 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
356 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
357 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
358 writeln (ets2str ets1);
359 " --------------- 2. --- test100 order 1 3 1 2 --------------------";
360 val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
361 val Rewrite'(_,_,_,_,("radd_0",""),f,(_,[])) = m';
362 Sign.string_of_term (sign_of (thy)) f;
363 (*"#0 + sqrt (sqrt a) ^^^ #2 = #0"
364 -> AssocWeak .. pt aus ass_up,ass_dn,assy _verworfen_.. nur letzte tac*)
366 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
367 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
368 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
369 " --------------- 3. --- test100 order 1 3 1 2 --------------------";
370 val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv",""));
372 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
373 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
374 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
375 " --------------- 4. --- test100 order 1 3 1 2 --------------------";
376 val Appl m'=applicable_in p pt (Rewrite("square_equation_left",""));
378 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
379 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
380 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
381 if res="a = #0 ^^^ #2"then()else raise error "test100 order 1 3 1 2";
382 " --------------- 5. --- test100 order 1 3 1 2 --------------------";
383 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
384 writeln (pr_ptree pr_short pt);writeln("result: "^res^
385 "\n===================================================================");
386 "--- test100 order 1 3 1 2: finished correctly --------------";
387 "--- test100 order 1 3 1 2: finished correctly --------------";
392 " --- test200: nxt_tac order ------------------------------------- ";
393 " --- test200: nxt_tac order ------------------------------------- ";
395 val scr as (Script sc) =
396 Script (((inst_abs Test.thy) o term_of o the o (parse thy))
397 "Script Testterm (g_::real) = \
399 \ ((Repeat (Rewrite rmult_1 False g_)) Or \
400 \ (Repeat (Rewrite rmult_0 False g_)) Or \
401 \ (Repeat (Rewrite radd_0 False g_))) ");
402 val d = e_rls; (*domain-rls for assod*)
403 val (dI',pI',mI') = ("Test.thy",e_pblID,
404 ("Test.thy","sqrt-equ-test"));
405 val p = e_pos'; val c = [];
406 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
407 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
408 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
409 val (p,_,_,_,_,pt) = me nxt p c pt;
410 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
411 val (p,_,_,_,_,pt) = me nxt p c pt;
412 val p = ([1],Res):pos';
413 val g_ = (term_of o the o (parse thy)) "g_";
415 val ct = "(#0+#0)*(#1*(#1*a))";
416 val vg0_= (term_of o the o (parse thy)) ct;
417 val ets0 = [([],(Mstep'(Script.thy,"sB","",""), [(g_,vg0_)], [(g_,vg0_)],
418 e_term, e_term,Safe)),
419 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
421 " --------------- 1. ---------------------------------------------";
422 val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete;
423 val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
425 val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0;
426 (*val l = [R,R,L,R,L,R,R] : loc_
427 val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*(#1*a)*)
429 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
430 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
431 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
433 " --------------- 2. ---------------------------------------------";
434 val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
436 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
437 (*val l = [R,R,L,R,L,R,R] : loc_
438 val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*a*)
440 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
441 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
442 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
444 " --------------- 3. ---------------------------------------------";
445 val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
447 val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
448 (*val l = [R,R,R,R] : loc_
449 val m' = Rewrite'...("radd_0","") (#0+#0)*a *)
451 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
452 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
453 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
455 " --------------- 4. ---------------------------------------------";
456 val Appl m'=applicable_in p pt (Rewrite("rmult_0",""));
458 val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3;
459 (*al l = [R,R,L,R,R,R] : loc_
460 val m' = Rewrite'...("rmult_0","") #0*a *)
462 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
463 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
464 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
466 " --------------- 5. ---------------------------------------------";
467 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
468 (*al l = [R,R,L,R,R,R] : loc_
469 val m' = Rewrite'...("rmult_0","") #0*a *)
470 writeln (pr_ptree pr_short pt);writeln("result: "^res^
471 "\n===================================================================");
472 "--- test200 nxt_tac order: finished correctly ---------------";
473 "--- test200 nxt_tac order: finished correctly ---------------";
478 " --- test200: order 3 1 1 2 --------------------------------- ";
479 " --- test200: order 3 1 1 2 --------------------------------- ";
480 val p = e_pos'; val c = [];
481 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
482 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
483 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
484 val (p,_,_,_,_,pt) = me nxt p c pt;
485 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
486 val (p,_,_,_,_,pt) = me nxt p c pt;
487 val p = ([1],Res):pos';
488 val g_ = (term_of o the o (parse thy)) "g_";
490 val ct = "(#0+#0)*(#1*(#1*a))";
491 val vg0_= (term_of o the o (parse thy)) ct;
492 val ets0 = [([],(Mstep'(Script.thy,"sB","",""),[(g_,vg0_)],[(g_,vg0_)],
493 e_term,e_term,Safe)),
494 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
496 " --------------- 1. --- test200: order 3 1 1 2 -----------------";
497 val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete;
498 val Appl m'=applicable_in p pt (Rewrite("radd_0",""));
500 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
501 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
502 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
504 " --------------- 2. --- test200: order 3 1 1 2 -----------------";
505 val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
507 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
508 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
509 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
510 if res="#0 * (#1 * a)"then()else raise error "error test200: order 3 1 1 2";
511 " --------------- 3. --- test200: order 3 1 1 2 -----------------";
512 val Appl m'=applicable_in p pt (Rewrite("rmult_1",""));
514 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] =
515 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
516 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
518 " --------------- 4. --- test200: order 3 1 1 2 -----------------";
519 val Appl m'=applicable_in p pt (Rewrite("rmult_0",""));
521 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
522 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
523 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
525 if res="#0"then()else raise error "test200 order 3 1 1 2";
526 " --------------- 5. --- test200: order 3 1 1 2 -----------------";
527 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
528 writeln (pr_ptree pr_short pt);writeln("result: "^res^
529 "\n===================================================================");
530 "--- test200 order 3 1 1 2: finished correctly ---------------";
531 "--- test200 order 3 1 1 2: finished correctly ---------------";
534 ------------------------------------11.5.02: ets disabolished ---*)
535 (* use"test-script-nxt_tac.sml";
539 ### Currently parsed expression could be extremely ambiguous. ----------
541 " --- root-equation: nxt_tac order------------------------------ ";
542 " --- root-equation: nxt_tac order------------------------------ ";
543 val scr as (Script sc) =
544 Script (((inst_abs Test.thy) o term_of o the o (parse thy))
545 "Script Solve_root_equation (e_::bool) (v_::real) (err_::bool) =\
547 \ (While (contains_root e_) Do \
549 \ e_ = Rewrite square_equation_left True e_; \
550 \ e_ = Try (Rewrite_Set Test_simplify False e_); \
551 \ e_ = Try (Rewrite_Set rearrange_assoc False e_); \
552 \ e_ = Try (Rewrite_Set isolate_root False e_) \
553 \ in Try (Rewrite_Set Test_simplify False e_))); \
554 \ e_ = Try (Rewrite_Set norm_equation False e_); \
555 \ e_ = Try (Rewrite_Set Test_simplify False e_); \
556 \ e_ = Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False e_;\
557 \ e_ = Try (Rewrite_Set Test_simplify False e_) \
559 val (dI',pI',mI') = ("Test.thy",e_pblID,
560 ("Test.thy","sqrt-equ-test"));
561 val p = e_pos'; val c = [];
562 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
563 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
564 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
565 val (p,_,_,_,_,pt) = me nxt p c pt;
566 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
567 val (p,_,_,_,_,pt) = me nxt p c pt;
568 val p = ([1],Frm):pos';
570 val bdv_ =(term_of o the o (parse thy))"v_::real";
571 val v_ =(term_of o the o (parse thy))"x::real";
572 val eq_ = (term_of o the o (parse thy))"e_::bool";
573 val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)";
574 val ve0_= (term_of o the o (parse thy)) ct;
575 val env= [(bdv_, v_), (eq_, ve0_)];
576 val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)),
577 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
579 " -------root-equation--- 1.--- nxt_tac-order----------------------";
580 val (pt,_) = cappend_form pt[1]e_istate ct;
582 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
583 (*square_equation_left*)
584 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
585 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
586 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
587 if res = "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"
588 then () else raise error "new behaviour in test-example";
589 writeln (pr_ptree pr_short pt);
590 " -------root-equation--- 2.--- nxt_tac-order----------------------";
591 val ets1 = ets2; val l1 = l2;
593 > val eee = (hd) ets2;
594 > val (_,(_,_,ennv,_,rees,_)) = eee;
596 > Sign.string_of_term (sign_of ( thy)) rees;
598 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
600 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
601 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
602 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
603 if res = "#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))"
604 then () else raise error "new behaviour in test-example";
605 writeln (pr_ptree pr_short pt);
606 " -------root-equation--- 3.--- nxt_tac-order----------------------";
607 val ets1 = ets2; val l1 = l2;
608 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
610 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
611 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
612 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
613 if res = "#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)"
614 then () else raise error "new behaviour in test-example";
615 writeln (pr_ptree pr_short pt);
616 " -------root-equation--- 4.--- nxt_tac-order----------------------";
617 val ets1 = ets2; val l1 = l2;
618 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
620 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
621 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
622 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
623 if res = "sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 * #2)"
624 then () else raise error "new behaviour in test-example";
625 writeln (pr_ptree pr_short pt);
626 " -------root-equation--- 5.--- nxt_tac-order----------------------";
627 val ets1 = ets2; val l1 = l2;
628 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
630 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
631 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
632 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
633 if res = "sqrt (x ^^^ #2 + #5 * x) = #2 + x"
634 then () else raise error "new behaviour in test-example";
635 writeln (pr_ptree pr_short pt);
636 " -------root-equation--- 6.--- nxt_tac-order----------------------";
637 val ets1 = ets2; val l1 = l2;
638 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
639 (*square_equation_left*)
640 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
641 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
642 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
643 if res = "x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2"
644 then () else raise error "new behaviour in test-example";
645 writeln (pr_ptree pr_short pt);
646 " -------root-equation--- 7.--- nxt_tac-order----------------------";
647 val ets1 = ets2; val l1 = l2;
648 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
650 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
651 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
652 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
653 if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"
654 then () else raise error "new behaviour in test-example";
655 writeln (pr_ptree pr_short pt);
656 " -------root-equation--- 8.--- nxt_tac-order----------------------";
657 val ets1 = ets2; val l1 = l2;
658 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
659 (*rearrange_assoc ...<> test-root-equ.sml: norm_equation*)
660 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
661 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
662 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
663 if res = "x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x"
664 (* "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"
665 ...<> test-root-equ.sml*)
666 then () else raise error "new behaviour in test-example";
667 writeln (pr_ptree pr_short pt);
668 " -------root-equation--- 9.--- nxt_tac-order----------------------";
669 val ets1 = ets2; val l1 = l2;
670 (*> Sign.string_of_term (sign_of thy) (go l2 sc);
671 val it = "Rewrite_Set rearrange_assoc False e_" : string*)
673 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
675 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
676 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
677 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
678 if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"
679 then () else raise error "new behaviour in test-example";
680 writeln (pr_ptree pr_short pt);
681 " -------root-equation--- 10.--- nxt_tac-order----------------------";
682 val ets1 = ets2; val l1 = l2;
683 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
685 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
686 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
687 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
688 if res = "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"
689 then () else raise error "new behaviour in test-example";
690 writeln (pr_ptree pr_short pt);
691 " -------root-equation--- 11.--- nxt_tac-order----------------------";
692 val ets1 = ets2; val l1 = l2;
693 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
695 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
696 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
697 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
698 if res = "#-4 + x = #0"
699 then () else raise error "new behaviour in test-example";
700 writeln (pr_ptree pr_short pt);
701 " -------root-equation--- 12.--- nxt_tac-order----------------------";
702 val ets1 = ets2; val l1 = l2;
703 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
705 (*> val eee = (last_elem o drop_last) ets2;
706 > val (_,(mmm,_,ennv,_,rees,_)) = eee;
707 val mmm = Rewrite_Set'
708 ("Test.thy","erls",false,"Test_simplify",# $ # $ Free #,(# $ #,[]))
709 > writeln(subst2str ennv);
710 ["(e_, x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0)"]
711 > Sign.string_of_term (sign_of ( thy)) rees;
712 val it = "#-4 + x = #0" : string*)
714 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
715 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
716 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
717 if res = "x = #0 + #-1 * #-4"
718 then () else raise error "new behaviour in test-example";
719 writeln (pr_ptree pr_short pt);
720 " -------root-equation--- 13.--- nxt_tac-order----------------------";
721 val ets1 = ets2; val l1 = l2;
722 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
724 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
725 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
726 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
728 then () else raise error "new behaviour in test-example";
729 writeln (pr_ptree pr_short pt);
730 " -------root-equation--- 14.--- nxt_tac-order----------------------";
731 val ets1 = ets2; val l1 = l2;
732 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
734 writeln (pr_ptree pr_short pt);
735 writeln("result: "^res^"\n===================================================================");
736 " --- root-equation: nxt_tac order .. finised correctly --------- ";
737 " --- root-equation: nxt_tac order .. finised correctly --------- ";
740 -------------------------------------11.5.02-----*)
741 (*-----------------------------------11.5.02 ets disabolished -------
743 " --- root-equation: 1.norm_equation ------------------------------ ";
744 " --- root-equation: 1.norm_equation ------------------------------ ";
745 val p = e_pos'; val c = [];
746 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
747 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
748 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
749 val (p,_,_,_,_,pt) = me nxt p c pt;
750 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
751 val (p,_,_,_,_,pt) = me nxt p c pt;
752 val p = ([1],Frm):pos';
753 val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)),
755 " -------root-equation--- 1.--- 1.norm_equation----------------------";
756 val (pt,_) = cappend_form pt[1]e_istate ct;
757 val Appl m'= applicable_in p pt (Rewrite_Set "norm_equation");
759 val l1 = (fst o last_elem o drop_last) ets1;
760 (*val l1 = [R,L,R,R,L,R];//////////////test-root_equ, me 11.10.00*)
761 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
762 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
763 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
764 if res = "sqrt (#9 + #4 * x) + #-1 * (sqrt x + sqrt (#5 + x)) = #0"
765 then () else raise error "new behaviour in test-example";
767 val l2 = (fst o last_elem o drop_last) ets2;
768 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
770 " -------root-equation--- 2.--- 1.norm_equation----------------------";
771 (*m'=Rewrite_Set'...,"Test_simplify" *)
772 val l1 = (fst o last_elem o drop_last) ets1;
773 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
774 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
775 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
776 if res = "#-1 * sqrt x + (#-1 * sqrt (#5 + x) + sqrt (#9 + #4 * x)) = #0"
777 then () else raise error "new behaviour in test-example";
780 applicable_in p pt (Rewrite_Set_Inst(["(bdv,v_)"],"isolate_bdv"));
781 val Notappl _ = applicable_in p pt (Rewrite_Set "Test_simplify");
783 val l2 = (fst o last_elem o drop_last) ets2;
784 val Helpless = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
785 (* ~~~~ because isolate_bdv goes without Try *)
786 writeln (pr_ptree pr_short pt);
788 " -------root-equation--- 3.--- 1.norm_equation----------------------";
789 val Appl m'= applicable_in p pt (Rewrite_Set "rearrange_assoc");
791 val l1 = (fst o last_elem o drop_last) ets1;
792 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
793 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
794 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
796 val l2 = (fst o last_elem o drop_last) ets2;
797 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
798 writeln (pr_ptree pr_short pt);
800 " -------root-equation--- 4.--- 1.norm_equation----------------------";
801 (*m' = .. isolate_root*)
802 val l1 = (fst o last_elem o drop_last) ets1;
803 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
804 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
805 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
807 val l2 = (fst o last_elem o drop_last) ets2;
808 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
809 writeln (pr_ptree pr_short pt);
811 " -------root-equation--- 5.--- 1.norm_equation----------------------";
812 (*m' = .. Test_simplify*)
813 val l1 = (fst o last_elem o drop_last) ets1;
814 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
815 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
816 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
818 val l2 = (fst o last_elem o drop_last) ets2;
819 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
820 writeln (pr_ptree pr_short pt);
821 if res="sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)" then ()
822 else raise error "new behaviour in test-example";
824 -------------------------------------11.5.02-----*)
827 (* use"test-script.sml";
836 (* --- test200: calculate -----------------------------------------
837 " --- test200: calculate -----------------------------------------";
838 val scr as (Script sc) =
839 Script (((inst_abs Test.thy) o term_of o the o (parse thy))
840 "Script Testterm (g_::real) = \
841 \Repeat (Calculate plus g_) ");
842 val (dI',pI',mI') = ("Test.thy",e_pblID,
843 ("Test.thy","sqrt-equ-test"));
844 val p = e_pos'; val c = [];
845 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
846 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
847 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
848 val (p,_,_,_,_,pt) = me nxt p c pt;
849 val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
850 val (p,_,_,_,_,pt) = me nxt p c pt;
851 val p = ([1],Res):pos';
852 val g_ = (term_of o the o (parse thy)) "g_";
853 val vg_= (term_of o the o (parse thy)) "#1+#2";
854 val env = [(g_,vg_)];
857 (* --------------- 1. ---------------------------------------------*)
858 val (pt,_) = cappend_atomic pt [1] e_istate ""
859 (Rewrite("test","")) "#1+#2" Complete;
860 val Appl m'=applicable_in p pt (Calculate "plus");
862 val NextStep(l,m') = nxt_tac "Test.thy" (pt,p) scr ets l;
863 (*val l = [R,R,R,R] : loc_
864 val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*)
866 val ets = (l,mstep'2etac m')::ets;
867 (* --------------- 2. ---------------------------------------------*)
868 val (pt,_) = cappend_atomic pt [1] e_istate ""
869 (Rewrite("test","")) "#3" Complete;
871 val Helpless = nxt_tac "Test.thy" (pt,p) scr ets l;
872 (*val l = [R,R,R,R] : loc_
873 val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*)
877 (* --- test200: Test_simplify -----------------------------------
879 val scr as (Script sc) =
880 Script (((inst_abs Test.thy) o term_of o the o (parse thy))
881 "Script Testterm (g_::real) = \
883 \ ((Repeat (Rewrite radd_mult_distrib2 False g_)) Or \
884 \ (Repeat (Rewrite rdistr_right_assoc False g_)) Or \
885 \ (Repeat (Rewrite rdistr_right_assoc_p False g_)) Or \
886 \ (Repeat (Rewrite rdistr_div_right False g_)) Or \
887 \ (Repeat (Rewrite rbinom_power_2 False g_)) Or \
888 \ (Repeat (Rewrite radd_commute False g_)) Or \
889 \ (Repeat (Rewrite radd_left_commute False g_)) Or \
890 \ (Repeat (Rewrite radd_assoc False g_)) Or \
891 \ (Repeat (Rewrite rmult_commute False g_)) Or \
892 \ (Repeat (Rewrite rmult_left_commute False g_)) Or \
893 \ (Repeat (Rewrite rmult_assoc False g_)) Or \
894 \ (Repeat (Rewrite radd_real_const_eq False g_)) Or \
895 \ (Repeat (Rewrite radd_real_const False g_)) Or \
896 \ (Repeat (Calculate plus g_)) Or \
897 \ (Repeat (Calculate times g_)) Or \
898 \ (Repeat (Rewrite rcollect_right False g_)) Or \
899 \ (Repeat (Rewrite rcollect_one_left False g_)) Or \
900 \ (Repeat (Rewrite rcollect_one_left_assoc False g_)) Or \
901 \ (Repeat (Rewrite rcollect_one_left_assoc_p False g_))) ");
904 "%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\
905 \ (Repeat (Calculate cancel g_)) Or \n\
906 \ (Repeat (Calculate pow g_)) Or \n\
907 \%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\
908 \%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set";
911 (*-------------------------------------11.5.02 ets disablished -------
913 " --- check_elementwise ------------------------------ ";
914 " --- check_elementwise ------------------------------ ";
916 val scr as (Script sc) = Script (((inst_abs Test.thy)
917 o term_of o the o (parse thy))
918 "Script Testchk (e_::bool) (v_::real) = \
919 \ (let e_ = Try (Rewrite_Set Test_simplify False e_); \
920 \ (L_::real list) = Mstep subproblem_equation_dummy; \
921 \ L_ = Mstep solve_equation_dummy \
922 \ in Check_elementwise L_ {(v_::real). Assumptions})");
923 val (dI',pI',mI') = ("Test.thy",e_pblID,
924 ("Test.thy","sqrt-equ-test"));
925 val p = e_pos'; val c = [];
926 val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI')));
927 val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree;
928 val nxt = ("Specify_Domain",Specify_Domain "Test.thy");
929 val (p,_,_,_,_,pt) = me nxt p c pt;
930 val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*)
931 val (p,_,_,_,_,pt) = me nxt p c pt;
932 val pt = union_asm pt [] [("#0 <= sqrt x + sqrt (#5 + x)",[11]),
933 ("#0 <= #9 + #4 * x",[22]),
934 ("#0 <= x ^^^ #2 + #5 * x",[33]),
935 ("#0 <= #2 + x",[44])];
936 val p = ([1],Res):pos';
937 val eq_ = (term_of o the o (parse thy))"e_::bool";
939 val ve0_= (term_of o the o (parse thy)) ct;
940 val v_ = (term_of o the o (parse thy))"v_::real";
941 val xx = (term_of o the o (parse thy))"x::real";
942 val env0= [(eq_,ve0_),(v_,xx)];
944 val ets0=[([],(Mstep'(Script.thy,"BS","",""),env0,env0,e_term,e_term,Safe)),
945 ([],(User', [], [], e_term, e_term,Sundef))]:ets;
947 val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete;
948 " --------------- 1. ---------------------------------------------";
949 val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify");
951 val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0;
952 (*val l1 = [R,L,R,R] : loc_*)
953 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] =
954 locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0;
955 (*val ets1 = [([R,L,R,R],(Rewrite_Set' #,[#],[#],Free #,# $ #,Safe)),..*)
956 val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)];
957 writeln(ets2str ets1);
958 " --------------- 2. ---------------------------------------------";
959 val Appl m'=applicable_in p pt (Mstep "subproblem_equation_dummy");
961 val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1;
962 (*val l2 = [R,R,D,L,R] : loc_|| val m' = Mstep' ("x = #4",...*)
963 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] =
964 locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1;
965 (*val ets2 =[([R,R,D,L,R],(Mstep' ..subpbl..,[#],[#],Const #,# $ #,Safe)),..*)
966 val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)];
967 writeln(ets2str ets2);
968 " --------------- 3. ---------------------------------------------";
969 val Appl m'=applicable_in p pt (Mstep "solve_equation_dummy");
971 val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2;
972 (*val l3 = [R,R,D,R,D,L,R] : loc_
973 val m' = Mstep'("subproblem_equation_dummy (x = #4)",..*)
974 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = (*@@@*)
975 locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2;
976 (*val ets3 = [([R,R,D,R,D,L,R], (Mstep' (..,"solve_equation_dummy",..*)
977 val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)];
978 writeln(ets2str ets3);
979 " --------------- 4. ---------------------------------------------";
980 val Appl (m' as (Check_elementwise' (consts,"Assumptions",consts'))) =
981 applicable_in p pt (Check_elementwise "Assumptions");
983 val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3;
984 (*val l4 = [R,R,D,R,D,R,D] : loc_ val m' = Check_elementwise' (Const (#,#) $ ...*)
986 val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] =
987 locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3;
988 (*val ets4 = [([R,R,D,R,D,R,D], (Check_elementwise' (# $ #,"Assumptions",Const #),..*)
989 val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)];
990 " --------------- 5. ---------------------------------------------";
991 val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4;
993 writeln (pr_ptree pr_short pt);writeln("result: "^res^
994 "\n===================================================================");
996 -------------------------------------11.5.02-----*)