1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/sml/kbtest/rational.sml Thu Apr 17 18:01:03 2003 +0200
1.3 @@ -0,0 +1,1005 @@
1.4 +(*.tests for rationals
1.5 + Stefan Karnel
1.6 + 2002
1.7 + use"../kbtest/rational.sml";
1.8 + use"kbtest/rational.sml";
1.9 + use"rational.sml";
1.10 +.*)
1.11 +
1.12 +
1.13 +(*. tests of internal functions: to make them work,
1.14 + out-comment (*!!!*) in knowledge/Rational.ML:
1.15 +(*!!!
1.16 +structure RationalI : RATIONALI =
1.17 +struct
1.18 +!!!*)
1.19 +
1.20 +(*!!!
1.21 +end;(*struct*)
1.22 +open RationalI;
1.23 +!!!*)
1.24 +
1.25 +print("\n\n********************* rational.sml - TESTS *************************\n\n");
1.26 +print("\n\n***** divide tests *****\n");
1.27 +val mv_pquot1 = (#1(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
1.28 +(* result: [(1,[0,0,1]),(1,[0,0,0])] *)
1.29 +if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.30 +
1.31 +val mv_prest1 = (#2(mv_division([(1,[1,1,1]),(1,[1,1,0]),(1,[1,0,1]),(1,[0,0,0])],[(1,[1,1,0]),(1,[0,0,0])],LEX_)));
1.32 +(* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
1.33 +if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.34 +
1.35 +val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.36 +(* result: [(4,[1]),(4,[0])] *)
1.37 +if mv_pquot2=[(4,[1]),(4,[0])] then () else raise error ("rational.sml: example failed");
1.38 +
1.39 +val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.40 +(* result: [(12,[0]] *)
1.41 +if mv_prest2=[(12,[0])] then () else raise error ("rational.sml: example failed");
1.42 +
1.43 +val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
1.44 +(* [(2,[1]),(~2,[0])] *)
1.45 +if mv_pquot3=[(2,[1]),(~2,[0])] then () else raise error ("rational.sml: example failed");
1.46 +
1.47 +val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
1.48 +(* [(1,[2]),(~1,[0])] *)
1.49 +if mv_prest3=[(1,[2]),(~1,[0])] then () else raise error ("rational.sml: example failed");
1.50 +
1.51 +val mv_pquot4 = (#1(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1])],[(2,[1,0,0]),(4,[0,0,1])],LEX_)));
1.52 +(* [(1,[0,1,1])] *)
1.53 +if mv_pquot4=[(1,[0,1,1])] then () else raise error ("rational.sml: example failed");
1.54 +
1.55 +val mv_prest4 = (#2(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1])],[(2,[1,0,0]),(4,[0,0,1])],GGO_)));
1.56 +(* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
1.57 +if mv_prest4 =[(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.58 +
1.59 +val mv_pquot5 = (#1(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1]),(6,[2,1,3]),(4,[0,4,1]),(1,[2,2,1])],[(1,[0,0,1])],LEX_)));
1.60 +(* [(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])]*)
1.61 +if mv_pquot5=[(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.62 +
1.63 +val mv_prest5 = (#2(mv_division([(3,[1,1,1]),(4,[1,0,1]),(3,[0,0,1]),(6,[2,1,3]),(4,[0,4,1]),(1,[2,2,1])],[(1,[0,0,1])],LEX_)));
1.64 +(* [] *)
1.65 +if mv_prest5=[] then () else raise error ("rational.sml: example failed");
1.66 +
1.67 +(* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
1.68 +val mv_pquot6 = (#1(mv_division([(1,[2,0,0]),(2,[1,1,0]),(2,[1,0,0]),(1,[0,2,0]),(2,[0,1,0]),(1,[0,0,0])],[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])],LEX_)));
1.69 +if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.70 +
1.71 +val mv_prest6 = (#2(mv_division([(1,[2,0,0]),(2,[1,1,0]),(2,[1,0,0]),(1,[0,2,0]),(2,[0,1,0]),(1,[0,0,0])],[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])],LEX_)));
1.72 +if mv_prest6=[] then () else raise error ("rational.sml: example failed");
1.73 +
1.74 +
1.75 +print("\n\n***** MV_CONTENT-TESTS *****\n");
1.76 +val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.77 +(* [(1,[0,1]),(1,[0,0])] *)
1.78 +if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.79 +
1.80 +val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.81 +(*[(1,[1,0]),(1,[0,0])]*)
1.82 +if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.83 +
1.84 +val mv_cont2=mv_content([(2,[1]),(4,[0])]);
1.85 +(* [(2,[0])] *)
1.86 +if mv_cont2=[(2,[0])] then () else raise error ("rational.sml: example failed");
1.87 +
1.88 +val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
1.89 +(* [(1,[1]),(2,[0])] *)
1.90 +if mv_pp2=[(1,[1]),(2,[0])] then () else raise error ("rational.sml: example failed");
1.91 +
1.92 +val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.93 +(* [(2,[0,0,0])] *)
1.94 +if mv_cont3=[(2,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.95 +
1.96 +val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.97 +(* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
1.98 +if mv_pp3=[(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] then () else raise error ("rational.sml: example failed");
1.99 +
1.100 +val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.101 +(* [(1,[0,0,0])] *)
1.102 +if mv_cont4=[(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.103 +
1.104 +val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.105 +(* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
1.106 +if mv_pp4=[(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.107 +
1.108 +val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.109 +(* [(3,[0,0])] *)
1.110 +if con1=[(3,[0,0])] then () else raise error ("rational.sml: example failed");
1.111 +
1.112 +val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.113 +(* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
1.114 +if pp1=[(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] then () else raise error ("rational.sml: example failed");
1.115 +
1.116 +val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.117 +(* [(1,[0,0])] *)
1.118 +if con2=[(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.119 +
1.120 +val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.121 +(* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
1.122 +if pp2=[(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] then () else raise error ("rational.sml: example failed");
1.123 +
1.124 +val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
1.125 +(* [(3,[0,1,0])] *)
1.126 +if cont1=[(3,[0,1,0])] then () else raise error ("rational.sml: example failed");
1.127 +
1.128 +val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
1.129 +(* [(1,[2,0,0])] *)
1.130 +if pp1=[(1,[2,0,0])] then () else raise error ("rational.sml: example failed");
1.131 +
1.132 +val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
1.133 +(* [(2,[0,1,0])] *)
1.134 +if cont2=[(2,[0,1,0])] then () else raise error ("rational.sml: example failed");
1.135 +
1.136 +val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
1.137 +(* [(1,[2,0,0]),(2,[1,1,0])] *)
1.138 +if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else raise error ("rational.sml: example failed");
1.139 +
1.140 +print("\n\n\n\n********************************************************\n\n");
1.141 +val cont3=mv_content [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
1.142 +if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
1.143 +val pp3=mv_pp [(65,[3,2,2]),(52,[3,2,1]),(26,[3,1,2]),(~95,[2,2,3]),(~76,[2,2,2]),(35,[2,2,1]),(28,[2,2,0]),(~38,[2,1,3]),(14,[2,1,1])];
1.144 +
1.145 +---------------------------------------------------------------------------*)
1.146 +
1.147 +fun parse_rat str = (term_of o the o (parse thy)) str;
1.148 +
1.149 +print("\n\n***** mv_gcd-tests *****\n");
1.150 +val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
1.151 +(* [(2,[1,1]),(2,[0,0])] *)
1.152 +if ggt1=[(2,[1,1]),(2,[0,0])] then () else raise error ("rational.sml: example failed");
1.153 +
1.154 +val ggt2 = mv_gcd [(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(15,[1,1,1])] [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.155 +(* [(2,[1,1,0]),(3,[0,0,1])] *)
1.156 +if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.157 +
1.158 +
1.159 +val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.160 +(* [(1,[1,0]),(~1,[0,1])] *)
1.161 +if ggt3=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
1.162 +
1.163 +
1.164 +val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
1.165 +(* [(1,[1,0,0])] *)
1.166 +if ggt4=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
1.167 +
1.168 +
1.169 +val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.170 +(* [(1,[1,0]),(~1,[0,1])] *)
1.171 +if ggt5=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
1.172 +
1.173 +
1.174 +val ggt6 = mv_gcd [(10,[2,1,1]),(14,[1,1,0]),(3,[1,0,1]),(20,[1,2,1])] [(5,[1,1,1]),(7,[2,1,1])];
1.175 +(* [(1,[0,0,0])] *)
1.176 +if ggt6=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
1.177 +
1.178 +print("\n\n***** kgv-tests *****\n");
1.179 +val kgv1=mv_lcm [(10,[])] [(15,[])];
1.180 +(* [(30,[])] *)
1.181 +if kgv1=[(30,[])] then () else raise error ("rational.sml: example failed");
1.182 +
1.183 +val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.184 +(* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
1.185 +if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else raise error ("rational.sml: example failed");
1.186 +
1.187 +val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.188 +(* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
1.189 +if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else raise error ("rational.sml: example failed");
1.190 +
1.191 +(*!!!--------
1.192 +print("\n\n***** STEP_CANCEL_TESTS: *****\n");
1.193 +
1.194 +val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) / (6 * a * c)";
1.195 +val div2 = term2str (step_cancel term2);
1.196 +if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else raise error ("rational.sml: example failed");
1.197 +
1.198 +
1.199 +val term1 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) / a";
1.200 +val div1 = term2str(step_cancel term1);
1.201 +if div1 = "(3 * c + 14 * b + 20 * (b ^^^ 2 * c) + 10 * (a * (b * c))) * a / (1 * a)" then () else raise error ("rational.sml: example failed");
1.202 +
1.203 +val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
1.204 +val div3 = term2str(step_cancel term3);
1.205 +if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else raise error ("rational.sml: example failed");
1.206 +
1.207 +--------------------------------------------------------------------------!!!*)
1.208 +
1.209 +(*-----versuche 13.3.03-----
1.210 + val t = str2term "1 - x^^^2 - 5 * x^^^5";
1.211 + val vs=(((map free2str) o vars) t);
1.212 + val Some ml = expanded2poly t vs;
1.213 + poly2term (ml, vs);
1.214 + poly2term'(rev(sort (mv_geq LEX_) (ml)),vs);
1.215 + poly2term'([(~5,[5]),(~1,[2]),(1,[0])], vs);
1.216 + monom2term((~5,[5]),vs);
1.217 + monom2term((~1,[2]),vs);
1.218 + val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
1.219 +
1.220 + val (i,is) = (~1,[2]);
1.221 + val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
1.222 + (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
1.223 + Free ((str_of_int o abs) i, HOLogic.realT)) $
1.224 + powerproduct2term(is, vs);
1.225 + term2str ttt;
1.226 +-------versuche 13.3.03-----*)
1.227 +
1.228 + val t = str2term "1 - x^^^2 - 5 * x^^^5";
1.229 + val Some t' = expanded2polynomial t; term2str t';
1.230 +"1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5";
1.231 + val t = str2term "1 - x";
1.232 + val Some t' = expanded2polynomial t; term2str t';
1.233 +"1 + - 1 * x";
1.234 + val t = str2term "1 + (-1) * x";
1.235 + val Some t' = expanded2polynomial t; term2str t';
1.236 +"1 + - 1 * x";
1.237 + val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5";
1.238 + val Some t' = polynomial2expanded t; term2str t';
1.239 +"1 - x ^^^ 2 - 5 * x ^^^ 5";
1.240 +
1.241 +
1.242 +" external calculating functions test ";
1.243 +" external calculating functions test ";
1.244 +" external calculating functions test ";
1.245 +
1.246 +val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.247 +val Some (t1',asm)= factout_p_ thy t1;
1.248 +term2str t1'; terms2str asm;
1.249 +"(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))";
1.250 +"[]";
1.251 +val Some (t1',asm)= cancel_p_ thy t1;
1.252 +term2str t1'; terms2str asm;
1.253 +"(3 + 3 * x) / 2";
1.254 +"[\"1 + 1 * x ~= 0\"]";
1.255 +
1.256 +val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
1.257 +val Some (t',asm)= cancel_ thy t;
1.258 +term2str t'; terms2str asm;
1.259 +"(3 - 3 * x) / 2";
1.260 +"[\"-1 + x ~= 0\"]";
1.261 +val Some (t',asm)= factout_ thy t;
1.262 +term2str t'; terms2str asm;
1.263 +"(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))";
1.264 +"[]";
1.265 +
1.266 +val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.267 +val Some (t',asm) = add_fraction_p_ thy t;
1.268 +term2str t'; terms2str asm;
1.269 +"(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)";
1.270 +"[]";
1.271 +val Some (t',asm) = common_nominator_p_ thy t;
1.272 +term2str t'; terms2str asm;
1.273 +"(-1 + 1 * x) * (-1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x)) +\n(1 + 1 * x) * (1 + 1 * x) / ((1 + 1 * x) * (-1 + 1 * x))";
1.274 +"[]";
1.275 +
1.276 +val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
1.277 +val Some (t',asm) = add_fraction_ thy t;
1.278 +term2str t'; terms2str asm;
1.279 +"(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)";
1.280 +"[]";
1.281 +val Some (t',asm) = common_nominator_ thy t;
1.282 +term2str t'; terms2str asm;
1.283 +"(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))";
1.284 +"[]";
1.285 +
1.286 +val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
1.287 +val Some (t',asm) = common_nominator_p_ thy t;
1.288 +term2str t'; terms2str asm;
1.289 +"1 * (1 + -2 * x + 1 * x ^^^ 2) /\n((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n(1 * (-1 + 1 * x ^^^ 2) /\n ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n (1 * (-2 + 2 * x) / ((-1 + 1 * x) * (2 * ((-1 + 1 * x) * (1 + 1 * x)))) +\n 1 * (#";
1.290 +"[]";
1.291 +val Some (t',asm) = add_fraction_p_ thy t;
1.292 +term2str t'; terms2str asm;
1.293 +"1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
1.294 +"[\"1 + 1 * x ~= 0\"]";
1.295 +val Some(t',asm) = norm_rational_ thy t;
1.296 +term2str t'; terms2str asm;
1.297 +"1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
1.298 +"[\"1 + 1 * x ~= 0\"]";
1.299 +
1.300 +val t3 = (term_of o the o (parse thy)) "((1) / (2*x + 2)) + ((1) / (2*x - 2)) + ((1) / ( x^^^2 - 1))+((1) / (x^^^2 - 2 * x + 1))";
1.301 +val Some (t3',_) = common_nominator_ thy t3;
1.302 +val Some (t3'',_) = add_fraction_ thy t3;
1.303 +(term2str t3');
1.304 +(term2str t3'');
1.305 +
1.306 +val Some(t4,t5) = norm_expanded_rat_ thy t3;
1.307 +term2str t4;
1.308 +term2str (hd(t5));
1.309 +
1.310 +
1.311 +
1.312 + val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
1.313 + val Some (t',_) = factout_ thy t;
1.314 + val Some (t'',_) = cancel_ thy t;
1.315 + term2str t';
1.316 + term2str t'';
1.317 + "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
1.318 + "(3 + x) / (3 - x)";
1.319 +
1.320 + val t=(term_of o the o (parse thy))
1.321 + "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)";
1.322 + val Some (t',_) = common_nominator_ thy t;
1.323 + val Some (t'',_) = add_fraction_ thy t;
1.324 + term2str t';
1.325 + term2str t'';
1.326 + "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))";
1.327 + "(4 + x) / (3 - x)";
1.328 +
1.329 + (*WN.16.10.02 hinzugef"ugt -----vv---*)
1.330 + val t=(term_of o the o (parse thy))
1.331 + "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
1.332 + val Some (t',_) = common_nominator_ thy t;
1.333 + val Some (t'',_) = add_fraction_ thy t;
1.334 + term2str t';
1.335 + term2str t'';
1.336 + "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\
1.337 + \1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.338 + "6 / (3 - x)";
1.339 +
1.340 + val t=(term_of o the o (parse thy))
1.341 + "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
1.342 + val Some (t',_) = common_nominator_ thy t;
1.343 + val Some (t'',_) = add_fraction_ thy t;
1.344 + term2str t';
1.345 + term2str t'';
1.346 + "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\
1.347 + \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.348 + "6 / (3 - x)";
1.349 + (*WN.16.10.02 hinzugef"ugt -----^^---*)
1.350 +
1.351 + val t=(term_of o the o (parse thy))
1.352 + "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
1.353 + val Some (t',_) = factout_ thy t;
1.354 + val Some (t'',_) = cancel_ thy t;
1.355 + term2str t';
1.356 + term2str t'';
1.357 + "(y + x) * (y - x) / ((y - x) * (y - x))";
1.358 + "(y + x) / (y - x)";
1.359 +
1.360 + val t=(term_of o the o (parse thy))
1.361 + "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
1.362 + val Some (t',_) = common_nominator_ thy t;
1.363 + val Some (t'',_) = add_fraction_ thy t;
1.364 + term2str t';
1.365 + term2str t'';
1.366 + "((-1) * x ^^^ 2 + y ^^^ 2) / (((-1) * x + y) * ((-1) * x + y)) +\
1.367 + \1 * ((-1) * x + y) / (((-1) * x + y) * ((-1) * x + y))";
1.368 + "((-1) - x - y) / (x - y)";
1.369 + (*WN.16.10.02 ^^^^^^^ Reihenfolge aus Angabe umgekehrt ?!*)
1.370 +
1.371 + val t=(term_of o the o (parse thy))
1.372 + "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
1.373 + val Some (t',_) = common_nominator_ thy t;
1.374 + val Some (t'',_) = add_fraction_ thy t;
1.375 + term2str t';
1.376 + term2str t'';
1.377 + "((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
1.378 + \1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
1.379 + "((-1) - y - x) / (y - x)";
1.380 + (*WN.16.10.02 ^^^^^^^ lexicographische Ordnung ?!*)
1.381 +
1.382 + val t=(term_of o the o (parse thy))
1.383 + "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
1.384 + val Some (t',_) = norm_expanded_rat_ thy t;
1.385 + term2str t';
1.386 + "(y + x) / (y - x)";
1.387 +(*val Some (t'',_) = norm_rational_ thy t;
1.388 + term2str t'';
1.389 + *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
1.390 + WN.16.10.02 ?!*)
1.391 +
1.392 + val t=(term_of o the o (parse thy))
1.393 + "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
1.394 + val Some (t',_) = norm_expanded_rat_ thy t;
1.395 + term2str t';
1.396 + "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
1.397 +(*val Some (t'',_) = norm_rational_ thy t;
1.398 + term2str t'';
1.399 + *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
1.400 + WN.16.10.02 ?!*)
1.401 +
1.402 + val t=(term_of o the o (parse thy))
1.403 + "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
1.404 + val Some (t',_) = norm_expanded_rat_ thy t;
1.405 + val Some (t'',_) = norm_rational_ thy t;
1.406 + term2str t';
1.407 + term2str t'';
1.408 + "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
1.409 + "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)";
1.410 +
1.411 +
1.412 +" examples from: Mathematik 1 Schalk Reniets Verlag ";
1.413 +" examples from: Mathematik 1 Schalk Reniets Verlag ";
1.414 +" examples from: Mathematik 1 Schalk Reniets Verlag ";
1.415 +
1.416 +
1.417 +"------------------ cancel -----------------------";
1.418 +"------------------ cancel -----------------------";
1.419 +"------------------ cancel -----------------------";
1.420 +val thy' = "Rational.thy";
1.421 +val rls' = "cancel";
1.422 +val mp = "make_polynomial";
1.423 +
1.424 +print("\n\nexample 186:\n");
1.425 +print("a)\n");
1.426 +val e186a'="(14 * x * y) / ( x * y )";
1.427 +val e186a = the (rewrite_set thy' false "cancel" e186a');
1.428 + is_expanded (parse_rat "14 * x * y");
1.429 + is_expanded (parse_rat "x * y");
1.430 +
1.431 +print("b)\n");
1.432 +val e186b'="(60 * a * b) / ( 15 * a * b )";
1.433 +val e186b = the (rewrite_set thy' false "cancel" e186b');
1.434 +print("c)\n");
1.435 +val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
1.436 +val e186c = (the (rewrite_set thy' false "cancel" e186c'))
1.437 + handle e => print_exn e;
1.438 +val t = (term_of o the o (parse thy)) e186c';
1.439 +atomt t;
1.440 +
1.441 +print("\n\nexample 187:\n");
1.442 +print("a)\n");
1.443 +val e187a'="(12 * x * y) / (8 * y^^^2 )";
1.444 +val e187a = the (rewrite_set thy' false "cancel" e187a');
1.445 +print("b)\n");
1.446 +val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
1.447 +val e187b = the (rewrite_set thy' false "cancel" e187b');
1.448 +print("c)\n");
1.449 +val e187c'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";
1.450 +val e187c = the (rewrite_set thy' false "cancel" e187c');
1.451 +
1.452 +"example 188:";
1.453 +val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";
1.454 +val e188a = the (rewrite_set thy' false "cancel" e188a');
1.455 + is_expanded (parse_rat "8 * x + -8");
1.456 +(* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
1.457 +if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
1.458 +else raise error "rationals.sml: e188a new behaviour";
1.459 +val Some (t,_) = rewrite_set thy' false mp
1.460 + "(8*((-1) + x))/(9*((-1) + x))";
1.461 +print("b)\n");
1.462 +val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";
1.463 +val Some (t,_) = rewrite_set thy' false "cancel" e188b';
1.464 +print("c)\n");
1.465 +(*WN.23.10.02-------
1.466 +val e188c'="( a + -1 * b ) / ( b + -1 * a )";
1.467 +val e188c = the (rewrite_set thy' false "cancel" e188c');
1.468 + is_expanded (parse_rat "a + -1 * b");
1.469 + false; -----------!!!*)
1.470 +val Some (t,_) =
1.471 + rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
1.472 +if t= "(-1 * b + a) / (b + -1 * a)" then()
1.473 +else raise error "rationals.sml: e188c new behaviour";
1.474 +
1.475 +print("\n\nexample 190:\n");
1.476 +print("c)\n");
1.477 +val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
1.478 +val e190c = the (rewrite_set thy' false "cancel" e190c');
1.479 +val Some (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1.480 +(* t="(1 + (3 * a + (27 * a ^^^ 3 + 9 * a ^^^ 2))) /\n(3 * a + (18 * a ^^^ 2 + 27 * a ^^^ 3))"then()
1.481 + WN:TERMORDER ~~~~~~~ ~~~~~~~ f"ur Matthias Goldgruber*)
1.482 +if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
1.483 +else raise error "rationals.sml: e190c new behaviour";
1.484 +
1.485 +print("\n\nexample 191:\n");
1.486 +print("a)\n");
1.487 +val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )";
1.488 +(*WN.23.10.02-------
1.489 +val e191a = the (rewrite_set thy' false "cancel" e191a');
1.490 + is_expanded (parse_rat "x^^^2 + -1 * y^^^2");
1.491 + false;
1.492 + is_expanded (parse_rat "x + y");
1.493 + true; -----------*)
1.494 +val Some (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
1.495 +(* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
1.496 +if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
1.497 +else raise error "rationals.sml: e191a new behaviour";
1.498 +
1.499 +print("c)\n");
1.500 +val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
1.501 +(*WN.23.10.02-------
1.502 +val e191c = the (rewrite_set thy' false "cancel" e191c');
1.503 + is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25");
1.504 + false;
1.505 + is_expanded (parse_rat "25 + -30*x + 9*x^^^2");
1.506 + false;
1.507 + is_expanded (parse_rat "-25 + 9*x^^^2");
1.508 + true;------------*)
1.509 +val Some (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
1.510 +(* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
1.511 +if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
1.512 +else raise error "rationals.sml: 'e191c' new behaviour";
1.513 +
1.514 +
1.515 +print("\n\nexample 192:\n");
1.516 +print("b)\n");
1.517 +val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
1.518 +(*WN.23.10.02-------
1.519 +val e192b = the (rewrite_set thy' false "cancel" e192b');
1.520 +-------------------*)
1.521 +val Some (t,_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.522 +(* t="(7 * x ^^^ 3 + -1 * (y * x ^^^ 2)) / (-1 * y ^^^ 3 + 7 * (x * y ^^^ 2))"then()
1.523 + TERMORDER ~~~~~ f"ur Matthias Goldgruber*)
1.524 +if t = "(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"
1.525 +then () else raise error "rationals.sml: 'e192b' new behaviour";
1.526 +
1.527 +print("\n\nexample 193:\n");
1.528 +print("a)\n");
1.529 +val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
1.530 +(*WN.23.10.02-------
1.531 +val e193a = the (rewrite_set thy' false "cancel" e193a');
1.532 +-------------------*)
1.533 +print("b)\n");
1.534 +val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
1.535 +(*WN.23.10.02-------
1.536 +val e193b = the (rewrite_set thy' false "cancel" e193b');
1.537 +print("c)\n");
1.538 +val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
1.539 +val Some(t,_) = rewrite_set thy' false "cancel" e193c';
1.540 +-------------------*)
1.541 +
1.542 +val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
1.543 +val Some (t,_) = rewrite_set thy' false "cancel" wn01;
1.544 +(* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
1.545 +if t = "(-5 + 3 * x) / 1" then ()
1.546 +else raise error "rational.sml: new behav. in cancel wn01";
1.547 +
1.548 +
1.549 +"------------------ common_nominator_p -----------------------";
1.550 +"------------------ common_nominator_p -----------------------";
1.551 +"------------------ common_nominator_p -----------------------";
1.552 +val rls' = "common_nominator_p";
1.553 +
1.554 +print("\n\nexample 204:\n");
1.555 +print("a)\n");
1.556 +val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)";
1.557 +val e204a = the (rewrite_set thy' false "common_nominator_p" e204a');
1.558 +print("b)\n");
1.559 +val e204b'="5 / x + -3 / x + -1 / x";
1.560 +val e204b = the (rewrite_set thy' false "common_nominator_p" e204b');
1.561 +
1.562 +print("\n\nexample 205:\n");
1.563 +print("a)\n");
1.564 +val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)";
1.565 +val e205a = the (rewrite_set thy' false "common_nominator_p" e205a');
1.566 +print("b)\n");
1.567 +val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)";
1.568 +val e205b = the (rewrite_set thy' false "common_nominator_p" e205b');
1.569 +
1.570 +print("\n\nexample 206:\n");
1.571 +print("a)\n");
1.572 +val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))";
1.573 +val e206a = the (rewrite_set thy' false "common_nominator_p" e206a');
1.574 +print("b)\n");
1.575 +val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))";
1.576 +val e206b = the (rewrite_set thy' false "common_nominator_p" e206b');
1.577 +
1.578 +print("\n\nexample 207:\n");
1.579 +val e207'="((3 * x * y + 3 * y) / (x * y)) + ((5 * x * y + 7 * y) / (x * y)) + ((9 * x * y + -2 * y) / (x * y)) + ((x * y + 4 * y) / (x * y)) ";
1.580 +val e207 = the (rewrite_set thy' false "common_nominator_p" e207');
1.581 +
1.582 +print("\n\nexample 208:\n");
1.583 +val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) ";
1.584 +val e208 = the (rewrite_set thy' false "common_nominator_p" e208');
1.585 +
1.586 +print("\n\nexample 209:\n");
1.587 +val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) ";
1.588 +val e209 = the (rewrite_set thy' false "common_nominator_p" e209');
1.589 +
1.590 +print("\n\nexample 210:\n");
1.591 +val e210'="((2 * x + 3 + -1 * x^^^2) / (5 * x)) + ((5 * x^^^2 + -2 * x + 1) / (5 * x)) + ((-3 * x^^^2 + -2 * x + 1) / (5 * x)) + ((-1 * x^^^2 + -3 * x + -5) / (5 * x)) ";
1.592 +val e210 = the (rewrite_set thy' false "common_nominator_p" e210');
1.593 +
1.594 +print("\n\nexample 211:\n");
1.595 +print("a)\n");
1.596 +val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))";
1.597 +val e211a = the (rewrite_set thy' false "common_nominator_p" e211a');
1.598 +print("b)\n");
1.599 +val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))";
1.600 +val e211b = the (rewrite_set thy' false "common_nominator_p" e211b');
1.601 +
1.602 +print("\n\nexample 212:\n");
1.603 +print("a)\n");
1.604 +val e212a'="((4) / (x)) + ((-3) / (y)) + -1";
1.605 +val e212a = the (rewrite_set thy' false "common_nominator_p" e212a');
1.606 +print("b)\n");
1.607 +val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))";
1.608 +val e212b = the (rewrite_set thy' false "common_nominator_p" e212b');
1.609 +
1.610 +print("\n\nexample 213:\n");
1.611 +print("a)\n");
1.612 +val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) ";
1.613 +val e213a = the (rewrite_set thy' false "common_nominator_p" e213a');
1.614 +print("b)\n");
1.615 +val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))";
1.616 +val e213b = the (rewrite_set thy' false "common_nominator_p" e213b');
1.617 +
1.618 +print("\n\nexample 214:\n");
1.619 +print("a)\n");
1.620 +val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))";
1.621 +val e214a = the (rewrite_set thy' false "common_nominator_p" e214a');
1.622 +print("b)\n");
1.623 +val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))";
1.624 +val e214b = the (rewrite_set thy' false "common_nominator_p" e214b');
1.625 +
1.626 +print("\n\nexample 216:\n");
1.627 +print("a)\n");
1.628 +val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))";
1.629 +val e216a = the (rewrite_set thy' false "common_nominator_p" e216a');
1.630 +print("b)\n");
1.631 +val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))";
1.632 +val e216b = the (rewrite_set thy' false "common_nominator_p" e216b');
1.633 +
1.634 +print("\n\nexample 217:\n");
1.635 +val e217'="((z + -1) / (z)) + ((3 * z ^^^2 + -6 * z + 5) / (z^^^2)) + ((-4 * z^^^3 + 7 * z^^^2 + -5 * z + 5) / (z^^^3))";
1.636 +val e217 = the (rewrite_set thy' false "common_nominator_p" e217');
1.637 +
1.638 +
1.639 +val rls' = "common_nominator";
1.640 +print("\n\nexample 218:\n");
1.641 +val e218'="((9 * a^^^3 - 5 * a^^^2 + 2 * a + 8) / (108 * a^^^4)) + ((-5 * a + 3 * a^^^2 + 4) / (8 * a^^^3)) + ((-261 * a^^^3 + 19 * a^^^2 + -112 * a + 16) / (216 * a^^^4))";
1.642 +val e218 = the (rewrite_set thy' false "common_nominator" e218');
1.643 +
1.644 +print("\n\nexample 219:\n");
1.645 +print("a)\n");
1.646 +val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))";
1.647 +val e219a = the (rewrite_set thy' false "common_nominator" e219a');
1.648 +print("b)\n");
1.649 +val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))";
1.650 +val e219b = the (rewrite_set thy' false "common_nominator" e219b');
1.651 +
1.652 +print("\n\nexample 220:\n");
1.653 +print("a)\n");
1.654 +val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))";
1.655 +val e220a = the (rewrite_set thy' false "common_nominator" e220a');
1.656 +print("b)\n");
1.657 +val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))";
1.658 +val e220b = the (rewrite_set thy' false "common_nominator" e220b');
1.659 +
1.660 +print("\n\nexample 221:\n");
1.661 +print("a)\n");
1.662 +val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))";
1.663 +val e221a = the (rewrite_set thy' false "common_nominator" e221a');
1.664 +print("b)\n");
1.665 +val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) ";
1.666 +val e221b = the (rewrite_set thy' false "common_nominator" e221b');
1.667 +
1.668 +print("\n\nexample 222:\n");
1.669 +print("a)\n");
1.670 +val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))";
1.671 +val e222a = the (rewrite_set thy' false "common_nominator" e222a');
1.672 +print("b)\n");
1.673 +val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))";
1.674 +val e222b = the (rewrite_set thy' false "common_nominator" e222b');
1.675 +
1.676 +print("\n\nexample 225:\n");
1.677 +print("a)\n");
1.678 +val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))";
1.679 +val e225a = the (rewrite_set thy' false "common_nominator" e225a');
1.680 +print("b)\n");
1.681 +val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))";
1.682 +val e225b = the (rewrite_set thy' false "common_nominator" e225b');
1.683 +
1.684 +print("\n\nexample 226:\n");
1.685 +print("a)\n");
1.686 +val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) ";
1.687 +val e226a = the (rewrite_set thy' false "common_nominator" e226a');
1.688 +print("b)\n");
1.689 +val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2";
1.690 +val e226b = the (rewrite_set thy' false "common_nominator" e226b');
1.691 +
1.692 +print("\n\nexample 227:\n");
1.693 +print("a)\n");
1.694 +val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 ";
1.695 +val e227a = the (rewrite_set thy' false "common_nominator" e227a');
1.696 +print("b)\n");
1.697 +val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 ";
1.698 +val e227b = the (rewrite_set thy' false "common_nominator" e227b');
1.699 +
1.700 +print("\n\nexample 228:\n");
1.701 +print("a)\n");
1.702 +val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))";
1.703 +val e228a = the (rewrite_set thy' false "common_nominator" e228a');
1.704 +print("b)\n");
1.705 +val e228b'="((11 * z + 2 * b) / (4 * b * z + -8 * b^^^2)) + ((-8 * z) / (z^^^2 + -4 * b^^^2)) + ((-9 * z + -2 * b) / (4 * b * z + 8 * b^^^2))";
1.706 +val e228b = the (rewrite_set thy' false "common_nominator" e228b');
1.707 +
1.708 +
1.709 +print("\n\nexample 229:\n");
1.710 +print("a)\n");
1.711 +val e229a'="((5 * x^^^2 + y) / (x + 2 * y)) + ((-8 * x^^^3 + 4 * x^^^2 * y + 3 * x * y) / (x^^^2 + -4 * y^^^2)) + ((3 * x^^^2 + -4 * y) / (x + -2 * y))";
1.712 +val e229a = the (rewrite_set thy' false "common_nominator" e229a');
1.713 +print("b)\n");
1.714 +val e229b'="((7 * x^^^2 + y) / (x + 3 * y)) + ((-24 * x^^^2 * y + 5 * x * y + 21 * y^^^2) / (x^^^2 + -9 * y^^^2)) + ((4 * x^^^2 + -6 * y) / (x + -3 * y))";
1.715 +val e229b = the (rewrite_set thy' false "common_nominator" e229b');
1.716 +
1.717 +print("\n\nexample 230:\n");
1.718 +print("a)\n");
1.719 +val e230a'="((5 * x^^^2 + y) / (2 * x + y)) + ((-16 * x^^^3 + 2 * x^^^2 * y + 6 * x * y) / (4 * x^^^2 + -1 * y^^^2)) + ((3 * x^^^2 + -4 * y) / (2 * x + -1 * y))";
1.720 +val e230a = the (rewrite_set thy' false "common_nominator" e230a');
1.721 +print("b)\n");
1.722 +val e230b'="((7 * x^^^2 + y) / (3 * x + y)) + ((-3 * x^^^3 + 15 * x * y + -7 * x^^^2 * y + 7 * y^^^2) / (9 * x^^^2 + -1 * y^^^2)) + ((4 * x^^^2 + -6 * y) / (3 * x + -1 * y))";
1.723 +val e230b = the (rewrite_set thy' false "common_nominator" e230b');
1.724 +
1.725 +print("\n\nexample 231:\n");
1.726 +print("a)\n");
1.727 +val e231a'="((2 * x + 5 * y) / (x)) + ((2 * x^^^3 + -5 * y^^^3 + 3 * x * y^^^2) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-3 * x + -6 * y) / (x + -1 * y))";
1.728 +val e231a = the (rewrite_set thy' false "common_nominator" e231a');
1.729 +print("b)\n");
1.730 +val e231b'="((6 * x + 2 * y) / (x)) + ((6 * x^^^2 * y + -4 * x * y^^^2 + -2 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-5 * x + -3 * y) / (x + -1 * y))";
1.731 +val e231b = the (rewrite_set thy' false "common_nominator" e231b');
1.732 +
1.733 +print("\n\nexample 232:\n");
1.734 +print("a)\n");
1.735 +val e232a'="((2 * x + 3 * y) / (x)) + ((4 * x^^^3 + -1 * x * y^^^2 + -3 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-5 * x + -6 * y) / (x + -1 * y))";
1.736 +val e232a = the (rewrite_set thy' false "common_nominator" e232a');
1.737 +print("b)\n");
1.738 +val e232b'="((5 * x + 2 * y) / (x)) + ((2 * x^^^3 + -3 * x * y^^^2 + 3 * x^^^2 * y + -2 * y^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-6 * x + -3 * y) / (x + -1 * y))";
1.739 +val e232b = the (rewrite_set thy' false "common_nominator" e232b');
1.740 +
1.741 +print("\n\nexample 233:\n");
1.742 +print("a)\n");
1.743 +val e233a'="((5 * x + 6 * y) / (x)) + ((5 * x * y^^^2 + -6 * y^^^3 + -2 * x^^^3 + 3 * x^^^2 * y) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-2 * x + -3 * y) / (x + -1 * y))";
1.744 +val e233a = the (rewrite_set thy' false "common_nominator" e233a');
1.745 +print("b)\n");
1.746 +val e233b'="((6 * x + 5 * y) / (x)) + ((4 * x^^^2 * y + 3 * x * y^^^2 + -5 * y^^^3 + -2 * x^^^3) / (x^^^3 + -2 * x^^^2 * y + x * y^^^2)) + ((-3 * x + -2 * y) / (x + -1 * y))";
1.747 +val e233b = the (rewrite_set thy' false "common_nominator" e233b');
1.748 +
1.749 +print("\n\nexample 234:\n");
1.750 +print("a)\n");
1.751 +val e234a'="((5 * a + b) / (2 * a * b + -2 * b^^^2)) + ((-3 * a + -1 * b) / (2 * a * b + 2 * b^^^2)) + ((-2 * a) / (a^^^2 + -1 * b^^^2))";
1.752 +val e234a = the (rewrite_set thy' false "common_nominator" e234a');
1.753 +print("b)\n");
1.754 +val e234b'="((5 * a + 3 * b) / (6 * a * b + -18 * b^^^2)) + ((-3 * a + -3 * b) / (6 * a * b + 18 * b^^^2)) + ((-2 * a) / (a^^^2 + -9 * b^^^2)) ";
1.755 +val e234b = the (rewrite_set thy' false "common_nominator" e234b');
1.756 +
1.757 +print("\n\nexample 235:\n");
1.758 +print("a)\n");
1.759 +val e235a'="((10 * x + 3 * y) / (12 * x * y + -18 * y^^^2)) + ((-6 * x + -3 * y) / (12 * x * y + 18 * y^^^2)) + ((-4 * x) / (4 * x^^^2 + -9 * y^^^2))";
1.760 +val e235a = the (rewrite_set thy' false "common_nominator" e235a');
1.761 +print("b)\n");
1.762 +val e235b'="((8 * a + b) / (4 * a * b + -2 * b^^^2)) + ((-4 * a + -1 * b) / (4 * a * b + 2 * b^^^2)) + ((-2 * a) / (4 * a^^^2 + -1 * b^^^2)) ";
1.763 +val e235b = the (rewrite_set thy' false "common_nominator" e235b');
1.764 +
1.765 +print("\n\nexample 236:\n");
1.766 +print("a)\n");
1.767 +val e236a'="((8 * a + 5 * b) / (20 * a * b + -50 * b^^^2)) + ((-4 * a + -5 * b) / (20 * a * b + 50 * b^^^2)) + ((-2 * a) / (4 * a^^^2 + -25 * b^^^2))";
1.768 +val e236a = the (rewrite_set thy' false "common_nominator" e236a');
1.769 +print("b)\n");
1.770 +val e236b'="((24 * x + y) / (6 * x * y + -2 * y^^^2)) + ((-18 * x + -1 * y) / (6 * x * y + 2 * y^^^2)) + ((-15 * x) / (9 * x^^^2 + -1 * y^^^2)) ";
1.771 +val e236b = the (rewrite_set thy' false "common_nominator" e236b');
1.772 +
1.773 +
1.774 +val rls' = "cancel";
1.775 +print("\n\nexample heuberger:\n");
1.776 +val eheu'="(x^^^4 + x * y + x^^^3 * y + y^^^2) / (x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)";
1.777 +val eheu = the (rewrite_set thy' false "cancel" eheu');
1.778 +
1.779 +val rls' = "common_nominator_p";
1.780 +print("\n\nexample stiefel:\n");
1.781 +val est1'="(7) / (-14) + (-2) / (4)";
1.782 +val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
1.783 +if est1 = ("-1 / 1",[]) then ()
1.784 +else raise error "new behaviour in rationals.sml: est1'";
1.785 +
1.786 +val t = (term_of o the o (parse thy))
1.787 +"(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.788 +val Some (t',_) = factout_ thy t;
1.789 +term2str t';
1.790 +"(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
1.791 +
1.792 +
1.793 +(*WN.28.8.02: tests for the 'reverse-rewrite' functions:
1.794 + these are defined in Rationals.ML and stored in
1.795 + the 'reverse-ruleset' cancel*)
1.796 +
1.797 +(*the term for which reverse rewriting is demonstrated*)
1.798 + val t = (term_of o the o (parse thy))
1.799 + "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
1.800 + val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.801 + next_rule=nex,normal_form=nor,...},...} = cancel;
1.802 +
1.803 +(*normal_form produces the result in ONE step*)
1.804 + val Some (t',_) = nor t;
1.805 + term2str t';
1.806 +
1.807 +(*initialize the interpreter state used by the 'me'*)
1.808 + val (t,_,revsets,_) = ini t;
1.809 +
1.810 +(*find the rule 'r' to apply to term 't'*)
1.811 + val Some r = nex revsets t;
1.812 + (*val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
1.813 +
1.814 +(*check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
1.815 + if the rule is OK, the term resulting from applying the rule is returned,too;
1.816 + there might be several rule applications inbetween,
1.817 + which are listed after the thead in reverse order*)
1.818 + val (r,(t,asm))::_ = loc revsets t r;
1.819 + term2str t;
1.820 + "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
1.821 +
1.822 +(*find the next rule to apply*)
1.823 + val Some r = nex revsets t;
1.824 + (*val r = Thm ("sym_#power_3_2","9 = 3 ^^^ 2") : rule*)
1.825 +
1.826 +(*check the next rule*)
1.827 + val (r,(t,asm))::_ = loc revsets t r;
1.828 + term2str t;
1.829 + "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
1.830 +
1.831 +(*find and check the next rules, rewrite*)
1.832 + val Some r = nex revsets t;
1.833 + val (r,(t,asm))::_ = loc revsets t r;
1.834 + term2str t;
1.835 + "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
1.836 +
1.837 + val Some r = nex revsets t;
1.838 + val (r,(t,asm))::_ = loc revsets t r;
1.839 + term2str t;
1.840 + "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
1.841 +
1.842 + val Some r = nex revsets t;
1.843 + val (r,(t,asm))::_ = loc revsets t r;
1.844 + term2str t;
1.845 + "(3 - x) * (3 + x) / ((3 + x) * (3 + x))";
1.846 +
1.847 + val Some r = nex revsets t;
1.848 + val (r,(t,asm))::_ = loc revsets t r;
1.849 + val ss = term2str t;
1.850 + if ss = "(3 - x) / (3 + x)" then ()
1.851 + else raise error "rational.sml: new behav. in rev-set cancel";
1.852 + terms2str asm;
1.853 +
1.854 +
1.855 +
1.856 +(*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
1.857 +
1.858 + (*the term for which reverse rewriting is demonstrated*)
1.859 + val t = (term_of o the o (parse thy))
1.860 + "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
1.861 + val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.862 + next_rule=nex,normal_form=nor,...},...} = cancel_p;
1.863 + (*normal_form produces the result in ONE step*)
1.864 + val Some (t',_) = nor t;
1.865 + term2str t';
1.866 + (*initialize the interpreter state used by the 'me'*)
1.867 +(* WN.14.3.03: rewrite__ Thm | Calc | missing: Rls_ FIXXXXME --------
1.868 + val (t,_,revsets,_) = ini t;
1.869 +---------------------------------------------------------------------*)
1.870 +
1.871 +(*
1.872 + val [rs] = revsets;
1.873 + filter_out (eq_Thms ["sym_real_add_zero_left",
1.874 + "sym_real_mult_0",
1.875 + "sym_real_mult_1"]) rs;
1.876 +
1.877 + 10.10.02: dieser Fall terminiert nicht (make_poly enth"alt zu viele rules)
1.878 + val Some r = nex revsets t;
1.879 + val (r,(t,asm))::_ = loc revsets t r;
1.880 + term2str t;
1.881 +
1.882 + val Some r = nex revsets t;
1.883 + val (r,(t,asm))::_ = loc revsets t r;
1.884 + term2str t;
1.885 +
1.886 + ------ revset ----------------------------------------------------
1.887 +/// [Thm ("sym_real_add_zero_left","?z = 0 + ?z"),
1.888 +/// Thm ("sym_real_mult_0","0 = 0 * ?z"),
1.889 +! Thm ("sym_#mult_2_(-3)","(-6) * x = 2 * ((-3) * x)"),
1.890 +! Thm ("sym_#add_(-3)_3","0 = (-3) + 3"),
1.891 +
1.892 +? Thm ("sym_real_num_collect_assoc",
1.893 + "[| ?l is_const; ?m is_const |]
1.894 + ==> (?l + ?m) * ?n + ?k = ?l * ?n + (?m * ?n + ?k)"),
1.895 +OK Thm ("sym_real_mult_2_assoc","2 * ?z1.0 + ?k = ?z1.0 + (?z1.0 + ?k)"),
1.896 +OK Thm ("sym_real_add_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"),
1.897 +/// Thm ("sym_real_mult_1","?z = 1 * ?z"),
1.898 +! Thm ("sym_#power_3_2","9 = 3 ^^^ 2"),
1.899 +! Thm ("sym_#mult_-1_-1","1 * x ^^^ 2 = -1 * (-1 * x ^^^ 2)"),
1.900 +! Thm ("sym_#mult_-1_3","(-3) * x = -1 * (3 * x)"),
1.901 +OK Thm ("realpow_twoI","?r1 ^^^ 2 = ?r1 * ?r1" [.]),
1.902 +OK Thm ("sym_real_add_assoc",
1.903 + "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"),
1.904 +OK Thm
1.905 + ("sym_real_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
1.906 +OK Thm ("sym_real_mult_left_commute",
1.907 + "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"),
1.908 +OK Thm ("sym_real_mult_commute","?w * ?z = ?z * ?w"),
1.909 +? Thm ("sym_real_add_mult_distrib2",
1.910 + "?w * ?z1.0 + ?w * ?z2.0 = ?w * (?z1.0 + ?z2.0)"),
1.911 +? Thm ("sym_real_add_mult_distrib",
1.912 + "?z1.0 * ?w + ?z2.0 * ?w = (?z1.0 + ?z2.0) * ?w"),
1.913 +OK Thm ("real_mult_div_cancel2","?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n")]
1.914 + -------- revset ----------------------------------------------------
1.915 +
1.916 + val t = (term_of o the o (parse thy)) "(-6) * x";
1.917 + val t = (term_of o the o (parse thy))
1.918 + "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
1.919 + val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)")
1.920 + handle e => print_exn e;
1.921 + val Some (t',_) = rewrite_ thy e_rew_ord e_rls false thm t;
1.922 + term2str t';
1.923 +----------------------------------------------------------------------*)
1.924 +
1.925 +print "\n\n\n****************** all tests successfull *************************\n";
1.926 +
1.927 +
1.928 +
1.929 +(*WN.17.3.03 =========================================================vvv---*)
1.930 +val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.931 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.932 +if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1";
1.933 +
1.934 +val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.935 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.936 +if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
1.937 +else raise error "rational.sml 2";
1.938 +
1.939 +val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
1.940 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.941 +if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1" then ()
1.942 +else raise error "rational.sml 3";
1.943 +trace_rewrite:=true;
1.944 +val t = str2term "Not (6*x is_atom)";
1.945 +val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1.946 +"True";
1.947 +val t = str2term "1 < 2";
1.948 +val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1.949 +"True";
1.950 +val t = str2term "(6*x)^^^2";
1.951 +val Some (t',_) = rewrite_ thy dummy_ord powers_erls false
1.952 + (num_str realpow_def_atom) t;
1.953 +term2str t';
1.954 +trace_rewrite:=false;
1.955 +
1.956 +val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
1.957 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.958 +if term2str t' = "130 * x / 4" then () else raise error "rational.sml 4";
1.959 +
1.960 +val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
1.961 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.962 +if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4" then ()
1.963 +else raise error "rational.sml 5";
1.964 +
1.965 +(*Schalk I, p.92 Nr. 609a*)
1.966 +val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
1.967 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.968 +if term2str t' = "(-255 + 112 * x) / 135" then ()
1.969 +else raise error "rational.sml 6";
1.970 +
1.971 +(*Schalk I, p.92 Nr. 610c*)
1.972 +val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
1.973 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.974 +if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7";
1.975 +
1.976 +(*Schalk I, p.92 Nr. 476a*)
1.977 +val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\
1.978 + \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
1.979 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.980 +if term2str t' = "1 / 1" then () else raise error "rational.sml 8";
1.981 +
1.982 +(*............................vvv---TODO: sollte gehen mit poly_order *)
1.983 +(*Schalk I, p.92 Nr. 472a*)
1.984 +val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1.985 + \((4*x - 8*y)/(x + y))";
1.986 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.987 +"(-32 * y ^^^ 3 +\n (8 * x ^^^ 3 + (-32 * (x * y ^^^ 2) + 8 * (y * x ^^^ 2)))) /\n(-32 * y ^^^ 2 + 8 * x ^^^ 2)";
1.988 +(*###########################statt "x + y" poly_order notwendig!*)
1.989 +
1.990 +(*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1.991 +val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.992 + \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1.993 + \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1.994 + \(20*x*y/(x^^^2 - 25*y^^^2))";
1.995 +(*... nicht simpl, zerlegt ...*)
1.996 +val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.997 + \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))";
1.998 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.999 +"(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
1.1000 +(* ~~~~~~~~~~ poly_order notwendig!*)
1.1001 +val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1.1002 + \(20*x*y/(x^^^2 - 25*y^^^2))";
1.1003 +val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1004 +"(-500 * (x * y ^^^ 3) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2))) +\n 20 * (x * (y * x ^^^ 2)) /\n (x ^^^ 4 + (625 * y ^^^ 4 + -50 * (x ^^^ 2 * y ^^^ 2)))) /\n(20 * (x * y))";
1.1005 +trace_rewrite:=true;
1.1006 +trace_rewrite:=false;
1.1007 +
1.1008 +(*WN.17.3.03 =========================================================^^^---*)
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/sml/kbtest/ratrooteq.sml Thu Apr 17 18:01:03 2003 +0200
2.3 @@ -0,0 +1,2 @@
2.4 +(* testexamples for RatRootEq, equations mixing fractions and roots
2.5 + *)
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/sml/kbtest/rlang.sml Thu Apr 17 18:01:03 2003 +0200
3.3 @@ -0,0 +1,1390 @@
3.4 +(* use"kbtest/rlang.sml";
3.5 + use"rlang.sml";
3.6 + (c) Richard Lang 2003
3.7 + tests over all equations implemented in his diploma thesis
3.8 + Elementare Gleichungen der Mittelschulmathematik in der ISAC Wissensbasis,
3.9 + Master's thesis, University of Technology, Graz, Austria, March 2003.
3.10 + created: 030228
3.11 + from: rlang
3.12 + last change: 030228
3.13 +*)
3.14 +(*@Book{bSchalk1,
3.15 + author = {Schalk, Heinz-Christian and Binder, Christian and Fertl, Walter and
3.16 + Firneis, Friedrich and Gems, Werner and Lehner, Dieter and
3.17 + Plihal, Andreas and Würl,Manfred},
3.18 + title = {Mathematik für höhere technische Lehranstalten Band I},
3.19 + publisher = {Reniets Verlag},
3.20 + year = {1986},
3.21 + note = {Schulbuch-Nr. 942},
3.22 +}
3.23 +
3.24 +@Book{bSchalk2,
3.25 + author = {Schalk, Heinz-Christian and Baumgartner, Gerhard and Binder, Christian and
3.26 + Eder, Hans Gerhard and Fertl, Walter and Firneis, Friedrich and
3.27 + Konstantiniuk, Peter and Plihal, Andreas and Rümmele, Goswin and
3.28 + Steinwender, Andreas and Zangerl, Nikolaus},
3.29 + title = {Mathematik für höhere technische Lehranstalten Band II},
3.30 + publisher = {Reniets Verlag},
3.31 + year = {1987},
3.32 + note = {Schulbuch-Nr. 1682},
3.33 +}
3.34 +*)
3.35 +
3.36 +(* Compiler.Control.Print.printDepth:=5; (*4 default*)
3.37 + trace_rewrite:=true;
3.38 + trace_rewrite:=false;
3.39 + refine fmz ["univariate","equation"];
3.40 +*)
3.41 +"---- rlang.sml begin-----------------------------------";
3.42 +(*----------------- Schalk I s.86 Bsp 5 ------------------------*)
3.43 +"Schalk I s.86 Bsp 5 (3*x - 1 - (5*x - (2 - 4*x)) = -11)";
3.44 +val fmz = ["equality (3*x - 1 - (5*x - (2 - 4*x)) = -11)",
3.45 + "solveFor x","solutions L"];
3.46 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.47 +val p = e_pos';
3.48 +val c = [];
3.49 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.50 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.51 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.52 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.53 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.54 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.55 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.56 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.57 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.58 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.59 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.60 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.61 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.62 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.63 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.64 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.65 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2]")) => ()
3.66 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 5 [x = 2]";
3.67 +
3.68 +(*----------------- Schalk I s.86 Bsp 19 ------------------------*)
3.69 +"Schalk I s.86 Bsp 19 (x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20)";
3.70 +val fmz = ["equality ((x - 5)*(10 - x) = (3 - x)*(2 + x) + 2*(x + 20))",
3.71 + "solveFor x","solutions L"];
3.72 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.73 +val p = e_pos';
3.74 +val c = [];
3.75 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.76 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.77 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.78 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.79 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.80 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.81 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.82 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.83 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.84 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.85 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.86 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.87 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.88 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.89 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.90 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.91 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 8]")) => ()
3.92 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 19 [x = 8]";
3.93 +
3.94 +(*----------------- Schalk I s.86 Bsp 23 ------------------------*)
3.95 +"Schalk I s.86 Bsp 19 ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))";
3.96 +val fmz = ["equality ((2*x+5)^^^2+(3*x+4)^^^2=(13*x+2)*(x+1)+2*(15+14*x))",
3.97 + "solveFor x","solutions L"];
3.98 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.99 +val p = e_pos';
3.100 +val c = [];
3.101 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.102 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.103 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.104 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.105 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.106 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.107 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.108 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.109 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.110 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.111 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.112 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.113 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.114 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.115 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.116 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.117 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -9]")) => ()
3.118 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 23 [x = -9]";
3.119 +
3.120 +(*----------------- Schalk I s.86 Bsp 25 ------------------------*)
3.121 +"Schalk I s.86 Bsp 25 ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)";
3.122 +val fmz = ["equality ((2*x+1)^^^3+(x+1)^^^3=(2*x+1)^^^2*2*x+(x+2)^^^3+x^^^2)",
3.123 + "solveFor x","solutions L"];
3.124 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.125 +val p = e_pos';
3.126 +val c = [];
3.127 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.128 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.129 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.130 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.131 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.132 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.133 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.134 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.135 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.136 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.137 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.138 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.139 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.140 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.141 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.142 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.143 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -6 / 5]")) => ()
3.144 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 25 [x = -6 / 5]";
3.145 +
3.146 +(*----------------- Schalk I s.86 Bsp 28b ------------------------*)
3.147 +"Schalk I s.86 Bsp 28b ((3*x+5)/18 - x/2 = -((3*x - 2)/9))";
3.148 +val fmz = ["equality ((3*x+5)/18 - x/2 = -((3*x - 2)/9))",
3.149 + "solveFor x","solutions L"];
3.150 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.151 +val p = e_pos';
3.152 +val c = [];
3.153 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.154 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.155 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.156 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.157 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.158 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.159 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.160 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.161 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.162 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.163 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.164 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.165 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.166 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.167 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.168 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[]")) => ()
3.169 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 28b []";
3.170 +
3.171 +(*WN---v *)
3.172 +val bdv= (term_of o the o (parse thy)) "bdv";
3.173 +val v = (term_of o the o (parse thy)) "x";
3.174 +val t = (term_of o the o (parse thy)) "3 * x / 5";
3.175 +val Some (t',_) = rewrite_set_inst_ PolyEq.thy true
3.176 + [(bdv, v)] make_ratpoly_in t;
3.177 +if term2str t' = "3 / 5 * x" then () else raise error "rlang.sml: 1";
3.178 +
3.179 +val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
3.180 +val subst = [(str2term "bdv", str2term "x")];
3.181 +val Some (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
3.182 +if term2str t' = "1 / 18 = 0" then () else raise error "rlang.sml: 2";
3.183 +(*WN---^ *)
3.184 +
3.185 +(*----------------- Schalk I s.87 Bsp 36b ------------------------*)
3.186 +"Schalk I s.87 Bsp 36b ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)";
3.187 +val fmz = ["equality ((17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0)",
3.188 + "solveFor x","solutions L"];
3.189 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.190 +val p = e_pos';
3.191 +val c = [];
3.192 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.193 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.194 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.195 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.196 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.197 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.198 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.199 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.200 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.201 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.202 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.203 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.204 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.205 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.206 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.207 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -1 * (79 / 12) / (65 / 36)]")) => ()
3.208 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 36b [x = -1 * (79 / 12) / (65 / 36)]";
3.209 +
3.210 +(*WN---v *)
3.211 +val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
3.212 +val subst = [(str2term "bdv", str2term "x")];
3.213 +val Some (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
3.214 +term2str t';
3.215 +if term2str t' = "79 / 12 + 65 / 36 * x = 0" then ()
3.216 +else raise error "rlang.sml: 3";
3.217 +(*WN---^ *)
3.218 +
3.219 +
3.220 +(*----------------- Schalk I s.87 Bsp 38b ------------------------*)
3.221 +"Schalk I s.87 Bsp 38b (-(2/x) + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)";
3.222 +val fmz = ["equality (-2/x + 3/(2*x) - 4/(3*x) + 5/(4*x) + 6/(5*x) = 65/8)",
3.223 + "solveFor x","solutions L"];
3.224 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.225 +val p = e_pos';
3.226 +val c = [];
3.227 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.228 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.229 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.230 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.231 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.232 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.233 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.234 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.235 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.236 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.237 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.238 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.239 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.240 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.241 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.242 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.243 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.244 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.245 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.246 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.247 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.248 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.249 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.250 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.251 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.252 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 74 / 975]")) => ()
3.253 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.86 Bsp 38b [x = 74 / 975]";
3.254 +
3.255 +(*----------------- Schalk I s.87 Bsp 40b ------------------------*)
3.256 +"Schalk I s.87 Bsp 40b ((x+3)/(2*x - 4)=3)";
3.257 +val fmz = ["equality ((x+3)/(2*x - 4)=3)",
3.258 + "solveFor x","solutions L"];
3.259 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.260 +val p = e_pos';
3.261 +val c = [];
3.262 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.263 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.264 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.265 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.266 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.267 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.268 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.269 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.270 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.271 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.272 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.273 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.274 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.275 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.276 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.277 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.278 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.279 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.280 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.281 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.282 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.283 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.284 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.285 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 3]")) => ()
3.286 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 40b [x = 3]";
3.287 +
3.288 +(*----------------- Schalk I s.87 Bsp 44a ------------------------*)
3.289 +"Schalk I s.87 Bsp 44a ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -(6*x)^^^2 + 29)";
3.290 +val fmz = ["equality ((1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 = -1*(6*x)^^^2 + 29)",
3.291 + "solveFor x","solutions L"];
3.292 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.293 +val p = e_pos';
3.294 +val c = [];
3.295 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.296 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.297 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.298 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.299 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.300 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.301 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.302 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.303 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.304 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.305 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.306 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.307 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.308 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.309 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.310 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.311 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 1]")) => ()
3.312 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 44a [x = 1]";
3.313 +
3.314 +(*WN---v *)
3.315 +val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
3.316 +val subst = [(str2term "bdv", str2term "x")];
3.317 +val Some (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
3.318 +if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
3.319 +else raise error "rlang.sml: 4";
3.320 +
3.321 +val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 + (6*x)^^^2 - 29";
3.322 +val subst = [(str2term "bdv", str2term "x")];
3.323 +val Some (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
3.324 +if term2str t' = "-35 + 35 * x" then ()
3.325 +else raise error "rlang.sml: 4.1";
3.326 +(*WN---^ *)
3.327 +
3.328 +(*----------------- Schalk I s.87 Bsp 52a ------------------------*)
3.329 +"Schalk I s.87 Bsp 52a ((5*x)/(x - 2) - x/(x+2)=4)";
3.330 +val fmz = ["equality ((5*x)/(x - 2) - x/(x+2)=4)",
3.331 + "solveFor x","solutions L"];
3.332 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.333 +val p = e_pos';
3.334 +val c = [];
3.335 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.336 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.337 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.338 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.339 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.340 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.341 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.342 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.343 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.344 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.345 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.346 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.347 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.348 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.349 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.350 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.351 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.352 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.353 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.354 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.355 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.356 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.357 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.358 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.359 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.360 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -4 / 3]")) => ()
3.361 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 52a [x = -4 / 3]";
3.362 +
3.363 +(*----------------- Schalk I s.87 Bsp 55b ------------------------*)
3.364 +"Schalk I s.87 Bsp 55b (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)";
3.365 +val fmz = ["equality (x/(x^^^2 - 6*x+9) - 1/(x^^^2 - 3*x) =1/x)",
3.366 + "solveFor x","solutions L"];
3.367 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.368 +val p = e_pos';
3.369 +val c = [];
3.370 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.371 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.372 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.373 +(*val nxt = ("Model_Problem",Model_Problem["rational","univariate","equation"*)
3.374 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.375 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.376 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.377 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.378 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.379 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.380 +(*"(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x"))
3.381 +val nxt = ("Rewrite_Set",Rewrite_Set "rat_eliminate")
3.382 +get_assumptions pt (fst p);
3.383 +val it = [] : string list*)
3.384 +
3.385 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.386 +(*get_assumptions pt (fst p);
3.387 +val it = ["9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0","x ~= 0"]
3.388 +
3.389 +"(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^3)"))
3.390 +WN: Grad hoeher ~~~~~~~~~~~~ als notwendig ~~~~~~~~
3.391 +val nxt = ("Subproblem",Subproblem ("RatEq.thy",["univariate","equation"])) *)
3.392 +
3.393 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.394 +(* nxt =Model_Problem ["normalize","polynomial","univariate","equation"])*)
3.395 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.396 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.397 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.398 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.399 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.400 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.401 +(*val f = Form' (FormKF (~1,EdUndef,2,Nundef,"-6 * x + 5 * x ^^^ 2 = 0"))
3.402 +val nxt = Subproblem ("PolyEq.thy",["polynomial","univariate","equation"]))*)
3.403 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.404 +(*nxt=Model_Problem["bdv_only","degree_2","polynomial","univariate","equation*)
3.405 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.406 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.407 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.408 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.409 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.410 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.411 +(*val f = Form' (FormKF (~1,EdUndef,3,Nundef,"x = 0 | x = 6 / 5")) : mout
3.412 +val nxt = ("Or_to_List",Or_to_List) *)
3.413 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.414 +(*val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 0, x = 6 / 5]")) : mout
3.415 +val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
3.416 +get_assumptions pt (fst p);
3.417 +val it = [] : string list ... correct for this subproblem !*)
3.418 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.419 +(*val p = ([6,5,5],Res) : pos'
3.420 +val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 0, x = 6 / 5]")) : mout
3.421 +nxt=Check_Postcond ["bdv_only","degree_2","polynomial","univariate","equation*)
3.422 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.423 +(*val p = ([6,5],Res) : pos'
3.424 +val f = Form' (FormKF (~1,EdUndef,2,Nundef,"[x = 0, x = 6 / 5]")) : mout
3.425 +val nxt =Check_Postcond ["normalize","polynomial","univariate","equation"])*)
3.426 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.427 +(*val p = ([6],Res) : pos'
3.428 +val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 0, x = 6 / 5]")) : mout
3.429 +val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
3.430 +get_assumptions pt (fst p);
3.431 +val it = ["9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0","x ~= 0"]
3.432 +
3.433 +> val subs = [(str2term "x", str2term "0")];
3.434 +> val pred = str2term "9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0 & x ~= 0";
3.435 +> eval_true thy [subst_atomic subs pred] rateq_erls;
3.436 +val it = false : bool
3.437 +> val subs = [(str2term "x", str2term "6 / 5")];
3.438 +> val pred = str2term "9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0 & x ~= 0";
3.439 +> eval_true thy [subst_atomic subs pred] rateq_erls;
3.440 +val it = true : bool*)
3.441 +
3.442 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.443 +(*val p = ([7],Res) : pos'
3.444 +val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 6 / 5]")) : mout
3.445 +val nxt =Check_Postcond ["rational","univariate","equation"]) *)
3.446 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.447 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 6 / 5]")) => ()
3.448 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
3.449 +*)
3.450 +(*----------------- Schalk I s.88 Bsp 64c ------------------------*)
3.451 +"Schalk I s.88 Bsp 64c (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)";
3.452 +val fmz = ["equality (((x - 1)/(x+1)+1)/((x - 1)/(x+1) - (x+1)/(x - 1))=2)",
3.453 + "solveFor x","solutions L"];
3.454 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.455 +val p = e_pos';
3.456 +val c = [];
3.457 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.458 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.459 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.460 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.461 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.462 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.463 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.464 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.465 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.466 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.467 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.468 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.469 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.470 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.471 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.472 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.473 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.474 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.475 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.476 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.477 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.478 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.479 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.480 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.481 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.482 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.483 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.484 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.485 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.486 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.487 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.488 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.489 +(*"Check_elementwise",Check_elementwise "Assumptions"*)
3.490 +
3.491 +(*case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = -3]")) => ()
3.492 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 64c [x = -3]";
3.493 +*)
3.494 +
3.495 +(*----------------- Schalk I s.88 Bsp 79a (2) ------------------------*)
3.496 +"Schalk I s.88 Bsp 79a (2) (m1*v1+m2*v2=0)";
3.497 +val fmz = ["equality (m1*v1+m2*v2=0)",
3.498 + "solveFor m1","solutions L"];
3.499 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.500 +val p = e_pos';
3.501 +val c = [];
3.502 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.503 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.504 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.505 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.506 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.507 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.508 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.509 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.510 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.511 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.512 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.513 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.514 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.515 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.516 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.517 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[m1 = -1 * m2 * v2 / v1]")) => ()
3.518 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.88 Bsp 79a (2) [m1 = -1 * m2 * v2 / v1]";
3.519 +
3.520 +(*----------------- Schalk I s.89 Bsp 90a (1) ------------------------*)
3.521 +"Schalk I s.89 Bsp 90a (1) (f=((w+u)/(w+v))*v0)";
3.522 +val fmz = ["equality (f=((w+u)/(w+v))*v0)",
3.523 + "solveFor v","solutions L"];
3.524 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.525 +val p = e_pos';
3.526 +val c = [];
3.527 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.528 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.529 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.530 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.531 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.532 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.533 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.534 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.535 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.536 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.537 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.538 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.539 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.540 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.541 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.542 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.543 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.544 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.545 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.546 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.547 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.548 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.549 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.550 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[v = -1 * (f * w + -1 * u * v0 + -1 * v0 * w) / f]")) => ()
3.551 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (1) [v=...]";
3.552 +
3.553 +(*----------------- Schalk I s.89 Bsp 90a (2) ------------------------*)
3.554 +"Schalk I s.89 Bsp 90a (2) (f=((w+u)/(w+v))*v0)";
3.555 +val fmz = ["equality (f=((w+u)/(w+v))*v0)",
3.556 + "solveFor w","solutions L"];
3.557 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.558 +val p = e_pos';
3.559 +val c = [];
3.560 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.561 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.562 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.563 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.564 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.565 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.566 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.567 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.568 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.569 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.570 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.571 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.572 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.573 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.574 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.575 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.576 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.577 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.578 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.579 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.580 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.581 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.582 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.583 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[w = -1 * (f * v + -1 * u * v0) / (f + -1 * v0)]")) => ()
3.584 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 90a (2) [w=...]";
3.585 +
3.586 +(*----------------- Schalk I s.89 Bsp 98a (1) ------------------------*)
3.587 +"Schalk I s.89 Bsp 98a (1) (1/R=1/R1+1/R2)";
3.588 +val fmz = ["equality (1/R=1/R1+1/R2)",
3.589 + "solveFor R1","solutions L"];
3.590 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.591 +val p = e_pos';
3.592 +val c = [];
3.593 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.594 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.595 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.596 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.597 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.598 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.599 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.600 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.601 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.602 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.603 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.604 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.605 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.606 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.607 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.608 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.609 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.610 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.611 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.612 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.613 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.614 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.615 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.616 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[R1 = 1 * R * R2 / (R2 + -1 * R)]")) => ()
3.617 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 98a (1) [R1 =...]";
3.618 +
3.619 +
3.620 +(*----------------- Schalk I s.89 Bsp 104a (1) ------------------------*)
3.621 +"Schalk I s.89 Bsp 104a (1) (y^^^2=2*p*x)";
3.622 +val fmz = ["equality (y^^^2=2*p*x)",
3.623 + "solveFor p","solutions L"];
3.624 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.625 +val p = e_pos';
3.626 +val c = [];
3.627 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.628 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.629 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.630 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.631 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.632 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.633 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.634 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.635 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.636 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.637 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.638 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.639 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.640 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.641 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.642 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.643 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[p = -1 * y ^^^ 2 / (-2 * x)]")) => ()
3.644 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a (1) [p = -1 * y ^^^ 2 / (-2 * x)]";
3.645 +
3.646 +(*----------------- Schalk I s.89 Bsp 104a (2) ------------------------*)
3.647 +"Schalk I s.89 Bsp 104a (2) (y^^^2=2*p*x)";
3.648 +val fmz = ["equality (y^^^2=2*p*x)",
3.649 + "solveFor y","solutions L"];
3.650 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.651 +val p = e_pos';
3.652 +val c = [];
3.653 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.654 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.655 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.656 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.657 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.658 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.659 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.660 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.661 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.662 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.663 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.664 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.665 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.666 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.667 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.668 +(*"Check_elementwise",Check_elementwise "Assumptions"*)
3.669 +
3.670 +(*case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = ]")) => ()
3.671 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 104a(2) [x = ]";
3.672 +*)
3.673 +
3.674 +(*----------------- Schalk I s.90 Bsp 118a (1) ------------------------*)
3.675 +"Schalk I s.90 Bsp 118a (1) (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)";
3.676 +val fmz = ["equality (b^^^2*x^^^2 + a^^^2*y^^^2 = a^^^2*b^^^2)",
3.677 + "solveFor x","solutions L"];
3.678 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.679 +val p = e_pos';
3.680 +val c = [];
3.681 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.682 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.683 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.684 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.685 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.686 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.687 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.688 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.689 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.690 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.691 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.692 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.693 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.694 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.695 +(*"Check_elementwise",Check_elementwise "Assumptions"*)
3.696 +
3.697 +(*case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = ]")) => ()
3.698 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.89 Bsp 118a(2) [x = ]";
3.699 +*)
3.700 +
3.701 +(*----------------- Schalk I s.102 Bsp 268(1) ------------------------*)
3.702 +"Schalk I s.102 Bsp 268(1) (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))";
3.703 +val fmz = ["equality (A = (1/2)*(x1*(y2 - y3)+x2*(y3 - y1)+x3*(y1 - y2)))",
3.704 + "solveFor x2","solutions L"];
3.705 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.706 +val p = e_pos';
3.707 +val c = [];
3.708 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.709 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.710 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.711 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.712 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.713 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.714 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.715 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.716 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.717 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.718 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.719 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.720 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.721 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.722 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.723 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.724 +case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x2 =\n -1 *\n (2 * A / 2 + x1 * y3 / 2 + x3 * y2 / 2 + -1 * x1 * y2 / 2 +\n -1 * x3 * y1 / 2) /\n (y1 / 2 + -1 * y3 / 2)]")) => ()
3.725 + | _ => raise error "rlang.sml: diff.behav. in Schalk I s.102 Bsp 268(1) [x2=...]";
3.726 +
3.727 +(*----------------- Schalk II s.56 Bsp 67b ------------------------*)
3.728 +"Schalk II s.56 Bsp 67b (4*sqrt(4*x+1)=3*sqrt(7*x+2))";
3.729 +val fmz = ["equality (4*sqrt(4*x+1)=3*sqrt(7*x+2))",
3.730 + "solveFor x","solutions L"];
3.731 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.732 +val p = e_pos';
3.733 +val c = [];
3.734 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.735 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.736 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.737 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.738 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.739 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.740 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.741 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.742 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.743 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.744 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.745 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.746 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.747 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.748 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.749 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.750 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.751 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.752 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.753 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.754 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.755 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.756 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.757 +(*
3.758 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.759 +val p = ([4,3],Res) : pos'
3.760 +val f = Form' (FormKF (~1,EdUndef,2,Nundef,"[x = 2]")) : mout
3.761 +val nxt =
3.762 + ("Check_Postcond",
3.763 + Check_Postcond ["normalize","polynomial","univariate","equation"])
3.764 + : string * mstep
3.765 +val pt =
3.766 + Nd
3.767 + (PblObj
3.768 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.769 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #]) : ptree
3.770 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.771 +### applicable_in Check_elementwise: erls= rooteq_erls
3.772 +### applicable_in Check_elementwise: pred= Assumptions
3.773 +GC #3.97.133.343.2360.206311: (0 ms)
3.774 +### Ambiguous input "x occurs_in 4 * x + 1"
3.775 +### produces the following parse trees:
3.776 +### ("occurs'_in" x ("op +" ("op *" ("_Numeral" ("_constify" 4)) x) "1"))
3.777 +### ("op +" ("occurs'_in" x ("op *" ("_Numeral" ("_constify" 4)) x)) "1")
3.778 +### ("op +" ("op *" ("occurs'_in" x ("_Numeral" ("_constify" 4))) x) "1")
3.779 +### Fortunately, only one parse tree is type correct.
3.780 +### You may still want to disambiguate your grammar or your input.
3.781 +### applicable_in Check_elementwise: --> []
3.782 +val p = ([4],Res) : pos'
3.783 +val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[x = 2]")) : mout
3.784 +val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
3.785 + : string * mstep
3.786 +val pt =
3.787 + Nd
3.788 + (PblObj
3.789 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.790 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #]) : ptree
3.791 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.792 +### applicable_in Check_elementwise: erls= rooteq_erls
3.793 +### applicable_in Check_elementwise: pred= Assumptions
3.794 +### Ambiguous input "x occurs_in 4 * x + 1"
3.795 +### produces the following parse trees:
3.796 +### ("occurs'_in" x ("op +" ("op *" ("_Numeral" ("_constify" 4)) x) "1"))
3.797 +### ("op +" ("occurs'_in" x ("op *" ("_Numeral" ("_constify" 4)) x)) "1")
3.798 +### ("op +" ("op *" ("occurs'_in" x ("_Numeral" ("_constify" 4))) x) "1")
3.799 +### Fortunately, only one parse tree is type correct.
3.800 +### You may still want to disambiguate your grammar or your input.
3.801 +### applicable_in Check_elementwise: --> []
3.802 +val p = ([5],Res) : pos'
3.803 +val f = Form' (FormKF (~1,EdUndef,1,Nundef,"[]")) : mout
3.804 +val nxt =
3.805 + ("Check_Postcond",Check_Postcond ["sq","root","univariate","equation"])
3.806 + : string * mstep
3.807 +val pt =
3.808 + Nd
3.809 + (PblObj
3.810 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.811 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #,Nd #]) : ptree
3.812 +*)
3.813 +
3.814 +(*----------------- Schalk II s.56 Bsp 68a ------------------------*)
3.815 +"Schalk II s.56 Bsp 68a (5*sqrt(x) - 1 = 7*sqrt(x) - 5)";
3.816 +val fmz = ["equality (5*sqrt(x) - 1 = 7*sqrt(x) - 5)",
3.817 + "solveFor x","solutions L"];
3.818 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.819 +val p = e_pos';
3.820 +val c = [];
3.821 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.822 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.823 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.824 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.825 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.826 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.827 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.828 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.829 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.830 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.831 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.832 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.833 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.834 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.835 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.836 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.837 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.838 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.839 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.840 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.841 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.842 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.843 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.844 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.845 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.846 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.847 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.848 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.849 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.850 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.851 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.852 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.853 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.854 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.855 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.856 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.857 +(*
3.858 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.859 +val p = ([2,5,6,4],Res) : pos'
3.860 +val f = Form' (FormKF (~1,EdUndef,4,Nundef,"[x = 4, x = 1 / 9]")) : mout
3.861 +val nxt =
3.862 + ("Check_Postcond",
3.863 + Check_Postcond ["normalize","polynomial","univariate","equation"])
3.864 + : string * mstep
3.865 +val pt =
3.866 + Nd
3.867 + (PblObj
3.868 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.869 + result=#,spec=#},[Nd #,Nd #]) : ptree
3.870 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.871 +### applicable_in Check_elementwise: erls= rooteq_erls
3.872 +### applicable_in Check_elementwise: pred= Assumptions
3.873 +GC #3.92.125.254.1053.73002: (0 ms)
3.874 +### applicable_in Check_elementwise: --> []
3.875 +val p = ([2,5,6],Res) : pos'
3.876 +val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[x = 4, x = 1 / 9]")) : mout
3.877 +val nxt = ("Check_elementwise",Check_elementwise "Assumptions")
3.878 + : string * mstep
3.879 +val pt =
3.880 + Nd
3.881 + (PblObj
3.882 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.883 + result=#,spec=#},[Nd #,Nd #]) : ptree
3.884 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.885 +### applicable_in Check_elementwise: erls= rooteq_erls
3.886 +### applicable_in Check_elementwise: pred= Assumptions
3.887 +### applicable_in Check_elementwise: --> []
3.888 +val p = ([2,5,7],Res) : pos'
3.889 +val f = Form' (FormKF (~1,EdUndef,3,Nundef,"[]")) : mout
3.890 +val nxt =
3.891 + ("Check_Postcond",Check_Postcond ["sq","root","univariate","equation"])
3.892 + : string * mstep
3.893 +val pt =
3.894 + Nd
3.895 + (PblObj
3.896 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.897 + result=#,spec=#},[Nd #,Nd #]) : ptree
3.898 +*)
3.899 +
3.900 +(*----------------- Schalk II s.56 Bsp 73b ------------------------*)
3.901 +"Schalk II s.56 Bsp 73b (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))";
3.902 +val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))",
3.903 + "solveFor x","solutions L"];
3.904 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.905 +val p = e_pos';
3.906 +val c = [];
3.907 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.908 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.909 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.910 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.911 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.912 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.913 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.914 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.915 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.916 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.917 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.918 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.919 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.920 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.921 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.922 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.923 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.924 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.925 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.926 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.927 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.928 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.929 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.930 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.931 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.932 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.933 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.934 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.935 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.936 +
3.937 +(*
3.938 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.939 +val p = ([6,6,3,1],Frm) : pos'
3.940 +val f = Form' (FormKF (~1,EdUndef,4,Nundef,"0 = 0")) : mout
3.941 +val nxt = ("Rewrite_Set_Inst",Rewrite_Set_Inst ([#],"d0_poly_simplify"))
3.942 + : string * mstep
3.943 +val pt =
3.944 + Nd
3.945 + (PblObj
3.946 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.947 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #,Nd #,Nd #]) : ptree
3.948 +val p = ([6,6,3,1],Res) : pos'
3.949 +val f = Form' (FormKF (~1,EdUndef,4,Nundef,"True")) : mout
3.950 +val nxt = ("Or_to_List",Or_to_List) : string * mstep
3.951 +val pt =
3.952 + Nd
3.953 + (PblObj
3.954 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.955 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #,Nd #,Nd #]) : ptree
3.956 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.957 +val p = ([6,6,3,2],Res) : pos'
3.958 +val f = Form' (FormKF (~1,EdUndef,4,Nundef,"UniversalList")) : mout
3.959 +val nxt =
3.960 + ("Check_Postcond",
3.961 + Check_Postcond ["degree_0","polynomial","univariate","equation"])
3.962 + : string * mstep
3.963 +val pt =
3.964 + Nd
3.965 + (PblObj
3.966 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.967 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #,Nd #,Nd #]) : ptree
3.968 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.969 +val p = ([6,6,3],Res) : pos'
3.970 +val f = Form' (FormKF (~1,EdUndef,3,Nundef,"UniversalList")) : mout
3.971 +val nxt =
3.972 + ("Check_Postcond",
3.973 + Check_Postcond ["normalize","polynomial","univariate","equation"])
3.974 + : string * mstep
3.975 +val pt =
3.976 + Nd
3.977 + (PblObj
3.978 + {branch=#,cell=#,env=#,loc=#,meth=#,model=#,origin=#,ostate=#,probl=#,
3.979 + result=#,spec=#},[Nd #,Nd #,Nd #,Nd #,Nd #,Nd #]) : ptree
3.980 +ML> val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.981 +### applicable_in Check_elementwise: erls= rooteq_erls
3.982 +### applicable_in Check_elementwise: pred= Assumptions
3.983 +*** check_elementwise: no set UniversalList
3.984 +
3.985 +uncaught exception ERROR
3.986 + raised at: library.ML:1161.35-1161.40
3.987 +*)
3.988 +
3.989 +(*----------------- Schalk II s.56 Bsp 74a ------------------------*)
3.990 +"Schalk II s.56 Bsp 74a (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))";
3.991 +val fmz = ["equality (sqrt(4*x+1) - sqrt(x+3) = sqrt(x - 2))",
3.992 + "solveFor x","solutions L"];
3.993 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.994 +val p = e_pos';
3.995 +val c = [];
3.996 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.997 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.998 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.999 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1000 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1001 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1002 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1003 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1004 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1005 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1006 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1007 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1008 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1009 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1010 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1011 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1012 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1013 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1014 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1015 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1016 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1017 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1018 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1019 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1020 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1021 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1022 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1023 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1024 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1025 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1026 +(*
3.1027 +Auch hier wird die Loesung von Check_elementwise: eliminiert
3.1028 +*)
3.1029 +
3.1030 +(*----------------- Schalk II s.56 Bsp 77b ------------------------*)
3.1031 +"Schalk II s.56 Bsp 77b (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))";
3.1032 +val fmz = ["equality (sqrt(x+12)+sqrt(x - 3) = sqrt(x + 32) - sqrt(5+x))",
3.1033 + "solveFor x","solutions L"];
3.1034 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.1035 +val p = e_pos';
3.1036 +val c = [];
3.1037 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1038 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1039 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1040 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1041 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1042 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1043 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1044 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1045 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1046 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1047 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1048 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1049 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1050 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1051 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1052 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1053 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1054 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1055 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1056 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1057 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1058 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1059 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1060 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1061 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1062 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1063 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1064 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1065 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1066 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1067 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1068 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1069 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1070 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1071 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1072 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1073 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1074 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1075 +(*
3.1076 +Auch hier wird die Loesung von Check_elementwise: eliminiert
3.1077 +*)
3.1078 +
3.1079 +(*----------------- Schalk II s.66 Bsp 4 ------------------------*)
3.1080 +"Schalk II s.66 Bsp 4 ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)";
3.1081 +val fmz = ["equality ((6*x - 9)*(5*x+7) - (4*x+7)*(3*x - 6) = 429)",
3.1082 + "solveFor x","solutions L"];
3.1083 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.1084 +val p = e_pos';
3.1085 +val c = [];
3.1086 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1087 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1088 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1089 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1090 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1091 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1092 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1093 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1094 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1095 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1096 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1097 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1098 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1099 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1100 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1101 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1102 +(*
3.1103 +Auch hier wird die Loesung von Check_elementwise: eliminiert
3.1104 +*)
3.1105 +(*case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 5, x = -5]")) => ()
3.1106 + | _ => raise error "rlang.sml: diff.behav. in Schalk II s.6 Bsp 4 [x = 5, x = -5]";*)
3.1107 +
3.1108 +(*----------------- Schalk II s.66 Bsp 8a ------------------------*)
3.1109 +"Schalk II s.66 Bsp 8a ((x - 4)/(x+4) = (1 - x)/(1+x))";
3.1110 +val fmz = ["equality ((x - 4)/(x+4) = (1 - x)/(1+x))",
3.1111 + "solveFor x","solutions L"];
3.1112 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.1113 +val p = e_pos';
3.1114 +val c = [];
3.1115 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1116 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1117 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1118 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1119 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1120 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1121 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1122 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1123 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1124 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1125 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1126 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1127 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1128 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1129 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1130 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1131 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1132 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1133 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1134 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1135 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1136 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1137 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1138 +(*
3.1139 +Auch hier wird die Loesung von Check_elementwise: eliminiert
3.1140 +*)
3.1141 +(*case f of Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 2, x = -2]")) => ()
3.1142 + | _ => raise error "rlang.sml: diff.behav. in Schalk II s.66 Bsp 8a [x = 2, x = -2]";*)
3.1143 +
3.1144 +(*----------------- Schalk II s.66 Bsp 10b ------------------------*)
3.1145 +"Schalk II s.66 Bsp 10b (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))";
3.1146 +val fmz = ["equality (1/(x^^^2 - 9)+(2*x+3)/(x+3)=(3*x+4)/(x - 3))",
3.1147 + "solveFor x","solutions L"];
3.1148 +val (dI',pI',mI') = ("RatEq.thy",["univariate","equation"],("RatEq.thy","no_met"));
3.1149 +val p = e_pos';
3.1150 +val c = [];
3.1151 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1152 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1153 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1154 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1155 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1156 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1157 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1158 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1159 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1160 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1161 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1162 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1163 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1164 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1165 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1166 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1167 +(*
3.1168 +60 + 28 * x + -13 * x ^^^ 2 + -1 * x ^^^ 3 = 0
3.1169 +*)
3.1170 +
3.1171 +(*----------------- Schalk II s.66 Bsp 20a ------------------------*)
3.1172 +"Schalk II s.66 Bsp 20a (sqrt(29 - sqrt (x^^^2 - 9))=5)";
3.1173 +val fmz = ["equality (sqrt(29 - sqrt(x^^^2 - 9))=5)",
3.1174 + "solveFor x","solutions L"];
3.1175 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.1176 +val p = e_pos';
3.1177 +val c = [];
3.1178 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1179 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1180 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1181 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1182 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1183 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1184 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1185 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1186 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1187 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1188 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1189 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1190 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1191 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1192 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1193 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1194 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1195 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1196 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1197 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1198 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1199 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1200 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1201 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1202 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1203 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1204 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1205 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1206 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1207 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1208 +(*
3.1209 +Auch hier wird die Loesung von Check_elementwise: eliminiert
3.1210 +*)
3.1211 +
3.1212 +(*----------------- Schalk II s.66 Bsp 23b ------------------------*)
3.1213 +"Schalk II s.66 Bsp 23b (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))";
3.1214 +val fmz = ["equality (2*sqrt(261 - x) - sqrt(2+2*x)=sqrt(2)*sqrt(5 - 3*x))",
3.1215 + "solveFor x","solutions L"];
3.1216 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.1217 +val p = e_pos';
3.1218 +val c = [];
3.1219 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1220 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1221 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1222 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1223 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1224 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1225 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1226 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1227 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1228 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1229 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1230 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1231 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1232 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1233 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1234 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1235 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1236 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1237 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1238 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1239 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1240 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1241 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1242 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1243 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1244 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1245 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1246 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1247 +(*
3.1248 +Regel wird angewendet obwohl prems false:
3.1249 + ### trying thm 'd2_abcformula1'
3.1250 +### --- begin eval. condition(s) ---
3.1251 +...
3.1252 +### rewrites to: 204469248 <= 1024
3.1253 +...
3.1254 +### calc. to: False
3.1255 +### --- end eval. condition(s) ---
3.1256 +### rewrites to: x = (- 32 + sqrt (32 ^^^ 2 - 4 * -48 * -1064944)) / (2 * -48) |
3.1257 +x = (- 32 - sqrt (32 ^^^ 2 - 4 * -48 * -1064944)) / (2 * -48)
3.1258 +*)
3.1259 +
3.1260 +(*----------------- Schalk II s.66 Bsp 28a ------------------------*)
3.1261 +"Schalk II s.66 Bsp 28a (A=(c/d)*sqrt(4*a^^^2 - c^^^2))";
3.1262 +val fmz = ["equality (A=(c/d)*sqrt(4*a^^^2 - c^^^2))",
3.1263 + "solveFor a","solutions L"];
3.1264 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
3.1265 +val p = e_pos';
3.1266 +val c = [];
3.1267 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1268 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1269 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1270 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1271 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1272 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1273 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1274 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1275 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1276 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1277 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1278 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1279 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1280 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1281 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1282 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1283 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1284 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1285 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1286 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1287 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1288 +(*
3.1289 +Auch hier wird die Loesung von Check_elementwise: eliminiert
3.1290 +*)
3.1291 +
3.1292 +"------ @@@@@TEST---------------------------------";
3.1293 +val fmz = ["equality ((2*x+1)*x^^^2 = 0)",
3.1294 + "solveFor x","solutions L"];
3.1295 +val (dI',pI',mI') = ("PolyEq.thy",["univariate","equation"],("PolyEq.thy","no_met"));
3.1296 +val p = e_pos';
3.1297 +val c = [];
3.1298 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
3.1299 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
3.1300 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1301 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1302 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1303 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1304 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1305 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1306 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1307 +(*
3.1308 +val f = Form' (FormKF (~1,EdUndef,1,Nundef,"(2 * x + 1) * x ^^^ 2 = 0"))
3.1309 +normiert nicht ... korr.WN:
3.1310 +val t = str2term "(2*x+1)*x^^^2 = 0";
3.1311 +val subst = [(str2term "bdv", str2term "x")];
3.1312 +val Some (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
3.1313 +if term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then ()
3.1314 +else raise error "rlang.sml: 7";
3.1315 +*)
3.1316 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1317 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1318 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1319 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1320 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1321 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1322 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1323 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1324 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1325 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1326 +
3.1327 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1328 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1329 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1330 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1331 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1332 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1333 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1334 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1335 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
3.1336 +if f = Form' (FormKF (~1,EdUndef,0,Nundef,"[x = 0, x = 0, x = -1 / 2]"))then()
3.1337 +else raise error "rlang.sml Schalk II Bsp 28a new behaviour";
3.1338 +
3.1339 +"------ rlang.sml end---------------------------------";
3.1340 +
3.1341 +(*------------------------------vvv-Rewrite_Set "rat_eliminate"---------
3.1342 +> trace_rewrite:=true;
3.1343 +> val t = str2term
3.1344 + "(3 + -1 * x + 1 * x ^^^ 2) / (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3) = 1 / x";
3.1345 +> val Some (t',asm) =
3.1346 + rewrite_ thy dummy_ord rateq_erls true rat_mult_denominator_both t;
3.1347 +> term2str t'; terms2str asm;
3.1348 +"(3 + -1 * x + 1 * x ^^^ 2) * x = 1 * (9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3)"
3.1349 +"[\"9 * x + -6 * x ^^^ 2 + 1 * x ^^^ 3 ~= 0\",\"x ~= 0\"]"
3.1350 +> trace_rewrite:=false;
3.1351 + ------------------------------^^^-Rewrite_Set "rat_eliminate"---------*)
3.1352 +
3.1353 +(*-------vvv-Rewrite_Set "d1_poly_simplify""x = 0 | -6 + 5 * x = 0"---------*)
3.1354 +
3.1355 +val t = str2term "-6 + 5 * x = 0";
3.1356 +val subst = [(str2term "bdv", str2term "x")];
3.1357 +val Some (t',_) = rewrite_set_inst_ thy true subst d1_poly_simplify t;
3.1358 +term2str t'; (*gleich*)
3.1359 +val Some (t',_) = rewrite_set_inst_ thy false subst d1_poly_simplify t;
3.1360 +term2str t'; (*unterschied*)
3.1361 +val t = str2term "5 * x = - -6";
3.1362 +val Some (t',_) = rewrite_inst_ thy dummy_ord polyeq_erls false
3.1363 + subst d1_isolate_div t;
3.1364 +term2str t';
3.1365 +
3.1366 +memrls (Thm ("d1_isolate_div",num_str d1_isolate_div)) d1_poly_simplify;
3.1367 +(*val it = true : bool*)
3.1368 +memrls (Calc ("op =",eval_equal "#equal_")) d1_poly_simplify;
3.1369 +memrls (Calc ("op =",eval_equal "#equal_")) rateq_erls;
3.1370 +(*val it = false : bool*)
3.1371 +
3.1372 +val t = str2term "5 ~= 0";
3.1373 +eval_true thy [t] polyeq_erls ;
3.1374 +(*val it = false : bool --- beide gleichg*)
3.1375 +val t = str2term "~ x occurs_in - -6";
3.1376 +eval_true thy [t] polyeq_erls ;
3.1377 +(*val it = true : bool --- beide gleichg*)
3.1378 +
3.1379 +trace_rewrite:=true;
3.1380 +trace_rewrite:=false;
3.1381 +(*-------vvv-Rewrite_Set "d1_poly_simplify""x = 0 | -6 + 5 * x = 0"---------*)
3.1382 +
3.1383 +
3.1384 +
3.1385 +
3.1386 +(*
3.1387 +val t = str2term "(2*x+1)*x^^^2 = 0";
3.1388 +val subst = [(str2term "bdv", str2term "x")];
3.1389 +val Some (t',_) = rewrite_set_inst_ thy false subst make_ratpoly_in t;
3.1390 +trace_rewrite:=true;depth:=4;
3.1391 +if term2str t' = "x ^^^ 2 + 2 * x ^^^ 3 = 0" then ()
3.1392 +else raise error "rlang.sml: 7";
3.1393 +*)
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/sml/kbtest/root.sml Thu Apr 17 18:01:03 2003 +0200
4.3 @@ -0,0 +1,2 @@
4.4 +(* testexamples for Root, radicals
4.5 + *)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/sml/kbtest/rooteq.sml Thu Apr 17 18:01:03 2003 +0200
5.3 @@ -0,0 +1,70 @@
5.4 +(* RL 10.02
5.5 + use"../kbtest/rooteq.sml";
5.6 + testexamples for RootEq, equations with fractions
5.7 +
5.8 + Compiler.Control.Print.printDepth:=10; (*4 default*)
5.9 + Compiler.Control.Print.printDepth:=5; (*4 default*)
5.10 + trace_rewrite:=true;
5.11 +*)
5.12 +val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootequation_in x";
5.13 +val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t;
5.14 +val result = term2str t_;
5.15 +if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
5.16 +
5.17 +val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootequation_in x";
5.18 +val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t;
5.19 +val result = term2str t_;
5.20 +if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
5.21 +
5.22 +val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootequation_in x";
5.23 +val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t;
5.24 +val result = term2str t_;
5.25 +if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
5.26 +
5.27 +val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtequation_in x";
5.28 +val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t;
5.29 +val result = term2str t_;
5.30 +if result <> "True" then raise error "rooteq.sml: new behaviour:" else ();
5.31 +
5.32 +val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtequation_in x";
5.33 +val Some(t_, _) = rewrite_set_ RootEq.thy false rooteq_prls t;
5.34 +val result = term2str t_;
5.35 +if result <> "False" then raise error "rooteq.sml: new behaviour:" else ();
5.36 +
5.37 +
5.38 +val result = match_pbl ["equality (sqrt(x)=1)","solveFor x","solutions L"]
5.39 + (get_pbt ["root","univariate","equation"]);
5.40 +case result of Matches' _ => () | _ => raise error "rooteq.sml: new behaviour:";
5.41 +
5.42 +val result = match_pbl ["equality (sqrt(25)=1)","solveFor x","solutions L"]
5.43 + (get_pbt ["root","univariate","equation"]);
5.44 +case result of NoMatch' _ => () | _ => raise error "rooteq.sml: new behaviour:";
5.45 +
5.46 +(*---------rooteq---- 23.8.02 ---------------------*)
5.47 +val fmz = ["equality (sqrt(x)=5)","solveFor x","solutions L"];
5.48 +val fmz = ["equality (5*sqrt(3*x+1)=3*sqrt(5*x+25))","solveFor x","solutions L"];
5.49 +val fmz = ["equality (sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))","solveFor x","solutions L"];
5.50 +(*0=0*)
5.51 +val fmz = ["equality (3*sqrt(x+3)+sqrt(x+6)=sqrt(4*x+33))","solveFor x","solutions L"];
5.52 +(* [x = -2] *)
5.53 +
5.54 +(* refine fmz ["univariate","equation"];
5.55 + Compiler.Control.Print.printDepth:=10; (*4 default*)
5.56 + Compiler.Control.Print.printDepth:=5; (*4 default*)
5.57 + trace_rewrite:=true;
5.58 +*)
5.59 +val (dI',pI',mI') = ("RootEq.thy",["univariate","equation"],("RootEq.thy","no_met"));
5.60 +val p = e_pos';
5.61 +val c = [];
5.62 +val (mI,m) = ("Init_Proof",Init_Proof (fmz, (dI',pI',mI')));
5.63 +val (p,_,f,nxt,_,pt) = me (mI,m) p c EmptyPtree;
5.64 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.65 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.66 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.67 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.68 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.69 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.70 +val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
5.71 +
5.72 +
5.73 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/sml/kbtest/termorder.sml Thu Apr 17 18:01:03 2003 +0200
6.3 @@ -0,0 +1,174 @@
6.4 + (* tests on rewrite orders
6.5 +
6.6 + use"../kbtest/termorder.sml";
6.7 + use"kbtest/termorder.sml";
6.8 + *)
6.9 +
6.10 +
6.11 + (*die ersten Tests*)
6.12 + val substa = [(e_term, (term_of o the o (parse thy)) "a")];
6.13 + val substb = [(e_term, (term_of o the o (parse thy)) "b")];
6.14 + val substx = [(e_term, (term_of o the o (parse thy)) "x")];
6.15 + val x1 = (term_of o the o (parse thy)) "a + b + x";
6.16 + val x2 = (term_of o the o (parse thy)) "a + x + b";
6.17 + val x3 = (term_of o the o (parse thy)) "a + x + b";
6.18 + val x4 = (term_of o the o (parse thy)) "x + a + b";
6.19 + ord_make_polynomial_in true thy substx (x1,x2);
6.20 + true; (* => LESS *)
6.21 + ord_make_polynomial_in true thy substa (x1,x2);
6.22 + true; (* => LESS *)
6.23 + ord_make_polynomial_in true thy substb (x1,x2);
6.24 + false; (* => GREATER *)
6.25 +
6.26 + val aa = (term_of o the o (parse thy)) "-1 * a * x";
6.27 + val bb = (term_of o the o (parse thy)) "x^^^3";
6.28 + ord_make_polynomial_in true thy substx (aa, bb);
6.29 + true; (* => LESS *)
6.30 +
6.31 + val aa = (term_of o the o (parse thy)) "-1 * a * x";
6.32 + val bb = (term_of o the o (parse thy)) "x^^^3";
6.33 + ord_make_polynomial_in true thy substa (aa, bb);
6.34 + false; (* => GREATER *)
6.35 +
6.36 + (*und nach dem Re-engineering der Termorders in den 'rulesets'
6.37 + kannst Du die 'gr"osste' Variable frei w"ahlen: *)
6.38 + val bdv= (term_of o the o (parse thy)) "bdv";
6.39 + val x = (term_of o the o (parse thy)) "x";
6.40 + val a = (term_of o the o (parse thy)) "a";
6.41 + val b = (term_of o the o (parse thy)) "b";
6.42 + val Some (t',_) =
6.43 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
6.44 + term2str t';
6.45 + "b + x + a";
6.46 + val None =
6.47 + rewrite_set_inst_ thy false [(bdv,b)] make_polynomial_in x2;
6.48 + term2str t';
6.49 + "a + x + b";
6.50 + val Some (t',_) =
6.51 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in x2;
6.52 + term2str t';
6.53 + "a + b + x";
6.54 +
6.55 +
6.56 + val ppp' = "-6 + -5*x + x^^^3 + -1*x^^^2 + -1*x^^^3 + -14*x^^^2";
6.57 + val ppp = (term_of o the o (parse thy)) ppp';
6.58 + val Some (t',_) =
6.59 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
6.60 + term2str t';
6.61 + "(-6) + (-5 * x + (-15 * x ^^^ 2))";
6.62 + val Some (t',_) =
6.63 + rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp';
6.64 + "(-6) + (-5 * x + (-15) * x ^^^ 2)";
6.65 +
6.66 +
6.67 + val ttt' = "(3*x + 5)/18";
6.68 + val ttt = (term_of o the o (parse thy)) ttt';
6.69 + val Some (uuu,_) =
6.70 + rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ttt;
6.71 + term2str uuu;
6.72 + "(5 + 3 * x) / 18";
6.73 + val Some (uuu,_) =
6.74 + rewrite_set_ thy false make_polynomial ttt;
6.75 + term2str uuu;
6.76 + "(5 + 3 * x) / 18";
6.77 +
6.78 +
6.79 +
6.80 +
6.81 +(*-----------28.2.03: war nicht upgedatet (und ausgeklammert in ROOT.ML
6.82 +
6.83 + (*Aufgabe zum Einstieg in die Arbeit...*)
6.84 + val t = (term_of o the o (parse thy)) "a*b - (a+b)*x + x^^^2 = 0";
6.85 + (*ein 'ruleset' aus Poly.ML wird angewandt...*)
6.86 + val Some (t,_) = rewrite_set_ thy poly_erls false make_polynomial t;
6.87 + term2str t;
6.88 + "a * b + (-1 * (a * x) + (-1 * (b * x) + x ^^^ 2)) = 0";
6.89 + val Some (t,_) =
6.90 + rewrite_set_inst_ thy poly_erls false [("bdv","a")] make_polynomial_in t;
6.91 + term2str t;
6.92 + "x ^^^ 2 + (-1 * (b * x) + (-1 * (x * a) + b * a)) = 0";
6.93 +(* bei Verwendung von "size_of-term" nach MG :*)
6.94 +(*"x ^^^ 2 + (-1 * (b * x) + (b * a + -1 * (x * a))) = 0" !!! *)
6.95 +
6.96 + (*wir holen 'a' wieder aus der Klammerung heraus...*)
6.97 + val Some (t,_) = rewrite_set_ thy poly_erls false discard_parentheses t;
6.98 + term2str t;
6.99 + "x ^^^ 2 + -1 * b * x + -1 * x * a + b * a = 0";
6.100 +(* "x ^^^ 2 + -1 * b * x + b * a + -1 * x * a = 0" !!! *)
6.101 +
6.102 + val Some (t,_) =
6.103 + rewrite_set_inst_ thy poly_erls false [("bdv","a")] make_polynomial_in t;
6.104 + term2str t;
6.105 + "x ^^^ 2 + (-1 * (b * x) + a * (b + -1 * x)) = 0";
6.106 + (*da sind wir fast am Ziel: make_polynomial_in 'a' sollte ergeben
6.107 + "x ^^^ 2 + (-1 * (b * x)) + (b + -1 * x) * a = 0"*)
6.108 +
6.109 + (*das rewriting l"asst sich beobachten mit
6.110 + trace_rewrite:=true;
6.111 + *)
6.112 +
6.113 +
6.114 +
6.115 +"------15.11.02 --------------------------";
6.116 + val t = (term_of o the o (parse thy)) "1 + a * x + b * x";
6.117 + val bdv = (term_of o the o (parse thy)) "bdv";
6.118 + val a = (term_of o the o (parse thy)) "a";
6.119 +
6.120 + trace_rewrite:=true;
6.121 + (* Anwenden einer Regelmenge aus Termorder.ML: *)
6.122 + val Some (t,_) =
6.123 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.124 + term2str t;
6.125 + val Some (t,_) =
6.126 + rewrite_set_ thy false discard_parentheses t;
6.127 + term2str t;
6.128 +"1 + b * x + x * a";
6.129 +
6.130 + val t = (term_of o the o (parse thy)) "1 + a * (x + b * x) + a^^^2";
6.131 + val Some (t,_) =
6.132 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.133 + term2str t;
6.134 + val Some (t,_) =
6.135 + rewrite_set_ thy false discard_parentheses t;
6.136 + term2str t;
6.137 +"1 + (x + b * x) * a + a ^^^ 2";
6.138 +
6.139 + val t = (term_of o the o (parse thy)) "1 + a ^^^2 * x + b * a + 7*a^^^2";
6.140 + val Some (t,_) =
6.141 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.142 + term2str t;
6.143 + val Some (t,_) =
6.144 + rewrite_set_ thy false discard_parentheses t;
6.145 + term2str t;
6.146 +"1 + b * a + (7 + x) * a ^^^ 2";
6.147 +
6.148 +(*
6.149 + Atools.thy grundlegende Algebra
6.150 + Poly.thy Polynome
6.151 + Rational.thy Br"uche
6.152 + Root.thy Wurzeln
6.153 + RootRat.thy Wurzen + Br"uche
6.154 + Termorder.thy BITTE NUR HIERHER SCHREIBEN
6.155 +
6.156 + cd"knowledge";
6.157 + remove_thy"Termorder";
6.158 + use_thy"Isac";
6.159 +
6.160 + get_thm Termorder.thy "bdv_n_collect";
6.161 + get_thm Isac.thy "bdv_n_collect";
6.162 +
6.163 +*)
6.164 + val t = (term_of o the o (parse thy)) "a ^^^2 * x + 7 * a^^^2";
6.165 + val Some (t,_) =
6.166 + rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in t;
6.167 + term2str t;
6.168 + val Some (t,_) =
6.169 + rewrite_set_ thy false discard_parentheses t;
6.170 + term2str t;
6.171 +"(7 + x) * a ^^^ 2";
6.172 +
6.173 + val t = (term_of o the o (parse Termorder.thy)) "Pi";
6.174 +
6.175 + val t = (term_of o the o (parseold thy)) "7";
6.176 +
6.177 +----------------------------------------------------------------------*)
6.178 \ No newline at end of file