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