75 (*"#0 * a"*) |
75 (*"#0 * a"*) |
76 (*----script 555 ------------------------------------------------*) |
76 (*----script 555 ------------------------------------------------*) |
77 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
77 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
78 (*"#0"*) |
78 (*"#0"*) |
79 if p=([4],Res) then () |
79 if p=([4],Res) then () |
80 else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p)); |
80 else error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p)); |
81 (*----script 666 ------------------------------------------------*) |
81 (*----script 666 ------------------------------------------------*) |
82 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
82 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
83 (*"#0"*) |
83 (*"#0"*) |
84 if nxt=("End_Proof'",End_Proof') then () |
84 if nxt=("End_Proof'",End_Proof') then () |
85 else raise error "new behaviour in 30.4.02 Testterm: End_Proof"; |
85 else error "new behaviour in 30.4.02 Testterm: End_Proof"; |
86 |
86 |
87 |
87 |
88 |
88 |
89 |
89 |
90 |
90 |
147 (*** No such constant: "Test.contains'_root" *) |
147 (*** No such constant: "Test.contains'_root" *) |
148 |
148 |
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
149 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
150 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso |
150 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso |
151 nxt=("End_Proof'",End_Proof') then () |
151 nxt=("End_Proof'",End_Proof') then () |
152 else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@"; |
152 else error "different behaviour test 9.5.02 Testeq: While Try Repeat @@"; |
153 |
153 |
154 |
154 |
155 |
155 |
156 |
156 |
157 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- "; |
157 " --- test 11.5.02 Testeq: let e_e =... in [e_] --------- "; |
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
196 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
197 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; |
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 |
199 if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso |
200 nxt=("End_Proof'",End_Proof') then () |
200 nxt=("End_Proof'",End_Proof') then () |
201 else raise error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]"; |
201 else error "different behaviour in test 11.5.02 Testeq: let e_e =... in [e_]"; |
202 |
202 |
203 |
203 |
204 |
204 |
205 |
205 |
206 " _________________ me + nxt_step from script _________________ "; |
206 " _________________ me + nxt_step from script _________________ "; |
288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
288 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
289 "--- 14<> ---"; |
289 "--- 14<> ---"; |
290 (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*) |
290 (* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*) |
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
291 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
292 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
292 if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) |
293 then raise error "scriptnew.sml 1: me + tacs from script: new behaviour" |
293 then error "scriptnew.sml 1: me + tacs from script: new behaviour" |
294 else (); |
294 else (); |
295 "--- 15<> ---"; |
295 "--- 15<> ---"; |
296 (* val nxt = ("End_Proof'",End_Proof');*) |
296 (* val nxt = ("End_Proof'",End_Proof');*) |
297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
297 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
298 |
298 |
373 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
373 (* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) |
374 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
374 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; |
375 |
375 |
376 (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check: |
376 (*FIXXXXXXXXXXXXXXXXXXXXXXXME reestablish check: |
377 if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)")) |
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"; |
378 then() else error "new behaviour in test-example 1.norm sqrt-equ-test"; |
379 #################################################*) |
379 #################################################*) |
380 |
380 |
381 (* use"../tests/scriptnew.sml"; |
381 (* use"../tests/scriptnew.sml"; |
382 *) |
382 *) |
383 |
383 |
409 trace_rewrite:=false; |
409 trace_rewrite:=false; |
410 val asms = get_assumptions_ pt p; |
410 val asms = get_assumptions_ pt p; |
411 if asms = [(str2term "0 <= 9 + 4 * x",[1]), |
411 if asms = [(str2term "0 <= 9 + 4 * x",[1]), |
412 (str2term "0 <= x",[1]), |
412 (str2term "0 <= x",[1]), |
413 (str2term "0 <= -3 + x",[1])] then () |
413 (str2term "0 <= -3 + x",[1])] then () |
414 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 1"; |
414 else error "scriptnew.sml diff.behav. in sqrt assumptions 1"; |
415 |
415 |
416 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
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; |
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", *) |
418 (*val nxt = Rewrite ("square_equation_left", *) |
419 val asms = get_assumptions_ pt p; |
419 val asms = get_assumptions_ pt p; |
423 if asms = [(str2term "0 <= 9 + 4 * x",[1]), |
423 if asms = [(str2term "0 <= 9 + 4 * x",[1]), |
424 (str2term "0 <= x",[1]), |
424 (str2term "0 <= x",[1]), |
425 (str2term "0 <= -3 + x",[1]), |
425 (str2term "0 <= -3 + x",[1]), |
426 (str2term "0 <= x ^^^ 2 + -3 * x",[6]), |
426 (str2term "0 <= x ^^^ 2 + -3 * x",[6]), |
427 (str2term "0 <= 6 + x",[6])] then () |
427 (str2term "0 <= 6 + x",[6])] then () |
428 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 2"; |
428 else error "scriptnew.sml diff.behav. in sqrt assumptions 2"; |
429 |
429 |
430 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt; |
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; |
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; |
432 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
433 (*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*) |
433 (*val nxt = Subproblem ("Test.thy",["linear","univariate","equation","test"*) |
440 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
440 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
441 (*val nxt = |
441 (*val nxt = |
442 ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*) |
442 ("Check_Postcond",Check_Postcond ["linear","univariate","equation","test"])*) |
443 val asms = get_assumptions_ pt p; |
443 val asms = get_assumptions_ pt p; |
444 if asms = [] then () |
444 if asms = [] then () |
445 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 3"; |
445 else error "scriptnew.sml diff.behav. in sqrt assumptions 3"; |
446 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
446 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
447 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*) |
447 (*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*) |
448 |
448 |
449 val asms = get_assumptions_ pt p; |
449 val asms = get_assumptions_ pt p; |
450 if asms = [(str2term "0 <= 9 + 4 * x",[1]), |
450 if asms = [(str2term "0 <= 9 + 4 * x",[1]), |
466 |
466 |
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
467 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
468 val Form' (FormKF (_,_,_,_,ff)) = f; |
468 val Form' (FormKF (_,_,_,_,ff)) = f; |
469 if ff="[x = -12 / 5]" |
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") |
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 = []"; |
471 else error "diff.behav. in scriptnew.sml; root-eq: L = []"; |
472 |
472 |
473 val asms = get_assumptions_ pt p; |
473 val asms = get_assumptions_ pt p; |
474 if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]), |
474 if asms = [(str2term "0 <= 9 + 4 * (-12 / 5)",[]), |
475 (str2term "0 <= -12 / 5", []), |
475 (str2term "0 <= -12 / 5", []), |
476 (str2term "0 <= -3 + -12 / 5", []), |
476 (str2term "0 <= -3 + -12 / 5", []), |
477 (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []), |
477 (str2term "0 <= (-12 / 5) ^^^ 2 + -3 * (-12 / 5)", []), |
478 (str2term "0 <= 6 + -12 / 5", [])] then () |
478 (str2term "0 <= 6 + -12 / 5", [])] then () |
479 else raise error "scriptnew.sml diff.behav. in sqrt assumptions 4"; |
479 else error "scriptnew.sml diff.behav. in sqrt assumptions 4"; |
480 |
480 |
481 |
481 |
482 "------------------ script with Map, Subst (biquadr.equ.)---------"; |
482 "------------------ script with Map, Subst (biquadr.equ.)---------"; |
483 "------------------ script with Map, Subst (biquadr.equ.)---------"; |
483 "------------------ script with Map, Subst (biquadr.equ.)---------"; |
484 "------------------ script with Map, Subst (biquadr.equ.)---------"; |
484 "------------------ script with Map, Subst (biquadr.equ.)---------"; |