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