src/Doc/Datatypes/Datatypes.thy
author blanchet
Mon Aug 18 17:20:13 2014 +0200 (2014-08-18)
changeset 57984 cbe9a16f8e11
parent 57983 6edc3529bb4e
child 57988 030ff4ceb6c3
permissions -rw-r--r--
added collection theorem for consistency and convenience
     1 (*  Title:      Doc/Datatypes/Datatypes.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Author:     Martin Desharnais, Ecole de technologie superieure
     4     Author:     Lorenz Panny, TU Muenchen
     5     Author:     Andrei Popescu, TU Muenchen
     6     Author:     Dmitriy Traytel, TU Muenchen
     7 
     8 Tutorial for (co)datatype definitions with the new package.
     9 *)
    10 
    11 theory Datatypes
    12 imports
    13   Setup
    14   "~~/src/HOL/Library/BNF_Axiomatization"
    15   "~~/src/HOL/Library/Cardinal_Notations"
    16   "~~/src/HOL/Library/FSet"
    17   "~~/src/HOL/Library/Simps_Case_Conv"
    18 begin
    19 
    20 section {* Introduction
    21   \label{sec:introduction} *}
    22 
    23 text {*
    24 The 2013 edition of Isabelle introduced a new definitional package for freely
    25 generated datatypes and codatatypes. The datatype support is similar to that
    26 provided by the earlier package due to Berghofer and Wenzel
    27 \cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
    28 \cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
    29 @{command datatype_new} is usually all that is needed to port existing theories
    30 to use the new package.
    31 
    32 Perhaps the main advantage of the new package is that it supports recursion
    33 through a large class of non-datatypes, such as finite sets:
    34 *}
    35 
    36     datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
    37 
    38 text {*
    39 \noindent
    40 Another strong point is the support for local definitions:
    41 *}
    42 
    43     context linorder
    44     begin
    45     datatype_new flag = Less | Eq | Greater
    46     end
    47 
    48 text {*
    49 \noindent
    50 Furthermore, the package provides a lot of convenience, including automatically
    51 generated discriminators, selectors, and relators as well as a wealth of
    52 properties about them.
    53 
    54 In addition to inductive datatypes, the new package supports coinductive
    55 datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
    56 following command introduces the type of lazy lists, which comprises both finite
    57 and infinite values:
    58 *}
    59 
    60 (*<*)
    61     locale early
    62     locale late
    63 (*>*)
    64     codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
    65 
    66 text {*
    67 \noindent
    68 Mixed inductive--coinductive recursion is possible via nesting. Compare the
    69 following four Rose tree examples:
    70 *}
    71 
    72     datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
    73     datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
    74     codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
    75     codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
    76 
    77 text {*
    78 The first two tree types allow only paths of finite length, whereas the last two
    79 allow infinite paths. Orthogonally, the nodes in the first and third types have
    80 finitely many direct subtrees, whereas those of the second and fourth may have
    81 infinite branching.
    82 
    83 The package is part of @{theory Main}. Additional functionality is provided by
    84 the theory @{theory BNF_Axiomatization}, located in the directory
    85 \verb|~~/src/HOL/Library|.
    86 
    87 The package, like its predecessor, fully adheres to the LCF philosophy
    88 \cite{mgordon79}: The characteristic theorems associated with the specified
    89 (co)datatypes are derived rather than introduced axiomatically.%
    90 \footnote{However, some of the
    91 internal constructions and most of the internal proof obligations are skipped
    92 if the @{text quick_and_dirty} option is enabled.}
    93 The package is described in a number of papers
    94 \cite{traytel-et-al-2012,blanchette-et-al-wit,blanchette-et-al-2014-impl,panny-et-al-2014}.
    95 The central notion is that of a \emph{bounded natural functor} (BNF)---a
    96 well-behaved type constructor for which nested (co)recursion is supported.
    97 
    98 This tutorial is organized as follows:
    99 
   100 \begin{itemize}
   101 \setlength{\itemsep}{0pt}
   102 
   103 \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
   104 describes how to specify datatypes using the @{command datatype_new} command.
   105 
   106 \item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
   107 Functions,'' describes how to specify recursive functions using
   108 @{command primrec}.
   109 
   110 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
   111 describes how to specify codatatypes using the @{command codatatype} command.
   112 
   113 \item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
   114 Functions,'' describes how to specify corecursive functions using the
   115 @{command primcorec} and @{command primcorecursive} commands.
   116 
   117 \item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
   118 Bounded Natural Functors,'' explains how to use the @{command bnf} command
   119 to register arbitrary type constructors as BNFs.
   120 
   121 \item Section
   122 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},
   123 ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
   124 use the command @{command free_constructors} to derive destructor constants
   125 and theorems for freely generated types, as performed internally by @{command
   126 datatype_new} and @{command codatatype}.
   127 
   128 %\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
   129 %describes the package's programmatic interface.
   130 
   131 %\item Section \ref{sec:interoperability}, ``Interoperability,''
   132 %is concerned with the packages' interaction with other Isabelle packages and
   133 %tools, such as the code generator and the counterexample generators.
   134 
   135 %\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
   136 %Limitations,'' concludes with known open issues at the time of writing.
   137 \end{itemize}
   138 
   139 
   140 \newbox\boxA
   141 \setbox\boxA=\hbox{\texttt{NOSPAM}}
   142 
   143 \newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
   144 in.\allowbreak tum.\allowbreak de}}
   145 \newcommand\authoremailii{\texttt{desh{\color{white}NOSPAM}\kern-\wd\boxA{}arna@\allowbreak
   146 in.\allowbreak tum.\allowbreak de}}
   147 \newcommand\authoremailiii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak
   148 in.\allowbreak tum.\allowbreak de}}
   149 \newcommand\authoremailiv{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak
   150 in.\allowbreak tum.\allowbreak de}}
   151 \newcommand\authoremailv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
   152 in.\allowbreak tum.\allowbreak de}}
   153 
   154 The command @{command datatype_new} is expected to replace \keyw{datatype} in a
   155 future release. Authors of new theories are encouraged to use the new commands,
   156 and maintainers of older theories may want to consider upgrading.
   157 
   158 Comments and bug reports concerning either the tool or this tutorial should be
   159 directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
   160 \authoremailiv, and \authoremailv.
   161 *}
   162 
   163 
   164 section {* Defining Datatypes
   165   \label{sec:defining-datatypes} *}
   166 
   167 text {*
   168 Datatypes can be specified using the @{command datatype_new} command.
   169 *}
   170 
   171 
   172 subsection {* Introductory Examples
   173   \label{ssec:datatype-introductory-examples} *}
   174 
   175 text {*
   176 Datatypes are illustrated through concrete examples featuring different flavors
   177 of recursion. More examples can be found in the directory
   178 \verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
   179 *}
   180 
   181 subsubsection {* Nonrecursive Types
   182   \label{sssec:datatype-nonrecursive-types} *}
   183 
   184 text {*
   185 Datatypes are introduced by specifying the desired names and argument types for
   186 their constructors. \emph{Enumeration} types are the simplest form of datatype.
   187 All their constructors are nullary:
   188 *}
   189 
   190     datatype_new trool = Truue | Faalse | Perhaaps
   191 
   192 text {*
   193 \noindent
   194 Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
   195 
   196 Polymorphic types are possible, such as the following option type, modeled after
   197 its homologue from the @{theory Option} theory:
   198 *}
   199 
   200 (*<*)
   201     hide_const None Some map_option
   202     hide_type option
   203 (*>*)
   204     datatype_new 'a option = None | Some 'a
   205 
   206 text {*
   207 \noindent
   208 The constructors are @{text "None :: 'a option"} and
   209 @{text "Some :: 'a \<Rightarrow> 'a option"}.
   210 
   211 The next example has three type parameters:
   212 *}
   213 
   214     datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
   215 
   216 text {*
   217 \noindent
   218 The constructor is
   219 @{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
   220 Unlike in Standard ML, curried constructors are supported. The uncurried variant
   221 is also possible:
   222 *}
   223 
   224     datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
   225 
   226 text {*
   227 \noindent
   228 Occurrences of nonatomic types on the right-hand side of the equal sign must be
   229 enclosed in double quotes, as is customary in Isabelle.
   230 *}
   231 
   232 
   233 subsubsection {* Simple Recursion
   234   \label{sssec:datatype-simple-recursion} *}
   235 
   236 text {*
   237 Natural numbers are the simplest example of a recursive type:
   238 *}
   239 
   240     datatype_new nat = Zero | Suc nat
   241 
   242 text {*
   243 \noindent
   244 Lists were shown in the introduction. Terminated lists are a variant that
   245 stores a value of type @{typ 'b} at the very end:
   246 *}
   247 
   248     datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
   249 
   250 
   251 subsubsection {* Mutual Recursion
   252   \label{sssec:datatype-mutual-recursion} *}
   253 
   254 text {*
   255 \emph{Mutually recursive} types are introduced simultaneously and may refer to
   256 each other. The example below introduces a pair of types for even and odd
   257 natural numbers:
   258 *}
   259 
   260     datatype_new even_nat = Even_Zero | Even_Suc odd_nat
   261     and odd_nat = Odd_Suc even_nat
   262 
   263 text {*
   264 \noindent
   265 Arithmetic expressions are defined via terms, terms via factors, and factors via
   266 expressions:
   267 *}
   268 
   269     datatype_new ('a, 'b) exp =
   270       Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
   271     and ('a, 'b) trm =
   272       Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
   273     and ('a, 'b) fct =
   274       Const 'a | Var 'b | Expr "('a, 'b) exp"
   275 
   276 
   277 subsubsection {* Nested Recursion
   278   \label{sssec:datatype-nested-recursion} *}
   279 
   280 text {*
   281 \emph{Nested recursion} occurs when recursive occurrences of a type appear under
   282 a type constructor. The introduction showed some examples of trees with nesting
   283 through lists. A more complex example, that reuses our @{type option} type,
   284 follows:
   285 *}
   286 
   287     datatype_new 'a btree =
   288       BNode 'a "'a btree option" "'a btree option"
   289 
   290 text {*
   291 \noindent
   292 Not all nestings are admissible. For example, this command will fail:
   293 *}
   294 
   295     datatype_new 'a wrong = W1 | W2 (*<*)'a
   296     typ (*>*)"'a wrong \<Rightarrow> 'a"
   297 
   298 text {*
   299 \noindent
   300 The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
   301 only through its right-hand side. This issue is inherited by polymorphic
   302 datatypes defined in terms of~@{text "\<Rightarrow>"}:
   303 *}
   304 
   305     datatype_new ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
   306     datatype_new 'a also_wrong = W1 | W2 (*<*)'a
   307     typ (*>*)"('a also_wrong, 'a) fun_copy"
   308 
   309 text {*
   310 \noindent
   311 The following definition of @{typ 'a}-branching trees is legal:
   312 *}
   313 
   314     datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
   315 
   316 text {*
   317 \noindent
   318 And so is the definition of hereditarily finite sets:
   319 *}
   320 
   321     datatype_new hfset = HFSet "hfset fset"
   322 
   323 text {*
   324 \noindent
   325 In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
   326 allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
   327 @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
   328 type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
   329 @{typ "('a, 'b) fun_copy"}, the type variable @{typ 'a} is dead and
   330 @{typ 'b} is live.
   331 
   332 Type constructors must be registered as BNFs to have live arguments. This is
   333 done automatically for datatypes and codatatypes introduced by the @{command
   334 datatype_new} and @{command codatatype} commands.
   335 Section~\ref{sec:introducing-bounded-natural-functors} explains how to
   336 register arbitrary type constructors as BNFs.
   337 
   338 Here is another example that fails:
   339 *}
   340 
   341     datatype_new 'a pow_list = PNil 'a (*<*)'a
   342     datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
   343 
   344 text {*
   345 \noindent
   346 This attempted definition features a different flavor of nesting, where the
   347 recursive call in the type specification occurs around (rather than inside)
   348 another type constructor.
   349 *}
   350 
   351 subsubsection {* Auxiliary Constants and Properties
   352   \label{sssec:datatype-auxiliary-constants-and-properties} *}
   353 
   354 text {*
   355 The @{command datatype_new} command introduces various constants in addition to
   356 the constructors. With each datatype are associated set functions, a map
   357 function, a relator, discriminators, and selectors, all of which can be given
   358 custom names. In the example below, the familiar names @{text null}, @{text hd},
   359 @{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
   360 default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
   361 @{text set_list}, @{text map_list}, and @{text rel_list}:
   362 *}
   363 
   364 (*<*)
   365     no_translations
   366       "[x, xs]" == "x # [xs]"
   367       "[x]" == "x # []"
   368 
   369     no_notation
   370       Nil ("[]") and
   371       Cons (infixr "#" 65)
   372 
   373     hide_type list
   374     hide_const Nil Cons hd tl set map list_all2 rec_list size_list
   375 
   376     context early begin
   377 (*>*)
   378     datatype_new (set: 'a) list =
   379       null: Nil
   380     | Cons (hd: 'a) (tl: "'a list")
   381     for
   382       map: map
   383       rel: list_all2
   384     where
   385       "tl Nil = Nil"
   386 
   387 text {*
   388 \noindent
   389 The types of the constants that appear in the specification are listed below.
   390 
   391 \medskip
   392 
   393 \begin{tabular}{@ {}ll@ {}}
   394 Constructors: &
   395   @{text "Nil \<Colon> 'a list"} \\
   396 &
   397   @{text "Cons \<Colon> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\
   398 Discriminator: &
   399   @{text "null \<Colon> 'a list \<Rightarrow> bool"} \\
   400 Selectors: &
   401   @{text "hd \<Colon> 'a list \<Rightarrow> 'a"} \\
   402 &
   403   @{text "tl \<Colon> 'a list \<Rightarrow> 'a list"} \\
   404 Set function: &
   405   @{text "set \<Colon> 'a list \<Rightarrow> 'a set"} \\
   406 Map function: &
   407   @{text "map \<Colon> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
   408 Relator: &
   409   @{text "list_all2 \<Colon> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"}
   410 \end{tabular}
   411 
   412 \medskip
   413 
   414 The discriminator @{const null} and the selectors @{const hd} and @{const tl}
   415 are characterized by the following conditional equations:
   416 %
   417 \[@{thm list.collapse(1)[of xs, no_vars]}
   418   \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
   419 %
   420 For two-constructor datatypes, a single discriminator constant is sufficient.
   421 The discriminator associated with @{const Cons} is simply
   422 @{term "\<lambda>xs. \<not> null xs"}.
   423 
   424 The \keyw{where} clause at the end of the command specifies a default value for
   425 selectors applied to constructors on which they are not a priori specified.
   426 Here, it is used to ensure that the tail of the empty list is itself (instead of
   427 being left unspecified).
   428 
   429 Because @{const Nil} is nullary, it is also possible to use
   430 @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
   431 if we omit the identifier @{const null} and the associated colon. Some users
   432 argue against this, because the mixture of constructors and selectors in the
   433 characteristic theorems can lead Isabelle's automation to switch between the
   434 constructor and the destructor view in surprising ways.
   435 
   436 The usual mixfix syntax annotations are available for both types and
   437 constructors. For example:
   438 *}
   439 
   440 (*<*)
   441     end
   442 (*>*)
   443     datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
   444 
   445 text {* \blankline *}
   446 
   447     datatype_new (set: 'a) list =
   448       null: Nil ("[]")
   449     | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
   450     for
   451       map: map
   452       rel: list_all2
   453 
   454 text {*
   455 \noindent
   456 Incidentally, this is how the traditional syntax can be set up:
   457 *}
   458 
   459     syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
   460 
   461 text {* \blankline *}
   462 
   463     translations
   464       "[x, xs]" == "x # [xs]"
   465       "[x]" == "x # []"
   466 
   467 
   468 subsection {* Command Syntax
   469   \label{ssec:datatype-command-syntax} *}
   470 
   471 
   472 subsubsection {* \keyw{datatype_new}
   473   \label{sssec:datatype-new} *}
   474 
   475 text {*
   476 \begin{matharray}{rcl}
   477   @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
   478 \end{matharray}
   479 
   480 @{rail \<open>
   481   @@{command datatype_new} target? @{syntax dt_options}? \<newline>
   482     (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
   483      @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
   484   ;
   485   @{syntax_def dt_options}: '(' (('discs_sels' | 'no_code') + ',') ')'
   486   ;
   487   @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
   488 \<close>}
   489 
   490 \medskip
   491 
   492 \noindent
   493 The @{command datatype_new} command introduces a set of mutually recursive
   494 datatypes specified by their constructors.
   495 
   496 The syntactic entity \synt{target} can be used to specify a local
   497 context (e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}),
   498 and \synt{prop} denotes a HOL proposition.
   499 
   500 The optional target is optionally followed by one or both of the following
   501 options:
   502 
   503 \begin{itemize}
   504 \setlength{\itemsep}{0pt}
   505 
   506 \item
   507 The @{text "discs_sels"} option indicates that discriminators and selectors
   508 should be generated. The option is implicitly enabled if names are specified for
   509 discriminators or selectors.
   510 
   511 \item
   512 The @{text "no_code"} option indicates that the datatype should not be
   513 registered for code generation.
   514 \end{itemize}
   515 
   516 The optional \keyw{where} clause specifies default values for selectors.
   517 Each proposition must be an equation of the form
   518 @{text "un_D (C \<dots>) = \<dots>"}, where @{text C} is a constructor and
   519 @{text un_D} is a selector.
   520 
   521 The left-hand sides of the datatype equations specify the name of the type to
   522 define, its type parameters, and additional information:
   523 
   524 @{rail \<open>
   525   @{syntax_def dt_name}: @{syntax tyargs}? name mixfix?
   526   ;
   527   @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')'
   528 \<close>}
   529 
   530 \medskip
   531 
   532 \noindent
   533 The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
   534 the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
   535 variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
   536 
   537 The optional names preceding the type variables allow to override the default
   538 names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
   539 arguments can be marked as dead by entering ``@{text dead}'' in front of the
   540 type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
   541 (and a set function is generated or not) depending on where they occur in the
   542 right-hand sides of the definition. Declaring a type argument as dead can speed
   543 up the type definition but will prevent any later (co)recursion through that
   544 type argument.
   545 
   546 Inside a mutually recursive specification, all defined datatypes must
   547 mention exactly the same type variables in the same order.
   548 
   549 @{rail \<open>
   550   @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) mixfix?
   551 \<close>}
   552 
   553 \medskip
   554 
   555 \noindent
   556 The main constituents of a constructor specification are the name of the
   557 constructor and the list of its argument types. An optional discriminator name
   558 can be supplied at the front to override the default, which is
   559 @{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
   560 @{text t.is_C\<^sub>j} otherwise.
   561 
   562 @{rail \<open>
   563   @{syntax_def dt_ctor_arg}: type | '(' name ':' type ')'
   564 \<close>}
   565 
   566 \medskip
   567 
   568 \noindent
   569 The syntactic entity \synt{type} denotes a HOL type \cite{isabelle-isar-ref}.
   570 
   571 In addition to the type of a constructor argument, it is possible to specify a
   572 name for the corresponding selector to override the default name
   573 (@{text un_C\<^sub>ji}). The same selector names can be reused for several
   574 constructors as long as they share the same type.
   575 *}
   576 
   577 
   578 subsubsection {* \keyw{datatype_compat}
   579   \label{sssec:datatype-compat} *}
   580 
   581 text {*
   582 \begin{matharray}{rcl}
   583   @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
   584 \end{matharray}
   585 
   586 @{rail \<open>
   587   @@{command datatype_compat} (name +)
   588 \<close>}
   589 
   590 \medskip
   591 
   592 \noindent
   593 The @{command datatype_compat} command registers new-style datatypes as
   594 old-style datatypes. For example:
   595 *}
   596 
   597     datatype_compat even_nat odd_nat
   598 
   599 text {* \blankline *}
   600 
   601     ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
   602 
   603 text {*
   604 The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
   605 
   606 The command is interesting because the old datatype package provides some
   607 functionality that is not yet replicated in the new package, such as the
   608 integration with Quickcheck.
   609 
   610 A few remarks concern nested recursive datatypes:
   611 
   612 \begin{itemize}
   613 \setlength{\itemsep}{0pt}
   614 
   615 \item The old-style, nested-as-mutual induction rule and recursor theorems are
   616 generated under their usual names but with ``@{text "compat_"}'' prefixed
   617 (e.g., @{text compat_tree.induct}).
   618 
   619 \item All types through which recursion takes place must be new-style datatypes
   620 or the function type. In principle, it should be possible to support old-style
   621 datatypes as well, but this has not been implemented yet (and there is currently
   622 no way to register old-style datatypes as new-style datatypes).
   623 
   624 \item The recursor produced for types that recurse through functions has a
   625 different signature than with the old package. This might affect the behavior of
   626 some third-party extensions.
   627 \end{itemize}
   628 
   629 An alternative to @{command datatype_compat} is to use the old package's
   630 \keyw{rep_\allowbreak datatype} command. The associated proof obligations must then be
   631 discharged manually.
   632 *}
   633 
   634 
   635 subsection {* Generated Constants
   636   \label{ssec:datatype-generated-constants} *}
   637 
   638 text {*
   639 Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
   640 with $m > 0$ live type variables and $n$ constructors
   641 @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
   642 following auxiliary constants are introduced:
   643 
   644 \medskip
   645 
   646 \begin{tabular}{@ {}ll@ {}}
   647 Case combinator: &
   648   @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
   649 Discriminators: &
   650   @{text "t.is_C\<^sub>1"}$, \ldots, $@{text "t.is_C\<^sub>n"} \\
   651 Selectors: &
   652   @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
   653 & \quad\vdots \\
   654 & @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
   655 Set functions: &
   656   @{text t.set1_t}, \ldots, @{text t.setm_t} \\
   657 Map function: &
   658   @{text t.map_t} \\
   659 Relator: &
   660   @{text t.rel_t} \\
   661 Recursor: &
   662   @{text t.rec_t} \\
   663 Size function: &
   664   @{text t.size_t}
   665 \end{tabular}
   666 
   667 \medskip
   668 
   669 \noindent
   670 The case combinator, discriminators, and selectors are collectively called
   671 \emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
   672 names and is normally hidden.
   673 
   674 In addition to the above, the @{class size} class is instantiated to overload the
   675 @{const size} function based on @{text t.size_t}.
   676 *}
   677 
   678 
   679 subsection {* Generated Theorems
   680   \label{ssec:datatype-generated-theorems} *}
   681 
   682 text {*
   683 The characteristic theorems generated by @{command datatype_new} are grouped in
   684 three broad categories:
   685 
   686 \begin{itemize}
   687 \setlength{\itemsep}{0pt}
   688 
   689 \item The \emph{free constructor theorems}
   690 (Section~\ref{sssec:free-constructor-theorems}) are properties of the
   691 constructors and destructors that can be derived for any freely generated type.
   692 Internally, the derivation is performed by @{command free_constructors}.
   693 
   694 \item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
   695 are properties of datatypes related to their BNF nature.
   696 
   697 \item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
   698 are properties of datatypes related to their inductive nature.
   699 
   700 \end{itemize}
   701 
   702 \noindent
   703 The full list of named theorems can be obtained as usual by entering the
   704 command \keyw{print_theorems} immediately after the datatype definition.
   705 This list normally excludes low-level theorems that reveal internal
   706 constructions. To make these accessible, add the line
   707 *}
   708 
   709     declare [[bnf_note_all]]
   710 (*<*)
   711     declare [[bnf_note_all = false]]
   712 (*>*)
   713 
   714 text {*
   715 \noindent
   716 to the top of the theory file.
   717 *}
   718 
   719 subsubsection {* Free Constructor Theorems
   720   \label{sssec:free-constructor-theorems} *}
   721 
   722 (*<*)
   723     consts nonnull :: 'a
   724 (*>*)
   725 
   726 text {*
   727 The free constructor theorems are partitioned in three subgroups. The first
   728 subgroup of properties is concerned with the constructors. They are listed below
   729 for @{typ "'a list"}:
   730 
   731 \begin{indentblock}
   732 \begin{description}
   733 
   734 \item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
   735 @{thm list.inject[no_vars]}
   736 
   737 \item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
   738 @{thm list.distinct(1)[no_vars]} \\
   739 @{thm list.distinct(2)[no_vars]}
   740 
   741 \item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
   742 @{thm list.exhaust[no_vars]}
   743 
   744 \item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
   745 @{thm list.nchotomy[no_vars]}
   746 
   747 \end{description}
   748 \end{indentblock}
   749 
   750 \noindent
   751 In addition, these nameless theorems are registered as safe elimination rules:
   752 
   753 \begin{indentblock}
   754 \begin{description}
   755 
   756 \item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
   757 @{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
   758 @{thm list.distinct(2)[THEN notE, elim!, no_vars]}
   759 
   760 \end{description}
   761 \end{indentblock}
   762 
   763 \noindent
   764 The next subgroup is concerned with the case combinator:
   765 
   766 \begin{indentblock}
   767 \begin{description}
   768 
   769 \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
   770 @{thm list.case(1)[no_vars]} \\
   771 @{thm list.case(2)[no_vars]}
   772 
   773 \item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
   774 @{thm list.case_cong[no_vars]}
   775 
   776 \item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
   777 @{thm list.case_cong_weak[no_vars]}
   778 
   779 \item[@{text "t."}\hthm{split}\rm:] ~ \\
   780 @{thm list.split[no_vars]}
   781 
   782 \item[@{text "t."}\hthm{split_asm}\rm:] ~ \\
   783 @{thm list.split_asm[no_vars]}
   784 
   785 \item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
   786 
   787 \end{description}
   788 \end{indentblock}
   789 
   790 \noindent
   791 The third subgroup revolves around discriminators and selectors:
   792 
   793 \begin{indentblock}
   794 \begin{description}
   795 
   796 \item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
   797 @{thm list.disc(1)[no_vars]} \\
   798 @{thm list.disc(2)[no_vars]}
   799 
   800 \item[@{text "t."}\hthm{discI}\rm:] ~ \\
   801 @{thm list.discI(1)[no_vars]} \\
   802 @{thm list.discI(2)[no_vars]}
   803 
   804 \item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
   805 @{thm list.sel(1)[no_vars]} \\
   806 @{thm list.sel(2)[no_vars]}
   807 
   808 \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
   809 @{thm list.collapse(1)[no_vars]} \\
   810 @{thm list.collapse(2)[no_vars]}
   811 
   812 \item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
   813 These properties are missing for @{typ "'a list"} because there is only one
   814 proper discriminator. Had the datatype been introduced with a second
   815 discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
   816 @{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
   817 @{prop "nonnull list \<Longrightarrow> \<not> null list"}
   818 
   819 \item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
   820 @{thm list.exhaust_disc[no_vars]}
   821 
   822 \item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
   823 @{thm list.exhaust_sel[no_vars]}
   824 
   825 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
   826 @{thm list.expand[no_vars]}
   827 
   828 \item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
   829 @{thm list.split_sel[no_vars]}
   830 
   831 \item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
   832 @{thm list.split_sel_asm[no_vars]}
   833 
   834 \item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}]
   835 
   836 \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
   837 @{thm list.case_eq_if[no_vars]}
   838 
   839 \end{description}
   840 \end{indentblock}
   841 
   842 \noindent
   843 In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
   844 attribute.
   845 *}
   846 
   847 
   848 subsubsection {* Functorial Theorems
   849   \label{sssec:functorial-theorems} *}
   850 
   851 text {*
   852 The functorial theorems are partitioned in two subgroups. The first subgroup
   853 consists of properties involving the constructors or the destructors and either
   854 a set function, the map function, or the relator:
   855 
   856 \begin{indentblock}
   857 \begin{description}
   858 
   859 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
   860 @{thm list.set(1)[no_vars]} \\
   861 @{thm list.set(2)[no_vars]}
   862 
   863 \item[@{text "t."}\hthm{set_cases}\rm:] ~ \\
   864 @{thm list.set_cases[no_vars]}
   865 
   866 \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\
   867 @{thm list.set_empty[no_vars]}
   868 
   869 \item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
   870 @{thm list.set_intros(1)[no_vars]} \\
   871 @{thm list.set_intros(2)[no_vars]}
   872 
   873 \item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
   874 @{thm list.set_sel[no_vars]}
   875 
   876 \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
   877 @{thm list.map(1)[no_vars]} \\
   878 @{thm list.map(2)[no_vars]}
   879 
   880 \item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
   881 @{thm list.map_disc_iff[no_vars]}
   882 
   883 \item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
   884 @{thm list.map_sel[no_vars]}
   885 
   886 \item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
   887 @{thm list.rel_inject(1)[no_vars]} \\
   888 @{thm list.rel_inject(2)[no_vars]}
   889 
   890 \item[@{text "t."}\hthm{rel_distinct} @{text "[simp]"}\rm:] ~ \\
   891 @{thm list.rel_distinct(1)[no_vars]} \\
   892 @{thm list.rel_distinct(2)[no_vars]}
   893 
   894 \item[@{text "t."}\hthm{rel_intros}\rm:] ~ \\
   895 @{thm list.rel_intros(1)[no_vars]} \\
   896 @{thm list.rel_intros(2)[no_vars]}
   897 
   898 % FIXME (and add @ before antiquotation below)
   899 %\item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
   900 %{thm list.rel_cases[no_vars]}
   901 
   902 \item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
   903 @{thm list.rel_sel[no_vars]}
   904 
   905 \end{description}
   906 \end{indentblock}
   907 
   908 \noindent
   909 In addition, equational versions of @{text t.rel_inject} and @{text
   910 rel_distinct} are registered with the @{text "[code]"} attribute.
   911 
   912 The second subgroup consists of more abstract properties of the set functions,
   913 the map function, and the relator:
   914 
   915 \begin{indentblock}
   916 \begin{description}
   917 
   918 \item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
   919 @{thm list.inj_map[no_vars]}
   920 
   921 \item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\
   922 @{thm list.inj_map_strong[no_vars]}
   923 
   924 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
   925 @{thm list.set_map[no_vars]}
   926 
   927 \item[@{text "t."}\hthm{map_comg0}\rm:] ~ \\
   928 @{thm list.map_cong0[no_vars]}
   929 
   930 \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
   931 @{thm list.map_cong[no_vars]}
   932 
   933 \item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
   934 @{thm list.map_cong_simp[no_vars]}
   935 
   936 \item[@{text "t."}\hthm{map_id}\rm:] ~ \\
   937 @{thm list.map_id[no_vars]}
   938 
   939 \item[@{text "t."}\hthm{map_id0}\rm:] ~ \\
   940 @{thm list.map_id0[no_vars]}
   941 
   942 \item[@{text "t."}\hthm{map_ident}\rm:] ~ \\
   943 @{thm list.map_ident[no_vars]}
   944 
   945 \item[@{text "t."}\hthm{rel_compp}\rm:] ~ \\
   946 @{thm list.rel_compp[no_vars]}
   947 
   948 \item[@{text "t."}\hthm{rel_conversep}\rm:] ~ \\
   949 @{thm list.rel_conversep[no_vars]}
   950 
   951 \item[@{text "t."}\hthm{rel_eq}\rm:] ~ \\
   952 @{thm list.rel_eq[no_vars]}
   953 
   954 \item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
   955 @{thm list.rel_flip[no_vars]}
   956 
   957 \item[@{text "t."}\hthm{rel_map}\rm:] ~ \\
   958 @{thm list.rel_map(1)[no_vars]} \\
   959 @{thm list.rel_map(2)[no_vars]}
   960 
   961 \item[@{text "t."}\hthm{rel_mono}\rm:] ~ \\
   962 @{thm list.rel_mono[no_vars]}
   963 
   964 \end{description}
   965 \end{indentblock}
   966 *}
   967 
   968 
   969 subsubsection {* Inductive Theorems
   970   \label{sssec:inductive-theorems} *}
   971 
   972 text {*
   973 The inductive theorems are as follows:
   974 
   975 \begin{indentblock}
   976 \begin{description}
   977 
   978 \item[@{text "t."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct t]"}\rm:] ~ \\
   979 @{thm list.induct[no_vars]}
   980 
   981 \item[@{text "t."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct pred]"}\rm:] ~ \\
   982 @{thm list.rel_induct[no_vars]}
   983 
   984 \item[\begin{tabular}{@ {}l@ {}}
   985   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm: \\
   986   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm: \\
   987 \end{tabular}] ~ \\
   988 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
   989 prove $m$ properties simultaneously.
   990 
   991 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
   992 @{thm list.rec(1)[no_vars]} \\
   993 @{thm list.rec(2)[no_vars]}
   994 
   995 \item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
   996 @{thm list.rec_o_map[no_vars]}
   997 
   998 \item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
   999 @{thm list.size(1)[no_vars]} \\
  1000 @{thm list.size(2)[no_vars]} \\
  1001 @{thm list.size(3)[no_vars]} \\
  1002 @{thm list.size(4)[no_vars]}
  1003 
  1004 \item[@{text "t."}\hthm{size_o_map}\rm:] ~ \\
  1005 @{thm list.size_o_map[no_vars]}
  1006 
  1007 \end{description}
  1008 \end{indentblock}
  1009 
  1010 \noindent
  1011 For convenience, @{command datatype_new} also provides the following collection:
  1012 
  1013 \begin{indentblock}
  1014 \begin{description}
  1015 
  1016 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\
  1017 @{text t.rel_distinct} @{text t.set}
  1018 
  1019 \end{description}
  1020 \end{indentblock}
  1021 *}
  1022 
  1023 
  1024 subsection {* Compatibility Issues
  1025   \label{ssec:datatype-compatibility-issues} *}
  1026 
  1027 text {*
  1028 The command @{command datatype_new} has been designed to be highly compatible
  1029 with the old \keyw{datatype}, to ease migration. There are nonetheless a few
  1030 incompatibilities that may arise when porting to the new package:
  1031 
  1032 \begin{itemize}
  1033 \setlength{\itemsep}{0pt}
  1034 
  1035 \item \emph{The Standard ML interfaces are different.} Tools and extensions
  1036 written to call the old ML interfaces will need to be adapted to the new
  1037 interfaces. This concerns Quickcheck in particular. Whenever possible, it is
  1038 recommended to use @{command datatype_compat} to register new-style datatypes
  1039 as old-style datatypes.
  1040 
  1041 \item \emph{The constants @{text t_case}, @{text t_rec}, and @{text t_size} are
  1042 now called @{text case_t}, @{text rec_t}, and @{text size_t}.}
  1043 
  1044 \item \emph{The recursor @{text rec_t} has a different signature for nested
  1045 recursive datatypes.} In the old package, nested recursion through non-functions
  1046 was internally reduced to mutual recursion. This reduction was visible in the
  1047 type of the recursor, used by \keyw{primrec}. Recursion through functions was
  1048 handled specially. In the new package, nested recursion (for functions and
  1049 non-functions) is handled in a more modular fashion. The old-style recursor can
  1050 be generated on demand using @{command primrec} if the recursion is via
  1051 new-style datatypes, as explained in
  1052 Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
  1053 
  1054 \item \emph{Accordingly, the induction rule is different for nested recursive
  1055 datatypes.} Again, the old-style induction rule can be generated on demand using
  1056 @{command primrec} if the recursion is via new-style datatypes, as explained in
  1057 Section~\ref{sssec:primrec-nested-as-mutual-recursion}.
  1058 
  1059 \item \emph{The internal constructions are completely different.} Proof texts
  1060 that unfold the definition of constants introduced by \keyw{datatype} will be
  1061 difficult to port.
  1062 
  1063 \item \emph{Some theorems have different names.}
  1064 For non-mutually recursive datatypes,
  1065 the alias @{text t.inducts} for @{text t.induct} is no longer generated.
  1066 For $m > 1$ mutually recursive datatypes,
  1067 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
  1068 @{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}, and similarly the
  1069 collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} has been divided into @{text "t\<^sub>1.size"},
  1070 \ldots, @{text "t\<^sub>m.size"}.
  1071 
  1072 \item \emph{The @{text t.simps} collection has been extended.}
  1073 Previously available theorems are available at the same index.
  1074 
  1075 \item \emph{Variables in generated properties have different names.} This is
  1076 rarely an issue, except in proof texts that refer to variable names in the
  1077 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
  1078 @{text "[of \<dots>]"} syntax.
  1079 \end{itemize}
  1080 
  1081 In the other direction, there is currently no way to register old-style
  1082 datatypes as new-style datatypes. If the goal is to define new-style datatypes
  1083 with nested recursion through old-style datatypes, the old-style
  1084 datatypes can be registered as a BNF
  1085 (Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
  1086 to derive discriminators and selectors, this can be achieved using
  1087 @{command free_constructors}
  1088 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
  1089 *}
  1090 
  1091 
  1092 section {* Defining Recursive Functions
  1093   \label{sec:defining-recursive-functions} *}
  1094 
  1095 text {*
  1096 Recursive functions over datatypes can be specified using the @{command primrec}
  1097 command, which supports primitive recursion, or using the more general
  1098 \keyw{fun} and \keyw{function} commands. Here, the focus is on
  1099 @{command primrec}; the other two commands are described in a separate
  1100 tutorial \cite{isabelle-function}.
  1101 
  1102 %%% TODO: partial_function
  1103 *}
  1104 
  1105 
  1106 subsection {* Introductory Examples
  1107   \label{ssec:primrec-introductory-examples} *}
  1108 
  1109 text {*
  1110 Primitive recursion is illustrated through concrete examples based on the
  1111 datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
  1112 examples can be found in the directory \verb|~~/src/HOL/BNF_Examples|.
  1113 *}
  1114 
  1115 
  1116 subsubsection {* Nonrecursive Types
  1117   \label{sssec:primrec-nonrecursive-types} *}
  1118 
  1119 text {*
  1120 Primitive recursion removes one layer of constructors on the left-hand side in
  1121 each equation. For example:
  1122 *}
  1123 
  1124     primrec bool_of_trool :: "trool \<Rightarrow> bool" where
  1125       "bool_of_trool Faalse \<longleftrightarrow> False" |
  1126       "bool_of_trool Truue \<longleftrightarrow> True"
  1127 
  1128 text {* \blankline *}
  1129 
  1130     primrec the_list :: "'a option \<Rightarrow> 'a list" where
  1131       "the_list None = []" |
  1132       "the_list (Some a) = [a]"
  1133 
  1134 text {* \blankline *}
  1135 
  1136     primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
  1137       "the_default d None = d" |
  1138       "the_default _ (Some a) = a"
  1139 
  1140 text {* \blankline *}
  1141 
  1142     primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
  1143       "mirrror (Triple a b c) = Triple c b a"
  1144 
  1145 text {*
  1146 \noindent
  1147 The equations can be specified in any order, and it is acceptable to leave out
  1148 some cases, which are then unspecified. Pattern matching on the left-hand side
  1149 is restricted to a single datatype, which must correspond to the same argument
  1150 in all equations.
  1151 *}
  1152 
  1153 
  1154 subsubsection {* Simple Recursion
  1155   \label{sssec:primrec-simple-recursion} *}
  1156 
  1157 text {*
  1158 For simple recursive types, recursive calls on a constructor argument are
  1159 allowed on the right-hand side:
  1160 *}
  1161 
  1162     primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
  1163       "replicate Zero _ = []" |
  1164       "replicate (Suc n) x = x # replicate n x"
  1165 
  1166 text {* \blankline *}
  1167 
  1168     primrec at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
  1169       "at (x # xs) j =
  1170          (case j of
  1171             Zero \<Rightarrow> x
  1172           | Suc j' \<Rightarrow> at xs j')"
  1173 
  1174 text {* \blankline *}
  1175 
  1176     primrec (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
  1177       "tfold _ (TNil y) = y" |
  1178       "tfold f (TCons x xs) = f x (tfold f xs)"
  1179 
  1180 text {*
  1181 \noindent
  1182 Pattern matching is only available for the argument on which the recursion takes
  1183 place. Fortunately, it is easy to generate pattern-maching equations using the
  1184 \keyw{simps_of_case} command provided by the theory
  1185 \verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
  1186 *}
  1187 
  1188     simps_of_case at_simps: at.simps
  1189 
  1190 text {*
  1191 This generates the lemma collection @{thm [source] at_simps}:
  1192 %
  1193 \[@{thm at_simps(1)[no_vars]}
  1194   \qquad @{thm at_simps(2)[no_vars]}\]
  1195 %
  1196 The next example is defined using \keyw{fun} to escape the syntactic
  1197 restrictions imposed on primitively recursive functions. The
  1198 @{command datatype_compat} command is needed to register new-style datatypes
  1199 for use with \keyw{fun} and \keyw{function}
  1200 (Section~\ref{sssec:datatype-compat}):
  1201 *}
  1202 
  1203     datatype_compat nat
  1204 
  1205 text {* \blankline *}
  1206 
  1207     fun at_least_two :: "nat \<Rightarrow> bool" where
  1208       "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
  1209       "at_least_two _ \<longleftrightarrow> False"
  1210 
  1211 
  1212 subsubsection {* Mutual Recursion
  1213   \label{sssec:primrec-mutual-recursion} *}
  1214 
  1215 text {*
  1216 The syntax for mutually recursive functions over mutually recursive datatypes
  1217 is straightforward:
  1218 *}
  1219 
  1220     primrec
  1221       nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
  1222       nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
  1223     where
  1224       "nat_of_even_nat Even_Zero = Zero" |
  1225       "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
  1226       "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
  1227 
  1228 text {* \blankline *}
  1229 
  1230     primrec
  1231       eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
  1232       eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
  1233       eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
  1234     where
  1235       "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
  1236       "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
  1237       "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f" |
  1238       "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
  1239       "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
  1240       "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
  1241       "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
  1242 
  1243 text {*
  1244 \noindent
  1245 Mutual recursion is possible within a single type, using \keyw{fun}:
  1246 *}
  1247 
  1248     fun
  1249       even :: "nat \<Rightarrow> bool" and
  1250       odd :: "nat \<Rightarrow> bool"
  1251     where
  1252       "even Zero = True" |
  1253       "even (Suc n) = odd n" |
  1254       "odd Zero = False" |
  1255       "odd (Suc n) = even n"
  1256 
  1257 
  1258 subsubsection {* Nested Recursion
  1259   \label{sssec:primrec-nested-recursion} *}
  1260 
  1261 text {*
  1262 In a departure from the old datatype package, nested recursion is normally
  1263 handled via the map functions of the nesting type constructors. For example,
  1264 recursive calls are lifted to lists using @{const map}:
  1265 *}
  1266 
  1267 (*<*)
  1268     datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
  1269 (*>*)
  1270     primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
  1271       "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
  1272          (case js of
  1273             [] \<Rightarrow> a
  1274           | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
  1275 
  1276 text {*
  1277 \noindent
  1278 The next example features recursion through the @{text option} type. Although
  1279 @{text option} is not a new-style datatype, it is registered as a BNF with the
  1280 map function @{const map_option}:
  1281 *}
  1282 
  1283     primrec (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
  1284       "sum_btree (BNode a lt rt) =
  1285          a + the_default 0 (map_option sum_btree lt) +
  1286            the_default 0 (map_option sum_btree rt)"
  1287 
  1288 text {*
  1289 \noindent
  1290 The same principle applies for arbitrary type constructors through which
  1291 recursion is possible. Notably, the map function for the function type
  1292 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
  1293 *}
  1294 
  1295     primrec (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
  1296       "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
  1297       "relabel_ft f (FTNode g) = FTNode (relabel_ft f \<circ> g)"
  1298 
  1299 text {*
  1300 \noindent
  1301 For convenience, recursion through functions can also be expressed using
  1302 $\lambda$-abstractions and function application rather than through composition.
  1303 For example:
  1304 *}
  1305 
  1306     primrec relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
  1307       "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
  1308       "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
  1309 
  1310 text {* \blankline *}
  1311 
  1312     primrec subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
  1313       "subtree_ft x (FTNode g) = g x"
  1314 
  1315 text {*
  1316 \noindent
  1317 For recursion through curried $n$-ary functions, $n$ applications of
  1318 @{term "op \<circ>"} are necessary. The examples below illustrate the case where
  1319 $n = 2$:
  1320 *}
  1321 
  1322     datatype_new 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
  1323 
  1324 text {* \blankline *}
  1325 
  1326     primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
  1327       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
  1328       "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
  1329 
  1330 text {* \blankline *}
  1331 
  1332     primrec relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
  1333       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)" |
  1334       "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
  1335 
  1336 text {* \blankline *}
  1337 
  1338     primrec subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
  1339       "subtree_ft2 x y (FTNode2 g) = g x y"
  1340 
  1341 
  1342 subsubsection {* Nested-as-Mutual Recursion
  1343   \label{sssec:primrec-nested-as-mutual-recursion} *}
  1344 
  1345 (*<*)
  1346     locale n2m begin
  1347 (*>*)
  1348 
  1349 text {*
  1350 For compatibility with the old package, but also because it is sometimes
  1351 convenient in its own right, it is possible to treat nested recursive datatypes
  1352 as mutually recursive ones if the recursion takes place though new-style
  1353 datatypes. For example:
  1354 *}
  1355 
  1356     primrec
  1357       at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
  1358       ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
  1359     where
  1360       "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
  1361          (case js of
  1362             [] \<Rightarrow> a
  1363           | j # js' \<Rightarrow> ats\<^sub>f\<^sub>f ts j js')" |
  1364       "ats\<^sub>f\<^sub>f (t # ts) j =
  1365          (case j of
  1366             Zero \<Rightarrow> at\<^sub>f\<^sub>f t
  1367           | Suc j' \<Rightarrow> ats\<^sub>f\<^sub>f ts j')"
  1368 
  1369 text {*
  1370 \noindent
  1371 Appropriate induction rules are generated as
  1372 @{thm [source] at\<^sub>f\<^sub>f.induct},
  1373 @{thm [source] ats\<^sub>f\<^sub>f.induct}, and
  1374 @{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The
  1375 induction rules and the underlying recursors are generated on a per-need basis
  1376 and are kept in a cache to speed up subsequent definitions.
  1377 
  1378 Here is a second example:
  1379 *}
  1380 
  1381     primrec
  1382       sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" and
  1383       sum_btree_option :: "'a btree option \<Rightarrow> 'a"
  1384     where
  1385       "sum_btree (BNode a lt rt) =
  1386          a + sum_btree_option lt + sum_btree_option rt" |
  1387       "sum_btree_option None = 0" |
  1388       "sum_btree_option (Some t) = sum_btree t"
  1389 
  1390 text {*
  1391 %  * can pretend a nested type is mutually recursive (if purely inductive)
  1392 %  * avoids the higher-order map
  1393 %  * e.g.
  1394 
  1395 %  * this can always be avoided;
  1396 %     * e.g. in our previous example, we first mapped the recursive
  1397 %       calls, then we used a generic at function to retrieve the result
  1398 %
  1399 %  * there's no hard-and-fast rule of when to use one or the other,
  1400 %    just like there's no rule when to use fold and when to use
  1401 %    primrec
  1402 %
  1403 %  * higher-order approach, considering nesting as nesting, is more
  1404 %    compositional -- e.g. we saw how we could reuse an existing polymorphic
  1405 %    at or the_default, whereas @{const ats\<^sub>f\<^sub>f} is much more specific
  1406 %
  1407 %  * but:
  1408 %     * is perhaps less intuitive, because it requires higher-order thinking
  1409 %     * may seem inefficient, and indeed with the code generator the
  1410 %       mutually recursive version might be nicer
  1411 %     * is somewhat indirect -- must apply a map first, then compute a result
  1412 %       (cannot mix)
  1413 %     * the auxiliary functions like @{const ats\<^sub>f\<^sub>f} are sometimes useful in own right
  1414 %
  1415 %  * impact on automation unclear
  1416 %
  1417 *}
  1418 (*<*)
  1419     end
  1420 (*>*)
  1421 
  1422 
  1423 subsection {* Command Syntax
  1424   \label{ssec:primrec-command-syntax} *}
  1425 
  1426 
  1427 subsubsection {* \keyw{primrec}
  1428   \label{sssec:primrec-new} *}
  1429 
  1430 text {*
  1431 \begin{matharray}{rcl}
  1432   @{command_def "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"}
  1433 \end{matharray}
  1434 
  1435 @{rail \<open>
  1436   @@{command primrec} target? @{syntax pr_option}? fixes \<newline>
  1437   @'where' (@{syntax pr_equation} + '|')
  1438   ;
  1439   @{syntax_def pr_option}: '(' 'nonexhaustive' ')'
  1440   ;
  1441   @{syntax_def pr_equation}: thmdecl? prop
  1442 \<close>}
  1443 
  1444 \medskip
  1445 
  1446 \noindent
  1447 The @{command primrec} command introduces a set of mutually recursive functions
  1448 over datatypes.
  1449 
  1450 The syntactic entity \synt{target} can be used to specify a local context,
  1451 \synt{fixes} denotes a list of names with optional type signatures,
  1452 \synt{thmdecl} denotes an optional name for the formula that follows, and
  1453 \synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
  1454 
  1455 The optional target is optionally followed by the following option:
  1456 
  1457 \begin{itemize}
  1458 \setlength{\itemsep}{0pt}
  1459 
  1460 \item
  1461 The @{text "nonexhaustive"} option indicates that the functions are not
  1462 necessarily specified for all constructors. It can be used to suppress the
  1463 warning that is normally emitted when some constructors are missing.
  1464 \end{itemize}
  1465 
  1466 %%% TODO: elaborate on format of the equations
  1467 %%% TODO: elaborate on mutual and nested-to-mutual
  1468 *}
  1469 
  1470 
  1471 (*
  1472 subsection {* Generated Theorems
  1473   \label{ssec:primrec-generated-theorems} *}
  1474 
  1475 text {*
  1476 %  * synthesized nonrecursive definition
  1477 %  * user specification is rederived from it, exactly as entered
  1478 %
  1479 %  * induct
  1480 %    * mutualized
  1481 %    * without some needless induction hypotheses if not used
  1482 %  * rec
  1483 %    * mutualized
  1484 *}
  1485 *)
  1486 
  1487 
  1488 subsection {* Recursive Default Values for Selectors
  1489   \label{ssec:primrec-recursive-default-values-for-selectors} *}
  1490 
  1491 text {*
  1492 A datatype selector @{text un_D} can have a default value for each constructor
  1493 on which it is not otherwise specified. Occasionally, it is useful to have the
  1494 default value be defined recursively. This leads to a chicken-and-egg
  1495 situation, because the datatype is not introduced yet at the moment when the
  1496 selectors are introduced. Of course, we can always define the selectors
  1497 manually afterward, but we then have to state and prove all the characteristic
  1498 theorems ourselves instead of letting the package do it.
  1499 
  1500 Fortunately, there is a workaround that relies on overloading to relieve us
  1501 from the tedium of manual derivations:
  1502 
  1503 \begin{enumerate}
  1504 \setlength{\itemsep}{0pt}
  1505 
  1506 \item
  1507 Introduce a fully unspecified constant @{text "un_D\<^sub>0 \<Colon> 'a"} using
  1508 @{keyword consts}.
  1509 
  1510 \item
  1511 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
  1512 value.
  1513 
  1514 \item
  1515 Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced
  1516 datatype using the \keyw{overloading} command.
  1517 
  1518 \item
  1519 Derive the desired equation on @{text un_D} from the characteristic equations
  1520 for @{text "un_D\<^sub>0"}.
  1521 \end{enumerate}
  1522 
  1523 \noindent
  1524 The following example illustrates this procedure:
  1525 *}
  1526 
  1527 (*<*)
  1528     hide_const termi
  1529 (*>*)
  1530     consts termi\<^sub>0 :: 'a
  1531 
  1532 text {* \blankline *}
  1533 
  1534     datatype_new ('a, 'b) tlist =
  1535       TNil (termi: 'b)
  1536     | TCons (thd: 'a) (ttl: "('a, 'b) tlist")
  1537     where
  1538       "ttl (TNil y) = TNil y"
  1539     | "termi (TCons _ xs) = termi\<^sub>0 xs"
  1540 
  1541 text {* \blankline *}
  1542 
  1543     overloading
  1544       termi\<^sub>0 \<equiv> "termi\<^sub>0 \<Colon> ('a, 'b) tlist \<Rightarrow> 'b"
  1545     begin
  1546     primrec termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
  1547       "termi\<^sub>0 (TNil y) = y" |
  1548       "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
  1549     end
  1550 
  1551 text {* \blankline *}
  1552 
  1553     lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs"
  1554     by (cases xs) auto
  1555 
  1556 
  1557 subsection {* Compatibility Issues
  1558   \label{ssec:primrec-compatibility-issues} *}
  1559 
  1560 text {*
  1561 The command @{command primrec}'s behavior on new-style datatypes has been
  1562 designed to be highly compatible with that for old-style datatypes, to ease
  1563 migration. There is nonetheless at least one incompatibility that may arise when
  1564 porting to the new package:
  1565 
  1566 \begin{itemize}
  1567 \setlength{\itemsep}{0pt}
  1568 
  1569 \item \emph{Some theorems have different names.}
  1570 For $m > 1$ mutually recursive functions,
  1571 @{text "f\<^sub>1_\<dots>_f\<^sub>m.simps"} has been broken down into separate
  1572 subcollections @{text "f\<^sub>i.simps"}.
  1573 \end{itemize}
  1574 *}
  1575 
  1576 
  1577 section {* Defining Codatatypes
  1578   \label{sec:defining-codatatypes} *}
  1579 
  1580 text {*
  1581 Codatatypes can be specified using the @{command codatatype} command. The
  1582 command is first illustrated through concrete examples featuring different
  1583 flavors of corecursion. More examples can be found in the directory
  1584 \verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
  1585 \emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
  1586 for lazy lists \cite{lochbihler-2010}.
  1587 *}
  1588 
  1589 
  1590 subsection {* Introductory Examples
  1591   \label{ssec:codatatype-introductory-examples} *}
  1592 
  1593 
  1594 subsubsection {* Simple Corecursion
  1595   \label{sssec:codatatype-simple-corecursion} *}
  1596 
  1597 text {*
  1598 Non-corecursive codatatypes coincide with the corresponding datatypes, so they
  1599 are rarely used in practice. \emph{Corecursive codatatypes} have the same syntax
  1600 as recursive datatypes, except for the command name. For example, here is the
  1601 definition of lazy lists:
  1602 *}
  1603 
  1604     codatatype (lset: 'a) llist =
  1605       lnull: LNil
  1606     | LCons (lhd: 'a) (ltl: "'a llist")
  1607     for
  1608       map: lmap
  1609       rel: llist_all2
  1610     where
  1611       "ltl LNil = LNil"
  1612 
  1613 text {*
  1614 \noindent
  1615 Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
  1616 @{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Here is a related type, that of
  1617 infinite streams:
  1618 *}
  1619 
  1620     codatatype (sset: 'a) stream =
  1621       SCons (shd: 'a) (stl: "'a stream")
  1622     for
  1623       map: smap
  1624       rel: stream_all2
  1625 
  1626 text {*
  1627 \noindent
  1628 Another interesting type that can
  1629 be defined as a codatatype is that of the extended natural numbers:
  1630 *}
  1631 
  1632     codatatype enat = EZero | ESuc enat
  1633 
  1634 text {*
  1635 \noindent
  1636 This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
  1637 that represents $\infty$. In addition, it has finite values of the form
  1638 @{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
  1639 
  1640 Here is an example with many constructors:
  1641 *}
  1642 
  1643     codatatype 'a process =
  1644       Fail
  1645     | Skip (cont: "'a process")
  1646     | Action (prefix: 'a) (cont: "'a process")
  1647     | Choice (left: "'a process") (right: "'a process")
  1648 
  1649 text {*
  1650 \noindent
  1651 Notice that the @{const cont} selector is associated with both @{const Skip}
  1652 and @{const Action}.
  1653 *}
  1654 
  1655 
  1656 subsubsection {* Mutual Corecursion
  1657   \label{sssec:codatatype-mutual-corecursion} *}
  1658 
  1659 text {*
  1660 \noindent
  1661 The example below introduces a pair of \emph{mutually corecursive} types:
  1662 *}
  1663 
  1664     codatatype even_enat = Even_EZero | Even_ESuc odd_enat
  1665     and odd_enat = Odd_ESuc even_enat
  1666 
  1667 
  1668 subsubsection {* Nested Corecursion
  1669   \label{sssec:codatatype-nested-corecursion} *}
  1670 
  1671 text {*
  1672 \noindent
  1673 The next examples feature \emph{nested corecursion}:
  1674 *}
  1675 
  1676     codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i (lbl\<^sub>i\<^sub>i: 'a) (sub\<^sub>i\<^sub>i: "'a tree\<^sub>i\<^sub>i llist")
  1677 
  1678 text {* \blankline *}
  1679 
  1680     codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s (lbl\<^sub>i\<^sub>s: 'a) (sub\<^sub>i\<^sub>s: "'a tree\<^sub>i\<^sub>s fset")
  1681 
  1682 text {* \blankline *}
  1683 
  1684     codatatype 'a sm = SM (accept: bool) (trans: "'a \<Rightarrow> 'a sm")
  1685 
  1686 
  1687 subsection {* Command Syntax
  1688   \label{ssec:codatatype-command-syntax} *}
  1689 
  1690 
  1691 subsubsection {* \keyw{codatatype}
  1692   \label{sssec:codatatype} *}
  1693 
  1694 text {*
  1695 \begin{matharray}{rcl}
  1696   @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
  1697 \end{matharray}
  1698 
  1699 @{rail \<open>
  1700   @@{command codatatype} target? \<newline>
  1701     (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
  1702 \<close>}
  1703 
  1704 \medskip
  1705 
  1706 \noindent
  1707 Definitions of codatatypes have almost exactly the same syntax as for datatypes
  1708 (Section~\ref{ssec:datatype-command-syntax}). The @{text "discs_sels"} option
  1709 is superfluous because discriminators and selectors are always generated for
  1710 codatatypes.
  1711 *}
  1712 
  1713 
  1714 subsection {* Generated Constants
  1715   \label{ssec:codatatype-generated-constants} *}
  1716 
  1717 text {*
  1718 Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
  1719 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
  1720 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
  1721 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
  1722 recursor is replaced by a dual concept and no size function is produced:
  1723 
  1724 \medskip
  1725 
  1726 \begin{tabular}{@ {}ll@ {}}
  1727 Corecursor: &
  1728   @{text t.corec_t}
  1729 \end{tabular}
  1730 *}
  1731 
  1732 
  1733 subsection {* Generated Theorems
  1734   \label{ssec:codatatype-generated-theorems} *}
  1735 
  1736 text {*
  1737 The characteristic theorems generated by @{command codatatype} are grouped in
  1738 three broad categories:
  1739 
  1740 \begin{itemize}
  1741 \setlength{\itemsep}{0pt}
  1742 
  1743 \item The \emph{free constructor theorems}
  1744 (Section~\ref{sssec:free-constructor-theorems}) are properties of the
  1745 constructors and destructors that can be derived for any freely generated type.
  1746 
  1747 \item The \emph{functorial theorems}
  1748 (Section~\ref{sssec:functorial-theorems}) are properties of datatypes related to
  1749 their BNF nature.
  1750 
  1751 \item The \emph{coinductive theorems} (Section~\ref{sssec:coinductive-theorems})
  1752 are properties of datatypes related to their coinductive nature.
  1753 \end{itemize}
  1754 
  1755 \noindent
  1756 The first two categories are exactly as for datatypes.
  1757 *}
  1758 
  1759 
  1760 subsubsection {* Coinductive Theorems
  1761   \label{sssec:coinductive-theorems} *}
  1762 
  1763 text {*
  1764 The coinductive theorems are listed below for @{typ "'a llist"}:
  1765 
  1766 \begin{indentblock}
  1767 \begin{description}
  1768 
  1769 \item[\begin{tabular}{@ {}l@ {}}
  1770   @{text "t."}\hthm{coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1771   \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  1772   D\<^sub>n, coinduct t]"}\rm:
  1773 \end{tabular}] ~ \\
  1774 @{thm llist.coinduct[no_vars]}
  1775 
  1776 \item[\begin{tabular}{@ {}l@ {}}
  1777   @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1778   \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
  1779 \end{tabular}] ~ \\
  1780 @{thm llist.coinduct_strong[no_vars]}
  1781 
  1782 \item[\begin{tabular}{@ {}l@ {}}
  1783   @{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1784   \phantom{@{text "t."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  1785   D\<^sub>n, coinduct pred]"}\rm:
  1786 \end{tabular}] ~ \\
  1787 @{thm llist.rel_coinduct[no_vars]}
  1788 
  1789 \item[\begin{tabular}{@ {}l@ {}}
  1790   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m, case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"} \\
  1791   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1792   \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
  1793   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1794   \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
  1795 \end{tabular}] ~ \\
  1796 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
  1797 used to prove $m$ properties simultaneously.
  1798 
  1799 \item[\begin{tabular}{@ {}l@ {}}
  1800   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{set_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n,"} \\
  1801   \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{set_induct} @{text "["}}@{text "induct set: set\<^sub>j_t\<^sub>1, \<dots>, induct set: set\<^sub>j_t\<^sub>m]"}\rm: \\
  1802 \end{tabular}] ~ \\
  1803 @{thm llist.set_induct[no_vars]} \\
  1804 If $m = 1$, the attribute @{text "[consumes 1]"} is generated as well.
  1805 
  1806 \item[@{text "t."}\hthm{corec}\rm:] ~ \\
  1807 @{thm llist.corec(1)[no_vars]} \\
  1808 @{thm llist.corec(2)[no_vars]}
  1809 
  1810 \item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
  1811 @{thm llist.corec_code[no_vars]}
  1812 
  1813 \item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
  1814 @{thm llist.corec_disc(1)[no_vars]} \\
  1815 @{thm llist.corec_disc(2)[no_vars]}
  1816 
  1817 \item[@{text "t."}\hthm{corec_disc_iff} @{text "[simp]"}\rm:] ~ \\
  1818 @{thm llist.corec_disc_iff(1)[no_vars]} \\
  1819 @{thm llist.corec_disc_iff(2)[no_vars]}
  1820 
  1821 \item[@{text "t."}\hthm{corec_sel} @{text "[simp]"}\rm:] ~ \\
  1822 @{thm llist.corec_sel(1)[no_vars]} \\
  1823 @{thm llist.corec_sel(2)[no_vars]}
  1824 
  1825 \end{description}
  1826 \end{indentblock}
  1827 
  1828 \noindent
  1829 For convenience, @{command codatatype} also provides the following collection:
  1830 
  1831 \begin{indentblock}
  1832 \begin{description}
  1833 
  1834 \item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff}] @{text t.corec_sel} ~ \\
  1835 @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
  1836 
  1837 \end{description}
  1838 \end{indentblock}
  1839 *}
  1840 
  1841 
  1842 section {* Defining Corecursive Functions
  1843   \label{sec:defining-corecursive-functions} *}
  1844 
  1845 text {*
  1846 Corecursive functions can be specified using the @{command primcorec} and
  1847 \keyw{prim\-corec\-ursive} commands, which support primitive corecursion, or
  1848 using the more general \keyw{partial_function} command. Here, the focus is on
  1849 the first two. More examples can be found in the directory
  1850 \verb|~~/src/HOL/BNF_Examples|.
  1851 
  1852 Whereas recursive functions consume datatypes one constructor at a time,
  1853 corecursive functions construct codatatypes one constructor at a time.
  1854 Partly reflecting a lack of agreement among proponents of coalgebraic methods,
  1855 Isabelle supports three competing syntaxes for specifying a function $f$:
  1856 
  1857 \begin{itemize}
  1858 \setlength{\itemsep}{0pt}
  1859 
  1860 \abovedisplayskip=.5\abovedisplayskip
  1861 \belowdisplayskip=.5\belowdisplayskip
  1862 
  1863 \item The \emph{destructor view} specifies $f$ by implications of the form
  1864 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
  1865 equations of the form
  1866 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\]
  1867 This style is popular in the coalgebraic literature.
  1868 
  1869 \item The \emph{constructor view} specifies $f$ by equations of the form
  1870 \[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C\<^sub>j \<dots>"}\]
  1871 This style is often more concise than the previous one.
  1872 
  1873 \item The \emph{code view} specifies $f$ by a single equation of the form
  1874 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
  1875 with restrictions on the format of the right-hand side. Lazy functional
  1876 programming languages such as Haskell support a generalized version of this
  1877 style.
  1878 \end{itemize}
  1879 
  1880 All three styles are available as input syntax. Whichever syntax is chosen,
  1881 characteristic theorems for all three styles are generated.
  1882 
  1883 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
  1884 %%% lists (cf. terminal0 in TLList.thy)
  1885 *}
  1886 
  1887 
  1888 subsection {* Introductory Examples
  1889   \label{ssec:primcorec-introductory-examples} *}
  1890 
  1891 text {*
  1892 Primitive corecursion is illustrated through concrete examples based on the
  1893 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
  1894 examples can be found in the directory \verb|~~/src/HOL/BNF_Examples|. The code
  1895 view is favored in the examples below. Sections
  1896 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
  1897 present the same examples expressed using the constructor and destructor views.
  1898 *}
  1899 
  1900 subsubsection {* Simple Corecursion
  1901   \label{sssec:primcorec-simple-corecursion} *}
  1902 
  1903 text {*
  1904 Following the code view, corecursive calls are allowed on the right-hand side as
  1905 long as they occur under a constructor, which itself appears either directly to
  1906 the right of the equal sign or in a conditional expression:
  1907 *}
  1908 
  1909     primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
  1910       "literate g x = LCons x (literate g (g x))"
  1911 
  1912 text {* \blankline *}
  1913 
  1914     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
  1915       "siterate g x = SCons x (siterate g (g x))"
  1916 
  1917 text {*
  1918 \noindent
  1919 The constructor ensures that progress is made---i.e., the function is
  1920 \emph{productive}. The above functions compute the infinite lazy list or stream
  1921 @{text "[x, g x, g (g x), \<dots>]"}. Productivity guarantees that prefixes
  1922 @{text "[x, g x, g (g x), \<dots>, (g ^^ k) x]"} of arbitrary finite length
  1923 @{text k} can be computed by unfolding the code equation a finite number of
  1924 times.
  1925 
  1926 Corecursive functions construct codatatype values, but nothing prevents them
  1927 from also consuming such values. The following function drops every second
  1928 element in a stream:
  1929 *}
  1930 
  1931     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
  1932       "every_snd s = SCons (shd s) (stl (stl s))"
  1933 
  1934 text {*
  1935 \noindent
  1936 Constructs such as @{text "let"}--@{text "in"}, @{text
  1937 "if"}--@{text "then"}--@{text "else"}, and @{text "case"}--@{text "of"} may
  1938 appear around constructors that guard corecursive calls:
  1939 *}
  1940 
  1941     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  1942       "lappend xs ys =
  1943          (case xs of
  1944             LNil \<Rightarrow> ys
  1945           | LCons x xs' \<Rightarrow> LCons x (lappend xs' ys))"
  1946 
  1947 text {*
  1948 \noindent
  1949 Pattern matching is not supported by @{command primcorec}. Fortunately, it is
  1950 easy to generate pattern-maching equations using the \keyw{simps_of_case}
  1951 command provided by the theory \verb|~~/src/HOL/Library/Simps_Case_Conv|.
  1952 *}
  1953 
  1954     simps_of_case lappend_simps: lappend.code
  1955 
  1956 text {*
  1957 This generates the lemma collection @{thm [source] lappend_simps}:
  1958 %
  1959 \begin{gather*%
  1960 }
  1961   @{thm lappend_simps(1)[no_vars]} \\
  1962   @{thm lappend_simps(2)[no_vars]}
  1963 \end{gather*%
  1964 }
  1965 %
  1966 Corecursion is useful to specify not only functions but also infinite objects:
  1967 *}
  1968 
  1969     primcorec infty :: enat where
  1970       "infty = ESuc infty"
  1971 
  1972 text {*
  1973 \noindent
  1974 The example below constructs a pseudorandom process value. It takes a stream of
  1975 actions (@{text s}), a pseudorandom function generator (@{text f}), and a
  1976 pseudorandom seed (@{text n}):
  1977 *}
  1978 
  1979     primcorec
  1980       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
  1981     where
  1982       "random_process s f n =
  1983          (if n mod 4 = 0 then
  1984             Fail
  1985           else if n mod 4 = 1 then
  1986             Skip (random_process s f (f n))
  1987           else if n mod 4 = 2 then
  1988             Action (shd s) (random_process (stl s) f (f n))
  1989           else
  1990             Choice (random_process (every_snd s) (f \<circ> f) (f n))
  1991               (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))"
  1992 
  1993 text {*
  1994 \noindent
  1995 The main disadvantage of the code view is that the conditions are tested
  1996 sequentially. This is visible in the generated theorems. The constructor and
  1997 destructor views offer nonsequential alternatives.
  1998 *}
  1999 
  2000 
  2001 subsubsection {* Mutual Corecursion
  2002   \label{sssec:primcorec-mutual-corecursion} *}
  2003 
  2004 text {*
  2005 The syntax for mutually corecursive functions over mutually corecursive
  2006 datatypes is unsurprising:
  2007 *}
  2008 
  2009     primcorec
  2010       even_infty :: even_enat and
  2011       odd_infty :: odd_enat
  2012     where
  2013       "even_infty = Even_ESuc odd_infty" |
  2014       "odd_infty = Odd_ESuc even_infty"
  2015 
  2016 
  2017 subsubsection {* Nested Corecursion
  2018   \label{sssec:primcorec-nested-corecursion} *}
  2019 
  2020 text {*
  2021 The next pair of examples generalize the @{const literate} and @{const siterate}
  2022 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
  2023 infinite trees in which subnodes are organized either as a lazy list (@{text
  2024 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}). They rely on the map functions of
  2025 the nesting type constructors to lift the corecursive calls:
  2026 *}
  2027 
  2028     primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2029       "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i g) (g x))"
  2030 
  2031 text {* \blankline *}
  2032 
  2033     primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
  2034       "iterate\<^sub>i\<^sub>s g x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s g) (g x))"
  2035 
  2036 text {*
  2037 \noindent
  2038 Both examples follow the usual format for constructor arguments associated
  2039 with nested recursive occurrences of the datatype. Consider
  2040 @{const iterate\<^sub>i\<^sub>i}. The term @{term "g x"} constructs an @{typ "'a llist"}
  2041 value, which is turned into an @{typ "'a tree\<^sub>i\<^sub>i llist"} value using
  2042 @{const lmap}.
  2043 
  2044 This format may sometimes feel artificial. The following function constructs
  2045 a tree with a single, infinite branch from a stream:
  2046 *}
  2047 
  2048     primcorec tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2049       "tree\<^sub>i\<^sub>i_of_stream s =
  2050          Node\<^sub>i\<^sub>i (shd s) (lmap tree\<^sub>i\<^sub>i_of_stream (LCons (stl s) LNil))"
  2051 
  2052 text {*
  2053 \noindent
  2054 A more natural syntax, also supported by Isabelle, is to move corecursive calls
  2055 under constructors:
  2056 *}
  2057 
  2058     primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2059       "tree\<^sub>i\<^sub>i_of_stream s =
  2060          Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
  2061 
  2062 text {*
  2063 The next example illustrates corecursion through functions, which is a bit
  2064 special. Deterministic finite automata (DFAs) are traditionally defined as
  2065 5-tuples @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
  2066 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
  2067 is an initial state, and @{text F} is a set of final states. The following
  2068 function translates a DFA into a state machine:
  2069 *}
  2070 
  2071     primcorec (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
  2072       "sm_of_dfa \<delta> F q = SM (q \<in> F) (sm_of_dfa \<delta> F \<circ> \<delta> q)"
  2073 
  2074 text {*
  2075 \noindent
  2076 The map function for the function type (@{text \<Rightarrow>}) is composition
  2077 (@{text "op \<circ>"}). For convenience, corecursion through functions can
  2078 also be expressed using $\lambda$-abstractions and function application rather
  2079 than through composition. For example:
  2080 *}
  2081 
  2082     primcorec sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
  2083       "sm_of_dfa \<delta> F q = SM (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
  2084 
  2085 text {* \blankline *}
  2086 
  2087     primcorec empty_sm :: "'a sm" where
  2088       "empty_sm = SM False (\<lambda>_. empty_sm)"
  2089 
  2090 text {* \blankline *}
  2091 
  2092     primcorec not_sm :: "'a sm \<Rightarrow> 'a sm" where
  2093       "not_sm M = SM (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
  2094 
  2095 text {* \blankline *}
  2096 
  2097     primcorec or_sm :: "'a sm \<Rightarrow> 'a sm \<Rightarrow> 'a sm" where
  2098       "or_sm M N =
  2099          SM (accept M \<or> accept N) (\<lambda>a. or_sm (trans M a) (trans N a))"
  2100 
  2101 text {*
  2102 \noindent
  2103 For recursion through curried $n$-ary functions, $n$ applications of
  2104 @{term "op \<circ>"} are necessary. The examples below illustrate the case where
  2105 $n = 2$:
  2106 *}
  2107 
  2108     codatatype ('a, 'b) sm2 =
  2109       SM2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) sm2")
  2110 
  2111 text {* \blankline *}
  2112 
  2113     primcorec
  2114       (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
  2115     where
  2116       "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
  2117 
  2118 text {* \blankline *}
  2119 
  2120     primcorec
  2121       sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
  2122     where
  2123       "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
  2124 
  2125 
  2126 subsubsection {* Nested-as-Mutual Corecursion
  2127   \label{sssec:primcorec-nested-as-mutual-corecursion} *}
  2128 
  2129 text {*
  2130 Just as it is possible to recurse over nested recursive datatypes as if they
  2131 were mutually recursive
  2132 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
  2133 pretend that nested codatatypes are mutually corecursive. For example:
  2134 *}
  2135 
  2136 (*<*)
  2137     context late
  2138     begin
  2139 (*>*)
  2140     primcorec
  2141       iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
  2142       iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
  2143     where
  2144       "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i g (g x))" |
  2145       "iterates\<^sub>i\<^sub>i g xs =
  2146          (case xs of
  2147             LNil \<Rightarrow> LNil
  2148           | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i g x) (iterates\<^sub>i\<^sub>i g xs'))"
  2149 
  2150 text {*
  2151 \noindent
  2152 Coinduction rules are generated as
  2153 @{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
  2154 @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
  2155 @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
  2156 and analogously for @{text coinduct_strong}. These rules and the
  2157 underlying corecursors are generated on a per-need basis and are kept in a cache
  2158 to speed up subsequent definitions.
  2159 *}
  2160 
  2161 (*<*)
  2162     end
  2163 (*>*)
  2164 
  2165 
  2166 subsubsection {* Constructor View
  2167   \label{ssec:primrec-constructor-view} *}
  2168 
  2169 (*<*)
  2170     locale ctr_view
  2171     begin
  2172 (*>*)
  2173 
  2174 text {*
  2175 The constructor view is similar to the code view, but there is one separate
  2176 conditional equation per constructor rather than a single unconditional
  2177 equation. Examples that rely on a single constructor, such as @{const literate}
  2178 and @{const siterate}, are identical in both styles.
  2179 
  2180 Here is an example where there is a difference:
  2181 *}
  2182 
  2183     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2184       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lappend xs ys = LNil" |
  2185       "_ \<Longrightarrow> lappend xs ys = LCons (lhd (if lnull xs then ys else xs))
  2186          (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
  2187 
  2188 text {*
  2189 \noindent
  2190 With the constructor view, we must distinguish between the @{const LNil} and
  2191 the @{const LCons} case. The condition for @{const LCons} is
  2192 left implicit, as the negation of that for @{const LNil}.
  2193 
  2194 For this example, the constructor view is slighlty more involved than the
  2195 code equation. Recall the code view version presented in
  2196 Section~\ref{sssec:primcorec-simple-corecursion}.
  2197 % TODO: \[{thm code_view.lappend.code}\]
  2198 The constructor view requires us to analyze the second argument (@{term ys}).
  2199 The code equation generated from the constructor view also suffers from this.
  2200 % TODO: \[{thm lappend.code}\]
  2201 
  2202 In contrast, the next example is arguably more naturally expressed in the
  2203 constructor view:
  2204 *}
  2205 
  2206     primcorec
  2207       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
  2208     where
  2209       "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
  2210       "n mod 4 = 1 \<Longrightarrow>
  2211          random_process s f n = Skip (random_process s f (f n))" |
  2212       "n mod 4 = 2 \<Longrightarrow>
  2213          random_process s f n = Action (shd s) (random_process (stl s) f (f n))" |
  2214       "n mod 4 = 3 \<Longrightarrow>
  2215          random_process s f n = Choice (random_process (every_snd s) f (f n))
  2216            (random_process (every_snd (stl s)) f (f n))"
  2217 (*<*)
  2218     end
  2219 (*>*)
  2220 
  2221 text {*
  2222 \noindent
  2223 Since there is no sequentiality, we can apply the equation for @{const Choice}
  2224 without having first to discharge @{term "n mod (4\<Colon>int) \<noteq> 0"},
  2225 @{term "n mod (4\<Colon>int) \<noteq> 1"}, and
  2226 @{term "n mod (4\<Colon>int) \<noteq> 2"}.
  2227 The price to pay for this elegance is that we must discharge exclusivity proof
  2228 obligations, one for each pair of conditions
  2229 @{term "(n mod (4\<Colon>int) = i, n mod (4\<Colon>int) = j)"}
  2230 with @{term "i < j"}. If we prefer not to discharge any obligations, we can
  2231 enable the @{text "sequential"} option. This pushes the problem to the users of
  2232 the generated properties.
  2233 %Here are more examples to conclude:
  2234 *}
  2235 
  2236 
  2237 subsubsection {* Destructor View
  2238   \label{ssec:primrec-destructor-view} *}
  2239 
  2240 (*<*)
  2241     locale dtr_view
  2242     begin
  2243 (*>*)
  2244 
  2245 text {*
  2246 The destructor view is in many respects dual to the constructor view. Conditions
  2247 determine which constructor to choose, and these conditions are interpreted
  2248 sequentially or not depending on the @{text "sequential"} option.
  2249 Consider the following examples:
  2250 *}
  2251 
  2252     primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
  2253       "\<not> lnull (literate _ x)" |
  2254       "lhd (literate _ x) = x" |
  2255       "ltl (literate g x) = literate g (g x)"
  2256 
  2257 text {* \blankline *}
  2258 
  2259     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
  2260       "shd (siterate _ x) = x" |
  2261       "stl (siterate g x) = siterate g (g x)"
  2262 
  2263 text {* \blankline *}
  2264 
  2265     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
  2266       "shd (every_snd s) = shd s" |
  2267       "stl (every_snd s) = stl (stl s)"
  2268 
  2269 text {*
  2270 \noindent
  2271 The first formula in the @{const literate} specification indicates which
  2272 constructor to choose. For @{const siterate} and @{const every_snd}, no such
  2273 formula is necessary, since the type has only one constructor. The last two
  2274 formulas are equations specifying the value of the result for the relevant
  2275 selectors. Corecursive calls appear directly to the right of the equal sign.
  2276 Their arguments are unrestricted.
  2277 
  2278 The next example shows how to specify functions that rely on more than one
  2279 constructor:
  2280 *}
  2281 
  2282     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2283       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
  2284       "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
  2285       "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)"
  2286 
  2287 text {*
  2288 \noindent
  2289 For a codatatype with $n$ constructors, it is sufficient to specify $n - 1$
  2290 discriminator formulas. The command will then assume that the remaining
  2291 constructor should be taken otherwise. This can be made explicit by adding
  2292 *}
  2293 
  2294 (*<*)
  2295     end
  2296 
  2297     locale dtr_view2
  2298     begin
  2299 
  2300     primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2301       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lappend xs ys)" |
  2302       "lhd (lappend xs ys) = lhd (if lnull xs then ys else xs)" |
  2303       "ltl (lappend xs ys) = (if xs = LNil then ltl ys else lappend (ltl xs) ys)" |
  2304 (*>*)
  2305       "_ \<Longrightarrow> \<not> lnull (lappend xs ys)"
  2306 
  2307 text {*
  2308 \noindent
  2309 to the specification. The generated selector theorems are conditional.
  2310 
  2311 The next example illustrates how to cope with selectors defined for several
  2312 constructors:
  2313 *}
  2314 
  2315     primcorec
  2316       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
  2317     where
  2318       "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" |
  2319       "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" |
  2320       "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" |
  2321       "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" |
  2322       "cont (random_process s f n) = random_process s f (f n)" of Skip |
  2323       "prefix (random_process s f n) = shd s" |
  2324       "cont (random_process s f n) = random_process (stl s) f (f n)" of Action |
  2325       "left (random_process s f n) = random_process (every_snd s) f (f n)" |
  2326       "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
  2327 
  2328 text {*
  2329 \noindent
  2330 Using the @{text "of"} keyword, different equations are specified for @{const
  2331 cont} depending on which constructor is selected.
  2332 
  2333 Here are more examples to conclude:
  2334 *}
  2335 
  2336     primcorec
  2337       even_infty :: even_enat and
  2338       odd_infty :: odd_enat
  2339     where
  2340       "even_infty \<noteq> Even_EZero" |
  2341       "un_Even_ESuc even_infty = odd_infty" |
  2342       "un_Odd_ESuc odd_infty = even_infty"
  2343 
  2344 text {* \blankline *}
  2345 
  2346     primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2347       "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = x" |
  2348       "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = lmap (iterate\<^sub>i\<^sub>i g) (g x)"
  2349 (*<*)
  2350     end
  2351 (*>*)
  2352 
  2353 
  2354 subsection {* Command Syntax
  2355   \label{ssec:primcorec-command-syntax} *}
  2356 
  2357 
  2358 subsubsection {* \keyw{primcorec} and \keyw{primcorecursive}
  2359   \label{sssec:primcorecursive-and-primcorec} *}
  2360 
  2361 text {*
  2362 \begin{matharray}{rcl}
  2363   @{command_def "primcorec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
  2364   @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  2365 \end{matharray}
  2366 
  2367 @{rail \<open>
  2368   (@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
  2369     @{syntax pcr_option}? fixes @'where' (@{syntax pcr_formula} + '|')
  2370   ;
  2371   @{syntax_def pcr_option}: '(' ('sequential' | 'exhaustive') ')'
  2372   ;
  2373   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
  2374 \<close>}
  2375 
  2376 \medskip
  2377 
  2378 \noindent
  2379 The @{command primcorec} and @{command primcorecursive} commands introduce a set
  2380 of mutually corecursive functions over codatatypes.
  2381 
  2382 The syntactic entity \synt{target} can be used to specify a local context,
  2383 \synt{fixes} denotes a list of names with optional type signatures,
  2384 \synt{thmdecl} denotes an optional name for the formula that follows, and
  2385 \synt{prop} denotes a HOL proposition \cite{isabelle-isar-ref}.
  2386 
  2387 The optional target is optionally followed by one or both of the following
  2388 options:
  2389 
  2390 \begin{itemize}
  2391 \setlength{\itemsep}{0pt}
  2392 
  2393 \item
  2394 The @{text "sequential"} option indicates that the conditions in specifications
  2395 expressed using the constructor or destructor view are to be interpreted
  2396 sequentially.
  2397 
  2398 \item
  2399 The @{text "exhaustive"} option indicates that the conditions in specifications
  2400 expressed using the constructor or destructor view cover all possible cases.
  2401 \end{itemize}
  2402 
  2403 The @{command primcorec} command is an abbreviation for @{command
  2404 primcorecursive} with @{text "by auto?"} to discharge any emerging proof
  2405 obligations.
  2406 
  2407 %%% TODO: elaborate on format of the propositions
  2408 %%% TODO: elaborate on mutual and nested-to-mutual
  2409 *}
  2410 
  2411 
  2412 (*
  2413 subsection {* Generated Theorems
  2414   \label{ssec:primcorec-generated-theorems} *}
  2415 *)
  2416 
  2417 
  2418 (*
  2419 subsection {* Recursive Default Values for Selectors
  2420   \label{ssec:primcorec-recursive-default-values-for-selectors} *}
  2421 
  2422 text {*
  2423 partial_function to the rescue
  2424 *}
  2425 *)
  2426 
  2427 
  2428 section {* Introducing Bounded Natural Functors
  2429   \label{sec:introducing-bounded-natural-functors} *}
  2430 
  2431 text {*
  2432 The (co)datatype package can be set up to allow nested recursion through
  2433 arbitrary type constructors, as long as they adhere to the BNF requirements
  2434 and are registered as BNFs. It is also possible to declare a BNF abstractly
  2435 without specifying its internal structure.
  2436 *}
  2437 
  2438 
  2439 subsection {* Bounded Natural Functors
  2440   \label{ssec:bounded-natural-functors} *}
  2441 
  2442 text {*
  2443 Bounded natural functors (BNFs) are a semantic criterion for where
  2444 (co)re\-cur\-sion may appear on the right-hand side of an equation
  2445 \cite{traytel-et-al-2012,blanchette-et-al-wit}.
  2446 
  2447 An $n$-ary BNF is a type constructor equipped with a map function
  2448 (functorial action), $n$ set functions (natural transformations),
  2449 and an infinite cardinal bound that satisfy certain properties.
  2450 For example, @{typ "'a llist"} is a unary BNF.
  2451 Its relator @{text "llist_all2 \<Colon>
  2452   ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow>
  2453   'a llist \<Rightarrow> 'b llist \<Rightarrow> bool"}
  2454 extends binary predicates over elements to binary predicates over parallel
  2455 lazy lists. The cardinal bound limits the number of elements returned by the
  2456 set function; it may not depend on the cardinality of @{typ 'a}.
  2457 
  2458 The type constructors introduced by @{command datatype_new} and
  2459 @{command codatatype} are automatically registered as BNFs. In addition, a
  2460 number of old-style datatypes and non-free types are preregistered.
  2461 
  2462 Given an $n$-ary BNF, the $n$ type variables associated with set functions,
  2463 and on which the map function acts, are \emph{live}; any other variables are
  2464 \emph{dead}. Nested (co)recursion can only take place through live variables.
  2465 *}
  2466 
  2467 
  2468 subsection {* Introductory Examples
  2469   \label{ssec:bnf-introductory-examples} *}
  2470 
  2471 text {*
  2472 The example below shows how to register a type as a BNF using the @{command bnf}
  2473 command. Some of the proof obligations are best viewed with the theory
  2474 @{theory Cardinal_Notations}, located in \verb|~~/src/HOL/Library|,
  2475 imported.
  2476 
  2477 The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
  2478 is live and @{typ 'd} is dead. We introduce it together with its map function,
  2479 set function, and relator.
  2480 *}
  2481 
  2482     typedef ('d, 'a) fn = "UNIV \<Colon> ('d \<Rightarrow> 'a) set"
  2483     by simp
  2484 
  2485     text {* \blankline *}
  2486 
  2487     setup_lifting type_definition_fn
  2488 
  2489 text {* \blankline *}
  2490 
  2491     lift_definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" is "op \<circ>" .
  2492     lift_definition set_fn :: "('d, 'a) fn \<Rightarrow> 'a set" is range .
  2493 
  2494 text {* \blankline *}
  2495 
  2496     lift_definition
  2497       rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
  2498     is
  2499       "rel_fun (op =)" .
  2500 
  2501 text {* \blankline *}
  2502 
  2503     bnf "('d, 'a) fn"
  2504       map: map_fn
  2505       sets: set_fn
  2506       bd: "natLeq +c |UNIV :: 'd set|"
  2507       rel: rel_fn
  2508     proof -
  2509       show "map_fn id = id"
  2510         by transfer auto
  2511     next
  2512       fix F G show "map_fn (G \<circ> F) = map_fn G \<circ> map_fn F"
  2513         by transfer (auto simp add: comp_def)
  2514     next
  2515       fix F f g
  2516       assume "\<And>x. x \<in> set_fn F \<Longrightarrow> f x = g x"
  2517       thus "map_fn f F = map_fn g F"
  2518         by transfer auto
  2519     next
  2520       fix f show "set_fn \<circ> map_fn f = op ` f \<circ> set_fn"
  2521         by transfer (auto simp add: comp_def)
  2522     next
  2523       show "card_order (natLeq +c |UNIV \<Colon> 'd set| )"
  2524         apply (rule card_order_csum)
  2525         apply (rule natLeq_card_order)
  2526         by (rule card_of_card_order_on)
  2527     next
  2528       show "cinfinite (natLeq +c |UNIV \<Colon> 'd set| )"
  2529         apply (rule cinfinite_csum)
  2530         apply (rule disjI1)
  2531         by (rule natLeq_cinfinite)
  2532     next
  2533       fix F :: "('d, 'a) fn"
  2534       have "|set_fn F| \<le>o |UNIV \<Colon> 'd set|" (is "_ \<le>o ?U")
  2535         by transfer (rule card_of_image)
  2536       also have "?U \<le>o natLeq +c ?U"
  2537         by (rule ordLeq_csum2) (rule card_of_Card_order)
  2538       finally show "|set_fn F| \<le>o natLeq +c |UNIV \<Colon> 'd set|" .
  2539     next
  2540       fix R S
  2541       show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
  2542         by (rule, transfer) (auto simp add: rel_fun_def)
  2543     next
  2544       fix R
  2545       show "rel_fn R =
  2546             (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
  2547              BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
  2548         unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
  2549         apply transfer
  2550         unfolding rel_fun_def subset_iff image_iff
  2551         by auto (force, metis pair_collapse)
  2552     qed
  2553 
  2554 text {* \blankline *}
  2555 
  2556     print_theorems
  2557     print_bnfs
  2558 
  2559 text {*
  2560 \noindent
  2561 Using \keyw{print_theorems} and @{keyword print_bnfs}, we can contemplate and
  2562 show the world what we have achieved.
  2563 
  2564 This particular example does not need any nonemptiness witness, because the
  2565 one generated by default is good enough, but in general this would be
  2566 necessary. See \verb|~~/src/HOL/Basic_BNFs.thy|,
  2567 \verb|~~/src/HOL/Library/FSet.thy|, and \verb|~~/src/HOL/Library/Multiset.thy|
  2568 for further examples of BNF registration, some of which feature custom
  2569 witnesses.
  2570 
  2571 The next example declares a BNF axiomatically. This can be convenient for
  2572 reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization}
  2573 command below introduces a type @{text "('a, 'b, 'c) F"}, three set constants,
  2574 a map function, a relator, and a nonemptiness witness that depends only on
  2575 @{typ 'a}. (The type @{text "'a \<Rightarrow> ('a, 'b, 'c) F"} of
  2576 the witness can be read as an implication: If we have a witness for @{typ 'a},
  2577 we can construct a witness for @{text "('a, 'b, 'c) F"}.) The BNF
  2578 properties are postulated as axioms.
  2579 *}
  2580 
  2581     bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F
  2582       [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
  2583 
  2584 text {* \blankline *}
  2585 
  2586     print_theorems
  2587     print_bnfs
  2588 
  2589 
  2590 subsection {* Command Syntax
  2591   \label{ssec:bnf-command-syntax} *}
  2592 
  2593 
  2594 subsubsection {* \keyw{bnf}
  2595   \label{sssec:bnf} *}
  2596 
  2597 text {*
  2598 \begin{matharray}{rcl}
  2599   @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  2600 \end{matharray}
  2601 
  2602 @{rail \<open>
  2603   @@{command bnf} target? (name ':')? type \<newline>
  2604     'map:' term ('sets:' (term +))? 'bd:' term \<newline>
  2605     ('wits:' (term +))? ('rel:' term)?
  2606 \<close>}
  2607 
  2608 \medskip
  2609 
  2610 \noindent
  2611 The @{command bnf} command registers an existing type as a bounded natural
  2612 functor (BNF). The type must be equipped with an appropriate map function
  2613 (functorial action). In addition, custom set functions, relators, and
  2614 nonemptiness witnesses can be specified; otherwise, default versions are used.
  2615 
  2616 The syntactic entity \synt{target} can be used to specify a local context,
  2617 \synt{type} denotes a HOL type, and \synt{term} denotes a HOL term
  2618 \cite{isabelle-isar-ref}.
  2619 
  2620 %%% TODO: elaborate on proof obligations
  2621 *}
  2622 
  2623 
  2624 subsubsection {* \keyw{bnf_axiomatization}
  2625   \label{sssec:bnf-axiomatization} *}
  2626 
  2627 text {*
  2628 \begin{matharray}{rcl}
  2629   @{command_def "bnf_axiomatization"} & : & @{text "local_theory \<rightarrow> local_theory"}
  2630 \end{matharray}
  2631 
  2632 @{rail \<open>
  2633   @@{command bnf_axiomatization} target? @{syntax tyargs}? name \<newline>
  2634     @{syntax wit_types}? mixfix? @{syntax map_rel}?
  2635   ;
  2636   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
  2637 \<close>}
  2638 
  2639 \medskip
  2640 
  2641 \noindent
  2642 The @{command bnf_axiomatization} command declares a new type and associated constants
  2643 (map, set, relator, and cardinal bound) and asserts the BNF properties for
  2644 these constants as axioms.
  2645 
  2646 The syntactic entity \synt{target} can be used to specify a local context,
  2647 \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable
  2648 (@{typ 'a}, @{typ 'b}, \ldots), and \synt{mixfix} denotes the usual
  2649 parenthesized mixfix notation \cite{isabelle-isar-ref}.
  2650 
  2651 Type arguments are live by default; they can be marked as dead by entering
  2652 ``@{text dead}'' in front of the type variable (e.g., ``@{text "(dead 'a)"}'')
  2653 instead of an identifier for the corresponding set function. Witnesses can be
  2654 specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
  2655 is identical to the left-hand side of a @{command datatype_new} or
  2656 @{command codatatype} definition.
  2657 
  2658 The command is useful to reason abstractly about BNFs. The axioms are safe
  2659 because there exist BNFs of arbitrary large arities. Applications must import
  2660 the theory @{theory BNF_Axiomatization}, located in the directory
  2661 \verb|~~/src/|\allowbreak\verb|HOL/Library|, to use this functionality.
  2662 *}
  2663 
  2664 
  2665 subsubsection {* \keyw{print_bnfs}
  2666   \label{sssec:print-bnfs} *}
  2667 
  2668 text {*
  2669 \begin{matharray}{rcl}
  2670   @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
  2671 \end{matharray}
  2672 
  2673 @{rail \<open>
  2674   @@{command print_bnfs}
  2675 \<close>}
  2676 *}
  2677 
  2678 
  2679 section {* Deriving Destructors and Theorems for Free Constructors
  2680   \label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
  2681 
  2682 text {*
  2683 The derivation of convenience theorems for types equipped with free constructors,
  2684 as performed internally by @{command datatype_new} and @{command codatatype},
  2685 is available as a stand-alone command called @{command free_constructors}.
  2686 
  2687 %  * need for this is rare but may arise if you want e.g. to add destructors to
  2688 %    a type not introduced by ...
  2689 %
  2690 %  * also useful for compatibility with old package, e.g. add destructors to
  2691 %    old \keyw{datatype}
  2692 %
  2693 %  * @{command free_constructors}
  2694 %    * @{text "no_discs_sels"}, @{text "no_code"}
  2695 %    * hack to have both co and nonco view via locale (cf. ext nats)
  2696 %  * code generator
  2697 %     * eq, refl, simps
  2698 *}
  2699 
  2700 
  2701 (*
  2702 subsection {* Introductory Example
  2703   \label{ssec:ctors-introductory-example} *}
  2704 *)
  2705 
  2706 
  2707 subsection {* Command Syntax
  2708   \label{ssec:ctors-command-syntax} *}
  2709 
  2710 
  2711 subsubsection {* \keyw{free_constructors}
  2712   \label{sssec:free-constructors} *}
  2713 
  2714 text {*
  2715 \begin{matharray}{rcl}
  2716   @{command_def "free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  2717 \end{matharray}
  2718 
  2719 @{rail \<open>
  2720   @@{command free_constructors} target? @{syntax dt_options} \<newline>
  2721     name 'for' (@{syntax fc_ctor} + '|') \<newline>
  2722   (@'where' (prop + '|'))?
  2723   ;
  2724   @{syntax_def fc_ctor}: (name ':')? term (name * )
  2725 \<close>}
  2726 
  2727 \medskip
  2728 
  2729 \noindent
  2730 The @{command free_constructors} command generates destructor constants for
  2731 freely constructed types as well as properties about constructors and
  2732 destructors. It also registers the constants and theorems in a data structure
  2733 that is queried by various tools (e.g., \keyw{function}).
  2734 
  2735 The syntactic entity \synt{target} can be used to specify a local context,
  2736 \synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
  2737 \synt{term} denotes a HOL term \cite{isabelle-isar-ref}.
  2738 
  2739 The syntax resembles that of @{command datatype_new} and @{command codatatype}
  2740 definitions (Sections
  2741 \ref{ssec:datatype-command-syntax}~and~\ref{ssec:codatatype-command-syntax}).
  2742 A constructor is specified by an optional name for the discriminator, the
  2743 constructor itself (as a term), and a list of optional names for the selectors.
  2744 
  2745 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
  2746 For bootstrapping reasons, the generally useful @{text "[fundef_cong]"}
  2747 attribute is not set on the generated @{text case_cong} theorem. It can be
  2748 added manually using \keyw{declare}.
  2749 *}
  2750 
  2751 
  2752 (*
  2753 section {* Standard ML Interface
  2754   \label{sec:standard-ml-interface} *}
  2755 
  2756 text {*
  2757 The package's programmatic interface.
  2758 *}
  2759 *)
  2760 
  2761 
  2762 (*
  2763 section {* Interoperability
  2764   \label{sec:interoperability} *}
  2765 
  2766 text {*
  2767 The package's interaction with other Isabelle packages and tools, such as the
  2768 code generator and the counterexample generators.
  2769 *}
  2770 
  2771 
  2772 subsection {* Transfer and Lifting
  2773   \label{ssec:transfer-and-lifting} *}
  2774 
  2775 
  2776 subsection {* Code Generator
  2777   \label{ssec:code-generator} *}
  2778 
  2779 
  2780 subsection {* Quickcheck
  2781   \label{ssec:quickcheck} *}
  2782 
  2783 
  2784 subsection {* Nitpick
  2785   \label{ssec:nitpick} *}
  2786 
  2787 
  2788 subsection {* Nominal Isabelle
  2789   \label{ssec:nominal-isabelle} *}
  2790 *)
  2791 
  2792 
  2793 (*
  2794 section {* Known Bugs and Limitations
  2795   \label{sec:known-bugs-and-limitations} *}
  2796 
  2797 text {*
  2798 Known open issues of the package.
  2799 *}
  2800 
  2801 text {*
  2802 %* slow n-ary mutual (co)datatype, avoid as much as possible (e.g. using nesting)
  2803 %
  2804 %* partial documentation
  2805 %
  2806 %* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
  2807 %  (for @{command datatype_compat} and prim(co)rec)
  2808 %
  2809 %    * a fortiori, no way to register same type as both data- and codatatype
  2810 %
  2811 %* no recursion through unused arguments (unlike with the old package)
  2812 %
  2813 %* in a locale, cannot use locally fixed types (because of limitation in typedef)?
  2814 %
  2815 % *names of variables suboptimal
  2816 *}
  2817 *)
  2818 
  2819 
  2820 text {*
  2821 \section*{Acknowledgment}
  2822 
  2823 Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
  2824 (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
  2825 versions of the package, especially on the coinductive part. Brian Huffman
  2826 suggested major simplifications to the internal constructions, many of which
  2827 have yet to be implemented. Florian Haftmann and Christian Urban provided
  2828 general advice on Isabelle and package writing. Stefan Milius and Lutz
  2829 Schr\"oder found an elegant proof that eliminated one of the BNF proof
  2830 obligations. Andreas Lochbihler and Christian Sternagel suggested many textual
  2831 improvements to this tutorial.
  2832 *}
  2833 
  2834 end