(* use"../systest/root-equ.sml";

   use"systest/root-equ.sml";

   use"root-equ.sml";

   trace_rewrite:= true;

   trace_rewrite:= false;

   method "sqrt-equ-test", _NOT_ "square-equation" 

*)

" ================= equation with x =(-12)/5, but L ={} ======= ";

" _________________ rewrite _________________ ";

" ================= equation with result={4} ================== ";

" -------------- model, specify ------------ ";

"  ________________ rewrite _________________";

" _________________ rewrite_ x=4_________________ ";

" _________________ rewrite + cappend _________________ ";

" _________________ me Free_Solve _________________ ";

" _________________ me + tacs input _________________ ";

(*" _______________ me + nxt_step from script _________---> scriptnew.sml*)

(*" _________________ me + nxt_step from script (check_elementwise..)______ 

                     ...       L_a = Tac subproblem_equation_dummy; ";*)

(*" _______________ me + root-equ: 1.norm_equation  ___---> scriptnew.sml*)

val c = [];

(*

> val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";

> val eval_fn = the (assoc (!eval_list, "pow"));

> val (SOME (id,t')) = get_pair thy "pow" eval_fn t;

> Syntax.string_of_term (thy2ctxt thy) t';

*)

(******************************************************************)

(*                  -------------------------------------         *)

" _________________ equation with x =(-12)/5, but L ={} ------- ";

(*                  -------------------------------------         *)

" _________________ rewrite _________________ ";

val thy' = "Test";

val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";

val thm = ("square_equation_left","");

val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;

(*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)

val rls = ("Test_simplify");

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*)

val rls = ("rearrange_assoc");

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*)

val rls = ("isolate_root"); 

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"sqrt (x ^^^ 2 + -3 * x) =

(-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)

val rls = ("Test_simplify");

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)

val thm = ("square_equation_left","");

val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);

val asm = asm union asm';

(*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)

val rls = ("Test_simplify");

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*)

val rls = ("norm_equation");

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*)

val rls = ("Test_simplify");

val (ct,_) = the (rewrite_set thy' false rls ct);

(*"-36 + -15 * x = 0"*)

val rls = ("isolate_bdv");

val (ct,_) = the (rewrite_set_inst thy' false 

		  [("bdv","x::real")] rls ct);

(*"x = (0 + -1 * -36) // -15"*)

val rls = ("Test_simplify");

val (ct,_) = the (rewrite_set thy' false rls ct);

if ct<>"x = -12 / 5"then error "new behaviour in testexample"else ();

(* 

val ct = "x = (-12) / 5" : cterm'

> asm;

val it =

  ["(+0) <= sqrt x  + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",

   "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list

*)

" ================== equation with result={4} ================== ";

" ================== equation with result={4} ================== ";

" ================== equation with result={4} ================== ";

" -------------- model, specify ------------ ";

" -------------- model, specify ------------ ";

" -------------- model, specify ------------ ";

" --- subproblem 1: linear-equation --- ";

val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	   "bound_variable x","error_bound 0"(*,

	   "solutions L::real set" ,

	  "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];

val thy = (theory "Isac");

val formals = map (the o (parse thy)) origin;

val given  = ["equation (l=(r::real))",

	     "bound_variable bdv",   (* TODO type *) 

	     "error_bound eps"];

val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.yy*)

	      "bdv is_var",

	      "eps is_const_expr"];

val find   = ["solutions (L::bool list)"];

val with_  = [(* parseold ...

	  "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];

val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";

(* 31.1.00 

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;       *)

" --- subproblem 2: linear-equation --- ";

val origin = ["x + 4 = (0::real)","x::real"];

val formals = map (the o (parse thy)) origin;

val given  = ["equation (l=(0::real))",

	     "bound_variable bdv"];

val where_ = ["l is_linear_in bdv","bdv is_const"];

val find   = ["l::real"];

val with_  = ["l = (%x. l) bdv"];

val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);

val givens = map (the o (parse thy)) given;

val tag__forms = chktyps thy (formals, givens);

map ((atomty) o Thm.term_of) tag__forms;

" _________________ rewrite_ x+4_________________ ";

" _________________ rewrite_ x+4_________________ ";

" _________________ rewrite_ x+4_________________ ";

val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";

val thm = num_str @{thm square_equation_left};

val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);

val rls = Test_simplify;

val (t,_) = the (rewrite_set_ thy false rls t);

val rls = rearrange_assoc;	  

val (t,_) = the (rewrite_set_ thy false rls t);

val rls = isolate_root;		  

val (t,_) = the (rewrite_set_ thy false rls t);

val rls = Test_simplify;	  

val (t,_) = the (rewrite_set_ thy false rls t);

(*

sqrt (x ^^^ 2 + 5 * x) =

(5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

### trying thm 'rdistr_div_right'

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

(5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

(5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

5 / (-1 * 2) + 2 * x / (-1 * 2) +

(-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))

### trying thm 'radd_left_commute'

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

-1 * 9 / (-1 * 2) +

(5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))

### trying thm 'radd_assoc'

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

-1 * 9 / (-1 * 2) +

(5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))

### trying thm 'radd_real_const_eq'

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

-1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))

### rewrites to: sqrt (x ^^^ 2 + 5 * x) =

-1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)

### rewrites to: sqrt (x ^^^ 2 + 5 * x) = 

(-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

28.8.02: ruleset besser zusammenstellen !!!

*)

val thm = num_str @{thm square_equation_left};

val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);

val asm = asm union asm';

val rls = Test_simplify;

val (t,_) = the (rewrite_set_ thy false rls t);

val rls = norm_equation;	  

val (t,_) = the (rewrite_set_ thy false rls t);

val rls = Test_simplify;	  

val (t,_) = the (rewrite_set_ thy false rls t);

val rls = isolate_bdv;

val subst = [(str2term "bdv", str2term "x")];

val (t,_) = the (rewrite_set_inst_ thy false subst rls t);

val rls = Test_simplify;

val (t,_) = the (rewrite_set_ thy false rls t);

val t' = term2str t;

if t' = "x = 4" then ()

else error "root-equ.sml: new behav. in rewrite_ x+4";

" _________________ rewrite x=4_________________ ";

" _________________ rewrite x=4_________________ ";

" _________________ rewrite x=4_________________ ";

(*

rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct;

atomty ((#prop o Thm.rep_thm) (!tthm));

atomty (Thm.term_of (!tct));

*)

val thy' = "Test";

val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";

(*1*)val thm = ("square_equation_left","");

val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);

"9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";

(*2*)val rls = "Test_simplify";

val (ct,_) = the (rewrite_set thy' false rls ct);

"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";

(*3*)val rls = "rearrange_assoc";

val (ct,_) = the (rewrite_set thy' false rls ct);

"9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";

(*4*)val rls = "isolate_root";

val (ct,_) = the (rewrite_set thy' false rls ct);

"sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";

(*5*)val rls = "Test_simplify";

val (ct,_) = the (rewrite_set thy' false rls ct);

"sqrt (x ^^^ 2 + 5 * x) = 2 + x";

(*6*)val thm = ("square_equation_left","");

val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);

val asm = asm union asm';

"x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";

(*7*)val rls = "Test_simplify";

val (ct,_) = the (rewrite_set thy' false rls ct);

"x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";

(*8*)val rls = "norm_equation";

val (ct,_) = the (rewrite_set thy' false rls ct);

"x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";

(*9*)val rls = "Test_simplify";

val (ct,_) = the (rewrite_set thy' false rls ct);

"-4 + x = 0";

(*10*)val rls = "isolate_bdv";

val (ct,_) = the (rewrite_set_inst thy' false 

		  [("bdv","x")] rls ct);

"x = 0 + -1 * -4";

(*11*)val rls = "Test_simplify";

val (ct,_) = the (rewrite_set thy' false rls ct);

if ct="x = 4" then () else error "new behaviour in test-example";

" _________________ rewrite + cappend _________________ ";

" _________________ rewrite + cappend _________________ ";

" _________________ rewrite + cappend _________________ ";

val thy' = "Test";

val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";

val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];

val oris = prep_ori ctl thy 

		    ((#ppc o get_pbt)

			 ["sqroot-test","univariate","equation","test"]);

val loc = e_istate;

val (pt,pos) = (e_ctree,[]);

val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term);

val pt = update_branch pt [] TransitiveB;

(*

val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));

*)

(*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)

val pt = update_domID  pt [] "Test";

val pt = update_pblID  pt [] ["Test",

			      "equations","univariate","square-root"];

val pt = update_metID  pt [] ["Test","sqrt-equ-test"];

val pt = update_pbl    pt [] [];

val pt = update_met    pt [] [];

(*

> get_obj g_spec pt [];

val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec

> val pt = update_domID  pt [] "RatArith";

> get_obj g_spec pt [];

val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec

> val pt = update_pblID  pt [] ["RatArith",

			      "equations","univariate","square-root"];

> get_obj g_spec pt [];

("RatArith",["RatArith","equations","univariate","square-root"],

   ("e_domID","e_metID")) : spec

> val pt = update_metID  pt [] ("RatArith","sqrt-equ-test");

> get_obj g_spec pt [];

  ("RatArith",["RatArith","equations","univariate","square-root"],

   ("RatArith","sqrt-equ-test")) : spec

*)

val pos = [1]:pos;

val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;

val pos = (lev_on o lev_dn) pos;

val thm = ("square_equation_left",""); val ctold = ct;

val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (term2str ct));

val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;

(*val pt = union_asm pt [] (map (rpair []) asm);*)

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("rearrange_assoc"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("isolate_root"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val thm = ("square_equation_left",""); val ctold = str2term ct;

val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

(*val pt = union_asm pt [] (map (rpair []) asm);*)

val pos = lev_up pos;

val (pt,_) = append_result pt pos e_istate (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("norm_equation"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

(* --- see comments in interface_ME_ISA/instantiate''

val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv");

val (ct,_) = the (rewrite_set thy'  false 

		                 ("#isolate_bdv",rlsdat') ct);   *)

val pos = lev_on pos;

val rls = ("isolate_bdv"); val ctold = str2term ct;

val (ct,_) = the (rewrite_set_inst thy'  false 

		  [("bdv","x")] rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = str2term ct;  

val (ct,_) = the (rewrite_set thy'  false rls ct);

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;

val pos = lev_up pos;

val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete;

get_assumptions_ pt ([],Res);

writeln (pr_ctree pr_short pt);

(* aus src.24-11-99:

.   sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)

1.   sqrt(9+4*x)=sqrt x + sqrt(5+x)

1.1.   sqrt(9+4*x)=sqrt x + sqrt(5+x)

1.2.   9 + 4 * x = (sqrt x  + sqrt (5 + x) ) ^^^ 2

1.3.   9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )

1.4.   9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) 

1.5.   sqrt (5 * x + x ^^^ 2)  = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))

1.6.   sqrt (5 * x + x ^^^ 2)  = (+2) + x

2.   5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2

3.   5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2)     ###12.12.99: indent 2.1. !?!

4.   5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)

5.   (-4) + x = (+0)

6.   x = (+0) + (-1) * (-4)

*)

(*

val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";

atomty t;

*)

(*- 20.9.02: Free_Solve would need the erls (for conditions of rules)

    from thy ???, i.e. together with the *_simplify ?!!!? ----------

" _________________ me Free_Solve _________________ ";

" _________________ me Free_Solve _________________ ";

" _________________ me Free_Solve _________________ ";

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	   "solveFor x","errorBound (eps=0)",

	   "solutions L"(*,

      "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];

val (dI',pI',mI') =

  ("Test",["sqroot-test","univariate","equation","test"],

   ("Test","sqrt-equ-test"));

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 nxt = ("Add_Given", Add_Given "equation (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 "bound_variable x");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt = ("Add_Given",Add_Given "error_bound #0");*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt = ("Add_Find",Add_Find "solutions L"); *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");

> get_obj g_spec pt (fst p);

val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = ("Specify_Problem", Specify_Problem *)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

val nxt = ("Free_Solve",Free_Solve);

val (p,_,f,nxt,_,pt) = me nxt p [] pt;

get_obj g_spec pt [];

"--- -2 ---";

get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;

val (p,_,f,nxt,_,pt)=

me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;

(* 15.4.

"--- -1 ---";

get_form ("Begin_Trans",Begin_Trans) p pt;

val (p,_,f,nxt,_,pt)=

me ("Begin_Trans",Begin_Trans) p [4] pt; *)

"--- 1 ---";

get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt;

"--- 2 ---";

get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;

"--- 3 ---";

get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;

"--- 4 ---";

get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;

"--- 5 ---";

get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;

"--- 6 ---";

get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt;

(* 15.4.

"--- ---";

get_form ("End_Trans",End_Trans) p pt;

val (p,_,f,nxt,_,pt)=

me ("End_Trans",End_Trans) p [11] pt; *)

"--- 7 ---";

get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;

"--- 8 ---";

get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;

"--- 9 ---";

get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;

"--- 10 ---.";

get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt;

val (p,_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt;

"--- 11 ---";

get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;

val ((p,p_),_,f,nxt,_,pt)=

me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;

(* 5.4.00.: ---

get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;

val (p,_,f,nxt,_,pt)=

me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;

--- *) 

writeln (pr_ctree pr_short pt);

writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;

*)

" _________________ me + tacs input _________________ ";

" _________________ me + tacs input _________________ ";

" _________________ me + tacs input _________________ ";

val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",

	   "solveFor x","errorBound (eps=0)",

	   "solutions L"];

val (dI',pI',mI') =

  ("Test",["sqroot-test","univariate","equation","test"],

   ["Test","sqrt-equ-test"]);

"--- s1 ---";

(*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) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

"--- s1b ---";

val nxt = ("Model_Problem",

	   Model_Problem(*["sqroot-test","univariate","equation","test"]*));

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 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 c pt;

"--- s3 ---";

val nxt = ("Add_Given",Add_Given "solveFor x");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*"--- s4 ---";

val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");

val (p,_,f,nxt,_,pt) = me nxt p c pt;*)

"--- s5 ---";

val nxt = ("Add_Find",Add_Find "solutions L");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- s6 ---";

val nxt = ("Specify_Theory",Specify_Theory "Test");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- s7 ---";

val nxt = ("Specify_Problem",

Specify_Problem ["sqroot-test","univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- s8 ---";

val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- s9 ---";

val nxt = ("Apply_Method",Apply_Method ["Test","sqrt-equ-test"]);

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 1 ---";

val nxt = ("Rewrite",Rewrite ("square_equation_left",""));

val (p,_,f,nxt,_,pt) = me nxt p c pt;

(*.9.6.03

 val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";

 val SOME (t',asm) = rewrite_set_ thy false rls t;

 term2str t';

 trace_rewrite:=true; 

 trace_rewrite:=false; 

*)

(*me------------

 val (mI,m) = nxt; val pos' as (p,p_) = p; 

 val Appl m = applicable_in (p,p_) pt m; 

(*solve*)

      val pp = par_pblobj pt p;

      val metID = get_obj g_metID pt pp;

      val sc = (#scr o get_met) metID;

      val is = get_istate pt (p,p_);

      val thy' = get_obj g_domID pt pp;

      val thy = assoc_thy thy';

      val d = e_rls;

    val Steps [(m',f',pt',p',c',s')] = 

	     locate_gen thy' m  (pt,(p,p_)) (sc,d) is;

         val is' = get_istate pt' p';

	 next_tac thy' (pt'(*'*),p') sc is';  

val ttt = (Thm.term_of o the o (parse Test.thy))

"Let (((While contains_root e_e Do\

\Rewrite square_equation_left True @@\

\Try (Rewrite_Set Test_simplify False) @@\

\Try (Rewrite_Set rearrange_assoc False) @@\

\Try (Rewrite_Set Test_simplify False)) @@\

\Try (Rewrite_Set norm_equation False) @@\

\Try (Rewrite_Set Test_simplify False) @@\

\Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False @@\

\Try (Rewrite_Set Test_simplify False))\

\e_)";

-------------------------*)

"--- 2 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 3 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 4 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 5 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 6 ---";

val nxt = ("Rewrite",Rewrite ("square_equation_left",""));

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 7 ---";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 8<> ---";

val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 9<> ---";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 10<> ---";

val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 11<> ---.";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 12<> ---";

val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 13<> ---";

val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");

val (p,_,f,nxt,_,pt) = me nxt p c pt;

"--- 1<> ---";

val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]);

val (p,_,f,nxt,_,pt) = me nxt p [1] pt;

(* val nxt = ("End_Proof'",End_Proof');*)

if f <> (Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))

then error "root-equ.sml: diff.behav. in me + tacs input"

else ();

writeln (pr_ctree pr_short pt);

writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^

"\n==============================================================");