neuper@37906: (* use"../systest/root-equ.sml";
neuper@37906:    use"systest/root-equ.sml";
neuper@37906:    use"root-equ.sml";
neuper@37906:    trace_rewrite:= true;
neuper@37906:    trace_rewrite:= false;
neuper@37906: 
neuper@37906:    method "sqrt-equ-test", _NOT_ "square-equation" 
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: " ================= equation with x =(-12)/5, but L ={} ======= ";
neuper@37906: " _________________ rewrite _________________ ";
neuper@37906: 
neuper@37906: 
neuper@37906: " ================= equation with result={4} ================== ";
neuper@37906: " -------------- model, specify ------------ ";
neuper@37906: "  ________________ rewrite _________________";
neuper@37906: " _________________ rewrite_ x=4_________________ ";
neuper@37906: " _________________ rewrite + cappend _________________ ";
neuper@37906: " _________________ me Free_Solve _________________ ";
neuper@37906: " _________________ me + tacs input _________________ ";
neuper@37906: (*" _______________ me + nxt_step from script _________---> scriptnew.sml*)
neuper@37906: (*" _________________ me + nxt_step from script (check_elementwise..)______ 
neuper@37906:                      ...       L_a = Tac subproblem_equation_dummy; ";*)
neuper@37906: (*" _______________ me + root-equ: 1.norm_equation  ___---> scriptnew.sml*)
neuper@37906: 
neuper@37906: val c = [];
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: (*
wneuper@59188: > val t = (Thm.term_of o the o (parse thy)) "#2^^^#3";
neuper@37906: > val eval_fn = the (assoc (!eval_list, "pow"));
neuper@37926: > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
neuper@37934: > Syntax.string_of_term (thy2ctxt thy) t';
neuper@37906: *)
neuper@37906: (******************************************************************)
neuper@37906: (*                  -------------------------------------         *)
neuper@37906: " _________________ equation with x =(-12)/5, but L ={} ------- ";
neuper@37906: (*                  -------------------------------------         *)
neuper@37906: " _________________ rewrite _________________ ";
neuper@38058: val thy' = "Test";
neuper@37906: val ct = "sqrt(9+4*x)=sqrt x + sqrt(-3+x)";
neuper@37906: val thm = ("square_equation_left","");
neuper@37926: val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
neuper@37906: (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) ^^^ 2"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x ^^^ 2 + -3 * x))"*)
neuper@37906: val rls = ("rearrange_assoc");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x ^^^ 2 + -3 * x)"*)
neuper@37906: val rls = ("isolate_root"); 
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"sqrt (x ^^^ 2 + -3 * x) =
neuper@37906: (-3 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"sqrt (x ^^^ 2 + -3 * x) = 6 + x"*)
neuper@37906: val thm = ("square_equation_left","");
neuper@37906: val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
neuper@37906: val asm = asm union asm';
neuper@37906: (*"x ^^^ 2 + -3 * x = (6 + x) ^^^ 2"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"x ^^^ 2 + -3 * x = 36 + (x ^^^ 2 + 12 * x)"*)
neuper@37906: val rls = ("norm_equation");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"x ^^^ 2 + -3 * x + -1 * (36 + (x ^^^ 2 + 12 * x)) = 0"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: (*"-36 + -15 * x = 0"*)
neuper@37906: val rls = ("isolate_bdv");
neuper@37906: val (ct,_) = the (rewrite_set_inst thy' false 
neuper@37906: 		  [("bdv","x::real")] rls ct);
neuper@37906: (*"x = (0 + -1 * -36) // -15"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@38031: if ct<>"x = -12 / 5"then error "new behaviour in testexample"else ();
neuper@37906: 
neuper@37906: (* 
neuper@37906: val ct = "x = (-12) / 5" : cterm'
neuper@37906: > asm;
neuper@37906: val it =
neuper@37906:   ["(+0) <= sqrt x  + sqrt ((-3) + x) ","(+0) <= 9 + 4 * x",
neuper@37906:    "(+0) <= (-3) * x + x ^^^ 2","(+0) <= 6 + x"] : cterm' list
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: " ================== equation with result={4} ================== ";
neuper@37906: " ================== equation with result={4} ================== ";
neuper@37906: " ================== equation with result={4} ================== ";
neuper@37906: 
neuper@37906: " -------------- model, specify ------------ ";
neuper@37906: " -------------- model, specify ------------ ";
neuper@37906: " -------------- model, specify ------------ ";
neuper@37906: " --- subproblem 1: linear-equation --- ";
neuper@37906: val origin = ["equation (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37906: 	   "bound_variable x","error_bound 0"(*,
neuper@37906: 	   "solutions L::real set" ,
neuper@37906: 	  "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
neuper@38050: val thy = (theory "Isac");
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["equation (l=(r::real))",
neuper@37906: 	     "bound_variable bdv",   (* TODO type *) 
neuper@37906: 	     "error_bound eps"];
neuper@37906: val where_ = [(*"(l=r) is_root_equation_in bdv", 5.3.yy*)
neuper@37906: 	      "bdv is_var",
neuper@37906: 	      "eps is_const_expr"];
neuper@37906: val find   = ["solutions (L::bool list)"];
neuper@37906: val with_  = [(* parseold ...
neuper@37906: 	  "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
neuper@37906: val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
neuper@37906: (* 31.1.00 
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59188: map ((atomty) o Thm.term_of) tag__forms;       *)
neuper@37906: 
neuper@37906: " --- subproblem 2: linear-equation --- ";
neuper@37906: val origin = ["x + 4 = (0::real)","x::real"];
neuper@37906: val formals = map (the o (parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["equation (l=(0::real))",
neuper@37906: 	     "bound_variable bdv"];
neuper@37906: val where_ = ["l is_linear_in bdv","bdv is_const"];
neuper@37906: val find   = ["l::real"];
neuper@37906: val with_  = ["l = (%x. l) bdv"];
neuper@37906: val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
neuper@37906: val givens = map (the o (parse thy)) given;
neuper@37906: 
neuper@37906: val tag__forms = chktyps thy (formals, givens);
wneuper@59188: map ((atomty) o Thm.term_of) tag__forms;
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ rewrite_ x+4_________________ ";
neuper@37906: " _________________ rewrite_ x+4_________________ ";
neuper@37906: " _________________ rewrite_ x+4_________________ ";
wneuper@59188: val t = (Thm.term_of o the o (parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
neuper@37969: val thm = num_str @{thm square_equation_left};
neuper@37906: val (t,asm) = the (rewrite_ thy tless_true tval_rls true thm t);
neuper@37906: val rls = Test_simplify;
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: val rls = rearrange_assoc;	  
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: val rls = isolate_root;		  
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: 				  
neuper@37906: val rls = Test_simplify;	  
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: (*
neuper@37906: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
neuper@37906: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@37906: ### trying thm 'rdistr_div_right'
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: 5 / (-1 * 2) + 2 * x / (-1 * 2) +
neuper@37906: (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
neuper@37906: 
neuper@37906: ### trying thm 'radd_left_commute'
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: -1 * 9 / (-1 * 2) +
neuper@37906: (5 / (-1 * 2) + 2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
neuper@37906: ### trying thm 'radd_assoc'
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: -1 * 9 / (-1 * 2) +
neuper@37906: (5 / (-1 * 2) + (2 * x / (-1 * 2) + -1 * (4 * x) / (-1 * 2)))
neuper@37906: 
neuper@37906: ### trying thm 'radd_real_const_eq'
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) =
neuper@37906: -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
neuper@37906: ### rewrites to: sqrt (x ^^^ 2 + 5 * x) = 
neuper@37906: (-1 * 9 + (5 + (2 * x + -1 * (4 * x)))) / (-1 * 2)
neuper@37906: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@37906: 
neuper@37906: 28.8.02: ruleset besser zusammenstellen !!!
neuper@37906: *)
neuper@37969: val thm = num_str @{thm square_equation_left};
neuper@37906: val (t,asm') = the (rewrite_ thy tless_true tval_rls true thm t);
neuper@37906: val asm = asm union asm';
neuper@37906: val rls = Test_simplify;
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: val rls = norm_equation;	  
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: val rls = Test_simplify;	  
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: val rls = isolate_bdv;
neuper@37906: val subst = [(str2term "bdv", str2term "x")];
neuper@37906: val (t,_) = the (rewrite_set_inst_ thy false subst rls t);
neuper@37906: val rls = Test_simplify;
neuper@37906: val (t,_) = the (rewrite_set_ thy false rls t);
neuper@37906: val t' = term2str t;
neuper@37906: if t' = "x = 4" then ()
neuper@38031: else error "root-equ.sml: new behav. in rewrite_ x+4";
neuper@37906: 
neuper@37906: " _________________ rewrite x=4_________________ ";
neuper@37906: " _________________ rewrite x=4_________________ ";
neuper@37906: " _________________ rewrite x=4_________________ ";
neuper@37906: (*
neuper@37969: rewrite thy' "tless_true" "tval_rls" true (num_str @{thm rbinom_power_2}) ct;
wneuper@59188: atomty ((#prop o Thm.rep_thm) (!tthm));
wneuper@59188: atomty (Thm.term_of (!tct));
neuper@37906: *)
neuper@38058: val thy' = "Test";
neuper@37906: val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
neuper@37906: (*1*)val thm = ("square_equation_left","");
neuper@37906: val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
neuper@37906: "9 + 4 * x = (sqrt x + sqrt (5 + x)) ^^^ 2";
neuper@37906: (*2*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "9 + 4 * x = 5 + (2 * x + 2 * sqrt (x ^^^ 2 + 5 * x))";
neuper@37906: (*3*)val rls = "rearrange_assoc";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x ^^^ 2 + 5 * x)";
neuper@37906: (*4*)val rls = "isolate_root";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "sqrt (x ^^^ 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";
neuper@37906: (*5*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "sqrt (x ^^^ 2 + 5 * x) = 2 + x";
neuper@37906: (*6*)val thm = ("square_equation_left","");
neuper@37906: val (ct,asm') = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
neuper@37906: val asm = asm union asm';
neuper@37906: "x ^^^ 2 + 5 * x = (2 + x) ^^^ 2";
neuper@37906: (*7*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "x ^^^ 2 + 5 * x = 4 + (x ^^^ 2 + 4 * x)";
neuper@37906: (*8*)val rls = "norm_equation";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "x ^^^ 2 + 5 * x + -1 * (4 + (x ^^^ 2 + 4 * x)) = 0";
neuper@37906: (*9*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@37906: "-4 + x = 0";
neuper@37906: (*10*)val rls = "isolate_bdv";
neuper@37906: val (ct,_) = the (rewrite_set_inst thy' false 
neuper@37906: 		  [("bdv","x")] rls ct);
neuper@37906: "x = 0 + -1 * -4";
neuper@37906: (*11*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
neuper@38031: if ct="x = 4" then () else error "new behaviour in test-example";
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ rewrite + cappend _________________ ";
neuper@37906: " _________________ rewrite + cappend _________________ ";
neuper@37906: " _________________ rewrite + cappend _________________ ";
neuper@38058: val thy' = "Test";
neuper@37906: val ct = str2term"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
neuper@37906: val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)","x::real","0"];
neuper@37906: val oris = prep_ori ctl thy 
neuper@37906: 		    ((#ppc o get_pbt)
neuper@37906: 			 ["sqroot-test","univariate","equation","test"]);
neuper@37906: val loc = e_istate;
wneuper@59279: val (pt,pos) = (e_ctree,[]);
neuper@37906: val (pt,_) = cappend_problem pt pos loc e_fmz (oris,empty_spec,e_term);
neuper@37906: val pt = update_branch pt [] TransitiveB;
neuper@37906: (*
neuper@37906: val pt = update_model pt [] (map init_item (snd (get_obj g_origin pt [])));
neuper@37906: *)
neuper@37906: (*val pt = update_model pt [] (fst (get_obj g_origin pt [])); *)
neuper@37906: val pt = update_domID  pt [] "Test";
neuper@37906: val pt = update_pblID  pt [] ["Test",
neuper@37906: 			      "equations","univariate","square-root"];
neuper@37906: val pt = update_metID  pt [] ["Test","sqrt-equ-test"];
neuper@37906: val pt = update_pbl    pt [] [];
neuper@37906: val pt = update_met    pt [] [];
neuper@37906: (*
neuper@37906: > get_obj g_spec pt [];
neuper@37906: val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec
neuper@37906: > val pt = update_domID  pt [] "RatArith";
neuper@37906: > get_obj g_spec pt [];
neuper@37906: val it = ("RatArith",["e_pblID"],("e_domID","e_metID")) : spec
neuper@37906: > val pt = update_pblID  pt [] ["RatArith",
neuper@37906: 			      "equations","univariate","square-root"];
neuper@37906: > get_obj g_spec pt [];
neuper@37906: ("RatArith",["RatArith","equations","univariate","square-root"],
neuper@37906:    ("e_domID","e_metID")) : spec
neuper@37906: > val pt = update_metID  pt [] ("RatArith","sqrt-equ-test");
neuper@37906: > get_obj g_spec pt [];
neuper@37906:   ("RatArith",["RatArith","equations","univariate","square-root"],
neuper@37906:    ("RatArith","sqrt-equ-test")) : spec
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: val pos = [1]:pos;
neuper@37906: val (pt,_) = cappend_parent pt pos loc ct (Tac "repeat") TransitiveB;
neuper@37906: 
neuper@37906: val pos = (lev_on o lev_dn) pos;
neuper@37906: val thm = ("square_equation_left",""); val ctold = ct;
neuper@37906: val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (term2str ct));
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (str2term ct,[])Complete;
neuper@37906: (*val pt = union_asm pt [] (map (rpair []) asm);*)
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("Test_simplify"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("rearrange_assoc"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("isolate_root"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("Test_simplify"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val thm = ("square_equation_left",""); val ctold = str2term ct;
neuper@37906: val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: (*val pt = union_asm pt [] (map (rpair []) asm);*)
neuper@37906: 
neuper@37906: val pos = lev_up pos;
neuper@37906: val (pt,_) = append_result pt pos e_istate (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("Test_simplify"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("norm_equation"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("Test_simplify"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: (* --- see comments in interface_ME_ISA/instantiate''
neuper@37906: val rlsdat' = instantiate_rls' thy' [("bdv","x")] ("isolate_bdv");
neuper@37906: val (ct,_) = the (rewrite_set thy'  false 
neuper@37906: 		                 ("#isolate_bdv",rlsdat') ct);   *)
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("isolate_bdv"); val ctold = str2term ct;
neuper@37906: val (ct,_) = the (rewrite_set_inst thy'  false 
neuper@37906: 		  [("bdv","x")] rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
neuper@37906: val rls = ("Test_simplify"); val ctold = str2term ct;  
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
neuper@37906: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (str2term ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_up pos;
neuper@37906: val (pt,pos) = append_result pt pos e_istate (str2term ct,[]) Complete;
neuper@37906: get_assumptions_ pt ([],Res);
neuper@37906: 
wneuper@59279: writeln (pr_ctree pr_short pt);
neuper@37906: (* aus src.24-11-99:
neuper@37906: .   sqrt(9+4*x)=sqrt x + sqrt(5+x), x, (+0)
neuper@37906: 1.   sqrt(9+4*x)=sqrt x + sqrt(5+x)
neuper@37906: 1.1.   sqrt(9+4*x)=sqrt x + sqrt(5+x)
neuper@37906: 1.2.   9 + 4 * x = (sqrt x  + sqrt (5 + x) ) ^^^ 2
neuper@37906: 1.3.   9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) )
neuper@37906: 1.4.   9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x ^^^ 2) 
neuper@37906: 1.5.   sqrt (5 * x + x ^^^ 2)  = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
neuper@37906: 1.6.   sqrt (5 * x + x ^^^ 2)  = (+2) + x
neuper@37906: 2.   5 * x + x ^^^ 2 = ((+2) + x) ^^^ 2
neuper@37906: 3.   5 * x + x ^^^ 2 = 4 + (4 * x + x ^^^ 2)     ###12.12.99: indent 2.1. !?!
neuper@37906: 4.   5 * x + x ^^^ 2 + (-1) * (4 + (4 * x + x ^^^ 2)) = (+0)
neuper@37906: 5.   (-4) + x = (+0)
neuper@37906: 6.   x = (+0) + (-1) * (-4)
neuper@37906: *)
neuper@37906: 
neuper@37906: (*
wneuper@59188: val t = (Thm.term_of o the o (parse thy)) "solutions (L::real set)";
neuper@37906: atomty t;
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: (*- 20.9.02: Free_Solve would need the erls (for conditions of rules)
neuper@37906:     from thy ???, i.e. together with the *_simplify ?!!!? ----------
neuper@37906: " _________________ me Free_Solve _________________ ";
neuper@37906: " _________________ me Free_Solve _________________ ";
neuper@37906: " _________________ me Free_Solve _________________ ";
neuper@37906: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37906: 	   "solveFor x","errorBound (eps=0)",
neuper@37906: 	   "solutions L"(*,
neuper@37906:       "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["sqroot-test","univariate","equation","test"],
neuper@38058:    ("Test","sqrt-equ-test"));
neuper@37906: val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: 
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
neuper@37906: (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x)  = sqrt x  + sqrt (#5 + x) )");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt = ("Add_Given",Add_Given "bound_variable x");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt = ("Add_Given",Add_Given "error_bound #0");*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt = ("Add_Find",Add_Find "solutions L"); *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (* val nxt = ("Specify_Theory",Specify_Theory "DiffAppl");
neuper@37906: > get_obj g_spec pt (fst p);
neuper@37906: val it = ("e_domID",["e_pblID"],("e_domID","e_metID")) : spec*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (*val nxt = ("Specify_Problem", Specify_Problem *)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Specify_Method",Specify_Method ("DiffAppl","sqrt-equ-test"));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@38058: (*val nxt = ("Apply_Method",Apply_Method ("DiffAppl","sqrt-equ-test"));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: val nxt = ("Free_Solve",Free_Solve);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [] pt;
neuper@37906: get_obj g_spec pt [];
neuper@37906: 
neuper@37906: "--- -2 ---";
neuper@37906: get_form ("Take",Take"sqrt(9+4*x)=sqrt x + sqrt(5+x)") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Take",Take "sqrt(9+4*x)=sqrt x + sqrt(5+x)") p [3] pt;
neuper@37906: (* 15.4.
neuper@37906: "--- -1 ---";
neuper@37906: get_form ("Begin_Trans",Begin_Trans) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Begin_Trans",Begin_Trans) p [4] pt; *)
neuper@37906: 
neuper@37906: "--- 1 ---";
neuper@37906: get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [5] pt;
neuper@37906: "--- 2 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "Test_simplify")p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "Test_simplify")p [6] pt;
neuper@37906: "--- 3 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "rearrange_assoc") p [7] pt;
neuper@37906: "--- 4 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "isolate_root") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "isolate_root") p [8] pt;
neuper@37906: "--- 5 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [9] pt;
neuper@37906: "--- 6 ---";
neuper@37906: get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Asm",Rewrite_Asm ("square_equation_left","")) p [10] pt;
neuper@37906: (* 15.4.
neuper@37906: "--- ---";
neuper@37906: get_form ("End_Trans",End_Trans) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("End_Trans",End_Trans) p [11] pt; *)
neuper@37906: "--- 7 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [12] pt;
neuper@37906: "--- 8 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "norm_equation") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "norm_equation") p [13] pt;
neuper@37906: "--- 9 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [14] pt;
neuper@37906: "--- 10 ---.";
neuper@37906: get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv")) p [15] pt;
neuper@37906: "--- 11 ---";
neuper@37906: get_form ("Rewrite_Set",Rewrite_Set "Test_simplify") p pt;
neuper@37906: val ((p,p_),_,f,nxt,_,pt)=
neuper@37906: me ("Rewrite_Set",Rewrite_Set "Test_simplify") p [16] pt;
neuper@37906: (* 5.4.00.: ---
neuper@38058: get_form ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
neuper@38058: me ("Check_Postcond",Check_Postcond ("Test","solve-root-equation")) (p,Met) [17] pt;
neuper@37906: --- *) 
wneuper@59279: writeln (pr_ctree pr_short pt);
neuper@37906: writeln("result: "^(get_obj g_result pt [])^"\n==================================================================="*;
neuper@37906: *)
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ me + tacs input _________________ ";
neuper@37906: " _________________ me + tacs input _________________ ";
neuper@37906: " _________________ me + tacs input _________________ ";
neuper@37906: val fmz = ["equality (sqrt(9+4*x)=sqrt x + sqrt(5+x))",
neuper@37906: 	   "solveFor x","errorBound (eps=0)",
neuper@37906: 	   "solutions L"];
neuper@37906: val (dI',pI',mI') =
neuper@38058:   ("Test",["sqroot-test","univariate","equation","test"],
neuper@37906:    ["Test","sqrt-equ-test"]);
neuper@37906: "--- s1 ---";
neuper@37906: (*val p = e_pos'; val c = []; 
neuper@37906: val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
neuper@37906: val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)
neuper@37906: val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
neuper@37906: "--- s1b ---";
neuper@37906: val nxt = ("Model_Problem",
neuper@37906: 	   Model_Problem(*["sqroot-test","univariate","equation","test"]*));
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s2 ---";
neuper@37906: val nxt = ("Add_Given",
neuper@37906: Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s3 ---";
neuper@37906: val nxt = ("Add_Given",Add_Given "solveFor x");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: (*"--- s4 ---";
neuper@37906: val nxt = ("Add_Given",Add_Given "errorBound (eps = 0)");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;*)
neuper@37906: "--- s5 ---";
neuper@37906: val nxt = ("Add_Find",Add_Find "solutions L");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s6 ---";
neuper@38058: val nxt = ("Specify_Theory",Specify_Theory "Test");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s7 ---";
neuper@37906: val nxt = ("Specify_Problem",
neuper@37906: Specify_Problem ["sqroot-test","univariate","equation","test"]);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s8 ---";
neuper@37906: val nxt = ("Specify_Method",Specify_Method ["Test","sqrt-equ-test"]);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s9 ---";
neuper@37906: val nxt = ("Apply_Method",Apply_Method ["Test","sqrt-equ-test"]);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 1 ---";
neuper@37906: val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: 
neuper@37906: (*.9.6.03
neuper@37906:  val t = str2term "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
neuper@37926:  val SOME (t',asm) = rewrite_set_ thy false rls t;
neuper@37906:  term2str t';
neuper@37906:  trace_rewrite:=true; 
neuper@37906:  trace_rewrite:=false; 
neuper@37906: *)
neuper@37906: 
neuper@37906: (*me------------
neuper@37906:  val (mI,m) = nxt; val pos' as (p,p_) = p; 
neuper@37906: 
neuper@37906:  val Appl m = applicable_in (p,p_) pt m; 
neuper@37906: (*solve*)
neuper@37906:       val pp = par_pblobj pt p;
neuper@37906:       val metID = get_obj g_metID pt pp;
neuper@37906:       val sc = (#scr o get_met) metID;
neuper@37906:       val is = get_istate pt (p,p_);
neuper@37906:       val thy' = get_obj g_domID pt pp;
neuper@37906:       val thy = assoc_thy thy';
neuper@37906:       val d = e_rls;
neuper@37906:     val Steps [(m',f',pt',p',c',s')] = 
neuper@37906: 	     locate_gen thy' m  (pt,(p,p_)) (sc,d) is;
neuper@37906:          val is' = get_istate pt' p';
neuper@37906: 	 next_tac thy' (pt'(*'*),p') sc is';  
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
wneuper@59188: val ttt = (Thm.term_of o the o (parse Test.thy))
neuper@37981: "Let (((While contains_root e_e Do\
neuper@37906: \Rewrite square_equation_left True @@\
neuper@37906: \Try (Rewrite_Set Test_simplify False) @@\
neuper@37906: \Try (Rewrite_Set rearrange_assoc False) @@\
neuper@37906: \Try (Rewrite_Set Test_simplify False)) @@\
neuper@37906: \Try (Rewrite_Set norm_equation False) @@\
neuper@37906: \Try (Rewrite_Set Test_simplify False) @@\
neuper@37981: \Rewrite_Set_Inst [(bdv, v_v)] isolate_bdv False @@\
neuper@37906: \Try (Rewrite_Set Test_simplify False))\
neuper@37906: \e_)";
neuper@37906: 
neuper@37906: -------------------------*)
neuper@37906: 
neuper@37906: 
neuper@37906: "--- 2 ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 3 ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 4 ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "isolate_root");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 5 ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 6 ---";
neuper@37906: val nxt = ("Rewrite",Rewrite ("square_equation_left",""));
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 7 ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 8<> ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "rearrange_assoc");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 9<> ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 10<> ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "norm_equation");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 11<> ---.";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 12<> ---";
neuper@37906: val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(bdv,x)"],"isolate_bdv"));
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 13<> ---";
neuper@37906: val nxt = ("Rewrite_Set",Rewrite_Set "Test_simplify");
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- 1<> ---";
neuper@37906: val nxt = ("Check_Postcond",Check_Postcond ["sqroot-test","univariate","equation","test"]);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
neuper@37906: (* val nxt = ("End_Proof'",End_Proof');*)
neuper@37906: if f <> (Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")))
neuper@38031: then error "root-equ.sml: diff.behav. in me + tacs input"
neuper@37906: else ();
neuper@37906: 
wneuper@59279: writeln (pr_ctree pr_short pt);
neuper@37906: writeln("result: "^((term2str o fst o (get_obj g_result pt)) [])^
neuper@37906: "\n==============================================================");
neuper@37906: