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