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.
CITATION STYLE
Berghofer, S., & Wenzel, M. (1999). Inductive datatypes in hol-lessons learned in formal-logic engineering. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1690, pp. 19–36). Springer Verlag. https://doi.org/10.1007/3-540-48256-3_3
Mendeley helps you to discover research relevant for your work.