Algebraic Numbers in Isabelle/HOL

René Thiemann and Akihisa Yamada

Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP 2016), Lecture Notes in Computer Science 9807, pp. 391 – 408, 2016.


We formalize algebraic numbers in Isabelle/HOL, based on existing libraries for matrices and Sturm’ s theorem. Our development serves as a verified implementation for real and complex numbers, and it admits to compute roots and completely factor real and complex polynomials, provided that all coefficients are rational numbers. Moreover, we provide two implementations to display algebraic numbers, an injective and expensive one, and a faster but approximative version.
To this end, we mechanize several results on resultants, which also required us to prove that polynomials over a unique factorization domain form again a unique factorization domain. We moreover formalize algorithms for factorization of integer polynomials: Newton interpolation, factorization over the integers, and Kronecker’ s factorization algorithm, as well as a
factorization oracle via Berlekamp’ s algorithm with the Hensel lifting.


  PDF |    doi:10.1007/978-3-319-43144-4_24  |  ©  Springer International Publishing Switzerland


author = "Ren{\'e} Thiemann and Akihisa Yamada",
title = "Algebraic Numbers in Isabelle/HOL",
booktitle = "Proceedings of the 7th International Conference on Interactive Theorem Proving",
editor = "Jasmin Christian Blanchette and Stephan Merz",
series = "Lecture Notes in Computer Science",
volume = 9807,
pages = "391--408",
year = 2016,
doi = "10.1007/978-3-319-43144-4_24"
Nach oben scrollen