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