1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 16 10:46:51 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 16 11:28:43 2013 +0200
     1.3 @@ -658,14 +658,14 @@
     1.4  
     1.5  subsection {* gcd_poly algorithm, code for [1] p.95 *}
     1.6  ML {*
     1.7 -  fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2)
     1.8 +  fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2) 
     1.9  
    1.10    (* naming of n, M, m, r, ...  follows Winkler p. 95 
    1.11      assumes: n = length es1 = length es2
    1.12      r: *)
    1.13 -  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom]
    1.14 -    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom]
    1.15 -    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
    1.16 +  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom] 
    1.17 +    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom] 
    1.18 +    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = 
    1.19        if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
    1.20          if n > 1
    1.21          then

     2.1 --- a/test/Tools/isac/Knowledge/rational.sml	Mon Sep 16 10:46:51 2013 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Mon Sep 16 11:28:43 2013 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4  "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
     2.5  "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
     2.6  "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
     2.7 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
     2.8  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
     2.9  "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
    2.10  "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
    2.11 @@ -330,6 +331,38 @@
    2.12                val ((a', b'), c) = gcd_poly a b
    2.13  *)
    2.14  
    2.15 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    2.16 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    2.17 +"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
    2.18 +val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
    2.19 +trace_rewrite := false (*true false*);
    2.20 +(* trace stops with ...: (and then jEdit hangs)..
    2.21 +rewrite_set_ thy false norm_Rational t;
    2.22 +:
    2.23 +###  rls: cancel_p on: (-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /
    2.24 +(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)
    2.25 +*)
    2.26 +val t = str2term (*copy from above: "::real" is not required due to "^^^"*)
    2.27 +  ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
    2.28 +  "(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)");
    2.29 +(*cancel_p_ thy t;
    2.30 +exception Div raised*)
    2.31 +
    2.32 +"~~~~~ fun cancel_p_, args:"; val (t) = (t);
    2.33 +val opt = check_fraction t;
    2.34 +val SOME (numerator, denominator) = opt
    2.35 +        val vs = t |> vars |> map free2str |> sort string_ord
    2.36 +        val baseT = type_of numerator
    2.37 +        val expT = HOLogic.realT;
    2.38 +print_depth 3; (*999*)
    2.39 +val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
    2.40 +print_depth 3; (*999*)
    2.41 +(* does not terminate instead of returning ?:
    2.42 +        val ((a', b'), c) = gcd_poly a b
    2.43 +val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
    2.44 +val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly
    2.45 +*)
    2.46 +
    2.47  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
    2.48  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
    2.49  "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";