Generalizing a Mathematical Analysis Library in Isabelle/HOL

  • Jesús Aransay
  • Jose DivasónEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)


The HOL Multivariate Analysis Library (HMA) of Isabelle/HOL is focused on concrete types such as \(\mathbb {R}\), \(\mathbb {C}\) and \(\mathbb {R}^n\) and on algebraic structures such as real vector spaces and Euclidean spaces, represented by means of type classes. The generalization of HMA to more abstract algebraic structures is something desirable but it has not been tackled yet. Using that library, we were able to prove the Gauss-Jordan algorithm over real matrices, but our interest lied on generating verified code for matrices over arbitrary fields, greatly increasing the range of applications of such an algorithm. This short paper presents the steps that we did and the methodology that we devised to generalize such a library, which were successful to generalize the Gauss-Jordan algorithm to matrices over arbitrary fields.


Theorem proving Isabelle/HOL Type classes Linear Algebra 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Harrison, J.: The HOL Light Theory of Euclidean Space. J. Autom. Reasoning. 50(2), 173–190 (2013)CrossRefzbMATHGoogle Scholar
  2. 2.
    Heras, J., Dénès, M., Mata, G., Mörtberg, A., Poza, M., Siles, V.: Towards a certified computation of homology groups for digital images. In: Ferri, M., Frosini, P., Landi, C., Cerri, A., Di Fabio, B. (eds.) CTIC 2012. LNCS, vol. 7309, pp. 49–57. Springer, Heidelberg (2012) CrossRefGoogle Scholar
  3. 3.
    Avigad, J., Hölzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. CoRR (2014)Google Scholar
  4. 4.
    Hölzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle/HOL. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 279–294. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  5. 5.
  6. 6.
    Axler, S.: Linear Algebra Done Right, 2nd edn. Springer (2004)Google Scholar
  7. 7.
    Strang, G.: Introduction to Linear Algebra. Wellesley - Cambridge Press (2009)Google Scholar
  8. 8.
    Aransay, J., Divasón, J.: Rank-Nullity Theorem in Linear Algebra. AFP (2013)Google Scholar
  9. 9.
    Mackiw, G.: A Note on the Equality of the Column and Row Rank of a Matrix. Mathematics Magazine 68(4), 285–286 (1995)CrossRefzbMATHMathSciNetGoogle Scholar
  10. 10.
    Aransay, J., Divasón, J.: Gauss-Jordan Algorithm and its Applications. AFP (2014)Google Scholar
  11. 11.
  12. 12.
    Durán, A.J., Pérez, M., Varona, J.L.: The Misfortunes of a Trio of Mathematicians Using Computer Algebra Systems. Can We Trust in Them? Notices of the AMS 51(10), 1249–1252 (2014)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Departamento de Matemáticas y ComputaciónUniversidad de La RiojaLogroñoSpain

Personalised recommendations