3 Copyright (c) Stefan Karnel 2002
4 Use is subject to license terms.
6 use"../smltest/IsacKnowledge/rational.sml";
10 nonterm.SK marks non-terminating examples
11 ord.SK PARTIALLY marks crucial ordering examples
12 *SK* of some (secondary) interest (on 070906)
13 ****************************************************************.*)
15 (******************************************************************
16 WN060104 transfer marked (*SR..*)examples to the exp-collection
17 # exp_IsacCore_Simp_Rat_Cancel.xml from rational.sml (*SRC*) 10 exp
18 # exp_IsacCore_Simp_Rat_Add.xml from rational.sml (*SRA*) 11 exp
19 # exp_IsacCore_Simp_Rat_Mult.xml from rational.sml (*SRM*) 5 exp
20 # exp_IsacCore_Simp_Rat_AddMult.xml from rational.sml (*SRAM*) 11 exp
21 # exp_IsacCore_Simp_Rat_Double.xml from rational.sml (*SRD*) 12 exp
22 *******************************************************************)
23 "-----------------------------------------------------------------";
24 "table of contents -----------------------------------------------";
25 "-----------------------------------------------------------------";
26 "~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~~~~~~~~~~";
27 "-------- ... missing WN060103 -----------------------------------";
28 "-------- fun monom2term, fun poly2term' ------------------------";
29 "~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
30 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
31 "-------- common_nominator_p ---------------------------- --------";
32 "-------- reverse rewrite ----------------------------------------";
33 "-------- 'reverse-ruleset' cancel_p -----------------------------";
34 "-------- norm_Rational ------------------------------------------";
35 "-------- numeral rationals --------------------------------------";
36 "-------- cancellation -------------------------------------------";
37 "-------- common denominator -------------------------------------";
38 "-------- multiply and cancel ------------------------------------";
39 "-------- common denominator and multiplication ------------------";
40 "-------- double fractions ---------------------------------------";
41 "-------- me Schalk I No.186 -------------------------------------";
42 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
43 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
44 "-------- investigate rulesets for cancel_p ----------------------";
45 "-------- investigate format of factout_ and factout_p_ ----------";
46 "-----------------------------------------------------------------";
47 "-----------------------------------------------------------------";
48 "-----------------------------------------------------------------";
51 "~~~~~BEGIN: decomment structure RationalI : RATIONALI ~~~~~~~~~~~";
52 (*.~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
53 tests of internal functions: to make them work,
54 out-comment (*!!!*) in knowledge/Rational.ML:
56 structure RationalI : RATIONALI =
63 !!!##*)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~.*)
65 (*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
66 print("\n\n********************* rational.sml - TESTS *************************\n\n");
67 print("\n\n***** divide tests *****\n");
68 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_)));
69 (* result: [(1,[0,0,1]),(1,[0,0,0])] *)
70 if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
72 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_)));
73 (* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
74 if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else raise error ("rational.sml: example failed");
76 val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
77 (* result: [(4,[1]),(4,[0])] *)
78 if mv_pquot2=[(4,[1]),(4,[0])] then () else raise error ("rational.sml: example failed");
80 val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
81 (* result: [(12,[0]] *)
82 if mv_prest2=[(12,[0])] then () else raise error ("rational.sml: example failed");
84 val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
85 (* [(2,[1]),(~2,[0])] *)
86 if mv_pquot3=[(2,[1]),(~2,[0])] then () else raise error ("rational.sml: example failed");
88 val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
89 (* [(1,[2]),(~1,[0])] *)
90 if mv_prest3=[(1,[2]),(~1,[0])] then () else raise error ("rational.sml: example failed");
92 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_)));
94 if mv_pquot4=[(1,[0,1,1])] then () else raise error ("rational.sml: example failed");
96 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_)));
97 (* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
98 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");
100 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_)));
101 (* [(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])]*)
102 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");
104 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_)));
106 if mv_prest5=[] then () else raise error ("rational.sml: example failed");
108 (* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
109 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_)));
110 if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
112 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_)));
113 if mv_prest6=[] then () else raise error ("rational.sml: example failed");
116 print("\n\n***** MV_CONTENT-TESTS *****\n");
117 val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
118 (* [(1,[0,1]),(1,[0,0])] *)
119 if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
121 val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
122 (*[(1,[1,0]),(1,[0,0])]*)
123 if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
125 val mv_cont2=mv_content([(2,[1]),(4,[0])]);
127 if mv_cont2=[(2,[0])] then () else raise error ("rational.sml: example failed");
129 val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
130 (* [(1,[1]),(2,[0])] *)
131 if mv_pp2=[(1,[1]),(2,[0])] then () else raise error ("rational.sml: example failed");
133 val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
135 if mv_cont3=[(2,[0,0,0])] then () else raise error ("rational.sml: example failed");
137 val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
138 (* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
139 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");
141 val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
143 if mv_cont4=[(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
145 val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
146 (* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
147 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");
149 val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
151 if con1=[(3,[0,0])] then () else raise error ("rational.sml: example failed");
153 val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
154 (* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
155 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");
157 val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
159 if con2=[(1,[0,0])] then () else raise error ("rational.sml: example failed");
161 val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
162 (* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
163 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");
165 val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
167 if cont1=[(3,[0,1,0])] then () else raise error ("rational.sml: example failed");
169 val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
171 if pp1=[(1,[2,0,0])] then () else raise error ("rational.sml: example failed");
173 val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
175 if cont2=[(2,[0,1,0])] then () else raise error ("rational.sml: example failed");
177 val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
178 (* [(1,[2,0,0]),(2,[1,1,0])] *)
179 if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else raise error ("rational.sml: example failed");
181 print("\n\n\n\n********************************************************\n\n");
182 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])];
183 if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
184 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])];
187 "-------- fun monom2term, fun poly2term' ------------------------";
188 "-------- fun monom2term, fun poly2term' ------------------------";
189 "-------- fun monom2term, fun poly2term' ------------------------";
190 val t = monom2term ((3,[2,1,0]), ["c","b","a"](*reverse ???SK-*));
191 term2str t = "3 * (c ^^^ 2 * b)" (*true*);
193 val t = monom2term ((1,[1,0]), ["b","a"]);
194 term2str t = "b" (*true*);
196 val t = poly2term ([(1,[0,0,0]),(2,[1,0,0]),(3,[2,1,0]),(4,[3,2,1])],
198 term2str t = "1 + 2 * c + 3 * (c ^^^ 2 * b) + 4 * (c ^^^ 3 * (b ^^^ 2 * a))";
200 val t = poly2term ([(1,[1,0]),(1,[0,1])], ["b","a"]);
201 term2str t = "a + b" (*true*);
204 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
205 "~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
206 "~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
207 "~~~~~END: decomment structure RationalI : RATIONALI ~~~~~~~~~~~~~";
210 fun parse_rat str = (term_of o the o (parse thy)) str;
212 print("\n\n***** mv_gcd-tests *****\n");
213 val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
214 (* [(2,[1,1]),(2,[0,0])] *)
215 if ggt1=[(2,[1,1]),(2,[0,0])] then () else raise error ("rational.sml: example failed");
217 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])];
218 (* [(2,[1,1,0]),(3,[0,0,1])] *)
219 if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
222 val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
223 (* [(1,[1,0]),(~1,[0,1])] *)
224 if ggt3=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
227 val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
229 if ggt4=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
232 val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
233 (* [(1,[1,0]),(~1,[0,1])] *)
234 if ggt5=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
237 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])];
239 if ggt6=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
241 print("\n\n***** kgv-tests *****\n");
242 val kgv1=mv_lcm [(10,[])] [(15,[])];
244 if kgv1=[(30,[])] then () else raise error ("rational.sml: example failed");
246 val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
247 (* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
248 if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else raise error ("rational.sml: example failed");
250 val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
251 (* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
252 if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else raise error ("rational.sml: example failed");
255 print("\n\n***** STEP_CANCEL_TESTS: *****\n");
257 val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) / (6 * a * c)";
258 val div2 = term2str (step_cancel term2);
259 if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else raise error ("rational.sml: example failed");
262 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";
263 val div1 = term2str(step_cancel term1);
264 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");
266 val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
267 val div3 = term2str(step_cancel term3);
268 if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else raise error ("rational.sml: example failed");
270 --------------------------------------------------------------------------!!!*)
272 (*-----versuche 13.3.03-----
273 val t = str2term "1 - x^^^2 - 5 * x^^^5";
274 val vs=(((map free2str) o vars) t);
275 val SOME ml = expanded2poly t vs;
277 poly2term'(rev(sort (mv_geq LEX_) (ml)),vs);
278 poly2term'([(~5,[5]),(~1,[2]),(1,[0])], vs);
279 monom2term((~5,[5]),vs);
280 monom2term((~1,[2]),vs);
281 val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
283 val (i,is) = (~1,[2]);
284 val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
285 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
286 Free ((str_of_int o abs) i, HOLogic.realT)) $
287 powerproduct2term(is, vs);
289 -------versuche 13.3.03-----*)
291 val t = str2term "1 - x^^^2 - 5 * x^^^5";
292 val SOME t' = expanded2polynomial t; term2str t';
293 "1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5";
294 val t = str2term "1 - x";
295 val SOME t' = expanded2polynomial t; term2str t';
297 val t = str2term "1 + (-1) * x";
298 val SOME t' = expanded2polynomial t; term2str t';
300 val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5";
301 val SOME t' = polynomial2expanded t; term2str t';
302 "1 - x ^^^ 2 - 5 * x ^^^ 5";
305 " external calculating functions test ";
306 " external calculating functions test ";
307 " external calculating functions test ";
309 val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
310 val SOME (t1',asm)= factout_p_ thy t1;
311 term2str t1'; terms2str asm;
312 "(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))";
314 val SOME (t1',asm)= cancel_p_ thy t1;
315 term2str t1'; terms2str asm;
317 "[\"1 + 1 * x ~= 0\"]";
319 val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
320 val SOME (t',asm)= cancel_ thy t;
321 term2str t'; terms2str asm;
324 val SOME (t',asm)= factout_ thy t;
325 term2str t'; terms2str asm;
326 "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))";
329 val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
330 val SOME (t',asm) = add_fraction_p_ thy t;
331 term2str t'; terms2str asm;
332 "(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)";
334 val SOME (t',asm) = common_nominator_p_ thy t;
335 term2str t'; terms2str asm;
336 "(-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))";
339 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
340 val SOME (t',asm) = add_fraction_ thy t;
341 term2str t'; terms2str asm;
342 "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)";
344 val SOME (t',asm) = common_nominator_ thy t;
345 term2str t'; terms2str asm;
346 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))";
349 val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
350 val SOME (t',asm) = common_nominator_p_ thy t;
351 term2str t'; terms2str asm;
352 "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 * (#";
354 val SOME (t',asm) = add_fraction_p_ thy t;
355 term2str t'; terms2str asm;
356 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
357 "[\"1 + 1 * x ~= 0\"]";
358 val SOME(t',asm) = norm_rational_ thy t;
359 term2str t'; terms2str asm;
360 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
361 "[\"1 + 1 * x ~= 0\"]";
363 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))";
364 val SOME (t3',_) = common_nominator_ thy t3;
365 val SOME (t3'',_) = add_fraction_ thy t3;
369 val SOME(t4,t5) = norm_expanded_rat_ thy t3;
375 val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
376 val SOME (t',_) = factout_ thy t;
377 val SOME (t'',_) = cancel_ thy t;
380 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
383 val t=(term_of o the o (parse thy))
384 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)";
385 val SOME (t',_) = common_nominator_ thy t;
386 val SOME (t'',_) = add_fraction_ thy t;
389 "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))";
392 (*WN021016 added -----vv---*)
393 val t = str2term "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
394 val SOME (t',_) = common_nominator_ thy t;
395 val SOME (t'',_) = add_fraction_ thy t;
396 term2str t' = "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n1\
397 \ * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
398 term2str t'' = "6 / (3 - x)" (*true*);
400 val t = str2term "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
401 val SOME (t',_) = common_nominator_ thy t;
402 val SOME (t'',_) = add_fraction_ thy t;
403 term2str t' = "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\n\
404 \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)" (*true*);
405 term2str t'' = "6 / (3 - x)" (*true*);
406 (*WN021016 added -----^^---*)
407 (*WN030602 added -----vv--- no rewrite -> NONE !*)
408 val t = str2term "1 / a";
409 val NONE = cancel_p_ thy t;
410 val NONE = rewrite_set_ thy false cancel_p t;
411 (*WN.2.6.03 added -------^^---*)
413 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
414 val SOME (t',_) = factout_ thy t;
415 val SOME (t'',_) = cancel_ thy t;
416 term2str t' = "(y + x) * (y - x) / ((y - x) * (y - x))"(*true*);
417 term2str t'' = "(y + x) / (y - x)";
419 val t = str2term "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
420 val SOME (t',_) = common_nominator_ thy t;
421 val SOME (t'',_) = add_fraction_ thy t;
423 "(-1 * x ^^^ 2 + y ^^^ 2) / ((-1 * x + y) * (-1 * x + y)) +\n1\
424 \ * (-1 * x + y) / ((-1 * x + y) * (-1 * x + y))" (*true*);
425 term2str t'' = "(-1 - x - y) / (x - y)" (*true*);
427 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
428 val SOME (t',_) = common_nominator_ thy t;
429 val SOME (t'',_) = add_fraction_ thy t;
430 if term2str t' = "(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x))\
431 \ +\n1 * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" then ()
432 else raise error "rational.sml lex-ord 1";
433 if term2str t'' = "(-1 - y - x) / (y - x)" then ()
434 else raise error "rational.sml lex-ord 2";
435 (*WN.16.10.02 WN070905 lexicographische Ordnung erhalten ! SK.ord*)
438 val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2)";
439 val SOME (t',_) = norm_expanded_rat_ thy t;
440 if term2str t' = "(x + y) / (x - y)" then ()
441 else raise error "rational.sml term2poly: invalid x ^^^ 2 - y ^^^ 2 1";
442 (*val SOME (t'',_) = norm_rational_ thy t;
443 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
444 WN.16.10.02 ?! + WN060831???SK4
445 WN070905 *** term2poly: invalid = x ^^^ 2 - y ^^^ 2*)
448 val t = str2term "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
449 val SOME (t',_) = norm_expanded_rat_ thy t;
450 if term2str t' = "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)" then ()
451 else raise error "rational.sml (9 - x^^^2)/(9 - 6*x + x^^^2) +...";
452 (*val SOME (t'',_) = norm_rational_ thy t;
453 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial WN.16.10.02 ?!
454 WN070906 *** term2poly: invalid = 9 - x ^^^ 2 SK.term2poly*)
456 val t=(term_of o the o (parse thy))
457 "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
458 val SOME (t',_) = norm_expanded_rat_ thy t;
459 val SOME (t'',_) = norm_rational_ thy t;
462 "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
463 "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)";
466 " examples from: Mathematik 1 Schalk Reniets Verlag ";
467 " examples from: Mathematik 1 Schalk Reniets Verlag ";
468 " examples from: Mathematik 1 Schalk Reniets Verlag ";
471 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
472 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
473 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
474 val thy' = "Rational.thy";
476 val mp = "make_polynomial";
478 print("\n\nexample 186:\n");
480 val e186a'="(14 * x * y) / ( x * y )";(*SRC*)
481 val e186a = the (rewrite_set thy' false "cancel" e186a');
482 is_expanded (parse_rat "14 * x * y");
483 is_expanded (parse_rat "x * y");
486 val e186b'="(60 * a * b) / ( 15 * a * b )";
487 val e186b = the (rewrite_set thy' false "cancel" e186b');
489 val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
490 val e186c = (the (rewrite_set thy' false "cancel" e186c'))
491 handle e => print_exn e;
492 val t = (term_of o the o (parse thy)) e186c';
495 print("\n\nexample 187:\n");
497 val e187a'="(12 * x * y) / (8 * y^^^2 )";(*SRC*)
498 val e187a = the (rewrite_set thy' false "cancel" e187a');
500 val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
501 val e187b = the (rewrite_set thy' false "cancel" e187b');
503 val e187c'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*)
504 val e187c = the (rewrite_set thy' false "cancel" e187c');
507 val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*)
508 val e188a = the (rewrite_set thy' false "cancel" e188a');
509 is_expanded (parse_rat "8 * x + -8");
510 (* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
511 if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
512 else raise error "rational.sml: e188a new behaviour";
513 val SOME (t,_) = rewrite_set thy' false mp
514 "(8*((-1) + x))/(9*((-1) + x))";
516 val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
517 val SOME (t,_) = rewrite_set thy' false "cancel" e188b';
518 t = "5 / 6" (*true*);
521 val e188c'="( a + -1 * b ) / ( b + -1 * a )";
522 val e188c = the (rewrite_set thy' false "cancel_p" e188c');
523 (*is_expanded (parse_rat "a + -1 * b");*)
525 rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
526 if t= "(a + -1 * b) / (-1 * a + b)" then()
527 else raise error "rational.sml: e188c new behaviour";
529 print("\n\nexample 190:\n");
531 val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
532 val e190c = the (rewrite_set thy' false "cancel" e190c');
533 val SOME (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
534 if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
535 else raise error "rational.sml: e190c new behaviour";
537 print("\n\nexample 191:\n");
539 val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )";
541 val e191a = the (rewrite_set thy' false "cancel" e191a');
542 is_expanded (parse_rat "x^^^2 + -1 * y^^^2");
544 is_expanded (parse_rat "x + y");
546 val SOME (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
547 (* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
548 if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
549 else raise error "rational.sml: e191a new behaviour";
552 val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
554 val e191c = the (rewrite_set thy' false "cancel" e191c');
555 is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25");
557 is_expanded (parse_rat "25 + -30*x + 9*x^^^2");
559 is_expanded (parse_rat "-25 + 9*x^^^2");
561 val SOME (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
562 (* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
563 if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
564 else raise error "rational.sml: 'e191c' new behaviour";
567 print("\n\nexample 192:\n");
569 val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
571 val e192b = the (rewrite_set thy' false "cancel" e192b');
572 -------------------*)
573 val SOME (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
574 if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)"
575 (*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*)
576 then () else raise error "rational.sml: 'e192b' new behaviour";
577 (*^^^ works with MG's simplifier vvv*)
578 val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
579 val SOME (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
580 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";
583 print("\n\nexample 193:\n");
585 val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
587 val e193a = the (rewrite_set thy' false "cancel" e193a');
588 -------------------*)
590 val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
592 val e193b = the (rewrite_set thy' false "cancel" e193b');
594 val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
595 val SOME(t,_) = rewrite_set thy' false "cancel" e193c';
596 -------------------*)
598 val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
599 val SOME (t,_) = rewrite_set thy' false "cancel" wn01;
600 (* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
601 if t = "(-5 + 3 * x) / 1" then ()
602 else raise error "rational.sml: new behav. in cancel wn01";
605 "-------- common_nominator_p ---------------------------- --------";
606 "-------- common_nominator_p ---------------------------- --------";
607 "-------- common_nominator_p ---------------------------- --------";
608 val rls' = "common_nominator_p";
610 print("\n\nexample 204:\n");
612 val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)";
613 val e204a = the (rewrite_set thy' false "common_nominator_p" e204a');
615 val e204b'="5 / x + -3 / x + -1 / x";
616 val e204b = the (rewrite_set thy' false "common_nominator_p" e204b');
618 print("\n\nexample 205:\n");
620 val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)";
621 val e205a = the (rewrite_set thy' false "common_nominator_p" e205a');
623 val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)";
624 val e205b = the (rewrite_set thy' false "common_nominator_p" e205b');
626 print("\n\nexample 206:\n");
628 val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))";
629 val e206a = the (rewrite_set thy' false "common_nominator_p" e206a');
631 val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))";
632 val e206b = the (rewrite_set thy' false "common_nominator_p" e206b');
634 print("\n\nexample 207:\n");
635 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)) ";
636 val e207 = the (rewrite_set thy' false "common_nominator_p" e207');
638 print("\n\nexample 208:\n");
639 val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) ";
640 val e208 = the (rewrite_set thy' false "common_nominator_p" e208');
642 print("\n\nexample 209:\n");
643 val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) ";
644 val e209 = the (rewrite_set thy' false "common_nominator_p" e209');
646 print("\n\nexample 210:\n");
647 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)) ";
648 val e210 = the (rewrite_set thy' false "common_nominator_p" e210');
650 print("\n\nexample 211:\n");
652 val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))";
653 val e211a = the (rewrite_set thy' false "common_nominator_p" e211a');
655 val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))";
656 val e211b = the (rewrite_set thy' false "common_nominator_p" e211b');
658 print("\n\nexample 212:\n");
660 val e212a'="((4) / (x)) + ((-3) / (y)) + -1";
661 val e212a = the (rewrite_set thy' false "common_nominator_p" e212a');
663 val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))";
664 val e212b = the (rewrite_set thy' false "common_nominator_p" e212b');
666 print("\n\nexample 213:\n");
668 val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) ";
669 val e213a = the (rewrite_set thy' false "common_nominator_p" e213a');
671 val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))";
672 val e213b = the (rewrite_set thy' false "common_nominator_p" e213b');
674 print("\n\nexample 214:\n");
676 val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))";
677 val e214a = the (rewrite_set thy' false "common_nominator_p" e214a');
679 val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))";
680 val e214b = the (rewrite_set thy' false "common_nominator_p" e214b');
682 print("\n\nexample 216:\n");
684 val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))";
685 val e216a = the (rewrite_set thy' false "common_nominator_p" e216a');
687 val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))";
688 val e216b = the (rewrite_set thy' false "common_nominator_p" e216b');
690 print("\n\nexample 217:\n");
691 val e217'="((z + -1) / (z)) + ((3 * z ^^^2 + -6 * z + 5) / (z^^^2)) + ((-4 * z^^^3 + 7 * z^^^2 + -5 * z + 5) / (z^^^3))";
692 val e217 = the (rewrite_set thy' false "common_nominator_p" e217');
695 val rls' = "common_nominator";
696 print("\n\nexample 218:\n");
697 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))";
698 val e218 = the (rewrite_set thy' false "common_nominator" e218');
700 print("\n\nexample 219:\n");
702 val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))";
703 val e219a = the (rewrite_set thy' false "common_nominator" e219a');
705 val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))";
706 val e219b = the (rewrite_set thy' false "common_nominator" e219b');
708 print("\n\nexample 220:\n");
710 val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))";
711 val e220a = the (rewrite_set thy' false "common_nominator" e220a');
713 val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))";
714 val e220b = the (rewrite_set thy' false "common_nominator" e220b');
716 print("\n\nexample 221:\n");
718 val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))";
719 val e221a = the (rewrite_set thy' false "common_nominator" e221a');
721 val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) ";
722 val e221b = the (rewrite_set thy' false "common_nominator" e221b');
724 print("\n\nexample 222:\n");
726 val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))";
727 val e222a = the (rewrite_set thy' false "common_nominator" e222a');
729 val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))";
730 val e222b = the (rewrite_set thy' false "common_nominator" e222b');
732 print("\n\nexample 225:\n");
734 val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))";
735 val e225a = the (rewrite_set thy' false "common_nominator" e225a');
737 val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))";
738 val e225b = the (rewrite_set thy' false "common_nominator" e225b');
740 print("\n\nexample 226:\n");
742 val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) ";
743 val e226a = the (rewrite_set thy' false "common_nominator" e226a');
745 val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2";
746 val e226b = the (rewrite_set thy' false "common_nominator" e226b');
748 print("\n\nexample 227:\n");
750 val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 ";
751 val e227a = the (rewrite_set thy' false "common_nominator" e227a');
753 val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 ";
754 val e227b = the (rewrite_set thy' false "common_nominator" e227b');
756 print("\n\nexample 228:\n");
758 val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))";
759 val e228a = the (rewrite_set thy' false "common_nominator" e228a');
761 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))";
762 val e228b = the (rewrite_set thy' false "common_nominator" e228b');
765 print("\n\nexample 229:\n");
767 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))";
768 val e229a = the (rewrite_set thy' false "common_nominator" e229a');
770 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))";
771 val e229b = the (rewrite_set thy' false "common_nominator" e229b');
773 print("\n\nexample 230:\n");
775 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))";
776 val e230a = the (rewrite_set thy' false "common_nominator" e230a');
778 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))";
779 val e230b = the (rewrite_set thy' false "common_nominator" e230b');
781 print("\n\nexample 231:\n");
783 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))";
784 val e231a = the (rewrite_set thy' false "common_nominator" e231a');
786 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))";
787 val e231b = the (rewrite_set thy' false "common_nominator" e231b');
789 print("\n\nexample 232:\n");
791 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))";
792 val e232a = the (rewrite_set thy' false "common_nominator" e232a');
794 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))";
795 val e232b = the (rewrite_set thy' false "common_nominator" e232b');
797 print("\n\nexample 233:\n");
799 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))";
800 val e233a = the (rewrite_set thy' false "common_nominator" e233a');
802 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))";
803 val e233b = the (rewrite_set thy' false "common_nominator" e233b');
805 print("\n\nexample 234:\n");
807 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))";
808 val e234a = the (rewrite_set thy' false "common_nominator" e234a');
810 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)) ";
811 val e234b = the (rewrite_set thy' false "common_nominator" e234b');
813 print("\n\nexample 235:\n");
815 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))";
816 val e235a = the (rewrite_set thy' false "common_nominator" e235a');
818 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)) ";
819 val e235b = the (rewrite_set thy' false "common_nominator" e235b');
821 print("\n\nexample 236:\n");
823 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))";
824 val e236a = the (rewrite_set thy' false "common_nominator" e236a');
826 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)) ";
827 val e236b = the (rewrite_set thy' false "common_nominator" e236b');
831 print("\n\nexample heuberger:\n");
832 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)";
833 val eheu = the (rewrite_set thy' false "cancel" eheu');
835 val rls' = "common_nominator_p";
836 print("\n\nexample stiefel:\n");
837 val est1'="(7) / (-14) + (-2) / (4)";
838 val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
839 if est1 = ("-1 / 1",[]) then ()
840 else raise error "new behaviour in rational.sml: est1'";
842 val t = (term_of o the o (parse thy))
843 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
844 val SOME (t',_) = factout_ thy t;
846 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
849 "-------- reverse rewrite ----------------------------------------";
850 "-------- reverse rewrite ----------------------------------------";
851 "-------- reverse rewrite ----------------------------------------";
853 (*WN.28.8.02: tests for the 'reverse-rewrite' functions:
854 these are defined in Rationals.ML and stored in
855 the 'reverse-ruleset' cancel*)
857 (*the term for which reverse rewriting is demonstrated*)
858 val t = (term_of o the o (parse thy))
859 "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
860 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
861 next_rule=nex,normal_form=nor,...},...} = cancel;
863 (*normal_form produces the result in ONE step*)
864 val SOME (t',_) = nor t;
867 (*initialize the interpreter state used by the 'me'*)
868 val (t,_,revsets,_) = ini t;
870 (*find the rule 'r' to apply to term 't'*)
871 val SOME r = nex revsets t;
872 (*val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
874 (*check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
875 if the rule is OK, the term resulting from applying the rule is returned,too;
876 there might be several rule applications inbetween,
877 which are listed after the head in reverse order*)
878 val (r,(t,asm))::_ = loc revsets t r;
880 "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
882 (*find the next rule to apply*)
883 val SOME r = nex revsets t;
884 (*val r = Thm ("sym_#power_3_2","9 = 3 ^^^ 2") : rule*)
886 (*check the next rule*)
887 val (r,(t,asm))::_ = loc revsets t r;
889 "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
891 (*find and check the next rules, rewrite*)
892 val SOME r = nex revsets t;
893 val (r,(t,asm))::_ = loc revsets t r;
895 "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
897 val SOME r = nex revsets t;
898 val (r,(t,asm))::_ = loc revsets t r;
900 "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
902 val SOME r = nex revsets t;
903 val (r,(t,asm))::_ = loc revsets t r;
905 "(3 - x) * (3 + x) / ((3 + x) * (3 + x))";
907 val SOME r = nex revsets t;
908 val (r,(t,asm))::_ = loc revsets t r;
910 if ss = "(3 - x) / (3 + x)" then ()
911 else raise error "rational.sml: new behav. in rev-set cancel";
915 "-------- 'reverse-ruleset' cancel_p -----------------------------";
916 "-------- 'reverse-ruleset' cancel_p -----------------------------";
917 "-------- 'reverse-ruleset' cancel_p -----------------------------";
918 (*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
920 (*the term for which reverse rewriting is demonstrated*)
921 val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
922 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
923 next_rule=nex,normal_form=nor,...},...} = cancel_p;
925 (*normal_form produces the result in ONE step*)
926 val SOME (t',_) = nor t;
927 term2str t' = "(3 + 1 * x) / (3 + -1 * x)";
929 (*initialize the interpreter state used by the 'me'*)
930 val SOME (t', asm) = cancel_p_ thy t;
931 term2str t' = "(3 + x) / (3 + -1 * x)" (*true*);
932 terms2str asm = "[\"3 + -1 * x ~= 0\"]" (*true*);
933 val (t,_,revsets,_) = ini t;
935 (* WN.10.10.02: dieser Fall terminiert nicht
936 (make_polynomial enth"alt zu viele rules)
937 WN060823 'init_state' requires rewriting on specified location in the term
938 print_depth 99; Rfuns; print_depth 3;
939 WN060831 cycling "sym_order_mult_rls_" "sym_real_mult_assoc"
940 as was with make_polynomial before ?!?*)
942 val SOME r = nex revsets t;
943 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",
944 mk_thm Rational.thy "9 = 3 ^^^ 2"));
945 (*WN060831 *** id_of_thm
946 Exception- ERROR raised ...
947 val (r,(t,asm))::_ = loc revsets t r;
950 val SOME r = nex revsets t;
951 val (r,(t,asm))::_ = loc revsets t r;
955 print "\n\n\n****************** all tests successfull *************************\n";
959 (*WN.17.3.03 =========================================================vvv---*)
960 "-------- norm_Rational ------------------------------------------";
961 "-------- norm_Rational ------------------------------------------";
962 "-------- norm_Rational ------------------------------------------";
963 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
964 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
965 if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1";
967 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
968 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
969 if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
970 else raise error "rational.sml 2";
972 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
973 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
974 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
975 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
976 else raise error "rational.sml 3";
977 (*trace_rewrite:=true;*)
978 val t = str2term "Not (6*x is_atom)";
979 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
981 val t = str2term "1 < 2";
982 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
984 val t = str2term "(6*x)^^^2";
985 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
986 (num_str realpow_def_atom) t;
988 trace_rewrite:=false;
990 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
991 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
992 if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4";
994 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
995 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
996 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
997 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
998 else raise error "rational.sml 5";
1000 (*SRAM Schalk I, p.92 Nr. 609a*)
1001 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
1002 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1003 if term2str t' = "(-255 + 112 * x) / 135" then ()
1004 else raise error "rational.sml 6";
1006 (*SRAM Schalk I, p.92 Nr. 610c*)
1007 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
1008 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1009 if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7";
1011 (*SRAM Schalk I, p.92 Nr. 476a*)
1012 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\
1013 \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
1014 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1015 (*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*)
1016 if term2str t' = "1" then () else raise error "rational.sml 8";
1018 (*............................vvv---TODO: sollte gehen mit poly_order *)
1019 (*Schalk I, p.92 Nr. 472a*)
1020 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
1021 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1022 if term2str t' = "x + y" then () else raise error "rational.sml p.92 Nr. 472a";
1024 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1025 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1026 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1027 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1028 \(20*x*y/(x^^^2 - 25*y^^^2))";
1029 (*... nicht simpl, zerlegt ...*)
1030 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1031 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))";
1032 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1033 "(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
1034 (* ~~~~~~~~~~ poly_order notwendig!*)
1035 val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1036 \(20*x*y/(x^^^2 - 25*y^^^2))";
1037 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1038 "(-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))";
1039 trace_rewrite:=true;
1040 trace_rewrite:=false;
1042 "nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
1043 (*WN.2.6.03 from rlang.sml 56a
1044 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)";
1045 val NONE = rewrite_set_ thy false common_nominator_p t;
1047 WN060831 nonterm.SK7
1048 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1049 val NONE = add_fraction_p_ thy t;
1053 (* ------------------------------------------------------------------- *)
1054 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
1055 (* Simplifier fuer beliebige Buchterme *)
1056 (* ------------------------------------------------------------------- *)
1057 (*----------------------- norm_Rational_mg ----------------------------*)
1058 (* ------------------------------------------------------------------- *)
1060 "-------- numeral rationals --------------------------------------";
1061 "-------- numeral rationals --------------------------------------";
1062 "-------- numeral rationals --------------------------------------";
1064 (*SRA Schalk I, p.40 Nr. 164b *)
1065 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
1066 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1068 if (term2str t) = "19 / 21" then ()
1069 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
1071 (*SRA Schalk I, p.40 Nr. 166a *)
1072 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1073 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1075 if (term2str t) = "45 / 2" then ()
1076 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
1079 "-------- cancellation -------------------------------------------";
1080 "-------- cancellation -------------------------------------------";
1081 "-------- cancellation -------------------------------------------";
1083 (* e190c Stefan K.*)
1085 "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1086 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1089 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1091 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
1093 (* e192b Stefan K.*)
1095 "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1096 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1101 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
1103 (*SRC Schalk I, p.66 Nr. 379c *)
1106 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1111 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
1113 (*SRC Schalk I, p.66 Nr. 380b *)
1115 "15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
1116 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1119 "(27 + 12 * x) / (28 + 8 * x)"
1121 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1123 (*Schalk I, p.60 Nr. 215c *)
1124 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
1126 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1127 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1130 "(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)"
1132 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
1135 "(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)"
1136 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1138 (* uncaught exception nonexhaustive binding failure
1139 raised at: stdIn:93.1-93.51 *)
1141 (*Schalk I, p.66 Nr. 381a *)
1142 (* ACHTUNG: rechnet ca. 2 Minuten !!! *)
1144 val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
1145 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1148 "(a + b) / (4 * a + -4 * b)"
1149 then () else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1152 (*SRC Schalk I, p.66 Nr. 381b *)
1154 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1155 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1160 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
1162 (*SRC Schalk I, p.66 Nr. 381c *)
1164 "(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
1165 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1168 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1170 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
1172 (*SRC Schalk I, p.66 Nr. 383a *)
1174 "(5*a^^^2 - 5*a*b)/(a - b)^^^2";
1175 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1178 "5 * a / (a + -1 * b)"
1180 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
1182 "-------- common denominator -------------------------------------";
1183 "-------- common denominator -------------------------------------";
1184 "-------- common denominator -------------------------------------";
1186 (*SRA Schalk I, p.67 Nr. 403a *)
1189 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1192 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1194 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
1196 (*SRA Schalk I, p.67 Nr. 407b *)
1198 "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
1199 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1204 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
1206 (*SRA Schalk I, p.67 Nr. 410b *)
1208 "1/(x+1) + 1/(x+2) - 2/(x+3)";
1209 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1212 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1214 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
1216 (*SRA Schalk I, p.67 Nr. 413b *)
1218 "(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
1219 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1222 "6 * x / (1 + -1 * x ^^^ 2)"
1224 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
1226 (*SRA Schalk I, p.68 Nr. 414a *)
1228 "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
1229 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1232 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1234 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
1236 (*SRA Schalk I, p.68 Nr. 423a *)
1238 "(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)";
1239 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1244 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
1246 (*SRA Schalk I, p.68 Nr. 428b *)
1248 "1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
1249 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1252 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1254 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
1256 (*SRA Schalk I, p.68 Nr. 430b *)
1258 "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";
1259 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1264 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
1267 (*SRA Schalk I, p.68 Nr. 432 *)
1269 "(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)";
1270 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1275 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
1280 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1283 "(3 * y + b * x) / (b * y)"
1285 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
1288 "-------- multiply and cancel ------------------------------------";
1289 "-------- multiply and cancel ------------------------------------";
1290 "-------- multiply and cancel ------------------------------------";
1292 (*SRM Schalk I, p.68 Nr. 436a *)
1294 "3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)";
1295 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1298 "(5 * x + -5 * y) / (18 * x + 18 * y)"
1300 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1302 (*SRM.test Schalk I, p.68 Nr. 436b *)
1303 (*WN060420???MG3 crashes with method 'simplify' in
1304 IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
1305 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1306 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1309 "5 * a / (a + -1 * b)"
1311 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1313 (*Schalk I, p.68 Nr. 437a *)
1314 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1315 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1316 if (term2str t) = "1 / (4 * c + 3 * e)" then ()
1317 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1319 "----- S.K. corrected non-termination 060904";
1320 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1321 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1322 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 ()
1323 else raise error "rational.sml.sml: S.K.8..corrected 060904-6";
1325 "----- S.K. corrected non-termination of cancel_p_";
1326 val t'' = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
1327 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
1328 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1329 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1330 else raise error "rational.sml.sml: diff.behav. in cancel_p S.K.8";
1334 (*Schalk I, p.68 Nr. 437b *)
1335 (* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1336 val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1337 (* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1340 (*a casual output from above*)
1342 "(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)";
1343 (* WN060831 nonterm.SK10
1344 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1348 (*SRM Schalk I, p.68 Nr. 438a *)
1350 "x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
1351 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1356 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1358 (*SRM Schalk I, p.68 Nr. 439b *)
1360 "(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
1361 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1364 "(x + -4 * x ^^^ 3) / 2"
1366 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
1368 (*SRM Schalk I, p.68 Nr. 440a *)
1370 "(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
1371 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1374 "(-3 + x) / (2 + x)"
1376 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1378 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
1380 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1381 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1382 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1383 else raise error "rational.sml.sml: diff.behav. in norm_Rational 27";
1385 "----- SK12 works since 0707xx";
1386 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1387 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1388 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1389 else raise error "rational.sml.sml: diff.behav. in norm_Rational 28";
1392 "-------- common denominator and multiplication ------------------";
1393 "-------- common denominator and multiplication ------------------";
1394 "-------- common denominator and multiplication ------------------";
1396 (*----------------------------------------------------------------------*)
1397 (*--------- Gemeinsamer Nenner und Multiplikation von Bruechen ---------*)
1398 (*----------------------------------------------------------------------*)
1401 (*SRAM Schalk I, p.69 Nr. 441b *)
1402 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1403 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1406 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1408 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1410 (*SRAM Schalk I, p.69 Nr. 442b *)
1411 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)";
1412 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1415 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1417 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1419 (*SRAM Schalk I, p.69 Nr. 443b *)
1420 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1421 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1424 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1426 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1428 (*SRAM Schalk I, p.69 Nr. 445b *)
1429 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1430 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1435 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1437 (*SRAM Schalk I, p.69 Nr. 446b *)
1438 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1439 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1442 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1444 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1446 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1448 "(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)";
1449 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1452 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1454 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1456 (*SRAM Schalk I, p.69 Nr. 450a *)
1458 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1459 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1462 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1464 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1466 "-------- double fractions ---------------------------------------";
1467 "-------- double fractions ---------------------------------------";
1468 "-------- double fractions ---------------------------------------";
1470 (*SRD Schalk I, p.69 Nr. 454b *)
1472 "((2 - x)/(2*a)) / (2*a/(x - 2))";
1473 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1476 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1478 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1480 (*SRD Schalk I, p.69 Nr. 455a *)
1482 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1483 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1486 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1487 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1490 "----- Schalk I, p.69 Nr. 455b";
1491 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1492 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1493 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1494 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1496 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1497 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1498 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1499 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1500 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37b";
1502 "----- ?: worked before 0707xx";
1503 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1504 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1505 if term2str t = "-1 / (3 + y)" then ()
1506 else raise error "rational.sml: -1 / (3 + y) norm_Rational";
1508 (*SRD Schalk I, p.69 Nr. 456b *)
1510 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1511 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1513 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1514 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1516 (*SRD Schalk I, p.69 Nr. 457b *)
1518 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1519 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1522 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1524 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1526 "----- Schalk I, p.69 Nr. 458b works since 0707";
1528 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1529 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1530 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
1531 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39b";
1533 (*SRD Schalk I, p.69 Nr. 459b *)
1534 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1535 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1536 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
1537 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1540 (*Schalk I, p.69 Nr. 460b nonterm.SK
1542 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1543 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1546 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1549 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1550 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1551 ... non terminating.
1552 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1553 "(-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)";
1554 val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1555 ... non terminating.*)
1557 (*SRD Schalk I, p.70 Nr. 472a *)
1558 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1559 \((4*x - 8*y)/(x + y))";
1560 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1565 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1568 (*----------------------------------------------------------------------*)
1569 (*---------------------- Einfache Dppelbrche --------------------------*)
1570 (*----------------------------------------------------------------------*)
1572 (*SRD Schalk I, p.69 Nr. 461a *)
1574 "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1575 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1580 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1582 (*SRD Schalk I, p.69 Nr. 464b *)
1584 "(a - a/(a - 2)) / (a + a/(a - 2))";
1585 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1588 "(3 + -1 * a) / (1 + -1 * a)"
1590 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1592 (*SRD Schalk I, p.69 Nr. 465b *)
1594 "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1595 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1598 "(4 * x + 6 * y + -9 * z) / (4 * x)"
1600 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1602 (*SRD Schalk I, p.69 Nr. 466b *)
1604 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1605 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1608 "(25 + -10 * x + x ^^^ 2) / 18"
1610 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1612 (*SRD Schalk I, p.70 Nr. 469 *)
1614 "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))";
1615 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1618 "3 * b ^^^ 3 / (2 * a + -2 * b)"
1620 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1622 (*----------------------------------------------------------------------*)
1623 (*---------------------- Mehrfache Dppelbrueche ------------------------*)
1624 (*----------------------------------------------------------------------*)
1626 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1627 (*WN060419 crashes with method 'simplify' ????SK*)
1629 "((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)";
1630 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1631 if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
1632 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1634 "----- Schalk I, p.70 Nr. 477a";
1635 (* MG Achtung: terme explodieren; Bsp zu komplex;
1636 L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1637 val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /\
1638 \(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1639 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1642 val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / \
1643 \((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
1644 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1648 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
1649 val t = str2term "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / \
1650 \((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1651 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1653 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1655 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1657 (* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
1658 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 ()
1659 else raise error "rational.sml: works again";
1660 re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
1664 (*Schalk I, p.70 Nr. 480a *)
1665 (* Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831 nonterm.SK00
1667 "(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)))";
1668 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1673 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1675 (*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
1677 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
1678 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1680 "(x ^^^ 2 * y ^^^ 2 * z + x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2) /
1681 (-1 * x ^^^ 2 * y ^^^ 2 * z + -1 * x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2)";
1683 "2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z))";
1684 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1688 (* SK 1. Ausdruck kann nicht weiter gekrzt werden; cancel_p !!!*)
1689 ### rls: cancel_p on:
1690 (x ^^^ 2 * (y ^^^ 2 * z) + x ^^^ 2 * (y * z ^^^ 2) + x * (y ^^^ 2 * z ^^^ 2)) /
1691 (-1 * (x ^^^ 2 * (y ^^^ 2 * z)) + -1 * (x ^^^ 2 * (y * z ^^^ 2)) + x * (y ^^^ 2 * z ^^^ 2))
1692 GC #3.61.81.101.197.17503: (0 ms)
1693 *** RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction
1696 "(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))";
1697 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1699 (*uncaught exception nonexhaustive binding failure*)
1701 (* Das kann er aber krzen !!????: *)
1703 "(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1704 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1706 "(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1714 (*--------------------------------------------------------------------*)
1715 (*----------------------- Problem-Beispiele --------------------------*)
1716 (*--------------------------------------------------------------------*)
1718 (*Schalk I, p.60 Nr. 215d *)
1719 (* Achtung: rechnet ewig ...
1720 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1721 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1722 term2str t; noterm.SK
1725 (* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
1727 val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1728 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1730 "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";
1731 val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
1732 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1734 "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";
1736 (*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1738 (*--------------------------------------------------------------------*)
1739 (*Schalk I, p.70 Nr. 480b
1740 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1741 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1742 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1743 \(20*x*y/(x^^^2 - 25*y^^^2))";
1744 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1746 Kann nicht weiter vereinfacht werden !!!!?? *)
1748 (*--------------------------------------------------------------------*)
1749 "---- MGs test set";
1750 val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
1751 val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
1752 if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
1753 else raise error "";
1755 (*--------------------------------------------------------------------*)
1756 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
1757 ---> Sortierung FALSCH !! *)
1758 val t = str2term "b^^^3 * a^^^5/a ";
1759 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1761 "1 * (a^^^4 * b^^^3) / 1"; (*OK*)
1763 val t = str2term "b^^^3 * a^^^5/b ";
1764 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1766 "1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
1768 (* Problem liegt NICHT bei ord_make_polynomial! (siehe folgende Bsple) *)
1770 val x = str2term "x"; val bdv = str2term "bdv";
1771 val t1 = str2term "b^^^2 * a^^^5";
1772 val t2 = str2term "a^^^5 * b^^^2 ";
1773 ord_make_polynomial false Rational.thy [(x,bdv)] (t1,t2); (*false*)
1775 (* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
1777 (*--------------------------------------------------------------------*)
1778 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
1779 ---> erzeugt berflssige "1 * ..."
1781 val t = str2term "-1 / (3 + y)";
1783 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1786 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1787 (* -1 im Z???ler der Angabe verursacht das Problem !*)
1790 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1791 "----- MGs test set";
1792 val t = str2term "(a^^^2 + -1)/(a+1)";
1793 val SOME (t',_) = rewrite_set_ thy false cancel_p t;
1794 if term2str t' = "(-1 + a) / 1" then ()
1795 else raise error "rational.sml MG tests 3d";
1797 "----- NOT TERMINATING ?: worked before 0707xx";
1798 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1799 val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
1800 if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
1801 else raise error "rational.sml MG tests 3e";
1803 "----- corrected SK060905";
1804 val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1805 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1806 if term2str t' = "-1 / (5 + -2 * x)" then ()
1807 else raise error "rational.sml corrected SK060905";
1810 "--------------------------------------------------------------------";
1811 "----------------------- Muster-Beispiele fuer DA -------------------";
1812 "--------------------------------------------------------------------";
1814 (*SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1816 "(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))";
1817 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1820 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
1822 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
1824 "-------- me Schalk I No.186 -------------------------------------";
1825 "-------- me Schalk I No.186 -------------------------------------";
1826 "-------- me Schalk I No.186 -------------------------------------";
1827 val fmz = ["term ((14 * x * y) / ( x * y ))",
1830 ("Rational.thy",["rational","simplification"],
1831 ["simplification","of_rationals"]);
1832 val p = e_pos'; val c = [];
1833 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1834 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1835 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1836 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1837 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1838 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1839 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1840 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1841 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1842 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1843 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1844 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1845 case (f2str f, nxt) of
1846 ("14", ("End_Proof'", _)) => ()
1847 | _ => raise error "rational.sml diff.behav. in me Schalk I No.186";
1850 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1851 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1852 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
1855 [(["term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1856 ("Rational.thy",["rational","simplification"],
1857 ["simplification","of_rationals"]))];
1860 autoCalculate 1 CompleteCalc;
1861 val ((pt,p),_) = get_calc 1; show_pt pt;
1863 interSteps 1 ([1],Res);
1864 val ((pt,p),_) = get_calc 1; show_pt pt;
1867 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1868 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1869 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
1872 [(["term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1873 ("Rational.thy",["rational","simplification"],
1874 ["simplification","of_rationals"]))];
1877 autoCalculate 1 CompleteCalc;
1878 val ((pt,p),_) = get_calc 1; show_pt pt;
1879 (*with explicit script done already... and removed [1,..] at below...
1880 interSteps 1 ([1],Res);
1881 val ((pt,p),_) = get_calc 1; show_pt pt;
1883 interSteps 1 ([2],Res);
1884 val ((pt,p),_) = get_calc 1; show_pt pt;
1886 interSteps 1 ([2,1],Res);
1887 val ((pt,p),_) = get_calc 1; show_pt pt;
1888 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1889 (*if length newnds = 12 then () WN060905*)
1890 if length newnds = 13 then ()
1891 else raise error "rational.sml: interSteps cancel_p rev_rew_p";
1893 val p = ([2,1,9],Res);
1895 val (_, tac, _) = pt_extract (pt, p);
1896 (*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
1898 case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
1899 | _ => raise error "rational.sml: getTactic, sym_real_plus_binom_times1";
1902 "-------- investigate rulesets for cancel_p ----------------------";
1903 "-------- investigate rulesets for cancel_p ----------------------";
1904 "-------- investigate rulesets for cancel_p ----------------------";
1905 val thy = Rational.thy;
1906 "---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1907 val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1908 val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
1909 "----- with rewrite_set_";
1910 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1911 term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*);
1912 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
1913 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1914 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
1916 "----- with make_deriv";
1917 val SOME (tt, _) = factout_p_ Isac.thy t; term2str tt =
1918 "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
1920 "--- with ruleset as before 060829";
1921 val {rules, rew_ord=(_,ro),...} =
1922 rep_rls (assoc_rls "make_polynomial");
1923 val der = make_deriv thy Atools_erls rules ro NONE tt;
1924 print_depth 99; map (term2str o #1) der; print_depth 3;
1925 print_depth 99; map (rule2str o #2) der; print_depth 3;
1926 ... did not terminate"*)
1927 "--- with simpler ruleset";
1928 val {rules, rew_ord=(_,ro),...} =
1929 rep_rls (assoc_rls "rev_rew_p");
1930 val der = make_deriv thy Atools_erls rules ro NONE tt;
1931 print_depth 99; writeln (deriv2str der); print_depth 3;
1933 print_depth 99; map (term2str o #1) der; print_depth 3;
1934 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
1935 print_depth 99; map (rule2str o #2) der; print_depth 3;
1936 print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
1938 val der = make_deriv thy Atools_erls rules ro NONE
1939 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1940 print_depth 99; writeln (deriv2str der); print_depth 3;
1942 val {rules, rew_ord=(_,ro),...} =
1943 rep_rls (assoc_rls "rev_rew_p");
1944 val der = make_deriv thy Atools_erls rules ro NONE
1945 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1946 print_depth 99; writeln (deriv2str der); print_depth 3;
1947 print_depth 99; map (term2str o #1) der; print_depth 3;
1948 (*WN060829 ...postponed*)
1951 "-------- investigate format of factout_ and factout_p_ ----------";
1952 "-------- investigate format of factout_ and factout_p_ ----------";
1953 "-------- investigate format of factout_ and factout_p_ ----------";
1954 val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
1955 val (thy, eval_rls) = (Rational.thy, Atools_erls)(*see 'fun init_state'*);
1956 val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
1958 "----- see Rational.ML, local cancel_p, fun init_state";
1959 val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
1960 val SOME (t',_) = factout_p_ thy t; term2str t';
1962 val rtas = reverse_deriv thy eval_rls rules ro NONE t';
1963 writeln(trtas2str rst);
1967 "----- see Rational.ML, local cancel_p, fun init_state";
1968 val t = str2term "a^^^2 / a";
1969 val SOME (t',_) = factout_p_ thy t;
1970 term2str t' = "a * a / (1 * a)" (*true*);
1971 (*... can be canceled with
1972 real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
1973 (* sml/ME/rewtools.sml:
1974 val rtas = reverse_deriv thy Atools_erls rules ro NONE t';
1975 writeln (deri2str rtas);
1980 "-------- SK 060904 ----------------------------------------------";
1981 "-------- SK 060904 ----------------------------------------------";
1982 "-------- SK 060904 ----------------------------------------------";
1983 "----- order on polynomials -- input + output";
1985 val t = str2term "(a + -1 * b) / (-1 * a + b)";
1986 val SOME (t', _) = factout_p_ thy t; term2str t';
1987 val SOME (t', _) = cancel_p_ thy t; term2str t';
1989 val t = str2term "a*b*c*d / (d*e*f*g)";
1990 val SOME (t', _) = cancel_p_ thy t; term2str t';
1992 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
1993 val SOME (t', _) = cancel_p_ thy t; term2str t';
1996 "----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
1997 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
1998 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1999 if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
2000 else raise error "rational.sml SK060904-1a worked since 0707xx";
2002 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
2003 val t = str2term "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\
2004 \(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))";
2005 val SOME (t',_) = cancel_p_ thy t;
2006 if term2str t' = "1 / (4 * c + 3 * e)" then ()
2007 else raise error "rational.sml SK060904-1b";
2010 "----- SK060904-2a non-termination of add_fraction_p_";
2011 val t = str2term " (a + b * x) / (a + -1 * (b * x)) + \
2012 \ (-1 * a + b * x) / (a + b * x) ";
2014 val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
2016 common_nominator_p_ thy t;
2017 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + \
2018 \ (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
2020 add_fraction_p_ thy t;
2021 " ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /\
2022 \ ((a + b * x)*(-1 * a + b * x)) ";