1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Sun Sep 01 16:50:51 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 02 14:56:57 2013 +0200
     1.3 @@ -658,10 +658,13 @@
     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 +
     1.9    (* naming of n, M, m, r, ...  follows Winkler p. 95 
    1.10 -    n: amount of variables 
    1.11 +    assumes: n = length es1 = length es2
    1.12      r: *)
    1.13 -  fun gcd_poly' [(c1, es1)] [(c2, es2)] _ _ = [(Integer.gcd c1 c2, map2 Integer.min es1 es2)]
    1.14 +  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom]
    1.15 +    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom]
    1.16      | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
    1.17        if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
    1.18          if n > 1
    1.19 @@ -677,7 +680,10 @@
    1.20            end
    1.21  
    1.22    (* fn: poly -> poly -> int -> 
    1.23 -                      int -> int -> int list -> poly list -> poly*)
    1.24 +                      int -> int -> int list -> poly list -> poly
    1.25 +     assumes length a > 1  \<and>  length b > 1
    1.26 +     yields TODO  
    1.27 +  *)
    1.28    and try_new_r a b n M r r_list steps = 
    1.29       let 
    1.30          val r = find_new_r a b r;
    1.31 @@ -688,7 +694,10 @@
    1.32        in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end
    1.33    (* fn: poly -> poly -> int -> 
    1.34                             int -> int -> int -> int list -> poly list -> 
    1.35 -                           |                  poly -> poly -> int list -> poly*)
    1.36 +                           |                  poly -> poly -> int list -> poly
    1.37 +     assumes length a > 1  \<and>  length b > 1
    1.38 +     yields TODO  
    1.39 +  *)
    1.40    and HENSEL_lifting a b n M m r r_list steps g g_n mult =
    1.41      if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else
    1.42        try_new_r a b n M r r_list steps