prepare for SK; rev.rew. postponed until rewrite to lrd is possible
3 Copyright (c) Stefan Karnel 2002
4 Use is subject to license terms.
6 use"../smltest/IsacKnowledge/rational.sml";
10 (******************************************************************
11 WN060104 transfer marked (*SR..*)examples to the exp-collection
12 # exp_IsacCore_Simp_Rat_Cancel.xml from rational.sml (*SRC*) 10 exp
13 # exp_IsacCore_Simp_Rat_Add.xml from rational.sml (*SRA*) 11 exp
14 # exp_IsacCore_Simp_Rat_Mult.xml from rational.sml (*SRM*) 5 exp
15 # exp_IsacCore_Simp_Rat_AddMult.xml from rational.sml (*SRAM*) 11 exp
16 # exp_IsacCore_Simp_Rat_Double.xml from rational.sml (*SRD*) 12 exp
17 *******************************************************************)
18 "-----------------------------------------------------------------";
19 "table of contents -----------------------------------------------";
20 "-----------------------------------------------------------------";
21 "-------- ... missing WN060103 -----------------------------------";
22 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
23 "-------- common_nominator_p ---------------------------- --------";
24 "-------- reverse rewrite ----------------------------------------";
25 "-------- 'reverse-ruleset' cancel_p -----------------------------";
26 "-------- norm_Rational ------------------------------------------";
27 "-------- numeral rationals --------------------------------------";
28 "-------- cancellation -------------------------------------------";
29 "-------- common denominator -------------------------------------";
30 "-------- multiply and cancel ------------------------------------";
31 "-------- common denominator and multiplication ------------------";
32 "-------- double fractions ---------------------------------------";
33 "-------- me Schalk I No.186 -------------------------------------";
34 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
35 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
36 "-----------------------------------------------------------------";
37 "-----------------------------------------------------------------";
38 "-----------------------------------------------------------------";
41 (*. tests of internal functions: to make them work,
42 out-comment (*!!!*) in knowledge/Rational.ML:
44 structure RationalI : RATIONALI =
53 print("\n\n********************* rational.sml - TESTS *************************\n\n");
54 print("\n\n***** divide tests *****\n");
55 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_)));
56 (* result: [(1,[0,0,1]),(1,[0,0,0])] *)
57 if mv_pquot1=[(1,[0,0,1]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
59 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_)));
60 (* result: [(1,[1,0,1]),(~1,[0,0,1])] *)
61 if mv_prest1=[(1,[1,0,1]),(~1,[0,0,1])] then () else raise error ("rational.sml: example failed");
63 val mv_pquot2 = (#1(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
64 (* result: [(4,[1]),(4,[0])] *)
65 if mv_pquot2=[(4,[1]),(4,[0])] then () else raise error ("rational.sml: example failed");
67 val mv_prest2 = (#2(mv_division([(4,[2]),(8,[1]),(16,[0])],[(1,[1]),(1,[0])],LEX_)));
68 (* result: [(12,[0]] *)
69 if mv_prest2=[(12,[0])] then () else raise error ("rational.sml: example failed");
71 val mv_pquot3 = (#1(mv_division([(4,[2]),(~4,[0])],[(2,[1]),(2,[0])],LEX_)));
72 (* [(2,[1]),(~2,[0])] *)
73 if mv_pquot3=[(2,[1]),(~2,[0])] then () else raise error ("rational.sml: example failed");
75 val mv_prest3 = (#2(mv_division([(1,[2]),(~1,[0])],[(2,[1]),(2,[0])],LEX_)));
76 (* [(1,[2]),(~1,[0])] *)
77 if mv_prest3=[(1,[2]),(~1,[0])] then () else raise error ("rational.sml: example failed");
79 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_)));
81 if mv_pquot4=[(1,[0,1,1])] then () else raise error ("rational.sml: example failed");
83 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_)));
84 (* [(1,[1,1,1]),(~4,[0,1,2]),(4,[1,0,1]),(3,[0,0,1])] *)
85 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");
87 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_)));
88 (* [(1,[2,2,0]),(6,[2,1,2]),(3,[1,1,0]),(4,[1,0,0]),(4,[0,4,0]),(3,[0,0,0])]*)
89 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");
91 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_)));
93 if mv_prest5=[] then () else raise error ("rational.sml: example failed");
95 (* (x^2 + 2(a+1)x + (a^2+2a+1)) / (x+a+1) = x+a+1 *)
96 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_)));
97 if mv_pquot6=[(1,[1,0,0]),(1,[0,1,0]),(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
99 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_)));
100 if mv_prest6=[] then () else raise error ("rational.sml: example failed");
103 print("\n\n***** MV_CONTENT-TESTS *****\n");
104 val mv_cont1=mv_content([(1,[2,1]),(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
105 (* [(1,[0,1]),(1,[0,0])] *)
106 if mv_cont1=[(1,[0,1]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
108 val mv_pp1=mv_pp([(1,[1,1]),(1,[1,0]),(1,[0,1]),(1,[0,0])]);
109 (*[(1,[1,0]),(1,[0,0])]*)
110 if mv_pp1=[(1,[1,0]),(1,[0,0])] then () else raise error ("rational.sml: example failed");
112 val mv_cont2=mv_content([(2,[1]),(4,[0])]);
114 if mv_cont2=[(2,[0])] then () else raise error ("rational.sml: example failed");
116 val mv_pp2=mv_pp([(2,[1]),(4,[0])]);
117 (* [(1,[1]),(2,[0])] *)
118 if mv_pp2=[(1,[1]),(2,[0])] then () else raise error ("rational.sml: example failed");
120 val mv_cont3=mv_content[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
122 if mv_cont3=[(2,[0,0,0])] then () else raise error ("rational.sml: example failed");
124 val mv_pp3=mv_pp[(8,[2,1,1]),(12,[1,0,2]),(10,[2,2,0]),(16,[1,1,1])];
125 (* [(5,[2,2,0]),(4,[2,1,1]),(8,[1,1,1]),(6,[1,0,2])] *)
126 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");
128 val mv_cont4=mv_content[(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
130 if mv_cont4=[(1,[0,0,0])] then () else raise error ("rational.sml: example failed");
132 val mv_pp4=mv_pp [(2,[2,1,0]),(3,[1,0,1]),(2,[1,1,0]),(3,[0,0,1])];
133 (* [(2,[2,1,0]),(2,[1,1,0]),(3,[1,0,1]),(3,[0,0,1])] *)
134 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");
136 val con1=mv_content([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
138 if con1=[(3,[0,0])] then () else raise error ("rational.sml: example failed");
140 val pp1=mv_pp([(9,[2,0]),(15,[1,1]),(12,[1,0]),(6,[0,2]),(12,[0,1])]);
141 (* [(3,[2,0]),(5,[1,1]),(4,[1,0]),(2,[0,2]),(4,[0,1])] *)
142 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");
144 val con2=mv_content([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
146 if con2=[(1,[0,0])] then () else raise error ("rational.sml: example failed");
148 val pp2 =mv_pp([(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])]);
149 (* [(1,[2,0]),(1,[1,1]),(1,[1,0]),(1,[0,2]),(1,[0,1])] *)
150 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");
152 val cont1 = mv_content [(1,[2,1,0]),(2,[2,1,0])];
154 if cont1=[(3,[0,1,0])] then () else raise error ("rational.sml: example failed");
156 val pp1 = mv_pp [(1,[2,1,0]),(2,[2,1,0])];
158 if pp1=[(1,[2,0,0])] then () else raise error ("rational.sml: example failed");
160 val cont2 = mv_content [(4,[1,2,0]),(2,[2,1,0])];
162 if cont2=[(2,[0,1,0])] then () else raise error ("rational.sml: example failed");
164 val pp2 = mv_pp [(4,[1,2,0]),(2,[2,1,0])];
165 (* [(1,[2,0,0]),(2,[1,1,0])] *)
166 if pp2=[(1,[2,0,0]),(2,[1,1,0])] then () else raise error ("rational.sml: example failed");
168 print("\n\n\n\n********************************************************\n\n");
169 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])];
170 if cont3=[(5,[0,2,1]),(4,[0,2,0]),(2,[0,1,1])] then () else raise error ("rational.sml: example failed");
171 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])];
173 ---------------------------------------------------------------------------*)
175 fun parse_rat str = (term_of o the o (parse thy)) str;
177 print("\n\n***** mv_gcd-tests *****\n");
178 val ggt1 = mv_gcd [(4,[2,2]),(8,[1,1]),(4,[0,0])] [(2,[1,1]),(2,[0,0])];
179 (* [(2,[1,1]),(2,[0,0])] *)
180 if ggt1=[(2,[1,1]),(2,[0,0])] then () else raise error ("rational.sml: example failed");
182 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])];
183 (* [(2,[1,1,0]),(3,[0,0,1])] *)
184 if ggt2=[(2,[1,1,0]),(3,[0,0,1])] then () else raise error ("rational.sml: example failed");
187 val ggt3 = mv_gcd [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
188 (* [(1,[1,0]),(~1,[0,1])] *)
189 if ggt3=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
192 val ggt4 = mv_gcd [(1,[2,1,0]),(2,[2,1,0])] [(5,[1,0,0])];
194 if ggt4=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
197 val ggt5 = mv_gcd [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
198 (* [(1,[1,0]),(~1,[0,1])] *)
199 if ggt5=[(1,[1,0]),(~1,[0,1])] then () else raise error ("rational.sml: example failed");
202 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])];
204 if ggt6=[(1,[1,0,0])] then () else raise error ("rational.sml: example failed");
206 print("\n\n***** kgv-tests *****\n");
207 val kgv1=mv_lcm [(10,[])] [(15,[])];
209 if kgv1=[(30,[])] then () else raise error ("rational.sml: example failed");
211 val kgv2=mv_lcm [(1,[2,0]),(~2,[1,1]),(1,[0,2])] [(1,[1,0]),(~1,[0,1])];
212 (* [(1,[2,0]),(~2,[1,1]),(1,[0,2])] *)
213 if kgv2=[(1,[2,0]),(~2,[1,1]),(1,[0,2])] then () else raise error ("rational.sml: example failed");
215 val kgv3=mv_lcm [(4,[2,0]),(~8,[1,1]),(4,[0,2])] [(1,[2,0]),(~1,[0,2])];
216 (* [(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] *)
217 if kgv3=[(4,[3,0]),(~4,[2,1]),(~4,[1,2]),(4,[0,3])] then () else raise error ("rational.sml: example failed");
220 print("\n\n***** STEP_CANCEL_TESTS: *****\n");
222 val term2 = (term_of o the o (parse thy)) " (9 * a^^^2 * b) / (6 * a * c)";
223 val div2 = term2str (step_cancel term2);
224 if div2 = "3 * (a * b) * (3 * a) / (2 * c * (3 * a))" then () else raise error ("rational.sml: example failed");
227 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";
228 val div1 = term2str(step_cancel term1);
229 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");
231 val term3 = (term_of o the o (parse thy)) "(10 * a^^^2 * b * c) / (1 * x * y * z) ";
232 val div3 = term2str(step_cancel term3);
233 if div3="10 * a ^^^ 2 * b * c / (1 * x * y * z)" then () else raise error ("rational.sml: example failed");
235 --------------------------------------------------------------------------!!!*)
237 (*-----versuche 13.3.03-----
238 val t = str2term "1 - x^^^2 - 5 * x^^^5";
239 val vs=(((map free2str) o vars) t);
240 val Some ml = expanded2poly t vs;
242 poly2term'(rev(sort (mv_geq LEX_) (ml)),vs);
243 poly2term'([(~5,[5]),(~1,[2]),(1,[0])], vs);
244 monom2term((~5,[5]),vs);
245 monom2term((~1,[2]),vs);
246 val t' = monom2term((1,[0]),vs);(*uncaught exception LIST*)
248 val (i,is) = (~1,[2]);
249 val ttt = Const ("op *", [HOLogic.realT,HOLogic.realT]---> HOLogic.realT) $
250 (Const ("uminus", HOLogic.realT --> HOLogic.realT) $
251 Free ((str_of_int o abs) i, HOLogic.realT)) $
252 powerproduct2term(is, vs);
254 -------versuche 13.3.03-----*)
256 val t = str2term "1 - x^^^2 - 5 * x^^^5";
257 val Some t' = expanded2polynomial t; term2str t';
258 "1 + - 1 * x ^^^ 2 + - 5 * x ^^^ 5";
259 val t = str2term "1 - x";
260 val Some t' = expanded2polynomial t; term2str t';
262 val t = str2term "1 + (-1) * x";
263 val Some t' = expanded2polynomial t; term2str t';
265 val t = (term_of o the o (parse thy)) "1 + (-1) * x ^^^ 2 + (-5) * x ^^^5";
266 val Some t' = polynomial2expanded t; term2str t';
267 "1 - x ^^^ 2 - 5 * x ^^^ 5";
270 " external calculating functions test ";
271 " external calculating functions test ";
272 " external calculating functions test ";
274 val t1 = (term_of o the o (parse thy)) "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
275 val Some (t1',asm)= factout_p_ thy t1;
276 term2str t1'; terms2str asm;
277 "(3 + 3 * x) * (1 + 1 * x) / (2 * (1 + 1 * x))";
279 val Some (t1',asm)= cancel_p_ thy t1;
280 term2str t1'; terms2str asm;
282 "[\"1 + 1 * x ~= 0\"]";
284 val t = (term_of o the o (parse thy)) "((-3 * x^^^2 + 6 *x - 3) / (2*x - 2))";
285 val Some (t',asm)= cancel_ thy t;
286 term2str t'; terms2str asm;
289 val Some (t',asm)= factout_ thy t;
290 term2str t'; terms2str asm;
291 "(3 - 3 * x) * (-1 + x) / (2 * (-1 + x))";
294 val t = str2term "((x+ (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
295 val Some (t',asm) = add_fraction_p_ thy t;
296 term2str t'; terms2str asm;
297 "(2 + 2 * x ^^^ 2) / (-1 + 1 * x ^^^ 2)";
299 val Some (t',asm) = common_nominator_p_ thy t;
300 term2str t'; terms2str asm;
301 "(-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))";
304 val t = str2term "((x - 1) / (x + 1)) + ((x + 1) / (x - 1))";
305 val Some (t',asm) = add_fraction_ thy t;
306 term2str t'; terms2str asm;
307 "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)";
309 val Some (t',asm) = common_nominator_ thy t;
310 term2str t'; terms2str asm;
311 "(-1 + x) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(1 + x) * (1 + x) / ((1 + x) * (-1 + x))";
314 val t = str2term "((1) / (2*x + 2)) + ((1) / (2*x + (-2))) + ((1) / ( x^^^2 + (-1)))+((1) / (x^^^2 + (-2)*x + 1))";
315 val Some (t',asm) = common_nominator_p_ thy t;
316 term2str t'; terms2str asm;
317 "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 * (#";
319 val Some (t',asm) = add_fraction_p_ thy t;
320 term2str t'; terms2str asm;
321 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
322 "[\"1 + 1 * x ~= 0\"]";
323 val Some(t',asm) = norm_rational_ thy t;
324 term2str t'; terms2str asm;
325 "1 * x / (1 + -2 * x + 1 * x ^^^ 2)";
326 "[\"1 + 1 * x ~= 0\"]";
328 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))";
329 val Some (t3',_) = common_nominator_ thy t3;
330 val Some (t3'',_) = add_fraction_ thy t3;
334 val Some(t4,t5) = norm_expanded_rat_ thy t3;
340 val t=(term_of o the o (parse thy)) "(9 - x^^^2)/(9 - 6*x + x^^^2)";
341 val Some (t',_) = factout_ thy t;
342 val Some (t'',_) = cancel_ thy t;
345 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
348 val t=(term_of o the o (parse thy))
349 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1 / (3 - x)";
350 val Some (t',_) = common_nominator_ thy t;
351 val Some (t'',_) = add_fraction_ thy t;
354 "(9 - x ^^^ 2) / ((3 - x) * (3 - x)) + 1 * (3 - x) / ((3 - x) * (3 - x))";
357 (*WN.16.10.02 hinzugef"ugt -----vv---*)
358 val t=(term_of o the o (parse thy))
359 "(9 - x^^^2) / (9 - 6*x + x^^^2) + 1";
360 val Some (t',_) = common_nominator_ thy t;
361 val Some (t'',_) = add_fraction_ thy t;
364 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\
365 \1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
368 val t=(term_of o the o (parse thy))
369 "1 + (9 - x^^^2) / (9 - 6*x + x^^^2)";
370 val Some (t',_) = common_nominator_ thy t;
371 val Some (t'',_) = add_fraction_ thy t;
374 "1 * (9 - 6 * x + x ^^^ 2) / (9 - 6 * x + x ^^^ 2) +\
375 \(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
377 (*WN.16.10.02 hinzugef"ugt -----^^---*)
378 (*WN.2.6.03 added -------vv--- no rewrite -> None !*)
379 val t = str2term "1 / a";
380 val None = cancel_p_ thy t;
381 val None = rewrite_set_ thy false cancel_p t;
382 (*WN.2.6.03 added -------^^---*)
384 val t=(term_of o the o (parse thy))
385 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
386 val Some (t',_) = factout_ thy t;
387 val Some (t'',_) = cancel_ thy t;
390 "(y + x) * (y - x) / ((y - x) * (y - x))";
393 val t=(term_of o the o (parse thy))
394 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2) + 1 / (y - x)";
395 val Some (t',_) = common_nominator_ thy t;
396 val Some (t'',_) = add_fraction_ thy t;
399 "((-1) * x ^^^ 2 + y ^^^ 2) / (((-1) * x + y) * ((-1) * x + y)) +\
400 \1 * ((-1) * x + y) / (((-1) * x + y) * ((-1) * x + y))";
401 "((-1) - x - y) / (x - y)";
402 (*WN.16.10.02 ^^^^^^^ Reihenfolge aus Angabe umgekehrt ?!*)
404 val t=(term_of o the o (parse thy))
405 "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
406 val Some (t',_) = common_nominator_ thy t;
407 val Some (t'',_) = add_fraction_ thy t;
410 "((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
411 \1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
412 "((-1) - y - x) / (y - x)";
413 (*WN.16.10.02 ^^^^^^^ lexicographische Ordnung ?!*)
415 val t=(term_of o the o (parse thy))
416 "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
417 val Some (t',_) = norm_expanded_rat_ thy t;
420 (*val Some (t'',_) = norm_rational_ thy t;
422 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
425 val t=(term_of o the o (parse thy))
426 "(9 - x^^^2)/(9 - 6*x + x^^^2) + (1)/(3 + x)";
427 val Some (t',_) = norm_expanded_rat_ thy t;
429 "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
430 (*val Some (t'',_) = norm_rational_ thy t;
432 *** RATIONALS_TERM2POLY_EXCEPTION: Invalid Polynomial
435 val t=(term_of o the o (parse thy))
436 "(9 + (-1)* x^^^2)/(9 + (-1)* 6*x + x^^^2) + (1)/(3 + x)";
437 val Some (t',_) = norm_expanded_rat_ thy t;
438 val Some (t'',_) = norm_rational_ thy t;
441 "(12 + 5 * x + x ^^^ 2) / (9 - x ^^^ 2)";
442 "(12 + 5 * x + x ^^^ 2) / (9 + (-1) * x ^^^ 2)";
445 " examples from: Mathematik 1 Schalk Reniets Verlag ";
446 " examples from: Mathematik 1 Schalk Reniets Verlag ";
447 " examples from: Mathematik 1 Schalk Reniets Verlag ";
450 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
451 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
452 "-------- cancel from: Mathematik 1 Schalk Reniets Verlag --------";
453 val thy' = "Rational.thy";
455 val mp = "make_polynomial";
457 print("\n\nexample 186:\n");
459 val e186a'="(14 * x * y) / ( x * y )";(*SRC*)
460 val e186a = the (rewrite_set thy' false "cancel" e186a');
461 is_expanded (parse_rat "14 * x * y");
462 is_expanded (parse_rat "x * y");
465 val e186b'="(60 * a * b) / ( 15 * a * b )";
466 val e186b = the (rewrite_set thy' false "cancel" e186b');
468 val e186c'="(144 * a^^^2 * b * c) / (12 * a * b * c )";
469 val e186c = (the (rewrite_set thy' false "cancel" e186c'))
470 handle e => print_exn e;
471 val t = (term_of o the o (parse thy)) e186c';
474 print("\n\nexample 187:\n");
476 val e187a'="(12 * x * y) / (8 * y^^^2 )";(*SRC*)
477 val e187a = the (rewrite_set thy' false "cancel" e187a');
479 val e187b'="(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
480 val e187b = the (rewrite_set thy' false "cancel" e187b');
482 val e187c'="(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";(*SRC*)
483 val e187c = the (rewrite_set thy' false "cancel" e187c');
486 val e188a'="(-8 + 8 * x) / (-9 + 9 * x)";(*SRC*)
487 val e188a = the (rewrite_set thy' false "cancel" e188a');
488 is_expanded (parse_rat "8 * x + -8");
489 (* e188a = ("8 / 9",["not ((-1) + x = 0)"]) then () 13.3.03*)
490 if e188a = ("8 / 9",["-1 + x ~= 0"]) then ()
491 else raise error "rational.sml: e188a new behaviour";
492 val Some (t,_) = rewrite_set thy' false mp
493 "(8*((-1) + x))/(9*((-1) + x))";
495 val e188b'="(-15 + 5 * x) / (-18 + 6 * x)";(*SRC*)
496 val Some (t,_) = rewrite_set thy' false "cancel" e188b';
499 val e188c'="( a + -1 * b ) / ( b + -1 * a )";
500 val e188c = the (rewrite_set thy' false "cancel" e188c');
501 is_expanded (parse_rat "a + -1 * b");
502 false; -----------!!!*)
504 rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
505 if t= "(a + -1 * b) / (-1 * a + b)" then()
506 else raise error "rational.sml: e188c new behaviour";
508 print("\n\nexample 190:\n");
510 val e190c'="( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
511 val e190c = the (rewrite_set thy' false "cancel" e190c');
512 val Some (t,_) = rewrite_set thy' false mp "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
513 if t = "(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)" then ()
514 else raise error "rational.sml: e190c new behaviour";
516 print("\n\nexample 191:\n");
518 val e191a'="( x^^^2 + -1 * y^^^2 ) / ( x + y )";
520 val e191a = the (rewrite_set thy' false "cancel" e191a');
521 is_expanded (parse_rat "x^^^2 + -1 * y^^^2");
523 is_expanded (parse_rat "x + y");
525 val Some (t,_) = rewrite_set thy' false mp "((x + (-1) * y)*(x + y))/((1)*(x + y))";
526 (* t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then() WN.13.3.03*)
527 if t="(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)" then()
528 else raise error "rational.sml: e191a new behaviour";
531 val e191c'="( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
533 val e191c = the (rewrite_set thy' false "cancel" e191c');
534 is_expanded (parse_rat "9 * x^^^2 + -30 * x + 25");
536 is_expanded (parse_rat "25 + -30*x + 9*x^^^2");
538 is_expanded (parse_rat "-25 + 9*x^^^2");
540 val Some (t,_) = rewrite_set thy' false mp "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
541 (* t="(25 + ((-30) * x + 9 * x ^^^ 2)) / ((-25) + 9 * x ^^^ 2)"then() 13.3.03*)
542 if t= "(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)" then()
543 else raise error "rational.sml: 'e191c' new behaviour";
546 print("\n\nexample 192:\n");
548 val e192b'="( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
550 val e192b = the (rewrite_set thy' false "cancel" e192b');
551 -------------------*)
552 val Some (t',_) = rewrite_set thy' false mp "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
553 if t' = "(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)"
554 (*"(-1 * y * x ^^^ 2 + 7 * x ^^^ 3) / (-1 * y ^^^ 3 + 7 * x * y ^^^ 2)"WN050929*)
555 then () else raise error "rational.sml: 'e192b' new behaviour";
556 (*^^^ works with MG's simplifier vvv*)
557 val t =str2term"((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
558 val Some (t',_) = rewrite_set_ Isac.thy false make_polynomial t;
559 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";
562 print("\n\nexample 193:\n");
564 val e193a'="( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
566 val e193a = the (rewrite_set thy' false "cancel" e193a');
567 -------------------*)
569 val e193b'="( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
571 val e193b = the (rewrite_set thy' false "cancel" e193b');
573 val e193c'="( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
574 val Some(t,_) = rewrite_set thy' false "cancel" e193c';
575 -------------------*)
577 val wn01 = "(-25 + 9*x^^^2)/(5 + 3*x)";
578 val Some (t,_) = rewrite_set thy' false "cancel" wn01;
579 (* t = "((-5) + 3 * x) / 1" then () WN.13.3.03*)
580 if t = "(-5 + 3 * x) / 1" then ()
581 else raise error "rational.sml: new behav. in cancel wn01";
584 "-------- common_nominator_p ---------------------------- --------";
585 "-------- common_nominator_p ---------------------------- --------";
586 "-------- common_nominator_p ---------------------------- --------";
587 val rls' = "common_nominator_p";
589 print("\n\nexample 204:\n");
591 val e204a'="((5 * x) / 9) + ((3 * x) / 9) + (x / 9)";
592 val e204a = the (rewrite_set thy' false "common_nominator_p" e204a');
594 val e204b'="5 / x + -3 / x + -1 / x";
595 val e204b = the (rewrite_set thy' false "common_nominator_p" e204b');
597 print("\n\nexample 205:\n");
599 val e205a'="((4 * x + 7) / 8) + ((4 * x + 3) / 8)";
600 val e205a = the (rewrite_set thy' false "common_nominator_p" e205a');
602 val e205b'="((5 * x + 2) / 3) + ((-2 * x + 1) / 3)";
603 val e205b = the (rewrite_set thy' false "common_nominator_p" e205b');
605 print("\n\nexample 206:\n");
607 val e206a'="((5 * x + 4) / (2 * x + -1)) + ((9 * x + 5) / (2 * x + -1))";
608 val e206a = the (rewrite_set thy' false "common_nominator_p" e206a');
610 val e206b'="((17 * x + -23) / (5 * x + 4)) + ((-25 + -17 * x) / (5 * x + 4))";
611 val e206b = the (rewrite_set thy' false "common_nominator_p" e206b');
613 print("\n\nexample 207:\n");
614 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)) ";
615 val e207 = the (rewrite_set thy' false "common_nominator_p" e207');
617 print("\n\nexample 208:\n");
618 val e208'="((3 * x + 2) / (x + 2)) + ((5 * x + -1) / (x + 2)) + ((-7 * x + -3) / (x + 2)) + ((-1 * x + -3) / (x + 2)) ";
619 val e208 = the (rewrite_set thy' false "common_nominator_p" e208');
621 print("\n\nexample 209:\n");
622 val e209'="((3 * x + -7 * y + 3 * z) / (4)) + ((2 * x + 17 * y + 10 * z) / (4)) + ((-1 * x + 2 * y + z) / (4)) ";
623 val e209 = the (rewrite_set thy' false "common_nominator_p" e209');
625 print("\n\nexample 210:\n");
626 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)) ";
627 val e210 = the (rewrite_set thy' false "common_nominator_p" e210');
629 print("\n\nexample 211:\n");
631 val e211a'="((b) / (a + -1 * b)) + ((-1 * a) / (a + -1 * b))";
632 val e211a = the (rewrite_set thy' false "common_nominator_p" e211a');
634 val e211b'="((b) / (b^^^2 + -1 * a^^^2)) + ((-1 * a) / (b^^^2 + -1 * a^^^2))";
635 val e211b = the (rewrite_set thy' false "common_nominator_p" e211b');
637 print("\n\nexample 212:\n");
639 val e212a'="((4) / (x)) + ((-3) / (y)) + -1";
640 val e212a = the (rewrite_set thy' false "common_nominator_p" e212a');
642 val e212b'="((4) / (x)) + ((-5) / (y)) + ((6) / (x*y))";
643 val e212b = the (rewrite_set thy' false "common_nominator_p" e212b');
645 print("\n\nexample 213:\n");
647 val e213a'="((5 * x) / (3 * y^^^2)) + ((19 * z) / (6 * x * y)) + ((-2 * x) / (3 * y^^^2)) + ((7 * y^^^2) / (6 * x^^^2)) ";
648 val e213a = the (rewrite_set thy' false "common_nominator_p" e213a');
650 val e213b'="((2 * b) / (3 * a^^^2)) + ((3 * c) / (7 * a * b)) + ((4 * b) / (3 * a^^^2)) + ((3 * a) / (7 * b^^^2))";
651 val e213b = the (rewrite_set thy' false "common_nominator_p" e213b');
653 print("\n\nexample 214:\n");
655 val e214a'="((3 * x + 2 * y + 2 * z) / (4)) + ((-5 * x + -3 * y) / (3)) + ((x + y + -2 * z) / (2))";
656 val e214a = the (rewrite_set thy' false "common_nominator_p" e214a');
658 val e214b'="((5 * x + 2 * y + z) / (2)) + ((-7 * x + -3 * y) / (3)) + ((3 * x + 6 * y + -1 * z) / (12))";
659 val e214b = the (rewrite_set thy' false "common_nominator_p" e214b');
661 print("\n\nexample 216:\n");
663 val e216a'="((2 * b + 3 * c) / (a * c)) + ((3 * a + b) / (a * b)) + ((-2 * b^^^2 + -3 * a * c) / (a * b * c))";
664 val e216a = the (rewrite_set thy' false "common_nominator_p" e216a');
666 val e216b'="((2 * a + 3 * b) / (b * c)) + ((3 * c + a) / (a * c)) + ((-2 * a^^^2 + -3 * b * c) / (a * b * c))";
667 val e216b = the (rewrite_set thy' false "common_nominator_p" e216b');
669 print("\n\nexample 217:\n");
670 val e217'="((z + -1) / (z)) + ((3 * z ^^^2 + -6 * z + 5) / (z^^^2)) + ((-4 * z^^^3 + 7 * z^^^2 + -5 * z + 5) / (z^^^3))";
671 val e217 = the (rewrite_set thy' false "common_nominator_p" e217');
674 val rls' = "common_nominator";
675 print("\n\nexample 218:\n");
676 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))";
677 val e218 = the (rewrite_set thy' false "common_nominator" e218');
679 print("\n\nexample 219:\n");
681 val e219a'="((1) / (y + 1)) + ((1) / (y + 2)) + ((1) / (y + 3))";
682 val e219a = the (rewrite_set thy' false "common_nominator" e219a');
684 val e219b'="((1) / (x + 1)) + ((1) / (x + 2)) + ((-2) / (x + 3))";
685 val e219b = the (rewrite_set thy' false "common_nominator" e219b');
687 print("\n\nexample 220:\n");
689 val e220a'="((17) / (5 * r + -2)) + ((-13) / (2 * r + 3)) + ((4) / (3 * r + -5))";
690 val e220a = the (rewrite_set thy' false "common_nominator" e220a');
692 val e220b'="((20 * a) / (a + -3)) + ((-19 * a) / (a + -4)) + ((a) / (a + -5))";
693 val e220b = the (rewrite_set thy' false "common_nominator" e220b');
695 print("\n\nexample 221:\n");
697 val e221a'="((a + b) / (a + -1 * b)) + ((a + -1 * b) / (a + b))";
698 val e221a = the (rewrite_set thy' false "common_nominator" e221a');
700 val e221b'="((x + -1 * y) / (x + y)) + ((x + y) / (x + -1 * y)) ";
701 val e221b = the (rewrite_set thy' false "common_nominator" e221b');
703 print("\n\nexample 222:\n");
705 val e222a'="((1 + -1 * x) / (1 + x)) + ((-1 + -1 * x) / (1 + -1 * x)) + ((4 * x) / (1 + -1 * x^^^2))";
706 val e222a = the (rewrite_set thy' false "common_nominator" e222a');
708 val e222b'="((1 + x ) / (1 + -1 * x)) + ((-1 + x) / (1 + x)) + ((2 * x) / (1 + -1 * x^^^2))";
709 val e222b = the (rewrite_set thy' false "common_nominator" e222b');
711 print("\n\nexample 225:\n");
713 val e225a'="((6 * a) / (a^^^2 + -64)) + ((a + 2) / (2 * a + 16)) + ((-1) / (2))";
714 val e225a = the (rewrite_set thy' false "common_nominator" e225a');
716 val e225b'="((a + 2 ) / (2 * a + 12)) + ((4 * a) / (a^^^2 + -36)) + ((-1) / (2))";
717 val e225b = the (rewrite_set thy' false "common_nominator" e225b');
719 print("\n\nexample 226:\n");
721 val e226a'="((35 * z) / (49 * z^^^2 + -4)) + -1 + ((14 * z + -1) / (14 * z + 4)) ";
722 val e226a = the (rewrite_set thy' false "common_nominator" e226a');
724 val e226b'="((45 * a * b) / (25 * a^^^2 + -9 * b^^^2)) + ((20 * a + 3 * b) / (10 * a + 6 * b)) + -2";
725 val e226b = the (rewrite_set thy' false "common_nominator" e226b');
727 print("\n\nexample 227:\n");
729 val e227a'="((6 * z + 11) / (6 * z + 14)) + ((9 * z ) / (9 * z^^^2 + -49)) + -1 ";
730 val e227a = the (rewrite_set thy' false "common_nominator" e227a');
732 val e227b'="((16 * a + 37 * b) / (4 * a + 10 * b)) + ((6 * a * b) / (4 * a^^^2 + -25 * b^^^2)) + -4 ";
733 val e227b = the (rewrite_set thy' false "common_nominator" e227b');
735 print("\n\nexample 228:\n");
737 val e228a'="((7 * a + 11) / (3 * a^^^2 + -3)) + ((-2 * a + -1) / (a^^^2 + -1 * a)) + ((-1) / (3 * a + 3))";
738 val e228a = the (rewrite_set thy' false "common_nominator" e228a');
740 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))";
741 val e228b = the (rewrite_set thy' false "common_nominator" e228b');
744 print("\n\nexample 229:\n");
746 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))";
747 val e229a = the (rewrite_set thy' false "common_nominator" e229a');
749 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))";
750 val e229b = the (rewrite_set thy' false "common_nominator" e229b');
752 print("\n\nexample 230:\n");
754 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))";
755 val e230a = the (rewrite_set thy' false "common_nominator" e230a');
757 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))";
758 val e230b = the (rewrite_set thy' false "common_nominator" e230b');
760 print("\n\nexample 231:\n");
762 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))";
763 val e231a = the (rewrite_set thy' false "common_nominator" e231a');
765 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))";
766 val e231b = the (rewrite_set thy' false "common_nominator" e231b');
768 print("\n\nexample 232:\n");
770 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))";
771 val e232a = the (rewrite_set thy' false "common_nominator" e232a');
773 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))";
774 val e232b = the (rewrite_set thy' false "common_nominator" e232b');
776 print("\n\nexample 233:\n");
778 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))";
779 val e233a = the (rewrite_set thy' false "common_nominator" e233a');
781 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))";
782 val e233b = the (rewrite_set thy' false "common_nominator" e233b');
784 print("\n\nexample 234:\n");
786 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))";
787 val e234a = the (rewrite_set thy' false "common_nominator" e234a');
789 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)) ";
790 val e234b = the (rewrite_set thy' false "common_nominator" e234b');
792 print("\n\nexample 235:\n");
794 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))";
795 val e235a = the (rewrite_set thy' false "common_nominator" e235a');
797 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)) ";
798 val e235b = the (rewrite_set thy' false "common_nominator" e235b');
800 print("\n\nexample 236:\n");
802 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))";
803 val e236a = the (rewrite_set thy' false "common_nominator" e236a');
805 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)) ";
806 val e236b = the (rewrite_set thy' false "common_nominator" e236b');
810 print("\n\nexample heuberger:\n");
811 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)";
812 val eheu = the (rewrite_set thy' false "cancel" eheu');
814 val rls' = "common_nominator_p";
815 print("\n\nexample stiefel:\n");
816 val est1'="(7) / (-14) + (-2) / (4)";
817 val est1 = the (rewrite_set thy' false "common_nominator_p" est1');
818 if est1 = ("-1 / 1",[]) then ()
819 else raise error "new behaviour in rational.sml: est1'";
821 val t = (term_of o the o (parse thy))
822 "(9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
823 val Some (t',_) = factout_ thy t;
825 "(3 + x) * (3 - x) / ((3 - x) * (3 - x))";
828 "-------- reverse rewrite ----------------------------------------";
829 "-------- reverse rewrite ----------------------------------------";
830 "-------- reverse rewrite ----------------------------------------";
832 (*WN.28.8.02: tests for the 'reverse-rewrite' functions:
833 these are defined in Rationals.ML and stored in
834 the 'reverse-ruleset' cancel*)
836 (*the term for which reverse rewriting is demonstrated*)
837 val t = (term_of o the o (parse thy))
838 "(9 - x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
839 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
840 next_rule=nex,normal_form=nor,...},...} = cancel;
842 (*normal_form produces the result in ONE step*)
843 val Some (t',_) = nor t;
846 (*initialize the interpreter state used by the 'me'*)
847 val (t,_,revsets,_) = ini t;
849 (*find the rule 'r' to apply to term 't'*)
850 val Some r = nex revsets t;
851 (*val r = Thm ("sym_#mult_2_3","6 = 2 * 3") : rule*)
853 (*check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
854 if the rule is OK, the term resulting from applying the rule is returned,too;
855 there might be several rule applications inbetween,
856 which are listed after the head in reverse order*)
857 val (r,(t,asm))::_ = loc revsets t r;
859 "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
861 (*find the next rule to apply*)
862 val Some r = nex revsets t;
863 (*val r = Thm ("sym_#power_3_2","9 = 3 ^^^ 2") : rule*)
865 (*check the next rule*)
866 val (r,(t,asm))::_ = loc revsets t r;
868 "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)";
870 (*find and check the next rules, rewrite*)
871 val Some r = nex revsets t;
872 val (r,(t,asm))::_ = loc revsets t r;
874 "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
876 val Some r = nex revsets t;
877 val (r,(t,asm))::_ = loc revsets t r;
879 "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)";
881 val Some r = nex revsets t;
882 val (r,(t,asm))::_ = loc revsets t r;
884 "(3 - x) * (3 + x) / ((3 + x) * (3 + x))";
886 val Some r = nex revsets t;
887 val (r,(t,asm))::_ = loc revsets t r;
889 if ss = "(3 - x) / (3 + x)" then ()
890 else raise error "rational.sml: new behav. in rev-set cancel";
894 "-------- 'reverse-ruleset' cancel_p -----------------------------";
895 "-------- 'reverse-ruleset' cancel_p -----------------------------";
896 "-------- 'reverse-ruleset' cancel_p -----------------------------";
897 (*WN.11.9.02: the 'reverse-ruleset' cancel_p*)
899 (*the term for which reverse rewriting is demonstrated*)
900 val t = (term_of o the o (parse thy))
901 "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
902 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
903 next_rule=nex,normal_form=nor,...},...} = cancel_p;
905 (*normal_form produces the result in ONE step*)
906 val Some (t',_) = nor t; term2str t';
908 (*initialize the interpreter state used by the 'me'*)
909 val Some (t', asm) = cancel_p_ thy t; term2str t'; terms2str asm;
912 (* WN.14.3.03: rewrite__ Thm | Calc | missing: Rls_ FIXXXXME --------
913 val (t,_,revsets,_) = ini t;
914 ---------------------------------------------------------------------*)
918 filter_out (eq_Thms ["sym_real_add_zero_left",
920 "sym_real_mult_1"]) rs;
922 10.10.02: dieser Fall terminiert nicht
923 (make_polynomial enth"alt zu viele rules)
924 WN060823 'init_state' requires rewriting on specified location in the term
925 print_depth 99; Rfuns; print_depth 3;
928 val Some r = nex revsets t;
929 val (r,(t,asm))::_ = loc revsets t r;
932 val Some r = nex revsets t;
933 val (r,(t,asm))::_ = loc revsets t r;
936 ------ revset ----------------------------------------------------
937 /// [Thm ("sym_real_add_zero_left","?z = 0 + ?z"),
938 /// Thm ("sym_real_mult_0","0 = 0 * ?z"),
939 ! Thm ("sym_#mult_2_(-3)","(-6) * x = 2 * ((-3) * x)"),
940 ! Thm ("sym_#add_(-3)_3","0 = (-3) + 3"),
942 ? Thm ("sym_real_num_collect_assoc",
943 "[| ?l is_const; ?m is_const |]
944 ==> (?l + ?m) * ?n + ?k = ?l * ?n + (?m * ?n + ?k)"),
945 OK Thm ("sym_real_mult_2_assoc","2 * ?z1.0 + ?k = ?z1.0 + (?z1.0 + ?k)"),
946 OK Thm ("sym_real_add_left_commute","?y + (?x + ?z) = ?x + (?y + ?z)"),
947 /// Thm ("sym_real_mult_1","?z = 1 * ?z"),
948 ! Thm ("sym_#power_3_2","9 = 3 ^^^ 2"),
949 ! Thm ("sym_#mult_-1_-1","1 * x ^^^ 2 = -1 * (-1 * x ^^^ 2)"),
950 ! Thm ("sym_#mult_-1_3","(-3) * x = -1 * (3 * x)"),
951 OK Thm ("realpow_twoI","?r1 ^^^ 2 = ?r1 * ?r1" [.]),
952 OK Thm ("sym_real_add_assoc",
953 "?z1.0 + (?z2.0 + ?z3.0) = ?z1.0 + ?z2.0 + ?z3.0"),
955 ("sym_real_mult_assoc","?z1.0 * (?z2.0 * ?z3.0) = ?z1.0 * ?z2.0 * ?z3.0"),
956 OK Thm ("sym_real_mult_left_commute",
957 "?z2.0 * (?z1.0 * ?z3.0) = ?z1.0 * (?z2.0 * ?z3.0)"),
958 OK Thm ("sym_real_mult_commute","?w * ?z = ?z * ?w"),
959 ? Thm ("sym_real_add_mult_distrib2",
960 "?w * ?z1.0 + ?w * ?z2.0 = ?w * (?z1.0 + ?z2.0)"),
961 ? Thm ("sym_real_add_mult_distrib",
962 "?z1.0 * ?w + ?z2.0 * ?w = (?z1.0 + ?z2.0) * ?w"),
963 OK Thm ("real_mult_div_cancel2","?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n")]
964 -------- revset ----------------------------------------------------
966 val t = (term_of o the o (parse thy)) "(-6) * x";
967 val t = (term_of o the o (parse thy))
968 "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
969 val thm = (mk_thm thy "(-6) * x = 2 * ((-3) * x)")
970 handle e => print_exn e;
971 val Some (t',_) = rewrite_ thy e_rew_ord e_rls false thm t;
973 ----------------------------------------------------------------------*)
975 print "\n\n\n****************** all tests successfull *************************\n";
979 (*WN.17.3.03 =========================================================vvv---*)
980 "-------- norm_Rational ------------------------------------------";
981 "-------- norm_Rational ------------------------------------------";
982 "-------- norm_Rational ------------------------------------------";
983 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
984 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
985 if term2str t' = "1 / 18 = 0" then () else raise error "rational.sml 1";
987 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
988 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
989 if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
990 else raise error "rational.sml 2";
992 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
993 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
994 (*before 040209:if term2str t' = "(23 + (35 * x + -72 * x ^^^ 2)) / 1"then()*)
995 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
996 else raise error "rational.sml 3";
998 val t = str2term "Not (6*x is_atom)";
999 val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1001 val t = str2term "1 < 2";
1002 val Some (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
1004 val t = str2term "(6*x)^^^2";
1005 val Some (t',_) = rewrite_ thy dummy_ord powers_erls false
1006 (num_str realpow_def_atom) t;
1008 trace_rewrite:=false;
1010 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
1011 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1012 if term2str t' = "65 * x / 2" then () else raise error "rational.sml 4";
1014 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
1015 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1016 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
1017 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
1018 else raise error "rational.sml 5";
1020 (*SRAM Schalk I, p.92 Nr. 609a*)
1021 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
1022 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1023 if term2str t' = "(-255 + 112 * x) / 135" then ()
1024 else raise error "rational.sml 6";
1026 (*SRAM Schalk I, p.92 Nr. 610c*)
1027 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
1028 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1029 if term2str t' = "(-3 + -1 * x) / 2" then () else raise error "rational.sml 7";
1031 (*SRAM Schalk I, p.92 Nr. 476a*)
1032 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) *\
1033 \ (1 + x)";(*. a/b : c/d translated to a/b * d/c .*)
1034 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1035 (*if term2str t' = "1 / 1" then () else raise error "rational.sml 8";3.6.03*)
1036 if term2str t' = "1" then () else raise error "rational.sml 8";
1038 (*............................vvv---TODO: sollte gehen mit poly_order *)
1039 (*Schalk I, p.92 Nr. 472a*)
1040 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1041 \((4*x - 8*y)/(x + y))";
1042 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1043 "(-32 * y ^^^ 3 +\n (8 * x ^^^ 3 + (-32 * (x * y ^^^ 2) + 8 * (y * x ^^^ 2)))) /\n(-32 * y ^^^ 2 + 8 * x ^^^ 2)";
1044 (*###########################statt "x + y" poly_order notwendig!*)
1046 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
1047 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1048 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1049 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1050 \(20*x*y/(x^^^2 - 25*y^^^2))";
1051 (*... nicht simpl, zerlegt ...*)
1052 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1053 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))";
1054 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1055 "(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
1056 (* ~~~~~~~~~~ poly_order notwendig!*)
1057 val t = str2term "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1058 \(20*x*y/(x^^^2 - 25*y^^^2))";
1059 val Some (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1060 "(-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))";
1061 trace_rewrite:=true;
1062 trace_rewrite:=false;
1064 (*WN.17.3.03 =========================================================^^^---*)
1067 (*WN.2.6.03 from rlang.sml 56a =======================================vvv---*)
1068 (*... takes uncredible much time:*)
1070 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)";
1071 val None = rewrite_set_ thy false common_nominator_p t;
1073 "----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1074 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1075 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1076 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n\
1077 \----- rational.sml: add_fraction_p_ throws overflow exn ! -----\n";
1078 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1079 val None = add_fraction_p_ thy t;
1083 GC #1.48.88.223.2775.290178: (0 ms)
1084 GC #1.48.88.223.2776.290363: (0 ms)
1085 GC #1.48.88.223.2777.290712: (0 ms)
1086 GC #1.48.88.223.2778.291102: (0 ms)
1087 GC #1.48.88.223.2779.291684: (0 ms)
1088 GC #1.48.88.223.2780.292389: (0 ms)
1089 GC #1.48.88.223.2781.293163: (0 ms)
1090 GC #1.48.88.223.2782.294133: (0 ms)
1091 GC #1.48.88.223.2783.295181: (0 ms)
1093 (*WN.2.6.03 from rlang.sml 56a =======================================^^^---*)
1097 (* 25.08.03: Durchlauf(rechen)zeit: 1 min *)
1099 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
1101 (* ------------------------------------------------------------------- *)
1102 (* Simplifier für beliebige Buchterme *)
1103 (* ------------------------------------------------------------------- *)
1104 (*----------------------- norm_Rational_mg --------------------------*)
1105 (* ------------------------------------------------------------------- *)
1108 "-------- numeral rationals --------------------------------------";
1109 "-------- numeral rationals --------------------------------------";
1110 "-------- numeral rationals --------------------------------------";
1112 (*SRA Schalk I, p.40 Nr. 164b *)
1113 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
1114 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1119 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 1";
1121 (*SRA Schalk I, p.40 Nr. 166a *)
1122 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
1123 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1128 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 2";
1131 "-------- cancellation -------------------------------------------";
1132 "-------- cancellation -------------------------------------------";
1133 "-------- cancellation -------------------------------------------";
1135 (* e190c Stefan K.*)
1137 "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
1138 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1141 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1143 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 3";
1145 (* e192b Stefan K.*)
1147 "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
1148 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1153 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 4";
1155 (*SRC Schalk I, p.66 Nr. 379c *)
1158 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1163 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 5";
1165 (*SRC Schalk I, p.66 Nr. 380b *)
1167 "15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
1168 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1171 "(27 + 12 * x) / (28 + 8 * x)"
1173 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 6";
1175 (*Schalk I, p.60 Nr. 215c *)
1176 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter kürzen!!!*)
1178 "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
1179 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1182 "(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)"
1184 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 7";
1187 "(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)"
1188 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1190 (* uncaught exception nonexhaustive binding failure
1191 raised at: stdIn:93.1-93.51 *)
1193 (*Schalk I, p.66 Nr. 381a *)
1194 (* ACHTUNG: rechnet ca. 2 Minuten !!! *)
1196 "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
1197 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1200 "(a + b) / (4 * a + -4 * b)"
1202 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 8";
1205 (*SRC Schalk I, p.66 Nr. 381b *)
1207 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1208 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1213 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 9";
1215 (*SRC Schalk I, p.66 Nr. 381c *)
1217 "(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
1218 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1221 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
1223 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 10";
1225 (*SRC Schalk I, p.66 Nr. 383a *)
1227 "(5*a^^^2 - 5*a*b)/(a - b)^^^2";
1228 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1231 "5 * a / (a + -1 * b)"
1233 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 11";
1235 "-------- common denominator -------------------------------------";
1236 "-------- common denominator -------------------------------------";
1237 "-------- common denominator -------------------------------------";
1239 (*SRA Schalk I, p.67 Nr. 403a *)
1242 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1245 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
1247 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 12";
1249 (*SRA Schalk I, p.67 Nr. 407b *)
1251 "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
1252 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1257 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 13";
1259 (*SRA Schalk I, p.67 Nr. 410b *)
1261 "1/(x+1) + 1/(x+2) - 2/(x+3)";
1262 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1265 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
1267 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 14";
1269 (*SRA Schalk I, p.67 Nr. 413b *)
1271 "(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
1272 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1275 "6 * x / (1 + -1 * x ^^^ 2)"
1277 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 15";
1279 (*SRA Schalk I, p.68 Nr. 414a *)
1281 "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
1282 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1285 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
1287 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 16";
1289 (*SRA Schalk I, p.68 Nr. 423a *)
1291 "(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)";
1292 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1297 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 17";
1299 (*SRA Schalk I, p.68 Nr. 428b *)
1301 "1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
1302 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1305 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1307 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 18";
1309 (*SRA Schalk I, p.68 Nr. 430b *)
1311 "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";
1312 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1317 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 19";
1320 (*SRA Schalk I, p.68 Nr. 432 *)
1322 "(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)";
1323 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1328 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 20";
1333 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1336 "(3 * y + b * x) / (b * y)"
1338 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 21";
1341 "-------- multiply and cancel ------------------------------------";
1342 "-------- multiply and cancel ------------------------------------";
1343 "-------- multiply and cancel ------------------------------------";
1345 (*SRM Schalk I, p.68 Nr. 436a *)
1347 "3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)";
1348 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1351 "(5 * x + -5 * y) / (18 * x + 18 * y)"
1353 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 22";
1355 (*SRM.test Schalk I, p.68 Nr. 436b *)
1356 (*WN060420 crashes with method 'simplify' in
1357 IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
1358 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1359 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1362 "5 * a / (a + -1 * b)"
1364 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 23";
1366 (*Schalk I, p.68 Nr. 437a *)
1367 (* SK loops: rechnet ewig; cancel_p hängt sich auf...
1369 "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1371 rewrite_set_ thy false norm_Rational(*_mg*) t;
1376 "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1378 rewrite_set_ thy false make_polynomial t;
1380 "(9 * a ^^^ 2 + -16 * b ^^^ 2) /
1381 (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)";
1383 rewrite_set_ thy false cancel_p t;
1387 (*Schalk I, p.68 Nr. 437b *)
1388 (* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter kürzen!!!
1389 val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1390 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1392 "(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)";
1398 "(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)";
1399 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1401 uncaught exception nonexhaustive binding failure
1402 raised at: stdIn:270.1-270.51
1405 (*SRM Schalk I, p.68 Nr. 438a *)
1407 "x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
1408 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1413 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 24";
1415 (*SRM Schalk I, p.68 Nr. 439b *)
1417 "(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
1418 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1421 "(x + -4 * x ^^^ 3) / 2"
1423 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 25";
1425 (*SRM Schalk I, p.68 Nr. 440a *)
1427 "(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
1428 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1431 "(-3 + x) / (2 + x)"
1433 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 26";
1435 (*Schalk I, p.68 Nr. 440b *)
1436 (* Achtung: rechnet ewig; cancel_p hängt sich auf...
1438 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1439 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1444 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 27";
1447 "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1448 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1450 "(-9 * a ^^^ 3 * b + -9 * a ^^^ 2 * b ^^^ 2 + a ^^^ 5 * b + a ^^^ 4 * b ^^^ 2)/
1451 (3 * a ^^^ 3 * b + -3 * a * b ^^^ 3 + a ^^^ 4 * b + -1 * a ^^^ 2 * b ^^^ 3)";
1452 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1456 "-------- common denominator and multiplication ------------------";
1457 "-------- common denominator and multiplication ------------------";
1458 "-------- common denominator and multiplication ------------------";
1460 (*----------------------------------------------------------------------*)
1461 (*--------- Gemeinsamer Nenner und Multiplikation von Brüchen ----------*)
1462 (*----------------------------------------------------------------------*)
1465 (*SRAM Schalk I, p.69 Nr. 441b *)
1466 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1467 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1470 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1472 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 28";
1474 (*SRAM Schalk I, p.69 Nr. 442b *)
1475 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)";
1476 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1479 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1481 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 29";
1483 (*SRAM Schalk I, p.69 Nr. 443b *)
1484 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1485 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1488 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1490 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 30";
1492 (*SRAM Schalk I, p.69 Nr. 445b *)
1493 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1494 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1499 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 31";
1501 (*SRAM Schalk I, p.69 Nr. 446b *)
1502 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1503 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1506 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1508 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 32";
1510 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1512 "(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)";
1513 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1516 "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1518 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 33";
1520 (*SRAM Schalk I, p.69 Nr. 450a *)
1522 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1523 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1526 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1528 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 34";
1530 "-------- double fractions ---------------------------------------";
1531 "-------- double fractions ---------------------------------------";
1532 "-------- double fractions ---------------------------------------";
1534 (*SRD Schalk I, p.69 Nr. 454b *)
1536 "((2 - x)/(2*a)) / (2*a/(x - 2))";
1537 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1540 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1542 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 35";
1544 (*SRD Schalk I, p.69 Nr. 455a *)
1546 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1547 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1550 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)"
1552 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 36";
1554 (*Schalk I, p.69 Nr. 455b *)
1555 (* Achtung: Endlosschleife
1557 "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1558 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1563 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 37";
1566 "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1567 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1569 "(-12 + 4 * y + 3 * x ^^^ 2 + -1 * x ^^^ 2 * y) /
1570 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"
1571 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1573 (* Achtung: rechnet ewig; cancel_p hängt sich auf...*)
1576 "(3 + -1 * y) / (-9 + y ^^^ 2)";
1577 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1579 (*ENDLOSSCHLEIFE!!!*)
1584 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1587 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1588 (* -1 im Zähler der Angabe verursacht das Problem !*)
1591 (*SRD Schalk I, p.69 Nr. 456b *)
1593 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1594 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1597 "b / (1 + 2 * b + b ^^^ 2)"
1599 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 38";
1601 (*SRD Schalk I, p.69 Nr. 457b *)
1603 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1604 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1607 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1609 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 39";
1611 (*Schalk I, p.69 Nr. 458b *)
1612 (* Achtung: rechnet ewig; cancel_p hängt sich auf...
1614 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1615 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1620 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 40";
1623 (*SRD Schalk I, p.69 Nr. 459b *)
1625 "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1626 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1629 "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)"
1631 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 41";
1634 (*Schalk I, p.69 Nr. 460b *)
1635 (* Achtung: rechnet ewig; cancel_p hängt sich auf...
1637 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1638 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1643 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 42";
1646 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1647 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1649 "(-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)";
1650 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1654 (*SRD Schalk I, p.70 Nr. 472a *)
1655 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/\
1656 \((4*x - 8*y)/(x + y))";
1657 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1662 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 43";
1664 (*----------------------------------------------------------------------*)
1665 (*---------------------- Einfache Dppelbrüche --------------------------*)
1666 (*----------------------------------------------------------------------*)
1668 (*SRD Schalk I, p.69 Nr. 461a *)
1670 "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1671 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1676 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 44";
1678 (*SRD Schalk I, p.69 Nr. 464b *)
1680 "(a - a/(a - 2)) / (a + a/(a - 2))";
1681 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1684 "(3 + -1 * a) / (1 + -1 * a)"
1686 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 45";
1688 (*SRD Schalk I, p.69 Nr. 465b *)
1690 "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1691 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1694 "(4 * x + 6 * y + -9 * z) / (4 * x)"
1696 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 46";
1698 (*SRD Schalk I, p.69 Nr. 466b *)
1700 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1701 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1704 "(25 + -10 * x + x ^^^ 2) / 18"
1706 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 47";
1708 (*SRD Schalk I, p.70 Nr. 469 *)
1710 "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))";
1711 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1714 "3 * b ^^^ 3 / (2 * a + -2 * b)"
1716 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 48";
1718 (*----------------------------------------------------------------------*)
1719 (*---------------------- Mehrfache Dppelbrüche -------------------------*)
1720 (*----------------------------------------------------------------------*)
1722 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1723 (*WN060419 crashes with method 'simplify'*)
1725 "((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)";
1726 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1729 "1 / (a ^^^ 2 + -1 * b ^^^ 2)"
1731 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 49";
1733 (*Schalk I, p.70 Nr. 477a *)
1734 (* Achtung: rechnet ewig; Bsp zu komplex;
1735 Lösung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1737 "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) / (b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1738 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1743 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 50";
1746 "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / ((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
1747 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1749 "(a ^^^ 2 * b ^^^ 4 * y + 2 * a ^^^ 2 * b ^^^ 3 * y ^^^ 2 +\n -4 * a ^^^ 2 * b ^^^ 2 * y ^^^ 3 +\n -8 * a ^^^ 2 * b * y ^^^ 4 +\n 4 * a * b ^^^ 4 * x * y +\n 8 * a * b ^^^ 3 * x * y ^^^ 2 +\n -16 * a * b ^^^ 2 * x * y ^^^ 3 +\n -32 * a * b * x * y ^^^ 4 +\n 4 * b ^^^ 4 * x ^^^ 2 * y +\n 8 * b ^^^ 3 * x ^^^ 2 * y ^^^ 2 +\n -16 * b ^^^ 2 * x ^^^ 2 * y ^^^ 3 +\n -32 * b * x ^^^ 2 * y ^^^ 4)
1750 /\n(a ^^^ 2 * b ^^^ 5 * y + -1 * a ^^^ 2 * b ^^^ 4 * y ^^^ 2 +\n -3 * a ^^^ 2 * b ^^^ 3 * y ^^^ 3 +\n a ^^^ 2 * b ^^^ 2 * y ^^^ 4 +\n 2 * a ^^^ 2 * b * y ^^^ 5 +\n 2 * a * b ^^^ 5 * x * y +\n -2 * a * b ^^^ 4 * x * y ^^^ 2 +\n -6 * a * b ^^^ 3 * x * y ^^^ 3 +\n 2 * a * b ^^^ 2 * x * y ^^^ 4 +\n 4 * a * b * x * y ^^^ 5 +\n b ^^^ 5 * x ^^^ 2 * y +\n -1 * b ^^^ 4 * x ^^^ 2 * y ^^^ 2 +\n -3 * b ^^^ 3 * x ^^^ 2 * y ^^^ 3 +\n b ^^^ 2 * x ^^^ 2 * y ^^^ 4 +\n 2 * b * x ^^^ 2 * y ^^^ 5)";
1753 (*Schalk I, p.70 Nr. 478b *) (* Rechenzeit: 5 sec *)
1755 "(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / ((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))";
1756 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1758 (* WN050820 was OK until STOP_REW_SUB introduced -- the ONLY change !!!
1760 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1762 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 51";
1763 -----------------------------------------------------------------------*)
1765 (*Schalk I, p.70 Nr. 480a *)
1766 (* SK Achtung: rechnet ewig; cancel_p kann nicht kürzen:
1768 "(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)))";
1769 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1774 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 52";
1776 (* Berechne Zwischenergebnisse:*)
1778 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
1779 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1781 "(x ^^^ 2 * y ^^^ 2 * z + x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2) /
1782 (-1 * x ^^^ 2 * y ^^^ 2 * z + -1 * x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2)";
1784 "2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z))";
1785 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1789 (* SK 1. Ausdruck kann nicht weiter gekürzt werden; cancel_p !!!*)
1790 ### rls: cancel_p on:
1791 (x ^^^ 2 * (y ^^^ 2 * z) + x ^^^ 2 * (y * z ^^^ 2) + x * (y ^^^ 2 * z ^^^ 2)) /
1792 (-1 * (x ^^^ 2 * (y ^^^ 2 * z)) + -1 * (x ^^^ 2 * (y * z ^^^ 2)) + x * (y ^^^ 2 * z ^^^ 2))
1793 GC #3.61.81.101.197.17503: (0 ms)
1794 *** RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction
1797 "(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))";
1798 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1800 (*uncaught exception nonexhaustive binding failure*)
1802 (* Das kann er aber kürzen !!???: *)
1804 "(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1805 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1807 "(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1815 (*--------------------------------------------------------------------*)
1816 (*----------------------- Problem-Beispiele --------------------------*)
1817 (*--------------------------------------------------------------------*)
1819 (*Schalk I, p.60 Nr. 215d *)
1820 (* Achtung: rechnet ewig ...
1821 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1822 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1826 (* Kein Wunder, denn Zähler und Nenner extra als Polynom dargestellt ergibt:*)
1828 val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1829 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1831 "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";
1832 val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
1833 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1835 "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";
1837 (*anscheinend macht dem Rechner das Kürzen diese Bruches keinen Spass mehr ...*)
1839 (*--------------------------------------------------------------------*)
1840 (*Schalk I, p.70 Nr. 480b *)
1842 trace_rewrite:=false; (*sonst dauert Berechnung sehr lange!*)
1844 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/\
1845 \(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *\
1846 \(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/\
1847 \(20*x*y/(x^^^2 - 25*y^^^2))";
1848 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1850 "((180 * x^^^4 * y + 675 * x^^^3 * y^^^2 + 1105 * x^^^2 * y^^^3 +\n -75 * x * y^^^4 +\n -125 * y^^^5) /\n (x^^^3 + 5 * x^^^2 * y + -25 * x * y^^^2 + -125 * y^^^3) +\n (225 * x^^^2 * y^^^2 + -25 * y^^^4) /\n (x^^^2 + 10 * x * y + 25 * y^^^2)) /\n(20 * x * y)";
1852 (* Kann nicht weiter vereinfacht werden !!!!?? *)
1854 (*--------------------------------------------------------------------*)
1855 (*Seltsames in common_nominator_p: *)
1857 val t = str2term " (1 + x^^^5) / (x + y) + x^^^3 / x ";
1859 val Some (t,_) = rewrite_set_ thy false common_nominator_p t;
1862 (*### add_fraction_p_ called
1863 uncaught exception nonexhaustive binding failure
1864 raised at: stdIn:175.1-175.61*)
1866 val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
1868 val Some (t,_) = rewrite_set_ thy false common_nominator_p t;
1870 "(1 + 1 * x^^^3 + 1 * x^^^5 + 1 * (y * x^^^2)) / (1 * x + 1 * y)";
1872 (*--------------------------------------------------------------------*)
1873 (* cancel_p liefert nicht immer Polynomnormalform (2):
1874 ---> Sortierung FALSCH !! *)
1877 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1879 "1 * (a^^^4 * b^^^3) / 1"; (*OK*)
1883 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1885 "1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
1887 (* Problem liegt NICHT bei ord_make_polynomial! (siehe folgende Bsple) *)
1889 val x = str2term "x"; val bdv = str2term "bdv";
1890 val t1 = str2term "b^^^2 * a^^^5";
1891 val t2 = str2term "a^^^5 * b^^^2 ";
1892 ord_make_polynomial false Rational.thy [(x,bdv)] (t1,t2); (*false*)
1894 (* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
1896 (*--------------------------------------------------------------------*)
1897 (* cancel_p liefert nicht immer Polynomnormalform (2):
1898 ---> erzeugt überflüssige "1 * ..."
1903 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1906 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1907 (* -1 im Zähler der Angabe verursacht das Problem !*)
1910 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1912 (* Achtung: Endlosschleife bei cancel_p:
1914 "(a^^^2 - 1)/(a+1)";
1915 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1917 "(-1 + a^^^2) / (1 + a)";
1918 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1920 "(-1 + 1 * a) / 1"; (*OK*)
1923 "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1924 val Some (t,_) = rewrite_set_ thy false make_polynomial t;
1926 "(-1 + -1 * b + a^^^2 + a^^^2 * b) /
1927 (-1 + -1 * a + b^^^2 + a * b^^^2)"
1928 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1937 (*--------------------------------------------------------------------*)
1938 (* EHEMALIG (MG 2004) FEHLER *)
1939 (*--------------------------------------------------------------------*)
1941 (* cancel_p liefert nicht immer Polynomnormalform (2):
1942 ---> Minus (binärer Operator) wird erzeugt !!! *)
1944 "-1 / (5 + -2 * x)";
1945 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1947 "-1 / (5 - 2 * x)";*)
1950 (*aber wenn im Zähler kein Minus tritt Problem nicht auf !!??:*)
1953 val Some (t,_) = rewrite_set_ thy false cancel_p t;
1955 "1 / (5 + -2 * x)";*)
1957 (* ACHTUNG: Endlosschleife !!! *)
1958 (*Schalk I, p.66 Nr. 381b *)
1960 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1961 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1963 (*--------------------------------------------------------------------*)
1967 "--------------------------------------------------------------------";
1968 "----------------------- Muster-Beispiele fuer DA -------------------";
1969 "--------------------------------------------------------------------";
1971 (*SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1973 "(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))";
1974 val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1977 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
1979 else raise error "rational.sml.sml: diff.behav. in norm_Rational_mg 53";
1981 "-------- me Schalk I No.186 -------------------------------------";
1982 "-------- me Schalk I No.186 -------------------------------------";
1983 "-------- me Schalk I No.186 -------------------------------------";
1984 val fmz = ["term ((14 * x * y) / ( x * y ))",
1987 ("Rational.thy",["rational","simplification"],
1988 ["simplification","of_rationals"]);
1989 val p = e_pos'; val c = [];
1990 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1991 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1992 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1993 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1994 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1995 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1996 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1997 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1998 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1999 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
2000 if f2str f = "14" then ()
2001 else raise error "rational.sml diff.behav. in me Schalk I No.186";
2004 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
2005 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
2006 "-------- interSteps ..Simp_Rat_Double_No-1.xml ------------------";
2009 [(["term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
2010 ("Rational.thy",["rational","simplification"],
2011 ["simplification","of_rationals"]))];
2014 autoCalculate 1 CompleteCalc;
2015 val ((pt,p),_) = get_calc 1; show_pt pt;
2017 interSteps 1 ([1],Res);
2018 val ((pt,p),_) = get_calc 1; show_pt pt;
2021 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
2022 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
2023 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ------------------";
2026 [(["term ((14 * x * y) / ( x * y ))", "normalform N"],
2027 ("Rational.thy",["rational","simplification"],
2028 ["simplification","of_rationals"]))];
2031 autoCalculate 1 CompleteCalc;
2032 val ((pt,p),_) = get_calc 1; show_pt pt;
2034 interSteps 1 ([1],Res);
2035 val ((pt,p),_) = get_calc 1; show_pt pt;
2037 interSteps 1 ([1,2],Res);
2038 val ((pt,p),_) = get_calc 1; show_pt pt;
2040 (*WN060823 cancel_p_ init_state does not terminate, see Rational.ML
2041 interSteps 1 ([1,2,1],Res);
2042 val ((pt,p),_) = get_calc 1; show_pt pt;