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