1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy	Fri Feb 15 15:04:08 2013 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy	Fri Feb 15 15:46:29 2013 +0100
     1.3 @@ -312,15 +312,17 @@
     1.4          end
     1.5      end
     1.6    
     1.7 -  (* TODO *)
     1.8 -  fun GCD_MOD (a: unipoly) (b: unipoly) =
     1.9 -   (* if a = [0] orelse b = [0] then [0] else  --> / [(0,[0])] *)
    1.10 -       if a = b then a else
    1.11 -       Hensel_lifting' a b  (abs (Integer.gcd (lc a) (lc b)))  
    1.12 -             (2 * (abs (Integer.gcd (lc a) (lc b))) * landau_mignotte_bound a b) 1;
    1.13 -
    1.14 -
    1.15 -
    1.16 +  (* gcd_poly :: unipoly -> unipoly -> unipoly
    1.17 +     gcd_poly a b = c
    1.18 +     assumes 
    1.19 +       not (a = []) \<and> not (b = [])
    1.20 +     yields c dvd a \<and> c dvd b \<and>
    1.21 +       \<And> cc. (cc dvd a \<and> cc dvd b) => cc \<le> c
    1.22 + *)
    1.23 +  fun gcd_unipoly (a: unipoly) (b: unipoly) =
    1.24 +    if a = b then a else
    1.25 +      HENSEL_lifting_up a b (abs (Integer.gcd (lc a) (lc b)))  
    1.26 +        (2 * (abs (Integer.gcd (lc a) (lc b))) * landau_mignotte_bound a b) 1;
    1.27  *}
    1.28  (* ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.29  subsection {* gcd_poly Algorgithmus, auxiliary functions multivariate *}
    1.30 @@ -334,7 +336,7 @@
    1.31  subsection {* calculations for multivariate polynomials *}
    1.32  
    1.33  ML {*
    1.34 -(* a and b have the same length *)
    1.35 +(* assumes a and b have the same length*)
    1.36    fun listgreater a b = 
    1.37      let fun gr a b = a>=b;
    1.38      fun all [] = true 
    1.39 @@ -369,7 +371,7 @@
    1.40            in add (List.tl mvp) (order) (new @ [((get_coef mvp 0),(first @ [0] @ last))]) end 
    1.41      in add mvp order [] end
    1.42  
    1.43 -  fun cero_multipoly (different_var: int) = [(0,replicate diferent_var 0)];
    1.44 +  fun cero_multipoly (different_var: int) = [(0, replicate different_var 0)];
    1.45  *}
    1.46  ML{*
    1.47    (* if a is greater than b --> true or false*)
    1.48 @@ -389,16 +391,17 @@
    1.49  
    1.50    (* add same variables *)
    1.51    fun short_multipoly (mvp: multipoly) = 
    1.52 -    let fun short  (new: multipoly) (mvp: multipoly)=
    1.53 -             if (List.length mvp) = 1 then 
    1.54 -               if new = [] then drop_lc0_multipoly mvp else drop_lc0_multipoly (new @ mvp) 
    1.55 -             else
    1.56 -               if get_varlist mvp 0 = get_varlist mvp 1 
    1.57 -               then short new ([((get_coef mvp 0) + (get_coef mvp 1), (get_varlist mvp 0))] @
    1.58 -                             (List.tl (List.tl mvp)))  
    1.59 -               else if (get_coef mvp 0) = 0 then short new (List.tl mvp)
    1.60 -                    else  short (new @ [((get_coef mvp 0), (get_varlist mvp 0))]) (List.tl mvp)
    1.61 -    in short [] mvp end;
    1.62 +    let fun short (mvp: multipoly) (new: multipoly) =
    1.63 +              if length mvp =1 
    1.64 +              then if (get_coef mvp 0) = 0 
    1.65 +                   then if new = [] then cero_multipoly (length (get_varlist mvp 0)) else new
    1.66 +                   else  new @ mvp 
    1.67 +              else if get_varlist  mvp 0 = get_varlist mvp 1
    1.68 +                then short ( [(get_coef mvp 0 + get_coef mvp 1,get_varlist  mvp 0)]
    1.69 +                             @ nth_drop 0 (nth_drop 0 mvp))   new 
    1.70 +                else if (get_coef mvp 0) = 0 then short (nth_drop 0 mvp) new 
    1.71 +                  else short (nth_drop 0 mvp) (new @ [nth mvp 0])
    1.72 +    in short mvp [] end
    1.73  
    1.74    (* brings the polynom in correct order and add same variables*)
    1.75    fun order_multipoly (a: multipoly)=

     2.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri Feb 15 15:04:08 2013 +0100
     2.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy	Fri Feb 15 15:46:29 2013 +0100
     2.3 @@ -453,12 +453,22 @@
     2.4  value "mod_poly_gcd [8, 28, 22, -11, -14, 1, 2] [2, 6, 0, 2, 6] 7 = [2, 6, 0, 2, 6]" 
     2.5  value "mod_poly_gcd [20, 15, 8, 6] [8, -2, -2, 3] 2 = [0, 1]"
     2.6  
     2.7 -(*----------------------------------------------------------------------------*)
     2.8 +(* primitive polynom = no prime divide the polynom:
     2.9 +   pp :: unipoly -> unipoly
    2.10 +   pp [p_1, p_2, p_3,..., p_k] = g
    2.11 +   assumes 
    2.12 +   yields \<exists> t. 0 < i < k \<Rightarrow> t = gcd (p_i, p_{i+1}) \<and> [p_1, p_2, .., p_k] = t * g *)
    2.13 +fun pp :: "unipoly  \<Rightarrow> unipoly" where
    2.14 +  "pp [c] = (if c = 0 then [0] else [1])"
    2.15 +| "pp "
    2.16 +
    2.17 +(*
    2.18  value "xxx" -- "= "
    2.19  
    2.20  print_configs
    2.21  declare [[simp_trace_depth_limit=99]]
    2.22  declare [[simp_trace=true]]
    2.23 +*)
    2.24  (*---------------------------------------------------------------------------------------------*)
    2.25  
    2.26  (*