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>
Tue, 19 Jul 2011 13:04:59 +0200
branchdecompose-isar
changeset 42115 41a68869d217
parent 42111 d0ba4fce4892
child 42279 e2759e250604
permissions -rw-r--r--
tuned 
     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 if p = ([], Res) andalso 

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

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

   307 

   308 

   309 "----------- 139 c ---";

   310 states:=[];

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

   312 	    "normalform N"],

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

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

   315 moveActiveRoot 1;

   316 autoCalculate 1 CompleteCalc;

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

   318 if p = ([], Res) andalso 

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

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

   321 

   322 "----------- 139 b ---";

   323 states:=[];

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

   325 	    "normalform N"],

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

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

   328 moveActiveRoot 1;

   329 autoCalculate 1 CompleteCalc;

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

   331 if p = ([], Res) andalso 

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

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

   334 

   335 "----------- 138 a ---";

   336 states:=[];

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

   338 	    "normalform N"],

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

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

   341 moveActiveRoot 1;

   342 autoCalculate 1 CompleteCalc;

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

   344 if p = ([], Res) andalso 

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

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

   347 

   348 

   349 "----------- met probe fuer_polynom ------------------------------";

   350 "----------- met probe fuer_polynom ------------------------------";

   351 "----------- met probe fuer_polynom ------------------------------";

   352 val str = 

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

   354 \ (let e_e = Take e_e;                             \

   355 \      e_e = Substitute w_s e_e                    \

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

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

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

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

   360 atomty sc;

   361 

   362 

   363 "----------- pbl polynom probe -----------------------------------";

   364 "----------- pbl polynom probe -----------------------------------";

   365 "----------- pbl polynom probe -----------------------------------";

   366 states:=[];

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

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

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

   370 	    "Geprueft b"],

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

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

   373 moveActiveRoot 1;

   374 autoCalculate 1 CompleteCalc;

   375 (* autoCalculate 1 CompleteCalcHead;

   376    autoCalculate 1 (Step 1);

   377    autoCalculate 1 (Step 1);

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

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

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

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

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

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

   384 show_pt pt;

   385 

   386 

   387 

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

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

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

   391 states:=[];

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

   393 	    "normalform N"],

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

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

   396 moveActiveRoot 1;

   397 autoCalculate 1 CompleteCalc;

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

   399 if p = ([], Res) andalso 

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

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

   402 show_pt pt;

   403 

   404 "----- probe p.34 -----";

   405 states:=[];

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

   407 	    "mitWert [u = 2]",

   408 	    "Geprueft b"],

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

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

   411 moveActiveRoot 1;

   412 autoCalculate 1 CompleteCalc;

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

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

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

   416 show_pt pt;

   417 (*========== inhibit exn 110719 ================================================

   418 

   419 

   420 "----------- try fun applyTactics --------------------------------";

   421 "----------- try fun applyTactics --------------------------------";

   422 "----------- try fun applyTactics --------------------------------";

   423 states:=[];

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

   425 	    "normalform N"],

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

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

   428 moveActiveRoot 1;

   429 autoCalculate 1 CompleteCalcHead;

   430 autoCalculate 1 (Step 1);

   431 autoCalculate 1 (Step 1);

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

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

   434 fetchApplicableTactics 1 0 p;

   435 val appltacs = sel_appl_atomic_tacs pt p;

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

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

   438 "----- 2 ^^^";

   439 trace_rewrite := true;

   440 val erls = erls_ordne_alphabetisch;

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

   442 val SOME (t',_) = 

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

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

   445 

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

   447 val NONE = 

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

   449 

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

   451 val SOME (t',_) = 

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

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

   454 trace_rewrite := false;

   455 

   456 

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

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

   459 "----- 3 ^^^";

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

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

   462 "----- 4 ^^^";

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

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

   465 "----- 5 ^^^";

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

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

   468 "----- 6 ^^^";

   469 

   470 (*<CALCMESSAGE> failure </CALCMESSAGE>

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

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

   473 "----- 7 ^^^";

   474 *)

   475 ============ inhibit exn 110719 ==============================================*)

   476 autoCalculate 1 CompleteCalc;

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

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

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

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

   481 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   482 

   483 

   484 "#############################################################################";

   485 states:=[];

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

   487 	    "normalform N"],

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

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

   490 moveActiveRoot 1;

   491 autoCalculate 1 CompleteCalc;

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

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

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

   495 

   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 (*========== inhibit exn 110719 ================================================

   510 

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

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

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

   514 val rls = klammern_ausmultiplizieren;

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

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

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

   518 val rls = discard_parentheses;

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

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

   521 val rls = ordne_monome;

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

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

   524 (*

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

   526 val rls = ordne_monome;

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

   528 *)

   529 val rls = klammern_aufloesen;

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

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

   532 val rls = ordne_alphabetisch;

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

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

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

   536 (*STOPPED.WN080104

   537 val rls = fasse_zusammen;

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

   539 val rls = verschoenere;

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

   541 *)

   542 

   543 

   544 trace_rewrite := true;

   545 trace_rewrite := false;

   546 

   547 (*@@@@@@@*)

   548 ============ inhibit exn 110719 ==============================================*)

   549 states:=[];

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

   551 	    "normalform N"],

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

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

   554 moveActiveRoot 1;

   555 autoCalculate 1 CompleteCalc;

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

   557 if p = ([], Res) andalso 

   558    term2str (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"

   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 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "12 * a - 16 * q" 

   574 then () else error "pbl binom polynom vereinfachen: cube";

   575 

   576 (*========== inhibit exn 110719 ================================================

   577 

   578 "----------- refine Vereinfache ----------------------------------";

   579 "----------- refine Vereinfache ----------------------------------";

   580 "----------- refine Vereinfache ----------------------------------";

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

   582 	    "normalform N"];

   583 print_depth 11;

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

   585 print_depth 3;

   586 

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

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

   589 (*=== inhibit exn ==============================================================

   590 !!!!! no '?a' ............

   591 val t = str2term 

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

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

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

   595 case ma of

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

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

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

   599 

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

   601 val prls = append_rls "prls_pbl_vereinf_poly" e_rls 

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

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

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

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

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

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

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

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

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

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

   612 trace_rewrite := true;

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

   614 trace_rewrite := false;

   615 

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

   617 val t = str2term 

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

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

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

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

   622 trace_rewrite := true;

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

   624 trace_rewrite := false;

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

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

   627 ============ inhibit exn =====================================================*)

   628 

   629 

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

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

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

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

   634 val t = parse_patt thy "t_t is_polyexp";

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

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

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

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

   639 show_types := true;

   640 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)"

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

   642 show_types := false;

   643 

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

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

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

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

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

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

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

   651 (*val it =

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

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

   654    : ori list

   655 *)

   656 val t = str2term "TERM ttt";

   657 atomwy t;

   658 val t = str2term "term ttt";

   659 atomwy t;

   660 val t = str2term "Term ttt";

   661 atomwy t;

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

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

   664 (*val it =

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

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

   667    : ori list

   668 *)

   669 ============ inhibit exn 110719 ==============================================*)

   670
wneuper/isa