author | blanchet |
Mon, 12 Aug 2013 15:25:17 +0200 | |
changeset 52969 | f2df0730f8ac |
parent 52868 | cca9e958da5c |
child 53018 | 11ebef554439 |
permissions | -rw-r--r-- |
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 |
52840 | 9 |
keywords |
10 |
"primrec_new" :: thy_decl and |
|
11 |
"primcorec" :: thy_decl |
|
52792 | 12 |
begin |
13 |
||
52840 | 14 |
(*<*) |
15 |
(* FIXME: Evil setup until "primrec_new" and "primcorec" are in place. *) |
|
16 |
ML_command {* |
|
17 |
fun add_dummy_cmd _ _ lthy = lthy; |
|
52828 | 18 |
|
52840 | 19 |
val _ = Outer_Syntax.local_theory @{command_spec "primrec_new"} "" |
20 |
(Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd); |
|
52828 | 21 |
|
52840 | 22 |
val _ = Outer_Syntax.local_theory @{command_spec "primcorec"} "" |
23 |
(Parse.fixes -- Parse_Spec.where_alt_specs >> uncurry add_dummy_cmd); |
|
52828 | 24 |
*} |
52840 | 25 |
(*>*) |
26 |
||
52828 | 27 |
|
28 |
section {* Introduction |
|
29 |
\label{sec:introduction} *} |
|
52792 | 30 |
|
31 |
text {* |
|
52794 | 32 |
The 2013 edition of Isabelle introduced new definitional package for datatypes |
33 |
and codatatypes. The datatype support is similar to that provided by the earlier |
|
52828 | 34 |
package due to Berghofer and Wenzel \cite{Berghofer-Wenzel:1999:TPHOL}, |
35 |
documented in the Isar reference manual \cite{isabelle-isar-ref}; |
|
52840 | 36 |
indeed, replacing the keyword @{command datatype} by @{command datatype_new} is |
37 |
usually all that is needed to port existing theories to use the new package. |
|
38 |
||
52841 | 39 |
Perhaps the main advantage of the new package is that it supports recursion |
40 |
through a large class of non-datatypes, comprising finite sets: |
|
52792 | 41 |
*} |
42 |
||
52840 | 43 |
datatype_new 'a treeFS = NodeFS 'a "'a treeFS fset" |
52792 | 44 |
|
45 |
text {* |
|
52794 | 46 |
\noindent |
52840 | 47 |
Another strong point is that the package supports local definitions: |
52792 | 48 |
*} |
49 |
||
52805 | 50 |
context linorder |
51 |
begin |
|
52841 | 52 |
datatype_new flag = Less | Eq | Greater |
52805 | 53 |
end |
52792 | 54 |
|
55 |
text {* |
|
52794 | 56 |
\noindent |
52840 | 57 |
The package also provides some convenience, notably automatically generated |
52841 | 58 |
destructors (discriminators and selectors). |
52794 | 59 |
|
52840 | 60 |
In addition to plain inductive datatypes, the package supports coinductive |
61 |
datatypes, or \emph{codatatypes}, which may have infinite values. For example, |
|
52843 | 62 |
the following command introduces the type of lazy lists: |
52794 | 63 |
*} |
64 |
||
52843 | 65 |
codatatype 'a llist = LNil | LCons 'a "'a llist" |
52794 | 66 |
|
67 |
text {* |
|
68 |
\noindent |
|
52840 | 69 |
Mixed inductive--coinductive recursion is possible via nesting. Compare the |
70 |
following four examples: |
|
52843 | 71 |
|
72 |
%%% TODO: Avoid 0 |
|
52794 | 73 |
*} |
74 |
||
52843 | 75 |
datatype_new 'a treeFF0 = NodeFF 'a "'a treeFF0 list" |
76 |
datatype_new 'a treeFI0 = NodeFI 'a "'a treeFI0 llist" |
|
77 |
codatatype 'a treeIF0 = NodeIF 'a "'a treeIF0 list" |
|
78 |
codatatype 'a treeII0 = NodeII 'a "'a treeII0 llist" |
|
52792 | 79 |
|
52794 | 80 |
text {* |
52840 | 81 |
The first two tree types allow only finite branches, whereas the last two allow |
82 |
infinite branches. Orthogonally, the nodes in the first and third types have |
|
52843 | 83 |
finite branching, whereas those of the second and fourth may have infinitely |
84 |
many direct subtrees. |
|
52840 | 85 |
|
52794 | 86 |
To use the package, it is necessary to import the @{theory BNF} theory, which |
52806 | 87 |
can be precompiled as the \textit{HOL-BNF} image. The following commands show |
88 |
how to launch jEdit/PIDE with the image loaded and how to build the image |
|
89 |
without launching jEdit: |
|
52794 | 90 |
*} |
91 |
||
92 |
text {* |
|
93 |
\noindent |
|
52806 | 94 |
\ \ \ \ \texttt{isabelle jedit -l HOL-BNF} \\ |
52827 | 95 |
\noindent |
52828 | 96 |
\hbox{}\ \ \ \ \texttt{isabelle build -b HOL-BNF} |
52794 | 97 |
*} |
98 |
||
99 |
text {* |
|
52805 | 100 |
The package, like its predecessor, fully adheres to the LCF philosophy |
101 |
\cite{mgordon79}: The characteristic theorems associated with the specified |
|
102 |
(co)datatypes are derived rather than introduced axiomatically.% |
|
52841 | 103 |
\footnote{If the \textit{quick\_and\_dirty} option is enabled, some of the |
104 |
internal constructions and most of the internal proof obligations are skipped.} |
|
52805 | 105 |
The package's metatheory is described in a pair of papers |
106 |
\cite{traytel-et-al-2012,blanchette-et-al-wit}. |
|
52792 | 107 |
|
52794 | 108 |
This tutorial is organized as follows: |
109 |
||
52805 | 110 |
\begin{itemize} |
52822 | 111 |
\setlength{\itemsep}{0pt} |
112 |
||
52805 | 113 |
\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,'' |
52822 | 114 |
describes how to specify datatypes using the @{command datatype_new} command. |
52805 | 115 |
|
116 |
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive |
|
117 |
Functions,'' describes how to specify recursive functions using |
|
52824 | 118 |
\keyw{primrec\_new}, @{command fun}, and @{command function}. |
52805 | 119 |
|
120 |
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,'' |
|
52822 | 121 |
describes how to specify codatatypes using the @{command codatatype} command. |
52805 | 122 |
|
123 |
\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive |
|
124 |
Functions,'' describes how to specify corecursive functions using the |
|
52824 | 125 |
\keyw{primcorec} command. |
52794 | 126 |
|
52805 | 127 |
\item Section \ref{sec:registering-bounded-natural-functors}, ``Registering |
128 |
Bounded Natural Functors,'' explains how to set up the (co)datatype package to |
|
129 |
allow nested recursion through custom well-behaved type constructors. |
|
130 |
||
131 |
\item Section \ref{sec:generating-free-constructor-theorems}, ``Generating Free |
|
132 |
Constructor Theorems,'' explains how to derive convenience theorems for free |
|
52822 | 133 |
constructors, as performed internally by @{command datatype_new} and |
134 |
@{command codatatype}. |
|
52794 | 135 |
|
52805 | 136 |
\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,'' |
137 |
describes the package's programmatic interface. |
|
52794 | 138 |
|
52805 | 139 |
\item Section \ref{sec:interoperability}, ``Interoperability,'' |
140 |
is concerned with the packages' interaction with other Isabelle packages and |
|
141 |
tools, such as the code generator and the counterexample generators. |
|
142 |
||
143 |
\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and |
|
52822 | 144 |
Limitations,'' concludes with known open issues at the time of writing. |
52805 | 145 |
\end{itemize} |
52822 | 146 |
|
147 |
||
148 |
\newbox\boxA |
|
149 |
\setbox\boxA=\hbox{\texttt{nospam}} |
|
150 |
||
151 |
\newcommand\authoremaili{\texttt{blan{\color{white}nospam}\kern-\wd\boxA{}chette@\allowbreak |
|
152 |
in.\allowbreak tum.\allowbreak de}} |
|
153 |
\newcommand\authoremailii{\texttt{pope{\color{white}nospam}\kern-\wd\boxA{}scua@\allowbreak |
|
154 |
in.\allowbreak tum.\allowbreak de}} |
|
155 |
\newcommand\authoremailiii{\texttt{tray{\color{white}nospam}\kern-\wd\boxA{}tel@\allowbreak |
|
156 |
in.\allowbreak tum.\allowbreak de}} |
|
157 |
||
52841 | 158 |
The command @{command datatype_new} is expected to displace @{command datatype} |
159 |
in a future release. Authors of new theories are encouraged to use |
|
160 |
@{command datatype_new}, and maintainers of older theories may want to consider |
|
161 |
upgrading in the coming months. |
|
162 |
||
163 |
Comments and bug reports concerning either the tool or this tutorial should be |
|
164 |
directed to the authors at \authoremaili, \authoremailii, and \authoremailiii. |
|
52822 | 165 |
|
166 |
\begin{framed} |
|
167 |
\noindent |
|
52841 | 168 |
\textbf{Warning:} This tutorial is under heavy construction. Please apologise |
52827 | 169 |
for its appearance and come back in a few months. If you have ideas regarding |
170 |
material that should be included, please let the authors know. |
|
52822 | 171 |
\end{framed} |
172 |
||
52794 | 173 |
*} |
174 |
||
52827 | 175 |
section {* Defining Datatypes |
52805 | 176 |
\label{sec:defining-datatypes} *} |
177 |
||
178 |
text {* |
|
52822 | 179 |
This section describes how to specify datatypes using the @{command datatype_new} |
52805 | 180 |
command. The command is first illustrated through concrete examples featuring |
52822 | 181 |
different flavors of recursion. More examples can be found in the directory |
182 |
\verb|~~/src/HOL/BNF/Examples|. |
|
52843 | 183 |
|
184 |
* libraries include many useful datatypes, e.g. list, option, etc., as well |
|
185 |
as operations on these; |
|
186 |
see e.g. ``What's in Main'' \cite{xxx} |
|
52805 | 187 |
*} |
52792 | 188 |
|
52824 | 189 |
|
52840 | 190 |
subsection {* Examples |
191 |
\label{ssec:datatype-examples} *} |
|
52794 | 192 |
|
193 |
subsubsection {* Nonrecursive Types *} |
|
194 |
||
52805 | 195 |
text {* |
196 |
enumeration type: |
|
197 |
*} |
|
198 |
||
52828 | 199 |
datatype_new trool = Truue | Faalse | Perhaaps |
52805 | 200 |
|
201 |
text {* |
|
202 |
Haskell-style option type: |
|
203 |
*} |
|
204 |
||
205 |
datatype_new 'a maybe = Nothing | Just 'a |
|
206 |
||
207 |
text {* |
|
208 |
triple: |
|
209 |
*} |
|
210 |
||
211 |
datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c |
|
212 |
||
52824 | 213 |
|
52794 | 214 |
subsubsection {* Simple Recursion *} |
215 |
||
52805 | 216 |
text {* |
217 |
simplest recursive type: natural numbers |
|
218 |
*} |
|
219 |
||
220 |
datatype_new nat = Zero | Suc nat |
|
221 |
||
222 |
text {* |
|
52868 | 223 |
Setup to be able to write @{text 0} instead of @{const Zero}: |
52841 | 224 |
*} |
225 |
||
226 |
instantiation nat :: zero |
|
227 |
begin |
|
228 |
definition "0 = Zero" |
|
229 |
instance .. |
|
230 |
end |
|
231 |
||
232 |
text {* |
|
52805 | 233 |
lists were shown in the introduction |
234 |
||
235 |
terminated lists are a variant: |
|
236 |
*} |
|
237 |
||
238 |
datatype_new ('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist" |
|
239 |
||
240 |
text {* |
|
241 |
On the right-hand side of the equal sign, the usual Isabelle conventions apply: |
|
242 |
Nonatomic types must be enclosed in double quotes. |
|
243 |
*} |
|
244 |
||
52824 | 245 |
|
52794 | 246 |
subsubsection {* Mutual Recursion *} |
247 |
||
52805 | 248 |
text {* |
249 |
Mutual recursion = Define several types simultaneously, referring to each other. |
|
250 |
||
251 |
Simple example: distinction between even and odd natural numbers: |
|
252 |
*} |
|
253 |
||
52841 | 254 |
datatype_new enat = EZero | ESuc onat |
255 |
and onat = OSuc enat |
|
52805 | 256 |
|
257 |
text {* |
|
258 |
More complex, and more realistic, example: |
|
259 |
*} |
|
260 |
||
52841 | 261 |
datatype_new ('a, 'b) exp = |
262 |
Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
|
52805 | 263 |
and ('a, 'b) trm = |
52841 | 264 |
Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm" |
265 |
and ('a, 'b) fct = |
|
266 |
Const 'a | Var 'b | Expr "('a, 'b) exp" |
|
52805 | 267 |
|
52824 | 268 |
|
52794 | 269 |
subsubsection {* Nested Recursion *} |
270 |
||
52805 | 271 |
text {* |
272 |
Nested recursion = Have recursion through a type constructor. |
|
273 |
||
274 |
The introduction showed some examples of trees with nesting through lists. |
|
275 |
||
52843 | 276 |
More complex example, which reuses our maybe: |
52805 | 277 |
*} |
278 |
||
52843 | 279 |
datatype_new 'a btree = |
280 |
BNode 'a "'a btree maybe" "'a btree maybe" |
|
52805 | 281 |
|
282 |
text {* |
|
283 |
Recursion may not be arbitrary; e.g. impossible to define |
|
284 |
*} |
|
285 |
||
52806 | 286 |
datatype_new 'a evil = Evil (*<*)'a |
287 |
typ (*>*)"'a evil \<Rightarrow> 'a evil" |
|
288 |
||
289 |
text {* |
|
290 |
Issue: => allows recursion only on its right-hand side. |
|
291 |
This issue is inherited by polymorphic datatypes (and codatatypes) |
|
292 |
defined in terms of =>. |
|
293 |
In general, type constructors "('a1, ..., 'an) k" allow recursion on a subset |
|
294 |
of their type arguments. |
|
295 |
*} |
|
296 |
||
297 |
||
52805 | 298 |
subsubsection {* Auxiliary Constants and Syntaxes *} |
299 |
||
300 |
text {* |
|
52822 | 301 |
The @{command datatype_new} command introduces various constants in addition to the |
302 |
constructors. Given a type @{text "('a1,\<dots>,'aM) t"} with constructors |
|
52827 | 303 |
@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>m"}, the following auxiliary |
304 |
constants are introduced (among others): |
|
52822 | 305 |
|
306 |
\begin{itemize} |
|
307 |
\setlength{\itemsep}{0pt} |
|
308 |
||
52827 | 309 |
\item \emph{Set functions} (\emph{natural transformations}): |
310 |
@{text t_set1}, \ldots, @{text t_setM} |
|
52822 | 311 |
|
312 |
\item \emph{Map function} (\emph{functorial action}): @{text t_map} |
|
313 |
||
314 |
\item \emph{Relator}: @{text t_rel} |
|
315 |
||
316 |
\item \emph{Iterator}: @{text t_fold} |
|
317 |
||
318 |
\item \emph{Recursor}: @{text t_rec} |
|
319 |
||
52827 | 320 |
\item \emph{Discriminators}: @{text "t.is_C\<^sub>1"}, \ldots, |
321 |
@{text "t.is_C\<^sub>m"} |
|
52822 | 322 |
|
323 |
\item \emph{Selectors}: |
|
52827 | 324 |
@{text t.un_C}$_{11}$, \ldots, @{text t.un_C}$_{1n_1}$, \ldots, |
325 |
@{text t.un_C}$_{m1}$, \ldots, @{text t.un_C}$_{mn_m}$ |
|
52822 | 326 |
\end{itemize} |
327 |
||
52827 | 328 |
The discriminators and selectors are collectively called \emph{destructors}. The |
329 |
@{text "t."} prefix is an optional component of the name and is normally hidden. |
|
52822 | 330 |
|
331 |
The set functions, map function, relator, discriminators, and selectors can be |
|
332 |
given custom names, as in the example below: |
|
52841 | 333 |
|
334 |
%%% FIXME: get rid of 0 below |
|
52822 | 335 |
*} |
336 |
||
52841 | 337 |
(*<*) |
338 |
no_translations |
|
339 |
"[x, xs]" == "x # [xs]" |
|
340 |
"[x]" == "x # []" |
|
341 |
||
342 |
no_notation |
|
343 |
Nil ("[]") and |
|
344 |
Cons (infixr "#" 65) |
|
345 |
||
346 |
hide_const Nil Cons hd tl map |
|
347 |
(*>*) |
|
348 |
datatype_new (set0: 'a) list0 (map: map0 rel: list0_all2) = |
|
52822 | 349 |
null: Nil (defaults tl: Nil) |
52841 | 350 |
| Cons (hd: 'a) (tl: "'a list0") |
52822 | 351 |
|
352 |
text {* |
|
353 |
\noindent |
|
354 |
The command introduces a discriminator @{const null} and a pair of selectors |
|
355 |
@{const hd} and @{const tl} characterized as follows: |
|
356 |
% |
|
52841 | 357 |
\[@{thm list0.collapse(1)[of xs, no_vars]} |
358 |
\qquad @{thm list0.collapse(2)[of xs, no_vars]}\] |
|
52822 | 359 |
% |
360 |
For two-constructor datatypes, a single discriminator constant suffices. The |
|
361 |
discriminator associated with @{const Cons} is simply @{text "\<not> null"}. |
|
362 |
||
52824 | 363 |
The \keyw{defaults} keyword following the @{const Nil} constructor specifies a |
52822 | 364 |
default value for selectors associated with other constructors. Here, it is |
365 |
used to specify that the tail of the empty list is the empty list (instead of |
|
366 |
being unspecified). |
|
367 |
||
368 |
Because @{const Nil} is a nullary constructor, it is also possible to use @{text |
|
369 |
"= Nil"} as a discriminator. This is specified by specifying @{text "="} instead |
|
370 |
of the identifier @{const null} in the declaration above. Although this may look |
|
371 |
appealing, the mixture of constructors and selectors in the resulting |
|
372 |
characteristic theorems can lead Isabelle's automation to switch between the |
|
373 |
constructor and the destructor view in surprising ways. |
|
374 |
*} |
|
375 |
||
376 |
text {* |
|
377 |
The usual mixfix syntaxes are available for both types and constructors. For example: |
|
378 |
||
379 |
%%% FIXME: remove trailing underscore and use locale trick instead once this is |
|
380 |
%%% supported. |
|
52805 | 381 |
*} |
52794 | 382 |
|
52822 | 383 |
datatype_new ('a, 'b) prod (infixr "*" 20) = |
384 |
Pair 'a 'b |
|
385 |
||
52841 | 386 |
(*<*) |
387 |
hide_const Nil Cons hd tl |
|
388 |
(*>*) |
|
389 |
datatype_new (set: 'a) list (map: map rel: list_all2) = |
|
52822 | 390 |
null: Nil ("[]") |
52841 | 391 |
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) |
392 |
||
393 |
text {* |
|
394 |
Incidentally, this is how the traditional syntaxes are set up in @{theory List}: |
|
395 |
*} |
|
396 |
||
397 |
syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]") |
|
398 |
||
399 |
translations |
|
400 |
"[x, xs]" == "x # [xs]" |
|
401 |
"[x]" == "x # []" |
|
52822 | 402 |
|
52824 | 403 |
|
52840 | 404 |
subsection {* Syntax |
405 |
\label{ssec:datatype-syntax} *} |
|
52794 | 406 |
|
52822 | 407 |
text {* |
408 |
Datatype definitions have the following general syntax: |
|
409 |
||
52824 | 410 |
@{rail " |
52828 | 411 |
@@{command datatype_new} @{syntax target}? @{syntax dt_options}? \\ |
52824 | 412 |
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and') |
52828 | 413 |
; |
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52868
diff
changeset
|
414 |
@{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')' |
52824 | 415 |
"} |
416 |
||
52828 | 417 |
The syntactic quantity @{syntax target} can be used to specify a local context |
418 |
(e.g., @{text "(in linorder)"}). It is documented in the Isar reference manual |
|
419 |
\cite{isabelle-isar-ref}. |
|
420 |
||
421 |
The optional target is followed by optional options: |
|
52822 | 422 |
|
52824 | 423 |
\begin{itemize} |
424 |
\setlength{\itemsep}{0pt} |
|
425 |
||
426 |
\item |
|
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52868
diff
changeset
|
427 |
The \keyw{no\_discs\_sels} option indicates that no destructors (i.e., |
52824 | 428 |
discriminators and selectors) should be generated. |
52822 | 429 |
|
52824 | 430 |
\item |
431 |
The \keyw{rep\_compat} option indicates that the names generated by the |
|
432 |
package should contain optional (and normally not displayed) @{text "new."} |
|
433 |
components to prevent clashes with a later call to @{command rep_datatype}. See |
|
434 |
Section~\ref{ssec:datatype-compatibility-issues} for details. |
|
435 |
\end{itemize} |
|
52822 | 436 |
|
52827 | 437 |
The left-hand sides of the datatype equations specify the name of the type to |
438 |
define, its type parameters, and optional additional information: |
|
52822 | 439 |
|
52824 | 440 |
@{rail " |
52827 | 441 |
@{syntax_def dt_name}: @{syntax tyargs}? @{syntax name} |
52824 | 442 |
@{syntax map_rel}? @{syntax mixfix}? |
443 |
; |
|
52827 | 444 |
@{syntax_def tyargs}: @{syntax typefree} | '(' ((@{syntax name} ':')? @{syntax typefree} + ',') ')' |
52824 | 445 |
; |
446 |
@{syntax_def map_rel}: '(' ((('map' | 'rel') ':' @{syntax name}) +) ')' |
|
447 |
"} |
|
52822 | 448 |
|
52827 | 449 |
\noindent |
450 |
The syntactic quantity @{syntax name} denotes an identifier, @{syntax typefree} |
|
451 |
denotes fixed type variable (@{typ 'a}, @{typ 'b}, \ldots), and @{syntax |
|
452 |
mixfix} denotes the usual parenthesized mixfix notation. They are documented in |
|
453 |
the Isar reference manual \cite{isabelle-isar-ref}. |
|
52822 | 454 |
|
52827 | 455 |
The optional names preceding the type variables allow to override the default |
456 |
names of the set functions (@{text t_set1}, \ldots, @{text t_setM}). |
|
457 |
Inside a mutually recursive datatype specification, all defined datatypes must |
|
458 |
specify exactly the same type variables in the same order. |
|
52822 | 459 |
|
52824 | 460 |
@{rail " |
52840 | 461 |
@{syntax_def ctor}: (@{syntax name} ':')? @{syntax name} (@{syntax ctor_arg} * ) \\ |
52824 | 462 |
@{syntax sel_defaults}? @{syntax mixfix}? |
463 |
"} |
|
464 |
||
52827 | 465 |
\noindent |
466 |
The main constituents of a constructor specification is the name of the |
|
467 |
constructor and the list of its argument types. An optional discriminator name |
|
468 |
can be supplied at the front to override the default name |
|
469 |
(@{text t.un_C}$_{ij}$). |
|
52822 | 470 |
|
52824 | 471 |
@{rail " |
52828 | 472 |
@{syntax_def ctor_arg}: @{syntax type} | '(' @{syntax name} ':' @{syntax type} ')' |
52827 | 473 |
"} |
474 |
||
475 |
\noindent |
|
476 |
In addition to the type of a constructor argument, it is possible to specify a |
|
477 |
name for the corresponding selector to override the default name |
|
478 |
(@{text t.un_C}$_{ij}$). The same selector names can be reused for several |
|
479 |
constructors as long as they have the same type. |
|
480 |
||
481 |
@{rail " |
|
52828 | 482 |
@{syntax_def sel_defaults}: '(' @'defaults' (@{syntax name} ':' @{syntax term} +) ')' |
52824 | 483 |
"} |
52827 | 484 |
|
485 |
\noindent |
|
486 |
Given a constructor |
|
487 |
@{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"}, |
|
488 |
default values can be specified for any selector |
|
489 |
@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"} |
|
490 |
associated with other constructors. The specified default value must have type |
|
52828 | 491 |
@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"} |
52827 | 492 |
(i.e., it may dependend on @{text C}'s arguments). |
52822 | 493 |
*} |
494 |
||
52840 | 495 |
subsection {* Generated Theorems |
496 |
\label{ssec:datatype-generated-theorems} *} |
|
52828 | 497 |
|
498 |
text {* |
|
499 |
* free ctor theorems |
|
500 |
* case syntax |
|
501 |
||
502 |
* per-type theorems |
|
503 |
* sets, map, rel |
|
504 |
* induct, fold, rec |
|
505 |
* simps |
|
506 |
||
507 |
* multi-type (``common'') theorems |
|
508 |
* induct |
|
509 |
||
510 |
* mention what is registered with which attribute |
|
511 |
* and also nameless safes |
|
512 |
*} |
|
513 |
||
52794 | 514 |
|
52827 | 515 |
subsection {* Compatibility Issues |
52824 | 516 |
\label{ssec:datatype-compatibility-issues} *} |
52794 | 517 |
|
52828 | 518 |
text {* |
519 |
* main incompabilities between two packages |
|
520 |
* differences in theorem names (e.g. singular vs. plural for some props?) |
|
521 |
* differences in "simps"? |
|
522 |
* different recursor/induction in nested case |
|
523 |
* discussed in Section~\ref{sec:defining-recursive-functions} |
|
524 |
* different ML interfaces / extension mechanisms |
|
525 |
||
526 |
* register new datatype as old datatype |
|
527 |
* motivation: |
|
528 |
* do recursion through new datatype in old datatype |
|
529 |
(e.g. useful when porting to the new package one type at a time) |
|
530 |
* use old primrec |
|
531 |
* use fun |
|
532 |
* use extensions like size (needed for fun), the AFP order, Quickcheck, |
|
533 |
Nitpick |
|
534 |
* provide exactly the same theorems with the same names (compatibility) |
|
535 |
* option 1 |
|
536 |
* \keyw{rep\_compat} |
|
537 |
* \keyw{rep\_datatype} |
|
538 |
* has some limitations |
|
539 |
* mutually recursive datatypes? (fails with rep\_datatype?) |
|
540 |
* nested datatypes? (fails with datatype\_new?) |
|
541 |
* option 2 |
|
542 |
* \keyw{datatype\_compat} |
|
543 |
* not fully implemented yet? |
|
544 |
||
545 |
* register old datatype as new datatype |
|
546 |
* no clean way yet |
|
547 |
* if the goal is to do recursion through old datatypes, can register it as |
|
548 |
a BNF (Section XXX) |
|
549 |
* can also derive destructors etc. using @{command wrap_free_constructors} |
|
550 |
(Section XXX) |
|
551 |
*} |
|
552 |
||
52792 | 553 |
|
52827 | 554 |
section {* Defining Recursive Functions |
52805 | 555 |
\label{sec:defining-recursive-functions} *} |
556 |
||
557 |
text {* |
|
558 |
This describes how to specify recursive functions over datatypes |
|
52824 | 559 |
specified using @{command datatype_new}. The focus in on the \keyw{primrec\_new} |
52805 | 560 |
command, which supports primitive recursion. A few examples feature the |
52822 | 561 |
@{command fun} and @{command function} commands, described in a separate |
562 |
tutorial \cite{isabelle-function}. |
|
52828 | 563 |
|
52805 | 564 |
%%% TODO: partial_function? |
565 |
*} |
|
52792 | 566 |
|
52805 | 567 |
text {* |
568 |
More examples in \verb|~~/src/HOL/BNF/Examples|. |
|
569 |
*} |
|
570 |
||
52840 | 571 |
subsection {* Examples |
572 |
\label{ssec:primrec-examples} *} |
|
52828 | 573 |
|
574 |
subsubsection {* Nonrecursive Types *} |
|
575 |
||
52841 | 576 |
text {* |
577 |
* simple (depth 1) pattern matching on the left-hand side |
|
578 |
*} |
|
579 |
||
580 |
primrec_new bool_of_trool :: "trool \<Rightarrow> bool" where |
|
581 |
"real_of_trool Faalse = False" | |
|
582 |
"real_of_trool Truue = True" |
|
583 |
||
584 |
text {* |
|
585 |
* OK to specify the cases in a different order |
|
586 |
* OK to leave out some case (but get a warning -- maybe we need a "quiet" |
|
587 |
or "silent" flag?) |
|
588 |
* case is then unspecified |
|
589 |
||
590 |
More examples: |
|
591 |
*} |
|
592 |
||
52843 | 593 |
primrec_new list_of_maybe :: "'a maybe \<Rightarrow> 'a list" where |
52841 | 594 |
"list_of_maybe Nothing = []" | |
595 |
"list_of_maybe (Just a) = [a]" |
|
596 |
||
52843 | 597 |
primrec_new maybe_def :: "'a \<Rightarrow> 'a maybe \<Rightarrow> 'a" where |
598 |
"maybe_def d Nothing = d" | |
|
599 |
"maybe_def _ (Just a) = a" |
|
600 |
||
52841 | 601 |
primrec_new mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where |
602 |
"mirrror (Triple a b c) = Triple c b a" |
|
603 |
||
52828 | 604 |
|
605 |
subsubsection {* Simple Recursion *} |
|
606 |
||
52841 | 607 |
text {* |
608 |
again, simple pattern matching on left-hand side, but possibility |
|
609 |
to call a function recursively on an argument to a constructor: |
|
610 |
*} |
|
611 |
||
612 |
primrec_new replicate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
613 |
"rep 0 _ = []" | |
|
614 |
"rep (Suc n) a = a # rep n a" |
|
615 |
||
52843 | 616 |
text {* |
617 |
we don't like the confusing name @{const nth}: |
|
618 |
*} |
|
619 |
||
620 |
primrec_new at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where |
|
621 |
"at (a # as) j = |
|
622 |
(case j of |
|
623 |
0 \<Rightarrow> a |
|
624 |
| Suc j' \<Rightarrow> at as j')" |
|
625 |
||
52841 | 626 |
primrec_new tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where |
627 |
"tfold _ (TNil b) = b" | |
|
628 |
"tfold f (TCons a as) = f a (tfold f as)" |
|
629 |
||
52828 | 630 |
|
631 |
subsubsection {* Mutual Recursion *} |
|
632 |
||
52841 | 633 |
text {* |
634 |
E.g., converting even/odd naturals to plain old naturals: |
|
635 |
*} |
|
636 |
||
637 |
primrec_new |
|
638 |
nat_of_enat :: "enat \<Rightarrow> nat" and |
|
639 |
nat_of_onat :: "onat => nat" |
|
640 |
where |
|
641 |
"nat_of_enat EZero = 0" | |
|
642 |
"nat_of_enat (ESuc n) = Suc (nat_of_onat n)" | |
|
643 |
"nat_of_onat (OSuc n) = Suc (nat_of_enat n)" |
|
644 |
||
645 |
text {* |
|
646 |
Mutual recursion is even possible within a single type, an innovation over the |
|
647 |
old package: |
|
648 |
*} |
|
649 |
||
650 |
primrec_new |
|
651 |
even :: "nat \<Rightarrow> bool" and |
|
652 |
odd :: "nat \<Rightarrow> bool" |
|
653 |
where |
|
654 |
"even 0 = True" | |
|
655 |
"even (Suc n) = odd n" | |
|
656 |
"odd 0 = False" | |
|
657 |
"odd (Suc n) = even n" |
|
658 |
||
659 |
text {* |
|
660 |
More elaborate: |
|
661 |
*} |
|
662 |
||
663 |
primrec_new |
|
664 |
eval\<^sub>e :: "('a, 'b) exp \<Rightarrow> real" and |
|
665 |
eval\<^sub>t :: "('a, 'b) trm \<Rightarrow> real" and |
|
666 |
eval\<^sub>f :: "('a, 'b) fct \<Rightarrow> real" |
|
667 |
where |
|
668 |
"eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" | |
|
669 |
"eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" | |
|
670 |
"eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f)" | |
|
671 |
"eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" | |
|
672 |
"eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" | |
|
673 |
"eval\<^sub>f _ \<xi> (Var b) = \<xi> b" | |
|
674 |
"eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e" |
|
675 |
||
52828 | 676 |
|
677 |
subsubsection {* Nested Recursion *} |
|
678 |
||
52843 | 679 |
(*<*) |
680 |
datatype_new 'a treeFF = NodeFF 'a "'a treeFF list" |
|
681 |
datatype_new 'a treeFI = NodeFI 'a "'a treeFI llist" |
|
682 |
(*>*) |
|
683 |
primrec_new atFF0 :: "'a treeFF \<Rightarrow> nat list \<Rightarrow> 'a" where |
|
684 |
"atFF0 (NodeFF a ts) js = |
|
685 |
(case js of |
|
686 |
[] \<Rightarrow> a |
|
687 |
| j # js' \<Rightarrow> at (map (\<lambda>t. atFF0 t js') ts) j)" |
|
688 |
||
689 |
primrec_new atFI :: "'a treeFI \<Rightarrow> nat list \<Rightarrow> 'a" where |
|
690 |
"atFF (NodeFI a ts) js = |
|
691 |
(case js of |
|
692 |
[] \<Rightarrow> a |
|
693 |
| j # js' \<Rightarrow> at (llist_map (\<lambda>t. atFF t js') ts) j)" |
|
694 |
||
695 |
primrec_new sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" where |
|
696 |
"sum_btree (BNode a lt rt) = |
|
697 |
a + maybe_def 0 (maybe_map sum_btree lt) + |
|
698 |
maybe_def 0 (maybe_map sum_btree rt)" |
|
699 |
||
52828 | 700 |
|
701 |
subsubsection {* Nested-as-Mutual Recursion *} |
|
702 |
||
52843 | 703 |
text {* |
704 |
* can pretend a nested type is mutually recursive |
|
705 |
* avoids the higher-order map |
|
706 |
* e.g. |
|
707 |
*} |
|
708 |
||
709 |
primrec_new |
|
710 |
at_treeFF :: "'a treeFF \<Rightarrow> nat list \<Rightarrow> 'a" and |
|
711 |
at_treesFF :: "'a treeFF list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a" |
|
712 |
where |
|
713 |
"at_treeFF (NodeFF a ts) js = |
|
714 |
(case js of |
|
715 |
[] \<Rightarrow> a |
|
716 |
| j # js' \<Rightarrow> at_treesFF ts j js')" | |
|
717 |
"at_treesFF (t # ts) j = |
|
718 |
(case j of |
|
719 |
0 \<Rightarrow> at_treeFF t |
|
720 |
| Suc j' \<Rightarrow> at_treesFF ts j')" |
|
721 |
||
722 |
primrec_new |
|
723 |
sum_btree :: "('a\<Colon>plus) btree \<Rightarrow> 'a" and |
|
724 |
sum_btree_maybe :: "('a\<Colon>plus) btree maybe \<Rightarrow> 'a" |
|
725 |
where |
|
726 |
"sum_btree (BNode a lt rt) = |
|
727 |
a + sum_btree_maybe lt + sum_btree_maybe rt" | |
|
728 |
"sum_btree_maybe Nothing = 0" | |
|
729 |
"sum_btree_maybe (Just t) = sum_btree t" |
|
730 |
||
731 |
text {* |
|
732 |
* this can always be avoided; |
|
733 |
* e.g. in our previous example, we first mapped the recursive |
|
734 |
calls, then we used a generic at function to retrieve the result |
|
735 |
||
736 |
* there's no hard-and-fast rule of when to use one or the other, |
|
737 |
just like there's no rule when to use fold and when to use |
|
738 |
primrec_new |
|
739 |
||
740 |
* higher-order approach, considering nesting as nesting, is more |
|
741 |
compositional -- e.g. we saw how we could reuse an existing polymorphic |
|
742 |
at or maybe_def, whereas at_treesFF is much more specific |
|
743 |
||
744 |
* but: |
|
745 |
* is perhaps less intuitive, because it requires higher-order thinking |
|
746 |
* may seem inefficient, and indeed with the code generator the |
|
747 |
mutually recursive version might be nicer |
|
748 |
* is somewhat indirect -- must apply a map first, then compute a result |
|
749 |
(cannot mix) |
|
750 |
* the auxiliary functions like at_treesFF are sometimes useful in own right |
|
751 |
||
752 |
* impact on automation unclear |
|
753 |
*} |
|
754 |
||
52824 | 755 |
|
52840 | 756 |
subsection {* Syntax |
757 |
\label{ssec:primrec-syntax} *} |
|
52828 | 758 |
|
759 |
text {* |
|
52840 | 760 |
Primitive recursive functions have the following general syntax: |
52794 | 761 |
|
52840 | 762 |
@{rail " |
763 |
@@{command primrec_new} @{syntax target}? @{syntax \"fixes\"} \\ @'where' |
|
764 |
(@{syntax primrec_equation} + '|') |
|
765 |
; |
|
766 |
@{syntax_def primrec_equation}: @{syntax thmdecl}? @{syntax prop} |
|
767 |
"} |
|
52828 | 768 |
*} |
769 |
||
52840 | 770 |
|
771 |
subsection {* Generated Theorems |
|
772 |
\label{ssec:primrec-generated-theorems} *} |
|
52824 | 773 |
|
52828 | 774 |
text {* |
775 |
* synthesized nonrecursive definition |
|
776 |
* user specification is rederived from it, exactly as entered |
|
52794 | 777 |
|
52828 | 778 |
* induct |
779 |
* mutualized |
|
780 |
* without some needless induction hypotheses if not used |
|
781 |
* fold, rec |
|
782 |
* mutualized |
|
783 |
*} |
|
52824 | 784 |
|
52840 | 785 |
subsection {* Recursive Default Values for Selectors |
786 |
\label{ssec:recursive-default-values-for-selectors} *} |
|
52827 | 787 |
|
788 |
text {* |
|
789 |
A datatype selector @{text un_D} can have a default value for each constructor |
|
790 |
on which it is not otherwise specified. Occasionally, it is useful to have the |
|
791 |
default value be defined recursively. This produces a chicken-and-egg situation |
|
792 |
that appears unsolvable, because the datatype is not introduced yet at the |
|
793 |
moment when the selectors are introduced. Of course, we can always define the |
|
794 |
selectors manually afterward, but we then have to state and prove all the |
|
795 |
characteristic theorems ourselves instead of letting the package do it. |
|
796 |
||
797 |
Fortunately, there is a fairly elegant workaround that relies on overloading and |
|
798 |
that avoids the tedium of manual derivations: |
|
799 |
||
800 |
\begin{enumerate} |
|
801 |
\setlength{\itemsep}{0pt} |
|
802 |
||
803 |
\item |
|
804 |
Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using |
|
805 |
@{keyword consts}. |
|
806 |
||
807 |
\item |
|
808 |
Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default value. |
|
809 |
||
810 |
\item |
|
811 |
Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced datatype |
|
812 |
using the @{command overloading} command. |
|
813 |
||
814 |
\item |
|
815 |
Derive the desired equation on @{text un_D} from the characteristic equations |
|
816 |
for @{text "un_D\<^sub>0"}. |
|
817 |
\end{enumerate} |
|
818 |
||
819 |
The following example illustrates this procedure: |
|
820 |
*} |
|
821 |
||
822 |
consts termi\<^sub>0 :: 'a |
|
823 |
||
824 |
datatype_new (*<*)(rep_compat) (*>*)('a, 'b) tlist_ = |
|
825 |
TNil (termi: 'b) (defaults ttl: TNil) |
|
826 |
| TCons (thd: 'a) (ttl : "('a, 'b) tlist_") (defaults termi: "\<lambda>_ xs. termi\<^sub>0 xs") |
|
827 |
||
828 |
(*<*) |
|
52843 | 829 |
(* FIXME: remove hack once "primrec_new" is in place *) |
52827 | 830 |
rep_datatype TNil TCons |
831 |
by (erule tlist_.induct, assumption) auto |
|
832 |
(*>*) |
|
833 |
overloading |
|
834 |
termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist_ \<Rightarrow> 'b" |
|
835 |
begin |
|
52843 | 836 |
(*<*) |
837 |
(* FIXME: remove hack once "primrec_new" is in place *) |
|
52827 | 838 |
fun termi\<^sub>0 :: "('a, 'b) tlist_ \<Rightarrow> 'b" where |
839 |
"termi\<^sub>0 (TNil y) = y" | |
|
840 |
"termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs" |
|
52843 | 841 |
(*>*) |
842 |
primrec_new termi\<^sub>0 :: "('a, 'b) tlist_ \<Rightarrow> 'b" where |
|
843 |
"termi\<^sub>0 (TNil y) = y" | |
|
844 |
"termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs" |
|
52827 | 845 |
end |
846 |
||
847 |
lemma terminal_TCons[simp]: "termi (TCons x xs) = termi xs" |
|
848 |
by (cases xs) auto |
|
849 |
||
850 |
||
52828 | 851 |
subsection {* Compatibility Issues |
852 |
\label{ssec:datatype-compatibility-issues} *} |
|
853 |
||
854 |
text {* |
|
855 |
* different induction in nested case |
|
856 |
* solution: define nested-as-mutual functions with primrec, |
|
857 |
and look at .induct |
|
858 |
||
859 |
* different induction and recursor in nested case |
|
860 |
* only matters to low-level users; they can define a dummy function to force |
|
861 |
generation of mutualized recursor |
|
862 |
*} |
|
52794 | 863 |
|
864 |
||
52827 | 865 |
section {* Defining Codatatypes |
52805 | 866 |
\label{sec:defining-codatatypes} *} |
867 |
||
868 |
text {* |
|
52822 | 869 |
This section describes how to specify codatatypes using the @{command codatatype} |
52805 | 870 |
command. |
52843 | 871 |
|
872 |
* libraries include some useful codatatypes, notably lazy lists; |
|
873 |
see the ``Coinductive'' AFP entry \cite{xxx} for an elaborate library |
|
52805 | 874 |
*} |
52792 | 875 |
|
52824 | 876 |
|
52840 | 877 |
subsection {* Examples |
878 |
\label{ssec:codatatype-examples} *} |
|
52794 | 879 |
|
52805 | 880 |
text {* |
881 |
More examples in \verb|~~/src/HOL/BNF/Examples|. |
|
882 |
*} |
|
883 |
||
52824 | 884 |
|
52840 | 885 |
subsection {* Syntax |
886 |
\label{ssec:codatatype-syntax} *} |
|
52805 | 887 |
|
52824 | 888 |
text {* |
52827 | 889 |
Definitions of codatatypes have almost exactly the same syntax as for datatypes |
52840 | 890 |
(Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called |
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52868
diff
changeset
|
891 |
@{command codatatype}; the \keyw{no\_discs\_sels} option is not available, because |
52840 | 892 |
destructors are a central notion for codatatypes. |
52824 | 893 |
*} |
894 |
||
52840 | 895 |
subsection {* Generated Theorems |
896 |
\label{ssec:codatatype-generated-theorems} *} |
|
52805 | 897 |
|
898 |
||
52827 | 899 |
section {* Defining Corecursive Functions |
52805 | 900 |
\label{sec:defining-corecursive-functions} *} |
901 |
||
902 |
text {* |
|
903 |
This section describes how to specify corecursive functions using the |
|
52824 | 904 |
\keyw{primcorec} command. |
52828 | 905 |
|
906 |
%%% TODO: partial_function? E.g. for defining tail recursive function on lazy |
|
907 |
%%% lists (cf. terminal0 in TLList.thy) |
|
52805 | 908 |
*} |
909 |
||
52824 | 910 |
|
52840 | 911 |
subsection {* Examples |
912 |
\label{ssec:primcorec-examples} *} |
|
52805 | 913 |
|
914 |
text {* |
|
915 |
More examples in \verb|~~/src/HOL/BNF/Examples|. |
|
52827 | 916 |
|
917 |
Also, for default values, the same trick as for datatypes is possible for |
|
52840 | 918 |
codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}). |
52805 | 919 |
*} |
920 |
||
52824 | 921 |
|
52840 | 922 |
subsection {* Syntax |
923 |
\label{ssec:primcorec-syntax} *} |
|
924 |
||
925 |
text {* |
|
926 |
Primitive corecrusvie definitions have the following general syntax: |
|
927 |
||
928 |
@{rail " |
|
929 |
@@{command primcorec} @{syntax target}? @{syntax \"fixes\"} \\ @'where' |
|
930 |
(@{syntax primcorec_formula} + '|') |
|
931 |
; |
|
932 |
@{syntax_def primcorec_formula}: @{syntax thmdecl}? @{syntax prop} |
|
933 |
(@'of' (@{syntax term} * ))? |
|
934 |
"} |
|
935 |
*} |
|
52794 | 936 |
|
52824 | 937 |
|
52840 | 938 |
subsection {* Generated Theorems |
939 |
\label{ssec:primcorec-generated-theorems} *} |
|
52794 | 940 |
|
941 |
||
52827 | 942 |
section {* Registering Bounded Natural Functors |
52805 | 943 |
\label{sec:registering-bounded-natural-functors} *} |
52792 | 944 |
|
52805 | 945 |
text {* |
946 |
This section explains how to set up the (co)datatype package to allow nested |
|
947 |
recursion through custom well-behaved type constructors. The key concept is that |
|
948 |
of a bounded natural functor (BNF). |
|
52829 | 949 |
|
950 |
* @{command bnf} |
|
951 |
* @{command print_bnfs} |
|
52805 | 952 |
*} |
953 |
||
52824 | 954 |
|
52840 | 955 |
subsection {* Example |
956 |
\label{ssec:bnf-examples} *} |
|
52805 | 957 |
|
958 |
text {* |
|
959 |
More examples in \verb|~~/src/HOL/BNF/Basic_BNFs.thy| and |
|
960 |
\verb|~~/src/HOL/BNF/More_BNFs.thy|. |
|
52806 | 961 |
|
962 |
Mention distinction between live and dead type arguments; |
|
963 |
mention =>. |
|
52805 | 964 |
*} |
52794 | 965 |
|
52824 | 966 |
|
52840 | 967 |
subsection {* Syntax |
968 |
\label{ssec:bnf-syntax} *} |
|
52794 | 969 |
|
52805 | 970 |
|
52827 | 971 |
section {* Generating Free Constructor Theorems |
52805 | 972 |
\label{sec:generating-free-constructor-theorems} *} |
52794 | 973 |
|
52805 | 974 |
text {* |
975 |
This section explains how to derive convenience theorems for free constructors, |
|
52822 | 976 |
as performed internally by @{command datatype_new} and @{command codatatype}. |
52794 | 977 |
|
52805 | 978 |
* need for this is rare but may arise if you want e.g. to add destructors to |
979 |
a type not introduced by ... |
|
52794 | 980 |
|
52805 | 981 |
* also useful for compatibility with old package, e.g. add destructors to |
52822 | 982 |
old @{command datatype} |
52829 | 983 |
|
984 |
* @{command wrap_free_constructors} |
|
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52868
diff
changeset
|
985 |
* \keyw{no\_discs\_sels}, \keyw{rep\_compat} |
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
52868
diff
changeset
|
986 |
* hack to have both co and nonco view via locale (cf. ext nats) |
52805 | 987 |
*} |
52792 | 988 |
|
52824 | 989 |
|
52840 | 990 |
subsection {* Example |
991 |
\label{ssec:ctors-examples} *} |
|
52794 | 992 |
|
52824 | 993 |
|
52840 | 994 |
subsection {* Syntax |
995 |
\label{ssec:ctors-syntax} *} |
|
52828 | 996 |
|
997 |
||
52840 | 998 |
subsection {* Generated Theorems |
999 |
\label{ssec:ctors-generated-theorems} *} |
|
52794 | 1000 |
|
1001 |
||
52827 | 1002 |
section {* Standard ML Interface |
52805 | 1003 |
\label{sec:standard-ml-interface} *} |
52792 | 1004 |
|
52805 | 1005 |
text {* |
1006 |
This section describes the package's programmatic interface. |
|
1007 |
*} |
|
52794 | 1008 |
|
1009 |
||
52827 | 1010 |
section {* Interoperability |
52805 | 1011 |
\label{sec:interoperability} *} |
52794 | 1012 |
|
52805 | 1013 |
text {* |
1014 |
This section is concerned with the packages' interaction with other Isabelle |
|
1015 |
packages and tools, such as the code generator and the counterexample |
|
1016 |
generators. |
|
1017 |
*} |
|
52794 | 1018 |
|
52824 | 1019 |
|
52828 | 1020 |
subsection {* Transfer and Lifting |
1021 |
\label{ssec:transfer-and-lifting} *} |
|
52794 | 1022 |
|
52824 | 1023 |
|
52828 | 1024 |
subsection {* Code Generator |
1025 |
\label{ssec:code-generator} *} |
|
52794 | 1026 |
|
52824 | 1027 |
|
52828 | 1028 |
subsection {* Quickcheck |
1029 |
\label{ssec:quickcheck} *} |
|
52794 | 1030 |
|
52824 | 1031 |
|
52828 | 1032 |
subsection {* Nitpick |
1033 |
\label{ssec:nitpick} *} |
|
52794 | 1034 |
|
52824 | 1035 |
|
52828 | 1036 |
subsection {* Nominal Isabelle |
1037 |
\label{ssec:nominal-isabelle} *} |
|
52794 | 1038 |
|
52805 | 1039 |
|
52827 | 1040 |
section {* Known Bugs and Limitations |
52805 | 1041 |
\label{sec:known-bugs-and-limitations} *} |
1042 |
||
1043 |
text {* |
|
1044 |
This section lists known open issues of the package. |
|
1045 |
*} |
|
52794 | 1046 |
|
1047 |
text {* |
|
52806 | 1048 |
* primrec\_new and primcorec are vaporware |
1049 |
||
52794 | 1050 |
* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting) |
52806 | 1051 |
|
1052 |
* issues with HOL-Proofs? |
|
1053 |
||
1054 |
* partial documentation |
|
1055 |
||
1056 |
* too much output by commands like "datatype_new" and "codatatype" |
|
52822 | 1057 |
|
1058 |
* no direct way to define recursive functions for default values -- but show trick |
|
1059 |
based on overloading |
|
1060 |
*} |
|
1061 |
||
1062 |
||
52827 | 1063 |
section {* Acknowledgments |
52822 | 1064 |
\label{sec:acknowledgments} *} |
1065 |
||
1066 |
text {* |
|
52829 | 1067 |
Tobias Nipkow and Makarius Wenzel made this work possible. Andreas Lochbihler |
1068 |
provided lots of comments on earlier versions of the package, especially for the |
|
1069 |
coinductive part. Brian Huffman suggested major simplifications to the internal |
|
1070 |
constructions, much of which has yet to be implemented. Florian Haftmann and |
|
1071 |
Christian Urban provided general advice advice on Isabelle and package writing. |
|
1072 |
Stefan Milius and Lutz Schr\"oder suggested an elegant prove to eliminate one of |
|
1073 |
the BNF assumptions. |
|
52794 | 1074 |
*} |
52792 | 1075 |
|
1076 |
end |