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