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.›