(* Authors: Jose Divasón Sebastiaan Joosten René Thiemann Akihisa Yamada *) section ‹Hensel Lifting› subsection ‹Properties about Factors› text ‹We define and prove properties of Hensel-lifting. Here, we show the result that Hensel-lifting can lift a factorization mod $p$ to a factorization mod $p^n$. For the lifting we have proofs for both versions, the original linear Hensel-lifting or the quadratic approach from Zassenhaus. Via the linear version, we also show a uniqueness result, however only in the binary case, i.e., where $f = g \cdot h$. Uniqueness of the general case will later be shown in theory Berlekamp-Hensel by incorporating the factorization algorithm for finite fields algorithm.› theory Hensel_Lifting imports "HOL-Computational_Algebra.Euclidean_Algorithm" Poly_Mod_Finite_Field_Record_Based Polynomial_Factorization.Square_Free_Factorization begin lemma uniqueness_poly_equality: fixes f g :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes cop: "coprime f g" and deg: "B = 0 ∨ degree B < degree f" "B' = 0 ∨ degree B' < degree f" and f: "f ≠ 0" and eq: "A * f + B * g = A' * f + B' * g" shows "A = A'" "B = B'" proof - from eq have *: "(A - A') * f = (B' - B) * g" by (simp add: field_simps) hence "f dvd (B' - B) * g" unfolding dvd_def by (intro exI[of _ "A - A'"], auto simp: field_simps) with cop[simplified] have dvd: "f dvd (B' - B)" by (simp add: coprime_dvd_mult_right_iff ac_simps) from divides_degree[OF this] have "degree f ≤ degree (B' - B) ∨ B = B'" by auto with degree_diff_le_max[of B' B] deg show "B = B'" by auto with * f show "A = A'" by auto qed lemmas (in poly_mod_prime_type) uniqueness_poly_equality = uniqueness_poly_equality[where 'a="'a mod_ring", untransferred] lemmas (in poly_mod_prime) uniqueness_poly_equality = poly_mod_prime_type.uniqueness_poly_equality [unfolded poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty] lemma pseudo_divmod_main_list_1_is_divmod_poly_one_main_list: "pseudo_divmod_main_list (1 :: 'a :: comm_ring_1) q f g n = divmod_poly_one_main_list q f g n" by (induct n arbitrary: q f g, auto simp: Let_def) lemma pdivmod_monic_pseudo_divmod: assumes g: "monic g" shows "pdivmod_monic f g = pseudo_divmod f g" proof - from g have id: "(coeffs g = []) = False" by auto from g have mon: "hd (rev (coeffs g)) = 1" by (metis coeffs_eq_Nil hd_rev id last_coeffs_eq_coeff_degree) show ?thesis unfolding pseudo_divmod_impl pseudo_divmod_list_def id if_False pdivmod_monic_def Let_def mon pseudo_divmod_main_list_1_is_divmod_poly_one_main_list by (auto split: prod.splits) qed lemma pdivmod_monic: assumes g: "monic g" and res: "pdivmod_monic f g = (q, r)" shows "f = g * q + r" "r = 0 ∨ degree r < degree g" proof - from g have g0: "g ≠ 0" by auto from pseudo_divmod[OF g0 res[unfolded pdivmod_monic_pseudo_divmod[OF g]], unfolded g] show "f = g * q + r" "r = 0 ∨ degree r < degree g" by auto qed definition dupe_monic :: "'a :: comm_ring_1 poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly ⇒ 'a poly * 'a poly" where "dupe_monic D H S T U = (case pdivmod_monic (T * U) D of (q,r) ⇒ (S * U + H * q, r))" lemma dupe_monic: assumes 1: "D*S + H*T = 1" and mon: "monic D" and dupe: "dupe_monic D H S T U = (A,B)" shows "A * D + B * H = U" "B = 0 ∨ degree B < degree D" proof - obtain Q R where div: "pdivmod_monic ((T * U)) D = (Q,R)" by force from dupe[unfolded dupe_monic_def div split] have A: "A = (S * U + H * Q)" and B: "B = R" by auto from pdivmod_monic[OF mon div] have TU: "T * U = D * Q + R" and deg: "R = 0 ∨ degree R < degree D" by auto hence R: "R = T * U - D * Q" by simp have "A * D + B * H = (D * S + H * T) * U" unfolding A B R by (simp add: field_simps) also have "… = U" unfolding 1 by simp finally show eq: "A * D + B * H = U" . show "B = 0 ∨ degree B < degree D" using deg unfolding B . qed lemma dupe_monic_unique: fixes D :: "'a :: {factorial_ring_gcd,semiring_gcd_mult_normalize} poly" assumes 1: "D*S + H*T = 1" and mon: "monic D" and dupe: "dupe_monic D H S T U = (A,B)" and cop: "coprime D H" and other: "A' * D + B' * H = U" "B' = 0 ∨ degree B' < degree D" shows "A' = A" "B' = B" proof - from dupe_monic[OF 1 mon dupe] have one: "A * D + B * H = U" "B = 0 ∨ degree B < degree D" by auto from mon have D0: "D ≠ 0" by auto from uniqueness_poly_equality[OF cop one(2) other(2) D0, of A A', unfolded other, OF one(1)] show "A' = A" "B' = B" by auto qed context ring_ops begin lemma poly_rel_dupe_monic_i: assumes mon: "monic D" and rel: "poly_rel d D" "poly_rel h H" "poly_rel s S" "poly_rel t T" "poly_rel u U" shows "rel_prod poly_rel poly_rel (dupe_monic_i ops d h s t u) (dupe_monic D H S T U)" proof - note defs = dupe_monic_i_def dupe_monic_def note [transfer_rule] = rel have [transfer_rule]: "rel_prod poly_rel poly_rel (pdivmod_monic_i ops (times_poly_i ops t u) d) (pdivmod_monic (T * U) D)" by (rule poly_rel_pdivmod_monic[OF mon], transfer_prover+) show ?thesis unfolding defs by transfer_prover qed end context mod_ring_gen begin lemma monic_of_int_poly: "monic D ⟹ monic (of_int_poly (Mp D) :: 'a mod_ring poly)" using Mp_f_representative Mp_to_int_poly monic_Mp by auto lemma dupe_monic_i: assumes dupe_i: "dupe_monic_i ff_ops d h s t u = (a,b)" and 1: "D*S + H*T =m 1" and mon: "monic D" and A: "A = to_int_poly_i ff_ops a" and B: "B = to_int_poly_i ff_ops b" and d: "Mp_rel_i d D" and h: "Mp_rel_i h H" and s: "Mp_rel_i s S" and t: "Mp_rel_i t T" and u: "Mp_rel_i u U" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp_rel_i a A" "Mp_rel_i b B" proof - let ?I = "λ f. of_int_poly (Mp f) :: 'a mod_ring poly" let ?i = "to_int_poly_i ff_ops" note dd = Mp_rel_iD[OF d] note hh = Mp_rel_iD[OF h] note ss = Mp_rel_iD[OF s] note tt = Mp_rel_iD[OF t] note uu = Mp_rel_iD[OF u] obtain A' B' where dupe: "dupe_monic (?I D) (?I H) (?I S) (?I T) (?I U) = (A',B')" by force from poly_rel_dupe_monic_i[OF monic_of_int_poly[OF mon] dd(1) hh(1) ss(1) tt(1) uu(1), unfolded dupe_i dupe] have a: "poly_rel a A'" and b: "poly_rel b B'" by auto show aa: "Mp_rel_i a A" by (rule Mp_rel_iI'[OF a, folded A]) show bb: "Mp_rel_i b B" by (rule Mp_rel_iI'[OF b, folded B]) note Aa = Mp_rel_iD[OF aa] note Bb = Mp_rel_iD[OF bb] from poly_rel_inj[OF a Aa(1)] A have A: "A' = ?I A" by simp from poly_rel_inj[OF b Bb(1)] B have B: "B' = ?I B" by simp note Mp = dd(2) hh(2) ss(2) tt(2) uu(2) note [transfer_rule] = Mp have "(=) (D * S + H * T =m 1) (?I D * ?I S + ?I H * ?I T = 1)" by transfer_prover with 1 have 11: "?I D * ?I S + ?I H * ?I T = 1" by simp from dupe_monic[OF 11 monic_of_int_poly[OF mon] dupe, unfolded A B] have res: "?I A * ?I D + ?I B * ?I H = ?I U" "?I B = 0 ∨ degree (?I B) < degree (?I D)" by auto note [transfer_rule] = Aa(2) Bb(2) have "(=) (A * D + B * H =m U) (?I A * ?I D + ?I B * ?I H = ?I U)" "(=) (B =m 0 ∨ degree_m B < degree_m D) (?I B = 0 ∨ degree (?I B) < degree (?I D))" by transfer_prover+ with res have *: "A * D + B * H =m U" "B =m 0 ∨ degree_m B < degree_m D" by auto show "A * D + B * H =m U" by fact have B: "Mp B = B" using Mp_rel_i_Mp_to_int_poly_i assms(5) bb by blast from *(2) show "B = 0 ∨ degree B < degree D" unfolding B using degree_m_le[of D] by auto qed lemma Mp_rel_i_of_int_poly_i: assumes "Mp F = F" shows "Mp_rel_i (of_int_poly_i ff_ops F) F" by (metis Mp_f_representative Mp_rel_iI' assms poly_rel_of_int_poly to_int_poly_i) lemma dupe_monic_i_int: assumes dupe_i: "dupe_monic_i_int ff_ops D H S T U = (A,B)" and 1: "D*S + H*T =m 1" and mon: "monic D" and norm: "Mp D = D" "Mp H = H" "Mp S = S" "Mp T = T" "Mp U = U" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" proof - let ?oi = "of_int_poly_i ff_ops" let ?ti = "to_int_poly_i ff_ops" note rel = norm[THEN Mp_rel_i_of_int_poly_i] obtain a b where dupe: "dupe_monic_i ff_ops (?oi D) (?oi H) (?oi S) (?oi T) (?oi U) = (a,b)" by force from dupe_i[unfolded dupe_monic_i_int_def this Let_def] have AB: "A = ?ti a" "B = ?ti b" by auto from dupe_monic_i[OF dupe 1 mon AB rel] Mp_rel_i_Mp_to_int_poly_i show "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" unfolding AB by auto qed end definition dupe_monic_dynamic :: "int ⇒ int poly ⇒ int poly ⇒ int poly ⇒ int poly ⇒ int poly ⇒ int poly × int poly" where "dupe_monic_dynamic p = ( if p ≤ 65535 then dupe_monic_i_int (finite_field_ops32 (uint32_of_int p)) else if p ≤ 4294967295 then dupe_monic_i_int (finite_field_ops64 (uint64_of_int p)) else dupe_monic_i_int (finite_field_ops_integer (integer_of_int p)))" context poly_mod_2 begin lemma dupe_monic_i_int_finite_field_ops_integer: assumes dupe_i: "dupe_monic_i_int (finite_field_ops_integer (integer_of_int m)) D H S T U = (A,B)" and 1: "D*S + H*T =m 1" and mon: "monic D" and norm: "Mp D = D" "Mp H = H" "Mp S = S" "Mp T = T" "Mp U = U" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" using m1 mod_ring_gen.dupe_monic_i_int[OF mod_ring_locale.mod_ring_finite_field_ops_integer[unfolded mod_ring_locale_def], internalize_sort "'a :: nontriv", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF _ assms] by auto lemma dupe_monic_i_int_finite_field_ops32: assumes m: "m ≤ 65535" and dupe_i: "dupe_monic_i_int (finite_field_ops32 (uint32_of_int m)) D H S T U = (A,B)" and 1: "D*S + H*T =m 1" and mon: "monic D" and norm: "Mp D = D" "Mp H = H" "Mp S = S" "Mp T = T" "Mp U = U" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" using m1 mod_ring_gen.dupe_monic_i_int[OF mod_ring_locale.mod_ring_finite_field_ops32[unfolded mod_ring_locale_def], internalize_sort "'a :: nontriv", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF _ assms] by auto lemma dupe_monic_i_int_finite_field_ops64: assumes m: "m ≤ 4294967295" and dupe_i: "dupe_monic_i_int (finite_field_ops64 (uint64_of_int m)) D H S T U = (A,B)" and 1: "D*S + H*T =m 1" and mon: "monic D" and norm: "Mp D = D" "Mp H = H" "Mp S = S" "Mp T = T" "Mp U = U" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" using m1 mod_ring_gen.dupe_monic_i_int[OF mod_ring_locale.mod_ring_finite_field_ops64[unfolded mod_ring_locale_def], internalize_sort "'a :: nontriv", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF _ assms] by auto lemma dupe_monic_dynamic: assumes dupe: "dupe_monic_dynamic m D H S T U = (A,B)" and 1: "D*S + H*T =m 1" and mon: "monic D" and norm: "Mp D = D" "Mp H = H" "Mp S = S" "Mp T = T" "Mp U = U" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" using dupe dupe_monic_i_int_finite_field_ops32[OF _ _ 1 mon norm, of A B] dupe_monic_i_int_finite_field_ops64[OF _ _ 1 mon norm, of A B] dupe_monic_i_int_finite_field_ops_integer[OF _ 1 mon norm, of A B] unfolding dupe_monic_dynamic_def by (auto split: if_splits) end context poly_mod begin definition dupe_monic_int :: "int poly ⇒ int poly ⇒ int poly ⇒ int poly ⇒ int poly ⇒ int poly * int poly" where "dupe_monic_int D H S T U = (case pdivmod_monic (Mp (T * U)) D of (q,r) ⇒ (Mp (S * U + H * q), Mp r))" end declare poly_mod.dupe_monic_int_def[code] text ‹Old direct proof on int poly. It does not permit to change implementation. This proof is still present, since we did not export the uniqueness part from the type-based uniqueness result @{thm dupe_monic_unique} via the various relations.› lemma (in poly_mod_2) dupe_monic_int: assumes 1: "D*S + H*T =m 1" and mon: "monic D" and dupe: "dupe_monic_int D H S T U = (A,B)" shows "A * D + B * H =m U" "B = 0 ∨ degree B < degree D" "Mp A = A" "Mp B = B" "coprime_m D H ⟹ A' * D + B' * H =m U ⟹ B' = 0 ∨ degree B' < degree D ⟹ Mp D = D ⟹ Mp A' = A' ⟹ Mp B' = B' ⟹ prime m ⟹ A' = A ∧ B' = B" proof - obtain Q R where div: "pdivmod_monic (Mp (T * U)) D = (Q,R)" by force from dupe[unfolded dupe_monic_int_def div split] have A: "A = Mp (S * U + H * Q)" and B: "B = Mp R" by auto from pdivmod_monic[OF mon div] have TU: "Mp (T * U) = D * Q + R" and deg: "R = 0 ∨ degree R < degree D" by auto hence "Mp R = Mp (Mp (T * U) - D * Q)" by simp also have "… = Mp (T * U - Mp (Mp (Mp D * Q)))" unfolding Mp_Mp unfolding minus_Mp using minus_Mp mult_Mp by metis also have "… = Mp (T * U - D * Q)" by simp finally have r: "Mp R = Mp (T * U - D * Q)" by simp have "Mp (A * D + B * H) = Mp (Mp (A * D) + Mp (B * H))" by simp also have "Mp (A * D) = Mp ((S * U + H * Q) * D)" unfolding A by simp also have "Mp (B * H) = Mp (Mp R * Mp H)" unfolding B by simp also have "… = Mp ((T * U - D * Q) * H)" unfolding r by simp also have "Mp (Mp ((S * U + H * Q) * D) + Mp ((T * U - D * Q) * H)) = Mp ((S * U + H * Q) * D + (T * U - D * Q) * H)" by simp also have "(S * U + H * Q) * D + (T * U - D * Q) * H = (D * S + H * T) * U" by (simp add: field_simps) also have "Mp … = Mp (Mp (D * S + H * T) * U)" by simp also have "Mp (D * S + H * T) = 1" using 1 by simp finally show eq: "A * D + B * H =m U" by simp have id: "degree_m (Mp R) = degree_m R" by simp have id': "degree D = degree_m D" using mon by simp show degB: "B = 0 ∨ degree B < degree D" using deg unfolding B id id' using degree_m_le[of R] by (cases "R = 0", auto) show Mp: "Mp A = A" "Mp B = B" unfolding A B by auto assume another: "A' * D + B' * H =m U" and degB': "B' = 0 ∨ degree B' < degree D" and norm: "Mp A' = A'" "Mp B' = B'" and cop: "coprime_m D H" and D: "Mp D = D" and prime: "prime m" from degB Mp D have degB: "B =m 0 ∨ degree_m B < degree_m D" by auto from degB' Mp D norm have degB': "B' =m 0 ∨ degree_m B' < degree_m D" by auto from mon D have D0: "¬ (D =m 0)" by auto from prime interpret poly_mod_prime m by unfold_locales from another eq have "A' * D + B' * H =m A * D + B * H" by simp from uniqueness_poly_equality[OF cop degB' degB D0 this] show "A' = A ∧ B' = B" unfolding norm Mp by auto qed lemma coprime_bezout_coefficients: assumes cop: "coprime f g" and ext: "bezout_coefficients f g = (a, b)" shows "a * f + b * g = 1" using assms bezout_coefficients [of f g a b] by simp lemma (in poly_mod_prime_type) bezout_coefficients_mod_int: assumes f: "(F :: 'a mod_ring poly) = of_int_poly f" and g: "(G :: 'a mod_ring poly) = of_int_poly g" and cop: "coprime_m f g" and fact: "bezout_coefficients F G = (A,B)" and a: "a = to_int_poly A" and b: "b = to_int_poly B" shows "f * a + g * b =m 1" proof - have f[transfer_rule]: "MP_Rel f F" unfolding f MP_Rel_def by (simp add: Mp_f_representative) have g[transfer_rule]: "MP_Rel g G" unfolding g MP_Rel_def by (simp add: Mp_f_representative) have [transfer_rule]: "MP_Rel a A" unfolding a MP_Rel_def by (rule Mp_to_int_poly) have [transfer_rule]: "MP_Rel b B" unfolding b MP_Rel_def by (rule Mp_to_int_poly) from cop have "coprime F G" using coprime_MP_Rel[unfolded rel_fun_def] f g by auto from coprime_bezout_coefficients [OF this fact] have "A * F + B * G = 1" . from this [untransferred] show ?thesis by (simp add: ac_simps) qed definition bezout_coefficients_i :: "'i arith_ops_record ⇒ 'i list ⇒ 'i list ⇒ 'i list × 'i list" where "bezout_coefficients_i ff_ops f g = fst (euclid_ext_poly_i ff_ops f g)" definition euclid_ext_poly_mod_main :: "int ⇒ 'a arith_ops_record ⇒ int poly ⇒ int poly ⇒ int poly × int poly" where "euclid_ext_poly_mod_main p ff_ops f g = (case bezout_coefficients_i ff_ops (of_int_poly_i ff_ops f) (of_int_poly_i ff_ops g) of (a,b) ⇒ (to_int_poly_i ff_ops a, to_int_poly_i ff_ops b))" definition euclid_ext_poly_dynamic :: "int ⇒ int poly ⇒ int poly ⇒ int poly × int poly" where "euclid_ext_poly_dynamic p = ( if p ≤ 65535 then euclid_ext_poly_mod_main p (finite_field_ops32 (uint32_of_int p)) else if p ≤ 4294967295 then euclid_ext_poly_mod_main p (finite_field_ops64 (uint64_of_int p)) else euclid_ext_poly_mod_main p (finite_field_ops_integer (integer_of_int p)))" context prime_field_gen begin lemma bezout_coefficients_i[transfer_rule]: "(poly_rel ===> poly_rel ===> rel_prod poly_rel poly_rel) (bezout_coefficients_i ff_ops) bezout_coefficients" unfolding bezout_coefficients_i_def bezout_coefficients_def by transfer_prover lemma bezout_coefficients_i_sound: assumes f: "f' = of_int_poly_i ff_ops f" "Mp f = f" and g: "g' = of_int_poly_i ff_ops g" "Mp g = g" and cop: "coprime_m f g" and res: "bezout_coefficients_i ff_ops f' g' = (a',b')" and a: "a = to_int_poly_i ff_ops a'" and b: "b = to_int_poly_i ff_ops b'" shows "f * a + g * b =m 1" "Mp a = a" "Mp b = b" proof - from f have f': "f' = of_int_poly_i ff_ops (Mp f)" by simp define f'' where "f'' ≡ of_int_poly (Mp f) :: 'a mod_ring poly" have f'': "f'' = of_int_poly f" unfolding f''_def f by simp have rel_f[transfer_rule]: "poly_rel f' f''" by (rule poly_rel_of_int_poly[OF f'], simp add: f'' f) from g have g': "g' = of_int_poly_i ff_ops (Mp g)" by simp define g'' where "g'' ≡ of_int_poly (Mp g) :: 'a mod_ring poly" have g'': "g'' = of_int_poly g" unfolding g''_def g by simp have rel_g[transfer_rule]: "poly_rel g' g''" by (rule poly_rel_of_int_poly[OF g'], simp add: g'' g) obtain a'' b'' where eucl: "bezout_coefficients f'' g'' = (a'',b'')" by force from bezout_coefficients_i[unfolded rel_fun_def rel_prod_conv, rule_format, OF rel_f rel_g, unfolded res split eucl] have rel[transfer_rule]: "poly_rel a' a''" "poly_rel b' b''" by auto with to_int_poly_i have a: "a = to_int_poly a''" and b: "b = to_int_poly b''" unfolding a b by auto from bezout_coefficients_mod_int [OF f'' g'' cop eucl a b] show "f * a + g * b =m 1" . show "Mp a = a" "Mp b = b" unfolding a b by (auto simp: Mp_to_int_poly) qed lemma euclid_ext_poly_mod_main: assumes cop: "coprime_m f g" and f: "Mp f = f" and g: "Mp g = g" and res: "euclid_ext_poly_mod_main m ff_ops f g = (a,b)" shows "f * a + g * b =m 1" "Mp a = a" "Mp b = b" proof - obtain a' b' where res': "bezout_coefficients_i ff_ops (of_int_poly_i ff_ops f) (of_int_poly_i ff_ops g) = (a', b')" by force show "f * a + g * b =m 1" "Mp a = a" "Mp b = b" by (insert bezout_coefficients_i_sound[OF refl f refl g cop res'] res [unfolded euclid_ext_poly_mod_main_def res'], auto) qed end context poly_mod_prime begin lemmas euclid_ext_poly_mod_integer = prime_field_gen.euclid_ext_poly_mod_main [OF prime_field.prime_field_finite_field_ops_integer, unfolded prime_field_def mod_ring_locale_def poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty] lemmas euclid_ext_poly_mod_uint32 = prime_field_gen.euclid_ext_poly_mod_main [OF prime_field.prime_field_finite_field_ops32, unfolded prime_field_def mod_ring_locale_def poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty] lemmas euclid_ext_poly_mod_uint64 = prime_field_gen.euclid_ext_poly_mod_main[OF prime_field.prime_field_finite_field_ops64, unfolded prime_field_def mod_ring_locale_def poly_mod_type_simps, internalize_sort "'a :: prime_card", OF type_to_set, unfolded remove_duplicate_premise, cancel_type_definition, OF non_empty] lemma euclid_ext_poly_dynamic: assumes cop: "coprime_m f g" and f: "Mp f = f" and g: "Mp g = g" and res: "euclid_ext_poly_dynamic p f g = (a,b)" shows "f * a + g * b =m 1" "Mp a = a" "Mp b = b" using euclid_ext_poly_mod_integer[OF cop f g, of p a b] euclid_ext_poly_mod_uint32[OF _ cop f g, of p a b] euclid_ext_poly_mod_uint64[OF _ cop f g, of p a b] res[unfolded euclid_ext_poly_dynamic_def] by (auto split: if_splits) end lemma range_sum_prod: assumes xy: "x ∈ {0..<q}" "(y :: int) ∈ {0..<p}" shows "x + q * y ∈ {0..<p * q}" proof - { fix x q :: int have "x ∈ {0 ..< q} ⟷ 0 ≤ x ∧ x < q" by auto } note id = this from xy have 0: "0 ≤ x + q * y" by auto have "x + q * y ≤ q - 1 + q * y" using xy by simp also have "q * y ≤ q * (p - 1)" using xy by auto finally have "x + q * y ≤ q - 1 + q * (p - 1)" by auto also have "… = p * q - 1" by (simp add: field_simps) finally show ?thesis using 0 by auto qed context fixes C :: "int poly" begin context fixes p :: int and S T D1 H1 :: "int poly" begin (* The linear lifting is implemented for ease of provability. Aim: show uniqueness of factorization *) fun linear_hensel_main where "linear_hensel_main (Suc 0) = (D1,H1)" | "linear_hensel_main (Suc n) = ( let (D,H) = linear_hensel_main n; q = p ^ n; U = poly_mod.Mp p (sdiv_poly (C - D * H) q); ― ‹‹H2 + H3›› (A,B) = poly_mod.dupe_monic_int p D1 H1 S T U in (D + smult q B, H + smult q A)) ― ‹‹H4››" | "linear_hensel_main 0 = (D1,H1)" lemma linear_hensel_main: assumes 1: "poly_mod.eq_m p (D1 * S + H1 * T) 1" and equiv: "poly_mod.eq_m p (D1 * H1) C" and monD1: "monic D1" and normDH1: "poly_mod.Mp p D1 = D1" "poly_mod.Mp p H1 = H1" and res: "linear_hensel_main n = (D,H)" and n: "n ≠ 0" and prime: "prime p" ― ‹‹p > 1› suffices if one does not need uniqueness› and cop: "poly_mod.coprime_m p D1 H1" shows "poly_mod.eq_m (p^n) (D * H) C ∧ monic D ∧ poly_mod.eq_m p D D1 ∧ poly_mod.eq_m p H H1 ∧ poly_mod.Mp (p^n) D = D ∧ poly_mod.Mp (p^n) H = H ∧ (poly_mod.eq_m (p^n) (D' * H') C ⟶ poly_mod.eq_m p D' D1 ⟶ poly_mod.eq_m p H' H1 ⟶ poly_mod.Mp (p^n) D' = D' ⟶ poly_mod.Mp (p^n) H' = H' ⟶ monic D' ⟶ D' = D ∧ H' = H) " using res n proof (induct n arbitrary: D H D' H') case (Suc n D' H' D'' H'') show ?case proof (cases "n = 0") case True with Suc equiv monD1 normDH1 show ?thesis by auto next case False hence n: "n ≠ 0" by auto let ?q = "p^n" let ?pq = "p * p^n" from prime have p: "p > 1" using prime_gt_1_int by force from n p have q: "?q > 1" by auto from n p have pq: "?pq > 1" by (metis power_gt1_lemma) interpret p: poly_mod_2 p using p unfolding poly_mod_2_def . interpret q: poly_mod_2 ?q using q unfolding poly_mod_2_def . interpret pq: poly_mod_2 ?pq using pq unfolding poly_mod_2_def . obtain D H where rec: "linear_hensel_main n = (D,H)" by force obtain V where V: "sdiv_poly (C - D * H) ?q = V" by force obtain U where U: "p.Mp (sdiv_poly (C - D * H) ?q) = U" by auto obtain A B where dupe: "p.dupe_monic_int D1 H1 S T U = (A,B)" by force note IH = Suc(1)[OF rec n] from IH have CDH: "q.eq_m (D * H) C" and monD: "monic D" and p_eq: "p.eq_m D D1" "p.eq_m H H1" and norm: "q.Mp D = D" "q.Mp H = H" by auto from n obtain k where n: "n = Suc k" by (cases n, auto) have qq: "?q * ?q = ?pq * p^k" unfolding n by simp from Suc(2)[unfolded n linear_hensel_main.simps, folded n, unfolded rec split Let_def U dupe] have D': "D' = D + smult ?q B" and H': "H' = H + smult ?q A" by auto note dupe = p.dupe_monic_int[OF 1 monD1 dupe] from CDH have "q.Mp C - q.Mp (D * H) = 0" by simp hence "q.Mp (q.Mp C - q.Mp (D * H)) = 0" by simp hence "q.Mp (C - D*H) = 0" by simp from q.Mp_0_smult_sdiv_poly[OF this] have CDHq: "smult ?q (sdiv_poly (C - D * H) ?q) = C - D * H" . have ADBHU: "p.eq_m (A * D + B * H) U" using p_eq dupe(1) by (metis (mono_tags, lifting) p.mult_Mp(2) poly_mod.plus_Mp) have "pq.Mp (D' * H') = pq.Mp ((D + smult ?q B) * (H + smult ?q A))" unfolding D' H' by simp also have "(D + smult ?q B) * (H + smult ?q A) = (D * H + smult ?q (A * D + B * H)) + smult (?q * ?q) (A * B)" by (simp add: field_simps smult_distribs) also have "pq.Mp … = pq.Mp (D * H + pq.Mp (smult ?q (A * D + B * H)) + pq.Mp (smult (?q * ?q) (A * B)))" using pq.plus_Mp by metis also have "pq.Mp (smult (?q * ?q) (A * B)) = 0" unfolding qq by (metis pq.Mp_smult_m_0 smult_smult) finally have DH': "pq.Mp (D' * H') = pq.Mp (D * H + pq.Mp (smult ?q (A * D + B * H)))" by simp also have "pq.Mp (smult ?q (A * D + B * H)) = pq.Mp (smult ?q U)" using p.Mp_lift_modulus[OF ADBHU, of ?q] by simp also have "… = pq.Mp (C - D * H)" unfolding arg_cong[OF CDHq, of pq.Mp, symmetric] U[symmetric] V by (rule p.Mp_lift_modulus[of _ _ ?q], auto) also have "pq.Mp (D * H + pq.Mp (C - D * H)) = pq.Mp C" by simp finally have CDH: "pq.eq_m C (D' * H')" by simp have deg: "degree D1 = degree D" using p_eq(1) monD1 monD by (metis p.monic_degree_m) have mon: "monic D'" unfolding D' using dupe(2) monD unfolding deg by (rule monic_smult_add_small) have normD': "pq.Mp D' = D'" unfolding D' pq.Mp_ident_iff poly_mod.Mp_coeff plus_poly.rep_eq coeff_smult proof fix i from norm(1) dupe(4) have "coeff D i ∈ {0..<?q}" "coeff B i ∈ {0..<p}" unfolding p.Mp_ident_iff q.Mp_ident_iff by auto thus "coeff D i + ?q * coeff B i ∈ {0..< ?pq}" by (rule range_sum_prod) qed have normH': "pq.Mp H' = H'" unfolding H' pq.Mp_ident_iff poly_mod.Mp_coeff plus_poly.rep_eq coeff_smult proof fix i from norm(2) dupe(3) have "coeff H i ∈ {0..<?q}" "coeff A i ∈ {0..<p}" unfolding p.Mp_ident_iff q.Mp_ident_iff by auto thus "coeff H i + ?q * coeff A i ∈ {0..< ?pq}" by (rule range_sum_prod) qed have eq: "p.eq_m D D'" "p.eq_m H H'" unfolding D' H' n poly_eq_iff p.Mp_coeff p.M_def by (auto simp: field_simps) with p_eq have eq: "p.eq_m D' D1" "p.eq_m H' H1" by auto { assume CDH'': "pq.eq_m C (D'' * H'')" and DH1'': "p.eq_m D1 D''" "p.eq_m H1 H''" and norm'': "pq.Mp D'' = D''" "pq.Mp H'' = H''" and monD'': "monic D''" from q.Dp_Mp_eq[of D''] obtain d B' where D'': "D'' = q.Mp d + smult ?q B'" by auto from q.Dp_Mp_eq[of H''] obtain h A' where H'': "H'' = q.Mp h + smult ?q A'" by auto { fix A B assume *: "pq.Mp (q.Mp A + smult ?q B) = q.Mp A + smult ?q B" have "p.Mp B = B" unfolding p.Mp_ident_iff proof fix i from arg_cong[OF *, of "λ f. coeff f i", unfolded pq.Mp_coeff pq.M_def] have "coeff (q.Mp A + smult ?q B) i ∈ {0 ..< ?pq}" using "*" pq.Mp_ident_iff by blast hence sum: "coeff (q.Mp A) i + ?q * coeff B i ∈ {0 ..< ?pq}" by auto have "q.Mp (q.Mp A) = q.Mp A" by auto from this[unfolded q.Mp_ident_iff] have A: "coeff (q.Mp A) i ∈ {0 ..< p^n}" by auto { assume "coeff B i < 0" hence "coeff B i ≤ -1" by auto from mult_left_mono[OF this, of ?q] q.m1 have "?q * coeff B i ≤ -?q" by simp with A sum have False by auto } hence "coeff B i ≥ 0" by force moreover { assume "coeff B i ≥ p" from mult_left_mono[OF this, of ?q] q.m1 have "?q * coeff B i ≥ ?pq" by simp with A sum have False by auto } hence "coeff B i < p" by force ultimately show "coeff B i ∈ {0 ..< p}" by auto qed } note norm_convert = this from norm_convert[OF norm''(1)[unfolded D'']] have normB': "p.Mp B' = B'" . from norm_convert[OF norm''(2)[unfolded H'']] have normA': "p.Mp A' = A'" . let ?d = "q.Mp d" let ?h = "q.Mp h" { assume lt: "degree ?d < degree B'" hence eq: "degree D'' = degree B'" unfolding D'' using q.m1 p.m1 by (subst degree_add_eq_right, auto) from lt have [simp]: "coeff ?d (degree B') = 0" by (rule coeff_eq_0) from monD''[unfolded eq, unfolded D'', simplified] False q.m1 lt have False by (metis mod_mult_self1_is_0 poly_mod.M_def q.M_1 zero_neq_one) } hence deg_dB': "degree ?d ≥ degree B'" by presburger { assume eq: "degree ?d = degree B'" and B': "B' ≠ 0" let ?B = "coeff B' (degree B')" from normB'[unfolded p.Mp_ident_iff, rule_format, of "degree B'"] B' have "?B ∈ {0..<p} - {0}" by simp hence bnds: "?B > 0" "?B < p" by auto have degD'': "degree D'' ≤ degree ?d" unfolding D'' using eq by (simp add: degree_add_le) have "?q * ?B ≥ 1 * 1" by (rule mult_mono, insert q.m1 bnds, auto) moreover have "coeff D'' (degree ?d) = 1 + ?q * ?B" using monD'' unfolding D'' using eq by (metis D'' coeff_smult monD'' plus_poly.rep_eq poly_mod.Dp_Mp_eq poly_mod.degree_m_eq_monic poly_mod.plus_Mp(1) q.Mp_smult_m_0 q.m1 q.monic_Mp q.plus_Mp(2)) ultimately have gt: "coeff D'' (degree ?d) > 1" by auto hence "coeff D'' (degree ?d) ≠ 0" by auto hence "degree D'' ≥ degree ?d" by (rule le_degree) with degree_add_le_max[of ?d "smult ?q B'", folded D''] eq have deg: "degree D'' = degree ?d" using degD'' by linarith from gt[folded this] have "¬ monic D''" by auto with monD'' have False by auto } with deg_dB' have deg_dB2: "B' = 0 ∨ degree B' < degree ?d" by fastforce have d: "q.Mp D'' = ?d" unfolding D'' by (metis add.right_neutral poly_mod.Mp_smult_m_0 poly_mod.plus_Mp) have h: "q.Mp H'' = ?h" unfolding H'' by (metis add.right_neutral poly_mod.Mp_smult_m_0 poly_mod.plus_Mp) from CDH'' have "pq.Mp C = pq.Mp (D'' * H'')" by simp from arg_cong[OF this, of q.Mp] have "q.Mp C = q.Mp (D'' * H'')" using p.m1 q.Mp_product_modulus by auto also have "… = q.Mp (q.Mp D'' * q.Mp H'')" by simp also have "… = q.Mp (?d * ?h)" unfolding d h by simp finally have eqC: "q.eq_m (?d * ?h) C" by auto have d1: "p.eq_m ?d D1" unfolding d[symmetric] using DH1'' using assms(4) n p.Mp_product_modulus p.m1 by auto have h1: "p.eq_m ?h H1" unfolding h[symmetric] using DH1'' using assms(5) n p.Mp_product_modulus p.m1 by auto have mond: "monic (q.Mp d)" using monD'' deg_dB2 unfolding D'' using d q.monic_Mp[OF monD''] by simp from eqC d1 h1 mond IH[of "q.Mp d" "q.Mp h"] have IH: "?d = D" "?h = H" by auto from deg_dB2[unfolded IH] have degB': "B' = 0 ∨ degree B' < degree D" by auto from IH have D'': "D'' = D + smult ?q B'" and H'': "H'' = H + smult ?q A'" unfolding D'' H'' by auto have "pq.Mp (D'' * H'') = pq.Mp (D' * H')" using CDH'' CDH by simp also have "pq.Mp (D'' * H'') = pq.Mp ((D + smult ?q B') * (H + smult ?q A'))" unfolding D'' H'' by simp also have "(D + smult ?q B') * (H + smult ?q A') = (D * H + smult ?q (A' * D + B' * H)) + smult (?q * ?q) (A' * B')" by (simp add: field_simps smult_distribs) also have "pq.Mp … = pq.Mp (D * H + pq.Mp (smult ?q (A' * D + B' * H)) + pq.Mp (smult (?q * ?q) (A' * B')))" using pq.plus_Mp by metis also have "pq.Mp (smult (?q * ?q) (A' * B')) = 0" unfolding qq by (metis pq.Mp_smult_m_0 smult_smult) finally have "pq.Mp (D * H + pq.Mp (smult ?q (A' * D + B' * H))) = pq.Mp (D * H + pq.Mp (smult ?q (A * D + B * H)))" unfolding DH' by simp hence "pq.Mp (smult ?q (A' * D + B' * H)) = pq.Mp (smult ?q (A * D + B * H))" by (metis (no_types, lifting) add_diff_cancel_left' poly_mod.minus_Mp(1) poly_mod.plus_Mp(2)) hence "p.Mp (A' * D + B' * H) = p.Mp (A * D + B * H)" unfolding poly_eq_iff p.Mp_coeff pq.Mp_coeff coeff_smult by (insert p, auto simp: p.M_def pq.M_def) hence "p.Mp (A' * D1 + B' * H1) = p.Mp (A * D1 + B * H1)" using p_eq by (metis p.mult_Mp(2) poly_mod.plus_Mp) hence eq: "p.eq_m (A' * D1 + B' * H1) U" using dupe(1) by auto have "degree D = degree D1" using monD monD1 arg_cong[OF p_eq(1), of degree] p.degree_m_eq_monic[OF _ p.m1] by auto hence "B' = 0 ∨ degree B' < degree D1" using degB' by simp from dupe(5)[OF cop eq this normDH1(1) normA' normB' prime] have "A' = A" "B' = B" by auto hence "D'' = D'" "H'' = H'" unfolding D'' H'' D' H' by auto } thus ?thesis using normD' normH' CDH mon eq by simp qed qed simp end end definition linear_hensel_binary :: "int ⇒ nat ⇒ int poly ⇒ int poly ⇒ int poly ⇒ int poly × int poly" where "linear_hensel_binary p n C D H = (let (S,T) = euclid_ext_poly_dynamic p D H in linear_hensel_main C p S T D H n)" lemma (in poly_mod_prime) unique_hensel_binary: assumes prime: "prime p" and cop: "coprime_m D H" and eq: "eq_m (D * H) C" and normalized_input: "Mp D = D" "Mp H = H" and monic_input: "monic D" and n: "n ≠ 0" shows "∃! (D',H'). ― ‹‹D'›, ‹H'› are computed via ‹linear_hensel_binary›› poly_mod.eq_m (p^n) (D' * H') C ― ‹the main result: equivalence mod ‹p^n›› ∧ monic D' ― ‹monic output› ∧ eq_m D D' ∧ eq_m H H' ― ‹apply ‹`mod p`› on ‹D'› and ‹H'› yields ‹D› and ‹H› again› ∧ poly_mod.Mp (p^n) D' = D' ∧ poly_mod.Mp (p^n) H' = H' ― ‹output is normalized›" proof - obtain D' H' where hensel_result: "linear_hensel_binary p n C D H = (D',H')" by force from m1 have p: "p > 1" . obtain S T where ext: "euclid_ext_poly_dynamic p D H = (S,T)" by force obtain D1 H1 where main: "linear_hensel_main C p S T D H n = (D1,H1)" by force from hensel_result[unfolded linear_hensel_binary_def ext split Let_def main] have id: "D1 = D'" "H1 = H'" by auto note eucl = euclid_ext_poly_dynamic [OF cop normalized_input ext] from linear_hensel_main [OF eucl(1) eq monic_input normalized_input main [unfolded id] n prime cop] show ?thesis by (intro ex1I, auto) qed (* The quadratic lifting is implemented more efficienty. Aim: compute factorization *) context fixes C :: "int poly" begin lemma hensel_step_main: assumes one_q: "poly_mod.eq_m q (D * S + H * T) 1" and one_p: "poly_mod.eq_m p (D1 * S1 + H1 * T1) 1" and CDHq: "poly_mod.eq_m q C (D * H)" and D1D: "poly_mod.eq_m p D1 D" and H1H: "poly_mod.eq_m p H1 H" and S1S: "poly_mod.eq_m p S1 S" and T1T: "poly_mod.eq_m p T1 T" and mon: "monic D" and mon1: "monic D1" and q: "q > 1" and p: "p > 1" and D1: "poly_mod.Mp p D1 = D1" and H1: "poly_mod.Mp p H1 = H1" and S1: "poly_mod.Mp p S1 = S1" and T1: "poly_mod.Mp p T1 = T1" and D: "poly_mod.Mp q D = D" and H: "poly_mod.Mp q H = H" and S: "poly_mod.Mp q S = S" and T: "poly_mod.Mp q T = T" and U1: "U1 = poly_mod.Mp p (sdiv_poly (C - D * H) q)" and dupe1: "dupe_monic_dynamic p D1 H1 S1 T1 U1 = (A,B)" and D': "D' = D + smult q B" and H': "H' = H + smult q A" and U2: "U2 = poly_mod.Mp q (sdiv_poly (S*D' + T*H' - 1) p)" and dupe2: "dupe_monic_dynamic q D H S T U2 = (A',B')" and rq: "r = p * q" and pq: "p dvd q" and S': "S' = poly_mod.Mp r (S - smult p A')" and T': "T' = poly_mod.Mp r (T - smult p B')" shows "poly_mod.eq_m r C (D' * H')" "poly_mod.Mp r D' = D'" "poly_mod.Mp r H' = H'" "poly_mod.Mp r S' = S'" "poly_mod.Mp r T' = T'" "poly_mod.eq_m r (D' * S' + H' * T') 1" "monic D'" unfolding rq proof - from pq obtain k where qp: "q = p * k" unfolding dvd_def by auto from arg_cong[OF qp, of sgn] q p have k0: "k > 0" unfolding sgn_mult by (auto simp: sgn_1_pos) from qp have qq: "q * q = p * q * k" by auto let ?r = "p * q" interpret poly_mod_2 p by (standard, insert p, auto) interpret q: poly_mod_2 q by (standard, insert q, auto) from p q have r: "?r > 1" by (simp add: less_1_mult) interpret r: poly_mod_2 ?r using r unfolding poly_mod_2_def . have Mp_conv: "Mp (q.Mp x) = Mp x" for x unfolding qp by (rule Mp_product_modulus[OF refl k0]) from arg_cong[OF CDHq, of Mp, unfolded Mp_conv] have "Mp C = Mp (Mp D * Mp H)" by simp also have "Mp D = Mp D1" using D1D by simp also have "Mp H = Mp H1" using H1H by simp finally have CDHp: "eq_m C (D1 * H1)" by simp have "Mp U1 = U1" unfolding U1 by simp note dupe1 = dupe_monic_dynamic[OF dupe1 one_p mon1 D1 H1 S1 T1 this] have "q.Mp U2 = U2" unfolding U2 by simp note dupe2 = q.dupe_monic_dynamic[OF dupe2 one_q mon D H S T this] from CDHq have "q.Mp C - q.Mp (D * H) = 0" by simp hence "q.Mp (q.Mp C - q.Mp (D * H)) = 0" by simp hence "q.Mp (C - D*H) = 0" by simp from q.Mp_0_smult_sdiv_poly[OF this] have CDHq: "smult q (sdiv_poly (C - D * H) q) = C - D * H" . { fix A B have "Mp (A * D1 + B * H1) = Mp (Mp (A * D1) + Mp (B * H1))" by simp also have "Mp (A * D1) = Mp (A * Mp D1)" by simp also have "… = Mp (A * D)" unfolding D1D by simp also have "Mp (B * H1) = Mp (B * Mp H1)" by simp also have "… = Mp (B * H)" unfolding H1H by simp finally have "Mp (A * D1 + B * H1) = Mp (A * D + B * H)" by simp } note D1H1 = this have "r.Mp (D' * H') = r.Mp ((D + smult q B) * (H + smult q A))" unfolding D' H' by simp also have "(D + smult q B) * (H + smult q A) = (D * H + smult q (A * D + B * H)) + smult (q * q) (A * B)" by (simp add: field_simps smult_distribs) also have "r.Mp … = r.Mp (D * H + r.Mp (smult q (A * D + B * H)) + r.Mp (smult (q * q) (A * B)))" using r.plus_Mp by metis also have "r.Mp (smult (q * q) (A * B)) = 0" unfolding qq by (metis r.Mp_smult_m_0 smult_smult) also have "r.Mp (smult q (A * D + B * H)) = r.Mp (smult q U1)" proof (rule Mp_lift_modulus[of _ _ q]) show "Mp (A * D + B * H) = Mp U1" using dupe1(1) unfolding D1H1 by simp qed also have "… = r.Mp (C - D * H)" unfolding arg_cong[OF CDHq, of r.Mp, symmetric] using Mp_lift_modulus[of U1 "sdiv_poly (C - D * H) q" q] unfolding U1 by simp also have "r.Mp (D * H + r.Mp (C - D * H) + 0) = r.Mp C" by simp finally show CDH: "r.eq_m C (D' * H')" by simp have "degree D1 = degree (Mp D1)" using mon1 by simp also have "… = degree D" unfolding D1D using mon by simp finally have deg_eq: "degree D1 = degree D" by simp show mon: "monic D'" unfolding D' using dupe1(2) mon unfolding deg_eq by (rule monic_smult_add_small) have "Mp (S * D' + T * H' - 1) = Mp (Mp (D * S + H * T) + (smult q (S * B + T * A) - 1))" unfolding D' H' plus_Mp by (simp add: field_simps smult_distribs) also have "Mp (D * S + H * T) = Mp (Mp (D1 * Mp S) + Mp (H1 * Mp T))" using D1H1[of S T] by (simp add: ac_simps) also have "… = 1" using one_p unfolding S1S[symmetric] T1T[symmetric] by simp also have "Mp (1 + (smult q (S * B + T * A) - 1)) = Mp (smult q (S * B + T * A))" by simp also have "… = 0" unfolding qp by (metis Mp_smult_m_0 smult_smult) finally have "Mp (S * D' + T * H' - 1) = 0" . from Mp_0_smult_sdiv_poly[OF this] have SDTH: "smult p (sdiv_poly (S * D' + T * H' - 1) p) = S * D' + T * H' - 1" . have swap: "q * p = p * q" by simp have "r.Mp (D' * S' + H' * T') = r.Mp ((D + smult q B) * (S - smult p A') + (H + smult q A) * (T - smult p B'))" unfolding D' S' H' T' rq using r.plus_Mp r.mult_Mp by metis also have "… = r.Mp ((D * S + H * T + smult q (B * S + A * T)) - smult p (A' * D + B' * H) - smult ?r (A * B' + B * A'))" by (simp add: field_simps smult_distribs) also have "… = r.Mp ((D * S + H * T + smult q (B * S + A * T)) - r.Mp (smult p (A' * D + B' * H)) - r.Mp (smult ?r (A * B' + B * A')))" using r.plus_Mp r.minus_Mp by metis also have "r.Mp (smult ?r (A * B' + B * A')) = 0" by simp also have "r.Mp (smult p (A' * D + B' * H)) = r.Mp (smult p U2)" using q.Mp_lift_modulus[OF dupe2(1), of p] unfolding swap . also have "… = r.Mp (S * D' + T * H' - 1)" unfolding arg_cong[OF SDTH, of r.Mp, symmetric] using q.Mp_lift_modulus[of U2 "sdiv_poly (S * D' + T * H' - 1) p" p] unfolding U2 swap by simp also have "S * D' + T * H' - 1 = S * D + T * H + smult q (B * S + A * T) - 1" unfolding D' H' by (simp add: field_simps smult_distribs) also have "r.Mp (D * S + H * T + smult q (B * S + A * T) - r.Mp (S * D + T * H + smult q (B * S + A * T) - 1) - 0) = 1" by simp finally show 1: "r.eq_m (D' * S' + H' * T') 1" by simp show D': "r.Mp D' = D'" unfolding D' r.Mp_ident_iff poly_mod.Mp_coeff plus_poly.rep_eq coeff_smult proof fix n from D dupe1(4) have "coeff D n ∈ {0..<q}" "coeff B n ∈ {0..<p}" unfolding q.Mp_ident_iff Mp_ident_iff by auto thus "coeff D n + q * coeff B n ∈ {0..<?r}" by (metis range_sum_prod) qed show H': "r.Mp H' = H'" unfolding H' r.Mp_ident_iff poly_mod.Mp_coeff plus_poly.rep_eq coeff_smult proof fix n from H dupe1(3) have "coeff H n ∈ {0..<q}" "coeff A n ∈ {0..<p}" unfolding q.Mp_ident_iff Mp_ident_iff by auto thus "coeff H n + q * coeff A n ∈ {0..<?r}" by (metis range_sum_prod) qed show "poly_mod.Mp ?r S' = S'" "poly_mod.Mp ?r T' = T'" unfolding S' T' rq by auto qed definition hensel_step where "hensel_step p q S1 T1 D1 H1 S T D H = ( let U = poly_mod.Mp p (sdiv_poly (C - D * H) q); ― ‹‹Z2 and Z3›› (A,B) = dupe_monic_dynamic p D1 H1 S1 T1 U; D' = D + smult q B; ― ‹‹Z4›› H' = H + smult q A; U' = poly_mod.Mp q (sdiv_poly (S*D' + T*H' - 1) p); ― ‹‹Z5 + Z6›› (A',B') = dupe_monic_dynamic q D H S T U'; q' = p * q; S' = poly_mod.Mp q' (S - smult p A'); ― ‹‹Z7›› T' = poly_mod.Mp q' (T - smult p B') in (S',T',D',H'))" definition "quadratic_hensel_step q S T D H = hensel_step q q S T D H S T D H" lemma quadratic_hensel_step_code[code]: "quadratic_hensel_step q S T D H = (let dupe = dupe_monic_dynamic q D H S T; ― ‹this will share the conversions of ‹D H S T›› U = poly_mod.Mp q (sdiv_poly (C - D * H) q); (A, B) = dupe U; D' = D + Polynomial.smult q B; H' = H + Polynomial.smult q A; U' = poly_mod.Mp q (sdiv_poly (S * D' + T * H' - 1) q); (A', B') = dupe U'; q' = q * q; S' = poly_mod.Mp q' (S - Polynomial.smult q A'); T' = poly_mod.Mp q' (T - Polynomial.smult q B') in (S', T', D', H'))" unfolding quadratic_hensel_step_def[unfolded hensel_step_def] Let_def .. definition simple_quadratic_hensel_step where ― ‹do not compute new values ‹S'› and ‹T'›› "simple_quadratic_hensel_step q S T D H = ( let U = poly_mod.Mp q (sdiv_poly (C - D * H) q); ― ‹‹Z2 + Z3›› (A,B) = dupe_monic_dynamic q D H S T U; D' = D + smult q B; ― ‹‹Z4›› H' = H + smult q A in (D',H'))" lemma hensel_step: assumes step: "hensel_step p q S1 T1 D1 H1 S T D H = (S', T', D', H')" and one_p: "poly_mod.eq_m p (D1 * S1 + H1 * T1) 1" and mon1: "monic D1" and p: "p > 1" and CDHq: "poly_mod.eq_m q C (D * H)" and one_q: "poly_mod.eq_m q (D * S + H * T) 1" and D1D: "poly_mod.eq_m p D1 D" and H1H: "poly_mod.eq_m p H1 H" and S1S: "poly_mod.eq_m p S1 S" and T1T: "poly_mod.eq_m p T1 T" and mon: "monic D" and q: "q > 1" and D1: "poly_mod.Mp p D1 = D1" and H1: "poly_mod.Mp p H1 = H1" and S1: "poly_mod.Mp p S1 = S1" and T1: "poly_mod.Mp p T1 = T1" and D: "poly_mod.Mp q D = D" and H: "poly_mod.Mp q H = H" and S: "poly_mod.Mp q S = S" and T: "poly_mod.Mp q T = T" and rq: "r = p * q" and pq: "p dvd q" shows "poly_mod.eq_m r C (D' * H')" "poly_mod.eq_m r (D' * S' + H' * T') 1" "poly_mod.Mp r D' = D'" "poly_mod.Mp r H' = H'" "poly_mod.Mp r S' = S'" "poly_mod.Mp r T' = T'" "poly_mod.Mp p D1 = poly_mod.Mp p D'" "poly_mod.Mp p H1 = poly_mod.Mp p H'" "poly_mod.Mp p S1 = poly_mod.Mp p S'" "poly_mod.Mp p T1 = poly_mod.Mp p T'" "monic D'" proof - define U where U: "U = poly_mod.Mp p (sdiv_poly (C - D * H) q)" note step = step[unfolded hensel_step_def Let_def, folded U] obtain A B where dupe1: "dupe_monic_dynamic p D1 H1 S1 T1 U = (A,B)" by force note step = step[unfolded dupe1 split] from step have D': "D' = D + smult q B" and H': "H' = H + smult q A" by (auto split: prod.splits) define U' where U': "U' = poly_mod.Mp q (sdiv_poly (S * D' + T * H' - 1) p)" obtain A' B' where dupe2: "dupe_monic_dynamic q D H S T U' = (A',B')" by force from step[folded D' H', folded U', unfolded dupe2 split, folded rq] have S': "S' = poly_mod.Mp r (S - Polynomial.smult p A')" and T': "T' = poly_mod.Mp r (T - Polynomial.smult p B')" by auto from hensel_step_main[OF one_q one_p CDHq D1D H1H S1S T1T mon mon1 q p D1 H1 S1 T1 D H S T U dupe1 D' H' U' dupe2 rq pq S' T'] show "poly_mod.eq_m r (D' * S' + H' * T') 1" "poly_mod.eq_m r C (D' * H')" "poly_mod.Mp r D' = D'" "poly_mod.Mp r H' = H'" "poly_mod.Mp r S' = S'" "poly_mod.Mp r T' = T'" "monic D'" by auto from pq obtain s where q: "q = p * s" by (metis dvdE) show "poly_mod.Mp p D1 = poly_mod.Mp p D'" "poly_mod.Mp p H1 = poly_mod.Mp p H'" unfolding q D' D1D H' H1H by (metis add.right_neutral poly_mod.Mp_smult_m_0 poly_mod.plus_Mp(2) smult_smult)+ from ‹q > 1› have q0: "q > 0" by auto show "poly_mod.Mp p S1 = poly_mod.Mp p S'" "poly_mod.Mp p T1 = poly_mod.Mp p T'" unfolding S' S1S T' T1T poly_mod_2.Mp_product_modulus[OF poly_mod_2.intro[OF ‹p > 1›] rq q0] by (metis group_add_class.diff_0_right poly_mod.Mp_smult_m_0 poly_mod.minus_Mp(2))+ qed lemma quadratic_hensel_step: assumes step: "quadratic_hensel_step q S T D H = (S', T', D', H')" and CDH: "poly_mod.eq_m q C (D * H)" and one: "poly_mod.eq_m q (D * S + H * T) 1" and D: "poly_mod.Mp q D = D" and H: "poly_mod.Mp q H = H" and S: "poly_mod.Mp q S = S" and T: "poly_mod.Mp q T = T" and mon: "monic D" and q: "q > 1" and rq: "r = q * q" shows "poly_mod.eq_m r C (D' * H')" "poly_mod.eq_m r (D' * S' + H' * T') 1" "poly_mod.Mp r D' = D'" "poly_mod.Mp r H' = H'" "poly_mod.Mp r S' = S'" "poly_mod.Mp r T' = T'" "poly_mod.Mp q D = poly_mod.Mp q D'" "poly_mod.Mp q H = poly_mod.Mp q H'" "poly_mod.Mp q S = poly_mod.Mp q S'" "poly_mod.Mp q T = poly_mod.Mp q T'" "monic D'" proof (atomize(full), goal_cases) case 1 from hensel_step[OF step[unfolded quadratic_hensel_step_def] one mon q CDH one refl refl refl refl mon q D H S T D H S T rq] show ?case by auto qed context fixes p :: int and S1 T1 D1 H1 :: "int poly" begin private lemma decrease[termination_simp]: "¬ j ≤ 1 ⟹ odd j ⟹ Suc (j div 2) < j" by presburger fun quadratic_hensel_loop where "quadratic_hensel_loop (j :: nat) = ( if j ≤ 1 then (p, S1, T1, D1, H1) else if even j then (case quadratic_hensel_loop (j div 2) of (q, S, T, D, H) ⇒ let qq = q * q in (case quadratic_hensel_step q S T D H of ― ‹quadratic step› (S', T', D', H') ⇒ (qq, S', T', D', H'))) else ― ‹odd ‹j›› (case quadratic_hensel_loop (j div 2 + 1) of (q, S, T, D, H) ⇒ (case quadratic_hensel_step q S T D H of ― ‹quadratic step› (S', T', D', H') ⇒ let qq = q * q; pj = qq div p; down = poly_mod.Mp pj in (pj, down S', down T', down D', down H'))))" definition "quadratic_hensel_main j = (case quadratic_hensel_loop j of (qq, S, T, D, H) ⇒ (D, H))" declare quadratic_hensel_loop.simps[simp del] ― ‹unroll the definition of ‹hensel_loop› so that in outermost iteration we can use ‹simple_hensel_step›› lemma quadratic_hensel_main_code[code]: "quadratic_hensel_main j = ( if j ≤ 1 then (D1, H1) else if even j then (case quadratic_hensel_loop (j div 2) of (q, S, T, D, H) ⇒ simple_quadratic_hensel_step q S T D H) else (case