1.1 --- a/src/sml/IsacKnowledge/Diff.thy Mon Dec 03 15:54:09 2007 +0100
1.2 +++ b/src/sml/IsacKnowledge/Diff.thy Mon Dec 03 15:59:34 2007 +0100
1.3 @@ -13,6 +13,11 @@
1.4
1.5 d_d :: "[real, real]=> real"
1.6 sin, cos :: "real => real"
1.7 +(*
1.8 + log, ln :: "real => real"
1.9 + nlog :: "[real, real] => real"
1.10 + exp :: "real => real" ("E'_ ^^^ _" 80)
1.11 +*)
1.12 (*descriptions in the related problems*)
1.13 derivativeEq :: bool => una
1.14
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/smltest/IsacKnowledge/poly.sml Mon Dec 03 15:59:34 2007 +0100
2.3 @@ -0,0 +1,478 @@
2.4 +(* testexamples for Poly, polynomials
2.5 + author: Matthias Goldgruber 2003
2.6 + (c) due to copyright terms
2.7 +
2.8 +use"../smltest/IsacKnowledge/poly.sml";
2.9 +use"poly.sml";
2.10 +****************************************************************.*)
2.11 +
2.12 +(******************************************************************
2.13 + WN060104 'SPB' came into 'exp_IsacCore_Simp_Poly_Book.xml'
2.14 + 'SPO' came into 'exp_IsacCore_Simp_Poly_Other.xml'
2.15 +*******************************************************************)
2.16 +"-----------------------------------------------------------------";
2.17 +"table of contents -----------------------------------------------";
2.18 +"-----------------------------------------------------------------";
2.19 +"-------- investigate new uniary minus ---------------------------";
2.20 +"-------- Bsple aus Schalk I -------------------------------------";
2.21 +"-------- Script 'simplification for_polynomials' ----------------";
2.22 +"-------- check pbl 'polynomial simplification' -----------------";
2.23 +"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
2.24 +"-------- norm_Poly NOT COMPLETE ---------------------------------";
2.25 +"-------- ord_make_polynomial ------------------------------------";
2.26 +"-----------------------------------------------------------------";
2.27 +"-----------------------------------------------------------------";
2.28 +"-----------------------------------------------------------------";
2.29 +
2.30 +
2.31 +"-------- investigate new uniary minus ---------------------------";
2.32 +"-------- investigate new uniary minus ---------------------------";
2.33 +"-------- investigate new uniary minus ---------------------------";
2.34 +val t = (#prop o rep_thm) real_diff_0; (*"0 - ?x = - ?x"*)
2.35 +atomty t;
2.36 +(*** -------------
2.37 +*** Const ( Trueprop, bool => prop)
2.38 +*** . Const ( op =, [real, real] => bool)
2.39 +*** . . Const ( op -, [real, real] => real)
2.40 +*** . . . Const ( 0, real)
2.41 +*** . . . Var ((x, 0), real)
2.42 +*** . . Const ( uminus, real => real)
2.43 +*** . . . Var ((x, 0), real) *)
2.44 +
2.45 +val t = (term_of o the o (parse thy)) "-1";
2.46 +atomty t;
2.47 +(*** -------------
2.48 +*** Free ( -1, real) *)
2.49 +val t = (term_of o the o (parse thy)) "- 1";
2.50 +atomty t;
2.51 +(*** -------------
2.52 +*** Const ( uminus, real => real)
2.53 +*** . Free ( 1, real) *)
2.54 +
2.55 +val t = (term_of o the o (parse thy)) "-x"; (*1-x syntyx error !!!*)
2.56 +atomty t;
2.57 +(**** -------------
2.58 +*** Free ( -x, real)*)
2.59 +val t = (term_of o the o (parse thy)) "- x";
2.60 +atomty t;
2.61 +(**** -------------
2.62 +*** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
2.63 +val t = (term_of o the o (parse thy)) "-(x)";
2.64 +atomty t;
2.65 +(**** -------------
2.66 +*** Free ( -x, real)*)
2.67 +
2.68 +
2.69 +"-------- Bsple aus Schalk I -------------------------------------";
2.70 +"-------- Bsple aus Schalk I -------------------------------------";
2.71 +"-------- Bsple aus Schalk I -------------------------------------";
2.72 +(*SPB Schalk I p.63 No.267b*)
2.73 + val t = str2term
2.74 + "(5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)";
2.75 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.76 + term2str t;
2.77 +if (term2str t) =
2.78 +"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
2.79 +then ()
2.80 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.81 +
2.82 +(*SPB Schalk I p.63 No.275b*)
2.83 + val t = str2term
2.84 + "(3*x^^^2 - 2*x*y + y^^^2) * (x^^^2 - 2*y^^^2)";
2.85 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.86 + term2str t;
2.87 +if (term2str t) =
2.88 +"3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
2.89 +\4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
2.90 +then ()
2.91 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.92 +
2.93 +(*SPB Schalk I p.63 No.279b*)
2.94 + val t = str2term
2.95 + "(x-a)*(x-b)*(x-c)*(x-d)";
2.96 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.97 + term2str t;
2.98 +(* Richtig! *)
2.99 +if (term2str t) =
2.100 +"a * b * c * d + -1 * a * b * c * x + -1 * a * b * d * x + a * b * x ^^^ 2 +\n-1 * a * c * d * x +\na * c * x ^^^ 2 +\na * d * x ^^^ 2 +\n-1 * a * x ^^^ 3 +\n-1 * b * c * d * x +\nb * c * x ^^^ 2 +\nb * d * x ^^^ 2 +\n-1 * b * x ^^^ 3 +\nc * d * x ^^^ 2 +\n-1 * c * x ^^^ 3 +\n-1 * d * x ^^^ 3 +\nx ^^^ 4"
2.101 +then ()
2.102 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.103 +
2.104 +(*SPB Schalk I p.63 No.291*)
2.105 + val t = str2term
2.106 + "(5+96*x^^^3+8*x*(-4+(7- 3*x)*4*x))*(5*(2- 3*x)- (-15*x*(-8*x- 5)))";
2.107 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.108 + term2str t;
2.109 +if (term2str t) =
2.110 +"50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
2.111 +then ()
2.112 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.113 +
2.114 +(*SPB Schalk I p.64 No.295c*)
2.115 + val t = str2term
2.116 + "(13*a^^^4*b^^^9*c - 12*a^^^3*b^^^6*c^^^9)^^^2";
2.117 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.118 + term2str t;
2.119 +if (term2str t) =
2.120 +"169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
2.121 +\ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
2.122 +then ()
2.123 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.124 +
2.125 +(*SPB Schalk I p.64 No.299a*)
2.126 + val t = str2term
2.127 + "(x - y)*(x + y)";
2.128 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.129 + term2str t;
2.130 +if (term2str t) =
2.131 +"x ^^^ 2 + -1 * y ^^^ 2"
2.132 +then ()
2.133 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.134 +
2.135 +(*SPB Schalk I p.64 No.300c*)
2.136 + val t = str2term
2.137 + "(3*x^^^2*y - 1)*(3*x^^^2*y + 1)";
2.138 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.139 + term2str t;
2.140 +if (term2str t) =
2.141 +"-1 + 9 * x ^^^ 4 * y ^^^ 2"
2.142 +then ()
2.143 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.144 +
2.145 +(*SPB Schalk I p.64 No.302*)
2.146 + val t = str2term
2.147 + "(13*x^^^2 + 5)*(13*x^^^2 - 5) - (5*x^^^2 + 3)*(5*x^^^2 - 3) - (12*x^^^2 + 4)*(12*x^^^2 - 4)";
2.148 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.149 + term2str t;
2.150 +if (term2str t) =
2.151 +"0"
2.152 +then ()
2.153 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.154 +(* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
2.155 +
2.156 +
2.157 +(*SPB Schalk I p.64 No.306a*)
2.158 + val t = str2term
2.159 + "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
2.160 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.161 + term2str t;
2.162 +if (term2str t) =
2.163 +"1 + -2 * x ^^^ 4 + x ^^^ 8"
2.164 +then ()
2.165 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.166 +
2.167 +(*SPB Schalk I p.64 No.296a*)
2.168 + val t = str2term
2.169 + "(x - a)^^^3";
2.170 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.171 + term2str t;
2.172 +if (term2str t) =
2.173 +"-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
2.174 +then ()
2.175 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.176 +
2.177 +(*SPB Schalk I p.64 No.296c*)
2.178 + val t = str2term
2.179 + "(-3*x - 4*y)^^^3";
2.180 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.181 + term2str t;
2.182 +if (term2str t) =
2.183 +"-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
2.184 +then ()
2.185 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.186 +
2.187 +(*SPB Schalk I p.62 No.242c*)
2.188 + val t = str2term
2.189 + "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
2.190 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.191 + term2str t;
2.192 +if (term2str t) =
2.193 +"1"
2.194 +then ()
2.195 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.196 +
2.197 +(*SPB Schalk I p.60 No.209a*)
2.198 + val t = str2term
2.199 + "a^^^(7-x) * a^^^x";
2.200 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.201 + term2str t;
2.202 +if (term2str t) =
2.203 +"a ^^^ 7"
2.204 +then ()
2.205 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.206 +
2.207 +(*SPB Schalk I p.60 No.209d*)
2.208 + val t = str2term
2.209 + "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
2.210 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.211 + term2str t;
2.212 +if (term2str t) =
2.213 +"d ^^^ 3"
2.214 +then ()
2.215 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.216 +
2.217 +
2.218 +(*---------------------------------------------------------------------*)
2.219 +(*------------------ Bsple bei denen es Probleme gibt------------------*)
2.220 +(*---------------------------------------------------------------------*)
2.221 +
2.222 +(*Schalk I p.64 No.303*)
2.223 + val t = str2term
2.224 + "(a + 2*b)*(a^^^2 + 4*b^^^2)*(a - 2*b) - (a - 6*b)*(a^^^2 + 36*b^^^2)*(a + 6*b)";
2.225 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.226 + term2str t;
2.227 +"1280 * b ^^^ 4";
2.228 +(* Richtig - aber Binomische Formel wurde nicht verwendet! *)
2.229 +
2.230 +
2.231 +(*--------------------------------------------------------------------*)
2.232 +(*----------------------- Eigene Beispiele ---------------------------*)
2.233 +(*--------------------------------------------------------------------*)
2.234 +(*SPO*)
2.235 +val t = str2term "a^^^2*a^^^(-2)";
2.236 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.237 + term2str t;
2.238 +if (term2str t) =
2.239 +"1"
2.240 +then ()
2.241 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.242 +(*SPO*)
2.243 +val t = str2term "a + a + a";
2.244 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.245 + term2str t;
2.246 +if (term2str t) =
2.247 +"3 * a"
2.248 +then ()
2.249 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.250 +(*SPO*)
2.251 +val t = str2term "a + b + b + b";
2.252 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.253 + term2str t;
2.254 +if (term2str t) =
2.255 +"a + 3 * b"
2.256 +then ()
2.257 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.258 +(*SPO*)
2.259 +val t = str2term "a^^^2*b*b^^^(-1)";
2.260 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.261 + term2str t;
2.262 +if (term2str t) =
2.263 +"a ^^^ 2"
2.264 +then ()
2.265 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.266 +(*SPO*)
2.267 +val t = str2term "a^^^2*a^^^(-2)";
2.268 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.269 + term2str t;
2.270 +if (term2str t) =
2.271 +"1"
2.272 +then ()
2.273 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.274 +(*SPO*)
2.275 +val t = str2term "b + a - b";
2.276 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.277 + term2str t;
2.278 +if (term2str t) =
2.279 +"a"
2.280 +then ()
2.281 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.282 +(*SPO*)
2.283 +val t = (term_of o the o (parse thy)) "b * a * a";
2.284 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.285 +term2str t;
2.286 +if (term2str t) =
2.287 +"a ^^^ 2 * b"
2.288 +then ()
2.289 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.290 +(*SPO*)
2.291 +val t = str2term "(a^^^2)^^^3";
2.292 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.293 +term2str t;
2.294 +if (term2str t) =
2.295 +"a ^^^ 6"
2.296 +then ()
2.297 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.298 +(*SPO*)
2.299 +val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
2.300 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.301 +term2str t;
2.302 +if (term2str t) =
2.303 +"x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2"
2.304 +then ()
2.305 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.306 +(*SPO*)
2.307 +val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
2.308 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.309 +term2str t;
2.310 +if (term2str t) =
2.311 +"a ^^^ 4"
2.312 +then ()
2.313 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.314 +(*SPO*)
2.315 +val t = str2term "a * b * b^^^(-1) + a";
2.316 +val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.317 +term2str t;
2.318 +if (term2str t) =
2.319 +"2 * a"
2.320 +then ()
2.321 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.322 +(*SPO*)
2.323 +val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
2.324 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.325 + term2str t;
2.326 +if (term2str t) =
2.327 +"3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
2.328 +then ()
2.329 +else raise error "poly.sml: diff.behav. in make_polynomial";
2.330 +
2.331 +
2.332 +(*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
2.333 +(*SPO*)
2.334 +val t = str2term "(1 + (x*y*a) + x)^^^(1 + (x*y*a) + x)";
2.335 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.336 + term2str t;
2.337 +if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
2.338 + then () else raise error "poly.sml: diff.behav. in make_polynomial";(*SPO*)
2.339 +val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
2.340 + val Some (t,_) = rewrite_set_ thy false make_polynomial t;
2.341 + term2str t;
2.342 +if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
2.343 + then () else raise error "poly.sml: diff.behav. in make_polynomial";
2.344 +
2.345 +"-------- Script 'simplification for_polynomials' ----------------";
2.346 +"-------- Script 'simplification for_polynomials' ----------------";
2.347 +"-------- Script 'simplification for_polynomials' ----------------";
2.348 +val str =
2.349 +"Script SimplifyScript (t_::real) = \
2.350 +\ ((Rewrite_Set norm_Poly False) t_)";
2.351 +val sc = ((inst_abs thy) o term_of o the o (parse thy)) str;
2.352 +atomty sc;
2.353 +
2.354 +
2.355 +"-------- check pbl 'polynomial simplification' -----------------";
2.356 +"-------- check pbl 'polynomial simplification' -----------------";
2.357 +"-------- check pbl 'polynomial simplification' -----------------";
2.358 +val fmz = ["term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
2.359 + \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
2.360 + "normalform N"];
2.361 +(*0*)
2.362 +case refine fmz ["polynomial","simplification"]of
2.363 + [Matches (["polynomial", "simplification"], _)] => ()
2.364 + | _ => raise error "poly.sml diff.behav. in check pbl, refine";
2.365 +(*...if there is an error, then ...*)
2.366 +
2.367 +(*1*)
2.368 +print_depth 7;
2.369 +val pbt = get_pbt ["polynomial","simplification"];
2.370 +print_depth 3;
2.371 +(*if there is ...
2.372 +> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
2.373 +... then trace_rewrite:*)
2.374 +
2.375 +(*2*)
2.376 +trace_rewrite:=true;
2.377 +match_pbl fmz pbt;
2.378 +trace_rewrite:=false;
2.379 +(*... if there is no rewrite, then there is something wrong with prls*)
2.380 +
2.381 +(*3*)
2.382 +print_depth 7;
2.383 +val prls = (#prls o get_pbt) ["polynomial","simplification"];
2.384 +print_depth 3;
2.385 +val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) \
2.386 + \- (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp";
2.387 +trace_rewrite:=true;
2.388 +val Some (t',_) = rewrite_set_ thy false prls t;
2.389 +trace_rewrite:=false;
2.390 +if t' = HOLogic.true_const then ()
2.391 +else raise error "poly.sml: diff.behav. in check pbl 'polynomial..";
2.392 +(*... if this works, but (*1*) does still NOT work, check types:*)
2.393 +
2.394 +(*4*)
2.395 +show_types:=true;
2.396 +(*
2.397 +> val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt;
2.398 +val wh = [False "(t_::real => real) (is_polyexp::real)"]
2.399 +......................^^^^^^^^^^^^...............^^^^*)
2.400 +val Matches' _ = match_pbl fmz pbt;
2.401 +show_types:=false;
2.402 +
2.403 +
2.404 +"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
2.405 +"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
2.406 +"-------- me 'polynomial simplification' Schalk I p.63 No.267b ---";
2.407 +val fmz = ["term ((5*x^^^2 + 3) * (2*x^^^7 + 3) \
2.408 + \- (3*x^^^5 + 8) * (6*x^^^4 - 1))",
2.409 + "normalform N"];
2.410 +val (dI',pI',mI') =
2.411 + ("Poly.thy",["polynomial","simplification"],
2.412 + ["simplification","for_polynomials"]);
2.413 +val p = e_pos'; val c = [];
2.414 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
2.415 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.416 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.417 +(writeln o (itms2str thy)) (get_obj g_pbl pt (fst p));
2.418 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.419 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.420 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.421 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.422 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.423 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.424 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2.425 +if f2str f =
2.426 +"17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
2.427 +then () else raise error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
2.428 +
2.429 +
2.430 +"-------- interSteps for Schalk 299a -----------------------------";
2.431 +"-------- interSteps for Schalk 299a -----------------------------";
2.432 +"-------- interSteps for Schalk 299a -----------------------------";
2.433 +states:=[];
2.434 +CalcTree
2.435 +[(["term ((x - y)*(x + y))", "normalform N"],
2.436 + ("Poly.thy",["polynomial","simplification"],
2.437 + ["simplification","for_polynomials"]))];
2.438 +Iterator 1;
2.439 +moveActiveRoot 1;
2.440 +autoCalculate 1 CompleteCalc;
2.441 +val ((pt,p),_) = get_calc 1; show_pt pt;
2.442 +
2.443 +interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
2.444 +val ((pt,p),_) = get_calc 1; show_pt pt;
2.445 +if existpt' ([1,1], Frm) pt then ()
2.446 +else raise error "poly.sml: interSteps doesnt work again 1";
2.447 +
2.448 +interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
2.449 +val ((pt,p),_) = get_calc 1; show_pt pt;
2.450 +if existpt' ([1,1,1], Frm) pt then ()
2.451 +else raise error "poly.sml: interSteps doesnt work again 2";
2.452 +
2.453 +
2.454 +"-------- norm_Poly NOT COMPLETE ---------------------------------";
2.455 +"-------- norm_Poly NOT COMPLETE ---------------------------------";
2.456 +"-------- norm_Poly NOT COMPLETE ---------------------------------";
2.457 +trace_rewrite:=true;
2.458 +val Some (f',_) = rewrite_set_ thy false norm_Poly
2.459 +(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*);
2.460 +trace_rewrite:=false;
2.461 +term2str f';
2.462 +
2.463 +"-------- ord_make_polynomial ------------------------------------";
2.464 +"-------- ord_make_polynomial ------------------------------------";
2.465 +"-------- ord_make_polynomial ------------------------------------";
2.466 +val t1 = str2term "2 * b + (3 * a + 3 * b)";
2.467 +val t2 = str2term "3 * a + 3 * b + 2 * b";
2.468 +
2.469 +if ord_make_polynomial true Poly.thy [] (t1, t2) then ()
2.470 +else raise error "poly.sml: diff.behav. in ord_make_polynomial";
2.471 +
2.472 +(*WN071202: ^^^ why then is there no rewriting ...*)
2.473 +val term = str2term "2*b + (3*a + 3*b)";
2.474 +val None = rewrite_set_ Isac.thy false order_add_mult term;
2.475 +
2.476 +(*or why is there no rewriting this way...*)
2.477 +val t1 = str2term "2 * b + (3 * a + 3 * b)";
2.478 +val t2 = str2term "3 * a + (2 * b + 3 * b)";
2.479 +
2.480 +
2.481 +