52792
|
1 |
(* Title: Doc/Datatypes/Datatypes.thy
|
|
2 |
Author: Jasmin Blanchette, TU Muenchen
|
|
3 |
|
|
4 |
Tutorial for (co)datatype definitions with the new package.
|
|
5 |
*)
|
|
6 |
|
|
7 |
theory Datatypes
|
52824
|
8 |
imports Setup
|
52792
|
9 |
begin
|
|
10 |
|
|
11 |
section {* Introduction *}
|
|
12 |
|
|
13 |
text {*
|
52794
|
14 |
The 2013 edition of Isabelle introduced new definitional package for datatypes
|
|
15 |
and codatatypes. The datatype support is similar to that provided by the earlier
|
|
16 |
package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL};
|
52822
|
17 |
indeed, replacing @{command datatype} by @{command datatype_new} is usually sufficient
|
52794
|
18 |
to port existing specifications to the new package. What makes the new package
|
|
19 |
attractive is that it supports definitions with recursion through a large class
|
|
20 |
of non-datatypes, notably finite sets:
|
52792
|
21 |
*}
|
|
22 |
|
52805
|
23 |
datatype_new 'a treeFS = TreeFS 'a "'a treeFS fset"
|
52792
|
24 |
|
|
25 |
text {*
|
52794
|
26 |
\noindent
|
|
27 |
Another advantage of the new package is that it supports local definitions:
|
52792
|
28 |
*}
|
|
29 |
|
52805
|
30 |
context linorder
|
|
31 |
begin
|
|
32 |
datatype_new flag = Less | Eq | Greater
|
|
33 |
end
|
52792
|
34 |
|
|
35 |
text {*
|
52794
|
36 |
\noindent
|
|
37 |
Finally, the package also provides some convenience, notably automatically
|
52822
|
38 |
generated destructors.
|
52794
|
39 |
|
52822
|
40 |
The command @{command datatype_new} is expected to displace @{command datatype} in a future
|
|
41 |
release. Authors of new theories are encouraged to use @{command datatype_new}, and
|
52805
|
42 |
maintainers of older theories may want to consider upgrading in the coming months.
|
52794
|
43 |
|
|
44 |
The package also provides codatatypes (or ``coinductive datatypes''), which may
|
52805
|
45 |
have infinite values. The following command introduces a codatatype of infinite
|
52794
|
46 |
streams:
|
|
47 |
*}
|
|
48 |
|
52805
|
49 |
codatatype 'a stream = Stream 'a "'a stream"
|
52794
|
50 |
|
|
51 |
text {*
|
|
52 |
\noindent
|
|
53 |
Mixed inductive--coinductive recursion is possible via nesting.
|
|
54 |
Compare the following four examples:
|
|
55 |
*}
|
|
56 |
|
52805
|
57 |
datatype_new 'a treeFF = TreeFF 'a "'a treeFF list"
|
|
58 |
datatype_new 'a treeFI = TreeFI 'a "'a treeFF stream"
|
|
59 |
codatatype 'a treeIF = TreeIF 'a "'a treeFF list"
|
|
60 |
codatatype 'a treeII = TreeII 'a "'a treeFF stream"
|
52792
|
61 |
|
52794
|
62 |
text {*
|
|
63 |
To use the package, it is necessary to import the @{theory BNF} theory, which
|
52806
|
64 |
can be precompiled as the \textit{HOL-BNF} image. The following commands show
|
|
65 |
how to launch jEdit/PIDE with the image loaded and how to build the image
|
|
66 |
without launching jEdit:
|
52794
|
67 |
*}
|
|
68 |
|
|
69 |
text {*
|
|
70 |
\noindent
|
52806
|
71 |
\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\
|
52805
|
72 |
\ \ \ \ \texttt{isabelle build -b HOL-BNF}
|
52794
|
73 |
*}
|
|
74 |
|
|
75 |
text {*
|
52805
|
76 |
The package, like its predecessor, fully adheres to the LCF philosophy
|
|
77 |
\cite{mgordon79}: The characteristic theorems associated with the specified
|
|
78 |
(co)datatypes are derived rather than introduced axiomatically.%
|
|
79 |
\footnote{Nonetheless, if the \textit{quick\_and\_dirty} option is enabled, some
|
|
80 |
of the internal constructions and most of the internal proof obligations are
|
|
81 |
skipped.}
|
|
82 |
The package's metatheory is described in a pair of papers
|
|
83 |
\cite{traytel-et-al-2012,blanchette-et-al-wit}.
|
52792
|
84 |
*}
|
|
85 |
|
52794
|
86 |
text {*
|
|
87 |
This tutorial is organized as follows:
|
|
88 |
|
52805
|
89 |
\begin{itemize}
|
52822
|
90 |
\setlength{\itemsep}{0pt}
|
|
91 |
|
52805
|
92 |
\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
|
52822
|
93 |
describes how to specify datatypes using the @{command datatype_new} command.
|
52805
|
94 |
|
|
95 |
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
|
|
96 |
Functions,'' describes how to specify recursive functions using
|
52824
|
97 |
\keyw{primrec\_new}, @{command fun}, and @{command function}.
|
52805
|
98 |
|
|
99 |
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
|
52822
|
100 |
describes how to specify codatatypes using the @{command codatatype} command.
|
52805
|
101 |
|
|
102 |
\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
|
|
103 |
Functions,'' describes how to specify corecursive functions using the
|
52824
|
104 |
\keyw{primcorec} command.
|
52794
|
105 |
|
52805
|
106 |
\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
|
|
107 |
Bounded Natural Functors,'' explains how to set up the (co)datatype package to
|
|
108 |
allow nested recursion through custom well-behaved type constructors.
|
|
109 |
|
|
110 |
\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free
|
|
111 |
Constructor Theorems,'' explains how to derive convenience theorems for free
|
52822
|
112 |
constructors, as performed internally by @{command datatype_new} and
|
|
113 |
@{command codatatype}.
|
52794
|
114 |
|
52805
|
115 |
\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
|
|
116 |
describes the package's programmatic interface.
|
52794
|
117 |
|
52805
|
118 |
\item Section \ref{sec:interoperability}, ``Interoperability,''
|
|
119 |
is concerned with the packages' interaction with other Isabelle packages and
|
|
120 |
tools, such as the code generator and the counterexample generators.
|
|
121 |
|
|
122 |
\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
|
52822
|
123 |
Limitations,'' concludes with known open issues at the time of writing.
|
52805
|
124 |
\end{itemize}
|
52822
|
125 |
|
|
126 |
|
|
127 |
\newbox\boxA
|
|
128 |
\setbox\boxA=\hbox{\texttt{nospam}}
|
|
129 |
|
|
130 |
\newcommand\authoremaili{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak
|
|
131 |
in.\allowbreak tum.\allowbreak de}}
|
|
132 |
\newcommand\authoremailii{\texttt{pope{\color{white}nospam}\kern-\wd\boxA{}scua@\allowbreak
|
|
133 |
in.\allowbreak tum.\allowbreak de}}
|
|
134 |
\newcommand\authoremailiii{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak
|
|
135 |
in.\allowbreak tum.\allowbreak de}}
|
|
136 |
|
|
137 |
\noindent
|
|
138 |
Comments and bug reports concerning either
|
|
139 |
the tool or the manual should be directed to the authors at
|
|
140 |
\authoremaili, \authoremailii, and \authoremailiii.
|
|
141 |
|
|
142 |
\begin{framed}
|
|
143 |
\noindent
|
|
144 |
\textbf{Warning:} This document is under heavy construction. Please apologise
|
|
145 |
for its appearance and come back in a few months.
|
|
146 |
\end{framed}
|
|
147 |
|
52794
|
148 |
*}
|
|
149 |
|
52805
|
150 |
section {* Defining Datatypes%
|
|
151 |
\label{sec:defining-datatypes} *}
|
|
152 |
|
|
153 |
text {*
|
52822
|
154 |
This section describes how to specify datatypes using the @{command datatype_new}
|
52805
|
155 |
command. The command is first illustrated through concrete examples featuring
|
52822
|
156 |
different flavors of recursion. More examples can be found in the directory
|
|
157 |
\verb|~~/src/HOL/BNF/Examples|.
|
52805
|
158 |
*}
|
52792
|
159 |
|
52824
|
160 |
|
52794
|
161 |
subsection {* Introductory Examples *}
|
|
162 |
|
|
163 |
subsubsection {* Nonrecursive Types *}
|
|
164 |
|
52805
|
165 |
text {*
|
|
166 |
enumeration type:
|
|
167 |
*}
|
|
168 |
|
|
169 |
datatype_new trool = Truue | Faalse | Maaybe
|
|
170 |
|
|
171 |
text {*
|
|
172 |
Haskell-style option type:
|
|
173 |
*}
|
|
174 |
|
|
175 |
datatype_new 'a maybe = Nothing | Just 'a
|
|
176 |
|
|
177 |
text {*
|
|
178 |
triple:
|
|
179 |
*}
|
|
180 |
|
|
181 |
datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
|
|
182 |
|
52824
|
183 |
|
52794
|
184 |
subsubsection {* Simple Recursion *}
|
|
185 |
|
52805
|
186 |
text {*
|
|
187 |
simplest recursive type: natural numbers
|
|
188 |
*}
|
|
189 |
|
|
190 |
datatype_new nat = Zero | Suc nat
|
|
191 |
|
|
192 |
text {*
|
|
193 |
lists were shown in the introduction
|
|
194 |
|
|
195 |
terminated lists are a variant:
|
|
196 |
*}
|
|
197 |
|
|
198 |
datatype_new ('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
|
|
199 |
|
|
200 |
text {*
|
|
201 |
On the right-hand side of the equal sign, the usual Isabelle conventions apply:
|
|
202 |
Nonatomic types must be enclosed in double quotes.
|
|
203 |
*}
|
|
204 |
|
52824
|
205 |
|
52794
|
206 |
subsubsection {* Mutual Recursion *}
|
|
207 |
|
52805
|
208 |
text {*
|
|
209 |
Mutual recursion = Define several types simultaneously, referring to each other.
|
|
210 |
|
|
211 |
Simple example: distinction between even and odd natural numbers:
|
|
212 |
*}
|
|
213 |
|
|
214 |
datatype_new even_nat = Zero | Even_Suc odd_nat
|
|
215 |
and odd_nat = Odd_Suc even_nat
|
|
216 |
|
|
217 |
text {*
|
|
218 |
More complex, and more realistic, example:
|
|
219 |
*}
|
|
220 |
|
|
221 |
datatype_new ('a, 'b) expr =
|
52806
|
222 |
Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) expr"
|
52805
|
223 |
and ('a, 'b) trm =
|
|
224 |
Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
|
|
225 |
and ('a, 'b) factor =
|
|
226 |
Const 'a | Var 'b | Sub_Expr "('a, 'b) expr"
|
|
227 |
|
52824
|
228 |
|
52794
|
229 |
subsubsection {* Nested Recursion *}
|
|
230 |
|
52805
|
231 |
text {*
|
|
232 |
Nested recursion = Have recursion through a type constructor.
|
|
233 |
|
|
234 |
The introduction showed some examples of trees with nesting through lists.
|
|
235 |
|
|
236 |
More complex example, which reuses our maybe and triple types:
|
|
237 |
*}
|
|
238 |
|
|
239 |
datatype_new 'a triple_tree =
|
|
240 |
Triple_Tree "('a triple_tree maybe, bool, 'a triple_tree maybe) triple"
|
|
241 |
|
|
242 |
text {*
|
|
243 |
Recursion may not be arbitrary; e.g. impossible to define
|
|
244 |
*}
|
|
245 |
|
|
246 |
(*
|
|
247 |
datatype_new 'a foo = Foo (*<*) datatype_new 'a bar = Bar "'a foo \<Rightarrow> 'a foo"
|
|
248 |
*)
|
|
249 |
|
52806
|
250 |
datatype_new 'a evil = Evil (*<*)'a
|
|
251 |
typ (*>*)"'a evil \<Rightarrow> 'a evil"
|
|
252 |
|
|
253 |
text {*
|
|
254 |
Issue: => allows recursion only on its right-hand side.
|
|
255 |
This issue is inherited by polymorphic datatypes (and codatatypes)
|
|
256 |
defined in terms of =>.
|
|
257 |
In general, type constructors "('a1, ..., 'an) k" allow recursion on a subset
|
|
258 |
of their type arguments.
|
|
259 |
*}
|
|
260 |
|
|
261 |
|
52805
|
262 |
subsubsection {* Auxiliary Constants and Syntaxes *}
|
|
263 |
|
|
264 |
text {*
|
52822
|
265 |
The @{command datatype_new} command introduces various constants in addition to the
|
|
266 |
constructors. Given a type @{text "('a1,\<dots>,'aM) t"} with constructors
|
|
267 |
@{text t.C1}, \ldots, @{text t.C}$\!M,$ the following auxiliary constants are
|
|
268 |
introduced (among others):
|
|
269 |
|
|
270 |
\begin{itemize}
|
|
271 |
\setlength{\itemsep}{0pt}
|
|
272 |
|
|
273 |
\item \emph{Set functions} (\emph{natural transformations}): @{text t_set1},
|
|
274 |
\ldots, @{text t_set}$M$
|
|
275 |
|
|
276 |
\item \emph{Map function} (\emph{functorial action}): @{text t_map}
|
|
277 |
|
|
278 |
\item \emph{Relator}: @{text t_rel}
|
|
279 |
|
|
280 |
\item \emph{Iterator}: @{text t_fold}
|
|
281 |
|
|
282 |
\item \emph{Recursor}: @{text t_rec}
|
|
283 |
|
|
284 |
\item \emph{Discriminators}: @{text t.is_C1}, \ldots, @{text t.is_C}$\!M$
|
|
285 |
|
|
286 |
\item \emph{Selectors}:
|
|
287 |
@{text t.un_C11}, \ldots, @{text t.un_C1}$k_1$, \ldots,
|
|
288 |
@{text t.un_C}$\!M$@{text 1}, \ldots, @{text t.un_C}$\!Mk_M$
|
|
289 |
\end{itemize}
|
|
290 |
|
|
291 |
The discriminators and selectors are collectively called \emph{destructors}.
|
|
292 |
The @{text "t."} prefix is optional.
|
|
293 |
|
|
294 |
The set functions, map function, relator, discriminators, and selectors can be
|
|
295 |
given custom names, as in the example below:
|
|
296 |
*}
|
|
297 |
|
|
298 |
(*<*)hide_const Nil Cons hd tl(*>*)
|
|
299 |
datatype_new (set: 'a) list (map: map rel: list_all2) =
|
|
300 |
null: Nil (defaults tl: Nil)
|
|
301 |
| Cons (hd: 'a) (tl: "'a list")
|
|
302 |
|
|
303 |
text {*
|
|
304 |
\noindent
|
|
305 |
The command introduces a discriminator @{const null} and a pair of selectors
|
|
306 |
@{const hd} and @{const tl} characterized as follows:
|
|
307 |
%
|
|
308 |
\[@{thm list.collapse(1)[of xs, no_vars]}
|
|
309 |
\qquad @{thm list.collapse(2)[of xs, no_vars]}\]
|
|
310 |
%
|
|
311 |
For two-constructor datatypes, a single discriminator constant suffices. The
|
|
312 |
discriminator associated with @{const Cons} is simply @{text "\<not> null"}.
|
|
313 |
|
52824
|
314 |
The \keyw{defaults} keyword following the @{const Nil} constructor specifies a
|
52822
|
315 |
default value for selectors associated with other constructors. Here, it is
|
|
316 |
used to specify that the tail of the empty list is the empty list (instead of
|
|
317 |
being unspecified).
|
|
318 |
|
|
319 |
Because @{const Nil} is a nullary constructor, it is also possible to use @{text
|
|
320 |
"= Nil"} as a discriminator. This is specified by specifying @{text "="} instead
|
|
321 |
of the identifier @{const null} in the declaration above. Although this may look
|
|
322 |
appealing, the mixture of constructors and selectors in the resulting
|
|
323 |
characteristic theorems can lead Isabelle's automation to switch between the
|
|
324 |
constructor and the destructor view in surprising ways.
|
|
325 |
*}
|
|
326 |
|
|
327 |
text {*
|
|
328 |
The usual mixfix syntaxes are available for both types and constructors. For example:
|
|
329 |
|
|
330 |
%%% FIXME: remove trailing underscore and use locale trick instead once this is
|
|
331 |
%%% supported.
|
52805
|
332 |
*}
|
52794
|
333 |
|
52822
|
334 |
datatype_new ('a, 'b) prod (infixr "*" 20) =
|
|
335 |
Pair 'a 'b
|
|
336 |
|
|
337 |
datatype_new (set_: 'a) list_ =
|
|
338 |
null: Nil ("[]")
|
|
339 |
| Cons (hd: 'a) (tl: "'a list_") (infixr "#" 65)
|
|
340 |
|
52824
|
341 |
|
52794
|
342 |
subsection {* General Syntax *}
|
|
343 |
|
52822
|
344 |
text {*
|
|
345 |
Datatype definitions have the following general syntax:
|
|
346 |
|
52824
|
347 |
@{rail "
|
|
348 |
@@{command datatype_new} ('(' (@{syntax dt_option} + ',') ')')? \\
|
|
349 |
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
|
|
350 |
"}
|
|
351 |
|
|
352 |
Two options are supported:
|
52822
|
353 |
|
52824
|
354 |
@{rail "
|
|
355 |
@{syntax_def dt_option}: @'no_dests' | @'rep_compat'
|
|
356 |
"}
|
52822
|
357 |
|
52824
|
358 |
\begin{itemize}
|
|
359 |
\setlength{\itemsep}{0pt}
|
|
360 |
|
|
361 |
\item
|
|
362 |
The \keyw{no\_dests} option indicates that no destructors (i.e.,
|
|
363 |
discriminators and selectors) should be generated.
|
52822
|
364 |
|
52824
|
365 |
\item
|
|
366 |
The \keyw{rep\_compat} option indicates that the names generated by the
|
|
367 |
package should contain optional (and normally not displayed) @{text "new."}
|
|
368 |
components to prevent clashes with a later call to @{command rep_datatype}. See
|
|
369 |
Section~\ref{ssec:datatype-compatibility-issues} for details.
|
|
370 |
\end{itemize}
|
52822
|
371 |
|
52824
|
372 |
Left-hand sides specify the name of the type to define, its type parameters,
|
|
373 |
and more:
|
52822
|
374 |
|
52824
|
375 |
@{rail "
|
|
376 |
@{syntax_def dt_name}: @{syntax type_params}? @{syntax name} \\
|
|
377 |
@{syntax map_rel}? @{syntax mixfix}?
|
|
378 |
;
|
|
379 |
@{syntax_def type_params}: @{syntax typefree} | '(' ((@{syntax name} ':')? @{syntax typefree} + ',') ')'
|
|
380 |
;
|
|
381 |
@{syntax_def map_rel}: '(' ((('map' | 'rel') ':' @{syntax name}) +) ')'
|
|
382 |
"}
|
52822
|
383 |
|
52824
|
384 |
@{syntax name} specifies the type name ...
|
52822
|
385 |
|
52824
|
386 |
@{syntax typefree} is type variable ('a, 'b, \ldots)
|
|
387 |
The names are for the set functions.
|
52822
|
388 |
|
|
389 |
Additional constraint: All mutually recursive datatypes defined together must
|
|
390 |
specify the same type variables in the same order.
|
|
391 |
|
52824
|
392 |
@{syntax mixfix} is the usual parenthesized mixfix notation, documented in the
|
|
393 |
Isar reference manual \cite{isabelle-isar-ref}.
|
52822
|
394 |
|
52824
|
395 |
@{rail "
|
|
396 |
@{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} *) \\
|
|
397 |
@{syntax sel_defaults}? @{syntax mixfix}?
|
|
398 |
"}
|
|
399 |
|
52822
|
400 |
|
|
401 |
First, optional name: discriminator. Second, mandatory name: name of
|
|
402 |
constructor. Default names for discriminators are generated.
|
|
403 |
|
52824
|
404 |
@{rail "
|
|
405 |
@{syntax_def ctor_arg}: @{syntax type} | '(' (@{syntax name} ':')? @{syntax type} ')'
|
|
406 |
;
|
|
407 |
@{syntax_def sel_defaults}: '(' @'defaults' (@{syntax name} ':' @{syntax term} *) ')'
|
|
408 |
"}
|
52822
|
409 |
*}
|
|
410 |
|
|
411 |
|
52794
|
412 |
subsection {* Characteristic Theorems *}
|
|
413 |
|
52824
|
414 |
|
|
415 |
subsection {* Compatibility Issues%
|
|
416 |
\label{ssec:datatype-compatibility-issues} *}
|
52794
|
417 |
|
52792
|
418 |
|
52805
|
419 |
section {* Defining Recursive Functions%
|
|
420 |
\label{sec:defining-recursive-functions} *}
|
|
421 |
|
|
422 |
text {*
|
|
423 |
This describes how to specify recursive functions over datatypes
|
52824
|
424 |
specified using @{command datatype_new}. The focus in on the \keyw{primrec\_new}
|
52805
|
425 |
command, which supports primitive recursion. A few examples feature the
|
52822
|
426 |
@{command fun} and @{command function} commands, described in a separate
|
|
427 |
tutorial \cite{isabelle-function}.
|
52805
|
428 |
%%% TODO: partial_function?
|
|
429 |
*}
|
52792
|
430 |
|
52824
|
431 |
|
52794
|
432 |
subsection {* Introductory Examples *}
|
|
433 |
|
52805
|
434 |
text {*
|
|
435 |
More examples in \verb|~~/src/HOL/BNF/Examples|.
|
|
436 |
*}
|
|
437 |
|
52824
|
438 |
|
52794
|
439 |
subsection {* General Syntax *}
|
|
440 |
|
52824
|
441 |
|
52794
|
442 |
subsection {* Characteristic Theorems *}
|
|
443 |
|
52824
|
444 |
|
52794
|
445 |
subsection {* Compatibility Issues *}
|
|
446 |
|
|
447 |
|
52805
|
448 |
section {* Defining Codatatypes%
|
|
449 |
\label{sec:defining-codatatypes} *}
|
|
450 |
|
|
451 |
text {*
|
52822
|
452 |
This section describes how to specify codatatypes using the @{command codatatype}
|
52805
|
453 |
command.
|
|
454 |
*}
|
52792
|
455 |
|
52824
|
456 |
|
52794
|
457 |
subsection {* Introductory Examples *}
|
|
458 |
|
52805
|
459 |
text {*
|
|
460 |
More examples in \verb|~~/src/HOL/BNF/Examples|.
|
|
461 |
*}
|
|
462 |
|
52824
|
463 |
|
52805
|
464 |
subsection {* General Syntax *}
|
|
465 |
|
52824
|
466 |
text {*
|
|
467 |
\keyw{no\_dests} is not available.
|
|
468 |
*}
|
|
469 |
|
52805
|
470 |
subsection {* Characteristic Theorems *}
|
|
471 |
|
|
472 |
|
|
473 |
section {* Defining Corecursive Functions%
|
|
474 |
\label{sec:defining-corecursive-functions} *}
|
|
475 |
|
|
476 |
text {*
|
|
477 |
This section describes how to specify corecursive functions using the
|
52824
|
478 |
\keyw{primcorec} command.
|
52805
|
479 |
*}
|
|
480 |
|
52824
|
481 |
|
52805
|
482 |
subsection {* Introductory Examples *}
|
|
483 |
|
|
484 |
text {*
|
|
485 |
More examples in \verb|~~/src/HOL/BNF/Examples|.
|
|
486 |
*}
|
|
487 |
|
52824
|
488 |
|
52794
|
489 |
subsection {* General Syntax *}
|
|
490 |
|
52824
|
491 |
|
52794
|
492 |
subsection {* Characteristic Theorems *}
|
|
493 |
|
|
494 |
|
52805
|
495 |
section {* Registering Bounded Natural Functors%
|
|
496 |
\label{sec:registering-bounded-natural-functors} *}
|
52792
|
497 |
|
52805
|
498 |
text {*
|
|
499 |
This section explains how to set up the (co)datatype package to allow nested
|
|
500 |
recursion through custom well-behaved type constructors. The key concept is that
|
|
501 |
of a bounded natural functor (BNF).
|
|
502 |
*}
|
|
503 |
|
52824
|
504 |
|
52805
|
505 |
subsection {* Introductory Example *}
|
|
506 |
|
|
507 |
text {*
|
|
508 |
More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and
|
|
509 |
\verb|~~/src/HOL/BNF/More_BNFs.thy|.
|
52806
|
510 |
|
|
511 |
Mention distinction between live and dead type arguments;
|
|
512 |
mention =>.
|
52805
|
513 |
*}
|
52794
|
514 |
|
52824
|
515 |
|
52794
|
516 |
subsection {* General Syntax *}
|
|
517 |
|
52805
|
518 |
|
|
519 |
section {* Generating Free Constructor Theorems%
|
|
520 |
\label{sec:generating-free-constructor-theorems} *}
|
52794
|
521 |
|
52805
|
522 |
text {*
|
|
523 |
This section explains how to derive convenience theorems for free constructors,
|
52822
|
524 |
as performed internally by @{command datatype_new} and @{command codatatype}.
|
52794
|
525 |
|
52805
|
526 |
* need for this is rare but may arise if you want e.g. to add destructors to
|
|
527 |
a type not introduced by ...
|
52794
|
528 |
|
52805
|
529 |
* also useful for compatibility with old package, e.g. add destructors to
|
52822
|
530 |
old @{command datatype}
|
52805
|
531 |
*}
|
52792
|
532 |
|
52824
|
533 |
|
52794
|
534 |
subsection {* Introductory Example *}
|
|
535 |
|
52824
|
536 |
|
52794
|
537 |
subsection {* General Syntax *}
|
|
538 |
|
|
539 |
|
52805
|
540 |
section {* Standard ML Interface%
|
|
541 |
\label{sec:standard-ml-interface} *}
|
52792
|
542 |
|
52805
|
543 |
text {*
|
|
544 |
This section describes the package's programmatic interface.
|
|
545 |
*}
|
52794
|
546 |
|
|
547 |
|
52805
|
548 |
section {* Interoperability%
|
|
549 |
\label{sec:interoperability} *}
|
52794
|
550 |
|
52805
|
551 |
text {*
|
|
552 |
This section is concerned with the packages' interaction with other Isabelle
|
|
553 |
packages and tools, such as the code generator and the counterexample
|
|
554 |
generators.
|
|
555 |
*}
|
52794
|
556 |
|
52824
|
557 |
|
52794
|
558 |
subsection {* Transfer and Lifting *}
|
|
559 |
|
52824
|
560 |
|
52794
|
561 |
subsection {* Code Generator *}
|
|
562 |
|
52824
|
563 |
|
52794
|
564 |
subsection {* Quickcheck *}
|
|
565 |
|
52824
|
566 |
|
52794
|
567 |
subsection {* Nitpick *}
|
|
568 |
|
52824
|
569 |
|
52794
|
570 |
subsection {* Nominal Isabelle *}
|
|
571 |
|
52805
|
572 |
|
|
573 |
section {* Known Bugs and Limitations%
|
|
574 |
\label{sec:known-bugs-and-limitations} *}
|
|
575 |
|
|
576 |
text {*
|
|
577 |
This section lists known open issues of the package.
|
|
578 |
*}
|
52794
|
579 |
|
|
580 |
text {*
|
52806
|
581 |
* primrec\_new and primcorec are vaporware
|
|
582 |
|
52794
|
583 |
* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
|
52806
|
584 |
|
|
585 |
* issues with HOL-Proofs?
|
|
586 |
|
|
587 |
* partial documentation
|
|
588 |
|
|
589 |
* too much output by commands like "datatype_new" and "codatatype"
|
52822
|
590 |
|
|
591 |
* no direct way to define recursive functions for default values -- but show trick
|
|
592 |
based on overloading
|
|
593 |
*}
|
|
594 |
|
|
595 |
|
|
596 |
section {* Acknowledgments%
|
|
597 |
\label{sec:acknowledgments} *}
|
|
598 |
|
|
599 |
text {*
|
|
600 |
* same people as usual
|
52824
|
601 |
* Tobias Nipkow
|
|
602 |
* Makarius Wenzel
|
|
603 |
* Andreas Lochbihler
|
52822
|
604 |
* Brian Huffman
|
52824
|
605 |
* also:
|
|
606 |
* Stefan Milius
|
|
607 |
* Lutz Schr\"oder
|
52794
|
608 |
*}
|
52792
|
609 |
|
|
610 |
end
|