1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly.thy Fri May 24 12:40:15 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly.thy Fri May 24 14:25:34 2013 +0200
1.3 @@ -383,9 +383,6 @@
1.4 argumentns "a b d M p" named according to [1] p.93 *)
1.5 fun HENSEL_lifting_up a b d M p =
1.6 let
1.7 -val _ = writeln ("HENSEL-univ d = " ^ PolyML.makestring d ^
1.8 -", M = " ^ PolyML.makestring (2 * d * LANDAU_MIGNOTTE_bound a b) ^
1.9 -", p = " ^ PolyML.makestring p)
1.10 val p = p next_prime_not_dvd d
1.11 val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p (*see above*)
1.12 in
1.13 @@ -393,11 +390,7 @@
1.14 let
1.15 val g = primitive_up (try_new_prime_up a b d M p g_p p)
1.16 in
1.17 - if (g %|% a) andalso (g %|% b) then
1.18 -(writeln ("HENSEL-univ -------------------> " ^ PolyML.makestring g);
1.19 - g:unipoly
1.20 -)
1.21 - else HENSEL_lifting_up a b d M p
1.22 + if (g %|% a) andalso (g %|% b) then g:unipoly else HENSEL_lifting_up a b d M p
1.23 end
1.24 end
1.25
1.26 @@ -410,9 +403,7 @@
1.27 let val d = abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))
1.28 in
1.29 if a = b then a else
1.30 -(writeln ("gcd_up calls HENSEL-univ");
1.31 HENSEL_lifting_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1
1.32 -)
1.33 end;
1.34 *}
1.35
1.36 @@ -706,26 +697,12 @@
1.37 val g_r = gcd_poly' (order (eval a (n - 2) r))
1.38 (order (eval b (n - 2) r)) (n - 1) 0
1.39 val steps = steps @ [g_r];
1.40 - in
1.41 -(writeln ("try_new_r calls HENSEL-poly");
1.42 - HENSEL_lifting a b n M 1 r r_list steps g_r ( cero_poly n ) [1]
1.43 -)
1.44 - end
1.45 + in HENSEL_lifting a b n M 1 r r_list steps g_r ( cero_poly n ) [1] end
1.46 (* fn: poly -> poly -> int ->
1.47 int -> int -> int -> int list -> poly list ->
1.48 | poly -> poly -> int list -> poly*)
1.49 and HENSEL_lifting a b n M m r r_list steps g g_n mult =
1.50 -((*begin function body*)
1.51 -writeln ("HENSEL-poly n = " ^ PolyML.makestring n ^
1.52 -", M = " ^ PolyML.makestring M ^ ", m = " ^ PolyML.makestring m ^
1.53 -", r = " ^ PolyML.makestring r ^ ", r_list = " ^ PolyML.makestring r_list^
1.54 -", steps = " ^ PolyML.makestring steps ^ ", g = " ^ PolyML.makestring g ^
1.55 -", g_n = " ^ PolyML.makestring g_n ^ ", mult = " ^ PolyML.makestring mult);
1.56 - if m > M then if g_n %%|%% a andalso g_n %%|%% b then
1.57 -(writeln ("HENSEL-poly ------------------------------> " ^ PolyML.makestring g_n);
1.58 - g_n
1.59 -)
1.60 - else
1.61 + if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else
1.62 try_new_r a b n M r r_list steps
1.63 else
1.64 let
1.65 @@ -735,30 +712,18 @@
1.66 (order (eval b (n - 2) r)) (n - 1) 0
1.67 in
1.68 if lex_ord (lmonom g) (lmonom g_r)
1.69 - then
1.70 -(writeln ("recurs.call 1 HENSEL-poly");
1.71 - HENSEL_lifting a b n M 1 r r_list steps g g_n mult
1.72 -)
1.73 + then HENSEL_lifting a b n M 1 r r_list steps g g_n mult
1.74 else if (lexp g) = (lexp g_r)
1.75 then
1.76 let val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2)
1.77 in
1.78 if (nth steps (length steps - 1)) = (cero_poly (n - 1))
1.79 - then
1.80 -(writeln ("recurs.call 2 HENSEL-poly");
1.81 - HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new
1.82 -)
1.83 - else
1.84 -(writeln ("recurs.call 3 HENSEL-poly");
1.85 - HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
1.86 -)
1.87 + then HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new
1.88 + else HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
1.89 end
1.90 else (* \<not> lex_ord (lmonom g) (lmonom g_r) *)
1.91 -(writeln ("recurs.call 4 HENSEL-poly");
1.92 - HENSEL_lifting a b n M (m + 1) r r_list steps g g_n mult
1.93 -)
1.94 + HENSEL_lifting a b n M (m + 1) r r_list steps g g_n mult
1.95 end
1.96 -)(*end function body*)
1.97
1.98 (* gcd_poly :: poly \<Rightarrow> poly \<Rightarrow> poly
1.99 gcd_poly a b = ((a', b'), c)