--- a/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 19:38:09 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Fri Sep 13 21:28:57 2013 +0200
@@ -51,7 +51,11 @@
finite and infinite values:
*}
- codatatype 'a llist (*<*)(map: lmap) (*>*)= LNil | LCons 'a "'a llist"
+(*<*)
+ locale dummy_llist
+ begin
+(*>*)
+ codatatype 'a llist = LNil | LCons 'a "'a llist"
text {*
\noindent
@@ -59,10 +63,6 @@
following four Rose tree examples:
*}
-(*<*)
- locale dummy_tree
- begin
-(*>*)
datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
codatatype 'a tree\<^sub>i\<^sub>f = Node\<^sub>i\<^sub>f 'a "'a tree\<^sub>i\<^sub>f list"
@@ -177,10 +177,10 @@
\label{sec:defining-datatypes} *}
text {*
-This section describes how to specify datatypes using the @{command
-datatype_new} command. The command is first illustrated through concrete
-examples featuring different flavors of recursion. More examples can be found in
-the directory \verb|~~/src/HOL/BNF/Examples|.
+Datatypes can be specified using the @{command datatype_new} command. The
+command is first illustrated through concrete examples featuring different
+flavors of recursion. More examples can be found in the directory
+\verb|~~/src/HOL/BNF/Examples|.
*}
@@ -272,8 +272,8 @@
natural numbers:
*}
- datatype_new enat = EZero | ESuc onat
- and onat = OSuc enat
+ datatype_new even_nat = Even_Zero | Even_Suc odd_nat
+ and odd_nat = Odd_Suc even_nat
text {*
\noindent
@@ -443,7 +443,7 @@
@@{command_def datatype_new} target? @{syntax dt_options}? \\
(@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
;
- @{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
+ @{syntax_def dt_options}: '(' (('no_discs_sels' | 'rep_compat') + ',') ')'
"}
The syntactic quantity \synt{target} can be used to specify a local
@@ -456,11 +456,11 @@
\setlength{\itemsep}{0pt}
\item
-The \keyw{no\_discs\_sels} option indicates that no discriminators or selectors
+The @{text "no_discs_sels"} option indicates that no discriminators or selectors
should be generated.
\item
-The \keyw{rep\_compat} option indicates that the names generated by the
+The @{text "rep_compat"} option indicates that the names generated by the
package should contain optional (and normally not displayed) ``@{text "new."}''
components to prevent clashes with a later call to \keyw{rep\_datatype}. See
Section~\ref{ssec:datatype-compatibility-issues} for details.
@@ -557,15 +557,15 @@
that are mutually recursive. For example:
*}
- datatype_new_compat enat onat
+ datatype_new_compat even_nat odd_nat
text {* \blankline *}
- thm enat_onat.size
+ thm even_nat_odd_nat.size
text {* \blankline *}
- ML {* Datatype_Data.get_info @{theory} @{type_name enat} *}
+ ML {* Datatype_Data.get_info @{theory} @{type_name even_nat} *}
text {*
For nested recursive datatypes, all types through which recursion takes place
@@ -578,7 +578,7 @@
\label{ssec:datatype-generated-constants} *}
text {*
-Given a type @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+Given a datatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
with $m > 0$ live type variables and $n$ constructors
@{text "t.C\<^sub>1"}, \ldots, @{text "t.C\<^sub>n"}, the
following auxiliary constants are introduced:
@@ -622,7 +622,7 @@
text {*
The characteristic theorems generated by @{command datatype_new} are grouped in
-two broad categories:
+three broad categories:
\begin{itemize}
\item The \emph{free constructor theorems} are properties about the constructors
@@ -767,7 +767,7 @@
\label{sssec:functorial-theorems} *}
text {*
-The BNF-related theorem are listed below:
+The BNF-related theorem are as follows:
\begin{indentblock}
\begin{description}
@@ -797,7 +797,7 @@
\label{sssec:inductive-theorems} *}
text {*
-The inductive theorems are listed below:
+The inductive theorems are as follows:
\begin{indentblock}
\begin{description}
@@ -856,7 +856,7 @@
% Nitpick
% * provide exactly the same theorems with the same names (compatibility)
% * option 1
-% * \keyw{rep\_compat}
+% * @{text "rep_compat"}
% * \keyw{rep\_datatype}
% * has some limitations
% * mutually recursive datatypes? (fails with rep_datatype?)
@@ -989,12 +989,12 @@
*}
primrec_new
- nat_of_enat :: "enat \<Rightarrow> nat" and
- nat_of_onat :: "onat \<Rightarrow> nat"
+ nat_of_even_nat :: "even_nat \<Rightarrow> nat" and
+ nat_of_odd_nat :: "odd_nat \<Rightarrow> nat"
where
- "nat_of_enat EZero = Zero" |
- "nat_of_enat (ESuc n) = Suc (nat_of_onat n)" |
- "nat_of_onat (OSuc n) = Suc (nat_of_enat n)"
+ "nat_of_even_nat Even_Zero = Zero" |
+ "nat_of_even_nat (Even_Suc n) = Suc (nat_of_odd_nat n)" |
+ "nat_of_odd_nat (Odd_Suc n) = Suc (nat_of_even_nat n)"
primrec_new
eval\<^sub>e :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) exp \<Rightarrow> int" and
@@ -1035,7 +1035,6 @@
(*<*)
datatype_new 'a tree\<^sub>f\<^sub>f = Node\<^sub>f\<^sub>f 'a "'a tree\<^sub>f\<^sub>f list"
- datatype_new 'a tree\<^sub>f\<^sub>i = Node\<^sub>f\<^sub>i 'a "'a tree\<^sub>f\<^sub>i llist"
context dummy_tlist
begin
@@ -1051,7 +1050,7 @@
text {*
The next example features recursion through the @{text option} type. Although
-@{text option} is not a new-style datatype, it is registered as a BNF, with the
+@{text option} is not a new-style datatype, it is registered as a BNF with the
map function @{const option_map}:
*}
@@ -1187,7 +1186,7 @@
subsection {* Recursive Default Values for Selectors
- \label{ssec:recursive-default-values-for-selectors} *}
+ \label{ssec:primrec-recursive-default-values-for-selectors} *}
text {*
A datatype selector @{text un_D} can have a default value for each constructor
@@ -1269,23 +1268,71 @@
\label{sec:defining-codatatypes} *}
text {*
-This section describes how to specify codatatypes using the @{command
-codatatype} command. The command is first illustrated through concrete examples
-featuring different flavors of corecursion. More examples can be found in the
-directory \verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs}
-also includes some useful codatatypes, notably for lazy lists
-\cite{lochbihler-2010}.
+Codatatypes can be specified using the @{command codatatype} command. The
+command is first illustrated through concrete examples featuring different
+flavors of corecursion. More examples can be found in the directory
+\verb|~~/src/HOL/BNF/Examples|. The \emph{Archive of Formal Proofs} also
+includes some useful codatatypes, notably for lazy lists \cite{lochbihler-2010}.
*}
-(*
subsection {* Introductory Examples
\label{ssec:codatatype-introductory-examples} *}
+
+subsubsection {* Simple Corecursion
+ \label{sssec:codatatype-simple-corecursion} *}
+
text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
+Noncorecursive codatatypes coincide with the corresponding datatypes, so
+they have no practical uses. \emph{Corecursive codatatypes} have the same syntax
+as recursive datatypes, except for the command name. For example, here is the
+definition of lazy lists:
+*}
+
+ codatatype (lset: 'a) llist (map: lmap rel: llist_all2) =
+ lnull: LNil (defaults ltl: LNil)
+ | LCons (lhd: 'a) (ltl: "'a llist")
+
+text {*
+\noindent
+Lazy lists can be infinite, such as @{text "LCons 0 (LCons 0 (\<dots>))"} and
+@{text "LCons 0 (LCons 1 (LCons 2 (\<dots>)))"}. Another interesting type that can
+be defined as a codatatype is that of the extended natural numbers:
+*}
+
+ codatatype enat = EZero | ESuc nat
+
+text {*
+\noindent
+This type has exactly one infinite element, @{text "ESuc (ESuc (ESuc (\<dots>)))"},
+that represents $\infty$. In addition, it has finite values of the form
+@{text "ESuc (\<dots> (ESuc EZero)\<dots>)"}.
*}
-*)
+
+
+subsubsection {* Mutual Corecursion
+ \label{sssec:codatatype-mutual-corecursion} *}
+
+text {*
+\noindent
+The example below introduces a pair of \emph{mutually corecursive} types:
+*}
+
+ codatatype even_enat = Even_EZero | Even_ESuc odd_enat
+ and odd_enat = Odd_ESuc even_enat
+
+
+subsubsection {* Nested Corecursion
+ \label{sssec:codatatype-nested-corecursion} *}
+
+text {*
+\noindent
+The next two examples feature \emph{nested corecursion}:
+*}
+
+ codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
+ codatatype 'a tree\<^sub>i\<^sub>s = Node\<^sub>i\<^sub>s 'a "'a tree\<^sub>i\<^sub>s fset"
subsection {* Command Syntax
@@ -1298,29 +1345,116 @@
text {*
Definitions of codatatypes have almost exactly the same syntax as for datatypes
(Section~\ref{ssec:datatype-command-syntax}), with two exceptions: The command
-is called @{command codatatype}; the \keyw{no\_discs\_sels} option is not
-available, because destructors are a central notion for codatatypes.
+is called @{command codatatype}. The @{text "no_discs_sels"} option is not
+available, because destructors are a crucial notion for codatatypes.
+*}
+
+
+subsection {* Generated Constants
+ \label{ssec:codatatype-generated-constants} *}
+
+text {*
+Given a codatatype @{text "('a\<^sub>1, \<dots>, 'a\<^sub>m) t"}
+with $m > 0$ live type variables and $n$ constructors @{text "t.C\<^sub>1"},
+\ldots, @{text "t.C\<^sub>n"}, the same auxiliary constants are generated as for
+datatypes (Section~\ref{ssec:datatype-generated-constants}), except that the
+iterator and the recursor are replaced by dual concepts:
+
+\begin{itemize}
+\setlength{\itemsep}{0pt}
+
+\item \relax{Coiterator}: @{text t_unfold}
+
+\item \relax{Corecursor}: @{text t_corec}
+
+\end{itemize}
+*}
+
+
+subsection {* Generated Theorems
+ \label{ssec:codatatype-generated-theorems} *}
+
+text {*
+The characteristic theorems generated by @{command codatatype} are grouped in
+three broad categories:
+
+\begin{itemize}
+\item The \emph{free constructor theorems} are properties about the constructors
+and destructors that can be derived for any freely generated type.
+
+\item The \emph{functorial theorems} are properties of datatypes related to
+their BNF nature.
+
+\item The \emph{coinductive theorems} are properties of datatypes related to
+their coinductive nature.
+\end{itemize}
+
+\noindent
+The first two categories are exactly as for datatypes and are described in
+Sections \ref{ssec:free-constructor-theorems}~and~\ref{ssec:functorial-theorems}.
*}
-(*
-subsection {* Generated Constants
- \label{ssec:codatatype-generated-constants} *}
-*)
+subsubsection {* Coinductive Theorems
+ \label{sssec:coinductive-theorems} *}
+
+text {*
+The coinductive theorems are as follows:
+
+% [(coinductN, map single coinduct_thms,
+% fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
+% (corecN, corec_thmss, K coiter_attrs),
+% (disc_corecN, disc_corec_thmss, K disc_coiter_attrs),
+% (disc_corec_iffN, disc_corec_iff_thmss, K disc_coiter_iff_attrs),
+% (disc_unfoldN, disc_unfold_thmss, K disc_coiter_attrs),
+% (disc_unfold_iffN, disc_unfold_iff_thmss, K disc_coiter_iff_attrs),
+% (sel_corecN, sel_corec_thmss, K sel_coiter_attrs),
+% (sel_unfoldN, sel_unfold_thmss, K sel_coiter_attrs),
+% (simpsN, simp_thmss, K []),
+% (strong_coinductN, map single strong_coinduct_thms, K coinduct_attrs),
+% (unfoldN, unfold_thmss, K coiter_attrs)]
+% |> massage_multi_notes;
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{coinduct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
+@{thm llist.coinduct[no_vars]}
+\item[@{text "t\<^sub>1_\<dots>_t\<^sub>m."}\hthm{coinduct} @{text "[case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\
+Given $m > 1$ mutually recursive datatypes, this induction rule can be used to
+prove $m$ properties simultaneously.
-(*
-subsection {* Generated Theorems
- \label{ssec:codatatype-generated-theorems} *}
-*)
+\item[@{text "t."}\hthm{unfold} @{text "[code]"}\rmfamily:] ~ \\
+@{thm llist.unfold(1)[no_vars]} \\
+@{thm llist.unfold(2)[no_vars]}
+
+\item[@{text "t."}\hthm{corec} @{text "[code]"}\rmfamily:] ~ \\
+@{thm llist.corec(1)[no_vars]} \\
+@{thm llist.corec(2)[no_vars]}
+
+\end{description}
+\end{indentblock}
+
+\noindent
+For convenience, @{command codatatype} also provides the following collection:
+
+\begin{indentblock}
+\begin{description}
+
+\item[@{text "t."}\hthm{simps} = @{text t.inject} @{text t.distinct} @{text t.case} @{text t.rec} @{text t.fold} @{text t.map} @{text t.rel_inject}] ~ \\
+@{text t.rel_distinct} @{text t.sets}
+
+\end{description}
+\end{indentblock}
+*}
section {* Defining Corecursive Functions
\label{sec:defining-corecursive-functions} *}
text {*
-This section describes how to specify corecursive functions using the
-@{command primcorec} command.
+Corecursive functions can be specified using the @{command primcorec} command.
%%% TODO: partial_function? E.g. for defining tail recursive function on lazy
%%% lists (cf. terminal0 in TLList.thy)
@@ -1333,9 +1467,6 @@
text {*
More examples in \verb|~~/src/HOL/BNF/Examples|.
-
-Also, for default values, the same trick as for datatypes is possible for
-codatatypes (Section~\ref{ssec:recursive-default-values-for-selectors}).
*}
*)
@@ -1365,13 +1496,23 @@
*)
+(*
+subsection {* Recursive Default Values for Selectors
+ \label{ssec:primcorec-recursive-default-values-for-selectors} *}
+
+text {*
+partial_function to the rescue
+*}
+*)
+
+
section {* Registering Bounded Natural Functors
\label{sec:registering-bounded-natural-functors} *}
text {*
-This section explains how to set up the (co)datatype package to allow nested
-recursion through custom well-behaved type constructors. The key concept is that
-of a bounded natural functor (BNF).
+The (co)datatype package can be set up to allow nested recursion through custom
+well-behaved type constructors. The key concept is that of a bounded natural
+functor (BNF).
*}
@@ -1420,8 +1561,9 @@
\label{sec:deriving-destructors-and-theorems-for-free-constructors} *}
text {*
-This section explains how to derive convenience theorems for free constructors,
-as performed internally by @{command datatype_new} and @{command codatatype}.
+The derivation of convenience theorems for types equipped with free constructors,
+as performed internally by @{command datatype_new} and @{command codatatype},
+is available as a stand-alone command called @{command wrap_free_constructors}.
% * need for this is rare but may arise if you want e.g. to add destructors to
% a type not introduced by ...
@@ -1430,7 +1572,7 @@
% old \keyw{datatype}
%
% * @{command wrap_free_constructors}
-% * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
+% * @{text "no_discs_sels"}, @{text "rep_compat"}
% * hack to have both co and nonco view via locale (cf. ext nats)
*}
@@ -1473,7 +1615,7 @@
\label{sec:standard-ml-interface} *}
text {*
-This section describes the package's programmatic interface.
+The package's programmatic interface.
*}
*)
@@ -1483,9 +1625,8 @@
\label{sec:interoperability} *}
text {*
-This section is concerned with the packages' interaction with other Isabelle
-packages and tools, such as the code generator and the counterexample
-generators.
+The package's interaction with other Isabelle packages and tools, such as the
+code generator and the counterexample generators.
*}
@@ -1515,7 +1656,7 @@
\label{sec:known-bugs-and-limitations} *}
text {*
-This section lists known open issues of the package.
+Known open issues of the package.
*}
text {*