# Theory Hensel_Lifting_Type_Based

```(*
Authors:      Jose Divasón
Sebastiaan Joosten
René Thiemann
*)
theory Hensel_Lifting_Type_Based
imports Hensel_Lifting
begin

subsection‹Hensel Lifting in a Type-Based Setting›

(* TODO: Move? *)

lemma degree_smult_eq_iff:
"degree (smult a p) = degree p ⟷ degree p = 0 ∨ a * lead_coeff p ≠ 0"
by (metis (no_types, lifting) coeff_smult degree_0 degree_smult_le le_antisym

lemma degree_smult_eqI[intro!]:
assumes "degree p ≠ 0 ⟹ a * lead_coeff p ≠ 0"
shows "degree (smult a p) = degree p"
using assms degree_smult_eq_iff by auto

lemma degree_mult_eq2:
shows "degree (p * q) = degree p + degree q" (is "_ = ?r")
proof(intro antisym[OF degree_mult_le] le_degree, unfold coeff_mult)
let ?f = "λi. coeff p i * coeff q (?r - i)"
have "(∑i≤?r. ?f i) = sum ?f {..degree p} + sum ?f {Suc (degree p)..?r}"
by (rule sum_up_index_split)
also have "sum ?f {Suc (degree p)..?r} = 0"
proof-
{ fix x assume "x > degree p"
then have "coeff p x = 0" by (rule coeff_eq_0)
then have "?f x = 0" by auto
}
then show ?thesis by (intro sum.neutral, auto)
qed
also have "sum ?f {..degree p} = sum ?f {..<degree p} + ?f (degree p)"
by(fold lessThan_Suc_atMost, unfold sum.lessThan_Suc, auto)
also have "sum ?f {..<degree p} = 0"
proof-
{fix x assume "x < degree p"
then have "coeff q (?r - x) = 0" by (intro coeff_eq_0, auto)
then have "?f x = 0" by auto
}
then show ?thesis by (intro sum.neutral, auto)
qed
finally show "(∑i≤?r. ?f i) ≠ 0" using assms by (auto simp:)
qed

lemma degree_mult_eq_left_unit:
fixes p q :: "'a :: comm_semiring_1 poly"
assumes unit: "lead_coeff p dvd 1" and q0: "q ≠ 0"
shows "degree (p * q) = degree p + degree q"
proof(intro degree_mult_eq2 notI)
from unit obtain c where "lead_coeff p * c = 1" by (elim dvdE,auto)
then have "c * lead_coeff p = 1" by (auto simp: ac_simps)
then have "c * lead_coeff p * lead_coeff q = 0" by (auto simp: ac_simps)
ultimately have "lead_coeff q = 0" by auto
with q0 show False by auto
qed

context ring_hom begin
lemma monic_degree_map_poly_hom: "monic p ⟹ degree (map_poly hom p) = degree p"
by (auto intro: degree_map_poly)

lemma monic_map_poly_hom: "monic p ⟹ monic (map_poly hom p)"

end

lemma of_nat_zero:
assumes "CARD('a::nontriv) dvd n"
shows "(of_nat n :: 'a mod_ring) = 0"
apply (transfer fixing: n) using assms by (presburger)

abbreviation rebase :: "'a :: nontriv mod_ring ⇒ 'b :: nontriv mod_ring "("@_" [100]100)
where "@x ≡ of_int (to_int_mod_ring x)"

abbreviation rebase_poly :: "'a :: nontriv mod_ring poly ⇒ 'b :: nontriv mod_ring poly" ("#_" [100]100)
where "#x ≡ of_int_poly (to_int_poly x)"

lemma rebase_self [simp]:
"@x = x"

lemma map_poly_rebase [simp]:
"map_poly rebase p = #p"
by (induct p) simp_all

lemma rebase_poly_0: "#0 = 0"
by simp

lemma rebase_poly_1: "#1 = 1"
by simp

lemma rebase_poly_pCons[simp]: "#pCons a p = pCons (@a) (#p)"
by(cases "a = 0 ∧ p = 0", simp, fold map_poly_rebase, subst map_poly_pCons, auto)

lemma rebase_poly_self[simp]: "#p = p" by (induct p, auto)

lemma degree_rebase_poly_le: "degree (#p) ≤ degree p"
by (fold map_poly_rebase, subst degree_map_poly_le, auto)

lemma(in comm_ring_hom) degree_map_poly_unit: assumes "lead_coeff p dvd 1"
shows "degree (map_poly hom p) = degree p"
using hom_dvd_1[OF assms] by (auto intro: degree_map_poly)

lemma rebase_poly_eq_0_iff:
"(#p :: 'a :: nontriv mod_ring poly) = 0 ⟷ (∀i. (@coeff p i :: 'a mod_ring) = 0)" (is "?l ⟷ ?r")
proof(intro iffI)
assume ?l
then have "coeff (#p :: 'a mod_ring poly) i = 0" for i by auto
then show ?r by auto
next
assume ?r
then have "coeff (#p :: 'a mod_ring poly) i = 0" for i by auto
then show ?l by (intro poly_eqI, auto)
qed

lemma mod_mod_le:
assumes ab: "(a::int) ≤ b" and a0: "0 < a" and c0: "c ≥ 0" shows "(c mod a) mod b = c mod a"
by (meson Divides.pos_mod_bound Divides.pos_mod_sign a0 ab less_le_trans mod_pos_pos_trivial)

locale rebase_ge =
fixes ty1 :: "'a :: nontriv itself" and ty2 :: "'b :: nontriv itself"
assumes card: "CARD('a) ≤ CARD('b)"
begin

lemma ab: "int CARD('a) ≤ CARD('b)" using card by auto

lemma rebase_eq_0[simp]:
shows "(@(x :: 'a mod_ring) :: 'b mod_ring) = 0 ⟷ x = 0"
using card by (transfer, auto)

lemma degree_rebase_poly_eq[simp]:
shows "degree (#(p :: 'a mod_ring poly) :: 'b mod_ring poly) = degree p"
by (subst degree_map_poly; simp)

by simp

lemma to_int_mod_ring_rebase: "to_int_mod_ring(@(x :: 'a mod_ring)::'b mod_ring) = to_int_mod_ring x"
using card by (transfer, auto)

lemma rebase_id[simp]: "@(@(x::'a mod_ring) :: 'b mod_ring) = @x"
using card by (transfer, auto)

lemma rebase_poly_id[simp]: "#(#(p::'a mod_ring poly) :: 'b mod_ring poly) = #p" by (induct p, auto)

end

locale rebase_dvd =
fixes ty1 :: "'a :: nontriv itself" and ty2 :: "'b :: nontriv itself"
assumes dvd: "CARD('b) dvd CARD('a)"
begin

lemma ab: "CARD('a) ≥ CARD('b)" by (rule dvd_imp_le[OF dvd], auto)

lemma rebase_id[simp]: "@(@(x::'b mod_ring) :: 'a mod_ring) = x" using ab by (transfer, auto)

lemma rebase_poly_id[simp]: "#(#(p::'b mod_ring poly) :: 'a mod_ring poly) = p" by (induct p, auto)

lemma rebase_of_nat[simp]: "(@(of_nat n :: 'a mod_ring) :: 'b mod_ring) = of_nat n"
apply transfer apply (rule mod_mod_cancel) using dvd by presburger

lemma mod_1_lift_nat:
assumes "(of_int (int x) :: 'a mod_ring) = 1"
shows "(of_int (int x) :: 'b mod_ring) = 1"
proof -
from assms have "int x mod CARD('a) = 1"
by transfer
then have "x mod CARD('a) = 1"
then have "x mod CARD('b) = 1"
by (metis dvd mod_mod_cancel one_mod_card)
then have "int x mod CARD('b) = 1"
then show ?thesis
by transfer
qed

sublocale comm_ring_hom "rebase :: 'a mod_ring ⇒ 'b mod_ring"
proof
fix x y :: "'a mod_ring"
show hom_add: "(@(x+y) :: 'b mod_ring) = @x + @y"
by transfer (simp add: mod_simps dvd mod_mod_cancel)
show "(@(x*y) :: 'b mod_ring) = @x * @y"
by transfer (simp add: mod_simps dvd mod_mod_cancel)
qed auto

lemma of_nat_CARD_eq_0[simp]: "(of_nat CARD('a) :: 'b mod_ring) = 0"
using dvd by (transfer, presburger)

interpretation map_poly_hom: map_poly_comm_ring_hom "rebase :: 'a mod_ring ⇒ 'b mod_ring"..

sublocale poly: comm_ring_hom "rebase_poly :: 'a mod_ring poly ⇒ 'b mod_ring poly"
by (fold map_poly_rebase, unfold_locales)

lemma poly_rebase[simp]: "@poly p x = poly (#(p :: 'a mod_ring poly) :: 'b mod_ring poly) (@(x::'a mod_ring) :: 'b mod_ring)"
by (fold map_poly_rebase poly_map_poly, rule)

lemma rebase_poly_smult[simp]: "(#(smult a p :: 'a mod_ring poly) :: 'b mod_ring poly) = smult (@a) (#p)"
by(induct p, auto simp: hom_distribs)

end

locale rebase_mult =
fixes ty1 :: "'a :: nontriv itself"
and ty2 :: "'b :: nontriv itself"
and ty3 :: "'d :: nontriv itself" (* due to some type reason, 'd has to be nontriv. *)
assumes d: "CARD('a) = CARD('b) * CARD('d)"
begin

sublocale rebase_dvd ty1 ty2 using d by (unfold_locales, auto)

lemma rebase_mult_eq[simp]: "(of_nat CARD('d) * a :: 'a mod_ring) = of_nat CARD('d) * a' ⟷ (@a :: 'b mod_ring) = @a'"
proof-
from dvd obtain d' where "CARD('a) = d' * CARD('b)" by (elim dvdE, auto)
then show ?thesis by (transfer, auto simp:d)
qed

lemma rebase_poly_smult_eq[simp]:
fixes a a' :: "'a mod_ring poly"
defines "d ≡ of_nat CARD('d) :: 'a mod_ring"
shows "smult d a = smult d a' ⟷ (#a :: 'b mod_ring poly) = #a'" (is "?l ⟷ ?r")
proof (intro iffI)
assume l: ?l show "?r"
proof (intro poly_eqI)
fix n
from l have "coeff (smult d a) n = coeff (smult d a') n" by auto
then have "d * coeff a n = d * coeff a' n" by auto
from this[unfolded d_def rebase_mult_eq]
show "coeff (#a :: 'b mod_ring poly) n = coeff (#a') n" by auto
qed
next
assume r: ?r show ?l
proof(intro poly_eqI)
fix n
from r have "coeff (#a :: 'b mod_ring poly) n = coeff (#a') n" by auto
then have "(@coeff a n :: 'b mod_ring) = @coeff a' n" by auto
from this[folded d_def rebase_mult_eq]
show "coeff (smult d a) n = coeff (smult d a') n" by auto
qed
qed

lemma rebase_eq_0_imp_ex_mult:
"(@(a :: 'a mod_ring) :: 'b mod_ring) = 0 ⟹ (∃c :: 'd mod_ring. a = of_nat CARD('b) * @c)" (is "?l ⟹ ?r")
proof(cases "CARD('a) = CARD('b)")
case True then show "?l ⟹ ?r"
by (transfer, auto)
next
case False
have [simp]: "int CARD('b) mod int CARD('a) = int CARD('b)"
by(rule mod_pos_pos_trivial, insert ab False, auto)
{
fix a
assume a: "0 ≤ a" "a < int CARD('a)" and mod: "a mod int CARD('b) = 0"
from mod have "int CARD('b) dvd a" by auto
then obtain i where *: "a = int CARD('b) * i" by (elim dvdE, auto)
from * a have "i < int CARD('d)" by (simp add:d)
moreover
hence "(i mod int CARD('a)) = i"
by (metis dual_order.order_iff_strict less_le_trans not_le of_nat_less_iff "*" a(1) a(2)
mod_pos_pos_trivial mult_less_cancel_right1 nat_neq_iff nontriv of_nat_1)
with * a have "a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)"
by (auto simp:d)
moreover from * a have "0 ≤ i"
using linordered_semiring_strict_class.mult_pos_neg of_nat_0_less_iff zero_less_card_finite
ultimately have "∃i≥0. i < int CARD('d) ∧ a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)"
by (auto intro: exI[of _ i])
}
then show "?l ⟹ ?r" by (transfer, auto simp:d)
qed

lemma rebase_poly_eq_0_imp_ex_smult:
"(#(p :: 'a mod_ring poly) :: 'b mod_ring poly) = 0 ⟹
(∃p' :: 'd mod_ring poly. (p = 0 ⟷ p' = 0) ∧ degree p' ≤ degree p ∧ p = smult (of_nat CARD('b)) (#p'))"
(is "?l ⟹ ?r")
proof(induct p)
case 0
then show ?case by (intro exI[of _ 0],auto)
next
case IH: (pCons a p)
from IH(3) have "(#p :: 'b mod_ring poly) = 0" by auto
from IH(2)[OF this] obtain p' :: "'d mod_ring poly"
where *: "p = 0 ⟷ p' = 0" "degree p' ≤ degree p" "p = smult (of_nat CARD('b)) (#p')" by (elim exE conjE)
from IH have "(@a :: 'b mod_ring) = 0" by auto
from rebase_eq_0_imp_ex_mult[OF this]
obtain a' :: "'d mod_ring" where a': "of_nat CARD('b) * (@a') = a" by auto
from IH(1) have "pCons a p ≠ 0" by auto
moreover from *(1,2) have "degree (pCons a' p') ≤ degree (pCons a p)" by auto
moreover from a' *(3)
have "pCons a p = smult (of_nat CARD('b)) (#pCons a' p')" by auto
ultimately show ?case by (intro exI[of _ "pCons a' p'"], auto)
qed

end

lemma mod_mod_nat[simp]: "a mod b mod (b * c :: nat) = a mod b" by (simp add: Divides.mod_mult2_eq)

locale Knuth_ex_4_6_2_22_base =
fixes ty_p :: "'p :: nontriv itself"
and ty_q :: "'q :: nontriv itself"
and ty_pq :: "'pq :: nontriv itself"
assumes pq: "CARD('pq) = CARD('p) * CARD('q)"
and p_dvd_q: "CARD('p) dvd CARD('q)"
begin

sublocale rebase_q_to_p: rebase_dvd "TYPE('q)" "TYPE('p)" using p_dvd_q by (unfold_locales, auto)
sublocale rebase_pq_to_p: rebase_mult "TYPE('pq)" "TYPE('p)" "TYPE('q)" using pq by (unfold_locales, auto)
sublocale rebase_pq_to_q: rebase_mult "TYPE('pq)" "TYPE('q)" "TYPE('p)" using pq by (unfold_locales, auto)

sublocale rebase_p_to_q: rebase_ge "TYPE('p)" "TYPE ('q)" by (unfold_locales, insert p_dvd_q, simp add: dvd_imp_le)
sublocale rebase_p_to_pq: rebase_ge "TYPE('p)" "TYPE ('pq)" by (unfold_locales, simp add: pq)
sublocale rebase_q_to_pq: rebase_ge "TYPE('q)" "TYPE ('pq)" by (unfold_locales, simp add: pq)

(* TODO: needs ugly workaround to fix 'p... *)
definition "p ≡ if (ty_p :: 'p itself) = ty_p then CARD('p) else undefined"
lemma p[simp]: "p ≡ CARD('p)" unfolding p_def by auto

definition "q ≡ if (ty_q :: 'q itself) = ty_q then CARD('q) else undefined"
lemma q[simp]: "q = CARD('q)" unfolding q_def by auto

lemma p1: "int p > 1"
using nontriv [where ?'a = 'p] p by simp
lemma q1: "int q > 1"
using nontriv [where ?'a = 'q] q by simp
lemma q0: "int q > 0"
using q1 by auto

lemma pq2[simp]: "CARD('pq) = p * q" using pq by simp

lemma qq_eq_0[simp]: "(of_nat CARD('q) * of_nat CARD('q) :: 'pq mod_ring) = 0"
proof-
have "(of_nat (q * q) :: 'pq mod_ring) = 0" by (rule of_nat_zero, auto simp: p_dvd_q)
then show ?thesis by auto
qed

lemma of_nat_q[simp]: "of_nat q :: 'q mod_ring ≡ 0" by (fold of_nat_card_eq_0, auto)

lemma rebase_rebase[simp]: "(@(@(x::'pq mod_ring) :: 'q mod_ring) :: 'p mod_ring) = @x"
using p_dvd_q by (transfer) (simp add: mod_mod_cancel)

lemma rebase_rebase_poly[simp]: "(#(#(f::'pq mod_ring poly) :: 'q mod_ring poly) :: 'p mod_ring poly) = #f"
by (induct f, auto)

end

definition dupe_monic 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:
fixes D :: "'a :: prime_card mod_ring poly"
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"
"coprime D H ⟹ A' * D + B' * H = U ⟹ B' = 0 ∨ degree B' < degree D ⟹ A' = A ∧ B' = B"
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 = (S * U + H * q) * D + (T * U - D * q) * H" unfolding A B r by simp
also have "... = (D * S + H * T) * U" by (simp add: field_simps)
also have "D * S + H * T = 1" using 1 by simp
finally show eq: "A * D + B * H = U" by simp
show degB: "B = 0 ∨ degree B < degree D" using deg unfolding B by (cases "r = 0", auto)
assume another: "A' * D + B' * H = U" and degB': "B' = 0 ∨ degree B' < degree D"
and cop: "coprime D H"
from degB have degB: "B = 0 ∨ degree B < degree D" by auto
from degB' have degB': "B' = 0 ∨ degree B' < degree D" by auto
from mon have D0: "D ≠ 0" by auto
from another eq have "A' * D + B' * H = A * D + B * H" by simp
from uniqueness_poly_equality[OF cop degB' degB D0 this]
show "A' = A ∧ B' = B" by auto
qed

locale Knuth_ex_4_6_2_22_main = Knuth_ex_4_6_2_22_base p_ty q_ty pq_ty
for p_ty :: "'p::nontriv itself"
and q_ty :: "'q::nontriv itself"
and pq_ty :: "'pq::nontriv itself" +
fixes a b :: "'p mod_ring poly" and u :: "'pq mod_ring poly" and v w :: "'q mod_ring poly"
assumes uvw: "(#u :: 'q mod_ring poly) = v * w"
and degu: "degree u = degree v + degree w" (* not in Knuth's book *)
and avbw: "(a * #v + b * #w :: 'p mod_ring poly) = 1"
and monic_v: "monic v" (* stronger than Knuth's *)
(* not needed!
and aw: "degree a < degree w" *)
and bv: "degree b < degree v"
begin

lemma deg_v: "degree (#v :: 'p mod_ring poly) = degree v"
using monic_v by (simp add: of_int_hom.monic_degree_map_poly_hom)

lemma u0: "u ≠ 0" using degu bv by auto

lemma ex_f: "∃f :: 'p mod_ring poly. u = #v * #w + smult (of_nat q) (#f)"
proof-
from uvw have "(#(u - #v * #w) :: 'q mod_ring poly) = 0" by (auto simp:hom_distribs)
from rebase_pq_to_q.rebase_poly_eq_0_imp_ex_smult[OF this]
obtain f :: "'p mod_ring poly" where "u - #v * #w = smult (of_nat q) (#f)" by force
then have "u = #v * #w + smult (of_nat q) (#f)" by (metis add_diff_cancel_left' add_diff_eq)
then show ?thesis by (intro exI[of _ f], auto)
qed

definition "f :: 'p mod_ring poly ≡ SOME f. u = #v * #w + smult (of_nat q) (#f)"

lemma u: "u = #v * #w + smult (of_nat q) (#f)"
using ex_f[folded some_eq_ex] f_def by auto

lemma t_ex: "∃t :: 'p mod_ring poly. degree (b * f - t * #v) < degree v"
proof-
define v' where "v' ≡ #v :: 'p mod_ring poly"
from monic_v
then have 4: "v' ≠ 0" by auto
obtain t rem :: "'p mod_ring poly"
where "pseudo_divmod (b * f) v' = (t,rem)" by force
from pseudo_divmod[OF 4 this, folded, unfolded 1]
have "b * f = v' * t + rem" and deg: "rem = 0 ∨ degree rem < degree v'" by auto
then have "rem = b * f - t * v'" by(auto simp: ac_simps)
also have "... = b * f - #(#t :: 'p mod_ring poly) * v'" (is "_ = _ - ?t * v'") by simp
also have "... = b * f - ?t * #v"
by (unfold v'_def, rule)
finally have "degree rem = degree ..." by auto
with deg bv have "degree (b * f - ?t * #v :: 'p mod_ring poly) < degree v" by (auto simp: v'_def deg_v)
then show ?thesis by (rule exI)
qed

definition t where "t ≡ SOME t :: 'p mod_ring poly. degree (b * f - t * #v) < degree v"

definition "v' ≡ b * f - t * #v"
definition "w' ≡ a * f + t * #w"

lemma f: "w' * #v + v' * #w = f" (is "?l = _")
proof-
have "?l = f * (a * #v + b * #w :: 'p mod_ring poly)" by (simp add: v'_def w'_def ring_distribs ac_simps)
also
from avbw have "(#(a * #v + b * #w) :: 'p mod_ring poly) = 1" by auto
then have "(a * #v + b * #w :: 'p mod_ring poly) = 1" by auto
finally show ?thesis by auto
qed

lemma degv': "degree v' < degree v" by (unfold v'_def t_def, rule someI_ex, rule t_ex)

lemma degqf[simp]: "degree (smult (of_nat CARD('q)) (#f :: 'pq mod_ring poly)) = degree (#f :: 'pq mod_ring poly)"
proof (intro degree_smult_eqI)
assume "degree (#f :: 'pq mod_ring poly) ≠ 0"
then have f0: "degree f ≠ 0" by simp
moreover define l where "l ≡ lead_coeff f"
ultimately have l0: "l ≠ 0" by auto
then show "of_nat CARD('q) * lead_coeff (#f::'pq mod_ring poly) ≠ 0"
apply (transfer)
using q1 by (simp add: pq mod_mod_cancel)
qed

lemma degw': "degree w' ≤ degree w"
proof(rule ccontr)
let ?f = "#f :: 'pq mod_ring poly"
let ?qf = "smult (of_nat q) (#f) :: 'pq mod_ring poly"

have "degree (#w::'p mod_ring poly) ≤ degree w" by (rule degree_rebase_poly_le)
also assume "¬ degree w' ≤ degree w"
then have 1: "degree w < degree w'" by auto
finally have 2: "degree (#w :: 'p mod_ring poly) < degree w'" by auto
then have w'0: "w' ≠ 0" by auto

have 3: "degree (#v * w') = degree (#v :: 'p mod_ring poly) + degree w'"
using monic_v[unfolded] by (intro degree_monic_mult[OF _ w'0], auto simp: deg_v)

have "degree f ≤ degree u"
proof(rule ccontr)
assume "¬?thesis"
then have *: "degree u < degree f" by auto
with degu have 1: "degree v + degree w < degree f" by auto
define lcf where "lcf ≡ lead_coeff f"
with 1 have lcf0: "lcf ≠ 0" by (unfold, auto)
have "degree f = degree ?qf" by simp
also have "... = degree (#v * #w + ?qf)"
from 1 degree_mult_le[of "#v::'pq mod_ring poly" "#w"]
show "degree (#v * #w :: 'pq mod_ring poly) < degree ?qf" by simp
qed
also have "... < degree f" using * u by auto
finally show "False" by auto
qed
with degu have "degree f ≤ degree v + degree w" by auto
also note f[symmetric]
finally have "degree (w' * #v + v' * #w) ≤ degree v + degree w".
moreover have "degree (w' * #v + v' * #w) = degree (w' * #v)"
have "degree (v' * #w) ≤ degree v' + degree (#w :: 'p mod_ring poly)"
by(rule degree_mult_le)
also have "... < degree v + degree (#w :: 'p mod_ring poly)" using degv' by auto
also have "... < degree (#v :: 'p mod_ring poly) + degree w'" using 2 by (auto simp: deg_v)
also have "... = degree (#v * w')" using 3 by auto
finally show "degree (v' * #w) < degree (w' * #v)" by (auto simp: ac_simps)
qed
ultimately have "degree (w' * #v) ≤ degree v + degree w" by auto
moreover
from 3 have "degree (w' * #v) = degree w' + degree v" by (auto simp: ac_simps deg_v)
with 1 have "degree w + degree v < degree (w' * #v)" by auto
ultimately show False by auto
qed

abbreviation "qv' ≡ smult (of_nat q) (#v') :: 'pq mod_ring poly"
abbreviation "qw' ≡ smult (of_nat q) (#w') :: 'pq mod_ring poly"

abbreviation "V ≡ #v + qv'"
abbreviation "W ≡ #w + qw'"

lemma vV: "v = #V" by (auto simp: v'_def hom_distribs)

lemma wW: "w = #W" by (auto simp: w'_def hom_distribs)

lemma uVW: "u = V * W"

lemma degV: "degree V = degree v"
and degW: "degree W = degree w"
proof-
from p1 q1 have "int p < int p * int q" by auto
from less_trans[OF _ this]
have 1: "l < int p ⟹ l < int p * int q" for l by auto
have "degree qv' = degree (#v' :: 'pq mod_ring poly)"
proof (rule degree_smult_eqI, safe, unfold rebase_p_to_pq.degree_rebase_poly_eq)
define l where "l ≡ lead_coeff v'"
assume "degree v' > 0"
then have "lead_coeff v' ≠ 0" by auto
then have "(@l :: 'pq mod_ring) ≠ 0" by (simp add: l_def)
then have "(of_nat q * @l :: 'pq mod_ring) ≠ 0"
apply (transfer fixing:q_ty) using p_dvd_q p1 q1 1 by auto
moreover assume " of_nat q * coeff (#v') (degree v') = (0 :: 'pq mod_ring)"
ultimately show False by (auto simp: l_def)
qed
also from degv' have "... < degree (#v::'pq mod_ring poly)" by simp
finally have *: "degree qv' < degree (#v :: 'pq mod_ring poly)".
show **: "degree V = degree v" by (simp add: v'_def)

from * have "coeff qv' (degree v) = 0" by (intro coeff_eq_0, auto)
then show "lead_coeff V = @lead_coeff v" by (unfold **, auto simp: v'_def)

with u0 uVW have "degree (V * W) = degree V + degree W"
by (intro degree_mult_eq_left_unit, auto simp: monic_v)
from this[folded uVW, unfolded degu **] show "degree W = degree w" by auto
qed

end

locale Knuth_ex_4_6_2_22_prime = Knuth_ex_4_6_2_22_main ty_p ty_q ty_pq a b u v w
for ty_p :: "'p :: prime_card itself"
and ty_q :: "'q :: nontriv itself"
and ty_pq :: "'pq :: nontriv itself"
and a b u v w +
assumes coprime: "coprime (#v :: 'p mod_ring poly) (#w)" (* not in Knuth *)

begin

lemma coprime_preserves: "coprime (#V :: 'p mod_ring poly) (#W)"
apply (intro coprimeI,simp add: rebase_q_to_p.of_nat_CARD_eq_0[simplified] hom_distribs)
using coprime by (elim coprimeE, auto)

lemma pre_unique:
assumes f2: "w'' * #v + v'' * #w = f"
and degv'': "degree v'' < degree v"
shows "v'' = v' ∧ w'' = w'"
proof(intro conjI)
from f f2
have "w' * #v + v' * #w = w'' * #v + v'' * #w" by auto
also have "... - w'' * #v = v'' * #w" by auto
also have "... - v' * #w = (v''- v') * #w" by (auto simp: left_diff_distrib)
finally have *: "(w' - w'') * #v = (v''- v') * #w" by (auto simp: left_diff_distrib)
then have "#v dvd (v'' - v') * #w" by (auto intro: dvdI[of _ _ "w' - w''"] simp: ac_simps)
with coprime have "#v dvd v'' - v'"
moreover have "degree (v'' - v') < degree v" by (rule degree_diff_less[OF degv'' degv'])
ultimately have "v'' - v' = 0"
by (metis deg_v degree_0 gr_implies_not_zero poly_divides_conv0)
then show "v'' = v'" by auto
with * have "(w' - w'') * #v = 0" by auto
with bv have "w' - w'' = 0"
by (metis deg_v degree_0 gr_implies_not_zero mult_eq_0_iff)
then show "w'' = w'" by auto
qed

lemma unique:
assumes vV2: "v = #V2" and wW2: "w = #W2" and uVW2: "u = V2 * W2"
and degV2: "degree V2 = degree v" and degW2: "degree W2 = degree w"
shows "V2 = V" "W2 = W"
proof-
from vV2 have "(#(V2 - #v) :: 'q mod_ring poly) = 0" by (auto simp: hom_distribs)
from rebase_pq_to_q.rebase_poly_eq_0_imp_ex_smult[OF this]
obtain v'' :: "'p mod_ring poly"
where deg: "degree v'' ≤ degree (V2 - #v)"
and v'': "V2 - #v = smult (of_nat CARD('q)) (#v'')" by (elim exE conjE)
then have V2: "V2 = #v + ..." by (metis add_diff_cancel_left' diff_add_cancel)

from lc[unfolded degV2, unfolded V2]
have "of_nat q * (@coeff v'' (degree v) :: 'pq mod_ring) = of_nat q * 0" by auto
from this[unfolded q rebase_pq_to_p.rebase_mult_eq]
have "coeff v'' (degree v) = 0" by simp
moreover have "degree v'' ≤  degree v" using deg degV2
by (metis degree_diff_le le_antisym nat_le_linear rebase_q_to_pq.degree_rebase_poly_eq)
ultimately have degv'': "degree v'' < degree v"
using bv eq_zero_or_degree_less by fastforce

from wW2 have "(#(W2 - #w) :: 'q mod_ring poly) = 0" by (auto simp: hom_distribs)
from rebase_pq_to_q.rebase_poly_eq_0_imp_ex_smult[OF this] pq
obtain w'' :: "'p mod_ring poly" where w'': "W2 - #w = smult (of_nat q) (#w'')" by force
then have W2: "W2 = #w + ..." by (metis add_diff_cancel_left' diff_add_cancel)

have "u = #v * #w + smult (of_nat q) (#w'' * #v + #v'' * #w) + smult (of_nat (q * q)) (#v'' * #w'')"
also have "smult (of_nat (q * q)) (#v'' * #w'' :: 'pq mod_ring poly) = 0" by simp
finally have "u - #v * #w = smult (of_nat q) (#w'' * #v + #v'' * #w)" by auto
also have "u - #v * #w = smult (of_nat q) (#f)" by (subst u, simp)
finally have "w'' * #v + v'' * #w = f" by (simp add: hom_distribs)
from pre_unique[OF this degv'']
have pre: "v'' = v'" "w'' = w'" by auto
with V2 W2 show "V2 = V" "W2 = W" by auto
qed

end

definition
"hensel_1 (ty ::'p :: prime_card itself)
(u :: 'pq :: nontriv mod_ring poly) (v :: 'q :: nontriv mod_ring poly) (w :: 'q mod_ring poly) ≡
if v = 1 then (1,u) else
let (s, t) = bezout_coefficients (#v :: 'p mod_ring poly) (#w) in
let (a, b) = dupe_monic (#v::'p mod_ring poly) (#w) s t 1 in
(Knuth_ex_4_6_2_22_main.V TYPE('q) b u v w, Knuth_ex_4_6_2_22_main.W TYPE('q) a b u v w)"

lemma hensel_1:
fixes u :: "'pq :: nontriv mod_ring poly"
and v w :: "'q :: nontriv mod_ring poly"
assumes "CARD('pq) = CARD('p :: prime_card) * CARD('q)"
and "CARD('p) dvd CARD('q)"
and uvw: "#u = v * w"
and degu: "degree u = degree v + degree w"
and monic: "monic v"
and coprime: "coprime (#v :: 'p mod_ring poly) (#w)"
and out: "hensel_1 TYPE('p) u v w = (V',W')"
shows "u = V' * W' ∧ v = #V' ∧ w = #W' ∧ degree V' = degree v ∧ degree W' = degree w ∧
monic V' ∧ coprime (#V' :: 'p mod_ring poly) (#W')" (is ?main)
and "(∀V'' W''. u = V'' * W'' ⟶ v = #V'' ⟶ w = #W'' ⟶
degree V'' = degree v ⟶ degree W'' = degree w ⟶ lead_coeff V'' = @lead_coeff v ⟶
V'' = V' ∧ W'' = W')" (is "?unique")
proof-
from monic
have degv: "degree (#v :: 'p mod_ring poly) = degree v"
from monic
have monic2: "monic (#v :: 'p mod_ring poly)"
by (auto simp: degv)
obtain s t where bezout: "bezout_coefficients (#v :: 'p mod_ring poly) (#w) = (s, t)"
then have "s * #v + t * #w = gcd (#v :: 'p mod_ring poly) (#w)"
by (rule bezout_coefficients)
with coprime have vswt: "#v * s + #w * t = 1"
obtain a b where dupe: "dupe_monic (#v) (#w) s t 1 = (a, b)" by force
from dupe_monic(1,2)[OF vswt monic2, where U=1, unfolded this]
have avbw: "a * #v + b * #w = 1" and degb: "b = 0 ∨ degree b < degree (#v::'p mod_ring poly)" by auto
have "?main ∧ ?unique"
proof (cases "b = 0")
case b0: True
with avbw have "a * #v = 1" by auto
then have "degree (#v :: 'p mod_ring poly) = 0"
by (metis degree_1 degree_mult_eq_0 mult_zero_left one_neq_zero)
from this[unfolded degv] monic_degree_0[OF monic[unfolded]]
have 1: "v = 1" by auto
with b0 out uvw have 2: "V' = 1" "W' = u"
by (unfold split hensel_1_def Let_def dupe) auto
have 3: ?unique apply (simp add: 1 2) by (metis monic_degree_0 mult.left_neutral)
with uvw degu show ?thesis unfolding 1 2 by auto
next
case b0: False
with degb degv have degb: "degree b < degree v" by auto
then have v1: "v ≠ 1" by auto
interpret Knuth_ex_4_6_2_22_prime "TYPE('p)" "TYPE('q)" "TYPE('pq)" a b
by (unfold_locales; fact assms degb avbw)
show ?thesis
proof (intro conjI)
from out [unfolded hensel_1_def] v1
have 1 [simp]: "V' = V" "W' = W" by (auto simp: bezout dupe)
from uVW show "u = V' * W'" by auto
from degV show [simp]: "degree V' = degree v" by simp
from degW show [simp]: "degree W' = degree w" by simp