1.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Sep 28 13:30:29 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly.sml Fri Oct 01 10:23:38 2010 +0200
1.3 @@ -16,17 +16,21 @@
1.4 "--------------------------------------------------------";
1.5 "-------- check is'_polyexp is_polyexp ------------------";
1.6 "-------- build Script Expand_binoms --------------------";
1.7 -"-------- investigate new uniary minus ------------------";
1.8 -"-------- Bsple aus Schalk I ----------------------------";
1.9 +"-------- investigate (new) uniary minus ----------------";
1.10 +"-------- check make_polynomial with simple terms -------";
1.11 +"-------- fun is_multUnordered --------------------------";
1.12 +"-------- examples from textbook Schalk I ---------------";
1.13 "-------- Script 'simplification for_polynomials' -------";
1.14 "-------- check pbl 'polynomial simplification' --------";
1.15 "-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.16 +"-------- interSteps for Schalk 299a --------------------";
1.17 "-------- norm_Poly NOT COMPLETE ------------------------";
1.18 "-------- ord_make_polynomial ---------------------------";
1.19 "--------------------------------------------------------";
1.20 "--------------------------------------------------------";
1.21 "--------------------------------------------------------";
1.22
1.23 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.24
1.25 "-------- check is'_polyexp is_polyexp ------------------";
1.26 "-------- check is'_polyexp is_polyexp ------------------";
1.27 @@ -35,7 +39,6 @@
1.28 then error "poly.sml: check is'_polyexp is_polyexp" else ();
1.29
1.30
1.31 -(*===== inhibit exn ?===========================================================
1.32 "-------- build Script Expand_binoms -----------------------------";
1.33 "-------- build Script Expand_binoms -----------------------------";
1.34 "-------- build Script Expand_binoms -----------------------------";
1.35 @@ -72,18 +75,19 @@
1.36 " (Try (Repeat (Calculate TIMES ))) @@ " ^
1.37 " (Try (Repeat (Calculate POWER)))) " ^
1.38 " t_t)";
1.39 +(*
1.40 val scr_expand_binoms =
1.41 "Script Expand_binoms t_t = t_t";
1.42 -
1.43 +*)
1.44 val ---------------------------------------------- = "11111";
1.45 parse thy scr_expand_binoms;
1.46 val ---------------------------------------------- = "22222";
1.47 -(*----------------------------------------------
1.48
1.49 -"-------- investigate new uniary minus ---------------------------";
1.50 -"-------- investigate new uniary minus ---------------------------";
1.51 -"-------- investigate new uniary minus ---------------------------";
1.52 -val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
1.53 +
1.54 +"-------- investigate (new) uniary minus ----------------";
1.55 +"-------- investigate (new) uniary minus ----------------";
1.56 +"-------- investigate (new) uniary minus ----------------";
1.57 +val t = (#prop o rep_thm) @{thm real_diff_0}; (*"0 - ?x = - ?x"*)
1.58 atomty t;
1.59 (*** -------------
1.60 *** Const ( Trueprop, bool => prop)
1.61 @@ -117,20 +121,180 @@
1.62 (**** -------------
1.63 *** Free ( -x, real)*)
1.64
1.65 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.66 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.67
1.68 -"-------- Bsple aus Schalk I -------------------------------------";
1.69 -"-------- Bsple aus Schalk I -------------------------------------";
1.70 -"-------- Bsple aus Schalk I -------------------------------------";
1.71 -(*SPB Schalk I p.63 No.267b*)
1.72 +"-------- check make_polynomial with simple terms -------";
1.73 +"-------- check make_polynomial with simple terms -------";
1.74 +"-------- check make_polynomial with simple terms -------";
1.75 +"----- check 1 ---";
1.76 +val t = str2term "2*3*a";
1.77 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.78 +if term2str t = "6 * a" then () else error "check make_polynomial 1";
1.79 +
1.80 +"----- check 2 ---";
1.81 +val t = str2term "2*a + 3*a";
1.82 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.83 +if term2str t = "5 * a" then () else error "check make_polynomial 2";
1.84 +
1.85 +"----- check 3 ---";
1.86 +val t = str2term "2*a + 3*a + 3*a";
1.87 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.88 +if term2str t = "8 * a" then () else error "check make_polynomial 3";
1.89 +
1.90 +"----- check 4 ---";
1.91 +val t = str2term "3*a - 2*a";
1.92 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.93 +if term2str t = "a" then () else error "check make_polynomial 4";
1.94 +
1.95 +"----- check 5 ---";
1.96 +val t = str2term "4*(3*a - 2*a)";
1.97 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.98 +if term2str t = "4 * a" then () else error "check make_polynomial 5";
1.99 +
1.100 +"----- check 6 ---";
1.101 +val t = str2term "4*(3*a^^^2 - 2*a^^^2)";
1.102 +val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
1.103 +if term2str t = "4 * a ^^^ 2" then () else error "check make_polynomial 6";
1.104 +
1.105 +
1.106 +"-------- fun is_multUnordered --------------------------";
1.107 +"-------- fun is_multUnordered --------------------------";
1.108 +"-------- fun is_multUnordered --------------------------";
1.109 +val thy = theory "Isac";
1.110 +(* 100928 trace_rewrite gives the following (first occurring) difference:
1.111 +:
1.112 +### 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) +
1.113 + (-48 * x ^^^ 4 + 8))
1.114 +###### rls: e_rls-is_multUnordered on: p is_multUnordered
1.115 +####### try calc: Poly.is'_multUnordered'
1.116 +======= calc. to: False !!!!!!!!!!!!! INSTEAD OF TRUE in 2002 !!!!!!!!!!!!!
1.117 +*)
1.118 +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))";
1.119 +
1.120 +"----- is_multUnordered ---";
1.121 +val tsort = sort_variables t;
1.122 +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";
1.123 +is_polyexp t;
1.124 +tsort = t;
1.125 +is_polyexp t andalso not (t = sort_variables t);
1.126 +if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 1";
1.127 +
1.128 +"----- eval_is_multUnordered ---";
1.129 +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";
1.130 +case eval_is_multUnordered "testid" "" tm thy of
1.131 + SOME (_, Const ("Trueprop", _) $
1.132 + (Const ("op =", _) $
1.133 + (Const ("Poly.is'_multUnordered", _) $ _) $
1.134 + Const ("True", _))) => ()
1.135 + | _ => error "poly.sml diff. eval_is_multUnordered";
1.136 +
1.137 +"----- rewrite_set_ ---";
1.138 +(*fixme*)val NONE = rewrite_set_ thy true order_mult_ tm; (*fixme*)
1.139 +
1.140 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.141 +
1.142 +
1.143 +"===== take simpler testdata ===";
1.144 +val t = str2term "x^^^2 * x";
1.145 +if is_multUnordered t then () else error "poly.sml diff. is_multUnordered 2";
1.146 +val tm = str2term "(x^^^2 * x) is_multUnordered";
1.147 +case eval_is_multUnordered "testid" "" tm thy of
1.148 + SOME (_, Const ("Trueprop", _) $
1.149 + (Const ("op =", _) $
1.150 + (Const ("Poly.is'_multUnordered", _) $ _) $
1.151 + Const ("True", _))) => ()
1.152 + | _ => error "poly.sml diff. eval_is_multUnordered 2";
1.153 +
1.154 +(*fixme val NONE = rewrite_set_ thy true order_mult_ tm;*)
1.155 +"----- rewrite__set_ ---";
1.156 +val (thy, i, _, _, (rrls as Rrls _), t) = (thy, 0, true, [], order_mult_, tm);
1.157 + val (t', asm, rew) = app_rev thy (i+1) rrls t;
1.158 +"----- app_rev ---";
1.159 +val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.160 + fun chk_prepat thy erls [] t = true
1.161 + | chk_prepat thy erls prepat t =
1.162 + let fun chk (pres, pat) =
1.163 + (let val subst: Type.tyenv * Envir.tenv =
1.164 + Pattern.match thy (pat, t)
1.165 + (Vartab.empty, Vartab.empty)
1.166 + in snd (eval__true thy (i+1)
1.167 + (map (Envir.subst_term subst) pres)
1.168 + [] erls)
1.169 + end)
1.170 + handle _ => false
1.171 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.172 + | scan_ f (pp::pps) = if f pp then true
1.173 + else scan_ f pps;
1.174 + in scan_ chk prepat end;
1.175 +
1.176 + (*.apply the normal_form of a rev-set.*)
1.177 + fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
1.178 + if chk_prepat thy erls prepat t
1.179 + then ((*tracing("### app_rev': t = "^(term2str t));*)
1.180 + normal_form t)
1.181 + else NONE;
1.182 +(*fixme val NONE = app_rev' thy rrls t;*)
1.183 +"----- app_rev' ---";
1.184 +val (thy, Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}, t) = (thy, rrls, t);
1.185 +(*fixme false*) chk_prepat thy erls prepat t;
1.186 +"----- chk_prepat ---";
1.187 +val (thy, erls, prepat, t) = (thy, erls, prepat, t);
1.188 + fun chk (pres, pat) =
1.189 + (let val subst: Type.tyenv * Envir.tenv =
1.190 + Pattern.match thy (pat, t)
1.191 + (Vartab.empty, Vartab.empty)
1.192 + in snd (eval__true thy (i+1)
1.193 + (map (Envir.subst_term subst) pres)
1.194 + [] erls)
1.195 + end)
1.196 + handle _ => false;
1.197 + fun scan_ f [] = false (*scan_ NEVER called by []*)
1.198 + | scan_ f (pp::pps) = if f pp then true
1.199 + else scan_ f pps;
1.200 +tracing "=== poly.sml: scan_ chk prepat begin";
1.201 +scan_ chk prepat;
1.202 +tracing "=== poly.sml: scan_ chk prepat end";
1.203 +
1.204 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.205 +
1.206 +"----- chk ---";
1.207 +val [(pres, pat)] = prepat;
1.208 + val subst: Type.tyenv * Envir.tenv =
1.209 + Pattern.match thy (pat, t)
1.210 + (Vartab.empty, Vartab.empty);
1.211 +(*fixme: asms = ["p is_multUnordered"]...instantiate*)
1.212 +"----- eval__true ---";
1.213 +val asms = (map (Envir.subst_term subst) pres);
1.214 +val (thy, i, asms, bdv, rls) =
1.215 + (thy, (i+1), [str2term "(x^^^2 * x) is_multUnordered"],
1.216 + [] : (term * term) list, erls);
1.217 +case eval__true thy i asms bdv rls of
1.218 + ([], true) => ()
1.219 + | _ => error "poly.sml: diff. is_multUnordered, eval__true";
1.220 +
1.221 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.222 +
1.223 +(*===== inhibit exn ?===========================================================
1.224 +
1.225 +
1.226 +
1.227 +"-------- examples from textbook Schalk I ---------------";
1.228 +"-------- examples from textbook Schalk I ---------------";
1.229 +"-------- examples from textbook Schalk I ---------------";
1.230 +"-----SPB Schalk I p.63 No.267b ---";
1.231 +trace_rewrite := true; tracing "-----SPB Schalk I p.63 No.267b ---begin";
1.232 val t = str2term
1.233 "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
1.234 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.235 +term2str t;
1.236 +trace_rewrite := false; tracing "-----SPB Schalk I p.63 No.267b ---end";
1.237 if (term2str t) =
1.238 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
1.239 then ()
1.240 else error "poly.sml: diff.behav. in make_polynomial 1";
1.241
1.242 -(*SPB Schalk I p.63 No.275b*)
1.243 +"-----SPB Schalk I p.63 No.275b ---";
1.244 val t = str2term
1.245 "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
1.246 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.247 @@ -141,7 +305,7 @@
1.248 then ()
1.249 else error "poly.sml: diff.behav. in make_polynomial 2";
1.250
1.251 -(*SPB Schalk I p.63 No.279b*)
1.252 +"-----SPB Schalk I p.63 No.279b ---";
1.253 val t = str2term
1.254 "(x-a)*(x-b)*(x-c)*(x-d)";
1.255 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.256 @@ -152,7 +316,7 @@
1.257 then ()
1.258 else error "poly.sml: diff.behav. in make_polynomial 3";
1.259
1.260 -(*SPB Schalk I p.63 No.291*)
1.261 +"-----SPB Schalk I p.63 No.291 ---";
1.262 val t = str2term
1.263 "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
1.264 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.265 @@ -162,7 +326,7 @@
1.266 then ()
1.267 else error "poly.sml: diff.behav. in make_polynomial 4";
1.268
1.269 -(*SPB Schalk I p.64 No.295c*)
1.270 +"-----SPB Schalk I p.64 No.295c ---";
1.271 val t = str2term
1.272 "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
1.273 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.274 @@ -173,17 +337,17 @@
1.275 then ()
1.276 else error "poly.sml: diff.behav. in make_polynomial 5";
1.277
1.278 -(*SPB Schalk I p.64 No.299a*)
1.279 +"-----SPB Schalk I p.64 No.299a ---";
1.280 val t = str2term
1.281 "(x - y)*(x + y)";
1.282 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.283 term2str t;
1.284 -if (term2str t) =
1.285 -"x ^^^ 2 + -1 * y ^^^ 2"
1.286 -then ()
1.287 +(*
1.288 +if (term2str t) = "x ^^^ 2 + -1 * y ^^^ 2" then ()
1.289 else error "poly.sml: diff.behav. in make_polynomial 6";
1.290 +*)
1.291
1.292 -(*SPB Schalk I p.64 No.300c*)
1.293 +"-----SPB Schalk I p.64 No.300c ---";
1.294 val t = str2term
1.295 "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
1.296 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.297 @@ -193,7 +357,7 @@
1.298 then ()
1.299 else error "poly.sml: diff.behav. in make_polynomial 7";
1.300
1.301 -(*SPB Schalk I p.64 No.302*)
1.302 +"-----SPB Schalk I p.64 No.302 ---";
1.303 val t = str2term
1.304 "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
1.305 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.306 @@ -202,7 +366,7 @@
1.307 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
1.308
1.309
1.310 -(*SPB Schalk I p.64 No.306a*)
1.311 +"-----SPB Schalk I p.64 No.306a ---";
1.312 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
1.313 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.314 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
1.315 @@ -217,32 +381,32 @@
1.316 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
1.317 else error "poly.sml: diff.behav. in make_polynomial 9b";
1.318
1.319 -(*SPB Schalk I p.64 No.296a*)
1.320 +"-----SPB Schalk I p.64 No.296a ---";
1.321 val t = str2term "(x - a)^^^3";
1.322 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.323 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
1.324 then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.325
1.326 -(*SPB Schalk I p.64 No.296c*)
1.327 +"-----SPB Schalk I p.64 No.296c ---";
1.328 val t = str2term "(-3*x - 4*y)^^^3";
1.329 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.330 if (term2str t) =
1.331 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
1.332 then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.333
1.334 -(*SPB Schalk I p.62 No.242c*)
1.335 +"-----SPB Schalk I p.62 No.242c ---";
1.336 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
1.337 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.338 if (term2str t) = "1" then ()
1.339 else error "poly.sml: diff.behav. in make_polynomial 12";
1.340
1.341 -(*SPB Schalk I p.60 No.209a*)
1.342 +"-----SPB Schalk I p.60 No.209a ---";
1.343 val t = str2term "a^^^(7-x) * a^^^x";
1.344 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.345 if term2str t = "a ^^^ 7" then ()
1.346 else error "poly.sml: diff.behav. in make_polynomial 13";
1.347
1.348 -(*SPB Schalk I p.60 No.209d*)
1.349 +"-----SPB Schalk I p.60 No.209d ---";
1.350 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
1.351 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.352 if term2str t = "d ^^^ 3" then ()
1.353 @@ -253,7 +417,7 @@
1.354 (*------------------ Bsple bei denen es Probleme gibt------------------*)
1.355 (*---------------------------------------------------------------------*)
1.356
1.357 -(*Schalk I p.64 No.303*)
1.358 +"-----Schalk I p.64 No.303 ---";
1.359 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)";
1.360 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.361 if term2str t = "1280 * b ^^^ 4" then ()
1.362 @@ -264,62 +428,62 @@
1.363 (*--------------------------------------------------------------------*)
1.364 (*----------------------- Eigene Beispiele ---------------------------*)
1.365 (*--------------------------------------------------------------------*)
1.366 -(*SPO*)
1.367 +"-----SPO ---";
1.368 val t = str2term "a^^^2*a^^^(-2)";
1.369 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.370 if term2str t = "1" then ()
1.371 else error "poly.sml: diff.behav. in make_polynomial 15";
1.372 -(*SPO*)
1.373 +"-----SPO ---";
1.374 val t = str2term "a + a + a";
1.375 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.376 if term2str t = "3 * a" then ()
1.377 else error "poly.sml: diff.behav. in make_polynomial 16";
1.378 -(*SPO*)
1.379 +"-----SPO ---";
1.380 val t = str2term "a + b + b + b";
1.381 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.382 if term2str t = "a + 3 * b" then ()
1.383 else error "poly.sml: diff.behav. in make_polynomial 17";
1.384 -(*SPO*)
1.385 +"-----SPO ---";
1.386 val t = str2term "a^^^2*b*b^^^(-1)";
1.387 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.388 if term2str t = "a ^^^ 2" then ()
1.389 else error "poly.sml: diff.behav. in make_polynomial 18";
1.390 -(*SPO*)
1.391 +"-----SPO ---";
1.392 val t = str2term "a^^^2*a^^^(-2)";
1.393 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.394 if (term2str t) = "1" then ()
1.395 else error "poly.sml: diff.behav. in make_polynomial 19";
1.396 -(*SPO*)
1.397 +"-----SPO ---";
1.398 val t = str2term "b + a - b";
1.399 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.400 if (term2str t) = "a" then ()
1.401 else error "poly.sml: diff.behav. in make_polynomial 20";
1.402 -(*SPO*)
1.403 +"-----SPO ---";
1.404 val t = str2term "b * a * a";
1.405 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.406 if term2str t = "a ^^^ 2 * b" then ()
1.407 else error "poly.sml: diff.behav. in make_polynomial 21";
1.408 -(*SPO*)
1.409 +"-----SPO ---";
1.410 val t = str2term "(a^^^2)^^^3";
1.411 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.412 if term2str t = "a ^^^ 6" then ()
1.413 else error "poly.sml: diff.behav. in make_polynomial 22";
1.414 -(*SPO*)
1.415 +"-----SPO ---";
1.416 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
1.417 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.418 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
1.419 else error "poly.sml: diff.behav. in make_polynomial 23";
1.420 -(*SPO*)
1.421 +"-----SPO ---";
1.422 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
1.423 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.424 if (term2str t) = "a ^^^ 4" then ()
1.425 else error "poly.sml: diff.behav. in make_polynomial 24";
1.426 -(*SPO*)
1.427 +"-----SPO ---";
1.428 val t = str2term "a * b * b^^^(-1) + a";
1.429 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.430 if (term2str t) = "2 * a" then ()
1.431 else error "poly.sml: diff.behav. in make_polynomial 25";
1.432 -(*SPO*)
1.433 +"-----SPO ---";
1.434 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
1.435 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.436 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
1.437 @@ -327,7 +491,7 @@
1.438
1.439
1.440 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
1.441 -(*SPO*)
1.442 +"-----SPO ---";
1.443 val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
1.444 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.445 term2str t;
1.446 @@ -339,9 +503,9 @@
1.447 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
1.448 then () else error "poly.sml: diff.behav. in make_polynomial 28";
1.449
1.450 -"-------- Script 'simplification for_polynomials' ----------------";
1.451 -"-------- Script 'simplification for_polynomials' ----------------";
1.452 -"-------- Script 'simplification for_polynomials' ----------------";
1.453 +"-------- Script 'simplification for_polynomials' -------";
1.454 +"-------- Script 'simplification for_polynomials' -------";
1.455 +"-------- Script 'simplification for_polynomials' -------";
1.456 val str =
1.457 "Script SimplifyScript (t_::real) = \
1.458 \ ((Rewrite_Set norm_Poly False) t_)";
1.459 @@ -349,19 +513,19 @@
1.460 atomty sc;
1.461
1.462
1.463 -"-------- check pbl 'polynomial simplification' -----------------";
1.464 -"-------- check pbl 'polynomial simplification' -----------------";
1.465 -"-------- check pbl 'polynomial simplification' -----------------";
1.466 +"-------- check pbl 'polynomial simplification' --------";
1.467 +"-------- check pbl 'polynomial simplification' --------";
1.468 +"-------- check pbl 'polynomial simplification' --------";
1.469 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
1.470 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
1.471 "normalform N"];
1.472 -(*0*)
1.473 +"-----0 ---";
1.474 case refine fmz ["polynomial","simplification"]of
1.475 [Matches (["polynomial", "simplification"], _)] => ()
1.476 | _ => error "poly.sml diff.behav. in check pbl, refine";
1.477 (*...if there is an error, then ...*)
1.478
1.479 -(*1*)
1.480 +"-----1 ---";
1.481 print_depth 7;
1.482 val pbt = get_pbt ["polynomial","simplification"];
1.483 print_depth 3;
1.484 @@ -369,13 +533,13 @@
1.485 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
1.486 ... then trace_rewrite:*)
1.487
1.488 -(*2*)
1.489 +"-----2 ---";
1.490 trace_rewrite:=true;
1.491 match_pbl fmz pbt;
1.492 trace_rewrite:=false;
1.493 (*... if there is no rewrite, then there is something wrong with prls*)
1.494
1.495 -(*3*)
1.496 +"-----3 ---";
1.497 print_depth 7;
1.498 val prls = (#prls o get_pbt) ["polynomial","simplification"];
1.499 print_depth 3;
1.500 @@ -388,7 +552,7 @@
1.501 else error "poly.sml: diff.behav. in check pbl 'polynomial..";
1.502 (*... if this works, but (*1*) does still NOT work, check types:*)
1.503
1.504 -(*4*)
1.505 +"-----4 ---";
1.506 show_types:=true;
1.507 (*
1.508 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
1.509 @@ -398,9 +562,9 @@
1.510 show_types:=false;
1.511
1.512
1.513 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
1.514 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
1.515 -"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
1.516 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.517 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.518 +"-------- me 'poly. simpl.' Schalk I p.63 No.267b -------";
1.519 val fmz = ["TERM ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
1.520 \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
1.521 "normalform N"];
1.522 @@ -424,9 +588,9 @@
1.523 then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
1.524
1.525
1.526 -"-------- interSteps for Schalk 299a -----------------------------";
1.527 -"-------- interSteps for Schalk 299a -----------------------------";
1.528 -"-------- interSteps for Schalk 299a -----------------------------";
1.529 +"-------- interSteps for Schalk 299a --------------------";
1.530 +"-------- interSteps for Schalk 299a --------------------";
1.531 +"-------- interSteps for Schalk 299a --------------------";
1.532 states:=[];
1.533 CalcTree
1.534 [(["TERM ((x - y)*(x + y))", "normalform N"],
1.535 @@ -448,18 +612,19 @@
1.536 else error "poly.sml: interSteps doesnt work again 2";
1.537
1.538
1.539 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
1.540 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
1.541 -"-------- norm_Poly NOT COMPLETE ---------------------------------";
1.542 +"-------- norm_Poly NOT COMPLETE ------------------------";
1.543 +"-------- norm_Poly NOT COMPLETE ------------------------";
1.544 +"-------- norm_Poly NOT COMPLETE ------------------------";
1.545 trace_rewrite:=true;
1.546 val SOME (f',_) = rewrite_set_ thy false norm_Poly
1.547 (str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben")(*see poly.sml: -- norm_Poly NOT COMPLETE -- TODO MG*);
1.548 trace_rewrite:=false;
1.549 term2str f';
1.550
1.551 -"-------- ord_make_polynomial ------------------------------------";
1.552 -"-------- ord_make_polynomial ------------------------------------";
1.553 -"-------- ord_make_polynomial ------------------------------------";
1.554 +
1.555 +"-------- ord_make_polynomial ---------------------------";
1.556 +"-------- ord_make_polynomial ---------------------------";
1.557 +"-------- ord_make_polynomial ---------------------------";
1.558 val t1 = str2term "2 * b + (3 * a + 3 * b)";
1.559 val t2 = str2term "3 * a + 3 * b + 2 * b";
1.560
1.561 @@ -475,5 +640,4 @@
1.562 val t2 = str2term "3 * a + (2 * b + 3 * b)";
1.563
1.564
1.565 -----------------------------------------------*)
1.566 ===== inhibit exn ?===========================================================*)