# HG changeset patch # User agriesma # Date 1050595263 -7200 # Node ID 90390fecbe74d2ff5a4754aff24eb8fc43b96691 # Parent 53c9925d2d9cf47cbd37b61b8e0fb729b704bebb neues cvs-verzeichnis diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/FE-KE.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/FE-KE.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,403 @@ +(* use"test-FE-KE.sml"; + W.N.16.4.00 + *) + +(*contents*) +" _________________ stdin: tutor active_________________ "; +" _________________ stdin: student active_________________ "; +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +" ------------- test-FE-KE.sml: test100 ------------- "; +" _________________ stdin: root_equ: Auto ________________ "; +(*contents*) + + + + +(*#########################################################*) +" _________________ stdin: tutor active_________________ "; +" _________________ stdin: tutor active_________________ "; +" _________________ stdin: tutor active_________________ "; +" _________________ stdin: tutor active_________________ "; +" _________________ stdin: tutor active_________________ "; +" _________________ stdin: tutor active_________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +set_dstate 1 test_hide 0 2;(*PutRule,TskipS..PutRuleRes,Tt..*) +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,PpcKF (_,_,_,_,ppc),req],_) = +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- s2 ---"; +StdinSML 1 1 ~1 ~1 (Command Accept); +(*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*) +"--- s3 ---"; +StdinSML 1 1 ~2 ~2 (Command Accept); +(*RuleFK (Add_Given "solveFor x")*) +"--- s4 ---"; +StdinSML 1 1 ~3 ~3 (Command Accept); +(*RuleFK (Add_Given "errorBound (eps = #0)")*) +"--- s5 ---"; +StdinSML 1 1 ~4 ~4 (Command Accept); +(*RuleFK (Add_Find "solutions L")*) +"--- s6 ---"; +StdinSML 1 1 ~5 ~5 (Command Accept); +(*RuleFK (Specify_Domain "Test.thy")*) +"--- s7 ---"; +StdinSML 1 1 ~6 ~6 (Command Accept); +(*RuleFK (Specify_Problem ["sqroot-test","univariate","equation","test"])*) +"--- s8 ---"; +StdinSML 1 1 ~7 ~7 (Command Accept); +(*RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))*) +"--- s9 ---"; +val (_,1,1,~8,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~8 ~8 (Command Accept); +if ct'="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" andalso +r = Apply_Method ("Test.thy","sqrt-equ-test") +then () else raise error "new behaviour in test-example"; +(*RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))*) + +"--- 1 ---"; +val (_,1,1,~9,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~9 ~9 (Command Accept); +(*RuleFK (Rewrite ("square_equation_left",""))*) +"--- 2 ---"; +val (_,1,1,~10,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~10 ~10 (Command Accept); +(*RuleFK (Rewrite_Set "Test_simplify")*) +"--- 3 ---"; +val (_,1,1,~11,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~11 ~11 (Command Accept); +(*RuleFK (Rewrite_Set "rearrange_assoc")*) +"--- 4 ---"; +val (_,1,1,~12,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~12 ~12 (Command Accept); +(*RuleFK (Rewrite_Set "isolate_root")*) +"--- 5 ---"; +val (_,1,1,~13,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~13 ~13 (Command Accept); +(*RuleFK (Rewrite_Set "Test_simplify")*) +"--- 6 ---"; +val (_,1,1,~14,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~14 ~14 (Command Accept); +(*RuleFK (Rewrite ("square_equation_left",""))*) +"--- 7 ---"; +val (_,1,1,~15,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~15 ~15 (Command Accept); +(*RuleFK (Rewrite_Set "Test_simplify")*) +"--- 8 ---"; +val (_,1,1,~16,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~16 ~16 (Command Accept); +(*val r = Rewrite_Set "rearrange_assoc"*) +"--- 9 ---"; +val (_,1,1,~17,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~17 ~17 (Command Accept); +(*RuleFK (Rewrite_Set "Test_simplify")*) +"--- 10 ---"; +val (_,1,1,~18,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~18 ~18 (Command Accept); +(*val r = Rewrite_Set "norm_equation"*) +"--- 11 ---"; +val (_,1,1,~19,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~19 ~19 (Command Accept); +(*RuleFK (Rewrite_Set "Test_simplify")*) +"--- 13 ---"; +val (_,1,1,~20,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~20 ~20 (Command Accept); +(*RuleFK (Rewrite_Set_Inst ([(#,#)],"isolate_bdv"))*) +"--- 14 ---"; +val (_,1,1,~21,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~21 ~21 (Command Accept); +(*RuleFK (Rewrite_Set "Test_simplify")*) +"--- 15 ---"; +val (_,1,1,~22,[],[RuleKF (_,r),FormKF (_,_,_,_,ct'),req],_) = +StdinSML 1 1 ~22 ~22 (Command Accept); +"--- 16 ---"; +val (_,1,1,~23,[],[req,End_Proof],_) = +StdinSML 1 1 ~23 ~23 (Command Accept); + +(* +"=====================";======================= + use"test-FE-KE.sml"; + *) + + +(*#########################################################*) +" _________________ stdin: student active_________________ "; +" _________________ stdin: student active_________________ "; +" _________________ stdin: student active_________________ "; +" _________________ stdin: student active_________________ "; +" _________________ stdin: student active_________________ "; +" _________________ stdin: student active_________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +set_dstate 1 test_hide 4 1;(*SelRule,St..PutRuleRes,TskipS..*) +(*SelRule WORKS BY CAHCNE, and wrong, IN SPECIFY*) +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,PpcKF (_,_,_,_,f), Select _, req],_) = + StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- s2 ---"; +(*val (_,1,1,~1,[],[PpcKF (_,_,_,_,ppc),RuleKF (_,r),req],_) = *) + StdinSML 1 1 ~1 ~1 + (RuleFK (Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))")); +"--- s3 ---"; +StdinSML 1 1 ~2 ~2 (RuleFK (Add_Given "solveFor x")); +"--- s4 ---"; +StdinSML 1 1 ~3 ~3 (RuleFK (Add_Given "errorBound (eps = 0)")); +"--- s5 ---"; +StdinSML 1 1 ~4 ~4 (RuleFK (Add_Find "solutions L")); +"--- s6 ---"; +StdinSML 1 1 ~5 ~5 (RuleFK (Specify_Domain "Test.thy")); +"--- s7 ---"; +StdinSML 1 1 ~6 ~6 (RuleFK +(Specify_Problem ["sqroot-test","univariate","equation","test"])); +"--- s8 ---"; +StdinSML 1 1 ~7 ~7 (RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))); +"--- s9 ---"; +StdinSML 1 1 ~8 ~8 (RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))); +"--- 1 ---"; +StdinSML 1 1 ~9 ~9 (RuleFK (Rewrite ("square_equation_left",""))); +"--- 2 ---"; +StdinSML 1 1 ~10 ~10 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 3 ---"; +StdinSML 1 1 ~11 ~11 (RuleFK (Rewrite_Set "rearrange_assoc")); +"--- 4 ---"; +StdinSML 1 1 ~12 ~12 (RuleFK (Rewrite_Set "isolate_root")); +"--- 5 ---"; +StdinSML 1 1 ~13 ~13 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 6 ---"; +StdinSML 1 1 ~14 ~14 (RuleFK +(Rewrite ("square_equation_left",""))); +"--- 7 ---"; +StdinSML 1 1 ~15 ~15 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 8<> ---"; +StdinSML 1 1 ~16 ~16 (RuleFK (Rewrite_Set "rearrange_assoc")); +"--- 9<> ---"; +StdinSML 1 1 ~17 ~17 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 10<> ---"; +StdinSML 1 1 ~18 ~18 (RuleFK (Rewrite_Set "norm_equation")); +"--- 11<> ---"; +StdinSML 1 1 ~19 ~19 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 12<> ---"; +StdinSML 1 1 ~20 ~20 (RuleFK +(Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"))); +"--- 13<> ---"; +StdinSML 1 1 ~21 ~21 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 14<> ---"; +val (begin,uI,pI,acI,cI,dats,eend) = +StdinSML 1 1 ~22 ~22 (RuleFK +(Check_Postcond ["sqroot-test","univariate","equation","test"])); + + +(* +"=====================";======================= + use"test-FE-KE.sml"; + *) + + + + +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +" _________________ stdin: root_equ: 1.norm_equation ________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +set_dstate 1 test_hide 0 2; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- s2 ---"; +StdinSML 1 1 ~1 ~1 (Command Accept); +(*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*) +"--- s3 ---"; +StdinSML 1 1 ~2 ~2 (Command Accept); +(*RuleFK (Add_Given "solveFor x")*) +"--- s4 ---"; +StdinSML 1 1 ~3 ~3 (Command Accept); +(*RuleFK (Add_Given "errorBound (eps = #0)")*) +"--- s5 ---"; +StdinSML 1 1 ~4 ~4 (Command Accept); +(*RuleFK (Add_Find "solutions L")*) +"--- s6 ---"; +StdinSML 1 1 ~5 ~5 (Command Accept); +(*RuleFK (Specify_Domain "Test.thy")*) +"--- s7 ---"; +StdinSML 1 1 ~6 ~6 (Command Accept); +(*RuleFK (Specify_Problem ["sqroot-test","univariate","equation","test"])*) +"--- s8 ---"; +StdinSML 1 1 ~7 ~7 (Command Accept); +(*RuleFK (Specify_Method ("Test.thy","sqrt-equ-test"))*) +"--- s9 ---"; +val (_,1,1,~8,[],[RuleKF (_,r),FormKF (_,_,_,_,f),req],_) = +StdinSML 1 1 ~8 ~8 (Command Accept); +(*RuleFK (Apply_Method ("Test.thy","sqrt-equ-test"))*) +"--- !!! x1 --- strange choice"; +StdinSML 1 1 ~9 2 (RuleFK (Rewrite_Set "norm_equation")); +"--- !!! x2 --- ME knows nxt_step"; +StdinSML 1 1 ~10 3 (RuleFK (Rewrite_Set "Test_simplify")); +"--- !!! x3 --- helpless !!!"; +StdinSML 1 1 ~11 4 (RuleFK (Rewrite_Set "rearrange_assoc")); +"--- !!! x4 ---"; +StdinSML 1 1 ~12 5 (RuleFK (Rewrite_Set "isolate_root")); +"--- !!! x5 --- back at original equation !!!"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),requ],_) = +StdinSML 1 1 ~13 5 (RuleFK (Rewrite_Set "Test_simplify")); +if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" +then () else raise error "new behaviour in 1.norm_equ"; + +(* +"=====================================";=====@@@@@s===== + use"test-FE-KE.sml"; + W.N.16.4.00 + *) + +" _________________ stdin: root_equ: spec_hide ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +" _________________ stdin: root_equ: spec_hide ________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +set_dstate 1 spec_hide 4 1; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); +writeln(term2str sc); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),Select _,req],_) = + +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- !!! x1 --- strange choice"; (*TODO 31.10.00: hier nochmals spec ?!?!?*) +StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "norm_equation")); +"--- !!! x2 --- ME knows nxt_step"; +StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify")); +"--- !!! x3 --- helpless !!!"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = +StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc")); +"--- !!! x4 ---"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = +StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root")); +"--- !!! x5 --- back at original equation !!!"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = + +StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify")); +if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" +then () else raise error "new behaviour in test-example"; + +"--- !!! x6 --- not applicable"; +val (_,_,_,_,_,[Error_ err,Select _,requ],_) = +StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite_Set "Test_simplify")); + +val (_,_,_,_,_,[RuleKF r,FormKF (_,_,_,_,f),requ],_) = +StdinSML 1 1 ~6 ~6 (Command YourTurn); + +StdinSML 1 1 ~7 ~7 (Command ActiveMinus); +StdinSML 1 1 ~7 ~7 (Command ActiveMinus); +StdinSML 1 1 ~7 ~7 (Command ActiveMinus); +StdinSML 1 1 ~7 ~7 (Command ActiveMinus);(*acti=0*) +StdinSML 1 1 ~7 ~7 (Command SpeedPlus);(*speed=2:PutRule,TskipS..PutRuleRes,Tt.*) +StdinSML 1 1 ~7 ~7 (Command Accept); +StdinSML 1 1 ~8 ~8 (Command Accept); +StdinSML 1 1 ~9 ~9 (Command Accept); +StdinSML 1 1 ~10 ~10 (Command Accept); +StdinSML 1 1 ~11 ~11 (Command Accept); +StdinSML 1 1 ~12 ~12 (Command Accept); +StdinSML 1 1 ~13 ~13 (Command Accept); +StdinSML 1 1 ~14 ~14 (Command Accept); + +(*17.9.02: nach Umbau KB wird Equ immer gr"osser ?!----- +StdinSML 1 1 ~15 ~15 (Command Accept); +StdinSML 1 1 ~16 ~16 (Command Accept); +StdinSML 1 1 ~17 ~17 (Command Accept); +StdinSML 1 1 ~18 ~18 (Command Accept); +val (_,1,1,_,_,[FormKF (~20,_,0,_,f),req],_) = +StdinSML 1 1 ~19 ~19 (Command Accept); +if f="[x = 4]" then () else raise error "new behaviour in test-example"; + +val (_,1,1,~20,[],[Request "start another example",End_Proof],_) = +StdinSML 1 1 ~20 ~20 (Command Accept); +--------------------------------------------------------------------*) + +(* +"=====================================";=====@@@@@===== + use"test-FE-KE.sml"; + *) + + +" ------------- test-FE-KE.sml: test100 ------------- "; +" ------------- test-FE-KE.sml: test100 ------------- "; +" ------------- test-FE-KE.sml: test100 ------------- "; +" ------------- test-FE-KE.sml: test100 ------------- "; +" ------------- test-FE-KE.sml: test100 ------------- "; +" ------------- test-FE-KE.sml: test100 ------------- "; +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["realTestGiven (0+0)*(1*(1*a))", + "realTestFind a"]; +val (dI',pI',mI') = + ("Script.thy",["Script.thy","pbl-testterm"], + ("Script.thy","met-testterm")); +"--- s1 ---"; +(* +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +*** Type unification failed: Clash of types "Descript.una" and "RealDef.real". +*) +"--- s2 ---"; +(*too many problems with setup of this example*) + + +" _________________ stdin: root_equ: Auto ________________ "; +" _________________ stdin: root_equ: Auto ________________ "; +" _________________ stdin: root_equ: Auto ________________ "; +" _________________ stdin: root_equ: Auto ________________ "; +" _________________ stdin: root_equ: Auto ________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +set_dstate 1 spec_hide 4 1; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),Select _,req],_) = +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); + +val (_,1,1,~1,[], + [RuleKF _,_,_,_,_,_,_,_,_,_,_,_,_,_,_,req,End_Proof],_) = +StdinSML 1 1 ~1 ~1 (Command Auto); + + + +"######################### test-FE_KE.sml complete #####################"; diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/calculate.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/calculate.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,455 @@ +(* use"tests/calculate.sml"; + use"calculate.sml"; + *) +(*contents +" ================= calculate.sml: calculate_ ======================== "; +" ================= calculate.sml: aus script ======================== "; +" ================= calculate.sml: from test-root-equ.sml ================== "; +" ================= calculate.sml: 2.8.02 check test-root-equ ======== "; +" ================= calculate.sml:10.8.02 2002:///->/ ======== "; +" ================= calculate.sml: calculate_ 2002 =================== "; +" ================= eval_binop Float =================== "; +*) + +(* [("Var",("Tools.Var",fn)),("Length",("Tools.Length",fn)), + ("Nth",("Tools.Nth",fn)), + ("power_",("Atools.pow",fn)),("plus",("op +",fn)),("times",("op *",fn)), + ("is_const",("Atools.is'_const",fn)), + ("le",("op <",fn)),("leq",("op <=",fn)), + ("ident",("Atools.ident",fn))] *) + +" ================= calculate.sml: calculate_ ======================== "; +" ================= calculate.sml: calculate_ ======================== "; +" ================= calculate.sml: calculate_ ======================== "; + + +val thy = Test.thy; +val t = (term_of o the o (parse thy)) "1+2"; +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; + +val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2"; +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +Sign.string_of_term (sign_of thy) t; +(*val it = "(#3 * #4 // #3) ^^^ #2" : string*) +val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t; +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +Sign.string_of_term (sign_of thy) t; +(*val it = "(#12 // #3) ^^^ #2" : string*) +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t; +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +Sign.string_of_term (sign_of thy) t; +(*it = "#4 ^^^ #2" : string*) +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +Sign.string_of_term (sign_of thy) t; +(*val it = "#16" : string*) +if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" +else (); + +" ================= calculate.sml: aus script ======================== "; +" ================= calculate.sml: aus script ======================== "; +" ================= calculate.sml: aus script ======================== "; + +store_pbt + (prep_pbt Test.thy + (["test"], + [], + e_rls, None, [])); +store_pbt + (prep_pbt Test.thy + (["calculate","test"], + [("#Given" ,["realTestGiven t_"]), + ("#Find" ,["realTestFind s_"]) + ], + e_rls, None, [("Test.thy","test_calculate")])); + +methods:= overwritel (!methods, +[ + prep_met + (("Test.thy","test_calculate"):metID, + [("#Given" ,["realTestGiven t_"]), + ("#Find" ,["realTestFind s_"]) + ], + {rew_ord'="sqrt_right",rls'=tval_rls,srls=e_rls,prls=e_rls, + calc=[("plus" ,("op +" ,eval_binop "#add_")), + ("times" ,("op *" ,eval_binop "#mult_")), + ("divide_" ,("HOL.divide" ,eval_cancel "#divide_")), + ("power_" ,("Atools.pow" ,eval_binop "#power_"))], + asm_rls=[],asm_thm=[]}, + "Script STest_simplify (t_::real) = \ + \(Repeat \ + \ ((Try (Repeat (Calculate plus))) @@ \ + \ (Try (Repeat (Calculate times))) @@ \ + \ (Try (Repeat (Calculate divide_))) @@ \ + \ (Try (Repeat (Calculate power_))))) t_" + ) +]); + +val fmz = ["realTestGiven (((1+2)*4/3)^^^2)","realTestFind s"]; +val (dI',pI',mI') = + ("Test.thy",["calculate","test"],("Test.thy","test_calculate")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +(*nxt =("Add_Given",Add_Given "realTestGiven (((#1 + #2) * #4 // #3) ^^^#2)")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Add_Find",Add_Find "realTestFind s") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Specify_Problem",Specify_Problem ["calculate","test"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Specify_Method",Specify_Method ("Test.thy","test_calculate"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_calculate"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Calculate",Calculate "plus")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Calculate",Calculate "times")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Calculate",Calculate "divide_")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Calculate",Calculate "power_")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("Check_Postcond",Check_Postcond ["calculate","test"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*nxt = ("End_Proof'",End_Proof')*) +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"16")) then () +else raise error "calculate.sml: script test_calculate changed behaviour"; + + + + +" ================= calculate.sml: from test-root-equ.sml ================== "; +" ================= calculate.sml: from test-root-equ.sml ================== "; +" ================= calculate.sml: from test-root-equ.sml ================== "; +val thy' = "Test.thy"; +val ct = "1 + 2"; +val (ct,thm') = the (calculate thy' (the(assoc(calclist,"plus"))) ct); +(*val ct = "#3" : string +val thm' = ("#add_#1_#2","\"#1 + #2 = #3\"") : thm'*) + +"----- me -----"; +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val (pt,_) = cappend_atomic pt [1] e_istate "1 + 2" + (Calculate "test") ct Complete; +val p = ([1],Frm):pos'; +val nxt = ("Calculate",Calculate "plus"); +val (p,_,f,nxt,_,pt)=me nxt p c pt; +Compiler.Control.Print.printDepth:=9; (*4 default*) +(* Nd (PblObj... + [Nd (PrfObj + {branch=NoBranch,cell=[],form="#1 + #2",loc=(([],None),([],None)), + mstep=Calculate "plus",ostate=Complete,result="#3"},[])]) : squ*) +Compiler.Control.Print.printDepth:=4; (*4 default*) + +val (pt,_) = cappend_atomic pt [1] e_istate "6/4" + (Calculate "test") ct Complete; +val p = ([1],Frm):pos'; +val nxt = ("Calculate",Calculate "divide_"); +val (p,_,f,nxt,_,pt)=me nxt p c pt; +(*{branch=NoBranch,cell=[],form="#6 // #4",loc=(([],None),([],None)), + mstep=Calculate "divide_",ostate=Complete,result="#3 // #2"},[])]) *) + +(*5.7.00: interne ops in calclist*) + + +" ================= calculate.sml: 2.8.02 check test-root-equ ======== "; +" ================= calculate.sml: 2.8.02 check test-root-equ ======== "; +" ================= calculate.sml: 2.8.02 check test-root-equ ======== "; +(*(1): 2nd Test_simplify didn't work: +val ct = + "sqrt (x ^^^ 2 + -3 * x) = (-3 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)" +> val rls = ("Test_simplify"); +> val (ct,_) = the (rewrite_set thy' ("tval_rls") false rls ct); +val ct = "sqrt (x ^^^ 2 + -3 * x) = +(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"; +ie. cancel does not work properly +*) + val thy = "Test.thy"; + val op_ = "divide_"; + val ct = "sqrt (x ^^^ 2 + -3 * x) =\ + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2))))"; + val Some (ct,_) = calculate thy (the(assoc(calclist,op_))) ct; + writeln ct; +(* + sqrt (x ^^^ 2 + -3 * x) =\ + \(-9) / (-2) + (-3 / (-2) + (x * ((-4) / (-2)) + x * (2 / (-2)))) +............... does not work *) + +(*--------------(2): does divide work in Test_simplify ?: ------*) + val thy = Test.thy; + val t = (term_of o the o (parse thy)) "6 / 2"; + val rls = Test_simplify; + val (t,_) = the (rewrite_set_ thy false rls t); +(*val t = Free ("3","RealDef.real") : term*) + + val thy = "Test.thy"; + val t = "6 / 2"; + val rls = "Test_simplify"; + val (t,_) = the (rewrite_set thy false rls t); +(*val t = "3" : string + ....... works, thus: which rule in SqRoot_simplify works differently ?*) + + +(*--------------(3): is_const works ?: -------------------------------------*) + val t = (term_of o the o (parse Test.thy)) "2 is_const"; + atomty Test.thy t; + rewrite_set_ Test.thy false tval_rls t; +(*val it = Some (Const ("True","bool"),[]) ... works*) + + +(*--------------(4): check bottom up: ---------------------------*) +(*-------------- eval_cancel works: *) + trace_rewrite:=true; + val thy = Test.thy; + val t = (term_of o the o (parse thy)) "(-4) / 2"; + val Some (_,t) = eval_cancel "xxx" 111 t thy; + term2str t; +"-4 / 2 = (-2)"; +(*-------------- but ... *) + val ct = "x + (-4) / 2"; + val (ct,_) = the (rewrite_set thy' false rls ct); +"(-2) + x"; +(*-------------- while ... *) + val ct = "(-4) / 2"; + val (ct,_) = the (rewrite_set thy' false rls ct); +"(-2)"; + +(*--------------(5): reproduce (1) with simpler term: ------------*) + val thy = "Test.thy"; + val t = "(3+5)/2"; + val (t,_) = the (rewrite_set thy false rls t); +(*val t = "4" ... works*) + + val t = "(3+1+2*x)/2"; + val (t,_) = the (rewrite_set thy false rls t); +(*val t = "2 + x" ... works*) + + val t = "(3+(1+2*x))/2"; + val (t,_) = the (rewrite_set thy false rls t); +(*val t = "2 + x" ... works: give up----------------------------------------*) + + + +(*--- trace_rewrite before correction of ... -------------------- + val ct = "(-3 + 2 * x + -1) / 2"; + val (ct,_) = the (rewrite_set thy' false rls ct); +: +### trying thm 'root_ge0_2' +### rewrite_set_: x + (-1 + -3) / 2 +### trying thm 'radd_real_const_eq' +### trying thm 'radd_real_const' +### rewrite_set_: x + (-4) / 2 +### trying thm 'rcollect_right' +: +"x + (-4) / 2" +-------------------------------------while before Isabelle20002: + val ct = "(#-3 + #2 * x + #-1) // #2"; + val (ct,_) = the (rewrite_set thy' false rls ct); +: +### trying thm 'root_ge0_2' +### rewrite_set_: x + (#-1 + #-3) // #2 +### trying thm 'radd_real_const_eq' +### trying thm 'radd_real_const' +### rewrite_set_: x + #-4 // #2 +### rewrite_set_: x + #-2 +### trying thm 'rcollect_right' +: +"#-2 + x" +-----------------------------------------------------------------*) + + + toggle trace_rewrite; +(*===================*) + trace_rewrite:=true; + val thy' = "Test.thy"; + val rls = "Test_simplify"; + val ct = "x + (-1 + -3) / 2"; + val (ct,_) = the (rewrite_set thy' false rls ct); +"x + (-4) / 2"; +(* +### trying calc. 'cancel' +@@@ get_pair: binop, t = x + (-4) / 2 +@@@ get_pair: t else +@@@ get_pair: t else -> None +@@@ get_pair: binop, t = (-4) / 2 +@@@ get_pair: then 1 +@@@ get_pair: t -> None +@@@ get_pair: t1 -> None +@@@ get_calculation: None +### trying calc. 'pow' +*) + + trace_rewrite:=true; + val thy' = "Test.thy"; + val rls = "Test_simplify"; + val ct = "x + (-4) / 2"; + val (ct,_) = the (rewrite_set thy' false rls ct); +"(-2) + x"; +(* +### trying calc. 'cancel' +@@@ get_pair: binop, t = x + -4 / 2 +@@@ get_pair: t else +@@@ get_pair: t else -> None +@@@ get_pair: binop, t = -4 / 2 +@@@ get_pair: then 1 +@@@ get_calculation: Some #cancel_-4_2 +### calc. to: x + (-2) +### trying calc. 'cancel' +*) + trace_rewrite:=false; + +" ================= calculate.sml:10.8.02 2002:///->/ ======== "; +" ================= calculate.sml:10.8.02 2002:///->/ ======== "; +" ================= calculate.sml:10.8.02 2002:///->/ ======== "; +" ----------------- rewriting works ? -----------------------"; + val thy = Isac.thy; + val prop = (#prop o rep_thm) real_divide_1; + atomty thy prop; +(*** ------------- +*** Const ( Trueprop, bool => prop) +*** . Const ( op =, [real, real] => bool) +*** . . Const ( HOL.divide, [real, real] => real) +*** . . . Var ((x, 0), real) +*** . . . Const ( 1, real) +*** . . Var ((x, 0), real) *) + val prop' = (#prop o rep_thm o num_str) real_divide_1; + atomty thy prop'; +(*** ------------- +*** Const ( Trueprop, bool => prop) +*** . Const ( op =, [real, real] => bool) +*** . . Const ( HOL.divide, [real, real] => real) +*** . . . Var ((x, 0), real) +*** . . . Free ( 1, real) (*app_num_tr'*) +*** . . Var ((x, 0), real)*) + val t = (term_of o the o (parseold thy)) "aaa/1"; + atomty thy t; +(*** ------------- +*** Const ( HOL.divide, ['a, 'a] => 'a) +*** . Free ( aaa, 'a) +*** . Free ( 1, 'a) *) + val t = (term_of o the o (parse thy)) "aaa/1"; + atomty thy t; +(*** ------------- +*** Const ( HOL.divide, [real, real] => real) +*** . Free ( aaa, real) +*** . Free ( 1, real) *) + val thm = num_str real_divide_1; + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +(*val t = Free ("aaa","RealDef.real") : term*) + + + val prop = (#prop o rep_thm) realpow_eq_one; + atomty thy prop; +(*** ------------- +*** Const ( Trueprop, bool => prop) +*** . Const ( op =, [real, real] => bool) +*** . . Const ( Nat.power, [real, nat] => real) +*** . . . Const ( 1, real) +*** . . . Var ((n, 0), nat) +*** . . Const ( 1, real) *) + val prop' = (#prop o rep_thm o num_str) realpow_eq_one; + atomty thy prop'; +(*** ------------- +*** Const ( Trueprop, bool => prop) +*** . Const ( op =, [real, real] => bool) +*** . . Const ( Nat.power, [real, nat] => real) +*** . . . Free ( 1, real) +*** . . . Var ((n, 0), nat) +*** . . Free ( 1, real)*) + val t = (term_of o the o (parseold thy)) "1 ^ aaa"; + atomty thy t; +(*** ------------- +*** Const ( Nat.power, ['a, nat] => 'a) +*** . Free ( 1, 'a) +*** . Free ( aaa, nat) *) + val t = (term_of o the o (parse thy)) "1 ^ aaa"; + atomty thy t; +(*** ------------- +*** Const ( Nat.power, [real, nat] => real) +*** . Free ( 1, real) +*** . Free ( aaa, nat) .......................... nat !!! *) + val thm = num_str realpow_eq_one; + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +(*val t = Free ("1","RealDef.real") : term*) + +" ================= calculate.sml: calculate_ 2002 =================== "; +" ================= calculate.sml: calculate_ 2002 =================== "; +" ================= calculate.sml: calculate_ 2002 =================== "; + +val thy = Test.thy; +val t = (term_of o the o (parse thy)) "12 / 3"; +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t; +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +"12 / 3 = 4"; +val thy = Test.thy; +val t = (term_of o the o (parse thy)) "4 ^^^ 2"; +val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_"))) t; +val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; +"4 ^ 2 = 16"; + + val t = (term_of o the o (parse thy)) "((1 + 2) * 4 / 3) ^^^ 2"; + val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t; +"1 + 2 = 3"; + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; + Sign.string_of_term (sign_of thy) t; +"(3 * 4 / 3) ^^^ 2"; + val Some (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t; +"3 * 4 = 12"; + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; + Sign.string_of_term (sign_of thy) t; +"(12 / 3) ^^^ 2"; + val Some (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t; +"12 / 3 = 4"; + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; + Sign.string_of_term (sign_of thy) t; +"4 ^^^ 2"; + val Some (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t; +"4 ^^^ 2 = 16"; + val Some (t,_) = rewrite_ thy tless_true tval_rls true thm t; + Sign.string_of_term (sign_of thy) t; +"16"; + if it <> "16" then raise error "calculate.sml: new behaviour in calculate_" + else (); + +(*13.9.02 *** calc: operator = pow not defined*) + val t = (term_of o the o (parse thy)) "3^^^2"; + val Some (thmID,thm) = + get_calculation_ thy (the(assoc(calclist,"power_"))) t; +(*** calc: operator = pow not defined*) + + val (op_, eval_fn) = the (assoc(calclist,"power_")); + (* +val op_ = "Atools.pow" : string +val eval_fn = fn : string -> term -> theory -> (string * term) option*) + + val Some (thmid,t') = get_pair thy op_ eval_fn t; +(*** calc: operator = pow not defined*) + + val Some (id,t') = eval_fn op_ t thy; +(*** calc: operator = pow not defined*) + + val (thmid, (Const (op0,t0) $ Free (n1,t1) $ Free(n2,t2))) = (op_, t); + val Some (id,t') = eval_binop thmid op_ t thy; +(*** calc: operator = pow not defined*) + + + +" ================= eval_binop Float =================== "; +val t = str2term "Float ((1,2),(0,0))"; +atomty thy t; +val Const ("Float.Float",_) $ + (Const ("Pair",_) $ + (Const ("Pair",_) $ Free (i1,_) $ Free (i2,_)) $ _) = t; + +val t = str2term "Float ((1,2),(0,0)) * Float ((3,4),(0,0))"; +atomty thy t; +(*GOON.10.4.03*) \ No newline at end of file diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/details.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/details.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,280 @@ +(* use"../systest/details.sml"; + use"systest/details.sml"; + use"details.sml"; + +######################################################## +is NOT dependent on Test, but on other thys: +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +uses from Rational.ML: Rrls cancel_p, Rrls cancel +which in turn +uses from Poly.ML: Rls make_polynomial, Rls expand_binom +######################################################## +*) +"-------- cancel, without detail ------------------------------"; +"-------- cancel, detail rev-rew (cancel) afterwards ----------"; +"-------------- cancel_p, without detail ------------------------------"; +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; + +store_pbt + (prep_pbt Test.thy + (["test"], + [], + e_rls, None, [])); +store_pbt + (prep_pbt Test.thy + (["detail","test"], + [("#Given" ,["realTestGiven t_"]), + ("#Find" ,["realTestFind s_"]) + ], + e_rls, None, [("Test.thy","test_detail")])); + +methods:= overwritel (!methods, +[ + prep_met + (("Test.thy","test_detail_binom"):metID, + [("#Given" ,["realTestGiven t_"]), + ("#Find" ,["realTestFind s_"]) + ], + {rew_ord'="sqrt_right",rls'=tval_rls,calc = [],srls=e_rls,prls=e_rls, + asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]}, + "Script Testterm (g_::real) = \ + \(((Rewrite_Set expand_binoms False) @@\ + \ (Rewrite_Set cancel False)) g_)" + ), + prep_met + (("Test.thy","test_detail_poly"):metID, + [("#Given" ,["realTestGiven t_"]), + ("#Find" ,["realTestFind s_"]) + ], + {rew_ord'="sqrt_right",rls'=tval_rls,calc=[],srls=e_rls,prls=e_rls, + asm_rls=[],asm_thm=[("real_mult_div_cancel2","")]}, + "Script Testterm (g_::real) = \ + \(((Rewrite_Set make_polynomial False) @@\ + \ (Rewrite_Set cancel_p False)) g_)" + )]); + +(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) + +"-------- cancel, without detail ------------------------------"; +"-------- cancel, without detail ------------------------------"; +"-------- cancel, without detail ------------------------------"; +val fmz = ["realTestGiven (((3 + x) * (3 - x)) / ((3 + x) * (3 + x)))", + "realTestFind s"]; +val (dI',pI',mI') = + ("Test.thy",["detail","test"],("Test.thy","test_detail_binom")); + +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"(3 + -1 * x) / (3 + x)"*) +if nxt = ("End_Proof'",End_Proof') then () +else raise error "details.sml, changed behaviour in: without detail"; + + +"-------- cancel, detail rev-rew (cancel) afterwards ----------"; +"-------- cancel, detail rev-rew (cancel) afterwards ----------"; +"-------- cancel, detail rev-rew (cancel) afterwards ----------"; + val p = e_pos'; val c = []; + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*val nxt = ("Rewrite_Set",Rewrite_Set "expand_binoms")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) + val nxt = ("Detail",Detail);"----------------------"; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*val nxt = ("End_Detail",End_Detail)*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) + val nxt = ("Detail",Detail);"----------------------"; + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*15.10.02*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(* +rewrite "Rationals.thy" "tless_true""e_rls"true("sym_real_plus_minus_binom","") + "3 ^^^ 2 - x ^^^ 2"; +*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 - x) / (3 + x)")) + andalso nxt = ("End_Proof'",End_Proof') then () +else raise error "new behaviour in details.sml, \ + \cancel, rev-rew (cancel) afterwards"; + +(*---- funktionieren mit Rationals.ML: dummy-Funktionen(1)--------*) + +"-------------- cancel_p, without detail ------------------------------"; +"-------------- cancel_p, without detail ------------------------------"; +"-------------- cancel_p, without detail ------------------------------"; +val fmz = ["realTestGiven (((3 + x)*(3+(-1)*x)) / ((3+x) * (3+x)))", + "realTestFind s"]; +val (dI',pI',mI') = + ("Test.thy",["detail","test"],("Test.thy","test_detail_poly")); + +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail"))*) +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +"(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))"; + + (*14.3.03*) + val t = str2term "(3 + x) * (3 + -1 * x) / ((3 + x) * (3 + x))"; + val Some (t,_) = rewrite_set_ thy false make_polynomial t; term2str t; + "(9 + - (x ^^^ 2)) / (9 + 6 * x + x ^^^ 2)"; + val Some (t,_) = rewrite_set_ thy false cancel_p t; term2str t; + cancel_p_ thy t; + + val t = str2term "(3 + x) * (3 + -1 * x)"; + val Some (t,_) = rewrite_set_ thy false expand_poly t; term2str t; + "3 * 3 + 3 * (-1 * x) + (x * 3 + x * (-1 * x))"; + val Some (t,_) = rewrite_set_ thy false order_add_mult t; term2str t; + "3 * 3 + (3 * x + (-1 * (3 * x) + -1 * (x * x)))"; + val Some (t,_) = rewrite_set_ thy false simplify_power t; term2str t; + "3 ^^^ 2 + (3 * x + (-1 * (3 * x) + -1 * x ^^^ 2))"; + val Some (t,_) = rewrite_set_ thy false collect_numerals t; term2str t; + "9 + (0 * x + -1 * x ^^^ 2)"; + val Some (t,_) = rewrite_set_ thy false reduce_012 t; term2str t; + "9 + - (x ^^^ 2)"; + (*14.3.03*) + +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*"(3 + -1 * x) / (3 + x)"*) +if nxt = ("End_Proof'",End_Proof') then () +else raise error "details.sml, changed behaviour in: cancel_p, without detail"; + +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; +"-------------- cancel_p, detail rev-rew (cancel) afterwards ----------"; + val p = e_pos'; val c = []; + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) + +(*14.3.03.FIXXXXXME since Isa02/reverse-rew.sml: + fun make_deriv ... Rls_ not yet impl. (| Thm | Calc) + Rls_ needed for make_polynomial ---------------------- + val nxt = ("Detail",Detail);"----------------------"; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + if nxt = ("End_Detail",End_Detail) then () + else raise error "details.sml: new behav. in Detail make_polynomial"; +----------------------------------------------------------------------*) + +(*--------------- + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*val nxt = ("Rewrite_Set",Rewrite_Set "cancel_p")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) + val nxt = ("Detail",Detail);"----------------------"; + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = (me nxt p [] pt) handle e => print_exn e; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"(3 + x) / (3 - x)")) + andalso nxt = ("End_Proof'",End_Proof') then () +else raise error "new behaviour in details.sml, cancel_p afterwards"; + +----------------*) + + + + + +val fmz = ["realTestGiven ((x+3)+(-1)*(2+6*x))", + "realTestFind s"]; +val (dI',pI',mI') = + ("Test.thy",["detail","test"],("Test.thy","test_detail_poly")); + + val p = e_pos'; val c = []; + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + (*nxt = ("Apply_Method",Apply_Method ("Test.thy","test_detail_poly"))*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*16.10.02 --- kommt auf POLY_EXCEPTION ?!??? ---------------------------- + (*val nxt = ("Rewrite_Set",Rewrite_Set "make_polynomial")*) + val (p,_,f,nxt,_,pt) = me nxt p [] pt; (* rewrite must exist for Detail*) + val nxt = ("Detail",Detail);"----------------------"; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; + val (p,_,f,nxt,_,pt) = me nxt p [] pt; +-------------------------------------------------------------------------*) + + + diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/list_rls.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/list_rls.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,32 @@ +(* use"tests/list_rls.sml"; + W.N. 8.01 + only one item per file for test-impl. +*) + + +val thy' = "ListG.thy"; +val ct = "length_ [1,1,1]"; +val thm = ("length_Cons_",""); +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); +val thm = ("length_Nil_",""); +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") false thm ct); +if ct="1 + (1 + (1 + 0))"then() +else raise error ("list_rls.sml 1: behaviour of test-expl changed: "^ct); + + +val ct = "length_ [1,1,1]"; +val rls = "list_rls"; +val (ct,asm) = the (rewrite_set thy' false rls ct); +if ct="3"then() +else raise error ("list_rls.sml 2: behaviour of test-expl changed: "^ct); + + +val ct = "length_ [1,1,1]"; +val t = (term_of o the o (parse ListG.thy)) ct; +val t = eval_listexpr_ ListG.thy list_rls t; +case t of Free ("3",_) => () +| _ => raise error ("list-rls.sml 3: behaviour of test-expl changed: "^ct); + + diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/refine.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/refine.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,396 @@ +(* intermediately stores !ptyps + WN.16.9.01 + use"tests/refine.sml"; + *) + + +"----------------------- store test-pbtyps ----------------------------"; +"----------------------- refin test-pbtyps ----------------------------"; +"----------------------- refine_ori test-pbtyps ----------------------------"; +"----------------------- refine test-pbtyps ----------------------------"; +"----------------------- Refine_Problem (aus subp-rooteq.sml) ---------"; + + + + +"----------------------- store test-pbtyps ----------------------------"; +val intermediate_ptyps = !ptyps; +ptyps:= ([]:ptyps); + +store_pbt + (prep_pbt DiffApp.thy + (["pbla"], + [("#Given", ["fixedValues a_"])], e_rls, None, [])); +store_pbt + (prep_pbt DiffApp.thy + (["pbla1","pbla"], + [("#Given", ["fixedValues a_","maximum a1_"])], e_rls, None, [])); +store_pbt + (prep_pbt DiffApp.thy + (["pbla2","pbla"], + [("#Given", ["fixedValues a_","valuesFor a2_"])], e_rls, None, [])); +store_pbt + (prep_pbt DiffApp.thy + (["pbla2x","pbla2","pbla"], + [("#Given", ["fixedValues a_","valuesFor a2_","functionOf a2x_"])], + e_rls, None, [])); +store_pbt + (prep_pbt DiffApp.thy + (["pbla2y","pbla2","pbla"], + [("#Given" ,["fixedValues a_","valuesFor a2_","boundVariable a2y_"])], + e_rls, None, [])); +store_pbt + (prep_pbt DiffApp.thy + (["pbla2z","pbla2","pbla"], + [("#Given" ,["fixedValues a_","valuesFor a2_","interval a2z_"])], + e_rls, None, [])); +store_pbt + (prep_pbt DiffApp.thy + (["pbla3","pbla"], + [("#Given" ,["fixedValues a_","relations a3_"])], + e_rls, None, [])); + +show_ptyps(); + +(*case 1: no refinement *) +val thy = Isac.thy; +val (d1,ts1,vs1) = split_dts thy ((term_of o the o (parse thy)) + "fixedValues [aaa=0]"); +val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) + "errorBound (ddd=0)"); +val ori1 = [(1,[1],"#Given",d1,ts1), + (2,[1],"#Given",d2,ts2)]:ori list; + + +(*case 2: refined to pbt without children *) +val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) + "relations aaa333"); +val ori2 = [(1,[1],"#Given",d1,ts1), + (2,[1],"#Given",d2,ts2)]:ori list; + + +(*case 3: refined to pbt with children *) +val (d2,ts2,vs2) = split_dts thy ((term_of o the o (parse thy)) + "valuesFor aaa222"); +val ori3 = [(1,[1],"#Given",d1,ts1), + (2,[1],"#Given",d2,ts2)]:ori list; + + +(*case 4: refined to children (without child)*) +val (d3,ts3,vs3) = split_dts thy ((term_of o the o (parse thy)) + "boundVariable aaa222yyy"); +val ori4 = [(1,[1],"#Given",d1,ts1), + (2,[1],"#Given",d2,ts2), + (3,[1],"#Given",d3,ts3)]:ori list; + +"----------------------- refin test-pbtyps ----------------------------"; + +(*case 1: no refinement *) +refin [] ori1 (hd (!ptyps)); +(*val it = Some ["pbla"] : pblID option*) + +(*case 2: refined to pbt without children *) +refin [] ori2 (hd (!ptyps)); +(*val it = Some ["pbla","pbla3"] : pblID option*) + +(*case 3: refined to pbt with children *) +refin [] ori3 (hd (!ptyps)); +(*val it = Some ["pbla","pbla2"] : pblID option*) + +(*case 4: refined to children (without child)*) +refin [] ori4 (hd (!ptyps)); +(*val it = Some ["pbla","pbla2","pbla2y"] : pblID option*) + +(*case 5: start refinement somewhere in ptyps*) +val [Ptyp ("pbla",_,[_, ppp as Ptyp ("pbla2",_,_), _])] = !ptyps; +refin ["pbla"] ori4 ppp; +(*val it = Some ["pbla2","pbla2y"] : pblRD option*) + + +"----------------------- refine_ori test-pbtyps ----------------------------"; + +(*case 1: no refinement *) +refine_ori ori1 ["pbla"]; +(*val it = None : pblID option !!!!*) + +(*case 2: refined to pbt without children *) +refine_ori ori2 ["pbla"]; +(*val it = Some ["pbla3","pbla"] : pblID option*) + +(*case 3: refined to pbt with children *) +refine_ori ori3 ["pbla"]; +(*val it = Some ["pbla2","pbla"] : pblID option*) + +(*case 4: refined to children (without child)*) +val opt = refine_ori ori4 ["pbla"]; +if opt = Some ["pbla2y","pbla2","pbla"] then () +else raise error "new behaviour in refine.sml case 4"; + +(*case 5: start refinement somewhere in ptyps*) +refine_ori ori4 ["pbla2","pbla"]; +(*val it = Some ["pbla2y","pbla2","pbla"] : pblID option*) + + +"----------------------- refine test-pbtyps ----------------------------"; + +val fmz1 = ["fixedValues [aaa=0]","errorBound (ddd=0)"]; +val fmz2 = ["fixedValues [aaa=0]","relations aaa333"]; +val fmz3 = ["fixedValues [aaa=0]","valuesFor aaa222"]; +val fmz4 = ["fixedValues [aaa=0]","valuesFor aaa222", + "boundVariable aaa222yyy"]; + +(*case 1: no refinement *) +refine fmz1 ["pbla"]; +(* +*** pass ["pbla"] +*** pass ["pbla","pbla1"] +*** pass ["pbla","pbla2"] +*** pass ["pbla","pbla3"] +val it = + [Matches + (["pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]", + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla1","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_", + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla3","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_", + Superfl "errorBound (ddd = #0)"],Relate=[],Where=[],With=[]})] + : match list*) + +(*case 2: refined to pbt without children *) +refine fmz2 ["pbla"]; +(* +*** pass ["pbla"] +*** pass ["pbla","pbla1"] +*** pass ["pbla","pbla2"] +*** pass ["pbla","pbla3"] +val it = + [Matches + (["pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Superfl "relations aaa333"], + Relate=[],Where=[],With=[]}), + NoMatch + (["pbla1","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", + Superfl "relations aaa333"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "valuesFor a2_", + Superfl "relations aaa333"],Relate=[],Where=[],With=[]}), + Matches + (["pbla3","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "relations aaa333"], + Relate=[],Where=[],With=[]})] : match list*) + +(*case 3: refined to pbt with children *) +refine fmz3 ["pbla"]; +(* +*** pass ["pbla"] +*** pass ["pbla","pbla1"] +*** pass ["pbla","pbla2"] +*** pass ["pbla","pbla2","pbla2x"] +*** pass ["pbla","pbla2","pbla2y"] +*** pass ["pbla","pbla2","pbla2z"] +*** pass ["pbla","pbla3"] +val it = + [Matches + (["pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222"], + Relate=[],Where=[],With=[]}), + NoMatch + (["pbla1","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", + Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]}), + Matches + (["pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222"], + Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2x","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Missing "functionOf a2x_"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2y","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Missing "boundVariable a2y_"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2z","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Missing "interval a2z_"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla3","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "relations a3_", + Superfl "valuesFor aaa222"],Relate=[],Where=[],With=[]})] + : match list*) + +(*case 4: refined to children (without child)*) +refine fmz4 ["pbla"]; +(* +*** pass ["pbla"] +*** pass ["pbla","pbla1"] +*** pass ["pbla","pbla2"] +*** pass ["pbla","pbla2","pbla2x"] +*** pass ["pbla","pbla2","pbla2y"] +val it = + [Matches + (["pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Superfl "valuesFor aaa222", + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla1","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Missing "maximum a1_", + Superfl "valuesFor aaa222",Superfl "boundVariable aaa222yyy"], + Relate=[],Where=[],With=[]}), + Matches + (["pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2x","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"], + Relate=[],Where=[],With=[]}), + Matches + (["pbla2y","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})] + : match list*) + +(*case 5: start refinement somewhere in ptyps*) +refine fmz4 ["pbla2","pbla"]; +(* +*** pass ["pbla","pbla2"] +*** pass ["pbla","pbla2","pbla2x"] +*** pass ["pbla","pbla2","pbla2y"] +val it = + [Matches + (["pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Superfl "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]}), + NoMatch + (["pbla2x","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Missing "functionOf a2x_",Superfl "boundVariable aaa222yyy"], + Relate=[],Where=[],With=[]}), + Matches + (["pbla2y","pbla2","pbla"], + {Find=[], + Given=[Correct "fixedValues [aaa = #0]",Correct "valuesFor aaa222", + Correct "boundVariable aaa222yyy"],Relate=[],Where=[],With=[]})] + : match list*) + + +ptyps:= intermediate_ptyps; +show_ptyps(); + + + +"----------------------- Refine_Problem (aus subp-rooteq.sml) ---------"; +"----------------refine.sml: miniscript with mini-subpbl -------------"; +val fmz = ["equality ((x+1)*(x+2)=x^^^2+8)","solveFor x", + "errorBound (eps=0)","solutions L"]; +val (dI',pI',mI') = ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","squ-equ-test-subpbl1")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; + +val nxt = ("Specify_Problem", + Specify_Problem ["linear","univariate","equation","test"]); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*ML> f; +val it = Form' (PpcKF (0,EdUndef,0,Nundef, + (Problem ["linear","univariate","equation","test"], + {Find=[Incompl "solutions []"], + Given=[Incompl "errorBound", + Correct "equality ((x + #1) * (x + #2) = x ^^^ #2 + #8)", + Correct "solveFor x"],Relate=[], + Where=[False "matches (x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) + |\nmatches (?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) + |\nmatches (?a + x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8) + |\nmatches (?a + ?b * x = #0) ((x + #1) * (x + #2) = x ^^^ #2 + #8)"], + With=[]}))) : mout + +val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)")*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Refine_Problem",Refine_Problem ["linear","univariate","equation","test"] + kann nicht gut gehen --------- *) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Specify_Problem",Specify_Problem []) FIXXXME*) + +val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*("Specify_Problem",Specify_Problem ["normalize","univariate","equation","test"])*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep + in Script "uberdefiniert -^-*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation","test"]*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)") *) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*("Specify_Problem",Specify_Problem ["linear","univariate","equation","test"])*) + +val nxt = ("Refine_Problem",Refine_Problem ["univariate","equation","test"]); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Specify_Method",Specify_Method ("RatArith.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*("Check_Postcond",Check_Postcond ["normalize","univariate","equation","test"])*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = 2]" then () +else raise error "new behaviour in test:refine.sml: miniscript with mini-subpbl"; + + diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/root-equ.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/root-equ.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,620 @@ +(* use"../tests/test-root-equ.sml"; + use"tests/test-root-equ.sml"; + use"test-root-equ.sml"; + trace_rewrite:= true; + trace_rewrite:= false; + + method "sqrt-equ-test", _NOT_ "square-equation" +*) + + +" ================= equation with x =(-12)/5, but L ={} ======= "; +" _________________ rewrite _________________ "; + + +" ================= equation with result={4} ================== "; +" -------------- model, specify ------------ "; +" ________________ rewrite _________________"; +" _________________ rewrite_ x=4_________________ "; +" _________________ rewrite + cappend _________________ "; +" _________________ me Free_Solve _________________ "; +" _________________ me + msteps input _________________ "; +(*" _______________ me + nxt_step from script _________---> scriptnew.sml*) +(*" _________________ me + nxt_step from script (check_elementwise..)______ + ... L_a = Mstep subproblem_equation_dummy; ";*) +(*" _______________ me + root-equ: 1.norm_equation ___---> scriptnew.sml*) + +(* +> val t = (term_of o the o (parse thy)) "#2^^^#3"; +> val eval_fn = the (assoc (!eval_list, "pow")); +> val (Some (id,t')) = get_pair thy "pow" eval_fn t; +> Sign.string_of_term (sign_of thy) t'; +*) +(******************************************************************) +(* ------------------------------------- *) +" _________________ equation with x =(-12)/5, but L ={} ------- "; +(* ------------------------------------- *) +" _________________ rewrite _________________ "; +val thy' = "Test.thy"; +val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)"; +val thm = ("square_equation_left",""); +val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); +(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*) +val rls = ("Test_simplify"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*) +val rls = ("rearrange_assoc"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*) +val rls = ("isolate_root"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"sqrt (x ^^^ 2 + -3 * x) = +(-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*) +val rls = ("Test_simplify"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*) +val thm = ("square_equation_left",""); +val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct); +val asm = asm union asm'; +(*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*) +val rls = ("Test_simplify"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*) +val rls = ("norm_equation"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*) +val rls = ("Test_simplify"); +val (ct,_) = the (rewrite_set thy' false rls ct); +(*"-36 + -15 * x = 0"*) +val rls = ("isolate_bdv"); +val (ct,_) = the (rewrite_set_inst thy' false + [("bdv","x::real")] rls ct); +(*"x = (0 + -1 * -36) // -15"*) +val rls = ("Test_simplify"); +val (ct,_) = the (rewrite_set thy' false rls ct); +if ct<>"x = -12 / 5"then raise error "new behaviour in testexample"else (); + +(* +val ct = "x = (-12) / 5" : cterm' +> asm; +val it = + ["(+0) <= sqrt x + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x", + "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list +*) + + + + + +" ================== equation with result={4} ================== "; +" ================== equation with result={4} ================== "; +" ================== equation with result={4} ================== "; + +" -------------- model, specify ------------ "; +" -------------- model, specify ------------ "; +" -------------- model, specify ------------ "; +" --- subproblem 1: linear-equation --- "; +val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "bound_variable x","error_bound 0"(*, + "solutions L::real set" , + "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)]; +val thy = Isac.thy; +val formals = map (the o (parse thy)) origin; + +val given = ["equation (l=(r::real))", + "bound_variable bdv", (* TODO type *) + "error_bound eps"]; +val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.*) + "bdv is_var", + "eps is_const_expr"]; +val find = ["solutions (L::bool list)"]; +val with_ = [(* parseold ... + "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)]; +val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_); +val givens = map (the o (parse thy)) given; +parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}"; +(* 31.1.00 +val tag__forms = chktyps thy (formals, givens); +map ((atomty thy) o term_of) tag__forms; *) + +" --- subproblem 2: linear-equation --- "; +val origin = ["x + 4 = (0::real)","x::real"]; +val formals = map (the o (parse thy)) origin; + +val given = ["equation (l=(0::real))", + "bound_variable bdv"]; +val where_ = ["l is_linear_in bdv","bdv is_const"]; +val find = ["l::real"]; +val with_ = ["l = (%x. l) bdv"]; +val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_); +val givens = map (the o (parse thy)) given; + +val tag__forms = chktyps thy (formals, givens); +map ((atomty thy) o term_of) tag__forms; + + + +" _________________ rewrite_ x+4_________________ "; +" _________________ rewrite_ x+4_________________ "; +" _________________ rewrite_ x+4_________________ "; +val t = (term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; +val thm = num_str square_equation_left; +val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t); +val rls = Test_simplify; +val (t,_) = the (rewrite_set_ thy false rls t); +val rls = rearrange_assoc; +val (t,_) = the (rewrite_set_ thy false rls t); +val rls = isolate_root; +val (t,_) = the (rewrite_set_ thy false rls t); + +val rls = Test_simplify; +val (t,_) = the (rewrite_set_ thy false rls t); +(* +sqrt (x ^^^ 2 + 5 * x) = +(5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +### trying thm 'rdistr_div_right' +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +(5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2) +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +(5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2)) +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +5 / (-1 * 2) + 2 * x / (-1 * 2) + +(-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2)) + +### trying thm 'radd_left_commute' +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +-1 * 9 / (-1 * 2) + +(5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)) +### trying thm 'radd_assoc' +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +-1 * 9 / (-1 * 2) + +(5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))) + +### trying thm 'radd_real_const_eq' +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +-1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2)) +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +-1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2) +### rewrites to: sqrt (x ^^^ 2 + 5 * x) = +(-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +28.8.02: ruleset besser zusammenstellen !!! +*) +val thm = num_str square_equation_left; +val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t); +val asm = asm union asm'; +val rls = Test_simplify; +val (t,_) = the (rewrite_set_ thy false rls t); +val rls = norm_equation; +val (t,_) = the (rewrite_set_ thy false rls t); +val rls = Test_simplify; +val (t,_) = the (rewrite_set_ thy false rls t); +val rls = isolate_bdv; +val subst = [(str2term "bdv", str2term "x")]; +val (t,_) = the (rewrite_set_inst_ thy false subst rls t); +val rls = Test_simplify; +val (t,_) = the (rewrite_set_ thy false rls t); +val t' = term2str t; +if t' = "x = 4" then () +else raise error "root-equ.sml: new behav. in rewrite_ x+4"; + +" _________________ rewrite x=4_________________ "; +" _________________ rewrite x=4_________________ "; +" _________________ rewrite x=4_________________ "; +(* +rewrite thy' "tless_true" "tval_rls" true (num_str rbinom_power_2) ct; +atomty thy ((#prop o rep_thm) (!tthm)); +atomty thy (term_of (!tct)); +*) +val thy' = "Test.thy"; +val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; +(*1*)val thm = ("square_equation_left",""); +val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); +"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2"; +(*2*)val rls = "Test_simplify"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))"; +(*3*)val rls = "rearrange_assoc"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)"; +(*4*)val rls = "isolate_root"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"; +(*5*)val rls = "Test_simplify"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"sqrt (x ^^^ 2 + 5 * x) = 2 + x"; +(*6*)val thm = ("square_equation_left",""); +val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct); +val asm = asm union asm'; +"x ^^^ 2 + 5 * x = (2 + x) ^^^ 2"; +(*7*)val rls = "Test_simplify"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)"; +(*8*)val rls = "norm_equation"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"; +(*9*)val rls = "Test_simplify"; +val (ct,_) = the (rewrite_set thy' false rls ct); +"-4 + x = 0"; +(*10*)val rls = "isolate_bdv"; +val (ct,_) = the (rewrite_set_inst thy' false + [("bdv","x")] rls ct); +"x = 0 + -1 * -4"; +(*11*)val rls = "Test_simplify"; +val (ct,_) = the (rewrite_set thy' false rls ct); +if ct="x = 4" then () else raise error "new behaviour in test-example"; + + + + +" _________________ rewrite + cappend _________________ "; +" _________________ rewrite + cappend _________________ "; +" _________________ rewrite + cappend _________________ "; +val thy' = "Test.thy"; +val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)"; +val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"]; +val oris = prep_ori ctl thy ((#ppc o get_pbt) + ["sqroot-test","univariate","equation","test"]); +val loc = e_istate; +val (pt,pos) = (e_ptree,[]); +val (pt,_) = cappend_problem pt pos loc (oris,empty_spec); +val pt = update_branch pt [] Transitive; +(* +val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt []))); +*) +(*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *) +val pt = update_domID pt [] "Test"; +val pt = update_pblID pt [] ["Test", + "equations","univariate","square-root"]; +val pt = update_metID pt [] ("Test","sqrt-equ-test"); +val pt = update_pbl pt [] []; +val pt = update_met pt [] []; +(* +> get_obj g_spec pt []; +val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec +> val pt = update_domID pt [] "RatArith"; +> get_obj g_spec pt []; +val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec +> val pt = update_pblID pt [] ["RatArith", + "equations","univariate","square-root"]; +> get_obj g_spec pt []; +("RatArith",["RatArith","equations","univariate","square-root"], + ("e_domID","e_metID")) : spec +> val pt = update_metID pt [] ("RatArith","sqrt-equ-test"); +> get_obj g_spec pt []; + ("RatArith",["RatArith","equations","univariate","square-root"], + ("RatArith","sqrt-equ-test")) : spec +*) + +val pos = [1]; +val (pt,_) = cappend_parent pt pos loc ct (Mstep "repeat") Transitive; + +val pos = (lev_on o lev_dn) pos; +val thm = ("square_equation_left",""); val ctold = ct; +val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep (fst thm)) ct Complete; +val pt = union_asm pt [] (map (rpair []) asm); + +val pos = lev_on pos; +val rls = ("Test_simplify"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val rls = ("rearrange_assoc"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val rls = ("isolate_root"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val rls = ("Test_simplify"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val thm = ("square_equation_left",""); val ctold = ct; +val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; +val pt = union_asm pt [] (map (rpair []) asm); + +val pos = lev_up pos; +val (pt,_) = append_result pt pos e_istate ct Complete; + +val pos = lev_on pos; +val rls = ("Test_simplify"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val rls = ("norm_equation"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val rls = ("Test_simplify"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +(* --- see comments in interface_ME_ISA/instantiate'' +val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv"); +val (ct,_) = the (rewrite_set thy' false + ("#isolate_bdv",rlsdat') ct); *) +val pos = lev_on pos; +val rls = ("isolate_bdv"); val ctold = ct; +val (ct,_) = the (rewrite_set_inst thy' false + [("bdv","x")] rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_on pos; +val rls = ("Test_simplify"); val ctold = ct; +val (ct,_) = the (rewrite_set thy' false rls ct); +val (pt,_) = cappend_atomic pt pos loc ctold (Mstep rls) ct Complete; + +val pos = lev_up pos; +val (pt,pos) = append_result pt pos e_istate ct Complete; +get_obj g_asm pt []; + +writeln (pr_ptree pr_short pt); +(* aus src.24-11-99: +. sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0) +1. sqrt(9+4*x)=sqrt x + sqrt(5+x) +1.1. sqrt(9+4*x)=sqrt x + sqrt(5+x) +1.2. 9 + 4 * x = (sqrt x + sqrt (5 + x) ) ^^^ 2 +1.3. 9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) ) +1.4. 9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) +1.5. sqrt (5 * x + x ^^^ 2) = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2)) +1.6. sqrt (5 * x + x ^^^ 2) = (+2) + x +2. 5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2 +3. 5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2) ###12.12.99: indent 2.1. !?! +4. 5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0) +5. (-4) + x = (+0) +6. x = (+0) + (-1) * (-4) +*) + +(* +val t = (term_of o the o (parse thy)) "solutions (L::real set)"; +atomty thy t; +*) + + +(*- 20.9.02: Free_Solve would need the erls (for conditions of rules) + from thy ???, i.e. together with the *_simplify ?!!!? ---------- +" _________________ me Free_Solve _________________ "; +" _________________ me Free_Solve _________________ "; +" _________________ me Free_Solve _________________ "; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"(*, + "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); + +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +(*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x) )");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = ("Add_Given",Add_Given "bound_variable x");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = ("Add_Given",Add_Given "error_bound #0");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = ("Add_Find",Add_Find "solutions L"); *) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = ("Specify_Domain",Specify_Domain "DiffAppl.thy"); +> get_obj g_spec pt (fst p); +val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Problem", Specify_Problem *) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = ("Free_Solve",Free_Solve); +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +get_obj g_spec pt []; + +"--- -2 ---"; +get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt; +val (p,_,f,nxt,_,pt)= +me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt; +(* 15.4. +"--- -1 ---"; +get_form ("Begin_Trans",Begin_Trans) p pt; +val (p,_,f,nxt,_,pt)= +me ("Begin_Trans",Begin_Trans) p [4] pt; *) + +"--- 1 ---"; +get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt; +"--- 2 ---"; +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt; +"--- 3 ---"; +get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt; +"--- 4 ---"; +get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt; +"--- 5 ---"; +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt; +"--- 6 ---"; +get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt; +(* 15.4. +"--- ---"; +get_form ("End_Trans",End_Trans) p pt; +val (p,_,f,nxt,_,pt)= +me ("End_Trans",End_Trans) p [11] pt; *) +"--- 7 ---"; +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt; +"--- 8 ---"; +get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt; +"--- 9 ---"; +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt; +"--- 10 ---."; +get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt; +val (p,_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt; +"--- 11 ---"; +get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt; +val ((p,p_),_,f,nxt,_,pt)= +me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt; +(* 5.4.00.: --- +get_form ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) pt; +val (p,_,f,nxt,_,pt)= +me ("Check_Postcond",Check_Postcond ("Test.thy","solve-root-equation")) (p,Met) [17] pt; +--- *) +writeln (pr_ptree pr_short pt); +writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*; +*) + + +" _________________ me + msteps input _________________ "; +" _________________ me + msteps input _________________ "; +" _________________ me + msteps input _________________ "; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +"--- s1 ---"; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +"--- s2 ---"; +val nxt = ("Add_Given", +Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s3 ---"; +val nxt = ("Add_Given",Add_Given "solveFor x"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s4 ---"; +val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s5 ---"; +val nxt = ("Add_Find",Add_Find "solutions L"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s6 ---"; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s7 ---"; +val nxt = ("Specify_Problem", +Specify_Problem ["sqroot-test","univariate","equation","test"]); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s8 ---"; +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- s9 ---"; +val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test")); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 1 ---"; +val nxt = ("Rewrite",Rewrite ("square_equation_left","")); +val (p,_,f,nxt,_,pt) = me nxt p c pt; + +(*me------------ + val (mI,m) = nxt; val pos' as (p,p_) = p; + + val Appl m = applicable_in (p,p_) pt m; +(*solve*) + val pp = par_pblobj pt p; + val metID = get_obj g_metID pt pp; + val sc = (#scr o get_met) metID; + val is = get_istate pt (p,p_); + val thy' = get_obj g_domID pt pp; + val thy = assoc_thy thy'; + val d = e_rls; + val Steps [(m',f',pt',p',c',s')] = + locate_gen thy' m (pt,(p,p_)) (sc,d) is; + val is' = get_istate pt' p'; + next_tac thy' (pt'(*'*),p') sc is'; + + + + +val ttt = (term_of o the o (parse Test.thy)) +"Let (((While contains_root e_ Do\ +\Rewrite square_equation_left True @@\ +\Try (Rewrite_Set Test_simplify False) @@\ +\Try (Rewrite_Set rearrange_assoc False) @@\ +\Try (Rewrite_Set Test_simplify False)) @@\ +\Try (Rewrite_Set norm_equation False) @@\ +\Try (Rewrite_Set Test_simplify False) @@\ +\Rewrite_Set_Inst [(bdv, v_)] isolate_bdv False @@\ +\Try (Rewrite_Set Test_simplify False))\ +\e_)"; + +-------------------------*) + + +"--- 2 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 3 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 4 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 5 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 6 ---"; +val nxt = ("Rewrite",Rewrite ("square_equation_left","")); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 7 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 8<> ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 9<> ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 10<> ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 11<> ---."; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 12<> ---"; +val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 13<> ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p c pt; +"--- 1<> ---"; +val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(* val nxt = ("End_Proof'",End_Proof');*) +if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) +then raise error "me + msteps input: not finished correctly" +else "root-equation, me + msteps input: OK"; + +writeln (pr_ptree pr_short pt); +writeln("result: "^(get_obj g_result pt [])^ +"\n=============================================================="); + + + diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/script.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/script.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,996 @@ +(* use"test-script.sml"; + WN.13.3.00 + *) + +" scripts: Variante 'funktional' "; +"############## Make_fun_by_new_variable ##############"; +"############## Make_fun_by_explicit ##############"; +"################ Solve_root_equation #################"; +"------- Notlocatable: Free_Solve -------"; + +" --- test100: nxt_tac order------------------------------------ "; +" --- test100: order 1 3 1 2 ----------------------------------- "; +" --- test200: nxt_tac order ------------------------------------- "; +" --- test200: order 3 1 1 2 --------------------------------- "; + +" --- root-equation: nxt_tac order------------------------------ "; +" --- root-equation: 1.norm_equation ------------------------------ "; +(* --- test200: calculate -----------------------------------------*) +" --- check_elementwise ------------------------------ "; + +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; + + + + + + +" #################################################### "; +" scripts: Variante 'funktional' "; +" #################################################### "; + +val c = (the o (parse DiffApp.thy)) + "Script Maximum_value(fix_::bool list)(m_::real) (rs_::bool list)\ + \ (v_::real) (itv_::real set) (err_::bool) = \ + \ (let e_ = (hd o (filter (Testvar m_))) rs_; \ + \ t_ = (if 1 < Length rs_ \ + \ then (SubProblem (Reals_,[make,function],(Isac_,no_met))\ + \ [real_ m_, real_ v_, bool_list_ rs_])\ + \ else (hd rs_)); \ + \ (mx_::real) = SubProblem (Reals_,[on_interval,max_of,function], \ + \ (DiffAppl_,maximum_on_interval))\ + \ [bool_ t_, real_ v_, real_set_ itv_]\ + \ in ((SubProblem (Reals_,[find_values,tool],(DiffAppl_,find_values)) \ + \ [real_ mx_, real_ (Rhs t_), real_ v_, real_ m_, \ + \ bool_list_ (dropWhile (ident e_) rs_)])::bool list))"; + + +"######################################################"; +"############## Make_fun_by_new_variable ##############"; +"######################################################"; + +val sc = (the o (parse DiffApp.thy)) (*start interpretieren*) + "Script Make_fun_by_new_variable (f_::real) (v_::real) \ + \ (eqs_::bool list) = \ + \(let h_ = (hd o (filter (Testvar m_))) eqs_; \ + \ es_ = dropWhile (ident h_) eqs_; \ + \ vs_ = dropWhile (ident f_) (Var h_); \ + \ v1_ = Nth 1 vs_; \ + \ v2_ = Nth 2 vs_; \ + \ e1_ = (hd o (filter (Testvar v1_))) es_; \ + \ e2_ = (hd o (filter (Testvar v2_))) es_; \ + \ (s_1::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\ + \ [bool_ e1_, real_ v1_]);\ + \ (s_2::bool list) = (SubProblem(Reals_, [univar,equation],(Isac_,no_met))\ + \ [bool_ e2_, real_ v2_])\ + \in Substitute [(v_1, (Rhs o hd) s_1),(v_2, (Rhs o hd) s_2)] h_)"; +val ags = map (term_of o the o (parse DiffApp.thy)) + ["A::real", "alpha::real", + "[A=a*b, a/2=r*sin alpha, b/2=r*cos alpha]"]; +val ll = []:loc_; +(* problem with exn PTREE + eval_to ------------------------- +"-------------- subproblem with empty formalizaton -------"; +val (mI1,m1) = + ("Subproblem", mstep2mstep' pt p + (Subproblem (("Reals",["univar","equation","test"], + (""(*"ANDERN !!!!!!!*),"no_met")),[]))); +val (mI2,m2) = (mI1,m1); +val (mI3,m3) = + ("Substitute", mstep2mstep' pt p + (Substitute [("a","#2*r*sin alpha"),("b","#2*r*cos alpha")])); +"------- same_tacpbl + eval_to -------"; +val Some(l1,t1) = same_tacpbl sc ll (mI1,m1); +loc_2str l1; +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) +Sign.string_of_term (sign_of DiffApp.thy) t1; +(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *) + +val Some(l2,t2) = same_tacpbl sc l1 (mI2,m2); +loc_2str l2; +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*) +Sign.string_of_term (sign_of DiffApp.thy) t2; +(*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *) + +val Some(l3,t3) = same_tacpbl sc l2 (mI3,m3); +loc_2str l3; +(*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*) +Sign.string_of_term (sign_of DiffApp.thy) t3; +(*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*) + + +"------- eq_tacIDs + eq_consts + eval_args -------"; +val eq_ids = eq_tacIDs (*start-loc_*)[] sc (mI,m) []; +val eq_cons = filter (eq_consts m) eq_ids; +val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons; +"------- locate -------"; + + +"-------------- subproblem with formalizaton -------"; +val (mI,m) = + ("Subproblem", mstep2mstep' pt [] + (Subproblem (("Reals",["univar","equation","test"], + (""(*"ANDERN !!!!!!!*),"no_met")), + ["a//#2=r*sin alpha","a"]))); +"------- same_tacpbl + eval_to -------"; + + +"------- eq_tacIDs + eq_consts + eval_args -------"; +val eq_ids = eq_tacIDs [] sc (mI,m) []; +val eq_cons = filter (eq_consts m) eq_ids; +val Ready (l,(_,m)::_,_) = eval_args sc (mI,m) [(1,ags)] eq_cons; + + +"------- locate -------"; +-------------------------------------------------------*) +(* use"ME/script.sml"; + use"test-script.sml"; + *) + + + +(*#####################################################*) +(*#####################################################*) +"############## Make_fun_by_explicit ##############"; +val c = (the o (parse DiffApp.thy)) + "Script Make_fun_by_explicit (f_::real) (v_::real) \ + \ (eqs_::bool list) = \ + \ (let h_ = (hd o (filter (Testvar m_))) eqs_; \ + \ e1_ = hd (dropWhile (ident h_) eqs_); \ + \ vs_ = dropWhile (ident f_) (Var h_); \ + \ v1_ = hd (dropWhile (ident v_) vs_); \ + \ (s1::bool list) = (SubProblem (Reals_, [univar,equation],(Isac_,no_met))\ + \ [bool_ e1_, real_ v1_])\ + \ in Substitute [(v_1, (Rhs o hd) s_1)] h_)"; + + +(*#####################################################--------11.5.02 +"################ Solve_root_equation #################"; +(*#####################################################*) +val sc = (term_of o the o (parse Test.thy)) + "Script Solve_root_equation (eq_::bool) (v_::real) (err_::bool) =\ + \ (let e_ = Rewrite square_equation_left True eq_; \ + \ e_ = Rewrite_Set Test_simplify False e_; \ + \ e_ = Rewrite_Set rearrange_assoc False e_; \ + \ e_ = Rewrite_Set isolate_root False e_; \ + \ e_ = Rewrite_Set Test_simplify False e_; \ + + \ e_ = Rewrite square_equation_left True e_; \ + \ e_ = Rewrite_Set Test_simplify False e_; \ + + \ e_ = Rewrite_Set norm_equation False e_; \ + \ e_ = Rewrite_Set Test_simplify False e_; \ + \ e_ = Rewrite_Set_Inst [(bdv,v_)] isolate_bdv False e_;\ + \ e_ = Rewrite_Set Test_simplify False e_ \ + \ in [e_::bool])"; +val ags = map (term_of o the o (parse Test.thy)) + ["sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)", "x::real","#0"]; +val fmz = + ["equality (sqrt(#9+#4*x)=sqrt x + sqrt(#5+x))", + "solveFor x","errorBound (eps = #0)","solutions v_i_"]; +----------------------------------------------------------------11.5.02...*) + + +(*#####################################################*) +"------- Notlocatable: Free_Solve -------"; +"------- Notlocatable: Free_Solve -------"; +"------- Notlocatable: Free_Solve -------"; +val fmz = []; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) e_pos'[1] EmptyPtree; +val nxt = + ("Add_Given", + Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = ("Add_Given",Add_Given "solveFor x"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = ("Add_Find",Add_Find "solutions v_i_"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = + ("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation","test"]); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; + +"--- -1 ---"; +val nxt = ("Free_Solve",Free_Solve); +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +"--- 0 ---"; +val nxt = ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)"); +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +(*me ("Begin_Trans" ////*) + +"--- 1 ---"; +val nxt = ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")); +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +"--- 2 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify"); +val (p,_,f,nxt,_,pt) = me nxt p [] pt; + +"--- 3 ---"; +val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); +val (p,_,f,nxt,_,pt) = me nxt p [] pt; +if f = Form' + (FormKF + (~1,EdUndef,1,Nundef, + "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)")) +then () else raise error "behaviour in root-expl. Free_Solve changed"; +writeln (pr_ptree pr_short pt); + + + +val d = e_rls; + +" --- test100: nxt_tac order------------------------------------ "; +" --- test100: nxt_tac order------------------------------------ "; + +val scr as (Script sc) = Script (((inst_abs Test.thy) + o term_of o the o (parse thy)) + "Script Testeq (e_::bool) = \ + \(While (contains_root e_) Do \ + \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ + \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ + \ (Try (Repeat (Rewrite radd_0 False)))))\ + \ e_ "); +atomty thy sc; +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Res):pos'; +val eq_ = (term_of o the o (parse thy))"e_::bool"; + +val ct = "0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0"; +val ve0_= (term_of o the o (parse thy)) ct; +val ets0=[([],(Mstep'(Script.thy,"BS","",""),[(eq_,ve0_)],[(eq_,ve0_)], + e_term,e_term,Safe)), + ([],(User', [], [], e_term, e_term,Sundef))]:ets; +val l0 = []; +" --------------- 1. ---------------------------------------------"; +val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete; +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); + + +(*-----------11.5.02: ets disabolished ------------------ + +val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0; +(*val l = [R,R,L,R,R,R] : loc_ + val m' = Rewrite'...("rroot_square_inv",..(sqrt (sqrt (sqrt a)).. + -> sqrt (sqrt a)*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; +writeln(ets2str ets1); +" --------------- 2. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); + +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*val l = [R,R,L,R,R,R] : loc_ +val m' = Rewrite'...("rroot_square_inv",..,sqrt (sqrt a).. + -> #0+ sqrt a =#0*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +writeln(ets2str ets2); +" --------------- 3. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite("radd_0","")); + +val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +(*val l = [R,R,R,D,R,D,R,R] : loc_ +val m' = Rewrite'...("radd_0","")..(#0 + sqrt a = #0)..-> sqrt a = #0*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; +writeln(ets2str ets3); +" --------------- 4. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite("square_equation_left","")); + +val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3; +(*val l = [R,R,R,D,L,R,R,R] : loc_ +val m' = Rewrite'...("square_equation_left"..(sqrt a = #0)..a = #0^#2*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = +(*=====*) locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; + +" --------------- 5. ---------------------------------------------"; +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; + +writeln (pr_ptree pr_short pt);writeln("result: "^res^ +"\n==================================================================="); +"--- test100 nxt_tac order: finished correctly ---------------"; +"--- test100 nxt_tac order: finished correctly ---------------"; +"--- test100 nxt_tac order: finished correctly ---------------"; + + + + +" --- test100: order 1 3 1 2 ----------------------------------- "; +" --- test100: order 1 3 1 2 ----------------------------------- "; +val scr as (Script sc) = + Script (((inst_abs Test.thy) o term_of o the o (parse thy)) + "Script Testeq (e_::bool) = \ + \While (contains_root e_) Do \ + \ (let e_ = Try (Repeat (Rewrite rroot_square_inv False e_)); \ + \ e_ = Try (Repeat (Rewrite square_equation_left True e_)) \ + \ in Try (Repeat (Rewrite radd_0 False e_))) "); +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Res):pos'; +val eq_ = (term_of o the o (parse thy))"e_::bool"; + +val ct = "#0+(sqrt(sqrt(sqrt a))^^^#2)^^^#2=#0"; +val ve0_= (term_of o the o (parse thy)) ct; +val ets0=[([],(Mstep'(Script.thy,"bS","",""),[(eq_,ve0_)],[(eq_,ve0_)], + e_term,e_term,Safe)), + ([],(User', [], [], e_term, e_term,Sundef))]:ets; +val l0 = []; +" --------------- 1. --- test100 order 1 3 1 2 --------------------"; +val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete; +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; +writeln (ets2str ets1); +" --------------- 2. --- test100 order 1 3 1 2 --------------------"; +val Appl m'=applicable_in p pt (Rewrite("radd_0","")); +val Rewrite'(_,_,_,_,("radd_0",""),f,(_,[])) = m'; +Sign.string_of_term (sign_of (thy)) f; +(*"#0 + sqrt (sqrt a) ^^^ #2 = #0" + -> AssocWeak .. pt aus ass_up,ass_dn,assy _verworfen_.. nur letzte tac*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +" --------------- 3. --- test100 order 1 3 1 2 --------------------"; +val Appl m'=applicable_in p pt (Rewrite("rroot_square_inv","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; +" --------------- 4. --- test100 order 1 3 1 2 --------------------"; +val Appl m'=applicable_in p pt (Rewrite("square_equation_left","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; +if res="a = #0 ^^^ #2"then()else raise error "test100 order 1 3 1 2"; +" --------------- 5. --- test100 order 1 3 1 2 --------------------"; +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; +writeln (pr_ptree pr_short pt);writeln("result: "^res^ +"\n==================================================================="); +"--- test100 order 1 3 1 2: finished correctly --------------"; +"--- test100 order 1 3 1 2: finished correctly --------------"; + + + + +" --- test200: nxt_tac order ------------------------------------- "; +" --- test200: nxt_tac order ------------------------------------- "; + +val scr as (Script sc) = + Script (((inst_abs Test.thy) o term_of o the o (parse thy)) + "Script Testterm (g_::real) = \ + \Repeat \ + \ ((Repeat (Rewrite rmult_1 False g_)) Or \ + \ (Repeat (Rewrite rmult_0 False g_)) Or \ + \ (Repeat (Rewrite radd_0 False g_))) "); +val d = e_rls; (*domain-rls for assod*) +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Res):pos'; +val g_ = (term_of o the o (parse thy)) "g_"; + +val ct = "(#0+#0)*(#1*(#1*a))"; +val vg0_= (term_of o the o (parse thy)) ct; +val ets0 = [([],(Mstep'(Script.thy,"sB","",""), [(g_,vg0_)], [(g_,vg0_)], + e_term, e_term,Safe)), + ([],(User', [], [], e_term, e_term,Sundef))]:ets; +val l0 = []; +" --------------- 1. ---------------------------------------------"; +val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete; +val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); + +val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0; +(*val l = [R,R,L,R,L,R,R] : loc_ +val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*(#1*a)*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; + +" --------------- 2. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); + +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*val l = [R,R,L,R,L,R,R] : loc_ +val m' = Rewrite' ... ("rmult_1","") (#0+#0)*#1*a*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; + +" --------------- 3. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite("radd_0","")); + +val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +(*val l = [R,R,R,R] : loc_ +val m' = Rewrite'...("radd_0","") (#0+#0)*a *) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; + +" --------------- 4. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite("rmult_0","")); + +val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3; +(*al l = [R,R,L,R,R,R] : loc_ +val m' = Rewrite'...("rmult_0","") #0*a *) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; + +" --------------- 5. ---------------------------------------------"; +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; +(*al l = [R,R,L,R,R,R] : loc_ +val m' = Rewrite'...("rmult_0","") #0*a *) +writeln (pr_ptree pr_short pt);writeln("result: "^res^ +"\n==================================================================="); +"--- test200 nxt_tac order: finished correctly ---------------"; +"--- test200 nxt_tac order: finished correctly ---------------"; + + + + +" --- test200: order 3 1 1 2 --------------------------------- "; +" --- test200: order 3 1 1 2 --------------------------------- "; +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Res):pos'; +val g_ = (term_of o the o (parse thy)) "g_"; + +val ct = "(#0+#0)*(#1*(#1*a))"; +val vg0_= (term_of o the o (parse thy)) ct; +val ets0 = [([],(Mstep'(Script.thy,"sB","",""),[(g_,vg0_)],[(g_,vg0_)], + e_term,e_term,Safe)), + ([],(User', [], [], e_term, e_term,Sundef))]:ets; +val l0 = []; +" --------------- 1. --- test200: order 3 1 1 2 -----------------"; +val (pt,_) = cappend_atomic pt[1]e_istate ""(Rewrite("test",""))ct Complete; +val Appl m'=applicable_in p pt (Rewrite("radd_0","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; + +" --------------- 2. --- test200: order 3 1 1 2 -----------------"; +val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res="#0 * (#1 * a)"then()else raise error "error test200: order 3 1 1 2"; +" --------------- 3. --- test200: order 3 1 1 2 -----------------"; +val Appl m'=applicable_in p pt (Rewrite("rmult_1","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; + +" --------------- 4. --- test200: order 3 1 1 2 -----------------"; +val Appl m'=applicable_in p pt (Rewrite("rmult_0","")); + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; + +if res="#0"then()else raise error "test200 order 3 1 1 2"; +" --------------- 5. --- test200: order 3 1 1 2 -----------------"; +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; +writeln (pr_ptree pr_short pt);writeln("result: "^res^ +"\n==================================================================="); +"--- test200 order 3 1 1 2: finished correctly ---------------"; +"--- test200 order 3 1 1 2: finished correctly ---------------"; + + +------------------------------------11.5.02: ets disabolished ---*) +(* use"test-script-nxt_tac.sml"; + *) + +(*---------11.5.02: +### Currently parsed expression could be extremely ambiguous. ---------- + +" --- root-equation: nxt_tac order------------------------------ "; +" --- root-equation: nxt_tac order------------------------------ "; +val scr as (Script sc) = + Script (((inst_abs Test.thy) o term_of o the o (parse thy)) + "Script Solve_root_equation (e_::bool) (v_::real) (err_::bool) =\ + \ (let e_ = \ + \ (While (contains_root e_) Do \ + \ (let \ + \ e_ = Rewrite square_equation_left True e_; \ + \ e_ = Try (Rewrite_Set Test_simplify False e_); \ + \ e_ = Try (Rewrite_Set rearrange_assoc False e_); \ + \ e_ = Try (Rewrite_Set isolate_root False e_) \ + \ in Try (Rewrite_Set Test_simplify False e_))); \ + \ e_ = Try (Rewrite_Set norm_equation False e_); \ + \ e_ = Try (Rewrite_Set Test_simplify False e_); \ + \ e_ = Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False e_;\ + \ e_ = Try (Rewrite_Set Test_simplify False e_) \ + \ in [e_::bool])"); +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Frm):pos'; + +val bdv_ =(term_of o the o (parse thy))"v_::real"; +val v_ =(term_of o the o (parse thy))"x::real"; +val eq_ = (term_of o the o (parse thy))"e_::bool"; +val ct = "sqrt(#9+#4*x)=sqrt x + sqrt(#5+x)"; +val ve0_= (term_of o the o (parse thy)) ct; +val env= [(bdv_, v_), (eq_, ve0_)]; +val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)), + ([],(User', [], [], e_term, e_term,Sundef))]:ets; +val l1 = []; +" -------root-equation--- 1.--- nxt_tac-order----------------------"; +val (pt,_) = cappend_form pt[1]e_istate ct; + +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*square_equation_left*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 2.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +(* +> val eee = (hd) ets2; +> val (_,(_,_,ennv,_,rees,_)) = eee; +> subst2str ennv; +> Sign.string_of_term (sign_of ( thy)) rees; +*) +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*Test_simplify*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 3.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*rearrange_assoc*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 4.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*isolate_root*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 * #2)" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 5.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*Test_simplify*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "sqrt (x ^^^ #2 + #5 * x) = #2 + x" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 6.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*square_equation_left*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 7.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*Test_simplify*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 8.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*rearrange_assoc ...<> test-root-equ.sml: norm_equation*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x" +(* "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0" + ...<> test-root-equ.sml*) +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 9.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +(*> Sign.string_of_term (sign_of thy) (go l2 sc); +val it = "Rewrite_Set rearrange_assoc False e_" : string*) + +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*Test_simplify*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 10.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*norm_equation*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 11.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*Test_simplify*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "#-4 + x = #0" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 12.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*isolate_bdv*) +(*> val eee = (last_elem o drop_last) ets2; +> val (_,(mmm,_,ennv,_,rees,_)) = eee; +val mmm = Rewrite_Set' + ("Test.thy","erls",false,"Test_simplify",# $ # $ Free #,(# $ #,[])) +> writeln(subst2str ennv); +["(e_, x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0)"] +> Sign.string_of_term (sign_of ( thy)) rees; +val it = "#-4 + x = #0" : string*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x = #0 + #-1 * #-4" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 13.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*Test_simplify*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "x = #4" +then () else raise error "new behaviour in test-example"; +writeln (pr_ptree pr_short pt); +" -------root-equation--- 14.--- nxt_tac-order----------------------"; +val ets1 = ets2; val l1 = l2; +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets1 l1; + +writeln (pr_ptree pr_short pt); +writeln("result: "^res^"\n==================================================================="); +" --- root-equation: nxt_tac order .. finised correctly --------- "; +" --- root-equation: nxt_tac order .. finised correctly --------- "; + + +-------------------------------------11.5.02-----*) +(*-----------------------------------11.5.02 ets disabolished ------- + +" --- root-equation: 1.norm_equation ------------------------------ "; +" --- root-equation: 1.norm_equation ------------------------------ "; +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Frm):pos'; +val ets1 =[([],(Mstep'(Script.thy,"BS","",""),env,env,e_term,e_term,Safe)), + user_interrupt]:ets; +" -------root-equation--- 1.--- 1.norm_equation----------------------"; +val (pt,_) = cappend_form pt[1]e_istate ct; +val Appl m'= applicable_in p pt (Rewrite_Set "norm_equation"); + +val l1 = (fst o last_elem o drop_last) ets1; +(*val l1 = [R,L,R,R,L,R];//////////////test-root_equ, me 11.10.00*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "sqrt (#9 + #4 * x) + #-1 * (sqrt x + sqrt (#5 + x)) = #0" +then () else raise error "new behaviour in test-example"; + +val l2 = (fst o last_elem o drop_last) ets2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +val ets1 = ets2; +" -------root-equation--- 2.--- 1.norm_equation----------------------"; +(*m'=Rewrite_Set'...,"Test_simplify" *) +val l1 = (fst o last_elem o drop_last) ets1; +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +if res = "#-1 * sqrt x + (#-1 * sqrt (#5 + x) + sqrt (#9 + #4 * x)) = #0" +then () else raise error "new behaviour in test-example"; + +val Notappl _ = + applicable_in p pt (Rewrite_Set_Inst(["(bdv,v_)"],"isolate_bdv")); +val Notappl _ = applicable_in p pt (Rewrite_Set "Test_simplify"); + +val l2 = (fst o last_elem o drop_last) ets2; +val Helpless = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +(* ~~~~ because isolate_bdv goes without Try *) +writeln (pr_ptree pr_short pt); +val ets1 = ets2; +" -------root-equation--- 3.--- 1.norm_equation----------------------"; +val Appl m'= applicable_in p pt (Rewrite_Set "rearrange_assoc"); + +val l1 = (fst o last_elem o drop_last) ets1; +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; + +val l2 = (fst o last_elem o drop_last) ets2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +writeln (pr_ptree pr_short pt); +val ets1 = ets2; +" -------root-equation--- 4.--- 1.norm_equation----------------------"; +(*m' = .. isolate_root*) +val l1 = (fst o last_elem o drop_last) ets1; +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; + +val l2 = (fst o last_elem o drop_last) ets2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +writeln (pr_ptree pr_short pt); +val ets1 = ets2; +" -------root-equation--- 5.--- 1.norm_equation----------------------"; +(*m' = .. Test_simplify*) +val l1 = (fst o last_elem o drop_last) ets1; +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; + +val l2 = (fst o last_elem o drop_last) ets2; +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +writeln (pr_ptree pr_short pt); +if res="sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)" then () +else raise error "new behaviour in test-example"; + +-------------------------------------11.5.02-----*) + + +(* use"test-script.sml"; + *) + + + + + + + +(* --- test200: calculate ----------------------------------------- +" --- test200: calculate -----------------------------------------"; +val scr as (Script sc) = + Script (((inst_abs Test.thy) o term_of o the o (parse thy)) + "Script Testterm (g_::real) = \ + \Repeat (Calculate plus g_) "); +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val p = ([1],Res):pos'; +val g_ = (term_of o the o (parse thy)) "g_"; +val vg_= (term_of o the o (parse thy)) "#1+#2"; +val env = [(g_,vg_)]; + +val ets = []:ets; +(* --------------- 1. ---------------------------------------------*) +val (pt,_) = cappend_atomic pt [1] e_istate "" + (Rewrite("test","")) "#1+#2" Complete; +val Appl m'=applicable_in p pt (Calculate "plus"); + +val NextStep(l,m') = nxt_tac "Test.thy" (pt,p) scr ets l; +(*val l = [R,R,R,R] : loc_ + val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*) + +val ets = (l,mstep'2etac m')::ets; +(* --------------- 2. ---------------------------------------------*) +val (pt,_) = cappend_atomic pt [1] e_istate "" + (Rewrite("test","")) "#3" Complete; + +val Helpless = nxt_tac "Test.thy" (pt,p) scr ets l; +(*val l = [R,R,R,R] : loc_ + val m' = Calculate' ("Test.thy","plus", #1+#2 = #3*) +---*) + + +(* --- test200: Test_simplify ----------------------------------- + +val scr as (Script sc) = + Script (((inst_abs Test.thy) o term_of o the o (parse thy)) + "Script Testterm (g_::real) = \ + \Repeat \ + \ ((Repeat (Rewrite radd_mult_distrib2 False g_)) Or \ + \ (Repeat (Rewrite rdistr_right_assoc False g_)) Or \ + \ (Repeat (Rewrite rdistr_right_assoc_p False g_)) Or \ + \ (Repeat (Rewrite rdistr_div_right False g_)) Or \ + \ (Repeat (Rewrite rbinom_power_2 False g_)) Or \ + \ (Repeat (Rewrite radd_commute False g_)) Or \ + \ (Repeat (Rewrite radd_left_commute False g_)) Or \ + \ (Repeat (Rewrite radd_assoc False g_)) Or \ + \ (Repeat (Rewrite rmult_commute False g_)) Or \ + \ (Repeat (Rewrite rmult_left_commute False g_)) Or \ + \ (Repeat (Rewrite rmult_assoc False g_)) Or \ + \ (Repeat (Rewrite radd_real_const_eq False g_)) Or \ + \ (Repeat (Rewrite radd_real_const False g_)) Or \ + \ (Repeat (Calculate plus g_)) Or \ + \ (Repeat (Calculate times g_)) Or \ + \ (Repeat (Rewrite rcollect_right False g_)) Or \ + \ (Repeat (Rewrite rcollect_one_left False g_)) Or \ + \ (Repeat (Rewrite rcollect_one_left_assoc False g_)) Or \ + \ (Repeat (Rewrite rcollect_one_left_assoc_p False g_))) "); +---*) +writeln +"%%%%%%%%%%TODO 7.9.00---vvvvvv--- conflicts with Isa-types \n\ +\ (Repeat (Calculate cancel g_)) Or \n\ +\ (Repeat (Calculate pow g_)) Or \n\ +\%%%%%%%%%%%%%%%%%%%%%---^^^^^^--- conflicts with Isa-types \n\ +\%%%%%%%%%%%%%%%%%%%%%TODO before Detail Rewrite_Set"; + + +(*-------------------------------------11.5.02 ets disablished ------- + +" --- check_elementwise ------------------------------ "; +" --- check_elementwise ------------------------------ "; +val d = e_rls; +val scr as (Script sc) = Script (((inst_abs Test.thy) + o term_of o the o (parse thy)) + "Script Testchk (e_::bool) (v_::real) = \ + \ (let e_ = Try (Rewrite_Set Test_simplify False e_); \ + \ (L_::real list) = Mstep subproblem_equation_dummy; \ + \ L_ = Mstep solve_equation_dummy \ + \ in Check_elementwise L_ {(v_::real). Assumptions})"); +val (dI',pI',mI') = ("Test.thy",e_pblID, + ("Test.thy","sqrt-equ-test")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof ([], (dI',pI',mI'))); +val (p,_,_,_,_,pt) = me (mI,m) p c EmptyPtree; +val nxt = ("Specify_Domain",Specify_Domain "Test.thy"); +val (p,_,_,_,_,pt) = me nxt p c pt; +val nxt = ("Specify_Method",Specify_Method("Test.thy","sqrt-equ-test")); (*for asm in square_equation_left*) +val (p,_,_,_,_,pt) = me nxt p c pt; +val pt = union_asm pt [] [("#0 <= sqrt x + sqrt (#5 + x)",[11]), + ("#0 <= #9 + #4 * x",[22]), + ("#0 <= x ^^^ #2 + #5 * x",[33]), + ("#0 <= #2 + x",[44])]; +val p = ([1],Res):pos'; +val eq_ = (term_of o the o (parse thy))"e_::bool"; +val ct = "x=#1+#3"; +val ve0_= (term_of o the o (parse thy)) ct; +val v_ = (term_of o the o (parse thy))"v_::real"; +val xx = (term_of o the o (parse thy))"x::real"; +val env0= [(eq_,ve0_),(v_,xx)]; + +val ets0=[([],(Mstep'(Script.thy,"BS","",""),env0,env0,e_term,e_term,Safe)), + ([],(User', [], [], e_term, e_term,Sundef))]:ets; +val l0 = []; +val (pt,_) = cappend_atomic pt[1]e_istate""(Rewrite("test","")) ct Complete; +" --------------- 1. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Rewrite_Set "Test_simplify"); + +val NextStep(l1,m') = nxt_tac "Test.thy" (pt,p) scr ets0 l0; +(*val l1 = [R,L,R,R] : loc_*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets1)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets0 l0; +(*val ets1 = [([R,L,R,R],(Rewrite_Set' #,[#],[#],Free #,# $ #,Safe)),..*) +val ets1 = (drop_last ets0) @ ets1;val pt = update_ets pt [] [(1,ets1)]; +writeln(ets2str ets1); +" --------------- 2. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Mstep "subproblem_equation_dummy"); + +val NextStep(l2,m') = nxt_tac "Test.thy" (pt,p) scr ets1 l1; +(*val l2 = [R,R,D,L,R] : loc_|| val m' = Mstep' ("x = #4",...*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets2)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets1 l1; +(*val ets2 =[([R,R,D,L,R],(Mstep' ..subpbl..,[#],[#],Const #,# $ #,Safe)),..*) +val ets2 = (drop_last ets1) @ ets2;val pt = update_ets pt [] [(1,ets2)]; +writeln(ets2str ets2); +" --------------- 3. ---------------------------------------------"; +val Appl m'=applicable_in p pt (Mstep "solve_equation_dummy"); + +val NextStep(l3,m') = nxt_tac "Test.thy" (pt,p) scr ets2 l2; +(*val l3 = [R,R,D,R,D,L,R] : loc_ + val m' = Mstep'("subproblem_equation_dummy (x = #4)",..*) +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets3)] = (*@@@*) + locate_gen "Test.thy" m' (pt,p) (scr,d) ets2 l2; +(*val ets3 = [([R,R,D,R,D,L,R], (Mstep' (..,"solve_equation_dummy",..*) +val ets3 = (drop_last ets2) @ ets3; val pt = update_ets pt [] [(1,ets3)]; +writeln(ets2str ets3); +" --------------- 4. ---------------------------------------------"; +val Appl (m' as (Check_elementwise' (consts,"Assumptions",consts'))) = + applicable_in p pt (Check_elementwise "Assumptions"); + +val NextStep(l4,m') = nxt_tac "Test.thy" (pt,p) scr ets3 l3; +(*val l4 = [R,R,D,R,D,R,D] : loc_ val m' = Check_elementwise' (Const (#,#) $ ...*) + +val Steps[(Form' (FormKF (_,_,_,_,res)),pt,p,_,s,ets4)] = + locate_gen "Test.thy" m' (pt,p) (scr,d) ets3 l3; +(*val ets4 = [([R,R,D,R,D,R,D], (Check_elementwise' (# $ #,"Assumptions",Const #),..*) +val ets4 = (drop_last ets3) @ ets4; val pt = update_ets pt [] [(1,ets4)]; +" --------------- 5. ---------------------------------------------"; +val Finished _ = nxt_tac "Test.thy" (pt,p) scr ets4 l4; + +writeln (pr_ptree pr_short pt);writeln("result: "^res^ +"\n==================================================================="); + +-------------------------------------11.5.02-----*) diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/script_if.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/script_if.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,169 @@ +(* 1.if-te-else- 8.02 f"ur Richard + + use"ifthenelse.sml"; + use"tests/rationals2.sml"; + *) + + + +(*---------------- 25.7.02 ---------------------*) + +val thy = Isac.thy; +val t = (term_of o the o (parse thy)) "contains_root (sqrt(x)=1)"; +val Some(ss,tt) = eval_contains_root "xxx" 1 t thy; + +val t = (term_of o the o (parse thy)) "is_rootequation_in (sqrt(x)=1) x"; +val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; + +(*--- +val v = (term_of o the o (parse thy)) "x"; +val t = (term_of o the o (parse thy)) "sqrt(#3+#4*x)"; +scan t v; +val t = (term_of o the o (parse thy)) "sqrt(#3+#4*a)"; +scan t v; +val t = (term_of o the o (parse thy)) "#1 + #2*sqrt(#3+#4*x)"; +scan t v; +val t = (term_of o the o (parse thy)) "x + #2*sqrt(#3+#4*a)"; +scan t v; +---*) +val t = (term_of o the o (parse thy)) + "is_rootequation_in (1 + 2*sqrt(3+4*x)=0) x"; +val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; + +val t = (term_of o the o (parse thy)) + "is_rootequation_in (x + 2*sqrt(3+4*a)=0) x"; +val Some(ss,tt) = eval_is_rootequation_in "is_rootequation_i" 1 t thy; + +val t = (term_of o the o (parse Test.thy)) + "is_rootequation_in (sqrt(x)=1) x"; +atomty Test.thy t; +val t = (term_of o the o (parse Isac.thy)) + "is_rootequation_in (sqrt(x)=1) x"; +atomty Isac.thy t; + +(* +val Some(tt,_) = rewrite_set_ Test.thytrue tval_rls t; +*) +val Some(tt,_) = rewrite_set_ Isac.thy true tval_rls t; + +rewrite_set "Isac.thy" true + "tval_rls" "is_rootequation_in (sqrt(x)=1) x"; +rewrite_set "Test.thy" true + "tval_rls" "is_rootequation_in (sqrt(x)=1) x"; + + +(*WN: ^^^--- bitte nimm vorerst immer Isac.thy, damit wird richtig gematcht, + siehe unten. Wir werden w"ahrend der Arbeit auf diesen Fehler drauskommen*) +store_pbt + (prep_pbt (*Test.thy*) Isac.thy + (["root","univariate","equation","test"], + [("#Given" ,["equality e_","solveFor v_"]), + ("#Where" ,["is_rootequation_in (e_::bool) (v_::real)"]), + ("#Find" ,["solutions v_i_"]) + ], + append_rls e_rls [Calc ("Test.is'_rootequation'_in", + eval_is_rootequation_in "")], + [("Test.thy","methode")])); + +match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"] (get_pbt ["root","univariate","equation","test"]); + + +(*---------------- 29.7.02 ---------------------*) + +store_pbt + (prep_pbt Isac.thy + (["approximate","univariate","equation","test"], + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]), + ("#Where" ,["matches (?a = ?b) e_"]), + ("#Find" ,["solutions v_i_"]) + ], + append_rls e_rls [Calc ("Tools.matches",eval_matches "#matches_")], + [])); + +methods:= overwritel (!methods, +[ + prep_met + (("Isac.thy","solve_univar_err"):metID, + [("#Given" ,["equality e_","solveFor v_","errorBound err_"]), + ("#Find" ,["solutions v_i_"]) + ], + {rew_ord'="tless_true",rls'="tval_rls",erls=e_rls,prls=e_rls,calc=[], + asm_rls=[],asm_thm=[]}, + "Script Solve_univar_err (e_::bool) (v_::real) (err_::bool) = \ + \ (if (is_rootequation_in e_ v_)\ + \ then ((SubProblem (Isac_,[squareroot,univariate,equation],\ + \ (SqRoot_,square_equation)) [bool_ e_, real_ v_, bool_ err_]))\ + \ else ((SubProblem (Isac_,[linear,univariate,equation],\ + \ (RatArith_,solve_linear)) [bool_ e_, real_ v_])))" + )]); + +val fmz = ["equality (1+2*x=0)","solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Isac.thy",["approximate","univariate","equation","test"], + ("Isac.thy","solve_univar_err")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("RatArith.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 / 2]")) + andalso nxt = ("End_Proof'",End_Proof') then () +else raise error "new behaviour in testexample rationals2.sml 1+2*x=0"; + +(*---------------------------------*) +"-------------- is_rootequ_in - SubProblem -------------------------"; +"-------------- is_rootequ_in - SubProblem -------------------------"; +"-------------- is_rootequ_in - SubProblem -------------------------"; +val fmz = ["equality (sqrt(x) - 1 = 0)","solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Isac.thy",["approximate","univariate","equation","test"], + ("Isac.thy","solve_univar_err")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Isac.thy","solve_univar_err"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = (me nxt p [1] pt) handle e => print_exn_G e; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +if p = ([1,1],Frm) andalso + f = Form' (FormKF (~1,EdUndef,2,Nundef,"sqrt x - 1 = 0")) andalso + nxt = ("Empty_Mstep",Empty_Mstep) (*script ist noch 'helpless'*) then () +else raise error "new behaviour in testexample rationals2.sml sqrt(x) - 1 = 0"; diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/scriptnew.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/scriptnew.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,421 @@ +(* use"../tests/scriptnew.sml"; + use"tests/scriptnew.sml"; + *) + +(*contents*) +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; +" --- test 11.5.02 Testeq: let e_ =... in [e_] ------------------ "; +" _________________ me + nxt_step from script ___________________ "; +" _________________ me + sqrt-equ-test: 1.norm_equation ________ "; +" _________________ equation with x =(-12)/5, but L ={} ------- "; +(*contents*) + + + + +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; +" --- test 30.4.02 Testterm: Repeat Repeat Or ------------------ "; +store_pbt + (prep_pbt Test.thy + (["tests"], + []:(string * string list) list, + e_rls, None, [])); +store_pbt + (prep_pbt Test.thy + (["met-testterm","tests"], + [("#Given" ,["realTestGiven g_"]), + ("#Find" ,["realTestFind f_"]) + ], + e_rls, None, [])); +methods:= overwritel (!methods, +[ prep_met (*test for simplification*) + (("Test.thy","met-testterm"):metID, + [("#Given" ,["realTestGiven g_"]), + ("#Find" ,["realTestFind f_"]) + ], + {rew_ord'="tless_true",rls'=tval_rls,srls=e_rls,prls=e_rls,calc=[], + asm_rls=[],asm_thm=[]}, + "Script Testterm (g_::real) = \ + \Repeat\ + \ ((Repeat (Rewrite rmult_1 False)) Or\ + \ (Repeat (Rewrite rmult_0 False)) Or\ + \ (Repeat (Rewrite radd_0 False))) g_" + )]); +val fmz = ["realTestGiven ((0+0)*(1*(1*a)))","realTestFind F"]; +val (dI',pI',mI') = ("Test.thy",["met-testterm","tests"], + ("Test.thy","met-testterm")); +val p = e_pos'; val c = []; +val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","met-testterm"))*) +(*----script 111 ------------------------------------------------*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*"(#0 + #0) * (#1 * (#1 * a))" nxt= Rewrite ("rmult_1",*) +(*----script 222 ------------------------------------------------*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*"(#0 + #0) * (#1 * a)" nxt= Rewrite ("rmult_1",*) +(*----script 333 ------------------------------------------------*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*"(#0 + #0) * a" nxt= Rewrite ("radd_0",*) +(*----script 444 ------------------------------------------------*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*"#0 * a"*) +(*----script 555 ------------------------------------------------*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*"#0"*) +if p=([4],Res) then () +else raise error ("new behaviour in 30.4.02 Testterm: p="^(pos'2str p)); +(*----script 666 ------------------------------------------------*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*"#0"*) +if nxt=("End_Proof'",End_Proof') then () +else raise error "new behaviour in 30.4.02 Testterm: End_Proof"; + + + + + +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; +" --- test 9.5.02 Testeq: While Try Repeat @@ ------------------ "; +store_pbt + (prep_pbt Test.thy + (["met-testeq","tests"], + [("#Given" ,["boolTestGiven e_"]), + ("#Find" ,["boolTestFind v_i_"]) + ], + e_rls, None, [])); +methods:= overwritel (!methods, +[ + prep_met + (("Test.thy","testeq1"):metID, + [("#Given",["boolTestGiven e_"]), + ("#Where" ,[]), + ("#Find" ,["boolTestFind v_i_"]) + ], + {rew_ord'="tless_true",rls'=tval_rls, + srls=append_rls "testeq1_srls" e_rls + [Calc ("Test.contains'_root", eval_contains_root"")], + prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]}, + "Script Testeq (e_::bool) = \ + \(While (contains_root e_) Do \ + \((Try (Repeat (Rewrite rroot_square_inv False))) @@ \ + \ (Try (Repeat (Rewrite square_equation_left True))) @@ \ + \ (Try (Repeat (Rewrite radd_0 False)))))\ + \ e_" + ) +]); + +val fmz = ["boolTestGiven (0+(sqrt(sqrt(sqrt a))^^^2)^^^2=0)", + "boolTestFind v_i_"]; +val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"], + ("Test.thy","testeq1")); +val Script sc = (#scr o get_met) ("Test.thy","testeq1"); +atomt sc; +val p = e_pos'; val c = []; +val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testeq1")) *) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#0 + sqrt a = #0")) +val nxt = ("Rewrite",Rewrite ("radd_0","#0 + ?k = ?k"))*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; + +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*** No such constant: "Test.contains'_root" *) + +val (p,_,f,nxt,_,pt) = me nxt p c pt; +if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"a = 0 ^^^ 2"))) andalso + nxt=("End_Proof'",End_Proof') then () +else raise error "different behaviour test 9.5.02 Testeq: While Try Repeat @@"; + + + + +" --- test 11.5.02 Testeq: let e_ =... in [e_] --------- "; +" --- test 11.5.02 Testeq: let e_ =... in [e_] --------- "; +" --- test 11.5.02 Testeq: let e_ =... in [e_] --------- "; +methods:= overwritel (!methods, +[ + prep_met + (("Test.thy","testlet"):metID, + [("#Given",["boolTestGiven e_"]), + ("#Where" ,[]), + ("#Find" ,["boolTestFind v_i_"]) + ], + {rew_ord'="tless_true",rls'=tval_rls, + srls=append_rls "testlet_srls" e_rls + [Calc ("Test.contains'_root",eval_contains_root"")], + prls=e_rls,calc=[],asm_rls=[],asm_thm=[("square_equation_left","")]}, + "Script Testeq2 (e_::bool) = \ + \(let e_ =\ + \ ((While (contains_root e_) Do \ + \ (Rewrite square_equation_left True))\ + \ e_)\ + \in [e_::bool])" + ) + ]); +val Script sc = (#scr o get_met) ("Test.thy","testlet"); +writeln(term2str sc); +val fmz = ["boolTestGiven (sqrt a = 0)", + "boolTestFind v_i_"]; +val (dI',pI',mI') = ("Test.thy",["met-testeq","tests"], + ("Test.thy","testlet")); +val p = e_pos'; val c = []; +val nxt = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me nxt p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","testlet"))*) +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +val (p,_,f,nxt,_,pt) = me nxt p c pt; +if f=(Form' (FormKF (~1,EdUndef,0,Nundef,"[a = 0 ^^^ 2]"))) andalso + nxt=("End_Proof'",End_Proof') then () +else raise error "different behaviour in test 11.5.02 Testeq: let e_ =... in [e_]"; + + + + +" _________________ me + nxt_step from script _________________ "; +" _________________ me + nxt_step from script _________________ "; +" _________________ me + nxt_step from script _________________ "; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); +writeln(term2str sc); + +val p = e_pos'; val c = []; +"--- s1 ---"; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +"--- s2 ---"; +(* val nxt = + ("Add_Given", + Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s3 ---"; +(* val nxt = ("Add_Given",Add_Given "solveFor x");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s4 ---"; +(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s5 ---"; +(* val nxt = ("Add_Find",Add_Find "solutions L");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s6 ---"; +(* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s7 ---"; +(* val nxt = + ("Specify_Problem", + Specify_Problem ["sqroot-test","univariate","equation","test"]);*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s8 ---"; +(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s9 ---"; +(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 1 ---"; +(* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 2 ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 3 ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 4 ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 5 ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 6 ---"; +(* val nxt = ("Rewrite",Rewrite ("square_equation_left",""));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 7 ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 8<> ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 9<> ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 10<> ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 11<> ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 12<> ---."; +(* val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));*) +get_form nxt p pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 13<> ---"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- 14<> ---"; +(* nxt = ("Check_Postcond",Check_Postcond ("Test.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +if f<>(Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]"))) +then raise error "scriptnew.sml 1: me + msteps from script: new behaviour" +else (); +"--- 15<> ---"; +(* val nxt = ("End_Proof'",End_Proof');*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; + +writeln (pr_ptree pr_short pt); +writeln("result: "^(get_obj g_result pt [])^ +"\n============================================================="); +(*get_obj g_asm pt []; +val it = [("#0 <= sqrt x + sqrt (#5 + x)",[1]),("#0 <= #9 + #4 * x",[1]),...*) + + + + + +" _________________ me + sqrt-equ-test: 1.norm_equation _________________ "; +" _________________ me + sqrt-equ-test: 1.norm_equation _________________ "; +" _________________ me + sqrt-equ-test: 1.norm_equation _________________ "; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); + val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); + (writeln o term2str) sc; +val p = e_pos'; val c = []; +"--- s1 ---"; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +"--- s2 ---"; +(* val nxt = ("Add_Given", + Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s3 ---"; +(* val nxt = ("Add_Given",Add_Given "solveFor x");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s4 ---"; +(* val nxt = ("Add_Given",Add_Given "errorBound (eps = #0)");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s5 ---"; +(* val nxt = ("Add_Find",Add_Find "solutions L");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s6 ---"; +(* val nxt = ("Specify_Domain",Specify_Domain "Test.thy");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s7 ---"; +(* val nxt = ("Specify_Problem", + Specify_Problem ["sqroot-test","univariate","equation","test"]);*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s8 ---"; +(* val nxt = ("Specify_Method",Specify_Method ("Test.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- s9 ---"; +(* val nxt = ("Apply_Method",Apply_Method ("Test.thy","sqrt-equ-test"));*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- !!! x1 --- 1.norm_equation"; +(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- !!! x2 --- 1.norm_equation"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*(me nxt p [1] pt) handle e => print_exn_G e;*) +"--- !!! x3 --- 1.norm_equation"; +(*val nxt = ("Empty_Mstep",Empty_Mstep) ### helpless*) +(*###*)val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc"); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- !!! x4 --- 1.norm_equation"; +(*val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +"--- !!! x5 --- 1.norm_equation"; +(* val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +if f= Form'(FormKF(~1,EdUndef,1,Nundef,"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)")) +then() else raise error "new behaviour in test-example 1.norm sqrt-equ-test"; + + +(* use"../tests/scriptnew.sml"; + *) + +" _________________ equation with x =(-12)/5, but L ={} ------- "; + +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","square_equation")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +trace_rewrite:=true; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; + +trace_rewrite:=false; + +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (_,_,_,_,ff)) = f; +if ff="[]" then () +else raise error "diff.behav. in scriptnew.sml; root-eq: L = []"; + + +val tt = (term_of o the o (parse thy)) "?xxx"; +rewrite_set_ thy true tval_rls ; diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/stdinout.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/stdinout.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,183 @@ +(* use"test-FE-KE.sml"; + W.N.16.4.00 + *) + +Compiler.Control.Print.printDepth:=4; (*4 default*) + +(*#########################################################*) +" _________________ stdin: tutor active_________________ "; +proofs:=[]; dials:=([],[],[]); +(*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*) + +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Script.thy",["sqroot-test","univariate","equation"], + ("Script.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 (*@@@@@begin !!!!!*) + (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- s2 ---"; +StdinSML 1 1 ~1 ~1 (Command Accept); +(*RuleFK (Add_Given "equality (sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x))"*) +"--- s3 ---"; +StdinSML 1 1 ~2 ~2 (Command Accept); +(*RuleFK (Add_Given "solveFor x")*) +"--- s4 ---"; +StdinSML 1 1 ~3 ~3 (Command Accept); +(*RuleFK (Add_Given "errorBound (eps = #0)")*) +"--- s5 ---"; +StdinSML 1 1 ~4 ~4 (Command Accept); +(*RuleFK (Add_Find "solutions L")*) +"--- s6 ---"; +StdinSML 1 1 ~5 ~5 (Command Accept); +(*RuleFK (Specify_Domain "Script.thy")*) +"--- s7 ---"; +StdinSML 1 1 ~6 ~6 (Command Accept); +(*RuleFK (Specify_Problem ["sqroot-test","univariate","equation"])*) +"--- s8 ---"; +StdinSML 1 1 ~7 ~7 (Command Accept); +(*RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))*) +"--- s9 ---"; +StdinSML 1 1 ~8 ~8 (Command Accept); +(*RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))*) +"--- 1 ---"; +StdinSML 1 1 ~9 ~9 (Command Accept); +(*RuleFK (Rewrite ("square_equation_left",""))*) +"--- 2 ---"; +StdinSML 1 1 ~10 ~10 (Command Accept); +(*RuleFK (Rewrite_Set "SqRoot_simplify")*) +"--- 3 ---"; +StdinSML 1 1 ~11 ~11 (Command Accept); +(*RuleFK (Rewrite_Set "rearrange_assoc")*) +"--- 4 ---"; +StdinSML 1 1 ~12 ~12 (Command Accept); +(*RuleFK (Rewrite_Set "isolate_root")*) +"--- 5 ---"; +StdinSML 1 1 ~13 ~13 (Command Accept); +(*RuleFK (Rewrite_Set "SqRoot_simplify")*) +"--- 6 ---"; +StdinSML 1 1 ~14 ~14 (Command Accept); +(*RuleFK (Rewrite ("square_equation_left",""))*) +"--- 7 ---"; +StdinSML 1 1 ~15 ~15 (Command Accept); +(*RuleFK (Rewrite_Set "SqRoot_simplify")*) +"--- 8 ---"; +StdinSML 1 1 ~16 ~16 (Command Accept); +(*RuleFK (Rewrite_Set "norm_equation")*) +"--- 9 ---"; +StdinSML 1 1 ~17 ~17 (Command Accept); +(*RuleFK (Rewrite_Set "SqRoot_simplify")*) +"--- 10 ---"; +StdinSML 1 1 ~18 ~18 (Command Accept); +(*RuleFK (Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))*) +"--- 11 ---"; +StdinSML 1 1 ~19 ~19 (Command Accept); +(*RuleFK (Rewrite_Set "SqRoot_simplify")*) +"--- 12 ---"; +val (begin,uI,pI,acI,cI,dats,eend) = +StdinSML 1 1 ~20 ~20 (Command Accept); +(*RuleFK (Check_Postcond ("Script.thy","sqrt-equ-test"))*) + +if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]")) +then raise error "do_ + msteps input: not finished correctly" +else "roo-equation, do_ + msteps input: OK"; + +"=========================================================="; +writeln (get_history 1 1); +"=========================================================="; + + + +(*#########################################################*) +" _________________ stdin: student active_________________ "; +proofs:=[]; dials:=([],[],[]); +(*dmts:= [(PutRuleRes, Tt, Skip),(PutRule, St, SkipNo)];*) + +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Script.thy",["sqroot-test","univariate","equation"], + ("Script.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,uI,pI,acI,cI,dats,_)=StdinSML 1 1 1 1 + (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- s2 ---"; +StdinSML 1 1 ~1 2 (RuleFK +(Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))")); +"--- s3 ---"; +StdinSML 1 1 ~2 3 (RuleFK (Add_Given "solveFor x")); +"--- s4 ---"; +StdinSML 1 1 ~3 4 (RuleFK (Add_Given "errorBound (eps = 0)")); +"--- s5 ---"; +StdinSML 1 1 ~4 5 (RuleFK (Add_Find "solutions L")); +"--- s6 ---"; +StdinSML 1 1 ~5 6 (RuleFK (Specify_Domain "Script.thy")); +"--- s7 ---"; +StdinSML 1 1 ~6 7 (RuleFK +(Specify_Problem ["sqroot-test","univariate","equation"])); +"--- s8 ---"; +StdinSML 1 1 ~7 8 (RuleFK (Specify_Method ("Script.thy","sqrt-equ-test"))); +"--- s9 ---"; +StdinSML 1 1 ~8 9 (RuleFK (Apply_Method ("Script.thy","sqrt-equ-test"))); +"--- 1 ---"; +StdinSML 1 1 ~9 10 (RuleFK +(Rewrite ("square_equation_left",""))); +"--- 2 ---"; +StdinSML 1 1 ~10 11 (RuleFK (Rewrite_Set "SqRoot_simplify")); +"--- 3 ---"; +StdinSML 1 1 ~11 12 (RuleFK (Rewrite_Set "rearrange_assoc")); +"--- 4 ---"; +StdinSML 1 1 ~12 13 (RuleFK (Rewrite_Set "isolate_root")); +"--- 5 ---"; +StdinSML 1 1 ~13 14 (RuleFK (Rewrite_Set "SqRoot_simplify")); +"--- 6 ---"; +StdinSML 1 1 ~14 15 (RuleFK +(Rewrite ("square_equation_left",""))); +"--- 7 ---"; +StdinSML 1 1 ~15 16 (RuleFK (Rewrite_Set "SqRoot_simplify")); +"--- 8 ---"; +StdinSML 1 1 ~16 17 (RuleFK (Rewrite_Set "norm_equation")); +"--- 9 ---"; +StdinSML 1 1 ~17 18 (RuleFK (Rewrite_Set "SqRoot_simplify")); +"--- 10 ---"; +StdinSML 1 1 ~18 19 (RuleFK +(Rewrite_Set_Inst ([("bdv","x")],"isolate_bdv"))); +"--- 11 ---"; +StdinSML 1 1 ~19 20 (RuleFK (Rewrite_Set "SqRoot_simplify")); +"--- 12 ---"; +val (begin,uI,pI,acI,cI,dats,eend) = +StdinSML 1 1 ~20 21 (RuleFK +(Check_Postcond ("Script.thy","sqrt-equ-test"))); + +if (hd dats) <> (FormKF (~21,Protect,0,"[x = 4]")) +then raise error "do_ + msteps input: not finished correctly" +else "roo-equation, do_ + msteps input: OK"; + +"=========================================================="; +writeln (get_history 1 1); +"=========================================================="; + + +(*=========27.4.01===============================================*) + proofs:= []; dials:=([],[],[]); +" _________________ exampel [x=4]: Rules 4.2.01a________________ "; +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("SqRoot.thy",["sqroot-test","univariate","equation"], + ("SqRoot.thy","squ-equ-test2")); +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); + +StdinSML uI pI ~1 ~1 (Command Accept); + +StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "norm_equation")); diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/subp-rooteq.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/subp-rooteq.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,492 @@ +(* use"tests/subp-rooteq.sml"; + use"subp-rooteq.sml"; + *) + + +"---------------- miniscript with mini-subpbl -------------"; +"---------------- solve_linear as rootpbl -----------------"; +"---------------- solve_plain_square as rootpbl -----------"; +"---------------- root-eq + subpbl: solve_linear ----------"; +"---------------- root-eq + subpbl: solve_plain_square ----"; +"---------------- root-eq + subpbl: no_met: linear ----"; +"---------------- root-eq + subpbl: no_met: square ----"; +"---------------- no_met in rootpbl -> linear --------------"; + + + + + +"---------------- miniscript with mini-subpbl -------------"; +"---------------- miniscript with mini-subpbl -------------"; +"---------------- miniscript with mini-subpbl -------------"; +val fmz = ["equality (x+1=2)", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","squ-equ-test-subpbl1")); + val Script sc = (#scr o get_met) ("Test.thy","squ-equ-test-subpbl1"); + (writeln o term2str) sc; + +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*("Specify_Problem",Specify_Problem ["sqroot-test","univariate","equation"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*("Specify_Method",Specify_Method ("Test.thy","squ-equ-test-subpbl1"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","squ-equ-test-subpbl1"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Subproblem",Subproblem ("Test.thy",[#,#,#])) : string * mstep + ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; + p; + writeln(istate2str (get_istate pt ([3],Frm))); +(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Add_Given",Add_Given "equality (-1 + x = 0)") *) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Add_Find",Add_Find "solutions x_i") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*) + + +(*-----30.9.02----------------------------------------------*) + +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*) + val Script sc = (#scr o get_met) ("Test.thy","solve_linear"); + (writeln o term2str) sc; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","eq*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; + p; + writeln(istate2str (get_istate pt ([3],Res))); + +(*val nxt = ("Check_elementwise",Check_elementwise "Assumptions")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = 1]" then () +else raise error "new behaviour in test: miniscript with mini-subpbl"; + + +"---------------- solve_linear as rootpbl -----------------"; +"---------------- solve_linear as rootpbl -----------------"; +"---------------- solve_linear as rootpbl -----------------"; +val fmz = ["equality (1+-1*2+x=0)", + "solveFor x","solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["linear","univariate","equation","test"], + ("Test.thy","solve_linear")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +(*val nxt = ("Add_Given",Add_Given "equality (x + #1 + #-1 * #2 = #0)")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Add_Given",Add_Given "solveFor x") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Add_Find",Add_Find "solutions L") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Problem",Specify_Problem ["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Method",Specify_Method ("Test.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"#1 + #-1 * #2 + x = #0")) + val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"isolate_bdv"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #0 + #-1 * (#1 + #-1 * #2)")) + val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify") : string * mstep*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val f = Form' (FormKF (~1,EdUndef,1,Nundef,"x = #1")) : mout val nxt = ("Check_Postcond",Check_Postcond ["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = #1]")) : mout + val nxt = ("End_Proof'",End_Proof') : string * mstep*) +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = 1]" then () +else raise error "new behaviour in test: solve_linear as rootpbl"; + + +"---------------- solve_plain_square as rootpbl -----------"; +"---------------- solve_plain_square as rootpbl -----------"; +"---------------- solve_plain_square as rootpbl -----------"; +val fmz = ["equality (9 + -1 * x ^^^ 2 = 0)","solveFor x", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["plain_square","univariate","equation","test"], + ("Test.thy","solve_plain_square")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; + +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if snd nxt=End_Proof' andalso res="[x = -3, x = 3]" then () +else raise error "new behaviour in test: solve_plain_square as rootpbl"; + + + + +"---------------- root-eq + subpbl: solve_linear ----------"; +"---------------- root-eq + subpbl: solve_linear ----------"; +"---------------- root-eq + subpbl: solve_linear ----------"; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","square_equation1")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" +square_equation_left*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2" +Test_simplify*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))" +rearrange_assoc*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)" +isolate_root*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) / (-1 * 2)" +Test_simplify*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"-4 + x = 0" + val nxt =("Subproblem",Subproblem ("Test.thy",["linear","univariate"...*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt =("Model_Problem",Model_Problem ["linear","univariate"...*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*("Specify_Problem",Specify_Problem ["linear","univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x = 0 + -1 * -4", nxt Test_simplify*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x = 4", nxt Check_Postcond ["linear","univariate","equation","test"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"[x = 4]", nxt Check_elementwise "Assumptions"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = 4]" then () +else raise error "new behaviour in test: root-eq + subpbl: solve_linear"; + + + +"---------------- root-eq + subpbl: solve_plain_square ----"; +"---------------- root-eq + subpbl: solve_plain_square ----"; +"---------------- root-eq + subpbl: solve_plain_square ----"; +val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["sqroot-test","univariate","equation","test"], + ("Test.thy","square_equation2")); +val Script sc = (#scr o get_met) ("Test.thy","square_equation2"); +(writeln o term2str) sc; + +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*) +val (p,_,f,nxt,_,pt) = + +me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"9 + -1 * x ^^^ 2 = 0" + Subproblem ("Test.thy",["plain_square","univariate","equation"]))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*Model_Problem ["plain_square","univariate","equation"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*Apply_Method ("Test.thy","solve_plain_square")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"9 + -1 * x ^^^ 2 = 0", nxt Rewrite_Set "isolate_bdv"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x ^^^ 2 = (0 + -1 * 9) / -1", nxt Rewrite_Set "Test_simplify"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x ^^^ 2 = 9", nxt Rewrite ("square_equality"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x = sqrt 9 | x = -1 * sqrt 9", nxt Rewrite_Set "tval_rls"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"x = -3 | x = 3", nxt Or_to_List*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"[x = -3, x = 3]", + nxt Check_Postcond ["plain_square","univariate","equation","test"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; + + + +(*"[x = -3, x = 3]", nxt Check_elementwise "Assumptions"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"[]", nxt Check_Postcond ["sqroot-test","univariate","equation","test"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then () +else raise error "new behaviour in test: root-eq + subpbl: solve_plain_square"; + + +writeln (pr_ptree pr_short pt); + + + +val Script s = (#scr o get_met) ("Test.thy","square_equation"); +atomt s; + + + + +"---------------- root-eq + subpbl: no_met: linear ----"; +"---------------- root-eq + subpbl: no_met: linear ----"; +"---------------- root-eq + subpbl: no_met: linear ----"; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","square_equation")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*"-4 + x = 0", nxt Subproblem ("Test.thy",["univariate","equation"]))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt =("Model_Problem",Model_Problem ["linear","univar...*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Problem",Specify_Problem ["linear","univariate","equ*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*Apply_Method ("Test.thy","norm_univar_equation")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +if p = ([13],Res) then () +else raise error ("new behaviour in test: \ + \root-eq + subpbl: solve_linear, p ="^(pos'2str p)); +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = 4]" then () +else raise error "new behaviour in test: root-eq + subpbl: solve_plain_square"; + + + + +"---------------- root-eq + subpbl: no_met: square ----"; +"---------------- root-eq + subpbl: no_met: square ----"; +"---------------- root-eq + subpbl: no_met: square ----"; +val fmz = ["equality (sqrt(5+x)+sqrt(5-x)=sqrt 18)", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","square_equation")); + val Script sc = (#scr o get_met) ("Test.thy","square_equation"); + (writeln o term2str) sc; + +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","square_equation1"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*Subproblem ("Test.thy",["univariate","equation"]))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*Model_Problem ["plain_square","univariate","equation"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Specify_Domain",Specify_Domain "Test.thy")*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Check_Postcond",Check_Postcond ["squareroot","univariate","equ*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val Form' (FormKF (~1,EdUndef,0,Nundef,res)) = f; +if (snd nxt)=End_Proof' andalso res="[x = -3, x = 3]" then () +else raise error "new behaviour in test: root-eq + subpbl: no_met: square"; + + + +"---------------- no_met in rootpbl -> linear --------------"; +"---------------- no_met in rootpbl -> linear --------------"; +"---------------- no_met in rootpbl -> linear --------------"; +val fmz = ["equality (1+2*x+3=4*x- 6)", + "solveFor x","solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["univariate","equation","test"], + ("Test.thy","no_met")); +val p = e_pos'; val c = []; +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI'))); +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree; +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Model_Problem",Model_Problem ["normalize","univariate","equati*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","norm_univar_equation"*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Subproblem",Subproblem ("Test.thy",["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Model_Problem",Model_Problem ["linear","univariate","equation"]*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Apply_Method",Apply_Method ("Test.thy","solve_linear"))*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Check_Postcond",Check_Postcond ["linear","univariate","equatio*) +val (p,_,f,nxt,_,pt) = me nxt p [1] pt; +(*val nxt = ("Check_Postcond",Check_Postcond ["normalize","univariate","equa*) +val (p,_,Form' (FormKF (_,_,_,_,f)),nxt,_,_) = + me nxt p [1] pt; +if f="[x = 5]" andalso nxt=("End_Proof'",End_Proof') then () +else raise error "new behaviour in test: no_met in rootpbl -> linear ---"; + diff -r 53c9925d2d9c -r 90390fecbe74 src/sml/systest/testdaten.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sml/systest/testdaten.sml Thu Apr 17 18:01:03 2003 +0200 @@ -0,0 +1,400 @@ +(* testdaten f"ur isac demo0 + WN 31.10.00, .., 18.1.01 + use"tests/testdaten.sml"; + use"testdaten.sml"; + + proofs:= []; dials:=([],[],[]); + *) +" _________________ exampel [x=4]: Rules 4.2.01a________________ "; +" _________________ exampel [x=4]: Rules 4.2.01b________________ "; +" _________________ exampel [x=4]: tutor active ________________ "; +" _________________ exampel [x=4] ________________ "; +" _________________ exampel [x =(-12)/5] ________________ "; +" _________________ exampel [x =(-12)/5] Auto ________________ "; +" ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- "; +" ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- "; +" ----------------- Schalk III S.62 Nr. 51a) --------- "; +" ----------------- Schalk III S.144 Nr. 408b) --------- "; +" ----------------- Schalk III S.137 Nr. 359g) --------- "; + + + + + +" _________________ exampel [x=4]: Rules 4.2.01a________________ "; +" _________________ exampel [x=4]: Rules 4.2.01a________________ "; +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- 0 ---"; +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- 1 ---"; +StdinSML uI pI ~1 ~1 (Command Accept); +(* square_equation_left +"#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*) +"--- 2 ---"; +StdinSML uI pI ~2 ~2 (Command Rules); +"--- 3 ---"; +StdinSML uI pI ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify")); +"--- 4 ---"; +val (_,_,_,_,_,[Error_ _ (*"Error_ Test_simplify not applicable to ..*), + Request "apply a rule !"],_) = +StdinSML uI pI ~3 ~3 (RuleFK (Rewrite_Set "Test_simplify")); + + +" _________________ exampel [x=4]: Rules 4.2.01b________________ "; +" _________________ exampel [x=4]: Rules 4.2.01b________________ "; +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- 0 ---"; +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- 1 ---"; +StdinSML uI pI ~1 ~1 (Command Accept); +(* square_equation_left +"#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*) +"--- 2 ---"; +StdinSML uI pI ~2 ~2 (Command Rules); +"--- 3 ---"; +val (_,_,_,_,_, + [Error_ _ (*"Error_ 'square_equation_left' not applicable to: #9 *), + Select _, Request "select a rule !"],_) = +StdinSML uI pI ~2 ~2 (RuleFK (Rewrite ("square_equation_left",""))); + + +" _________________ exampel [x=4]: tutor active ________________ "; +" _________________ exampel [x=4]: tutor active ________________ "; +val (_,uI,0,0,[],[New_User],_) = StdinSML 0 0 0 0 New_User; +val (_,_,pI,0,[],[New_Proof],_) = StdinSML uI 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +StdinSML uI pI 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +"--- 1 ---"; +StdinSML uI pI ~1 ~1 (Command Accept); +(* square_equation_left +"#9 + #4 * x = (sqrt x + sqrt (#5 + x)) ^^^ #2"*) +"--- 2 ---"; +StdinSML uI pI ~2 ~2 (Command Accept); +(* Test_simplify +"#9 + #4 * x = #5 + (#2 * x + #2 * sqrt (x ^^^ #2 + #5 * x))"*) +"--- 3 ---"; +StdinSML uI pI ~3 ~3 (Command Accept); +(* rearrange_assoc +"#9 + #4 * x = #5 + #2 * x + #2 * sqrt (x ^^^ #2 + #5 * x)"*) +"--- 4 ---"; +StdinSML uI pI ~4 ~4 (Command Accept); +(* isolate_root +"sqrt (x ^^^ #2 + #5 * x) = (#5 + #2 * x + #-1 * (#9 + #4 * x)) // (#-1 *#2)"*) +"--- 5 ---"; +StdinSML uI pI ~5 ~5 (Command Accept); +(* Test_simplify +"sqrt (x ^^^ #2 + #5 * x) = #2 + x"*) +"--- 6 ---"; +StdinSML uI pI ~6 ~6 (Command Accept); +(* square_equation_left +"x ^^^ #2 + #5 * x = (#2 + x) ^^^ #2"*) +"--- 7 ---"; +StdinSML uI pI ~7 ~7 (Command Accept); +(* Test_simplify +"x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*) +"--- 8 ---"; +StdinSML uI pI ~8 ~8 (Command Accept); +(* rearrange_assoc +"x ^^^ #2 + #5 * x = #4 + x ^^^ #2 + #4 * x"*) +"--- 9 ---"; +StdinSML uI pI ~9 ~9 (Command Accept); +(* Test_simplify +"x ^^^ #2 + #5 * x = #4 + (x ^^^ #2 + #4 * x)"*) +"--- 10 ---"; +StdinSML uI pI ~10 ~10 (Command Accept); +(* norm_equation +"x ^^^ #2 + #5 * x + #-1 * (#4 + (x ^^^ #2 + #4 * x)) = #0"*) +"--- 11 ---"; +StdinSML uI pI ~11 ~11 (Command Accept); +(* Test_simplify + "#-4 + x = #0"*) +"--- 12 ---"; +StdinSML uI pI ~12 ~12 (Command Accept); +(* isolate_bdv +"x = #0 + #-1 * #-4" *) +"--- 13 ---"; +StdinSML uI pI ~13 ~13 (Command Accept); +(* Test_simplify +"x = #4" *) +"--- 14 ---"; +StdinSML uI pI ~14 ~14 (Command Accept); +val (_,_,1,~14,[],[RuleKF (_,m),FormKF (_,_,_,_,f),Request "Accept ?"],_) = it; +if m = Check_Postcond ["squareroot","univariate","equation","test"] + andalso f = "[x = 4]" then () +else raise error "new behaviour in: exampel [x=4]: tutor active"; +"--- 15 ---"; +StdinSML uI pI ~15 ~15 (Command Accept); +(* Request "start another example"*) + +(*---- after restruct. kb 18.9.02 ---- (same is in test-FE...) +" _________________ exampel [x=4] ________________ "; +" _________________ exampel [x=4] ________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) = +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); + +StdinSML 1 1 ~1 ~1 (Command ActivePlus); +StdinSML 1 1 ~1 ~1 (Command ActivePlus); +StdinSML 1 1 ~1 ~1 (Command ActivePlus); +StdinSML 1 1 ~1 ~1 (Command ActivePlus);(*acti=4..SelRule*) + +"--- !!! x1 --- strange choice"; (* hier nochmals spec !*) +StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "norm_equation")); +"--- !!! x2 --- ME knows nxt_step"; +StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Set "Test_simplify")); +"--- !!! x3 --- helpless !!!"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = +StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc")); +"--- !!! x4 ---"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = +StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root")); +"--- !!! x5 --- back at original equation !!!"; +val (_,_,_,_,_,[FormKF (_,_,_,_,res),_,requ],_) = +StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify")); +if res="sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)" +then () else raise error "new behaviour in test-example"; +"--- !!! x6 --- not applicable"; +val (_,_,_,_,_,[Error_ err,_,requ],_) = +StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite_Set "Test_simplify")); +(*val (_,_,_,_,_,[RuleKF r,requ],_) =*) +val (_,_,_,_,_,ios,_) = +StdinSML 1 1 ~6 ~6 (Command YourTurn); +StdinSML 1 1 ~7 ~7 (Command Accept); +StdinSML 1 1 ~8 ~8 (Command Accept); +StdinSML 1 1 ~9 ~9 (Command Accept); +StdinSML 1 1 ~10 ~10 (Command Accept); +StdinSML 1 1 ~11 ~11 (Command Accept); +StdinSML 1 1 ~12 ~12 (Command Accept); +StdinSML 1 1 ~13 ~13 (Command Accept); +StdinSML 1 1 ~14 ~14 (Command Accept); +StdinSML 1 1 ~15 ~15 (Command Accept); +StdinSML 1 1 ~16 ~16 (Command Accept); +StdinSML 1 1 ~17 ~17 (Command Accept); +StdinSML 1 1 ~18 ~18 (Command Accept); +StdinSML 1 1 ~19 ~19 (Command Accept); +val (_,1,1,_,[],[FormKF (_,_,_,_,f),Request "Accept ?"],_) = it; +if f="[x = 4]" then () else raise error "new behaviour in test-example[x=4]"; + +val (_,1,1,~20,[],[Request "start another example",End_Proof],_) = +StdinSML 1 1 ~20 ~20 (Command Accept); +-------------------------------------------------------------------*) + + + +" _________________ exampel [x =(-12)/5] ________________ "; +" _________________ exampel [x =(-12)/5] ________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) = +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); + +StdinSML 1 1 ~1 ~1 (Command SpeedMinus); +StdinSML 1 1 ~1 ~1 (Command SpeedMinus); +StdinSML 1 1 ~1 ~1 (Command Accept);(*->rule*) +StdinSML 1 1 ~1 ~1 (Command Accept);(*->form*) +val (_,_,_,_,_,dats,_) = +StdinSML 1 1 ~2 ~2 (Command Accept);(*->rule*) +StdinSML 1 1 ~2 ~2 (Command Accept);(*->form*) + + +StdinSML 1 1 ~3 ~3 (Command ActivePlus); +StdinSML 1 1 ~3 ~3 (Command ActivePlus);(*act=2: SelRule..PutRuleRes,Tt*) +StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Set "rearrange_assoc")); +StdinSML 1 1 ~4 ~4 (Command Accept); +StdinSML 1 1 ~4 ~4 (RuleFK (Rewrite_Set "isolate_root")); +StdinSML 1 1 ~5 ~5 (Command Accept); +StdinSML 1 1 ~5 ~5 (RuleFK (Rewrite_Set "Test_simplify")); +StdinSML 1 1 ~6 ~6 (Command Accept); + + +StdinSML 1 1 ~6 ~6 (Command SpeedPlus); +StdinSML 1 1 ~6 ~6 (Command SpeedPlus);(*act=2: SelRule..SelRule*) +StdinSML 1 1 ~6 ~6 (RuleFK (Rewrite ("square_equation_left",""))); +StdinSML 1 1 ~7 ~7 (RuleFK (Rewrite_Set "Test_simplify")); +StdinSML 1 1 ~8 ~8 (RuleFK (Rewrite_Set "rearrange_assoc")); + + +StdinSML 1 1 ~9 ~9 (Command YourTurn); +StdinSML 1 1 ~10 ~10 (Command Accept); +StdinSML 1 1 ~11 ~11 (Command Accept); +StdinSML 1 1 ~12 ~12 (Command Accept); +StdinSML 1 1 ~13 ~13 (Command Accept); +StdinSML 1 1 ~14 ~14 (Command Accept); +val (_,_,_,_,_,dats,_) = +StdinSML 1 1 ~15 ~15 (Command Accept); +if dats=[Request "start another example",End_Proof] then () +else raise error "new behaviour in test-example 1: [x =(-12)/5]"; + + +" _________________ exampel [x =(-12)/5] Auto ________________ "; +" _________________ exampel [x =(-12)/5] Auto ________________ "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(-3+x))", + "solveFor x","errorBound (eps=0)", + "solutions L"]; +val (dI',pI',mI') = + ("Test.thy",["squareroot","univariate","equation","test"], + ("Test.thy","sqrt-equ-test")); +val Script sc = (#scr o get_met) ("Test.thy","sqrt-equ-test"); +writeln(term2str sc); +"--- s1 ---"; +val (_,1,1,1,[],[_,_,FormKF (_,_,_,_,f),req],_) = +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); + +val (_,_,_,_,_,dats,_) = StdinSML 1 1 ~1 ~1 (Command Auto); +val FormKF (~16,Protect,0,Nundef,res) = + (last_elem o drop_last o drop_last) dats; +if res=(*"[]"*)"[x = -12 / 5]" then () +else raise error "new behaviour in test-example 2: [x =(-12)/5]"; + + + +" ----------------- differentiate ----------------- "; +" ----------------- d_d x (x ^^^ 2 + 3 * x + 4) ----------------- "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["functionTerm (d_d x (x ^^^ 2 + 3 * x + 4))", + "differentiateFor x","derivative f_'_"]; +val (dI',pI',mI') = + ("Diff.thy",["derivative_of","function"], + ("Diff.thy","differentiate_on_R")); +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +(*FormKF (~10,Protect,0,Nundef,"#3 + #2 * x")*) +(* 25.4.01: remove Error with NotAppl + StdinSML 1 1 ~1 ~1 (RuleFK (Rewrite_Set "Test_simplify")); + StdinSML 1 1 ~2 ~2 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_sum","")))); + StdinSML 1 1 ~3 ~3 (RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const","")))); +uncaught exception TYPE ... + +val uI=1;val pI=1;val acI= ~3;val cI= ~3; +val dat=(RuleFK (Rewrite_Inst (["(bdv,x)"],("diff_const",""))));; +*) + + +(*18.4.01 tests mit speed*) + +StdinSML 1 1 ~1 ~1 (Command Accept); + +StdinSML 1 1 ~2 ~2 (Command SpeedPlus); +StdinSML 1 1 ~2 ~2 (Command Accept); + +StdinSML 1 1 ~4 ~4 (Command SpeedMinus); +StdinSML 1 1 ~4 ~4 (Command Accept); + +StdinSML 1 1 ~5 ~5 (Command Accept); +(**) +val xxx = StdinSML 1 1 ~6 ~6 (Command Auto); +if xxx = ("@@@@@begin@@@@@",1,1,~6,[], + [FormKF (~7,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * d_d x x + 0"), + FormKF (~8,Protect,1,Nundef,"2 * x ^^^ (2 - 1) + 3 * 1 + 0"), + FormKF (~9,Protect,1,Nundef,"3 + 2 * x"), + FormKF (~10,Protect,0,Nundef,"3 + 2 * x"), + Request "start another example",End_Proof],"@@@@@end@@@@@") +then () else writeln "new behaviour in example d_d x (x ^^^ 2 + 3 * x + 4), SpeedPlus/Minus"; + + +" ----------------- d_d x (x ^^^ 2 + x + 1 / x ^^^ 2) ----------------- "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["functionTerm (d_d x (x ^^^ 2 + x + 1 / x ^^^ 2))", + "differentiateFor x","derivative f_'_"]; +val (dI',pI',mI') = + ("Diff.thy",["derivative_of","function"], + ("Diff.thy","differentiate_on_R")); +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +StdinSML 1 1 ~1 ~1 (Command Auto); +(*FormKF (~12,Protect,0,Nundef,"#1 + (#2 * x + #-2 * x ^^^ #-3)")*) + +" ----------------- Schalk III S.62 Nr. 34a) --------- "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["functionTerm (d_d x ((5 * x ^^^ 2 - 2) * (7 * x + 1)))", + "differentiateFor x","derivative f_'_"]; +val (dI',pI',mI') = + ("Diff.thy",["derivative_of","function"], + ("Diff.thy","differentiate_on_R")); +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +StdinSML 1 1 ~1 ~1 (Command Auto); + + +" ----------------- Schalk III S.62 Nr. 51a) --------- "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["functionTerm (d_d x ((x+1)/(x- 1)))", + "differentiateFor x","derivative f_'_"]; +val (dI',pI',mI') = + ("Diff.thy",["derivative_of","function"], + ("Diff.thy","differentiate_on_R")); +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +StdinSML 1 1 ~1 ~1 (Command Auto); +(*"#-1 // (#1 + (x ^^^ #2 + #-2 * x)) +\n(x // (#1 + (x ^^^ #2 + #-2 * x)) +\n (#1 + x) * (#-1 // (#1 + (x ^^^ #2 + #-2 * x))))" ----- simplification !?!*) + + +" ----------------- Schalk III S.144 Nr. 408b) --------- "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["functionTerm (d_d x (x ^^^ 2 * (ln ((sin x) ^^^ 2))))", + "differentiateFor x","derivative f_'_"]; +val (dI',pI',mI') = + ("Diff.thy",["derivative_of","function"], + ("Diff.thy","differentiate_on_R")); +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +StdinSML 1 1 ~1 ~1 (Command Auto); +(*"#2 * (x * ln (sin x ^^^ #2)) +\ncos x * (sin x * (x ^^^ #2 * (#2 // sin x ^^^ #2)))"---- cancel sin x !!!*) + + +" ----------------- Schalk III S.137 Nr. 359g) --------- "; +proofs:= []; dials:=([],[],[]); +StdinSML 0 0 0 0 New_User; +StdinSML 1 0 0 0 New_Proof; +val fmz = ["functionTerm (d_d x (sqrt (cos (3*x))))", + "differentiateFor x","derivative f_'_"]; +val (dI',pI',mI') = + ("Diff.thy",["derivative_of","function"], + ("Diff.thy","differentiate_on_R")); +StdinSML 1 1 1 1 (RuleFK (Init_Proof (fmz,(dI',pI',mI')))); +StdinSML 1 1 ~1 ~1 (Command Auto);