# HG changeset patch # User wenzelm # Date 1375219046 -7200 # Node ID add5c023ba03cd2df2c270aa324639c9c9c81c38 # Parent 126ee2abed9becb8db4111d47b6464c4344dfbdf# Parent bcaa5bbf7e6b928cf7cada4e77283c92d70ad03d merged diff -r bcaa5bbf7e6b -r add5c023ba03 doc/Contents --- 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 diff -r bcaa5bbf7e6b -r add5c023ba03 src/Doc/Datatypes/Datatypes.thy --- /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 diff -r bcaa5bbf7e6b -r add5c023ba03 src/Doc/Datatypes/document/build --- /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" + diff -r bcaa5bbf7e6b -r add5c023ba03 src/Doc/Datatypes/document/root.tex --- /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} diff -r bcaa5bbf7e6b -r add5c023ba03 src/Doc/Datatypes/document/style.sty --- /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: diff -r bcaa5bbf7e6b -r add5c023ba03 src/Doc/Functions/document/root.tex --- 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, diff -r bcaa5bbf7e6b -r add5c023ba03 src/Doc/ROOT --- 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 diff -r bcaa5bbf7e6b -r add5c023ba03 src/HOL/BNF/README.html --- 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: diff -r bcaa5bbf7e6b -r add5c023ba03 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- 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 =