# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1378126617 -7200
# Node ID 2a95fc276d0a0d91281a3d1b70982a0950a441de
# Parent  bb49dd92fa04f85e5685d7a29cd76518492400c6
GCD_Poly_ML: generalised gcd_poly handling monomials

this also fixes bug in 6ceee9c5d6fd, which had been fixed in bb49dd92fa04 half-assed.

diff -r bb49dd92fa04 -r 2a95fc276d0a src/Tools/isac/Knowledge/GCD_Poly_ML.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Sun Sep 01 16:50:51 2013 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 02 14:56:57 2013 +0200
@@ -658,10 +658,13 @@
 
 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)
+
   (* naming of n, M, m, r, ...  follows Winkler p. 95 
-    n: amount of variables 
+    assumes: n = length es1 = length es2
     r: *)
-  fun gcd_poly' [(c1, es1)] [(c2, es2)] _ _ = [(Integer.gcd c1 c2, map2 Integer.min es1 es2)]
+  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
@@ -677,7 +680,10 @@
           end
 
   (* fn: poly -> poly -> int -> 
-                      int -> int -> int list -> poly list -> poly*)
+                      int -> int -> int list -> poly list -> poly
+     assumes length a > 1  \<and>  length b > 1
+     yields TODO  
+  *)
   and try_new_r a b n M r r_list steps = 
      let 
         val r = find_new_r a b r;
@@ -688,7 +694,10 @@
       in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end
   (* fn: poly -> poly -> int -> 
                            int -> int -> int -> int list -> poly list -> 
-                           |                  poly -> poly -> int list -> poly*)
+                           |                  poly -> poly -> int list -> poly
+     assumes length a > 1  \<and>  length b > 1
+     yields TODO  
+  *)
   and HENSEL_lifting a b n M m r r_list steps g g_n mult =
     if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else
       try_new_r a b n M r r_list steps 
diff -r bb49dd92fa04 -r 2a95fc276d0a test/Tools/isac/Knowledge/gcd_poly_ml.sml
--- a/test/Tools/isac/Knowledge/gcd_poly_ml.sml	Sun Sep 01 16:50:51 2013 +0200
+++ b/test/Tools/isac/Knowledge/gcd_poly_ml.sml	Mon Sep 02 14:56:57 2013 +0200
@@ -741,7 +741,6 @@
 "----------- fun gcd_poly'  ------------------------------";
 "----------- fun gcd_poly'  ------------------------------";
 "----------- fun gcd_poly'  ------------------------------";
-
 if gcd_poly' [(~3,[2,0]),(1,[5,0]),(3,[0,1]),(~6,[1,1]),(~1,[3,1]),(2,[4,1]),(1,[3,2]),(~1,[1,3]),(2,[2,3])]
 [(2,[2,0]),(~2,[0,1]),(4,[1,1]),(~1,[3,1]),(1,[1,2]),(~1,[2,2]),(~1,[0,3]),(2,[1,3])] 2 0 
 = [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])] then () else error 
@@ -750,7 +749,7 @@
 "= [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])] changed";
 (* -xy +xy^2z+yz - 1*)(* xy +1*) (*=*) (*xy -1*)
 if gcd_poly' [(~1,[0,0,0]),(1,[0,1,1]),(1,[1,2,1]),(~1,[1,1,0])] [(1,[0,0,0]),(1,[1,1,0])] 3 0 
-= [(1, [0, 0, 0]), (1, [1, 1, 0])] then () else error
+ = [(~1, [0, 0, 0]), (~1, [1, 1, 0])] then () else error
 "gcd_poly' [(~1,[0,0,0]),(1,[0,1,1]),(1,[1,2,1]),(~1,[1,1,0])] [(1,[0,0,0]),(1,[1,1,0])] 3 0 "
 "= [(1, [0, 0, 0]), (1, [1, 1, 0])] changed";
 
@@ -810,6 +809,16 @@
 val ((a', b'), c) = gcd_poly a b;
 if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "regression test changed";
 
+(* regression test for --- integration lev.1 -- lev.5 in rational.sml *)
+val a = [(1, [0, 1, 1, 0, 1]), (1, [1, 0, 0, 1, 1])]: poly
+val b = [(1, [0, 1, 0, 1, 1])]: poly
+val ((a', b'), c) = gcd_poly a b;
+
+a' = [(1, [0, 1, 1, 0, 0]), (1, [1, 0, 0, 1, 0])];
+b' = [(1, [0, 1, 0, 1, 0])];
+c = [(1, [0, 0, 0, 0, 1])];
+if a = (a' %%*%% c) andalso b = (b' %%*%% c) then () else error "gcd_monom changed";
+
 "----------- fun gcd_poly downto division by zero -------";
 "----------- fun gcd_poly downto division by zero -------";
 "----------- fun gcd_poly downto division by zero -------";