(* 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 #####################";