# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1369392015 -7200
# Node ID 1676be88dbcbdb88ded7913368b9252cd75302d7
# Parent  4d4254cc6e3454bab6e11b23c30a028ceb319fc3
tuned

diff -r 4d4254cc6e34 -r 1676be88dbcb src/Tools/isac/Knowledge/GCD_Poly.thy
--- a/src/Tools/isac/Knowledge/GCD_Poly.thy	Fri May 24 10:41:57 2013 +0200
+++ b/src/Tools/isac/Knowledge/GCD_Poly.thy	Fri May 24 12:40:15 2013 +0200
@@ -382,7 +382,10 @@
 
     argumentns "a b d M p" named according to [1] p.93 *)
   fun HENSEL_lifting_up a b d M p = 
-    let 
+    let
+val _ = writeln ("HENSEL-univ d = " ^ PolyML.makestring d ^ 
+", M = " ^ PolyML.makestring (2 * d * LANDAU_MIGNOTTE_bound a b) ^ 
+", p = " ^ PolyML.makestring p)
       val p = p next_prime_not_dvd d 
       val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p (*see above*)
     in
@@ -391,9 +394,7 @@
           val g = primitive_up (try_new_prime_up a b d M p g_p p)
         in
           if (g %|% a) andalso (g %|% b) then 
-(writeln ("HENSEL-univ M = " ^ PolyML.makestring M ^ ", p = " ^ PolyML.makestring p ^ 
-": " ^ PolyML.makestring g ^ " %|% " ^ PolyML.makestring a  ^ 
-" /\\ " ^ PolyML.makestring g ^ " %|% " ^ PolyML.makestring b);
+(writeln ("HENSEL-univ -------------------> " ^ PolyML.makestring g);
                                               g:unipoly 
 )
                                                         else HENSEL_lifting_up a b d M p
@@ -493,8 +494,8 @@
 
 subsection {* evaluation, translation uni--multivariate, etc *}
 ML {*
-  (* evaluate a polynomial in a certain variable and remove this from the exp-list *)         
-  fun eval (p: poly) var value = 
+  (* evaluate a polynomial in a certain variable and remove this var from the exp-list *)         
+  fun eval (p: poly) var value = (* TODO use "map" instead*)
     let 
       fun eval [] _ _ new = order new 
         | eval ((c, es)::ps) var value new =
@@ -679,20 +680,22 @@
 
 subsection {* gcd_poly algorithm, code for [1] p.95 *}
 ML {*
-  (* naming of n, M, m, r, ...  follows Winkler p. 95 *)
+  (* naming of n, M, m, r, ...  follows Winkler p. 95 
+    n: amount of variables 
+    r: *)
   fun 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 = 0 
+      if n > 1
       then
+        let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); 
+        in try_new_r a b n M r [] [] end
+      else 
         let val (a', b') = (multi_to_uni a, multi_to_uni b)
         in
           (* a b are made primitive and this is compensated by multiplying with gcd of divisors *)
           uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %* 
                         (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))
         end
-      else 
-        let val M = 1 + Int.min (max_deg_var a (length es1 - 2), max_deg_var b (length es2 - 2)); 
-        in try_new_r a b n M r [] [] end
 
   (* fn: poly -> poly -> int -> 
                       int -> int -> int list -> poly list -> poly*)
@@ -712,10 +715,14 @@
                            int -> int -> int -> int list -> poly list -> 
                            |                  poly -> poly -> int list -> poly*)
   and HENSEL_lifting a b n M m r r_list steps g g_n mult =
+((*begin function body*)
+writeln ("HENSEL-poly n = " ^ PolyML.makestring n ^ 
+", M = " ^ PolyML.makestring M ^ ", m = " ^ PolyML.makestring m ^ 
+", r = " ^ PolyML.makestring r ^ ", r_list = " ^ PolyML.makestring r_list^ 
+", steps = " ^ PolyML.makestring steps ^ ", g = " ^ PolyML.makestring g ^ 
+", g_n = " ^ PolyML.makestring g_n ^ ", mult = " ^ PolyML.makestring mult);
     if m > M then if g_n %%|%% a andalso g_n %%|%% b then
-(writeln ("HENSEL-poly M = " ^ PolyML.makestring M ^ "HENSEL-poly M = " ^ PolyML.makestring M ^ 
-": " ^ PolyML.makestring g_n ^ " %%|%% " ^ PolyML.makestring a ^ 
-" /\\ " ^ PolyML.makestring g_n ^ " %%|%% " ^ PolyML.makestring b);
+(writeln ("HENSEL-poly ------------------------------> " ^ PolyML.makestring g_n);
                                                           g_n
 ) 
                                                               else
@@ -750,7 +757,8 @@
 (writeln ("recurs.call 4 HENSEL-poly"); 
                HENSEL_lifting a b n M (m + 1) r r_list steps g  g_n mult
 )
-      end     
+      end
+)(*end function body*)     
 
   (* gcd_poly :: poly \<Rightarrow> poly \<Rightarrow> poly
      gcd_poly a b = ((a', b'), c)
diff -r 4d4254cc6e34 -r 1676be88dbcb test/Tools/isac/Test_Some2.thy
--- a/test/Tools/isac/Test_Some2.thy	Fri May 24 10:41:57 2013 +0200
+++ b/test/Tools/isac/Test_Some2.thy	Fri May 24 12:40:15 2013 +0200
@@ -10,31 +10,23 @@
 ML {*
 *}
 ML {*
-if gcd_poly 
+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])]
-= (([(~3, [0, 0]), (1, [3, 0]), (1, [1, 2])], [(2, [0, 0]), (~1, [1, 1]), (1, [0, 2])]),
-    [(1, [2, 0]), (~1, [0, 1]), (2, [1, 1])]) then () else error "gcd_poly ex1 changed";
+  [(2,[2,0]),(~2,[0,1]),(4,[1,1]),(~1,[3,1]),(1,[1,2]),(~1,[2,2]),(~1,[0,3]),(2,[1,3])];
 *}
 ML {*
-if gcd_poly 
+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])]
-  = (([(~1, [0,0,0]), (1, [0,1,1])], [(1, [0,0,0])]), [(1, [0,0,0]), (1, [1,1,0])]) 
-then () else error "gcd_poly ex2 changed";
+  [(1,[0,0,0]),(1,[1,1,0])];
 *}
 ML {*
-val a = uni_to_multi [~18, ~15, ~20, 12, 20, ~13, 2];
-val b = uni_to_multi [8, 28, 22, ~11, ~14, 1, 2];
-val ((a', b'), c) = gcd_poly a b;
+gcd_poly (uni_to_multi [~18, ~15, ~20, 12, 20, ~13, 2]) (uni_to_multi [8, 28, 22, ~11, ~14, 1, 2]);
 *}
 ML {*
-val a = [(1,[2, 0]), (~1,[0, 2])]; (* x^2 - y^2 *)
-val b = [(1,[2, 0]), (~1,[1, 1])]; (* x^2 - x y *)
-val ((a', b'), c) = gcd_poly a b;
+          (* x^2 - y^2 *)           (* x^2 - x y *)
+gcd_poly [(1,[2, 0]), (~1,[0, 2])] [(1,[2, 0]), (~1,[1, 1])];
 *}
 ML {*
-try_new_r
 *}
 ML {*
 *}