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