src/Doc/Datatypes/Datatypes.thy

 datatypes, or \emph{codatatypes}, which may have infinite values. For example,
 the following command introduces the type of lazy lists, which comprises both
 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
 Mixed inductive--coinductive recursion is possible via nesting. Compare the
 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"
     codatatype 'a tree\<^sub>i\<^sub>i = Node\<^sub>i\<^sub>i 'a "'a tree\<^sub>i\<^sub>i llist"
 (*<*)

 
 section {* Defining Datatypes
   \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|.
 *}
 
 
 subsection {* Introductory Examples
   \label{ssec:datatype-introductory-examples} *}

 \emph{Mutually recursive} types are introduced simultaneously and may refer to
 each other. The example below introduces a pair of types for even and odd
 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
 Arithmetic expressions are defined via terms, terms via factors, and factors via
 expressions:

 
 @{rail "
   @@{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
 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
 manual \cite{isabelle-isar-ref}.

 
 \begin{itemize}
 \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.
 \end{itemize}
 

 \noindent
 where the \textit{names} argument is simply a space-separated list of type names
 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
 must be new-style datatypes. In principle, it should be possible to support
 old-style datatypes as well, but the command does not support this yet.

 
 subsection {* Generated Constants
   \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:
 
 \begin{itemize}

 subsection {* Generated Theorems
   \label{ssec:datatype-generated-theorems} *}
 
 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
 and destructors that can be derived for any freely generated type. Internally,
 the derivation is performed by @{command wrap_free_constructors}.

 
 subsubsection {* Functorial Theorems
   \label{sssec:functorial-theorems} *}
 
 text {*
-The BNF-related theorem are listed below:
+The BNF-related theorem are as follows:
 
 \begin{indentblock}
 \begin{description}
 
 \item[@{text "t."}\hthm{sets} @{text "[code]"}\rmfamily:] ~ \\

 
 subsubsection {* Inductive Theorems
   \label{sssec:inductive-theorems} *}
 
 text {*
-The inductive theorems are listed below:
+The inductive theorems are as follows:
 
 \begin{indentblock}
 \begin{description}
 
 \item[@{text "t."}\hthm{induct} @{text "[induct t, case_names C\<^sub>1 \<dots> C\<^sub>n]"}\rmfamily:] ~ \\

 %      * use fun
 %      * use extensions like size (needed for fun), the AFP order, Quickcheck,
 %        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?)
 %        * nested datatypes? (fails with datatype_new?)
 %    * option 2

 The syntax for mutually recursive functions over mutually recursive datatypes
 is straightforward:
 *}
 
     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
       eval\<^sub>t :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) trm \<Rightarrow> int" and
       eval\<^sub>f :: "('a \<Rightarrow> int) \<Rightarrow> ('b \<Rightarrow> int) \<Rightarrow> ('a, 'b) fct \<Rightarrow> int"

 recursive calls are lifted to lists using @{const map}:
 *}
 
 (*<*)
     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
 (*>*)
     primrec_new at\<^sub>f\<^sub>f :: "'a tree\<^sub>f\<^sub>f \<Rightarrow> nat list \<Rightarrow> 'a" where

     end
 (*>*)
 
 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}:
 *}
 
 (*<*)
     locale sum_btree_nested

 *}
 *)
 
 
 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
 on which it is not otherwise specified. Occasionally, it is useful to have the
 default value be defined recursively. This produces a chicken-and-egg situation

 
 section {* Defining Codatatypes
   \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} *}
 
-text {*
-More examples in \verb|~~/src/HOL/BNF/Examples|.
-*}
-*)
+
+subsubsection {* Simple Corecursion
+  \label{sssec:codatatype-simple-corecursion} *}
+
+text {*
+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
   \label{ssec:codatatype-command-syntax} *}
 

   \label{sssec:codatatype} *}
 
 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}.
+*}
+
+
+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.
+
+\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)
 *}
 

 subsection {* Introductory Examples
   \label{ssec:primcorec-introductory-examples} *}
 
 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}).
 *}
 *)
 
 
 subsection {* Command Syntax

 subsection {* Generated Theorems
   \label{ssec:primcorec-generated-theorems} *}
 *)
 
 
+(*
+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).
 
 *}
 
 
 (*

 
 section {* Deriving Destructors and Theorems for Free Constructors
   \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 ...
 %
 %  * also useful for compatibility with old package, e.g. add destructors to
 %    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)
 *}
 
 
 (*

 (*
 section {* Standard ML Interface
   \label{sec:standard-ml-interface} *}
 
 text {*
-This section describes the package's programmatic interface.
+The package's programmatic interface.
 *}
 *)
 
 
 (*
 section {* Interoperability
   \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.
 *}
 
 
 subsection {* Transfer and Lifting
   \label{ssec:transfer-and-lifting} *}

 (*
 section {* Known Bugs and Limitations
   \label{sec:known-bugs-and-limitations} *}
 
 text {*
-This section lists known open issues of the package.
+Known open issues of the package.
 *}
 
 text {*
 %* primcorec is unfinished
 %