|Time:|| 12:00 - 13:20
Baker Hall 150
Department of Computer Science
Formal power series in Isabelle/HOL
We show how to use (axiomatic) type classes to formalize formal power series (FPS) over arbitrary domains. We prove that if the basic domain is an integral domain, then so is the FPS construction. We also formalize multiplicative inverses and division, arbitrary nth roots, composition of FPS and the compositional inverses. We present simple proofs and formalizations from Generatingfunctionology by Wilf and formalize some elementary FPS like the exponential, logarithmic, binomial, and some trigonometric series and some of their simple applications. From this formalization we immediately obtain (for free) the field of formal Laurent series and with minimal efforts a formalization of polynomials. All formalizations referred to above are univariate.