1.1 --- a/test/Tools/isac/Knowledge/rooteq.sml Tue Sep 28 08:58:06 2010 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rooteq.sml Tue Sep 28 09:06:56 2010 +0200
1.3 @@ -18,72 +18,72 @@
1.4 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
1.5 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.6 val result = term2str t_;
1.7 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.8 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.9
1.10 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in x";
1.11 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.12 val result = term2str t_;
1.13 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.14 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.15
1.16 val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in x";
1.17 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.18 val result = term2str t_;
1.19 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.20 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.21
1.22 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in x";
1.23 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.24 val result = term2str t_;
1.25 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.26 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.27
1.28 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in x";
1.29 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.30 val result = term2str t_;
1.31 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.32 +if result <> "False" then error "rooteq.sml: new behaviour:" else ();
1.33
1.34 val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
1.35 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.36 val result = term2str t_;
1.37 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.38 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.39
1.40 val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
1.41 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.42 val result = term2str t_;
1.43 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.44 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.45
1.46 val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
1.47 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.48 val result = term2str t_;
1.49 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.50 +if result <> "False" then error "rooteq.sml: new behaviour:" else ();
1.51
1.52 val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
1.53 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.54 val result = term2str t_;
1.55 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.56 +if result <> "False" then error "rooteq.sml: new behaviour:" else ();
1.57
1.58 val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
1.59 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.60 val result = term2str t_;
1.61 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.62 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.63
1.64 val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
1.65 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.66 val result = term2str t_;
1.67 -if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
1.68 +if result <> "False" then error "rooteq.sml: new behaviour:" else ();
1.69
1.70 val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in x";
1.71 val SOME(t_, _) = rewrite_set_ RootEq.thy false RootEq_prls t;
1.72 val result = term2str t_;
1.73 -if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
1.74 +if result <> "True" then error "rooteq.sml: new behaviour:" else ();
1.75
1.76
1.77
1.78 val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
1.79 (get_pbt ["root'","univariate","equation"]);
1.80 -case result of Matches' _ => () | _ => raise error "rooteq.sml: new behaviour:";
1.81 +case result of Matches' _ => () | _ => error "rooteq.sml: new behaviour:";
1.82
1.83 val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
1.84 (get_pbt ["root'","univariate","equation"]);
1.85 -case result of NoMatch' _ => () | _ => raise error "rooteq.sml: new behaviour:";
1.86 +case result of NoMatch' _ => () | _ => error "rooteq.sml: new behaviour:";
1.87
1.88 (*---------rooteq---- 23.8.02 ---------------------*)
1.89 "---------(1/sqrt(x)=5)---------------------";
1.90 @@ -112,7 +112,7 @@
1.91 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.92 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.93 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "1 + -25 * x = 0")) then ()
1.94 -else raise error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
1.95 +else error "rooteq.sml: diff.behav.poly in (1/sqrt(x)=5)";
1.96 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
1.97 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.98 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.99 @@ -126,14 +126,14 @@
1.100 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.101 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.102 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1 / 25]")) => ()
1.103 - | _ => raise error "rooteq.sml: diff.behav. [x = 1 / 25]";
1.104 + | _ => error "rooteq.sml: diff.behav. [x = 1 / 25]";
1.105 if asms2str (get_assumptions_ pt p) = "[(0 <= 1 / 25, [])]"
1.106 (*WN050916 before correction 'rewrite__set_ called with 'Erls' for ..:
1.107 [(str2term"25 ~= 0",[])] *)
1.108 then writeln "should be True\n\
1.109 \should be True\n\
1.110 \should be True\n"
1.111 -else raise error "rooteq.sml: diff.behav. with 25 ~= 0";
1.112 +else error "rooteq.sml: diff.behav. with 25 ~= 0";
1.113
1.114 "---------(sqrt(x+1)=5)---------------------";
1.115 val fmz = ["equality (sqrt(x+1)=5)","solveFor x","solutions L"];
1.116 @@ -157,7 +157,7 @@
1.117 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.118 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.119 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-24 + x = 0")) then ()
1.120 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
1.121 +else error "rooteq.sml: diff.behav.poly in sqrt(x+1)=5";
1.122 (*-> Subproblem ("PolyEq", ["polynomial", ...])*)
1.123 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.124 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.125 @@ -169,7 +169,7 @@
1.126 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.127 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.128 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 24]")) => ()
1.129 - | _ => raise error "rooteq.sml: diff.behav. [x = 24]";
1.130 + | _ => error "rooteq.sml: diff.behav. [x = 24]";
1.131
1.132 "-------------(4*sqrt(4*x+2)=3*sqrt(2*x+24))-----------------";
1.133 val fmz = ["equality (4*sqrt(4*x+2)=3*sqrt(2*x+24))","solveFor x","solutions L"];
1.134 @@ -188,7 +188,7 @@
1.135 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.136 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.137 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-184 + 46 * x = 0")) then ()
1.138 -else raise error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
1.139 +else error "rooteq.sml: diff.behav.poly in 4*sqrt(4*x+2)=3*sqrt(2*x+24)";
1.140 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.142 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.143 @@ -199,11 +199,11 @@
1.144 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.145 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
1.146 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 4]")) => ()
1.147 - | _ => raise error "rooteq.sml: diff.behav. [x = 4]";
1.148 + | _ => error "rooteq.sml: diff.behav. [x = 4]";
1.149 if get_assumptions_ pt p = [(str2term"0 <= 12 * sqrt 2 * 4",[])]
1.150 then writeln "should be True\nshould be True\nshould be True\n\
1.151 \should be True\nshould be True\nshould be True\n"
1.152 -else raise error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
1.153 +else error "rooteq.sml: diff.behav. with 0 <= 12 * sqrt 2 * 4";
1.154
1.155 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))----------------";
1.156 val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
1.157 @@ -238,7 +238,7 @@
1.158 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.159 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.160 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.161 -else raise error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
1.162 +else error "rooteq.sml: diff.behav.poly in (sqrt(x+1)+sqrt(4*x+4)=sqr..";
1.163 (*-> Subproblem ("PolyEq", ["degree_0", ...])*)
1.164 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.165 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.166 @@ -252,7 +252,7 @@
1.167 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.168 val asm = get_assumptions_ pt p;
1.169 if f = Form' (FormKF (~1,EdUndef,0,Nundef,"UniversalList")) andalso asm = []
1.170 -then () else raise error "rooteq.sml: diff.behav. in UniversalList 1";
1.171 +then () else error "rooteq.sml: diff.behav. in UniversalList 1";
1.172
1.173
1.174
1.175 @@ -285,7 +285,7 @@
1.176 (*val p = ([6,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
1.177 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
1.178 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.179 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.180 +else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.181 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.182 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.183 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.184 @@ -303,7 +303,7 @@
1.185 val nxt = Check_Postcond ["normalize","polynomial","univariate","equation"])*)
1.186 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.187 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "UniversalList")) then ()
1.188 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.189 +else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.190 (* val Form' (FormKF (~1, EdUndef, 0, Nundef, str)) = f;
1.191 *)
1.192
1.193 @@ -337,7 +337,7 @@
1.194 (*val p = ([3,2],Res)val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-1 + x = 0"))
1.195 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
1.196 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-1 + x = 0")) then ()
1.197 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.198 +else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.199 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.200 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.201 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.202 @@ -366,7 +366,7 @@
1.203 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *)
1.204 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.205 if p = ([],Res) andalso f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]"))
1.206 -then () else raise error "diff.behav. in rooteq.sml: sqrt(x) = 1";
1.207 +then () else error "diff.behav. in rooteq.sml: sqrt(x) = 1";
1.208
1.209
1.210 "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))---------- SHORTEST.1.----\
1.211 @@ -394,7 +394,7 @@
1.212 (*val p = ([2,2],Res) val f = Form' (FormKF (~1,EdUndef,2,Nundef,"0 = 0"))
1.213 val nxt = Subproblem ("PolyEq",["polynomial","univariate","equation"]))*)
1.214 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "0 = 0")) then ()
1.215 -else raise error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.216 +else error "rooteq.sml: diff.behav.poly in sqrt(x+1)+sqrt(4*x+4)=sqrt..";
1.217 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.218 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.219 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.220 @@ -415,7 +415,7 @@
1.221 val nxt = Check_Postcond ["sq","root'","univariate","equation"]) *)
1.222 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.223 if p = ([],Res) andalso f = Form'(FormKF (~1,EdUndef,0,Nundef,"UniversalList"))
1.224 -then () else raise error "new behav. in rooteq.sml: sqrt x = sqrt x";
1.225 +then () else error "new behav. in rooteq.sml: sqrt x = sqrt x";
1.226
1.227
1.228 "--------------(3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))----------------";
1.229 @@ -450,7 +450,7 @@
1.230 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.231 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.232 if f = Form' (FormKF (~1, EdUndef, 0, Nundef, "-648 + -324 * x = 0")) then ()
1.233 -else raise error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
1.234 +else error "rooteq.sml: diff.behav.poly in 3*sqrt(x+3)+sqrt(x+6)=sqrt..";
1.235 (*-> Subproblem ("PolyEq", ["degree_1", ...])*)
1.236 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.237 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.238 @@ -463,7 +463,7 @@
1.239 val (p,_,f,nxt,_,pt) = me nxt p c pt;val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.240 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.241 case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2]")) => ()
1.242 - | _ => raise error "rooteq.sml: diff.behav. [x = -2]";
1.243 + | _ => error "rooteq.sml: diff.behav. [x = -2]";
1.244
1.245 "----------- rooteq.sml end--------";
1.246