(* 

   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 (TermC.parse thy)) "#2 \<up> #3";

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

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

> Syntax.string_of_term (Proof_Context.init_global 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)) \<up> 2"*)

val rls = ("Test_simplify");

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

(*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x \<up> 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 \<up> 2 + -3 * x)"*)

val rls = ("isolate_root"); 

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

(*"sqrt (x \<up> 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 \<up> 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 \<up> 2 + -3 * x = (6 + x) \<up> 2"*)

val rls = ("Test_simplify");

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

(*"x \<up> 2 + -3 * x = 36 + (x \<up> 2 + 12 * x)"*)

val rls = ("norm_equation");

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

(*"x \<up> 2 + -3 * x + -1 * (36 + (x \<up> 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" : TermC.as_string

> asm;

val it =

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

   "(+0) <= (-3) * x + x \<up> 2", "(+0) <= 6 + x"] : TermC.as_string 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_Knowledge");

val formals = map (the o (TermC.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 (TermC.parse thy)) (given @ where_ @ find @ with_);

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

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

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

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

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

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

	     "bound_variable bdv"];

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

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 (TermC.parse thy)) given;

" _________________ rewrite_ x+4_________________ ";

" _________________ rewrite_ x+4_________________ ";

" _________________ rewrite_ x+4_________________ ";

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

val thm = ThmC.numerals_to_Free @{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 \<up> 2 + 5 * x) =

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

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

### trying thm 'rdistr_div_right'

### rewrites to: sqrt (x \<up> 2 + 5 * x) =

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

### rewrites to: sqrt (x \<up> 2 + 5 * x) =

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

### rewrites to: sqrt (x \<up> 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 \<up> 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 \<up> 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 \<up> 2 + 5 * x) =

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

### rewrites to: sqrt (x \<up> 2 + 5 * x) =

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

### rewrites to: sqrt (x \<up> 2 + 5 * x) = 

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

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

28.8.02: ruleset besser zusammenstellen !!!

*)

val thm = ThmC.numerals_to_Free @{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 = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "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' = UnparseC.term 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 (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;

TermC.atom_trace_detail @{context} (Thm.prop_of (!tthm));

TermC.atom_trace_detail @{context} (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)) \<up> 2";

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

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

"9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 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 \<up> 2 + 5 * x)";

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

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

"sqrt (x \<up> 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 \<up> 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 \<up> 2 + 5 * x = (2 + x) \<up> 2";

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

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

"x \<up> 2 + 5 * x = 4 + (x \<up> 2 + 4 * x)";

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

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

"x \<up> 2 + 5 * x + -1 * (4 + (x \<up> 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 = TermC.parse_test @{context}"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 = O_Model.init thy ctl 

		    ((#model o Problem.from_store)

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

val loc = Istate.empty;

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

val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)

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 = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec

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

> get_obj g_spec pt [];

val it = ("RatArith",Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec

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

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

> get_obj g_spec pt [];

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

   (ThyC.id_empty, MethodC.id_empty)) : 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 (UnparseC.term ct));

val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.parse_test @{context} ct,[])Complete;

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

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("rearrange_assoc"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("isolate_root"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val thm = ("square_equation_left", ""); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

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

val pos = lev_up pos;

val (pt,_) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("norm_equation"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} 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 = TermC.parse_test @{context} ct;

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

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_on pos;

val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;  

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

val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;

val pos = lev_up pos;

val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;

Ctree.get_assumptions pt ([],Res);

writeln (pr_ctree ctxt 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) ) \<up> 2

1.3.   9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x \<up> 2) )

1.4.   9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x \<up> 2) 

1.5.   sqrt (5 * x + x \<up> 2)  = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))

1.6.   sqrt (5 * x + x \<up> 2)  = (+2) + x

2.   5 * x + x \<up> 2 = ((+2) + x) \<up> 2

3.   5 * x + x \<up> 2 = 4 + (4 * x + x \<up> 2)     ###12.12.99: indent 2.1. !?!

4.   5 * x + x \<up> 2 + (-1) * (4 + (4 * x + x \<up> 2)) = (+0)

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

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

*)

(*

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

TermC.atom_trace_detail @{context} t;

*)

(*- 20.9.02: Free_Solve would need the asm_rls (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,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

> get_obj g_spec pt (fst p);

val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : 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 ("Diff_Appl", "sqrt-equ-test"));*)

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

(*val nxt = ("Apply_Method",Apply_Method ("Diff_Appl", "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 ctxt 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,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(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 = TermC.parse_test @{context} "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";

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

 UnparseC.term t';

 Rewrite.trace_on:=false; (*true false*)

*)

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

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

 val Applicable.Yes m = Step.check m (pt, (p,p_)); 

(*solve*)

      val pp = par_pblobj pt p;

      val metID = get_obj g_metID pt pp;

      val sc = (#program o MethodC.from_store ctxt) metID;

      val is = get_istate_LI pt (p,p_);

      val thy' = get_obj g_domID pt pp;

      val thy = ThyC.get_theory thy';

      val d = Rule_Set.empty;

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

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

         val is' = get_istate_LI pt' p';

	 LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);  

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

"Let (((While contains_root e_e Do\

\Rewrite square_equation_left #>\

\Try (Rewrite_Set Test_simplify) #>\

\Try (Rewrite_Set rearrange_assoc) #>\

\Try (Rewrite_Set Test_simplify)) #>\

\Try (Rewrite_Set norm_equation) #>\

\Try (Rewrite_Set Test_simplify) #>\

\Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\

\Try (Rewrite_Set Test_simplify))\

\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' (Test_Out.FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))

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

else ();

writeln (pr_ctree ctxt pr_short pt);

writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^

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