# Theory Finite_Fields.Finite_Fields_Mod_Ring_Code

```section ‹Executable Factor Rings›

theory Finite_Fields_Mod_Ring_Code
imports Finite_Fields_Indexed_Algebra_Code Ring_Characteristic
begin

definition mod_ring :: "nat ⇒ nat idx_ring_enum"
where "mod_ring n = ⦇
idx_pred = (λx. x < n),
idx_uminus = (λx. (n-x) mod n),
idx_plus = (λx y. (x+y) mod n),
idx_udivide = (λx. nat (fst (bezout_coefficients (int x) (int n)) mod (int n))),
idx_mult = (λx y. (x*y) mod n),
idx_zero = 0,
idx_one = 1,
idx_size = n,
idx_enum = id,
idx_enum_inv = id
⦈"

lemma zfact_iso_0:
assumes "n > 0"
shows "zfact_iso n 0 = 𝟬⇘ZFact (int n)⇙"
proof -
let ?I = "Idl⇘𝒵⇙ {int n}"
have ideal_I: "ideal ?I 𝒵"

interpret i:ideal "?I" "𝒵" using ideal_I by simp
interpret s:ring_hom_ring "𝒵" "ZFact (int n)" "(+>⇘𝒵⇙) ?I"
using i.rcos_ring_hom_ring ZFact_def by auto

show ?thesis
qed

lemma zfact_prime_is_field:
assumes "Factorial_Ring.prime (p :: nat)"
shows "field (ZFact (int p))"
using zfact_prime_is_finite_field[OF assms] finite_field_def by auto

definition zfact_iso_inv :: "nat ⇒ int set ⇒ nat" where
"zfact_iso_inv p = the_inv_into {..<p} (zfact_iso p)"

lemma zfact_iso_inv_0:
assumes n_ge_0: "n > 0"
shows "zfact_iso_inv n 𝟬⇘ZFact (int n)⇙ = 0"
unfolding zfact_iso_inv_def zfact_iso_0[OF n_ge_0, symmetric] using n_ge_0
by (rule the_inv_into_f_f[OF zfact_iso_inj], simp add:mod_ring_def)

lemma zfact_coset:
assumes n_ge_0: "n > 0"
assumes "x ∈ carrier (ZFact (int n))"
defines "I ≡ Idl⇘𝒵⇙ {int n}"
shows "x = I +>⇘𝒵⇙ (int (zfact_iso_inv n x))"
proof -
have "x ∈ zfact_iso n ` {..<n}"
using assms zfact_iso_ran by simp
hence "zfact_iso n (zfact_iso_inv n x) = x"
unfolding zfact_iso_inv_def by (intro f_the_inv_into_f zfact_iso_inj) auto
thus ?thesis unfolding zfact_iso_def I_def by blast
qed

lemma zfact_iso_inv_bij:
assumes "n > 0"
shows "bij_betw (zfact_iso_inv n) (carrier (ZFact (int n))) (carrier (ring_of (mod_ring n)))"
proof -
have "bij_betw (the_inv_into {..<n} (zfact_iso n)) (carrier (ZFact (int n))) {..<n}"
by (intro bij_betw_the_inv_into zfact_iso_bij[OF assms])
thus ?thesis
unfolding zfact_iso_inv_def mod_ring_def ring_of_def lessThan_def by simp
qed

lemma zfact_iso_inv_is_ring_iso:
fixes n :: nat
assumes n_ge_1: "n > 1"
shows "zfact_iso_inv n ∈ ring_iso (ZFact (int n)) (ring_of (mod_ring n))" (is "?f ∈ _")
proof (rule ring_iso_memI)
interpret r:cring "(ZFact (int n))"
using ZFact_is_cring by simp

define I where "I = Idl⇘𝒵⇙ {int n}"

have n_ge_0: "n > 0" using n_ge_1 by simp

interpret i:ideal "I" "𝒵"
unfolding I_def using int.genideal_ideal by simp

interpret s:ring_hom_ring "𝒵" "ZFact (int n)" "(+>⇘𝒵⇙) I"
using i.rcos_ring_hom_ring ZFact_def I_def by auto

show "zfact_iso_inv n x ∈ carrier (ring_of (mod_ring n))" if "x ∈ carrier (ZFact (int n))" for x
proof -
have "zfact_iso_inv n x ∈ {..<n}"
unfolding zfact_iso_inv_def using that zfact_iso_ran[OF n_ge_0]
by (intro the_inv_into_into zfact_iso_inj n_ge_0) auto
thus "zfact_iso_inv n x ∈ carrier (ring_of (mod_ring n))"
qed

show "?f (x ⊗⇘ZFact (int n)⇙ y) = ?f x ⊗⇘ring_of (mod_ring n)⇙ ?f y"
if x_carr: "x ∈ carrier (ZFact (int n))" and y_carr: "y ∈ carrier (ZFact (int n))" for x y
proof -
define x' where "x' = zfact_iso_inv n x"
define y' where "y' = zfact_iso_inv n y"
have "x ⊗⇘ZFact (int n)⇙ y = (I +>⇘𝒵⇙ (int x')) ⊗⇘ZFact (int n)⇙ (I +>⇘𝒵⇙ (int y'))"
unfolding x'_def y'_def
using x_carr y_carr zfact_coset[OF n_ge_0] I_def by simp
also have "... = (I +>⇘𝒵⇙ (int x' * int y'))"
by simp
also have "... = (I +>⇘𝒵⇙ (int ((x' * y') mod n)))"
unfolding I_def zmod_int by (rule int_cosetI[OF n_ge_0],simp)
also have "... = (I +>⇘𝒵⇙ (x' ⊗⇘ring_of (mod_ring n)⇙ y'))"
unfolding ring_of_def mod_ring_def by simp
also have "... = zfact_iso n (x' ⊗⇘ring_of (mod_ring n)⇙ y')"
unfolding zfact_iso_def I_def by simp
finally have a:"x ⊗⇘ZFact (int n)⇙ y = zfact_iso n (x' ⊗⇘ring_of (mod_ring n)⇙ y')"
by simp
have b:"x' ⊗⇘ring_of (mod_ring n)⇙ y' ∈ {..<n}"
using mod_ring_def n_ge_0 by (auto simp:ring_of_def)
have "?f (zfact_iso n (x' ⊗⇘ring_of (mod_ring n)⇙ y')) = x' ⊗⇘ring_of (mod_ring n)⇙ y'"
unfolding zfact_iso_inv_def
by (rule the_inv_into_f_f[OF zfact_iso_inj[OF n_ge_0] b])
thus
"zfact_iso_inv n (x ⊗⇘ZFact (int n)⇙ y) =
zfact_iso_inv n x ⊗⇘ring_of (mod_ring n)⇙ zfact_iso_inv n y"
using a x'_def y'_def by simp
qed

show "zfact_iso_inv n (x ⊕⇘ZFact (int n)⇙ y) =
zfact_iso_inv n x ⊕⇘ring_of (mod_ring n)⇙ zfact_iso_inv n y"
if x_carr: "x ∈ carrier (ZFact (int n))" and y_carr: "y ∈ carrier (ZFact (int n))" for x y
proof -
define x' where "x' = zfact_iso_inv n x"
define y' where "y' = zfact_iso_inv n y"
have "x ⊕⇘ZFact (int n)⇙ y = (I +>⇘𝒵⇙ (int x')) ⊕⇘ZFact (int n)⇙ (I +>⇘𝒵⇙ (int y'))"
unfolding x'_def y'_def
using x_carr y_carr zfact_coset[OF n_ge_0] I_def by simp
also have "... = (I +>⇘𝒵⇙ (int x' + int y'))"
by simp
also have "... = (I +>⇘𝒵⇙ (int ((x' + y') mod n)))"
unfolding I_def zmod_int by (rule int_cosetI[OF n_ge_0],simp)
also have "... = (I +>⇘𝒵⇙ (x' ⊕⇘ring_of (mod_ring n)⇙ y'))"
unfolding mod_ring_def ring_of_def by simp
also have "... = zfact_iso n (x' ⊕⇘ring_of (mod_ring n)⇙ y')"
unfolding zfact_iso_def I_def by simp
finally have a:"x ⊕⇘ZFact (int n)⇙ y = zfact_iso n (x' ⊕⇘ring_of (mod_ring n)⇙ y')"
by simp
have b:"x' ⊕⇘ring_of (mod_ring n)⇙ y' ∈ {..<n}"
using mod_ring_def n_ge_0 by (auto simp:ring_of_def)
have "?f (zfact_iso n (x' ⊕⇘ring_of (mod_ring n)⇙ y')) = x' ⊕⇘ring_of (mod_ring n)⇙ y'"
unfolding zfact_iso_inv_def
by (rule the_inv_into_f_f[OF zfact_iso_inj[OF n_ge_0] b])
thus "?f (x ⊕⇘ZFact (int n)⇙ y) = ?f x ⊕⇘ring_of (mod_ring n)⇙ ?f y"
using a x'_def y'_def by simp
qed

have "𝟭⇘ZFact (int n)⇙ = zfact_iso n (𝟭⇘ring_of (mod_ring n)⇙)"
by (simp add:zfact_iso_def ZFact_def I_def[symmetric] ring_of_def mod_ring_def)

thus "zfact_iso_inv n 𝟭⇘ZFact (int n)⇙ = 𝟭⇘ring_of (mod_ring n)⇙"
unfolding zfact_iso_inv_def mod_ring_def ring_of_def
using the_inv_into_f_f[OF zfact_iso_inj] n_ge_1 by simp

show "bij_betw (zfact_iso_inv n) (carrier (ZFact (int n))) (carrier (ring_of (mod_ring n)))"
by (intro zfact_iso_inv_bij n_ge_0)
qed

lemma mod_ring_finite:
"finite (carrier (ring_of (mod_ring n)))"

lemma mod_ring_carr:
"x ∈ carrier (ring_of (mod_ring n)) ⟷  x < n"

lemma mod_ring_is_cring:
assumes n_ge_1: "n > 1"
shows "cring (ring_of (mod_ring n))"
proof -
have n_ge_0: "n > 0" using n_ge_1 by simp

interpret cring "ZFact (int n)"
using ZFact_is_cring by simp

have "cring ((ring_of (mod_ring n)) ⦇ zero := zfact_iso_inv n 𝟬⇘ZFact (int n)⇙ ⦈)"
by (rule ring_iso_imp_img_cring[OF zfact_iso_inv_is_ring_iso[OF n_ge_1]])
moreover have
"ring_of (mod_ring n) ⦇ zero := zfact_iso_inv n 𝟬⇘ZFact (int n)⇙ ⦈ = ring_of (mod_ring n)"
using zfact_iso_inv_0[OF n_ge_0] by (simp add:mod_ring_def ring_of_def)
ultimately show ?thesis by simp
qed

lemma zfact_iso_is_ring_iso:
assumes n_ge_1: "n > 1"
shows "zfact_iso n ∈ ring_iso (ring_of (mod_ring n)) (ZFact (int n))"
proof -
have r:"ring (ZFact (int n))"
using ZFact_is_cring cring.axioms(1) by blast

interpret s: ring "(ring_of (mod_ring n))"
using mod_ring_is_cring cring.axioms(1) n_ge_1 by blast
have n_ge_0: "n > 0" using n_ge_1 by linarith

have "inv_into (carrier (ZFact (int n))) (zfact_iso_inv n)
∈ ring_iso (ring_of (mod_ring n)) (ZFact (int n))"
using ring_iso_set_sym[OF r zfact_iso_inv_is_ring_iso[OF n_ge_1]] by simp
moreover have "inv_into (carrier (ZFact (int n))) (zfact_iso_inv n) x = zfact_iso n x"
if "x ∈ carrier (ring_of (mod_ring n))" for x
proof -
have "x ∈ {..<n}" using that by (simp add:mod_ring_def ring_of_def)
thus "inv_into (carrier (ZFact (int n))) (zfact_iso_inv n) x = zfact_iso n x"
using zfact_iso_inv_bij[OF n_ge_0] zfact_iso_bij[OF n_ge_0] unfolding zfact_iso_inv_def
by (intro inv_into_f_eq bij_betw_apply[OF zfact_iso_inv_bij[OF n_ge_0]] the_inv_into_f_f)
(auto intro:bij_betw_imp_inj_on simp:bij_betwE)
qed

ultimately show ?thesis using s.ring_iso_restrict by blast
qed

text ‹If @{term "p"} is a prime than @{term "mod_ring p"} is a field:›

lemma mod_ring_is_field:
assumes"Factorial_Ring.prime p"
shows "field (ring_of (mod_ring p))"
proof -
have p_ge_0: "p > 0" using assms prime_gt_0_nat by blast
have p_ge_1: "p > 1" using assms prime_gt_1_nat by blast

interpret field "ZFact (int p)"
using zfact_prime_is_field[OF assms] by simp

have "field ((ring_of (mod_ring p)) ⦇ zero := zfact_iso_inv p 𝟬⇘ZFact (int p)⇙ ⦈)"
by (rule ring_iso_imp_img_field[OF zfact_iso_inv_is_ring_iso[OF p_ge_1]])

moreover have
"(ring_of (mod_ring p)) ⦇ zero := zfact_iso_inv p 𝟬⇘ZFact (int p)⇙ ⦈ = ring_of (mod_ring p)"
using zfact_iso_inv_0[OF p_ge_0] by (simp add:mod_ring_def ring_of_def)
ultimately show ?thesis by simp
qed

lemma mod_ring_is_ring_c:
assumes "n > 1"
shows "cring⇩C (mod_ring n)"
proof (intro cring_cI mod_ring_is_cring assms)
fix x
assume a:"x ∈ carrier (ring_of (mod_ring n))"
hence x_le_n: "x < n" unfolding mod_ring_def ring_of_def by simp

interpret cring "(ring_of (mod_ring n))" by (intro mod_ring_is_cring assms)

show "-⇩C⇘mod_ring n⇙ x = ⊖⇘ring_of (mod_ring n)⇙ x" using x_le_n
by (intro minus_equality[symmetric] a) (simp_all add:ring_of_def mod_ring_def mod_simps)
next
fix x
assume a:"x ∈ Units (ring_of (mod_ring n))"

let ?l = "fst (bezout_coefficients (int x) (int n))"
let ?r = "snd (bezout_coefficients (int x) (int n))"

interpret cring "ring_of (mod_ring n)" by (intro mod_ring_is_cring assms)

obtain y where "x ⊗⇘ring_of (mod_ring n)⇙ y = 𝟭⇘ring_of (mod_ring n)⇙"
using a by (meson Units_r_inv_ex)
hence "x * y mod n = 1" by (simp_all add:mod_ring_def ring_of_def)
hence "gcd x n = 1" by (metis dvd_triv_left gcd.assoc gcd_1_nat gcd_nat.absorb_iff1 gcd_red_nat)
hence 0:"gcd (int x) (int n) = 1" unfolding gcd_int_int_eq by simp

have "int x * ?l mod int n = (?l * int x + ?r * int n) mod int n"
using assms by (simp add:mod_simps algebra_simps)
also have "... = (gcd (int x) (int n)) mod int n"
by (intro arg_cong2[where f="(mod)"] refl bezout_coefficients) simp
also have "... = 1" unfolding 0 using assms by simp
finally have "int x * ?l mod int n = 1" by simp
hence "int x * nat (fst (bezout_coefficients (int x) (int n)) mod int n) mod n = 1"
hence "x * nat (fst (bezout_coefficients (int x) (int n)) mod int n) mod n = 1"
by (metis nat_mod_as_int nat_one_as_int of_nat_mult)
hence "x ⊗⇘ring_of (mod_ring n)⇙ x ¯⇩C⇘mod_ring n⇙ = 𝟭⇘ring_of (mod_ring n)⇙"
using assms unfolding mod_ring_def ring_of_def by simp
moreover have "nat (fst (bezout_coefficients (int x) (int n)) mod int n) < n"
using assms by (subst nat_less_iff) auto
hence "x ¯⇩C⇘mod_ring n⇙ ∈ carrier (ring_of (mod_ring n))"
using assms unfolding mod_ring_def ring_of_def by simp
moreover have "x ∈ carrier (ring_of (mod_ring n))" using a by auto
ultimately show "x ¯⇩C⇘mod_ring n⇙ = inv⇘ring_of (mod_ring n)⇙ x"
by (intro comm_inv_char[symmetric])
qed

lemma mod_ring_is_field_c:
assumes"Factorial_Ring.prime p"
shows "field⇩C (mod_ring p)"
unfolding field⇩C_def domain⇩C_def
by (intro conjI mod_ring_is_ring_c mod_ring_is_field assms prime_gt_1_nat
domain.axioms(1) field.axioms(1))

lemma mod_ring_is_enum_c:
shows "enum⇩C (mod_ring n)"
by (intro enum_cI) (simp_all add:mod_ring_def ring_of_def Coset.order_def lessThan_def)

end```