src/Doc/Datatypes/Datatypes.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 56124 315cc3c0a19a
child 56644 efb39e0a89b0
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
     1
(*  Title:      Doc/Datatypes/Datatypes.thy
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
     2
    Author:     Jasmin Blanchette, TU Muenchen
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
     3
    Author:     Lorenz Panny, TU Muenchen
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
     4
    Author:     Andrei Popescu, TU Muenchen
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
     5
    Author:     Dmitriy Traytel, TU Muenchen
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
     6
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
     7
Tutorial for (co)datatype definitions with the new package.
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
     8
*)
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
     9
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    10
theory Datatypes
55073
9b96fb4c8cfd reduced dependencies + updated docs
blanchet
parents: 55029
diff changeset
    11
imports
9b96fb4c8cfd reduced dependencies + updated docs
blanchet
parents: 55029
diff changeset
    12
  Setup
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55073
diff changeset
    13
  "~~/src/HOL/Library/BNF_Decl"
55350
cf34abe28209 docs about registering a BNF
blanchet
parents: 55290
diff changeset
    14
  "~~/src/HOL/Library/Cardinal_Notations"
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
    15
  "~~/src/HOL/Library/FSet"
55073
9b96fb4c8cfd reduced dependencies + updated docs
blanchet
parents: 55029
diff changeset
    16
  "~~/src/HOL/Library/Simps_Case_Conv"
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    17
begin
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    18
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
    19
section {* Introduction
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
    20
  \label{sec:introduction} *}
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    21
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    22
text {*
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    23
The 2013 edition of Isabelle introduced a new definitional package for freely
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    24
generated datatypes and codatatypes. The datatype support is similar to that
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    25
provided by the earlier package due to Berghofer and Wenzel
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    26
\cite{Berghofer-Wenzel:1999:TPHOL}, documented in the Isar reference manual
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
    27
\cite{isabelle-isar-ref}; indeed, replacing the keyword \keyw{datatype} by
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    28
@{command datatype_new} is usually all that is needed to port existing theories
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    29
to use the new package.
52840
a0da63cec918 more (co)datatype documentation
blanchet
parents: 52829
diff changeset
    30
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
    31
Perhaps the main advantage of the new package is that it supports recursion
53619
27d2c98d9d9f more (co)data docs
blanchet
parents: 53617
diff changeset
    32
through a large class of non-datatypes, such as finite sets:
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    33
*}
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    34
53644
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
    35
    datatype_new 'a tree\<^sub>f\<^sub>s = Node\<^sub>f\<^sub>s (lbl\<^sub>f\<^sub>s: 'a) (sub\<^sub>f\<^sub>s: "'a tree\<^sub>f\<^sub>s fset")
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    36
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    37
text {*
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    38
\noindent
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
    39
Another strong point is the support for local definitions:
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    40
*}
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    41
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    42
    context linorder
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    43
    begin
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
    44
    datatype_new flag = Less | Eq | Greater
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    45
    end
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    46
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    47
text {*
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    48
\noindent
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    49
Furthermore, the package provides a lot of convenience, including automatically
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    50
generated discriminators, selectors, and relators as well as a wealth of
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    51
properties about them.
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    52
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    53
In addition to inductive datatypes, the new package supports coinductive
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    54
datatypes, or \emph{codatatypes}, which allow infinite values. For example, the
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    55
following command introduces the type of lazy lists, which comprises both finite
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    56
and infinite values:
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    57
*}
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    58
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
    59
(*<*)
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
    60
    locale early
54072
7bee26d970f0 more primcorec docs
blanchet
parents: 54071
diff changeset
    61
    locale late
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
    62
(*>*)
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
    63
    codatatype (*<*)(in early) (*>*)'a llist = LNil | LCons 'a "'a llist"
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    64
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    65
text {*
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    66
\noindent
52840
a0da63cec918 more (co)datatype documentation
blanchet
parents: 52829
diff changeset
    67
Mixed inductive--coinductive recursion is possible via nesting. Compare the
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
    68
following four Rose tree examples:
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    69
*}
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    70
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
    71
    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
    72
    datatype_new (*<*)(in early) (*>*)'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
    73
    codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
    74
    codatatype (*<*)(in early) (*>*)'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    75
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    76
text {*
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    77
The first two tree types allow only paths of finite length, whereas the last two
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    78
allow infinite paths. Orthogonally, the nodes in the first and third types have
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    79
finitely many direct subtrees, whereas those of the second and fourth may have
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
    80
infinite branching.
52840
a0da63cec918 more (co)datatype documentation
blanchet
parents: 52829
diff changeset
    81
55073
9b96fb4c8cfd reduced dependencies + updated docs
blanchet
parents: 55029
diff changeset
    82
The package is part of @{theory Main}. Additional functionality is provided by
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
    83
the theory @{theory BNF_Decl}, located in the directory
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
    84
\verb|~~/src/HOL/Library|.
55073
9b96fb4c8cfd reduced dependencies + updated docs
blanchet
parents: 55029
diff changeset
    85
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    86
The package, like its predecessor, fully adheres to the LCF philosophy
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    87
\cite{mgordon79}: The characteristic theorems associated with the specified
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    88
(co)datatypes are derived rather than introduced axiomatically.%
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
    89
\footnote{If the @{text quick_and_dirty} option is enabled, some of the
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
    90
internal constructions and most of the internal proof obligations are skipped.}
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    91
The package's metatheory is described in a pair of papers
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
    92
\cite{traytel-et-al-2012,blanchette-et-al-wit}. The central notion is that of a
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
    93
\emph{bounded natural functor} (BNF)---a well-behaved type constructor for which
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
    94
nested (co)recursion is supported.
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
    95
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    96
This tutorial is organized as follows:
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
    97
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
    98
\begin{itemize}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
    99
\setlength{\itemsep}{0pt}
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   100
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   101
\item Section \ref{sec:defining-datatypes}, ``Defining Datatypes,''
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   102
describes how to specify datatypes using the @{command datatype_new} command.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   103
53018
11ebef554439 added rail diagram
blanchet
parents: 52969
diff changeset
   104
\item Section \ref{sec:defining-recursive-functions}, ``Defining Recursive
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   105
Functions,'' describes how to specify recursive functions using
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
   106
@{command primrec}, \keyw{fun}, and \keyw{function}.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   107
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   108
\item Section \ref{sec:defining-codatatypes}, ``Defining Codatatypes,''
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   109
describes how to specify codatatypes using the @{command codatatype} command.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   110
53018
11ebef554439 added rail diagram
blanchet
parents: 52969
diff changeset
   111
\item Section \ref{sec:defining-corecursive-functions}, ``Defining Corecursive
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   112
Functions,'' describes how to specify corecursive functions using the
53826
92a8ae172242 use "primcorec" in doc
blanchet
parents: 53822
diff changeset
   113
@{command primcorec} and @{command primcorecursive} commands.
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   114
55351
blanchet
parents: 55350
diff changeset
   115
\item Section \ref{sec:introducing-bounded-natural-functors}, ``Introducing
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   116
Bounded Natural Functors,'' explains how to use the @{command bnf} command
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   117
to register arbitrary type constructors as BNFs.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   118
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   119
\item Section
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   120
\ref{sec:deriving-destructors-and-theorems-for-free-constructors},
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   121
``Deriving Destructors and Theorems for Free Constructors,'' explains how to
55468
98b25c51e9e5 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents: 55460
diff changeset
   122
use the command @{command free_constructors} to derive destructor constants
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   123
and theorems for freely generated types, as performed internally by @{command
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   124
datatype_new} and @{command codatatype}.
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   125
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   126
%\item Section \ref{sec:standard-ml-interface}, ``Standard ML Interface,''
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   127
%describes the package's programmatic interface.
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   128
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   129
%\item Section \ref{sec:interoperability}, ``Interoperability,''
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   130
%is concerned with the packages' interaction with other Isabelle packages and
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   131
%tools, such as the code generator and the counterexample generators.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   132
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   133
%\item Section \ref{sec:known-bugs-and-limitations}, ``Known Bugs and
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   134
%Limitations,'' concludes with known open issues at the time of writing.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   135
\end{itemize}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   136
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   137
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   138
\newbox\boxA
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   139
\setbox\boxA=\hbox{\texttt{NOSPAM}}
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   140
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   141
\newcommand\authoremaili{\texttt{blan{\color{white}NOSPAM}\kern-\wd\boxA{}chette@\allowbreak
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   142
in.\allowbreak tum.\allowbreak de}}
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   143
\newcommand\authoremailii{\texttt{lore{\color{white}NOSPAM}\kern-\wd\boxA{}nz.panny@\allowbreak
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   144
\allowbreak tum.\allowbreak de}}
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   145
\newcommand\authoremailiii{\texttt{pope{\color{white}NOSPAM}\kern-\wd\boxA{}scua@\allowbreak
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   146
in.\allowbreak tum.\allowbreak de}}
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   147
\newcommand\authoremailiv{\texttt{tray{\color{white}NOSPAM}\kern-\wd\boxA{}tel@\allowbreak
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   148
in.\allowbreak tum.\allowbreak de}}
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   149
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
   150
The command @{command datatype_new} is expected to replace \keyw{datatype} in a
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
   151
future release. Authors of new theories are encouraged to use the new commands,
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
   152
and maintainers of older theories may want to consider upgrading.
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   153
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   154
Comments and bug reports concerning either the tool or this tutorial should be
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   155
directed to the authors at \authoremaili, \authoremailii, \authoremailiii,
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   156
and \authoremailiv.
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   157
*}
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   158
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   159
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   160
section {* Defining Datatypes
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   161
  \label{sec:defining-datatypes} *}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   162
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   163
text {*
53646
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
   164
Datatypes can be specified using the @{command datatype_new} command.
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   165
*}
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
   166
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   167
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   168
subsection {* Introductory Examples
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   169
  \label{ssec:datatype-introductory-examples} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   170
53646
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
   171
text {*
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
   172
Datatypes are illustrated through concrete examples featuring different flavors
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
   173
of recursion. More examples can be found in the directory
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   174
\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
53646
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
   175
*}
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   176
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   177
subsubsection {* Nonrecursive Types
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   178
  \label{sssec:datatype-nonrecursive-types} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   179
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   180
text {*
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   181
Datatypes are introduced by specifying the desired names and argument types for
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   182
their constructors. \emph{Enumeration} types are the simplest form of datatype.
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   183
All their constructors are nullary:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   184
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   185
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   186
    datatype_new trool = Truue | Faalse | Perhaaps
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   187
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   188
text {*
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   189
\noindent
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   190
Here, @{const Truue}, @{const Faalse}, and @{const Perhaaps} have the type @{typ trool}.
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   191
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   192
Polymorphic types are possible, such as the following option type, modeled after
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   193
its homologue from the @{theory Option} theory:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   194
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   195
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   196
(*<*)
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   197
    hide_const None Some
54958
4933165fd112 do not use wrong constructor in auto-generated proof goal
panny
parents: 54955
diff changeset
   198
    hide_type option
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   199
(*>*)
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   200
    datatype_new 'a option = None | Some 'a
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   201
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   202
text {*
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   203
\noindent
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   204
The constructors are @{text "None :: 'a option"} and
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   205
@{text "Some :: 'a \<Rightarrow> 'a option"}.
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   206
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   207
The next example has three type parameters:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   208
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   209
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   210
    datatype_new ('a, 'b, 'c) triple = Triple 'a 'b 'c
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   211
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   212
text {*
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   213
\noindent
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   214
The constructor is
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   215
@{text "Triple :: 'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> ('a, 'b, 'c) triple"}.
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   216
Unlike in Standard ML, curried constructors are supported. The uncurried variant
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   217
is also possible:
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   218
*}
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   219
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   220
    datatype_new ('a, 'b, 'c) triple\<^sub>u = Triple\<^sub>u "'a * 'b * 'c"
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
   221
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   222
text {*
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   223
\noindent
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   224
Occurrences of nonatomic types on the right-hand side of the equal sign must be
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   225
enclosed in double quotes, as is customary in Isabelle.
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   226
*}
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   227
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   228
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   229
subsubsection {* Simple Recursion
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   230
  \label{sssec:datatype-simple-recursion} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   231
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   232
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   233
Natural numbers are the simplest example of a recursive type:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   234
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   235
53332
c97a05a26dd6 Doc improvements
traytel
parents: 53331
diff changeset
   236
    datatype_new nat = Zero | Suc nat
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   237
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   238
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   239
\noindent
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   240
Lists were shown in the introduction. Terminated lists are a variant that
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   241
stores a value of type @{typ 'b} at the very end:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   242
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   243
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   244
    datatype_new (*<*)(in early) (*>*)('a, 'b) tlist = TNil 'b | TCons 'a "('a, 'b) tlist"
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   245
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   246
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   247
subsubsection {* Mutual Recursion
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   248
  \label{sssec:datatype-mutual-recursion} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   249
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   250
text {*
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   251
\emph{Mutually recursive} types are introduced simultaneously and may refer to
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   252
each other. The example below introduces a pair of types for even and odd
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   253
natural numbers:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   254
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   255
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   256
    datatype_new even_nat = Even_Zero | Even_Suc odd_nat
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   257
    and odd_nat = Odd_Suc even_nat
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   258
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   259
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   260
\noindent
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   261
Arithmetic expressions are defined via terms, terms via factors, and factors via
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   262
expressions:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   263
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   264
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   265
    datatype_new ('a, 'b) exp =
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   266
      Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   267
    and ('a, 'b) trm =
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   268
      Factor "('a, 'b) fct" | Prod "('a, 'b) fct" "('a, 'b) trm"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   269
    and ('a, 'b) fct =
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   270
      Const 'a | Var 'b | Expr "('a, 'b) exp"
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   271
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   272
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   273
subsubsection {* Nested Recursion
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   274
  \label{sssec:datatype-nested-recursion} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   275
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   276
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   277
\emph{Nested recursion} occurs when recursive occurrences of a type appear under
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   278
a type constructor. The introduction showed some examples of trees with nesting
53675
d4a4b32038eb more (co)data docs
blanchet
parents: 53654
diff changeset
   279
through lists. A more complex example, that reuses our @{type option} type,
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   280
follows:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   281
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   282
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
   283
    datatype_new 'a btree =
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   284
      BNode 'a "'a btree option" "'a btree option"
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   285
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   286
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   287
\noindent
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   288
Not all nestings are admissible. For example, this command will fail:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   289
*}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   290
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   291
    datatype_new 'a wrong = W1 | W2 (*<*)'a
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   292
    typ (*>*)"'a wrong \<Rightarrow> 'a"
52806
146ce45c3619 more work on (co)datatype docs
blanchet
parents: 52805
diff changeset
   293
146ce45c3619 more work on (co)datatype docs
blanchet
parents: 52805
diff changeset
   294
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   295
\noindent
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   296
The issue is that the function arrow @{text "\<Rightarrow>"} allows recursion
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   297
only through its right-hand side. This issue is inherited by polymorphic
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   298
datatypes defined in terms of~@{text "\<Rightarrow>"}:
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   299
*}
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   300
55350
cf34abe28209 docs about registering a BNF
blanchet
parents: 55290
diff changeset
   301
    datatype_new ('a, 'b) fun_copy = Fun "'a \<Rightarrow> 'b"
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   302
    datatype_new 'a also_wrong = W1 | W2 (*<*)'a
55350
cf34abe28209 docs about registering a BNF
blanchet
parents: 55290
diff changeset
   303
    typ (*>*)"('a also_wrong, 'a) fun_copy"
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   304
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   305
text {*
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   306
\noindent
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   307
The following definition of @{typ 'a}-branching trees is legal:
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   308
*}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   309
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   310
    datatype_new 'a ftree = FTLeaf 'a | FTNode "'a \<Rightarrow> 'a ftree"
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   311
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   312
text {*
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   313
\noindent
55129
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   314
And so is the definition of hereditarily finite sets:
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   315
*}
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   316
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   317
    datatype_new hfset = HFSet "hfset fset"
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   318
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   319
text {*
26bd1cba3ab5 killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents: 55114
diff changeset
   320
\noindent
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   321
In general, type constructors @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   322
allow recursion on a subset of their type arguments @{text 'a\<^sub>1}, \ldots,
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   323
@{text 'a\<^sub>m}. These type arguments are called \emph{live}; the remaining
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   324
type arguments are called \emph{dead}. In @{typ "'a \<Rightarrow> 'b"} and
55350
cf34abe28209 docs about registering a BNF
blanchet
parents: 55290
diff changeset
   325
@{typ "('a, 'b) fun_copy"}, the type variable @{typ 'a} is dead and
cf34abe28209 docs about registering a BNF
blanchet
parents: 55290
diff changeset
   326
@{typ 'b} is live.
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   327
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   328
Type constructors must be registered as BNFs to have live arguments. This is
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   329
done automatically for datatypes and codatatypes introduced by the @{command
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   330
datatype_new} and @{command codatatype} commands.
55351
blanchet
parents: 55350
diff changeset
   331
Section~\ref{sec:introducing-bounded-natural-functors} explains how to
blanchet
parents: 55350
diff changeset
   332
register arbitrary type constructors as BNFs.
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   333
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   334
Here is another example that fails:
52806
146ce45c3619 more work on (co)datatype docs
blanchet
parents: 52805
diff changeset
   335
*}
146ce45c3619 more work on (co)datatype docs
blanchet
parents: 52805
diff changeset
   336
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   337
    datatype_new 'a pow_list = PNil 'a (*<*)'a
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   338
    datatype_new 'a pow_list' = PNil' 'a (*>*)| PCons "('a * 'a) pow_list"
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   339
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   340
text {*
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   341
\noindent
55351
blanchet
parents: 55350
diff changeset
   342
This attempted definition features a different flavor of nesting, where the
blanchet
parents: 55350
diff changeset
   343
recursive call in the type specification occurs around (rather than inside)
blanchet
parents: 55350
diff changeset
   344
another type constructor.
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   345
*}
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   346
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   347
subsubsection {* Auxiliary Constants and Properties
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   348
  \label{sssec:datatype-auxiliary-constants-and-properties} *}
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   349
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   350
text {*
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   351
The @{command datatype_new} command introduces various constants in addition to
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   352
the constructors. With each datatype are associated set functions, a map
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   353
function, a relator, discriminators, and selectors, all of which can be given
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   354
custom names. In the example below, the familiar names @{text null}, @{text hd},
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   355
@{text tl}, @{text set}, @{text map}, and @{text list_all2}, override the
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   356
default names @{text is_Nil}, @{text un_Cons1}, @{text un_Cons2},
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   357
@{text set_list}, @{text map_list}, and @{text rel_list}:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   358
*}
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   359
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   360
(*<*)
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   361
    no_translations
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   362
      "[x, xs]" == "x # [xs]"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   363
      "[x]" == "x # []"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   364
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   365
    no_notation
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   366
      Nil ("[]") and
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   367
      Cons (infixr "#" 65)
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   368
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   369
    hide_type list
54494
a220071f6708 updated docs
blanchet
parents: 54491
diff changeset
   370
    hide_const Nil Cons hd tl set map list_all2
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   371
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   372
    context early begin
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   373
(*>*)
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   374
    datatype_new (set: 'a) list (map: map rel: list_all2) =
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   375
      null: Nil (defaults tl: Nil)
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   376
    | Cons (hd: 'a) (tl: "'a list")
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   377
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   378
text {*
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   379
\noindent
55353
blanchet
parents: 55351
diff changeset
   380
The types of the constants that appear in the specification are listed below.
55351
blanchet
parents: 55350
diff changeset
   381
blanchet
parents: 55350
diff changeset
   382
\medskip
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   383
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   384
\begin{tabular}{@ {}ll@ {}}
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   385
Constructors: &
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   386
  @{text "Nil \<Colon> 'a list"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   387
&
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   388
  @{text "Cons \<Colon> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   389
Discriminator: &
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   390
  @{text "null \<Colon> 'a list \<Rightarrow> bool"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   391
Selectors: &
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   392
  @{text "hd \<Colon> 'a list \<Rightarrow> 'a"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   393
&
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   394
  @{text "tl \<Colon> 'a list \<Rightarrow> 'a list"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   395
Set function: &
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   396
  @{text "set \<Colon> 'a list \<Rightarrow> 'a set"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   397
Map function: &
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   398
  @{text "map \<Colon> ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   399
Relator: &
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   400
  @{text "list_all2 \<Colon> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"}
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   401
\end{tabular}
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   402
55351
blanchet
parents: 55350
diff changeset
   403
\medskip
blanchet
parents: 55350
diff changeset
   404
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   405
The discriminator @{const null} and the selectors @{const hd} and @{const tl}
55351
blanchet
parents: 55350
diff changeset
   406
are characterized by the following conditional equations:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   407
%
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   408
\[@{thm list.collapse(1)[of xs, no_vars]}
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   409
  \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   410
%
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   411
For two-constructor datatypes, a single discriminator constant is sufficient.
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   412
The discriminator associated with @{const Cons} is simply
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   413
@{term "\<lambda>xs. \<not> null xs"}.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   414
53553
d4191bf88529 avoid a keyword
blanchet
parents: 53552
diff changeset
   415
The @{text defaults} clause following the @{const Nil} constructor specifies a
d4191bf88529 avoid a keyword
blanchet
parents: 53552
diff changeset
   416
default value for selectors associated with other constructors. Here, it is used
d4191bf88529 avoid a keyword
blanchet
parents: 53552
diff changeset
   417
to ensure that the tail of the empty list is itself (instead of being left
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   418
unspecified).
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   419
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   420
Because @{const Nil} is nullary, it is also possible to use
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   421
@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is specified by
53534
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   422
entering ``@{text "="}'' instead of the identifier @{const null}. Although this
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   423
may look appealing, the mixture of constructors and selectors in the
53534
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   424
characteristic theorems can lead Isabelle's automation to switch between the
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   425
constructor and the destructor view in surprising ways.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   426
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   427
The usual mixfix syntax annotations are available for both types and
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   428
constructors. For example:
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
   429
*}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   430
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   431
(*<*)
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   432
    end
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   433
(*>*)
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   434
    datatype_new ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   435
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   436
text {* \blankline *}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   437
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   438
    datatype_new (set: 'a) list (map: map rel: list_all2) =
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   439
      null: Nil ("[]")
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   440
    | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   441
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   442
text {*
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   443
\noindent
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   444
Incidentally, this is how the traditional syntax can be set up:
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   445
*}
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   446
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   447
    syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   448
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   449
text {* \blankline *}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   450
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   451
    translations
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   452
      "[x, xs]" == "x # [xs]"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   453
      "[x]" == "x # []"
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   454
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   455
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   456
subsection {* Command Syntax
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   457
  \label{ssec:datatype-command-syntax} *}
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   458
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   459
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   460
subsubsection {* \keyw{datatype\_new}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   461
  \label{sssec:datatype-new} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   462
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   463
text {*
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   464
\begin{matharray}{rcl}
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   465
  @{command_def "datatype_new"} & : & @{text "local_theory \<rightarrow> local_theory"}
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   466
\end{matharray}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   467
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   468
@{rail \<open>
55029
61a6bf7d4b02 clarified @{rail} syntax: prefer explicit \<newline> symbol;
wenzelm
parents: 54958
diff changeset
   469
  @@{command datatype_new} target? @{syntax dt_options}? \<newline>
55472
990651bfc65b updated docs to reflect the new 'free_constructors' syntax
blanchet
parents: 55468
diff changeset
   470
    (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') + @'and')
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   471
  ;
55410
54b09e82b9e1 killed 'rep_compat' option
blanchet
parents: 55398
diff changeset
   472
  @{syntax_def dt_options}: '(' (('no_discs_sels' | 'no_code') + ',') ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   473
\<close>}
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   474
55351
blanchet
parents: 55350
diff changeset
   475
\medskip
blanchet
parents: 55350
diff changeset
   476
blanchet
parents: 55350
diff changeset
   477
\noindent
55460
3f4efd7d950d added a bit of documentation for the different commands
blanchet
parents: 55459
diff changeset
   478
The @{command datatype_new} command introduces a set of mutually recursive
3f4efd7d950d added a bit of documentation for the different commands
blanchet
parents: 55459
diff changeset
   479
datatypes specified by their constructors.
3f4efd7d950d added a bit of documentation for the different commands
blanchet
parents: 55459
diff changeset
   480
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   481
The syntactic entity \synt{target} can be used to specify a local
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   482
context---e.g., @{text "(in linorder)"} \cite{isabelle-isar-ref}.
55460
3f4efd7d950d added a bit of documentation for the different commands
blanchet
parents: 55459
diff changeset
   483
56124
315cc3c0a19a tuned wording (pun)
blanchet
parents: 56123
diff changeset
   484
The optional target is optionally followed by one or both of the following
315cc3c0a19a tuned wording (pun)
blanchet
parents: 56123
diff changeset
   485
options:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   486
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   487
\begin{itemize}
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   488
\setlength{\itemsep}{0pt}
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   489
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   490
\item
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   491
The @{text "no_discs_sels"} option indicates that no discriminators or selectors
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   492
should be generated.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   493
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   494
\item
54626
8a5e82425e55 added 'no_code' option
blanchet
parents: 54624
diff changeset
   495
The @{text "no_code"} option indicates that the datatype should not be
8a5e82425e55 added 'no_code' option
blanchet
parents: 54624
diff changeset
   496
registered for code generation.
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   497
\end{itemize}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   498
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   499
The left-hand sides of the datatype equations specify the name of the type to
53534
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   500
define, its type parameters, and additional information:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   501
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   502
@{rail \<open>
53534
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   503
  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   504
  ;
55705
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   505
  @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   506
  ;
53534
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   507
  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   508
\<close>}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   509
55351
blanchet
parents: 55350
diff changeset
   510
\medskip
blanchet
parents: 55350
diff changeset
   511
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   512
\noindent
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   513
The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   514
the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   515
variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   516
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   517
The optional names preceding the type variables allow to override the default
55705
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   518
names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   519
arguments can be marked as dead by entering ``-'' (hyphen) instead of an
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   520
identifier for the corresponding set function; otherwise, they are live or dead
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   521
(and a set function is generated or not) depending on where they occur in the
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   522
right-hand sides of the definition. Declaring a type argument as dead can speed
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   523
up the type definition but will prevent any later (co)recursion through that
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   524
type argument.
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   525
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   526
Inside a mutually recursive specification, all defined datatypes must
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   527
mention exactly the same type variables in the same order.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   528
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   529
@{rail \<open>
55472
990651bfc65b updated docs to reflect the new 'free_constructors' syntax
blanchet
parents: 55468
diff changeset
   530
  @{syntax_def dt_ctor}: (name ':')? name (@{syntax dt_ctor_arg} * ) \<newline>
53534
de2027f9aff3 more (co)datatype documentation
blanchet
parents: 53491
diff changeset
   531
    @{syntax dt_sel_defaults}? mixfix?
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   532
\<close>}
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   533
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   534
\medskip
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   535
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   536
\noindent
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   537
The main constituents of a constructor specification are the name of the
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   538
constructor and the list of its argument types. An optional discriminator name
53554
78fe0002024d more (co)data docs
blanchet
parents: 53553
diff changeset
   539
can be supplied at the front to override the default name
78fe0002024d more (co)data docs
blanchet
parents: 53553
diff changeset
   540
(@{text t.is_C\<^sub>j}).
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   541
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   542
@{rail \<open>
55472
990651bfc65b updated docs to reflect the new 'free_constructors' syntax
blanchet
parents: 55468
diff changeset
   543
  @{syntax_def dt_ctor_arg}: type | '(' name ':' type ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   544
\<close>}
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   545
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   546
\medskip
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   547
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   548
\noindent
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   549
The syntactic entity \synt{type} denotes a HOL type \cite{isabelle-isar-ref}.
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   550
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   551
In addition to the type of a constructor argument, it is possible to specify a
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   552
name for the corresponding selector to override the default name
53554
78fe0002024d more (co)data docs
blanchet
parents: 53553
diff changeset
   553
(@{text un_C\<^sub>ji}). The same selector names can be reused for several
78fe0002024d more (co)data docs
blanchet
parents: 53553
diff changeset
   554
constructors as long as they share the same type.
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   555
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   556
@{rail \<open>
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   557
  @{syntax_def dt_sel_defaults}: '(' 'defaults' (name ':' term +) ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   558
\<close>}
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   559
55351
blanchet
parents: 55350
diff changeset
   560
\medskip
blanchet
parents: 55350
diff changeset
   561
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   562
\noindent
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   563
Given a constructor
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   564
@{text "C \<Colon> \<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<sigma>"},
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   565
default values can be specified for any selector
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   566
@{text "un_D \<Colon> \<sigma> \<Rightarrow> \<tau>"}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   567
associated with other constructors. The specified default value must be of type
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   568
@{text "\<sigma>\<^sub>1 \<Rightarrow> \<dots> \<Rightarrow> \<sigma>\<^sub>p \<Rightarrow> \<tau>"}
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   569
(i.e., it may depend on @{text C}'s arguments).
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   570
*}
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   571
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   572
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   573
subsubsection {* \keyw{datatype\_new\_compat}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   574
  \label{sssec:datatype-new-compat} *}
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   575
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   576
text {*
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   577
\begin{matharray}{rcl}
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   578
  @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   579
\end{matharray}
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   580
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   581
@{rail \<open>
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   582
  @@{command datatype_compat} (name +)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   583
\<close>}
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   584
55351
blanchet
parents: 55350
diff changeset
   585
\medskip
blanchet
parents: 55350
diff changeset
   586
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   587
\noindent
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   588
The @{command datatype_compat} command registers new-style datatypes as
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   589
old-style datatypes. For example:
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   590
*}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   591
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   592
    datatype_compat even_nat odd_nat
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   593
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   594
text {* \blankline *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   595
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   596
    thm even_nat_odd_nat.size
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   597
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   598
text {* \blankline *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   599
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   600
    ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   601
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   602
text {*
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   603
The syntactic entity \synt{name} denotes an identifier \cite{isabelle-isar-ref}.
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   604
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   605
The command is interesting because the old datatype package provides some
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   606
functionality that is not yet replicated in the new package:
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   607
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   608
\begin{itemize}
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   609
\setlength{\itemsep}{0pt}
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   610
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   611
\item It is integrated with \keyw{fun} \cite{isabelle-function},
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   612
Nitpick \cite{isabelle-nitpick}, Quickcheck, and other packages.
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   613
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   614
\item It is extended by various add-ons, notably to produce instances of the
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   615
@{const size} function.
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   616
\end{itemize}
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   617
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   618
A few remarks concern nested recursive datatypes:
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   619
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   620
\begin{itemize}
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   621
\setlength{\itemsep}{0pt}
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   622
55871
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55705
diff changeset
   623
\item The old-style, nested-as-mutual induction rule and recursor theorems are
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55705
diff changeset
   624
generated under their usual names but with ``@{text "compat_"}'' prefixed
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55705
diff changeset
   625
(e.g., @{text compat_tree.induct}).
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   626
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   627
\item All types through which recursion takes place must be new-style datatypes
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   628
or the function type. In principle, it should be possible to support old-style
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   629
datatypes as well, but this has not been implemented yet (and there is currently
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   630
no way to register old-style datatypes as new-style datatypes).
54184
3fe73f3c84a2 more docs
blanchet
parents: 54183
diff changeset
   631
3fe73f3c84a2 more docs
blanchet
parents: 54183
diff changeset
   632
\item The recursor produced for types that recurse through functions has a
3fe73f3c84a2 more docs
blanchet
parents: 54183
diff changeset
   633
different signature than with the old package. This makes it impossible to use
3fe73f3c84a2 more docs
blanchet
parents: 54183
diff changeset
   634
the old \keyw{primrec} command.
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   635
\end{itemize}
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   636
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   637
An alternative to @{command datatype_compat} is to use the old package's
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   638
\keyw{rep\_datatype} command. The associated proof obligations must then be
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   639
discharged manually.
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   640
*}
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   641
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   642
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   643
subsection {* Generated Constants
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   644
  \label{ssec:datatype-generated-constants} *}
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   645
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   646
text {*
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   647
Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   648
with $m > 0$ live type variables and $n$ constructors
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   649
@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   650
following auxiliary constants are introduced:
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   651
55353
blanchet
parents: 55351
diff changeset
   652
\medskip
blanchet
parents: 55351
diff changeset
   653
blanchet
parents: 55351
diff changeset
   654
\begin{tabular}{@ {}ll@ {}}
blanchet
parents: 55351
diff changeset
   655
Case combinator: &
blanchet
parents: 55351
diff changeset
   656
  @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
blanchet
parents: 55351
diff changeset
   657
Discriminators: &
blanchet
parents: 55351
diff changeset
   658
  @{text "t.is_C\<^sub>1"}$, \ldots, $@{text "t.is_C\<^sub>n"} \\
blanchet
parents: 55351
diff changeset
   659
Selectors: &
blanchet
parents: 55351
diff changeset
   660
  @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
blanchet
parents: 55351
diff changeset
   661
& \quad\vdots \\
blanchet
parents: 55351
diff changeset
   662
& @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
blanchet
parents: 55351
diff changeset
   663
Set functions: &
blanchet
parents: 55351
diff changeset
   664
  @{text set1_t}, \ldots, @{text t.setm_t} \\
blanchet
parents: 55351
diff changeset
   665
Map function: &
blanchet
parents: 55351
diff changeset
   666
  @{text t.map_t} \\
blanchet
parents: 55351
diff changeset
   667
Relator: &
blanchet
parents: 55351
diff changeset
   668
  @{text t.rel_t} \\
blanchet
parents: 55351
diff changeset
   669
Recursor: &
blanchet
parents: 55351
diff changeset
   670
  @{text t.rec_t}
blanchet
parents: 55351
diff changeset
   671
\end{tabular}
blanchet
parents: 55351
diff changeset
   672
blanchet
parents: 55351
diff changeset
   673
\medskip
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   674
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   675
\noindent
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   676
The case combinator, discriminators, and selectors are collectively called
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   677
\emph{destructors}. The prefix ``@{text "t."}'' is an optional component of the
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   678
names and is normally hidden.
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   679
*}
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   680
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   681
52840
a0da63cec918 more (co)datatype documentation
blanchet
parents: 52829
diff changeset
   682
subsection {* Generated Theorems
a0da63cec918 more (co)datatype documentation
blanchet
parents: 52829
diff changeset
   683
  \label{ssec:datatype-generated-theorems} *}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   684
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   685
text {*
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   686
The characteristic theorems generated by @{command datatype_new} are grouped in
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   687
three broad categories:
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   688
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   689
\begin{itemize}
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   690
\setlength{\itemsep}{0pt}
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   691
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   692
\item The \emph{free constructor theorems} are properties about the constructors
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   693
and destructors that can be derived for any freely generated type. Internally,
55468
98b25c51e9e5 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents: 55460
diff changeset
   694
the derivation is performed by @{command free_constructors}.
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   695
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   696
\item The \emph{functorial theorems} are properties of datatypes related to
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   697
their BNF nature.
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   698
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   699
\item The \emph{inductive theorems} are properties of datatypes related to
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   700
their inductive nature.
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   701
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   702
\end{itemize}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   703
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   704
\noindent
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   705
The full list of named theorems can be obtained as usual by entering the
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   706
command \keyw{print\_theorems} immediately after the datatype definition.
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   707
This list normally excludes low-level theorems that reveal internal
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   708
constructions. To make these accessible, add the line
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   709
*}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   710
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   711
    declare [[bnf_note_all]]
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   712
(*<*)
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   713
    declare [[bnf_note_all = false]]
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   714
(*>*)
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   715
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   716
text {*
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   717
\noindent
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   718
to the top of the theory file.
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   719
*}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   720
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   721
subsubsection {* Free Constructor Theorems
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   722
  \label{sssec:free-constructor-theorems} *}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   723
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   724
(*<*)
53837
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   725
    consts nonnull :: 'a
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   726
(*>*)
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   727
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   728
text {*
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   729
The free constructor theorems are partitioned in three subgroups. The first
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   730
subgroup of properties is concerned with the constructors. They are listed below
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   731
for @{typ "'a list"}:
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   732
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   733
\begin{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   734
\begin{description}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   735
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   736
\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   737
@{thm list.inject[no_vars]}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   738
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   739
\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   740
@{thm list.distinct(1)[no_vars]} \\
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   741
@{thm list.distinct(2)[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   742
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   743
\item[@{text "t."}\hthm{exhaust} @{text "[cases t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   744
@{thm list.exhaust[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   745
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   746
\item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   747
@{thm list.nchotomy[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   748
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   749
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   750
\end{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   751
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   752
\noindent
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   753
In addition, these nameless theorems are registered as safe elimination rules:
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   754
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   755
\begin{indentblock}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   756
\begin{description}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   757
54386
3514fdfdf59b minor doc fix
blanchet
parents: 54287
diff changeset
   758
\item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   759
@{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   760
@{thm list.distinct(2)[THEN notE, elim!, no_vars]}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   761
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   762
\end{description}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   763
\end{indentblock}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   764
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   765
\noindent
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   766
The next subgroup is concerned with the case combinator:
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   767
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   768
\begin{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   769
\begin{description}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   770
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   771
\item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   772
@{thm list.case(1)[no_vars]} \\
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   773
@{thm list.case(2)[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   774
55398
67e9fdd9ae9e updated docs
blanchet
parents: 55355
diff changeset
   775
\item[@{text "t."}\hthm{case\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   776
@{thm list.case_cong[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   777
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   778
\item[@{text "t."}\hthm{weak\_case\_cong} @{text "[cong]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   779
@{thm list.weak_case_cong[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   780
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   781
\item[@{text "t."}\hthm{split}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   782
@{thm list.split[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   783
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   784
\item[@{text "t."}\hthm{split\_asm}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   785
@{thm list.split_asm[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   786
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   787
\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   788
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   789
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   790
\end{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   791
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   792
\noindent
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   793
The third subgroup revolves around discriminators and selectors:
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   794
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   795
\begin{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   796
\begin{description}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   797
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   798
\item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   799
@{thm list.disc(1)[no_vars]} \\
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   800
@{thm list.disc(2)[no_vars]}
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   801
53703
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   802
\item[@{text "t."}\hthm{discI}\rm:] ~ \\
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   803
@{thm list.discI(1)[no_vars]} \\
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   804
@{thm list.discI(2)[no_vars]}
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   805
53805
4163160853fd added [code] to selectors
blanchet
parents: 53798
diff changeset
   806
\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   807
@{thm list.sel(1)[no_vars]} \\
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   808
@{thm list.sel(2)[no_vars]}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   809
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   810
\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   811
@{thm list.collapse(1)[no_vars]} \\
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   812
@{thm list.collapse(2)[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   813
53837
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   814
\item[@{text "t."}\hthm{disc\_exclude} @{text "[dest]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   815
These properties are missing for @{typ "'a list"} because there is only one
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   816
proper discriminator. Had the datatype been introduced with a second
53837
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   817
discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   818
@{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   819
@{prop "nonnull list \<Longrightarrow> \<not> null list"}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   820
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   821
\item[@{text "t."}\hthm{disc\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   822
@{thm list.disc_exhaust[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   823
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53863
diff changeset
   824
\item[@{text "t."}\hthm{sel\_exhaust} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53863
diff changeset
   825
@{thm list.sel_exhaust[no_vars]}
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53863
diff changeset
   826
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   827
\item[@{text "t."}\hthm{expand}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   828
@{thm list.expand[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   829
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   830
\item[@{text "t."}\hthm{sel\_split}\rm:] ~ \\
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   831
@{thm list.sel_split[no_vars]}
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   832
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   833
\item[@{text "t."}\hthm{sel\_split\_asm}\rm:] ~ \\
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   834
@{thm list.sel_split_asm[no_vars]}
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   835
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   836
\item[@{text "t."}\hthm{case\_eq\_if}\rm:] ~ \\
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   837
@{thm list.case_eq_if[no_vars]}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   838
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   839
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   840
\end{indentblock}
54152
f15bd1f81220 updated docs
blanchet
parents: 54146
diff changeset
   841
f15bd1f81220 updated docs
blanchet
parents: 54146
diff changeset
   842
\noindent
f15bd1f81220 updated docs
blanchet
parents: 54146
diff changeset
   843
In addition, equational versions of @{text t.disc} are registered with the @{text "[code]"}
f15bd1f81220 updated docs
blanchet
parents: 54146
diff changeset
   844
attribute.
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   845
*}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   846
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   847
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   848
subsubsection {* Functorial Theorems
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   849
  \label{sssec:functorial-theorems} *}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   850
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   851
text {*
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   852
The functorial theorems are partitioned in two subgroups. The first subgroup
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   853
consists of properties involving the constructors and either a set function, the
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   854
map function, or the relator:
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   855
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   856
\begin{indentblock}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   857
\begin{description}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   858
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   859
\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   860
@{thm list.set(1)[no_vars]} \\
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   861
@{thm list.set(2)[no_vars]}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   862
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   863
\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   864
@{thm list.map(1)[no_vars]} \\
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   865
@{thm list.map(2)[no_vars]}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   866
54146
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   867
\item[@{text "t."}\hthm{rel\_inject} @{text "[simp]"}\rm:] ~ \\
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   868
@{thm list.rel_inject(1)[no_vars]} \\
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   869
@{thm list.rel_inject(2)[no_vars]}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   870
54146
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   871
\item[@{text "t."}\hthm{rel\_distinct} @{text "[simp]"}\rm:] ~ \\
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   872
@{thm list.rel_distinct(1)[no_vars]} \\
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   873
@{thm list.rel_distinct(2)[no_vars]}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   874
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   875
\end{description}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   876
\end{indentblock}
54146
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   877
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   878
\noindent
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   879
In addition, equational versions of @{text t.rel_inject} and @{text
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   880
rel_distinct} are registered with the @{text "[code]"} attribute.
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   881
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   882
The second subgroup consists of more abstract properties of the set functions,
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   883
the map function, and the relator:
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   884
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   885
\begin{indentblock}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   886
\begin{description}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   887
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   888
\item[@{text "t."}\hthm{map\_comp}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   889
@{thm list.map_cong0[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   890
54624
36301c99ed26 revert making 'map_cong' a 'cong' -- it breaks too many proofs in the AFP
blanchet
parents: 54621
diff changeset
   891
\item[@{text "t."}\hthm{map\_cong} @{text "[fundef_cong]"}\rm:] ~ \\
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   892
@{thm list.map_cong[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   893
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   894
\item[@{text "t."}\hthm{map\_id}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   895
@{thm list.map_id[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   896
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   897
\item[@{text "t."}\hthm{rel\_compp}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   898
@{thm list.rel_compp[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   899
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   900
\item[@{text "t."}\hthm{rel\_conversep}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   901
@{thm list.rel_conversep[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   902
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   903
\item[@{text "t."}\hthm{rel\_eq}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   904
@{thm list.rel_eq[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   905
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   906
\item[@{text "t."}\hthm{rel\_flip}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   907
@{thm list.rel_flip[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   908
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   909
\item[@{text "t."}\hthm{rel\_mono}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   910
@{thm list.rel_mono[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   911
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   912
\item[@{text "t."}\hthm{set\_map}\rm:] ~ \\
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   913
@{thm list.set_map[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   914
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   915
\end{description}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   916
\end{indentblock}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   917
*}
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   918
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   919
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   920
subsubsection {* Inductive Theorems
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   921
  \label{sssec:inductive-theorems} *}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   922
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   923
text {*
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   924
The inductive theorems are as follows:
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   925
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   926
\begin{indentblock}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   927
\begin{description}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   928
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   929
\item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   930
@{thm list.induct[no_vars]}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   931
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   932
\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{induct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rm:] ~ \\
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   933
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   934
prove $m$ properties simultaneously.
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   935
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   936
\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   937
@{thm list.rec(1)[no_vars]} \\
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   938
@{thm list.rec(2)[no_vars]}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   939
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   940
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   941
\end{indentblock}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   942
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   943
\noindent
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   944
For convenience, @{command datatype_new} also provides the following collection:
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   945
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   946
\begin{indentblock}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   947
\begin{description}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   948
55871
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55705
diff changeset
   949
\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.map} @{text t.rel_inject}] ~ \\
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   950
@{text t.rel_distinct} @{text t.set}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   951
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   952
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   953
\end{indentblock}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   954
*}
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   955
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   956
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   957
subsection {* Compatibility Issues
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   958
  \label{ssec:datatype-compatibility-issues} *}
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   959
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   960
text {*
53997
8ff43f638da2 more "primrec_new" documentation
blanchet
parents: 53917
diff changeset
   961
The command @{command datatype_new} has been designed to be highly compatible
8ff43f638da2 more "primrec_new" documentation
blanchet
parents: 53917
diff changeset
   962
with the old \keyw{datatype}, to ease migration. There are nonetheless a few
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   963
incompatibilities that may arise when porting to the new package:
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   964
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   965
\begin{itemize}
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   966
\setlength{\itemsep}{0pt}
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   967
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   968
\item \emph{The Standard ML interfaces are different.} Tools and extensions
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   969
written to call the old ML interfaces will need to be adapted to the new
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   970
interfaces. Little has been done so far in this direction. Whenever possible, it
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   971
is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   972
to register new-style datatypes as old-style datatypes.
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   973
54537
f37354a894a3 fixed LaTeX missing }
blanchet
parents: 54494
diff changeset
   974
\item \emph{The constants @{text t_case} and @{text t_rec} are now called
f37354a894a3 fixed LaTeX missing }
blanchet
parents: 54494
diff changeset
   975
@{text case_t} and @{text rec_t}.}
f37354a894a3 fixed LaTeX missing }
blanchet
parents: 54494
diff changeset
   976
f37354a894a3 fixed LaTeX missing }
blanchet
parents: 54494
diff changeset
   977
\item \emph{The recursor @{text rec_t} has a different signature for nested
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   978
recursive datatypes.} In the old package, nested recursion through non-functions
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   979
was internally reduced to mutual recursion. This reduction was visible in the
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   980
type of the recursor, used by \keyw{primrec}. Recursion through functions was
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   981
handled specially. In the new package, nested recursion (for functions and
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
   982
non-functions) is handled in a more modular fashion. The old-style recursor can
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
   983
be generated on demand using @{command primrec}, as explained in
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   984
Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   985
new-style datatypes.
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   986
54287
7f096d8eb3d0 more docs
blanchet
parents: 54278
diff changeset
   987
\item \emph{Accordingly, the induction rule is different for nested recursive
7f096d8eb3d0 more docs
blanchet
parents: 54278
diff changeset
   988
datatypes.} Again, the old-style induction rule can be generated on demand using
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
   989
@{command primrec}, as explained in
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   990
Section~\ref{sssec:primrec-nested-as-mutual-recursion}, if the recursion is via
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   991
new-style datatypes.
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   992
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   993
\item \emph{The internal constructions are completely different.} Proof texts
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   994
that unfold the definition of constants introduced by \keyw{datatype} will be
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   995
difficult to port.
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   996
55641
5b466efedd2c renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
blanchet
parents: 55531
diff changeset
   997
\item \emph{Some induction rules have different names.}
5b466efedd2c renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
blanchet
parents: 55531
diff changeset
   998
For non-mutually recursive datatypes,
5b466efedd2c renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
blanchet
parents: 55531
diff changeset
   999
the alias @{text t.inducts} for @{text t.induct} is no longer generated.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1000
For $m > 1$ mutually recursive datatypes,
53997
8ff43f638da2 more "primrec_new" documentation
blanchet
parents: 53917
diff changeset
  1001
@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
55641
5b466efedd2c renamed 'recs' and 'cases' theorems 'rec' and 'case' in old datatype package, for consistency with new package
blanchet
parents: 55531
diff changeset
  1002
@{text "t\<^sub>i.induct"} for each @{text "i \<in> {1, \<dots>, t}"}.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1003
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1004
\item \emph{The @{text t.simps} collection has been extended.}
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1005
Previously available theorems are available at the same index.
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1006
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1007
\item \emph{Variables in generated properties have different names.} This is
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1008
rarely an issue, except in proof texts that refer to variable names in the
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1009
@{text "[where \<dots>]"} attribute. The solution is to use the more robust
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1010
@{text "[of \<dots>]"} syntax.
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1011
\end{itemize}
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1012
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1013
In the other direction, there is currently no way to register old-style
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1014
datatypes as new-style datatypes. If the goal is to define new-style datatypes
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1015
with nested recursion through old-style datatypes, the old-style
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1016
datatypes can be registered as a BNF
55351
blanchet
parents: 55350
diff changeset
  1017
(Section~\ref{sec:introducing-bounded-natural-functors}). If the goal is
55468
98b25c51e9e5 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents: 55460
diff changeset
  1018
to derive discriminators and selectors, this can be achieved using
98b25c51e9e5 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
blanchet
parents: 55460
diff changeset
  1019
@{command free_constructors}
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1020
(Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1021
*}
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1022
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
  1023
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
  1024
section {* Defining Recursive Functions
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
  1025
  \label{sec:defining-recursive-functions} *}
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
  1026
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
  1027
text {*
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1028
Recursive functions over datatypes can be specified using the @{command primrec}
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1029
command, which supports primitive recursion, or using the more general
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1030
\keyw{fun} and \keyw{function} commands. Here, the focus is on
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1031
@{command primrec}; the other two commands are described in a separate
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1032
tutorial \cite{isabelle-function}.
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1033
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1034
%%% TODO: partial_function
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
  1035
*}
52792
3e651be14fcd sketched documentation for new (co)datatype package
blanchet
parents:
diff changeset
  1036
52805
7f2f42046361 more (co)datatype documentation
blanchet
parents: 52795
diff changeset
  1037
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
  1038
subsection {* Introductory Examples
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
  1039
  \label{ssec:primrec-introductory-examples} *}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1040
53646
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1041
text {*
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1042
Primitive recursion is illustrated through concrete examples based on the
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1043
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
55075
b3d0a02a756d dissolved BNF session
blanchet
parents: 55073
diff changeset
  1044
examples can be found in the directory \verb|~~/src/HOL/BNF_Examples|.
53646
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1045
*}
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1046
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1047
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1048
subsubsection {* Nonrecursive Types
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1049
  \label{sssec:primrec-nonrecursive-types} *}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1050
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1051
text {*
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1052
Primitive recursion removes one layer of constructors on the left-hand side in
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1053
each equation. For example:
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1054
*}
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1055
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1056
    primrec bool_of_trool :: "trool \<Rightarrow> bool" where
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1057
      "bool_of_trool Faalse \<longleftrightarrow> False" |
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1058
      "bool_of_trool Truue \<longleftrightarrow> True"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1059
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1060
text {* \blankline *}
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1061
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1062
    primrec the_list :: "'a option \<Rightarrow> 'a list" where
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1063
      "the_list None = []" |
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1064
      "the_list (Some a) = [a]"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1065
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1066
text {* \blankline *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1067
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1068
    primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1069
      "the_default d None = d" |
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1070
      "the_default _ (Some a) = a"
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1071
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1072
text {* \blankline *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1073
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1074
    primrec mirrror :: "('a, 'b, 'c) triple \<Rightarrow> ('c, 'b, 'a) triple" where
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1075
      "mirrror (Triple a b c) = Triple c b a"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1076
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1077
text {*
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1078
\noindent
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1079
The equations can be specified in any order, and it is acceptable to leave out
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1080
some cases, which are then unspecified. Pattern matching on the left-hand side
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1081
is restricted to a single datatype, which must correspond to the same argument
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1082
in all equations.
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1083
*}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1084
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1085
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1086
subsubsection {* Simple Recursion
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1087
  \label{sssec:primrec-simple-recursion} *}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1088
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1089
text {*
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1090
For simple recursive types, recursive calls on a constructor argument are
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1091
allowed on the right-hand side:
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1092
*}
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1093
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1094
    primrec replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
53330
77da8d3c46e0 fixed docs w.r.t. availability of "primrec_new" and friends
blanchet
parents: 53262
diff changeset
  1095
      "replicate Zero _ = []" |
53644
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1096
      "replicate (Suc n) x = x # replicate n x"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1097
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1098
text {* \blankline *}
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1099
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1100
    primrec at :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" where
53644
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1101
      "at (x # xs) j =
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1102
         (case j of
53644
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1103
            Zero \<Rightarrow> x
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1104
          | Suc j' \<Rightarrow> at xs j')"
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1105
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1106
text {* \blankline *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1107
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1108
    primrec (*<*)(in early) (*>*)tfold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) tlist \<Rightarrow> 'b" where
53644
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1109
      "tfold _ (TNil y) = y" |
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1110
      "tfold f (TCons x xs) = f x (tfold f xs)"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1111
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1112
text {*
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1113
\noindent
54402
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1114
Pattern matching is only available for the argument on which the recursion takes
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1115
place. Fortunately, it is easy to generate pattern-maching equations using the
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1116
\keyw{simps\_of\_case} command provided by the theory
55290
3951ced4156c searchable underscores
blanchet
parents: 55254
diff changeset
  1117
\verb|~~/src/HOL/|\allowbreak\verb|Library/|\allowbreak\verb|Simps_Case_Conv|.
54402
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1118
*}
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1119
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1120
    simps_of_case at_simps: at.simps
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1121
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1122
text {*
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1123
This generates the lemma collection @{thm [source] at_simps}:
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1124
%
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1125
\[@{thm at_simps(1)[no_vars]}
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1126
  \qquad @{thm at_simps(2)[no_vars]}\]
5d1b7ee6070e document idiomatic use of 'simps_of_case'
blanchet
parents: 54386
diff changeset
  1127
%
54184
3fe73f3c84a2 more docs
blanchet
parents: 54183
diff changeset
  1128
The next example is defined using \keyw{fun} to escape the syntactic
55254
2bc951e6761a 'primitive' is not an adverb
blanchet
parents: 55129
diff changeset
  1129
restrictions imposed on primitively recursive functions. The
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
  1130
@{command datatype_compat} command is needed to register new-style datatypes
54184
3fe73f3c84a2 more docs
blanchet
parents: 54183
diff changeset
  1131
for use with \keyw{fun} and \keyw{function}
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1132
(Section~\ref{sssec:datatype-new-compat}):
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1133
*}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1134
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
  1135
    datatype_compat nat
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1136
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1137
text {* \blankline *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1138
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1139
    fun at_least_two :: "nat \<Rightarrow> bool" where
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1140
      "at_least_two (Suc (Suc _)) \<longleftrightarrow> True" |
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1141
      "at_least_two _ \<longleftrightarrow> False"
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1142
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1143
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1144
subsubsection {* Mutual Recursion
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1145
  \label{sssec:primrec-mutual-recursion} *}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1146
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1147
text {*
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1148
The syntax for mutually recursive functions over mutually recursive datatypes
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1149
is straightforward:
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1150
*}
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1151
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1152
    primrec
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1153
      nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1154
      nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1155
    where
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1156
      "nat_of_even_nat Even_Zero = Zero" |
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1157
      "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1158
      "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1159
53752
1a883094fbe0 more primcorec docs
blanchet
parents: 53751
diff changeset
  1160
text {* \blankline *}
1a883094fbe0 more primcorec docs
blanchet
parents: 53751
diff changeset
  1161
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1162
    primrec
53330
77da8d3c46e0 fixed docs w.r.t. availability of "primrec_new" and friends
blanchet
parents: 53262
diff changeset
  1163
      eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
77da8d3c46e0 fixed docs w.r.t. availability of "primrec_new" and friends
blanchet
parents: 53262
diff changeset
  1164
      eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
77da8d3c46e0 fixed docs w.r.t. availability of "primrec_new" and friends
blanchet
parents: 53262
diff changeset
  1165
      eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1166
    where
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1167
      "eval\<^sub>e \<gamma> \<xi> (Term t) = eval\<^sub>t \<gamma> \<xi> t" |
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1168
      "eval\<^sub>e \<gamma> \<xi> (Sum t e) = eval\<^sub>t \<gamma> \<xi> t + eval\<^sub>e \<gamma> \<xi> e" |
53330
77da8d3c46e0 fixed docs w.r.t. availability of "primrec_new" and friends
blanchet
parents: 53262
diff changeset
  1169
      "eval\<^sub>t \<gamma> \<xi> (Factor f) = eval\<^sub>f \<gamma> \<xi> f" |
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1170
      "eval\<^sub>t \<gamma> \<xi> (Prod f t) = eval\<^sub>f \<gamma> \<xi> f + eval\<^sub>t \<gamma> \<xi> t" |
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1171
      "eval\<^sub>f \<gamma> _ (Const a) = \<gamma> a" |
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1172
      "eval\<^sub>f _ \<xi> (Var b) = \<xi> b" |
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1173
      "eval\<^sub>f \<gamma> \<xi> (Expr e) = eval\<^sub>e \<gamma> \<xi> e"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1174
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1175
text {*
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1176
\noindent
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1177
Mutual recursion is possible within a single type, using \keyw{fun}:
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1178
*}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1179
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1180
    fun
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1181
      even :: "nat \<Rightarrow> bool" and
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1182
      odd :: "nat \<Rightarrow> bool"
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1183
    where
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1184
      "even Zero = True" |
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1185
      "even (Suc n) = odd n" |
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1186
      "odd Zero = False" |
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1187
      "odd (Suc n) = even n"
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1188
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1189
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1190
subsubsection {* Nested Recursion
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1191
  \label{sssec:primrec-nested-recursion} *}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1192
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1193
text {*
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1194
In a departure from the old datatype package, nested recursion is normally
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1195
handled via the map functions of the nesting type constructors. For example,
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1196
recursive calls are lifted to lists using @{const map}:
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1197
*}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1198
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1199
(*<*)
53644
eb8362530715 more (co)data docs
blanchet
parents: 53643
diff changeset
  1200
    datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f (lbl\<^sub>f\<^sub>f: 'a) (sub\<^sub>f\<^sub>f: "'a tree\<^sub>f\<^sub>f list")
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1201
(*>*)
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1202
    primrec at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
  1203
      "at\<^sub>f\<^sub>f (Node\<^sub>f\<^sub>f a ts) js =
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1204
         (case js of
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1205
            [] \<Rightarrow> a
53028
a1e64c804c35 more (co)datatype documentation
blanchet
parents: 53025
diff changeset
  1206
          | j # js' \<Rightarrow> at (map (\<lambda>t. at\<^sub>f\<^sub>f t js') ts) j)"
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1207
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1208
text {*
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1209
\noindent
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1210
The next example features recursion through the @{text option} type. Although
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1211
@{text option} is not a new-style datatype, it is registered as a BNF with the
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
  1212
map function @{const map_option}:
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
  1213
*}
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1214
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1215
    primrec (*<*)(in early) (*>*)sum_btree :: "('a\<Colon>{zero,plus}) btree \<Rightarrow> 'a" where
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1216
      "sum_btree (BNode a lt rt) =
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
  1217
         a + the_default 0 (map_option sum_btree lt) +
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
  1218
           the_default 0 (map_option sum_btree rt)"
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1219
53136
98a2c33d5d1b ideas for (co)datatype docs
blanchet
parents: 53028
diff changeset
  1220
text {*
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1221
\noindent
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1222
The same principle applies for arbitrary type constructors through which
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1223
recursion is possible. Notably, the map function for the function type
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1224
(@{text \<Rightarrow>}) is simply composition (@{text "op \<circ>"}):
53136
98a2c33d5d1b ideas for (co)datatype docs
blanchet
parents: 53028
diff changeset
  1225
*}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1226
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1227
    primrec (*<*)(in early) (*>*)relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
54182
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1228
      "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1229
      "relabel_ft f (FTNode g) = FTNode (relabel_ft f \<circ> g)"
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1230
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1231
text {*
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1232
\noindent
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1233
For convenience, recursion through functions can also be expressed using
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1234
$\lambda$-abstractions and function application rather than through composition.
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1235
For example:
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1236
*}
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1237
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1238
    primrec relabel_ft :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
54182
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1239
      "relabel_ft f (FTLeaf x) = FTLeaf (f x)" |
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1240
      "relabel_ft f (FTNode g) = FTNode (\<lambda>x. relabel_ft f (g x))"
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1241
54183
8a6a49385122 more docs
blanchet
parents: 54182
diff changeset
  1242
text {* \blankline *}
8a6a49385122 more docs
blanchet
parents: 54182
diff changeset
  1243
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1244
    primrec subtree_ft :: "'a \<Rightarrow> 'a ftree \<Rightarrow> 'a ftree" where
54183
8a6a49385122 more docs
blanchet
parents: 54182
diff changeset
  1245
      "subtree_ft x (FTNode g) = g x"
8a6a49385122 more docs
blanchet
parents: 54182
diff changeset
  1246
52843
ea95702328cf more (co)datatype docs
blanchet
parents: 52841
diff changeset
  1247
text {*
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1248
\noindent
54182
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset
  1249
For recursion through curried $n$-ary functions, $n$ applications of
e3759cbde221 expand doc a bit
blanchet
parents: 54181
diff changeset