--- a/src/Doc/Datatypes/Datatypes.thy Wed Jul 31 13:00:42 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Jul 31 15:24:07 2013 +0200
@@ -20,17 +20,17 @@
of non-datatypes, notably finite sets:
*}
-datatype_new 'a tree = Node 'a "('a tree fset)"
+ datatype_new 'a treeFS = TreeFS 'a "'a treeFS fset"
text {*
\noindent
Another advantage of the new package is that it supports local definitions:
*}
-context linorder
-begin
- datatype_new flag = Less | Eq | Greater
-end
+ context linorder
+ begin
+ datatype_new flag = Less | Eq | Greater
+ end
text {*
\noindent
@@ -39,25 +39,25 @@
*}
(*<*)hide_const Nil Cons hd tl(*>*)
-datatype_new 'a list = null: Nil | Cons (hd: 'a) (tl: "'a list")
+ 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]}
+%
+\[@{thm list.collapse(1)[no_vars]}\qquad @{thm list.collapse(2)[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.
+maintainers of older theories may want to consider upgrading in the coming months.
The package also provides codatatypes (or ``coinductive datatypes''), which may
-have infinite values. The following command introduces a type of infinite
+have infinite values. The following command introduces a codatatype of infinite
streams:
*}
-codatatype 'a stream = Stream 'a "('a stream)"
+ codatatype 'a stream = Stream 'a "'a stream"
text {*
\noindent
@@ -65,60 +65,189 @@
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)"
+ 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}:
+can be precompiled as the \textit{HOL-BNF} image. The following commands show
+how to launch jEdit/PIDE with the image loaded and how to build the image
+without launching jEdit:
*}
text {*
\noindent
-\texttt{isabelle build -b HOL-BNF}
+\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\
+\ \ \ \ \texttt{isabelle build -b HOL-BNF}
*}
text {*
- * TODO: LCF tradition
- * internals: LICS paper
+The package, like its predecessor, fully adheres to the LCF philosophy
+\cite{mgordon79}: The characteristic theorems associated with the specified
+(co)datatypes are derived rather than introduced axiomatically.%
+\footnote{Nonetheless, if the \textit{quick\_and\_dirty} option is enabled, some
+of the internal constructions and most of the internal proof obligations are
+skipped.}
+The package's metatheory is described in a pair of papers
+\cite{traytel-et-al-2012,blanchette-et-al-wit}.
*}
text {*
This tutorial is organized as follows:
- * datatypes
- * primitive recursive functions
- * codatatypes
- * primitive corecursive functions
+\begin{itemize}
+\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
+describes how to specify datatypes using the \cmd{datatype\_new} command.
+
+\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
+Functions,'' describes how to specify recursive functions using
+\cmd{primrec\_new}, \cmd{fun}, and \cmd{function}.
+
+\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
+describes how to specify codatatypes using the \cmd{codatatype} command.
+
+\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
+Functions,'' describes how to specify corecursive functions using the
+\cmd{primcorec} command.
-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}.
+\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
+Bounded Natural Functors,'' explains how to set up the (co)datatype package to
+allow nested recursion through custom well-behaved type constructors.
+
+\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free
+Constructor Theorems,'' explains how to derive convenience theorems for free
+constructors, as performed internally by \cmd{datatype\_new} and
+\cmd{codatatype}.
-then: Standard ML interface
+\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
+describes the package's programmatic interface.
-interaction with other tools
- * code generator (and Quickcheck)
- * Nitpick
+\item Section \ref{sec:interoperability}, ``Interoperability,''
+is concerned with the packages' interaction with other Isabelle packages and
+tools, such as the code generator and the counterexample generators.
+
+\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
+Limitations,'' concludes with open issues.
+\end{itemize}
*}
-section {* Defining Datatypes *}
+section {* Defining Datatypes%
+ \label{sec:defining-datatypes} *}
+
+text {*
+This section describes how to specify datatypes using the \cmd{datatype\_new}
+command. The command is first illustrated through concrete examples featuring
+different flavors of recursion. More examples are available in
+\verb|~~/src/HOL/BNF/Examples|. The syntax is largely modeled after that of the
+existing \cmd{datatype} command.
+*}
subsection {* Introductory Examples *}
subsubsection {* Nonrecursive Types *}
+text {*
+enumeration type:
+*}
+
+ datatype_new trool = Truue | Faalse | Maaybe
+
+text {*
+Haskell-style option type:
+*}
+
+ datatype_new 'a maybe = Nothing | Just 'a
+
+text {*
+triple:
+*}
+
+ datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
+
subsubsection {* Simple Recursion *}
+text {*
+simplest recursive type: natural numbers
+*}
+
+ datatype_new nat = Zero | Suc nat
+
+text {*
+lists were shown in the introduction
+
+terminated lists are a variant:
+*}
+
+ datatype_new ('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
+
+text {*
+On the right-hand side of the equal sign, the usual Isabelle conventions apply:
+Nonatomic types must be enclosed in double quotes.
+*}
+
subsubsection {* Mutual Recursion *}
+text {*
+Mutual recursion = Define several types simultaneously, referring to each other.
+
+Simple example: distinction between even and odd natural numbers:
+*}
+
+ datatype_new even_nat = Zero | Even_Suc odd_nat
+ and odd_nat = Odd_Suc even_nat
+
+text {*
+More complex, and more realistic, example:
+*}
+
+ datatype_new ('a, 'b) expr =
+ Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) expr"
+ and ('a, 'b) trm =
+ Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
+ and ('a, 'b) factor =
+ Const 'a | Var 'b | Sub_Expr "('a, 'b) expr"
+
subsubsection {* Nested Recursion *}
-subsubsection {* Auxiliary Constants *}
+text {*
+Nested recursion = Have recursion through a type constructor.
+
+The introduction showed some examples of trees with nesting through lists.
+
+More complex example, which reuses our maybe and triple types:
+*}
+
+ datatype_new 'a triple_tree =
+ Triple_Tree "('a triple_tree maybe, bool, 'a triple_tree maybe) triple"
+
+text {*
+Recursion may not be arbitrary; e.g. impossible to define
+*}
+
+(*
+ datatype_new 'a foo = Foo (*<*) datatype_new 'a bar = Bar "'a foo \<Rightarrow> 'a foo"
+*)
+
+ datatype_new 'a evil = Evil (*<*)'a
+ typ (*>*)"'a evil \<Rightarrow> 'a evil"
+
+text {*
+Issue: => allows recursion only on its right-hand side.
+This issue is inherited by polymorphic datatypes (and codatatypes)
+defined in terms of =>.
+In general, type constructors "('a1, ..., 'an) k" allow recursion on a subset
+of their type arguments.
+*}
+
+
+subsubsection {* Auxiliary Constants and Syntaxes *}
+
+text {*
+* destructors
+* also mention special syntaxes
+*}
subsection {* General Syntax *}
@@ -127,10 +256,24 @@
subsection {* Compatibility Issues *}
-section {* Defining Primitive Recursive Functions *}
+section {* Defining Recursive Functions%
+ \label{sec:defining-recursive-functions} *}
+
+text {*
+This describes how to specify recursive functions over datatypes
+specified using \cmd{datatype\_new}. The focus in on the \cmd{primrec\_new}
+command, which supports primitive recursion. A few examples feature the
+\cmd{fun} and \cmd{function} commands, described in a separate tutorial
+\cite{isabelle-function}.
+%%% TODO: partial_function?
+*}
subsection {* Introductory Examples *}
+text {*
+More examples in \verb|~~/src/HOL/BNF/Examples|.
+*}
+
subsection {* General Syntax *}
subsection {* Characteristic Theorems *}
@@ -138,44 +281,101 @@
subsection {* Compatibility Issues *}
-section {* Defining Codatatypes *}
+section {* Defining Codatatypes%
+ \label{sec:defining-codatatypes} *}
+
+text {*
+This section describes how to specify codatatypes using the \cmd{codatatype}
+command.
+*}
subsection {* Introductory Examples *}
+text {*
+More examples in \verb|~~/src/HOL/BNF/Examples|.
+*}
+
+subsection {* General Syntax *}
+
+subsection {* Characteristic Theorems *}
+
+
+section {* Defining Corecursive Functions%
+ \label{sec:defining-corecursive-functions} *}
+
+text {*
+This section describes how to specify corecursive functions using the
+\cmd{primcorec} command.
+*}
+
+subsection {* Introductory Examples *}
+
+text {*
+More examples in \verb|~~/src/HOL/BNF/Examples|.
+*}
+
subsection {* General Syntax *}
subsection {* Characteristic Theorems *}
-section {* Defining Primitive Corecursive Functions *}
+section {* Registering Bounded Natural Functors%
+ \label{sec:registering-bounded-natural-functors} *}
+
+text {*
+This section explains how to set up the (co)datatype package to allow nested
+recursion through custom well-behaved type constructors. The key concept is that
+of a bounded natural functor (BNF).
+*}
-subsection {* Introductory Examples *}
+subsection {* Introductory Example *}
+
+text {*
+More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
+\verb|~~/src/HOL/BNF/More_BNFs.thy|.
+
+Mention distinction between live and dead type arguments;
+mention =>.
+*}
subsection {* General Syntax *}
-subsection {* Characteristic Theorems *}
+
+section {* Generating Free Constructor Theorems%
+ \label{sec:generating-free-constructor-theorems} *}
-subsection {* Compatibility Issues *}
+text {*
+This section explains how to derive convenience theorems for free constructors,
+as performed internally by \cmd{datatype\_new} and \cmd{codatatype}.
+ * need for this is rare but may arise if you want e.g. to add destructors to
+ a type not introduced by ...
-section {* Registering Bounded Natural Functors *}
+ * also useful for compatibility with old package, e.g. add destructors to
+ old \cmd{datatype}
+*}
subsection {* Introductory Example *}
subsection {* General Syntax *}
-section {* Generating Free Constructor Theorems *}
+section {* Standard ML Interface%
+ \label{sec:standard-ml-interface} *}
-subsection {* Introductory Example *}
+text {*
+This section describes the package's programmatic interface.
+*}
-subsection {* General Syntax *}
-section {* Registering Bounded Natural Functors *}
+section {* Interoperability%
+ \label{sec:interoperability} *}
-section {* Standard ML Interface *}
-
-section {* Interoperability Issues *}
+text {*
+This section is concerned with the packages' interaction with other Isabelle
+packages and tools, such as the code generator and the counterexample
+generators.
+*}
subsection {* Transfer and Lifting *}
@@ -187,10 +387,24 @@
subsection {* Nominal Isabelle *}
-section {* Known Bugs and Limitations *}
+
+section {* Known Bugs and Limitations%
+ \label{sec:known-bugs-and-limitations} *}
+
+text {*
+This section lists known open issues of the package.
+*}
text {*
+* primrec\_new and primcorec are vaporware
+
* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
+
+* issues with HOL-Proofs?
+
+* partial documentation
+
+* too much output by commands like "datatype_new" and "codatatype"
*}
end
--- a/src/Doc/Datatypes/document/root.tex Wed Jul 31 13:00:42 2013 +0200
+++ b/src/Doc/Datatypes/document/root.tex Wed Jul 31 15:24:07 2013 +0200
@@ -1,4 +1,6 @@
\documentclass[12pt,a4paper]{article} % fleqn
+\usepackage{cite}
+\usepackage{enumitem}
\usepackage{latexsym}
\usepackage{graphicx}
\usepackage{iman}
@@ -9,10 +11,18 @@
\usepackage{style}
\usepackage{pdfsetup}
+\newbox\boxA
+\setbox\boxA=\hbox{\ }
+\parindent=4\wd\boxA
+
\newcommand{\cmd}[1]{\isacommand{#1}}
+\def\isacharprime{\isamath{{'}\mskip-2mu}}
\renewcommand{\isacharunderscore}{\mbox{\_}}
\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
+\renewcommand{\isachardoublequote}{\mbox{\upshape{``}}}
+\renewcommand{\isachardoublequoteopen}{\mbox{\upshape{``}\,}}
+\renewcommand{\isachardoublequoteclose}{\mbox{\,\upshape{''}}}
\hyphenation{isa-belle}
@@ -21,7 +31,9 @@
\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
Defining (Co)datatypes in Isabelle/HOL}
\author{\hbox{} \\
-Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel \\
+Jasmin Christian Blanchette \\
+Andrei Popescu \\
+Dmitriy Traytel \\
{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
\hbox{}}
\begin{document}
--- a/src/Doc/manual.bib Wed Jul 31 13:00:42 2013 +0200
+++ b/src/Doc/manual.bib Wed Jul 31 15:24:07 2013 +0200
@@ -301,6 +301,12 @@
author = "Jasmin Christian Blanchette and Tobias Nipkow",
crossref = {itp2010}}
+@unpublished{blanchette-et-al-wit,
+ author = {J.C. Blanchette and A. Popescu and D. Traytel},
+ title = {Witnessing (Co)datatypes},
+ year = 2013,
+ note = {\url{http://www21.in.tum.de/~traytel/papers/witness/wit.pdf}}}
+
@inproceedings{why3,
author = {Fran\c{c}ois Bobot and Jean-Christophe Filli\^atre and Claude March\'e and Andrei Paskevich},
title = {{Why3}: Shepherd Your Herd of Provers},
@@ -1662,7 +1668,16 @@
Subtyping (long version)},
year = 2011,
note = {Submitted,
- \url{http://isabelle.in.tum.de/doc/implementation.pdf}}},
+ \url{http://isabelle.in.tum.de/doc/implementation.pdf}}}
+
+@inproceedings{traytel-et-al-2012,
+ author = "Dmitriy Traytel and Andrei Popescu and Jasmin Christian Blanchette",
+ title = {Foundational, Compositional (Co)datatypes for Higher-Order
+ Logic---{C}ategory Theory Applied to Theorem Proving},
+ year = {2012},
+ pages = {596--605},
+ booktitle = {LICS 2012},
+ publisher = {IEEE}
}
@Unpublished{Trybulec:1993:MizarFeatures,