Inductive definitions: automation and application

John Harrison.

Proceedings of the 1995 International Workshop on Higher Order Logic theorem proving and its applications, Aspen Grove, Utah, 1995. Springer LNCS 971, pp. 186-199, 1995.

Abstract:

This paper demonstrates the great practical utility of inductive definitions in HOL. We describe a new package we have implemented for automating inductive definitions, based on the Knaster-Tarski fixpoint theorem. As an example, we use it to give a simple proof of the well-founded recursion theorem. We then describe how to generate free recursive types starting just from the Axiom of Infinity. This contrasts with the existing HOL development where several specific free recursive types are developed first.

DVI or PostScript

Bibtex entry:

@INPROCEEDINGS{harrison-ind,
        crossref        = "hol95",
        author          = "John Harrison",
        title           = "Inductive definitions: automation and application",
        pages           = "200--213"}

@PROCEEDINGS{hol95,
        editor          = "Phillip J. Windley and Thomas Schubert and
                           Jim Alves-Foss",
        booktitle       = "Higher Order Logic Theorem Proving and Its
                           Applications: Proceedings of the 8th
                           International Workshop",
        series          = "Lecture Notes in Computer Science",
        volume          = 971,
        address         = "Aspen Grove, Utah",
        date            = "11--14 September 1995",
        year            = 1995,
        publisher       = "Springer-Verlag"}