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