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