1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 15:17:34 2013 +0200
1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy Mon Sep 02 16:16:08 2013 +0200
1.3 @@ -374,15 +374,15 @@
1.4 in try_new_prime_up a b d M P g p end
1.5 end
1.6
1.7 - (* HENSEL_lifting_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
1.8 - HENSEL_lifting_up p1 p2 d M p = gcd
1.9 + (* iterate_CHINESE_up :: unipoly \<Rightarrow> unipoly \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> unipoly
1.10 + iterate_CHINESE_up p1 p2 d M p = gcd
1.11 assumes d = gcd (lcoeff_up p1, lcoeff_up p2) \<and>
1.12 M = LANDAU_MIGNOTTE_bound \<and> p = prime \<and> p ~| d \<and>
1.13 p1 is primitive \<and> p2 is primitive
1.14 yields gcd | p1 \<and> gcd | p2 \<and> gcd is primitive
1.15
1.16 argumentns "a b d M p" named according to [1] p.93 *)
1.17 - fun HENSEL_lifting_up a b d M p =
1.18 + fun iterate_CHINESE_up a b d M p =
1.19 let
1.20 val p = p next_prime_not_dvd d
1.21 val g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (d mod p)) mod_up p) p
1.22 @@ -392,7 +392,7 @@
1.23 let
1.24 val g = primitive_up (try_new_prime_up a b d M p g_p p)
1.25 in
1.26 - if (g %|% a) andalso (g %|% b) then g:unipoly else HENSEL_lifting_up a b d M p
1.27 + if (g %|% a) andalso (g %|% b) then g:unipoly else iterate_CHINESE_up a b d M p
1.28 end
1.29 end
1.30
1.31 @@ -405,7 +405,7 @@
1.32 let val d = abs (Integer.gcd (lcoeff_up a) (lcoeff_up b))
1.33 in
1.34 if a = b then a else
1.35 - HENSEL_lifting_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1
1.36 + iterate_CHINESE_up a b d (2 * d * LANDAU_MIGNOTTE_bound a b) 1
1.37 end;
1.38 *}
1.39
1.40 @@ -679,10 +679,10 @@
1.41 (abs (Integer.gcd (gcd_coeff a') (gcd_coeff b'))))
1.42 end
1.43
1.44 - (* fn: poly -> poly -> int ->
1.45 - int -> int -> int list -> poly list -> poly
1.46 + (* try_new_r :: poly -> poly -> int -> int -> int -> int list -> poly list -> poly
1.47 + try_new_r a b n M r r_list steps =
1.48 assumes length a > 1 \<and> length b > 1
1.49 - yields TODO
1.50 + yields TODO
1.51 *)
1.52 and try_new_r a b n M r r_list steps =
1.53 let
1.54 @@ -691,16 +691,18 @@
1.55 val g_r = gcd_poly' (order (eval a (n - 2) r))
1.56 (order (eval b (n - 2) r)) (n - 1) 0
1.57 val steps = steps @ [g_r];
1.58 - in HENSEL_lifting a b n M 1 r r_list steps g_r ( zero_poly n ) [1] end
1.59 - (* fn: poly -> poly -> int ->
1.60 - int -> int -> int -> int list -> poly list ->
1.61 - | poly -> poly -> int list -> poly
1.62 + in iterate_CHINESE a b n M 1 r r_list steps g_r (zero_poly n) [1] end
1.63 +
1.64 + (* iterate_CHINESE :: poly -> poly -> int -> int -> int -> int -> int list ->
1.65 + | poly list -> poly -> poly -> int list -> poly
1.66 + iterate_CHINESE a | b n M m r r_list
1.67 + steps g g_n mult =
1.68 assumes length a > 1 \<and> length b > 1
1.69 - yields TODO
1.70 + yields TODO
1.71 *)
1.72 - and HENSEL_lifting a b n M m r r_list steps g g_n mult =
1.73 + and iterate_CHINESE a b n M m r r_list steps g g_n mult =
1.74 if m > M then if g_n %%|%% a andalso g_n %%|%% b then g_n else
1.75 - try_new_r a b n M r r_list steps
1.76 + try_new_r a b n M r r_list steps
1.77 else
1.78 let
1.79 val r = find_new_r a b r;
1.80 @@ -709,20 +711,20 @@
1.81 (order (eval b (n - 2) r)) (n - 1) 0
1.82 in
1.83 if lex_ord (lmonom g) (lmonom g_r)
1.84 - then HENSEL_lifting a b n M 1 r r_list steps g g_n mult
1.85 - else if (lexp g) = (lexp g_r)
1.86 + then iterate_CHINESE a b n M 1 r r_list steps g g_n mult
1.87 + else if lexp g = lexp g_r
1.88 then
1.89 let val (g_n, new, steps) = NEWTON r_list [g, g_r] steps mult g_n (n - 2)
1.90 in
1.91 - if (nth steps (length steps - 1)) = (zero_poly (n - 1))
1.92 - then HENSEL_lifting a b n M (M + 1) r r_list steps g_r g_n new
1.93 - else HENSEL_lifting a b n M (m + 1) r r_list steps g_r g_n new
1.94 + if nth steps (length steps - 1) = zero_poly (n - 1)
1.95 + then iterate_CHINESE a b n M (M + 1) r r_list steps g_r g_n new
1.96 + else iterate_CHINESE a b n M (m + 1) r r_list steps g_r g_n new
1.97 end
1.98 else (* \<not> lex_ord (lmonom g) (lmonom g_r) *)
1.99 - HENSEL_lifting a b n M (m + 1) r r_list steps g g_n mult
1.100 + iterate_CHINESE a b n M (m + 1) r r_list steps g g_n mult
1.101 end
1.102
1.103 - fun majority_of_coefficients_is_negative a b c =
1.104 + fun majority_of_coefficients_is_negative_in a b c =
1.105 let val cs = (coeffs a) @ (coeffs b) @ (coeffs c)
1.106 in length (filter (curry op < 0) cs) < length cs div 2 end
1.107
1.108 @@ -736,7 +738,7 @@
1.109 val (a': poly, _) = a %%/%% c
1.110 val (b': poly, _) = b %%/%% c
1.111 in
1.112 - if majority_of_coefficients_is_negative a' b' c
1.113 + if majority_of_coefficients_is_negative_in a' b' c
1.114 then ((a' %%* ~1, b' %%* ~1), c %%* ~1) (*makes results look nicer*)
1.115 else ((a', b'), c)
1.116 end