Abstract
Isabelle/HOL has recently acquired new versions of definitional packages for inductive datatypes and primitive recursive functions. In contrast to its predecessors and most other implementations, Isabelle/HOL datatypes may be mutually and indirect recursive, even infinitely branching. We also support inverted datatype definitions for characterizing existing types as being inductive ones later. All our constructions are fully definitional according to established HOL tradition. Stepping back from the logical details, we also see this work as a typical example of what could be called “Formal-Logic Engineering”. We observe that building realistic theorem proving environments involves further issues rather than pure logic only.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
H. P. Barendregt. The quest for correctness. In Images of SMC Research, pages 39–58. Stichting Mathematisch Centrum, Amsterdam, 1996.
S. Berghofer. Definitorische Konstruktion induktiver Datentypen in Isabelle/HOL (in German). Master’s thesis, Technische Universität München, 1998.
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, pages 56–68, 1940.
C. Cornes, J. Courant, J.-C. Filliâtre, G. Huet, P. Manoury, and C. Muñoz. The Coq Proof Assistant User’s Guide, version 6.1. INRIA-Rocquencourt et CNRSENS Lyon, 1996.
M. J. C. Gordon and T. F. Melham (editors). Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
E. L. Gunter. Why we can’t have SML style datatype declarations in HOL. In L. J. M. Claesen and M. J. C. Gordon, editors, Higher Order Logic Theorem Proving and Its Applications, volume A-20 of IFIP Transactions, pages 561–568. North-Holland Press, 1992.
E. L. Gunter. A broader class of trees for recursive type definitions for HOL. In J. Joyce and C. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, volume 780 of LNCS, pages 141–154. Springer, 1994.
J. Harrison. Inductive definitions: automation and application. In P. J. Windley, T. Schubert, and J. Alves-Foss, editors, Higher Order Logic Theorem Proving and Its Applications: Proceedings of the 8th International Workshop, volume 971 of LNCS, pages 200–213, Aspen Grove, Utah, 1995. Springer.
J. Harrison. HOL done right. Unpublished draft, 1996.
U. Hensel and B. Jacobs. Proof principles for datatypes with iterated recursion. In E. Moggi and G. Rosolini, editors, Category Theory and Computer Science, volume 1290 of LNCS, pages 220–241. Springer, 1997.
F. Kammüller and M. Wenzel. Locales — a sectioning concept for Isabelle. Technical Report 449, University of Cambridge, Computer Laboratory, October 1998.
T. F. Melham. Automating recursive type definitions in higher order logic. In G. Birtwistle and P. A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving, pages 341–386. Springer, 1989.
W. Naraschewski and M. Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, volume 1479 of LNCS. Springer, 1998.
T. Nipkow and D. von Oheimb. Javalight is type-safe — definitely. In Proc. 25th ACM Symp. Principles of Programming Languages. ACM Press, New York, 1998.
S. Owre, S. Rajan, J. M. Rushby, N. Shankar, and M. Srivas. PVS: combining specification, proof checking, and model checking. In R. Alur and T. A. Henzinger, editors, Computer Aided Verification, volume 1102 of LNCS. Springer, 1996.
S. Owre and N. Shankar. Abstract datatypes in PVS. Technical Report CSL-93-9R, Computer Science Laboratory, SRI International, 1993.
L. C. Paulson. A fixed-point approach to implementing (co)inductive defonitions. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, volume 814 of LNAI, pages 148–161, Nancy, France, 1994. Springer.
L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer, 1994.
L. C. Paulson. Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation, 7(2):175–204, 1997.
F. Pfenning and C. Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In Proceedings of Mathematical Foundations of Programming Semantics, volume 442 of LNCS. Springer, 1990.
K. Slind. Function definition in higher order logic. In J. Wright, J. Grundy, and J. Harrison, editors, 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs’96, volume 1125 of LNCS. Springer, 1996.
K. Slind. Derivation and use of induction schemes in higher-order logic. In 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs’97, volume 1275 of LNCS. Springer, 1997.
[23] N. Völker. On the representation of datatypes in Isabelle/HOL. In L. C. Paulson, editor, First Isabelle Users Workshop, 1995.
[24] M. Wenzel. Type classes and overloading in higher-order logic. In 10th International Conference on Theorem Proving in Higher Order Logics, TPHOLs’97, volume 1275 of LNCS. Springer, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berghofer, S., Wenzel, M. (1999). Inductive Datatypes in HOL — Lessons Learned in Formal-Logic Engineering. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_3
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive