src/HOL/Codatatype/README.html
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49159 7af3f9f41783
child 49509 163914705f8d
permissions -rw-r--r--
tuned simpset
blanchet@48975
     1
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
blanchet@48975
     2
blanchet@48975
     3
<html>
blanchet@48975
     4
blanchet@48975
     5
<head>
blanchet@48975
     6
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
blanchet@48975
     7
  <title>Codatatype Package</title>
blanchet@48975
     8
</head>
blanchet@48975
     9
blanchet@48975
    10
<body>
blanchet@48975
    11
blanchet@48975
    12
<h3><i>Codatatype</i>: A (co)datatype package based on bounded natural functors
blanchet@48975
    13
(BNFs)</h3>
blanchet@48975
    14
blanchet@48975
    15
<p>
blanchet@48975
    16
The <i>Codatatype</i> package provides a fully modular framework for
blanchet@48975
    17
constructing inductive and coinductive datatypes in HOL, with support for mixed
blanchet@48975
    18
mutual and nested (co)recursion. Mixed (co)recursion enables type definitions
blanchet@48975
    19
involving both datatypes and codatatypes, such as the type of finitely branching
blanchet@48975
    20
trees of possibly infinite depth. The framework draws heavily from category
blanchet@48975
    21
theory.
blanchet@48975
    22
blanchet@48975
    23
<p>
blanchet@48975
    24
The package is described in the following paper:
blanchet@48975
    25
blanchet@48975
    26
<ul>
blanchet@48975
    27
  <li><a href="http://www21.in.tum.de/~traytel/papers/codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic&mdash;Category Theory Applied to Theorem Proving</a>, <br>
blanchet@48975
    28
  Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
blanchet@48975
    29
  <i>Logic in Computer Science (LICS 2012)</i>, 2012.
blanchet@48975
    30
</ul>
blanchet@48975
    31
blanchet@48975
    32
<p>
blanchet@48975
    33
The main entry point for applications is <tt>Codatatype.thy</tt>.
blanchet@48975
    34
The <tt>Examples</tt> directory contains various examples of (co)datatypes,
blanchet@48975
    35
including the examples from the paper.
blanchet@48975
    36
blanchet@48975
    37
<p>
blanchet@48975
    38
The key notion underlying the package is that of a <i>bounded natural functor</i>
blanchet@48975
    39
(<i>BNF</i>)&mdash;an enriched type constructor satisfying specific properties
blanchet@48975
    40
preserved by interesting categorical operations (composition, least fixed point,
blanchet@48975
    41
and greatest fixed point). The <tt>Basic_BNFs.thy</tt> file registers
blanchet@48975
    42
various basic types, notably for sums, products, function spaces, finite sets,
blanchet@48975
    43
multisets, and countable sets. Custom BNFs can be registered as well.
blanchet@48975
    44
blanchet@48975
    45
<p>
blanchet@48975
    46
<b>Warning:</b> The package is under development. Future versions are expected
blanchet@48975
    47
to support multiple constructors and selectors per (co)datatype (instead of a
blanchet@48975
    48
single <i>fld</i> or <i>unf</i> constant) and provide a nicer syntax for
blanchet@49159
    49
(co)induction and (co)recursive function definitions. Please contact
blanchet@49159
    50
any nonempty subset of
blanchet@48975
    51
<a href="mailto:traytel@in.tum.de">the</a>
blanchet@48975
    52
<a href="mailto:popescua@in.tum.de">above</a>
blanchet@48975
    53
<a href="mailto:blanchette@in.tum.de">authors</a>
blanchet@48975
    54
if you have questions or comments.
blanchet@48975
    55
blanchet@48975
    56
</body>
blanchet@48975
    57
blanchet@48975
    58
</html>