wneuper/isa: test/Tools/isac/OLDTESTS/root-equ.sml@06ec8abfd3bc

     1 (*

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

     5 *)

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

     8 " _________________ rewrite _________________ ";

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

    12 " -------------- model, specify ------------ ";

    13 "  ________________ rewrite _________________";

    14 " _________________ rewrite_ x=4_________________ ";

    15 " _________________ rewrite + cappend _________________ ";

    16 " _________________ me Free_Solve _________________ ";

    17 " _________________ me + tacs input _________________ ";

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

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

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

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

    23 val c = [];

    28 (*

    29 > val t = (Thm.term_of o the o (TermC.parse thy)) "#2 \<up> #3";

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

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

    32 > Syntax.string_of_term (Proof_Context.init_global thy) t';

    33 *)

    34 (******************************************************************)

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

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

    37 (*                  -------------------------------------         *)

    38 " _________________ rewrite _________________ ";

    39 val thy' = "Test";

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

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

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

    43 (*"9 + 4 * x = (sqrt x + sqrt (-3 + x)) \<up> 2"*)

    44 val rls = ("Test_simplify");

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

    46 (*"9 + 4 * x = -3 + (2 * x + 2 * sqrt (x \<up> 2 + -3 * x))"*)

    47 val rls = ("rearrange_assoc");

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

    49 (*"9 + 4 * x = -3 + 2 * x + 2 * sqrt (x \<up> 2 + -3 * x)"*)

    50 val rls = ("isolate_root");

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

    52 (*"sqrt (x \<up> 2 + -3 * x) =

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

    54 val rls = ("Test_simplify");

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

    56 (*"sqrt (x \<up> 2 + -3 * x) = 6 + x"*)

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

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

    59 val asm = asm union asm';

    60 (*"x \<up> 2 + -3 * x = (6 + x) \<up> 2"*)

    61 val rls = ("Test_simplify");

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

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

    64 val rls = ("norm_equation");

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

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

    67 val rls = ("Test_simplify");

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

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

    70 val rls = ("isolate_bdv");

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

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

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

    74 val rls = ("Test_simplify");

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

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

    78 (*

    79 val ct = "x = (-12) / 5" : TermC.as_string

    80 > asm;

    81 val it =

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

    83    "(+0) <= (-3) * x + x \<up> 2", "(+0) <= 6 + x"] : TermC.as_string list

    84 *)

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

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

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

    94 " -------------- model, specify ------------ ";

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

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

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

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

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

   100 	   "solutions L::real set" ,

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

   102 val thy = (theory "Isac_Knowledge");

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

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

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

   107 	     "error_bound eps"];

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

   109 	      "bdv is_var",

   110 	      "eps is_const_expr"];

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

   112 val with_  = [(* parseold ...

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

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

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

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

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

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

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

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

   123 	     "bound_variable bdv"];

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

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

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

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

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

   131 " _________________ rewrite_ x+4_________________ ";

   132 " _________________ rewrite_ x+4_________________ ";

   133 " _________________ rewrite_ x+4_________________ ";

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

   135 val thm = ThmC.numerals_to_Free @{thm square_equation_left};

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

   137 val rls = Test_simplify;

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

   139 val rls = rearrange_assoc;

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

   141 val rls = isolate_root;

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

   144 val rls = Test_simplify;

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

   146 (*

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

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

   149 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   150 ### trying thm 'rdistr_div_right'

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

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

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

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

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

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

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

   159 ### trying thm 'radd_left_commute'

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

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

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

   163 ### trying thm 'radd_assoc'

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

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

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

   168 ### trying thm 'radd_real_const_eq'

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

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

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

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

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

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

   175 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   177 28.8.02: ruleset besser zusammenstellen !!!

   178 *)

   179 val thm = ThmC.numerals_to_Free @{thm square_equation_left};

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

   181 val asm = asm union asm';

   182 val rls = Test_simplify;

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

   184 val rls = norm_equation;

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

   186 val rls = Test_simplify;

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

   188 val rls = isolate_bdv;

   189 val subst = [(TermC.parse_test @{context} "bdv", TermC.parse_test @{context} "x")];

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

   191 val rls = Test_simplify;

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

   193 val t' = UnparseC.term t;

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

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

   197 " _________________ rewrite x=4_________________ ";

   198 " _________________ rewrite x=4_________________ ";

   199 " _________________ rewrite x=4_________________ ";

   200 (*

   201 rewrite thy' "tless_true" "tval_rls" true (ThmC.numerals_to_Free @{thm rbinom_power_2}) ct;

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

   203 TermC.atom_trace_detail @{context} (Thm.term_of (!tct));

   204 *)

   205 val thy' = "Test";

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

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

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

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

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

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

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

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

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

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

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

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

   218 "sqrt (x \<up> 2 + 5 * x) = (5 + 2 * x + -1 * (9 + 4 * x)) // (-1 * 2)";

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

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

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

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

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

   224 val asm = asm union asm';

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

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

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

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

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

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

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

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

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

   234 "-4 + x = 0";

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

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

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

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

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

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

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

   246 " _________________ rewrite + cappend _________________ ";

   247 " _________________ rewrite + cappend _________________ ";

   248 " _________________ rewrite + cappend _________________ ";

   249 val thy' = "Test";

   250 val ct = TermC.parse_test @{context}"sqrt(9+4*x)=sqrt x + sqrt(5+x)";

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

   252 val oris = O_Model.init thy ctl

   253 		    ((#model o Problem.from_store)

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

   255 val loc = Istate.empty;

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

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

   258 val pt = update_branch pt [] TransitiveB;

   259 (*

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

   261 *)

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

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

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

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

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

   267 val pt = update_pbl    pt [] [];

   268 val pt = update_met    pt [] [];

   269 (*

   270 > get_obj g_spec pt [];

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

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

   273 > get_obj g_spec pt [];

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

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

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

   277 > get_obj g_spec pt [];

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

   279    (ThyC.id_empty, MethodC.id_empty)) : spec

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

   281 > get_obj g_spec pt [];

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

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

   284 *)

   287 val pos = [1]:pos;

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

   290 val pos = (lev_on o lev_dn) pos;

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

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

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

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

   296 val pos = lev_on pos;

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

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

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

   301 val pos = lev_on pos;

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

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

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

   306 val pos = lev_on pos;

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

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

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

   311 val pos = lev_on pos;

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

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

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

   316 val pos = lev_on pos;

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

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

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

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

   322 val pos = lev_up pos;

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

   325 val pos = lev_on pos;

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

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

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

   330 val pos = lev_on pos;

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

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

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

   335 val pos = lev_on pos;

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

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

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

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

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

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

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

   344 val pos = lev_on pos;

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

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

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

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

   350 val pos = lev_on pos;

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

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

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

   355 val pos = lev_up pos;

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

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

   359 writeln (pr_ctree ctxt pr_short pt);

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

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

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

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

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

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

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

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

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

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

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

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

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

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

   374 *)

   376 (*

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

   378 TermC.atom_trace_detail @{context} t;

   379 *)

   382 (*- 20.9.02: Free_Solve would need the asm_rls (for conditions of rules)

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

   384 " _________________ me Free_Solve _________________ ";

   385 " _________________ me Free_Solve _________________ ";

   386 " _________________ me Free_Solve _________________ ";

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

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

   389 	   "solutions L"(*,

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

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

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

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

   394 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

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

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

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

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

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

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

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

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

   403 (* val nxt = ("Specify_Theory",Specify_Theory "Diff_Appl");

   404 > get_obj g_spec pt (fst p);

   405 val it = (ThyC.id_empty,Problem.id_empty,(ThyC.id_empty, MethodC.id_empty)) : spec*)

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

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

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

   409 (*val nxt = ("Specify_Method",Specify_Method ("Diff_Appl", "sqrt-equ-test"));*)

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

   411 (*val nxt = ("Apply_Method",Apply_Method ("Diff_Appl", "sqrt-equ-test"));*)

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

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

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

   415 get_obj g_spec pt [];

   417 "--- -2 ---";

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

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

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

   421 (* 15.4.

   422 "--- -1 ---";

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

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

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

   427 "--- 1 ---";

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

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

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

   431 "--- 2 ---";

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

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

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

   435 "--- 3 ---";

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

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

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

   439 "--- 4 ---";

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

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

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

   443 "--- 5 ---";

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

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

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

   447 "--- 6 ---";

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

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

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

   451 (* 15.4.

   452 "--- ---";

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

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

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

   456 "--- 7 ---";

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

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

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

   460 "--- 8 ---";

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

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

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

   464 "--- 9 ---";

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

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

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

   468 "--- 10 ---.";

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

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

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

   472 "--- 11 ---";

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

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

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

   476 (* 5.4.00.: ---

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

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

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

   480 --- *)

   481 writeln (pr_ctree ctxt pr_short pt);

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

   483 *)

   486 " _________________ me + tacs input _________________ ";

   487 " _________________ me + tacs input _________________ ";

   488 " _________________ me + tacs input _________________ ";

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

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

   491 	   "solutions L"];

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

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

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

   495 "--- s1 ---";

   496 val (p,_,f,nxt,_,pt) = Test_Code.init_calc @{context} [(fmz, (dI',pI',mI'))];

   497 "--- s1b ---";

   498 val nxt = ("Model_Problem",

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

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

   501 "--- s2 ---";

   502 val nxt = ("Add_Given",

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

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

   505 "--- s3 ---";

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

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

   508 (*"--- s4 ---";

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

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

   511 "--- s5 ---";

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

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

   514 "--- s6 ---";

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

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

   517 "--- s7 ---";

   518 val nxt = ("Specify_Problem",

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

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

   521 "--- s8 ---";

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

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

   524 "--- s9 ---";

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

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

   527 "--- 1 ---";

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

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

   531 (*.9.6.03

   532  val t = TermC.parse_test @{context} "sqrt (9 + 4 * x) = sqrt x + sqrt (5 + x)";

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

   534  UnparseC.term t';

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

   536 *)

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

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

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

   542 (*solve*)

   543       val pp = par_pblobj pt p;

   544       val metID = get_obj g_metID pt pp;

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

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

   547       val thy' = get_obj g_domID pt pp;

   548       val thy = ThyC.get_theory thy';

   549       val d = Rule_Set.empty;

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

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

   552          val is' = get_istate_LI pt' p';

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

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

   559 "Let (((While contains_root e_e Do\

   560 \Rewrite square_equation_left #>\

   561 \Try (Rewrite_Set Test_simplify) #>\

   562 \Try (Rewrite_Set rearrange_assoc) #>\

   563 \Try (Rewrite_Set Test_simplify)) #>\

   564 \Try (Rewrite_Set norm_equation) #>\

   565 \Try (Rewrite_Set Test_simplify) #>\

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

   567 \Try (Rewrite_Set Test_simplify))\

   568 \e_)";

   570 -------------------------*)

   573 "--- 2 ---";

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

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

   576 "--- 3 ---";

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

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

   579 "--- 4 ---";

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

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

   582 "--- 5 ---";

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

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

   585 "--- 6 ---";

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

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

   588 "--- 7 ---";

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

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

   591 "--- 8<> ---";

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

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

   594 "--- 9<> ---";

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

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

   597 "--- 10<> ---";

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

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

   600 "--- 11<> ---.";

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

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

   603 "--- 12<> ---";

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

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

   606 "--- 13<> ---";

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

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

   609 "--- 1<> ---";

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

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

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

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

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

   615 else ();

   617 writeln (pr_ctree ctxt pr_short pt);

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

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

author	wneuper <Walther.Neuper@jku.at>
	Wed, 11 Jan 2023 11:38:01 +0100
changeset 60650	06ec8abfd3bc
parent 60608	5dabcc1c9235
child 60660	c4b24621077e
permissions	-rw-r--r--