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