wneuper/isa: test/Tools/isac/OLDTESTS/root-equ.sml@255c853ea2f0

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

     2    use"systest/root-equ.sml";

     3    use"root-equ.sml";

     4    trace_rewrite:= true;

     5    trace_rewrite:= false;

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

     8 *)

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

    12 " _________________ rewrite _________________ ";

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

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

    17 "  ________________ rewrite _________________";

    18 " _________________ rewrite_ x=4_________________ ";

    19 " _________________ rewrite + cappend _________________ ";

    20 " _________________ me Free_Solve _________________ ";

    21 " _________________ me + tacs input _________________ ";

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

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

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

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

    27 val c = [];

    32 (*

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

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

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

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

    37 *)

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

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

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

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

    42 " _________________ rewrite _________________ ";

    43 val thy' = "Test";

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

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

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

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

    48 val rls = ("Test_simplify");

    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 = ("rearrange_assoc");

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

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

    54 val rls = ("isolate_root");

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

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

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

    58 val rls = ("Test_simplify");

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

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

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

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

    63 val asm = asm union asm';

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

    65 val rls = ("Test_simplify");

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

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

    68 val rls = ("norm_equation");

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

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

    71 val rls = ("Test_simplify");

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

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

    74 val rls = ("isolate_bdv");

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

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

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

    78 val rls = ("Test_simplify");

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

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

    82 (*

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

    84 > asm;

    85 val it =

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

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

    88 *)

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

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

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

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

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

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

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

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

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

   104 	   "solutions L::real set" ,

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

   106 val thy = (theory "Isac");

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

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

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

   111 	     "error_bound eps"];

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

   113 	      "bdv is_var",

   114 	      "eps is_const_expr"];

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

   116 val with_  = [(* parseold ...

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

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

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

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

   121 (* 31.1.00

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

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

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

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

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

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

   130 	     "bound_variable bdv"];

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

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

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

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

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

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

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

   142 " _________________ rewrite_ x+4_________________ ";

   143 " _________________ rewrite_ x+4_________________ ";

   144 " _________________ rewrite_ x+4_________________ ";

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

   146 val thm = num_str @{thm square_equation_left};

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

   148 val rls = Test_simplify;

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

   150 val rls = rearrange_assoc;

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

   152 val rls = isolate_root;

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

   155 val rls = Test_simplify;

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

   157 (*

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

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

   160 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   161 ### trying thm 'rdistr_div_right'

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

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

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

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

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

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

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

   170 ### trying thm 'radd_left_commute'

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

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

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

   174 ### trying thm 'radd_assoc'

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

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

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

   179 ### trying thm 'radd_real_const_eq'

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

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

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

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

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

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

   186 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   188 28.8.02: ruleset besser zusammenstellen !!!

   189 *)

   190 val thm = num_str @{thm square_equation_left};

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

   192 val asm = asm union asm';

   193 val rls = Test_simplify;

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

   195 val rls = norm_equation;

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

   197 val rls = Test_simplify;

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

   199 val rls = isolate_bdv;

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

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

   202 val rls = Test_simplify;

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

   204 val t' = term2str t;

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

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

   208 " _________________ rewrite x=4_________________ ";

   209 " _________________ rewrite x=4_________________ ";

   210 " _________________ rewrite x=4_________________ ";

   211 (*

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

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

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

   215 *)

   216 val thy' = "Test";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   235 val asm = asm union asm';

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

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

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

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

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

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

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

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

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

   245 "-4 + x = 0";

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

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

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

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

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

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

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

   257 " _________________ rewrite + cappend _________________ ";

   258 " _________________ rewrite + cappend _________________ ";

   259 " _________________ rewrite + cappend _________________ ";

   260 val thy' = "Test";

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

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

   263 val oris = prep_ori ctl thy

   264 		    ((#ppc o get_pbt)

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

   266 val loc = e_istate;

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

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

   269 val pt = update_branch pt [] TransitiveB;

   270 (*

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

   272 *)

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

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

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

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

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

   278 val pt = update_pbl    pt [] [];

   279 val pt = update_met    pt [] [];

   280 (*

   281 > get_obj g_spec pt [];

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

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

   284 > get_obj g_spec pt [];

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

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

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

   288 > get_obj g_spec pt [];

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

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

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

   292 > get_obj g_spec pt [];

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

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

   295 *)

   298 val pos = [1]:pos;

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

   301 val pos = (lev_on o lev_dn) pos;

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

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

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

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

   307 val pos = lev_on pos;

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

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

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

   312 val pos = lev_on pos;

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

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

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

   317 val pos = lev_on pos;

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

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

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

   322 val pos = lev_on pos;

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

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

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

   327 val pos = lev_on pos;

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

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

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

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

   333 val pos = lev_up pos;

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

   336 val pos = lev_on pos;

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

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

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

   341 val pos = lev_on pos;

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

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

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

   346 val pos = lev_on pos;

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

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

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

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

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

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

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

   355 val pos = lev_on pos;

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

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

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

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

   361 val pos = lev_on pos;

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

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

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

   366 val pos = lev_up pos;

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

   368 get_assumptions_ pt ([],Res);

   370 writeln (pr_ctree pr_short pt);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   385 *)

   387 (*

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

   389 atomty t;

   390 *)

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

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

   395 " _________________ me Free_Solve _________________ ";

   396 " _________________ me Free_Solve _________________ ";

   397 " _________________ me Free_Solve _________________ ";

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

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

   400 	   "solutions L"(*,

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   418 > get_obj g_spec pt (fst p);

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

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

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

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

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

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

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

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

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

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

   429 get_obj g_spec pt [];

   431 "--- -2 ---";

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

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

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

   435 (* 15.4.

   436 "--- -1 ---";

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

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

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

   441 "--- 1 ---";

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

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

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

   445 "--- 2 ---";

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

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

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

   449 "--- 3 ---";

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

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

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

   453 "--- 4 ---";

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

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

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

   457 "--- 5 ---";

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

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

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

   461 "--- 6 ---";

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

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

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

   465 (* 15.4.

   466 "--- ---";

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

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

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

   470 "--- 7 ---";

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

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

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

   474 "--- 8 ---";

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

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

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

   478 "--- 9 ---";

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

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

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

   482 "--- 10 ---.";

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

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

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

   486 "--- 11 ---";

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

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

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

   490 (* 5.4.00.: ---

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

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

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

   494 --- *)

   495 writeln (pr_ctree pr_short pt);

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

   497 *)

   500 " _________________ me + tacs input _________________ ";

   501 " _________________ me + tacs input _________________ ";

   502 " _________________ me + tacs input _________________ ";

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

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

   505 	   "solutions L"];

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

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

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

   509 "--- s1 ---";

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

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

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

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

   514 "--- s1b ---";

   515 val nxt = ("Model_Problem",

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

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

   518 "--- s2 ---";

   519 val nxt = ("Add_Given",

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

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

   522 "--- s3 ---";

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

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

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

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

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

   528 "--- s5 ---";

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

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

   531 "--- s6 ---";

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

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

   534 "--- s7 ---";

   535 val nxt = ("Specify_Problem",

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

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

   538 "--- s8 ---";

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

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

   541 "--- s9 ---";

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

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

   544 "--- 1 ---";

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

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

   548 (*.9.6.03

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

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

   551  term2str t';

   552  trace_rewrite:=true;

   553  trace_rewrite:=false;

   554 *)

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

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

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

   560 (*solve*)

   561       val pp = par_pblobj pt p;

   562       val metID = get_obj g_metID pt pp;

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

   564       val is = get_istate pt (p,p_);

   565       val thy' = get_obj g_domID pt pp;

   566       val thy = assoc_thy thy';

   567       val d = e_rls;

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

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

   570          val is' = get_istate pt' p';

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

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

   577 "Let (((While contains_root e_e Do\

   578 \Rewrite square_equation_left True @@\

   579 \Try (Rewrite_Set Test_simplify False) @@\

   580 \Try (Rewrite_Set rearrange_assoc False) @@\

   581 \Try (Rewrite_Set Test_simplify False)) @@\

   582 \Try (Rewrite_Set norm_equation False) @@\

   583 \Try (Rewrite_Set Test_simplify False) @@\

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

   585 \Try (Rewrite_Set Test_simplify False))\

   586 \e_)";

   588 -------------------------*)

   591 "--- 2 ---";

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

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

   594 "--- 3 ---";

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

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

   597 "--- 4 ---";

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

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

   600 "--- 5 ---";

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

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

   603 "--- 6 ---";

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

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

   606 "--- 7 ---";

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   633 else ();

   635 writeln (pr_ctree pr_short pt);

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

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

author	Walther Neuper <wneuper@ist.tugraz.at>
	Thu, 22 Dec 2016 11:36:20 +0100
changeset 59279	255c853ea2f0
parent 59188	c477d0f79ab9
child 59497	8952c43fdce3
permissions	-rw-r--r--