wneuper/isa: test/Tools/isac/OLDTESTS/root-equ.sml@65ec9f679c3f

     1 (* trace_rewrite:= true;

     2    trace_rewrite:= false;

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

     5 *)

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

     9 " _________________ rewrite _________________ ";

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

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

    14 "  ________________ rewrite _________________";

    15 " _________________ rewrite_ x=4_________________ ";

    16 " _________________ rewrite + cappend _________________ ";

    17 " _________________ me Free_Solve _________________ ";

    18 " _________________ me + tacs input _________________ ";

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

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

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

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

    24 val c = [];

    29 (*

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

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

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

    33 > Syntax.string_of_term (thy2ctxt thy) t';

    34 *)

    35 (******************************************************************)

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

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

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

    39 " _________________ rewrite _________________ ";

    40 val thy' = "Test";

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

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

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

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

    45 val rls = ("Test_simplify");

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

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

    48 val rls = ("rearrange_assoc");

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

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

    51 val rls = ("isolate_root");

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

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

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

    55 val rls = ("Test_simplify");

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

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

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

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

    60 val asm = asm union asm';

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

    62 val rls = ("Test_simplify");

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

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

    65 val rls = ("norm_equation");

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

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

    68 val rls = ("Test_simplify");

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

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

    71 val rls = ("isolate_bdv");

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

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

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

    75 val rls = ("Test_simplify");

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

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

    79 (*

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

    81 > asm;

    82 val it =

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

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

    85 *)

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

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

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

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

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

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

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

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

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

   101 	   "solutions L::real set" ,

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

   103 val thy = (theory "Isac_Knowledge");

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

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

   107 	     "bound_variable bdv",   (* TODO type *)

   108 	     "error_bound eps"];

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

   110 	      "bdv is_var",

   111 	      "eps is_const_expr"];

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

   113 val with_  = [(* parseold ...

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

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

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

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

   118 (* 31.1.00

   119 val tag__forms = chktyps thy (formals, givens);

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

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

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

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

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

   127 	     "bound_variable bdv"];

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

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

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

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

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

   134 val tag__forms = chktyps thy (formals, givens);

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

   139 " _________________ rewrite_ x+4_________________ ";

   140 " _________________ rewrite_ x+4_________________ ";

   141 " _________________ rewrite_ x+4_________________ ";

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

   143 val thm = num_str @{thm square_equation_left};

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

   145 val rls = Test_simplify;

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

   147 val rls = rearrange_assoc;

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

   149 val rls = isolate_root;

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

   152 val rls = Test_simplify;

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

   154 (*

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

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

   157 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   158 ### trying thm 'rdistr_div_right'

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

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

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

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

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

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

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

   167 ### trying thm 'radd_left_commute'

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

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

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

   171 ### trying thm 'radd_assoc'

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

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

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

   176 ### trying thm 'radd_real_const_eq'

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

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

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

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

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

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

   183 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   185 28.8.02: ruleset besser zusammenstellen !!!

   186 *)

   187 val thm = num_str @{thm square_equation_left};

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

   189 val asm = asm union asm';

   190 val rls = Test_simplify;

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

   192 val rls = norm_equation;

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

   194 val rls = Test_simplify;

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

   196 val rls = isolate_bdv;

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

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

   199 val rls = Test_simplify;

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

   201 val t' = UnparseC.term2str t;

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

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

   205 " _________________ rewrite x=4_________________ ";

   206 " _________________ rewrite x=4_________________ ";

   207 " _________________ rewrite x=4_________________ ";

   208 (*

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

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

   211 atomty (Thm.term_of (!tct));

   212 *)

   213 val thy' = "Test";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   232 val asm = asm union asm';

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

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

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

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

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

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

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

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

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

   242 "-4 + x = 0";

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

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

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

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

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

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

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

   254 " _________________ rewrite + cappend _________________ ";

   255 " _________________ rewrite + cappend _________________ ";

   256 " _________________ rewrite + cappend _________________ ";

   257 val thy' = "Test";

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

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

   260 val oris = prep_ori ctl thy

   261 		    ((#ppc o get_pbt)

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

   263 val loc = Istate.empty;

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

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

   266 val pt = update_branch pt [] TransitiveB;

   267 (*

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

   269 *)

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

   271 val pt = update_domID  pt [] "Test";

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

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

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

   275 val pt = update_pbl    pt [] [];

   276 val pt = update_met    pt [] [];

   277 (*

   278 > get_obj g_spec pt [];

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

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

   281 > get_obj g_spec pt [];

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

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

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

   285 > get_obj g_spec pt [];

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

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

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

   289 > get_obj g_spec pt [];

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

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

   292 *)

   295 val pos = [1]:pos;

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

   298 val pos = (lev_on o lev_dn) pos;

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

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

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

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

   304 val pos = lev_on pos;

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

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

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

   309 val pos = lev_on pos;

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

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

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

   314 val pos = lev_on pos;

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

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

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

   319 val pos = lev_on pos;

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

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

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

   324 val pos = lev_on pos;

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

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

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

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

   330 val pos = lev_up pos;

   331 val (pt,_) = append_result pt pos Istate.empty (str2term ct,[]) Complete;

   333 val pos = lev_on pos;

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

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

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

   338 val pos = lev_on pos;

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

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

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

   343 val pos = lev_on pos;

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

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

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

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

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

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

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

   352 val pos = lev_on pos;

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

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

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

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

   358 val pos = lev_on pos;

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

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

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

   363 val pos = lev_up pos;

   364 val (pt,pos) = append_result pt pos Istate.empty (str2term ct,[]) Complete;

   365 Ctree.get_assumptions pt ([],Res);

   367 writeln (pr_ctree pr_short pt);

   368 (* aus src.24-11-99:

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

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

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

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

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

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

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

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

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

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

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

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

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

   382 *)

   384 (*

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

   386 atomty t;

   387 *)

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

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

   392 " _________________ me Free_Solve _________________ ";

   393 " _________________ me Free_Solve _________________ ";

   394 " _________________ me Free_Solve _________________ ";

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

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

   397 	   "solutions L"(*,

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

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

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

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

   402 val p = e_pos'; val c = [];

   403 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   405 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;

   406 (*val nxt = ("Add_Given", Add_Given "equation (sqrt (#9 + #4 * x)  = sqrt x  + sqrt (#5 + x) )");*)

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

   408 (* val nxt = ("Add_Given",Add_Given "bound_variable x");*)

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

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

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

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

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

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

   415 > get_obj g_spec pt (fst p);

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

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

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

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

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

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

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

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

   424 val nxt = ("Free_Solve",Free_Solve);

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

   426 get_obj g_spec pt [];

   428 "--- -2 ---";

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

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

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

   432 (* 15.4.

   433 "--- -1 ---";

   434 get_form ("Begin_Trans",Begin_Trans) p pt;

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

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

   438 "--- 1 ---";

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

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

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

   442 "--- 2 ---";

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

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

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

   446 "--- 3 ---";

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

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

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

   450 "--- 4 ---";

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

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

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

   454 "--- 5 ---";

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

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

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

   458 "--- 6 ---";

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

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

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

   462 (* 15.4.

   463 "--- ---";

   464 get_form ("End_Trans",End_Trans) p pt;

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

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

   467 "--- 7 ---";

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

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

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

   471 "--- 8 ---";

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

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

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

   475 "--- 9 ---";

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

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

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

   479 "--- 10 ---.";

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

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

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

   483 "--- 11 ---";

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

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

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

   487 (* 5.4.00.: ---

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

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

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

   491 --- *)

   492 writeln (pr_ctree pr_short pt);

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

   494 *)

   497 " _________________ me + tacs input _________________ ";

   498 " _________________ me + tacs input _________________ ";

   499 " _________________ me + tacs input _________________ ";

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

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

   502 	   "solutions L"];

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

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

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

   506 "--- s1 ---";

   507 (*val p = e_pos'; val c = [];

   508 val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));

   509 val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;*)

   510 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];

   511 "--- s1b ---";

   512 val nxt = ("Model_Problem",

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

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

   515 "--- s2 ---";

   516 val nxt = ("Add_Given",

   517 Add_Given "equality (sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x))");

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

   519 "--- s3 ---";

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

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

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

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

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

   525 "--- s5 ---";

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

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

   528 "--- s6 ---";

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

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

   531 "--- s7 ---";

   532 val nxt = ("Specify_Problem",

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

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

   535 "--- s8 ---";

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

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

   538 "--- s9 ---";

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

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

   541 "--- 1 ---";

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

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

   545 (*.9.6.03

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

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

   548  UnparseC.term2str t';

   549 > trace_rewrite:=true;

   550  trace_rewrite:=false;

   551 *)

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

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

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

   557 (*solve*)

   558       val pp = par_pblobj pt p;

   559       val metID = get_obj g_metID pt pp;

   560       val sc = (#scr o get_met) metID;

   561       val is = get_istate_LI pt (p,p_);

   562       val thy' = get_obj g_domID pt pp;

   563       val thy = assoc_thy thy';

   564       val d = Rule_Set.empty;

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

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

   567          val is' = get_istate_LI pt' p';

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

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

   574 "Let (((While contains_root e_e Do\

   575 \Rewrite square_equation_left #>\

   576 \Try (Rewrite_Set Test_simplify) #>\

   577 \Try (Rewrite_Set rearrange_assoc) #>\

   578 \Try (Rewrite_Set Test_simplify)) #>\

   579 \Try (Rewrite_Set norm_equation) #>\

   580 \Try (Rewrite_Set Test_simplify) #>\

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

   582 \Try (Rewrite_Set Test_simplify))\

   583 \e_)";

   585 -------------------------*)

   588 "--- 2 ---";

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

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

   591 "--- 3 ---";

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

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

   594 "--- 4 ---";

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

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

   597 "--- 5 ---";

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

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

   600 "--- 6 ---";

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

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

   603 "--- 7 ---";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   630 else ();

   632 writeln (pr_ctree pr_short pt);

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

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

author	Walther Neuper <walther.neuper@jku.at>
	Thu, 09 Apr 2020 17:13:17 +0200
changeset 59861	65ec9f679c3f
parent 59852	ea7e6679080e
child 59865	75a9d629ea53
permissions	-rw-r--r--