Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/polyminus.sml
author Thomas Leh <t.leh@gmx.at>
Mon, 18 Jul 2011 15:20:04 +0200
branchdecompose-isar
changeset 42098 c77e77ebbf3d
parent 42017 ce19769e9dc4
child 42102 8a263c47ac85
permissions -rw-r--r--
TESTS not WORKING !

intermed: autocalculuate..CompleteCalc
? done in Knowledge/diophanteq.sml ?
test/Tools/isac/Knowledge/polyminus.sml 
     1 (* tests on PolyMinus

     2    author: Walther Neuper

     3    WN071207,

     4    (c) due to copyright terms

     5 

     6 use"../smltest/IsacKnowledge/polyminus.sml";

     7 use"polyminus.sml";

     8 *)

     9 "--------------------------------------------------------";

    10 "--------------------------------------------------------";

    11 "table of contents --------------------------------------";

    12 "--------------------------------------------------------";

    13 "----------- fun eval_ist_monom -------------------------";

    14 "----------- watch order_add_mult  ----------------------";

    15 "----------- build predicate for +- ordering ------------";

    16 "----------- build fasse_zusammen -----------------------";

    17 "----------- build verschoenere -------------------------";

    18 "----------- met simplification for_polynomials with_minu";

    19 "----------- me simplification.for_polynomials.with_minus";

    20 "----------- pbl polynom vereinfachen p.33 --------------";

    21 "----------- met probe fuer_polynom ---------------------";

    22 "----------- pbl polynom probe --------------------------";

    23 "----------- pbl klammer polynom vereinfachen p.34 ------";

    24 "----------- try fun applyTactics -----------------------";

    25 "----------- pbl binom polynom vereinfachen p.39 --------";

    26 "----------- pbl binom polynom vereinfachen: cube -------";

    27 "----------- refine Vereinfache -------------------------";

    28 "----------- *** prep_pbt: syntax error in '#Where' of [v";

    29 "----------- check: fmz matches pbt ---------------------";

    30 "--------------------------------------------------------";

    31 "--------------------------------------------------------";

    32 "--------------------------------------------------------";

    33 

    34 val thy = @{theory "PolyMinus"};

    35 

    36 "----------- fun eval_ist_monom ----------------------------------";

    37 "----------- fun eval_ist_monom ----------------------------------";

    38 "----------- fun eval_ist_monom ----------------------------------";

    39 ist_monom (str2term "12");

    40 case eval_ist_monom 0 0 (str2term "12 ist_monom") 0 of

    41     SOME ("12 ist_monom = True", _) => ()

    42   | _ => error "polyminus.sml: 12 ist_monom = True";

    43 

    44 case eval_ist_monom 0 0 (str2term "a ist_monom") 0 of

    45     SOME ("a ist_monom = True", _) => ()

    46   | _ => error "polyminus.sml: a ist_monom = True";

    47 

    48 case eval_ist_monom 0 0 (str2term "(3*a) ist_monom") 0 of

    49     SOME ("3 * a ist_monom = True", _) => ()

    50   | _ => error "polyminus.sml: 3 * a ist_monom = True";

    51 

    52 case eval_ist_monom 0 0 (str2term "(a^^^2) ist_monom") 0 of 

    53    SOME ("a ^^^ 2 ist_monom = True", _) => ()

    54   | _ => error "polyminus.sml: a^^^2 ist_monom = True";

    55 

    56 case eval_ist_monom 0 0 (str2term "(3*a^^^2) ist_monom") 0 of

    57     SOME ("3 * a ^^^ 2 ist_monom = True", _) => ()

    58   | _ => error "polyminus.sml: 3*a^^^2 ist_monom = True";

    59 

    60 case eval_ist_monom 0 0 (str2term "(a*b) ist_monom") 0 of

    61     SOME ("a * b ist_monom = True", _) => ()

    62   | _ => error "polyminus.sml: a*b ist_monom = True";

    63 

    64 case eval_ist_monom 0 0 (str2term "(3*a*b) ist_monom") 0 of

    65     SOME ("3 * a * b ist_monom = True", _) => ()

    66   | _ => error "polyminus.sml: 3*a*b ist_monom = True";

    67 

    68 

    69 "----------- watch order_add_mult  -------------------------------";

    70 "----------- watch order_add_mult  -------------------------------";

    71 "----------- watch order_add_mult  -------------------------------";

    72 "----- with these simple variables it works...";

    73 trace_rewrite:=true;

    74 trace_rewrite:=false;

    75 val t = str2term "((a + d) + c) + b";

    76 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;

    77 if term2str t = "a + (b + (c + d))" then ()

    78 else error "polyminus.sml 1 watch order_add_mult";

    79 trace_rewrite:=false;

    80 

    81 "----- the same stepwise...";

    82 val od = ord_make_polynomial true (@{theory "Poly"});

    83 val t = str2term "((a + d) + c) + b";

    84 "((a + d) + c) + b"; 

    85 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;

    86 "b + ((a + d) + c)";

    87 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t; term2str t;

    88 "b + (c + (a + d))";

    89 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;

    90 "b + (a + (c + d))";

    91 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;

    92 "a + (b + (c + d))";

    93 if term2str t = "a + (b + (c + d))" then ()

    94 else error "polyminus.sml 2 watch order_add_mult";

    95 

    96 "----- if parentheses are right, left_commute is (almost) sufficient...";

    97 val t = str2term "a + (d + (c + b))";

    98 "a + (d + (c + b))";

    99 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;

   100 "a + (c + (d + b))";

   101 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_commute} t;term2str t;

   102 "a + (c + (b + d))";

   103 val SOME (t,_) = rewrite_ thy od e_rls true @{thm add_left_commute} t;term2str t;

   104 "a + (b + (c + d))";

   105 

   106 "----- but we do not want the parentheses at right; thus: cond.rew.";

   107 "WN0712707 complicated monomials do not yet work ...";

   108 val t = str2term "((5*a + 4*d) + 3*c) + 2*b";

   109 val SOME (t,_) = rewrite_set_ thy false order_add_mult t; term2str t;

   110 if term2str t = "2 * b + (3 * c + (4 * d + 5 * a))" then ()

   111 else error "polyminus.sml: order_add_mult changed";

   112 

   113 "----- here we see rew_sub going into subterm with ord.rew....";

   114 val od = ord_make_polynomial false (@{theory "Poly"});

   115 val t = str2term "b + a + c + d";

   116 val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;

   117 val SOME (t,_) = rewrite_ thy od e_rls false @{thm add_commute} t; term2str t;

   118 (*@@@ rew_sub gosub: t = d + (b + a + c)

   119   @@@ rew_sub begin: t = b + a + c*)

   120 

   121 

   122 "----------- build predicate for +- ordering ---------------------";

   123 "----------- build predicate for +- ordering ---------------------";

   124 "----------- build predicate for +- ordering ---------------------";

   125 "a" < "b";

   126 "ba" < "ab";

   127 "123" < "a"; (*unused due to ---vvv*)

   128 "12" < "3"; (*true !!!*)

   129 

   130 " a kleiner b ==> (b + a) = (a + b)";

   131 str2term "aaa";

   132 str2term "222 * aaa";

   133 (*

   134 case eval_kleiner 0 0 (str2term "123 kleiner 32") 0 of

   135     SOME ("12 kleiner 9 = False", _) => ()

   136   | _ => error "polyminus.sml: 12 kleiner 9 = False";

   137 *)

   138 (*========== inhibit exn =======================================================

   139 case eval_kleiner 0 0 (str2term "a kleiner b") 0 of

   140     SOME ("a kleiner b = True", _) => ()

   141   | _ => error "polyminus.sml: a kleiner b = True";

   142 

   143 case eval_kleiner 0 0 (str2term "(10*g) kleiner f") 0 of

   144     SOME ("10 * g kleiner f = False", _) => ()

   145   | _ => error "polyminus.sml: 10 * g kleiner f = False";

   146 

   147 case eval_kleiner 0 0 (str2term "(a^^^2) kleiner b") 0 of

   148     SOME ("a ^^^ 2 kleiner b = True", _) => ()

   149   | _ => error "polyminus.sml: a ^^^ 2 kleiner b = True";

   150 

   151 case eval_kleiner 0 0 (str2term "(3*a^^^2) kleiner b") 0 of

   152     SOME ("3 * a ^^^ 2 kleiner b = True", _) => ()

   153   | _ => error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True";

   154 

   155 case eval_kleiner 0 0 (str2term "(a*b) kleiner c") 0 of

   156     SOME ("a * b kleiner c = True", _) => ()

   157   | _ => error "polyminus.sml: a * b kleiner b = True";

   158 

   159 case eval_kleiner 0 0 (str2term "(3*a*b) kleiner c") 0 of

   160     SOME ("3 * a * b kleiner c = True", _) => ()

   161   | _ => error "polyminus.sml: 3 * a * b kleiner b = True";

   162 

   163 ============ inhibit exn =====================================================*)

   164 

   165 

   166 "----- compare tausche_plus with real_num_collect";

   167 val od = dummy_ord;

   168 

   169 val erls = erls_ordne_alphabetisch;

   170 val t = str2term "b + a";

   171 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t;

   172 if term2str t = "a + b" then ()

   173 else error "polyminus.sml: ordne_alphabetisch1 b + a";

   174 

   175 val erls = Atools_erls;

   176 val t = str2term "2*a + 3*a";

   177 val SOME (t,_) = rewrite_ thy od erls false @{thm real_num_collect} t; term2str t;

   178 

   179 "----- test rewrite_, rewrite_set_";

   180 trace_rewrite:=true;

   181 val erls = erls_ordne_alphabetisch;

   182 val t = str2term "b + a";

   183 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;

   184 if term2str t = "a + b" then ()

   185 else error "polyminus.sml: ordne_alphabetisch a + b";

   186 

   187 val t = str2term "2*b + a";

   188 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;

   189 if term2str t = "a + 2 * b" then ()

   190 else error "polyminus.sml: ordne_alphabetisch a + 2 * b";

   191 

   192 val t = str2term "a + c + b";

   193 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;

   194 if term2str t = "a + b + c" then ()

   195 else error "polyminus.sml: ordne_alphabetisch a + b + c";

   196 

   197 "----- rewrite goes into subterms";

   198 val t = str2term "a + c + b + d";

   199 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus_plus} t; term2str t;

   200 if term2str t = "a + b + c + d" then ()

   201 else error "polyminus.sml: ordne_alphabetisch1 a + b + c + d";

   202 

   203 val t = str2term "a + c + d + b";

   204 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; term2str t;

   205 if term2str t = "a + b + c + d" then ()

   206 else error "polyminus.sml: ordne_alphabetisch2 a + b + c + d";

   207 

   208 "----- here we see rew_sub going into subterm with cond.rew....";

   209 val t = str2term "b + a + c + d";

   210 val SOME (t,_) = rewrite_ thy od erls false @{thm tausche_plus} t; term2str t;

   211 if term2str t = "a + b + c + d" then ()

   212 else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";

   213 

   214 "----- compile rls for the most complicated terms";

   215 val t = str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";

   216 "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";

   217 val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; 

   218 if term2str t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"

   219 then () else error "polyminus.sml: ordne_alphabetisch finished";

   220 

   221 

   222 "----------- build fasse_zusammen --------------------------------";

   223 "----------- build fasse_zusammen --------------------------------";

   224 "----------- build fasse_zusammen --------------------------------";

   225 val t = str2term "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";

   226 val SOME (t,_) = rewrite_set_ thy false fasse_zusammen t;

   227 if term2str t = "3 + -2 * e + 2 * f + 2 * g" then ()

   228 else error "polyminus.sml: fasse_zusammen finished";

   229 

   230 "----------- build verschoenere ----------------------------------";

   231 "----------- build verschoenere ----------------------------------";

   232 "----------- build verschoenere ----------------------------------";

   233 val t = str2term "3 + -2 * e + 2 * f + 2 * g";

   234 val SOME (t,_) = rewrite_set_ thy false verschoenere t;

   235 if term2str t = "3 - 2 * e + 2 * f + 2 * g" then ()

   236 else error "polyminus.sml: verschoenere 3 + -2 * e ...";

   237 

   238 trace_rewrite:=true;

   239 trace_rewrite:=false;

   240 

   241 "----------- met simplification for_polynomials with_minus -------";

   242 "----------- met simplification for_polynomials with_minus -------";

   243 "----------- met simplification for_polynomials with_minus -------";

   244 val str = 

   245 "Script SimplifyScript (t_t::real) =                \

   246 \  (((Try (Rewrite_Set ordne_alphabetisch False)) @@     \

   247 \    (Try (Rewrite_Set fasse_zusammen False)) @@     \

   248 \    (Try (Rewrite_Set verschoenere False))) t_t)"

   249 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   250 atomty sc;

   251 

   252 

   253 "----------- me simplification.for_polynomials.with_minus";

   254 "----------- me simplification.for_polynomials.with_minus";

   255 "----------- me simplification.for_polynomials.with_minus";

   256 val c = [];

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

   258       CalcTreeTEST 

   259         [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",

   260            "normalform N"],

   261 	          ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   262 	           ["simplification","for_polynomials","with_minus"]))];

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

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

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

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

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

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

   269 

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

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

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

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

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

   275 if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()

   276 else error "polyminus.sml: me simplification.for_polynomials.with_minus";

   277 

   278 

   279 "----------- pbl polynom vereinfachen p.33 -----------------------";

   280 "----------- pbl polynom vereinfachen p.33 -----------------------";

   281 "----------- pbl polynom vereinfachen p.33 -----------------------";

   282 "----------- 140 c ---";

   283 states:=[];

   284 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",

   285 	    "normalform N"],

   286 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   287 	    ["simplification","for_polynomials","with_minus"]))];

   288 moveActiveRoot 1;

   289 autoCalculate 1 CompleteCalc;

   290 val ((pt,p),_) = get_calc 1; show_pt pt;

   291 if p = ([], Res) andalso 

   292    term2str (get_obj g_res pt (fst p)) = "3 - 2 * e + 2 * f + 2 * g"

   293 then () else error "polyminus.sml: Vereinfache (3 - 2 * e + 2 * f...";

   294 

   295 "----------- 140 d ---";

   296 states:=[];

   297 CalcTree [(["Term (-r - 2*s - 3*t + 5 + 4*r + 8*s - 5*t - 2)",

   298 	    "normalform N"],

   299 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   300 	    ["simplification","for_polynomials","with_minus"]))];

   301 moveActiveRoot 1;

   302 autoCalculate 1 CompleteCalc;

   303 val ((pt,p),_) = get_calc 1; show_pt pt;

   304 

   305 show_pt pt;

   306 p;

   307 (get_obj g_res pt (fst p));

   308 term2str (get_obj g_res pt (fst p));

   309 if p = ([], Res) andalso 

   310    term2str (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"

   311 then () else error "polyminus.sml: Vereinfache 140 d)";

   312 

   313 

   314 "----------- 139 c ---";

   315 states:=[];

   316 CalcTree [(["Term (3*e - 6*f - 8*e - 4*f + 5*e + 7*f)",

   317 	    "normalform N"],

   318 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   319 	    ["simplification","for_polynomials","with_minus"]))];

   320 moveActiveRoot 1;

   321 autoCalculate 1 CompleteCalc;

   322 val ((pt,p),_) = get_calc 1; show_pt pt;

   323 if p = ([], Res) andalso 

   324    term2str (get_obj g_res pt (fst p)) = "- (3 * f)"

   325 then () else error "polyminus.sml: Vereinfache 139 c)";

   326 

   327 "----------- 139 b ---";

   328 states:=[];

   329 CalcTree [(["Term (8*u - 5*v - 5*u + 7*v - 6*u - 3*v)",

   330 	    "normalform N"],

   331 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   332 	    ["simplification","for_polynomials","with_minus"]))];

   333 moveActiveRoot 1;

   334 autoCalculate 1 CompleteCalc;

   335 val ((pt,p),_) = get_calc 1; show_pt pt;

   336 if p = ([], Res) andalso 

   337    term2str (get_obj g_res pt (fst p)) = "-3 * u - v"

   338 then () else error "polyminus.sml: Vereinfache 139 b)";

   339 

   340 "----------- 138 a ---";

   341 states:=[];

   342 CalcTree [(["Term (2*u - 3*v - 6*u + 5*v)",

   343 	    "normalform N"],

   344 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   345 	    ["simplification","for_polynomials","with_minus"]))];

   346 moveActiveRoot 1;

   347 autoCalculate 1 CompleteCalc;

   348 val ((pt,p),_) = get_calc 1; show_pt pt;

   349 if p = ([], Res) andalso 

   350    term2str (get_obj g_res pt (fst p)) = "-4 * u + 2 * v"

   351 then () else error "polyminus.sml: Vereinfache 138 a)";

   352 

   353 

   354 "----------- met probe fuer_polynom ------------------------------";

   355 "----------- met probe fuer_polynom ------------------------------";

   356 "----------- met probe fuer_polynom ------------------------------";

   357 val str = 

   358 "Script ProbeScript (e_e::bool) (w_s::bool list) =\

   359 \ (let e_e = Take e_e;                             \

   360 \      e_e = Substitute w_s e_e                    \

   361 \ in (Repeat((Try (Repeat (Calculate TIMES))) @@  \

   362 \            (Try (Repeat (Calculate PLUS ))) @@  \

   363 \            (Try (Repeat (Calculate MINUS))))) e_e)"

   364 val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;

   365 atomty sc;

   366 

   367 

   368 "----------- pbl polynom probe -----------------------------------";

   369 "----------- pbl polynom probe -----------------------------------";

   370 "----------- pbl polynom probe -----------------------------------";

   371 states:=[];

   372 CalcTree [(["Pruefe ((5::int)*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12 =\

   373 	    \3 - 2 * e + 2 * f + 2 * g)",

   374 	    "mitWert [e = 1, f = 2, g = 3]",

   375 	    "Geprueft b"],

   376 	   ("PolyMinus",["polynom","probe"],

   377 	    ["probe","fuer_polynom"]))];

   378 moveActiveRoot 1;

   379 autoCalculate 1 CompleteCalc;

   380 (* autoCalculate 1 CompleteCalcHead;

   381    autoCalculate 1 (Step 1);

   382    autoCalculate 1 (Step 1);

   383    val ((pt,p),_) = get_calc 1; term2str (get_obj g_res pt (fst p));

   384 @@@@@WN081114 gives "??.empty", all "Pruefe" are the same,

   385 although analogies work in interface.sml: FIXME.WN081114 in "Pruefe"*)

   386 val ((pt,p),_) = get_calc 1;

   387 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "11 = 11"

   388 then () else error "polyminus.sml: Probe 11 = 11";

   389 show_pt pt;

   390 

   391 

   392 "----------- pbl klammer polynom vereinfachen p.34 ---------------";

   393 "----------- pbl klammer polynom vereinfachen p.34 ---------------";

   394 "----------- pbl klammer polynom vereinfachen p.34 ---------------";

   395 states:=[];

   396 CalcTree [(["Term (2*u - 5 - (3 - 4*u) + (8*u + 9))",

   397 	    "normalform N"],

   398 	   ("PolyMinus",["klammer","polynom","vereinfachen"],

   399 	    ["simplification","for_polynomials","with_parentheses"]))];

   400 moveActiveRoot 1;

   401 autoCalculate 1 CompleteCalc;

   402 val ((pt,p),_) = get_calc 1;

   403 if p = ([], Res) andalso 

   404    term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"

   405 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";

   406 show_pt pt;

   407 

   408 "----- probe p.34 -----";

   409 states:=[];

   410 CalcTree [(["Pruefe (2*u - 5 - (3 - 4*u) + (8*u + 9) = 1 + 14 * u)",

   411 	    "mitWert [u = 2]",

   412 	    "Geprueft b"],

   413 	   ("PolyMinus",["polynom","probe"],

   414 	    ["probe","fuer_polynom"]))];

   415 moveActiveRoot 1;

   416 autoCalculate 1 CompleteCalc;

   417 val ((pt,p),_) = get_calc 1;

   418 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "29 = 29"

   419 then () else error "polyminus.sml: Probe 29 = 29";

   420 show_pt pt;

   421 

   422 

   423 "----------- try fun applyTactics --------------------------------";

   424 "----------- try fun applyTactics --------------------------------";

   425 "----------- try fun applyTactics --------------------------------";

   426 states:=[];

   427 CalcTree [(["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)",

   428 	    "normalform N"],

   429 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   430 	    ["simplification","for_polynomials","with_minus"]))];

   431 moveActiveRoot 1;

   432 autoCalculate 1 CompleteCalcHead;

   433 autoCalculate 1 (Step 1);

   434 autoCalculate 1 (Step 1);

   435 val ((pt,p),_) = get_calc 1; show_pt pt;

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

   437 fetchApplicableTactics 1 0 p;

   438 val appltacs = sel_appl_atomic_tacs pt p;

   439 applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);

   440 val ((pt,p),_) = get_calc 1; show_pt pt;

   441 "----- 2 ^^^";

   442 trace_rewrite := true;

   443 val erls = erls_ordne_alphabetisch;

   444 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";

   445 val SOME (t',_) = 

   446     rewrite_ (@{theory "Isac"}) e_rew_ord erls false @{thm tausche_minus} t;

   447 term2str t';     "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g";

   448 

   449 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";

   450 val NONE = 

   451     rewrite_ (@{theory "Isac"}) e_rew_ord erls false @{thm tausche_minus_plus} t;

   452 

   453 val t = str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";

   454 val SOME (t',_) = 

   455     rewrite_set_ (@{theory "Isac"}) false ordne_alphabetisch t;

   456 term2str t';     "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f";

   457 trace_rewrite := false;

   458 

   459 

   460 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (*tausche_minus*);

   461 val ((pt,p),_) = get_calc 1; show_pt pt;

   462 "----- 3 ^^^";

   463 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);

   464 val ((pt,p),_) = get_calc 1; show_pt pt;

   465 "----- 4 ^^^";

   466 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);

   467 val ((pt,p),_) = get_calc 1; show_pt pt;

   468 "----- 5 ^^^";

   469 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);

   470 val ((pt,p),_) = get_calc 1; show_pt pt;

   471 "----- 6 ^^^";

   472 

   473 (*<CALCMESSAGE> failure </CALCMESSAGE>

   474 applyTactic 1 p (hd (sel_appl_atomic_tacs pt p)) (**);

   475 val ((pt,p),_) = get_calc 1; show_pt pt;

   476 "----- 7 ^^^";

   477 *)

   478 

   479 autoCalculate 1 CompleteCalc;

   480 val ((pt,p),_) = get_calc 1; show_pt pt;

   481 (*independent from failure above: met_simp_poly_minus not confluent:

   482 (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),

   483 (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]

   484 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   485 

   486 states:=[];

   487 CalcTree [(["Term (- (8 * g) + 10 * g + h)",

   488 	    "normalform N"],

   489 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   490 	    ["simplification","for_polynomials","with_minus"]))];

   491 moveActiveRoot 1;

   492 autoCalculate 1 CompleteCalc;

   493 val ((pt,p),_) = get_calc 1; show_pt pt;

   494 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "2 * g + h"

   495 then () else error "polyminus.sml: addiere_vor_minus";

   496 

   497 

   498 states:=[];

   499 CalcTree [(["Term (- (8 * g) + 10 * g + f)",

   500 	    "normalform N"],

   501 	   ("PolyMinus",["plus_minus","polynom","vereinfachen"],

   502 	    ["simplification","for_polynomials","with_minus"]))];

   503 moveActiveRoot 1;

   504 autoCalculate 1 CompleteCalc;

   505 val ((pt,p),_) = get_calc 1; show_pt pt;

   506 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "f + 2 * g"

   507 then () else error "polyminus.sml: tausche_vor_plus";

   508 

   509 

   510 "----------- pbl binom polynom vereinfachen p.39 -----------------";

   511 "----------- pbl binom polynom vereinfachen p.39 -----------------";

   512 "----------- pbl binom polynom vereinfachen p.39 -----------------";

   513 val rls = klammern_ausmultiplizieren;

   514 val t = str2term "(3 * a + 2) * (4 * a - 1)";

   515 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   516 "3 * a * (4 * a) - 3 * a * 1 + (2 * (4 * a) - 2 * 1)";

   517 val rls = discard_parentheses;

   518 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   519 "3 * a * 4 * a - 3 * a * 1 + (2 * 4 * a - 2 * 1)";

   520 val rls = ordne_monome;

   521 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   522 "3 * 4 * a * a - 1 * 3 * a + (2 * 4 * a - 1 * 2)";

   523 (*

   524 val t = str2term "3 * a * 4 * a";

   525 val rls = ordne_monome;

   526 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   527 *)

   528 val rls = klammern_aufloesen;

   529 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   530 "3 * 4 * a * a - 1 * 3 * a + 2 * 4 * a - 1 * 2";

   531 val rls = ordne_alphabetisch;

   532 (*TODO: make is_monom more general, a*a=a^2, ...*)

   533 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   534 "3 * 4 * a * a - 1 * 2 - 1 * 3 * a + 2 * 4 * a";

   535 (*STOPPED.WN080104

   536 val rls = fasse_zusammen;

   537 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   538 val rls = verschoenere;

   539 val SOME (t,_) = rewrite_set_ thy false rls t; term2str t;

   540 *)

   541 

   542 

   543 trace_rewrite := true;

   544 trace_rewrite := false;

   545 

   546 (*@@@@@@@*)

   547 states:=[];

   548 CalcTree [(["Term ((3*a + 2) * (4*a - 1))",

   549 	    "normalform N"],

   550 	   ("PolyMinus",["binom_klammer","polynom","vereinfachen"],

   551 	    ["simplification","for_polynomials","with_parentheses_mult"]))];

   552 moveActiveRoot 1;

   553 autoCalculate 1 CompleteCalc;

   554 val ((pt,p),_) = get_calc 1; show_pt pt;

   555 

   556 (*

   557 if p = ([], Res) andalso 

   558    term2str (get_obj g_res pt (fst p)) = "1 + 14 * u"

   559 then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";

   560 *)

   561 

   562 

   563 "----------- pbl binom polynom vereinfachen: cube ----------------";

   564 "----------- pbl binom polynom vereinfachen: cube ----------------";

   565 "----------- pbl binom polynom vereinfachen: cube ----------------";

   566 states:=[];

   567 CalcTree [(["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))", "normalform N"],

   568 	   ("PolyMinus",["binom_klammer","polynom","vereinfachen"],

   569 	    ["simplification","for_polynomials","with_parentheses_mult"]))];

   570 moveActiveRoot 1;

   571 autoCalculate 1 CompleteCalc;

   572 val ((pt,p),_) = get_calc 1; show_pt pt;

   573 

   574 

   575 "----------- refine Vereinfache ----------------------------------";

   576 "----------- refine Vereinfache ----------------------------------";

   577 "----------- refine Vereinfache ----------------------------------";

   578 val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*q))",

   579 	    "normalform N"];

   580 print_depth 11;

   581 val matches = refine fmz ["vereinfachen"];

   582 print_depth 3;

   583 

   584 "----- go into details, if it seems not to work -----";

   585 "--- does the predicate evaluate correctly ?";

   586 (*=== inhibit exn ==============================================================

   587 !!!!! no '?a' ............

   588 val t = str2term 

   589 	    "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + \

   590 	    \3 * (a - 2 * q))";

   591 val ma = eval_matchsub "" "Tools.matchsub" t thy;

   592 case ma of

   593     SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \

   594 	  \a - 2 * q + 3 * (a - 2 * q)) = True", _) => ()

   595   | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A";

   596 

   597 "--- does the respective prls rewrite ?";

   598 val prls = append_rls "prls_pbl_vereinf_poly" e_rls 

   599 	     [Calc ("Poly.is'_polyexp", eval_is_polyexp ""),

   600 	      Calc ("Tools.matchsub", eval_matchsub ""),

   601 	      Thm ("or_true",@{thm or_true}),

   602 	      (*"(?a | True) = True"*)

   603 	      Thm ("or_false",@{thm or_false}),

   604 	      (*"(?a | False) = ?a"*)

   605 	      Thm ("not_true",num_str @{thm not_true}),

   606 	      (*"(~ True) = False"*)

   607 	      Thm ("not_false",num_str @{thm not_false})

   608 	      (*"(~ False) = True"*)];

   609 trace_rewrite := true;

   610 val SOME (t', _) = rewrite_set_ thy false prls t;

   611 trace_rewrite := false;

   612 

   613 "--- does the respective prls rewrite the whole predicate ?";

   614 val t = str2term 

   615 	    "Not (matchsub (?a * (?b + ?c)) (8 * (a - q) + a - 2 * q) | \

   616 	    \     matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q) | \

   617 	    \     matchsub ((?b + ?c) * ?a) (8 * (a - q) + a - 2 * q) | \

   618 	    \     matchsub ((?b - ?c) * ?a) (8 * (a - q) + a - 2 * q) )";

   619 trace_rewrite := true;

   620 val SOME (t', _) = rewrite_set_ thy false prls t;

   621 trace_rewrite := false;

   622 if term2str t' = "HOL.False" then ()

   623 else error "polyminus.sml Not (matchsub (?a * (?b + ?c)) (8 ...";

   624 ============ inhibit exn =====================================================*)

   625 

   626 

   627 "----------- *** prep_pbt: syntax error in '#Where' of [v";

   628 "----------- *** prep_pbt: syntax error in '#Where' of [v";

   629 "----------- *** prep_pbt: syntax error in '#Where' of [v";

   630 (*see test/../termC.sml for details*)

   631 val t = parse_patt thy "t_t is_polyexp";

   632 val t = parse_patt thy ("Not (matchsub (?a + (?b + ?c)) t_t | " ^

   633 	                "     matchsub (?a + (?b - ?c)) t_t | " ^

   634 	                "     matchsub (?a - (?b + ?c)) t_t | " ^

   635 	                "     matchsub (?a + (?b - ?c)) t_t )");

   636 show_types := true;

   637 if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n   matchsub (?a + (?b - ?c)) t_t |\n   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"

   638 then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";

   639 show_types := false;

   640 

   641 "----------- check: fmz matches pbt ---------------------";

   642 "----------- check: fmz matches pbt ---------------------";

   643 "----------- check: fmz matches pbt ---------------------";

   644 "101230 error *** nxt_add: EX itm. not(dat(itm)<=dat(ori))";

   645 val fmz = ["TERM (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];

   646 val pI = ["plus_minus","polynom","vereinfachen"];

   647 prep_ori fmz thy ((#ppc o get_pbt) pI);

   648 (*val it =

   649    [(1, [1], "#undef", Const (...), [...]),       <<<===

   650     (2, [1], "#Find", Const (...), [...])]

   651    : ori list

   652 *)

   653 val t = str2term "TERM ttt";

   654 atomwy t;

   655 val t = str2term "term ttt";

   656 atomwy t;

   657 val t = str2term "Term ttt";

   658 atomwy t;

   659 val fmz = ["Term (5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12)","normalform N"];

   660 prep_ori fmz thy ((#ppc o get_pbt) pI);

   661 (*val it =

   662    [(1, [1], "#Given", Const (...), [...]),

   663     (2, [1], "#Find", Const (...), [...])]

   664    : ori list

   665 *)
wneuper/isa