wneuper/isa: test/Tools/isac/Knowledge/poly.sml@c3f399ce32af

     1 (* testexamples for Poly, polynomials

     2    author: Matthias Goldgruber 2003

     3    (c) due to copyright terms

     5 12345678901234567890123456789012345678901234567890123456789012345678901234567890

     6         10        20        30        40        50        60        70        80

     7 LEGEND:

     8 WN060104: examples marked with 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'

     9           examples marked with 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'

    10 *)

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

    13 "--------------------------------------------------------";

    14 "table of contents --------------------------------------";

    15 "--------------------------------------------------------";

    16 "-------- check is'_polyexp is_polyexp ------------------";

    17 "-------- investigate (new 2002) uniary minus -----------";

    18 "-------- check make_polynomial with simple terms -------";

    19 "-------- fun is_multUnordered --------------------------";

    20 "-------- examples from textbook Schalk I ---------------";

    21 "-------- check pbl  'polynomial simplification' --------";

    22 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

    23 "-------- interSteps for Schalk 299a --------------------";

    24 "-------- norm_Poly NOT COMPLETE ------------------------";

    25 "-------- ord_make_polynomial ---------------------------";

    26 "--------------------------------------------------------";

    27 "--------------------------------------------------------";

    28 "--------------------------------------------------------";

    31 "-------- check is'_polyexp is_polyexp ------------------";

    32 "-------- check is'_polyexp is_polyexp ------------------";

    33 "-------- check is'_polyexp is_polyexp ------------------";

    34 if is_polyexp @{term "x / x"}

    35 then error "poly.sml: check is'_polyexp is_polyexp" else ();

    37 "-------- investigate (new 2002) uniary minus -----------";

    38 "-------- investigate (new 2002) uniary minus -----------";

    39 "-------- investigate (new 2002) uniary minus -----------";

    40 (*---------------------------------------------- vvvvvvvvvvvvvv -----------------------*)

    41 val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)

    42 atomty t;

    43 (*** -------------

    44 *** Const ( Trueprop, bool => prop)

    45 *** . Const ( op =, [real, real] => bool)

    46 *** . . Const ( op -, [real, real] => real)

    47 *** . . . Const ( 0, real)

    48 *** . . . Var ((x, 0), real)

    49 *** . . Const ( uminus, real => real)

    50 *** . . . Var ((x, 0), real)              *)

    51 case t of

    52   Const ("HOL.Trueprop", _) $

    53           (Const ("HOL.eq", _) $

    54             (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $

    55               Var (("x", 0), _)) $

    56             (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()

    57 | _ => error "internal representation of \"0 - ?x = - ?x\" changed";

    59 (*----------------------------------- vvvv --------------------------------------------*)

    60 val t = (term_of o the o (parse thy)) "-1";

    61 atomty t;

    62 (*** -------------

    63 *** Free ( -1, real)                      *)

    64 case t of

    65   Free ("-1", _) => ()

    66 | _ => error "internal representation of \"-1\" changed";

    67 (*----------------------------------- vvvvv -------------------------------------------*)

    68 val t = (term_of o the o (parse thy)) "- 1";

    69 atomty t;

    70 (*** -------------

    71 *** Const ( uminus, real => real)

    72 *** . Free ( 1, real)                     *)

    73 case t of

    74   Const ("Groups.uminus_class.uminus", _) $ Free ("1", _) => ()

    75 | _ => error "internal representation of \"- 1\" changed";

    77 "======= these external values all have the same internal representation";

    78 (* "1-x" causes syntyx error --- binary minus detected by blank inbetween !!!*)

    79 (*----------------------------------- vvvvv -------------------------------------------*)

    80 val t = (term_of o the o (parse thy)) "-x";

    81 atomty t;

    82 (**** -------------

    83 *** Free ( -x, real)*)

    84 case t of

    85   Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

    86 | _ => error "internal representation of \"-x\" changed";

    87 (*----------------------------------- vvvvv -------------------------------------------*)

    88 val t = (term_of o the o (parse thy)) "- x";

    89 atomty t;

    90 (**** -------------

    91 *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)

    92 case t of

    93   Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

    94 | _ => error "internal representation of \"- x\" changed";

    95 (*----------------------------------- vvvvvv ------------------------------------------*)

    96 val t = (term_of o the o (parse thy)) "-(x)";

    97 atomty t;

    98 (**** -------------

    99 *** Free ( -x, real)*)

   100 case t of

   101   Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()

   102 | _ => error "internal representation of \"-(x)\" changed";

   104 "-------- check make_polynomial with simple terms -------";

   105 "-------- check make_polynomial with simple terms -------";

   106 "-------- check make_polynomial with simple terms -------";

   107 "----- check 1 ---";

   108 val t = str2term "2*3*a";

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

   110 if term2str t = "6 * a" then () else error "check make_polynomial 1";

   112 "----- check 2 ---";

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

   114 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

   115 if term2str t = "5 * a" then () else error "check make_polynomial 2";

   117 "----- check 3 ---";

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

   119 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

   120 if term2str t = "8 * a" then () else error "check make_polynomial 3";

   122 "----- check 4 ---";

   123 val t = str2term "3*a - 2*a";

   124 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

   125 if term2str t = "a" then () else error "check make_polynomial 4";

   127 "----- check 5 ---";

   128 val t = str2term "4*(3*a - 2*a)";

   129 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

   130 if term2str t = "4 * a" then () else error "check make_polynomial 5";

   132 "----- check 6 ---";

   133 val t = str2term "4*(3*a^^^2 - 2*a^^^2)";

   134 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;

   135 if term2str t = "4 * a ^^^ 2" then () else error "check make_polynomial 6";

   137 "-------- fun is_multUnordered --------------------------";

   138 "-------- fun is_multUnordered --------------------------";

   139 "-------- fun is_multUnordered --------------------------";

   140 val thy = @{theory "Isac"};

   141 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";

   142 val t = str2term "x^^^2 * x";

   143 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;

   144 if term2str t' = "x * x ^^^ 2" then ()

   145 else error "poly.sml Poly.is'_multUnordered doesn't work";

   147 (* 100928 trace_rewrite shows the first occurring difference in 267b:

   148 ###  rls: order_mult_ on: 5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +

   149  (-48 * x ^^^ 4 + 8))

   150 ######  rls: e_rls-is_multUnordered on: p is_multUnordered

   151 #######  try calc: Poly.is'_multUnordered'

   152 =======  calc. to: False  !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!

   153 *)

   154 val t = str2term "5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +  (-48 * x ^^^ 4 + 8))";

   156 "----- is_multUnordered ---";

   157 val tsort = sort_variables t;

   158 term2str tsort = "2 * (5 * (x ^^^ 2 * x ^^^ 7)) + 3 * (5 * x ^^^ 2) + 6 * x ^^^ 7 + 9 +\n-1 * (3 * (6 * (x ^^^ 4 * x ^^^ 5))) +\n-1 * (-1 * (3 * x ^^^ 5)) +\n-48 * x ^^^ 4 +\n8";

   159 is_polyexp t;

   160 tsort = t;

   161 is_polyexp t andalso not (t = sort_variables t);

   162 if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";

   164 "----- eval_is_multUnordered ---";

   165 val tm = str2term "(5 * x ^^^ 2 * (2 * x ^^^ 7) + 5 * x ^^^ 2 * 3 + (6 * x ^^^ 7 + 9) + (-1 * (3 * x ^^^ 5 * (6 * x ^^^ 4)) + -1 * (3 * x ^^^ 5 * -1) +  (-48 * x ^^^ 4 + 8))) is_multUnordered";

   166 case eval_is_multUnordered "testid" "" tm thy of

   167     SOME (_, Const ("HOL.Trueprop", _) $

   168                    (Const ("HOL.eq", _) $

   169                           (Const ("Poly.is'_multUnordered", _) $ _) $

   170                           Const ("HOL.True", _))) => ()

   171   | _ => error "poly.sml diff. eval_is_multUnordered";

   173 "----- rewrite_set_ STILL DIDN'T WORK";

   174 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;

   175 term2str t;

   177 "-------- examples from textbook Schalk I ---------------";

   178 "-------- examples from textbook Schalk I ---------------";

   179 "-------- examples from textbook Schalk I ---------------";

   180 "-----SPB Schalk I p.63 No.267b ---";

   181 val t = str2term "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";

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

   183 if (term2str t) = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"

   184 then () else error "poly.sml: diff.behav. in make_polynomial 1";

   186 "-----SPB Schalk I p.63 No.275b ---";

   187 val t = str2term "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";

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

   189 if (term2str t) = ("3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + " ^

   190   "4 * x * y ^^^ 3 +\n-2 * y ^^^ 4")

   191 then () else error "poly.sml: diff.behav. in make_polynomial 2";

   193 "-----SPB Schalk I p.63 No.279b ---";

   194 val t = str2term "(x-a)*(x-b)*(x-c)*(x-d)";

   195 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   196 if (term2str t) =

   197   ("a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n" ^

   198   "-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n" ^

   199   "-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\n" ^

   200   "c * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4")

   201 then () else error "poly.sml: diff.behav. in make_polynomial 3";

   203 "-----SPB Schalk I p.63 No.291 ---";

   204 val t = str2term "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";

   205 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   206 if (term2str t) = "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"

   207 then () else error "poly.sml: diff.behav. in make_polynomial 4";

   209 "-----SPB Schalk I p.64 No.295c ---";

   210 val t = str2term "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";

   211 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   212 if (term2str t) = ("169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10" ^

   213   " +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18")

   214 then ()else error "poly.sml: diff.behav. in make_polynomial 5";

   216 "-----SPB Schalk I p.64 No.299a ---";

   217 val t = str2term "(x - y)*(x + y)";

   218 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   219 if (term2str t) = "x ^^^ 2 + -1 * y ^^^ 2"

   220 then () else error "poly.sml: diff.behav. in make_polynomial 6";

   222 "-----SPB Schalk I p.64 No.300c ---";

   223 val t = str2term "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";

   224 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   225 if (term2str t) = "-1 + 9 * x ^^^ 4 * y ^^^ 2"

   226 then () else error "poly.sml: diff.behav. in make_polynomial 7";

   228 "-----SPB Schalk I p.64 No.302 ---";

   229 val t = str2term

   230   "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";

   231 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   232 if term2str t = "0"

   233 then () else error "poly.sml: diff.behav. in make_polynomial 8";

   234 (* RL?MG?: Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)

   236 "-----SPB Schalk I p.64 No.306a ---";

   237 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";

   238 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   239 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()

   240 else error "poly.sml: diff.behav. in 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4";

   242 (*WN071729 when reducing "rls reduce_012_" for Schaerding,

   243 the above resulted in the term below ... but reduces from then correctly*)

   244 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";

   245 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   246 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8"

   247 then () else error "poly.sml: diff.behav. in make_polynomial 9b";

   249 "-----SPB Schalk I p.64 No.296a ---";

   250 val t = str2term "(x - a)^^^3";

   251 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   252 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"

   253 then () else error "poly.sml: diff.behav. in make_polynomial 10";

   255 "-----SPB Schalk I p.64 No.296c ---";

   256 val t = str2term "(-3*x - 4*y)^^^3";

   257 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   258 if (term2str t) = "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"

   259 then () else error "poly.sml: diff.behav. in make_polynomial 11";

   261 "-----SPB Schalk I p.62 No.242c ---";

   262 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";

   263 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   264 if (term2str t) = "1"

   265 then () else error "poly.sml: diff.behav. in make_polynomial 12";

   267 "-----SPB Schalk I p.60 No.209a ---";

   268 val t = str2term "a^^^(7-x) * a^^^x";

   269 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   270 if term2str t = "a ^^^ 7"

   271 then () else error "poly.sml: diff.behav. in make_polynomial 13";

   273 "-----SPB Schalk I p.60 No.209d ---";

   274 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";

   275 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   276 if term2str t = "d ^^^ 3"

   277 then () else error "poly.sml: diff.behav. in make_polynomial 14";

   279 (*---------------------------------------------------------------------*)

   280 (*---------------- ?RL?Bsple bei denen es Probleme gibt----------------*)

   281 (*---------------------------------------------------------------------*)

   282 "-----Schalk I p.64 No.303 ---";

   283 val t = str2term "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";

   284 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   285 if term2str t = "1280 * b ^^^ 4"

   286 then () else error "poly.sml: diff.behav. in make_polynomial 14b";

   287 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)

   289 (*--------------------------------------------------------------------*)

   290 (*----------------------- Eigene Beispiele ---------------------------*)

   291 (*--------------------------------------------------------------------*)

   292 "-----SPO ---";

   293 val t = str2term "a^^^2*a^^^(-2)";

   294 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   295 if term2str t = "1" then ()

   296 else error "poly.sml: diff.behav. in make_polynomial 15";

   297 "-----SPO ---";

   298 val t = str2term "a + a + a";

   299 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   300 if term2str t = "3 * a" then ()

   301 else error "poly.sml: diff.behav. in make_polynomial 16";

   302 "-----SPO ---";

   303 val t = str2term "a + b + b + b";

   304 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   305 if term2str t = "a + 3 * b" then ()

   306 else error "poly.sml: diff.behav. in make_polynomial 17";

   307 "-----SPO ---";

   308 val t = str2term "a^^^2*b*b^^^(-1)";

   309 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   310 if term2str t = "a ^^^ 2" then ()

   311 else error "poly.sml: diff.behav. in make_polynomial 18";

   312 "-----SPO ---";

   313 val t = str2term "a^^^2*a^^^(-2)";

   314 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   315 if (term2str t) = "1" then ()

   316 else error "poly.sml: diff.behav. in make_polynomial 19";

   317 "-----SPO ---";

   318 val t = str2term "b + a - b";

   319 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   320 if (term2str t) = "a" then ()

   321 else error "poly.sml: diff.behav. in make_polynomial 20";

   322 "-----SPO ---";

   323 val t = str2term "b * a * a";

   324 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   325 if term2str t = "a ^^^ 2 * b" then ()

   326 else error "poly.sml: diff.behav. in make_polynomial 21";

   327 "-----SPO ---";

   328 val t = str2term "(a^^^2)^^^3";

   329 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   330 if term2str t = "a ^^^ 6" then ()

   331 else error "poly.sml: diff.behav. in make_polynomial 22";

   332 "-----SPO ---";

   333 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";

   334 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   335 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()

   336 else error "poly.sml: diff.behav. in make_polynomial 23";

   337 "-----SPO ---";

   338 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";

   339 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   340 if (term2str t) = "a ^^^ 4" then ()

   341 else error "poly.sml: diff.behav. in make_polynomial 24";

   342 "-----SPO ---";

   343 val t = str2term "a * b * b^^^(-1) + a";

   344 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   345 if (term2str t) = "2 * a" then ()

   346 else error "poly.sml: diff.behav. in make_polynomial 25";

   347 "-----SPO ---";

   348 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";

   349 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;

   350 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"

   351 then () else error "poly.sml: diff.behav. in make_polynomial 26";

   353 (*MG030627 -------------vvv-: Verschachtelte Terme -----------*)

   354 "-----SPO ---";

   355 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";

   356 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   357 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"

   358 then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)

   360 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";

   361 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;

   362 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"

   363 then () else error "poly.sml: diff.behav. in make_polynomial 28";

   365 "-------- check pbl  'polynomial simplification' --------";

   366 "-------- check pbl  'polynomial simplification' --------";

   367 "-------- check pbl  'polynomial simplification' --------";

   368 val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];

   369 "-----0 ---";

   370 case refine fmz ["polynomial","simplification"]of

   371     [Matches (["polynomial", "simplification"], _)] => ()

   372   | _ => error "poly.sml diff.behav. in check pbl, refine";

   373 (*...if there is an error, then ...*)

   375 "-----1 ---";

   376 print_depth 7;

   377 val pbt = get_pbt ["polynomial","simplification"];

   378 print_depth 3;

   379 (*if there is ...

   380 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;

   381 ... then trace_rewrite:*)

   383 "-----2 ---";

   384 trace_rewrite := false;

   385 match_pbl fmz pbt;

   386 trace_rewrite := false;

   387 (*... if there is no rewrite, then there is something wrong with prls*)

   389 "-----3 ---";

   390 print_depth 7;

   391 val prls = (#prls o get_pbt) ["polynomial","simplification"];

   392 print_depth 3;

   393 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";

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

   395 if t' = @{term True} then ()

   396 else error "poly.sml: diff.behav. in check pbl 'polynomial..";

   397 (*... if this works, but --1-- does still NOT work, check types:*)

   399 "-----4 ---";

   400 (*show_types:=true;*)

   401 (*

   402 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;

   403 val wh = [False "(t_::real => real) (is_polyexp::real)"]

   404 ......................^^^^^^^^^^^^...............^^^^*)

   405 val Matches' _ = match_pbl fmz pbt;

   406 (*show_types:=false;*)

   408 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

   409 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

   410 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";

   411 val fmz = ["Term ((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1))", "normalform N"];

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

   413   ("Poly",["polynomial","simplification"],

   414    ["simplification","for_polynomials"]);

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

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

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

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

   419 (writeln o (itms2str_ ctxt)) (get_obj g_pbl pt (fst p));

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

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

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

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

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

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

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

   427 if f2str f = "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"

   428 then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";

   430 "-------- interSteps for Schalk 299a --------------------";

   431 "-------- interSteps for Schalk 299a --------------------";

   432 "-------- interSteps for Schalk 299a --------------------";

   433 states:=[];

   434 CalcTree

   435 [(["Term ((x - y)*(x + (y::real)))", "normalform N"],

   436   ("Poly",["polynomial","simplification"],

   437   ["simplification","for_polynomials"]))];

   438 Iterator 1;

   439 moveActiveRoot 1;

   440 autoCalculate 1 CompleteCalc;

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

   443 interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);

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

   445 if existpt' ([1,1], Frm) pt then ()

   446 else error "poly.sml: interSteps doesnt work again 1";

   448 interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);

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

   450 (*============ inhibit exn WN120316 ==============================================

   451 if existpt' ([1,1,1], Frm) pt then ()

   452 else error "poly.sml: interSteps doesnt work again 2";

   453 ============ inhibit exn WN120316 ==============================================*)

   455 "-------- norm_Poly NOT COMPLETE ------------------------";

   456 "-------- norm_Poly NOT COMPLETE ------------------------";

   457 "-------- norm_Poly NOT COMPLETE ------------------------";

   458 val SOME (f',_) = rewrite_set_ thy false norm_Poly

   459 (str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");

   460 if term2str f' = "L = 2 * 2 * k + oben + 2 * -4 * q + senkrecht"

   461 then ((*norm_Poly NOT COMPLETE -- TODO MG*))

   462 else error "norm_Poly changed behavior";

   464 "-------- ord_make_polynomial ---------------------------";

   465 "-------- ord_make_polynomial ---------------------------";

   466 "-------- ord_make_polynomial ---------------------------";

   467 val t1 = str2term "2 * b + (3 * a + 3 * b)";

   468 val t2 = str2term "3 * a + 3 * b + 2 * b";

   470 if ord_make_polynomial true thy [] (t1, t2) then ()

   471 else error "poly.sml: diff.behav. in ord_make_polynomial";

   473 (*WN071202: ^^^ why then is there no rewriting ...*)

   474 val term = str2term "2*b + (3*a + 3*b)";

   475 val NONE = rewrite_set_ (@{theory "Isac"}) false order_add_mult term;

   477 (*or why is there no rewriting this way...*)

   478 val t1 = str2term "2 * b + (3 * a + 3 * b)";

   479 val t2 = str2term "3 * a + (2 * b + 3 * b)";

author	Walther Neuper <neuper@ist.tugraz.at>
	Mon, 02 Sep 2013 16:16:08 +0200
changeset 52101	c3f399ce32af
parent 48760	5e1e45b3ddef
child 55445	33b0f6db720c
permissions	-rw-r--r--