# HG changeset patch # User blanchet # Date 1375206582 -7200 # Node ID aae782070611688e9d4378c362f6dd6a88b4abf1 # Parent 062aa11e98e1a777830155015d4477dbffa441b7 more (co)datatype documentation diff -r 062aa11e98e1 -r aae782070611 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 16:22:39 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 19:49:42 2013 +0200 @@ -11,52 +11,194 @@ section {* Introduction *} text {* - * Isabelle2013 introduced new definitional package for datatypes and codatatypes - - * datatype support is similar to old package, due to Berghofer \& Wenzel \cite{xxx} - * indeed, replacing \cmd{datatype} by \cmd{datatype\_new} is usually sufficient - to port existing specifications to the new package - - * but it is more powerful, because it is now possible to have nested recursion - through a large class of non-datatypes, notably finite sets: +The 2013 edition of Isabelle introduced new definitional package for datatypes +and codatatypes. The datatype support is similar to that provided by the earlier +package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}; +indeed, replacing \cmd{datatype} by \cmd{datatype\_new} is usually sufficient +to port existing specifications to the new package. What makes the new package +attractive is that it supports definitions with recursion through a large class +of non-datatypes, notably finite sets: *} datatype_new 'a tree = Node 'a "('a tree fset)" text {* - * another advantage: it supports local definitions: +\noindent +Another advantage of the new package is that it supports local definitions: *} context linorder begin - -datatype_new flag = Less | Eq | Greater - + datatype_new flag = Less | Eq | Greater end text {* +\noindent +Finally, the package also provides some convenience, notably automatically +generated destructors. For example, the command +*} - * in a future release, \cmd{datatype\_new} is expected to displace \cmd{datatype} +(*<*)hide_const Nil Cons hd tl(*>*) +datatype_new 'a list = null: Nil | Cons (hd: 'a) (tl: "'a list") + +text {* +\noindent +introduces a discriminator @{const null} and a pair of selectors @{const hd} and +@{const tl} characterized as follows: + +@{thm [display] list.collapse[no_vars]} + +The command \cmd{datatype\_new} is expected to displace \cmd{datatype} in a future +release. Authors of new theories are encouraged to use \cmd{datatype\_new}, and +maintainers of older theories might want to consider upgrading now. + +The package also provides codatatypes (or ``coinductive datatypes''), which may +have infinite values. The following command introduces a type of infinite +streams: +*} + +codatatype 'a stream = Stream 'a "('a stream)" + +text {* +\noindent +Mixed inductive--coinductive recursion is possible via nesting. +Compare the following four examples: +*} + +datatype_new 'a treeFF = TreeFF 'a "('a treeFF list)" +datatype_new 'a treeFI = TreeFI 'a "('a treeFF stream)" +codatatype 'a treeIF = TreeIF 'a "('a treeFF list)" +codatatype 'a treeII = TreeII 'a "('a treeFF stream)" - * +text {* +To use the package, it is necessary to import the @{theory BNF} theory, which +can be precompiled as the \textit{HOL-BNF}: +*} + +text {* +\noindent +\texttt{isabelle build -b HOL-BNF} +*} + +text {* + * TODO: LCF tradition + * internals: LICS paper *} +text {* +This tutorial is organized as follows: + + * datatypes + * primitive recursive functions + * codatatypes + * primitive corecursive functions + +the following sections focus on more technical aspects: +how to register bounded natural functors (BNFs), i.e., type +constructors via which (co)datatypes can (co)recurse, +and how to derive convenience theorems for free constructors, +as performed internally by \cmd{datatype\_new} and \cmd{codatatype}. + +then: Standard ML interface + +interaction with other tools + * code generator (and Quickcheck) + * Nitpick +*} + +section {* Registering Bounded Natural Functors *} + +subsection {* Introductory Example *} + +subsection {* General Syntax *} + +section {* Generating Free Constructor Theorems *} + section {* Defining Datatypes *} -text {* - * theory to include -*} +subsection {* Introductory Examples *} + +subsubsection {* Nonrecursive Types *} + +subsubsection {* Simple Recursion *} + +subsubsection {* Mutual Recursion *} + +subsubsection {* Nested Recursion *} + +subsubsection {* Auxiliary Constants *} + +subsection {* General Syntax *} + +subsection {* Characteristic Theorems *} + +subsection {* Compatibility Issues *} + section {* Defining Primitive Recursive Functions *} +subsection {* Introductory Examples *} + +subsection {* General Syntax *} + +subsection {* Characteristic Theorems *} + +subsection {* Compatibility Issues *} + + section {* Defining Codatatypes *} +subsection {* Introductory Examples *} + +subsection {* General Syntax *} + +subsection {* Characteristic Theorems *} + + section {* Defining Primitive Corecursive Functions *} +subsection {* Introductory Examples *} + +subsection {* General Syntax *} + +subsection {* Characteristic Theorems *} + +subsection {* Compatibility Issues *} + + section {* Registering Bounded Natural Functors *} +subsection {* Introductory Example *} + +subsection {* General Syntax *} + + section {* Generating Free Constructor Theorems *} -section {* Conclusion *} +subsection {* Introductory Example *} + +subsection {* General Syntax *} + +section {* Registering Bounded Natural Functors *} + +section {* Standard ML Interface *} + +section {* Interoperability Issues *} + +subsection {* Transfer and Lifting *} + +subsection {* Code Generator *} + +subsection {* Quickcheck *} + +subsection {* Nitpick *} + +subsection {* Nominal Isabelle *} + +section {* Known Bugs and Limitations *} + +text {* +* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) +*} end diff -r 062aa11e98e1 -r aae782070611 src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Tue Jul 30 16:22:39 2013 +0200 +++ b/src/Doc/Datatypes/document/root.tex Tue Jul 30 19:49:42 2013 +0200 @@ -1,4 +1,4 @@ -\documentclass[12pt,a4paper,fleqn]{article} +\documentclass[12pt,a4paper]{article} % fleqn \usepackage{latexsym} \usepackage{graphicx} \usepackage{iman} @@ -11,6 +11,9 @@ \newcommand{\cmd}[1]{\isacommand{#1}} +\renewcommand{\isacharunderscore}{\mbox{\_}} +\renewcommand{\isacharunderscorekeyword}{\mbox{\_}} + \hyphenation{isa-belle} \isadroptag{theory} @@ -27,13 +30,15 @@ \begin{abstract} \noindent -This tutorial describes how to use the new package for defining -datatypes and codatatypes in Isabelle/HOL. The package provides four -main user-level commands: \cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and -\cmd{primcorec}. The \cmd{\_new} commands are designed to subsume, and eventually +This tutorial describes how to use the new package for defining datatypes and +codatatypes in Isabelle/HOL. The package provides four main user-level commands: +\cmd{datatype\_new}, \cmd{codatatype}, \cmd{primrec\_new}, and \cmd{primcorec}. +The commands suffixed by \cmd{\_new} are intended to subsume, and eventually replace, the corresponding commands from the old datatype package. \end{abstract} +\tableofcontents + \input{Datatypes.tex} \let\em=\sl diff -r 062aa11e98e1 -r aae782070611 src/HOL/BNF/README.html --- a/src/HOL/BNF/README.html Tue Jul 30 16:22:39 2013 +0200 +++ b/src/HOL/BNF/README.html Tue Jul 30 19:49:42 2013 +0200 @@ -23,7 +23,7 @@ The package is described in the following paper: