Theory Finite_Field

```(*
Authors:      Jose Divasón
Sebastiaan Joosten
René Thiemann
Akihisa Yamada
*)
section ‹Finite Rings and Fields›

text ‹We start by establishing some preliminary results about finite rings and finite fields›

subsection ‹Finite Rings›

theory Finite_Field
imports
"HOL-Computational_Algebra.Primes"
"HOL-Number_Theory.Residues"
"HOL-Library.Cardinality"
Subresultants.Binary_Exponentiation
Polynomial_Interpolation.Ring_Hom_Poly
begin

typedef ('a::finite) mod_ring = "{0..<int CARD('a)}" by auto

setup_lifting type_definition_mod_ring

lemma CARD_mod_ring[simp]: "CARD('a mod_ring) = CARD('a::finite)"
proof -
have "card {y. ∃x∈{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} = card {0..<int CARD('a)}"
proof (rule bij_betw_same_card)
have "inj_on Rep_mod_ring {y. ∃x∈{0..<int CARD('a)}. y = Abs_mod_ring x}"
by (meson Rep_mod_ring_inject inj_onI)
moreover have "Rep_mod_ring ` {y. ∃x∈{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x} = {0..<int CARD('a)}"
proof (auto simp add: image_def Rep_mod_ring_inject)
fix xb show "0 ≤ Rep_mod_ring (Abs_mod_ring xb)"
using Rep_mod_ring atLeastLessThan_iff by blast
assume xb1: "0 ≤ xb" and xb2: "xb < int CARD('a)"
thus " Rep_mod_ring (Abs_mod_ring xb) < int CARD('a)"
by (metis Abs_mod_ring_inverse Rep_mod_ring atLeastLessThan_iff le_less_trans linear)
have xb: "xb ∈ {0..<int CARD('a)}" using xb1 xb2 by simp
show "∃xa::'a mod_ring. (∃x∈{0..<int CARD('a)}. xa = Abs_mod_ring x) ∧ xb = Rep_mod_ring xa"
by (rule exI[of _ "Abs_mod_ring xb"], auto simp add: xb1 xb2, rule Abs_mod_ring_inverse[OF xb, symmetric])
qed
ultimately show "bij_betw Rep_mod_ring
{y. ∃x∈{0..<int CARD('a)}. (y::'a mod_ring) = Abs_mod_ring x}
{0..<int CARD('a)}"
by (simp add: bij_betw_def)
qed
thus ?thesis
unfolding type_definition.univ[OF type_definition_mod_ring]
unfolding image_def by auto
qed

instance mod_ring :: (finite) finite
proof (intro_classes)
show "finite (UNIV::'a mod_ring set)"
unfolding type_definition.univ[OF type_definition_mod_ring]
using finite by simp
qed

instantiation mod_ring :: (finite) equal
begin
lift_definition equal_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ bool" is "(=)" .
instance by (intro_classes, transfer, auto)
end

instantiation mod_ring :: (finite) comm_ring
begin

lift_definition plus_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" is
"λ x y. (x + y) mod int (CARD('a))" by simp

lift_definition uminus_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" is
"λ x. if x = 0 then 0 else int (CARD('a)) - x" by simp

lift_definition minus_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" is
"λ x y. (x - y) mod int (CARD('a))" by simp

lift_definition times_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" is
"λ x y. (x * y) mod int (CARD('a))" by simp

lift_definition zero_mod_ring :: "'a mod_ring" is 0 by simp

instance
by standard
(transfer; auto simp add: mod_simps algebra_simps intro: mod_diff_cong)+

end

lift_definition to_int_mod_ring :: "'a::finite mod_ring ⇒ int" is "λ x. x" .

lift_definition of_int_mod_ring :: "int ⇒ 'a::finite mod_ring" is
"λ x. x mod int (CARD('a))" by simp

interpretation to_int_mod_ring_hom: inj_zero_hom to_int_mod_ring
by (unfold_locales; transfer, auto)

lemma int_nat_card[simp]: "int (nat CARD('a::finite)) = CARD('a)" by auto

interpretation of_int_mod_ring_hom: zero_hom of_int_mod_ring
by (unfold_locales, transfer, auto)

lemma of_int_mod_ring_to_int_mod_ring[simp]:
"of_int_mod_ring (to_int_mod_ring x) = x" by (transfer, auto)

lemma to_int_mod_ring_of_int_mod_ring[simp]: "0 ≤ x ⟹ x < int CARD('a :: finite) ⟹
to_int_mod_ring (of_int_mod_ring x :: 'a mod_ring) = x"
by (transfer, auto)

lemma range_to_int_mod_ring:
"range (to_int_mod_ring :: ('a :: finite mod_ring ⇒ int)) = {0 ..< CARD('a)}"
apply (intro equalityI subsetI)
apply (elim rangeE, transfer, force)
by (auto intro!: range_eqI to_int_mod_ring_of_int_mod_ring[symmetric])

subsection ‹Nontrivial Finite Rings›

class nontriv = assumes nontriv: "CARD('a) > 1"

subclass(in nontriv) finite by(intro_classes,insert nontriv,auto intro:card_ge_0_finite)

instantiation mod_ring :: (nontriv) comm_ring_1
begin

lift_definition one_mod_ring :: "'a mod_ring" is 1 using nontriv[where ?'a='a] by auto

instance by (intro_classes; transfer, simp)

end

interpretation to_int_mod_ring_hom: inj_one_hom to_int_mod_ring
by (unfold_locales, transfer, simp)

lemma of_nat_of_int_mod_ring [code_unfold]:
"of_nat = of_int_mod_ring o int"
proof (rule ext, unfold o_def)
show "of_nat n = of_int_mod_ring (int n)" for n
proof (induct n)
case (Suc n)
show ?case
by (simp only: of_nat_Suc Suc, transfer) (simp add: mod_simps)
qed simp
qed

lemma of_nat_card_eq_0[simp]: "(of_nat (CARD('a::nontriv)) :: 'a mod_ring) = 0"
by (unfold of_nat_of_int_mod_ring, transfer, auto)

lemma of_int_of_int_mod_ring[code_unfold]: "of_int = of_int_mod_ring"
proof (rule ext)
fix x :: int
obtain n1 n2 where x: "x = int n1 - int n2" by (rule int_diff_cases)
show "of_int x = of_int_mod_ring x"
unfolding x of_int_diff of_int_of_nat_eq of_nat_of_int_mod_ring o_def
by (transfer, simp add: mod_diff_right_eq mod_diff_left_eq)
qed

unbundle lifting_syntax

lemma pcr_mod_ring_to_int_mod_ring: "pcr_mod_ring = (λx y. x = to_int_mod_ring y)"
unfolding mod_ring.pcr_cr_eq unfolding cr_mod_ring_def to_int_mod_ring.rep_eq ..

lemma [transfer_rule]:
"((=) ===> pcr_mod_ring) (λ x. int x mod int (CARD('a :: nontriv))) (of_nat :: nat ⇒ 'a mod_ring)"
by (intro rel_funI, unfold pcr_mod_ring_to_int_mod_ring of_nat_of_int_mod_ring, transfer, auto)

lemma [transfer_rule]:
"((=) ===> pcr_mod_ring) (λ x. x mod int (CARD('a :: nontriv))) (of_int :: int ⇒ 'a mod_ring)"
by (intro rel_funI, unfold pcr_mod_ring_to_int_mod_ring of_int_of_int_mod_ring, transfer, auto)

lemma one_mod_card [simp]: "1 mod CARD('a::nontriv) = 1"
using mod_less nontriv by blast

lemma Suc_0_mod_card [simp]: "Suc 0 mod CARD('a::nontriv) = 1"
using one_mod_card by simp

lemma one_mod_card_int [simp]: "1 mod int CARD('a::nontriv) = 1"
proof -
from nontriv [where ?'a = 'a] have "int (1 mod CARD('a::nontriv)) = 1"
by simp
then show ?thesis
using of_nat_mod [of 1 "CARD('a)", where ?'a = int] by simp
qed

lemma pow_mod_ring_transfer[transfer_rule]:
"(pcr_mod_ring ===> (=) ===> pcr_mod_ring)
(λa::int. λn. a^n mod CARD('a::nontriv)) ((^)::'a mod_ring ⇒ nat ⇒ 'a mod_ring)"
unfolding pcr_mod_ring_to_int_mod_ring
proof (intro rel_funI,simp)
fix x::"'a mod_ring" and n
show "to_int_mod_ring x ^ n mod int CARD('a) = to_int_mod_ring (x ^ n)"
proof (induct n)
case 0
thus ?case by auto
next
case (Suc n)
have "to_int_mod_ring (x ^ Suc n) = to_int_mod_ring (x * x ^ n)" by auto
also have "... = to_int_mod_ring x * to_int_mod_ring (x ^ n) mod CARD('a)"
unfolding to_int_mod_ring_def using times_mod_ring.rep_eq by auto
also have "... = to_int_mod_ring x * (to_int_mod_ring x ^ n mod CARD('a)) mod CARD('a)"
using Suc.hyps by auto
also have "... = to_int_mod_ring x ^ Suc n mod int CARD('a)"
by (simp add: mod_simps)
finally show ?case ..
qed
qed

lemma dvd_mod_ring_transfer[transfer_rule]:
"((pcr_mod_ring :: int ⇒ 'a :: nontriv mod_ring ⇒ bool) ===>
(pcr_mod_ring :: int ⇒ 'a mod_ring ⇒ bool) ===> (=))
(λ i j. ∃k ∈ {0..<int CARD('a)}. j = i * k mod int CARD('a)) (dvd)"
proof (unfold pcr_mod_ring_to_int_mod_ring, intro rel_funI iffI)
fix x y :: "'a mod_ring" and i j
assume i: "i = to_int_mod_ring x" and j: "j = to_int_mod_ring y"
{ assume "x dvd y"
then obtain z where "y = x * z" by (elim dvdE, auto)
then have "j = i * to_int_mod_ring z mod CARD('a)" by (unfold i j, transfer)
with range_to_int_mod_ring
show "∃k ∈ {0..<int CARD('a)}. j = i * k mod CARD('a)" by auto
}
assume "∃k ∈ {0..<int CARD('a)}. j = i * k mod CARD('a)"
then obtain k where k: "k ∈ {0..<int CARD('a)}" and dvd: "j = i * k mod CARD('a)" by auto
from k have "to_int_mod_ring (of_int k :: 'a mod_ring) = k" by (transfer, auto)
also from dvd have "j = i * ... mod CARD('a)" by auto
finally have "y = x * (of_int k :: 'a mod_ring)" unfolding i j using k by (transfer, auto)
then show "x dvd y" by auto
qed

lemma Rep_mod_ring_mod[simp]: "Rep_mod_ring (a :: 'a :: nontriv mod_ring) mod CARD('a) = Rep_mod_ring a"
using Rep_mod_ring[where 'a = 'a] by auto

subsection ‹Finite Fields›

text ‹When the domain is prime, the ring becomes a field›

class prime_card = assumes prime_card: "prime (CARD('a))"
begin
lemma prime_card_int: "prime (int (CARD('a)))" using prime_card by auto

subclass nontriv using prime_card prime_gt_1_nat by (intro_classes,auto)
end

instance bool :: prime_card
by standard auto

instantiation mod_ring :: (prime_card) field
begin

definition inverse_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" where
"inverse_mod_ring x = (if x = 0 then 0 else x ^ (nat (CARD('a) - 2)))"

definition divide_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring"  where
"divide_mod_ring x y = x * ((λc. if c = 0 then 0 else c ^ (nat (CARD('a) - 2))) y)"

instance
proof
fix a b c::"'a mod_ring"
show "inverse 0 = (0::'a mod_ring)" by (simp add: inverse_mod_ring_def)
show "a div b = a * inverse b"
unfolding inverse_mod_ring_def by (transfer', simp add: divide_mod_ring_def)
show "a ≠ 0 ⟹ inverse a * a = 1"
proof (unfold inverse_mod_ring_def, transfer)
let ?p="CARD('a)"
fix x
assume x: "x ∈ {0..<int CARD('a)}" and x0: "x ≠ 0"
have p0': "0≤?p" by auto
have "¬ ?p dvd x"
using x x0 zdvd_imp_le by fastforce
then have "¬ CARD('a) dvd nat ¦x¦"
by simp
with x have "¬ CARD('a) dvd nat x"
by simp
have rw: "x ^ nat (int (?p - 2)) * x = x ^ nat (?p - 1)"
proof -
have p2: "0 ≤ int (?p-2)" using x by simp
have card_rw: "(CARD('a) - Suc 0) = nat (1 + int (CARD('a) - 2))"
using nat_eq_iff x x0 by auto
have "x ^ nat (?p - 2)*x = x ^ (Suc (nat (?p - 2)))" by simp
also have "... = x ^ (nat (?p - 1))"
using Suc_nat_eq_nat_zadd1[OF p2] card_rw by auto
finally show ?thesis .
qed
have "[int (nat x ^ (CARD('a) - 1)) = int 1] (mod CARD('a))"
using fermat_theorem [OF prime_card ‹¬ CARD('a) dvd nat x›]
by (simp only: cong_def cong_def of_nat_mod [symmetric])
then have *: "[x ^ (CARD('a) - 1) = 1] (mod CARD('a))"
using x by auto
have "x ^ (CARD('a) - 2) mod CARD('a) * x mod CARD('a)
= (x ^ nat (CARD('a) - 2) * x) mod CARD('a)" by (simp add: mod_simps)
also have "... =  (x ^ nat (?p - 1) mod ?p)" unfolding rw by simp
also have "... = (x ^ (nat ?p - 1) mod ?p)" using p0' by (simp add: nat_diff_distrib')
also have "... = 1"
using * by (simp add: cong_def)
finally show "(if x = 0 then 0 else x ^ nat (int (CARD('a) - 2)) mod CARD('a)) * x mod CARD('a) = 1"
using x0 by auto
qed
qed
end

instantiation mod_ring :: (prime_card) "{normalization_euclidean_semiring, euclidean_ring}"
begin

definition modulo_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" where "modulo_mod_ring x y = (if y = 0 then x else 0)"
definition normalize_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" where "normalize_mod_ring x = (if x = 0 then 0 else 1)"
definition unit_factor_mod_ring :: "'a mod_ring ⇒ 'a mod_ring" where "unit_factor_mod_ring x = x"
definition euclidean_size_mod_ring :: "'a mod_ring ⇒ nat" where "euclidean_size_mod_ring x = (if x = 0 then 0 else 1)"

instance
proof (intro_classes)
fix a :: "'a mod_ring" show "a ≠ 0 ⟹ unit_factor a dvd 1"
unfolding dvd_def unit_factor_mod_ring_def by (intro exI[of _ "inverse a"], auto)
qed (auto simp: normalize_mod_ring_def unit_factor_mod_ring_def modulo_mod_ring_def
euclidean_size_mod_ring_def field_simps)
end

instantiation mod_ring :: (prime_card) euclidean_ring_gcd
begin

definition gcd_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" where "gcd_mod_ring = Euclidean_Algorithm.gcd"
definition lcm_mod_ring :: "'a mod_ring ⇒ 'a mod_ring ⇒ 'a mod_ring" where "lcm_mod_ring = Euclidean_Algorithm.lcm"
definition Gcd_mod_ring :: "'a mod_ring set ⇒ 'a mod_ring" where "Gcd_mod_ring = Euclidean_Algorithm.Gcd"
definition Lcm_mod_ring :: "'a mod_ring set ⇒ 'a mod_ring" where "Lcm_mod_ring = Euclidean_Algorithm.Lcm"

instance by (intro_classes, auto simp: gcd_mod_ring_def lcm_mod_ring_def Gcd_mod_ring_def Lcm_mod_ring_def)
end

instantiation mod_ring :: (prime_card) unique_euclidean_ring
begin

definition [simp]: "division_segment_mod_ring (x :: 'a mod_ring) = (1 :: 'a mod_ring)"

instance by intro_classes (auto simp: euclidean_size_mod_ring_def split: if_splits)

end

instance mod_ring :: (prime_card) field_gcd
by intro_classes auto

lemma surj_of_nat_mod_ring: "∃ i. i < CARD('a :: prime_card) ∧ (x :: 'a mod_ring) = of_nat i"
by (rule exI[of _ "nat (to_int_mod_ring x)"], unfold of_nat_of_int_mod_ring o_def,
subst nat_0_le, transfer, simp, simp, transfer, auto)

lemma of_nat_0_mod_ring_dvd: assumes x: "of_nat x = (0 :: 'a ::prime_card mod_ring)"
shows "CARD('a) dvd x"
proof -
let ?x = "of_nat x :: int"
from x have "of_int_mod_ring ?x = (0 :: 'a mod_ring)" by (fold of_int_of_int_mod_ring, simp)
hence "?x mod CARD('a) = 0" by (transfer, auto)
hence "x mod CARD('a) = 0" by presburger
thus ?thesis unfolding mod_eq_0_iff_dvd .
qed

lemma semiring_char_mod_ring [simp]:
"CHAR('n :: nontriv mod_ring) = CARD('n)"
proof (rule CHAR_eq_posI)
fix x assume "x > 0" "x < CARD('n)"
thus "of_nat x ≠ (0 :: 'n mod_ring)"
by transfer auto
qed auto

text ‹
The following Material was contributed by Manuel Eberl
›
instance mod_ring :: (prime_card) finite_field
by standard simp_all

instantiation mod_ring :: (prime_card) enum_finite_field
begin

definition enum_finite_field_mod_ring :: "nat ⇒ 'a mod_ring" where
"enum_finite_field_mod_ring n = of_int_mod_ring (int n)"

instance proof
interpret type_definition "Rep_mod_ring :: 'a mod_ring ⇒ int" Abs_mod_ring "{0..<CARD('a)}"
by (rule type_definition_mod_ring)
have "enum_finite_field ` {..<CARD('a mod_ring)} = of_int_mod_ring ` int ` {..<CARD('a mod_ring)}"
unfolding enum_finite_field_mod_ring_def by (simp add: image_image o_def)
also have "int ` {..<CARD('a mod_ring)} = {0..<int CARD('a mod_ring)}"
by (simp add: image_atLeastZeroLessThan_int)
also have "of_int_mod_ring ` … = (Abs_mod_ring ` … :: 'a mod_ring set)"
by (intro image_cong refl) (auto simp: of_int_mod_ring_def)
also have "… = (UNIV :: 'a mod_ring set)"
using Abs_image by simp
finally show "enum_finite_field ` {..<CARD('a mod_ring)} = (UNIV :: 'a mod_ring set)" .
qed

end

typedef (overloaded) 'a :: semiring_1 ring_char = "if CHAR('a) = 0 then UNIV else {0..<CHAR('a)}"
by auto

lemma CARD_ring_char [simp]: "CARD ('a :: semiring_1 ring_char) = CHAR('a)"
proof -
let ?A = "if CHAR('a) = 0 then UNIV else {0..<CHAR('a)}"
interpret type_definition "Rep_ring_char :: 'a ring_char ⇒ nat" Abs_ring_char ?A
by (rule type_definition_ring_char)
from card show ?thesis
by auto
qed

instance ring_char :: (semiring_prime_char) nontriv
proof
show "CARD('a ring_char) > 1"
using prime_nat_iff by auto
qed

instance ring_char :: (semiring_prime_char) prime_card
proof
from CARD_ring_char show "prime CARD('a ring_char)"
by auto
qed

lemma to_int_mod_ring_add:
"to_int_mod_ring (x + y :: 'a :: finite mod_ring) = (to_int_mod_ring x + to_int_mod_ring y) mod CARD('a)"
by transfer auto

lemma to_int_mod_ring_mult:
"to_int_mod_ring (x * y :: 'a :: finite mod_ring) = (to_int_mod_ring x * to_int_mod_ring y) mod CARD('a)"
by transfer auto

lemma of_nat_mod_CHAR [simp]: "of_nat (x mod CHAR('a :: semiring_1)) = (of_nat x :: 'a)"
by (metis (no_types, opaque_lifting) comm_monoid_add_class.add_0 div_mod_decomp
mult_zero_right of_nat_CHAR of_nat_add of_nat_mult)

lemma of_int_mod_CHAR [simp]: "of_int (x mod int CHAR('a :: ring_1)) = (of_int x :: 'a)"
by (simp add: of_int_eq_iff_cong_CHAR)

end
```