walther@60330: (* 
walther@60330:    
neuper@37906: 
neuper@37906:    method "sqrt-equ-test", _NOT_ "square-equation" 
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: (*
walther@60340: > val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";
walther@59686: > val eval_fn = the (LibraryC.assoc (!eval_list, "pow"));
neuper@37926: > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
walther@60360: > Syntax.string_of_term (Proof_Context.init_global 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)";
walther@59997: val thm = ("square_equation_left", "");
neuper@37926: val SOME (ct,asm) = rewrite thy' "tless_true" "tval_rls" true thm ct;
walther@60242: (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) \<up> 2"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: (*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x \<up> 2 + -3 * x))"*)
neuper@37906: val rls = ("rearrange_assoc");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: (*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x \<up> 2 + -3 * x)"*)
neuper@37906: val rls = ("isolate_root"); 
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: (*"sqrt (x \<up> 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);
walther@60242: (*"sqrt (x \<up> 2 + -3 * x) = 6 + x"*)
walther@59997: 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';
walther@60242: (*"x \<up> 2 + -3 * x = (6 + x) \<up> 2"*)
neuper@37906: val rls = ("Test_simplify");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: (*"x \<up> 2 + -3 * x = 36 + (x \<up> 2 + 12 * x)"*)
neuper@37906: val rls = ("norm_equation");
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: (*"x \<up> 2 + -3 * x + -1 * (36 + (x \<up> 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 
walther@59997: 		  [("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: (* 
walther@59865: val ct = "x = (-12) / 5" : TermC.as_string
neuper@37906: > asm;
neuper@37906: val it =
walther@59997:   ["(+0) <= sqrt x  + sqrt ((-3) + x) ", "(+0) <= 9 + 4 * x",
walther@60242:    "(+0) <= (-3) * x + x \<up> 2", "(+0) <= 6 + x"] : TermC.as_string 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))",
walther@59997: 	   "bound_variable x", "error_bound 0"(*,
neuper@37906: 	   "solutions L::real set" ,
neuper@37906: 	  "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < eps}"*)];
wneuper@59592: val thy = (theory "Isac_Knowledge");
walther@60230: val formals = map (the o (TermC.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}"*)];
walther@60230: val chkpbl = map (the o (TermC.parse thy)) (given @ where_ @ find @ with_);
walther@60230: val givens = map (the o (TermC.parse thy)) given;
neuper@37906: parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
neuper@37906: 
neuper@37906: " --- subproblem 2: linear-equation --- ";
walther@59997: val origin = ["x + 4 = (0::real)", "x::real"];
walther@60230: val formals = map (the o (TermC.parse thy)) origin;
neuper@37906: 
neuper@37906: val given  = ["equation (l=(0::real))",
neuper@37906: 	     "bound_variable bdv"];
walther@60387: val where_ = ["l is_linear_in bdv", "bdv is_atom"];
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_);
walther@60230: val givens = map (the o (TermC.parse thy)) given;
neuper@37906: 
neuper@37906: 
neuper@37906: " _________________ rewrite_ x+4_________________ ";
neuper@37906: " _________________ rewrite_ x+4_________________ ";
neuper@37906: " _________________ rewrite_ x+4_________________ ";
walther@60340: val t = (Thm.term_of o the o (TermC.parse thy)) "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
walther@59871: val thm = ThmC.numerals_to_Free @{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: (*
walther@60242: sqrt (x \<up> 2 + 5 * x) =
neuper@37906: (5 + 2 * x + (-1 * 9 + -1 * (4 * x))) / (-1 * 2)
neuper@37906: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
neuper@37906: ### trying thm 'rdistr_div_right'
walther@60242: ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
neuper@37906: (5 + 2 * x) / (-1 * 2) + (-1 * 9 + -1 * (4 * x)) / (-1 * 2)
walther@60242: ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
neuper@37906: (5 + 2 * x) / (-1 * 2) + (-1 * 9 / (-1 * 2) + -1 * (4 * x) / (-1 * 2))
walther@60242: ### rewrites to: sqrt (x \<up> 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'
walther@60242: ### rewrites to: sqrt (x \<up> 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'
walther@60242: ### rewrites to: sqrt (x \<up> 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'
walther@60242: ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
neuper@37906: -1 * 9 / (-1 * 2) + (5 / (-1 * 2) + (2 * x + -1 * (4 * x)) / (-1 * 2))
walther@60242: ### rewrites to: sqrt (x \<up> 2 + 5 * x) =
neuper@37906: -1 * 9 / (-1 * 2) + (5 + (2 * x + -1 * (4 * x))) / (-1 * 2)
walther@60242: ### rewrites to: sqrt (x \<up> 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: *)
walther@59871: val thm = ThmC.numerals_to_Free @{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;
Walther@60565: val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "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);
walther@59868: val t' = UnparseC.term 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: (*
walther@59871: rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;
Walther@60650: TermC.atom_trace_detail @{context} (Thm.prop_of (!tthm));
Walther@60650: TermC.atom_trace_detail @{context} (Thm.term_of (!tct));
neuper@37906: *)
neuper@38058: val thy' = "Test";
neuper@37906: val ct = "sqrt(9+4*x)=sqrt x + sqrt(5+x)";
walther@59997: (*1*)val thm = ("square_equation_left", "");
neuper@37906: val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
walther@60242: "9 + 4 * x = (sqrt x + sqrt (5 + x)) \<up> 2";
neuper@37906: (*2*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: "9 + 4 * x = 5 + (2 * x + 2 * sqrt (x \<up> 2 + 5 * x))";
neuper@37906: (*3*)val rls = "rearrange_assoc";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: "9 + 4 * x = 5 + 2 * x + 2 * sqrt (x \<up> 2 + 5 * x)";
neuper@37906: (*4*)val rls = "isolate_root";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: "sqrt (x \<up> 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);
walther@60242: "sqrt (x \<up> 2 + 5 * x) = 2 + x";
walther@59997: (*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';
walther@60242: "x \<up> 2 + 5 * x = (2 + x) \<up> 2";
neuper@37906: (*7*)val rls = "Test_simplify";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: "x \<up> 2 + 5 * x = 4 + (x \<up> 2 + 4 * x)";
neuper@37906: (*8*)val rls = "norm_equation";
neuper@37906: val (ct,_) = the (rewrite_set thy' false rls ct);
walther@60242: "x \<up> 2 + 5 * x + -1 * (4 + (x \<up> 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 
walther@59997: 		  [("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";
Walther@60565: val ct = TermC.parse_test @{context}"sqrt(9+4*x)=sqrt x + sqrt(5+x)";
walther@59997: val ctl = ["sqrt(9+4*x)=sqrt x + sqrt(5+x)", "x::real", "0"];
Walther@60469: val oris = O_Model.init thy ctl 
Walther@60586: 		    ((#model o Problem.from_store)
walther@59997: 			 ["sqroot-test", "univariate", "equation", "test"]);
walther@59846: val loc = Istate.empty;
wneuper@59279: val (pt,pos) = (e_ctree,[]);
walther@59941: val (pt,_) = cappend_problem pt pos loc Formalise.empty (oris,empty_spec,TermC.empty, ContextC.empty)
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",
walther@59997: 			      "equations", "univariate", "square-root"];
walther@59997: 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 [];
Walther@60428: val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec
neuper@37906: > val pt = update_domID  pt [] "RatArith";
neuper@37906: > get_obj g_spec pt [];
Walther@60428: val it = ("RatArith",Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec
neuper@37906: > val pt = update_pblID  pt [] ["RatArith",
walther@59997: 			      "equations", "univariate", "square-root"];
neuper@37906: > get_obj g_spec pt [];
walther@59997: ("RatArith",["RatArith", "equations", "univariate", "square-root"],
Walther@60428:    (ThyC.id_empty, MethodC.id_empty)) : spec
walther@59997: > val pt = update_metID  pt [] ("RatArith", "sqrt-equ-test");
neuper@37906: > get_obj g_spec pt [];
walther@59997:   ("RatArith",["RatArith", "equations", "univariate", "square-root"],
walther@59997:    ("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;
walther@59997: val thm = ("square_equation_left", ""); val ctold = ct;
walther@59868: val (ct,asm) = the (rewrite thy' "tless_true" ("tval_rls") true thm (UnparseC.term ct));
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac (fst thm)) (TermC.parse_test @{context} ct,[])Complete;
neuper@37906: (*val pt = union_asm pt [] (map (rpair []) asm);*)
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("rearrange_assoc"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("isolate_root"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val thm = ("square_equation_left", ""); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,asm) = the (rewrite thy' "tless_true" "tval_rls" true thm ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: (*val pt = union_asm pt [] (map (rpair []) asm);*)
neuper@37906: 
neuper@37906: val pos = lev_up pos;
Walther@60565: val (pt,_) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("norm_equation"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: (* --- see comments in interface_ME_ISA/instantiate''
walther@59997: 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;
Walther@60565: val rls = ("isolate_bdv"); val ctold = TermC.parse_test @{context} ct;
neuper@37906: val (ct,_) = the (rewrite_set_inst thy'  false 
walther@59997: 		  [("bdv", "x")] rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_on pos;
Walther@60565: val rls = ("Test_simplify"); val ctold = TermC.parse_test @{context} ct;  
neuper@37906: val (ct,_) = the (rewrite_set thy'  false rls ct);
Walther@60565: val (pt,_) = cappend_atomic pt pos loc ctold (Tac rls) (TermC.parse_test @{context} ct,[]) Complete;
neuper@37906: 
neuper@37906: val pos = lev_up pos;
Walther@60565: val (pt,pos) = append_result pt pos Istate.empty (TermC.parse_test @{context} ct,[]) Complete;
walther@59844: Ctree.get_assumptions pt ([],Res);
neuper@37906: 
Walther@60608: writeln (pr_ctree ctxt 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)
walther@60242: 1.2.   9 + 4 * x = (sqrt x  + sqrt (5 + x) ) \<up> 2
walther@60242: 1.3.   9 + 4 * x = 5 + ((+2) * x + (+2) * sqrt (5 * x + x \<up> 2) )
walther@60242: 1.4.   9 + 4 * x = 5 + (+2) * x + (+2) * sqrt (5 * x + x \<up> 2) 
walther@60242: 1.5.   sqrt (5 * x + x \<up> 2)  = (5 + (+2) * x + (-1) * (9 + 4 * x)) / ((-1) * (+2))
walther@60242: 1.6.   sqrt (5 * x + x \<up> 2)  = (+2) + x
walther@60242: 2.   5 * x + x \<up> 2 = ((+2) + x) \<up> 2
walther@60242: 3.   5 * x + x \<up> 2 = 4 + (4 * x + x \<up> 2)     ###12.12.99: indent 2.1. !?!
walther@60242: 4.   5 * x + x \<up> 2 + (-1) * (4 + (4 * x + x \<up> 2)) = (+0)
neuper@37906: 5.   (-4) + x = (+0)
neuper@37906: 6.   x = (+0) + (-1) * (-4)
neuper@37906: *)
neuper@37906: 
neuper@37906: (*
walther@60340: val t = (Thm.term_of o the o (TermC.parse thy)) "solutions (L::real set)";
Walther@60650: TermC.atom_trace_detail @{context} t;
neuper@37906: *)
neuper@37906: 
neuper@37906: 
Walther@60586: (*- 20.9.02: Free_Solve would need the asm_rls (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))",
walther@59997: 	   "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') =
walther@59997:   ("Test",["sqroot-test", "univariate", "equation", "test"],
walther@59997:    ("Test", "sqrt-equ-test"));
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
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;
Walther@60458: (* val nxt = ("Specify_Theory",Specify_Theory "Diff_Appl");
neuper@37906: > get_obj g_spec pt (fst p);
Walther@60428: val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : 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;
Walther@60458: (*val nxt = ("Specify_Method",Specify_Method ("Diff_Appl", "sqrt-equ-test"));*)
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
Walther@60458: (*val nxt = ("Apply_Method",Apply_Method ("Diff_Appl", "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 ---";
walther@59997: get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
walther@59997: 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 ---";
walther@59997: get_form ("Rewrite_Asm",Rewrite_Asm ("square_equation_left", "")) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
walther@59997: 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 ---.";
wneuper@59497: get_form ("Rewrite_Set_Inst",Rewrite_Set_Inst (["(''bdv'',x)"],"isolate_bdv")) p pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
wneuper@59497: 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.: ---
walther@59997: get_form ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) pt;
neuper@37906: val (p,_,f,nxt,_,pt)=
walther@59997: me ("Check_Postcond",Check_Postcond ("Test", "solve-root-equation")) (p,Met) [17] pt;
neuper@37906: --- *) 
Walther@60608: writeln (pr_ctree ctxt 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))",
walther@59997: 	   "solveFor x", "errorBound (eps=0)",
neuper@37906: 	   "solutions L"];
neuper@37906: val (dI',pI',mI') =
walther@59997:   ("Test",["sqroot-test", "univariate", "equation", "test"],
walther@59997:    ["Test", "sqrt-equ-test"]);
neuper@37906: "--- s1 ---";
Walther@60571: val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];
neuper@37906: "--- s1b ---";
neuper@37906: val nxt = ("Model_Problem",
walther@59997: 	   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",
walther@59997: Specify_Problem ["sqroot-test", "univariate", "equation", "test"]);
neuper@37906: val (p,_,f,nxt,_,pt) = me nxt p c pt;
neuper@37906: "--- s8 ---";
walther@59997: 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 ---";
walther@59997: 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 ---";
walther@59997: 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
Walther@60565:  val t = TermC.parse_test @{context} "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";
neuper@37926:  val SOME (t',asm) = rewrite_set_ thy false rls t;
walther@59868:  UnparseC.term t';
walther@60330:  Rewrite.trace_on:=false; (*true false*)
neuper@37906: *)
neuper@37906: 
neuper@37906: (*me------------
neuper@37906:  val (mI,m) = nxt; val pos' as (p,p_) = p; 
neuper@37906: 
walther@59922:  val Applicable.Yes m = Step.check m (pt, (p,p_)); 
neuper@37906: (*solve*)
neuper@37906:       val pp = par_pblobj pt p;
neuper@37906:       val metID = get_obj g_metID pt pp;
Walther@60586:       val sc = (#program o MethodC.from_store ctxt) metID;
walther@59807:       val is = get_istate_LI pt (p,p_);
neuper@37906:       val thy' = get_obj g_domID pt pp;
walther@59881:       val thy = ThyC.get_theory thy';
walther@59852:       val d = Rule_Set.empty;
neuper@37906:     val Steps [(m',f',pt',p',c',s')] = 
wneuper@59559: 	     locate_input_tactic thy' m  (pt,(p,p_)) (sc,d) is;
walther@59807:          val is' = get_istate_LI pt' p';
walther@59791: 	 LI.find_next_step thy' sc (pt'(*'*),p') is' (*as (ist, ctxt) ---> ist ctxt*);  
neuper@37906: 
neuper@37906: 
neuper@37906: 
neuper@37906: 
walther@60230: val ttt = (Thm.term_of o the o (TermC.parse Test.thy))
neuper@37981: "Let (((While contains_root e_e Do\
walther@59637: \Rewrite square_equation_left #>\
walther@59637: \Try (Rewrite_Set Test_simplify) #>\
walther@59637: \Try (Rewrite_Set rearrange_assoc) #>\
walther@59637: \Try (Rewrite_Set Test_simplify)) #>\
walther@59637: \Try (Rewrite_Set norm_equation) #>\
walther@59637: \Try (Rewrite_Set Test_simplify) #>\
walther@59637: \Rewrite_Set_Inst [(''bdv'', v_v)] isolate_bdv #>\
walther@59635: \Try (Rewrite_Set Test_simplify))\
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 ---";
walther@59997: 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<> ---";
wneuper@59497: 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<> ---";
walther@59997: 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');*)
walther@59959: if f <> (Form' (Test_Out.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: 
Walther@60608: writeln (pr_ctree ctxt pr_short pt);
walther@59868: writeln("result: "^((UnparseC.term o fst o (get_obj g_result pt)) [])^
neuper@37906: "\n==============================================================");
neuper@37906: