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