Datentypspezifikationen in HOLCF



David von Oheimb


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.


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

Available as Postscript (288K)

   author = {Oheimb, David von},
   title  = {Datentypspezifikationen in {H}igher-{O}rder {LCF}},
   school = {Technische Universit{\"a}t M{\"u}nchen},
   year   = {1995},
   url    = {\url{}}

Oscar Slotosch, 05-12-1995