Theory Finite_Fields.Finite_Fields_Poly_Ring_Code

section ‹Executable Polynomial Rings›

theory Finite_Fields_Poly_Ring_Code
  imports
    Finite_Fields_Indexed_Algebra_Code
    "HOL-Algebra.Polynomials"
    Finite_Fields.Card_Irreducible_Polynomials_Aux
begin

fun o_normalize :: "('a,'b) idx_ring_scheme  'a list  'a list"
  where
    "o_normalize E [] = []"
  | "o_normalize E p = (if lead_coeff p  0CEthen p else o_normalize E (tl p))"

fun o_poly_add :: "('a,'b) idx_ring_scheme  'a list  'a list  'a list" where
  "o_poly_add E p1 p2 = (
    if length p1  length p2
      then o_normalize E (map2 (idx_plus E) p1 ((replicate (length p1 - length p2) 0CE) @ p2))
      else o_poly_add E p2 p1)"

fun o_poly_mult :: "('a,'b) idx_ring_scheme  'a list  'a list  'a list"
  where
    "o_poly_mult E [] p2 = []"
  | "o_poly_mult E p1 p2 =
       o_poly_add E ((map (idx_mult E (hd p1)) p2) @
      (replicate (degree p1) 0CE)) (o_poly_mult E (tl p1) p2)"

definition poly :: "('a,'b) idx_ring_scheme  'a list idx_ring"
  where "poly E = 
    idx_pred = (λx. (x = []  hd x  0CE)  list_all (idx_pred E) x),
    idx_uminus = (λx. map (idx_uminus E) x),
    idx_plus = o_poly_add E,
    idx_udivide = (λx. [idx_udivide E (hd x)]),
    idx_mult = o_poly_mult E,
    idx_zero = [],
    idx_one = [idx_one E] "

definition poly_var :: "('a,'b) idx_ring_scheme  'a list"  ("XCı")
  where "poly_var E = [idx_one E, idx_zero E]"

lemma poly_var: "poly_var R = Xring_of R⇙"
  unfolding var_def poly_var_def by (simp add:ring_of_def)

fun poly_eval :: "('a,'b) idx_ring_scheme  'a list  'a  'a"
  where "poly_eval R fs x = fold (λa b. b *CRx +CRa) fs 0CR⇙"



lemma ring_of_poly:
  assumes "ringC A"
  shows "ring_of (poly A) = poly_ring (ring_of A)"
proof (intro ring.equality)
  interpret ring "ring_of A" using assms unfolding ringC_def by auto

  have b: "𝟬ring_of A= 0CA⇙" unfolding ring_of_def by simp
  have c: "(⊗ring_of A) = (*CA)" unfolding ring_of_def by simp
  have d: "(⊕ring_of A) = (+CA)" unfolding ring_of_def by simp

  have " o_normalize A  x = normalize x" for x
    using b by (induction x) simp_all

  hence "o_poly_add A x y = poly_add x y" if "length y  length x" for x y
    using that by (subst o_poly_add.simps, subst poly_add.simps) (simp add: b d)
  hence a:"o_poly_add A x y = poly_add x y" for x y
    by (subst o_poly_add.simps, subst poly_add.simps) simp

  hence "x ring_of (poly A)y = x poly_ring (ring_of A)y" for x y
    by (simp add:univ_poly_def poly_def ring_of_def)

  thus "(⊕ring_of (poly A)) = (⊕poly_ring (ring_of A))" by (intro ext)

  show "carrier (ring_of (poly A)) = carrier (poly_ring (ring_of A))"
    by (auto simp add: ring_of_def poly_def univ_poly_def polynomial_def list_all_iff)

  have "o_poly_mult A x y = poly_mult x y" for x y
  proof (induction x)
    case Nil then show ?case by simp
  next
    case (Cons a x) then show ?case
      by (subst o_poly_mult.simps,subst poly_mult.simps)
        (simp add:a b c del:poly_add.simps o_poly_add.simps)
  qed
  hence "x ring_of (poly A)y = x poly_ring (ring_of A)y" for x y
    by (simp add:  univ_poly_def poly_def ring_of_def)
  thus "(⊗ring_of (poly A)) = (⊗poly_ring (ring_of A))" by (intro ext)

qed (simp_all add:ring_of_def poly_def univ_poly_def)

lemma poly_eval:
  assumes "ringC R"
  assumes fsc:"fs  carrier (ring_of (poly R))" and xc:"x  carrier (ring_of R)"
  shows "poly_eval R fs x = ring.eval (ring_of R) fs x"
proof -
  interpret ring "ring_of R" using assms unfolding ringC_def by auto

  have fs_carr:"fs  carrier (poly_ring (ring_of R))" using ring_of_poly[OF assms(1)] fsc by auto
  hence "set fs  carrier (ring_of R)" by (simp add: polynomial_incl univ_poly_carrier)
  thus ?thesis
  proof (induction rule:rev_induct)
    case Nil thus ?case by simp (simp add:ring_of_def)
  next
    case (snoc ft fh)
    have "poly_eval R (fh @ [ft]) x = poly_eval R fh x *CRx +CRft" by simp
    also have "... = eval fh x *CRx +CRft" using snoc by (subst snoc) auto
    also have "... = eval fh x ring_of Rx ring_of Rft " by (simp add:ring_of_def)
    also have " ... = eval (fh@[ft]) x" using snoc by (intro eval_append_aux[symmetric] xc) auto
    finally show ?case by auto
  qed
qed

lemma poly_domain:
  assumes "domainC A"
  shows "domainC (poly A)"
proof -
  interpret domain "ring_of A" using assms unfolding domainC_def by auto

  have a:"ring_of Ax = -CAx" if "x  carrier (ring_of A)" for x
    using that by (intro domain_cD[symmetric] assms)
  have "ringC A"
    using assms unfolding domainC_def cringC_def by auto
  hence b:"ring_of (poly A) = poly_ring (ring_of A)"
    by (subst ring_of_poly) auto

  have c:"domain (ring_of (poly A))"
    unfolding b by (rule univ_poly_is_domain[OF carrier_is_subring])

  interpret d: domain "poly_ring (ring_of A)"
    using c unfolding b by simp

  have "-Cpoly Ax = ring_of (poly A)x" if "x  carrier (ring_of (poly A))" for x
  proof -
    have "ring_of (poly A)x =  map (a_inv (ring_of A)) x"
      using that unfolding b by (subst univ_poly_a_inv_def'[OF carrier_is_subring]) auto
    also have "... = map (λr. -CAr) x"
      using that  unfolding b univ_poly_carrier[symmetric] polynomial_def
      by (intro map_cong refl a) auto
    also have "... = -Cpoly Ax"
      unfolding poly_def by simp
    finally show ?thesis by simp
  qed
  moreover have "x ¯Cpoly A= invring_of (poly A)x" if "x  Units (ring_of (poly A))" for x
  proof -
    have "x  {[k] |k. k  carrier (ring_of A) - {𝟬ring_of A}}"
      using that univ_poly_carrier_units_incl unfolding b by auto
    then obtain k where x_eq: "k  carrier (ring_of A) - {𝟬ring_of A}" "x = [k]" by auto
    have "invring_of (poly A)x  Units (poly_ring (ring_of A))"
      using that unfolding b by simp
    hence "invring_of (poly A)x  {[k] |k. k  carrier (ring_of A) - {𝟬ring_of A}}"
      using that univ_poly_carrier_units_incl unfolding b by auto
    then obtain v where x_inv_eq: "v carrier (ring_of A) - {𝟬ring_of A}"
      "invring_of (poly A)x = [v]" by auto

    have "poly_mult [k] [v] = [k] ring_of (poly A)[v]" unfolding b univ_poly_mult by simp
    also have "... = x ring_of (poly A)invring_of (poly A)x" using x_inv_eq x_eq by auto
    also have "... = 𝟭ring_of (poly A)⇙" using that unfolding b by simp
    also have "... = [𝟭ring_of A]" unfolding b univ_poly_one by (simp add:ring_of_def)
    finally have "poly_mult [k] [v] = [𝟭ring_of A]" by simp
    hence "k ring_of Av ring_of A𝟬ring_of A=  𝟭ring_of A⇙"
      by (simp add:if_distribR if_distrib) (simp cong:if_cong, metis)
    hence e: "k ring_of Av = 𝟭ring_of A⇙" using x_eq(1) x_inv_eq(1) by simp
    hence f: "v ring_of Ak = 𝟭ring_of A⇙" using x_eq(1) x_inv_eq(1) m_comm by simp
    have g: "v = invring_of Ak"
      using e x_eq(1) x_inv_eq(1) by (intro comm_inv_char[symmetric]) auto
    hence h: "k  Units (ring_of A)" unfolding Units_def using e f x_eq(1) x_inv_eq(1) by blast

    have "x ¯Cpoly A= [k] ¯Cpoly A⇙" unfolding x_eq by simp
    also have "... = [k ¯CA]" unfolding poly_def by simp
    also have "... = [v]"
      unfolding g by (intro domain_cD[OF assms(1)] arg_cong2[where f="(#)"] h refl)
    also have "... = invring_of (poly A)x" unfolding x_inv_eq by simp
    finally show ?thesis by simp
  qed
  ultimately show ?thesis using c by (intro domain_cI)
qed

function long_divisionC :: "('a,'b) idx_ring_scheme  'a list  'a list  'a list × 'a list"
  where "long_divisionC F f g = (
    if (length g = 0  length f < length g)
      then ([], f)
      else (
        let k = length f - length g;
            α = -CF(hd f *CF(hd g) ¯CF);
            h = [α] *Cpoly FXCF^Cpoly Fk;
            f' = f +Cpoly F(h *Cpoly Fg);
            f'' = take (length f - 1) f'
        in apfst (λx. x +Cpoly F-Cpoly Fh) (long_divisionC F f'' g)))"
  by pat_completeness auto

lemma pmod_termination_helper:
  "g  []  ¬length f < length g  min x (length f - 1) < length f"
  by (metis diff_less length_greater_0_conv list.size(3) min.strict_coboundedI2 zero_less_one)

termination by (relation "measure (λ(_, f, _). length f)") (use pmod_termination_helper in auto)

declare long_divisionC.simps[simp del]

lemma long_division_c_length:
  assumes "length g > 0"
  shows "length (snd (long_divisionC R f g)) < length g"
proof (induction "length f" arbitrary:f rule:nat_less_induct)
  case 1
  have 0:"length (snd (long_divisionC R x g)) < length g"
    if "length x < length f" for x using 1 that by blast

  show "length (snd (long_divisionC R f g)) < length g"
  proof (cases "length f < length g")
    case True then show ?thesis by (subst long_divisionC.simps) simp
  next
    case False
    hence "length f > 0" using assms by auto
    thus ?thesis using assms by (subst long_divisionC.simps)
       (auto intro!:0 simp: min.commute min.strict_coboundedI1 Let_def)
  qed
qed


context field
begin

interpretation r:polynomial_ring R "(carrier R)"
    unfolding polynomial_ring_def polynomial_ring_axioms_def
    using carrier_is_subfield field_axioms by force

lemma poly_length_from_coeff:
  assumes "p  carrier (poly_ring R)"
  assumes "i. i  k  coeff p i = 𝟬"
  shows "length p  k"
proof (rule ccontr)
  assume a:"¬length p  k"
  hence p_nz: "p  []" by auto
  have "k < length p" using a by simp
  hence "k  length p - 1" by simp
  hence "𝟬 = coeff p (degree p)" by (intro assms(2)[symmetric])
  also have "... = lead_coeff p" by (intro lead_coeff_simp[OF p_nz])
  finally have "𝟬 = lead_coeff p" by simp
  thus "False"
    using p_nz assms(1) unfolding univ_poly_def polynomial_def by simp
qed

lemma  poly_add_cancel_len:
  assumes "f  carrier (poly_ring R) - {𝟬poly_ring R}"
  assumes "g  carrier (poly_ring R) - {𝟬poly_ring R}"
  assumes "hd f =  hd g" "degree f = degree g"
  shows "length (f poly_ring Rg) < length f"
proof -
  have f_ne: "f  []" using assms(1) unfolding univ_poly_zero by simp
  have g_ne: "g  []" using assms(2) unfolding univ_poly_zero by simp

  have "coeff f i = coeff g i" if "i  degree f" for i
  proof (cases "i = degree f")
    case True
    have "coeff f i = hd f" unfolding True by (subst lead_coeff_simp[OF f_ne]) simp
    also have "... = hd g" using assms(3) by simp
    also have "... = coeff g i" unfolding True assms(4) by (subst lead_coeff_simp[OF g_ne]) simp
    finally show ?thesis by simp
  next
    case False
    hence "i > degree f" "i > degree g" using  assms(4) that by auto
    thus "coeff f i =  coeff g i" using coeff_degree by simp
  qed
  hence "coeff (f poly_ring Rg) i = 𝟬" if "i  degree f" for i
    using assms(1,2) that by (subst r.coeff_add) (auto intro:l_neg simp:  r.coeff_range)

  hence "length (f poly_ring Rg)  length f - 1"
    using assms(1,2) by (intro poly_length_from_coeff) auto
  also have "... < length f" using f_ne by simp
  finally show ?thesis by simp
qed

lemma pmod_mult_left:
  assumes "f  carrier (poly_ring R)"
  assumes "g  carrier (poly_ring R)"
  assumes "h  carrier (poly_ring R)"
  shows "(f poly_ring Rg) pmod h = ((f pmod h) poly_ring Rg) pmod h" (is "?L = ?R")
proof -
  have "h pdivides (h poly_ring R(f pdiv h)) poly_ring Rg"
    using assms long_division_closed[OF carrier_is_subfield]
    by (simp add: dividesI' pdivides_def r.p.m_assoc)
  hence 0:"(h poly_ring R(f pdiv h)) poly_ring Rg pmod h = 𝟬poly_ring R⇙"
    using pmod_zero_iff_pdivides[OF carrier_is_subfield] assms
      long_division_closed[OF carrier_is_subfield] univ_poly_zero
    by (metis (no_types, opaque_lifting) r.p.m_closed)

  have "?L = (h poly_ring R(f pdiv h) poly_ring R(f pmod h)) poly_ring Rg pmod h"
    using assms by (intro arg_cong2[where f="(⊗poly_ring R)"] arg_cong2[where f="(pmod)"]
     pdiv_pmod[OF carrier_is_subfield]) auto
  also have "... = ((h poly_ring R(f pdiv h)) poly_ring Rg poly_ring R(f pmod h) poly_ring Rg) pmod h"
    using assms long_division_closed[OF carrier_is_subfield]
    by (intro r.p.l_distr arg_cong2[where f="(pmod)"]) auto
  also have "... = ((h poly_ring R(f pdiv h)) poly_ring Rg) pmod h poly_ring R((f pmod h) poly_ring Rg pmod h)"
    using assms long_division_closed[OF carrier_is_subfield]
    by (intro long_division_add[OF carrier_is_subfield]) auto
  also have "... = ?R"
    using assms long_division_closed[OF carrier_is_subfield] unfolding 0 by auto
  finally show ?thesis
    by simp
qed

lemma pmod_mult_right:
  assumes "f  carrier (poly_ring R)"
  assumes "g  carrier (poly_ring R)"
  assumes "h  carrier (poly_ring R)"
  shows "(f poly_ring Rg) pmod h = (f poly_ring R(g pmod h)) pmod h" (is "?L = ?R")
proof -
  have "?L = (g poly_ring Rf) pmod h" using assms by algebra
  also have "... = ((g pmod h) poly_ring Rf) pmod h" by (intro pmod_mult_left assms)
  also have "... = ?R" using assms long_division_closed[OF carrier_is_subfield] by algebra
  finally show ?thesis by simp
qed

lemma pmod_mult_both:
  assumes "f  carrier (poly_ring R)"
  assumes "g  carrier (poly_ring R)"
  assumes "h  carrier (poly_ring R)"
  shows "(f poly_ring Rg) pmod h = ((f pmod h) poly_ring R(g pmod h)) pmod h"
    (is "?L = ?R")
proof -
  have "(f poly_ring Rg) pmod h = ((f pmod h) poly_ring Rg) pmod h"
    by (intro pmod_mult_left assms)
  also have "... = ?R"
    using assms long_division_closed[OF carrier_is_subfield] by (intro pmod_mult_right) auto
  finally show ?thesis by simp
qed

lemma field_Unit_minus_closed:
  assumes "x  Units R"
  shows " x  Units R"
  using assms mult_of.Units_eq by auto

end

lemma long_division_c:
  assumes "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  assumes "g  carrier (poly_ring (ring_of R))"
  shows "long_divisionC R f g = (ring.pdiv (ring_of R) f g, ring.pmod (ring_of R) f g)"
proof -
  let ?P = "poly_ring (ring_of R)"
  let ?result = "(λf r. f = snd r poly_ring (ring_of R)(fst r poly_ring (ring_of R)g))"

  define r where "r = long_divisionC R f g"

  interpret field "ring_of R" using assms(1) unfolding fieldC_def by auto
  interpret d_poly_ring: domain "poly_ring (ring_of R)"
    by (rule univ_poly_is_domain[OF carrier_is_subring])

  have ring_c: "ringC R" using assms(1) unfolding fieldC_def domainC_def cringC_def by auto
  have d_poly: "domainC (poly R)" using assms (1) unfolding fieldC_def by (intro poly_domain) auto

  have "r = long_divisionC R f g  ?result f r  {fst r, snd r}  carrier (poly_ring (ring_of R))"
    using assms(2)
  proof (induction "length f" arbitrary: f r rule:nat_less_induct)
    case 1

    have ind: "x = snd q ?Pfst q ?Pg" "{fst q, snd q}  carrier (poly_ring (ring_of R))"
      if "length x < length f " "q = long_divisionC R x g" "x  carrier (poly_ring (ring_of R)) "
      for x q using 1(1) that by auto

    show ?case
    proof (cases "length g = 0  length f < length g")
      case True
      hence "r = (𝟬poly_ring (ring_of R), f)"
        unfolding 1(2) univ_poly_zero by (subst long_divisionC.simps) simp
      then show ?thesis using assms(3) 1(3) by simp
    next
      case False
      hence "length g > 0" "length f  length g" by auto
      hence "f  []" "g  []" by auto
      hence f_carr: "f  carrier ?P - {𝟬?P}" and g_carr: "g  carrier ?P - {𝟬?P}"
         using 1(3) assms(3) univ_poly_zero by auto

      define k where "k = length f - length g"
      define α where "α = -CR(hd f *CR(hd g) ¯CR)"
      define h where "h = [α] *Cpoly RXCR^Cpoly Rk"
      define f' where "f' = f +Cpoly R(h *Cpoly Rg)"
      define f'' where "f'' = take (length f - 1) f'"
      obtain s t where st_def: "(s,t) = long_divisionC R f'' g" by (metis surj_pair)

      have "r = apfst (λx. x +Cpoly R-Cpoly Rh) (long_divisionC R f'' g)"
        using False unfolding 1(2)
        by (subst long_divisionC.simps) (simp add:Let_def f''_def f'_def h_def α_def k_def)

      hence r_def: "r = (s +Cpoly R-Cpoly Rh, t)"
        unfolding st_def[symmetric] by simp

      have "monic_poly (ring_of R) (Xring_of R[^]poly_ring (ring_of R)k)"
        by (intro monic_poly_pow monic_poly_var)
      hence [simp]: "lead_coeff (Xring_of R[^]poly_ring (ring_of R)k) = 𝟭ring_of R⇙"
        unfolding monic_poly_def by simp

      have hd_f_unit: "hd f  Units (ring_of R)" and hd_g_unit: "hd g  Units (ring_of R)"
        using f_carr g_carr lead_coeff_carr field_Units by auto
      hence hd_f_carr: "hd f  carrier (ring_of R)" and hd_g_carr: "hd g  carrier (ring_of R)"
        by auto

      have k_def': "k = degree f - degree g" using False unfolding k_def by auto
      have α_def': "α = ring_of R(hd f ring_of Rinvring_of Rhd g)"
        unfolding α_def using hd_g_unit hd_f_carr field_cD[OF assms(1)] by simp

      have α_unit: "α  Units (ring_of R)" unfolding α_def' using hd_f_unit hd_g_unit
        by (intro field_Unit_minus_closed) simp
      hence α_carr: "α  carrier (ring_of R) - {𝟬ring_of R}" unfolding field_Units by simp
      hence α_poly_carr: "[α]  carrier (poly_ring (ring_of R)) - {𝟬poly_ring (ring_of R)}"
        by (simp add: univ_poly_carrier[symmetric] univ_poly_zero polynomial_def)

      have h_def': "h = [α] ?PXring_of R[^]?Pk"
        unfolding h_def poly_var domain_cD[OF d_poly] by (simp add:ring_of_poly[OF ring_c])
      have f'_def': "f' = f ?P(h ?Pg)"
        unfolding f'_def domain_cD[OF d_poly] by (simp add:ring_of_poly[OF ring_c])

      have h_carr: "h  carrier (poly_ring (ring_of R)) - {𝟬poly_ring (ring_of R)}"
        using d_poly_ring.mult_of.m_closed α_poly_carr var_pow_carr[OF carrier_is_subring]
        unfolding h_def' by auto

      have "degree f = k + degree g" using False unfolding k_def by linarith
      also have "... = degree [α] + degree (Xring_of R[^]?Pk) + degree g"
        unfolding var_pow_degree[OF carrier_is_subring] by simp
      also have "... = degree h + degree g" unfolding h_def'
        by (intro arg_cong2[where f="(+)"] degree_mult[symmetric]
            carrier_is_subring α_poly_carr var_pow_carr refl)
      also have "... = degree (h poly_ring (ring_of R)g)"
        by (intro degree_mult[symmetric] carrier_is_subring h_carr g_carr)
      finally have deg_f: "degree f = degree (h poly_ring (ring_of R)g)" by simp

      have f'_carr: "f'  carrier (poly_ring (ring_of R))"
        using f_carr h_carr g_carr unfolding f'_def' by auto

      have "hd f = ring_of R(α ring_of Rlead_coeff g)"
        using hd_g_unit hd_f_carr hd_g_carr α_unit α_carr unfolding α_def'
        by (simp add: m_assoc l_minus)
      also have "... = ring_of R(hd h ring_of Rhd g)"
        using hd_f_carr α_carr α_poly_carr var_pow_carr[OF carrier_is_subring] unfolding h_def'
        by (subst lead_coeff_mult) (simp_all add:algebra_simps)
      also have "... = ring_of Rhd (h poly_ring (ring_of R)g)"
        using h_carr g_carr by (subst lead_coeff_mult) auto
      finally have "hd f = ring_of Rhd (h poly_ring (ring_of R)g)"
        by simp
      hence len_f': "length f' < length f" using deg_f h_carr g_carr d_poly_ring.integral
        unfolding f'_def' by (intro poly_add_cancel_len f_carr) auto
      hence f''_def': "f'' = f'" unfolding f''_def by simp

      have "{fst (s,t),snd (s,t)}  carrier (poly_ring (ring_of R))"
        using len_f' f''_def' f'_carr by (intro ind(2)[where x="f''"] st_def) auto
      hence s_carr: "s  carrier ?P" and t_carr: "t  carrier ?P" by auto

      have r_def': "r = (s poly_ring (ring_of R)h, t)"
        using h_carr domain_cD[OF d_poly] unfolding r_def a_minus_def
        using ring_of_poly[OF ring_c,symmetric] by simp

      have r_carr: "{fst r, snd r}  carrier (poly_ring (ring_of R))"
        using s_carr t_carr h_carr unfolding r_def' by auto
      have "f = f'' ?Ph ?Pg"
        using h_carr g_carr f_carr unfolding f''_def' f'_def' by simp algebra
      also have "... = (snd (s,t) ?Pfst (s,t) ?Pg) ?Ph ?Pg"
        using f'_carr f''_def' len_f'
        by (intro arg_cong2[where f="λx y. x ?Py"] ind(1) st_def) auto
      also have "... = t ?P(s ?Ph) ?Pg"
        using s_carr t_carr h_carr g_carr by simp algebra
      also have "... = snd r poly_ring (ring_of R)fst r poly_ring (ring_of R)g"
        unfolding r_def' by simp
      finally have "f = snd r poly_ring (ring_of R)fst r poly_ring (ring_of R)g" by simp
      thus ?thesis using r_carr by auto
    qed
  qed
  hence result: "?result f r" "{fst r, snd r}  carrier (poly_ring (ring_of R))"
    using r_def by auto
  show ?thesis
  proof (cases "g = []")
    case True then show ?thesis by (simp add:long_divisionC.simps pmod_def pdiv_def)
  next
    case False
    hence "snd r = []  degree (snd r) < degree g"
      using long_division_c_length unfolding r_def
      by (metis One_nat_def Suc_pred length_greater_0_conv not_less_eq)
    moreover have "f = g ?P(fst r) poly_ring (ring_of R)(snd r)"
      using result(1,2) assms(2,3) by simp algebra
    ultimately have "long_divides f g (fst r, snd r)"
      using result(2) unfolding long_divides_def by (auto simp:mem_Times_iff)
    hence "(fst r, snd r) = (pdiv f g, pmod f g)"
      by (intro long_divisionI[OF carrier_is_subfield] False assms)
    then show ?thesis unfolding r_def by simp
  qed
qed

definition pdivC :: "('a,'b) idx_ring_scheme  'a list  'a list  'a list" where
  "pdivC R f g = fst (long_divisionC R f g)"

lemma pdiv_c:
  assumes "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  assumes "g  carrier (poly_ring (ring_of R))"
  shows "pdivC R f g = ring.pdiv (ring_of R) f g"
  unfolding pdivC_def long_division_c[OF assms] by simp

definition pmodC :: "('a,'b) idx_ring_scheme  'a list  'a list  'a list" where
  "pmodC R f g = snd (long_divisionC R f g)"

lemma pmod_c:
  assumes "fieldC R"
  assumes "f  carrier (poly_ring (ring_of R))"
  assumes "g  carrier (poly_ring (ring_of R))"
  shows "pmodC R f g = ring.pmod (ring_of R) f g"
  unfolding pmodC_def long_division_c[OF assms] by simp

function ext_euclidean ::
  "('a,'b) idx_ring_scheme  'a list  'a list  ('a list × 'a list) × 'a list"
  where "ext_euclidean F f g = (
    if f = []  g = [] then
      ((1Cpoly F, 1Cpoly F),f +Cpoly Fg)
    else (
      let (p,q) = long_divisionC F f g;
          ((u,v),r) = ext_euclidean F g q
       in ((v,u +Cpoly F(-Cpoly F(p *Cpoly Fv))),r)))"
  by pat_completeness auto

termination
  apply (relation "measure (λ(_, _, f). length f)")
  subgoal by simp
  by (metis case_prod_conv in_measure length_greater_0_conv long_division_c_length prod.sel(2))

(* TODO MOVE *)
lemma (in domain) pdivides_self:
  assumes "x  carrier (poly_ring R)"
  shows "x pdivides x"
proof -
  interpret d:domain "poly_ring R" by (rule univ_poly_is_domain[OF carrier_is_subring])
  show ?thesis
    using assms unfolding pdivides_def
    by (intro dividesI[where c="𝟭poly_ring R⇙"]) simp_all
qed

declare ext_euclidean.simps[simp del]

lemma ext_euclidean:
  assumes "fieldC R"
  defines "P  poly_ring (ring_of R)"
  assumes "f  carrier (poly_ring (ring_of R))"
  assumes "g  carrier (poly_ring (ring_of R))"
  defines "r  ext_euclidean R f g"
  shows "snd r = f P(fst (fst r)) Pg P(snd (fst r))" (is "?T1")
    and "snd r pdividesring_of Rf" (is "?T2") "snd r pdividesring_of Rg" (is "?T3")
    and "{snd r, fst (fst r), snd (fst r)}  carrier P" (is "?T4")
    and "snd r = []  f = []  g = []" (is "?T5")
proof -
  let ?P= "poly_ring (ring_of R)"

  interpret field "ring_of R" using assms(1) unfolding fieldC_def by auto
  interpret d_poly_ring: domain "poly_ring (ring_of R)"
    by (rule univ_poly_is_domain[OF carrier_is_subring])

  have ring_c: "ringC R" using assms(1) unfolding fieldC_def domainC_def cringC_def by auto
  have d_poly: "domainC (poly R)" using assms (1) unfolding fieldC_def by (intro poly_domain) auto

  have pdiv_zero: "x pdividesring_of R𝟬?P⇙" if "x  carrier ?P" for x
    using that unfolding univ_poly_zero by (intro pdivides_zero[OF carrier_is_subring])

  have "snd r = f ?P(fst (fst r)) ?Pg ?P(snd (fst r)) 
    snd r pdividesring_of Rf  snd r pdividesring_of Rg 
    {snd r, fst (fst r), snd (fst r)}  carrier ?P 
    (snd r = []  f = []  g = [])"
    if "r = ext_euclidean R f g" "{f,g}  carrier ?P"
    using that
  proof (induction "length g" arbitrary: f g r rule:nat_less_induct)
    case 1
    have ind:
      "snd s = x ?Pfst (fst s) ?Py ?Psnd (fst s)"
      "snd s pdividesring_of Rx" "snd s pdividesring_of Ry"
      "{snd s, fst (fst s), snd (fst s)}  carrier ?P"
      "(snd s = []  x = []  y = [])"
      if "length y < length g" "s = ext_euclidean R x y" "{x, y}  carrier ?P"
      for x y s using that 1(1) by metis+
    show ?case
    proof (cases "f = []  g = []")
      case True
      hence r_def: "r = ((𝟭?P, 𝟭?P), f ?Pg)" unfolding 1(2)
        by (simp add:ext_euclidean.simps domain_cD[OF d_poly] ring_of_poly[OF ring_c])

      consider "f = 𝟬?P⇙" |  "g = 𝟬?P⇙"
        using True unfolding univ_poly_zero by auto
      hence "snd r pdividesring_of Rf  snd r pdividesring_of Rg"
        using 1(3) pdiv_zero pdivides_self unfolding r_def by cases auto
      moreover have "snd r = f ?Pfst (fst r) ?Pg ?Psnd (fst r)"
        using 1(3) unfolding r_def by simp
      moreover have "{snd r, fst (fst r), snd (fst r)}  carrier ?P"
        using 1(3) unfolding r_def by auto
      moreover have "snd r = []  f = []  g = []"
        using 1(3) True unfolding r_def by (auto simp:univ_poly_zero)
      ultimately show ?thesis by (intro conjI) metis+
    next
      case False
      obtain p q where pq_def: "(p,q) = long_divisionC R f g"
        by (metis surj_pair)
      obtain u v s where uvs_def: "((u,v),s) = ext_euclidean R g q"
        by (metis surj_pair)

      have "(p,q) = (pdiv f g, pmod f g)"
        using 1(3) unfolding pq_def by (intro long_division_c[OF assms(1)]) auto
      hence p_def: "p = pdiv f g" and q_def: "q = pmod f g" by auto
      have p_carr: "p  carrier ?P" and q_carr: "q  carrier ?P"
        using 1(3) long_division_closed[OF carrier_is_subfield] unfolding p_def q_def by auto

      have "length g > 0" using False by auto
      hence len_q: "length q < length g" using long_division_c_length pq_def by (metis snd_conv)
      have s_eq: "s = g ?Pu ?Pq ?Pv"
        and s_div_g: "s pdividesring_of Rg"
        and s_div_q: "s pdividesring_of Rq"
        and suv_carr: "{s,u,v}  carrier ?P"
        and s_zero_iff: "s = []  g = []  q = []"
        using ind[OF len_q uvs_def _] q_carr 1(3) by auto

      have "r = ((v,u +Cpoly R(-Cpoly R(p *Cpoly Rv))),s)" unfolding 1(2) using False
        by (subst ext_euclidean.simps) (simp add: pq_def[symmetric] uvs_def[symmetric])
      also have "... = ((v, u ?P(p ?Pv)), s)" using p_carr suv_carr domain_cD[OF d_poly]
        unfolding a_minus_def ring_of_poly[OF ring_c] by (intro arg_cong2[where f="Pair"] refl) simp
      finally have r_def: "r = ((v, u ?P(p ?Pv)), s)" by simp

      have "snd r = g ?Pu ?Pq ?Pv" unfolding r_def s_eq by simp
      also have "... = g ?Pu ?P(f ?Pg ?Pp) ?Pv"
        using 1(3) p_carr q_carr suv_carr
        by (subst pdiv_pmod[OF carrier_is_subfield, of "f" "g"])
         (simp_all add:p_def[symmetric] q_def[symmetric], algebra)
      also have "... = f ?Pv ?Pg ?P(u ?P((p ?Pv)))"
        using 1(3) p_carr q_carr suv_carr  by simp algebra
      finally have r1: "snd r = f ?Pfst (fst r) ?Pg ?Psnd (fst r)"
        unfolding r_def by simp
      have "pmod f s = pmod (g ?Pp ?Pq) s" using 1(3)
        by (subst pdiv_pmod[OF carrier_is_subfield, of "f" "g"])
          (simp_all add:p_def[symmetric] q_def[symmetric])
      also have "... = pmod (g ?Pp) s ?Ppmod q s"
        using 1(3) p_carr q_carr suv_carr
        by (subst long_division_add[OF carrier_is_subfield]) simp_all
      also have "... = pmod (pmod g s ?Pp) s ?P[]"
        using 1(3) p_carr q_carr suv_carr s_div_q
        by (intro arg_cong2[where f="(⊕?P)"] pmod_mult_left)
          (simp_all add: pmod_zero_iff_pdivides[OF carrier_is_subfield])
      also have "... = pmod (𝟬?P?Pp) s ?P𝟬?P⇙" unfolding univ_poly_zero
        using 1(3) p_carr q_carr suv_carr s_div_g by (intro arg_cong2[where f="(⊕?P)"]
            arg_cong2[where f="(⊗?P)"] arg_cong2[where f="pmod"])
          (simp_all add: pmod_zero_iff_pdivides[OF carrier_is_subfield])
      also have "... = pmod 𝟬?Ps"
        using p_carr suv_carr long_division_closed[OF carrier_is_subfield] by simp
      also have "... = []" unfolding univ_poly_zero
        using suv_carr long_division_zero(2)[OF carrier_is_subfield] by simp
      finally have "pmod f s = []" by simp
      hence r2: "snd r pdividesring_of Rf" using suv_carr 1(3)  unfolding r_def
        by (subst pmod_zero_iff_pdivides[OF carrier_is_subfield,symmetric]) simp_all
      have r3: "snd r pdividesring_of Rg" unfolding r_def using s_div_g by auto
      have r4: "{snd r, fst (fst r), snd (fst r)}  carrier ?P"
        using suv_carr p_carr unfolding r_def by simp_all
      have r5: "f = []  g = []" if "snd r = []"
      proof -
        have r5_a: "g = []  q = []" using that s_zero_iff unfolding r_def by simp
        hence "pmod f [] = []" unfolding q_def by auto
        hence "f = []" using pmod_def by simp
        thus ?thesis using r5_a by auto
      qed

      show ?thesis using r1 r2 r3 r4 r5  by (intro conjI) metis+
    qed
  qed
  thus ?T1 ?T2 ?T3 ?T4 ?T5 using assms by auto
qed

end