src/Doc/Datatypes/Datatypes.thy
author blanchet
Wed, 06 Jan 2016 13:04:31 +0100
changeset 62081 fd18b51bdc55
parent 61788 1e4caf2beb5d
child 62093 bd73a2279fcd
permissions -rw-r--r--
updated docs
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
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   345
function, a relator, discriminators, and selectors, all of which can be given
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   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
58245
7e54225acef1 more docs
blanchet
parents: 58244
diff changeset
   362
    hide_const Nil Cons case_list hd tl set map list_all2 rec_list size_list pred_list
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   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
57200
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   373
    where
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   374
      "tl Nil = Nil"
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   375
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   376
text \<open>
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   377
\noindent
55353
blanchet
parents: 55351
diff changeset
   378
The types of the constants that appear in the specification are listed below.
55351
blanchet
parents: 55350
diff changeset
   379
blanchet
parents: 55350
diff changeset
   380
\medskip
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   381
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   382
\begin{tabular}{@ {}ll@ {}}
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   383
Constructors: &
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   384
  @{text "Nil :: 'a list"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   385
&
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   386
  @{text "Cons :: 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   387
Discriminator: &
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   388
  @{text "null :: 'a list \<Rightarrow> bool"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   389
Selectors: &
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   390
  @{text "hd :: 'a list \<Rightarrow> 'a"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   391
&
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   392
  @{text "tl :: 'a list \<Rightarrow> 'a list"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   393
Set function: &
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   394
  @{text "set :: 'a list \<Rightarrow> 'a set"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   395
Map function: &
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   396
  @{text "map :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"} \\
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   397
Relator: &
61076
bdc1e2f0a86a eliminated \<Colon>;
wenzelm
parents: 60920
diff changeset
   398
  @{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
   399
\end{tabular}
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   400
55351
blanchet
parents: 55350
diff changeset
   401
\medskip
blanchet
parents: 55350
diff changeset
   402
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   403
The discriminator @{const null} and the selectors @{const hd} and @{const tl}
55351
blanchet
parents: 55350
diff changeset
   404
are characterized by the following conditional equations:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   405
%
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   406
\[@{thm list.collapse(1)[of xs, no_vars]}
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   407
  \qquad @{thm list.collapse(2)[of xs, no_vars]}\]
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   408
%
54187
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   409
For two-constructor datatypes, a single discriminator constant is sufficient.
80259d79a81e more doc -- feedback from Andrei P.
blanchet
parents: 54185
diff changeset
   410
The discriminator associated with @{const Cons} is simply
53491
2479b39d9d09 more docs
blanchet
parents: 53335
diff changeset
   411
@{term "\<lambda>xs. \<not> null xs"}.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   412
57200
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   413
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
   414
selectors applied to constructors on which they are not a priori specified.
59282
blanchet
parents: 59280
diff changeset
   415
In the example, it is used to ensure that the tail of the empty list is itself
blanchet
parents: 59280
diff changeset
   416
(instead of being left unspecified).
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   417
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   418
Because @{const Nil} is nullary, it is also possible to use
57091
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   419
@{term "\<lambda>xs. xs = Nil"} as a discriminator. This is the default behavior
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   420
if we omit the identifier @{const null} and the associated colon. Some users
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   421
argue against this, because the mixture of constructors and selectors in the
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   422
characteristic theorems can lead Isabelle's automation to switch between the
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   423
constructor and the destructor view in surprising ways.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   424
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   425
The usual mixfix syntax annotations are available for both types and
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   426
constructors. For example:
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   427
\<close>
52794
aae782070611 more (co)datatype documentation
blanchet
parents: 52792
diff changeset
   428
53025
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   429
(*<*)
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   430
    end
c820c9e9e8f4 more work on (co)datatype docs
blanchet
parents: 53018
diff changeset
   431
(*>*)
58310
91ea607a34d8 updated news
blanchet
parents: 58309
diff changeset
   432
    datatype ('a, 'b) prod (infixr "*" 20) = Pair 'a 'b
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   433
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   434
text \<open> \blankline \<close>
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   435
58310
91ea607a34d8 updated news
blanchet
parents: 58309
diff changeset
   436
    datatype (set: 'a) list =
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   437
      null: Nil ("[]")
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   438
    | 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
   439
    for
d9be905d6283 changed syntax of map: and rel: arguments to BNF-based datatypes
blanchet
parents: 57200
diff changeset
   440
      map: map
d9be905d6283 changed syntax of map: and rel: arguments to BNF-based datatypes
blanchet
parents: 57200
diff changeset
   441
      rel: list_all2
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   442
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   443
text \<open>
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   444
\noindent
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   445
Incidentally, this is how the traditional syntax can be set up:
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   446
\<close>
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   447
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   448
    syntax "_list" :: "args \<Rightarrow> 'a list" ("[(_)]")
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   449
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   450
text \<open> \blankline \<close>
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   451
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   452
    translations
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   453
      "[x, xs]" == "x # [xs]"
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
   454
      "[x]" == "x # []"
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   455
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   456
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   457
subsection \<open> Command Syntax
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   458
  \label{ssec:datatype-command-syntax} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   459
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   460
subsubsection \<open> \keyw{datatype}
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   461
  \label{sssec:datatype-new} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   462
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   463
text \<open>
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   464
\begin{matharray}{rcl}
58310
91ea607a34d8 updated news
blanchet
parents: 58309
diff changeset
   465
  @{command_def "datatype"} & : & @{text "local_theory \<rightarrow> local_theory"}
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   466
\end{matharray}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   467
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   468
@{rail \<open>
59282
blanchet
parents: 59280
diff changeset
   469
  @@{command datatype} target? @{syntax dt_options}? @{syntax dt_spec}
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
   470
  ;
59280
blanchet
parents: 59278
diff changeset
   471
  @{syntax_def dt_options}: '(' ((@{syntax plugins} | 'discs_sels') + ',') ')'
58190
89034dc40247 updated docs
blanchet
parents: 58151
diff changeset
   472
  ;
59280
blanchet
parents: 59278
diff changeset
   473
  @{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
   474
  ;
59282
blanchet
parents: 59280
diff changeset
   475
  @{syntax_def dt_spec}: (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
blanchet
parents: 59280
diff changeset
   476
     @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
blanchet
parents: 59280
diff changeset
   477
  ;
57206
d9be905d6283 changed syntax of map: and rel: arguments to BNF-based datatypes
blanchet
parents: 57200
diff changeset
   478
  @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   479
\<close>}
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   480
55351
blanchet
parents: 55350
diff changeset
   481
\medskip
blanchet
parents: 55350
diff changeset
   482
blanchet
parents: 55350
diff changeset
   483
\noindent
58310
91ea607a34d8 updated news
blanchet
parents: 58309
diff changeset
   484
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
   485
datatypes specified by their constructors.
3f4efd7d950d added a bit of documentation for the different commands
blanchet
parents: 55459
diff changeset
   486
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   487
The syntactic entity \synt{target} can be used to specify a local
58620
7435b6a3f72e more antiquotations;
wenzelm
parents: 58509
diff changeset
   488
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
   489
and \synt{prop} denotes a HOL proposition.
55460
3f4efd7d950d added a bit of documentation for the different commands
blanchet
parents: 55459
diff changeset
   490
58190
89034dc40247 updated docs
blanchet
parents: 58151
diff changeset
   491
The optional target is optionally followed by a combination of the following
56124
315cc3c0a19a tuned wording (pun)
blanchet
parents: 56123
diff changeset
   492
options:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   493
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   494
\begin{itemize}
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   495
\setlength{\itemsep}{0pt}
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   496
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   497
\item
59280
blanchet
parents: 59278
diff changeset
   498
The @{text plugins} option indicates which plugins should be enabled
blanchet
parents: 59278
diff changeset
   499
(@{text only}) or disabled (@{text del}). By default, all plugins are enabled.
58190
89034dc40247 updated docs
blanchet
parents: 58151
diff changeset
   500
89034dc40247 updated docs
blanchet
parents: 58151
diff changeset
   501
\item
57094
589ec121ce1a don't generate discriminators and selectors for 'datatype_new' unless the user asked for it
blanchet
parents: 57092
diff changeset
   502
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
   503
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
   504
discriminators or selectors.
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   505
\end{itemize}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   506
57200
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   507
The optional \keyw{where} clause specifies default values for selectors.
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   508
Each proposition must be an equation of the form
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   509
@{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
   510
@{text un_D} is a selector.
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   511
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   512
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
   513
define, its type parameters, and additional information:
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   514
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   515
@{rail \<open>
57206
d9be905d6283 changed syntax of map: and rel: arguments to BNF-based datatypes
blanchet
parents: 57200
diff changeset
   516
  @{syntax_def dt_name}: @{syntax tyargs}? name mixfix?
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   517
  ;
57092
59603f4f1d2e changed '-:' to 'dead' in BNF
blanchet
parents: 57091
diff changeset
   518
  @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   519
\<close>}
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   520
55351
blanchet
parents: 55350
diff changeset
   521
\medskip
blanchet
parents: 55350
diff changeset
   522
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   523
\noindent
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   524
The syntactic entity \synt{name} denotes an identifier, \synt{mixfix} denotes
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   525
the usual parenthesized mixfix notation, and \synt{typefree} denotes fixed type
58620
7435b6a3f72e more antiquotations;
wenzelm
parents: 58509
diff changeset
   526
variable (@{typ 'a}, @{typ 'b}, \ldots) @{cite "isabelle-isar-ref"}.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   527
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   528
The optional names preceding the type variables allow to override the default
57988
030ff4ceb6c3 updated docs
blanchet
parents: 57984
diff changeset
   529
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
   530
arguments can be marked as dead by entering @{text dead} in front of the
58220
a2afad27a0b1 wildcards in plugins
blanchet
parents: 58215
diff changeset
   531
type variable (e.g., @{text "(dead 'a)"}); otherwise, they are live or dead
55705
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   532
(and a set function is generated or not) depending on where they occur in the
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   533
right-hand sides of the definition. Declaring a type argument as dead can speed
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   534
up the type definition but will prevent any later (co)recursion through that
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   535
type argument.
a98a045a6169 updated docs
blanchet
parents: 55641
diff changeset
   536
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   537
Inside a mutually recursive specification, all defined datatypes must
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
   538
mention exactly the same type variables in the same order.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   539
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   540
@{rail \<open>
57200
aab87ffa60cc use 'where' clause for selector default value syntax
blanchet
parents: 57153
diff changeset
   541
  @{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
   542
\<close>}
52824
b7a83845bc93 more (co)datatype documentation
blanchet
parents: 52822
diff changeset
   543
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   544
\medskip
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   545
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   546
\noindent
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
   547
The main constituents of a constructor specification are the name of the
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   548
constructor and the list of its argument types. An optional discriminator name
59722
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   549
can be supplied at the front. If discriminators are enabled (cf.\ the
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   550
@{text "discs_sels"} option) but no name is supplied, the default is
57091
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   551
@{text "\<lambda>x. x = C\<^sub>j"} for nullary constructors and
1fa9c19ba2c9 got rid of '=:' squiggly
blanchet
parents: 57088
diff changeset
   552
@{text t.is_C\<^sub>j} otherwise.
52822
ae938ac9a721 more (co)datatype docs
blanchet
parents: 52806
diff changeset
   553
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   554
@{rail \<open>
55472
990651bfc65b updated docs to reflect the new 'free_constructors' syntax
blanchet
parents: 55468
diff changeset
   555
  @{syntax_def dt_ctor_arg}: type | '(' name ':' type ')'
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   556
\<close>}
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   557
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   558
\medskip
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   559
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   560
\noindent
58620
7435b6a3f72e more antiquotations;
wenzelm
parents: 58509
diff changeset
   561
The syntactic entity \synt{type} denotes a HOL type @{cite "isabelle-isar-ref"}.
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   562
52827
395d3df496ed more (co)datatype documentation
blanchet
parents: 52824
diff changeset
   563
In addition to the type of a constructor argument, it is possible to specify a
59722
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   564
name for the corresponding selector. The same selector name can be reused for
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   565
arguments to several constructors as long as the arguments share the same type.
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   566
If selectors are enabled (cf.\ the @{text "discs_sels"} option) but no name is
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   567
supplied, the default name is @{text un_C\<^sub>ji}.
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   568
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   569
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   570
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   571
subsubsection \<open> \keyw{datatype_compat}
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   572
  \label{sssec:datatype-compat} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   573
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   574
text \<open>
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   575
\begin{matharray}{rcl}
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   576
  @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   577
\end{matharray}
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   578
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   579
@{rail \<open>
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   580
  @@{command datatype_compat} (name +)
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55029
diff changeset
   581
\<close>}
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   582
55351
blanchet
parents: 55350
diff changeset
   583
\medskip
blanchet
parents: 55350
diff changeset
   584
53829
92e71eb22ebe more (co)data docs
blanchet
parents: 53828
diff changeset
   585
\noindent
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   586
The @{command datatype_compat} command registers new-style datatypes as
58245
7e54225acef1 more docs
blanchet
parents: 58244
diff changeset
   587
old-style datatypes and invokes the old-style plugins. For example:
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   588
\<close>
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   589
55531
601ca8efa000 renamed 'datatype_new_compat' to 'datatype_compat'
blanchet
parents: 55530
diff changeset
   590
    datatype_compat even_nat odd_nat
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   591
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   592
text \<open> \blankline \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   593
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   594
    ML \<open> Old_Datatype_Data.get_info @{theory} @{type_name even_nat} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   595
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   596
text \<open>
58620
7435b6a3f72e more antiquotations;
wenzelm
parents: 58509
diff changeset
   597
The syntactic entity \synt{name} denotes an identifier @{cite "isabelle-isar-ref"}.
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   598
60135
852f7a49ec0c updated docs, esp. relating to 'datatype_compat'
blanchet
parents: 60134
diff changeset
   599
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
   600
the new one.
55474
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   601
501df9ad117b more (co)datatype docs
blanchet
parents: 55472
diff changeset
   602
A few remarks concern nested recursive datatypes:
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   603
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   604
\begin{itemize}
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   605
\setlength{\itemsep}{0pt}
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   606
55871
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55705
diff changeset
   607
\item The old-style, nested-as-mutual induction rule and recursor theorems are
a28817253b31 removed (co)iterators from documentation
blanchet
parents: 55705
diff changeset
   608
generated under their usual names but with ``@{text "compat_"}'' prefixed
58215
cccf5445e224 tuned docs
blanchet
parents: 58212
diff changeset
   609
(e.g., @{text compat_tree.induct}, @{text compat_tree.inducts}, and
61351
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
   610
@{text compat_tree.rec}). These theorems should be identical to the ones
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
   611
generated by the old datatype package, \emph{up to the order of the
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
   612
premises}---meaning that the subgoals generated by the @{text induct} or
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
   613
@{text induction} method may be in a different order than before.
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   614
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   615
\item All types through which recursion takes place must be new-style datatypes
59722
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   616
or the function type.
53748
be0ddf3dd01b updated docs
blanchet
parents: 53722
diff changeset
   617
\end{itemize}
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   618
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   619
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   620
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   621
subsection \<open> Generated Constants
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   622
  \label{ssec:datatype-generated-constants} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   623
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   624
text \<open>
59722
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   625
Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"} with $m$ live type variables
59284
blanchet
parents: 59282
diff changeset
   626
and $n$ constructors @{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the following
blanchet
parents: 59282
diff changeset
   627
auxiliary constants are introduced:
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   628
55353
blanchet
parents: 55351
diff changeset
   629
\medskip
blanchet
parents: 55351
diff changeset
   630
blanchet
parents: 55351
diff changeset
   631
\begin{tabular}{@ {}ll@ {}}
blanchet
parents: 55351
diff changeset
   632
Case combinator: &
blanchet
parents: 55351
diff changeset
   633
  @{text t.case_t} (rendered using the familiar @{text case}--@{text of} syntax) \\
blanchet
parents: 55351
diff changeset
   634
Discriminators: &
57988
030ff4ceb6c3 updated docs
blanchet
parents: 57984
diff changeset
   635
  @{text t.is_C\<^sub>1}$, \ldots, $@{text t.is_C\<^sub>n} \\
55353
blanchet
parents: 55351
diff changeset
   636
Selectors: &
blanchet
parents: 55351
diff changeset
   637
  @{text t.un_C\<^sub>11}$, \ldots, $@{text t.un_C\<^sub>1k\<^sub>1} \\
blanchet
parents: 55351
diff changeset
   638
& \quad\vdots \\
blanchet
parents: 55351
diff changeset
   639
& @{text t.un_C\<^sub>n1}$, \ldots, $@{text t.un_C\<^sub>nk\<^sub>n} \\
blanchet
parents: 55351
diff changeset
   640
Set functions: &
57988
030ff4ceb6c3 updated docs
blanchet
parents: 57984
diff changeset
   641
  @{text t.set\<^sub>1_t}, \ldots, @{text t.set\<^sub>m_t} \\
55353
blanchet
parents: 55351
diff changeset
   642
Map function: &
blanchet
parents: 55351
diff changeset
   643
  @{text t.map_t} \\
blanchet
parents: 55351
diff changeset
   644
Relator: &
blanchet
parents: 55351
diff changeset
   645
  @{text t.rel_t} \\
blanchet
parents: 55351
diff changeset
   646
Recursor: &
58190
89034dc40247 updated docs
blanchet
parents: 58151
diff changeset
   647
  @{text t.rec_t}
55353
blanchet
parents: 55351
diff changeset
   648
\end{tabular}
blanchet
parents: 55351
diff changeset
   649
blanchet
parents: 55351
diff changeset
   650
\medskip
53617
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   651
da5e1887d7a7 more (co)data doc
blanchet
parents: 53565
diff changeset
   652
\noindent
59722
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   653
The discriminators and selectors are generated only if the @{text "discs_sels"}
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   654
option is enabled or if names are specified for discriminators or selectors.
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   655
The set functions, map function, and relator are generated only if $m > 0$.
c1e19e6ae980 updated docs
blanchet
parents: 59721
diff changeset
   656
58245
7e54225acef1 more docs
blanchet
parents: 58244
diff changeset
   657
In addition, some of the plugins introduce their own constants
59282
blanchet
parents: 59280
diff changeset
   658
(Section~\ref{sec:selecting-plugins}). The case combinator, discriminators,
58508
cb68c3f564fe fixed a few mistakes in the documentation
blanchet
parents: 58474
diff changeset
   659
and selectors are collectively called \emph{destructors}. The prefix
cb68c3f564fe fixed a few mistakes in the documentation
blanchet
parents: 58474
diff changeset
   660
``@{text "t."}'' is an optional component of the names and is normally hidden.
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   661
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   662
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   663
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   664
subsection \<open> Generated Theorems
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   665
  \label{ssec:datatype-generated-theorems} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   666
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   667
text \<open>
58310
91ea607a34d8 updated news
blanchet
parents: 58309
diff changeset
   668
The characteristic theorems generated by @{command datatype} are grouped in
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
   669
three broad categories:
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   670
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   671
\begin{itemize}
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   672
\setlength{\itemsep}{0pt}
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
   673
56655
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   674
\item The \emph{free constructor theorems}
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   675
(Section~\ref{sssec:free-constructor-theorems}) are properties of the
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   676
constructors and destructors that can be derived for any freely generated type.
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   677
Internally, the derivation is performed by @{command free_constructors}.
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   678
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   679
\item The \emph{functorial theorems} (Section~\ref{sssec:functorial-theorems})
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   680
are properties of datatypes related to their BNF nature.
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   681
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   682
\item The \emph{inductive theorems} (Section~\ref{sssec:inductive-theorems})
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
   683
are properties of datatypes related to their inductive nature.
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   684
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   685
\end{itemize}
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   686
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   687
\noindent
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   688
The full list of named theorems can be obtained as usual by entering the
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   689
command \keyw{print_theorems} immediately after the datatype definition.
58508
cb68c3f564fe fixed a few mistakes in the documentation
blanchet
parents: 58474
diff changeset
   690
This list includes theorems produced by plugins
59282
blanchet
parents: 59280
diff changeset
   691
(Section~\ref{sec:selecting-plugins}), but normally excludes low-level
58508
cb68c3f564fe fixed a few mistakes in the documentation
blanchet
parents: 58474
diff changeset
   692
theorems that reveal internal constructions. To make these accessible, add
cb68c3f564fe fixed a few mistakes in the documentation
blanchet
parents: 58474
diff changeset
   693
the line
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   694
\<close>
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   695
53542
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   696
    declare [[bnf_note_all]]
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   697
(*<*)
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   698
    declare [[bnf_note_all = false]]
14000a283ce0 more (co)data docs
blanchet
parents: 53535
diff changeset
   699
(*>*)
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   700
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   701
text \<open>
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   702
\noindent
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   703
to the top of the theory file.
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   704
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   705
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   706
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   707
subsubsection \<open> Free Constructor Theorems
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   708
  \label{sssec:free-constructor-theorems} \<close>
53535
d0c163c6c725 more (co)data docs
blanchet
parents: 53534
diff changeset
   709
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   710
(*<*)
53837
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   711
    consts nonnull :: 'a
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   712
(*>*)
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   713
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   714
text \<open>
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   715
The free constructor theorems are partitioned in three subgroups. The first
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   716
subgroup of properties is concerned with the constructors. They are listed below
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   717
for @{typ "'a list"}:
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   718
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   719
\begin{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   720
\begin{description}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   721
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   722
\item[@{text "t."}\hthm{inject} @{text "[iff, induct_simp]"}\rm:] ~ \\
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   723
@{thm list.inject[no_vars]}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   724
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   725
\item[@{text "t."}\hthm{distinct} @{text "[simp, induct_simp]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   726
@{thm list.distinct(1)[no_vars]} \\
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   727
@{thm list.distinct(2)[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   728
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   729
\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
   730
@{thm list.exhaust[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   731
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   732
\item[@{text "t."}\hthm{nchotomy}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   733
@{thm list.nchotomy[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   734
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   735
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   736
\end{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   737
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   738
\noindent
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   739
In addition, these nameless theorems are registered as safe elimination rules:
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   740
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   741
\begin{indentblock}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   742
\begin{description}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   743
54386
3514fdfdf59b minor doc fix
blanchet
parents: 54287
diff changeset
   744
\item[@{text "t."}\hthm{distinct {\upshape[}THEN notE}@{text ", elim!"}\hthm{\upshape]}\rm:] ~ \\
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   745
@{thm list.distinct(1)[THEN notE, elim!, no_vars]} \\
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   746
@{thm list.distinct(2)[THEN notE, elim!, no_vars]}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   747
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   748
\end{description}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   749
\end{indentblock}
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   750
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
   751
\noindent
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   752
The next subgroup is concerned with the case combinator:
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   753
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   754
\begin{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   755
\begin{description}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   756
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   757
\item[@{text "t."}\hthm{case} @{text "[simp, code]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   758
@{thm list.case(1)[no_vars]} \\
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58311
diff changeset
   759
@{thm list.case(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   760
The @{text "[code]"} attribute is set by the @{text code} plugin
blanchet
parents: 59282
diff changeset
   761
(Section~\ref{ssec:code-generator}).
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   762
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   763
\item[@{text "t."}\hthm{case_cong} @{text "[fundef_cong]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   764
@{thm list.case_cong[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   765
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   766
\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
   767
@{thm list.case_cong_weak[no_vars]}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   768
59268
3f5d6ee7596f document 'case_distrib'
desharna
parents: 58935
diff changeset
   769
\item[@{text "t."}\hthm{case_distrib}\rm:] ~ \\
3f5d6ee7596f document 'case_distrib'
desharna
parents: 58935
diff changeset
   770
@{thm list.case_distrib[no_vars]}
3f5d6ee7596f document 'case_distrib'
desharna
parents: 58935
diff changeset
   771
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   772
\item[@{text "t."}\hthm{split}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   773
@{thm list.split[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   774
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   775
\item[@{text "t."}\hthm{split_asm}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   776
@{thm list.split_asm[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   777
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   778
\item[@{text "t."}\hthm{splits} = @{text "split split_asm"}]
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   779
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   780
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   781
\end{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   782
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   783
\noindent
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   784
The third subgroup revolves around discriminators and selectors:
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   785
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   786
\begin{indentblock}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   787
\begin{description}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
   788
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   789
\item[@{text "t."}\hthm{disc} @{text "[simp]"}\rm:] ~ \\
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   790
@{thm list.disc(1)[no_vars]} \\
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   791
@{thm list.disc(2)[no_vars]}
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   792
53703
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   793
\item[@{text "t."}\hthm{discI}\rm:] ~ \\
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   794
@{thm list.discI(1)[no_vars]} \\
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   795
@{thm list.discI(2)[no_vars]}
0c565fec9c78 updated docs
blanchet
parents: 53694
diff changeset
   796
53805
4163160853fd added [code] to selectors
blanchet
parents: 53798
diff changeset
   797
\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   798
@{thm list.sel(1)[no_vars]} \\
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58311
diff changeset
   799
@{thm list.sel(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   800
The @{text "[code]"} attribute is set by the @{text code} plugin
blanchet
parents: 59282
diff changeset
   801
(Section~\ref{ssec:code-generator}).
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   802
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   803
\item[@{text "t."}\hthm{collapse} @{text "[simp]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   804
@{thm list.collapse(1)[no_vars]} \\
58151
414deb2ef328 take out 'x = C' of the simplifier for unit types
blanchet
parents: 58121
diff changeset
   805
@{thm list.collapse(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   806
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
   807
with a single nullary constructor, because a property of the form
59284
blanchet
parents: 59282
diff changeset
   808
@{prop "x = C"} is not suitable as a simplification rule.
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   809
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   810
\item[@{text "t."}\hthm{distinct_disc} @{text "[dest]"}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   811
These properties are missing for @{typ "'a list"} because there is only one
59284
blanchet
parents: 59282
diff changeset
   812
proper discriminator. If the datatype had been introduced with a second
53837
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   813
discriminator called @{const nonnull}, they would have read thusly: \\[\jot]
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   814
@{prop "null list \<Longrightarrow> \<not> nonnull list"} \\
65c775430caa updated docs
blanchet
parents: 53831
diff changeset
   815
@{prop "nonnull list \<Longrightarrow> \<not> null list"}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   816
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   817
\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
   818
@{thm list.exhaust_disc[no_vars]}
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   819
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   820
\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
   821
@{thm list.exhaust_sel[no_vars]}
53916
37c31a619eee generate "sel_exhaust" theorem
blanchet
parents: 53863
diff changeset
   822
53642
05ca82603671 more (co)data docs
blanchet
parents: 53623
diff changeset
   823
\item[@{text "t."}\hthm{expand}\rm:] ~ \\
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   824
@{thm list.expand[no_vars]}
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   825
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   826
\item[@{text "t."}\hthm{split_sel}\rm:] ~ \\
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   827
@{thm list.split_sel[no_vars]}
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   828
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   829
\item[@{text "t."}\hthm{split_sel_asm}\rm:] ~ \\
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   830
@{thm list.split_sel_asm[no_vars]}
53917
bf74357f91f8 generate "sel_splits(_asm)" theorems
blanchet
parents: 53916
diff changeset
   831
57984
cbe9a16f8e11 added collection theorem for consistency and convenience
blanchet
parents: 57983
diff changeset
   832
\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
   833
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   834
\item[@{text "t."}\hthm{case_eq_if}\rm:] ~ \\
54491
27966e17d075 case_if -> case_eq_if + docs
blanchet
parents: 54422
diff changeset
   835
@{thm list.case_eq_if[no_vars]}
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   836
59273
2c1e58190664 document 'disc_eq_case'
desharna
parents: 59268
diff changeset
   837
\item[@{text "t."}\hthm{disc_eq_case}\rm:] ~ \\
2c1e58190664 document 'disc_eq_case'
desharna
parents: 59268
diff changeset
   838
@{thm list.disc_eq_case(1)[no_vars]} \\
2c1e58190664 document 'disc_eq_case'
desharna
parents: 59268
diff changeset
   839
@{thm list.disc_eq_case(2)[no_vars]}
2c1e58190664 document 'disc_eq_case'
desharna
parents: 59268
diff changeset
   840
53543
c6c8dce7e9ab more (co)data docs
blanchet
parents: 53542
diff changeset
   841
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   842
\end{indentblock}
54152
f15bd1f81220 updated docs
blanchet
parents: 54146
diff changeset
   843
f15bd1f81220 updated docs
blanchet
parents: 54146
diff changeset
   844
\noindent
58151
414deb2ef328 take out 'x = C' of the simplifier for unit types
blanchet
parents: 58121
diff changeset
   845
In addition, equational versions of @{text t.disc} are registered with the
59284
blanchet
parents: 59282
diff changeset
   846
@{text "[code]"} attribute. The @{text "[code]"} attribute is set by the
blanchet
parents: 59282
diff changeset
   847
@{text code} plugin (Section~\ref{ssec:code-generator}).
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   848
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   849
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   850
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   851
subsubsection \<open> Functorial Theorems
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   852
  \label{sssec:functorial-theorems} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   853
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
   854
text \<open>
61349
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   855
The functorial theorems are generated for type constructors with at least
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   856
one live type argument (e.g., @{typ "'a list"}). They are partitioned in two
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   857
subgroups. The first subgroup consists of properties involving the
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   858
constructors or the destructors and either a set function, the map function,
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   859
or the relator:
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   860
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   861
\begin{indentblock}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   862
\begin{description}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   863
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   864
\item[@{text "t."}\hthm{case_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   865
@{thm list.case_transfer[no_vars]} \\
61350
821ba62ed31b updated docs
blanchet
parents: 61349
diff changeset
   866
This property is generated by the @{text transfer} plugin
61349
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   867
(Section~\ref{ssec:transfer}).
61350
821ba62ed31b updated docs
blanchet
parents: 61349
diff changeset
   868
%The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
821ba62ed31b updated docs
blanchet
parents: 61349
diff changeset
   869
%(Section~\ref{ssec:transfer}).
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   870
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   871
\item[@{text "t."}\hthm{sel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
58677
74a81d6f3c54 document 'sel_transfer'
desharna
parents: 58659
diff changeset
   872
This property is missing for @{typ "'a list"} because there is no common
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   873
selector to all constructors. \\
59284
blanchet
parents: 59282
diff changeset
   874
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
61349
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   875
(Section~\ref{ssec:transfer}).
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   876
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   877
\item[@{text "t."}\hthm{ctr_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
58000
52181f7b4468 document 'ctr_transfer'
desharna
parents: 57988
diff changeset
   878
@{thm list.ctr_transfer(1)[no_vars]} \\
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   879
@{thm list.ctr_transfer(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   880
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
61349
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   881
(Section~\ref{ssec:transfer}) .
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   882
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   883
\item[@{text "t."}\hthm{disc_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
58096
5a48fef59fab document 'disc_transfer'
desharna
parents: 58094
diff changeset
   884
@{thm list.disc_transfer(1)[no_vars]} \\
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   885
@{thm list.disc_transfer(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   886
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
61349
24e7b6c91514 made documentation more accurate
blanchet
parents: 61304
diff changeset
   887
(Section~\ref{ssec:transfer}).
58096
5a48fef59fab document 'disc_transfer'
desharna
parents: 58094
diff changeset
   888
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   889
\item[@{text "t."}\hthm{set} @{text "[simp, code]"}\rm:] ~ \\
53694
7b453b619b5f use singular to avoid confusion
blanchet
parents: 53691
diff changeset
   890
@{thm list.set(1)[no_vars]} \\
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58311
diff changeset
   891
@{thm list.set(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   892
The @{text "[code]"} attribute is set by the @{text code} plugin
blanchet
parents: 59282
diff changeset
   893
(Section~\ref{ssec:code-generator}).
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   894
57988
030ff4ceb6c3 updated docs
blanchet
parents: 57984
diff changeset
   895
\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
   896
@{thm list.set_cases[no_vars]}
6c992a4bcfbd document property 'set_cases'
desharna
parents: 57892
diff changeset
   897
57892
3d61d6a61cfc document property 'set_intros'
desharna
parents: 57701
diff changeset
   898
\item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
3d61d6a61cfc document property 'set_intros'
desharna
parents: 57701
diff changeset
   899
@{thm list.set_intros(1)[no_vars]} \\
3d61d6a61cfc document property 'set_intros'
desharna
parents: 57701
diff changeset
   900
@{thm list.set_intros(2)[no_vars]}
3d61d6a61cfc document property 'set_intros'
desharna
parents: 57701
diff changeset
   901
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   902
\item[@{text "t."}\hthm{set_sel}\rm:] ~ \\
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   903
@{thm list.set_sel[no_vars]}
57153
690cf0d83162 document property 'sel_set'
desharna
parents: 57094
diff changeset
   904
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
   905
\item[@{text "t."}\hthm{map} @{text "[simp, code]"}\rm:] ~ \\
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   906
@{thm list.map(1)[no_vars]} \\
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58311
diff changeset
   907
@{thm list.map(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   908
The @{text "[code]"} attribute is set by the @{text code} plugin
blanchet
parents: 59282
diff changeset
   909
(Section~\ref{ssec:code-generator}).
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   910
57983
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   911
\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
   912
@{thm list.map_disc_iff[no_vars]}
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   913
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   914
\item[@{text "t."}\hthm{map_sel}\rm:] ~ \\
6edc3529bb4e reordered some (co)datatype property names for more consistency
blanchet
parents: 57982
diff changeset
   915
@{thm list.map_sel[no_vars]}
57047
90d4db566e12 document property 'sel_map'
desharna
parents: 56995
diff changeset
   916
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   917
\item[@{text "t."}\hthm{rel_inject} @{text "[simp]"}\rm:] ~ \\
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   918
@{thm list.rel_inject(1)[no_vars]} \\
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   919
@{thm list.rel_inject(2)[no_vars]}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   920
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   921
\item[@{text "t."}\hthm{rel_distinct} @{text "[simp]"}\rm:] ~ \\
57526
7027cf5c1f2c document property 'rel_cases'
desharna
parents: 57494
diff changeset
   922
@{thm list.rel_distinct(1)[no_vars]} \\
7027cf5c1f2c document property 'rel_cases'
desharna
parents: 57494
diff changeset
   923
@{thm list.rel_distinct(2)[no_vars]}
7027cf5c1f2c document property 'rel_cases'
desharna
parents: 57494
diff changeset
   924
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   925
\item[@{text "t."}\hthm{rel_intros}\rm:] ~ \\
57494
c29729f764b1 document property 'rel_intros'
desharna
parents: 57490
diff changeset
   926
@{thm list.rel_intros(1)[no_vars]} \\
c29729f764b1 document property 'rel_intros'
desharna
parents: 57490
diff changeset
   927
@{thm list.rel_intros(2)[no_vars]}
c29729f764b1 document property 'rel_intros'
desharna
parents: 57490
diff changeset
   928
58474
330ebcc3e77d reintroduced 'rel_cases' in docs
blanchet
parents: 58449
diff changeset
   929
\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
   930
@{thm list.rel_cases[no_vars]}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   931
57564
4351b7b96abd document property 'rel_sel'
desharna
parents: 57558
diff changeset
   932
\item[@{text "t."}\hthm{rel_sel}\rm:] ~ \\
4351b7b96abd document property 'rel_sel'
desharna
parents: 57558
diff changeset
   933
@{thm list.rel_sel[no_vars]}
4351b7b96abd document property 'rel_sel'
desharna
parents: 57558
diff changeset
   934
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   935
\end{description}
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
   936
\end{indentblock}
54146
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   937
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   938
\noindent
97f69d44f732 doc fixes suggested by Andreas L.
blanchet
parents: 54072
diff changeset
   939
In addition, equational versions of @{text t.rel_inject} and @{text
59284
blanchet
parents: 59282
diff changeset
   940
rel_distinct} are registered with the @{text "[code]"} attribute. The
blanchet
parents: 59282
diff changeset
   941
@{text "[code]"} attribute is set by the @{text code} plugin
blanchet
parents: 59282
diff changeset
   942
(Section~\ref{ssec:code-generator}).
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   943
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   944
The second subgroup consists of more abstract properties of the set functions,
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   945
the map function, and the relator:
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   946
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   947
\begin{indentblock}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   948
\begin{description}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   949
57969
1e7b9579b14f note 'inj_map' more often
desharna
parents: 57933
diff changeset
   950
\item[@{text "t."}\hthm{inj_map}\rm:] ~ \\
1e7b9579b14f note 'inj_map' more often
desharna
parents: 57933
diff changeset
   951
@{thm list.inj_map[no_vars]}
1e7b9579b14f note 'inj_map' more often
desharna
parents: 57933
diff changeset
   952
57971
07e81758788d document 'inj_map_strong'
desharna
parents: 57969
diff changeset
   953
\item[@{text "t."}\hthm{inj_map_strong}\rm:] ~ \\
07e81758788d document 'inj_map_strong'
desharna
parents: 57969
diff changeset
   954
@{thm list.inj_map_strong[no_vars]}
07e81758788d document 'inj_map_strong'
desharna
parents: 57969
diff changeset
   955
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   956
\item[@{text "t."}\hthm{set_map}\rm:] ~ \\
56992
d0e5225601d3 document property 'disc_map_iff'
desharna
parents: 56957
diff changeset
   957
@{thm list.set_map[no_vars]}
d0e5225601d3 document property 'disc_map_iff'
desharna
parents: 56957
diff changeset
   958
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   959
\item[@{text "t."}\hthm{set_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
   960
@{thm list.set_transfer[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   961
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
59824
057b1018d589 clarified doc
blanchet
parents: 59793
diff changeset
   962
(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
58107
f3c5360711e9 document 'set_transfer'
desharna
parents: 58105
diff changeset
   963
58245
7e54225acef1 more docs
blanchet
parents: 58244
diff changeset
   964
\item[@{text "t."}\hthm{map_cong0}\rm:] ~ \\
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   965
@{thm list.map_cong0[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   966
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   967
\item[@{text "t."}\hthm{map_cong} @{text "[fundef_cong]"}\rm:] ~ \\
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   968
@{thm list.map_cong[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
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
58244
5e7830b39823 more documentation
blanchet
parents: 58235
diff changeset
   987
\item[@{text "t."}\hthm{rel_compp} @{text "[relator_distr]"}\rm:] ~ \\
58245
7e54225acef1 more docs
blanchet
parents: 58244
diff changeset
   988
@{thm list.rel_compp[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
   989
The @{text "[relator_distr]"} attribute is set by the @{text lifting} plugin
blanchet
parents: 59282
diff changeset
   990
(Section~\ref{ssec:lifting}).
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   991
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   992
\item[@{text "t."}\hthm{rel_conversep}\rm:] ~ \\
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   993
@{thm list.rel_conversep[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   994
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   995
\item[@{text "t."}\hthm{rel_eq}\rm:] ~ \\
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   996
@{thm list.rel_eq[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   997
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
   998
\item[@{text "t."}\hthm{rel_flip}\rm:] ~ \\
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
   999
@{thm list.rel_flip[no_vars]}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
  1000
57933
f620851148a9 document property 'rel_map'
desharna
parents: 57894
diff changeset
  1001
\item[@{text "t."}\hthm{rel_map}\rm:] ~ \\
f620851148a9 document property 'rel_map'
desharna
parents: 57894
diff changeset
  1002
@{thm list.rel_map(1)[no_vars]} \\
f620851148a9 document property 'rel_map'
desharna
parents: 57894
diff changeset
  1003
@{thm list.rel_map(2)[no_vars]}
f620851148a9 document property 'rel_map'
desharna
parents: 57894
diff changeset
  1004
58344
ea3d989219b4 set 'mono' attribute on 'rel_mono'
blanchet
parents: 58339
diff changeset
  1005
\item[@{text "t."}\hthm{rel_mono} @{text "[mono, relator_mono]"}\rm:] ~ \\
58245
7e54225acef1 more docs
blanchet
parents: 58244
diff changeset
  1006
@{thm list.rel_mono[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
  1007
The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin
blanchet
parents: 59282
diff changeset
  1008
(Section~\ref{ssec:lifting}).
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
  1009
61242
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1010
\item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1011
@{thm list.rel_mono_strong[no_vars]}
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1012
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1013
\item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1014
@{thm list.rel_cong[no_vars]}
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1015
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1016
\item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1017
@{thm list.rel_cong_simp[no_vars]}
1f92b0ac9c96 congruence rules for the relator
traytel
parents: 61240
diff changeset
  1018
59793
a46efc5510ea reordered properties
blanchet
parents: 59727
diff changeset
  1019
\item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
a46efc5510ea reordered properties
blanchet
parents: 59727
diff changeset
  1020
@{thm list.rel_refl[no_vars]}
a46efc5510ea reordered properties
blanchet
parents: 59727
diff changeset
  1021
61240
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1022
\item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1023
@{thm list.rel_refl_strong[no_vars]}
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1024
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1025
\item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1026
@{thm list.rel_reflp[no_vars]}
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1027
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1028
\item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1029
@{thm list.rel_symp[no_vars]}
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1030
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1031
\item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1032
@{thm list.rel_transp[no_vars]}
464c5da3f508 more useful properties of the relators
traytel
parents: 61076
diff changeset
  1033
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
  1034
\item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
  1035
@{thm list.rel_transfer[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
  1036
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
59824
057b1018d589 clarified doc
blanchet
parents: 59793
diff changeset
  1037
(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
58105
42c09d2ac48b document 'rel_transfer'
desharna
parents: 58103
diff changeset
  1038
54621
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
  1039
\end{description}
82a78bc9fa0d docs for forgotten BNF theorems
blanchet
parents: 54616
diff changeset
  1040
\end{indentblock}
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1041
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1042
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1043
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1044
subsubsection \<open> Inductive Theorems
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1045
  \label{sssec:inductive-theorems} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1046
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1047
text \<open>
53623
501e2091182b more (co)data docs
blanchet
parents: 53621
diff changeset
  1048
The inductive theorems are as follows:
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1049
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
  1050
\begin{indentblock}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1051
\begin{description}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1052
57304
d2061dc953a4 document property 'rel_coinduct'
desharna
parents: 57206
diff changeset
  1053
\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
  1054
@{thm list.induct[no_vars]}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1055
57542
faa8b4486d5a more docs
blanchet
parents: 57526
diff changeset
  1056
\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
  1057
@{thm list.rel_induct[no_vars]}
c2ee3f6754c8 document property 'rel_induct'
desharna
parents: 57398
diff changeset
  1058
57701
13b446b62825 document property 'set_induct'
desharna
parents: 57575
diff changeset
  1059
\item[\begin{tabular}{@ {}l@ {}}
13b446b62825 document property 'set_induct'
desharna
parents: 57575
diff changeset
  1060
  @{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
  1061
  @{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
  1062
\end{tabular}] ~ \\
57472
c2ee3f6754c8 document property 'rel_induct'
desharna
parents: 57398
diff changeset
  1063
Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
c2ee3f6754c8 document property 'rel_induct'
desharna
parents: 57398
diff changeset
  1064
prove $m$ properties simultaneously.
c2ee3f6754c8 document property 'rel_induct'
desharna
parents: 57398
diff changeset
  1065
53798
6a4e3299dfd1 set [code] on case equations
blanchet
parents: 53753
diff changeset
  1066
\item[@{text "t."}\hthm{rec} @{text "[simp, code]"}\rm:] ~ \\
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1067
@{thm list.rec(1)[no_vars]} \\
58335
a5a3b576fcfb generate 'code' attribute only if 'code' plugin is enabled
blanchet
parents: 58311
diff changeset
  1068
@{thm list.rec(2)[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
  1069
The @{text "[code]"} attribute is set by the @{text code} plugin
blanchet
parents: 59282
diff changeset
  1070
(Section~\ref{ssec:code-generator}).
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1071
58733
797d0e7aefc7 move documentation of 'rec_o_map'
desharna
parents: 58677
diff changeset
  1072
\item[@{text "t."}\hthm{rec_o_map}\rm:] ~ \\
797d0e7aefc7 move documentation of 'rec_o_map'
desharna
parents: 58677
diff changeset
  1073
@{thm list.rec_o_map[no_vars]}
797d0e7aefc7 move documentation of 'rec_o_map'
desharna
parents: 58677
diff changeset
  1074
58915
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
  1075
\item[@{text "t."}\hthm{rec_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
7d673ab6a8d9 document '*_transfer' attribute
desharna
parents: 58914
diff changeset
  1076
@{thm list.rec_transfer[no_vars]} \\
59284
blanchet
parents: 59282
diff changeset
  1077
The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin
59824
057b1018d589 clarified doc
blanchet
parents: 59793
diff changeset
  1078
(Section~\ref{ssec:transfer}) for type constructors with no dead type arguments.
58447
ea23ce403a3e document 'rec_transfer'
desharna
parents: 58395
diff changeset
  1079
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1080
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
  1081
\end{indentblock}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1082
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1083
\noindent
58310
91ea607a34d8 updated news
blanchet
parents: 58309
diff changeset
  1084
For convenience, @{command datatype} also provides the following collection:
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1085
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
  1086
\begin{indentblock}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1087
\begin{description}
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1088
59284
blanchet
parents: 59282
diff changeset
  1089
\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
  1090
@{text t.rel_distinct} @{text t.set}
53544
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1091
2176a7e40786 more (co)data docs
blanchet
parents: 53543
diff changeset
  1092
\end{description}
53552
eed6efba4e3f more (co)datatype docs
blanchet
parents: 53544
diff changeset
  1093
\end{indentblock}
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1094
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1095
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1096
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1097
subsection \<open> Proof Method
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1098
  \label{ssec:datatype-proof-method} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1099
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1100
subsubsection \<open> \textit{countable_datatype}
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1101
  \label{sssec:datatype-compat} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1102
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1103
text \<open>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1104
The theory @{file "~~/src/HOL/Library/Countable.thy"} provides a
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1105
proof method called @{text countable_datatype} that can be used to prove the
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1106
countability of many datatypes, building on the countability of the types
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1107
appearing in their definitions and of any type arguments. For example:
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1108
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1109
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1110
    instance list :: (countable) countable
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1111
      by countable_datatype
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1112
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1113
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1114
subsection \<open> Compatibility Issues
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1115
  \label{ssec:datatype-compatibility-issues} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1116
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1117
text \<open>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1118
The command @{command datatype} has been designed to be highly compatible with
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1119
the old command, to ease migration. There are nonetheless a few
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1120
incompatibilities that may arise when porting:
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1121
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1122
\begin{itemize}
53749
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
  1123
\setlength{\itemsep}{0pt}
b37db925b663 adapted primcorec documentation to reflect the three views
blanchet
parents: 53748
diff changeset
  1124
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1125
\item \emph{The Standard ML interfaces are different.} Tools and extensions
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1126
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
  1127
interfaces. The @{text BNF_LFP_Compat} structure provides convenience functions
852f7a49ec0c updated docs, esp. relating to 'datatype_compat'
blanchet
parents: 60134
diff changeset
  1128
that simulate the old interfaces in terms of the new ones.
54537
f37354a894a3 fixed LaTeX missing }
blanchet
parents: 54494
diff changeset
  1129
f37354a894a3 fixed LaTeX missing }
blanchet
parents: 54494
diff changeset
  1130
\item \emph{The recursor @{text rec_t} has a different signature for nested
54185
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
  1131
recursive datatypes.} In the old package, nested recursion through non-functions
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
  1132
was internally reduced to mutual recursion. This reduction was visible in the
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
  1133
type of the recursor, used by \keyw{primrec}. Recursion through functions was
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
  1134
handled specially. In the new package, nested recursion (for functions and
3fe3b5d33e41 more docs
blanchet
parents: 54184
diff changeset
  1135
non-functions) is handled in a more modular fashion. The old-style recursor can
56655
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
  1136
be generated on demand using @{command primrec} if the recursion is via
34f2fe40dc7b updated BNF docs
blanchet
parents: 56653
diff changeset
  1137
new-style datatypes, as explained in
61351
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1138
Section~\ref{sssec:primrec-nested-as-mutual-recursion}, or using
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1139
@{command datatype_compat}.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1140
54287
7f096d8eb3d0 more docs
blanchet
parents: 54278
diff changeset
  1141
\item \emph{Accordingly, the induction rule is different for nested recursive
61351
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1142
datatypes.} Again, the old-style induction rule can be generated on demand
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1143
using @{command primrec} if the recursion is via new-style datatypes, as
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1144
explained in Section~\ref{sssec:primrec-nested-as-mutual-recursion}, or using
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1145
@{command datatype_compat}. For recursion through functions, the old-style
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1146
induction rule can be obtained by applying the @{text "[unfolded
c0c8bce2a21b clarify docs
blanchet
parents: 61350
diff changeset
  1147
all_mem_range]"} attribute on @{text t.induct}.
52828
e1c6fa322d96 more (co)datatype docs
blanchet
parents: 52827
diff changeset
  1148
58336
a7add8066122 document size difference
blanchet
parents: 58335
diff changeset
  1149
\item \emph{The @{const size} function has a slightly different definition.}
a7add8066122 document size difference
blanchet
parents: 58335
diff changeset
  1150
The new function returns @{text 1} instead of @{text 0} for some nonrecursive
a7add8066122 document size difference
blanchet
parents: 58335
diff changeset
  1151
constructors. This departure from the old behavior made it possible to implement
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1152
@{const size} in terms of the generic function @{text "t.size_t"}. Moreover,
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1153
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
  1154
recursive case. The old behavior can be obtained by disabling the @{text size}
59282
blanchet
parents: 59280
diff changeset
  1155
plugin (Section~\ref{sec:selecting-plugins}) and instantiating the
58339
f6af48bd7c04 more hints on how to port 'size'
blanchet
parents: 58336
diff changeset
  1156
@{text size} type class manually.
58336
a7add8066122 document size difference
blanchet
parents: 58335
diff changeset
  1157
53863
c7364dca96f2 textual improvements following Christian Sternagel's feedback
blanchet
parents: 53857
diff changeset
  1158
\item \emph{The internal constructions are completely different.} Proof texts
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1159
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
  1160
be difficult to port.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1161
58207
75b3a5e95d68 more compatibility documentation
blanchet
parents: 58192
diff changeset
  1162
\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
  1163
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
  1164
the alias @{text t.inducts} for @{text t.induct} is no longer generated.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1165
For $m > 1$ mutually recursive datatypes,
58207
75b3a5e95d68 more compatibility documentation
blanchet
parents: 58192
diff changeset
  1166
@{text "rec_t\<^sub>1_\<dots>_t\<^sub>m_i"} has been renamed
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1167
@{text "rec_t\<^sub>i"} for each @{text "i \<in> {1, \<dots>, m}"},
53997
8ff43f638da2 more "primrec_new" documentation
blanchet
parents: 53917
diff changeset
  1168
@{text "t\<^sub>1_\<dots>_t\<^sub>m.inducts(i)"} has been renamed
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1169
@{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
  1170
collection @{text "t\<^sub>1_\<dots>_t\<^sub>m.size"} (generated by the
75b3a5e95d68 more compatibility documentation
blanchet
parents: 58192
diff changeset
  1171
@{text size} plugin, Section~\ref{ssec:size}) has been divided into
75b3a5e95d68 more compatibility documentation
blanchet
parents: 58192
diff changeset
  1172
@{text "t\<^sub>1.size"}, \ldots, @{text "t\<^sub>m.size"}.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1173
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1174
\item \emph{The @{text t.simps} collection has been extended.}
58207
75b3a5e95d68 more compatibility documentation
blanchet
parents: 58192
diff changeset
  1175
Previously available theorems are available at the same index as before.
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1176
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1177
\item \emph{Variables in generated properties have different names.} This is
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1178
rarely an issue, except in proof texts that refer to variable names in the
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1179
@{text "[where \<dots>]"} attribute. The solution is to use the more robust
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1180
@{text "[of \<dots>]"} syntax.
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1181
\end{itemize}
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1182
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1183
The old command is still available as \keyw{old_datatype} in theory
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1184
@{file "~~/src/HOL/Library/Old_Datatype.thy"}. However, there is no general
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1185
way to register old-style datatypes as new-style datatypes. If the objective
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1186
is to define new-style datatypes with nested recursion through old-style
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1187
datatypes, the old-style datatypes can be registered as a BNF
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1188
(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
  1189
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
  1190
@{command free_constructors}
53647
e78ebb290dd6 more (co)data docs
blanchet
parents: 53646
diff changeset
  1191
(Section~\ref{sec:deriving-destructors-and-theorems-for-free-constructors}).
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1192
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1193
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1194
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1195
section \<open> Defining Primitively Recursive Functions
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1196
  \label{sec:defining-primitively-recursive-functions} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1197
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1198
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
  1199
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
  1200
command, which supports primitive recursion, or using the more general
59861
99d9304daeb4 tuned doc
blanchet
parents: 59824
diff changeset
  1201
\keyw{fun}, \keyw{function}, and \keyw{partial_function} commands. In this
99d9304daeb4 tuned doc
blanchet
parents: 59824
diff changeset
  1202
tutorial, the focus is on @{command primrec}; \keyw{fun} and \keyw{function} are
99d9304daeb4 tuned doc
blanchet
parents: 59824
diff changeset
  1203
described in a separate tutorial @{cite "isabelle-function"}.
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1204
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1205
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1206
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1207
subsection \<open> Introductory Examples
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1208
  \label{ssec:primrec-introductory-examples} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1209
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1210
text \<open>
53646
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1211
Primitive recursion is illustrated through concrete examples based on the
ac6e0a28489f more (co)data docs
blanchet
parents: 53644
diff changeset
  1212
datatypes defined in Section~\ref{ssec:datatype-introductory-examples}. More
61304
754e8ddbbc82 tuned documentation
blanchet
parents: 61303
diff changeset
  1213
examples can be found in the directory @{file "~~/src/HOL/Datatype_Examples"}.
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1214
\<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1215
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1216
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1217
subsubsection \<open> Nonrecursive Types
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1218
  \label{sssec:primrec-nonrecursive-types} \<close>
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1219
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1220
text \<open>
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1221
Primitive recursion removes one layer of constructors on the left-hand side in
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1222
each equation. For example:
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1223
\<close>
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1224
60136
4e1ba085be4a suppressed warnings
blanchet
parents: 60135
diff changeset
  1225
    primrec (nonexhaustive) bool_of_trool :: "trool \<Rightarrow> bool" where
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1226
      "bool_of_trool Faalse \<longleftrightarrow> False"
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1227
    | "bool_of_trool Truue \<longleftrightarrow> True"
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1228
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1229
text \<open> \blankline \<close>
52841
87a66bad0796 more (co)datatype documentation
blanchet
parents: 52840
diff changeset
  1230
55530
3dfb724db099 renamed 'primrec_new' to 'primrec', overriding the old command (which it still uses as a fallback for old-style datatypes)
blanchet
parents: 55474
diff changeset
  1231
    primrec the_list :: "'a option \<Rightarrow> 'a list" where
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1232
      "the_list None = []"
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1233
    | "the_list (Some a) = [a]"
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1234
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1235
text \<open> \blankline \<close>
53621
9c3a80af72ff more (co)data doc
blanchet
parents: 53619
diff changeset
  1236
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
  1237
    primrec the_default :: "'a \<Rightarrow> 'a option \<Rightarrow> 'a" where
62081
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1238
      "the_default d None = d"
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1239
    | "the_default _ (Some a) = a"
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff changeset
  1240
fd18b51bdc55 updated docs
blanchet
parents: 61788
diff ch