Mathematical logic seminar - March 24, 2009

Time: 12:00 - 13:20

Room: Baker Hall 150

Speaker:     Amine Chaieb    
Department of Computer Science
TU Munich

Title: 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.