Abstract
Mathematical reasoning may involve several arithmetic types, including those of the natural, integer, rational, real, and complex numbers. These types satisfy many of the same algebraic laws. These laws need to be made available to users, uniformly and preferably without repetition, but with due account for the peculiarities of each type. Subtyping, where a type inherits properties from a supertype, can eliminate repetition only for a fixed type hierarchy set up in advance by implementors. The approach recently adopted for Isabelle uses axiomatic type classes, an established approach to overloading. Abstractions such as semirings, rings, fields, and their ordered counterparts are defined, and theorems are proved algebraically. Types that meet the abstractions inherit the appropriate theorems.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Farmer, W. M., Guttman, J. D. and Thayer, F. J.: IMPS: An interactive mathematical proof system, J. Automated Reasoning 11(2) (1993), 213–248.
Fleuriot, J. D. and Paulson, L. C.: Mechanizing nonstandard real analysis, LMS J. Comput. Math. 3 (2000), 140–190, http://www.lms.ac.uk/jcm/3/lms1999-027/.
Geuvers, H., Pollack, R., Wiedijk, F. and Zwanenburg, J.: A constructive algebraic hierarchy in Coq, J. Symbolic Comput. 34(4) (2002), 271–286.
Gordon, M. J. C. and Melham, T. F.: Introduction to HOL: A Theorem Proving Environment for Higher Order Logic, Cambridge University Press, 1993.
Hudak, P.: The Haskell School of Expression, Cambridge University Press, 2000.
Klein, G. and Nipkow, T.: Verified bytecode verifiers, Theoret. Comput. Sci. 298 (2003), 583–626.
Nipkow, T.: Order-sorted polymorphism in Isabelle, in G. Huet and G. Plotkin (eds.), Logical Environments, Cambridge University Press, 1993, pp. 164–188.
Nipkow, T., Paulson, L. C. and Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer, 2002.
Paulson, L. C.: ML for the Working Programmer, 2nd edn, Cambridge University Press, 1996.
Paulson, L. C.: Inductive analysis of the Internet protocol TLS, ACM Transactions on Information and System Security 2(3) (1999), 332–351.
The PVS standard prelude, http://pvs.csl.sri.com/doc/prelude.html, 2003.
Wadler, P. and Blott, S.: How to make ad-hoc polymorphism less ad hoc, in 16th Annual Symposium on Principles of Programming Languages, ACM Press, 1989, pp. 60–76.
Wenzel, M.: Type classes and overloading in higher-order logic, in E. L. Gunter and A. Felty (eds.), Theorem Proving in Higher Order Logics: TPHOLs ‘97, LNCS 1275, Springer, 1997, pp. 307–322.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Paulson, L.C. Organizing Numerical Theories Using Axiomatic Type Classes. J Autom Reasoning 33, 29–49 (2004). https://doi.org/10.1007/s10817-004-3997-6
Issue Date:
DOI: https://doi.org/10.1007/s10817-004-3997-6