1.1 --- a/test/Tools/isac/Knowledge/poly.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/poly.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -32,7 +32,7 @@
1.4 "-------- check is'_polyexp is_polyexp ------------------";
1.5 "-------- check is'_polyexp is_polyexp ------------------";
1.6 if is_polyexp @{term "x / x"}
1.7 -then raise error "poly.sml: check is'_polyexp is_polyexp" else ();
1.8 +then error "poly.sml: check is'_polyexp is_polyexp" else ();
1.9
1.10
1.11 (*===== inhibit exn ?===========================================================
1.12 @@ -128,7 +128,7 @@
1.13 if (term2str t) =
1.14 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
1.15 then ()
1.16 -else raise error "poly.sml: diff.behav. in make_polynomial 1";
1.17 +else error "poly.sml: diff.behav. in make_polynomial 1";
1.18
1.19 (*SPB Schalk I p.63 No.275b*)
1.20 val t = str2term
1.21 @@ -139,7 +139,7 @@
1.22 "3 * x ^^^ 4 + -2 * x ^^^ 3 * y + -5 * x ^^^ 2 * y ^^^ 2 + \
1.23 \4 * x * y ^^^ 3 +\n-2 * y ^^^ 4"
1.24 then ()
1.25 -else raise error "poly.sml: diff.behav. in make_polynomial 2";
1.26 +else error "poly.sml: diff.behav. in make_polynomial 2";
1.27
1.28 (*SPB Schalk I p.63 No.279b*)
1.29 val t = str2term
1.30 @@ -150,7 +150,7 @@
1.31 if (term2str t) =
1.32 "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"
1.33 then ()
1.34 -else raise error "poly.sml: diff.behav. in make_polynomial 3";
1.35 +else error "poly.sml: diff.behav. in make_polynomial 3";
1.36
1.37 (*SPB Schalk I p.63 No.291*)
1.38 val t = str2term
1.39 @@ -160,7 +160,7 @@
1.40 if (term2str t) =
1.41 "50 + -770 * x + 4520 * x ^^^ 2 + -16320 * x ^^^ 3 + -26880 * x ^^^ 4"
1.42 then ()
1.43 -else raise error "poly.sml: diff.behav. in make_polynomial 4";
1.44 +else error "poly.sml: diff.behav. in make_polynomial 4";
1.45
1.46 (*SPB Schalk I p.64 No.295c*)
1.47 val t = str2term
1.48 @@ -171,7 +171,7 @@
1.49 "169 * a ^^^ 8 * b ^^^ 18 * c ^^^ 2 + -312 * a ^^^ 7 * b ^^^ 15 * c ^^^ 10\
1.50 \ +\n144 * a ^^^ 6 * b ^^^ 12 * c ^^^ 18"
1.51 then ()
1.52 -else raise error "poly.sml: diff.behav. in make_polynomial 5";
1.53 +else error "poly.sml: diff.behav. in make_polynomial 5";
1.54
1.55 (*SPB Schalk I p.64 No.299a*)
1.56 val t = str2term
1.57 @@ -181,7 +181,7 @@
1.58 if (term2str t) =
1.59 "x ^^^ 2 + -1 * y ^^^ 2"
1.60 then ()
1.61 -else raise error "poly.sml: diff.behav. in make_polynomial 6";
1.62 +else error "poly.sml: diff.behav. in make_polynomial 6";
1.63
1.64 (*SPB Schalk I p.64 No.300c*)
1.65 val t = str2term
1.66 @@ -191,14 +191,14 @@
1.67 if (term2str t) =
1.68 "-1 + 9 * x ^^^ 4 * y ^^^ 2"
1.69 then ()
1.70 -else raise error "poly.sml: diff.behav. in make_polynomial 7";
1.71 +else error "poly.sml: diff.behav. in make_polynomial 7";
1.72
1.73 (*SPB Schalk I p.64 No.302*)
1.74 val t = str2term
1.75 "(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.76 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.77 if term2str t = "0" then ()
1.78 -else raise error "poly.sml: diff.behav. in make_polynomial 8";
1.79 +else error "poly.sml: diff.behav. in make_polynomial 8";
1.80 (* Bei Berechnung sollte 3 mal real_plus_minus_binom1_p aus expand_poly verwendet werden *)
1.81
1.82
1.83 @@ -206,7 +206,7 @@
1.84 val t = str2term "((x^^^2 + 1)*(x^^^2 - 1))^^^2";
1.85 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.86 if (term2str t) = "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8" then ()
1.87 -else raise error "poly.sml: diff.behav. in make_polynomial: not confluent \
1.88 +else error "poly.sml: diff.behav. in make_polynomial: not confluent \
1.89 \2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 = -2 * x ^^^ 4 works again";
1.90
1.91
1.92 @@ -215,38 +215,38 @@
1.93 val t = str2term "1 + 2 * x ^^^ 4 + 2 * -2 * x ^^^ 4 + x ^^^ 8";
1.94 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.95 if (term2str t) = "1 + -2 * x ^^^ 4 + x ^^^ 8" then ()
1.96 -else raise error "poly.sml: diff.behav. in make_polynomial 9b";
1.97 +else error "poly.sml: diff.behav. in make_polynomial 9b";
1.98
1.99 (*SPB Schalk I p.64 No.296a*)
1.100 val t = str2term "(x - a)^^^3";
1.101 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.102 if (term2str t) = "-1 * a ^^^ 3 + 3 * a ^^^ 2 * x + -3 * a * x ^^^ 2 + x ^^^ 3"
1.103 -then () else raise error "poly.sml: diff.behav. in make_polynomial 10";
1.104 +then () else error "poly.sml: diff.behav. in make_polynomial 10";
1.105
1.106 (*SPB Schalk I p.64 No.296c*)
1.107 val t = str2term "(-3*x - 4*y)^^^3";
1.108 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.109 if (term2str t) =
1.110 "-27 * x ^^^ 3 + -108 * x ^^^ 2 * y + -144 * x * y ^^^ 2 + -64 * y ^^^ 3"
1.111 -then () else raise error "poly.sml: diff.behav. in make_polynomial 11";
1.112 +then () else error "poly.sml: diff.behav. in make_polynomial 11";
1.113
1.114 (*SPB Schalk I p.62 No.242c*)
1.115 val t = str2term "x^^^(-4)*(x^^^(-4)*y^^^(-2))^^^(-1)*y^^^(-2)";
1.116 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.117 if (term2str t) = "1" then ()
1.118 -else raise error "poly.sml: diff.behav. in make_polynomial 12";
1.119 +else error "poly.sml: diff.behav. in make_polynomial 12";
1.120
1.121 (*SPB Schalk I p.60 No.209a*)
1.122 val t = str2term "a^^^(7-x) * a^^^x";
1.123 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.124 if term2str t = "a ^^^ 7" then ()
1.125 -else raise error "poly.sml: diff.behav. in make_polynomial 13";
1.126 +else error "poly.sml: diff.behav. in make_polynomial 13";
1.127
1.128 (*SPB Schalk I p.60 No.209d*)
1.129 val t = str2term "d^^^x * d^^^(x+1) * d^^^(2 - 2*x)";
1.130 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.131 if term2str t = "d ^^^ 3" then ()
1.132 -else raise error "poly.sml: diff.behav. in make_polynomial 14";
1.133 +else error "poly.sml: diff.behav. in make_polynomial 14";
1.134
1.135
1.136 (*---------------------------------------------------------------------*)
1.137 @@ -257,7 +257,7 @@
1.138 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.139 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.140 if term2str t = "1280 * b ^^^ 4" then ()
1.141 -else raise error "poly.sml: diff.behav. in make_polynomial 14b";
1.142 +else error "poly.sml: diff.behav. in make_polynomial 14b";
1.143 (* Richtig - aber Binomische Formel wurde nicht verwendet! *)
1.144
1.145
1.146 @@ -268,62 +268,62 @@
1.147 val t = str2term "a^^^2*a^^^(-2)";
1.148 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.149 if term2str t = "1" then ()
1.150 -else raise error "poly.sml: diff.behav. in make_polynomial 15";
1.151 +else error "poly.sml: diff.behav. in make_polynomial 15";
1.152 (*SPO*)
1.153 val t = str2term "a + a + a";
1.154 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.155 if term2str t = "3 * a" then ()
1.156 -else raise error "poly.sml: diff.behav. in make_polynomial 16";
1.157 +else error "poly.sml: diff.behav. in make_polynomial 16";
1.158 (*SPO*)
1.159 val t = str2term "a + b + b + b";
1.160 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.161 if term2str t = "a + 3 * b" then ()
1.162 -else raise error "poly.sml: diff.behav. in make_polynomial 17";
1.163 +else error "poly.sml: diff.behav. in make_polynomial 17";
1.164 (*SPO*)
1.165 val t = str2term "a^^^2*b*b^^^(-1)";
1.166 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.167 if term2str t = "a ^^^ 2" then ()
1.168 -else raise error "poly.sml: diff.behav. in make_polynomial 18";
1.169 +else error "poly.sml: diff.behav. in make_polynomial 18";
1.170 (*SPO*)
1.171 val t = str2term "a^^^2*a^^^(-2)";
1.172 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.173 if (term2str t) = "1" then ()
1.174 -else raise error "poly.sml: diff.behav. in make_polynomial 19";
1.175 +else error "poly.sml: diff.behav. in make_polynomial 19";
1.176 (*SPO*)
1.177 val t = str2term "b + a - b";
1.178 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.179 if (term2str t) = "a" then ()
1.180 -else raise error "poly.sml: diff.behav. in make_polynomial 20";
1.181 +else error "poly.sml: diff.behav. in make_polynomial 20";
1.182 (*SPO*)
1.183 val t = str2term "b * a * a";
1.184 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.185 if term2str t = "a ^^^ 2 * b" then ()
1.186 -else raise error "poly.sml: diff.behav. in make_polynomial 21";
1.187 +else error "poly.sml: diff.behav. in make_polynomial 21";
1.188 (*SPO*)
1.189 val t = str2term "(a^^^2)^^^3";
1.190 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.191 if term2str t = "a ^^^ 6" then ()
1.192 -else raise error "poly.sml: diff.behav. in make_polynomial 22";
1.193 +else error "poly.sml: diff.behav. in make_polynomial 22";
1.194 (*SPO*)
1.195 val t = str2term "x^^^2 * y^^^2 + x * x^^^2 * y";
1.196 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.197 if term2str t = "x ^^^ 3 * y + x ^^^ 2 * y ^^^ 2" then ()
1.198 -else raise error "poly.sml: diff.behav. in make_polynomial 23";
1.199 +else error "poly.sml: diff.behav. in make_polynomial 23";
1.200 (*SPO*)
1.201 val t = (term_of o the o (parse thy)) "a^^^2 * (-a)^^^2";
1.202 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.203 if (term2str t) = "a ^^^ 4" then ()
1.204 -else raise error "poly.sml: diff.behav. in make_polynomial 24";
1.205 +else error "poly.sml: diff.behav. in make_polynomial 24";
1.206 (*SPO*)
1.207 val t = str2term "a * b * b^^^(-1) + a";
1.208 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.209 if (term2str t) = "2 * a" then ()
1.210 -else raise error "poly.sml: diff.behav. in make_polynomial 25";
1.211 +else error "poly.sml: diff.behav. in make_polynomial 25";
1.212 (*SPO*)
1.213 val t = str2term "a*c*b^^^(2*n) + 3*a + 5*b^^^(2*n)*c*b";
1.214 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; term2str t;
1.215 if (term2str t) = "3 * a + 5 * b ^^^ (1 + 2 * n) * c + a * b ^^^ (2 * n) * c"
1.216 -then () else raise error "poly.sml: diff.behav. in make_polynomial 26";
1.217 +then () else error "poly.sml: diff.behav. in make_polynomial 26";
1.218
1.219
1.220 (*MG.27.6.03 -------------vvv-: Verschachtelte Terme -----------*)
1.221 @@ -332,12 +332,12 @@
1.222 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.223 term2str t;
1.224 if term2str t = "(1 + x + a * x * y) ^^^ (1 + x + a * x * y)"
1.225 - then () else raise error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
1.226 + then () else error "poly.sml: diff.behav. in make_polynomial 27";(*SPO*)
1.227 val t = str2term "(1 + x*(y*z)*zz)^^^(1 + x*(y*z)*zz)";
1.228 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.229 term2str t;
1.230 if term2str t = "(1 + x * y * z * zz) ^^^ (1 + x * y * z * zz)"
1.231 - then () else raise error "poly.sml: diff.behav. in make_polynomial 28";
1.232 + then () else error "poly.sml: diff.behav. in make_polynomial 28";
1.233
1.234 "-------- Script 'simplification for_polynomials' ----------------";
1.235 "-------- Script 'simplification for_polynomials' ----------------";
1.236 @@ -358,7 +358,7 @@
1.237 (*0*)
1.238 case refine fmz ["polynomial","simplification"]of
1.239 [Matches (["polynomial", "simplification"], _)] => ()
1.240 - | _ => raise error "poly.sml diff.behav. in check pbl, refine";
1.241 + | _ => error "poly.sml diff.behav. in check pbl, refine";
1.242 (*...if there is an error, then ...*)
1.243
1.244 (*1*)
1.245 @@ -385,7 +385,7 @@
1.246 val SOME (t',_) = rewrite_set_ thy false prls t;
1.247 trace_rewrite:=false;
1.248 if t' = HOLogic.true_const then ()
1.249 -else raise error "poly.sml: diff.behav. in check pbl 'polynomial..";
1.250 +else error "poly.sml: diff.behav. in check pbl 'polynomial..";
1.251 (*... if this works, but (*1*) does still NOT work, check types:*)
1.252
1.253 (*4*)
1.254 @@ -421,7 +421,7 @@
1.255 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.256 if f2str f =
1.257 "17 + 15 * x ^^^ 2 + -48 * x ^^^ 4 + 3 * x ^^^ 5 + 6 * x ^^^ 7 + -8 * x ^^^ 9"
1.258 -then () else raise error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
1.259 +then () else error "poly.sml diff.behav. in me Schalk I p.63 No.267b";
1.260
1.261
1.262 "-------- interSteps for Schalk 299a -----------------------------";
1.263 @@ -440,12 +440,12 @@
1.264 interSteps 1 ([1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
1.265 val ((pt,p),_) = get_calc 1; show_pt pt;
1.266 if existpt' ([1,1], Frm) pt then ()
1.267 -else raise error "poly.sml: interSteps doesnt work again 1";
1.268 +else error "poly.sml: interSteps doesnt work again 1";
1.269
1.270 interSteps 1 ([1,1],Res)(*<ERROR> syserror in detailstep </ERROR>*);
1.271 val ((pt,p),_) = get_calc 1; show_pt pt;
1.272 if existpt' ([1,1,1], Frm) pt then ()
1.273 -else raise error "poly.sml: interSteps doesnt work again 2";
1.274 +else error "poly.sml: interSteps doesnt work again 2";
1.275
1.276
1.277 "-------- norm_Poly NOT COMPLETE ---------------------------------";
1.278 @@ -464,7 +464,7 @@
1.279 val t2 = str2term "3 * a + 3 * b + 2 * b";
1.280
1.281 if ord_make_polynomial true Poly.thy [] (t1, t2) then ()
1.282 -else raise error "poly.sml: diff.behav. in ord_make_polynomial";
1.283 +else error "poly.sml: diff.behav. in ord_make_polynomial";
1.284
1.285 (*WN071202: ^^^ why then is there no rewriting ...*)
1.286 val term = str2term "2*b + (3*a + 3*b)";