# HG changeset patch # User blanchet # Date 1379083835 -7200 # Node ID 27d2c98d9d9f029656735a38a8f3f6b7896a430a # Parent 4161d2b96b8ce715b3a95a65a721506d9d50f739 more (co)data docs diff -r 4161d2b96b8c -r 27d2c98d9d9f src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 16:30:16 2013 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 16:50:35 2013 +0200 @@ -25,7 +25,7 @@ to use the new package. Perhaps the main advantage of the new package is that it supports recursion -through a large class of non-datatypes, comprising finite sets: +through a large class of non-datatypes, such as finite sets: *} datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s 'a "'a tree\<^sub>f\<^sub>s fset" @@ -1050,6 +1050,7 @@ *} +(* subsection {* Generated Theorems \label{ssec:primrec-generated-theorems} *} @@ -1063,6 +1064,8 @@ % * fold, rec % * mutualized *} +*) + subsection {* Recursive Default Values for Selectors \label{ssec:recursive-default-values-for-selectors} *} @@ -1099,15 +1102,20 @@ for @{text "un_D\<^sub>0"}. \end{enumerate} +\noindent The following example illustrates this procedure: *} consts termi\<^sub>0 :: 'a +text {* \blankline *} + datatype_new ('a, 'b) tlist = TNil (termi: 'b) (defaults ttl: TNil) | TCons (thd: 'a) (ttl : "('a, 'b) tlist") (defaults termi: "\_ xs. termi\<^sub>0 xs") +text {* \blankline *} + overloading termi\<^sub>0 \ "termi\<^sub>0 \ ('a, 'b) tlist \ 'b" begin @@ -1116,6 +1124,8 @@ "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs" end +text {* \blankline *} + lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs" by (cases xs) auto @@ -1140,25 +1150,31 @@ \label{sec:defining-codatatypes} *} text {* -This section describes how to specify codatatypes using the @{command codatatype} -command. - -% * libraries include some useful codatatypes, notably lazy lists; -% see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library +This section describes how to specify codatatypes using the @{command +codatatype} command. The command is first illustrated through concrete examples +featuring different flavors of corecursion. More examples can be found in the +directory \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} +also includes some useful codatatypes, notably for lazy lists +\cite{lochbihler-2010}. *} +(* subsection {* Introductory Examples \label{ssec:codatatype-introductory-examples} *} text {* More examples in \verb|~~/src/HOL/BNF/Examples|. *} +*) subsection {* Command Syntax \label{ssec:codatatype-command-syntax} *} + +subsubsection {* \keyw{codatatype} *} + text {* Definitions of codatatypes have almost exactly the same syntax as for datatypes (Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command @@ -1167,12 +1183,16 @@ *} +(* subsection {* Generated Constants \label{ssec:codatatype-generated-constants} *} +*) +(* subsection {* Generated Theorems \label{ssec:codatatype-generated-theorems} *} +*) section {* Defining Corecursive Functions @@ -1187,6 +1207,7 @@ *} +(* subsection {* Introductory Examples \label{ssec:primcorec-introductory-examples} *} @@ -1196,6 +1217,7 @@ Also, for default values, the same trick as for datatypes is possible for codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}). *} +*) subsection {* Command Syntax @@ -1216,8 +1238,10 @@ *} +(* subsection {* Generated Theorems \label{ssec:primcorec-generated-theorems} *} +*) section {* Registering Bounded Natural Functors @@ -1231,6 +1255,7 @@ *} +(* subsection {* Introductory Example \label{ssec:bnf-introductory-example} *} @@ -1242,6 +1267,7 @@ % * and existence of map, set for those %mention =>. *} +*) subsection {* Command Syntax @@ -1257,8 +1283,6 @@ ; X_list: '[' (X + ',') ']' "} - -options: no_discs_sels rep_compat *} @@ -1288,8 +1312,10 @@ *} +(* subsection {* Introductory Example \label{ssec:ctors-introductory-example} *} +*) subsection {* Command Syntax @@ -1377,19 +1403,16 @@ % %* partial documentation % -%* too much output by commands like "datatype_new" and "codatatype" -% -%* no direct way to define recursive functions for default values -- but show trick -% based on overloading -% %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them % (for @{command datatype_new_compat} and prim(co)rec) % -%* no way to register same type as both data- and codatatype? +% * a fortiori, no way to register same type as both data- and codatatype % %* no recursion through unused arguments (unlike with the old package) % %* in a locale, cannot use locally fixed types (because of limitation in typedef)? +% +% *names of variables suboptimal *} diff -r 4161d2b96b8c -r 27d2c98d9d9f src/Doc/Datatypes/document/root.tex --- a/src/Doc/Datatypes/document/root.tex Fri Sep 13 16:30:16 2013 +0200 +++ b/src/Doc/Datatypes/document/root.tex Fri Sep 13 16:50:35 2013 +0200 @@ -45,9 +45,9 @@ \title{%\includegraphics[scale=0.5]{isabelle_hol} \\[4ex] Defining (Co)datatypes in Isabelle/HOL} \author{\hbox{} \\ -Jasmin Christian Blanchette \\ -Lorenz Panny \\ -Andrei Popescu \\ +Jasmin Christian Blanchette, +Lorenz Panny, \\ +Andrei Popescu, and Dmitriy Traytel \\ {\normalsize Institut f\"ur Informatik, Technische Universit\"at M\"unchen} \\ \hbox{}} @@ -58,10 +58,11 @@ \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: -\keyw{datatype\_new}, \keyw{codatatype}, \keyw{primrec\_new}, and \keyw{primcorec}. -The commands suffixed by \keyw{\_new} are intended to subsume, and eventually -replace, the corresponding commands from the old datatype package. +codatatypes in Isabelle/HOL. The package provides four main commands: +\keyw{datatype\_new}, \keyw{codatatype}, \keyw{primrec\_new}, and +\keyw{primcorec}. The commands suffixed by \keyw{\_new} are intended to subsume, +and eventually replace, the corresponding commands from the old datatype +package. \end{abstract} \tableofcontents