1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/kbtest/poly.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,2 @@
1.4 +(* testexamples for Poly, polynomials
1.5 + *)
1.6 \ No newline at end of file
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/kbtest/polyeq.sml Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,479 @@
2.4 +(* testexamples for PolyEq, poynomial equations and equational systems
2.5 + use"kbtest/polyeq.sml";
2.6 + use"polyeq.sml";
2.7 +
2.8 + *)
2.9 +
2.10 +"-------------- tests on predicates in problems ---------------------------";
2.11 +"----------------------test matching problems -----------------------------";
2.12 +"-------------------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b-----";
2.13 +"-------------------- (-16 + 4*x + 2*x^^^2 = 0), ----------------------";
2.14 +"-------------------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2, S.68 Nr.44.a*)";
2.15 +"-------------------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
2.16 +"-------------------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b--------*)";
2.17 +
2.18 +"---- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk I s.86 Bsp 5-------------*)";
2.19 +"((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1)),(*Schal II s.68 Bsp 37*)";
2.20 +
2.21 +
2.22 +"-------------- tests on predicates in problems ---------------------------";
2.23 +"-------------- tests on predicates in problems ---------------------------";
2.24 +"-------------- tests on predicates in problems ---------------------------";
2.25 +(* Compiler.Control.Print.printDepth:=5; (*4 default*)
2.26 + trace_rewrite:=true;
2.27 + trace_rewrite:=false;
2.28 +*)
2.29 + val t1 = (term_of o the o (parse thy)) "lhs (-8 - 2*x + x^^^2 = 0)";
2.30 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t1;
2.31 + if ((term2str t) = "-8 - 2 * x + x ^^^ 2") then ()
2.32 + else raise error "polyeq.sml: diff.behav. in lhs";
2.33 +
2.34 +
2.35 + val t2 = (term_of o the o (parse thy)) "(-8 - 2*x + x^^^2) is_expanded_in x";
2.36 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t2;
2.37 + if (term2str t) = "True" then ()
2.38 + else raise error "polyeq.sml: diff.behav. in is_expended_in";
2.39 +
2.40 + val t0 = (term_of o the o (parse thy)) "(sqrt(x)) is_poly_in x";
2.41 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t0;
2.42 + if (term2str t) = "False" then ()
2.43 + else raise error "polyeq.sml: diff.behav. in is_poly_in";
2.44 +
2.45 +
2.46 + val t3 = (term_of o the o (parse thy)) "(-8 + (-1)*2*x + x^^^2) is_poly_in x";
2.47 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t3;
2.48 + if (term2str t) = "True" then ()
2.49 + else raise error "polyeq.sml: diff.behav. in is_poly_in";
2.50 +
2.51 +
2.52 + val t4 = (term_of o the o (parse thy)) "(lhs (-8 + (-1)*2*x + x^^^2 = 0)) is_expanded_in x";
2.53 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t4;
2.54 + if (term2str t) = "True" then ()
2.55 + else raise error "polyeq.sml: diff.behav. in is_expended_in";
2.56 +
2.57 +
2.58 + val t6 = (term_of o the o (parse thy)) "(lhs (-8 - 2*x + x^^^2 = 0)) is_expanded_in x";
2.59 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t6;
2.60 + if (term2str t) = "True" then ()
2.61 + else raise error "polyeq.sml: diff.behav. in is_expended_in";
2.62 +
2.63 + val t3 = (term_of o the o (parse thy))"((-8 - 2*x + x^^^2) has_degree_in x) = 2";
2.64 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t3;
2.65 + if (term2str t) = "2 = 2" then ()
2.66 + else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
2.67 +
2.68 +
2.69 + val t3 = (term_of o the o (parse thy)) "((sqrt(x)) has_degree_in x) = 2";
2.70 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t3;
2.71 + if (term2str t) = "-1 = 2" then ()
2.72 + else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
2.73 +
2.74 + val t4 = (term_of o the o (parse thy))
2.75 + "((-8 - 2*x + x^^^2) has_degree_in x) = 1";
2.76 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t4;
2.77 + if (term2str t) = "2 = 1" then ()
2.78 + else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
2.79 +
2.80 +
2.81 + val t5 = (term_of o the o (parse thy))
2.82 + "((-8 - 2*x + x^^^2) has_degree_in x) =!= 2";
2.83 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_prls t5;
2.84 + if (term2str t) = "True" then ()
2.85 + else raise error "polyeq.sml: diff.behav. in has_degree_in_in";
2.86 +
2.87 +"----------------------test matching problems -----------------------------";
2.88 +"----------------------test matching problems -----------------------------";
2.89 +"----------------------test matching problems -----------------------------";
2.90 + val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", "solveFor x","solutions L"];
2.91 + val pbt as {thy = thy, where_ = pre, ppc = ppc,...} =
2.92 + get_pbt ["expanded","univariate","equation"];
2.93 +
2.94 + match_pbl fmz (get_pbt ["expanded","univariate","equation"]);
2.95 + (*Matches'
2.96 + {Find=[Correct "solutions L"],
2.97 + Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
2.98 + Correct "solveFor x"],Relate=[],
2.99 + Where=[Correct "matches (?a = 0) (-8 - 2 * x + x ^^^ 2 = 0)",
2.100 + Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) is_expanded_in x"],With=[]}
2.101 + *)
2.102 + match_pbl fmz (get_pbt ["degree_2","expanded","univariate","equation"]);
2.103 + (*Matches'
2.104 + {Find=[Correct "solutions L"],
2.105 + Given=[Correct "equality (-8 - 2 * x + x ^^^ 2 = 0)",
2.106 + Correct "solveFor x"],Relate=[],
2.107 + Where=[Correct "lhs (-8 - 2 * x + x ^^^ 2 = 0) has_degree_in x =!= 2"],
2.108 + With=[]}*)
2.109 +
2.110 +
2.111 +"-------------------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b-----";
2.112 +"-------------------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b-----";
2.113 +"-------------------- (-8 - 2*x + x^^^2 = 0), (*Schalk 2, S.67 Nr.31.b-----";
2.114 + val fmz = ["equality (-8 - 2*x + x^^^2 = 0)", (*Schalk 2, S.67 Nr.31.b*)
2.115 + "solveFor x","solutions L"];
2.116 + val (dI',pI',mI') =
2.117 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
2.118 + ("PolyEq.thy","complete_square"));
2.119 + val p = e_pos'; val c = [];
2.120 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.121 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.122 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.123 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.124 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.125 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.126 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.127 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.128 + (*Apply_Method ("PolyEq.thy","complete_square")*)
2.129 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.130 + (*"-8 - 2 * x + x ^^^ 2 = 0", nxt = Rewrite_Set_Inst ... "complete_square*)
2.131 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.132 + (*"-8 + (2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2", nxt = Rewrite("square_explicit1"*)
2.133 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.134 + (*"(2 / 2 - x) ^^^ 2 = (2 / 2) ^^^ 2 - -8" nxt = Rewrite("root_plus_minus*)
2.135 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.136 + (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
2.137 + 2 / 2 - x = - sqrt ((2 / 2) ^^^ 2 - -8)" nxt = Rewr_Inst("bdv_explicit2"*)
2.138 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.139 + (*"2 / 2 - x = sqrt ((2 / 2) ^^^ 2 - -8) |
2.140 + -1*x = - (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8)"nxt = R_Inst("bdv_explt2"*)
2.141 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.142 + (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
2.143 + -1 * x = (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = bdv_explicit3*)
2.144 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.145 + (*"-1 * x = - (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8) |
2.146 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))" nxt = bdv_explicit3*)
2.147 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.148 + (*"x = -1 * (- (2 / 2) + sqrt ((2 / 2) ^^^ 2 - -8)) |
2.149 + x = -1 * (- (2 / 2) + - sqrt ((2 / 2) ^^^ 2 - -8))"nxt = calculate_Ration*)
2.150 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.151 + (*"x = -2 | x = 4" nxt = Or_to_List*)
2.152 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.153 + (*"[x = -2, x = 4]" nxt = Check_Postcond*)
2.154 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.155 +(* FIXXX ME
2.156 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -2, x = 4]")) => ()
2.157 + | _ => raise error "polyeq.sml: diff.behav. in [x = -2, x = 4]";
2.158 +*)
2.159 +
2.160 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
2.161 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
2.162 +"-------------------- (3 - 10*x + 3*x^^^2 = 0), ----------------------";
2.163 +"---- test the erls ----";
2.164 + val t1 = (term_of o the o (parse thy)) "0 <= (10/3/2)^^^2 - 1";
2.165 + val Some (t,_) = rewrite_set_ PolyEq.thy false polyeq_erls t1;
2.166 + val t' = term2str t;
2.167 + (*if t'= "True" then ()
2.168 + else raise error "polyeq.sml: diff.behav. in 'rewrite_set_.. polyeq_erls";*)
2.169 +(* *)
2.170 + val fmz = ["equality (3 - 10*x + 3*x^^^2 = 0)",
2.171 + "solveFor x","solutions L"];
2.172 + val (dI',pI',mI') =
2.173 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
2.174 + ("PolyEq.thy","complete_square"));
2.175 + val p = e_pos'; val c = [];
2.176 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.177 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.178 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.179 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.180 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.181 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.182 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.183 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.184 + (*Apply_Method ("PolyEq.thy","complete_square")*)
2.185 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.186 +
2.187 +"-------------------- (-16 + 4*x + 2*x^^^2 = 0), ----------------------";
2.188 +"-------------------- (-16 + 4*x + 2*x^^^2 = 0), ----------------------";
2.189 +"-------------------- (-16 + 4*x + 2*x^^^2 = 0), ----------------------";
2.190 + val fmz = ["equality (-16 + 4*x + 2*x^^^2 = 0)",
2.191 + "solveFor x","solutions L"];
2.192 + val (dI',pI',mI') =
2.193 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
2.194 + ("PolyEq.thy","complete_square"));
2.195 + val p = e_pos'; val c = [];
2.196 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.197 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.198 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.199 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.200 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.201 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.202 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.203 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.204 + (*Apply_Method ("PolyEq.thy","complete_square")*)
2.205 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.206 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.207 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.208 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.209 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.210 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.211 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.212 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.213 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.214 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.215 +(* FIXXXX ME
2.216 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -4]")) => ()
2.217 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -4]";
2.218 +*)
2.219 +
2.220 +"-------------------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2, S.68 Nr.44.a*)";
2.221 +"-------------------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2, S.68 Nr.44.a*)";
2.222 +"-------------------- (a*b - (a+b)*x + x^^^2 = 0), (*Schalk 2, S.68 Nr.44.a*)";
2.223 + val fmz = ["equality (a*b - (a+b)*x + x^^^2 = 0)",(*Schalk 2, S.68 Nr.44.a*)
2.224 + "solveFor x","solutions L"];
2.225 + val (dI',pI',mI') =
2.226 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
2.227 + ("PolyEq.thy","complete_square"));
2.228 + val p = e_pos'; val c = [];
2.229 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.230 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.231 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.232 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.233 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.234 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.235 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.236 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.237 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.238 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.239 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.240 +
2.241 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.242 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.243 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.244 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.245 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.246 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.247 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.248 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.249 + case f of
2.250 + Form'
2.251 + (FormKF
2.252 + (~1,EdUndef,0,Nundef,
2.253 + "[x = (a + b) / 2 + -1 * sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b),\n x = (a + b) / 2 + sqrt ((a + b) ^^^ 2 / 2 ^^^ 2 - a * b)]"))
2.254 + => ()
2.255 + | _ => raise error "polyeq.sml: diff.behav. in a*b - (a+b)*x + x^^^2 = 0";
2.256 + (*this will be simplified [x = a, x = b] to by Factor.ML*)
2.257 +
2.258 +
2.259 +"-------------------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
2.260 +"-------------------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
2.261 +"-------------------- (-64 + x^^^2 = 0), (*Schalk 2, S.66 Nr.1.a~--------*)";
2.262 + val fmz = ["equality (-64 + x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.a~*)
2.263 + "solveFor x","solutions L"];
2.264 + val (dI',pI',mI') =
2.265 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
2.266 + ("PolyEq.thy","complete_square"));
2.267 + val p = e_pos'; val c = [];
2.268 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.269 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.270 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.271 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.272 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.273 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.274 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.275 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.276 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.277 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.278 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.279 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.280 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.281 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.282 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8, x = -8]")) => ()
2.283 + | _ => raise error "polyeq.sml: diff.behav. in [x = 8, x = -8]";
2.284 +
2.285 +
2.286 +"-------------------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b--------*)";
2.287 +"-------------------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b--------*)";
2.288 +"-------------------- (-147 + 3*x^^^2 = 0), (*Schalk 2, S.66 Nr.1.b--------*)";
2.289 + val fmz = ["equality (-147 + 3*x^^^2 = 0)",(*Schalk 2, S.66 Nr.1.b*)
2.290 + "solveFor x","solutions L"];
2.291 + val (dI',pI',mI') =
2.292 + ("PolyEq.thy",["degree_2","expanded","univariate","equation"],
2.293 + ("PolyEq.thy","complete_square"));
2.294 + val p = e_pos'; val c = [];
2.295 + val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.296 + val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.297 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.298 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.299 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.300 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.301 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.302 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.303 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.304 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.305 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.306 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.307 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.308 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.309 + val (p,_,f,nxt,_,pt) = me nxt p c pt;
2.310 + case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 7, x = -7]")) => ()
2.311 + | _ => raise error "polyeq.sml: diff.behav. in [x = 7, x = -7]";
2.312 +
2.313 +
2.314 +
2.315 +"---- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk I s.86 Bsp 5-------------*)";
2.316 +"---- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk I s.86 Bsp 5-------------*)";
2.317 +"---- (3*x - 1 - (5*x - (2 - 4*x)) = -11),(*Schalk I s.86 Bsp 5-------------*)";
2.318 +val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)","solveFor x","solutions L"];
2.319 +(* refine fmz ["univariate","equation"];
2.320 +*)
2.321 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
2.322 +val p = e_pos';
2.323 +val c = [];
2.324 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.325 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.326 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.327 +(* val nxt =
2.328 + ("Model_Problem",
2.329 + Model_Problem ["normalize","polynomial","univariate","equation"])
2.330 + : string * mstep*)
2.331 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.332 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.333 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.334 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.335 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.336 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.337 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.338 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.339 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.340 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.341 +(* val nxt =
2.342 + ("Subproblem",
2.343 + Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
2.344 + : string * mstep *)
2.345 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.346 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.347 +(*val nxt =
2.348 + ("Model_Problem",
2.349 + Model_Problem ["degree_1","polynomial","univariate","equation"])
2.350 + : string * mstep *)
2.351 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.352 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.353 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.354 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.355 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.356 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.357 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.358 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.359 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.360 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.361 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.362 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.363 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.364 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.365 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
2.366 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2]";
2.367 +(* [x = 2] *)
2.368 +
2.369 +(*----------------- Schal II s.68 Bsp 37 ------------------------*)
2.370 +"Schal II s.68 Bsp 37 ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1)) ";
2.371 +"Schal II s.68 Bsp 37 ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1)) ";
2.372 +"Schal II s.68 Bsp 37 ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1)) ";
2.373 +val fmz = ["equality ((x+1)*(x+2) - (3*x - 2)^^^2=(2*x - 1)^^^2+(3*x - 1)*(x+1))",
2.374 + "solveFor x","solutions L"];
2.375 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
2.376 +val p = e_pos';
2.377 +val c = [];
2.378 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.379 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.380 +(*val nxt = ("Refine_Tacitly",Refine_Tacitly ["univariate","equation"])*)
2.381 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.382 +(* val nxt =
2.383 + ("Model_Problem",
2.384 + Model_Problem ["normalize","polynomial","univariate","equation"])
2.385 + : string * mstep *)
2.386 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.387 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.388 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.389 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.390 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.391 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.392 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.393 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.394 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.395 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.396 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.397 +(* val nxt =
2.398 + ("Subproblem",
2.399 + Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))
2.400 + : string * mstep*)
2.401 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.402 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.403 +(*val nxt =
2.404 + ("Model_Problem",
2.405 + Model_Problem ["abcFormula","degree_2","polynomial","univariate","equation"])
2.406 + : string * mstep*)
2.407 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.408 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.409 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.410 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.411 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.412 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.413 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.414 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.415 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.416 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.417 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.418 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.419 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.420 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.421 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2 / 15, x = 1]")) => ()
2.422 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2 / 15, x = 1]";
2.423 +(* [x = 2 / 15 , x = 1]*)
2.424 +"----------------- polyeq.sml end ------------------";
2.425 +val fmz = ["equality ( -4 + x^^^2 =0)", "solveFor x","solutions L"];
2.426 +(* val fmz = ["equality (1 + x^^^2 =0)", "solveFor x","solutions L"];*)
2.427 +(*val fmz = ["equality (0 =0)", "solveFor x","solutions L"];*)
2.428 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
2.429 +val p = e_pos';
2.430 +val c = [];
2.431 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
2.432 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
2.433 +
2.434 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.435 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.436 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.437 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.438 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.439 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.440 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.441 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.442 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.443 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.444 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.445 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.446 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.447 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
2.448 +(* FIXXX ME applicable_in Check_elementwise:
2.449 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
2.450 + | _ => raise error "polyeq.sml: diff.behav. in [x = 2, x = -2]";
2.451 +*)
2.452 +
2.453 +(*Punkte aus dem TestBericht, die ich in rlang.sml nicht zuordnen konnte:*)
2.454 +(*WN.19.3.03 ---v-*)
2.455 +(*3(b)*)val (bdv,v) = (str2term "bdv", str2term "R1");
2.456 +val t = str2term "-1 * (R * R2) + R2 * R1 + -1 * (R * R1) = 0";
2.457 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
2.458 +term2str t';
2.459 +"-1 * R * R2 + (R2 + -1 * R) * R1 = 0";
2.460 +(*WN.19.3.03 ---^-*)
2.461 +
2.462 +(*3(c)*)val (bdv,v) = (str2term "bdv", str2term "p");
2.463 +val t = str2term "y ^^^ 2 + -2 * (x * p) = 0";
2.464 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
2.465 +term2str t';
2.466 +"y ^^^ 2 + -2 * x * p = 0";
2.467 +
2.468 +(*3(d)*)val (bdv,v) = (str2term "bdv", str2term "x2");
2.469 +val t = str2term
2.470 +"A + x1 * (y3 * (1 / 2)) + x3 * (y2 * (1 / 2)) + -1 * (x1 * (y2 * (1 / 2))) + -1 * (x3 * (y1 * (1 / 2 ))) + y1 * (1 / 2 * x2) + -1 * (y3 * (1 / 2 * x2)) = 0";
2.471 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
2.472 +term2str t';
2.473 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + - x1 * y2 * (1 / 2) + - x3 * y1 * (1 / 2) + (y1 * (1 / 2) + - y3 * (1 / 2)) * x2 = 0";
2.474 +val Some (t',_) = rewrite_set_inst_ thy false [(bdv,v)] make_ratpoly_in t;
2.475 +term2str t';
2.476 +"A + x1 * y3 * (1 / 2) + x3 * y2 * (1 / 2) + -1 * x1 * y2 * (1 / 2) + -1 * x3 * y1 * (1 / 2) + (y1 * (1 / 2) + -1 * y3 * (1 / 2)) * x2 = 0";
2.477 +
2.478 +(*3(e)*)val (bdv,v) = (str2term "bdv", str2term "a");
2.479 +val t = str2term
2.480 +"A ^^^ 2 + c ^^^ 2 * (c / d) ^^^ 2 + (-4 * (c / d) ^^^ 2) * a ^^^ 2 = 0";
2.481 +val None = rewrite_set_inst_ thy false [(bdv,v)] make_polynomial_in t;
2.482 +(*die _unsichtbare_ Klammern sind genau wie gew"unscht*)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/kbtest/rateq.sml Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,170 @@
3.4 +(* RL 09.02
3.5 + testexamples for RatEq, equations with fractions
3.6 +
3.7 + Compiler.Control.Print.printDepth:=10; (*4 default*)
3.8 + Compiler.Control.Print.printDepth:=5; (*4 default*)
3.9 + trace_rewrite:=true;
3.10 +*)
3.11 + "----------- rateq.sml begin--------";
3.12 +"---------(1/x=5) ---------------------";
3.13 +"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
3.14 +
3.15 +val t = (term_of o the o (parse RatEq.thy)) "(1/b+1/x=1) is_ratequation_in x";
3.16 +val Some(t_, _) = rewrite_set_ RatEq.thy false rateq_prls t;
3.17 +val result = term2str t_;
3.18 +if result <> "True" then raise error "rateq.sml: new behaviour:" else ();
3.19 +
3.20 +val t = (term_of o the o (parse RatEq.thy)) "(sqrt(x)=1) is_ratequation_in x";
3.21 +val Some(t_, _) = rewrite_set_ RatEq.thy false rateq_prls t;
3.22 +val result = term2str t_;
3.23 +if result <> "False" then raise error "rateq.sml: new behaviour:" else ();
3.24 +
3.25 +val t = (term_of o the o (parse RatEq.thy)) "(x=-1) is_ratequation_in x";
3.26 +val Some(t_,_) = rewrite_set_ RatEq.thy false rateq_prls t;
3.27 +val result = term2str t_;
3.28 +if result <> "False" then raise error "rateq.sml: new behaviour:" else ();
3.29 +
3.30 +val t = (term_of o the o (parse RatEq.thy)) "(3 + x^^^2 + 1/(x^^^2+3)=1) is_ratequation_in x";
3.31 +val Some(t_,_) = rewrite_set_ RatEq.thy false rateq_prls t;
3.32 +val result = term2str t_;
3.33 +if result <> "True" then raise error "rateq.sml: new behaviour:" else ();
3.34 +
3.35 +val result = match_pbl ["equality (x=1)","solveFor x","solutions L"]
3.36 + (get_pbt ["rational","univariate","equation"]);
3.37 +case result of NoMatch' _ => () | _ => raise error "rateq.sml: new behaviour:";
3.38 +
3.39 +val result = match_pbl ["equality (3 + x^^^2 + 1/(x^^^2+3)=1)","solveFor x","solutions L"]
3.40 + (get_pbt ["rational","univariate","equation"]);
3.41 +case result of Matches' _ => () | _ => raise error "rateq.sml: new behaviour:";
3.42 +
3.43 +
3.44 +(*---------rateq---- 23.8.02 ---------------------*)
3.45 +"---------(1/x=5) ---------------------";
3.46 +val fmz = ["equality (1/x=5)","solveFor x","solutions L"];
3.47 +(* refine fmz ["univariate","equation"];
3.48 +*)
3.49 +
3.50 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.51 +val p = e_pos';
3.52 +val c = [];
3.53 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.54 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.55 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.56 +(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"]) *)
3.57 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.58 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.59 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.60 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.61 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.62 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.63 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.64 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.65 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.66 +(* val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
3.67 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.68 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.69 +(*val nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
3.70 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.71 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.72 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.73 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.74 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.75 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.76 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.77 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.78 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.79 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.80 +(* val nxt = ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
3.81 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.82 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.83 +(* ("Model_Problem", Model_Problem ["degree_1","polynomial","univariate","equation"])*)
3.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.85 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.88 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.89 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.90 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.91 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.92 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.93 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.94 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.95 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.96 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.97 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.98 +(* "x = 1 / 5" *)
3.99 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.100 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.101 +if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = 1 / 5])" then ()
3.102 +else raise error "rateq.sml: new behaviour:";
3.103 +
3.104 +(*---------((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------*)
3.105 +"--------- S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)---------------------";
3.106 +val fmz = ["equality ((x)/(x - 8) + (x - 8)/(x) = 26/5)","solveFor x","solutions L"];
3.107 +(* val fmz = ["equality (3+x= 9*x^^^4+((1+2*x)/x^^^2)^^^2 + 6*(x^^^2*((1+2*x)/x^^^2)))",
3.108 + "solveFor x","solutions L"];*)
3.109 +
3.110 +(* refine fmz ["univariate","equation"];
3.111 +*)
3.112 +
3.113 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.114 +val p = e_pos';
3.115 +val c = [];
3.116 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.117 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.118 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.119 +(* nxt = ("Model_Problem",Model_Problem ["rational","univariate","equation"])*)
3.120 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.121 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.122 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.123 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.124 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.125 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.126 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.127 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.128 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.129 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.130 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.131 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.132 +(* nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"]))*)
3.133 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.134 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.135 +(* nxt = ("Model_Problem", Model_Problem ["normalize","polynomial","univariate","equation"])*)
3.136 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.137 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.138 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.139 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.140 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.141 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.142 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.143 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.144 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.145 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.146 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.147 +(* ("Subproblem", Subproblem ("PolyEq.thy",["polynomial","univariate","equation"])) *)
3.148 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.149 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.150 +(* nxt = ("Model_Problem", Model_Problem
3.151 + ["abcFormula","degree_2","polynomial","univariate","equation"])*)
3.152 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.153 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.154 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.155 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.156 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.157 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.158 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.159 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.160 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.161 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.162 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.163 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.164 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.165 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.166 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.167 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.168 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.169 +(* "x = -2, x = 10" *)
3.170 +if mout2str(f) = "Form' FormKF (~1,EdUndef,0,Nundef,([x = -2, x = 10])" then ()
3.171 +else raise error "rateq.sml: new behaviour:";
3.172 +
3.173 +"----------- rateq.sml end--------";