1 (* use"../systest/scriptnew.sml";
2 use"systest/scriptnew.sml";
7 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
8 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
9 " --- test 11.5.02 Testeq: let e_e =... in [e_] ------------------ ";
10 " _________________ me + nxt_step from script ___________________ ";
11 " _________________ me + sqrt-equ-test: 1.norm_equation ________ ";
12 " _________________ equation with x =(-12)/5, but L ={} ------- ";
13 "------------------ script with Map, Subst (biquadr.equ.)---------";
19 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
20 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
21 " --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ ";
23 (prep_pbt Test.thy "pbl_testss" [] e_pblID
25 []:(string * string list) list,
28 (prep_pbt Test.thy "pbl_testss_term" [] e_pblID
29 (["met_testterm","tests"],
30 [("#Given" ,["realTestGiven g_"]),
31 ("#Find" ,["realTestFind f_"])
35 (prep_met Test.thy "met_test_simp" [] e_metID
36 (*test for simplification*)
37 (["Test","met_testterm"]:metID,
38 [("#Given" ,["realTestGiven g_"]),
39 ("#Find" ,["realTestFind f_"])
41 {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[],
42 crls=tval_rls, nrls=e_rls(*,
43 asm_rls=[],asm_thm=[]*)},
44 "Script Testterm (g_::real) = \
46 \ ((Repeat (Rewrite rmult_1 False)) Or\
47 \ (Repeat (Rewrite rmult_0 False)) Or\
48 \ (Repeat (Rewrite radd_0 False))) g_"
50 val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"];
51 val (dI',pI',mI') = ("Test.thy",["met_testterm","tests"],
52 ["Test","met_testterm"]);
53 (*val p = e_pos'; val c = [];
54 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
55 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
56 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
57 val (p,_,f,nxt,_,pt) = me nxt p c pt;
58 val (p,_,f,nxt,_,pt) = me nxt p c pt;
59 val (p,_,f,nxt,_,pt) = me nxt p c pt;
60 val (p,_,f,nxt,_,pt) = me nxt p c pt;
61 val (p,_,f,nxt,_,pt) = me nxt p c pt;
62 val (p,_,f,nxt,_,pt) = me nxt p c pt;
63 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met_testterm"))*)
64 (*----script 111 ------------------------------------------------*)
65 val (p,_,f,nxt,_,pt) = me nxt p c pt;
66 (*"(#0 + #0) * (#1 * (#1 * a))" nxt= Rewrite ("rmult_1",*)
67 (*----script 222 ------------------------------------------------*)
68 val (p,_,f,nxt,_,pt) = me nxt p c pt;
69 (*"(#0 + #0) * (#1 * a)" nxt= Rewrite ("rmult_1",*)
70 (*----script 333 ------------------------------------------------*)
71 val (p,_,f,nxt,_,pt) = me nxt p c pt;
72 (*"(#0 + #0) * a" nxt= Rewrite ("radd_0",*)
73 (*----script 444 ------------------------------------------------*)
74 val (p,_,f,nxt,_,pt) = me nxt p c pt;
76 (*----script 555 ------------------------------------------------*)
77 val (p,_,f,nxt,_,pt) = me nxt p c pt;
79 if p=([4],Res) then ()
80 else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p));
81 (*----script 666 ------------------------------------------------*)
82 val (p,_,f,nxt,_,pt) = me nxt p c pt;
84 if nxt=("End_Proof'",End_Proof') then ()
85 else raise error "new behaviour in 30.4.02 Testterm: End_Proof";
91 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
92 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
93 " --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ ";
95 (prep_pbt Test.thy "pbl_testss_eq" [] e_pblID
96 (["met_testeq","tests"],
97 [("#Given" ,["boolTestGiven e_e"]),
98 ("#Find" ,["boolTestFind v_i_"])
103 (prep_met Test.thy "met_test_eq1" [] e_metID
104 (["Test","testeq1"]:metID,
105 [("#Given",["boolTestGiven e_e"]),
107 ("#Find" ,["boolTestFind v_i_"])
109 {rew_ord'="tless_true",rls'=tval_rls,
110 srls=append_rls "testeq1_srls" e_rls
111 [Calc ("Test.contains'_root", eval_contains_root"")],
112 prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls
113 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
114 "Script Testeq (e_e::bool) = \
115 \(While (contains_root e_e) Do \
116 \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \
117 \ (Try (Repeat (Rewrite square_equation_left True))) @@ \
118 \ (Try (Repeat (Rewrite radd_0 False)))))\
122 val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)",
123 "boolTestFind v_i_"];
124 val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],
126 val Script sc = (#scr o get_met) ["Test","testeq1"];
128 (*val p = e_pos'; val c = [];
129 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
130 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
131 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
132 val (p,_,f,nxt,_,pt) = me nxt p c pt;
133 val (p,_,f,nxt,_,pt) = me nxt p c pt;
134 val (p,_,f,nxt,_,pt) = me nxt p c pt;
135 val (p,_,f,nxt,_,pt) = me nxt p c pt;
136 val (p,_,f,nxt,_,pt) = me nxt p c pt;
137 val (p,_,f,nxt,_,pt) = me nxt p c pt;
138 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *)
139 val (p,_,f,nxt,_,pt) = me nxt p c pt;
140 val (p,_,f,nxt,_,pt) = me nxt p c pt;
141 val (p,_,f,nxt,_,pt) = me nxt p c pt;
142 (*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0"))
143 val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*)
144 val (p,_,f,nxt,_,pt) = me nxt p c pt;
146 val (p,_,f,nxt,_,pt) = me nxt p c pt;
147 (*** No such constant: "Test.contains'_root" *)
149 val (p,_,f,nxt,_,pt) = me nxt p c pt;
150 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso
151 nxt=("End_Proof'",End_Proof') then ()
152 else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@";
157 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
158 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
159 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- ";
161 (prep_met Test.thy "met_test_let" [] e_metID
162 (["Test","testlet"]:metID,
163 [("#Given",["boolTestGiven e_e"]),
165 ("#Find" ,["boolTestFind v_i_"])
167 {rew_ord'="tless_true",rls'=tval_rls,
168 srls=append_rls "testlet_srls" e_rls
169 [Calc ("Test.contains'_root",eval_contains_root"")],
170 prls=e_rls,calc=[], crls=tval_rls, nrls=e_rls
171 (*,asm_rls=[],asm_thm=[("square_equation_left","")]*)},
172 "Script Testeq2 (e_e::bool) = \
174 \ ((While (contains_root e_e) Do \
175 \ (Rewrite square_equation_left True))\
179 val Script sc = (#scr o get_met) ["Test","testlet"];
180 writeln(term2str sc);
181 val fmz = ["boolTestGiven (sqrt a = 0)",
182 "boolTestFind v_i_"];
183 val (dI',pI',mI') = ("Test.thy",["met_testeq","tests"],
185 (*val p = e_pos'; val c = [];
186 val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
187 val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree;*)
188 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
189 val (p,_,f,nxt,_,pt) = me nxt p c pt;
190 val (p,_,f,nxt,_,pt) = me nxt p c pt;
191 val (p,_,f,nxt,_,pt) = me nxt p c pt;
192 val (p,_,f,nxt,_,pt) = me nxt p c pt;
193 val (p,_,f,nxt,_,pt) = me nxt p c pt;
194 val (p,_,f,nxt,_,pt) = me nxt p c pt;
195 (*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*)
196 val (p,_,f,nxt,_,pt) = me nxt p c pt;
197 val (p,_,f,nxt,_,pt) = me nxt p c pt;
198 val (p,_,f,nxt,_,pt) = (me nxt p c pt) handle e => print_exn e;
199 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso
200 nxt=("End_Proof'",End_Proof') then ()
201 else raise error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]";
206 " _________________ me + nxt_step from script _________________ ";
207 " _________________ me + nxt_step from script _________________ ";
208 " _________________ me + nxt_step from script _________________ ";
209 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
210 "solveFor x","solutions L"];
212 ("Test.thy",["sqroot-test","univariate","equation","test"],
213 ["Test","sqrt-equ-test"]);
214 val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
215 writeln(term2str sc);
218 (*val p = e_pos'; val c = [];
219 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
220 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
221 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
223 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
226 Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
227 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
229 (* val nxt = ("Add_Given",Add_Given "solveFor x");*)
230 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
232 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
234 (* val nxt = ("Add_Find",Add_Find "solutions L");*)
235 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
237 (* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)
238 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
242 Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
243 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
245 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
246 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
248 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
249 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
251 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
252 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
254 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
255 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
257 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
258 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
260 (* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*)
261 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
263 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
264 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
266 (* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*)
267 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
269 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
270 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
272 (* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*)
273 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
275 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
276 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
278 (* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*)
279 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
281 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
282 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
284 (* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*)
285 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
287 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
290 (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*)
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
292 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
293 then raise error "scriptnew.sml 1: me + tacs from script: new behaviour"
296 (* val nxt = ("End_Proof'",End_Proof');*)
297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
299 writeln (pr_ptree pr_short pt);
300 writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^
301 "\n=============================================================");
302 (*get_obj g_asm pt [];
303 val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*)
309 " _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
310 " _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
311 " _________________ me + sqrt-equ-test: 1.norm_equation _________________ ";
312 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
313 "solveFor x","errorBound (eps=0)",
316 ("Test.thy",["sqroot-test","univariate","equation","test"],
317 ["Test","sqrt-equ-test"]);
318 val Script sc = (#scr o get_met) ["Test","sqrt-equ-test"];
319 (writeln o term2str) sc;
321 (*val p = e_pos'; val c = [];
322 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
323 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
324 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
326 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
327 (* val nxt = ("Add_Given",
328 Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*)
329 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
331 (* val nxt = ("Add_Given",Add_Given "solveFor x");*)
332 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
334 (* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*)
335 (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt;*)
337 (* val nxt = ("Add_Find",Add_Find "solutions L");*)
338 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
340 (* val nxt = ("Specify_Theory",Specify_Theory "Test.thy");*)
341 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
343 (* val nxt = ("Specify_Problem",
344 Specify_Problem ["sqroot-test","univariate","equation","test"]);*)
345 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
347 (* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*)
348 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
350 (* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*)
351 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
352 (*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"*)
353 "--- !!! x1 --- 1.norm_equation";
354 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
355 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
356 "--- !!! x2 --- 1.norm_equation";
357 (*meNEW: "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2" -- NICHT norm_equation!!*)
358 (*meOLD: "sqrt (9 + 4 * x) + -1 * (sqrt x + sqrt (5 + x)) = 0"*)
359 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
360 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
361 (*"-1 * sqrt x + (-1 * sqrt (5 + x) + sqrt (9 + 4 * x)) = 0"*)
362 (*(me nxt p [1] pt) handle e => print_exn_G e;*)
363 "--- !!! x3 --- 1.norm_equation";
364 (*val nxt = ("Empty_Tac",Empty_Tac) ### helpless*)
365 (*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
366 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
367 "--- !!! x4 --- 1.norm_equation";
368 (*"-1 * sqrt x + -1 * sqrt (5 + x) + sqrt (9 + 4 * x) = 0"*)
369 (*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*)
370 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
371 "--- !!! x5 --- 1.norm_equation";
372 (*"sqrt (9 + 4 * x) = 0 + -1 * (-1 * sqrt x + -1 * sqrt (5 + x))"*)
373 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*)
374 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
376 (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check:
377 if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)"))
378 then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test";
379 #################################################*)
381 (* use"../tests/scriptnew.sml";
384 " _________________ equation with x =(-12)/5, but L ={} ------- ";
386 val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))",
387 "solveFor x","errorBound (eps=0)",
390 ("Test.thy",["sqroot-test","univariate","equation","test"],
391 ["Test","square_equation"]);
393 (*val p = e_pos'; val c = [];
394 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
395 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
396 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
397 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
398 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
399 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
400 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
401 (*val nxt = ("Apply_Method",Apply_Method ["Test","square_equation"])*)
402 val (p,_,f,nxt,_,pt) = me nxt p c pt;
403 (*val nxt = "square_equation_left",
404 "[| 0 <= ?a; 0 <= ?b |] ==> (sqrt ?a = ?b) = (?a = ?b ^^^ 2)"))*)
405 get_assumptions_ pt p;
406 (*it = [] : string list;*)
408 val (p,_,f,nxt,_,pt) = me nxt p c pt;
409 trace_rewrite:=false;
410 val asms = get_assumptions_ pt p;
411 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
412 (str2term "0 <= x",[1]),
413 (str2term "0 <= -3 + x",[1])] then ()
414 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 1";
416 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
417 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
418 (*val nxt = Rewrite ("square_equation_left", *)
419 val asms = get_assumptions_ pt p;
420 [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1])];
421 val (p,_,f,nxt,_,pt) = me nxt p c pt;
422 val asms = get_assumptions_ pt p;
423 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
424 (str2term "0 <= x",[1]),
425 (str2term "0 <= -3 + x",[1]),
426 (str2term "0 <= x ^^^ 2 + -3 * x",[6]),
427 (str2term "0 <= 6 + x",[6])] then ()
428 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 2";
430 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
431 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
432 val (p,_,f,nxt,_,pt) = me nxt p c pt;
433 (*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*)
434 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
435 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
436 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
437 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
438 (*val nxt = ("Apply_Method",Apply_Method ["Test","solve_linear"])*)
439 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
440 val (p,_,f,nxt,_,pt) = me nxt p c pt;
442 ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*)
443 val asms = get_assumptions_ pt p;
445 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 3";
446 val (p,_,f,nxt,_,pt) = me nxt p c pt;
447 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*)
449 val asms = get_assumptions_ pt p;
450 if asms = [(str2term "0 <= 9 + 4 * x",[1]),
451 (str2term "0 <= x",[1]),
452 (str2term "0 <= -3 + x",[1]),
453 (str2term "0 <= x ^^^ 2 + -3 * x",[6]),
454 (str2term "0 <= 6 + x",[6])] then ()
456 error "scriptnew.sml: diff.behav. at Check_elementwise [x = -12 / 5]";
458 val (p,_,f,nxt,_,pt) = me nxt p c pt;
459 (*val nxt = Check_Postcond ["sqroot-test","univariate","equation","test"])*)
460 val asms = get_assumptions_ pt p;
461 [("0 <= 9 + 4 * x",[1]),("0 <= x",[1]),("0 <= -3 + x",[1]),
462 ("0 <= x ^^^ 2 + -3 * x",[6]),("0 <= 6 + x",[6]),
463 ("0 <= 6 + -12 / 5 &\n0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5) &\n0 <= -3 + -12 / 5 & 0 <= -12 / 5 & 0 <= 9 + 4 * (-12 / 5)",
467 val (p,_,f,nxt,_,pt) = me nxt p c pt;
468 val Form' (FormKF (_,_,_,_,ff)) = f;
469 if ff="[x = -12 / 5]"
470 then writeln("there should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\nthere should be L = []\n")
471 else raise error "diff.behav. in scriptnew.sml; root-eq: L = []";
473 val asms = get_assumptions_ pt p;
474 if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]),
475 (str2term "0 <= -12 / 5", []),
476 (str2term "0 <= -3 + -12 / 5", []),
477 (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []),
478 (str2term "0 <= 6 + -12 / 5", [])] then ()
479 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 4";
482 "------------------ script with Map, Subst (biquadr.equ.)---------";
483 "------------------ script with Map, Subst (biquadr.equ.)---------";
484 "------------------ script with Map, Subst (biquadr.equ.)---------";
487 (*GoOn.5.03. script with Map, Subst (biquadr.equ.)
488 val scr = Script (((inst_abs thy) o term_of o the o (parse thy))
489 "Script Biquadrat_poly (e_e::bool) (v_::real) = \
490 \(let e_e = Substitute [(v_^^^4, v_0_^^^2),(v_^^^2, v_0_)] e_; \
491 \ L_0_ = (SubProblem (PolyEq_,[univariate,equation], [no_met]) \
492 \ [BOOL e_e, REAL v_0_]); \
493 \ L_i_ = Map (((Substitute [(v_0_, v_^^^2)]) @@ \
494 \ ((Rewrite real_root_positive False) Or \
495 \ (Rewrite real_root_negative False)) @@ \