# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1379323723 -7200
# Node ID 83166e7c7e529da1070715c2f54dd3c2f8b3af80
# Parent  0d13f07d8e2a7261235325c347692d4c5f2d48f2
gcd_poly requires special handling for a monomial argument

diff -r 0d13f07d8e2a -r 83166e7c7e52 src/Tools/isac/Knowledge/GCD_Poly_ML.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 16 10:46:51 2013 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 16 11:28:43 2013 +0200
@@ -658,14 +658,14 @@
 
 subsection {* gcd_poly algorithm, code for [1] p.95 *}
 ML {*
-  fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2)
+  fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2) 
 
   (* naming of n, M, m, r, ...  follows Winkler p. 95 
     assumes: n = length es1 = length es2
     r: *)
-  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom]
-    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom]
-    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
+  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom] 
+    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom] 
+    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = 
       if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
         if n > 1
         then
diff -r 0d13f07d8e2a -r 83166e7c7e52 test/Tools/isac/Knowledge/rational.sml
--- a/test/Tools/isac/Knowledge/rational.sml	Mon Sep 16 10:46:51 2013 +0200
+++ b/test/Tools/isac/Knowledge/rational.sml	Mon Sep 16 11:28:43 2013 +0200
@@ -16,6 +16,7 @@
 "-------- integration lev.1 fun add_fraction_p_ ------------------------------";
 "-------- and app_rev ...traced down from rewrite_set_ until prepats ---------";
 "-------- fun rewrite_set_ cancel_p downto fun gcd_poly ----------------------";
+"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
 "-------- rewrite_set_ common_nominator_p from: Mathematik 1 Schalk ----------";
 "-------- integration lev.1 -- lev.5: cancel_p_ & common_nominator_p_ --------";
@@ -330,6 +331,38 @@
               val ((a', b'), c) = gcd_poly a b
 *)
 
+"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
+"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
+"-------- rls norm_Rational downto fun gcd_poly ------------------------------";
+val t = str2term "(x^^^2 - 4)*(3 - y) / ((y^^^2 - 9)*(2+x))";
+trace_rewrite := false (*true false*);
+(* trace stops with ...: (and then jEdit hangs)..
+rewrite_set_ thy false norm_Rational t;
+:
+###  rls: cancel_p on: (-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /
+(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)
+*)
+val t = str2term (*copy from above: "::real" is not required due to "^^^"*)
+  ("(-12 + 4 * y + 3 * x ^^^ 2 + -1 * (x ^^^ 2 * y)) /" ^
+  "(-18 + -9 * x + 2 * y ^^^ 2 + x * y ^^^ 2)");
+(*cancel_p_ thy t;
+exception Div raised*)
+
+"~~~~~ fun cancel_p_, args:"; val (t) = (t);
+val opt = check_fraction t;
+val SOME (numerator, denominator) = opt
+        val vs = t |> vars |> map free2str |> sort string_ord
+        val baseT = type_of numerator
+        val expT = HOLogic.realT;
+print_depth 3; (*999*)
+val (SOME a, SOME b) = (poly_of_term vs numerator, poly_of_term vs denominator);
+print_depth 3; (*999*)
+(* does not terminate instead of returning ?:
+        val ((a', b'), c) = gcd_poly a b
+val a = [(~12, [0, 0]), (3, [2, 0]), (4, [0, 1]), (~1, [2, 1])]: poly
+val b = [(~18, [0, 0]), (~9, [1, 0]), (2, [0, 2]), (1, [1, 2])]: poly
+*)
+
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";
 "-------- rewrite_set_ cancel_p from: Mathematik 1 Schalk Reniets Verlag -----";