Email Gateway (Aug 23 2022 at 09:12): Email Gateway (Aug 23 2022 at 09:12):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to present the following new AFP-entry.
All the best,
René
A verified algorithm for computing the Smith normal form of a matrix
by Jose Divasón
This work presents a formal proof in Isabelle/HOL of an algorithm to transform a
matrix into its Smith normal form, a canonical matrix form, in a general
setting: the algorithm is parameterized by operations to prove its existence
over elementary divisor rings, while execution is guaranteed over Euclidean
domains. We also provide a formal proof on some results about the generality of
this algorithm as well as the uniqueness of the Smith normal form. Since
Isabelle/HOL does not feature dependent types, the development is carried out
switching conveniently between two different existing libraries: the Hermite
normal form (based on HOL Analysis) and the Jordan normal form AFP entries. This
permits to reuse results from both developments and it is done by means of the
lifting and transfer package together with the use of local type definitions.
More details are available at:
https://www.isa-afp.org/entries/Smith_Normal_Form.html
Last updated: Apr 26 2024 at 16:20 UTC