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