14 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
14 "-------- integration lev.1 fun cancel_p_ ------------------------------------"; |
15 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
15 "-------- integration lev.1 fun common_nominator_p_ --------------------------"; |
16 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
16 "-------- integration lev.1 fun add_fraction_p_ ------------------------------"; |
17 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------"; |
17 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------"; |
18 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; |
18 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------"; |
|
19 "-------- rls norm_Rational downto fun gcd_poly ------------------------------"; |
19 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
20 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
20 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; |
21 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------"; |
21 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
22 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------"; |
22 "-------- reverse rewrite ----------------------------------------------------"; |
23 "-------- reverse rewrite ----------------------------------------------------"; |
23 "-------- 'reverse-ruleset' cancel_p -----------------------------------------"; |
24 "-------- 'reverse-ruleset' cancel_p -----------------------------------------"; |
328 val a = [(9, [5, 2, 4])]: poly |
329 val a = [(9, [5, 2, 4])]: poly |
329 val b = [(15, [6, 3, 1])]: poly |
330 val b = [(15, [6, 3, 1])]: poly |
330 val ((a', b'), c) = gcd_poly a b |
331 val ((a', b'), c) = gcd_poly a b |
331 *) |
332 *) |
332 |
333 |
|
334 "-------- rls norm_Rational downto fun gcd_poly ------------------------------"; |
|
335 "-------- rls norm_Rational downto fun gcd_poly ------------------------------"; |
|
336 "-------- rls norm_Rational downto fun gcd_poly ------------------------------"; |
|
337 val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))"; |
|
338 trace_rewrite := false (*true false*); |
|
339 (* trace stops with ...: (and then jEdit hangs).. |
|
340 rewrite_set_ thy false norm_Rational t; |
|
341 : |
|
342 ### rls: cancel_p on: (-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) / |
|
343 (-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2) |
|
344 *) |
|
345 val t = str2term (*copy from above: "::real" is not required due to "^^^"*) |
|
346 ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^ |
|
347 "(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)"); |
|
348 (*cancel_p_ thy t; |
|
349 exception Div raised*) |
|
350 |
|
351 "~~~~~ fun cancel_p_, args:"; val (t) = (t); |
|
352 val opt = check_fraction t; |
|
353 val SOME (numerator, denominator) = opt |
|
354 val vs = t |> vars |> map free2str |> sort string_ord |
|
355 val baseT = type_of numerator |
|
356 val expT = HOLogic.realT; |
|
357 print_depth 3; (*999*) |
|
358 val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator); |
|
359 print_depth 3; (*999*) |
|
360 (* does not terminate instead of returning ?: |
|
361 val ((a', b'), c) = gcd_poly a b |
|
362 val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly |
|
363 val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly |
|
364 *) |
|
365 |
333 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
366 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
334 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
367 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
335 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
368 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----"; |
336 val thy = @{theory "Rational"}; |
369 val thy = @{theory "Rational"}; |
337 "-------- WN"; |
370 "-------- WN"; |