paper available

The following report is available by anonymous ftp from the University of

A Fixedpoint Approach to Implementing (Co)Inductive Definitions

by Lawrence C. Paulson

  Several theorem provers provide commands for formalizing recursive
  datatypes or inductively defined sets.  This paper presents a new
  approach, based on fixedpoint definitions.  It is unusually general: it
  admits all provably monotone inductive definitions.  It is conceptually
  simple, which has allowed the easy implementation of mutual recursion and
  other conveniences.  It also handles coinductive definitions: simply
  replace the least fixedpoint by a greatest fixedpoint.  This represents
  the first automated support for coinductive definitions.

  The method has been implemented in Isabelle's formalization of ZF set
  theory.  It should be applicable to any logic in which the Knaster-Tarski
  Theorem can be proved.  The paper briefly describes a method of
  formalizing non-well-founded data structures in standard ZF set theory.

  Examples include lists of n elements, the accessible part of a relation
  and the set of primitive recursive functions.  One example of a
  coinductive definition is bisimulations for lazy lists.  
  Recursive datatypes are examined in detail, as well as one example of a
  "codatatype": lazy lists.  The appendices are simple user's manuals
  for this Isabelle/ZF package.

FTP Instructions:

* Connect to host ftp.cl.cam.ac.uk []
* Use login id "ftp" with your internet address as password
* put ftp in BINARY MODE ("binary") 
* go to directory reports (by typing "cd reports")
* "get" the file TR320-lcp-isabelle-ind-defs.dvi.gz from that directory.  

This is a gzip'ed dvi file.  It should be unpacked using the Gnu utility

							Larry Paulson