Theory Hensel_Lifting_Type_Based

(*
    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
*)
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 
      le_degree le_zero_eq leading_coeff_0_iff)

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:
  assumes lc: "lead_coeff p * lead_coeff q  0"
  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)
  moreover assume "lead_coeff p * lead_coeff q = 0"
    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)"
  by (simp add: monic_degree_map_poly_hom)

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"
  by (simp add: of_int_of_int_mod_ring)

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)

lemma lead_coeff_rebase_poly[simp]:
  "lead_coeff (#(p::'a mod_ring poly) :: 'b mod_ring poly) = @lead_coeff p"
  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"
    by (simp add: of_nat_mod [symmetric])
  then have "x mod CARD('b) = 1"
    by (metis dvd mod_mod_cancel one_mod_card)
  then have "int x mod CARD('b) = 1"
    by (simp add: of_nat_mod [symmetric])
  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
      by (simp add: zero_le_mult_iff)
    ultimately have "i0. 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
  have 1: "lead_coeff v' = 1" by (simp add: v'_def deg_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 (unfold rebase_p_to_pq.lead_coeff_rebase_poly, fold l_def)
  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)"
    proof(rule sym, rule degree_add_eq_right)
      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)"
  proof(rule degree_add_eq_left)
    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"
  by (subst u, fold f, simp add: ring_distribs add.left_cancel smult_add_right[symmetric] hom_distribs)

lemma degV: "degree V = degree v"
  and lcV: "lead_coeff V = @lead_coeff 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)".
  from degree_add_eq_left[OF *]
  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'"
    by (simp add: coprime_dvd_mult_left_iff)
  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"
      and lc: "lead_coeff V2 = @lead_coeff v"
  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'')"
    by(simp add: uVW2 V2 W2 ring_distribs smult_add_right ac_simps)
  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"
    by (simp add: of_int_hom.monic_degree_map_poly_hom)
  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)"
    by (auto simp add: prod_eq_iff)
  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"
    by (simp add: ac_simps)
  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
      from lcV have "lead_coeff V' = @lead_coeff v" by simp
      with monic_v show "monic V'" by (simp add:)
      from vV show "v = #V'" by simp
      from wW show "w = #W'" by simp
      from coprime_preserves show "coprime (#V' :: 'p mod_ring poly) (#W')" by simp
      show 9: ?unique by (unfold 1, intro allI conjI impI; rule unique)
    qed
  qed
  then show ?main ?unique by (fact conjunct1, fact conjunct2)
qed

end