Author:

Abstract:

This data type package is an extension to the object logic HOLCF (Higher-Order Logic
of Computable Functions, by F.Regensburger) for the generic theorem prover Isabelle
(by L.C.Paulson and T.Nipkow). It determines and proofs the properties of datatypes
that are given in the form of recursive domain equations, and produces induction rules
from datatype generation rules. The datatypes may be simultaneously recursive and
contain non-strict constructors.

For datatypes defined by domain equations, the generated theory extension is
conservative, which is confirmed by a given external category-theoretic argument
that is further motivated and adapted to simultaneous equations here. As axioms, just
an isomorphism resulting from the equations and a fixed-point property of the
so-called `copy functional' is needed.

A number of user-relevant theorems concerning the constructors, discriminatiors, and
selectors of the datatype, as well as induction and co-induction principles, are
proved by the package. As they simplify the use of datatypes significantly, this work
is an important step towards the applicability of Isabelle/HOLCF as a specification
and verification tool.

Keywords:

datatypes, domain equations, induction, Isabelle, HOLCF, theory extension

Available as Postscript (288K)

@mastersthesis{DvO95, author = {Oheimb, David von}, title = {Datentypspezifikationen in {H}igher-{O}rder {LCF}}, school = {Technische Universit{\"a}t M{\"u}nchen}, year = {1995}, url = {\url{http://ddvo.net/papers/DA_Oheimb.html}} }

Oscar Slotosch, 05-12-1995