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