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