# Theory Finite_Fields.Finite_Fields_Indexed_Algebra_Code

```section ‹Executable Structures›

theory Finite_Fields_Indexed_Algebra_Code
imports "HOL-Algebra.Ring" "HOL-Algebra.Coset"
begin

text ‹In the following, we introduce records for executable operations for algebraic structures,
which can be used for code-generation and evaluation. These are then shown to be equivalent to the
(not-necessarily constructive) definitions using ▩‹HOL-Algebra›. A more direct approach, i.e.,
instantiating the structures in the framework with effective operations fails. For example the
structure records represent the domain of the algebraic structure as a set, which implies the
evaluation of @{term "(⊕⇘residue_ring (10^100)⇙)"} requires the construction of
@{term "{0..10^100-1}"}. This is technically constructive but very impractical.
Moreover, the additive/multiplicative inverse is defined non-constructively using the
description operator ▩‹THE› in ▩‹HOL-Algebra›.

The above could be avoided, if it were possible to introduce code equations conditionally, e.g.,
for example for @{term "a_inv (residue_ring n) x y"} (if @{term "x y"} are in the carrier of the
structure, but this does not seem to be possible.

Note that, the algebraic structures defined in ▩‹HOL-Computational_Algebra› are type-based,
which prevents using them in some algorithmic settings. For example, choosing an
irreducible polynomial dynamically and performing operations in the factoring ring with respect to
it is not possible in the type-based approach.›

record 'a idx_ring =
idx_pred :: "'a ⇒ bool"
idx_uminus :: "'a ⇒ 'a"
idx_plus :: "'a ⇒ 'a ⇒ 'a"
idx_udivide :: "'a ⇒ 'a"
idx_mult :: "'a ⇒ 'a ⇒ 'a"
idx_zero :: "'a"
idx_one :: "'a"

record 'a idx_ring_enum = "'a idx_ring" +
idx_size :: nat
idx_enum :: "nat ⇒ 'a"
idx_enum_inv :: "'a ⇒ nat"

fun idx_pow :: "('a,'b) idx_ring_scheme  ⇒ 'a ⇒ nat ⇒ 'a" where
"idx_pow E x 0 = idx_one E" |
"idx_pow E x (Suc n) = idx_mult E (idx_pow E x n) x"

bundle index_algebra_notation
begin
notation idx_zero ("0⇩Cı")
notation idx_one ("1⇩Cı")
notation idx_plus (infixl "+⇩Cı" 65)
notation idx_mult (infixl "*⇩Cı" 70)
notation idx_uminus ("-⇩Cı _" [81] 80)
notation idx_udivide ("_ ¯⇩Cı" [81] 80)
notation idx_pow  (infixr "^⇩Cı" 75)
end
unbundle index_algebra_notation

bundle no_index_algebra_notation
begin
no_notation idx_zero ("0⇩Cı")
no_notation idx_one ("1⇩Cı")
no_notation idx_plus (infixl "+⇩Cı" 65)
no_notation idx_mult (infixl "*⇩Cı" 70)
no_notation idx_uminus ("-⇩Cı _" [81] 80)
no_notation idx_udivide ("_ ¯⇩Cı" [81] 80)
no_notation idx_pow  (infixr "^⇩Cı" 75)
end

definition ring_of :: "('a,'b) idx_ring_scheme ⇒ 'a ring"
where "ring_of A = ⦇
carrier = {x. idx_pred A x},
mult = (λ x y. x *⇩C⇘A⇙ y),
one = 1⇩C⇘A⇙,
zero = 0⇩C⇘A⇙,
add = (λ x y. x +⇩C⇘A⇙ y) ⦈"

definition ring⇩C where
"ring⇩C A = (ring (ring_of A) ∧ (∀x. idx_pred A x ⟶ -⇩C⇘A⇙ x = ⊖⇘ring_of A⇙ x) ∧
(∀x. x ∈ Units (ring_of A) ⟶ x ¯⇩C⇘A⇙ = inv⇘ring_of A⇙ x))"

lemma ring_cD_aux:
"x ^⇩C⇘A⇙ n = x [^]⇘ring_of A⇙ n"
by (induction n) (auto simp:ring_of_def)

lemma ring_cD:
assumes "ring⇩C A"
shows
"0⇩C⇘A⇙ = 𝟬⇘ring_of A⇙"
"1⇩C⇘A⇙ = 𝟭⇘ring_of A⇙"
"⋀x y. x *⇩C⇘A⇙ y = x ⊗⇘ring_of A⇙ y"
"⋀x y. x +⇩C⇘A⇙ y = x ⊕⇘ring_of A⇙ y"
"⋀x. x ∈ carrier (ring_of A) ⟹  -⇩C⇘A⇙ x = ⊖⇘ring_of A⇙ x"
"⋀x. x ∈ Units (ring_of A) ⟹  x ¯⇩C⇘A⇙ = inv⇘ring_of A⇙ x"
"⋀x. x ^⇩C⇘A⇙ n = x [^]⇘ring_of A⇙ n"
using assms ring_cD_aux unfolding ring⇩C_def ring_of_def by auto

lemma ring_cI:
assumes "ring (ring_of A)"
assumes "⋀x. x ∈ carrier (ring_of A) ⟹  -⇩C⇘A⇙ x = ⊖⇘ring_of A⇙ x"
assumes "⋀x. x ∈ Units (ring_of A) ⟹  x¯⇩C⇘A⇙ = inv⇘ring_of A⇙ x"
shows "ring⇩C A"
proof -
have " x ∈ carrier (ring_of A) ⟷ idx_pred A x" for x unfolding ring_of_def by auto
thus ?thesis using assms unfolding ring⇩C_def by auto
qed

definition cring⇩C where "cring⇩C A = (ring⇩C A ∧ cring (ring_of A))"

lemma cring_cI:
assumes "cring (ring_of A)"
assumes "⋀x. x ∈ carrier (ring_of A) ⟹  -⇩C⇘A⇙ x = ⊖⇘ring_of A⇙ x"
assumes "⋀x. x ∈ Units (ring_of A) ⟹ x¯⇩C⇘A⇙ = inv⇘ring_of A⇙ x"
shows "cring⇩C A"
unfolding cring⇩C_def by (intro ring_cI conjI assms cring.axioms(1))

lemma cring_c_imp_ring: "cring⇩C A ⟹ ring⇩C A"
unfolding cring⇩C_def by simp

lemmas cring_cD = ring_cD[OF cring_c_imp_ring]

definition domain⇩C where "domain⇩C A = (cring⇩C A ∧ domain (ring_of A))"

lemma domain_cI:
assumes "domain (ring_of A)"
assumes "⋀x. x ∈ carrier (ring_of A) ⟹  -⇩C⇘A⇙ x = ⊖⇘ring_of A⇙ x"
assumes "⋀x. x ∈ Units (ring_of A) ⟹ x¯⇩C⇘A⇙ = inv⇘ring_of A⇙ x"
shows "domain⇩C A"
unfolding domain⇩C_def by (intro conjI cring_cI assms domain.axioms(1))

lemma domain_c_imp_ring: "domain⇩C A ⟹ ring⇩C A"
unfolding cring⇩C_def domain⇩C_def by simp

lemmas domain_cD = ring_cD[OF domain_c_imp_ring]

definition field⇩C where "field⇩C A = (domain⇩C A ∧ field (ring_of A))"

lemma field_cI:
assumes "field (ring_of A)"
assumes "⋀x. x ∈ carrier (ring_of A) ⟹  -⇩C⇘A⇙ x = ⊖⇘ring_of A⇙ x"
assumes "⋀x. x ∈ Units (ring_of A) ⟹  x¯⇩C⇘A⇙ = inv⇘ring_of A⇙ x"
shows "field⇩C A"
unfolding field⇩C_def by (intro conjI domain_cI assms field.axioms(1))

lemma field_c_imp_ring: "field⇩C A ⟹ ring⇩C A"
unfolding field⇩C_def cring⇩C_def domain⇩C_def by simp

lemmas field_cD = ring_cD[OF field_c_imp_ring]

definition enum⇩C where "enum⇩C A = (
finite (carrier (ring_of A)) ∧
idx_size A = order (ring_of A) ∧
bij_betw (idx_enum A) {..<order (ring_of A)} (carrier (ring_of A)) ∧
(∀x < order (ring_of A). idx_enum_inv A (idx_enum A x) = x))"

lemma enum_cI:
assumes "finite (carrier (ring_of A))"
assumes "idx_size A = order (ring_of A)"
assumes "bij_betw (idx_enum A) {..<order (ring_of A)} (carrier (ring_of A))"
assumes "⋀x. x < order (ring_of A) ⟹ idx_enum_inv A (idx_enum A x) = x"
shows "enum⇩C A"
using assms unfolding enum⇩C_def by auto

lemma enum_cD:
assumes "enum⇩C R"
shows "finite (carrier (ring_of R))"
and "idx_size R = order (ring_of R)"
and "bij_betw (idx_enum R) {..<order (ring_of R)} (carrier (ring_of R))"
and "bij_betw (idx_enum_inv R) (carrier (ring_of R)) {..<order (ring_of R)}"
and "⋀x. x < order (ring_of R) ⟹ idx_enum_inv R (idx_enum R x) = x"
and "⋀x. x ∈ carrier (ring_of R) ⟹ idx_enum R (idx_enum_inv R x) = x"
using assms
proof -
let ?n = "order (ring_of R)"
have a:"idx_enum_inv R x = the_inv_into {..<?n} (idx_enum R) x"
if x_carr: "x ∈ carrier (ring_of R)" for x
proof -
have "idx_enum R ` {..<order (ring_of R)} = carrier (ring_of R)"
using assms unfolding bij_betw_def enum⇩C_def by simp
then obtain y where y_carr: "y ∈ {..< order (ring_of R)}" and x_def: "x = idx_enum R y"
using x_carr by auto
have "idx_enum_inv R x = y" using assms y_carr unfolding x_def enum⇩C_def by simp
also have "... = the_inv_into {..<?n} (idx_enum R) x"
using assms unfolding bij_betw_def enum⇩C_def unfolding x_def
by (intro the_inv_into_f_f[symmetric] y_carr) auto
finally show ?thesis by simp
qed

have "bij_betw (the_inv_into {..<?n} (idx_enum R)) (carrier (ring_of R)) {..<?n}"
using assms unfolding enum⇩C_def by (intro bij_betw_the_inv_into) auto
thus "bij_betw (idx_enum_inv R) (carrier (ring_of R)) {..<order (ring_of R)}"
by (subst bij_betw_cong[OF a]) auto
show "idx_enum R (idx_enum_inv R x) = x" if "x ∈ carrier (ring_of R)" for x
using that assms unfolding a[OF that] enum⇩C_def bij_betw_def by (intro f_the_inv_into_f) auto
qed (use assms enum⇩C_def in auto)

end```