Theory GF_p
section ‹The prime fields ‹GF(p) = ℤ/pℤ››
theory GF_p
imports Ring_Theory Poly_Ring Poly_Ideal "HOL-Computational_Algebra.Primes"
begin
subsection ‹The residue rings ‹ℤ/nℤ››
text ‹‹Ring_Theory› suppresses HOL's arithmetic notation; restore it locally for the modular
arithmetic below.›
notation plus (infixl ‹+› 65)
notation minus (infixl ‹-› 65)
unbundle uminus_syntax
text ‹For any @{term "n > 1"}, the integers modulo @{term n} form a commutative ring: carrier
@{term "{0..<n}"} of @{typ nat}, arithmetic modulo @{term n}. This is the abstract residue ring
‹ℤ/nℤ›; when @{term n} is prime it is in fact a field, developed in ‹GF_p›. The bound
@{term "n > 1"} ensures both @{term 0} and @{term 1} lie in @{term "{0..<n}"} and are distinct
in @{typ nat}; the trivial ring case @{term "n = 1"} is not modelled by this carrier.›
definition gfp_add :: "nat ⇒ nat ⇒ nat ⇒ nat"
where "gfp_add n x y = (x + y) mod n"
definition gfp_mult :: "nat ⇒ nat ⇒ nat ⇒ nat"
where "gfp_mult n x y = (x * y) mod n"
context
fixes n :: nat
assumes n_gt_1: "n > 1"
begin
lemma n_gt_0: "n > 0" using n_gt_1 by simp
text ‹Closure: results of modular arithmetic land in @{term "{0..<n}"}.›
lemma gfp_add_closed [simp]: "gfp_add n x y ∈ {0..<n}"
using n_gt_0 by (simp add: gfp_add_def)
lemma gfp_mult_closed [simp]: "gfp_mult n x y ∈ {0..<n}"
using n_gt_0 by (simp add: gfp_mult_def)
lemma zero_mem: "(0::nat) ∈ {0..<n}" and one_mem: "(1::nat) ∈ {0..<n}"
using n_gt_1 by auto
text ‹The additive part is an abelian group: associative and commutative modular addition, with
@{term "n - x"} (reduced) as the inverse of @{term x}.›
lemma gfp_add_group: "Group {0..<n} (gfp_add n) 0"
proof (rule GroupI)
show "⋀x y z. ⟦ x ∈ {0..<n}; y ∈ {0..<n}; z ∈ {0..<n} ⟧
⟹ gfp_add n (gfp_add n x y) z = gfp_add n x (gfp_add n y z)"
by (simp add: gfp_add_def mod_add_left_eq mod_add_right_eq add.assoc)
next
fix x assume x: "x ∈ {0..<n}"
then have key: "(x + (n - x) mod n) mod n = 0"
by (simp_all add: mod_add_right_eq)
then show "∃y∈{0..<n}. gfp_add n x y = 0 ∧ gfp_add n y x = 0"
by (metis add.commute add.right_neutral gfp_add_closed gfp_add_def)
qed (use zero_mem n_gt_0 in ‹simp_all add: add.commute gfp_add_def›)
lemma gfp_add_commutative_monoid: "commutative_monoid {0..<n} (gfp_add n) 0"
unfolding commutative_monoid_def
by (metis Group_def add.commute commutative_monoid_axioms.intro gfp_add_def gfp_add_group)
lemma gfp_additive: "Abelian_Group {0..<n} (gfp_add n) 0"
by (rule Abelian_Group.intro [OF gfp_add_group gfp_add_commutative_monoid])
text ‹The multiplicative part is a commutative monoid with unit @{term 1}.›
lemma gfp_multiplicative: "commutative_monoid {0..<n} (gfp_mult n) 1"
proof
show "⋀x y z. ⟦ x ∈ {0..<n}; y ∈ {0..<n}; z ∈ {0..<n} ⟧
⟹ gfp_mult n (gfp_mult n x y) z = gfp_mult n x (gfp_mult n y z)"
by (simp add: gfp_mult_def mod_mult_left_eq mod_mult_right_eq mult.assoc)
qed (use one_mem n_gt_1 in ‹simp_all add: mult.commute gfp_mult_def›)
lemma zfact_ring: "Ring {0..<n} (gfp_add n) (gfp_mult n) 0 1"
proof (intro Ring.intro gfp_additive)
show "Monoid {0..<n} (gfp_mult n) 1"
by (rule commutative_monoid.axioms(1) [OF gfp_multiplicative])
show "Ring_axioms {0..<n} (gfp_add n) (gfp_mult n)"
by unfold_locales
(simp_all add: gfp_add_def gfp_mult_def mod_mult_left_eq mod_mult_right_eq
add_mult_distrib add_mult_distrib2 mod_add_left_eq mod_add_right_eq)
qed
lemma zfact_commutative_ring: "commutative_ring {0..<n} (gfp_add n) (gfp_mult n) 0 1"
by (rule commutative_ring.intro [OF zfact_ring gfp_multiplicative])
text ‹The residue ring @{text "ℤ/nℤ"} has exactly @{term n} elements.›
lemma card_zfact: "card {0..<n} = n" by simp
end
text ‹Hence, for every @{term "n > 1"}, the locale @{locale commutative_ring} is non-vacuous with
a witness of cardinality @{term n}.›
subsection ‹The residue ring as a field›
text ‹For a prime @{term p}, the residue ring ‹ZFact› becomes a field:
the only extra step over the general @{term "n > 0"} case is that every nonzero residue has a
multiplicative inverse, which follows from Bézout's identity since @{term p} is prime.
Carrier @{term "{0..<p}"} of @{typ nat}, arithmetic modulo @{term p}, arithmetic operations
@{const gfp_add} and @{const gfp_mult} shared with the ring-level development in @{text ZFact}.›
context
fixes p :: nat
assumes prime_p: "prime p"
begin
lemma p_gt_1: "p > 1" using prime_p by (simp add: prime_nat_iff)
lemma p_gt_0: "p > 0" using p_gt_1 by simp
text ‹∗‹Inverses.› For @{term "a ∈ {1..<p}"}, @{term a} is coprime to the prime @{term p}, so
Bézout gives integers with @{text "u⋅a + v⋅p = 1"}; reducing @{text "u"} modulo @{term p}
yields a multiplicative inverse of @{term a}.›
lemma gfp_inverse_exists:
assumes a: "a ∈ {0..<p}" and anz: "a ≠ 0"
shows "∃b∈{0..<p}. gfp_mult p a b = 1"
proof -
have ap: "a < p" and a1: "a ≥ 1" using a anz by auto
have ndvd: "¬ p dvd a" using ap anz by (simp add: nat_dvd_not_less)
then have "gcd a p = 1"
by (metis gcd_unique prime_nat_iff prime_p)
then have cop: "coprime (int a) (int p)" by (simp add: coprime_iff_gcd_eq_1)
obtain u v :: int where uv: "u * int a + v * int p = 1"
using cop bezout_int by (metis coprime_imp_gcd_eq_1)
define b where "b = nat (u mod int p)"
have brange: "b ∈ {0..<p}" using p_gt_0 by (simp add: b_def) (simp add: nat_less_iff)
have "int (gfp_mult p a b) = (int a * u) mod int p"
by (simp add: b_def gfp_mult_def mod_mult_right_eq of_nat_mod p_gt_0)
also have "… = (1 - v * int p + v * int p) mod int p"
by (metis diff_add_cancel mod_mult_self1 mult.commute uv)
also have "… = 1" using p_gt_1 by simp
finally show ?thesis using brange
using of_nat_eq_1_iff by blast
qed
lemma gfp_field: "Field {0..<p} (gfp_add p) (gfp_mult p) 0 1"
proof -
interpret R: commutative_ring "{0..<p}" "gfp_add p" "gfp_mult p" 0 1
using zfact_commutative_ring[OF p_gt_1] .
show ?thesis
proof
show "(1::nat) ≠ 0" using p_gt_1 by simp
show "⋀a. a ∈ {0..<p} ⟹ a ≠ 0 ⟹ R.multiplicative.invertible a"
by (metis R.multiplicative.invertibleI gfp_inverse_exists gfp_mult_def mult.commute)
qed
qed
text ‹The prime field has exactly @{term p} elements.›
lemma card_gfp: "card {0..<p} = p" by simp
end
text ‹Hence prime fields of every prime order exist --- in particular the @{locale Field} locale is
non-vacuous for every prime cardinality.›
subsection ‹The two-element field as a non-vacuity witness›
text ‹
A concrete field with two elements, witnessing that the @{locale Field} and
@{locale integral_domain} locales (and hence the abstract @{typ "'a ring"} type as a
field) are non-vacuous. Carrier @{term "{0, 1}"} of @{typ nat}.
›
definition gf2_add :: "nat ⇒ nat ⇒ nat" where "gf2_add x y ≡ (x + y) mod 2"
definition gf2_mult :: "nat ⇒ nat ⇒ nat" where "gf2_mult x y ≡ (x * y) mod 2"
text ‹Enumeration helper: membership in the two-element carrier.›
lemma gf2_cases: "x ∈ {0, 1::nat} ⟹ x = 0 ∨ x = 1" by auto
lemma gf2_add_simps [simp]:
"gf2_add 0 0 = 0" "gf2_add 0 1 = 1" "gf2_add 1 0 = 1" "gf2_add 1 1 = 0"
by (simp_all add: gf2_add_def)
lemma gf2_mult_simps [simp]:
"gf2_mult 0 0 = 0" "gf2_mult 0 1 = 0" "gf2_mult 1 0 = 0" "gf2_mult 1 1 = 1"
by (simp_all add: gf2_mult_def)
lemma gf2_add_closed [simp]: "⟦ x ∈ {0,1::nat}; y ∈ {0,1} ⟧ ⟹ gf2_add x y ∈ {0,1}"
by (auto simp: gf2_add_def)
lemma gf2_mult_closed [simp]: "⟦ x ∈ {0,1::nat}; y ∈ {0,1} ⟧ ⟹ gf2_mult x y ∈ {0,1}"
by (auto simp: gf2_mult_def)
text ‹The additive part is a group (each element is its own inverse), via @{thm [source] GroupI}.›
lemma gf2_add_group: "Group {0, 1::nat} gf2_add 0"
proof (rule GroupI)
fix u :: nat assume u: "u ∈ {0,1}"
then have "gf2_add u u = 0" by (auto simp: gf2_add_def)
with u show "∃v ∈ {0,1::nat}. gf2_add u v = 0 ∧ gf2_add v u = 0" by blast
qed (auto simp: gf2_add_def)
lemma gf2_add_commutative_monoid: "commutative_monoid {0, 1::nat} gf2_add 0"
by unfold_locales (auto simp: gf2_add_def)
text ‹The additive part is therefore an abelian group.›
lemma gf2_additive: "Abelian_Group {0, 1::nat} gf2_add 0"
by (rule Abelian_Group.intro [OF gf2_add_group gf2_add_commutative_monoid])
text ‹The multiplicative part is a commutative monoid.›
lemma gf2_multiplicative: "commutative_monoid {0, 1::nat} gf2_mult 1"
by unfold_locales (auto simp: gf2_mult_def)
lemma gf2_ring: "Ring {0, 1::nat} gf2_add gf2_mult 0 1"
proof (rule Ring.intro)
show "Abelian_Group {0,1::nat} gf2_add 0" by (rule gf2_additive)
show "Monoid {0,1::nat} gf2_mult 1" by (rule commutative_monoid.axioms(1) [OF gf2_multiplicative])
show "Ring_axioms {0,1::nat} gf2_add gf2_mult" by unfold_locales (auto simp: gf2_add_def gf2_mult_def)
qed
lemma gf2_commutative_ring: "commutative_ring {0, 1::nat} gf2_add gf2_mult 0 1"
by (rule commutative_ring.intro [OF gf2_ring gf2_multiplicative])
text ‹The two-element field. This is the single witness the downstream constructions consume (via
‹interpretation … by (rule gf2_field)› in ‹GF4› and ‹GF8›); it also witnesses non-vacuity of the
@{locale Field}, @{locale integral_domain} and @{locale commutative_ring} locales, the last two by
the locale hierarchy (a @{locale Field} is in particular an @{locale integral_domain}).›
lemma gf2_field: "Field {0, 1::nat} gf2_add gf2_mult 0 1"
proof -
interpret R: commutative_ring "{0,1::nat}" gf2_add gf2_mult 0 1 by (rule gf2_commutative_ring)
show ?thesis
proof
show "(1::nat) ≠ 0" by simp
next
fix a :: nat assume a: "a ∈ {0,1}" "a ≠ 0"
then have a1: "a = 1" by auto
then have "gf2_mult a a = 1" by (simp add: gf2_mult_def)
then show "R.multiplicative.invertible a"
using a1 by (intro R.multiplicative.invertibleI [where v = a]) auto
qed
qed
subsection ‹The two-element field with polynomial machinery›