Theory Finite_Fields_Poly_Factor_Ring_Code

section ‹Executable Polynomial Factor Rings›

theory Finite_Fields_Poly_Factor_Ring_Code
  imports
    Finite_Fields_Poly_Ring_Code
    Rabin_Irreducibility_Test_Code
    Finite_Fields_More_Bijections
begin

text ‹Enumeration of the polynomials with a given degree:›

definition poly_enum :: "('a,'b) idx_ring_enum_scheme  nat  nat  'a list"
  where "poly_enum R l n =
    dropWhile ((=) 0CR) (map (λp. idx_enum R (nth_digit n (l-1-p) (idx_size R))) [0..<l])"

lemma replicate_drop_while_cancel:
  assumes "k = length (takeWhile ((=) x) y)"
  shows  "replicate k x @ dropWhile ((=) x) y = y" (is "?L = ?R")
proof -
  have "replicate k x = takeWhile ((=) x) y"
    using assms by (metis (full_types) replicate_length_same set_takeWhileD)
  thus ?thesis by simp
qed

lemma arg_cong3:
  assumes "x = u" "y = v" "z = w"
  shows "f x y z = f u v w"
  using assms by simp

lemma list_all_dropwhile: "list_all p xs  list_all p (dropWhile q xs)"
  by (induction xs) auto

lemma bij_betw_poly_enum:
  assumes "enumC R" "ringC R"
  shows "bij_betw (poly_enum R l) {..<idx_size R^l}
  {xs. xs  carrier (poly_ring (ring_of R))  length xs  l}"
proof -
  let ?b = "idx_size R"
  let ?S0 = "{..<l} E {..<order (ring_of R)}"
  let ?S1 = "{..<l} E {x. idx_pred R x}"
  let ?S2 = "{xs. list_all (idx_pred R) xs  length xs = l}"
  let ?S3 = "{xs. (xs = []  hd xs  0CR)  list_all (idx_pred R) xs  length xs  l}"
  let ?S4 = "{xs. xs  carrier (poly_ring (ring_of R))  length xs  l}"

  interpret ring "ring_of R" using assms(2) unfolding ringC_def by simp

  have "0 < order (ring_of R)" using enum_cD(1)[OF assms(1)] order_gt_0_iff_finite by metis
  also have "... = ?b" using enum_cD[OF assms(1)] by auto
  finally have b_gt_0: "?b > 0" by simp

  note bij0 = lift_bij_betw[OF enum_cD(3)[OF assms(1)], where I="{..<l}"]
  note bij1 = lists_bij[where d="l" and S="{x. idx_pred R x}"]

  have "bij_betw (dropWhile ((=) 0CR)) ?S2 ?S3"
  proof (rule bij_betwI[where g="λxs. replicate (l - length xs) 0CR@ xs"])
    have "dropWhile ((=) 0CR) xs  ?S3" if "xs  ?S2" for xs
    proof -
      have "dropWhile ((=) 0CR) xs = []  hd (dropWhile ((=) 0CR) xs)  0CR⇙"
        using hd_dropWhile by (metis (full_types))
      moreover have "length (dropWhile ((=) 0CR) xs)  l"
        by (metis (mono_tags, lifting) mem_Collect_eq length_dropWhile_le that)
      ultimately show ?thesis using that by (auto simp:list_all_dropwhile)
    qed
    thus "dropWhile ((=) 0CR)  ?S2  ?S3"  by auto
    have "replicate (l - length xs) 0CR@ xs  ?S2" if "xs  ?S3" for xs
    proof -
      have "idx_pred R 0CR⇙" using add.one_closed by (simp add:ring_of_def)
      moreover have "length (replicate (l - length xs) 0CR@ xs) = l" using that by auto
      ultimately show ?thesis using that by (auto simp:list_all_iff)
    qed
    thus "(λxs. replicate (l - length xs) 0CR@ xs)  ?S3  ?S2" by auto

    show "replicate (l - length (dropWhile ((=) 0CR) x)) 0CR@ dropWhile ((=) 0CR) x = x"
      if "x  ?S2" for x
    proof -
      have "length (takeWhile ((=) 0CR) x) + length (dropWhile ((=) 0CR) x) = length x"
        unfolding length_append[symmetric] by simp
      thus ?thesis using that by (intro replicate_drop_while_cancel) auto
    qed
    show "dropWhile ((=) 0CR) (replicate (l - length y) 0CR@ y) = y"
      if "y  ?S3" for y
    proof -
      have "dropWhile ((=) 0CR) (replicate (l - length y) 0CR@ y) = dropWhile ((=) 0CR) y"
        by (intro dropWhile_append2) simp
      also have "... = y" using that by (intro iffD2[OF dropWhile_eq_self_iff]) auto
      finally show ?thesis by simp
    qed
  qed
  moreover have "?S3 = ?S4"
    unfolding ring_of_poly[OF assms(2),symmetric] by (simp add:ring_of_def poly_def)
  ultimately have bij2: "bij_betw (dropWhile ((=) 0CR)) ?S2 ?S4" by simp

  have bij3: "bij_betw (λx. l-1-x) {..<l}  {..<l}"
    by (intro bij_betwI[where g="λx. l-1-x"]) auto
  note bij4 = bij_betw_reindex[OF bij3, where S="{..<order (ring_of R)}"]
  have bij5: "bij_betw (λn. (λp{..<l}. nth_digit n p ?b)) {..<?b^l} ?S0"
    using nth_digit_bij[where n="l"] enum_cD[OF assms(1)] by simp
  have bij6: "bij_betw (λn. (λp{..<l}. nth_digit n (l-1-p) ?b)) {..<?b^l} ?S0"
    by (intro iffD2[OF arg_cong3[where f="bij_betw"] bij_betw_trans[OF bij5 bij4]]) force+

  have "carrier (ring_of R) = {x. idx_pred R x}" unfolding ring_of_def by auto
  hence bij7: "bij_betw (λn. (λp{..<l}. idx_enum R (nth_digit n (l-1-p) ?b))) {..<?b^l} ?S1"
    by (intro iffD2[OF arg_cong3[where f="bij_betw"] bij_betw_trans[OF bij6 bij0]]) fastforce+

  have bij8: "bij_betw (λn. map (λp. idx_enum R (nth_digit n (l-1-p) ?b)) [0..<l]) {..<?b^l} ?S2"
    by (intro iffD2[OF arg_cong3[where f="bij_betw"] bij_betw_trans[OF bij7 bij1]])
       (auto simp:comp_def list_all_iff atLeast0LessThan[symmetric])

  thus "bij_betw (poly_enum R l) {..<idx_size R ^ l} ?S4"
    using bij_betw_trans[OF bij8 bij2] unfolding poly_enum_def comp_def by simp
qed


definition poly_enum_inv :: "('a,'b) idx_ring_enum_scheme  nat  'a list  nat"
  where "poly_enum_inv R l f =
    (let f' = replicate (l - length f) 0CR@ f in
    (i<l. idx_enum_inv R (f' ! (l - 1 - i)) * idx_size R ^i ))"

find_theorems "(i<?l. ?f i * ?x^i) < ?x^?l"

lemma poly_enum_inv:
  assumes "enumC R" "ringC R"
  assumes "x   {xs. xs  carrier (poly_ring (ring_of R))  length xs  l}"
  shows "the_inv_into {..<idx_size R^l} (poly_enum R l) x = poly_enum_inv R l x"
proof -
  define f where "f = replicate (l- length x) 0CR@ x"
  let ?b = "idx_size R"
  let ?d = "dropWhile ((=) 0CR)"

  have len_f: "length f = l" using assms(3) unfolding f_def by auto
  note enum_c = enum_cD[OF assms(1)]

  interpret ring "ring_of R" using assms(2) unfolding ringC_def by simp

  have 0: "idx_enum_inv R y < ?b" if "y  carrier (ring_of R)" for y
    using bij_betw_imp_surj_on[OF enum_c(4)] enum_c(2) that by auto
  have 1: "(x = []  lead_coeff x  0CR)  list_all (idx_pred R) x  length x  l"
    using assms(3) unfolding ring_of_poly[OF assms(2),symmetric] by (simp add:ring_of_def poly_def)
  moreover have "𝟬ring_of R carrier (ring_of R)" by simp
  hence "idx_pred R 0CR⇙" unfolding ring_of_def by simp
  ultimately have 2: "set f  carrier (ring_of R)"
    unfolding f_def by (auto simp add:ring_of_def list_all_iff)

  have "poly_enum R l(poly_enum_inv R l x)= poly_enum R l (i<l. idx_enum_inv R (f ! (l-1-i))*?b^i)"
    unfolding poly_enum_inv_def f_def[symmetric] by simp
  also have "... = ?d (map (λp. idx_enum R (idx_enum_inv R (f ! (l - 1 - (l - 1 - p))))) [0..<l])"
    unfolding poly_enum_def using 2 len_f by (intro arg_cong[where f="?d"]
        arg_cong[where f="idx_enum R"] map_cong refl nth_digit_sum 0) auto
  also have "... =?d (map (λp. (f ! (l-1 - (l-1-p)))) [0..<l])"
    using 2 len_f by (intro arg_cong[where f="?d"] map_cong refl enum_c) auto
  also have "... =?d (map (λp. (f ! p)) [0..<l])"
    by (intro arg_cong[where f="?d"] map_cong) auto
  also have "... = ?d f" using len_f map_nth by (intro arg_cong[where f="?d"]) auto
  also have "... = ?d x" unfolding f_def by (intro dropWhile_append2) auto
  also have "... = x" using 1 by (intro iffD2[OF dropWhile_eq_self_iff]) auto
  finally have "poly_enum R l (poly_enum_inv R l x) = x" by simp
  moreover have "poly_enum_inv R l x < idx_size R^l"
    unfolding poly_enum_inv_def Let_def f_def[symmetric] using len_f 2
    by (intro nth_digit_sum(2) 0) auto
  ultimately show ?thesis
    by (intro the_inv_into_f_eq bij_betw_imp_inj_on[OF bij_betw_poly_enum[OF assms(1,2)]]) auto
qed

definition poly_mod_ring :: "('a,'b) idx_ring_enum_scheme  'a list => 'a list idx_ring_enum"
  where "poly_mod_ring R f = 
    idx_pred = (λxs. idx_pred (poly R) xs  length xs  degree f),
    idx_uminus = idx_uminus (poly R),
    idx_plus = (λx y. pmodC R (x +Cpoly Ry) f),
    idx_udivide = (λx. let ((u,v),r) = ext_euclidean R x f in pmodC R (r¯Cpoly R*Cpoly Ru) f),
    idx_mult = (λx y. pmodC R (x *Cpoly Ry) f),
    idx_zero = 0Cpoly R,
    idx_one = 1Cpoly R,
    idx_size = idx_size R ^ degree f,
    idx_enum = poly_enum R (degree f),
    idx_enum_inv = poly_enum_inv R (degree f) "

definition poly_mod_ring_iso :: "('a,'b) idx_ring_enum_scheme  'a list  'a list  'a list set"
  where "poly_mod_ring_iso R f x = PIdlpoly_ring (ring_of R)f +>poly_ring (ring_of R)x"

definition poly_mod_ring_iso_inv :: "('a,'b) idx_ring_enum_scheme  'a list  'a list set  'a list"
  where "poly_mod_ring_iso_inv R f =
    the_inv_into (carrier (ring_of (poly_mod_ring R f))) (poly_mod_ring_iso R f)"

context
  fixes f
  fixes R :: "('a,'b) idx_ring_enum_scheme"
  assumes field_R: "fieldC R"
  assumes f_carr: "f  carrier (poly_ring (ring_of R))"
  assumes deg_f: "degree f > 0"
begin

private abbreviation P where "P  poly_ring (ring_of R)"
private abbreviation I where "I  PIdlpoly_ring (ring_of R)f"

interpretation field "ring_of R"
  using field_R unfolding fieldC_def by auto

interpretation d: domain "P"
  by (intro univ_poly_is_domain carrier_is_subring)

interpretation i: ideal I P
  using f_carr by (intro d.cgenideal_ideal) auto

interpretation s: ring_hom_ring P "P Quot I"  "(+>P) I"
  using i.rcos_ring_hom_ring by auto

interpretation cr: cring "P Quot I"
    by (intro i.quotient_is_cring d.cring_axioms)

lemma ring_c: "ringC R"
  using field_R unfolding fieldC_def domainC_def cringC_def by auto

lemma d_poly: "domainC (poly R)" using field_R unfolding fieldC_def by (intro poly_domain) auto

lemma ideal_mod:
  assumes "y  carrier P"
  shows "I +>P(pmod y f) = I +>Py"
proof -
  have "f  I" by (intro d.cgenideal_self f_carr)
  hence "(f P(pdiv y f))  I"
    using long_division_closed[OF carrier_is_subfield] assms f_carr
    by (intro i.I_r_closed) (simp_all)
  hence "y  I +>P(pmod y f)"
    using assms f_carr unfolding a_r_coset_def'
    by (subst pdiv_pmod[OF carrier_is_subfield, where q="f"]) auto
  thus ?thesis
    by (intro i.a_repr_independence' assms long_division_closed[OF carrier_is_subfield] f_carr)
qed

lemma poly_mod_ring_carr_1:
  "carrier (ring_of (poly_mod_ring R f)) = {xs. xs  carrier P  degree xs < degree f}"
  (is "?L = ?R")
proof -
  have "?L = {xs. xs  carrier (ring_of (poly R))  degree xs < degree f}"
    using deg_f unfolding poly_mod_ring_def ring_of_def by auto
  also have "... = ?R" unfolding ring_of_poly[OF ring_c] by simp
  finally show ?thesis by simp
qed

lemma poly_mod_ring_carr:
  assumes "y  carrier P"
  shows "pmod y f  carrier (ring_of (poly_mod_ring R f))"
proof -
  have "f  []" using deg_f by auto
  hence "pmod y f = []  degree (pmod y f) < degree f"
    by (intro pmod_degree[OF carrier_is_subfield] assms f_carr)
  hence "degree (pmod y f) < degree f" using deg_f by auto
  moreover have "pmod y f  carrier P"
    using f_carr assms long_division_closed[OF carrier_is_subfield] by auto
  ultimately show ?thesis unfolding poly_mod_ring_carr_1 by auto
qed

lemma poly_mod_ring_iso_ran:
  "poly_mod_ring_iso R f ` carrier (ring_of (poly_mod_ring R f)) = carrier (P Quot I)"
proof -
  have "poly_mod_ring_iso R f x  carrier (P Quot I)"
    if "x  carrier (ring_of (poly_mod_ring R f))" for x
  proof -
    have "I  carrier P" by auto
    moreover have "x  carrier P" using that unfolding poly_mod_ring_carr_1 by auto
    ultimately have "poly_mod_ring_iso R f x  a_rcosetsPI"
      using that f_carr unfolding  poly_mod_ring_iso_def by (intro d.a_rcosetsI) auto
    thus ?thesis unfolding FactRing_def by simp
  qed
  moreover have "x  poly_mod_ring_iso R f ` carrier (ring_of (poly_mod_ring R f))"
    if "x  carrier (P Quot I)" for x
  proof -
    have "x  a_rcosetsPI" using that unfolding FactRing_def by auto
    then obtain y where y_def: "x = I +>Py" "y  carrier P"
      using that unfolding A_RCOSETS_def' by auto
    define z where "z = pmod y f"
    have "I +>Pz = I +>Py" unfolding z_def by (intro ideal_mod y_def)
    hence "poly_mod_ring_iso R f z = x" unfolding poly_mod_ring_iso_def y_def by simp
    moreover have "z  carrier (ring_of (poly_mod_ring R f))"
      unfolding z_def by (intro poly_mod_ring_carr y_def)
    ultimately show ?thesis by auto
  qed
  ultimately show ?thesis by auto
qed

lemma poly_mod_ring_iso_inj:
  "inj_on (poly_mod_ring_iso R f) (carrier (ring_of (poly_mod_ring R f)))"
proof (rule inj_onI)
  fix x y
  assume "x  carrier (ring_of (poly_mod_ring R f))"
  hence x:"x  carrier P" "degree x < degree f" unfolding poly_mod_ring_carr_1 by auto
  assume "y  carrier (ring_of (poly_mod_ring R f))"
  hence y:"y  carrier P" "degree y < degree f" unfolding poly_mod_ring_carr_1 by auto

  have "degree (x Py)  max (degree x) (degree (Py))"
    unfolding a_minus_def by (intro degree_add)
  also have "... = max (degree x) (degree y)"
    unfolding univ_poly_a_inv_degree[OF carrier_is_subring y(1)] by simp
  also have "... < degree f" using x(2) y(2) by simp
  finally have d:"degree (x Py) < degree f" by simp

  assume "poly_mod_ring_iso R f x = poly_mod_ring_iso R f y"
  hence "I +>Px = I +>Py" unfolding poly_mod_ring_iso_def by simp
  hence "x Py  I" using x y by (subst d.quotient_eq_iff_same_a_r_cos[OF i.ideal_axioms]) auto
  hence "f pdividesring_of R(x Py)"
    using f_carr x(1) y d.m_comm unfolding cgenideal_def pdivides_def factor_def by auto
  hence "(x Py) = []  degree (x Py)  degree f"
    using x(1) y(1) f_carr pdivides_imp_degree_le[OF carrier_is_subring] by (meson d.minus_closed)
  hence "(x Py) = 𝟬P⇙" unfolding univ_poly_zero using d by simp
  thus "x = y" using x(1) y(1) by simp
qed

lemma poly_mod_iso_ring_bij:
  "bij_betw (poly_mod_ring_iso R f) (carrier (ring_of (poly_mod_ring R f))) (carrier (P Quot I))"
  using poly_mod_ring_iso_ran poly_mod_ring_iso_inj unfolding bij_betw_def by simp

lemma poly_mod_iso_ring_bij_2:
  "bij_betw (poly_mod_ring_iso_inv R f) (carrier (P Quot I)) (carrier (ring_of (poly_mod_ring R f)))"
  unfolding poly_mod_ring_iso_inv_def using poly_mod_iso_ring_bij bij_betw_the_inv_into by blast

lemma poly_mod_ring_iso_inv_1:
  assumes "x  carrier (P Quot I)"
  shows "poly_mod_ring_iso R f (poly_mod_ring_iso_inv R f x) = x"
  unfolding poly_mod_ring_iso_inv_def using assms poly_mod_iso_ring_bij
  by (intro f_the_inv_into_f_bij_betw) auto

lemma poly_mod_ring_iso_inv_2:
  assumes "x  carrier (ring_of (poly_mod_ring R f))"
  shows "poly_mod_ring_iso_inv R f (poly_mod_ring_iso R f x) = x"
  unfolding poly_mod_ring_iso_inv_def using assms
  by (intro the_inv_into_f_f poly_mod_ring_iso_inj)

lemma poly_mod_ring_add:
  assumes "x  carrier P"
  assumes "y  carrier P"
  shows "x ring_of (poly_mod_ring R f)y = pmod (x Py) f" (is "?L = ?R")
proof -
  have "?L = pmodC R (x ring_of (poly R)y) f"
    unfolding poly_mod_ring_def ring_of_def using domain_cD[OF d_poly] by simp
  also have "... = ?R"
    using assms unfolding ring_of_poly[OF ring_c] by (intro pmod_c[OF field_R] f_carr) auto
  finally show ?thesis
    by simp
qed

lemma poly_mod_ring_zero: "𝟬ring_of (poly_mod_ring R f)= 𝟬P⇙"
proof-
  have "𝟬ring_of (poly_mod_ring R f)= 𝟬ring_of (poly R)⇙"
    using domain_cD[OF d_poly] unfolding ring_of_def poly_mod_ring_def by simp
  also have "... = 𝟬P⇙" unfolding ring_of_poly[OF ring_c] by simp
  finally show ?thesis by simp
qed

lemma poly_mod_ring_one: "𝟭ring_of (poly_mod_ring R f)= 𝟭P⇙"
proof-
  have "𝟭ring_of (poly_mod_ring R f)= 𝟭ring_of (poly R)⇙"
    using domain_cD[OF d_poly] unfolding ring_of_def poly_mod_ring_def by simp
  also have "... = 𝟭P⇙" unfolding ring_of_poly[OF ring_c] by simp
  finally show "𝟭ring_of (poly_mod_ring R f)= 𝟭P⇙" by simp
qed

lemma poly_mod_ring_mult:
  assumes "x  carrier P"
  assumes "y  carrier P"
  shows "x ring_of (poly_mod_ring R f)y = pmod (x Py) f" (is "?L = ?R")
proof -
  have "?L = pmodC R (x ring_of (poly R)y) f"
    unfolding poly_mod_ring_def ring_of_def using domain_cD[OF d_poly] by simp
  also have "... = ?R"
    using assms unfolding poly_mod_ring_carr_1 ring_of_poly[OF ring_c]
    by (intro pmod_c[OF field_R] f_carr) auto
  finally show ?thesis
    by simp
qed

lemma poly_mod_ring_iso_inv:
  "poly_mod_ring_iso_inv R f  ring_iso (P Quot I) (ring_of (poly_mod_ring R f))"
  (is "?f  ring_iso ?S ?T")
proof (rule ring_iso_memI)
  fix x assume "x  carrier ?S"
  thus "?f x  carrier ?T" using bij_betw_apply[OF poly_mod_iso_ring_bij_2] by auto
next
  fix x y assume x:"x  carrier ?S" and y: "y  carrier ?S"
  have "?f x  carrier (ring_of (poly_mod_ring R f))"
    by (rule bij_betw_apply[OF poly_mod_iso_ring_bij_2 x])
  hence x':"?f x  carrier P" unfolding poly_mod_ring_carr_1 by simp
  have "?f y  carrier (ring_of (poly_mod_ring R f))"
    by (rule bij_betw_apply[OF poly_mod_iso_ring_bij_2 y])
  hence y':"?f y  carrier P" unfolding poly_mod_ring_carr_1 by simp

  have 0:"?f x ?T?f y = pmod (?f x P?f y) f"
    by (intro poly_mod_ring_mult x' y')
  also have "...  carrier (ring_of (poly_mod_ring R f))"
    using x' y' by (intro poly_mod_ring_carr) auto
  finally have xy: "?f x ?T?f y  carrier (ring_of (poly_mod_ring R f))" by simp

  have "?f (x ?Sy) = ?f (poly_mod_ring_iso R f (?f x) ?Spoly_mod_ring_iso R f (?f y))"
    using x y by (simp add:poly_mod_ring_iso_inv_1)
  also have "... = ?f ((I +>P(?f x)) ?S(I +>P(?f y)))"
    unfolding poly_mod_ring_iso_def by simp
  also have "... = ?f (I +>P(?f x P?f y))"
    using x' y' by simp
  also have "... = ?f (I +>P(pmod (?f x P?f y) f))"
    using x' y' by (subst ideal_mod) auto
  also have "... = ?f (I +>P(?f x ?T?f y))"
    unfolding 0 by simp
  also have "... = ?f (poly_mod_ring_iso R f (?f x ?T?f y))"
    unfolding poly_mod_ring_iso_def by simp
  also have "... = ?f x ?T?f y"
    using xy by (intro poly_mod_ring_iso_inv_2)
  finally show "?f (x ?Sy) = ?f x ?T?f y" by simp
next
  fix x y assume x:"x  carrier ?S" and y: "y  carrier ?S"
  have "?f x  carrier (ring_of (poly_mod_ring R f))"
    by (rule bij_betw_apply[OF poly_mod_iso_ring_bij_2 x])
  hence x':"?f x  carrier P" unfolding poly_mod_ring_carr_1 by simp
  have "?f y  carrier (ring_of (poly_mod_ring R f))"
    by (rule bij_betw_apply[OF poly_mod_iso_ring_bij_2 y])
  hence y':"?f y  carrier P" unfolding poly_mod_ring_carr_1 by simp

  have 0:"?f x ?T?f y = pmod (?f x P?f y) f"  by (intro poly_mod_ring_add x' y')
  also have "...  carrier (ring_of (poly_mod_ring R f))"
    using x' y' by (intro poly_mod_ring_carr) auto
  finally have xy: "?f x ?T?f y  carrier (ring_of (poly_mod_ring R f))" by simp

  have "?f (x ?Sy) = ?f (poly_mod_ring_iso R f (?f x) ?Spoly_mod_ring_iso R f (?f y))"
    using x y by (simp add:poly_mod_ring_iso_inv_1)
  also have "... = ?f ((I +>P(?f x)) ?S(I +>P(?f y)))"
    unfolding poly_mod_ring_iso_def by simp
  also have "... = ?f (I +>P(?f x P?f y))"
    using x' y' by simp
  also have "... = ?f (I +>P(pmod (?f x P?f y) f))"
    using x' y' by (subst ideal_mod) auto
  also have "... = ?f (I +>P(?f x ?T?f y))"
    unfolding 0 by simp
  also have "... = ?f (poly_mod_ring_iso R f (?f x ?T?f y))"
    unfolding poly_mod_ring_iso_def by simp
  also have "... = ?f x ?T?f y"
    using xy by (intro poly_mod_ring_iso_inv_2)
  finally show "?f (x ?Sy) = ?f x ?T?f y" by simp
next
  have "poly_mod_ring_iso R f 𝟭ring_of (poly_mod_ring R f)= (I +>P𝟭P)"
    unfolding poly_mod_ring_one poly_mod_ring_iso_def by simp
  also have "... = 𝟭P Quot I⇙" using s.hom_one by simp
  finally have "poly_mod_ring_iso R f 𝟭ring_of (poly_mod_ring R f)= 𝟭P Quot I⇙" by simp
  moreover have "degree 𝟭P< degree f"
    using deg_f unfolding univ_poly_one by simp
  hence "𝟭ring_of (poly_mod_ring R f) carrier (ring_of (poly_mod_ring R f))"
    unfolding poly_mod_ring_one poly_mod_ring_carr_1 by simp
  ultimately show "?f (𝟭?S) = 𝟭?T⇙"
    unfolding poly_mod_ring_iso_inv_def by (intro the_inv_into_f_eq poly_mod_ring_iso_inj)
next
  show "bij_betw ?f (carrier ?S) (carrier ?T)" by (rule poly_mod_iso_ring_bij_2)
qed

lemma cring_poly_mod_ring_1:
  shows "ring_of (poly_mod_ring R f)zero := poly_mod_ring_iso_inv R f 𝟬P Quot I =
    ring_of (poly_mod_ring R f)"
    and  "cring (ring_of (poly_mod_ring R f))"
proof -
  let ?f = "poly_mod_ring_iso_inv R f"

  have "poly_mod_ring_iso R f 𝟬P= 𝟬P Quot PIdlPf⇙"
    unfolding poly_mod_ring_iso_def by simp
  moreover have "[]  carrier P" using univ_poly_zero[where K="carrier (ring_of R)"] by auto
  ultimately have "?f 𝟬P Quot I= 𝟬P⇙"
    unfolding univ_poly_zero poly_mod_ring_iso_inv_def using deg_f
    by (intro the_inv_into_f_eq bij_betw_imp_inj_on[OF poly_mod_iso_ring_bij])
      (simp_all add:add:poly_mod_ring_carr_1)
  also have "... = 0Cpoly R⇙" using ring_of_poly[OF ring_c] domain_cD[OF d_poly] by auto
  finally have "?f 𝟬P Quot I= 0Cpoly R⇙" by simp
  thus "ring_of (poly_mod_ring R f)zero := ?f 𝟬P Quot I = ring_of (poly_mod_ring R f)"
    unfolding ring_of_def poly_mod_ring_def by auto
  thus "cring (ring_of (poly_mod_ring R f))"
    using cr.ring_iso_imp_img_cring[OF poly_mod_ring_iso_inv] by simp
qed

interpretation cr_p: cring "(ring_of (poly_mod_ring R f))"
  by (rule cring_poly_mod_ring_1)

lemma cring_c_poly_mod_ring: "cringC (poly_mod_ring R f)"
proof -
  let ?P = "ring_of (poly_mod_ring R f)"
  have "-Cpoly_mod_ring R fx = ring_of (poly_mod_ring R f)x" (is "?L = ?R")
    if "x  carrier (ring_of (poly_mod_ring R f))" for x
  proof (rule cr_p.minus_equality[symmetric, OF _ that])
    have "-Cpoly_mod_ring R fx = -Cpoly Rx" unfolding poly_mod_ring_def by simp
    also have "... = Px" using that unfolding poly_mod_ring_carr_1
      by (subst domain_cD[OF d_poly]) (simp_all add:ring_of_poly[OF ring_c])
    finally have 0:"-Cpoly_mod_ring R fx = Px" by simp

    have 1:"Px   carrier (ring_of (poly_mod_ring R f))"
      using that univ_poly_a_inv_degree[OF carrier_is_subring] unfolding poly_mod_ring_carr_1
      by auto

    have "-Cpoly_mod_ring R fx ?Px = pmod (Px Px) f"
      using that 1 unfolding 0 poly_mod_ring_carr_1 by (intro poly_mod_ring_add) auto
    also have "... = pmod 𝟬Pf"
      using that unfolding poly_mod_ring_carr_1 by simp algebra
    also have "... = []"
      unfolding univ_poly_zero using carrier_is_subfield f_carr long_division_zero(2) by presburger
    also have "... =  𝟬?P⇙" by (simp add:poly_mod_ring_def ring_of_def poly_def)
    finally show "-Cpoly_mod_ring R fx ?Px = 𝟬?P⇙" by simp

    show " -Cpoly_mod_ring R fx  carrier (ring_of (poly_mod_ring R f))"
      unfolding 0 by (rule 1)
  qed
  moreover have "x ¯Cpoly_mod_ring R f= invring_of (poly_mod_ring R f)x"
    if x_unit: "x  Units (ring_of (poly_mod_ring R f))" for x
  proof (rule cr_p.comm_inv_char[symmetric])
    show x_carr: "x  carrier (ring_of (poly_mod_ring R f))"
      using that unfolding Units_def by auto

    obtain y where y:"x ring_of (poly_mod_ring R f)y = 𝟭ring_of (poly_mod_ring R f)⇙"
       and y_carr: "y  carrier (ring_of (poly_mod_ring R f))"
      using x_unit unfolding Units_def by auto

    have "pmod (x Py) f =x ring_of (poly_mod_ring R f)y"
      using x_carr y_carr by (intro poly_mod_ring_mult[symmetric]) (auto simp:poly_mod_ring_carr_1)
    also have "... = 𝟭P⇙"
      unfolding y poly_mod_ring_one by simp
    finally have 1:"pmod (x Py) f = 𝟭P⇙" by simp

    have "pcoprimering_of R(x Py) f = pcoprimering_of Rf (pmod (x Py) f)"
      using x_carr y_carr f_carr unfolding poly_mod_ring_carr_1 by (intro pcoprime_step) auto
    also have "... = pcoprimering_of Rf  𝟭P⇙" unfolding 1 by simp
    also have "... = True" using pcoprime_one by simp
    finally have "pcoprimering_of R(x Py) f" by simp
    hence "pcoprimering_of Rx f"
      using x_carr y_carr f_carr pcoprime_left_factor unfolding poly_mod_ring_carr_1 by blast
    hence 2:"length (snd ( ext_euclidean R x f)) = 1"
      using f_carr x_carr pcoprime_c[OF field_R] unfolding poly_mod_ring_carr_1 pcoprimeC.simps
      by auto

    obtain u v r where uvr_def: "((u,v),r) = ext_euclidean R x f"  by (metis surj_pair)

    have x_carr': "x  carrier P" using x_carr unfolding poly_mod_ring_carr_1 by auto
    have r_eq:"r = x Pu Pf Pv" and ruv_carr: "{r, u, v}  carrier P"
      using uvr_def[symmetric] ext_euclidean[OF field_R x_carr' f_carr] by auto

    have "length r = 1" using 2 uvr_def[symmetric] by simp
    hence 3:"r = [hd r]" by (cases r) auto
    hence "r  𝟬P⇙" unfolding univ_poly_zero by auto
    hence "hd r  carrier (ring_of R) - {𝟬ring_of R}"
      using ruv_carr by (intro lead_coeff_carr) auto
    hence r_unit: "r  Units P" using 3 univ_poly_units[OF carrier_is_subfield] by auto
    hence inv_r_carr: "invPr  carrier P" by simp

    have 0: "x ¯Cpoly_mod_ring R f= pmodC R (r ¯Cpoly R*Cpoly Ru) f"
      by (simp add:poly_mod_ring_def uvr_def[symmetric])
    also have "... = pmodC R (invPr Pu) f"
      using r_unit unfolding domain_cD[OF d_poly]
      by (subst domain_cD[OF d_poly]) (simp_all add:ring_of_poly[OF ring_c])
    also have "... = pmod (invPr Pu) f"
      using ruv_carr inv_r_carr by (intro pmod_c[OF field_R] f_carr) simp
    finally have 0: "x ¯Cpoly_mod_ring R f= pmod (invPr Pu) f"
      by simp

    show "x ¯Cpoly_mod_ring R f carrier (ring_of (poly_mod_ring R f))"
      using ruv_carr r_unit unfolding 0 by (intro poly_mod_ring_carr) simp

    have 4: "degree 𝟭P< degree f" unfolding univ_poly_one using deg_f by auto

    have "f dividesPinvPr Pf Pv"
      using inv_r_carr ruv_carr  f_carr
      by (intro dividesI[where c="invPr Pv"]) (simp_all, algebra)
    hence 5: "pmod (invPr Pf Pv) f = []"
      using f_carr ruv_carr inv_r_carr
      by (intro  iffD2[OF pmod_zero_iff_pdivides[OF carrier_is_subfield]]) (auto simp:pdivides_def)

    have "x ?Px ¯Cpoly_mod_ring R f= pmod (x Ppmod (invPr Pu) f) f"
      using ruv_carr inv_r_carr f_carr unfolding 0
      by (intro poly_mod_ring_mult x_carr' long_division_closed[OF carrier_is_subfield]) simp_all
    also have "... = pmod (x P(invPr Pu)) f"
      using ruv_carr inv_r_carr f_carr by (intro pmod_mult_right[symmetric] x_carr') auto
    also have "... = pmod (invPr P(x Pu)) f"
      using x_carr' ruv_carr inv_r_carr by (intro arg_cong2[where f="pmod"] refl) (simp, algebra)
    also have "... = pmod (invPr P(r Pf Pv)) f" using ruv_carr f_carr x_carr'
      by (intro arg_cong2[where f="pmod"] arg_cong2[where f="(⊗P)"] refl) (simp add:r_eq, algebra)
    also have "... = pmod (invPr Pr PinvPr Pf Pv) f"
      using ruv_carr inv_r_carr f_carr by (intro arg_cong2[where f="pmod"] refl) (simp, algebra)
    also have "... = pmod 𝟭Pf Ppmod (P(invPr Pf Pv)) f"
      using ruv_carr inv_r_carr f_carr  unfolding d.Units_l_inv[OF r_unit] a_minus_def
      by (intro long_division_add[OF carrier_is_subfield]) simp_all
    also have "... = 𝟭PPpmod (invPr Pf Pv) f"
      using ruv_carr f_carr inv_r_carr unfolding a_minus_def
      by (intro arg_cong2[where f="(⊕P)"] pmod_const[OF carrier_is_subfield]
          long_division_a_inv[OF carrier_is_subfield] 4) simp_all
    also have "... = 𝟭PP𝟬P⇙" unfolding 5 univ_poly_zero by simp
    also have "... =  𝟭ring_of (poly_mod_ring R f)⇙" unfolding poly_mod_ring_one by algebra
    finally show "x ring_of (poly_mod_ring R f)x ¯Cpoly_mod_ring R f= 𝟭?P⇙" by simp
  qed
  ultimately show ?thesis using cring_poly_mod_ring_1 by (intro cring_cI)
qed


end

lemma field_c_poly_mod_ring:
  assumes field_R: "fieldC R"
  assumes "monic_irreducible_poly (ring_of R) f"
  shows "fieldC (poly_mod_ring R f)"
proof -
  interpret field "ring_of R" using field_R unfolding fieldC_def by auto

  have f_carr: "f  carrier (poly_ring (ring_of R))"
    using assms(2) monic_poly_carr unfolding monic_irreducible_poly_def by auto

  have deg_f: "degree f > 0" using monic_poly_min_degree assms(2) by fastforce

  have f_irred: "pirreduciblering_of R(carrier (ring_of R)) f"
    using assms(2) unfolding monic_irreducible_poly_def by auto

  interpret r:field "poly_ring (ring_of R) Quot (PIdlpoly_ring (ring_of R)f)"
    using f_irred f_carr iffD2[OF rupture_is_field_iff_pirreducible[OF carrier_is_subfield]]
    unfolding rupture_def by blast

  have "field (ring_of (poly_mod_ring R f))"
    using r.ring_iso_imp_img_field[OF poly_mod_ring_iso_inv[OF field_R f_carr deg_f]]
    using cring_poly_mod_ring_1(1)[OF field_R f_carr deg_f] by simp
  moreover have "cringC (poly_mod_ring R f)"
    by (rule cring_c_poly_mod_ring[OF field_R f_carr deg_f])
  ultimately show ?thesis unfolding fieldC_def domainC_def using field.axioms(1) by blast
qed


lemma enum_c_poly_mod_ring:
  assumes "enumC R" "ringC R"
  shows "enumC (poly_mod_ring R f)"
proof (rule enum_cI)
  let ?l = "degree f"
  let ?b = "idx_size R"
  let ?S = "carrier (ring_of (poly_mod_ring R f))"

  note bij_0 = bij_betw_poly_enum[where l="degree f", OF assms(1,2)]
  have "?S = {xs  carrier (poly_ring (ring_of R)). length xs  ?l}"
    unfolding ring_of_poly[OF assms(2),symmetric] poly_mod_ring_def by (simp add:ring_of_def)
  hence bij_1:"bij_betw (poly_enum R (degree f)) {..<idx_size R ^ degree f} ?S"
    using bij_0 by simp
  hence bij_2:"bij_betw (idx_enum (poly_mod_ring R f)) {..<idx_size R^degree f} ?S"
    unfolding poly_mod_ring_def by simp

  have "order (ring_of (poly_mod_ring R f)) = card ?S"
    unfolding Coset.order_def by simp
  also have "... = card {..<idx_size R ^ degree f}" using bij_2 by (metis bij_betw_same_card)
  finally have ord_poly_mod_ring: "order (ring_of (poly_mod_ring R f)) = idx_size R^degree f"
    by simp

  show "finite ?S" using bij_2 bij_betw_finite by blast
  show "idx_size (poly_mod_ring R f) = order (ring_of (poly_mod_ring R f))"
    unfolding ord_poly_mod_ring by (simp add:poly_mod_ring_def)
  show "bij_betw (idx_enum (poly_mod_ring R f)) {..<order (ring_of (poly_mod_ring R f))} ?S"
    using bij_2 ord_poly_mod_ring by auto
  show "idx_enum_inv (poly_mod_ring R f) (idx_enum (poly_mod_ring R f) x) = x" (is "?L = _ ")
    if "x < order (ring_of (poly_mod_ring R f))" for x
  proof -
    have "?L = poly_enum_inv R (degree f) (poly_enum R (degree f) x)"
      unfolding poly_mod_ring_def by simp
    also have "... = the_inv_into {..<?b ^ ?l} (poly_enum R ?l) (poly_enum R ?l x)"
      using that ord_poly_mod_ring
      by (intro poly_enum_inv[OF assms(1,2),symmetric] bij_betw_apply[OF bij_0]) auto
    also have "... = x"
      using that ord_poly_mod_ring by (intro the_inv_into_f_f bij_betw_imp_inj_on[OF bij_0]) auto
    finally show ?thesis by simp
  qed
qed

end