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 Walther Neuper <neuper@ist.tugraz.at>
Thu, 22 Sep 2011 14:24:34 +0200
branchdecompose-isar
changeset 42279 e2759e250604
parent 42115 41a68869d217
child 42390 96174a374a7a
permissions -rw-r--r--
made Build_Inverse_Z_Transform.thy run

Build_Inverse_Z_Transform.thy imports Isac.thy for CalcTreeTEST;
Since Isac.thy has Inverse_Z_Transform.thy already as a subtheory
Build_..thy only mimics the process of building the knowledge for a new problem. 
     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 "--------------------------------------------------------";

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

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

    32 

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

    34 

    35 "----------- fun eval_ist_monom ----------------------------------";

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

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

    38 ist_monom (str2term "12");

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

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

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

    42 

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

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

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

    46 

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

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

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

    50 

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

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

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

    54 

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

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

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

    58 

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

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

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

    62 

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

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

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

    66 

    67 

    68 "----------- watch order_add_mult  -------------------------------";

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

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

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

    72 trace_rewrite:=true;

    73 trace_rewrite:=false;

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

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

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

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

    78 trace_rewrite:=false;

    79 

    80 "----- the same stepwise...";

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

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

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

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

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

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

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

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

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

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

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

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

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

    94 

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

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

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

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

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

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

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

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

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

   104 

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

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

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

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

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

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

   111 

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

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

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

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

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

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

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

   119 

   120 

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

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

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

   124 "a" < "b";

   125 "ba" < "ab";

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

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

   128 

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

   130 str2term "aaa";

   131 str2term "222 * aaa";

   132 (*

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

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

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

   136 *)

   137 (*========== inhibit exn =======================================================

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

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

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

   141 

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

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

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

   145 

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

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

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

   149 

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

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

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

   153 

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

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

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

   157 

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

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

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

   161 

   162 ============ inhibit exn =====================================================*)

   163 

   164 

   165 "----- compare tausche_plus with real_num_collect";

   166 val od = dummy_ord;

   167 

   168 val erls = erls_ordne_alphabetisch;

   169 val t = str2term "b + a";

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

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

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

   173 

   174 val erls = Atools_erls;

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

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

   177 

   178 "----- test rewrite_, rewrite_set_";

   179 trace_rewrite:=true;

   180 val erls = erls_ordne_alphabetisch;

   181 val t = str2term "b + a";

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

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

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

   185 

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

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

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

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

   190 

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

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

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

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

   195 

   196 "----- rewrite goes into subterms";

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

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

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

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

   201 

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

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

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

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

   206 

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

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

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

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

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

   212 

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

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

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

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

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

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

   219 

   220 

   221 "----------- build fasse_zusammen --------------------------------";

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

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

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

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

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

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

   228 

   229 "----------- build verschoenere ----------------------------------";

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

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

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

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

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

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

   236 

   237 trace_rewrite:=true;

   238 trace_rewrite:=false;

   239 

   240 "----------- met simplification for_polynomials with_minus -------";

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

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

   243 val str = 

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

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

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

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

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

   249 atomty sc;

   250 

   251 

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

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

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

   255 val c = [];

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

   257       CalcTreeTEST 

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

   259            "normalform N"],

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

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

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

   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 

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

   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 if f2str f = "3 - 2 * e + 2 * f + 2 * g" andalso #1 nxt = "End_Proof'" then ()

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

   276 

   277 

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

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

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

   281 "----------- 140 c ---";

   282 states:=[];

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

   284 	    "normalform N"],

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

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

   287 moveActiveRoot 1;

   288 autoCalculate 1 CompleteCalc;

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

   290 if p = ([], Res) andalso 

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

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

   293 

   294 "----------- 140 d ---";

   295 states:=[];

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

   297 	    "normalform N"],

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

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

   300 moveActiveRoot 1;

   301 autoCalculate 1 CompleteCalc;

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

   303 if p = ([], Res) andalso 

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

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

   306 

   307 

   308 "----------- 139 c ---";

   309 states:=[];

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

   311 	    "normalform N"],

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

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

   314 moveActiveRoot 1;

   315 autoCalculate 1 CompleteCalc;

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

   317 if p = ([], Res) andalso 

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

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

   320 

   321 "----------- 139 b ---";

   322 states:=[];

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

   324 	    "normalform N"],

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

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

   327 moveActiveRoot 1;

   328 autoCalculate 1 CompleteCalc;

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

   330 if p = ([], Res) andalso 

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

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

   333 

   334 "----------- 138 a ---";

   335 states:=[];

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

   337 	    "normalform N"],

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

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

   340 moveActiveRoot 1;

   341 autoCalculate 1 CompleteCalc;

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

   343 if p = ([], Res) andalso 

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

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

   346 

   347 

   348 "----------- met probe fuer_polynom ------------------------------";

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

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

   351 val str = 

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

   353 \ (let e_e = Take e_e;                             \

   354 \      e_e = Substitute w_s e_e                    \

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

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

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

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

   359 atomty sc;

   360 

   361 

   362 "----------- pbl polynom probe -----------------------------------";

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

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

   365 states:=[];

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

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

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

   369 	    "Geprueft b"],

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

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

   372 moveActiveRoot 1;

   373 autoCalculate 1 CompleteCalc;

   374 (* autoCalculate 1 CompleteCalcHead;

   375    autoCalculate 1 (Step 1);

   376    autoCalculate 1 (Step 1);

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

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

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

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

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

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

   383 show_pt pt;

   384 

   385 

   386 

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

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

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

   390 states:=[];

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

   392 	    "normalform N"],

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

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

   395 moveActiveRoot 1;

   396 autoCalculate 1 CompleteCalc;

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

   398 if p = ([], Res) andalso 

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

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

   401 show_pt pt;

   402 

   403 "----- probe p.34 -----";

   404 states:=[];

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

   406 	    "mitWert [u = 2]",

   407 	    "Geprueft b"],

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

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

   410 moveActiveRoot 1;

   411 autoCalculate 1 CompleteCalc;

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

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

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

   415 show_pt pt;

   416 (*========== inhibit exn 110719 ================================================

   417 

   418 

   419 "----------- try fun applyTactics --------------------------------";

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

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

   422 states:=[];

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

   424 	    "normalform N"],

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

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

   427 moveActiveRoot 1;

   428 autoCalculate 1 CompleteCalcHead;

   429 autoCalculate 1 (Step 1);

   430 autoCalculate 1 (Step 1);

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

   432 "----- 1 ^^^";

   433 fetchApplicableTactics 1 0 p;

   434 val appltacs = sel_appl_atomic_tacs pt p;

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

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

   437 "----- 2 ^^^";

   438 trace_rewrite := true;

   439 val erls = erls_ordne_alphabetisch;

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

   441 val SOME (t',_) = 

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

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

   444 

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

   446 val NONE = 

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

   448 

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

   450 val SOME (t',_) = 

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

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

   453 trace_rewrite := false;

   454 

   455 

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

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

   458 "----- 3 ^^^";

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

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

   461 "----- 4 ^^^";

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

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

   464 "----- 5 ^^^";

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

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

   467 "----- 6 ^^^";

   468 

   469 (*<CALCMESSAGE> failure </CALCMESSAGE>

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

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

   472 "----- 7 ^^^";

   473 *)

   474 ============ inhibit exn 110719 ==============================================*)

   475 autoCalculate 1 CompleteCalc;

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

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

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

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

   480 ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)

   481 

   482 

   483 "#############################################################################";

   484 states:=[];

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

   486 	    "normalform N"],

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

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

   489 moveActiveRoot 1;

   490 autoCalculate 1 CompleteCalc;

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

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

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

   494 

   495 

   496 "#############################################################################";

   497 states:=[];

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

   499 	    "normalform N"],

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

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

   502 moveActiveRoot 1;

   503 autoCalculate 1 CompleteCalc;

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

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

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

   507 

   508 (*========== inhibit exn 110719 ================================================

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

   548 states:=[];

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

   550 	    "normalform N"],

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

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

   553 moveActiveRoot 1;

   554 autoCalculate 1 CompleteCalc;

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

   556 if p = ([], Res) andalso 

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

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

   559 

   560 

   561 

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

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

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

   565 states:=[];

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

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

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

   569 moveActiveRoot 1;

   570 autoCalculate 1 CompleteCalc;

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

   572 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "12 * a - 16 * q" 

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

   574 

   575 (*========== inhibit exn 110719 ================================================

   576 

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

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

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

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

   581 	    "normalform N"];

   582 print_depth 11;

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

   584 print_depth 3;

   585 

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

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

   588 (*=== inhibit exn ==============================================================

   589 !!!!! no '?a' ............

   590 val t = str2term 

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

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

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

   594 case ma of

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

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

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

   598 

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

   600 val prls = append_rls "prls_pbl_vereinf_poly" e_rls 

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

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

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

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

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

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

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

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

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

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

   611 trace_rewrite := true;

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

   613 trace_rewrite := false;

   614 

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

   616 val t = str2term 

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

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

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

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

   621 trace_rewrite := true;

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

   623 trace_rewrite := false;

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

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

   626 ============ inhibit exn =====================================================*)

   627 

   628 

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

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

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

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

   633 val t = parse_patt thy "t_t is_polyexp";

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

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

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

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

   638 show_types := true;

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

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

   641 show_types := false;

   642 

   643 

   644 ============ inhibit exn 110719 ==============================================*)

   645
wneuper/isa