1.1 --- a/test/Tools/isac/Knowledge/rational.sml Mon Aug 26 15:37:48 2013 +0200
1.2 +++ b/test/Tools/isac/Knowledge/rational.sml Mon Aug 26 16:32:21 2013 +0200
1.3 @@ -14,18 +14,17 @@
1.4 WN060104 transfer examples marked with (*SR..*) to the exp-collection
1.5 *)
1.6
1.7 -(*========== inhibit exn WN130824 TODO =======================================================
1.8 -"--------------------------------------------------------";
1.9 -"--------------------------------------------------------";
1.10 -"table of contents --------------------------------------";
1.11 -"--------------------------------------------------------";
1.12 -"~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~";
1.13 -"-------- ... missing WN060103 --------------------------";
1.14 -"-------- fun monom2term, fun poly2term' ---------------";
1.15 -"~~~~~END: decomment structure RationalI : RATIONALI ~~~~";
1.16 +"-----------------------------------------------------------------------------";
1.17 +"-----------------------------------------------------------------------------";
1.18 +"table of contents -----------------------------------------------------------";
1.19 +"-----------------------------------------------------------------------------";
1.20 "-------- fun poly_of_term ---------------------------------------------------";
1.21 "-------- fun is_poly --------------------------------------------------------";
1.22 "-------- fun term_of_poly ---------------------------------------------------";
1.23 +"-------- fun factout_p_ -----------------------------------------------------";
1.24 +"-------- fun common_nominator_p_ --------------------------------------------";
1.25 +"-------- fun add_fraction_p_ ------------------------------------------------";
1.26 +"-------- TODO ---------------------------------------------------------------";
1.27 "-------- and app_rev --------------------------------------------------------";
1.28 "-------- external calculating functions test -----------";
1.29 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag";
1.30 @@ -55,262 +54,6 @@
1.31 "--------------------------------------------------------";
1.32
1.33
1.34 -"~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~";
1.35 -(*.~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.36 - tests of internal functions: to make them work,
1.37 - out-comment (*!!!*) in knowledge/Rational.ML:
1.38 -(*##!!!
1.39 -structure RationalI : RATIONALI =
1.40 -struct
1.41 -!!!##*)
1.42 -
1.43 -(*##!!!
1.44 -end;(*struct*)
1.45 -open RationalI;
1.46 -!!!##*)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~.*)
1.47 -
1.48 -"-------- ... missing WN060103 --------------------------";
1.49 -"-------- ... missing WN060103 --------------------------";
1.50 -"-------- ... missing WN060103 --------------------------";
1.51 -(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
1.52 -writeln ("********************* rational.sml - TESTS *************************");
1.53 -writeln ("***** divide tests *****");
1.54 -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.55 -(* result: [(1,[0,0,1]),(1,[0,0,0])] *)
1.56 -if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else error ("rational.sml: example failed");
1.57 -
1.58 -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.59 -(* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
1.60 -if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else error ("rational.sml: example failed");
1.61 -
1.62 -val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.63 -(* result: [(4,[1]),(4,[0])] *)
1.64 -if mv_pquot2=[(4,[1]),(4,[0])] then () else error ("rational.sml: example failed");
1.65 -
1.66 -val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
1.67 -(* result: [(12,[0]] *)
1.68 -if mv_prest2=[(12,[0])] then () else error ("rational.sml: example failed");
1.69 -
1.70 -val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
1.71 -(* [(2,[1]),(~2,[0])] *)
1.72 -if mv_pquot3=[(2,[1]),(~2,[0])] then () else error ("rational.sml: example failed");
1.73 -
1.74 -val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
1.75 -(* [(1,[2]),(~1,[0])] *)
1.76 -if mv_prest3=[(1,[2]),(~1,[0])] then () else error ("rational.sml: example failed");
1.77 -
1.78 -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.79 -(* [(1,[0,1,1])] *)
1.80 -if mv_pquot4=[(1,[0,1,1])] then () else error ("rational.sml: example failed");
1.81 -
1.82 -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.83 -(* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
1.84 -if mv_prest4 =[(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
1.85 -
1.86 -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.87 -(* [(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.88 -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 error ("rational.sml: example failed");
1.89 -
1.90 -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.91 -(* [] *)
1.92 -if mv_prest5=[] then () else error ("rational.sml: example failed");
1.93 -
1.94 -(* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
1.95 -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.96 -if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else error ("rational.sml: example failed");
1.97 -
1.98 -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.99 -if mv_prest6=[] then () else error ("rational.sml: example failed");
1.100 -
1.101 -
1.102 -writeln ("***** MV_CONTENT-TESTS *****");
1.103 -val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.104 -(* [(1,[0,1]),(1,[0,0])] *)
1.105 -if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else error ("rational.sml: example failed");
1.106 -
1.107 -val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
1.108 -(*[(1,[1,0]),(1,[0,0])]*)
1.109 -if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else error ("rational.sml: example failed");
1.110 -
1.111 -val mv_cont2=mv_content([(2,[1]),(4,[0])]);
1.112 -(* [(2,[0])] *)
1.113 -if mv_cont2=[(2,[0])] then () else error ("rational.sml: example failed");
1.114 -
1.115 -val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
1.116 -(* [(1,[1]),(2,[0])] *)
1.117 -if mv_pp2=[(1,[1]),(2,[0])] then () else error ("rational.sml: example failed");
1.118 -
1.119 -val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.120 -(* [(2,[0,0,0])] *)
1.121 -if mv_cont3=[(2,[0,0,0])] then () else error ("rational.sml: example failed");
1.122 -
1.123 -val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
1.124 -(* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
1.125 -if mv_pp3=[(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] then () else error ("rational.sml: example failed");
1.126 -
1.127 -val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.128 -(* [(1,[0,0,0])] *)
1.129 -if mv_cont4=[(1,[0,0,0])] then () else error ("rational.sml: example failed");
1.130 -
1.131 -val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
1.132 -(* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
1.133 -if mv_pp4=[(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
1.134 -
1.135 -val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.136 -(* [(3,[0,0])] *)
1.137 -if con1=[(3,[0,0])] then () else error ("rational.sml: example failed");
1.138 -
1.139 -val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
1.140 -(* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
1.141 -if pp1=[(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] then () else error ("rational.sml: example failed");
1.142 -
1.143 -val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.144 -(* [(1,[0,0])] *)
1.145 -if con2=[(1,[0,0])] then () else error ("rational.sml: example failed");
1.146 -
1.147 -val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
1.148 -(* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
1.149 -if pp2=[(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] then () else error ("rational.sml: example failed");
1.150 -
1.151 -val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
1.152 -(* [(3,[0,1,0])] *)
1.153 -if cont1=[(3,[0,1,0])] then () else error ("rational.sml: example failed");
1.154 -
1.155 -val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
1.156 -(* [(1,[2,0,0])] *)
1.157 -if pp1=[(1,[2,0,0])] then () else error ("rational.sml: example failed");
1.158 -
1.159 -val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
1.160 -(* [(2,[0,1,0])] *)
1.161 -if cont2=[(2,[0,1,0])] then () else error ("rational.sml: example failed");
1.162 -
1.163 -val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
1.164 -(* [(1,[2,0,0]),(2,[1,1,0])] *)
1.165 -if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else error ("rational.sml: example failed");
1.166 -
1.167 -writeln ("********************************************************");
1.168 -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.169 -if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else error ("rational.sml: example failed");
1.170 -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.171 -
1.172 -
1.173 -"-------- fun monom2term, fun poly2term' ---------------";
1.174 -"-------- fun monom2term, fun poly2term' ---------------";
1.175 -"-------- fun monom2term, fun poly2term' ---------------";
1.176 -val t = monom2term ((3,[2,1,0]), ["c","b","a"](*reverse ???SK-*));
1.177 -term2str t = "3 * (c ^^^ 2 * b)" (*true*);
1.178 -
1.179 -val t = monom2term ((1,[1,0]), ["b","a"]);
1.180 -term2str t = "b" (*true*);
1.181 -
1.182 -val t = poly2term ([(1,[0,0,0]),(2,[1,0,0]),(3,[2,1,0]),(4,[3,2,1])],
1.183 - ["c","b","a"]);
1.184 -term2str t = "1 + 2 * c + 3 * (c ^^^ 2 * b) + 4 * (c ^^^ 3 * (b ^^^ 2 * a))";
1.185 -
1.186 -val t = poly2term ([(1,[1,0]),(1,[0,1])], ["b","a"]);
1.187 -term2str t = "a + b" (*true*);
1.188 -
1.189 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
1.190 -"~~~~~END: decomment structure RationalI : RATIONALI ~~~~";
1.191 -"~~~~~END: decomment structure RationalI : RATIONALI ~~~~";
1.192 -"~~~~~END: decomment structure RationalI : RATIONALI ~~~~";
1.193 -
1.194 -
1.195 -fun parse_rat str = (term_of o the o (parse thy)) str;
1.196 -
1.197 -writeln ("***** mv_gcd-tests *****");
1.198 -val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
1.199 -(* [(2,[1,1]),(2,[0,0])] *)
1.200 -if ggt1=[(2,[1,1]),(2,[0,0])] then () else error ("rational.sml: example failed");
1.201 -
1.202 -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.203 -(* [(2,[1,1,0]),(3,[0,0,1])] *)
1.204 -if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else error ("rational.sml: example failed");
1.205 -
1.206 -
1.207 -val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.208 -(* [(1,[1,0]),(~1,[0,1])] *)
1.209 -if ggt3=[(1,[1,0]),(~1,[0,1])] then () else error ("rational.sml: example failed");
1.210 -
1.211 -
1.212 -val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
1.213 -(* [(1,[1,0,0])] *)
1.214 -if ggt4=[(1,[1,0,0])] then () else error ("rational.sml: example failed");
1.215 -
1.216 -
1.217 -val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.218 -(* [(1,[1,0]),(~1,[0,1])] *)
1.219 -if ggt5=[(1,[1,0]),(~1,[0,1])] then () else error ("rational.sml: example failed");
1.220 -
1.221 -
1.222 -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.223 -(* [(1,[0,0,0])] *)
1.224 -if ggt6=[(1,[1,0,0])] then () else error ("rational.sml: example failed");
1.225 -
1.226 -writeln ("***** kgv-tests *****");
1.227 -val kgv1=mv_lcm [(10,[])] [(15,[])];
1.228 -(* [(30,[])] *)
1.229 -if kgv1=[(30,[])] then () else error ("rational.sml: example failed");
1.230 -
1.231 -val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
1.232 -(* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
1.233 -if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else error ("rational.sml: example failed");
1.234 -
1.235 -val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
1.236 -(* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
1.237 -if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else error ("rational.sml: example failed");
1.238 -
1.239 -(*!!!--------
1.240 -writeln ("***** STEP_CANCEL_TESTS: *****");
1.241 -
1.242 -val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) / (6 * a * c)";
1.243 -val div2 = term2str (step_cancel term2);
1.244 -if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else error ("rational.sml: example failed");
1.245 -
1.246 -
1.247 -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.248 -val div1 = term2str(step_cancel term1);
1.249 -if div1 = "(3 * c + 14 * b + 20 * (b ^^^ 2 * c) + 10 * (a * (b * c))) * a / (1 * a)" then () else error ("rational.sml: example failed");
1.250 -
1.251 -val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
1.252 -val div3 = term2str(step_cancel term3);
1.253 -if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else error ("rational.sml: example failed");
1.254 -
1.255 ---------------------------------------------------------------------------!!!*)
1.256 -
1.257 -(*-----versuche 13.3.03-----
1.258 - val t = str2term "1 - x^^^2 - 5 * x^^^5";
1.259 - val vs=(((map free2str) o vars) t);
1.260 - val SOME ml = expanded2poly t vs;
1.261 - poly2term (ml, vs);
1.262 - poly2term'(rev(sort (mv_geq LEX_) (ml)),vs);
1.263 - poly2term'([(~5,[5]),(~1,[2]),(1,[0])], vs);
1.264 - monom2term((~5,[5]),vs);
1.265 - monom2term((~1,[2]),vs);
1.266 - val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
1.267 -
1.268 - val (i,is) = (~1,[2]);
1.269 - val ttt = Const ("Groups.times_class.times", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
1.270 - (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
1.271 - Free ((str_of_int o abs) i, HOLogic.realT)) $
1.272 - powerproduct2term(is, vs);
1.273 - term2str ttt;
1.274 --------versuche 13.3.03-----*)
1.275 -
1.276 - val t = str2term "1 - x^^^2 - 5 * x^^^5";
1.277 - val SOME t' = expanded2polynomial t; term2str t';
1.278 -"1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5";
1.279 - val t = str2term "1 - x";
1.280 - val SOME t' = expanded2polynomial t; term2str t';
1.281 -"1 + - 1 * x";
1.282 - val t = str2term "1 + (-1) * x";
1.283 - val SOME t' = expanded2polynomial t; term2str t';
1.284 -"1 + - 1 * x";
1.285 - val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5";
1.286 - val SOME t' = polynomial2expanded t; term2str t';
1.287 -"1 - x ^^^ 2 - 5 * x ^^^ 5";
1.288 -============ inhibit exn WN130824 TODO ======================================================*)
1.289 -
1.290 "-------- fun poly_of_term ---------------------------------------------------";
1.291 "-------- fun poly_of_term ---------------------------------------------------";
1.292 "-------- fun poly_of_term ---------------------------------------------------";
1.293 @@ -363,6 +106,77 @@
1.294 if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
1.295 then () else error "term_of_poly 1 changed";
1.296
1.297 +"-------- fun factout_p_ -----------------------------------------------------";
1.298 +"-------- fun factout_p_ -----------------------------------------------------";
1.299 +"-------- fun factout_p_ -----------------------------------------------------";
1.300 +val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
1.301 +val SOME (t', asm) = factout_p_ thy t;
1.302 +if term2str t' = "(x + y) * (x + -1 * y) / (x * (x + -1 * y))"
1.303 +then () else error ("factout_p_ term 1 changed: " ^ term2str t')
1.304 +;
1.305 +(*========== inhibit exn WN130822 asm different by Rational.thy | Rational2.thy ================
1.306 +if terms2str asm = "[\"x\",\"x + -1 * y\"]"
1.307 +then () else error "factout_p_ asm 1 changed"
1.308 +============ inhibit exn WN130822 asm different by Rational.thy | Rational2.thy ===============*)
1.309 +;
1.310 +val t = str2term "nothing + to_cancel ::real";
1.311 +if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable";
1.312 +
1.313 +"-------- fun common_nominator_p_ --------------------------------------------";
1.314 +"-------- fun common_nominator_p_ --------------------------------------------";
1.315 +"-------- fun common_nominator_p_ --------------------------------------------";
1.316 +val t = str2term ("y / (a*x + b*x + c*x) " ^
1.317 + (* n1 d1 *)
1.318 + "+ a / (x*y)");
1.319 + (* n2 d2 *)
1.320 +val SOME (t', asm) = common_nominator_p_ thy t;
1.321 +if term2str t' =
1.322 + ("y * y / (x * ((a + b + c) * y)) " ^
1.323 + (* n1 *d2'/ (c'* ( d1' *d2')) *)
1.324 + "+ a * (a + b + c) / (x * ((a + b + c) * y))")
1.325 + (* n2 * d1' / (c'* ( d1' *d2')) *)
1.326 +then () else error "common_nominator_p_ term 1 changed";
1.327 +(*========== inhibit exn WN130823 asm different Rational<-->2.thy ==============================
1.328 +if terms2str asm = "[\"a + b + c\",\"y\",\"x\"]"
1.329 +then () else error "common_nominator_p_ asm 1 changed"
1.330 +============ inhibit exn WN130823 asm different Rational<-->2.thy =============================*)
1.331 +
1.332 +"-------- example in mail Nipkow";
1.333 +val t = str2term "x/(x^^^2 + -1*y^^^2) + y/(x^^^2 + -1*x*y)";
1.334 +val SOME (t', asm) = common_nominator_p_ thy t;
1.335 +if term2str t' = "x * x / " ^
1.336 + "((x + -1 * y) * ((x + y) * x))" ^
1.337 + " +\n" ^
1.338 + "y * (x + y) / " ^
1.339 + "((x + -1 * y) * ((x + y) * x))"
1.340 +then () else error "common_nominator_p_ term 2 changed"
1.341 +;
1.342 +(*========== inhibit exn WN130823 asm different Rational<-->2.thy ==============================
1.343 +if terms2str asm = "[\"x + y\",\"x\",\"x + ~1 * y\"]"
1.344 +then () else error "common_nominator_p_ asm 2 changed"
1.345 +============ inhibit exn WN130823 asm different Rational<-->2.thy =============================*)
1.346 +
1.347 +"-------- example: applicable tested by SML code";
1.348 +val t = str2term "nothing / to_add";
1.349 +if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed";
1.350 +
1.351 +"-------- fun add_fraction_p_ ------------------------------------------------";
1.352 +"-------- fun add_fraction_p_ ------------------------------------------------";
1.353 +"-------- fun add_fraction_p_ ------------------------------------------------";
1.354 +val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.355 +val SOME (t', asm) = add_fraction_p_ thy t;
1.356 +if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)"
1.357 +then () else error "add_fraction_p_ 3 changed";
1.358 +(*========== inhibit exn WN130823 asm different Rational<-->2.thy ==============================
1.359 +if terms2str asm = "[\"-1 + x ^^^ 2\"]"
1.360 +then () else error "add_fraction_p_ 3 changed";
1.361 +============ inhibit exn WN130823 asm different Rational<-->2.thy =============================*)
1.362 +
1.363 +"-------- TODO ---------------------------------------------------------------";
1.364 +"-------- TODO ---------------------------------------------------------------";
1.365 +"-------- TODO ---------------------------------------------------------------";
1.366 +
1.367 +
1.368
1.369 "-------- and app_rev --------------------------------------------------------";
1.370 "-------- and app_rev --------------------------------------------------------";
1.371 @@ -378,7 +192,7 @@
1.372 "~~~~~ fun rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
1.373 (thy, 1, bool, [], rls, term);
1.374 (*val (t', asm, rew) = app_rev thy (i+1) rrls t; rew = false!!!!!!!!!!!!!!!!!!!!!*)
1.375 -"~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.376 +"~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
1.377 fun chk_prepat thy erls [] t = true
1.378 | chk_prepat thy erls prepat t =
1.379 let
1.380 @@ -495,6 +309,205 @@
1.381 then () else error "norm_rational_ 5 changed";
1.382
1.383
1.384 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------------------";
1.385 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------------------";
1.386 +"-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------------------";
1.387 +val thy = @{theory "Rational"};
1.388 +val thy' = "Rational";
1.389 +val rls' = "cancel";
1.390 +val mp = "make_polynomial";
1.391 +
1.392 +"-------- example 186a";
1.393 +val t = str2term "(14 * x * y) / (x * y)";
1.394 + is_expanded (str2term "14 * x * y");
1.395 + is_expanded (str2term "x * y");
1.396 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.397 +if (term2str t', terms2str asm) = ("14 / 1", "[\"y * x ~= 0\"]")
1.398 +then () else error "rational.sml cancel Schalk 186a";
1.399 +
1.400 +"-------- example 186b";
1.401 +val t = str2term "(60 * a * b) / ( 15 * a * b )";
1.402 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.403 +if (term2str t', terms2str asm) = ("4 / 1", "[\"15 * (b * a) ~= 0\"]")
1.404 +then () else error "rational.sml cancel Schalk 186b";
1.405 +
1.406 +"-------- example 186c";
1.407 +val t = str2term "(144 * a^^^2 * b * c) / (12 * a * b * c)";
1.408 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.409 +if (term2str t', terms2str asm) = ("12 * a / 1", "[\"12 * (c * (b * a)) ~= 0\"]")
1.410 +then () else error "rational.sml cancel Schalk 186c";
1.411 +
1.412 +"-------- example 187a";
1.413 +val t = str2term "(12 * x * y) / (8 * y^^^2 )";
1.414 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.415 +if (term2str t', terms2str asm) = ("3 * x / (2 * y)", "[\"4 * y ~= 0\"]")
1.416 +then () else error "rational.sml cancel Schalk 187a";
1.417 +
1.418 +"-------- example 187b";
1.419 +val t = str2term "(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
1.420 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.421 +if (term2str t', terms2str asm) = ("4 * x / (9 * y)", "[\"2 * (z * (y * x)) ~= 0\"]")
1.422 +then () else error "rational.sml cancel Schalk 187b";
1.423 +
1.424 +"-------- example 187c";
1.425 +val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";
1.426 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.427 +if (term2str t', terms2str asm) =
1.428 + ("3 * z ^^^ 3 / (5 * (y * x))", "[\"3 * (z * (y ^^^ 2 * x ^^^ 5)) ~= 0\"]")
1.429 +then () else error "rational.sml cancel Schalk 187c";
1.430 +
1.431 +"-------- example 188a";
1.432 +val t = str2term "(-8 + 8 * x) / (-9 + 9 * x)";
1.433 + is_expanded (str2term "8 * x + -8");
1.434 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.435 +if (term2str t', terms2str asm) = ("8 / 9", "[\"-1 + x ~= 0\"]")
1.436 +then () else error "rational.sml cancel Schalk 188a";
1.437 +
1.438 +val t = str2term "(8*((-1) + x))/(9*((-1) + x))";
1.439 +val SOME (t,_) = rewrite_set_ thy false (*!!!!!!!!!!!!!!!!!!!!!!1*) make_polynomial t;
1.440 +if (term2str t', terms2str asm) = ("8 / 9", "[\"-1 + x ~= 0\"]")
1.441 +then () else error "rational.sml cancel Schalk make_polynomial 1";
1.442 +
1.443 +"-------- example 188b";
1.444 +val t = str2term "(-15 + 5 * x) / (-18 + 6 * x)";
1.445 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.446 +if (term2str t', terms2str asm) = ("5 / 6", "[\"-3 + x ~= 0\"]")
1.447 +then () else error "rational.sml cancel Schalk 188b";
1.448 +
1.449 +"-------- example 188c";
1.450 +val t = str2term "(a + -1 * b) / (b + -1 * a)";
1.451 +val SOME (t', asm) = rewrite_set_ thy false (*!!!!! NONE with cancel !!!!!*) cancel_p t;
1.452 +if (term2str t', terms2str asm) = ("-1 / 1", "[\"b + -1 * a ~= 0\"]")
1.453 +then () else error "rational.sml cancel Schalk 188c";
1.454 +
1.455 +is_expanded (str2term "a + -1 * b") = false (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*);
1.456 +val t = str2term "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
1.457 +val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.458 +if (term2str t', terms2str asm) = ("(a + -1 * b) / (-1 * a + b)", "[]")
1.459 +then () else error "rational.sml cancel Schalk make_polynomial 2";
1.460 +
1.461 +"-------- example 190a";
1.462 +val t = str2term "( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
1.463 +val SOME (t', asm) = rewrite_set_ thy false cancel t;
1.464 +if (term2str t', terms2str asm) =
1.465 + ("(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)", "[\"1 + 3 * a ~= 0\"]")
1.466 +then () else error "rational.sml cancel Schalk 190a";
1.467 +
1.468 +"-------- example 190c";
1.469 +val t = str2term "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1.470 +val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.471 +if (term2str t', terms2str asm) =
1.472 + ("(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)", "[]")
1.473 +then () else error "rational.sml make_polynomial Schalk 190c";
1.474 +
1.475 +"-------- example 191a";
1.476 +val t = str2term "( x^^^2 + -1 * y^^^2 ) / ( x + y )";
1.477 + is_expanded (str2term "x^^^2 + -1 * y^^^2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
1.478 + is_expanded (str2term "x + y") = true;
1.479 +val NONE (*!!!!!!!! WN.23.10.02 !!!!!!!!!!!!!!!*) = rewrite_set_ thy false cancel t;
1.480 +
1.481 +"-------- example 191b";
1.482 +val t = str2term "((x + (-1) * y)*(x + y))/((1)*(x + y))";
1.483 +val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.484 +if (term2str t', terms2str asm) = ("(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)", "[]")
1.485 +then () else error "rational.sml make_polynomial Schalk 191b";
1.486 +
1.487 +"-------- example 191c";
1.488 +val t = str2term "( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
1.489 + is_expanded (str2term "9 * x^^^2 + -30 * x + 25") = false; (*!!!!WN.23.10.02!!!!!!!!!!*)
1.490 + is_expanded (str2term "25 + -30*x + 9*x^^^2") = false; (*!!!!!!!!WN.23.10.02!!!!!!!!!!*)
1.491 + is_expanded (str2term "-25 + 9*x^^^2") = true;
1.492 +
1.493 +val t = str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
1.494 +val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.495 +if (term2str t', terms2str asm) = ("(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)", "[]")
1.496 +then () else error "rational.sml make_polynomial Schalk 191c";
1.497 +
1.498 +"-------- example 192b";
1.499 +val t = str2term "( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
1.500 +val NONE (*!!!!!!!! WN.23.10.02 !!!!!!!!!!!!!!!*) = rewrite_set_ thy false cancel t;
1.501 +
1.502 +val t = str2term "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.503 +val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.504 +if (term2str t', terms2str asm) =
1.505 + ("(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)", "[]")
1.506 +then () else error "rational.sml make_polynomial Schalk 192b";
1.507 +
1.508 +(*WN050929, === inhibit exn 110317 ===*)
1.509 +val t = str2term "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1.510 +val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
1.511 +if (term2str t', terms2str asm) =
1.512 + ("(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)", "[]")
1.513 +then () else error "rational.sml make_polynomial Schalk WN050929";
1.514 +
1.515 +"-------- example 193a";
1.516 +val t = str2term "( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
1.517 +val NONE (*!!!!!!!!!!!WN.23.10.02!!!!!!!!!!!!!11*) = rewrite_set_ thy false cancel t;
1.518 +
1.519 +"-------- example 193b";
1.520 +val t = str2term "( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
1.521 +val NONE (*!!!!!!!!!!!WN.23.10.02!!!!!!!!!!!!!11*) = rewrite_set_ thy false cancel t;
1.522 +
1.523 +"-------- example 193c";
1.524 +val t = str2term "( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
1.525 +val NONE (*!!!!!!!!!!!WN.23.10.02!!!!!!!!!!!!!11*) = rewrite_set_ thy false cancel t;
1.526 +
1.527 +(*WN:*)
1.528 +val t = str2term "(-25 + 9*x^^^2)/(5 + 3*x)";
1.529 +val SOME (t, asm) = rewrite_set_ thy false cancel t;
1.530 +if (term2str t', terms2str asm) =
1.531 + ("(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)", "[\"5 + 3 * x ~= 0\"]")
1.532 +then () else error "rational.sml cancel WN 1";
1.533 +
1.534 +"-------- some old tests REVISE ! --------------------------------------------";
1.535 +"-------- some old tests REVISE ! --------------------------------------------";
1.536 +"-------- some old tests REVISE ! --------------------------------------------";
1.537 +(*WAS --- external calculating functions test ---*)
1.538 +val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
1.539 +val SOME (t', asm) = factout_p_ thy t;
1.540 +if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso terms2str asm = "[]"
1.541 +then () else error "factout_p_ 1 changed";
1.542 +val SOME (t', asm) = cancel_p_ thy t;
1.543 +if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[\"1 + x ~= 0\"]"
1.544 +then () else error "cancel_p_ 1 changed";
1.545 +
1.546 +val t = str2term "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
1.547 +val SOME (t', asm) = factout_(*p_*) thy t;
1.548 +if term2str t' = "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))" andalso terms2str asm = "[]"
1.549 +then () else error "factout_ 2 changed";
1.550 +val SOME (t', asm) = cancel_(*p_*) thy t;
1.551 +if term2str t' = "(3 - 3 * x) / 2" andalso terms2str asm = "[\"-1 + x ~= 0\"]"
1.552 +then () else error "cancel_ 2 changed";
1.553 +
1.554 +val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
1.555 +val SOME (t', asm) = add_fraction_p_ thy t;
1.556 +if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
1.557 +then () else error "add_fraction_p_ 3 changed";
1.558 +val SOME (t', asm) = common_nominator_p_ thy t;
1.559 +if term2str t' =
1.560 + "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
1.561 + andalso terms2str asm = "[]"
1.562 +then () else error "common_nominator_p_ 3 changed";
1.563 +
1.564 +val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
1.565 +val SOME (t', asm) = add_fraction_ thy t;
1.566 +if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso terms2str asm = "[]"
1.567 +then () else error "factout_ 4 changed";
1.568 +val SOME (t', asm) = common_nominator_ thy t;
1.569 +if term2str t' =
1.570 + "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))"
1.571 + andalso terms2str asm = "[]"
1.572 +then () else error "cancel_ 4 changed";
1.573 +
1.574 +val t = str2term
1.575 + "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
1.576 +val SOME (t', asm) = add_fraction_p_ thy t;
1.577 +if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
1.578 +then () else error "add_fraction_p_ 5 changed";
1.579 +val SOME (t', asm) = norm_rational_ thy t;
1.580 +if term2str t' = "x / (1 + -2 * x + x ^^^ 2)" andalso terms2str asm = "[\"1 + x ~= 0\"]"
1.581 +then () else error "norm_rational_ 5 changed";
1.582 +
1.583
1.584 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.585 val SOME (t3',_) = common_nominator_ thy t3;