Theory 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 ("0Cı")
notation idx_one ("1Cı")
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 ("0Cı")
no_notation idx_one ("1Cı")
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 *CAy),
    one = 1CA,
    zero = 0CA,
    add = (λ x y. x +CAy) "

definition ringC where
  "ringC A = (ring (ring_of A)  (x. idx_pred A x  -CAx = ring_of Ax) 
    (x. x  Units (ring_of A)  x ¯CA= invring_of Ax))"

lemma ring_cD_aux:
  "x ^CAn = x [^]ring_of An"
  by (induction n) (auto simp:ring_of_def)

lemma ring_cD:
  assumes "ringC A"
  shows
    "0CA= 𝟬ring_of A⇙"
    "1CA= 𝟭ring_of A⇙"
    "x y. x *CAy = x ring_of Ay"
    "x y. x +CAy = x ring_of Ay"
    "x. x  carrier (ring_of A)   -CAx = ring_of Ax"
    "x. x  Units (ring_of A)   x ¯CA= invring_of Ax"
    "x. x ^CAn = x [^]ring_of An"
  using assms ring_cD_aux unfolding ringC_def ring_of_def by auto

lemma ring_cI:
  assumes "ring (ring_of A)"
  assumes "x. x  carrier (ring_of A)   -CAx = ring_of Ax"
  assumes "x. x  Units (ring_of A)   x¯CA= invring_of Ax"
  shows "ringC 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 ringC_def by auto
qed

definition cringC where "cringC A = (ringC A  cring (ring_of A))"

lemma cring_cI:
  assumes "cring (ring_of A)"
  assumes "x. x  carrier (ring_of A)   -CAx = ring_of Ax"
  assumes "x. x  Units (ring_of A)  x¯CA= invring_of Ax"
  shows "cringC A"
  unfolding cringC_def by (intro ring_cI conjI assms cring.axioms(1))

lemma cring_c_imp_ring: "cringC A  ringC A"
  unfolding cringC_def by simp

lemmas cring_cD = ring_cD[OF cring_c_imp_ring]

definition domainC where "domainC A = (cringC A  domain (ring_of A))"

lemma domain_cI:
  assumes "domain (ring_of A)"
  assumes "x. x  carrier (ring_of A)   -CAx = ring_of Ax"
  assumes "x. x  Units (ring_of A)  x¯CA= invring_of Ax"
  shows "domainC A"
  unfolding domainC_def by (intro conjI cring_cI assms domain.axioms(1))

lemma domain_c_imp_ring: "domainC A  ringC A"
  unfolding cringC_def domainC_def by simp

lemmas domain_cD = ring_cD[OF domain_c_imp_ring]

definition fieldC where "fieldC A = (domainC A  field (ring_of A))"

lemma field_cI:
  assumes "field (ring_of A)"
  assumes "x. x  carrier (ring_of A)   -CAx = ring_of Ax"
  assumes "x. x  Units (ring_of A)   x¯CA= invring_of Ax"
  shows "fieldC A"
  unfolding fieldC_def by (intro conjI domain_cI assms field.axioms(1))

lemma field_c_imp_ring: "fieldC A  ringC A"
  unfolding fieldC_def cringC_def domainC_def by simp

lemmas field_cD = ring_cD[OF field_c_imp_ring]

definition enumC where "enumC 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 "enumC A"
  using assms unfolding enumC_def by auto

lemma enum_cD:
  assumes "enumC 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 enumC_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 enumC_def by simp
    also have "... = the_inv_into {..<?n} (idx_enum R) x"
      using assms unfolding bij_betw_def enumC_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 enumC_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] enumC_def bij_betw_def by (intro f_the_inv_into_f) auto
qed (use assms enumC_def in auto)

end