p1 is primitive  \<and>  p2 is primitive

                p1 is primitive  \<and>  p2 is primitive

        yields  gcd | p1  \<and>  gcd | p2  \<and>  gcd is primitive

        yields  gcd | p1  \<and>  gcd | p2  \<and>  gcd is primitive

     argumentns "a b d M p" named according to [1] p.93 *)

     argumentns "a b d M p" named according to [1] p.93 *)

   fun HENSEL_lifting_up a b d M p = 

   fun HENSEL_lifting_up a b d M p = 

       val p = p next_prime_not_dvd d 

       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*)

       val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p (*see above*)

     in

     in

       if deg_up g_p = 0 then [1] else

       if deg_up g_p = 0 then [1] else

         let 

         let 

           val g = primitive_up (try_new_prime_up a b d M p g_p p)

           val g = primitive_up (try_new_prime_up a b d M p g_p p)

         in

         in

           if (g %|% a) andalso (g %|% b) then 

           if (g %|% a) andalso (g %|% b) then 

                                               g:unipoly 

                                               g:unipoly 

 )

 )

                                                         else HENSEL_lifting_up a b d M p

                                                         else HENSEL_lifting_up a b d M p

         end

         end

     end

     end

   fun max_deg_var (p: poly) var = (maxs o (map ((nth_swapped var) o snd))) p;

   fun max_deg_var (p: poly) var = (maxs o (map ((nth_swapped var) o snd))) p;

 *}

 *}

 subsection {* evaluation, translation uni--multivariate, etc *}

 subsection {* evaluation, translation uni--multivariate, etc *}

 ML {*

 ML {*

     let 

     let 

       fun eval [] _ _ new = order new 

       fun eval [] _ _ new = order new 

         | eval ((c, es)::ps) var value new =

         | eval ((c, es)::ps) var value new =

           eval ps var value (new @ [((Integer.pow  (nth es var) value) * c, nth_drop var es)]);

           eval ps var value (new @ [((Integer.pow  (nth es var) value) * c, nth_drop var es)]);

     in eval p var value [] end

     in eval p var value [] end

       in (order p', new_vals, steps) end 

       in (order p', new_vals, steps) end 

 *}

 *}

 subsection {* gcd_poly algorithm, code for [1] p.95 *}

 subsection {* gcd_poly algorithm, code for [1] p.95 *}

 ML {*

 ML {*

   fun gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n 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 lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else

       then

       then

         let val (a', b') = (multi_to_uni a, multi_to_uni b)

         let val (a', b') = (multi_to_uni a, multi_to_uni b)

         in

         in

           (* a b are made primitive and this is compensated by multiplying with gcd of divisors *)

           (* 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')) %* 

           uni_to_multi ((gcd_up (primitive_up a') (primitive_up b')) %* 

                         (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))

                         (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))

         end

         end

   (* fn: poly -> poly -> int -> 

   (* fn: poly -> poly -> int -> 

                       int -> int -> int list -> poly list -> poly*)

                       int -> int -> int list -> poly list -> poly*)

   and try_new_r a b n M r r_list steps = 

   and try_new_r a b n M r r_list steps = 

      let 

      let 

                                                                          end

                                                                          end

   (* fn: poly -> poly -> int -> 

   (* fn: poly -> poly -> int -> 

                            int -> int -> int -> int list -> poly list -> 

                            int -> int -> int -> int list -> poly list -> 

                            |                  poly -> poly -> int list -> poly*)

                            |                  poly -> poly -> int list -> poly*)

   and HENSEL_lifting a b n M m r r_list steps g g_n mult =

   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

     if m > M then if g_n %%|%% a andalso g_n %%|%% b then

                                                           g_n

                                                           g_n

 ) 

 ) 

                                                               else

                                                               else

       try_new_r a b n M r r_list steps 

       try_new_r a b n M r r_list steps 

     else

     else

             end

             end

           else (* \<not> lex_ord (lmonom g) (lmonom g_r) *)

           else (* \<not> lex_ord (lmonom g) (lmonom g_r) *)

 (writeln ("recurs.call 4 HENSEL-poly"); 

 (writeln ("recurs.call 4 HENSEL-poly"); 

                HENSEL_lifting a b n M (m + 1) r r_list steps g  g_n mult

                HENSEL_lifting a b n M (m + 1) r r_list steps g  g_n mult

 )

 )

   (* gcd_poly :: poly \<Rightarrow> poly \<Rightarrow> poly

   (* gcd_poly :: poly \<Rightarrow> poly \<Rightarrow> poly

      gcd_poly a b = ((a', b'), c)

      gcd_poly a b = ((a', b'), c)

      assumes a \<noteq> [] \<and> b \<noteq> [] \<and> 

      assumes a \<noteq> [] \<and> b \<noteq> [] \<and> 

      yields a = a' *\<^isub>p c  \<and>  b = b' *\<^isub>p c \<and> 

      yields a = a' *\<^isub>p c  \<and>  b = b' *\<^isub>p c \<and>