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