--- a/doc/Contents Tue Jul 30 23:16:17 2013 +0200
+++ b/doc/Contents Tue Jul 30 23:17:26 2013 +0200
@@ -3,6 +3,7 @@
tutorial Tutorial on Isabelle/HOL
locales Tutorial on Locales
classes Tutorial on Type Classes
+ datatypes Tutorial on (Co)datatype Definitions
functions Tutorial on Function Definitions
codegen Tutorial on Code Generation
nitpick User's Guide to Nitpick
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Jul 30 23:17:26 2013 +0200
@@ -0,0 +1,196 @@
+(* Title: Doc/Datatypes/Datatypes.thy
+ Author: Jasmin Blanchette, TU Muenchen
+
+Tutorial for (co)datatype definitions with the new package.
+*)
+
+theory Datatypes
+imports BNF
+begin
+
+section {* Introduction *}
+
+text {*
+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 {*
+\noindent
+Another advantage of the new package is that it supports local definitions:
+*}
+
+context linorder
+begin
+ datatype_new flag = Less | Eq | Greater
+end
+
+text {*
+\noindent
+Finally, the package also provides some convenience, notably automatically
+generated destructors. For example, the command
+*}
+
+(*<*)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 {* Defining Datatypes *}
+
+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 *}
+
+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
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/build Tue Jul 30 23:17:26 2013 +0200
@@ -0,0 +1,14 @@
+#!/bin/bash
+
+set -e
+
+FORMAT="$1"
+VARIANT="$2"
+
+cp "$ISABELLE_HOME/src/Doc/iman.sty" .
+cp "$ISABELLE_HOME/src/Doc/extra.sty" .
+cp "$ISABELLE_HOME/src/Doc/isar.sty" .
+cp "$ISABELLE_HOME/src/Doc/manual.bib" .
+
+"$ISABELLE_HOME/src/Doc/prepare_document" "$FORMAT"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/root.tex Tue Jul 30 23:17:26 2013 +0200
@@ -0,0 +1,48 @@
+\documentclass[12pt,a4paper]{article} % fleqn
+\usepackage{latexsym}
+\usepackage{graphicx}
+\usepackage{iman}
+\usepackage{extra}
+\usepackage{isar}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+\newcommand{\cmd}[1]{\isacommand{#1}}
+
+\renewcommand{\isacharunderscore}{\mbox{\_}}
+\renewcommand{\isacharunderscorekeyword}{\mbox{\_}}
+
+\hyphenation{isa-belle}
+
+\isadroptag{theory}
+
+\title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex]
+Defining (Co)datatypes in Isabelle/HOL}
+\author{\hbox{} \\
+Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel \\
+{\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\
+\hbox{}}
+\begin{document}
+
+\maketitle
+
+\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 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
+\bibliography{manual}{}
+\bibliographystyle{abbrv}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/style.sty Tue Jul 30 23:17:26 2013 +0200
@@ -0,0 +1,58 @@
+
+%% toc
+\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
+\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
+
+%% paragraphs
+\setlength{\parindent}{1em}
+
+%% references
+\newcommand{\secref}[1]{\S\ref{#1}}
+\newcommand{\figref}[1]{figure~\ref{#1}}
+
+%% logical markup
+\newcommand{\strong}[1]{{\bfseries {#1}}}
+\newcommand{\qn}[1]{\emph{#1}}
+
+%% typographic conventions
+\newcommand{\qt}[1]{``{#1}''}
+\newcommand{\ditem}[1]{\item[\isastyletext #1]}
+
+%% quote environment
+\isakeeptag{quote}
+\renewenvironment{quote}
+ {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
+ {\endlist}
+\renewcommand{\isatagquote}{\begin{quote}}
+\renewcommand{\endisatagquote}{\end{quote}}
+\newcommand{\quotebreak}{\\[1.2ex]}
+
+%% typewriter text
+\newenvironment{typewriter}{\renewcommand{\isastyletext}{}%
+\renewcommand{\isadigit}[1]{{##1}}%
+\parindent0pt%
+\makeatletter\isa@parindent0pt\makeatother%
+\isabellestyle{tt}\isastyle%
+\fontsize{9pt}{9pt}\selectfont}{}
+
+\isakeeptag{quotetypewriter}
+\renewcommand{\isatagquotetypewriter}{\begin{quote}\begin{typewriter}}
+\renewcommand{\endisatagquotetypewriter}{\end{typewriter}\end{quote}}
+
+%% presentation
+\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
+
+%% character detail
+\renewcommand{\isadigit}[1]{\isamath{#1}}
+\binperiod
+\underscoreoff
+
+%% format
+\pagestyle{headings}
+\isabellestyle{it}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "implementation"
+%%% End:
--- a/src/Doc/Functions/document/root.tex Tue Jul 30 23:16:17 2013 +0200
+++ b/src/Doc/Functions/document/root.tex Tue Jul 30 23:17:26 2013 +0200
@@ -59,7 +59,7 @@
\maketitle
\begin{abstract}
- This tutorial describes the use of the new \emph{function} package,
+ This tutorial describes the use of the \emph{function} package,
which provides general recursive function definitions for Isabelle/HOL.
We start with very simple examples and then gradually move on to more
advanced topics such as manual termination proofs, nested recursion,
--- a/src/Doc/ROOT Tue Jul 30 23:16:17 2013 +0200
+++ b/src/Doc/ROOT Tue Jul 30 23:17:26 2013 +0200
@@ -37,6 +37,20 @@
"document/root.tex"
"document/style.sty"
+session Datatypes (doc) in "Datatypes" = "HOL-BNF" +
+ options [document_variants = "datatypes"]
+ theories Datatypes
+ files
+ "../prepare_document"
+ "../pdfsetup.sty"
+ "../iman.sty"
+ "../extra.sty"
+ "../isar.sty"
+ "../manual.bib"
+ "document/build"
+ "document/root.tex"
+ "document/style.sty"
+
session Functions (doc) in "Functions" = HOL +
options [document_variants = "functions", skip_proofs = false]
theories Functions
--- a/src/HOL/BNF/README.html Tue Jul 30 23:16:17 2013 +0200
+++ b/src/HOL/BNF/README.html Tue Jul 30 23:17:26 2013 +0200
@@ -23,7 +23,7 @@
The package is described in the following paper:
<ul>
- <li><a href="http://www21.in.tum.de/~traytel/papers/codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br>
+ <li><a href="http://www21.in.tum.de/~traytel/papers/lics12-codatatypes/index.html">Foundational, Compositional (Co)datatypes for Higher-Order Logic—Category Theory Applied to Theorem Proving</a>, <br>
Dmitriy Traytel, Andrei Popescu, and Jasmin Christian Blanchette.<br>
<i>Logic in Computer Science (LICS 2012)</i>, 2012.
</ul>
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Jul 30 23:16:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Jul 30 23:17:26 2013 +0200
@@ -135,7 +135,7 @@
fun register_fp_sugar key fp_sugar =
Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update_new (key, morph_fp_sugar phi fp_sugar)));
+ (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
fun register_fp_sugars fp pre_bnfs nested_bnfs (fp_res as {Ts, ...}) ctr_defss ctr_sugars co_iterss
co_inducts co_iter_thmsss lthy =