# HG changeset patch
# User blanchet
# Date 1375194159 -7200
# Node ID 3e651be14fcd7415ade06e4217209b95f221b017
# Parent  9e4bb60f8007a8fea1be8ec5ebe61660f0dd4131
sketched documentation for new (co)datatype package

diff -r 9e4bb60f8007 -r 3e651be14fcd doc/Contents
--- a/doc/Contents	Tue Jul 30 16:22:39 2013 +0200
+++ b/doc/Contents	Tue Jul 30 16:22:39 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 9e4bb60f8007 -r 3e651be14fcd src/Doc/Datatypes/Datatypes.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Jul 30 16:22:39 2013 +0200
@@ -0,0 +1,62 @@
+(*  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 {*
+  * 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:
+*}
+
+datatype_new 'a tree = Node 'a "('a tree fset)"
+
+text {*
+  * another advantage: it supports local definitions:
+*}
+
+context linorder
+begin
+
+datatype_new flag = Less | Eq | Greater
+
+end
+
+text {*
+
+ * in a future release, \cmd{datatype\_new} is expected to displace \cmd{datatype}
+
+ * 
+*}
+
+section {* Defining Datatypes *}
+
+text {*
+  * theory to include
+*}
+
+section {* Defining Primitive Recursive Functions *}
+
+section {* Defining Codatatypes *}
+
+section {* Defining Primitive Corecursive Functions *}
+
+section {* Registering Bounded Natural Functors *}
+
+section {* Generating Free Constructor Theorems *}
+
+section {* Conclusion *}
+
+end
diff -r 9e4bb60f8007 -r 3e651be14fcd src/Doc/Datatypes/document/build
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/Datatypes/document/build	Tue Jul 30 16:22:39 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 9e4bb60f8007 -r 3e651be14fcd 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 16:22:39 2013 +0200
@@ -0,0 +1,43 @@
+\documentclass[12pt,a4paper,fleqn]{article}
+\usepackage{latexsym}
+\usepackage{graphicx}
+\usepackage{iman}
+\usepackage{extra}
+\usepackage{isar}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{style}
+\usepackage{pdfsetup}
+
+\newcommand{\cmd}[1]{\isacommand{#1}}
+
+\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 \cmd{\_new} commands are designed to subsume, and eventually
+replace, the corresponding commands from the old datatype package.
+\end{abstract}
+
+\input{Datatypes.tex}
+
+\let\em=\sl
+\bibliography{manual}{}
+\bibliographystyle{abbrv}
+
+\end{document}
diff -r 9e4bb60f8007 -r 3e651be14fcd 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 16:22:39 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 9e4bb60f8007 -r 3e651be14fcd src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Jul 30 16:22:39 2013 +0200
+++ b/src/Doc/ROOT	Tue Jul 30 16:22:39 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