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