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