src/Doc/Datatypes/Datatypes.thy
author wenzelm
Mon Oct 30 20:04:10 2017 +0100 (22 months ago)
changeset 66946 3d8fd98c7c86
parent 66453 cc19f7ca2ed6
child 67325 79260409a680
permissions -rw-r--r--
ROOT cleanup: empty 'document_files' means there is no document;
     1 (*  Title:      Doc/Datatypes/Datatypes.thy
     2     Author:     Julian Biendarra, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Author:     Martin Desharnais, Ecole de technologie superieure
     5     Author:     Lorenz Panny, TU Muenchen
     6     Author:     Andrei Popescu, TU Muenchen
     7     Author:     Dmitriy Traytel, TU Muenchen
     8 
     9 Tutorial for (co)datatype definitions.
    10 *)
    11 
    12 theory Datatypes
    13 imports
    14   Setup
    15   "HOL-Library.BNF_Axiomatization"
    16   "HOL-Library.Cardinal_Notations"
    17   "HOL-Library.Countable"
    18   "HOL-Library.FSet"
    19   "HOL-Library.Simps_Case_Conv"
    20 begin
    21 
    22 section \<open>Introduction
    23   \label{sec:introduction}\<close>
    24 
    25 text \<open>
    26 The 2013 edition of Isabelle introduced a definitional package for freely
    27 generated datatypes and codatatypes. This package replaces the earlier
    28 implementation due to Berghofer and Wenzel @{cite "Berghofer-Wenzel:1999:TPHOL"}.
    29 Perhaps the main advantage of the new package is that it supports recursion
    30 through a large class of non-datatypes, such as finite sets:
    31 \<close>
    32 
    33     datatype '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")
    34 
    35 text \<open>
    36 \noindent
    37 Another strong point is the support for local definitions:
    38 \<close>
    39 
    40     context linorder
    41     begin
    42     datatype flag = Less | Eq | Greater
    43     end
    44 
    45 text \<open>
    46 \noindent
    47 Furthermore, the package provides a lot of convenience, including automatically
    48 generated discriminators, selectors, and relators as well as a wealth of
    49 properties about them.
    50 
    51 In addition to inductive datatypes, the package supports coinductive
    52 datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
    53 following command introduces the type of lazy lists, which comprises both finite
    54 and infinite values:
    55 \<close>
    56 
    57 (*<*)
    58     locale early
    59     locale late
    60 (*>*)
    61     codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
    62 
    63 text \<open>
    64 \noindent
    65 Mixed inductive--coinductive recursion is possible via nesting. Compare the
    66 following four Rose tree examples:
    67 \<close>
    68 
    69     datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
    70     datatype (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
    71     codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
    72     codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
    73 
    74 text \<open>
    75 The first two tree types allow only paths of finite length, whereas the last two
    76 allow infinite paths. Orthogonally, the nodes in the first and third types have
    77 finitely many direct subtrees, whereas those of the second and fourth may have
    78 infinite branching.
    79 
    80 The package is part of @{theory Main}. Additional functionality is provided by
    81 the theory \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close>.
    82 
    83 The package, like its predecessor, fully adheres to the LCF philosophy
    84 @{cite mgordon79}: The characteristic theorems associated with the specified
    85 (co)datatypes are derived rather than introduced axiomatically.%
    86 \footnote{However, some of the
    87 internal constructions and most of the internal proof obligations are omitted
    88 if the @{text quick_and_dirty} option is enabled.}
    89 The package is described in a number of scientific papers
    90 @{cite "traytel-et-al-2012" and "blanchette-et-al-2014-impl" and
    91 "panny-et-al-2014" and "blanchette-et-al-2015-wit"}.
    92 The central notion is that of a \emph{bounded natural functor} (BNF)---a
    93 well-behaved type constructor for which nested (co)recursion is supported.
    94 
    95 This tutorial is organized as follows:
    96 
    97 \begin{itemize}
    98 \setlength{\itemsep}{0pt}
    99 
   100 \item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
   101 describes how to specify datatypes using the @{command datatype} command.
   102 
   103 \item Section \ref{sec:defining-primitively-recursive-functions}, ``Defining
   104 Primitively Recursive Functions,'' describes how to specify functions
   105 using @{command primrec}. (A separate tutorial @{cite "isabelle-function"}
   106 describes the more powerful \keyw{fun} and \keyw{function} commands.)
   107 
   108 \item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
   109 describes how to specify codatatypes using the @{command codatatype} command.
   110 
   111 \item Section \ref{sec:defining-primitively-corecursive-functions},
   112 ``Defining Primitively Corecursive Functions,'' describes how to specify
   113 functions using the @{command primcorec} and
   114 @{command primcorecursive} commands. (A separate tutorial
   115 @{cite "isabelle-corec"} describes the more powerful \keyw{corec} and
   116 \keyw{corecursive} commands.)
   117 
   118 \item Section \ref{sec:registering-bounded-natural-functors}, ``Registering
   119 Bounded Natural Functors,'' explains how to use the @{command bnf} command
   120 to register arbitrary type constructors as BNFs.
   121 
   122 \item Section
   123 \ref{sec:deriving-destructors-and-theorems-for-free-constructors},
   124 ``Deriving Destructors and Theorems for Free Constructors,'' explains how to
   125 use the command @{command free_constructors} to derive destructor constants
   126 and theorems for freely generated types, as performed internally by
   127 @{command datatype} and @{command codatatype}.
   128 
   129 %\item Section \ref{sec:using-the-standard-ml-interface}, ``Using the Standard
   130 %ML Interface,'' describes the package's programmatic interface.
   131 
   132 \item Section \ref{sec:selecting-plugins}, ``Selecting Plugins,'' is concerned
   133 with the package's interoperability with other Isabelle packages and tools, such
   134 as the code generator, Transfer, Lifting, and Quickcheck.
   135 
   136 \item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
   137 Limitations,'' concludes with known open issues.
   138 \end{itemize}
   139 
   140 \newbox\boxA
   141 \setbox\boxA=\hbox{\texttt{NOSPAM}}
   142 
   143 \newcommand\authoremaili{\texttt{jasmin.blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
   144 gmail.\allowbreak com}}
   145 
   146 Comments and bug reports concerning either the package or this tutorial should
   147 be directed to the second author at \authoremaili{} or to the
   148 \texttt{cl-isabelle-users} mailing list.
   149 \<close>
   150 
   151 
   152 section \<open>Defining Datatypes
   153   \label{sec:defining-datatypes}\<close>
   154 
   155 text \<open>
   156 Datatypes can be specified using the @{command datatype} command.
   157 \<close>
   158 
   159 
   160 subsection \<open>Introductory Examples
   161   \label{ssec:datatype-introductory-examples}\<close>
   162 
   163 text \<open>
   164 Datatypes are illustrated through concrete examples featuring different flavors
   165 of recursion. More examples can be found in the directory
   166 \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
   167 \<close>
   168 
   169 
   170 subsubsection \<open>Nonrecursive Types
   171   \label{sssec:datatype-nonrecursive-types}\<close>
   172 
   173 text \<open>
   174 Datatypes are introduced by specifying the desired names and argument types for
   175 their constructors. \emph{Enumeration} types are the simplest form of datatype.
   176 All their constructors are nullary:
   177 \<close>
   178 
   179     datatype trool = Truue | Faalse | Perhaaps
   180 
   181 text \<open>
   182 \noindent
   183 @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
   184 
   185 Polymorphic types are possible, such as the following option type, modeled after
   186 its homologue from the @{theory Option} theory:
   187 \<close>
   188 
   189 (*<*)
   190     hide_const None Some map_option
   191     hide_type option
   192 (*>*)
   193     datatype 'a option = None | Some 'a
   194 
   195 text \<open>
   196 \noindent
   197 The constructors are @{text "None :: 'a option"} and
   198 @{text "Some :: 'a \<Rightarrow> 'a option"}.
   199 
   200 The next example has three type parameters:
   201 \<close>
   202 
   203     datatype ('a, 'b, 'c) triple = Triple 'a 'b 'c
   204 
   205 text \<open>
   206 \noindent
   207 The constructor is
   208 @{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
   209 Unlike in Standard ML, curried constructors are supported. The uncurried variant
   210 is also possible:
   211 \<close>
   212 
   213     datatype ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
   214 
   215 text \<open>
   216 \noindent
   217 Occurrences of nonatomic types on the right-hand side of the equal sign must be
   218 enclosed in double quotes, as is customary in Isabelle.
   219 \<close>
   220 
   221 
   222 subsubsection \<open>Simple Recursion
   223   \label{sssec:datatype-simple-recursion}\<close>
   224 
   225 text \<open>
   226 Natural numbers are the simplest example of a recursive type:
   227 \<close>
   228 
   229     datatype nat = Zero | Succ nat
   230 
   231 text \<open>
   232 \noindent
   233 Lists were shown in the introduction. Terminated lists are a variant that
   234 stores a value of type @{typ 'b} at the very end:
   235 \<close>
   236 
   237     datatype (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
   238 
   239 
   240 subsubsection \<open>Mutual Recursion
   241   \label{sssec:datatype-mutual-recursion}\<close>
   242 
   243 text \<open>
   244 \emph{Mutually recursive} types are introduced simultaneously and may refer to
   245 each other. The example below introduces a pair of types for even and odd
   246 natural numbers:
   247 \<close>
   248 
   249     datatype even_nat = Even_Zero | Even_Succ odd_nat
   250     and odd_nat = Odd_Succ even_nat
   251 
   252 text \<open>
   253 \noindent
   254 Arithmetic expressions are defined via terms, terms via factors, and factors via
   255 expressions:
   256 \<close>
   257 
   258     datatype ('a, 'b) exp =
   259       Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
   260     and ('a, 'b) trm =
   261       Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
   262     and ('a, 'b) fct =
   263       Const 'a | Var 'b | Expr "('a, 'b) exp"
   264 
   265 
   266 subsubsection \<open>Nested Recursion
   267   \label{sssec:datatype-nested-recursion}\<close>
   268 
   269 text \<open>
   270 \emph{Nested recursion} occurs when recursive occurrences of a type appear under
   271 a type constructor. The introduction showed some examples of trees with nesting
   272 through lists. A more complex example, that reuses our @{type option} type,
   273 follows:
   274 \<close>
   275 
   276     datatype 'a btree =
   277       BNode 'a "'a btree option" "'a btree option"
   278 
   279 text \<open>
   280 \noindent
   281 Not all nestings are admissible. For example, this command will fail:
   282 \<close>
   283 
   284     datatype 'a wrong = W1 | W2 (*<*)'a
   285     typ (*>*)"'a wrong \<Rightarrow> 'a"
   286 
   287 text \<open>
   288 \noindent
   289 The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
   290 only through its right-hand side. This issue is inherited by polymorphic
   291 datatypes defined in terms of~@{text "\<Rightarrow>"}:
   292 \<close>
   293 
   294     datatype ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
   295     datatype 'a also_wrong = W1 | W2 (*<*)'a
   296     typ (*>*)"('a also_wrong, 'a) fun_copy"
   297 
   298 text \<open>
   299 \noindent
   300 The following definition of @{typ 'a}-branching trees is legal:
   301 \<close>
   302 
   303     datatype 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
   304 
   305 text \<open>
   306 \noindent
   307 And so is the definition of hereditarily finite sets:
   308 \<close>
   309 
   310     datatype hfset = HFSet "hfset fset"
   311 
   312 text \<open>
   313 \noindent
   314 In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
   315 allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
   316 @{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
   317 type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
   318 @{typ "('a, 'b) fun_copy"}, the type variable @{typ 'a} is dead and
   319 @{typ 'b} is live.
   320 
   321 Type constructors must be registered as BNFs to have live arguments. This is
   322 done automatically for datatypes and codatatypes introduced by the
   323 @{command datatype} and @{command codatatype} commands.
   324 Section~\ref{sec:registering-bounded-natural-functors} explains how to
   325 register arbitrary type constructors as BNFs.
   326 
   327 Here is another example that fails:
   328 \<close>
   329 
   330     datatype 'a pow_list = PNil 'a (*<*)'a
   331     datatype 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
   332 
   333 text \<open>
   334 \noindent
   335 This attempted definition features a different flavor of nesting, where the
   336 recursive call in the type specification occurs around (rather than inside)
   337 another type constructor.
   338 \<close>
   339 
   340 
   341 subsubsection \<open>Auxiliary Constants
   342   \label{sssec:datatype-auxiliary-constants}\<close>
   343 
   344 text \<open>
   345 The @{command datatype} command introduces various constants in addition to
   346 the constructors. With each datatype are associated set functions, a map
   347 function, a predicator, a relator, discriminators, and selectors, all of which can be given
   348 custom names. In the example below, the familiar names @{text null}, @{text hd},
   349 @{text tl}, @{text set}, @{text map}, and @{text list_all2} override the
   350 default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
   351 @{text set_list}, @{text map_list}, and @{text rel_list}:
   352 \<close>
   353 
   354 (*<*)
   355     no_translations
   356       "[x, xs]" == "x # [xs]"
   357       "[x]" == "x # []"
   358 
   359     no_notation
   360       Nil ("[]") and
   361       Cons (infixr "#" 65)
   362 
   363     hide_type list
   364     hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list list_all
   365 
   366     context early
   367     begin
   368 (*>*)
   369     datatype (set: 'a) list =
   370       null: Nil
   371     | Cons (hd: 'a) (tl: "'a list")
   372     for
   373       map: map
   374       rel: list_all2
   375       pred: list_all
   376     where
   377       "tl Nil = Nil"
   378 
   379 text \<open>
   380 \noindent
   381 The types of the constants that appear in the specification are listed below.
   382 
   383 \medskip
   384 
   385 \begin{tabular}{@ {}ll@ {}}
   386 Constructors: &
   387   @{text "Nil :: 'a list"} \\
   388 &
   389   @{text "Cons :: 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\
   390 Discriminator: &
   391   @{text "null :: 'a list \<Rightarrow> bool"} \\
   392 Selectors: &
   393   @{text "hd :: 'a list \<Rightarrow> 'a"} \\
   394 &
   395   @{text "tl :: 'a list \<Rightarrow> 'a list"} \\
   396 Set function: &
   397   @{text "set :: 'a list \<Rightarrow> 'a set"} \\
   398 Map function: &
   399   @{text "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
   400 Relator: &
   401   @{text "list_all2 :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"}
   402 \end{tabular}
   403 
   404 \medskip
   405 
   406 The discriminator @{const null} and the selectors @{const hd} and @{const tl}
   407 are characterized by the following conditional equations:
   408 %
   409 \[@{thm list.collapse(1)[of xs, no_vars]}
   410   \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
   411 %
   412 For two-constructor datatypes, a single discriminator constant is sufficient.
   413 The discriminator associated with @{const Cons} is simply
   414 @{term "\<lambda>xs. \<not> null xs"}.
   415 
   416 The \keyw{where} clause at the end of the command specifies a default value for
   417 selectors applied to constructors on which they are not a priori specified.
   418 In the example, it is used to ensure that the tail of the empty list is itself
   419 (instead of being left unspecified).
   420 
   421 Because @{const Nil} is nullary, it is also possible to use
   422 @{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
   423 if we omit the identifier @{const null} and the associated colon. Some users
   424 argue against this, because the mixture of constructors and selectors in the
   425 characteristic theorems can lead Isabelle's automation to switch between the
   426 constructor and the destructor view in surprising ways.
   427 
   428 The usual mixfix syntax annotations are available for both types and
   429 constructors. For example:
   430 \<close>
   431 
   432 (*<*)
   433     end
   434 (*>*)
   435     datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
   436 
   437 text \<open>\blankline\<close>
   438 
   439     datatype (set: 'a) list =
   440       null: Nil ("[]")
   441     | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
   442     for
   443       map: map
   444       rel: list_all2
   445       pred: list_all
   446 
   447 text \<open>
   448 \noindent
   449 Incidentally, this is how the traditional syntax can be set up:
   450 \<close>
   451 
   452     syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
   453 
   454 text \<open>\blankline\<close>
   455 
   456     translations
   457       "[x, xs]" == "x # [xs]"
   458       "[x]" == "x # []"
   459 
   460 
   461 subsection \<open>Command Syntax
   462   \label{ssec:datatype-command-syntax}\<close>
   463 
   464 subsubsection \<open>\keyw{datatype}
   465   \label{sssec:datatype}\<close>
   466 
   467 text \<open>
   468 \begin{matharray}{rcl}
   469   @{command_def "datatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
   470 \end{matharray}
   471 
   472 @{rail \<open>
   473   @@{command datatype} target? @{syntax dt_options}? @{syntax dt_spec}
   474   ;
   475   @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels') + ',') ')'
   476   ;
   477   @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +)
   478   ;
   479   @{syntax_def dt_spec}: (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
   480      @{syntax map_rel_pred}? (@'where' (prop + '|'))? + @'and')
   481   ;
   482   @{syntax_def map_rel_pred}: @'for' ((('map' | 'rel' | 'pred') ':' name) +)
   483 \<close>}
   484 
   485 \medskip
   486 
   487 \noindent
   488 The @{command datatype} command introduces a set of mutually recursive
   489 datatypes specified by their constructors.
   490 
   491 The syntactic entity \synt{target} can be used to specify a local
   492 context (e.g., @{text "(in linorder)"} @{cite "isabelle-isar-ref"}),
   493 and \synt{prop} denotes a HOL proposition.
   494 
   495 The optional target is optionally followed by a combination of the following
   496 options:
   497 
   498 \begin{itemize}
   499 \setlength{\itemsep}{0pt}
   500 
   501 \item
   502 The @{text plugins} option indicates which plugins should be enabled
   503 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
   504 
   505 \item
   506 The @{text "discs_sels"} option indicates that discriminators and selectors
   507 should be generated. The option is implicitly enabled if names are specified for
   508 discriminators or selectors.
   509 \end{itemize}
   510 
   511 The optional \keyw{where} clause specifies default values for selectors.
   512 Each proposition must be an equation of the form
   513 @{text "un_D (C \<dots>) = \<dots>"}, where @{text C} is a constructor and
   514 @{text un_D} is a selector.
   515 
   516 The left-hand sides of the datatype equations specify the name of the type to
   517 define, its type parameters, and additional information:
   518 
   519 @{rail \<open>
   520   @{syntax_def dt_name}: @{syntax tyargs}? name mixfix?
   521   ;
   522   @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')'
   523 \<close>}
   524 
   525 \medskip
   526 
   527 \noindent
   528 The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
   529 the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
   530 variable (@{typ 'a}, @{typ 'b}, \ldots) @{cite "isabelle-isar-ref"}.
   531 
   532 The optional names preceding the type variables allow to override the default
   533 names of the set functions (@{text set\<^sub>1_t}, \ldots, @{text set\<^sub>m_t}). Type
   534 arguments can be marked as dead by entering @{text dead} in front of the
   535 type variable (e.g., @{text "(dead 'a)"}); otherwise, they are live or dead
   536 (and a set function is generated or not) depending on where they occur in the
   537 right-hand sides of the definition. Declaring a type argument as dead can speed
   538 up the type definition but will prevent any later (co)recursion through that
   539 type argument.
   540 
   541 Inside a mutually recursive specification, all defined datatypes must
   542 mention exactly the same type variables in the same order.
   543 
   544 @{rail \<open>
   545   @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) mixfix?
   546 \<close>}
   547 
   548 \medskip
   549 
   550 \noindent
   551 The main constituents of a constructor specification are the name of the
   552 constructor and the list of its argument types. An optional discriminator name
   553 can be supplied at the front. If discriminators are enabled (cf.\ the
   554 @{text "discs_sels"} option) but no name is supplied, the default is
   555 @{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
   556 @{text t.is_C\<^sub>j} otherwise.
   557 
   558 @{rail \<open>
   559   @{syntax_def dt_ctor_arg}: type | '(' name ':' type ')'
   560 \<close>}
   561 
   562 \medskip
   563 
   564 \noindent
   565 The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
   566 
   567 In addition to the type of a constructor argument, it is possible to specify a
   568 name for the corresponding selector. The same selector name can be reused for
   569 arguments to several constructors as long as the arguments share the same type.
   570 If selectors are enabled (cf.\ the @{text "discs_sels"} option) but no name is
   571 supplied, the default name is @{text un_C\<^sub>ji}.
   572 \<close>
   573 
   574 
   575 subsubsection \<open>\keyw{datatype_compat}
   576   \label{sssec:datatype-compat}\<close>
   577 
   578 text \<open>
   579 \begin{matharray}{rcl}
   580   @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
   581 \end{matharray}
   582 
   583 @{rail \<open>
   584   @@{command datatype_compat} (name +)
   585 \<close>}
   586 
   587 \medskip
   588 
   589 \noindent
   590 The @{command datatype_compat} command registers new-style datatypes as
   591 old-style datatypes and invokes the old-style plugins. For example:
   592 \<close>
   593 
   594     datatype_compat even_nat odd_nat
   595 
   596 text \<open>\blankline\<close>
   597 
   598     ML \<open>Old_Datatype_Data.get_info @{theory} @{type_name even_nat}\<close>
   599 
   600 text \<open>
   601 The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
   602 
   603 The command is sometimes useful when migrating from the old datatype package to
   604 the new one.
   605 
   606 A few remarks concern nested recursive datatypes:
   607 
   608 \begin{itemize}
   609 \setlength{\itemsep}{0pt}
   610 
   611 \item The old-style, nested-as-mutual induction rule and recursor theorems are
   612 generated under their usual names but with ``@{text "compat_"}'' prefixed
   613 (e.g., @{text compat_tree.induct}, @{text compat_tree.inducts}, and
   614 @{text compat_tree.rec}). These theorems should be identical to the ones
   615 generated by the old datatype package, \emph{up to the order of the
   616 premises}---meaning that the subgoals generated by the @{text induct} or
   617 @{text induction} method may be in a different order than before.
   618 
   619 \item All types through which recursion takes place must be new-style datatypes
   620 or the function type.
   621 \end{itemize}
   622 \<close>
   623 
   624 
   625 subsection \<open>Generated Constants
   626   \label{ssec:datatype-generated-constants}\<close>
   627 
   628 text \<open>
   629 Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ live type variables
   630 and $n$ constructors @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the following
   631 auxiliary constants are introduced:
   632 
   633 \medskip
   634 
   635 \begin{tabular}{@ {}ll@ {}}
   636 Case combinator: &
   637   @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
   638 Discriminators: &
   639   @{text t.is_C\<^sub>1}$, \ldots, $@{text t.is_C\<^sub>n} \\
   640 Selectors: &
   641   @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
   642 & \quad\vdots \\
   643 & @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
   644 Set functions: &
   645   @{text t.set\<^sub>1_t}, \ldots, @{text t.set\<^sub>m_t} \\
   646 Map function: &
   647   @{text t.map_t} \\
   648 Relator: &
   649   @{text t.rel_t} \\
   650 Recursor: &
   651   @{text t.rec_t}
   652 \end{tabular}
   653 
   654 \medskip
   655 
   656 \noindent
   657 The discriminators and selectors are generated only if the @{text "discs_sels"}
   658 option is enabled or if names are specified for discriminators or selectors.
   659 The set functions, map function, predicator, and relator are generated only if $m > 0$.
   660 
   661 In addition, some of the plugins introduce their own constants
   662 (Section~\ref{sec:selecting-plugins}). The case combinator, discriminators,
   663 and selectors are collectively called \emph{destructors}. The prefix
   664 ``@{text "t."}'' is an optional component of the names and is normally hidden.
   665 \<close>
   666 
   667 
   668 subsection \<open>Generated Theorems
   669   \label{ssec:datatype-generated-theorems}\<close>
   670 
   671 text \<open>
   672 The characteristic theorems generated by @{command datatype} are grouped in
   673 three broad categories:
   674 
   675 \begin{itemize}
   676 \setlength{\itemsep}{0pt}
   677 
   678 \item The \emph{free constructor theorems}
   679 (Section~\ref{sssec:free-constructor-theorems}) are properties of the
   680 constructors and destructors that can be derived for any freely generated type.
   681 Internally, the derivation is performed by @{command free_constructors}.
   682 
   683 \item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
   684 are properties of datatypes related to their BNF nature.
   685 
   686 \item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
   687 are properties of datatypes related to their inductive nature.
   688 
   689 \end{itemize}
   690 
   691 \noindent
   692 The full list of named theorems can be obtained by issuing the command
   693 \keyw{print_theorems} immediately after the datatype definition. This list
   694 includes theorems produced by plugins (Section~\ref{sec:selecting-plugins}),
   695 but normally excludes low-level theorems that reveal internal constructions.
   696 To make these accessible, add the line
   697 \<close>
   698 
   699     declare [[bnf_internals]]
   700 (*<*)
   701     declare [[bnf_internals = false]]
   702 (*>*)
   703 
   704 
   705 subsubsection \<open>Free Constructor Theorems
   706   \label{sssec:free-constructor-theorems}\<close>
   707 
   708 (*<*)
   709     consts nonnull :: 'a
   710 (*>*)
   711 
   712 text \<open>
   713 The free constructor theorems are partitioned in three subgroups. The first
   714 subgroup of properties is concerned with the constructors. They are listed below
   715 for @{typ "'a list"}:
   716 
   717 \begin{indentblock}
   718 \begin{description}
   719 
   720 \item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
   721 @{thm list.inject[no_vars]}
   722 
   723 \item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
   724 @{thm list.distinct(1)[no_vars]} \\
   725 @{thm list.distinct(2)[no_vars]}
   726 
   727 \item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
   728 @{thm list.exhaust[no_vars]}
   729 
   730 \item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
   731 @{thm list.nchotomy[no_vars]}
   732 
   733 \end{description}
   734 \end{indentblock}
   735 
   736 \noindent
   737 In addition, these nameless theorems are registered as safe elimination rules:
   738 
   739 \begin{indentblock}
   740 \begin{description}
   741 
   742 \item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
   743 @{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
   744 @{thm list.distinct(2)[THEN notE, elim!, no_vars]}
   745 
   746 \end{description}
   747 \end{indentblock}
   748 
   749 \noindent
   750 The next subgroup is concerned with the case combinator:
   751 
   752 \begin{indentblock}
   753 \begin{description}
   754 
   755 \item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
   756 @{thm list.case(1)[no_vars]} \\
   757 @{thm list.case(2)[no_vars]} \\
   758 The @{text "[code]"} attribute is set by the @{text code} plugin
   759 (Section~\ref{ssec:code-generator}).
   760 
   761 \item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
   762 @{thm list.case_cong[no_vars]}
   763 
   764 \item[@{text "t."}\hthm{case_cong_weak} @{text "[cong]"}\rm:] ~ \\
   765 @{thm list.case_cong_weak[no_vars]}
   766 
   767 \item[@{text "t."}\hthm{case_distrib}\rm:] ~ \\
   768 @{thm list.case_distrib[no_vars]}
   769 
   770 \item[@{text "t."}\hthm{split}\rm:] ~ \\
   771 @{thm list.split[no_vars]}
   772 
   773 \item[@{text "t."}\hthm{split_asm}\rm:] ~ \\
   774 @{thm list.split_asm[no_vars]}
   775 
   776 \item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
   777 
   778 \end{description}
   779 \end{indentblock}
   780 
   781 \noindent
   782 The third subgroup revolves around discriminators and selectors:
   783 
   784 \begin{indentblock}
   785 \begin{description}
   786 
   787 \item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
   788 @{thm list.disc(1)[no_vars]} \\
   789 @{thm list.disc(2)[no_vars]}
   790 
   791 \item[@{text "t."}\hthm{discI}\rm:] ~ \\
   792 @{thm list.discI(1)[no_vars]} \\
   793 @{thm list.discI(2)[no_vars]}
   794 
   795 \item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
   796 @{thm list.sel(1)[no_vars]} \\
   797 @{thm list.sel(2)[no_vars]} \\
   798 The @{text "[code]"} attribute is set by the @{text code} plugin
   799 (Section~\ref{ssec:code-generator}).
   800 
   801 \item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
   802 @{thm list.collapse(1)[no_vars]} \\
   803 @{thm list.collapse(2)[no_vars]} \\
   804 The @{text "[simp]"} attribute is exceptionally omitted for datatypes equipped
   805 with a single nullary constructor, because a property of the form
   806 @{prop "x = C"} is not suitable as a simplification rule.
   807 
   808 \item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
   809 These properties are missing for @{typ "'a list"} because there is only one
   810 proper discriminator. If the datatype had been introduced with a second
   811 discriminator called @{const nonnull}, they would have read as follows: \\[\jot]
   812 @{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
   813 @{prop "nonnull list \<Longrightarrow> \<not> null list"}
   814 
   815 \item[@{text "t."}\hthm{exhaust_disc} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
   816 @{thm list.exhaust_disc[no_vars]}
   817 
   818 \item[@{text "t."}\hthm{exhaust_sel} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
   819 @{thm list.exhaust_sel[no_vars]}
   820 
   821 \item[@{text "t."}\hthm{expand}\rm:] ~ \\
   822 @{thm list.expand[no_vars]}
   823 
   824 \item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
   825 @{thm list.split_sel[no_vars]}
   826 
   827 \item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
   828 @{thm list.split_sel_asm[no_vars]}
   829 
   830 \item[@{text "t."}\hthm{split_sels} = @{text "split_sel split_sel_asm"}]
   831 
   832 \item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
   833 @{thm list.case_eq_if[no_vars]}
   834 
   835 \item[@{text "t."}\hthm{disc_eq_case}\rm:] ~ \\
   836 @{thm list.disc_eq_case(1)[no_vars]} \\
   837 @{thm list.disc_eq_case(2)[no_vars]}
   838 
   839 \end{description}
   840 \end{indentblock}
   841 
   842 \noindent
   843 In addition, equational versions of @{text t.disc} are registered with the
   844 @{text "[code]"} attribute. The @{text "[code]"} attribute is set by the
   845 @{text code} plugin (Section~\ref{ssec:code-generator}).
   846 \<close>
   847 
   848 
   849 subsubsection \<open>Functorial Theorems
   850   \label{sssec:functorial-theorems}\<close>
   851 
   852 text \<open>
   853 The functorial theorems are generated for type constructors with at least
   854 one live type argument (e.g., @{typ "'a list"}). They are partitioned in two
   855 subgroups. The first subgroup consists of properties involving the
   856 constructors or the destructors and either a set function, the map function,
   857 the predicator, or the relator:
   858 
   859 \begin{indentblock}
   860 \begin{description}
   861 
   862 \item[@{text "t."}\hthm{case_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
   863 @{thm list.case_transfer[no_vars]} \\
   864 This property is generated by the @{text transfer} plugin
   865 (Section~\ref{ssec:transfer}).
   866 %The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
   867 %(Section~\ref{ssec:transfer}).
   868 
   869 \item[@{text "t."}\hthm{sel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
   870 This property is missing for @{typ "'a list"} because there is no common
   871 selector to all constructors. \\
   872 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
   873 (Section~\ref{ssec:transfer}).
   874 
   875 \item[@{text "t."}\hthm{ctr_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
   876 @{thm list.ctr_transfer(1)[no_vars]} \\
   877 @{thm list.ctr_transfer(2)[no_vars]} \\
   878 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
   879 (Section~\ref{ssec:transfer}) .
   880 
   881 \item[@{text "t."}\hthm{disc_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
   882 @{thm list.disc_transfer(1)[no_vars]} \\
   883 @{thm list.disc_transfer(2)[no_vars]} \\
   884 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
   885 (Section~\ref{ssec:transfer}).
   886 
   887 \item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
   888 @{thm list.set(1)[no_vars]} \\
   889 @{thm list.set(2)[no_vars]} \\
   890 The @{text "[code]"} attribute is set by the @{text code} plugin
   891 (Section~\ref{ssec:code-generator}).
   892 
   893 \item[@{text "t."}\hthm{set_cases} @{text "[consumes 1, cases set: set\<^sub>i_t]"}\rm:] ~ \\
   894 @{thm list.set_cases[no_vars]}
   895 
   896 \item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
   897 @{thm list.set_intros(1)[no_vars]} \\
   898 @{thm list.set_intros(2)[no_vars]}
   899 
   900 \item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
   901 @{thm list.set_sel[no_vars]}
   902 
   903 \item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
   904 @{thm list.map(1)[no_vars]} \\
   905 @{thm list.map(2)[no_vars]} \\
   906 The @{text "[code]"} attribute is set by the @{text code} plugin
   907 (Section~\ref{ssec:code-generator}).
   908 
   909 \item[@{text "t."}\hthm{map_disc_iff} @{text "[simp]"}\rm:] ~ \\
   910 @{thm list.map_disc_iff[no_vars]}
   911 
   912 \item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
   913 @{thm list.map_sel[no_vars]}
   914 
   915 \item[@{text "t."}\hthm{pred_inject} @{text "[simp]"}\rm:] ~ \\
   916 @{thm list.pred_inject(1)[no_vars]} \\
   917 @{thm list.pred_inject(2)[no_vars]}
   918 
   919 \item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
   920 @{thm list.rel_inject(1)[no_vars]} \\
   921 @{thm list.rel_inject(2)[no_vars]}
   922 
   923 \item[@{text "t."}\hthm{rel_distinct} @{text "[simp]"}\rm:] ~ \\
   924 @{thm list.rel_distinct(1)[no_vars]} \\
   925 @{thm list.rel_distinct(2)[no_vars]}
   926 
   927 \item[@{text "t."}\hthm{rel_intros}\rm:] ~ \\
   928 @{thm list.rel_intros(1)[no_vars]} \\
   929 @{thm list.rel_intros(2)[no_vars]}
   930 
   931 \item[@{text "t."}\hthm{rel_cases} @{text "[consumes 1, case_names t\<^sub>1 \<dots> t\<^sub>m, cases pred]"}\rm:] ~ \\
   932 @{thm list.rel_cases[no_vars]}
   933 
   934 \item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
   935 @{thm list.rel_sel[no_vars]}
   936 
   937 \end{description}
   938 \end{indentblock}
   939 
   940 \noindent
   941 In addition, equational versions of @{text t.rel_inject} and @{text
   942 rel_distinct} are registered with the @{text "[code]"} attribute. The
   943 @{text "[code]"} attribute is set by the @{text code} plugin
   944 (Section~\ref{ssec:code-generator}).
   945 
   946 The second subgroup consists of more abstract properties of the set functions,
   947 the map function, the predicator, and the relator:
   948 
   949 \begin{indentblock}
   950 \begin{description}
   951 
   952 \item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
   953 @{thm list.inj_map[no_vars]}
   954 
   955 \item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\
   956 @{thm list.inj_map_strong[no_vars]}
   957 
   958 \item[@{text "t."}\hthm{map_comp}\rm:] ~ \\
   959 @{thm list.map_comp[no_vars]}
   960 
   961 \item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
   962 @{thm list.map_cong0[no_vars]}
   963 
   964 \item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
   965 @{thm list.map_cong[no_vars]}
   966 
   967 \item[@{text "t."}\hthm{map_cong_pred}\rm:] ~ \\
   968 @{thm list.map_cong_pred[no_vars]}
   969 
   970 \item[@{text "t."}\hthm{map_cong_simp}\rm:] ~ \\
   971 @{thm list.map_cong_simp[no_vars]}
   972 
   973 \item[@{text "t."}\hthm{map_id0}\rm:] ~ \\
   974 @{thm list.map_id0[no_vars]}
   975 
   976 \item[@{text "t."}\hthm{map_id}\rm:] ~ \\
   977 @{thm list.map_id[no_vars]}
   978 
   979 \item[@{text "t."}\hthm{map_ident}\rm:] ~ \\
   980 @{thm list.map_ident[no_vars]}
   981 
   982 \item[@{text "t."}\hthm{map_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
   983 @{thm list.map_transfer[no_vars]} \\
   984 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
   985 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
   986 
   987 \item[@{text "t."}\hthm{pred_cong} @{text "[fundef_cong]"}\rm:] ~ \\
   988 @{thm list.pred_cong[no_vars]}
   989 
   990 \item[@{text "t."}\hthm{pred_cong_simp}\rm:] ~ \\
   991 @{thm list.pred_cong_simp[no_vars]}
   992 
   993 \item[@{text "t."}\hthm{pred_map}\rm:] ~ \\
   994 @{thm list.pred_map[no_vars]}
   995 
   996 \item[@{text "t."}\hthm{pred_mono_strong}\rm:] ~ \\
   997 @{thm list.pred_mono_strong[no_vars]}
   998 
   999 \item[@{text "t."}\hthm{pred_rel}\rm:] ~ \\
  1000 @{thm list.pred_rel[no_vars]}
  1001 
  1002 \item[@{text "t."}\hthm{pred_set}\rm:] ~ \\
  1003 @{thm list.pred_set[no_vars]}
  1004 
  1005 \item[@{text "t."}\hthm{pred_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
  1006 @{thm list.pred_transfer[no_vars]} \\
  1007 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
  1008 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
  1009 
  1010 \item[@{text "t."}\hthm{pred_True}\rm:] ~ \\
  1011 @{thm list.pred_True[no_vars]}
  1012 
  1013 \item[@{text "t."}\hthm{set_map}\rm:] ~ \\
  1014 @{thm list.set_map[no_vars]}
  1015 
  1016 \item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
  1017 @{thm list.set_transfer[no_vars]} \\
  1018 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
  1019 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
  1020 
  1021 \item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
  1022 @{thm list.rel_compp[no_vars]} \\
  1023 The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin
  1024 (Section~\ref{ssec:lifting}).
  1025 
  1026 \item[@{text "t."}\hthm{rel_conversep}\rm:] ~ \\
  1027 @{thm list.rel_conversep[no_vars]}
  1028 
  1029 \item[@{text "t."}\hthm{rel_eq}\rm:] ~ \\
  1030 @{thm list.rel_eq[no_vars]}
  1031 
  1032 \item[@{text "t."}\hthm{rel_eq_onp}\rm:] ~ \\
  1033 @{thm list.rel_eq_onp[no_vars]}
  1034 
  1035 \item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
  1036 @{thm list.rel_flip[no_vars]}
  1037 
  1038 \item[@{text "t."}\hthm{rel_map}\rm:] ~ \\
  1039 @{thm list.rel_map(1)[no_vars]} \\
  1040 @{thm list.rel_map(2)[no_vars]}
  1041 
  1042 \item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\
  1043 @{thm list.rel_mono[no_vars]} \\
  1044 The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin
  1045 (Section~\ref{ssec:lifting}).
  1046 
  1047 \item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\
  1048 @{thm list.rel_mono_strong[no_vars]}
  1049 
  1050 \item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\
  1051 @{thm list.rel_cong[no_vars]}
  1052 
  1053 \item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\
  1054 @{thm list.rel_cong_simp[no_vars]}
  1055 
  1056 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
  1057 @{thm list.rel_refl[no_vars]}
  1058 
  1059 \item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\
  1060 @{thm list.rel_refl_strong[no_vars]}
  1061 
  1062 \item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\
  1063 @{thm list.rel_reflp[no_vars]}
  1064 
  1065 \item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\
  1066 @{thm list.rel_symp[no_vars]}
  1067 
  1068 \item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\
  1069 @{thm list.rel_transp[no_vars]}
  1070 
  1071 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
  1072 @{thm list.rel_transfer[no_vars]} \\
  1073 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
  1074 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
  1075 
  1076 \end{description}
  1077 \end{indentblock}
  1078 \<close>
  1079 
  1080 
  1081 subsubsection \<open>Inductive Theorems
  1082   \label{sssec:inductive-theorems}\<close>
  1083 
  1084 text \<open>
  1085 The inductive theorems are as follows:
  1086 
  1087 \begin{indentblock}
  1088 \begin{description}
  1089 
  1090 \item[@{text "t."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct t]"}\rm:] ~ \\
  1091 @{thm list.induct[no_vars]}
  1092 
  1093 \item[@{text "t."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n, induct pred]"}\rm:] ~ \\
  1094 @{thm list.rel_induct[no_vars]}
  1095 
  1096 \item[\begin{tabular}{@ {}l@ {}}
  1097   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm: \\
  1098   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm: \\
  1099 \end{tabular}] ~ \\
  1100 Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
  1101 prove $m$ properties simultaneously.
  1102 
  1103 \item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
  1104 @{thm list.rec(1)[no_vars]} \\
  1105 @{thm list.rec(2)[no_vars]} \\
  1106 The @{text "[code]"} attribute is set by the @{text code} plugin
  1107 (Section~\ref{ssec:code-generator}).
  1108 
  1109 \item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
  1110 @{thm list.rec_o_map[no_vars]}
  1111 
  1112 \item[@{text "t."}\hthm{rec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
  1113 @{thm list.rec_transfer[no_vars]} \\
  1114 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
  1115 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
  1116 
  1117 \end{description}
  1118 \end{indentblock}
  1119 
  1120 \noindent
  1121 For convenience, @{command datatype} also provides the following collection:
  1122 
  1123 \begin{indentblock}
  1124 \begin{description}
  1125 
  1126 \item[@{text "t."}\hthm{simps}] = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject} \\
  1127 @{text t.rel_distinct} @{text t.set}
  1128 
  1129 \end{description}
  1130 \end{indentblock}
  1131 \<close>
  1132 
  1133 
  1134 subsection \<open>Proof Method
  1135   \label{ssec:datatype-proof-method}\<close>
  1136 
  1137 subsubsection \<open>\textit{countable_datatype}
  1138   \label{sssec:datatype-compat}\<close>
  1139 
  1140 text \<open>
  1141 The theory \<^file>\<open>~~/src/HOL/Library/Countable.thy\<close> provides a
  1142 proof method called @{method countable_datatype} that can be used to prove the
  1143 countability of many datatypes, building on the countability of the types
  1144 appearing in their definitions and of any type arguments. For example:
  1145 \<close>
  1146 
  1147     instance list :: (countable) countable
  1148       by countable_datatype
  1149 
  1150 
  1151 subsection \<open>Compatibility Issues
  1152   \label{ssec:datatype-compatibility-issues}\<close>
  1153 
  1154 text \<open>
  1155 The command @{command datatype} has been designed to be highly compatible with
  1156 the old command, to ease migration. There are nonetheless a few
  1157 incompatibilities that may arise when porting:
  1158 
  1159 \begin{itemize}
  1160 \setlength{\itemsep}{0pt}
  1161 
  1162 \item \emph{The Standard ML interfaces are different.} Tools and extensions
  1163 written to call the old ML interfaces will need to be adapted to the new
  1164 interfaces. The @{text BNF_LFP_Compat} structure provides convenience functions
  1165 that simulate the old interfaces in terms of the new ones.
  1166 
  1167 \item \emph{The recursor @{text rec_t} has a different signature for nested
  1168 recursive datatypes.} In the old package, nested recursion through non-functions
  1169 was internally reduced to mutual recursion. This reduction was visible in the
  1170 type of the recursor, used by \keyw{primrec}. Recursion through functions was
  1171 handled specially. In the new package, nested recursion (for functions and
  1172 non-functions) is handled in a more modular fashion. The old-style recursor can
  1173 be generated on demand using @{command primrec} if the recursion is via
  1174 new-style datatypes, as explained in
  1175 Section~\ref{sssec:primrec-nested-as-mutual-recursion}, or using
  1176 @{command datatype_compat}.
  1177 
  1178 \item \emph{Accordingly, the induction rule is different for nested recursive
  1179 datatypes.} Again, the old-style induction rule can be generated on demand
  1180 using @{command primrec} if the recursion is via new-style datatypes, as
  1181 explained in Section~\ref{sssec:primrec-nested-as-mutual-recursion}, or using
  1182 @{command datatype_compat}. For recursion through functions, the old-style
  1183 induction rule can be obtained by applying the @{text "[unfolded
  1184 all_mem_range]"} attribute on @{text t.induct}.
  1185 
  1186 \item \emph{The @{const size} function has a slightly different definition.}
  1187 The new function returns @{text 1} instead of @{text 0} for some nonrecursive
  1188 constructors. This departure from the old behavior made it possible to implement
  1189 @{const size} in terms of the generic function @{text "t.size_t"}. Moreover,
  1190 the new function considers nested occurrences of a value, in the nested
  1191 recursive case. The old behavior can be obtained by disabling the @{text size}
  1192 plugin (Section~\ref{sec:selecting-plugins}) and instantiating the
  1193 @{text size} type class manually.
  1194 
  1195 \item \emph{The internal constructions are completely different.} Proof texts
  1196 that unfold the definition of constants introduced by the old command will
  1197 be difficult to port.
  1198 
  1199 \item \emph{Some constants and theorems have different names.}
  1200 For non-mutually recursive datatypes,
  1201 the alias @{text t.inducts} for @{text t.induct} is no longer generated.
  1202 For $m > 1$ mutually recursive datatypes,
  1203 @{text "rec_t\<^sub>1_\<dots>_t\<^sub>m_i"} has been renamed
  1204 @{text "rec_t\<^sub>i"} for each @{text "i \<in> {1, \<dots>, m}"},
  1205 @{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
  1206 @{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, m}"}, and the
  1207 collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} (generated by the
  1208 @{text size} plugin, Section~\ref{ssec:size}) has been divided into
  1209 @{text "t\<^sub>1.size"}, \ldots, @{text "t\<^sub>m.size"}.
  1210 
  1211 \item \emph{The @{text t.simps} collection has been extended.}
  1212 Previously available theorems are available at the same index as before.
  1213 
  1214 \item \emph{Variables in generated properties have different names.} This is
  1215 rarely an issue, except in proof texts that refer to variable names in the
  1216 @{text "[where \<dots>]"} attribute. The solution is to use the more robust
  1217 @{text "[of \<dots>]"} syntax.
  1218 \end{itemize}
  1219 
  1220 The old command is still available as \keyw{old_datatype} in theory
  1221 \<^file>\<open>~~/src/HOL/Library/Old_Datatype.thy\<close>. However, there is no general
  1222 way to register old-style datatypes as new-style datatypes. If the objective
  1223 is to define new-style datatypes with nested recursion through old-style
  1224 datatypes, the old-style datatypes can be registered as a BNF
  1225 (Section~\ref{sec:registering-bounded-natural-functors}). If the objective is
  1226 to derive discriminators and selectors, this can be achieved using
  1227 @{command free_constructors}
  1228 (Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
  1229 \<close>
  1230 
  1231 
  1232 section \<open>Defining Primitively Recursive Functions
  1233   \label{sec:defining-primitively-recursive-functions}\<close>
  1234 
  1235 text \<open>
  1236 Recursive functions over datatypes can be specified using the @{command primrec}
  1237 command, which supports primitive recursion, or using the more general
  1238 \keyw{fun}, \keyw{function}, and \keyw{partial_function} commands. In this
  1239 tutorial, the focus is on @{command primrec}; \keyw{fun} and \keyw{function} are
  1240 described in a separate tutorial @{cite "isabelle-function"}.
  1241 \<close>
  1242 
  1243 
  1244 subsection \<open>Introductory Examples
  1245   \label{ssec:primrec-introductory-examples}\<close>
  1246 
  1247 text \<open>
  1248 Primitive recursion is illustrated through concrete examples based on the
  1249 datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
  1250 examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
  1251 \<close>
  1252 
  1253 
  1254 subsubsection \<open>Nonrecursive Types
  1255   \label{sssec:primrec-nonrecursive-types}\<close>
  1256 
  1257 text \<open>
  1258 Primitive recursion removes one layer of constructors on the left-hand side in
  1259 each equation. For example:
  1260 \<close>
  1261 
  1262     primrec (nonexhaustive) bool_of_trool :: "trool \<Rightarrow> bool" where
  1263       "bool_of_trool Faalse \<longleftrightarrow> False"
  1264     | "bool_of_trool Truue \<longleftrightarrow> True"
  1265 
  1266 text \<open>\blankline\<close>
  1267 
  1268     primrec the_list :: "'a option \<Rightarrow> 'a list" where
  1269       "the_list None = []"
  1270     | "the_list (Some a) = [a]"
  1271 
  1272 text \<open>\blankline\<close>
  1273 
  1274     primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
  1275       "the_default d None = d"
  1276     | "the_default _ (Some a) = a"
  1277 
  1278 text \<open>\blankline\<close>
  1279 
  1280     primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
  1281       "mirrror (Triple a b c) = Triple c b a"
  1282 
  1283 text \<open>
  1284 \noindent
  1285 The equations can be specified in any order, and it is acceptable to leave out
  1286 some cases, which are then unspecified. Pattern matching on the left-hand side
  1287 is restricted to a single datatype, which must correspond to the same argument
  1288 in all equations.
  1289 \<close>
  1290 
  1291 
  1292 subsubsection \<open>Simple Recursion
  1293   \label{sssec:primrec-simple-recursion}\<close>
  1294 
  1295 text \<open>
  1296 For simple recursive types, recursive calls on a constructor argument are
  1297 allowed on the right-hand side:
  1298 \<close>
  1299 
  1300     primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
  1301       "replicate Zero _ = []"
  1302     | "replicate (Succ n) x = x # replicate n x"
  1303 
  1304 text \<open>\blankline\<close>
  1305 
  1306     primrec (nonexhaustive) at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
  1307       "at (x # xs) j =
  1308          (case j of
  1309             Zero \<Rightarrow> x
  1310           | Succ j' \<Rightarrow> at xs j')"
  1311 
  1312 text \<open>\blankline\<close>
  1313 
  1314     primrec (*<*)(in early) (transfer) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
  1315       "tfold _ (TNil y) = y"
  1316     | "tfold f (TCons x xs) = f x (tfold f xs)"
  1317 
  1318 text \<open>
  1319 \noindent
  1320 Pattern matching is only available for the argument on which the recursion takes
  1321 place. Fortunately, it is easy to generate pattern-maching equations using the
  1322 @{command simps_of_case} command provided by the theory
  1323 \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
  1324 \<close>
  1325 
  1326     simps_of_case at_simps_alt: at.simps
  1327 
  1328 text \<open>
  1329 This generates the lemma collection @{thm [source] at_simps_alt}:
  1330 %
  1331 \[@{thm at_simps_alt(1)[no_vars]}
  1332   \qquad @{thm at_simps_alt(2)[no_vars]}\]
  1333 %
  1334 The next example is defined using \keyw{fun} to escape the syntactic
  1335 restrictions imposed on primitively recursive functions:
  1336 \<close>
  1337 
  1338     fun at_least_two :: "nat \<Rightarrow> bool" where
  1339       "at_least_two (Succ (Succ _)) \<longleftrightarrow> True"
  1340     | "at_least_two _ \<longleftrightarrow> False"
  1341 
  1342 
  1343 subsubsection \<open>Mutual Recursion
  1344   \label{sssec:primrec-mutual-recursion}\<close>
  1345 
  1346 text \<open>
  1347 The syntax for mutually recursive functions over mutually recursive datatypes
  1348 is straightforward:
  1349 \<close>
  1350 
  1351     primrec
  1352       nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
  1353       nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
  1354     where
  1355       "nat_of_even_nat Even_Zero = Zero"
  1356     | "nat_of_even_nat (Even_Succ n) = Succ (nat_of_odd_nat n)"
  1357     | "nat_of_odd_nat (Odd_Succ n) = Succ (nat_of_even_nat n)"
  1358 
  1359 text \<open>\blankline\<close>
  1360 
  1361     primrec
  1362       eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
  1363       eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
  1364       eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
  1365     where
  1366       "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t"
  1367     | "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e"
  1368     | "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f"
  1369     | "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t"
  1370     | "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a"
  1371     | "eval\<^sub>f _ \<xi> (Var b) = \<xi> b"
  1372     | "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
  1373 
  1374 text \<open>
  1375 \noindent
  1376 Mutual recursion is possible within a single type, using \keyw{fun}:
  1377 \<close>
  1378 
  1379     fun
  1380       even :: "nat \<Rightarrow> bool" and
  1381       odd :: "nat \<Rightarrow> bool"
  1382     where
  1383       "even Zero = True"
  1384     | "even (Succ n) = odd n"
  1385     | "odd Zero = False"
  1386     | "odd (Succ n) = even n"
  1387 
  1388 
  1389 subsubsection \<open>Nested Recursion
  1390   \label{sssec:primrec-nested-recursion}\<close>
  1391 
  1392 text \<open>
  1393 In a departure from the old datatype package, nested recursion is normally
  1394 handled via the map functions of the nesting type constructors. For example,
  1395 recursive calls are lifted to lists using @{const map}:
  1396 \<close>
  1397 
  1398 (*<*)
  1399     datatype '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")
  1400 (*>*)
  1401     primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
  1402       "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
  1403          (case js of
  1404             [] \<Rightarrow> a
  1405           | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
  1406 
  1407 text \<open>
  1408 \noindent
  1409 The next example features recursion through the @{text option} type. Although
  1410 @{text option} is not a new-style datatype, it is registered as a BNF with the
  1411 map function @{const map_option}:
  1412 \<close>
  1413 
  1414     primrec (*<*)(in early) (*>*)sum_btree :: "('a::{zero,plus}) btree \<Rightarrow> 'a" where
  1415       "sum_btree (BNode a lt rt) =
  1416          a + the_default 0 (map_option sum_btree lt) +
  1417            the_default 0 (map_option sum_btree rt)"
  1418 
  1419 text \<open>
  1420 \noindent
  1421 The same principle applies for arbitrary type constructors through which
  1422 recursion is possible. Notably, the map function for the function type
  1423 (@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
  1424 \<close>
  1425 
  1426     primrec (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
  1427       "relabel_ft f (FTLeaf x) = FTLeaf (f x)"
  1428     | "relabel_ft f (FTNode g) = FTNode (relabel_ft f \<circ> g)"
  1429 
  1430 text \<open>
  1431 \noindent
  1432 For convenience, recursion through functions can also be expressed using
  1433 $\lambda$-abstractions and function application rather than through composition.
  1434 For example:
  1435 \<close>
  1436 
  1437     primrec relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
  1438       "relabel_ft f (FTLeaf x) = FTLeaf (f x)"
  1439     | "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
  1440 
  1441 text \<open>\blankline\<close>
  1442 
  1443     primrec (nonexhaustive) subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
  1444       "subtree_ft x (FTNode g) = g x"
  1445 
  1446 text \<open>
  1447 \noindent
  1448 For recursion through curried $n$-ary functions, $n$ applications of
  1449 @{term "op \<circ>"} are necessary. The examples below illustrate the case where
  1450 $n = 2$:
  1451 \<close>
  1452 
  1453     datatype 'a ftree2 = FTLeaf2 'a | FTNode2 "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2"
  1454 
  1455 text \<open>\blankline\<close>
  1456 
  1457     primrec (*<*)(in early) (*>*)relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
  1458       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
  1459     | "relabel_ft2 f (FTNode2 g) = FTNode2 (op \<circ> (op \<circ> (relabel_ft2 f)) g)"
  1460 
  1461 text \<open>\blankline\<close>
  1462 
  1463     primrec relabel_ft2 :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
  1464       "relabel_ft2 f (FTLeaf2 x) = FTLeaf2 (f x)"
  1465     | "relabel_ft2 f (FTNode2 g) = FTNode2 (\<lambda>x y. relabel_ft2 f (g x y))"
  1466 
  1467 text \<open>\blankline\<close>
  1468 
  1469     primrec (nonexhaustive) subtree_ft2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a ftree2 \<Rightarrow> 'a ftree2" where
  1470       "subtree_ft2 x y (FTNode2 g) = g x y"
  1471 
  1472 text \<open>
  1473 For any datatype featuring nesting, the predicator can be used instead of the
  1474 map function, typically when defining predicates. For example:
  1475 \<close>
  1476 
  1477     primrec increasing_tree :: "int \<Rightarrow> int tree\<^sub>f\<^sub>f \<Rightarrow> bool" where
  1478       "increasing_tree m (Node\<^sub>f\<^sub>f n ts) \<longleftrightarrow>
  1479        n \<ge> m \<and> list_all (increasing_tree (n + 1)) ts"
  1480 
  1481 
  1482 subsubsection \<open>Nested-as-Mutual Recursion
  1483   \label{sssec:primrec-nested-as-mutual-recursion}\<close>
  1484 
  1485 (*<*)
  1486     locale n2m
  1487     begin
  1488 (*>*)
  1489 
  1490 text \<open>
  1491 For compatibility with the old package, but also because it is sometimes
  1492 convenient in its own right, it is possible to treat nested recursive datatypes
  1493 as mutually recursive ones if the recursion takes place though new-style
  1494 datatypes. For example:
  1495 \<close>
  1496 
  1497     primrec (nonexhaustive)
  1498       at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" and
  1499       ats\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f list \<Rightarrow> nat \<Rightarrow> nat list \<Rightarrow> 'a"
  1500     where
  1501       "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
  1502          (case js of
  1503             [] \<Rightarrow> a
  1504           | j # js' \<Rightarrow> ats\<^sub>f\<^sub>f ts j js')"
  1505     | "ats\<^sub>f\<^sub>f (t # ts) j =
  1506          (case j of
  1507             Zero \<Rightarrow> at\<^sub>f\<^sub>f t
  1508           | Succ j' \<Rightarrow> ats\<^sub>f\<^sub>f ts j')"
  1509 
  1510 text \<open>
  1511 \noindent
  1512 Appropriate induction rules are generated as
  1513 @{thm [source] at\<^sub>f\<^sub>f.induct},
  1514 @{thm [source] ats\<^sub>f\<^sub>f.induct}, and
  1515 @{thm [source] at\<^sub>f\<^sub>f_ats\<^sub>f\<^sub>f.induct}. The
  1516 induction rules and the underlying recursors are generated dynamically
  1517 and are kept in a cache to speed up subsequent definitions.
  1518 
  1519 Here is a second example:
  1520 \<close>
  1521 
  1522     primrec
  1523       sum_btree :: "('a::{zero,plus}) btree \<Rightarrow> 'a" and
  1524       sum_btree_option :: "'a btree option \<Rightarrow> 'a"
  1525     where
  1526       "sum_btree (BNode a lt rt) =
  1527          a + sum_btree_option lt + sum_btree_option rt"
  1528     | "sum_btree_option None = 0"
  1529     | "sum_btree_option (Some t) = sum_btree t"
  1530 
  1531 text \<open>
  1532 %  * can pretend a nested type is mutually recursive (if purely inductive)
  1533 %  * avoids the higher-order map
  1534 %  * e.g.
  1535 
  1536 %  * this can always be avoided;
  1537 %     * e.g. in our previous example, we first mapped the recursive
  1538 %       calls, then we used a generic at function to retrieve the result
  1539 %
  1540 %  * there's no hard-and-fast rule of when to use one or the other,
  1541 %    just like there's no rule when to use fold and when to use
  1542 %    primrec
  1543 %
  1544 %  * higher-order approach, considering nesting as nesting, is more
  1545 %    compositional -- e.g. we saw how we could reuse an existing polymorphic
  1546 %    at or the_default, whereas @{const ats\<^sub>f\<^sub>f} is much more specific
  1547 %
  1548 %  * but:
  1549 %     * is perhaps less intuitive, because it requires higher-order thinking
  1550 %     * may seem inefficient, and indeed with the code generator the
  1551 %       mutually recursive version might be nicer
  1552 %     * is somewhat indirect -- must apply a map first, then compute a result
  1553 %       (cannot mix)
  1554 %     * the auxiliary functions like @{const ats\<^sub>f\<^sub>f} are sometimes useful in own right
  1555 %
  1556 %  * impact on automation unclear
  1557 %
  1558 \<close>
  1559 (*<*)
  1560     end
  1561 (*>*)
  1562 
  1563 
  1564 subsection \<open>Command Syntax
  1565   \label{ssec:primrec-command-syntax}\<close>
  1566 
  1567 subsubsection \<open>\keyw{primrec}
  1568   \label{sssec:primrec}\<close>
  1569 
  1570 text \<open>
  1571 \begin{matharray}{rcl}
  1572   @{command_def "primrec"} & : & @{text "local_theory \<rightarrow> local_theory"}
  1573 \end{matharray}
  1574 
  1575 @{rail \<open>
  1576   @@{command primrec} target? @{syntax pr_options}? fixes \<newline>
  1577   @'where' (@{syntax pr_equation} + '|')
  1578   ;
  1579   @{syntax_def pr_options}: '(' ((@{syntax plugins} | 'nonexhaustive' | 'transfer') + ',') ')'
  1580   ;
  1581   @{syntax_def pr_equation}: thmdecl? prop
  1582 \<close>}
  1583 
  1584 \medskip
  1585 
  1586 \noindent
  1587 The @{command primrec} command introduces a set of mutually recursive functions
  1588 over datatypes.
  1589 
  1590 The syntactic entity \synt{target} can be used to specify a local context,
  1591 \synt{fixes} denotes a list of names with optional type signatures,
  1592 \synt{thmdecl} denotes an optional name for the formula that follows, and
  1593 \synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
  1594 
  1595 The optional target is optionally followed by a combination of the following
  1596 options:
  1597 
  1598 \begin{itemize}
  1599 \setlength{\itemsep}{0pt}
  1600 
  1601 \item
  1602 The @{text plugins} option indicates which plugins should be enabled
  1603 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
  1604 
  1605 \item
  1606 The @{text nonexhaustive} option indicates that the functions are not
  1607 necessarily specified for all constructors. It can be used to suppress the
  1608 warning that is normally emitted when some constructors are missing.
  1609 
  1610 \item
  1611 The @{text transfer} option indicates that an unconditional transfer rule
  1612 should be generated and proved @{text "by transfer_prover"}. The
  1613 @{text "[transfer_rule]"} attribute is set on the generated theorem.
  1614 \end{itemize}
  1615 
  1616 %%% TODO: elaborate on format of the equations
  1617 %%% TODO: elaborate on mutual and nested-to-mutual
  1618 \<close>
  1619 
  1620 
  1621 subsection \<open>Generated Theorems
  1622   \label{ssec:primrec-generated-theorems}\<close>
  1623 
  1624 (*<*)
  1625     context early
  1626     begin
  1627 (*>*)
  1628 
  1629 text \<open>
  1630 The @{command primrec} command generates the following properties (listed
  1631 for @{const tfold}):
  1632 
  1633 \begin{indentblock}
  1634 \begin{description}
  1635 
  1636 \item[@{text "f."}\hthm{simps} @{text "[simp, code]"}\rm:] ~ \\
  1637 @{thm tfold.simps(1)[no_vars]} \\
  1638 @{thm tfold.simps(2)[no_vars]} \\
  1639 The @{text "[code]"} attribute is set by the @{text code} plugin
  1640 (Section~\ref{ssec:code-generator}).
  1641 
  1642 \item[@{text "f."}\hthm{transfer} @{text "[transfer_rule]"}\rm:] ~ \\
  1643 @{thm tfold.transfer[no_vars]} \\
  1644 This theorem is generated by the @{text transfer} plugin
  1645 (Section~\ref{ssec:transfer}) for functions declared with the @{text transfer}
  1646 option enabled.
  1647 
  1648 \item[@{text "f."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
  1649 This induction rule is generated for nested-as-mutual recursive functions
  1650 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}).
  1651 
  1652 \item[@{text "f\<^sub>1_\<dots>_f\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
  1653 This induction rule is generated for nested-as-mutual recursive functions
  1654 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}). Given $m > 1$ mutually
  1655 recursive functions, this rule can be used to prove $m$ properties
  1656 simultaneously.
  1657 
  1658 \end{description}
  1659 \end{indentblock}
  1660 \<close>
  1661 
  1662 (*<*)
  1663     end
  1664 (*>*)
  1665 
  1666 
  1667 subsection \<open>Recursive Default Values for Selectors
  1668   \label{ssec:primrec-recursive-default-values-for-selectors}\<close>
  1669 
  1670 text \<open>
  1671 A datatype selector @{text un_D} can have a default value for each constructor
  1672 on which it is not otherwise specified. Occasionally, it is useful to have the
  1673 default value be defined recursively. This leads to a chicken-and-egg
  1674 situation, because the datatype is not introduced yet at the moment when the
  1675 selectors are introduced. Of course, we can always define the selectors
  1676 manually afterward, but we then have to state and prove all the characteristic
  1677 theorems ourselves instead of letting the package do it.
  1678 
  1679 Fortunately, there is a workaround that relies on overloading to relieve us
  1680 from the tedium of manual derivations:
  1681 
  1682 \begin{enumerate}
  1683 \setlength{\itemsep}{0pt}
  1684 
  1685 \item
  1686 Introduce a fully unspecified constant @{text "un_D\<^sub>0 :: 'a"} using
  1687 @{command consts}.
  1688 
  1689 \item
  1690 Define the datatype, specifying @{text "un_D\<^sub>0"} as the selector's default
  1691 value.
  1692 
  1693 \item
  1694 Define the behavior of @{text "un_D\<^sub>0"} on values of the newly introduced
  1695 datatype using the \keyw{overloading} command.
  1696 
  1697 \item
  1698 Derive the desired equation on @{text un_D} from the characteristic equations
  1699 for @{text "un_D\<^sub>0"}.
  1700 \end{enumerate}
  1701 
  1702 \noindent
  1703 The following example illustrates this procedure:
  1704 \<close>
  1705 
  1706 (*<*)
  1707     hide_const termi
  1708 (*>*)
  1709     consts termi\<^sub>0 :: 'a
  1710 
  1711 text \<open>\blankline\<close>
  1712 
  1713     datatype ('a, 'b) tlist =
  1714       TNil (termi: 'b)
  1715     | TCons (thd: 'a) (ttl: "('a, 'b) tlist")
  1716     where
  1717       "ttl (TNil y) = TNil y"
  1718     | "termi (TCons _ xs) = termi\<^sub>0 xs"
  1719 
  1720 text \<open>\blankline\<close>
  1721 
  1722     overloading
  1723       termi\<^sub>0 \<equiv> "termi\<^sub>0 :: ('a, 'b) tlist \<Rightarrow> 'b"
  1724     begin
  1725     primrec termi\<^sub>0 :: "('a, 'b) tlist \<Rightarrow> 'b" where
  1726       "termi\<^sub>0 (TNil y) = y"
  1727     | "termi\<^sub>0 (TCons x xs) = termi\<^sub>0 xs"
  1728     end
  1729 
  1730 text \<open>\blankline\<close>
  1731 
  1732     lemma termi_TCons[simp]: "termi (TCons x xs) = termi xs"
  1733       by (cases xs) auto
  1734 
  1735 
  1736 subsection \<open>Compatibility Issues
  1737   \label{ssec:primrec-compatibility-issues}\<close>
  1738 
  1739 text \<open>
  1740 The command @{command primrec}'s behavior on new-style datatypes has been
  1741 designed to be highly compatible with that for old-style datatypes, to ease
  1742 migration. There is nonetheless at least one incompatibility that may arise when
  1743 porting to the new package:
  1744 
  1745 \begin{itemize}
  1746 \setlength{\itemsep}{0pt}
  1747 
  1748 \item \emph{Some theorems have different names.}
  1749 For $m > 1$ mutually recursive functions,
  1750 @{text "f\<^sub>1_\<dots>_f\<^sub>m.simps"} has been broken down into separate
  1751 subcollections @{text "f\<^sub>i.simps"}.
  1752 \end{itemize}
  1753 \<close>
  1754 
  1755 
  1756 section \<open>Defining Codatatypes
  1757   \label{sec:defining-codatatypes}\<close>
  1758 
  1759 text \<open>
  1760 Codatatypes can be specified using the @{command codatatype} command. The
  1761 command is first illustrated through concrete examples featuring different
  1762 flavors of corecursion. More examples can be found in the directory
  1763 \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>. The \emph{Archive of Formal Proofs} also
  1764 includes some useful codatatypes, notably for lazy lists @{cite
  1765 "lochbihler-2010"}.
  1766 \<close>
  1767 
  1768 
  1769 subsection \<open>Introductory Examples
  1770   \label{ssec:codatatype-introductory-examples}\<close>
  1771 
  1772 subsubsection \<open>Simple Corecursion
  1773   \label{sssec:codatatype-simple-corecursion}\<close>
  1774 
  1775 text \<open>
  1776 Non-corecursive codatatypes coincide with the corresponding datatypes, so they
  1777 are rarely used in practice. \emph{Corecursive codatatypes} have the same syntax
  1778 as recursive datatypes, except for the command name. For example, here is the
  1779 definition of lazy lists:
  1780 \<close>
  1781 
  1782     codatatype (lset: 'a) llist =
  1783       lnull: LNil
  1784     | LCons (lhd: 'a) (ltl: "'a llist")
  1785     for
  1786       map: lmap
  1787       rel: llist_all2
  1788       pred: llist_all
  1789     where
  1790       "ltl LNil = LNil"
  1791 
  1792 text \<open>
  1793 \noindent
  1794 Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
  1795 @{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Here is a related type, that of
  1796 infinite streams:
  1797 \<close>
  1798 
  1799     codatatype (sset: 'a) stream =
  1800       SCons (shd: 'a) (stl: "'a stream")
  1801     for
  1802       map: smap
  1803       rel: stream_all2
  1804 
  1805 text \<open>
  1806 \noindent
  1807 Another interesting type that can
  1808 be defined as a codatatype is that of the extended natural numbers:
  1809 \<close>
  1810 
  1811     codatatype enat = EZero | ESucc enat
  1812 
  1813 text \<open>
  1814 \noindent
  1815 This type has exactly one infinite element, @{text "ESucc (ESucc (ESucc (\<dots>)))"},
  1816 that represents $\infty$. In addition, it has finite values of the form
  1817 @{text "ESucc (\<dots> (ESucc EZero)\<dots>)"}.
  1818 
  1819 Here is an example with many constructors:
  1820 \<close>
  1821 
  1822     codatatype 'a process =
  1823       Fail
  1824     | Skip (cont: "'a process")
  1825     | Action (prefix: 'a) (cont: "'a process")
  1826     | Choice (left: "'a process") (right: "'a process")
  1827 
  1828 text \<open>
  1829 \noindent
  1830 Notice that the @{const cont} selector is associated with both @{const Skip}
  1831 and @{const Action}.
  1832 \<close>
  1833 
  1834 
  1835 subsubsection \<open>Mutual Corecursion
  1836   \label{sssec:codatatype-mutual-corecursion}\<close>
  1837 
  1838 text \<open>
  1839 \noindent
  1840 The example below introduces a pair of \emph{mutually corecursive} types:
  1841 \<close>
  1842 
  1843     codatatype even_enat = Even_EZero | Even_ESucc odd_enat
  1844     and odd_enat = Odd_ESucc even_enat
  1845 
  1846 
  1847 subsubsection \<open>Nested Corecursion
  1848   \label{sssec:codatatype-nested-corecursion}\<close>
  1849 
  1850 text \<open>
  1851 \noindent
  1852 The next examples feature \emph{nested corecursion}:
  1853 \<close>
  1854 
  1855     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")
  1856 
  1857 text \<open>\blankline\<close>
  1858 
  1859     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")
  1860 
  1861 text \<open>\blankline\<close>
  1862 
  1863     codatatype 'a sm = SM (accept: bool) (trans: "'a \<Rightarrow> 'a sm")
  1864 
  1865 
  1866 subsection \<open>Command Syntax
  1867   \label{ssec:codatatype-command-syntax}\<close>
  1868 
  1869 subsubsection \<open>\keyw{codatatype}
  1870   \label{sssec:codatatype}\<close>
  1871 
  1872 text \<open>
  1873 \begin{matharray}{rcl}
  1874   @{command_def "codatatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
  1875 \end{matharray}
  1876 
  1877 @{rail \<open>
  1878   @@{command codatatype} target? @{syntax dt_options}? @{syntax dt_spec}
  1879 \<close>}
  1880 
  1881 \medskip
  1882 
  1883 \noindent
  1884 Definitions of codatatypes have almost exactly the same syntax as for datatypes
  1885 (Section~\ref{ssec:datatype-command-syntax}). The @{text "discs_sels"} option
  1886 is superfluous because discriminators and selectors are always generated for
  1887 codatatypes.
  1888 \<close>
  1889 
  1890 
  1891 subsection \<open>Generated Constants
  1892   \label{ssec:codatatype-generated-constants}\<close>
  1893 
  1894 text \<open>
  1895 Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
  1896 with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
  1897 \ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
  1898 datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
  1899 recursor is replaced by a dual concept:
  1900 
  1901 \medskip
  1902 
  1903 \begin{tabular}{@ {}ll@ {}}
  1904 Corecursor: &
  1905   @{text t.corec_t}
  1906 \end{tabular}
  1907 \<close>
  1908 
  1909 
  1910 subsection \<open>Generated Theorems
  1911   \label{ssec:codatatype-generated-theorems}\<close>
  1912 
  1913 text \<open>
  1914 The characteristic theorems generated by @{command codatatype} are grouped in
  1915 three broad categories:
  1916 
  1917 \begin{itemize}
  1918 \setlength{\itemsep}{0pt}
  1919 
  1920 \item The \emph{free constructor theorems}
  1921 (Section~\ref{sssec:free-constructor-theorems}) are properties of the
  1922 constructors and destructors that can be derived for any freely generated type.
  1923 
  1924 \item The \emph{functorial theorems}
  1925 (Section~\ref{sssec:functorial-theorems}) are properties of datatypes related to
  1926 their BNF nature.
  1927 
  1928 \item The \emph{coinductive theorems} (Section~\ref{sssec:coinductive-theorems})
  1929 are properties of datatypes related to their coinductive nature.
  1930 \end{itemize}
  1931 
  1932 \noindent
  1933 The first two categories are exactly as for datatypes.
  1934 \<close>
  1935 
  1936 
  1937 subsubsection \<open>Coinductive Theorems
  1938   \label{sssec:coinductive-theorems}\<close>
  1939 
  1940 text \<open>
  1941 The coinductive theorems are listed below for @{typ "'a llist"}:
  1942 
  1943 \begin{indentblock}
  1944 \begin{description}
  1945 
  1946 \item[\begin{tabular}{@ {}l@ {}}
  1947   @{text "t."}\hthm{coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1948   \phantom{@{text "t."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  1949   D\<^sub>n, coinduct t]"}\rm:
  1950 \end{tabular}] ~ \\
  1951 @{thm llist.coinduct[no_vars]}
  1952 
  1953 \item[\begin{tabular}{@ {}l@ {}}
  1954   @{text "t."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1955   \phantom{@{text "t."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm:
  1956 \end{tabular}] ~ \\
  1957 @{thm llist.coinduct_strong[no_vars]}
  1958 
  1959 \item[\begin{tabular}{@ {}l@ {}}
  1960   @{text "t."}\hthm{rel_coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1961   \phantom{@{text "t."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  1962   D\<^sub>n, coinduct pred]"}\rm:
  1963 \end{tabular}] ~ \\
  1964 @{thm llist.rel_coinduct[no_vars]}
  1965 
  1966 \item[\begin{tabular}{@ {}l@ {}}
  1967   @{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]"} \\
  1968   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1969   \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
  1970   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  1971   \phantom{@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{rel_coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots> D\<^sub>n]"}\rm: \\
  1972 \end{tabular}] ~ \\
  1973 Given $m > 1$ mutually corecursive codatatypes, these coinduction rules can be
  1974 used to prove $m$ properties simultaneously.
  1975 
  1976 \item[\begin{tabular}{@ {}l@ {}}
  1977   @{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{set_induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n,"} \\
  1978   \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: \\
  1979 \end{tabular}] ~ \\
  1980 @{thm llist.set_induct[no_vars]} \\
  1981 If $m = 1$, the attribute @{text "[consumes 1]"} is generated as well.
  1982 
  1983 \item[@{text "t."}\hthm{corec}\rm:] ~ \\
  1984 @{thm llist.corec(1)[no_vars]} \\
  1985 @{thm llist.corec(2)[no_vars]}
  1986 
  1987 \item[@{text "t."}\hthm{corec_code} @{text "[code]"}\rm:] ~ \\
  1988 @{thm llist.corec_code[no_vars]} \\
  1989 The @{text "[code]"} attribute is set by the @{text code} plugin
  1990 (Section~\ref{ssec:code-generator}).
  1991 
  1992 \item[@{text "t."}\hthm{corec_disc}\rm:] ~ \\
  1993 @{thm llist.corec_disc(1)[no_vars]} \\
  1994 @{thm llist.corec_disc(2)[no_vars]}
  1995 
  1996 \item[@{text "t."}\hthm{corec_disc_iff} @{text "[simp]"}\rm:] ~ \\
  1997 @{thm llist.corec_disc_iff(1)[no_vars]} \\
  1998 @{thm llist.corec_disc_iff(2)[no_vars]}
  1999 
  2000 \item[@{text "t."}\hthm{corec_sel} @{text "[simp]"}\rm:] ~ \\
  2001 @{thm llist.corec_sel(1)[no_vars]} \\
  2002 @{thm llist.corec_sel(2)[no_vars]}
  2003 
  2004 \item[@{text "t."}\hthm{map_o_corec}\rm:] ~ \\
  2005 @{thm llist.map_o_corec[no_vars]}
  2006 
  2007 \item[@{text "t."}\hthm{corec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
  2008 @{thm llist.corec_transfer[no_vars]} \\
  2009 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
  2010 (Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
  2011 
  2012 \end{description}
  2013 \end{indentblock}
  2014 
  2015 \noindent
  2016 For convenience, @{command codatatype} also provides the following collection:
  2017 
  2018 \begin{indentblock}
  2019 \begin{description}
  2020 
  2021 \item[@{text "t."}\hthm{simps}] = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.corec_disc_iff} @{text t.corec_sel} \\
  2022 @{text t.map} @{text t.rel_inject} @{text t.rel_distinct} @{text t.set}
  2023 
  2024 \end{description}
  2025 \end{indentblock}
  2026 \<close>
  2027 
  2028 
  2029 section \<open>Defining Primitively Corecursive Functions
  2030   \label{sec:defining-primitively-corecursive-functions}\<close>
  2031 
  2032 text \<open>
  2033 Corecursive functions can be specified using the @{command primcorec} and
  2034 \keyw{prim\-corec\-ursive} commands, which support primitive corecursion.
  2035 Other approaches include the more general \keyw{partial_function} command, the
  2036 \keyw{corec} and \keyw{corecursive} commands, and techniques based on domains
  2037 and topologies @{cite "lochbihler-hoelzl-2014"}. In this tutorial, the focus is
  2038 on @{command primcorec} and @{command primcorecursive}; \keyw{corec} and
  2039 \keyw{corecursive} are described in a separate tutorial
  2040 @{cite "isabelle-corec"}. More examples can be found in the directories
  2041 \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close> and \<^dir>\<open>~~/src/HOL/Corec_Examples\<close>.
  2042 
  2043 Whereas recursive functions consume datatypes one constructor at a time,
  2044 corecursive functions construct codatatypes one constructor at a time.
  2045 Partly reflecting a lack of agreement among proponents of coalgebraic methods,
  2046 Isabelle supports three competing syntaxes for specifying a function $f$:
  2047 
  2048 \begin{itemize}
  2049 \setlength{\itemsep}{0pt}
  2050 
  2051 \abovedisplayskip=.5\abovedisplayskip
  2052 \belowdisplayskip=.5\belowdisplayskip
  2053 
  2054 \item The \emph{destructor view} specifies $f$ by implications of the form
  2055 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and
  2056 equations of the form
  2057 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\]
  2058 This style is popular in the coalgebraic literature.
  2059 
  2060 \item The \emph{constructor view} specifies $f$ by equations of the form
  2061 \[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C\<^sub>j \<dots>"}\]
  2062 This style is often more concise than the previous one.
  2063 
  2064 \item The \emph{code view} specifies $f$ by a single equation of the form
  2065 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\]
  2066 with restrictions on the format of the right-hand side. Lazy functional
  2067 programming languages such as Haskell support a generalized version of this
  2068 style.
  2069 \end{itemize}
  2070 
  2071 All three styles are available as input syntax. Whichever syntax is chosen,
  2072 characteristic theorems for all three styles are generated.
  2073 
  2074 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy
  2075 %%% lists (cf. terminal0 in TLList.thy)
  2076 \<close>
  2077 
  2078 
  2079 subsection \<open>Introductory Examples
  2080   \label{ssec:primcorec-introductory-examples}\<close>
  2081 
  2082 text \<open>
  2083 Primitive corecursion is illustrated through concrete examples based on the
  2084 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More
  2085 examples can be found in the directory \<^dir>\<open>~~/src/HOL/Datatype_Examples\<close>.
  2086 The code view is favored in the examples below. Sections
  2087 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view}
  2088 present the same examples expressed using the constructor and destructor views.
  2089 \<close>
  2090 
  2091 
  2092 subsubsection \<open>Simple Corecursion
  2093   \label{sssec:primcorec-simple-corecursion}\<close>
  2094 
  2095 text \<open>
  2096 Following the code view, corecursive calls are allowed on the right-hand side as
  2097 long as they occur under a constructor, which itself appears either directly to
  2098 the right of the equal sign or in a conditional expression:
  2099 \<close>
  2100 
  2101     primcorec (*<*)(transfer) (*>*)literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
  2102       "literate g x = LCons x (literate g (g x))"
  2103 
  2104 text \<open>\blankline\<close>
  2105 
  2106     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
  2107       "siterate g x = SCons x (siterate g (g x))"
  2108 
  2109 text \<open>
  2110 \noindent
  2111 The constructor ensures that progress is made---i.e., the function is
  2112 \emph{productive}. The above functions compute the infinite lazy list or stream
  2113 @{text "[x, g x, g (g x), \<dots>]"}. Productivity guarantees that prefixes
  2114 @{text "[x, g x, g (g x), \<dots>, (g ^^ k) x]"} of arbitrary finite length
  2115 @{text k} can be computed by unfolding the code equation a finite number of
  2116 times.
  2117 
  2118 Corecursive functions construct codatatype values, but nothing prevents them
  2119 from also consuming such values. The following function drops every second
  2120 element in a stream:
  2121 \<close>
  2122 
  2123     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
  2124       "every_snd s = SCons (shd s) (stl (stl s))"
  2125 
  2126 text \<open>
  2127 \noindent
  2128 Constructs such as @{text "let"}--@{text "in"}, @{text
  2129 "if"}--@{text "then"}--@{text "else"}, and @{text "case"}--@{text "of"} may
  2130 appear around constructors that guard corecursive calls:
  2131 \<close>
  2132 
  2133     primcorec lapp :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2134       "lapp xs ys =
  2135          (case xs of
  2136             LNil \<Rightarrow> ys
  2137           | LCons x xs' \<Rightarrow> LCons x (lapp xs' ys))"
  2138 
  2139 text \<open>
  2140 \noindent
  2141 For technical reasons, @{text "case"}--@{text "of"} is only supported for
  2142 case distinctions on (co)datatypes that provide discriminators and selectors.
  2143 
  2144 Pattern matching is not supported by @{command primcorec}. Fortunately, it is
  2145 easy to generate pattern-maching equations using the @{command simps_of_case}
  2146 command provided by the theory \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close>.
  2147 \<close>
  2148 
  2149     simps_of_case lapp_simps: lapp.code
  2150 
  2151 text \<open>
  2152 This generates the lemma collection @{thm [source] lapp_simps}:
  2153 %
  2154 \begin{gather*}
  2155   @{thm lapp_simps(1)[no_vars]} \\
  2156   @{thm lapp_simps(2)[no_vars]}
  2157 \end{gather*}
  2158 %
  2159 Corecursion is useful to specify not only functions but also infinite objects:
  2160 \<close>
  2161 
  2162     primcorec infty :: enat where
  2163       "infty = ESucc infty"
  2164 
  2165 text \<open>
  2166 \noindent
  2167 The example below constructs a pseudorandom process value. It takes a stream of
  2168 actions (@{text s}), a pseudorandom function generator (@{text f}), and a
  2169 pseudorandom seed (@{text n}):
  2170 \<close>
  2171 
  2172 (*<*)
  2173     context early
  2174     begin
  2175 (*>*)
  2176     primcorec
  2177       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
  2178     where
  2179       "random_process s f n =
  2180          (if n mod 4 = 0 then
  2181             Fail
  2182           else if n mod 4 = 1 then
  2183             Skip (random_process s f (f n))
  2184           else if n mod 4 = 2 then
  2185             Action (shd s) (random_process (stl s) f (f n))
  2186           else
  2187             Choice (random_process (every_snd s) (f \<circ> f) (f n))
  2188               (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))"
  2189 (*<*)
  2190     end
  2191 (*>*)
  2192 
  2193 text \<open>
  2194 \noindent
  2195 The main disadvantage of the code view is that the conditions are tested
  2196 sequentially. This is visible in the generated theorems. The constructor and
  2197 destructor views offer nonsequential alternatives.
  2198 \<close>
  2199 
  2200 
  2201 subsubsection \<open>Mutual Corecursion
  2202   \label{sssec:primcorec-mutual-corecursion}\<close>
  2203 
  2204 text \<open>
  2205 The syntax for mutually corecursive functions over mutually corecursive
  2206 datatypes is unsurprising:
  2207 \<close>
  2208 
  2209     primcorec
  2210       even_infty :: even_enat and
  2211       odd_infty :: odd_enat
  2212     where
  2213       "even_infty = Even_ESucc odd_infty"
  2214     | "odd_infty = Odd_ESucc even_infty"
  2215 
  2216 
  2217 subsubsection \<open>Nested Corecursion
  2218   \label{sssec:primcorec-nested-corecursion}\<close>
  2219 
  2220 text \<open>
  2221 The next pair of examples generalize the @{const literate} and @{const siterate}
  2222 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly
  2223 infinite trees in which subnodes are organized either as a lazy list (@{text
  2224 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}). They rely on the map functions of
  2225 the nesting type constructors to lift the corecursive calls:
  2226 \<close>
  2227 
  2228     primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2229       "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i g) (g x))"
  2230 
  2231 text \<open>\blankline\<close>
  2232 
  2233     primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
  2234       "iterate\<^sub>i\<^sub>s g x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s g) (g x))"
  2235 
  2236 text \<open>
  2237 \noindent
  2238 Both examples follow the usual format for constructor arguments associated
  2239 with nested recursive occurrences of the datatype. Consider
  2240 @{const iterate\<^sub>i\<^sub>i}. The term @{term "g x"} constructs an @{typ "'a llist"}
  2241 value, which is turned into an @{typ "'a tree\<^sub>i\<^sub>i llist"} value using
  2242 @{const lmap}.
  2243 
  2244 This format may sometimes feel artificial. The following function constructs
  2245 a tree with a single, infinite branch from a stream:
  2246 \<close>
  2247 
  2248     primcorec tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2249       "tree\<^sub>i\<^sub>i_of_stream s =
  2250          Node\<^sub>i\<^sub>i (shd s) (lmap tree\<^sub>i\<^sub>i_of_stream (LCons (stl s) LNil))"
  2251 
  2252 text \<open>
  2253 \noindent
  2254 A more natural syntax, also supported by Isabelle, is to move corecursive calls
  2255 under constructors:
  2256 \<close>
  2257 
  2258     primcorec (*<*)(in late) (*>*)tree\<^sub>i\<^sub>i_of_stream :: "'a stream \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2259       "tree\<^sub>i\<^sub>i_of_stream s =
  2260          Node\<^sub>i\<^sub>i (shd s) (LCons (tree\<^sub>i\<^sub>i_of_stream (stl s)) LNil)"
  2261 
  2262 text \<open>
  2263 The next example illustrates corecursion through functions, which is a bit
  2264 special. Deterministic finite automata (DFAs) are traditionally defined as
  2265 5-tuples @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states,
  2266 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0}
  2267 is an initial state, and @{text F} is a set of final states. The following
  2268 function translates a DFA into a state machine:
  2269 \<close>
  2270 
  2271     primcorec (*<*)(in early) (*>*)sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
  2272       "sm_of_dfa \<delta> F q = SM (q \<in> F) (sm_of_dfa \<delta> F \<circ> \<delta> q)"
  2273 
  2274 text \<open>
  2275 \noindent
  2276 The map function for the function type (@{text \<Rightarrow>}) is composition
  2277 (@{text "op \<circ>"}). For convenience, corecursion through functions can
  2278 also be expressed using $\lambda$-abstractions and function application rather
  2279 than through composition. For example:
  2280 \<close>
  2281 
  2282     primcorec sm_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a sm" where
  2283       "sm_of_dfa \<delta> F q = SM (q \<in> F) (\<lambda>a. sm_of_dfa \<delta> F (\<delta> q a))"
  2284 
  2285 text \<open>\blankline\<close>
  2286 
  2287     primcorec empty_sm :: "'a sm" where
  2288       "empty_sm = SM False (\<lambda>_. empty_sm)"
  2289 
  2290 text \<open>\blankline\<close>
  2291 
  2292     primcorec not_sm :: "'a sm \<Rightarrow> 'a sm" where
  2293       "not_sm M = SM (\<not> accept M) (\<lambda>a. not_sm (trans M a))"
  2294 
  2295 text \<open>\blankline\<close>
  2296 
  2297     primcorec or_sm :: "'a sm \<Rightarrow> 'a sm \<Rightarrow> 'a sm" where
  2298       "or_sm M N =
  2299          SM (accept M \<or> accept N) (\<lambda>a. or_sm (trans M a) (trans N a))"
  2300 
  2301 text \<open>
  2302 \noindent
  2303 For recursion through curried $n$-ary functions, $n$ applications of
  2304 @{term "op \<circ>"} are necessary. The examples below illustrate the case where
  2305 $n = 2$:
  2306 \<close>
  2307 
  2308     codatatype ('a, 'b) sm2 =
  2309       SM2 (accept2: bool) (trans2: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) sm2")
  2310 
  2311 text \<open>\blankline\<close>
  2312 
  2313     primcorec
  2314       (*<*)(in early) (*>*)sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
  2315     where
  2316       "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (op \<circ> (op \<circ> (sm2_of_dfa \<delta> F)) (\<delta> q))"
  2317 
  2318 text \<open>\blankline\<close>
  2319 
  2320     primcorec
  2321       sm2_of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> ('a, 'b) sm2"
  2322     where
  2323       "sm2_of_dfa \<delta> F q = SM2 (q \<in> F) (\<lambda>a b. sm2_of_dfa \<delta> F (\<delta> q a b))"
  2324 
  2325 
  2326 subsubsection \<open>Nested-as-Mutual Corecursion
  2327   \label{sssec:primcorec-nested-as-mutual-corecursion}\<close>
  2328 
  2329 text \<open>
  2330 Just as it is possible to recurse over nested recursive datatypes as if they
  2331 were mutually recursive
  2332 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to
  2333 pretend that nested codatatypes are mutually corecursive. For example:
  2334 \<close>
  2335 
  2336 (*<*)
  2337     context late
  2338     begin
  2339 (*>*)
  2340     primcorec
  2341       iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and
  2342       iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist"
  2343     where
  2344       "iterate\<^sub>i\<^sub>i g x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i g (g x))"
  2345     | "iterates\<^sub>i\<^sub>i g xs =
  2346          (case xs of
  2347             LNil \<Rightarrow> LNil
  2348           | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i g x) (iterates\<^sub>i\<^sub>i g xs'))"
  2349 
  2350 text \<open>
  2351 \noindent
  2352 Coinduction rules are generated as
  2353 @{thm [source] iterate\<^sub>i\<^sub>i.coinduct},
  2354 @{thm [source] iterates\<^sub>i\<^sub>i.coinduct}, and
  2355 @{thm [source] iterate\<^sub>i\<^sub>i_iterates\<^sub>i\<^sub>i.coinduct}
  2356 and analogously for @{text coinduct_strong}. These rules and the
  2357 underlying corecursors are generated dynamically and are kept in a cache
  2358 to speed up subsequent definitions.
  2359 \<close>
  2360 
  2361 (*<*)
  2362     end
  2363 (*>*)
  2364 
  2365 
  2366 subsubsection \<open>Constructor View
  2367   \label{ssec:primrec-constructor-view}\<close>
  2368 
  2369 (*<*)
  2370     locale ctr_view
  2371     begin
  2372 (*>*)
  2373 
  2374 text \<open>
  2375 The constructor view is similar to the code view, but there is one separate
  2376 conditional equation per constructor rather than a single unconditional
  2377 equation. Examples that rely on a single constructor, such as @{const literate}
  2378 and @{const siterate}, are identical in both styles.
  2379 
  2380 Here is an example where there is a difference:
  2381 \<close>
  2382 
  2383     primcorec lapp :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2384       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lapp xs ys = LNil"
  2385     | "_ \<Longrightarrow> lapp xs ys = LCons (lhd (if lnull xs then ys else xs))
  2386          (if xs = LNil then ltl ys else lapp (ltl xs) ys)"
  2387 
  2388 text \<open>
  2389 \noindent
  2390 With the constructor view, we must distinguish between the @{const LNil} and
  2391 the @{const LCons} case. The condition for @{const LCons} is
  2392 left implicit, as the negation of that for @{const LNil}.
  2393 
  2394 For this example, the constructor view is slightly more involved than the
  2395 code equation. Recall the code view version presented in
  2396 Section~\ref{sssec:primcorec-simple-corecursion}.
  2397 % TODO: \[{thm code_view.lapp.code}\]
  2398 The constructor view requires us to analyze the second argument (@{term ys}).
  2399 The code equation generated from the constructor view also suffers from this.
  2400 % TODO: \[{thm lapp.code}\]
  2401 
  2402 In contrast, the next example is arguably more naturally expressed in the
  2403 constructor view:
  2404 \<close>
  2405 
  2406     primcorec
  2407       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
  2408     where
  2409       "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail"
  2410     | "n mod 4 = 1 \<Longrightarrow>
  2411          random_process s f n = Skip (random_process s f (f n))"
  2412     | "n mod 4 = 2 \<Longrightarrow>
  2413          random_process s f n = Action (shd s) (random_process (stl s) f (f n))"
  2414     | "n mod 4 = 3 \<Longrightarrow>
  2415          random_process s f n = Choice (random_process (every_snd s) f (f n))
  2416            (random_process (every_snd (stl s)) f (f n))"
  2417 (*<*)
  2418     end
  2419 (*>*)
  2420 
  2421 text \<open>
  2422 \noindent
  2423 Since there is no sequentiality, we can apply the equation for @{const Choice}
  2424 without having first to discharge @{term "n mod (4::int) \<noteq> 0"},
  2425 @{term "n mod (4::int) \<noteq> 1"}, and
  2426 @{term "n mod (4::int) \<noteq> 2"}.
  2427 The price to pay for this elegance is that we must discharge exclusiveness proof
  2428 obligations, one for each pair of conditions
  2429 @{term "(n mod (4::int) = i, n mod (4::int) = j)"}
  2430 with @{term "i < j"}. If we prefer not to discharge any obligations, we can
  2431 enable the @{text "sequential"} option. This pushes the problem to the users of
  2432 the generated properties.
  2433 %Here are more examples to conclude:
  2434 \<close>
  2435 
  2436 
  2437 subsubsection \<open>Destructor View
  2438   \label{ssec:primrec-destructor-view}\<close>
  2439 
  2440 (*<*)
  2441     locale dtr_view
  2442     begin
  2443 (*>*)
  2444 
  2445 text \<open>
  2446 The destructor view is in many respects dual to the constructor view. Conditions
  2447 determine which constructor to choose, and these conditions are interpreted
  2448 sequentially or not depending on the @{text "sequential"} option.
  2449 Consider the following examples:
  2450 \<close>
  2451 
  2452     primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where
  2453       "\<not> lnull (literate _ x)"
  2454     | "lhd (literate _ x) = x"
  2455     | "ltl (literate g x) = literate g (g x)"
  2456 
  2457 text \<open>\blankline\<close>
  2458 
  2459     primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where
  2460       "shd (siterate _ x) = x"
  2461     | "stl (siterate g x) = siterate g (g x)"
  2462 
  2463 text \<open>\blankline\<close>
  2464 
  2465     primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where
  2466       "shd (every_snd s) = shd s"
  2467     | "stl (every_snd s) = stl (stl s)"
  2468 
  2469 text \<open>
  2470 \noindent
  2471 The first formula in the @{const literate} specification indicates which
  2472 constructor to choose. For @{const siterate} and @{const every_snd}, no such
  2473 formula is necessary, since the type has only one constructor. The last two
  2474 formulas are equations specifying the value of the result for the relevant
  2475 selectors. Corecursive calls appear directly to the right of the equal sign.
  2476 Their arguments are unrestricted.
  2477 
  2478 The next example shows how to specify functions that rely on more than one
  2479 constructor:
  2480 \<close>
  2481 
  2482     primcorec lapp :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2483       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lapp xs ys)"
  2484     | "lhd (lapp xs ys) = lhd (if lnull xs then ys else xs)"
  2485     | "ltl (lapp xs ys) = (if xs = LNil then ltl ys else lapp (ltl xs) ys)"
  2486 
  2487 text \<open>
  2488 \noindent
  2489 For a codatatype with $n$ constructors, it is sufficient to specify $n - 1$
  2490 discriminator formulas. The command will then assume that the remaining
  2491 constructor should be taken otherwise. This can be made explicit by adding
  2492 \<close>
  2493 
  2494 (*<*)
  2495     end
  2496 
  2497     locale dtr_view2
  2498     begin
  2499 
  2500     primcorec lapp :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where
  2501       "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lnull (lapp xs ys)"
  2502     | "lhd (lapp xs ys) = lhd (if lnull xs then ys else xs)"
  2503     | "ltl (lapp xs ys) = (if xs = LNil then ltl ys else lapp (ltl xs) ys)" |
  2504 (*>*)
  2505       "_ \<Longrightarrow> \<not> lnull (lapp xs ys)"
  2506 
  2507 text \<open>
  2508 \noindent
  2509 to the specification. The generated selector theorems are conditional.
  2510 
  2511 The next example illustrates how to cope with selectors defined for several
  2512 constructors:
  2513 \<close>
  2514 
  2515     primcorec
  2516       random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process"
  2517     where
  2518       "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail"
  2519     | "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)"
  2520     | "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)"
  2521     | "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)"
  2522     | "cont (random_process s f n) = random_process s f (f n)" of Skip
  2523     | "prefix (random_process s f n) = shd s"
  2524     | "cont (random_process s f n) = random_process (stl s) f (f n)" of Action
  2525     | "left (random_process s f n) = random_process (every_snd s) f (f n)"
  2526     | "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)"
  2527 
  2528 text \<open>
  2529 \noindent
  2530 Using the @{text "of"} keyword, different equations are specified for @{const
  2531 cont} depending on which constructor is selected.
  2532 
  2533 Here are more examples to conclude:
  2534 \<close>
  2535 
  2536     primcorec
  2537       even_infty :: even_enat and
  2538       odd_infty :: odd_enat
  2539     where
  2540       "even_infty \<noteq> Even_EZero"
  2541     | "un_Even_ESucc even_infty = odd_infty"
  2542     | "un_Odd_ESucc odd_infty = even_infty"
  2543 
  2544 text \<open>\blankline\<close>
  2545 
  2546     primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where
  2547       "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = x"
  2548     | "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i g x) = lmap (iterate\<^sub>i\<^sub>i g) (g x)"
  2549 (*<*)
  2550     end
  2551 (*>*)
  2552 
  2553 
  2554 subsection \<open>Command Syntax
  2555   \label{ssec:primcorec-command-syntax}\<close>
  2556 
  2557 subsubsection \<open>\keyw{primcorec} and \keyw{primcorecursive}
  2558   \label{sssec:primcorecursive-and-primcorec}\<close>
  2559 
  2560 text \<open>
  2561 \begin{matharray}{rcl}
  2562   @{command_def "primcorec"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
  2563   @{command_def "primcorecursive"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  2564 \end{matharray}
  2565 
  2566 @{rail \<open>
  2567   (@@{command primcorec} | @@{command primcorecursive}) target? \<newline>
  2568     @{syntax pcr_options}? fixes @'where' (@{syntax pcr_formula} + '|')
  2569   ;
  2570   @{syntax_def pcr_options}: '(' ((@{syntax plugins} | 'sequential' | 'exhaustive' | 'transfer') + ',') ')'
  2571   ;
  2572   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
  2573 \<close>}
  2574 
  2575 \medskip
  2576 
  2577 \noindent
  2578 The @{command primcorec} and @{command primcorecursive} commands introduce a set
  2579 of mutually corecursive functions over codatatypes.
  2580 
  2581 The syntactic entity \synt{target} can be used to specify a local context,
  2582 \synt{fixes} denotes a list of names with optional type signatures,
  2583 \synt{thmdecl} denotes an optional name for the formula that follows, and
  2584 \synt{prop} denotes a HOL proposition @{cite "isabelle-isar-ref"}.
  2585 
  2586 The optional target is optionally followed by a combination of the following
  2587 options:
  2588 
  2589 \begin{itemize}
  2590 \setlength{\itemsep}{0pt}
  2591 
  2592 \item
  2593 The @{text plugins} option indicates which plugins should be enabled
  2594 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
  2595 
  2596 \item
  2597 The @{text sequential} option indicates that the conditions in specifications
  2598 expressed using the constructor or destructor view are to be interpreted
  2599 sequentially.
  2600 
  2601 \item
  2602 The @{text exhaustive} option indicates that the conditions in specifications
  2603 expressed using the constructor or destructor view cover all possible cases.
  2604 This generally gives rise to an additional proof obligation.
  2605 
  2606 \item
  2607 The @{text transfer} option indicates that an unconditional transfer rule
  2608 should be generated and proved @{text "by transfer_prover"}. The
  2609 @{text "[transfer_rule]"} attribute is set on the generated theorem.
  2610 \end{itemize}
  2611 
  2612 The @{command primcorec} command is an abbreviation for @{command
  2613 primcorecursive} with @{text "by auto?"} to discharge any emerging proof
  2614 obligations.
  2615 
  2616 %%% TODO: elaborate on format of the propositions
  2617 %%% TODO: elaborate on mutual and nested-to-mutual
  2618 \<close>
  2619 
  2620 
  2621 subsection \<open>Generated Theorems
  2622   \label{ssec:primcorec-generated-theorems}\<close>
  2623 
  2624 text \<open>
  2625 The @{command primcorec} and @{command primcorecursive} commands generate the
  2626 following properties (listed for @{const literate}):
  2627 
  2628 \begin{indentblock}
  2629 \begin{description}
  2630 
  2631 \item[@{text "f."}\hthm{code} @{text "[code]"}\rm:] ~ \\
  2632 @{thm literate.code[no_vars]} \\
  2633 The @{text "[code]"} attribute is set by the @{text code} plugin
  2634 (Section~\ref{ssec:code-generator}).
  2635 
  2636 \item[@{text "f."}\hthm{ctr}\rm:] ~ \\
  2637 @{thm literate.ctr[no_vars]}
  2638 
  2639 \item[@{text "f."}\hthm{disc} @{text "[simp, code]"}\rm:] ~ \\
  2640 @{thm literate.disc[no_vars]} \\
  2641 The @{text "[code]"} attribute is set by the @{text code} plugin
  2642 (Section~\ref{ssec:code-generator}). The @{text "[simp]"} attribute is set only
  2643 for functions for which @{text f.disc_iff} is not available.
  2644 
  2645 \item[@{text "f."}\hthm{disc_iff} @{text "[simp]"}\rm:] ~ \\
  2646 @{thm literate.disc_iff[no_vars]} \\
  2647 This property is generated only for functions declared with the
  2648 @{text exhaustive} option or whose conditions are trivially exhaustive.
  2649 
  2650 \item[@{text "f."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
  2651 @{thm literate.disc[no_vars]} \\
  2652 The @{text "[code]"} attribute is set by the @{text code} plugin
  2653 (Section~\ref{ssec:code-generator}).
  2654 
  2655 \item[@{text "f."}\hthm{exclude}\rm:] ~ \\
  2656 These properties are missing for @{const literate} because no exclusiveness
  2657 proof obligations arose. In general, the properties correspond to the
  2658 discharged proof obligations.
  2659 
  2660 \item[@{text "f."}\hthm{exhaust}\rm:] ~ \\
  2661 This property is missing for @{const literate} because no exhaustiveness
  2662 proof obligation arose. In general, the property correspond to the discharged
  2663 proof obligation.
  2664 
  2665 \item[\begin{tabular}{@ {}l@ {}}
  2666   @{text "f."}\hthm{coinduct} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  2667   \phantom{@{text "f."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  2668   D\<^sub>n]"}\rm:
  2669 \end{tabular}] ~ \\
  2670 This coinduction rule is generated for nested-as-mutual corecursive functions
  2671 (Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}).
  2672 
  2673 \item[\begin{tabular}{@ {}l@ {}}
  2674   @{text "f."}\hthm{coinduct_strong} @{text "[consumes m, case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  2675   \phantom{@{text "f."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  2676   D\<^sub>n]"}\rm:
  2677 \end{tabular}] ~ \\
  2678 This coinduction rule is generated for nested-as-mutual corecursive functions
  2679 (Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}).
  2680 
  2681 \item[\begin{tabular}{@ {}l@ {}}
  2682   @{text "f\<^sub>1_\<dots>_f\<^sub>m."}\hthm{coinduct} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  2683   \phantom{@{text "f."}\hthm{coinduct} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  2684   D\<^sub>n]"}\rm:
  2685 \end{tabular}] ~ \\
  2686 This coinduction rule is generated for nested-as-mutual corecursive functions
  2687 (Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}). Given $m > 1$
  2688 mutually corecursive functions, this rule can be used to prove $m$ properties
  2689 simultaneously.
  2690 
  2691 \item[\begin{tabular}{@ {}l@ {}}
  2692   @{text "f\<^sub>1_\<dots>_f\<^sub>m."}\hthm{coinduct_strong} @{text "[case_names t\<^sub>1 \<dots> t\<^sub>m,"} \\
  2693   \phantom{@{text "f."}\hthm{coinduct_strong} @{text "["}}@{text "case_conclusion D\<^sub>1 \<dots>
  2694   D\<^sub>n]"}\rm:
  2695 \end{tabular}] ~ \\
  2696 This coinduction rule is generated for nested-as-mutual corecursive functions
  2697 (Section~\ref{sssec:primcorec-nested-as-mutual-corecursion}). Given $m > 1$
  2698 mutually corecursive functions, this rule can be used to prove $m$ properties
  2699 simultaneously.
  2700 
  2701 \end{description}
  2702 \end{indentblock}
  2703 
  2704 \noindent
  2705 For convenience, @{command primcorec} and @{command primcorecursive} also
  2706 provide the following collection:
  2707 
  2708 \begin{indentblock}
  2709 \begin{description}
  2710 
  2711 \item[@{text "f."}\hthm{simps}] = @{text f.disc_iff} (or @{text f.disc}) @{text t.sel}
  2712 
  2713 \end{description}
  2714 \end{indentblock}
  2715 \<close>
  2716 
  2717 
  2718 (*
  2719 subsection \<open>Recursive Default Values for Selectors
  2720   \label{ssec:primcorec-recursive-default-values-for-selectors}\<close>
  2721 
  2722 text \<open>
  2723 partial_function to the rescue
  2724 \<close>
  2725 *)
  2726 
  2727 
  2728 section \<open>Registering Bounded Natural Functors
  2729   \label{sec:registering-bounded-natural-functors}\<close>
  2730 
  2731 text \<open>
  2732 The (co)datatype package can be set up to allow nested recursion through
  2733 arbitrary type constructors, as long as they adhere to the BNF requirements
  2734 and are registered as BNFs. It is also possible to declare a BNF abstractly
  2735 without specifying its internal structure.
  2736 \<close>
  2737 
  2738 
  2739 subsection \<open>Bounded Natural Functors
  2740   \label{ssec:bounded-natural-functors}\<close>
  2741 
  2742 text \<open>
  2743 Bounded natural functors (BNFs) are a semantic criterion for where
  2744 (co)re\-cur\-sion may appear on the right-hand side of an equation
  2745 @{cite "traytel-et-al-2012" and "blanchette-et-al-2015-wit"}.
  2746 
  2747 An $n$-ary BNF is a type constructor equipped with a map function
  2748 (functorial action), $n$ set functions (natural transformations),
  2749 and an infinite cardinal bound that satisfy certain properties.
  2750 For example, @{typ "'a llist"} is a unary BNF.
  2751 Its predicator @{text "llist_all ::
  2752   ('a \<Rightarrow> bool) \<Rightarrow>
  2753   'a llist \<Rightarrow> bool"}
  2754 extends unary predicates over elements to unary predicates over
  2755 lazy lists.
  2756 Similarly, its relator @{text "llist_all2 ::
  2757   ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow>
  2758   'a llist \<Rightarrow> 'b llist \<Rightarrow> bool"}
  2759 extends binary predicates over elements to binary predicates over parallel
  2760 lazy lists. The cardinal bound limits the number of elements returned by the
  2761 set function; it may not depend on the cardinality of @{typ 'a}.
  2762 
  2763 The type constructors introduced by @{command datatype} and
  2764 @{command codatatype} are automatically registered as BNFs. In addition, a
  2765 number of old-style datatypes and non-free types are preregistered.
  2766 
  2767 Given an $n$-ary BNF, the $n$ type variables associated with set functions,
  2768 and on which the map function acts, are \emph{live}; any other variables are
  2769 \emph{dead}. Nested (co)recursion can only take place through live variables.
  2770 \<close>
  2771 
  2772 
  2773 subsection \<open>Introductory Examples
  2774   \label{ssec:bnf-introductory-examples}\<close>
  2775 
  2776 text \<open>
  2777 The example below shows how to register a type as a BNF using the @{command bnf}
  2778 command. Some of the proof obligations are best viewed with the theory
  2779 \<^file>\<open>~~/src/HOL/Library/Cardinal_Notations.thy\<close> imported.
  2780 
  2781 The type is simply a copy of the function space @{typ "'d \<Rightarrow> 'a"}, where @{typ 'a}
  2782 is live and @{typ 'd} is dead. We introduce it together with its map function,
  2783 set function, predicator, and relator.
  2784 \<close>
  2785 
  2786     typedef ('d, 'a) fn = "UNIV :: ('d \<Rightarrow> 'a) set"
  2787       by simp
  2788 
  2789 text \<open>\blankline\<close>
  2790 
  2791     setup_lifting type_definition_fn
  2792 
  2793 text \<open>\blankline\<close>
  2794 
  2795     lift_definition map_fn :: "('a \<Rightarrow> 'b) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn" is "op \<circ>" .
  2796     lift_definition set_fn :: "('d, 'a) fn \<Rightarrow> 'a set" is range .
  2797 
  2798 text \<open>\blankline\<close>
  2799 
  2800     lift_definition
  2801       pred_fn :: "('a \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> bool"
  2802     is
  2803       "pred_fun (\<lambda>_. True)" .
  2804 
  2805     lift_definition
  2806       rel_fn :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('d, 'a) fn \<Rightarrow> ('d, 'b) fn \<Rightarrow> bool"
  2807     is
  2808       "rel_fun (op =)" .
  2809 
  2810 text \<open>\blankline\<close>
  2811 
  2812     bnf "('d, 'a) fn"
  2813       map: map_fn
  2814       sets: set_fn
  2815       bd: "natLeq +c |UNIV :: 'd set|"
  2816       rel: rel_fn
  2817       pred: pred_fn
  2818     proof -
  2819       show "map_fn id = id"
  2820         by transfer auto
  2821     next
  2822       fix f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
  2823       show "map_fn (g \<circ> f) = map_fn g \<circ> map_fn f"
  2824         by transfer (auto simp add: comp_def)
  2825     next
  2826       fix F :: "('d, 'a) fn" and f g :: "'a \<Rightarrow> 'b"
  2827       assume "\<And>x. x \<in> set_fn F \<Longrightarrow> f x = g x"
  2828       then show "map_fn f F = map_fn g F"
  2829         by transfer auto
  2830     next
  2831       fix f :: "'a \<Rightarrow> 'b"
  2832       show "set_fn \<circ> map_fn f = op ` f \<circ> set_fn"
  2833         by transfer (auto simp add: comp_def)
  2834     next
  2835       show "card_order (natLeq +c |UNIV :: 'd set| )"
  2836         apply (rule card_order_csum)
  2837         apply (rule natLeq_card_order)
  2838         by (rule card_of_card_order_on)
  2839     next
  2840       show "cinfinite (natLeq +c |UNIV :: 'd set| )"
  2841         apply (rule cinfinite_csum)
  2842         apply (rule disjI1)
  2843         by (rule natLeq_cinfinite)
  2844     next
  2845       fix F :: "('d, 'a) fn"
  2846       have "|set_fn F| \<le>o |UNIV :: 'd set|" (is "_ \<le>o ?U")
  2847         by transfer (rule card_of_image)
  2848       also have "?U \<le>o natLeq +c ?U"
  2849         by (rule ordLeq_csum2) (rule card_of_Card_order)
  2850       finally show "|set_fn F| \<le>o natLeq +c |UNIV :: 'd set|" .
  2851     next
  2852       fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
  2853       show "rel_fn R OO rel_fn S \<le> rel_fn (R OO S)"
  2854         by (rule, transfer) (auto simp add: rel_fun_def)
  2855     next
  2856       fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool"
  2857       show "rel_fn R = (\<lambda>x y. \<exists>z. set_fn z \<subseteq> {(x, y). R x y} \<and> map_fn fst z = x \<and> map_fn snd z = y)"
  2858         unfolding fun_eq_iff relcompp.simps conversep.simps
  2859         by transfer (force simp: rel_fun_def subset_iff)
  2860     next
  2861       fix P :: "'a \<Rightarrow> bool"
  2862       show "pred_fn P = (\<lambda>x. Ball (set_fn x) P)"
  2863         unfolding fun_eq_iff by transfer simp
  2864     qed
  2865 
  2866 text \<open>\blankline\<close>
  2867 
  2868     print_theorems
  2869     print_bnfs
  2870 
  2871 text \<open>
  2872 \noindent
  2873 Using \keyw{print_theorems} and @{command print_bnfs}, we can contemplate and
  2874 show the world what we have achieved.
  2875 
  2876 This particular example does not need any nonemptiness witness, because the
  2877 one generated by default is good enough, but in general this would be
  2878 necessary. See \<^file>\<open>~~/src/HOL/Basic_BNFs.thy\<close>,
  2879 \<^file>\<open>~~/src/HOL/Library/Countable_Set_Type.thy\<close>,
  2880 \<^file>\<open>~~/src/HOL/Library/FSet.thy\<close>, and
  2881 \<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for further examples of BNF
  2882 registration, some of which feature custom witnesses.
  2883 
  2884 For many typedefs, lifting the BNF structure from the raw type to the abstract
  2885 type can be done uniformly. This is the task of the @{command lift_bnf} command.
  2886 Using @{command lift_bnf}, the above registration of @{typ "('d, 'a) fn"} as a
  2887 BNF becomes much shorter:
  2888 \<close>
  2889 
  2890 (*<*)
  2891     context early
  2892     begin
  2893 (*>*)
  2894     lift_bnf (*<*)(no_warn_wits) (*>*)('d, 'a) fn
  2895       by auto
  2896 (*<*)
  2897     end
  2898 (*>*)
  2899 
  2900 text \<open>
  2901 For type copies (@{command typedef}s with @{term UNIV} as the representing set),
  2902 the proof obligations are so simple that they can be
  2903 discharged automatically, yielding another command, @{command copy_bnf}, which
  2904 does not emit any proof obligations:
  2905 \<close>
  2906 
  2907 (*<*)
  2908     context late
  2909     begin
  2910 (*>*)
  2911     copy_bnf ('d, 'a) fn
  2912 (*<*)
  2913     end
  2914 (*>*)
  2915 
  2916 text \<open>
  2917 Since record schemas are type copies, @{command copy_bnf} can be used to
  2918 register them as BNFs:
  2919 \<close>
  2920 
  2921     record 'a point =
  2922       xval :: 'a
  2923       yval :: 'a
  2924 
  2925 text \<open>\blankline\<close>
  2926 
  2927     copy_bnf ('a, 'z) point_ext
  2928 
  2929 text \<open>
  2930 In the general case, the proof obligations generated by @{command lift_bnf} are
  2931 simpler than the acual BNF properties. In particular, no cardinality reasoning
  2932 is required. Consider the following type of nonempty lists:
  2933 \<close>
  2934 
  2935     typedef 'a nonempty_list = "{xs :: 'a list. xs \<noteq> []}" by auto
  2936 
  2937 text \<open>
  2938 The @{command lift_bnf} command requires us to prove that the set of nonempty lists
  2939 is closed under the map function and the zip function. The latter only
  2940 occurs implicitly in the goal, in form of the variable
  2941 @{term "zs :: ('a \<times> 'b) list"}.
  2942 \<close>
  2943 
  2944     lift_bnf (*<*)(no_warn_wits) (*>*)'a nonempty_list
  2945     proof -
  2946       fix f (*<*):: "'a \<Rightarrow> 'c"(*>*)and xs :: "'a list"
  2947       assume "xs \<in> {xs. xs \<noteq> []}"
  2948       then show "map f xs \<in> {xs. xs \<noteq> []}"
  2949         by (cases xs(*<*) rule: list.exhaust(*>*)) auto
  2950     next
  2951       fix zs :: "('a \<times> 'b) list"
  2952       assume "map fst zs \<in> {xs. xs \<noteq> []}" "map snd zs \<in> {xs. xs \<noteq> []}"
  2953       then show "zs \<in> {xs. xs \<noteq> []}"
  2954         by (cases zs (*<*)rule: list.exhaust(*>*)) auto
  2955     qed
  2956 
  2957 text \<open>
  2958 The next example declares a BNF axiomatically. This can be convenient for
  2959 reasoning abstractly about an arbitrary BNF. The @{command bnf_axiomatization}
  2960 command below introduces a type @{text "('a, 'b, 'c) F"}, three set constants,
  2961 a map function, a predicator, a relator, and a nonemptiness witness that depends only on
  2962 @{typ 'a}. The type @{text "'a \<Rightarrow> ('a, 'b, 'c) F"} of the witness can be read
  2963 as an implication: Given a witness for @{typ 'a}, we can construct a witness for
  2964 @{text "('a, 'b, 'c) F"}. The BNF properties are postulated as axioms.
  2965 \<close>
  2966 
  2967     bnf_axiomatization (setA: 'a, setB: 'b, setC: 'c) F
  2968       [wits: "'a \<Rightarrow> ('a, 'b, 'c) F"]
  2969 
  2970 text \<open>\blankline\<close>
  2971 
  2972     print_theorems
  2973     print_bnfs
  2974 
  2975 
  2976 subsection \<open>Command Syntax
  2977   \label{ssec:bnf-command-syntax}\<close>
  2978 
  2979 subsubsection \<open>\keyw{bnf}
  2980   \label{sssec:bnf}\<close>
  2981 
  2982 text \<open>
  2983 \begin{matharray}{rcl}
  2984   @{command_def "bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  2985 \end{matharray}
  2986 
  2987 @{rail \<open>
  2988   @@{command bnf} target? (name ':')? type \<newline>
  2989     'map:' term ('sets:' (term +))? 'bd:' term \<newline>
  2990     ('wits:' (term +))? ('rel:' term)? \<newline>
  2991     ('pred:' term)? @{syntax plugins}?
  2992 \<close>}
  2993 
  2994 \medskip
  2995 
  2996 \noindent
  2997 The @{command bnf} command registers an existing type as a bounded natural
  2998 functor (BNF). The type must be equipped with an appropriate map function
  2999 (functorial action). In addition, custom set functions, predicators, relators, and
  3000 nonemptiness witnesses can be specified; otherwise, default versions are used.
  3001 
  3002 The syntactic entity \synt{target} can be used to specify a local context,
  3003 \synt{type} denotes a HOL type, and \synt{term} denotes a HOL term
  3004 @{cite "isabelle-isar-ref"}.
  3005 
  3006 The @{syntax plugins} option indicates which plugins should be enabled
  3007 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
  3008 
  3009 %%% TODO: elaborate on proof obligations
  3010 \<close>
  3011 
  3012 subsubsection \<open>\keyw{lift_bnf}
  3013   \label{sssec:lift-bnf}\<close>
  3014 
  3015 text \<open>
  3016 \begin{matharray}{rcl}
  3017   @{command_def "lift_bnf"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  3018 \end{matharray}
  3019 
  3020 @{rail \<open>
  3021   @@{command lift_bnf} target? lb_options? \<newline>
  3022     @{syntax tyargs} name wit_terms?  \<newline>
  3023     ('via' thm)? @{syntax map_rel_pred}?
  3024   ;
  3025   @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
  3026   ;
  3027   @{syntax_def wit_terms}: '[' 'wits' ':' terms ']'
  3028 \<close>}
  3029 \medskip
  3030 
  3031 \noindent
  3032 The @{command lift_bnf} command registers as a BNF an existing type (the
  3033 \emph{abstract type}) that was defined as a subtype of a BNF (the \emph{raw
  3034 type}) using the @{command typedef} command. To achieve this, it lifts the BNF
  3035 structure on the raw type to the abstract type following a @{term
  3036 type_definition} theorem. The theorem is usually inferred from the type, but can
  3037 also be explicitly supplied by means of the optional @{text via} clause. In
  3038 addition, custom names for the set functions, the map function, the predicator, and the relator,
  3039 as well as nonemptiness witnesses can be specified.
  3040 
  3041 Nonemptiness witnesses are not lifted from the raw type's BNF, as this would be
  3042 incomplete. They must be given as terms (on the raw type) and proved to be
  3043 witnesses. The command warns about witness types that are present in the raw
  3044 type's BNF but not supplied by the user. The warning can be disabled by
  3045 specifying the @{text no_warn_wits} option.
  3046 \<close>
  3047 
  3048 subsubsection \<open>\keyw{copy_bnf}
  3049   \label{sssec:copy-bnf}\<close>
  3050 
  3051 text \<open>
  3052 \begin{matharray}{rcl}
  3053   @{command_def "copy_bnf"} & : & @{text "local_theory \<rightarrow> local_theory"}
  3054 \end{matharray}
  3055 
  3056 @{rail \<open>
  3057   @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
  3058     @{syntax tyargs} name ('via' thm)? @{syntax map_rel_pred}?
  3059 \<close>}
  3060 \medskip
  3061 
  3062 \noindent
  3063 The @{command copy_bnf} command performs the same lifting as @{command lift_bnf}
  3064 for type copies (@{command typedef}s with @{term UNIV} as the representing set),
  3065 without requiring the user to discharge any proof obligations or provide
  3066 nonemptiness witnesses.
  3067 \<close>
  3068 
  3069 subsubsection \<open>\keyw{bnf_axiomatization}
  3070   \label{sssec:bnf-axiomatization}\<close>
  3071 
  3072 text \<open>
  3073 \begin{matharray}{rcl}
  3074   @{command_def "bnf_axiomatization"} & : & @{text "local_theory \<rightarrow> local_theory"}
  3075 \end{matharray}
  3076 
  3077 @{rail \<open>
  3078   @@{command bnf_axiomatization} target? ('(' @{syntax plugins} ')')? \<newline>
  3079     @{syntax tyargs}? name @{syntax wit_types}? \<newline>
  3080     mixfix? @{syntax map_rel_pred}?
  3081   ;
  3082   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
  3083 \<close>}
  3084 
  3085 \medskip
  3086 
  3087 \noindent
  3088 The @{command bnf_axiomatization} command declares a new type and associated constants
  3089 (map, set, predicator, relator, and cardinal bound) and asserts the BNF properties for
  3090 these constants as axioms.
  3091 
  3092 The syntactic entity \synt{target} can be used to specify a local context,
  3093 \synt{name} denotes an identifier, \synt{typefree} denotes fixed type variable
  3094 (@{typ 'a}, @{typ 'b}, \ldots), \synt{mixfix} denotes the usual parenthesized
  3095 mixfix notation, and \synt{types} denotes a space-separated list of types
  3096 @{cite "isabelle-isar-ref"}.
  3097 
  3098 The @{syntax plugins} option indicates which plugins should be enabled
  3099 (@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
  3100 
  3101 Type arguments are live by default; they can be marked as dead by entering
  3102 @{text dead} in front of the type variable (e.g., @{text "(dead 'a)"})
  3103 instead of an identifier for the corresponding set function. Witnesses can be
  3104 specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
  3105 is identical to the left-hand side of a @{command datatype} or
  3106 @{command codatatype} definition.
  3107 
  3108 The command is useful to reason abstractly about BNFs. The axioms are safe
  3109 because there exist BNFs of arbitrary large arities. Applications must import
  3110 the \<^file>\<open>~~/src/HOL/Library/BNF_Axiomatization.thy\<close> theory
  3111 to use this functionality.
  3112 \<close>
  3113 
  3114 
  3115 subsubsection \<open>\keyw{print_bnfs}
  3116   \label{sssec:print-bnfs}\<close>
  3117 
  3118 text \<open>
  3119 \begin{matharray}{rcl}
  3120   @{command_def "print_bnfs"} & : & @{text "local_theory \<rightarrow>"}
  3121 \end{matharray}
  3122 
  3123 @{rail \<open>
  3124   @@{command print_bnfs}
  3125 \<close>}
  3126 \<close>
  3127 
  3128 
  3129 section \<open>Deriving Destructors and Theorems for Free Constructors
  3130   \label{sec:deriving-destructors-and-theorems-for-free-constructors}\<close>
  3131 
  3132 text \<open>
  3133 The derivation of convenience theorems for types equipped with free constructors,
  3134 as performed internally by @{command datatype} and @{command codatatype},
  3135 is available as a stand-alone command called @{command free_constructors}.
  3136 
  3137 %  * need for this is rare but may arise if you want e.g. to add destructors to
  3138 %    a type not introduced by ...
  3139 %
  3140 %  * @{command free_constructors}
  3141 %    * @{text plugins}, @{text discs_sels}
  3142 %    * hack to have both co and nonco view via locale (cf. ext nats)
  3143 \<close>
  3144 
  3145 
  3146 (*
  3147 subsection \<open>Introductory Example
  3148   \label{ssec:ctors-introductory-example}\<close>
  3149 *)
  3150 
  3151 
  3152 subsection \<open>Command Syntax
  3153   \label{ssec:ctors-command-syntax}\<close>
  3154 
  3155 subsubsection \<open>\keyw{free_constructors}
  3156   \label{sssec:free-constructors}\<close>
  3157 
  3158 text \<open>
  3159 \begin{matharray}{rcl}
  3160   @{command_def "free_constructors"} & : & @{text "local_theory \<rightarrow> proof(prove)"}
  3161 \end{matharray}
  3162 
  3163 @{rail \<open>
  3164   @@{command free_constructors} target? @{syntax dt_options} \<newline>
  3165     name 'for' (@{syntax fc_ctor} + '|') \<newline>
  3166   (@'where' (prop + '|'))?
  3167   ;
  3168   @{syntax_def fc_ctor}: (name ':')? term (name * )
  3169 \<close>}
  3170 
  3171 \medskip
  3172 
  3173 \noindent
  3174 The @{command free_constructors} command generates destructor constants for
  3175 freely constructed types as well as properties about constructors and
  3176 destructors. It also registers the constants and theorems in a data structure
  3177 that is queried by various tools (e.g., \keyw{function}).
  3178 
  3179 The syntactic entity \synt{target} can be used to specify a local context,
  3180 \synt{name} denotes an identifier, \synt{prop} denotes a HOL proposition, and
  3181 \synt{term} denotes a HOL term @{cite "isabelle-isar-ref"}.
  3182 
  3183 The syntax resembles that of @{command datatype} and @{command codatatype}
  3184 definitions (Sections
  3185 \ref{ssec:datatype-command-syntax}~and~\ref{ssec:codatatype-command-syntax}).
  3186 A constructor is specified by an optional name for the discriminator, the
  3187 constructor itself (as a term), and a list of optional names for the selectors.
  3188 
  3189 Section~\ref{ssec:datatype-generated-theorems} lists the generated theorems.
  3190 For bootstrapping reasons, the generally useful @{text "[fundef_cong]"}
  3191 attribute is not set on the generated @{text case_cong} theorem. It can be
  3192 added manually using \keyw{declare}.
  3193 \<close>
  3194 
  3195 
  3196 subsubsection \<open>\keyw{simps_of_case}
  3197   \label{sssec:simps-of-case}\<close>
  3198 
  3199 text \<open>
  3200 \begin{matharray}{rcl}
  3201   @{command_def "simps_of_case"} & : & @{text "local_theory \<rightarrow> local_theory"}
  3202 \end{matharray}
  3203 
  3204 @{rail \<open>
  3205   @@{command simps_of_case} target? (name ':')? \<newline>
  3206     (thm + ) (@'splits' ':' (thm + ))?
  3207 \<close>}
  3208 
  3209 \medskip
  3210 
  3211 \noindent
  3212 The @{command simps_of_case} command provided by theory
  3213 \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a single equation with
  3214 a complex case expression on the right-hand side into a set of pattern-matching
  3215 equations. For example,
  3216 \<close>
  3217 
  3218 (*<*)
  3219     context late
  3220     begin
  3221 (*>*)
  3222     simps_of_case lapp_simps: lapp.code
  3223 
  3224 text \<open>
  3225 \noindent
  3226 translates @{thm lapp.code[no_vars]} into
  3227 %
  3228 \begin{gather*}
  3229   @{thm lapp_simps(1)[no_vars]} \\
  3230   @{thm lapp_simps(2)[no_vars]}
  3231 \end{gather*}
  3232 \<close>
  3233 
  3234 
  3235 subsubsection \<open>\keyw{case_of_simps}
  3236   \label{sssec:case-of-simps}\<close>
  3237 
  3238 text \<open>
  3239 \begin{matharray}{rcl}
  3240   @{command_def "case_of_simps"} & : & @{text "local_theory \<rightarrow> local_theory"}
  3241 \end{matharray}
  3242 
  3243 @{rail \<open>
  3244   @@{command case_of_simps} target? (name ':')? \<newline>
  3245     (thm + )
  3246 \<close>}
  3247 
  3248 \medskip
  3249 
  3250 \noindent
  3251 The \keyw{case_of_simps} command provided by theory
  3252 \<^file>\<open>~~/src/HOL/Library/Simps_Case_Conv.thy\<close> converts a set of
  3253 pattern-matching equations into single equation with a complex case expression
  3254 on the right-hand side (cf.\ @{command simps_of_case}). For example,
  3255 \<close>
  3256 
  3257     case_of_simps lapp_case: lapp_simps
  3258 
  3259 text \<open>
  3260 \noindent
  3261 translates
  3262 %
  3263 \begin{gather*}
  3264   @{thm lapp_simps(1)[no_vars]} \\
  3265   @{thm lapp_simps(2)[no_vars]}
  3266 \end{gather*}
  3267 %
  3268 into @{thm lapp_case[no_vars]}.
  3269 \<close>
  3270 (*<*)
  3271     end
  3272 (*>*)
  3273 
  3274 
  3275 (*
  3276 section \<open>Using the Standard ML Interface
  3277   \label{sec:using-the-standard-ml-interface}\<close>
  3278 
  3279 text \<open>
  3280 The package's programmatic interface.
  3281 \<close>
  3282 *)
  3283 
  3284 
  3285 section \<open>Selecting Plugins
  3286   \label{sec:selecting-plugins}\<close>
  3287 
  3288 text \<open>
  3289 Plugins extend the (co)datatype package to interoperate with other Isabelle
  3290 packages and tools, such as the code generator, Transfer, Lifting, and
  3291 Quickcheck. They can be enabled or disabled individually using the
  3292 @{syntax plugins} option to the commands @{command datatype},
  3293 @{command primrec}, @{command codatatype}, @{command primcorec},
  3294 @{command primcorecursive}, @{command bnf}, @{command bnf_axiomatization}, and
  3295 @{command free_constructors}. For example:
  3296 \<close>
  3297 
  3298     datatype (plugins del: code "quickcheck") color = Red | Black
  3299 
  3300 text \<open>
  3301 Beyond the standard plugins, the \emph{Archive of Formal Proofs} includes a
  3302 \keyw{derive} command that derives class instances of datatypes
  3303 @{cite "sternagel-thiemann-2015"}.
  3304 \<close>
  3305 
  3306 subsection \<open>Code Generator
  3307   \label{ssec:code-generator}\<close>
  3308 
  3309 text \<open>
  3310 The \hthm{code} plugin registers freely generated types, including
  3311 (co)datatypes, and (co)recursive functions for code generation. No distinction
  3312 is made between datatypes and codatatypes. This means that for target languages
  3313 with a strict evaluation strategy (e.g., Standard ML), programs that attempt to
  3314 produce infinite codatatype values will not terminate.
  3315 
  3316 For types, the plugin derives the following properties:
  3317 
  3318 \begin{indentblock}
  3319 \begin{description}
  3320 
  3321 \item[@{text "t."}\hthm{eq.refl} @{text "[code nbe]"}\rm:] ~ \\
  3322 @{thm list.eq.refl[no_vars]}
  3323 
  3324 \item[@{text "t."}\hthm{eq.simps} @{text "[code]"}\rm:] ~ \\
  3325 @{thm list.eq.simps(1)[no_vars]} \\
  3326 @{thm list.eq.simps(2)[no_vars]} \\
  3327 @{thm list.eq.simps(3)[no_vars]} \\
  3328 @{thm list.eq.simps(4)[no_vars]} \\
  3329 @{thm list.eq.simps(5)[no_vars]} \\
  3330 @{thm list.eq.simps(6)[no_vars]}
  3331 
  3332 \end{description}
  3333 \end{indentblock}
  3334 
  3335 In addition, the plugin sets the @{text "[code]"} attribute on a number of
  3336 properties of freely generated types and of (co)recursive functions, as
  3337 documented in Sections \ref{ssec:datatype-generated-theorems},
  3338 \ref{ssec:primrec-generated-theorems}, \ref{ssec:codatatype-generated-theorems},
  3339 and~\ref{ssec:primcorec-generated-theorems}.
  3340 \<close>
  3341 
  3342 
  3343 subsection \<open>Size
  3344   \label{ssec:size}\<close>
  3345 
  3346 text \<open>
  3347 For each datatype @{text t}, the \hthm{size} plugin generates a generic size
  3348 function @{text "t.size_t"} as well as a specific instance
  3349 @{text "size :: t \<Rightarrow> nat"} belonging to the @{text size} type class. The
  3350 \keyw{fun} command relies on @{const size} to prove termination of recursive
  3351 functions on datatypes.
  3352 
  3353 The plugin derives the following properties:
  3354 
  3355 \begin{indentblock}
  3356 \begin{description}
  3357 
  3358 \item[@{text "t."}\hthm{size} @{text "[simp, code]"}\rm:] ~ \\
  3359 @{thm list.size(1)[no_vars]} \\
  3360 @{thm list.size(2)[no_vars]} \\
  3361 @{thm list.size(3)[no_vars]} \\
  3362 @{thm list.size(4)[no_vars]}
  3363 
  3364 \item[@{text "t."}\hthm{size_gen}\rm:] ~ \\
  3365 @{thm list.size_gen(1)[no_vars]} \\
  3366 @{thm list.size_gen(2)[no_vars]}
  3367 
  3368 \item[@{text "t."}\hthm{size_gen_o_map}\rm:] ~ \\
  3369 @{thm list.size_gen_o_map[no_vars]}
  3370 
  3371 \item[@{text "t."}\hthm{size_neq}\rm:] ~ \\
  3372 This property is missing for @{typ "'a list"}. If the @{term size} function
  3373 always evaluates to a non-zero value, this theorem has the form
  3374 @{prop "\<not> size x = 0"}.
  3375 
  3376 \end{description}
  3377 \end{indentblock}
  3378 
  3379 The @{text "t.size"} and @{text "t.size_t"} functions generated for datatypes
  3380 defined by nested recursion through a datatype @{text u} depend on
  3381 @{text "u.size_u"}.
  3382 
  3383 If the recursion is through a non-datatype @{text u} with type arguments
  3384 @{text "'a\<^sub>1, \<dots>, 'a\<^sub>m"}, by default @{text u} values are given a size of 0. This
  3385 can be improved upon by registering a custom size function of type
  3386 @{text "('a\<^sub>1 \<Rightarrow> nat) \<Rightarrow> \<dots> \<Rightarrow> ('a\<^sub>m \<Rightarrow> nat) \<Rightarrow> u \<Rightarrow> nat"} using
  3387 the ML function @{ML BNF_LFP_Size.register_size} or
  3388 @{ML BNF_LFP_Size.register_size_global}. See theory
  3389 \<^file>\<open>~~/src/HOL/Library/Multiset.thy\<close> for an example.
  3390 \<close>
  3391 
  3392 
  3393 subsection \<open>Transfer
  3394   \label{ssec:transfer}\<close>
  3395 
  3396 text \<open>
  3397 For each (co)datatype with live type arguments and each manually registered BNF,
  3398 the \hthm{transfer} plugin generates a predicator @{text "t.pred_t"} and
  3399 properties that guide the Transfer tool.
  3400 
  3401 For types with at least one live type argument and \emph{no dead type
  3402 arguments}, the plugin derives the following properties:
  3403 
  3404 \begin{indentblock}
  3405 \begin{description}
  3406 
  3407 \item[@{text "t."}\hthm{Domainp_rel} @{text "[relator_domain]"}\rm:] ~ \\
  3408 @{thm list.Domainp_rel[no_vars]}
  3409 
  3410 \item[@{text "t."}\hthm{left_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
  3411 @{thm list.left_total_rel[no_vars]}
  3412 
  3413 \item[@{text "t."}\hthm{left_unique_rel} @{text "[transfer_rule]"}\rm:] ~ \\
  3414 @{thm list.left_unique_rel[no_vars]}
  3415 
  3416 \item[@{text "t."}\hthm{right_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
  3417 @{thm list.right_total_rel[no_vars]}
  3418 
  3419 \item[@{text "t."}\hthm{right_unique_rel} @{text "[transfer_rule]"}\rm:] ~ \\
  3420 @{thm list.right_unique_rel[no_vars]}
  3421 
  3422 \item[@{text "t."}\hthm{bi_total_rel} @{text "[transfer_rule]"}\rm:] ~ \\
  3423 @{thm list.bi_total_rel[no_vars]}
  3424 
  3425 \item[@{text "t."}\hthm{bi_unique_rel} @{text "[transfer_rule]"}\rm:] ~ \\
  3426 @{thm list.bi_unique_rel[no_vars]}
  3427 
  3428 \end{description}
  3429 \end{indentblock}
  3430 
  3431 For (co)datatypes with at least one live type argument, the plugin sets the
  3432 @{text "[transfer_rule]"} attribute on the following (co)datatypes properties:
  3433 @{text "t.case_"}\allowbreak @{text "transfer"},
  3434 @{text "t.sel_"}\allowbreak @{text "transfer"},
  3435 @{text "t.ctr_"}\allowbreak @{text "transfer"},
  3436 @{text "t.disc_"}\allowbreak @{text "transfer"},
  3437 @{text "t.rec_"}\allowbreak @{text "transfer"}, and
  3438 @{text "t.corec_"}\allowbreak @{text "transfer"}.
  3439 For (co)datatypes that further have \emph{no dead type arguments}, the plugin
  3440 sets @{text "[transfer_rule]"} on
  3441 @{text "t.set_"}\allowbreak @{text "transfer"},
  3442 @{text "t.map_"}\allowbreak @{text "transfer"}, and
  3443 @{text "t.rel_"}\allowbreak @{text "transfer"}.
  3444 
  3445 For @{command primrec}, @{command primcorec}, and @{command primcorecursive},
  3446 the plugin implements the generation of the @{text "f.transfer"} property,
  3447 conditioned by the @{text transfer} option, and sets the
  3448 @{text "[transfer_rule]"} attribute on these.
  3449 \<close>
  3450 
  3451 
  3452 subsection \<open>Lifting
  3453   \label{ssec:lifting}\<close>
  3454 
  3455 text \<open>
  3456 For each (co)datatype and each manually registered BNF with at least one live
  3457 type argument \emph{and no dead type arguments}, the \hthm{lifting} plugin
  3458 generates properties and attributes that guide the Lifting tool.
  3459 
  3460 The plugin derives the following property:
  3461 
  3462 \begin{indentblock}
  3463 \begin{description}
  3464 
  3465 \item[@{text "t."}\hthm{Quotient} @{text "[quot_map]"}\rm:] ~ \\
  3466 @{thm list.Quotient[no_vars]}
  3467 
  3468 \end{description}
  3469 \end{indentblock}
  3470 
  3471 In addition, the plugin sets the @{text "[relator_eq]"} attribute on a
  3472 variant of the @{text t.rel_eq_onp} property, the @{text "[relator_mono]"}
  3473 attribute on @{text t.rel_mono}, and the @{text "[relator_distr]"} attribute
  3474 on @{text t.rel_compp}.
  3475 \<close>
  3476 
  3477 
  3478 subsection \<open>Quickcheck
  3479   \label{ssec:quickcheck}\<close>
  3480 
  3481 text \<open>
  3482 The integration of datatypes with Quickcheck is accomplished by the
  3483 \hthm{quick\-check} plugin. It combines a number of subplugins that instantiate
  3484 specific type classes. The subplugins can be enabled or disabled individually.
  3485 They are listed below:
  3486 
  3487 \begin{indentblock}
  3488 \hthm{quickcheck_random} \\
  3489 \hthm{quickcheck_exhaustive} \\
  3490 \hthm{quickcheck_bounded_forall} \\
  3491 \hthm{quickcheck_full_exhaustive} \\
  3492 \hthm{quickcheck_narrowing}
  3493 \end{indentblock}
  3494 \<close>
  3495 
  3496 
  3497 subsection \<open>Program Extraction
  3498   \label{ssec:program-extraction}\<close>
  3499 
  3500 text \<open>
  3501 The \hthm{extraction} plugin provides realizers for induction and case analysis,
  3502 to enable program extraction from proofs involving datatypes. This functionality
  3503 is only available with full proof objects, i.e., with the \emph{HOL-Proofs}
  3504 session.
  3505 \<close>
  3506 
  3507 
  3508 section \<open>Known Bugs and Limitations
  3509   \label{sec:known-bugs-and-limitations}\<close>
  3510 
  3511 text \<open>
  3512 This section lists the known bugs and limitations of the (co)datatype package at
  3513 the time of this writing.
  3514 
  3515 \begin{enumerate}
  3516 \setlength{\itemsep}{0pt}
  3517 
  3518 \item
  3519 \emph{Defining mutually (co)recursive (co)datatypes can be slow.} Fortunately,
  3520 it is always possible to recast mutual specifications to nested ones, which are
  3521 processed more efficiently.
  3522 
  3523 \item
  3524 \emph{Locally fixed types and terms cannot be used in type specifications.}
  3525 The limitation on types can be circumvented by adding type arguments to the local
  3526 (co)datatypes to abstract over the locally fixed types.
  3527 
  3528 \item
  3529 \emph{The \emph{\keyw{primcorec}} command does not allow user-specified names and
  3530 attributes next to the entered formulas.} The less convenient syntax, using the
  3531 \keyw{lemmas} command, is available as an alternative.
  3532 
  3533 \item
  3534 \emph{The \emph{\keyw{primcorec}} command does not allow corecursion under
  3535 @{text "case"}--@{text "of"} for datatypes that are defined without
  3536 discriminators and selectors.}
  3537 
  3538 \item
  3539 \emph{There is no way to use an overloaded constant from a syntactic type
  3540 class, such as @{text 0}, as a constructor.}
  3541 
  3542 \item
  3543 \emph{There is no way to register the same type as both a datatype and a
  3544 codatatype.} This affects types such as the extended natural numbers, for which
  3545 both views would make sense (for a different set of constructors).
  3546 
  3547 \item
  3548 \emph{The names of variables are often suboptimal in the properties generated by
  3549 the package.}
  3550 
  3551 \item
  3552 \emph{The compatibility layer sometimes produces induction principles with a
  3553 slightly different ordering of the premises than the old package.}
  3554 
  3555 \end{enumerate}
  3556 \<close>
  3557 
  3558 
  3559 text \<open>
  3560 \section*{Acknowledgment}
  3561 
  3562 Tobias Nipkow and Makarius Wenzel encouraged us to implement the new
  3563 (co)datatype package. Andreas Lochbihler provided lots of comments on earlier
  3564 versions of the package, especially on the coinductive part. Brian Huffman
  3565 suggested major simplifications to the internal constructions. Ond\v{r}ej
  3566 Kun\v{c}ar implemented the @{text transfer} and @{text lifting} plugins.
  3567 Christian Sternagel and Ren\'e Thiemann ported the \keyw{derive} command
  3568 from the \emph{Archive of Formal Proofs} to the new datatypes. Gerwin Klein and
  3569 Lars Noschinski implemented the @{command simps_of_case} and @{command
  3570 case_of_simps} commands. Florian Haftmann, Christian Urban, and Makarius
  3571 Wenzel provided general advice on Isabelle and package writing. Stefan Milius
  3572 and Lutz Schr\"oder found an elegant proof that eliminated one of the BNF
  3573 proof obligations. Mamoun Filali-Amine, Gerwin Klein, Andreas Lochbihler,
  3574 Tobias Nipkow, and Christian Sternagel suggested many textual improvements to
  3575 this tutorial.
  3576 \<close>
  3577 
  3578 end