1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Mon Sep 16 10:46:51 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Mon Sep 16 11:28:43 2013 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
     1.5  "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
     1.6  "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
     1.7 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
     1.8  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
     1.9  "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
    1.10  "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
    1.11 @@ -330,6 +331,38 @@
    1.12                val ((a', b'), c) = gcd_poly a b
    1.13  *)
    1.14  
    1.15 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    1.16 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    1.17 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    1.18 +val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
    1.19 +trace_rewrite := false (*true false*);
    1.20 +(* trace stops with ...: (and then jEdit hangs)..
    1.21 +rewrite_set_ thy false norm_Rational t;
    1.22 +:
    1.23 +###  rls: cancel_p on: (-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /
    1.24 +(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)
    1.25 +*)
    1.26 +val t = str2term (*copy from above: "::real" is not required due to "^^^"*)
    1.27 +  ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
    1.28 +  "(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)");
    1.29 +(*cancel_p_ thy t;
    1.30 +exception Div raised*)
    1.31 +
    1.32 +"~~~~~ fun cancel_p_, args:"; val (t) = (t);
    1.33 +val opt = check_fraction t;
    1.34 +val SOME (numerator, denominator) = opt
    1.35 +        val vs = t |> vars |> map free2str |> sort string_ord
    1.36 +        val baseT = type_of numerator
    1.37 +        val expT = HOLogic.realT;
    1.38 +print_depth 3; (*999*)
    1.39 +val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
    1.40 +print_depth 3; (*999*)
    1.41 +(* does not terminate instead of returning ?:
    1.42 +        val ((a', b'), c) = gcd_poly a b
    1.43 +val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
    1.44 +val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly
    1.45 +*)
    1.46 +
    1.47  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
    1.48  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
    1.49  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";