Test_Isac works again, almost ..
4 files raise errors:
# Interpret/solve.sml: "solve.sml: interSteps on norm_Rational 2"
# Interpret/inform.sml: "inform.sml: [rational,simplification] 2"
# Knowledge/partial_fractions.sml: "autoCalculate for met_partial_fraction changed: final result"
# Knowledge/eqsystem.sml: "eqsystem.sml: exp 7.70 normalize 4x4 by rewrite changed"
The chunk of changes is due to the fact, that Isac's code still is unstable.
The changes are accumulated since e8f46493af82.
1 (* Title: tests for rationals
3 Use is subject to license terms.
6 "-----------------------------------------------------------------------------";
7 "-----------------------------------------------------------------------------";
8 "table of contents -----------------------------------------------------------";
9 "-----------------------------------------------------------------------------";
10 "-------- fun poly_of_term ---------------------------------------------------";
11 "-------- fun is_poly --------------------------------------------------------";
12 "-------- fun term_of_poly ---------------------------------------------------";
13 "-------- integration lev.1 fun factout_p_ -----------------------------------";
14 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
15 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
16 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
17 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
18 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
19 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
20 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
21 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
22 "-------- reverse rewrite ----------------------------------------------------";
23 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
24 "-------- investigate rls norm_Rational --------------------------------------";
25 "-------- examples: rls norm_Rational ----------------------------------------";
26 "-------- numeral rationals -----------------------------";
27 "-------- cancellation ----------------------------------";
28 "-------- common denominator ----------------------------";
29 "-------- multiply and cancel ---------------------------";
30 "-------- common denominator and multiplication ---------";
31 "-------- double fractions ------------------------------";
32 "-------- crucial examples ------------------------------";
33 "-------- examples for Stefan Karnels thesis ------------";
34 "-------- me Schalk I No.186 ----------------------------";
35 "-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
36 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
37 "-------- investigate rulesets for cancel_p -------------";
38 "-------- investigate format of factout_ and factout_p_ -";
39 "-------- how to stepwise construct Scripts -------------";
40 "----------- get_denominator ----------------------------";
41 "--------- several errpats in complicated term -------------------";
42 "--------------------------------------------------------";
43 "-------- nonterminating cancel_p, norm_Rational 2002 ---";
44 "--------------------------------------------------------";
45 "--------------------------------------------------------";
48 "-------- fun poly_of_term ---------------------------------------------------";
49 "-------- fun poly_of_term ---------------------------------------------------";
50 "-------- fun poly_of_term ---------------------------------------------------";
51 val vs = "12 * x^^^3 * y^^^4 * z^^^6" |> str2term |> vars |> map free2str |> sort string_ord;
53 if poly_of_term vs (str2term "12::real") = SOME [(12, [0, 0, 0])]
54 then () else error "poly_of_term 1 changed";
55 if poly_of_term vs (str2term "x::real") = SOME [(1, [1, 0, 0])]
56 then () else error "poly_of_term 2 changed";
57 if poly_of_term vs (str2term "12 * x^^^3") = SOME [(12, [3, 0, 0])]
58 then () else error "poly_of_term 3 changed";
59 if poly_of_term vs (str2term "12 * x^^^3 * y^^^4 * z^^^6") = SOME [(12, [3, 4, 6])]
60 then () else error "poly_of_term 4 changed";
61 if poly_of_term vs (str2term "1 + 2 * x^^^3 * y^^^4 * z^^^6 + y") =
62 SOME [(1, [0, 0, 0]), (1, [0, 1, 0]), (2, [3, 4, 6])]
63 then () else error "poly_of_term 5 changed";
65 (*poly_of_term is quite liberal:*)
66 (*the coefficient may be somewhere, the order of variables and the parentheses
67 within a monomial are arbitrary*)
68 if poly_of_term vs (str2term "y^^^4 * (x^^^3 * 12 * z^^^6)") = SOME [(12, [3, 4, 6])]
69 then () else error "poly_of_term 6 changed";
71 (*there may even be more than 1 coefficient:*)
72 if poly_of_term vs (str2term "2 * y^^^4 * (x^^^3 * 6 * z^^^6)") = SOME [(12, [3, 4, 6])]
73 then () else error "poly_of_term 7 changed";
75 (*the order and the parentheses within monomials are arbitrary:*)
76 if poly_of_term vs (str2term "2 * x^^^3 * y^^^4 * z^^^6 + (7 * y^^^8 + 1)")
77 = SOME [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 6])]
78 then () else error "poly_of_term 8 changed";
80 "-------- fun is_poly --------------------------------------------------------";
81 "-------- fun is_poly --------------------------------------------------------";
82 "-------- fun is_poly --------------------------------------------------------";
83 if is_poly (str2term "2 * x^^^3 * y^^^4 * z^^^6 + 7 * y^^^8 + 1")
84 then () else error "is_poly 1 changed";
85 if not (is_poly (str2term "2 * (x^^^3 * y^^^4 * z^^^6 + 7) * y^^^8 + 1"))
86 then () else error "is_poly 2 changed";
88 "-------- fun term_of_poly ---------------------------------------------------";
89 "-------- fun term_of_poly ---------------------------------------------------";
90 "-------- fun term_of_poly ---------------------------------------------------";
91 val expT = HOLogic.realT
92 val Free (_, baseT) = (hd o vars o str2term) "12 * x^^^3 * y^^^4 * z^^^6";
93 val p = [(1, [0, 0, 0]), (7, [0, 8, 0]), (2, [3, 4, 5])]
94 val vs = ["x","y","z"]
95 (*precondition for [(c, es),...]: legth es = length vs*)
97 if term2str (term_of_poly baseT expT vs p) = "1 + 7 * y ^^^ 8 + 2 * x ^^^ 3 * y ^^^ 4 * z ^^^ 5"
98 then () else error "term_of_poly 1 changed";
100 "-------- integration lev.1 fun factout_p_ -----------------------------------";
101 "-------- integration lev.1 fun factout_p_ -----------------------------------";
102 "-------- integration lev.1 fun factout_p_ -----------------------------------";
103 val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
104 val SOME (t', asm) = factout_p_ thy t;
105 if term2str t' = "(x + y) * (x + -1 * y) / (x * (x + -1 * y))"
106 then () else error ("factout_p_ term 1 changed: " ^ term2str t')
108 if terms2str asm = "[\"x ~= 0\",\"x + -1 * y ~= 0\"]"
109 then () else error "factout_p_ asm 1 changed"
111 val t = str2term "nothing + to_cancel ::real";
112 if NONE = factout_p_ thy t then () else error "factout_p_ doesn't report non-applicable";
114 val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
115 val SOME (t', asm) = factout_p_ thy t;
116 if term2str t' = "(3 + 3 * x) * (1 + x) / (2 * (1 + x))" andalso
117 terms2str asm = "[\"1 + x ~= 0\"]"
118 then () else error "factout_p_ 1 changed";
120 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
121 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
122 "-------- integration lev.1 fun cancel_p_ ------------------------------------";
123 val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)"
124 val SOME (t', asm) = cancel_p_ thy t;
125 if (term2str t', terms2str asm) = ("(x + y) / x", "[\"x ~= 0\"]")
126 then () else error ("cancel_p_ (t', asm) 1 changed: " ^ term2str t')
128 val t = str2term "nothing + to_cancel ::real";
129 if NONE = cancel_p_ thy t then () else error "cancel_p_ doesn't report non-applicable";
131 val t = str2term "((3 * x^^^2 + 6 *x + 3) / (2*x + 2))";
132 val SOME (t', asm) = cancel_p_ thy t;
133 if term2str t' = "(3 + 3 * x) / 2" andalso terms2str asm = "[]"
134 then () else error "cancel_p_ 1 changed";
136 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
137 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
138 "-------- integration lev.1 fun common_nominator_p_ --------------------------";
139 val t = str2term ("y / (a*x + b*x + c*x) " ^
143 val SOME (t', asm) = common_nominator_p_ thy t;
145 ("y * y / (x * ((a + b + c) * y)) " ^
146 (* n1 *d2'/ (c'* ( d1' *d2')) *)
147 "+ a * (a + b + c) / (x * ((a + b + c) * y))")
148 (* n2 * d1' / (c'* ( d1' *d2')) *)
149 then () else error "common_nominator_p_ term 1 changed";
150 if terms2str asm = "[\"a + b + c ~= 0\",\"y ~= 0\",\"x ~= 0\"]"
151 then () else error "common_nominator_p_ asm 1 changed"
153 "-------- example in mail Nipkow";
154 val t = str2term "x/(x^^^2 + -1*y^^^2) + y/(x^^^2 + -1*x*y)";
155 val SOME (t', asm) = common_nominator_p_ thy t;
156 if term2str t' = "x * x / " ^
157 "((x + -1 * y) * ((x + y) * x))" ^
160 "((x + -1 * y) * ((x + y) * x))"
161 then () else error "common_nominator_p_ term 2 changed"
163 if terms2str asm = "[\"x + y ~= 0\",\"x ~= 0\",\"x + -1 * y ~= 0\"]"
164 then () else error "common_nominator_p_ asm 2 changed"
166 "-------- example: applicable tested by SML code";
167 val t = str2term "nothing / to_add";
168 if NONE = common_nominator_p_ thy t then () else error "common_nominator_p_ term 3 changed";
170 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
171 val SOME (t', asm) = common_nominator_p_ thy t;
173 "(x + -1) * (-1 + x) / ((1 + x) * (-1 + x)) +\n(x + 1) * (1 + x) / ((1 + x) * (-1 + x))"
174 andalso terms2str asm = "[\"1 + x ~= 0\",\"-1 + x ~= 0\"]"
175 then () else error "common_nominator_p_ 3 changed";
177 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
178 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
179 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
180 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
181 val SOME (t', asm) = add_fraction_p_ thy t;
182 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)"
183 then () else error "add_fraction_p_ 3 changed";
185 if terms2str asm = "[\"-1 + x ^^^ 2 ~= 0\"]"
186 then () else error "add_fraction_p_ 3 changed";
188 val t = str2term "nothing / to_add";
189 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ term 3 changed";
191 val t = str2term "((x + (-1)) / (x + 1)) + ((x + 1) / (x + (-1)))";
192 val SOME (t', asm) = add_fraction_p_ thy t;
193 if term2str t' = "(2 + 2 * x ^^^ 2) / (-1 + x ^^^ 2)" andalso
194 terms2str asm = "[\"-1 + x ^^^ 2 ~= 0\"]"
195 then () else error "add_fraction_p_ 3 changed";
197 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
198 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
199 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
200 (* trace down until prepats are evaluated
201 (which does not to work, because substitution is not done -- compare rew_sub!);
202 keep this sequence for the case, factout_p, cancel_p, common_nominator_p, add_fraction_p
203 (again) get prepat = [] changed to <>[]. *)
204 val t = str2term "(x^^^2 + -1*y^^^2) / (x^^^2 + -1*x*y)";
206 (*rewrite_set_ @{theory Isac} true cancel t = NONE; !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
207 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (thy, false, cancel_p, t);
208 "~~~~~ fun rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
209 (thy, 1, bool, [], rls, term);
210 (*val (t', asm, rew) = app_rev thy (i+1) rrls t; rew = false!!!!!!!!!!!!!!!!!!!!!*)
211 "~~~~~ and app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
212 fun chk_prepat thy erls [] t = true
213 | chk_prepat thy erls prepat t =
215 fun chk (pres, pat) =
217 val subst: Type.tyenv * Envir.tenv =
218 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
220 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
221 end) handle _ => false
222 fun scan_ f [] = false (*scan_ NEVER called by []*)
223 | scan_ f (pp::pps) =
224 if f pp then true else scan_ f pps;
225 in scan_ chk prepat end;
226 (* apply the normal_form of a rev-set *)
227 fun app_rev' thy (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}) t =
228 if chk_prepat thy erls prepat t
229 then ((*tracing("### app_rev': t = "^(term2str t));*) normal_form t)
231 (* val opt = app_rev' thy rrls t ..NONE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
232 "~~~~~ and app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
234 (* chk_prepat thy erls prepat t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
235 (* app_sub thy i rrls t = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
236 "~~~~~ fun chk_prepat, args:"; val (thy, erls, prepat, t) = (thy, erls, prepat, t);
237 fun chk (pres, pat) =
239 val subst: Type.tyenv * Envir.tenv =
240 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
242 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
243 end) handle _ => false
244 fun scan_ f [] = false (*scan_ NEVER called by []*)
245 | scan_ f (pp::pps) =
246 if f pp then true else scan_ f pps;
248 (*========== inhibit exn WN130823: prepat is empty ====================================
249 (* scan_ chk prepat = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
250 "~~~~~ fun , args:"; val (f, (pp::pps)) = (chk, prepat);
252 val ([t1, t2], t) = pp;
253 term2str t1 = "?r is_expanded";
254 term2str t2 = "?s is_expanded";
255 term2str t = "?r / ?s";
256 (* f pp = false!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
257 "~~~~~ fun chk, args:"; val (pres, pat) = (pp);
258 val subst: Type.tyenv * Envir.tenv =
259 Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty)
261 ({}, {(("r", 0), ("real", Var (("r", 0), "real"))),
262 (("s", 0), ("real", Var (("s", 0), "real")))}*)
264 snd (eval__true thy (i + 1) (map (Envir.subst_term subst) pres) [] erls)
265 "~~~~~ fun eval__true, args:"; val (thy, i, asms, bdv, rls) =
266 (thy, (i + 1), (map (Envir.subst_term subst) pres), [], erls);
267 terms2str asms; (* = "[\"?r is_expanded\",\"?s is_expanded\"]"*)
268 asms = [@{term True}] orelse asms = []; (* = false*)
269 asms = [@{term False}] ; (* = false*)
270 "~~~~~ fun chk, args:"; val (indets, (a::asms)) = ([], asms);
271 bdv (*= []: _a list*);
272 val bdv : (term * term) list = [];
273 rewrite__set_ thy (i+1) false;
274 term2str a = "?r is_expanded"; (*hier m"usste doch der Numerator eingesetzt sein ??????????????*)
275 val SOME (Const ("HOL.False", _), []) = rewrite__set_ thy (i+1) false bdv rls a
276 ============ inhibit exn WN130823: prepat is empty ===================================*)
278 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
279 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
280 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
281 val t = str2term "(12 * x * y) / (8 * y^^^2 )";
282 (* "-------- example 187a": exception Div raised...
283 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
284 val t = str2term "(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
285 (* "-------- example 187b": doesn't terminate...
286 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
287 val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";
288 (* "-------- example 187c": doesn't terminate...
289 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;*)
290 "~~~~~ fun rewrite_set_, args:"; val (thy, bool, rls, term) = (@{theory Isac}, false, cancel_p, t);
291 (* WN130827: exception Div raised...
292 rewrite__set_ thy 1 bool [] rls term
294 "~~~~~ and rewrite__set_, args:"; val (thy, i, _, _, (rrls as Rrls _), t) =
295 (thy, 1, bool, [], rls, term);
296 (* WN130827: exception Div raised...
297 val (t', asm, rew) = app_rev thy (i+1) rrls t
299 "~~~~~ fun app_rev, args:"; val (thy, i, rrls, t) = (thy, (i+1), rrls, t);
300 (* WN130827: exception Div raised...
301 val opt = app_rev' thy rrls t
303 "~~~~~ fun app_rev', args:"; val (thy, (Rrls{erls,prepat,scr=Rfuns{normal_form,...},...}), t) =
305 chk_prepat thy erls prepat t = true;
306 (* WN130827: exception Div raised...
309 (* lookup Rational.thy, cancel_p: normal_form = cancel_p_ thy*)
310 "~~~~~ fun cancel_p_, args:"; val (t) = (t);
311 val opt = check_fraction t;
312 val SOME (numerator, denominator) = opt
313 val vs = t |> vars |> map free2str |> sort string_ord
314 val baseT = type_of numerator
315 val expT = HOLogic.realT
316 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
317 (*"-------- example 187a": exception Div raised...
318 val a = [(12, [1, 1])]: poly
319 val b = [(8, [0, 2])]: poly
320 val ((a', b'), c) = gcd_poly a b
322 (* "-------- example 187b": doesn't terminate...
323 val a = [(8, [2, 1, 1])]: poly
324 val b = [(18, [1, 2, 1])]: poly
325 val ((a', b'), c) = gcd_poly a b
327 (* "-------- example 187c": doesn't terminate...
328 val a = [(9, [5, 2, 4])]: poly
329 val b = [(15, [6, 3, 1])]: poly
330 val ((a', b'), c) = gcd_poly a b
333 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
334 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
335 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
336 val thy = @{theory "Rational"};
338 val t = str2term "(2 + -3 * x) / 9";
339 if NONE = rewrite_set_ thy false cancel_p t then ()
340 else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled";
342 "-------- example 186a";
343 val t = str2term "(14 * x * y) / (x * y)";
344 is_expanded (str2term "14 * x * y");
345 is_expanded (str2term "x * y");
346 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
347 if (term2str t', terms2str asm) = ("14 / 1", "[]")
348 then () else error "rational.sml cancel Schalk 186a";
350 "-------- example 186b";
351 val t = str2term "(60 * a * b) / ( 15 * a * b )";
352 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
353 if (term2str t', terms2str asm) = ("4 / 1", "[]")
354 then () else error "rational.sml cancel Schalk 186b";
356 "-------- example 186c";
357 val t = str2term "(144 * a^^^2 * b * c) / (12 * a * b * c)";
358 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
359 if (term2str t', terms2str asm) = ("12 * a / 1", "[]")
360 then () else error "rational.sml cancel Schalk 186c";
362 (* !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! exception Div raised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
363 see --- fun rewrite_set_ downto fun gcd_poly ---
364 "-------- example 187a";
365 val t = str2term "(12 * x * y) / (8 * y^^^2 )";
366 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
367 if (term2str t', terms2str asm) = ("3 * x / (2 * y)", "[\"4 * y ~= 0\"]")
368 then () else error "rational.sml cancel Schalk 187a";
371 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
372 see --- fun rewrite_set_ downto fun gcd_poly ---
373 "-------- example 187b";
374 val t = str2term "(8 * x^^^2 * y * z ) / (18 * x * y^^^2 * z )";
375 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
376 if (term2str t', terms2str asm) = ("4 * x / (9 * y)", "[\"2 * (z * (y * x)) ~= 0\"]")
377 then () else error "rational.sml cancel Schalk 187b";
380 (* doesn't terminate !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
381 see --- fun rewrite_set_ downto fun gcd_poly ---
382 "-------- example 187c";
383 val t = str2term "(9 * x^^^5 * y^^^2 * z^^^4) / (15 * x^^^6 * y^^^3 * z )";
384 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
385 if (term2str t', terms2str asm) =
386 ("3 * z ^^^ 3 / (5 * (y * x))", "[\"3 * (z * (y ^^^ 2 * x ^^^ 5)) ~= 0\"]")
387 then () else error "rational.sml cancel Schalk 187c";
390 "-------- example 188a";
391 val t = str2term "(-8 + 8 * x) / (-9 + 9 * x)";
392 is_expanded (str2term "8 * x + -8");
393 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
394 if (term2str t', terms2str asm) = ("8 / 9", "[]")
395 then () else error "rational.sml cancel Schalk 188a";
397 val t = str2term "(8*((-1) + x))/(9*((-1) + x))";
398 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
399 if (term2str t', terms2str asm) = ("8 / 9", "[]")
400 then () else error "rational.sml cancel Schalk make_polynomial 1";
402 "-------- example 188b";
403 val t = str2term "(-15 + 5 * x) / (-18 + 6 * x)";
404 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
405 if (term2str t', terms2str asm) = ("5 / 6", "[]")
406 then () else error "rational.sml cancel Schalk 188b";
408 "-------- example 188c";
409 val t = str2term "(a + -1 * b) / (b + -1 * a)";
410 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
411 if (term2str t', terms2str asm) = ("-1 / 1", "[]")
412 then () else error "rational.sml cancel Schalk 188c";
414 is_expanded (str2term "a + -1 * b") = true;
415 val t = str2term "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
416 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
417 if (term2str t', terms2str asm) = ("(a + -1 * b) / (-1 * a + b)", "[]")
418 then () else error "rational.sml cancel Schalk make_polynomial 2";
420 "-------- example 190a";
421 val t = str2term "( 27 * a^^^3 + 9 * a^^^2 + 3 * a + 1 ) / ( 27 * a^^^3 + 18 * a^^^2 + 3 * a )";
422 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
423 if (term2str t', terms2str asm) =
424 ("(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)", "[\"3 * a + 9 * a ^^^ 2 ~= 0\"]")
425 then () else error "rational.sml cancel Schalk 190a";
427 "-------- example 190c";
428 val t = str2term "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
429 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
430 if (term2str t', terms2str asm) =
431 ("(1 + 3 * a + 9 * a ^^^ 2 + 27 * a ^^^ 3) /\n(3 * a + 18 * a ^^^ 2 + 27 * a ^^^ 3)", "[]")
432 then () else error "rational.sml make_polynomial Schalk 190c";
434 "-------- example 191a";
435 val t = str2term "( x^^^2 + -1 * y^^^2 ) / ( x + y )";
436 is_expanded (str2term "x^^^2 + -1 * y^^^2") = false; (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
437 is_expanded (str2term "x + y") = true;
438 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
439 if (term2str t', terms2str asm) = ("(x + -1 * y) / 1", "[]")
440 then () else error "rational.sml make_polynomial Schalk 191a";
442 "-------- example 191b";
443 val t = str2term "((x + (-1) * y)*(x + y))/((1)*(x + y))";
444 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
445 if (term2str t', terms2str asm) = ("(x ^^^ 2 + -1 * y ^^^ 2) / (x + y)", "[]")
446 then () else error "rational.sml make_polynomial Schalk 191b";
448 "-------- example 191c";
449 val t = str2term "( 9 * x^^^2 + -30 * x + 25 ) / ( 9 * x^^^2 + -25 )";
450 is_expanded (str2term "9 * x^^^2 + -30 * x + 25") = true;
451 is_expanded (str2term "25 + -30*x + 9*x^^^2") = true;
452 is_expanded (str2term "-25 + 9*x^^^2") = true;
454 val t = str2term "(((-5) + 3 * x)*((-5) + 3 * x))/((5 + 3 * x)*((-5) + 3 * x))";
455 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
456 if (term2str t', terms2str asm) = ("(25 + -30 * x + 9 * x ^^^ 2) / (-25 + 9 * x ^^^ 2)", "[]")
457 then () else error "rational.sml make_polynomial Schalk 191c";
459 "-------- example 192b";
460 val t = str2term "( 7 * x^^^3 + -1 * x^^^2 * y ) / ( 7 * x * y^^^2 + -1 * y^^^3 )";
461 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
462 if (term2str t', terms2str asm) = ("x ^^^ 2 / y ^^^ 2", "[\"y ^^^ 2 ~= 0\"]")
463 then () else error "rational.sml cancel_p Schalk 192b";
465 val t = str2term "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
466 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
467 if (term2str t', terms2str asm) =
468 ("(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)", "[]")
469 then () else error "rational.sml make_polynomial Schalk 192b";
471 val t = str2term "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
472 val SOME (t', asm) = rewrite_set_ thy false make_polynomial t;
473 if (term2str t', terms2str asm) =
474 ("(7 * x ^^^ 3 + -1 * x ^^^ 2 * y) / (7 * x * y ^^^ 2 + -1 * y ^^^ 3)", "[]")
475 then () else error "rational.sml make_polynomial Schalk WN050929 not working";
477 "-------- example 193a";
478 val t = str2term "( x^^^2 + -6 * x + 9 ) / ( x^^^2 + -9 )";
479 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
480 if (term2str t', terms2str asm) = ("(-3 + x) / (3 + x)", "[\"3 + x ~= 0\"]")
481 then () else error "rational.sml cancel_p Schalk 193a";
483 "-------- example 193b";
484 val t = str2term "( x^^^2 + -8 * x + 16 ) / ( 2 * x^^^2 + -32 )";
485 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
486 if (term2str t', terms2str asm) = ("(-4 + x) / (8 + 2 * x)", "[\"8 + 2 * x ~= 0\"]")
487 then () else error "rational.sml cancel_p Schalk 193b";
489 "-------- example 193c";
490 val t = str2term "( 2 * x + -50 * x^^^3 ) / ( 25 * x^^^2 + -10 * x + 1 )";
491 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
492 if (term2str t', terms2str asm) =
493 ("(2 * x + 10 * x ^^^ 2) / (1 + -5 * x)", "[\"1 + -5 * x ~= 0\"]")
494 then () else error "rational.sml cancel_p Schalk 193c";
497 val t = str2term "(-25 + 9*x^^^2)/(5 + 3*x)";
498 val SOME (t, asm) = rewrite_set_ thy false cancel_p t;
499 if (term2str t', terms2str asm) = ("(2 * x + 10 * x ^^^ 2) / (1 + -5 * x)", "[]")
500 then () else error "rational.sml cancel WN 1";
502 "-------- example heuberger";
503 val t = str2term ("(x^^^4 + x * y + x^^^3 * y + y^^^2) / " ^
504 "(x + 5 * x^^^2 + y + 5 * x * y + x^^^2 * y^^^3 + x * y^^^4)");
505 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
506 if (term2str t', terms2str asm) =
507 ("(x ^^^ 3 + y) / (1 + 5 * x + x * y ^^^ 3)", "[\"1 + 5 * x + x * y ^^^ 3 ~= 0\"]")
508 then () else error "rational.sml cancel_p heuberger";
510 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
511 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
512 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
513 (*deleted example 204 ... 236b at update Isabelle2012-->2013*)
515 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
516 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
517 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
518 val t = str2term ("123 = (a*x)/(b*x) + (c*x)/(d*x) + (e*x)/(f*x::real)");
519 "-------- gcd_poly integration level 1: works on exact term";
520 if NONE = cancel_p_ thy t then () else error "cancel_p_ works on exact fraction";
521 if NONE = add_fraction_p_ thy t then () else error "add_fraction_p_ works on exact fraction";
523 "-------- gcd_poly integration level 2: picks out ONE appropriate subterm";
524 val SOME (t', asm) = rewrite_set_ thy false cancel_p t;
525 if term2str t' = "123 = a * x / (b * x) + c * x / (d * x) + e / f"
526 then () else error "level 2, rewrite_set_ cancel_p: changed";
527 val SOME (t', asm) = rewrite_set_ thy false add_fractions_p t;
528 if term2str t' = "123 = (b * c * x + a * d * x) / (b * d * x) + e * x / (f * x)"
529 then () else error "level 2, rewrite_set_ add_fractions_p: changed";
531 "-------- gcd_poly integration level 3: rewrites all appropriate subterms";
532 val SOME (t', asm) = rewrite_set_ thy false cancel_p_rls t;
533 if term2str t' = "123 = a / b + c / d + e / f"
534 then () else error "level 3, rewrite_set_ cancel_p_rls: changed";
535 val SOME (t', asm) = rewrite_set_ thy false common_nominator_p_rls t; (*CREATE add_fractions_p_rls*)
536 if term2str t' = "123 = (b * d * e * x + b * c * f * x + a * d * f * x) / (b * d * f * x)"
537 then () else error "level 3, rewrite_set_ add_fractions_p_rls: changed";
539 "-------- gcd_poly integration level 4: iteration cancel_p -- add_fraction_p";
540 (* simpler variant *)
541 val testrls = append_rls "testrls" e_rls [Rls_ cancel_p, Rls_ add_fractions_p]
542 val SOME (t', asm) = rewrite_set_ thy false testrls t;
543 (*trace_rewrite := false;
544 # rls: testrls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
545 ## rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
546 ## rls: common_nominator_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
547 ## rls: cancel_p on: 123 = (b * c * x + a * d * x) / (b * d * x) + e / f
548 ## rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
549 ## rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
550 ## rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
551 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
552 then () else error "level 4, rewrite_set_ *_p: changed";
554 (* complicated variant *)
555 val testrls_rls = append_rls "testrls_rls" e_rls [Rls_ cancel_p_rls, Rls_ common_nominator_p_rls];
556 val SOME (t', asm) = rewrite_set_ thy false testrls_rls t;
557 (*# rls: testrls_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
558 ## rls: cancel_p_rls on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
559 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e * x / (f * x)
560 ### rls: cancel_p on: 123 = a * x / (b * x) + c * x / (d * x) + e / f
561 ### rls: cancel_p on: 123 = a * x / (b * x) + c / d + e / f
562 ### rls: cancel_p on: 123 = a / b + c / d + e / f
563 ## rls: common_nominator_p_rls on: 123 = a / b + c / d + e / f
564 ### rls: common_nominator_p on: 123 = a / b + c / d + e / f
565 ### rls: common_nominator_p on: 123 = (b * c + a * d) / (b * d) + e / f
566 ### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
567 ## rls: cancel_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
568 ### rls: cancel_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
569 ## rls: common_nominator_p_rls on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)
570 ### rls: common_nominator_p on: 123 = (b * d * e + b * c * f + a * d * f) / (b * d * f) *)
571 if term2str t' = "123 = (b * d * e + b * c * f + a * d * f) / (b * d * f)"
572 then () else error "level 4, rewrite_set_ *_p_rls: changed"
574 "-------- gcd_poly integration level 5: cancel_p & add_fraction_p within norm_Rational";
575 val SOME (t', asm) = rewrite_set_ thy false norm_Rational t;
576 if term2str t' = "123 = (a * d * f + b * c * f + b * d * e) / (b * d * f)"
577 then () else error "level 5, rewrite_set_ norm_Rational: changed"
579 "-------- reverse rewrite ----------------------------------------------------";
580 "-------- reverse rewrite ----------------------------------------------------";
581 "-------- reverse rewrite ----------------------------------------------------";
582 (** the term for which reverse rewriting is demonstrated **)
583 val t = str2term "(9 + -1 * x ^^^ 2) / (9 + 6 * x + x ^^^ 2)";
584 val Rrls {scr = Rfuns {init_state = ini, locate_rule = loc,
585 next_rule = nex, normal_form = nor, ...},...} = cancel_p;
587 (** normal_form produces the result in ONE step **)
588 val SOME (t',_) = nor t;
589 if term2str t' = "(3 + -1 * x) / (3 + x)" then ()
590 else error "rational.sml normal_form (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
592 (** initialize the interpreter state used by the 'me' **)
593 val (t, _, revsets, _) = ini t;
595 if length (hd revsets) = 11 then () else error "length of revset changed";
596 if (revsets |> nth 1 |> nth 1 |> id_of_thm) =
597 (@{thm realpow_twoI} |> string_of_thm |> thmID_of_derivation_name)
598 then () else error "first element of revset changed";
600 (revsets |> nth 1 |> nth 1 |> rule2str) = "Thm (\"realpow_twoI\",??.unknown)" andalso
601 (revsets |> nth 1 |> nth 2 |> rule2str) =
602 "Thm (\"sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))\",??.unknown)" andalso
603 (revsets |> nth 1 |> nth 3 |> rule2str) =
604 "Thm (\"sym_#mult_Float ((2,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso
605 (revsets |> nth 1 |> nth 4 |> rule2str) =
606 "Thm (\"sym_#mult_Float ((~1,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso
607 (revsets |> nth 1 |> nth 5 |> rule2str) =
608 "Thm (\"sym_#mult_Float ((3,0), (0,0)) __ ((3,0), (0,0))\",??.unknown)" andalso
609 (revsets |> nth 1 |> nth 6 |> rule2str) = "Rls_ (\"sym_order_mult_rls_\")" andalso
610 (revsets |> nth 1 |> nth 7 |> rule2str) =
611 "Thm (\"sym_mult_assoc\",Groups.semigroup_mult_class.mult_assoc)"
612 then () else error "first 7 elements in revset changed"
614 (** find the rule 'r' to apply to term 't' **)
615 (*/------- since cancel_ (accepted "-" between monomials) has been replaced by cancel_p_
616 for Isabelle2013, we don't get a working revset, but non-termination:
618 val SOME (r as (Thm (str, thm))) = nex revsets t;
620 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x),
621 Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))","
622 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x),
623 Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x), []))","
624 ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * 3 * x + x * x),
625 Thm ("sym_mult_assoc",""), ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), []))","
626 ((3 * 3 + -1 * x * x) / (3 * 3 + 2 * 3 * x + x * x), Rls_ ("sym_order_mult_rls_"), ((3 * 3 + -1 * (x * x)) / (3 * 3 + 2 * (3 * x) + x * x), []))","
629 Thm ("sym_#mult_2_3", "6 = 2 * 3")
630 ### Isabelle2009-2 for cancel_ (not cancel_p_):
631 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))"
632 andalso string_of_thm thm =
633 (string_of_thm o make_thm o (cterm_of (@{theory "Isac"})))
634 (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
635 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
636 \---------------------------------------------------------------------------------------/*)
638 (** check, if the rule 'r' applied by the user to 't' belongs to the ruleset;
639 if the rule is OK, the term resulting from applying the rule is returned,too;
640 there might be several rule applications inbetween,
641 which are listed after the head in reverse order **)
642 (*/-------------------------------------------- Isabelle2013: this gives "error id_of_thm";
643 we don't repair this, because interaction within "reverse rewriting" never worked properly:
645 val (r, (t, asm))::_ = loc revsets t r;
646 if term2str t = "(9 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" andalso asm = []
647 then () else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
649 (* find the next rule to apply *)
650 val SOME (r as (Thm (str, thm))) = nex revsets t;
651 if str = "sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))" andalso
652 string_of_thm thm = (string_of_thm o make_thm o (cterm_of (@{theory "Isac"})))
653 (Trueprop $ (term_of o the o (parse thy)) "9 = 3 ^^^ 2") then ()
654 else error "rational.sml next_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2)";
656 (*check the next rule*)
657 val (r, (t, asm)) :: _ = loc revsets t r;
658 if term2str t = "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 6 * x + x ^^^ 2)" then ()
659 else error "rational.sml locate_rule (9 - x ^^^ 2) / (9 - 6 * x + x ^^^ 2) II";
661 (*find and check the next rules, rewrite*)
662 val SOME r = nex revsets t;
663 val (r,(t,asm))::_ = loc revsets t r;
664 if term2str t = "(3 ^^^ 2 - x ^^^ 2) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)" then ()
665 else error "rational.sml locate_rule II";
667 val SOME r = nex revsets t;
668 val (r,(t,asm))::_ = loc revsets t r;
669 if term2str t = "(3 - x) * (3 + x) / (3 ^^^ 2 + 2 * 3 * x + x ^^^ 2)" then ()
670 else error "rational.sml next_rule II";
672 val SOME r = nex revsets t;
673 val (r,(t,asm))::_ = loc revsets t r;
674 if term2str t = "(3 - x) * (3 + x) / ((3 + x) * (3 + x))" then ()
675 else error "rational.sml next_rule III";
677 val SOME r = nex revsets t;
678 val (r, (t, asm)) :: _ = loc revsets t r;
680 if ss = "(3 - x) / (3 + x)" andalso terms2str asm = "[\"3 + x ~= 0\"]" then ()
681 else error "rational.sml: new behav. in rev-set cancel";
682 \--------------------------------------------------------------------------------------/*)
684 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
685 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
686 "-------- 'reverse-ruleset' cancel_p -----------------------------------------";
687 (*Isabelle2013: the example below shows, why "reverse rewriting" only worked for
690 (*the term for which reverse rewriting is demonstrated*)
691 val t = str2term "(9 + (-1)*x^^^2) / (9 + ((-6)*x + x^^^2))";
692 val Rrls {scr=Rfuns {init_state=ini,locate_rule=loc,
693 next_rule=nex,normal_form=nor,...},...} = cancel_p;
695 (*normal_form produces the result in ONE step*)
696 val SOME (t',_) = nor t;
697 term2str t' = "(3 + 1 * x) / (3 + -1 * x)";
699 (*initialize the interpreter state used by the 'me'*)
700 val SOME (t', asm) = cancel_p_ thy t;
701 term2str t' = "(3 + x) / (3 + -1 * x)" (*true*);
702 terms2str asm = "[\"3 + -1 * x ~= 0\"]" (*true*);
703 val (t,_,revsets,_) = ini t;
705 (* WN.10.10.02: dieser Fall terminiert nicht
706 (make_polynomial enth"alt zu viele rules)
707 WN060823 'init_state' requires rewriting on specified location in the term
708 print_depth 99; Rfuns; print_depth 3;
709 WN060831 cycling "sym_order_mult_rls_" "sym_mult_assoc"
710 as was with make_polynomial before ?!?*)
712 val SOME r = nex revsets t;
713 eq_Thm (r, Thm ("sym_#power_Float ((3,0), (0,0)) __ ((2,0), (0,0))",
714 mk_thm thy "9 = 3 ^^^ 2"));
715 (*WN060831 *** id_of_thm
716 Exception- ERROR raised ...
717 val (r,(t,asm))::_ = loc revsets t r;
720 val SOME r = nex revsets t;
721 val (r,(t,asm))::_ = loc revsets t r;
725 (*========== inhibit exn WN130824 TODO =======================================================
726 "-------- examples: rls norm_Rational ----------------------------------------";
727 "-------- examples: rls norm_Rational ----------------------------------------";
728 "-------- examples: rls norm_Rational ----------------------------------------";
729 val t = str2term "(3*x+5)/18 - x/2 - -(3*x - 2)/9 = 0";
730 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
731 if term2str t' = "1 / 18 = 0" then () else error "rational.sml 1";
733 val t = str2term "(17*x - 51)/9 - (-(13*x - 3)/6) + 11 - (9*x - 7)/4 = 0";
734 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
735 if term2str t' = "(237 + 65 * x) / 36 = 0" then ()
736 else error "rational.sml 2";
738 val t = str2term "(1/2 + (5*x)/2)^^^2 - ((13*x)/2 - 5/2)^^^2 - (6*x)^^^2 + 29";
739 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
740 if term2str t' = "23 + 35 * x + -72 * x ^^^ 2" then ()
741 else error "rational.sml 3";
743 (*trace_rewrite:=true;*)
744 val t = str2term "Not (6*x is_atom)";
745 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
747 val t = str2term "1 < 2";
748 val SOME (t',_) = rewrite_set_ thy false powers_erls t; term2str t';
751 val t = str2term "(6*x)^^^2";
752 val SOME (t',_) = rewrite_ thy dummy_ord powers_erls false
753 (num_str @{thm realpow_def_atom}) t;
754 if term2str t' = "6 * x * (6 * x) ^^^ (2 + -1)" then ()
755 else error "rational.sml powers_erls (6*x)^^^2";
757 val t = str2term "-1 * (-2 * (5 / 2 * (13 * x / 2)))";
758 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
759 if term2str t' = "65 * x / 2" then () else error "rational.sml 4";
761 val t = str2term "1 - ((13*x)/2 - 5/2)^^^2";
762 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
763 (*bef.040209: if term2str t' = "(-21 + (130 * x + -169 * x ^^^ 2)) / 4"then()*)
764 if term2str t' = "(-21 + 130 * x + -169 * x ^^^ 2) / 4" then ()
765 else error "rational.sml 5";
767 (*SRAM Schalk I, p.92 Nr. 609a*)
768 val t = str2term "2*(3 - x/5)/3 - 4*(1 - x/3) - x/3 - 2*(x/2 - 1/4)/27 +5/54";
769 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
770 if term2str t' = "(-255 + 112 * x) / 135" then ()
771 else error "rational.sml 6";
773 (*SRAM Schalk I, p.92 Nr. 610c*)
774 val t = str2term "((x- 1)/(x+1) + 1) / ((x- 1)/(x+1) - (x+1)/(x- 1)) - 2";
775 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
776 if term2str t' = "(-3 + -1 * x) / 2" then () else error "rational.sml 7";
778 (*SRAM Schalk I, p.92 Nr. 476a*)
779 val t = str2term "(x^^^2/(1 - x^^^2) + 1)/(x/(1 - x) + 1) * (1 + x)";
780 (*. a/b : c/d translated to a/b * d/c .*)
781 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
782 (*if term2str t' = "1 / 1" then () else error "rational.sml 8";3.6.03*)
783 if term2str t' = "1" then () else error "rational.sml 8";
785 (*............................vvv---TODO: sollte gehen mit poly_order *)
786 (*Schalk I, p.92 Nr. 472a*)
787 val t = str2term "((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/((4*x - 8*y)/(x + y))";
788 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
789 if term2str t' = "x + y" then () else error "rational.sml p.92 Nr. 472a";
791 (*Schalk I, p.70 Nr. 480b; a/b : c/d translated to a/b * d/c*)
792 val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
793 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
794 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
795 "(20*x*y/(x^^^2 - 25*y^^^2))");
796 (*... nicht simpl, zerlegt ...*)
797 val t = str2term ("((12*x*y/(9*x^^^2 - y^^^2))/" ^
798 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2))");
799 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
800 "(-12 * (x * y ^^^ 3) + 108 * (x * (y * x ^^^ 2))) / (12 * (x * y))";
801 (* ~~~~~~~~~~ poly_order notwendig!*)
802 val t = str2term ("(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
803 "(20*x*y/(x^^^2 - 25*y^^^2))");
804 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
805 if term2str t' = "1 / (x ^^^ 2 + -25 * y ^^^ 2)" then ()
806 else error "rational.sml norm_Rational 1 / (x ^^^ 2 + -25 * y ^^^ 2)";
808 "nonterm.SK6 ----- SK060904-2a non-termination of add_fraction_p_";
809 (*WN.2.6.03 from rlang.sml 56a
810 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)";
811 val NONE = rewrite_set_ thy false common_nominator_p t;
814 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
815 val NONE = add_fraction_p_ thy t;
819 (* ------------------------------------------------------------------- *)
820 (*---------vvv------------ MG: ab 1.7.03 ----------------vvv-----------*)
821 (* Simplifier fuer beliebige Buchterme *)
822 (* ------------------------------------------------------------------- *)
823 (*----------------------- norm_Rational_mg ----------------------------*)
824 (* ------------------------------------------------------------------- *)
826 "-------- numeral rationals -----------------------------";
827 "-------- numeral rationals -----------------------------";
828 "-------- numeral rationals -----------------------------";
829 (*SRA Schalk I, p.40 Nr. 164b *)
830 val t = str2term "(47/6 - 76/9 + 13/4)/(35/12)";
831 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
833 if (term2str t) = "19 / 21" then ()
834 else error "rational.sml: diff.behav. in norm_Rational_mg 1";
836 (*SRA Schalk I, p.40 Nr. 166a *)
837 val t = str2term "((5/4)/(4+22/7) + 37/20)*(110/3 - 110/9 * 23/11)";
838 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
840 if (term2str t) = "45 / 2" then ()
841 else error "rational.sml: diff.behav. in norm_Rational_mg 2";
844 "-------- cancellation ----------------------------------";
845 "-------- cancellation ----------------------------------";
846 "-------- cancellation ----------------------------------";
849 "((1 + 9 * a ^^^ 2)*(1 + 3 * a))/((3 * a + 9 * a ^^^ 2)*(1 + 3 * a))";
850 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
853 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
855 else error "rational.sml: diff.behav. in norm_Rational_mg 3";
859 "((x ^^^ 2)*(7 * x + (-1) * y))/((y ^^^ 2)*(7 * x + (-1) * y))";
860 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
865 else error "rational.sml: diff.behav. in norm_Rational_mg 4";
867 (*SRC Schalk I, p.66 Nr. 379c *)
870 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
875 else error "rational.sml: diff.behav. in norm_Rational_mg 5";
877 (*SRC Schalk I, p.66 Nr. 380b *)
879 "15*(3*x+3)*(4*x+9)/(12*(2*x+7)*(5*x+5))";
880 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
883 "(27 + 12 * x) / (28 + 8 * x)"
885 else error "rational.sml: diff.behav. in norm_Rational_mg 6";
887 (*Schalk I, p.60 Nr. 215c *)
888 (* Falsches Ergebnis: rechnet lange und cancel_p kann nicht weiter krzen!!!*)
890 val t = str2term "(a+b)^^^4*(x - y)/((x - y)^^^3*(a+b)^^^2)";
891 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
894 "(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)"
896 else error "rational.sml: diff.behav. in norm_Rational_mg 7";
899 "(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)"
900 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
902 (* uncaught exception nonexhaustive binding failure
903 raised at: stdIn:93.1-93.51 *)
905 (*Schalk I, p.66 Nr. 381a *)
906 (* ACHTUNG: rechnet ca. 2 Minuten !!! *)
908 val t = str2term "18*(a+b)^^^3*(a - b)^^^2/(72*(a - b)^^^3*(a+b)^^^2)";
909 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
912 "(a + b) / (4 * a + -4 * b)"
913 then () else error "rational.sml: diff.behav. in norm_Rational_mg 8";
916 (*SRC Schalk I, p.66 Nr. 381b *)
918 "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
919 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
924 else error "rational.sml: diff.behav. in norm_Rational_mg 9";
926 (*SRC Schalk I, p.66 Nr. 381c *)
928 "(27*a^^^3+9*a^^^2+3*a+1)/(27*a^^^3+18*a^^^2+3*a)";
929 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
932 "(1 + 9 * a ^^^ 2) / (3 * a + 9 * a ^^^ 2)"
934 else error "rational.sml: diff.behav. in norm_Rational_mg 10";
936 (*SRC Schalk I, p.66 Nr. 383a *)
938 "(5*a^^^2 - 5*a*b)/(a - b)^^^2";
939 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
942 "5 * a / (a + -1 * b)"
944 else error "rational.sml: diff.behav. in norm_Rational_mg 11";
947 "-------- common denominator ----------------------------";
948 "-------- common denominator ----------------------------";
949 "-------- common denominator ----------------------------";
950 (*SRA Schalk I, p.67 Nr. 403a *)
953 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
956 "(-3 * x + 4 * y + -1 * x * y) / (x * y)"
958 else error "rational.sml: diff.behav. in norm_Rational_mg 12";
960 (*SRA Schalk I, p.67 Nr. 407b *)
962 "(2*a+3*b)/(b*c) + (3*c+a)/(a*c) - (2*a^^^2+3*b*c)/(a*b*c)";
963 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
968 else error "rational.sml: diff.behav. in norm_Rational_mg 13";
970 (*SRA Schalk I, p.67 Nr. 410b *)
972 "1/(x+1) + 1/(x+2) - 2/(x+3)";
973 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
976 "(5 + 3 * x) / (6 + 11 * x + 6 * x ^^^ 2 + x ^^^ 3)"
978 else error "rational.sml: diff.behav. in norm_Rational_mg 14";
980 (*SRA Schalk I, p.67 Nr. 413b *)
982 "(1+x)/(1 - x) - (1 - x)/(1+x) + 2*x/(1 - x^^^2)";
983 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
986 "6 * x / (1 + -1 * x ^^^ 2)"
988 else error "rational.sml: diff.behav. in norm_Rational_mg 15";
990 (*SRA Schalk I, p.68 Nr. 414a *)
992 "(x + 2)/(x - 1) + (x - 3)/(x - 2) - (x + 1)/((x - 1)*(x - 2))";
993 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
996 "(-2 + -5 * x + 2 * x ^^^ 2) / (2 + -3 * x + x ^^^ 2)"
998 else error "rational.sml: diff.behav. in norm_Rational_mg 16";
1000 (*SRA Schalk I, p.68 Nr. 423a *)
1002 "(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)";
1003 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1008 else error "rational.sml: diff.behav. in norm_Rational_mg 17";
1010 (*SRA Schalk I, p.68 Nr. 428b *)
1012 "1/(a - b)^^^2 + 1/(a+b)^^^2 - 2/(a^^^2 - b^^^2) - 4*(b^^^2 - 1)/(a^^^2 - b^^^2)^^^2";
1013 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1016 "4 / (a ^^^ 4 + -2 * a ^^^ 2 * b ^^^ 2 + b ^^^ 4)"
1018 else error "rational.sml: diff.behav. in norm_Rational_mg 18";
1020 (*SRA Schalk I, p.68 Nr. 430b *)
1022 "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";
1023 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1028 else error "rational.sml: diff.behav. in norm_Rational_mg 19";
1031 (*SRA Schalk I, p.68 Nr. 432 *)
1033 "(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)";
1034 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1039 else error "rational.sml: diff.behav. in norm_Rational_mg 20";
1044 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1047 "(3 * y + b * x) / (b * y)"
1049 else error "rational.sml: diff.behav. in norm_Rational_mg 21";
1052 "-------- multiply and cancel ---------------------------";
1053 "-------- multiply and cancel ---------------------------";
1054 "-------- multiply and cancel ---------------------------";
1055 (*SRM Schalk I, p.68 Nr. 436a *)
1057 "3*(x+y)/(15*(x - y)) * 25*(x - y)^^^2/(18*(x+y)^^^2)";
1058 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1061 "(5 * x + -5 * y) / (18 * x + 18 * y)"
1063 else error "rational.sml: diff.behav. in norm_Rational_mg 22";
1065 (*SRM.test Schalk I, p.68 Nr. 436b *)
1066 (*WN060420???MG3 crashes with method 'simplify' in
1067 IsacCore > Simplification > Rational Terms > Multiplication > No.2*)
1068 val t = str2term "5*a*(a - b)^^^2*(a + b)^^^3/(7*b*(a - b)^^^3) * 7*b/(a + b)^^^3";
1069 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1072 "5 * a / (a + -1 * b)"
1074 else error "rational.sml: diff.behav. in norm_Rational_mg 23";
1076 (*Schalk I, p.68 Nr. 437a *)
1077 val t = str2term "(3*a - 4*b)/(4*c+3*e) * (3*a+4*b)/(9*a^^^2 - 16*b^^^2)";
1078 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1079 if (term2str t) = "1 / (4 * c + 3 * e)" then ()
1080 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1082 "----- S.K. corrected non-termination 060904";
1083 val t = str2term "(3*a - 4*b) * (3*a+4*b)/((4*c+3*e)*(9*a^^^2 - 16*b^^^2))";
1084 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1087 "(9 * a ^^^ 2 + -16 * b ^^^ 2) /\n(36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c +\n -48 * b ^^^ 2 * e)"
1088 (*"(9 * a ^^^ 2 + -16 * b ^^^ 2) / (36 * a ^^^ 2 * c + 27 * a ^^^ 2 * e + -64 * b ^^^ 2 * c + -48 * b ^^^ 2 * e)"*)
1089 then () else error "rational.sml: S.K.8..corrected 060904-6";
1091 "----- S.K. corrected non-termination of cancel_p_";
1092 val t'' = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
1093 "(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
1094 val SOME (t',_) = rewrite_set_ thy false cancel_p t'';
1095 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1096 else error "rational.sml: diff.behav. in cancel_p S.K.8";
1098 (*Schalk I, p.68 Nr. 437b *)
1099 (* nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1100 val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1101 (* val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1104 "================delete===";
1105 (*a casual output from above*)
1107 "(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)";
1108 (* WN060831 nonterm.SK10
1109 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1113 (*SRM Schalk I, p.68 Nr. 438a *)
1115 "x*y/(x*y - y^^^2)*(x^^^2 - x*y)";
1116 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1121 else error "rational.sml: diff.behav. in norm_Rational_mg 24";
1123 (*SRM Schalk I, p.68 Nr. 439b *)
1125 "(4*x^^^2+4*x+1)*((x^^^2 - 2*x^^^3)/(4*x^^^2+2*x))";
1126 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1129 "(x + -4 * x ^^^ 3) / 2"
1131 else error "rational.sml: diff.behav. in norm_Rational_mg 25";
1133 (*SRM Schalk I, p.68 Nr. 440a *)
1135 "(x^^^2 - 2*x)/(x^^^2 - 3*x) * (x - 3)^^^2/(x^^^2 - 4)";
1136 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1139 "(-3 + x) / (2 + x)"
1141 else error "rational.sml: diff.behav. in norm_Rational_mg 26";
1143 "----- Schalk I, p.68 Nr. 440b SK11 works since 0707xx";
1145 "(a^^^3 - 9*a)/(a^^^3*b - a*b^^^3)*(a^^^2*b+a*b^^^2)/(a+3)";
1146 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1147 if term2str t = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1148 else error "rational.sml: diff.behav. in norm_Rational 27";
1150 "----- SK12 works since 0707xx";
1151 val t = str2term "(a^^^3 - 9*a)*(a^^^2*b+a*b^^^2)/((a^^^3*b - a*b^^^3)*(a+3))";
1152 val SOME (t',_) = rewrite_set_ thy false norm_Rational t; term2str t';
1153 if term2str t' = "(-3 * a + a ^^^ 2) / (a + -1 * b)" then ()
1154 else error "rational.sml: diff.behav. in norm_Rational 28";
1157 "-------- common denominator and multiplication ---------";
1158 "-------- common denominator and multiplication ---------";
1159 "-------- common denominator and multiplication ---------";
1160 (*SRAM Schalk I, p.69 Nr. 441b *)
1161 val t = str2term "(4*a/3 + 3*b^^^2/a^^^3 + b/(4*a))*(4*b/(3*a))";
1162 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1165 "(36 * b ^^^ 3 + 3 * a ^^^ 2 * b ^^^ 2 + 16 * a ^^^ 4 * b) / (9 * a ^^^ 4)"
1166 then () else error "rational.sml: diff.behav. in norm_Rational_mg 28";
1168 (*SRAM Schalk I, p.69 Nr. 442b *)
1169 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)";
1170 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1173 "5 * x ^^^ 2 / (a * b ^^^ 3 * c)"
1174 then () else error "rational.sml: diff.behav. in norm_Rational_mg 29";
1176 (*SRAM Schalk I, p.69 Nr. 443b *)
1177 val t = str2term "(a/2 + b/3)*(b/3 - a/2)";
1178 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1181 "(-9 * a ^^^ 2 + 4 * b ^^^ 2) / 36"
1182 then () else error "rational.sml: diff.behav. in norm_Rational_mg 30";
1184 (*SRAM Schalk I, p.69 Nr. 445b *)
1185 val t = str2term "(a^^^2/9 + 2*a/(3*b) + 4/b^^^2)*(a/3 - 2/b) + 8/b^^^3";
1186 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1190 then () else error "rational.sml: diff.behav. in norm_Rational_mg 31";
1192 (*SRAM Schalk I, p.69 Nr. 446b *)
1193 val t = str2term "(x/(5*x + 4*y) - y/(5*x - 4*y) + 1)*(25*x^^^2 - 16*y^^^2)";
1194 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1197 "30 * x ^^^ 2 + -9 * x * y + -20 * y ^^^ 2"
1199 else error "rational.sml: diff.behav. in norm_Rational_mg 32";
1201 (*SRAM Schalk I, p.69 Nr. 449a *)(*Achtung: rechnet ca 8 Sekunden*)
1203 "(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)";
1204 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1206 if (term2str t) = "(-81 * x ^^^ 4 + 16 * x ^^^ 8 * y ^^^ 4) / (81 * y ^^^ 8)"
1207 then () else error "rational.sml: diff.behav. in norm_Rational_mg 33";
1210 (*SRAM Schalk I, p.69 Nr. 450a *)
1212 "(4*x/(3*y)+2*y/(3*x))^^^2 - (2*y/(3*x) - 2*x/y)*(2*y/(3*x)+2*x/y)";
1213 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1216 "(52 * x ^^^ 2 + 16 * y ^^^ 2) / (9 * y ^^^ 2)"
1218 else error "rational.sml: diff.behav. in norm_Rational_mg 34";
1221 "-------- double fractions ------------------------------";
1222 "-------- double fractions ------------------------------";
1223 "-------- double fractions ------------------------------";
1224 (*SRD Schalk I, p.69 Nr. 454b *)
1226 "((2 - x)/(2*a)) / (2*a/(x - 2))";
1227 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1230 "(-4 + 4 * x + -1 * x ^^^ 2) / (4 * a ^^^ 2)"
1232 else error "rational.sml: diff.behav. in norm_Rational_mg 35";
1234 (*SRD Schalk I, p.69 Nr. 455a *)
1236 "(a^^^2 + 1)/(a^^^2 - 1) / ((a+1)/(a - 1))";
1237 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1240 "(1 + a ^^^ 2) / (1 + 2 * a + a ^^^ 2)" then ()
1241 else error "rational.sml: diff.behav. in norm_Rational_mg 36";
1244 "----- Schalk I, p.69 Nr. 455b";
1245 val t = str2term "(x^^^2 - 4)/(y^^^2 - 9)/((2+x)/(3 - y))";
1246 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1247 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1248 else error "rational.sml: diff.behav. in norm_Rational_mg 37";
1250 "----- SK060904-1a non-termination of cancel_p_ ?: worked before 0707xx";
1251 val t = str2term "(x^^^2 - 4)*(3 - y)/((y^^^2 - 9)*(2+x))";
1252 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1253 if term2str t = "(2 + -1 * x) / (3 + y)" then ()
1254 else error "rational.sml: diff.behav. in norm_Rational_mg 37b";
1256 "----- ?: worked before 0707xx";
1257 val t = str2term "(3 + -1 * y) / (-9 + y ^^^ 2)";
1258 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1259 if term2str t = "-1 / (3 + y)" then ()
1260 else error "rational.sml: -1 / (3 + y) norm_Rational";
1262 (*SRD Schalk I, p.69 Nr. 456b *)
1264 "(b^^^3 - b^^^2)/(b^^^2+b)/(b^^^2 - 1)";
1265 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1267 if (term2str t) = "b / (1 + 2 * b + b ^^^ 2)" then ()
1268 else error "rational.sml: diff.behav. in norm_Rational_mg 38";
1270 (*SRD Schalk I, p.69 Nr. 457b *)
1272 "(16*a^^^2 - 9*b^^^2)/(2*a+3*a*b) / ((4*a+3*b)/(4*a^^^2 - 9*a^^^2*b^^^2))";
1273 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1276 "8 * a ^^^ 2 + -6 * a * b + -12 * a ^^^ 2 * b + 9 * a * b ^^^ 2"
1277 then () else error "rational.sml: diff.behav. in norm_Rational_mg 39";
1279 "----- Schalk I, p.69 Nr. 458b works since 0707";
1281 "(2*a^^^2*x - a^^^2)/(a*x - b*x) / (b^^^2*(2*x - 1)/(x*(a - b)))";
1282 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1283 if term2str t = "a ^^^ 2 / b ^^^ 2" then ()
1284 else error "rational.sml: diff.behav. in norm_Rational_mg 39b";
1286 (*SRD Schalk I, p.69 Nr. 459b *)
1287 val t = str2term "(a^^^2 - b^^^2)/(a*b) / (4*(a+b)^^^2/a)";
1288 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1289 if term2str t = "(a + -1 * b) / (4 * a * b + 4 * b ^^^ 2)" then ()
1290 else error "rational.sml: diff.behav. in norm_Rational_mg 41";
1293 (*Schalk I, p.69 Nr. 460b nonterm.SK
1295 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1296 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1299 else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1302 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1303 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1304 ... non terminating.
1305 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1306 "(-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)";
1307 val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1308 ... non terminating.*)
1310 (*SRD Schalk I, p.70 Nr. 472a *)
1311 val t = str2term ("((8*x^^^2 - 32*y^^^2)/(2*x + 4*y))/" ^
1312 "((4*x - 8*y)/(x + y))");
1313 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1318 else error "rational.sml: diff.behav. in norm_Rational_mg 43";
1321 (*----------------------------------------------------------------------*)
1322 (*---------------------- Einfache Dppelbrche --------------------------*)
1323 (*----------------------------------------------------------------------*)
1325 (*SRD Schalk I, p.69 Nr. 461a *)
1327 "(2/(x+3) + 2/(x - 3)) / (8*x/(x^^^2 - 9))";
1328 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1333 else error "rational.sml: diff.behav. in norm_Rational_mg 44";
1335 (*SRD Schalk I, p.69 Nr. 464b *)
1337 "(a - a/(a - 2)) / (a + a/(a - 2))";
1338 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1341 "(3 + -1 * a) / (1 + -1 * a)"
1343 else error "rational.sml: diff.behav. in norm_Rational_mg 45";
1345 (*SRD Schalk I, p.69 Nr. 465b *)
1347 "((x+3*y)/9 + (4*y^^^2 - 9*z^^^2)/(16*x)) /(x/9+y/6+z/4)";
1348 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1351 "(4 * x + 6 * y + -9 * z) / (4 * x)"
1353 else error "rational.sml: diff.behav. in norm_Rational_mg 46";
1355 (*SRD Schalk I, p.69 Nr. 466b *)
1357 "((1 - 7*(x - 2)/(x^^^2 - 4)) / (6/(x+2))) / (3/(x+5)+30/(x^^^2 - 25))";
1358 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1361 "(25 + -10 * x + x ^^^ 2) / 18"
1363 else error "rational.sml: diff.behav. in norm_Rational_mg 47";
1365 (*SRD Schalk I, p.70 Nr. 469 *)
1367 "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))";
1368 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1371 "3 * b ^^^ 3 / (2 * a + -2 * b)"
1373 else error "rational.sml: diff.behav. in norm_Rational_mg 48";
1375 (*----------------------------------------------------------------------*)
1376 (*---------------------- Mehrfache Dppelbrueche ------------------------*)
1377 (*----------------------------------------------------------------------*)
1379 (*SRD.test Schalk I, p.70 Nr. 476b *) (* Rechenzeit: 10 sec *)
1380 (*WN060419 crashes with method 'simplify' ????SK*)
1382 "((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)";
1383 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1384 if term2str t = "1 / (a ^^^ 2 + -1 * b ^^^ 2)" then ()
1385 else error "rational.sml: diff.behav. in norm_Rational_mg 49";
1387 "----- Schalk I, p.70 Nr. 477a";
1388 (* MG Achtung: terme explodieren; Bsp zu komplex;
1389 L???ung sollte (ziemlich grosser) Faktorisierter Ausdruck sein
1390 val t = str2term "b*y/(b - 2*y)/((b^^^2 - y^^^2)/(b+2*y)) /" ^
1391 "(b^^^2*y+b*y^^^2)*(a+x)^^^2/((b^^^2 - 4*y^^^2)*(a+2*x)^^^2)";
1392 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1395 val t = str2term "b*y*(b+2*y)*(b^^^2 - 4*y^^^2)*(a+2*x)^^^2 / " ^
1396 "((b - 2*y)*(b^^^2 - y^^^2)*(b^^^2*y+b*y^^^2)*(a+x)^^^2)";
1397 val SOME (t,_) = rewrite_set_ thy false make_polynomial t;
1401 "----- Schalk I, p.70 Nr. 478b ----- Rechenzeit: 5 sec";
1402 val t = str2term ("(a - (a*b+b^^^2)/(a+b))/(b+(a - b)/(1+(a+b)/(a - b))) / " ^
1403 "((a - a^^^2/(a+b))/(a+(a*b)/(a - b)))");
1404 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1406 "(2 * a ^^^ 3 + 2 * a ^^^ 2 * b) / (a ^^^ 2 * b + b ^^^ 3)"
1408 else error "rational.sml: diff.behav. in norm_Rational_mg 51";
1410 (* TODO.new_c:WN050820 STOP_REW_SUB introduced gave ...
1411 if term2str t' = "(a ^^^ 4 + -1 * a ^^^ 2 * b ^^^ 2) /(a * b * (b + (a * (a + -1 * b) + -1 * b * (a + -1 * b)) / (2 * a)) * (a + -1 * b))" then ()
1412 else error "rational.sml: works again";
1413 re-outcommented with TODO.new_c: cvs before 071227, 11:50*)
1417 (*Schalk I, p.70 Nr. 480a *)
1418 (* Achtung: rechnet ewig; cancel_p kann nicht krzen: WN060831 nonterm.SK00
1420 "(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)))";
1421 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1426 else error "rational.sml: diff.behav. in norm_Rational_mg 52";
1428 (*MG Berechne Zwischenergebnisse: WN060831 nonterm.SK00*)
1430 "(1/x+1/y+1/z)/(1/x - 1/y - 1/z)";
1431 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1433 "(x ^^^ 2 * y ^^^ 2 * z + x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2) /
1434 (-1 * x ^^^ 2 * y ^^^ 2 * z + -1 * x ^^^ 2 * y * z ^^^ 2 + x * y ^^^ 2 * z ^^^ 2)";
1436 "2*x^^^2/(x^^^2 - z^^^2)/(x/(x+z)+x/(x - z))";
1437 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1441 (* SK 1. Ausdruck kann nicht weiter gekrzt werden; cancel_p !!!*)
1442 ### rls: cancel_p on:
1443 (x ^^^ 2 * (y ^^^ 2 * z) + x ^^^ 2 * (y * z ^^^ 2) + x * (y ^^^ 2 * z ^^^ 2)) /
1444 (-1 * (x ^^^ 2 * (y ^^^ 2 * z)) + -1 * (x ^^^ 2 * (y * z ^^^ 2)) + x * (y ^^^ 2 * z ^^^ 2))
1445 GC #3.61.81.101.197.17503: (0 ms)
1446 *** RATIONALS_DIRECT_CANCEL_EXCEPTION: Invalid fraction
1449 "(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))";
1450 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1452 (*uncaught exception nonexhaustive binding failure*)
1454 (* Das kann er aber krzen !!????: *)
1456 "(x^^^2 * (y^^^2 * z) + x * (y^^^2 * z^^^2)) / (-1 * (x^^^2 * (y * z^^^2)) + x * (y^^^2 * z^^^2))";
1457 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1459 "(-1 * (y * x) + -1 * (z * y)) / (1 * (z * x) + -1 * (z * y))";
1463 "-------- crucial examples ------------------------------";
1464 "-------- crucial examples ------------------------------";
1465 "-------- crucial examples ------------------------------";
1466 (*Schalk I, p.60 Nr. 215d *)
1467 (* Achtung: rechnet ewig ...
1468 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1469 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1470 term2str t; noterm.SK
1473 (* Kein Wunder, denn Z???ler und Nenner extra als Polynom dargestellt ergibt:*)
1475 val t = str2term "(a-b)^^^3 * (x+y)^^^4";
1476 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1478 "a^^^3 * x^^^4 + 4 * a^^^3 * x^^^3 * y +6 * a^^^3 * x^^^2 * y^^^2 +4 * a^^^3 * x * y^^^3 +a^^^3 * y^^^4 +-3 * a^^^2 * b * x^^^4 +-12 * a^^^2 * b * x^^^3 * y +-18 * a^^^2 * b * x^^^2 * y^^^2 +-12 * a^^^2 * b * x * y^^^3 +-3 * a^^^2 * b * y^^^4 +3 * a * b^^^2 * x^^^4 +12 * a * b^^^2 * x^^^3 * y +18 * a * b^^^2 * x^^^2 * y^^^2 +12 * a * b^^^2 * x * y^^^3 +3 * a * b^^^2 * y^^^4 +-1 * b^^^3 * x^^^4 +-4 * b^^^3 * x^^^3 * y +-6 * b^^^3 * x^^^2 * y^^^2 +-4 * b^^^3 * x * y^^^3 +-1 * b^^^3 * y^^^4";
1479 val t = str2term "((x+y)^^^2 * (a-b)^^^5)";
1480 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1482 "a^^^5 * x^^^2 + 2 * a^^^5 * x * y + a^^^5 * y^^^2 +-5 * a^^^4 * b * x^^^2 +-10 * a^^^4 * b * x * y +-5 * a^^^4 * b * y^^^2 +10 * a^^^3 * b^^^2 * x^^^2 +20 * a^^^3 * b^^^2 * x * y +10 * a^^^3 * b^^^2 * y^^^2 +-10 * a^^^2 * b^^^3 * x^^^2 +-20 * a^^^2 * b^^^3 * x * y +-10 * a^^^2 * b^^^3 * y^^^2 +5 * a * b^^^4 * x^^^2 +10 * a * b^^^4 * x * y +5 * a * b^^^4 * y^^^2 +-1 * b^^^5 * x^^^2 +-2 * b^^^5 * x * y +-1 * b^^^5 * y^^^2";
1484 (*anscheinend macht dem Rechner das Krzen diese Bruches keinen Spass mehr ...*)
1486 (*--------------------------------------------------------------------*)
1487 (*Schalk I, p.70 Nr. 480b
1488 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
1489 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1490 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1491 "(20*x*y/(x^^^2 - 25*y^^^2))";
1492 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1494 Kann nicht weiter vereinfacht werden !!!!?? *)
1496 (*--------------------------------------------------------------------*)
1497 "---- MGs test set";
1498 val t = str2term " (1 + x^^^5) / (y + x) + x^^^3 / x ";
1499 val SOME (t,_) = rewrite_set_ thy false common_nominator_p t;
1500 if term2str t = "(1 + x ^^^ 3 + x ^^^ 5 + y * x ^^^ 2) / (x + y)" then()
1503 (*--------------------------------------------------------------------*)
1504 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3b
1505 ---> Sortierung FALSCH !! *)
1506 val t = str2term "b^^^3 * a^^^5/a ";
1507 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1509 "1 * (a^^^4 * b^^^3) / 1"; (*OK*)
1511 val t = str2term "b^^^3 * a^^^5/b ";
1512 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1514 "1 * (b^^^2 * a^^^5) / 1"; (*cancel_p sortiert hier falsch um!*)
1516 (* Problem liegt NICHT bei ord_make_polynomial! (siehe folgende Bsple) *)
1518 val x = str2term "x"; val bdv = str2term "bdv";
1519 val t1 = str2term "b^^^2 * a^^^5";
1520 val t2 = str2term "a^^^5 * b^^^2 ";
1521 ord_make_polynomial false Rational.thy [(x,bdv)] (t1,t2); (*false*)
1523 (* ==> "b^^^2 * a^^^5" > "a^^^5 * b^^^2 " ... OK!*)
1525 (*--------------------------------------------------------------------*)
1526 (* cancel_p liefert nicht immer Polynomnormalform (2): WN060831???SK3c
1527 ---> erzeugt berflssige "1 * ..."
1529 val t = str2term "-1 / (3 + y)";
1531 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1534 (********* Das ist das PROBLEM !!!!!!!??? *******************)
1535 (* -1 im Z???ler der Angabe verursacht das Problem !*)
1538 (* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *)
1539 "----- MGs test set";
1540 val t = str2term "(a^^^2 + -1)/(a+1)";
1541 val SOME (t',_) = rewrite_set_ thy false cancel_p t;
1542 if term2str t' = "(-1 + a) / 1" then ()
1543 else error "rational.sml MG tests 3d";
1545 "----- NOT TERMINATING ?: worked before 0707xx";
1546 val t = str2term "(a^^^2 - 1)*(b + 1) / ((b^^^2 - 1)*(a+1))";
1547 val SOME (t'',_) = rewrite_set_ thy false norm_Rational t;
1548 if term2str t'' = "(1 + -1 * a) / (1 + -1 * b)" then ()
1549 else error "rational.sml MG tests 3e";
1551 "----- corrected SK060905";
1552 val t = str2term "(4*x^^^2 - 20*x + 25)/(2*x - 5)^^^3";
1553 val SOME (t',_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1554 if term2str t' = "-1 / (5 + -2 * x)" then ()
1555 else error "rational.sml corrected SK060905";
1558 "-------- examples for Stefan Karnels thesis ------------";
1559 "-------- examples for Stefan Karnels thesis ------------";
1560 "-------- examples for Stefan Karnels thesis ------------";
1561 (*SRAM Schalk I, p.69 Nr. 442b --- abgewandelt*)
1563 "(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))";
1564 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1567 "5 * x ^^^ 2 / (b ^^^ 3 * c)"
1569 else error "rational.sml: diff.behav. in norm_Rational_mg 53";
1572 "-------- me Schalk I No.186 ----------------------------";
1573 "-------- me Schalk I No.186 ----------------------------";
1574 "-------- me Schalk I No.186 ----------------------------";
1575 val fmz = ["Term ((14 * x * y) / ( x * y ))",
1578 ("Rational",["rational","simplification"],
1579 ["simplification","of_rationals"]);
1580 val p = e_pos'; val c = [];
1581 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];
1582 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1583 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1584 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1585 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1586 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1587 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1588 val (p,_,f,nxt,_,pt) = me nxt p c pt;
1589 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1590 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
1591 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1592 val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;(*++ for explicit script*)
1593 case (f2str f, nxt) of
1594 ("14", ("End_Proof'", _)) => ()
1595 | _ => error "rational.sml diff.behav. in me Schalk I No.186";
1598 "-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1599 "-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1600 "-------- interSteps ..Simp_Rat_Double_No-1.xml ---------";
1603 [(["Term (((2 - x)/(2*a)) / (2*a/(x - 2)))", "normalform N"],
1604 ("Rational",["rational","simplification"],
1605 ["simplification","of_rationals"]))];
1608 autoCalculate 1 CompleteCalc;
1609 val ((pt,p),_) = get_calc 1; show_pt pt;
1611 interSteps 1 ([1],Res);
1612 val ((pt,p),_) = get_calc 1; show_pt pt;
1615 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1616 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1617 "-------- interSteps ..Simp_Rat_Cancel_No-1.xml ---------";
1620 [(["Term ((a^2 + -1*b^2) / (a^2 + -2*a*b + b^2))", "normalform N"],
1621 ("Rational",["rational","simplification"],
1622 ["simplification","of_rationals"]))];
1625 autoCalculate 1 CompleteCalc;
1626 val ((pt,p),_) = get_calc 1; show_pt pt;
1627 (*========== inhibit exn 110314 ================================================
1628 (*with explicit script done already... and removed [1,..] at below...
1629 interSteps 1 ([1],Res);
1630 val ((pt,p),_) = get_calc 1; show_pt pt;
1632 interSteps 1 ([2],Res);
1633 val ((pt,p),_) = get_calc 1; show_pt pt;
1635 interSteps 1 ([2,1],Res);
1636 val ((pt,p),_) = get_calc 1; show_pt pt;
1637 val newnds = children (get_nd pt [2,1]) (*see "fun detailrls"*);
1638 (*if length newnds = 12 then () WN060905*)
1639 if length newnds = 13 then ()
1640 else error "rational.sml: interSteps cancel_p rev_rew_p";
1642 val p = ([2,1,9],Res);
1644 val (_, tac, _) = pt_extract (pt, p);
1645 (*case tac of SOME (Rewrite ("sym_real_plus_binom_times1", _)) => ()
1647 case tac of SOME (Rewrite ("sym_real_add_mult_distrib2", _)) => ()
1648 | _ => error "rational.sml: getTactic, sym_real_plus_binom_times1";
1649 ============ inhibit exn 110314 ==============================================*)
1652 "-------- investigate rulesets for cancel_p -------------";
1653 "-------- investigate rulesets for cancel_p -------------";
1654 "-------- investigate rulesets for cancel_p -------------";
1655 val thy = @{theory "Rational"};
1656 "---------------- (a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1657 val t = str2term "(a^^^2 + -1*b^^^2) / (a^^^2 + -2*a*b + b^^^2)";
1658 val tt = str2term "(1 * a + 1 * b) * (1 * a + -1 * b)"(*numerator only*);
1659 "----- with rewrite_set_";
1660 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1661 term2str tt'= "a ^^^ 2 + -1 * b ^^^ 2" (*true*);
1662 val tt = str2term "((1 * a + -1 * b) * (1 * a + -1 * b))"(*denominator only*);
1663 val SOME (tt',asm) = rewrite_set_ thy false make_polynomial tt;
1664 term2str tt' = "a ^^^ 2 + -2 * a * b + b ^^^ 2" (*true*);
1666 "----- with make_deriv";
1667 val SOME (tt, _) = factout_p_ thy t; term2str tt =
1668 "(1 * a + 1 * b) * (1 * a + -1 * b) / ((1 * a + -1 * b) * (1 * a + -1 * b))";
1670 "--- with ruleset as before 060829";
1671 val {rules, rew_ord=(_,ro),...} =
1672 rep_rls (assoc_rls "make_polynomial");
1673 val der = make_deriv thy Atools_erls rules ro NONE tt;
1674 print_depth 99; map (term2str o #1) der; print_depth 3;
1675 print_depth 99; map (rule2str o #2) der; print_depth 3;
1676 ... did not terminate*)
1677 "--- with simpler ruleset";
1678 val {rules, rew_ord=(_,ro),...} =
1679 rep_rls (assoc_rls "rev_rew_p");
1680 val der = make_deriv thy Atools_erls rules ro NONE tt;
1681 print_depth 99; writeln (deriv2str der); print_depth 3;
1683 print_depth 99; map (term2str o #1) der; print_depth 3;
1684 "...,(-1 * b ^^^ 2 + a ^^^ 2) / (-2 * (a * b) + a ^^^ 2 + (-1 * b) ^^^ 2) ]";
1685 print_depth 99; map (rule2str o #2) der; print_depth 3;
1686 print_depth 99; map (term2str o #1 o #3) der; print_depth 3;
1688 val der = make_deriv thy Atools_erls rules ro NONE
1689 (str2term "(1 * a + 1 * b) * (1 * a + -1 * b)");
1690 print_depth 99; writeln (deriv2str der); print_depth 3;
1692 val {rules, rew_ord=(_,ro),...} =
1693 rep_rls (assoc_rls "rev_rew_p");
1694 val der = make_deriv thy Atools_erls rules ro NONE
1695 (str2term "(1 * a + -1 * b) * (1 * a + -1 * b)");
1696 print_depth 99; writeln (deriv2str der); print_depth 3;
1697 print_depth 99; map (term2str o #1) der; print_depth 3;
1698 (*WN060829 ...postponed*)
1701 "-------- investigate format of factout_ and factout_p_ -";
1702 "-------- investigate format of factout_ and factout_p_ -";
1703 "-------- investigate format of factout_ and factout_p_ -";
1704 val {rules, rew_ord = (_,ro),...} = rep_rls (assoc_rls "make_polynomial");
1705 val (thy, eval_rls) = (@{theory "Rational"}, Atools_erls)(*see 'fun init_state'*);
1706 val Rrls {scr = Rfuns {init_state,...},...} = assoc_rls "cancel_p";
1708 "----- see Rational.ML, local cancel_p, fun init_state";
1709 val t = str2term "(a^^^2 + (-1)*b^^^2) / (a^^^2 + (-2)*a*b + b^^^2)";
1710 val SOME (t',_) = factout_p_ thy t; term2str t';
1712 val rtas = reverse_deriv thy eval_rls rules ro NONE t';
1713 writeln(trtas2str rst);
1717 "----- see Rational.ML, local cancel_p, fun init_state";
1718 val t = str2term "a^^^2 / a";
1719 val SOME (t',_) = factout_p_ thy t;
1720 term2str t' = "a * a / (1 * a)" (*true*);
1721 (*... can be canceled with
1722 real_mult_div_cancel2 ?k ~= 0 ==> ?m * ?k / (?n * ?k) = ?m / ?n"*)
1723 (* sml/ME/rewtools.sml:
1724 val rtas = reverse_deriv thy Atools_erls rules ro NONE t';
1725 writeln (deri2str rtas);
1729 "-------- SK 060904 ----------------------------------------------";
1730 "----- order on polynomials -- input + output";
1731 val thy = @{theory "Isac"};
1732 val t = str2term "(a + -1 * b) / (-1 * a + b)";
1733 val SOME (t', _) = factout_p_ thy t; term2str t';
1734 val SOME (t', _) = cancel_p_ thy t; term2str t';
1736 val t = str2term "a*b*c*d / (d*e*f*g)";
1737 val SOME (t', _) = cancel_p_ thy t; term2str t';
1739 val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
1740 val SOME (t', _) = cancel_p_ thy t; term2str t';
1743 "----- SK060904-1a non-termination of cancel_p_ ? worked before 0707xx";
1744 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
1745 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1746 if term2str t' = "(2 + -1 * x) / (3 + y)" then ()
1747 else error "rational.sml SK060904-1a worked since 0707xx";
1749 "----- SK060904-1b non-termination of cancel_p_ ... worked before 0707xx";
1750 val t = str2term ("(9 * a ^^^ 2 + -16 * b ^^^ 2) /" ^
1751 "(36 * a^^^2 * c + (27 * a^^^2 * e + (-64 * b^^^2 * c + -48 * b^^^2 * e)))");
1752 val SOME (t',_) = cancel_p_ thy t;
1753 if term2str t' = "1 / (4 * c + 3 * e)" then ()
1754 else error "rational.sml SK060904-1b";
1757 "----- SK060904-2a non-termination of add_fraction_p_";
1758 val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1759 " (-1 * a + b * x) / (a + b * x) ");
1761 val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
1763 common_nominator_p_ thy t;
1764 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + " ^
1765 " (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
1767 add_fraction_p_ thy t;
1768 " ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
1769 " ((a + b * x)*(-1 * a + b * x)) ";
1773 "-------- how to stepwise construct Scripts -------------";
1774 "-------- how to stepwise construct Scripts -------------";
1775 "-------- how to stepwise construct Scripts -------------";
1776 val thy = @{theory "Rational"};
1778 val p1 = parse thy (
1779 "Script SimplifyScript (t_t::real) = " ^
1780 " (Rewrite_Set discard_minus False " ^
1783 (*required (): (Rewrite_Set discard_minus False)*)
1784 val p2 = parse thy (
1785 "Script SimplifyScript (t_t::real) = " ^
1786 " (Rewrite_Set discard_minus False " ^
1789 val p3 = parse thy (
1790 "Script SimplifyScript (t_t::real) = " ^
1791 " ((Rewrite_Set discard_minus False) " ^
1794 val p4 = parse thy (
1795 "Script SimplifyScript (t_t::real) = " ^
1796 " ((Rewrite_Set discard_minus False) " ^
1799 val p5 = parse thy (
1800 "Script SimplifyScript (t_t::real) = " ^
1801 " ((Try (Rewrite_Set discard_minus False) " ^
1802 " Try (Rewrite_Set discard_parentheses False)) " ^
1805 val p6 = parse thy (
1806 "Script SimplifyScript (t_t::real) = " ^
1807 " ((Try (Rewrite_Set discard_minus False) @@ " ^
1808 " Try (Rewrite_Set rat_mult_poly False) @@ " ^
1809 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@ " ^
1810 " Try (Rewrite_Set cancel_p_rls False) @@ " ^
1812 " ((Try (Rewrite_Set common_nominator_p_rls False) @@ " ^
1813 " Try (Rewrite_Set rat_mult_div_pow False) @@ " ^
1814 " Try (Rewrite_Set make_rat_poly_with_parentheses False) @@" ^
1815 " Try (Rewrite_Set cancel_p_rls False) @@ " ^
1816 " Try (Rewrite_Set rat_reduce_1 False)))) @@ " ^
1817 " Try (Rewrite_Set discard_parentheses False)) " ^
1821 "----------- get_denominator ----------------------------";
1822 "----------- get_denominator ----------------------------";
1823 "----------- get_denominator ----------------------------";
1824 val thy = @{theory Isac};
1825 val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
1826 val SOME (_, t') = eval_get_denominator "" 0 t thy;
1827 if term2str t' = "get_denominator ((a + x) / b) = b" then ()
1828 else error "get_denominator ((a + x) / b) = b"
1831 "--------- several errpats in complicated term -------------------";
1832 "--------- several errpats in complicated term -------------------";
1833 "--------- several errpats in complicated term -------------------";
1834 (*TODO: instead of Gabriella's example here (27.Jul.12) find a simpler one*)
1837 [(["Term ((5*b + 25)/(a^2 - b^2) * (a - b)/(5*b))", "normalform N"],
1838 ("Rational",["rational","simplification"], ["simplification","of_rationals"]))];
1841 autoCalculate 1 CompleteCalc;
1842 val ((pt,p),_) = get_calc 1; show_pt pt;
1844 "-------- nonterminating cancel_p, norm_Rational 2002 ---";
1845 "-------- nonterminating cancel_p, norm_Rational 2002 ---";
1846 "-------- nonterminating cancel_p, norm_Rational 2002 ---";
1847 (*------------------------------------------------------------------------------------\
1848 "--- WN121204: searched rational.sml for "nonterm", added new numbering" ^
1849 " and thoroughly tested with this numbering subsequently";
1851 WN.2.6.03 from rlang.sml 56a
1852 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)";
1853 val NONE = rewrite_set_ thy false common_nominator_p t;
1855 WN060831 nonterm.SK7
1856 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1857 val NONE = add_fraction_p_ thy t;
1859 nonterm.SK9 loops: cancel_p kann nicht weiter kuerzen!!! *)
1860 val t'' = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1861 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t'';
1864 "(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)";
1865 WN060831 nonterm.SK10
1866 val SOME (t,_) = rewrite_set_ thy false cancel_p t;
1870 "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1871 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1874 else error "rational.sml: diff.behav. in norm_Rational_mg 42";
1877 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1878 val SOME (t',_) = rewrite_set_ thy false norm_Rational t;
1879 ... non terminating.
1881 val SOME (t',_) = rewrite_set_ thy false make_polynomial t;
1882 "(-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)";
1883 val SOME (t,_) = rewrite_set_ thy false cancel_p t';
1885 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1886 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1888 val t = str2term "((12*x*y/(9*x^^^2 - y^^^2))/" ^
1889 "(1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1890 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2)/" ^
1891 "(20*x*y/(x^^^2 - 25*y^^^2))";
1892 val SOME (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
1894 SK060904-2a non-termination of add_fraction_p_";
1895 val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + " ^
1896 " (-1 * a + b * x) / (a + b * x) ");
1897 (* nonterm.SK = WN130830
1898 val SOME (t',_) = rewrite_set_ thy false common_nominator_p t;
1900 common_nominator_p_ thy t;
1901 " (a + b * x)*(a + b * x) / ((a + -1 * (b * x))*(a + -1 * (b * x))) + " ^
1902 " (-1 * a + b * x)*(a + -1 * (b * x)) / ((a + b * x)*(-1 * a + b * x)) ";
1904 add_fraction_p_ thy t;
1905 " ((a + b * x)*(a + b * x) + (-1 * a + b * x)*(a + -1 * (b * x))) /" ^
1906 " ((a + b * x)*(-1 * a + b * x)) ";
1907 --------------------------------------------------------------------------------------/*)
1909 (*------------------------------------------------------------------------------------\
1910 "WN121205: thoroughly tested with the above numbering.";
1911 " errors in cancel_p: --- 4,5,6,7.";
1912 " error in common_nominator_p, common_nominator_p_: --- 10; 1,2?.";
1913 " errors caused by ruleset norm_Rational: --- 8,9.";
1914 trace_rewrite := false;
1916 "--- 1 ---: non-terminating with ### add_fract: done t22 "; = WN130830
1917 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)";
1918 trace_rewrite := false;
1919 rewrite_set_ thy false common_nominator_p t;
1921 "--- 2 ---: non-terminating with ### add_fract: done t22 ";
1922 val t = str2term "(a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)";
1923 add_fraction_p_ thy t;
1925 "--- 3 ---: norm_Rational calls Rrls cancel_p with non-normalised polys";
1926 val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
1927 rewrite_set_ thy false norm_Rational t;
1928 (*tracing end...#### rls: cancel_p on:
1929 (a * x ^^^ 2 + -2 * (a * (x * y)) + a * y ^^^ 2 + b * x ^^^ 2 + -2 * (b * (x * y)) + b * y ^^^ 2) /
1930 (a ^^^ 2 * x ^^^ 2 + -1 * (a ^^^ 2 * y ^^^ 2) + -1 * (b ^^^ 2 * x ^^^ 2) + b ^^^ 2 * y ^^^ 2) *)
1932 "--- 4 ---: non-terminating with Rrls cancel_p on plausible input";
1934 "(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /"^
1935 "(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)");
1936 rewrite_set_ thy false cancel_p t;
1937 (*# rls: cancel_p on:
1938 (a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /
1939 (a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2) *)
1941 "--- 5 ---: non-terminating with Rrls cancel_p on plausible input";
1942 val t = str2term "(9*(x^^^2 - 8*x+16)/(4*(y^^^2 - 2*y+1)))/((3*x - 12)/(16*y - 16))";
1943 rewrite_set_ thy false norm_Rational t;
1944 (*#### rls: cancel_p on:
1945 (2304 + -1152 * x + -2304 * y + 144 * x ^^^ 2 + 1152 * (x * y) + -144 * (x ^^^ 2 * y)) /
1946 (48 + -12 * x + -96 * y + 24 * (x * y) + 48 * y ^^^ 2 + -12 * (x * y ^^^ 2)) *)
1948 "--- 6 ---: non-terminating with Rrls cancel_p on plausible input";
1950 "9*(x^^^2 - 8*x+16)*(16*y - 16)/(4*(y^^^2 - 2*y+1)*(3*x - 12))";
1951 rewrite_set_ thy false norm_Rational t;
1952 (*### rls: cancel_p on: (-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * (x * y) +
1953 144 * (x ^^^ 2 * y)) /
1954 (-48 + 12 * x + 96 * y + -24 * (x * y) + -48 * y ^^^ 2 + 12 * (x * y ^^^ 2)) *)
1956 "--- 7 ---: non-terminating with Rrls cancel_p on plausible input";
1958 "(-2304 + 1152 * x + 2304 * y + -144 * x ^^^ 2 + -1152 * x * y + 144 * x ^^^ 2 * y) /"^
1959 "(-48 + 12 * x + 96 * y + -24 * x * y + -48 * y ^^^ 2 + 12 * x * y ^^^ 2)");
1960 rewrite_set_ thy false cancel_p t';
1962 "--- 8 ---: bottom of output cannot be looked ad (due to looping?)";
1963 val t = str2term "(a-b)^^^3 * (x+y)^^^4 / ((x+y)^^^2 * (a-b)^^^5)";
1964 val SOME (t,_) = rewrite_set_ thy false norm_Rational t;
1966 "--- 9 ---: probably error in norm_Rational";
1968 "((12*x*y / (9*x^^^2 - y^^^2)) / (1/(3*x - y)^^^2 - 1/(3*x + y)^^^2)) *" ^
1969 "(1/(x - 5*y)^^^2 - 1/(x + 5*y)^^^2) / (20*x*y/(x^^^2 - 25*y^^^2))");
1970 rewrite_set_ thy false norm_Rational t;
1971 (*#### rls: cancel_p on: (19440 * (x ^^^ 8 * y ^^^ 2) + -490320 * (x ^^^ 6 * y ^^^ 4) +
1972 108240 * (x ^^^ 4 * y ^^^ 6) +
1973 -6000 * (x ^^^ 2 * y ^^^ 8)) /
1974 (2160 * (x ^^^ 8 * y ^^^ 2) + -108240 * (x ^^^ 6 * y ^^^ 4) +
1975 1362000 * (x ^^^ 4 * y ^^^ 6) +
1976 -150000 * (x ^^^ 2 * y ^^^ 8)) *)
1978 "--- 10 ---: non-terminating with ### add_fract: done t22: error in common_nominator_p ";
1979 val t = str2term (" (a + b * x) / (a + -1 * (b * x)) + (-1 * a + b * x) / (a + b * x)");
1980 rewrite_set_ thy false common_nominator_p t; (*### add_fract: done t22 *)
1981 common_nominator_p_ thy t; (*loops without output*)
1982 "--- reformulated 10:";
1983 val t = str2term "(a + -1 * (b * x)) / (a + b * x)";
1984 rewrite_set_ thy false cancel_p t = NONE;
1987 "...both are to be considered after common_nominator_p_ is improved";
1988 --------------------------------------------------------------------------------------/*)
1989 ============ inhibit exn WN130824 TODO ======================================================*)