1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Aug 30 14:35:51 2010 +0200
1.3 @@ -0,0 +1,2023 @@
1.4 +(*.tests for rationals
1.5 + author: Stefan Karnel
1.6 + Copyright (c) Stefan Karnel 2002
1.7 + Use is subject to license terms.
1.8 +
1.9 +use"../smltest/IsacKnowledge/rational.sml";
1.10 +use"rational.sml";
1.11 +
1.12 +LEGEND WN070906
1.13 + nonterm.SK marks non-terminating examples
1.14 + ord.SK PARTIALLY marks crucial ordering examples
1.15 + *SK* of some (secondary) interest (on 070906)
1.16 +****************************************************************.*)
1.17 +
1.18 +(******************************************************************
1.19 +WN060104 transfer marked (*SR..*)examples to the exp-collection
1.20 + # exp_IsacCore_Simp_Rat_Cancel.xml from rational.sml (*SRC*) 10 exp
1.21 + # exp_IsacCore_Simp_Rat_Add.xml from rational.sml (*SRA*) 11 exp
1.22 + # exp_IsacCore_Simp_Rat_Mult.xml from rational.sml (*SRM*) 5 exp
1.23 + # exp_IsacCore_Simp_Rat_AddMult.xml from rational.sml (*SRAM*) 11 exp
1.24 + # exp_IsacCore_Simp_Rat_Double.xml from rational.sml (*SRD*) 12 exp
1.25 +*******************************************************************)
1.26 +"-----------------------------------------------------------------";
1.27 +"table of contents -----------------------------------------------";
1.28 +"-----------------------------------------------------------------";
1.29 +"~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~~~~~~~~~~";
1.30 +"-------- ... missing WN060103 -----------------------------------";
1.31 +"-------- fun monom2term, fun poly2term' ------------------------";
1.32 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
1.33 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
1.34 +"-------- common_nominator_p ---------------------------- --------";
1.35 +"-------- reverse rewrite ----------------------------------------";
1.36 +"-------- 'reverse-ruleset' cancel_p -----------------------------";
1.37 +"-------- norm_Rational ------------------------------------------";
1.38 +"-------- numeral rationals --------------------------------------";
1.39 +"-------- cancellation -------------------------------------------";
1.40 +"-------- common denominator -------------------------------------";
1.41 +"-------- multiply and cancel ------------------------------------";
1.42 +"-------- common denominator and multiplication ------------------";
1.43 +"-------- double fractions ---------------------------------------";
1.44 +"-------- me Schalk I No.186 -------------------------------------";
1.45 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1.46 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1.47 +"-------- investigate rulesets for cancel_p ----------------------";
1.48 +"-------- investigate format of factout_ and factout_p_ ----------";
1.49 +"-----------------------------------------------------------------";
1.50 +"-----------------------------------------------------------------";
1.51 +"-----------------------------------------------------------------";
1.52 +
1.53 +
1.54 +"~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~~~~~~~~~~";
1.55 +(*.~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.56 + tests of internal functions: to make them work,
1.57 + out-comment (*!!!*) in knowledge/Rational.ML:
1.58 +(*##!!!
1.59 +structure RationalI : RATIONALI =
1.60 +struct
1.61 +!!!##*)
1.62 +
1.63 +(*##!!!
1.64 +end;(*struct*)
1.65 +open RationalI;
1.66 +!!!##*)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~.*)
1.67 +
1.68 +(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.69 +print("\n\n********************* rational.sml - TESTS *************************\n\n");
1.70 +print("\n\n***** divide tests *****\n");
1.71 +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.72 +(* result: [(1,[0,0,1]),(1,[0,0,0])] *)
1.73 +if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.74 +
1.75 +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.76 +(* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
1.77 +if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.78 +
1.79 +val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.80 +(* result: [(4,[1]),(4,[0])] *)
1.81 +if mv_pquot2=[(4,[1]),(4,[0])] then () else raise error ("rational.sml: example failed");
1.82 +
1.83 +val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.84 +(* result: [(12,[0]] *)
1.85 +if mv_prest2=[(12,[0])] then () else raise error ("rational.sml: example failed");
1.86 +
1.87 +val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
1.88 +(* [(2,[1]),(~2,[0])] *)
1.89 +if mv_pquot3=[(2,[1]),(~2,[0])] then () else raise error ("rational.sml: example failed");
1.90 +
1.91 +val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
1.92 +(* [(1,[2]),(~1,[0])] *)
1.93 +if mv_prest3=[(1,[2]),(~1,[0])] then () else raise error ("rational.sml: example failed");
1.94 +
1.95 +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.96 +(* [(1,[0,1,1])] *)
1.97 +if mv_pquot4=[(1,[0,1,1])] then () else raise error ("rational.sml: example failed");
1.98 +
1.99 +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.100 +(* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
1.101 +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.102 +
1.103 +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.104 +(* [(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.105 +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.106 +
1.107 +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.108 +(* [] *)
1.109 +if mv_prest5=[] then () else raise error ("rational.sml: example failed");
1.110 +
1.111 +(* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
1.112 +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.113 +if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.114 +
1.115 +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.116 +if mv_prest6=[] then () else raise error ("rational.sml: example failed");
1.117 +
1.118 +
1.119 +print("\n\n***** MV_CONTENT-TESTS *****\n");
1.120 +val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.121 +(* [(1,[0,1]),(1,[0,0])] *)
1.122 +if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.123 +
1.124 +val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.125 +(*[(1,[1,0]),(1,[0,0])]*)
1.126 +if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.127 +
1.128 +val mv_cont2=mv_content([(2,[1]),(4,[0])]);
1.129 +(* [(2,[0])] *)
1.130 +if mv_cont2=[(2,[0])] then () else raise error ("rational.sml: example failed");
1.131 +
1.132 +val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
1.133 +(* [(1,[1]),(2,[0])] *)
1.134 +if mv_pp2=[(1,[1]),(2,[0])] then () else raise error ("rational.sml: example failed");
1.135 +
1.136 +val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.137 +(* [(2,[0,0,0])] *)
1.138 +if mv_cont3=[(2,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.139 +
1.140 +val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.141 +(* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
1.142 +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.143 +
1.144 +val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.145 +(* [(1,[0,0,0])] *)
1.146 +if mv_cont4=[(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
1.147 +
1.148 +val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.149 +(* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
1.150 +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.151 +
1.152 +val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.153 +(* [(3,[0,0])] *)
1.154 +if con1=[(3,[0,0])] then () else raise error ("rational.sml: example failed");
1.155 +
1.156 +val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.157 +(* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
1.158 +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.159 +
1.160 +val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.161 +(* [(1,[0,0])] *)
1.162 +if con2=[(1,[0,0])] then () else raise error ("rational.sml: example failed");
1.163 +
1.164 +val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.165 +(* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
1.166 +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.167 +
1.168 +val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
1.169 +(* [(3,[0,1,0])] *)
1.170 +if cont1=[(3,[0,1,0])] then () else raise error ("rational.sml: example failed");
1.171 +
1.172 +val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
1.173 +(* [(1,[2,0,0])] *)
1.174 +if pp1=[(1,[2,0,0])] then () else raise error ("rational.sml: example failed");
1.175 +
1.176 +val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
1.177 +(* [(2,[0,1,0])] *)
1.178 +if cont2=[(2,[0,1,0])] then () else raise error ("rational.sml: example failed");
1.179 +
1.180 +val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
1.181 +(* [(1,[2,0,0]),(2,[1,1,0])] *)
1.182 +if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else raise error ("rational.sml: example failed");
1.183 +
1.184 +print("\n\n\n\n********************************************************\n\n");
1.185 +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.186 +if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
1.187 +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.188 +
1.189 +
1.190 +"-------- fun monom2term, fun poly2term' ------------------------";
1.191 +"-------- fun monom2term, fun poly2term' ------------------------";
1.192 +"-------- fun monom2term, fun poly2term' ------------------------";
1.193 +val t = monom2term ((3,[2,1,0]), ["c","b","a"](*reverse ???SK-*));
1.194 +term2str t = "3 * (c ^^^ 2 * b)" (*true*);
1.195 +
1.196 +val t = monom2term ((1,[1,0]), ["b","a"]);
1.197 +term2str t = "b" (*true*);
1.198 +
1.199 +val t = poly2term ([(1,[0,0,0]),(2,[1,0,0]),(3,[2,1,0]),(4,[3,2,1])],
1.200 + ["c","b","a"]);
1.201 +term2str t = "1 + 2 * c + 3 * (c ^^^ 2 * b) + 4 * (c ^^^ 3 * (b ^^^ 2 * a))";
1.202 +
1.203 +val t = poly2term ([(1,[1,0]),(1,[0,1])], ["b","a"]);
1.204 +term2str t = "a + b" (*true*);
1.205 +
1.206 +
1.207 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.208 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
1.209 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
1.210 +"~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
1.211 +
1.212 +
1.213 +fun parse_rat str = (term_of o the o (parse thy)) str;
1.214 +
1.215 +print("\n\n***** mv_gcd-tests *****\n");
1.216 +val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
1.217 +(* [(2,[1,1]),(2,[0,0])] *)
1.218 +if ggt1=[(2,[1,1]),(2,[0,0])] then () else raise error ("rational.sml: example failed");
1.219 +
1.220 +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.221 +(* [(2,[1,1,0]),(3,[0,0,1])] *)
1.222 +if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
1.223 +
1.224 +
1.225 +val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.226 +(* [(1,[1,0]),(~1,[0,1])] *)
1.227 +if ggt3=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
1.228 +
1.229 +
1.230 +val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
1.231 +(* [(1,[1,0,0])] *)
1.232 +if ggt4=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
1.233 +
1.234 +
1.235 +val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.236 +(* [(1,[1,0]),(~1,[0,1])] *)
1.237 +if ggt5=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
1.238 +
1.239 +
1.240 +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.241 +(* [(1,[0,0,0])] *)
1.242 +if ggt6=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
1.243 +
1.244 +print("\n\n***** kgv-tests *****\n");
1.245 +val kgv1=mv_lcm [(10,[])] [(15,[])];
1.246 +(* [(30,[])] *)
1.247 +if kgv1=[(30,[])] then () else raise error ("rational.sml: example failed");
1.248 +
1.249 +val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.250 +(* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
1.251 +if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else raise error ("rational.sml: example failed");
1.252 +
1.253 +val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.254 +(* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
1.255 +if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else raise error ("rational.sml: example failed");
1.256 +
1.257 +(*!!!--------
1.258 +print("\n\n***** STEP_CANCEL_TESTS: *****\n");
1.259 +
1.260 +val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) / (6 * a * c)";
1.261 +val div2 = term2str (step_cancel term2);
1.262 +if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else raise error ("rational.sml: example failed");
1.263 +
1.264 +
1.265 +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.266 +val div1 = term2str(step_cancel term1);
1.267 +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.268 +
1.269 +val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
1.270 +val div3 = term2str(step_cancel term3);
1.271 +if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else raise error ("rational.sml: example failed");
1.272 +
1.273 +--------------------------------------------------------------------------!!!*)
1.274 +
1.275 +(*-----versuche 13.3.03-----
1.276 + val t = str2term "1 - x^^^2 - 5 * x^^^5";
1.277 + val vs=(((map free2str) o vars) t);
1.278 + val SOME ml = expanded2poly t vs;
1.279 + poly2term (ml, vs);
1.280 + poly2term'(rev(sort (mv_geq LEX_) (ml)),vs);
1.281 + poly2term'([(~5,[5]),(~1,[2]),(1,[0])], vs);
1.282 + monom2term((~5,[5]),vs);
1.283 + monom2term((~1,[2]),vs);
1.284 + val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
1.285 +
1.286 + val (i,is) = (~1,[2]);
1.287 + val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
1.288 + (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
1.289 + Free ((str_of_int o abs) i, HOLogic.realT)) $
1.290 + powerproduct2term(is, vs);
1.291 + term2str ttt;
1.292 +-------versuche 13.3.03-----*)
1.293 +
1.294 + val t = str2term "1 - x^^^2 - 5 * x^^^5";
1.295 + val SOME t' = expanded2polynomial t; term2str t';
1.296 +"1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5";
1.297 + val t = str2term "1 - x";
1.298 + val SOME t' = expanded2polynomial t; term2str t';
1.299 +"1 + - 1 * x";
1.300 + val t = str2term "1 + (-1) * x";
1.301 + val SOME t' = expanded2polynomial t; term2str t';
1.302 +"1 + - 1 * x";
1.303 + val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5";
1.304 + val SOME t' = polynomial2expanded t; term2str t';
1.305 +"1 - x ^^^ 2 - 5 * x ^^^ 5";
1.306 +
1.307 +
1.308 +" external calculating functions test ";
1.309 +" external calculating functions test ";
1.310 +" external calculating functions test ";
1.311 +
1.312 +val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.313 +val SOME (t1',asm)= factout_p_ thy t1;
1.314 +term2str t1'; terms2str asm;
1.315 +"(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))";
1.316 +"[]";
1.317 +val SOME (t1',asm)= cancel_p_ thy t1;
1.318 +term2str t1'; terms2str asm;
1.319 +"(3 + 3 * x) / 2";
1.320 +"[\"1 + 1 * x ~= 0\"]";
1.321 +
1.322 +val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
1.323 +val SOME (t',asm)= cancel_ thy t;
1.324 +term2str t'; terms2str asm;
1.325 +"(3 - 3 * x) / 2";
1.326 +"[\"-1 + x ~= 0\"]";
1.327 +val SOME (t',asm)= factout_ thy t;
1.328 +term2str t'; terms2str asm;
1.329 +"(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))";
1.330 +"[]";
1.331 +
1.332 +val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.333 +val SOME (t',asm) = add_fraction_p_ thy t;
1.334 +term2str t'; terms2str asm;
1.335 +"(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)";
1.336 +"[]";
1.337 +val SOME (t',asm) = common_nominator_p_ thy t;
1.338 +term2str t'; terms2str asm;
1.339 +"(-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.340 +"[]";
1.341 +
1.342 +val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
1.343 +val SOME (t',asm) = add_fraction_ thy t;
1.344 +term2str t'; terms2str asm;
1.345 +"(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)";
1.346 +"[]";
1.347 +val SOME (t',asm) = common_nominator_ thy t;
1.348 +term2str t'; terms2str asm;
1.349 +"(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))";
1.350 +"[]";
1.351 +
1.352 +val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
1.353 +val SOME (t',asm) = common_nominator_p_ thy t;
1.354 +term2str t'; terms2str asm;
1.355 +"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.356 +"[]";
1.357 +val SOME (t',asm) = add_fraction_p_ thy t;
1.358 +term2str t'; terms2str asm;
1.359 +"1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
1.360 +"[\"1 + 1 * x ~= 0\"]";
1.361 +val SOME(t',asm) = norm_rational_ thy t;
1.362 +term2str t'; terms2str asm;
1.363 +"1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
1.364 +"[\"1 + 1 * x ~= 0\"]";
1.365 +
1.366 +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.367 +val SOME (t3',_) = common_nominator_ thy t3;
1.368 +val SOME (t3'',_) = add_fraction_ thy t3;
1.369 +(term2str t3');
1.370 +(term2str t3'');
1.371 +
1.372 +val SOME(t4,t5) = norm_expanded_rat_ thy t3;
1.373 +term2str t4;
1.374 +term2str (hd(t5));
1.375 +
1.376 +
1.377 +
1.378 + val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
1.379 + val SOME (t',_) = factout_ thy t;
1.380 + val SOME (t'',_) = cancel_ thy t;
1.381 + term2str t';
1.382 + term2str t'';
1.383 + "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
1.384 + "(3 + x) / (3 - x)";
1.385 +
1.386 + val t=(term_of o the o (parse thy))
1.387 + "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)";
1.388 + val SOME (t',_) = common_nominator_ thy t;
1.389 + val SOME (t'',_) = add_fraction_ thy t;
1.390 + term2str t';
1.391 + term2str t'';
1.392 + "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))";
1.393 + "(4 + x) / (3 - x)";
1.394 +
1.395 +(*WN021016 added -----vv---*)
1.396 +val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
1.397 +val SOME (t',_) = common_nominator_ thy t;
1.398 +val SOME (t'',_) = add_fraction_ thy t;
1.399 +term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1\
1.400 + \ * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
1.401 +term2str t'' = "6 / (3 - x)" (*true*);
1.402 +
1.403 +val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
1.404 +val SOME (t',_) = common_nominator_ thy t;
1.405 +val SOME (t'',_) = add_fraction_ thy t;
1.406 +term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n\
1.407 + \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
1.408 +term2str t'' = "6 / (3 - x)" (*true*);
1.409 +(*WN021016 added -----^^---*)
1.410 +(*WN030602 added -----vv--- no rewrite -> NONE !*)
1.411 +val t = str2term "1 / a";
1.412 +val NONE = cancel_p_ thy t;
1.413 +val NONE = rewrite_set_ thy false cancel_p t;
1.414 +(*WN.2.6.03 added -------^^---*)
1.415 +
1.416 +val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
1.417 +val SOME (t',_) = factout_ thy t;
1.418 +val SOME (t'',_) = cancel_ thy t;
1.419 +term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*);
1.420 +term2str t'' = "(y + x) / (y - x)";
1.421 +
1.422 +val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
1.423 +val SOME (t',_) = common_nominator_ thy t;
1.424 +val SOME (t'',_) = add_fraction_ thy t;
1.425 +term2str t' =
1.426 +"(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1\
1.427 +\ * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*);
1.428 +term2str t'' = "(-1 - x - y) / (x - y)" (*true*);
1.429 +
1.430 +val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
1.431 +val SOME (t',_) = common_nominator_ thy t;
1.432 +val SOME (t'',_) = add_fraction_ thy t;
1.433 +if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\
1.434 +\ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then ()
1.435 +else raise error "rational.sml lex-ord 1";
1.436 +if term2str t'' = "(-1 - y - x) / (y - x)" then ()
1.437 +else raise error "rational.sml lex-ord 2";
1.438 +(*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*)
1.439 +
1.440 +
1.441 +val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
1.442 +val SOME (t',_) = norm_expanded_rat_ thy t;
1.443 +if term2str t' = "(x + y) / (x - y)" then ()
1.444 +else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
1.445 +(*val SOME (t'',_) = norm_rational_ thy t;
1.446 + *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
1.447 +WN.16.10.02 ?! + WN060831???SK4
1.448 +WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*)
1.449 +
1.450 +
1.451 +val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
1.452 +val SOME (t',_) = norm_expanded_rat_ thy t;
1.453 +if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then ()
1.454 +else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
1.455 +(*val SOME (t'',_) = norm_rational_ thy t;
1.456 + *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!
1.457 +WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*)
1.458 +
1.459 + val t=(term_of o the o (parse thy))
1.460 + "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
1.461 + val SOME (t',_) = norm_expanded_rat_ thy t;
1.462 + val SOME (t'',_) = norm_rational_ thy t;
1.463 + term2str t';
1.464 + term2str t'';
1.465 + "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
1.466 + "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)";
1.467 +
1.468 +
1.469 +" examples from: Mathematik 1 Schalk Reniets Verlag ";
1.470 +" examples from: Mathematik 1 Schalk Reniets Verlag ";
1.471 +" examples from: Mathematik 1 Schalk Reniets Verlag ";
1.472 +
1.473 +
1.474 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
1.475 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
1.476 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
1.477 +val thy' = "Rational.thy";
1.478 +val rls' = "cancel";
1.479 +val mp = "make_polynomial";
1.480 +
1.481 +print("\n\nexample 186:\n");
1.482 +print("a)\n");
1.483 +val e186a'="(14 * x * y) / ( x * y )";(*SRC*)
1.484 +val e186a = the (rewrite_set thy' false "cancel" e186a');
1.485 + is_expanded (parse_rat "14 * x * y");
1.486 + is_expanded (parse_rat "x * y");
1.487 +
1.488 +print("b)\n");
1.489 +val e186b'="(60 * a * b) / ( 15 * a * b )";
1.490 +val e186b = the (rewrite_set thy' false "cancel" e186b');
1.491 +print("c)\n");
1.492 +val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
1.493 +val e186c = (the (rewrite_set thy' false "cancel" e186c'))
1.494 + handle e => print_exn e;
1.495 +val t = (term_of o the o (parse thy)) e186c';
1.496 +atomt t;
1.497 +
1.498 +print("\n\nexample 187:\n");
1.499 +print("a)\n");
1.500 +val e187a'="(12 * x * y) / (8 * y^^^2 )";(*SRC*)
1.501 +val e187a = the (rewrite_set thy' false "cancel" e187a');
1.502 +print("b)\n");
1.503 +val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
1.504 +val e187b = the (rewrite_set thy' false "cancel" e187b');
1.505 +print("c)\n");
1.506 +val e187c'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*)
1.507 +val e187c = the (rewrite_set thy' false "cancel" e187c');
1.508 +
1.509 +"example 188:";
1.510 +val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*)
1.511 +val e188a = the (rewrite_set thy' false "cancel" e188a');
1.512 + is_expanded (parse_rat "8 * x + -8");
1.513 +(* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
1.514 +if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
1.515 +else raise error "rational.sml: e188a new behaviour";
1.516 +val SOME (t,_) = rewrite_set thy' false mp
1.517 + "(8*((-1) + x))/(9*((-1) + x))";
1.518 +print("b)\n");
1.519 +val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
1.520 +val SOME (t,_) = rewrite_set thy' false "cancel" e188b';
1.521 +t = "5 / 6" (*true*);
1.522 +print("c)\n");
1.523 +
1.524 +val e188c'="( a + -1 * b ) / ( b + -1 * a )";
1.525 +val e188c = the (rewrite_set thy' false "cancel_p" e188c');
1.526 +(*is_expanded (parse_rat "a + -1 * b");*)
1.527 +val SOME (t,_) =
1.528 + rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
1.529 +if t= "(a + -1 * b) / (-1 * a + b)" then()
1.530 +else raise error "rational.sml: e188c new behaviour";
1.531 +
1.532 +print("\n\nexample 190:\n");
1.533 +print("c)\n");
1.534 +val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
1.535 +val e190c = the (rewrite_set thy' false "cancel" e190c');
1.536 +val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1.537 +if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
1.538 +else raise error "rational.sml: e190c new behaviour";
1.539 +
1.540 +print("\n\nexample 191:\n");
1.541 +print("a)\n");
1.542 +val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )";
1.543 +(*WN.23.10.02-------
1.544 +val e191a = the (rewrite_set thy' false "cancel" e191a');
1.545 + is_expanded (parse_rat "x^^^2 + -1 * y^^^2");
1.546 + false;
1.547 + is_expanded (parse_rat "x + y");
1.548 + true; -----------*)
1.549 +val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
1.550 +(* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
1.551 +if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
1.552 +else raise error "rational.sml: e191a new behaviour";
1.553 +
1.554 +print("c)\n");
1.555 +val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
1.556 +(*WN.23.10.02-------
1.557 +val e191c = the (rewrite_set thy' false "cancel" e191c');
1.558 + is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25");
1.559 + false;
1.560 + is_expanded (parse_rat "25 + -30*x + 9*x^^^2");
1.561 + false;
1.562 + is_expanded (parse_rat "-25 + 9*x^^^2");
1.563 + true;------------*)
1.564 +val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
1.565 +(* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
1.566 +if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
1.567 +else raise error "rational.sml: 'e191c' new behaviour";
1.568 +
1.569 +
1.570 +print("\n\nexample 192:\n");
1.571 +print("b)\n");
1.572 +val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
1.573 +(*WN.23.10.02-------
1.574 +val e192b = the (rewrite_set thy' false "cancel" e192b');
1.575 +-------------------*)
1.576 +val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.577 +if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)"
1.578 +(*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*)
1.579 +then () else raise error "rational.sml: 'e192b' new behaviour";
1.580 +(*^^^ works with MG's simplifier vvv*)
1.581 +val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.582 +val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
1.583 +if term2str t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)" then () else raise error "rational.sml: 'e192b'MG new behaviour";
1.584 +
1.585 +
1.586 +print("\n\nexample 193:\n");
1.587 +print("a)\n");
1.588 +val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
1.589 +(*WN.23.10.02-------
1.590 +val e193a = the (rewrite_set thy' false "cancel" e193a');
1.591 +-------------------*)
1.592 +print("b)\n");
1.593 +val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
1.594 +(*WN.23.10.02-------
1.595 +val e193b = the (rewrite_set thy' false "cancel" e193b');
1.596 +print("c)\n");
1.597 +val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
1.598 +val SOME(t,_) = rewrite_set thy' false "cancel" e193c';
1.599 +-------------------*)
1.600 +
1.601 +val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
1.602 +val SOME (t,_) = rewrite_set thy' false "cancel" wn01;
1.603 +(* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
1.604 +if t = "(-5 + 3 * x) / 1" then ()
1.605 +else raise error "rational.sml: new behav. in cancel wn01";
1.606 +
1.607 +
1.608 +"-------- common_nominator_p ---------------------------- --------";
1.609 +"-------- common_nominator_p ---------------------------- --------";
1.610 +"-------- common_nominator_p ---------------------------- --------";
1.611 +val rls' = "common_nominator_p";
1.612 +
1.613 +print("\n\nexample 204:\n");
1.614 +print("a)\n");
1.615 +val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)";
1.616 +val e204a = the (rewrite_set thy' false "common_nominator_p" e204a');
1.617 +print("b)\n");
1.618 +val e204b'="5 / x + -3 / x + -1 / x";
1.619 +val e204b = the (rewrite_set thy' false "common_nominator_p" e204b');
1.620 +
1.621 +print("\n\nexample 205:\n");
1.622 +print("a)\n");
1.623 +val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)";
1.624 +val e205a = the (rewrite_set thy' false "common_nominator_p" e205a');
1.625 +print("b)\n");
1.626 +val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)";
1.627 +val e205b = the (rewrite_set thy' false "common_nominator_p" e205b');
1.628 +
1.629 +print("\n\nexample 206:\n");
1.630 +print("a)\n");
1.631 +val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))";
1.632 +val e206a = the (rewrite_set thy' false "common_nominator_p" e206a');
1.633 +print("b)\n");
1.634 +val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))";
1.635 +val e206b = the (rewrite_set thy' false "common_nominator_p" e206b');
1.636 +
1.637 +print("\n\nexample 207:\n");
1.638 +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.639 +val e207 = the (rewrite_set thy' false "common_nominator_p" e207');
1.640 +
1.641 +print("\n\nexample 208:\n");
1.642 +val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) ";
1.643 +val e208 = the (rewrite_set thy' false "common_nominator_p" e208');
1.644 +
1.645 +print("\n\nexample 209:\n");
1.646 +val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) ";
1.647 +val e209 = the (rewrite_set thy' false "common_nominator_p" e209');
1.648 +
1.649 +print("\n\nexample 210:\n");
1.650 +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.651 +val e210 = the (rewrite_set thy' false "common_nominator_p" e210');
1.652 +
1.653 +print("\n\nexample 211:\n");
1.654 +print("a)\n");
1.655 +val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))";
1.656 +val e211a = the (rewrite_set thy' false "common_nominator_p" e211a');
1.657 +print("b)\n");
1.658 +val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))";
1.659 +val e211b = the (rewrite_set thy' false "common_nominator_p" e211b');
1.660 +
1.661 +print("\n\nexample 212:\n");
1.662 +print("a)\n");
1.663 +val e212a'="((4) / (x)) + ((-3) / (y)) + -1";
1.664 +val e212a = the (rewrite_set thy' false "common_nominator_p" e212a');
1.665 +print("b)\n");
1.666 +val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))";
1.667 +val e212b = the (rewrite_set thy' false "common_nominator_p" e212b');
1.668 +
1.669 +print("\n\nexample 213:\n");
1.670 +print("a)\n");
1.671 +val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) ";
1.672 +val e213a = the (rewrite_set thy' false "common_nominator_p" e213a');
1.673 +print("b)\n");
1.674 +val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))";
1.675 +val e213b = the (rewrite_set thy' false "common_nominator_p" e213b');
1.676 +
1.677 +print("\n\nexample 214:\n");
1.678 +print("a)\n");
1.679 +val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))";
1.680 +val e214a = the (rewrite_set thy' false "common_nominator_p" e214a');
1.681 +print("b)\n");
1.682 +val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))";
1.683 +val e214b = the (rewrite_set thy' false "common_nominator_p" e214b');
1.684 +
1.685 +print("\n\nexample 216:\n");
1.686 +print("a)\n");
1.687 +val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))";
1.688 +val e216a = the (rewrite_set thy' false "common_nominator_p" e216a');
1.689 +print("b)\n");
1.690 +val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))";
1.691 +val e216b = the (rewrite_set thy' false "common_nominator_p" e216b');
1.692 +
1.693 +print("\n\nexample 217:\n");
1.694 +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.695 +val e217 = the (rewrite_set thy' false "common_nominator_p" e217');
1.696 +
1.697 +
1.698 +val rls' = "common_nominator";
1.699 +print("\n\nexample 218:\n");
1.700 +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.701 +val e218 = the (rewrite_set thy' false "common_nominator" e218');
1.702 +
1.703 +print("\n\nexample 219:\n");
1.704 +print("a)\n");
1.705 +val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))";
1.706 +val e219a = the (rewrite_set thy' false "common_nominator" e219a');
1.707 +print("b)\n");
1.708 +val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))";
1.709 +val e219b = the (rewrite_set thy' false "common_nominator" e219b');
1.710 +
1.711 +print("\n\nexample 220:\n");
1.712 +print("a)\n");
1.713 +val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))";
1.714 +val e220a = the (rewrite_set thy' false "common_nominator" e220a');
1.715 +print("b)\n");
1.716 +val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))";
1.717 +val e220b = the (rewrite_set thy' false "common_nominator" e220b');
1.718 +
1.719 +print("\n\nexample 221:\n");
1.720 +print("a)\n");
1.721 +val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))";
1.722 +val e221a = the (rewrite_set thy' false "common_nominator" e221a');
1.723 +print("b)\n");
1.724 +val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) ";
1.725 +val e221b = the (rewrite_set thy' false "common_nominator" e221b');
1.726 +
1.727 +print("\n\nexample 222:\n");
1.728 +print("a)\n");
1.729 +val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))";
1.730 +val e222a = the (rewrite_set thy' false "common_nominator" e222a');
1.731 +print("b)\n");
1.732 +val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))";
1.733 +val e222b = the (rewrite_set thy' false "common_nominator" e222b');
1.734 +
1.735 +print("\n\nexample 225:\n");
1.736 +print("a)\n");
1.737 +val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))";
1.738 +val e225a = the (rewrite_set thy' false "common_nominator" e225a');
1.739 +print("b)\n");
1.740 +val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))";
1.741 +val e225b = the (rewrite_set thy' false "common_nominator" e225b');
1.742 +
1.743 +print("\n\nexample 226:\n");
1.744 +print("a)\n");
1.745 +val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) ";
1.746 +val e226a = the (rewrite_set thy' false "common_nominator" e226a');
1.747 +print("b)\n");
1.748 +val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2";
1.749 +val e226b = the (rewrite_set thy' false "common_nominator" e226b');
1.750 +
1.751 +print("\n\nexample 227:\n");
1.752 +print("a)\n");
1.753 +val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 ";
1.754 +val e227a = the (rewrite_set thy' false "common_nominator" e227a');
1.755 +print("b)\n");
1.756 +val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 ";
1.757 +val e227b = the (rewrite_set thy' false "common_nominator" e227b');
1.758 +
1.759 +print("\n\nexample 228:\n");
1.760 +print("a)\n");
1.761 +val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))";
1.762 +val e228a = the (rewrite_set thy' false "common_nominator" e228a');
1.763 +print("b)\n");
1.764 +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.765 +val e228b = the (rewrite_set thy' false "common_nominator" e228b');
1.766 +
1.767 +
1.768 +print("\n\nexample 229:\n");
1.769 +print("a)\n");
1.770 +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.771 +val e229a = the (rewrite_set thy' false "common_nominator" e229a');
1.772 +print("b)\n");
1.773 +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.774 +val e229b = the (rewrite_set thy' false "common_nominator" e229b');
1.775 +
1.776 +print("\n\nexample 230:\n");
1.777 +print("a)\n");
1.778 +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.779 +val e230a = the (rewrite_set thy' false "common_nominator" e230a');
1.780 +print("b)\n");
1.781 +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.782 +val e230b = the (rewrite_set thy' false "common_nominator" e230b');
1.783 +
1.784 +print("\n\nexample 231:\n");
1.785 +print("a)\n");
1.786 +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.787 +val e231a = the (rewrite_set thy' false "common_nominator" e231a');
1.788 +print("b)\n");
1.789 +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.790 +val e231b = the (rewrite_set thy' false "common_nominator" e231b');
1.791 +
1.792 +print("\n\nexample 232:\n");
1.793 +print("a)\n");
1.794 +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.795 +val e232a = the (rewrite_set thy' false "common_nominator" e232a');
1.796 +print("b)\n");
1.797 +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.798 +val e232b = the (rewrite_set thy' false "common_nominator" e232b');
1.799 +
1.800 +print("\n\nexample 233:\n");
1.801 +print("a)\n");
1.802 +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.803 +val e233a = the (rewrite_set thy' false "common_nominator" e233a');
1.804 +print("b)\n");
1.805 +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.806 +val e233b = the (rewrite_set thy' false "common_nominator" e233b');
1.807 +
1.808 +print("\n\nexample 234:\n");
1.809 +print("a)\n");
1.810 +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.811 +val e234a = the (rewrite_set thy' false "common_nominator" e234a');
1.812 +print("b)\n");
1.813 +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.814 +val e234b = the (rewrite_set thy' false "common_nominator" e234b');
1.815 +
1.816 +print("\n\nexample 235:\n");
1.817 +print("a)\n");
1.818 +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.819 +val e235a = the (rewrite_set thy' false "common_nominator" e235a');
1.820 +print("b)\n");
1.821 +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.822 +val e235b = the (rewrite_set thy' false "common_nominator" e235b');
1.823 +
1.824 +print("\n\nexample 236:\n");
1.825 +print("a)\n");
1.826 +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.827 +val e236a = the (rewrite_set thy' false "common_nominator" e236a');
1.828 +print("b)\n");
1.829 +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.830 +val e236b = the (rewrite_set thy' false "common_nominator" e236b');
1.831 +
1.832 +
1.833 +val rls' = "cancel";
1.834 +print("\n\nexample heuberger:\n");
1.835 +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.836 +val eheu = the (rewrite_set thy' false "cancel" eheu');
1.837 +
1.838 +val rls' = "common_nominator_p";
1.839 +print("\n\nexample stiefel:\n");
1.840 +val est1'="(7) / (-14) + (-2) / (4)";
1.841 +val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
1.842 +if est1 = ("-1 / 1",[]) then ()
1.843 +else raise error "new behaviour in rational.sml: est1'";
1.844 +
1.845 +val t = (term_of o the o (parse thy))
1.846 +"(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
1.847 +val SOME (t',_) = factout_ thy t;
1.848 +term2str t';
1.849 +"(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
1.850 +
1.851 +
1.852 +"-------- reverse rewrite ----------------------------------------";
1.853 +"-------- reverse rewrite ----------------------------------------";
1.854 +"-------- reverse rewrite ----------------------------------------";
1.855 +
1.856 +(*WN.28.8.02: tests for the 'reverse-rewrite' functions:
1.857 + these are defined in Rationals.ML and stored in
1.858 + the 'reverse-ruleset' cancel*)
1.859 +
1.860 +(*the term for which reverse rewriting is demonstrated*)
1.861 + val t = (term_of o the o (parse thy))
1.862 + "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
1.863 + val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.864 + next_rule=nex,normal_form=nor,...},...} = cancel;
1.865 +
1.866 +(*normal_form produces the result in ONE step*)
1.867 + val SOME (t',_) = nor t;
1.868 + term2str t';
1.869 +
1.870 +(*initialize the interpreter state used by the 'me'*)
1.871 + val (t,_,revsets,_) = ini t;
1.872 +
1.873 +(*find the rule 'r' to apply to term 't'*)
1.874 + val SOME r = nex revsets t;
1.875 + (*val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
1.876 +
1.877 +(*check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
1.878 + if the rule is OK, the term resulting from applying the rule is returned,too;
1.879 + there might be several rule applications inbetween,
1.880 + which are listed after the head in reverse order*)
1.881 + val (r,(t,asm))::_ = loc revsets t r;
1.882 + term2str t;
1.883 + "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
1.884 +
1.885 +(*find the next rule to apply*)
1.886 + val SOME r = nex revsets t;
1.887 + (*val r = Thm ("sym_#power_3_2","9 = 3 ^^^ 2") : rule*)
1.888 +
1.889 +(*check the next rule*)
1.890 + val (r,(t,asm))::_ = loc revsets t r;
1.891 + term2str t;
1.892 + "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
1.893 +
1.894 +(*find and check the next rules, rewrite*)
1.895 + val SOME r = nex revsets t;
1.896 + val (r,(t,asm))::_ = loc revsets t r;
1.897 + term2str t;
1.898 + "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
1.899 +
1.900 + val SOME r = nex revsets t;
1.901 + val (r,(t,asm))::_ = loc revsets t r;
1.902 + term2str t;
1.903 + "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
1.904 +
1.905 + val SOME r = nex revsets t;
1.906 + val (r,(t,asm))::_ = loc revsets t r;
1.907 + term2str t;
1.908 + "(3 - x) * (3 + x) / ((3 + x) * (3 + x))";
1.909 +
1.910 + val SOME r = nex revsets t;
1.911 + val (r,(t,asm))::_ = loc revsets t r;
1.912 + val ss = term2str t;
1.913 + if ss = "(3 - x) / (3 + x)" then ()
1.914 + else raise error "rational.sml: new behav. in rev-set cancel";
1.915 + terms2str asm;
1.916 +
1.917 +
1.918 +"-------- 'reverse-ruleset' cancel_p -----------------------------";
1.919 +"-------- 'reverse-ruleset' cancel_p -----------------------------";
1.920 +"-------- 'reverse-ruleset' cancel_p -----------------------------";
1.921 +(*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
1.922 +
1.923 +(*the term for which reverse rewriting is demonstrated*)
1.924 +val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
1.925 +val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
1.926 + next_rule=nex,normal_form=nor,...},...} = cancel_p;
1.927 +
1.928 +(*normal_form produces the result in ONE step*)
1.929 +val SOME (t',_) = nor t;
1.930 +term2str t' = "(3 + 1 * x) / (3 + -1 * x)";
1.931 +
1.932 +(*initialize the interpreter state used by the 'me'*)
1.933 +val SOME (t', asm) = cancel_p_ thy t;
1.934 +term2str t' = "(3 + x) / (3 + -1 * x)" (*true*);
1.935 +terms2str asm = "[\"3 + -1 * x ~= 0\"]" (*true*);
1.936 +val (t,_,revsets,_) = ini t;
1.937 +
1.938 +(* WN.10.10.02: dieser Fall terminiert nicht
1.939 + (make_polynomial enth"alt zu viele rules)
1.940 +WN060823 'init_state' requires rewriting on specified location in the term
1.941 +print_depth 99; Rfuns; print_depth 3;
1.942 +WN060831 cycling "sym_order_mult_rls_" "sym_real_mult_assoc"
1.943 + as was with make_polynomial before ?!?*)
1.944 +
1.945 +val SOME r = nex revsets t;
1.946 +eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",
1.947 + mk_thm Rational.thy "9 = 3 ^^^ 2"));
1.948 +(*WN060831 *** id_of_thm
1.949 + Exception- ERROR raised ...
1.950 +val (r,(t,asm))::_ = loc revsets t r;
1.951 +term2str t;
1.952 +
1.953 + val SOME r = nex revsets t;
1.954 + val (r,(t,asm))::_ = loc revsets t r;
1.955 + term2str t;
1.956 +*)
1.957 +
1.958 +print "\n\n\n****************** all tests successfull *************************\n";
1.959 +
1.960 +
1.961 +
1.962 +(*WN.17.3.03 =========================================================vvv---*)
1.963 +"-------- norm_Rational ------------------------------------------";
1.964 +"-------- norm_Rational ------------------------------------------";
1.965 +"-------- norm_Rational ------------------------------------------";
1.966 +val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
1.967 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.968 +if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1";
1.969 +
1.970 +val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
1.971 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.972 +if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
1.973 +else raise error "rational.sml 2";
1.974 +
1.975 +val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
1.976 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.977 +(*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
1.978 +if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
1.979 +else raise error "rational.sml 3";
1.980 +(*trace_rewrite:=true;*)
1.981 +val t = str2term "Not (6*x is_atom)";
1.982 +val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1.983 +"True";
1.984 +val t = str2term "1 < 2";
1.985 +val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1.986 +"True";
1.987 +val t = str2term "(6*x)^^^2";
1.988 +val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
1.989 + (num_str realpow_def_atom) t;
1.990 +term2str t';
1.991 +trace_rewrite:=false;
1.992 +
1.993 +val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
1.994 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.995 +if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4";
1.996 +
1.997 +val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
1.998 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.999 +(*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
1.1000 +if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
1.1001 +else raise error "rational.sml 5";
1.1002 +
1.1003 +(*SRAM Schalk I, p.92 Nr. 609a*)
1.1004 +val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
1.1005 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1006 +if term2str t' = "(-255 + 112 * x) / 135" then ()
1.1007 +else raise error "rational.sml 6";
1.1008 +
1.1009 +(*SRAM Schalk I, p.92 Nr. 610c*)
1.1010 +val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
1.1011 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1012 +if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7";
1.1013 +
1.1014 +(*SRAM Schalk I, p.92 Nr. 476a*)
1.1015 +val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\
1.1016 + \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
1.1017 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1018 +(*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*)
1.1019 +if term2str t' = "1" then () else raise error "rational.sml 8";
1.1020 +
1.1021 +(*............................vvv---TODO: sollte gehen mit poly_order *)
1.1022 +(*Schalk I, p.92 Nr. 472a*)
1.1023 +val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
1.1024 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1025 +if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a";
1.1026 +
1.1027 +(*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1.1028 +val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.1029 + \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1.1030 + \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1.1031 + \(20*x*y/(x^^^2 - 25*y^^^2))";
1.1032 +(*... nicht simpl, zerlegt ...*)
1.1033 +val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.1034 + \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))";
1.1035 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1036 +"(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
1.1037 +(* ~~~~~~~~~~ poly_order notwendig!*)
1.1038 +val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1.1039 + \(20*x*y/(x^^^2 - 25*y^^^2))";
1.1040 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1041 +"(-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.1042 +trace_rewrite:=true;
1.1043 +trace_rewrite:=false;
1.1044 +
1.1045 +"nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
1.1046 +(*WN.2.6.03 from rlang.sml 56a
1.1047 +val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x) = 4 * (a * b) / (a ^^^ 2 + -1 * b ^^^ 2)";
1.1048 +val NONE = rewrite_set_ thy false common_nominator_p t;
1.1049 +
1.1050 +WN060831 nonterm.SK7
1.1051 +val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1.1052 +val NONE = add_fraction_p_ thy t;
1.1053 +*)
1.1054 +
1.1055 +
1.1056 +(* ------------------------------------------------------------------- *)
1.1057 +(*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
1.1058 +(* Simplifier fuer beliebige Buchterme *)
1.1059 +(* ------------------------------------------------------------------- *)
1.1060 +(*----------------------- norm_Rational_mg ----------------------------*)
1.1061 +(* ------------------------------------------------------------------- *)
1.1062 +
1.1063 +"-------- numeral rationals --------------------------------------";
1.1064 +"-------- numeral rationals --------------------------------------";
1.1065 +"-------- numeral rationals --------------------------------------";
1.1066 +
1.1067 +(*SRA Schalk I, p.40 Nr. 164b *)
1.1068 +val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
1.1069 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1070 +term2str t;
1.1071 +if (term2str t) = "19 / 21" then ()
1.1072 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
1.1073 +
1.1074 +(*SRA Schalk I, p.40 Nr. 166a *)
1.1075 +val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1.1076 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1077 +term2str t;
1.1078 +if (term2str t) = "45 / 2" then ()
1.1079 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
1.1080 +
1.1081 +
1.1082 +"-------- cancellation -------------------------------------------";
1.1083 +"-------- cancellation -------------------------------------------";
1.1084 +"-------- cancellation -------------------------------------------";
1.1085 +
1.1086 +(* e190c Stefan K.*)
1.1087 +val t = str2term
1.1088 +"((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1.1089 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1090 +term2str t;
1.1091 +if (term2str t) =
1.1092 +"(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.1093 +then ()
1.1094 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
1.1095 +
1.1096 +(* e192b Stefan K.*)
1.1097 +val t = str2term
1.1098 +"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.1099 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1100 +term2str t;
1.1101 +if (term2str t) =
1.1102 +"x ^^^ 2 / y ^^^ 2"
1.1103 +then ()
1.1104 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
1.1105 +
1.1106 +(*SRC Schalk I, p.66 Nr. 379c *)
1.1107 +val t = str2term
1.1108 +"(a - b)/(b - a)";
1.1109 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1110 +term2str t;
1.1111 +if (term2str t) =
1.1112 +"-1"
1.1113 +then ()
1.1114 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
1.1115 +
1.1116 +(*SRC Schalk I, p.66 Nr. 380b *)
1.1117 +val t = str2term
1.1118 +"15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
1.1119 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1120 +term2str t;
1.1121 +if (term2str t) =
1.1122 +"(27 + 12 * x) / (28 + 8 * x)"
1.1123 +then ()
1.1124 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1.1125 +
1.1126 +(*Schalk I, p.60 Nr. 215c *)
1.1127 +(* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
1.1128 +(* WN060831????MG1
1.1129 +val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1.1130 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1131 +term2str t;
1.1132 +if (term2str t) =
1.1133 +"(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.1134 +then ()
1.1135 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
1.1136 +*)
1.1137 +(*val t = str2term
1.1138 +"(a ^^^ 4 * x + -1 * a ^^^ 4 * y + 4 * a ^^^ 3 * b * x + -4 * a ^^^ 3 * b * y + 6 * a ^^^ 2 * b ^^^ 2 * x + -6 * a ^^^ 2 * b ^^^ 2 * y + 4 * a * b ^^^ 3 * x + -4 * a * b ^^^ 3 * y + b ^^^ 4 * x + -1 * b ^^^ 4 * y) /(a ^^^ 2 * x ^^^ 3 + -3 * a ^^^ 2 * x ^^^ 2 * y + 3 * a ^^^ 2 * x * y ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 3 + 2 * a * b * x ^^^ 3 + -6 * a * b * x ^^^ 2 * y + 6 * a * b * x * y ^^^ 2 + -2 * a * b * y ^^^ 3 + b ^^^ 2 * x ^^^ 3 + -3 * b ^^^ 2 * x ^^^ 2 * y + 3 * b ^^^ 2 * x * y ^^^ 2 + -1 * b ^^^ 2 * y ^^^ 3)"
1.1139 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1140 +term2str t;*)
1.1141 +(* uncaught exception nonexhaustive binding failure
1.1142 + raised at: stdIn:93.1-93.51 *)
1.1143 +
1.1144 +(*Schalk I, p.66 Nr. 381a *)
1.1145 +(* ACHTUNG: rechnet ca. 2 Minuten !!! *)
1.1146 +(* WN060831???MG2
1.1147 +val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
1.1148 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1149 +term2str t;
1.1150 +if (term2str t) =
1.1151 +"(a + b) / (4 * a + -4 * b)"
1.1152 +then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1.1153 +*)
1.1154 +
1.1155 +(*SRC Schalk I, p.66 Nr. 381b *)
1.1156 +val t = str2term
1.1157 +"(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1.1158 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1159 +term2str t;
1.1160 +if (term2str t) =
1.1161 +"-1 / (5 + -2 * x)"
1.1162 +then ()
1.1163 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
1.1164 +
1.1165 +(*SRC Schalk I, p.66 Nr. 381c *)
1.1166 +val t = str2term
1.1167 +"(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
1.1168 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1169 +term2str t;
1.1170 +if (term2str t) =
1.1171 +"(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1.1172 +then ()
1.1173 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
1.1174 +
1.1175 +(*SRC Schalk I, p.66 Nr. 383a *)
1.1176 +val t = str2term
1.1177 +"(5*a^^^2 - 5*a*b)/(a - b)^^^2";
1.1178 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1179 +term2str t;
1.1180 +if (term2str t) =
1.1181 +"5 * a / (a + -1 * b)"
1.1182 +then ()
1.1183 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
1.1184 +
1.1185 +"-------- common denominator -------------------------------------";
1.1186 +"-------- common denominator -------------------------------------";
1.1187 +"-------- common denominator -------------------------------------";
1.1188 +
1.1189 +(*SRA Schalk I, p.67 Nr. 403a *)
1.1190 +val t = str2term
1.1191 +"4/x - 3/y - 1";
1.1192 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1193 +term2str t;
1.1194 +if (term2str t) =
1.1195 +"(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1.1196 +then ()
1.1197 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
1.1198 +
1.1199 +(*SRA Schalk I, p.67 Nr. 407b *)
1.1200 +val t = str2term
1.1201 +"(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
1.1202 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1203 +term2str t;
1.1204 +if (term2str t) =
1.1205 +"4 / c"
1.1206 +then ()
1.1207 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
1.1208 +
1.1209 +(*SRA Schalk I, p.67 Nr. 410b *)
1.1210 +val t = str2term
1.1211 +"1/(x+1) + 1/(x+2) - 2/(x+3)";
1.1212 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1213 +term2str t;
1.1214 +if (term2str t) =
1.1215 +"(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1.1216 +then ()
1.1217 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
1.1218 +
1.1219 +(*SRA Schalk I, p.67 Nr. 413b *)
1.1220 +val t = str2term
1.1221 +"(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
1.1222 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1223 +term2str t;
1.1224 +if (term2str t) =
1.1225 +"6 * x / (1 + -1 * x ^^^ 2)"
1.1226 +then ()
1.1227 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
1.1228 +
1.1229 +(*SRA Schalk I, p.68 Nr. 414a *)
1.1230 +val t = str2term
1.1231 +"(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
1.1232 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1233 +term2str t;
1.1234 +if (term2str t) =
1.1235 +"(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1.1236 +then ()
1.1237 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
1.1238 +
1.1239 +(*SRA Schalk I, p.68 Nr. 423a *)
1.1240 +val t = str2term
1.1241 +"(2*x+3*y)/x + (4*x^^^3 - x*y^^^2 - 3*y^^^3)/(x^^^3 - 2*x^^^2*y+x*y^^^2) - (5*x+6*y)/(x - y)";
1.1242 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1243 +term2str t;
1.1244 +if (term2str t) =
1.1245 +"1"
1.1246 +then ()
1.1247 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
1.1248 +
1.1249 +(*SRA Schalk I, p.68 Nr. 428b *)
1.1250 +val t = str2term
1.1251 +"1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
1.1252 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1253 +term2str t;
1.1254 +if (term2str t) =
1.1255 +"4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1.1256 +then ()
1.1257 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
1.1258 +
1.1259 +(*SRA Schalk I, p.68 Nr. 430b *)
1.1260 +val t = str2term
1.1261 +"a^^^2/(a - 3*b) - 108*a*b^^^3/((a+3*b)*(a^^^2 - 9*b^^^2)) - 9*b^^^2*(a - 3*b)/(a+3*b)^^^2";
1.1262 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1263 +term2str t;
1.1264 +if (term2str t) =
1.1265 +"a + 3 * b"
1.1266 +then ()
1.1267 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
1.1268 +
1.1269 +
1.1270 +(*SRA Schalk I, p.68 Nr. 432 *)
1.1271 +val t = str2term
1.1272 +"(a^^^2+a*b)/(a^^^2 - b^^^2) - (b^^^2 - a*b)/(b^^^2 - a^^^2) + a^^^2*(a - b)/(a^^^3 - a^^^2*b) - 2*a*(a^^^2 - b^^^2)/(a^^^3 - a*b^^^2) - 2*b^^^2/(a^^^2 - b^^^2)";
1.1273 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1274 +term2str t;
1.1275 +if (term2str t) =
1.1276 +"0"
1.1277 +then ()
1.1278 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
1.1279 +
1.1280 +(*Eigenes*)
1.1281 +val t = str2term
1.1282 +"3*a/(a*b) + x/y";
1.1283 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1284 +term2str t;
1.1285 +if (term2str t) =
1.1286 +"(3 * y + b * x) / (b * y)"
1.1287 +then ()
1.1288 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
1.1289 +
1.1290 +
1.1291 +"-------- multiply and cancel ------------------------------------";
1.1292 +"-------- multiply and cancel ------------------------------------";
1.1293 +"-------- multiply and cancel ------------------------------------";
1.1294 +
1.1295 +(*SRM Schalk I, p.68 Nr. 436a *)
1.1296 +val t = str2term
1.1297 +"3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)";
1.1298 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1299 +term2str t;
1.1300 +if (term2str t) =
1.1301 +"(5 * x + -5 * y) / (18 * x + 18 * y)"
1.1302 +then ()
1.1303 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1.1304 +
1.1305 +(*SRM.test Schalk I, p.68 Nr. 436b *)
1.1306 +(*WN060420???MG3 crashes with method 'simplify' in
1.1307 + IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
1.1308 +val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1.1309 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1310 +term2str t;
1.1311 +if (term2str t) =
1.1312 +"5 * a / (a + -1 * b)"
1.1313 +then ()
1.1314 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1.1315 +
1.1316 +(*Schalk I, p.68 Nr. 437a *)
1.1317 +val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1.1318 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1319 +if (term2str t) = "1 / (4 * c + 3 * e)" then ()
1.1320 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.1321 +
1.1322 +"----- S.K. corrected non-termination 060904";
1.1323 +val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1.1324 +val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.1325 +if term2str t' = "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)" then ()
1.1326 +else raise error "rational.sml.sml: S.K.8..corrected 060904-6";
1.1327 +
1.1328 +"----- S.K. corrected non-termination of cancel_p_";
1.1329 +val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.1330 +\(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.1331 +val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1.1332 +if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.1333 +else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
1.1334 +
1.1335 +(**)
1.1336 +
1.1337 +(*Schalk I, p.68 Nr. 437b *)
1.1338 +(* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1.1339 +val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1.1340 +(* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1.1341 + *)
1.1342 +
1.1343 +(*a casual output from above*)
1.1344 +val t = str2term
1.1345 +"(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
1.1346 +(* WN060831 nonterm.SK10
1.1347 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1348 +term2str t;
1.1349 +*)
1.1350 +
1.1351 +(*SRM Schalk I, p.68 Nr. 438a *)
1.1352 +val t = str2term
1.1353 +"x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
1.1354 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1355 +term2str t;
1.1356 +if (term2str t) =
1.1357 +"x ^^^ 2"
1.1358 +then ()
1.1359 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1.1360 +
1.1361 +(*SRM Schalk I, p.68 Nr. 439b *)
1.1362 +val t = str2term
1.1363 +"(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
1.1364 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1365 +term2str t;
1.1366 +if (term2str t) =
1.1367 +"(x + -4 * x ^^^ 3) / 2"
1.1368 +then ()
1.1369 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
1.1370 +
1.1371 +(*SRM Schalk I, p.68 Nr. 440a *)
1.1372 +val t = str2term
1.1373 +"(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
1.1374 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1375 +term2str t;
1.1376 +if (term2str t) =
1.1377 +"(-3 + x) / (2 + x)"
1.1378 +then ()
1.1379 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1.1380 +
1.1381 +"----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
1.1382 +val t = str2term
1.1383 +"(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1.1384 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1385 +if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1.1386 +else raise error "rational.sml.sml: diff.behav. in norm_Rational 27";
1.1387 +
1.1388 +"----- SK12 works since 0707xx";
1.1389 +val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1.1390 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1.1391 +if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1.1392 +else raise error "rational.sml.sml: diff.behav. in norm_Rational 28";
1.1393 +
1.1394 +
1.1395 +"-------- common denominator and multiplication ------------------";
1.1396 +"-------- common denominator and multiplication ------------------";
1.1397 +"-------- common denominator and multiplication ------------------";
1.1398 +
1.1399 +(*----------------------------------------------------------------------*)
1.1400 +(*--------- Gemeinsamer Nenner und Multiplikation von Bruechen ---------*)
1.1401 +(*----------------------------------------------------------------------*)
1.1402 +
1.1403 +
1.1404 +(*SRAM Schalk I, p.69 Nr. 441b *)
1.1405 +val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1.1406 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1407 +term2str t;
1.1408 +if (term2str t) =
1.1409 +"(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1.1410 +then ()
1.1411 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1.1412 +
1.1413 +(*SRAM Schalk I, p.69 Nr. 442b *)
1.1414 +val t = str2term "(15*a^^^2/x^^^3 - 5*b^^^4/x^^^2 + 25*c^^^2/x)*(x^^^3/(5*a*b^^^3*c^^^3)) + 1/c^^^3 * (b*x/a - 3*a/b^^^3)";
1.1415 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1416 +term2str t;
1.1417 +if (term2str t) =
1.1418 +"5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1.1419 +then ()
1.1420 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1.1421 +
1.1422 +(*SRAM Schalk I, p.69 Nr. 443b *)
1.1423 +val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1.1424 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1425 +term2str t;
1.1426 +if (term2str t) =
1.1427 +"(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1.1428 +then ()
1.1429 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1.1430 +
1.1431 +(*SRAM Schalk I, p.69 Nr. 445b *)
1.1432 +val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1.1433 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1434 +term2str t;
1.1435 +if (term2str t) =
1.1436 +"a ^^^ 3 / 27"
1.1437 +then ()
1.1438 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1.1439 +
1.1440 +(*SRAM Schalk I, p.69 Nr. 446b *)
1.1441 +val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1.1442 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1443 +term2str t;
1.1444 +if (term2str t) =
1.1445 +"30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1.1446 +then ()
1.1447 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1.1448 +
1.1449 +(*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1.1450 +val t = str2term
1.1451 +"(2*x^^^2/(3*y)+x/y^^^2)*(4*x^^^4/(9*y^^^2)+x^^^2/y^^^4)*(2*x^^^2/(3*y) - x/y^^^2)";
1.1452 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1453 +term2str t;
1.1454 +if (term2str t) =
1.1455 +"(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1.1456 +then ()
1.1457 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1.1458 +
1.1459 +(*SRAM Schalk I, p.69 Nr. 450a *)
1.1460 +val t = str2term
1.1461 +"(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1.1462 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1463 +term2str t;
1.1464 +if (term2str t) =
1.1465 +"(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1.1466 +then ()
1.1467 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1.1468 +
1.1469 +"-------- double fractions ---------------------------------------";
1.1470 +"-------- double fractions ---------------------------------------";
1.1471 +"-------- double fractions ---------------------------------------";
1.1472 +
1.1473 +(*SRD Schalk I, p.69 Nr. 454b *)
1.1474 +val t = str2term
1.1475 +"((2 - x)/(2*a)) / (2*a/(x - 2))";
1.1476 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1477 +term2str t;
1.1478 +if (term2str t) =
1.1479 +"(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1.1480 +then ()
1.1481 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1.1482 +
1.1483 +(*SRD Schalk I, p.69 Nr. 455a *)
1.1484 +val t = str2term
1.1485 +"(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1.1486 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1487 +term2str t;
1.1488 +if (term2str t) =
1.1489 +"(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1.1490 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1.1491 +
1.1492 +
1.1493 +"----- Schalk I, p.69 Nr. 455b";
1.1494 +val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1.1495 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1496 +if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1.1497 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1.1498 +
1.1499 +"----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1.1500 +val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1.1501 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1502 +if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1.1503 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
1.1504 +
1.1505 +"----- ?: worked before 0707xx";
1.1506 +val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1.1507 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1508 +if term2str t = "-1 / (3 + y)" then ()
1.1509 +else raise error "rational.sml: -1 / (3 + y) norm_Rational";
1.1510 +
1.1511 +(*SRD Schalk I, p.69 Nr. 456b *)
1.1512 +val t = str2term
1.1513 +"(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1.1514 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1515 +term2str t;
1.1516 +if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1.1517 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1.1518 +
1.1519 +(*SRD Schalk I, p.69 Nr. 457b *)
1.1520 +val t = str2term
1.1521 +"(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1.1522 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1523 +term2str t;
1.1524 +if (term2str t) =
1.1525 +"8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1.1526 +then ()
1.1527 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1.1528 +
1.1529 +"----- Schalk I, p.69 Nr. 458b works since 0707";
1.1530 +val t = str2term
1.1531 +"(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1.1532 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1533 +if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
1.1534 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
1.1535 +
1.1536 +(*SRD Schalk I, p.69 Nr. 459b *)
1.1537 +val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1.1538 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1539 +if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
1.1540 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1.1541 +
1.1542 +
1.1543 +(*Schalk I, p.69 Nr. 460b nonterm.SK
1.1544 +val t = str2term
1.1545 +"(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1.1546 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1547 +if term2str t =
1.1548 +then ()
1.1549 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1.1550 +
1.1551 +val t = str2term
1.1552 +"9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1.1553 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.1554 +... non terminating.
1.1555 +val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1.1556 +"(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)";
1.1557 +val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1.1558 +... non terminating.*)
1.1559 +
1.1560 +(*SRD Schalk I, p.70 Nr. 472a *)
1.1561 +val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1.1562 + \((4*x - 8*y)/(x + y))";
1.1563 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1564 +term2str t;
1.1565 +if (term2str t) =
1.1566 +"x + y"
1.1567 +then ()
1.1568 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1.1569 +
1.1570 +
1.1571 +(*----------------------------------------------------------------------*)
1.1572 +(*---------------------- Einfache Dppelbrche --------------------------*)
1.1573 +(*----------------------------------------------------------------------*)
1.1574 +
1.1575 +(*SRD Schalk I, p.69 Nr. 461a *)
1.1576 +val t = str2term
1.1577 +"(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1.1578 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1579 +term2str t;
1.1580 +if (term2str t) =
1.1581 +"1 / 2"
1.1582 +then ()
1.1583 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1.1584 +
1.1585 +(*SRD Schalk I, p.69 Nr. 464b *)
1.1586 +val t = str2term
1.1587 +"(a - a/(a - 2)) / (a + a/(a - 2))";
1.1588 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1589 +term2str t;
1.1590 +if (term2str t) =
1.1591 +"(3 + -1 * a) / (1 + -1 * a)"
1.1592 +then ()
1.1593 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1.1594 +
1.1595 +(*SRD Schalk I, p.69 Nr. 465b *)
1.1596 +val t = str2term
1.1597 +"((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1.1598 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1599 +term2str t;
1.1600 +if (term2str t) =
1.1601 +"(4 * x + 6 * y + -9 * z) / (4 * x)"
1.1602 +then ()
1.1603 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1.1604 +
1.1605 +(*SRD Schalk I, p.69 Nr. 466b *)
1.1606 +val t = str2term
1.1607 +"((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1.1608 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1609 +term2str t;
1.1610 +if (term2str t) =
1.1611 +"(25 + -10 * x + x ^^^ 2) / 18"
1.1612 +then ()
1.1613 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1.1614 +
1.1615 +(*SRD Schalk I, p.70 Nr. 469 *)
1.1616 +val t = str2term
1.1617 +"3*b^^^2/(4*a^^^2 - 8*a*b + 4*b^^^2)/(a/(a^^^2*b - b^^^3) + (a - b)/(4*a*b^^^2+4*b^^^3) - 1/(4*b^^^2))";
1.1618 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1619 +term2str t;
1.1620 +if (term2str t) =
1.1621 +"3 * b ^^^ 3 / (2 * a + -2 * b)"
1.1622 +then ()
1.1623 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1.1624 +
1.1625 +(*----------------------------------------------------------------------*)
1.1626 +(*---------------------- Mehrfache Dppelbrueche ------------------------*)
1.1627 +(*----------------------------------------------------------------------*)
1.1628 +
1.1629 +(*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1.1630 +(*WN060419 crashes with method 'simplify' ????SK*)
1.1631 +val t = str2term
1.1632 +"((a^^^2 - b^^^2)/(2*a*b)+2*a*b/(a^^^2 - b^^^2))/((a^^^2+b^^^2)/(2*a*b)+1) / ((a^^^2+b^^^2)^^^2/(a+b)^^^2)";
1.1633 +val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1.1634 +if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
1.1635 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1.1636 +
1.1637 +"----- Schalk I, p.70 Nr. 477a";
1.1638 +(* MG Achtung: terme explodieren; Bsp zu komplex;
1.1639 + L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1.1640 +val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
1.1641 + \(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1.1642 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.1643 +
1.1644 +
1.1645 +val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / \
1.1646 + \((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
1.1647 +val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1.1648 +????SK ???MG*)
1.1649 +
1.1650 +
1.1651 +"----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
1.1652 +val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
1.1653 + \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1.1654 +val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1655 +if term2str t' =
1.1656 +"(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1.1657 +then ()
1.1658 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1.1659 +
1.1660 +(* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
1.1661 +if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /\n(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) *\n (a + -1 * b))" then ()
1.1662 +else raise error "rational.sml: works again";
1.1663 +re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
1.1664 +
1.1665 +
1.1666 +
1.1667 +(*Schalk I, p.70 Nr. 480a *)
1.1668 +(* Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831 nonterm.SK00
1.1669 +val t = str2term
1.1670 +"(1/x+1/y+1/z)/(1/x - 1/y - 1/z) / (2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z)))";
1.1671 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1672 +term2str t;
1.1673 +if (term2str t) =
1.1674 +
1.1675 +then ()
1.1676 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1.1677 +
1.1678 +(*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
1.1679 +val t = str2term
1.1680 +"(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
1.1681 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1682 +term2str t;
1.1683 +"(x ^^^ 2 * y ^^^ 2 * z + x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2) /
1.1684 +(-1 * x ^^^ 2 * y ^^^ 2 * z + -1 * x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2)";
1.1685 +val t = str2term
1.1686 +"2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z))";
1.1687 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1688 +term2str t;
1.1689 +"1"
1.1690 +
1.1691 +(* SK 1. Ausdruck kann nicht weiter gekrzt werden; cancel_p !!!*)
1.1692 +### rls: cancel_p on:
1.1693 +(x ^^^ 2 * (y ^^^ 2 * z) + x ^^^ 2 * (y * z ^^^ 2) + x * (y ^^^ 2 * z ^^^ 2)) /
1.1694 +(-1 * (x ^^^ 2 * (y ^^^ 2 * z)) + -1 * (x ^^^ 2 * (y * z ^^^ 2)) + x * (y ^^^ 2 * z ^^^ 2))
1.1695 +GC #3.61.81.101.197.17503: (0 ms)
1.1696 +*** RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction
1.1697 +
1.1698 +val t = str2term
1.1699 +"(x^^^2 * (y^^^2 * z) + x^^^2 * (y * z^^^2) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y^^^2 * z)) + -1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1.1700 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1701 +term2str t;
1.1702 +(*uncaught exception nonexhaustive binding failure*)
1.1703 +
1.1704 +(* Das kann er aber krzen !!????: *)
1.1705 +val t = str2term
1.1706 +"(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1.1707 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1708 +term2str t;
1.1709 +"(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1.1710 +*)
1.1711 +
1.1712 +
1.1713 +
1.1714 +
1.1715 +
1.1716 +
1.1717 +(*--------------------------------------------------------------------*)
1.1718 +(*----------------------- Problem-Beispiele --------------------------*)
1.1719 +(*--------------------------------------------------------------------*)
1.1720 +
1.1721 +(*Schalk I, p.60 Nr. 215d *)
1.1722 +(* Achtung: rechnet ewig ...
1.1723 +val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1.1724 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1725 +term2str t; noterm.SK
1.1726 +*)
1.1727 +
1.1728 +(* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
1.1729 +(*
1.1730 +val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1.1731 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1732 +term2str t;
1.1733 +"a^^^3 * x^^^4 + 4 * a^^^3 * x^^^3 * y +\n6 * a^^^3 * x^^^2 * y^^^2 +\n4 * a^^^3 * x * y^^^3 +\na^^^3 * y^^^4 +\n-3 * a^^^2 * b * x^^^4 +\n-12 * a^^^2 * b * x^^^3 * y +\n-18 * a^^^2 * b * x^^^2 * y^^^2 +\n-12 * a^^^2 * b * x * y^^^3 +\n-3 * a^^^2 * b * y^^^4 +\n3 * a * b^^^2 * x^^^4 +\n12 * a * b^^^2 * x^^^3 * y +\n18 * a * b^^^2 * x^^^2 * y^^^2 +\n12 * a * b^^^2 * x * y^^^3 +\n3 * a * b^^^2 * y^^^4 +\n-1 * b^^^3 * x^^^4 +\n-4 * b^^^3 * x^^^3 * y +\n-6 * b^^^3 * x^^^2 * y^^^2 +\n-4 * b^^^3 * x * y^^^3 +\n-1 * b^^^3 * y^^^4";
1.1734 +val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
1.1735 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1736 +term2str t;
1.1737 +"a^^^5 * x^^^2 + 2 * a^^^5 * x * y + a^^^5 * y^^^2 +\n-5 * a^^^4 * b * x^^^2 +\n-10 * a^^^4 * b * x * y +\n-5 * a^^^4 * b * y^^^2 +\n10 * a^^^3 * b^^^2 * x^^^2 +\n20 * a^^^3 * b^^^2 * x * y +\n10 * a^^^3 * b^^^2 * y^^^2 +\n-10 * a^^^2 * b^^^3 * x^^^2 +\n-20 * a^^^2 * b^^^3 * x * y +\n-10 * a^^^2 * b^^^3 * y^^^2 +\n5 * a * b^^^4 * x^^^2 +\n10 * a * b^^^4 * x * y +\n5 * a * b^^^4 * y^^^2 +\n-1 * b^^^5 * x^^^2 +\n-2 * b^^^5 * x * y +\n-1 * b^^^5 * y^^^2";
1.1738 +*)
1.1739 +(*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1.1740 +
1.1741 +(*--------------------------------------------------------------------*)
1.1742 +(*Schalk I, p.70 Nr. 480b
1.1743 +val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1.1744 + \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1.1745 + \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1.1746 + \(20*x*y/(x^^^2 - 25*y^^^2))";
1.1747 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1748 +SK.nonterm
1.1749 +Kann nicht weiter vereinfacht werden !!!!?? *)
1.1750 +
1.1751 +(*--------------------------------------------------------------------*)
1.1752 +"---- MGs test set";
1.1753 +val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
1.1754 +val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
1.1755 +if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
1.1756 +else raise error "";
1.1757 +
1.1758 +(*--------------------------------------------------------------------*)
1.1759 +(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
1.1760 + ---> Sortierung FALSCH !! *)
1.1761 +val t = str2term "b^^^3 * a^^^5/a ";
1.1762 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1763 +term2str t;
1.1764 +"1 * (a^^^4 * b^^^3) / 1"; (*OK*)
1.1765 +
1.1766 +val t = str2term "b^^^3 * a^^^5/b ";
1.1767 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1768 +term2str t;
1.1769 +"1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
1.1770 +
1.1771 +(* Problem liegt NICHT bei ord_make_polynomial! (siehe folgende Bsple) *)
1.1772 +(*
1.1773 +val x = str2term "x"; val bdv = str2term "bdv";
1.1774 +val t1 = str2term "b^^^2 * a^^^5";
1.1775 +val t2 = str2term "a^^^5 * b^^^2 ";
1.1776 +ord_make_polynomial false Rational.thy [(x,bdv)] (t1,t2); (*false*)
1.1777 +*)
1.1778 +(* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
1.1779 +
1.1780 +(*--------------------------------------------------------------------*)
1.1781 +(* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
1.1782 + ---> erzeugt berflssige "1 * ..."
1.1783 +
1.1784 +val t = str2term "-1 / (3 + y)";
1.1785 +(*~~ *)
1.1786 +val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1.1787 +term2str t;
1.1788 +"-1 / (3 + 1 * y)";
1.1789 +(********* Das ist das PROBLEM !!!!!!!??? *******************)
1.1790 +(* -1 im Z???ler der Angabe verursacht das Problem !*)
1.1791 +*)
1.1792 +
1.1793 +(* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1.1794 +"----- MGs test set";
1.1795 +val t = str2term "(a^^^2 + -1)/(a+1)";
1.1796 +val SOME (t',_) = rewrite_set_ thy false cancel_p t;
1.1797 +if term2str t' = "(-1 + a) / 1" then ()
1.1798 +else raise error "rational.sml MG tests 3d";
1.1799 +
1.1800 +"----- NOT TERMINATING ?: worked before 0707xx";
1.1801 +val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1.1802 +val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
1.1803 +if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
1.1804 +else raise error "rational.sml MG tests 3e";
1.1805 +
1.1806 +"----- corrected SK060905";
1.1807 +val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1.1808 +val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1809 +if term2str t' = "-1 / (5 + -2 * x)" then ()
1.1810 +else raise error "rational.sml corrected SK060905";
1.1811 +
1.1812 +
1.1813 +"--------------------------------------------------------------------";
1.1814 +"----------------------- Muster-Beispiele fuer DA -------------------";
1.1815 +"--------------------------------------------------------------------";
1.1816 +
1.1817 +(*SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1.1818 +val t = str2term
1.1819 +"(15*a^^^4/(a*x^^^3) - 5*a*((b^^^4 - 5*c^^^2*x)/x^^^2))*(x^^^3/(5*a*b^^^3*c^^^3)) + a/c^^^3 * (x*(b/a) - 3*b*(a/b^^^4))";
1.1820 +val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1.1821 +term2str t;
1.1822 +if (term2str t) =
1.1823 +"5 * x ^^^ 2 / (b ^^^ 3 * c)"
1.1824 +then ()
1.1825 +else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
1.1826 +
1.1827 +"-------- me Schalk I No.186 -------------------------------------";
1.1828 +"-------- me Schalk I No.186 -------------------------------------";
1.1829 +"-------- me Schalk I No.186 -------------------------------------";
1.1830 +val fmz = ["term ((14 * x * y) / ( x * y ))",
1.1831 + "normalform N"];
1.1832 +val (dI',pI',mI') =
1.1833 + ("Rational.thy",["rational","simplification"],
1.1834 + ["simplification","of_rationals"]);
1.1835 +val p = e_pos'; val c = [];
1.1836 +val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1.1837 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1838 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1839 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1840 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1841 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1842 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1843 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
1.1844 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.1845 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1.1846 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1.1847 +val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1.1848 +case (f2str f, nxt) of
1.1849 + ("14", ("End_Proof'", _)) => ()
1.1850 + | _ => raise error "rational.sml diff.behav. in me Schalk I No.186";
1.1851 +
1.1852 +
1.1853 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1.1854 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1.1855 +"-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1.1856 +states:=[];
1.1857 +CalcTree
1.1858 +[(["term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1.1859 + ("Rational.thy",["rational","simplification"],
1.1860 + ["simplification","of_rationals"]))];
1.1861 +Iterator 1;
1.1862 +moveActiveRoot 1;
1.1863 +autoCalculate 1 CompleteCalc;
1.1864 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1865 +
1.1866 +interSteps 1 ([1],Res);
1.1867 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1868 +
1.1869 +
1.1870 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1.1871 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1.1872 +"-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1.1873 +states:=[];
1.1874 +CalcTree
1.1875 +[(["term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1.1876 + ("Rational.thy",["rational","simplification"],
1.1877 + ["simplification","of_rationals"]))];
1.1878 +Iterator 1;
1.1879 +moveActiveRoot 1;
1.1880 +autoCalculate 1 CompleteCalc;
1.1881 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1882 +(*with explicit script done already... and removed [1,..] at below...
1.1883 +interSteps 1 ([1],Res);
1.1884 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1885 +*)
1.1886 +interSteps 1 ([2],Res);
1.1887 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1888 +
1.1889 +interSteps 1 ([2,1],Res);
1.1890 +val ((pt,p),_) = get_calc 1; show_pt pt;
1.1891 +val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1.1892 +(*if length newnds = 12 then () WN060905*)
1.1893 +if length newnds = 13 then ()
1.1894 +else raise error "rational.sml: interSteps cancel_p rev_rew_p";
1.1895 +
1.1896 +val p = ([2,1,9],Res);
1.1897 +getTactic 1 p;
1.1898 +val (_, tac, _) = pt_extract (pt, p);
1.1899 +(*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
1.1900 +WN060905*)
1.1901 +case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
1.1902 +| _ => raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
1.1903 +
1.1904 +
1.1905 +"-------- investigate rulesets for cancel_p ----------------------";
1.1906 +"-------- investigate rulesets for cancel_p ----------------------";
1.1907 +"-------- investigate rulesets for cancel_p ----------------------";
1.1908 +val thy = Rational.thy;
1.1909 +"---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1.1910 +val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1.1911 +val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
1.1912 +"----- with rewrite_set_";
1.1913 +val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1.1914 +term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*);
1.1915 +val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
1.1916 +val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1.1917 +term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
1.1918 +
1.1919 +"----- with make_deriv";
1.1920 +val SOME (tt, _) = factout_p_ Isac.thy t; term2str tt =
1.1921 +"(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
1.1922 +(*
1.1923 +"--- with ruleset as before 060829";
1.1924 +val {rules, rew_ord=(_,ro),...} =
1.1925 + rep_rls (assoc_rls "make_polynomial");
1.1926 +val der = make_deriv thy Atools_erls rules ro NONE tt;
1.1927 +print_depth 99; map (term2str o #1) der; print_depth 3;
1.1928 +print_depth 99; map (rule2str o #2) der; print_depth 3;
1.1929 +... did not terminate"*)
1.1930 +"--- with simpler ruleset";
1.1931 +val {rules, rew_ord=(_,ro),...} =
1.1932 + rep_rls (assoc_rls "rev_rew_p");
1.1933 +val der = make_deriv thy Atools_erls rules ro NONE tt;
1.1934 +print_depth 99; writeln (deriv2str der); print_depth 3;
1.1935 +
1.1936 +print_depth 99; map (term2str o #1) der; print_depth 3;
1.1937 +"...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
1.1938 +print_depth 99; map (rule2str o #2) der; print_depth 3;
1.1939 +print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
1.1940 +
1.1941 +val der = make_deriv thy Atools_erls rules ro NONE
1.1942 + (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1.1943 +print_depth 99; writeln (deriv2str der); print_depth 3;
1.1944 +
1.1945 +val {rules, rew_ord=(_,ro),...} =
1.1946 + rep_rls (assoc_rls "rev_rew_p");
1.1947 +val der = make_deriv thy Atools_erls rules ro NONE
1.1948 + (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1.1949 +print_depth 99; writeln (deriv2str der); print_depth 3;
1.1950 +print_depth 99; map (term2str o #1) der; print_depth 3;
1.1951 +(*WN060829 ...postponed*)
1.1952 +
1.1953 +
1.1954 +"-------- investigate format of factout_ and factout_p_ ----------";
1.1955 +"-------- investigate format of factout_ and factout_p_ ----------";
1.1956 +"-------- investigate format of factout_ and factout_p_ ----------";
1.1957 +val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
1.1958 +val (thy, eval_rls) = (Rational.thy, Atools_erls)(*see 'fun init_state'*);
1.1959 +val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
1.1960 +
1.1961 +"----- see Rational.ML, local cancel_p, fun init_state";
1.1962 +val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
1.1963 +val SOME (t',_) = factout_p_ thy t; term2str t';
1.1964 +(*
1.1965 +val rtas = reverse_deriv thy eval_rls rules ro NONE t';
1.1966 +writeln(trtas2str rst);
1.1967 +*)
1.1968 +
1.1969 +
1.1970 +"----- see Rational.ML, local cancel_p, fun init_state";
1.1971 +val t = str2term "a^^^2 / a";
1.1972 +val SOME (t',_) = factout_p_ thy t;
1.1973 +term2str t' = "a * a / (1 * a)" (*true*);
1.1974 +(*... can be canceled with
1.1975 +real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
1.1976 +(* sml/ME/rewtools.sml:
1.1977 +val rtas = reverse_deriv thy Atools_erls rules ro NONE t';
1.1978 +writeln (deri2str rtas);
1.1979 +*)
1.1980 +
1.1981 +
1.1982 +
1.1983 +"-------- SK 060904 ----------------------------------------------";
1.1984 +"-------- SK 060904 ----------------------------------------------";
1.1985 +"-------- SK 060904 ----------------------------------------------";
1.1986 +"----- order on polynomials -- input + output";
1.1987 +val thy = Isac.thy;
1.1988 +val t = str2term "(a + -1 * b) / (-1 * a + b)";
1.1989 +val SOME (t', _) = factout_p_ thy t; term2str t';
1.1990 +val SOME (t', _) = cancel_p_ thy t; term2str t';
1.1991 +
1.1992 +val t = str2term "a*b*c*d / (d*e*f*g)";
1.1993 +val SOME (t', _) = cancel_p_ thy t; term2str t';
1.1994 +
1.1995 +val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
1.1996 +val SOME (t', _) = cancel_p_ thy t; term2str t';
1.1997 +(*???order.SK ???*)
1.1998 +
1.1999 +"----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
1.2000 +val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
1.2001 +val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1.2002 +if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
1.2003 +else raise error "rational.sml SK060904-1a worked since 0707xx";
1.2004 +
1.2005 +"----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
1.2006 +val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1.2007 +\(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1.2008 +val SOME (t',_) = cancel_p_ thy t;
1.2009 +if term2str t' = "1 / (4 * c + 3 * e)" then ()
1.2010 +else raise error "rational.sml SK060904-1b";
1.2011 +
1.2012 +
1.2013 +"----- SK060904-2a non-termination of add_fraction_p_";
1.2014 +val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \
1.2015 + \ (-1 * a + b * x) / (a + b * x) ";
1.2016 +(* nonterm.SK
1.2017 +val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
1.2018 +
1.2019 +common_nominator_p_ thy t;
1.2020 +" (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \
1.2021 +\ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
1.2022 +
1.2023 +add_fraction_p_ thy t;
1.2024 +" ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /\
1.2025 +\ ((a + b * x)*(-1 * a + b * x)) ";
1.2026 +*)
1.2027 \ No newline at end of file