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