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