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