Journal of Automated Reasoning

, Volume 47, Issue 3, pp 291–318 | Cite as

Formal Power Series



We present a formalization of the topological ring of formal power series in Isabelle/HOL. We also formalize formal derivatives, division, radicals, composition and reverses. As an application, we show how formal elementary and hyper-geometric series yield elegant proofs for some combinatorial identities. We easily derive a basic theory of polynomials. Then, using a generic formalization of the fraction field of an integral domain, we obtain formal Laurent series and rational functions for free.


Formalization of mathematics Theorem proving Formal power series Generating functions 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Chaieb, A.: Automated methods for formal proofs in simple arithmetics and algebra. Ph.D. thesis, Technische Universität München, Germany (2008)Google Scholar
  2. 2.
    Chaieb, A., Wenzel, M.: Context aware calculation and deduction—ring equalities via Gröbner bases in Isabelle. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) CALCULEMUS 2007. Lecture Notes in Computer Science, vol. 4573, pp. 27–39. Springer (2007)Google Scholar
  3. 3.
    Goulden, I.P., Jackson, D.M.: Combinatorial Enumeration. Dover Publications, Incorporated (2004)Google Scholar
  4. 4.
    Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics: a Foundation for Computer Science. Addison-Wesley, Boston (1994)MATHGoogle Scholar
  5. 5.
    Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs (2006)Google Scholar
  6. 6.
    Harrison, J.: Automating elementary number-theoretic proofs using Gröbner bases. In: Pfenning, F. (ed.) Proceedings of CADE 21. Lecture Notes in Computer Science, vol. 4603, pp. 51–66. Springer, Bremen, Germany (2007)Google Scholar
  7. 7.
    Henrici, P.: Applied and Computational Complex Analysis, vol. 1. Wiley, New York (1988)Google Scholar
  8. 8.
    Nipkow, T., Paulson, L.C.: Proof pearl: defining functions over finite sets. In: Hurd, J. (ed.) Theorem Proving in Higher Order Logics (TPHOLs 2005). Lecture Notes in Computer Science, vol. 3603, pp. 385–396. Springer (2005)Google Scholar
  9. 9.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL—A Proof Assistant for Higher-Order Logic. Lecture Notes in Computer Science, vol. 2283. Springer (2002)Google Scholar
  10. 10.
    Niven, I.: Formal power series. Am. Math. Mon. 76(8), 871–889 (1969)MathSciNetMATHCrossRefGoogle Scholar
  11. 11.
    Rudnicki, P., Trybulec, A.: Multivariate polynomials with arbitrary number of variables. Formaliz. Math. 11(1), 95–110 (1999)Google Scholar
  12. 12.
    Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A. (eds.) Theorem Proving in Higher Order Logics (TPHOLs ’97). Lecture Notes in Computer Science, vol. 1275 (1997)Google Scholar
  13. 13.
    Wenzel, M.: Isabelle/Isar—a versatile environment for human-readable formal proof documents. Ph.D. thesis, TU München. (2002)
  14. 14.
    Wilf, H.S.: Generatingfunctionology. Academic (1990)Google Scholar

Copyright information

© Springer Science+Business Media B.V. 2010

Authors and Affiliations

  1. 1.Computer LaboratoryUniversity of CambridgeCambridgeUK

Personalised recommendations